m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -652,12 +652,12 @@ module DynamoToStruct {
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
     //# 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 attrNames := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
+    var attrNames : seq<AttributeName> := SortedSets.ComputeSetToOrderedSequence2(m.Keys, CharLess);
     SequenceIsSafeBecauseItIsInMemory(attrNames);
     var len := |attrNames| as uint64;
     var output :- U32ToBigEndian64(len);
     for i : uint64 := 0 to len {
-      var k := attrNames[i];
+      var k : AttributeName := attrNames[i];
       var val := AttrToBytes(m[k], true, depth+1);
       if val.Failure? {
         var result := Failure(val.error);

DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

@@ -1264,7 +1264,7 @@ module DynamoDBFilterExpr {
   }
 
   // call the function
-  method apply_function(input : Token, stack : seq<StackValue>, num_args : nat) returns (ret : Result<StackValue, Error>)
+  method apply_function(input : Token, stack : seq<StackValue>, num_args : nat) returns (result : Result<StackValue, Error>)
   {
     match input {
       case Between =>
@@ -1274,7 +1274,7 @@ module DynamoDBFilterExpr {
           var ret :- is_between(stack[|stack|-3].s, stack[|stack|-2].s, stack[|stack|-1].s);
           return Success(Bool(ret));
         } else {
-          return Failure(E("Wrong Types for contains"));
+          return Failure(E("Wrong Types for Between"));
         }
 
       case In =>