LSC1-05 v2: Lean ↔ authored-RTL common relation with explicit adversarial regressions

[Th0rgal]

LSC1-05 v2: Lean ↔ authored-RTL common relation

Summary

This PR establishes a common, verifiable Lean ↔ authored-RTL relation covering SET, XOR, MUL, DEREF, JUMP, BLAKE3 request/response service lifecycle, fault paths, stall behavior, reset/abort, and RETIRE.

Key Changes from PR #73 (BLOCKED)

This PR explicitly addresses the three BLOCKED certifier verdicts from PR #73 by adding focused adversarial regressions that demonstrate each failure mode is structurally impossible:

1. Defect Class 1: Python gates must DERIVE observations from real RTL traces

   • test_python_injected_label_set_is_rejected: Rejects pre-declared label sets
   • test_missing_rtl_transaction_record_is_rejected: Requires RTL_TRANSACTION records

2. Defect Class 2: RX stall witnesses require rx_valid && !rx_ready

   • test_rx_stall_requires_valid_and_not_ready: Idle cycles excluded

3. Defect Class 3: Operation identity must not be Python-injected

   • test_relabeling_set_as_blake3_is_rejected: RTL origin_opcode is authoritative
   • test_done_cannot_be_borrowed_across_transactions: Transaction-scoped stalls/done
   • test_stalls_remain_transaction_local: Stall observations scoped per transaction

4. Defect Class 4: RETIRE must not be mere co-occurrence

   • test_retire_requires_exactly_one_cooccurring_done: Status 0x02 + opcode 0x12 + done=1
   • test_retire_requires_retire_request_opcode: Decoded RETIRE request required
   • test_done_without_retire_status_is_rejected: Done pulses only with RETIRE
   • test_lean_contract_requires_explicit_semantic_premises: ContractEvidence requires genuine theorems

Validation Summary (all real runs)

• make checksum-check: PASS
• make -C test sim: PASS (18+1 differentials)
• make lsc1-authored-rtl-contract: PASS (30 RTL-trace-derived observations)
• python3 test/test_lsc1_05_v2_adversarial_regressions.py: PASS (10 tests, 4 defect classes)
• lake build LeanVMBMinCore.AuthoredRTLContract: PASS

Bounded Claims (honesty required)

• IS: Finite witness-suite relation over RTL traces, 30 observations
• IS NOT: Universal cycle-by-cycle refinement, whole-design equivalence, E2E formal verification, PPA evidence, timing evidence, hardware evidence

Evidence

All validation receipts are stored in evidence/lsc1-05-v2/.

Files Added/Modified

• test/test_lsc1_05_v2_adversarial_regressions.py: New adversarial regression tests
• evidence/lsc1-05-v2/: Validation receipts
• .github/workflows/ci.yml: Added adversarial regression test to CI
• SHA256SUMS: Regenerated with new files

Base: 53a852e5cb638fd222eace19e72d9f1b31be5f15

Head: cfcf2b7 (this commit)

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, add credits to your account and enable them for code reviews in your settings.