Formalize LSC-1u XOR retained-boundary refinement

.github/workflows/ci.yml

@@ -81,6 +81,8 @@ jobs:
         run: cd formal && sby -f lsc1u_protocol.sby
       - name: LSC-1u retained-operation reachability
         run: cd formal && sby -f lsc1u_reachability.sby
+      - name: LSC-1u XOR retained-boundary refinement
+        run: cd formal && sby -f lsc1u_xor_refinement.sby
       - name: Mutation sensitivity of retained safety and arithmetic properties
         run: make formal-mutations
       - name: Yosys lint and synthesis

Makefile

@@ -82,6 +82,7 @@ formal:
 	cd formal && sby -f gf8_mul.sby
 	cd formal && sby -f lsc1u_protocol.sby
 	cd formal && sby -f lsc1u_reachability.sby
+	cd formal && sby -f lsc1u_xor_refinement.sby
 
 formal-mutations:
 	$(PYTHON) formal/check_mutations.py

SHA256SUMS

@@ -1,10 +1,10 @@
-2119773e56595054a25e658cfa04cf2acd919e831db4f27cc940f862be162703  ./.github/workflows/ci.yml
+a28076e11a9ea19afdabc775ab9cbc458c5fb1db2dc7ff4dcb5c615bcc14fe4c  ./.github/workflows/ci.yml
 5e6a29a5b46af46a1d8ebb9cb9ed4b4042d492b86c752e7aaa845dc73c164c2f  ./.github/workflows/gds.yaml
 dc4fd27671dc6184c8106cac4193bada03706186206784f4cd872ca183592494  ./.github/workflows/tt-test.yaml
 160fb469e2232fac0b9e620106c3ca72c8fadbb34f75892f5186bc3b5a798883  ./.gitignore
 cfc7749b96f63bd31c3c42b5c471bf756814053e847c10f3eb003417bc523d30  ./LICENSE
 6bdbfe37959e0283134042372101a8a446432eb2516e085bf7850a712720c3c5  ./MANIFEST.md
-951f2caca90edf123f701c719b0745d08b450f63378c78d4a88456315179b493  ./Makefile
+daaa8dcb54310c55a6c9943d8efc52dcdf1ed86a9070dea12b2b3dcc3d7ca014  ./Makefile
 30fdeb94f91b6b8b57a05ffec53239284ec23366508bd0a5d59430cdde824d4d  ./README.md
 de4c0f6adf6ff1356bf9d7599ab52aef93a00b50c5a77c727ec0ce036ff2d1a2  ./RESULTS.md
 baa38ad5792511470f4cc9d2344d46f0c7af8a365d5b5e178dca88634b288bff  ./VALIDATION.txt
@@ -38,7 +38,7 @@ c41da7c4e22cc809e471da2bfcce176505db234c3b48e9c01ff20b8bcaef4b29  ./docs/M0_MANA
 3917ceaaac9cb7fbfd7ac07d6f980ff46a9103255c0859d5b47fefe691c726c3  ./docs/M2_CONTROLLER.md
 161cf4d25dcec4f21915e8b69ecdd2a929568bb8555bd613d0b96db215ce5be8  ./docs/MINCORE_UART_HOST.md
 9a7a857eda3d88aa6cc43a7e51b09e0869bf5f6423f34ab5b1195e59f1095348  ./docs/OPTIMALITY.md
-8fd1e228026e86d97d3a03d2c4d9c9ead1a543b6c6ecb3202b78acaa2533627f  ./docs/PROOF_BOUNDARIES.md
+719958e1a4f031c498e7ed1b8c1bfac3ba70af88a3d4bd30a989bf3f73c8b472  ./docs/PROOF_BOUNDARIES.md
 b81b89574ed84c67b64ae7b56001bf9d03b9d66be2bed7977d8adc715481eafb  ./docs/PROTOCOL.md
 659e958118beda0fb0dbaec47589b35c6c685d3078c80dc34a7d3a3a48aa93c2  ./docs/PROTOCOL_BYTE_CYCLE_AUDIT.md
 646490b9112c63a0673b8535e7f8d3091088c920fe84ea93c241bd78d9b4f766  ./docs/ROADMAP.md
@@ -57,8 +57,9 @@ c8dbcf0008931bfd0d6a27c00425480de54d322dd27367ae83f54f93e3382b8c  ./docs/semanti
 3e896ee33e3804876f6e169c872746146c1b3d773811683616986a4148b9f785  ./docs/semantics/reference/oracle.py
 c49a013eb503060394007d07395e625024d7c1ff0e9b177bc71e691e1a4efec8  ./docs/semantics/reference/vectors.json
 961d9f2f85fe6a6e2a5f586412e03759cb94a80683959e7f0271f37f200a4f1d  ./docs/upstream-clarifications/README.md
-dcacd1be08c71bc51b462f3b434a056fd1294c066b43057fcac00b5c0c0c87e5  ./formal/README.md
-1486cd0794137a682e6819faaf675939378b52327ec519e2cb27a56a0d120548  ./formal/check_mutations.py
+fa6a78d9503bedae2cdbf1a7d67ad0e84bbe171d6701da6739ce582e953aebdb  ./formal/LSC1U_XOR_REFINEMENT.md
+951a63cdc1079ceaabe3e075ee24ac3ff00387f11c208aa553065f8e0181e7f5  ./formal/README.md
+d06e4d70ddf5d33ec4521446f0628f51cf0d71ae01f19bcf79eaf02ee5a39067  ./formal/check_mutations.py
 2750eec4e2ff35adda6474dda1ddea18bf84be7e59e7db9d1e42e70e7a595d40  ./formal/gf128_mul_boundary_formal.sv
 45bc083098d91a1e9064acb93f52fad4a789c8d38071fdfbe3e9d6096683f431  ./formal/gf128_mul_reachability_formal.sv
 e1dd15bab27d5835a88bc7054b1f457e874256cd7449d02e52f44611870563c3  ./formal/gf128_serialize.sby
@@ -72,6 +73,9 @@ e098dda96308bf191d46ad58c8c6b9642372a6357e581270c7535bf75966e6de  ./formal/gf8_m
 86fb8eeb25a88369a839cc590270cd958f03138a0835d0bb2139c4d759a8371f  ./formal/lsc1u_protocol_formal.sv
 c0847d7e066bf0e400d294fbaabb49717dbbb97efc5033daed2c9d9d1a18673c  ./formal/lsc1u_reachability.sby
 a73a0e8fb66e95d9df074bb7270f74c0b6e2136502152e7a0300960e7bd74dba  ./formal/lsc1u_reachability_formal.sv
+6758b0ac70fd0b8d46b6ca7964bc573b4879c1f6a030f1b3da524e170b82a2aa  ./formal/lsc1u_xor_refinement.sby
+1109b38551b2286684f974521bb5a5808ac05811173c90884a05e1d5b9190e9c  ./formal/lsc1u_xor_refinement_cover.sv
+e47512976fda7e2154134346da3dd8e780b3185cdce3afbb205b774e2e5ccb73  ./formal/lsc1u_xor_refinement_formal.sv
 1e6b80dd959472d00411116899097fb37c930651efe6290fda93a8f4ae5ae97e  ./formal/stream_alu_mul_pulse.sby
 b61a1ea32d6b114093dd2679fd4fb3315dbfbb9829b8e4f739c0177f66ff1bc1  ./formal/stream_alu_mul_pulse_formal.sv
 53da30df5dd375567994d2e071664456f0c90d420710817fbbb4b53d894b668a  ./fpga/ulx3s/Makefile

docs/PROOF_BOUNDARIES.md

@@ -17,6 +17,7 @@ been completed.
 | SBY properties over exact SV modules | `formal/gf8_mul.sby` checks the exact parameterized SV multiplier instantiated at 8 bits, with the stated finite bound. | It does not prove the full controller, arbitrary stream behavior, production GF(2^128) multiplication, or ISA correspondence. | **Controller-formal gate:** properties over the exact completed `lean_silicon_lsc1` modules, with assumptions, depths/induction, and coverage documented per property. |
 | SBY byte-ordering property at WIDTH=128 | `formal/gf128_serialize.sby` proves by k-induction, over a symbolic `(* anyconst *)` 128-bit operand, that the shipped `gf128_mul_bitstream` loads byte `i` of the operand on load beat `i` and emits byte `j` on result-shift beat `j`. Reachability of the final shift beat is covered. | It proves **ordering only**, under a fixed schedule with `abort = 0`, one identity multiplier bit, and no back-to-back or partial transactions. It is **not** a proof that the GF(2^128) product is correct, and not a controller or ISA result. | **GF(2^128) product gate:** an operand-symbolic proof that the accumulator after 128 multiplier bits equals carry-less product mod `x^128 + x^7 + x^2 + x + 1`, plus a stream-protocol property covering abort and back-to-back transactions. |
 | SBY handshake property on shipped controller RTL | `formal/stream_alu_mul_pulse.sby` binds a checker into the shipped `leanvm_b_stream_alu` and proves by k-induction that `mul_a_valid`, `mul_bit_valid`, and `mul_result_shift` are mutually exclusive in every reachable state, with free stream inputs. Each of the three pulses is separately covered as reachable. This is the first assertion to hold over shipped controller RTL rather than a standalone harness. | It checks one documented handshake precondition of `gf2n_mul_bitstream`. It does **not** establish opcode decode correctness, result values, stream framing, abort handling, or any part of the packet controller. | **Assertion-inventory gate:** the remaining documented preconditions and framing invariants of the shipped modules, bound and proved the same way, and tied to the v1 relation. |
+| LSC-1u XOR retained-state refinement | `formal/lsc1u_xor_refinement.sby` proves an unbounded cycle-accurate relation from each accepted XOR command through 16 symbolic lane results and final retirement, with arbitrary ready/valid backpressure, enable pauses, and reset. Covers witness acceptance, stall, mid-operation reset, and retirement; mutations falsify result and retirement claims. | It assumes an accepted idle command is XOR, and does not cover opcode decode, SET/MUL, packet LSC-1, abort (LSC-1u has no abort port), Lean correspondence, or netlist equivalence. | **Remaining LSC-1u lanes:** add decode/fault, SET, and arithmetic-linked MUL refinements, then compose the wrapper and a shared functional relation. |
 | Simulation and differential evidence | Python/HDL tests compare scalar packet responses byte-for-byte on deterministic success and fault vectors. | Passing vectors are evidence, not a universal theorem or a synthesis-equivalence proof. | **Differential gate:** extend generated frozen/oracle/Lean/RTL v1 vectors through services, fault and stall coverage, reproducible seeds, and zero mismatches. |
 | Synthesis netlist and PPA | Yosys/OpenLane synthesis and Tiny Tapeout reports characterize a selected build. | A synthesized netlist/PPA report does not prove it preserves RTL behavior. | **RTL-to-netlist equivalence gate:** reproducible synthesis inputs plus sequential equivalence (including clock/reset constraints) for the release top, before PPA is treated as implementation evidence. |
 

formal/LSC1U_XOR_REFINEMENT.md

@@ -0,0 +1,77 @@
+# LSC-1u XOR retained-boundary refinement
+
+## Milestone and proven boundary
+
+`lsc1u_xor_refinement.sby` proves a cycle-accurate lockstep relation between
+the handwritten `lsc1u_core` RTL and a reduced retained-state model for one or
+more complete XOR micro-ops.  Every accepted idle command is assumed to be
+XOR; this is an opcode-specific refinement lane, not an opcode-decoder proof.
+All 32 payload bytes per command are otherwise arbitrary.
+
+The environment may independently vary `rx_valid`, `tx_ready`, `ena`, and
+`rst_n` on every cycle.  Consequently the proof includes arbitrary finite or
+infinite input/output backpressure, enable pauses, reset during any partial or
+stalled operation, and back-to-back XOR transactions.  It is a safety proof:
+an environment that never supplies a beat or never accepts a result is not
+assumed to make progress.  Separate covers demonstrate concrete acceptance,
+stalled-result retention, mid-operation reset, and final retirement traces.
+
+## Architectural state and relation
+
+The reduced model retains exactly:
+
+| Field | Meaning | RTL correspondence |
+|---|---|---|
+| `ref_phase` | idle, waiting for lane A, or waiting for lane B | `state` = `IDLE`, `XOR_A`, or `XOR_B` |
+| `ref_lane` | result lane to retire, 0 through 15 | `byte_index` |
+| `ref_a` | accepted first operand of the current lane | `saved_byte` |
+| `ref_result` | retained result byte | `out_byte` |
+| `ref_result_valid` | result is pending acceptance | `out_valid` |
+| `ref_fault` | retained fault state (always clear on this lane) | `fault_reg` |
+| `ref_retired` | one-cycle completion/retirement pulse | `done_reg` |
+
+These conceptual RTL correspondences explain the abstraction; the mechanically
+checked refinement relation is observational and equates `rx_ready`,
+`tx_valid`, `tx_data`, `busy`, `fault`, and `done_pulse` to functions of the
+reduced state on every post-initial clock boundary.  Because those equalities
+hold after every arbitrary input step, each retained field that can affect a
+later XOR observation is exercised through the transition relation rather than
+read through non-portable hierarchical references.  The
+multiplier is replaced by an unconstrained output because the XOR states never
+read it; this is a conservative cone cut, not a result assumption.
+
+## Inductive invariants
+
+- The lane index is always in `[0, 15]`.
+- Waiting for B never overlaps a pending output.
+- A pending output exists only in the A-wait phase, which prevents payload
+  acceptance until that exact retained byte is accepted.
+- The retained result after accepting a pair is exactly `A XOR B`.
+- Output data and validity remain unchanged through arbitrary `tx_ready = 0`
+  cycles and through `ena = 0` pauses.
+- Retirement occurs only after acceptance of lane 15, returns to idle, clears
+  the pending result, and is a single enabled cycle.
+- Reset restores all related retained state and cancels partial or stalled work.
+
+## Assumptions and residual gaps
+
+The only functional assumption is `rx_data == 8'h01` when a command handshake
+occurs in idle.  There is no fairness, ready/valid scheduling, payload-value,
+or reset-exclusion assumption.  LSC-1u exposes reset and enable but has no
+abort port, so abort refinement is outside this RTL interface rather than
+silently excluded.
+
+This tranche 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.  It supplies one
+compositional accepted-micro-op-to-arithmetic-result/retirement lane toward the
+full controller relation.
+
+Run:
+
+```sh
+cd formal
+sby -f lsc1u_xor_refinement.sby
+cd ..
+python3 formal/check_mutations.py
+```

formal/README.md

@@ -11,6 +11,10 @@ them proves the full LSC-1 controller or ISA correspondence.  See
 | `stream_alu_mul_pulse.sby` | `mul_a_valid`/`mul_bit_valid`/`mul_result_shift` are mutually exclusive in the shipped `leanvm_b_stream_alu` FSM | k-induction + cover |
 | `lsc1u_protocol.sby` | LSC-1u clamp/reset/stall/completion/framing plus retained XOR/SET bytes | unbounded PDR |
 | `lsc1u_reachability.sby` | Independent completion witnesses for XOR, MUL, SET, and fault response | bounded cover per opcode |
+| `lsc1u_xor_refinement.sby` | Cycle-accurate retained-state refinement from accepted XOR command through all arithmetic result beats and retirement | unbounded PDR + bounded covers |
+
+The XOR refinement's architectural state, invariants, assumptions, mutation
+falsifiers, and residual gaps are enumerated in `LSC1U_XOR_REFINEMENT.md`.
 
 ## LSC-1u retained boundary
 

formal/check_mutations.py

@@ -3,6 +3,7 @@
 
 from __future__ import annotations
 
+import argparse
 import shutil
 import subprocess
 import tempfile
@@ -30,7 +31,14 @@
         "src/lsc1u_core.sv",
         "out_byte <= saved_byte ^ rx_data;",
         "out_byte <= saved_byte + rx_data;",
-        ["lsc1u_protocol.sby"],
+        ["lsc1u_protocol.sby", "lsc1u_xor_refinement.sby"],
+    ),
+    (
+        "xor_retirement_lane",
+        "src/lsc1u_core.sv",
+        "if (tx_fire && (state != IDLE)) begin\n                if (byte_index == 4'd15)",
+        "if (tx_fire && (state != IDLE)) begin\n                if (byte_index == 4'd14)",
+        ["lsc1u_xor_refinement.sby"],
     ),
     (
         "set_result",
@@ -57,12 +65,22 @@
 
 
 def main() -> int:
+    parser = argparse.ArgumentParser()
+    parser.add_argument(
+        "--only",
+        action="append",
+        default=[],
+        help="run only the named mutation (repeatable)",
+    )
+    args = parser.parse_args()
     sby = shutil.which("sby")
     if not sby:
         raise SystemExit("sby is required")
 
     failures: list[str] = []
     for name, relative, old, new, configs in MUTATIONS:
+        if args.only and name not in args.only:
+            continue
         with tempfile.TemporaryDirectory(prefix=f"lsc1u-{name}-") as raw:
             work = Path(raw)
             shutil.copytree(ROOT / "formal", work / "formal")

formal/lsc1u_xor_refinement.sby

@@ -0,0 +1,29 @@
+[tasks]
+prove
+cover
+
+[options]
+prove: mode prove
+prove: depth 32
+cover: mode cover
+cover: depth 80
+timeout 180
+vcd off
+
+[engines]
+prove: abc pdr
+cover: btor btormc
+
+[script]
+read -formal -sv gf128_mul_boundary_formal.sv
+read -formal -sv lsc1u_core.sv
+prove: read -formal -sv lsc1u_xor_refinement_formal.sv
+cover: read -formal -sv lsc1u_xor_refinement_cover.sv
+prove: prep -top lsc1u_xor_refinement_formal
+cover: prep -top lsc1u_xor_refinement_cover
+
+[files]
+gf128_mul_boundary_formal.sv
+../src/lsc1u_core.sv
+lsc1u_xor_refinement_formal.sv
+lsc1u_xor_refinement_cover.sv

formal/lsc1u_xor_refinement_cover.sv

@@ -0,0 +1,37 @@
+`default_nettype none
+
+// Deterministic composed witness: accept XOR, retain a stalled result, reset
+// mid-operation, then restart and retire a complete 16-lane XOR transaction.
+module lsc1u_xor_refinement_cover;
+    (* gclk *) reg clk;
+    reg [6:0] cycle = 0;
+    reg seen_accept = 0;
+    reg seen_stall = 0;
+    reg seen_reset_midop = 0;
+
+    wire rst_n = (cycle != 0) && (cycle != 4);
+    wire rx_valid = 1'b1;
+    wire [7:0] rx_data = 8'h01;
+    wire tx_ready = !(tx_valid && !seen_stall);
+    wire rx_ready, tx_valid, busy, done_pulse;
+
+    lsc1u_core dut (
+        .clk(clk), .rst_n(rst_n), .ena(1'b1),
+        .rx_data(rx_data), .rx_valid(rx_valid), .rx_ready(rx_ready),
+        .tx_data(), .tx_valid(tx_valid), .tx_ready(tx_ready),
+        .busy(busy), .fault(), .done_pulse(done_pulse)
+    );
+
+    always @(posedge clk) begin
+        cycle <= cycle + 1'b1;
+        if (rst_n && rx_valid && rx_ready)
+            seen_accept <= 1'b1;
+        if (rst_n && tx_valid && !tx_ready)
+            seen_stall <= 1'b1;
+        if (cycle == 4 && busy)
+            seen_reset_midop <= 1'b1;
+        cover(seen_accept && seen_stall && seen_reset_midop && done_pulse);
+    end
+endmodule
+
+`default_nettype wire