## 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)<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, the last five terms are<br />always greater than the lookup term. It is therefore sufficient to calculate `query` and<br />`lookup`.<br /><br />Six of the twelve descriptor fields are used in those two 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) * 247 = 4940`. 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 />because truncating the positive series and rounding each intermediate value down can only make<br />`b` smaller. The estimator adds one bit only when this lower bound is sufficient to 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 /># Why the other five 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 five 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 />- DEEP: `deep_terms <= 8192` gives `127 - floor(log2(deep)) + deep_pow >= 114`;<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. The composition and DEEP bounds retain a one-bit<br />margin at the edge of the accepted range. DEEP and FRI folding grinding are nonnegative and can<br />only increase those terms, so their minimum occurs at zero grinding.<br /><br />It follows that the minimum of the native seven-term report is the minimum of `query` and<br />`lookup` 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. Taking the minimum 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 /> |