Remove comments and small fixes

leanprover · Oct 11, 2024 · 1b5df7c · 1b5df7c
1 parent 8a0756d
commit 1b5df7c
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 36 deletions.
diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
@@ -705,10 +705,9 @@ theorem shift_right_common_aux_64_2_tff (operand : BitVec 128)
   simp only [minimal_theory, bitvec_rules]
   unfold shift_right_common_aux
   simp only [minimal_theory, bitvec_rules]
-  simp only [-- -extractLsb_toNat,
-             state_simp_rules,
+  simp only [state_simp_rules,
              minimal_theory,
-             -- FIXME: simply using bitvec_rules will expand out extractLsb and truncate
+             -- FIXME: simply using bitvec_rules will expand out setWidth
              -- bitvec_rules,
              BitVec.cast_eq,
              Nat.shiftRight_zero,
@@ -801,10 +800,9 @@ theorem shift_right_common_aux_32_4_fff (operand : BitVec 128)
   simp only [minimal_theory, bitvec_rules]
   unfold shift_right_common_aux
   simp only [minimal_theory, bitvec_rules]
-  simp only [-- -extractLsb_toNat,
-             state_simp_rules,
+  simp only [state_simp_rules,
              minimal_theory,
-             -- FIXME: simply using bitvec_rules will expand out extractLsb and truncate
+             -- FIXME: simply using bitvec_rules will expand out setWidth
              -- bitvec_rules,
              BitVec.cast_eq,
              Nat.shiftRight_zero,

diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -16,7 +16,6 @@ set_option bv.ac_nf false
 abbrev H_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s
 abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s
 
-set_option debug.byAsSorry true in
 set_option maxRecDepth 1000000 in
 -- set_option profiler true in
 theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
@@ -37,7 +36,7 @@ theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
 
 set_option maxRecDepth 100000 in
 set_option maxHeartbeats 500000 in
--- set_option sat.timeout 120 in
+set_option sat.timeout 120 in
 -- set_option pp.deepTerms true in
 -- set_option pp.maxSteps 10000 in
 set_option trace.profiler true in

diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean
@@ -51,16 +51,6 @@ def pmult (x: BitVec (m + 1)) (y : BitVec (n + 1)) : BitVec (m + n + 1) :=
 
 example: pmult 0b1101#4 0b10#2 = 0b11010#5 := rfl
 
--- /-- Degree of x. -/
--- def degree (x : BitVec n) : Nat :=
---   let rec degreeTR (x : BitVec n) (n : Nat) : Nat :=
---     match n with
---     | 0 => 0
---     | m + 1 =>
---       if getLsbD x n then n else degreeTR x m
---   degreeTR x (n - 1)
--- example: GCMV8.degree 0b0101#4 = 2 := rfl
-
 /-- Degree of x. Defined using non-ite statements. -/
 def degree (x : BitVec n) : Nat :=
   let rec degreeTR (x : BitVec n) (n : Nat) (i : Nat) (acc : Nat) : Nat :=
@@ -74,10 +64,6 @@ def degree (x : BitVec n) : Nat :=
 example: GCMV8.degree 0b0101#4 = 2 := rfl
 example: GCMV8.degree 0b1101#4 = 3 := rfl
 
--- /-- Subtract x from y if y's x-degree-th bit is 1. -/
--- def reduce (x : BitVec n) (y : BitVec n) : BitVec n :=
---   if getLsbD y (GCMV8.degree x) then y ^^^ x else y
-
 /-- Subtract x from y if y's x-degree-th bit is 1.
     Defined using non-ite statements. -/
 def reduce (x : BitVec n) (y : BitVec n) : BitVec n :=
@@ -103,20 +89,6 @@ example : pdiv 0b1101#4 0b10#2 = 0b110#4 := rfl
 example : pdiv 0x1a#5 0b10#2 = 0b1101#5 := rfl
 example : pdiv 0b1#1 0b10#2 = 0b0#1 := rfl
 
--- /-- Performs modulus of polynomials over GF(2). -/
--- def pmod (x : BitVec n) (y : BitVec (m + 1)) (H : 0 < m) : BitVec m :=
---   let rec pmodTR (x : BitVec n) (y : BitVec (m + 1)) (p : BitVec (m + 1))
---     (i : Nat) (r : BitVec m) (H : 0 < m) : BitVec m :=
---     match i with
---     | 0 => r
---     | j + 1 =>
---       let xi := getLsbD x (n - i)
---       let tmp :=
---         if xi then extractLsb' 0 m p else BitVec.zero m
---       let r := r ^^^ tmp
---       pmodTR x y (GCMV8.reduce y (p <<< 1)) j r H
---   if y = 0 then 0 else pmodTR x y (GCMV8.reduce y 1) n (BitVec.zero m) H
-
 /-- Performs modulus of polynomials over GF(2).
     Defined using non-ite statements.-/
 def pmod (x : BitVec n) (y : BitVec (m + 1)) (H : 0 < m) : BitVec m :=