chore(dafny): allow FileIO to deal in uint8, rather than bv8 (#770)

Author: ajewellamz

TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy

@@ -248,8 +248,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
             ==>
               SupportedEncryptVersion?(manifestData.value.version)
   {
-    var decryptManifestBv :- FileIO.ReadBytesFromFile(manifestPath + manifestFileName);
-    var decryptManifestBytes := BvToBytes(decryptManifestBv);
+    var decryptManifestBytes :- FileIO.ReadBytesFromFile(manifestPath + manifestFileName);
     var manifestJson :- API.Deserialize(decryptManifestBytes)
     .MapFailure(( e: Errors.DeserializationError ) => e.ToString());
     :- Need(manifestJson.Object?, "Not a JSON object");

TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy

@@ -542,14 +542,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
   method ReadVectorsFile(location: string)
     returns (output: Result<seq<uint8>, string>)
   {
-    var fileBv :- FileIO.ReadBytesFromFile(location);
-    output := Success(BvToBytes(fileBv));
+    output := FileIO.ReadBytesFromFile(location);
   }
 
   method WriteVectorsFile(location: string, bytes: seq<uint8>)
     returns (output: Result<(), string>)
   {
-    var bv := BytesBv(bytes);
-    output := FileIO.WriteBytesToFile(location, bv);
+    output := FileIO.WriteBytesToFile(location, bytes);
   }
 }

TestVectors/dafny/TestVectors/src/WriteVectors.dfy

@@ -108,11 +108,10 @@ module {:options "-functionSyntax:4"} WriteVectors {
     );
 
     var esdkEncryptManifestBytes :- expect API.Serialize(esdkEncryptManifests);
-    var esdkEncryptManifestBv := JSONHelpers.BytesBv(esdkEncryptManifestBytes);
 
     var _ :- expect FileIO.WriteBytesToFile(
       op.encryptManifestOutput + "encrypt-manifest.json",
-      esdkEncryptManifestBv
+      esdkEncryptManifestBytes
     );
 
     output := Success(());
@@ -155,11 +154,10 @@ module {:options "-functionSyntax:4"} WriteVectors {
     );
 
     var esdkDecryptManifestBytes :- expect API.Serialize(esdkDecryptManifest);
-    var esdkDecryptManifestBv := JSONHelpers.BytesBv(esdkDecryptManifestBytes);
 
     var _ :- expect FileIO.WriteBytesToFile(
       op.decryptManifestOutput + "manifest.json",
-      esdkDecryptManifestBv
+      esdkDecryptManifestBytes
     );
 
     output := Success(());