From a5b497227c2e186d4b7bf164167ace58c50b445e Mon Sep 17 00:00:00 2001 From: Ernie Cohen Date: Sat, 26 Sep 2026 14:45:51 -0400 Subject: [PATCH] fix: No unguarded reverse casts in the arguments type encoding Fixes #1168. 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 says that U has at most two elements, while the left inverse for int makes U infinite, so the axioms had no model (#1168). The predicates encoding guards the same axiom with type(x) == B; the arguments encoding has no type function to guard it with. The change is to TypeErasureArguments.cs. It changes /typeEncoding:a only, and it adds no axiom: 1. No reverse cast. TypeAxiomBuilderArguments.GenReverseCastAxiom returns true. The left inverses stay. 2. No retyping. TypeEraserArguments.Visit(VCExprQuantifier) no longer redoes a quantifier whose int (bool, ...) variable occurs in its triggers only under a cast, with that variable retyped to U (RedoQuantifier). 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 dropping the reverse cast alone is still unsound: from forall b: bool :: {Box(b)} Box(b) == Box(IdB(b)), the redone quantifier says that every value boxed at bool is a bool. The predicates encoding keeps RedoQuantifier, with a type premise on each retyped variable. 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; Test/test21/Triggers1.bpl then loses assert f(m[x]) from axiom (forall x: int :: f(x)). Why the result is sound. Boogie's own axioms under the arguments encoding are now 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, 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 in Boogie's semantics. Not changed: 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, such as forall x, y: Unit :: x == y, still bounds U. That is the erasure of the program's axiom, not an axiom of Boogie's, and the predicates encoding guards it. The predicates and monomorphic encodings are unchanged. Tests: Test/test21/issue-1168.bpl is the issue's program, and issue-1168-redo.bpl shows that dropping the reverse casts alone is not enough. Each ends in "assert false" and runs the three encodings with model-based quantifier instantiation, bounded at 10 iterations. Both fail before this change, where /typeEncoding:a proves "assert false", and pass after it. Co-Authored-By: Claude Opus 5.5 --- .../TypeErasure/TypeErasureArguments.cs | 69 ++++++++++++------- Test/test21/issue-1168-redo.bpl | 36 ++++++++++ Test/test21/issue-1168-redo.bpl.expect | 5 ++ Test/test21/issue-1168.bpl | 29 ++++++++ Test/test21/issue-1168.bpl.expect | 5 ++ 5 files changed, 119 insertions(+), 25 deletions(-) create mode 100644 Test/test21/issue-1168-redo.bpl create mode 100644 Test/test21/issue-1168-redo.bpl.expect create mode 100644 Test/test21/issue-1168.bpl create mode 100644 Test/test21/issue-1168.bpl.expect diff --git a/Source/VCExpr/TypeErasure/TypeErasureArguments.cs b/Source/VCExpr/TypeErasure/TypeErasureArguments.cs index 93a82c978..5da852f09 100644 --- a/Source/VCExpr/TypeErasure/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasure/TypeErasureArguments.cs @@ -47,16 +47,28 @@ public override Object Clone() /////////////////////////////////////////////////////////////////////////////// - // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))} Int2U(U2Int(x))==x" - // (this makes use of the assumption that only well-typed terms are generated - // by the SMT-solver, i.e., that U2Int is only applied to terms that actually - // are of type int) + // This encoding emits NO reverse cast axiom. The axiom it used to emit, + // forall x:U. {U2Int(x)} Int2U(U2Int(x)) == x, + // says that every value of U is an int; its bool instance says that U has at + // most two elements, while the left inverse axiom U2Int(Int2U(n)) == n + // (GenLeftInverseAxiom, emitted for every cast) makes U infinite, so the two + // have no model together (boogie-org/boogie#1168). It relied on "only + // well-typed terms are generated by the SMT-solver", which a solver does not + // promise. A guard in terms of the explicit type arguments of polymorphic + // functions (f(intType, ...) is always an int) is not true either: an axiom + // forall x: T :: Id(x) == x + // is erased to forall t: T, x: U :: Id(t, x) == x, which makes Id(intType, x) + // equal to x for EVERY x in U. + // What relied on the reverse cast: quantifiers whose int (bool, ...) + // variables were retyped to U for the sake of their triggers, which this + // encoding no longer does (TypeEraserArguments.Visit(VCExprQuantifier)); and + // an int reaching a U position as a U term in one formula and as a cast in + // another, which the normal form of OpTypeEraserArguments.AssembleOpExpression + // rules out. protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) { Contract.Ensures(Contract.Result() != null); - VCExpr - eq = GenReverseCastEq(castToU, castFromU, out var var, out var triggers); - return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, 1, eq); + return VCExpressionGenerator.True; } protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) @@ -510,23 +522,17 @@ public override VCExpr Visit(VCExprQuantifier node, VariableBindings oldBindings // type variables are replaced with ordinary quantified variables GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings); - VCExpr - newNode = HandleQuantifier(node, newBoundVars, bindings); - Contract.Assert(newNode != null); - - if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node)) - { - return newNode; - } - if (!RedoQuantifier(node, (VCExprQuantifier) newNode, node.BoundVars, oldBindings, - out var bindings2, out newBoundVars)) - { - return newNode; - } - - GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings2); - return HandleQuantifier(node, newBoundVars, bindings2); + // The quantifier is NOT redone with its int (bool, ...) variables retyped to + // U when they occur in the triggers only under a cast (RedoQuantifier, which + // the predicates encoding still uses, with a type premise on each retyped + // variable). Here the redone body spoke of every value x of U where the + // original speaks of the ints, and the two agreed only under the reverse + // cast axiom Int2U(U2Int(x)) == x, which this encoding no longer emits (see + // GenReverseCastAxiom). A trigger Int2U(n) still matches every U term the + // solver knows to be a cast, and under the normal form of + // AssembleOpExpression a value of type int reaches a U position as a cast. + return HandleQuantifier(node, newBoundVars, bindings); } private void GenBoundVarsForTypeParams(List typeParams, @@ -623,8 +629,21 @@ private VCExpr AssembleOpExpression(OpTypesPair opTypes, IEnumerable old foreach (VCExpr arg in oldArgs) { Contract.Assert(arg != null); - newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), - Cce.NonNull(newFun.InParams[i]).TypedIdent.Type)); + VCExpr newArg = Eraser.Mutate(arg, bindings); + Type paramType = Cce.NonNull(newFun.InParams[i]).TypedIdent.Type; + // A value whose type is int (bool, ...) is passed to a U parameter as the + // cast of an int, Int2U(U2Int(t)), also when its translation t is already + // a U term -- the result of a polymorphic function or of a map select at + // int. In Boogie's semantics this is the identity. Without the reverse + // cast axiom (see GenReverseCastAxiom) t and Int2U(U2Int(t)) are no + // longer known to be equal, and without this normal form the same int + // would reach a U position in two forms, as t in one formula and as + // Int2U(U2Int(t)) in another. + if (paramType.Equals(AxBuilder.U) && newArg.Type.Equals(AxBuilder.U) && AxBuilder.UnchangedType(arg.Type)) + { + newArg = AxBuilder.Cast(newArg, arg.Type); + } + newArgs.Add(AxBuilder.Cast(newArg, paramType)); i = i + 1; } diff --git a/Test/test21/issue-1168-redo.bpl b/Test/test21/issue-1168-redo.bpl new file mode 100644 index 000000000..5dd21d2d1 --- /dev/null +++ b/Test/test21/issue-1168-redo.bpl @@ -0,0 +1,36 @@ +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:a "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:p "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:m "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// Issue #1168, continued (see issue-1168.bpl). The last two axioms below are +// quantifiers whose int (bool) variable occurs in the trigger only under a cast, +// Box(intType, int_2_U(n)). The arguments encoding used to redo such a +// quantifier with the variable retyped to U, so that the trigger matches boxed +// values that are not casts; the redone body is then stated for every value of U, +// not only the ints (bools), and only the reverse casts made the two readings +// agree. So dropping the reverse casts is not enough: with the retyping kept, +// the bool axiom says that every value boxed at bool is a bool, and with +// Unbox(Box(x)) == x that bounds U to two elements again. Every axiom here is +// true in Boogie's semantics, and no encoding may prove "assert false". + +type Box; +function Box(x: T): Box; +function Unbox(b: Box): T; +axiom (forall x: T :: { Box(x) } Unbox(Box(x)): T == x); + +function IdI(n: int): int; +axiom (forall n: int :: { IdI(n) } IdI(n) == n); +function IdB(b: bool): bool; +axiom (forall b: bool :: { IdB(b) } IdB(b) == b); + +axiom (forall n: int :: { Box(n) } Box(n) == Box(IdI(n))); +axiom (forall b: bool :: { Box(b) } Box(b) == Box(IdB(b))); + +procedure P(n: int) +{ + assert Unbox(Box(n)): int == n; + assert false; // not provable +} diff --git a/Test/test21/issue-1168-redo.bpl.expect b/Test/test21/issue-1168-redo.bpl.expect new file mode 100644 index 000000000..cab3ca297 --- /dev/null +++ b/Test/test21/issue-1168-redo.bpl.expect @@ -0,0 +1,5 @@ +issue-1168-redo.bpl(35,3): Error: this assertion could not be proved +Execution trace: + issue-1168-redo.bpl(34,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/issue-1168.bpl b/Test/test21/issue-1168.bpl new file mode 100644 index 000000000..1f5e10da0 --- /dev/null +++ b/Test/test21/issue-1168.bpl @@ -0,0 +1,29 @@ +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:a "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:p "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %parallel-boogie /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.mbqi.max_iterations=10 /typeEncoding:m "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// Issue #1168. The arguments encoding erases every non-built-in type to one +// sort U, with casts in and out of U for each built-in type. Beside the left +// inverse U_2_int(int_2_U(n)) == n, which makes U infinite, it used to emit +// reverse casts such as +// forall x: U :: bool_2_U(U_2_bool(x)) == x +// which say that every value of U is a bool, so that U has at most two +// elements. Together they have no model, and model-based quantifier +// instantiation found that out: it proved "assert false" below under +// /typeEncoding:a. No encoding may prove it. The iteration bound keeps the +// search short: when the solver reaches it, it answers unknown, and the +// assertion is reported as not proved. + +type Box; +function Box(x: T): Box; +function Unbox(b: Box): T; +axiom (forall x: T :: { Box(x) } Unbox(Box(x)): T == x); + +procedure P(b: bool, n: int) +{ + assert Unbox(Box(b)): bool == b && Unbox(Box(n)): int == n; + assert false; // not provable +} diff --git a/Test/test21/issue-1168.bpl.expect b/Test/test21/issue-1168.bpl.expect new file mode 100644 index 000000000..b66c32cee --- /dev/null +++ b/Test/test21/issue-1168.bpl.expect @@ -0,0 +1,5 @@ +issue-1168.bpl(28,3): Error: this assertion could not be proved +Execution trace: + issue-1168.bpl(27,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error