logicaffeine_compile/codegen_sva/
fabric_config.rs

1//! fabric_config — Phase D: the config-driven reconfigurable grid = THE INTERPRETER.
2//!
3//! Phase 5 (`fabric_reconfig_lock`) proved ONE tile array becomes any of several SAME-SHAPE datapaths under
4//! a config word. The honest gap it left is the **same-shape constraint**: the fabrics had to be hand-crafted
5//! to identical dimensions. Phase D closes it. A DIVERSE set of program datapaths — different sizes, different
6//! tile mixes (arithmetic, branch/select, comparison) — is each if-converted to a single-output island,
7//! PADDED to a common `rows × cols` ([`pad_grid`], purely additive), and placed on ONE reconfigurable array.
8//! A per-datapath CONFIG WORD (its index in the table, streamed from the `LGB1` bytecode frame) selects which
9//! datapath the array computes. Proven by our certified SAT (Z3-free): for EACH config value `k`,
10//! `config == k ⇒ the array's output ≡ island k`, for ALL inputs — so projecting the whole program set onto
11//! ONE physical fabric is SEMANTICS-PRESERVING. This is "send the bytes down the wire and the tiled fabric
12//! runs them", now for an arbitrary program corpus rather than a same-shape triple.
13//!
14//! Boundary (honest): each corpus datapath is a single-output island (a function if-converted to a
15//! select-DAG). A single function's INTERNAL multi-output basic blocks streamed as separate configs — the
16//! multi-output reconfigurable block walk — is the natural follow-on; the config-table core (one array,
17//! any datapath, padded, certified) is what this module and `fabric_whole_program_lock` prove.
18
19use super::fabric_grid::{
20    eval_grid, grid_to_bounded, pad_grid, route_loop_body, time_mux_n_bounded, Grid,
21};
22use super::fabric_rtl::decision_fabric_from_source;
23
24/// A configuration word: the index of the datapath the array is currently configured to compute. Streamed
25/// per datapath from the bytecode frame — the config table is the projection of the program onto the array.
26#[derive(Clone, Copy, Debug, PartialEq, Eq)]
27pub struct ConfigWord(pub u64);
28
29/// The config word that selects datapath / block `k`. (Trivial today — the index — but the named seam is
30/// where a richer encoding, e.g. an interned block id, would live.)
31pub fn block_config(block: usize) -> ConfigWord {
32    ConfigWord(block as u64)
33}
34
35/// A program corpus compiled to ONE reconfigurable tile array: every datapath placed as a same-shape island
36/// (all padded to `rows × cols`), plus the datapath widths for the certified reconfig proof. `grids[k]` is
37/// the island selected by `block_config(k)`.
38#[derive(Clone, Debug)]
39pub struct ConfigTable {
40    /// One island per datapath, ALL padded to the common array shape so they co-reside.
41    pub grids: Vec<Grid>,
42    /// The array's common dimensions (every `grids[k]` has these).
43    pub rows: usize,
44    pub cols: usize,
45    /// The datapath bit width for the reconfig SAT proof.
46    pub width: u32,
47    /// The config-word bit width (`ceil(log2(n))`), so `time_mux_n_bounded` selects among all islands.
48    pub cfg_width: u32,
49}
50
51/// Compile a set of `(source, function-name)` datapaths to a [`ConfigTable`]: if-convert each function to a
52/// single-output decision island, place it on the tile array, then PAD every island to the common
53/// `max_rows × max_cols` so they share ONE reconfigurable array. `width` is the datapath width for the SAT
54/// proof; `cfg_width` must index all datapaths (`(1 << cfg_width) >= sources.len()`).
55pub fn compile_to_config_table(
56    sources: &[(&str, &str)],
57    width: u32,
58    cfg_width: u32,
59) -> ConfigTable {
60    assert!(
61        !sources.is_empty(),
62        "a config table needs at least one datapath"
63    );
64    assert!(
65        (1usize << cfg_width) >= sources.len(),
66        "cfg_width {cfg_width} cannot index {} datapaths",
67        sources.len()
68    );
69    let raw: Vec<Grid> = sources
70        .iter()
71        .map(|(src, name)| {
72            let df = decision_fabric_from_source(src, name);
73            route_loop_body(&df.cells, df.n_in, &[df.result])
74        })
75        .collect();
76    let rows = raw.iter().map(|g| g.rows).max().unwrap();
77    let cols = raw.iter().map(|g| g.cols).max().unwrap();
78    let grids: Vec<Grid> = raw.iter().map(|g| pad_grid(g, rows, cols)).collect();
79    ConfigTable {
80        grids,
81        rows,
82        cols,
83        width,
84        cfg_width,
85    }
86}
87
88/// Certify the config table END TO END with our SAT: for EACH config value `k`, prove
89/// `config == k ⇒ the ONE reconfigurable array ≡ island k`, for ALL inputs (bounded at `width`). Returns the
90/// per-config verdicts — all `true` ⇒ the config word losslessly selects any datapath on one physical array.
91pub fn certify_config_table(table: &ConfigTable) -> Vec<bool> {
92    use super::bitblast::lower_bool_bounded;
93    use super::sva_to_verify::BoundedExpr;
94    use logicaffeine_proof::sat::{prove_unsat, UnsatOutcome};
95    use logicaffeine_proof::ProofExpr;
96
97    // The reconfig SAT lowers every grid's tiles to a BoundedExpr; a `Func` (division/float) tile has no
98    // bitblast lowering. A Func-bearing config table is proven by eval ≡ VM + iverilog (see fabric_soc_lock),
99    // not by this SAT — refuse it loudly here rather than panic opaquely inside `tile_bounded`.
100    assert!(
101        table.grids.iter().all(super::fabric_grid::grid_is_combinational),
102        "certify_config_table: the table has a Func (division/float) tile — a Func-bearing config table is \
103         proven by eval + iverilog, not by our SAT reconfig cert"
104    );
105    let refs: Vec<&Grid> = table.grids.iter().collect();
106    (0..table.grids.len())
107        .map(|k| {
108            let combined = time_mux_n_bounded(&refs, k as u64, table.width, table.cfg_width);
109            let island = grid_to_bounded(&table.grids[k], table.width);
110            // config == k  ⇒  array ≡ island k, for ALL inputs: prove ¬(array == island) is UNSAT.
111            // ★ THE BUDGET IS A LEGITIMATE OUTCOME HERE, SO IT GETS A SENTENCE RATHER THAN AN `.expect`.
112            // `lower_bool` returns `None` past the blast ceiling, and this used to `.expect("bitvec
113            // equality lowers to a boolean")` — a message that tells a reader nothing about why a table
114            // that certified yesterday stopped today. A per-config verdict has no room to carry a reason,
115            // so this refuses the way the Func case above refuses: loudly, naming the cause, the size and
116            // the proof path that does cover it.
117            let eq = match lower_bool_bounded(&BoundedExpr::Eq(Box::new(combined), Box::new(island))) {
118                Ok(e) => e,
119                Err(why) => panic!(
120                    "certify_config_table: config {k} of {} could not be bit-blasted within the ceiling \
121                     ({why:?}) — the reconfig SAT materialises a time-mux of every grid against island {k}, \
122                     so a table this wide is proven by eval + iverilog (see fabric_soc_lock) rather than by \
123                     this SAT, or the ceiling is raised deliberately with a measurement behind it",
124                    table.grids.len()
125                ),
126            };
127            prove_unsat(&ProofExpr::Not(Box::new(eq))) == UnsatOutcome::Refuted
128        })
129        .collect()
130}
131
132/// Evaluate the reconfigurable array configured as datapath `k` on `inputs`. Because the reconfig proof
133/// certifies `config == k ⇒ array ≡ island k`, the array's output IS `island k`'s — so this evaluates the
134/// placed island directly. The result is the value the physical fabric would drive when its config word is
135/// [`block_config`]`(k)`.
136pub fn eval_config_table(table: &ConfigTable, k: usize, inputs: &[i64]) -> i64 {
137    eval_grid(&table.grids[k], inputs)
138}
logicaffeine_compile/codegen_sva/fabric_config.rs

logicaffeine_compile/codegen_sva/
fabric_config.rs
