feat(infra): add optional --rrc alignment to lake_build_ingest.py

When --rrc is given, the shim runs pist-classify-trace on the trace fixture
and rrc-watchdog for RRC alignment, then writes an additional
rrc_alignment receipt into ene.receipts alongside the build receipt.
This commit is contained in:
allaun 2026-06-22 03:46:58 -05:00
parent 94b04ae321
commit 5e7200c84f

View file

@ -17,12 +17,18 @@ Tables used:
ene.ingest_events provenance for the ingestion itself
Usage:
python3 4-Infrastructure/shim/lake_build_ingest.py [target] [--dir LEAN_DIR] [--actor NAME]
python3 4-Infrastructure/shim/lake_build_ingest.py [target] [--dir LEAN_DIR] [--actor NAME] [--rrc TRACE_JSON]
Examples:
python3 4-Infrastructure/shim/lake_build_ingest.py
python3 4-Infrastructure/shim/lake_build_ingest.py Compiler
python3 4-Infrastructure/shim/lake_build_ingest.py Semantics.NKHodgeFAMM --actor opencode
python3 4-Infrastructure/shim/lake_build_ingest.py Compiler --rrc Compiler.trace.json
When --rrc is given, the shim looks for <target>.trace.json (or the explicit path),
runs the canonical `pist-classify-trace` executable, then runs `rrc-watchdog` with
its predicted shape. The resulting RRC alignment receipt is stored alongside the
build receipt. Both steps are pure I/O wrappers around Lean executables.
"""
from __future__ import annotations
@ -43,6 +49,8 @@ LEAN_DIR = ROOT / "0-Core-Formalism/lean/Semantics"
NEON_HOST = "100.92.88.64"
CONTAINER = "arxiv-pg"
DB = "ene"
PIST_CLASSIFY = LEAN_DIR / ".lake" / "build" / "bin" / "pist-classify-trace"
RRC_WATCHDOG = LEAN_DIR / ".lake" / "build" / "bin" / "rrc-watchdog"
def _now() -> str:
@ -253,12 +261,176 @@ def _escape_sql(s: str) -> str:
return s.replace("'", "''").replace("\\", "\\\\")
def _find_rrc_trace(target: str, explicit_path: Path | None, lean_dir: Path) -> Path | None:
"""Resolve the RRC trace fixture path.
If an explicit path is given, use it. Otherwise look for <target>.trace.json
in the Lean directory. Returns None if not found.
"""
if explicit_path is not None:
if explicit_path.is_absolute():
return explicit_path if explicit_path.exists() else None
candidate = lean_dir / explicit_path
if candidate.exists():
return candidate
candidate = ROOT / explicit_path
return candidate if candidate.exists() else None
if not target:
return None
candidate = lean_dir / f"{target}.trace.json"
return candidate if candidate.exists() else None
def _run_pist_classify(trace_path: Path, lean_dir: Path) -> dict[str, Any]:
"""Run the canonical pist-classify-trace executable on a trace fixture."""
if not PIST_CLASSIFY.exists():
raise RuntimeError(f"pist-classify-trace not found at {PIST_CLASSIFY}")
proc = subprocess.run(
[str(PIST_CLASSIFY), str(trace_path)],
cwd=lean_dir,
capture_output=True,
text=True,
timeout=60,
)
if proc.returncode != 0:
raise RuntimeError(
f"pist-classify-trace failed: {proc.stderr[:500]}"
)
return json.loads(proc.stdout)
def _run_rrc_watchdog(pist_label: str, exact_label: str | None, rrc_shape: str, lean_dir: Path) -> dict[str, Any]:
"""Run the canonical rrc-watchdog executable for RRC alignment.
The executable returns JSON and exits 0 when score >= 86.
We capture exit code as part of the result but do not treat non-zero as failure.
"""
if not RRC_WATCHDOG.exists():
raise RuntimeError(f"rrc-watchdog not found at {RRC_WATCHDOG}")
cmd = [str(RRC_WATCHDOG), "--pist-label", pist_label]
if exact_label:
cmd.extend(["--exact-label", exact_label])
cmd.extend(["--rrc-shape", rrc_shape])
proc = subprocess.run(
cmd,
cwd=lean_dir,
capture_output=True,
text=True,
timeout=60,
)
try:
result = json.loads(proc.stdout)
except json.JSONDecodeError as e:
raise RuntimeError(
f"rrc-watchdog produced non-JSON output: {proc.stdout[:500]}"
) from e
result["exit_code"] = proc.returncode
return result
def _run_rrc_alignment(target: str, trace_path: Path, lean_dir: Path) -> dict[str, Any] | None:
"""Run PIST classification + RRC alignment gate on a trace fixture.
Returns a dict with the PIST output, RRC alignment output, and computed
receipt hash. Returns None if any step cannot be completed.
"""
try:
pist = _run_pist_classify(trace_path, lean_dir)
except Exception as e:
print(f"RRC PIST classification skipped: {e}", file=sys.stderr)
return None
predicted_shape = pist.get("predicted_rrc_shape", "HoldForUnlawfulOrUnderspecifiedShape")
tactic_family = pist.get("tactic_family", "unknown")
# rrc-watchdog expects a shape argument. Use the predicted shape as both
# the PIST label and the declared RRC shape, so the gate tests self-alignment.
try:
rrc = _run_rrc_watchdog(
predicted_shape,
None,
_shape_to_watchdog_arg(predicted_shape),
lean_dir,
)
except Exception as e:
print(f"RRC alignment gate skipped: {e}", file=sys.stderr)
return None
canonical = json.dumps(
{"pist": pist, "rrc": rrc},
sort_keys=True,
separators=(",", ":"),
)
return {
"pist": pist,
"rrc": rrc,
"predicted_shape": predicted_shape,
"tactic_family": tactic_family,
"canonical_json": canonical,
"receipt_hash": hashlib.sha256(canonical.encode()).hexdigest(),
}
def _shape_to_watchdog_arg(shape: str) -> str:
"""Map pist-classify-trace shape strings to rrc-watchdog CLI arguments."""
mapping = {
"SignalShapedRouteCompiler": "signalShapedRouteCompiler",
"ProjectableGeometryTopology": "projectableGeometryTopology",
"CognitiveLoadField": "cognitiveLoadField",
"CadForceProbeReceipt": "cadForceProbeReceipt",
"LogogramProjection": "logogramProjection",
"HoldForUnlawfulOrUnderspecifiedShape": "holdForUnlawfulOrUnderspecifiedShape",
}
return mapping.get(shape, "holdForUnlawfulOrUnderspecifiedShape")
def _insert_rrc_receipt(
pkg_id: str,
session_id: str,
alignment: dict[str, Any],
target: str,
) -> None:
"""Insert an RRC alignment receipt bound to the build package."""
pist = alignment["pist"]
rrc = alignment["rrc"]
residual = json.dumps(
{
"target": target,
"predicted_shape": alignment["predicted_shape"],
"tactic_family": alignment["tactic_family"],
"alignment_status": rrc.get("alignmentStatus", "unknown"),
"alignment_score": rrc.get("score"),
"alignment_warnings": rrc.get("warnings", []),
"pist_spectral_radius": pist.get("spectral_radius_q16"),
"rrc_exit_code": rrc.get("exit_code"),
},
separators=(",", ":"),
)
sql = f"""
INSERT INTO ene.receipts
(package_id, receipt_type, receipt_hash, input_hash, output_hash,
toolchain, verifier, status, residual)
VALUES
('{pkg_id}', 'rrc_alignment', '{alignment['receipt_hash']}',
'{hashlib.sha256(alignment['canonical_json'].encode()).hexdigest()}',
'{alignment['receipt_hash']}',
'pist-classify-trace; rrc-watchdog', 'opencode',
'{rrc.get('alignmentStatus', 'unknown')}',
'{residual}'::jsonb)
ON CONFLICT (package_id, receipt_type, receipt_hash) DO NOTHING;
"""
_ssh_psql(sql)
def main() -> int:
parser = argparse.ArgumentParser(description="Ingest lake build output into ENE on neon-64gb")
parser.add_argument("target", nargs="?", default="", help="lake build target (default: full build)")
parser.add_argument("--dir", type=Path, default=LEAN_DIR, help="directory to run lake build in")
parser.add_argument("--actor", default="opencode", help="actor name for session")
parser.add_argument("--dry-run", action="store_true", help="print parsed build info without writing")
parser.add_argument("--rrc", type=Path, nargs="?", const=True, default=None,
help="enable RRC alignment. Uses <target>.trace.json in LEAN_DIR if no path is given.")
args = parser.parse_args()
actor = args.actor
@ -282,13 +454,38 @@ def main() -> int:
file=sys.stderr,
)
# Resolve RRC trace fixture if requested.
rrc_alignment: dict[str, Any] | None = None
if args.rrc is not None:
explicit_path = args.rrc if isinstance(args.rrc, Path) else None
trace_path = _find_rrc_trace(target, explicit_path, args.dir)
if trace_path:
print(f"RRC trace fixture: {trace_path}", file=sys.stderr)
rrc_alignment = _run_rrc_alignment(target, trace_path, args.dir)
if rrc_alignment:
print(
f"RRC alignment: {rrc_alignment['rrc'].get('alignmentStatus')} "
f"score={rrc_alignment['rrc'].get('score')}",
file=sys.stderr,
)
else:
print(
f"RRC trace fixture not found for target '{target}' (use --rrc <path>)",
file=sys.stderr,
)
if args.dry_run:
print(json.dumps({"git": git, "build": build, "elapsed_ms": elapsed_ms}, indent=2))
payload = {"git": git, "build": build, "elapsed_ms": elapsed_ms}
if rrc_alignment:
payload["rrc_alignment"] = rrc_alignment
print(json.dumps(payload, indent=2))
return 0
session_id = _insert_session(target, git, build, elapsed_ms, actor)
pkg_id = _insert_package(session_id, target, git, build)
_insert_receipt(pkg_id, session_id, build)
if rrc_alignment:
_insert_rrc_receipt(pkg_id, session_id, rrc_alignment, target)
_insert_ingest_event(pkg_id, session_id)
print(f"Ingested: session={session_id} package={pkg_id}", file=sys.stderr)