The prover models function values as a closed Boogie datatype: closure packs, one constant constructor $param'fn$p'() per fun-typed parameter of a verified function, and struct-field constructors. Verification entry pins each fun param to its own constructor (assume $t_i == $param'fn$p'();), and spec-level == on fun values translates to native datatype equality.
Datatype constructors are pairwise provably distinct, so distinctness of the abstraction leaks into specs as provable facts about values:
fun h(f: |u64|u64, g: |u64|u64) { .. } spec h { ensures f != g; } verifies ($param'h$f'() != $param'h$g'() by constructor distinctness) — yet a caller h(c, c) then assumes c != c, i.e. false, making everything downstream vacuous.- Same with
ensures f != some_named_function against a caller passing exactly that function (param vs closure constructor).
Positive equalities are fine (never provable from the abstraction alone); only disequality-exposing conclusions are unsound. This exists independently of the carried-mutation work, but chained-application specs (issue #20273) make fun-value equality a central idiom, so the hole stops being latent.
Candidate fixes (from the design review): (a) validation rejecting spec-level disequality-exposing comparisons of fun values across distinct opaque origins; (b) translating fun-value == through an uninterpreted equivalence that Boogie == implies but that is never refutable, keeping positive equalities provable while blocking negative conclusions.
Filed by Claude (AI agent) on behalf of @wrwg.
The prover models function values as a closed Boogie datatype: closure packs, one constant constructor
$param'fn$p'()per fun-typed parameter of a verified function, and struct-field constructors. Verification entry pins each fun param to its own constructor (assume $t_i == $param'fn$p'();), and spec-level==on fun values translates to native datatype equality.Datatype constructors are pairwise provably distinct, so distinctness of the abstraction leaks into specs as provable facts about values:
fun h(f: |u64|u64, g: |u64|u64) { .. } spec h { ensures f != g; }verifies ($param'h$f'() != $param'h$g'()by constructor distinctness) — yet a callerh(c, c)then assumesc != c, i.e.false, making everything downstream vacuous.ensures f != some_named_functionagainst a caller passing exactly that function (param vs closure constructor).Positive equalities are fine (never provable from the abstraction alone); only disequality-exposing conclusions are unsound. This exists independently of the carried-mutation work, but chained-application specs (issue #20273) make fun-value equality a central idiom, so the hole stops being latent.
Candidate fixes (from the design review): (a) validation rejecting spec-level disequality-exposing comparisons of fun values across distinct opaque origins; (b) translating fun-value
==through an uninterpreted equivalence that Boogie==implies but that is never refutable, keeping positive equalities provable while blocking negative conclusions.Filed by Claude (AI agent) on behalf of @wrwg.