Module fabric_config 

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

ConfigTable

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 by block_config(k).

ConfigWord

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, prove config == k ⇒ the ONE reconfigurable array ≡ island k, for ALL inputs (bounded at width). Returns the per-config verdicts — all true ⇒ the config word losslessly selects any datapath on one physical array.

compile_to_config_table

Compile a set of (source, function-name) datapaths to a ConfigTable: if-convert each function to a single-output decision island, place it on the tile array, then PAD every island to the common max_rows × max_cols so they share ONE reconfigurable array. width is the datapath width for the SAT proof; cfg_width must index all datapaths ((1 << cfg_width) >= sources.len()).

eval_config_table

Evaluate the reconfigurable array configured as datapath k on inputs. Because the reconfig proof certifies config == k ⇒ array ≡ island k, the array’s output IS island k’s — so this evaluates the placed island directly. The result is the value the physical fabric would drive when its config word is block_config(k).