From 29fe3e1aa5c0dfc50a802019276c77a7b59eaf06 Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Wed, 28 Oct 2026 21:26:55 +0800 Subject: [PATCH] feat(schema): persist and instantiate scoped multi-role relation schemas --- docs/research-plan.md | 12 +- docs/simplex-schema.md | 163 +++ examples/simplex_registry.py | 35 + experiments/P0-pilot/README.md | 10 + experiments/P0-pilot/build_schemas.py | 185 +++ .../results/simplex-schema-index.json | 1210 +++++++++++++++++ .../results/simplex-schema-summary.json | 27 + leanbench/schema.py | 69 +- leanbench/schema_registry.py | 208 +++ tests/test_schema_registry.py | 162 +++ 10 files changed, 2068 insertions(+), 13 deletions(-) create mode 100644 docs/simplex-schema.md create mode 100644 examples/simplex_registry.py create mode 100644 experiments/P0-pilot/build_schemas.py create mode 100644 experiments/P0-pilot/results/simplex-schema-index.json create mode 100644 experiments/P0-pilot/results/simplex-schema-summary.json create mode 100644 leanbench/schema_registry.py create mode 100644 tests/test_schema_registry.py diff --git a/docs/research-plan.md b/docs/research-plan.md index 0b163c3..b444060 100644 --- a/docs/research-plan.md +++ b/docs/research-plan.md @@ -8,9 +8,15 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro ## 0. The idea in one page +**Terminology clarification (2026-10-28).** The owner uses "simplex" for a semantic, +multi-role relation schema: one statement joins objects, assumptions and a conclusion. +It does not mean a geometric simplex or assert a mathematical simplicial complex. +See [the implemented schema design](simplex-schema.md) for scoped slots, storage and +candidate retrieval. Existing signature projections and AI source annotations remain partial. + **Simplex, as it exists in the archived code.** - `Role(name, context, choices)`: a named semantic slot with a description and an optional closed set of allowed values (`is_constrained`, `validate_value`). -- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so simplices nest; nesting gives a *simplicial complex*. `Equivalence` is the two-role special case. +- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so explicitly supplied schemas can be nested as semantic composition. `Equivalence` is the two-role special case. - `State` / `Fact` / `Goal`: a role plus a value. A `Fact` has a value, a `Goal` does not; `SolvingTask.is_completed()` is "every goal resolved". - `SchemaRegistry` (SQLite): `set_role`, `set_simplex`, `search_roles`, `find_by_roles(known_roles)`, `find_solvable(known_role_names)`. - `SchemaParserAgent`: turns a query into a Simplex through a forced tool call whose JSON schema says `minItems: 2`, with a **search-first, reuse-before-create** rule for roles. `AnalogySchemaMiner`: proposes new simplices by the ratio *Simplex B : Role B :: Simplex A : Role A*. @@ -19,11 +25,11 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro | Lean | Simplex view | |---|---| -| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", `choices` = admissible type/class constraints | +| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", type/class constraints as attributes; `choices` only for explicit finite value sets | | `(h : P x)` hypothesis | `Fact` role | | conclusion after the final `:` | `Goal` role | | `def` / `structure` being introduced | `own` role (what the thing *is*) | -| a lemma used inside a proof | nested simplex (edge in the complex) | +| a lemma used inside a proof | explicit nested schema reference (when recorded) | `leanbench/typeindex.py` already extracts exactly this split: `input` (binders and hypotheses), `goal` (the conclusion), `own` (definitions). So the type index is a simplex index in all but name. The new work is to make it a **first-class schema that steers inference** instead of a passive index. diff --git a/docs/simplex-schema.md b/docs/simplex-schema.md new file mode 100644 index 0000000..4a1c8d8 --- /dev/null +++ b/docs/simplex-schema.md @@ -0,0 +1,163 @@ +# Simplex schema: a semantic relation joining roles + +Here **simplex** means the owner's multi-role relation pattern: one statement relates +objects, assumptions and a conclusion. The implementation does not construct geometric +simplices, faces, boundaries or a mathematical simplicial complex. + +## The model + +| Concept | Representation | Meaning | +|---|---|---| +| Reusable role definition | `Role` | A semantic slot type with optional textual type/context and finite `choices` | +| Statement/relation pattern | `Simplex` | A named mapping from at least two local aliases to roles | +| Object or assumption supplied by a caller | `Fact` | A role plus a non-None value | +| Requested result | `Goal` | A role whose value is not supplied yet | +| Application to particular objects | `SimplexInstance` | Facts and goals bound by local slot alias | +| Explicit composition | A `Simplex` used as a role | A supplied nested pattern; no proof dependency is discovered automatically | +| Persistent catalog | `SchemaRegistry` | JSON/SQLite nodes and alias-to-definition references | + +`kind` separates `object`, `fact`, `goal`, `own` and nested `simplex` roles. +A role's `attrs.references` may name other aliases in the same simplex; unknown aliases +are rejected. These references can describe the objects mentioned in an assumption or +conclusion. They are not geometric edges. Their provenance must distinguish manually +supplied relationships from incomplete syntactic candidates. + +`type_text` is descriptive Lean/mathematical text, not an executable type checker. +`choices` is a finite set of admissible values, not a replacement for arbitrary Lean typeclass +constraints. Supplied fact and resolved goal values are checked against explicit choices. +No registry method establishes that a string is a proof or that a mathematical premise is true. + +## Concrete example: two groups and a homomorphism + +One schema joins these slots: + +| Local alias | Role | Type/claim | References | +|---|---|---|---| +| `left` | object | group carrier | none | +| `right` | object | group carrier | none | +| `map` | object | `left →* right` | left, right | +| `bijective` | fact | `Bijective map` | map | +| `goal` | goal | `Nonempty (left ≃* right)` | left, right | + +The simplex is this complete relation pattern, not an individual role or an asserted +geometric object. `left` and `right` may explicitly reuse the same `role:group` definition +while binding to different group objects. Reusing a role definition does not equate their values. + +Run the synthetic, offline example: + +```sh +PYTHONPATH=. python3 examples/simplex_registry.py +``` + +It binds symbolic caller values for the input slots, leaves the goal unresolved, and returns +a structurally ready candidate. It does not run a Lean proof. + +## Scope, persistence and reuse + +`SchemaRegistry.set_simplex` assigns every child a scoped key by default: +`/slot/`. Thus `G` in one theorem is not the same object as `G` +in another. Corpus keys also include the frozen annotation hash and item identity. + +To reuse a definition, register it with `set_role` and explicitly pass a `role_keys` mapping +to `set_simplex`. The referenced definition must match the supplied role exactly. A shared +definition still has distinct occurrence keys for every alias. No role is semantically merged +merely because its spelling, type text or keywords resemble another role. + +Keys are immutable within a registry. Identical registration is idempotent; changed content +or changed definition references require a new version key. `get_role` and `get_simplex` +resolve exact keys, not ambiguous bare names. `search_roles` returns literal-substring candidates +for a caller to review; it does not approve semantic reuse. + +Serialization includes names, kinds, context, types, choices, attributes and nested aliases. +`role_from_dict` restores JSON snapshots. SQLite uses one connection and one transaction per +nested registration, foreign keys and JSON payloads; it does not load archived pickle blobs. +Cyclic nesting and failed reuse checks roll back the complete write. Returned objects are +restored snapshots; changing one does not silently update a registered definition. + +## Query and binding APIs + +```python +from leanbench.schema_registry import SchemaRegistry, slot_key + +with SchemaRegistry("private-registry.sqlite") as registry: + schema = registry.get_simplex("schema:example") + matches = registry.search_roles("group") + containers = registry.find_by_roles(["role:group"], match_all=True) + candidates = registry.find_solvable([ + slot_key("schema:example", "left"), + slot_key("schema:example", "right"), + slot_key("schema:example", "map"), + slot_key("schema:example", "bijective"), + ]) +``` + +`find_by_roles` searches definition references, including descendants of nested schemas. +`find_solvable` retains the archived API name but implements **structural readiness only**: +all input occurrences must be supplied and at least one marked goal/own occurrence must +remain unresolved. It returns `structural_candidate_only: true`, not a proof or a computed value. +Having one `role:group` definition cannot satisfy two distinct group slots. A nested input +must itself be explicitly supplied; the registry does not apply its internal theorem automatically. + +`SimplexInstance(schema, facts=..., goals=...)` binds local aliases. Facts and goals must be +distinct declared slots. Omitting `goals` uses roles marked `goal` or `own`; `resolve` checks +a supplied goal value against choices. Completion means that declared goals have values, +not that Lean verified them. Value unification, dependent type checking and proof search +remain outside this implementation. + +## Materialization of the 65 P0 items + +The builder consumes the frozen current-chat GPT diagnostic's source descriptions and +unchanged Lean strings. It makes no model request, revises no assessment and performs no +Lean compilation. Results: + +| Artifact | Count | +|---|---:| +| Source annotation seed schemas | 65 | +| Lean signature schema seeds | 50 | +| Items with fewer than two projected Lean roles | 15 | +| Stored schemas | 115 | +| Scoped role records / slot occurrences | 483 / 483 | + +These 115 seeds deliberately do not auto-reuse definitions across statements. Explicit reuse +is supported and tested by the synthetic example; a reviewed shared ontology is future work. +The 15 incomplete Lean sides remain in the index with status `insufficient_projected_roles`. +A closed declaration may mention concrete objects inside its conclusion that the binder-based +projector misses. No object roles were invented to hide this limitation. + +Source schemas are marked `unreviewed_annotation_seed`. Existing `given` tags are preserved +with `quantifier_status: unreviewed`; they are not silently converted to universal/existential +quantifiers. References on the source side use explicit symbol candidates; Lean references +are syntactic identifier candidates. Neither is a complete dependency analysis. +For example, P11's source seed lists a named size while Lean uses `Fintype.card G` inline. +The materializer preserves both representations; it does not invent a validated cardinality +binding or repair the old alignment result. Annotation quality and semantic normalization +still require a separate review. + +Private outputs under `experiments/P0-pilot/data/simplex-schemas-v1/`: + +- `registry.sqlite`: queryable catalog with the 115 schemas and scoped slots. +- `schemas.json`: all 65 source/Lean pairs, retaining incomplete Lean projections. +- `schemas.html`: a local review of all 65 pairs. +- `schema-inputs.json`: input hashes; an existing directory rejects changed inputs. + +Tracked, text-free outputs: + +- `experiments/P0-pilot/results/simplex-schema-index.json`: 65 item IDs, schema keys, + role counts, coverage status and reference-candidate counts. +- `experiments/P0-pilot/results/simplex-schema-summary.json`: coverage, limitations and hashes. + +Replay from the repository root with private inputs present: + +```sh +PYTHONPATH=. python3 experiments/P0-pilot/build_schemas.py \ + --items experiments/P0-pilot/data/simplex-schemas-v1/items.jsonl \ + --assessments experiments/P0-pilot/data/simplex-schemas-v1/assistant-assessments.json \ + --key experiments/P0-pilot/labels/key.json \ + --private-out experiments/P0-pilot/data/simplex-schemas-v1 \ + --index experiments/P0-pilot/results/simplex-schema-index.json \ + --summary experiments/P0-pilot/results/simplex-schema-summary.json +``` + +The original annotations, judgments, Qwen results and matcher thresholds remain unchanged. +The registry is a usable schema foundation, not evidence of a validated theorem, a working +prover, independently measured faithfulness, or a completed Phase 1 experiment. diff --git a/examples/simplex_registry.py b/examples/simplex_registry.py new file mode 100644 index 0000000..5646758 --- /dev/null +++ b/examples/simplex_registry.py @@ -0,0 +1,35 @@ +"""Synthetic example: one isomorphism schema relates two groups and a map.""" +from __future__ import annotations + +import json + +from leanbench.schema import KIND_FACT, KIND_GOAL, Role, Simplex, SimplexInstance +from leanbench.schema_registry import SchemaRegistry, slot_key + + +def example(): + group = Role("group", type_text="group carrier", context="Reusable group role definition") + schema = Simplex("group_isomorphism", { + "left": group, + "right": group, + "map": Role("homomorphism", type_text="left →* right", + attrs={"references": ["left", "right"]}), + "bijective": Role("bijective", KIND_FACT, type_text="Bijective map", + attrs={"references": ["map"]}), + "goal": Role("isomorphic", KIND_GOAL, type_text="Nonempty (left ≃* right)", + attrs={"references": ["left", "right"]}), + }, context="A bijective homomorphism supplies a group isomorphism") + with SchemaRegistry() as registry: + registry.set_role(group, "role:group") + key = registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"}) + instance = SimplexInstance(schema, facts={ + "left": "group A", "right": "group B", "map": "f", "bijective": "supplied evidence"}) + candidates = registry.find_solvable([slot_key(key, alias) for alias in instance.facts]) + return {"schema": registry.get_simplex(key).as_dict(), "definition_keys": registry.slots(key), + "bindings": {alias: fact.value for alias, fact in instance.facts.items()}, + "structural_candidates": candidates, "completed": instance.is_completed(), + "note": "Evidence is symbolic user input; this example does not run a Lean proof."} + + +if __name__ == "__main__": + print(json.dumps(example(), indent=2, ensure_ascii=False)) diff --git a/experiments/P0-pilot/README.md b/experiments/P0-pilot/README.md index 58ab084..adfb31b 100644 --- a/experiments/P0-pilot/README.md +++ b/experiments/P0-pilot/README.md @@ -65,3 +65,13 @@ See `docs/experiments/P0-gpt-diagnostic.md` for all counts, limitations, artifac and the offline replay command. The tracked `results/gpt-diagnostic-*.json` files contain only categorical/numeric outputs and audit metadata. The authored source structures, reasons and full review page stay in the ignored `data/gpt-diagnostic/` directory. + +## Semantic simplex registry + +The current 65-item annotation cohort is materialized as multi-role relation schemas: +65 source seeds, 50 Lean signature seeds and 15 explicitly incomplete Lean projections. +See `docs/simplex-schema.md` for the data model, scoped identities, explicit role reuse, +structural candidate queries, bindings and replay command. Private SQLite/JSON/HTML outputs +stay under `data/simplex-schemas-v1/`; tracked `results/simplex-schema-*.json` files contain +only counts, opaque keys, provenance hashes and coverage status. This does not change the +frozen diagnostic or claim complete semantic extraction or proof verification. diff --git a/experiments/P0-pilot/build_schemas.py b/experiments/P0-pilot/build_schemas.py new file mode 100644 index 0000000..5f7ac11 --- /dev/null +++ b/experiments/P0-pilot/build_schemas.py @@ -0,0 +1,185 @@ +"""Materialize scoped multi-role relation schemas from the frozen 65-item review. + +The schema is the relation joining its slots. No geometric faces, inferred proof +links or cross-theorem object identities are constructed. +""" +from __future__ import annotations + +import argparse +import hashlib +import html +import json +import re +from collections import Counter +from pathlib import Path + +from leanbench.project import project +from leanbench.schema import KIND_OBJECT, Role, Simplex, role_from_dict +from leanbench.schema_registry import SchemaRegistry, slot_key +from leanbench.srcsimplex import parse_source_simplex + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def source_schema(name, payload): + source = parse_source_simplex(payload) + symbol_slots = {} + for role in source.roles: + if role.kind == KIND_OBJECT: + for symbol in role.symbols: + symbol_slots.setdefault(symbol, []).append(role.alias) + roles = {} + for role in source.roles: + references = sorted({alias for symbol in role.symbols for alias in symbol_slots.get(symbol, []) + if alias != role.alias and len(symbol_slots[symbol]) == 1}) + roles[role.alias] = Role( + role.symbols[0] if len(role.symbols) == 1 else role.alias, + role.kind, context=role.description, + attrs={"symbols": role.symbols, "keywords": role.keywords, + "introduced": role.introduced, "quantifier_status": "unreviewed", + "references": references, + "reference_status": "explicit_symbol_candidates" if references else "unknown", + "origin": "frozen_current_chat_annotation"}) + return Simplex(name, roles, attrs={"side": "source", "goal_has_exists": source.goal_has_exists, + "reference_completeness": "partial"}) + + +def lean_schema(name, code): + projection = project(code) + if projection.simplex is None: + return None, projection + originals = projection.simplex.roles + by_name = {} + for alias, role in originals.items(): + by_name.setdefault(role.name, []).append(alias) + roles = {} + for alias, role in originals.items(): + identifiers = set(re.findall(r"[^\W\d]\w*'?", role.type_text, flags=re.UNICODE)) + references = sorted({target for symbol in identifiers for target in by_name.get(symbol, []) + if len(by_name[symbol]) == 1 and target != alias}) + roles[alias] = Role(role.name, role.kind, type_text=role.type_text, context=role.context, + choices=role.choices, attrs={**role.attrs, "references": references, + "reference_status": "syntactic_candidates", + "origin": "deterministic_signature_projection"}) + return Simplex(name, roles, attrs={"side": "lean", "reference_completeness": "syntactic_only"}), projection + + +def build(items, assessment, key, registry, namespace="p0-v1"): + by_id = {item["id"]: item for item in items} + records = {row["blind_id"]: row for row in assessment["records"]} + if (not key or len(by_id) != len(items) or len(records) != len(assessment["records"]) + or len(set(key.values())) != len(key) or set(by_id) != set(key.values()) + or set(records) != set(key)): + raise ValueError("Items, assessments and blind key must match exactly once") + index, snapshots = [], [] + for blind, item_id in key.items(): + record = records[blind] + if record["id"] != item_id: + raise ValueError("Assessment identity mismatch") + source_key = f"schema:{namespace}:{item_id}:source:v1" + lean_key = f"schema:{namespace}:{item_id}:lean:v1" + source = source_schema(source_key, record["source"]) + lean, projection = lean_schema(lean_key, by_id[item_id]["lean_code"]) + registry.set_simplex(source, source_key) + if lean is not None: + registry.set_simplex(lean, lean_key) + source_restored = registry.get_simplex(source_key) + if source_restored.as_dict() != source.as_dict(): + raise ValueError("Source schema persistence roundtrip failed") + if lean is not None and registry.get_simplex(lean_key).as_dict() != lean.as_dict(): + raise ValueError("Lean schema persistence roundtrip failed") + index.append({"blind_id": blind, "source_schema": source_key, + "source_status": "unreviewed_annotation_seed", + "source_slots": len(source.roles), + "lean_schema": lean_key if lean is not None else None, + "lean_slots": len(projection.roles), + "lean_status": "materialized" if lean is not None else "insufficient_projected_roles", + "source_role_counts": dict(Counter(r.kind for r in source.roles.values())), + "lean_role_counts": dict(Counter(r.kind for r in projection.roles)), + "source_slots_with_reference_candidates": sum(bool(r.attrs["references"]) for r in source.roles.values())}) + snapshots.append({"blind_id": blind, "source": source.as_dict(), + "lean": lean.as_dict() if lean is not None else None, + "lean_projection": projection.as_dict(), + "source_slot_keys": [slot_key(source_key, alias) for alias in source.roles]}) + return index, snapshots + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--items", required=True, type=Path) + parser.add_argument("--assessments", required=True, type=Path) + parser.add_argument("--key", required=True, type=Path) + parser.add_argument("--private-out", required=True, type=Path) + parser.add_argument("--index", required=True, type=Path) + parser.add_argument("--summary", required=True, type=Path) + args = parser.parse_args() + if "data" not in args.private_out.parts: + parser.error("Private schemas must remain in the gitignored data/ directory") + assessment = json.loads(args.assessments.read_text()) + key = json.loads(args.key.read_text())["key"] + if (assessment["provenance"]["items_sha256"] != digest(args.items) + or assessment["provenance"]["key_sha256"] != digest(args.key)): + parser.error("Frozen assessment hashes do not match inputs/key") + items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()] + args.private_out.mkdir(parents=True, exist_ok=True) + identity = {"items": digest(args.items), "assessments": digest(args.assessments), + "key": digest(args.key)} + manifest = args.private_out / "schema-inputs.json" + if manifest.exists() and json.loads(manifest.read_text()) != identity: + parser.error("Existing schema output belongs to different inputs; choose a new directory") + temporary = args.private_out / "registry.sqlite.tmp" + if temporary.exists(): + temporary.unlink() + with SchemaRegistry(temporary) as registry: + index, snapshots = build(items, assessment, key, registry, + namespace=f"p0-{identity['assessments'][:12]}") + info = registry.info() + temporary.replace(args.private_out / "registry.sqlite") + manifest.write_text(json.dumps(identity, indent=2) + "\n") + (args.private_out / "schemas.json").write_text(json.dumps(snapshots, indent=2, ensure_ascii=False) + "\n") + sections = [] + for row in snapshots: + sides = [] + for side in ["source", "lean"]: + value = row[side] + content = (json.dumps(value, indent=2, ensure_ascii=False) if value is not None + else "Insufficient projected roles; no object roles were invented.") + sides.append(f'

{side}

{html.escape(content)}
') + sections.append(f'

{row["blind_id"]}

' + + ''.join(sides) + '
') + (args.private_out / "schemas.html").write_text( + 'P0 semantic simplex schemas' + '' + '

65 semantic multi-role relation schemas

' + '

Private annotation seeds, not independently validated mathematical statements. ' + 'A simplex joins the objects, assumptions and conclusion in its slots. ' + 'References are partial symbol/syntax candidates.

' + ''.join(sections) + '') + # JSON-only reload is independently checked; it does not use pickle. + for row in snapshots: + for side in ["source", "lean"]: + if row[side] is not None: + if role_from_dict(row[side]).as_dict() != row[side]: + raise ValueError("JSON schema roundtrip failed") + summary = {"representation": "semantic_multi_role_relation_schema_v1", "items": len(items), + "source_schemas": len(index), "lean_schemas": sum(r["lean_schema"] is not None for r in index), + "lean_incomplete": sum(r["lean_schema"] is None for r in index), "registry": info, + "hashes": {"items": digest(args.items), "assessments": digest(args.assessments), + "key": digest(args.key), "builder": digest(Path(__file__)), + "schema_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema.py"), + "registry_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema_registry.py")}, + "limitations": ["Source annotations come from a non-independent current-chat diagnostic.", + "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.", + "References are symbol/syntax candidates, not complete semantic dependencies.", + "No cross-theorem identity or proof dependency is inferred.", + "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent."]} + for path, value in [(args.index, index), (args.summary, summary)]: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n") + print(json.dumps({k: summary[k] for k in ["items", "source_schemas", "lean_schemas", "lean_incomplete", "registry"]})) + + +if __name__ == "__main__": + main() diff --git a/experiments/P0-pilot/results/simplex-schema-index.json b/experiments/P0-pilot/results/simplex-schema-index.json new file mode 100644 index 0000000..eaf6724 --- /dev/null +++ b/experiments/P0-pilot/results/simplex-schema-index.json @@ -0,0 +1,1210 @@ +[ + { + "blind_id": "P01", + "source_schema": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P02", + "source_schema": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P03", + "source_schema": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P04", + "source_schema": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P05", + "source_schema": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "own": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P06", + "source_schema": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P07", + "source_schema": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:lean:v1", + "lean_slots": 7, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P08", + "source_schema": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P09", + "source_schema": "schema:p0-f12735802ba0:8b39fc5b656bac00bc1e863f:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 8, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 7, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P10", + "source_schema": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P11", + "source_schema": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P12", + "source_schema": "schema:p0-f12735802ba0:e3d40d93cda13ec59c35d9a5:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P13", + "source_schema": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P14", + "source_schema": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P15", + "source_schema": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P16", + "source_schema": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 8, + "lean_schema": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P17", + "source_schema": "schema:p0-f12735802ba0:a7396b1a5d5ebcd5b48ea7ba:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 5, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P18", + "source_schema": "schema:p0-f12735802ba0:59bb865c9bdfb8521e414743:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P19", + "source_schema": "schema:p0-f12735802ba0:283d407566264b02fbee6560:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:283d407566264b02fbee6560:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P20", + "source_schema": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P21", + "source_schema": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P22", + "source_schema": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P23", + "source_schema": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 9, + "lean_schema": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:lean:v1", + "lean_slots": 11, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 5, + "fact": 5, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P24", + "source_schema": "schema:p0-f12735802ba0:437d02fe69d580bde075648c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P25", + "source_schema": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:lean:v1", + "lean_slots": 6, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P26", + "source_schema": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:lean:v1", + "lean_slots": 7, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P27", + "source_schema": "schema:p0-f12735802ba0:8d4d64143a8b214e38d7ba1b:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P28", + "source_schema": "schema:p0-f12735802ba0:6017927fdafd91ca22ed6ade:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P29", + "source_schema": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 7, + "lean_schema": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P30", + "source_schema": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 9, + "lean_schema": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:lean:v1", + "lean_slots": 8, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "fact": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 4, + "fact": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 4 + }, + { + "blind_id": "P31", + "source_schema": "schema:p0-f12735802ba0:9091f6a277215174e821d373:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": "schema:p0-f12735802ba0:9091f6a277215174e821d373:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P32", + "source_schema": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P33", + "source_schema": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P34", + "source_schema": "schema:p0-f12735802ba0:534c6ffcf56931559e70657b:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P35", + "source_schema": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P36", + "source_schema": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P37", + "source_schema": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P38", + "source_schema": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P39", + "source_schema": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P40", + "source_schema": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 4, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P41", + "source_schema": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P42", + "source_schema": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P43", + "source_schema": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P44", + "source_schema": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P45", + "source_schema": "schema:p0-f12735802ba0:3c00c37b39285cbd7d0be732:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P46", + "source_schema": "schema:p0-f12735802ba0:186d922a4121917ac8643316:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P47", + "source_schema": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P48", + "source_schema": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:lean:v1", + "lean_slots": 5, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P49", + "source_schema": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P50", + "source_schema": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P51", + "source_schema": "schema:p0-f12735802ba0:25af34567cb2040bf41869e5:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P52", + "source_schema": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P53", + "source_schema": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 2, + "lean_schema": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:lean:v1", + "lean_slots": 2, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "own": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P54", + "source_schema": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P55", + "source_schema": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P56", + "source_schema": "schema:p0-f12735802ba0:bcdfa01447e7060e1fd3d935:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P57", + "source_schema": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P58", + "source_schema": "schema:p0-f12735802ba0:89fe687db9136379cd276fff:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + }, + { + "blind_id": "P59", + "source_schema": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 4, + "lean_schema": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P60", + "source_schema": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 5, + "lean_schema": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:lean:v1", + "lean_slots": 3, + "lean_status": "materialized", + "source_role_counts": { + "object": 2, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P61", + "source_schema": "schema:p0-f12735802ba0:a892779bfcaca35b91e7d611:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "fact": 3, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 3 + }, + { + "blind_id": "P62", + "source_schema": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:lean:v1", + "lean_slots": 4, + "lean_status": "materialized", + "source_role_counts": { + "object": 1, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 2, + "fact": 1, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P63", + "source_schema": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 6, + "lean_schema": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:lean:v1", + "lean_slots": 6, + "lean_status": "materialized", + "source_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "lean_role_counts": { + "object": 3, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 2 + }, + { + "blind_id": "P64", + "source_schema": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 7, + "lean_schema": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:lean:v1", + "lean_slots": 9, + "lean_status": "materialized", + "source_role_counts": { + "object": 5, + "fact": 1, + "goal": 1 + }, + "lean_role_counts": { + "object": 6, + "fact": 2, + "goal": 1 + }, + "source_slots_with_reference_candidates": 1 + }, + { + "blind_id": "P65", + "source_schema": "schema:p0-f12735802ba0:f8d2e206681972927560be2c:source:v1", + "source_status": "unreviewed_annotation_seed", + "source_slots": 3, + "lean_schema": null, + "lean_slots": 1, + "lean_status": "insufficient_projected_roles", + "source_role_counts": { + "object": 2, + "goal": 1 + }, + "lean_role_counts": { + "goal": 1 + }, + "source_slots_with_reference_candidates": 0 + } +] diff --git a/experiments/P0-pilot/results/simplex-schema-summary.json b/experiments/P0-pilot/results/simplex-schema-summary.json new file mode 100644 index 0000000..e63ef98 --- /dev/null +++ b/experiments/P0-pilot/results/simplex-schema-summary.json @@ -0,0 +1,27 @@ +{ + "representation": "semantic_multi_role_relation_schema_v1", + "items": 65, + "source_schemas": 65, + "lean_schemas": 50, + "lean_incomplete": 15, + "registry": { + "roles": 483, + "simplices": 115, + "slots": 483 + }, + "hashes": { + "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272", + "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", + "builder": "3c8a7112f2d86737b646fbc9abfe5e9b8660efabc1023f2cc3357398445675e9", + "schema_module": "958b81e89c0befeb32d24036c130f2b37bd2e881bd5b009acf873cbcdada50ae", + "registry_module": "7b434b1eb178f597d4f60591a5ab74eff0c96a40fa751cb0ba75589b52e56271" + }, + "limitations": [ + "Source annotations come from a non-independent current-chat diagnostic.", + "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.", + "References are symbol/syntax candidates, not complete semantic dependencies.", + "No cross-theorem identity or proof dependency is inferred.", + "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent." + ] +} diff --git a/leanbench/schema.py b/leanbench/schema.py index b59f667..b81b5a7 100644 --- a/leanbench/schema.py +++ b/leanbench/schema.py @@ -1,4 +1,4 @@ -"""Roles and simplices: the parameters of a declaration as a small typed schema. +"""Semantic multi-role relation schemas, not geometric simplices. A Lean declaration is a bundle of roles: the objects it is about (``(G : Type*)``), the facts it assumes (``(h : a ∣ b)``), and the goal it asserts or the thing it @@ -8,8 +8,8 @@ be read off the prose of a book, so the two can be compared role by role. Design notes (from the archived ``schema-simplex`` prototype): * a role may be *constrained* to a closed set of allowed values (``choices``); -* a simplex is itself a role, so simplices nest (a lemma used by another is a role - of it), which is how a dependency structure appears; +* a simplex is itself a role, so explicitly supplied schemas can be composed; + nesting does not discover a proof dependency; * validation lives in ``__init__``. The prototype put it in a dataclass ``__post_init__`` next to a hand-written ``__init__``, where it never ran. """ @@ -41,7 +41,7 @@ class Role: choices: Sequence[Any] | None = None, attrs: dict[str, Any] | None = None, ) -> None: - if not name: + if not isinstance(name, str) or not name.strip(): raise ValueError("a role needs a name") if kind not in KINDS: raise ValueError(f"unknown role kind {kind!r}; expected one of {KINDS}") @@ -49,6 +49,8 @@ class Role: self.kind = kind self.type_text = type_text self.context = context + if isinstance(choices, (str, bytes)): + raise ValueError("choices must be a value sequence, not a string") self.choices: list[Any] | None = list(choices) if choices is not None else None self.attrs: dict[str, Any] = dict(attrs or {}) @@ -83,12 +85,21 @@ class Role: class Simplex(Role): """A reusable bundle of at least two roles, keyed by alias. Itself a role.""" - def __init__(self, name: str, roles: dict[str, Role], *, context: str = "") -> None: - super().__init__(name, KIND_SIMPLEX, context=context) + def __init__(self, name: str, roles: dict[str, Role], *, context: str = "", + attrs: dict[str, Any] | None = None) -> None: + super().__init__(name, KIND_SIMPLEX, context=context, attrs=attrs) if len(roles) < MIN_ROLES: raise ValueError( f"simplex {name!r} needs at least {MIN_ROLES} roles, got {len(roles)}" ) + if any(not isinstance(alias, str) or not alias or not isinstance(role, Role) + for alias, role in roles.items()): + raise ValueError("simplex slots need nonempty aliases and Role values") + for role in roles.values(): + references = role.attrs.get("references", []) + if (not isinstance(references, list) + or any(not isinstance(alias, str) or alias not in roles for alias in references)): + raise ValueError("role references must name slots in this simplex") self.roles = dict(roles) def by_kind(self, kind: str) -> list[Role]: @@ -105,16 +116,16 @@ class Simplex(Role): return out def as_dict(self) -> dict[str, Any]: - return { - "name": self.name, - "roles": {alias: role.as_dict() for alias, role in self.roles.items()}, - } + return {**super().as_dict(), + "roles": {alias: role.as_dict() for alias, role in self.roles.items()}} class State: """A role together with a value; unresolved until it has one.""" def __init__(self, role: Role, value: Any = None) -> None: + if value is not None: + role.check_value(value) self.role = role self.value = value @@ -133,3 +144,41 @@ class Fact(State): class Goal(State): """To be resolved.""" + + +def role_from_dict(data: dict[str, Any]) -> Role: + """Restore JSON role/schema data without executing code or loading pickle.""" + kind = data.get("kind", KIND_SIMPLEX if "roles" in data else KIND_OBJECT) + if kind == KIND_SIMPLEX: + return Simplex(data["name"], {alias: role_from_dict(role) + for alias, role in data["roles"].items()}, + context=data.get("context", ""), attrs=data.get("attrs")) + return Role(data["name"], kind, type_text=data.get("type", ""), + context=data.get("context", ""), choices=data.get("choices"), + attrs=data.get("attrs")) + + +class SimplexInstance: + """Values bind local slot aliases; a resolved goal is supplied, not proved here.""" + + def __init__(self, schema: Simplex, facts: dict[str, Any] | None = None, + goals: Sequence[str] | None = None) -> None: + self.schema = schema + facts = facts or {} + goal_aliases = list(goals) if goals is not None else [ + alias for alias, role in schema.roles.items() if role.kind in (KIND_GOAL, KIND_OWN)] + if (len(set(goal_aliases)) != len(goal_aliases) + or not (set(facts) | set(goal_aliases)) <= set(schema.roles) + or set(facts) & set(goal_aliases)): + raise ValueError("facts/goals need distinct, declared slot aliases") + self.facts = {alias: Fact(schema.roles[alias], value) for alias, value in facts.items()} + self.goals = {alias: Goal(schema.roles[alias]) for alias in goal_aliases} + + def resolve(self, alias: str, value: Any) -> None: + if alias not in self.goals or value is None: + raise ValueError("resolve needs a declared goal and a non-None value") + self.goals[alias].role.check_value(value) + self.goals[alias].value = value + + def is_completed(self) -> bool: + return bool(self.goals) and all(goal.is_resolved() for goal in self.goals.values()) diff --git a/leanbench/schema_registry.py b/leanbench/schema_registry.py new file mode 100644 index 0000000..77e173c --- /dev/null +++ b/leanbench/schema_registry.py @@ -0,0 +1,208 @@ +"""JSON/SQLite registry of semantic relation schemas and scoped slot occurrences. + +A role definition may be reused deliberately. Occurrences remain local to a +simplex: sharing a role definition never equates the objects bound to its aliases. +""" +from __future__ import annotations + +import fnmatch +import json +import sqlite3 +from collections.abc import Iterable, Mapping +from pathlib import Path +from urllib.parse import quote + +from .schema import KIND_GOAL, KIND_OWN, KIND_SIMPLEX, Role, Simplex, role_from_dict + + +def slot_key(parent: str, alias: str) -> str: + """An occurrence identity, distinct even when two slots reuse one definition.""" + return f"{parent}/slot/{quote(alias, safe='')}" + + +class SchemaRegistry: + """Immutable versioned records; reusing a key with changed content is rejected.""" + + def __init__(self, path: str | Path = ":memory:") -> None: + self.connection = sqlite3.connect(str(path)) + self.connection.execute("PRAGMA foreign_keys = ON") + self.connection.executescript(""" + CREATE TABLE IF NOT EXISTS schema_nodes ( + key TEXT PRIMARY KEY, + kind TEXT NOT NULL CHECK(kind IN ('role', 'simplex')), + payload TEXT NOT NULL + ); + CREATE TABLE IF NOT EXISTS schema_slots ( + parent TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE CASCADE, + alias TEXT NOT NULL, + child TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE RESTRICT, + position INTEGER NOT NULL, + PRIMARY KEY(parent, alias), + UNIQUE(parent, position) + ); + CREATE INDEX IF NOT EXISTS schema_slots_child ON schema_slots(child); + """) + + def __enter__(self): + return self + + def __exit__(self, *_): + self.close() + + def close(self) -> None: + self.connection.close() + + def _insert(self, key: str, kind: str, payload: dict) -> None: + if not isinstance(key, str) or not key: + raise ValueError("a registry key must be nonempty") + if (kind == "simplex") != (payload.get("kind") == KIND_SIMPLEX): + raise ValueError("nested simplex roles must use a Simplex object") + encoded = json.dumps(payload, sort_keys=True, ensure_ascii=False, allow_nan=False) + existing = self.connection.execute( + "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if existing is not None and existing != (kind, encoded): + raise ValueError(f"key {key!r} already has different content; use a new version key") + self.connection.execute("INSERT OR IGNORE INTO schema_nodes VALUES (?, ?, ?)", + (key, kind, encoded)) + + def set_role(self, role: Role, key: str | None = None) -> str: + if isinstance(role, Simplex): + raise ValueError("use set_simplex for nested schemas") + key = key or f"role:{role.name}" + with self.connection: + self._insert(key, "role", role.as_dict()) + return key + + def set_simplex(self, simplex: Simplex, key: str | None = None, + role_keys: Mapping[str, str] | None = None) -> str: + """Default children are scoped. role_keys explicitly opts into definition reuse.""" + key = key or f"schema:{simplex.name}" + role_keys = dict(role_keys or {}) + if not set(role_keys) <= set(simplex.roles): + raise ValueError("reuse map has an unknown alias") + with self.connection: + self._put_simplex(simplex, key, role_keys, set()) + return key + + def _put_simplex(self, simplex: Simplex, key: str, reuse: dict[str, str], + active: set[int]) -> None: + if id(simplex) in active: + raise ValueError("cyclic simplex nesting") + active = active | {id(simplex)} + # Metadata only; children live in a relational slot table, not pickle blobs. + payload = Role.as_dict(simplex) + existing = self.connection.execute( + "SELECT key FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if existing: + restored = self.get_simplex(key) + if restored is None or restored.as_dict() != simplex.as_dict(): + raise ValueError(f"key {key!r} already has different content; use a new version key") + expected = {alias: reuse.get(alias, slot_key(key, alias)) for alias in simplex.roles} + if self.slots(key) != expected: + raise ValueError("same schema key cannot change its role-definition references") + return + self._insert(key, "simplex", payload) + for position, (alias, child) in enumerate(simplex.roles.items()): + child_key = reuse.get(alias, slot_key(key, alias)) + if alias in reuse: + restored = self.get(child_key) + if restored is None or restored.as_dict() != child.as_dict(): + raise ValueError(f"reused role definition does not match slot {alias!r}") + elif isinstance(child, Simplex): + self._put_simplex(child, child_key, {}, active) + else: + self._insert(child_key, "role", child.as_dict()) + self.connection.execute("INSERT INTO schema_slots VALUES (?, ?, ?, ?)", + (key, alias, child_key, position)) + + def get(self, key: str) -> Role | None: + return self._get(key, set()) + + def _get(self, key: str, active: set[str]) -> Role | None: + if key in active: + raise ValueError("cyclic schema references in registry") + row = self.connection.execute( + "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone() + if row is None: + return None + kind, encoded = row + payload = json.loads(encoded) + if kind == "role": + return role_from_dict(payload) + slots = self.slots(key) + children = {alias: self._get(child, active | {key}) for alias, child in slots.items()} + return Simplex(payload["name"], children, context=payload.get("context", ""), + attrs=payload.get("attrs")) + + def get_role(self, key: str) -> Role | None: + value = self.get(key) + return value if not isinstance(value, Simplex) else None + + def get_simplex(self, key: str) -> Simplex | None: + value = self.get(key) + return value if isinstance(value, Simplex) else None + + def slots(self, key: str) -> dict[str, str]: + return dict(self.connection.execute( + "SELECT alias, child FROM schema_slots WHERE parent = ? ORDER BY position", (key,))) + + def keys(self, pattern: str = "*") -> list[str]: + return [key for (key,) in self.connection.execute("SELECT key FROM schema_nodes ORDER BY key") + if fnmatch.fnmatchcase(key, pattern)] + + def search_roles(self, query: str, limit: int = 10) -> list[dict]: + """Literal substring candidates; search does not authorize semantic reuse.""" + if not query.strip() or limit < 1: + return [] + found = [] + for key, payload in self.connection.execute( + "SELECT key, payload FROM schema_nodes WHERE kind = 'role' ORDER BY key"): + if query.casefold() in (key + payload).casefold(): + found.append({"key": key, "role": json.loads(payload)}) + if len(found) == limit: + break + return found + + def find_by_roles(self, role_keys: Iterable[str], match_all: bool = False) -> list[str]: + """Find schema keys containing definition keys, including nested descendants.""" + wanted = set(role_keys) + if not wanted: + return [] + found = [] + for key in self._simplex_keys(): + descendants = {row[0] for row in self.connection.execute(""" + WITH RECURSIVE descendants(child) AS ( + SELECT child FROM schema_slots WHERE parent = ? + UNION + SELECT slots.child FROM schema_slots slots JOIN descendants d ON slots.parent = d.child + ) SELECT child FROM descendants + """, (key,))} + matches = wanted <= descendants if match_all else bool(wanted & descendants) + if matches: + found.append(key) + return found + + def find_solvable(self, known_slots: Iterable[str]) -> list[dict]: + """Structural readiness by scoped occurrences, not proof or value unification.""" + known = set(known_slots) + candidates = [] + for key in self._simplex_keys(): + schema = self.get_simplex(key) + inputs, outputs = [], [] + for alias, role in schema.roles.items(): + target = outputs if role.kind in (KIND_GOAL, KIND_OWN) else inputs + target.append(slot_key(key, alias)) + missing_outputs = [output for output in outputs if output not in known] + if missing_outputs and set(inputs) <= known: + candidates.append({"schema_key": key, "input_slots": inputs, + "target_slots": missing_outputs, "structural_candidate_only": True}) + return candidates + + def _simplex_keys(self) -> list[str]: + return [row[0] for row in self.connection.execute( + "SELECT key FROM schema_nodes WHERE kind = 'simplex' ORDER BY key")] + + def info(self) -> dict[str, int]: + counts = dict(self.connection.execute("SELECT kind, count(*) FROM schema_nodes GROUP BY kind")) + return {"roles": counts.get("role", 0), "simplices": counts.get("simplex", 0), + "slots": self.connection.execute("SELECT count(*) FROM schema_slots").fetchone()[0]} diff --git a/tests/test_schema_registry.py b/tests/test_schema_registry.py new file mode 100644 index 0000000..51d38ce --- /dev/null +++ b/tests/test_schema_registry.py @@ -0,0 +1,162 @@ +"""Semantic role definitions, scoped occurrences and structural candidate retrieval.""" +import json + +import pytest + +from leanbench.schema import ( + KIND_FACT, + KIND_GOAL, + Fact, + Role, + Simplex, + SimplexInstance, + role_from_dict, +) +from leanbench.schema_registry import SchemaRegistry, slot_key + + +def theorem(name="t"): + return Simplex(name, {"G": Role("group", context="A group carrier"), + "g": Role("element", type_text="G", attrs={"references": ["G"]}), + "finite": Role("finite", KIND_FACT, type_text="Finite G", + attrs={"references": ["G"]}), + "goal": Role("claim", KIND_GOAL, type_text="P G g", + attrs={"references": ["G", "g"]})}, + context="A multi-object claim", attrs={"provenance": "synthetic"}) + + +def test_json_roundtrip_keeps_metadata_and_nesting(): + outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)}, + context="Composed relation", attrs={"version": 1}) + encoded = json.loads(json.dumps(outer.as_dict())) + restored = role_from_dict(encoded) + assert restored.as_dict() == outer.as_dict() + assert restored.roles["lemma"].roles["g"].attrs["references"] == ["G"] + + +def test_registry_persists_nested_schemas_in_one_transaction(tmp_path): + path = tmp_path / "registry.sqlite" + outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)}) + with SchemaRegistry(path) as registry: + registry.set_simplex(outer) + registry.set_simplex(outer) + assert registry.info() == {"roles": 5, "simplices": 2, "slots": 6} + with SchemaRegistry(path) as registry: + assert registry.get_simplex("schema:outer").as_dict() == outer.as_dict() + leaf = slot_key(slot_key("schema:outer", "lemma"), "g") + assert registry.find_by_roles([leaf], match_all=True) == [ + "schema:outer", slot_key("schema:outer", "lemma")] + + +def test_same_names_in_different_theorems_are_scoped(): + with SchemaRegistry() as registry: + registry.set_simplex(theorem("first")) + registry.set_simplex(theorem("second")) + first_group = slot_key("schema:first", "G") + assert registry.find_by_roles([first_group]) == ["schema:first"] + assert registry.get_role(first_group).name == "group" + assert registry.slots("schema:first")["G"] != registry.slots("schema:second")["G"] + + +def test_explicit_reuse_does_not_equate_local_bindings_or_multiplicity(): + group = Role("group") + schema = Simplex("isomorphism", {"left": group, "right": group, + "goal": Role("equivalence", KIND_GOAL)}) + with SchemaRegistry() as registry: + registry.set_role(group, "role:group") + registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"}) + assert registry.slots("schema:isomorphism")["left"] == "role:group" + assert registry.find_solvable(["role:group"]) == [] + assert registry.find_solvable([slot_key("schema:isomorphism", "left")]) == [] + candidate = registry.find_solvable([slot_key("schema:isomorphism", x) for x in ["left", "right"]]) + assert candidate[0]["target_slots"] == [slot_key("schema:isomorphism", "goal")] + instance = SimplexInstance(schema, {"left": "C2", "right": "C3"}) + assert instance.facts["left"].value != instance.facts["right"].value + assert not instance.is_completed() + instance.resolve("goal", "a supplied result, not checked by the registry") + assert instance.is_completed() + + +def test_premise_is_required_and_known_goal_is_not_a_missing_target(): + with SchemaRegistry() as registry: + registry.set_simplex(theorem()) + inputs = [slot_key("schema:t", alias) for alias in ["G", "g", "finite"]] + assert registry.find_solvable(inputs[:-1]) == [] + assert registry.find_solvable(inputs)[0]["structural_candidate_only"] + assert registry.find_solvable(inputs + [slot_key("schema:t", "goal")]) == [] + + +def test_failed_write_rolls_back_every_child(): + with SchemaRegistry() as registry: + registry.set_role(Role("incompatible"), "role:shared") + before = registry.info() + with pytest.raises(ValueError, match="does not match"): + registry.set_simplex(theorem(), role_keys={"goal": "role:shared"}) + assert registry.info() == before + assert registry.get_simplex("schema:t") is None + + +def test_cyclic_nesting_is_rejected_without_partial_write(): + schema = Simplex("cycle", {"a": Role("a"), "b": Role("b")}) + schema.roles["b"] = schema + with SchemaRegistry() as registry: + with pytest.raises(ValueError, match="cyclic"): + registry.set_simplex(schema) + assert registry.info() == {"roles": 0, "simplices": 0, "slots": 0} + + +def test_keys_are_immutable_and_reuse_map_cannot_silently_change(): + with SchemaRegistry() as registry: + registry.set_role(Role("G"), "role:G") + with pytest.raises(ValueError, match="different content"): + registry.set_role(Role("H"), "role:G") + schema = theorem() + registry.set_simplex(schema) + registry.set_role(schema.roles["G"], "role:shared") + with pytest.raises(ValueError, match="cannot change"): + registry.set_simplex(schema, role_keys={"G": "role:shared"}) + assert registry.search_roles("%") == [] + assert registry.search_roles("group", limit=1)[0]["role"]["name"] == "group" + + +def test_instance_constraints_unknown_slots_and_invalid_references(): + role = Role("parity", choices=["even", "odd"]) + with pytest.raises(ValueError, match="not allowed"): + Fact(role, "prime") + schema = Simplex("pair", {"input": role, "goal": Role("result", KIND_GOAL, choices=[True])}) + instance = SimplexInstance(schema, {"input": "even"}) + with pytest.raises(ValueError, match="not allowed"): + instance.resolve("goal", False) + with pytest.raises(ValueError, match="declared"): + SimplexInstance(schema, {"unknown": "value"}) + with pytest.raises(ValueError, match="references"): + Simplex("invalid", {"x": Role("x", attrs={"references": ["missing"]}), "y": Role("y")}) + with pytest.raises(ValueError, match="name"): + Role(" ") + with pytest.raises(ValueError, match="sequence"): + Role("choice", choices="even") + with SchemaRegistry() as registry, pytest.raises(ValueError, match="Simplex object"): + registry.set_role(Role("fake", "simplex")) + + +def test_pilot_materialization_keeps_partial_lean_projection_explicit(): + import importlib.util + from pathlib import Path + + path = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/build_schemas.py" + spec = importlib.util.spec_from_file_location("build_schemas", path) + builder = importlib.util.module_from_spec(spec) + spec.loader.exec_module(builder) + items = [{"id": "closed", "lean_code": "theorem t : True := trivial"}] + assessment = {"records": [{"id": "closed", "blind_id": "P01", "source": { + "roles": [{"kind": "object", "symbols": ["G"], "description": "group"}, + {"kind": "goal", "description": "A synthetic claim"}]}}]} + with SchemaRegistry() as registry: + index, snapshots = builder.build(items, assessment, {"P01": "closed"}, registry) + assert registry.info()["simplices"] == 1 + assert index[0]["source_status"] == "unreviewed_annotation_seed" + assert index[0]["lean_schema"] is None + assert index[0]["lean_status"] == "insufficient_projected_roles" + assert snapshots[0]["lean_projection"]["roles"][0]["kind"] == "goal" + with pytest.raises(ValueError, match="exactly once"): + builder.build(items, {"records": []}, {"P01": "closed"}, registry)