fix: No unguarded reverse casts in the arguments type encoding

[erniecohen]

Fixes #1168.

The bug

Under /typeEncoding:a, every value of a type that is not built in is erased to one sort U, and each built-in type B gets casts B_2_U and U_2_B with the left inverse U_2_B(B_2_U(x)) == x. Beside it the encoding emitted a reverse cast

forall x: U :: {U_2_B(x)} B_2_U(U_2_B(x)) == x

which says that every value of U is a B. For bool it bounds U to two elements, while the left inverse for int makes U infinite, so Boogie's own axioms had no model. The new test Test/test21/issue-1168.bpl is the issue's program ending in assert false: with model-based quantifier instantiation, /typeEncoding:a proves it on master.

The change

One file, Source/VCExpr/TypeErasure/TypeErasureArguments.cs. It changes /typeEncoding:a only, and it adds no axiom.

1. No reverse casts. TypeAxiomBuilderArguments.GenReverseCastAxiom returns true. The left inverses stay.
2. No retyping. TypeEraserArguments.Visit(VCExprQuantifier) no longer calls RedoQuantifier, which redid a quantifier whose int (bool, ...) variable occurs in its triggers only under a cast, with that variable retyped to U. The redone body is stated for every value of U where the original speaks of the ints, and the two agree only under the reverse cast. So part 1 alone is still unsound: issue-1168-redo.bpl has forall b: bool :: {Box(b)} Box(b) == Box(IdB(b)), whose redone form says that every value boxed at bool is a bool, and with part 1 alone it still proves assert false. The predicates encoding keeps RedoQuantifier, with its type(x) == B premise.
3. A cast normal form. OpTypeEraserArguments.AssembleOpExpression passes a value whose Boogie type is built in to a U parameter as B_2_U(U_2_B(t)) also when its translation t is already a U term: the result of a polymorphic function, or a map select, at B. In Boogie's semantics this is the identity. Without it the same value reaches a U position as t in one formula and as a cast in another, and only the reverse cast joined the two: test21/Triggers1.bpl then loses assert f(m[x]) from axiom (forall x: int :: f(x)).

The predicates and monomorphic encodings are unchanged, and so is every query that does not use /typeEncoding:a.

Why the result is sound

Boogie's own axioms under the arguments encoding are then the numbering and the left inverses of the type constructors, the left inverses of the casts, and the map axioms. They hold in a model where U is a tagged union of the built-in values, the values of the other types and the map values (finite-support functions), each cast injects into U and projects out of it, and a projection of a value of another type gives a default. The reverse casts were the only axioms of Boogie's own that no such model satisfies. With part 2 every quantifier is the plain erasure of the typed one, and part 3 replaces a term with one that denotes the same value.

This was also checked by machine on the queries of four small programs (the issue's, issue-1168-redo.bpl's, and two built from the shapes of Dafny's prelude): with the model written as SMT-LIB datatypes and definitions, Z3 shows that every axiom and term the patched Boogie emits holds in it. Before the change, exactly the reverse casts and the retyped quantifiers fail that check.

What it does not fix

The arguments encoding still states a program's own axioms for every value of U. So a program axiom that bounds the size of a type still bounds U: with function F<T>(x: T): bool and axiom (forall x, y: Unit :: {F(x), F(y)} x == y), two terms F(UnitType, int_2_U(k)) refute it. That is the erasure of the program's axiom, not an axiom of Boogie's, and the predicates encoding guards it.

The two fixes sketched in the issue

• (a) The result of each polymorphic function at a built-in type is a cast of that type. This has no model once a program has an axiom that is parametric in such a function. forall<T> x: T :: Lit(x) == x is erased to forall t: T, x: U :: Lit(t, x) == x, which makes Lit(boolType, int_2_U(k)) equal to int_2_U(k), not a bool. The same holds for Unbox(Box(x)) == x. Dafny's prelude has both, and three such terms refute (a) in Dafny's own queries.
• (b) The predicates encoding's type guard, for the built-in types only. If only casts have a type, the guard holds only where the left inverse already gives the reverse cast. If a function's result gets its type unguarded, one term Lit(boolType, int_2_U(0)) refutes it. If the result's type is guarded by the arguments' types, every value of U needs a type, and that is the predicates encoding.

Two sound variants of part 2 that keep the retyping were measured as well: the redone body let-bound at U_2_B(x), or guarded by a predicate U_is_B(x) that holds of every cast. Each made one Dafny query run out of resources (at 16M) that needs under 1M before the change. Not retyping was the simplest of the three and the cheapest.

Testing

• Test/test21/issue-1168.bpl and issue-1168-redo.bpl, in the style of issue-735.bpl: each ends in assert false, and runs /typeEncoding:a, :p and :m with smt.mbqi bounded at 10 iterations. On master, /typeEncoding:a proves assert false in both, and the second also with part 1 alone (measured on v3.5.5, whose TypeErasureArguments.cs is master's). With the change, no encoding proves it. The same holds with Z3 4.11.2 and 5.1.0 on master, and with 4.11.2, 4.12.1, 4.16.0 and 5.1.0 on v3.5.5, with and without batch mode.
• Boogie's CI (test.yml and test-lean-auto.yml, unchanged) passes on this branch in the fork: Boogie CI and LeanAuto CI.
• Every other RUN line of the test suite that selects /typeEncoding:a (40 of them, most in test21) gives the same output on master with and without the change, with Z3 4.11.2.

Effect on completeness

Dafny selects /typeEncoding:a. A Dafny 4.11.0 built against this change (on v3.5.5, where TypeErasureArguments.cs is identical to master's) was compared with the same Dafny on v3.5.5. That Dafny also carries fixes for its own prelude's soundness issues (dafny-lang/dafny#6531 to #6537), in both builds.

• Dafny's test suite, 1,069 programs under dafny0 to dafny4 and git-issues, at a resource limit of 16,000,000: 10 programs change, none by a new error. In 5 a proof now finishes within the limit (6 proofs in all), and in 5 one proof no longer does.
• 60 declarations of a large Dafny development: all still verify, and the total resource count is x0.99 of the count before the change.

---

This pull request was prepared by an AI, Claude (Anthropic's model, in Claude Code), for @erniecohen, who filed #1168 and asked for the fix to be offered here. The AI wrote the change and the tests and ran the checks and measurements described above. The same change, on v3.5.5, is the branch review/3.5.5 of the fork, whose CI runs this repository's test jobs and packs it.

🤖 Generated with Claude Code