Module gain 

Gain scaling + the range-safety certificate — the compiler side of the analog trust story.

Values on nets are MATH-domain quantities; voltage is 2^e · math under a single power-of-two block scale e chosen so the largest net magnitude fits the usable rail half-span (headroom · (rail_hi − rail_lo) / 2, differential-symmetric around mid-rail). Powers of two keep every certificate multiplication exact in f64 and make the ADC descale a bit shift. With a common scale, Sum weights ride unchanged, a GainConst is the same ratio in both domains (gated against the target’s realizable range), and the four-quadrant Mul divides by a programmed V_ref = 2^e so its output returns to the block scale — the standard translinear normalization.

The produced RangeCertificate carries per-net math and volt bounds from directed-outward interval propagation over the DECLARED input ranges. It is judged by the INDEPENDENT replay checker in logicaffeine_proof::interval_replay (this producer converts to the checker’s neutral vocabulary via to_range_claim) — the checker trusts nothing computed here.

Structs

GainSchedule

The per-program gain schedule: one block scale for every net, the exact ADC descale, the REALIZABLE multiplier reference, and the weight-quantized twin of the netlist (weights snapped to the target’s unit elements — what the silicon actually programs).

MathBound

A directed-outward f64 interval — the same arithmetic the independent checker replays.

NetBound

One net’s certified bounds.

RangeCertificate

The range-safety certificate: per-net bounds + the physical envelope they were proven against. Independently judged by logicaffeine_proof::interval_replay::check_range_claim via to_range_claim; nothing here is trusted by the checker.

Functions

scale_pass

Run the gain-scaling pass: propagate declared ranges, choose the block scale, gate realizable ratios, and emit the schedule + certificate. ranges is one AssumedRange per plane input, in input order (the caller resolves parameter names to input indices).

to_range_claim

Convert a netlist + schedule + certificate into the INDEPENDENT checker’s neutral vocabulary. The producer’s only role here is faithful translation; the judgment belongs to logicaffeine_proof::interval_replay::check_range_claim.