Fix stack handling in casts involving external structs

[Antonio95]

Closes #3330, see details therein.

This PR is in draft mode until a decision is made on consensus gating.

The issue boiled down to the fact that FinalizeTypes::matches_struct (here: https://github.com/ProvableHQ/snarkVM/blob/staging/synthesizer/process/src/stack/finalize_types/matches.rs#L20) only received one stack when actually two separate ones could be involved (one for the target struct and one for the operand(s') struct(s)). The Stack(id) type needs information about the program it refers to in order to be uniquely determined.

This problem had already been detected and fixed for the function (i.e. private) scope, corresponding to RegisterTypes::matches_struct (here: https://github.com/ProvableHQ/snarkVM/blob/staging/synthesizer/process/src/stack/register_types/matches.rs#L20).

This PR fixes the issue by porting those simple changes to FinalizeTypes::matches_struct. It also adds many intentionally designed test cases involving relatively complex casts (in synthesizer/src/vm/tests/test_v18/external_struct_stacks.rs). Aside from the pure struct case, that file includes test functions focused on arrays and records containing external structs. No issues have been found than in FinalizeTypes::matches_struct, but this part of the language is difficult to test exhaustively so we should keep an eye out in the future.

Aside from the fix, the PR includes several non-functional changes to a couple of functions involved in the check to improve code clarity (e.g. renaming the stacks received by matches_struct).

[Copilot]

Pull request overview

This PR fixes finalize-scope type checking for cast instructions involving external structs by ensuring operand type resolution uses the instruction’s stack while struct layout resolution uses the struct-definition stack, aligning FinalizeTypes::matches_struct behavior with the already-correct RegisterTypes::matches_struct.

Changes:

• Update FinalizeTypes::matches_struct to accept two stacks (instruction vs. definition) and use them appropriately during struct-cast checking.
• Clarify stack roles in the parallel RegisterTypes::matches_struct implementation and related type-equivalence plumbing.
• Add comprehensive V18 VM tests covering external-struct casts across structs, arrays, and records.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
synthesizer/src/vm/tests/test_v18/mod.rs	Adds the new V18 test module for external-struct stack/type-check scenarios.
synthesizer/src/vm/tests/test_v18/external_struct_stacks.rs	Introduces extensive VM tests for external-struct casts (function + finalize) including nested member accesses and container types.
synthesizer/program/src/traits/stack_and_registers.rs	Adds clarifying parameter comments for stack-aware type equivalence.
synthesizer/process/src/stack/register_types/matches.rs	Renames/clarifies stack parameters and ensures operand vs. definition stack usage is explicit for struct matching.
synthesizer/process/src/stack/finalize_types/matches.rs	Fixes finalize struct matching by splitting instruction-stack vs. definition-stack responsibilities.
synthesizer/process/src/stack/finalize_types/initialize.rs	Updates struct-cast call sites to pass both stacks into the new finalize matches_struct signature.

Comments suppressed due to low confidence (1)

synthesizer/src/vm/tests/test_v18/external_struct_stacks.rs:409

• Typo/inconsistency in the comment: "finalise/FinaliseType" should be "finalize/FinalizeType".

// Checks that various instances of casts to arrays involving external structs and their members, as
// well as structs having arrays as members, work as expected. This is tested in both the function
// (i.e. private, RegisterType) setting as well as the public (i.e. finalise, FinaliseType) one.

[mohammadfawaz]

Maybe add a rejection case where same-named structs have different member layouts; the current definitions are equivalent, so a stack mix-up could still pass. A constructor or view case would also cover the other scopes sharing FinalizeTypes.

[mohammadfawaz]

Could most cases use Process::add_program instead of full deployment/proof/execution flows? The bug occurs during stack type checking; keeping one end-to-end case and making the rest focused tests would reduce CI time and duplication.

[mohammadfawaz]

Trailing spaces on this blank line can be removed.

[Antonio95]

After the internal discussions on consensus gating, I think I have a solution which is strictly consensus-preserving (i.e. the new code at < V19 runs exactly like the old code) backwards compatibility while not threading the consensus version to any of the delicate internal places we wanted to avoid.

The idea is:

1. The internal call to matches_struct for FinaliseTypes::check_instruction_opcode is left in its new, corrected form (as corrected in the first version of the PR: it receives two stacks and passes the correct values; mirroring its RegisterTypes counterpart).

2. Inside VM::check_transaction, we add one more case to the legacy checks for consensus_version < ConsensusVersion::V19: https://github.com/ProvableHQ/snarkVM/blob/fix/external_struct_stacks/synthesizer/src/vm/verify.rs#L368.

   1. Note this check cannot happen inside synthesizer/program/src/lib.rs, since achieving strict consensus preservation means one truly needs the stack type (which is not available to synthesizer_program: that would create a circular dependency).
   2. For efficiency, this < V19 legacy check is guarded by an instruction-level check on whether any finalize-like scope (finalize, view, constructor) contains a cast-to-external-struct instruction: https://github.com/ProvableHQ/snarkVM/blob/fix/external_struct_stacks/synthesizer/program/src/lib.rs#L1066.
   3. The legacy check performs the minimal amount of work needed to mimic the pre-V19 behaviour: instead of creating a full stack for the program being checked, it creates a lightweight stack and only populates it with the relevant data for the legacy check (mostly, types of output registers in finalise-like scopes). It then goes through every cast-to-external-struct instruction and makes the call finalize_types.matches_struct(&*external_stack,&*external_stack,cast.operands(),struct_,)?;, which exactly mimics the old code (which made a call to the original matches_struct, which received only one Stack: external_stack). Note that other stacks relevant to this check (the external stacks which may have to be explored during type resolution) must exist beforehand and therefore aren’t affected by the fact that, for the current program, we are only building a lightweight stack.

   I’ve implemented this check in as much of a self contained way as possible within VM::check_transaction. This has only required pub-exposing a couple of new things (e.g. methods of FinaliseTypes) in exchange for not having to add the legacy-logic-specific into e.g. FinaliseTypes methods.

Small caveat: The new legacy check has only been added to the verifier side, to VM::check_transaction. Nothing analogous has been added to VM::deploy, which in particular uses the new, correct matches_struct when judging the validity of the deployment it is building (even at ConsensusVersion < V19). This means that a program with a problematic cast-to-external instruction will fail to build the deployment with the old code, but succeed to build it (even at ConsensusVersion < V19) with the new code. From what I have seen, this should not be an issue as we have many other legacy (and the opposite kind) checks we perform in VM::check_transaction and VM::deploy. What matters is that VM::check_transaction has a consistent behaviour.

As part of these latest changes, I have done the following:

1. Checked that all test_v* pass with the new version of the code but always being executed at consensus version < V19 (I simply temporarily added enough space between the test consensus heights for V18 and V19 to ensure the latter was never reached). This is a sanity check that the changes don’t break anything.

2. Expanded test_v19::external_struct_stacks.rs with test cases for the view and constructor scopes.

3. Crucially: checked that, for all test cases in test_v19::external_struct_stacks.rs (new and old), the finalize/view/constructor scopes that are rejected with the new code at consensus version < V19 are exactly the same as those that failed in the old code. This was indeed the case: exactly four out of 33 cases were rejected in the new and old code (views/view_2, constructor/constructor_case_2, only/run_10, only/run_16).

   NB: This can’t be tested with the clean version of the code (since one needs to develop each test finalize/view/constructor scopes separately to see which ones fail), but I left in the commit which enables this: 141bbd4 “temporary changes to print exact rejections”.

   Also, because of the “Small caveat” mentioned earlier, the new-code-vs.-old-code check could not be completely symmetric: in the new code, acceptance rejection was judged based on vm.check_transaction (vm.deploy always succeeds); in the old code, it was based on vm.deploy.

4. Ran timing tests to ensure that pre-V19, the new legacy check doesn’t significantly impact verifying times. In other words, I’ve run check_transaction on the old and new code at pre-V19. I’ve only done so for the external_struct_stacks.rs, (note that, for programs whose finalize scopes don’t cast an external structs, the only new pre-V19 computation is precisely the check of whether they contain any such instructions, which guards the full legacy check). The results are in the attached file (the serial numbers are much more meaningful than the parallel ones, since tests are themselves run in parallel and therefore affect each other’s measurements). The change in verification time (for the accepting cases) between the old and the new code ranges between -8.6% (yes, decrease) and +12.6 (the average is ~0.8%), which means that, random noise aside, the effect of the new check should be negligible (as expected by pure inspection of the code). Let me know if you want more reliable numbers (e.g. benching each case several times to get a less noisy average).

I have not addressed the original review comments yet, will do that shortly.

times.txt

[Copilot]

Pull request overview

Copilot reviewed 11 out of 11 changed files in this pull request and generated no new comments.

Comments suppressed due to low confidence (5)

synthesizer/src/vm/verify.rs:398

• For consensus_version < V19, the legacy gate is intended to mirror the pre-V19 (buggy) cast-to-external-struct check, but check_scope currently calls finalize_types.check_command(...) on every command first. check_command will run the post-fix external-struct cast validation (via FinalizeTypes::check_instruction / matches_struct(stack, external_stack, ...)) and can therefore reject a deployment that the actual pre-V19 logic would have accepted, which is a consensus risk. Consider adding a legacy-only path that accumulates register types while skipping (or using the legacy single-stack version of) the external-struct cast operand check.

                            for command in commands {
                                // This also helps accumulate the types of non-input registers.
                                finalize_types.check_command(stack, positions, command)?;

synthesizer/process/src/stack/finalize_types/initialize.rs:239

• FinalizeTypes::check_input and check_command were made public to support the legacy verification code path. This expands the public API surface of snarkvm_synthesizer_process with methods that look like internal helpers and may be hard to keep stable. Consider keeping these helpers pub(crate) and exposing a single purpose-built API for the legacy pre-V19 check instead.

    /// Ensure the given input register is well-formed.
    pub fn check_input(
        &mut self,
        stack: &Stack<N>,
        register: &Register<N>,
        finalize_type: &FinalizeType<N>,
    ) -> Result<()> {
        // Ensure the register type is defined in the program.
        match finalize_type {
            FinalizeType::Plaintext(plaintext_type) => RegisterTypes::check_plaintext_type(stack, plaintext_type)?,
            FinalizeType::Future(locator) => {
                ensure!(
                    stack.program().contains_import(locator.program_id()),
                    "Program '{locator}' is not imported by '{}'.",
                    stack.program().id()
                )
            }
            FinalizeType::DynamicFuture => {} // Do nothing.
        };

        // Insert the input register.
        self.add_input(register.clone(), finalize_type.clone())?;

        // Ensure the register type and the input type are equivalent.
        if !finalize_types_equivalent(stack, finalize_type, stack, &self.get_type(stack, register)?)? {
            bail!("Input '{register}' does not match the expected input register type.")
        }

        Ok(())
    }

    /// Ensures the given command is well-formed.
    #[inline]
    pub fn check_command(
        &mut self,
        stack: &Stack<N>,
        positions: &HashMap<Identifier<N>, usize>,
        command: &Command<N>,
    ) -> Result<()> {

synthesizer/src/vm/tests/test_v19/external_struct_stacks.rs:20

• Spelling in the test header comment uses "finalise" / "FinaliseType" but the code and types are spelled "finalize" / FinalizeType. Keeping terminology consistent makes these tests easier to search and cross-reference with the implementation.

// Checks that various instances of casts to external structs or from using external-structs members
// function as expected. This is tested in both the function (i.e. private, RegisterType) setting as
// well as the public (i.e. finalise, FinaliseType) one.

synthesizer/src/vm/verify.rs:250

• The legacy-consensus comment uses "finalise-type" (British spelling) while the rest of the codebase uses "finalize". This makes the gating documentation harder to grep and can be confusing alongside the FinalizeTypes type name.

This issue also appears on line 395 of the same file.

                // If the `CONSENSUS_VERSION` is less than `V19`, ensure that
                //   - the program does not break the pre-V19 version of `matches_struct` in casts to external structs within finalise-type scopes.

.circleci/config.yml:1327

• Adding a feature-branch name to the merge-workflow condition can unintentionally trigger very heavy CI jobs (ledger partitions, prerelease suites, etc.) on non-merge branches, increasing CI cost and queue time. If this was only for temporary debugging, it should be removed before merging.

    when: pipeline.git.branch == "staging"
      or pipeline.git.branch == "canary"
      or pipeline.git.branch == "testnet"
      or pipeline.git.branch == "mainnet"
      or pipeline.git.branch == "fix/external_struct_stacks"