feat: Allow more assumptions in library backend (#4545)

The "library backend" which is selected using `--target:lib` and
produces `.doo` files is currently more restrictive than the other
backends. The common SinglePassCompiler logic rejects features that
cannot be compiled such as `assume` statements without `{:axiom}`, but
the library backend doesn't actually use that base class. It instead
leverages the `Declaration.Assumptions()` method that the auditor uses
to identify assumptions. `AssumptionDescription`s have a
`allowedInLibraries` flag to indicate whether they should cause build
errors when trying to build a `.doo` file, and the initial version was
intentionally very conservative.

This PR switches the value of this flag for a few cases that are very
likely to appear in useful libraries and where the risk of misuse is
zero or very low:

* `assume {:axiom} ...` - already allowed by other backends.
* `decreases *` - not really an assumption, more of a sound
specification limitation, and we may even remove this from the auditor
as well in the future.
* `{:extern}` declarations with `requires` or `ensures` - now allowed
only if the declaration also has `{:axiom}`, and this case now creates
auditor warnings as well.
* ~`{:termination false}` - allowed because there is no mitigation and
traits are highly valuable to share in libraries.~ This is worth
discussing, and the better alternative may be to support an assumption
attribute on the class extending a trait instead, so that the assumption
appears in the consumer instead of the library code. (Update: I reverted
the change to allow this attribute in libraries and will implement the
alternative instead in a separate PR)

Also corrected a typo in mitigation text suggesting `modifies *` when it
should be `modifies {}` - `modifies *` doesn't even parse. :)

<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/Auditor/Assumption.cs

@@ -25,10 +25,11 @@ bool allowedInLibraries
     allowedInLibraries: false);
   public static AssumptionDescription ExternFunction = new(
     issue: "Function with [{:extern}] attribute.",
-    mitigation: "Turn into a [method] with [modifies *] or test thoroughly for lack of side effects.",
-    mitigationIETF: "SHOULD use [method] with [modifies *] instead.",
+    mitigation: "Turn into a [method] with [modifies {}] and test thoroughly for lack of side effects.",
+    mitigationIETF: "SHOULD use [method] with [modifies {}] instead.",
     isExplicit: false,
     allowedInLibraries: false);
+
   public static AssumptionDescription ExternWithPrecondition = new(
     issue: "Declaration with [{:extern}] has a requires clause.",
     mitigation: "Test any external callers (maybe with [/testContracts]).",
@@ -41,6 +42,7 @@ bool allowedInLibraries
     mitigationIETF: "MUST test external callee.",
     isExplicit: false,
     allowedInLibraries: false);
+
   public static AssumptionDescription AssumeStatement(bool hasAxiomAttribute) {
     return new(
       issue:
@@ -56,18 +58,15 @@ public static AssumptionDescription AssumeStatement(bool hasAxiomAttribute) {
           ? "SHOULD replace with [assert] and prove."
           : "MUST replace with [assert] and prove or add [{:axiom}].",
       isExplicit: false,
-      allowedInLibraries: false
+      allowedInLibraries: hasAxiomAttribute
     );
   }
   public static AssumptionDescription MayNotTerminate = new(
     issue: "Method may not terminate (uses [decreases *]).",
     mitigation: "Provide a valid [decreases] clause.",
     mitigationIETF: "SHOULD provide a valid [decreases] clause.",
     isExplicit: false,
-    // This isn't unsound but it's hard to imagine useful libraries
-    // with non-terminating methods. If we ever want to offer something like a
-    // top-level event loop driver we can revisit.
-    allowedInLibraries: false);
+    allowedInLibraries: true);
   public static AssumptionDescription HasTerminationFalseAttribute = new(
     issue: "Trait method calls may not terminate (uses [{:termination false}]).",
     mitigation: "Remove if possible.",
@@ -86,12 +85,6 @@ public static AssumptionDescription AssumeStatement(bool hasAxiomAttribute) {
     mitigationIETF: "MUST provide a body.",
     isExplicit: false,
     allowedInLibraries: false);
-  public static AssumptionDescription HasConcurrentAttribute = new(
-    issue: "Declaration has [{:concurrent}] attribute.",
-    mitigation: "Manually review and test in a concurrent setting.",
-    mitigationIETF: "MUST manually review and test in a concurrent setting.",
-    isExplicit: false,
-    allowedInLibraries: false);
 
   public static AssumptionDescription NoBody(bool isGhost) {
     return new(

Test/auditor/TestAuditor.dfy

@@ -134,4 +134,13 @@ method AssertOnly() {
 
 method {:only} MethodOnly() {
   assert false;
-}
+}
+
+// Externs with {:axiom} (only changes whether the externs are allowed by the library backend)
+
+method {:extern} {:axiom} GenerateBytesWithAxiom(i: int32) returns (res: seq<uint8>)
+    requires i >= 0
+    ensures |res| == i as int
+
+function {:extern} {:axiom} ExternFunctionWithAxiom(i: int32): (res: int32)
+  ensures res != i

Test/auditor/TestAuditor.dfy-ietf.md.expect

@@ -38,7 +38,7 @@
 
 ### Member `ExternFunction`
 
-* Function with `{:extern}` attribute. SHOULD use `method` with `modifies *` instead.
+* Function with `{:extern}` attribute. SHOULD use `method` with `modifies {}` instead.
 
 * Declaration with `{:extern}` has a ensures clause. MUST test external callee.
 
@@ -74,6 +74,16 @@
 
 * Member has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute.
 
+### Member `GenerateBytesWithAxiom`
+
+* Declaration has explicit `{:axiom}` attribute. SHOULD provide a proof or test.
+
+### Member `ExternFunctionWithAxiom`
+
+* Declaration has explicit `{:axiom}` attribute. SHOULD provide a proof or test.
+
+* Function with `{:extern}` attribute. SHOULD use `method` with `modifies {}` instead.
+
 ## Type `T`
 
 * Trait method calls may not terminate (uses `{:termination false}`). MUST remove `{:termination false}` or justify.

Test/auditor/TestAuditor.dfy.expect

@@ -16,15 +16,17 @@ TestAuditor.dfy(50,17): Warning: GenerateBytesWithModel: Declaration with `{:ext
 TestAuditor.dfy(50,17): Warning: GenerateBytesWithModel: Declaration with `{:extern}` has a requires clause. Possible mitigation: Test any external callers (maybe with `/testContracts`).
 TestAuditor.dfy(60,2): Warning: GenerateBytesWrapper: Definition has `assume {:axiom}` statement in body. Possible mitigation: Replace with `assert` and prove.
 TestAuditor.dfy(68,17): Warning: GenerateBytesNoGuarantee: Declaration with `{:extern}` has a requires clause. Possible mitigation: Test any external callers (maybe with `/testContracts`).
-TestAuditor.dfy(72,19): Warning: ExternFunction: Function with `{:extern}` attribute. Possible mitigation: Turn into a `method` with `modifies *` or test thoroughly for lack of side effects.
+TestAuditor.dfy(72,19): Warning: ExternFunction: Function with `{:extern}` attribute. Possible mitigation: Turn into a `method` with `modifies {}` and test thoroughly for lack of side effects.
 TestAuditor.dfy(72,19): Warning: ExternFunction: Declaration with `{:extern}` has a ensures clause. Possible mitigation: Test external callee (maybe with `/testContracts`).
 TestAuditor.dfy(83,7): Warning: DoesNotTerminate: Method may not terminate (uses `decreases *`). Possible mitigation: Provide a valid `decreases` clause.
 TestAuditor.dfy(95,4): Warning: ForallWithoutBody: Definition contains `forall` statement with no body. Possible mitigation: Provide a body.
 TestAuditor.dfy(102,4): Warning: LoopWithoutBody: Definition contains loop with no body. Possible mitigation: Provide a body.
 TestAuditor.dfy(116,16): Warning: AxiomWithStuffInIt: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
 TestAuditor.dfy(131,2): Warning: AssertOnly: Assertion has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
 TestAuditor.dfy(135,15): Warning: MethodOnly: Member has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
+TestAuditor.dfy(141,26): Warning: GenerateBytesWithAxiom: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
+TestAuditor.dfy(145,28): Warning: ExternFunctionWithAxiom: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
 TestAuditor.dfy(89,27): Warning: T: Trait method calls may not terminate (uses `{:termination false}`). Possible mitigation: Remove if possible.
-Dafny auditor completed with 18 findings
+Dafny auditor completed with 20 findings
 
 Dafny program verifier did not attempt verification

Test/auditor/TestAuditor.dfy.html.expect

@@ -42,14 +42,16 @@
 <tr><td>GenerateBytesWithModel</td><td>True</td><td>False</td><td>True</td><td>Declaration with <code>{:extern}</code> has a requires clause.</td><td>Test any external callers (maybe with <code>/testContracts</code>).</td></tr>
 <tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has <code>assume {:axiom}</code> statement in body.</td><td>Replace with <code>assert</code> and prove.</td></tr>
 <tr><td>GenerateBytesNoGuarantee</td><td>True</td><td>False</td><td>True</td><td>Declaration with <code>{:extern}</code> has a requires clause.</td><td>Test any external callers (maybe with <code>/testContracts</code>).</td></tr>
-<tr><td>ExternFunction</td><td>True</td><td>False</td><td>True</td><td>Function with <code>{:extern}</code> attribute.</td><td>Turn into a <code>method</code> with <code>modifies *</code> or test thoroughly for lack of side effects.</td></tr>
+<tr><td>ExternFunction</td><td>True</td><td>False</td><td>True</td><td>Function with <code>{:extern}</code> attribute.</td><td>Turn into a <code>method</code> with <code>modifies {}</code> and test thoroughly for lack of side effects.</td></tr>
 <tr><td>ExternFunction</td><td>True</td><td>False</td><td>True</td><td>Declaration with <code>{:extern}</code> has a ensures clause.</td><td>Test external callee (maybe with <code>/testContracts</code>).</td></tr>
 <tr><td>DoesNotTerminate</td><td>True</td><td>False</td><td>False</td><td>Method may not terminate (uses <code>decreases *</code>).</td><td>Provide a valid <code>decreases</code> clause.</td></tr>
 <tr><td>ForallWithoutBody</td><td>False</td><td>False</td><td>False</td><td>Definition contains <code>forall</code> statement with no body.</td><td>Provide a body.</td></tr>
 <tr><td>LoopWithoutBody</td><td>True</td><td>False</td><td>False</td><td>Definition contains loop with no body.</td><td>Provide a body.</td></tr>
 <tr><td>AxiomWithStuffInIt</td><td>True</td><td>True</td><td>False</td><td>Declaration has explicit <code>{:axiom}</code> attribute.</td><td>Provide a proof or test.</td></tr>
 <tr><td>AssertOnly</td><td>True</td><td>False</td><td>False</td><td>Assertion has explicit temporary <code>{:only}</code> attribute.</td><td>Remove the <code>{:only}</code> attribute.</td></tr>
 <tr><td>MethodOnly</td><td>True</td><td>False</td><td>False</td><td>Member has explicit temporary <code>{:only}</code> attribute.</td><td>Remove the <code>{:only}</code> attribute.</td></tr>
+<tr><td>GenerateBytesWithAxiom</td><td>True</td><td>True</td><td>True</td><td>Declaration has explicit <code>{:axiom}</code> attribute.</td><td>Provide a proof or test.</td></tr>
+<tr><td>ExternFunctionWithAxiom</td><td>True</td><td>True</td><td>True</td><td>Declaration has explicit <code>{:axiom}</code> attribute.</td><td>Provide a proof or test.</td></tr>
 <tr><td>T</td><td>True</td><td>False</td><td>False</td><td>Trait method calls may not terminate (uses <code>{:termination false}</code>).</td><td>Remove if possible.</td></tr>
 </table>
 <script>$( "table" ).last().addClass( "sortable" );</script>

Test/auditor/TestAuditor.dfy.md.expect

@@ -9,12 +9,14 @@
 | GenerateBytesWithModel | True | False | True | Declaration with `{:extern}` has a requires clause. | Test any external callers (maybe with `/testContracts`). |
 | GenerateBytesWrapper | True | False | False | Definition has `assume {:axiom}` statement in body. | Replace with `assert` and prove. |
 | GenerateBytesNoGuarantee | True | False | True | Declaration with `{:extern}` has a requires clause. | Test any external callers (maybe with `/testContracts`). |
-| ExternFunction | True | False | True | Function with `{:extern}` attribute. | Turn into a `method` with `modifies *` or test thoroughly for lack of side effects. |
+| ExternFunction | True | False | True | Function with `{:extern}` attribute. | Turn into a `method` with `modifies {}` and test thoroughly for lack of side effects. |
 | ExternFunction | True | False | True | Declaration with `{:extern}` has a ensures clause. | Test external callee (maybe with `/testContracts`). |
 | DoesNotTerminate | True | False | False | Method may not terminate (uses `decreases *`). | Provide a valid `decreases` clause. |
 | ForallWithoutBody | False | False | False | Definition contains `forall` statement with no body. | Provide a body. |
 | LoopWithoutBody | True | False | False | Definition contains loop with no body. | Provide a body. |
 | AxiomWithStuffInIt | True | True | False | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. |
 | AssertOnly | True | False | False | Assertion has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. |
 | MethodOnly | True | False | False | Member has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. |
+| GenerateBytesWithAxiom | True | True | True | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. |
+| ExternFunctionWithAxiom | True | True | True | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. |
 | T | True | False | False | Trait method calls may not terminate (uses `{:termination false}`). | Remove if possible. |

Test/dafny0/ForLoops-Resolution.dfy

@@ -75,15 +75,15 @@ module Tests {
   method Termination0()
   {
     var s := 0;
-    for i := 0 to * { // error: * is allowed only if method uses "modifies *"
+    for i := 0 to * { // error: * is allowed only if method uses "decreases *"
       s := s + i;
     }
   }
 
   method Termination1()
   {
     var s := 0;
-    for i := 0 downto * { // error: * is allowed only if method uses "modifies *"
+    for i := 0 downto * { // error: * is allowed only if method uses "decreases *"
       s := s + i;
     }
   }
@@ -92,7 +92,7 @@ module Tests {
   {
     var s := 0;
     for i := 0 downto *
-      decreases * // error: * is allowed only if method uses "modifies *"
+      decreases * // error: * is allowed only if method uses "decreases *"
     {
       s := s + i;
     }

Test/separate-verification/assumptions.dfy.expect

@@ -16,19 +16,17 @@ TestAuditor.dfy(45,17): Error: Declaration with [{:extern}] has a ensures clause
 TestAuditor.dfy(45,17): Error: Declaration with [{:extern}] has a requires clause.
 TestAuditor.dfy(50,17): Error: Declaration with [{:extern}] has a ensures clause.
 TestAuditor.dfy(50,17): Error: Declaration with [{:extern}] has a requires clause.
-TestAuditor.dfy(60,2): Error: Definition has [assume {:axiom}] statement in body.
 TestAuditor.dfy(68,17): Error: Declaration with [{:extern}] has a requires clause.
 TestAuditor.dfy(72,19): Error: Function with [{:extern}] attribute.
 TestAuditor.dfy(72,19): Error: Declaration with [{:extern}] has a ensures clause.
-TestAuditor.dfy(83,7): Error: Method may not terminate (uses [decreases *]).
 TestAuditor.dfy(95,4): Error: Definition contains [forall] statement with no body.
 TestAuditor.dfy(102,4): Error: Definition contains loop with no body.
 TestAuditor.dfy(117,2): Error: Definition has [assume] statement in body.
-TestAuditor.dfy(118,2): Error: Definition has [assume {:axiom}] statement in body.
 TestAuditor.dfy(120,2): Error: Definition contains [forall] statement with no body.
 TestAuditor.dfy(124,2): Error: Definition contains loop with no body.
 TestAuditor.dfy(131,2): Error: Assertion has explicit temporary [{:only}] attribute.
 TestAuditor.dfy(135,15): Error: Member has explicit temporary [{:only}] attribute.
+TestAuditor.dfy(145,28): Error: Function with [{:extern}] attribute.
 IgnoredAssumptions.dfy(2,15): Error: Ghost declaration has no body and has an ensures clause.
 TestAuditor.dfy(89,27): Error: Trait method calls may not terminate (uses [{:termination false}]).
 Wrote textual form of partial target program to assumptions-lib/assumptions.doo