[Bug] storage vector push can evaluate values.len() after incrementing length

[Kuhai9801]

🐛 Bug Report

Vector::push can evaluate a pushed values.len() expression after incrementing the storage vector length.

In the reproducer below, values.push(values.len()) stores the post-push length instead of the length at the source evaluation point. Starting from an empty vector, it stores 1u32 at index 0 instead of 0u32.

Affected upstream commit: 4f2aa458190b53b055e606ba1b432ed2dd232ddc

Fork CI repro:
https://github.com/Kuhai9801/leo/actions/runs/27871600925

The storage-lowering comment for Vector::push(v, 42u32) describes this order:

let $len_var = Mapping::get_or_use(len_map, false, 0u32);
Mapping::set(vec_map, $len_var, 42u32);
Mapping::set(len_map, false, $len_var + 1u32);

But when the pushed value is itself values.len(), the generated finalizer increments the length first, then re-reads the length for the stored value.

Steps to Reproduce

Code snippet to reproduce

program push_len_semantics.aleo {
    storage values: [u32];

    fn push_literal(v: u32) -> Final {
        return final {
            values.push(v);
        };
    }

    fn push_len() -> Final {
        return final {
            values.push(values.len());
        };
    }

    @noupgrade
    constructor() {}
}

Test:

import push_len_semantics.aleo;

program test_push_len_semantics.aleo {
    @test
    fn empty_pre_len() -> Final {
        let f: Final = push_len_semantics.aleo::push_len();
        return final {
            f.run();
            assert(push_len_semantics.aleo::values.len() == 1u32);
            assert(push_len_semantics.aleo::values.get(0u32).unwrap() == 0u32);
        };
    }

    @test
    fn nonempty_pre_len() -> Final {
        let f1: Final = push_len_semantics.aleo::push_literal(7u32);
        let f2: Final = push_len_semantics.aleo::push_len();
        return final {
            f1.run();
            f2.run();
            assert(push_len_semantics.aleo::values.len() == 2u32);
            assert(push_len_semantics.aleo::values.get(1u32).unwrap() == 1u32);
        };
    }

    @noupgrade
    constructor() {}
}

Run:

leo test

Stack trace & error message

0 / 2 tests passed.
FAILED: test_push_len_semantics.aleo/empty_pre_len | rejected
FAILED: test_push_len_semantics.aleo/nonempty_pre_len | rejected
Error [ECLI0377046]: 2 out of 2 tests failed

Generated Aleo for push_len:

finalize push_len:
    get.or_use values__len__[false] 0u32 into r0;
    add r0 1u32 into r1;
    set r1 into values__len__[false];
    get.or_use values__len__[false] 0u32 into r2;
    set r2 into values__[r0];

The second get.or_use reads the length after set r1 into values__len__[false], so the stored value is the post-increment length.

Expected Behavior

values.push(values.len()) should store the length observed before the push mutates the vector length.

Starting from an empty vector, the stored value at index 0 should be 0u32. Starting from a vector with one element, the stored value at index 1 should be 1u32.

Your Environment

• Leo Version: leo 4.3.0, built from fork branch with no compiler source changes
• Affected commit: 4f2aa458190b53b055e606ba1b432ed2dd232ddc
• Rust Version: stable
• OS: GitHub Actions ubuntu-latest