From 4783c09278d11c5bf5f2629010fe488a2724f3e9 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Tue, 22 Oct 2024 12:53:50 -0700
Subject: [PATCH 01/26] feat: Optimize sort by `Below`
The `Below` function is in the hot path.
The slice (x[1..]) operation is not optimized in Dafny.
This optimizes this function by turning the recursive slice
into a loop over an index into the seq.
Further, a bounded integer version is also included.
---
.../StructuredEncryption/src/SortCanon.dfy | 80 ++++++++++++++++++-
1 file changed, 79 insertions(+), 1 deletion(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
index 1033d899e..f9c977cbf 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
@@ -148,11 +148,89 @@ module SortCanon {
}
}
- predicate method Below(x: seq<uint8>, y: seq<uint8>) {
+ predicate Below(x: seq<uint8>, y: seq<uint8>) {
|x| != 0 ==>
&& |y| != 0
&& x[0] <= y[0]
&& (x[0] == y[0] ==> Below(x[1..], y[1..]))
+ } by method {
+
+ // The slice x[1..], y[1..] are un-optimized operations in Dafny.
+ // This means that their usage will result in a lot of data copying.
+ // Additional, it is very likely that these size of these sequences
+ // will be less than uint64.
+ // So writing an optimized version that only works on bounded types
+ // should further optimized this hot code.
+
+ if HasUint64Len(x) && HasUint64Len(y) {
+ return BoundedBelow(x,y);
+ }
+
+ if |x| == 0 {
+ assert Below(x, y);
+ return true;
+ }
+
+ if |y| == 0 {
+ assert !Below(x, y);
+ return false;
+ }
+
+ for i := 0 to |x|
+ invariant i <= |y|
+ // The function on the initial arguments
+ // is equal to function applied to the intermediate arguments.
+ invariant Below(x, y) == Below(x[i..], y[i..])
+ {
+ if |y| <= i {
+ return false;
+ } else if y[i] < x[i] {
+ return false;
+ } else if x[i] < y[i] {
+ return true;
+ } else {
+ assert x[i] == y[i];
+ }
+ }
+
+ return true;
+ }
+
+ predicate BoundedBelow(x: seq64<uint8>, y: seq64<uint8>)
+ {
+ Below(x,y)
+ } by method {
+ var xLength := |x| as uint64;
+ var yLength := |y| as uint64;
+
+ if xLength == 0 {
+ assert BoundedBelow(x, y);
+ return true;
+ }
+
+ if yLength == 0 {
+ assert !BoundedBelow(x, y);
+ return false;
+ }
+
+ for i := 0 to xLength
+ invariant i <= yLength
+ // The function on the initial arguments
+ // is equal to function applied to the intermediate arguments.
+ invariant BoundedBelow(x, y) == BoundedBelow(x[i..], y[i..])
+ {
+ if yLength <= i {
+ return false;
+ } else if y[i] < x[i] {
+ return false;
+ } else if x[i] < y[i] {
+ return true;
+ } else {
+ assert x[i] == y[i];
+ }
+ }
+
+ return true;
}
lemma BelowIsTotal()
From b4a071aac043179d4beeef22e57c3096df0452c7 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Sat, 26 Oct 2024 06:43:00 -0700
Subject: [PATCH 02/26] Compatability things
---
.../src/DynamoDbEncryptionBranchKeyIdSupplier.dfy | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
index 4533b8def..c79ca3294 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
@@ -70,7 +70,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
// We expect this interface to be implemented in the native language,
// so any errors thrown by the native implementation will appear as Opaque errors
if err.Opaque? then
- MPL.Opaque(obj:=err.obj)
+ MPL.Opaque(obj:=err.obj, alt_text:="")
else
MPL.AwsCryptographicMaterialProvidersException(message:="Unexpected error while getting Branch Key ID.")
}
From ea794cc2b84497c3d5781b66ebd988c6f319822f Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Thu, 31 Oct 2024 09:32:52 -0700
Subject: [PATCH 03/26] feat: Optimize sort by `MergeSort`
The `MergeSort` function is in the hot path.
The slice (x[1..]) operation is not optimized in Dafny.
This optimizes this function by turning the recursive slice
into a loop over an index into the seq.
Further, a bounded integer version is also included.
It also limits the total amount of data copied.
---
.../src/OptimizedMergeSort.dfy | 515 ++++++++++++++++++
.../StructuredEncryption/src/SortCanon.dfy | 16 +-
2 files changed, 529 insertions(+), 2 deletions(-)
create mode 100644 DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
new file mode 100644
index 000000000..a9b3d12a5
--- /dev/null
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -0,0 +1,515 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy"
+
+module {:options "-functionSyntax:4"} OptimizedMergeSort {
+ import Seq.MergeSort
+ import Relations = MergeSort.Relations
+ import opened StandardLibrary.UInt
+
+ // The Seq.MergeSort function implemented as implemented
+ // does not compile to an optimal implementation
+ // in any of the Dafny target languages.
+ // This implementation aims to be significantly more optimal.
+ // First, it minimizes copies.
+ // It does this by making 2 arrays of the original sequence
+ // and then using these 2 as left and right alternatively.
+ // This can be audited by verifying
+ // that the arrays are only sliced into a seq in `FastMergeSort`.
+ // All other slicing is done in ghost state.
+ // Second, is has a bounded number implementation
+ // that avoids using `nat`.
+
+ function {:isolate_assertions} FastMergeSort<T(!new)>(s: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ {
+ MergeSort.MergeSortBy(s, lessThanOrEq)
+ }
+ by method {
+ if |s| <= 1 {
+ return s;
+ } else {
+
+ // The slice x[1..], y[1..] are un-optimized operations in Dafny.
+ // This means that their usage will result in a lot of data copying.
+ // Additional, it is very likely that these size of these sequences
+ // will be less than uint64.
+ // So writing an optimized version that only works on bounded types
+ // should further optimized this hot code.
+
+ var left := new T[|s|](i requires 0 <= i < |s| => s[i]);
+ var right := new T[|s|](i requires 0 <= i < |s| => s[i]);
+ var lo, hi := 0, right.Length;
+
+ label BEFORE_WORK:
+
+ if HasUint64Len(s) {
+ var boundedLo: uint64, boundedHi: uint64 := 0, right.Length as uint64;
+ ghost var _ := BoundedMergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
+
+ result := right[..];
+ } else {
+ ghost var _ := MergeSortMethod(left, right, lessThanOrEq, lo, hi, Right);
+
+ result := right[..];
+ }
+
+ ghost var other := MergeSort.MergeSortBy(s, lessThanOrEq);
+
+ assert Relations.SortedBy(right[..], lessThanOrEq) by {
+ assert right[..] == right[lo..hi];
+ }
+ assert multiset(right[..]) == multiset(other) by {
+ calc {
+ multiset(right[..]);
+ == {assert right[..] == right[lo..hi];}
+ multiset(right[lo..hi]);
+ ==
+ multiset(old@BEFORE_WORK(left[lo..hi]));
+ == {assert old@BEFORE_WORK(left[lo..hi]) == s;}
+ multiset(s);
+ ==
+ multiset(other);
+ }
+ }
+
+ // Implementing a by method can be complicated.
+ // Because methods can have non-determinism,
+ // where functions can not.
+ // This means that Dafny normally wants to know
+ // that the method and function maintain equality at every step.
+ // But this is hard for this kind of optimized sorting.
+ // Because what is the functional state at every step
+ // and how does it correspond the state of 2 optimized arrays?
+ // This lemma works around this
+ // by proving that the outcomes are always deterministic and the same.
+ // It does this by proving that given a total ordering,
+ // there is one and only one way to sort a given sequence.
+ TotalOrderingImpliesSortingIsUnique(right[..], other, lessThanOrEq);
+ }
+ }
+
+ datatype PlaceResults = Left | Right | Either
+ type ResultPlacement = r: PlaceResults | !r.Either? witness *
+
+ method {:isolate_assertions} MergeSortMethod<T(!new)>(
+ left: array<T>,
+ right: array<T>,
+ lessThanOrEq: (T, T) -> bool,
+ lo: nat,
+ hi: nat,
+ where: PlaceResults
+ )
+ returns (resultPlacement: ResultPlacement)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires lo < hi <= left.Length
+ requires hi <= right.Length && left != right
+ // reads left, right
+ modifies left, right
+ ensures !where.Either? ==> where == resultPlacement
+
+ // We do not modify anything before lo
+ ensures left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ // We do not modify anything above hi
+ ensures left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+
+ ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
+ ensures resultPlacement.Left? ==> Relations.SortedBy(left[lo..hi], lessThanOrEq)
+ ensures resultPlacement.Right? ==> Relations.SortedBy(right[lo..hi], lessThanOrEq)
+ ensures resultPlacement.Right? ==> multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
+
+ decreases hi - lo
+ {
+ if hi - lo == 1 {
+ if where == Right {
+ right[lo] := left[lo];
+ return Right;
+ } else {
+ return Left;
+ }
+ }
+
+ ghost var beforeWork := multiset(left[lo..hi]);
+ var mid := (lo + hi) / 2;
+ var placement? := MergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
+ assert left[mid..hi] == old(left[mid..hi]);
+ ghost var placement2? := MergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
+ assert placement2? == placement?;
+
+ ghost var preMergeResult := if placement?.Left? then left else right;
+ calc {
+ multiset(preMergeResult[lo..hi]);
+ == { assert preMergeResult[lo..hi] == preMergeResult[lo..mid] + preMergeResult[mid..hi]; }
+ multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]);
+ ==
+ multiset(old(left[lo..mid]) + old(left[mid..hi]));
+ == { assert old(left[lo..hi]) == old(left[lo..mid]) + old(left[mid..hi]); }
+ beforeWork;
+ }
+
+ ghost var mergedResult;
+ if placement?.Left? {
+ MergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ resultPlacement := Right;
+
+ mergedResult := right[lo..hi];
+ assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ } else {
+ assert placement?.Right?;
+ MergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ resultPlacement := Left;
+
+ mergedResult := left[lo..hi];
+ assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ }
+
+ label BEFORE_RETURN:
+ assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
+ if resultPlacement.Left? && where == Right {
+ forall i | lo <= i < hi {
+ right[i] := left[i];
+ }
+
+ assert right[lo..hi] == mergedResult;
+ assert left[..] == old@BEFORE_RETURN(left[..]);
+ assert right[..lo] == old(right[..lo]);
+
+ resultPlacement := Right;
+ }
+ if resultPlacement.Right? && where == Left {
+ forall i | lo <= i < hi {
+ left[i] := right[i];
+ }
+
+ assert left[lo..hi] == mergedResult;
+ assert right[..] == old@BEFORE_RETURN(right[..]);
+ assert left[..lo] == old(left[..lo]);
+
+ resultPlacement := Left;
+ }
+ }
+
+ method {:isolate_assertions} MergeIntoRight<T(!new)>(
+ nameonly left: array<T>,
+ nameonly right: array<T>,
+ nameonly lessThanOrEq: (T, T) -> bool,
+ nameonly lo: nat,
+ nameonly mid: nat,
+ nameonly hi: nat
+ )
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires lo <= mid <= hi <= left.Length
+ requires hi <= right.Length && left != right
+ // We store "left" in [lo..mid]
+ requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
+ // We store "right" in [mid..hi]
+ requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
+ // reads left, right
+ modifies right
+ // We do not modify anything before lo
+ ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
+ // We do not modify anything above hi
+ ensures right[hi..] == old(right[hi..]) && left[..lo] == old(left[..lo])
+ ensures Relations.SortedBy(right[lo..hi], lessThanOrEq)
+ ensures multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
+ ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
+ {
+ var leftPosition, rightPosition, iter := lo, mid, lo;
+ while iter < hi
+ modifies right
+
+ invariant lo <= leftPosition <= mid <= rightPosition <= hi
+ invariant leftPosition - lo + rightPosition - mid == iter - lo
+ invariant right[..lo] == old(right[..lo])
+ invariant right[hi..] == old(right[hi..])
+
+ invariant Relations.SortedBy(left[leftPosition..mid], lessThanOrEq)
+ invariant Relations.SortedBy(left[rightPosition..hi], lessThanOrEq)
+ invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq)
+ invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq)
+ invariant Relations.SortedBy(right[lo..iter], lessThanOrEq)
+ invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition]) + multiset(left[mid..rightPosition])
+ {
+ if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
+ right[iter] := left[rightPosition];
+
+ PushStillSortedBy(right, lo, iter, lessThanOrEq);
+ rightPosition, iter := rightPosition + 1, iter + 1;
+
+ BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+ BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+ } else {
+ right[iter] := left[leftPosition];
+
+ PushStillSortedBy(right, lo, iter, lessThanOrEq);
+ leftPosition, iter := leftPosition + 1, iter + 1;
+
+ BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+ BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+ }
+ }
+ assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by {
+ assert leftPosition == mid && rightPosition == hi;
+ assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi];
+ }
+ }
+
+ // Helpers to prove MergeSort
+
+ ghost predicate Below<T(!new)>(a: seq<T>, b: seq<T>, lessThanOrEq: (T, T) -> bool)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ {
+ forall i, j :: 0 <= i < |a| && 0 <= j < |b| ==> lessThanOrEq(a[i], b[j])
+ }
+
+ lemma BelowIsTransitive<T(!new)>(a: seq<T>, b: seq<T>, lessThanOrEq: (T, T) -> bool)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires Relations.SortedBy(a, lessThanOrEq)
+ requires Relations.SortedBy(b, lessThanOrEq)
+ requires 0 < |a| && 0 < |b| ==> lessThanOrEq(a[|a| - 1], b[0])
+ ensures Below(a, b, lessThanOrEq)
+ {}
+
+ lemma PushStillSortedBy<T(!new)>(a: array<T>, lo:nat, i: nat, lessThanOrEq: (T, T) -> bool)
+ requires 0 <= lo <= i < a.Length
+ requires Relations.SortedBy(a[lo..i], lessThanOrEq)
+ requires |a[lo..i]| == 0 || lessThanOrEq(a[lo..i][|a[lo..i]| - 1], a[i])
+ requires Relations.TotalOrdering(lessThanOrEq)
+ ensures Relations.SortedBy(a[lo..i + 1], lessThanOrEq)
+ ensures lo < i ==> lessThanOrEq(a[i - 1], a[i])
+ {}
+
+ lemma {:isolate_assertions} TotalOrderingImpliesSortingIsUnique<T(!new)>(s1: seq<T>, s2: seq<T>, lessThanOrEq: (T, T) -> bool)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires Relations.SortedBy(s1, lessThanOrEq) && Relations.SortedBy(s2, lessThanOrEq)
+ requires multiset(s1) == multiset(s2)
+ ensures s1 == s2
+ {
+ if |s1| == 0 {
+ } else {
+ assert s1[0] in s2 by {
+ assert s1[0] in multiset(s2);
+ }
+
+ var i :| 0 <= i < |s2| && s2[i] == s1[0];
+ assert multiset{s1[0]} == multiset{s2[i]};
+ assert multiset{s1[0]} + multiset(s1[1..]) == multiset(s1) by {
+ assert s1 == [s1[0]] + s1[1..];
+ }
+ assert multiset{s2[i]} + multiset(s2[0..i] + s2[i+1..]) == multiset(s2) by {
+ assert s2 == s2[0..i] + [s2[i]] + s2[i+1..];
+ }
+
+ assert Relations.SortedBy(s1[1..], lessThanOrEq);
+ assert Relations.SortedBy(s2[0..i] + s2[i+1..], lessThanOrEq) by {
+ if i == 0 || i == |s2| - 1 {
+ } else {
+ assert lessThanOrEq(s2[i-1], s2[i]);
+ assert lessThanOrEq(s2[i], s2[i+1]);
+ }
+ }
+ MultisetProperty(multiset{s1[0]}, multiset(s1[1..]), multiset(s2[0..i] + s2[i+1..]));
+ TotalOrderingImpliesSortingIsUnique(s1[1..], s2[0..i] + s2[i+1..], lessThanOrEq);
+
+ if i == 0 {
+ } else {
+ assert s1 == [s2[i]] + s1[1..];
+ assert lessThanOrEq(s2[0], s2[i]);
+ assert s2[0] in s1;
+ }
+ }
+ }
+
+ lemma MultisetProperty(m: multiset, a: multiset, b: multiset)
+ requires m + a == m + b
+ ensures a == b
+ {
+ var a' := (m + a) - m;
+ var b' := (m + b) - m;
+ assert a == a' == b' == b;
+ }
+
+ // These are bounded implementations of the above.
+ // They do exactly the same thing,
+ // but they use `uint64`.
+ // This further speeds things up
+ // because math with bounded variables
+ // is significantly faster that math with big numbers.
+
+ method {:isolate_assertions} BoundedMergeSortMethod<T(!new)>(
+ left: array<T>,
+ right: array<T>,
+ lessThanOrEq: (T, T) -> bool,
+ lo: uint64,
+ hi: uint64,
+ where: PlaceResults
+ )
+ returns (resultPlacement: ResultPlacement)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires
+ && left.Length < UINT64_LIMIT
+ && right.Length < UINT64_LIMIT
+ requires lo < hi <= left.Length as uint64
+ requires hi <= right.Length as uint64 && left != right
+ // reads left, right
+ modifies left, right
+ ensures !where.Either? ==> where == resultPlacement
+
+ // We do not modify anything before lo
+ ensures left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ // We do not modify anything above hi
+ ensures left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+
+ ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
+ ensures resultPlacement.Left? ==> Relations.SortedBy(left[lo..hi], lessThanOrEq)
+ ensures resultPlacement.Right? ==> Relations.SortedBy(right[lo..hi], lessThanOrEq)
+ ensures resultPlacement.Right? ==> multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
+
+ decreases hi - lo
+ {
+ if hi - lo == 1 {
+ if where == Right {
+ right[lo] := left[lo];
+ return Right;
+ } else {
+ return Left;
+ }
+ }
+
+ ghost var beforeWork := multiset(left[lo..hi]);
+ var mid := ((hi - lo)/2) + lo;
+ var placement? := BoundedMergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
+ assert left[mid..hi] == old(left[mid..hi]);
+ ghost var placement2? := BoundedMergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
+ assert placement2? == placement?;
+
+ ghost var preMergeResult := if placement?.Left? then left else right;
+ calc {
+ multiset(preMergeResult[lo..hi]);
+ == { assert preMergeResult[lo..hi] == preMergeResult[lo..mid] + preMergeResult[mid..hi]; }
+ multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]);
+ ==
+ multiset(old(left[lo..mid]) + old(left[mid..hi]));
+ == { assert old(left[lo..hi]) == old(left[lo..mid]) + old(left[mid..hi]); }
+ beforeWork;
+ }
+
+ ghost var mergedResult;
+ if placement?.Left? {
+ BoundedMergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ resultPlacement, mergedResult := Right, right[lo..hi];
+
+ assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ } else {
+ assert placement?.Right?;
+ BoundedMergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ resultPlacement, mergedResult := Left, left[lo..hi];
+
+ assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ }
+
+ label BEFORE_RETURN:
+ assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
+ if resultPlacement.Left? && where == Right {
+ forall i | lo <= i < hi {
+ right[i] := left[i];
+ }
+
+ assert right[lo..hi] == mergedResult;
+ assert left[..] == old@BEFORE_RETURN(left[..]);
+ assert right[..lo] == old(right[..lo]);
+
+ resultPlacement := Right;
+ }
+ if resultPlacement.Right? && where == Left {
+ forall i | lo <= i < hi {
+ left[i] := right[i];
+ }
+ assert left[lo..hi] == mergedResult;
+ assert right[..] == old@BEFORE_RETURN(right[..]);
+ assert left[..lo] == old(left[..lo]);
+
+ resultPlacement := Left;
+ }
+ }
+
+ method {:isolate_assertions} BoundedMergeIntoRight<T(!new)>(
+ nameonly left: array<T>,
+ nameonly right: array<T>,
+ nameonly lessThanOrEq: (T, T) -> bool,
+ nameonly lo: uint64,
+ nameonly mid: uint64,
+ nameonly hi: uint64
+ )
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires
+ && left.Length < UINT64_LIMIT
+ && right.Length < UINT64_LIMIT
+ requires lo <= mid <= hi <= left.Length as uint64
+ requires hi <= right.Length as uint64 && left != right
+ // We store "left" in [lo..mid]
+ requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
+ // We store "right" in [mid..hi]
+ requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
+ // reads left, right
+ modifies right
+ // We do not modify anything before lo
+ ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
+ // We do not modify anything above hi
+ ensures right[hi..] == old(right[hi..]) && left[..lo] == old(left[..lo])
+ ensures Relations.SortedBy(right[lo..hi], lessThanOrEq)
+ ensures multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
+ ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
+ {
+ var leftPosition, rightPosition, iter := lo, mid, lo;
+ while iter < hi
+ modifies right
+
+ invariant lo <= leftPosition <= mid <= rightPosition <= hi
+ invariant leftPosition as nat - lo as nat + rightPosition as nat - mid as nat == iter as nat - lo as nat
+ invariant right[..lo] == old(right[..lo])
+ invariant right[hi..] == old(right[hi..])
+
+ invariant Relations.SortedBy(left[leftPosition..mid], lessThanOrEq)
+ invariant Relations.SortedBy(left[rightPosition..hi], lessThanOrEq)
+ invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq)
+ invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq)
+ invariant Relations.SortedBy(right[lo..iter], lessThanOrEq)
+ invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition]) + multiset(left[mid..rightPosition])
+ {
+ label BEFORE_WORK:
+ if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
+ right[iter] := left[rightPosition];
+
+ PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
+ rightPosition, iter := rightPosition + 1, iter + 1;
+
+ BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+
+ assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]);
+ BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+ } else {
+ right[iter] := left[leftPosition];
+
+ PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
+ leftPosition, iter := leftPosition + 1, iter + 1;
+
+ assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
+ if 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| {
+ assert lessThanOrEq(left[leftPosition-1], left[leftPosition]) by {
+ assert lo <= leftPosition-1 < leftPosition < mid;
+ assert Relations.SortedBy(left[lo..mid], lessThanOrEq);
+ }
+ }
+ }
+ BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+ BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+ }
+ }
+ assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by {
+ assert leftPosition == mid && rightPosition == hi;
+ assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi];
+ }
+ }
+}
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
index f9c977cbf..ae86e268b 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
@@ -3,6 +3,7 @@
include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy"
include "Util.dfy"
+include "OptimizedMergeSort.dfy"
module SortCanon {
export
@@ -22,6 +23,7 @@ module SortCanon {
import opened Relations
import opened Seq.MergeSort
import opened StructuredEncryptionUtil
+ import OptimizedMergeSort
predicate method AuthBelow(x: CanonAuthItem, y: CanonAuthItem) {
Below(x.key, y.key)
@@ -295,7 +297,7 @@ module SortCanon {
{}
- function method AuthSort(x : CanonAuthList) : (result : CanonAuthList)
+ function AuthSort(x : CanonAuthList) : (result : CanonAuthList)
requires CanonAuthListHasNoDuplicates(x)
ensures multiset(x) == multiset(result)
ensures SortedBy(result, AuthBelow)
@@ -307,9 +309,14 @@ module SortCanon {
CanonAuthListMultiNoDup(x, ret);
assert CanonAuthListHasNoDuplicates(ret);
ret
+ } by method {
+ AuthBelowIsTotal();
+ result := OptimizedMergeSort.FastMergeSort(x, AuthBelow);
+ CanonAuthListMultiNoDup(x, result);
+ assert CanonAuthListHasNoDuplicates(result);
}
- function method CryptoSort(x : CanonCryptoList) : (result : CanonCryptoList)
+ function CryptoSort(x : CanonCryptoList) : (result : CanonCryptoList)
requires CanonCryptoListHasNoDuplicates(x)
ensures multiset(x) == multiset(result)
ensures multiset(result) == multiset(x)
@@ -322,6 +329,11 @@ module SortCanon {
CanonCryptoListMultiNoDup(x, ret);
assert CanonCryptoListHasNoDuplicates(ret);
ret
+ } by method {
+ CryptoBelowIsTotal();
+ result := OptimizedMergeSort.FastMergeSort(x, CryptoBelow);
+ CanonCryptoListMultiNoDup(x, result);
+ assert CanonCryptoListHasNoDuplicates(result);
}
lemma MultisetHasNoDuplicates(xs: CanonCryptoList)
From a41a673416a91cf5c8b47395e24ca9e99f96d088 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Fri, 1 Nov 2024 13:08:12 -0700
Subject: [PATCH 04/26] roll back
---
.../src/DynamoDbEncryptionBranchKeyIdSupplier.dfy | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
index c79ca3294..4533b8def 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy
@@ -70,7 +70,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
// We expect this interface to be implemented in the native language,
// so any errors thrown by the native implementation will appear as Opaque errors
if err.Opaque? then
- MPL.Opaque(obj:=err.obj, alt_text:="")
+ MPL.Opaque(obj:=err.obj)
else
MPL.AwsCryptographicMaterialProvidersException(message:="Unexpected error while getting Branch Key ID.")
}
From 3aa38da1bd6683c86d4fbf54af31cb313fbdc912 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Fri, 1 Nov 2024 20:53:15 -0700
Subject: [PATCH 05/26] do not use for comprehension
---
.../src/OptimizedMergeSort.dfy | 25 +++++++++++++++----
1 file changed, 20 insertions(+), 5 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index a9b3d12a5..1bde8c058 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -85,7 +85,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
// This lemma works around this
// by proving that the outcomes are always deterministic and the same.
// It does this by proving that given a total ordering,
- // there is one and only one way to sort a given sequence.
+ // there is one and only one way to sort a given sequence.
TotalOrderingImpliesSortingIsUnique(right[..], other, lessThanOrEq);
}
}
@@ -412,21 +412,36 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
label BEFORE_RETURN:
assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
if resultPlacement.Left? && where == Right {
- forall i | lo <= i < hi {
+ for i := lo to hi
+ modifies right
+ invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+ invariant right[lo..i] == left[lo..i]
+ {
right[i] := left[i];
}
- assert right[lo..hi] == mergedResult;
+ assert right[lo..hi] == mergedResult by {
+ assert mergedResult == left[lo..hi];
+ }
assert left[..] == old@BEFORE_RETURN(left[..]);
assert right[..lo] == old(right[..lo]);
resultPlacement := Right;
}
if resultPlacement.Right? && where == Left {
- forall i | lo <= i < hi {
+ for i := lo to hi
+ modifies left
+ invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+ invariant left[lo..i] == right[lo..i]
+ {
left[i] := right[i];
}
- assert left[lo..hi] == mergedResult;
+
+ assert left[lo..hi] == mergedResult by {
+ assert mergedResult == right[lo..hi];
+ }
assert right[..] == old@BEFORE_RETURN(right[..]);
assert left[..lo] == old(left[..lo]);
From 63789b68bbaea65b1aa437741585b2dfbe6295fb Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Mon, 4 Nov 2024 09:59:05 -0800
Subject: [PATCH 06/26] update optimize
---
.../src/OptimizedMergeSort.dfy | 22 +++++++++++++++++--
1 file changed, 20 insertions(+), 2 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index 1bde8c058..5c5152a79 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -167,7 +167,12 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
label BEFORE_RETURN:
assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
if resultPlacement.Left? && where == Right {
- forall i | lo <= i < hi {
+ for i := lo to hi
+ modifies right
+ invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+ invariant right[lo..i] == left[lo..i]
+ {
right[i] := left[i];
}
@@ -178,7 +183,12 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
resultPlacement := Right;
}
if resultPlacement.Right? && where == Left {
- forall i | lo <= i < hi {
+ for i := lo to hi
+ modifies left
+ invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
+ invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
+ invariant left[lo..i] == right[lo..i]
+ {
left[i] := right[i];
}
@@ -412,6 +422,14 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
label BEFORE_RETURN:
assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
if resultPlacement.Left? && where == Right {
+ // A forall comprehension might seem like a nice fit here,
+ // however this does not good for two reasons.
+ // First, Dafny currently creates a range fur the full bounds of the bounded number
+ // see: https://github.com/dafny-lang/dafny/issues/5897
+ // Second this would create two loops.
+ // First loop would create the `lo to hi` range of numbers.
+ // The second loop would then loop over these elements.
+ // A single loop with
for i := lo to hi
modifies right
invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
From d83759abe9a5fdfac7bf9388a406d29c5d648f48 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Tue, 4 Feb 2025 16:07:23 -0800
Subject: [PATCH 07/26] chore: make EncodeAscii ghost
---
.../dafny/DynamoDbEncryption/test/Beacon.dfy | 7 ++-
...amoDbEncryptionBranchKeyIdSupplierTest.dfy | 26 ++++++++--
...moDbGetEncryptedDataKeyDescriptionTest.dfy | 51 ++++++++++++++++---
.../src/DynamoDbMiddlewareSupport.dfy | 5 +-
.../dafny/DynamoDbItemEncryptor/src/Util.dfy | 17 +++++--
.../test/DynamoDBItemEncryptorTest.dfy | 5 +-
.../dafny/StructuredEncryption/src/Crypt.dfy | 20 ++++++--
.../dafny/StructuredEncryption/src/Footer.dfy | 24 ++++++---
.../dafny/StructuredEncryption/src/Util.dfy | 42 ++++++++++++---
.../test/HappyCaseTests.dfy | 12 ++++-
.../StructuredEncryption/test/Header.dfy | 36 +++++++++++--
.../dafny/StructuredEncryption/test/Paths.dfy | 30 +++++------
.../dafny/DDBEncryption/src/JsonConfig.dfy | 9 +++-
submodules/MaterialProviders | 2 +-
14 files changed, 223 insertions(+), 63 deletions(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy
index a812cdc0e..e0579c635 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy
@@ -18,6 +18,11 @@ module TestBaseBeacon {
import DDB = ComAmazonawsDynamodbTypes
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
+ const x123 : UTF8.ValidUTF8Bytes :=
+ var s := [0x31, 0x32, 0x33];
+ assert s == UTF8.EncodeAscii("123");
+ s
+
method {:test} TestBeacon() {
var primitives :- expect Primitives.AtomicPrimitives();
@@ -31,7 +36,7 @@ module TestBaseBeacon {
expect bytes[7] == 0x80;
str :- expect b.hash([], key := [1,2]);
expect str == "80";
- bytes :- expect bb.getHmac(UTF8.EncodeAscii("123"), key := [1,2]);
+ bytes :- expect bb.getHmac(x123, key := [1,2]);
expect bytes[7] == 0x61;
}
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
index 74e12264f..63cb0b9c3 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
@@ -27,7 +27,12 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
// These tests require a keystore populated with a key with this Id
const BRANCH_KEY_ID := "75789115-1deb-4fe3-a2ec-be9e885d1945"
- const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
+
+ const BRANCH_KEY_ID_UTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x37, 0x35, 0x37, 0x38, 0x39, 0x31, 0x31, 0x35, 0x2d, 0x31, 0x64, 0x65, 0x62, 0x2d, 0x34, 0x66, 0x65, 0x33, 0x2d, 0x61, 0x32, 0x65, 0x63, 0x2d, 0x62, 0x65, 0x39, 0x65, 0x38, 0x38, 0x35, 0x64, 0x31, 0x39, 0x34, 0x35];
+ assert s == UTF8.EncodeAscii(BRANCH_KEY_ID);
+ s
+
const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
// Constants for TestBranchKeySupplier
@@ -41,10 +46,23 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42]
const BRANCH_KEY_ID_A := BRANCH_KEY_ID
const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
- const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
+
+ const EC_PARTITION_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x61, 0x72, 0x74, 0x69, 0x74, 0x69, 0x6f, 0x6e, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("aws-crypto-partition-name");
+ s
+
const RESERVED_PREFIX := "aws-crypto-attr."
- const KEY_ATTR_NAME := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY)
- const BRANCH_KEY_NAME := UTF8.EncodeAscii(BRANCH_KEY)
+
+ const KEY_ATTR_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x61, 0x74, 0x74, 0x72, 0x2e, 0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
+ assert s == UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY);
+ s
+
+ const BRANCH_KEY_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
+ assert s == UTF8.EncodeAscii(BRANCH_KEY);
+ s
method {:test} {:vcs_split_on_every_assert} TestHappyCase()
{
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
index 2f5cb02a8..91633e3db 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
@@ -14,20 +14,55 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
import EdkWrapping
import AlgorithmSuites
+ const abc : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x62, 0x63];
+ assert s == UTF8.EncodeAscii("abc");
+ s
+
+ const def : UTF8.ValidUTF8Bytes :=
+ var s := [0x64, 0x65, 0x66];
+ assert s == UTF8.EncodeAscii("def");
+ s
+
+ const awskms : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73];
+ assert s == UTF8.EncodeAscii("aws-kms");
+ s
+
+ const keyproviderInfo : UTF8.ValidUTF8Bytes :=
+ var s := [0x6b, 0x65, 0x79, 0x70, 0x72, 0x6f, 0x76, 0x69, 0x64, 0x65, 0x72, 0x49, 0x6e, 0x66, 0x6f];
+ assert s == UTF8.EncodeAscii("keyproviderInfo");
+ s
+
+ const aws_kms_hierarchy : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
+ assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
+ s
+
+ const raw_rsa : UTF8.ValidUTF8Bytes :=
+ var s := [0x72, 0x61, 0x77, 0x2d, 0x72, 0x73, 0x61];
+ assert s == UTF8.EncodeAscii("raw-rsa");
+ s
+
+ const aws_kms_rsa : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x72, 0x73, 0x61];
+ assert s == UTF8.EncodeAscii("aws-kms-rsa");
+ s
+
// THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
const testVersion : Version := 1
const testFlavor0 : Flavor := 0
const testFlavor1 : Flavor := 1
const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]
const testLegend : Legend := [0x65, 0x73]
- const testEncContext : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def")]
+ const testEncContext : CMPEncryptionContext := map[abc := def]
const testAwsKmsDataKey := CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("aws-kms") ,
- keyProviderInfo := EncodeAscii("keyproviderInfo"),
+ keyProviderId := awskms ,
+ keyProviderInfo := keyproviderInfo,
ciphertext := [1, 2, 3, 4, 5])
const testAwsKmsHDataKey := CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
- keyProviderInfo := EncodeAscii("keyproviderInfo"),
+ keyProviderId := aws_kms_hierarchy,
+ keyProviderInfo := keyproviderInfo,
ciphertext := [
64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34,
11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122,
@@ -40,12 +75,12 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])
const testRawRsaDataKey := CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("raw-rsa") ,
+ keyProviderId := raw_rsa,
keyProviderInfo := [1, 2, 3, 4, 5],
ciphertext := [6, 7, 8, 9])
const testAwsKmsRsaDataKey := CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("aws-kms-rsa") ,
- keyProviderInfo := EncodeAscii("keyproviderInfo"),
+ keyProviderId := aws_kms_rsa,
+ keyProviderInfo := keyproviderInfo,
ciphertext := [1, 2, 3, 4, 5])
method CreatePartialHeader(version : Version, flavor : Flavor, msgID : MessageID, legend : Legend, encContext : CMPEncryptionContext, dataKeyList : CMPEncryptedDataKeyList)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
index 8d2ce7e19..ab5524224 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
@@ -121,7 +121,10 @@ module DynamoDbMiddlewareSupport {
.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e))
}
- const HierarchicalKeyringId := UTF8.EncodeAscii("aws-kms-hierarchy")
+ const HierarchicalKeyringId : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
+ assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
+ s
// Return Beacon Key ID for use in beaconizing records to be written
function method GetKeyIdFromHeader(config : ValidTableConfig, output : AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.EncryptItemOutput) :
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
index 1c1233d71..08ba1fef9 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
@@ -35,9 +35,20 @@ module DynamoDbItemEncryptorUtil {
x < y
}
- const TABLE_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-table-name")
- const PARTITION_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-partition-name")
- const SORT_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-sort-name")
+ const TABLE_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x74, 0x61, 0x62, 0x6c, 0x65, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("aws-crypto-table-name");
+ s
+
+ const PARTITION_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x61, 0x72, 0x74, 0x69, 0x74, 0x69, 0x6f, 0x6e, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("aws-crypto-partition-name");
+ s
+
+ const SORT_NAME : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x73, 0x6f, 0x72, 0x74, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("aws-crypto-sort-name");
+ s
const SELECTOR_TABLE_NAME : DDB.AttributeName := "aws_dbe_table_name"
const SELECTOR_PARTITION_NAME : DDB.AttributeName := "aws_dbe_partition_name"
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
index aa4dfaa65..6ec3f8a4c 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
@@ -25,7 +25,10 @@ module DynamoDbItemEncryptorTest {
// encrypt => encrypted fields changed, others did not
// various errors
- const PublicKeyUtf8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-public-key")
+ const PublicKeyUtf8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x75, 0x62, 0x6c, 0x69, 0x63, 0x2d, 0x6b, 0x65, 0x79];
+ assert s == UTF8.EncodeAscii("aws-crypto-public-key");
+ s
function method DDBS(x : string) : DDB.AttributeValue {
DDB.AttributeValue.S(x)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
index f8c178764..54609b0ec 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
@@ -49,6 +49,11 @@ module StructuredEncryptionCrypt {
keyR.MapFailure(e => AwsCryptographyPrimitives(e))
}
+ const AwsDbeField : UTF8.ValidUTF8Bytes :=
+ var s := [0x41, 0x77, 0x73, 0x44, 0x62, 0x65, 0x46, 0x69, 0x65, 0x6c, 0x64];
+ assert s == UTF8.EncodeAscii("AwsDbeField");
+ s
+
function method FieldKeyNonce(offset : uint32)
: (ret : Bytes)
ensures |ret| == 16 // NOT NonceSize
@@ -61,17 +66,24 @@ module StructuredEncryptionCrypt {
//# | 0x2c | 1 | 44, the length of the eventual FieldKey |
//# | offset | 4 | 32 bit integer representation of offset |
ensures ret ==
- UTF8.EncodeAscii("AwsDbeField")
+ AwsDbeField
+ [(KeySize+NonceSize) as uint8]
+ UInt32ToSeq(offset)
{
- UTF8.EncodeAscii("AwsDbeField")
+ AwsDbeField
+ [(KeySize+NonceSize) as uint8] // length
+ UInt32ToSeq(offset)
}
- const LABEL_COMMITMENT_KEY := UTF8.EncodeAscii("AWS_DBE_COMMIT_KEY")
- const LABEL_ENCRYPTION_KEY := UTF8.EncodeAscii("AWS_DBE_DERIVE_KEY")
+ const LABEL_COMMITMENT_KEY : UTF8.ValidUTF8Bytes :=
+ var s := [0x41, 0x57, 0x53, 0x5f, 0x44, 0x42, 0x45, 0x5f, 0x43, 0x4f, 0x4d, 0x4d, 0x49, 0x54, 0x5f, 0x4b, 0x45, 0x59];
+ assert s == UTF8.EncodeAscii("AWS_DBE_COMMIT_KEY");
+ s
+
+ const LABEL_ENCRYPTION_KEY : UTF8.ValidUTF8Bytes :=
+ var s := [0x41, 0x57, 0x53, 0x5f, 0x44, 0x42, 0x45, 0x5f, 0x44, 0x45, 0x52, 0x49, 0x56, 0x45, 0x5f, 0x4b, 0x45, 0x59];
+ assert s == UTF8.EncodeAscii("AWS_DBE_DERIVE_KEY");
+ s
// suitable for header field
method GetCommitKey(
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
index 6c7f537ee..9239ad4cb 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
@@ -140,16 +140,28 @@ module StructuredEncryptionFooter {
}
}
+ const ENCRYPTED : UTF8.ValidUTF8Bytes :=
+ var s := [0x45, 0x4e, 0x43, 0x52, 0x59, 0x50, 0x54, 0x45, 0x44];
+ assert s == UTF8.EncodeAscii("ENCRYPTED");
+ s
+
+ const PLAINTEXT : UTF8.ValidUTF8Bytes :=
+ var s := [0x50, 0x4c, 0x41, 0x49, 0x4e, 0x54, 0x45, 0x58, 0x54];
+ assert s == UTF8.EncodeAscii("PLAINTEXT");
+ s
+
+
+
// Given a StructuredDataTerminal, return the canonical value for the type, for use in the footer checksum calculations
function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool)
: Result<Bytes, Error>
{
if isEncrypted then
:- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
- Success(UInt64ToSeq((|value.value| - 2) as uint64) + UTF8.EncodeAscii("ENCRYPTED"))
+ Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED)
else
:- Need(|value.value| < UINT64_LIMIT, E("Bad length."));
- Success(UInt64ToSeq((|value.value|) as uint64) + UTF8.EncodeAscii("PLAINTEXT") + value.typeId)
+ Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId)
}
function method GetCanonicalEncryptedField(fieldName : CanonicalPath, value : StructuredDataTerminal)
@@ -169,14 +181,14 @@ module StructuredEncryptionFooter {
&& ret.value ==
fieldName
+ UInt64ToSeq((|value.value| - 2) as uint64)
- + UTF8.EncodeAscii("ENCRYPTED")
+ + ENCRYPTED
+ value.value // this is 2 bytes of unencrypted type, followed by encrypted value
{
:- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
Success(
fieldName
+ UInt64ToSeq((|value.value| - 2) as uint64)
- + UTF8.EncodeAscii("ENCRYPTED")
+ + ENCRYPTED
+ value.value
)
}
@@ -198,7 +210,7 @@ module StructuredEncryptionFooter {
&& ret.value ==
fieldName
+ UInt64ToSeq((|value.value|) as uint64)
- + UTF8.EncodeAscii("PLAINTEXT")
+ + PLAINTEXT
+ value.typeId
+ value.value
{
@@ -206,7 +218,7 @@ module StructuredEncryptionFooter {
Success(
fieldName
+ UInt64ToSeq((|value.value|) as uint64)
- + UTF8.EncodeAscii("PLAINTEXT")
+ + PLAINTEXT
+ value.typeId
+ value.value
)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
index fecdcad0a..93e36cd56 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
@@ -26,23 +26,48 @@ module StructuredEncryptionUtil {
const FooterPath : Path := [member(StructureSegment(key := FooterField))]
const HeaderPaths : seq<Path> := [HeaderPath, FooterPath]
const ReservedCryptoContextPrefixString := "aws-crypto-"
- const ReservedCryptoContextPrefixUTF8 := UTF8.EncodeAscii(ReservedCryptoContextPrefixString)
+
+ const ReservedCryptoContextPrefixUTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d];
+ assert s == UTF8.EncodeAscii(ReservedCryptoContextPrefixString);
+ s
const ATTR_PREFIX := ReservedCryptoContextPrefixString + "attr."
- const EC_ATTR_PREFIX : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(ATTR_PREFIX)
+
+ const EC_ATTR_PREFIX : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x61, 0x74, 0x74, 0x72, 0x2e];
+ assert s == UTF8.EncodeAscii(ATTR_PREFIX);
+ s
+
const LEGEND := ReservedCryptoContextPrefixString + "legend"
- const LEGEND_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(LEGEND)
+
+ const LEGEND_UTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x6c, 0x65, 0x67, 0x65, 0x6e, 0x64];
+ assert s == UTF8.EncodeAscii(LEGEND);
+ s
+
const LEGEND_STRING : char := 'S'
const LEGEND_NUMBER : char := 'N'
const LEGEND_LITERAL : char := 'L'
const LEGEND_BINARY : char := 'B'
const NULL_STR : string := "null"
- const NULL_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(NULL_STR)
+ const NULL_UTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x6e, 0x75, 0x6c, 0x6c];
+ assert s == UTF8.EncodeAscii(NULL_STR);
+ s
+
const TRUE_STR : string := "true"
- const TRUE_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(TRUE_STR)
+ const TRUE_UTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x74, 0x72, 0x75, 0x65];
+ assert s == UTF8.EncodeAscii(TRUE_STR);
+ s
+
const FALSE_STR : string := "false"
- const FALSE_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(FALSE_STR)
+ const FALSE_UTF8 : UTF8.ValidUTF8Bytes :=
+ var s := [0x66, 0x61, 0x6c, 0x73, 0x65];
+ assert s == UTF8.EncodeAscii(FALSE_STR);
+ s
datatype CanonCryptoItem = CanonCryptoItem (
key : CanonicalPath,
@@ -290,9 +315,10 @@ module StructuredEncryptionUtil {
//# where `typeId` is the attribute's [type ID](./ddb-attribute-serialization.md#type-id)
//# and `serializedValue` is the attribute's value serialized according to
//# [Attribute Value Serialization](./ddb-attribute-serialization.md#attribute-value-serialization).
- ensures ret == UTF8.EncodeAscii(Base64.Encode(t.typeId + t.value))
+ ensures ret == UTF8.Encode(Base64.Encode(t.typeId + t.value)).value
{
- UTF8.EncodeAscii(Base64.Encode(t.typeId + t.value))
+ var base := Base64.Encode(t.typeId + t.value);
+ UTF8.Encode(base).value
}
function method DecodeTerminal(t : UTF8.ValidUTF8Bytes) : (ret : Result<StructuredDataTerminal, string>)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy
index 7c41f025c..b498fa212 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy
@@ -13,12 +13,22 @@ module HappyCaseTests {
import MaterialProviders
import StructuredDataTestFixtures
+ const some : UTF8.ValidUTF8Bytes :=
+ var s := [0x73, 0x6f, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("some");
+ s
+
+ const value : UTF8.ValidUTF8Bytes :=
+ var s := [0x76, 0x61, 0x6c, 0x75, 0x65];
+ assert s == UTF8.EncodeAscii("value");
+ s
+
method {:test} TestRoundTrip() {
var structuredEncryption :-
expect StructuredEncryption.StructuredEncryption(StructuredEncryption.DefaultStructuredEncryptionConfig());
var cmm := StructuredDataTestFixtures.GetDefaultCMMWithKMSKeyring();
- var encContext := map[UTF8.EncodeAscii("some") := UTF8.EncodeAscii("value")];
+ var encContext := map[some := value];
var algSuiteId := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384.id.DBE;
assert && structuredEncryption.ValidState();
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
index be8905c86..fbd200499 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
@@ -21,15 +21,41 @@ module TestHeader {
import AlgorithmSuites
import Canonize
+ const abc : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x62, 0x63];
+ assert s == UTF8.EncodeAscii("abc");
+ s
+
+ const def : UTF8.ValidUTF8Bytes :=
+ var s := [0x64, 0x65, 0x66];
+ assert s == UTF8.EncodeAscii("def");
+ s
+
+ const cba : UTF8.ValidUTF8Bytes :=
+ var s := [0x63, 0x62, 0x61];
+ assert s == UTF8.EncodeAscii("cba");
+ s
+
+ const fed : UTF8.ValidUTF8Bytes :=
+ var s := [0x66, 0x65, 0x64];
+ assert s == UTF8.EncodeAscii("fed");
+ s
+
+ const provID : UTF8.ValidUTF8Bytes :=
+ var s := [0x70, 0x72, 0x6f, 0x76, 0x49, 0x44];
+ assert s == UTF8.EncodeAscii("provID");
+ s
+
+
method {:test} TestRoundTrip() {
var head := PartialHeader (
version := 1,
flavor := 1,
msgID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32],
legend := [0x65, 0x73],
- encContext := map[EncodeAscii("abc") := EncodeAscii("def")],
+ encContext := map[abc := def],
dataKeys := [CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("provID") ,
+ keyProviderId := provID,
keyProviderInfo := [1,2,3,4,5],
ciphertext := [6,7,8,9])]
);
@@ -45,9 +71,9 @@ module TestHeader {
flavor := 1,
msgID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32],
legend := [0x65, 0x73],
- encContext := map[EncodeAscii("abc") := EncodeAscii("def")],
+ encContext := map[abc := def],
dataKeys := [CMP.EncryptedDataKey(
- keyProviderId := EncodeAscii("provID") ,
+ keyProviderId := provID,
keyProviderInfo := [1,2,3,4,5],
ciphertext := [6,7,8,9])]
);
@@ -76,7 +102,7 @@ module TestHeader {
const e : uint8 := 'e' as uint8
const f : uint8 := 'f' as uint8
method {:test} TestDuplicateContext() {
- var cont : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def"), EncodeAscii("cba") := EncodeAscii("fed")];
+ var cont : CMPEncryptionContext := map[abc := def, cba := fed];
var serCont := SerializeContext(cont);
expect serCont == [
0,2, // two items
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy
index 63726a18d..ce3c1704b 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Paths.dfy
@@ -9,31 +9,25 @@ module PathsTests {
import opened StructuredEncryptionUtil
import opened StructuredEncryptionPaths
+ const example_table : UTF8.ValidUTF8Bytes :=
+ var s := [0x65, 0x78, 0x61, 0x6d, 0x70, 0x6c, 0x65, 0x5f, 0x74, 0x61, 0x62, 0x6c, 0x65];
+ assert s == UTF8.EncodeAscii("example_table");
+ s
+
+ const name : UTF8.ValidUTF8Bytes :=
+ var s := [0x6e, 0x61, 0x6d, 0x65];
+ assert s == UTF8.EncodeAscii("name");
+ s
+
method {:test} TestSpecExamples() {
var tableName : GoodString := "example_table";
assert(ValidString("example_table"));
var pathToTest := StringToUniPath("name");
expect CanonPath(tableName, pathToTest) ==
- UTF8.EncodeAscii("example_table")
+ example_table
+ [0,0,0,0,0,0,0,1] // depth
+ ['$' as uint8] // map
+ [0,0,0,0,0,0,0,4] // length
- + UTF8.EncodeAscii("name");
-
- // var history := Selector.Map("status-history");
- // var index := Selector.List(0);
- // var timestamp := Selector.Map("timestamp");
- // var pathToTest2 := TerminalLocation([history, index, timestamp]);
- // expect CanonPath(tableName, pathToTest2) ==
- // UTF8.EncodeAscii("example_table")
- // + [0,0,0,0,0,0,0,3] // depth
- // + ['$' as uint8] // map
- // + [0,0,0,0,0,0,0,14] // length of "status-history"
- // + UTF8.EncodeAscii("status-history")
- // + ['#' as uint8] // array
- // + [0,0,0,0,0,0,0,0] // index
- // + ['$' as uint8] // map
- // + [0,0,0,0,0,0,0,9] // length of "timestamp"
- // + UTF8.EncodeAscii("timestamp");
+ + name;
}
}
diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
index 46605a425..b39125129 100644
--- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
@@ -33,6 +33,11 @@ module {:options "-functionSyntax:4"} JsonConfig {
import DynamoDbItemEncryptor
+ const abc : UTF8.ValidUTF8Bytes :=
+ var s := [0x61, 0x62, 0x63];
+ assert s == UTF8.EncodeAscii("abc");
+ s
+
const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000}
@@ -483,7 +488,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
:- Need(|standardBeacons| > 0, "A Search Config needs at least one standard beacon.");
var keyMaterial : KeyMaterial.KeyMaterial :=
- KeyMaterial.StaticKeyStoreInformation("abc", UTF8.EncodeAscii("abc"), [1,2,3,4,5], [1,2,3,4,5]);
+ KeyMaterial.StaticKeyStoreInformation("abc", abc, [1,2,3,4,5], [1,2,3,4,5]);
var store := SKS.CreateStaticKeyStore(keyMaterial);
var source : Types.BeaconKeySource :=
if keySource.Some? then
@@ -508,7 +513,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
ensures output.Success? ==> output.value.ValidState() && fresh(output.value.Modifies())
{
var keyMaterial : KeyMaterial.KeyMaterial :=
- KeyMaterial.StaticKeyStoreInformation("abc", UTF8.EncodeAscii("abc"), [1,2,3,4,5], [1,2,3,4,5]);
+ KeyMaterial.StaticKeyStoreInformation("abc", abc, [1,2,3,4,5], [1,2,3,4,5]);
var store := SKS.CreateStaticKeyStore(keyMaterial);
var source : Types.BeaconKeySource := Types.single(Types.SingleKeyStore(keyId := "foo", cacheTTL := 42));
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 5808fbfd1..786404f1d 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 5808fbfd13ed12eb258883010626e1ae75708089
+Subproject commit 786404f1d1bdf86814c5018ce0b3b1149ef65b3e
From bd9d7bef24c10c95a8ceb9efe8c2d23636c5d76f Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Thu, 6 Feb 2025 11:07:51 -0800
Subject: [PATCH 08/26] m
---
...ptionSdkStructuredEncryptionOperations.dfy | 13 ++++-
.../dafny/StructuredEncryption/src/Footer.dfy | 50 ++++++++++++++++---
2 files changed, 54 insertions(+), 9 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
index e2aef0b72..fffc07f73 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
@@ -127,7 +127,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
}
// Return the sum of the sizes of the given fields
- function method {:opaque} SumValueSize(fields : CanonCryptoList)
+ function {:opaque} SumValueSize(fields : CanonCryptoList)
: nat
{
if |fields| == 0 then
@@ -136,6 +136,17 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
|fields[0].data.value| + SumValueSize(fields[1..])
else
SumValueSize(fields[1..])
+ } by method {
+ reveal SumValueSize();
+ var sum : nat := 0;
+ for i := |fields| downto 0
+ invariant sum == SumValueSize(fields[i..])
+ {
+ if fields[i].action == ENCRYPT_AND_SIGN {
+ sum := |fields[i].data.value| + sum;
+ }
+ }
+ return sum;
}
function method {:opaque} GetAlgorithmSuiteId(alg : Option<CMP.DBEAlgorithmSuiteId>)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
index 9239ad4cb..e994c382e 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
@@ -234,20 +234,46 @@ module StructuredEncryptionFooter {
GetCanonicalPlaintextField(data.key, data.data)
}
- function method CanonContent (
- data : CanonCryptoList, // remaining fields to be canonized
- canonized : Bytes := [] // output
- ) : Result<Bytes, Error>
+ function CanonContent (data : CanonCryptoList)
+ : Result<Bytes, Error>
{
if |data| == 0 then
- Success(canonized)
+ Success([])
else if data[0].action == DO_NOTHING then
- CanonContent(data[1..], canonized)
+ CanonContent(data[1..])
else
+ var tail :- CanonContent(data[1..]);
var newPart :- GetCanonicalItem(data[0]);
- CanonContent(data[1..], canonized + newPart)
+ Success(newPart + tail)
+ } by method {
+ var i: nat := |data|;
+ var vectors : Bytes := [];
+
+ while i != 0
+ decreases i
+ invariant Success(vectors) == CanonContent(data[i..])
+ {
+ i := i - 1;
+ if data[i].action != DO_NOTHING {
+ var test := GetCanonicalItem(data[i]);
+ if test.Failure? {
+ ghost var j := i;
+ while j != 0
+ decreases j
+ invariant Failure(test.error) == CanonContent(data[j..])
+ {
+ j := j - 1;
+ }
+ return Failure(test.error);
+ }
+ vectors := test.value + vectors;
+ }
+ }
+
+ return Success(vectors);
}
+
function method CanonRecord (
data : CanonCryptoList,
header : Bytes,
@@ -377,13 +403,21 @@ module StructuredEncryptionFooter {
}
}
- function method SerializeTags(tags : seq<RecipientTag>)
+ function SerializeTags(tags : seq<RecipientTag>)
: Bytes
{
if |tags| == 0 then
[]
else
tags[0] + SerializeTags(tags[1..])
+ } by method {
+ var result : Bytes := [];
+ for i := |tags| downto 0
+ invariant result == SerializeTags(tags[i..])
+ {
+ result := tags[i] + result;
+ }
+ return result;
}
function method SerializeSig(sig : Option<Signature>)
From bbebafc4864d866f070fca0cb52013b96fd396bd Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Sun, 9 Feb 2025 13:42:20 -0500
Subject: [PATCH 09/26] m
---
.../src/Index.dfy | 24 +-
.../dafny/DynamoDbItemEncryptor/src/Util.dfy | 19 +-
...ptionSdkStructuredEncryptionOperations.dfy | 134 +++++++----
.../StructuredEncryption/src/Canonize.dfy | 75 ++++---
.../dafny/StructuredEncryption/src/Header.dfy | 209 ++++++++++--------
.../dafny/StructuredEncryption/src/Paths.dfy | 29 ++-
.../dafny/StructuredEncryption/src/Util.dfy | 10 +-
.../DDBEncryption/src/DecryptManifest.dfy | 2 +
submodules/MaterialProviders | 2 +-
submodules/smithy-dafny | 2 +-
10 files changed, 319 insertions(+), 187 deletions(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
index 77f3b7aab..4d2ca0cbc 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
@@ -58,13 +58,19 @@ module
requires tableName in config.tableEncryptionConfigs
ensures SearchModifies(config, tableName) <= TheModifies(config)
- function method {:tailrecursion} AddSignedBeaconActions(names : seq<string>, actions : ET.AttributeActions) : ET.AttributeActions
+ function method {:tailrecursion} AddSignedBeaconActions(
+ names : seq<string>,
+ actions : ET.AttributeActions,
+ pos : nat := 0
+ ) : ET.AttributeActions
requires forall k <- names :: DDB.IsValid_AttributeName(k)
+ requires pos <= |names|
+ decreases |names| - pos
{
- if |names| == 0 then
+ if |names| == pos then
actions
else
- AddSignedBeaconActions(names[1..], actions[names[0] := SET.SIGN_ONLY])
+ AddSignedBeaconActions(names, actions[names[0] := SET.SIGN_ONLY], pos+1)
}
predicate method IsConfigured(config : AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTableEncryptionConfig, name : string)
@@ -79,11 +85,11 @@ module
{
forall tableName <- configs :: ValidTableConfig?(configs[tableName])
}
- predicate {:opaque} CorrectlyTransferedStructure?(
+ predicate {:opaque} CorrectlyTransferredStructure?(
internalConfigs: map<string, DdbMiddlewareConfig.ValidTableConfig>,
config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig
)
- ensures 0 == |internalConfigs| ==> CorrectlyTransferedStructure?(internalConfigs, config)
+ ensures 0 == |internalConfigs| ==> CorrectlyTransferredStructure?(internalConfigs, config)
{
forall tableName <- internalConfigs
::
@@ -142,7 +148,7 @@ module
invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k]
invariant forall internalConfig <- internalConfigs.Values :: internalConfig.logicalTableName in allLogicalTableNames
- invariant CorrectlyTransferedStructure?(internalConfigs, config)
+ invariant CorrectlyTransferredStructure?(internalConfigs, config)
invariant AllTableConfigsValid?(internalConfigs)
invariant ValidConfig?(Config(internalConfigs))
@@ -223,10 +229,10 @@ module
assert internalConfig.physicalTableName == tableName;
}
- assert CorrectlyTransferedStructure?(internalConfigs, config) by {
- reveal CorrectlyTransferedStructure?();
+ assert CorrectlyTransferredStructure?(internalConfigs, config) by {
+ reveal CorrectlyTransferredStructure?();
reveal ConfigsMatch();
- assert CorrectlyTransferedStructure?(internalConfigs - {tableName}, config);
+ assert CorrectlyTransferredStructure?(internalConfigs - {tableName}, config);
assert ConfigsMatch(tableName, internalConfig, inputConfig);
}
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
index 08ba1fef9..7bea3d88b 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
@@ -191,25 +191,30 @@ module DynamoDbItemEncryptorUtil {
keys : seq<UTF8.ValidUTF8Bytes>,
context : MPL.EncryptionContext,
legend : string,
+ keyPos : nat := 0,
+ legendPos : nat := 0,
attrMap : DDB.AttributeMap := map[]
)
: Result<DDB.AttributeMap, string>
requires forall k <- keys :: k in context
+ requires keyPos <= |keys|
+ requires legendPos <= |legend|
+ decreases |keys| - keyPos
{
- if |keys| == 0 then
- if |legend| == 0 then
+ if |keys| == keyPos then
+ if |legend| == legendPos then
Success(attrMap)
else
Failure("Encryption Context Legend is too long.")
else
- var key : UTF8.ValidUTF8Bytes := keys[0];
+ var key : UTF8.ValidUTF8Bytes := keys[keyPos];
if SE.EC_ATTR_PREFIX < key then
- :- Need(0 < |legend|, "Encryption Context Legend is too short.");
+ :- Need(legendPos < |legend|, "Encryption Context Legend is too short.");
var attrName :- GetAttributeName(key);
- var attrValue :- GetAttrValue(context[key], legend[0]);
- GetV2AttrMap(keys[1..], context, legend[1..], attrMap[attrName := attrValue])
+ var attrValue :- GetAttrValue(context[key], legend[legendPos]);
+ GetV2AttrMap(keys, context, legend, keyPos+1, legendPos+1, attrMap[attrName := attrValue])
else
- GetV2AttrMap(keys[1..], context, legend, attrMap)
+ GetV2AttrMap(keys, context, legend, keyPos+1, legendPos, attrMap)
}
function method GetAttributeName(ddbAttrKey: UTF8.ValidUTF8Bytes)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
index fffc07f73..a5204fc19 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
@@ -114,16 +114,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
function method {:opaque} GetBinary(data : AuthList, path : Path): (result: Result<StructuredDataTerminal, Error>)
ensures result.Success? ==> exists x :: x in data && x.key == path
{
- var data := FindAuth(data, path);
+ var pos := FindAuth(data, path);
- if data.None? then
+ if pos.None? then
Failure(E("The field name " + Paths.PathToString(path) + " is required."))
- else if data.value.data.typeId != BYTES_TYPE_ID then
+ else if data[pos.value].data.typeId != BYTES_TYPE_ID then
Failure(E(Paths.PathToString(path) + " must be a binary Terminal."))
- else if data.value.action != DO_NOT_SIGN then
+ else if data[pos.value].action != DO_NOT_SIGN then
Failure(E(Paths.PathToString(path) + " must be DO_NOT_SIGN."))
else
- Success(data.value.data)
+ Success(data[pos.value].data)
}
// Return the sum of the sizes of the given fields
@@ -269,28 +269,66 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
output := GetV2EncryptionContext2(contextAttrs);
}
- function method {:opaque} Find(haystack : CryptoList, needle : Path) : Result<CryptoItem, Error>
+ function {:opaque} Find(haystack : CryptoList, needle : Path, start : nat := 0) : (res : Result<nat, Error>)
+ requires start <= |haystack|
+ requires forall i | 0 <= i < start :: haystack[i].key != needle
+ ensures (exists x <- haystack :: x.key == needle) <==> res.Success?
+ ensures (forall x <- haystack :: x.key != needle) <==> res.Failure?
+ ensures (forall x <- haystack :: x.key != needle) <==> res == Failure(E("Not Found"))
+ ensures res.Success? ==>
+ && 0 <= res.value < |haystack|
+ && haystack[res.value].key == needle
+ && (forall i | 0 <= i < res.value :: haystack[i].key != needle)
+ decreases |haystack| - start
{
- if |haystack| == 0 then
+ if |haystack| == start then
Failure(E("Not Found"))
- else if haystack[0].key == needle
- then Success(haystack[0])
+ else if haystack[start].key == needle then
+ Success(start)
else
- Find(haystack[1..], needle)
+ Find(haystack, needle, start + 1)
+ }
+ by method {
+ for i := 0 to |haystack|
+ invariant forall x <- haystack[..i] :: x.key != needle
+ {
+ if haystack[i].key == needle {
+ return Success(i);
+ }
+ }
+ return Failure(E("Not Found"));
}
- function method {:opaque} FindAuth(haystack : AuthList, needle : Path) : (result : Option<AuthItem>)
- ensures result.Some? ==> exists x :: x in haystack && x.key == needle
+ function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : nat := 0) : (res : Option<nat>)
+ requires start <= |haystack|
+ requires forall i | 0 <= i < start :: haystack[i].key != needle
+ ensures (exists x <- haystack :: x.key == needle) <==> res.Some?
+ ensures (forall x <- haystack :: x.key != needle) <==> res == None
+ ensures res.Some? ==>
+ && 0 <= res.value < |haystack|
+ && haystack[res.value].key == needle
+ && (forall i | 0 <= i < res.value :: haystack[i].key != needle)
+ decreases |haystack| - start
{
- if |haystack| == 0 then
+ if |haystack| == start then
None
- else if haystack[0].key == needle
- then Some(haystack[0])
+ else if haystack[start].key == needle then
+ Some(start)
else
- FindAuth(haystack[1..], needle)
+ FindAuth(haystack, needle, start + 1)
+ }
+ by method {
+ for i := 0 to |haystack|
+ invariant forall x <- haystack[..i] :: x.key != needle
+ {
+ if haystack[i].key == needle {
+ return Some(i);
+ }
+ }
+ return None;
}
- function method {:opaque} CountEncrypted(list : CanonCryptoList) : nat
+ function {:opaque} CountEncrypted(list : CanonCryptoList) : nat
{
if |list| == 0 then
0
@@ -298,6 +336,17 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
1 + CountEncrypted(list[1..])
else
CountEncrypted(list[1..])
+ } by method {
+ reveal CountEncrypted();
+ var result : nat := 0;
+ for i := |list| downto 0
+ invariant result == CountEncrypted(list[i..])
+ {
+ if list[i].action == ENCRYPT_AND_SIGN {
+ result := result + 1;
+ }
+ }
+ return result;
}
method {:vcs_split_on_every_assert} GetV2EncryptionContext2(fields : CryptoList)
@@ -355,7 +404,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
var fieldUtf8 := keys[i];
var fieldStr := fieldMap[fieldUtf8];
var item :- Find(fields, fieldMap[fieldUtf8]);
- var attr : StructuredDataTerminal := item.data;
+ var attr : StructuredDataTerminal := fields[item].data;
var attrStr : ValidUTF8Bytes;
var legendChar : char;
if attr.typeId == NULL {
@@ -395,19 +444,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
keys : seq<string>,
plaintextStructure: StructuredDataMap,
cryptoSchema: CryptoSchemaMap,
- ghost origKeys : seq<string> := keys,
+ pos : nat := 0,
acc : CryptoList := []
)
: (ret : Result<CryptoList, Error>)
+ requires 0 <= pos <= |keys|
+ requires |acc| == pos
requires forall k <- keys :: k in plaintextStructure
requires forall k <- keys :: k in cryptoSchema
requires forall k <- acc :: |k.key| == 1
- requires CryptoListHasNoDuplicates(acc)
- requires |acc| + |keys| == |origKeys|
- requires keys == origKeys[|acc|..]
- requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i])
+ requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
requires Seq.HasNoDuplicates(keys)
- requires Seq.HasNoDuplicates(origKeys)
+ decreases |keys| - pos
ensures ret.Success? ==>
&& (forall k <- ret.value :: |k.key| == 1)
@@ -415,14 +463,14 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
{
reveal Seq.HasNoDuplicates();
Paths.StringToUniPathUnique();
- if |keys| == 0 then
+ if |keys| == pos then
Success(acc)
else
- var key := keys[0];
+ var key := keys[pos];
var path := Paths.StringToUniPath(key);
var item := CryptoItem(key := path, data := plaintextStructure[key], action := cryptoSchema[key]);
var newAcc := acc + [item];
- BuildCryptoMap2(keys[1..], plaintextStructure, cryptoSchema, origKeys, newAcc)
+ BuildCryptoMap2(keys, plaintextStructure, cryptoSchema, pos+1, newAcc)
}
function method BuildCryptoMap(plaintextStructure: StructuredDataMap, cryptoSchema: CryptoSchemaMap) :
@@ -440,33 +488,33 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
keys : seq<string>,
plaintextStructure: StructuredDataMap,
authSchema: AuthenticateSchemaMap,
- ghost origKeys : seq<string> := keys,
+ pos : nat := 0,
acc : AuthList := []
)
: (ret : Result<AuthList, Error>)
+ requires 0 <= pos <= |keys|
+ requires |acc| == pos
requires forall k <- keys :: k in plaintextStructure
requires forall k <- keys :: k in authSchema
requires forall k <- acc :: |k.key| == 1
+ requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
requires AuthListHasNoDuplicates(acc)
- requires |acc| + |keys| == |origKeys|
- requires keys == origKeys[|acc|..]
- requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(origKeys[i])
requires Seq.HasNoDuplicates(keys)
- requires Seq.HasNoDuplicates(origKeys)
+ decreases |keys| - pos
ensures ret.Success? ==>
&& (forall k <- ret.value :: |k.key| == 1)
&& AuthListHasNoDuplicates(ret.value)
{
reveal Seq.HasNoDuplicates();
- if |keys| == 0 then
+ if |keys| == pos then
Success(acc)
else
- var key := keys[0];
+ var key := keys[pos];
var path := Paths.StringToUniPath(key);
var item := AuthItem(key := path, data := plaintextStructure[key], action := authSchema[key]);
var newAcc := acc + [item];
- BuildAuthMap2(keys[1..], plaintextStructure, authSchema, origKeys, newAcc)
+ BuildAuthMap2(keys, plaintextStructure, authSchema, pos+1, newAcc)
}
function method BuildAuthMap(plaintextStructure: StructuredDataMap, authSchema: AuthenticateSchemaMap)
@@ -480,24 +528,28 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
BuildAuthMap2(keys, plaintextStructure, authSchema)
}
- function method UnBuildCryptoMap(list : CryptoList, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
+ function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : nat := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
(res : Result<(StructuredDataMap, CryptoSchemaMap), Error>)
+ requires 0 <= pos <= |list|
+ requires |dataSoFar| == pos
+ requires |actionsSoFar| <= pos
requires forall k <- actionsSoFar :: k in dataSoFar
requires (forall v :: v in actionsSoFar.Values ==> IsAuthAttr(v))
requires forall k <- list :: |k.key| == 1
+ decreases |list| - pos
ensures res.Success? ==>
&& (forall k <- res.value.1 :: k in res.value.0)
&& (forall v :: v in res.value.1.Values ==> IsAuthAttr(v))
{
- if |list| == 0 then
+ if |list| == pos then
Success((dataSoFar, actionsSoFar))
else
- var key :- Paths.UniPathToString(list[0].key);
+ var key :- Paths.UniPathToString(list[pos].key);
:- Need(key !in dataSoFar, E("Duplicate Key " + key));
- if IsAuthAttr(list[0].action) then
- UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar[key := list[0].action])
+ if IsAuthAttr(list[pos].action) then
+ UnBuildCryptoMap(list, pos+1, dataSoFar[key := list[pos].data], actionsSoFar[key := list[pos].action])
else
- UnBuildCryptoMap(list[1..], dataSoFar[key := list[0].data], actionsSoFar)
+ UnBuildCryptoMap(list, pos+1, dataSoFar[key := list[pos].data], actionsSoFar)
}
lemma EncryptStructureOutputHasSinglePaths(origData : CryptoList, finalData : CryptoList)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
index 306f63521..698dc237b 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -139,25 +139,28 @@ module {:options "/functionSyntax:4" } Canonize {
opaque function {:tailrecursion} ResolveLegend(
fields : CanonAuthList,
legend : Header.Legend,
- ghost origFields : CanonAuthList,
- acc : CanonCryptoList
+ pos : nat := 0,
+ legendPos : nat := 0,
+ acc : CanonCryptoList := []
)
: (ret : Result<CanonCryptoList, Error>)
- requires |fields| + |acc| == |origFields|
- requires forall i | 0 <= i < |acc| :: Same(origFields[i], acc[i])
- requires forall i | |acc| <= i < |origFields| :: origFields[i] == fields[i-|acc|]
+ requires 0 <= pos <= |fields|
+ requires 0 <= legendPos <= |legend|
+ requires pos == |acc|
+ requires forall i | 0 <= i < pos :: Same(fields[i], acc[i])
ensures ret.Success? ==>
- && |origFields| == |ret.value|
- && forall i | 0 <= i < |origFields| :: Same(origFields[i], ret.value[i])
+ && |fields| == |ret.value|
+ && forall i | 0 <= i < |fields| :: Same(fields[i], ret.value[i])
+ decreases |fields| - pos
{
- if |fields| == 0 then
- :- Need(|legend| == 0, E("Schema changed : something that was signed is now unsigned."));
+ if |fields| == pos then
+ :- Need(|legend| == legendPos, E("Schema changed : something that was signed is now unsigned."));
Success(acc)
- else if fields[0].action == DO_NOT_SIGN then
- ResolveLegend(fields[1..], legend, origFields, acc + [MakeCryptoItem(fields[0], DO_NOTHING)])
+ else if fields[pos].action == DO_NOT_SIGN then
+ ResolveLegend(fields, legend, pos+1, legendPos, acc + [MakeCryptoItem(fields[pos], DO_NOTHING)])
else
- :- Need(0 < |legend|, E("Schema changed : something that was unsigned is now signed."));
- ResolveLegend(fields[1..], legend[1..], origFields, acc + [MakeCryptoItem(fields[0], LegendToAction(legend[0]))])
+ :- Need(legendPos < |legend|, E("Schema changed : something that was unsigned is now signed."));
+ ResolveLegend(fields, legend, pos+1, legendPos+1, acc + [MakeCryptoItem(fields[pos], LegendToAction(legend[legendPos]))])
}
opaque function ForEncrypt(tableName : GoodString, data : CryptoList)
@@ -562,7 +565,7 @@ module {:options "/functionSyntax:4" } Canonize {
reveal CanonAuthMatchesAuthList();
reveal CanonCryptoMatchesAuthList();
reveal IsCryptoSorted();
- var canonResolved :- ResolveLegend(canonSorted, legend, canonSorted, []);
+ var canonResolved :- ResolveLegend(canonSorted, legend);
assert (forall k <- data :: AuthExistsInCanonCrypto(k, canonResolved)) by {
reveal AuthExistsInCanonCrypto();
@@ -622,17 +625,19 @@ module {:options "/functionSyntax:4" } Canonize {
&& x.action == y.action
}
- function UnCanon(input : CanonCryptoList) : (ret : CryptoList)
- ensures
- && |ret| == |input|
- && (forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i]))
+ function {:tailrecursion} UnCanon(input : CanonCryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList)
+ requires 0 <= pos <= |input|
+ requires pos == |acc|
+ requires forall i | 0 <= i < |acc| :: SameUnCanon(input[i], acc[i])
+ ensures |ret| == |input|
+ ensures forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i])
+ decreases |input| - pos
{
- if |input| == 0 then
- []
+ if |input| == pos then
+ acc
else
- var newItem := CryptoItem(key := input[0].origKey, data := input[0].data, action := input[0].action);
- assert SameUnCanon(input[0], newItem);
- [newItem] + UnCanon(input[1..])
+ var newItem := CryptoItem(key := input[pos].origKey, data := input[pos].data, action := input[pos].action);
+ UnCanon(input, pos+1, acc + [newItem])
}
lemma Update2ImpliesUpdate3()
@@ -795,17 +800,33 @@ module {:options "/functionSyntax:4" } Canonize {
&& CryptoListHasNoDuplicates(finalData)
}
- opaque function RemoveHeaderPaths(xs : CryptoList) : (ret : CryptoList)
+ opaque function {:tailrecursion} RemoveHeaderPaths(xs : CryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList)
requires CryptoListHasNoDuplicates(xs)
+ requires 0 <= pos <= |xs|
+ requires !exists x :: x in acc && x.key in [HeaderPath, FooterPath]
+ requires !exists x :: x in acc && x.key == HeaderPath
+ requires !exists x :: x in acc && x.key == FooterPath
+ requires forall x <- acc :: x in xs[..pos]
+ requires forall i | 0 <= i < pos :: (xs[i].key in [HeaderPath, FooterPath] || xs[i] in acc)
+ // should file a ticket, because this is FALSE but verifies
+ // requires forall x <- xs :: (x.key in [HeaderPath, FooterPath] || x in acc)
+ requires CryptoListHasNoDuplicates(acc)
+
ensures !exists x :: x in ret && x.key in [HeaderPath, FooterPath]
ensures !exists x :: x in ret && x.key == HeaderPath
ensures !exists x :: x in ret && x.key == FooterPath
ensures forall x <- ret :: x in xs
- ensures forall x <- xs :: x.key in [HeaderPath, FooterPath] || x in ret
+ ensures forall x <- xs :: (x.key in [HeaderPath, FooterPath] || x in ret)
ensures CryptoListHasNoDuplicates(ret)
+
+ decreases |xs| - pos
{
- if |xs| == 0 then []
- else (if xs[0].key in [HeaderPath, FooterPath] then [] else [xs[0]]) + RemoveHeaderPaths(xs[1..])
+ if |xs| == pos then
+ acc
+ else if xs[pos].key in [HeaderPath, FooterPath] then
+ RemoveHeaderPaths(xs, pos+1, acc)
+ else
+ RemoveHeaderPaths(xs, pos+1, acc + [xs[pos]])
}
opaque function RemoveHeaders(input : CryptoList, ghost origData : AuthList)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
index 66169eea6..fd016868d 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -387,18 +387,21 @@ module StructuredEncryptionHeader {
// Create a Legend for the given attrs of the Schema
function method {:tailrecursion} MakeLegend2(
data : CanonCryptoList,
+ pos : nat := 0,
serialized : Legend := EmptyLegend
)
: (ret : Result<Legend, Error>)
+ requires 0 <= pos <= |data|
+ decreases |data| - pos
{
- if |data| == 0 then
+ if |data| == pos then
Success(serialized)
- else if IsAuthAttr(data[0].action) then
+ else if IsAuthAttr(data[pos].action) then
:- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
- var legendChar := GetActionLegend(data[0].action);
- MakeLegend2(data[1..], serialized + [legendChar])
+ var legendChar := GetActionLegend(data[pos].action);
+ MakeLegend2(data, pos+1, serialized + [legendChar])
else
- MakeLegend2(data[1..], serialized)
+ MakeLegend2(data, pos+1, serialized)
}
// CryptoAction to bytes. One byte for signed, zero bytes for unsigned
@@ -432,15 +435,17 @@ module StructuredEncryptionHeader {
}
// How many elements of Schema are included in the signature?
- function method CountAuthAttrs(data : CanonCryptoList)
+ function method CountAuthAttrs(data : CanonCryptoList, pos : nat := 0, acc : nat := 0)
: nat
+ requires 0 <= pos <= |data|
+ decreases |data| - pos
{
- if |data| == 0 then
- 0
- else if IsAuthAttr(data[0].action) then
- 1 + CountAuthAttrs(data[1..])
+ if |data| == pos then
+ acc
+ else if IsAuthAttr(data[pos].action) then
+ CountAuthAttrs(data, pos+1, acc+1)
else
- CountAuthAttrs(data[1..])
+ CountAuthAttrs(data, pos+1, acc)
}
// Legend to Bytes
@@ -470,11 +475,12 @@ module StructuredEncryptionHeader {
&& ret.value.0 == data[2..ret.value.1]
{
:- Need(2 <= |data|, E("Unexpected end of header data."));
- var len := SeqToUInt16(data[0..2]);
+ var len := SeqPosToUInt16(data, 0);
var size := len as nat + 2;
:- Need(size <= |data|, E("Unexpected end of header data."));
- :- Need(forall x <- data[2..size] :: ValidLegendByte(x), E("Invalid byte in stored legend"));
- Success((data[2..size], size))
+ var legend := data[2..size];
+ :- Need(forall x <- legend :: ValidLegendByte(x), E("Invalid byte in stored legend"));
+ Success((legend, size))
}
// Bytes to Encryption Context
@@ -484,77 +490,78 @@ module StructuredEncryptionHeader {
&& ret.value.1 <= |data|
ensures (
&& 2 <= |data|
- && GetContext2(SeqToUInt16(data[0..2]) as nat, data, data[2..], (map[], 2)).Success?
+ && GetContext2(SeqPosToUInt16(data, 0) as nat, data, (map[], 2)).Success?
) ==> ret.Success?
{
:- Need(2 <= |data|, E("Unexpected end of header data."));
- var count := SeqToUInt16(data[0..2]) as nat;
- var context :- GetContext2(count, data, data[2..], (map[], 2));
+ var count := SeqPosToUInt16(data, 0) as nat;
+ var context :- GetContext2(count, data, (map[], 2));
Success(context)
}
// Bytes to one Key Value pair
- function method GetOneKVPair(data : Bytes)
+ function method GetOneKVPair(data : Bytes, pos : nat)
: (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, nat), Error>)
ensures ret.Success? ==>
- && ret.value.2 <= |data|
- && SerializeOneKVPair(ret.value.0, ret.value.1) == data[..ret.value.2]
+ && ret.value.2 + pos <= |data|
+ && SerializeOneKVPair(ret.value.0, ret.value.1) == data[pos..pos+ret.value.2]
ensures (
- && 2 <= |data|
- && var keyLen := SeqToUInt16(data[0..2]) as nat;
- && keyLen + 4 <= |data|
- && UTF8.ValidUTF8Seq(data[2..keyLen+2])
- && var valueLen := SeqToUInt16(data[keyLen+2..keyLen+4]) as nat;
- && keyLen + valueLen + 4 <= |data|
- && UTF8.ValidUTF8Seq(data[keyLen+4..keyLen + valueLen + 4])
- ) <==> ret.Success? && SerializeOneKVPair(ret.value.0, ret.value.1) == data[..ret.value.2]
- {
- :- Need(2 <= |data|, E("Unexpected end of header data."));
- var keyLen := SeqToUInt16(data[0..2]) as nat;
- :- Need(keyLen + 4 <= |data|, E("Unexpected end of header data."));
- var key := data[2..keyLen+2];
+ && 2 + pos <= |data|
+ && var keyLen := SeqPosToUInt16(data, pos) as nat;
+ && keyLen + 4 + pos <= |data|
+ && UTF8.ValidUTF8Seq(data[2+pos..keyLen+2+pos])
+ && var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat;
+ && keyLen + valueLen + 4 + pos <= |data|
+ && UTF8.ValidUTF8Seq(data[keyLen+4+pos..keyLen + valueLen + 4 + pos])
+ ) <==> ret.Success? && SerializeOneKVPair(ret.value.0, ret.value.1) == data[pos..pos+ret.value.2]
+ {
+ :- Need(2 + pos <= |data|, E("Unexpected end of header data."));
+ var keyLen := SeqPosToUInt16(data, pos) as nat;
+ :- Need(keyLen + 4 +pos <= |data|, E("Unexpected end of header data."));
+ var key := data[2+pos..keyLen+2+pos];
:- Need(UTF8.ValidUTF8Seq(key), E("Invalid UTF8 found in header."));
- var valueLen := SeqToUInt16(data[keyLen+2..keyLen+4]) as nat;
+ var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat;
var kvLen := 2 + keyLen + 2 + valueLen;
- :- Need(kvLen <= |data|, E("Unexpected end of header data."));
- var value := data[keyLen+4..kvLen];
+ :- Need(kvLen + pos <= |data|, E("Unexpected end of header data."));
+ var value := data[keyLen+4+pos..kvLen+pos];
:- Need(UTF8.ValidUTF8Seq(value), E("Invalid UTF8 found in header."));
Success((key, value, kvLen))
}
- predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes) {
+ predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes, pos : nat := 0)
+ requires 0 <= pos <= |a|
+ requires 0 <= pos <= |b|
+ decreases |a| - pos
+ {
if a == b then
false
- else if |a| == 0 then
+ else if |a| == pos then
true
- else if |b| == 0 then
+ else if |b| == pos then
false
- else if a[0] != b[0] then
- a[0] < b[0]
+ else if a[pos] != b[pos] then
+ a[pos] < b[pos]
else
- BytesLess(a[1..], b[1..])
+ BytesLess(a, b, pos+1)
}
// For "count" items, Deserialize key value pairs into an Encryption Context
function method {:tailrecursion} GetContext2(
count : nat,
- origData : Bytes,
data : Bytes,
deserialized : (CMPEncryptionContext, nat),
prevKey : CMPUtf8Bytes := [])
: (ret : Result<(CMPEncryptionContext, nat), Error>)
- requires deserialized.1 <= |origData|
- requires deserialized.1 + |data| == |origData|
- requires data == origData[deserialized.1..]
+ requires deserialized.1 <= |data|
ensures ret.Success? ==>
- && ret.value.1 <= |origData|
- && (count > 0 ==> GetOneKVPair(data).Success?)
+ && ret.value.1 <= |data|
+ && (count > 0 ==> GetOneKVPair(data, deserialized.1).Success?)
{
if count == 0 then
Success(deserialized)
else
:- Need(|deserialized.0| + 1 < UINT16_LIMIT, E("Too much context"));
- var kv :- GetOneKVPair(data);
+ var kv :- GetOneKVPair(data, deserialized.1);
//= specification/structured-encryption/header.md#key-value-pair-entries
//# This sequence MUST NOT contain duplicate entries.
// if the previous key is always less than the current key, there can be no duplicates
@@ -563,7 +570,7 @@ module StructuredEncryptionHeader {
//# These entries MUST have entries sorted, by key,
//# in ascending order according to the UTF-8 encoded binary value.
:- Need(BytesLess(prevKey, kv.0), E("Context keys out of order."));
- GetContext2(count-1, origData, data[2+|kv.0|+2+|kv.1|..], (deserialized.0[kv.0 := kv.1], deserialized.1 + kv.2), kv.0)
+ GetContext2(count-1, data, (deserialized.0[kv.0 := kv.1], deserialized.1 + kv.2), kv.0)
}
// Encryption Context to Bytes
@@ -641,30 +648,30 @@ module StructuredEncryptionHeader {
}
// Bytes to Data Key
- function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes)
+ function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes, pos : nat)
: (ret : Result<(CMPEncryptedDataKey, nat), Error>)
ensures ret.Success? ==>
- && ret.value.1 <= |data|
+ && ret.value.1 + pos <= |data|
&& |SerializeOneDataKey(ret.value.0)| == ret.value.1
- && SerializeOneDataKey(ret.value.0) == data[0..ret.value.1]
+ && SerializeOneDataKey(ret.value.0) == data[pos..pos+ret.value.1]
{
- :- Need(2 < |data|, E("Unexpected end of header data."));
- var provIdSize := SeqToUInt16(data[0..2]) as nat;
- :- Need(provIdSize + 2 < |data|, E("Unexpected end of header data."));
- var provId := data[2..2+provIdSize];
+ :- Need(2 + pos < |data|, E("Unexpected end of header data."));
+ var provIdSize := SeqPosToUInt16(data, pos) as nat;
+ :- Need(provIdSize + 2 + pos < |data|, E("Unexpected end of header data."));
+ var provId := data[pos+2..pos+2+provIdSize];
:- Need(UTF8.ValidUTF8Seq(provId), E("Invalid UTF8 found in header."));
var part1Size := 2 + provIdSize;
- :- Need(part1Size+2 <= |data|, E("Unexpected end of header data."));
- var provInfoSize := SeqToUInt16(data[part1Size..part1Size+2]) as nat;
- :- Need(part1Size + provInfoSize + 2 < |data|, E("Unexpected end of header data."));
- var provInfo := data[part1Size+2..part1Size+2+provInfoSize];
+ :- Need(part1Size+2 + pos <= |data|, E("Unexpected end of header data."));
+ var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as nat;
+ :- Need(part1Size + provInfoSize + 2 + pos < |data|, E("Unexpected end of header data."));
+ var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize];
var part2Size := part1Size + 2 + provInfoSize;
- :- Need(part2Size+2 <= |data|, E("Unexpected end of header data."));
- var cipherSize := SeqToUInt16(data[part2Size..part2Size+2]) as nat;
- :- Need(part2Size + cipherSize + 2 <= |data|, E("Unexpected end of header data."));
- var cipher := data[part2Size+2..part2Size+2+cipherSize];
+ :- Need(part2Size+2+pos <= |data|, E("Unexpected end of header data."));
+ var cipherSize := SeqPosToUInt16(data, pos+part2Size) as nat;
+ :- Need(part2Size + cipherSize + 2 + pos <= |data|, E("Unexpected end of header data."));
+ var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize];
var part3Size := part2Size + 2 + cipherSize;
var edk := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher);
@@ -672,14 +679,21 @@ module StructuredEncryptionHeader {
}
// for items in "keys", turn Key Value Pairs into Bytes
- function method {:tailrecursion} SerializeContext2(keys : seq<CMPUtf8Bytes>, x : CMPEncryptionContext)
+ function method {:tailrecursion} SerializeContext2(
+ keys : seq<CMPUtf8Bytes>,
+ x : CMPEncryptionContext,
+ pos : nat := 0,
+ acc : Bytes := []
+ )
: (ret : Bytes)
requires forall k <- keys :: k in x
+ requires 0 <= pos <= |keys|
+ decreases |keys| - pos
{
- if |keys| == 0 then
- []
+ if |keys| == pos then
+ acc
else
- SerializeOneKVPair(keys[0], x[keys[0]]) + SerializeContext2(keys[1..], x)
+ SerializeContext2(keys, x, pos+1, acc + SerializeOneKVPair(keys[pos], x[keys[pos]]))
}
// Data Key List to Bytes
@@ -702,13 +716,19 @@ module StructuredEncryptionHeader {
}
// Data Keys to Bytes
- function method {:tailrecursion} SerializeDataKeys2(x : CMPEncryptedDataKeyListEmptyOK)
+ function method {:tailrecursion} SerializeDataKeys2(
+ x : CMPEncryptedDataKeyListEmptyOK,
+ pos : nat := 0,
+ acc : Bytes := []
+ )
: (ret : Bytes)
+ requires 0 <= pos <= |x|
+ decreases |x| - pos
{
- if |x| == 0 then
- []
+ if |x| == pos then
+ acc
else
- SerializeOneDataKey(x[0]) + SerializeDataKeys2(x[1..])
+ SerializeDataKeys2(x, pos+1, acc + SerializeOneDataKey(x[pos]))
}
// Bytes to Data Key List
@@ -719,11 +739,11 @@ module StructuredEncryptionHeader {
&& 1 <= |data|
&& 1 <= ret.value.1
&& |ret.value.0| == data[0] as nat
- && GetDataKeys2(|ret.value.0|, |ret.value.0|, data, data[1..], ([], 1)).Success?
+ && GetDataKeys2(|ret.value.0|, |ret.value.0|, data, ([], 1)).Success?
{
:- Need(1 <= |data|, E("Unexpected end of header data."));
var count := data[0] as nat;
- var keys :- GetDataKeys2(count, count, data, data[1..], ([], 1));
+ var keys :- GetDataKeys2(count, count, data, ([], 1));
if |keys.0| == 0 then
Failure(E("At least one Data Key required"))
else
@@ -734,18 +754,15 @@ module StructuredEncryptionHeader {
function method {:tailrecursion} GetDataKeys2(
count : nat,
origCount : nat,
- origData : Bytes,
data : Bytes,
- deserialized
- : (CMPEncryptedDataKeyListEmptyOK, nat))
+ deserialized : (CMPEncryptedDataKeyListEmptyOK, nat))
: (ret : Result<(CMPEncryptedDataKeyListEmptyOK, nat), Error>)
- requires deserialized.1 <= |origData|
- requires deserialized.1 + |data| == |origData|
+ requires deserialized.1 <= |data|
requires origCount == count + |deserialized.0|
ensures ret.Success? ==>
- && ret.value.1 <= |origData|
+ && ret.value.1 <= |data|
&& ret.value.1 >= deserialized.1
- && (count > 0 ==> GetOneDataKey(data).Success?)
+ && (count > 0 ==> GetOneDataKey(data, deserialized.1).Success?)
&& |ret.value.0| == origCount
{
if count == 0 then
@@ -754,9 +771,9 @@ module StructuredEncryptionHeader {
if |deserialized.0| >= 255 then
Failure(E("Too Many Data Keys"))
else
- var edk :- GetOneDataKey(data);
- assert SerializeOneDataKey(edk.0) == data[..edk.1];
- GetDataKeys2(count-1, origCount, origData, data[edk.1..], (deserialized.0 + [edk.0], deserialized.1+edk.1))
+ var edk :- GetOneDataKey(data, deserialized.1);
+ assert SerializeOneDataKey(edk.0) == data[deserialized.1..deserialized.1+edk.1];
+ GetDataKeys2(count-1, origCount, data, (deserialized.0 + [edk.0], deserialized.1+edk.1))
}
// End code, begin proofs
@@ -790,7 +807,7 @@ module StructuredEncryptionHeader {
// SerializeOneKVPair ==> GetOneKVPair
lemma SerializeOneKVPairRoundTrip(key : CMPUtf8Bytes, value : CMPUtf8Bytes)
- ensures GetOneKVPair(SerializeOneKVPair(key, value)).Success?
+ ensures GetOneKVPair(SerializeOneKVPair(key, value), 0).Success?
{
var data := SerializeOneKVPair(key, value);
assert 2 <= |data|;
@@ -806,9 +823,9 @@ module StructuredEncryptionHeader {
// GetOneKVPair ==> SerializeOneKVPair
lemma GetOneKVPairRoundTrip(data : Bytes)
- requires GetOneKVPair(data).Success?
+ requires GetOneKVPair(data, 0).Success?
ensures
- && var cont := GetOneKVPair(data).value;
+ && var cont := GetOneKVPair(data, 0).value;
&& SerializeOneKVPair(cont.0, cont.1) == data[..cont.2]
{}
@@ -816,9 +833,9 @@ module StructuredEncryptionHeader {
lemma SerializeOneDataKeyRoundTrip(k : CMPEncryptedDataKey)
ensures
&& var data := SerializeOneDataKey(k);
- && GetOneDataKey(data).Success?
- && GetOneDataKey(data).value.0 == k
- && GetOneDataKey(data).value.1 == |data|
+ && GetOneDataKey(data, 0).Success?
+ && GetOneDataKey(data, 0).value.0 == k
+ && GetOneDataKey(data, 0).value.1 == |data|
{
var data := SerializeOneDataKey(k);
assert 2 <= |data|;
@@ -837,9 +854,9 @@ module StructuredEncryptionHeader {
// GetOneDataKey ==> SerializeOneDataKey
lemma GetOneDataKeyRoundTrip(data : Bytes)
- requires GetOneDataKey(data).Success?
+ requires GetOneDataKey(data, 0).Success?
ensures
- && var cont := GetOneDataKey(data).value;
+ && var cont := GetOneDataKey(data, 0).value;
&& SerializeOneDataKey(cont.0) == data[..cont.1]
{}
@@ -847,10 +864,10 @@ module StructuredEncryptionHeader {
// the unexamined bytes do not change the result
lemma GetOneKVPairExt(x : Bytes, y : Bytes)
requires x <= y
- requires GetOneKVPair(x).Success?
+ requires GetOneKVPair(x, 0).Success?
ensures
- && GetOneKVPair(y).Success?
- && GetOneKVPair(x).value == GetOneKVPair(y).value
+ && GetOneKVPair(y, 0).Success?
+ && GetOneKVPair(x, 0).value == GetOneKVPair(y, 0).value
{
assert 2 <= |y|;
var keyLen := SeqToUInt16(y[0..2]) as nat;
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
index f5b8bba4e..5b64497bb 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
@@ -110,7 +110,7 @@ module StructuredEncryptionPaths {
}
// get the Canonical Path for these Selectors
- function method {:tailrecursion} MakeCanonicalPath(path : Path)
+ function MakeCanonicalPath(path : Path)
: (ret : CanonicalPath)
requires ValidPath(path)
ensures |path| == 0 ==> ret == []
@@ -120,8 +120,35 @@ module StructuredEncryptionPaths {
[]
else
CanonicalPart(path[0]) + MakeCanonicalPath(path[1..])
+ } by method {
+ var result : CanonicalPath := [];
+ for i := |path| downto 0
+ invariant result == MakeCanonicalPath(path[i..])
+ {
+ result := CanonicalPart(path[i]) + result;
+ }
+ return result;
}
+ // get the Canonical Path for these Selectors
+ // function method {:tailrecursion} MakeCanonicalPath(path : Path, pos : nat := 0, acc : CanonicalPath := [])
+ // : (ret : CanonicalPath)
+ // requires ValidPath(path)
+ // requires pos <= |path|
+ // requires pos == 0 ==> |acc| == 0
+ // requires pos == 1 ==> acc == CanonicalPart(path[0])
+ // requires acc == MakeCanonicalPathGhost(path[..pos])
+ // ensures |path| == 0 && pos == 0 ==> ret == []
+ // ensures |path| == 1 ==> ret == CanonicalPart(path[0])
+ // ensures ret == MakeCanonicalPathGhost(path)
+ // decreases |path| - pos
+ // {
+ // if |path| == pos then
+ // acc
+ // else
+ // MakeCanonicalPath(path, pos+1, acc + CanonicalPart(path[pos]))
+ // }
+
// Does NOT guarantee a unique output for every unique input
// e.g. ['a.b'] and ['a','b'] both return 'a.b'.
function method PathToString(path : Path) : string
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
index 93e36cd56..20cb74b34 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
@@ -199,14 +199,16 @@ module StructuredEncryptionUtil {
// sequences are equal if zero is returned
// Some care should be taken to ensure that target languages don't over optimize this.
- function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, acc : bv8 := 0) : bv8
+ function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, pos : nat := 0, acc : bv8 := 0) : bv8
requires |a| == |b|
+ requires 0 <= pos <= |a|
+ decreases |a| - pos
{
- if |a| == 0 then
+ if |a| == pos then
acc
else
- var x := ((a[0] as bv8) ^ (b[0] as bv8));
- ConstantTimeCompare(a[1..], b[1..], x | acc)
+ var x := ((a[pos] as bv8) ^ (b[pos] as bv8));
+ ConstantTimeCompare(a, b, pos+1, x | acc)
}
predicate method ConstantTimeEquals(a : Bytes, b : Bytes)
diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
index 5ee680b4e..551dd83b7 100644
--- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
@@ -168,11 +168,13 @@ module {:options "-functionSyntax:4"} DecryptManifest {
}
}
+ var time := Time.GetAbsoluteTime();
for i := 0 to |tests.value| {
var obj := tests.value[i];
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
var _ :- OneTest(obj.0, obj.1, keyVectors);
}
+ Time.PrintTimeSinceLong(time, "DB-ESDK-TV " + inFile);
timeStamp :- expect Time.GetCurrentTimeStamp();
print timeStamp + " Tests Complete.\n";
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 786404f1d..70d6a59a7 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 786404f1d1bdf86814c5018ce0b3b1149ef65b3e
+Subproject commit 70d6a59a732261e4aee3ccf6f69dfeb319f3bf3e
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index 186339f25..5fb3f25ea 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 186339f258f9116a3c25cc781c747ab0e94e9dc6
+Subproject commit 5fb3f25ea3444c51b2ad30b25ab03964cf866cd1
From 87b103c02a0841117fac9983fb6cd6355e652349 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 10 Feb 2025 09:00:36 -0500
Subject: [PATCH 10/26] m
---
DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy | 1 +
1 file changed, 1 insertion(+)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
index 698dc237b..e8b0eb240 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -826,6 +826,7 @@ module {:options "/functionSyntax:4" } Canonize {
else if xs[pos].key in [HeaderPath, FooterPath] then
RemoveHeaderPaths(xs, pos+1, acc)
else
+ assert xs[pos] !in acc;
RemoveHeaderPaths(xs, pos+1, acc + [xs[pos]])
}
From b60be2b0b458f72980b3aac230869d11b86287f6 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 10 Feb 2025 09:11:20 -0500
Subject: [PATCH 11/26] m
---
DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy | 1 -
1 file changed, 1 deletion(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
index fd016868d..5930ae6ce 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -504,7 +504,6 @@ module StructuredEncryptionHeader {
: (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, nat), Error>)
ensures ret.Success? ==>
&& ret.value.2 + pos <= |data|
- && SerializeOneKVPair(ret.value.0, ret.value.1) == data[pos..pos+ret.value.2]
ensures (
&& 2 + pos <= |data|
&& var keyLen := SeqPosToUInt16(data, pos) as nat;
From 8b183a8d5c981a4fcfc4703859196b80747aeee6 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 10 Feb 2025 09:29:24 -0500
Subject: [PATCH 12/26] m
---
project.properties | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/project.properties b/project.properties
index 28a3b90f1..1bba22bde 100644
--- a/project.properties
+++ b/project.properties
@@ -1,6 +1,6 @@
projectJavaVersion=3.8.0-SNAPSHOT
mplDependencyJavaVersion=1.9.0-SNAPSHOT
dafnyVersion=4.9.0
-dafnyVerifyVersion=4.9.0
+dafnyVerifyVersion=4.9.1
dafnyRuntimeJavaVersion=4.9.0
smithyDafnyJavaConversionVersion=0.1.1
From 005f287bf947e37f1dbdbc4e3bca1b7c3f15b4cf Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 10 Feb 2025 11:11:14 -0500
Subject: [PATCH 13/26] m
---
.../dafny/StructuredEncryption/src/OptimizedMergeSort.dfy | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index 5c5152a79..7b3ba1b36 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -429,7 +429,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
// Second this would create two loops.
// First loop would create the `lo to hi` range of numbers.
// The second loop would then loop over these elements.
- // A single loop with
+ // A single loop with
for i := lo to hi
modifies right
invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
From a0b4787ef1f745bfa9e217169640752ba88497d1 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Wed, 12 Feb 2025 16:13:55 -0500
Subject: [PATCH 14/26] m
---
.../DynamoDbEncryption/src/CompoundBeacon.dfy | 9 ++--
.../DynamoDbEncryption/src/DynamoToStruct.dfy | 42 +++++++++++++------
.../DynamoDbEncryption/src/FilterExpr.dfy | 24 ++++++-----
.../dafny/DynamoDbEncryption/src/Virtual.dfy | 3 +-
.../dafny/StructuredEncryption/src/Header.dfy | 8 ++--
.../DDBEncryption/src/DecryptManifest.dfy | 11 ++++-
submodules/MaterialProviders | 2 +-
7 files changed, 65 insertions(+), 34 deletions(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
index e8fc00e35..bb1dd0883 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy
@@ -20,6 +20,7 @@ module CompoundBeacon {
import UTF8
import Seq
import SortedSets
+ import StandardLibrary.Sequence
type Prefix = x : string | 0 < |x| witness *
@@ -289,7 +290,7 @@ module CompoundBeacon {
// return all the fields involved in this beacon
function method GetFields(virtualFields : VirtualFieldMap) : seq<string>
{
- Seq.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(virtualFields), parts))
+ Sequence.Flatten(Seq.Map((p : BeaconPart) => p.GetFields(virtualFields), parts))
}
// calculate value for a single piece of a compound beacon query string
@@ -315,9 +316,9 @@ module CompoundBeacon {
Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value)))
else
var parts := Split(value.S, split);
- var partsUsed :- Seq.MapWithResult(s => getPartFromPrefix(s), parts);
+ var partsUsed :- Sequence.MapWithResult(s => getPartFromPrefix(s), parts);
var _ :- ValidatePartOrder(partsUsed, value.S);
- var beaconParts :- Seq.MapWithResult(s => FindAndCalcPart(s, keys), parts);
+ var beaconParts :- Sequence.MapWithResult(s => FindAndCalcPart(s, keys), parts);
var lastIsPrefix :- justPrefix(Seq.Last(parts));
if !forEquality && lastIsPrefix then
var result := Join(beaconParts[..|parts|-1] + [Seq.Last(parts)], [split]);
@@ -534,7 +535,7 @@ module CompoundBeacon {
requires pos < |parts|
{
var partNumbers : seq<nat> := seq(|parts|, (i : nat) => i as nat);
- var _ :- Seq.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i));
+ var _ :- Sequence.MapWithResult((p : int) requires 0 <= p < |parts| => CheckOnePrefixPart(pos, p), seq(|parts|, i => i));
Success(true)
}
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
index 616dfe404..4306dfb2a 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
@@ -18,6 +18,7 @@ module DynamoToStruct {
import Seq
import Norm = DynamoDbNormalizeNumber
import SE = StructuredEncryptionUtil
+ import StandardLibrary.Sequence
type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error
@@ -437,7 +438,7 @@ module DynamoToStruct {
:- Need(|asSet| == |ns|, "Number Set had duplicate values");
Seq.LemmaNoDuplicatesCardinalityOfSet(ns);
- var normList :- Seq.MapWithResult(n => Norm.NormalizeNumber(n), ns);
+ var normList :- Sequence.MapWithResult(n => Norm.NormalizeNumber(n), ns);
var asSet := Seq.ToSet(normList);
:- Need(|asSet| == |normList|, "Number Set had duplicate values after normalization.");
@@ -454,6 +455,10 @@ module DynamoToStruct {
function method BinarySetAttrToBytes(bs: BinarySetAttributeValue): (ret: Result<seq<uint8>, string>)
ensures ret.Success? ==> Seq.HasNoDuplicates(bs)
+ ensures ret.Success? ==>
+ && U32ToBigEndian(|bs|).Success?
+ && LENGTH_LEN <= |ret.value|
+ && ret.value[..LENGTH_LEN] == U32ToBigEndian(|bs|).value
{
var asSet := Seq.ToSet(bs);
:- Need(|asSet| == |bs|, "Binary Set had duplicate values");
@@ -561,14 +566,17 @@ module DynamoToStruct {
// String Set or Number Set to Bytes
function method {:tailrecursion} {:opaque} CollectString(
setToSerialize : StringSetAttributeValue,
+ pos : nat := 0,
serialized : seq<uint8> := [])
: Result<seq<uint8>, string>
+ requires pos <= |setToSerialize|
+ decreases |setToSerialize| - pos
{
- if |setToSerialize| == 0 then
+ if |setToSerialize| == pos then
Success(serialized)
else
- var entry :- EncodeString(setToSerialize[0]);
- CollectString(setToSerialize[1..], serialized + entry)
+ var entry :- EncodeString(setToSerialize[pos]);
+ CollectString(setToSerialize, pos+1, serialized + entry)
}
@@ -596,13 +604,19 @@ module DynamoToStruct {
}
// Binary Set to Bytes
- function method {:tailrecursion} CollectBinary(setToSerialize : BinarySetAttributeValue, serialized : seq<uint8> := []) : Result<seq<uint8>, string>
+ function method {:tailrecursion} CollectBinary(
+ setToSerialize : BinarySetAttributeValue,
+ pos : nat := 0,
+ serialized : seq<uint8> := []
+ ) : Result<seq<uint8>, string>
+ requires pos <= |setToSerialize|
+ decreases |setToSerialize| - pos
{
- if |setToSerialize| == 0 then
+ if |setToSerialize| == pos then
Success(serialized)
else
- var item :- SerializeBinaryValue(setToSerialize[0]);
- CollectBinary(setToSerialize[1..], serialized + item)
+ var item :- SerializeBinaryValue(setToSerialize[pos]);
+ CollectBinary(setToSerialize, pos+1, serialized + item)
}
// List to Bytes
@@ -641,6 +655,7 @@ module DynamoToStruct {
if |listToSerialize| == 0 then
Success(serialized)
else
+ // Can't do the `pos` optimization, because I can't appease the `decreases`
var val :- AttrToBytes(listToSerialize[0], true, depth+1);
CollectList(listToSerialize[1..], depth, serialized + val)
}
@@ -705,24 +720,27 @@ module DynamoToStruct {
//# Entries in a serialized Map MUST be ordered by key value,
//# ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
var keys := SortedSets.ComputeSetToOrderedSequence2(mapToSerialize.Keys, CharLess);
- CollectOrderedMapSubset(keys, mapToSerialize, serialized)
+ CollectOrderedMapSubset(keys, mapToSerialize, 0, serialized)
}
function method {:tailrecursion} {:opaque} CollectOrderedMapSubset(
keys : seq<AttributeName>,
mapToSerialize : map<AttributeName, seq<uint8>>,
+ pos : nat := 0,
serialized : seq<uint8> := []
)
: (ret : Result<seq<uint8>, string>)
+ requires pos <= |keys|
requires forall k <- keys :: k in mapToSerialize
ensures (ret.Success? && |keys| == 0) ==> (ret.value == serialized)
ensures (ret.Success? && |keys| == 0) ==> (|ret.value| == |serialized|)
+ decreases |keys| - pos
{
- if |keys| == 0 then
+ if |keys| == pos then
Success(serialized)
else
- var data :- SerializeMapItem(keys[0], mapToSerialize[keys[0]]);
- CollectOrderedMapSubset(keys[1..], mapToSerialize, serialized + data)
+ var data :- SerializeMapItem(keys[pos], mapToSerialize[keys[pos]]);
+ CollectOrderedMapSubset(keys, mapToSerialize, pos+1, serialized + data)
}
function method BoolToUint8(b : bool) : uint8
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
index 2f2a2cff9..5a0d25ca0 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy
@@ -1271,25 +1271,27 @@ module DynamoDBFilterExpr {
// If only surrogates are involved, comparison is normal
// if one surrogate is involved, the surrogate is larger
// results undefined if not valid UTF16 encodings, but the idea of 'less' is also undefined for invalid encodings.
- predicate method {:tailrecursion} UnicodeLess(a : string, b : string)
+ predicate method {:tailrecursion} UnicodeLess(a : string, b : string, pos : nat := 0)
+ requires pos <= |a|
+ requires pos <= |b|
+ decreases |a| - pos
{
- if |a| == 0 && |b| == 0 then
+ if |a| == pos && |b| == pos then
false
- else if |a| == 0 then
+ else if |a| == pos then
true
- else if |b| == 0 then
+ else if |b| == pos then
false
+ else if a[pos] == b[pos] then
+ UnicodeLess(a, b, pos+1) // correct independent of surrogate status
else
- if a[0] == b[0] then
- UnicodeLess(a[1..], b[1..]) // correct independent of surrogate status
- else
- var aIsHighSurrogate := IsHighSurrogate(a[0]);
- var bIsHighSurrogate := IsHighSurrogate(b[0]);
+ var aIsHighSurrogate := IsHighSurrogate(a[pos]);
+ var bIsHighSurrogate := IsHighSurrogate(b[pos]);
if aIsHighSurrogate == bIsHighSurrogate then
- a[0] < b[0]
+ a[pos] < b[pos]
else
bIsHighSurrogate
- // we know aIsHighSurrogate != bIsHighSurrogate and a[0] != b[0]
+ // we know aIsHighSurrogate != bIsHighSurrogate and a[pos] != b[pos]
// so if bIsHighSurrogate then a is less
// and if aIsHighSurrogate then a is greater
}
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy
index c3cdbf5f6..1dae70d08 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy
@@ -23,11 +23,12 @@ module DdbVirtualFields {
import DDB = ComAmazonawsDynamodbTypes
import Seq
import TermLoc
+ import StandardLibrary.Sequence
function method ParseVirtualFieldConfig(vf : VirtualField) : Result<VirtField, Error>
{
- var parts :- Seq.MapWithResult((p : VirtualPart) => ParseVirtualPartConfig(p), vf.parts);
+ var parts :- Sequence.MapWithResult((p : VirtualPart) => ParseVirtualPartConfig(p), vf.parts);
Success(VirtField(vf.name, parts))
}
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
index 5930ae6ce..abd39ddd3 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -821,11 +821,11 @@ module StructuredEncryptionHeader {
}
// GetOneKVPair ==> SerializeOneKVPair
- lemma GetOneKVPairRoundTrip(data : Bytes)
- requires GetOneKVPair(data, 0).Success?
+ lemma GetOneKVPairRoundTrip(data : Bytes, pos : nat)
+ requires GetOneKVPair(data, pos).Success?
ensures
- && var cont := GetOneKVPair(data, 0).value;
- && SerializeOneKVPair(cont.0, cont.1) == data[..cont.2]
+ && var cont := GetOneKVPair(data, pos).value;
+ && SerializeOneKVPair(cont.0, cont.1) == data[pos..cont.2+pos]
{}
// SerializeOneDataKey ==> GetOneDataKey
diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
index 551dd83b7..61a325668 100644
--- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
import JsonConfig
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
import KeyVectors
+ import OsLang
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
returns (output : Result<bool, string>)
@@ -110,6 +111,14 @@ module {:options "-functionSyntax:4"} DecryptManifest {
}
}
+ function LogFileName() : string
+ {
+ if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
+ "..\\..\\PerfLog.txt"
+ else
+ "../../PerfLog.txt"
+ }
+
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
returns (output : Result<bool, string>)
requires keyVectors.ValidState()
@@ -174,7 +183,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
var _ :- OneTest(obj.0, obj.1, keyVectors);
}
- Time.PrintTimeSinceLong(time, "DB-ESDK-TV " + inFile);
+ Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
timeStamp :- expect Time.GetCurrentTimeStamp();
print timeStamp + " Tests Complete.\n";
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 70d6a59a7..d5c4a20d9 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 70d6a59a732261e4aee3ccf6f69dfeb319f3bf3e
+Subproject commit d5c4a20d97d5e074f874d672f22cef996b2c5079
From bfa2d684c515195efc9d747f59c899982df6b154 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Tue, 3 Dec 2024 13:35:17 -0800
Subject: [PATCH 15/26] Update some of the proof
---
.../src/OptimizedMergeSort.dfy | 44 ++++++++++++++-----
1 file changed, 33 insertions(+), 11 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index 7b3ba1b36..e071bfa9e 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -105,7 +105,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.TotalOrdering(lessThanOrEq)
requires lo < hi <= left.Length
requires hi <= right.Length && left != right
- // reads left, right
+ reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -217,6 +217,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
// reads left, right
modifies right
+ reads left, right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
// We do not modify anything above hi
@@ -239,8 +240,10 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq)
invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq)
invariant Relations.SortedBy(right[lo..iter], lessThanOrEq)
- invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition]) + multiset(left[mid..rightPosition])
+ invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition])
{
+
+ ghost var oldRightPosition, oldIter, oldLeftPosition := rightPosition, iter, leftPosition;
if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
right[iter] := left[rightPosition];
@@ -255,7 +258,26 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
PushStillSortedBy(right, lo, iter, lessThanOrEq);
leftPosition, iter := leftPosition + 1, iter + 1;
+ assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
+ if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| {
+ } else {
+ assert rightPosition == oldRightPosition;
+ assert oldLeftPosition < mid;
+ // This is true, but uncommenting it causes the proof to fail
+ // leaving it here it make what is going on a little more clear
+ // assert right[lo..iter][|right[lo..iter]| - 1] == right[oldIter];
+ assert left[leftPosition..mid][0] == left[leftPosition];
+ }
+ }
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+
+ assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
+ if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
+ } else {
+ assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1];
+ assert left[rightPosition..hi][0] == left[rightPosition];
+ }
+ }
BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
}
}
@@ -362,7 +384,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
&& right.Length < UINT64_LIMIT
requires lo < hi <= left.Length as uint64
requires hi <= right.Length as uint64 && left != right
- // reads left, right
+ reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -485,7 +507,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
// We store "right" in [mid..hi]
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
- // reads left, right
+ reads left, right
modifies right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
@@ -509,9 +531,10 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq)
invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq)
invariant Relations.SortedBy(right[lo..iter], lessThanOrEq)
- invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition]) + multiset(left[mid..rightPosition])
+ invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition])
{
- label BEFORE_WORK:
+
+ ghost var oldRightPosition, oldIter, oldLeftPosition := rightPosition, iter, leftPosition;
if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
right[iter] := left[rightPosition];
@@ -529,11 +552,10 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
leftPosition, iter := leftPosition + 1, iter + 1;
assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
- if 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| {
- assert lessThanOrEq(left[leftPosition-1], left[leftPosition]) by {
- assert lo <= leftPosition-1 < leftPosition < mid;
- assert Relations.SortedBy(left[lo..mid], lessThanOrEq);
- }
+ if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| {
+ } else {
+ assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1];
+ assert left[leftPosition..mid][0] == left[leftPosition];
}
}
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
From 40153a582b3cd900844ef28e87519cd556a3d7c4 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Wed, 12 Feb 2025 15:15:27 -0800
Subject: [PATCH 16/26] Updates to keep inline with Dafny standard library.
---
.../src/OptimizedMergeSort.dfy | 320 +++++++++++++-----
.../StructuredEncryption/src/SortCanon.dfy | 4 +-
2 files changed, 241 insertions(+), 83 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index e071bfa9e..f85b5cb82 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -4,11 +4,16 @@
include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy"
module {:options "-functionSyntax:4"} OptimizedMergeSort {
- import Seq.MergeSort
- import Relations = MergeSort.Relations
- import opened StandardLibrary.UInt
- // The Seq.MergeSort function implemented as implemented
+ import Relations
+ import BoundedInts
+ import InternalModule = Seq.MergeSort
+
+ predicate HasUint64Len<T>(s: seq<T>) {
+ |s| < BoundedInts.TWO_TO_THE_64
+ }
+
+ // The MergeSortBy function implemented as implemented
// does not compile to an optimal implementation
// in any of the Dafny target languages.
// This implementation aims to be significantly more optimal.
@@ -16,15 +21,80 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
// It does this by making 2 arrays of the original sequence
// and then using these 2 as left and right alternatively.
// This can be audited by verifying
- // that the arrays are only sliced into a seq in `FastMergeSort`.
+ // that the arrays are only sliced into a seq in `MergeSortNat`.
// All other slicing is done in ghost state.
// Second, is has a bounded number implementation
// that avoids using `nat`.
- function {:isolate_assertions} FastMergeSort<T(!new)>(s: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
+ function {:isolate_assertions} MergeSort<T(!new)>(s: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
+ requires Relations.TotalOrdering(lessThanOrEq)
+ requires HasUint64Len(s)
+ {
+ InternalModule.MergeSortBy(s, lessThanOrEq)
+ }
+ by method {
+ if |s| <= 1 {
+ return s;
+ } else {
+
+ // The slice x[1..], y[1..] are un-optimized operations in Dafny.
+ // This means that their usage will result in a lot of data copying.
+ // Additional, it is very likely that these size of these sequences
+ // will be less than uint64.
+ // So writing an optimized version that only works on bounded types
+ // should further optimized this hot code.
+
+ var left := new T[|s|](i requires 0 <= i < |s| => s[i]);
+ var right := new T[|s|](i requires 0 <= i < |s| => s[i]);
+ var lo, hi := 0, right.Length;
+
+ label BEFORE_WORK:
+
+ var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64;
+ ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
+
+ result := right[..];
+
+ ghost var other := InternalModule.MergeSortBy(s, lessThanOrEq);
+
+ assert Relations.SortedBy(right[..], lessThanOrEq) by {
+ assert right[..] == right[lo..hi];
+ }
+ assert multiset(right[..]) == multiset(other) by {
+ calc {
+ multiset(right[..]);
+ == {assert right[..] == right[lo..hi];}
+ multiset(right[lo..hi]);
+ ==
+ multiset(old@BEFORE_WORK(left[lo..hi]));
+ == {assert old@BEFORE_WORK(left[lo..hi]) == s;}
+ multiset(s);
+ ==
+ multiset(other);
+ }
+ }
+
+ // Implementing a by method can be complicated.
+ // Because methods can have non-determinism,
+ // where functions can not.
+ // This means that Dafny normally wants to know
+ // that the method and function maintain equality at every step.
+ // But this is hard for this kind of optimized sorting.
+ // Because what is the functional state at every step
+ // and how does it correspond the state of 2 optimized arrays?
+ // This lemma works around this
+ // by proving that the outcomes are always deterministic and the same.
+ // It does this by proving that given a total ordering,
+ // there is one and only one way to sort a given sequence.
+ TotalOrderingImpliesSortingIsUnique(right[..], other, lessThanOrEq);
+ }
+ }
+
+ // This is included as sugar in case you don't want to ensure your seq HasUint64Len.
+ function {:isolate_assertions} MergeSortNat<T(!new)>(s: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
requires Relations.TotalOrdering(lessThanOrEq)
{
- MergeSort.MergeSortBy(s, lessThanOrEq)
+ InternalModule.MergeSortBy(s, lessThanOrEq)
}
by method {
if |s| <= 1 {
@@ -45,17 +115,22 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
label BEFORE_WORK:
if HasUint64Len(s) {
- var boundedLo: uint64, boundedHi: uint64 := 0, right.Length as uint64;
- ghost var _ := BoundedMergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
+ var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64;
+ ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
result := right[..];
} else {
- ghost var _ := MergeSortMethod(left, right, lessThanOrEq, lo, hi, Right);
+ // Fallback to `nat` or BigInt.
+ // This is a little silly, but this ensures
+ // that the behavior for very large seq will be the same.
+ // Though it is likely if any such seq existed in the real world,
+ // the performance improvement here would still not be enough to complete the sort...
+ ghost var _ := NatMergeSortMethod(left, right, lessThanOrEq, lo, hi, Right);
result := right[..];
}
- ghost var other := MergeSort.MergeSortBy(s, lessThanOrEq);
+ ghost var other := InternalModule.MergeSortBy(s, lessThanOrEq);
assert Relations.SortedBy(right[..], lessThanOrEq) by {
assert right[..] == right[lo..hi];
@@ -93,18 +168,26 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
datatype PlaceResults = Left | Right | Either
type ResultPlacement = r: PlaceResults | !r.Either? witness *
+ // These are bounded implementations of merge sort.
+ // This further speeds things up
+ // because math with bounded variables
+ // is significantly faster that math with big numbers.
+
method {:isolate_assertions} MergeSortMethod<T(!new)>(
left: array<T>,
right: array<T>,
lessThanOrEq: (T, T) -> bool,
- lo: nat,
- hi: nat,
+ lo: BoundedInts.uint64,
+ hi: BoundedInts.uint64,
where: PlaceResults
)
returns (resultPlacement: ResultPlacement)
requires Relations.TotalOrdering(lessThanOrEq)
- requires lo < hi <= left.Length
- requires hi <= right.Length && left != right
+ requires left.Length < BoundedInts.TWO_TO_THE_64
+ requires right.Length < BoundedInts.TWO_TO_THE_64
+ requires lo < hi <= left.Length as BoundedInts.uint64
+ requires hi <= right.Length as BoundedInts.uint64
+ requires left != right
reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -131,7 +214,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
}
ghost var beforeWork := multiset(left[lo..hi]);
- var mid := (lo + hi) / 2;
+ var mid := ((hi - lo)/2) + lo;
var placement? := MergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
assert left[mid..hi] == old(left[mid..hi]);
ghost var placement2? := MergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
@@ -140,33 +223,47 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
ghost var preMergeResult := if placement?.Left? then left else right;
calc {
multiset(preMergeResult[lo..hi]);
- == { assert preMergeResult[lo..hi] == preMergeResult[lo..mid] + preMergeResult[mid..hi]; }
+ == { LemmaSplitAt(preMergeResult[..], lo as nat, mid as nat, hi as nat); }
multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]);
==
multiset(old(left[lo..mid]) + old(left[mid..hi]));
- == { assert old(left[lo..hi]) == old(left[lo..mid]) + old(left[mid..hi]); }
+ == { LemmaSplitAt(old(left[..]), lo as nat, mid as nat, hi as nat); }
beforeWork;
}
ghost var mergedResult;
if placement?.Left? {
MergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
- resultPlacement := Right;
+ resultPlacement, mergedResult := Right, right[lo..hi];
- mergedResult := right[lo..hi];
- assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
} else {
assert placement?.Right?;
MergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
- resultPlacement := Left;
+ resultPlacement, mergedResult := Left, left[lo..hi];
- mergedResult := left[lo..hi];
- assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
}
label BEFORE_RETURN:
- assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
if resultPlacement.Left? && where == Right {
+ // A forall comprehension might seem like a nice fit here,
+ // however this does not good for two reasons.
+ // First, Dafny currently creates a range for the full bounds of the bounded number
+ // see: https://github.com/dafny-lang/dafny/issues/5897
+ // Second this would create two loops.
+ // First loop would create the `lo to hi` range of numbers.
+ // The second loop would then loop over these elements.
for i := lo to hi
modifies right
invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
@@ -174,9 +271,12 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant right[lo..i] == left[lo..i]
{
right[i] := left[i];
+ assert right[lo..i] == left[lo..i];
}
- assert right[lo..hi] == mergedResult;
+ assert right[lo..hi] == mergedResult by {
+ assert mergedResult == left[lo..hi];
+ }
assert left[..] == old@BEFORE_RETURN(left[..]);
assert right[..lo] == old(right[..lo]);
@@ -190,9 +290,12 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant left[lo..i] == right[lo..i]
{
left[i] := right[i];
+ assert right[lo..i] == left[lo..i];
}
- assert left[lo..hi] == mergedResult;
+ assert left[lo..hi] == mergedResult by {
+ assert mergedResult == right[lo..hi];
+ }
assert right[..] == old@BEFORE_RETURN(right[..]);
assert left[..lo] == old(left[..lo]);
@@ -204,20 +307,22 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
nameonly left: array<T>,
nameonly right: array<T>,
nameonly lessThanOrEq: (T, T) -> bool,
- nameonly lo: nat,
- nameonly mid: nat,
- nameonly hi: nat
+ nameonly lo: BoundedInts.uint64,
+ nameonly mid: BoundedInts.uint64,
+ nameonly hi: BoundedInts.uint64
)
requires Relations.TotalOrdering(lessThanOrEq)
- requires lo <= mid <= hi <= left.Length
- requires hi <= right.Length && left != right
+ requires
+ && left.Length < BoundedInts.TWO_TO_THE_64
+ && right.Length < BoundedInts.TWO_TO_THE_64
+ requires lo <= mid <= hi <= left.Length as BoundedInts.uint64
+ requires hi <= right.Length as BoundedInts.uint64 && left != right
// We store "left" in [lo..mid]
requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
// We store "right" in [mid..hi]
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
- // reads left, right
- modifies right
reads left, right
+ modifies right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
// We do not modify anything above hi
@@ -231,7 +336,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
modifies right
invariant lo <= leftPosition <= mid <= rightPosition <= hi
- invariant leftPosition - lo + rightPosition - mid == iter - lo
+ invariant leftPosition as nat - lo as nat + rightPosition as nat - mid as nat == iter as nat - lo as nat
invariant right[..lo] == old(right[..lo])
invariant right[hi..] == old(right[hi..])
@@ -247,30 +352,37 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
right[iter] := left[rightPosition];
- PushStillSortedBy(right, lo, iter, lessThanOrEq);
+ PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
rightPosition, iter := rightPosition + 1, iter + 1;
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+
+ assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
+ if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
+ } else {
+ assert Relations.SortedBy(left[oldRightPosition..hi], lessThanOrEq);
+ assert lessThanOrEq(left[oldRightPosition..hi][0], left[oldRightPosition..hi][1]);
+ }
+ }
BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+
+ assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
+ // Dafny just wants to be reminded
+ }
} else {
right[iter] := left[leftPosition];
- PushStillSortedBy(right, lo, iter, lessThanOrEq);
+ PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
leftPosition, iter := leftPosition + 1, iter + 1;
assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| {
} else {
- assert rightPosition == oldRightPosition;
- assert oldLeftPosition < mid;
- // This is true, but uncommenting it causes the proof to fail
- // leaving it here it make what is going on a little more clear
- // assert right[lo..iter][|right[lo..iter]| - 1] == right[oldIter];
- assert left[leftPosition..mid][0] == left[leftPosition];
+ assert Relations.SortedBy(left[oldLeftPosition..mid], lessThanOrEq);
+ assert lessThanOrEq(left[oldLeftPosition..mid][0], left[oldLeftPosition..mid][1]);
}
}
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
-
assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
} else {
@@ -279,10 +391,15 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
}
}
BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+
+ assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
+ // Dafny just wants to be reminded
+ }
}
}
assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by {
assert leftPosition == mid && rightPosition == hi;
+ LemmaSplitAt(left[..], lo as nat, mid as nat, hi as nat);
assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi];
}
}
@@ -362,28 +479,37 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
assert a == a' == b' == b;
}
- // These are bounded implementations of the above.
- // They do exactly the same thing,
- // but they use `uint64`.
- // This further speeds things up
- // because math with bounded variables
- // is significantly faster that math with big numbers.
+ lemma LemmaNewFirstElementStillSortedBy<T(!new)>(x: T, s: seq<T>, lessThan: (T, T) -> bool)
+ requires Relations.SortedBy(s, lessThan)
+ requires |s| == 0 || lessThan(x, s[0])
+ requires Relations.TotalOrdering(lessThan)
+ ensures Relations.SortedBy([x] + s, lessThan)
+ {}
- method {:isolate_assertions} BoundedMergeSortMethod<T(!new)>(
+ lemma LemmaSplitAt<T>(s: seq<T>, lo: nat, split: nat, hi: nat)
+ requires 0 <= lo
+ requires lo <= split
+ requires split <= hi
+ requires hi <= |s|
+ ensures s[lo..hi] == s[lo..split] + s[split..hi]
+ {}
+
+ // This is the nat version of merge sort.
+ // This is an exact copy of the bounded integer implementation above
+ // but with `nat` instead of BoundedInts.uint64.
+
+ method {:isolate_assertions} NatMergeSortMethod<T(!new)>(
left: array<T>,
right: array<T>,
lessThanOrEq: (T, T) -> bool,
- lo: uint64,
- hi: uint64,
+ lo: nat,
+ hi: nat,
where: PlaceResults
)
returns (resultPlacement: ResultPlacement)
requires Relations.TotalOrdering(lessThanOrEq)
- requires
- && left.Length < UINT64_LIMIT
- && right.Length < UINT64_LIMIT
- requires lo < hi <= left.Length as uint64
- requires hi <= right.Length as uint64 && left != right
+ requires lo < hi <= left.Length
+ requires hi <= right.Length && left != right
reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -411,42 +537,51 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
ghost var beforeWork := multiset(left[lo..hi]);
var mid := ((hi - lo)/2) + lo;
- var placement? := BoundedMergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
+ var placement? := NatMergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
assert left[mid..hi] == old(left[mid..hi]);
- ghost var placement2? := BoundedMergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
+ ghost var placement2? := NatMergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
assert placement2? == placement?;
ghost var preMergeResult := if placement?.Left? then left else right;
calc {
multiset(preMergeResult[lo..hi]);
- == { assert preMergeResult[lo..hi] == preMergeResult[lo..mid] + preMergeResult[mid..hi]; }
+ == { LemmaSplitAt(preMergeResult[..], lo as nat, mid as nat, hi as nat); }
multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]);
==
multiset(old(left[lo..mid]) + old(left[mid..hi]));
- == { assert old(left[lo..hi]) == old(left[lo..mid]) + old(left[mid..hi]); }
+ == { LemmaSplitAt(old(left[..]), lo as nat, mid as nat, hi as nat); }
beforeWork;
}
ghost var mergedResult;
if placement?.Left? {
- BoundedMergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ NatMergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
resultPlacement, mergedResult := Right, right[lo..hi];
- assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
} else {
assert placement?.Right?;
- BoundedMergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
+ NatMergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
resultPlacement, mergedResult := Left, left[lo..hi];
- assert left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
}
label BEFORE_RETURN:
- assert left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo]);
+ assert left[hi..] == old(left[hi..]);
+ assert right[hi..] == old(right[hi..]);
+ assert left[..lo] == old(left[..lo]);
+ assert right[..lo] == old(right[..lo]);
if resultPlacement.Left? && where == Right {
// A forall comprehension might seem like a nice fit here,
// however this does not good for two reasons.
- // First, Dafny currently creates a range fur the full bounds of the bounded number
+ // First, Dafny currently creates a range for the full bounds of the bounded number
// see: https://github.com/dafny-lang/dafny/issues/5897
// Second this would create two loops.
// First loop would create the `lo to hi` range of numbers.
@@ -459,6 +594,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant right[lo..i] == left[lo..i]
{
right[i] := left[i];
+ assert right[lo..i] == left[lo..i];
}
assert right[lo..hi] == mergedResult by {
@@ -477,6 +613,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
invariant left[lo..i] == right[lo..i]
{
left[i] := right[i];
+ assert right[lo..i] == left[lo..i];
}
assert left[lo..hi] == mergedResult by {
@@ -489,26 +626,24 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
}
}
- method {:isolate_assertions} BoundedMergeIntoRight<T(!new)>(
+ method {:isolate_assertions} NatMergeIntoRight<T(!new)>(
nameonly left: array<T>,
nameonly right: array<T>,
nameonly lessThanOrEq: (T, T) -> bool,
- nameonly lo: uint64,
- nameonly mid: uint64,
- nameonly hi: uint64
+ nameonly lo: nat,
+ nameonly mid: nat,
+ nameonly hi: nat
)
requires Relations.TotalOrdering(lessThanOrEq)
- requires
- && left.Length < UINT64_LIMIT
- && right.Length < UINT64_LIMIT
- requires lo <= mid <= hi <= left.Length as uint64
- requires hi <= right.Length as uint64 && left != right
+ requires lo <= mid <= hi <= left.Length
+ requires hi <= right.Length && left != right
// We store "left" in [lo..mid]
requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
// We store "right" in [mid..hi]
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
- reads left, right
+ // reads left, right
modifies right
+ reads left, right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
// We do not modify anything above hi
@@ -543,8 +678,18 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
- assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]);
+ assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
+ if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
+ } else {
+ assert Relations.SortedBy(left[oldRightPosition..hi], lessThanOrEq);
+ assert lessThanOrEq(left[oldRightPosition..hi][0], left[oldRightPosition..hi][1]);
+ }
+ }
BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+
+ assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
+ // Dafny just wants to be reminded
+ }
} else {
right[iter] := left[leftPosition];
@@ -554,17 +699,30 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| {
} else {
- assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1];
- assert left[leftPosition..mid][0] == left[leftPosition];
+ assert Relations.SortedBy(left[oldLeftPosition..mid], lessThanOrEq);
+ assert lessThanOrEq(left[oldLeftPosition..mid][0], left[oldLeftPosition..mid][1]);
}
}
BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
+ assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
+ if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
+ } else {
+ assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1];
+ assert left[rightPosition..hi][0] == left[rightPosition];
+ }
+ }
BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
+
+ assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
+ // Dafny just wants to be reminded
+ }
}
}
assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by {
assert leftPosition == mid && rightPosition == hi;
+ LemmaSplitAt(left[..], lo as nat, mid as nat, hi as nat);
assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi];
}
}
+
}
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
index ae86e268b..f4a5fbde2 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
@@ -311,7 +311,7 @@ module SortCanon {
ret
} by method {
AuthBelowIsTotal();
- result := OptimizedMergeSort.FastMergeSort(x, AuthBelow);
+ result := OptimizedMergeSort.MergeSortNat(x, AuthBelow);
CanonAuthListMultiNoDup(x, result);
assert CanonAuthListHasNoDuplicates(result);
}
@@ -331,7 +331,7 @@ module SortCanon {
ret
} by method {
CryptoBelowIsTotal();
- result := OptimizedMergeSort.FastMergeSort(x, CryptoBelow);
+ result := OptimizedMergeSort.MergeSortNat(x, CryptoBelow);
CanonCryptoListMultiNoDup(x, result);
assert CanonCryptoListHasNoDuplicates(result);
}
From 286e7c7a46bf6f08013eab6655ecb43bb2535341 Mon Sep 17 00:00:00 2001
From: seebees <ryanemer@amazon.com>
Date: Wed, 12 Feb 2025 15:30:43 -0800
Subject: [PATCH 17/26] reads on methods not enabled
---
.../StructuredEncryption/src/OptimizedMergeSort.dfy | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index f85b5cb82..2ed337996 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -188,7 +188,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires lo < hi <= left.Length as BoundedInts.uint64
requires hi <= right.Length as BoundedInts.uint64
requires left != right
- reads left, right
+ // reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -321,7 +321,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
// We store "right" in [mid..hi]
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
- reads left, right
+ // reads left, right
modifies right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
@@ -510,7 +510,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.TotalOrdering(lessThanOrEq)
requires lo < hi <= left.Length
requires hi <= right.Length && left != right
- reads left, right
+ // reads left, right
modifies left, right
ensures !where.Either? ==> where == resultPlacement
@@ -641,9 +641,8 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
// We store "right" in [mid..hi]
requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
- // reads left, right
modifies right
- reads left, right
+ // reads left, right
// We do not modify anything before lo
ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
// We do not modify anything above hi
From 6118d8a554a677ae533ee586362bcfed80607512 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Thu, 13 Feb 2025 10:39:00 -0500
Subject: [PATCH 18/26] chore(dafny): add timing support
---
.../dafny/DDBEncryption/src/DecryptManifest.dfy | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
index 5ee680b4e..61a325668 100644
--- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
@@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
import JsonConfig
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
import KeyVectors
+ import OsLang
method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
returns (output : Result<bool, string>)
@@ -110,6 +111,14 @@ module {:options "-functionSyntax:4"} DecryptManifest {
}
}
+ function LogFileName() : string
+ {
+ if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
+ "..\\..\\PerfLog.txt"
+ else
+ "../../PerfLog.txt"
+ }
+
method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
returns (output : Result<bool, string>)
requires keyVectors.ValidState()
@@ -168,11 +177,13 @@ module {:options "-functionSyntax:4"} DecryptManifest {
}
}
+ var time := Time.GetAbsoluteTime();
for i := 0 to |tests.value| {
var obj := tests.value[i];
:- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
var _ :- OneTest(obj.0, obj.1, keyVectors);
}
+ Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
timeStamp :- expect Time.GetCurrentTimeStamp();
print timeStamp + " Tests Complete.\n";
From 13bb0c8081b749a788d8d60468e9d50204c66688 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Thu, 13 Feb 2025 10:39:31 -0500
Subject: [PATCH 19/26] chore(dafny): add timing support
---
submodules/MaterialProviders | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 70e580991..c503da828 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 70e580991678387ce897a286c4f7f449aa616785
+Subproject commit c503da8285a510b25ace619b2cc27ffa247840ee
From b8915c53c9a4d2449f8e95267a35ae92866e70a7 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 14 Mar 2025 12:11:03 -0400
Subject: [PATCH 20/26] m
---
submodules/MaterialProviders | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index d5c4a20d9..841e263e0 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit d5c4a20d97d5e074f874d672f22cef996b2c5079
+Subproject commit 841e263e0a3a17ce99d33b02cda27597e32fc86a
From 04641d218720e798476d3fc8aa68cdc26c6070b1 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Tue, 25 Mar 2025 10:07:10 -0400
Subject: [PATCH 21/26] m
---
submodules/MaterialProviders | 2 +-
submodules/smithy-dafny | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 5ef166374..5ac41210f 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 5ef166374997984fe34e1ff28d5589ad1f2573d8
+Subproject commit 5ac41210f9b933a105a4eb6443a920a348453f34
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index 5fb3f25ea..b82c09eca 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 5fb3f25ea3444c51b2ad30b25ab03964cf866cd1
+Subproject commit b82c09eca754d242d1c50281b76aed8d687f9f93
From 6420c5a1da91fba343add7cf4292b2694bff9cce Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Tue, 25 Mar 2025 10:23:39 -0400
Subject: [PATCH 22/26] m
---
submodules/MaterialProviders | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 5ac41210f..977f43119 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 5ac41210f9b933a105a4eb6443a920a348453f34
+Subproject commit 977f431198e84ac7c9b2efa460f37596d5e350c4
From 06c119532a5ea094f725381fab7526cb6e3ec780 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 28 Mar 2025 11:18:25 -0400
Subject: [PATCH 23/26] m
---
.../test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy | 4 ++--
submodules/MaterialProviders | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
index 91633e3db..ee74a7383 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy
@@ -24,7 +24,7 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
assert s == UTF8.EncodeAscii("def");
s
- const awskms : UTF8.ValidUTF8Bytes :=
+ const aws_kms : UTF8.ValidUTF8Bytes :=
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73];
assert s == UTF8.EncodeAscii("aws-kms");
s
@@ -57,7 +57,7 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
const testLegend : Legend := [0x65, 0x73]
const testEncContext : CMPEncryptionContext := map[abc := def]
const testAwsKmsDataKey := CMP.EncryptedDataKey(
- keyProviderId := awskms ,
+ keyProviderId := aws_kms ,
keyProviderInfo := keyproviderInfo,
ciphertext := [1, 2, 3, 4, 5])
const testAwsKmsHDataKey := CMP.EncryptedDataKey(
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 977f43119..ab521336e 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 977f431198e84ac7c9b2efa460f37596d5e350c4
+Subproject commit ab521336ea59c6df2430b87519b3c931e967ed30
From 14a43111cd21e900ed76c0aaf8640b1ac3666bba Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Tue, 8 Apr 2025 11:08:27 -0400
Subject: [PATCH 24/26] m
---
.../test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
index 5117ac892..43585a0e8 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy
@@ -29,8 +29,8 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
const BRANCH_KEY_ID := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
const BRANCH_KEY_ID_UTF8 : UTF8.ValidUTF8Bytes :=
- var s := [0x37, 0x35, 0x37, 0x38, 0x39, 0x31, 0x31, 0x35, 0x2d, 0x31, 0x64, 0x65, 0x62, 0x2d, 0x34, 0x66, 0x65, 0x33, 0x2d, 0x61, 0x32, 0x65, 0x63, 0x2d, 0x62, 0x65, 0x39, 0x65, 0x38, 0x38, 0x35, 0x64, 0x31, 0x39, 0x34, 0x35];
- assert s == UTF8.EncodeAscii(BRANCH_KEY_ID);
+ var s := [0x33, 0x66, 0x34, 0x33, 0x61, 0x39, 0x61, 0x66, 0x2d, 0x30, 0x38, 0x63, 0x35, 0x2d, 0x34, 0x33, 0x31, 0x37, 0x2d, 0x62, 0x36, 0x39, 0x34, 0x2d, 0x33, 0x64, 0x33, 0x65, 0x38, 0x38, 0x33, 0x64, 0x63, 0x61, 0x65, 0x66];
+ assert s == UTF8.EncodeAscii("3f43a9af-08c5-4317-b694-3d3e883dcaef");
s
const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
From cf528f53c7dd1a6759cf33914f7264d9b157ec81 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Wed, 9 Apr 2025 13:57:12 -0400
Subject: [PATCH 25/26] m
---
submodules/MaterialProviders | 2 +-
submodules/smithy-dafny | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 5e6458921..d808fd88d 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 5e64589215eb4cf9337f5d4fac24a815d0f28831
+Subproject commit d808fd88df92acf64fb9ca0e7c652d72e05fa50a
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index b82c09eca..72f38c32d 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit b82c09eca754d242d1c50281b76aed8d687f9f93
+Subproject commit 72f38c32dab1cc3d5b12db959e738dc4d46e950f
From dc551b2b99fc74ef394d5c67609afc106827b21f Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Mon, 14 Apr 2025 16:19:29 -0400
Subject: [PATCH 26/26] m
---
DynamoDbEncryption/runtimes/rust/Cargo.toml | 18 +++++++++---------
TestVectors/runtimes/rust/Cargo.toml | 2 +-
submodules/MaterialProviders | 2 +-
submodules/smithy-dafny | 2 +-
4 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/DynamoDbEncryption/runtimes/rust/Cargo.toml b/DynamoDbEncryption/runtimes/rust/Cargo.toml
index cdad092d6..a5877c06d 100644
--- a/DynamoDbEncryption/runtimes/rust/Cargo.toml
+++ b/DynamoDbEncryption/runtimes/rust/Cargo.toml
@@ -16,20 +16,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.15"
+aws-config = "1.6.0"
aws-lc-rs = "1.12.2"
aws-lc-sys = "0.25.0"
-aws-sdk-dynamodb = "1.62.0"
-aws-sdk-kms = "1.57.0"
-aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
-aws-smithy-types = "1.2.12"
-chrono = "0.4.39"
+aws-sdk-dynamodb = "1.69.0"
+aws-sdk-kms = "1.63.0"
+aws-smithy-runtime-api = {version = "1.7.4", features = ["client"] }
+aws-smithy-types = "1.3.0"
+chrono = "0.4.40"
cpu-time = "1.0.0"
-dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"] }
+dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] }
dashmap = "6.1.0"
pem = "3.0.4"
-tokio = {version = "1.43.0", features = ["full"] }
-uuid = { version = "1.12.1", features = ["v4"] }
+tokio = {version = "1.44.1", features = ["full"] }
+uuid = { version = "1.16.0", features = ["v4"] }
[[example]]
name = "main"
diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml
index 3b632b1d7..aad1d58f9 100644
--- a/TestVectors/runtimes/rust/Cargo.toml
+++ b/TestVectors/runtimes/rust/Cargo.toml
@@ -16,7 +16,7 @@ aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
aws-smithy-types = "1.2.12"
chrono = "0.4.39"
cpu-time = "1.0.0"
-dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"] }
+dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] }
dashmap = "6.1.0"
pem = "3.0.4"
tokio = {version = "1.43.0", features = ["full"] }
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index d808fd88d..515995e68 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit d808fd88df92acf64fb9ca0e7c652d72e05fa50a
+Subproject commit 515995e68400e56fc720412fe355e6965715136e
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index 72f38c32d..2f83e28ad 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 72f38c32dab1cc3d5b12db959e738dc4d46e950f
+Subproject commit 2f83e28ad9532b24c93d2229476c9a268355d338