1use crate::circuit::{Circuit, Comparison, OpKind, OutOfRange, RoundingPointKind};
7use crate::numeric::{
8 EXACT_GRID_STEPS, Range, fround, largest_grid, lowest_power_of_two, pow2, power_of_two_exponent_at_least,
9 smallest_grid,
10};
11use crate::wire::{Lin, Term, Wire};
12
13pub fn emit_relu(circuit: &mut Circuit, value: Wire) -> Wire {
15 circuit.reglu(1.0, value)
16}
17
18pub fn emit_maximum(circuit: &mut Circuit, a: Wire, b: Wire) -> Wire {
21 let difference = circuit.round_affine(a - b);
22 let positive = emit_relu(circuit, difference);
23 let result = circuit.round_affine(b + positive);
24 let (a_range, b_range) = (circuit.range(a), circuit.range(b));
25 if a_range.min >= 0.0 && a_range.max <= 1.0 && b_range.min >= 0.0 && b_range.max <= 1.0 {
26 circuit.assume_range(result, 0.0, 1.0);
27 }
28 result
29}
30
31pub fn emit_minimum(circuit: &mut Circuit, a: Wire, b: Wire) -> Wire {
34 let difference = circuit.round_affine(a - b);
35 let positive = emit_relu(circuit, difference);
36 let result = circuit.round_affine(a - positive);
37 if circuit.is_non_negative(a)
38 && circuit.is_non_negative(b)
39 && circuit.range(a).is_finite()
40 && circuit.range(b).is_finite()
41 {
42 let maximum = fround(circuit.range(a).max);
43 circuit.assume_range(result, 0.0, maximum);
44 }
45 result
46}
47
48pub fn emit_select(circuit: &mut Circuit, gate: Wire, off: Wire, on: Wire) -> Wire {
50 circuit.select(gate, off, on)
51}
52
53pub fn emit_not(circuit: &mut Circuit, bit: Wire) -> Wire {
55 circuit.affine(1.0 - bit)
56}
57
58pub fn emit_and(circuit: &mut Circuit, bits: &[Wire]) -> Wire {
60 let sum = Lin::new(bits.iter().map(|&bit| (bit, 1.0)).collect(), 1.0 - bits.len() as f64);
61 circuit.reglu(1.0, sum)
62}
63
64pub fn emit_or(circuit: &mut Circuit, bits: &[Wire]) -> Wire {
66 let missing = Lin::new(bits.iter().map(|&bit| (bit, -1.0)).collect(), 1.0);
67 let none = circuit.relu(missing);
68 circuit.affine(1.0 - none)
69}
70
71pub fn emit_round(circuit: &mut Circuit, value: Wire) -> Wire {
75 const SHIFT: f64 = 12_582_912.0; let shifted = circuit.round_affine(value + SHIFT);
77 let rounded = circuit.round_affine(shifted - SHIFT);
78 circuit.mark_rounding_point(shifted);
79 circuit.mark_rounding_point(rounded);
80 rounded
81}
82
83#[derive(Copy, Clone, Debug, PartialEq, Eq)]
84pub enum Relation {
85 Greater,
86 AtLeast,
87 Less,
88 AtMost,
89 Equal,
90}
91
92impl Relation {
93 pub fn symbol(self) -> &'static str {
95 match self {
96 Relation::Greater => ">",
97 Relation::AtLeast => ">=",
98 Relation::Less => "<",
99 Relation::AtMost => "<=",
100 Relation::Equal => "==",
101 }
102 }
103
104 pub fn holds(self, a: f32, b: f32) -> bool {
106 match self {
107 Relation::Greater => a > b,
108 Relation::AtLeast => a >= b,
109 Relation::Less => a < b,
110 Relation::AtMost => a <= b,
111 Relation::Equal => a == b,
112 }
113 }
114}
115
116#[derive(Copy, Clone, Debug, Default)]
117pub struct CompareOptions {
118 pub end_with_boolean: bool,
122}
123
124#[derive(Copy, Clone, Debug, PartialEq, Eq)]
125enum SignTest {
126 Greater,
127 AtLeast,
128 Equal,
129}
130
131#[derive(Copy, Clone, Debug)]
132struct CompareOperand {
133 wire: Option<Wire>,
134 value: f64,
135 range: Range,
136 grid: Option<f64>,
137}
138
139fn compare_operand(circuit: &Circuit, operand: Wire) -> CompareOperand {
140 circuit.assert_wire(operand);
141 if let Some(constant) = circuit.constant_value(operand) {
142 let value = fround(constant);
143 assert!(value.is_finite(), "a constant comparison operand must be finite");
144 let value = if value == 0.0 { 0.0 } else { value };
146 return CompareOperand {
147 wire: None,
148 value,
149 range: Range::new(value, value),
150 grid: Some(if value == 0.0 { f64::INFINITY } else { lowest_power_of_two(value) }),
151 };
152 }
153 CompareOperand { wire: Some(operand), value: 0.0, range: circuit.range(operand), grid: circuit.grid(operand) }
154}
155
156pub fn emit_compare(circuit: &mut Circuit, a: Wire, relation: Relation, b: Wire) -> Wire {
162 emit_compare_with(circuit, a, relation, b, CompareOptions::default())
163}
164
165pub fn emit_compare_with(circuit: &mut Circuit, a: Wire, relation: Relation, b: Wire, options: CompareOptions) -> Wire {
166 let mut left = compare_operand(circuit, a);
167 let mut right = compare_operand(circuit, b);
168 if matches!(relation, Relation::Less | Relation::AtMost) {
169 std::mem::swap(&mut left, &mut right);
170 }
171 let test = match relation {
172 Relation::Greater | Relation::Less => SignTest::Greater,
173 Relation::AtLeast | Relation::AtMost => SignTest::AtLeast,
174 Relation::Equal => SignTest::Equal,
175 };
176 if left.wire.is_none() && right.wire.is_none() {
177 let holds = match test {
178 SignTest::Greater => left.value > right.value,
179 SignTest::AtLeast => left.value >= right.value,
180 SignTest::Equal => left.value == right.value,
181 };
182 return circuit.constant(if holds { 1.0 } else { 0.0 });
183 }
184 for operand in [left, right] {
185 assert!(
186 operand.range.is_finite(),
187 "emit_compare needs finite declared ranges on both operands, got {}..{}",
188 operand.range.min,
189 operand.range.max
190 );
191 }
192 if left.wire == right.wire {
194 return circuit.constant(if test == SignTest::Greater { 0.0 } else { 1.0 });
195 }
196 let difference_bound = (left.range.max - right.range.min).abs().max((left.range.min - right.range.max).abs());
197 assert!(fround(difference_bound).is_finite(), "the difference of the declared operand ranges can overflow FP32");
198 let mut terms: Vec<Term> = Vec::new();
199 if let Some(wire) = left.wire {
200 terms.push((wire, 1.0));
201 }
202 if let Some(wire) = right.wire {
203 terms.push((wire, -1.0));
204 }
205 let bias = left.value - right.value;
207 let bit = match emit_grid_compare(circuit, &left, &right, &terms, bias, test, options.end_with_boolean) {
208 Some(bit) => bit,
209 None => emit_cascade_compare(circuit, &terms, bias, fround(difference_bound), test, options.end_with_boolean),
210 };
211 circuit.assume_range(bit, 0.0, 1.0);
212 circuit.assume_grid(bit, 1.0);
213 if bit.index() >= circuit.source_size() {
214 let index = bit.index() - circuit.source_size();
215 circuit.operations[index].comparison_bit = true;
216 circuit.operations[index].comparison = Some(Comparison { terms, bias, equal: test == SignTest::Equal });
217 }
218 bit
219}
220
221fn largest_partial_sum(terms: &[Term], bias: f64, ranges: &[Range]) -> f64 {
224 let (mut minimum, mut maximum, mut largest) = (bias, bias, bias.abs());
225 for &(wire, coefficient) in terms {
226 let range = ranges[wire.index()];
227 let (low, high) = if coefficient >= 0.0 {
228 (coefficient * range.min, coefficient * range.max)
229 } else {
230 (coefficient * range.max, coefficient * range.min)
231 };
232 minimum += low;
233 maximum += high;
234 largest = largest.max(low.abs()).max(high.abs()).max(minimum.abs()).max(maximum.abs());
235 }
236 largest
237}
238
239fn scaled_terms(terms: &[Term], factor: f64) -> Vec<Term> {
240 terms.iter().map(|&(wire, coefficient)| (wire, coefficient * factor)).collect()
241}
242
243fn emit_grid_compare(
246 circuit: &mut Circuit,
247 left: &CompareOperand,
248 right: &CompareOperand,
249 terms: &[Term],
250 bias: f64,
251 test: SignTest,
252 end_with_boolean: bool,
253) -> Option<Wire> {
254 let grid = left.grid?.min(right.grid?);
255 let largest_steps = |circuit: &Circuit, sign: f64, offset: f64| {
256 largest_partial_sum(&scaled_terms(terms, sign / grid), sign * bias / grid + offset, &circuit.ranges)
257 };
258 let mut emitted = Vec::new();
259 let bit;
260 if end_with_boolean {
261 let score_scale = pow2(-24) / grid;
264 let fits = match test {
265 SignTest::Equal => {
266 largest_steps(circuit, 1.0, 0.0) <= pow2(22) && largest_steps(circuit, -1.0, 0.0) <= pow2(22)
267 }
268 _ => largest_steps(circuit, 1.0, if test == SignTest::Greater { -1.0 } else { 0.0 }) <= pow2(22),
269 };
270 if !(fits && score_scale >= smallest_grid() && score_scale <= largest_grid()) {
271 return None;
272 }
273 let mut emit_atom = |circuit: &mut Circuit, sign: f64, offset: f64| {
274 let score =
275 Lin::new(scaled_terms(terms, sign * score_scale), 0.5 + (sign * bias / grid - offset) * pow2(-24));
276 let atom = circuit.append(OpKind::Boolean, score, Lin::default(), true, None);
277 emitted.push(atom);
278 atom
279 };
280 if test == SignTest::Equal {
281 let at_least = emit_atom(circuit, 1.0, 0.0);
282 let at_most = emit_atom(circuit, -1.0, 0.0);
283 bit = circuit.reglu(1.0, at_least + at_most - 1.0);
284 emitted.push(bit);
285 } else {
286 bit = emit_atom(circuit, 1.0, if test == SignTest::Greater { 1.0 } else { 0.0 });
287 }
288 } else {
289 let scale = 1.0 / grid;
290 let fits = match test {
292 SignTest::Equal => {
293 largest_steps(circuit, 1.0, 0.0) < EXACT_GRID_STEPS
294 && largest_steps(circuit, -1.0, 0.0) < EXACT_GRID_STEPS
295 }
296 _ => largest_steps(circuit, -1.0, if test == SignTest::Greater { 1.0 } else { 0.0 }) < EXACT_GRID_STEPS,
297 };
298 if !(fits && scale <= largest_grid()) {
299 return None;
300 }
301 bit = emit_integer_bit(circuit, test, &mut emitted, |circuit, sign, offset| {
302 let ramp = Lin::new(scaled_terms(terms, sign * scale), sign * bias / grid + offset);
303 circuit.append(OpKind::Reglu, Lin::constant(1.0), ramp, true, None)
304 });
305 }
306 for wire in emitted {
307 circuit.record_rounding_point(wire, RoundingPointKind::IntegerBit);
308 }
309 Some(bit)
310}
311
312fn emit_integer_bit(
317 circuit: &mut Circuit,
318 test: SignTest,
319 emitted: &mut Vec<Wire>,
320 mut emit_ramp: impl FnMut(&mut Circuit, f64, f64) -> Wire,
321) -> Wire {
322 let ramps = if test == SignTest::Equal {
323 vec![emit_ramp(circuit, 1.0, 0.0), emit_ramp(circuit, -1.0, 0.0)]
324 } else {
325 vec![emit_ramp(circuit, -1.0, if test == SignTest::Greater { 1.0 } else { 0.0 })]
326 };
327 let bit = circuit.reglu(1.0, Lin::new(ramps.iter().map(|&ramp| (ramp, -1.0)).collect(), 1.0));
328 emitted.extend(ramps);
329 emitted.push(bit);
330 bit
331}
332
333const FULL_LIFT_EXPONENT: i32 = 149;
335const ROUNDING_STAGE_LIFT_EXPONENT: i32 = 104;
338
339#[derive(Copy, Clone, Debug, PartialEq)]
340struct CascadeStage {
341 scale: f64,
342 limit: f64,
343}
344
345fn plan_sign_cascade(difference_bound: f64, lift_exponent: i32) -> Vec<CascadeStage> {
349 let bound_exponent = power_of_two_exponent_at_least(difference_bound.max(smallest_grid()));
350 let mut stages = Vec::new();
351 let mut limit_exponent = bound_exponent;
352 let mut gain_exponent = 0;
353 while stages.is_empty() || limit_exponent > 0 || gain_exponent < lift_exponent {
354 let next_limit_exponent = (limit_exponent - 24).max(0);
355 let room = (24 + next_limit_exponent - limit_exponent).min(127);
357 let scale_exponent = room.min((lift_exponent - gain_exponent).max(0));
358 stages.push(CascadeStage { scale: pow2(scale_exponent), limit: pow2(next_limit_exponent) });
359 limit_exponent = next_limit_exponent;
360 gain_exponent += scale_exponent;
361 }
362 stages
363}
364
365struct Cascade {
366 difference: Wire,
367 difference_sign: f64,
368}
369
370impl Cascade {
371 fn emit_clamp_stages(
373 &self,
374 circuit: &mut Circuit,
375 sign: f64,
376 stages: &[CascadeStage],
377 emitted: &mut Vec<Wire>,
378 ) -> Wire {
379 let mut stage_output = self.difference;
380 for (index, &CascadeStage { scale, limit }) in stages.iter().enumerate() {
381 let (scaled_term, above_limit) = if index == 0 {
382 let gate: Vec<Term> = vec![(self.difference, sign * self.difference_sign * scale)];
384 let scaled_positive =
385 circuit.append(OpKind::Reglu, Lin::constant(1.0), Lin::new(gate.clone(), 0.0), true, None);
386 let above_limit = circuit.append(OpKind::Reglu, Lin::constant(1.0), Lin::new(gate, -limit), true, None);
387 emitted.push(scaled_positive);
388 ((scaled_positive, 1.0), above_limit)
389 } else {
390 let above_limit = circuit.reglu(1.0, stage_output * scale - limit);
391 ((stage_output, scale), above_limit)
392 };
393 stage_output = circuit.round_affine(Lin::new(vec![scaled_term, (above_limit, -1.0)], 0.0));
395 circuit.assume_range(stage_output, 0.0, limit);
396 emitted.push(above_limit);
397 emitted.push(stage_output);
398 }
399 stage_output
400 }
401}
402
403fn emit_cascade_compare(
404 circuit: &mut Circuit,
405 terms: &[Term],
406 bias: f64,
407 difference_bound: f64,
408 test: SignTest,
409 end_with_boolean: bool,
410) -> Wire {
411 let mut emitted = Vec::new();
412 let cascade = if bias == 0.0 && terms.len() == 1 {
415 Cascade { difference: terms[0].0, difference_sign: terms[0].1 }
416 } else {
417 let difference = circuit.round_affine(Lin::new(terms.to_vec(), bias));
418 emitted.push(difference);
419 Cascade { difference, difference_sign: 1.0 }
420 };
421 let lift = if end_with_boolean { ROUNDING_STAGE_LIFT_EXPONENT } else { FULL_LIFT_EXPONENT };
422 let stages = plan_sign_cascade(difference_bound, lift);
423 let bit;
424 if end_with_boolean {
425 let score_scale = pow2(22);
426 if test == SignTest::Greater {
427 let stage_output = cascade.emit_clamp_stages(circuit, 1.0, &stages, &mut emitted);
428 let just_below_half = 0.5 - pow2(-25);
430 let score_above_zero = circuit.reglu(1.0, stage_output * score_scale + just_below_half);
431 let score_above_one = circuit.reglu(1.0, stage_output * score_scale + (just_below_half - 1.0));
432 let score = circuit.affine(score_above_zero - score_above_one);
433 circuit.assume_range(score, 0.0, 1.0);
434 emitted.push(score_above_zero);
435 emitted.push(score_above_one);
436 bit = circuit.boolean(score);
437 } else {
438 let mut gate = vec![(cascade.emit_clamp_stages(circuit, -1.0, &stages, &mut emitted), -score_scale)];
439 if test == SignTest::Equal {
440 gate.push((cascade.emit_clamp_stages(circuit, 1.0, &stages, &mut emitted), -score_scale));
441 }
442 let score = circuit.reglu(1.0, Lin::new(gate, 0.5));
443 emitted.push(score);
444 bit = circuit.boolean(score);
445 }
446 emitted.push(bit);
447 } else {
448 let final_scale = stages.last().unwrap().scale;
449 let clamp_stages = &stages[..stages.len() - 1];
450 if clamp_stages.is_empty() {
451 bit = emit_integer_bit(circuit, test, &mut emitted, |circuit, sign, offset| {
453 let gate = Lin::new(vec![(cascade.difference, sign * cascade.difference_sign * final_scale)], offset);
454 circuit.append(OpKind::Reglu, Lin::constant(1.0), gate, true, None)
455 });
456 } else if test == SignTest::Greater {
457 let stage = cascade.emit_clamp_stages(circuit, 1.0, clamp_stages, &mut emitted);
459 let not_greater = circuit.reglu(1.0, 1.0 - stage * final_scale);
460 bit = circuit.reglu(1.0, 1.0 - not_greater);
461 emitted.push(not_greater);
462 emitted.push(bit);
463 } else {
464 let mut gate = vec![(cascade.emit_clamp_stages(circuit, -1.0, clamp_stages, &mut emitted), -final_scale)];
465 if test == SignTest::Equal {
466 gate.push((cascade.emit_clamp_stages(circuit, 1.0, clamp_stages, &mut emitted), -final_scale));
467 }
468 bit = circuit.reglu(1.0, Lin::new(gate, 1.0));
469 emitted.push(bit);
470 }
471 }
472 for wire in emitted {
473 circuit.record_rounding_point(wire, RoundingPointKind::SignCascade);
474 }
475 bit
476}
477
478pub fn emit_minimum_exact(circuit: &mut Circuit, a: Wire, b: Wire) -> Wire {
481 let a_is_smaller = emit_compare(circuit, a, Relation::AtMost, b);
482 let a_range = compare_operand(circuit, a).range;
483 let b_range = compare_operand(circuit, b).range;
484 emit_select_operand(circuit, a_is_smaller, b, a, a_range.min.min(b_range.min), a_range.max.min(b_range.max))
485}
486
487pub fn emit_maximum_exact(circuit: &mut Circuit, a: Wire, b: Wire) -> Wire {
489 let a_is_larger = emit_compare(circuit, a, Relation::AtLeast, b);
490 let a_range = compare_operand(circuit, a).range;
491 let b_range = compare_operand(circuit, b).range;
492 emit_select_operand(circuit, a_is_larger, b, a, a_range.min.max(b_range.min), a_range.max.max(b_range.max))
493}
494
495pub fn emit_clamp_exact(circuit: &mut Circuit, value: Wire, minimum: Wire, maximum: Wire) -> Wire {
497 let at_least_minimum = emit_maximum_exact(circuit, value, minimum);
498 emit_minimum_exact(circuit, at_least_minimum, maximum)
499}
500
501fn emit_select_operand(circuit: &mut Circuit, bit: Wire, off: Wire, on: Wire, minimum: f64, maximum: f64) -> Wire {
504 let selected_on = circuit.reglu(on, bit);
505 let selected_off = circuit.reglu(off, 1.0 - bit);
506 let result = circuit.affine(selected_on + selected_off);
507 circuit.assume_range(result, minimum, maximum);
508 result
509}
510
511enum WinnerNode {
514 Leaf { mass: Wire, item: usize },
515 Pair { mass: Wire, left: Box<WinnerNode>, right: Box<WinnerNode> },
516}
517
518impl WinnerNode {
519 fn mass(&self) -> Wire {
520 match self {
521 WinnerNode::Leaf { mass, .. } | WinnerNode::Pair { mass, .. } => *mass,
522 }
523 }
524}
525
526enum ArgmaxNode {
527 Leaf { score: Wire, item: usize },
528 Pair { score: Wire, left_wins: Wire, left: Box<ArgmaxNode>, right: Box<ArgmaxNode> },
529}
530
531impl ArgmaxNode {
532 fn score(&self) -> Wire {
533 match self {
534 ArgmaxNode::Leaf { score, .. } | ArgmaxNode::Pair { score, .. } => *score,
535 }
536 }
537}
538
539fn pair_up<T>(level: Vec<T>, mut combine: impl FnMut(T, T) -> T) -> Vec<T> {
541 let mut next = Vec::with_capacity(level.len().div_ceil(2));
542 let mut nodes = level.into_iter();
543 while let Some(left) = nodes.next() {
544 match nodes.next() {
545 Some(right) => next.push(combine(left, right)),
546 None => next.push(left),
547 }
548 }
549 next
550}
551
552pub fn emit_argmax(circuit: &mut Circuit, scores: &[Wire], unit: Wire) -> (Vec<Wire>, Wire) {
559 assert!(!scores.is_empty(), "argmax needs at least one score");
560 let unit_range = circuit.range(unit);
561 assert!(unit_range.min == 1.0 && unit_range.max == 1.0, "argmax unit must equal one");
562 let mut level: Vec<ArgmaxNode> = scores
563 .iter()
564 .enumerate()
565 .map(|(item, &score)| {
566 let range = circuit.range(score);
567 assert!(range.min >= 0.0 && range.max <= 1.0, "argmax scores must be within zero and one");
568 ArgmaxNode::Leaf { score, item }
569 })
570 .collect();
571 while level.len() > 1 {
572 level = pair_up(level, |left, right| {
573 const COMPARISON_BIAS: f64 = 0.500_000_059_604_644_8;
575 const COMPARISON_SCALE: f64 = 0.499_999_940_395_355_2;
576 let comparison =
577 circuit.affine(left.score() * COMPARISON_SCALE - right.score() * COMPARISON_SCALE + COMPARISON_BIAS);
578 circuit.assume_range(comparison, 0.0, 1.0);
579 let left_wins = circuit.boolean(comparison);
580 let score = emit_select(circuit, left_wins, right.score(), left.score());
581 ArgmaxNode::Pair { score, left_wins, left: Box::new(left), right: Box::new(right) }
582 });
583 }
584 let root = level.pop().unwrap();
585 let score = root.score();
586 let mut selected = vec![unit; scores.len()];
587 route_argmax(circuit, root, unit, &mut selected);
588 circuit.assume_one_hot(&selected, false);
590 (selected, score)
591}
592
593fn route_argmax(circuit: &mut Circuit, node: ArgmaxNode, route: Wire, selected: &mut [Wire]) {
594 match node {
595 ArgmaxNode::Leaf { item, .. } => selected[item] = route,
596 ArgmaxNode::Pair { left_wins, left, right, .. } => {
597 let left_route = circuit.multiply(route, left_wins);
598 let right_route = circuit.affine(route - left_route);
599 circuit.assume_range(right_route, 0.0, 1.0);
600 route_argmax(circuit, *left, left_route, selected);
601 route_argmax(circuit, *right, right_route, selected);
602 }
603 }
604}
605
606pub fn emit_first_active(circuit: &mut Circuit, active: Wire, candidates: &[Wire]) -> Vec<Wire> {
613 if candidates.is_empty() {
614 return Vec::new();
615 }
616 let active_range = circuit.range(active);
617 assert!(active_range.min >= 0.0 && active_range.max <= 1.0, "winner selection must be gated within zero and one");
618 let mut level: Vec<WinnerNode> = candidates
619 .iter()
620 .enumerate()
621 .map(|(item, &mass)| {
622 let range = circuit.range(mass);
623 assert!(range.min >= 0.0 && range.max <= 1.0, "winner candidates must be within zero and one");
624 WinnerNode::Leaf { mass, item }
625 })
626 .collect();
627 while level.len() > 1 {
628 level = pair_up(level, |left, right| {
629 let mass = emit_maximum(circuit, left.mass(), right.mass());
630 WinnerNode::Pair { mass, left: Box::new(left), right: Box::new(right) }
631 });
632 }
633 let root = level.pop().unwrap();
634 let start = circuit.multiply(active, root.mass());
635 let mut selected = vec![start; candidates.len()];
636 route_winner(circuit, root, start, &mut selected);
637 if is_proven_bit(circuit, active) && candidates.iter().all(|&candidate| is_proven_bit(circuit, candidate)) {
640 let distinct = selected.iter().enumerate().all(|(index, wire)| !selected[..index].contains(wire));
641 if distinct {
642 circuit.assume_one_hot(&selected, true);
643 }
644 }
645 selected
646}
647
648fn route_winner(circuit: &mut Circuit, node: WinnerNode, route: Wire, selected: &mut [Wire]) {
649 match node {
650 WinnerNode::Leaf { item, .. } => selected[item] = route,
651 WinnerNode::Pair { left, right, .. } => {
652 let left_route = circuit.multiply(route, left.mass());
653 let right_route = circuit.affine(route - left_route);
654 circuit.assume_range(right_route, 0.0, 1.0);
655 route_winner(circuit, *left, left_route, selected);
656 route_winner(circuit, *right, right_route, selected);
657 }
658 }
659}
660
661pub fn is_proven_bit(circuit: &Circuit, wire: Wire) -> bool {
665 let mut pending = vec![wire];
666 let mut visited = Vec::new();
667 while let Some(current) = pending.pop() {
668 if visited.contains(¤t) {
669 continue;
670 }
671 visited.push(current);
672 if is_bit_by_construction(circuit, current) {
673 continue;
674 }
675 let Some(read) = circuit.operation(current).and_then(|operation| operation.index_read.as_ref()) else {
676 return false;
677 };
678 let candidates = &circuit.tables[read.table].candidates;
680 let count = candidates.len() as i64;
681 let lowest = (read.index_range.min.floor() as i64).clamp(-1, count);
682 let highest = (read.index_range.max.floor() as i64).clamp(-1, count);
683 for position in lowest.max(0)..=highest.min(count - 1) {
684 pending.push(candidates[position as usize]);
685 }
686 if lowest < 0 && read.below == OutOfRange::Clamp {
687 pending.push(candidates[0]);
688 }
689 if highest > count - 1 && read.above == OutOfRange::Clamp {
690 pending.push(candidates[candidates.len() - 1]);
691 }
692 }
693 true
694}
695
696fn is_bit_by_construction(circuit: &Circuit, wire: Wire) -> bool {
697 let range = circuit.range(wire);
698 if range.min == range.max && (range.min == 0.0 || range.min == 1.0) {
699 return true;
700 }
701 if let Some(operation) = circuit.operation(wire)
702 && (operation.kind == OpKind::Boolean || operation.comparison_bit)
703 {
704 return true;
705 }
706 circuit.one_hot_groups().iter().any(|group| group.members.contains(&wire))
707}
708
709#[cfg(test)]
710mod tests {
711 use super::*;
712
713 #[test]
714 fn cascade_plan_matches_handwired_comment() {
715 let scales: Vec<f64> =
717 plan_sign_cascade(16_384.0, FULL_LIFT_EXPONENT).iter().map(|stage| stage.scale.log2()).collect();
718 assert_eq!(scales, vec![10.0, 24.0, 24.0, 24.0, 24.0, 24.0, 19.0]);
719 assert!(plan_sign_cascade(16_384.0, FULL_LIFT_EXPONENT).iter().all(|stage| stage.limit == 1.0));
720 }
721}