Expand description
fabric_config — Phase D: the config-driven reconfigurable grid = THE INTERPRETER.
Phase 5 (fabric_reconfig_lock) proved ONE tile array becomes any of several SAME-SHAPE datapaths under
a config word. The honest gap it left is the same-shape constraint: the fabrics had to be hand-crafted
to identical dimensions. Phase D closes it. A DIVERSE set of program datapaths — different sizes, different
tile mixes (arithmetic, branch/select, comparison) — is each if-converted to a single-output island,
PADDED to a common rows × cols (pad_grid, purely additive), and placed on ONE reconfigurable array.
A per-datapath CONFIG WORD (its index in the table, streamed from the LGB1 bytecode frame) selects which
datapath the array computes. Proven by our certified SAT (Z3-free): for EACH config value k,
config == k ⇒ the array's output ≡ island k, for ALL inputs — so projecting the whole program set onto
ONE physical fabric is SEMANTICS-PRESERVING. This is “send the bytes down the wire and the tiled fabric
runs them”, now for an arbitrary program corpus rather than a same-shape triple.
Boundary (honest): each corpus datapath is a single-output island (a function if-converted to a
select-DAG). A single function’s INTERNAL multi-output basic blocks streamed as separate configs — the
multi-output reconfigurable block walk — is the natural follow-on; the config-table core (one array,
any datapath, padded, certified) is what this module and fabric_whole_program_lock prove.
Structs§
- Config
Table - A program corpus compiled to ONE reconfigurable tile array: every datapath placed as a same-shape island
(all padded to
rows × cols), plus the datapath widths for the certified reconfig proof.grids[k]is the island selected byblock_config(k). - Config
Word - A configuration word: the index of the datapath the array is currently configured to compute. Streamed per datapath from the bytecode frame — the config table is the projection of the program onto the array.
Functions§
- block_
config - The config word that selects datapath / block
k. (Trivial today — the index — but the named seam is where a richer encoding, e.g. an interned block id, would live.) - certify_
config_ table - Certify the config table END TO END with our SAT: for EACH config value
k, proveconfig == k ⇒ the ONE reconfigurable array ≡ island k, for ALL inputs (bounded atwidth). Returns the per-config verdicts — alltrue⇒ the config word losslessly selects any datapath on one physical array. - compile_
to_ config_ table - Compile a set of
(source, function-name)datapaths to aConfigTable: if-convert each function to a single-output decision island, place it on the tile array, then PAD every island to the commonmax_rows × max_colsso they share ONE reconfigurable array.widthis the datapath width for the SAT proof;cfg_widthmust index all datapaths ((1 << cfg_width) >= sources.len()). - eval_
config_ table - Evaluate the reconfigurable array configured as datapath
koninputs. Because the reconfig proof certifiesconfig == k ⇒ array ≡ island k, the array’s output ISisland k’s — so this evaluates the placed island directly. The result is the value the physical fabric would drive when its config word isblock_config(k).