LSC1-08 S12: inline taken_proposal dead-write in JUMP decode arm

SHA256SUMS

@@ -26,7 +26,7 @@ af51a2f56073aee7ef95c183e06d0e7c0e0613a0c7193d9f883ed26b026986a8  ./asic_core/rt
 d89d5cef0c529810a8a456892aaf13134e3b7ce34894f4c45da43ba81c7e066d  ./asic_core/rtl/lsc1_cell_alias_check.sv
 5fafb0f5fe81ac5aaf32d0d9974d7d7d2e2b66dde05cdb707e2067ab516f5e05  ./asic_core/rtl/lsc1_field_encoder.sv
 320e989e5480b6641f99f18822edeee5634f3d277f2faa408aaee2d21503d625  ./asic_core/rtl/lsc1_gf128_mul.sv
-73801f1c662270f021ded1ab9e2d525afe6b5cb693d83a8397a35d2502e615d3  ./asic_core/rtl/lsc1_packet_frontend.sv
+fe5d7e710409b784406733e217cd1b8e00bfb539575d01b95d400f2a0f1546e3  ./asic_core/rtl/lsc1_packet_frontend.sv
 5ce2edcd9e18a02ea276a541623c981b523945936e198e04c379981efe5f81a3  ./asic_core/rtl/lsc1_packet_rx.sv
 8a9a1c80b85fbeb253f955e618dc1521aff6fb432698c8bb5eef743e1eefcb2e  ./asic_core/rtl/lsc1_packet_tx.sv
 0d0cee24aea05b1a2ae2691a1cc46518af79b79e6228b8bb41031394c15b8d4f  ./asic_core/rtl/lsc1_request_validator.sv
@@ -100,6 +100,7 @@ ec0be722d23f23486060648e705689d862f6dd50c8440059b285ccedb430e6c9  ./evidence/lsc
 3da9065a4d97a00c735b10e92739b598b1309f13ce58c02f35e4cb1d69566ee6  ./evidence/lsc1-08-s11/dominance_probe.sv
 a6da3737284a64f9fd8f71e2ecb0b63a557232cbf069ed2e534ac097c54ec372  ./evidence/lsc1-08-s11/receipt.json
 ae3d9bc7b886cd8acdac310195130c582fe4bb235ded5f61cd53df732cc034af  ./evidence/lsc1-08-s11/receipt.json.sha256
+76e24c05a2f298378e7f85a06b8b90cb58a9c94e41d6567a38b20272a9136e8c  ./evidence/lsc1-08-s12/jump_taken_proposal_differential.py
 b0afb9a5a826e8a468f3bae65991c624abb01fa3796b889fc854e8cc76872a9e  ./evidence/lsc1-08-s3/full-lsc1-netlist-receipt.json
 cfa734602cf69a09a9d7d2a5219e59dc4ec89e73afbf9007b00b0b2d24c0de8c  ./evidence/lsc1-08-s3/yosys-structure-receipt.json
 b954bbd1a96b146b15df8fa0d675c44af3737a6191baa1fb00e29e2cb9f40e90  ./evidence/lsc1-08-s4/receipt.json

asic_core/rtl/lsc1_packet_frontend.sv

@@ -357,7 +357,6 @@ module lsc1_packet_frontend (
     reg [31:0] next_pc_value, next_fp_value;
     reg [31:0] deferred_target, deferred_local;
     reg [7:0] profile, pres_a, pres_b, pres_c, inv_present;
-    reg [7:0] taken_proposal;
     reg [127:0] val_a, val_b, val_c, inv_value, result_value;
     reg [127:0] solved_a, solved_b;
     reg [31:0] write_address;
@@ -906,7 +905,6 @@ module lsc1_packet_frontend (
                         val_a = frame_payload[216 +: 128];
                         val_b = frame_payload[352 +: 128];
                         val_c = frame_payload[488 +: 128];
-                        taken_proposal = frame_payload[77*8 +: 8];
                         proposed_pc = frame_payload[78*8 +: 32];
                         proposed_fp = frame_payload[82*8 +: 32];
                         inv_present = frame_payload[86*8 +: 8];
@@ -918,10 +916,10 @@ module lsc1_packet_frontend (
                             addr_a = fp + off_a; addr_b = fp + off_b; addr_c = fp + off_c;
                             if (cell_alias_inconsistent) begin
                                 decision_ok = 0; decision_fault = ALIAS_INCONSISTENT;
-                            end else if (taken_proposal != (val_a != 0)) begin
+                            end else if (frame_payload[77*8 +: 8] != (val_a != 0)) begin
                                 decision_ok = 0; decision_fault = BAD_BRANCH_PROPOSAL;
                                 decision_detail = 1;
-                            end else if (taken_proposal) begin
+                            end else if (frame_payload[77*8 +: 8]) begin
                                 if (proposed_pc >= 32'h00010000 ||
                                     proposed_fp >= 32'h00010000) begin
                                     decision_ok = 0; decision_fault = INDEX_RANGE;

evidence/lsc1-08-s12/jump_taken_proposal_differential.py

@@ -0,0 +1,132 @@
+#!/usr/bin/env python3
+"""Direct differential proof: JUMP taken_proposal field enumeration.
+
+This script enumerates JUMP frames varying the taken byte (byte 77)
+and verifies model vs RTL behavior is identical after inlining
+taken_proposal = frame_payload[77*8 +: 8].
+"""
+from __future__ import annotations
+import os
+import random
+import shutil
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[0]
+sys.path.insert(0, str(ROOT / "sim"))
+from sim import lsc1_transaction as protocol
+
+RTL = [
+    "asic_core/rtl/lsc1_packet_rx.sv",
+    "asic_core/rtl/lsc1_packet_tx.sv",
+    "asic_core/rtl/lsc1_response_payload_mux.sv",
+    "asic_core/rtl/lsc1_blake3_alias_check.sv",
+    "asic_core/rtl/lsc1_request_validator.sv",
+    "asic_core/rtl/lsc1_cell_alias_check.sv",
+    "asic_core/rtl/lsc1_blake3_lifecycle.sv",
+    "asic_core/rtl/gf2n_mul_bitstream.sv",
+    "asic_core/rtl/gf128_mul_bitstream.sv",
+    "asic_core/rtl/leanvm_b_stream_alu.sv",
+    "asic_core/rtl/lsc1_stream_adapter.sv",
+    "asic_core/rtl/lsc1_field_encoder.sv",
+    "asic_core/rtl/lsc1_packet_frontend.sv",
+    "test/packet_frontend/tb_lsc1_packet_vector.sv",
+]
+
+
+def rtl_path(path: str) -> Path:
+    override = os.environ.get("LSC1_RTL_DIR")
+    if override and path.startswith("asic_core/rtl/"):
+        return Path(override) / Path(path).name
+    return ROOT / path
+
+
+def model_exchange(frame: protocol.RequestFrame) -> bytes:
+    endpoint = protocol.Lsc1Endpoint()
+    response, _ = protocol.drive(endpoint, frame.encode())
+    return response
+
+
+class DifferentialProof:
+    def __init__(self):
+        if shutil.which("iverilog") is None or shutil.which("vvp") is None:
+            raise RuntimeError("Icarus Verilog not available")
+        self.temporary = tempfile.TemporaryDirectory()
+        self.simulator = Path(self.temporary.name) / "packet-vector.vvp"
+        sources = [str(rtl_path(path)) for path in RTL]
+        subprocess.run(
+            ["iverilog", "-g2012", "-s", "tb_lsc1_packet_vector", "-o", str(self.simulator)]
+            + sources,
+            cwd=ROOT,
+            check=True,
+            capture_output=True,
+            text=True,
+        )
+
+    def rtl_exchange(self, frame: protocol.RequestFrame) -> bytes:
+        encoded = frame.encode()
+        request = Path(self.temporary.name) / "request.hex"
+        request.write_text("\n".join(f"{byte:02x}" for byte in encoded) + "\n")
+        run = subprocess.run(
+            ["vvp", str(self.simulator), f"+REQUEST={request}", f"+LENGTH={len(encoded)}"],
+            cwd=ROOT,
+            check=True,
+            capture_output=True,
+            text=True,
+        )
+        line = next(item for item in run.stdout.splitlines() if item.startswith("RESPONSE "))
+        return bytes.fromhex(line.removeprefix("RESPONSE "))
+
+    def close(self):
+        self.temporary.cleanup()
+
+
+def build_jump_varying_taken(txn_id: int, taken_byte: int, val_a_zero: bool) -> protocol.RequestFrame:
+    """Build a JUMP frame with a specific taken_byte value."""
+    payload = protocol.transaction_preamble(txn_id, pc=0, fp=64, profile=protocol.Profile.INTERPRETER_COMPAT)
+    payload += b"".join(protocol.u32le(offset) for offset in (1, 2, 3))
+    payload += b"".join(cell.encode() for cell in (
+        protocol.Cell(True, 7),
+        protocol.Cell(True, 9),
+        protocol.ABSENT,
+    ))
+    payload += protocol.u8(taken_byte)
+    payload += protocol.u32le(0x1000)
+    payload += protocol.u32le(0x40)
+    payload += protocol.Cell(True, 1).encode()
+    return protocol.RequestFrame(protocol.Opcode.JUMP, payload)
+
+
+def main():
+    random.seed(0xdeadbeef)
+    proof = DifferentialProof()
+    mismatches = []
+    total = 0
+
+    taken_values = list(range(256))
+
+    for taken_byte in taken_values:
+        for val_a_zero in (True, False):
+            total += 1
+            frame = build_jump_varying_taken(0, taken_byte, val_a_zero)
+            model_resp = model_exchange(frame)
+            rtl_resp = proof.rtl_exchange(frame)
+            if model_resp != rtl_resp:
+                mismatches.append((taken_byte, val_a_zero, model_resp.hex(), rtl_resp.hex()))
+
+    proof.close()
+
+    if mismatches:
+        print(f"FAIL: {len(mismatches)}/{total} mismatches")
+        for m in mismatches[:5]:
+            print(f"  taken={m[0]} val_a_zero={m[1]} model={m[2]} rtl={m[3]}")
+        return 1
+
+    print(f"PASS: {total}/{total} JUMP taken_proposal enumerations match")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())