working around #646

smithy-lang · Oct 18, 2024 · 2967451 · 2967451
1 parent 49c3871
commit 2967451
Show file tree

Hide file tree

Showing 4 changed files with 84 additions and 17 deletions.
diff --git a/TestModels/Resource/Model/resources.smithy b/TestModels/Resource/Model/resources.smithy
@@ -104,5 +104,26 @@ structure MutableResourceReference {}
 @smithy.api#suppress(["MutableLocalStateTrait"])
 @aws.polymorph#mutableLocalState
 resource MutableResource {
-  operations: [ GetResourceData ]
+  operations: [ GetMutableResourceData ]
+}
+
+operation GetMutableResourceData {
+  input: GetMutableResourceDataInput,
+  output: GetMutableResourceDataOutput,
+}
+
+structure GetMutableResourceDataInput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+  integerValue: Integer,
+  longValue: Long,
 }
+
+structure GetMutableResourceDataOutput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+  integerValue: Integer,
+  longValue: Long,
+}
diff --git a/TestModels/Resource/src/MutableResource.dfy b/TestModels/Resource/src/MutableResource.dfy
@@ -18,10 +18,10 @@ module MutableResource {
       // all the things that need to be implement from the trait
       // need to be visible..
       // These are provided so that the spec is not visible.
-      MutableResource.GetResourceData',
+      MutableResource.GetMutableResourceData',
       MutableResource.ValidState,
       MutableResource.InternalValidState,
-      MutableResource.GetResourceDataEnsuresPublicly,
+      MutableResource.GetMutableResourceDataEnsuresPublicly,
       // These are values that need to be visible
       // because they are in the spec of the constructor.
       MutableResource.value,
@@ -76,15 +76,15 @@ module MutableResource {
 
     }
 
-    predicate GetResourceDataEnsuresPublicly(
-      input: Types.GetResourceDataInput,
-      output: Wrappers.Result<Types.GetResourceDataOutput, Types.Error>
+    predicate GetMutableResourceDataEnsuresPublicly(
+      input: Types.GetMutableResourceDataInput,
+      output: Wrappers.Result<Types.GetMutableResourceDataOutput, Types.Error>
     ) {true}
 
-    method GetResourceData'(
-      input: Types.GetResourceDataInput
+    method GetMutableResourceData'(
+      input: Types.GetMutableResourceDataInput
     ) returns (
-        output: Wrappers.Result<Types.GetResourceDataOutput, Types.Error>
+        output: Wrappers.Result<Types.GetMutableResourceDataOutput, Types.Error>
       )
       requires
         && InternalValidState()
@@ -93,7 +93,7 @@ module MutableResource {
       decreases InternalModifies
       ensures
         && InternalValidState()
-      ensures GetResourceDataEnsuresPublicly(input, output)
+      ensures GetMutableResourceDataEnsuresPublicly(input, output)
       ensures unchanged(History)
     {
 
@@ -104,7 +104,7 @@ module MutableResource {
         this.name + " " + input.stringValue.value
       else
         this.name;
-      var rtn: Types.GetResourceDataOutput := Types.GetResourceDataOutput(
+      var rtn: Types.GetMutableResourceDataOutput := Types.GetMutableResourceDataOutput(
         blobValue := input.blobValue,
         booleanValue := input.booleanValue,
         stringValue := Wrappers.Some(rtnString),

diff --git a/TestModels/Resource/test/Helpers.dfy b/TestModels/Resource/test/Helpers.dfy
@@ -52,4 +52,50 @@ module Helpers {
     expect Some(1) == output.integerValue;
     expect Some(1) == output.longValue; 
   }
+
+  function method allMutableNone(): Types.GetMutableResourceDataInput
+  {
+   Types.GetMutableResourceDataInput(
+      blobValue := None,
+      booleanValue := None,
+      stringValue := None,
+      integerValue := None,
+      longValue := None
+    )
+  }
+
+  method checkMutableMostNone(
+    name: string,
+    output: Types.GetMutableResourceDataOutput
+  )
+  {
+    expect Some(name) == output.stringValue;
+    expect None == output.blobValue;
+    expect None == output.booleanValue;
+    expect None == output.integerValue;
+    expect None == output.longValue; 
+  }
+
+  function method allMutableSome(): Types.GetMutableResourceDataInput
+  {
+   Types.GetMutableResourceDataInput(
+      blobValue := Some([1]),
+      booleanValue := Some(true),
+      stringValue := Some("Some"),
+      integerValue := Some(1),
+      longValue := Some(1)
+    )
+  }
+
+  method checkMutableSome(
+    name: string,
+    output: Types.GetMutableResourceDataOutput
+  )
+  {
+    expect Some(name + " Some") == output.stringValue;
+    expect Some([1]) == output.blobValue;
+    expect Some(true) == output.booleanValue;
+    expect Some(1) == output.integerValue;
+    expect Some(1) == output.longValue; 
+  }
 }
diff --git a/TestModels/Resource/test/SimpleResourcesTest.dfy b/TestModels/Resource/test/SimpleResourcesTest.dfy
@@ -92,15 +92,15 @@ module SimpleResourcesTest {
     modifies resource.Modifies
     ensures resource.ValidState()
   {
-    var input := allNone();
+    var input := allMutableNone();
 
     expect resource is MutableResource.MutableResource;
     var test:MutableResource.MutableResource := resource;
 
     var before := test.MyInternalState;
 
-    var result :- expect resource.GetResourceData(input);
-    checkMostNone(config.name, result);
+    var result :- expect resource.GetMutableResourceData(input);
+    checkMutableMostNone(config.name, result);
 
     // This sort of things SHOULD NOT be able to be proved.
     // Dafny does not have a way to say `assert something is impossible to prove;`
@@ -123,9 +123,9 @@ module SimpleResourcesTest {
     modifies resource.Modifies
     ensures resource.ValidState()
   {
-    var input := allSome();
-    var output :- expect resource.GetResourceData(input);
-    checkSome(config.name, output);
+    var input := allMutableSome();
+    var output :- expect resource.GetMutableResourceData(input);
+    checkMutableSome(config.name, output);
   }
 
   method TestGetMutableResources(