Formalize LSC-1u XOR retained-boundary refinement

[Th0rgal]

Scope

One sharply bounded LSC-1u equivalence tranche: a cycle-accurate reduced retained-state model for accepted XOR micro-ops, checked in lockstep against handwritten lsc1u_core observables from command acceptance through all 16 result beats and final retirement.

Base gate: origin/main was independently fetched immediately before branch creation and again immediately before commit/push. Both checks returned commit 31b146234bb786a77e25cef50b991ac3ba69de75, tree e2a5118d3f9c036337f0fe6e29e98eddcb30ec52.

Exact claims

The unbounded ABC PDR task proves, for every reachable execution after an initial reset:

• accepted idle commands in this lane are XOR (the only functional assumption);
• all 32 payload bytes are symbolic;
• rx_valid, tx_ready, ena, and rst_n may vary independently every cycle;
• retained XOR results equal A XOR B byte-for-byte;
• pending output data/valid survive arbitrary output stalls and enable pauses;
• input cannot advance across a pending result;
• reset at any cycle cancels partial or stalled work and restores the related boundary;
• lane 15 acceptance retires exactly once, clears the pending result, and returns idle.

The mechanically checked relation covers rx_ready, tx_valid, tx_data, busy, fault, and done_pulse. The reduced architectural state and inductive invariants are enumerated in formal/LSC1U_XOR_REFINEMENT.md.

The cover task reaches one composed trace containing command acceptance, a retained output stall, reset during an active operation, restart, and final retirement at depth 56.

Falsifiers / non-vacuity

• XOR ^ changed to +: both the existing protocol proof and the new refinement proof terminal-fail.
• retirement threshold changed from lane 15 to lane 14: the new refinement proof terminal-fails.
• the composed cover reaches all advertised behaviors in one concrete RTL trace.

Residual gaps

This is not full-controller equivalence. It does not prove opcode decode/fault responses, SET, MUL arithmetic, the Tiny Tapeout wrapper, packet LSC-1, Lean-to-RTL correspondence, liveness under unfair backpressure, or RTL-to-netlist equivalence. LSC-1u has no abort input, so abort refinement is outside this RTL interface rather than excluded by an assumption. The multiplier is replaced only for this XOR proof by an unconstrained-output boundary; no XOR transition reads it.

PR #30 was inspected read-only for proof-structure ideas and was not merged, checked out, rebased, or modified.

Local validation

• cd formal && sby -f lsc1u_xor_refinement.sby — exit 0, 2.00s; PDR PASS and cover PASS at depth 56.
• python3 formal/check_mutations.py --only xor_result --only xor_retirement_lane — exit 0, 5.16s; all three selected config runs rejected their mutations.
• make python conformance-check host-comparison design-space exact-xor interface-check consistency mincore-state-count smoke placeholders fpga-boundary fpga-harness — exit 0, 22.90s.
• make sim — exit 0, 3.14s.
• cd lean && lake build LeanVMBMinCore with pinned Lean 4.32.1 — exit 0, 21.71s.
• make checksum-check after final regeneration — exit 0, 0.05s.

One broader local python3 formal/check_mutations.py diagnostic reached and rejected every new mutation, then exited 1 because this host lacks yices-smt2 for the pre-existing gf128_serialize.sby mutation. That is a local dependency error, not hidden proof evidence; the targeted new mutation gate above passed, and CI installs the repository's pinned OSS CAD Suite.

Review / merge guard

Draft only. The author must not merge this PR. A distinct integrator must independently fetch and review the exact immutable head and merge only after exact-head gates and required CI are green.