use nebu::{Fp3, Goldilocks};

use super::*;
use crate::recursion::circuit::builder::Builder;
use crate::recursion::ops::Ops;

#[test]
fn the_wrap_constraint_graph_compiles_to_the_circuit_constraints() {
    for mode in [Mode::Inner, Mode::Final] {
        graph_case(mode);
    }
}

fn graph_case(mode: Mode) {
    let air = CircuitAir::default();
    let (g, k) = g_graph(&air, mode);
    let w = View(&air, mode).width();
    let e = |i: u64| {
        Fp3::new(
            Goldilocks::new(i * 7 + 1),
            Goldilocks::new(i * i + 11),
            Goldilocks::new(3 * i + 2),
        )
    };
    let x: Vec<Fp3> = (0..g_inputs(w) as u64).map(e).collect();
    let mut out = vec![Fp3::ZERO; k];
    let (local, rest) = x.split_at(w);
    let (next, rest) = rest.split_at(w);
    let (pubs, rest) = rest.split_at(pre::COUNT + PIN);
    View(&air, mode).eval_with(local, next, pubs, rest[0], rest[1], &mut out);
    let mut want = Fp3::ZERO;
    let mut m = Fp3::ONE;
    for c in out {
        want += m * c;
        m *= rest[2];
    }
    assert_eq!(g.eval(&x), vec![want]);
    let mut b = Builder::new(true);
    let ins: Vec<_> = x.iter().map(|&v| b.witness(v)).collect();
    let outs = crate::recursion::expr::compile(&mut b, &g, &ins);
    assert_eq!(b.value(outs[0]), want);
    eprintln!(
        "wrap G ({mode:?}): {k} constraints, {} nodes, {} gates",
        g.nodes.len(),
        b.gates.len()
    );
}

#[test]
fn every_ledger_row_of_the_wrap_profiles_reaches_128_bits() {
    let base = crate::execution::succinct::params_for(20);
    for (rate, pow, n, mode, reads) in [
        (4u8, 16u8, 16usize, Mode::Inner, 0usize),
        (6, 24, 16, Mode::Inner, 0),
        (8, 24, 15, Mode::Inner, 0),
        (7, 22, 15, Mode::Inner, 0),
        (8, 30, 14, Mode::Final, 1 << 18),
        (9, 24, 14, Mode::Final, 1 << 18),
        (9, 26, 14, Mode::Final, 1 << 18),
    ] {
        let mut whir = base;
        whir.log_inv_rate = rate;
        whir.pow_bits = pow;
        let params = WrapParams { whir, n, mode };
        let fresh = crate::accumulate::fresh_ood(&whir, n + CBITS).unwrap();
        let (groups, claims): (&[usize], usize) = if mode == Mode::Inner {
            (&[1, 1, 2], 2 * (fresh + 1) + 2)
        } else {
            (&[1], fresh + 3)
        };
        let cfg = whir::Config::derive(&whir, n + CBITS, groups, claims).unwrap();
        let constraints = View(&CircuitAir::default(), mode).constraints();
        for (name, bits) in ledger(&params, &cfg, constraints, reads) {
            eprintln!("rate 1/{} {mode:?}: {name:40} {bits:8.2}", 1u32 << rate);
            assert!(bits >= 128.0, "{name}: {bits}");
        }
    }
}

#[test]
fn a_coefficient_applies_as_the_field_product() {
    let e = |i: u64| {
        Fp3::new(
            Goldilocks::new(i * 7 + 1),
            Goldilocks::new(i * i + 11),
            Goldilocks::new(3 * i + 2),
        )
    };
    let t = Fp3::new(Goldilocks::ZERO, Goldilocks::ONE, Goldilocks::ZERO);
    for i in 0..5 {
        let v = e(i);
        for c in [Fp3::ONE, t, t * t, e(9)] {
            assert_eq!(Coef::of(c).apply(v), c * v);
        }
    }
    assert_eq!(Coef::of(t), Coef::T);
    assert_eq!(Coef::of(t * t), Coef::T2);
}

/// The shipped chain's outermost proof is โ‰ค 64 KiB over every transcript
/// (a hard bound from the key's shapes, not a measurement), and the bound
/// is tight: a proof whose queries share no Merkle node reaches it.
#[test]
fn the_shipped_final_proof_is_at_most_64_kib_over_every_transcript() {
    use crate::recursion::ivc;
    let mut whir = crate::execution::succinct::params_for(20);
    whir.log_inv_rate = 4;
    whir.pow_bits = ivc::SHIPPED_POW;
    let ikey = ivc::key(&whir, 15).unwrap();
    let mut prev: Option<WrapKey> = None;
    for l in super::SHIPPED.split(',') {
        let mut parts = l.split(':');
        let head = parts.next().unwrap();
        let (rate, mode) = head.split_at(head.len() - 1);
        let mut w = whir;
        w.log_inv_rate = rate.parse().unwrap();
        w.pow_bits = parts.next().unwrap().parse().unwrap();
        let params = WrapParams {
            whir: w,
            n: 0,
            mode: if mode == "f" {
                Mode::Final
            } else {
                Mode::Inner
            },
        };
        prev = Some(match &prev {
            None => super::derive_shape_ivc(params, &ikey).unwrap(),
            Some(p) => super::derive_shape(params, p).unwrap(),
        });
    }
    let k = prev.unwrap();
    let max = super::max_proof_bytes(&k);
    eprintln!("shipped final proof โ‰ค {max} B");
    assert!(max <= super::MAX_FINAL_BYTES, "{max}");
}

/// The sibling bound is exact: leaves spread over distinct subtrees at
/// every level reach it.
#[test]
fn the_size_bound_is_the_worst_case_encoding() {
    use crate::recursion::whir::wire::max_siblings;
    use crate::recursion::word::Arity;
    // the sibling bound is reached by leaves spread over distinct subtrees
    for (q, d) in [(1usize, 5usize), (3, 6), (8, 10), (24, 25), (5, 3)] {
        // leaves in distinct subtrees at every level they can be
        let top = q.next_power_of_two().trailing_zeros() as usize;
        let spread: Vec<usize> = if top <= d {
            (0..q)
                .map(|i| nebu::ntt::bit_reverse(i, top as u32) << (d - top))
                .collect()
        } else {
            (0..1 << d).collect()
        };
        let mut spread = spread;
        spread.sort_unstable();
        let q = spread.len();
        let mut known = spread.clone();
        let mut sib = 0;
        for _ in 0..d {
            let mut par: Vec<usize> = known.iter().map(|x| x / 2).collect();
            par.dedup();
            sib += 2 * par.len() - known.len();
            known = par;
        }
        assert_eq!(sib, max_siblings(q, d, Arity::Two), "{q} {d}");
    }
}

Homonyms

neural/trident/src/neural/tests.rs
cyb/honeycrisp/aruminium/src/tests.rs
soft3/radio/iroh-blobs/src/tests.rs
warriors/trisha/rs/lower/tests.rs
neural/trident/src/deploy/tests.rs
soft3/crate/src/wallet/tests.rs
soft3/lens/cli/src/tests.rs
soft3/crate/src/genesis/tests.rs
neural/trident/src/verify/solve/tests.rs
neural/trident/src/package/hash/tests.rs
cyb/wysm/crates/wasmi/src/tests.rs
soft3/zheng/rs/src/accumulate/tests.rs
soft3/zheng/rs/src/air/tests.rs
neural/trident/src/package/registry/tests.rs
neural/trident/src/verify/sym/tests.rs
cyb/honeycrisp/aruminium/src/render/tests.rs
neural/trident/src/syntax/format/tests.rs
neural/trident/src/verify/smt/tests.rs
neural/trident/src/syntax/grammar/tests.rs
neural/trident/src/config/scaffold/tests.rs
warriors/trisha/rs/cost/stack_verifier/tests.rs
soft3/radio/quinn/quinn-udp/tests/tests.rs
soft3/radio/cyber-bao/src/tree/tests.rs
cyb/honeycrisp/unimem/src/block/tests.rs
neural/trident/src/lsp/semantic/tests.rs
neural/trident/src/package/manifest/tests.rs
soft3/radio/cyber-bao/src/group/tests.rs
cyb/wysm/crates/cli/src/tests.rs
soft3/crate/src/chain/pool/tests.rs
soft3/cybernode/rs/src/genesis/tests.rs
soft3/zheng/rs/src/envelope/tests.rs
soft3/zheng/rs/src/machine/tests.rs
soft3/cybernode/rs/src/wallet/tests.rs
neural/trident/src/verify/synthesize/tests.rs
warriors/trisha/rs/lower/legalize/tests.rs
neural/trident/src/syntax/lexer/tests.rs
cyb/wysm/crates/collections/src/tests.rs
neural/trident/src/verify/equiv/tests.rs
neural/trident/src/lsp/util/tests.rs
neural/trident/src/verify/report/tests.rs
soft3/crate/src/chain/economy/tests.rs
soft3/radio/quinn/quinn/src/tests.rs
neural/trident/src/config/resolve/tests.rs
neural/trident/src/package/store/tests.rs
soft3/zheng/rs/src/execution/veil/tests.rs
soft3/zheng/rs/src/execution/zk/tests.rs
warriors/erga/rs/mine-bench/src/texture_ffi/tests.rs
neural/trident/src/ir/tir/stack/tests.rs
cyb/wysm/crates/core/src/memory/tests.rs
cyb/evy/forks/bevy_ecs/src/bundle/tests.rs
warriors/erga/rs/rtable-bench/src/probe/tests.rs
soft3/radio/quinn/quinn-proto/src/range_set/tests.rs
cyb/wysm/crates/core/src/table/tests.rs
warriors/erga/rs/blake-bench/src/batch/tests.rs
soft3/crate/src/chain/net/kernel/tests.rs
soft3/zheng/rs/src/recursion/circuit/tests.rs
soft3/zheng/rs/src/recursion/whir/tests.rs
soft3/cybernode/rs/src/chain/economy/tests.rs
neural/trident/src/neural/data/tir_graph/tests.rs
neural/trident/src/ir/tir/optimize/tests.rs
soft3/zheng/rs/src/execution/tagged/tests.rs
warriors/erga/rs/rtable-bench/src/table/tests.rs
warriors/erga/rs/mine-bench/src/owner/tests.rs
soft3/cybernode/rs/src/chain/pool/tests.rs
soft3/zheng/rs/src/ccs/universal/tests.rs
cyb/wysm/crates/wasmi/src/instance/tests.rs
soft3/zheng/rs/src/execution/disclosed/stream/tests.rs
cyb/evy/forks/naga/src/front/wgsl/tests.rs
cyb/wysm/crates/wasmi/src/module/instantiate/tests.rs
soft3/bbg/rs/src/storage/application/transfer/tests.rs
soft3/zheng/rs/src/execution/disclosed/evaluation/tests.rs
warriors/erga/rs/mine-bench/src/cli/timed/tests.rs
cyb/wysm/crates/wasmi/src/engine/limits/tests.rs
soft3/cybernode/rs/src/chain/net/kernel/tests.rs
soft3/zheng/rs/src/execution/veil/hiding/tests.rs
soft3/zheng/rs/src/execution/disclosed/memory/tests.rs

Graph