## miden::core::stark::security
| Procedure | Description |
| ----------- | ------------- |
| compute_conjectured_security_level | Computes a proof's conjectured security level from the descriptor returned by the MVM or PVM<br />recursive verifier.<br /><br />level = min(query, lookup, deep)<br /><br />The native security report takes the minimum of seven terms: query sampling, lookup challenges,<br />constraint composition, out-of-domain evaluation, DEEP composition, FRI folding, and the<br />field/hash security cap. Within the bounds enforced by this procedure, constraint composition,<br />out-of-domain evaluation, FRI folding, and the field/hash cap are greater than lookup. DEEP<br />composition can bind, so this procedure calculates `query`, `lookup`, and `deep`.<br /><br />Eight of the twelve descriptor fields are used in those three calculations. The remaining fields<br />are validated before they are discarded. The AIR-shape bounds are assumptions in the proof<br />below, while the grinding bounds match the range accepted by the generic verifier. Lifted STARK<br />currently applies grinding before the DEEP challenge, before each FRI folding challenge, and<br />before query sampling. It does not apply grinding before sampling the lookup challenges, so<br />both verifiers return `lookup_pow_bits = 0` and this procedure requires that value. Keeping the<br />field in the descriptor avoids changing the descriptor layout when lookup grinding is added to<br />the backend.<br /><br /># Query term<br /><br />Each FRI query contributes `BITS_PER_QUERY_FP` Q16 bits. Query grinding contributes an integer<br />number of bits, giving<br /><br />query = floor(num_queries * BITS_PER_QUERY_FP / 2^16) + query_pow_bits<br /><br />exactly as in the native fixed-point calculation.<br /><br /># Lookup term<br /><br />Let<br /><br />A = (max_message_width + 2) * fractions_per_row,<br />q = ceil(log2(A)),<br />R = r_w * 65536 + r_f.<br /><br />`R` is the Q16 correction for lookup fractions consumed once at the proof boundary rather than<br />once per trace row. With these definitions, the whole-bit lookup term is<br /><br />lookup = (127 - q - height - r_w) + delta.<br /><br />The dominance argument constrains the product `A`. Each factor is also limited to 65536 so the<br />multiplication cannot wrap, but the estimator imposes no tighter bound on either factor by<br />itself. The current MVM value is `(16 + 2) * 28 = 504`; the current PVM value is<br />`(18 + 2) * 248 = 4960`. These values are well inside the accepted range of 257 through 65536.<br />For example, a message width of 12 needs only 19 fractions per row to exceed the lower limit.<br />At the current message widths, the upper limit allows 3640 MVM fractions or 3276 PVM fractions.<br />The verifier-specific drift tests derive both factors from the AIRs and check their product<br />against these limits.<br /><br />The value `delta` accounts for the fractional part discarded when the lookup term is converted<br />from Q16 to whole bits. Set `P = 2^q`, `g = P - A`, and<br /><br />s = q * FP_ONE - ceil(FP_ONE * log2(A))<br />= floor(FP_ONE * -log2(1 - g/P)).<br /><br />Here `s` is the Q16 difference between `log2(A)` and the next whole bit. The lookup term's Q16<br />remainder is `FP_ONE - CHALLENGE_FIELD_OFFSET_FP + s - r_f`. Here<br />`CHALLENGE_FIELD_OFFSET_FP = 2` is the difference between `128 * FP_ONE` and the conservative<br />Q16 challenge-field bound used by the native estimator. Consequently,<br /><br />delta = +1 if s >= r_f + CHALLENGE_FIELD_OFFSET_FP (the remainder reaches FP_ONE)<br />delta = -1 if s = 0 and r_f = MAX_Q16_FRACTION (the remainder falls below zero)<br />delta = 0 otherwise.<br /><br />Computing `s` directly would require a fixed-point logarithm. Instead, the procedure computes a<br />lower bound from the first two terms of<br /><br />-log2(1 - x) = log2(e) * (x + x^2/2 + x^3/3 + ...).<br /><br />For `x = g/P` and `t1 = floor(LOG2_E_FP * g / P)`, that lower bound is<br /><br />b = t1 + floor(t1 * g / (2 * P)) <= s,<br /><br />on the accepted coefficient range. `LOG2_E_FP` is rounded up, but the omitted positive series<br />terms exceed that rounding error for every nonzero gap in the accepted range; the exhaustive<br />native test checks the bound at every coefficient. The estimator adds one bit only when it can prove that<br />the native calculation adds it. If the bound is inconclusive, the estimator can be one bit<br />below the native result but never above it. The `-1` case is determined exactly because `s = 0`<br />precisely when `A` is a power of two (`g = 0`). The bound is conclusive for every descriptor<br />currently returned by either verifier, so the MASM and native lookup terms agree there.<br /><br /># DEEP term<br /><br />Let `n = num_deep_terms` and `q = ceil(log2(n))`. The native round subtracts<br />`ceil(log2(n) * FP_ONE)` and the LDE height `height + 3` from the conservative Q16 field size,<br />then adds `deep_pow_bits`. Since `n <= 8192`, every non-power-of-two `n` has at least three Q16<br />units of slack below `q`; the field-size offset is only two units. Thus its whole-bit value is<br /><br />deep = min(127, 124 - q - height + deep_pow_bits + (n is not a power of two)).<br /><br /># Why the other four terms can be omitted<br /><br />Since `A >= 257`, `q` is at least 9. Since `height >= 6`, `r_w >= 0`, and `delta <= 1`,<br /><br />lookup <= 127 - 9 - height + 1 = 119 - height <= 113.<br /><br />Each of the other four terms has a larger lower bound:<br /><br />- out-of-domain: the configured PCS has `log_blowup = 3`. For an AIR whose largest symbolic<br />constraint degree is `M`, Lifted STARK splits the quotient into the smallest power-of-two<br />number of chunks `c` that is at least `max(M - 1, 1)`. The prover and verifier reject the AIR<br />configuration if it requires more than `2^3` chunks. Therefore every proof accepted under<br />this configuration has `M <= 9` and `c <= 8`. The AIRs read the `local` and `next` rows only,<br />so the DEEP-ALI identity is tested at a point where it has degree at most<br />`max(M * (2^height + 1) + 2^height - 1, (c + 1) * 2^height + 1) <= 10 * 2^height + 8`, which<br />`11 * 2^height` bounds for `height >= 3`. Its out-of-domain term is therefore at least<br />`127 - ceil(log2(11)) - height = 123 - height`, which is greater than the lookup bound<br />`119 - height`;<br />- FRI folding: `FRI_FOLDING_BASE_BITS - height + folding_pow >= 122 - height`, above<br />`119 - height`;<br />- composition: `composed <= 8192` gives `127 - floor(log2(composed)) >= 114 > 113`;<br />- collision cap: `SECURITY_CAP_BITS = 127 > 113`, so neither the cap nor a query clamp is<br />needed.<br /><br />Both the out-of-domain and FRI folding terms subtract the same height as the lookup term, so<br />their margins do not shrink for taller traces. Composition retains a one-bit margin at the edge<br />of the accepted range. FRI folding grinding can only increase its term.<br /><br />It follows that the minimum of the native seven-term report is the minimum of `query`, `lookup`,<br />and `deep` throughout the accepted range. The query expression uses the same fixed-point floor as<br />the native calculation. If it exceeds the native cap, the lookup term is already smaller, so<br />omitting that cap cannot change the result. The lookup calculation is exact for both deployed<br />relations and, for any other accepted descriptor, is either exact or one bit lower than the<br />native value. The DEEP calculation is exact over the accepted envelope. Taking the minimum<br />preserves those guarantees.<br /><br /># Contract<br /><br />Every descriptor field is checked before it is used or discarded. The lower bounds on height<br />and the lookup coefficient support the proof that the other terms cannot determine the result.<br />The upper bounds on height, coefficient, and boundary terms keep the arithmetic in range, and<br />the explicit `base >= 2` check validates the lookup subtraction after applying the correction.<br />Requiring zero lookup grinding keeps the native cap irrelevant to the lookup term. An<br />unsupported input traps instead of returning a security level.<br /><br />This is not a general-purpose estimator for caller-assembled parameters. Its input must be the<br />descriptor returned by a successful MVM or PVM recursive verifier, without modification. The<br />procedure is loop-free and has bounded execution cost for every accepted descriptor.<br /><br />The meaning of `num_lookup_boundary_terms` is the same for both relations even though its source<br />differs. The MVM adds the kernel-procedure count to three fixed core-boundary terms. The PVM<br />uses the number of fixed `UintVal` and `EcGroup` messages added at its verifier boundary. The<br />estimator needs only the resulting count. It does not enforce an acceptance policy; the caller<br />compares the returned level with the threshold required by its application.<br /><br />Inputs: [lookup_pow_bits, num_composed_constraints, max_constraint_degree, num_deep_terms,<br />max_message_width, num_lookup_boundary_terms, lookup_fractions_per_row,<br />log_max_height, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...]<br />Outputs: [level, ...]<br /><br />Invocation: exec<br /> |