diff --git a/4-Infrastructure/shim/lake_build_ingest.py b/4-Infrastructure/shim/lake_build_ingest.py index e3bf39f6..8bc1f3e8 100644 --- a/4-Infrastructure/shim/lake_build_ingest.py +++ b/4-Infrastructure/shim/lake_build_ingest.py @@ -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 .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 .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 .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 )", + 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)