chore(dafny): let FileIO deal in uint8 rather than bv8 (#1746)

* chore(dafny): let FileIO deal in uint8 rather than bv8

Author: ajewellamz

TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

@@ -118,8 +118,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
   {
     var timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Decrypt : ", inFile, "\n";
-    var configBv :- expect FileIO.ReadBytesFromFile(inFile);
-    var configBytes := BvToBytes(configBv);
+    var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " File Read.\n";
     var json :- expect API.Deserialize(configBytes);

TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy

@@ -151,8 +151,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   {
     var timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Encrypt : ", inFile, "\n";
-    var configBv :- expect FileIO.ReadBytesFromFile(inFile);
-    var configBytes := BvToBytes(configBv);
+    var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " File Read.\n";
     var json :- expect API.Deserialize(configBytes);
@@ -212,8 +211,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
 
     var final := Object(result + [("tests", Object(test))]);
     var jsonBytes :- expect API.Serialize(final);
-    var jsonBv := BytesBv(jsonBytes);
-    var x :- expect FileIO.WriteBytesToFile(outFile, jsonBv);
+    var x :- expect FileIO.WriteBytesToFile(outFile, jsonBytes);
 
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Tests Complete.\n";

TestVectors/dafny/DDBEncryption/src/Index.dfy

@@ -26,13 +26,12 @@ module WrappedDDBEncryptionMain {
     modifies keyVectors.Modifies
     ensures keyVectors.ValidState()
   {
-    var configBv := FileIO.ReadBytesFromFile(file);
-    if configBv.Failure? {
+    var configBytes := FileIO.ReadBytesFromFile(file);
+    if configBytes.Failure? {
       print "Failed to open ", file, " continuing anyway.\n";
       return Success(MakeEmptyTestVector());
     }
-    var configBytes := BvToBytes(configBv.value);
-    var json :- expect API.Deserialize(configBytes);
+    var json :- expect API.Deserialize(configBytes.value);
     output := ParseTestVector(json, prev, keyVectors);
     if output.Failure? {
       print output.error, "\n";

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -560,8 +560,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         jsonItems := jsonItems + [item];
       }
       var jsonBytes :- expect API.Serialize(Array(jsonItems));
-      var jsonBv := BytesBv(jsonBytes);
-      var x := FileIO.WriteBytesToFile(fileName, jsonBv);
+      var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
       expect x.Success?;
     }
 

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

@@ -401,8 +401,7 @@ module {:options "-functionSyntax:4"} WriteManifest {
     var final := Object(result + [("tests", Object(tests))]);
 
     var jsonBytes :- expect API.Serialize(final);
-    var jsonBv := BytesBv(jsonBytes);
-    var x := FileIO.WriteBytesToFile(fileName, jsonBv);
+    var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
     expect x.Success?;
     return Success(true);
   }

TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy

@@ -117,11 +117,6 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
     return recs1 + recs2 + recs3 + recs4;
   }
 
-  function BytesBv(bits: seq<BoundedInts.uint8>): seq<bv8>
-  {
-    seq(|bits|, i requires 0 <= i < |bits| => bits[i] as bv8)
-  }
-
   method WriteSetPermutations()
   {
     var configs := GetConfigs();
@@ -132,11 +127,10 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
                           ]))]);
 
     var jsonBytes :- expect API.Serialize(whole);
-    var jsonBv := BytesBv(jsonBytes);
 
     var _ :- expect FileIO.WriteBytesToFile(
       "PermTest.json",
-      jsonBv
+      jsonBytes
     );
   }
 }