mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
fbb71cffc9
- Add python/build_corpus250.py generator (deterministic, uses classifier receipt + PIST matrices, computes labels via SilverSight.PIST.Classify). - Generate formal/SilverSight/RRC/Corpus250.lean with 250 FixtureRows. - Register SilverSight.RRC.Corpus250 in lakefile.lean. - Add AVMIsa.Emit.emitCorpus250 and update rrc-emit-fixture to emit it. - Regenerate PROJECT_MAP.md/json. Verification: - lake build: 2981 jobs, 0 errors - lake build SilverSightRRC: 2995 jobs, 0 errors - rrc-emit-fixture | validate_rrc_predictions.py: OK 250 rows, avm_rrc_corpus250_v1
233 lines
9.1 KiB
Python
233 lines
9.1 KiB
Python
#!/usr/bin/env python3
|
||
# /// script
|
||
# requires-python = ">=3.10"
|
||
# dependencies = []
|
||
# ///
|
||
"""
|
||
Build formal/SilverSight/RRC/Corpus250.lean from
|
||
archive/experimental-shim-probes/rrc_equation_classifier_receipt.json,
|
||
merged with 8×8 braid adjacency matrices from
|
||
shared-data/rrc_pist_predictions_250_v1.json.
|
||
|
||
Python's role:
|
||
- read raw features from the classifier receipt
|
||
- merge matrices by invariant_receipt.object_id
|
||
- emit deterministic Lean source
|
||
|
||
Lean's role:
|
||
- PIST classification (classifyProxy/classifyExact) from the matrix
|
||
- alignment gate via determineAlignment
|
||
- receipt stamping and all admissibility/promotion decisions
|
||
|
||
Usage:
|
||
python3 python/build_corpus250.py
|
||
python3 python/build_corpus250.py \
|
||
--receipt /path/to/rrc_equation_classifier_receipt.json \
|
||
--predictions /path/to/rrc_pist_predictions_250_v1.json \
|
||
--out-lean formal/SilverSight/RRC/Corpus250.lean
|
||
"""
|
||
from __future__ import annotations
|
||
import argparse, hashlib, json, sys
|
||
from pathlib import Path
|
||
|
||
|
||
# classifier JSON shape name → SilverSight.RRCLogogramProjection.RRCShape constructor
|
||
SHAPE_MAP = {
|
||
"CognitiveLoadField": ".cognitiveLoadField",
|
||
"SignalShapedRouteCompiler": ".signalShapedRouteCompiler",
|
||
"ProjectableGeometryTopology": ".projectableGeometryTopology",
|
||
"CadForceProbeReceipt": ".cadForceProbeReceipt",
|
||
"LogogramProjection": ".logogramProjection",
|
||
"HoldForUnlawfulOrUnderspecifiedShape": ".holdForUnlawfulOrUnderspecifiedShape",
|
||
}
|
||
|
||
|
||
def template_key(rrc_kind: str, status: str) -> str:
|
||
"""Map rrc_kind + classifier status to a page-generator template key."""
|
||
if status == "HOLD":
|
||
return "hold"
|
||
kind_map = {
|
||
"cognitive_field_receipt": "definition",
|
||
"compression_route_prior": "master_equation",
|
||
"geometry_topology_receipt": "definition",
|
||
"cad_force_receipt": "gate",
|
||
"logogram_projection": "receipt",
|
||
"negative_control": "hold",
|
||
}
|
||
return kind_map.get(rrc_kind, "definition")
|
||
|
||
|
||
def operator_tokens(er: dict) -> list[str]:
|
||
"""Derive operator/domain tokens from route_hint, rrc_kind, and equation text."""
|
||
tokens = []
|
||
rh = (er.get("route_hint_non_authoritative") or "").strip()
|
||
rk = (er.get("rrc_kind") or "").strip()
|
||
if rh and rh != "unclassified_equation":
|
||
tokens.append(rh)
|
||
if rk:
|
||
tokens.append(rk)
|
||
eq_text = (er.get("equation") or "").lower()
|
||
for op in ["exp(", "log(", "max(", "min(", "sum(", "integral", "derivative",
|
||
"laplacian", "nabla", "div(", "curl(", "sigmoid", "softmax",
|
||
"tanh(", "relu(", "norm(", "dot(", "cross("]:
|
||
if op in eq_text:
|
||
tokens.append(op.rstrip("("))
|
||
return list(dict.fromkeys(tokens))
|
||
|
||
|
||
def lean_str(s: str) -> str:
|
||
s = s.replace("\\", "\\\\").replace('"', '\\"')
|
||
return f'"{s}"'
|
||
|
||
|
||
def lean_opt(s: str | None) -> str:
|
||
return "none" if s is None else f"some {lean_str(s)}"
|
||
|
||
|
||
def lean_str_list(xs: list[str]) -> str:
|
||
return "[" + ", ".join(lean_str(x) for x in xs) + "]"
|
||
|
||
|
||
def load_matrices(path: Path) -> dict[str, list[list[int]]]:
|
||
"""Load predictions JSON into equation_id → matrix lookup."""
|
||
data = json.loads(path.read_text())
|
||
return {
|
||
p.get("equation_id", ""): p.get("matrix_8x8", [])
|
||
for p in data.get("predictions", [])
|
||
if p.get("equation_id")
|
||
}
|
||
|
||
|
||
def main() -> int:
|
||
parser = argparse.ArgumentParser(description="Generate SilverSight RRC Corpus250.lean")
|
||
parser.add_argument(
|
||
"--receipt",
|
||
type=Path,
|
||
default=Path("/home/allaun/Research Stack/archive/experimental-shim-probes/rrc_equation_classifier_receipt.json"),
|
||
help="Path to rrc_equation_classifier_receipt.json",
|
||
)
|
||
parser.add_argument(
|
||
"--predictions",
|
||
type=Path,
|
||
default=Path("/home/allaun/Research Stack/shared-data/rrc_pist_predictions_250_v1.json"),
|
||
help="Path to rrc_pist_predictions_250_v1.json",
|
||
)
|
||
parser.add_argument(
|
||
"--out-lean",
|
||
type=Path,
|
||
default=Path("formal/SilverSight/RRC/Corpus250.lean"),
|
||
help="Output Lean module path",
|
||
)
|
||
args = parser.parse_args()
|
||
|
||
receipt = json.loads(args.receipt.read_text())
|
||
eqs = receipt.get("compiled_equations", [])
|
||
matrices = load_matrices(args.predictions)
|
||
print(f"Loaded {len(eqs)} equations and {len(matrices)} matrices", file=sys.stderr)
|
||
|
||
# Deterministic order by equation_id.
|
||
eqs_sorted = sorted(eqs, key=lambda eq: eq.get("invariant_receipt", {}).get("object_id", ""))
|
||
|
||
# Content hash over the raw corpus data for reproducibility.
|
||
content_blob = json.dumps(
|
||
[
|
||
{
|
||
"object_id": eq.get("invariant_receipt", {}).get("object_id"),
|
||
"name": eq.get("equation_record", {}).get("name"),
|
||
"shape": eq.get("invariant_receipt", {}).get("shape"),
|
||
"status": eq.get("invariant_receipt", {}).get("status"),
|
||
"matrix": matrices.get(eq.get("invariant_receipt", {}).get("object_id", "")),
|
||
}
|
||
for eq in eqs_sorted
|
||
],
|
||
sort_keys=True,
|
||
separators=(",", ":"),
|
||
).encode("utf-8")
|
||
content_hash = hashlib.sha256(content_blob).hexdigest()
|
||
|
||
rows: list[str] = []
|
||
for eq in eqs_sorted:
|
||
er = eq["equation_record"]
|
||
ir = eq["invariant_receipt"]
|
||
tw = eq["type_witness"]
|
||
|
||
eq_id = ir.get("object_id", "")
|
||
name = er.get("name", "")
|
||
shape_str = ir.get("shape", "HoldForUnlawfulOrUnderspecifiedShape")
|
||
lean_shape = SHAPE_MAP.get(shape_str, ".holdForUnlawfulOrUnderspecifiedShape")
|
||
status_str = ir.get("status", "HOLD")
|
||
lean_status = ".candidate" if status_str == "CANDIDATE" else ".hold"
|
||
rrc_kind = er.get("rrc_kind", "")
|
||
weak_cnt = len(tw.get("missing_or_weak_axes") or [])
|
||
|
||
op_tokens = operator_tokens(er)
|
||
inv_declared = (er.get("domain_type") or "unknown").strip() or "unknown"
|
||
bound_conds = (er.get("bind_class") or "unknown").strip() or "unknown"
|
||
t_key = template_key(rrc_kind, status_str)
|
||
route_hint = er.get("route_hint_non_authoritative") or "unclassified_equation"
|
||
t_params = f"route={route_hint};shape={shape_str}"
|
||
arxiv_pid = (er.get("arxiv_paper_id") or "").strip() or None
|
||
|
||
rows.append(
|
||
f" {{ equationId := {lean_str(eq_id)}\n"
|
||
f" name := {lean_str(name)}\n"
|
||
f" shape := {lean_shape}\n"
|
||
f" status := {lean_status}\n"
|
||
f" rrcKind := {lean_str(rrc_kind)}\n"
|
||
f" weakAxesCnt := {weak_cnt}\n"
|
||
f" pistProxyLabel := Option.bind (findMatrix {lean_str(eq_id)}) SilverSight.PIST.Classify.classifyProxy\n"
|
||
f" pistExactLabel := Option.bind (findMatrix {lean_str(eq_id)}) SilverSight.PIST.Classify.classifyExact\n"
|
||
f" arxivPaperId := {lean_opt(arxiv_pid)}\n"
|
||
f" operatorTokens := {lean_str_list(op_tokens)}\n"
|
||
f" invariantsDeclared := {lean_str(inv_declared)}\n"
|
||
f" boundaryConds := {lean_str(bound_conds)}\n"
|
||
f" templateKey := {lean_str(t_key)}\n"
|
||
f" templateParams := {lean_str(t_params)} }}"
|
||
)
|
||
|
||
lines = [
|
||
"-- SilverSight.RRC.Corpus250 — AUTO-GENERATED by python/build_corpus250.py",
|
||
"-- DO NOT EDIT BY HAND. Regenerate with:",
|
||
"-- python3 python/build_corpus250.py",
|
||
"--",
|
||
"-- Python role: raw feature extraction + matrix merge.",
|
||
"-- Lean role: PIST classification, alignment gate (determineAlignment),",
|
||
"-- receipt stamping, and all admissibility/promotion decisions.",
|
||
"--",
|
||
"-- Source: rrc_equation_classifier_receipt.json",
|
||
"-- Matrices: rrc_pist_predictions_250_v1.json",
|
||
f"-- Content hash (SHA-256): {content_hash}",
|
||
f"-- Equation count: {len(rows)}",
|
||
"--",
|
||
"import SilverSight.RRC.Emit",
|
||
"import SilverSight.PIST.Classify",
|
||
"import SilverSight.PIST.Matrices250",
|
||
"",
|
||
"namespace SilverSight.RRC.Corpus250",
|
||
"",
|
||
"open SilverSight.RRC.Emit",
|
||
"open SilverSight.RRCLogogramProjection",
|
||
"open SilverSight.ReceiptCore",
|
||
"open SilverSight.PIST.Matrices250",
|
||
"",
|
||
"/-- Full 250-equation corpus from rrc_equation_classifier_receipt.json,",
|
||
" merged with 8×8 braid adjacency matrices from",
|
||
" rrc_pist_predictions_250_v1.json.",
|
||
" Each row carries raw features only; the alignment gate in",
|
||
" SilverSight.RRC.Emit.emitCorpus makes all admissibility decisions. -/",
|
||
"def corpus250 : List FixtureRow := [",
|
||
",\n".join(rows),
|
||
"]",
|
||
"",
|
||
"end SilverSight.RRC.Corpus250",
|
||
"",
|
||
]
|
||
|
||
args.out_lean.parent.mkdir(parents=True, exist_ok=True)
|
||
args.out_lean.write_text("\n".join(lines))
|
||
print(f"Wrote {args.out_lean} ({len(rows)} rows)", file=sys.stderr)
|
||
return 0
|
||
|
||
|
||
if __name__ == "__main__":
|
||
sys.exit(main())
|