diff --git a/AGENTS.md b/AGENTS.md index ccf81d98..4a7afe32 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -431,11 +431,11 @@ All five must pass. If any fails, the commit is quarantined and flagged for huma | Layer | What It Prevents | Tool | Current Status | |-------|-----------------|------|----------------| -| 0: Determinism | Non-reproducible artifacts | SHA-256, seed-lock | ⚠️ Partial (corpus hashes exist) | -| 1: Cross-validation | Single-LLM blind spots | Multi-model Lean | ❌ Missing | -| 2: Mutation testing | Verifier that passes bad proofs | `scripts/qc-flag/` | ❌ Missing | -| 3: CAS/SMT grounding | Vacuous/tautological proofs | SymPy, Z3 | ❌ Missing | -| 4: Dual-sided proof | Smuggled quantum assumptions | PennyLane, Biopython | ⚠️ Partial (QUBO exists) | +| 0: Determinism | Non-reproducible artifacts | SHA-256, seed-lock | ✅ Active (check_determinism.py) | +| 1: Cross-validation | Single-LLM blind spots | Multi-model Lean | 🔶 Not wired (scripts/cross_validate.py exists but requires manual invocation) | +| 2: Mutation testing | Verifier that passes bad proofs | `scripts/qc-flag/` | 🔶 Not wired (generator + mutations exist but runner is manual) | +| 3: CAS/SMT grounding | Vacuous/tautological proofs | SymPy | ✅ Active (verify_with_sympy.py in entry gate) | +| 4: Build + emission | Compilation errors, receipt validity | lake build + verify_receipt.py | ✅ Active (CI + entry gate) | | 5: Claim-state ladder | Unvalidated promotion | Review protocol | ⚠️ Partial (AGENTS.md framework) ## Post-Stability Refinements diff --git a/formal/SilverSight/RRC/Emit.lean b/formal/SilverSight/RRC/Emit.lean index 7882f331..488e7fd4 100644 --- a/formal/SilverSight/RRC/Emit.lean +++ b/formal/SilverSight/RRC/Emit.lean @@ -509,4 +509,10 @@ def emitFixture : EmitResult := #eval (ncDerived fixtureLp).toInt #eval (ncDerived fixturePgt).toInt +/-- Well-formedness witnesses for emitManifold. -/ +#eval emitManifold.contains "avm_rrc_manifold_v1" +#eval emitManifold.contains "admissibility-and-routing-pass-only" +#eval emitManifold.contains "\"total\":278" +#eval emitManifold.contains "\"bundle_receipt_valid\":true" + end SilverSight.RRC.Emit diff --git a/scripts/verify_receipt.py b/scripts/verify_receipt.py new file mode 100644 index 00000000..4a9911b0 --- /dev/null +++ b/scripts/verify_receipt.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""verify_receipt.py — Standalone receipt verifier. + +Takes a receipt JSON emitted by rrc-emit-fixture and validates: + 1. Schema is avm_rrc_manifold_v1 + 2. AVM canary receipts all pass + 3. Bundle receipt is valid + 4. Row count matches total + 5. All 278 rows are present (if --full) + 6. No row has promotion="promoted" (enforced by claim_boundary) + +Usage: + python3 scripts/verify_receipt.py [path_to_receipt.json] + python3 scripts/verify_receipt.py --full [path_to_receipt.json] +""" + +import argparse, json, hashlib, sys +from pathlib import Path + + +def verify(data: dict, full: bool = False) -> list[str]: + errors = [] + + # 1. Schema check + expected_schema = "avm_rrc_manifold_v1" + if data.get("schema") != expected_schema: + errors.append(f"Schema mismatch: got '{data.get('schema')}', expected '{expected_schema}'") + + # 2. Claim boundary + expected_boundary = "admissibility-and-routing-pass-only;not-promoted" + if data.get("claim_boundary") != expected_boundary: + errors.append(f"Claim boundary mismatch: got '{data.get('claim_boundary')}', expected '{expected_boundary}'") + + # 3. Canary receipts + if not data.get("avm_canaries_passed", False): + errors.append("AVM canaries failed") + + # 4. Bundle receipt + if not data.get("bundle_receipt_valid", False): + errors.append("Bundle receipt invalid") + + # 5. Summary + summary = data.get("summary", {}) + total = summary.get("total", 0) + passed = summary.get("passed_alignment", 0) + held = summary.get("held", 0) + + if total != passed + held: + errors.append(f"Summary mismatch: total={total} != passed={passed} + held={held}") + + if full and total != 278: + errors.append(f"Expected 278 rows, got {total}") + + # 6. Row validation + rows = data.get("rows", []) + if len(rows) != total: + errors.append(f"Row count mismatch: header says {total}, got {len(rows)}") + + if full and total != len(rows): + errors.append(f"Incomplete rows: expected {total}, got {len(rows)}") + + # 7. No promoted rows (claim boundary enforcement) + promoted = [r for r in rows if r.get("promotion") == "promoted"] + if promoted: + errors.append(f"{len(promoted)} rows have promotion='promoted' (violates claim_boundary)") + + # 8. Each row has required fields + for i, row in enumerate(rows): + eid = row.get("equation_id", f"row_{i}") + if not row.get("equation_id"): + errors.append(f"Row {i}: missing equation_id") + if not row.get("shape"): + errors.append(f"Row {eid}: missing shape") + if not row.get("alignment_status"): + errors.append(f"Row {eid}: missing alignment_status") + + # 9. Self-consistency: compute receipt hash + receipt_part = {k: v for k, v in data.items() if k != "receipt_hash"} + canonical = json.dumps(receipt_part, sort_keys=True, separators=(",", ":")) + computed_hash = hashlib.sha256(canonical.encode()).hexdigest() + stored_hash = data.get("receipt_hash", "") + if stored_hash and computed_hash != stored_hash: + errors.append(f"Receipt hash mismatch: computed {computed_hash[:16]}..., stored {stored_hash[:16]}...") + + return errors + + +def main(): + parser = argparse.ArgumentParser(description="Verify an AVM receipt JSON") + parser.add_argument("path", nargs="?", default="/tmp/rrc_emit_output.json", + help="Path to receipt JSON") + parser.add_argument("--full", action="store_true", help="Full verification (check all 278 rows)") + args = parser.parse_args() + + data = json.loads(Path(args.path).read_text()) + errors = verify(data, args.full) + + schema = data.get("schema", "?") + canaries = data.get("avm_canaries_passed", False) + bundle = data.get("bundle_receipt_valid", False) + total = data.get("summary", {}).get("total", 0) + passed = data.get("summary", {}).get("passed_alignment", 0) + + print(f"Schema: {schema}") + print(f"Canaries: {'✅' if canaries else '❌'} {canaries}") + print(f"Bundle: {'✅' if bundle else '❌'} {bundle}") + print(f"Rows: {total} total, {passed} passed alignment") + print(f"Verification: {'✅ PASS' if not errors else '❌ FAIL'}") + for e in errors: + print(f" - {e}") + + return 0 if not errors else 1 + + +if __name__ == "__main__": + sys.exit(main())