Changes addressing review from Hanno Becker

Specs/AES.lean → 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

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

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

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
-