[prover] Opaque callee with an undeclared closure parameter is assumed pure, blocking generic container APIs whose callbacks touch memory

Summary

When a function is pragma opaque and takes a function-typed parameter with no
modifies_of/reads_of declaration, the prover treats that parameter as pure and rejects
any caller whose closure touches global memory. For a generic container operation this default
is unsatisfiable: the container cannot name the resources its callers' callbacks touch.

The rejection happens during bytecode transformation, so it does not fail one function — the
caller's entire module produces zero verification conditions and nothing in it can be verified.

Repro

30 lines, depends only on the framework.

module ex::m {
    struct Counter has key { n: u64 }
    struct Box has key { v: u64 }

    /// A generic container operation that applies a caller-supplied callback
    /// to an element. Its body is not verified, so it is opaque.
    public fun apply(b: &mut Box, f: |&mut u64|) {
        f(&mut b.v)
    }
    spec apply {
        pragma opaque;
        pragma verify = false;
        // No `modifies_of<f>`. `apply` is generic over its callers, so it
        // cannot name the resources any particular callback touches.
    }

    /// Bookkeeping the callback performs, fully and correctly specified.
    fun bump(addr: address) acquires Counter {
        Counter[addr].n = Counter[addr].n + 1;
    }
    spec bump {
        pragma opaque;
        aborts_if !exists<Counter>(addr);
        aborts_if global<Counter>(addr).n + 1 > MAX_U64;
        modifies global<Counter>(addr);
        ensures global<Counter>(addr).n == old(global<Counter>(addr).n) + 1;
    }

    /// The caller passes a literal lambda that touches a resource.
    public fun caller(b: &mut Box, addr: address) acquires Counter {
        apply(b, |v| { *v = *v + 1; bump(addr); })
    }
}

Result:

error: function argument may modify resource `m::Counter`,
       which is not declared in `modifies_of` for `f`
   ┌─ sources/m.move:31:9
   │
31 │         apply(b, |v| { *v = *v + 1; bump(addr); })
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

{ "Error": "Move Prover failed: exiting with bytecode transformation errors" }

Deleting the single line pragma opaque; from spec apply, changing nothing else:

[INFO] 3 verification roots
[INFO]  0.489s ok m::bump [verification]
[INFO]  0.491s ok m::caller [verification]
[INFO]  0.463s ok m::__lambda__1__caller [verification]
{ "Result": "Success" }

bump is fully specified and correct. The callback is doing nothing questionable. It is
rejected solely because apply did not declare that a callback may touch memory.

Where this comes from

third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs:

// Skip validation only for transparent callees with no declarations.
// For opaque callees, missing declarations means "pure" — validate
// that closures don't access memory.
if access.is_empty() && !callee_env.is_opaque() {
    return true;
}

Why the existing options do not cover this

Declaring the frame on the callee is the documented pattern, and it works — see
move-prover/tests/sources/functional/closures/lambda_spec_global_memory.move, which is this
exact shape and verifies clean. But it requires naming concrete resources:

modifies_of<f>(v: &mut u64) Counter[@0x42];

A generic container cannot do that. It has no knowledge of Counter. Note there are currently
zero uses of modifies_of/reads_of anywhere in aptos-move/framework/ — every use in
the tree is in prover tests, so the feature has not yet been exercised by a generic container
API.

The wildcard modifies_of<f> *; makes the error go away, but it short-circuits the
footprint check entirely (if access.frame_spec.modifies_all { continue; }), so nothing
validates what the callback touches. As the comment in lambda_spec_global_memory.move
explains, the declared frame is also what saves the pre-state the two-state evaluators read and
havocs memory across the opaque call — so a wildcard leaves that machinery without concrete
memory to work from. It does not look safe to recommend as the general answer for container
APIs.

Dropping opaque is not available either when the callee is an intrinsic type's operation:
it exposes an implementation that is deliberately modelled rather than translated.

Suggested direction

For an opaque callee whose function-typed parameter carries no frame declaration, infer the
frame from the actual closure at each call site rather than assuming purity. The checker
already computes that footprint exactly — it computes it in order to produce the rejection.

For a function-typed parameter the effect is genuinely call-site dependent, so a fixed
declaration on a generic container can never be correct for all callers. Inferring it also
yields a tighter frame than any declaration a container author could write.

If changing the default is undesirable, an explicit opt-in that means "this parameter's frame
is whatever the caller passes" would also unblock the case, and would be safer than the
wildcard.

Some implementation notes from tracing this through, in case they save someone time. Two
things turned out to be non-obvious: which check actually fires, and that the frame has a
soundness role as well as a checking role.

The rejection comes from the bytecode pipeline, not the compiler

There are two independent checks, and they derive the closure's footprint from different
sources.

move-compiler-v2/src/env_pipeline/spec_rewriter.rs,
validate_closure_access_of_compliance, computes the footprint via compute_arg_memory.
For a lifted lambda that takes the Operation::Closure branch and reads the lifted
function's spec memory:

ExpData::Call(id, Operation::Closure(mid, fid, _), _) => {
    let target_env = env.get_function(mid.qualified(*fid));
    (target_env.get_spec_used_memory_instantiated(&inst), ...)
}

A lifted lambda has no spec conditions, so this is empty and the check is inert. I
instrumented it to be sure: on the repro it reports arg_used=0 arg_old=0 and emits
nothing.

The error actually comes from move-prover/bytecode-pipeline/src/spec_instrumentation.rs,
check_fun_arg_frames, which derives the footprint from usage analysis
(closure_footprints) and therefore sees the transitive memory. The relevant default is in
DeclaredFrame::of_fun_param:

let Some(access) = param_access.iter().find(|a| a.fun_param == param) else {
    return Self::default();     // no declaration => empty frame => "pure"
};

The frame is also load-bearing for soundness

This is the part that makes a naive fix wrong. The declaration feeds two places:

check_fun_arg_frames — the validation above.
move-model/bytecode/src/usage_analysis.rs — for a function whose body contains
Invoke, the declared frame's old_memory is added through add_direct_invoke_frame.
That is what puts the closure's writes into the callee's modified set, which is what
makes the caller havoc them across the opaque call.

So simply not rejecting when no declaration exists would be unsound: callers would continue
to assume the closure touched nothing. Any fix has to supply (2), not just relax (1). The
same consideration explains why modifies_of<f> * is not a good general answer for a
container API — it short-circuits the check without naming memory for the havoc.

Where it gets awkward

The natural inferred frame for an opaque callee's undeclared function-typed parameter is the
union, over all call sites, of the footprints of the closures actually passed. That
information exists — closure_footprints already computes it — but it is derived from
usage analysis, while the place that needs it (add_direct_invoke_frame) runs inside
usage analysis. Feeding it back requires either a global pre-scan collecting, per (callee,
parameter), the closure targets passed at call sites, so their memory is available before
the analysis needs it, or a second pass over the affected callees.

I tried the inference in the compiler-v2 rewriter first, which does not work: at that point
the lifted lambda's spec memory is empty, so there is nothing to infer from. The usable
footprint only exists after lambda lifting and usage analysis.

Minimal repro, unchanged from the issue body

Still reproduces on main. Adding it as
move-prover/tests/sources/functional/closures/infer_undeclared_frame.move gives a failing
test that should pass once this is addressed.

I tried the obvious fix and it does not work. Writing up what it rules out, since the dead
end is informative and the surviving design is narrower than I expected.

What I tried

Rather than infer the frame, let the callback declare its own and have the call site use
that. This looked attractive because the information is local, author-written, and
checkable, and because a sibling diagnostic already advises "give the lambda an explicit
specification". Lambdas do accept modifies in an inline spec block, and that declaration
is verified against the body — declaring the wrong resource produces:

error: caller `__lambda__1__caller` specifies modify targets for `Counter`
       but callee `bump` does not

So the ingredient exists. The change was small: in check_fun_arg_frames, when the callee
declares nothing for a function-typed parameter, accept writes covered by the closure
target's own modifies.

The new repro passes with it, and a negative test confirms the caller still cannot claim
the resource is unchanged across the opaque call.

Why it is wrong anyway

regression/fun_arg_frame_check.move catches two separate defects.

1. The absence of a declaration can be load-bearing.

fun apply_pure(fv: |address| has drop, a: address) { fv(a) }
spec apply_pure {
    pragma opaque;
    requires exists<R>(a);
    ensures R[a].value == old(R[a].value);   // claims R unchanged
}

apply_pure declares no modifies_of, but its own postcondition asserts R is unchanged,
and it is verified — the proof depends on fv being pure. Letting a callback that declares
modifies R[a] through makes that postcondition false. So "no declaration" does not mean
"the callee is agnostic about this memory"; sometimes it is exactly what makes the callee's
own proof go through.

2. Author-declared and inferred modifies are indistinguishable.

apply_pure(|x| { R[x].value = R[x].value + 1; }, a)

This lambda has no spec block at all, yet get_modify_targets() on the lifted function
reports R, inferred from the body. A fallback keyed on the closure's declared modifies
therefore accepts every memory-touching closure, which is the wildcard by another route.

What survives

The callee has to opt in — something like modifies_of<f> from_closure;, meaning "this
parameter's frame is whatever the caller's callback declares". That:

leaves apply_pure rejecting, because it does not opt in, so defect 1 cannot arise;
makes defect 2 moot, since an opted-in parameter is explicitly delegating and does not
need to distinguish declared from inferred;
keeps the property that a generic container never has to name a caller's resources.

It is a small language addition rather than a pure defaulting change, which is more than I
suggested in the earlier comment, but the defaulting change is not available.

One thing I did not fully isolate

The negative test showed the caller cannot claim the resource unchanged across the opaque
call, which suggests no change to usage_analysis is needed to keep the havoc. But that
caller also declared modifies on the resource itself, so the havoc may have come from its
own declaration rather than from the callback's. Worth isolating before relying on it.

Tests

Two files, usable as-is:

functional/closures/infer_undeclared_frame.move — the minimal repro. Currently fails;
it is what should go green.
functional/closures/lambda_declared_frame_havoc.move — the soundness test. A caller
claiming the resource is unchanged across the call must still fail. Any fix that makes
the first pass while making this one pass too has silenced the check without supplying
the effect.

[prover] Let a generic opaque callee leave its closure's frame to the…

Navigation Menu

Repository navigation

[prover] Opaque callee with an undeclared closure parameter is assumed pure, blocking generic container APIs whose callbacks touch memory #20689

Summary

Repro

Where this comes from

Why the existing options do not cover this

Suggested direction

The rejection comes from the bytecode pipeline, not the compiler

The frame is also load-bearing for soundness

Where it gets awkward

Minimal repro, unchanged from the issue body

What I tried

Why it is wrong anyway

What survives

One thing I did not fully isolate

Tests

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[prover] Opaque callee with an undeclared closure parameter is assumed pure, blocking generic container APIs whose callbacks touch memory #20689

Description

Summary

Repro

Where this comes from

Why the existing options do not cover this

Suggested direction

Activity

rahxephon89 commented on Oct 7, 2026

The rejection comes from the bytecode pipeline, not the compiler

The frame is also load-bearing for soundness

Where it gets awkward

Minimal repro, unchanged from the issue body

rahxephon89 commented on Oct 7, 2026

What I tried

Why it is wrong anyway

What survives

One thing I did not fully isolate

Tests

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions