Skip to content

Commit 297d00d

Browse files
ajewellamzajewellamz
authored
feat: repair numeric equality (#228)
* feat: repair numeric equality * add numeric test to test vectors * validate numbers in queries * add failure test for malformed number
1 parent 2c1f31a commit 297d00d

File tree

6 files changed

+145
-32
lines changed

6 files changed

+145
-32
lines changed

Diff for: ‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

+49-22
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ module DynamoDBFilterExpr {
4040
import StandardLibrary.String
4141
import CompoundBeacon
4242
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
43+
import Norm = DynamoDbNormalizeNumber
4344

4445
// extract all the attributes from a filter expression
4546
// except for those which do not need the attribute's value
@@ -1125,9 +1126,11 @@ module DynamoDBFilterExpr {
11251126
}
11261127

11271128
// true if middle between left and right
1128-
predicate method is_between(middle : DDB.AttributeValue, left : DDB.AttributeValue, right : DDB.AttributeValue)
1129+
function method is_between(middle : DDB.AttributeValue, left : DDB.AttributeValue, right : DDB.AttributeValue) : Result<bool, Error>
11291130
{
1130-
AttributeLE(left, middle) && AttributeLE(middle, right)
1131+
var leftRet :- AttributeLE(left, middle);
1132+
var rightRet :- AttributeLE(middle, right);
1133+
Success(leftRet && rightRet)
11311134
}
11321135

11331136
// true if target in list
@@ -1166,7 +1169,8 @@ module DynamoDBFilterExpr {
11661169
Failure(E("No Stack for Between"))
11671170
else
11681171
if stack[|stack|-1].Str? && stack[|stack|-2].Str? && stack[|stack|-3].Str? then
1169-
Success(Bool(is_between(stack[|stack|-3].s, stack[|stack|-2].s, stack[|stack|-1].s)))
1172+
var ret :- is_between(stack[|stack|-3].s, stack[|stack|-2].s, stack[|stack|-1].s);
1173+
Success(Bool(ret))
11701174
else
11711175
Failure(E("Wrong Types for contains"))
11721176

@@ -1257,43 +1261,66 @@ module DynamoDBFilterExpr {
12571261
LexicographicLessOrEqual(b, a, less)
12581262
}
12591263

1260-
predicate method CharLess(a: char, b: char) { a < b }
1261-
predicate method ByteLess(a: uint8, b: uint8) { a < b }
1264+
function method CompareFloat(x : string, y : string) : Result<FloatCompare.CompareType, Error>
1265+
{
1266+
var newX :- Norm.NormalizeNumber(x).MapFailure(e => E(e));
1267+
var newY :- Norm.NormalizeNumber(y).MapFailure(e => E(e));
1268+
Success(FloatCompare.CompareFloat(newX, newY))
1269+
}
12621270

1263-
predicate method AttributeLE(a : DDB.AttributeValue, b : DDB.AttributeValue)
1271+
function method AttributeEQ(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
12641272
{
12651273
if a.N? && b.N? then
1266-
FloatCompare.CompareFloat(a.N, b.N) <= 0
1274+
var ret :- CompareFloat(a.N, b.N);
1275+
Success(ret == 0)
1276+
else
1277+
Success(a == b)
1278+
}
1279+
1280+
function method AttributeNE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
1281+
{
1282+
var ret :- AttributeEQ(a, b);
1283+
Success(!ret)
1284+
}
1285+
1286+
function method AttributeLE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
1287+
{
1288+
if a.N? && b.N? then
1289+
var ret :- CompareFloat(a.N, b.N);
1290+
Success(ret <= 0)
12671291
else if a.S? && b.S? then
1268-
LexicographicLessOrEqual(a.S, b.S, CharLess)
1292+
Success(LexicographicLessOrEqual(a.S, b.S, CharLess))
12691293
else if a.B? && b.B? then
1270-
LexicographicLessOrEqual(a.B, b.B, ByteLess)
1294+
Success(LexicographicLessOrEqual(a.B, b.B, ByteLess))
12711295
else
1272-
false
1296+
Success(false)
12731297
}
1274-
predicate method AttributeLT(a : DDB.AttributeValue, b : DDB.AttributeValue)
1298+
function method AttributeLT(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
12751299
{
1276-
!AttributeLE(b,a)
1300+
var ret :- AttributeLE(b,a);
1301+
Success(!ret)
12771302
}
1278-
predicate method AttributeGT(a : DDB.AttributeValue, b : DDB.AttributeValue)
1303+
function method AttributeGT(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
12791304
{
1280-
!AttributeLE(a,b)
1305+
var ret :- AttributeLE(a,b);
1306+
Success(!ret)
12811307
}
1282-
predicate method AttributeGE(a : DDB.AttributeValue, b : DDB.AttributeValue)
1308+
function method AttributeGE(a : DDB.AttributeValue, b : DDB.AttributeValue) : Result<bool, Error>
12831309
{
1284-
AttributeLE(b,a)
1310+
var ret :- AttributeLE(b,a);
1311+
Success(ret)
12851312
}
12861313

12871314
// apply the comparison function
12881315
function method apply_binary_comp(input : Token, x : DDB.AttributeValue, y : DDB.AttributeValue) : Result<bool, Error>
12891316
{
12901317
match input
1291-
case Eq => Success(x == y)
1292-
case Ne => Success(x != y)
1293-
case Le => Success(AttributeLE(x, y))
1294-
case Lt => Success(AttributeLT(x, y))
1295-
case Ge => Success(AttributeGE(x, y))
1296-
case Gt => Success(AttributeGT(x, y))
1318+
case Eq => AttributeEQ(x, y)
1319+
case Ne => AttributeNE(x, y)
1320+
case Le => AttributeLE(x, y)
1321+
case Lt => AttributeLT(x, y)
1322+
case Ge => AttributeGE(x, y)
1323+
case Gt => AttributeGT(x, y)
12971324
case _ => Failure(E("invalid op in apply_binary_bool"))
12981325
}
12991326

Diff for: ‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

+53
Original file line numberDiff line numberDiff line change
@@ -274,6 +274,59 @@ module TestDynamoDBFilterExpr {
274274
newItems :- expect FilterResults(bv, [item1], None, Some("three = two"), None, None);
275275
expect_equal(newItems, [item1]);
276276
}
277+
278+
method {:test} TestFilterFailNumeric() {
279+
var item1 : DDB.AttributeMap := map[
280+
"one" := DN("800")
281+
];
282+
var values : DDB.ExpressionAttributeValueMap := map [
283+
":two" := DN("foo")
284+
];
285+
var version := GetLotsaBeacons();
286+
var src := GetLiteralSource([1,2,3,4,5], version);
287+
var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src);
288+
var newItems := FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values));
289+
expect newItems.Failure?;
290+
expect newItems.error == E("Number needs digits either before or after the decimal point. when parsing 'foo'.");
291+
}
292+
293+
method {:test} TestFilterCompareNumeric() {
294+
var item1 : DDB.AttributeMap := map[
295+
"one" := DN("800")
296+
];
297+
var values : DDB.ExpressionAttributeValueMap := map [
298+
":two" := DN("0800.000e0")
299+
];
300+
var version := GetLotsaBeacons();
301+
var src := GetLiteralSource([1,2,3,4,5], version);
302+
var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src);
303+
var newItems :- expect FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values));
304+
expect_equal(newItems, []);
305+
newItems :- expect FilterResults(bv, [item1], None, Some("one > :two"), None, Some(values));
306+
expect_equal(newItems, []);
307+
newItems :- expect FilterResults(bv, [item1], None, Some("one <= :two"), None, Some(values));
308+
expect_equal(newItems, [item1]);
309+
newItems :- expect FilterResults(bv, [item1], None, Some("one >= :two"), None, Some(values));
310+
expect_equal(newItems, [item1]);
311+
newItems :- expect FilterResults(bv, [item1], None, Some("one <> :two"), None, Some(values));
312+
expect_equal(newItems, []);
313+
newItems :- expect FilterResults(bv, [item1], None, Some("one = :two"), None, Some(values));
314+
expect_equal(newItems, [item1]);
315+
316+
newItems :- expect FilterResults(bv, [item1], None, Some(":two < one"), None, Some(values));
317+
expect_equal(newItems, []);
318+
newItems :- expect FilterResults(bv, [item1], None, Some(":two > one"), None, Some(values));
319+
expect_equal(newItems, []);
320+
newItems :- expect FilterResults(bv, [item1], None, Some(":two <= one"), None, Some(values));
321+
expect_equal(newItems, [item1]);
322+
newItems :- expect FilterResults(bv, [item1], None, Some(":two >= one"), None, Some(values));
323+
expect_equal(newItems, [item1]);
324+
newItems :- expect FilterResults(bv, [item1], None, Some(":two <> one"), None, Some(values));
325+
expect_equal(newItems, []);
326+
newItems :- expect FilterResults(bv, [item1], None, Some(":two = one"), None, Some(values));
327+
expect_equal(newItems, [item1]);
328+
}
329+
277330
method {:test} TestFilterIn() {
278331
var item1 : DDB.AttributeMap := map[
279332
"one" := DS("abc"),

Diff for: ‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

+23-4
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
2626
import FileIO
2727
import JSON.API
2828
import opened JSONHelpers
29+
import Norm = DynamoDbNormalizeNumber
2930

3031
import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
3132
import DDB = ComAmazonawsDynamodbTypes
@@ -681,8 +682,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
681682

682683
method FindMatchingRecord(expected : DDB.AttributeMap, actual : DDB.ItemList) returns (output : bool)
683684
{
685+
var exp := NormalizeItem(expected);
684686
for i := 0 to |actual| {
685-
if actual[i] == expected {
687+
if actual[i] == exp {
686688
return true;
687689
}
688690
}
@@ -740,7 +742,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
740742
);
741743
var out :- expect client.GetItem(input);
742744
expect out.Item.Some?;
743-
expect out.Item.value == records[i].item;
745+
expect out.Item.value == NormalizeItem(records[i].item);
744746
}
745747
}
746748

@@ -764,13 +766,30 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
764766
}
765767
}
766768

769+
function NormalizeItem(value : DDB.AttributeMap) : DDB.AttributeMap
770+
{
771+
map k <- value :: k := Normalize(value[k])
772+
}
773+
774+
function Normalize(value : DDB.AttributeValue) : DDB.AttributeValue
775+
{
776+
match value {
777+
case N(n) =>
778+
var nn := Norm.NormalizeNumber(n);
779+
if nn.Success? then
780+
DDB.AttributeValue.N(nn.value)
781+
else
782+
value
783+
case _ => value
784+
}
785+
}
767786

768787
method ItemExists(number : DDB.AttributeValue, record : Record, resp : DDB.ItemList) returns (output : bool)
769788
{
770789
if |resp| == 0 {
771790
return false;
772791
} else if HashName in resp[0] && resp[0][HashName] == number {
773-
expect resp[0] == record.item;
792+
expect resp[0] == NormalizeItem(record.item);
774793
return true;
775794
} else {
776795
output := ItemExists(number, record, resp[1..]);
@@ -781,7 +800,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
781800
if |resp| == 0 {
782801
return false;
783802
} else if resp[0].Item.Some? && HashName in resp[0].Item.value && resp[0].Item.value[HashName] == number {
784-
expect resp[0].Item.value == record.item;
803+
expect resp[0].Item.value == NormalizeItem(record.item);
785804
return true;
786805
} else {
787806
output := ItemExists2(number, record, resp[1..]);

Diff for: ‎TestVectors/runtimes/java/configs.json

+14-5
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@
1313
"One": "DO_NOTHING",
1414
"Seven": "DO_NOTHING",
1515
"Eight": "DO_NOTHING",
16-
"Nine": "DO_NOTHING"
16+
"Nine": "DO_NOTHING",
17+
"NumberTest" : "ENCRYPT_AND_SIGN"
1718
},
1819
"allowedUnsignedAttributes": [
1920
"One",
@@ -36,6 +37,10 @@
3637
{
3738
"Name": "Three",
3839
"Length": 32
40+
},
41+
{
42+
"Name": "NumberTest",
43+
"Length": 32
3944
}
4045
]
4146
}
@@ -54,7 +59,8 @@
5459
"One": "DO_NOTHING",
5560
"Seven": "DO_NOTHING",
5661
"Eight": "DO_NOTHING",
57-
"Nine": "DO_NOTHING"
62+
"Nine": "DO_NOTHING",
63+
"NumberTest" : "SIGN_ONLY"
5864
},
5965
"allowedUnsignedAttributes": [
6066
"One",
@@ -99,7 +105,8 @@
99105
"One": "DO_NOTHING",
100106
"Seven": "DO_NOTHING",
101107
"Eight": "DO_NOTHING",
102-
"Nine": "DO_NOTHING"
108+
"Nine": "DO_NOTHING",
109+
"NumberTest" : "SIGN_ONLY"
103110
},
104111
"allowedUnsignedAttributes": [
105112
"One",
@@ -120,7 +127,8 @@
120127
"One": "DO_NOTHING",
121128
"Seven": "DO_NOTHING",
122129
"Eight": "DO_NOTHING",
123-
"Nine": "DO_NOTHING"
130+
"Nine": "DO_NOTHING",
131+
"NumberTest" : "SIGN_ONLY"
124132
},
125133
"allowedUnsignedAttributes": [
126134
"One",
@@ -141,7 +149,8 @@
141149
"One": "DO_NOTHING",
142150
"Seven": "DO_NOTHING",
143151
"Eight": "DO_NOTHING",
144-
"Nine": "DO_NOTHING"
152+
"Nine": "DO_NOTHING",
153+
"NumberTest" : "SIGN_ONLY"
145154
},
146155
"allowedUnsignedAttributes": [
147156
"One",

Diff for: ‎TestVectors/runtimes/java/data.json

+4
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
":six": "Seis",
3232
":seven": "Siete",
3333
":eight": "Ocho",
34+
":NumberTest" : {"N" : "0800.000e0"},
3435
":nine": "Nueve",
3536
":cmp1a": "F_Cuatro.S_Junk",
3637
":cmp1b": "F_444.S_Junk",
@@ -96,6 +97,9 @@
9697
{
9798
"Filter": "Nine between :nine and :nine"
9899
},
100+
{
101+
"Filter": "NumberTest = :NumberTest"
102+
},
99103
{
100104
"Filter": "RecNum in (:zero, :one)"
101105
},

Diff for: ‎TestVectors/runtimes/java/records.json

+2-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@
1313
"Six": "666",
1414
"Seven": "777",
1515
"Eight": "888",
16-
"Nine": "999"
16+
"Nine": "999",
17+
"NumberTest" : {"N" : "0800.000e0"}
1718
},
1819
{
1920
"RecNum": {

0 commit comments

Comments
 (0)