Skip to content

Conversation

@d0cd
Copy link
Collaborator

@d0cd d0cd commented Dec 11, 2025

TODO

  • Resolve merge conflicts after all V13 changes are merged.
  • Complete the VK migration PR.
  • Complete the field-based identifier PR
  • Prepare the deployment cannon.
  • Upload parameters for the credits.aleo record translation keys.
  • Dynamic futures should be displayed on the Explorer in a human readable way.
  • Update developer docs.
  • Run regressions.
    • Number of programs with records
      • mainnet: 81 programs, 117 records total
      • testnet: 1097 programs, 1790 records total
      • canary: 3 programs, 3 records total
    • The modified cost calculation produces the same cost as snarkVM 4.4.0

For Reviewers

  • Do we actually want to disallow re-entrancy at the VM layer?
    • @d0cd's viewpoint. We currently disallow re-entrancy at the granularity of (program, function). However this permits re-entrancy across different functions within a program. It's not sufficient to disallow re-entrancy at the program layer either, since it would be a severe restriction on developers. An alternate solution is for a compiler to introduce re-entrant locks.
  • Is a single field element sufficient for identifier uniqueness?
  • Should caller metadata be included in the transition ID computation?
  • Are there better names for this instruction?
  • Is local record consumption the expected behavior in recursive calls?

You may find these questions in context by grepping for @reviewers.

Summary

Implements ARC-0009: Dynamic Dispatch for ConsensusVersion::V14.


Implementation Overview

1. Console Data Types (console/program/src/data/dynamic/)

DynamicRecord represents a static record as a fixed-size Merkle commitment.
It stores the owner, a Merkle root of the record entries, the nonce, and the version.
The from_record() method builds a depth-5 tree (max 32 entries) using Poseidon8 for leaf hashes and Poseidon2 for path nodes.
The optional data field holds the full entry map when available for extraction.

DynamicFuture represents a future as a fixed-size Merkle commitment.
It stores the program name, network, and function name as field elements, plus a Merkle root of the arguments.
The from_future() method builds a depth-4 tree (max 16 arguments) using the same hash scheme.
Field encoding of identifiers enables runtime resolution without variable-size strings.

2. Circuit Types (circuit/program/src/data/dynamic/)

circuit::DynamicRecord mirrors the console type with circuit-native field representations.
It optionally stores the console data for ejection.
The from_record() method performs in-circuit Merkle tree construction.
The find() method verifies a Merkle path to a specific entry and returns the entry value.

circuit::DynamicFuture mirrors the console type for circuit verification.
It optionally stores the console arguments for ejection.

3. Request and Transition Versioning

Request (console/program/src/request/) is now versioned.
V1 requests represent static calls with no dynamic flag.
V2 requests add an optional dynamic flag and methods caller_inputs() and caller_input_ids() that convert record inputs to their dynamic representations.

Transition (ledger/block/src/transition/) is now versioned.
V2 transitions include TransitionCallerMetadata containing the caller's view of inputs and outputs.
This metadata is essential because the caller sees static records while the callee sees dynamic records.
Translation proofs use this dual view to verify record equivalence.

Both versions of requests and transitions are supported.

4. Instructions (synthesizer/program/src/logic/instruction/operation/)

call.dynamic (call/dynamic.rs) enables runtime function dispatch.
The first three operands specify the program name, network, and function name as field elements.
Subsequent operands are the function arguments.
Records are automatically converted to dynamic records at call boundaries.
Destinations receive plaintexts, dynamic records, or dynamic futures.

get.record.dynamic (get_record_dynamic.rs) extracts an entry from a dynamic record.
In evaluate mode, it retrieves the entry from the data map.
In execute mode, it constructs the expected leaf hash and verifies a Merkle path against the record's root.

5. Execution (synthesizer/process/src/stack/call/dynamic.rs)

CallDynamic implements the evaluate() and execute() methods of the CallTrait.
The implementation is similar in structure to the Call, however it does differ non-trivially.
The resolve_dynamic_target() method converts field operands to a program ID and function name.
Dynamic calls to credits.aleo/fee_private and fee_public are blocked.
The collect_input_translations() and collect_output_translations() methods identify records that require translation proofs.

6. Translation Proofs (synthesizer/process/src/trace/translation/)

Translation proofs verify that a dynamic record and static record represent the same underlying data.

RecordTranslationData captures the metadata for one translation: both record forms, the function ID, whether it is an input or output, and the computed IDs for each form.

TranslationAssignment (assignment.rs) defines the translation circuit.
The circuit proves that the owner, nonce, and version match, and that the Merkle root of the static record entries equals the dynamic record's root.

prepare.rs handles key synthesis for translation circuits, with separate paths for regular calls and fee operations.

7. Varuna Integration (algorithms/src/snark/varuna/)

Translation proofs are batched with execution proofs in prove_batch_with_terminator().
The Translation struct in synthesizer/process/src/trace/translation/mod.rs generates verifier inputs by matching caller and callee views across transitions.

8. Dynamic Mapping Operations (synthesizer/program/src/logic/command/)

These finalize-time commands access mappings using runtime-resolved program IDs.

contains.dynamic checks if a key exists in an external mapping.
get.dynamic retrieves a value from an external mapping, failing if the key is absent.
get.or_use.dynamic retrieves a value with a fallback default if the key is absent.

Each command takes field operands for the program name, network, and mapping name, plus the key operand.


Tests (synthesizer/src/vm/tests/test_v14/)

File Coverage
call_dynamic.rs Call patterns including credits.aleo transfers, AMM swaps, conditional execution, deep call hierarchies, circular calls, fee function restrictions, and closure rejection
dynamic_futures.rs Await ordering, nested futures, finalize failures, type/mode mismatches, double-await detection, and skipped await detection
dynamic_mapping_operations.rs External and local mapping access, type validation, non-existent mappings, and struct values
get_record_dynamic.rs Polymorphic entry extraction, Merkle verification, boundary indices, and credits.aleo record handling
translation.rs Input/output translations, chained translations, key differentiation across programs, and tampered metadata detection
recursion.rs Self-recursive calls and double-spend detection across static/dynamic record consumption patterns
cast.rs Circuit and console DynamicRecord::from_record() consistency, external and non-external record casting
mixed.rs Cost estimation with translation proofs, combined translation/cast/extraction scenarios

Appended: an overview of semver breaking changes from commit 44644ef
semver_checks_results.txt

Antonio95 and others added 30 commits November 10, 2025 16:27
…ation

Translation circuit for dynamic dispatch
number_of_leaves: usize,
}

impl<E: Environment, LH: LeafHash<E, Hash = PH::Hash>, PH: PathHash<E, Hash = Field<E>>, const DEPTH: u8>
Copy link
Collaborator Author

@d0cd d0cd Jan 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code looks similar to native impl, ensure that it is not underconstrained.
@raychu86


/// Asserts whether the underlying constraints of the two assignments are equal
/// regardless of the concrete values taken in the assignments.
pub fn compare_constraints<F: PrimeField>(assignment_1: &Assignment<F>, assignment_2: &Assignment<F>) -> Result<()> {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See if this can be moved under a test flag.


impl<A: Aleo> DynamicRecord<A> {
/// Creates a dynamic record from a static one.
pub fn from_record(record: &Record<A, Plaintext<A>>) -> Result<Self> {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Equivalency test between console and circuit, with constraint counts.

Self::Private(..) => vec.extend_from_slice(&[Boolean::constant(true), Boolean::constant(false)]),
impl<A: Aleo> Entry<A, Plaintext<A>> {
/// Returns this entry as a list of **little-endian** bits, with the specified mode.
pub(super) fn write_bits_le_with_mode(&self, vec: &mut Vec<Boolean<A>>, mode: Mode) {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Concerns on not pinning mode of visibility. Revisit.


impl<A: Aleo> Entry<A, Plaintext<A>> {
/// Returns this entry as a list of field elements, with the specified mode.
pub fn to_fields_with_mode(&self, mode: Mode) -> Vec<Field<A>> {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Concerns on _with_mode. Revist.

/// The signer commitment.
scm: Field<A>,
/// An flag indicating whether or not the request is dynamic.
/// Note that this field is intentionally excluded from the circuit representation and is only used to eject back to the console representation.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use same comment as console implementation.

// Inject the transition view key as `Mode::Private`.
let circuit_tvk = circuit::Field::<A>::new(circuit::Mode::Private, self.tvk);

// TODO (Compute the circuit RVK using the TVK)
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Antonio95 is this a dangling TODO?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(okay this did send me down a rabbithole)

I see the TODO was added by you in e64f0fe213b2a3f3d4f24e382c7771d36f9fa9a4: WIP redesign caller input IDs (Dec 13) when the most of the surrounding code already looked the same as above. It might come from the discussions we had around unsigned caller metadata (which will show up at the end of this message). So just trying to reverse-engineer the TODO: perhaps you were concerned that the rvk is directly fed as a secret witness value instead of being computed inside the circuit. For reference, the current implementation follows the design doc, where the rvk is a private input and cm := commit(program_id, record_name, record_view_key, R_s). The short version of the rest of this message is: I think the rvk is okay and it can't be tampered with; but it would be a way to partially (cf. case i vs. ii below) avoid tampering with tvk, which I think is currently possible.

This is where the prover currently computes the rvk in preparation for the Translation assignment (out-circuit):

https://github.com/ProvableHQ/snarkVM/blob/feat/dynamic-dispatch/synthesizer/process/src/stack/call/dynamic.rs#L545-L565

Making the switch to in-circuit computation wouldn't be too complicated:

  • We'd remove the rvk private circuit input and add a register_index private input
  • We'd perform a couple more in-circuit computations to derive the rvk, the most expensive of which would be a Poseidon permutation with rate 2 involving the tvk.
  • Note the current single tvk private input would split into two, since, in the case of an input translation, the tvk that goes into the computation of dynamic record's input ID is different from the tvk used in the chain of computations tvk -> rvk -> record commitment -> record serial number, the last of which is the public input id_static.

I'd argue that a prover must use the correct rvk (coming from the honest tvk). The train of thought is as follows:

  • The record commitment is satisfies one of the following:
    1. It is a public input itself (more precisely, it is constrained to have the same value as the public input id_static) when the public input is_input is false and the public input static_is_external is false.
    2. It is hashed together with other data (in fn serial_number(...)) into the computation of a public input (more precisely, into the computation of a value which is constrained to have the same value as the public input id_static) when the public input is_input is true and the public input static_is_external is false.
    3. It is irrelevant when when the public input static_is_external is true.
  • Case i corresponds to translation of a non-external static output record (in the callee) to a dynamic one (in the caller). In this case
    • the public input the rvk is tied to in the translation circuit is fed the same record commitment value produced by the (callee) Transition circuit, which in particular is known to satisfy cm := commit(program_id, record_name, record_view_key, R_s) with a correct rvk of the form
      randomizer = hash(tvk, register_index)
      rvk = (owner.to_group() * randomizer).to_x_coordinate()
      
      with the correct tvk. By the collision reistance of the hash function used in cm := commit(...) above, a malicious prover couldn't use an rvk different from the one coming out of the last computation above.
  • The situation in case ii is similar. It corresponds to translation of a dynamic input record (in the caller) to non-external static record (in the callee). By collision-resistance of the hash function used to compute the serial number (which involves the commitment), this is reduced to case ii: rvk must be correct.

However, one can look at the TODO from the opposite side and see it as a way to ensure that the correct tvk is being used when computing the dynamic record's input ID. I think there is some merit to it. Here are my thoughts at the moment:

  • In case i above, nothing prevents a malicious prover from using a dishonest tvk as the private input. This is because the public input id_dynamic is never matched against a value known to have been computed honestly as id_dynamic = HashPSD8(function_id | R_d | tvk | input_output_index). This in turn the case because in case i the dynamic record is a caller input, which means its ID isn't computed in-circuit (unless that of regular Transition inputs, whose IDs are computed in the signature-verification part of the callee's Transition circuit). In this case, the attack of using a malicious tvk would be prevented by the proposed modification above (i. e. adding it to the computation of the rvk) for the reasons explained above.
  • Case ii is even more problematic: again, nothing prevents a malicious prover from using a dishonest tvk for the same reason as in the previous point. However, In this case, the above modification does not prevent the use of a malicious tvk here because, as explained, the "tvk" private variable would split into two: the one used to compute the rvk corresponds to the transition which minted the record; and the one used to compute id_dynamic would still be correspond to the callee in the call that consumes the record. The latter has nothing to be matched against.
  • In case iii above, I think the attack is already prevented by the fact that the same in-circuit private tvk variable is used to compute the dynamic_id and the static_id; and the latter is the ID of an external record known to have been computed honestly.

I think the second point illustrates we need to rethink what the meaning/need for the tvk is as an ingredient of the computation of the ID of a dynamic record, especially as a caller input/output, i. e. when translation is involved (as opposed to a static call passing a dynamic record received as such by the callee, which isn't problematic; or the same situation for outputs). Assuming we want to keep the tvk in the computation, I think some approaches to avoid the attack would be:

  • Changing the meaning of the tvk that goes into the computation of the dynamic record's ID from the current "tvk of the callee in the dynamic call" to "tvk of the transition that produced the original commitment". This would prevent the tvk split mentioned above and I think it, together with the modification proposed above, would avoid the attack. If necessary, we could also play around with having two separate meanings of dynamic-record ID for inputs and outputs (as is already the case for non-external static records)
  • Signing the caller metadata. I know this is a big change we're trying to stay away from, but I do think it would resolve the issue (even without the rvk-computation switch from above) as it would tie the id_dynamic passed to the translation circuit to a value known to have been computed as HashPSD8(function_id | R_d | tvk | input_output_index) with the correct tvk (am I correct in thinking the signature-verification portion of the callee's Transition circuit would ensure this?).

These are my thoughts atm. It's possible I'm missing something or some of the above reasonings/assumptions are incorrect. Happy to discuss this in any form, including on call.

Also a small reminder that changing the Translation circuit would require regeneration of some keys (at least in examples/translation)

/// The name of the static record (to be embedded as a constant).
pub(super) record_name: Identifier<N>,
/// True if translation is happening for an input to `dynamic.call` (static record is being produced) or an output of `dynamic.call` (static record is being consumed).
pub(super) is_input: bool,
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rename to is_to_static.

/// True if translation is happening for an input to `dynamic.call` (static record is being produced) or an output of `dynamic.call` (static record is being consumed).
pub(super) is_input: bool,
/// Whether the value type corresponding to the static record is `Record` or that of an `ExternalRecord`.
pub(super) static_is_external: bool,
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
pub(super) static_is_external: bool,
pub(super) is_external_record: bool,


#[test]
fn test_translation_simple() {
let mut rng = TestRng::default();
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Write a test with credits.aleo

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants