Add safe BLAKE3 service host/model prerequisites

.gitignore

@@ -19,6 +19,7 @@ formal/stream_alu_mul_pulse_induction/
 formal/stream_alu_mul_pulse_cover/
 openlane/
 reports/
+tools/blake3_reference/target/
 
 # Scratch outputs of the ULX3S build scripts. The scripts archive the copies
 # that matter under results/.

SHA256SUMS

@@ -1,5 +1,5 @@
 16c3eb42112e6e913a017dd1d12c05ab5c4455ead68d24b12d6c3c4b5dec138c  ./.github/workflows/ci.yml
-e01c466509630117b96ee5ddac3ad887ec95a932cfd5b1efcff77fe4f3891133  ./.gitignore
+89ddbb926aa9bfae6b904e68e706996b52c461789805bcc44ec111ba5e471942  ./.gitignore
 cfc7749b96f63bd31c3c42b5c471bf756814053e847c10f3eb003417bc523d30  ./LICENSE
 ca1b6b510bfeb5dc906aa0862e95d962c2901c246fa10fa72296d1666239d601  ./MANIFEST.md
 7d9bcd140d1c908e8aec2db0f7fc139b543b35b9f20a94c327fd1fe21d3ad9bd  ./Makefile
@@ -20,6 +20,7 @@ bf844b461def08fbf5b69093f95f792fd9302b26098351d192e32c76583f001b  ./asic_core/rt
 d0e2aa043df30c49d946e88503a4edf55ad4fa4467fb8b7e0b49b1e385a58c94  ./asic_core/rtl/lsc1_packet_tx.sv
 41b68a8068f417ff8f0d33f0408405f4fae5a7b5e2fd60b482d11148e541e6c7  ./asic_core/rtl/lsc1_stream_adapter.sv
 44078c940b3fa598bed96be6856e1f35f2ae9ec8d2ad9b8f0ec3d95fb287d6ed  ./docs/ARCHITECTURE.md
+24632f4d4e5ded07d158f5c70c0b4fb1ca323424217fff8a6348b062fddc22d0  ./docs/BLAKE3_EXTERNAL_SERVICE.md
 ac44a1838e7da255ed93835cc0de01e1751efc05f78cf9f8b8145cc963d6836a  ./docs/DECISIONS.md
 5ecf1ccdc8eb9562aaee69502fab30727351290892df2483e29680149eada14f  ./docs/FULL_CORE.md
 b989d03d5e6c7dd3c1c11bf40277da8d700463601f23c8c51787f8ac371bc596  ./docs/FULL_CORE_PROTOCOL.md
@@ -37,7 +38,7 @@ b81b89574ed84c67b64ae7b56001bf9d03b9d66be2bed7977d8adc715481eafb  ./docs/PROTOCO
 0d787acfaa683bf07cedea98ba403d51079593b50f84b48ee199a479cc35b099  ./docs/SEMANTICS.md
 6ec7c4c80628391da706725be1a2361ae8eb2ee014fb4cde6dae31c53f13e9f0  ./docs/SEMANTIC_DIFFERENCES.md
 02e8a5b52b341390f008ff8bc62f5d2d982b23adb8b26cb73ef3b07dddeed807  ./docs/SOURCE_AUDIT.md
-d7dd7941ebb9bfc41f1a64a8cdcaa1131c33c166ae83e6efb45126a86add6def  ./docs/STATUS.md
+fa5be10092d58337585f6a070bced8f814c82e75f0fabddb71daeca0cdc5c7ab  ./docs/STATUS.md
 9c2582c40fbd9a4e2b163abed784f5a6c82b2cb3136c37a4123a0ba6584f6136  ./docs/TAPEOUT.md
 e61e74c84bce2ec92ef18520eb134299f9341e63d3ec43cdbe0ef4879d22ba37  ./docs/ULX3S_SMOKE_AND_UART.md
 a08743f1a3cf4af68683cdaac5b00ca624ac875dbeef9f78614bda7297579df8  ./docs/USE_CASES.md
@@ -94,8 +95,9 @@ ee455920032996e22976f2ddba66233deb1d6c7a0c2052f07a5522a08650165b  ./fpga_harness
 1dbb9ccfc98a89a3e9cab14a940657e2a4a7401296c79234fd59640cb1a1230a  ./fpga_harness/tests/host_uart/test_lsc1_packet_uart.py
 704cd872313034d4d729e28be9ea2f38acedb91b012bbb29defadc4dc86baddb  ./fpga_harness/tests/host_uart/test_mincore_uart.py
 20b18779647bb635239ad75a2ee36c9e83b3014ff0fd8fd13a9e7eb0aa3754d4  ./fpga_harness/ulx3s_uart.py
-f5ed308c1920b2b2df6baa2de33ee72b982c7cf1cdc4d085c0cf6238dc8ae22e  ./host/README.md
+c0e199f835d0666e415cc16973d0ffa448fad205662305fb5ab1843481a7c162  ./host/README.md
 a8294c47be51b34fd3d8f80499618218838d3dece1e3d6b06f8e704ee02ca25f  ./host/__init__.py
+de09f085c4774abffbfbc6821b57f37ae1507614bab2c95007257732878bdb56  ./host/blake3_service.py
 8fb848653468cf64ecf26e1d7acf598fe30027630ebe1941ec8424ee2f0a6079  ./host/errors.py
 874459bdbf12b235ed93f333f5f4db176008b43c02e943d38e44fefc974c9b5a  ./host/fixtures/assert_set_xor_mul.program.json
 861f78055c35b7d1a5a80aa7a219d1334f52488f273dcb14017a3ff47bcc60a9  ./host/fixtures/assert_set_xor_mul.zkdsl
@@ -304,6 +306,7 @@ dee5dc820b96f24d4dbd752b17aaad3c8e025d519c043dfd1ab7c46be5600245  ./sim/packet_e
 659496fd9f21edafb7c4c12500d9b623bd0ea063808dc9494053ad923102dc31  ./sim/protocol_contract.py
 33a0956687b75cb08d19e58a7da8fc4acf622e63795f1220f57a38bc6d2c4117  ./sim/scalar_step_oracle.py
 d14a3e8aed08ece9ce5d9ac4ddc2d29bf218dcb4626592a11ff63eb36fe454dc  ./sim/test_atomic_publish.py
+45dff2ed4c9b579c66524abc7a0207d84c47421de401439b9cbd7826f0688b3b  ./sim/test_blake3_service.py
 a2fda9c21da5f3301de411060ffbb644c08c4c5e4c103e036b3834e2922ce10a  ./sim/test_cycle_model.py
 002325ca4bcceb7b5ec19e8b279df399661ac368b118eb160d97a6a450fe74e7  ./sim/test_host_runtime.py
 f1ab500117ae9d7a20a9258a32dbc7271b4d0ec5f57d3fc058ff426ba2289a40  ./sim/test_lsc1_protocol_doc.py
@@ -328,6 +331,9 @@ d0c03fb87fe5f08fbec435d485e4dd14c96d164e90b0e8b0ed8980cf27e8c077  ./test/tb_m2_s
 b78b938f396ae20d1fdccde99281430778a879808e60a35788b6fe044151329c  ./test/tb_stream_alu.sv
 1cdfef46a813dd43f5700b5e3ed7ec0bfb07e07403c82f8ac8fa4fb4dfbd0d55  ./test/tb_uart_bridge.sv
 e401ecd06a20a3f1e54de6e47ff6e12f61064bd2b9278517fe3d0db97933bd8a  ./tools/atomic_publish.py
+7894f75175f62edfd1ed33639a23d736ad6e57ddd9182e040f556502bff21a52  ./tools/blake3_reference/Cargo.lock
+e28e67bc3fd6dee898130648c74691ca7b8e61d1fccfa75c52d87d52fc8d9c3f  ./tools/blake3_reference/Cargo.toml
+3414b26004416f8871274b30fa975b40f611b5b6b148a2e1b3d97c109cd37f52  ./tools/blake3_reference/src/main.rs
 008f814b114282389ae48ff82e4412fe455cbe8c377cf71e534862d490d3cb79  ./tools/design_space.csv
 75dc51b45b2631ddc57c4629982949696f1b711323f6e857ca19dc42961f7359  ./tools/design_space.md
 0af763b6f1c340179fc959f243e0af93f0a1138482d6f60a23590691f47fce5a  ./tools/design_space.py

docs/BLAKE3_EXTERNAL_SERVICE.md

@@ -0,0 +1,84 @@
+# External BLAKE3 service prerequisites
+
+This document freezes the software/model boundary only. No production
+SystemVerilog, ASIC/FPGA transport, UART, JTAG, or hardware path implements this
+service yet.
+
+## Transport-independent schema
+
+All integers are little-endian. Exactly one service may be outstanding.
+
+`SERVICE_REQUIRED` is 131 bytes:
+
+| Offset | Bytes | Field |
+| ---: | ---: | --- |
+| 0 | 1 | schema version (`1`) |
+| 1 | 8 | host-created nonzero `session_epoch` |
+| 9 | 4 | `txn_id` |
+| 13 | 4 | `service_id` |
+| 17 | 1 | kind (`1`, BLAKE3 compression) |
+| 18 | 1 | reserved zero |
+| 19 | 64 | message block |
+| 83 | 32 | chaining value |
+| 115 | 8 | counter |
+| 123 | 4 | block length (`0..64`) |
+| 127 | 4 | flags (known mask `0x7f`) |
+
+`SERVICE_RESPONSE` is 53 bytes:
+
+| Offset | Bytes | Field |
+| ---: | ---: | --- |
+| 0 | 1 | schema version (`1`) |
+| 1 | 8 | `session_epoch` |
+| 9 | 4 | `txn_id` |
+| 13 | 4 | `service_id` |
+| 17 | 1 | kind |
+| 18 | 1 | status (`OK`, transient failure, permanent failure) |
+| 19 | 2 | digest length (must be `32`) |
+| 21 | 32 | digest |
+
+The binding key is `(session_epoch, txn_id, service_id, kind)`. The host creates
+a fresh unpredictable epoch after endpoint reset or reconnect and does not
+reuse transaction IDs within it. ABORT invalidates the outstanding key. Reset
+invalidates the epoch. A retry reuses the identical key and operands. The
+current v1 wire payload remains the inner model ABI; until an eventual wire
+revision, the adapter is the trusted epoch boundary.
+
+Malformed lengths, version/status values, digest lengths, metadata, and
+bindings are semantic failures and never mutate staged state. Tool startup,
+process exit, and transport availability are infrastructure failures and are
+reported separately. Only infrastructure failures receive bounded automatic
+retry. A successful response moves the model to `RESULT_PENDING`; neither
+endpoint state nor host memory commits until a validated `RETIRE`/`RETIRED`
+exchange.
+
+There is no endpoint service-latency bound. Ready/valid data must remain stable
+under arbitrary stalls, and timeout policy belongs to the host. Timeout
+recovery must explicitly ABORT or reset; reconnect alone is not a commit or an
+abort.
+
+## Future production direction
+
+The recommended RTL direction remains one logical 122-byte v1
+`SERVICE_REQUIRED` payload serialized scatter/gather from immutable RX storage.
+The current TX payload store is 68 bytes, so production RTL cannot emit it.
+Scatter/gather avoids duplicating another 122-byte register bank and avoids
+transport-level fragmentation. Its design gates are:
+
+- byte-exact mapping and CRC under a stall at every output byte;
+- RX storage immutable until the final transmitted beat;
+- ABORT/reset invalidate same-edge transfers and all source references;
+- existing short responses remain byte-identical.
+
+These are documentation/design-test requirements, not implemented RTL claims.
+Production SystemVerilog and ASIC/FPGA transports remain out of scope until the
+logical corpus and protocol interfaces stabilize.
+
+## Executable evidence
+
+`host/blake3_service.py` supplies the codecs, epoch/replay adapter, bounded retry
+policy, and a direct compression implementation. `sim/test_blake3_service.py`
+compares it against the official `blake3_guts` low-level compression API using
+the exact dependency and registry checksum pinned by
+`tools/blake3_reference/Cargo.lock`. Oracle build/execution failures raise
+`ServiceInfrastructureError`; byte mismatches remain ordinary test failures.

docs/STATUS.md

@@ -7,7 +7,7 @@
 | v1 transaction protocol | specified and executably modelled | `docs/LSC1_TRANSACTION_PROTOCOL.md`, `sim/lsc1_transaction.py` |
 | v1 scalar packet executor | SET/XOR/MUL/DEREF/JUMP implemented in RTL; BLAKE3 service pending | `asic_core/rtl/lsc1_packet_frontend.sv`, RTL differential tests |
 | Host runtime, SET/XOR/MUL/DEREF/JUMP transactions | driven against the executable endpoint; frozen fixture reaches full `MATCH` | `docs/HOST_RUNTIME.md`, `host/`, `sim/test_host_runtime.py` |
-| Host runtime, BLAKE3 | not implemented, explicit unsupported path | `host/lean_compiler_adapter.py` |
+| Host runtime, BLAKE3 | schema/model adapter prerequisites tested; compiler/runtime and production transport remain explicit unsupported paths | `host/blake3_service.py`, `sim/test_blake3_service.py` |
 | lean_compiler integration | artifact exported from the frozen compiler; `hints`/`main_frame`/`witness`/`trace` are `pub(crate)` upstream | `tools/lean_compiler_export.py`, `docs/HOST_RUNTIME.md` section 4 |
 | Host vs frozen Rust comparison | final memory for the 12 cells the fixture run touched and `cycles` compared when the run reaches the sentinel; every per-step field explicitly not compared | `tools/host_upstream_comparison.py`, `docs/HOST_RUNTIME.md` section 5 |
 | Scalar packet subset | SET/XOR/MUL/DEREF/JUMP implemented in the executable model, host path and RTL; finite differential evidence only, with no full-scalar refinement theorem | `sim/test_packet_frontend_rtl_differential.py`, `docs/PROOF_BOUNDARIES.md` |

host/README.md

@@ -11,11 +11,15 @@ the upstream comparison.
 | `memory.py` | write-once memory, pointer map, deferred state, inverse witnesses |
 | `lean_compiler_adapter.py` | loads and validates an exported program artifact |
 | `runtime.py` | prepares, drives, retires and applies one transaction per instruction |
+| `blake3_service.py` | transport-neutral schema, epoch guard and compression adapter |
 | `fixtures/` | a zkDSL source and the artifact compiled from it by the frozen upstream |
 
 This package consumes the transaction protocol. It does not define wire
 formats, opcodes, status codes or profiles, and must not change them.
 
 `SET_CONSTANT`, `XOR`, `MUL_NATIVE`, `DEREF` and `JUMP` are integrated in the
-host runtime. `BLAKE3` raises `UnsupportedCapability` naming the missing host
-service.
+host runtime. `BLAKE3` program execution still raises `UnsupportedCapability`
+naming the missing compiler/runtime integration. The transport-independent
+service codecs, official-library compression adapter, epoch binding, and model
+tests are available in `host/blake3_service.py`; they intentionally do not
+claim a production transport or RTL service path.