diff --git a/.github/workflows/go-release.yml b/.github/workflows/go-release.yml new file mode 100644 index 000000000..36d2fbe42 --- /dev/null +++ b/.github/workflows/go-release.yml @@ -0,0 +1,112 @@ +name: Go Release Automation + +on: + workflow_dispatch: + inputs: + project-name: + description: "Project name (e.g., AwsEncryptionSDK)" + required: true + type: string + version: + description: "Version (e.g., v0.1.0)" + required: true + type: string + +jobs: + get-dafny-version: + uses: ./.github/workflows/dafny_version.yaml + + go-release: + needs: get-dafny-version + runs-on: macos-13 + permissions: + contents: write + pull-requests: write + id-token: write + + steps: + - name: Support longpaths on Git checkout + run: | + git config --global core.longpaths true + + - name: Configure AWS Credentials for Tests + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: GoReleaseTest + + - name: Checkout repository + uses: actions/checkout@v4 + with: + fetch-depth: 0 + token: ${{ secrets.GITHUB_TOKEN }} + + - name: Update submodules + run: | + git submodule update --init --recursive + + - name: Setup Dafny + uses: ./mpl/.github/actions/setup_dafny + with: + dafny-version: ${{ needs.get-dafny-version.outputs.version }} + + - name: Install Go + uses: actions/setup-go@v5 + with: + go-version: "1.23" + + - name: Install Go imports + run: | + go install golang.org/x/tools/cmd/goimports@latest + + - name: Install Smithy-Dafny codegen dependencies + uses: ./.github/actions/install_smithy_dafny_codegen_dependencies + + - name: Configure Git + run: | + git config --global user.name "GitHub Actions" + git config --global user.email "actions@github.com" + + - name: Get release directory name + id: release-dir + run: | + chmod +x mpl/scripts/go-release-automation.sh + RELEASE_DIR_NAME=$(mpl/scripts/go-release-automation.sh get_release_dir_name "${{ github.event.inputs.project-name }}" "${{ github.event.inputs.version }}") + echo "releaseDirName=$RELEASE_DIR_NAME" >> $GITHUB_OUTPUT + + - name: Generate a changelog + uses: orhun/git-cliff-action@v4 + with: + config: releases/go/.git-cliff.toml + args: --bump -u --prepend releases/go/${{ steps.release-dir.outputs.releaseDirName }}/CHANGELOG.md + + - name: Run Go release automation script + run: | + mpl/scripts/go-release-automation.sh run_release_script ${{ github.event.inputs.project-name }} ${{ github.event.inputs.version }} + + - name: Create Pull Request + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + run: | + PROJECT_NAME="${{ github.event.inputs.project-name }}" + VERSION="${{ github.event.inputs.version }}" + + # Get the release directory name using the sourced function + RELEASE_DIR_NAME="${{ steps.release-dir.outputs.releaseDirName }}" + + BRANCH_NAME="golang-release-staging-branch/$RELEASE_DIR_NAME/$VERSION" + + DIFF_FILES=$(diff -qr $PROJECT_NAME/runtimes/go/ImplementationFromDafny-go releases/go/$RELEASE_DIR_NAME || true) + + # Create PR using GitHub CLI + gh pr create \ + --title "chore(go): Release $RELEASE_DIR_NAME Go module $VERSION" \ + --body "This PR was automatically created by the Go Release Automation workflow. It releases version $VERSION of the $RELEASE_DIR_NAME Go module. The diff between $PROJECT_NAME/runtimes/go/ImplementationFromDafny-go and releases/go/$RELEASE_DIR_NAME is below: + + $DIFF_FILES + " \ + --base mainline \ + --head "$BRANCH_NAME" \ + --label "golang" \ + --draft diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod index 14f52cf12..fdeec323e 100644 --- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod +++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/go.mod @@ -3,7 +3,7 @@ module github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk go 1.23.0 replace ( - github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl => ../../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ + github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb => ../../../../mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms => ../../../../mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ diff --git a/mpl b/mpl index ec013f6ba..6fed3f6c8 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit ec013f6ba85d62ab41db48fec92baca85625e4b9 +Subproject commit 6fed3f6c89f06d6d7d35b85937c0216b2d5fa03b diff --git a/project.properties b/project.properties index 3e44ddb9d..cc17413a5 100644 --- a/project.properties +++ b/project.properties @@ -4,6 +4,6 @@ dafnyVersion=4.9.0 dafnyVerifyVersion=4.9.0 dafnyFormatVersion=4.9.0 projectJavaVersion=4.1.0 -mplDependencyJavaVersion=1.11.0-SNAPSHOT +mplDependencyJavaVersion=1.11.1-SNAPSHOT dafnyRuntimeJavaVersion=4.9.0 smithyDafnyJavaConversionVersion=0.1.1 diff --git a/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes/AwsCryptographyEncryptionSdkTypes.go b/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes/AwsCryptographyEncryptionSdkTypes.go index afdd9dfa5..b396d43b1 100644 --- a/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes/AwsCryptographyEncryptionSdkTypes.go +++ b/releases/go/encryption-sdk/AwsCryptographyEncryptionSdkTypes/AwsCryptographyEncryptionSdkTypes.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -120,6 +121,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -144,40 +146,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -202,7 +205,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ diff --git a/releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go b/releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go index 33c3961d0..ca3ad810f 100644 --- a/releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go +++ b/releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -136,6 +137,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -160,40 +162,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -218,7 +221,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -349,9 +351,9 @@ func (_static *CompanionStruct_Default___) Encrypt(config Config, input m_AwsCry if (_7_algorithmSuiteId).Is_Some() { var _8_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _8_valueOrError4 - _8_valueOrError4 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnEncrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_((_7_algorithmSuiteId).Dtor_value().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer30 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg31 interface{}) interface{} { - return coer30(arg31.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _8_valueOrError4 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnEncrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_((_7_algorithmSuiteId).Dtor_value().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer29 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg30 interface{}) interface{} { + return coer29(arg30.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_9_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_9_e) @@ -366,7 +368,7 @@ func (_static *CompanionStruct_Default___) Encrypt(config Config, input m_AwsCry } var _11_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _11_valueOrError5 - _11_valueOrError5 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((input).Dtor_plaintext()).Cardinality())).Cmp(m_StandardLibrary_UInt.Companion_Default___.INT64__MAX__LIMIT()) < 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Plaintext exceeds maximum allowed size"))) + _11_valueOrError5 = m_Wrappers.Companion_Default___.Need((uint64(((input).Dtor_plaintext()).Cardinality())) < ((m_StandardLibrary_UInt.Companion_Default___.INT64__MAX__LIMIT()).Uint64()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Plaintext exceeds maximum allowed size"))) if (_11_valueOrError5).IsFailure() { output = (_11_valueOrError5).PropagateFailure() return output @@ -422,9 +424,9 @@ func (_static *CompanionStruct_Default___) Encrypt(config Config, input m_AwsCry _19_maybeDerivedDataKeys = _out3 var _20_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_KeyDerivation.Companion_ExpandedKeyMaterial_.Default()) _ = _20_valueOrError10 - _20_valueOrError10 = (_19_maybeDerivedDataKeys).MapFailure(func(coer31 func(m_AwsCryptographyEncryptionSdkTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg32 interface{}) interface{} { - return coer31(arg32.(m_AwsCryptographyEncryptionSdkTypes.Error)) + _20_valueOrError10 = (_19_maybeDerivedDataKeys).MapFailure(func(coer30 func(m_AwsCryptographyEncryptionSdkTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg31 interface{}) interface{} { + return coer30(arg31.(m_AwsCryptographyEncryptionSdkTypes.Error)) } }(func(_21_e m_AwsCryptographyEncryptionSdkTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Failed to derive data keys")) @@ -506,9 +508,9 @@ func (_static *CompanionStruct_Default___) SignAndSerializeMessage(config Config _4_maybeBytes = _out0 var _5_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) _ = _5_valueOrError2 - _5_valueOrError2 = (_4_maybeBytes).MapFailure(func(coer32 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg33 interface{}) interface{} { - return coer32(arg33.(m_AwsCryptographyPrimitivesTypes.Error)) + _5_valueOrError2 = (_4_maybeBytes).MapFailure(func(coer31 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg32 interface{}) interface{} { + return coer31(arg32.(m_AwsCryptographyPrimitivesTypes.Error)) } }(func(_6_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_6_e) @@ -522,7 +524,7 @@ func (_static *CompanionStruct_Default___) SignAndSerializeMessage(config Config _7_bytes = (_5_valueOrError2).Extract().(_dafny.Sequence) var _8_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _8_valueOrError3 - _8_valueOrError3 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_7_bytes).Cardinality())).Cmp(m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()) < 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Length of signature bytes is larger than the uint16 limit."))) + _8_valueOrError3 = m_Wrappers.Companion_Default___.Need((uint64((_7_bytes).Cardinality())) < ((m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()).Uint64()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Length of signature bytes is larger than the uint16 limit."))) if (_8_valueOrError3).IsFailure() { output = (_8_valueOrError3).PropagateFailure() return output @@ -567,7 +569,7 @@ func (_static *CompanionStruct_Default___) Decrypt(config Config, input m_AwsCry _1_cmm = m_AwsCryptographyMaterialProvidersTypes.Companion_ICryptographicMaterialsManager_.CastTo_((_0_valueOrError0).Extract()) var _2_buffer m_SerializeFunctions.ReadableBuffer _ = _2_buffer - _2_buffer = m_SerializeFunctions.Companion_ReadableBuffer_.Create_ReadableBuffer_((input).Dtor_ciphertext(), _dafny.Zero) + _2_buffer = m_SerializeFunctions.Companion_ReadableBuffer_.Create_ReadableBuffer_((input).Dtor_ciphertext(), uint64(0)) var _out1 m_Wrappers.Result _ = _out1 _out1 = Companion_Default___.InternalDecrypt(config, _1_cmm, _2_buffer, (input).Dtor_encryptionContext()) @@ -582,9 +584,9 @@ func (_static *CompanionStruct_Default___) InternalDecrypt(config Config, cmm m_ _0_v4Retry = false var _1_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _1_valueOrError0 - _1_valueOrError0 = (m_Header.Companion_Default___.ReadHeaderBody(buffer, (config).Dtor_maxEncryptedDataKeys(), (config).Dtor_mpl())).MapFailure(func(coer33 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg34 interface{}) interface{} { - return coer33(arg34.(m_SerializeFunctions.ReadProblems)) + _1_valueOrError0 = (m_Header.Companion_Default___.ReadHeaderBody(buffer, (config).Dtor_maxEncryptedDataKeys(), (config).Dtor_mpl())).MapFailure(func(coer32 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg33 interface{}) interface{} { + return coer32(arg33.(m_SerializeFunctions.ReadProblems)) } }(m_EncryptDecryptHelpers.Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadHeaderBody")))) if (_1_valueOrError0).IsFailure() { @@ -596,15 +598,15 @@ func (_static *CompanionStruct_Default___) InternalDecrypt(config Config, cmm m_ _2_headerBody = (_1_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) var _3_rawHeader _dafny.Sequence _ = _3_rawHeader - _3_rawHeader = ((buffer).Dtor_bytes()).Subsequence(((buffer).Dtor_start()).Uint32(), (((_2_headerBody).Dtor_tail()).Dtor_start()).Uint32()) + _3_rawHeader = ((buffer).Dtor_bytes()).Subsequence(uint32((buffer).Dtor_start()), uint32(((_2_headerBody).Dtor_tail()).Dtor_start())) var _4_algorithmSuite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo _ = _4_algorithmSuite _4_algorithmSuite = ((_2_headerBody).Dtor_data().(m_HeaderTypes.HeaderBody)).Dtor_algorithmSuite() var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _5_valueOrError1 - _5_valueOrError1 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnDecrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_((_4_algorithmSuite).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer34 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg35 interface{}) interface{} { - return coer34(arg35.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _5_valueOrError1 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnDecrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_((_4_algorithmSuite).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer33 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg34 interface{}) interface{} { + return coer33(arg34.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_6_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_6_e) @@ -641,9 +643,9 @@ func (_static *CompanionStruct_Default___) InternalDecrypt(config Config, cmm m_ } var _12_valueOrError4 m_Wrappers.Result = m_Wrappers.Result{} _ = _12_valueOrError4 - _12_valueOrError4 = (m_HeaderAuth.Companion_Default___.ReadHeaderAuthTag((_2_headerBody).Dtor_tail(), _10_suite)).MapFailure(func(coer35 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg36 interface{}) interface{} { - return coer35(arg36.(m_SerializeFunctions.ReadProblems)) + _12_valueOrError4 = (m_HeaderAuth.Companion_Default___.ReadHeaderAuthTag((_2_headerBody).Dtor_tail(), _10_suite)).MapFailure(func(coer34 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg35 interface{}) interface{} { + return coer34(arg35.(m_SerializeFunctions.ReadProblems)) } }(m_EncryptDecryptHelpers.Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadHeaderAuthTag")))) if (_12_valueOrError4).IsFailure() { @@ -731,9 +733,9 @@ func (_static *CompanionStruct_Default___) InternalDecrypt(config Config, cmm m_ } var _26_valueOrError9 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) _ = _26_valueOrError9 - _26_valueOrError9 = (_24_maybeHeaderAuth).MapFailure(func(coer36 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg37 interface{}) interface{} { - return coer36(arg37.(m_AwsCryptographyPrimitivesTypes.Error)) + _26_valueOrError9 = (_24_maybeHeaderAuth).MapFailure(func(coer35 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg36 interface{}) interface{} { + return coer35(arg36.(m_AwsCryptographyPrimitivesTypes.Error)) } }(func(_27_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_27_e) @@ -802,7 +804,7 @@ Lmatch0: _ = _37_valueOrError12 var _out8 m_Wrappers.Result _ = _out8 - _out8 = m_EncryptDecryptHelpers.Companion_Default___.VerifySignature(_32_messageBodyTail, ((_32_messageBodyTail).Dtor_bytes()).Subsequence(((buffer).Dtor_start()).Uint32(), ((_32_messageBodyTail).Dtor_start()).Uint32()), _9_decMat, (config).Dtor_crypto()) + _out8 = m_EncryptDecryptHelpers.Companion_Default___.VerifySignature(_32_messageBodyTail, ((_32_messageBodyTail).Dtor_bytes()).Subsequence(uint32((buffer).Dtor_start()), uint32((_32_messageBodyTail).Dtor_start())), _9_decMat, (config).Dtor_crypto()) _37_valueOrError12 = _out8 if (_37_valueOrError12).IsFailure() { output = (_37_valueOrError12).PropagateFailure() @@ -813,7 +815,7 @@ Lmatch0: _38_signature = (_37_valueOrError12).Extract().(m_SerializeFunctions.ReadableBuffer) var _39_valueOrError13 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _39_valueOrError13 - _39_valueOrError13 = m_Wrappers.Companion_Default___.Need(((_38_signature).Dtor_start()).Cmp(_dafny.IntOfUint32(((_38_signature).Dtor_bytes()).Cardinality())) == 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Data after message footer."))) + _39_valueOrError13 = m_Wrappers.Companion_Default___.Need(((_38_signature).Dtor_start()) == (uint64(((_38_signature).Dtor_bytes()).Cardinality())), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Data after message footer."))) if (_39_valueOrError13).IsFailure() { output = (_39_valueOrError13).PropagateFailure() return output diff --git a/releases/go/encryption-sdk/CHANGELOG.md b/releases/go/encryption-sdk/CHANGELOG.md index d20b375aa..37619f1ca 100644 --- a/releases/go/encryption-sdk/CHANGELOG.md +++ b/releases/go/encryption-sdk/CHANGELOG.md @@ -1,3 +1,37 @@ +## [releases/go/encryption-sdk/v0.2.1] - 2025-08-12 + +### 🐛 Bug Fixes + +- _(go)_ Fix and refactor go mod (#793) + +### 📚 Documentation + +- _(Go)_ Add Go to supported languages in the readme (#780) + +### ⚙️ Miscellaneous Tasks + +- Fail verification on warnings (#766) +- _(dafny)_ Allow FileIO to deal in uint8, rather than bv8 (#770) +- _(CI)_ Fix daily CI (#771) +- _(CI)_ Clean up unused attributes (#772) +- Add C to list of languages checked for interoperability (#773) +- Bump smithy-dafny to latest (#774) +- Bump MPL to latest version (#775) +- Improve performance (#764) +- _(rust)_ Update smithy-dafny and use small-int feature (#777) +- Bump MPL version (#778) +- _(dafny)_ Remove more usage of BigInteger (#781) +- Install polymorph deps in github workflows (#783) +- _(rust)_ Prepare rust 1.1.0 release (#782) +- _(rust)_ Prepare 1.1.1 release (#784) +- _(CI)_ Partially fix nightly build (#785) +- _(dafny)_ Update makefile to only use prettier 3.5.3 (#786) +- Bump mpl (#787) +- _(go)_ Update go test matrix and clean up setup (#788) +- Let interop testing launch N tasks instead of N^2 (#789) +- _(CI)_ Add backwards compatability tests for nightly (#790) +- _(CI)_ Add slack notifications (#797) + # Changelog # [0.2.0] (2025-03-21) diff --git a/releases/go/encryption-sdk/ESDK/ESDK.go b/releases/go/encryption-sdk/ESDK/ESDK.go index 8e6bba505..f8397fd11 100644 --- a/releases/go/encryption-sdk/ESDK/ESDK.go +++ b/releases/go/encryption-sdk/ESDK/ESDK.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -136,6 +137,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -160,40 +162,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -218,7 +221,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -304,9 +306,9 @@ func (_static *CompanionStruct_Default___) ESDK(config m_AwsCryptographyEncrypti _0_maybeCrypto = _out0 var _1_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _1_valueOrError0 - _1_valueOrError0 = (_0_maybeCrypto).MapFailure(func(coer37 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg38 interface{}) interface{} { - return coer37(arg38.(m_AwsCryptographyPrimitivesTypes.Error)) + _1_valueOrError0 = (_0_maybeCrypto).MapFailure(func(coer36 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg37 interface{}) interface{} { + return coer36(arg37.(m_AwsCryptographyPrimitivesTypes.Error)) } }(func(_2_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_2_e) @@ -329,9 +331,9 @@ func (_static *CompanionStruct_Default___) ESDK(config m_AwsCryptographyEncrypti _5_maybeMpl = _out1 var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Result{} _ = _6_valueOrError1 - _6_valueOrError1 = (_5_maybeMpl).MapFailure(func(coer38 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg39 interface{}) interface{} { - return coer38(arg39.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _6_valueOrError1 = (_5_maybeMpl).MapFailure(func(coer37 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg38 interface{}) interface{} { + return coer37(arg38.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_7_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_7_e) diff --git a/releases/go/encryption-sdk/EncryptDecryptHelpers/EncryptDecryptHelpers.go b/releases/go/encryption-sdk/EncryptDecryptHelpers/EncryptDecryptHelpers.go index 06ba67eb3..26aa28871 100644 --- a/releases/go/encryption-sdk/EncryptDecryptHelpers/EncryptDecryptHelpers.go +++ b/releases/go/encryption-sdk/EncryptDecryptHelpers/EncryptDecryptHelpers.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -135,6 +136,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -159,40 +161,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -217,7 +220,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -463,7 +465,7 @@ func (_static *CompanionStruct_Default___) CreateCmmFromInput(inputCmm m_Wrapper return res } func (_static *CompanionStruct_Default___) ValidateMaxEncryptedDataKeys(maxEncryptedDataKeys m_Wrappers.Option, edks _dafny.Sequence) m_Wrappers.Outcome { - if ((maxEncryptedDataKeys).Is_Some()) && ((_dafny.IntOfUint32((edks).Cardinality())).Cmp(_dafny.IntOfInt64((maxEncryptedDataKeys).Dtor_value().(int64))) > 0) { + if ((maxEncryptedDataKeys).Is_Some()) && ((uint64((edks).Cardinality())) > (uint64((maxEncryptedDataKeys).Dtor_value().(int64)))) { return m_Wrappers.Companion_Outcome_.Create_Fail_(m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Encrypted data keys exceed maxEncryptedDataKeys"))) } else { return m_Wrappers.Companion_Outcome_.Create_Pass_() @@ -477,12 +479,12 @@ func (_static *CompanionStruct_Default___) GenerateMessageId(suite m_AwsCryptogr if ((suite).Dtor_messageVersion()) == (int32(1)) { var _out0 m_Wrappers.Result _ = _out0 - _out0 = (crypto).GenerateRandomBytes(m_AwsCryptographyPrimitivesTypes.Companion_GenerateRandomBytesInput_.Create_GenerateRandomBytesInput_((m_HeaderTypes.Companion_Default___.MESSAGE__ID__LEN__V1()).Int32())) + _out0 = (crypto).GenerateRandomBytes(m_AwsCryptographyPrimitivesTypes.Companion_GenerateRandomBytesInput_.Create_GenerateRandomBytesInput_(int32(m_HeaderTypes.Companion_Default___.MESSAGE__ID__LEN__V1()))) _0_maybeId = _out0 } else { var _out1 m_Wrappers.Result _ = _out1 - _out1 = (crypto).GenerateRandomBytes(m_AwsCryptographyPrimitivesTypes.Companion_GenerateRandomBytesInput_.Create_GenerateRandomBytesInput_((m_HeaderTypes.Companion_Default___.MESSAGE__ID__LEN__V2()).Int32())) + _out1 = (crypto).GenerateRandomBytes(m_AwsCryptographyPrimitivesTypes.Companion_GenerateRandomBytesInput_.Create_GenerateRandomBytesInput_(int32(m_HeaderTypes.Companion_Default___.MESSAGE__ID__LEN__V2()))) _0_maybeId = _out1 } var _1_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) @@ -617,7 +619,7 @@ func (_static *CompanionStruct_Default___) BuildHeaderBody(messageId _dafny.Sequ { { if _source0.Is_None() { - res = m_HeaderTypes.Companion_HeaderBody_.Create_V1HeaderBody_(m_HeaderTypes.Companion_MessageType_.Create_TYPE__CUSTOMER__AED_(), suite, messageId, encryptionContext, encryptedDataKeys, _0_contentType, _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength(suite)), frameLength) + res = m_HeaderTypes.Companion_HeaderBody_.Create_V1HeaderBody_(m_HeaderTypes.Companion_MessageType_.Create_TYPE__CUSTOMER__AED_(), suite, messageId, encryptionContext, encryptedDataKeys, _0_contentType, uint64(m_SerializableTypes.Companion_Default___.GetIvLength(suite)), frameLength) return res goto Lmatch0 } @@ -634,54 +636,45 @@ Lmatch0: func (_static *CompanionStruct_Default___) BuildHeaderAuthTag(suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, dataKey _dafny.Sequence, rawHeader _dafny.Sequence, serializedReqEncryptionContext _dafny.Sequence, crypto *m_AtomicPrimitives.AtomicPrimitivesClient) m_Wrappers.Result { var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_HeaderTypes.Companion_HeaderAuth_.Default()) _ = res - var _0_keyLength _dafny.Int + var _0_keyLength int32 _ = _0_keyLength - _0_keyLength = _dafny.IntOfInt32(m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)) + _0_keyLength = m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite) var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _1_valueOrError0 - _1_valueOrError0 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((dataKey).Cardinality())).Cmp(_0_keyLength) == 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Incorrect data key length"))) + _1_valueOrError0 = m_Wrappers.Companion_Default___.Need((uint64((dataKey).Cardinality())) == (uint64(_0_keyLength)), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Incorrect data key length"))) if (_1_valueOrError0).IsFailure() { res = (_1_valueOrError0).PropagateFailure() return res } - var _2_ivLength uint8 - _ = _2_ivLength - _2_ivLength = m_SerializableTypes.Companion_Default___.GetIvLength(suite) - var _3_iv _dafny.Sequence - _ = _3_iv - _3_iv = _dafny.SeqCreate(uint32(_2_ivLength), func(coer20 func(_dafny.Int) uint8) func(_dafny.Int) interface{} { - return func(arg21 _dafny.Int) interface{} { - return coer20(arg21) - } - }(func(_4___v3 _dafny.Int) uint8 { - return uint8(0) - })) - var _5_maybeEncryptionOutput m_Wrappers.Result - _ = _5_maybeEncryptionOutput + var _2_iv _dafny.Sequence + _ = _2_iv + _2_iv = m_SerializableTypes.Companion_Default___.GetIvLengthZeros(suite) + var _3_maybeEncryptionOutput m_Wrappers.Result + _ = _3_maybeEncryptionOutput var _out0 m_Wrappers.Result _ = _out0 - _out0 = (crypto).AESEncrypt(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptInput_.Create_AESEncryptInput_(((suite).Dtor_encrypt()).Dtor_AES__GCM(), _3_iv, dataKey, _dafny.SeqOf(), _dafny.Companion_Sequence_.Concatenate(rawHeader, serializedReqEncryptionContext))) - _5_maybeEncryptionOutput = _out0 - var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Default()) - _ = _6_valueOrError1 - _6_valueOrError1 = (_5_maybeEncryptionOutput).MapFailure(func(coer21 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg22 interface{}) interface{} { - return coer21(arg22.(m_AwsCryptographyPrimitivesTypes.Error)) + _out0 = (crypto).AESEncrypt(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptInput_.Create_AESEncryptInput_(((suite).Dtor_encrypt()).Dtor_AES__GCM(), _2_iv, dataKey, _dafny.SeqOf(), _dafny.Companion_Sequence_.Concatenate(rawHeader, serializedReqEncryptionContext))) + _3_maybeEncryptionOutput = _out0 + var _4_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Default()) + _ = _4_valueOrError1 + _4_valueOrError1 = (_3_maybeEncryptionOutput).MapFailure(func(coer20 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg21 interface{}) interface{} { + return coer20(arg21.(m_AwsCryptographyPrimitivesTypes.Error)) } - }(func(_7_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { - return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_7_e) + }(func(_5_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { + return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_5_e) })) - if (_6_valueOrError1).IsFailure() { - res = (_6_valueOrError1).PropagateFailure() + if (_4_valueOrError1).IsFailure() { + res = (_4_valueOrError1).PropagateFailure() return res } - var _8_encryptionOutput m_AwsCryptographyPrimitivesTypes.AESEncryptOutput - _ = _8_encryptionOutput - _8_encryptionOutput = (_6_valueOrError1).Extract().(m_AwsCryptographyPrimitivesTypes.AESEncryptOutput) - var _9_headerAuth m_HeaderTypes.HeaderAuth - _ = _9_headerAuth - _9_headerAuth = m_HeaderTypes.Companion_HeaderAuth_.Create_AESMac_(_3_iv, (_8_encryptionOutput).Dtor_authTag()) - res = m_Wrappers.Companion_Result_.Create_Success_(_9_headerAuth) + var _6_encryptionOutput m_AwsCryptographyPrimitivesTypes.AESEncryptOutput + _ = _6_encryptionOutput + _6_encryptionOutput = (_4_valueOrError1).Extract().(m_AwsCryptographyPrimitivesTypes.AESEncryptOutput) + var _7_headerAuth m_HeaderTypes.HeaderAuth + _ = _7_headerAuth + _7_headerAuth = m_HeaderTypes.Companion_HeaderAuth_.Create_AESMac_(_2_iv, (_6_encryptionOutput).Dtor_authTag()) + res = m_Wrappers.Companion_Result_.Create_Success_(_7_headerAuth) return res return res } @@ -699,9 +692,9 @@ func (_static *CompanionStruct_Default___) GetEncryptionMaterials(cmm m_AwsCrypt _1_getEncMatResult = _out0 var _2_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _2_valueOrError0 - _2_valueOrError0 = (_1_getEncMatResult).MapFailure(func(coer22 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg23 interface{}) interface{} { - return coer22(arg23.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _2_valueOrError0 = (_1_getEncMatResult).MapFailure(func(coer21 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg22 interface{}) interface{} { + return coer21(arg22.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_3_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_3_e) @@ -718,9 +711,9 @@ func (_static *CompanionStruct_Default___) GetEncryptionMaterials(cmm m_AwsCrypt _5_materials = (_4_output).Dtor_encryptionMaterials() var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _6_valueOrError1 - _6_valueOrError1 = ((mpl).ValidateCommitmentPolicyOnEncrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_(((_5_materials).Dtor_algorithmSuite()).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_(commitmentPolicy)))).MapFailure(func(coer23 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg24 interface{}) interface{} { - return coer23(arg24.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _6_valueOrError1 = ((mpl).ValidateCommitmentPolicyOnEncrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_(((_5_materials).Dtor_algorithmSuite()).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_(commitmentPolicy)))).MapFailure(func(coer22 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg23 interface{}) interface{} { + return coer22(arg23.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_7_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_7_e) @@ -729,14 +722,14 @@ func (_static *CompanionStruct_Default___) GetEncryptionMaterials(cmm m_AwsCrypt res = (_6_valueOrError1).PropagateFailure() return res } - var _8___v4 _dafny.Tuple - _ = _8___v4 - _8___v4 = (_6_valueOrError1).Extract().(_dafny.Tuple) + var _8___v3 _dafny.Tuple + _ = _8___v3 + _8___v3 = (_6_valueOrError1).Extract().(_dafny.Tuple) var _9_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _9_valueOrError2 - _9_valueOrError2 = ((mpl).EncryptionMaterialsHasPlaintextDataKey(_5_materials)).MapFailure(func(coer24 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg25 interface{}) interface{} { - return coer24(arg25.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _9_valueOrError2 = ((mpl).EncryptionMaterialsHasPlaintextDataKey(_5_materials)).MapFailure(func(coer23 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg24 interface{}) interface{} { + return coer23(arg24.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_10_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_10_e) @@ -745,9 +738,9 @@ func (_static *CompanionStruct_Default___) GetEncryptionMaterials(cmm m_AwsCrypt res = (_9_valueOrError2).PropagateFailure() return res } - var _11___v5 _dafny.Tuple - _ = _11___v5 - _11___v5 = (_9_valueOrError2).Extract().(_dafny.Tuple) + var _11___v4 _dafny.Tuple + _ = _11___v4 + _11___v4 = (_9_valueOrError2).Extract().(_dafny.Tuple) var _12_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _12_valueOrError3 _12_valueOrError3 = m_Wrappers.Companion_Default___.Need(m_SerializableTypes.Companion_Default___.IsESDKEncryptionContext((_5_materials).Dtor_encryptionContext()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("CMM failed to return serializable encryption materials."))) @@ -794,9 +787,9 @@ func (_static *CompanionStruct_Default___) GetDecryptionMaterials(cmm m_AwsCrypt _2_decMatResult = _out0 var _3_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _3_valueOrError0 - _3_valueOrError0 = (_2_decMatResult).MapFailure(func(coer25 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg26 interface{}) interface{} { - return coer25(arg26.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _3_valueOrError0 = (_2_decMatResult).MapFailure(func(coer24 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg25 interface{}) interface{} { + return coer24(arg25.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_4_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_4_e) @@ -813,9 +806,9 @@ func (_static *CompanionStruct_Default___) GetDecryptionMaterials(cmm m_AwsCrypt _6_materials = (_5_output).Dtor_decryptionMaterials() var _7_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _7_valueOrError1 - _7_valueOrError1 = ((mpl).ValidateCommitmentPolicyOnDecrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_(((_6_materials).Dtor_algorithmSuite()).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_(commitmentPolicy)))).MapFailure(func(coer26 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg27 interface{}) interface{} { - return coer26(arg27.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _7_valueOrError1 = ((mpl).ValidateCommitmentPolicyOnDecrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnDecryptInput_.Create_ValidateCommitmentPolicyOnDecryptInput_(((_6_materials).Dtor_algorithmSuite()).Dtor_id(), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_(commitmentPolicy)))).MapFailure(func(coer25 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg26 interface{}) interface{} { + return coer25(arg26.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_8_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_8_e) @@ -824,14 +817,14 @@ func (_static *CompanionStruct_Default___) GetDecryptionMaterials(cmm m_AwsCrypt res = (_7_valueOrError1).PropagateFailure() return res } - var _9___v6 _dafny.Tuple - _ = _9___v6 - _9___v6 = (_7_valueOrError1).Extract().(_dafny.Tuple) + var _9___v5 _dafny.Tuple + _ = _9___v5 + _9___v5 = (_7_valueOrError1).Extract().(_dafny.Tuple) var _10_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf()) _ = _10_valueOrError2 - _10_valueOrError2 = ((mpl).DecryptionMaterialsWithPlaintextDataKey(_6_materials)).MapFailure(func(coer27 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg28 interface{}) interface{} { - return coer27(arg28.(m_AwsCryptographyMaterialProvidersTypes.Error)) + _10_valueOrError2 = ((mpl).DecryptionMaterialsWithPlaintextDataKey(_6_materials)).MapFailure(func(coer26 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg27 interface{}) interface{} { + return coer26(arg27.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_11_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error { return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_11_e) @@ -840,9 +833,9 @@ func (_static *CompanionStruct_Default___) GetDecryptionMaterials(cmm m_AwsCrypt res = (_10_valueOrError2).PropagateFailure() return res } - var _12___v7 _dafny.Tuple - _ = _12___v7 - _12___v7 = (_10_valueOrError2).Extract().(_dafny.Tuple) + var _12___v6 _dafny.Tuple + _ = _12___v6 + _12___v6 = (_10_valueOrError2).Extract().(_dafny.Tuple) var _13_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _13_valueOrError3 _13_valueOrError3 = m_Wrappers.Companion_Default___.Need(m_SerializableTypes.Companion_Default___.IsESDKEncryptionContext((_6_materials).Dtor_encryptionContext()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("CMM failed to return serializable encryption materials."))) @@ -859,7 +852,7 @@ func (_static *CompanionStruct_Default___) ValidateSuiteData(suite m_AwsCryptogr _ = res var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _0_valueOrError0 - _0_valueOrError0 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((header).Dtor_suiteData()).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength())) == 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Commitment key is invalid"))) + _0_valueOrError0 = m_Wrappers.Companion_Default___.Need((uint64(((header).Dtor_suiteData()).Cardinality())) == (uint64((((suite).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength())), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Commitment key is invalid"))) if (_0_valueOrError0).IsFailure() { res = (_0_valueOrError0).PropagateFailure() return res @@ -880,9 +873,9 @@ func (_static *CompanionStruct_Default___) ReadAndDecryptFramedMessageBody(buffe _ = res var _0_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _0_valueOrError0 - _0_valueOrError0 = (m_MessageBody.Companion_Default___.ReadFramedMessageBody(buffer, header, _dafny.SeqOf(), buffer)).MapFailure(func(coer28 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg29 interface{}) interface{} { - return coer28(arg29.(m_SerializeFunctions.ReadProblems)) + _0_valueOrError0 = (m_MessageBody.Companion_Default___.ReadFramedMessageBody(buffer, header, _dafny.SeqOf(), buffer)).MapFailure(func(coer27 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg28 interface{}) interface{} { + return coer27(arg28.(m_SerializeFunctions.ReadProblems)) } }(Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadFramedMessageBody")))) if (_0_valueOrError0).IsFailure() { @@ -917,9 +910,9 @@ func (_static *CompanionStruct_Default___) ReadAndDecryptNonFramedMessageBody(bu _ = res var _0_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{} _ = _0_valueOrError0 - _0_valueOrError0 = (m_MessageBody.Companion_Default___.ReadNonFramedMessageBody(buffer, header)).MapFailure(func(coer29 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { - return func(arg30 interface{}) interface{} { - return coer29(arg30.(m_SerializeFunctions.ReadProblems)) + _0_valueOrError0 = (m_MessageBody.Companion_Default___.ReadNonFramedMessageBody(buffer, header)).MapFailure(func(coer28 func(m_SerializeFunctions.ReadProblems) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} { + return func(arg29 interface{}) interface{} { + return coer28(arg29.(m_SerializeFunctions.ReadProblems)) } }(Companion_Default___.MapSerializeFailure(_dafny.SeqOfString(": ReadNonFramedMessageBody")))) if (_0_valueOrError0).IsFailure() { diff --git a/releases/go/encryption-sdk/EncryptedDataKeys/EncryptedDataKeys.go b/releases/go/encryption-sdk/EncryptedDataKeys/EncryptedDataKeys.go index 3350ed861..72b7843c7 100644 --- a/releases/go/encryption-sdk/EncryptedDataKeys/EncryptedDataKeys.go +++ b/releases/go/encryption-sdk/EncryptedDataKeys/EncryptedDataKeys.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -127,6 +128,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -151,40 +153,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -209,7 +212,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -279,7 +281,7 @@ func (_static *CompanionStruct_Default___) WriteEncryptedDataKeys(edks _dafny.Se _ = _0___accumulator goto TAIL_CALL_START TAIL_CALL_START: - if (_dafny.IntOfUint32((edks).Cardinality())).Sign() == 0 { + if (uint64((edks).Cardinality())) == (uint64(0)) { return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOf(), _0___accumulator) } else { _0___accumulator = _dafny.Companion_Sequence_.Concatenate(Companion_Default___.WriteEncryptedDataKey(m_Seq.Companion_Default___.Last(edks).(m_AwsCryptographyMaterialProvidersTypes.EncryptedDataKey)), _0___accumulator) @@ -342,7 +344,7 @@ func (_static *CompanionStruct_Default___) ReadEncryptedDataKey(buffer m_Seriali func (_static *CompanionStruct_Default___) ReadEncryptedDataKeys(buffer m_SerializeFunctions.ReadableBuffer, accumulator _dafny.Sequence, count uint16, nextEdkStart m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { goto TAIL_CALL_START TAIL_CALL_START: - if (_dafny.IntOfUint16(count)).Cmp(_dafny.IntOfUint32((accumulator).Cardinality())) > 0 { + if (uint64(count)) > (uint64((accumulator).Cardinality())) { var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.ReadEncryptedDataKey(nextEdkStart) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { @@ -386,7 +388,7 @@ func (_static *CompanionStruct_Default___) ReadEncryptedDataKeysSection(buffer m _ = _1_count var _2_edkStart m_SerializeFunctions.ReadableBuffer = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Tail _ = _2_edkStart - if ((maxEdks).Is_Some()) && ((_dafny.IntOfUint16(_1_count)).Cmp(_dafny.IntOfInt64((maxEdks).Dtor_value().(int64))) > 0) { + if ((maxEdks).Is_Some()) && ((int64(_1_count)) > ((maxEdks).Dtor_value().(int64))) { return m_Wrappers.Companion_Result_.Create_Failure_(m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Ciphertext encrypted data keys exceed maxEncryptedDataKeys"))) } else { var _3_valueOrError1 m_Wrappers.Result = Companion_Default___.ReadEncryptedDataKeys(_2_edkStart, _dafny.SeqOf(), _1_count, _2_edkStart) diff --git a/releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go b/releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go index f1949d639..f10316e5e 100644 --- a/releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go +++ b/releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -124,6 +125,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -148,40 +150,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -206,7 +209,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -287,7 +289,7 @@ func (_static *CompanionStruct_Default___) GetEncryptionContext(canonicalEncrypt }() } func (_static *CompanionStruct_Default___) WriteAADSection(ec _dafny.Sequence) _dafny.Sequence { - if (_dafny.IntOfUint32((ec).Cardinality())).Sign() == 0 { + if (uint64((ec).Cardinality())) == (uint64(0)) { return m_SerializeFunctions.Companion_Default___.WriteUint16(uint16(0)) } else { var _0_aad _dafny.Sequence = Companion_Default___.WriteAAD(ec) @@ -296,7 +298,7 @@ func (_static *CompanionStruct_Default___) WriteAADSection(ec _dafny.Sequence) _ } } func (_static *CompanionStruct_Default___) WriteEmptyEcOrWriteAAD(ec _dafny.Sequence) _dafny.Sequence { - if (_dafny.IntOfUint32((ec).Cardinality())).Sign() == 0 { + if (uint64((ec).Cardinality())) == (uint64(0)) { return _dafny.SeqOf() } else { return Companion_Default___.WriteAAD(ec) @@ -306,19 +308,19 @@ func (_static *CompanionStruct_Default___) WriteAAD(ec _dafny.Sequence) _dafny.S return _dafny.Companion_Sequence_.Concatenate(m_SerializeFunctions.Companion_Default___.WriteUint16(uint16((ec).Cardinality())), Companion_Default___.WriteAADPairs(ec)) } func (_static *CompanionStruct_Default___) WriteAADPairs(ec _dafny.Sequence) _dafny.Sequence { - var _0___accumulator _dafny.Sequence = _dafny.SeqOf() - _ = _0___accumulator - goto TAIL_CALL_START -TAIL_CALL_START: - if (_dafny.IntOfUint32((ec).Cardinality())).Sign() == 0 { - return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOf(), _0___accumulator) - } else { - _0___accumulator = _dafny.Companion_Sequence_.Concatenate(Companion_Default___.WriteAADPair(m_Seq.Companion_Default___.Last(ec).(m_SerializableTypes.Pair)), _0___accumulator) - var _in0 _dafny.Sequence = m_Seq.Companion_Default___.DropLast(ec) - _ = _in0 - ec = _in0 - goto TAIL_CALL_START + var ret _dafny.Sequence = _dafny.EmptySeq + _ = ret + var _0_result _dafny.Sequence + _ = _0_result + _0_result = _dafny.SeqOf() + var _hi0 uint64 = uint64((ec).Cardinality()) + _ = _hi0 + for _1_i := uint64(0); _1_i < _hi0; _1_i++ { + _0_result = _dafny.Companion_Sequence_.Concatenate(_0_result, Companion_Default___.WriteAADPair((ec).Select(uint32(_1_i)).(m_SerializableTypes.Pair))) } + ret = _0_result + return ret + return ret } func (_static *CompanionStruct_Default___) WriteAADPair(pair m_SerializableTypes.Pair) _dafny.Sequence { return _dafny.Companion_Sequence_.Concatenate(m_SerializeFunctions.Companion_Default___.WriteShortLengthSeq((pair).Dtor_key().(_dafny.Sequence)), m_SerializeFunctions.Companion_Default___.WriteShortLengthSeq((pair).Dtor_value().(_dafny.Sequence))) @@ -367,7 +369,7 @@ func (_static *CompanionStruct_Default___) ReadAADPair(buffer m_SerializeFunctio func (_static *CompanionStruct_Default___) ReadAADPairs(buffer m_SerializeFunctions.ReadableBuffer, accumulator _dafny.Sequence, keys _dafny.Set, count uint16, nextPair m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { goto TAIL_CALL_START TAIL_CALL_START: - if (_dafny.IntOfUint16(count)).Cmp(_dafny.IntOfUint32((accumulator).Cardinality())) > 0 { + if (count) > (uint16((accumulator).Cardinality())) { var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.ReadAADPair(nextPair) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { @@ -384,7 +386,7 @@ TAIL_CALL_START: if (_3_valueOrError1).IsFailure() { return (_3_valueOrError1).PropagateFailure() } else { - var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((((_2_newPos).Dtor_start()).Minus((buffer).Dtor_start())).Cmp(m_SerializableTypes.Companion_Default___.ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH()) < 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Encryption Context exceeds maximum length."))) + var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((((_2_newPos).Dtor_start()) >= ((buffer).Dtor_start())) && ((((_2_newPos).Dtor_start())-(func() uint64 { return ((buffer).Dtor_start()) })()) < (m_SerializableTypes.Companion_Default___.ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH())), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Encryption Context exceeds maximum length."))) _ = _4_valueOrError2 if (_4_valueOrError2).IsFailure() { return (_4_valueOrError2).PropagateFailure() @@ -466,7 +468,7 @@ func (_static *CompanionStruct_Default___) ReadAADSection(buffer m_SerializeFunc _ = _2_empty return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_2_empty, (_1_length).Dtor_tail())) } else { - var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((((_1_length).Dtor_tail()).Dtor_start()).Plus(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16)))).Cmp(_dafny.IntOfUint32((((_1_length).Dtor_tail()).Dtor_bytes()).Cardinality())) <= 0, m_SerializeFunctions.Companion_ReadProblems_.Create_MoreNeeded_((((_1_length).Dtor_tail()).Dtor_start()).Plus(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16))))) + var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((m_StandardLibrary_MemoryMath.Companion_Default___.Add(((_1_length).Dtor_tail()).Dtor_start(), uint64((_1_length).Dtor_data().(uint16)))) <= (uint64((((_1_length).Dtor_tail()).Dtor_bytes()).Cardinality())), m_SerializeFunctions.Companion_ReadProblems_.Create_MoreNeeded_(m_StandardLibrary_MemoryMath.Companion_Default___.Add(((_1_length).Dtor_tail()).Dtor_start(), uint64((_1_length).Dtor_data().(uint16))))) _ = _3_valueOrError1 if (_3_valueOrError1).IsFailure() { return (_3_valueOrError1).PropagateFailure() @@ -501,7 +503,7 @@ func (_static *CompanionStruct_Default___) ReadAADSection(buffer m_SerializeFunc } else { var _10_aad m_SerializeFunctions.SuccessfulRead = (_9_valueOrError5).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _10_aad - var _11_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((((_10_aad).Dtor_tail()).Dtor_start()).Minus(((_1_length).Dtor_tail()).Dtor_start())).Cmp(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16))) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("AAD Length did not match stored length."))) + var _11_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((((_10_aad).Dtor_tail()).Dtor_start()) >= (((_1_length).Dtor_tail()).Dtor_start())) && (((((_10_aad).Dtor_tail()).Dtor_start())-(func() uint64 { return (((_1_length).Dtor_tail()).Dtor_start()) })()) == (uint64((_1_length).Dtor_data().(uint16)))), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("AAD Length did not match stored length."))) _ = _11_valueOrError6 if (_11_valueOrError6).IsFailure() { return (_11_valueOrError6).PropagateFailure() diff --git a/releases/go/encryption-sdk/Frames/Frames.go b/releases/go/encryption-sdk/Frames/Frames.go index 1ee4ffa4e..bec6e3615 100644 --- a/releases/go/encryption-sdk/Frames/Frames.go +++ b/releases/go/encryption-sdk/Frames/Frames.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -131,6 +132,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -155,40 +157,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -213,7 +216,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -296,21 +298,21 @@ func (_static *CompanionStruct_Default___) ReadRegularFrame(buffer m_SerializeFu if (_2_valueOrError1).IsFailure() { return (_2_valueOrError1).PropagateFailure() } else { - var _3_valueOrError2 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_1_sequenceNumber).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) + var _3_valueOrError2 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_1_sequenceNumber).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) _ = _3_valueOrError2 if (_3_valueOrError2).IsFailure() { return (_3_valueOrError2).PropagateFailure() } else { var _4_iv m_SerializeFunctions.SuccessfulRead = (_3_valueOrError2).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _4_iv - var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_4_iv).Dtor_tail(), _dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength())) + var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_4_iv).Dtor_tail(), uint64(((header).Dtor_body()).Dtor_frameLength())) _ = _5_valueOrError3 if (_5_valueOrError3).IsFailure() { return (_5_valueOrError3).PropagateFailure() } else { var _6_encContent m_SerializeFunctions.SuccessfulRead = (_5_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _6_encContent - var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_6_encContent).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) + var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_6_encContent).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) _ = _7_valueOrError4 if (_7_valueOrError4).IsFailure() { return (_7_valueOrError4).PropagateFailure() @@ -349,7 +351,7 @@ func (_static *CompanionStruct_Default___) ReadFinalFrame(buffer m_SerializeFunc } else { var _4_sequenceNumber m_SerializeFunctions.SuccessfulRead = (_3_valueOrError2).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _4_sequenceNumber - var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_4_sequenceNumber).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) + var _5_valueOrError3 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_4_sequenceNumber).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) _ = _5_valueOrError3 if (_5_valueOrError3).IsFailure() { return (_5_valueOrError3).PropagateFailure() @@ -375,7 +377,7 @@ func (_static *CompanionStruct_Default___) ReadFinalFrame(buffer m_SerializeFunc } else { var _11_encContent m_SerializeFunctions.SuccessfulRead = (_10_valueOrError6).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _11_encContent - var _12_valueOrError7 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_11_encContent).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) + var _12_valueOrError7 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_11_encContent).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) _ = _12_valueOrError7 if (_12_valueOrError7).IsFailure() { return (_12_valueOrError7).PropagateFailure() @@ -395,7 +397,7 @@ func (_static *CompanionStruct_Default___) ReadFinalFrame(buffer m_SerializeFunc } } func (_static *CompanionStruct_Default___) ReadNonFrame(buffer m_SerializeFunctions.ReadableBuffer, header m_Header.HeaderInfo) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(m_SerializableTypes.Companion_Default___.GetIvLength((header).Dtor_suite()))) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -409,7 +411,7 @@ func (_static *CompanionStruct_Default___) ReadNonFrame(buffer m_SerializeFuncti } else { var _3_contentLength m_SerializeFunctions.SuccessfulRead = (_2_valueOrError1).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _3_contentLength - var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint64((_3_contentLength).Dtor_data().(uint64))).Cmp(Companion_Default___.SAFE__MAX__ENCRYPT()) < 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Frame exceeds AES-GCM cryptographic safety for a single key/iv."))) + var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_3_contentLength).Dtor_data().(uint64)) < (Companion_Default___.SAFE__MAX__ENCRYPT()), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Frame exceeds AES-GCM cryptographic safety for a single key/iv."))) _ = _4_valueOrError2 if (_4_valueOrError2).IsFailure() { return (_4_valueOrError2).PropagateFailure() @@ -421,7 +423,7 @@ func (_static *CompanionStruct_Default___) ReadNonFrame(buffer m_SerializeFuncti } else { var _6_encContent m_SerializeFunctions.SuccessfulRead = (_5_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _6_encContent - var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_6_encContent).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) + var _7_valueOrError4 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_6_encContent).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetTagLength((header).Dtor_suite()))) _ = _7_valueOrError4 if (_7_valueOrError4).IsFailure() { return (_7_valueOrError4).PropagateFailure() @@ -440,8 +442,8 @@ func (_static *CompanionStruct_Default___) ReadNonFrame(buffer m_SerializeFuncti func (_static *CompanionStruct_Default___) ENDFRAME__SEQUENCE__NUMBER() uint32 { return uint32(4294967295) } -func (_static *CompanionStruct_Default___) SAFE__MAX__ENCRYPT() _dafny.Int { - return _dafny.IntOfInt64(68719476704) +func (_static *CompanionStruct_Default___) SAFE__MAX__ENCRYPT() uint64 { + return uint64(68719476704) } func (_static *CompanionStruct_Default___) START__SEQUENCE__NUMBER() uint32 { return uint32(1) diff --git a/releases/go/encryption-sdk/Header/Header.go b/releases/go/encryption-sdk/Header/Header.go index 7942b29a7..317ee6133 100644 --- a/releases/go/encryption-sdk/Header/Header.go +++ b/releases/go/encryption-sdk/Header/Header.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -130,6 +131,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -154,40 +156,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -212,7 +215,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -279,7 +281,7 @@ func (_this *Default__) ParentTraits_() []*_dafny.TraitID { var _ _dafny.TraitOffspring = &Default__{} func (_static *CompanionStruct_Default___) HeaderVersionSupportsCommitment_q(suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, body m_HeaderTypes.HeaderBody) bool { - return (!(((suite).Dtor_commitment()).Is_HKDF()) || (((body).Is_V2HeaderBody()) && ((_dafny.IntOfUint32(((body).Dtor_suiteData()).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength())) == 0))) && (!(!(((suite).Dtor_commitment()).Is_HKDF())) || ((true) && ((body).Is_V1HeaderBody()))) + return (!(((suite).Dtor_commitment()).Is_HKDF()) || (((body).Is_V2HeaderBody()) && ((uint64(((body).Dtor_suiteData()).Cardinality())) == (uint64((((suite).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength()))))) && (!(!(((suite).Dtor_commitment()).Is_HKDF())) || ((true) && ((body).Is_V1HeaderBody()))) } func (_static *CompanionStruct_Default___) ReadHeaderBody(buffer m_SerializeFunctions.ReadableBuffer, maxEdks m_Wrappers.Option, mpl *m_MaterialProviders.MaterialProvidersClient) m_Wrappers.Result { var _0_valueOrError0 m_Wrappers.Result = m_SharedHeaderFunctions.Companion_Default___.ReadMessageFormatVersion(buffer) diff --git a/releases/go/encryption-sdk/HeaderAuth/HeaderAuth.go b/releases/go/encryption-sdk/HeaderAuth/HeaderAuth.go index 58a9b9366..0dbc7a38f 100644 --- a/releases/go/encryption-sdk/HeaderAuth/HeaderAuth.go +++ b/releases/go/encryption-sdk/HeaderAuth/HeaderAuth.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -129,6 +130,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -153,40 +155,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -211,7 +214,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -300,14 +302,14 @@ func (_static *CompanionStruct_Default___) WriteHeaderAuthTag(headerAuth m_Heade } } func (_static *CompanionStruct_Default___) ReadHeaderAuthTagV1(buffer m_SerializeFunctions.ReadableBuffer, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength(suite))) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(m_SerializableTypes.Companion_Default___.GetIvLength(suite))) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() } else { var _1_headerIv m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _1_headerIv - var _2_valueOrError1 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_1_headerIv).Dtor_tail(), _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength(suite))) + var _2_valueOrError1 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_1_headerIv).Dtor_tail(), uint64(m_SerializableTypes.Companion_Default___.GetTagLength(suite))) _ = _2_valueOrError1 if (_2_valueOrError1).IsFailure() { return (_2_valueOrError1).PropagateFailure() @@ -321,24 +323,18 @@ func (_static *CompanionStruct_Default___) ReadHeaderAuthTagV1(buffer m_Serializ } } func (_static *CompanionStruct_Default___) ReadHeaderAuthTagV2(buffer m_SerializeFunctions.ReadableBuffer, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) m_Wrappers.Result { - var _0_headerIv _dafny.Sequence = _dafny.SeqCreate((_dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength(suite))).Uint32(), func(coer6 func(_dafny.Int) uint8) func(_dafny.Int) interface{} { - return func(arg7 _dafny.Int) interface{} { - return coer6(arg7) - } - }(func(_1___v1 _dafny.Int) uint8 { - return uint8(0) - })) + var _0_headerIv _dafny.Sequence = m_SerializableTypes.Companion_Default___.GetIvLengthZeros(suite) _ = _0_headerIv - var _2_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetTagLength(suite))) - _ = _2_valueOrError0 - if (_2_valueOrError0).IsFailure() { - return (_2_valueOrError0).PropagateFailure() + var _1_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(m_SerializableTypes.Companion_Default___.GetTagLength(suite))) + _ = _1_valueOrError0 + if (_1_valueOrError0).IsFailure() { + return (_1_valueOrError0).PropagateFailure() } else { - var _3_headerAuthTag m_SerializeFunctions.SuccessfulRead = (_2_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) - _ = _3_headerAuthTag - var _4_auth m_HeaderTypes.HeaderAuth = m_HeaderTypes.Companion_HeaderAuth_.Create_AESMac_(_0_headerIv, (_3_headerAuthTag).Dtor_data().(_dafny.Sequence)) - _ = _4_auth - return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_4_auth, (_3_headerAuthTag).Dtor_tail())) + var _2_headerAuthTag m_SerializeFunctions.SuccessfulRead = (_1_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) + _ = _2_headerAuthTag + var _3_auth m_HeaderTypes.HeaderAuth = m_HeaderTypes.Companion_HeaderAuth_.Create_AESMac_(_0_headerIv, (_2_headerAuthTag).Dtor_data().(_dafny.Sequence)) + _ = _3_auth + return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_3_auth, (_2_headerAuthTag).Dtor_tail())) } } func (_static *CompanionStruct_Default___) ReadHeaderAuthTag(buffer m_SerializeFunctions.ReadableBuffer, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) m_Wrappers.Result { diff --git a/releases/go/encryption-sdk/HeaderTypes/HeaderTypes.go b/releases/go/encryption-sdk/HeaderTypes/HeaderTypes.go index 954153735..753ef59e0 100644 --- a/releases/go/encryption-sdk/HeaderTypes/HeaderTypes.go +++ b/releases/go/encryption-sdk/HeaderTypes/HeaderTypes.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -124,6 +125,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -148,40 +150,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -206,7 +209,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -266,11 +268,11 @@ func (_this *Default__) ParentTraits_() []*_dafny.TraitID { var _ _dafny.TraitOffspring = &Default__{} -func (_static *CompanionStruct_Default___) MESSAGE__ID__LEN__V1() _dafny.Int { - return _dafny.IntOfInt64(16) +func (_static *CompanionStruct_Default___) MESSAGE__ID__LEN__V1() uint64 { + return uint64(16) } -func (_static *CompanionStruct_Default___) MESSAGE__ID__LEN__V2() _dafny.Int { - return _dafny.IntOfInt64(32) +func (_static *CompanionStruct_Default___) MESSAGE__ID__LEN__V2() uint64 { + return uint64(32) } // End of class Default__ @@ -424,7 +426,7 @@ func (_static CompanionStruct_MessageFormatVersion_) Get(x _dafny.Sequence) m_Wr return (_0_valueOrError0).PropagateFailure() } else { return m_Wrappers.Companion_Result_.Create_Success_(func() MessageFormatVersion { - var _source0 uint8 = (x).Select(0).(uint8) + var _source0 uint8 = (x).Select(uint32(uint32(0))).(uint8) _ = _source0 { if (_source0) == (uint8(1)) { @@ -501,13 +503,13 @@ type HeaderBody_V1HeaderBody struct { EncryptionContext _dafny.Sequence EncryptedDataKeys _dafny.Sequence ContentType ContentType - HeaderIvLength _dafny.Int + HeaderIvLength uint64 FrameLength uint32 } func (HeaderBody_V1HeaderBody) isHeaderBody() {} -func (CompanionStruct_HeaderBody_) Create_V1HeaderBody_(MessageType MessageType, AlgorithmSuite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, MessageId _dafny.Sequence, EncryptionContext _dafny.Sequence, EncryptedDataKeys _dafny.Sequence, ContentType ContentType, HeaderIvLength _dafny.Int, FrameLength uint32) HeaderBody { +func (CompanionStruct_HeaderBody_) Create_V1HeaderBody_(MessageType MessageType, AlgorithmSuite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, MessageId _dafny.Sequence, EncryptionContext _dafny.Sequence, EncryptedDataKeys _dafny.Sequence, ContentType ContentType, HeaderIvLength uint64, FrameLength uint32) HeaderBody { return HeaderBody{HeaderBody_V1HeaderBody{MessageType, AlgorithmSuite, MessageId, EncryptionContext, EncryptedDataKeys, ContentType, HeaderIvLength, FrameLength}} } @@ -538,7 +540,7 @@ func (_this HeaderBody) Is_V2HeaderBody() bool { } func (CompanionStruct_HeaderBody_) Default() HeaderBody { - return Companion_HeaderBody_.Create_V1HeaderBody_(Companion_MessageType_.Default(), m_AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteInfo_.Default(), _dafny.EmptySeq, _dafny.EmptySeq, _dafny.EmptySeq, Companion_ContentType_.Default(), _dafny.Zero, uint32(0)) + return Companion_HeaderBody_.Create_V1HeaderBody_(Companion_MessageType_.Default(), m_AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteInfo_.Default(), _dafny.EmptySeq, _dafny.EmptySeq, _dafny.EmptySeq, Companion_ContentType_.Default(), uint64(0), uint32(0)) } func (_this HeaderBody) Dtor_messageType() MessageType { @@ -590,7 +592,7 @@ func (_this HeaderBody) Dtor_contentType() ContentType { } } -func (_this HeaderBody) Dtor_headerIvLength() _dafny.Int { +func (_this HeaderBody) Dtor_headerIvLength() uint64 { return _this.Get_().(HeaderBody_V1HeaderBody).HeaderIvLength } @@ -631,7 +633,7 @@ func (_this HeaderBody) Equals(other HeaderBody) bool { case HeaderBody_V1HeaderBody: { data2, ok := other.Get_().(HeaderBody_V1HeaderBody) - return ok && data1.MessageType.Equals(data2.MessageType) && data1.AlgorithmSuite.Equals(data2.AlgorithmSuite) && data1.MessageId.Equals(data2.MessageId) && data1.EncryptionContext.Equals(data2.EncryptionContext) && data1.EncryptedDataKeys.Equals(data2.EncryptedDataKeys) && data1.ContentType.Equals(data2.ContentType) && data1.HeaderIvLength.Cmp(data2.HeaderIvLength) == 0 && data1.FrameLength == data2.FrameLength + return ok && data1.MessageType.Equals(data2.MessageType) && data1.AlgorithmSuite.Equals(data2.AlgorithmSuite) && data1.MessageId.Equals(data2.MessageId) && data1.EncryptionContext.Equals(data2.EncryptionContext) && data1.EncryptedDataKeys.Equals(data2.EncryptedDataKeys) && data1.ContentType.Equals(data2.ContentType) && data1.HeaderIvLength == data2.HeaderIvLength && data1.FrameLength == data2.FrameLength } case HeaderBody_V2HeaderBody: { @@ -1107,5 +1109,5 @@ func (_this type_MessageId_) String() string { func (_this *CompanionStruct_MessageId_) Is_(__source _dafny.Sequence) bool { var _1_x _dafny.Sequence = (__source) _ = _1_x - return ((_dafny.IntOfUint32((_1_x).Cardinality())).Cmp(Companion_Default___.MESSAGE__ID__LEN__V1()) == 0) || ((_dafny.IntOfUint32((_1_x).Cardinality())).Cmp(Companion_Default___.MESSAGE__ID__LEN__V2()) == 0) + return ((_dafny.IntOfUint32((_1_x).Cardinality())).Cmp(_dafny.IntOfUint64(Companion_Default___.MESSAGE__ID__LEN__V1())) == 0) || ((_dafny.IntOfUint32((_1_x).Cardinality())).Cmp(_dafny.IntOfUint64(Companion_Default___.MESSAGE__ID__LEN__V2())) == 0) } diff --git a/releases/go/encryption-sdk/KeyDerivation/KeyDerivation.go b/releases/go/encryption-sdk/KeyDerivation/KeyDerivation.go index a824a717f..515af36b0 100644 --- a/releases/go/encryption-sdk/KeyDerivation/KeyDerivation.go +++ b/releases/go/encryption-sdk/KeyDerivation/KeyDerivation.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -133,6 +134,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -157,40 +159,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -215,7 +218,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -462,7 +464,7 @@ func (_static *CompanionStruct_Default___) DeriveKeys(messageId _dafny.Sequence, } var _2_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _2_valueOrError1 - _2_valueOrError1 = m_Wrappers.Companion_Default___.Need(((m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)) == ((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength())) && ((_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())) == 0), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Invalid Materials"))) + _2_valueOrError1 = m_Wrappers.Companion_Default___.Need(((m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)) == ((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength())) && ((int32((plaintextKey).Cardinality())) == ((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Invalid Materials"))) if (_2_valueOrError1).IsFailure() { res = (_2_valueOrError1).PropagateFailure() return res @@ -495,14 +497,14 @@ func (_static *CompanionStruct_Default___) DeriveKeys(messageId _dafny.Sequence, if _source0.Is_IDENTITY() { var _6_i m_AwsCryptographyMaterialProvidersTypes.IDENTITY = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm_IDENTITY).IDENTITY _ = _6_i - return (_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32(m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite))) == 0 + return (int32((plaintextKey).Cardinality())) == (m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)) } } { if _source0.Is_HKDF() { var _7_hkdf m_AwsCryptographyMaterialProvidersTypes.HKDF = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm_HKDF).HKDF _ = _7_hkdf - return ((_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())) == 0) && (((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength()) == (m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite))) + return ((int32((plaintextKey).Cardinality())) == ((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())) && (((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength()) == (m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite))) } } { diff --git a/releases/go/encryption-sdk/MessageBody/MessageBody.go b/releases/go/encryption-sdk/MessageBody/MessageBody.go index bb055886d..d8c281c07 100644 --- a/releases/go/encryption-sdk/MessageBody/MessageBody.go +++ b/releases/go/encryption-sdk/MessageBody/MessageBody.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -133,6 +134,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -157,40 +159,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -215,7 +218,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -301,22 +303,30 @@ func (_static *CompanionStruct_Default___) BodyAADContentTypeString(bc BodyAADCo } } func (_static *CompanionStruct_Default___) IVSeq(suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, sequenceNumber uint32) _dafny.Sequence { - return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqCreate(((_dafny.IntOfUint8(m_SerializableTypes.Companion_Default___.GetIvLength(suite))).Minus(_dafny.IntOfInt64(4))).Uint32(), func(coer7 func(_dafny.Int) uint8) func(_dafny.Int) interface{} { - return func(arg8 _dafny.Int) interface{} { - return coer7(arg8) - } - }(func(_0___v0 _dafny.Int) uint8 { - return uint8(0) - })), m_StandardLibrary_UInt.Companion_Default___.UInt32ToSeq(sequenceNumber)) + var _0_len uint8 = m_SerializableTypes.Companion_Default___.GetIvLength(suite) + _ = _0_len + var _1_num _dafny.Sequence = m_StandardLibrary_UInt.Companion_Default___.UInt32ToSeq(sequenceNumber) + _ = _1_num + if (_0_len) == (uint8(12)) { + return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOf(uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0)), _1_num) + } else { + return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqCreate(((_dafny.IntOfUint8(_0_len)).Minus(_dafny.IntOfInt64(4))).Uint32(), func(coer7 func(_dafny.Int) uint8) func(_dafny.Int) interface{} { + return func(arg8 _dafny.Int) interface{} { + return coer7(arg8) + } + }(func(_2___v0 _dafny.Int) uint8 { + return uint8(0) + })), _1_num) + } } func (_static *CompanionStruct_Default___) EncryptMessageBody(plaintext _dafny.Sequence, header m_Header.HeaderInfo, key _dafny.Sequence, crypto *m_AtomicPrimitives.AtomicPrimitivesClient) m_Wrappers.Result { var result m_Wrappers.Result = m_Wrappers.Result{} _ = result - var _0_n _dafny.Int + var _0_n uint64 _ = _0_n var _1_sequenceNumber uint32 _ = _1_sequenceNumber - var _rhs0 _dafny.Int = _dafny.Zero + var _rhs0 uint64 = uint64(0) _ = _rhs0 var _rhs1 uint32 = Companion_Default___.START__SEQUENCE__NUMBER() _ = _rhs1 @@ -325,7 +335,7 @@ func (_static *CompanionStruct_Default___) EncryptMessageBody(plaintext _dafny.S var _2_regularFrames _dafny.Sequence _ = _2_regularFrames _2_regularFrames = _dafny.SeqOf() - for ((_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength()))).Cmp(_dafny.IntOfUint32((plaintext).Cardinality())) < 0 { + for (m_StandardLibrary_MemoryMath.Companion_Default___.Add(_0_n, uint64(((header).Dtor_body()).Dtor_frameLength()))) < (uint64((plaintext).Cardinality())) { var _3_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() _ = _3_valueOrError0 _3_valueOrError0 = m_Wrappers.Companion_Default___.Need((_1_sequenceNumber) < (Companion_Default___.ENDFRAME__SEQUENCE__NUMBER()), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("too many frames"))) @@ -335,7 +345,7 @@ func (_static *CompanionStruct_Default___) EncryptMessageBody(plaintext _dafny.S } var _4_plaintextFrame _dafny.Sequence _ = _4_plaintextFrame - _4_plaintextFrame = (plaintext).Subsequence((_0_n).Uint32(), ((_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength()))).Uint32()) + _4_plaintextFrame = (plaintext).Subsequence(uint32(_0_n), uint32(m_StandardLibrary_MemoryMath.Companion_Default___.Add(_0_n, uint64(((header).Dtor_body()).Dtor_frameLength())))) var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Result{} _ = _5_valueOrError1 var _out0 m_Wrappers.Result @@ -350,14 +360,14 @@ func (_static *CompanionStruct_Default___) EncryptMessageBody(plaintext _dafny.S _ = _6_regularFrame _6_regularFrame = (_5_valueOrError1).Extract().(m_Frames.Frame) _2_regularFrames = _dafny.Companion_Sequence_.Concatenate(_2_regularFrames, _dafny.SeqOf(_6_regularFrame)) - _0_n = (_0_n).Plus(_dafny.IntOfUint32(((header).Dtor_body()).Dtor_frameLength())) + _0_n = m_StandardLibrary_MemoryMath.Companion_Default___.Add(_0_n, uint64(((header).Dtor_body()).Dtor_frameLength())) _1_sequenceNumber = (_1_sequenceNumber) + (uint32(1)) } var _7_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{} _ = _7_valueOrError2 var _out1 m_Wrappers.Result _ = _out1 - _out1 = Companion_Default___.EncryptFinalFrame(key, header, (plaintext).Drop((_0_n).Uint32()), _1_sequenceNumber, crypto) + _out1 = Companion_Default___.EncryptFinalFrame(key, header, (plaintext).Drop(uint32(_0_n)), _1_sequenceNumber, crypto) _7_valueOrError2 = _out1 if (_7_valueOrError2).IsFailure() { result = (_7_valueOrError2).PropagateFailure() @@ -457,14 +467,14 @@ func (_static *CompanionStruct_Default___) DecryptFramedMessageBody(body FramedM var _0_plaintext _dafny.Sequence _ = _0_plaintext _0_plaintext = _dafny.SeqOf() - var _hi0 _dafny.Int = _dafny.IntOfUint32(((body).Dtor_regularFrames()).Cardinality()) + var _hi0 uint64 = uint64(((body).Dtor_regularFrames()).Cardinality()) _ = _hi0 - for _1_i := _dafny.Zero; _1_i.Cmp(_hi0) < 0; _1_i = _1_i.Plus(_dafny.One) { + for _1_i := uint64(0); _1_i < _hi0; _1_i++ { var _2_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) _ = _2_valueOrError0 var _out0 m_Wrappers.Result _ = _out0 - _out0 = Companion_Default___.DecryptFrame(((body).Dtor_regularFrames()).Select((_1_i).Uint32()).(m_Frames.Frame), key, crypto) + _out0 = Companion_Default___.DecryptFrame(((body).Dtor_regularFrames()).Select(uint32(_1_i)).(m_Frames.Frame), key, crypto) _2_valueOrError0 = _out0 if (_2_valueOrError0).IsFailure() { res = (_2_valueOrError0).PropagateFailure() @@ -570,19 +580,19 @@ func (_static *CompanionStruct_Default___) WriteFramedMessageBody(body FramedMes return _dafny.Companion_Sequence_.Concatenate(Companion_Default___.WriteMessageRegularFrames((body).Dtor_regularFrames()), m_Frames.Companion_Default___.WriteFinalFrame((body).Dtor_finalFrame())) } func (_static *CompanionStruct_Default___) WriteMessageRegularFrames(frames _dafny.Sequence) _dafny.Sequence { - var _0___accumulator _dafny.Sequence = _dafny.SeqOf() - _ = _0___accumulator - goto TAIL_CALL_START -TAIL_CALL_START: - if (_dafny.IntOfUint32((frames).Cardinality())).Sign() == 0 { - return _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOf(), _0___accumulator) - } else { - _0___accumulator = _dafny.Companion_Sequence_.Concatenate(m_Frames.Companion_Default___.WriteRegularFrame(m_Seq.Companion_Default___.Last(frames).(m_Frames.Frame)), _0___accumulator) - var _in0 _dafny.Sequence = m_Seq.Companion_Default___.DropLast(frames) - _ = _in0 - frames = _in0 - goto TAIL_CALL_START + var ret _dafny.Sequence = _dafny.EmptySeq + _ = ret + var _0_result _dafny.Sequence + _ = _0_result + _0_result = _dafny.SeqOf() + var _hi0 uint64 = uint64((frames).Cardinality()) + _ = _hi0 + for _1_i := uint64(0); _1_i < _hi0; _1_i++ { + _0_result = _dafny.Companion_Sequence_.Concatenate(_0_result, m_Frames.Companion_Default___.WriteRegularFrame((frames).Select(uint32(_1_i)).(m_Frames.Frame))) } + ret = _0_result + return ret + return ret } func (_static *CompanionStruct_Default___) ReadFramedMessageBody(buffer m_SerializeFunctions.ReadableBuffer, header m_Header.HeaderInfo, regularFrames _dafny.Sequence, continuation m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { goto TAIL_CALL_START @@ -602,7 +612,7 @@ TAIL_CALL_START: } else { var _3_regularFrame m_SerializeFunctions.SuccessfulRead = (_2_valueOrError1).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _3_regularFrame - var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_3_regularFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())).Cmp((_dafny.IntOfUint32((regularFrames).Cardinality())).Plus(_dafny.One)) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order."))) + var _4_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64(((_3_regularFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())) == ((uint64((regularFrames).Cardinality()))+(uint64(1))), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order."))) _ = _4_valueOrError2 if (_4_valueOrError2).IsFailure() { return (_4_valueOrError2).PropagateFailure() @@ -632,7 +642,7 @@ TAIL_CALL_START: } else { var _7_finalFrame m_SerializeFunctions.SuccessfulRead = (_6_valueOrError3).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _7_finalFrame - var _8_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_7_finalFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())).Cmp((_dafny.IntOfUint32((regularFrames).Cardinality())).Plus(_dafny.One)) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order."))) + var _8_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64(((_7_finalFrame).Dtor_data().(m_Frames.Frame)).Dtor_seqNum())) == ((uint64((regularFrames).Cardinality()))+(uint64(1))), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Sequence number out of order."))) _ = _8_valueOrError4 if (_8_valueOrError4).IsFailure() { return (_8_valueOrError4).PropagateFailure() diff --git a/releases/go/encryption-sdk/SerializableTypes/SerializableTypes.go b/releases/go/encryption-sdk/SerializableTypes/SerializableTypes.go index 89241fdfb..e22a342f6 100644 --- a/releases/go/encryption-sdk/SerializableTypes/SerializableTypes.go +++ b/releases/go/encryption-sdk/SerializableTypes/SerializableTypes.go @@ -102,6 +102,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -123,6 +124,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -147,40 +149,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -205,7 +208,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -266,7 +268,7 @@ func (_static *CompanionStruct_Default___) IsESDKEncryptedDataKey(edk m_AwsCrypt return (((m_StandardLibrary_UInt.Companion_Default___.HasUint16Len((edk).Dtor_keyProviderId())) && (m_UTF8.Companion_Default___.ValidUTF8Seq((edk).Dtor_keyProviderId()))) && (m_StandardLibrary_UInt.Companion_Default___.HasUint16Len((edk).Dtor_keyProviderInfo()))) && (m_StandardLibrary_UInt.Companion_Default___.HasUint16Len((edk).Dtor_ciphertext())) } func (_static *CompanionStruct_Default___) IsESDKEncryptionContext(ec _dafny.Map) bool { - return ((((ec).Cardinality()).Cmp(m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()) < 0) && ((Companion_Default___.Length(ec)).Cmp(Companion_Default___.ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH()) < 0)) && (_dafny.Quantifier(((_dafny.MultiSetFromSet((ec).Keys())).Union(_dafny.MultiSetFromSet((ec).Values()))).UniqueElements(), true, func(_forall_var_0 _dafny.Sequence) bool { + return (((uint64((ec).CardinalityInt())) < ((m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()).Uint64())) && ((Companion_Default___.Length(ec)) < (Companion_Default___.ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH()))) && (_dafny.Quantifier(((_dafny.MultiSetFromSet((ec).Keys())).Union(_dafny.MultiSetFromSet((ec).Values()))).UniqueElements(), true, func(_forall_var_0 _dafny.Sequence) bool { var _0_element _dafny.Sequence _0_element = interface{}(_forall_var_0).(_dafny.Sequence) if m_UTF8.Companion_ValidUTF8Bytes_.Is_(_0_element) { @@ -285,6 +287,21 @@ func (_static *CompanionStruct_Default___) GetIvLength(a m_AwsCryptographyMateri return uint8((_0_e).Dtor_ivLength()) } } +func (_static *CompanionStruct_Default___) GetIvLengthZeros(a m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) _dafny.Sequence { + var _0_len uint8 = Companion_Default___.GetIvLength(a) + _ = _0_len + if (_0_len) == (uint8(12)) { + return _dafny.SeqOf(uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0), uint8(0)) + } else { + return _dafny.SeqCreate(uint32(_0_len), func(coer0 func(_dafny.Int) uint8) func(_dafny.Int) interface{} { + return func(arg0 _dafny.Int) interface{} { + return coer0(arg0) + } + }(func(_1___v0 _dafny.Int) uint8 { + return uint8(0) + })) + } +} func (_static *CompanionStruct_Default___) GetTagLength(a m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) uint8 { var _source0 m_AwsCryptographyMaterialProvidersTypes.Encrypt = (a).Dtor_encrypt() _ = _source0 @@ -303,9 +320,9 @@ func (_static *CompanionStruct_Default___) GetEncryptKeyLength(a m_AwsCryptograp return (_0_e).Dtor_keyLength() } } -func (_static *CompanionStruct_Default___) Length(encryptionContext _dafny.Map) _dafny.Int { - if ((encryptionContext).Cardinality()).Sign() == 0 { - return _dafny.Zero +func (_static *CompanionStruct_Default___) Length(encryptionContext _dafny.Map) uint64 { + if (uint64((encryptionContext).CardinalityInt())) == (uint64(0)) { + return uint64(0) } else { var _0_pairs _dafny.Sequence = Companion_Default___.GetCanonicalLinearPairs(encryptionContext) _ = _0_pairs @@ -313,15 +330,15 @@ func (_static *CompanionStruct_Default___) Length(encryptionContext _dafny.Map) } } func (_static *CompanionStruct_Default___) GetCanonicalLinearPairs(encryptionContext _dafny.Map) _dafny.Sequence { - var _0_keys _dafny.Sequence = m_SortedSets.SetToOrderedSequence2((encryptionContext).Keys(), func(coer0 func(uint8, uint8) bool) func(interface{}, interface{}) bool { - return func(arg0 interface{}, arg1 interface{}) bool { - return coer0(arg0.(uint8), arg1.(uint8)) + var _0_keys _dafny.Sequence = m_SortedSets.SetToOrderedSequence2((encryptionContext).Keys(), func(coer1 func(uint8, uint8) bool) func(interface{}, interface{}) bool { + return func(arg1 interface{}, arg2 interface{}) bool { + return coer1(arg1.(uint8), arg2.(uint8)) } }(m_StandardLibrary_UInt.Companion_Default___.UInt8Less)) _ = _0_keys - return _dafny.SeqCreate((_dafny.IntOfUint32((_0_keys).Cardinality())).Uint32(), func(coer1 func(_dafny.Int) Pair) func(_dafny.Int) interface{} { - return func(arg2 _dafny.Int) interface{} { - return coer1(arg2) + return _dafny.SeqCreate((_dafny.IntOfUint32((_0_keys).Cardinality())).Uint32(), func(coer2 func(_dafny.Int) Pair) func(_dafny.Int) interface{} { + return func(arg3 _dafny.Int) interface{} { + return coer2(arg3) } }((func(_1_keys _dafny.Sequence, _2_encryptionContext _dafny.Map) func(_dafny.Int) Pair { return func(_3_i _dafny.Int) Pair { @@ -329,26 +346,26 @@ func (_static *CompanionStruct_Default___) GetCanonicalLinearPairs(encryptionCon } })(_0_keys, encryptionContext))) } -func (_static *CompanionStruct_Default___) LinearLength(pairs _dafny.Sequence) _dafny.Int { - var _0___accumulator _dafny.Int = _dafny.Zero - _ = _0___accumulator - goto TAIL_CALL_START -TAIL_CALL_START: - if (_dafny.IntOfUint32((pairs).Cardinality())).Sign() == 0 { - return (_dafny.Zero).Plus(_0___accumulator) - } else { - _0___accumulator = (Companion_Default___.PairLength(m_Seq.Companion_Default___.Last(pairs).(Pair))).Plus(_0___accumulator) - var _in0 _dafny.Sequence = m_Seq.Companion_Default___.DropLast(pairs) - _ = _in0 - pairs = _in0 - goto TAIL_CALL_START +func (_static *CompanionStruct_Default___) LinearLength(pairs _dafny.Sequence) uint64 { + var ret uint64 = uint64(0) + _ = ret + var _0_result uint64 + _ = _0_result + _0_result = uint64(0) + var _hi0 uint64 = uint64((pairs).Cardinality()) + _ = _hi0 + for _1_i := uint64(0); _1_i < _hi0; _1_i++ { + _0_result = m_StandardLibrary_MemoryMath.Companion_Default___.Add(_0_result, Companion_Default___.PairLength((pairs).Select(uint32(_1_i)).(Pair))) } + ret = _0_result + return ret + return ret } -func (_static *CompanionStruct_Default___) PairLength(pair Pair) _dafny.Int { - return (((_dafny.IntOfInt64(2)).Plus(_dafny.IntOfUint32(((pair).Dtor_key().(_dafny.Sequence)).Cardinality()))).Plus(_dafny.IntOfInt64(2))).Plus(_dafny.IntOfUint32(((pair).Dtor_value().(_dafny.Sequence)).Cardinality())) +func (_static *CompanionStruct_Default___) PairLength(pair Pair) uint64 { + return m_StandardLibrary_MemoryMath.Companion_Default___.Add4(uint64(2), uint64(((pair).Dtor_key().(_dafny.Sequence)).Cardinality()), uint64(2), uint64(((pair).Dtor_value().(_dafny.Sequence)).Cardinality())) } -func (_static *CompanionStruct_Default___) ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH() _dafny.Int { - return (m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()).Minus(_dafny.IntOfInt64(2)) +func (_static *CompanionStruct_Default___) ESDK__CANONICAL__ENCRYPTION__CONTEXT__MAX__LENGTH() uint64 { + return ((m_StandardLibrary_UInt.Companion_Default___.UINT16__LIMIT()).Uint64()) - (func() uint64 { return (uint64(2)) })() } // End of class Default__ diff --git a/releases/go/encryption-sdk/SerializeFunctions/SerializeFunctions.go b/releases/go/encryption-sdk/SerializeFunctions/SerializeFunctions.go index a0711d03a..e43290b63 100644 --- a/releases/go/encryption-sdk/SerializeFunctions/SerializeFunctions.go +++ b/releases/go/encryption-sdk/SerializeFunctions/SerializeFunctions.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -122,6 +123,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -146,40 +148,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -204,7 +207,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -265,18 +267,18 @@ var _ _dafny.TraitOffspring = &Default__{} func (_static *CompanionStruct_Default___) Write(data _dafny.Sequence) _dafny.Sequence { return data } -func (_static *CompanionStruct_Default___) Read(buffer ReadableBuffer, length _dafny.Int) m_Wrappers.Result { - var _0_end _dafny.Int = ((buffer).Dtor_start()).Plus(length) +func (_static *CompanionStruct_Default___) Read(buffer ReadableBuffer, length uint64) m_Wrappers.Result { + var _0_end uint64 = m_StandardLibrary_MemoryMath.Companion_Default___.Add((buffer).Dtor_start(), length) _ = _0_end - var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((buffer).Dtor_bytes()).Cardinality())).Cmp(_0_end) >= 0, Companion_ReadProblems_.Create_MoreNeeded_(_0_end)) + var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64(((buffer).Dtor_bytes()).Cardinality())) >= (_0_end), Companion_ReadProblems_.Create_MoreNeeded_(_0_end)) _ = _1_valueOrError0 if (_1_valueOrError0).IsFailure() { return (_1_valueOrError0).PropagateFailure() } else { - return m_Wrappers.Companion_Result_.Create_Success_(Companion_SuccessfulRead_.Create_SuccessfulRead_(((buffer).Dtor_bytes()).Subsequence(((buffer).Dtor_start()).Uint32(), (_0_end).Uint32()), func(_pat_let0_0 ReadableBuffer) ReadableBuffer { + return m_Wrappers.Companion_Result_.Create_Success_(Companion_SuccessfulRead_.Create_SuccessfulRead_(((buffer).Dtor_bytes()).Subsequence(uint32((buffer).Dtor_start()), uint32(_0_end)), func(_pat_let0_0 ReadableBuffer) ReadableBuffer { return func(_2_dt__update__tmp_h0 ReadableBuffer) ReadableBuffer { - return func(_pat_let1_0 _dafny.Int) ReadableBuffer { - return func(_3_dt__update_hstart_h0 _dafny.Int) ReadableBuffer { + return func(_pat_let1_0 uint64) ReadableBuffer { + return func(_3_dt__update_hstart_h0 uint64) ReadableBuffer { return Companion_ReadableBuffer_.Create_ReadableBuffer_((_2_dt__update__tmp_h0).Dtor_bytes(), _3_dt__update_hstart_h0) }(_pat_let1_0) }(_0_end) @@ -288,7 +290,7 @@ func (_static *CompanionStruct_Default___) WriteUint16(number uint16) _dafny.Seq return Companion_Default___.Write(m_StandardLibrary_UInt.Companion_Default___.UInt16ToSeq(number)) } func (_static *CompanionStruct_Default___) ReadUInt16(buffer ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, _dafny.IntOfInt64(2)) + var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, uint64(2)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -306,7 +308,7 @@ func (_static *CompanionStruct_Default___) WriteUint32(number uint32) _dafny.Seq return Companion_Default___.Write(m_StandardLibrary_UInt.Companion_Default___.UInt32ToSeq(number)) } func (_static *CompanionStruct_Default___) ReadUInt32(buffer ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, _dafny.IntOfInt64(4)) + var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, uint64(4)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -324,7 +326,7 @@ func (_static *CompanionStruct_Default___) WriteUint64(number uint64) _dafny.Seq return Companion_Default___.Write(m_StandardLibrary_UInt.Companion_Default___.UInt64ToSeq(number)) } func (_static *CompanionStruct_Default___) ReadUInt64(buffer ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, _dafny.IntOfInt64(8)) + var _0_valueOrError0 m_Wrappers.Result = Companion_Default___.Read(buffer, uint64(8)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -349,7 +351,7 @@ func (_static *CompanionStruct_Default___) ReadShortLengthSeq(buffer ReadableBuf } else { var _1_length SuccessfulRead = (_0_valueOrError0).Extract().(SuccessfulRead) _ = _1_length - var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), _dafny.IntOfUint16((_1_length).Dtor_data().(uint16))) + var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), uint64((_1_length).Dtor_data().(uint16))) _ = _2_valueOrError1 if (_2_valueOrError1).IsFailure() { return (_2_valueOrError1).PropagateFailure() @@ -371,7 +373,7 @@ func (_static *CompanionStruct_Default___) ReadUint32Seq(buffer ReadableBuffer) } else { var _1_length SuccessfulRead = (_0_valueOrError0).Extract().(SuccessfulRead) _ = _1_length - var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), _dafny.IntOfUint32((_1_length).Dtor_data().(uint32))) + var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), uint64((_1_length).Dtor_data().(uint32))) _ = _2_valueOrError1 if (_2_valueOrError1).IsFailure() { return (_2_valueOrError1).PropagateFailure() @@ -393,7 +395,7 @@ func (_static *CompanionStruct_Default___) ReadUint64Seq(buffer ReadableBuffer) } else { var _1_length SuccessfulRead = (_0_valueOrError0).Extract().(SuccessfulRead) _ = _1_length - var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), _dafny.IntOfUint64((_1_length).Dtor_data().(uint64))) + var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.Read((_1_length).Dtor_tail(), (_1_length).Dtor_data().(uint64)) _ = _2_valueOrError1 if (_2_valueOrError1).IsFailure() { return (_2_valueOrError1).PropagateFailure() @@ -426,12 +428,12 @@ type CompanionStruct_ReadProblems_ struct { var Companion_ReadProblems_ = CompanionStruct_ReadProblems_{} type ReadProblems_MoreNeeded struct { - Pos _dafny.Int + Pos uint64 } func (ReadProblems_MoreNeeded) isReadProblems() {} -func (CompanionStruct_ReadProblems_) Create_MoreNeeded_(Pos _dafny.Int) ReadProblems { +func (CompanionStruct_ReadProblems_) Create_MoreNeeded_(Pos uint64) ReadProblems { return ReadProblems{ReadProblems_MoreNeeded{Pos}} } @@ -456,10 +458,10 @@ func (_this ReadProblems) Is_Error() bool { } func (CompanionStruct_ReadProblems_) Default() ReadProblems { - return Companion_ReadProblems_.Create_MoreNeeded_(_dafny.Zero) + return Companion_ReadProblems_.Create_MoreNeeded_(uint64(0)) } -func (_this ReadProblems) Dtor_pos() _dafny.Int { +func (_this ReadProblems) Dtor_pos() uint64 { return _this.Get_().(ReadProblems_MoreNeeded).Pos } @@ -491,7 +493,7 @@ func (_this ReadProblems) Equals(other ReadProblems) bool { case ReadProblems_MoreNeeded: { data2, ok := other.Get_().(ReadProblems_MoreNeeded) - return ok && data1.Pos.Cmp(data2.Pos) == 0 + return ok && data1.Pos == data2.Pos } case ReadProblems_Error: { @@ -593,12 +595,12 @@ var Companion_ReadableBuffer_ = CompanionStruct_ReadableBuffer_{} type ReadableBuffer_ReadableBuffer struct { Bytes _dafny.Sequence - Start _dafny.Int + Start uint64 } func (ReadableBuffer_ReadableBuffer) isReadableBuffer() {} -func (CompanionStruct_ReadableBuffer_) Create_ReadableBuffer_(Bytes _dafny.Sequence, Start _dafny.Int) ReadableBuffer { +func (CompanionStruct_ReadableBuffer_) Create_ReadableBuffer_(Bytes _dafny.Sequence, Start uint64) ReadableBuffer { return ReadableBuffer{ReadableBuffer_ReadableBuffer{Bytes, Start}} } @@ -608,14 +610,14 @@ func (_this ReadableBuffer) Is_ReadableBuffer() bool { } func (CompanionStruct_ReadableBuffer_) Default() ReadableBuffer { - return Companion_ReadableBuffer_.Create_ReadableBuffer_(_dafny.EmptySeq, _dafny.Zero) + return Companion_ReadableBuffer_.Create_ReadableBuffer_(_dafny.EmptySeq, uint64(0)) } func (_this ReadableBuffer) Dtor_bytes() _dafny.Sequence { return _this.Get_().(ReadableBuffer_ReadableBuffer).Bytes } -func (_this ReadableBuffer) Dtor_start() _dafny.Int { +func (_this ReadableBuffer) Dtor_start() uint64 { return _this.Get_().(ReadableBuffer_ReadableBuffer).Start } @@ -639,7 +641,7 @@ func (_this ReadableBuffer) Equals(other ReadableBuffer) bool { case ReadableBuffer_ReadableBuffer: { data2, ok := other.Get_().(ReadableBuffer_ReadableBuffer) - return ok && data1.Bytes.Equals(data2.Bytes) && data1.Start.Cmp(data2.Start) == 0 + return ok && data1.Bytes.Equals(data2.Bytes) && data1.Start == data2.Start } default: { diff --git a/releases/go/encryption-sdk/SharedHeaderFunctions/SharedHeaderFunctions.go b/releases/go/encryption-sdk/SharedHeaderFunctions/SharedHeaderFunctions.go index 66fc3cd1d..1368796f1 100644 --- a/releases/go/encryption-sdk/SharedHeaderFunctions/SharedHeaderFunctions.go +++ b/releases/go/encryption-sdk/SharedHeaderFunctions/SharedHeaderFunctions.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -125,6 +126,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -149,40 +151,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -207,7 +210,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -272,16 +274,16 @@ func (_static *CompanionStruct_Default___) WriteMessageFormatVersion(version m_H return m_SerializeFunctions.Companion_Default___.Write((version).Serialize()) } func (_static *CompanionStruct_Default___) ReadMessageFormatVersion(buffer m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.One) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(1)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() } else { var _1_rawVersion m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _1_rawVersion - var _2_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_MessageFormatVersion_.Get((_1_rawVersion).Dtor_data().(_dafny.Sequence))).MapFailure(func(coer2 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { - return func(arg3 interface{}) interface{} { - return coer2(arg3.(_dafny.Sequence)) + var _2_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_MessageFormatVersion_.Get((_1_rawVersion).Dtor_data().(_dafny.Sequence))).MapFailure(func(coer3 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { + return func(arg4 interface{}) interface{} { + return coer3(arg4.(_dafny.Sequence)) } }(func(_3_e _dafny.Sequence) m_SerializeFunctions.ReadProblems { return m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_3_e) @@ -300,16 +302,16 @@ func (_static *CompanionStruct_Default___) WriteESDKSuiteId(suite m_AwsCryptogra return m_SerializeFunctions.Companion_Default___.Write((suite).Dtor_binaryId()) } func (_static *CompanionStruct_Default___) ReadESDKSuiteId(buffer m_SerializeFunctions.ReadableBuffer, mpl *m_MaterialProviders.MaterialProvidersClient) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfInt64(2)) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(2)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() } else { var _1_esdkSuiteIdBytes m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _1_esdkSuiteIdBytes - var _2_valueOrError1 m_Wrappers.Result = ((mpl).GetAlgorithmSuiteInfo((_1_esdkSuiteIdBytes).Dtor_data().(_dafny.Sequence))).MapFailure(func(coer3 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { - return func(arg4 interface{}) interface{} { - return coer3(arg4.(m_AwsCryptographyMaterialProvidersTypes.Error)) + var _2_valueOrError1 m_Wrappers.Result = ((mpl).GetAlgorithmSuiteInfo((_1_esdkSuiteIdBytes).Dtor_data().(_dafny.Sequence))).MapFailure(func(coer4 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { + return func(arg5 interface{}) interface{} { + return coer4(arg5.(m_AwsCryptographyMaterialProvidersTypes.Error)) } }(func(_3___v0 m_AwsCryptographyMaterialProvidersTypes.Error) m_SerializeFunctions.ReadProblems { return m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Algorithm suite ID not supported.")) @@ -371,7 +373,7 @@ func (_static *CompanionStruct_Default___) WriteContentType(contentType m_Header return m_SerializeFunctions.Companion_Default___.Write(_dafny.SeqOf((contentType).Serialize())) } func (_static *CompanionStruct_Default___) ReadContentType(buffer m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.One) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(1)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -382,9 +384,9 @@ func (_static *CompanionStruct_Default___) ReadContentType(buffer m_SerializeFun _ = _1_raw var _2_tail m_SerializeFunctions.ReadableBuffer = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Tail _ = _2_tail - var _3_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_ContentType_.Get((_1_raw).Select(0).(uint8))).MapFailure(func(coer4 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { - return func(arg5 interface{}) interface{} { - return coer4(arg5.(_dafny.Sequence)) + var _3_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_ContentType_.Get((_1_raw).Select(uint32(uint32(0))).(uint8))).MapFailure(func(coer5 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { + return func(arg6 interface{}) interface{} { + return coer5(arg6.(_dafny.Sequence)) } }(func(_4_e _dafny.Sequence) m_SerializeFunctions.ReadProblems { return m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_4_e) diff --git a/releases/go/encryption-sdk/V1HeaderBody/V1HeaderBody.go b/releases/go/encryption-sdk/V1HeaderBody/V1HeaderBody.go index db566cfdd..1b2817970 100644 --- a/releases/go/encryption-sdk/V1HeaderBody/V1HeaderBody.go +++ b/releases/go/encryption-sdk/V1HeaderBody/V1HeaderBody.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -127,6 +128,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -151,40 +153,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -209,7 +212,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -356,7 +358,7 @@ func (_static *CompanionStruct_Default___) ReadV1HeaderBody(buffer m_SerializeFu } else { var _21_frameLength m_SerializeFunctions.SuccessfulRead = (_20_valueOrError11).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _21_frameLength - var _22_body m_HeaderTypes.HeaderBody = m_HeaderTypes.Companion_HeaderBody_.Create_V1HeaderBody_((_4_messageType).Dtor_data().(m_HeaderTypes.MessageType), (_6_suite).Dtor_data().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo), (_9_messageId).Dtor_data().(_dafny.Sequence), (_11_encryptionContext).Dtor_data().(_dafny.Sequence), (_13_encryptedDataKeys).Dtor_data().(_dafny.Sequence), (_15_contentType).Dtor_data().(m_HeaderTypes.ContentType), _dafny.IntOfUint8((_19_headerIvLength).Dtor_data().(uint8)), (_21_frameLength).Dtor_data().(uint32)) + var _22_body m_HeaderTypes.HeaderBody = m_HeaderTypes.Companion_HeaderBody_.Create_V1HeaderBody_((_4_messageType).Dtor_data().(m_HeaderTypes.MessageType), (_6_suite).Dtor_data().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo), (_9_messageId).Dtor_data().(_dafny.Sequence), (_11_encryptionContext).Dtor_data().(_dafny.Sequence), (_13_encryptedDataKeys).Dtor_data().(_dafny.Sequence), (_15_contentType).Dtor_data().(m_HeaderTypes.ContentType), uint64((_19_headerIvLength).Dtor_data().(uint8)), (_21_frameLength).Dtor_data().(uint32)) _ = _22_body return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_22_body, (_21_frameLength).Dtor_tail())) } @@ -376,7 +378,7 @@ func (_static *CompanionStruct_Default___) WriteV1MessageType(messageType m_Head return _dafny.SeqOf((messageType).Serialize()) } func (_static *CompanionStruct_Default___) ReadV1MessageType(buffer m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.One) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(1)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -387,9 +389,9 @@ func (_static *CompanionStruct_Default___) ReadV1MessageType(buffer m_SerializeF _ = _1_raw var _2_tail m_SerializeFunctions.ReadableBuffer = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Tail _ = _2_tail - var _3_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_MessageType_.Get((_1_raw).Select(0).(uint8))).MapFailure(func(coer5 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { - return func(arg6 interface{}) interface{} { - return coer5(arg6.(_dafny.Sequence)) + var _3_valueOrError1 m_Wrappers.Result = (m_HeaderTypes.Companion_MessageType_.Get((_1_raw).Select(uint32(uint32(0))).(uint8))).MapFailure(func(coer6 func(_dafny.Sequence) m_SerializeFunctions.ReadProblems) func(interface{}) interface{} { + return func(arg7 interface{}) interface{} { + return coer6(arg7.(_dafny.Sequence)) } }(func(_4_e _dafny.Sequence) m_SerializeFunctions.ReadProblems { return m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_4_e) @@ -408,7 +410,7 @@ func (_static *CompanionStruct_Default___) WriteV1ReservedBytes(reservedBytes _d return reservedBytes } func (_static *CompanionStruct_Default___) ReadV1ReservedBytes(buffer m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.IntOfUint32((Companion_Default___.RESERVED__BYTES()).Cardinality())) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64((Companion_Default___.RESERVED__BYTES()).Cardinality())) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -434,7 +436,7 @@ func (_static *CompanionStruct_Default___) WriteV1HeaderIvLength(ivLength uint8) return _dafny.SeqOf(ivLength) } func (_static *CompanionStruct_Default___) ReadV1HeaderIvLength(buffer m_SerializeFunctions.ReadableBuffer, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo) m_Wrappers.Result { - var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, _dafny.One) + var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read(buffer, uint64(1)) _ = _0_valueOrError0 if (_0_valueOrError0).IsFailure() { return (_0_valueOrError0).PropagateFailure() @@ -445,12 +447,12 @@ func (_static *CompanionStruct_Default___) ReadV1HeaderIvLength(buffer m_Seriali _ = _1_raw var _2_tail m_SerializeFunctions.ReadableBuffer = _let_tmp_rhs0.Get_().(m_SerializeFunctions.SuccessfulRead_SuccessfulRead).Tail _ = _2_tail - var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_1_raw).Select(0).(uint8)) == (m_SerializableTypes.Companion_Default___.GetIvLength(suite)), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("HeaderIv Length does not match Algorithm Suite."))) + var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_1_raw).Select(uint32(uint32(0))).(uint8)) == (m_SerializableTypes.Companion_Default___.GetIvLength(suite)), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("HeaderIv Length does not match Algorithm Suite."))) _ = _3_valueOrError1 if (_3_valueOrError1).IsFailure() { return (_3_valueOrError1).PropagateFailure() } else { - return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_((_1_raw).Select(0).(uint8), _2_tail)) + return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_((_1_raw).Select(uint32(uint32(0))).(uint8), _2_tail)) } } } diff --git a/releases/go/encryption-sdk/V2HeaderBody/V2HeaderBody.go b/releases/go/encryption-sdk/V2HeaderBody/V2HeaderBody.go index 5b65282a3..6e742f70f 100644 --- a/releases/go/encryption-sdk/V2HeaderBody/V2HeaderBody.go +++ b/releases/go/encryption-sdk/V2HeaderBody/V2HeaderBody.go @@ -101,6 +101,7 @@ import ( m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" + m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath" m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" @@ -128,6 +129,7 @@ var _ m__System.Dummy__ var _ m_Wrappers.Dummy__ var _ m_BoundedInts.Dummy__ var _ m_StandardLibrary_UInt.Dummy__ +var _ m_StandardLibrary_MemoryMath.Dummy__ var _ m_StandardLibrary_Sequence.Dummy__ var _ m_StandardLibrary_String.Dummy__ var _ m_StandardLibrary.Dummy__ @@ -152,40 +154,41 @@ var _ m_Relations.Dummy__ var _ m_Seq_MergeSort.Dummy__ var _ m__Math.Dummy__ var _ m_Seq.Dummy__ -var _ m_MultiKeyring.Dummy__ -var _ m_AwsArnParsing.Dummy__ -var _ m_AwsKmsMrkAreUnique.Dummy__ var _ m_Actions.Dummy__ -var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ -var _ m_AwsKmsUtils.Dummy__ -var _ m_Constants.Dummy__ -var _ m_MaterialWrapping.Dummy__ var _ m_CanonicalEncryptionContext.Dummy__ +var _ m_MaterialWrapping.Dummy__ var _ m_IntermediateKeyWrapping.Dummy__ var _ m_EdkWrapping.Dummy__ var _ m_ErrorMessages.Dummy__ +var _ m_RawAESKeyring.Dummy__ +var _ m_AwsArnParsing.Dummy__ +var _ m_Constants.Dummy__ +var _ m_EcdhEdkWrapping.Dummy__ +var _ m_RawECDHKeyring.Dummy__ +var _ m_RawRSAKeyring.Dummy__ +var _ m_AwsKmsMrkMatchForDecrypt.Dummy__ +var _ m_AwsKmsUtils.Dummy__ var _ m_AwsKmsKeyring.Dummy__ -var _ m_StrictMultiKeyring.Dummy__ var _ m_AwsKmsDiscoveryKeyring.Dummy__ -var _ m_Com_Amazonaws_Kms.Dummy__ -var _ m_Com_Amazonaws_Dynamodb.Dummy__ -var _ m_DiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ -var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ -var _ m_AwsKmsMrkKeyring.Dummy__ -var _ m_MrkAwareStrictMultiKeyring.Dummy__ +var _ m_AwsKmsEcdhKeyring.Dummy__ +var _ m_FileIO.Dummy__ var _ m_LocalCMC.Dummy__ var _ m_SynchronizedLocalCMC.Dummy__ var _ m_StormTracker.Dummy__ var _ m_StormTrackingCMC.Dummy__ var _ m_CacheConstants.Dummy__ var _ m_AwsKmsHierarchicalKeyring.Dummy__ +var _ m_AwsKmsMrkDiscoveryKeyring.Dummy__ +var _ m_AwsKmsMrkKeyring.Dummy__ var _ m_AwsKmsRsaKeyring.Dummy__ -var _ m_EcdhEdkWrapping.Dummy__ -var _ m_RawECDHKeyring.Dummy__ -var _ m_AwsKmsEcdhKeyring.Dummy__ -var _ m_RawAESKeyring.Dummy__ -var _ m_RawRSAKeyring.Dummy__ +var _ m_MultiKeyring.Dummy__ +var _ m_AwsKmsMrkAreUnique.Dummy__ +var _ m_StrictMultiKeyring.Dummy__ +var _ m_Com_Amazonaws_Kms.Dummy__ +var _ m_Com_Amazonaws_Dynamodb.Dummy__ +var _ m_DiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareDiscoveryMultiKeyring.Dummy__ +var _ m_MrkAwareStrictMultiKeyring.Dummy__ var _ m_CMM.Dummy__ var _ m_Defaults.Dummy__ var _ m_Commitment.Dummy__ @@ -210,7 +213,6 @@ var _ m_Functions.Dummy__ var _ m_Utf8EncodingForm.Dummy__ var _ m_Utf16EncodingForm.Dummy__ var _ m_UnicodeStrings.Dummy__ -var _ m_FileIO.Dummy__ var _ m_GeneralInternals.Dummy__ var _ m_MulInternalsNonlinear.Dummy__ var _ m_MulInternals.Dummy__ @@ -337,7 +339,7 @@ func (_static *CompanionStruct_Default___) ReadV2HeaderBody(buffer m_SerializeFu } else { var _15_frameLength m_SerializeFunctions.SuccessfulRead = (_14_valueOrError8).Extract().(m_SerializeFunctions.SuccessfulRead) _ = _15_frameLength - var _16_valueOrError9 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_15_frameLength).Dtor_tail(), _dafny.IntOfInt32(((((_4_suite).Dtor_data().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo)).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength())) + var _16_valueOrError9 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.Read((_15_frameLength).Dtor_tail(), uint64(((((_4_suite).Dtor_data().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo)).Dtor_commitment()).Dtor_HKDF()).Dtor_outputKeyLength())) _ = _16_valueOrError9 if (_16_valueOrError9).IsFailure() { return (_16_valueOrError9).PropagateFailure() @@ -358,8 +360,8 @@ func (_static *CompanionStruct_Default___) ReadV2HeaderBody(buffer m_SerializeFu } } } -func (_static *CompanionStruct_Default___) HeaderBytesToAADStart() _dafny.Int { - return ((_dafny.One).Plus(_dafny.IntOfInt64(2))).Plus(_dafny.IntOfInt64(32)) +func (_static *CompanionStruct_Default___) HeaderBytesToAADStart() uint64 { + return uint64(35) } // End of class Default__ diff --git a/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_dafny.go index 1328f1cc6..705de566c 100644 --- a/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_dafny.go +++ b/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_dafny.go @@ -139,6 +139,10 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith if enumVal == nativeInput { break } + if index == len(nativeInput.Values()) { + panic("Input value did not found in enum values") + } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { @@ -155,14 +159,14 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -178,14 +182,14 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -208,6 +212,10 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input if enumVal == input { break } + if index == len(input.Values()) { + panic("Input value did not found in enum values") + } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { @@ -223,14 +231,14 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -255,6 +263,7 @@ func Aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input if enumVal == *input { break } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { @@ -279,14 +288,14 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(input *int6 func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - var v []interface{} + v := make([]interface{}, 0, len(input)) if input == nil { return nil } for _, e := range input { v = append(v, e) } - return dafny.SeqOf(v...) + return dafny.SeqFromArray(v, false) }() } @@ -309,6 +318,10 @@ func Aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input if enumVal == input { break } + if index == len(input.Values()) { + panic("Input value did not found in enum values") + } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ { @@ -346,6 +359,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDa if enumVal == *input { break } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { @@ -379,6 +393,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy if enumVal == *input { break } + } var enum interface{} for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ { diff --git a/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_native.go b/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_native.go index 6247c1cdc..69db81e75 100644 --- a/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_native.go +++ b/releases/go/encryption-sdk/awscryptographyencryptionsdksmithygenerated/to_native.go @@ -157,18 +157,15 @@ func NetV4_0_0_RetryPolicy_FromDafny(input interface{}) awscryptographyencryptio func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -188,18 +185,15 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_FromDafny(inp } func Aws_cryptography_encryptionSdk_DecryptOutput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_DecryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -237,18 +231,15 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_FromDafny(inp } func Aws_cryptography_encryptionSdk_EncryptInput_plaintext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptInput_encryptionContext_FromDafny(input interface{}) map[string]string { @@ -299,18 +290,15 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_FromDafny(input int } func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_FromDafny(input interface{}) []byte { return func() []byte { - b := []byte{} if input == nil { return nil } - for i := dafny.Iterate(input); ; { - val, ok := i() - if !ok { - return b - } else { - b = append(b, val.(byte)) - } + a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray) + b := make([]byte, 0, a.Length()) + for i := uint32(0); i < a.Length(); i++ { + b = append(b, a.Select(i).(byte)) } + return b }() } func Aws_cryptography_encryptionSdk_EncryptOutput_encryptionContext_FromDafny(input interface{}) map[string]string { diff --git a/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeyRecipient.pem b/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeyRecipient.pem new file mode 100644 index 000000000..3c527903b --- /dev/null +++ b/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeyRecipient.pem @@ -0,0 +1,4 @@ +-----BEGIN PUBLIC KEY----- +MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE9istdPCuX9nF8EmA4tioe/k0TCa2 +M9VeBW1N9n0sxPA6uPVOfLtE4+KuYxAGT0dYoK6CY93nowUy1yS+R7A+wA== +-----END PUBLIC KEY----- diff --git a/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeySender.pem b/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeySender.pem new file mode 100644 index 000000000..40999490a --- /dev/null +++ b/releases/go/encryption-sdk/examples/KmsEccKeyringExamplePublicKeySender.pem @@ -0,0 +1,4 @@ +-----BEGIN PUBLIC KEY----- +MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE18m54QsLUnhWU7gT8hkAceNbZ/WB +GNUUSPCeIKqOyX5psiqyC1TXPOJXqKKaVv5Mg91WV9UjpboblOhNU35nRw== +-----END PUBLIC KEY----- diff --git a/releases/go/encryption-sdk/examples/go.mod b/releases/go/encryption-sdk/examples/go.mod index 91427c4d3..0897ebd6b 100644 --- a/releases/go/encryption-sdk/examples/go.mod +++ b/releases/go/encryption-sdk/examples/go.mod @@ -2,35 +2,34 @@ module github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk/examples go 1.23.0 -replace github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk => ../ - require ( - github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0 - github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0 - github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk v0.0.0-00010101000000-000000000000 - github.com/aws/aws-sdk-go-v2/config v1.29.0 - github.com/aws/aws-sdk-go-v2/credentials v1.17.53 - github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4 - github.com/aws/aws-sdk-go-v2/service/kms v1.37.12 - github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1 + github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk v0.2.0 + github.com/aws/aws-sdk-go-v2/config v1.31.0 + github.com/aws/aws-sdk-go-v2/credentials v1.18.4 + github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0 + github.com/aws/aws-sdk-go-v2/service/kms v1.44.0 + github.com/aws/aws-sdk-go-v2/service/sts v1.37.0 github.com/google/uuid v1.6.0 ) require ( - github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0 // indirect - github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0 // indirect - github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0 // indirect - github.com/aws/aws-sdk-go-v2 v1.33.0 // indirect - github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24 // indirect - github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28 // indirect - github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28 // indirect - github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9 // indirect - github.com/aws/aws-sdk-go-v2/service/sso v1.24.10 // indirect - github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9 // indirect - github.com/aws/smithy-go v1.22.1 // indirect - github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 // indirect - github.com/jmespath/go-jmespath v0.4.0 // indirect + github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1 // indirect + github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1 // indirect + github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1 // indirect + github.com/aws/aws-sdk-go-v2 v1.38.0 // indirect + github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3 // indirect + github.com/aws/aws-sdk-go-v2/service/sso v1.28.0 // indirect + github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0 // indirect + github.com/aws/smithy-go v1.22.5 // indirect + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1 // indirect ) + +replace github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk => ../ diff --git a/releases/go/encryption-sdk/examples/go.sum b/releases/go/encryption-sdk/examples/go.sum index 53885d3db..c872c995c 100644 --- a/releases/go/encryption-sdk/examples/go.sum +++ b/releases/go/encryption-sdk/examples/go.sum @@ -1,58 +1,46 @@ -github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0 h1:kow/mXv8Hu6aLWl8rlnRDKA897tl3lRa8ALOcSDwWMQ= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0/go.mod h1:JHhMzDQkrbrze8jkTYbIKI0+uK2Up6UxqVUOKRUj1qo= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0 h1:xVK6j0MNjVrzmwzjRXnuq2BOc0mjlRWQ35Mc1OTKmjo= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0/go.mod h1:KMs3humzWQ5kbdPLuXukCtxt/JbKr2tPWj+jlJUF7T4= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0 h1:M6tCnqVjHus/wulPyXrn63Y5gcDLfzbTOw1N31h4Wr4= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0/go.mod h1:wTGJJgTeWcyztSEDg5ziNqgCfOty9Ml83libL4HnkqM= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0 h1:nvPnMVl9dUqDb7oYvJh/7SiWcccs4n0dk7WjLX1BsJ8= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0/go.mod h1:W9V6Mm0ULDvH1JGL7/0qkrzRYuGTaxXfgEOoT7TodQM= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0 h1:NhVxn86bWyWc/uOnE+oTikZdj75yOW6kMCfZNBf2x5E= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0/go.mod h1:m3mzHKiNiSC0LWeWX6ZAxSe6mKbJHgliux1Yu/sjCYI= -github.com/aws/aws-sdk-go-v2 v1.33.0 h1:Evgm4DI9imD81V0WwD+TN4DCwjUMdc94TrduMLbgZJs= -github.com/aws/aws-sdk-go-v2 v1.33.0/go.mod h1:P5WJBrYqqbWVaOxgH0X/FYYD47/nooaPOZPlQdmiN2U= -github.com/aws/aws-sdk-go-v2/config v1.29.0 h1:Vk/u4jof33or1qAQLdofpjKV7mQQT7DcUpnYx8kdmxY= -github.com/aws/aws-sdk-go-v2/config v1.29.0/go.mod h1:iXAZK3Gxvpq3tA+B9WaDYpZis7M8KFgdrDPMmHrgbJM= -github.com/aws/aws-sdk-go-v2/credentials v1.17.53 h1:lwrVhiEDW5yXsuVKlFVUnR2R50zt2DklhOyeLETqDuE= -github.com/aws/aws-sdk-go-v2/credentials v1.17.53/go.mod h1:CkqM1bIw/xjEpBMhBnvqUXYZbpCFuj6dnCAyDk2AtAY= -github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24 h1:5grmdTdMsovn9kPZPI23Hhvp0ZyNm5cRO+IZFIYiAfw= -github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24/go.mod h1:zqi7TVKTswH3Ozq28PkmBmgzG1tona7mo9G2IJg4Cis= -github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28 h1:igORFSiH3bfq4lxKFkTSYDhJEUCYo6C8VKiWJjYwQuQ= -github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28/go.mod h1:3So8EA/aAYm36L7XIvCVwLa0s5N0P7o2b1oqnx/2R4g= -github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28 h1:1mOW9zAUMhTSrMDssEHS/ajx8JcAj/IcftzcmNlmVLI= -github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28/go.mod h1:kGlXVIWDfvt2Ox5zEaNglmq0hXPHgQFNMix33Tw22jA= -github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ= -github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc= -github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4 h1:pK2f6BM2vfbWOvjirUIabQH52fa1MycnFi1F8Ismeog= -github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4/go.mod h1:2xlKGs8OTgN92fRVfP4EgFgQGhYwVI7LQ2PLQ0tIFAQ= -github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1 h1:iXtILhvDxB6kPvEXgsDhGaZCSC6LQET5ZHSdJozeI0Y= -github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1/go.mod h1:9nu0fVANtYiAePIBh2/pFUSwtJ402hLnp854CNoDOeE= -github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9 h1:ramlTFqWSsOt4Y/skpd30D8oI0kfKf5wd1Yu9C5HhPw= -github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9/go.mod h1:+B//vxKaB6Z/HfJfRV4ikLz0M7nIcKheHKm96FuaRrs= -github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9 h1:TQmKDyETFGiXVhZfQ/I0cCFziqqX58pi4tKJGYGFSz0= -github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9/go.mod h1:HVLPK2iHQBUx7HfZeOQSEu3v2ubZaAY2YPbAm5/WUyY= -github.com/aws/aws-sdk-go-v2/service/kms v1.37.12 h1:jkZNsp+0NwC2isvmcRb2p1EYm188weJTfgcVr+3E9Pc= -github.com/aws/aws-sdk-go-v2/service/kms v1.37.12/go.mod h1:TTGECZ6vGfx8k/pmzQKokSJy7ux2PJID4r96QCh5L0A= -github.com/aws/aws-sdk-go-v2/service/sso v1.24.10 h1:DyZUj3xSw3FR3TXSwDhPhuZkkT14QHBiacdbUVcD0Dg= -github.com/aws/aws-sdk-go-v2/service/sso v1.24.10/go.mod h1:Ro744S4fKiCCuZECXgOi760TiYylUM8ZBf6OGiZzJtY= -github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9 h1:I1TsPEs34vbpOnR81GIcAq4/3Ud+jRHVGwx6qLQUHLs= -github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9/go.mod h1:Fzsj6lZEb8AkTE5S68OhcbBqeWPsR8RnGuKPr8Todl8= -github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3SotlEBvfUBPB1KVcM= -github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw= -github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro= -github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= -github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= -github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1 h1:nvrlDo1EddNCFknnyaW7s49P4Vwjgbm1VT13Mh87+D0= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1/go.mod h1:lZ/LN+rINEWvrfRItZoMNYPp6nTx/iZLIlXYq5yvWvA= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1 h1:GHba7vmqUvFOLhQvpzfE9KCh2oIOn/nQaN5Xu2rY1Ac= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1/go.mod h1:Rh8pLBW83043mr0GMCE5k68x7Gm/zMBtcWBuGFrsleM= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1 h1:TzZdNan/tjcDnwaiVwiR90t/iOohfQGdW5z5JyicBI0= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1/go.mod h1:d6R+lhtZXMkqsAuZ9zqNVZk3iXOYwVjxhBYQI3yr7OQ= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1 h1:TAIxapsLa/vJVrDyVM9R/+wuFWYdnyjfe/N9lvn5yFc= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1/go.mod h1:Uj8qJSU7Bx4YHEv0Up8J91Dh9TU0ggFnpAWLAbiFx+k= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1 h1:KShsiDfiiFa2A4UBh81BfiBMnNBIkelql7filQw6kfQ= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1/go.mod h1:j4QF5oVY9L1yNZrzoDu3l3d8TRh53uBw3FLZCL7xCTk= +github.com/aws/aws-sdk-go-v2 v1.38.0 h1:UCRQ5mlqcFk9HJDIqENSLR3wiG1VTWlyUfLDEvY7RxU= +github.com/aws/aws-sdk-go-v2 v1.38.0/go.mod h1:9Q0OoGQoboYIAJyslFyF1f5K1Ryddop8gqMhWx/n4Wg= +github.com/aws/aws-sdk-go-v2/config v1.31.0 h1:9yH0xiY5fUnVNLRWO0AtayqwU1ndriZdN78LlhruJR4= +github.com/aws/aws-sdk-go-v2/config v1.31.0/go.mod h1:VeV3K72nXnhbe4EuxxhzsDc/ByrCSlZwUnWH52Nde/I= +github.com/aws/aws-sdk-go-v2/credentials v1.18.4 h1:IPd0Algf1b+Qy9BcDp0sCUcIWdCQPSzDoMK3a8pcbUM= +github.com/aws/aws-sdk-go-v2/credentials v1.18.4/go.mod h1:nwg78FjH2qvsRM1EVZlX9WuGUJOL5od+0qvm0adEzHk= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3 h1:GicIdnekoJsjq9wqnvyi2elW6CGMSYKhdozE7/Svh78= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3/go.mod h1:R7BIi6WNC5mc1kfRM7XM/VHC3uRWkjc396sfabq4iOo= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3 h1:o9RnO+YZ4X+kt5Z7Nvcishlz0nksIt2PIzDglLMP0vA= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3/go.mod h1:+6aLJzOG1fvMOyzIySYjOFjcguGvVRL68R+uoRencN4= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3 h1:joyyUFhiTQQmVK6ImzNU9TQSNRNeD9kOklqTzyk5v6s= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3/go.mod h1:+vNIyZQP3b3B1tSLI0lxvrU9cfM7gpdRXMFfm67ZcPc= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3 h1:bIqFDwgGXXN1Kpp99pDOdKMTTb5d2KyU5X/BZxjOkRo= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3/go.mod h1:H5O/EsxDWyU+LP/V8i5sm8cxoZgc2fdNR9bxlOFrQTo= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0 h1:A5zeikrrAgz3YtNzhMat4K8hK/CFzOjFKLVk8pI7Cz8= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0/go.mod h1:tMQ/Edfn5xLcBFSVd3JDreJPias8GqBq0dVbCbMz9vs= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0 h1:6+lZi2JeGKtCraAj1rpoZfKqnQ9SptseRZioejfUOLM= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0/go.mod h1:eb3gfbVIxIoGgJsi9pGne19dhCBpK6opTYpQqAmdy44= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3 h1:xMmJPUT0G1q9+I0mzH4B6oN9fB5PkDoD+jvpVIcom1I= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3/go.mod h1:U0JFMTY/gPxV07XTXXz152nX0Hg1eBenzyslKF2j4j4= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3 h1:ieRzyHXypu5ByllM7Sp4hC5f/1Fy5wqxqY0yB85hC7s= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3/go.mod h1:O5ROz8jHiOAKAwx179v+7sHMhfobFVi6nZt8DEyiYoM= +github.com/aws/aws-sdk-go-v2/service/kms v1.44.0 h1:Z95XCqqSnwXr0AY7PgsiOUBhUG2GoDM5getw6RfD1Lg= +github.com/aws/aws-sdk-go-v2/service/kms v1.44.0/go.mod h1:DqcSngL7jJeU1fOzh5Ll5rSvX/MlMV6OZlE4mVdFAQc= +github.com/aws/aws-sdk-go-v2/service/sso v1.28.0 h1:Mc/MKBf2m4VynyJkABoVEN+QzkfLqGj0aiJuEe7cMeM= +github.com/aws/aws-sdk-go-v2/service/sso v1.28.0/go.mod h1:iS5OmxEcN4QIPXARGhavH7S8kETNL11kym6jhoS7IUQ= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0 h1:6csaS/aJmqZQbKhi1EyEMM7yBW653Wy/B9hnBofW+sw= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0/go.mod h1:59qHWaY5B+Rs7HGTuVGaC32m0rdpQ68N8QCN3khYiqs= +github.com/aws/aws-sdk-go-v2/service/sts v1.37.0 h1:MG9VFW43M4A8BYeAfaJJZWrroinxeTi2r3+SnmLQfSA= +github.com/aws/aws-sdk-go-v2/service/sts v1.37.0/go.mod h1:JdeBDPgpJfuS6rU/hNglmOigKhyEZtBmbraLE4GK1J8= +github.com/aws/smithy-go v1.22.5 h1:P9ATCXPMb2mPjYBgueqJNCA5S9UfktsW0tTxi+a7eqw= +github.com/aws/smithy-go v1.22.5/go.mod h1:t1ufH5HMublsJYulve2RKmHDC15xu1f26kHCp/HgceI= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1 h1:QyrSST4WJYQIXRSJNXFEwL1NIoA9bgirUHK8YwGoWkA= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo= -github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg= -github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo= -github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8= -github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U= -github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= -github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= -github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= -gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= -gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10= -gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI= diff --git a/releases/go/encryption-sdk/examples/recipient_private.pem b/releases/go/encryption-sdk/examples/recipient_private.pem new file mode 100644 index 000000000..d0dc5a92f --- /dev/null +++ b/releases/go/encryption-sdk/examples/recipient_private.pem @@ -0,0 +1,5 @@ +-----BEGIN PRIVATE KEY----- +MIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQg8A6AzcLeNQ/vUiM9 +Y/M5x2Zks7N5PSPLDhp901F8KnKhRANCAASExxbNXoELkYZ1jN+UURXryD3RG4GC +cqYrOZKJM4S85ZiKGFP6jXZFu20TGgjknKcyrPCkekSaJfe8Vu3OCE/b +-----END PRIVATE KEY----- diff --git a/releases/go/encryption-sdk/examples/recipient_public.pem b/releases/go/encryption-sdk/examples/recipient_public.pem new file mode 100644 index 000000000..58940d36d --- /dev/null +++ b/releases/go/encryption-sdk/examples/recipient_public.pem @@ -0,0 +1,4 @@ +-----BEGIN PUBLIC KEY----- +MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAEhMcWzV6BC5GGdYzflFEV68g90RuB +gnKmKzmSiTOEvOWYihhT+o12RbttExoI5JynMqzwpHpEmiX3vFbtzghP2w== +-----END PUBLIC KEY----- diff --git a/releases/go/encryption-sdk/examples/sender_private.pem b/releases/go/encryption-sdk/examples/sender_private.pem new file mode 100644 index 000000000..6ad84f079 --- /dev/null +++ b/releases/go/encryption-sdk/examples/sender_private.pem @@ -0,0 +1,5 @@ +-----BEGIN PRIVATE KEY----- +MIGHAgEAMBMGByqGSM49AgEGCCqGSM49AwEHBG0wawIBAQQgdjrJywvJP1T4wnT5 +7gg/Upi3SCL/5cAykelIoSX5joGhRANCAARzF0m1BgtIx645wWsjJ20ND1xQ6ScL +hvU0oCelOajQYY3sspsJiMCySHSlqdsBs0tu1TaM6CpWd49twPqT5zhC +-----END PRIVATE KEY----- diff --git a/releases/go/encryption-sdk/go.mod b/releases/go/encryption-sdk/go.mod index 8fc7ed2c2..59044f1f3 100644 --- a/releases/go/encryption-sdk/go.mod +++ b/releases/go/encryption-sdk/go.mod @@ -2,36 +2,32 @@ module github.com/aws/aws-encryption-sdk/releases/go/encryption-sdk go 1.23.0 -retract [v0.0.0-0, v0.1.1] - -require github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0 - require ( - github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0 - github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0 - github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0 - github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0 - github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1 + github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1 + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1 ) require ( - github.com/aws/aws-sdk-go-v2 v1.33.0 // indirect - github.com/aws/aws-sdk-go-v2/config v1.29.0 // indirect - github.com/aws/aws-sdk-go-v2/credentials v1.17.53 // indirect - github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24 // indirect - github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28 // indirect - github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28 // indirect - github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect - github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9 // indirect - github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9 // indirect - github.com/aws/aws-sdk-go-v2/service/kms v1.37.12 // indirect - github.com/aws/aws-sdk-go-v2/service/sso v1.24.10 // indirect - github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9 // indirect - github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 // indirect - github.com/aws/smithy-go v1.22.1 // indirect + github.com/aws/aws-sdk-go-v2 v1.38.0 // indirect + github.com/aws/aws-sdk-go-v2/config v1.31.0 // indirect + github.com/aws/aws-sdk-go-v2/credentials v1.18.4 // indirect + github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3 // indirect + github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3 // indirect + github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3 // indirect + github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3 // indirect + github.com/aws/aws-sdk-go-v2/service/kms v1.44.0 // indirect + github.com/aws/aws-sdk-go-v2/service/sso v1.28.0 // indirect + github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0 // indirect + github.com/aws/aws-sdk-go-v2/service/sts v1.37.0 // indirect + github.com/aws/smithy-go v1.22.5 // indirect github.com/google/uuid v1.6.0 // indirect - github.com/jmespath/go-jmespath v0.4.0 // indirect ) diff --git a/releases/go/encryption-sdk/go.sum b/releases/go/encryption-sdk/go.sum index 53885d3db..c872c995c 100644 --- a/releases/go/encryption-sdk/go.sum +++ b/releases/go/encryption-sdk/go.sum @@ -1,58 +1,46 @@ -github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0 h1:kow/mXv8Hu6aLWl8rlnRDKA897tl3lRa8ALOcSDwWMQ= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.0/go.mod h1:JHhMzDQkrbrze8jkTYbIKI0+uK2Up6UxqVUOKRUj1qo= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0 h1:xVK6j0MNjVrzmwzjRXnuq2BOc0mjlRWQ35Mc1OTKmjo= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.0/go.mod h1:KMs3humzWQ5kbdPLuXukCtxt/JbKr2tPWj+jlJUF7T4= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0 h1:M6tCnqVjHus/wulPyXrn63Y5gcDLfzbTOw1N31h4Wr4= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.0/go.mod h1:wTGJJgTeWcyztSEDg5ziNqgCfOty9Ml83libL4HnkqM= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0 h1:nvPnMVl9dUqDb7oYvJh/7SiWcccs4n0dk7WjLX1BsJ8= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.0/go.mod h1:W9V6Mm0ULDvH1JGL7/0qkrzRYuGTaxXfgEOoT7TodQM= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0 h1:NhVxn86bWyWc/uOnE+oTikZdj75yOW6kMCfZNBf2x5E= -github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0/go.mod h1:m3mzHKiNiSC0LWeWX6ZAxSe6mKbJHgliux1Yu/sjCYI= -github.com/aws/aws-sdk-go-v2 v1.33.0 h1:Evgm4DI9imD81V0WwD+TN4DCwjUMdc94TrduMLbgZJs= -github.com/aws/aws-sdk-go-v2 v1.33.0/go.mod h1:P5WJBrYqqbWVaOxgH0X/FYYD47/nooaPOZPlQdmiN2U= -github.com/aws/aws-sdk-go-v2/config v1.29.0 h1:Vk/u4jof33or1qAQLdofpjKV7mQQT7DcUpnYx8kdmxY= -github.com/aws/aws-sdk-go-v2/config v1.29.0/go.mod h1:iXAZK3Gxvpq3tA+B9WaDYpZis7M8KFgdrDPMmHrgbJM= -github.com/aws/aws-sdk-go-v2/credentials v1.17.53 h1:lwrVhiEDW5yXsuVKlFVUnR2R50zt2DklhOyeLETqDuE= -github.com/aws/aws-sdk-go-v2/credentials v1.17.53/go.mod h1:CkqM1bIw/xjEpBMhBnvqUXYZbpCFuj6dnCAyDk2AtAY= -github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24 h1:5grmdTdMsovn9kPZPI23Hhvp0ZyNm5cRO+IZFIYiAfw= -github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.24/go.mod h1:zqi7TVKTswH3Ozq28PkmBmgzG1tona7mo9G2IJg4Cis= -github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28 h1:igORFSiH3bfq4lxKFkTSYDhJEUCYo6C8VKiWJjYwQuQ= -github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.28/go.mod h1:3So8EA/aAYm36L7XIvCVwLa0s5N0P7o2b1oqnx/2R4g= -github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28 h1:1mOW9zAUMhTSrMDssEHS/ajx8JcAj/IcftzcmNlmVLI= -github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.28/go.mod h1:kGlXVIWDfvt2Ox5zEaNglmq0hXPHgQFNMix33Tw22jA= -github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ= -github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc= -github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4 h1:pK2f6BM2vfbWOvjirUIabQH52fa1MycnFi1F8Ismeog= -github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.4/go.mod h1:2xlKGs8OTgN92fRVfP4EgFgQGhYwVI7LQ2PLQ0tIFAQ= -github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1 h1:iXtILhvDxB6kPvEXgsDhGaZCSC6LQET5ZHSdJozeI0Y= -github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1/go.mod h1:9nu0fVANtYiAePIBh2/pFUSwtJ402hLnp854CNoDOeE= -github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9 h1:ramlTFqWSsOt4Y/skpd30D8oI0kfKf5wd1Yu9C5HhPw= -github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.9/go.mod h1:+B//vxKaB6Z/HfJfRV4ikLz0M7nIcKheHKm96FuaRrs= -github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9 h1:TQmKDyETFGiXVhZfQ/I0cCFziqqX58pi4tKJGYGFSz0= -github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.9/go.mod h1:HVLPK2iHQBUx7HfZeOQSEu3v2ubZaAY2YPbAm5/WUyY= -github.com/aws/aws-sdk-go-v2/service/kms v1.37.12 h1:jkZNsp+0NwC2isvmcRb2p1EYm188weJTfgcVr+3E9Pc= -github.com/aws/aws-sdk-go-v2/service/kms v1.37.12/go.mod h1:TTGECZ6vGfx8k/pmzQKokSJy7ux2PJID4r96QCh5L0A= -github.com/aws/aws-sdk-go-v2/service/sso v1.24.10 h1:DyZUj3xSw3FR3TXSwDhPhuZkkT14QHBiacdbUVcD0Dg= -github.com/aws/aws-sdk-go-v2/service/sso v1.24.10/go.mod h1:Ro744S4fKiCCuZECXgOi760TiYylUM8ZBf6OGiZzJtY= -github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9 h1:I1TsPEs34vbpOnR81GIcAq4/3Ud+jRHVGwx6qLQUHLs= -github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.9/go.mod h1:Fzsj6lZEb8AkTE5S68OhcbBqeWPsR8RnGuKPr8Todl8= -github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3SotlEBvfUBPB1KVcM= -github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw= -github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro= -github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= -github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= -github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1 h1:nvrlDo1EddNCFknnyaW7s49P4Vwjgbm1VT13Mh87+D0= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1/go.mod h1:lZ/LN+rINEWvrfRItZoMNYPp6nTx/iZLIlXYq5yvWvA= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1 h1:GHba7vmqUvFOLhQvpzfE9KCh2oIOn/nQaN5Xu2rY1Ac= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1/go.mod h1:Rh8pLBW83043mr0GMCE5k68x7Gm/zMBtcWBuGFrsleM= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1 h1:TzZdNan/tjcDnwaiVwiR90t/iOohfQGdW5z5JyicBI0= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1/go.mod h1:d6R+lhtZXMkqsAuZ9zqNVZk3iXOYwVjxhBYQI3yr7OQ= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1 h1:TAIxapsLa/vJVrDyVM9R/+wuFWYdnyjfe/N9lvn5yFc= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1/go.mod h1:Uj8qJSU7Bx4YHEv0Up8J91Dh9TU0ggFnpAWLAbiFx+k= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1 h1:KShsiDfiiFa2A4UBh81BfiBMnNBIkelql7filQw6kfQ= +github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1/go.mod h1:j4QF5oVY9L1yNZrzoDu3l3d8TRh53uBw3FLZCL7xCTk= +github.com/aws/aws-sdk-go-v2 v1.38.0 h1:UCRQ5mlqcFk9HJDIqENSLR3wiG1VTWlyUfLDEvY7RxU= +github.com/aws/aws-sdk-go-v2 v1.38.0/go.mod h1:9Q0OoGQoboYIAJyslFyF1f5K1Ryddop8gqMhWx/n4Wg= +github.com/aws/aws-sdk-go-v2/config v1.31.0 h1:9yH0xiY5fUnVNLRWO0AtayqwU1ndriZdN78LlhruJR4= +github.com/aws/aws-sdk-go-v2/config v1.31.0/go.mod h1:VeV3K72nXnhbe4EuxxhzsDc/ByrCSlZwUnWH52Nde/I= +github.com/aws/aws-sdk-go-v2/credentials v1.18.4 h1:IPd0Algf1b+Qy9BcDp0sCUcIWdCQPSzDoMK3a8pcbUM= +github.com/aws/aws-sdk-go-v2/credentials v1.18.4/go.mod h1:nwg78FjH2qvsRM1EVZlX9WuGUJOL5od+0qvm0adEzHk= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3 h1:GicIdnekoJsjq9wqnvyi2elW6CGMSYKhdozE7/Svh78= +github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.3/go.mod h1:R7BIi6WNC5mc1kfRM7XM/VHC3uRWkjc396sfabq4iOo= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3 h1:o9RnO+YZ4X+kt5Z7Nvcishlz0nksIt2PIzDglLMP0vA= +github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.3/go.mod h1:+6aLJzOG1fvMOyzIySYjOFjcguGvVRL68R+uoRencN4= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3 h1:joyyUFhiTQQmVK6ImzNU9TQSNRNeD9kOklqTzyk5v6s= +github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.3/go.mod h1:+vNIyZQP3b3B1tSLI0lxvrU9cfM7gpdRXMFfm67ZcPc= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3 h1:bIqFDwgGXXN1Kpp99pDOdKMTTb5d2KyU5X/BZxjOkRo= +github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3/go.mod h1:H5O/EsxDWyU+LP/V8i5sm8cxoZgc2fdNR9bxlOFrQTo= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0 h1:A5zeikrrAgz3YtNzhMat4K8hK/CFzOjFKLVk8pI7Cz8= +github.com/aws/aws-sdk-go-v2/service/dynamodb v1.47.0/go.mod h1:tMQ/Edfn5xLcBFSVd3JDreJPias8GqBq0dVbCbMz9vs= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0 h1:6+lZi2JeGKtCraAj1rpoZfKqnQ9SptseRZioejfUOLM= +github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0/go.mod h1:eb3gfbVIxIoGgJsi9pGne19dhCBpK6opTYpQqAmdy44= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3 h1:xMmJPUT0G1q9+I0mzH4B6oN9fB5PkDoD+jvpVIcom1I= +github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.3/go.mod h1:U0JFMTY/gPxV07XTXXz152nX0Hg1eBenzyslKF2j4j4= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3 h1:ieRzyHXypu5ByllM7Sp4hC5f/1Fy5wqxqY0yB85hC7s= +github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.3/go.mod h1:O5ROz8jHiOAKAwx179v+7sHMhfobFVi6nZt8DEyiYoM= +github.com/aws/aws-sdk-go-v2/service/kms v1.44.0 h1:Z95XCqqSnwXr0AY7PgsiOUBhUG2GoDM5getw6RfD1Lg= +github.com/aws/aws-sdk-go-v2/service/kms v1.44.0/go.mod h1:DqcSngL7jJeU1fOzh5Ll5rSvX/MlMV6OZlE4mVdFAQc= +github.com/aws/aws-sdk-go-v2/service/sso v1.28.0 h1:Mc/MKBf2m4VynyJkABoVEN+QzkfLqGj0aiJuEe7cMeM= +github.com/aws/aws-sdk-go-v2/service/sso v1.28.0/go.mod h1:iS5OmxEcN4QIPXARGhavH7S8kETNL11kym6jhoS7IUQ= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0 h1:6csaS/aJmqZQbKhi1EyEMM7yBW653Wy/B9hnBofW+sw= +github.com/aws/aws-sdk-go-v2/service/ssooidc v1.33.0/go.mod h1:59qHWaY5B+Rs7HGTuVGaC32m0rdpQ68N8QCN3khYiqs= +github.com/aws/aws-sdk-go-v2/service/sts v1.37.0 h1:MG9VFW43M4A8BYeAfaJJZWrroinxeTi2r3+SnmLQfSA= +github.com/aws/aws-sdk-go-v2/service/sts v1.37.0/go.mod h1:JdeBDPgpJfuS6rU/hNglmOigKhyEZtBmbraLE4GK1J8= +github.com/aws/smithy-go v1.22.5 h1:P9ATCXPMb2mPjYBgueqJNCA5S9UfktsW0tTxi+a7eqw= +github.com/aws/smithy-go v1.22.5/go.mod h1:t1ufH5HMublsJYulve2RKmHDC15xu1f26kHCp/HgceI= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1 h1:QyrSST4WJYQIXRSJNXFEwL1NIoA9bgirUHK8YwGoWkA= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo= -github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg= -github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo= -github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8= -github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U= -github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= -github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= -github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= -gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= -gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10= -gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI=