chore: fix tests

joehendrix · Sep 6, 2023 · 3d24bed · 3d24bed
1 parent acdc047
commit 3d24bed
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/lib/McEliece.lean b/lib/McEliece.lean
@@ -9,7 +9,7 @@ def main (args:List String): IO Unit := do
   | [reqPath, rspPath] => do
       let mut drbg0 := randombytesInit (byteSequence 48);
       let mut seedArray : Array Seed := #[]
-      let fpReq ← IO.FS.Handle.mk reqPath IO.FS.Mode.write false
+      let fpReq ← IO.FS.Handle.mk reqPath IO.FS.Mode.write
       for i in [0:10] do
         let (seed, drbg2) := PRNG.randombytes drbg0 48
         drbg0 := drbg2
@@ -20,7 +20,7 @@ def main (args:List String): IO Unit := do
         fpReq.putStrLn "ct ="
         fpReq.putStrLn "ss =\n"
         seedArray := seedArray.push seed
-      let fpRsp ← IO.FS.Handle.mk rspPath IO.FS.Mode.write false
+      let fpRsp ← IO.FS.Handle.mk rspPath IO.FS.Mode.write
       fpRsp.putStrLn $ s!"# kem/{Mceliece.Ref348864.name}\n"
       for i in [0:10], seed in seedArray do
         let (key, drbg) ←

diff --git a/tests/aes/GF256Pow.lean b/tests/aes/GF256Pow.lean
@@ -13,15 +13,16 @@ example (x : GF256) : GF256.pow2 8 x = x := by
   conv at GF256.pow2.def =>
     intro k x
     rw [ GaloisField2k.mul.GF256.specialization ]
-  save
+  -- TODO: breaks mvar context
+  -- save
 
   extract_def polyMod
   specialize_def GF2BVPoly.polyMod [16, 8]
-  save
+  -- save
 
   extract_def polyMul
   specialize_def GF2BVPoly.polyMul [8, 8]
-  save
+  -- save
 
   conv at GaloisField2k.mul.GF256.def =>
     intro a b
@@ -34,5 +35,5 @@ example (x : GF256) : GF256.pow2 8 x = x := by
     GF2BVPoly.polyMul.«8».«8»,
     GF2BVPoly.polyMod.«16».«8»
   ] 
-    
+
   sorry