Added keccak utils

ProvenZk/Binary.lean

@@ -66,6 +66,16 @@ def zmod_to_bit {n} (x : ZMod n) : Bit := match ZMod.val x with
 @[reducible]
 def is_bit (a : ZMod N): Prop := a = 0 ∨ a = 1
 
+@[simp]
+theorem is_bit_zero : is_bit (0 : ZMod n) := by tauto
+
+@[simp]
+theorem is_bit_one : is_bit (1 : ZMod n) := by tauto
+
+abbrev bOne : {v : ZMod n // is_bit v} := ⟨1, by simp⟩
+
+abbrev bZero : {v : ZMod n // is_bit v} := ⟨0, by simp⟩
+
 def is_vector_binary {d n} (x : Vector (ZMod n) d) : Prop :=
   (List.foldr (fun a r => is_bit a ∧ r) True (Vector.toList x))
 
@@ -516,3 +526,77 @@ lemma vector_bit_to_zmod_last {d n : Nat} [Fact (n > 1)] {xs : Vector Bit (d+1)}
   have hxs : vector_zmod_to_bit (Vector.map (fun i => @Bit.toZMod n i) xs) = xs := by
     simp [vector_bit_to_zmod_to_bit]
   rw [hx, hxs]
+
+@[elab_as_elim]
+def bitCases' {n : Nat} {C : Subtype (α := ZMod n.succ.succ) is_bit → Sort _} (v : Subtype (α := ZMod n.succ.succ) is_bit)
+  (zero : C bZero)
+  (one : C bOne): C v := by
+  rcases v with ⟨v, h⟩
+  rcases v with ⟨v, _⟩
+  cases v with
+  | zero => exact zero
+  | succ v => cases v with
+    | zero => exact one
+    | succ v =>
+      apply False.elim
+      rcases h with h | h <;> {
+        injection h with h
+        simp at h
+      }
+
+theorem isBitCases (b : Subtype (α := ZMod n) is_bit): b = bZero ∨ b = bOne := by
+  cases b with | mk _ prop =>
+  cases prop <;> {subst_vars ; tauto }
+
+
+def bitCases : { v : ZMod (Nat.succ (Nat.succ n)) // is_bit v} → Bit
+  | ⟨0, _⟩ => Bit.zero
+  | ⟨1, _⟩ => Bit.one
+  | ⟨⟨Nat.succ (Nat.succ i), _⟩, h⟩ => False.elim (by
+      cases h <;> {
+        rename_i h
+        injection h with h;
+        rw [Nat.mod_eq_of_lt] at h
+        . injection h; try (rename_i h; injection h)
+        . simp
+      }
+    )
+
+@[simp] lemma ne_1_0 {n:Nat}: ¬(1 : ZMod (n.succ.succ)) = (0 : ZMod (n.succ.succ)) := by
+  intro h;
+  conv at h => lhs; whnf
+  conv at h => rhs; whnf
+  injection h with h
+  injection h
+
+@[simp] lemma ne_0_1 {n:Nat}: ¬(0 : ZMod (n.succ.succ)) = (1 : ZMod (n.succ.succ)) := by
+  intro h;
+  conv at h => lhs; whnf
+  conv at h => rhs; whnf
+  injection h with h
+  injection h
+
+
+@[simp]
+lemma bitCases_eq_0 : bitCases b = Bit.zero ↔ b = bZero := by
+  cases b with | mk val prop =>
+  cases prop <;> {
+    subst_vars
+    conv => lhs; lhs; whnf
+    simp
+  }
+
+@[simp]
+lemma bitCases_eq_1 : bitCases b = Bit.one ↔ b = bOne := by
+  cases b with | mk val prop =>
+  cases prop <;> {
+    subst_vars
+    conv => lhs; lhs; whnf
+    simp
+  }
+
+@[simp]
+lemma bitCases_bZero {n:Nat}: bitCases (@bZero (n + 2)) = Bit.zero := by rfl
+
+@[simp]
+lemma bitCases_bOne {n:Nat}: bitCases (@bOne (n+2)) = Bit.one := by rfl

ProvenZk/Ext/Fin.lean

@@ -0,0 +1,26 @@
+import Std.Data.Fin.Basic
+import Std.Classes.Cast
+import Mathlib.Data.Fin.Basic
+import Mathlib.Tactic.Linarith.Frontend
+
+namespace Fin
+
+theorem castSucc_succ_eq_succ_castSucc : Fin.castSucc (Fin.succ i) = Fin.succ (Fin.castSucc i) := by
+  rfl
+
+theorem last_succ_eq_succ_last : Fin.last (Nat.succ n) = Fin.succ (Fin.last n) := by
+  rfl
+
+theorem last_def : Fin.mk (n := Nat.succ n) n (by simp) = Fin.last n := by
+  rfl
+
+theorem castSucc_def {i : Fin n} :
+  Fin.mk (n := Nat.succ n) (i.val) (by cases i; linarith) = i.castSucc := by
+  rfl
+
+theorem cast_last {n : Nat} : ↑n = Fin.last n := by
+  conv => lhs; whnf
+  conv => rhs; whnf
+  simp
+
+end Fin

ProvenZk/Ext/Vector/Basic.lean

@@ -2,6 +2,7 @@ import Mathlib.Data.Vector.Snoc
 import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.List.Defs
 
+import ProvenZk.Ext.Fin
 import ProvenZk.Ext.Range
 import ProvenZk.Ext.List
 
@@ -192,8 +193,101 @@ lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toLi
 lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by
   rfl
 
-lemma cons_zero {d : Nat } {y : α} {v : Vector α d} :
-  (y ::ᵥ v)[0] = y := by
-    rfl
+@[simp]
+theorem vector_get_zero {vs : Vector i n} : (v ::ᵥ vs)[0] = v := by rfl
+
+@[simp]
+theorem vector_get_succ_fin {vs : Vector i n} {i : Fin n} : (v ::ᵥ vs)[i.succ] = vs[i] := by rfl
+
+@[simp]
+theorem vector_get_succ_nat {vs : Vector i n} {i : Nat} {h : i.succ < n.succ } : (v ::ᵥ vs)[i.succ]'h = vs[i]'(by linarith) := by rfl
+
+@[simp]
+theorem vector_get_snoc_last { vs : Vector α n }:
+  (vs.snoc v).get (Fin.last n) = v := by
+  induction n with
+  | zero =>
+    cases vs using Vector.casesOn; rfl
+  | succ n ih =>
+    cases vs using Vector.casesOn
+    rw [Fin.last_succ_eq_succ_last, Vector.snoc_cons, Vector.get_cons_succ, ih]
+
+@[simp]
+lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = vs.get i := by
+  cases n
+  case zero => cases i using finZeroElim
+  case succ n =>
+  induction n with
+  | zero =>
+    cases i using Fin.cases with
+    | H0 => cases vs using Vector.casesOn with | cons hd tl => simp
+    | Hs i => cases i using finZeroElim
+  | succ n ih =>
+    cases vs using Vector.casesOn with | cons hd tl =>
+    cases i using Fin.cases with
+    | H0 => simp
+    | Hs i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih]
+
+theorem vector_get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by
+  rfl
+
+theorem getElem_def {v : Vector α n} {i : Nat} {prop}: v[i]'prop = v.get ⟨i, prop⟩ := by
+  rfl
+
+@[simp]
+lemma vector_get_snoc_fin_prev {vs : Vector α n} {v : α} {i : Fin n}:
+  (vs.snoc v)[i.val]'(by (have := i.prop); linarith) = vs[i.val]'(i.prop) := by
+  simp [vector_get_val_getElem, getElem_def, Fin.castSucc_def]
+
+theorem ofFn_snoc' { fn : Fin (Nat.succ n) → α }:
+  Vector.ofFn fn = Vector.snoc (Vector.ofFn (fun (x : Fin n) => fn (Fin.castSucc x))) (fn n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; rw [Vector.ofFn, ih]
+    simp [Vector.ofFn]
+    congr
+    simp [Fin.succ]
+    congr
+    simp [Nat.mod_eq_of_lt]
+
+def allIxes (f : α → Prop) : Vector α n → Prop := fun v => ∀(i : Fin n), f v[i]
+
+@[simp]
+theorem allIxes_cons : allIxes f (v ::ᵥ vs) ↔ f v ∧ allIxes f vs := by
+  simp [allIxes, GetElem.getElem]
+  apply Iff.intro
+  . intro h
+    exact ⟨h 0, fun i => h i.succ⟩
+  . intro h i
+    cases i using Fin.cases
+    . simp [h.1]
+    . simp [h.2]
+
+@[simp]
+theorem allIxes_nil : allIxes f Vector.nil := by
+  simp [allIxes]
+
+theorem getElem_allIxes {v : { v: Vector α n // allIxes prop v  }} {i : Nat} { i_small : i < n}:
+  v.val[i]'i_small = ↑(Subtype.mk (v.val.get ⟨i, i_small⟩) (v.prop ⟨i, i_small⟩)) := by rfl
+
+theorem getElem_allIxes₂ {v : { v: Vector (Vector α m) n // allIxes (allIxes prop) v  }} {i j: Nat} { i_small : i < n} { j_small : j < m}:
+  (v.val[i]'i_small)[j]'j_small = ↑(Subtype.mk ((v.val.get ⟨i, i_small⟩).get ⟨j, j_small⟩) (v.prop ⟨i, i_small⟩ ⟨j, j_small⟩)) := by rfl
+
+theorem allIxes_indexed {v : {v : Vector α n // allIxes prop v}} {i : Nat} {i_small : i < n}:
+  prop (v.val[i]'i_small) := v.prop ⟨i, i_small⟩
+
+theorem allIxes_indexed₂ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes prop) v}}
+  {i : Nat} {i_small : i < c}
+  {j : Nat} {j_small : j < b}:
+  prop ((v.val[i]'i_small)[j]'j_small) :=
+  v.prop ⟨i, i_small⟩ ⟨j, j_small⟩
+
+theorem allIxes_indexed₃ {v : {v : Vector (Vector (Vector α a) b) c // allIxes (allIxes (allIxes prop)) v}}
+  {i : Nat} {i_small : i < c}
+  {j : Nat} {j_small : j < b}
+  {k : Nat} {k_small : k < a}:
+  prop (((v.val[i]'i_small)[j]'j_small)[k]'k_small) :=
+  v.prop ⟨i, i_small⟩ ⟨j, j_small⟩ ⟨k, k_small⟩
 
 end Vector

ProvenZk/Misc.lean

@@ -1,6 +1,10 @@
 import ProvenZk.Gates
+import ProvenZk.Binary
 
-theorem or_rw [Fact (Nat.Prime N)] (a b out : (ZMod N)) : Gates.or a b out ↔
+variable {N : Nat}
+variable [Fact (Nat.Prime N)]
+
+theorem or_rw (a b out : (ZMod N)) : Gates.or a b out ↔
   (Gates.is_bool a ∧ Gates.is_bool b ∧
   ( (out = 1 ∧ (a = 1 ∨ b = 1) ∨
     (out = 0 ∧ a = 0 ∧ b = 0)))) := by
@@ -10,7 +14,7 @@ theorem or_rw [Fact (Nat.Prime N)] (a b out : (ZMod N)) : Gates.or a b out ↔
   intro ha hb
   cases ha <;> cases hb <;> { subst_vars; simp }
 
-lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with
+lemma select_rw {b i1 i2 out : (ZMod N)} : (Gates.select b i1 i2 out) ↔ is_bit b ∧ match zmod_to_bit b with
   | Bit.zero => out = i2
   | Bit.one => out = i1 := by
   unfold Gates.select
@@ -42,6 +46,38 @@ lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b
     }
   }
 
+@[simp]
+theorem is_bool_is_bit (a : ZMod n) [Fact (Nat.Prime n)]: Gates.is_bool a = is_bit a := by rfl
+
+@[simp]
+theorem select_zero {a b r : ZMod N}: Gates.select 0 a b r = (r = b) := by
+  simp [Gates.select]
+
+@[simp]
+theorem select_one {a b r : ZMod N}: Gates.select 1 a b r = (r = a) := by
+  simp [Gates.select]
+
+@[simp]
+theorem or_zero { a r : ZMod N}: Gates.or a 0 r = (is_bit a ∧ r = a) := by
+  simp [Gates.or]
+
+@[simp]
+theorem zero_or { a r : ZMod N}: Gates.or 0 a r = (is_bit a ∧ r = a) := by
+  simp [Gates.or]
+
+@[simp]
+theorem one_or { a r : ZMod N}: Gates.or 1 a r = (is_bit a ∧ r = 1) := by
+  simp [Gates.or]
+
+@[simp]
+theorem or_one { a r : ZMod N}: Gates.or a 1 r = (is_bit a ∧ r = 1) := by
+  simp [Gates.or]
+
+@[simp]
+theorem is_bit_one_sub {a : ZMod N}: is_bit (Gates.sub 1 a) ↔ is_bit a := by
+  simp [Gates.sub, is_bit, sub_eq_zero]
+  tauto
+
 lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by
   simp
   tauto

ProvenZk/Subvector.lean

@@ -0,0 +1,61 @@
+import ProvenZk.Ext.Vector
+
+abbrev SubVector α n prop := Subtype (α := Vector α n) (Vector.allIxes prop)
+
+namespace SubVector
+
+def nil : SubVector α 0 prop := ⟨Vector.nil, by simp⟩
+
+def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop :=
+  ⟨vs.val.snoc v.val, by
+    intro i
+    cases i using Fin.lastCases with
+    | hlast => simp [GetElem.getElem, Fin.last_def, Subtype.property]
+    | hcast i =>
+      have := vs.prop i
+      simp at this
+      simp [*]
+  ⟩
+
+@[elab_as_elim]
+def revCases {C : ∀ {n:Nat}, SubVector α n prop → Sort _} (v : SubVector α n prop)
+  (nil : C nil)
+  (snoc : ∀ {n : Nat} (vs : SubVector α n prop) (v : Subtype prop), C (vs.snoc v)): C v := by
+  rcases v with ⟨v, h⟩
+  cases v using Vector.revCasesOn with
+  | nil => exact nil
+  | snoc vs v =>
+    refine snoc ⟨vs, ?vsp⟩ ⟨v, ?vp⟩
+    case vsp =>
+      intro i
+      have := h i.castSucc
+      simp at this
+      simp [this]
+    case vp =>
+      have := h (Fin.last _)
+      simp [GetElem.getElem, Fin.last_def] at this
+      exact this
+
+instance : GetElem (SubVector α n prop) (Fin n) (Subtype prop) (fun _ _ => True) where
+  getElem v i _ := ⟨v.val.get i, v.prop i⟩
+
+def lower (v: SubVector α n prop): Vector {v : α // prop v} n :=
+  Vector.ofFn fun i => v[i]
+
+def lift {prop : α → Prop} (v : Vector (Subtype prop) n): SubVector α n prop :=
+  ⟨v.map Subtype.val, by
+    intro i
+    simp [GetElem.getElem, Subtype.property]⟩
+
+theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}:
+  (vs.snoc v).lower = vs.lower.snoc v := by
+  unfold lower
+  rw [Vector.ofFn_snoc']
+  congr
+  . funext i
+    cases n with
+    | zero => cases i using finZeroElim
+    | _ => simp [GetElem.getElem, snoc]
+  . simp [GetElem.getElem, snoc, Fin.cast_last]
+
+end SubVector