cleanup

Author: ajewellamz

DynamoDbEncryption/Makefile

@@ -78,7 +78,7 @@ SERVICE_DEPS_DynamoDbEncryptionTransforms := \
 format_net:
 	pushd runtimes/net && dotnet format DynamoDbEncryption.csproj && popd
 
-# First, export DAFNY_VERSION=4.2
 polymorph:
+	export DAFNY_VERSION=4.2
 	npm i --no-save prettier@3 [email protected]
 	make polymorph_code_gen PROJECT_DEPENDENCIES=

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

@@ -641,15 +641,13 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   function method ConvertCryptoSchemaToAttributeActions(config: ValidConfig, schema: CSE.CryptoSchemaMap)
     : (ret: Result<map<ComAmazonawsDynamodbTypes.AttributeName, CSE.CryptoAction>, Error>)
     requires forall k <- schema :: SE.IsAuthAttr(schema[k])
-    // ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k)
-    // ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING?
+    ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k)
+    ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING?
   {
-    // We can formally verify these properties, but it is too resource intensive
-    // :- Need(forall k <- schema :: InSignatureScope(config, k),
-    //         DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
+    :- Need(forall k <- schema :: InSignatureScope(config, k),
+            DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
     :- Need(forall k <- schema :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k),
             DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: Invalid attribute names"));
-    // Success(map k <- schema :: k := schema[k])
     Success(schema)
   }
 

DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy

@@ -127,6 +127,8 @@ module StructuredEncryptionCrypt {
 
   datatype EncryptionSelector = DoEncrypt | DoDecrypt
 
+  // Updated return true if the given item has been updated properly for the given operation.
+  // Updated2..Update5 do exactly the same thing, but with different data types.
   predicate Updated(oldVal : CanonCryptoItem, newVal : CanonCryptoItem, mode : EncryptionSelector)
   {
     && oldVal.key == newVal.key

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -419,36 +419,28 @@ module StructuredEncryptionHeader {
     //   as well as being included in the encryption context.
     //   This indicates that this field MUST NOT be attempted to be decrypted during decryption.    // - no entry if the attribute is not signed
     ensures match (x) {
-              case ENCRYPT_AND_SIGN => ret == ENCRYPT_AND_SIGN_LEGEND
-              case SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT => ret == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND
-              case SIGN_ONLY => ret == SIGN_ONLY_LEGEND
+              case ENCRYPT_AND_SIGN() => ret == ENCRYPT_AND_SIGN_LEGEND
+              case SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT() => ret == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND
+              case SIGN_ONLY() => ret == SIGN_ONLY_LEGEND
             }
   {
     match (x) {
-      case ENCRYPT_AND_SIGN => ENCRYPT_AND_SIGN_LEGEND
-      case SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT => SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND
-      case SIGN_ONLY => SIGN_ONLY_LEGEND
+      case ENCRYPT_AND_SIGN() => ENCRYPT_AND_SIGN_LEGEND
+      case SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT() => SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND
+      case SIGN_ONLY() => SIGN_ONLY_LEGEND
     }
   }
 
   // How many elements of Schema are included in the signature?
   function method CountAuthAttrs(data : CanonCryptoList)
     : nat
   {
-    |RestrictAuthAttrs(data)|
-  }
-
-  /*
-   * Restrict `data` to just the authenticated attributes.
-   */
-  function method RestrictAuthAttrs(data: CanonCryptoList)
-    : (authData: CanonCryptoList)
-    // ensures authData.Keys <= data.Keys
-    // ensures forall k <- data :: IsAuthAttr(data[k]) <==> k in authData
-    // ensures forall k <- authData :: authData[k] == data[k]
-    // ensures forall k <- authData :: IsAuthAttr(authData[k])
-  {
-    Seq.Filter((s : CanonCryptoItem) => IsAuthAttr(s.action), data)
+    if |data| == 0 then
+      0
+    else if IsAuthAttr(data[0].action) then
+      1 + CountAuthAttrs(data[1..])
+    else
+      CountAuthAttrs(data[1..])
   }
 
   // Legend to Bytes

DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy

@@ -253,25 +253,6 @@ module StructuredEncryptionPaths {
     }
   }
 
-  // lemma SelectorNeverPrefixList(x : Selector, y : Selector)
-  //   requires x != y
-  //   requires x.List?
-  //   requires y.List?
-  //   ensures !(CanonicalPart(x) <= CanonicalPart(y))
-  //   ensures !(CanonicalPart(y) <= CanonicalPart(x))
-  // {
-  //   assert x.pos != y.pos;
-  //   var cpX := CanonicalPart(x);
-  //   var cpY := CanonicalPart(y);
-  //   assert cpX == [ARRAY_TAG] + UInt64ToSeq(x.pos as uint64);
-  //   assert cpY == [ARRAY_TAG] + UInt64ToSeq(y.pos as uint64);
-  //   assert UInt64ToSeq(x.pos as uint64) != UInt64ToSeq(y.pos as uint64);
-  //   OnePlusOne([ARRAY_TAG], UInt64ToSeq(x.pos as uint64), UInt64ToSeq(y.pos as uint64));
-  //   assert cpX != cpY;
-  //   assert !(cpY <= cpX);
-  //   assert !(cpX <= cpY);
-  // }
-
   lemma SelectorNeverPrefix(x : PathSegment, y : PathSegment)
     requires x != y
     requires ValidString(x.member.key) && ValidString(y.member.key)

DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy

@@ -40,16 +40,12 @@ module SortCanon {
     BelowIsReflexive(x.key);
   }
 
+  // not actually required for sorting. Standard library being updated.
   lemma {:axiom} AuthBelowIsAntiSymmetric(x: CanonAuthItem, y: CanonAuthItem)
     requires AuthBelow(x, y) && AuthBelow(y, x)
     ensures x == y
-  // {
-  //   assert Below(x.key, y.key);
-  //   assert Below(y.key, x.key);
-  //   BelowIsAntiSymmetric(x.key, y.key);
-  //   BelowIsAntiSymmetric(y.key, x.key);
-  // }
 
+  // not actually required for sorting. Standard library being updated.
   lemma {:axiom} CryptoBelowIsAntiSymmetric(x: CanonCryptoItem, y: CanonCryptoItem)
     requires CryptoBelow(x, y) && CryptoBelow(y, x)
     ensures x == y

DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy

@@ -105,15 +105,6 @@ module StructuredEncryptionUtil {
     && UTF8.Encode(x).Success?
   }
 
-  // type StructuredDataPlain = map<GoodPath, StructuredDataTerminal>
-  // type StructuredDataCanon = map<CanonicalPath, StructuredDataTerminal>
-  // type CryptoSchemaPlain = map<GoodPath, CSE.CryptoAction>
-  // type CryptoSchemaCanon = map<CanonicalPath, CSE.CryptoAction>
-  // type AuthSchemaPlain = map<GoodPath, AuthenticateAction>
-  // type AuthSchemaCanon = map<CanonicalPath, AuthenticateAction>
-  // type CanonMap = map<CanonicalPath, GoodPath>
-
-
   // Within the context of the StructuredEncryptionClient, certain things must be true of any Algorithm Suite
   predicate method ValidSuite(alg : CMP.AlgorithmSuiteInfo)
   {