chore(dafny): change nat to uint64 in many places (#1852)

* chore(dafny): change nat to uint64 in many places

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -23,6 +23,7 @@ module SearchConfigToInfo {
   import opened DynamoDbEncryptionUtil
   import opened TermLoc
   import opened StandardLibrary.String
+  import opened MemoryMath
   import MaterialProviders
   import SortedSets
 
@@ -757,15 +758,15 @@ module SearchConfigToInfo {
   function method MakeDefaultConstructor(
     parts : seq<CB.BeaconPart>,
     ghost allParts : seq<CB.BeaconPart>,
-    ghost numNon : nat,
+    ghost numNon : uint64,
     converted : seq<CB.ConstructorPart> := []
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts| + |converted|
     requires |allParts| == |parts| + |converted|
     requires parts == allParts[|converted|..]
-    requires numNon <= |allParts|
-    requires CB.OrderedParts(allParts, numNon)
+    requires numNon as nat <= |allParts|
+    requires CB.OrderedParts(allParts, numNon as nat)
     requires forall i | 0 <= i < |converted| ::
                && converted[i].part == allParts[i]
                && converted[i].required
@@ -776,7 +777,7 @@ module SearchConfigToInfo {
                  //= type=implication
                  //# * This default constructor MUST be all of the signed parts,
                  //# followed by all the encrypted parts, all parts being required.
-              && CB.OrderedParts(allParts, numNon)
+              && CB.OrderedParts(allParts, numNon as nat)
               && (forall i | 0 <= i < |ret.value[0].parts| ::
                     && ret.value[0].parts[i].part == allParts[i]
                     && ret.value[0].parts[i].required)
@@ -887,13 +888,13 @@ module SearchConfigToInfo {
     constructors : Option<ConstructorList>,
     name : string,
     parts : seq<CB.BeaconPart>,
-    ghost numSigned : nat
+    ghost numSigned : uint64
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts|
     requires constructors.Some? ==> 0 < |constructors.value|
-    requires numSigned <= |parts|
-    requires CB.OrderedParts(parts, numSigned)
+    requires numSigned as nat <= |parts|
+    requires CB.OrderedParts(parts, numSigned as nat)
     ensures ret.Success? ==>
               && (constructors.None? ==> |ret.value| == 1)
               && (constructors.Some? ==> |ret.value| == |constructors.value|)
@@ -1065,10 +1066,11 @@ module SearchConfigToInfo {
     :- Need(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0,
             E("Compound beacon " + beacon.name + " defines no constructors, and also no local parts. Cannot make a default constructor from global parts."));
 
-    var numNon := |signed|;
-    assert CB.OrderedParts(signed, numNon);
+    SequenceIsSafeBecauseItIsInMemory(signed);
+    var numNon := |signed| as uint64;
+    assert CB.OrderedParts(signed, numNon as nat);
     var allParts := signed + encrypted;
-    assert CB.OrderedParts(allParts, numNon);
+    assert CB.OrderedParts(allParts, numNon as nat);
 
     var isSignedBeacon := |encrypted| == 0;
     var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon);
@@ -1087,7 +1089,7 @@ module SearchConfigToInfo {
       ),
       beacon.split[0],
       allParts,
-      numNon,
+      numNon as nat,
       constructors
     )
   }