feat(TestModels): Resource

TestModels/.gitignore

@@ -16,3 +16,4 @@
 
 # JetBrains
 **/.idea/
+**/Folder.DotSettings.user

TestModels/Resource/Makefile

@@ -0,0 +1,16 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+include ../SharedMakefile.mk
+
+NAMESPACE=simple.resources
+
+# This project has no dependencies 
+# DEPENDENT-MODELS:= 
+# LIBRARIES :=
+transpile_net_dependencies:
+
+format_net:
+	pushd runtimes/net && dotnet format && popd

TestModels/Resource/Model/resources.smithy

@@ -0,0 +1,83 @@
+namespace simple.resources
+
+@aws.polymorph#localService(
+  sdkId: "SimpleResources",
+  config: SimpleResourcesConfig,
+)
+service SimpleResources {
+  version: "2021-11-01",
+  resources: [],
+  operations: [ GetResources ],
+  errors: [ SimpleResourcesException ],
+}
+
+structure SimpleResourcesConfig {
+  @required @length(min: 1) name: String
+}
+
+// This operation MUST
+// return the values given in the Resources.
+// The internal config MUST somehow differ,
+// and this additional information MUST be returned.
+operation GetResources {
+  input: GetResourcesInput,
+  output: GetResourcesOutput,
+}
+
+structure GetResourcesInput {
+  value: String
+}
+
+structure GetResourcesOutput {
+  @required
+  output: SimpleResourceReference
+}
+
+@aws.polymorph#reference(resource: SimpleResource)
+structure SimpleResourceReference {}
+
+resource SimpleResource {
+  operations: [ GetResourceData ]
+}
+
+operation GetResourceData {
+  input: GetResourceDataInput,
+  output: GetResourceDataOutput,
+}
+
+structure GetResourceDataInput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+//  byteValue: Byte,
+//  shortValue: Short,
+  integerValue: Integer,
+  longValue: Long,
+//  floatValue: Float,
+//  doubleValue: Double,
+//  bigIntegerValue: BigInteger,
+//  bigDecimalValue: BigDecimal,
+//  timestampValue: Timestamp,
+}
+
+structure GetResourceDataOutput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+//  byteValue: Byte,
+//  shortValue: Short,
+  integerValue: Integer,
+  longValue: Long,
+//  floatValue: Float,
+//  doubleValue: Double,
+//  bigIntegerValue: BigInteger,
+//  bigDecimalValue: BigDecimal,
+//  timestampValue: Timestamp,
+}
+
+@error("client")
+structure SimpleResourcesException {
+  @required
+  message: String,
+}
+

TestModels/Resource/runtimes/net/.editorconfig

@@ -0,0 +1,29 @@
+###############################
+# Core EditorConfig Options   #
+# See https://github.com/dotnet/format/blob/main/docs/Supported-.editorconfig-options.md
+###############################
+root = true
+# All files
+[*]
+indent_style = space
+
+# XML project files
+[*.{csproj,vbproj,vcxproj,vcxproj.filters,proj,projitems,shproj}]
+indent_size = 2
+
+# XML config files
+[*.{props,targets,ruleset,config,nuspec,resx,vsixmanifest,vsct}]
+indent_size = 2
+
+# Code files
+[*.{cs,csx,vb,vbx}]
+indent_size = 2
+insert_final_newline = true
+
+# Rider is wrong, dotnet_diagnostic is supported
+# noinspection EditorConfigKeyCorrectness
+[*.{cs,vb}]
+dotnet_diagnostic.CS0436.severity = none # The type <> ... conflicts with the imported type <> in ...
+dotnet_diagnostic.CS0162.severity = none # Unreachable code detected
+dotnet_diagnostic.CS0618.severity = none # obsolete
+dotnet_diagnostic.CS0168.severity = none # Unused variable

TestModels/Resource/runtimes/net/Extern/__defualt.cs

@@ -0,0 +1,41 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+using Wrappers_Compile;
+using Simple.Resources;
+using Simple.Resources.Wrapped;
+using Dafny.Simple.Resources.Types;
+using TypeConversion = Simple.Resources.TypeConversion;
+namespace Dafny.Simple.Resources
+{
+  public partial class __default
+  {
+    public static
+      Wrappers_Compile._IResult<
+        SimpleResources_Compile.SimpleResourcesClient, Dafny.Simple.Resources.Types._IError
+      > SimpleResources(Dafny.Simple.Resources.Types._ISimpleResourcesConfig config)
+    {
+      return SimpleResources_Compile.__default.SimpleResources(config);
+    }
+  }
+}
+
+namespace Dafny.Simple.Resources.Wrapped
+{
+  public partial class __default
+  {
+    public static _IResult<
+        Types.ISimpleResourcesClient, Types._IError
+      > WrappedSimpleResources(Types._ISimpleResourcesConfig config)
+    {
+      var wrappedConfig =
+        TypeConversion.FromDafny_N6_simple__N9_resources__S21_SimpleResourcesConfig(
+          config);
+      var impl = new SimpleResources(wrappedConfig);
+      var wrappedClient = new SimpleResourcesShim(impl);
+      return Result<
+        Types.ISimpleResourcesClient, Types._IError
+      >.create_Success(wrappedClient);
+    }
+  }
+}

TestModels/Resource/runtimes/net/SimpleResources.csproj

@@ -0,0 +1,31 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>SimpleResources</RootNamespace>
+    <ImplicitUsings>disable</ImplicitUsings>
+    <Nullable>disable</Nullable>
+    <TargetFrameworks>net6.0</TargetFrameworks>
+    <LangVersion>10</LangVersion>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+    <!--
+      System.Collections.Immutable can be removed once dafny.msbuild is updated with
+      https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
+    -->
+    <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
+    <!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
+    <PackageReference Include="System.ValueTuple" Version="4.5.0" />
+
+    <Compile Include="Extern/**/*.cs" />
+    <Compile Include="Generated/**/*.cs" />
+    <Compile Include="ImplementationFromDafny.cs" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <ProjectReference Include="../../../dafny-dependencies/StandardLibrary/runtimes/net/STD.csproj" />
+  </ItemGroup>
+
+</Project>

TestModels/Resource/runtimes/net/tests/SimpleResourcesTest.csproj

@@ -0,0 +1,28 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>SimpleResourcesTest</RootNamespace>
+    <ImplicitUsings>disable</ImplicitUsings>
+    <Nullable>disable</Nullable>
+    <TargetFrameworks>net6.0</TargetFrameworks>
+    <LangVersion>10</LangVersion>
+    <OutputType>Exe</OutputType>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <!--
+      System.Collections.Immutable can be removed once dafny.msbuild is updated with
+      https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
+    -->
+    <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
+    <!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
+    <PackageReference Include="System.ValueTuple" Version="4.5.0" />
+
+    <ProjectReference Include="../SimpleResources.csproj" />
+    <Compile Include="../Generated/**" />
+    <Compile Include="../Extern/**" />
+    <Compile Include="TestsFromDafny.cs" />
+  </ItemGroup>
+
+</Project>

TestModels/Resource/src/Index.dfy

@@ -0,0 +1,59 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/SimpleResourcesTypes.dfy"
+include "./SimpleResourcesOperations.dfy"
+
+module SimpleResources refines AbstractSimpleResourcesService
+{
+  import Operations = SimpleResourcesOperations
+
+  function method DefaultSimpleResourcesConfig(): SimpleResourcesConfig
+  {
+    SimpleResourcesConfig(
+      name := "default"
+    )
+  }
+
+  method SimpleResources(
+    config: SimpleResourcesConfig
+  ) returns (
+    res: Result<SimpleResourcesClient, Error>
+  )
+  {
+    var internalConfig: Operations.InternalConfig := Operations.Config(
+      name := config.name
+    );
+
+    if Operations.ValidInternalConfig?(internalConfig) {
+      var client := new SimpleResourcesClient(
+        config := internalConfig
+      );
+      return Success(client);
+    } else {
+      return Failure(Types.SimpleResourcesException(
+        message := "Length of name must be greater than 0")
+     );
+    }
+  }
+
+  class SimpleResourcesClient...
+  {
+    predicate ValidState()
+    {
+      && Operations.ValidInternalConfig?(config)
+      && History !in Operations.ModifiesInternalConfig(config)
+      && Modifies == Operations.ModifiesInternalConfig(config) + {History}
+    }
+
+    constructor(
+      config: Operations.InternalConfig
+    )
+    {
+      this.config := config;
+      History := new ISimpleResourcesClientCallHistory();
+      Modifies := Operations.ModifiesInternalConfig(config) + {History};
+    }
+  }
+}
+

TestModels/Resource/src/SimpleResource.dfy

@@ -0,0 +1,69 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/SimpleResourcesTypes.dfy"
+
+module SimpleResource {
+  import opened StandardLibrary
+  import opened Wrappers
+  import Types = SimpleResourcesTypes    
+
+  class SimpleResource extends Types.ISimpleResource
+  {
+    predicate ValidState()
+      ensures ValidState() ==> History in Modifies
+    {
+      && History in Modifies
+    }
+
+    const name: string
+    const value: Option<string>
+
+    constructor (
+      value: Option<string>,
+      name: string
+    )
+      requires |name| > 0
+      ensures this.value == value
+      ensures this.name == name
+      ensures ValidState() && fresh(History) && fresh(Modifies)
+    {
+      this.value := value;
+      this.name := name;
+
+      History := new Types.ISimpleResourceCallHistory();
+      Modifies := {History};
+    }
+
+    predicate GetResourceDataEnsuresPublicly(
+      input: Types.GetResourceDataInput,
+      output: Result<Types.GetResourceDataOutput, Types.Error>
+    ) {true}
+
+    method GetResourceData'(
+      input: Types.GetResourceDataInput
+    ) returns (
+      output: Result<Types.GetResourceDataOutput, Types.Error>
+    )
+      requires ValidState()
+      modifies Modifies - {History}
+      decreases Modifies - {History}
+      ensures && ValidState()
+      ensures GetResourceDataEnsuresPublicly(input, output)
+      ensures unchanged(History)
+    {
+      var rtnString: string := if input.stringValue.Some? then
+        this.name + " " + input.stringValue.value
+      else
+        this.name;
+      var rtn: Types.GetResourceDataOutput := Types.GetResourceDataOutput(
+        blobValue := input.blobValue,
+        booleanValue := input.booleanValue,
+        stringValue := Option.Some(rtnString),
+        integerValue := input.integerValue,
+        longValue := input.longValue
+      );
+      return Success(rtn);  
+    }
+  }
+}