Allow translating by blocks (#6050)

### What was changed?
Allow translating by blocks

### How has this been tested?
Updated CLI tests

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -558,6 +558,9 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
         case TryRecoverStatement h:
           EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr);
           break;
+        case BlockByProofStmt blockByProofStmt:
+          TrStmt(blockByProofStmt.Body, wr, wStmts);
+          break;
         default:
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy

@@ -492,7 +492,9 @@ module NativeArrays {
     var iIndex: int, bIndex: byte, bvIndex: bv9 := 3, 4, 5;
     m[iIndex, bIndex] := arr[iIndex];
     arr[iIndex] := m[iIndex, bvIndex - 1];
-    assert arr[iIndex] == 17;
+    assert arr[iIndex] == 17 by {
+       assert true;
+    }
     print arr[iIndex], " "; // 17
     m[bIndex, iIndex] := arr[bIndex];
     arr[bIndex] := m[bvIndex - 1, iIndex];

Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy

@@ -8,7 +8,9 @@ include "../exceptions/NatOutcomeDt.dfy"
 include "../exceptions/GenericOutcomeDt.dfy"
 
 method TestAssignOrHalt() {
-    var stmt1: nat :- expect NatSuccess(42);
+    var stmt1: nat :- expect NatSuccess(42) by {
+       assert true;
+    }
     // Regression test for when assign-or-halt was also calling PropagateFailure, which led
     // to the error "type variable 'U' in the function call to 'PropagateFailure' could not be determined"
     // (because of the lack of type constraints).

Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect

@@ -1,12 +1,12 @@
 
 Dafny program verifier finished with 2 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!")
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!")
 
 Dafny program verifier finished with 2 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!")
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!")
 
 Dafny program verifier finished with 2 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!")
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!")
 
 Dafny program verifier finished with 2 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!")
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!")

Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect

@@ -1,15 +1,15 @@
 
 Dafny program verifier finished with 0 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!)
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!)
 
 Dafny program verifier finished with 0 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!)
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!)
 
 Dafny program verifier finished with 0 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!)
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!)
 
 Dafny program verifier finished with 0 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!)
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!)
 
 Dafny program verifier finished with 0 verified, 0 errors
-[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!)
+[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!)

docs/dev/news/6050.fix

@@ -0,0 +1 @@
+Fix a bug that caused a crash when translating by blocks