SilverSight/docs/refactor/ANTI_SMUGGLE_REFACTOR_PLAN.md

Anti-Smuggle Refactor Plan — Implementation Design

Generated: 2026-06-29 Source: AGENTS.md "Beyond Rigorous — Anti-Smuggle Protocol" (§5) Design agents: Layers 0+1 (determinism + cross-validation), Layers 2+3 (mutation testing + CAS/SMT)

---

Overview

15 new files, ~1,400 lines total, zero changes to Lean source code.

Layer	Files	Est. Effort	Verdict When Missing
0: Determinism	3 new + 15 shim modifications	3 hr	Non-reproducible artifacts
1: Cross-validation	2 new	2.5 hr	Single-LLM blind spots
2: Mutation testing	7 new	2.5 hr	Verifier passes bad proofs
3: CAS/SMT grounding	1 new	2 hr	Vacuous/tautological proofs
Entry gate	1 new + 1 CI	0.5 hr	—
Total	15 new	~10.5 hr

---

Layer 0: Deterministic Reproducibility (scripts/seedlock.py + check_determinism.py)

Core: scripts/seedlock.py

• SeededRNG(seed) class — canonical RNG using Python's random.Random (stable across CPython versions)
• lock(seed) — monkey-patches random.seed() and np.random.seed() to raise RuntimeError after locking
• All existing Python shims (python/*.py, qubo/*.py) gain --seed 0 parameter
• Every np.random.default_rng() → SeededRNG(seed).np_random()

Scanner: scripts/check_determinism.py

• Checks all artifacts in extraction/ for content_sha256 hash chain integrity
• Scans Python sources for unseeded RNG calls → exit code 3 on violation
• Supports --seed 0, --receipt-dir, --check-all, --output
• Receipt: anti_smuggle_layer0_receipt_v1

Shim modifications (15 files)

All python/*.py and qubo/*.py gain argparse --seed (default 0). seedlock.SeedingRNG replaces all bare random.Random() and np.random.default_rng() calls.

---

Layer 1: Cross-Validation (scripts/cross_validate.py)

Key design constraint

Does NOT call LLMs directly. User provides proof files from 2+ models — verification is offline, no API keys embedded.

Workflow

1. Extract provenance headers from .lean files (# Provenance: model=..., generation_id=...)
2. Extract theorem signatures (name + type) from both files
3. Build both independently (lake build SilverSightRRC)
4. Equivalence check: normalize binder names to canonical form, compare statement types
5. Receipt: anti_smuggle_layer1_crossval_v1

CLI

python3 scripts/cross_validate.py \
    --model-a-proof path/to/A.lean --model-b-proof path/to/B.lean \
    --model-a-label gemma4-12b --model-b-label deepseek-v4-flash \
    --lean-target SilverSightRRC --output crossval_receipt.json

---

Layer 2: Mutation Testing (scripts/qc-flag/)

Directory structure

scripts/qc-flag/
  __init__.py          # Empty
  __main__.py          # CLI: python3 -m scripts.qc-flag
  manifest.json        # 22 mutations across 6 modules
  mutation_generator.py  # Regex-based mutation engine
  mutation_runner.py     # Backup → build → restore → score
  mutations/.gitkeep    # Generated mutation Lean files
  receipts/.gitkeep     # Per-run coverage receipts

Manifest (22 mutations over 6 modules)

Module	Theorems	Mutations	Pattern
HachimojiN8.lean	n8_satisfies, n8_is_minimum, n8_unique, n8_necessity	9	= true ↔ = false, ↔ → →, ≥ → <
RRC/Emit.lean	ncDerived_mul, ncDerived_independence_justification	4	mul → add, True → False
FisherRigidity.lean	spectralGapIntCompare	2	> → <, 9984 → 9361
CartanConnection.lean	Jacobiator_basis_all, Jacobiator_basis_zero	2	= ∅ → ≠ ∅, = 0 → = 1
HachimojiN8Bridge.lean	hachimoji_card...	2	Fintype.card = 8 → = 7
ReceiptCore.lean	hasReceiptOfKind	2	r.valid → ¬r.valid

Protocol

1. Back up original .lean file
2. Copy mutation over source
3. lake build SilverSightRRC — expect FAIL
4. Restore original
5. Coverage = #failed / #total. Verdict FAIL if any mutation passes the build

---

Layer 3: CAS/SMT Grounding (scripts/verify_with_sympy.py)

Three extractors, one verifier engine

Extractor A: Q16_16.ofRatio — extract all Q16_16.ofRatio N D patterns from Lean sources. Compute expected raw value = floor(N * 65536 / D) in SymPy. Compare with Lean build output.

Extractor B: ncDerived chain — for each FixtureRow fixture, follow the computation chain:

• residualRisk × scaleBandDeclared → ncDerived
• SymPy: Rational(n1, d1) * Rational(n2, d2)
• Compare Q16_16 raw values: floor(expr * 65536)

Extractor C: Z3 SMT-LIB2 — for each by decide/by native_decide block, generate an SMT2 script with the negated goal. Run z3 -smt2 and expect unsat.

Receipt: cas_verification_receipt_v1

{
  "sympy_results": {"ofratio_checks": 95, "match": 95, "ncderived_chains": 6, "match": 6},
  "z3_results": {"scripts": 7, "unsat": 7, "sat_unexpected": 0},
  "verdict": "PASS"
}

---

Entry Gate (scripts/run_entry_gate.sh)

#!/usr/bin/env bash
set -euo pipefail

echo "=== Layer 0: Determinism ==="; python3 scripts/check_determinism.py --seed 0
echo "=== Layer 1: Cross-Validation ==="; python3 scripts/cross_validate.py
echo "=== Layer 2: Mutation Suite ==="; python3 -m scripts.qc-flag --run
echo "=== Layer 3: CAS/SMT Grounding ==="; python3 scripts/verify_with_sympy.py
echo "=== Build Gate ==="; lake build SilverSightRRC
echo "=== ALL 5 LAYERS PASS ==="

---

Zero Changes to Lean Source

The anti-smuggle protocol is entirely external to the formal content:

• Mutations are generated as separate files that temporarily overwrite originals
• No Lean pragmas, feature flags, or @[mutation] attributes
• Backup/restore protocol keeps the checkout clean between tests
• lake build SilverSightRRC stays as the single build target

---

Risk Register

Risk	Mitigation
LLM hallucinates fake # Provenance: headers	Cross-validate proves only build equivalence; generation_id is audit-only
Two models produce syntactically different but semantically identical statements	Equivalence checker normalizes alpha-renaming; CAS grounding catches numeric disagreement
np.random.default_rng(seed) differs between numpy versions	Canonical RNG is Python's random.Random (stable across CPython)
Mutation backup/restore race in CI	Sequential execution per file; single worker by default
Z3 unavailable on CI	Skippable with --skip-z3; CAS-only mode available