Skip to content

Commit e54400c

Browse files
ajewellamzajewellamz
committed
ResolveAuthActions
1 parent 782d91f commit e54400c

File tree

14 files changed

+695
-14
lines changed

14 files changed

+695
-14
lines changed

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

+61
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,14 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
9393
type Path = seq<PathSegment>
9494
datatype PathSegment =
9595
| member(member: StructureSegment)
96+
datatype ResolveAuthActionsInput = | ResolveAuthActionsInput (
97+
nameonly tableName: string ,
98+
nameonly authActions: AuthList ,
99+
nameonly headerBytes: seq<uint8>
100+
)
101+
datatype ResolveAuthActionsOutput = | ResolveAuthActionsOutput (
102+
nameonly cryptoActions: CryptoList
103+
)
96104
type StructuredDataMap = map<string, StructuredDataTerminal>
97105
datatype StructuredDataTerminal = | StructuredDataTerminal (
98106
nameonly value: TerminalValue ,
@@ -104,11 +112,13 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
104112
DecryptStructure := [];
105113
EncryptPathStructure := [];
106114
DecryptPathStructure := [];
115+
ResolveAuthActions := [];
107116
}
108117
ghost var EncryptStructure: seq<DafnyCallEvent<EncryptStructureInput, Result<EncryptStructureOutput, Error>>>
109118
ghost var DecryptStructure: seq<DafnyCallEvent<DecryptStructureInput, Result<DecryptStructureOutput, Error>>>
110119
ghost var EncryptPathStructure: seq<DafnyCallEvent<EncryptPathStructureInput, Result<EncryptPathStructureOutput, Error>>>
111120
ghost var DecryptPathStructure: seq<DafnyCallEvent<DecryptPathStructureInput, Result<DecryptPathStructureOutput, Error>>>
121+
ghost var ResolveAuthActions: seq<DafnyCallEvent<ResolveAuthActionsInput, Result<ResolveAuthActionsOutput, Error>>>
112122
}
113123
trait {:termination false} IStructuredEncryptionClient
114124
{
@@ -213,6 +223,21 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
213223
ensures DecryptPathStructureEnsuresPublicly(input, output)
214224
ensures History.DecryptPathStructure == old(History.DecryptPathStructure) + [DafnyCallEvent(input, output)]
215225

226+
predicate ResolveAuthActionsEnsuresPublicly(input: ResolveAuthActionsInput , output: Result<ResolveAuthActionsOutput, Error>)
227+
// The public method to be called by library consumers
228+
method ResolveAuthActions ( input: ResolveAuthActionsInput )
229+
returns (output: Result<ResolveAuthActionsOutput, Error>)
230+
requires
231+
&& ValidState()
232+
modifies Modifies - {History} ,
233+
History`ResolveAuthActions
234+
// Dafny will skip type parameters when generating a default decreases clause.
235+
decreases Modifies - {History}
236+
ensures
237+
&& ValidState()
238+
ensures ResolveAuthActionsEnsuresPublicly(input, output)
239+
ensures History.ResolveAuthActions == old(History.ResolveAuthActions) + [DafnyCallEvent(input, output)]
240+
216241
}
217242
datatype StructuredEncryptionConfig = | StructuredEncryptionConfig (
218243

@@ -394,6 +419,26 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionServic
394419
History.DecryptPathStructure := History.DecryptPathStructure + [DafnyCallEvent(input, output)];
395420
}
396421

422+
predicate ResolveAuthActionsEnsuresPublicly(input: ResolveAuthActionsInput , output: Result<ResolveAuthActionsOutput, Error>)
423+
{Operations.ResolveAuthActionsEnsuresPublicly(input, output)}
424+
// The public method to be called by library consumers
425+
method ResolveAuthActions ( input: ResolveAuthActionsInput )
426+
returns (output: Result<ResolveAuthActionsOutput, Error>)
427+
requires
428+
&& ValidState()
429+
modifies Modifies - {History} ,
430+
History`ResolveAuthActions
431+
// Dafny will skip type parameters when generating a default decreases clause.
432+
decreases Modifies - {History}
433+
ensures
434+
&& ValidState()
435+
ensures ResolveAuthActionsEnsuresPublicly(input, output)
436+
ensures History.ResolveAuthActions == old(History.ResolveAuthActions) + [DafnyCallEvent(input, output)]
437+
{
438+
output := Operations.ResolveAuthActions(config, input);
439+
History.ResolveAuthActions := History.ResolveAuthActions + [DafnyCallEvent(input, output)];
440+
}
441+
397442
}
398443
}
399444
abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations {
@@ -478,4 +523,20 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperat
478523
ensures
479524
&& ValidInternalConfig?(config)
480525
ensures DecryptPathStructureEnsuresPublicly(input, output)
526+
527+
528+
predicate ResolveAuthActionsEnsuresPublicly(input: ResolveAuthActionsInput , output: Result<ResolveAuthActionsOutput, Error>)
529+
// The private method to be refined by the library developer
530+
531+
532+
method ResolveAuthActions ( config: InternalConfig , input: ResolveAuthActionsInput )
533+
returns (output: Result<ResolveAuthActionsOutput, Error>)
534+
requires
535+
&& ValidInternalConfig?(config)
536+
modifies ModifiesInternalConfig(config)
537+
// Dafny will skip type parameters when generating a default decreases clause.
538+
decreases ModifiesInternalConfig(config)
539+
ensures
540+
&& ValidInternalConfig?(config)
541+
ensures ResolveAuthActionsEnsuresPublicly(input, output)
481542
}

‎DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy

+20-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ use aws.polymorph#localService
2222
)
2323
service StructuredEncryption {
2424
version: "2022-07-08",
25-
operations: [EncryptStructure, DecryptStructure, EncryptPathStructure, DecryptPathStructure],
25+
operations: [EncryptStructure, DecryptStructure, EncryptPathStructure, DecryptPathStructure, ResolveAuthActions],
2626
errors: [StructuredEncryptionException]
2727
}
2828

@@ -49,6 +49,11 @@ operation DecryptPathStructure {
4949
output: DecryptPathStructureOutput,
5050
}
5151

52+
operation ResolveAuthActions {
53+
input: ResolveAuthActionsInput,
54+
output: ResolveAuthActionsOutput,
55+
}
56+
5257
//= specification/structured-encryption/decrypt-path-structure.md#parsed-header
5358
//= type=implication
5459
//# This structure MUST contain the following values,
@@ -226,6 +231,20 @@ structure DecryptPathStructureOutput {
226231
parsedHeader: ParsedHeader,
227232
}
228233

234+
structure ResolveAuthActionsInput {
235+
@required
236+
tableName: String,
237+
@required
238+
authActions: AuthList,
239+
@required
240+
headerBytes: Blob
241+
}
242+
243+
structure ResolveAuthActionsOutput {
244+
@required
245+
cryptoActions: CryptoList,
246+
}
247+
229248
// Only handles bytes.
230249
// It is the responsibility of the caller to
231250
// serialize and deserialize the data they

‎DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

+15
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,21 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
8585
true
8686
}
8787

88+
predicate ResolveAuthActionsEnsuresPublicly(
89+
input: ResolveAuthActionsInput,
90+
output: Result<ResolveAuthActionsOutput, Error>) {
91+
true
92+
}
93+
94+
method ResolveAuthActions (config: InternalConfig, input: ResolveAuthActionsInput)
95+
returns (output: Result<ResolveAuthActionsOutput, Error>)
96+
{
97+
var head :- Header.PartialDeserialize(input.headerBytes);
98+
:- Need(ValidString(input.tableName), E("Bad Table Name"));
99+
var canonData :- CanonizeForDecrypt(input.tableName, input.authActions, head.legend);
100+
return Success(ResolveAuthActionsOutput(cryptoActions := UnCanon(canonData)));
101+
}
102+
88103
predicate method SameUnCanon(x : CanonCryptoItem, y : CryptoItem)
89104
{
90105
&& x.origKey == y.key

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/StructuredEncryption.java

+17
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@
1818
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.EncryptPathStructureOutput;
1919
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.EncryptStructureInput;
2020
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.EncryptStructureOutput;
21+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsInput;
22+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsOutput;
2123
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.StructuredEncryptionConfig;
2224

2325
public class StructuredEncryption {
@@ -100,6 +102,21 @@ public EncryptStructureOutput EncryptStructure(EncryptStructureInput input) {
100102
return ToNative.EncryptStructureOutput(result.dtor_value());
101103
}
102104

105+
public ResolveAuthActionsOutput ResolveAuthActions(
106+
ResolveAuthActionsInput input
107+
) {
108+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsInput dafnyValue =
109+
ToDafny.ResolveAuthActionsInput(input);
110+
Result<
111+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsOutput,
112+
Error
113+
> result = this._impl.ResolveAuthActions(dafnyValue);
114+
if (result.is_Failure()) {
115+
throw ToNative.Error(result.dtor_error());
116+
}
117+
return ToNative.ResolveAuthActionsOutput(result.dtor_value());
118+
}
119+
103120
protected IStructuredEncryptionClient impl() {
104121
return this._impl;
105122
}

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

+28
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@
3131
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.IStructuredEncryptionClient;
3232
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ParsedHeader;
3333
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.PathSegment;
34+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsInput;
35+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsOutput;
3436
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.StructureSegment;
3537
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.StructuredDataTerminal;
3638
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.StructuredEncryptionConfig;
@@ -394,6 +396,32 @@ public static ParsedHeader ParsedHeader(
394396
);
395397
}
396398

399+
public static ResolveAuthActionsInput ResolveAuthActionsInput(
400+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsInput nativeValue
401+
) {
402+
DafnySequence<? extends Character> tableName;
403+
tableName =
404+
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
405+
nativeValue.tableName()
406+
);
407+
DafnySequence<? extends AuthItem> authActions;
408+
authActions = ToDafny.AuthList(nativeValue.authActions());
409+
DafnySequence<? extends Byte> headerBytes;
410+
headerBytes =
411+
software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(
412+
nativeValue.headerBytes()
413+
);
414+
return new ResolveAuthActionsInput(tableName, authActions, headerBytes);
415+
}
416+
417+
public static ResolveAuthActionsOutput ResolveAuthActionsOutput(
418+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsOutput nativeValue
419+
) {
420+
DafnySequence<? extends CryptoItem> cryptoActions;
421+
cryptoActions = ToDafny.CryptoList(nativeValue.cryptoActions());
422+
return new ResolveAuthActionsOutput(cryptoActions);
423+
}
424+
397425
public static StructuredDataTerminal StructuredDataTerminal(
398426
software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.StructuredDataTerminal nativeValue
399427
) {

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/structuredencryption/ToNative.java

+32
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@
3232
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.OpaqueError;
3333
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ParsedHeader;
3434
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.PathSegment;
35+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsInput;
36+
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.ResolveAuthActionsOutput;
3537
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.StructureSegment;
3638
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.StructuredDataTerminal;
3739
import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.StructuredEncryptionConfig;
@@ -340,6 +342,36 @@ public static ParsedHeader ParsedHeader(
340342
return nativeBuilder.build();
341343
}
342344

345+
public static ResolveAuthActionsInput ResolveAuthActionsInput(
346+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsInput dafnyValue
347+
) {
348+
ResolveAuthActionsInput.Builder nativeBuilder =
349+
ResolveAuthActionsInput.builder();
350+
nativeBuilder.tableName(
351+
software.amazon.smithy.dafny.conversion.ToNative.Simple.String(
352+
dafnyValue.dtor_tableName()
353+
)
354+
);
355+
nativeBuilder.authActions(ToNative.AuthList(dafnyValue.dtor_authActions()));
356+
nativeBuilder.headerBytes(
357+
software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(
358+
dafnyValue.dtor_headerBytes()
359+
)
360+
);
361+
return nativeBuilder.build();
362+
}
363+
364+
public static ResolveAuthActionsOutput ResolveAuthActionsOutput(
365+
software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.ResolveAuthActionsOutput dafnyValue
366+
) {
367+
ResolveAuthActionsOutput.Builder nativeBuilder =
368+
ResolveAuthActionsOutput.builder();
369+
nativeBuilder.cryptoActions(
370+
ToNative.CryptoList(dafnyValue.dtor_cryptoActions())
371+
);
372+
return nativeBuilder.build();
373+
}
374+
343375
public static StructuredDataTerminal StructuredDataTerminal(
344376
software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.StructuredDataTerminal dafnyValue
345377
) {

0 commit comments

Comments
 (0)