Fix: Compiled lambdas now close only on non-ghost variables (#2854)

RELEASE_NOTES.md

@@ -1,5 +1,6 @@
 # Upcoming
 
+- fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854)
 - fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)
 
 # 3.9.0

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -5093,6 +5093,9 @@ void CreateFreeVarSubstitution(Expression expr, out List<BoundVar> bvars, out Li
       bvars = new List<BoundVar>();
       fexprs = new List<Expression>();
       foreach (var fv in fvs) {
+        if (fv.IsGhost) {
+          continue;
+        }
         fexprs.Add(new IdentifierExpr(fv.Tok, fv.Name) {
           Var = fv, // resolved here!
           Type = fv.Type

Test/git-issues/git-issue-2690.dfy

@@ -0,0 +1,24 @@
+// RUN: %dafny -compile:4 -compileTarget:cs "%s" > "%t"
+// RUN: %dafny -noVerify -compile:4 -compileTarget:js "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method InSeq<T>(ts: seq<T>) returns (f: T --> bool)
+  ensures forall t <- ts :: f.requires(t)
+{
+  ghost var pre := t => t in ts;
+  f := t requires pre(t) => true;
+}
+
+method InSeq2<T>(ghost ts: seq<T>) returns (f: T --> bool)
+  ensures forall t <- ts :: f.requires(t)
+{
+  f := t requires (ghost var b := t in ts; b) => true;
+}
+
+method Main() {
+  var f := InSeq([1, 2]);
+  print "2 in seq? ", f(2),"\n";
+  var g := InSeq2([1, 2]);
+  print "2 in seq? ", g(2),"\n";
+  print "All right";
+}

Test/git-issues/git-issue-2690.dfy.expect

@@ -0,0 +1,9 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+2 in seq? true
+2 in seq? true
+All right
+Dafny program verifier did not attempt verification
+2 in seq? true
+2 in seq? true
+All right

Test/git-issues/git-issue-2852.dfy

@@ -0,0 +1,19 @@
+// RUN: %dafny -compile:3 -compileTarget:cs "%s" > "%t"
+// RUN: %dafny -noVerify -compile:4 -compileTarget:js "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Returns a function that computes the sum of n consecutive integers starting at pos
+function method Sum(
+  ghost remaining: nat,
+  n: nat
+): (p: nat -> nat)
+  decreases remaining
+  requires remaining == n
+{
+  (pos: nat) =>
+    var x: nat := if n == 0 then 0 else Sum(remaining - 1, n - 1)(pos+1) + pos;
+    x
+}
+method Main() {
+  print Sum(5, 5)(10);
+}

Test/git-issues/git-issue-2852.dfy.expect

@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+60
+Dafny program verifier did not attempt verification
+60