From af8c57a0eb37462d51d9adb5222d7f702805ffd0 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 29 Aug 2025 13:11:36 -0700 Subject: [PATCH 1/2] auto commit --- submodules/MaterialProviders | 2 +- submodules/smithy-dafny | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index f6bdd23d4e..dc1678ab78 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit f6bdd23d4ef83e3513554abb41d0ddbd3d89e8b8 +Subproject commit dc1678ab78948bee223f029df36b9f5d2cb0276d diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index b60ee9f53a..8ac2c09112 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit b60ee9f53a997838ba02510de40c609b17a3a728 +Subproject commit 8ac2c09112187d7819088e8300d713a7ab3de83c From 58df075c717fcc0984d1f37b4440f651f4ece399 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 29 Aug 2025 13:14:25 -0700 Subject: [PATCH 2/2] auto commit --- .../to_dafny.go | 6 +----- .../to_dafny.go | 18 +++--------------- .../to_dafny.go | 6 +----- .../to_dafny.go | 18 +++--------------- 4 files changed, 8 insertions(+), 40 deletions(-) diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go index cc97aab3a9..0d502826c9 100644 --- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go @@ -552,14 +552,10 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionInp func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionUnion_header_ToDafny(input []byte) Wrappers.Option { return func() Wrappers.Option { - v := make([]interface{}, 0, len(input)) if input == nil { return Wrappers.Companion_Option_.Create_None_() } - for _, e := range input { - v = append(v, e) - } - return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false)) + return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input)) }() } diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go index fb1a93d7c4..f50a53a598 100644 --- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go @@ -251,27 +251,19 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_AuthItem_data_ToDafny func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_value_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() } func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_typeId_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() } @@ -809,14 +801,10 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInp func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInput_headerBytes_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() } diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go index cc97aab3a9..0d502826c9 100644 --- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go @@ -552,14 +552,10 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionInp func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionUnion_header_ToDafny(input []byte) Wrappers.Option { return func() Wrappers.Option { - v := make([]interface{}, 0, len(input)) if input == nil { return Wrappers.Companion_Option_.Create_None_() } - for _, e := range input { - v = append(v, e) - } - return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false)) + return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input)) }() } diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go index fb1a93d7c4..f50a53a598 100644 --- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go @@ -251,27 +251,19 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_AuthItem_data_ToDafny func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_value_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() } func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_typeId_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() } @@ -809,14 +801,10 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInp func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInput_headerBytes_ToDafny(input []byte) dafny.Sequence { return func() dafny.Sequence { - v := make([]interface{}, 0, len(input)) if input == nil { return nil } - for _, e := range input { - v = append(v, e) - } - return dafny.SeqFromArray(v, false) + return dafny.SeqOfBytes(input) }() }