The spec-fun memory-usage analysis (directly_used_memory, move-model/src/ast.rs) has no Operation::Behavior arm, so memory touched by behavioral predicates (result_of, write_of, ensures_of, ...) inside a spec function body is never added to the function's used_memory. For fun types whose evaluator memory union is non-empty (memory-touching closure targets), the emitted evaluator application then references Boogie global memory variables inside a function body — a Boogie name-resolution error with no earlier diagnostic (check_name_declared early-returns when no declarations are tracked).
Today every in-tree use has an empty union (pure lambdas), so the gap is latent; surfacing write_of makes it more reachable. fun_post_of has an explicit gate (memory-dependent values rejected, #20273); the other kinds do not.
Fix candidates: add a Behavior arm to the memory-usage analysis using the per-type evaluator union (coarse but sound), or require explicit reads clauses on spec funs whose bodies use BPs over memory-touching fun types.
Filed by Claude (AI agent) on behalf of @wrwg.
The spec-fun memory-usage analysis (
directly_used_memory, move-model/src/ast.rs) has noOperation::Behaviorarm, so memory touched by behavioral predicates (result_of,write_of,ensures_of, ...) inside a spec function body is never added to the function'sused_memory. For fun types whose evaluator memory union is non-empty (memory-touching closure targets), the emitted evaluator application then references Boogie global memory variables inside afunctionbody — a Boogie name-resolution error with no earlier diagnostic (check_name_declaredearly-returns when no declarations are tracked).Today every in-tree use has an empty union (pure lambdas), so the gap is latent; surfacing
write_ofmakes it more reachable.fun_post_ofhas an explicit gate (memory-dependent values rejected, #20273); the other kinds do not.Fix candidates: add a
Behaviorarm to the memory-usage analysis using the per-type evaluator union (coarse but sound), or require explicitreadsclauses on spec funs whose bodies use BPs over memory-touching fun types.Filed by Claude (AI agent) on behalf of @wrwg.