Skip to content

Commit 26fdaac

Browse files
ajewellamzajewellamz
committed
m
1 parent 5e498ed commit 26fdaac

File tree

12 files changed

+57
-23
lines changed

12 files changed

+57
-23
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ module SearchConfigToInfo {
2323
import opened DynamoDbEncryptionUtil
2424
import opened TermLoc
2525
import opened StandardLibrary.String
26-
import opened MemoryMath
26+
import opened StandardLibrary.MemoryMath
2727
import MaterialProviders
2828
import SortedSets
2929

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ module DynamoToStruct {
2020
import SE = StructuredEncryptionUtil
2121
import StandardLibrary.Sequence
2222
import DafnyLibraries
23-
import opened MemoryMath
23+
import opened StandardLibrary.MemoryMath
2424

2525
type Error = Types.Error
2626

@@ -126,7 +126,7 @@ module DynamoToStruct {
126126
var badNames := set k <- s | !IsValid_AttributeName(k) :: k;
127127
OneBadKey(s, badNames, IsValid_AttributeName);
128128
// We happen to order these values, but this ordering MUST NOT be relied upon.
129-
var orderedAttrNames := SetToOrderedSequence(badNames, CharLess);
129+
var orderedAttrNames := SortedSets.ComputeSetToOrderedSequence2(badNames, CharLess);
130130
var attrNameList := Join(orderedAttrNames, ",");
131131
MakeError("Not valid attribute names : " + attrNameList)
132132
}
@@ -1369,7 +1369,7 @@ module DynamoToStruct {
13691369
var badValues := FlattenErrors(m);
13701370
assert(|badValues| > 0);
13711371
// We happen to order these values, but this ordering MUST NOT be relied upon.
1372-
var badValueSeq := SetToOrderedSequence(badValues, CharLess);
1372+
var badValueSeq := SortedSets.ComputeSetToOrderedSequence2(badValues, CharLess);
13731373
Failure(Join(badValueSeq, "\n"))
13741374
}
13751375
}

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy

Lines changed: 44 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,38 @@ module TermLoc {
2626
import opened StandardLibrary.UInt
2727
import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
2828
import opened DynamoDbEncryptionUtil
29+
import opened StandardLibrary.MemoryMath
2930
import StandardLibrary.String
3031
import DDB = ComAmazonawsDynamodbTypes
3132
import Seq
3233
import DynamoToStruct
3334

35+
// function method {:tailrecursion} CountEven(x : seq<uint8>, pos : nat) : nat
36+
// requires pos <= |x|
37+
// decreases |x| - pos
38+
// {
39+
// if pos == |x| then
40+
// 0
41+
// else if x[0] % 2 == 0 then
42+
// 1 + CountEven(x, pos+1)
43+
// else
44+
// CountEven(x, pos+1)
45+
// }
46+
47+
function method {:tailrecursion} CountEven(x : seq<uint8>, pos : uint64 := 0) : (ret : uint64)
48+
requires pos as nat <= |x|
49+
ensures ret as nat <= |x| - pos as nat
50+
decreases |x| - pos as nat
51+
{
52+
SequenceIsSafeBecauseItIsInMemory(x);
53+
if pos == |x| as uint64 then
54+
0
55+
else if x[0] % 2 == 0 then
56+
1 + CountEven(x, pos+1)
57+
else
58+
CountEven(x, pos+1)
59+
}
60+
3461
datatype Selector =
3562
| List(pos : uint64)
3663
| Map(key : string)
@@ -175,9 +202,9 @@ module TermLoc {
175202
// return the number of characters until the next part begins
176203
// that is, '[' or '.'
177204
function method {:opaque} FindStartOfNext(s : string)
178-
: (index : Option<nat>)
205+
: (index : Option<uint64>)
179206
ensures index.Some? ==>
180-
&& index.value < |s|
207+
&& index.value as nat < |s|
181208
&& (s[index.value] == '.' || s[index.value] == '[')
182209
&& '.' !in s[..index.value]
183210
&& '[' !in s[..index.value]
@@ -199,13 +226,20 @@ module TermLoc {
199226
}
200227

201228
// read an unsigned decimal number, return value and length
202-
function method {:opaque} GetNumber(s : string, acc : nat := 0)
203-
: Result<nat, Error>
229+
// error if value exceeds 2^64
230+
function method {:opaque} GetNumber(s : string, acc : uint64 := 0, pos : uint64 := 0)
231+
: Result<uint64, Error>
232+
requires pos as nat <= |s|
233+
decreases |s| - pos as nat
204234
{
205-
if |s| == 0 then
235+
SequenceIsSafeBecauseItIsInMemory(s);
236+
if |s| as uint64 == pos then
206237
Success(acc)
207238
else if '0' <= s[0] <= '9' then
208-
GetNumber(s[1..], acc * 10 + s[0] as nat - '0' as nat)
239+
if acc < 0xfff_ffff_ffff_ffff then
240+
GetNumber(s, acc * 10 + s[0] as uint64 - '0' as uint64, Add(pos, 1))
241+
else
242+
Failure(E("Number is too big for list index : " + s))
209243
else
210244
Failure(E("Unexpected character in number : " + [s[0]]))
211245
}
@@ -231,18 +265,18 @@ module TermLoc {
231265
if s[|s|-1] != ']' then
232266
Failure(E("List index must end with ]"))
233267
else
234-
var num :- GetNumber(s[1..|s|-1]);
235-
:- Need(HasUint64Size(num), E("Array selector exceeds maximum."));
236-
Success(List(num as uint64))
268+
var num : uint64 :- GetNumber(s[1..|s|-1]);
269+
Success(List(num))
237270
}
238271

239272
// convert string to SelectorList
240273
function method {:tailrecursion} {:opaque} GetSelectors(s : string, acc : SelectorList := [])
241274
: Result<SelectorList, Error>
242275
requires |s| > 0 && (s[0] == '.' || s[0] == '[')
243276
{
277+
SequenceIsSafeBecauseItIsInMemory(s);
244278
var pos := FindStartOfNext(s[1..]);
245-
var end := if pos.None? then |s| else pos.value + 1;
279+
var end := if pos.None? then |s| as uint64 else Add(pos.value, 1);
246280
var sel : Selector :- GetSelector(s[..end]);
247281
:- Need(HasUint64Size(|acc|+1), E("Selector Overflow"));
248282
if pos.None? then

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -251,7 +251,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
251251
SORT_NAME !in ret.value
252252
{
253253
UTF8.EncodeAsciiUnique();
254-
:- Need(config.partitionKeyName in item, DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted"));
254+
:- FNeed(config.partitionKeyName in item, () => DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted"));
255255
var logicalTableName : ValidUTF8Bytes :- DDBEncode(config.logicalTableName);
256256
var partitionName : ValidUTF8Bytes :- DDBEncode(config.partitionKeyName);
257257
var partitionKeyName : ValidUTF8Bytes :- EncodeName(config.partitionKeyName);

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module DynamoDbItemEncryptorUtil {
88
import opened Wrappers
99
import opened StandardLibrary
1010
import opened StandardLibrary.UInt
11-
import opened MemoryMath
11+
import opened StandardLibrary.MemoryMath
1212

1313
import UTF8
1414
import MPL = AwsCryptographyMaterialProvidersTypes

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ include "Canonize.dfy"
1313
module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations {
1414
import opened StructuredEncryptionUtil
1515
import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
16-
import opened MemoryMath
16+
import opened StandardLibrary.MemoryMath
1717

1818
import Base64
1919
import CMP = AwsCryptographyMaterialProvidersTypes

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module {:options "/functionSyntax:4" } Canonize {
1111
import opened Wrappers
1212
import opened StandardLibrary
1313
import opened StandardLibrary.UInt
14-
import opened MemoryMath
14+
import opened StandardLibrary.MemoryMath
1515
import Header = StructuredEncryptionHeader
1616
import Paths = StructuredEncryptionPaths
1717
import SortCanon

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ module StructuredEncryptionFooter {
2323
import opened StandardLibrary.UInt
2424
import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
2525
import opened StructuredEncryptionUtil
26-
import opened MemoryMath
26+
import opened StandardLibrary.MemoryMath
2727
import Primitives = AtomicPrimitives
2828
import Materials
2929
import Header = StructuredEncryptionHeader

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module StructuredEncryptionHeader {
1313
import opened StandardLibrary.UInt
1414
import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
1515
import opened StructuredEncryptionUtil
16-
import opened MemoryMath
16+
import opened StandardLibrary.MemoryMath
1717

1818
import CMP = AwsCryptographyMaterialProvidersTypes
1919
import Prim = AwsCryptographyPrimitivesTypes

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
88
import Relations
99
import BoundedInts
1010
import InternalModule = Seq.MergeSort
11-
import MemoryMath
11+
import StandardLibrary.MemoryMath
1212

1313
predicate HasUint64Len<T>(s: seq<T>) {
1414
|s| < BoundedInts.TWO_TO_THE_64

0 commit comments

Comments
 (0)