Skip to content

Commit c97ebff

Browse files
lucasmcdonald3lucasmcdonald3
committed
repoly
1 parent cfc3e01 commit c97ebff

File tree

16 files changed

+225
-27
lines changed

16 files changed

+225
-27
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,9 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
143143
&& output.value.branchKeyIdSupplier.ValidState()
144144
&& output.value.branchKeyIdSupplier.Modifies !! {History}
145145
&& fresh(output.value.branchKeyIdSupplier)
146-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
146+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
147+
- Modifies - {History}
148+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
147149
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
148150
ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
149151

@@ -474,7 +476,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
474476
// || (!exit(A(I)) && !access(B(I)))
475477
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
476478
// The Opaque error, used for native, extern, wrapped or unknown errors
477-
| Opaque(obj: object)
479+
| Opaque(obj: object, alt_text : string := "")
478480
type OpaqueError = e: Error | e.Opaque? witness *
479481
}
480482
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
@@ -535,7 +537,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
535537
&& output.value.branchKeyIdSupplier.ValidState()
536538
&& output.value.branchKeyIdSupplier.Modifies !! {History}
537539
&& fresh(output.value.branchKeyIdSupplier)
538-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - Modifies - {History} - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
540+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
541+
- Modifies - {History}
542+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
539543
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
540544
ensures History.CreateDynamoDbEncryptionBranchKeyIdSupplier == old(History.CreateDynamoDbEncryptionBranchKeyIdSupplier) + [DafnyCallEvent(input, output)]
541545
{
@@ -592,7 +596,9 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations {
592596
&& ( output.Success? ==>
593597
&& output.value.branchKeyIdSupplier.ValidState()
594598
&& fresh(output.value.branchKeyIdSupplier)
595-
&& fresh ( output.value.branchKeyIdSupplier.Modifies - ModifiesInternalConfig(config) - input.ddbKeyBranchKeyIdSupplier.Modifies ) )
599+
&& fresh ( output.value.branchKeyIdSupplier.Modifies
600+
- ModifiesInternalConfig(config)
601+
- input.ddbKeyBranchKeyIdSupplier.Modifies ) )
596602
ensures CreateDynamoDbEncryptionBranchKeyIdSupplierEnsuresPublicly(input, output)
597603

598604

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -728,7 +728,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
728728
// || (!exit(A(I)) && !access(B(I)))
729729
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
730730
// The Opaque error, used for native, extern, wrapped or unknown errors
731-
| Opaque(obj: object)
731+
| Opaque(obj: object, alt_text : string := "")
732732
type OpaqueError = e: Error | e.Opaque? witness *
733733
}
734734
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
159159
// || (!exit(A(I)) && !access(B(I)))
160160
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
161161
// The Opaque error, used for native, extern, wrapped or unknown errors
162-
| Opaque(obj: object)
162+
| Opaque(obj: object, alt_text : string := "")
163163
type OpaqueError = e: Error | e.Opaque? witness *
164164
}
165165
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService

‎DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -283,7 +283,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
283283
// || (!exit(A(I)) && !access(B(I)))
284284
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
285285
// The Opaque error, used for native, extern, wrapped or unknown errors
286-
| Opaque(obj: object)
286+
| Opaque(obj: object, alt_text : string := "")
287287
type OpaqueError = e: Error | e.Opaque? witness *
288288
}
289289
abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,11 +84,25 @@ public static Error Error(RuntimeException nativeValue) {
8484
if (nativeValue instanceof CollectionOfErrors) {
8585
return ToDafny.Error((CollectionOfErrors) nativeValue);
8686
}
87-
return Error.create_Opaque(nativeValue);
87+
return Error.create_Opaque(
88+
nativeValue,
89+
dafny.DafnySequence.asString(
90+
java.util.Objects.nonNull(nativeValue.getMessage())
91+
? nativeValue.getMessage()
92+
: ""
93+
)
94+
);
8895
}
8996

9097
public static Error Error(OpaqueError nativeValue) {
91-
return Error.create_Opaque(nativeValue.obj());
98+
return Error.create_Opaque(
99+
nativeValue.obj(),
100+
dafny.DafnySequence.asString(
101+
java.util.Objects.nonNull(nativeValue.altText())
102+
? nativeValue.altText()
103+
: ""
104+
)
105+
);
92106
}
93107

94108
public static Error Error(CollectionOfErrors nativeValue) {

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,25 @@ public static Error Error(RuntimeException nativeValue) {
4444
if (nativeValue instanceof CollectionOfErrors) {
4545
return ToDafny.Error((CollectionOfErrors) nativeValue);
4646
}
47-
return Error.create_Opaque(nativeValue);
47+
return Error.create_Opaque(
48+
nativeValue,
49+
dafny.DafnySequence.asString(
50+
java.util.Objects.nonNull(nativeValue.getMessage())
51+
? nativeValue.getMessage()
52+
: ""
53+
)
54+
);
4855
}
4956

5057
public static Error Error(OpaqueError nativeValue) {
51-
return Error.create_Opaque(nativeValue.obj());
58+
return Error.create_Opaque(
59+
nativeValue.obj(),
60+
dafny.DafnySequence.asString(
61+
java.util.Objects.nonNull(nativeValue.altText())
62+
? nativeValue.altText()
63+
: ""
64+
)
65+
);
5266
}
5367

5468
public static Error Error(CollectionOfErrors nativeValue) {

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/model/OpaqueError.java‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,14 @@ public class OpaqueError extends RuntimeException {
1010
*/
1111
private final Object obj;
1212

13+
/**
14+
* A best effort text representation of obj.
15+
*/
16+
private final String altText;
17+
1318
protected OpaqueError(BuilderImpl builder) {
1419
super(messageFromBuilder(builder), builder.cause());
20+
this.altText = builder.altText();
1521
this.obj = builder.obj();
1622
}
1723

@@ -46,6 +52,13 @@ public Object obj() {
4652
return this.obj;
4753
}
4854

55+
/**
56+
* @return A best effort text representation of obj.
57+
*/
58+
public String altText() {
59+
return this.altText;
60+
}
61+
4962
public Builder toBuilder() {
5063
return new BuilderImpl(this);
5164
}
@@ -85,6 +98,16 @@ public interface Builder {
8598
*/
8699
Object obj();
87100

101+
/**
102+
* @param altText A best effort text representation of obj.
103+
*/
104+
Builder altText(String altText);
105+
106+
/**
107+
* @return A best effort text representation of obj.
108+
*/
109+
String altText();
110+
88111
OpaqueError build();
89112
}
90113

@@ -96,6 +119,8 @@ static class BuilderImpl implements Builder {
96119

97120
protected Object obj;
98121

122+
protected String altText;
123+
99124
protected BuilderImpl() {}
100125

101126
protected BuilderImpl(OpaqueError model) {
@@ -131,6 +156,15 @@ public Object obj() {
131156
return this.obj;
132157
}
133158

159+
public Builder altText(String altText) {
160+
this.altText = altText;
161+
return this;
162+
}
163+
164+
public String altText() {
165+
return this.altText;
166+
}
167+
134168
public OpaqueError build() {
135169
if (
136170
this.obj != null && this.cause == null && this.obj instanceof Throwable

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/OpaqueError.java‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,14 @@ public class OpaqueError extends RuntimeException {
1010
*/
1111
private final Object obj;
1212

13+
/**
14+
* A best effort text representation of obj.
15+
*/
16+
private final String altText;
17+
1318
protected OpaqueError(BuilderImpl builder) {
1419
super(messageFromBuilder(builder), builder.cause());
20+
this.altText = builder.altText();
1521
this.obj = builder.obj();
1622
}
1723

@@ -46,6 +52,13 @@ public Object obj() {
4652
return this.obj;
4753
}
4854

55+
/**
56+
* @return A best effort text representation of obj.
57+
*/
58+
public String altText() {
59+
return this.altText;
60+
}
61+
4962
public Builder toBuilder() {
5063
return new BuilderImpl(this);
5164
}
@@ -85,6 +98,16 @@ public interface Builder {
8598
*/
8699
Object obj();
87100

101+
/**
102+
* @param altText A best effort text representation of obj.
103+
*/
104+
Builder altText(String altText);
105+
106+
/**
107+
* @return A best effort text representation of obj.
108+
*/
109+
String altText();
110+
88111
OpaqueError build();
89112
}
90113

@@ -96,6 +119,8 @@ static class BuilderImpl implements Builder {
96119

97120
protected Object obj;
98121

122+
protected String altText;
123+
99124
protected BuilderImpl() {}
100125

101126
protected BuilderImpl(OpaqueError model) {
@@ -131,6 +156,15 @@ public Object obj() {
131156
return this.obj;
132157
}
133158

159+
public Builder altText(String altText) {
160+
this.altText = altText;
161+
return this;
162+
}
163+
164+
public String altText() {
165+
return this.altText;
166+
}
167+
134168
public OpaqueError build() {
135169
if (
136170
this.obj != null && this.cause == null && this.obj instanceof Throwable

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToDafny.java‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -113,11 +113,25 @@ public static Error Error(RuntimeException nativeValue) {
113113
if (nativeValue instanceof CollectionOfErrors) {
114114
return ToDafny.Error((CollectionOfErrors) nativeValue);
115115
}
116-
return Error.create_Opaque(nativeValue);
116+
return Error.create_Opaque(
117+
nativeValue,
118+
dafny.DafnySequence.asString(
119+
java.util.Objects.nonNull(nativeValue.getMessage())
120+
? nativeValue.getMessage()
121+
: ""
122+
)
123+
);
117124
}
118125

119126
public static Error Error(OpaqueError nativeValue) {
120-
return Error.create_Opaque(nativeValue.obj());
127+
return Error.create_Opaque(
128+
nativeValue.obj(),
129+
dafny.DafnySequence.asString(
130+
java.util.Objects.nonNull(nativeValue.altText())
131+
? nativeValue.altText()
132+
: ""
133+
)
134+
);
121135
}
122136

123137
public static Error Error(CollectionOfErrors nativeValue) {

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/model/OpaqueError.java‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,14 @@ public class OpaqueError extends RuntimeException {
1010
*/
1111
private final Object obj;
1212

13+
/**
14+
* A best effort text representation of obj.
15+
*/
16+
private final String altText;
17+
1318
protected OpaqueError(BuilderImpl builder) {
1419
super(messageFromBuilder(builder), builder.cause());
20+
this.altText = builder.altText();
1521
this.obj = builder.obj();
1622
}
1723

@@ -46,6 +52,13 @@ public Object obj() {
4652
return this.obj;
4753
}
4854

55+
/**
56+
* @return A best effort text representation of obj.
57+
*/
58+
public String altText() {
59+
return this.altText;
60+
}
61+
4962
public Builder toBuilder() {
5063
return new BuilderImpl(this);
5164
}
@@ -85,6 +98,16 @@ public interface Builder {
8598
*/
8699
Object obj();
87100

101+
/**
102+
* @param altText A best effort text representation of obj.
103+
*/
104+
Builder altText(String altText);
105+
106+
/**
107+
* @return A best effort text representation of obj.
108+
*/
109+
String altText();
110+
88111
OpaqueError build();
89112
}
90113

@@ -96,6 +119,8 @@ static class BuilderImpl implements Builder {
96119

97120
protected Object obj;
98121

122+
protected String altText;
123+
99124
protected BuilderImpl() {}
100125

101126
protected BuilderImpl(OpaqueError model) {
@@ -131,6 +156,15 @@ public Object obj() {
131156
return this.obj;
132157
}
133158

159+
public Builder altText(String altText) {
160+
this.altText = altText;
161+
return this;
162+
}
163+
164+
public String altText() {
165+
return this.altText;
166+
}
167+
134168
public OpaqueError build() {
135169
if (
136170
this.obj != null && this.cause == null && this.obj instanceof Throwable

0 commit comments

Comments
 (0)