From 66ad1dd02457dc874773f730a7ce26953e466c78 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Sat, 22 Mar 2025 09:23:00 -0400 Subject: [PATCH 1/2] chore(dafny): let FileIO deal in uint8 rather than bv8 --- TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy | 3 +-- TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy | 6 ++---- TestVectors/dafny/DDBEncryption/src/Index.dfy | 5 ++--- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 3 +-- TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy | 3 +-- .../dafny/DDBEncryption/src/WriteSetPermutations.dfy | 8 +------- submodules/MaterialProviders | 2 +- 7 files changed, 9 insertions(+), 21 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy index 5ee680b4e..f68489003 100644 --- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy +++ b/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); diff --git a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy index a25c80724..20c71636d 100644 --- a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy +++ b/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"; diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 77e49e3db..3c5801725 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -26,12 +26,11 @@ 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); output := ParseTestVector(json, prev, keyVectors); if output.Failure? { diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 6cb4a0195..657253054 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/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?; } diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 325fc0412..1e668a2de 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/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); } diff --git a/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy b/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy index 1c8b18ffb..3bf7c287b 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy @@ -117,11 +117,6 @@ module {:options "-functionSyntax:4"} WriteSetPermutations { return recs1 + recs2 + recs3 + recs4; } - function BytesBv(bits: seq): seq - { - 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 ); } } diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index aa2bed1f0..80e28f3f7 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit aa2bed1f0f9fbc48503870fe1b500a6aac59b130 +Subproject commit 80e28f3f7816e99ed22120cca6a81628a3ae4892 From 4a59b7336796f02b3400673c55b9731ad18f8cc6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Sat, 22 Mar 2025 09:44:08 -0400 Subject: [PATCH 2/2] m --- TestVectors/dafny/DDBEncryption/src/Index.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 3c5801725..03fa4492a 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -31,7 +31,7 @@ module WrappedDDBEncryptionMain { print "Failed to open ", file, " continuing anyway.\n"; return Success(MakeEmptyTestVector()); } - 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";