chore: Verify by file (#62)

The Dafny process does not
parallelize very well.

The vcsCores option controls
the number of Z3 processes,
not the number of processes handling parsing.

As such the MPL spends a long time
chewing processing files.
Breaking this up is less efficient,
but may be faster.

.github/workflows/library_dafny_verification.yml

@@ -13,14 +13,14 @@ jobs:
     strategy:
       matrix:
         library: [
+          TestVectorsAwsCryptographicMaterialProviders,
           AwsCryptographyPrimitives,
           ComAmazonawsKms,
           ComAmazonawsDynamodb,
           AwsCryptographicMaterialProviders, 
-          TestVectorsAwsCryptographicMaterialProviders,
           StandardLibrary,
         ]
-        os: [ macos-latest ]
+        os: [ macos-latest-large ]
     runs-on: ${{ matrix.os }}
     env:
       DOTNET_CLI_TELEMETRY_OPTOUT: 1
@@ -40,6 +40,13 @@ jobs:
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      # dafny-reportgenerator requires next6
+      # but only 7.0 is installed on macos-latest-large
+      - name: Setup .NET Core SDK '6.0.x'
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: '6.0.x'
+
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash
         working-directory: ./${{ matrix.library }}
@@ -49,6 +56,7 @@ jobs:
           make verify CORES=$CORES
 
       - name: Check solver resource use
+        if: success() || failure()
         shell: bash
         working-directory: ./${{ matrix.library }}
         run: |

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy

@@ -514,6 +514,7 @@ module AwsKmsMrkKeyring {
                                                                     message := "No Configured KMS Key was able to decrypt the Data Key. The list of encountered Exceptions is available via `list`."));
 
       assert decryptClosure.Ensures(Last(attempts).input, Success(SealedDecryptionMaterials), DropLast(attempts));
+      assert Last(attempts).input in input.encryptedDataKeys;
 
       return Success(Types.OnDecryptOutput(
                        materials := SealedDecryptionMaterials

SharedMakefileV2.mk

@@ -63,10 +63,24 @@ COMPILE_SUFFIX_OPTION := -compileSuffix:1
 
 ########################## Dafny targets
 
+# Proof of correctness for the math below
+#  function Z3_PROCESSES(cpus:nat): nat
+#  { if cpus >= 3 then 2 else 1 }
+
+#  function DAFNY_PROCESSES(cpus: nat): nat
+#   requires 0 < cpus // 0 cpus would do no work!
+#  { (cpus - 1 )/Z3_PROCESSES(cpus) }
+
+#  lemma Correct(cpus:nat)
+#    ensures DAFNY_PROCESSES(cpus) * Z3_PROCESSES(cpus) <= cpus
+#  {}
+
 # Verify the entire project
+verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
+verify:DAFNY_PROCESSES=$(shell echo $$(( ($(CORES) - 1 ) / ($(CORES) >= 3 ? 2 : 1))))
 verify:
-	dafny \
-		-vcsCores:$(CORES) \
+	find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny \
+		-vcsCores:$(Z3_PROCESSES) \
 		-compile:0 \
 		-definiteAssignment:3 \
 		-quantifierSyntax:3 \
@@ -75,13 +89,12 @@ verify:
 		-verificationLogger:csv \
 		-timeLimit:100 \
 		-trace \
-		`find . -name *.dfy`
+		%
 
 # Verify single file FILE with text logger.
 # This is useful for debugging resource count usage within a file.
 # Use PROC to further scope the verification
 verify_single:
-	@: $(if ${CORES},,CORES=2);
 	dafny \
 		-vcsCores:$(CORES) \
 		-compile:0 \

StandardLibrary/src/Base64.dfy

@@ -378,6 +378,7 @@ module Base64 {
       if s == [] {
       } else if Is1Padding(suffix) {
         assert !Is2Padding(suffix);
+        assert |prefix| % 4 == 0;
         var x, y := DecodeUnpadded(prefix), Decode1Padding(suffix);
         assert b == x + y;
         assert |x| == |x| / 3 * 3 && |y| == 2;

StandardLibrary/src/Base64Lemmas.dfy

@@ -58,9 +58,12 @@ module Base64Lemmas {
       Encode(DecodeValid(s));
     ==
       assert |DecodeValid(s)| % 3 == 2;
+      assert 2 <= |DecodeValid(s)|;
       EncodeUnpadded(DecodeValid(s)[..(|DecodeValid(s)| - 2)]) + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
     == { DecodeValidUnpaddedPartialFrom1PaddedSeq(s); }
-      assert IsUnpaddedBase64String(s[..(|s| - 4)]);
+      assert IsUnpaddedBase64String(s[..(|s| - 4)]) by {
+        assert |s| % 4 == 0;
+      }
       EncodeUnpadded(DecodeUnpadded(s[..(|s| - 4)])) + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
     == { DecodeEncodeUnpadded(s[..(|s| - 4)]); }
       s[..(|s| - 4)] + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);