You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <used_lib_defs>...</used_lib_defs>: Imported library definitions directly used by the theorem.
* <used_repo_defs>...</used_repo_defs>: Definitions from the local project (but outside the current file), directly or transitively used by the theorem.
* <lib_lemmas>...</lib_lemmas>: Imported library lemmas/theorems that may assist the proof.
* <repo_lemmas>...</repo_lemmas>: Lemmas/theorems defined in the local project outside this file.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for used definitions and helpful lemmas (used_lib_defs, used_repo_defs, lib_lemmas, repo_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<used_lib_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</used_lib_defs>

<repo_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]
</repo_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<used_lib_defs>
ZMod in Mathlib.Data.ZMod.Defs
Fin in Init.Prelude
DecidableEq in Init.Prelude
Vector in Init.Data.Vector.Basic
String in Init.Prelude
Unit in Init.Prelude
List in Init.Prelude
Field in Mathlib.Algebra.Field.Defs
Inhabited in Init.Prelude
Vector.mapM in Init.Data.Vector.Basic
UInt64 in Init.Prelude
Vector.finRange in Init.Data.Vector.FinRange
Vector.map in Init.Data.Vector.Basic
False.elim in Init.Prelude
Nat in Init.Prelude
id in Init.Prelude
Vector.push in Init.Data.Vector.Basic
Fin.reduceEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceFinMk in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Monad in Init.Prelude
NeZero in Init.Data.NeZero
IO in Init.System.IO
UInt32 in Init.Prelude
And in Init.Prelude
Not in Init.Prelude
Fin.foldl in Init.Data.Fin.Fold
Vector.foldlM in Init.Data.Vector.Basic
Repr in Init.Data.Repr
List.Vector in Mathlib.Data.Vector.Defs
Prod in Init.Prelude
Prod.snd in Init.Prelude
StateM in Init.Control.State
List.Forall in Mathlib.Data.List.Defs
</used_lib_defs>

<used_repo_defs>
syntax "infer_constant_length" : tactic

syntax "let " ident " <== " term : doElem

syntax "let " ident " : " term " <== " term : doElem

@[inherit_doc] notation:67 "<+>" => Trace.empty

macro_rules
  | `(doElem| let $x <== $e) => `(doElem| let $x ← HasAssignEq.assignEq $e)
  | `(doElem| let $x : $t <== $e) => `(doElem| let $x : $t ← HasAssignEq.assignEq $e)

macro_rules
  | `(tactic|simp_assign_row) =>
    `(tactic|(
    simp only [assignCurrRow, assignNextRow, size]
    rw [List.finRange, List.ofFn]
    repeat rw [Fin.foldr_succ]
    rw [Fin.foldr_zero]
    repeat rw [List.forM_cons]
    rw [List.forM_nil, bind_pure_unit]
    simp only [seval, toVars, toElements, Fin.cast_eq_self, Fin.val_zero, Fin.val_one, Fin.isValue,
      List.getElem_toArray, List.getElem_cons_zero, List.getElem_cons_succ, Fin.succ_zero_eq_one]))

macro_rules
  | `(tactic|infer_constant_length) => `(tactic|(
    apply ConstantLength.fromConstantLength
    try simp only [circuit_norm]
    try intros
    try ac_rfl))

example :
  let add (x : Expression F) := do
    let y : Expression F ← witness fun _ => 1
    let z ← witness fun eval => eval (x + y)
    assertZero (x + y - z)
    pure z
  ConstantLength add := by admit /- proof elided -/

def KeccakBlock.Normalized (block : KeccakBlock (F p)) :=
  ∀ i : Fin RATE, block[i.val].Normalized

def F p := ZMod p

@[reducible] def RATE := 17
example : RATE + CAPACITY = 25 := rfl

@[reducible] def CAPACITY := 8

def value (x : U64 (F p)) :=
  x.x0.val + x.x1.val * 256 + x.x2.val * 256^2 + x.x3.val * 256^3 +
  x.x4.val * 256^4 + x.x5.val * 256^5 + x.x6.val * 256^6 + x.x7.val * 256^7

structure U64 (T : Type) where
  x0 : T
  x1 : T
  x2 : T
  x3 : T
  x4 : T
  x5 : T
  x6 : T
  x7 : T
deriving DecidableEq

def KeccakRow.value (row : KeccakRow (F p)) := row.map U64.value

def map {α β : Type} (x : U64 α) (f : α → β) : U64 β :=
  ⟨ f x.x0, f x.x1, f x.x2, f x.x3, f x.x4, f x.x5, f x.x6, f x.x7 ⟩

def map {m : ℕ} (xs : Vector α m) (body : α → Circuit F β)
    (_constant : ConstantLength body := by admit /- proof elided -/
    ) : Circuit F (Vector β m) :=
  xs.mapM body

def Circuit (F : Type) [Field F] (α : Type) := ℕ → α × List (Operation F)

inductive Operation (F : Type) [Field F] where
  | witness : (m : ℕ) → (compute : Environment F → Vector F m) → Operation F
  | assert : Expression F → Operation F
  | lookup : Lookup F → Operation F
  | subcircuit : {n : ℕ} → Subcircuit F n → Operation F

structure Condition (F : Type) [Field F] where
  witness (offset : ℕ) : (m : ℕ) → (Environment F → Vector F m) → Prop := fun _ _ => True
  assert (offset : ℕ) (_ : Expression F) : Prop := True
  lookup (offset : ℕ) (_ : Lookup F) : Prop := True
  subcircuit (offset : ℕ) {m : ℕ} (_ : Subcircuit F m) : Prop := True

inductive FlatOperation (F : Type) where
  | witness : (m : ℕ) → (Environment F → Vector F m) → FlatOperation F
  | assert : Expression F → FlatOperation F
  | lookup : Lookup F → FlatOperation F

structure Subcircuit (F : Type) [Field F] (offset : ℕ) where
  ops : List (FlatOperation F)

  
  
  
  Soundness : Environment F → Prop
  Completeness : Environment F → Prop
  UsesLocalWitnesses : Environment F → Prop

  
  
  localLength : ℕ

  
  imply_soundness : ∀ env,
    ConstraintsHoldFlat env ops → Soundness env

  
  implied_by_completeness : ∀ env, env.ExtendsVector (localWitnesses env ops) offset →
    Completeness env → ConstraintsHoldFlat env ops

  
  imply_usesLocalWitnesses : ∀ env, env.ExtendsVector (localWitnesses env ops) offset →
    UsesLocalWitnesses env

  
  localLength_eq : localLength = FlatOperation.localLength ops

@[circuit_norm]
def localWitnesses (env : Environment F) : (l : List (FlatOperation F)) → Vector F (localLength l)
  | [] => #v[]
  | witness _ compute :: ops => compute env ++ localWitnesses env ops
  | assert _ :: ops | lookup _ :: ops => localWitnesses env ops

@[circuit_norm]
def lookup {Row : TypeMap} [ProvableType Row] (table : Table F Row)  (entry : Row (Expression F)) : Circuit F Unit := fun _ =>
  ((), [.lookup { table := table.toRaw, entry := toElements entry }])

@[circuit_norm]
def Table.toRaw (table : Table F Row) : RawTable F where
  name := table.name
  arity := size Row
  Contains row := table.Contains (fromElements row)
  Soundness row := table.Soundness (fromElements row)
  Completeness row := table.Completeness (fromElements row)
  imply_soundness row := table.imply_soundness (fromElements row)
  implied_by_completeness row := table.implied_by_completeness (fromElements row)

structure RawTable (F : Type) where
  name : String
  arity : ℕ
  Contains : Vector F arity → Prop
  Soundness : Vector F arity → Prop
  Completeness : Vector F arity → Prop
  imply_soundness : ∀ row, Contains row → Soundness row
  implied_by_completeness : ∀ row, Completeness row → Contains row

structure StaticTable (F : Type) (Row : TypeMap) [ProvableType Row] where
  name : String
  length : ℕ
  row : Fin length → Row F
  
  
  
  index : Row F → ℕ
  Spec : Row F → Prop
  contains_iff : ∀ t, (∃ i, t = row i) ↔ Spec t

def Contains (table : StaticTable F Row) (row : Row F) :=
  ∃ i : Fin table.length, row = table.row i

instance ProvableType.fromStruct {α : TypeMap} [ProvableStruct α] : ProvableType α where
  size := combinedSize α
  toElements x :=
    toComponents x |> componentsToElements (components α) |>.cast combinedSize_eq.symm
  fromElements v :=
    v.cast combinedSize_eq |> componentsFromElements (components α) |> fromComponents
  fromElements_toElements x := by admit /- proof elided -/

@[reducible]
def TypeMap := Type → Type

structure Table (F : Type) (Row : TypeMap) [ProvableType Row] where
  name : String
   
  Contains : Row F → Prop

   
  Soundness : Row F → Prop
  Completeness : Row F → Prop

  imply_soundness : ∀ row, Contains row → Soundness row
  implied_by_completeness : ∀ row, Completeness row → Contains row

inductive Expression (F : Type) where
  | var : Variable F -> Expression F
  | const : F -> Expression F
  | add : Expression F -> Expression F -> Expression F
  | mul : Expression F -> Expression F -> Expression F

structure Variable (F : Type) where
  index : ℕ

def const (x : α F) : Var α F :=
  let values : Vector F _ := toElements x
  fromVars (values.map .const)

@[reducible] def Var (M : TypeMap) (F : Type) := M (Expression F)

@[circuit_norm]
def fromVars (vars : Vector (Expression F) (size M)) := fromElements vars

structure Lookup (F : Type) where
  table : RawTable F
  entry : Vector (Expression F) table.arity

class Witnessable (F : Type) [Field F] (value : outParam TypeMap) (var : TypeMap) [ProvableType value] where
  witness : ((Environment F) → value F) → Circuit F (var F)
  var_eq : var F = value (Expression F) := by admit /- proof elided -/

structure Environment (F : Type) where
  get : ℕ → F

@[circuit_norm]
def localLength : List (FlatOperation F) → ℕ
  | [] => 0
  | witness m _ :: ops => m + localLength ops
  | assert _ :: ops | lookup _ :: ops => localLength ops

def ConstraintsHoldFlat (eval : Environment F) : List (FlatOperation F) → Prop
  | [] => True
  | op :: ops => match op with
    | assert e => (eval e = 0) ∧ ConstraintsHoldFlat eval ops
    | lookup { table, entry } =>
      table.Contains (entry.map eval) ∧ ConstraintsHoldFlat eval ops
    | _ => ConstraintsHoldFlat eval ops

class ConstantLength (circuit : α → Circuit F β) where
  localLength : ℕ
  localLength_eq : ∀ (a : α) (n : ℕ), (circuit a).localLength n = localLength

def ConstantLength.fromConstantLength {circuit : α → Circuit F β} [Inhabited α]
    (h : ∀ (a : α) n, (circuit a).localLength n = (circuit default).localLength 0) : ConstantLength circuit where
  localLength := (circuit default).localLength 0
  localLength_eq a n := h a n

structure InductiveTable (F : Type) [Field F] (State Input : Type → Type) [ProvableType State] [ProvableType Input] where
   
  step : Var State F → Var Input F → Circuit F (Var State F)

   
  Spec : (initialState : State F) → (xs : List (Input F)) → (i : ℕ) → (xs.length = i) → (currentState : State F) → Prop

   
  InputAssumptions : ℕ → Input F → Prop := fun _ _ => True
  InitialStateAssumptions : State F → Prop := fun _ => True

  soundness : InductiveTable.Soundness F State Input Spec step

  completeness : InductiveTable.Completeness F State Input InputAssumptions InitialStateAssumptions Spec step

  subcircuitsConsistent : ∀ acc x, ((step acc x).operations ((size State) + (size Input))).SubcircuitsConsistent ((size State) + (size Input))
    := by admit /- proof elided -/

def KeccakState.Normalized (state : KeccakState (F p)) :=
  ∀ i : Fin 25, state[i.val].Normalized

def Normalized (x : U32 (F p)) :=
  x.x0.val < 256 ∧ x.x1.val < 256 ∧ x.x2.val < 256 ∧ x.x3.val < 256

structure U32 (T : Type) where
  x0 : T
  x1 : T
  x2 : T
  x3 : T
deriving DecidableEq

def KeccakRow.Normalized (row : KeccakRow (F p)) :=
  ∀ i : Fin 5, row[i.val].Normalized

def KeccakBlock.value (block : KeccakBlock (F p)) := block.map U64.value

@[reducible] def Spec (input : Input (F p)) (out_state : KeccakState (F p)) :=
  out_state.Normalized ∧
  out_state.value = absorbBlock input.state.value input.block.value

structure Input (F : Type) where
  state : KeccakState F
  block : KeccakBlock F

@[reducible] def KeccakBlock := ProvableVector U64 RATE

instance ProvableVector.instance : ProvableType (ProvableVector α n) where
  size := n * size α
  toElements x := x.map toElements |>.flatten
  fromElements v := v.toChunks (psize α) |>.map fromElements
  fromElements_toElements x := by admit /- proof elided -/

@[reducible] def KeccakState := ProvableVector U64 25

structure Inputs (F : Type) where
  state : KeccakState F
  d : KeccakRow F

def state : Vector (U64 ℕ) 25 := #v[
  ⟨67, 168, 144, 181, 2, 173, 144, 47⟩,
  ⟨114, 52, 107, 105, 171, 22, 114, 75⟩,
  ⟨196, 118, 22, 253, 100, 162, 87, 52⟩,
  ⟨50, 65, 171, 81, 229, 6, 172, 155⟩,
  ⟨178, 167, 68, 225, 82, 73, 216, 194⟩,
  ⟨193, 5, 52, 193, 148, 168, 64, 147⟩,
  ⟨212, 142, 107, 244, 55, 237, 100, 203⟩,
  ⟨101, 34, 195, 62, 133, 216, 64, 34⟩,
  ⟨240, 214, 204, 27, 17, 231, 66, 179⟩,
  ⟨136, 37, 228, 137, 64, 208, 27, 90⟩,
  ⟨177, 229, 130, 4, 191, 7, 25, 117⟩,
  ⟨124, 168, 245, 7, 222, 138, 168, 16⟩,
  ⟨115, 130, 213, 74, 217, 123, 172, 109⟩,
  ⟨128, 149, 137, 6, 45, 133, 77, 101⟩,
  ⟨104, 90, 153, 237, 72, 44, 164, 84⟩,
  ⟨129, 177, 235, 28, 82, 30, 150, 201⟩,
  ⟨52, 55, 32, 241, 142, 211, 246, 68⟩,
  ⟨149, 124, 124, 204, 34, 220, 229, 69⟩,
  ⟨215, 168, 47, 96, 70, 5, 220, 2⟩,
  ⟨53, 224, 38, 18, 110, 66, 70, 9⟩,
  ⟨213, 122, 200, 196, 186, 122, 207, 42⟩,
  ⟨141, 103, 32, 88, 244, 160, 37, 76⟩,
  ⟨99, 242, 138, 24, 4, 30, 100, 196⟩,
  ⟨141, 253, 136, 54, 8, 21, 204, 152⟩,
  ⟨93, 161, 29, 12, 44, 252, 49, 57⟩
]

def absorbBlock (state : Vector ℕ 25) (block : Vector ℕ RATE) : Vector ℕ 25 :=
  
  let state' := Vector.mapFinRange 25 fun i => state[i] ^^^ (if _ : i.val < RATE then block[i] else 0)
  
  keccakPermutation state'

def keccakPermutation (state : Vector ℕ 25): Vector ℕ 25 :=
  roundConstants.foldl keccakRound state

def keccakRound (state : Vector ℕ 25) (rc : UInt64) : Vector ℕ 25 :=
  let theta_state := theta state
  let rho_pi_state := rhoPi theta_state
  let chi_state := chi rho_pi_state
  iota chi_state rc

def theta (state : Vector ℕ 25) : Vector ℕ 25 :=
  let c := thetaC state
  let d := thetaD c
  thetaXor state d

def thetaXor (state : Vector ℕ 25) (d : Vector ℕ 5) : Vector ℕ 25 :=
  #v[
    state[0] ^^^ d[0],
    state[1] ^^^ d[0],
    state[2] ^^^ d[0],
    state[3] ^^^ d[0],
    state[4] ^^^ d[0],
    state[5] ^^^ d[1],
    state[6] ^^^ d[1],
    state[7] ^^^ d[1],
    state[8] ^^^ d[1],
    state[9] ^^^ d[1],
    state[10] ^^^ d[2],
    state[11] ^^^ d[2],
    state[12] ^^^ d[2],
    state[13] ^^^ d[2],
    state[14] ^^^ d[2],
    state[15] ^^^ d[3],
    state[16] ^^^ d[3],
    state[17] ^^^ d[3],
    state[18] ^^^ d[3],
    state[19] ^^^ d[3],
    state[20] ^^^ d[4],
    state[21] ^^^ d[4],
    state[22] ^^^ d[4],
    state[23] ^^^ d[4],
    state[24] ^^^ d[4]
  ]

def thetaC (state : Vector ℕ 25) : Vector ℕ 5 :=
  #v[
    state[0] ^^^ state[1] ^^^ state[2] ^^^ state[3] ^^^ state[4],
    state[5] ^^^ state[6] ^^^ state[7] ^^^ state[8] ^^^ state[9],
    state[10] ^^^ state[11] ^^^ state[12] ^^^ state[13] ^^^ state[14],
    state[15] ^^^ state[16] ^^^ state[17] ^^^ state[18] ^^^ state[19],
    state[20] ^^^ state[21] ^^^ state[22] ^^^ state[23] ^^^ state[24]
  ]

def thetaD (c : Vector ℕ 5) : Vector ℕ 5 :=
  #v[
    c[4] ^^^ (rotLeft64 c[1] 1),
    c[0] ^^^ (rotLeft64 c[2] 1),
    c[1] ^^^ (rotLeft64 c[3] 1),
    c[2] ^^^ (rotLeft64 c[4] 1),
    c[3] ^^^ (rotLeft64 c[0] 1)
  ]

def rotLeft64 (value : ℕ) (left : Fin 64) : ℕ:=
  let right := (64 - left) % 64
  rotRight64 value right

def rotRight64 (x : ℕ) (offset : ℕ) : ℕ :=
  let offset := offset % 64
  let low := x % (2^offset)
  let high := x / (2^offset)
  low * (2^(64-offset)) + high

class HasAssignEq (β : Type) (F : outParam Type) [Field F] where
  assignEq : β → Circuit F β

def iota (state : Vector ℕ 25) (rc : UInt64) : Vector ℕ 25 :=
  state.set 0 ((state[0]) ^^^ rc.toFin)

def rhoPi (state : Vector ℕ 25) : Vector ℕ 25 :=
  #v[
    rotLeft64 state[0] 0,
    rotLeft64 state[15] 28,
    rotLeft64 state[5] 1,
    rotLeft64 state[20] 27,
    rotLeft64 state[10] 62,
    rotLeft64 state[6] 44,
    rotLeft64 state[21] 20,
    rotLeft64 state[11] 6,
    rotLeft64 state[1] 36,
    rotLeft64 state[16] 55,
    rotLeft64 state[12] 43,
    rotLeft64 state[2] 3,
    rotLeft64 state[17] 25,
    rotLeft64 state[7] 10,
    rotLeft64 state[22] 39,
    rotLeft64 state[18] 21,
    rotLeft64 state[8] 45,
    rotLeft64 state[23] 8,
    rotLeft64 state[13] 15,
    rotLeft64 state[3] 41,
    rotLeft64 state[24] 14,
    rotLeft64 state[14] 61,
    rotLeft64 state[4] 18,
    rotLeft64 state[19] 56,
    rotLeft64 state[9] 2
  ]

def chi (b : Vector ℕ 25) : Vector ℕ 25 :=
  #v[
    b[0] ^^^ ((not64 b[5]) &&& b[10]),
    b[1] ^^^ ((not64 b[6]) &&& b[11]),
    b[2] ^^^ ((not64 b[7]) &&& b[12]),
    b[3] ^^^ ((not64 b[8]) &&& b[13]),
    b[4] ^^^ ((not64 b[9]) &&& b[14]),
    b[5] ^^^ ((not64 b[10]) &&& b[15]),
    b[6] ^^^ ((not64 b[11]) &&& b[16]),
    b[7] ^^^ ((not64 b[12]) &&& b[17]),
    b[8] ^^^ ((not64 b[13]) &&& b[18]),
    b[9] ^^^ ((not64 b[14]) &&& b[19]),
    b[10] ^^^ ((not64 b[15]) &&& b[20]),
    b[11] ^^^ ((not64 b[16]) &&& b[21]),
    b[12] ^^^ ((not64 b[17]) &&& b[22]),
    b[13] ^^^ ((not64 b[18]) &&& b[23]),
    b[14] ^^^ ((not64 b[19]) &&& b[24]),
    b[15] ^^^ ((not64 b[20]) &&& b[0]),
    b[16] ^^^ ((not64 b[21]) &&& b[1]),
    b[17] ^^^ ((not64 b[22]) &&& b[2]),
    b[18] ^^^ ((not64 b[23]) &&& b[3]),
    b[19] ^^^ ((not64 b[24]) &&& b[4]),
    b[20] ^^^ ((not64 b[0]) &&& b[5]),
    b[21] ^^^ ((not64 b[1]) &&& b[6]),
    b[22] ^^^ ((not64 b[2]) &&& b[7]),
    b[23] ^^^ ((not64 b[3]) &&& b[8]),
    b[24] ^^^ ((not64 b[4]) &&& b[9])
  ]

def not64 (a : ℕ) : ℕ := a ^^^ 0xffffffffffffffff

def roundConstants : Vector UInt64 24 := #v[
  0x0000000000000001, 0x0000000000008082,
  0x800000000000808a, 0x8000000080008000,
  0x000000000000808b, 0x0000000080000001,
  0x8000000080008081, 0x8000000000008009,
  0x000000000000008a, 0x0000000000000088,
  0x0000000080008009, 0x000000008000000a,
  0x000000008000808b, 0x800000000000008b,
  0x8000000000008089, 0x8000000000008003,
  0x8000000000008002, 0x8000000000000080,
  0x000000000000800a, 0x800000008000000a,
  0x8000000080008081, 0x8000000000008080,
  0x0000000080000001, 0x8000000080008008
]

def mapFinRange (n : ℕ) (create : Fin n → α) : Vector α n := finRange n |>.map create

def KeccakState.value (state : KeccakState (F p)) := state.map U64.value

def value (x : U32 (F p)) :=
  x.x0.val + x.x1.val * 256 + x.x2.val * 256^2 + x.x3.val * 256^3

def Normalized (x : U64 (F p)) :=
  x.x0.val < 256 ∧ x.x1.val < 256 ∧ x.x2.val < 256 ∧ x.x3.val < 256 ∧
  x.x4.val < 256 ∧ x.x5.val < 256 ∧ x.x6.val < 256 ∧ x.x7.val < 256

@[reducible] def Assumptions (input : Input (F p)) :=
  input.state.Normalized ∧ input.block.Normalized

def InductiveTable.Completeness (F : Type) [Field F] (State Input : Type → Type) [ProvableType State] [ProvableType Input]
    (InputAssumptions : ℕ → Input F → Prop) (InitialStateAssumptions : State F → Prop)
    (Spec : (initialState : State F) → (xs : List (Input F)) → (i : ℕ) → (xs.length = i) → (currentState : State F) → Prop)
    (step : Var State F → Var Input F → Circuit F (Var State F)) :=
  ∀ (initialState : State F) (row_index : ℕ) (env : Environment F),
  
  ∀ (acc_var : Var State F) (x_var : Var Input F)
    (acc : State F) (x : Input F) (xs : List (Input F)) (xs_len : xs.length = row_index),
    (eval env acc_var = acc) ∧ (eval env x_var = x) →
  
  env.UsesLocalWitnessesCompleteness ((size State) + (size Input)) (step acc_var x_var |>.operations ((size State) + (size Input))) →
  
  InitialStateAssumptions initialState ∧
  Spec initialState xs row_index xs_len acc ∧ InputAssumptions row_index x →
  
  Circuit.ConstraintsHold.Completeness env (step acc_var x_var |>.operations ((size State) + (size Input)))

@[circuit_norm]
def ConstraintsHold (eval : Environment F) : List (Operation F) → Prop
  | [] => True
  | .witness _ _ :: ops => ConstraintsHold eval ops
  | .assert e :: ops => eval e = 0 ∧ ConstraintsHold eval ops
  | .lookup { table, entry, .. } :: ops =>
    table.Contains (entry.map eval) ∧ ConstraintsHold eval ops
  | .subcircuit s :: ops =>
    ConstraintsHoldFlat eval s.ops ∧ ConstraintsHold eval ops

@[circuit_norm]
def subcircuit (circuit : FormalCircuit F β α) (b : Var β F) : Circuit F (Var α F) :=
  fun offset =>
    let a := circuit.output b offset
    let subcircuit := circuit.toSubcircuit offset b
    (a, [.subcircuit subcircuit])

def FormalAssertion.toSubcircuit (circuit : FormalAssertion F β)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

  {
    ops := ops.toFlat,
    Soundness env := circuit.Assumptions (eval env input_var) → circuit.Spec (eval env input_var),
    Completeness env := circuit.Assumptions (eval env input_var) ∧ circuit.Spec (eval env input_var),
    UsesLocalWitnesses _ := True,
    localLength := circuit.localLength input_var

    imply_soundness := by admit /- proof elided -/

class ElaboratedCircuit (F : Type) (Input Output : TypeMap) [Field F] [ProvableType Input] [ProvableType Output] where
  main : Var Input F → Circuit F (Var Output F)

   
  localLength : Var Input F → ℕ

   
  localLength_eq : ∀ input offset, (main input).localLength offset = localLength input
    := by admit /- proof elided -/

@[circuit_norm]
def localLength : Operation F → ℕ
  | .witness m _ => m
  | .assert _ => 0
  | .lookup _ => 0
  | .subcircuit s => s.localLength

@[circuit_norm]
def localLength : Operations F → ℕ
  | [] => 0
  | .witness m _ :: ops => m + localLength ops
  | .assert _ :: ops => localLength ops
  | .lookup _ :: ops => localLength ops
  | .subcircuit s :: ops => s.localLength + localLength ops

@[reducible, circuit_norm]
def Operations (F : Type) [Field F] := List (Operation F)

structure FormalCircuit (F : Type) [Field F] (Input Output : TypeMap) [ProvableType Input] [ProvableType Output]
    extends elaborated : ElaboratedCircuit F Input Output where
  Assumptions (_ : Input F) : Prop := True
  Spec : Input F → Output F → Prop
  soundness : Soundness F elaborated Assumptions Spec
  completeness : Completeness F elaborated Assumptions

structure FormalAssertion (F : Type) (Input : TypeMap) [Field F] [ProvableType Input]
    extends elaborated : ElaboratedCircuit F Input unit where
  Assumptions : Input F → Prop
  Spec : Input F → Prop
  soundness : FormalAssertion.Soundness F elaborated Assumptions Spec
  completeness : FormalAssertion.Completeness F elaborated Assumptions Spec

  
  localLength _ := 0
  
  output _ _ := ()

structure GeneralFormalCircuit (F : Type) (Input Output : TypeMap) [Field F] [ProvableType Input] [ProvableType Output]
    extends elaborated : ElaboratedCircuit F Input Output where
  Assumptions : Input F → Prop 
  Spec : Input F → Output F → Prop 
  soundness : GeneralFormalCircuit.Soundness F elaborated Spec
  completeness : GeneralFormalCircuit.Completeness F elaborated Assumptions

@[circuit_norm]
def SubcircuitsConsistent (offset : ℕ) (ops : Operations F) := ops.forAll offset {
  subcircuit offset {n} _ := n = offset
}

 @[circuit_norm]
def forAll (offset : ℕ) (condition : Condition F) : Operations F → Prop
  | [] => True
  | .witness m c :: ops => condition.witness offset m c ∧ forAll (m + offset) condition ops
  | .assert e :: ops => condition.assert offset e ∧ forAll offset condition ops
  | .lookup l :: ops => condition.lookup offset l ∧ forAll offset condition ops
  | .subcircuit s :: ops => condition.subcircuit offset s ∧ forAll (s.localLength + offset) condition ops

def FlatOperation.forAll (offset : ℕ) (condition : Condition F) : List (FlatOperation F) → Prop
  | [] => True
  | .witness m c :: ops => condition.witness offset m c ∧ forAll (m + offset) condition ops
  | .assert e :: ops => condition.assert offset e ∧ forAll offset condition ops
  | .lookup l :: ops => condition.lookup offset l ∧ forAll offset condition ops

@[circuit_norm]
def FormalAssertion.Soundness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input unit)
    (Assumptions : Input F → Prop) (Spec : Input F → Prop) :=
  
  ∀ offset : ℕ, ∀ env,
  
  ∀ input_var : Var Input F, ∀ input : Input F, eval env input_var = input →
  Assumptions input →
  
  ConstraintsHold.Soundness env (circuit.main input_var |>.operations offset) →
  
  Spec input

@[reducible, circuit_norm]
def operations (circuit : Circuit F α) (offset : ℕ) : Operations F :=
  (circuit offset).2

@[circuit_norm]
def ConstraintsHold.Soundness (eval : Environment F) : List (Operation F) → Prop
  | [] => True
  | .witness _ _ :: ops => ConstraintsHold.Soundness eval ops
  | .assert e :: ops => eval e = 0 ∧ ConstraintsHold.Soundness eval ops
  | .lookup { table, entry } :: ops =>
    table.Soundness (entry.map eval) ∧ ConstraintsHold.Soundness eval ops
  | .subcircuit s :: ops =>
    s.Soundness eval ∧ ConstraintsHold.Soundness eval ops

@[circuit_norm]
def Soundness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input Output)
    (Assumptions : Input F → Prop) (Spec : Input F → Output F → Prop) :=
  
  ∀ offset : ℕ, ∀ env,
  
  ∀ input_var : Var Input F, ∀ input : Input F, eval env input_var = input →
  Assumptions input →
  
  ConstraintsHold.Soundness env (circuit.main input_var |>.operations offset) →
  
  let output := eval env (circuit.output input_var offset)
  Spec input output

@[reducible, circuit_norm]
def output (circuit : Circuit F α) (offset : ℕ) : α :=
  (circuit offset).1

@[explicit_provable_type]
def eval (env : Environment F) (x : Var α F) : α F :=
  let vars := toVars x
  let values := vars.map (Expression.eval env)
  fromElements values

@[circuit_norm]
def toVars (var : M (Expression F)) := toElements var

@[circuit_norm]
def eval (env : Environment F) : Expression F → F
  | var v => env.get v.index
  | const c => c
  | add x y => eval env x + eval env y
  | mul x y => eval env x * eval env y

@[circuit_norm]
def GeneralFormalCircuit.Soundness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input Output) (Spec : Input F → Output F → Prop) :=
  
  ∀ offset : ℕ, ∀ env,
  
  ∀ input_var : Var Input F, ∀ input : Input F, eval env input_var = input →
  
  ConstraintsHold.Soundness env (circuit.main input_var |>.operations offset) →
  
  let output := eval env (circuit.output input_var offset)
  Spec input output

@[reducible]
def unit (_ : Type) := Unit

@[reducible, circuit_norm]
def localLength (circuit : Circuit F α) (offset := 0) : ℕ :=
  Operations.localLength (circuit offset).2

@[circuit_norm]
def FormalAssertion.Completeness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input unit)
    (Assumptions : Input F → Prop) (Spec : Input F → Prop) :=
  
  ∀ offset, ∀ env, ∀ input_var : Var Input F,
  env.UsesLocalWitnessesCompleteness offset (circuit.main input_var |>.operations offset) →
  
  ∀ input : Input F, eval env input_var = input →
  Assumptions input → Spec input →
  
  ConstraintsHold.Completeness env (circuit.main input_var |>.operations offset)

@[circuit_norm]
def ConstraintsHold.Completeness (eval : Environment F) : List (Operation F) → Prop
  | [] => True
  | .witness _ _ :: ops => ConstraintsHold.Completeness eval ops
  | .assert e :: ops => eval e = 0 ∧ ConstraintsHold.Completeness eval ops
  | .lookup { table, entry } :: ops =>
    table.Completeness (entry.map eval) ∧ ConstraintsHold.Completeness eval ops
  | .subcircuit s :: ops =>
    s.Completeness eval ∧ ConstraintsHold.Completeness eval ops

@[circuit_norm]
def Completeness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input Output)
    (Assumptions : Input F → Prop) :=
  
  ∀ offset : ℕ, ∀ env, ∀ input_var : Var Input F,
  env.UsesLocalWitnessesCompleteness offset (circuit.main input_var |>.operations offset) →
  
  ∀ input : Input F, eval env input_var = input →
  Assumptions input →
  
  ConstraintsHold.Completeness env (circuit.main input_var |>.operations offset)

@[circuit_norm]
def GeneralFormalCircuit.Completeness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input Output) (Assumptions : Input F → Prop) :=
  
  ∀ offset : ℕ, ∀ env, ∀ input_var : Var Input F,
  env.UsesLocalWitnessesCompleteness offset (circuit.main input_var |>.operations offset) →
  
  ∀ input : Input F, eval env input_var = input →
  Assumptions input →
  
  ConstraintsHold.Completeness env (circuit.main input_var |>.operations offset)

def toFlat : Operations F → List (FlatOperation F)
  | [] => []
  | .witness m c :: ops => .witness m c :: toFlat ops
  | .assert e :: ops => .assert e :: toFlat ops
  | .lookup l :: ops => .lookup l :: toFlat ops
  | .subcircuit s :: ops => s.ops ++ toFlat ops

def Environment.UsesLocalWitnesses (env : Environment F) (offset : ℕ) (ops : Operations F) : Prop :=
  ops.forAllFlat offset { witness n _ compute := env.ExtendsVector (compute env) n }

@[circuit_norm]
def Environment.ExtendsVector (env : Environment F) (wit : Vector F n) (offset : ℕ) : Prop :=
  ∀ i : Fin n, env.get (offset + i.val) = wit[i.val]

def Operations.forAllFlat (n : ℕ) (condition : Condition F) (ops : Operations F) : Prop :=
  forAll n { condition with subcircuit n _ s := FlatOperation.forAll n condition s.ops } ops

def GeneralFormalCircuit.toSubcircuit (circuit : GeneralFormalCircuit F β α)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

  have imply_soundness : ∀ env : Environment F,
      let input := eval env input_var
      let output := eval env (circuit.output input_var n)
      ConstraintsHoldFlat env ops.toFlat → circuit.Spec input output :=

def FormalCircuit.toSubcircuit (circuit : FormalCircuit F β α)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

  have imply_soundness : ∀ env : Environment F,
    let input := eval env input_var
    let output := eval env (circuit.output input_var n)
    ConstraintsHoldFlat env ops.toFlat → circuit.Assumptions input → circuit.Spec input output :=

def map {α β : Type} (x : U32 α) (f : α → β) : U32 β :=
  ⟨ f x.x0, f x.x1, f x.x2, f x.x3 ⟩

def circuit : FormalCircuit (F p) Input KeccakState :=
  { elaborated with Assumptions, Spec, soundness, completeness }

instance elaborated : ElaboratedCircuit (F p) Input KeccakState where
  main
  localLength _ := 31048
  output _ i0 := Permutation.stateVar (i0 + 136) 23

  localLength_eq _ _ := by admit /- proof elided -/

def main (input : Var Input (F p)) : Circuit (F p) (Var KeccakState (F p)) := do
  let { state, block } := input
  
  let state_rate ← Circuit.mapFinRange RATE fun i => Xor64.circuit ⟨state[i.val], block[i.val]⟩

  
  let state_capacity := Vector.mapFinRange (25 - RATE) fun i => state[RATE + i.val]
  let state' : Vector _ 25 := state_rate ++ state_capacity

  
  Permutation.circuit state'

def circuit : FormalCircuit (F p) KeccakState KeccakState := {
  elaborated with
  Assumptions, Spec, soundness
  
  
  completeness := by admit /- proof elided -/

def Spec (state : KeccakState (F p)) (out_state : KeccakState (F p)) :=
  out_state.Normalized
  ∧ out_state.value = keccakPermutation state.value

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakState where
  main
  localLength _ := 30912
  output _ i0 := stateVar i0 23

  localLength_eq state i0 := by admit /- proof elided -/

def main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) :=
  .foldl roundConstants state
    fun state rc => KeccakRound.circuit rc state

def circuit (rc : UInt64) : FormalCircuit (F p) KeccakState KeccakState := {
  elaborated rc with
  Spec := Spec rc
  Assumptions
  soundness := soundness rc,
  completeness := completeness rc,
}

def Spec (rc : UInt64) (state : KeccakState (F p)) (out_state : KeccakState (F p)) :=
  out_state.Normalized
  ∧ out_state.value = keccakRound state.value rc

def Assumptions (state : KeccakState (F p)) := state.Normalized

instance elaborated (rc : UInt64) : ElaboratedCircuit (F p) KeccakState KeccakState where
  main := main rc
  localLength _ := 1288
  output _ i0 := (Vector.mapRange 25 fun i => varFromOffset U64 (i0 + i*16 + 888) ).set 0 (varFromOffset U64 (i0 + 1280))

  localLength_eq _ _ := by admit /- proof elided -/

def main (rc : UInt64) (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) := do
  let state ← Theta.circuit state
  let state ← RhoPi.circuit state
  let state ← Chi.circuit state

  
  let s0 ← Xor64.circuit ⟨state[0], const (U64.fromUInt64 rc)⟩
  return state.set 0 s0

def circuit : FormalCircuit (F p) Inputs U64 where
  Assumptions
  Spec
  soundness
  completeness

structure Inputs (F : Type) where
  x: U64 F
  y: U64 F

def Spec (input : Inputs (F p)) (z : U64 (F p)) :=
  let ⟨x, y⟩ := input
  z.value = x.value ^^^ y.value ∧ z.Normalized

def Assumptions (input : Inputs (F p)) :=
  let ⟨x, y⟩ := input
  x.Normalized ∧ y.Normalized

def fromUInt64 (x : UInt64) : U64 (F p) :=
  decomposeNat x.toFin

def decomposeNat (x : ℕ) : U64 (F p) :=
  let x0 := x % 256
  let x1 : ℕ := (x / 256) % 256
  let x2 : ℕ := (x / 256^2) % 256
  let x3 : ℕ := (x / 256^3) % 256
  let x4 : ℕ := (x / 256^4) % 256
  let x5 : ℕ := (x / 256^5) % 256
  let x6 : ℕ := (x / 256^6) % 256
  let x7 : ℕ := (x / 256^7) % 256
  ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩

def circuit : FormalCircuit (F p) KeccakState KeccakState :=
  { elaborated with Assumptions, Spec, soundness, completeness }

def Assumptions := KeccakState.Normalized (p:=p)

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakState where
  main
  localLength _ := 400
  localLength_eq _ _ := by admit /- proof elided -/

def main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) :=
  .map rhoPiConstants fun (i, s) =>
    Rotation64.circuit (-s) state[i.val]

def rhoPiConstants := rhoPiIndices.zip rhoPiShifts

def rhoPiIndices : Vector (Fin 25) 25 := #v[
  0, 15, 5, 20, 10, 6, 21, 11, 1, 16, 12, 2, 17, 7, 22, 18, 8, 23, 13, 3, 24, 14, 4, 19, 9
]

def rhoPiShifts : Vector (Fin 64) 25 := #v[
  0, 28, 1, 27, 62, 44, 20, 6, 36, 55, 43, 3, 25, 10, 39, 21, 45, 8, 15, 41, 14, 61, 18, 56, 2
]

def circuit (offset : Fin 64) : FormalCircuit (F p) U64 U64 := {
  elaborated offset with
  Assumptions
  Spec := Spec offset
  soundness := soundness offset
  completeness := completeness offset
}

def Spec (offset : Fin 64) (x : U64 (F p)) (y : U64 (F p)) :=
  y.value = rotRight64 x.value offset.val
  ∧ y.Normalized

def elaborated (off : Fin 64) : ElaboratedCircuit (F p) U64 U64 where
  main := main off
  localLength _ := 16
  output _ i0 := output off i0

def main (offset : Fin 64) (x : Var U64 (F p)) : Circuit (F p) (Var U64 (F p)) := do
  let byte_offset : Fin 8 := ⟨ offset.val / 8, by admit /- proof elided -/
  ⟩
  let bit_offset : Fin 8 := ⟨ offset.val % 8, by admit /- proof elided -/
  ⟩

  
  let byte_rotated ← Rotation64Bytes.circuit byte_offset x
  Rotation64Bits.circuit bit_offset byte_rotated

def circuit (offset : Fin 8) : FormalCircuit (F p) U64 U64 := {
  elaborated offset with
  Assumptions
  Spec := Spec offset
  soundness := soundness offset
  completeness := completeness offset
}

def elaborated (off : Fin 8) : ElaboratedCircuit (F p) U64 U64 where
  main := main off
  localLength _ := 16
  output _ i0 := output off i0
  localLength_eq _ i0 := by admit /- proof elided -/

def output (offset : Fin 8) (i0 : ℕ) : U64 (Expression (F p)) :=
  U64.fromLimbs (.ofFn fun ⟨i,_⟩ =>
    (var ⟨i0 + i*2 + 1⟩) + var ⟨i0 + (i + 1) % 8 * 2⟩ * .const ((2^(8-offset.val) : ℕ) : F p))

def fromLimbs {F} (v : Vector F 8) : U64 F := fromElements v

def main (offset : Fin 8) (x : Var U64 (F p)) : Circuit (F p) (Var U64 (F p)) := do
  let parts ← Circuit.map x.toLimbs (ByteDecomposition.circuit offset)
  let lows := parts.map Outputs.low
  let highs := parts.map Outputs.high

  let rotated := highs.zip (lows.rotate 1) |>.map fun (high, low) =>
    high + low * ((2^(8-offset.val) : ℕ) : F p)

  return U64.fromLimbs rotated

structure Outputs (F : Type) where
  low : F
  high : F

def toLimbs {F} (x : U64 F) : Vector F 8 := toElements x

def circuit (offset : Fin 8) : FormalCircuit (F p) field Outputs := {
  elaborated offset with
  main := main offset
  Assumptions
  Spec := Spec offset
  soundness := soundness offset
  completeness := completeness offset
}

def Spec (offset : Fin 8) (x : F p) (out : Outputs (F p)) :=
  let ⟨low, high⟩ := out
  (low.val = x.val % (2^offset.val) ∧ high.val = x.val / (2^offset.val))
  ∧ (low.val < 2^offset.val ∧ high.val < 2^(8-offset.val))

def main (offset : Fin 8) (x : Expression (F p)) : Circuit (F p) (Var Outputs (F p)) := do
  let low ← witness fun env => mod (env x) (2^offset.val) (by admit /- proof elided -/
  )
  let high ← witness fun env => floorDiv (env x) (2^offset.val)

  lookup ByteTable ((2^(8-offset.val) : F p) * low)
  lookup ByteTable high

  x === low + high * (2^offset.val : F p)

  return { low, high }

def floorDiv (x : F p) (c : ℕ+) : F p :=
  FieldUtils.natToField (x.val / c) (by admit /- proof elided -/
  )

def natToField (n : ℕ) (lt : n < p) : F p :=
  match p with
  | 0 => False.elim (Nat.not_lt_zero n lt)
  | _ + 1 => ⟨ n, lt ⟩

def less_than_p (x : F p) : x.val < p :=

def ByteTable : Table (F p) field := .fromStatic {
  name := "Bytes"
  length := 256

  row i := fromByte i
  index x := x.val

  Spec x := x.val < 256

  contains_iff := by admit /- proof elided -/

def fromByte (x : Fin 256) : F p :=
  FieldUtils.natToField x.val (by admit /- proof elided -/
  )

@[reducible] def field : TypeMap := id

def mod (x : F p) (c : ℕ+) (lt : c < p) : F p :=
  FieldUtils.natToField (x.val % c) (by admit /- proof elided -/
  )

class HasAssertEq (β : Type) (F : outParam Type) [Field F] where
  assert_eq : β → β → Circuit F Unit

def Assumptions (x : F p) := x.val < 256

def elaborated (offset : Fin 8) : ElaboratedCircuit (F p) field Outputs where
  main := main offset
  localLength _ := 2
  output _ i0 := varFromOffset Outputs i0

@[explicit_provable_type]
def varFromOffset (α : TypeMap) [ProvableType α] (offset : ℕ) : Var α F :=
  let vars := Vector.mapRange (size α) fun i => var ⟨offset + i⟩
  fromVars vars

def mapRange (n : ℕ) (create : ℕ → α) : Vector α n :=
  match n with
  | 0 => #v[]
  | k + 1 => mapRange k create |>.push (create k)

def rotate {α : Type} {n : ℕ} (v : Vector α n) (off : ℕ) : Vector α n :=
  ⟨(v.toList.rotate off).toArray, by admit /- proof elided -/
  ⟩

def toLimbs {F} (x : U32 F) : Vector F 4 := toElements x

def Assumptions (input : U64 (F p)) := input.Normalized

def Spec (offset : Fin 8) (x : U64 (F p)) (y : U64 (F p)) :=
  y.value = rotRight64 x.value offset.val
  ∧ y.Normalized

def circuit (off : Fin 8) : FormalCircuit (F p) U64 U64 := {
  elaborated off with
  main := main off
  Assumptions
  Spec := Spec off
  soundness := soundness off
  completeness := completeness off
}

def main (offset : Fin 8) (input : Var U64 (F p)) : Circuit (F p) (Var U64 (F p)) := do
  let ⟨x0, x1, x2, x3 , x4, x5, x6, x7⟩ := input

  if offset = 0 then
    return ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩
  else if offset = 1 then
    return ⟨ x1, x2, x3, x4, x5, x6, x7, x0 ⟩
  else if offset = 2 then
    return ⟨ x2, x3, x4, x5, x6, x7, x0, x1 ⟩
  else if offset = 3 then
    return ⟨ x3, x4, x5, x6, x7, x0, x1, x2 ⟩
  else if offset = 4 then
    return ⟨ x4, x5, x6, x7, x0, x1, x2, x3 ⟩
  else if offset = 5 then
    return ⟨ x5, x6, x7, x0, x1, x2, x3, x4 ⟩
  else if offset = 6 then
    return ⟨ x6, x7, x0, x1, x2, x3, x4, x5 ⟩
  else
    return ⟨ x7, x0, x1, x2, x3, x4, x5, x6 ⟩

instance elaborated (off : Fin 8): ElaboratedCircuit (F p) U64 U64 where
  main := main off
  localLength _ := 0
  output input i0 :=
    let ⟨x0, x1, x2, x3, x4, x5, x6, x7⟩ := input
    match off with
    | 0 => ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩
    | 1 => ⟨ x1, x2, x3, x4, x5, x6, x7, x0 ⟩
    | 2 => ⟨ x2, x3, x4, x5, x6, x7, x0, x1 ⟩
    | 3 => ⟨ x3, x4, x5, x6, x7, x0, x1, x2 ⟩
    | 4 => ⟨ x4, x5, x6, x7, x0, x1, x2, x3 ⟩
    | 5 => ⟨ x5, x6, x7, x0, x1, x2, x3, x4 ⟩
    | 6 => ⟨ x6, x7, x0, x1, x2, x3, x4, x5 ⟩
    | 7 => ⟨ x7, x0, x1, x2, x3, x4, x5, x6 ⟩
  subcircuitsConsistent x i0 := by admit /- proof elided -/

def Spec (offset : Fin 8) (x : U64 (F p)) (y : U64 (F p)) :=
  y.value = rotRight64 x.value (offset.val * 8) ∧ y.Normalized

def output (offset : Fin 64) (i0 : ℕ) : U64 (Expression (F p)) :=
  Rotation64Bits.output ⟨ offset.val % 8, by admit /- proof elided -/
  ⟩ i0

def Spec (state : KeccakState (F p)) (out_state : KeccakState (F p)) :=
  out_state.Normalized
  ∧ out_state.value = Specs.Keccak256.rhoPi state.value

def circuit : FormalCircuit (F p) KeccakState KeccakState :=
 { elaborated with Assumptions, Spec, soundness, completeness }

def Spec (state : KeccakState (F p)) (out_state : KeccakState (F p)) : Prop :=
  out_state.Normalized
  ∧ out_state.value = Specs.Keccak256.theta state.value

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakState where
  main
  localLength _ := 480

def main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) := do
  let c ← ThetaC.circuit state
  let d ← ThetaD.circuit c
  ThetaXor.circuit ⟨state, d⟩

def circuit : FormalCircuit (F p) KeccakRow KeccakRow :=
  { elaborated with Assumptions, Spec, soundness, completeness }

instance elaborated : ElaboratedCircuit (F p) KeccakRow KeccakRow where
  main
  localLength _ := 120

def main (row : Var KeccakRow (F p)) : Circuit (F p) (Var KeccakRow (F p)) := do
  let c0 ← Rotation64.circuit (64 - 1) row[1]
  let c0 ← Xor64.circuit ⟨row[4], c0⟩

  let c1 ← Rotation64.circuit (64 - 1) row[2]
  let c1 ← Xor64.circuit ⟨row[0], c1⟩

  let c2 ← Rotation64.circuit (64 - 1) row[3]
  let c2 ← Xor64.circuit ⟨row[1], c2⟩

  let c3 ← Rotation64.circuit (64 - 1) row[4]
  let c3 ← Xor64.circuit ⟨row[2], c3⟩

  let c4 ← Rotation64.circuit (64 - 1) row[0]
  let c4 ← Xor64.circuit ⟨row[3], c4⟩

  return #v[c0, c1, c2, c3, c4]

@[reducible] def KeccakRow := ProvableVector U64 5

def Spec (row : KeccakRow (F p)) (out : KeccakRow (F p)) : Prop :=
  out.Normalized
  ∧ out.value = Specs.Keccak256.thetaD row.value

def Assumptions (state : KeccakRow (F p)) := state.Normalized

def circuit : FormalCircuit (F p) Inputs KeccakState :=
  { elaborated with Assumptions, Spec, soundness, completeness }

instance elaborated : ElaboratedCircuit (F p) Inputs KeccakState where
  main
  localLength _ := 200

  localLength_eq _ n := by admit /- proof elided -/

def main : Var Inputs (F p) → Circuit (F p) (Var KeccakState (F p))
  | { state, d } => .mapFinRange 25 fun i =>
    Xor64.circuit ⟨state[i.val], d[i.val / 5]⟩

def mapFinRange (m : ℕ) [NeZero m] (body : Fin m → Circuit F β)
    (_constant : ConstantLength body := by admit /- proof elided -/
    ) : Circuit F (Vector β m) :=
  Vector.mapFinRangeM m body

def mapFinRangeM (n : ℕ) {m : Type → Type} [Monad m] (f : Fin n → m β) : m (Vector β n) := (finRange n).mapM f

def Spec (inputs : Inputs (F p)) (out : KeccakState (F p)) : Prop :=
  let ⟨state, d⟩ := inputs
  out.Normalized
  ∧ out.value = Specs.Keccak256.thetaXor state.value d.value

def Assumptions (inputs : Inputs (F p)) : Prop :=
  let ⟨state, d⟩ := inputs
  state.Normalized ∧ d.Normalized

def circuit : FormalCircuit (F p) KeccakState KeccakRow :=
 { elaborated with Assumptions, Spec, soundness, completeness }

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakRow where
  main
  localLength _ := 160
  localLength_eq _ _ := by admit /- proof elided -/

def main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakRow (F p)) :=
  .mapFinRange 5 fun i => do
    let c ← Xor64.circuit ⟨state[5*i.val], state[5*i.val + 1]⟩
    let c ← Xor64.circuit ⟨c, state[5*i.val + 2]⟩
    let c ← Xor64.circuit ⟨c, state[5*i.val + 3]⟩
    let c ← Xor64.circuit ⟨c, state[5*i.val + 4]⟩
    return c

def Spec (state : KeccakState (F p)) (out : KeccakRow (F p)) :=
  out.Normalized
  ∧ out.value = Specs.Keccak256.thetaC state.value

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakState where
  main
  localLength _ := 400
  output _ i0 := Vector.mapRange 25 fun i => varFromOffset U64 (i0 + i*16 + 8)

  localLength_eq state i0 := by admit /- proof elided -/

def main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) :=
  .mapFinRange 25 fun i => do
    let state_not ← Not.circuit (state[i + 5])
    let state_and ← And.And64.circuit ⟨state_not, state[i + 10]⟩
    Xor64.circuit ⟨state[i], state_and⟩

def Spec (input : Inputs (F p)) (z : U64 (F p)) :=
  let ⟨x, y⟩ := input
  z.value = x.value &&& y.value ∧ z.Normalized

def circuit : FormalCircuit (F p) U64 U64 where
  main x := pure (not64_bytewise x)
  Assumptions x := x.Normalized
  Spec x z := z.value = not64 x.value ∧ z.Normalized

  localLength _ := 0
  output x _ := not64_bytewise x

  soundness := by admit /- proof elided -/

def not64_bytewise (x : Var U64 (F p)) : Var U64 (F p) := U64.map x (fun x => 255 - x)

def main (args : List String) : IO Unit := do
  match args with
  | [steps_str, output_path] =>
    
    match steps_str.toNat? with
    | some steps => generateTrace steps output_path
    | none => IO.println "Error: Invalid number of steps"
  | _ =>
    IO.println "Usage: lake lean TraceGen.lean 

def Spec (state : KeccakState (F p)) (out_state : KeccakState (F p)) :=
  out_state.Normalized
  ∧ out_state.value = Specs.Keccak256.chi state.value

def stateVar (n : ℕ) (i : ℕ) : Var KeccakState (F p) :=
  Vector.mapRange 25 (fun j => varFromOffset U64 (n + i * 1288 + j * 16 + 888))
  |>.set 0 (varFromOffset U64 (n + i * 1288 + 1280))

instance ExplicitCircuits.from_pure {f : α → β} : ExplicitCircuits (fun a => pure (f a) : α → Circuit F β) where
  output a _ := f a
  localLength _ _ := 0
  operations _ _ := []

def KeccakBlock.normalized : FormalAssertion (F p) KeccakBlock where
  main block := .forEach block (assertion U64.AssertNormalized.circuit)
  Assumptions _ := True
  Spec block := block.Normalized
  localLength_eq _ _ := by admit /- proof elided -/

def circuit : FormalAssertion (F p) U64 where
  main

  Assumptions _ := True
  Spec inputs := inputs.Normalized

  soundness := by admit /- proof elided -/

def main (inputs : Var U64 (F p)) : Circuit (F p) Unit  := do
  let ⟨x0, x1, x2, x3, x4, x5, x6, x7⟩ := inputs
  lookup ByteTable x0
  lookup ByteTable x1
  lookup ByteTable x2
  lookup ByteTable x3
  lookup ByteTable x4
  lookup ByteTable x5
  lookup ByteTable x6
  lookup ByteTable x7

@[circuit_norm]
def assertion (circuit : FormalAssertion F β) (b : Var β F) : Circuit F Unit :=
  fun offset =>
    let subcircuit := circuit.toSubcircuit offset b
    ((), [.subcircuit subcircuit])

def absorbBlocks (blocks : List (Vector ℕ RATE)) : Vector ℕ 25 :=
  blocks.foldl absorbBlock initialState

def initialState : Vector ℕ 25 := .fill 25 0

def foldl {m : ℕ} [Inhabited β] [Inhabited α] (xs : Vector α m) (init : β) (body : β → α → Circuit F β)
  (_const_out : ConstantOutput (fun (s, a) => body s a) := by admit /- proof elided -/
    )
  (_constant : ConstantLength (fun (s, a) => body s a) := by admit /- proof elided -/
  )
   : Circuit F β :=
  xs.foldlM body init

@[circuit_norm]
def ConstantOutput (circuit : α → Circuit F β) [Inhabited α] :=
  ∀ (x : α) (n : ℕ), (circuit x).output n = (circuit default).output n

def InductiveTable.Soundness (F : Type) [Field F] (State Input : Type → Type) [ProvableType State] [ProvableType Input]
    (Spec : (initialState : State F) → (xs : List (Input F)) → (i : ℕ) → (xs.length = i) → (currentState : State F) → Prop)
    (step : Var State F → Var Input F → Circuit F (Var State F)) :=
  ∀ (initialState : State F) (row_index : ℕ) (env : Environment F),
  
  ∀ (acc_var : Var State F) (x_var : Var Input F)
    (acc : State F) (x : Input F) (xs : List (Input F)) (xs_len : xs.length = row_index),
      (eval env acc_var = acc) ∧ (eval env x_var = x) →
    
    Circuit.ConstraintsHold.Soundness env (step acc_var x_var |>.operations ((size State) + (size Input))) →
    
    Spec initialState xs row_index xs_len acc →
    
    Spec initialState (xs.concat x) (row_index + 1) (xs_len ▸ List.length_concat) (eval env (step acc_var x_var |>.output ((size State) + (size Input))))

def fromByte (x : Fin 256) : U64 (F p) :=
  ⟨ x.val, 0, 0, 0, 0, 0, 0, 0 ⟩

def traceInputs {N : ℕ} (trace : TraceOfLength F (ProvablePair State Input) N) : List (Input F) :=
  trace.val.toList.map Prod.snd

def toList : Operations F → List (Operation F) := id

def toList : Trace F S → List (Row F S)
  | <+> => []
  | rest +> row => rest.toList.concat row

inductive Trace (F : Type) (S : Type → Type) [ProvableType S] where
   
  | empty : Trace F S
   
  | cons (rest : Trace F S) (row : Row F S) : Trace F S

structure CellOffset (W : ℕ+) (S : Type → Type) [ProvableType S]  where
  row: Fin W
  column: Fin (size S)

@[reducible, table_norm, table_assignment_norm]
def empty : TableContext W S F where
  circuit := []
  assignment := .empty W

structure TableContext (W : ℕ+) (S : Type → Type) (F : Type) [Field F] [ProvableType S] where
  circuit : Operations F
  assignment : CellAssignment W S
deriving Repr

structure CellAssignment (W : ℕ+) (S : Type → Type) [ProvableType S] where
  offset : ℕ 
  aux_length : ℕ 

   
  vars : Vector (Cell W S) offset

@[reducible, table_norm, table_assignment_norm]
def offset (table : TableContext W S F) : ℕ := table.circuit.localLength

inductive Cell (W : ℕ+) (S : Type → Type) [ProvableType S] where
  | input : CellOffset W S → Cell W S
  | aux : ℕ → Cell W S

@[reducible]
def Row (F : Type) (S : Type → Type) [ProvableType S] := S F

instance ProvablePair.instance {α β: TypeMap} [ProvableType α] [ProvableType β] : ProvableType (ProvablePair α β) where
  size := size α + size β
  toElements := fun (a, b) => toElements a ++ toElements b
  fromElements {F} v :=
    let a : α F := v.take (size α) |>.cast Nat.min_add_right_self |> fromElements
    let b : β F := v.drop (size α) |>.cast (Nat.add_sub_self_left _ _) |> fromElements
    (a, b)
  fromElements_toElements x := by admit /- proof elided -/

def TraceOfLength (F : Type) (S : Type → Type) [ProvableType S] (N : ℕ) : Type :=
  { env : Trace F S // env.len = N }

def toList {N : ℕ} (trace : TraceOfLength F S N) : List.Vector (Row F S) N :=
  ⟨ trace.val.toList, by admit /- proof elided -/
  ⟩

def FormalTable.statement (table : FormalTable F S) (N : ℕ) (trace : TraceOfLength F S N) : Prop :=
  table.Assumption N → table.Spec trace

structure FormalTable (F : Type) [Field F] (S : Type → Type) [ProvableType S] where
   
  constraints : List (TableOperation S F)

   
  Assumption : ℕ → Prop := fun _ => True

   
  Spec {N : ℕ} : TraceOfLength F S N → Prop

   
  soundness :
    ∀ (N : ℕ) (trace : TraceOfLength F S N) (env : ℕ → ℕ → Environment F),
    Assumption N →
    TableConstraintsHold constraints trace env →
    Spec trace

   
  offset_consistent :
    constraints.Forall fun cs =>
      match cs with
      | .boundary _ constraint => constraint.OffsetConsistent
      | .everyRow constraint => constraint.OffsetConsistent
      | .everyRowExceptLast constraint => constraint.OffsetConsistent
    := by admit /- proof elided -/

def tail : Trace F S → Trace F S
  | <+>  => <+>
  | rest +> _ => rest

def tail {M : ℕ} (trace : TraceOfLength F S M) : TraceOfLength F S (M - 1) :=
  ⟨ trace.val.tail, by admit /- proof elided -/
  ⟩

def toFormal (table : InductiveTable F State Input) (input output : State F) : FormalTable F (ProvablePair State Input) where
  constraints := table.tableConstraints input output
  Assumption N := N > 0 ∧ table.Spec input [] 0 rfl input
  Spec {N} trace := table.Spec input (traceInputs trace.tail) (N-1) (traceInputs_length trace.tail) output

  soundness N trace env assumption constraints :=
    table.table_soundness input output ⟨N, assumption.left⟩ trace env assumption.right constraints

  offset_consistent := by admit /- proof elided -/

def equalityConstraint (Input : TypeMap) [ProvableType Input] (target : State F) : SingleRowConstraint (ProvablePair State Input) F := do
  let (actual, _) ← getCurrRow
  actual === (const target)

@[table_norm, table_assignment_norm]
def getCurrRow : TableConstraint W S F (Var S F) := getRow 0

@[reducible, table_norm, table_assignment_norm]
def TableConstraint (W : ℕ+) (S : Type → Type) (F : Type) [Field F] [ProvableType S] :=
  StateM (TableContext W S F)

@[table_norm, table_assignment_norm]
def getRow (row : Fin W) : TableConstraint W S F (Var S F) :=
  modifyGet fun ctx =>
    let ctx' : TableContext W S F := {
      circuit := ctx.circuit ++ [.witness (size S) fun env => .mapRange _ fun i => env.get (ctx.offset + i)],
      assignment := ctx.assignment.pushRow row
    }
    (varFromOffset S ctx.offset, ctx')

@[table_norm, table_assignment_norm]
def Row.get (row : Row F S) (i : Fin (size S)) : F :=
  (toElements row)[i.val]

@[table_assignment_norm]
def pushRow (assignment : CellAssignment W S) (row : Fin W) : CellAssignment W S :=
  let row_vars : Vector (Cell W S) (size S) := .mapFinRange _ fun col => .input ⟨ row, col ⟩
  {
    offset := assignment.offset + size S
    aux_length := assignment.aux_length
    vars := assignment.vars ++ row_vars
  }

@[table_assignment_norm]
def get {M : ℕ} :
    (env : TraceOfLength F S M) → (i : Fin M) → (j : Fin (size S)) → F
  | ⟨env, h⟩, i, j => env.getLeFromBottom ⟨
      M - 1 - i,
      by admit /- proof elided -/
    ⟩ j

@[reducible]
def SingleRowConstraint (S : Type → Type) (F : Type) [Field F] [ProvableType S] := TableConstraint 1 S F Unit

def inductiveConstraint (table : InductiveTable F State Input) : TableConstraint 2 (ProvablePair State Input) F Unit := do
  let (acc, x) ← getCurrRow
  let output ← table.step acc x
  let (output', _) ← getNextRow
  
  output' === output

@[table_norm, table_assignment_norm]
def getNextRow : TableConstraint W S F (Var S F) := getRow 1

def tableConstraints (table : InductiveTable F State Input) (input_state output_state : State F) :
  List (TableOperation (ProvablePair State Input) F) := [
    .everyRowExceptLast table.inductiveConstraint,
    .boundary (.fromStart 0) (equalityConstraint Input input_state),
    .boundary (.fromEnd 0) (equalityConstraint Input output_state),
  ]

inductive TableOperation (S : Type → Type) (F : Type) [Field F] [ProvableType S] where
   
  | boundary: RowIndex → SingleRowConstraint S F → TableOperation S F

   
  | everyRow: SingleRowConstraint S F → TableOperation S F

   
  | everyRowExceptLast: TwoRowsConstraint S F → TableOperation S F

inductive RowIndex where
  | fromStart : ℕ → RowIndex
  | fromEnd : ℕ → RowIndex

@[reducible]
def TwoRowsConstraint (S : Type → Type) (F : Type) [Field F] [ProvableType S] := TableConstraint 2 S F Unit

@[table_norm]
def TableConstraintsHold {N : ℕ} (constraints : List (TableOperation S F))
  (trace : TraceOfLength F S N) (env : ℕ → ℕ → Environment F) : Prop :=
  let constraints_and_envs := constraints.mapIdx (fun i cs => (cs, env i))
  foldl N constraints_and_envs trace.val constraints_and_envs
  where

@[table_assignment_norm]
def OffsetConsistent (table : TableConstraint W S F α) : Prop :=
  table.finalOffset = table.finalAssignment.offset

@[reducible, table_norm, table_assignment_norm]
def finalOffset (table : TableConstraint W S F α) : ℕ :=
  table .empty |>.snd.circuit.localLength

@[table_assignment_norm]
def finalAssignment (table : TableConstraint W S F α) : CellAssignment W S :=
  table .empty |>.snd.assignment

def fill (n : ℕ) (a : α) : Vector α n :=
  match n with
  | 0 => #v[]
  | k + 1 => (fill k a).push a

@[table_norm, table_assignment_norm]
def len : Trace F S → ℕ
  | <+> => 0
  | rest +> _ => rest.len + 1

infix:50 " === " => HasAssertEq.assert_eq

@[inherit_doc] notation:67 "<+>" => Trace.empty

@[inherit_doc] infixl:67 " +> " => Trace.cons
</used_repo_defs>

<lib_lemmas>
Fin.val_zero in Init.Data.Fin.Lemmas
Vector.getElem_map in Init.Data.Vector.Lemmas
List.length_map in Init.Data.List.Lemmas
true_and in Init.SimpLemmas
</lib_lemmas>

<repo_lemmas>
lemma fromByte_value {x : Fin 256} : (fromByte x).value (p:=p) = x

theorem getElem_fill {n} {a : α} {i : ℕ} {hi : i < n} :
    (fill n a)[i] = a

lemma fromByte_normalized {x : Fin 256} : (fromByte x).Normalized (p:=p)

lemma toList_length : (trace : Trace F S) → trace.toList.length = trace.len
  | <+> => rfl
</repo_lemmas>

<local_ctx>
import Clean.Table.Inductive

import Clean.Circuit.Extensions

import Clean.Gadgets.Keccak.AbsorbBlock

import Clean.Specs.Keccak256

open Specs.Keccak256

variable {p : ℕ} [Fact p.Prime] [Fact (p > 2 ^ 16 + 2 ^ 8)]

namespace Tables.KeccakInductive

open Gadgets.Keccak256

def table : InductiveTable (F p) KeccakState KeccakBlock where
  step state block := do
    KeccakBlock.normalized block
    AbsorbBlock.circuit { state, block }

  Spec _ blocks i _ state : Prop :=
    state.Normalized
    ∧ state.value = absorbBlocks (blocks.map KeccakBlock.value)

  InputAssumptions i block := block.Normalized

  soundness := by admit /- proof elided -/

def initialState : KeccakState (F p) := .fill 25 (U64.fromByte 0)

def formalTable (output : KeccakState (F p)) := table.toFormal initialState output
</local_ctx>

<target_theorem>
theorem tableStatement (output : KeccakState (F p)) : ∀ n > 0, ∀ trace, ∃ blocks, blocks.length = n - 1 ∧
  (formalTable output).statement n trace →
    output.Normalized ∧ output.value = absorbBlocks blocks :=
</target_theorem>

