chore: let fileio deal in uint8 instead of bv8 (#1347)

Author: ajewellamz

TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy

@@ -27,8 +27,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     ensures res.Success? ==>
               res.value is KeyVectorsClient
   {
-    var keysManifestBv :- expect FileIO.ReadBytesFromFile(config.keyManifestPath);
-    var keysManifestBytes := BvToBytes(keysManifestBv);
+    var keysManifestBytes :- expect FileIO.ReadBytesFromFile(config.keyManifestPath);
     var keysManifestJSON :- API.Deserialize(keysManifestBytes)
     .MapFailure((e: Errors.DeserializationError)  => KeyVectorException(
                     message := e.ToString()

TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/CompleteVectors.dfy

@@ -161,8 +161,7 @@ module {:options "-functionSyntax:4"} CompleteVectors {
   method WriteVectorsFile(location: string, bytes: seq<uint8>)
     returns (output: Result<(), string>)
   {
-    var bv := JSONHelpers.BytesBv(bytes);
-    output := FileIO.WriteBytesToFile(location, bv);
+    output := FileIO.WriteBytesToFile(location, bytes);
   }
 
 }

TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/JSONHelpers.dfy

@@ -11,16 +11,6 @@ module {:options "-functionSyntax:4"} JSONHelpers {
   import UTF8
   import Types = AwsCryptographyMaterialProvidersTypes
 
-  function BvToBytes(bits: seq<bv8>): seq<BoundedInts.uint8>
-  {
-    seq(|bits|, i requires 0 <= i < |bits| => bits[i] as BoundedInts.byte)
-  }
-
-  function BytesBv(bits: seq<BoundedInts.uint8>): seq<bv8>
-  {
-    seq(|bits|, i requires 0 <= i < |bits| => bits[i] as bv8)
-  }
-
   function Get(key: string, obj: seq<(string, JSON)>)
     : (output: Result<Values.JSON, string>)
   {

TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy

@@ -212,8 +212,7 @@ module {:options "-functionSyntax:4"} TestManifests {
               && fresh(manifestData.value.keys.Modifies)
               && manifestData.value.keys.ValidState()
   {
-    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");