miden-core-lib 0.24.2

Miden VM core library
Documentation
1
2
3
4
5
6
7

## miden::core::stark::public_inputs
| Procedure | Description |
| ----------- | ------------- |
| process_public_inputs | Processes the public inputs.<br /><br />This is a generic dispatch procedure that calls the instance-specific implementation<br />via `dynexec`. The instance-specific implementation loads fixed-length and variable-length<br />public inputs from the advice stack, reduces the variable-length inputs using auxiliary<br />randomness, and stores everything into the ACE READ section.<br /><br />This involves:<br /><br />1. Loading from the advice stack the fixed-length public inputs and storing them in memory<br />starting from the address pointed to by `public_inputs_address_ptr`.<br />2. Loading from the advice stack the variable-length public inputs, storing them temporarily<br />in memory, and then reducing them to an element in the challenge field using the auxiliary<br />randomness. This reduced value is then used to impose boundary conditions on the relevant<br />auxiliary columns.<br /><br />Note that the fixed-length public inputs are stored as extension field elements while<br />the variable-length ones are stored as base field elements, because the ACE circuit operates<br />only on extension field elements and the latter inputs are not direct inputs to the circuit,<br />i.e., only their reduced values are.<br />Both fixed-length and variable-length public inputs are absorbed into the Fiat-Shamir<br />transcript through the buffered duplex (`random_coin::observe_felt`), in `MultiAir::observe`<br />order, after loading.<br /><br />It is worth noting that:<br /><br />1. Only the fixed-length public inputs are stored for the lifetime of the verification<br />procedure. The variable-length public inputs are stored temporarily, as this simplifies<br />the task of reducing them using the auxiliary randomness. The resulting values from the<br />reductions are stored right after the fixed-length public inputs, in a word-aligned<br />manner and padded with zeros if needed.<br />2. The public inputs address is computed so that we end up with the following memory layout:<br /><br />[..., a_0..a_{m-1}, b_0..b_{n-1}, beta0, beta1, alpha0, alpha1, OOD-start, ...]<br /><br />where:<br /><br />a) [a_0..a_{m-1}] are the fixed-length public inputs stored as extension field elements.<br />This section is double-word-aligned.<br />b) [b_0..b_{n-1}] are the results of reducing the variable-length public inputs using<br />auxiliary randomness. This section is word-aligned.<br />c) [beta0, beta1, alpha0, alpha1] is the auxiliary randomness.<br />d) OOD-start is the first field element of the section containing the OOD evaluations.<br />3. For each bus message in a group in the variable-length public inputs, each message is<br />expected to be padded to the next multiple of 8 and provided in reverse order. This has<br />the benefit of making the reduction using the auxiliary randomness more efficient using<br />`horner_eval_base`.<br /><br />Inputs:  [...]<br />Outputs: [...]<br /><br />Invocation: exec<br /> |
| compute_and_store_public_inputs_address | Computes the addresses where the public inputs are to be stored.<br /><br />In order to call `eval_circuit`, we need to lay out the inputs to the constraint evaluation<br />circuit in a contiguous region of memory (called READ section in the ACE chiplet documentation)<br />right before the region storing the circuit description (called EVAL section).<br /><br />As the number of public inputs is a per-instance parameter, while the sizes of the OOD<br />evaluation frames and the number of auxiliary random values are fixed, we lay out the public<br />inputs right before the auxiliary random values and OOD evaluations.<br />Hence the address where public inputs are stored is computed using a negative offset from the<br />address where the OOD evaluations are stored.<br /><br />We compute two pointers:<br />var_len_ptr = OOD_EVALUATIONS_PTR - 4 - num_var_len_pi_groups * 4<br />pi_ptr      = var_len_ptr - num_fixed_len_pi * 2<br /><br />The `* 4` for VLPI groups provides word-alignment (each group uses 4 base felts = 2 EF<br />slots, even though the reduced value is only 1 EF). The `* 2` for FLPI converts the base<br />felt count to EF slots (each base felt is stored as [val, 0]).<br /><br />The `-4` accounts for the auxiliary randomness word [beta0, beta1, alpha0, alpha1] at<br />AUX_RAND_ELEM_PTR (4 base felts between var_len_ptr and OOD_EVALUATIONS_PTR).<br /><br />The var_len_ptr is the region that will temporarily store the variable-length public inputs<br />and permanently store the results of reducing them by the auxiliary randomness.<br /><br />Inputs:  [num_var_len_pi_groups, num_fixed_len_pi, ...]<br />Outputs: [...]<br /><br />Invocation: exec<br /> |
| load_base_store_extension_double_word | Loads 8 base field elements from the advice stack, stores them as extension field elements<br />in memory, and returns the original base element words on the stack.<br /><br />Transcript absorption is handled separately (see `sys/vm/public_inputs::absorb_public_inputs`),<br />so the caller discards the returned words `A0`/`A1`.<br /><br />Inputs:  [Y, Y, C, ptr, ...]<br />Outputs: [A0, A1, C, ptr + 16, ..]<br /><br />where A0 and A1 are the original base element words (from advice).<br /><br />Invocation: exec<br /> |