Allow let-such-that expression to be compiled, provided that they provably have a unique value

6 files changed, 81 insertions, 11 deletions

diff --git a/Test/dafny0/DeterministicPick.dfy b/Test/dafny0/DeterministicPick.dfy
new file mode 100644
index 00000000..a7ec55fa
--- /dev/null
+++ b/Test/dafny0/DeterministicPick.dfy
@@ -0,0 +1,48 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+abstract module Specification {

+  function method Pick(s: set<int>): int

+    requires s != {}

+    ensures Pick(s) in s

+}

+

+module Attempt_Arbitrary refines Specification {

+  function method Pick...

+  {

+    var x :| x in s;  // error: cannot prove this is deterministic

+    x

+  }

+}

+

+module Attempt_Smallest refines Specification {

+  function method Pick...

+  {

+    ASmallestToPick(s);

+    var x :| x in s && forall y :: y in s ==> x <= y;

+    x

+  }

+  lemma ASmallestToPick(s: set<int>)

+    requires s != {}

+    ensures exists x :: x in s && forall y :: y in s ==> x <= y

+  {

+    var z :| z in s;

+    if s != {z} {

+      var s' := s - {z};

+      ASmallestToPick(s');

+    }

+  }

+}

+

+module AnotherTest {

+  function method PickFromSingleton<U>(s: set<U>): U

+    requires exists y :: s == {y}

+  {

+    var x :| x in s; x

+  }

+  function method PickFromPair<U(==)>(a: U, b: U): U

+    requires a != b

+  {

+    var x :| x in {a,b} && x != a; x

+  }

+}

diff --git a/Test/dafny0/DeterministicPick.dfy.expect b/Test/dafny0/DeterministicPick.dfy.expect
new file mode 100644
index 00000000..f8b779ef
--- /dev/null
+++ b/Test/dafny0/DeterministicPick.dfy.expect
@@ -0,0 +1,6 @@
+DeterministicPick.dfy(13,5): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index b9f6a2c5..b8d68bd6 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -306,3 +306,20 @@ function method F_bad(d: Tuple<
   assert q < 200;  // error: assertion failure

   p.1 + if b0 then x + y0 else x + y1

 }

+

+// ----------------------------------

+

+method LetSuchThat_Deterministic() returns (x: int)

+{

+  if {

+    case true =>  

+      x := var y :| y < 0; y;  // error: not deterministic

+    case true =>  

+      x := var y :| y < 0; y*0;

+    case true =>  

+      x := var w :| w == 2*w; w;

+  }

+  var t := {3, 5};

+  var s := var a, b :| a in t && b in t && a != b; {a} + {b};

+  assert s == t;

+}

diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect
index b82e06ad..36fc9361 100644
--- a/Test/dafny0/LetExpr.dfy.expect
+++ b/Test/dafny0/LetExpr.dfy.expect
@@ -29,7 +29,11 @@ LetExpr.dfy(306,12): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

+LetExpr.dfy(316,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

 

-Dafny program verifier finished with 38 verified, 8 errors

+Dafny program verifier finished with 39 verified, 9 errors

 

 Dafny program verifier finished with 0 verified, 0 errors

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 78288b1e..f0138c6c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -541,11 +541,11 @@ module NoTypeArgs1 {
 method LetSuchThat(ghost z: int, n: nat)

 {

   var x: int;

-  x := var y :| y < 0; y;  // error: let-such-that not allowed in non-ghost context

+  x := var y :| y < 0; y;  // fine for the resolver (but would give a verification error for not being deterministic)

 

-  x := var y :| y < z; y;  // error (x2): contraint depend on ghost, and let-such-that not allowed in non-ghost context

+  x := var y :| y < z; y;  // error: contraint depend on ghost (z)

 

-  x := var w :| w == 2*w; w;  // error: let-such-that not allowed in non-ghost context

+  x := var w :| w == 2*w; w;  // fine (even for the verifier, this one)

   x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

   ghost var xg := var w :| w == 2*w; w;

 }

@@ -1339,6 +1339,6 @@ module GhostLet {
     x := ghost var tmp := 5; tmp;  // error: ghost -> non-ghost

     x := ghost var tmp := 5; 10;  // fine

     x := ghost var a0, a1 :| a0 == 0 && a1 == 1; a0 + a1;  // error: ghost -> non-ghost

-    x := ghost var a :| true; 10;  // error: (conservatively) considered ghost -> non-ghost

+    x := ghost var a :| 0 <= a; 10;  // fine

   }

 }

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index fd214fa8..c215d354 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -90,8 +90,6 @@ ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a typ
 ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(1341,9): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(1342,9): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

@@ -169,10 +167,7 @@ ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(386,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(544,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(546,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(548,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(549,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses

 ResolutionErrors.dfy(918,9): Error: unresolved identifier: s

@@ -187,4 +182,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-189 resolution/type errors detected in ResolutionErrors.dfy

+184 resolution/type errors detected in ResolutionErrors.dfy