feat(TestModels): Simple Integer (#127)

* feat: SimpleInteger Tests

* fix: README

* chore: Use shared makefile

.github/workflows/test_models_dafny_verification.yml

@@ -13,12 +13,13 @@ jobs:
       matrix:
         library: [
           TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
-          TestModels/SimpleTypes/SimpleString,
+          TestModels/Aggregate,
           TestModels/SimpleTypes/SimpleBoolean,
           TestModels/SimpleTypes/SimpleBlob,
           TestModels/SimpleTypes/SimpleEnum,
+          TestModels/SimpleTypes/SimpleInteger,
           TestModels/SimpleTypes/SimpleLong,
-          TestModels/Aggregate,
+          TestModels/SimpleTypes/SimpleString,
         ]
         os: [ ubuntu-latest ]
     runs-on: ${{ matrix.os }}

.github/workflows/test_models_net_tests.yml

@@ -13,12 +13,13 @@ jobs:
       matrix:
         library: [
           TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
-          TestModels/SimpleTypes/SimpleString,
+          TestModels/Aggregate,
           TestModels/SimpleTypes/SimpleBoolean,
           TestModels/SimpleTypes/SimpleBlob,
           TestModels/SimpleTypes/SimpleEnum,
+          TestModels/SimpleTypes/SimpleInteger,
           TestModels/SimpleTypes/SimpleLong,
-          TestModels/Aggregate,
+          TestModels/SimpleTypes/SimpleString,
         ]
         dotnet-version: [ '6.0.x' ]
         os: [ ubuntu-latest ]

TestModels/SimpleTypes/SimpleInteger/Makefile

@@ -0,0 +1,13 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+include ../../SharedMakefile.mk
+
+NAMESPACE=simple.types.integer
+
+# This project has no dependencies
+# DEPENDENT-MODELS:=
+# LIBRARIES :=
+transpile_net_dependencies:

TestModels/SimpleTypes/SimpleInteger/Model/SimpleInteger.smithy

@@ -0,0 +1,32 @@
+namespace simple.types.integer
+
+@aws.polymorph#localService(
+  sdkId: "SimpleInteger",
+  config: SimpleIntegerConfig,
+)
+service SimpleTypesInteger {
+  version: "2021-11-01",
+  resources: [],
+  operations: [ GetInteger, GetIntegerKnownValueTest ],
+  errors: [],
+}
+
+structure SimpleIntegerConfig {}
+
+operation GetInteger {
+  input: GetIntegerInput,
+  output: GetIntegerOutput,
+}
+
+operation GetIntegerKnownValueTest {
+  input: GetIntegerInput,
+  output: GetIntegerOutput,
+}
+
+structure GetIntegerInput {
+  value: Integer
+}
+
+structure GetIntegerOutput {
+  value: Integer
+}

TestModels/SimpleTypes/SimpleInteger/README.md

@@ -0,0 +1,29 @@
+# SimpleInteger
+
+This project implements the smithy type [integer](https://smithy.io/2.0/spec/simple-types.html#integer) and the associated operations in `dafny`. This is then transpiled to a target runtime, and each tests are executed - either as CI actions or manually.
+
+## Build
+### .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 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.
+
+*Example*
+
+`--output-dotnet <PATH>` in the `gradlew run` is used to generate the polymorph wrappers. Similarly `--compileTarget:<RUNTIME>` flags is used in dafny recipe to transpile to C#.

TestModels/SimpleTypes/SimpleInteger/runtimes/net/Extern/WrappedSimpleIntegerService.cs

@@ -0,0 +1,15 @@
+using Wrappers_Compile;
+using Simple.Types.Integer;
+using Simple.Types.Integer.Wrapped;
+using TypeConversion = Simple.Types.Integer.TypeConversion ;
+namespace Dafny.Simple.Types.Integer.Wrapped
+{
+    public partial class __default {
+        public static _IResult<Types.ISimpleTypesIntegerClient, Types._IError> WrappedSimpleInteger(Types._ISimpleIntegerConfig config) {
+            var wrappedConfig = TypeConversion.FromDafny_N6_simple__N5_types__N7_integer__S19_SimpleIntegerConfig(config);
+            var impl = new SimpleInteger(wrappedConfig);
+            var wrappedClient = new SimpleTypesIntegerShim(impl);
+            return Result<Types.ISimpleTypesIntegerClient, Types._IError>.create_Success(wrappedClient);
+        }
+    }
+}

TestModels/SimpleTypes/SimpleInteger/runtimes/net/SimpleInteger.csproj

@@ -0,0 +1,40 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>SimpleInteger</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>
+
+  <!--
+    TODO .NET assemblies are expected to have an ICON.
+    This MUST be replaced before launch.
+  -->
+  <!-- <ItemGroup>
+    <None Include="..\icon.png" Pack="true" PackagePath="" />
+    <None Include="..\README.md" Pack="true" PackagePath="" />
+  </ItemGroup> -->
+
+</Project>

TestModels/SimpleTypes/SimpleInteger/runtimes/net/tests/SimpleIntegerTest.csproj

@@ -0,0 +1,33 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>SimpleIntegerTest</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="../SimpleInteger.csproj" />
+    <Compile Include="../Extern/**" />
+    <Compile Include="../Generated/**" />
+    <Compile Include="TestsFromDafny.cs" />
+  </ItemGroup>
+
+  <!-- <ItemGroup>
+    <None Include="..\icon.png" Pack="true" PackagePath="" />
+    <None Include="..\README.md" Pack="true" PackagePath="" />
+  </ItemGroup> -->
+
+</Project>

TestModels/SimpleTypes/SimpleInteger/src/Index.dfy

@@ -0,0 +1,28 @@
+include "SimpleIntegerImpl.dfy"
+
+module {:extern "Dafny.Simple.Types.Integer" } SimpleInteger refines AbstractSimpleTypesIntegerService {
+    import Operations = SimpleIntegerImpl
+
+    function method DefaultSimpleIntegerConfig(): SimpleIntegerConfig {
+       SimpleIntegerConfig
+    }
+
+    method SimpleInteger(config: SimpleIntegerConfig)
+    returns (res: Result<SimpleIntegerClient, Error>) {
+        var client := new SimpleIntegerClient(Operations.Config);
+        return Success(client);
+    }
+
+    class SimpleIntegerClient... {
+        predicate ValidState()
+        {
+            && Operations.ValidInternalConfig?(config)
+            && Modifies == Operations.ModifiesInternalConfig(config) + {History}
+        }
+        constructor(config: Operations.InternalConfig) {
+            this.config := config;
+            History := new ISimpleTypesIntegerClientCallHistory();
+            Modifies := Operations.ModifiesInternalConfig(config) + {History};
+        }
+    }
+}

TestModels/SimpleTypes/SimpleInteger/src/SimpleIntegerImpl.dfy

@@ -0,0 +1,30 @@
+include "../Model/SimpleTypesIntegerTypes.dfy"
+
+module SimpleIntegerImpl refines AbstractSimpleTypesIntegerOperations  {
+    datatype Config = Config
+    type InternalConfig = Config
+    predicate ValidInternalConfig?(config: InternalConfig)
+    {true}
+    function ModifiesInternalConfig(config: InternalConfig) : set<object>
+    {{}}
+    predicate GetIntegerEnsuresPublicly(input: GetIntegerInput, output: Result<GetIntegerOutput, Error>) {
+        true
+    }
+    predicate GetIntegerKnownValueTestEnsuresPublicly(input: GetIntegerInput, output: Result<GetIntegerOutput, Error>) {
+        true
+    }
+    method GetInteger ( config: InternalConfig,  input: GetIntegerInput )
+    returns (output: Result<GetIntegerOutput, Error>) {
+        expect input.value.Some?;
+        expect (- UInt.INT32_MAX_LIMIT as int32) <= input.value.UnwrapOr(0) <= ((UInt.INT32_MAX_LIMIT - 1) as int32);
+        var res := GetIntegerOutput(value := input.value);
+        return Success(res);
+    }
+    method GetIntegerKnownValueTest ( config: InternalConfig,  input: GetIntegerInput )
+    returns (output: Result<GetIntegerOutput, Error>) {
+        expect input.value.Some?;
+        expect input.value.UnwrapOr(0) == 20;
+        var res := GetIntegerOutput(value := input.value);
+        return Success(res);
+    }
+}

TestModels/SimpleTypes/SimpleInteger/src/WrappedSimpleIntegerImpl.dfy

@@ -0,0 +1,8 @@
+include "../Model/SimpleTypesIntegerTypesWrapped.dfy"
+
+module {:extern "Dafny.Simple.Types.Integer.Wrapped"} WrappedSimpleTypesIntegerService refines WrappedAbstractSimpleTypesIntegerService {
+    import WrappedService = SimpleInteger
+    function method WrappedDefaultSimpleIntegerConfig(): SimpleIntegerConfig {
+        SimpleIntegerConfig
+    }
+}

TestModels/SimpleTypes/SimpleInteger/test/SimpleIntegerImplTest.dfy

@@ -0,0 +1,57 @@
+include "../src/Index.dfy"
+
+module  SimpleIntegerImplTest {
+    import SimpleInteger
+    import opened StandardLibrary.UInt
+    import opened SimpleTypesIntegerTypes
+    import opened Wrappers
+    method{:test} GetInteger(){
+        var client :- expect SimpleInteger.SimpleInteger();
+        TestGetInteger(client);
+        TestGetIntegerKnownValue(client);
+        TestGetIntegerEdgeCases(client);
+    }
+
+    method TestGetInteger(client: ISimpleTypesIntegerClient)
+      requires client.ValidState()
+      modifies client.Modifies
+      ensures client.ValidState()
+    {
+        var ret :- expect client.GetInteger(SimpleInteger.Types.GetIntegerInput(value:= Some(1)));
+        expect ret.value.UnwrapOr(0) == 1;
+        print ret;
+    }
+
+    method TestGetIntegerKnownValue(client: ISimpleTypesIntegerClient)
+      requires client.ValidState()
+      modifies client.Modifies
+      ensures client.ValidState()
+    {
+        var ret :- expect client.GetIntegerKnownValueTest(SimpleInteger.Types.GetIntegerInput(value:= Some(20)));
+        expect ret.value.UnwrapOr(0) == 20;
+        print ret;
+    }
+
+    method TestGetIntegerEdgeCases(client: ISimpleTypesIntegerClient)
+      requires client.ValidState()
+      modifies client.Modifies
+      ensures client.ValidState()
+    {
+        var inputInteger: seq<int32> :=
+            [-1, 0, 1,
+             // 2^32-1
+             ((UInt.INT32_MAX_LIMIT -1) as int32),
+             // -2^32 -1
+             -((UInt.INT32_MAX_LIMIT -1) as int32)
+            ];
+        for i := 0 to |inputInteger| {
+            var integerValue: int32 := inputInteger[i];
+            print integerValue;
+
+            var ret :- expect client.GetInteger(GetIntegerInput(value:= Some(integerValue)));
+            expect ret.value.UnwrapOr(0) == integerValue;
+            print ret;
+        }
+
+    }
+}

TestModels/SimpleTypes/SimpleInteger/test/WrappedSimpleIntegerTest.dfy

@@ -0,0 +1,14 @@
+include "../src/WrappedSimpleIntegerImpl.dfy"
+include "SimpleIntegerImplTest.dfy"
+
+module WrappedSimpleTypesIntegerTest {
+    import WrappedSimpleTypesIntegerService
+    import SimpleIntegerImplTest
+    import opened Wrappers
+    method{:test} GetInteger() {
+        var client :- expect WrappedSimpleTypesIntegerService.WrappedSimpleInteger();
+        SimpleIntegerImplTest.TestGetInteger(client);
+        SimpleIntegerImplTest.TestGetIntegerKnownValue(client);
+        SimpleIntegerImplTest.TestGetIntegerEdgeCases(client);
+    }
+}