logicaffeine_compile/codegen_ana/
reduction.rs

1//! The streamed reduction — the flagship MAC lane.
2//!
3//! A float-accumulator loop over a sequence (`Repeat for each x in xs: Set acc to acc + …`)
4//! becomes ONE analog tick datapath run once per element under the control plane's frame
5//! schedule: the element is validated (the `Assume` contract), DAC-driven, the plane settles,
6//! and the sample-and-hold commits the new accumulator — which LIVES IN ANALOG between frames,
7//! never re-quantized. Only the final accumulator crosses the ADC. That asymmetry (per-element
8//! DAC cost, one ADC, zero mid-stream conversions) is the analog win this lane exists to state.
9//!
10//! Semantics are sampled-data ZOH: each frame's update is exact arithmetic over the held
11//! element, so the ideal tier reproduces the VM's loop trajectory bit-for-bit, and the physical
12//! tier (converters + quantized weights) stays inside a budget ITERATED over the declared
13//! maximum frame count — which is why a `Assume length of xs is between A and B.` contract is
14//! REQUIRED: a budget over an unbounded stream would be a guess, and this lane does not guess.
15//!
16//! Extraction reuses the digital fabric's certified counted-loop front-end
17//! (`loop_fabric_from_source`, read-only) on the contract-free twin, exactly like the DAG lane.
18
19use std::collections::BTreeMap;
20
21use crate::ast::stmt::{Pattern, Stmt, TypeExpr};
22use crate::codegen_sva::fabric_rtl::{loop_fabric_from_source, LoopCell, Src};
23
24use super::cell::{ASrc, AnalogCell, AnalogNetlist};
25use super::control::{ControlProgram, CtrlStep};
26use super::error_budget::{outward_sum, ErrorSource, ErrorTerm, OutputBudget};
27use super::eval::eval_analog_dc;
28use super::gain::{
29    propagate_bounds, quantize_weights, select_scale, src_bound_of, GainSchedule, MathBound,
30    NetBound, RangeCertificate,
31};
32use super::lower::{map_float_cell, source_without_range_contracts, MappedCell, NetRef};
33use super::target::{AnaUnplaceable, AnalogCapability, AnalogCellKind, AnalogTarget};
34use super::{assumed_len_ranges_in, assumed_ranges_in, AnaLowerError, AssumedRange};
35
36/// A lowered streamed reduction. Tick-input convention: `In(0)` = the streamed element,
37/// `In(1)` = the held accumulator; `out` = the next accumulator value.
38#[derive(Clone, Debug, PartialEq)]
39pub struct AnalogReduction {
40    pub tick: AnalogNetlist,
41    /// The accumulator's initial value (a compile-time constant in this lane).
42    pub init: f64,
43    /// The declared length contract — the control plane schedules `max_len` frames.
44    pub min_len: usize,
45    pub max_len: usize,
46    /// The declared element range (each word validated before the DAC fires).
47    pub elem: AssumedRange,
48    pub control: ControlProgram,
49}
50
51/// Which numeric family a streamed lane carries — decides constant decoding (float bit
52/// patterns vs integer values), the cell mapper, and the grid-preservation obligation.
53#[derive(Clone, Copy, PartialEq, Eq)]
54enum Lane {
55    Float,
56    Int,
57}
58
59/// Lower `fn_name` (a single-`Seq of Float`-parameter accumulator loop) to a streamed analog
60/// reduction realizable on `target`.
61pub fn analog_reduction_from_source(
62    src: &str,
63    fn_name: &str,
64    target: &AnalogTarget,
65) -> Result<AnalogReduction, AnaLowerError> {
66    reduction_impl(src, fn_name, target, Lane::Float)
67}
68
69/// Lower a `Seq of Int` accumulator loop to a GRID-PRESERVING streamed reduction — the
70/// integer MAC. The exactness claim is made downstream by [`super::exactness_gate`] over the
71/// iterated budget.
72pub fn analog_int_reduction_from_source(
73    src: &str,
74    fn_name: &str,
75    target: &AnalogTarget,
76) -> Result<AnalogReduction, AnaLowerError> {
77    reduction_impl(src, fn_name, target, Lane::Int)
78}
79
80fn reduction_impl(
81    src: &str,
82    fn_name: &str,
83    target: &AnalogTarget,
84    lane: Lane,
85) -> Result<AnalogReduction, AnaLowerError> {
86    let (elem, min_len, max_len) = check_reduction_contracts(src, fn_name, lane)?;
87
88    let twin = source_without_range_contracts(src);
89    let lf = loop_fabric_from_source(&twin, fn_name);
90
91    // ── Shape gates: the single-accumulator streamed family. ──
92    if lf.seq_input.is_none() {
93        return Err(AnaLowerError::UnloweredOp(
94            "not a sequence loop (no streamed input)".to_string(),
95        ));
96    }
97    if lf.n_state != 1 {
98        return Err(AnaLowerError::UnloweredOp(format!(
99            "{} loop-carried accumulators (the streamed lane holds exactly one in the S&H)",
100            lf.n_state
101        )));
102    }
103    if !lf.epilogue.is_empty() || !lf.prologue_heap.is_empty() || !lf.invariants.is_empty() {
104        return Err(AnaLowerError::UnloweredOp(
105            "loop epilogue/prologue/invariants are not yet streamed".to_string(),
106        ));
107    }
108    let init = match lf.init[0] {
109        Src::Const(bits) => match lane {
110            Lane::Float => f64::from_bits(bits as u64),
111            Lane::Int => bits as f64,
112        },
113        _ => {
114            return Err(AnaLowerError::UnloweredOp(
115                "accumulator initial value must be a compile-time constant".to_string(),
116            ))
117        }
118    };
119
120    // ── Map the body: MemRead(iv) → the streamed element; state → the held accumulator. ──
121    // Body-input convention (LoopFabric): In(0) = state, In(1) = the induction variable.
122    for cell in &lf.body {
123        let uses_iv_as_value = |s: &Src| matches!(s, Src::In(k) if *k >= 1);
124        let illegal = match cell {
125            LoopCell::MemRead { .. } => false,
126            LoopCell::Arith { a, b, .. }
127            | LoopCell::Func { a, b, .. }
128            | LoopCell::VectorArith { a, b, .. } => uses_iv_as_value(a) || uses_iv_as_value(b),
129            LoopCell::Select { ca, cb, t, e, .. } => {
130                uses_iv_as_value(ca)
131                    || uses_iv_as_value(cb)
132                    || uses_iv_as_value(t)
133                    || uses_iv_as_value(e)
134            }
135            LoopCell::HeapRead { addr } => uses_iv_as_value(addr),
136            LoopCell::HeapWrite { addr, val } => uses_iv_as_value(addr) || uses_iv_as_value(val),
137            LoopCell::HeapAlloc { size } => uses_iv_as_value(size),
138        };
139        if illegal {
140            return Err(AnaLowerError::UnloweredOp(
141                "the induction variable used as a value (only the element stream is analog)"
142                    .to_string(),
143            ));
144        }
145    }
146
147    // Pre-mark the element wires: every `MemRead(iv)` IS tick input 0 (no tile, just the wire).
148    let mut map: BTreeMap<usize, NetRef> = BTreeMap::new();
149    for (i, cell) in lf.body.iter().enumerate() {
150        if let LoopCell::MemRead { addr } = cell {
151            if !matches!(addr, Src::In(1)) {
152                return Err(AnaLowerError::UnloweredOp(
153                    "sequence read off the stream head (only `xs[iv]` streams)".to_string(),
154                ));
155            }
156            map.insert(i, NetRef::Cell(usize::MAX)); // sentinel: the element wire, resolved as In(0)
157        }
158    }
159    let mut cells: Vec<AnalogCell> = Vec::new();
160    let resolve_with = |map: &BTreeMap<usize, NetRef>, s: &Src| -> ASrc {
161        match s {
162            Src::In(0) => ASrc::In(1), // the held accumulator
163            Src::In(_) => ASrc::In(1), // unreachable: iv-as-value gated above
164            Src::Const(bits) => ASrc::Const(match lane {
165                Lane::Float => f64::from_bits(*bits as u64),
166                Lane::Int => *bits as f64,
167            }),
168            Src::Val(v) => match map.get(v) {
169                Some(NetRef::Cell(c)) if *c == usize::MAX => ASrc::In(0), // the element wire
170                Some(NetRef::Cell(c)) => ASrc::Val(*c),
171                Some(NetRef::Const(f)) => ASrc::Const(*f),
172                None => ASrc::Val(usize::MAX),
173            },
174        }
175    };
176    for (i, cell) in lf.body.iter().enumerate() {
177        if matches!(cell, LoopCell::MemRead { .. }) {
178            continue;
179        }
180        let resolve = |s: &Src| resolve_with(&map, s);
181        let mapped = match lane {
182            Lane::Float => map_float_cell(cell, &resolve)?,
183            Lane::Int => super::int_lane::map_int_cell(cell, &resolve)?,
184        };
185        let mapped = match mapped {
186            MappedCell::Tile(t) => NetRef::Cell(push(&mut cells, t)),
187            MappedCell::Tiles(ts) => NetRef::Cell(super::lower::push_tiles(&mut cells, ts)),
188            MappedCell::Fold(v) => NetRef::Const(v),
189        };
190        map.insert(i, mapped);
191    }
192    let out = resolve_with(&map, &lf.next[0]);
193    if matches!(out, ASrc::Val(usize::MAX)) {
194        return Err(AnaLowerError::UnloweredOp(
195            "accumulator update references an unlowered value".to_string(),
196        ));
197    }
198    let tick = AnalogNetlist {
199        n_in: 2,
200        cells,
201        out,
202    };
203    if lane == Lane::Int {
204        super::int_lane::assert_grid_preserving(&tick)?;
205        if init.fract() != 0.0 {
206            return Err(AnaLowerError::UnloweredOp(
207                "non-integer accumulator initial value in the integer lane".to_string(),
208            ));
209        }
210    }
211
212    gate_reduction_on_target(&tick, target)?;
213
214    let control = ControlProgram {
215        frame: vec![
216            CtrlStep::LoadDac { ch: 0 },
217            CtrlStep::Settle,
218            CtrlStep::SampleHold,
219        ],
220        frames: max_len,
221        epilogue: vec![CtrlStep::ReadAdc { ch: 0 }],
222        tick_ns: target.settle_ns.0,
223    };
224    Ok(AnalogReduction {
225        tick,
226        init,
227        min_len,
228        max_len,
229        elem,
230        control,
231    })
232}
233
234fn push(cells: &mut Vec<AnalogCell>, c: AnalogCell) -> usize {
235    cells.push(c);
236    cells.len() - 1
237}
238
239/// Contract gates: one sequence parameter of the lane's element family with a declared LENGTH
240/// range, and a declared ELEMENT range on the loop variable (integer bounds for the int lane).
241fn check_reduction_contracts(
242    src: &str,
243    fn_name: &str,
244    lane: Lane,
245) -> Result<(AssumedRange, usize, usize), AnaLowerError> {
246    crate::ui_bridge::with_parsed_program(src, |parsed, interner| {
247        let (stmts, _types, _pol) = match parsed {
248            Ok(t) => t,
249            Err(advice) => {
250                return Err(AnaLowerError::UnloweredOp(format!(
251                    "parse failed: {advice}"
252                )))
253            }
254        };
255        let Some((params, body)) = stmts.iter().find_map(|s| match s {
256            Stmt::FunctionDef {
257                name, params, body, ..
258            } if interner.resolve(*name) == fn_name => Some((params, *body)),
259            _ => None,
260        }) else {
261            return Err(AnaLowerError::UnloweredOp(format!(
262                "function `{fn_name}` not found"
263            )));
264        };
265        if params.len() != 1 {
266            return Err(AnaLowerError::UnloweredOp(
267                "the streamed lane takes exactly one sequence parameter".to_string(),
268            ));
269        }
270        let (pname_sym, pty) = &params[0];
271        let pname = interner.resolve(*pname_sym);
272        let elem_matches = |s: &str| match lane {
273            Lane::Float => matches!(s, "Float" | "Real"),
274            Lane::Int => matches!(s, "Int" | "Nat"),
275        };
276        let is_lane_seq = matches!(
277            pty,
278            TypeExpr::Generic { base, params: ps }
279                if matches!(interner.resolve(*base), "Seq" | "List")
280                    && ps.len() == 1
281                    && matches!(&ps[0], TypeExpr::Primitive(s) | TypeExpr::Named(s)
282                        if elem_matches(interner.resolve(*s)))
283        );
284        if !is_lane_seq {
285            return Err(AnaLowerError::NoAnalogRegion);
286        }
287
288        let len_ranges = assumed_len_ranges_in(body, interner);
289        let Some(len) = len_ranges.iter().find(|r| r.var == pname) else {
290            return Err(AnaLowerError::UnboundedInput(format!(
291                "sequence `{pname}` has no declared length range (`Assume length of {pname} is between A and B.`) — \
292                 a budget over an unbounded stream would be a guess"
293            )));
294        };
295        if len.lo < 0 || len.hi < len.lo || len.hi == 0 {
296            return Err(AnaLowerError::UnboundedInput(format!(
297                "length range [{}, {}] is not a usable frame bound",
298                len.lo, len.hi
299            )));
300        }
301
302        // The loop variable's declared range = the element contract.
303        let loop_var = body.iter().find_map(|s| match s {
304            Stmt::Repeat {
305                pattern: Pattern::Identifier(v),
306                ..
307            } => Some(*v),
308            _ => None,
309        });
310        let Some(loop_var) = loop_var else {
311            return Err(AnaLowerError::UnloweredOp(
312                "no `Repeat for each` loop found".to_string(),
313            ));
314        };
315        let vname = interner.resolve(loop_var);
316        let ranges = assumed_ranges_in(body, interner);
317        let Some(elem) = ranges.iter().find(|r| r.var == vname) else {
318            return Err(AnaLowerError::UnboundedInput(format!(
319                "element `{vname}` has no declared range (`Assume {vname} is between A and B.`)"
320            )));
321        };
322        if lane == Lane::Int && (elem.lo.fract() != 0.0 || elem.hi.fract() != 0.0) {
323            return Err(AnaLowerError::UnboundedInput(format!(
324                "element `{vname}`'s range [{}, {}] is not an integer range",
325                elem.lo, elem.hi
326            )));
327        }
328        Ok((elem.clone(), len.lo as usize, len.hi as usize))
329    })
330}
331
332fn gate_reduction_on_target(
333    tick: &AnalogNetlist,
334    target: &AnalogTarget,
335) -> Result<(), AnaLowerError> {
336    let mut need = vec![
337        AnalogCapability::Cell(AnalogCellKind::SampleHold),
338        AnalogCapability::DacChannels(1),
339        AnalogCapability::AdcChannels(1),
340    ];
341    for cell in &tick.cells {
342        need.push(AnalogCapability::Cell(cell.kind()));
343    }
344    for cap in need {
345        if !target.provides(cap) {
346            return Err(AnaLowerError::Unplaceable(
347                AnaUnplaceable::MissingCapability {
348                    needed: cap,
349                    target: target.name,
350                },
351            ));
352        }
353    }
354    let n_mul = tick
355        .cells
356        .iter()
357        .filter(|c| matches!(c, AnalogCell::Mul { .. }))
358        .count();
359    if n_mul > 0 && !target.provides(AnalogCapability::MulTiles(n_mul)) {
360        return Err(AnaLowerError::Unplaceable(
361            AnaUnplaceable::MissingCapability {
362                needed: AnalogCapability::MulTiles(n_mul),
363                target: target.name,
364            },
365        ));
366    }
367    if tick.cells.len() > target.rows * target.cols {
368        return Err(AnaLowerError::Unplaceable(AnaUnplaceable::TooSmall {
369            needed_cells: tick.cells.len(),
370            target_rows: target.rows,
371            target_cols: target.cols,
372            target: target.name,
373        }));
374    }
375    Ok(())
376}
377
378/// Ideal sampled evaluation: the VM's loop trajectory, tick by tick (bit-exact — same f64 ops
379/// in the same order).
380pub fn eval_analog_sampled(r: &AnalogReduction, xs: &[f64]) -> f64 {
381    let mut acc = r.init;
382    for x in xs {
383        acc = eval_analog_dc(&r.tick, &[*x, acc]);
384    }
385    acc
386}
387
388/// The physical sampled tier: each element DAC-quantized on entry, the accumulator CONTINUOUS
389/// across frames (it lives in the S&H), one ADC quantization at the end — over the
390/// weight-quantized tick.
391pub fn eval_analog_sampled_quantized(
392    r: &AnalogReduction,
393    schedule: &GainSchedule,
394    target: &AnalogTarget,
395    xs: &[f64],
396) -> f64 {
397    let grid = super::eval::ConverterGrid::of(schedule, target);
398    let mut acc = r.init;
399    for x in xs {
400        acc = eval_analog_dc(&schedule.quantized, &[grid.dac_q(*x), acc]);
401    }
402    grid.adc_q(acc)
403}
404
405/// Schedule + certify the reduction: quantize the tick's weights, ITERATE the interval
406/// propagation over the declared maximum frame count (hulling per net), choose the block scale
407/// over the whole trajectory, and emit the certificate the independent checker replays with the
408/// same iteration.
409pub fn reduction_scale_pass(
410    r: &AnalogReduction,
411    target: &AnalogTarget,
412) -> Result<(GainSchedule, RangeCertificate), AnaLowerError> {
413    let quantized = quantize_weights(&r.tick, target)?;
414    let elem = MathBound {
415        lo: r.elem.lo,
416        hi: r.elem.hi,
417    };
418    let mut acc = MathBound {
419        lo: r.init,
420        hi: r.init,
421    };
422    let mut hulls: Vec<MathBound> = vec![
423        MathBound {
424            lo: f64::INFINITY,
425            hi: f64::NEG_INFINITY
426        };
427        quantized.cells.len()
428    ];
429    let mut acc_hull = acc;
430    for _ in 0..r.max_len {
431        let inputs = [elem, acc];
432        let bounds = propagate_bounds(&quantized.cells, &inputs)?;
433        for (h, b) in hulls.iter_mut().zip(&bounds) {
434            h.lo = h.lo.min(b.lo);
435            h.hi = h.hi.max(b.hi);
436        }
437        acc = src_bound_of(&quantized.out, &inputs, &bounds);
438        acc_hull.lo = acc_hull.lo.min(acc.lo);
439        acc_hull.hi = acc_hull.hi.max(acc.hi);
440        if !(acc.lo.is_finite() && acc.hi.is_finite()) {
441            return Err(AnaLowerError::UnloweredOp(
442                "accumulator range diverges over the declared frame count".to_string(),
443            ));
444        }
445    }
446    // An empty-body (identity) reduction leaves hulls untouched; normalize.
447    for h in hulls.iter_mut() {
448        if h.lo > h.hi {
449            *h = MathBound { lo: 0.0, hi: 0.0 };
450        }
451    }
452
453    let has_mul = quantized
454        .cells
455        .iter()
456        .any(|c| matches!(c, AnalogCell::Mul { .. }));
457    let input_bounds = vec![elem, acc_hull];
458    let all: Vec<MathBound> = input_bounds.iter().chain(hulls.iter()).copied().collect();
459    let scale_log2 = select_scale(&all, has_mul, target)?;
460    let s = f64::powi(2.0, scale_log2);
461
462    let mut per_net = Vec::with_capacity(hulls.len());
463    for b in &hulls {
464        per_net.push(NetBound {
465            math: *b,
466            volt_lo: (b.lo * s).next_down(),
467            volt_hi: (b.hi * s).next_up(),
468        });
469    }
470    let per_net_scale_log2 = vec![scale_log2; quantized.cells.len()];
471    let schedule = GainSchedule {
472        scale_log2,
473        out_descale_log2: -scale_log2,
474        mul_vref_v: s,
475        quantized,
476        per_net_scale_log2,
477    };
478    let cert = RangeCertificate {
479        input_bounds,
480        per_net,
481        rail_half_span_v: target.half_span_v(),
482        noise_floor_v: 0.0,
483        min_full_scale_over_noise: 1.0,
484    };
485    Ok((schedule, cert))
486}
487
488/// The reduction budget: the shared ε engine ITERATED over the declared maximum frame count —
489/// the element's DAC half-LSB enters every frame, the weight-snap deviation injects every
490/// frame, the accumulator's lanes carry, and one ADC half-LSB lands at the end.
491pub fn reduction_error_budget(
492    r: &AnalogReduction,
493    cert: &RangeCertificate,
494    schedule: &GainSchedule,
495    target: &AnalogTarget,
496) -> OutputBudget {
497    use super::error_budget::{eval_rounding_guard, half_lsb, out_lanes, propagate_eps_pass};
498    let dac_eps = half_lsb(cert, schedule, target.dac_bits);
499    let adc_eps = half_lsb(cert, schedule, target.adc_bits);
500    let bound_of = |src: &ASrc| -> MathBound {
501        match src {
502            ASrc::In(k) => cert.input_bounds[*k],
503            ASrc::Val(v) => cert.per_net[*v].math,
504            ASrc::Const(c) => MathBound { lo: *c, hi: *c },
505        }
506    };
507    // Lanes: 0 = element DAC, 1 = weight quant, 2 = Mul interaction; the accumulator carries.
508    let mut acc_eps = vec![0.0_f64; 3];
509    for _ in 0..r.max_len {
510        let carried = acc_eps.clone();
511        let input_eps = |src: &ASrc, lane: usize| -> f64 {
512            match src {
513                ASrc::In(0) if lane == 0 => dac_eps,
514                ASrc::In(0) => 0.0,
515                _ => carried[lane],
516            }
517        };
518        let input_total = |src: &ASrc| -> f64 {
519            match src {
520                ASrc::In(0) => dac_eps,
521                _ => outward_sum(carried.iter().copied()),
522            }
523        };
524        let pass = propagate_eps_pass(
525            &r.tick.cells,
526            &schedule.quantized.cells,
527            &bound_of,
528            3,
529            1,
530            2,
531            &input_eps,
532            &input_total,
533        );
534        acc_eps = out_lanes(&pass, &schedule.quantized.out, 3, &input_eps);
535    }
536
537    let mut terms = Vec::new();
538    if acc_eps[0] > 0.0 {
539        terms.push(ErrorTerm {
540            eps_math: acc_eps[0],
541            source: ErrorSource::DacQuant {
542                input: 0,
543                bits: target.dac_bits,
544            },
545        });
546    }
547    if acc_eps[1] > 0.0 {
548        terms.push(ErrorTerm {
549            eps_math: acc_eps[1],
550            source: ErrorSource::WeightQuant,
551        });
552    }
553    if acc_eps[2] > 0.0 {
554        terms.push(ErrorTerm {
555            eps_math: acc_eps[2],
556            source: ErrorSource::MulInteraction,
557        });
558    }
559    terms.push(ErrorTerm {
560        eps_math: adc_eps,
561        source: ErrorSource::AdcQuant {
562            bits: target.adc_bits,
563        },
564    });
565    terms.push(ErrorTerm {
566        eps_math: eval_rounding_guard(cert, r.max_len * schedule.quantized.cells.len()),
567        source: ErrorSource::EvalRounding,
568    });
569    let eps_math = outward_sum(terms.iter().map(|t| t.eps_math));
570    OutputBudget { eps_math, terms }
571}
logicaffeine_compile/codegen_ana/reduction.rs

logicaffeine_compile/codegen_ana/
reduction.rs
