From 2976e95ca0e05da4a72dbf9fe99cc853fb6353ff Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Mon, 2 Dec 2024 18:57:34 +0000
Subject: [PATCH] Removing debugging tests

---
 Specs/GCMV8.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean
index 3e258594..a491f1ff 100644
--- 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