feat: Allow more assumptions in library backend

Source/DafnyCore/AST/Members/Function.cs

@@ -65,13 +65,13 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
 
     if (HasExternAttribute) {
       yield return new Assumption(this, tok, AssumptionDescription.ExternFunction);
-      if (HasPostcondition && !HasAxiomAttribute) {
-        yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition);
+      if (HasPostcondition) {
+        yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition(HasAxiomAttribute));
       }
     }
 
-    if (HasExternAttribute && HasPrecondition && !HasAxiomAttribute) {
-      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPrecondition);
+    if (HasExternAttribute && HasPrecondition) {
+      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPrecondition(HasAxiomAttribute));
     }
 
     foreach (var c in this.Descendants()) {

Source/DafnyCore/AST/Members/Method.cs

@@ -50,12 +50,12 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
       yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
     }
 
-    if (HasExternAttribute && HasPostcondition && !HasAxiomAttribute) {
-      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition);
+    if (HasExternAttribute && HasPostcondition) {
+      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition(HasAxiomAttribute));
     }
 
-    if (HasExternAttribute && HasPrecondition && !HasAxiomAttribute) {
-      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPrecondition);
+    if (HasExternAttribute && HasPrecondition) {
+      yield return new Assumption(this, tok, AssumptionDescription.ExternWithPrecondition(HasAxiomAttribute));
     }
 
     if (AllowsNontermination) {

Source/DafnyCore/Auditor/Assumption.cs

@@ -25,22 +25,35 @@ 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.",
-    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]).",
-    mitigationIETF: "MUST test any external callers.",
-    isExplicit: false,
-    allowedInLibraries: false);
-  public static AssumptionDescription ExternWithPostcondition = new(
-    issue: "Declaration with [{:extern}] has a ensures clause.",
-    mitigation: "Test external callee (maybe with [/testContracts]).",
-    mitigationIETF: "MUST test external callee.",
+    mitigation: "Turn into a [method] with [modifies {}] or test thoroughly for lack of side effects.",
+    mitigationIETF: "SHOULD use [method] with [modifies {}] instead.",
     isExplicit: false,
     allowedInLibraries: false);
+
+  public static AssumptionDescription ExternWithPrecondition(bool hasAxiomAttribute) {
+    return new(
+      issue: 
+      hasAxiomAttribute
+        ? "Declaration with [{:extern}] and [{:axiom}] has a requires clause."
+        : "Declaration with [{:extern}] has a requires clause.",
+      mitigation: "Test any external callers (maybe with [/testContracts]).",
+      mitigationIETF: "MUST test any external callers.",
+      isExplicit: false,
+      allowedInLibraries: hasAxiomAttribute);
+  }
+
+  public static AssumptionDescription ExternWithPostcondition(bool hasAxiomAttribute) {
+    return new(
+      issue: 
+      hasAxiomAttribute
+        ? "Declaration with [{:extern}] and [{:axiom}] has a ensures clause."
+        : "Declaration with [{:extern}] has a ensures clause.",
+      mitigation: "Test external callee (maybe with [/testContracts]).",
+      mitigationIETF: "MUST test external callee.",
+      isExplicit: false,
+      allowedInLibraries: hasAxiomAttribute);
+  }
+
   public static AssumptionDescription AssumeStatement(bool hasAxiomAttribute) {
     return new(
       issue:
@@ -56,24 +69,23 @@ 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.",
     mitigationIETF: "MUST remove [{:termination false}] or justify.",
     isExplicit: false,
-    allowedInLibraries: false);
+    // DISCUSS: There is no realistic mitigation or way to attach :axiom,
+    // and no other way to share traits in a library.
+    allowedInLibraries: true);
   public static AssumptionDescription ForallWithoutBody = new(
     issue: "Definition contains [forall] statement with no body.",
     mitigation: "Provide a body.",
@@ -86,12 +98,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,22 @@
 
 * Member has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute.
 
+### Member `GenerateBytesWithAxiom`
+
+* Declaration has explicit `{:axiom}` attribute. SHOULD provide a proof or test.
+
+* Declaration with `{:extern}` and `{:axiom}` has a ensures clause. MUST test external callee.
+
+* Declaration with `{:extern}` and `{:axiom}` has a requires clause. MUST test any external callers.
+
+### Member `ExternFunctionWithAxiom`
+
+* Declaration has explicit `{:axiom}` attribute. SHOULD provide a proof or test.
+
+* Function with `{:extern}` attribute. SHOULD use `method` with `modifies {}` instead.
+
+* Declaration with `{:extern}` and `{:axiom}` has a ensures clause. MUST test external callee.
+
 ## 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 {}` or 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> or 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 {}` or 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,16 @@ 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