chore: make EncodeAscii ghost

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)
     }
 

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

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
   }

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))
   }
 

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;
   }
 

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 := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
-  const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
+
+  const BRANCH_KEY_ID_UTF8 : UTF8.ValidUTF8Bytes :=
+    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"
 
   // 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()
   {

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 aws_kms : 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 := aws_kms ,
+                               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)

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) :