The generated Honeycomb cell is not a raw SystemVerilog string. It is a Lean value
in a small RTL DSL. The emitter renders that value, and CI checks that the
checked-in rtl/honeycomb_cell.sv is exactly the renderer output.
The proof reaches the DSL value itself. Four theorem groups carry the execute
path:
cellExecCycle_refines_step relates the cycle model — a Lean transcription
of the cell's execute behavior — to the ISA step function: when the cell is
busy and not halted, one cycle commits exactly the ISA's architectural state
for the decoded instruction at pc.
cellExec_refines_execDecoded closes the gap that used to be bridged by eye:
it takes the generated AST's execute statement tree (cellExecStmts, the
very case_ opcode tree embedded in the emitted honeycomb_cell,
honeycomb_cell_sync, honeycomb_cell_pipe, and both net cells), runs it
under a width- and signedness-aware statement semantics with its read-stage
wires pinned to the model's reads, and proves the committed program counter,
accumulator, kernel pointers, halt flag, and every register equal
execDecoded's — for every opcode, every ALU funct, and all states.
cellRead_refines_envOf discharges that pinning: the base cell's
combinational read/decode stage (cellReadAssigns, the assign items the
emitted module embeds, in module order), evaluated from nothing but the
sequential state and the encoded 32-bit instruction word, computes exactly
the values the exec theorem consumes. Field extraction is proved against the
encoding layer, and the evaluation semantics carries the one rule the exec
stage never needed — SystemVerilog's sign-extending widening assignment, the
difference between a correct negative immediate and a silently zero-extended
one. The residual boundary is the SRAM read-port contract
rdata = mem[raddr], and cellRead_sram_addresses proves the stage drives
each raddr with exactly the model's wrapped index. The st/stw memory
effects — invisible to the exec case tree, which only commits registers —
are covered by cellRead_store_port/cellRead_weight_port: enable, wrapped
address, and stored (element-truncated) value are the model's.
cellMacExecC_mac/cellMacExecC_kmac cover the one tree the base theorem
does not: the mac and fpipe cells accumulate the drained two-stage
multiplier output prod instead of a combinational product. With prod
pinned to the model's product for the committing instruction (the value the
run-level pipeline invariants maintain), the prod arms commit exactly
execDecoded's state; the fpipe tree is proved equal to the mac tree
(cellFpipeArms_eq_macArms), and beyond mac/kmac the dispatch is proved
to select the very same arm ASTs the base-cell theorem evaluates
(macExec_selects_shared, cellMacArms_tail_shared) — those shared-arm
evaluations are not duplicated under the prod overlay.
Preparing the AST-level theorem surfaced two real divergences the golden suites
had never exercised — stw halted five of the six cell variants instead of
writing weight memory, and the model's funct decode read the full immediate
where the hardware cases on its low four bits — both fixed before the theorem
could close (review R3).
The trusted text renderer below the DSL value is intentionally small. What
remains outside these theorems: the honeycomb_sram adapter's read-port
contract (rdata = mem[raddr] — a few-line module, golden-tested, with its
address inputs proved above), the sequential wrapper around the exec tree
(reset/start/phase control, covered by the run-level theorems against the
cycle model), and a parser-level guarantee about external SystemVerilog
tooling, which remains a documented non-goal.
