Fix a bug related to hide/reveal and recursive functions (#5764)

Fixes #5763

Requires the upcoming Boogie version 3.2.5, for which this PR needs to
be merged first: boogie-org/boogie#945

### Description
- No longer allow hiding functions from the Dafny prelude by using `hide
*`. This affected recursive functions because they use `$LS` which is
defined in the prelude.

### How has this been tested?
- Added a CLI test-case to `revealFunctions.dfy`

<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/DafnyCore.csproj

@@ -34,7 +34,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.5" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -85,6 +85,9 @@ public BoogieGenerator(ErrorReporter reporter, ProofDependencyManager depManager
       Bpl.Program boogieProgram = ReadPrelude();
       if (boogieProgram != null) {
         sink = boogieProgram;
+        foreach (var function in boogieProgram.TopLevelDeclarations.OfType<Bpl.Function>()) {
+          function.AlwaysRevealed = true;
+        }
         predef = FindPredefinedDecls(boogieProgram);
       }
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy

@@ -84,4 +84,22 @@ method ReadsClause() {
       reveal Obj;
     }
   }
+}
+
+module M1 {
+    ghost function RecFunc(x: nat): nat { 
+        if x == 0 then 0
+        else 1 + RecFunc(x - 1)
+    }
+}
+module M2 {
+    import opened M1
+    lemma Lemma(x: nat) 
+    ensures RecFunc(0) == 0
+    {
+        // Because RecFunc is recursive, it uses the fuel related $LS function, 
+        // this was previously hidden by 'hide *', so that the ensures could not be proven
+        hide *;
+        reveal RecFunc;
+    }
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect

@@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold
 revealFunctions.dfy(22,12): Error: assertion might not hold
 revealFunctions.dfy(49,21): Error: assertion might not hold
 
-Dafny program verifier finished with 15 verified, 3 errors
+Dafny program verifier finished with 22 verified, 3 errors

customBoogie.patch

@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
        <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
        <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
        <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
--      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.5" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

dotnet-tools.json

@@ -9,7 +9,7 @@
       ]
     },
     "boogie": {
-      "version": "3.1.3",
+      "version": "3.2.5",
       "commands": [
         "boogie"
       ]