diff --git a/Specs/AES.lean b/Specs/AESArm.lean
similarity index 88%
rename from Specs/AES.lean
rename to Specs/AESArm.lean
index a97c6604..fc8e1633 100644
--- a/Specs/AES.lean
+++ b/Specs/AESArm.lean
@@ -37,7 +37,7 @@ import Tactics.Enum_bv
 --
 --------------------------------------------------
 
-namespace AES
+namespace AESArm
 
 open BitVec
 
@@ -118,7 +118,7 @@ protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len)
     let wd := h₁ ▸ extractLsb (i * 32 + 32 - 1) (i * 32) key
     let (x:KeySchedule) := [wd]
     have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega
-    AES.InitKey (Param := Param) (i + 1) key (acc ++ x)
+    AESArm.InitKey (Param := Param) (i + 1) key (acc ++ x)
   termination_by (Param.Nk - i)
 
 protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule)
@@ -137,13 +137,13 @@ protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule)
     let res := (List.get! ks (i - Param.Nk)) ^^^ tmp
     let ks := List.append ks [ res ]
     have _ : 4 * Param.Nr + 4 - (i + 1) < 4 * Param.Nr + 4 - i := by omega
-    AES.KeyExpansion_helper (Param := Param) (i + 1) ks
+    AESArm.KeyExpansion_helper (Param := Param) (i + 1) ks
   termination_by (4 * Param.Nr + 4 - i)
 
 def KeyExpansion {Param : KBR} (key : BitVec Param.key_len)
   : KeySchedule :=
-  let seeded := AES.InitKey (Param := Param) 0 key []
-  AES.KeyExpansion_helper (Param := Param) Param.Nk seeded
+  let seeded := AESArm.InitKey (Param := Param) 0 key []
+  AESArm.KeyExpansion_helper (Param := Param) Param.Nk seeded
 
 def SubBytes {Param : KBR} (state : BitVec Param.block_size)
   : BitVec Param.block_size :=
@@ -166,28 +166,28 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size)
   let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x
   h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03
 
-set_option maxRecDepth 3000 in
-set_option maxHeartbeats 300000 in
-set_option profiler true in
+-- set_option maxRecDepth 3000 in
+-- set_option maxHeartbeats 300000 in
+-- set_option profiler true in
 protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by
   funext x
-  enum_bv 8 x
-  -- sorry
+  -- enum_bv 8 x
+  sorry
 
-set_option maxRecDepth 3000 in
-set_option maxHeartbeats 300000 in
-set_option profiler true in
+-- set_option maxRecDepth 3000 in
+-- set_option maxHeartbeats 300000 in
+-- set_option profiler true in
 protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by
   funext x
-  enum_bv 8 x
-  -- sorry
+  -- enum_bv 8 x
+  sorry
 
 theorem MixColumns_table_lookup_equiv {Param : KBR}
   (state : BitVec Param.block_size):
   have h : Param.block_size = 128 := by simp only [Param.h, BlockSize]
   MixColumns (Param := Param) state = h ▸ DPSFP.AESMixColumns (h ▸ state) := by
     simp only [MixColumns, DPSFP.AESMixColumns]
-    rw [AES.FFmul02_equiv, AES.FFmul03_equiv]
+    rw [AESArm.FFmul02_equiv, AESArm.FFmul03_equiv]
 
 def AddRoundKey {Param : KBR} (state : BitVec Param.block_size)
   (roundKey : BitVec Param.block_size) : BitVec Param.block_size :=
@@ -209,23 +209,23 @@ protected def AES_encrypt_with_ks_loop {Param : KBR} (round : Nat)
     let state := SubBytes state
     let state := ShiftRows state
     let state := MixColumns state
-    let state := AddRoundKey state $ AES.getKey round w
-    AES.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w
+    let state := AddRoundKey state $ AESArm.getKey round w
+    AESArm.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w
   termination_by (Param.Nr - round)
 
 def AES_encrypt_with_ks {Param : KBR} (input : BitVec Param.block_size)
   (w : KeySchedule) : BitVec Param.block_size :=
   have h₀ : WordSize + WordSize + WordSize + WordSize = Param.block_size := by
     simp only [WordSize, BlockSize, Param.h]
-  let state := AddRoundKey input $ (h₀ ▸ AES.getKey 0 w)
-  let state := AES.AES_encrypt_with_ks_loop (Param := Param) 1 state w
+  let state := AddRoundKey input $ (h₀ ▸ AESArm.getKey 0 w)
+  let state := AESArm.AES_encrypt_with_ks_loop (Param := Param) 1 state w
   let state := SubBytes (Param := Param) state
   let state := ShiftRows (Param := Param) state
-  AddRoundKey state $ h₀ ▸ AES.getKey Param.Nr w
+  AddRoundKey state $ h₀ ▸ AESArm.getKey Param.Nr w
 
 def AES_encrypt {Param : KBR} (input : BitVec Param.block_size)
   (key : BitVec Param.key_len) : BitVec Param.block_size :=
   let ks := KeyExpansion (Param := Param) key
   AES_encrypt_with_ks (Param := Param) input ks
 
-end AES
+end AESArm
diff --git a/Specs/GCM.lean b/Specs/GCM.lean
index 5248624d..620845d4 100644
--- a/Specs/GCM.lean
+++ b/Specs/GCM.lean
@@ -12,6 +12,9 @@ namespace GCM
 
 open BitVec
 
+/-- NIST Special Publication 800-38D, page 11-12.
+    This constant represents, up to x^127, the polynomial for defining GF(2^128)
+    -/
 def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120
 
 /-- A Cipher type is a function that takes an input of size n and
@@ -51,14 +54,12 @@ def GHASH_aux (i : Nat) (H : BitVec 128) (X : BitVec n) (Y : BitVec 128)
   if n / 128 ≤ i then
     Y
   else
-    let lo := i * 128
+    let lo := (n/128 - 1 - i) * 128
     let hi := lo + 127
     have h₀ : hi - lo + 1 = 128 := by omega
     let Xi := extractLsb hi lo X
-    let res := rev_elems 128 8 (Y ^^^ (h₀ ▸ Xi)) (by decide) (by decide)
-    let H_rev := rev_elems 128 8 H (by decide) (by decide)
-    let Y := mul res H_rev
-    let Y := rev_elems 128 8 Y (by decide) (by decide)
+    let res := Y ^^^ (h₀ ▸ Xi)
+    let Y := mul res H
     GHASH_aux (i + 1) H X Y h
   termination_by (n / 128 - i)
 
@@ -72,15 +73,11 @@ def GCTR_aux (CIPH : Cipher (n := 128) (m := m))
   if n ≤ i then
     Y
   else
-    let lo := i * 128
+    let lo := (n - i - 1) * 128
     let hi := lo + 127
     have h : hi - lo + 1 = 128 := by omega
-    -- extractLsb will fill upper bits with zeros if hi >= len X
     let Xi := extractLsb hi lo X
-    -- reversing counter because AES expects little-endian
-    let ICB_rev := rev_elems 128 8 ICB (by decide) (by decide)
-    let Yi := h ▸ Xi ^^^ CIPH ICB_rev K
-    -- partInstall ignores val indexes that exceeds length of Y
+    let Yi := h ▸ Xi ^^^ CIPH ICB K
     let Y := BitVec.partInstall hi lo (h.symm ▸ Yi) Y
     let ICB := inc_s 32 ICB (by omega) (by omega)
     GCTR_aux CIPH (i + 1) n K ICB X Y
@@ -90,15 +87,23 @@ protected def ceiling_in_blocks (w : Nat) := (w - 1) / 128 + 1
 protected def ceiling_in_bits (w : Nat) := (GCM.ceiling_in_blocks w) * 128
 
 protected theorem bits_le_ceiling_in_bits (w : Nat) :
-  w ≤ (GCM.ceiling_in_blocks w) * 128 := by
-  simp only [GCM.ceiling_in_blocks]
+  w ≤ (GCM.ceiling_in_bits w) := by
+  simp only [GCM.ceiling_in_bits, GCM.ceiling_in_blocks]
   omega
 
 /-- GCTR: encrypting/decrypting message x using Galois counter mode -/
 def GCTR (CIPH : Cipher (n := 128) (m := m))
   (K : BitVec m) (ICB : BitVec 128) (X : BitVec v) : (BitVec v) :=
   let n := GCM.ceiling_in_blocks v
-  GCTR_aux CIPH 0 n K ICB X $ BitVec.zero v
+  let b := GCM.ceiling_in_bits v
+  let s := b - v
+  let h : v + s = b := by
+    simp only [s]
+    apply Nat.add_sub_cancel'
+          (by simp only [b]; apply GCM.bits_le_ceiling_in_bits)
+  let X' : BitVec b := h ▸ (shiftLeftZeroExtend X s)
+  let R := GCTR_aux CIPH 0 n K ICB X' $ BitVec.zero b
+  truncate v $ R >>> s
 
 protected theorem initialize_J0_simplification
   (lv : Nat) (x : Nat) (h : lv ≤ x * 128):
@@ -116,22 +121,15 @@ protected def initialize_J0 (H : BitVec 128) (IV : BitVec lv) :=
          rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
              (by apply GCM.bits_le_ceiling_in_bits)]
          omega
-       have h₃ : 8 ∣ (lv + (s + 64) + 64) := by
-         simp only [s, GCM.ceiling_in_bits]
-         rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
-             (by apply GCM.bits_le_ceiling_in_bits)]
-         omega
-       let block := rev_elems (lv + (s + 64 ) + 64) 8
-                      (IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv))
-                      h₃ (by decide)
-       rev_elems 128 8 (GHASH H block h₂) (by decide) (by decide)
+       let block := IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv)
+       GHASH H block h₂
 
 protected theorem GCM_AE_DE_simplification1 (a : Nat) (v : Nat) (p : Nat) (u : Nat) :
-  64 + 64 + u + p + v + a = 128 + (u + p) + (v + a) := by omega
+  a + v + p + u + 64 + 64 = 128 + (u + p) + (v + a) := by omega
 
 protected theorem GCM_AE_DE_simplification2
-  (y : Nat) (x : Nat) (h : y ≤ x * 128):
-  (x * 128 - y) + y = x * 128 := by omega
+  (y : Nat) (x : Nat) (h : y ≤ x):
+  (x - y) + y = x := by omega
 
 /-- GCM_AE : Galois Counter Mode Authenticated Encryption -/
 def GCM_AE (CIPH : Cipher (n := 128) (m := m))
@@ -143,17 +141,16 @@ def GCM_AE (CIPH : Cipher (n := 128) (m := m))
   let C := GCTR (m := m) CIPH K ICB P
   let u := GCM.ceiling_in_bits p - p
   let v := GCM.ceiling_in_bits a - a
-  let block := rev_elems 64 8 (BitVec.ofNat 64 p) (by decide) (by decide)
-               ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide)
-               ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A
-  have h : 128 ∣ 64 + 64 + u + p + v + a := by
+  let block := A ++ BitVec.zero v ++ C ++ BitVec.zero u
+               ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 p)
+  have h : 128 ∣ a + v + p + u + 64 + 64 := by
     rw [GCM.GCM_AE_DE_simplification1]
     simp only [u, v]
-    simp only [GCM.ceiling_in_bits]
-    rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_blocks p)
+    rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_bits p)
         (by apply GCM.bits_le_ceiling_in_bits)]
-    rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a)
+    rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a)
         (by apply GCM.bits_le_ceiling_in_bits)]
+    simp only [GCM.ceiling_in_bits]
     omega
   let S := GHASH H block h
   let T := truncate t $ GCTR (m := m) CIPH K J0 S
@@ -179,17 +176,16 @@ def GCM_AD (CIPH : Cipher (n := 128) (m := m))
     let P := GCTR (m := m) CIPH K ICB C
     let u := GCM.ceiling_in_bits c - c
     let v := GCM.ceiling_in_bits a - a
-    let block := rev_elems 64 8 (BitVec.ofNat 64 c) (by decide) (by decide)
-                 ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide)
-                 ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A
-    have h : 128 ∣ 64 + 64 + u + c + v + a := by
+    let block := A ++ BitVec.zero v ++ C ++ BitVec.zero u
+                 ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 c)
+    have h : 128 ∣ a + v + c + u + 64 + 64 := by
       rw [GCM.GCM_AE_DE_simplification1]
       simp only [u, v]
-      simp only [GCM.ceiling_in_bits]
-      rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_blocks c)
+      rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_bits c)
           (by apply GCM.bits_le_ceiling_in_bits)]
-      rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a)
+      rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a)
           (by apply GCM.bits_le_ceiling_in_bits)]
+      simp only [GCM.ceiling_in_bits]
       omega
     let S := GHASH H block h
     let T' := truncate t $ GCTR (m := m) CIPH K J0 S
diff --git a/Specs/Specs.lean b/Specs/Specs.lean
index 9586f35f..57e638db 100644
--- a/Specs/Specs.lean
+++ b/Specs/Specs.lean
@@ -5,5 +5,5 @@ Author(s): Shilpi Goel
 -/
 import «Specs».SHA512
 import «Specs».AESCommon
-import «Specs».AES
+import «Specs».AESArm
 import «Specs».GCM
diff --git a/Tactics/Enum_bv.lean b/Tactics/Enum_bv.lean
index 672b3559..474e4f69 100644
--- a/Tactics/Enum_bv.lean
+++ b/Tactics/Enum_bv.lean
@@ -164,4 +164,3 @@ elab "enum_bv" n:num var:ident : tactic => do
 -- theorem example_lemma : carry_less_add = lookup_cla := by
 --   funext x
 --   enum_bv 2 x
-
diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean
index 9c9f094c..8f17f107 100644
--- a/Tests/AESGCMSpecTest.lean
+++ b/Tests/AESGCMSpecTest.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 import Arm.BitVec
-import Specs.AES
+import Specs.AESArm
 import Specs.GCM
 
 -- Reference: https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf
@@ -13,8 +13,18 @@ namespace AES256GCMSpecTest
 
 open BitVec
 
+-- Reversing bytes in inputs and output because AES uses little-endian
+def revCIPH (CIPH : BitVec n -> BitVec m -> BitVec n)
+  (h₀ : 8 ∣ n) (h₁ : 8 ∣ m) (p : BitVec n) (k : BitVec m) :=
+  (rev_elems n 8
+    (CIPH (rev_elems n 8 p h₀ (by decide)) (rev_elems m 8 k h₁ (by decide)))
+    h₀ (by decide))
+
+def CIPH_128' : GCM.Cipher (n := 128) (m := 128) :=
+  AESArm.AES_encrypt (Param := AESArm.AES128KBR)
+
 def CIPH_128 : GCM.Cipher (n := 128) (m := 128) :=
-  AES.AES_encrypt (Param := AES.AES128KBR)
+  revCIPH CIPH_128' (by decide) (by decide)
 
 def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec a
   → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_128
@@ -22,8 +32,11 @@ def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec
 def GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t
   → Option (BitVec c) := GCM.GCM_AD CIPH_128
 
+def CIPH_192' : GCM.Cipher (n := 128) (m := 192) :=
+  AESArm.AES_encrypt (Param := AESArm.AES192KBR)
+
 def CIPH_192 : GCM.Cipher (n := 128) (m := 192) :=
-AES.AES_encrypt (Param := AES.AES192KBR)
+  revCIPH CIPH_192' (by decide) (by decide)
 
 def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec a
   → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_192
@@ -31,8 +44,11 @@ def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec
 def GCM_AD_192 : BitVec 192 → BitVec lv → BitVec c → BitVec a → BitVec t
   → Option (BitVec c) := GCM.GCM_AD CIPH_192
 
+def CIPH_256' : GCM.Cipher (n := 128) (m := 256) :=
+  AESArm.AES_encrypt (Param := AESArm.AES256KBR)
+
 def CIPH_256 : GCM.Cipher (n := 128) (m := 256) :=
-  AES.AES_encrypt (Param := AES.AES256KBR)
+  revCIPH CIPH_256' (by decide) (by decide)
 
 def GCM_AE_256 : BitVec 256 → (t : Nat) → BitVec lv → BitVec p → BitVec a
   → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_256
@@ -47,7 +63,7 @@ def IV0 : BitVec 96 := 0
 def P0 : BitVec 0 := BitVec.nil
 def A0 : BitVec 0 := BitVec.nil
 def C0 : BitVec 0 := BitVec.nil
-def T0 : BitVec 128 := rev_elems 128 8 0x58e2fccefa7e3061367f1d57a4e7455a#128 (by decide) (by decide)
+def T0 : BitVec 128 := 0x58e2fccefa7e3061367f1d57a4e7455a#128
 example : GCM_AE_128 K0 128 IV0 P0 A0 = (C0, T0) := by native_decide
 example : GCM_AD_128 K0 IV0 C0 A0 T0 = P0 := by native_decide
 
@@ -57,52 +73,52 @@ def K1 : BitVec 128 := 0
 def IV1 : BitVec 96 := 0
 def P1 : BitVec 128 := 0
 def A1 : BitVec 0 := BitVec.nil
-def C1 : BitVec 128 := rev_elems 128 8 0x0388dace60b6a392f328c2b971b2fe78#128 (by decide) (by decide)
-def T1 : BitVec 128 := rev_elems 128 8 0xab6e47d42cec13bdf53a67b21257bddf#128 (by decide) (by decide)
+def C1 : BitVec 128 := 0x0388dace60b6a392f328c2b971b2fe78#128
+def T1 : BitVec 128 := 0xab6e47d42cec13bdf53a67b21257bddf#128
 example : GCM_AE_128 K1 128 IV1 P1 A1 = (C1, T1) := by native_decide
 example : GCM_AD_128 K1 IV1 C1 A1 T1 = P1 := by native_decide
 
 -- Test Vector 2
 
-def K2 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def K2 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128
 def IV2 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P2 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide)
+def P2 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
 def A2 : BitVec 0 := BitVec.nil
-def C2 : BitVec 512 := rev_elems 512 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 (by decide) (by decide)
-def T2 : BitVec 128 := rev_elems 128 8 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 (by decide) (by decide)
+def C2 : BitVec 512 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512
+def T2 : BitVec 128 := 0x4d5c2af327cd64a62cf35abd2ba6fab4#128
 example : GCM_AE_128 K2 128 IV2 P2 A2 = (C2, T2) := by native_decide
 example : GCM_AD_128 K2 IV2 C2 A2 T2 = P2 := by native_decide
 
 -- Test Vector 3
 
-def K3 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def K3 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128
 def IV3 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P3 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A3 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C3 : BitVec 480 := rev_elems 480 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480 (by decide) (by decide)
-def T3 : BitVec 128 := rev_elems 128 8 0x5bc94fbc3221a5db94fae95ae7121a47#128 (by decide) (by decide)
+def P3 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A3 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C3 : BitVec 480 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480
+def T3 : BitVec 128 := 0x5bc94fbc3221a5db94fae95ae7121a47#128
 example : GCM_AE_128 K3 128 IV3 P3 A3 = (C3, T3) := by native_decide
 example : GCM_AD_128 K3 IV3 C3 A3 T3 = P3 := by native_decide
 
 -- Test Vector 4
 
-def K4 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def K4 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128
 def IV4 : BitVec 64 := 0xcafebabefacedbad#64
-def P4 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A4 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C4 : BitVec 480 := rev_elems 480 8 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 (by decide) (by decide)
-def T4 : BitVec 128 := rev_elems 128 8 0x3612d2e79e3b0785561be14aaca2fccb#128 (by decide) (by decide)
+def P4 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A4 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C4 : BitVec 480 := 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480
+def T4 : BitVec 128 := 0x3612d2e79e3b0785561be14aaca2fccb#128
 example : GCM_AE_128 K4 128 IV4 P4 A4 = (C4, T4) := by native_decide
 example : GCM_AD_128 K4 IV4 C4 A4 T4 = P4 := by native_decide
 
 -- Test Vector 5
 
-def K5 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def K5 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128
 def IV5 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
-def P5 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A5 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C5 : BitVec 480 := rev_elems 480 8 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 (by decide) (by decide)
-def T5 : BitVec 128 := rev_elems 128 8 0x619cc5aefffe0bfa462af43c1699d050#128 (by decide) (by decide)
+def P5 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A5 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C5 : BitVec 480 := 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480
+def T5 : BitVec 128 := 0x619cc5aefffe0bfa462af43c1699d050#128
 example : GCM_AE_128 K5 128 IV5 P5 A5 = (C5, T5) := by native_decide
 example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide
 
@@ -113,7 +129,7 @@ def IV6 : BitVec 96 := 0
 def P6 : BitVec 0 := BitVec.nil
 def A6 : BitVec 0 := BitVec.nil
 def C6 : BitVec 0 := BitVec.nil
-def T6 : BitVec 128 := rev_elems 128 8 0xcd33b28ac773f74ba00ed1f312572435#128 (by decide) (by decide)
+def T6 : BitVec 128 := 0xcd33b28ac773f74ba00ed1f312572435#128
 example : GCM_AE_192 K6 128 IV6 P6 A6 = (C6, T6) := by native_decide
 example : GCM_AD_192 K6 IV6 C6 A6 T6 = P6 := by native_decide
 
@@ -123,52 +139,52 @@ def K7 : BitVec 192 := 0
 def IV7 : BitVec 96 := 0
 def P7 : BitVec 128 := 0
 def A7 : BitVec 0 := BitVec.nil
-def C7 : BitVec 128 := rev_elems 128 8 0x98e7247c07f0fe411c267e4384b0f600#128 (by decide) (by decide)
-def T7 : BitVec 128 := rev_elems 128 8 0x2ff58d80033927ab8ef4d4587514f0fb#128 (by decide) (by decide)
+def C7 : BitVec 128 := 0x98e7247c07f0fe411c267e4384b0f600#128
+def T7 : BitVec 128 := 0x2ff58d80033927ab8ef4d4587514f0fb#128
 example : GCM_AE_192 K7 128 IV7 P7 A7 = (C7, T7) := by native_decide
 example : GCM_AD_192 K7 IV7 C7 A7 T7 = P7 := by native_decide
 
 -- Test Vector 8
 
-def K8 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide)
+def K8 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
 def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P8 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide)
+def P8 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
 def A8 : BitVec 0 := BitVec.nil
-def C8 : BitVec 512 := rev_elems 512 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512 (by decide) (by decide)
-def T8 : BitVec 128 := rev_elems 128 8 0x9924a7c8587336bfb118024db8674a14#128 (by decide) (by decide)
+def C8 : BitVec 512 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512
+def T8 : BitVec 128 := 0x9924a7c8587336bfb118024db8674a14#128
 example : GCM_AE_192 K8 128 IV8 P8 A8 = (C8, T8) := by native_decide
 example : GCM_AD_192 K8 IV8 C8 A8 T8 = P8 := by native_decide
 
 -- Test Vector 9
 
-def K9 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide)
+def K9 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
 def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P9 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A9 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C9 : BitVec 480 := rev_elems 480 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480 (by decide) (by decide)
-def T9 : BitVec 128 := rev_elems 128 8 0x2519498e80f1478f37ba55bd6d27618c#128 (by decide) (by decide)
+def P9 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A9 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C9 : BitVec 480 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480
+def T9 : BitVec 128 := 0x2519498e80f1478f37ba55bd6d27618c#128
 example : GCM_AE_192 K9 128 IV9 P9 A9 = (C9, T9) := by native_decide
 example : GCM_AD_192 K9 IV9 C9 A9 T9 = P9 := by native_decide
 
 -- Test Vector 10
 
-def K10 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide)
+def K10 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
 def IV10 : BitVec 64:= 0xcafebabefacedbad#64
-def P10 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A10 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C10 : BitVec 480 := rev_elems 480 8 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480 (by decide) (by decide)
-def T10 : BitVec 128 := rev_elems 128 8 0x65dcc57fcf623a24094fcca40d3533f8#128 (by decide) (by decide)
+def P10 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A10 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C10 : BitVec 480 := 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480
+def T10 : BitVec 128 := 0x65dcc57fcf623a24094fcca40d3533f8#128
 example : GCM_AE_192 K10 128 IV10 P10 A10 = (C10, T10) := by native_decide
 example : GCM_AD_192 K10 IV10 C10 A10 T10 = P10 := by native_decide
 
 -- Test Vector 11
 
-def K11 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide)
+def K11 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
 def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
-def P11 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A11 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C11 : BitVec 480 := rev_elems 480 8 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480 (by decide) (by decide)
-def T11 : BitVec 128 := rev_elems 128 8 0xdcf566ff291c25bbb8568fc3d376a6d9#128 (by decide) (by decide)
+def P11 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A11 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C11 : BitVec 480 := 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480
+def T11 : BitVec 128 := 0xdcf566ff291c25bbb8568fc3d376a6d9#128
 example : GCM_AE_192 K11 128 IV11 P11 A11 = (C11, T11) := by native_decide
 example : GCM_AD_192 K11 IV11 C11 A11 T11 = P11 := by native_decide
 
@@ -179,7 +195,7 @@ def IV12 : BitVec 96 := 0
 def P12 : BitVec 0 := BitVec.nil
 def A12 : BitVec 0 := BitVec.nil
 def C12 : BitVec 0 := BitVec.nil
-def T12 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide)
+def T12 : BitVec 128 := 0x530f8afbc74536b9a963b4f1c4cb738b#128
 example : GCM_AE_256 K12 128 IV12 P12 A12 = (C12, T12) := by native_decide
 example : GCM_AD_256 K12 IV12 C12 A12 T12 = P12 := by native_decide
 
@@ -189,52 +205,52 @@ def K13 : BitVec 256 := 0
 def IV13 : BitVec 96 := 0
 def P13 : BitVec 128 := 0
 def A13 : BitVec 0 := BitVec.nil
-def C13 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide)
-def T13 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide)
+def C13 : BitVec 128 := 0xcea7403d4d606b6e074ec5d3baf39d18#128
+def T13 : BitVec 128 := 0xd0d1c8a799996bf0265b98b5d48ab919#128
 example : GCM_AE_256 K13 128 IV13 P13 A13 = (C13, T13) := by native_decide
 example : GCM_AD_256 K13 IV13 C13 A13 T13 = P13 := by native_decide
 
 -- Test Vector 14
 
-def K14 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def K14 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
 def IV14 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P14 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide)
+def P14 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
 def A14 : BitVec 0 := BitVec.nil
-def C14 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide)
-def T14 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide)
+def C14 : BitVec 512 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512
+def T14 : BitVec 128 := 0xb094dac5d93471bdec1a502270e3cc6c#128
 example : GCM_AE_256 K14 128 IV14 P14 A14 = (C14, T14) := by native_decide
 example : GCM_AD_256 K14 IV14 C14 A14 T14 = P14 := by native_decide
 
 -- Test Vector 15
 
-def K15 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def K15 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
 def IV15 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
-def P15 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A15 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C15 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide)
-def T15 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide)
+def P15 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A15 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C15 : BitVec 480 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480
+def T15 : BitVec 128 := 0x76fc6ece0f4e1768cddf8853bb2d551b#128
 example : GCM_AE_256 K15 128 IV15 P15 A15 = (C15, T15) := by native_decide
 example : GCM_AD_256 K15 IV15 C15 A15 T15 = P15 := by native_decide
 
 -- Test Vector 16
 
-def K16 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def K16 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
 def IV16 : BitVec 64:= 0xcafebabefacedbad#64
-def P16 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A16 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C16 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide)
-def T16 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide)
+def P16 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A16 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C16 : BitVec 480 := 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480
+def T16 : BitVec 128 := 0x3a337dbf46a792c45e454913fe2ea8f2#128
 example : GCM_AE_256 K16 128 IV16 P16 A16 = (C16, T16) := by native_decide
 example : GCM_AD_256 K16 IV16 C16 A16 T16 = P16 := by native_decide
 
 -- Test Vector 17
 
-def K17 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def K17 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
 def IV17 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
-def P17 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
-def A17 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
-def C17 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide)
-def T17 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide)
+def P17 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A17 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C17 : BitVec 480 := 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480
+def T17 : BitVec 128 := 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128
 example : GCM_AE_256 K17 128 IV17 P17 A17 = (C17, T17) := by native_decide
 example : GCM_AD_256 K17 IV17 C17 A17 T17 = P17 := by native_decide
 
diff --git a/Tests/AESSpecTest.lean b/Tests/AESSpecTest.lean
index a8e2fa64..7564955b 100644
--- a/Tests/AESSpecTest.lean
+++ b/Tests/AESSpecTest.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 
-import Specs.AES
+import Specs.AESArm
 import Arm.BitVec
 
 -- Reference : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf Section B
@@ -37,6 +37,6 @@ protected def output : BitVec 128 :=
       0xdc#8, 0x11#8, 0x85#8, 0x97#8,
       0x19#8, 0x6a#8, 0x0b#8, 0x32#8 ].reverse
 
-example : AES.AES_encrypt (Param := AES.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide
+example : AESArm.AES_encrypt (Param := AESArm.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide
 
 end AESSpecTest