diff --git a/.github/workflows/test_models_dafny_verification.yml b/.github/workflows/test_models_dafny_verification.yml index 2449f64db..c1899ac5c 100644 --- a/.github/workflows/test_models_dafny_verification.yml +++ b/.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 }} diff --git a/.github/workflows/test_models_net_tests.yml b/.github/workflows/test_models_net_tests.yml index 312a81ad4..5591a9531 100644 --- a/.github/workflows/test_models_net_tests.yml +++ b/.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 ] diff --git a/TestModels/SimpleTypes/SimpleInteger/Makefile b/TestModels/SimpleTypes/SimpleInteger/Makefile new file mode 100644 index 000000000..ba44aae54 --- /dev/null +++ b/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: diff --git a/TestModels/SimpleTypes/SimpleInteger/Model/SimpleInteger.smithy b/TestModels/SimpleTypes/SimpleInteger/Model/SimpleInteger.smithy new file mode 100644 index 000000000..9a87f3966 --- /dev/null +++ b/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 +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/README.md b/TestModels/SimpleTypes/SimpleInteger/README.md new file mode 100644 index 000000000..8e25ce3ee --- /dev/null +++ b/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 ` in the `gradlew run` is used to generate the polymorph wrappers. Similarly `--compileTarget:` flags is used in dafny recipe to transpile to C#. \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/runtimes/net/Extern/WrappedSimpleIntegerService.cs b/TestModels/SimpleTypes/SimpleInteger/runtimes/net/Extern/WrappedSimpleIntegerService.cs new file mode 100644 index 000000000..81036399a --- /dev/null +++ b/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 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.create_Success(wrappedClient); + } + } +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/runtimes/net/SimpleInteger.csproj b/TestModels/SimpleTypes/SimpleInteger/runtimes/net/SimpleInteger.csproj new file mode 100644 index 000000000..9e1980339 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleInteger/runtimes/net/SimpleInteger.csproj @@ -0,0 +1,40 @@ + + + + SimpleInteger + disable + disable + net6.0 + 10 + false + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/runtimes/net/tests/SimpleIntegerTest.csproj b/TestModels/SimpleTypes/SimpleInteger/runtimes/net/tests/SimpleIntegerTest.csproj new file mode 100644 index 000000000..62e3ed009 --- /dev/null +++ b/TestModels/SimpleTypes/SimpleInteger/runtimes/net/tests/SimpleIntegerTest.csproj @@ -0,0 +1,33 @@ + + + + SimpleIntegerTest + disable + disable + net6.0 + 10 + Exe + false + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy b/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy new file mode 100644 index 000000000..68bba029d --- /dev/null +++ b/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) { + 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}; + } + } +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/src/SimpleIntegerImpl.dfy b/TestModels/SimpleTypes/SimpleInteger/src/SimpleIntegerImpl.dfy new file mode 100644 index 000000000..7fcf6a71d --- /dev/null +++ b/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 + {{}} + predicate GetIntegerEnsuresPublicly(input: GetIntegerInput, output: Result) { + true + } + predicate GetIntegerKnownValueTestEnsuresPublicly(input: GetIntegerInput, output: Result) { + true + } + method GetInteger ( config: InternalConfig, input: GetIntegerInput ) + returns (output: Result) { + 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) { + expect input.value.Some?; + expect input.value.UnwrapOr(0) == 20; + var res := GetIntegerOutput(value := input.value); + return Success(res); + } +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/src/WrappedSimpleIntegerImpl.dfy b/TestModels/SimpleTypes/SimpleInteger/src/WrappedSimpleIntegerImpl.dfy new file mode 100644 index 000000000..fe0a2457c --- /dev/null +++ b/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 + } +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/test/SimpleIntegerImplTest.dfy b/TestModels/SimpleTypes/SimpleInteger/test/SimpleIntegerImplTest.dfy new file mode 100644 index 000000000..5450fde69 --- /dev/null +++ b/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 := + [-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; + } + + } +} \ No newline at end of file diff --git a/TestModels/SimpleTypes/SimpleInteger/test/WrappedSimpleIntegerTest.dfy b/TestModels/SimpleTypes/SimpleInteger/test/WrappedSimpleIntegerTest.dfy new file mode 100644 index 000000000..007ebef62 --- /dev/null +++ b/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); + } +} \ No newline at end of file