p3_security/shape.rs
1//! Protocol-instance shape: data orthogonal to the runtime config.
2
3use p3_air::Air;
4use p3_air::symbolic::{
5 AirLayout, SymbolicAirBuilder, get_all_symbolic_constraints,
6 get_max_constraint_degree_extension,
7};
8use p3_commit::PolynomialSpace;
9use p3_field::{ExtensionField, Field};
10
11/// AIR-derived shape used in DEEP-ALI and composition-error bounds.
12#[derive(Copy, Clone, Debug)]
13pub struct StarkAirParams {
14 pub num_constraints: usize,
15 pub max_constraint_degree: usize,
16 /// Exact number of committed quotient chunks, including ZK degree padding and doubling.
17 pub num_quotient_chunks: usize,
18 /// DEEP-ALI `max_combo`: maximum number of out-of-domain points
19 /// referenced per column (typically 2 for `local`/`next`).
20 pub max_combo: usize,
21}
22
23impl StarkAirParams {
24 /// Derive `num_constraints` and `max_constraint_degree` by symbolically
25 /// evaluating the AIR's constraints. The caller supplies `max_combo`
26 /// (typically `2` for an AIR using `local`/`next` rotations, `1` if
27 /// there is no transition constraint).
28 /// `trace_domain` must be the prover's original trace domain (before ZK padding):
29 /// its selector model and size determine the constraint degree. `is_zk` selects
30 /// the prover's degree padding and quotient-chunk doubling.
31 ///
32 /// # `layout` must include every committed column width
33 ///
34 /// `layout` controls which column widths the symbolic builder allocates
35 /// when evaluating constraints. A base-only layout (e.g.
36 /// `AirLayout::from_air`, which fills only the `BaseAir` widths)
37 /// leaves the permutation / lookup / preprocessed widths at `0`, so
38 /// any constraints over those columns evaluate as identically zero and
39 /// are dropped — resulting in an **overstated** security bound.
40 ///
41 /// For an AIR that uses lookups or other permutation arguments,
42 /// construct the layout with the full set of widths (base + permutation
43 /// + preprocessed). For pure base AIRs, `AirLayout::from_air` is safe.
44 pub fn from_air<F, EF, A>(
45 air: &A,
46 layout: AirLayout,
47 trace_domain: impl PolynomialSpace<Val = F>,
48 max_combo: usize,
49 is_zk: bool,
50 ) -> Self
51 where
52 F: Field,
53 EF: ExtensionField<F>,
54 A: Air<SymbolicAirBuilder<F, EF>>,
55 {
56 let (base, ext) = get_all_symbolic_constraints::<F, EF, A>(air, layout);
57 let num_constraints = base.len() + ext.len();
58 let transition_degree = trace_domain.transition_degree_multiple();
59 let max_constraint_degree = if transition_degree == 0 {
60 // Two-adic periodic columns have trace-size-dependent degrees.
61 get_max_constraint_degree_extension::<F, EF, A>(air, layout, trace_domain.size())
62 } else {
63 // Circle selectors and periodic columns occupy the full trace space.
64 base.iter()
65 .map(|c| c.degree_multiple_with_transition(transition_degree))
66 .chain(
67 ext.iter()
68 .map(|c| c.degree_multiple_with_transition(transition_degree)),
69 )
70 .max()
71 .unwrap_or(0)
72 }
73 .max(1);
74 // The prover sizes the quotient from whichever of the two degrees is larger.
75 //
76 // An undersized hint therefore never shrinks the committed chunk count.
77 let committed_degree = air
78 .max_constraint_degree()
79 .map_or(max_constraint_degree, |hint| {
80 hint.max(max_constraint_degree)
81 });
82 let zk = usize::from(is_zk);
83 let num_quotient_chunks = committed_degree
84 .checked_add(zk)
85 .and_then(|degree| (degree.max(2) - 1).checked_next_power_of_two())
86 .and_then(|chunks| chunks.checked_mul(1 << zk))
87 .unwrap_or(usize::MAX);
88 Self {
89 num_constraints,
90 max_constraint_degree,
91 num_quotient_chunks,
92 max_combo,
93 }
94 }
95}
96
97/// Per-instance shape data not in the protocol params.
98#[derive(Copy, Clone, Debug)]
99pub struct InstanceShape {
100 pub log_trace_length: usize,
101 /// Bit-length of the field FRI/WHIR operates over (typically the
102 /// extension field).
103 pub modulus_bits: usize,
104 /// Collision resistance of the commitment hash, in bits.
105 pub collision_resistance: usize,
106 /// Number of committed codewords random-linear-combined into a single
107 /// low-degree-test instance (trace segments, quotient chunks, …). `1`
108 /// means no batching. Read by the batched-openings proximity term in
109 /// [`crate::stark::proven_security_report`].
110 pub num_batched_functions: usize,
111}