m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

@@ -27,15 +27,23 @@ module TestBaseBeacon {
     var primitives :- expect Primitives.AtomicPrimitives();
 
     var bb := BeaconBase(client := primitives, name := "foo", beaconName := "aws_dbe_b_foo");
-    var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None, 1);
+    var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None, 5);
+
     var bytes :- expect bb.getHmac([1,2,3], key := [1,2]);
     expect bytes == [0x27, 0x93, 0x93, 0x8b, 0x26, 0xe9, 0x52, 0x7e];
     var str :- expect b.hash([1,2,3], key := [1,2], bucket := 0);
     expect str == "7e";
+
+    bytes :- expect bb.getHmac([1,2,3,1], key := [1,2]);
+    expect bytes == [42, 100, 242, 20, 188, 0, 33, 0x1d];
     str :- expect b.hash([1,2,3], key := [1,2], bucket := 1);
     expect str == "1d";
+
+    bytes :- expect bb.getHmac([1,2,3,2], key := [1,2]);
+    expect bytes == [53, 151, 144, 34, 49, 19, 169, 0xef];
     str :- expect b.hash([1,2,3], key := [1,2], bucket := 2);
     expect str == "ef";
+
     bytes :- expect bb.getHmac([], key := [1,2]);
     expect bytes[7] == 0x80;
     str :- expect b.hash([], key := [1,2], bucket := 0);