Removing debugging tests

leanprover · Dec 2, 2024 · 2976e95 · 2976e95
1 parent 42ae5e1
commit 2976e95
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean
@@ -145,8 +145,6 @@ example : reverse irrepoly = refpoly := by native_decide
 def gcm_init_H (H : BitVec 128) : BitVec 128 :=
   pmod (H ++ 0b0#1) refpoly (by omega)
 
-#eval gcm_init_H 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128
-
 def gcm_polyval_red (x : BitVec 256) : BitVec 128 :=
   reverse $ pmod (reverse x) irrepoly (by omega)
 
@@ -162,8 +160,6 @@ def gcm_polyval_red (x : BitVec 256) : BitVec 128 :=
 def gcm_polyval (x : BitVec 128) (y : BitVec 128) : BitVec 128 :=
   GCMV8.gcm_polyval_red $ GCMV8.gcm_polyval_mul x y
 
-#eval gcm_polyval 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128
-
 /-- GCMInitV8 specification:
     H : [128] -- initial H input
     output : [12][128] -- precomputed Htable values