Context
Behavioral-predicate Skolems and evaluators introduced for inline HOF verification are emitted with non-bit-vector Boogie types. Functional specifications involving values marked with pragma bv therefore cannot be consumed without type mismatches.
The concrete framework case is std::features::set: feature bytes and its functional specification use bit-vector operations. Calling it from a for_each_ref lambda leaves the captured feature vector mutation underivable, so feature enable/disable iteration has to be written as explicit loops.
This boundary is documented in third_party/move/move-prover/doc/dev/inline_fun_specs.md.
Missing feature
Make behavioral predicate functions, Skolems, evaluators, and number-operation analysis bit-vector aware, including Operation::Behavior lowering and functional &mut post-value routing.
Expected result
Lambdas mutating bit-vector-modeled integers through function calls should verify through inline HOF invariants without weakening or explicit-loop workarounds.
Tracked from #20360.
Context
Behavioral-predicate Skolems and evaluators introduced for inline HOF verification are emitted with non-bit-vector Boogie types. Functional specifications involving values marked with
pragma bvtherefore cannot be consumed without type mismatches.The concrete framework case is
std::features::set: feature bytes and its functional specification use bit-vector operations. Calling it from afor_each_reflambda leaves the captured feature vector mutation underivable, so feature enable/disable iteration has to be written as explicit loops.This boundary is documented in
third_party/move/move-prover/doc/dev/inline_fun_specs.md.Missing feature
Make behavioral predicate functions, Skolems, evaluators, and number-operation analysis bit-vector aware, including
Operation::Behaviorlowering and functional&mutpost-value routing.Expected result
Lambdas mutating bit-vector-modeled integers through function calls should verify through inline HOF invariants without weakening or explicit-loop workarounds.
Tracked from #20360.