binius_ip_prover/fracaddcheck/
mod.rs

1// Copyright 2025-2026 The Binius Developers
2
3//! Fractional-addition check: proving a claim about a sum of fractions.
4//!
5//! A witness is a numerator column beside a denominator column, one fraction $N_i/D_i$ per leaf.
6//! The check reduces a claim on the sum of those fractions to a claim on the witness itself.
7//! Two sibling fractions add by
8//!
9//! $$\frac{a_0}{b_0} + \frac{a_1}{b_1} = \frac{a_0b_1 + a_1b_0}{b_0b_1}$$
10//!
11//! so a circuit is a tree of layers, each half the width of the one below it.
12//! One layer costs an MLE-check over the four column halves, then a line-fold.
13//!
14//! A batch runs one uniform layer schedule, so every tree in it must be of the same depth.
15//! Zero-fraction padding lifts a shallower tree to the batch's depth.
16//! The extra leaf positions hold $0/1$, the additive identity, so the tree's own sum is unchanged.
17//! The verifier is oblivious to that padding and never learns the individual depths.
18//! No padded witness is materialized: a layer's messages are corrected in $O(1)$ per round.
19//!
20//! One file per concern:
21//!
22//! - `fraction.rs` — the numerator/denominator pair that every layer and every claim carries.
23//! - `circuit.rs` — the materialized layers of one tree, and the loop that proves them.
24//! - `driver.rs` — the batched layer schedule, in four steps per layer.
25//! - `padding.rs` — the unequal-depth policy: pad lengths, equality weights, and unpadding.
26//! - `zero_pad_mle.rs` — the wrapper that corrects one padded layer's MLE-check messages.
27//!
28//! One layout decision is worth stating, because the obvious alternative is slower.
29//! Each instance of a batched layer keeps its own column store and its own round pass.
30//! Folding them into one store reads as the natural use of that type and costs 1.5-2x:
31//! it trades a fat parallel region per instance for chunk parallelism over a far larger set.
32
33mod circuit;
34mod driver;
35pub mod fraction;
36pub mod padding;
37pub mod zero_pad_mle;
38
39pub use circuit::FracAddCircuit;
40pub use driver::{BatchProveOutput, batch_prove_unequal_depths};
41pub use padding::unpad_leaf_claim;
42
43pub use crate::sumcheck::frac_add_mle::LayerProver;
binius_ip_prover/fracaddcheck/mod.rs

binius_ip_prover/fracaddcheck/
mod.rs
