Skip to content

Commit

Permalink
Merge branch 'main' into tony/chore-examples-postalHorn
Browse files Browse the repository at this point in the history
  • Loading branch information
texastony authored May 30, 2024
2 parents d260941 + 9db6e78 commit a150e6d
Show file tree
Hide file tree
Showing 5 changed files with 18 additions and 6 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci_verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ jobs:
uses: dafny-lang/[email protected]
with:
# A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.6.0' }}

- name: Regenerate code using smithy-dafny if necessary
if: ${{ inputs.nightly }}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -357,6 +357,9 @@ module DynamoToStruct {
&& U32ToBigEndian(|a.L|).Success?
&& |ret.value| >= PREFIX_LEN + LENGTH_LEN
&& ret.value[0..TYPEID_LEN] == SE.LIST
&& ListAttrToBytes(a.L, depth).Success?
&& ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value
&& ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value
&& ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
&& (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN)

Expand Down Expand Up @@ -492,6 +495,10 @@ module DynamoToStruct {
}

function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
ensures ret.Success? ==>
&& U32ToBigEndian(|l|).Success?
&& LENGTH_LEN <= |ret.value|
&& ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
{
var count :- U32ToBigEndian(|l|);
var body :- CollectList(l, depth);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,10 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
const RESERVED_PREFIX := "aws-crypto-attr."
const KEY_ATTR_NAME := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY)
const BRANCH_KEY_NAME := UTF8.EncodeAscii(BRANCH_KEY)

method {:test} TestHappyCase()
method {:test} {:vcs_split_on_every_assert} TestHappyCase()
{
var ddbKeyToBranchKeyId: Types.IDynamoDbKeyBranchKeyIdSupplier := new TestBranchKeyIdSupplier();
var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption();
Expand Down Expand Up @@ -80,27 +82,26 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
)
);

var keyAttrName := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY);

// Test Encryption Context with Case A
var materials :- expect mpl.InitializeEncryptionMaterials(
MPL.InitializeEncryptionMaterialsInput(
algorithmSuiteId := TEST_DBE_ALG_SUITE_ID,
encryptionContext := map[EC_PARTITION_NAME := UTF8.EncodeAscii(BRANCH_KEY)],
encryptionContext := map[EC_PARTITION_NAME := BRANCH_KEY_NAME],
requiredEncryptionContextKeys := [],
signingKey := None,
verificationKey := None
)
);

var caseA :- expect UTF8.Encode(Base64.Encode(CASE_A_BYTES));
var contextCaseA := materials.encryptionContext[keyAttrName := caseA];
var contextCaseA := materials.encryptionContext[KEY_ATTR_NAME := caseA];
var materialsA := materials.(encryptionContext := contextCaseA);
TestRoundtrip(hierarchyKeyring, materialsA, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_A);

// Test Encryption Context with Case B
var caseB :- expect UTF8.Encode(Base64.Encode(CASE_B_BYTES));
var contextCaseB := materials.encryptionContext[keyAttrName := caseB];
var contextCaseB := materials.encryptionContext[KEY_ATTR_NAME := caseB];
var materialsB := materials.(encryptionContext := contextCaseB);
TestRoundtrip(hierarchyKeyring, materialsB, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_B);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -667,6 +667,7 @@ module {:options "/functionSyntax:4" } Canonize {
forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
var x :| x in origData && Updated2(x, input[i], DoDecrypt);
}
assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
}

// command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false}
Expand All @@ -678,6 +679,7 @@ module {:options "/functionSyntax:4" } Canonize {
forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated5(x, input[i], DoEncrypt) {
var x :| x in origData && Updated5(x, input[i], DoEncrypt);
}
assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated5(x, input[i], DoEncrypt);
}

lemma CryptoUpdatedAuthMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,7 @@ module SortCanon {
ensures multiset(x) == multiset(result)
ensures SortedBy(result, AuthBelow)
ensures CanonAuthListHasNoDuplicates(result)
ensures |result| == |x|
{
AuthBelowIsTotal();
var ret := MergeSortBy(x, AuthBelow);
Expand All @@ -236,6 +237,7 @@ module SortCanon {
ensures multiset(result) == multiset(x)
ensures SortedBy(result, CryptoBelow)
ensures CanonCryptoListHasNoDuplicates(result)
ensures |result| == |x|
{
CryptoBelowIsTotal();
var ret := MergeSortBy(x, CryptoBelow);
Expand Down

0 comments on commit a150e6d

Please sign in to comment.