From cd459e3a2448e8ebb01aa3c0f27b05a49eb33ea7 Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Wed, 19 Aug 2026 11:37:30 +0200 Subject: [PATCH 1/2] LSC1-08 S12: inline taken_proposal dead-write in JUMP decode arm --- SHA256SUMS | 2 +- asic_core/rtl/lsc1_packet_frontend.sv | 6 +- .../jump_taken_proposal_differential.py | 132 ++++++++++++++++++ 3 files changed, 135 insertions(+), 5 deletions(-) create mode 100644 evidence/lsc1-08-s12/jump_taken_proposal_differential.py diff --git a/SHA256SUMS b/SHA256SUMS index ab49e75..62e291a 100644 --- a/SHA256SUMS +++ b/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 diff --git a/asic_core/rtl/lsc1_packet_frontend.sv b/asic_core/rtl/lsc1_packet_frontend.sv index d5a183b..24611ab 100644 --- a/asic_core/rtl/lsc1_packet_frontend.sv +++ b/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; diff --git a/evidence/lsc1-08-s12/jump_taken_proposal_differential.py b/evidence/lsc1-08-s12/jump_taken_proposal_differential.py new file mode 100644 index 0000000..34fbd65 --- /dev/null +++ b/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()) From d71b01cfb0fa782de694f67d9e5640738984dd95 Mon Sep 17 00:00:00 2001 From: Thomas Marchand Date: Wed, 19 Aug 2026 12:26:29 +0200 Subject: [PATCH 2/2] LSC1-08 S12: register evidence/lsc1-08-s12/jump_taken_proposal_differential.py in SHA256SUMS This is a pure evidence-provenance fix; no RTL semantic change; re-verifies the same JUMP taken_proposal source change from the predecessor head cd459e3a. --- SHA256SUMS | 1 + 1 file changed, 1 insertion(+) diff --git a/SHA256SUMS b/SHA256SUMS index 62e291a..c1f4cdb 100644 --- a/SHA256SUMS +++ b/SHA256SUMS @@ -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