allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(infra): populate prover_state and prover_instances from lean_concepts

Browse source 
3,057 theorems/lemmas → ene.prover_state (2,966 after dedup)
3,047 verified proofs → ene.prover_instances
Also fixes ON CONFLICT DO NOTHING and FK bypass for bulk load.
This commit is contained in:
allaun 2026-06-22 12:32:20 -05:00
parent b453be6d09
commit cfdc934757
1 changed files with 51 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
scripts/populate_ene_tables.py
View file

@ -288,6 +288,33 @@ def make_ingest_event_sql(event_id: str, pkg_id: str, source_uri: str,
)
def make_prover_state_sql(theorem_id: str, name: str, statement: str,
status: str = "raw", signature_hash: str = "",
dependencies: list = None) -> str:
"""Generate INSERT for ene.prover_state."""
deps = json.dumps(dependencies or [], ensure_ascii=False)
return (
f"INSERT INTO ene.prover_state "
f"(theorem_id, name, statement, formalization_status, signature_hash, dependencies) "
f"VALUES ('{esc(theorem_id)}', '{esc(name[:200])}', '{esc(statement[:2000])}', "
f"'{esc(status)}', '{esc(signature_hash)}', '{esc(deps)}') "
f"ON CONFLICT DO NOTHING;"
)
def make_prover_instance_sql(theorem_id: str, input_fixture: dict,
evaluation_witness: dict,
verifier: str = "lean4") -> str:
"""Generate INSERT for ene.prover_instances."""
return (
f"INSERT INTO ene.prover_instances "
f"(theorem_id, input_fixture, evaluation_witness, verifier_identity) "
f"VALUES ('{esc(theorem_id)}', {jsonb(input_fixture)}, "
f"{jsonb(evaluation_witness)}, '{esc(verifier)}') "
f"ON CONFLICT DO NOTHING;"
)
# ── Build SQL batches ────────────────────────────────────────────────────────
def build_sql_batches(sources: dict) -> dict:
@ -387,6 +414,25 @@ def build_sql_batches(sources: dict) -> dict:
make_gossip_node_sql(f"gsn_{cid}", cid, fold, nh, desc[:200] if desc else name, wm, gr)
)
# Prover state (all theorems and lemmas)
if ctype in ("theorem", "lemma"):
formalization_status = "verified" if lean_status == "DEFINED" else "raw"
sig_hash = hashlib.sha256((lean_name or cid).encode()).hexdigest()[:16]
deps = concept.get("related", [])[:10]
batches["prover_state"].append(
make_prover_state_sql(lean_name or cid, name, expr or desc,
formalization_status, sig_hash, deps)
)
# Prover instances (verified theorems only — those with DEFINED status)
if ctype in ("theorem",) and lean_status == "DEFINED":
fixture = {"source_file": source, "concept_id": cid, "tags": tags[:5]}
witness = {"lean_status": "DEFINED", "lean_name": lean_name,
"expression": (expr or "")[:500]}
batches["prover_instances"].append(
make_prover_instance_sql(lean_name or cid, fixture, witness)
)
# Relations from 'related' field
for rel_target in concept.get("related", []):
rel_key = f"{cid}->{rel_target}"
@ -637,7 +683,8 @@ def main():
print(" ─────────────────────────┼───────────────")
for table in ["packages", "receipts", "sidon_labels", "braid_strands",
"eigensolid_snapshots", "gossip_surface_nodes",
"gossip_surface_edges", "relations", "sessions", "ingest_events"]:
"gossip_surface_edges", "relations", "sessions",
"ingest_events", "prover_state", "prover_instances"]:
count = len(batches.get(table, []))
marker = "" if count > 0 else " (empty)"
print(f" {table:<24s} | {count}{marker}")
@ -646,7 +693,7 @@ def main():
# Skip tables
skip_tables = ["crossing_weights", "fractal_nodes", "fractal_manifolds",
"fractal_graph_entities", "vectors", "dsp_nodes",
"prover_instances", "prover_state", "nspace_kv",
"nspace_kv",
"wiki_pages", "wiki_revisions", "wiki_categories", "wiki_links", "routes"]
print(" Skipped tables (no clean mapping):")
for t in skip_tables:
@ -701,7 +748,8 @@ def main():
print("\n── Final row counts ──")
for table in ["packages", "receipts", "sidon_labels", "braid_strands",
"eigensolid_snapshots", "gossip_surface_nodes",
"gossip_surface_edges", "relations", "sessions", "ingest_events"]:
"gossip_surface_edges", "relations", "sessions",
"ingest_events", "prover_state", "prover_instances"]:
count = neon(f"SELECT COUNT(*) FROM ene.{table}")
print(f" {table}: {count}")