logicaffeine_compile/codegen_ana/
int_lane.rs

1//! The certified-EXACT integer lane — small-range integer dataflow with the ADC as restorer.
2//!
3//! Integer programs extract as integer ALU cells (`Arith`), and their constants are VALUES
4//! (`Src::Const(7)` is seven, not a bit pattern) — the mirror image of the float lane's
5//! conventions. The tile vocabulary is unchanged: integer add/sub is the weighted Kirchhoff
6//! sum, integer-constant multiply a programmed gain, variable×variable the four-quadrant
7//! multiplier. What is NEW is the claim: because every weight and constant is an integer, the
8//! region is GRID-PRESERVING, and when the compiler's error budget proves **ε < ½ grid step**
9//! ([`super::exactness_gate`]) the rounded readout is EXACTLY the VM's integer — a stronger
10//! statement than the float lane's ε-≡, purchased with the grid's slack. Division, remainder,
11//! and every bitwise op refuse: quotient grids are unforgiving and bit patterns are not
12//! voltages.
13
14use crate::ast::stmt::{Stmt, TypeExpr};
15use crate::codegen_sva::fabric_rtl::{decision_fabric_from_source, AluOp, FuncUnit, LoopCell, Src};
16use std::collections::BTreeMap;
17
18use super::cell::{ASrc, AnalogCell, AnalogNetlist};
19use super::lower::{gate_on_target, source_without_range_contracts, MappedCell, NetRef};
20use super::target::AnalogTarget;
21use super::{assumed_ranges_in, AnaLowerError};
22
23/// Map ONE integer fabric cell to an analog tile — the int-lane sibling of `map_float_cell`.
24/// `asrc` must decode `Src::Const` as an integer VALUE.
25pub(crate) fn map_int_cell(
26    cell: &LoopCell,
27    asrc: &dyn Fn(&Src) -> ASrc,
28) -> Result<MappedCell, AnaLowerError> {
29    Ok(match cell {
30        LoopCell::Arith {
31            op: AluOp::Add,
32            a,
33            b,
34        } => MappedCell::Tile(AnalogCell::Sum {
35            inputs: vec![asrc(a), asrc(b)],
36            weights: vec![1.0, 1.0],
37        }),
38        LoopCell::Arith {
39            op: AluOp::Sub,
40            a,
41            b,
42        } => MappedCell::Tile(AnalogCell::Sum {
43            inputs: vec![asrc(a), asrc(b)],
44            weights: vec![1.0, -1.0],
45        }),
46        LoopCell::Arith {
47            op: AluOp::Mul,
48            a,
49            b,
50        } => {
51            let (aa, bb) = (asrc(a), asrc(b));
52            MappedCell::Tile(match (aa, bb) {
53                (ASrc::Const(k), other) | (other, ASrc::Const(k)) => {
54                    AnalogCell::GainConst { a: other, k }
55                }
56                _ => AnalogCell::Mul { a: aa, b: bb },
57            })
58        }
59        LoopCell::Arith { op, .. } => {
60            return Err(AnaLowerError::UnloweredOp(format!(
61                "integer op {op:?} has no voltage semantics (a bit pattern is not a voltage)"
62            )))
63        }
64        LoopCell::Func {
65            unit: FuncUnit::DivS | FuncUnit::ModS | FuncUnit::FloorDivS,
66            ..
67        } => return Err(AnaLowerError::UnloweredOp(
68            "integer division/remainder (no exact analog divider — quotient grids are unforgiving)"
69                .to_string(),
70        )),
71        LoopCell::Func { unit, .. } => {
72            return Err(AnaLowerError::UnloweredOp(format!(
73                "functional unit {unit:?} has no exact integer analog tile"
74            )))
75        }
76        LoopCell::Select { cmp, ca, cb, t, e } => {
77            use crate::codegen_sva::fabric_rtl::CmpKind;
78            let (x, y, tt, ff) = match cmp {
79                CmpKind::Lt | CmpKind::Le => (asrc(ca), asrc(cb), asrc(t), asrc(e)),
80                CmpKind::Gt | CmpKind::Ge => (asrc(cb), asrc(ca), asrc(t), asrc(e)),
81                CmpKind::Eq | CmpKind::Ne => {
82                    return Err(AnaLowerError::UnloweredOp(
83                        "equality select: a continuous comparator has no measure-zero decision"
84                            .to_string(),
85                    ))
86                }
87            };
88            return Ok(super::lower::MappedCell::Tiles(vec![
89                AnalogCell::Sum {
90                    inputs: vec![x, y],
91                    weights: vec![1.0, -1.0],
92                },
93                AnalogCell::Select {
94                    c: ASrc::Val(super::lower::PREV_TILE),
95                    t: tt,
96                    f: ff,
97                },
98            ]));
99        }
100        LoopCell::MemRead { .. }
101        | LoopCell::HeapRead { .. }
102        | LoopCell::HeapWrite { .. }
103        | LoopCell::HeapAlloc { .. } => {
104            return Err(AnaLowerError::UnloweredOp(
105                "memory/state-plane access inside an analog region".to_string(),
106            ))
107        }
108        LoopCell::VectorArith { .. } => {
109            return Err(AnaLowerError::UnloweredOp(
110                "packed-SIMD op inside an analog region".to_string(),
111            ))
112        }
113    })
114}
115
116/// Lower an INTEGER function to an analog tile netlist realizable on `target`. The exactness
117/// claim itself is made downstream by [`super::exactness_gate`] over the scheduled budget.
118pub fn analog_int_netlist_from_source(
119    src: &str,
120    fn_name: &str,
121    target: &AnalogTarget,
122) -> Result<AnalogNetlist, AnaLowerError> {
123    check_int_params(src, fn_name)?; // ranges re-fetched by the schedule pass via `int_region_param_ranges`
124    let twin = source_without_range_contracts(src);
125    let df = decision_fabric_from_source(&twin, fn_name);
126    if df.escaped_first_return {
127        return Err(AnaLowerError::UnloweredOp(
128            "early-return branch shape: a branch continues past the first Return, and a \
129             tolerance-verified lane cannot detect a dropped branch — write the conditional \
130             as Let/Set so it if-converts"
131                .to_string(),
132        ));
133    }
134
135    let mut cells: Vec<AnalogCell> = Vec::new();
136    let mut map: BTreeMap<usize, NetRef> = BTreeMap::new();
137    let resolve_with = |map: &BTreeMap<usize, NetRef>, s: &Src| -> ASrc {
138        match s {
139            Src::In(k) => ASrc::In(*k),
140            // Integer constants are VALUES — the mirror of the float lane's bit-pattern decode.
141            Src::Const(c) => ASrc::Const(*c as f64),
142            Src::Val(v) => match map.get(v) {
143                Some(NetRef::Cell(c)) => ASrc::Val(*c),
144                Some(NetRef::Const(f)) => ASrc::Const(*f),
145                None => ASrc::Val(usize::MAX),
146            },
147        }
148    };
149    for (i, cell) in df.cells.iter().enumerate() {
150        let resolve = |s: &Src| resolve_with(&map, s);
151        let mapped = match map_int_cell(cell, &resolve)? {
152            MappedCell::Tile(t) => {
153                cells.push(t);
154                NetRef::Cell(cells.len() - 1)
155            }
156            MappedCell::Tiles(ts) => NetRef::Cell(super::lower::push_tiles(&mut cells, ts)),
157            MappedCell::Fold(v) => NetRef::Const(v),
158        };
159        map.insert(i, mapped);
160    }
161    let out = resolve_with(&map, &df.result);
162    if matches!(out, ASrc::Val(usize::MAX)) {
163        return Err(AnaLowerError::UnloweredOp(
164            "region output references an unlowered value".to_string(),
165        ));
166    }
167    let netlist = AnalogNetlist {
168        n_in: df.n_in,
169        cells,
170        out,
171    };
172    assert_grid_preserving(&netlist)?;
173    gate_on_target(&netlist, target)?;
174    Ok(netlist)
175}
176
177/// The grid-preservation guarantee: every weight and every constant is an integer, so integer
178/// inputs produce integer values on every net. An integer program cannot produce anything else
179/// through this lane's mapping — this check is the belt that makes the invariant loud.
180pub(crate) fn assert_grid_preserving(netlist: &AnalogNetlist) -> Result<(), AnaLowerError> {
181    let int_src = |s: &ASrc| match s {
182        ASrc::Const(c) => c.fract() == 0.0,
183        _ => true,
184    };
185    for cell in &netlist.cells {
186        let ok = match cell {
187            AnalogCell::Sum { inputs, weights } => {
188                weights.iter().all(|w| w.fract() == 0.0) && inputs.iter().all(int_src)
189            }
190            AnalogCell::GainConst { a, k } => k.fract() == 0.0 && int_src(a),
191            AnalogCell::Select { c, t, f } => int_src(c) && int_src(t) && int_src(f),
192            // Translinear outputs are irrational off the trivial points — never grid-preserving.
193            AnalogCell::Exp { .. }
194            | AnalogCell::Log { .. }
195            | AnalogCell::Tanh { .. }
196            | AnalogCell::Sqrt { .. }
197            | AnalogCell::Div { .. } => false,
198            AnalogCell::Mul { a, b } => int_src(a) && int_src(b),
199        };
200        if !ok {
201            return Err(AnaLowerError::UnloweredOp(
202                "non-integer weight/constant in an integer region — the grid would not be preserved".to_string(),
203            ));
204        }
205    }
206    Ok(())
207}
208
209/// The int region's declared per-parameter ranges, in parameter order, from its OWN body.
210pub(crate) fn int_region_param_ranges(
211    src: &str,
212    fn_name: &str,
213) -> Result<Vec<super::AssumedRange>, AnaLowerError> {
214    check_int_params(src, fn_name)
215}
216
217/// Gate 1: every parameter must be an integer with a declared integer range in the function body.
218/// Returns the ranges in parameter order.
219fn check_int_params(src: &str, fn_name: &str) -> Result<Vec<super::AssumedRange>, AnaLowerError> {
220    crate::ui_bridge::with_parsed_program(src, |parsed, interner| {
221        let (stmts, _types, _pol) = match parsed {
222            Ok(t) => t,
223            Err(advice) => {
224                return Err(AnaLowerError::UnloweredOp(format!(
225                    "parse failed: {advice}"
226                )))
227            }
228        };
229        let Some((params, body)) = stmts.iter().find_map(|s| match s {
230            Stmt::FunctionDef {
231                name, params, body, ..
232            } if interner.resolve(*name) == fn_name => Some((params, *body)),
233            _ => None,
234        }) else {
235            return Err(AnaLowerError::UnloweredOp(format!(
236                "function `{fn_name}` not found"
237            )));
238        };
239        let is_int = |t: &TypeExpr<'_>| {
240            matches!(t, TypeExpr::Primitive(s) | TypeExpr::Named(s)
241                if matches!(interner.resolve(*s), "Int" | "Nat"))
242        };
243        if params.is_empty() || !params.iter().any(|(_, t)| is_int(t)) {
244            return Err(AnaLowerError::NoAnalogRegion);
245        }
246        let ranges = assumed_ranges_in(body, interner);
247        let mut ordered = Vec::with_capacity(params.len());
248        for (p, t) in params.iter() {
249            let pname = interner.resolve(*p);
250            if !is_int(t) {
251                return Err(AnaLowerError::UnloweredOp(format!(
252                    "non-integer parameter `{pname}` in the integer lane"
253                )));
254            }
255            let Some(r) = ranges.iter().find(|r| r.var == pname) else {
256                return Err(AnaLowerError::UnboundedInput(format!(
257                    "parameter `{pname}` has no declared range (`Assume {pname} is between A and B.`)"
258                )));
259            };
260            if r.lo.fract() != 0.0 || r.hi.fract() != 0.0 {
261                return Err(AnaLowerError::UnboundedInput(format!(
262                    "parameter `{pname}`'s range [{}, {}] is not an integer range",
263                    r.lo, r.hi
264                )));
265            }
266            if r.lo > r.hi {
267                return Err(AnaLowerError::ContradictoryContract {
268                    var: r.var.clone(),
269                    lo: r.lo,
270                    hi: r.hi,
271                });
272            }
273            ordered.push(r.clone());
274        }
275        Ok(ordered)
276    })
277}
logicaffeine_compile/codegen_ana/int_lane.rs

logicaffeine_compile/codegen_ana/
int_lane.rs
