From 55055e562f61939ffc1a7e2edb8bcba0860ede72 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 17 Feb 2023 15:59:31 -0800 Subject: [PATCH 1/6] add types for completeness since these are benerated --- .../Model/SimpleDependenciesTypes.dfy | 480 ++++++++++++++++++ 1 file changed, 480 insertions(+) create mode 100644 TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy diff --git a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy new file mode 100644 index 000000000..ac0a788c6 --- /dev/null +++ b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy @@ -0,0 +1,480 @@ +// 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 "../../Constraints/src/Index.dfy" + include "../../Extendable/src/Index.dfy" + include "../../Resource/src/Index.dfy" + module {:extern "Dafny.Simple.Dependencies.Types" } SimpleDependenciesTypes + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import SimpleConstraintsTypes + import SimpleExtendableResourcesTypes + import SimpleResourcesTypes + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + + // Begin Generated Types + + class ISimpleDependenciesClientCallHistory { + ghost constructor() { + GetSimpleResource := []; + UseSimpleResource := []; + UseLocalExtendableResource := []; + LocalExtendableResourceAlwaysError := []; + LocalExtendableResourceAlwaysMultipleErrors := []; + LocalExtendableResourceAlwaysNativeError := []; +} + ghost var GetSimpleResource: seq>> + ghost var UseSimpleResource: seq>> + ghost var UseLocalExtendableResource: seq>> + ghost var LocalExtendableResourceAlwaysError: seq>> + ghost var LocalExtendableResourceAlwaysMultipleErrors: seq>> + ghost var LocalExtendableResourceAlwaysNativeError: seq>> +} + trait {:termination false} ISimpleDependenciesClient + { + // 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: ISimpleDependenciesClientCallHistory + predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + // The public method to be called by library consumers + method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + && ( output.Success? ==> + && output.value.output.ValidState() + && output.value.output.Modifies !! {History} + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - Modifies - {History} ) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + // The public method to be called by library consumers + method UseSimpleResource ( input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidState() + && input.value.ValidState() + && input.value.Modifies !! {History} + modifies Modifies - {History} , + input.value.Modifies , + History`UseSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} , + input.value.Modifies + ensures + && ValidState() + ensures UseSimpleResourceEnsuresPublicly(input, output) + ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + // The public method to be called by library consumers + method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`UseLocalExtendableResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures UseLocalExtendableResourceEnsuresPublicly(input, output) + ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysMultipleErrors + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysNativeError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] + +} + datatype SimpleDependenciesConfig = | SimpleDependenciesConfig ( + nameonly simpleResourcesConfig: Option , + nameonly extendableResourceReference: Option , + nameonly specialString: Option + ) + datatype UseSimpleResourceInput = | UseSimpleResourceInput ( + nameonly value: SimpleResourcesTypes.ISimpleResource , + nameonly input: SimpleResourcesTypes.GetResourceDataInput + ) + datatype Error = + // Local Error structures are listed here + + // Any dependent models are listed here + | SimpleConstraints(SimpleConstraints: SimpleConstraintsTypes.Error) + | SimpleExtendableResources(SimpleExtendableResources: SimpleExtendableResourcesTypes.Error) + | SimpleResources(SimpleResources: SimpleResourcesTypes.Error) + // 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) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + type OpaqueError = e: Error | e.Opaque? witness * +} + abstract module AbstractSimpleDependenciesService + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleDependenciesTypes + import Operations : AbstractSimpleDependenciesOperations + function method DefaultSimpleDependenciesConfig(): SimpleDependenciesConfig + method SimpleDependencies(config: SimpleDependenciesConfig := DefaultSimpleDependenciesConfig()) + returns (res: Result) + requires config.extendableResourceReference.Some? ==> config.extendableResourceReference.value.ValidState() + modifies if config.extendableResourceReference.Some? then config.extendableResourceReference.value.Modifies else {} + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.History) + && fresh(res.value.Modifies - Operations.ModifiesInternalConfig(res.value.config)) + && res.value.ValidState() + ensures !(config.extendableResourceReference.Some?) && res.Success? ==> fresh(Operations.ModifiesInternalConfig(res.value.config)) + class SimpleDependenciesClient extends ISimpleDependenciesClient + { + 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 GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + {Operations.GetSimpleResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History}, + History`GetSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + && ( output.Success? ==> + && output.value.output.ValidState() + && output.value.output.Modifies !! {History} + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - Modifies - {History}) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] + { + output := Operations.GetSimpleResource(config, input); + History.GetSimpleResource := History.GetSimpleResource + [DafnyCallEvent(input, output)]; +} + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + {Operations.UseSimpleResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method UseSimpleResource ( input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidState() + && input.value.ValidState() + && input.value.Modifies !! {History} + modifies Modifies - {History} , + input.value.Modifies , + History`UseSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} , + input.value.Modifies + ensures + && ValidState() + ensures UseSimpleResourceEnsuresPublicly(input, output) + ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] + { + output := Operations.UseSimpleResource(config, input); + History.UseSimpleResource := History.UseSimpleResource + [DafnyCallEvent(input, output)]; +} + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + {Operations.UseLocalExtendableResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`UseLocalExtendableResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures UseLocalExtendableResourceEnsuresPublicly(input, output) + ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] + { + output := Operations.UseLocalExtendableResource(config, input); + History.UseLocalExtendableResource := History.UseLocalExtendableResource + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysError(config, input); + History.LocalExtendableResourceAlwaysError := History.LocalExtendableResourceAlwaysError + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysMultipleErrors + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysMultipleErrors(config, input); + History.LocalExtendableResourceAlwaysMultipleErrors := History.LocalExtendableResourceAlwaysMultipleErrors + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysNativeError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysNativeError(config, input); + History.LocalExtendableResourceAlwaysNativeError := History.LocalExtendableResourceAlwaysNativeError + [DafnyCallEvent(input, output)]; +} + +} +} + abstract module AbstractSimpleDependenciesOperations { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleDependenciesTypes + type InternalConfig + predicate ValidInternalConfig?(config: InternalConfig) + function ModifiesInternalConfig(config: InternalConfig): set + predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + // The private method to be refined by the library developer + + + method GetSimpleResource ( config: InternalConfig , input: SimpleResourcesTypes.GetResourcesInput ) + 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) + && ( output.Success? ==> + && output.value.output.ValidState() + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - ModifiesInternalConfig(config) ) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + // The private method to be refined by the library developer + + + method UseSimpleResource ( config: InternalConfig , input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + && input.value.ValidState() + modifies ModifiesInternalConfig(config) , + input.value.Modifies + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) , + input.value.Modifies + ensures + && ValidInternalConfig?(config) + ensures UseSimpleResourceEnsuresPublicly(input, output) + + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + // The private method to be refined by the library developer + + + method UseLocalExtendableResource ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + 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 UseLocalExtendableResourceEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysMultipleErrors ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysNativeError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) +} From 4beb19c9d104d3ad9f968626dfa73dc4d2fc1056 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 26 Sep 2023 14:51:03 -0700 Subject: [PATCH 2/6] foo --- .../Model/SimpleDependenciesTypes.dfy | 480 ------------------ 1 file changed, 480 deletions(-) delete mode 100644 TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy diff --git a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy deleted file mode 100644 index ac0a788c6..000000000 --- a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy +++ /dev/null @@ -1,480 +0,0 @@ -// 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 "../../Constraints/src/Index.dfy" - include "../../Extendable/src/Index.dfy" - include "../../Resource/src/Index.dfy" - module {:extern "Dafny.Simple.Dependencies.Types" } SimpleDependenciesTypes - { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import SimpleConstraintsTypes - import SimpleExtendableResourcesTypes - import SimpleResourcesTypes - // Generic helpers for verification of mock/unit tests. - datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) - - // Begin Generated Types - - class ISimpleDependenciesClientCallHistory { - ghost constructor() { - GetSimpleResource := []; - UseSimpleResource := []; - UseLocalExtendableResource := []; - LocalExtendableResourceAlwaysError := []; - LocalExtendableResourceAlwaysMultipleErrors := []; - LocalExtendableResourceAlwaysNativeError := []; -} - ghost var GetSimpleResource: seq>> - ghost var UseSimpleResource: seq>> - ghost var UseLocalExtendableResource: seq>> - ghost var LocalExtendableResourceAlwaysError: seq>> - ghost var LocalExtendableResourceAlwaysMultipleErrors: seq>> - ghost var LocalExtendableResourceAlwaysNativeError: seq>> -} - trait {:termination false} ISimpleDependenciesClient - { - // 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: ISimpleDependenciesClientCallHistory - predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - // The public method to be called by library consumers - method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GetSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - && ( output.Success? ==> - && output.value.output.ValidState() - && output.value.output.Modifies !! {History} - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - Modifies - {History} ) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - // The public method to be called by library consumers - method UseSimpleResource ( input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidState() - && input.value.ValidState() - && input.value.Modifies !! {History} - modifies Modifies - {History} , - input.value.Modifies , - History`UseSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} , - input.value.Modifies - ensures - && ValidState() - ensures UseSimpleResourceEnsuresPublicly(input, output) - ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - // The public method to be called by library consumers - method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`UseLocalExtendableResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UseLocalExtendableResourceEnsuresPublicly(input, output) - ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysMultipleErrors - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysNativeError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] - -} - datatype SimpleDependenciesConfig = | SimpleDependenciesConfig ( - nameonly simpleResourcesConfig: Option , - nameonly extendableResourceReference: Option , - nameonly specialString: Option - ) - datatype UseSimpleResourceInput = | UseSimpleResourceInput ( - nameonly value: SimpleResourcesTypes.ISimpleResource , - nameonly input: SimpleResourcesTypes.GetResourceDataInput - ) - datatype Error = - // Local Error structures are listed here - - // Any dependent models are listed here - | SimpleConstraints(SimpleConstraints: SimpleConstraintsTypes.Error) - | SimpleExtendableResources(SimpleExtendableResources: SimpleExtendableResourcesTypes.Error) - | SimpleResources(SimpleResources: SimpleResourcesTypes.Error) - // 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) - // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * -} - abstract module AbstractSimpleDependenciesService - { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = SimpleDependenciesTypes - import Operations : AbstractSimpleDependenciesOperations - function method DefaultSimpleDependenciesConfig(): SimpleDependenciesConfig - method SimpleDependencies(config: SimpleDependenciesConfig := DefaultSimpleDependenciesConfig()) - returns (res: Result) - requires config.extendableResourceReference.Some? ==> config.extendableResourceReference.value.ValidState() - modifies if config.extendableResourceReference.Some? then config.extendableResourceReference.value.Modifies else {} - ensures res.Success? ==> - && fresh(res.value) - && fresh(res.value.History) - && fresh(res.value.Modifies - Operations.ModifiesInternalConfig(res.value.config)) - && res.value.ValidState() - ensures !(config.extendableResourceReference.Some?) && res.Success? ==> fresh(Operations.ModifiesInternalConfig(res.value.config)) - class SimpleDependenciesClient extends ISimpleDependenciesClient - { - 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 GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - {Operations.GetSimpleResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History}, - History`GetSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - && ( output.Success? ==> - && output.value.output.ValidState() - && output.value.output.Modifies !! {History} - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - Modifies - {History}) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] - { - output := Operations.GetSimpleResource(config, input); - History.GetSimpleResource := History.GetSimpleResource + [DafnyCallEvent(input, output)]; -} - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - {Operations.UseSimpleResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method UseSimpleResource ( input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidState() - && input.value.ValidState() - && input.value.Modifies !! {History} - modifies Modifies - {History} , - input.value.Modifies , - History`UseSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} , - input.value.Modifies - ensures - && ValidState() - ensures UseSimpleResourceEnsuresPublicly(input, output) - ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] - { - output := Operations.UseSimpleResource(config, input); - History.UseSimpleResource := History.UseSimpleResource + [DafnyCallEvent(input, output)]; -} - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - {Operations.UseLocalExtendableResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`UseLocalExtendableResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UseLocalExtendableResourceEnsuresPublicly(input, output) - ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] - { - output := Operations.UseLocalExtendableResource(config, input); - History.UseLocalExtendableResource := History.UseLocalExtendableResource + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysError(config, input); - History.LocalExtendableResourceAlwaysError := History.LocalExtendableResourceAlwaysError + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysMultipleErrors - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysMultipleErrors(config, input); - History.LocalExtendableResourceAlwaysMultipleErrors := History.LocalExtendableResourceAlwaysMultipleErrors + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysNativeError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysNativeError(config, input); - History.LocalExtendableResourceAlwaysNativeError := History.LocalExtendableResourceAlwaysNativeError + [DafnyCallEvent(input, output)]; -} - -} -} - abstract module AbstractSimpleDependenciesOperations { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = SimpleDependenciesTypes - type InternalConfig - predicate ValidInternalConfig?(config: InternalConfig) - function ModifiesInternalConfig(config: InternalConfig): set - predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - // The private method to be refined by the library developer - - - method GetSimpleResource ( config: InternalConfig , input: SimpleResourcesTypes.GetResourcesInput ) - 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) - && ( output.Success? ==> - && output.value.output.ValidState() - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - ModifiesInternalConfig(config) ) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - // The private method to be refined by the library developer - - - method UseSimpleResource ( config: InternalConfig , input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidInternalConfig?(config) - && input.value.ValidState() - modifies ModifiesInternalConfig(config) , - input.value.Modifies - // Dafny will skip type parameters when generating a default decreases clause. - decreases ModifiesInternalConfig(config) , - input.value.Modifies - ensures - && ValidInternalConfig?(config) - ensures UseSimpleResourceEnsuresPublicly(input, output) - - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - // The private method to be refined by the library developer - - - method UseLocalExtendableResource ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - 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 UseLocalExtendableResourceEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysMultipleErrors ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysNativeError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) -} From 036c46709dbfebbcff3e2e24e9e0070bfc0138c3 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Mon, 9 Oct 2023 18:05:47 -0400 Subject: [PATCH 3/6] feat: repair generateUnionConverter (#296) --- .../amazon/polymorph/smithydotnet/TypeConversionCodegen.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java index 06a7e2696..2de540f02 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java @@ -579,7 +579,7 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) { destructorValue = DafnyNameResolverHelpers.dafnyCompilesExtra_(memberShape.getMemberName()); } return TokenTree - .of("if (value.is_%s)".formatted(memberShape.getMemberName())) + .of("if (value.is_%s)".formatted(DafnyNameResolverHelpers.dafnyCompilesExtra_(memberShape.getMemberName()))) .append(TokenTree .of( "converted.%s = %s(concrete.dtor_%s);" From 43ab6c49f6cbe7718bfcb59e33921f69cd91b720 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Thu, 12 Oct 2023 12:10:49 -0400 Subject: [PATCH 4/6] feat: repair type deduction for AttributeValue (#299) --- .../amazon/polymorph/smithydotnet/TypeConversionCodegen.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java index 2de540f02..299ff5fda 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java @@ -637,7 +637,7 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) { .of("if (value.Is%sSet)".formatted(propertyName)); } else if (listTypes.contains(propertyName)) { checkIfValuePresent = TokenTree - .of("if (!value.%s.Any())".formatted(propertyName)); + .of("if (value.%s.Any())".formatted(propertyName)); } else if ("NULL".equals(propertyName)) { checkIfValuePresent = TokenTree .of("if (value.%s == true)".formatted(propertyName)); From 0a8d22647a631136f28257f1ebbb2e69a5d5db08 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 17 Feb 2023 15:59:31 -0800 Subject: [PATCH 5/6] add types for completeness since these are benerated --- .../Model/SimpleDependenciesTypes.dfy | 480 ++++++++++++++++++ 1 file changed, 480 insertions(+) create mode 100644 TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy diff --git a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy new file mode 100644 index 000000000..ac0a788c6 --- /dev/null +++ b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy @@ -0,0 +1,480 @@ +// 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 "../../Constraints/src/Index.dfy" + include "../../Extendable/src/Index.dfy" + include "../../Resource/src/Index.dfy" + module {:extern "Dafny.Simple.Dependencies.Types" } SimpleDependenciesTypes + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import SimpleConstraintsTypes + import SimpleExtendableResourcesTypes + import SimpleResourcesTypes + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + + // Begin Generated Types + + class ISimpleDependenciesClientCallHistory { + ghost constructor() { + GetSimpleResource := []; + UseSimpleResource := []; + UseLocalExtendableResource := []; + LocalExtendableResourceAlwaysError := []; + LocalExtendableResourceAlwaysMultipleErrors := []; + LocalExtendableResourceAlwaysNativeError := []; +} + ghost var GetSimpleResource: seq>> + ghost var UseSimpleResource: seq>> + ghost var UseLocalExtendableResource: seq>> + ghost var LocalExtendableResourceAlwaysError: seq>> + ghost var LocalExtendableResourceAlwaysMultipleErrors: seq>> + ghost var LocalExtendableResourceAlwaysNativeError: seq>> +} + trait {:termination false} ISimpleDependenciesClient + { + // 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: ISimpleDependenciesClientCallHistory + predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + // The public method to be called by library consumers + method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`GetSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + && ( output.Success? ==> + && output.value.output.ValidState() + && output.value.output.Modifies !! {History} + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - Modifies - {History} ) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + // The public method to be called by library consumers + method UseSimpleResource ( input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidState() + && input.value.ValidState() + && input.value.Modifies !! {History} + modifies Modifies - {History} , + input.value.Modifies , + History`UseSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} , + input.value.Modifies + ensures + && ValidState() + ensures UseSimpleResourceEnsuresPublicly(input, output) + ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + // The public method to be called by library consumers + method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`UseLocalExtendableResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures UseLocalExtendableResourceEnsuresPublicly(input, output) + ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysMultipleErrors + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysNativeError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] + +} + datatype SimpleDependenciesConfig = | SimpleDependenciesConfig ( + nameonly simpleResourcesConfig: Option , + nameonly extendableResourceReference: Option , + nameonly specialString: Option + ) + datatype UseSimpleResourceInput = | UseSimpleResourceInput ( + nameonly value: SimpleResourcesTypes.ISimpleResource , + nameonly input: SimpleResourcesTypes.GetResourceDataInput + ) + datatype Error = + // Local Error structures are listed here + + // Any dependent models are listed here + | SimpleConstraints(SimpleConstraints: SimpleConstraintsTypes.Error) + | SimpleExtendableResources(SimpleExtendableResources: SimpleExtendableResourcesTypes.Error) + | SimpleResources(SimpleResources: SimpleResourcesTypes.Error) + // 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) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + type OpaqueError = e: Error | e.Opaque? witness * +} + abstract module AbstractSimpleDependenciesService + { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleDependenciesTypes + import Operations : AbstractSimpleDependenciesOperations + function method DefaultSimpleDependenciesConfig(): SimpleDependenciesConfig + method SimpleDependencies(config: SimpleDependenciesConfig := DefaultSimpleDependenciesConfig()) + returns (res: Result) + requires config.extendableResourceReference.Some? ==> config.extendableResourceReference.value.ValidState() + modifies if config.extendableResourceReference.Some? then config.extendableResourceReference.value.Modifies else {} + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.History) + && fresh(res.value.Modifies - Operations.ModifiesInternalConfig(res.value.config)) + && res.value.ValidState() + ensures !(config.extendableResourceReference.Some?) && res.Success? ==> fresh(Operations.ModifiesInternalConfig(res.value.config)) + class SimpleDependenciesClient extends ISimpleDependenciesClient + { + 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 GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + {Operations.GetSimpleResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History}, + History`GetSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + && ( output.Success? ==> + && output.value.output.ValidState() + && output.value.output.Modifies !! {History} + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - Modifies - {History}) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] + { + output := Operations.GetSimpleResource(config, input); + History.GetSimpleResource := History.GetSimpleResource + [DafnyCallEvent(input, output)]; +} + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + {Operations.UseSimpleResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method UseSimpleResource ( input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidState() + && input.value.ValidState() + && input.value.Modifies !! {History} + modifies Modifies - {History} , + input.value.Modifies , + History`UseSimpleResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} , + input.value.Modifies + ensures + && ValidState() + ensures UseSimpleResourceEnsuresPublicly(input, output) + ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] + { + output := Operations.UseSimpleResource(config, input); + History.UseSimpleResource := History.UseSimpleResource + [DafnyCallEvent(input, output)]; +} + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + {Operations.UseLocalExtendableResourceEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`UseLocalExtendableResource + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures UseLocalExtendableResourceEnsuresPublicly(input, output) + ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] + { + output := Operations.UseLocalExtendableResource(config, input); + History.UseLocalExtendableResource := History.UseLocalExtendableResource + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysError(config, input); + History.LocalExtendableResourceAlwaysError := History.LocalExtendableResourceAlwaysError + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysMultipleErrors + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysMultipleErrors(config, input); + History.LocalExtendableResourceAlwaysMultipleErrors := History.LocalExtendableResourceAlwaysMultipleErrors + [DafnyCallEvent(input, output)]; +} + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + {Operations.LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`LocalExtendableResourceAlwaysNativeError + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) + ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] + { + output := Operations.LocalExtendableResourceAlwaysNativeError(config, input); + History.LocalExtendableResourceAlwaysNativeError := History.LocalExtendableResourceAlwaysNativeError + [DafnyCallEvent(input, output)]; +} + +} +} + abstract module AbstractSimpleDependenciesOperations { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Types = SimpleDependenciesTypes + type InternalConfig + predicate ValidInternalConfig?(config: InternalConfig) + function ModifiesInternalConfig(config: InternalConfig): set + predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) + // The private method to be refined by the library developer + + + method GetSimpleResource ( config: InternalConfig , input: SimpleResourcesTypes.GetResourcesInput ) + 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) + && ( output.Success? ==> + && output.value.output.ValidState() + && fresh(output.value.output) + && fresh ( output.value.output.Modifies - ModifiesInternalConfig(config) ) ) + ensures GetSimpleResourceEnsuresPublicly(input, output) + + + predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) + // The private method to be refined by the library developer + + + method UseSimpleResource ( config: InternalConfig , input: UseSimpleResourceInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + && input.value.ValidState() + modifies ModifiesInternalConfig(config) , + input.value.Modifies + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) , + input.value.Modifies + ensures + && ValidInternalConfig?(config) + ensures UseSimpleResourceEnsuresPublicly(input, output) + + + predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) + // The private method to be refined by the library developer + + + method UseLocalExtendableResource ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) + 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 UseLocalExtendableResourceEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysMultipleErrors ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) + + + predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) + // The private method to be refined by the library developer + + + method LocalExtendableResourceAlwaysNativeError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) + 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 LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) +} From 6a0312a07795aa11c8a768cb1aa970249797f3aa Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 26 Sep 2023 14:51:03 -0700 Subject: [PATCH 6/6] foo --- .../Model/SimpleDependenciesTypes.dfy | 480 ------------------ 1 file changed, 480 deletions(-) delete mode 100644 TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy diff --git a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy b/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy deleted file mode 100644 index ac0a788c6..000000000 --- a/TestModels/Dependencies/Model/SimpleDependenciesTypes.dfy +++ /dev/null @@ -1,480 +0,0 @@ -// 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 "../../Constraints/src/Index.dfy" - include "../../Extendable/src/Index.dfy" - include "../../Resource/src/Index.dfy" - module {:extern "Dafny.Simple.Dependencies.Types" } SimpleDependenciesTypes - { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import SimpleConstraintsTypes - import SimpleExtendableResourcesTypes - import SimpleResourcesTypes - // Generic helpers for verification of mock/unit tests. - datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) - - // Begin Generated Types - - class ISimpleDependenciesClientCallHistory { - ghost constructor() { - GetSimpleResource := []; - UseSimpleResource := []; - UseLocalExtendableResource := []; - LocalExtendableResourceAlwaysError := []; - LocalExtendableResourceAlwaysMultipleErrors := []; - LocalExtendableResourceAlwaysNativeError := []; -} - ghost var GetSimpleResource: seq>> - ghost var UseSimpleResource: seq>> - ghost var UseLocalExtendableResource: seq>> - ghost var LocalExtendableResourceAlwaysError: seq>> - ghost var LocalExtendableResourceAlwaysMultipleErrors: seq>> - ghost var LocalExtendableResourceAlwaysNativeError: seq>> -} - trait {:termination false} ISimpleDependenciesClient - { - // 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: ISimpleDependenciesClientCallHistory - predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - // The public method to be called by library consumers - method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GetSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - && ( output.Success? ==> - && output.value.output.ValidState() - && output.value.output.Modifies !! {History} - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - Modifies - {History} ) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - // The public method to be called by library consumers - method UseSimpleResource ( input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidState() - && input.value.ValidState() - && input.value.Modifies !! {History} - modifies Modifies - {History} , - input.value.Modifies , - History`UseSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} , - input.value.Modifies - ensures - && ValidState() - ensures UseSimpleResourceEnsuresPublicly(input, output) - ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - // The public method to be called by library consumers - method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`UseLocalExtendableResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UseLocalExtendableResourceEnsuresPublicly(input, output) - ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysMultipleErrors - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysNativeError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] - -} - datatype SimpleDependenciesConfig = | SimpleDependenciesConfig ( - nameonly simpleResourcesConfig: Option , - nameonly extendableResourceReference: Option , - nameonly specialString: Option - ) - datatype UseSimpleResourceInput = | UseSimpleResourceInput ( - nameonly value: SimpleResourcesTypes.ISimpleResource , - nameonly input: SimpleResourcesTypes.GetResourceDataInput - ) - datatype Error = - // Local Error structures are listed here - - // Any dependent models are listed here - | SimpleConstraints(SimpleConstraints: SimpleConstraintsTypes.Error) - | SimpleExtendableResources(SimpleExtendableResources: SimpleExtendableResourcesTypes.Error) - | SimpleResources(SimpleResources: SimpleResourcesTypes.Error) - // 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) - // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * -} - abstract module AbstractSimpleDependenciesService - { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = SimpleDependenciesTypes - import Operations : AbstractSimpleDependenciesOperations - function method DefaultSimpleDependenciesConfig(): SimpleDependenciesConfig - method SimpleDependencies(config: SimpleDependenciesConfig := DefaultSimpleDependenciesConfig()) - returns (res: Result) - requires config.extendableResourceReference.Some? ==> config.extendableResourceReference.value.ValidState() - modifies if config.extendableResourceReference.Some? then config.extendableResourceReference.value.Modifies else {} - ensures res.Success? ==> - && fresh(res.value) - && fresh(res.value.History) - && fresh(res.value.Modifies - Operations.ModifiesInternalConfig(res.value.config)) - && res.value.ValidState() - ensures !(config.extendableResourceReference.Some?) && res.Success? ==> fresh(Operations.ModifiesInternalConfig(res.value.config)) - class SimpleDependenciesClient extends ISimpleDependenciesClient - { - 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 GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - {Operations.GetSimpleResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method GetSimpleResource ( input: SimpleResourcesTypes.GetResourcesInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History}, - History`GetSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - && ( output.Success? ==> - && output.value.output.ValidState() - && output.value.output.Modifies !! {History} - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - Modifies - {History}) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - ensures History.GetSimpleResource == old(History.GetSimpleResource) + [DafnyCallEvent(input, output)] - { - output := Operations.GetSimpleResource(config, input); - History.GetSimpleResource := History.GetSimpleResource + [DafnyCallEvent(input, output)]; -} - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - {Operations.UseSimpleResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method UseSimpleResource ( input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidState() - && input.value.ValidState() - && input.value.Modifies !! {History} - modifies Modifies - {History} , - input.value.Modifies , - History`UseSimpleResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} , - input.value.Modifies - ensures - && ValidState() - ensures UseSimpleResourceEnsuresPublicly(input, output) - ensures History.UseSimpleResource == old(History.UseSimpleResource) + [DafnyCallEvent(input, output)] - { - output := Operations.UseSimpleResource(config, input); - History.UseSimpleResource := History.UseSimpleResource + [DafnyCallEvent(input, output)]; -} - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - {Operations.UseLocalExtendableResourceEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method UseLocalExtendableResource ( input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`UseLocalExtendableResource - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UseLocalExtendableResourceEnsuresPublicly(input, output) - ensures History.UseLocalExtendableResource == old(History.UseLocalExtendableResource) + [DafnyCallEvent(input, output)] - { - output := Operations.UseLocalExtendableResource(config, input); - History.UseLocalExtendableResource := History.UseLocalExtendableResource + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysError == old(History.LocalExtendableResourceAlwaysError) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysError(config, input); - History.LocalExtendableResourceAlwaysError := History.LocalExtendableResourceAlwaysError + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysMultipleErrors ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysMultipleErrors - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysMultipleErrors == old(History.LocalExtendableResourceAlwaysMultipleErrors) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysMultipleErrors(config, input); - History.LocalExtendableResourceAlwaysMultipleErrors := History.LocalExtendableResourceAlwaysMultipleErrors + [DafnyCallEvent(input, output)]; -} - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - {Operations.LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output)} - // The public method to be called by library consumers - method LocalExtendableResourceAlwaysNativeError ( input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`LocalExtendableResourceAlwaysNativeError - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) - ensures History.LocalExtendableResourceAlwaysNativeError == old(History.LocalExtendableResourceAlwaysNativeError) + [DafnyCallEvent(input, output)] - { - output := Operations.LocalExtendableResourceAlwaysNativeError(config, input); - History.LocalExtendableResourceAlwaysNativeError := History.LocalExtendableResourceAlwaysNativeError + [DafnyCallEvent(input, output)]; -} - -} -} - abstract module AbstractSimpleDependenciesOperations { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = SimpleDependenciesTypes - type InternalConfig - predicate ValidInternalConfig?(config: InternalConfig) - function ModifiesInternalConfig(config: InternalConfig): set - predicate GetSimpleResourceEnsuresPublicly(input: SimpleResourcesTypes.GetResourcesInput , output: Result) - // The private method to be refined by the library developer - - - method GetSimpleResource ( config: InternalConfig , input: SimpleResourcesTypes.GetResourcesInput ) - 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) - && ( output.Success? ==> - && output.value.output.ValidState() - && fresh(output.value.output) - && fresh ( output.value.output.Modifies - ModifiesInternalConfig(config) ) ) - ensures GetSimpleResourceEnsuresPublicly(input, output) - - - predicate UseSimpleResourceEnsuresPublicly(input: UseSimpleResourceInput , output: Result) - // The private method to be refined by the library developer - - - method UseSimpleResource ( config: InternalConfig , input: UseSimpleResourceInput ) - returns (output: Result) - requires - && ValidInternalConfig?(config) - && input.value.ValidState() - modifies ModifiesInternalConfig(config) , - input.value.Modifies - // Dafny will skip type parameters when generating a default decreases clause. - decreases ModifiesInternalConfig(config) , - input.value.Modifies - ensures - && ValidInternalConfig?(config) - ensures UseSimpleResourceEnsuresPublicly(input, output) - - - predicate UseLocalExtendableResourceEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput , output: Result) - // The private method to be refined by the library developer - - - method UseLocalExtendableResource ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceDataInput ) - 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 UseLocalExtendableResourceEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysErrorEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysMultipleErrors ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysMultipleErrorsEnsuresPublicly(input, output) - - - predicate LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput , output: Result) - // The private method to be refined by the library developer - - - method LocalExtendableResourceAlwaysNativeError ( config: InternalConfig , input: SimpleExtendableResourcesTypes.GetExtendableResourceErrorsInput ) - 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 LocalExtendableResourceAlwaysNativeErrorEnsuresPublicly(input, output) -}