Module fabric_rtl

Expand description

fabric_rtl — Futamura’s first projection in silicon: “the specialized residual IS the circuit,” end-to-end from the REAL compiler.

PE(interp, program) = compiled_program: our compiler specializes the evaluator to a program, producing register bytecode with no interpreter dispatch (count_dispatch == 0, Jones-optimal). For a straight-line function that residual is a dispatch-free arithmetic trace. This module takes that actual compiled residual, lowers it register→SSA to a fixed spatial dataflow circuit — one functional unit per op, wired SSA-style, with NO program counter, NO fetch, NO opcode dispatch — and proves it THREE ways: bit-identically to the RUNNING VM under iverilog, across a BATTERY of distinct compiled programs directly against the VM, and — where the residual is multiply-free — EXHAUSTIVELY by our OWN certified SAT against an independent closed form. The circuit does not interpret the program; it is the program.

Width is 64-bit signed wrapping. The VM’s Int is arbitrary-precision, so the circuit is its fixed-width projection: it computes the VM’s EXACT result reduced mod 2^64, and that equality holds for EVERY input, overflow included (no range restriction — the low 64 bits always agree). Unbounded precision is the BigInt coprocessor’s domain (bignum_rtl). Straight-line residuals (+ - *) lower here; COUNTED LOOPS lower to a sequential CGRA — a fixed spatial body datapath streamed by a loop counter — in the LoopFabric section below.

Structs§

CfgBlock: One spatially-lowered basic block: a wired residual body + its live-in registers + the register writes it commits + its terminator.
DecisionFabric: A combinational decision datapath: SSA LoopCells (arith + predicated select) over the function parameters (Src::In), plus the Src that drives the single output.
FabricOp: One residual operation: v_i = a op b.
LoopFabric: A counted-loop residual lowered to a CGRA: a fixed BODY datapath (SSA over the current loop-carried state + the induction variable + loop invariants, INCLUDING predicated select tiles for data-dependent branches) driven by a sequential controller that clocks the state through the body once per induction value in the inclusive range lo..=hi.
NestedFabric: A perfectly-nested counted loop lowered to a HIERARCHICAL CGRA: an outer counter over the shared loop-carried state, whose body is the inner loop (its own body datapath + inner counter), whose range may reference the outer induction variable.
PipelinedLoop: A counted loop emitted in the pipelined accumulator form.
ProgramCfgFabric: A whole function lowered to spatial block islands + a block-sequencing controller.
WhileFabric: A while-loop residual lowered to a CGRA: a fixed body datapath streamed by a controller whose CONTINUE predicate is fabric-computed over the loop-carried state (no counter).
WholeProgramFabric: The whole-program fabric: a straight-line Main’s cells plus the ordered Srcs it Shows. Evaluating it yields the program’s output TAPE, compared against the VM’s stdout — this is what covers Show and validates the whole fabric end-to-end (calls inlined, collections/structs/enums on the shared heap).

Enums§

AluOp: The straight-line ALU ops a dispatch-free residual is built from (the alu.v ops, each already proven ≡ the VM). 64-bit signed, wrapping — bit-identical to the VM’s Int.
CmpKind: A signed comparison (the VM’s Int order) that gates a predicated select.
Divergence: Why a cell’s fixed-width value is not the value the VM computes for the same operands. The fabric’s arithmetic is the 64-bit projection of the VM’s; the VM is exact and total in a way no fixed-width datapath is, so every point where the two part is named here, and a checked evaluation reports it instead of producing the wrapped, zeroed or saturated word.
FuncUnit: A SEQUENTIAL functional unit — signed division and remainder. Unlike an AluOp, division is NOT a combinational tile: on silicon it is the multi-cycle shared_divider (already proven ≡ the VM by rtl.rs::the_signed_divider_is_proven_correct_by_our_sat), issued as a functional unit. Keeping it a distinct fabric cell lets the emitter wire that sequential unit rather than synthesize a giant combinational divider. Semantics mirror the soft-core’s shared_divider exactly, INCLUDING the divide-by-zero trap (b == 0 → 0).
LoopCell: One body cell of the CGRA fabric: an arithmetic tile, or a predicated SELECT (mux) tile whose comparison is folded in. A branch in the loop body is if-CONVERTED to a Select: both arms compute, the signed predicate selects — control becomes data, no divergence.
LoweringError: Why the whole-program fabric lowering refused a program. A TYPED failure surface: unsupported constructs return Err(LoweringError) from the try_* entry points instead of panicking, so callers (and the lowering_coverage_lock ratchet) can tell “this construct is not lowered yet” apart from a real bug. The Display strings are byte-identical to the old panic! messages, so the panicking wrappers are unchanged.
NestSrc: A range bound in the nested context: a circuit input, a constant, or the OUTER induction variable (so for j from 1 to i is expressible).
Src: An operand of a residual op: a circuit input (a function parameter), a prior SSA value, or a compile-time constant (already specialized in by the partial evaluator).
Term: A basic block’s terminator: where control goes after the block’s body runs.

Constants§

POLY_BODY: The demonstration residual: a degree-3 polynomial in Horner form, 2x³ + 5x² − 3x + 100. Straight-line (+ - *), so the compiler residualizes it dispatch-free.
STATE_PLANE_HEAP_WORDS: The heap-word budget for a state-plane kernel: enough words for the largest collection any vector touches (a generous fixed LUTRAM — collections in these kernels are a handful of words; addresses index the low clog2(HEAP) bits, so an in-bounds pointer always resolves). Kept a power of two for clean address slicing.
W: The 64-bit datapath width — the VM’s Int is i64, so the circuit wraps identically.

Functions§

decision_fabric_from_source: The Futamura P1 lowering for a branchy decision. Compile src, take function fn_name’s straight-line-with-branches body (entry .. Return), and if-convert it to a combinational select-DAG: parameters become circuit inputs, every If a Select. Panics on a shape outside the compare/arith/branch family (the honest boundary — loops map to a CGRA, division to a separate functional unit).
decision_fabric_has_state: True iff the fabric carries a state-plane (heap) cell — i.e. it must be lowered by emit_state_plane_verilog (sequenced) rather than emit_decision_fabric_verilog (combinational).
decision_fabric_is_float_arith: True iff the fabric is a pure FLOAT-arithmetic datapath (its cells are all FuncUnit float ops over float/Val operands) — lowered by emit_float_datapath_verilog. It must end in a float result (no FFloorF float→int bridge here — the caller floors the streamed f64 downstream) and carry no heap.
decision_fabric_is_pow: True iff the fabric is a pure POWER datapath (every cell is a FuncUnit::Pow) — lowered by emit_pow_datapath_verilog. Pow cannot settle combinationally (FuncUnit::verilog refuses it), so a Pow-bearing fabric takes this sequenced lane exactly as a float fabric takes the fpu.v lane.
emit_decision_fabric_testbench_dummy: A self-checking testbench for a COMBINATIONAL decision_{name} fabric: drive n input vectors (each n_in 64-bit words) from dec_{name}_in.hex, compare the settled result against the VM oracle in dec_{name}_out.hex, and print PASS/FAIL. The combinational analog of emit_state_plane_testbench — no clock, one #1 settle per vector. Lets any Func/Cmp/Arith decision tile be iverilog-exercised ≡ the VM.
emit_decision_fabric_verilog: Emit the decision as a fixed COMBINATIONAL dataflow circuit — one wire per SSA cell, arith and predicated-select tiles, no clock. 64-bit so its wrapping arithmetic is bit-identical to the VM.
emit_fabric_testbench: A self-checking testbench: drive N inputs, compare result against the VM oracle from fabric_{in,out}.hex. Prints PASS/FAIL. 64-bit values.
emit_fabric_verilog: Emit the residual as a fixed dataflow circuit — one combinational wire per SSA value, no PC / fetch / dispatch. result names the SSA value driving the output. 64-bit, so the circuit’s wrapping arithmetic is bit-identical to the VM’s Int.
emit_float_datapath_verilog: Lower a pure-float-arithmetic DecisionFabric to a SEQUENCED float datapath binding fpu.v (see the block comment above). Each cell is one multi-cycle FPU step; the streamed result is the f64 bit-pattern of the final float. Panics on any non-float-arith cell (the honest boundary — FFloorF/Arith are not bound here).
emit_loop_fabric_testbench: A self-checking testbench for the CGRA: for each recorded input vector, pulse reset, clock until done, and compare result against the VM oracle from cgra_{in,out}.hex.
emit_loop_fabric_verilog: Emit the CGRA as a SEQUENTIAL circuit: a combinational body datapath (one wire per SSA value + next-state) plus a controller that clocks the loop-carried state through it once per induction value in lo..=hi. No fetch, no opcode dispatch: the body is WIRED (spatial), the loop is a counter (temporal). done pulses when the loop is finished; result is the returned accumulator.
emit_loop_fabric_verilog_int8: Emit the CGRA RTL with an INT8-NATIVE datapath: every multiply tile’s operands are mul_bits-bit signed, so each MAC maps to exactly ONE DSP48E1 (a 25×18 signed multiplier) instead of the ~10 DSPs a 64×64 multiply decomposes into. The product is sign-extended back to the 64-bit accumulator, so the ADDS and the carried accumulator stay exact 64-bit — the result is byte-identical to the 64-bit fabric (and the VM) whenever the multiply operands fit in mul_bits (which the int8 model guarantees, and the ≡VM locks verify). This is the datapath that makes the spatial array DSP-packable and fast on real silicon.
emit_loop_fabric_verilog_pipelined: Emit the counted-loop CGRA with every accumulator in carry-save form and its terms pipelined ahead of it.
emit_nested_fabric_testbench: A self-checking testbench for the nested CGRA vs the VM oracle (nested_{name}_{in,out}.hex).
emit_nested_fabric_verilog: Emit the nested CGRA as a HIERARCHICAL FSM: an outer counter that, per iteration, sets up the inner range (from the outer iv) and runs the inner counter to completion, streaming the shared state through the inner body datapath. Three states — SETUP (arm inner for oi), RUN (inner iterates), and advance-outer — so the inner range recomputes correctly when the outer advances.
emit_pow_datapath_testbench: A self-checking testbench for a power datapath: for each of n input vectors, pulse rst, drive in{k}, run until done (bounded by max_cycles), and compare result against the VM oracle loaded from pow_{name}_{in,out}.hex. Mirrors emit_state_plane_testbench (the sequenced clocked harness).
emit_pow_datapath_verilog: Lower a pure-Pow DecisionFabric to a SEQUENCED power datapath (see the block comment above). Each cell is one b-step multiply loop over a shared accumulator; the streamed result is the final power. Panics on any non-Pow cell (the honest boundary — mixed lanes are a follow-on).
emit_seq_block_verilog: Emit a per-block SEQUENCED datapath (seqblk_{name}) for a CfgBlock: on a start pulse it walks the block’s SSA cells (combinational in one step, multi-cycle division/float via the shared units), then holds done high with every needed output (each register write’s Src, then the terminator operand) driven from the settled cell/register values. The block-walk sequencer starts it, waits done, latches the writes, and evaluates the terminator. Multi-cycle TILES are first-class here.
emit_seq_datapath_testbench: A self-checking CLOCKED testbench for a seq_{name} sequenced datapath: for each of n input vectors it pulses rst, waits for done, and checks result == the VM oracle (seq_{name}_out.hex). Multi-cycle tiles (the divider / FPU) make a vector take many clocks, so it spins on done with a generous timeout.
emit_seq_datapath_verilog: Emit a general SEQUENCED datapath over a DecisionFabric’s cells — the LATENCY-INSENSITIVE fabric. A combinational Arith/Select cell settles in one step; a Func DIVISION cell (DivS/ModS/FloorDivS) ISSUES the multi-cycle shared_divider and STALLS until its done (a variable-latency TILE). This is the same cell stream emit_decision_fabric_verilog wires as a pure combinational DAG, but with the sequential functional units as first-class multi-cycle tiles — so it composes with the fpu.v FPU (Phase B) and the block-walk sequencer (Phase C). Proven == eval_decision_fabric == the VM by iverilog. (Phase A: Arith/ Select/division; float/pow/mem are the following increments and PANIC here as the honest boundary.)
emit_seq_program_testbench: A self-checking clocked testbench for seqprog_{name}: per vector, load params, pulse rst, spin on done (multi-cycle tiles + the block walk take many clocks), and check result == the VM (seqprog_{name}_out.hex).
emit_seq_program_verilog: Emit the DONE-AWARE whole-program sequenced fabric (seqprog_{name}): the per-block sequenced datapaths (seqblk_*, each with multi-cycle division/float TILES) + a block-PC FSM that STARTS the current block, waits its done, latches the register writes, and takes the terminator (Jump/Branch/Return). This is the unification — one whole program (loop + division + float) on one spatial fabric, latency-insensitive. Proven == run_program_cfg_on_grid == the VM by iverilog.
emit_seqprog_soc_verilog: Emit a Nexys A7 SoC wrapper for the whole-program sequenced fabric: a baked vector ROM steps seqprog_{name} through each input (drive params → pulse the fabric reset → wait done → capture result), streaming a 12-byte record {0xA5, result[63:0] MSB-first, run_cycles[15:0], 0x5A} out the UART TX per vector, then looping. Slow /128 core clock (781.25 kHz) + power-on reset. vectors are the params per run (n_params each). This is the multi-cycle fabric (division + fpu.v tiles) on real silicon.
emit_state_plane_testbench: A self-checking testbench for a state-plane controller: for each of n input vectors, pulse rst, drive in{k}, run until done (bounded by max_cycles), and compare result against the VM oracle loaded from state_{name}_{in,out}.hex. Mirrors emit_loop_fabric_testbench (the CGRA clocked harness).
emit_state_plane_verilog: Lower a heap-bearing DecisionFabric to a SEQUENCED state-plane controller (see the block comment above). heap_words sizes the shared LUTRAM. Pure-compute cells render as combinational v{i} wires (over the LATCHED cell registers R[j]) latched per step; heap cells access the LUTRAM with a bump-pointer hp.
emit_while_fabric_testbench: A self-checking testbench for the while-CGRA: for each vector, pulse reset, clock until done, and compare result against the VM oracle from while_{name}_{in,out}.hex.
emit_while_fabric_verilog: Emit the while-CGRA as a SEQUENTIAL circuit: a combinational body datapath + a controller whose running flag is the FABRIC PREDICATE — evaluated on the init state (at reset) and on the next state (each step) to decide whether to keep iterating. No counter: the trip count is data.
eval_decision_fabric: Evaluate the decision DAG (arith + select, 64-bit wrapping) — the reference the emitted circuit is checked against, bit-identical to the VM’s Int.
eval_decision_fabric_heap: Evaluate a decision fabric that reads the shared HEAP (the state plane). heap mirrors the VM’s exact layout — a collection at pointer p is heap[p] = length then its elements at heap[p+1..=p+len] (1-based) — so this evaluation is bit-identical to the VM’s Int. A LoopCell::HeapRead reads heap[addr]; length of xs is HeapRead(p), item i of xs is HeapRead(p + i). Reads are pure given the input heap, so the fabric stays a combinational DAG (heap WRITES/ALLOC are the next increment).
eval_fabric: Evaluate the residual op-by-op (64-bit wrapping) — the reference the circuit is checked against, identical to the VM’s arithmetic.
eval_loop_body: Evaluate ONE execution of a loop fabric’s body over bin (the body-input convention: 0..n_state = the current state, n_state = the induction variable, then the invariants), returning every SSA value. The single oracle every pipelined / metapipelined model of the body is checked against.
eval_loop_fabric: Evaluate the CGRA op-by-op the way the sequential controller does: initialise the state, then for each induction value in lo..=hi apply the body and latch the next state. 64-bit wrapping — bit-identical to the VM’s Int reduced mod 2⁶⁴. This is the reference the emitted clocked circuit is checked against.
eval_loop_fabric_heap: Evaluate a FOREACH OVER A LOCAL HEAP LIST (seq_heap_ptr.is_some()). The prologue-heap island builds the list into a shared heap ONCE; then for each iv in 0..heap[list_ptr] the body runs with that heap THREADED — the element heap[list_ptr + 1 + iv] is destructured via HeapRead, and any collection op in the body reads/writes the same heap (so mutation across iterations persists). Bit-identical to the VM.
eval_loop_fabric_seq: Evaluate a loop fabric, supplying the iterated SEQUENCE’s element values when it is a sequence loop (seq_input.is_some()). The induction range is then 0..=seq.len()-1 (an empty seq runs zero iterations, exactly like the VM), and each LoopCell::MemRead reads seq[addr]. For a numeric range loop, seq is unused and the bounds come from lo/hi.
eval_nested_fabric: Evaluate the nested CGRA: the outer counter drives the inner loop to completion each iteration (the inner range may reference the outer iv). 64-bit wrapping — the VM’s Int mod 2⁶⁴.
eval_program_cfg_fabric: Evaluate a whole-function CFG fabric: seed the register file with params, then let the block-sequencing controller walk the graph — each block runs its wired residual over its live-in registers, commits its writes to the file, and its terminator predicate picks the successor — until a block returns. Equals the VM interpreting the same function (proven by fabric_cfg_lock).
eval_program_cfg_fabric_traced: The same walk, reporting the returned value AND the sequence of values SHOWN along the path taken.
eval_seq_program: The faithful MODEL of the whole-program SEQUENCED fabric (emit_seq_program_verilog): walk blocks by a PC, evaluating each block’s cells in order (threading ONE shared heap = the state plane) and taking the terminator (Jump/Branch/Return), exactly as the block-walk FSM does in RTL. This is the sequenced fabric’s own oracle — distinct from run_program_cfg_on_grid (which models the GRID realization and cannot place a looping heap body). Bit-identical to the VM’s Int for a lowered program. budget bounds the block walk (a loop that never returns panics, catching a lowering back-edge bug — never a silent hang).
eval_while_fabric: Evaluate the while-CGRA: initialise the state, then WHILE the fabric predicate holds apply the body and latch. 64-bit wrapping — the VM’s Int mod 2⁶⁴. A guard bounds non-termination.
eval_whole_program: Run a whole-program fabric to its output tape — each Shown value RENDERED as the VM would print it: a text char-list decoded to its string, an Int as decimal. The strings are compared to the VM’s stdout lines.
fabric_to_bounded: Lower a residual op-list to a BoundedExpr (bit-vector datapath) at the given width — the bridge that lets our certified SAT reason about the emitted circuit exhaustively.
function_op_names: The op mnemonics a function’s decision body USES (entry .. first Return) — the SAME segment decision_fabric_from_source lowers. This is the ground truth for “which ops a fabric built from this function actually exercises”, so a coverage-corpus program’s realized-op claim is welded to a program that genuinely contains the op (not merely declared).
loop_cell_delay: The logic depth of one body tile in the pipelined loop’s stage budget, in units of a 64-bit add.
loop_fabric_from_source: The genuine Futamura P1 lowering for a counted loop. Compile src, recover the range loop in function fn_name (a counted header and its unit step, or NewRange/IterPrepare/IterNext, and the back-edge Jump), and lower it to a LoopFabric: the loop-carried accumulators (state), the induction variable, the loop invariants, and the straight-line body (SSA). Panics on any shape outside the counted range-loop family (the honest boundary — nested loops / data-dependent exits are future work).
loop_next_to_bounded: Lower ONE loop-carried state register’s next-state (next[which]) to a BoundedExpr over the body inputs s0.., iv, inv0.. at the given width — so our certified SAT can prove the induction STEP (the body transition ≡ the VM’s per-iteration semantics) exhaustively.
nested_fabric_from_source: Recover the perfectly-nested loop in fn_name and lower it to a NestedFabric.
nested_inner_next_to_bounded: Lower ONE inner-body state register’s next-state to a BoundedExpr over s0.., ij, oi, inv0.. — for the certified inner body step (the base of the double induction).
poly_program: The full program, with Main chosen by the caller (Show poly(N).).
program_cfg_fabric: Panicking wrapper preserving the original contract for all existing callers: lowers fn_name’s CFG to a whole-program fabric, or panics with the same message the old code did. New code that wants to handle an unsupported construct gracefully should call try_program_cfg_fabric.
residual_from_source: The genuine Futamura P1 lowering. Compile src with the real compiler, take the straight-line register bytecode of function fn_name (its dispatch-free residual), and lower it register→SSA to a dataflow op-list. Parameters become circuit inputs; LoadConst becomes a baked-in constant; Add/Sub/Mul become wired functional units. Also returns the input arity (parameter count). Panics on a non-straight-line op (control flow / unsupported) — the honest boundary of this block.
try_emit_seq_datapath_verilog: Graceful entry to a single sequenced decision datapath: Ok(rtl) when every cell is register-only, or Err(StatePlaneUnlowered) for a heap-reading fabric (which belongs on the state-plane emitter). The typed companion to emit_seq_datapath_verilog.
try_emit_seq_program_verilog: Graceful entry to the whole-program sequenced fabric: Ok(rtl) when every block lowers (register tiles + the shared state plane for Seq/string programs), or Err(StatePlaneUnlowered) for the residual MemRead loop-sequence form. The typed companion to the panicking emit_seq_program_verilog.
try_main_cfg_fabric: Lower the top-level ## Main through the CFG engine.
try_program_cfg_fabric
while_fabric_from_source: Recover the while loop in fn_name and lower it to a WhileFabric. The header (the back-edge target) computes the continue predicate; the body (to the back-edge) if-converts.
while_next_to_bounded: Lower ONE while-body state register’s next-state to a BoundedExpr (over s0.., inv0..) for the certified body step. No induction variable in the body-input convention.
whole_program_fabric_from_program: Lower an already-COMPILED program to a whole-program fabric. Shared by the source path and by the HAND-AUTHORED-bytecode witnesses (codegen_sva/rtl.rs’s precedent): the reversible ALU ops (RevXor/RevNeg/RevAdd/RevSub) and the scheduler/CRDT-internal ops (ChanClose/CrdtJoin) that no LOGOS source emits are still real ISA ops the soft-core executes, so their fabric tile is proven by building a raw CompiledProgram (op + Show) and differencing the fabric tape against the VM oracle (Vm::new(&prog).run(); vm.output()) — never a hand-coded golden. Hand-authored bytecode carries no PolicyRegistry, so it runs with NO modeled conditions (a CheckPolicy in it would refuse loudly).
whole_program_fabric_from_source: Lower a program’s Main (code[0..] up to its terminating Halt) to a whole-program fabric. STRAIGHT-LINE only: a top-level branch would make a Show conditional, which the combinational output tape cannot honor, so it is refused loudly. Calls inside Main inline normally (their branches if-convert).
whole_program_op_names: Like function_op_names, but scans the WHOLE compiled program — all functions plus the module-init prologue. Used to weld coverage for a compiler-emitted op that a user function never directly contains: NewCrdt is emitted in a Shared struct’s default-fill, which runs in global struct-init, not the user function’s own op stream. So function_op_names(f) cannot surface it; this can.
with_seq_reserve: Run f with the per-collection reserve set to n (restored after). Use a small n for a program that fills its collections sequentially (e.g. the whole-transformer fabric engine) to right-size its heap.