Penetrating by blocks

Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs

@@ -53,10 +53,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write("{0}: ", assertStmt.Label.Name);
         }
         PrintExpression(expr, true);
-        if (assertStmt != null && assertStmt.Proof != null) {
-          wr.Write(" by ");
-          PrintStatement(assertStmt.Proof, indent);
-        } else if (expectStmt != null && expectStmt.Message != null) {
+        if (expectStmt is { Message: not null }) {
           wr.Write(", ");
           PrintExpression(expectStmt.Message, true);
           wr.Write(";");
@@ -363,7 +360,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
         }
         PrintUpdateRHS(s, indent);
-        PrintBy(s);
+        wr.Write(";");
 
       } else if (stmt is CallStmt) {
         // Most calls are printed from their concrete syntax given in the input. However, recursive calls to
@@ -395,7 +392,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
           PrintUpdateRHS(s.Update, indent);
         }
-        PrintBy(s.Update);
+        wr.Write(";");
       } else if (stmt is VarDeclPattern) {
         var s = (VarDeclPattern)stmt;
         if (s.tok is AutoGeneratedToken) {
@@ -454,20 +451,6 @@ public void PrintStatement(Statement stmt, int indent) {
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
-
-      void PrintBy(ConcreteUpdateStatement statement) {
-        BlockStmt proof = statement switch {
-          UpdateStmt updateStmt => updateStmt.Proof,
-          AssignOrReturnStmt returnStmt => returnStmt.Proof,
-          _ => null
-        };
-        if (proof != null) {
-          wr.Write(" by ");
-          PrintStatement(proof, indent);
-        } else {
-          wr.Write(";");
-        }
-      }
     }
 
     private void PrintHideReveal(HideRevealStmt revealStmt) {

Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

@@ -559,9 +559,9 @@ public bool SetIndentAssertLikeStatement(Statement stmt, int indent) {
       }
     }
 
-    if (stmt is AssertStmt { Proof: { StartToken: { } startToken } }) {
-      SetOpeningIndentedRegion(startToken, indent);
-    }
+    // if (stmt is AssertStmt { Proof: { StartToken: { } startToken } }) {
+    //   SetOpeningIndentedRegion(startToken, indent);
+    // }
 
     return true;
   }

Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs

@@ -9,8 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable<AssignOrRe
   public readonly ExprRhs Rhs; // this is the unresolved RHS, and thus can also be a method call
   public readonly List<AssignmentRhs> Rhss;
   public readonly AttributedToken KeywordToken;
-  public readonly BlockStmt Proof;
-  [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();
+  [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new();
   public override IEnumerable<Statement> SubStatements => ResolvedStatements;
   public override IToken Tok {
     get {
@@ -23,7 +22,8 @@ public override IToken Tok {
     }
   }
 
-  public override IEnumerable<INode> Children => ResolvedStatements.Concat(Proof?.Children ?? new List<INode>());
+  public override IEnumerable<INode> Children => ResolvedStatements;
+
   public override IEnumerable<Statement> PreResolveSubStatements => Enumerable.Empty<Statement>();
 
   [ContractInvariantMethod]
@@ -44,14 +44,13 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo
     Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs);
     Rhss = original.Rhss.ConvertAll(cloner.CloneRHS);
     KeywordToken = cloner.AttributedTok(original.KeywordToken);
-    Proof = cloner.CloneBlockStmt(original.Proof);
 
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss, BlockStmt proof = null)
+  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss)
     : base(rangeToken, lhss) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(lhss != null);
@@ -61,7 +60,6 @@ public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs
     Rhs = rhs;
     Rhss = rhss;
     KeywordToken = keywordToken;
-    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -193,8 +191,6 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       return;
     }
 
-    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
-
     Expression lhsExtract = null;
     if (expectExtract) {
       if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) {
@@ -290,7 +286,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract,
       }
     }
     // " temp, ... := MethodOrExpression, ...;"
-    UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof);
+    var up = new UpdateStmt(RangeToken, lhss2, rhss2);
     if (expectExtract) {
       up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0];
     }
@@ -306,7 +302,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract,
       } else if (token.val == "assume") {
         ss = new AssumeStmt(new RangeToken(token, EndToken), notFailureExpr, SystemModuleManager.AxiomAttribute(KeywordToken.Attrs));
       } else if (token.val == "assert") {
-        ss = new AssertStmt(new RangeToken(token, EndToken), notFailureExpr, null, null, KeywordToken.Attrs);
+        ss = new AssertStmt(new RangeToken(token, EndToken), notFailureExpr, null, KeywordToken.Attrs);
       } else {
         Contract.Assert(false, $"Invalid token in :- statement: {token.val}");
       }

Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs

@@ -8,7 +8,6 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable<UpdateStmt>, ICanR
   public readonly List<AssignmentRhs> Rhss;
   public readonly bool CanMutateKnownState;
   public Expression OriginalInitialLhs = null;
-  public readonly BlockStmt Proof;
 
   public override IToken Tok {
     get {
@@ -23,7 +22,7 @@ public override IToken Tok {
   }
 
   [FilledInDuringResolution] public List<Statement> ResolvedStatements;
-  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>().Concat(Proof != null ? Proof.SubStatements : new List<Statement>());
+  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>();
 
   public override IEnumerable<Expression> NonSpecificationSubExpressions =>
     ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty<Expression>();
@@ -46,29 +45,26 @@ public UpdateStmt Clone(Cloner cloner) {
   public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) {
     Rhss = original.Rhss.Select(cloner.CloneRHS).ToList();
     CanMutateKnownState = original.CanMutateKnownState;
-    Proof = cloner.CloneBlockStmt(original.Proof);
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, BlockStmt proof = null)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = false;
-    Proof = proof;
   }
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, BlockStmt proof = null)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = mutate;
-    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -127,9 +123,6 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       resolver.ResolveAttributes(rhs, resolutionContext);
     }
 
-    // resolve proof
-    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
-
     // figure out what kind of UpdateStmt this is
     if (firstEffectfulRhs == null) {
       if (Lhss.Count == 0) {
@@ -185,7 +178,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
         foreach (var ll in Lhss) {
           resolvedLhss.Add(ll.Resolved);
         }
-        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof);
+        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
         a.OriginalInitialLhs = OriginalInitialLhs;
         ResolvedStatements.Add(a);
       }

Source/DafnyCore/AST/Statements/BlockByProofStmt.cs

@@ -1,3 +1,5 @@
+using System.Collections.Generic;
+
 namespace Microsoft.Dafny;
 
 public class BlockByProofStmt : Statement, ICanResolveNewAndOld {
@@ -9,11 +11,35 @@ public BlockByProofStmt(RangeToken range, BlockStmt proof, Statement body) : bas
   public Statement Body { get; }
   public BlockStmt Proof { get; }
 
+  public override IEnumerable<Statement> SubStatements => new[] { Body, Proof };
+
   public override void GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
     resolver.ResolveStatement(Body, resolutionContext);
-    resolver.ResolveBlockStatement(Proof, resolutionContext with {
+    ResolveByProof(resolver, Proof, resolutionContext with {
       CodeContext = new CodeContextWrapper(resolutionContext.CodeContext, true)
     });
     base.GenResolve(resolver, resolutionContext);
   }
+
+  // CheckLocalityUpdates
+
+  // GhostInterestVisitor
+  // if (s.Proof != null) {
+  //   Visit(s.Proof, true, "a call-by body");
+  // }
+
+  internal static void ResolveByProof(INewOrOldResolver resolver, BlockStmt proof, ResolutionContext resolutionContext) {
+    if (proof == null) {
+      return;
+    }
+
+    // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
+    var prevLblStmts = resolver.EnclosingStatementLabels;
+    var prevLoopStack = resolver.LoopStack;
+    resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
+    resolver.LoopStack = new List<Statement>();
+    resolver.ResolveStatement(proof, resolutionContext);
+    resolver.EnclosingStatementLabels = prevLblStmts;
+    resolver.LoopStack = prevLoopStack;
+  }
 }

Source/DafnyCore/AST/Statements/Methods/CallStmt.cs

@@ -29,12 +29,11 @@ public override IEnumerable<IdentifierExpr> GetAssignedLocals() {
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
   public Expression OriginalInitialLhs = null;
-  public readonly BlockStmt Proof;
 
-  public Expression Receiver { get { return MethodSelect.Obj; } }
-  public Method Method { get { return (Method)MethodSelect.Member; } }
+  public Expression Receiver => MethodSelect.Obj;
+  public Method Method => (Method)MethodSelect.Member;
 
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null, BlockStmt proof = null)
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null)
     : base(rangeToken) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(cce.NonNullElements(lhs));
@@ -46,7 +45,6 @@ public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr me
     this.MethodSelect = memSel;
     this.overrideToken = overrideToken;
     this.Bindings = new ActualBindings(args);
-    Proof = proof;
   }
 
   public CallStmt Clone(Cloner cloner) {
@@ -58,15 +56,14 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) {
     Lhs = original.Lhs.Select(cloner.CloneExpr).ToList();
     Bindings = new ActualBindings(cloner, original.Bindings);
     overrideToken = original.overrideToken;
-    Proof = cloner.CloneBlockStmt(original.Proof);
   }
 
   /// <summary>
   /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected
   /// to be already resolved, and are all given positionally.
   /// </summary>
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args, BlockStmt proof = null)
-    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) {
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)
+    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
   }
 

Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs

@@ -5,15 +5,13 @@
 namespace Microsoft.Dafny;
 
 public class AssertStmt : PredicateStmt, ICloneable<AssertStmt>, ICanFormat {
-  public readonly BlockStmt Proof;
   public readonly AssertLabel Label;
 
   public AssertStmt Clone(Cloner cloner) {
     return new AssertStmt(cloner, this);
   }
 
   public AssertStmt(Cloner cloner, AssertStmt original) : base(cloner, original) {
-    Proof = cloner.CloneBlockStmt(original.Proof);
     Label = original.Label == null ? null : new AssertLabel(cloner.Tok(original.Label.Tok), original.Label.Name);
   }
 
@@ -22,26 +20,18 @@ public static AssertStmt CreateErrorAssert(INode node, string message, Expressio
     errorMessage.Type = new SeqType(Type.Char);
     var attr = new Attributes("error", new List<Expression> { errorMessage }, null);
     guard ??= Expression.CreateBoolLiteral(node.Tok, false);
-    var assertFalse = new AssertStmt(node.RangeToken, guard, null, null, attr);
+    var assertFalse = new AssertStmt(node.RangeToken, guard, null, attr);
     assertFalse.IsGhost = true;
     return assertFalse;
   }
 
-  public AssertStmt(RangeToken rangeToken, Expression expr, BlockStmt/*?*/ proof, AssertLabel/*?*/ label, Attributes attrs)
+  public AssertStmt(RangeToken rangeToken, Expression expr, AssertLabel/*?*/ label, Attributes attrs)
     : base(rangeToken, expr, attrs) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(expr != null);
-    Proof = proof;
     Label = label;
   }
 
-  public override IEnumerable<Statement> SubStatements {
-    get {
-      if (Proof != null) {
-        yield return Proof;
-      }
-    }
-  }
   public void AddCustomizedErrorMessage(IToken tok, string s) {
     var args = new List<Expression>() { new StringLiteralExpr(tok, s, true) };
     IToken openBrace = tok;
@@ -88,8 +78,6 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co
     }
 
     base.GenResolve(resolver, context);
-
-    ModuleResolver.ResolveByProof(resolver, Proof, context);
   }
 
   public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) {

Source/DafnyCore/AST/Substituter.cs

@@ -766,7 +766,7 @@ protected virtual Statement SubstStmt(Statement stmt) {
         return null;
       } else if (stmt is AssertStmt) {
         var s = (AssertStmt)stmt;
-        r = new AssertStmt(s.RangeToken, Substitute(s.Expr), SubstBlockStmt(s.Proof), s.Label, SubstAttributes(s.Attributes));
+        r = new AssertStmt(s.RangeToken, Substitute(s.Expr), s.Label, SubstAttributes(s.Attributes));
       } else if (stmt is ExpectStmt) {
         var s = (ExpectStmt)stmt;
         r = new ExpectStmt(s.RangeToken, Substitute(s.Expr), Substitute(s.Message), SubstAttributes(s.Attributes));

Source/DafnyCore/Resolver/GhostInterestVisitor.cs

@@ -74,23 +74,17 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
     Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) CodeContext.IsGhost ==> mustBeErasable
     Contract.Assume(mustBeErasable || proofContext == null); // (this is really a precondition) !mustBeErasable ==> proofContext == null 
 
-    if (stmt is AssertStmt || stmt is AssumeStmt) {
+    if (stmt is AssertStmt or AssumeStmt) {
       stmt.IsGhost = true;
-      var assertStmt = stmt as AssertStmt;
-      if (assertStmt != null && assertStmt.Proof != null) {
-        Visit(assertStmt.Proof, true, "an assert-by body");
-      }
-
-    } else if (stmt is ExpectStmt) {
-      stmt.IsGhost = false;
-      var s = (ExpectStmt)stmt;
+    } else if (stmt is ExpectStmt expectStmt) {
+      expectStmt.IsGhost = false;
       if (mustBeErasable) {
-        Error(ErrorId.r_expect_statement_is_not_ghost, stmt, "expect statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+        Error(ErrorId.r_expect_statement_is_not_ghost, expectStmt, "expect statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
       } else {
-        ExpressionTester.CheckIsCompilable(resolver, reporter, s.Expr, codeContext);
+        ExpressionTester.CheckIsCompilable(resolver, reporter, expectStmt.Expr, codeContext);
         // If not provided, the message is populated with a default value in resolution
-        Contract.Assert(s.Message != null);
-        ExpressionTester.CheckIsCompilable(resolver, reporter, s.Message, codeContext);
+        Contract.Assert(expectStmt.Message != null);
+        ExpressionTester.CheckIsCompilable(resolver, reporter, expectStmt.Message, codeContext);
       }
 
     } else if (stmt is PrintStmt) {
@@ -145,10 +139,6 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
       var s = (UpdateStmt)stmt;
       s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext));
       s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost);
-      if (s.Proof != null) {
-        Visit(s.Proof, true, "a call-by body");
-      }
-
     } else if (stmt is AssignOrReturnStmt) {
       var s = (AssignOrReturnStmt)stmt;
       s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext));