feat(TestModels): Resource

.github/workflows/test_models_dafny_verification.yml

@@ -19,6 +19,7 @@ jobs:
           TestModels/Errors,
           TestModels/Extendable,
           TestModels/Refinement,
+          TestModels/Resource,
           TestModels/SimpleTypes/SimpleBoolean,
           TestModels/SimpleTypes/SimpleBlob,
           TestModels/SimpleTypes/SimpleEnum,

.github/workflows/test_models_net_tests.yml

@@ -18,6 +18,7 @@ jobs:
           TestModels/Errors,
           TestModels/Extendable,
           TestModels/Refinement,
+          TestModels/Resource,          
           TestModels/SimpleTypes/SimpleBoolean,
           TestModels/SimpleTypes/SimpleBlob,
           TestModels/SimpleTypes/SimpleEnum,

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/README.md

@@ -0,0 +1,66 @@
+# Resource
+
+This project tests [Smithy-Polymorph's](../../smithy-polymorph) support 
+for the smithy shape 
+[resource](https://smithy.io/1.0/spec/core/model.html#resource) 
+and the associated operations in `dafny` and `.NET`.
+
+## What is under test?
+
+The `resource` shape causes Smithy-Polymorph to generate a Class
+(or the language's equivalent)
+along with methods for all of a resource's operations.
+
+In Dafny, there is no such thing as an abstract class,
+so Smithy-Polymorph generates a Trait that describes the class.
+
+Users than implement a Dafny class that extends this trait.
+
+The Smithy-Polymorph expectation is that the behavior of this class
+will be entirely defined in the Dafny implementation.
+
+(Even if this expectation is not true, any Native logic 
+would be referenced via a Dafny extern, 
+and still only exposed via the Dafny implementation).
+
+As such, the Non-Dafny generated classes are merely wrappers
+to the Dafny implementation,
+providing input validation, conversion of the input or output,
+and protecting the Dafny implementation from unknown exceptions
+that would violate Dafny's Formal Verification assumptions.
+
+
+## Build
+### Dafny
+1. Generate the Abstract Dafny code
+```
+make polymorph_dafny
+```
+
+2. Validate the manually written Dafny Code
+```
+make verify
+```
+
+### .NET
+1. Generate the Wrappers using `polymorph`
+```
+make polymorph_net
+```
+
+2. Transpile the tests (and implementation) to the target runtime.
+```
+make transpile_net
+```
+
+3. Generate the executable in the .NET and execute the tests
+```
+make setup_net format_net test_net
+```
+
+## Development
+1. To add another target runtime support,
+   edit the `Makefile` and add the appropriate recipe to 
+   generate the `polymorph` wrappers, and Dafny transpilation.
+2. Provide any glue code between dafny and target runtime if required.
+3. Build, execute, and test in the target runtime.

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};
+    }
+  }
+}
+