From 1a12801a966f8eca3ac97882c5225e33756140c6 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 25 Oct 2024 09:45:30 -0700 Subject: [PATCH] Delete generated files --- .../model/ComAmazonawsDynamodbTypes.dfy | 1396 ----------------- .../kms-lite/model/ComAmazonawsKmsTypes.dfy | 601 ------- 2 files changed, 1997 deletions(-) delete mode 100644 TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy delete mode 100644 TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy diff --git a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy b/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy deleted file mode 100644 index 83895afa3..000000000 --- a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy +++ /dev/null @@ -1,1396 +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" -module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.types" } ComAmazonawsDynamodbTypes -{ - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - // Generic helpers for verification of mock/unit tests. - datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) - - // Begin Generated Types - - type ArchivalReason = string - datatype ArchivalSummary = | ArchivalSummary ( - nameonly ArchivalDateTime: Option := Option.None , - nameonly ArchivalReason: Option := Option.None , - nameonly ArchivalBackupArn: Option := Option.None - ) - datatype AttributeAction = - | ADD - | PUT - | DELETE - datatype AttributeDefinition = | AttributeDefinition ( - nameonly AttributeName: KeySchemaAttributeName , - nameonly AttributeType: ScalarAttributeType - ) - type AttributeDefinitions = seq - type AttributeMap = map - type AttributeName = x: string | IsValid_AttributeName(x) witness * - predicate method IsValid_AttributeName(x: string) { - ( 0 <= |x| <= 65535 ) - } - type AttributeNameList = x: seq | IsValid_AttributeNameList(x) witness * - predicate method IsValid_AttributeNameList(x: seq) { - ( 1 <= |x| ) - } - type AttributeUpdates = map - datatype AttributeValue = - | S(S: StringAttributeValue) - | N(N: NumberAttributeValue) - | B(B: BinaryAttributeValue) - | SS(SS: StringSetAttributeValue) - | NS(NS: NumberSetAttributeValue) - | BS(BS: BinarySetAttributeValue) - | M(M: MapAttributeValue) - | L(L: ListAttributeValue) - | NULL(NULL: NullAttributeValue) - | BOOL(BOOL: BooleanAttributeValue) - type AttributeValueList = seq - datatype AttributeValueUpdate = | AttributeValueUpdate ( - nameonly Value: Option := Option.None , - nameonly Action: Option := Option.None - ) - type Backfilling = bool - type BackupArn = x: string | IsValid_BackupArn(x) witness * - predicate method IsValid_BackupArn(x: string) { - ( 37 <= |x| <= 1024 ) - } - datatype BatchExecuteStatementInput = | BatchExecuteStatementInput ( - nameonly Statements: PartiQLBatchRequest , - nameonly ReturnConsumedCapacity: Option := Option.None - ) - datatype BatchExecuteStatementOutput = | BatchExecuteStatementOutput ( - nameonly Responses: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - datatype BatchGetItemInput = | BatchGetItemInput ( - nameonly RequestItems: BatchGetRequestMap , - nameonly ReturnConsumedCapacity: Option := Option.None - ) - datatype BatchGetItemOutput = | BatchGetItemOutput ( - nameonly Responses: Option := Option.None , - nameonly UnprocessedKeys: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - type BatchGetRequestMap = x: map | IsValid_BatchGetRequestMap(x) witness * - predicate method IsValid_BatchGetRequestMap(x: map) { - ( 1 <= |x| <= 100 ) - } - type BatchGetResponseMap = map - datatype BatchStatementError = | BatchStatementError ( - nameonly Code: Option := Option.None , - nameonly Message: Option := Option.None - ) - datatype BatchStatementErrorCodeEnum = - | ConditionalCheckFailed - | ItemCollectionSizeLimitExceeded - | RequestLimitExceeded - | ValidationError - | ProvisionedThroughputExceeded - | TransactionConflict - | ThrottlingError - | InternalServerError - | ResourceNotFound - | AccessDenied - | DuplicateItem - datatype BatchStatementRequest = | BatchStatementRequest ( - nameonly Statement: PartiQLStatement , - nameonly Parameters: Option := Option.None , - nameonly ConsistentRead: Option := Option.None - ) - datatype BatchStatementResponse = | BatchStatementResponse ( - nameonly Error: Option := Option.None , - nameonly TableName: Option := Option.None , - nameonly Item: Option := Option.None - ) - datatype BatchWriteItemInput = | BatchWriteItemInput ( - nameonly RequestItems: BatchWriteItemRequestMap , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ReturnItemCollectionMetrics: Option := Option.None - ) - datatype BatchWriteItemOutput = | BatchWriteItemOutput ( - nameonly UnprocessedItems: Option := Option.None , - nameonly ItemCollectionMetrics: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - type BatchWriteItemRequestMap = x: map | IsValid_BatchWriteItemRequestMap(x) witness * - predicate method IsValid_BatchWriteItemRequestMap(x: map) { - ( 1 <= |x| <= 25 ) - } - datatype BillingMode = - | PROVISIONED - | PAY_PER_REQUEST - datatype BillingModeSummary = | BillingModeSummary ( - nameonly BillingMode: Option := Option.None , - nameonly LastUpdateToPayPerRequestDateTime: Option := Option.None - ) - type BinaryAttributeValue = seq - type BinarySetAttributeValue = seq - type BooleanAttributeValue = bool - type BooleanObject = bool - datatype CancellationReason = | CancellationReason ( - nameonly Item: Option := Option.None , - nameonly Code: Option := Option.None , - nameonly Message: Option := Option.None - ) - type CancellationReasonList = x: seq | IsValid_CancellationReasonList(x) witness * - predicate method IsValid_CancellationReasonList(x: seq) { - ( 1 <= |x| <= 25 ) - } - datatype Capacity = | Capacity ( - nameonly ReadCapacityUnits: Option := Option.None , - nameonly WriteCapacityUnits: Option := Option.None , - nameonly CapacityUnits: Option := Option.None - ) - type ClientRequestToken = x: string | IsValid_ClientRequestToken(x) witness * - predicate method IsValid_ClientRequestToken(x: string) { - ( 1 <= |x| <= 36 ) - } - type Code = string - datatype ComparisonOperator = - | EQ - | NE - | IN - | LE - | LT - | GE - | GT - | BETWEEN - | NOT_NULL - | NULL - | CONTAINS - | NOT_CONTAINS - | BEGINS_WITH - datatype Condition = | Condition ( - nameonly AttributeValueList: Option := Option.None , - nameonly ComparisonOperator: ComparisonOperator - ) - datatype ConditionalOperator = - | AND - | OR - datatype ConditionCheck = | ConditionCheck ( - nameonly Key: Key , - nameonly TableName: TableName , - nameonly ConditionExpression: ConditionExpression , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None , - nameonly ReturnValuesOnConditionCheckFailure: Option := Option.None - ) - type ConditionExpression = string - type ConsistentRead = bool - datatype ConsumedCapacity = | ConsumedCapacity ( - nameonly TableName: Option := Option.None , - nameonly CapacityUnits: Option := Option.None , - nameonly ReadCapacityUnits: Option := Option.None , - nameonly WriteCapacityUnits: Option := Option.None , - nameonly Table: Option := Option.None , - nameonly LocalSecondaryIndexes: Option := Option.None , - nameonly GlobalSecondaryIndexes: Option := Option.None - ) - type ConsumedCapacityMultiple = seq - type ConsumedCapacityUnits = x: seq | IsValid_ConsumedCapacityUnits(x) witness * - predicate method IsValid_ConsumedCapacityUnits(x: seq) { - ( 8 <= |x| <= 8 ) - } - datatype CreateTableInput = | CreateTableInput ( - nameonly AttributeDefinitions: AttributeDefinitions , - nameonly TableName: TableName , - nameonly KeySchema: KeySchema , - nameonly LocalSecondaryIndexes: Option := Option.None , - nameonly GlobalSecondaryIndexes: Option := Option.None , - nameonly BillingMode: Option := Option.None , - nameonly ProvisionedThroughput: Option := Option.None , - nameonly StreamSpecification: Option := Option.None , - nameonly SSESpecification: Option := Option.None , - nameonly Tags: Option := Option.None , - nameonly TableClass: Option := Option.None - ) - datatype CreateTableOutput = | CreateTableOutput ( - nameonly TableDescription: Option := Option.None - ) - datatype Delete = | Delete ( - nameonly Key: Key , - nameonly TableName: TableName , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None , - nameonly ReturnValuesOnConditionCheckFailure: Option := Option.None - ) - datatype DeleteItemInput = | DeleteItemInput ( - nameonly TableName: TableName , - nameonly Key: Key , - nameonly Expected: Option := Option.None , - nameonly ConditionalOperator: Option := Option.None , - nameonly ReturnValues: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ReturnItemCollectionMetrics: Option := Option.None , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None - ) - datatype DeleteItemOutput = | DeleteItemOutput ( - nameonly Attributes: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None , - nameonly ItemCollectionMetrics: Option := Option.None - ) - datatype DeleteRequest = | DeleteRequest ( - nameonly Key: Key - ) - datatype DescribeTableInput = | DescribeTableInput ( - nameonly TableName: TableName - ) - datatype DescribeTableOutput = | DescribeTableOutput ( - nameonly Table: Option := Option.None - ) - class IDynamoDBClientCallHistory { - ghost constructor() { - BatchExecuteStatement := []; - BatchGetItem := []; - BatchWriteItem := []; - CreateTable := []; - DeleteItem := []; - DescribeTable := []; - ExecuteStatement := []; - ExecuteTransaction := []; - GetItem := []; - PutItem := []; - Query := []; - Scan := []; - TransactGetItems := []; - TransactWriteItems := []; - UpdateItem := []; - } - ghost var BatchExecuteStatement: seq>> - ghost var BatchGetItem: seq>> - ghost var BatchWriteItem: seq>> - ghost var CreateTable: seq>> - ghost var DeleteItem: seq>> - ghost var DescribeTable: seq>> - ghost var ExecuteStatement: seq>> - ghost var ExecuteTransaction: seq>> - ghost var GetItem: seq>> - ghost var PutItem: seq>> - ghost var Query: seq>> - ghost var Scan: seq>> - ghost var TransactGetItems: seq>> - ghost var TransactWriteItems: seq>> - ghost var UpdateItem: seq>> - } - trait {:termination false} IDynamoDBClient - { - // 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: IDynamoDBClientCallHistory - predicate BatchExecuteStatementEnsuresPublicly(input: BatchExecuteStatementInput , output: Result) - // The public method to be called by library consumers - method BatchExecuteStatement ( input: BatchExecuteStatementInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`BatchExecuteStatement - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures BatchExecuteStatementEnsuresPublicly(input, output) - ensures History.BatchExecuteStatement == old(History.BatchExecuteStatement) + [DafnyCallEvent(input, output)] - - predicate BatchGetItemEnsuresPublicly(input: BatchGetItemInput , output: Result) - // The public method to be called by library consumers - method BatchGetItem ( input: BatchGetItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`BatchGetItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures BatchGetItemEnsuresPublicly(input, output) - ensures History.BatchGetItem == old(History.BatchGetItem) + [DafnyCallEvent(input, output)] - - predicate BatchWriteItemEnsuresPublicly(input: BatchWriteItemInput , output: Result) - // The public method to be called by library consumers - method BatchWriteItem ( input: BatchWriteItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`BatchWriteItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures BatchWriteItemEnsuresPublicly(input, output) - ensures History.BatchWriteItem == old(History.BatchWriteItem) + [DafnyCallEvent(input, output)] - - predicate CreateTableEnsuresPublicly(input: CreateTableInput , output: Result) - // The public method to be called by library consumers - method CreateTable ( input: CreateTableInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`CreateTable - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures CreateTableEnsuresPublicly(input, output) - ensures History.CreateTable == old(History.CreateTable) + [DafnyCallEvent(input, output)] - - predicate DeleteItemEnsuresPublicly(input: DeleteItemInput , output: Result) - // The public method to be called by library consumers - method DeleteItem ( input: DeleteItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`DeleteItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures DeleteItemEnsuresPublicly(input, output) - ensures History.DeleteItem == old(History.DeleteItem) + [DafnyCallEvent(input, output)] - - predicate DescribeTableEnsuresPublicly(input: DescribeTableInput , output: Result) - // The public method to be called by library consumers - method DescribeTable ( input: DescribeTableInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`DescribeTable - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures DescribeTableEnsuresPublicly(input, output) - ensures History.DescribeTable == old(History.DescribeTable) + [DafnyCallEvent(input, output)] - - predicate ExecuteStatementEnsuresPublicly(input: ExecuteStatementInput , output: Result) - // The public method to be called by library consumers - method ExecuteStatement ( input: ExecuteStatementInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`ExecuteStatement - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures ExecuteStatementEnsuresPublicly(input, output) - ensures History.ExecuteStatement == old(History.ExecuteStatement) + [DafnyCallEvent(input, output)] - - predicate ExecuteTransactionEnsuresPublicly(input: ExecuteTransactionInput , output: Result) - // The public method to be called by library consumers - method ExecuteTransaction ( input: ExecuteTransactionInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`ExecuteTransaction - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures ExecuteTransactionEnsuresPublicly(input, output) - ensures History.ExecuteTransaction == old(History.ExecuteTransaction) + [DafnyCallEvent(input, output)] - - predicate GetItemEnsuresPublicly(input: GetItemInput , output: Result) - // The public method to be called by library consumers - method GetItem ( input: GetItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GetItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures GetItemEnsuresPublicly(input, output) - ensures History.GetItem == old(History.GetItem) + [DafnyCallEvent(input, output)] - - predicate PutItemEnsuresPublicly(input: PutItemInput , output: Result) - // The public method to be called by library consumers - method PutItem ( input: PutItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`PutItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures PutItemEnsuresPublicly(input, output) - ensures History.PutItem == old(History.PutItem) + [DafnyCallEvent(input, output)] - - predicate QueryEnsuresPublicly(input: QueryInput , output: Result) - // The public method to be called by library consumers - method Query ( input: QueryInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`Query - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures QueryEnsuresPublicly(input, output) - ensures History.Query == old(History.Query) + [DafnyCallEvent(input, output)] - - predicate ScanEnsuresPublicly(input: ScanInput , output: Result) - // The public method to be called by library consumers - method Scan ( input: ScanInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`Scan - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures ScanEnsuresPublicly(input, output) - ensures History.Scan == old(History.Scan) + [DafnyCallEvent(input, output)] - - predicate TransactGetItemsEnsuresPublicly(input: TransactGetItemsInput , output: Result) - // The public method to be called by library consumers - method TransactGetItems ( input: TransactGetItemsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`TransactGetItems - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures TransactGetItemsEnsuresPublicly(input, output) - ensures History.TransactGetItems == old(History.TransactGetItems) + [DafnyCallEvent(input, output)] - - predicate TransactWriteItemsEnsuresPublicly(input: TransactWriteItemsInput , output: Result) - // The public method to be called by library consumers - method TransactWriteItems ( input: TransactWriteItemsInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`TransactWriteItems - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures TransactWriteItemsEnsuresPublicly(input, output) - ensures History.TransactWriteItems == old(History.TransactWriteItems) + [DafnyCallEvent(input, output)] - - predicate UpdateItemEnsuresPublicly(input: UpdateItemInput , output: Result) - // The public method to be called by library consumers - method UpdateItem ( input: UpdateItemInput ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`UpdateItem - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UpdateItemEnsuresPublicly(input, output) - ensures History.UpdateItem == old(History.UpdateItem) + [DafnyCallEvent(input, output)] - - } - type ErrorMessage = string - datatype ExecuteStatementInput = | ExecuteStatementInput ( - nameonly Statement: PartiQLStatement , - nameonly Parameters: Option := Option.None , - nameonly ConsistentRead: Option := Option.None , - nameonly NextToken: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly Limit: Option := Option.None - ) - datatype ExecuteStatementOutput = | ExecuteStatementOutput ( - nameonly Items: Option := Option.None , - nameonly NextToken: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None , - nameonly LastEvaluatedKey: Option := Option.None - ) - datatype ExecuteTransactionInput = | ExecuteTransactionInput ( - nameonly TransactStatements: ParameterizedStatements , - nameonly ClientRequestToken: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None - ) - datatype ExecuteTransactionOutput = | ExecuteTransactionOutput ( - nameonly Responses: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - type ExpectedAttributeMap = map - datatype ExpectedAttributeValue = | ExpectedAttributeValue ( - nameonly Value: Option := Option.None , - nameonly Exists: Option := Option.None , - nameonly ComparisonOperator: Option := Option.None , - nameonly AttributeValueList: Option := Option.None - ) - type ExpressionAttributeNameMap = map - type ExpressionAttributeNameVariable = string - type ExpressionAttributeValueMap = map - type ExpressionAttributeValueVariable = string - type FilterConditionMap = map - datatype Get = | Get ( - nameonly Key: Key , - nameonly TableName: TableName , - nameonly ProjectionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None - ) - datatype GetItemInput = | GetItemInput ( - nameonly TableName: TableName , - nameonly Key: Key , - nameonly AttributesToGet: Option := Option.None , - nameonly ConsistentRead: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ProjectionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None - ) - datatype GetItemOutput = | GetItemOutput ( - nameonly Item: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - datatype GlobalSecondaryIndex = | GlobalSecondaryIndex ( - nameonly IndexName: IndexName , - nameonly KeySchema: KeySchema , - nameonly Projection: Projection , - nameonly ProvisionedThroughput: Option := Option.None - ) - datatype GlobalSecondaryIndexDescription = | GlobalSecondaryIndexDescription ( - nameonly IndexName: Option := Option.None , - nameonly KeySchema: Option := Option.None , - nameonly Projection: Option := Option.None , - nameonly IndexStatus: Option := Option.None , - nameonly Backfilling: Option := Option.None , - nameonly ProvisionedThroughput: Option := Option.None , - nameonly IndexSizeBytes: Option := Option.None , - nameonly ItemCount: Option := Option.None , - nameonly IndexArn: Option := Option.None - ) - type GlobalSecondaryIndexDescriptionList = seq - type GlobalSecondaryIndexList = seq - type IndexName = x: string | IsValid_IndexName(x) witness * - predicate method IsValid_IndexName(x: string) { - ( 3 <= |x| <= 255 ) - } - datatype IndexStatus = - | CREATING - | UPDATING - | DELETING - | ACTIVE - type Integer = int32 - type ItemCollectionKeyAttributeMap = map - datatype ItemCollectionMetrics = | ItemCollectionMetrics ( - nameonly ItemCollectionKey: Option := Option.None , - nameonly SizeEstimateRangeGB: Option := Option.None - ) - type ItemCollectionMetricsMultiple = seq - type ItemCollectionMetricsPerTable = map - type ItemCollectionSizeEstimateBound = x: seq | IsValid_ItemCollectionSizeEstimateBound(x) witness * - predicate method IsValid_ItemCollectionSizeEstimateBound(x: seq) { - ( 8 <= |x| <= 8 ) - } - type ItemCollectionSizeEstimateRange = seq - type ItemList = seq - datatype ItemResponse = | ItemResponse ( - nameonly Item: Option := Option.None - ) - type ItemResponseList = x: seq | IsValid_ItemResponseList(x) witness * - predicate method IsValid_ItemResponseList(x: seq) { - ( 1 <= |x| <= 25 ) - } - type Key = map - type KeyConditions = map - type KeyExpression = string - type KeyList = x: seq | IsValid_KeyList(x) witness * - predicate method IsValid_KeyList(x: seq) { - ( 1 <= |x| <= 100 ) - } - datatype KeysAndAttributes = | KeysAndAttributes ( - nameonly Keys: KeyList , - nameonly AttributesToGet: Option := Option.None , - nameonly ConsistentRead: Option := Option.None , - nameonly ProjectionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None - ) - type KeySchema = x: seq | IsValid_KeySchema(x) witness * - predicate method IsValid_KeySchema(x: seq) { - ( 1 <= |x| <= 2 ) - } - type KeySchemaAttributeName = x: string | IsValid_KeySchemaAttributeName(x) witness * - predicate method IsValid_KeySchemaAttributeName(x: string) { - ( 1 <= |x| <= 255 ) - } - datatype KeySchemaElement = | KeySchemaElement ( - nameonly AttributeName: KeySchemaAttributeName , - nameonly KeyType: KeyType - ) - datatype KeyType = - | HASH - | RANGE - type KMSMasterKeyArn = string - type KMSMasterKeyId = string - type ListAttributeValue = seq - datatype LocalSecondaryIndex = | LocalSecondaryIndex ( - nameonly IndexName: IndexName , - nameonly KeySchema: KeySchema , - nameonly Projection: Projection - ) - datatype LocalSecondaryIndexDescription = | LocalSecondaryIndexDescription ( - nameonly IndexName: Option := Option.None , - nameonly KeySchema: Option := Option.None , - nameonly Projection: Option := Option.None , - nameonly IndexSizeBytes: Option := Option.None , - nameonly ItemCount: Option := Option.None , - nameonly IndexArn: Option := Option.None - ) - type LocalSecondaryIndexDescriptionList = seq - type LocalSecondaryIndexList = seq - type Long = int64 - type MapAttributeValue = map - type NonKeyAttributeName = x: string | IsValid_NonKeyAttributeName(x) witness * - predicate method IsValid_NonKeyAttributeName(x: string) { - ( 1 <= |x| <= 255 ) - } - type NonKeyAttributeNameList = x: seq | IsValid_NonKeyAttributeNameList(x) witness * - predicate method IsValid_NonKeyAttributeNameList(x: seq) { - ( 1 <= |x| <= 20 ) - } - type NonNegativeLongObject = x: int64 | IsValid_NonNegativeLongObject(x) witness * - predicate method IsValid_NonNegativeLongObject(x: int64) { - ( 0 <= x ) - } - type NullAttributeValue = bool - type NumberAttributeValue = string - type NumberSetAttributeValue = seq - datatype ParameterizedStatement = | ParameterizedStatement ( - nameonly Statement: PartiQLStatement , - nameonly Parameters: Option := Option.None - ) - type ParameterizedStatements = x: seq | IsValid_ParameterizedStatements(x) witness * - predicate method IsValid_ParameterizedStatements(x: seq) { - ( 1 <= |x| <= 25 ) - } - type PartiQLBatchRequest = x: seq | IsValid_PartiQLBatchRequest(x) witness * - predicate method IsValid_PartiQLBatchRequest(x: seq) { - ( 1 <= |x| <= 25 ) - } - type PartiQLBatchResponse = seq - type PartiQLNextToken = x: string | IsValid_PartiQLNextToken(x) witness * - predicate method IsValid_PartiQLNextToken(x: string) { - ( 1 <= |x| <= 32768 ) - } - type PartiQLStatement = x: string | IsValid_PartiQLStatement(x) witness * - predicate method IsValid_PartiQLStatement(x: string) { - ( 1 <= |x| <= 8192 ) - } - type PositiveIntegerObject = x: int32 | IsValid_PositiveIntegerObject(x) witness * - predicate method IsValid_PositiveIntegerObject(x: int32) { - ( 1 <= x ) - } - type PositiveLongObject = x: int64 | IsValid_PositiveLongObject(x) witness * - predicate method IsValid_PositiveLongObject(x: int64) { - ( 1 <= x ) - } - type PreparedStatementParameters = x: seq | IsValid_PreparedStatementParameters(x) witness * - predicate method IsValid_PreparedStatementParameters(x: seq) { - ( 1 <= |x| ) - } - datatype Projection = | Projection ( - nameonly ProjectionType: Option := Option.None , - nameonly NonKeyAttributes: Option := Option.None - ) - type ProjectionExpression = string - datatype ProjectionType = - | ALL - | KEYS_ONLY - | INCLUDE - datatype ProvisionedThroughput = | ProvisionedThroughput ( - nameonly ReadCapacityUnits: PositiveLongObject , - nameonly WriteCapacityUnits: PositiveLongObject - ) - datatype ProvisionedThroughputDescription = | ProvisionedThroughputDescription ( - nameonly LastIncreaseDateTime: Option := Option.None , - nameonly LastDecreaseDateTime: Option := Option.None , - nameonly NumberOfDecreasesToday: Option := Option.None , - nameonly ReadCapacityUnits: Option := Option.None , - nameonly WriteCapacityUnits: Option := Option.None - ) - datatype ProvisionedThroughputOverride = | ProvisionedThroughputOverride ( - nameonly ReadCapacityUnits: Option := Option.None - ) - datatype Put = | Put ( - nameonly Item: PutItemInputAttributeMap , - nameonly TableName: TableName , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None , - nameonly ReturnValuesOnConditionCheckFailure: Option := Option.None - ) - datatype PutItemInput = | PutItemInput ( - nameonly TableName: TableName , - nameonly Item: PutItemInputAttributeMap , - nameonly Expected: Option := Option.None , - nameonly ReturnValues: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ReturnItemCollectionMetrics: Option := Option.None , - nameonly ConditionalOperator: Option := Option.None , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None - ) - type PutItemInputAttributeMap = map - datatype PutItemOutput = | PutItemOutput ( - nameonly Attributes: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None , - nameonly ItemCollectionMetrics: Option := Option.None - ) - datatype PutRequest = | PutRequest ( - nameonly Item: PutItemInputAttributeMap - ) - datatype QueryInput = | QueryInput ( - nameonly TableName: TableName , - nameonly IndexName: Option := Option.None , - nameonly Select: Option := Option.None , - nameonly ScanFilter: Option := Option.None , - nameonly ConditionalOperator: Option := Option.None , - nameonly ExclusiveStartKey: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly TotalSegments: Option := Option.None , - nameonly Segment: Option := Option.None , - nameonly ProjectionExpression: Option := Option.None , - nameonly FilterExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None , - nameonly ConsistentRead: Option := Option.None - ) - datatype ScanOutput = | ScanOutput ( - nameonly Items: Option := Option.None , - nameonly Count: Option := Option.None , - nameonly ScannedCount: Option := Option.None , - nameonly LastEvaluatedKey: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None - ) - type ScanSegment = x: int32 | IsValid_ScanSegment(x) witness * - predicate method IsValid_ScanSegment(x: int32) { - ( 0 <= x <= 999999 ) - } - type ScanTotalSegments = x: int32 | IsValid_ScanTotalSegments(x) witness * - predicate method IsValid_ScanTotalSegments(x: int32) { - ( 1 <= x <= 1000000 ) - } - type SecondaryIndexesCapacityMap = map - datatype Select = - | ALL_ATTRIBUTES - | ALL_PROJECTED_ATTRIBUTES - | SPECIFIC_ATTRIBUTES - | COUNT - datatype SSEDescription = | SSEDescription ( - nameonly Status: Option := Option.None , - nameonly SSEType: Option := Option.None , - nameonly KMSMasterKeyArn: Option := Option.None , - nameonly InaccessibleEncryptionDateTime: Option := Option.None - ) - type SSEEnabled = bool - datatype SSESpecification = | SSESpecification ( - nameonly Enabled: Option := Option.None , - nameonly SSEType: Option := Option.None , - nameonly KMSMasterKeyId: Option := Option.None - ) - datatype SSEStatus = - | ENABLING - | ENABLED - | DISABLING - | DISABLED - | UPDATING - datatype SSEType = - | AES256 - | KMS - type StreamArn = x: string | IsValid_StreamArn(x) witness * - predicate method IsValid_StreamArn(x: string) { - ( 37 <= |x| <= 1024 ) - } - type StreamEnabled = bool - datatype StreamSpecification = | StreamSpecification ( - nameonly StreamEnabled: StreamEnabled , - nameonly StreamViewType: Option := Option.None - ) - datatype StreamViewType = - | NEW_IMAGE - | OLD_IMAGE - | NEW_AND_OLD_IMAGES - | KEYS_ONLY - type String = string - type StringAttributeValue = string - type StringSetAttributeValue = seq - type TableArn = string - datatype TableClass = - | STANDARD - | STANDARD_INFREQUENT_ACCESS - datatype TableClassSummary = | TableClassSummary ( - nameonly TableClass: Option := Option.None , - nameonly LastUpdateDateTime: Option := Option.None - ) - datatype TableDescription = | TableDescription ( - nameonly AttributeDefinitions: Option := Option.None , - nameonly TableName: Option := Option.None , - nameonly KeySchema: Option := Option.None , - nameonly TableStatus: Option := Option.None , - nameonly CreationDateTime: Option := Option.None , - nameonly ProvisionedThroughput: Option := Option.None , - nameonly TableSizeBytes: Option := Option.None , - nameonly ItemCount: Option := Option.None , - nameonly TableArn: Option := Option.None , - nameonly TableId: Option := Option.None , - nameonly BillingModeSummary: Option := Option.None , - nameonly LocalSecondaryIndexes: Option := Option.None , - nameonly GlobalSecondaryIndexes: Option := Option.None , - nameonly StreamSpecification: Option := Option.None , - nameonly LatestStreamLabel: Option := Option.None , - nameonly LatestStreamArn: Option := Option.None , - nameonly GlobalTableVersion: Option := Option.None , - nameonly Replicas: Option := Option.None , - nameonly RestoreSummary: Option := Option.None , - nameonly SSEDescription: Option := Option.None , - nameonly ArchivalSummary: Option := Option.None , - nameonly TableClassSummary: Option := Option.None - ) - type TableId = string - type TableName = x: string | IsValid_TableName(x) witness * - predicate method IsValid_TableName(x: string) { - ( 3 <= |x| <= 255 ) - } - datatype TableStatus = - | CREATING - | UPDATING - | DELETING - | ACTIVE - | INACCESSIBLE_ENCRYPTION_CREDENTIALS - | ARCHIVING - | ARCHIVED - datatype Tag = | Tag ( - nameonly Key: TagKeyString , - nameonly Value: TagValueString - ) - type TagKeyString = x: string | IsValid_TagKeyString(x) witness * - predicate method IsValid_TagKeyString(x: string) { - ( 1 <= |x| <= 128 ) - } - type TagList = seq - type TagValueString = x: string | IsValid_TagValueString(x) witness * - predicate method IsValid_TagValueString(x: string) { - ( 0 <= |x| <= 256 ) - } - datatype TransactGetItem = | TransactGetItem ( - nameonly Get: Get - ) - type TransactGetItemList = x: seq | IsValid_TransactGetItemList(x) witness * - predicate method IsValid_TransactGetItemList(x: seq) { - ( 1 <= |x| <= 25 ) - } - datatype TransactGetItemsInput = | TransactGetItemsInput ( - nameonly TransactItems: TransactGetItemList , - nameonly ReturnConsumedCapacity: Option := Option.None - ) - datatype TransactGetItemsOutput = | TransactGetItemsOutput ( - nameonly ConsumedCapacity: Option := Option.None , - nameonly Responses: Option := Option.None - ) - datatype TransactWriteItem = | TransactWriteItem ( - nameonly ConditionCheck: Option := Option.None , - nameonly Put: Option := Option.None , - nameonly Delete: Option := Option.None , - nameonly Update: Option := Option.None - ) - type TransactWriteItemList = x: seq | IsValid_TransactWriteItemList(x) witness * - predicate method IsValid_TransactWriteItemList(x: seq) { - ( 1 <= |x| <= 25 ) - } - datatype TransactWriteItemsInput = | TransactWriteItemsInput ( - nameonly TransactItems: TransactWriteItemList , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ReturnItemCollectionMetrics: Option := Option.None , - nameonly ClientRequestToken: Option := Option.None - ) - datatype TransactWriteItemsOutput = | TransactWriteItemsOutput ( - nameonly ConsumedCapacity: Option := Option.None , - nameonly ItemCollectionMetrics: Option := Option.None - ) - datatype Update = | Update ( - nameonly Key: Key , - nameonly UpdateExpression: UpdateExpression , - nameonly TableName: TableName , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None , - nameonly ReturnValuesOnConditionCheckFailure: Option := Option.None - ) - type UpdateExpression = string - datatype UpdateItemInput = | UpdateItemInput ( - nameonly TableName: TableName , - nameonly Key: Key , - nameonly AttributeUpdates: Option := Option.None , - nameonly Expected: Option := Option.None , - nameonly ConditionalOperator: Option := Option.None , - nameonly ReturnValues: Option := Option.None , - nameonly ReturnConsumedCapacity: Option := Option.None , - nameonly ReturnItemCollectionMetrics: Option := Option.None , - nameonly UpdateExpression: Option := Option.None , - nameonly ConditionExpression: Option := Option.None , - nameonly ExpressionAttributeNames: Option := Option.None , - nameonly ExpressionAttributeValues: Option := Option.None - ) - datatype UpdateItemOutput = | UpdateItemOutput ( - nameonly Attributes: Option := Option.None , - nameonly ConsumedCapacity: Option := Option.None , - nameonly ItemCollectionMetrics: Option := Option.None - ) - datatype WriteRequest = | WriteRequest ( - nameonly PutRequest: Option := Option.None , - nameonly DeleteRequest: Option := Option.None - ) - type WriteRequests = x: seq | IsValid_WriteRequests(x) witness * - predicate method IsValid_WriteRequests(x: seq) { - ( 1 <= |x| <= 25 ) - } - datatype Error = - // Local Error structures are listed here - | ConditionalCheckFailedException ( - nameonly message: Option := Option.None - ) - | DuplicateItemException ( - nameonly message: Option := Option.None - ) - | IdempotentParameterMismatchException ( - nameonly Message: Option := Option.None - ) - | InternalServerError ( - nameonly message: Option := Option.None - ) - | InvalidEndpointException ( - nameonly Message: Option := Option.None - ) - | ItemCollectionSizeLimitExceededException ( - nameonly message: Option := Option.None - ) - | LimitExceededException ( - nameonly message: Option := Option.None - ) - | ProvisionedThroughputExceededException ( - nameonly message: Option := Option.None - ) - | RequestLimitExceeded ( - nameonly message: Option := Option.None - ) - | ResourceInUseException ( - nameonly message: Option := Option.None - ) - | ResourceNotFoundException ( - nameonly message: Option := Option.None - ) - | TransactionCanceledException ( - nameonly Message: Option := Option.None , - nameonly CancellationReasons: Option := Option.None - ) - | TransactionConflictException ( - nameonly message: Option := Option.None - ) - | TransactionInProgressException ( - nameonly Message: Option := Option.None - ) - // Any dependent models are listed here - - - // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) - type OpaqueError = e: Error | e.Opaque? witness * -} -abstract module AbstractComAmazonawsDynamodbService { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = ComAmazonawsDynamodbTypes - datatype DynamoDBClientConfigType = DynamoDBClientConfigType - function method DefaultDynamoDBClientConfigType(): DynamoDBClientConfigType - method {:extern} DynamoDBClient() - returns (res: Result) - ensures res.Success? ==> - && fresh(res.value) - && fresh(res.value.Modifies) - && fresh(res.value.History) - && res.value.ValidState() - // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IDynamoDBClient): Result { - Success(client) - } - function method CreateFailureOfError(error: Error): Result { - Failure(error) - } -} -abstract module AbstractComAmazonawsDynamodbOperations { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = ComAmazonawsDynamodbTypes - type InternalConfig - predicate ValidInternalConfig?(config: InternalConfig) - function ModifiesInternalConfig(config: InternalConfig): set - predicate BatchExecuteStatementEnsuresPublicly(input: BatchExecuteStatementInput , output: Result) - // The private method to be refined by the library developer - - - method BatchExecuteStatement ( config: InternalConfig , input: BatchExecuteStatementInput ) - 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 BatchExecuteStatementEnsuresPublicly(input, output) - - - predicate BatchGetItemEnsuresPublicly(input: BatchGetItemInput , output: Result) - // The private method to be refined by the library developer - - - method BatchGetItem ( config: InternalConfig , input: BatchGetItemInput ) - 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 BatchGetItemEnsuresPublicly(input, output) - - - predicate BatchWriteItemEnsuresPublicly(input: BatchWriteItemInput , output: Result) - // The private method to be refined by the library developer - - - method BatchWriteItem ( config: InternalConfig , input: BatchWriteItemInput ) - 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 BatchWriteItemEnsuresPublicly(input, output) - - - predicate CreateTableEnsuresPublicly(input: CreateTableInput , output: Result) - // The private method to be refined by the library developer - - - method CreateTable ( config: InternalConfig , input: CreateTableInput ) - 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 CreateTableEnsuresPublicly(input, output) - - - predicate DeleteItemEnsuresPublicly(input: DeleteItemInput , output: Result) - // The private method to be refined by the library developer - - - method DeleteItem ( config: InternalConfig , input: DeleteItemInput ) - 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 DeleteItemEnsuresPublicly(input, output) - - - predicate DescribeTableEnsuresPublicly(input: DescribeTableInput , output: Result) - // The private method to be refined by the library developer - - - method DescribeTable ( config: InternalConfig , input: DescribeTableInput ) - 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 DescribeTableEnsuresPublicly(input, output) - - - predicate ExecuteStatementEnsuresPublicly(input: ExecuteStatementInput , output: Result) - // The private method to be refined by the library developer - - - method ExecuteStatement ( config: InternalConfig , input: ExecuteStatementInput ) - 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 ExecuteStatementEnsuresPublicly(input, output) - - - predicate ExecuteTransactionEnsuresPublicly(input: ExecuteTransactionInput , output: Result) - // The private method to be refined by the library developer - - - method ExecuteTransaction ( config: InternalConfig , input: ExecuteTransactionInput ) - 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 ExecuteTransactionEnsuresPublicly(input, output) - - - predicate GetItemEnsuresPublicly(input: GetItemInput , output: Result) - // The private method to be refined by the library developer - - - method GetItem ( config: InternalConfig , input: GetItemInput ) - 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 GetItemEnsuresPublicly(input, output) - - - predicate PutItemEnsuresPublicly(input: PutItemInput , output: Result) - // The private method to be refined by the library developer - - - method PutItem ( config: InternalConfig , input: PutItemInput ) - 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 PutItemEnsuresPublicly(input, output) - - - predicate QueryEnsuresPublicly(input: QueryInput , output: Result) - // The private method to be refined by the library developer - - - method Query ( config: InternalConfig , input: QueryInput ) - 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 QueryEnsuresPublicly(input, output) - - - predicate ScanEnsuresPublicly(input: ScanInput , output: Result) - // The private method to be refined by the library developer - - - method Scan ( config: InternalConfig , input: ScanInput ) - 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 ScanEnsuresPublicly(input, output) - - - predicate TransactGetItemsEnsuresPublicly(input: TransactGetItemsInput , output: Result) - // The private method to be refined by the library developer - - - method TransactGetItems ( config: InternalConfig , input: TransactGetItemsInput ) - 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 TransactGetItemsEnsuresPublicly(input, output) - - - predicate TransactWriteItemsEnsuresPublicly(input: TransactWriteItemsInput , output: Result) - // The private method to be refined by the library developer - - - method TransactWriteItems ( config: InternalConfig , input: TransactWriteItemsInput ) - 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 TransactWriteItemsEnsuresPublicly(input, output) - - - predicate UpdateItemEnsuresPublicly(input: UpdateItemInput , output: Result) - // The private method to be refined by the library developer - - - method UpdateItem ( config: InternalConfig , input: UpdateItemInput ) - 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 UpdateItemEnsuresPublicly(input, output) -} diff --git a/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy b/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy deleted file mode 100644 index 54a1ee107..000000000 --- a/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy +++ /dev/null @@ -1,601 +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" -module {:extern "software.amazon.cryptography.services.kms.internaldafny.types" } ComAmazonawsKmsTypes -{ - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - // Generic helpers for verification of mock/unit tests. - datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) - - // Begin Generated Types - - type AttestationDocumentType = x: seq | IsValid_AttestationDocumentType(x) witness * - predicate method IsValid_AttestationDocumentType(x: seq) { - ( 1 <= |x| <= 262144 ) - } - type CiphertextType = x: seq | IsValid_CiphertextType(x) witness * - predicate method IsValid_CiphertextType(x: seq) { - ( 1 <= |x| <= 6144 ) - } - datatype CustomerMasterKeySpec = - | RSA_2048 - | RSA_3072 - | RSA_4096 - | ECC_NIST_P256 - | ECC_NIST_P384 - | ECC_NIST_P521 - | ECC_SECG_P256K1 - | SYMMETRIC_DEFAULT - | HMAC_224 - | HMAC_256 - | HMAC_384 - | HMAC_512 - | SM2 - datatype DataKeySpec = - | AES_256 - | AES_128 - datatype DecryptRequest = | DecryptRequest ( - nameonly CiphertextBlob: CiphertextType , - nameonly EncryptionContext: Option := Option.None , - nameonly GrantTokens: Option := Option.None , - nameonly KeyId: Option := Option.None , - nameonly EncryptionAlgorithm: Option := Option.None , - nameonly Recipient: Option := Option.None , - nameonly DryRun: Option := Option.None - ) - datatype DecryptResponse = | DecryptResponse ( - nameonly KeyId: Option := Option.None , - nameonly Plaintext: Option := Option.None , - nameonly EncryptionAlgorithm: Option := Option.None , - nameonly CiphertextForRecipient: Option := Option.None - ) - datatype DeriveSharedSecretRequest = | DeriveSharedSecretRequest ( - nameonly KeyId: KeyIdType , - nameonly KeyAgreementAlgorithm: KeyAgreementAlgorithmSpec , - nameonly PublicKey: PublicKeyType , - nameonly GrantTokens: Option := Option.None , - nameonly DryRun: Option := Option.None , - nameonly Recipient: Option := Option.None - ) - datatype DeriveSharedSecretResponse = | DeriveSharedSecretResponse ( - nameonly KeyId: Option := Option.None , - nameonly SharedSecret: Option := Option.None , - nameonly CiphertextForRecipient: Option := Option.None , - nameonly KeyAgreementAlgorithm: Option := Option.None , - nameonly KeyOrigin: Option := Option.None - ) - datatype EncryptionAlgorithmSpec = - | SYMMETRIC_DEFAULT - | RSAES_OAEP_SHA_1 - | RSAES_OAEP_SHA_256 - type EncryptionAlgorithmSpecList = seq - type EncryptionContextKey = string - type EncryptionContextType = map - type EncryptionContextValue = string - datatype EncryptRequest = | EncryptRequest ( - nameonly KeyId: KeyIdType , - nameonly Plaintext: PlaintextType , - nameonly EncryptionContext: Option := Option.None , - nameonly GrantTokens: Option := Option.None , - nameonly EncryptionAlgorithm: Option := Option.None , - nameonly DryRun: Option := Option.None - ) - datatype EncryptResponse = | EncryptResponse ( - nameonly CiphertextBlob: Option := Option.None , - nameonly KeyId: Option := Option.None , - nameonly EncryptionAlgorithm: Option := Option.None - ) - type ErrorMessageType = string - datatype GenerateDataKeyRequest = | GenerateDataKeyRequest ( - nameonly KeyId: KeyIdType , - nameonly EncryptionContext: Option := Option.None , - nameonly NumberOfBytes: Option := Option.None , - nameonly KeySpec: Option := Option.None , - nameonly GrantTokens: Option := Option.None , - nameonly Recipient: Option := Option.None , - nameonly DryRun: Option := Option.None - ) - datatype GenerateDataKeyResponse = | GenerateDataKeyResponse ( - nameonly CiphertextBlob: Option := Option.None , - nameonly Plaintext: Option := Option.None , - nameonly KeyId: Option := Option.None , - nameonly CiphertextForRecipient: Option := Option.None - ) - datatype GenerateDataKeyWithoutPlaintextRequest = | GenerateDataKeyWithoutPlaintextRequest ( - nameonly KeyId: KeyIdType , - nameonly EncryptionContext: Option := Option.None , - nameonly KeySpec: Option := Option.None , - nameonly NumberOfBytes: Option := Option.None , - nameonly GrantTokens: Option := Option.None , - nameonly DryRun: Option := Option.None - ) - datatype GenerateDataKeyWithoutPlaintextResponse = | GenerateDataKeyWithoutPlaintextResponse ( - nameonly CiphertextBlob: Option := Option.None , - nameonly KeyId: Option := Option.None - ) - datatype GetPublicKeyRequest = | GetPublicKeyRequest ( - nameonly KeyId: KeyIdType , - nameonly GrantTokens: Option := Option.None - ) - datatype GetPublicKeyResponse = | GetPublicKeyResponse ( - nameonly KeyId: Option := Option.None , - nameonly PublicKey: Option := Option.None , - nameonly CustomerMasterKeySpec: Option := Option.None , - nameonly KeySpec: Option := Option.None , - nameonly KeyUsage: Option := Option.None , - nameonly EncryptionAlgorithms: Option := Option.None , - nameonly SigningAlgorithms: Option := Option.None , - nameonly KeyAgreementAlgorithms: Option := Option.None - ) - type GrantTokenList = x: seq | IsValid_GrantTokenList(x) witness * - predicate method IsValid_GrantTokenList(x: seq) { - ( 0 <= |x| <= 10 ) - } - type GrantTokenType = x: string | IsValid_GrantTokenType(x) witness * - predicate method IsValid_GrantTokenType(x: string) { - ( 1 <= |x| <= 8192 ) - } - datatype KeyAgreementAlgorithmSpec = - | ECDH - type KeyAgreementAlgorithmSpecList = seq - datatype KeyEncryptionMechanism = - | RSAES_OAEP_SHA_256 - type KeyIdType = x: string | IsValid_KeyIdType(x) witness * - predicate method IsValid_KeyIdType(x: string) { - ( 1 <= |x| <= 2048 ) - } - datatype KeySpec = - | RSA_2048 - | RSA_3072 - | RSA_4096 - | ECC_NIST_P256 - | ECC_NIST_P384 - | ECC_NIST_P521 - | ECC_SECG_P256K1 - | SYMMETRIC_DEFAULT - | HMAC_224 - | HMAC_256 - | HMAC_384 - | HMAC_512 - | SM2 - datatype KeyUsageType = - | SIGN_VERIFY - | ENCRYPT_DECRYPT - | GENERATE_VERIFY_MAC - | KEY_AGREEMENT - type NullableBooleanType = bool - type NumberOfBytesType = x: int32 | IsValid_NumberOfBytesType(x) witness * - predicate method IsValid_NumberOfBytesType(x: int32) { - ( 1 <= x <= 1024 ) - } - datatype OriginType = - | AWS_KMS - | EXTERNAL - | AWS_CLOUDHSM - | EXTERNAL_KEY_STORE - type PlaintextType = x: seq | IsValid_PlaintextType(x) witness * - predicate method IsValid_PlaintextType(x: seq) { - ( 1 <= |x| <= 4096 ) - } - type PublicKeyType = x: seq | IsValid_PublicKeyType(x) witness * - predicate method IsValid_PublicKeyType(x: seq) { - ( 1 <= |x| <= 8192 ) - } - datatype RecipientInfo = | RecipientInfo ( - nameonly KeyEncryptionAlgorithm: Option := Option.None , - nameonly AttestationDocument: Option := Option.None - ) - datatype ReEncryptRequest = | ReEncryptRequest ( - nameonly CiphertextBlob: CiphertextType , - nameonly SourceEncryptionContext: Option := Option.None , - nameonly SourceKeyId: Option := Option.None , - nameonly DestinationKeyId: KeyIdType , - nameonly DestinationEncryptionContext: Option := Option.None , - nameonly SourceEncryptionAlgorithm: Option := Option.None , - nameonly DestinationEncryptionAlgorithm: Option := Option.None , - nameonly GrantTokens: Option := Option.None , - nameonly DryRun: Option := Option.None - ) - datatype ReEncryptResponse = | ReEncryptResponse ( - nameonly CiphertextBlob: Option := Option.None , - nameonly SourceKeyId: Option := Option.None , - nameonly KeyId: Option := Option.None , - nameonly SourceEncryptionAlgorithm: Option := Option.None , - nameonly DestinationEncryptionAlgorithm: Option := Option.None - ) - type RegionType = x: string | IsValid_RegionType(x) witness * - predicate method IsValid_RegionType(x: string) { - ( 1 <= |x| <= 32 ) - } - datatype SigningAlgorithmSpec = - | RSASSA_PSS_SHA_256 - | RSASSA_PSS_SHA_384 - | RSASSA_PSS_SHA_512 - | RSASSA_PKCS1_V1_5_SHA_256 - | RSASSA_PKCS1_V1_5_SHA_384 - | RSASSA_PKCS1_V1_5_SHA_512 - | ECDSA_SHA_256 - | ECDSA_SHA_384 - | ECDSA_SHA_512 - | SM2DSA - type SigningAlgorithmSpecList = seq - class IKMSClientCallHistory { - ghost constructor() { - Decrypt := []; - DeriveSharedSecret := []; - Encrypt := []; - GenerateDataKey := []; - GenerateDataKeyWithoutPlaintext := []; - GetPublicKey := []; - ReEncrypt := []; - UpdatePrimaryRegion := []; - } - ghost var Decrypt: seq>> - ghost var DeriveSharedSecret: seq>> - ghost var Encrypt: seq>> - ghost var GenerateDataKey: seq>> - ghost var GenerateDataKeyWithoutPlaintext: seq>> - ghost var GetPublicKey: seq>> - ghost var ReEncrypt: seq>> - ghost var UpdatePrimaryRegion: seq>> - } - trait {:termination false} IKMSClient - { - // 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: IKMSClientCallHistory - predicate DecryptEnsuresPublicly(input: DecryptRequest , output: Result) - // The public method to be called by library consumers - method Decrypt ( input: DecryptRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`Decrypt - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures DecryptEnsuresPublicly(input, output) - ensures History.Decrypt == old(History.Decrypt) + [DafnyCallEvent(input, output)] - - predicate DeriveSharedSecretEnsuresPublicly(input: DeriveSharedSecretRequest , output: Result) - // The public method to be called by library consumers - method DeriveSharedSecret ( input: DeriveSharedSecretRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`DeriveSharedSecret - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures DeriveSharedSecretEnsuresPublicly(input, output) - ensures History.DeriveSharedSecret == old(History.DeriveSharedSecret) + [DafnyCallEvent(input, output)] - - predicate EncryptEnsuresPublicly(input: EncryptRequest , output: Result) - // The public method to be called by library consumers - method Encrypt ( input: EncryptRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`Encrypt - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures EncryptEnsuresPublicly(input, output) - ensures History.Encrypt == old(History.Encrypt) + [DafnyCallEvent(input, output)] - - predicate GenerateDataKeyEnsuresPublicly(input: GenerateDataKeyRequest , output: Result) - // The public method to be called by library consumers - method GenerateDataKey ( input: GenerateDataKeyRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GenerateDataKey - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures GenerateDataKeyEnsuresPublicly(input, output) - ensures History.GenerateDataKey == old(History.GenerateDataKey) + [DafnyCallEvent(input, output)] - - predicate GenerateDataKeyWithoutPlaintextEnsuresPublicly(input: GenerateDataKeyWithoutPlaintextRequest , output: Result) - // The public method to be called by library consumers - method GenerateDataKeyWithoutPlaintext ( input: GenerateDataKeyWithoutPlaintextRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GenerateDataKeyWithoutPlaintext - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures GenerateDataKeyWithoutPlaintextEnsuresPublicly(input, output) - ensures History.GenerateDataKeyWithoutPlaintext == old(History.GenerateDataKeyWithoutPlaintext) + [DafnyCallEvent(input, output)] - - predicate GetPublicKeyEnsuresPublicly(input: GetPublicKeyRequest , output: Result) - // The public method to be called by library consumers - method GetPublicKey ( input: GetPublicKeyRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`GetPublicKey - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures GetPublicKeyEnsuresPublicly(input, output) - ensures History.GetPublicKey == old(History.GetPublicKey) + [DafnyCallEvent(input, output)] - - predicate ReEncryptEnsuresPublicly(input: ReEncryptRequest , output: Result) - // The public method to be called by library consumers - method ReEncrypt ( input: ReEncryptRequest ) - returns (output: Result) - requires - && ValidState() - modifies Modifies - {History} , - History`ReEncrypt - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures ReEncryptEnsuresPublicly(input, output) - ensures History.ReEncrypt == old(History.ReEncrypt) + [DafnyCallEvent(input, output)] - - predicate UpdatePrimaryRegionEnsuresPublicly(input: UpdatePrimaryRegionRequest , output: Result<(), Error>) - // The public method to be called by library consumers - method UpdatePrimaryRegion ( input: UpdatePrimaryRegionRequest ) - returns (output: Result<(), Error>) - requires - && ValidState() - modifies Modifies - {History} , - History`UpdatePrimaryRegion - // Dafny will skip type parameters when generating a default decreases clause. - decreases Modifies - {History} - ensures - && ValidState() - ensures UpdatePrimaryRegionEnsuresPublicly(input, output) - ensures History.UpdatePrimaryRegion == old(History.UpdatePrimaryRegion) + [DafnyCallEvent(input, output)] - - } - datatype UpdatePrimaryRegionRequest = | UpdatePrimaryRegionRequest ( - nameonly KeyId: KeyIdType , - nameonly PrimaryRegion: RegionType - ) - datatype Error = - // Local Error structures are listed here - | DependencyTimeoutException ( - nameonly message: Option := Option.None - ) - | DisabledException ( - nameonly message: Option := Option.None - ) - | DryRunOperationException ( - nameonly message: Option := Option.None - ) - | IncorrectKeyException ( - nameonly message: Option := Option.None - ) - | InvalidArnException ( - nameonly message: Option := Option.None - ) - | InvalidCiphertextException ( - nameonly message: Option := Option.None - ) - | InvalidGrantTokenException ( - nameonly message: Option := Option.None - ) - | InvalidKeyUsageException ( - nameonly message: Option := Option.None - ) - | KeyUnavailableException ( - nameonly message: Option := Option.None - ) - | KMSInternalException ( - nameonly message: Option := Option.None - ) - | KMSInvalidStateException ( - nameonly message: Option := Option.None - ) - | NotFoundException ( - nameonly message: Option := Option.None - ) - | UnsupportedOperationException ( - nameonly message: Option := Option.None - ) - // Any dependent models are listed here - - - // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object, alt_text : string) - type OpaqueError = e: Error | e.Opaque? witness * -} -abstract module AbstractComAmazonawsKmsService { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = ComAmazonawsKmsTypes - datatype KMSClientConfigType = KMSClientConfigType - function method DefaultKMSClientConfigType(): KMSClientConfigType - method {:extern} KMSClient() - returns (res: Result) - ensures res.Success? ==> - && fresh(res.value) - && fresh(res.value.Modifies) - && fresh(res.value.History) - && res.value.ValidState() - // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals - function method CreateSuccessOfClient(client: IKMSClient): Result { - Success(client) - } - function method CreateFailureOfError(error: Error): Result { - Failure(error) - } -} -abstract module AbstractComAmazonawsKmsOperations { - import opened Wrappers - import opened StandardLibrary.UInt - import opened UTF8 - import opened Types = ComAmazonawsKmsTypes - type InternalConfig - predicate ValidInternalConfig?(config: InternalConfig) - function ModifiesInternalConfig(config: InternalConfig): set - predicate DecryptEnsuresPublicly(input: DecryptRequest , output: Result) - // The private method to be refined by the library developer - - - method Decrypt ( config: InternalConfig , input: DecryptRequest ) - 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 DecryptEnsuresPublicly(input, output) - - - predicate DeriveSharedSecretEnsuresPublicly(input: DeriveSharedSecretRequest , output: Result) - // The private method to be refined by the library developer - - - method DeriveSharedSecret ( config: InternalConfig , input: DeriveSharedSecretRequest ) - 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 DeriveSharedSecretEnsuresPublicly(input, output) - - - predicate EncryptEnsuresPublicly(input: EncryptRequest , output: Result) - // The private method to be refined by the library developer - - - method Encrypt ( config: InternalConfig , input: EncryptRequest ) - 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 EncryptEnsuresPublicly(input, output) - - - predicate GenerateDataKeyEnsuresPublicly(input: GenerateDataKeyRequest , output: Result) - // The private method to be refined by the library developer - - - method GenerateDataKey ( config: InternalConfig , input: GenerateDataKeyRequest ) - 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 GenerateDataKeyEnsuresPublicly(input, output) - - - predicate GenerateDataKeyWithoutPlaintextEnsuresPublicly(input: GenerateDataKeyWithoutPlaintextRequest , output: Result) - // The private method to be refined by the library developer - - - method GenerateDataKeyWithoutPlaintext ( config: InternalConfig , input: GenerateDataKeyWithoutPlaintextRequest ) - 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 GenerateDataKeyWithoutPlaintextEnsuresPublicly(input, output) - - - predicate GetPublicKeyEnsuresPublicly(input: GetPublicKeyRequest , output: Result) - // The private method to be refined by the library developer - - - method GetPublicKey ( config: InternalConfig , input: GetPublicKeyRequest ) - 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 GetPublicKeyEnsuresPublicly(input, output) - - - predicate ReEncryptEnsuresPublicly(input: ReEncryptRequest , output: Result) - // The private method to be refined by the library developer - - - method ReEncrypt ( config: InternalConfig , input: ReEncryptRequest ) - 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 ReEncryptEnsuresPublicly(input, output) - - - predicate UpdatePrimaryRegionEnsuresPublicly(input: UpdatePrimaryRegionRequest , output: Result<(), Error>) - // The private method to be refined by the library developer - - - method UpdatePrimaryRegion ( config: InternalConfig , input: UpdatePrimaryRegionRequest ) - returns (output: Result<(), Error>) - requires - && ValidInternalConfig?(config) - modifies ModifiesInternalConfig(config) - // Dafny will skip type parameters when generating a default decreases clause. - decreases ModifiesInternalConfig(config) - ensures - && ValidInternalConfig?(config) - ensures UpdatePrimaryRegionEnsuresPublicly(input, output) -}