diff --git a/TestModels/HistoryAfter/Makefile b/TestModels/HistoryAfter/Makefile new file mode 100644 index 0000000000..5285f8ef55 --- /dev/null +++ b/TestModels/HistoryAfter/Makefile @@ -0,0 +1,12 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +CORES=2 + +include ../SharedMakefile.mk + +NAMESPACE=simple.types.smithyString + +# This project has no dependencies +# DEPENDENT-MODELS:= +# LIBRARIES := diff --git a/TestModels/HistoryAfter/Model/SimpleString.smithy b/TestModels/HistoryAfter/Model/SimpleString.smithy new file mode 100644 index 0000000000..60041441e8 --- /dev/null +++ b/TestModels/HistoryAfter/Model/SimpleString.smithy @@ -0,0 +1,39 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +namespace simple.types.smithyString + +@aws.polymorph#localService( + sdkId: "SimpleString", + config: SimpleStringConfig, +) +service SimpleTypesString { + version: "2021-11-01", + resources: [], + operations: [ GetString, GetStringSingleValue, GetStringUTF8 ], + errors: [], +} + +structure SimpleStringConfig {} + +operation GetString { + input: GetStringInput, + output: GetStringOutput, +} + +operation GetStringSingleValue { + input: GetStringInput, + output: GetStringOutput, +} + +operation GetStringUTF8 { + input: GetStringInput, + output: GetStringOutput, +} + +structure GetStringInput { + value: String +} + +structure GetStringOutput { + value: String +} diff --git a/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypes.dfy b/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypes.dfy new file mode 100644 index 0000000000..631c048291 --- /dev/null +++ b/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypes.dfy @@ -0,0 +1,375 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../../dafny-dependencies/StandardLibrary/src/Index.dfy" + module {:extern "simple.types.smithystring.internaldafny.types" } SimpleTypesSmithyStringTypes + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Histories + + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + + // Begin Generated Types + + datatype GetStringInput = | GetStringInput ( + nameonly value: Option + ) + datatype GetStringOutput = | GetStringOutput ( + nameonly value: Option + ) + datatype SimpleStringConfig = | SimpleStringConfig ( + + ) + +class GetStringEvent extends Event { + const input: GetStringInput + const output: Result + ghost constructor(input: GetStringInput, output: Result) + ensures this.input == input + ensures this.output == output + { + this.input := input; + this.output := output; + } + static predicate WasNthLastWith(history: History, n: nat, p: GetStringEvent -> bool) + reads history + { + && n < |history.events| + && var e: Event := history.events[|history.events| - 1 - n]; + && e is GetStringEvent + && var e' := e as GetStringEvent; + && p(e') + } + +} +class GetStringSingleValueEvent extends Event { + const input: GetStringInput + const output: Result + ghost constructor(input: GetStringInput, output: Result) + ensures this.input == input + ensures this.output == output + { + this.input := input; + this.output := output; + } + static predicate WasNthLastWith(history: History, n: nat, p: GetStringSingleValueEvent -> bool) + reads history + { + && n < |history.events| + && var e: Event := history.events[|history.events| - 1 - n]; + && e is GetStringSingleValueEvent + && var e' := e as GetStringSingleValueEvent; + && p(e') + } +} +class GetStringUTF8Event extends Event { + const input: GetStringInput + const output: Result + ghost constructor(input: GetStringInput, output: Result) + ensures this.input == input + ensures this.output == output + { + this.input := input; + this.output := output; + } + static predicate WasNthLastWith(history: History, n: nat, p: GetStringUTF8Event -> bool) + reads history + { + && n < |history.events| + && var e: Event := history.events[|history.events| - 1 - n]; + && e is GetStringUTF8Event + && var e' := e as GetStringUTF8Event; + && p(e') + } +} + + + + trait {:termination false} ISimpleTypesStringClient + { + // Helper to define any additional modifies/reads clauses. + // If your operations need to mutate state, + // add it in your constructor function: + // Modifies := {your, fields, here, History}; + // If you do not need to mutate anything: +// Modifies := {History}; + + ghost const Modifies: set + // For an unassigned field defined in a trait, + // Dafny can only assign a value in the constructor. + // This means that for Dafny to reason about this value, + // it needs some way to know (an invariant), + // about the state of the object. + // This builds on the Valid/Repr paradigm + // To make this kind requires safe to add + // to methods called from unverified code, + // the predicate MUST NOT take any arguments. + // This means that the correctness of this requires + // MUST only be evaluated by the class itself. + // If you require any additional mutation, + // then you MUST ensure everything you need in ValidState. + // You MUST also ensure ValidState in your constructor. + predicate ValidState() + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetString ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringEnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringEvent + && var e' := e as GetStringEvent; + && e'.input == input + && e'.output == output) + ensures history !in Modifies + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetStringSingleValue ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringSingleValueEnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringSingleValueEvent + && var e' := e as GetStringSingleValueEvent; + && e'.input == input + && e'.output == output) + ensures history !in Modifies + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetStringUTF8 ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringUTF8EnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringUTF8Event + && var e' := e as GetStringUTF8Event; + && e'.input == input + && e'.output == output) + ensures history !in Modifies + +} + datatype Error = + // Local Error structures are listed here + + // Any dependent models are listed here + + // The Collection error is used to collect several errors together + // This is useful when composing OR logic. + // Consider the following method: + // + // method FN(n:I) + // returns (res: Result) + // ensures A(I).Success? ==> res.Success? + // ensures B(I).Success? ==> res.Success? + // ensures A(I).Failure? && B(I).Failure? ==> res.Failure? + // + // If either A || B is successful then FN is successful. + // And if A && B fail then FN will fail. + // But what information should FN transmit back to the caller? + // While it may be correct to hide these details from the caller, + // this can not be the globally correct option. + // Suppose that A and B can be blocked by different ACLs, + // and that their representation of I is only eventually consistent. + // How can the caller distinguish, at a minimum for logging, + // the difference between the four failure modes? + // || (!access(A(I)) && !access(B(I))) + // || (!exit(A(I)) && !exit(B(I))) + // || (!access(A(I)) && !exit(B(I))) + // || (!exit(A(I)) && !access(B(I))) + | CollectionOfErrors(list: seq, nameonly message: string) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + type OpaqueError = e: Error | e.Opaque? witness * +} + abstract module AbstractSimpleTypesSmithyStringService + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Histories + import opened Types = SimpleTypesSmithyStringTypes + import Operations : AbstractSimpleTypesSmithyStringOperations + function method DefaultSimpleStringConfig(): SimpleStringConfig + method SimpleString(config: SimpleStringConfig := DefaultSimpleStringConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && res.value.ValidState() + + class SimpleStringClient extends ISimpleTypesStringClient + { + constructor(config: Operations.InternalConfig) + requires Operations.ValidInternalConfig?(config) + ensures + && ValidState() + && this.config == config + const config: Operations.InternalConfig + predicate ValidState() + ensures ValidState() ==> + && Operations.ValidInternalConfig?(config) + && Modifies == Operations.ModifiesInternalConfig(config) + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetString ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringEnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringEvent + && var e' := e as GetStringEvent; + && e'.input == input + && e'.output == output) + { + output := Operations.GetString(config, input); + if history != null { + var event := new GetStringEvent(input, output); + history.AddEvent(event); + } +} + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringSingleValueEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetStringSingleValue ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringSingleValueEnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringSingleValueEvent + && var e' := e as GetStringSingleValueEvent; + && e'.input == input + && e'.output == output) + { + output := Operations.GetStringSingleValue(config, input); + if history != null { + var event := new GetStringSingleValueEvent(input, output); + history.AddEvent(event); + } +} + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringUTF8EnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetStringUTF8 ( input: GetStringInput, ghost history: History? := null ) + returns (output: Result) + requires + && ValidState() + requires history !in Modifies + modifies Modifies , history + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies + ensures + && ValidState() + ensures GetStringUTF8EnsuresPublicly(input, output) + ensures history != null ==> history.NewEventSuchThat((e: Event) => + && e is GetStringUTF8Event + && var e' := e as GetStringUTF8Event; + && e'.input == input + && e'.output == output) + { + output := Operations.GetStringUTF8(config, input); + if history != null { + var event := new GetStringUTF8Event(input, output); + history.AddEvent(event); + } +} + +} +} + abstract module AbstractSimpleTypesSmithyStringOperations { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleTypesSmithyStringTypes + type InternalConfig + predicate ValidInternalConfig?(config: InternalConfig) + function ModifiesInternalConfig(config: InternalConfig): set + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetString ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringEnsuresPublicly(input, output) + + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetStringSingleValue ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringSingleValueEnsuresPublicly(input, output) + + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetStringUTF8 ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringUTF8EnsuresPublicly(input, output) +} diff --git a/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypesWrapped.dfy b/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypesWrapped.dfy new file mode 100644 index 0000000000..db73dd71e1 --- /dev/null +++ b/TestModels/HistoryAfter/Model/SimpleTypesSmithyStringTypesWrapped.dfy @@ -0,0 +1,19 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../../dafny-dependencies/StandardLibrary/src/Index.dfy" + include "../src/Index.dfy" + abstract module WrappedAbstractSimpleTypesSmithyStringService { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleTypesSmithyStringTypes + import WrappedService : AbstractSimpleTypesSmithyStringService + function method WrappedDefaultSimpleStringConfig(): SimpleStringConfig + method {:extern} WrappedSimpleString(config: SimpleStringConfig := WrappedDefaultSimpleStringConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && res.value.ValidState() +} diff --git a/TestModels/HistoryAfter/src/Index.dfy b/TestModels/HistoryAfter/src/Index.dfy new file mode 100644 index 0000000000..d5327d8cab --- /dev/null +++ b/TestModels/HistoryAfter/src/Index.dfy @@ -0,0 +1,29 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "SimpleStringImpl.dfy" + +module {:extern "simple.types.smithystring.internaldafny" } SimpleString refines AbstractSimpleTypesSmithyStringService { + import Operations = SimpleStringImpl + + function method DefaultSimpleStringConfig(): SimpleStringConfig { + SimpleStringConfig + } + + method SimpleString(config: SimpleStringConfig) + returns (res: Result) { + var client := new SimpleStringClient(Operations.Config); + return Success(client); + } + + class SimpleStringClient... { + predicate ValidState() + { + && Operations.ValidInternalConfig?(config) + && Modifies == Operations.ModifiesInternalConfig(config) + } + constructor(config: Operations.InternalConfig) { + this.config := config; + Modifies := Operations.ModifiesInternalConfig(config); + } + } +} diff --git a/TestModels/HistoryAfter/src/SimpleStringImpl.dfy b/TestModels/HistoryAfter/src/SimpleStringImpl.dfy new file mode 100644 index 0000000000..c979c657ec --- /dev/null +++ b/TestModels/HistoryAfter/src/SimpleStringImpl.dfy @@ -0,0 +1,39 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleTypesSmithyStringTypes.dfy" + +module SimpleStringImpl refines AbstractSimpleTypesSmithyStringOperations { + datatype Config = Config + type InternalConfig = Config + predicate ValidInternalConfig?(config: InternalConfig) + {true} + function ModifiesInternalConfig(config: InternalConfig) : set + {{}} + predicate GetStringEnsuresPublicly(input: GetStringInput, output: Result) { + true + } + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput, output: Result) { + true + } + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput, output: Result) { + true + } + method GetString ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + var res := GetStringOutput(value := input.value); + return Success(res); + } + method GetStringSingleValue ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + expect input.value.Some?; + expect input.value.value == "TEST_SIMPLE_STRING_SINGLE_VALUE"; // This is done so as to assert that polymorph layer is doing one way conversion right as well. + var res := GetStringOutput(value := input.value); + return Success(res); + } + method GetStringUTF8 ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + expect input.value.Some?; + var res := GetStringOutput(value := input.value); + return Success(res); + } +} diff --git a/TestModels/HistoryAfter/src/WrappedSimpleStringImpl.dfy b/TestModels/HistoryAfter/src/WrappedSimpleStringImpl.dfy new file mode 100644 index 0000000000..1c706a71b8 --- /dev/null +++ b/TestModels/HistoryAfter/src/WrappedSimpleStringImpl.dfy @@ -0,0 +1,10 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleTypesSmithyStringTypesWrapped.dfy" + +module {:extern "simple.types.smithystring.internaldafny.wrapped"} WrappedSimpleTypesStringService refines WrappedAbstractSimpleTypesSmithyStringService { + import WrappedService = SimpleString + function method WrappedDefaultSimpleStringConfig(): SimpleStringConfig { + SimpleStringConfig + } +} diff --git a/TestModels/HistoryAfter/test/SimpleStringImplTest.dfy b/TestModels/HistoryAfter/test/SimpleStringImplTest.dfy new file mode 100644 index 0000000000..2c9b806261 --- /dev/null +++ b/TestModels/HistoryAfter/test/SimpleStringImplTest.dfy @@ -0,0 +1,82 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/Index.dfy" + +module SimpleStringImplTest { + import SimpleString + import opened SimpleTypesSmithyStringTypes + import opened Wrappers + import opened Histories + method{:test} GetString(){ + var client :- expect SimpleString.SimpleString(); + TestSingleCall(client); + TestMultipleCallsToSameOperation(client); + TestMultipleCallsToDifferentOperations(client); + } + + method TestSingleCall(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var history := new History(); + + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE")), history); + + assert GetStringEvent.WasNthLastWith(history, 0, (e: GetStringEvent) => + && e.input.value == Some("TEST_SIMPLE_STRING_VALUE") + && e.output == Success(ret)); + } + + method TestMultipleCallsToSameOperation(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var history := new History(); + + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE")), history); + var ret2 :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE_2")), history); + + assert GetStringEvent.WasNthLastWith(history, 1, (e: GetStringEvent) => + && e.input.value == Some("TEST_SIMPLE_STRING_VALUE") + && e.output == Success(ret)); + assert GetStringEvent.WasNthLastWith(history, 0, (e: GetStringEvent) => + && e.input.value == Some("TEST_SIMPLE_STRING_VALUE_2") + && e.output == Success(ret2)); + } + + method TestMultipleCallsToDifferentOperations(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var history := new History(); + + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE")), history); + var ret2 :- expect client.GetStringUTF8(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE_2")), history); + + assert |history.events| == 2; + + assert GetStringEvent.WasNthLastWith(history, 1, (e: GetStringEvent) => + && e.input.value == Some("TEST_SIMPLE_STRING_VALUE") + && e.output == Success(ret)); + assert GetStringUTF8Event.WasNthLastWith(history, 0, (e: GetStringUTF8Event) => + && e.input.value == Some("TEST_SIMPLE_STRING_VALUE_2") + && e.output == Success(ret2)); + } + + // Normally from Seq.dfy in dafny-lang/libraries: + + function DropLast(s: seq): seq + requires 0 < |s| + { + s[..(|s| - 1)] + } + + function Last(s: seq): T + requires 0 < |s| + { + s[|s| - 1] + } +} diff --git a/TestModels/HistoryAfter/test/WrappedSimpleStringTest.dfy b/TestModels/HistoryAfter/test/WrappedSimpleStringTest.dfy new file mode 100644 index 0000000000..026aef18bc --- /dev/null +++ b/TestModels/HistoryAfter/test/WrappedSimpleStringTest.dfy @@ -0,0 +1,16 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/WrappedSimpleStringImpl.dfy" +include "SimpleStringImplTest.dfy" + +module WrappedSimpleTypesStringTest { + import WrappedSimpleTypesStringService + import SimpleStringImplTest + import opened Wrappers + method{:test} GetString() { + var client :- expect WrappedSimpleTypesStringService.WrappedSimpleString(); + SimpleStringImplTest.TestSingleCall(client); + SimpleStringImplTest.TestMultipleCallsToSameOperation(client); + SimpleStringImplTest.TestMultipleCallsToDifferentOperations(client); + } +} \ No newline at end of file diff --git a/TestModels/HistoryBefore/Makefile b/TestModels/HistoryBefore/Makefile new file mode 100644 index 0000000000..5285f8ef55 --- /dev/null +++ b/TestModels/HistoryBefore/Makefile @@ -0,0 +1,12 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +CORES=2 + +include ../SharedMakefile.mk + +NAMESPACE=simple.types.smithyString + +# This project has no dependencies +# DEPENDENT-MODELS:= +# LIBRARIES := diff --git a/TestModels/HistoryBefore/Model/SimpleString.smithy b/TestModels/HistoryBefore/Model/SimpleString.smithy new file mode 100644 index 0000000000..60041441e8 --- /dev/null +++ b/TestModels/HistoryBefore/Model/SimpleString.smithy @@ -0,0 +1,39 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +namespace simple.types.smithyString + +@aws.polymorph#localService( + sdkId: "SimpleString", + config: SimpleStringConfig, +) +service SimpleTypesString { + version: "2021-11-01", + resources: [], + operations: [ GetString, GetStringSingleValue, GetStringUTF8 ], + errors: [], +} + +structure SimpleStringConfig {} + +operation GetString { + input: GetStringInput, + output: GetStringOutput, +} + +operation GetStringSingleValue { + input: GetStringInput, + output: GetStringOutput, +} + +operation GetStringUTF8 { + input: GetStringInput, + output: GetStringOutput, +} + +structure GetStringInput { + value: String +} + +structure GetStringOutput { + value: String +} diff --git a/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypes.dfy b/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypes.dfy new file mode 100644 index 0000000000..f44e335145 --- /dev/null +++ b/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypes.dfy @@ -0,0 +1,286 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../../dafny-dependencies/StandardLibrary/src/Index.dfy" + module {:extern "simple.types.smithystring.internaldafny.types" } SimpleTypesSmithyStringTypes + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + + // Begin Generated Types + + datatype GetStringInput = | GetStringInput ( + nameonly value: Option + ) + datatype GetStringOutput = | GetStringOutput ( + nameonly value: Option + ) + datatype SimpleStringConfig = | SimpleStringConfig ( + + ) + class ISimpleTypesStringClientCallHistory { + ghost constructor() { + GetString := []; + GetStringSingleValue := []; + GetStringUTF8 := []; +} + ghost var GetString: seq>> + ghost var GetStringSingleValue: seq>> + ghost var GetStringUTF8: seq>> +} + trait {:termination false} ISimpleTypesStringClient + { + // Helper to define any additional modifies/reads clauses. + // If your operations need to mutate state, + // add it in your constructor function: + // Modifies := {your, fields, here, History}; + // If you do not need to mutate anything: +// Modifies := {History}; + + ghost const Modifies: set + // For an unassigned field defined in a trait, + // Dafny can only assign a value in the constructor. + // This means that for Dafny to reason about this value, + // it needs some way to know (an invariant), + // about the state of the object. + // This builds on the Valid/Repr paradigm + // To make this kind requires safe to add + // to methods called from unverified code, + // the predicate MUST NOT take any arguments. + // This means that the correctness of this requires + // MUST only be evaluated by the class itself. + // If you require any additional mutation, + // then you MUST ensure everything you need in ValidState. + // You MUST also ensure ValidState in your constructor. + predicate ValidState() + ensures ValidState() ==> History in Modifies + ghost const History: ISimpleTypesStringClientCallHistory + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetString ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetString + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringEnsuresPublicly(input, output) + ensures History.GetString == old(History.GetString) + [DafnyCallEvent(input, output)] + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetStringSingleValue ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetStringSingleValue + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringSingleValueEnsuresPublicly(input, output) + ensures History.GetStringSingleValue == old(History.GetStringSingleValue) + [DafnyCallEvent(input, output)] + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + // The public method to be called by library consumers + method GetStringUTF8 ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetStringUTF8 + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringUTF8EnsuresPublicly(input, output) + ensures History.GetStringUTF8 == old(History.GetStringUTF8) + [DafnyCallEvent(input, output)] + +} + datatype Error = + // Local Error structures are listed here + + // Any dependent models are listed here + + // The Collection error is used to collect several errors together + // This is useful when composing OR logic. + // Consider the following method: + // + // method FN(n:I) + // returns (res: Result) + // ensures A(I).Success? ==> res.Success? + // ensures B(I).Success? ==> res.Success? + // ensures A(I).Failure? && B(I).Failure? ==> res.Failure? + // + // If either A || B is successful then FN is successful. + // And if A && B fail then FN will fail. + // But what information should FN transmit back to the caller? + // While it may be correct to hide these details from the caller, + // this can not be the globally correct option. + // Suppose that A and B can be blocked by different ACLs, + // and that their representation of I is only eventually consistent. + // How can the caller distinguish, at a minimum for logging, + // the difference between the four failure modes? + // || (!access(A(I)) && !access(B(I))) + // || (!exit(A(I)) && !exit(B(I))) + // || (!access(A(I)) && !exit(B(I))) + // || (!exit(A(I)) && !access(B(I))) + | CollectionOfErrors(list: seq, nameonly message: string) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + type OpaqueError = e: Error | e.Opaque? witness * +} + abstract module AbstractSimpleTypesSmithyStringService + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleTypesSmithyStringTypes + import Operations : AbstractSimpleTypesSmithyStringOperations + function method DefaultSimpleStringConfig(): SimpleStringConfig + method SimpleString(config: SimpleStringConfig := DefaultSimpleStringConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && fresh(res.value.History) + && res.value.ValidState() + + class SimpleStringClient extends ISimpleTypesStringClient + { + constructor(config: Operations.InternalConfig) + requires Operations.ValidInternalConfig?(config) + ensures + && ValidState() + && fresh(History) + && this.config == config + const config: Operations.InternalConfig + predicate ValidState() + ensures ValidState() ==> + && Operations.ValidInternalConfig?(config) + && History !in Operations.ModifiesInternalConfig(config) + && Modifies == Operations.ModifiesInternalConfig(config) + {History} + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetString ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetString + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringEnsuresPublicly(input, output) + ensures History.GetString == old(History.GetString) + [DafnyCallEvent(input, output)] + { + output := Operations.GetString(config, input); + History.GetString := History.GetString + [DafnyCallEvent(input, output)]; +} + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringSingleValueEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetStringSingleValue ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetStringSingleValue + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringSingleValueEnsuresPublicly(input, output) + ensures History.GetStringSingleValue == old(History.GetStringSingleValue) + [DafnyCallEvent(input, output)] + { + output := Operations.GetStringSingleValue(config, input); + History.GetStringSingleValue := History.GetStringSingleValue + [DafnyCallEvent(input, output)]; +} + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + {Operations.GetStringUTF8EnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetStringUTF8 ( input: GetStringInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetStringUTF8 + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures GetStringUTF8EnsuresPublicly(input, output) + ensures History.GetStringUTF8 == old(History.GetStringUTF8) + [DafnyCallEvent(input, output)] + { + output := Operations.GetStringUTF8(config, input); + History.GetStringUTF8 := History.GetStringUTF8 + [DafnyCallEvent(input, output)]; +} + +} +} + abstract module AbstractSimpleTypesSmithyStringOperations { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleTypesSmithyStringTypes + type InternalConfig + predicate ValidInternalConfig?(config: InternalConfig) + function ModifiesInternalConfig(config: InternalConfig): set + predicate GetStringEnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetString ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringEnsuresPublicly(input, output) + + + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetStringSingleValue ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringSingleValueEnsuresPublicly(input, output) + + + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput , output: Result) + // The private method to be refined by the library developer + + + method GetStringUTF8 ( config: InternalConfig , input: GetStringInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures GetStringUTF8EnsuresPublicly(input, output) +} diff --git a/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypesWrapped.dfy b/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypesWrapped.dfy new file mode 100644 index 0000000000..71bdffeadc --- /dev/null +++ b/TestModels/HistoryBefore/Model/SimpleTypesSmithyStringTypesWrapped.dfy @@ -0,0 +1,20 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../../dafny-dependencies/StandardLibrary/src/Index.dfy" + include "../src/Index.dfy" + abstract module WrappedAbstractSimpleTypesSmithyStringService { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleTypesSmithyStringTypes + import WrappedService : AbstractSimpleTypesSmithyStringService + function method WrappedDefaultSimpleStringConfig(): SimpleStringConfig + method {:extern} WrappedSimpleString(config: SimpleStringConfig := WrappedDefaultSimpleStringConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && fresh(res.value.History) + && res.value.ValidState() +} diff --git a/TestModels/HistoryBefore/src/Index.dfy b/TestModels/HistoryBefore/src/Index.dfy new file mode 100644 index 0000000000..d0d2652190 --- /dev/null +++ b/TestModels/HistoryBefore/src/Index.dfy @@ -0,0 +1,30 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "SimpleStringImpl.dfy" + +module {:extern "simple.types.smithystring.internaldafny" } SimpleString refines AbstractSimpleTypesSmithyStringService { + import Operations = SimpleStringImpl + + function method DefaultSimpleStringConfig(): SimpleStringConfig { + SimpleStringConfig + } + + method SimpleString(config: SimpleStringConfig) + returns (res: Result) { + var client := new SimpleStringClient(Operations.Config); + return Success(client); + } + + class SimpleStringClient... { + predicate ValidState() + { + && Operations.ValidInternalConfig?(config) + && Modifies == Operations.ModifiesInternalConfig(config) + {History} + } + constructor(config: Operations.InternalConfig) { + this.config := config; + History := new ISimpleTypesStringClientCallHistory(); + Modifies := Operations.ModifiesInternalConfig(config) + {History}; + } + } +} diff --git a/TestModels/HistoryBefore/src/SimpleStringImpl.dfy b/TestModels/HistoryBefore/src/SimpleStringImpl.dfy new file mode 100644 index 0000000000..c979c657ec --- /dev/null +++ b/TestModels/HistoryBefore/src/SimpleStringImpl.dfy @@ -0,0 +1,39 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleTypesSmithyStringTypes.dfy" + +module SimpleStringImpl refines AbstractSimpleTypesSmithyStringOperations { + datatype Config = Config + type InternalConfig = Config + predicate ValidInternalConfig?(config: InternalConfig) + {true} + function ModifiesInternalConfig(config: InternalConfig) : set + {{}} + predicate GetStringEnsuresPublicly(input: GetStringInput, output: Result) { + true + } + predicate GetStringSingleValueEnsuresPublicly(input: GetStringInput, output: Result) { + true + } + predicate GetStringUTF8EnsuresPublicly(input: GetStringInput, output: Result) { + true + } + method GetString ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + var res := GetStringOutput(value := input.value); + return Success(res); + } + method GetStringSingleValue ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + expect input.value.Some?; + expect input.value.value == "TEST_SIMPLE_STRING_SINGLE_VALUE"; // This is done so as to assert that polymorph layer is doing one way conversion right as well. + var res := GetStringOutput(value := input.value); + return Success(res); + } + method GetStringUTF8 ( config: InternalConfig, input: GetStringInput ) + returns (output: Result) { + expect input.value.Some?; + var res := GetStringOutput(value := input.value); + return Success(res); + } +} diff --git a/TestModels/HistoryBefore/src/WrappedSimpleStringImpl.dfy b/TestModels/HistoryBefore/src/WrappedSimpleStringImpl.dfy new file mode 100644 index 0000000000..1c706a71b8 --- /dev/null +++ b/TestModels/HistoryBefore/src/WrappedSimpleStringImpl.dfy @@ -0,0 +1,10 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleTypesSmithyStringTypesWrapped.dfy" + +module {:extern "simple.types.smithystring.internaldafny.wrapped"} WrappedSimpleTypesStringService refines WrappedAbstractSimpleTypesSmithyStringService { + import WrappedService = SimpleString + function method WrappedDefaultSimpleStringConfig(): SimpleStringConfig { + SimpleStringConfig + } +} diff --git a/TestModels/HistoryBefore/test/SimpleStringImplTest.dfy b/TestModels/HistoryBefore/test/SimpleStringImplTest.dfy new file mode 100644 index 0000000000..a4e32689dc --- /dev/null +++ b/TestModels/HistoryBefore/test/SimpleStringImplTest.dfy @@ -0,0 +1,73 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/Index.dfy" + +module SimpleStringImplTest { + import SimpleString + import opened SimpleTypesSmithyStringTypes + import opened Wrappers + method{:test} GetString(){ + var client :- expect SimpleString.SimpleString(); + TestSingleCall(client); + } + + method TestSingleCall(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE"))); + + assert |client.History.GetString| == |old(client.History.GetString)| + 1; + assert Last(client.History.GetString).input.value == Some("TEST_SIMPLE_STRING_VALUE"); + assert Last(client.History.GetString).output.value == ret; + } + + method TestMultipleCallsToSameOperation(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE"))); + var ret2 :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE_2"))); + + assert |client.History.GetString| == |old(client.History.GetString)| + 2; + assert Last(client.History.GetString).input.value == Some("TEST_SIMPLE_STRING_VALUE_2"); + assert Last(client.History.GetString).output.value == ret2; + assert Last(DropLast(client.History.GetString)).input.value == Some("TEST_SIMPLE_STRING_VALUE"); + assert Last(DropLast(client.History.GetString)).output.value == ret; + } + + method TestMultipleCallsToDifferentOperations(client: ISimpleTypesStringClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var ret :- expect client.GetString(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE"))); + var ret2 :- expect client.GetStringUTF8(SimpleString.Types.GetStringInput(value:= Some("TEST_SIMPLE_STRING_VALUE_2"))); + + assert |client.History.GetString| == |old(client.History.GetString)| + 1; + assert Last(client.History.GetString).input.value == Some("TEST_SIMPLE_STRING_VALUE"); + assert Last(client.History.GetString).output.value == ret; + + assert |client.History.GetStringUTF8| == |old(client.History.GetStringUTF8)| + 1; + assert Last(client.History.GetStringUTF8).input.value == Some("TEST_SIMPLE_STRING_VALUE_2"); + assert Last(client.History.GetStringUTF8).output.value == ret2; + + // Not possible to express that the call to GetString occurred before the call to GetStringUTF8 + } + + // Normally from Seq.dfy in dafny-lang/libraries: + + function DropLast(s: seq): seq + requires 0 < |s| + { + s[..(|s| - 1)] + } + + function Last(s: seq): T + requires 0 < |s| + { + s[|s| - 1] + } +} diff --git a/TestModels/HistoryBefore/test/WrappedSimpleStringTest.dfy b/TestModels/HistoryBefore/test/WrappedSimpleStringTest.dfy new file mode 100644 index 0000000000..f63fac82e7 --- /dev/null +++ b/TestModels/HistoryBefore/test/WrappedSimpleStringTest.dfy @@ -0,0 +1,16 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/WrappedSimpleStringImpl.dfy" +include "SimpleStringImplTest.dfy" + +module WrappedSimpleTypesStringTest { + import WrappedSimpleTypesStringService + import SimpleStringImplTest + import opened Wrappers + method{:test} GetString() { + var client :- expect WrappedSimpleTypesStringService.WrappedSimpleString(); + SimpleStringImplTest.TestSingleCall(client); + SimpleStringImplTest.TestMultipleCallsToSameOperation(client); + SimpleStringImplTest.TestMultipleCallsToSameOperation(client); + } +} \ No newline at end of file diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/History.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/History.dfy new file mode 100644 index 0000000000..a4f81492fa --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/src/History.dfy @@ -0,0 +1,31 @@ + +module Histories { + trait {:termination false} Event { + } + + class History { + ghost var events: seq + + ghost constructor() + ensures events == [] + { + this.events := []; + } + + ghost method AddEvent(e: Event) + modifies this + ensures events == old(events) + [e] + // ensures forall p: Event -> bool | p(e) :: NewEventSuchThat(p) + { + events := events + [e]; + } + + twostate predicate NewEventSuchThat(p: Event -> bool) + reads this + { + && |events| == |old(events)| + 1 + && events[..(|events| - 1)] == old(events) + && p(events[|events| - 1]) + } + } +} \ No newline at end of file diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy index 1b47b6c9fe..897b60af8f 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy +++ b/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy @@ -3,4 +3,5 @@ include "./StandardLibrary.dfy" include "./UInt.dfy" -include "./UTF8.dfy" \ No newline at end of file +include "./UTF8.dfy" +include "./History.dfy" \ No newline at end of file