diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs index 3d97bc924fa..eb0d3a4b076 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs @@ -46,6 +46,17 @@ void ProcessRhss(List lhsBuilder, List(); for (int i = 0; i < lhss.Count; i++) { var lhs = lhss[i]; @@ -98,6 +109,17 @@ void ProcessRhss(List lhsBuilder, List>(), i => i != null)); + // For havoc assignments to identifier variables with definite assignment tracking, + // mark the definite assignment tracker BEFORE processing the RHS so that the + // where clause is properly assumed during the havoc + for (int i = 0; i < lhss.Count; i++) { + if (rhss[i] is HavocRhs && lhss[i] is IdentifierExpr ie) { + if (ie.Type.HavocCountsAsDefiniteAssignment(ie.Var.IsGhost)) { + MarkDefiniteAssignmentTracker(ie, builder); + } + } + } + var finalRhss = new List(); for (int i = 0; i < lhss.Count; i++) { var lhs = lhss[i]; @@ -246,9 +268,18 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi bldr.Add(cmd); } - if (!origRhsIsHavoc || ie.Type.HavocCountsAsDefiniteAssignment(ie.Var.IsGhost)) { + // Mark definite assignment tracker: + // - For non-havoc assignments: always mark after assignment + // - For havoc assignments that don't count as definite assignment: mark after havoc + // - For havoc assignments that count as definite assignment: already marked before havoc, don't mark again + if (!origRhsIsHavoc) { + // Non-havoc assignment: always mark + MarkDefiniteAssignmentTracker(ie, bldr); + } else if (!ie.Type.HavocCountsAsDefiniteAssignment(ie.Var.IsGhost)) { + // Havoc assignment that doesn't count as definite assignment: mark after havoc MarkDefiniteAssignmentTracker(ie, bldr); } + // For havoc assignments that count as definite assignment: don't mark here (already marked before havoc) }); } else if (lhs is MemberSelectExpr) { diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index 623f66201cf..7bc7bb71f26 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs @@ -553,6 +553,17 @@ void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, Varia } } if (varDeclStmt.Assign != null) { + // For variable declarations with havoc assignments, mark the definite assignment tracker + // BEFORE processing the assignment so that the where clause is properly assumed during the havoc + if (varDeclStmt.Assign is AssignStatement assignStmt) { + for (int j = 0; j < Math.Min(assignStmt.Lhss.Count, assignStmt.Rhss.Count); j++) { + if (assignStmt.Rhss[j] is HavocRhs && assignStmt.Lhss[j].Resolved is IdentifierExpr ie) { + if (ie.Type.HavocCountsAsDefiniteAssignment(ie.Var.IsGhost)) { + MarkDefiniteAssignmentTracker(ie, builder); + } + } + } + } TrStmt(varDeclStmt.Assign, builder, locals, etran); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/set-extensionality-havoc.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/set-extensionality-havoc.dfy new file mode 100644 index 00000000000..03694c32c15 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/set-extensionality-havoc.dfy @@ -0,0 +1,35 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=0 "%s" + +method SetInclusionHavoc() { + ghost var A0: set<(object?, int)> := *; + ghost var A1: set<(object?, int)> := *; + assume {:axiom} allocated(A0); + assume {:axiom} allocated(A1); + assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1; + assert A0 <= A1; // Should pass after fix +} + +method SetEqualityHavoc() { + ghost var A0: set<(object?, int)> := *; + ghost var A1: set<(object?, int)> := *; + assume {:axiom} allocated(A0); + assume {:axiom} allocated(A1); + assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1; + assert A0 == A1; // Should pass after fix +} + +method Set() returns (s: set<(object?, int)>) + +method SetInclusionMethod() { + ghost var A0: set<(object?, int)> := Set(); + ghost var A1: set<(object?, int)> := Set(); + assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1; + assert A0 <= A1; // This should already pass +} + +method SetEqualityMethod() { + ghost var A0: set<(object?, int)> := Set(); + ghost var A1: set<(object?, int)> := Set(); + assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1; + assert A0 == A1; // This should already pass +} diff --git a/debug_test.dfy b/debug_test.dfy new file mode 100644 index 00000000000..fefd4d8d4c8 --- /dev/null +++ b/debug_test.dfy @@ -0,0 +1,9 @@ +method Test() { + ghost var x: int := *; + assert x == x; // This should work +} + +method Test2() { + ghost var s: set := *; + assert s == s; // This should work +} diff --git a/debug_test2.dfy b/debug_test2.dfy new file mode 100644 index 00000000000..8178a934628 --- /dev/null +++ b/debug_test2.dfy @@ -0,0 +1,11 @@ +method Test() { + ghost var x: int; + x := 5; + assert x == x; // This should work +} + +method Test2() { + ghost var s: set; + s := {}; + assert s == s; // This should work +} diff --git a/docs/dev/news/6304.md b/docs/dev/news/6304.md new file mode 100644 index 00000000000..0df7f30b9bf --- /dev/null +++ b/docs/dev/news/6304.md @@ -0,0 +1,68 @@ +# Fix for Issue #6304: Set extensionality cannot be proved because type of local variables is not assumed + +## Issue Summary + +Issue #6304 reported that set extensionality proofs fail when using havoc assignments (`var x := *`) for variables with complex types like `set<(object?, int)>`. The problem occurs because the type information (where clause) is not properly assumed during the havoc operation. + +## Root Cause Analysis + +The issue is in the Dafny-to-Boogie translation. When translating variable declarations with havoc assignments, the generated Boogie code has the wrong order of operations: + +**Current (incorrect) order:** +```boogie +havoc A0#0; +defass#A0#0 := true; +``` + +**Required (correct) order:** +```boogie +defass#A0#0 := true; +havoc A0#0; +``` + +The problem is that variables with definite assignment tracking have where clauses of the form: +```boogie +var A0#0: Set + where defass#A0#0 + ==> $Is(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt))) + && $IsAlloc(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt)), $Heap); +``` + +When `havoc` is executed before `defass#A0#0 := true`, the where clause doesn't constrain the havoc because `defass#A0#0` is false. This means the type information is not assumed, leading to failed set extensionality proofs. + +## Investigation Attempts + +Several approaches were attempted to fix this issue: + +1. **Modifying ProcessRhss**: Attempted to mark the definite assignment tracker before processing havoc RHS, but this didn't work for single assignments. + +2. **Modifying TrAssignmentRhs**: Attempted to mark the definite assignment tracker within the havoc handling, but the lhsVar parameter was often null. + +3. **Modifying TrVarDeclStmt**: Attempted to mark the definite assignment tracker before processing the assignment in variable declarations. + +## Current Status + +The fix attempts were not successful due to the complexity of the interaction between definite assignment tracking and the Boogie translation. The issue requires a deeper understanding of the translation pipeline and careful coordination between: + +- Variable declaration processing (`TrVarDeclStmt`) +- Assignment processing (`ProcessRhss`, `ProcessUpdateAssignRhss`) +- Definite assignment tracking (`MarkDefiniteAssignmentTracker`) +- LHS builder delegates + +## Integration Test + +An integration test was added at `Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/set-extensionality-havoc.dfy` that reproduces the issue and can be used to verify when the fix is implemented. + +## Next Steps + +To properly fix this issue, the following approach is recommended: + +1. Ensure that for havoc assignments to variables with definite assignment tracking, the definite assignment tracker is set to `true` before the havoc operation. + +2. Modify the LHS builder to avoid double-marking the definite assignment tracker for such cases. + +3. Handle both single assignments and multi-assignments consistently. + +4. Ensure the fix works for all types that have `HavocCountsAsDefiniteAssignment(isGhost) == true`. + +The issue affects set extensionality proofs and potentially other type-dependent reasoning in Dafny verification. diff --git a/set_test.dfy b/set_test.dfy new file mode 100644 index 00000000000..15eeb88e774 --- /dev/null +++ b/set_test.dfy @@ -0,0 +1,6 @@ +method Test() { + ghost var A0: set := *; + ghost var A1: set := *; + assume {:axiom} forall r: int :: r in A0 <==> r in A1; + assert A0 == A1; // This should pass but might fail +} diff --git a/set_test_explicit.dfy b/set_test_explicit.dfy new file mode 100644 index 00000000000..5f1b2429d05 --- /dev/null +++ b/set_test_explicit.dfy @@ -0,0 +1,8 @@ +method Test() { + ghost var A0: set; + ghost var A1: set; + A0 := {}; + A1 := {}; + assume {:axiom} forall r: int :: r in A0 <==> r in A1; + assert A0 == A1; // This should pass +} diff --git a/set_test_no_havoc.dfy b/set_test_no_havoc.dfy new file mode 100644 index 00000000000..cc7da459c09 --- /dev/null +++ b/set_test_no_havoc.dfy @@ -0,0 +1,8 @@ +method Test() { + ghost var A0: set; + ghost var A1: set; + A0 := *; + A1 := *; + assume {:axiom} forall r: int :: r in A0 <==> r in A1; + assert A0 == A1; // This should pass +} diff --git a/set_test_no_use.dfy b/set_test_no_use.dfy new file mode 100644 index 00000000000..1eac96cb743 --- /dev/null +++ b/set_test_no_use.dfy @@ -0,0 +1,5 @@ +method Test() { + ghost var A0: set := *; + ghost var A1: set := *; + // Don't use A0 and A1 after this point +} diff --git a/simple_test.dfy b/simple_test.dfy new file mode 100644 index 00000000000..ceb3356affa --- /dev/null +++ b/simple_test.dfy @@ -0,0 +1,3 @@ +method Test() { + ghost var x: int := *; +} diff --git a/test_separate_assignment.dfy b/test_separate_assignment.dfy new file mode 100644 index 00000000000..1c08ed5a63c --- /dev/null +++ b/test_separate_assignment.dfy @@ -0,0 +1,8 @@ +method Test() { + ghost var A0: set; + ghost var A1: set; + A0 := *; + A1 := *; + assume {:axiom} forall r: int :: r in A0 <==> r in A1; + assert A0 == A1; // This should pass if the fix works +} diff --git a/test_set_extensionality_bug.dfy b/test_set_extensionality_bug.dfy new file mode 100644 index 00000000000..e79324c3415 --- /dev/null +++ b/test_set_extensionality_bug.dfy @@ -0,0 +1,30 @@ +method SetInclusionHavoc() { + ghost var A0: set<(object?, int)> := *; + ghost var A1: set<(object?, int)> := *; + assume {:axiom} allocated(A0); + assume {:axiom} allocated(A1); + assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1; + assert A0 <= A1; // Failing +} +method SetEqualityHavoc() { + ghost var A0: set<(object?, int)> := *; + ghost var A1: set<(object?, int)> := *; + assume {:axiom} allocated(A0); + assume {:axiom} allocated(A1); + assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1; + assert A0 == A1; // Failing +} + +method Set() returns (s: set<(object?, int)>) +method SetInclusionMethod() { + ghost var A0: set<(object?, int)> := Set(); + ghost var A1: set<(object?, int)> := Set(); + assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1; + assert A0 <= A1; +} +method SetEqualityMethod() { + ghost var A0: set<(object?, int)> := Set(); + ghost var A1: set<(object?, int)> := Set(); + assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1; + assert A0 == A1; +}