From 5de589d25d7452849d22896bda16f0885ef64802 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 05:57:20 +0100 Subject: [PATCH 1/6] feat(labinius): runtime SIS admission, root profile and root shape --- CONTRIBUTING.md | 8 + crates/akita-params/Cargo.toml | 2 +- crates/akita-params/src/sis/labinius.rs | 19 +- .../src/sis/labinius/generated_width_table.rs | 81 +++++ .../src/sis/labinius/parity_tests.rs | 245 ++++++++++++++++ .../src/sis/labinius/root_profile.rs | 116 ++++++++ .../src/sis/labinius/root_profile_tests.rs | 118 ++++++++ .../src/sis/labinius/root_shape.rs | 277 ++++++++++++++++++ .../src/sis/labinius/root_shape_tests.rs | 136 +++++++++ .../src/sis/labinius/width_table.rs | 46 +++ .../src/sis/labinius/width_table_tests.rs | 115 ++++++++ .../examples/labinius_infinity_width_table.rs | 111 ++++++- .../tests/labinius_width_table.rs | 51 ++++ specs/labinius-root-admission.md | 174 +++++++++++ 14 files changed, 1488 insertions(+), 11 deletions(-) create mode 100644 crates/akita-params/src/sis/labinius/generated_width_table.rs create mode 100644 crates/akita-params/src/sis/labinius/parity_tests.rs create mode 100644 crates/akita-params/src/sis/labinius/root_profile.rs create mode 100644 crates/akita-params/src/sis/labinius/root_profile_tests.rs create mode 100644 crates/akita-params/src/sis/labinius/root_shape.rs create mode 100644 crates/akita-params/src/sis/labinius/root_shape_tests.rs create mode 100644 crates/akita-params/src/sis/labinius/width_table.rs create mode 100644 crates/akita-params/src/sis/labinius/width_table_tests.rs create mode 100644 specs/labinius-root-admission.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index be9bb25ce..816341718 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -89,6 +89,14 @@ cargo run -p akita-sis-estimator --release --features parallel \ --example infinity_width_table -- --format rust-split --profile local-minimum ``` +The opt-in LaBinius runtime table is emitted from the certified checked-in CSV, +without rerunning the lattice search: + +```bash +cargo run -p akita-sis-estimator --no-default-features --features labinius-sis \ + --example labinius_infinity_width_table -- --from-csv +``` + Sage workflows in [`scripts/sis_golden/README.md`](scripts/sis_golden/README.md) remain useful for pinned-estimator goldens and Euclidean comparison artifacts, but must not overwrite the production L-infinity table. diff --git a/crates/akita-params/Cargo.toml b/crates/akita-params/Cargo.toml index 80d32dc62..dc4e56d74 100644 --- a/crates/akita-params/Cargo.toml +++ b/crates/akita-params/Cargo.toml @@ -24,7 +24,7 @@ blake2 = "0.11.0" sha3 = "0.12.0" [features] -labinius-sis = [] +labinius-sis = ["akita-challenges/labinius-challenges"] # Selects the dev protocol: every wire-format change `dev` carries that `main` # does not, together. Off by default. Schedules priced for it live in # `artifacts/schedules-dev`. See docs/branches.md. diff --git a/crates/akita-params/src/sis/labinius.rs b/crates/akita-params/src/sis/labinius.rs index 843227920..27637797d 100644 --- a/crates/akita-params/src/sis/labinius.rs +++ b/crates/akita-params/src/sis/labinius.rs @@ -1,9 +1,20 @@ //! LaBinius binary-source SIS identities and exact collision accounting. //! -//! This module deliberately stops at the security-table boundary. It does not -//! make any binary ring a native Akita runtime ring and it does not admit a -//! schedule. Challenge sampling and its certified multiplication bound belong -//! to `akita-challenges`; callers pass that bound here explicitly. +//! The opt-in root profile and shape admit binary root geometry against the +//! certified runtime width table and exact challenge/response bounds. This does +//! not select a protocol or admit a complete schedule. Challenge sampling and +//! its certified multiplication bound belong to `akita-challenges`. + +mod generated_width_table; +mod root_profile; +mod root_shape; +mod width_table; + +pub use root_profile::LabiniusRootProfile; +pub use root_shape::LabiniusRootShape; +pub use width_table::{ + labinius_min_secure_rank, LabiniusWidthCell, LABINIUS_WIDTH_TABLE, LABINIUS_WIDTH_TABLE_DIGEST, +}; use akita_error::AkitaError; diff --git a/crates/akita-params/src/sis/labinius/generated_width_table.rs b/crates/akita-params/src/sis/labinius/generated_width_table.rs new file mode 100644 index 000000000..79974a0bf --- /dev/null +++ b/crates/akita-params/src/sis/labinius/generated_width_table.rs @@ -0,0 +1,81 @@ +// AUTO-GENERATED by labinius_infinity_width_table --from-csv -- do not edit by hand. +// Source: crates/akita-sis-estimator/data/labinius_infinity_width.csv + +use super::width_table::LabiniusWidthCell; +use super::{LabiniusCoefficientPrime, LabiniusRingDegree}; + +#[rustfmt::skip] +pub const LABINIUS_WIDTH_TABLE: &[LabiniusWidthCell] = &[ + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 24116880, max_width: 2 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 24641160, max_width: 2 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 24116880, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 24641160, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 1580547964560, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 1614907702920, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 24116880, max_width: 9 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 24641160, max_width: 9 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 1580547964560, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 1614907702920, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 24116880, max_width: 2 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 24641160, max_width: 2 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 24116880, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 24641160, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 1580547964560, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 1614907702920, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 24116880, max_width: 338378 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 24641160, max_width: 322958 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 1580547964560, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 1614907702920, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D486, rank: 1, coeff_linf_bound: 13107000, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D486, rank: 2, coeff_linf_bound: 13107000, max_width: 842036 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D486, rank: 2, coeff_linf_bound: 858993459000, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D486, rank: 3, coeff_linf_bound: 13107000, max_width: 93729198805 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D486, rank: 3, coeff_linf_bound: 858993459000, max_width: 7 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 24116880, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 24641160, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 24116880, max_width: 542538891 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 24641160, max_width: 518564323 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 1580547964560, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 1614907702920, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 3, coeff_linf_bound: 1580547964560, max_width: 21782 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D648, rank: 3, coeff_linf_bound: 1614907702920, max_width: 20775 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D972, rank: 1, coeff_linf_bound: 13107000, max_width: 421018 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D972, rank: 2, coeff_linf_bound: 858993459000, max_width: 55205 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P64Offset23703, ring_degree: LabiniusRingDegree::D1944, rank: 1, coeff_linf_bound: 858993459000, max_width: 27602 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 24116880, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 24641160, max_width: 5 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 1580547964560, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 1, coeff_linf_bound: 1614907702920, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 24116880, max_width: 17 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 24641160, max_width: 16 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 1580547964560, max_width: 6 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 2, coeff_linf_bound: 1614907702920, max_width: 6 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 24116880, max_width: 676757 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 24641160, max_width: 645916 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 1580547964560, max_width: 10 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D162, rank: 3, coeff_linf_bound: 1614907702920, max_width: 10 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 24116880, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 24641160, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 1580547964560, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 1, coeff_linf_bound: 1614907702920, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 24116880, max_width: 1085077782 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 24641160, max_width: 1037128646 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 1580547964560, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 2, coeff_linf_bound: 1614907702920, max_width: 8 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 1580547964560, max_width: 43565 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D324, rank: 3, coeff_linf_bound: 1614907702920, max_width: 41550 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D486, rank: 1, coeff_linf_bound: 13107000, max_width: 842036 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D486, rank: 1, coeff_linf_bound: 858993459000, max_width: 3 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D486, rank: 2, coeff_linf_bound: 858993459000, max_width: 110411 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D486, rank: 3, coeff_linf_bound: 858993459000, max_width: 1526290668749 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 24116880, max_width: 542538891 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 24641160, max_width: 518564323 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 1580547964560, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 1, coeff_linf_bound: 1614907702920, max_width: 4 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 1580547964560, max_width: 2043422581 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D648, rank: 2, coeff_linf_bound: 1614907702920, max_width: 1953388126 }, + LabiniusWidthCell { coefficient_prime: LabiniusCoefficientPrime::P128OffsetA7F7, ring_degree: LabiniusRingDegree::D972, rank: 1, coeff_linf_bound: 858993459000, max_width: 55205 }, +]; + +#[rustfmt::skip] +pub const LABINIUS_WIDTH_TABLE_DIGEST: [u8; 32] = [5, 134, 238, 98, 148, 132, 109, 17, 141, 30, 110, 243, 100, 241, 12, 64, 248, 229, 103, 143, 19, 95, 17, 220, 222, 66, 176, 251, 97, 168, 155, 253]; diff --git a/crates/akita-params/src/sis/labinius/parity_tests.rs b/crates/akita-params/src/sis/labinius/parity_tests.rs new file mode 100644 index 000000000..1ec47e6c0 --- /dev/null +++ b/crates/akita-params/src/sis/labinius/parity_tests.rs @@ -0,0 +1,245 @@ +//! Independent coefficient oracles for the direct parity row, without production +//! polynomial arithmetic or the closed-form quotient coefficients. + +use num_bigint::BigInt; +use rand::{rngs::StdRng, Rng, SeedableRng}; + +use super::{LabiniusRootProfile, LabiniusRootShape}; + +const D: usize = 162; +const WEIGHT: usize = 46; +const LOWER: i128 = -32_768; +const UPPER: i128 = 32_767; + +struct Instance { + b: Vec>, + v: Vec>, + u: Vec>, + c: Vec>, +} + +fn integer_product(lhs: &[BigInt], rhs: &[BigInt]) -> Vec { + let mut product = vec![BigInt::from(0); lhs.len() + rhs.len() - 1]; + for (i, left) in lhs.iter().enumerate() { + for (j, right) in rhs.iter().enumerate() { + product[i + j] += left * right; + } + } + product +} + +fn residual(instance: &Instance) -> Vec { + let mut result = vec![BigInt::from(0); 2 * D - 1]; + for (lhs, rhs, sign) in instance + .b + .iter() + .zip(&instance.v) + .map(|(b, v)| (b, v, 1)) + .chain(instance.u.iter().zip(&instance.c).map(|(u, c)| (u, c, -1))) + { + let lhs: Vec<_> = lhs.iter().map(|&x| BigInt::from(x)).collect(); + let rhs: Vec<_> = rhs.iter().map(|&x| BigInt::from(x)).collect(); + for (target, value) in result.iter_mut().zip(integer_product(&lhs, &rhs)) { + *target += value * sign; + } + } + result +} + +// Ordinary schoolbook division by the monic X^162 + X^81 + 1. +fn integer_division(input: &[BigInt]) -> (Vec, Vec) { + let mut remainder = input.to_vec(); + let mut quotient = vec![BigInt::from(0); D - 1]; + for degree in (D..input.len()).rev() { + let coefficient = remainder[degree].clone(); + let shift = degree - D; + quotient[shift] = coefficient.clone(); + for exponent in [0, D / 2, D] { + remainder[shift + exponent] -= &coefficient; + } + } + assert!(remainder[D..].iter().all(|x| *x == BigInt::from(0))); + remainder.truncate(D); + (quotient, remainder) +} + +// A separate Boolean oracle computes each product directly in F2[X]/Phi162. +// It never reads the integer residual or quotient. +fn binary_product(lhs: &[i128], rhs: &[i128]) -> Vec { + let mut product = vec![false; 2 * D - 1]; + for (i, left) in lhs.iter().enumerate() { + for (j, right) in rhs.iter().enumerate() { + product[i + j] ^= left % 2 != 0 && right % 2 != 0; + } + } + for degree in (D..product.len()).rev() { + if product[degree] { + product[degree] = false; + product[degree - D] ^= true; + product[degree - D / 2] ^= true; + } + } + product.truncate(D); + product +} + +fn binary_residual(instance: &Instance) -> Vec { + let mut sum = vec![false; D]; + for (lhs, rhs) in instance + .b + .iter() + .zip(&instance.v) + .chain(instance.u.iter().zip(&instance.c)) + { + for (target, bit) in sum.iter_mut().zip(binary_product(lhs, rhs)) { + *target ^= bit; + } + } + sum +} + +fn make_valid(instance: &mut Instance) { + // Reserve C_0=1: the remaining RHS can be arbitrary, while its missing + // canonical U_0 is the binary difference from the LHS. + instance.c[0].fill(0); + instance.c[0][0] = 1; + instance.u[0].fill(0); + instance.u[0] = binary_residual(instance) + .into_iter() + .map(i128::from) + .collect(); + assert!(binary_residual(instance).iter().all(|bit| !bit)); +} + +fn check_oracles(instance: &Instance, log_m: u32, log_c: u32) -> bool { + let shape = LabiniusRootShape::derive( + LabiniusRootProfile::D648P128BoundedW46Delta16, + log_m + log_c, + log_c, + 128, + ) + .expect("small oracle geometry is admitted"); + assert_eq!(instance.b.len(), shape.scalars_per_column()); + assert_eq!(instance.v.len(), shape.scalars_per_column()); + assert_eq!(instance.u.len(), shape.fold_width()); + assert_eq!(instance.c.len(), shape.fold_width()); + assert!(instance + .b + .iter() + .chain(&instance.u) + .flatten() + .all(|&x| x == 0 || x == 1)); + assert!(instance + .v + .iter() + .flatten() + .all(|x| (LOWER..=UPPER).contains(x))); + assert!(instance + .c + .iter() + .all(|c| c.iter().map(|x| x.unsigned_abs()).sum::() <= 46)); + + let input = residual(instance); + let h = BigInt::from(shape.parity_residual_bound()); + assert!(input.iter().all(|x| x >= &(-&h) && x <= &h)); + let (quotient, remainder) = integer_division(&input); + let q_bound = BigInt::from(shape.honest_quotient_bound()); + assert_eq!(q_bound, &h * 2); + assert!(quotient.iter().all(|x| x >= &(-&q_bound) && x <= &q_bound)); + + // Check the full characteristic-zero identity as well as the coefficient + // envelopes, so a defective oracle division cannot pass on bounds alone. + let mut phi = vec![BigInt::from(0); D + 1]; + for exponent in [0, D / 2, D] { + phi[exponent] = BigInt::from(1); + } + let mut reconstructed = integer_product("ient, &phi); + for (coefficient, tail) in reconstructed.iter_mut().zip(&remainder) { + *coefficient += tail; + } + assert_eq!(reconstructed, input); + + let all_even = remainder.iter().all(|x| x % 2 == BigInt::from(0)); + let binary = binary_residual(instance); + assert_eq!(all_even, binary.iter().all(|bit| !bit)); + for (coefficient, bit) in remainder.iter().zip(binary) { + assert_eq!(coefficient % 2 != BigInt::from(0), bit); + } + if all_even { + let carry_bound = BigInt::from(shape.honest_carry_bound()); + assert_eq!(carry_bound, &h * 5 / 2); + for coefficient in remainder { + let carry = coefficient / 2; + assert!(carry >= -&carry_bound && carry <= carry_bound); + } + } + all_even +} + +fn random_instance(rng: &mut StdRng, m: usize, columns: usize) -> Instance { + let b = (0..m) + .map(|_| (0..D).map(|_| rng.gen_range(0..=1)).collect()) + .collect(); + let v = (0..m) + .map(|_| (0..D).map(|_| rng.gen_range(LOWER..=UPPER)).collect()) + .collect(); + let u = (0..columns) + .map(|_| (0..D).map(|_| rng.gen_range(0..=1)).collect()) + .collect(); + let c = (0..columns) + .map(|_| { + let mut polynomial = vec![0; D]; + let mut populated = 0; + while populated < WEIGHT { + let position = rng.gen_range(0..D); + if polynomial[position] == 0 { + polynomial[position] = if rng.gen_bool(0.5) { 1 } else { -1 }; + populated += 1; + } + } + polynomial + }) + .collect(); + Instance { b, v, u, c } +} + +#[test] +fn random_direct_parity_big_integer_and_binary_oracles_agree() { + let mut rng = StdRng::seed_from_u64(0x0002_4316_2648); + for (log_m, log_c) in [(2, 0), (2, 1), (3, 2)] { + for _ in 0..4 { + let mut instance = random_instance(&mut rng, 1 << log_m, 1 << log_c); + check_oracles(&instance, log_m, log_c); + make_valid(&mut instance); + assert!(check_oracles(&instance, log_m, log_c)); + // C_0=1 makes this one-bit partial mutation a nonzero F162 error. + instance.u[0][0] ^= 1; + assert!(!check_oracles(&instance, log_m, log_c)); + } + } +} + +#[test] +fn extremal_direct_parity_endpoint_and_challenge_sign_patterns() { + for endpoint in [LOWER, UPPER] { + for sign in [-1, 1] { + for (log_m, log_c) in [(2, 0), (2, 2), (3, 1)] { + let m = 1 << log_m; + let columns = 1 << log_c; + let mut challenge = vec![0; D]; + challenge[..WEIGHT].fill(sign); + let mut instance = Instance { + b: vec![vec![1; D]; m], + v: vec![vec![endpoint; D]; m], + u: vec![vec![1; D]; columns], + c: vec![challenge; columns], + }; + // Negative challenges reinforce the positive endpoint; positive + // challenges reinforce the negative endpoint in B*V - U*C. + check_oracles(&instance, log_m, log_c); + make_valid(&mut instance); + assert!(check_oracles(&instance, log_m, log_c)); + } + } + } +} diff --git a/crates/akita-params/src/sis/labinius/root_profile.rs b/crates/akita-params/src/sis/labinius/root_profile.rs new file mode 100644 index 000000000..d91f8a8f5 --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_profile.rs @@ -0,0 +1,116 @@ +use akita_challenges::{BinaryChallengeProfile, BinaryScalarRing}; +use akita_error::AkitaError; + +use super::{LabiniusCoefficientPrime, LabiniusRingDegree, LABINIUS_WIDTH_TABLE_DIGEST}; + +/// Closed set of binary-root parameter identities. Adding one requires a new variant. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum LabiniusRootProfile { + /// Degree-648/P128, bounded weight 46, signed 16-bit response coefficients. + D648P128BoundedW46Delta16, +} + +impl LabiniusRootProfile { + /// Every supported root profile. + pub const ALL: [Self; 1] = [Self::D648P128BoundedW46Delta16]; + + /// Stable wire tag; tags are never reassigned. + pub const fn tag(self) -> u8 { + match self { + Self::D648P128BoundedW46Delta16 => 0, + } + } + + /// Decode a wire tag, rejecting unknown identities. + pub fn from_tag(tag: u8) -> Result { + match tag { + 0 => Ok(Self::D648P128BoundedW46Delta16), + _ => Err(AkitaError::InvalidSetup(format!( + "unknown LaBinius root profile tag {tag}" + ))), + } + } + + /// Binary scalar ring. + pub const fn scalar_ring(self) -> BinaryScalarRing { + match self { + Self::D648P128BoundedW46Delta16 => BinaryScalarRing::Cyclotomic243, + } + } + + /// Commitment-ring identity. + pub const fn ring_degree(self) -> LabiniusRingDegree { + match self { + Self::D648P128BoundedW46Delta16 => LabiniusRingDegree::D648, + } + } + + /// Exact coefficient-prime identity. + pub const fn coefficient_prime(self) -> LabiniusCoefficientPrime { + match self { + Self::D648P128BoundedW46Delta16 => LabiniusCoefficientPrime::P128OffsetA7F7, + } + } + + /// Exact challenge family. Fallible construction preserves the no-panic boundary. + pub fn challenge_profile(self) -> Result { + match self { + Self::D648P128BoundedW46Delta16 => { + BinaryChallengeProfile::bounded_weight(self.scalar_ring(), 46) + } + } + } + + /// Full accepted response interval `[L, U]`, including both endpoints. + pub const fn response_interval(self) -> (i128, i128) { + match self { + Self::D648P128BoundedW46Delta16 => (-32_768, 32_767), + } + } + + /// Domain-separated, unambiguous identity binding every parameter and table bytes. + pub fn identity_bytes(self) -> Result, AkitaError> { + let challenge = self.challenge_profile()?; + Ok(encode_identity( + self.tag(), + self.scalar_ring(), + self.coefficient_prime(), + self.ring_degree(), + challenge.identity_bytes(), + self.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + )) + } +} + +fn encode_identity( + tag: u8, + scalar_ring: BinaryScalarRing, + prime: LabiniusCoefficientPrime, + degree: LabiniusRingDegree, + challenge: &[u8], + interval: (i128, i128), + table_digest: [u8; 32], +) -> Vec { + let mut bytes = b"akita/labinius/root-profile/v1\0".to_vec(); + bytes.push(tag); + bytes.push(match scalar_ring { + BinaryScalarRing::Cyclotomic243 => 0, + BinaryScalarRing::Cyclotomic729 => 1, + }); + bytes.extend_from_slice(&prime.modulus().to_le_bytes()); + bytes.extend_from_slice(°ree.degree().to_le_bytes()); + // Challenge identity is length framed without platform-dependent integers. + for byte in challenge { + bytes.extend_from_slice(&[1, *byte]); + } + bytes.push(0); + bytes.extend_from_slice(&interval.0.to_le_bytes()); + bytes.extend_from_slice(&interval.1.to_le_bytes()); + bytes.extend_from_slice(&table_digest); + bytes +} + +#[cfg(test)] +#[path = "root_profile_tests.rs"] +mod tests; diff --git a/crates/akita-params/src/sis/labinius/root_profile_tests.rs b/crates/akita-params/src/sis/labinius/root_profile_tests.rs new file mode 100644 index 000000000..fc5cbedd3 --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_profile_tests.rs @@ -0,0 +1,118 @@ +use super::*; + +#[test] +fn closed_profile_tags_and_exact_parameters() { + for profile in LabiniusRootProfile::ALL { + assert_eq!( + LabiniusRootProfile::from_tag(profile.tag()).unwrap(), + profile + ); + assert_eq!(profile.scalar_ring(), BinaryScalarRing::Cyclotomic243); + assert_eq!(profile.ring_degree(), LabiniusRingDegree::D648); + assert_eq!( + profile.coefficient_prime(), + LabiniusCoefficientPrime::P128OffsetA7F7 + ); + assert_eq!(profile.response_interval(), (-32_768, 32_767)); + let challenge = profile.challenge_profile().unwrap(); + assert_eq!(challenge.coefficient_l1_bound(), 46); + assert_eq!(challenge.multiplication_linf_operator_bound(), 92); + assert_eq!( + profile.identity_bytes().unwrap(), + profile.identity_bytes().unwrap() + ); + } + for tag in 1..=u8::MAX { + assert!(matches!( + LabiniusRootProfile::from_tag(tag), + Err(AkitaError::InvalidSetup(_)) + )); + } +} + +#[test] +fn identity_binds_each_field_independently() { + let p = LabiniusRootProfile::ALL[0]; + let c = p.challenge_profile().unwrap(); + let mut digest = LABINIUS_WIDTH_TABLE_DIGEST; + digest[0] ^= 1; + let original = p.identity_bytes().unwrap(); + let altered_challenge = BinaryChallengeProfile::bounded_weight(p.scalar_ring(), 45).unwrap(); + let variants = [ + encode_identity( + 1, + p.scalar_ring(), + p.coefficient_prime(), + p.ring_degree(), + c.identity_bytes(), + p.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + BinaryScalarRing::Cyclotomic729, + p.coefficient_prime(), + p.ring_degree(), + c.identity_bytes(), + p.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + LabiniusCoefficientPrime::P64Offset23703, + p.ring_degree(), + c.identity_bytes(), + p.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + p.coefficient_prime(), + LabiniusRingDegree::D324, + c.identity_bytes(), + p.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + p.coefficient_prime(), + p.ring_degree(), + altered_challenge.identity_bytes(), + p.response_interval(), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + p.coefficient_prime(), + p.ring_degree(), + c.identity_bytes(), + (-32_767, 32_767), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + p.coefficient_prime(), + p.ring_degree(), + c.identity_bytes(), + (-32_768, 32_768), + LABINIUS_WIDTH_TABLE_DIGEST, + ), + encode_identity( + 0, + p.scalar_ring(), + p.coefficient_prime(), + p.ring_degree(), + c.identity_bytes(), + p.response_interval(), + digest, + ), + ]; + for variant in variants { + assert_ne!(variant, original); + } +} diff --git a/crates/akita-params/src/sis/labinius/root_shape.rs b/crates/akita-params/src/sis/labinius/root_shape.rs new file mode 100644 index 000000000..4d2b6df0e --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_shape.rs @@ -0,0 +1,277 @@ +use akita_challenges::BinaryChallengeProfile; +use akita_error::{checked, AkitaError}; + +use super::{ + checked_source_comparison_class_bound, labinius_min_secure_rank, LabiniusCoefficientPrime, + LabiniusRingDegree, LabiniusRootProfile, LabiniusSourceComparisonId, SourceOccurrenceBound, +}; + +/// Fully derived and SIS-admitted geometry for the direct binary-root baseline. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct LabiniusRootShape { + profile: LabiniusRootProfile, + num_cells: usize, + fold_width: usize, + scalars_per_column: usize, + ring_elements_per_column: usize, + packing_degree: usize, + scalar_degree: usize, + commitment_degree: usize, + eta_a: u128, + rank_a: u32, + image_len: usize, + a_quotient_len: usize, + parity_residual_bound: u128, + honest_quotient_bound: u128, + honest_carry_bound: u128, +} + +impl LabiniusRootShape { + /// Derive the one shared prover/verifier/planner admission decision. + pub fn derive( + profile: LabiniusRootProfile, + log_num_cells: u32, + log_fold_width: u32, + lambda_fold: u32, + ) -> Result { + derive_shape( + profile, + profile.coefficient_prime(), + profile.ring_degree(), + &profile.challenge_profile()?, + profile.response_interval(), + log_num_cells, + log_fold_width, + lambda_fold, + ) + } + + /// Check the actual accepted quotient/carry envelopes, including range rounding. + pub fn check_parity_no_wrap( + &self, + enforced_quotient_bound: u128, + enforced_carry_bound: u128, + ) -> Result<(), AkitaError> { + if enforced_quotient_bound < self.honest_quotient_bound { + return Err(AkitaError::InvalidSetup( + "LaBinius parity quotient envelope is below the honest bound".into(), + )); + } + if enforced_carry_bound < self.honest_carry_bound { + return Err(AkitaError::InvalidSetup( + "LaBinius parity carry envelope is below the honest bound".into(), + )); + } + let total = enforced_quotient_bound + .checked_mul(3) + .and_then(|q| self.parity_residual_bound.checked_add(q)) + .and_then(|hq| enforced_carry_bound.checked_mul(2)?.checked_add(hq)) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius parity no-wrap sum overflow".into()) + })?; + if total >= self.profile.coefficient_prime().modulus() { + return Err(AkitaError::InvalidSetup( + "LaBinius parity envelopes do not satisfy H + 3*B_Q + 2*B_K < P".into(), + )); + } + Ok(()) + } + + /// Selected closed profile. + pub const fn profile(&self) -> LabiniusRootProfile { + self.profile + } + /// Source scalar cells `N`. + pub const fn num_cells(&self) -> usize { + self.num_cells + } + /// Columns/folding challenges `C`. + pub const fn fold_width(&self) -> usize { + self.fold_width + } + /// Scalar entries per column `M`. + pub const fn scalars_per_column(&self) -> usize { + self.scalars_per_column + } + /// Ring entries per column `m`. + pub const fn ring_elements_per_column(&self) -> usize { + self.ring_elements_per_column + } + /// Scalar components per ring element `k`. + pub const fn packing_degree(&self) -> usize { + self.packing_degree + } + /// Scalar polynomial degree `d`. + pub const fn scalar_degree(&self) -> usize { + self.scalar_degree + } + /// Commitment polynomial degree `D`. + pub const fn commitment_degree(&self) -> usize { + self.commitment_degree + } + /// Certified source-comparison collision bound `eta_A`. + pub const fn eta_a(&self) -> u128 { + self.eta_a + } + /// Minimum certified cryptographic module rank `n_A`. + pub const fn rank_a(&self) -> u32 { + self.rank_a + } + /// Image coefficient count `n_A * C * D`. + pub const fn image_len(&self) -> usize { + self.image_len + } + /// A-quotient coefficient count `n_A * (D - 1)`. + pub const fn a_quotient_len(&self) -> usize { + self.a_quotient_len + } + /// Direct parity residual coefficient bound `H`. + pub const fn parity_residual_bound(&self) -> u128 { + self.parity_residual_bound + } + /// Honest direct parity quotient magnitude `B_Q`. + pub const fn honest_quotient_bound(&self) -> u128 { + self.honest_quotient_bound + } + /// Honest direct parity carry magnitude `B_K`. + pub const fn honest_carry_bound(&self) -> u128 { + self.honest_carry_bound + } +} + +// Canonical domain derivation. Explicit fields also let tests exercise boundaries +// that the sole current closed profile cannot reach (not a public plugin seam). +#[allow(clippy::too_many_arguments)] +fn derive_shape( + profile: LabiniusRootProfile, + prime: LabiniusCoefficientPrime, + degree: LabiniusRingDegree, + challenge: &BinaryChallengeProfile, + interval: (i128, i128), + log_num_cells: u32, + log_fold_width: u32, + lambda_fold: u32, +) -> Result { + let geometry_overflow = + || AkitaError::InvalidSetup("LaBinius root geometry size overflow".into()); + let num_cells = checked::pow2(usize::try_from(log_num_cells).map_err(|_| geometry_overflow())?) + .ok_or_else(geometry_overflow)?; + let fold_width = + checked::pow2(usize::try_from(log_fold_width).map_err(|_| geometry_overflow())?) + .ok_or_else(geometry_overflow)?; + let scalar_degree = challenge.scalar_ring().degree(); + let commitment_degree = usize::try_from(degree.degree()).map_err(|_| geometry_overflow())?; + let packing_degree = checked::exact_div(commitment_degree, scalar_degree) + .filter(|&k| k > 0) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius root scalar/commitment degree mismatch".into()) + })?; + let scalars_per_column = checked::exact_div(num_cells, fold_width); + let ring_elements_per_column = scalars_per_column + .and_then(|m| checked::exact_div(m, packing_degree)) + .filter(|&m| m > 0) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius root M must be a positive multiple of k".into()) + })?; + let scalars_per_column = scalars_per_column.ok_or_else(geometry_overflow)?; + let columns = u64::try_from(fold_width).map_err(|_| geometry_overflow())?; + if !challenge.meets_budget(columns, lambda_fold) { + return Err(AkitaError::InvalidSetup( + "LaBinius root challenge profile does not meet fold budget".into(), + )); + } + let (lower, upper) = interval; + let diameter = upper + .checked_sub(lower) + .and_then(|delta| u128::try_from(delta).ok()) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius response interval diameter overflow".into()) + })?; + let gamma = u128::from(challenge.multiplication_linf_operator_bound()); + let honest_response = u128::from(columns).checked_mul(gamma).ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius honest response bound overflow".into()) + })?; + let symmetric_cap = u128::try_from(upper) + .ok() + .zip(lower.checked_neg().and_then(|v| u128::try_from(v).ok())) + .map(|(u, l)| u.min(l)) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius response interval must contain zero".into()) + })?; + if honest_response > symmetric_cap { + return Err(AkitaError::InvalidSetup( + "LaBinius root honest response exceeds accepted interval".into(), + )); + } + let occurrence = SourceOccurrenceBound::binary_extracted(gamma, diameter).ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius source occurrence bound overflow".into()) + })?; + let eta_a = checked_source_comparison_class_bound( + LabiniusSourceComparisonId { + coefficient_prime: prime, + ring_degree: degree, + matrix_view_digest: [0; 32], + }, + &[occurrence], + )?; + let rank_a = labinius_min_secure_rank( + prime, + degree, + eta_a, + u64::try_from(ring_elements_per_column).map_err(|_| geometry_overflow())?, + ) + .ok_or_else(|| AkitaError::InvalidSetup("LaBinius root has no certified SIS cell".into()))?; + let rank = usize::try_from(rank_a).map_err(|_| geometry_overflow())?; + let image_len = + checked::product([rank, fold_width, commitment_degree]).ok_or_else(geometry_overflow)?; + let a_quotient_len = checked::product([ + rank, + commitment_degree + .checked_sub(1) + .ok_or_else(geometry_overflow)?, + ]) + .ok_or_else(geometry_overflow)?; + let bv = lower.unsigned_abs().max(upper.unsigned_abs()); + let parity_overflow = || AkitaError::InvalidSetup("LaBinius parity bound overflow".into()); + let parity_residual_bound = u128::try_from(scalar_degree) + .map_err(|_| parity_overflow())? + .checked_mul(u128::try_from(scalars_per_column).map_err(|_| parity_overflow())?) + .and_then(|dm| dm.checked_mul(bv)) + .and_then(|v| { + u128::from(columns) + .checked_mul(u128::from(challenge.coefficient_l1_bound()))? + .checked_add(v) + }) + .ok_or_else(parity_overflow)?; + let honest_quotient_bound = parity_residual_bound + .checked_mul(2) + .ok_or_else(parity_overflow)?; + let honest_carry_bound = parity_residual_bound + .checked_mul(5) + .ok_or_else(parity_overflow)? + / 2; + Ok(LabiniusRootShape { + profile, + num_cells, + fold_width, + scalars_per_column, + ring_elements_per_column, + packing_degree, + scalar_degree, + commitment_degree, + eta_a, + rank_a, + image_len, + a_quotient_len, + parity_residual_bound, + honest_quotient_bound, + honest_carry_bound, + }) +} + +#[cfg(test)] +#[path = "parity_tests.rs"] +mod parity_tests; +#[cfg(test)] +#[path = "root_shape_tests.rs"] +mod tests; diff --git a/crates/akita-params/src/sis/labinius/root_shape_tests.rs b/crates/akita-params/src/sis/labinius/root_shape_tests.rs new file mode 100644 index 000000000..39db4d172 --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_shape_tests.rs @@ -0,0 +1,136 @@ +use super::*; +const PROFILE: LabiniusRootProfile = LabiniusRootProfile::D648P128BoundedW46Delta16; + +fn rejection(result: Result, message: &str) { + match result { + Err(AkitaError::InvalidSetup(actual)) => assert!(actual.contains(message), "{actual}"), + other => panic!("expected InvalidSetup containing {message:?}, got {other:?}"), + } +} + +#[test] +fn golden_shape_and_largest_fold_width() { + let shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + assert_eq!(shape.profile(), PROFILE); + assert_eq!(shape.num_cells(), 1 << 22); + assert_eq!(shape.fold_width(), 256); + assert_eq!(shape.scalars_per_column(), 1 << 14); + assert_eq!(shape.ring_elements_per_column(), 1 << 12); + assert_eq!(shape.packing_degree(), 4); + assert_eq!(shape.scalar_degree(), 162); + assert_eq!(shape.commitment_degree(), 648); + assert_eq!(shape.rank_a(), 1); + assert_eq!(shape.eta_a(), 24_116_880); + assert_eq!(shape.image_len(), 165_888); + assert_eq!(shape.a_quotient_len(), 647); + assert_eq!(shape.parity_residual_bound(), 86_973_099_520); + assert_eq!(shape.honest_quotient_bound(), 173_946_199_040); + assert_eq!(shape.honest_carry_bound(), 217_432_748_800); + let maximum = (0..=22) + .filter(|&log| LabiniusRootShape::derive(PROFILE, 22, log, 128).is_ok()) + .max() + .unwrap(); + assert!(maximum >= 8); + assert_eq!(maximum, 8); + rejection( + LabiniusRootShape::derive(PROFILE, 22, maximum + 1, 128), + "challenge profile does not meet fold budget", + ); +} + +#[test] +fn caller_geometry_budget_response_and_missing_cell_rejections() { + LabiniusRootShape::derive(PROFILE, 2, 0, 128).unwrap(); + rejection( + LabiniusRootShape::derive(PROFILE, 1, 0, 128), + "M must be a positive multiple of k", + ); + rejection( + LabiniusRootShape::derive(PROFILE, 2, 3, 128), + "M must be a positive multiple of k", + ); + rejection( + LabiniusRootShape::derive(PROFILE, usize::BITS, 0, 128), + "geometry size overflow", + ); + rejection( + LabiniusRootShape::derive(PROFILE, 22, usize::BITS, 128), + "geometry size overflow", + ); + rejection( + LabiniusRootShape::derive(PROFILE, u32::MAX, 0, 128), + "geometry size overflow", + ); + rejection( + LabiniusRootShape::derive(PROFILE, 22, 8, 129), + "challenge profile does not meet fold budget", + ); + LabiniusRootShape::derive(PROFILE, 22, 8, 127).unwrap(); + rejection( + LabiniusRootShape::derive(PROFILE, 22, 9, 127), + "honest response exceeds accepted interval", + ); + LabiniusRootShape::derive(PROFILE, 32, 0, 128).unwrap(); + rejection( + LabiniusRootShape::derive(PROFILE, 33, 0, 128), + "no certified SIS cell", + ); +} + +#[test] +fn ledger_no_wrap_boundary_is_exercised_through_the_canonical_derivation() { + // The sole public profile always has eta=24,116,880 assert!(message.contains(text)), + other => panic!("unexpected result {other:?}"), + } + } + let remaining = PROFILE.coefficient_prime().modulus() - shape.parity_residual_bound() - 2 * k; + let first_q = remaining.div_ceil(3); + shape.check_parity_no_wrap(first_q - 1, k).unwrap(); + assert!(shape.check_parity_no_wrap(first_q, k).is_err()); + assert!(shape.check_parity_no_wrap(u128::MAX, k).is_err()); + assert!(shape.check_parity_no_wrap(q, u128::MAX).is_err()); +} diff --git a/crates/akita-params/src/sis/labinius/width_table.rs b/crates/akita-params/src/sis/labinius/width_table.rs new file mode 100644 index 000000000..696221cff --- /dev/null +++ b/crates/akita-params/src/sis/labinius/width_table.rs @@ -0,0 +1,46 @@ +//! Runtime admission by domination of an exact certified SIS cutoff. + +use super::{LabiniusCoefficientPrime, LabiniusRingDegree}; + +pub use super::generated_width_table::{LABINIUS_WIDTH_TABLE, LABINIUS_WIDTH_TABLE_DIGEST}; + +/// One exact certified positive-width cell under quantum 128-bit ADPS16. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct LabiniusWidthCell { + /// Exact coefficient prime. + pub coefficient_prime: LabiniusCoefficientPrime, + /// Scalarized commitment-ring degree. + pub ring_degree: LabiniusRingDegree, + /// Module rank. + pub rank: u32, + /// Certified coefficient infinity-norm bound. + pub coeff_linf_bound: u64, + /// Largest certified number of ring columns. + pub max_width: u64, +} + +/// Smallest certified rank dominating both the requested norm and width. +/// +/// Only cells with the same prime and degree participate. There is no +/// interpolation or extrapolation; an uncovered request returns `None`. +pub fn labinius_min_secure_rank( + prime: LabiniusCoefficientPrime, + degree: LabiniusRingDegree, + coeff_linf_bound: u128, + width: u64, +) -> Option { + LABINIUS_WIDTH_TABLE + .iter() + .filter(|cell| { + cell.coefficient_prime == prime + && cell.ring_degree == degree + && u128::from(cell.coeff_linf_bound) >= coeff_linf_bound + && cell.max_width >= width + }) + .map(|cell| cell.rank) + .min() +} + +#[cfg(test)] +#[path = "width_table_tests.rs"] +mod tests; diff --git a/crates/akita-params/src/sis/labinius/width_table_tests.rs b/crates/akita-params/src/sis/labinius/width_table_tests.rs new file mode 100644 index 000000000..3322dbd6e --- /dev/null +++ b/crates/akita-params/src/sis/labinius/width_table_tests.rs @@ -0,0 +1,115 @@ +use super::*; + +fn independent_rank(cell: &LabiniusWidthCell, bound: u128, width: u64) -> Option { + // Rank-first enumeration is independent of the production filter/min path. + (1..=3).find(|rank| { + LABINIUS_WIDTH_TABLE.iter().any(|candidate| { + candidate.rank == *rank + && candidate.coefficient_prime == cell.coefficient_prime + && candidate.ring_degree == cell.ring_degree + && u128::from(candidate.coeff_linf_bound) >= bound + && candidate.max_width >= width + }) + }) +} + +#[test] +fn exact_cells_and_immediate_boundaries_use_only_certified_domination() { + assert_eq!(LABINIUS_WIDTH_TABLE.len(), 69); + for cell in LABINIUS_WIDTH_TABLE { + let bound = u128::from(cell.coeff_linf_bound); + let lookup = |bound, width| { + labinius_min_secure_rank(cell.coefficient_prime, cell.ring_degree, bound, width) + }; + assert_eq!(lookup(bound, cell.max_width), Some(cell.rank)); + + let next_width = lookup(bound, cell.max_width + 1); + assert_eq!( + next_width, + independent_rank(cell, bound, cell.max_width + 1) + ); + assert!(next_width.is_none_or(|rank| rank > cell.rank)); + + // A stronger norm cell can admit bound + 1 at the same rank. Once the + // greatest such norm is exceeded, only a larger rank can admit it. + let next_bound = lookup(bound + 1, cell.max_width); + assert_eq!( + next_bound, + independent_rank(cell, bound + 1, cell.max_width) + ); + assert!(next_bound.is_none_or(|rank| rank >= cell.rank)); + let norm_frontier = LABINIUS_WIDTH_TABLE + .iter() + .filter(|candidate| { + candidate.coefficient_prime == cell.coefficient_prime + && candidate.ring_degree == cell.ring_degree + && candidate.rank == cell.rank + && candidate.max_width >= cell.max_width + }) + .map(|candidate| u128::from(candidate.coeff_linf_bound)) + .max() + .unwrap(); + assert!(lookup(norm_frontier + 1, cell.max_width).is_none_or(|rank| rank > cell.rank)); + } +} + +#[test] +fn uncovered_prime_degree_combinations_and_unrepresentable_bounds_are_rejected() { + for bound in [0, 1, u128::from(u64::MAX), u128::MAX] { + assert_eq!( + labinius_min_secure_rank( + LabiniusCoefficientPrime::P128OffsetA7F7, + LabiniusRingDegree::D1944, + bound, + 1, + ), + None, + ); + } + for cell in LABINIUS_WIDTH_TABLE { + assert_eq!( + labinius_min_secure_rank( + cell.coefficient_prime, + cell.ring_degree, + u128::from(u64::MAX) + 1, + cell.max_width, + ), + None, + ); + } +} + +#[test] +fn reducing_either_request_coordinate_never_increases_the_admitted_rank() { + for cell in LABINIUS_WIDTH_TABLE { + let bound = u128::from(cell.coeff_linf_bound); + for dominated_bound in [0, 1, bound / 2, bound - 1, bound] { + for dominated_width in [0, 1, cell.max_width / 2, cell.max_width - 1, cell.max_width] { + let rank = labinius_min_secure_rank( + cell.coefficient_prime, + cell.ring_degree, + dominated_bound, + dominated_width, + ) + .expect("a certified cell dominates the request"); + assert!(rank <= cell.rank); + } + } + } +} + +#[test] +fn cells_have_canonical_numeric_degree_order_without_duplicates() { + let key = |cell: &LabiniusWidthCell| { + ( + cell.coefficient_prime, + cell.ring_degree.degree(), + cell.rank, + cell.coeff_linf_bound, + cell.max_width, + ) + }; + for pair in LABINIUS_WIDTH_TABLE.windows(2) { + assert!(key(&pair[0]) < key(&pair[1])); + } +} diff --git a/crates/akita-sis-estimator/examples/labinius_infinity_width_table.rs b/crates/akita-sis-estimator/examples/labinius_infinity_width_table.rs index bd5eed9ee..6288dfeb9 100644 --- a/crates/akita-sis-estimator/examples/labinius_infinity_width_table.rs +++ b/crates/akita-sis-estimator/examples/labinius_infinity_width_table.rs @@ -1,21 +1,28 @@ //! Generate the staged LaBinius binary-source SIS audit rows. //! -//! This is intentionally an offline CSV artifact. It does not generate a -//! runtime schedule table because the binary root protocol is not implemented. +//! `--from-csv` emits the runtime admission cells from the checked-in certified +//! CSV without running a lattice search. Search mode emits both artifacts. use akita_challenges::{BinaryChallengeFamily, BinaryChallengeProfile, BinaryScalarRing}; use akita_params::sis::{ - labinius::{LabiniusCoefficientPrime, SourceOccurrenceBound}, + labinius::{LabiniusCoefficientPrime, LabiniusRingDegree, SourceOccurrenceBound}, source_comparison_inf_norm, }; use akita_sis_estimator::{ + labinius_width_table::certified_rows, width_table::{ generate_infinity_width_rows, validate_infinity_width_rows, InfinityWidthOrigin, InfinityWidthRow, InfinityWidthTableConfig, INFINITY_WIDTH_EVALUATOR_ID, }, AkitaModulusProfileId, }; -use std::{env, fs, path::PathBuf, process, time::Instant}; +use sha3::{Digest, Sha3_256}; +use std::{ + env, fs, + path::{Path, PathBuf}, + process, + time::Instant, +}; const DELTA_32: u64 = (1u64 << 32) - 1; const DELTA_16: u64 = (1u64 << 16) - 1; @@ -76,6 +83,8 @@ const SOURCE_PROFILES: &[SourceProfile] = &[ struct Args { output: PathBuf, + rust_output: PathBuf, + from_csv: bool, profiles: Vec, dims: Vec, source_profiles: Vec<&'static str>, @@ -86,6 +95,13 @@ struct Args { fn main() { let args = Args::parse(); + if args.from_csv { + let rows = certified_rows() + .unwrap_or_else(|error| fatal(&format!("CSV certificate validation failed: {error}"))); + let csv = include_bytes!("../data/labinius_infinity_width.csv"); + write_runtime_table(&args.rust_output, rows, csv); + return; + } let specs = selected_specs(&args); let explicit_origins = specs .iter() @@ -136,7 +152,7 @@ fn main() { fs::create_dir_all(parent) .unwrap_or_else(|error| fatal(&format!("create output directory failed: {error}"))); } - fs::write(&args.output, output) + fs::write(&args.output, &output) .unwrap_or_else(|error| fatal(&format!("write {} failed: {error}", args.output.display()))); eprintln!( "wrote {} certified LaBinius row(s) to {} in {:.3}s", @@ -148,6 +164,70 @@ fn main() { "omitted {} zero-width or cap-limited candidate row(s)", rows.len() - certified_rows.len() ); + let certified_rows = certified_rows.into_iter().cloned().collect::>(); + write_runtime_table(&args.rust_output, &certified_rows, output.as_bytes()); +} + +fn runtime_table(rows: &[InfinityWidthRow], csv: &[u8]) -> String { + let mut rows = rows.iter().collect::>(); + rows.sort_by_key(|row| { + ( + coefficient_prime(row.modulus_profile), + row.d, + row.rank, + row.coeff_linf_bound, + row.max_width, + ) + }); + let mut output = String::from( + "// AUTO-GENERATED by labinius_infinity_width_table --from-csv -- do not edit by hand.\n\ + // Source: crates/akita-sis-estimator/data/labinius_infinity_width.csv\n\n\ + use super::width_table::LabiniusWidthCell;\n\ + use super::{LabiniusCoefficientPrime, LabiniusRingDegree};\n\n\ + #[rustfmt::skip]\n\ + pub const LABINIUS_WIDTH_TABLE: &[LabiniusWidthCell] = &[\n", + ); + for row in rows { + output.push_str(&format!( + " LabiniusWidthCell {{ coefficient_prime: LabiniusCoefficientPrime::{:?}, ring_degree: LabiniusRingDegree::{:?}, rank: {}, coeff_linf_bound: {}, max_width: {} }},\n", + coefficient_prime(row.modulus_profile), + ring_degree(row.d), + row.rank, + row.coeff_linf_bound, + row.max_width, + )); + } + let digest: [u8; 32] = Sha3_256::digest(csv).into(); + output.push_str(&format!( + "];\n\n#[rustfmt::skip]\npub const LABINIUS_WIDTH_TABLE_DIGEST: [u8; 32] = {digest:?};\n" + )); + output +} + +fn ring_degree(degree: u32) -> LabiniusRingDegree { + match degree { + 162 => LabiniusRingDegree::D162, + 324 => LabiniusRingDegree::D324, + 648 => LabiniusRingDegree::D648, + 486 => LabiniusRingDegree::D486, + 972 => LabiniusRingDegree::D972, + 1_944 => LabiniusRingDegree::D1944, + _ => fatal("unsupported LaBinius ring degree"), + } +} + +fn write_runtime_table(path: &Path, rows: &[InfinityWidthRow], csv: &[u8]) { + if let Some(parent) = path.parent() { + fs::create_dir_all(parent) + .unwrap_or_else(|error| fatal(&format!("create runtime directory failed: {error}"))); + } + fs::write(path, runtime_table(rows, csv)) + .unwrap_or_else(|error| fatal(&format!("write {} failed: {error}", path.display()))); + eprintln!( + "wrote {} certified runtime LaBinius cell(s) to {}", + rows.len(), + path.display() + ); } fn selected_specs(args: &Args) -> Vec<(AkitaModulusProfileId, u32, SourceProfile)> { @@ -259,6 +339,9 @@ impl Args { fn parse() -> Self { let mut parsed = Self { output: PathBuf::from("crates/akita-sis-estimator/data/labinius_infinity_width.csv"), + rust_output: PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("../akita-params/src/sis/labinius/generated_width_table.rs"), + from_csv: false, profiles: vec![ AkitaModulusProfileId::Q64Offset23703, AkitaModulusProfileId::Q128OffsetA7F7, @@ -277,11 +360,16 @@ impl Args { if arg == "--help" || arg == "-h" { usage(0); } + if arg == "--from-csv" { + parsed.from_csv = true; + continue; + } let value = args .next() .unwrap_or_else(|| fatal(&format!("missing value for {arg}"))); match arg.as_str() { "--output" => parsed.output = PathBuf::from(value), + "--rust-output" => parsed.rust_output = PathBuf::from(value), "--profiles" => { parsed.use_default_coverage = false; parsed.profiles = csv(&value) @@ -348,7 +436,7 @@ where fn usage(code: i32) -> ! { eprintln!( - "usage: labinius_infinity_width_table [--output PATH] [--profiles q64-labinius,q128] [--dims 162,324,648,486,972,1944] [--source-profiles phi243-bounded-w46-delta16,phi243-fixed-w47-delta16,phi243-bounded-w46-delta32,phi243-fixed-w47-delta32,phi729-fixed-w25-delta16,phi729-fixed-w25-delta32] [--max-rank N] [--search-cap N]" + "usage: labinius_infinity_width_table [--from-csv] [--rust-output PATH] [--output PATH] [--profiles q64-labinius,q128] [--dims 162,324,648,486,972,1944] [--source-profiles phi243-bounded-w46-delta16,phi243-fixed-w47-delta16,phi243-bounded-w46-delta32,phi243-fixed-w47-delta32,phi729-fixed-w25-delta16,phi729-fixed-w25-delta32] [--max-rank N] [--search-cap N]" ); process::exit(code); } @@ -363,6 +451,17 @@ mod tests { use super::*; use std::collections::BTreeSet; + #[test] + fn checked_in_runtime_table_is_the_csv_generator_output() { + assert_eq!( + runtime_table( + certified_rows().unwrap(), + include_bytes!("../data/labinius_infinity_width.csv"), + ), + include_str!("../../akita-params/src/sis/labinius/generated_width_table.rs"), + ); + } + #[test] fn canonical_bounds_are_the_exact_binary_diagonal_envelopes() { let p64 = AkitaModulusProfileId::Q64Offset23703; diff --git a/crates/akita-sis-estimator/tests/labinius_width_table.rs b/crates/akita-sis-estimator/tests/labinius_width_table.rs index 7730cc2ec..bae201026 100644 --- a/crates/akita-sis-estimator/tests/labinius_width_table.rs +++ b/crates/akita-sis-estimator/tests/labinius_width_table.rs @@ -1,13 +1,64 @@ #![cfg(feature = "labinius-sis")] +use akita_params::sis::labinius::{ + LabiniusCoefficientPrime, LabiniusRingDegree, LabiniusWidthCell, LABINIUS_WIDTH_TABLE, + LABINIUS_WIDTH_TABLE_DIGEST, +}; use akita_sis_estimator::{ + labinius_width_table::certified_rows, width_table::{validate_infinity_width_rows, InfinityWidthRow}, AkitaModulusProfileId, SisSecurityPolicy, }; +use sha3::{Digest, Sha3_256}; use std::collections::BTreeSet; const TABLE: &str = include_str!("../data/labinius_infinity_width.csv"); +#[test] +fn runtime_cells_and_digest_match_the_certified_csv_in_both_directions() { + let rows = certified_rows().expect("certified CSV"); + assert_eq!(rows.len(), 69); + assert_eq!(LABINIUS_WIDTH_TABLE.len(), rows.len()); + let csv_cells = rows + .iter() + .map(|row| LabiniusWidthCell { + coefficient_prime: match row.modulus_profile { + AkitaModulusProfileId::Q64Offset23703 => LabiniusCoefficientPrime::P64Offset23703, + AkitaModulusProfileId::Q128OffsetA7F7 => LabiniusCoefficientPrime::P128OffsetA7F7, + other => panic!("unexpected modulus profile: {other:?}"), + }, + ring_degree: match row.d { + 162 => LabiniusRingDegree::D162, + 324 => LabiniusRingDegree::D324, + 648 => LabiniusRingDegree::D648, + 486 => LabiniusRingDegree::D486, + 972 => LabiniusRingDegree::D972, + 1_944 => LabiniusRingDegree::D1944, + other => panic!("unexpected ring degree: {other}"), + }, + rank: row.rank, + coeff_linf_bound: row.coeff_linf_bound, + max_width: row.max_width, + }) + .collect::>(); + let runtime_cells = LABINIUS_WIDTH_TABLE + .iter() + .copied() + .collect::>(); + assert_eq!(csv_cells.len(), rows.len(), "CSV has duplicate cells"); + assert_eq!( + runtime_cells.len(), + rows.len(), + "runtime has duplicate cells" + ); + assert_eq!(csv_cells, runtime_cells, "runtime/CSV cell drift"); + let digest: [u8; 32] = Sha3_256::digest(TABLE.as_bytes()).into(); + assert_eq!( + LABINIUS_WIDTH_TABLE_DIGEST, digest, + "runtime/CSV digest drift" + ); +} + #[test] fn checked_in_labinius_cells_have_exact_cutoffs_and_rejected_successors() { let mut lines = TABLE.lines(); diff --git a/specs/labinius-root-admission.md b/specs/labinius-root-admission.md new file mode 100644 index 000000000..0a91a7d0b --- /dev/null +++ b/specs/labinius-root-admission.md @@ -0,0 +1,174 @@ +# LaBinius binary-root admission + +Status: active +Book-chapter: book/src/foundations/security.md +Tracking: https://github.com/LayerZero-Labs/akita/issues/45 + +## Scope and profile + +The opt-in `labinius-sis` feature supplies a runtime certified-width lookup and +one closed root profile. `LabiniusRootShape::derive` is the common admission +function for future prover, verifier and planner callers. Enabling the feature +does not select the extension or change the ordinary protocol. + +| Profile item | `D648P128BoundedW46Delta16` | +| --- | --- | +| Scalar ring | `BinaryScalarRing::Cyclotomic243`, degree 162 | +| Commitment ring | `LabiniusRingDegree::D648`, packing degree 4 | +| Coefficient prime | `LabiniusCoefficientPrime::P128OffsetA7F7` | +| Challenge family | Bounded weight 46 on `Cyclotomic243` | +| Accepted response interval | `[-32768, 32767]` | +| Accepted response diameter | `Delta = 65535` | +| Stable wire tag | 0 | + +Unknown tags reject. Adding a profile requires a new enum variant. Identity +bytes begin with `akita/labinius/root-profile/v1` and a zero byte, then encode +the tag, scalar-ring tag, exact prime (16 little-endian bytes), commitment degree +(4 little-endian bytes), challenge identity, both signed interval endpoints +(16 little-endian bytes each), and the 32-byte certified-table digest. Challenge +bytes are framed as `(1, byte)` pairs followed by zero, so variable lengths +cannot alias subsequent fields. This binds every norm, entropy, sign-rule and +accepted-range choice as well as the table version. Challenge construction and +identity accessors return errors rather than panicking on a violated profile +invariant. + +## Geometry and source admission + +Issue sections 2, 3, 4 (direct baseline) and 6 specify the contracts below. +Write `d=162`, `D=648`, `k=D/d=4`, `C=2^log_fold_width`, `N=2^log_num_cells`, +`M=N/C`, and `m=M/k`. N counts F162 scalar cells, M scalar cells per column, +and m commitment-ring elements per column. M must be a positive multiple of k. +Geometry and coefficient counts use checked `usize` arithmetic; norm arithmetic +uses checked `u128` arithmetic. No allocation is proportional to the geometry. + +The challenge profile supplies `w=46` and `Gamma_inf=92`. Its exact support +cardinality must satisfy `|C_family| >= C * 2^lambda_fold`, through +`BinaryChallengeProfile::meets_budget`. This budget is caller allocated and is +separate from the per-instance 128-bit quantum ADPS16 table policy. Deterministic +honest response admission requires `C * Gamma_inf <= min(U, -L)` for source +coefficients of magnitude at most one (issue section 3). + +The accepted response diameter, rather than an honest constructor's smaller +range, feeds a single `SourceOccurrenceBound::binary_extracted(Gamma_inf, +U-L)` into `checked_source_comparison_class_bound`. That existing ledger includes +the diagonal comparison and computes `eta_A = 4 * Gamma_inf * Delta`, enforcing +`eta_A < P` (issue sections 3 and 6). Its matrix-view digest is a fixed placeholder +here: this single-occurrence calculation does not compare root layouts or bind +an eventual protocol matrix view. The root protocol must supply that identity. + +`labinius_min_secure_rank(prime, degree, eta_A, m)` chooses the smallest rank +with a certified cell of the same prime and degree whose bound and width both +dominate the request. Missing coverage rejects. There is no interpolation, +extrapolation or runtime lattice estimation. A stronger norm cell can admit a +request at the same rank after one particular cell's norm boundary is crossed. + +The admitted image has `n_A * C * D` coefficients. Products in the A relation +have degree at most `2D-2`; division by the monic degree-D cyclotomic polynomial +therefore gives quotient degree at most `D-2`, or `n_A * (D-1)` coefficients +(issue section 5). + +## Direct parity quotient and carry + +The direct row of issue section 4 is + +```text +R(X) = sum_i B_i(X) V_i(X) - sum_j U_j(X) C_j(X) + = (X^162 + X^81 + 1) Q(X) + 2 K(X). +``` + +B and U have bit coefficients; V uses the full accepted interval; C has L1 +norm at most w. Each product coefficient in B*V has at most d summands of +magnitude `B_V=max(|L|,|U|)`. Each coefficient in U*C has magnitude at most w. +Thus `H = d*M*B_V + C*w` bounds every coefficient of R, whose degree is at most +322. The same reasoning holds for signed C lifts: their parity reductions +have the specified binary support. + +To check the honest bounds independently, write `r_t` for R's integer +coefficients, taking missing terms to be zero. Monic schoolbook division from +highest degree down gives + +```text +q_k = r_(k+162) for 80 <= k <= 160 +q_k = r_(k+162) - r_(k+243) for 0 <= k <= 79. +``` + +Indeed only a quotient coefficient 81 positions higher can affect the next +high coefficient. Those higher coefficients have already been assigned their +original residual value. Consequently `|q_k| <= 2H`; Q has 161 coefficients. +The remainder coefficient at `0 <= j <= 161` is +`r_j - q_j - q_(j-81)`, ignoring quotient indices outside `[0,160]`. Bounding +each quotient term by 2H gives `|remainder_j| <= 5H`. A valid F162 identity +holds exactly when all these remainder coefficients are even: integer division +commutes with reduction modulo two because the divisor is monic. Then K is +half the remainder and is integral, with + +```text +B_Q = 2H +B_K = floor(5H/2). +``` + +These are conservative honest construction bounds. They are not permission to +use tighter accepted alphabets in a proof. `check_parity_no_wrap(B_Q', B_K')` +requires each caller-supplied magnitude to cover its honest bound and enforces +the issue's full accepted-envelope inequality +`H + 3*B_Q' + 2*B_K' < P`. The coefficient sum of Phi has three terms, so this +ensures that a checked residual equality modulo P cannot conceal a nonzero +integer coefficient. Rounded digit alphabets must pass their actual enforced +magnitudes. An overflow rejects, as does equality at P. + +## Admission order and boundary fixture + +The canonical derivation applies these gates in order: + +1. Represent both powers of two; check ring/scalar compatibility and exact, + positive packing/column divisions. +2. Check the challenge family's exact fold budget. +3. Check the response interval and deterministic honest response envelope. +4. Use the source-comparison ledger, including its `eta_A < P` check. +5. Select the minimum dominating certified SIS rank; reject missing coverage. +6. Derive image/quotient lengths and honest parity bounds with checked arithmetic. + +Caller-selected failures use `AkitaError::InvalidSetup`, matching neighbouring +SIS admission. Actual parity range envelopes are checked separately once the +caller chooses an encoding. The sole profile's eta is fixed below P; tests +perturb internal fields to exercise the ledger boundary without exposing a +runtime profile plugin. + +For `(log_num_cells, log_fold_width, lambda_fold) = (22,8,128)` the shape has +`N=4194304`, `C=256`, `M=16384`, `m=4096`, `k=4`, `n_A=1`, +`eta_A=24116880`, image length 165888, and A-quotient length 647. +The direct residual bound is `162 * 2^29 + 256 * 46 = 86973099520`. +At budget 128 the bounded-weight family supports at most 315 columns, so the +largest admitted power-of-two fold width is 256 (log 8). Log 9 rejects at the +challenge gate. With a lower budget it instead fails the honest response gate. + +## Table provenance and verification + +The frozen CSV is +`crates/akita-sis-estimator/data/labinius_infinity_width.csv`, with 69 certified +rows. It records accepted cutoffs and rejected successors under the existing +quantum ADPS16 policy. The generator example `labinius_infinity_width_table` +can search new offline cells, or emit the runtime Rust file directly from the +checked-in CSV without repeating the lattice search: + +```bash +cargo run -p akita-sis-estimator --no-default-features --features labinius-sis \ + --example labinius_infinity_width_table -- --from-csv +``` + +The emitted `generated_width_table.rs` has canonical sorted cells and a +SHA3-256 digest of the exact CSV bytes. Runtime consumers depend only on +`akita-params`, never on the estimator. The estimator integration test +`labinius_width_table` compares all fields in both directions and recomputes +the digest, forming the drift gate. Fast parameter unit tests cover domination, +profile identity perturbations, admission boundaries, overflow and exact no-wrap +limits. An independent BigInt convolution/long-division oracle and separate +binary reduction cover random, extremal, valid and invalid parity rows. + +## Remaining protocol work + +This slice defines no schedule family, proof-size model, Fiat–Shamir ledger, +proof encoding, successor-witness layout, planner integration, or root protocol. +It does not claim complete PCS security admission. Those belong to the root +protocol and its composition with the ordinary tail. No unpublished paper or +unlicensed reference implementation is needed for these formulas or tests. From f629d7f2bc3b3ec5833931279b8585fa562efa04 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 06:13:29 +0100 Subject: [PATCH 2/6] feat(labinius): enforced digit ranges and root witness lengths --- crates/akita-params/src/sis/labinius.rs | 4 +- .../src/sis/labinius/parity_tests.rs | 64 +++- .../src/sis/labinius/root_encoding.rs | 266 ++++++++++++++++ .../src/sis/labinius/root_encoding_tests.rs | 292 ++++++++++++++++++ .../src/sis/labinius/root_shape.rs | 31 +- .../src/sis/labinius/root_shape_tests.rs | 2 +- specs/labinius-root-admission.md | 116 ++++++- 7 files changed, 752 insertions(+), 23 deletions(-) create mode 100644 crates/akita-params/src/sis/labinius/root_encoding.rs create mode 100644 crates/akita-params/src/sis/labinius/root_encoding_tests.rs diff --git a/crates/akita-params/src/sis/labinius.rs b/crates/akita-params/src/sis/labinius.rs index 27637797d..1a0164d4b 100644 --- a/crates/akita-params/src/sis/labinius.rs +++ b/crates/akita-params/src/sis/labinius.rs @@ -11,7 +11,9 @@ mod root_shape; mod width_table; pub use root_profile::LabiniusRootProfile; -pub use root_shape::LabiniusRootShape; +pub use root_shape::{ + LabiniusDigitBase, LabiniusRootEncoding, LabiniusRootShape, LabiniusSignedDigitRange, +}; pub use width_table::{ labinius_min_secure_rank, LabiniusWidthCell, LABINIUS_WIDTH_TABLE, LABINIUS_WIDTH_TABLE_DIGEST, }; diff --git a/crates/akita-params/src/sis/labinius/parity_tests.rs b/crates/akita-params/src/sis/labinius/parity_tests.rs index 1ec47e6c0..ac452aa1f 100644 --- a/crates/akita-params/src/sis/labinius/parity_tests.rs +++ b/crates/akita-params/src/sis/labinius/parity_tests.rs @@ -63,6 +63,19 @@ fn integer_division(input: &[BigInt]) -> (Vec, Vec) { (quotient, remainder) } +fn check_closed_form_remainder(input: &[BigInt], remainder: &[BigInt]) { + for (j, coefficient) in remainder.iter().enumerate() { + let expected = match j { + 0..=79 => &input[j] - &input[j + 162] + &input[j + 243], + 80 => &input[80] - &input[242], + 81..=160 => &input[j] - &input[j + 81], + 161 => &input[161] - &input[242], + _ => unreachable!("the remainder has degree below 162"), + }; + assert_eq!(*coefficient, expected, "remainder coefficient {j}"); + } +} + // A separate Boolean oracle computes each product directly in F2[X]/Phi162. // It never reads the integer residual or quotient. fn binary_product(lhs: &[i128], rhs: &[i128]) -> Vec { @@ -143,6 +156,7 @@ fn check_oracles(instance: &Instance, log_m: u32, log_c: u32) -> bool { let h = BigInt::from(shape.parity_residual_bound()); assert!(input.iter().all(|x| x >= &(-&h) && x <= &h)); let (quotient, remainder) = integer_division(&input); + check_closed_form_remainder(&input, &remainder); let q_bound = BigInt::from(shape.honest_quotient_bound()); assert_eq!(q_bound, &h * 2); assert!(quotient.iter().all(|x| x >= &(-&q_bound) && x <= &q_bound)); @@ -167,7 +181,7 @@ fn check_oracles(instance: &Instance, log_m: u32, log_c: u32) -> bool { } if all_even { let carry_bound = BigInt::from(shape.honest_carry_bound()); - assert_eq!(carry_bound, &h * 5 / 2); + assert_eq!(carry_bound, &h * 3 / 2); for coefficient in remainder { let carry = coefficient / 2; assert!(carry >= -&carry_bound && carry <= carry_bound); @@ -176,6 +190,54 @@ fn check_oracles(instance: &Instance, log_m: u32, log_c: u32) -> bool { all_even } +#[test] +fn arbitrary_residual_remainder_closed_form_matches_long_division() { + let mut rng = StdRng::seed_from_u64(0x0243_0162_0322); + let h = BigInt::from(100); + for _ in 0..32 { + let input: Vec<_> = (0..2 * D - 1) + .map(|_| BigInt::from(rng.gen_range(-100_i128..=100))) + .collect(); + let (_, remainder) = integer_division(&input); + check_closed_form_remainder(&input, &remainder); + assert!(remainder.iter().all(|x| x >= &(-&h * 3) && x <= &(&h * 3))); + } + + // Saturate each closed form separately, including every cancellation index. + // Even H makes the extremal remainder a valid even residual modulo Phi. + for j in 0..D { + for sign in [-1_i32, 1] { + let mut input = vec![BigInt::from(0); 2 * D - 1]; + let signed_h = &h * sign; + input[j] = signed_h.clone(); + let multiple = match j { + 0..=79 => { + input[j + 162] = -&signed_h; + input[j + 243] = signed_h; + 3 + } + 80 | 161 => { + input[242] = -signed_h; + 2 + } + 81..=160 => { + input[j + 81] = -signed_h; + 2 + } + _ => unreachable!("the remainder has degree below 162"), + }; + let (_, remainder) = integer_division(&input); + check_closed_form_remainder(&input, &remainder); + assert_eq!(remainder[j], &h * sign * multiple); + assert!(remainder.iter().all(|x| x % 2 == BigInt::from(0))); + let carry_bound: BigInt = &h * 3_i32 / 2_i32; + assert!(remainder + .iter() + .all(|x| x / 2 >= -&carry_bound && x / 2 <= carry_bound)); + } + } +} + fn random_instance(rng: &mut StdRng, m: usize, columns: usize) -> Instance { let b = (0..m) .map(|_| (0..D).map(|_| rng.gen_range(0..=1)).collect()) diff --git a/crates/akita-params/src/sis/labinius/root_encoding.rs b/crates/akita-params/src/sis/labinius/root_encoding.rs new file mode 100644 index 000000000..827bfe8f9 --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_encoding.rs @@ -0,0 +1,266 @@ +use akita_error::{checked, AkitaError}; + +use super::{parity_no_wrap_total, LabiniusRootShape}; + +/// Closed digit alphabets; a tag selects the number of bits in each digit. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum LabiniusDigitBase { + /// Digits in `[0, 1]`. + Bits1, + /// Digits in `[0, 3]`. + Bits2, + /// Digits in `[0, 15]`. + Bits4, +} + +impl LabiniusDigitBase { + /// Stable wire tag, never reassigned. + pub const fn tag(self) -> u8 { + match self { + Self::Bits1 => 0, + Self::Bits2 => 1, + Self::Bits4 => 2, + } + } + + /// Decode the closed digit alphabet. + pub fn from_tag(tag: u8) -> Result { + match tag { + 0 => Ok(Self::Bits1), + 1 => Ok(Self::Bits2), + 2 => Ok(Self::Bits4), + _ => Err(AkitaError::InvalidSetup(format!( + "unknown LaBinius digit base tag {tag}" + ))), + } + } + + /// Bits per digit `b`. + pub const fn bits(self) -> u32 { + match self { + Self::Bits1 => 1, + Self::Bits2 => 2, + Self::Bits4 => 4, + } + } +} + +/// One signed map: `value = sum_i digit_i * 2^(b*i) - offset`. +/// +/// The exact accepted interval is `[-offset, offset-1]`. The magnitude used +/// for no-wrap admission is `offset`, the larger absolute endpoint. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct LabiniusSignedDigitRange { + bits: u32, + digit_count: usize, + offset: u128, + interval: (i128, i128), +} + +impl LabiniusSignedDigitRange { + /// Enforced bit width `e`. + pub const fn bits(self) -> u32 { + self.bits + } + /// Number of digits `e/b`. + pub const fn digit_count(self) -> usize { + self.digit_count + } + /// Signed offset and enforced magnitude `2^(e-1)`. + pub const fn offset(self) -> u128 { + self.offset + } + /// Inclusive accepted endpoints. + pub const fn interval(self) -> (i128, i128) { + self.interval + } +} + +/// Accepted integer ranges and natural/padded lengths for the root digit vector. +/// +/// Segment order is response, parity quotient, parity carry. Within-segment +/// address order belongs to the lowered relation. All padded digits have the +/// same alphabet, zero public relation weights and honest value zero. The image +/// is a coefficient-field vector and needs no range proof. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct LabiniusRootEncoding { + base: LabiniusDigitBase, + response: LabiniusSignedDigitRange, + quotient: LabiniusSignedDigitRange, + carry: LabiniusSignedDigitRange, + no_wrap_total: u128, + segment_lengths: [usize; 3], + natural_len: usize, + padded_log_len: usize, + image_padded_log_len: usize, +} + +impl LabiniusRootEncoding { + /// Selected digit alphabet. + pub const fn base(&self) -> LabiniusDigitBase { + self.base + } + /// Accepted response map. + pub const fn response(&self) -> LabiniusSignedDigitRange { + self.response + } + /// Accepted parity quotient map. + pub const fn quotient(&self) -> LabiniusSignedDigitRange { + self.quotient + } + /// Accepted parity carry map. + pub const fn carry(&self) -> LabiniusSignedDigitRange { + self.carry + } + /// Checked `H + 3*quotient.offset + 2*carry.offset`, strictly below P. + pub const fn no_wrap_total(&self) -> u128 { + self.no_wrap_total + } + /// Natural digit lengths, in response/quotient/carry order. + pub const fn segment_lengths(&self) -> [usize; 3] { + self.segment_lengths + } + /// Sum of the three natural segment lengths. + pub const fn natural_len(&self) -> usize { + self.natural_len + } + /// Smallest `n` with `2^n >= natural_len`. + pub const fn padded_log_len(&self) -> usize { + self.padded_log_len + } + /// Smallest `n` with `2^n >= shape.image_len`. + pub const fn image_padded_log_len(&self) -> usize { + self.image_padded_log_len + } +} + +impl LabiniusRootShape { + /// Derive enforced ranges and witness lengths for one digit alphabet. + /// No allocation occurs; overflow or unsupported accepted intervals reject. + pub fn derive_encoding( + &self, + base: LabiniusDigitBase, + ) -> Result { + let (lower, upper) = self.response_interval; + let offset = lower.unsigned_abs(); + if lower >= 0 || !offset.is_power_of_two() { + return Err(AkitaError::InvalidSetup( + "LaBinius response interval is not a centered power of two".into(), + )); + } + let response_bits = offset.trailing_zeros().checked_add(1).ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius response bit width overflow".into()) + })?; + let response = signed_digit_range(response_bits, base)?; + if response.interval != (lower, upper) { + return Err(AkitaError::InvalidSetup( + "LaBinius response interval is not a centered power of two".into(), + )); + } + let quotient = envelope_for_bound(self.honest_quotient_bound, base)?; + let carry = envelope_for_bound(self.honest_carry_bound, base)?; + self.check_parity_no_wrap(quotient.offset, carry.offset)?; + let no_wrap_total = + parity_no_wrap_total(self.parity_residual_bound, quotient.offset, carry.offset) + .ok_or_else(|| { + AkitaError::InvalidSetup("LaBinius parity no-wrap sum overflow".into()) + })?; + let size_overflow = + || AkitaError::InvalidSetup("LaBinius root digit witness size overflow".into()); + let segment_lengths = [ + checked::product([ + self.ring_elements_per_column, + self.commitment_degree, + response.digit_count, + ]) + .ok_or_else(size_overflow)?, + checked::product([ + self.scalar_degree + .checked_sub(1) + .ok_or_else(size_overflow)?, + quotient.digit_count, + ]) + .ok_or_else(size_overflow)?, + checked::product([self.scalar_degree, carry.digit_count]).ok_or_else(size_overflow)?, + ]; + let natural_len = checked::sum(segment_lengths).ok_or_else(size_overflow)?; + let padded_log_len = checked::ceil_log2(natural_len).ok_or_else(size_overflow)?; + let image_padded_log_len = checked::ceil_log2(self.image_len).ok_or_else(size_overflow)?; + Ok(LabiniusRootEncoding { + base, + response, + quotient, + carry, + no_wrap_total, + segment_lengths, + natural_len, + padded_log_len, + image_padded_log_len, + }) + } +} + +// Canonical signed map metadata, shared by all three integer families. +fn signed_digit_range( + bits: u32, + base: LabiniusDigitBase, +) -> Result { + if bits == 0 || !bits.is_multiple_of(base.bits()) { + return Err(AkitaError::InvalidSetup( + "LaBinius enforced bits must be a positive multiple of digit bits".into(), + )); + } + let overflow = || AkitaError::InvalidSetup("LaBinius signed digit range overflow".into()); + let offset = 1u128 + .checked_shl(bits.checked_sub(1).ok_or_else(overflow)?) + .ok_or_else(overflow)?; + let upper = + i128::try_from(offset.checked_sub(1).ok_or_else(overflow)?).map_err(|_| overflow())?; + let lower = upper + .checked_neg() + .and_then(|v| v.checked_sub(1)) + .ok_or_else(overflow)?; + let digit_count = checked::exact_div( + usize::try_from(bits).map_err(|_| overflow())?, + usize::try_from(base.bits()).map_err(|_| overflow())?, + ) + .ok_or_else(overflow)?; + Ok(LabiniusSignedDigitRange { + bits, + digit_count, + offset, + interval: (lower, upper), + }) +} + +fn envelope_for_bound( + bound: u128, + base: LabiniusDigitBase, +) -> Result { + let overflow = || AkitaError::InvalidSetup("LaBinius honest digit envelope overflow".into()); + let required = bound + .checked_mul(2) + .and_then(|v| v.checked_add(1)) + .ok_or_else(overflow)?; + let bits = u128::BITS + .checked_sub( + required + .checked_sub(1) + .ok_or_else(overflow)? + .leading_zeros(), + ) + .ok_or_else(overflow)? + .max(1); + let digit_bits = usize::try_from(base.bits()).map_err(|_| overflow())?; + let rounded_bits = checked::product([ + checked::div_ceil(usize::try_from(bits).map_err(|_| overflow())?, digit_bits) + .ok_or_else(overflow)?, + digit_bits, + ]) + .ok_or_else(overflow)?; + signed_digit_range(u32::try_from(rounded_bits).map_err(|_| overflow())?, base) +} + +#[cfg(test)] +#[path = "root_encoding_tests.rs"] +mod tests; diff --git a/crates/akita-params/src/sis/labinius/root_encoding_tests.rs b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs new file mode 100644 index 000000000..b18fc183b --- /dev/null +++ b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs @@ -0,0 +1,292 @@ +use super::*; +use crate::sis::labinius::{LabiniusCoefficientPrime, LabiniusRootProfile}; + +const PROFILE: LabiniusRootProfile = LabiniusRootProfile::D648P128BoundedW46Delta16; +const BASES: [LabiniusDigitBase; 3] = [ + LabiniusDigitBase::Bits1, + LabiniusDigitBase::Bits2, + LabiniusDigitBase::Bits4, +]; + +#[test] +fn golden_enforced_ranges_and_root_witness_lengths() { + let shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + let expected = [ + ( + 39, + 38, + 1186484727296, + [42_467_328, 6_279, 6_156], + 42_479_763, + 26, + ), + ( + 40, + 38, + 2011118448128, + [21_233_664, 3_220, 3_078], + 21_239_962, + 25, + ), + ( + 40, + 40, + 2835752168960, + [10_616_832, 1_610, 1_620], + 10_620_062, + 24, + ), + ]; + for (base, (eq, ek, total, lengths, natural, padded)) in BASES.into_iter().zip(expected) { + let encoding = shape.derive_encoding(base).unwrap(); + assert_eq!(encoding.base(), base); + assert_eq!(encoding.response().bits(), 16); + assert_eq!(encoding.response().interval(), PROFILE.response_interval()); + assert_eq!(encoding.response().offset(), 32_768); + assert_eq!(encoding.quotient().bits(), eq); + assert_eq!(encoding.carry().bits(), ek); + assert_eq!(encoding.no_wrap_total(), total); + assert_eq!(encoding.segment_lengths(), lengths); + assert_eq!(encoding.natural_len(), natural); + assert_eq!(encoding.padded_log_len(), padded); + assert_eq!(shape.image_len(), 165_888); + assert_eq!(encoding.image_padded_log_len(), 18); + for (range, honest) in [ + ( + encoding.response(), + u128::try_from(shape.fold_width()).unwrap() * 92, + ), + (encoding.quotient(), shape.honest_quotient_bound()), + (encoding.carry(), shape.honest_carry_bound()), + ] { + let honest = i128::try_from(honest).unwrap(); + let (lower, upper) = range.interval(); + assert!(lower <= -honest && honest <= upper); + assert_eq!( + range.digit_count(), + usize::try_from(range.bits() / base.bits()).unwrap() + ); + } + } +} + +// Pure scalar map; iterates only the digits of one integer, not a root vector. +fn map_uniform_digit( + range: LabiniusSignedDigitRange, + base: LabiniusDigitBase, + digit: u128, +) -> i128 { + let mut encoded = 0u128; + for i in 0..range.digit_count() { + encoded += digit << (u32::try_from(i).unwrap() * base.bits()); + } + i128::try_from(encoded).unwrap() - i128::try_from(range.offset()).unwrap() +} + +#[test] +fn every_integer_family_uses_the_same_exact_signed_digit_map() { + let shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + for base in BASES { + let encoding = shape.derive_encoding(base).unwrap(); + for range in [encoding.response(), encoding.quotient(), encoding.carry()] { + let (lower, upper) = range.interval(); + assert_eq!(map_uniform_digit(range, base, 0), lower); + assert_eq!( + map_uniform_digit(range, base, (1u128 << base.bits()) - 1), + upper + ); + } + } +} + +#[test] +fn digit_base_tags_and_envelope_minimality_are_checked() { + for base in BASES { + assert_eq!(LabiniusDigitBase::from_tag(base.tag()).unwrap(), base); + for honest in [ + 0, + 1, + 2, + 3, + 7, + 8, + 15, + 16, + 127, + 128, + 1_024, + (1u128 << 126) - 1, + ] { + let range = envelope_for_bound(honest, base).unwrap(); + let required = 2 * honest + 1; + assert!( + (num_bigint::BigUint::from(1u8) << range.bits()) + >= num_bigint::BigUint::from(required) + ); + if range.bits() > base.bits() { + assert!((1u128 << (range.bits() - base.bits())) < required); + } + assert!(range.offset() > honest); + } + assert!(envelope_for_bound(u128::MAX, base).is_err()); + assert!(signed_digit_range(0, base).is_err()); + assert!(signed_digit_range(132, base).is_err()); + } + for tag in 3..=u8::MAX { + assert!(matches!( + LabiniusDigitBase::from_tag(tag), + Err(AkitaError::InvalidSetup(_)) + )); + } + let widest = signed_digit_range(128, LabiniusDigitBase::Bits4).unwrap(); + assert_eq!(widest.interval(), (i128::MIN, i128::MAX)); +} + +fn custom_shape( + prime: LabiniusCoefficientPrime, + interval: (i128, i128), + log_n: u32, + log_c: u32, +) -> Result { + super::super::derive_shape( + PROFILE, + prime, + PROFILE.ring_degree(), + &PROFILE.challenge_profile()?, + interval, + log_n, + log_c, + 0, + ) +} + +#[test] +fn incompatible_response_intervals_and_digit_divisibility_reject() { + for interval in [(-32_768, 32_768), (-32_767, 32_767)] { + let shape = custom_shape(PROFILE.coefficient_prime(), interval, 2, 0).unwrap(); + for base in BASES { + assert!(matches!( + shape.derive_encoding(base), + Err(AkitaError::InvalidSetup(_)) + )); + } + } + let odd_bits = custom_shape(PROFILE.coefficient_prime(), (-16_384, 16_383), 2, 0).unwrap(); + odd_bits.derive_encoding(LabiniusDigitBase::Bits1).unwrap(); + for base in [LabiniusDigitBase::Bits2, LabiniusDigitBase::Bits4] { + assert!(matches!( + odd_bits.derive_encoding(base), + Err(AkitaError::InvalidSetup(_)) + )); + } +} + +#[test] +fn rounded_no_wrap_rejects_after_an_internal_prime_perturbation() { + // Derive an admitted P128 shape, then isolate the envelope gate at P64. + // This perturbed shape is test-only: P64's SIS cells cannot admit its width. + let interval = (-(1i128 << 31), (1i128 << 31) - 1); + let mut shape = custom_shape(PROFILE.coefficient_prime(), interval, 22, 0).unwrap(); + shape.coefficient_prime = LabiniusCoefficientPrime::P64Offset23703; + shape + .check_parity_no_wrap(shape.honest_quotient_bound(), shape.honest_carry_bound()) + .unwrap(); + for base in BASES { + match shape.derive_encoding(base) { + Err(AkitaError::InvalidSetup(message)) => { + assert!(message.contains("H + 3*B_Q + 2*B_K < P")) + } + other => panic!("expected rounded-envelope rejection, got {other:?}"), + } + } + // The adjacent power-of-two geometry remains inside the rounded envelope. + let mut smaller = custom_shape(PROFILE.coefficient_prime(), interval, 21, 0).unwrap(); + smaller.coefficient_prime = LabiniusCoefficientPrime::P64Offset23703; + smaller.derive_encoding(LabiniusDigitBase::Bits1).unwrap(); + assert!(custom_shape(LabiniusCoefficientPrime::P64Offset23703, interval, 22, 0).is_err()); +} + +#[test] +fn nearest_certified_envelope_boundary_for_supported_primes() { + let challenge = PROFILE.challenge_profile().unwrap(); + let mut largest_p64 = 0; + // These cover every centered interval and dyadic geometry the D648 cells + // can admit: e>=33 exceeds every certified norm; M>=2^33 exceeds every + // certified width; C>=2^25 cannot fit any covered honest response interval. + for prime in [ + LabiniusCoefficientPrime::P64Offset23703, + PROFILE.coefficient_prime(), + ] { + for bits in 1..=32 { + let offset = 1i128 << (bits - 1); + for log_m in 2..=32 { + for log_c in 0..=24 { + let Ok(shape) = super::super::derive_shape( + PROFILE, + prime, + PROFILE.ring_degree(), + &challenge, + (-offset, offset - 1), + log_m + log_c, + log_c, + 0, + ) else { + continue; + }; + shape + .check_parity_no_wrap( + shape.honest_quotient_bound(), + shape.honest_carry_bound(), + ) + .unwrap(); + for base in BASES { + if bits % base.bits() != 0 { + continue; + } + let encoding = shape.derive_encoding(base).unwrap(); + if prime == LabiniusCoefficientPrime::P64Offset23703 { + largest_p64 = largest_p64.max(encoding.no_wrap_total()); + } + } + } + } + } + } + let nearest = custom_shape( + LabiniusCoefficientPrime::P64Offset23703, + (-(1i128 << 31), (1i128 << 31) - 1), + 40, + 24, + ) + .unwrap(); + assert_eq!(nearest.scalars_per_column(), 1 << 16); + let total = nearest + .derive_encoding(LabiniusDigitBase::Bits4) + .unwrap() + .no_wrap_total(); + assert_eq!(total, 1_824_239_324_833_513_472); + assert_eq!(total, largest_p64); + assert!(total < LabiniusCoefficientPrime::P64Offset23703.modulus()); +} + +#[test] +fn range_and_witness_overflows_reject_without_allocation() { + let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + shape.honest_quotient_bound = u128::MAX; + assert!(matches!( + shape.derive_encoding(LabiniusDigitBase::Bits1), + Err(AkitaError::InvalidSetup(_)) + )); + let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + shape.ring_elements_per_column = usize::MAX; + assert!(matches!( + shape.derive_encoding(LabiniusDigitBase::Bits1), + Err(AkitaError::InvalidSetup(_)) + )); + let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + shape.image_len = usize::MAX; + assert!(matches!( + shape.derive_encoding(LabiniusDigitBase::Bits1), + Err(AkitaError::InvalidSetup(_)) + )); +} diff --git a/crates/akita-params/src/sis/labinius/root_shape.rs b/crates/akita-params/src/sis/labinius/root_shape.rs index 4d2b6df0e..d3a781a0d 100644 --- a/crates/akita-params/src/sis/labinius/root_shape.rs +++ b/crates/akita-params/src/sis/labinius/root_shape.rs @@ -10,6 +10,8 @@ use super::{ #[derive(Debug, Clone, PartialEq, Eq)] pub struct LabiniusRootShape { profile: LabiniusRootProfile, + coefficient_prime: LabiniusCoefficientPrime, + response_interval: (i128, i128), num_cells: usize, fold_width: usize, scalars_per_column: usize, @@ -62,14 +64,13 @@ impl LabiniusRootShape { "LaBinius parity carry envelope is below the honest bound".into(), )); } - let total = enforced_quotient_bound - .checked_mul(3) - .and_then(|q| self.parity_residual_bound.checked_add(q)) - .and_then(|hq| enforced_carry_bound.checked_mul(2)?.checked_add(hq)) - .ok_or_else(|| { - AkitaError::InvalidSetup("LaBinius parity no-wrap sum overflow".into()) - })?; - if total >= self.profile.coefficient_prime().modulus() { + let total = parity_no_wrap_total( + self.parity_residual_bound, + enforced_quotient_bound, + enforced_carry_bound, + ) + .ok_or_else(|| AkitaError::InvalidSetup("LaBinius parity no-wrap sum overflow".into()))?; + if total >= self.coefficient_prime.modulus() { return Err(AkitaError::InvalidSetup( "LaBinius parity envelopes do not satisfy H + 3*B_Q + 2*B_K < P".into(), )); @@ -247,11 +248,13 @@ fn derive_shape( .checked_mul(2) .ok_or_else(parity_overflow)?; let honest_carry_bound = parity_residual_bound - .checked_mul(5) + .checked_mul(3) .ok_or_else(parity_overflow)? / 2; Ok(LabiniusRootShape { profile, + coefficient_prime: prime, + response_interval: interval, num_cells, fold_width, scalars_per_column, @@ -275,3 +278,13 @@ mod parity_tests; #[cfg(test)] #[path = "root_shape_tests.rs"] mod tests; + +// One shared accepted-envelope formula for admission and exposed range totals. +fn parity_no_wrap_total(h: u128, q: u128, k: u128) -> Option { + h.checked_add(q.checked_mul(3)?)? + .checked_add(k.checked_mul(2)?) +} + +#[path = "root_encoding.rs"] +mod root_encoding; +pub use root_encoding::{LabiniusDigitBase, LabiniusRootEncoding, LabiniusSignedDigitRange}; diff --git a/crates/akita-params/src/sis/labinius/root_shape_tests.rs b/crates/akita-params/src/sis/labinius/root_shape_tests.rs index 39db4d172..079d2ad95 100644 --- a/crates/akita-params/src/sis/labinius/root_shape_tests.rs +++ b/crates/akita-params/src/sis/labinius/root_shape_tests.rs @@ -25,7 +25,7 @@ fn golden_shape_and_largest_fold_width() { assert_eq!(shape.a_quotient_len(), 647); assert_eq!(shape.parity_residual_bound(), 86_973_099_520); assert_eq!(shape.honest_quotient_bound(), 173_946_199_040); - assert_eq!(shape.honest_carry_bound(), 217_432_748_800); + assert_eq!(shape.honest_carry_bound(), 130_459_649_280); let maximum = (0..=22) .filter(|&log| LabiniusRootShape::derive(PROFILE, 22, log, 128).is_ok()) .max() diff --git a/specs/labinius-root-admission.md b/specs/labinius-root-admission.md index 0a91a7d0b..5efca1d0a 100644 --- a/specs/labinius-root-admission.md +++ b/specs/labinius-root-admission.md @@ -1,4 +1,4 @@ -# LaBinius binary-root admission +# LaBinius binary-root matrix and shape admission Status: active Book-chapter: book/src/foundations/security.md @@ -96,17 +96,32 @@ Indeed only a quotient coefficient 81 positions higher can affect the next high coefficient. Those higher coefficients have already been assigned their original residual value. Consequently `|q_k| <= 2H`; Q has 161 coefficients. The remainder coefficient at `0 <= j <= 161` is -`r_j - q_j - q_(j-81)`, ignoring quotient indices outside `[0,160]`. Bounding -each quotient term by 2H gives `|remainder_j| <= 5H`. A valid F162 identity -holds exactly when all these remainder coefficients are even: integer division -commutes with reduction modulo two because the divisor is monic. Then K is -half the remainder and is integral, with +`r_j - q_j - q_(j-81)`, ignoring quotient indices outside `[0,160]`. +Substituting the quotient formulas exposes a cancellation: + +```text +rem_j = r_j - r_(j+162) + r_(j+243) for 0 <= j <= 79 +rem_80 = r_80 - r_242 +rem_j = r_j - r_(j+81) for 81 <= j <= 160 +rem_161 = r_161 - r_242. +``` + +For `81 <= j <= 160`, `q_j + q_(j-81) = r_(j+81)`; the two copies +of `r_(j+162)` cancel. Thus the first 80 remainder coefficients have magnitude +at most 3H, and every other coefficient at most 2H. A valid F162 identity holds +exactly when all remainder coefficients are even: integer division commutes +with reduction modulo two because the divisor is monic. Then K is half the +remainder and integral, with ```text B_Q = 2H -B_K = floor(5H/2). +B_K = floor(3H/2). ``` +The independent BigInt long-division oracle checks all 162 closed-form +remainder coefficients on random and extremal relation instances and arbitrary +residual polynomials, including extrema that attain the 3H remainder bound. + These are conservative honest construction bounds. They are not permission to use tighter accepted alphabets in a proof. `check_parity_no_wrap(B_Q', B_K')` requires each caller-supplied magnitude to cover its honest bound and enforces @@ -116,6 +131,82 @@ ensures that a checked residual equality modulo P cannot conceal a nonzero integer coefficient. Rounded digit alphabets must pass their actual enforced magnitudes. An overflow rejects, as does equality at P. +## Enforced signed digits and root witness lengths + +`LabiniusDigitBase` is a closed enum with digit widths `b=1,2,4` and stable tags +0, 1, 2 respectively. Unknown tags reject. `LabiniusRootShape::derive_encoding` +is the single derivation of the accepted integer ranges and witness lengths; +it allocates no vectors. `LabiniusSignedDigitRange` exposes the enforced bit +width e, digit count e/b, signed offset and both inclusive endpoints. +The same signed map applies to response, parity quotient and parity carry: + +```text +value = sum_(i < e/b) digit_i * 2^(b*i) - 2^(e-1) +0 <= digit_i <= 2^b - 1 +accepted interval = [-2^(e-1), 2^(e-1)-1] +enforced magnitude = offset = 2^(e-1). +``` + +The profile response interval must exactly equal that centered power-of-two +interval, with e positive and divisible by b. The current profile has e_v=16 +for every supported base. For the quotient choose the smallest positive multiple +of b satisfying `2^e_Q >= 2*B_Q+1`; choose e_K by the same rule from B_K. +The +1 ensures the positive honest endpoint fits the smaller positive accepted +endpoint. These are accepted power-of-two ranges, rather than the honest +magnitudes. The derivation calls `check_parity_no_wrap` with offsets +`2^(e_Q-1)` and `2^(e_K-1)` and exposes the checked total +`H + 3*2^(e_Q-1) + 2*2^(e_K-1)`. A rounded envelope reaching P rejects even +when the honest envelope would pass. Both paths use the same total formula. + +The natural digit vector W has three consecutive segments, in this order: + +| Segment | Natural digit length | +| --- | --- | +| Response | `m * D * (e_v/b)` | +| Parity quotient | `(d-1) * (e_Q/b)` | +| Parity carry | `d * (e_K/b)` | + +`LabiniusRootEncoding` exposes this ordered length array, its sum, the smallest +padded log n with `2^n >=` that sum, and the analogous padded log of the image +vector. The lowered relation owns segment-internal address order; it is not +fixed here. Products, sums and padding use `akita_error::checked`; range and +no-wrap computations use checked u128 arithmetic. Overflow rejects. + +Every position of the padded digit vector, including padding, is subject to +the same b-bit alphabet check. Public relation weights are zero at every +padding position, and the honest prover writes the zero digit there. Thus a +padding position cannot contribute to any relation row. No selector polynomial +or separate support proof is needed. Zero here means the unsigned digit value +zero, not the lower endpoint of an entire signed integer map. The image vector +is over the coefficient field and needs no range proof. + +At `(log_num_cells, log_fold_width, lambda_fold) = (22,8,128)`, +`B_Q=173946199040` and `B_K=130459649280`. Rounding gives: + +| b | e_Q | e_K | Accepted no-wrap total | Natural W length | Padded log | +| --- | --- | --- | --- | --- | --- | +| 1 | 39 | 38 | 1186484727296 | 42479763 | 26 | +| 2 | 40 | 38 | 2011118448128 | 21239962 | 25 | +| 4 | 40 | 40 | 2835752168960 | 10620062 | 24 | + +The image has 165888 coefficient-field elements and padded log 18. + +Tests exercise rounded rejection by deriving a P128 shape with a signed 32-bit +response interval and `(log_num_cells, log_fold_width)=(22,0)`, then perturbing +only its internal prime to P64. The honest total is 14591662792680407500, +below P64; the b=1 rounded total is 19905910352977592366, above P64. The +adjacent log-size 21 passes at b=1. This isolates the no-wrap gate: the perturbed +larger shape cannot itself pass P64's certified SIS lookup. + +An exhaustive internal search over both supported primes, the covered centered +response intervals and dyadic D648 geometries finds no certified shape whose +honest envelope passes but rounded envelope fails. The nearest certified P64 +boundary has e_v=32, M=2^16, C=2^24, b=4 and rounded total +1824239324833513472, still below `P64=18446744073709527913`. Wider response +intervals exceed the certified norm cells; larger M exceeds certified widths; +larger C violates deterministic honest response admission. This is test-only +parameter exploration, not an additional public profile. + ## Admission order and boundary fixture The canonical derivation applies these gates in order: @@ -129,8 +220,9 @@ The canonical derivation applies these gates in order: 6. Derive image/quotient lengths and honest parity bounds with checked arithmetic. Caller-selected failures use `AkitaError::InvalidSetup`, matching neighbouring -SIS admission. Actual parity range envelopes are checked separately once the -caller chooses an encoding. The sole profile's eta is fixed below P; tests +SIS admission. Actual parity range envelopes are checked by `derive_encoding` when the +caller chooses a digit base, or by `check_parity_no_wrap` for another enforced +envelope. The sole profile's eta is fixed below P; tests perturb internal fields to exercise the ledger boundary without exposing a runtime profile plugin. @@ -168,7 +260,9 @@ binary reduction cover random, extremal, valid and invalid parity rows. ## Remaining protocol work This slice defines no schedule family, proof-size model, Fiat–Shamir ledger, -proof encoding, successor-witness layout, planner integration, or root protocol. -It does not claim complete PCS security admission. Those belong to the root +proof wire grammar, segment-internal addresses, planner integration, or root +protocol. The three digit-segment lengths above do not specify a complete +successor witness. This is not protocol security admission and does not claim +complete PCS security admission. Those belong to the root protocol and its composition with the ordinary tail. No unpublished paper or unlicensed reference implementation is needed for these formulas or tests. From 4d2f34bf9c40bc99eaffa890b0ad34a5f7992a89 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 06:44:03 +0100 Subject: [PATCH 3/6] test(labinius): fixed fixtures for root identity bytes and digit tags Pin the root-profile identity bytes against a hand-assembled byte string and the digit-base tags against literals. Move the root_encoding module declaration and the shared no-wrap helper above the test modules. --- .../src/sis/labinius/root_encoding_tests.rs | 22 +++++++++++++ .../src/sis/labinius/root_profile_tests.rs | 33 +++++++++++++++++++ .../src/sis/labinius/root_shape.rs | 20 +++++------ 3 files changed, 65 insertions(+), 10 deletions(-) diff --git a/crates/akita-params/src/sis/labinius/root_encoding_tests.rs b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs index b18fc183b..238243740 100644 --- a/crates/akita-params/src/sis/labinius/root_encoding_tests.rs +++ b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs @@ -290,3 +290,25 @@ fn range_and_witness_overflows_reject_without_allocation() { Err(AkitaError::InvalidSetup(_)) )); } + +#[test] +fn stable_digit_base_tags_and_bits_have_literal_fixtures() { + assert_eq!(LabiniusDigitBase::Bits1.tag(), 0); + assert_eq!(LabiniusDigitBase::Bits2.tag(), 1); + assert_eq!(LabiniusDigitBase::Bits4.tag(), 2); + assert_eq!( + LabiniusDigitBase::from_tag(0).unwrap(), + LabiniusDigitBase::Bits1 + ); + assert_eq!( + LabiniusDigitBase::from_tag(1).unwrap(), + LabiniusDigitBase::Bits2 + ); + assert_eq!( + LabiniusDigitBase::from_tag(2).unwrap(), + LabiniusDigitBase::Bits4 + ); + assert_eq!(LabiniusDigitBase::Bits1.bits(), 1); + assert_eq!(LabiniusDigitBase::Bits2.bits(), 2); + assert_eq!(LabiniusDigitBase::Bits4.bits(), 4); +} diff --git a/crates/akita-params/src/sis/labinius/root_profile_tests.rs b/crates/akita-params/src/sis/labinius/root_profile_tests.rs index fc5cbedd3..5cccf4440 100644 --- a/crates/akita-params/src/sis/labinius/root_profile_tests.rs +++ b/crates/akita-params/src/sis/labinius/root_profile_tests.rs @@ -116,3 +116,36 @@ fn identity_binds_each_field_independently() { assert_ne!(variant, original); } } + +#[test] +fn root_profile_identity_matches_hand_assembled_stable_fixture() { + let prime = 340282366920938463463374607427473266697u128; + assert_eq!(prime, u128::MAX - (1u128 << 32) + 22538); + let challenge = + BinaryChallengeProfile::bounded_weight(BinaryScalarRing::Cyclotomic243, 46).unwrap(); + let digest: Vec = "0586ee6294846d118d1e6ef364f10c40f8e5678f135f11dcde42b0fb61a89bfd" + .as_bytes() + .chunks_exact(2) + .map(|pair| u8::from_str_radix(std::str::from_utf8(pair).unwrap(), 16).unwrap()) + .collect(); + assert_eq!(digest.len(), 32); + + let mut expected = b"akita/labinius/root-profile/v1\0".to_vec(); + expected.extend_from_slice(&[0, 0]); // Profile tag, then scalar-ring tag. + expected.extend_from_slice(&prime.to_le_bytes()); + expected.extend_from_slice(&648u32.to_le_bytes()); + for &byte in challenge.identity_bytes() { + expected.extend_from_slice(&[1, byte]); + } + expected.push(0); + expected.extend_from_slice(&(-32768i128).to_le_bytes()); + expected.extend_from_slice(&32767i128.to_le_bytes()); + expected.extend_from_slice(&digest); + + assert_eq!( + LabiniusRootProfile::D648P128BoundedW46Delta16 + .identity_bytes() + .unwrap(), + expected + ); +} diff --git a/crates/akita-params/src/sis/labinius/root_shape.rs b/crates/akita-params/src/sis/labinius/root_shape.rs index d3a781a0d..c497aa4f0 100644 --- a/crates/akita-params/src/sis/labinius/root_shape.rs +++ b/crates/akita-params/src/sis/labinius/root_shape.rs @@ -6,6 +6,10 @@ use super::{ LabiniusRingDegree, LabiniusRootProfile, LabiniusSourceComparisonId, SourceOccurrenceBound, }; +#[path = "root_encoding.rs"] +mod root_encoding; +pub use root_encoding::{LabiniusDigitBase, LabiniusRootEncoding, LabiniusSignedDigitRange}; + /// Fully derived and SIS-admitted geometry for the direct binary-root baseline. #[derive(Debug, Clone, PartialEq, Eq)] pub struct LabiniusRootShape { @@ -272,19 +276,15 @@ fn derive_shape( }) } -#[cfg(test)] -#[path = "parity_tests.rs"] -mod parity_tests; -#[cfg(test)] -#[path = "root_shape_tests.rs"] -mod tests; - // One shared accepted-envelope formula for admission and exposed range totals. fn parity_no_wrap_total(h: u128, q: u128, k: u128) -> Option { h.checked_add(q.checked_mul(3)?)? .checked_add(k.checked_mul(2)?) } -#[path = "root_encoding.rs"] -mod root_encoding; -pub use root_encoding::{LabiniusDigitBase, LabiniusRootEncoding, LabiniusSignedDigitRange}; +#[cfg(test)] +#[path = "parity_tests.rs"] +mod parity_tests; +#[cfg(test)] +#[path = "root_shape_tests.rs"] +mod tests; From fed6db8008471078745078fba9268f8dbe40f29c Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 07:24:26 +0100 Subject: [PATCH 4/6] refactor(labinius): root encoding exposes canonical response-table lengths --- .../src/sis/labinius/root_encoding.rs | 118 +++++++++++------- .../src/sis/labinius/root_encoding_tests.rs | 91 +++++++++----- specs/labinius-root-admission.md | 69 ++++++---- 3 files changed, 175 insertions(+), 103 deletions(-) diff --git a/crates/akita-params/src/sis/labinius/root_encoding.rs b/crates/akita-params/src/sis/labinius/root_encoding.rs index 827bfe8f9..13a1a6f33 100644 --- a/crates/akita-params/src/sis/labinius/root_encoding.rs +++ b/crates/akita-params/src/sis/labinius/root_encoding.rs @@ -76,12 +76,15 @@ impl LabiniusSignedDigitRange { } } -/// Accepted integer ranges and natural/padded lengths for the root digit vector. +/// Enforced integer ranges and canonical root response-table lengths. /// -/// Segment order is response, parity quotient, parity carry. Within-segment -/// address order belongs to the lowered relation. All padded digits have the -/// same alphabet, zero public relation weights and honest value zero. The image -/// is a coefficient-field vector and needs no range proof. +/// The committed table contains only response digits, addressed as +/// `digit + digit_count * (coefficient + padded_coefficient_len * ring_element)`. +/// Every position has the same alphabet; padding has zero public relation +/// weights and honest digit zero. Parity quotient and carry lengths count +/// integers outside this table; the root protocol chooses how to enforce their +/// ranges. The image uses the same padded coefficient index over the +/// coefficient field and needs no range proof. #[derive(Debug, Clone, PartialEq, Eq)] pub struct LabiniusRootEncoding { base: LabiniusDigitBase, @@ -89,10 +92,13 @@ pub struct LabiniusRootEncoding { quotient: LabiniusSignedDigitRange, carry: LabiniusSignedDigitRange, no_wrap_total: u128, - segment_lengths: [usize; 3], - natural_len: usize, - padded_log_len: usize, - image_padded_log_len: usize, + padded_coefficient_len: usize, + response_table_len: usize, + response_table_log_len: usize, + parity_quotient_len: usize, + parity_carry_len: usize, + image_table_len: usize, + image_table_log_len: usize, } impl LabiniusRootEncoding { @@ -104,11 +110,11 @@ impl LabiniusRootEncoding { pub const fn response(&self) -> LabiniusSignedDigitRange { self.response } - /// Accepted parity quotient map. + /// Enforced parity quotient range, independent of its protocol representation. pub const fn quotient(&self) -> LabiniusSignedDigitRange { self.quotient } - /// Accepted parity carry map. + /// Enforced parity carry range, independent of its protocol representation. pub const fn carry(&self) -> LabiniusSignedDigitRange { self.carry } @@ -116,21 +122,33 @@ impl LabiniusRootEncoding { pub const fn no_wrap_total(&self) -> u128 { self.no_wrap_total } - /// Natural digit lengths, in response/quotient/carry order. - pub const fn segment_lengths(&self) -> [usize; 3] { - self.segment_lengths + /// Coefficient-axis length `D` rounded up to a power of two. + pub const fn padded_coefficient_len(&self) -> usize { + self.padded_coefficient_len } - /// Sum of the three natural segment lengths. - pub const fn natural_len(&self) -> usize { - self.natural_len + /// Committed response digits `m * padded_coefficient_len * response.digit_count`. + pub const fn response_table_len(&self) -> usize { + self.response_table_len } - /// Smallest `n` with `2^n >= natural_len`. - pub const fn padded_log_len(&self) -> usize { - self.padded_log_len + /// Smallest `n` with `2^n >= response_table_len`. + pub const fn response_table_log_len(&self) -> usize { + self.response_table_log_len } - /// Smallest `n` with `2^n >= shape.image_len`. - pub const fn image_padded_log_len(&self) -> usize { - self.image_padded_log_len + /// Parity quotient integers `d - 1`, outside the committed response table. + pub const fn parity_quotient_len(&self) -> usize { + self.parity_quotient_len + } + /// Parity carry integers `d`, outside the committed response table. + pub const fn parity_carry_len(&self) -> usize { + self.parity_carry_len + } + /// Image field entries `padded_coefficient_len * C * n_A`, with no range proof. + pub const fn image_table_len(&self) -> usize { + self.image_table_len + } + /// Smallest `n` with `2^n >= image_table_len`. + pub const fn image_table_log_len(&self) -> usize { + self.image_table_log_len } } @@ -167,35 +185,43 @@ impl LabiniusRootShape { })?; let size_overflow = || AkitaError::InvalidSetup("LaBinius root digit witness size overflow".into()); - let segment_lengths = [ - checked::product([ - self.ring_elements_per_column, - self.commitment_degree, - response.digit_count, - ]) - .ok_or_else(size_overflow)?, - checked::product([ - self.scalar_degree - .checked_sub(1) - .ok_or_else(size_overflow)?, - quotient.digit_count, - ]) - .ok_or_else(size_overflow)?, - checked::product([self.scalar_degree, carry.digit_count]).ok_or_else(size_overflow)?, - ]; - let natural_len = checked::sum(segment_lengths).ok_or_else(size_overflow)?; - let padded_log_len = checked::ceil_log2(natural_len).ok_or_else(size_overflow)?; - let image_padded_log_len = checked::ceil_log2(self.image_len).ok_or_else(size_overflow)?; + let padded_coefficient_len = self + .commitment_degree + .checked_next_power_of_two() + .ok_or_else(size_overflow)?; + let response_table_len = checked::product([ + self.ring_elements_per_column, + padded_coefficient_len, + response.digit_count, + ]) + .ok_or_else(size_overflow)?; + let response_table_log_len = + checked::ceil_log2(response_table_len).ok_or_else(size_overflow)?; + let parity_quotient_len = self + .scalar_degree + .checked_sub(1) + .ok_or_else(size_overflow)?; + let parity_carry_len = self.scalar_degree; + let image_table_len = checked::product([ + padded_coefficient_len, + self.fold_width, + usize::try_from(self.rank_a).map_err(|_| size_overflow())?, + ]) + .ok_or_else(size_overflow)?; + let image_table_log_len = checked::ceil_log2(image_table_len).ok_or_else(size_overflow)?; Ok(LabiniusRootEncoding { base, response, quotient, carry, no_wrap_total, - segment_lengths, - natural_len, - padded_log_len, - image_padded_log_len, + padded_coefficient_len, + response_table_len, + response_table_log_len, + parity_quotient_len, + parity_carry_len, + image_table_len, + image_table_log_len, }) } } diff --git a/crates/akita-params/src/sis/labinius/root_encoding_tests.rs b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs index 238243740..27cba5e8b 100644 --- a/crates/akita-params/src/sis/labinius/root_encoding_tests.rs +++ b/crates/akita-params/src/sis/labinius/root_encoding_tests.rs @@ -12,32 +12,11 @@ const BASES: [LabiniusDigitBase; 3] = [ fn golden_enforced_ranges_and_root_witness_lengths() { let shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); let expected = [ - ( - 39, - 38, - 1186484727296, - [42_467_328, 6_279, 6_156], - 42_479_763, - 26, - ), - ( - 40, - 38, - 2011118448128, - [21_233_664, 3_220, 3_078], - 21_239_962, - 25, - ), - ( - 40, - 40, - 2835752168960, - [10_616_832, 1_610, 1_620], - 10_620_062, - 24, - ), + (39, 38, 1186484727296, 67_108_864, 26), + (40, 38, 2011118448128, 33_554_432, 25), + (40, 40, 2835752168960, 16_777_216, 24), ]; - for (base, (eq, ek, total, lengths, natural, padded)) in BASES.into_iter().zip(expected) { + for (base, (eq, ek, total, response_len, response_log)) in BASES.into_iter().zip(expected) { let encoding = shape.derive_encoding(base).unwrap(); assert_eq!(encoding.base(), base); assert_eq!(encoding.response().bits(), 16); @@ -46,11 +25,14 @@ fn golden_enforced_ranges_and_root_witness_lengths() { assert_eq!(encoding.quotient().bits(), eq); assert_eq!(encoding.carry().bits(), ek); assert_eq!(encoding.no_wrap_total(), total); - assert_eq!(encoding.segment_lengths(), lengths); - assert_eq!(encoding.natural_len(), natural); - assert_eq!(encoding.padded_log_len(), padded); + assert_eq!(encoding.padded_coefficient_len(), 1024); + assert_eq!(encoding.response_table_len(), response_len); + assert_eq!(encoding.response_table_log_len(), response_log); + assert_eq!(encoding.parity_quotient_len(), 161); + assert_eq!(encoding.parity_carry_len(), 162); assert_eq!(shape.image_len(), 165_888); - assert_eq!(encoding.image_padded_log_len(), 18); + assert_eq!(encoding.image_table_len(), 262_144); + assert_eq!(encoding.image_table_log_len(), 18); for (range, honest) in [ ( encoding.response(), @@ -70,6 +52,31 @@ fn golden_enforced_ranges_and_root_witness_lengths() { } } +#[test] +fn response_table_length_matches_digit_innermost_addresses_and_coefficient_tails() { + for (log_n, log_c, lambda) in [(2, 0, 0), (3, 0, 0), (22, 8, 128)] { + let shape = LabiniusRootShape::derive(PROFILE, log_n, log_c, lambda).unwrap(); + for base in BASES { + let encoding = shape.derive_encoding(base).unwrap(); + let digit_count = usize::try_from(16 / base.bits()).unwrap(); + let degree = shape.commitment_degree(); + let padded_coefficient_len = degree.next_power_of_two(); + // The address rule is increasing in each coordinate, so the natural + // maximum occurs at the last digit, coefficient and ring element. + let largest_natural_address = digit_count - 1 + + digit_count + * (degree - 1 + + padded_coefficient_len * (shape.ring_elements_per_column() - 1)); + let coefficient_tail = (padded_coefficient_len - degree) * digit_count; + assert!(coefficient_tail > 0); + assert_eq!( + largest_natural_address + coefficient_tail, + encoding.response_table_len() - 1 + ); + } + } +} + // Pure scalar map; iterates only the digits of one integer, not a root vector. fn map_uniform_digit( range: LabiniusSignedDigitRange, @@ -284,7 +291,31 @@ fn range_and_witness_overflows_reject_without_allocation() { Err(AkitaError::InvalidSetup(_)) )); let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); - shape.image_len = usize::MAX; + shape.fold_width = usize::MAX; + assert!(matches!( + shape.derive_encoding(LabiniusDigitBase::Bits1), + Err(AkitaError::InvalidSetup(_)) + )); +} + +#[test] +fn coefficient_padding_and_padded_response_product_overflows_reject() { + let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + shape.commitment_degree = usize::MAX; + assert!(matches!( + shape.derive_encoding(LabiniusDigitBase::Bits1), + Err(AkitaError::InvalidSetup(_)) + )); + let mut shape = LabiniusRootShape::derive(PROFILE, 22, 8, 128).unwrap(); + // The natural coefficient product fits, but padding the coefficient axis + // makes the response-table product overflow. + shape.ring_elements_per_column = usize::MAX / (shape.commitment_degree() * 16); + assert!(checked::product([ + shape.ring_elements_per_column(), + shape.commitment_degree(), + 16, + ]) + .is_some()); assert!(matches!( shape.derive_encoding(LabiniusDigitBase::Bits1), Err(AkitaError::InvalidSetup(_)) diff --git a/specs/labinius-root-admission.md b/specs/labinius-root-admission.md index 5efca1d0a..7e89819bb 100644 --- a/specs/labinius-root-admission.md +++ b/specs/labinius-root-admission.md @@ -158,38 +158,53 @@ magnitudes. The derivation calls `check_parity_no_wrap` with offsets `H + 3*2^(e_Q-1) + 2*2^(e_K-1)`. A rounded envelope reaching P rejects even when the honest envelope would pass. Both paths use the same total formula. -The natural digit vector W has three consecutive segments, in this order: +The committed successor table contains only response digits in the canonical +trinomial response layout, `akita_types::TrinomialResponseLayout`: digits are +innermost, then the coefficient index padded to a power of two, then the ring +element index. Its address rule and lengths are -| Segment | Natural digit length | -| --- | --- | -| Response | `m * D * (e_v/b)` | -| Parity quotient | `(d-1) * (e_Q/b)` | -| Parity carry | `d * (e_K/b)` | - -`LabiniusRootEncoding` exposes this ordered length array, its sum, the smallest -padded log n with `2^n >=` that sum, and the analogous padded log of the image -vector. The lowered relation owns segment-internal address order; it is not -fixed here. Products, sums and padding use `akita_error::checked`; range and -no-wrap computations use checked u128 arithmetic. Overflow rejects. - -Every position of the padded digit vector, including padding, is subject to -the same b-bit alphabet check. Public relation weights are zero at every -padding position, and the honest prover writes the zero digit there. Thus a -padding position cannot contribute to any relation row. No selector polynomial -or separate support proof is needed. Zero here means the unsigned digit value -zero, not the lower endpoint of an entire signed integer map. The image vector -is over the coefficient field and needs no range proof. +```text +address = digit + digit_count * (coefficient + padded_coefficient_len * ring_element) +padded_coefficient_len = next_power_of_two(D) +digit_count = e_v/b +response_table_len = m * padded_coefficient_len * digit_count +response_table_log_len = ceil_log2(response_table_len). +``` + +The parity quotient and carry are `d - 1` and `d` integers, respectively, with +the enforced ranges above; they are not part of the committed response table. +The root protocol must enforce those ranges, either by sending the integers in +the clear and checking them directly or by committing digits. Whichever method +it chooses, the no-wrap condition uses the enforced offsets +`2^(e_Q-1)` and `2^(e_K-1)`. + +`LabiniusRootEncoding` exposes the padded coefficient length, response table +length and log length, parity integer counts, and image table length and log +length. Products and padding use `akita_error::checked`; range and no-wrap +computations use checked u128 arithmetic. Overflow rejects. + +Every position of the response table, including coefficient positions `t >= D` +and any positions above the natural extent, is subject to the same b-bit +alphabet check. Public relation weights are zero at every padding position, +and the honest prover writes the zero digit there. Thus a padding position +cannot contribute to any relation row. No selector polynomial or separate +support proof is needed. Zero here means the unsigned digit value zero, not +the lower endpoint of an entire signed integer map. + +The image table uses the same padded coefficient index and has +`padded_coefficient_len * C * n_A` entries over the coefficient field, with no +range proof. At `(log_num_cells, log_fold_width, lambda_fold) = (22,8,128)`, `B_Q=173946199040` and `B_K=130459649280`. Rounding gives: -| b | e_Q | e_K | Accepted no-wrap total | Natural W length | Padded log | +| b | e_Q | e_K | Accepted no-wrap total | Response table length | Response table log length | | --- | --- | --- | --- | --- | --- | -| 1 | 39 | 38 | 1186484727296 | 42479763 | 26 | -| 2 | 40 | 38 | 2011118448128 | 21239962 | 25 | -| 4 | 40 | 40 | 2835752168960 | 10620062 | 24 | +| 1 | 39 | 38 | 1186484727296 | 67108864 | 26 | +| 2 | 40 | 38 | 2011118448128 | 33554432 | 25 | +| 4 | 40 | 40 | 2835752168960 | 16777216 | 24 | -The image has 165888 coefficient-field elements and padded log 18. +This gives image table length 262144, log 18. Tests exercise rounded rejection by deriving a P128 shape with a signed 32-bit response interval and `(log_num_cells, log_fold_width)=(22,0)`, then perturbing @@ -261,8 +276,8 @@ binary reduction cover random, extremal, valid and invalid parity rows. This slice defines no schedule family, proof-size model, Fiat–Shamir ledger, proof wire grammar, segment-internal addresses, planner integration, or root -protocol. The three digit-segment lengths above do not specify a complete -successor witness. This is not protocol security admission and does not claim +protocol. The lengths above fix the committed table's size but not the relation +over it. This is not protocol security admission and does not claim complete PCS security admission. Those belong to the root protocol and its composition with the ordinary tail. No unpublished paper or unlicensed reference implementation is needed for these formulas or tests. From 991b6765188054a53c9495744c487378ce535cf8 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 07:35:13 +0100 Subject: [PATCH 5/6] docs(labinius): root-admission spec states the address rule and checked helpers precisely --- specs/labinius-root-admission.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/specs/labinius-root-admission.md b/specs/labinius-root-admission.md index 7e89819bb..adc1f802d 100644 --- a/specs/labinius-root-admission.md +++ b/specs/labinius-root-admission.md @@ -180,8 +180,9 @@ it chooses, the no-wrap condition uses the enforced offsets `LabiniusRootEncoding` exposes the padded coefficient length, response table length and log length, parity integer counts, and image table length and log -length. Products and padding use `akita_error::checked`; range and no-wrap -computations use checked u128 arithmetic. Overflow rejects. +length. Coefficient padding uses checked integer rounding, products and log +rounding use `akita_error::checked`, and range and no-wrap computations use +checked u128 arithmetic. Overflow rejects. Every position of the response table, including coefficient positions `t >= D` and any positions above the natural extent, is subject to the same b-bit @@ -275,9 +276,10 @@ binary reduction cover random, extremal, valid and invalid parity rows. ## Remaining protocol work This slice defines no schedule family, proof-size model, Fiat–Shamir ledger, -proof wire grammar, segment-internal addresses, planner integration, or root -protocol. The lengths above fix the committed table's size but not the relation -over it. This is not protocol security admission and does not claim +proof wire grammar, representation of the parity quotient and carry, planner +integration, or root protocol. The response table's address rule and the +lengths above fix the committed table's size and index order but not the +relation over it. This is not protocol security admission and does not claim complete PCS security admission. Those belong to the root protocol and its composition with the ordinary tail. No unpublished paper or unlicensed reference implementation is needed for these formulas or tests. From 148b600896cab206d910dc4b23d6464e785008b9 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 9 Oct 2026 16:06:11 +0100 Subject: [PATCH 6/6] docs(labinius): root-admission spec header in the template table, owned by the security chapter --- specs/labinius-root-admission.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/specs/labinius-root-admission.md b/specs/labinius-root-admission.md index adc1f802d..c117b6686 100644 --- a/specs/labinius-root-admission.md +++ b/specs/labinius-root-admission.md @@ -1,8 +1,14 @@ # LaBinius binary-root matrix and shape admission -Status: active -Book-chapter: book/src/foundations/security.md -Tracking: https://github.com/LayerZero-Labs/akita/issues/45 +| Field | Value | +|---|---| +| Author(s) | Quang Dao | +| Created | 2026-10-09 | +| Status | active | +| PR | #199 | +| Book-chapter | book/src/how/security.md | + +Tracking issue: https://github.com/LayerZero-Labs/akita/issues/45 ## Scope and profile