diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 2d9f8f9bc..a02ca3ce8 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -53,7 +53,7 @@ jobs: # and to translate version strings such as "nightly-latest" # to an actual DAFNY_VERSION. - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index bab1bcde8..92eba7df6 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -48,7 +48,7 @@ jobs: - run: git submodule update --init smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml index a0e30c1b5..8a96bf569 100644 --- a/.github/workflows/library_format.yml +++ b/.github/workflows/library_format.yml @@ -49,7 +49,7 @@ jobs: - run: git submodule update --init smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml index a2f5687e0..3cbdc43d9 100644 --- a/.github/workflows/library_go_tests.yml +++ b/.github/workflows/library_go_tests.yml @@ -64,7 +64,7 @@ jobs: - run: git submodule update --init smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_interop_tests.yml b/.github/workflows/library_interop_tests.yml index b9592e94b..073d14ad2 100644 --- a/.github/workflows/library_interop_tests.yml +++ b/.github/workflows/library_interop_tests.yml @@ -81,20 +81,6 @@ jobs: uses: actions-rust-lang/setup-rust-toolchain@v1.10.1 with: components: rustfmt - # TODO - uncomment this after Rust formatter works - # - name: Rustfmt Check - # uses: actions-rust-lang/rustfmt@v1 - - # TODO: Remove this after the formatting in Rust starts working - - name: smithy-dafny Rust hacks - if: matrix.language == 'rust' - shell: bash - run: | - if [ "$RUNNER_OS" == "macOS" ]; then - sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - else - sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - fi - name: Setup Go uses: actions/setup-go@v5 @@ -109,8 +95,15 @@ jobs: if: matrix.language == 'rust' && matrix.os == 'windows-latest' uses: ilammy/setup-nasm@v1 - - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + - name: Setup Dafny Rust + if: matrix.language == 'rust' + uses: dafny-lang/setup-dafny-action@v1.8.0 + with: + dafny-version: nightly-2025-01-30-7db1e5f + + - name: Setup Dafny Not Rust + if: matrix.language != 'rust' + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} @@ -154,7 +147,7 @@ jobs: if: matrix.language == 'rust' uses: ./.github/actions/install_smithy_dafny_codegen_dependencies - # TODO: Remove this after checking in Rust polymorph code + # We do not check in Rust polymorph code - name: Run make polymorph_rust if: matrix.language == 'rust' shell: bash @@ -274,20 +267,6 @@ jobs: uses: actions-rust-lang/setup-rust-toolchain@v1.10.1 with: components: rustfmt - # TODO - uncomment this after Rust formatter works - # - name: Rustfmt Check - # uses: actions-rust-lang/rustfmt@v1 - - # TODO: Remove this after the formatting in Rust starts working - - name: smithy-dafny Rust hacks - if: matrix.decrypting_language == 'rust' - shell: bash - run: | - if [ "$RUNNER_OS" == "macOS" ]; then - sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - else - sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - fi - name: Setup Go uses: actions/setup-go@v5 @@ -302,8 +281,15 @@ jobs: if: matrix.decrypting_language == 'rust' && matrix.os == 'windows-latest' uses: ilammy/setup-nasm@v1 - - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.6.1 + - name: Setup Dafny 2 Rust + if: matrix.decrypting_language == 'rust' + uses: dafny-lang/setup-dafny-action@v1.8.0 + with: + dafny-version: nightly-2025-01-30-7db1e5f + + - name: Setup Dafny 2 Not Rust + if: matrix.decrypting_language != 'rust' + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml index 7bf4b68b4..830fa4413 100644 --- a/.github/workflows/library_java_tests.yml +++ b/.github/workflows/library_java_tests.yml @@ -61,7 +61,7 @@ jobs: - run: git submodule update --init smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index 2a0c732b4..fd303c99a 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -64,7 +64,7 @@ jobs: dotnet-version: ${{ matrix.dotnet-version }} - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_python_tests.yml b/.github/workflows/library_python_tests.yml index ec6105118..906c7eed6 100644 --- a/.github/workflows/library_python_tests.yml +++ b/.github/workflows/library_python_tests.yml @@ -64,7 +64,7 @@ jobs: - run: git submodule update --init smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: dafny-version: ${{ inputs.dafny }} diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml index 6448c1401..cda8f063c 100644 --- a/.github/workflows/library_rust_tests.yml +++ b/.github/workflows/library_rust_tests.yml @@ -58,25 +58,11 @@ jobs: uses: actions-rust-lang/setup-rust-toolchain@v1.10.1 with: components: rustfmt - # TODO - uncomment this after Rust formatter works - # - name: Rustfmt Check - # uses: actions-rust-lang/rustfmt@v1 - # TODO: Use setup-dafny-actions with correct version when Dafny releases 4.8.2 - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.7.0 + uses: dafny-lang/setup-dafny-action@v1.8.0 with: - dafny-version: 4.9.0 - - # TODO: Remove this after the formatting in Rust starts working - - name: smithy-dafny Rust hacks - shell: bash - run: | - if [ "$RUNNER_OS" == "macOS" ]; then - sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - else - sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk - fi + dafny-version: nightly-2025-01-30-7db1e5f - name: Setup Java 17 for codegen uses: actions/setup-java@v3 @@ -110,3 +96,4 @@ jobs: working-directory: ./${{ matrix.library }} run: | make test_rust + make test_rust_debug diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go index 8bceb7898..deb7cf265 100644 --- a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go +++ b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go @@ -376,15 +376,6 @@ func DeleteCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderss } -func CryptographicMaterialsCache_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache { - val, ok := nativeResource.(*CryptographicMaterialsCache) - if ok { - return val.Impl - } - return CryptographicMaterialsCache{&CryptographicMaterialsCacheNativeWrapper{Impl: nativeResource}}.Impl - -} - func GetCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput) AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput { return func() AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput { @@ -421,6 +412,15 @@ func UpdateUsageMetadataInput_ToDafny(nativeInput awscryptographymaterialprovide } +func CryptographicMaterialsCache_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache { + val, ok := nativeResource.(*CryptographicMaterialsCache) + if ok { + return val.Impl + } + return CryptographicMaterialsCache{&CryptographicMaterialsCacheNativeWrapper{Impl: nativeResource}}.Impl + +} + func DecryptMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput) AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput { return func() AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput { @@ -439,15 +439,6 @@ func DecryptMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialprovider } -func CryptographicMaterialsManager_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager { - val, ok := nativeResource.(*CryptographicMaterialsManager) - if ok { - return val.Impl - } - return CryptographicMaterialsManager{&CryptographicMaterialsManagerNativeWrapper{Impl: nativeResource}}.Impl - -} - func GetEncryptionMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput) AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput { return func() AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput { @@ -466,6 +457,15 @@ func GetEncryptionMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialpr } +func CryptographicMaterialsManager_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager { + val, ok := nativeResource.(*CryptographicMaterialsManager) + if ok { + return val.Impl + } + return CryptographicMaterialsManager{&CryptographicMaterialsManagerNativeWrapper{Impl: nativeResource}}.Impl + +} + func OnDecryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput) AwsCryptographyMaterialProvidersTypes.OnDecryptInput { return func() AwsCryptographyMaterialProvidersTypes.OnDecryptInput { @@ -484,15 +484,6 @@ func OnDecryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithy } -func Keyring_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) AwsCryptographyMaterialProvidersTypes.IKeyring { - val, ok := nativeResource.(*Keyring) - if ok { - return val.Impl - } - return Keyring{&KeyringNativeWrapper{Impl: nativeResource}}.Impl - -} - func OnEncryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput) AwsCryptographyMaterialProvidersTypes.OnEncryptInput { return func() AwsCryptographyMaterialProvidersTypes.OnEncryptInput { @@ -511,6 +502,15 @@ func OnEncryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithy } +func Keyring_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) AwsCryptographyMaterialProvidersTypes.IKeyring { + val, ok := nativeResource.(*Keyring) + if ok { + return val.Impl + } + return Keyring{&KeyringNativeWrapper{Impl: nativeResource}}.Impl + +} + func AwsCryptographicMaterialProvidersException_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException) AwsCryptographyMaterialProvidersTypes.Error { return func() AwsCryptographyMaterialProvidersTypes.Error { diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go index bea74e571..e25efe684 100644 --- a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go +++ b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go @@ -375,15 +375,6 @@ func DeleteCacheEntryInput_FromDafny(dafnyInput AwsCryptographyMaterialProviders } -func CryptographicMaterialsCache_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache { - val, ok := dafnyResource.(*CryptographicMaterialsCacheNativeWrapper) - if ok { - return val.Impl - } - - return &CryptographicMaterialsCache{dafnyResource} -} - func GetCacheEntryInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput { return awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput{Identifier: aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(dafnyInput.Dtor_identifier()), @@ -423,6 +414,15 @@ func UpdateUsageMetadataInput_FromDafny(dafnyInput AwsCryptographyMaterialProvid } +func CryptographicMaterialsCache_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache { + val, ok := dafnyResource.(*CryptographicMaterialsCacheNativeWrapper) + if ok { + return val.Impl + } + + return &CryptographicMaterialsCache{dafnyResource} +} + func DecryptMaterialsInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput) awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput { return awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput{AlgorithmSuiteId: aws_cryptography_materialProviders_DecryptMaterialsInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId()), @@ -440,15 +440,6 @@ func DecryptMaterialsOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvide } -func CryptographicMaterialsManager_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { - val, ok := dafnyResource.(*CryptographicMaterialsManagerNativeWrapper) - if ok { - return val.Impl - } - - return &CryptographicMaterialsManager{dafnyResource} -} - func GetEncryptionMaterialsInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput) awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput { return awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput{EncryptionContext: aws_cryptography_materialProviders_GetEncryptionMaterialsInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext()), @@ -466,6 +457,15 @@ func GetEncryptionMaterialsOutput_FromDafny(dafnyOutput AwsCryptographyMaterialP } +func CryptographicMaterialsManager_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { + val, ok := dafnyResource.(*CryptographicMaterialsManagerNativeWrapper) + if ok { + return val.Impl + } + + return &CryptographicMaterialsManager{dafnyResource} +} + func OnDecryptInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.OnDecryptInput) awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput { return awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput{Materials: aws_cryptography_materialProviders_OnDecryptInput_materials_FromDafny(dafnyInput.Dtor_materials()), @@ -480,15 +480,6 @@ func OnDecryptOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes } -func Keyring_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.IKeyring) awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { - val, ok := dafnyResource.(*KeyringNativeWrapper) - if ok { - return val.Impl - } - - return &Keyring{dafnyResource} -} - func OnEncryptInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.OnEncryptInput) awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput { return awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput{Materials: aws_cryptography_materialProviders_OnEncryptInput_materials_FromDafny(dafnyInput.Dtor_materials())} @@ -501,6 +492,15 @@ func OnEncryptOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes } +func Keyring_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.IKeyring) awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + val, ok := dafnyResource.(*KeyringNativeWrapper) + if ok { + return val.Impl + } + + return &Keyring{dafnyResource} +} + func AwsCryptographicMaterialProvidersException_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes.Error) awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException { return awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException{Message: aws_cryptography_materialProviders_AwsCryptographicMaterialProvidersException_message_FromDafny(dafnyOutput.Dtor_message())} diff --git a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go index 8bceb7898..deb7cf265 100644 --- a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go +++ b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_dafny.go @@ -376,15 +376,6 @@ func DeleteCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderss } -func CryptographicMaterialsCache_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache { - val, ok := nativeResource.(*CryptographicMaterialsCache) - if ok { - return val.Impl - } - return CryptographicMaterialsCache{&CryptographicMaterialsCacheNativeWrapper{Impl: nativeResource}}.Impl - -} - func GetCacheEntryInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput) AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput { return func() AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput { @@ -421,6 +412,15 @@ func UpdateUsageMetadataInput_ToDafny(nativeInput awscryptographymaterialprovide } +func CryptographicMaterialsCache_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache { + val, ok := nativeResource.(*CryptographicMaterialsCache) + if ok { + return val.Impl + } + return CryptographicMaterialsCache{&CryptographicMaterialsCacheNativeWrapper{Impl: nativeResource}}.Impl + +} + func DecryptMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput) AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput { return func() AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput { @@ -439,15 +439,6 @@ func DecryptMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialprovider } -func CryptographicMaterialsManager_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager { - val, ok := nativeResource.(*CryptographicMaterialsManager) - if ok { - return val.Impl - } - return CryptographicMaterialsManager{&CryptographicMaterialsManagerNativeWrapper{Impl: nativeResource}}.Impl - -} - func GetEncryptionMaterialsInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput) AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput { return func() AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput { @@ -466,6 +457,15 @@ func GetEncryptionMaterialsOutput_ToDafny(nativeOutput awscryptographymaterialpr } +func CryptographicMaterialsManager_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager) AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager { + val, ok := nativeResource.(*CryptographicMaterialsManager) + if ok { + return val.Impl + } + return CryptographicMaterialsManager{&CryptographicMaterialsManagerNativeWrapper{Impl: nativeResource}}.Impl + +} + func OnDecryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput) AwsCryptographyMaterialProvidersTypes.OnDecryptInput { return func() AwsCryptographyMaterialProvidersTypes.OnDecryptInput { @@ -484,15 +484,6 @@ func OnDecryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithy } -func Keyring_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) AwsCryptographyMaterialProvidersTypes.IKeyring { - val, ok := nativeResource.(*Keyring) - if ok { - return val.Impl - } - return Keyring{&KeyringNativeWrapper{Impl: nativeResource}}.Impl - -} - func OnEncryptInput_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput) AwsCryptographyMaterialProvidersTypes.OnEncryptInput { return func() AwsCryptographyMaterialProvidersTypes.OnEncryptInput { @@ -511,6 +502,15 @@ func OnEncryptOutput_ToDafny(nativeOutput awscryptographymaterialproviderssmithy } +func Keyring_ToDafny(nativeResource awscryptographymaterialproviderssmithygeneratedtypes.IKeyring) AwsCryptographyMaterialProvidersTypes.IKeyring { + val, ok := nativeResource.(*Keyring) + if ok { + return val.Impl + } + return Keyring{&KeyringNativeWrapper{Impl: nativeResource}}.Impl + +} + func AwsCryptographicMaterialProvidersException_ToDafny(nativeInput awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException) AwsCryptographyMaterialProvidersTypes.Error { return func() AwsCryptographyMaterialProvidersTypes.Error { diff --git a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go index bea74e571..e25efe684 100644 --- a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go +++ b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go @@ -375,15 +375,6 @@ func DeleteCacheEntryInput_FromDafny(dafnyInput AwsCryptographyMaterialProviders } -func CryptographicMaterialsCache_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache { - val, ok := dafnyResource.(*CryptographicMaterialsCacheNativeWrapper) - if ok { - return val.Impl - } - - return &CryptographicMaterialsCache{dafnyResource} -} - func GetCacheEntryInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput { return awscryptographymaterialproviderssmithygeneratedtypes.GetCacheEntryInput{Identifier: aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(dafnyInput.Dtor_identifier()), @@ -423,6 +414,15 @@ func UpdateUsageMetadataInput_FromDafny(dafnyInput AwsCryptographyMaterialProvid } +func CryptographicMaterialsCache_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsCache) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsCache { + val, ok := dafnyResource.(*CryptographicMaterialsCacheNativeWrapper) + if ok { + return val.Impl + } + + return &CryptographicMaterialsCache{dafnyResource} +} + func DecryptMaterialsInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.DecryptMaterialsInput) awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput { return awscryptographymaterialproviderssmithygeneratedtypes.DecryptMaterialsInput{AlgorithmSuiteId: aws_cryptography_materialProviders_DecryptMaterialsInput_algorithmSuiteId_FromDafny(dafnyInput.Dtor_algorithmSuiteId()), @@ -440,15 +440,6 @@ func DecryptMaterialsOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvide } -func CryptographicMaterialsManager_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { - val, ok := dafnyResource.(*CryptographicMaterialsManagerNativeWrapper) - if ok { - return val.Impl - } - - return &CryptographicMaterialsManager{dafnyResource} -} - func GetEncryptionMaterialsInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.GetEncryptionMaterialsInput) awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput { return awscryptographymaterialproviderssmithygeneratedtypes.GetEncryptionMaterialsInput{EncryptionContext: aws_cryptography_materialProviders_GetEncryptionMaterialsInput_encryptionContext_FromDafny(dafnyInput.Dtor_encryptionContext()), @@ -466,6 +457,15 @@ func GetEncryptionMaterialsOutput_FromDafny(dafnyOutput AwsCryptographyMaterialP } +func CryptographicMaterialsManager_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager) awscryptographymaterialproviderssmithygeneratedtypes.ICryptographicMaterialsManager { + val, ok := dafnyResource.(*CryptographicMaterialsManagerNativeWrapper) + if ok { + return val.Impl + } + + return &CryptographicMaterialsManager{dafnyResource} +} + func OnDecryptInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.OnDecryptInput) awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput { return awscryptographymaterialproviderssmithygeneratedtypes.OnDecryptInput{Materials: aws_cryptography_materialProviders_OnDecryptInput_materials_FromDafny(dafnyInput.Dtor_materials()), @@ -480,15 +480,6 @@ func OnDecryptOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes } -func Keyring_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.IKeyring) awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { - val, ok := dafnyResource.(*KeyringNativeWrapper) - if ok { - return val.Impl - } - - return &Keyring{dafnyResource} -} - func OnEncryptInput_FromDafny(dafnyInput AwsCryptographyMaterialProvidersTypes.OnEncryptInput) awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput { return awscryptographymaterialproviderssmithygeneratedtypes.OnEncryptInput{Materials: aws_cryptography_materialProviders_OnEncryptInput_materials_FromDafny(dafnyInput.Dtor_materials())} @@ -501,6 +492,15 @@ func OnEncryptOutput_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes } +func Keyring_FromDafny(dafnyResource AwsCryptographyMaterialProvidersTypes.IKeyring) awscryptographymaterialproviderssmithygeneratedtypes.IKeyring { + val, ok := dafnyResource.(*KeyringNativeWrapper) + if ok { + return val.Impl + } + + return &Keyring{dafnyResource} +} + func AwsCryptographicMaterialProvidersException_FromDafny(dafnyOutput AwsCryptographyMaterialProvidersTypes.Error) awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException { return awscryptographymaterialproviderssmithygeneratedtypes.AwsCryptographicMaterialProvidersException{Message: aws_cryptography_materialProviders_AwsCryptographicMaterialProvidersException_message_FromDafny(dafnyOutput.Dtor_message())} diff --git a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/models.py b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/models.py index e6bd23c5a..17d6d3771 100644 --- a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/models.py +++ b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/models.py @@ -856,7 +856,7 @@ def __repr__(self) -> str: def _symmetric_signature_algorithm_from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> SymmetricSignatureAlgorithm: if "HMAC" in d: return SymmetricSignatureAlgorithmHMAC.from_dict(d) @@ -1504,7 +1504,7 @@ def as_dict(self) -> Dict[str, Any]: @staticmethod def from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> "KmsEcdhStaticConfigurationsKmsPublicKeyDiscovery": if len(d) != 1: raise TypeError(f"Unions may have exactly 1 value, but found {len(d)}") @@ -1535,7 +1535,7 @@ def as_dict(self) -> Dict[str, Any]: @staticmethod def from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> "KmsEcdhStaticConfigurationsKmsPrivateKeyToStaticPublicKey": if len(d) != 1: raise TypeError(f"Unions may have exactly 1 value, but found {len(d)}") @@ -1591,7 +1591,7 @@ def __repr__(self) -> str: def _kms_ecdh_static_configurations_from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> KmsEcdhStaticConfigurations: if "KmsPublicKeyDiscovery" in d: return KmsEcdhStaticConfigurationsKmsPublicKeyDiscovery.from_dict(d) @@ -3252,7 +3252,7 @@ def as_dict(self) -> Dict[str, Any]: @staticmethod def from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> "CreateDefaultCryptographicMaterialsManagerInput": """Creates a CreateDefaultCryptographicMaterialsManagerInput from a dictionary.""" @@ -3630,7 +3630,7 @@ def as_dict(self) -> Dict[str, Any]: @staticmethod def from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> "RawEcdhStaticConfigurationsRawPrivateKeyToStaticPublicKey": if len(d) != 1: raise TypeError(f"Unions may have exactly 1 value, but found {len(d)}") @@ -3664,7 +3664,7 @@ def as_dict(self) -> Dict[str, Any]: @staticmethod def from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> "RawEcdhStaticConfigurationsEphemeralPrivateKeyToStaticPublicKey": if len(d) != 1: raise TypeError(f"Unions may have exactly 1 value, but found {len(d)}") @@ -3721,7 +3721,7 @@ def __repr__(self) -> str: def _raw_ecdh_static_configurations_from_dict( - d: Dict[str, Any] + d: Dict[str, Any], ) -> RawEcdhStaticConfigurations: if "PublicKeyDiscovery" in d: return RawEcdhStaticConfigurationsPublicKeyDiscovery.from_dict(d) diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml b/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml index 5cf3748b8..0451ab452 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml +++ b/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml @@ -13,20 +13,20 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.5.11" -aws-lc-rs = "1.12.0" -aws-lc-sys = "0.24.0" +aws-config = "1.5.15" +aws-lc-rs = "1.12.2" +aws-lc-sys = "0.25.0" aws-sdk-dynamodb = "1.55.0" aws-sdk-kms = "1.51.0" aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] } -aws-smithy-types = "1.2.10" +aws-smithy-types = "1.2.12" chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} dashmap = "6.1.0" pem = "3.0.4" -tokio = {version = "1.42.0", features = ["full"] } -uuid = { version = "1.11.0", features = ["v4"] } +tokio = {version = "1.43.0", features = ["full"] } +uuid = { version = "1.12.1", features = ["v4"] } timeout = "0.1.0" -rand = "0.8.5" +rand = "0.9.0" futures = "0.3" diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_gcm.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_gcm.rs index 8867c539d..b5f12b997 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_gcm.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_gcm.rs @@ -10,7 +10,7 @@ use crate::software::amazon::cryptography::primitives::internaldafny::types::Err use crate::software::amazon::cryptography::primitives::internaldafny::types::AES_GCM; use crate::*; use aws_lc_rs::aead::{Aad, LessSafeKey, Nonce, UnboundKey}; -use std::rc::Rc; +use dafny_runtime::Rc; struct DoAESEncryptOutput { cipher_text: Vec, diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_kdf_ctr.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_kdf_ctr.rs index 36f17bbea..5d2800cb8 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_kdf_ctr.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/aes_kdf_ctr.rs @@ -12,7 +12,7 @@ pub mod AesKdfCtr { use crate::*; use aws_lc_rs::cipher::{EncryptingKey, EncryptionContext, UnboundCipherKey, AES_256}; use dafny_runtime::Sequence; - use std::rc::Rc; + use dafny_runtime::Rc; fn error(s: &str) -> Rc { Rc::new(DafnyError::AwsCryptographicPrimitivesError { diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs index 4afd94ac5..7781dc322 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs @@ -73,9 +73,9 @@ pub mod DafnyLibraries { } impl - ::dafny_runtime::UpcastObject for MutableMap + ::dafny_runtime::UpcastObject for MutableMap { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); + ::dafny_runtime::UpcastObjectFn!(dafny_runtime::DynAny); } pub mod FileIO { diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/ddb.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/ddb.rs index 2032916b5..fe250f86d 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/ddb.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/ddb.rs @@ -17,10 +17,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { - pub fn DDBClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc< + pub fn DDBClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let region = @@ -44,15 +44,15 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } - pub fn DynamoDBClient() -> ::std::rc::Rc< + pub fn DynamoDBClient() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let shared_config = match tokio::runtime::Handle::try_current() { @@ -68,7 +68,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/digest.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/digest.rs index f3a01ce67..4d1ca6975 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/digest.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/digest.rs @@ -12,12 +12,12 @@ use software::amazon::cryptography::primitives::internaldafny::types::DigestAlgo impl crate::ExternDigest::_default { #[allow(non_snake_case)] pub fn Digest( - digest_algorithm: &::std::rc::Rc, + digest_algorithm: &::dafny_runtime::Rc, message: &::dafny_runtime::Sequence, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence, - ::std::rc::Rc, + ::dafny_runtime::Rc, >, > { let algorithm = match **digest_algorithm { @@ -27,7 +27,7 @@ impl crate::ExternDigest::_default { }; let message_vec: Vec = message.iter().collect(); let result = digest::digest(algorithm, &message_vec); - ::std::rc::Rc::new(_Wrappers_Compile::Result::Success { + ::dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value: result.as_ref().iter().cloned().collect(), }) } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdh.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdh.rs index eb44091cd..93e4f529a 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdh.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdh.rs @@ -9,7 +9,7 @@ #[allow(non_snake_case)] pub mod ECDH { use crate::software::amazon::cryptography::primitives::internaldafny::types::Error as DafnyError; - use std::rc::Rc; + use dafny_runtime::Rc; fn error(s: &str) -> Rc { Rc::new(DafnyError::AwsCryptographicPrimitivesError { @@ -23,7 +23,7 @@ pub mod ECDH { use crate::software::amazon::cryptography::primitives::internaldafny::types::Error as DafnyError; use crate::*; use aws_lc_sys; - use std::rc::Rc; + use dafny_runtime::Rc; fn get_nid(x: &ECDHCurveSpec) -> i32 { match x { @@ -422,7 +422,7 @@ pub mod ECDH { use crate::software::amazon::cryptography::primitives::internaldafny::types::ECDHCurveSpec; use crate::software::amazon::cryptography::primitives::internaldafny::types::Error as DafnyError; use crate::*; - use std::rc::Rc; + use dafny_runtime::Rc; pub fn agree( curve_algorithm: &ECDHCurveSpec, @@ -472,7 +472,7 @@ pub mod ECDH { use crate::*; use aws_lc_rs::encoding::AsDer; use aws_lc_rs::encoding::EcPrivateKeyRfc5915Der; - use std::rc::Rc; + use dafny_runtime::Rc; fn ecdsa_key_gen(alg: &ECDHCurveSpec) -> Result<(Vec, Vec), String> { let private_key = @@ -518,7 +518,7 @@ pub mod ECDH { use super::*; use crate::software::amazon::cryptography::primitives::internaldafny::types::ECDHCurveSpec; use crate::*; - use std::rc::Rc; + use dafny_runtime::Rc; #[test] fn test_generate() { diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdsa.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdsa.rs index ae4a51b7b..b31307f09 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdsa.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/ecdsa.rs @@ -18,7 +18,7 @@ pub mod Signature { use aws_lc_rs::signature::EcdsaVerificationAlgorithm; use aws_lc_rs::signature::KeyPair; use aws_lc_rs::signature::UnparsedPublicKey; - use std::rc::Rc; + use dafny_runtime::Rc; fn error(s: &str) -> Rc { Rc::new(DafnyError::AwsCryptographicPrimitivesError { @@ -228,7 +228,7 @@ pub mod Signature { #[cfg(test)] mod tests { use super::*; - use std::rc::Rc; + use dafny_runtime::Rc; #[test] fn test_generate() { diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/hmac.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/hmac.rs index a336060f5..5c441ef55 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/hmac.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/hmac.rs @@ -21,20 +21,20 @@ fn convert_algorithm(input: &DigestAlgorithm) -> hmac::Algorithm { impl crate::HMAC::_default { #[allow(non_snake_case)] pub fn Digest( - input: &::std::rc::Rc< + input: &::dafny_runtime::Rc< crate::software::amazon::cryptography::primitives::internaldafny::types::HMacInput, >, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence, - ::std::rc::Rc, + ::dafny_runtime::Rc, >, > { let key_vec: Vec = input.key().iter().collect(); let the_key = hmac::Key::new(convert_algorithm(input.digestAlgorithm()), &key_vec); let message_vec: Vec = input.message().iter().collect(); let result = hmac::sign(&the_key, &message_vec); - ::std::rc::Rc::new(_Wrappers_Compile::Result::Success { + ::dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value: result.as_ref().iter().cloned().collect(), }) } @@ -44,7 +44,7 @@ impl crate::HMAC::_default { pub mod HMAC { use crate::*; use aws_lc_rs::hmac; - use std::cell::RefCell; + use ::dafny_runtime::RefCell; #[allow(non_camel_case_types)] pub struct _default {} @@ -58,33 +58,33 @@ pub mod HMAC { inner: RefCell, } - impl dafny_runtime::UpcastObject for HMac { - dafny_runtime::UpcastObjectFn!(dyn std::any::Any); + impl dafny_runtime::UpcastObject for HMac { + dafny_runtime::UpcastObjectFn!(dafny_runtime::DynAny); } impl HMac { pub fn Init(&self, salt: &::dafny_runtime::Sequence) { let salt: Vec = salt.iter().collect(); - self.inner.borrow_mut().key = Some(hmac::Key::new(self.algorithm, &salt)); + self.inner.lock().unwrap().key = Some(hmac::Key::new(self.algorithm, &salt)); let context = Some(hmac::Context::with_key( - self.inner.borrow().key.as_ref().unwrap(), + self.inner.lock().unwrap().key.as_ref().unwrap(), )); - self.inner.borrow_mut().context = context; + self.inner.lock().unwrap().context = context; } pub fn re_init(&self) { let context = Some(hmac::Context::with_key( - self.inner.borrow().key.as_ref().unwrap(), + self.inner.lock().unwrap().key.as_ref().unwrap(), )); - self.inner.borrow_mut().context = context; + self.inner.lock().unwrap().context = context; } pub fn Build( - input: &::std::rc::Rc< + input: &::dafny_runtime::Rc< software::amazon::cryptography::primitives::internaldafny::types::DigestAlgorithm, >, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc< + ::dafny_runtime::Rc< software::amazon::cryptography::primitives::internaldafny::types::Error, >, >, @@ -97,23 +97,23 @@ pub mod HMAC { }), }); - ::std::rc::Rc::new(_Wrappers_Compile::Result::Success { value: inner }) + ::dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value: inner }) } pub fn BlockUpdate(&self, block: &::dafny_runtime::Sequence) { let part: Vec = block.iter().collect(); self.inner - .borrow_mut() + .lock().unwrap() .context .as_mut() .unwrap() .update(&part); } pub fn GetResult(&self) -> ::dafny_runtime::Sequence { - let is_empty = self.inner.borrow().context.is_none(); + let is_empty = self.inner.lock().unwrap().context.is_none(); if is_empty { return [].iter().cloned().collect(); } - let tag = self.inner.borrow_mut().context.take().unwrap().sign(); + let tag = self.inner.lock().unwrap().context.take().unwrap().sign(); // other languages allow you to call BlockUpdate after GetResult // so we re-initialize to mimic that behavior self.re_init(); diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/kms.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/kms.rs index 571a3b3fa..a18e397ed 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/kms.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/kms.rs @@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { #[allow(non_snake_case)] - pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -41,13 +41,13 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::deps::com_amazonaws_kms::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } #[allow(non_snake_case)] - pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClient() -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let shared_config = match tokio::runtime::Handle::try_current() { Ok(curr) => tokio::task::block_in_place(|| { curr.block_on(async { @@ -62,7 +62,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::deps::com_amazonaws_kms::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } @@ -71,7 +71,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def pub fn RegionMatch( kmsClient: &::dafny_runtime::Object, region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc> { + ) -> ::dafny_runtime::Rc> { let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -83,6 +83,6 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def Some(r) => r.as_ref() == region, None => false, }; - ::std::rc::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) + ::dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) } } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/local_cmc.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/local_cmc.rs index c12c67f4f..88521591a 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/local_cmc.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/local_cmc.rs @@ -24,8 +24,8 @@ pub mod internal_SynchronizedLocalCMC { } } - impl ::dafny_runtime::UpcastObject for SynchronizedLocalCMC { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); + impl ::dafny_runtime::UpcastObject for SynchronizedLocalCMC { + ::dafny_runtime::UpcastObjectFn!(dafny_runtime::DynAny); } impl ::dafny_runtime::UpcastObject @@ -34,19 +34,19 @@ pub mod internal_SynchronizedLocalCMC { } impl software::amazon::cryptography::materialproviders::internaldafny::types::ICryptographicMaterialsCache for SynchronizedLocalCMC { - fn r#_PutCacheEntry_k(&self, input: &std::rc::Rc) -> std::rc::Rc>> { + fn r#_PutCacheEntry_k(&self, input: &dafny_runtime::Rc) -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut()._PutCacheEntry_k(input) } - fn r#_UpdateUsageMetadata_k(&self, input: &std::rc::Rc) -> std::rc::Rc>> { + fn r#_UpdateUsageMetadata_k(&self, input: &dafny_runtime::Rc) -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut()._UpdateUsageMetadata_k(input) } - fn r#_GetCacheEntry_k(&self, input: &std::rc::Rc) -> std::rc::Rc, std::rc::Rc>> { + fn r#_GetCacheEntry_k(&self, input: &dafny_runtime::Rc) -> dafny_runtime::Rc, dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut()._GetCacheEntry_k(input) } - fn r#_DeleteCacheEntry_k(&self, input: &std::rc::Rc) -> std::rc::Rc>> { + fn r#_DeleteCacheEntry_k(&self, input: &dafny_runtime::Rc) -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut()._DeleteCacheEntry_k(input) } } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/random.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/random.rs index 437a22c69..3fafbf6b8 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/random.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/random.rs @@ -12,23 +12,23 @@ impl crate::ExternRandom::_default { #[allow(non_snake_case)] pub fn GenerateBytes( num_bytes: i32, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence, - ::std::rc::Rc, + ::dafny_runtime::Rc, >, > { let mut rand_bytes: Vec = vec![0; num_bytes as usize]; match rand::fill(&mut rand_bytes) { Ok(_) => { - ::std::rc::Rc::new( + ::dafny_runtime::Rc::new( _Wrappers_Compile::Result::Success{value : dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&rand_bytes, |x| *x) } ) } Err(_) => { - std::rc::Rc::new(_Wrappers_Compile::Result::Failure{ error : std::rc::Rc::new( + dafny_runtime::Rc::new(_Wrappers_Compile::Result::Failure{ error : dafny_runtime::Rc::new( software::amazon::cryptography::primitives::internaldafny::types::Error::AwsCryptographicPrimitivesError{ message : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("Error generating random bytes.") })}) diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs index 650d72a2b..5edfda2a6 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs @@ -13,7 +13,7 @@ pub mod RSAEncryption { use crate::software::amazon::cryptography::primitives::internaldafny::types::RSAPaddingMode; use crate::*; use aws_lc_rs::encoding::{AsDer, Pkcs8V1Der, PublicKeyX509Der}; - use std::rc::Rc; + use dafny_runtime::Rc; use aws_lc_rs::rsa::KeySize; use aws_lc_rs::rsa::OaepAlgorithm; diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/sets.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/sets.rs index 755615ddb..6c9fb380c 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/sets.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/sets.rs @@ -21,7 +21,7 @@ pub mod SortedSets { pub fn SetToOrderedSequence( elems: &::dafny_runtime::Set<::dafny_runtime::Sequence>, - less: &::std::rc::Rc bool>, + less: &::dafny_runtime::Rc bool + Send + Sync>, ) -> ::dafny_runtime::Sequence<::dafny_runtime::Sequence> { let mut vec = elems.iter().cloned().collect::>(); vec.sort_by(|a, b| Self::order(a, b, less)); @@ -30,7 +30,7 @@ pub mod SortedSets { pub fn SetToOrderedSequence2( elems: &::dafny_runtime::Set<::dafny_runtime::Sequence>, - less: &::std::rc::Rc bool>, + less: &::dafny_runtime::Rc bool + Send + Sync>, ) -> ::dafny_runtime::Sequence<::dafny_runtime::Sequence> { Self::SetToOrderedSequence(elems, less) } @@ -38,7 +38,7 @@ pub mod SortedSets { fn order( x: &::dafny_runtime::Sequence, y: &::dafny_runtime::Sequence, - less: &::std::rc::Rc bool>, + less: &::dafny_runtime::Rc bool + Send + Sync>, ) -> Ordering { let mut iter1 = x.iter(); let mut iter2 = y.iter(); diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs index 9ca4461ca..64012bcb3 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs @@ -25,8 +25,8 @@ pub mod internal_StormTrackingCMC { } } - impl ::dafny_runtime::UpcastObject for StormTrackingCMC { - ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); + impl ::dafny_runtime::UpcastObject for StormTrackingCMC { + ::dafny_runtime::UpcastObjectFn!(dafny_runtime::DynAny); } impl ::dafny_runtime::UpcastObject @@ -35,20 +35,20 @@ pub mod internal_StormTrackingCMC { } impl crate::software::amazon::cryptography::materialproviders::internaldafny::types::ICryptographicMaterialsCache for StormTrackingCMC { - fn r#_PutCacheEntry_k(&self, input: &std::rc::Rc) - -> std::rc::Rc>> + fn r#_PutCacheEntry_k(&self, input: &dafny_runtime::Rc) + -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut().PutCacheEntry(input) } - fn r#_UpdateUsageMetadata_k(&self, input: &std::rc::Rc) - -> std::rc::Rc>> + fn r#_UpdateUsageMetadata_k(&self, input: &dafny_runtime::Rc) + -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut().UpdateUsageMetadata(input) } - fn r#_GetCacheEntry_k(&self, input: &std::rc::Rc) - -> std::rc::Rc, std::rc::Rc>> + fn r#_GetCacheEntry_k(&self, input: &dafny_runtime::Rc) + -> dafny_runtime::Rc, dafny_runtime::Rc>> { let max_in_flight = crate::Time::_default::CurrentRelativeTimeMilli() + unsafe { *(*self.wrapped.lock().unwrap()).as_ref().inFlightTTL.get() }; let sleep_milli = unsafe { *(*self.wrapped.lock().unwrap()).as_ref().sleepMilli.get() }; @@ -56,13 +56,13 @@ pub mod internal_StormTrackingCMC { loop { let result = self.wrapped.lock().unwrap().as_mut().GetFromCache(input); match &*result { - crate::_Wrappers_Compile::Result::Failure{error} => {return std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : error.clone()});} + crate::_Wrappers_Compile::Result::Failure{error} => {return dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : error.clone()});} crate::_Wrappers_Compile::Result::Success{value} => { match &**value { - Full { data } => { return std::rc::Rc::new(crate::_Wrappers_Compile::Result::Success{value : data.clone()}); } + Full { data } => { return dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Success{value : data.clone()}); } EmptyFetch {} => { - return std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : - std::rc::Rc::new(crate::software::amazon::cryptography::materialproviders::internaldafny::types::Error::EntryDoesNotExist { message: + return dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : + dafny_runtime::Rc::new(crate::software::amazon::cryptography::materialproviders::internaldafny::types::Error::EntryDoesNotExist { message: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( "Entry does not exist" ) @@ -73,8 +73,8 @@ pub mod internal_StormTrackingCMC { if crate::Time::_default::CurrentRelativeTimeMilli() <= max_in_flight { std::thread::sleep(sleep_time); } else { - return std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : - std::rc::Rc::new(crate::software::amazon::cryptography::materialproviders::internaldafny::types::Error::InFlightTTLExceeded { message: + return dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure{error : + dafny_runtime::Rc::new(crate::software::amazon::cryptography::materialproviders::internaldafny::types::Error::InFlightTTLExceeded { message: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( "Storm cache inFlightTTL exceeded" ) @@ -88,7 +88,7 @@ pub mod internal_StormTrackingCMC { } } - fn r#_DeleteCacheEntry_k(&self, input: &std::rc::Rc) -> std::rc::Rc>> { + fn r#_DeleteCacheEntry_k(&self, input: &dafny_runtime::Rc) -> dafny_runtime::Rc>> { self.wrapped.lock().unwrap().as_mut().DeleteCacheEntry(input) } } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs index 3182c8020..c4d6f086a 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs @@ -35,7 +35,7 @@ impl crate::Time::_default { } #[allow(non_snake_case)] - pub fn GetCurrentTimeStamp() -> ::std::rc::Rc< + pub fn GetCurrentTimeStamp() -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -43,7 +43,7 @@ impl crate::Time::_default { > { let now_utc = chrono::Utc::now(); let formatted = format!("{}", now_utc.format("%Y-%m-%dT%H:%M:%S%.6fZ")); - ::std::rc::Rc::new( + ::dafny_runtime::Rc::new( _Wrappers_Compile::Result::Success{value : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&formatted) } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs index a751af3c1..ff54c50d4 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs @@ -1,6 +1,9 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 +use std::sync::atomic::AtomicUsize; +use std::sync::atomic::Ordering; + pub struct ResourceTracker { count: usize, total: usize, @@ -17,6 +20,9 @@ impl ResourceTracker { cpu: cpu_time::ProcessTime::now(), } } + pub fn report_leak(&self) { + println!("{} outstanding allocations totalling {} bytes.", get_net_counter(), get_net_total()); + } pub fn report(&self) { let time = self.time.elapsed().unwrap().as_secs_f64(); let cpu = self.cpu.elapsed().as_secs_f64(); @@ -30,25 +36,38 @@ impl ResourceTracker { } } -static mut COUNTER: usize = 0; -static mut TOTAL: usize = 0; +static COUNTER: AtomicUsize = AtomicUsize::new(0); +static TOTAL: AtomicUsize = AtomicUsize::new(0); + +static NET_COUNTER: AtomicUsize = AtomicUsize::new(0); +static NET_TOTAL: AtomicUsize = AtomicUsize::new(0); fn add_to_counter(inc: usize) { - // SAFETY: There are no other threads which could be accessing `COUNTER`. - unsafe { - COUNTER += 1; - TOTAL += inc; - } + COUNTER.fetch_add(1, Ordering::SeqCst); + TOTAL.fetch_add(inc, Ordering::SeqCst); + NET_COUNTER.fetch_add(1, Ordering::SeqCst); + NET_TOTAL.fetch_add(inc, Ordering::SeqCst); +} + +fn subtract_from_counter(inc: usize) { + NET_COUNTER.fetch_sub(1, Ordering::SeqCst); + NET_TOTAL.fetch_sub(inc, Ordering::SeqCst); } fn get_counter() -> usize { - // SAFETY: There are no other threads which could be accessing `COUNTER`. - unsafe { COUNTER } + COUNTER.load(Ordering::SeqCst); } fn get_total() -> usize { - // SAFETY: There are no other threads which could be accessing `COUNTER`. - unsafe { TOTAL } + TOTAL.load(Ordering::SeqCst); +} + +fn get_net_counter() -> usize { + NET_COUNTER.load(Ordering::SeqCst); +} + +fn get_net_total() -> usize { + NET_TOTAL.load(Ordering::SeqCst); } use std::alloc::{GlobalAlloc, Layout, System}; @@ -62,6 +81,7 @@ unsafe impl GlobalAlloc for MyAllocator { } unsafe fn dealloc(&self, ptr: *mut u8, layout: Layout) { + subtract_from_counter(layout.size()); System.dealloc(ptr, layout) } } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/uuid.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/uuid.rs index 700b2b1d2..2a75c8bab 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/uuid.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/uuid.rs @@ -12,7 +12,7 @@ impl crate::UUID::_default { #[allow(non_snake_case)] pub fn ToByteArray( bytes: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -25,12 +25,12 @@ impl crate::UUID::_default { match Uuid::parse_str(&my_str) { Ok(u) => { let b = u.as_bytes(); - std::rc::Rc::new(_Wrappers_Compile::Result::Success { value : + dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value : b.iter().cloned().collect() }) } Err(e) => { - std::rc::Rc::new(_Wrappers_Compile::Result::Failure{ error : + dafny_runtime::Rc::new(_Wrappers_Compile::Result::Failure{ error : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &format!("{my_str} is not a valid UUID ({e}).")) }) @@ -41,7 +41,7 @@ impl crate::UUID::_default { #[allow(non_snake_case)] pub fn FromByteArray( bytes: &::dafny_runtime::Sequence, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -49,27 +49,27 @@ impl crate::UUID::_default { > { let vec: Vec = bytes.iter().collect(); if vec.len() != 16 { - return std::rc::Rc::new(_Wrappers_Compile::Result::Failure{ error : + return dafny_runtime::Rc::new(_Wrappers_Compile::Result::Failure{ error : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("Not 16 bytes of input to FromByteArray.") }); } let bytes: ::uuid::Bytes = vec[..16].try_into().unwrap(); let uuid = Uuid::from_bytes_ref(&bytes); let my_str = uuid.to_string(); - std::rc::Rc::new(_Wrappers_Compile::Result::Success { value : + dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&my_str) }) } #[allow(non_snake_case)] - pub fn GenerateUUID() -> ::std::rc::Rc< + pub fn GenerateUUID() -> ::dafny_runtime::Rc< _Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >, > { let my_str = Uuid::new_v4().to_string(); - std::rc::Rc::new(_Wrappers_Compile::Result::Success { value : + dafny_runtime::Rc::new(_Wrappers_Compile::Result::Success { value : dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&my_str) }) } diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/tests/local_cmc_tests.rs b/AwsCryptographicMaterialProviders/runtimes/rust/tests/local_cmc_tests.rs index d1d5e6cd4..5a0e1c96b 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/tests/local_cmc_tests.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/tests/local_cmc_tests.rs @@ -39,7 +39,7 @@ pub mod local_cmc_tests { use aws_mpl_rs::deps::aws_cryptography_keyStore::types::BeaconKeyMaterials; use std::collections::HashMap; use chrono::Utc; - use rand::{thread_rng, Rng}; + use rand::{rng, Rng}; use futures::stream::StreamExt; // Currently this is commented out to keep it consistent with other // runtimes but every language should eventually have a network @@ -94,7 +94,7 @@ pub mod local_cmc_tests { async move { println!("-----------TestLotsofAdd-----------"); - let random = thread_rng().gen_range(0..id_size); + let random = rng().random_range(0..id_size); let beacon_key_identifier: &str = identifiers[random]; let cache_identifier: aws_smithy_types::Blob = aws_smithy_types::Blob::new(beacon_key_identifier.as_bytes()); diff --git a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml index 1de2e67bc..de0253aed 100644 --- a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml +++ b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml @@ -7,15 +7,15 @@ rust-version = "1.80.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.5.11" -aws-lc-rs = "1.12.0" -aws-lc-sys = "0.24.0" +aws-config = "1.5.15" +aws-lc-rs = "1.12.2" +aws-lc-sys = "0.25.0" aws-smithy-runtime-api = "1.7.3" -aws-smithy-types = "1.2.10" +aws-smithy-types = "1.2.12" chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} dashmap = "6.1.0" pem = "3.0.4" -tokio = {version = "1.42.0", features = ["full"] } -uuid = { version = "1.11.0", features = ["v4"] } +tokio = {version = "1.43.0", features = ["full"] } +uuid = { version = "1.12.1", features = ["v4"] } diff --git a/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml b/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml index 0fd167199..c5c676c33 100644 --- a/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml +++ b/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml @@ -7,13 +7,13 @@ rust-version = "1.80.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.5.11" +aws-config = "1.5.15" aws-sdk-dynamodb = "1.55.0" aws-smithy-runtime-api = "1.7.3" -aws-smithy-types = "1.2.10" +aws-smithy-types = "1.2.12" chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} dashmap = "6.1.0" -tokio = {version = "1.42.0", features = ["full"] } -uuid = { version = "1.11.0", features = ["v4"] } +tokio = {version = "1.43.0", features = ["full"] } +uuid = { version = "1.12.1", features = ["v4"] } diff --git a/ComAmazonawsDynamodb/runtimes/rust/src/ddb.rs b/ComAmazonawsDynamodb/runtimes/rust/src/ddb.rs index f2f942a0a..36ca46962 100644 --- a/ComAmazonawsDynamodb/runtimes/rust/src/ddb.rs +++ b/ComAmazonawsDynamodb/runtimes/rust/src/ddb.rs @@ -17,10 +17,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| #[allow(non_snake_case)] impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { - pub fn DDBClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc< + pub fn DDBClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let region = @@ -44,15 +44,15 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } - pub fn DynamoDBClient() -> ::std::rc::Rc< + pub fn DynamoDBClient() -> ::dafny_runtime::Rc< crate::r#_Wrappers_Compile::Result< ::dafny_runtime::Object, - ::std::rc::Rc + ::dafny_runtime::Rc > >{ let shared_config = match tokio::runtime::Handle::try_current() { @@ -68,7 +68,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny: let inner = aws_sdk_dynamodb::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } diff --git a/ComAmazonawsKms/runtimes/rust/Cargo.toml b/ComAmazonawsKms/runtimes/rust/Cargo.toml index 0a7670a3d..466fa9bee 100644 --- a/ComAmazonawsKms/runtimes/rust/Cargo.toml +++ b/ComAmazonawsKms/runtimes/rust/Cargo.toml @@ -7,13 +7,13 @@ rust-version = "1.80.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.5.11" +aws-config = "1.5.15" aws-sdk-kms = "1.51.0" aws-smithy-runtime-api = "1.7.3" -aws-smithy-types = "1.2.10" +aws-smithy-types = "1.2.12" chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} dashmap = "6.1.0" -tokio = {version = "1.42.0", features = ["full"] } -uuid = { version = "1.11.0", features = ["v4"] } +tokio = {version = "1.43.0", features = ["full"] } +uuid = { version = "1.12.1", features = ["v4"] } diff --git a/ComAmazonawsKms/runtimes/rust/src/kms.rs b/ComAmazonawsKms/runtimes/rust/src/kms.rs index 97abe65c4..d3fe8e54d 100644 --- a/ComAmazonawsKms/runtimes/rust/src/kms.rs +++ b/ComAmazonawsKms/runtimes/rust/src/kms.rs @@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default { #[allow(non_snake_case)] - pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClientForRegion(region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>) -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -41,13 +41,13 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } #[allow(non_snake_case)] - pub fn KMSClient() -> ::std::rc::Rc, ::std::rc::Rc>>{ + pub fn KMSClient() -> ::dafny_runtime::Rc, ::dafny_runtime::Rc>>{ let shared_config = match tokio::runtime::Handle::try_current() { Ok(curr) => tokio::task::block_in_place(|| { curr.block_on(async { @@ -62,7 +62,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def let inner = aws_sdk_kms::Client::new(&shared_config); let client = crate::client::Client { inner }; let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); - std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success { value: dafny_client, }) } @@ -71,7 +71,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def pub fn RegionMatch( kmsClient: &::dafny_runtime::Object, region: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc> { + ) -> ::dafny_runtime::Rc> { let region = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string( region, @@ -83,6 +83,6 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def Some(r) => r.as_ref() == region, None => false, }; - ::std::rc::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) + ::dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Option::Some { value: flag }) } } diff --git a/StandardLibrary/runtimes/rust/Cargo.toml b/StandardLibrary/runtimes/rust/Cargo.toml index afa8e60a5..a8e8ed8d8 100644 --- a/StandardLibrary/runtimes/rust/Cargo.toml +++ b/StandardLibrary/runtimes/rust/Cargo.toml @@ -9,5 +9,5 @@ rust-version = "1.80.0" [dependencies] chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} -uuid = { version = "1.11.0", features = ["v4"] } +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} +uuid = { version = "1.12.1", features = ["v4"] } diff --git a/StandardLibrary/runtimes/rust/src/standard_library_externs.rs b/StandardLibrary/runtimes/rust/src/standard_library_externs.rs index 54198eafa..6165ee389 100644 --- a/StandardLibrary/runtimes/rust/src/standard_library_externs.rs +++ b/StandardLibrary/runtimes/rust/src/standard_library_externs.rs @@ -8,7 +8,7 @@ use crate::implementation_from_dafny::UTF8; impl crate::implementation_from_dafny::UTF8::_default { pub fn Encode( s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -35,7 +35,7 @@ impl crate::implementation_from_dafny::UTF8::_default { surrogate = Some(c.0); continue; } - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) }); @@ -43,12 +43,12 @@ impl crate::implementation_from_dafny::UTF8::_default { } } if let Some(s) = surrogate { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::>::Failure { + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &format!("Surrogate pair missing: 0x{:04x}", s)) }); } - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::< UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, >::Success { @@ -57,7 +57,7 @@ impl crate::implementation_from_dafny::UTF8::_default { } pub fn Decode( b: &::dafny_runtime::Sequence, - ) -> ::std::rc::Rc< + ) -> ::dafny_runtime::Rc< r#_Wrappers_Compile::Result< ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, @@ -66,13 +66,13 @@ impl crate::implementation_from_dafny::UTF8::_default { let b = String::from_utf8(b.to_array().as_ref().clone()); match b { Ok(s) => { - ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) }) }, Err(e) => { - return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + return ::dafny_runtime::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( &e.to_string()) diff --git a/TestVectorsAwsCryptographicMaterialProviders/Makefile b/TestVectorsAwsCryptographicMaterialProviders/Makefile index 313de06a0..54cb9636f 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/Makefile +++ b/TestVectorsAwsCryptographicMaterialProviders/Makefile @@ -96,15 +96,6 @@ WRAPPED_INDEX_FILE_PATH=dafny/TestVectorsAwsCryptographicMaterialProviders/src/L WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny.wrapped\" } WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService" WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService" -# Rust SED Hacks -IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE=runtimes/rust/src/implementation_from_dafny.rs -IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN="WrappedMaterialProvidersMain::_default::Main();" -IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN= \ - "let args: Vec = std::env::args().collect();\ - let dafny_strings = args.iter().map(|x| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(\&x)).collect::>();\ - let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings);\ - r\#_WrappedMaterialProvidersMain_Compile::_default::Main(\&dafny_args);" - # TODO: Remove after wrapped client issue is fixed in Rust REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs @@ -113,14 +104,9 @@ REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;' REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;' REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;' -transpile_implementation_rust: _replace_main_method_name_rust - # TODO: Remove after wrapped client issue is fixed in Rust _polymorph_rust: _remove_wrapped_client_rust -_replace_main_method_name_rust: - $(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN) - # TODO: Remove after wrapped client issue is fixed in Rust _remove_wrapped_client_rust: $(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1) @@ -215,6 +201,7 @@ test_generate_vectors_python: cp dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json runtimes/python test_generate_vectors_rust: + rustc --version cd runtimes/rust && \ cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt-manifest --encrypt-manifest-output . && \ cd ../../ @@ -238,6 +225,7 @@ test_encrypt_vectors_python: python3 -m tox -c runtimes/python --verbose -e cli -- encrypt --manifest-path runtimes/python --decrypt-manifest-path runtimes/python test_encrypt_vectors_rust: + rustc --version cd runtimes/rust && \ cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt --manifest-path . --decrypt-manifest-path . && \ cd ../../ @@ -259,9 +247,10 @@ test_decrypt_encrypt_vectors_python: python3 -m tox -c runtimes/python --verbose -e cli -- decrypt --manifest-path runtimes/python test_decrypt_encrypt_vectors_rust: + rustc --version cd runtimes/rust && \ cargo run --bin test-vectors --features="wrapped-client" --release -- decrypt --manifest-path . && \ cd ../../ test_decrypt_encrypt_vectors_go: - go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. \ No newline at end of file + go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml index 778c41f64..6ec2c0ff1 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml @@ -10,20 +10,20 @@ rust-version = "1.80.0" wrapped-client = [] [dependencies] -aws-config = "1.5.11" -aws-lc-rs = "1.12.0" -aws-lc-sys = "0.24.0" +aws-config = "1.5.15" +aws-lc-rs = "1.12.2" +aws-lc-sys = "0.25.0" aws-sdk-dynamodb = "1.55.0" aws-sdk-kms = "1.51.0" aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] } -aws-smithy-types = "1.2.10" +aws-smithy-types = "1.2.12" chrono = "0.4.39" cpu-time = "1.0.0" -dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} +dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"]} dashmap = "6.1.0" pem = "3.0.4" -tokio = {version = "1.42.0", features = ["full"] } -uuid = { version = "1.11.0", features = ["v4"] } +tokio = {version = "1.43.0", features = ["full"] } +uuid = { version = "1.12.1", features = ["v4"] } [dev-dependencies] aws-mpl-test-vectors = { path = ".", features = ["wrapped-client"] } diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/main.rs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/main.rs index 4748f0c80..05b9e7d9e 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/main.rs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/main.rs @@ -65,9 +65,14 @@ pub(crate) use crate::implementation_from_dafny::_StormTracker_Compile; pub(crate) use crate::implementation_from_dafny::_LocalCMC_Compile; pub(crate) use crate::implementation_from_dafny::_TestWrappedMaterialProvidersMain_Compile; -fn main() { +fn main2() { let args: Vec = std::env::args().collect(); let dafny_strings = args.iter().map(|x| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x)).collect::>(); let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings); crate::implementation_from_dafny::r#_WrappedMaterialProvidersMain_Compile::_default::Main(&dafny_args); -} \ No newline at end of file +} + +// RUST_MIN_STACK does not work for `main`, so we need a new thread +fn main() { + std::thread::Builder::new().stack_size(64 * 1024 * 1024).spawn(main2).unwrap().join().unwrap(); +} diff --git a/smithy-dafny b/smithy-dafny index 6475c2ea5..5fb3f25ea 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit 6475c2ea5284c1204285156c74863c4c3294c7a0 +Subproject commit 5fb3f25ea3444c51b2ad30b25ab03964cf866cd1