PR feedback

Author: ajewellamz

TestVectors/README.md

@@ -18,6 +18,28 @@ This validates the Database Encryption SDK's cross-version compatibility.
 1. Start in the root `./TestVectors` directory
 2. Run `make build_java`
 3. Run `make test_java`
+4. Run `make transpile_net`
+5. Run `cd runtimes/net`
+6. Run `dotnet run --framework net6.0`
+
+### Saving results for later
+
+Running the above commands will create `runtimes/java/decrypt.json` and `runtimes/net/decrypt.json`.
+
+These files should be permanently saved before a release.
+
+For example, if we're on version 3.4 and are getting close to a new release, we would
+
+`cp runtimes/java/decrypt.json runtimes/java/decrypt_java_34.json`
+
+`cp runtimes/net/decrypt.json runtimes/java/decrypt_dotnet_34.json`
+
+and then modify `RunAllTests` in `dafny/DDBEncryption/src/TestVectors.dfy` to explicitly check these two files.
+
+As other languages are supported, we will also deal with runtimes/XXX/decrypt.json and runtimes/java/decrypt_XXX_34.json
+in a simlar manner.
+
+This ensures that records written in any version in any language can be read by the current version in any language.
 
 ## Security
 

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

@@ -248,6 +248,9 @@ module {:options "-functionSyntax:4"} WriteManifest {
       [0, 0, 0, 0, 0, 0]
   }
 
+  // To be consistent :
+  // 1) The primary key (actions[0]) must be sign_only or sign_and_include
+  // 2) If anything is sign_and_include, then The primary key must be sign_and_include
   predicate IsConsistent(actions : CryptoActions)
   {
     if actions[0] in [DoNothing, Encrypt] then
@@ -258,6 +261,9 @@ module {:options "-functionSyntax:4"} WriteManifest {
       true
   }
 
+  // For a new config to be consistent with an old config:
+  // 1) both configs must be individually consistent
+  // 2) they must agree on which fields are do_nothing
   predicate IsConsistentWith(oldActions : CryptoActions, newActions : CryptoActions)
   {
     if !IsConsistent(oldActions) || !IsConsistent(newActions) then
@@ -267,6 +273,8 @@ module {:options "-functionSyntax:4"} WriteManifest {
   }
 
   // make a test for every valid combination of Crypto Actions
+  // 'actions' holds the crypto actions for each of six attributes
+  // the loop iterates through all possible combinations of attributes by incrementing this list
   method MakeConfigTests() returns (output : seq<(string, JSON)>)
   {
     var actions : CryptoActions := [0,0,0,0,0,0];
@@ -289,6 +297,9 @@ module {:options "-functionSyntax:4"} WriteManifest {
 
         // for a subset of these,
         // make a test to decrypt with every possible valid combination of Crypto Actions
+        // testing all of them would take too much time and space,
+        // so we select a sample to produce about 2000 more tests
+        // every 100th seems as good as any other method to get a representative sample
         if (actionWrittenOuter % 100) == 0 {
           var otherActions : CryptoActions := [0,0,0,0,0,0];
           // 4096 == 4 ^ 6 == size of all possible values of `otherActions`