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:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <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 available definitions and lemmas (all_available_defs, all_available_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:
<all_available_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)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_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:
<all_available_defs>
def cons (a : α) (v : Vector α n) : Vector α (n + 1) :=
  ⟨ .mk (a :: v.toList), by admit /- proof elided -/
  ⟩

def induct {motive : {n : ℕ} → Vector α n → Sort u}
    (nil : motive #v[])
    (cons: ∀ {n : ℕ} (a : α) (as : Vector α n), motive as → motive (cons a as))
    {n : ℕ} (v : Vector α n) : motive v :=
  match v with
  | ⟨ .mk [], h ⟩ => by admit /- proof elided -/
  | ⟨ .mk (a :: as), h ⟩ => by admit /- proof elided -/

@[reducible]
def TypeMap := Type → Type

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

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

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 Lookup (F : Type) where
  table : RawTable F
  entry : Vector (Expression F) table.arity

@[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 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

structure Variable (F : Type) where
  index : ℕ

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 Environment (F : Type) where
  get : ℕ → F

@[reducible]
def TypeMap := Type → Type

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

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

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

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

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

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

@[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 }])

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 -/

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 -/

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

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

@[reducible]
def TypeMap := Type → Type

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

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

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

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 -/

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

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

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

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

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

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

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

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

@[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

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

def testChunk65 : List ℕ := List.range 65

localLength _ := n

Add in Init.Prelude

instance : Fact (p > 512) := .mk (by admit /- proof elided -/
)

IO.FS.writeFile output_path json_data.pretty
  IO.println s!"Generated trace with {steps} steps -> {output_path}"

| everyRowExceptLast: TwoRowsConstraint S F → TableOperation S F

instance (T : Type) [Inhabited T] : Inhabited (U32 T) where
  default := ⟨ default, default, default, default ⟩

imply_soundness := by admit /- proof elided -/

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

def Spec (offset : Fin 32) (x : U32 (F p)) (y : U32 (F p)) :=
  y.value = rotRight32 x.value offset.val
  ∧ y.Normalized

instance [Repr F] : Repr (Operation F) where
  reprPrec op _ := match op with
    | witness m _ => "(Witness " ++ reprStr m ++ ")"
    | assert e => "(Assert " ++ reprStr e ++ " == 0)"
    | lookup l => reprStr l
    | subcircuit { ops, .. } => "(Subcircuit " ++ reprStr ops ++ ")"

Nat.reduceGT in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

def Addition8Full.circuit : FormalCircuit (F p) Addition8FullCarry.Inputs field where
  main := fun inputs => do
    let { z, .. } ← Addition8FullCarry.circuit inputs
    return z

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

def formalTable (output : Row (F p)) := table.toFormal { x := U32.fromByte 0, y := U32.fromByte 1 } output

Circuit.forEach bits assertBool

instance elaborated (off : Fin 4): ElaboratedCircuit (F p) U32 U32 where
  main := main off
  localLength _ := 0
  output input i0 :=
    let ⟨x0, x1, x2, x3⟩ := input
    match off with
    | 0 => ⟨ x0, x1, x2, x3 ⟩
    | 1 => ⟨ x1, x2, x3, x0 ⟩
    | 2 => ⟨ x2, x3, x0, x1 ⟩
    | 3 => ⟨ x3, x0, x1, x2 ⟩

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 Spec (input : Inputs (F p)) (z : F p) :=
  let ⟨x, y⟩ := input
  z.val = x.val &&& y.val

Lean.MonadLCtx in Lean.LocalContext

def Environment.UsesLocalWitnessesFlat (env : Environment F) (n : ℕ) (ops : List (FlatOperation F)) : Prop :=
  FlatOperation.forAll n { witness n _ compute := env.ExtendsVector (compute env) n } ops

def circuit (n : ℕ) (hn : 2^(n+1) < p) : FormalCircuit (F p) fieldPair field where
  main := fun (x, y) =>
    LessThan.circuit n hn (y, x + 1)

Vector.cast in Init.Data.Vector.Basic

instance : ProvableStruct TestInputs where
  components := [field, field, field]
  toComponents := fun { x, y, z } => .cons x (.cons y (.cons z .nil))
  fromComponents := fun (.cons x (.cons y (.cons z .nil))) => { x, y, z }

Lean.Elab.Tactic.elabTermWithHoles in Lean.Elab.Tactic.ElabTerm

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
  ]

let (lout, _) ← Circuit.foldlRange n ((0 : Expression (F p)), (1 : Expression (F p))) fun (lout, e2) i => do
    
    out[i] * (out[i] - (1 : Expression (F p))) === (0 : Expression (F p))
    let lout := lout + out[i] * e2
    return (lout, e2 + e2)

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

Fin in Init.Prelude

def applyTwoRounds (state : Vector ℕ 16) (message : Vector ℕ 16) : Vector ℕ 16 × Vector ℕ 16 :=
  let state1 := round state message
  let msg1 := permute message
  let state2 := round state1 msg1
  let msg2 := permute msg1
  (state2, msg2)

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

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 : ProvableType DecodedInstructionType where
  size := 4
  toElements := fun { isAdd, isMul, isStoreState, isLoadState } => #v[isAdd, isMul, isStoreState, isLoadState]
  fromElements := fun elements => {
    isAdd := elements[0],
    isMul := elements[1],
    isStoreState := elements[2],
    isLoadState := elements[3]
  }

instance : NonEmptyProvableType fieldTriple where

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

def generateFieldBasedNames (baseName : Name) (fieldNames : Array Name) : Array Name :=
  fieldNames.map fun fieldName => baseName.appendAfter s!"_{fieldName}"

instance : ExplicitCircuits (F:=F) witnessVar where
  output _ n := ⟨ n ⟩
  localLength _ _ := 1
  operations c n := [.witness 1 fun env => #v[c env]]

let out <== c.map fun ci =>
    let a210 := (ci[7] - ci[6] - ci[5] + ci[4] - ci[3] + ci[2] + ci[1] - ci[0]) * s10
    let a21 := (ci[6] - ci[4] - ci[2] + ci[0]) * s[1]
    let a20 := (ci[5] - ci[4] - ci[1] + ci[0]) * s[0]
    let a2 := (ci[4] - ci[0])

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

def main (input : Var Inputs (F p)) : Circuit (F p) (Var U32 (F p))  := do
  let ⟨x, y⟩ := input

soundness : InductiveTable.Soundness F State Input Spec step

def floorDiv256 (x : F p) : F p := floorDiv x 256

combinedSize : ℕ := combinedSize' components
  combinedSize_eq : combinedSize = combinedSize' components := by admit /- proof elided -/

structure BlockInput (F : Type) where
  block_exists : F                      
  block_data : Vector (U32 F) 16

def Spec [DecidableEq F] (input : Inputs M F) (output : M F) : Prop :=
  output = if input.selector = 1 then input.ifTrue else input.ifFalse

instance {α : TypeMap} [ProvableType α] : Zero (α F) where
  zero := fromElements (Vector.replicate _ 0)

def sevenRoundsApplyStyle : FormalCircuit (F p) Round.Inputs BLAKE3State :=
  sevenRoundsFinal.weakenSpec SevenRoundsSpec (by admit /- proof elided -/
  )

@[table_assignment_norm]
def curr {W : ℕ+} (j : Fin (size S)) : CellOffset W S := ⟨0, j⟩

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

inductive Boolean (F : Type) where
  | private mk : Variable F → Boolean F

@[table_norm]
def lastRow {M : ℕ+} (trace : TraceOfLength F S M) : S F :=
  trace.val.lastRow (by admit /- proof elided -/
  )

return { low, high }

def formalFib32Table : FormalTable (F p) RowType := {
  constraints := fib32Table,
  Spec := Spec,

Prod.snd in Init.Prelude

def circuit : FormalAssertion (F p) U32 where
  main
  Assumptions _ := True
  Spec inputs := inputs.Normalized

InputAssumptions i block := block.Normalized

def circuit (n : ℕ) (hn : 2^n < p) : FormalCircuit (F p) field (fields n) where
  main := main n
  localLength _ := n + 2 
  localLength_eq := by admit /- proof elided -/

instance : ProvableStruct Inputs where
  components := [U32, U32]
  toComponents := fun { x, y } => .cons x (.cons y .nil)
  fromComponents := fun (.cons x (.cons y .nil)) => { x, y }

instance : Repr (CellOffset W S) where
  reprPrec off _ := "⟨" ++ reprStr off.row ++ ", " ++ reprStr off.column ++ "⟩"

instance : ProvableType U64 where
  size := 8
  toElements x := #v[x.x0, x.x1, x.x2, x.x3, x.x4, x.x5, x.x6, x.x7]
  fromElements v :=
    let ⟨.mk [v0, v1, v2, v3, v4, v5, v6, v7], _⟩ := v
    ⟨ v0, v1, v2, v3, v4, v5, v6, v7 ⟩

nextStateCircuit { state, decoded, v1, v2, v3 }
    localLength := 30

@[circuit_norm]
def witnessVector (m : ℕ) (compute : Environment F → Vector F m) : Circuit F (Vector (Expression F) m) :=
  fun (offset : ℕ) =>
    let vars := varFromOffset (fields m) offset
    (vars, [.witness m compute])

instance (p : ℕ) : CommRing (F p) := ZMod.commRing p

def Operations.ComputableWitnesses (ops : Operations F) (n : ℕ) (env env' : Environment F) : Prop :=
  ops.forAllFlat n { witness n _ compute := env.AgreesBelow n env' → compute env = compute env' }

let state_a ← Addition32.circuit ⟨state_a, ← Addition32.circuit ⟨state_b, y⟩⟩

def generateStructFieldNames (fvarId : FVarId) : MetaM AltVarNames := do
  let localDecl ← fvarId.getDecl
  let userName := localDecl.userName

List.filter in Init.Data.List.Basic

instance {m : ℕ} (α : TypeMap) [NonEmptyProvableType α] :
    Witnessable F (ProvableVector α m) (Var (ProvableVector α m)) where
  witness := ProvableVector.witness m

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

Std.HashMap.emptyWithCapacity in Std.Data.HashMap.Basic

let rawInstrType : Expression _ ← witness fun eval => program <| Fin.ofNat _ (eval pc).val
    let op1 ← witness fun eval => program <| Fin.ofNat _ (eval (pc + 1)).val
    let op2 ← witness fun eval => program <| Fin.ofNat _ (eval (pc + 2)).val
    let op3 ← witness fun eval => program <| Fin.ofNat _ (eval (pc + 3)).val

def circuit : FormalAssertion (F p) BlockInput where
  main
  localLength_eq := by admit /- proof elided -/

UInt64.toNat in Init.Data.UInt.BasicAux

Assumptions := fun { enabled, inp } =>
    enabled = 0 ∨ enabled = 1

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

instance [Repr F] : Repr (Lookup F) where
  reprPrec l _ := "(Lookup " ++ l.table.name ++ " " ++ repr l.entry ++ ")"

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

def Spec (offset : Fin 4) (x : U32 (F p)) (y : U32 (F p)) :=
  y.value = rotRight32 x.value (offset.val * 8) ∧ y.Normalized

def circuit (n r : ℕ) [NeZero n] : FormalCircuit (F p) (fields n) (fields n) where
  main := main n r

def takeShort {α : Type} {n : ℕ} (v : Vector α n) (j : ℕ) (h_j : j < n) : Vector α j :=
  (v.take j).cast (by admit /- proof elided -/
  )

UInt32.reduceToNat in Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt

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

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

Vector.foldlM in Init.Data.Vector.Basic

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

def FlatOperation.dynamicWitnesses (ops : List (FlatOperation F)) (init : List F) : List F :=
  ops.foldl (fun (acc : List F) (op : FlatOperation F) =>
    acc ++ op.dynamicWitness acc
  ) init

def hasFieldInstance (type : Expr) : MetaM Bool := do
  let fieldClass ← mkAppM ``Field #[type]
  match ← trySynthInstance fieldClass with
  | .some _ => return true
  | _ => return false

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

soundness := by admit /- proof elided -/

instance elaborated : ElaboratedCircuit (F p) Inputs field where
  main
  localLength _ := 1
  output _ i := var ⟨i⟩

def Condition.applyFlat (condition : Condition F) (offset : ℕ) : FlatOperation F → Prop
  | .witness m c => condition.witness offset m c
  | .assert e => condition.assert offset e
  | .lookup l => condition.lookup offset l

instance : HDiv (Expression F) F (Expression F) where
  hDiv e f := mul (f⁻¹ : F) e

localLength _ := 4
  Assumptions
  | pc => pc.val + 3 < programSize

instance {n : ℕ} [OfNat F n] : OfNat (field F) n where
  ofNat : F := OfNat.ofNat n

@[circuit_norm]
def lookupCircuit (circuit : LookupCircuit F α β) : FormalCircuit F α β where
  main (input : Var α F) := do
    
    let output ← witness fun env => circuit.constantOutput (eval env input)

@[table_norm]
def operations (table : TableConstraint W S F α) : Operations F :=
  table .empty |>.snd.circuit

def main (input : Var Inputs (F p)) : Circuit (F p) (fieldVar (F p)) := do
  let ⟨x, y⟩ := input
  let and ← witness fun eval => (eval x).val &&& (eval y).val
  
  let xor := x + y - 2*and
  lookup ByteXorTable (x, y, xor)
  return and

Inv in Init.Prelude

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

return nextState

def femtoCairoFormalTable
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p)
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p)) (h_memorySize : memorySize < p)
    (output : State (F p)) := (femtoCairoTable program h_programSize memory h_memorySize).toFormal {
  pc := 0,
  ap := 0,
  fp := 0
} output

soundness := by admit /- proof elided -/

return out

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

And in Init.Prelude

def ByteLessThanTwoPower (two_exponent : Fin 9) : Table (F p) field := .fromStatic {
  name := "ByteLessThanTwoPower"
  length := 2^two_exponent.val

return state
    |>.set a state_a
    |>.set b state_b
    |>.set c state_c
    |>.set d state_d

def circuit : FormalCircuit (F p) fieldPair field where
  main
  localLength _ := 1
  localLength_eq := by admit /- proof elided -/

def U32.witness (compute : Environment (F p) → U32 (F p)) := do
  let x ← ProvableType.witness compute
  U32.AssertNormalized.circuit x
  return x

def counter : ℕ := 953581910

instance elaborated: ElaboratedCircuit (F p) BLAKE3State BLAKE3State where
  main := main
  localLength _ := 0
  output state i0 := Vector.ofFn (fun i => state[msgPermutation[i]])

Int in Init.Data.Int.Basic

instance : Fact (p > 512) := .mk (by admit /- proof elided -/
)

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 ⟩

instance : HSub (field (Expression F)) (field (Expression F)) (field (Expression F)) where
  hSub (a : Expression F) (b : Expression F) := a - b

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))

let (instr_type, mode1, mode2, mode3) ← decodeInstruction rawInstrType

def m : Vector ℕ 16 := #v[3959934058, 3329161910, 3688806782, 3025089236, 897128991, 1111177342, 4132823147, 2420086736, 1951041921, 2483382132, 1478626316, 2397174491, 1858261849, 1494602388, 4275385857, 3719915132]
example : round stateInitRound m = #v[2183394319, 368400627, 2705018986, 1532359963, 184541119, 4093912516, 344508834, 154001542, 2580533130, 866577463, 1629990543, 2086044263, 618301763, 3154665623, 3243728413, 699478374] := rfl

def synthesizeConstVar : Var α F :=
  let zeros := Vector.fill (size α) 0
  fromVars (zeros.map .const)

def fib32 : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => (fib32 n + fib32 (n + 1)) % 2^32

@[circuit_norm]
def localWitnesses (env : Environment F) : (ops : Operations F) → Vector F ops.localLength
  | [] => #v[]
  | .witness _ c :: ops => c env ++ localWitnesses env ops
  | .assert _ :: ops => localWitnesses env ops
  | .lookup _ :: ops => localWitnesses env ops
  | .subcircuit s :: ops => s.witnesses env ++ localWitnesses env ops

def circuit : FormalAssertion (F p) (fields 254) where
  main
  localLength _ := 127 + 1 + 135 + 1

List.insertionSort in Mathlib.Data.List.Sort

Option in Init.Prelude

def Assumptions (n : ℕ) (input : fields n (F p)) : Prop :=
  ∀ (i : ℕ) (h : i < n), IsBool input[i]

def splitProvableStructEq : TacticM Unit := do
  withMainContext do
    
    let varsToCase ← findStructVarsInEqualities

instance {α : TypeMap} [ProvableType α] : ExplicitCircuits (ProvableType.witness (α:=α) (F:=F)) where
  output _ n := varFromOffset α n
  localLength _ _ := size α
  operations c n := [.witness (size α) (toElements ∘ c)]

def FormalCircuit.weakenSpec
    {F : Type} [Field F]
    {Input Output : TypeMap} [ProvableType Input] [ProvableType Output]
    (circuit : FormalCircuit F Input Output)
    (WeakerSpec : Input F → Output F → Prop)
    (h_spec_implication : ∀ input output,
      circuit.Assumptions input →
      circuit.Spec input output →
      WeakerSpec input output) :
    FormalCircuit F Input Output := {
  elaborated := circuit.elaborated
  Assumptions := circuit.Assumptions
  Spec := WeakerSpec
  soundness := by admit /- proof elided -/

def valueU32 (x : U32 (F p)) (h : x.Normalized) : UInt32 :=
  UInt32.ofNatLT x.value (value_lt_of_normalized h)

UInt32.ofNatLT in Init.Prelude

def IsBool {α : Type*} [Zero α] [One α] (x : α) : Prop := x = 0 ∨ x = 1

Finset.univ in Mathlib.Data.Fintype.Defs

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

def rotLeft8 (x : Fin 256) (offset : Fin 8) : Fin 256 :=
  let low := x % (2^(8-offset.val))
  let high := x / (2^(8-offset.val))
  low * (2^offset.val) + high

def main (input : Var Inputs (F p)) := do
  let { c, s } := input

def bytesToWords {F} (bytes : Vector F 64) : Vector (U32 F) 16 :=
  Vector.ofFn fun (i : Fin 16) =>
    let base := i.val*4
    U32.mk
      bytes[base]
      bytes[base + 1]
      bytes[base + 2]
      bytes[base + 3]

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

def testBlock64 : List ℕ := List.range 64

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

def FlatOperation.dynamicWitness (op : FlatOperation F) (acc : List F) : List F := match op with
  | .witness _ compute => (compute (.fromList acc)).toList
  | .assert _ => []
  | .lookup _ => []

instance : ProvableType RowType where
  size := 3
  toElements x := #v[x.x, x.y, x.z]
  fromElements v :=
    let ⟨ .mk [x, y, z], _ ⟩ := v
    ⟨ x, y, z ⟩

def main (n : ℕ) [NeZero n] (inp : BinSubInput n (Expression (F p))) := do
  
  let lin := Fin.foldl n (fun lin i =>
      let e2 : Expression (F p) := (2^i.val : F p)
      lin + inp[0][i] * e2 - inp[1][i] * e2)
    (2^n : F p)

instance [Field F] : Inhabited F where
  default := 0

Spec | { x, y }, z => z.val = (x.val + y.val) % 256

structure Inputs (F : Type) where
  c : Vector F 8  
  s : Vector F 3

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

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

Array.mapM in Init.Data.Array.Basic

def ProcessBlocksState.toChunkState (state : ProcessBlocksState (F p)) : ChunkState :=
  { chaining_value := state.chaining_value.map (·.value)
  , chunk_counter := state.chunk_counter.value
  , blocks_compressed := state.blocks_compressed.value
  , block_buffer := []  
  }

def formalAdd8Table : FormalTable (F p) RowType := {
  constraints := add8Table,
  Spec := Spec_add8,
  soundness := by admit /- proof elided -/

@[table_norm]
def ForAllRowsOfTraceExceptLast {N : ℕ}
    (trace : TraceOfLength F S N) (prop : Row F S → Prop) : Prop :=
  inner trace.val prop
  where
  inner : Trace F S → (Row F S → Prop) → Prop
    | <+>, _ => true
    | <+> +> _, _ => true
    | rest +> curr +> _, prop => prop curr ∧ inner (rest +> curr) prop

@[reducible] def CAPACITY := 8

instance : Repr (CellAssignment W S) where
  reprPrec := fun { offset, aux_length, vars } _ =>
    "{ offset := " ++ reprStr offset ++ ", aux_length := " ++ reprStr aux_length ++ ", vars := " ++ reprStr vars ++ "}"

let v1 ← subcircuitWithAssertion (readFromMemoryCircuit memory h_memorySize) { state, offset := op1, mode := decoded.mode1 }
      let v2 ← subcircuitWithAssertion (readFromMemoryCircuit memory h_memorySize) { state, offset := op2, mode := decoded.mode2 }
      let v3 ← subcircuitWithAssertion (readFromMemoryCircuit memory h_memorySize) { state, offset := op3, mode := decoded.mode3 }

LawfulMonad in Init.Control.Lawful.Basic

Lean.ToJson in Lean.Data.Json.FromToJson.Basic

instance elaborated : ElaboratedCircuit (F p) Inputs BLAKE3State where
  main := main
  localLength _ := 64
  output inputs i0 := #v[
    varFromOffset U32 (i0 + 0),
    varFromOffset U32 (i0 + 4),
    varFromOffset U32 (i0 + 8),
    varFromOffset U32 (i0 + 12),
    varFromOffset U32 (i0 + 16),
    varFromOffset U32 (i0 + 20),
    varFromOffset U32 (i0 + 24),
    varFromOffset U32 (i0 + 28),
    varFromOffset U32 (i0 + 32),
    varFromOffset U32 (i0 + 36),
    varFromOffset U32 (i0 + 40),
    varFromOffset U32 (i0 + 44),
    varFromOffset U32 (i0 + 48),
    varFromOffset U32 (i0 + 52),
    varFromOffset U32 (i0 + 56),
    varFromOffset U32 (i0 + 60)
  ]

List in Init.Prelude

Spec
  | pc, output =>
    match Spec.fetchInstruction program pc with
      | some claimed_output => output = claimed_output
      | none => False 
  soundness := by admit /- proof elided -/

Id.run in Init.Control.Id

UInt64.ofNatLT in Init.Prelude

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

Coe in Init.Coe

let ctx ← getLCtx
      for localDecl in ctx do
        if localDecl.isImplementationDetail then
          continue

instance {α : Type*} [Zero α] [One α] [DecidableEq α] {x : α} : Decidable (IsBool x) :=
  inferInstanceAs (Decidable (x = 0 ∨ x = 1))

def Assumptions (input : ApplyRounds.Inputs (F p)) : Prop :=
  ApplyRounds.Assumptions input

CoeFun in Init.Coe

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

@[table_assignment_norm]
def assignmentFromCircuit (as : CellAssignment W S) : Operations F → CellAssignment W S
  | [] => as
  | .witness m _ :: ops => assignmentFromCircuit (as.pushVarsAux m) ops
  | .assert _ :: ops => assignmentFromCircuit as ops
  | .lookup _ :: ops => assignmentFromCircuit as ops
  | .subcircuit s :: ops => assignmentFromCircuit (as.pushVarsAux s.localLength) ops

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

abbrev timestamp_ordering (x y : MemoryAccess) := match x, y with
| (t2, _a2, _r2, _w2), (t1, _a1, _r1, _w1) => t1 < t2

instance : ProvableStruct Inputs where
  components := [U32, U32]
  toComponents := fun {x, y} => .cons x ( .cons y .nil)
  fromComponents := fun (.cons x ( .cons y .nil)) => ⟨ x, y ⟩

Nat.reduceMod in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

instance ExplicitCircuits.to_single (circuit : α → Circuit F β) (a : α)
    [explicit : ExplicitCircuits circuit] : ExplicitCircuit (circuit a) where
  output n := output circuit a n
  localLength n := explicit.localLength a n
  operations n := operations circuit a n
  output_eq n := output_eq a n
  localLength_eq n := localLength_eq a n
  operations_eq n := operations_eq a n
  subcircuitsConsistent n := subcircuitsConsistent a n

@[circuit_norm]
def Condition.apply (condition : Condition F) (offset : ℕ) : Operation F → Prop
  | .witness m c => condition.witness offset m c
  | .assert e => condition.assert offset e
  | .lookup l => condition.lookup offset l
  | .subcircuit s => condition.subcircuit offset s

MulZeroOneClass in Mathlib.Algebra.GroupWithZero.Defs

UInt64.ofNat in Init.Data.UInt.BasicAux

let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words
  let block_words := permute block_words
  let state := round state block_words

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

soundness := by admit /- proof elided -/

replaceMainGoal [currentGoal]

def vals (x : U64 (F p)) : U64 ℕ := x.map ZMod.val

def updateChunk (state : ChunkState) (input_bytes : List ℕ) : ChunkState :=
  let combined := state.block_buffer ++ input_bytes
  let (blockWords, remainder) := splitIntoBlockWords combined
  let newState := processBlocksWords state blockWords
  { newState with block_buffer := remainder }

structure NonProvableStruct (F : Type) where
  a : F
  b : F

@[circuit_norm]
def subcircuitWithAssertion (circuit : GeneralFormalCircuit 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])

let env i :=
    if h : i < assignment.offset then
      match assignment.vars[i] with
      | .input ⟨r, c⟩ =>
        
          if r = 0 then cur_row[c]! else next_row[c]!
      | .aux _ =>
        
        
        
        next_row[aux_map[i]!]!
    
    else panic! s!"Invalid variable index {i} in environment"

lookup circuit.toTable (input, output)
    return output

def Circuit.proverEnvironment (circuit : Circuit F α) (init : List F := []) : Environment F :=
  .fromList (FlatOperation.dynamicWitnesses (circuit.operations init.length).toFlat init)

soundness := by admit /- proof elided -/

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

Assumptions | { x, y } => x.val < 256 ∧ y.val < 256

if isSoundness then
      match headConst? with
      | some ``Soundness =>
        evalTactic (← `(tactic| unfold Soundness))
        let names := [`i₀, `env, `input_var, `input, `h_input, `h_assumptions, `h_holds]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | some ``FormalAssertion.Soundness =>
        evalTactic (← `(tactic| unfold FormalAssertion.Soundness))
        let names := [`i₀, `env, `input_var, `input, `h_input, `h_assumptions, `h_holds]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | some ``GeneralFormalCircuit.Soundness =>
        evalTactic (← `(tactic| unfold GeneralFormalCircuit.Soundness))
        let names := [`i₀, `env, `input_var, `input, `h_input, `h_holds]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | _ => pure ()
      return
    else if isCompleteness then
      
      match headConst? with
      | some ``Completeness =>
        evalTactic (← `(tactic| unfold Completeness))
        let names := [`i₀, `env, `input_var, `h_env, `input, `h_input, `h_assumptions]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | some ``FormalAssertion.Completeness =>
        evalTactic (← `(tactic| unfold FormalAssertion.Completeness))
        let names := [`i₀, `env, `input_var, `h_env, `input, `h_input, `h_assumptions, `h_spec]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | some ``GeneralFormalCircuit.Completeness =>
        evalTactic (← `(tactic| unfold GeneralFormalCircuit.Completeness))
        let names := [`i₀, `env, `input_var, `h_env, `input, `h_input, `h_assumptions]
        for name in names do
          evalTactic (← `(tactic| intro $(mkIdent name):ident))
      | _ => pure ()
      return
    else
      
      throwError "circuitProofStartCore can only be used on Soundness, Completeness, FormalAssertion.Soundness, FormalAssertion.Completeness, GeneralFormalCircuit.Soundness, or GeneralFormalCircuit.Completeness goals"

instance : HSub (field (Expression F)) (Expression F) (Expression F) where
  hSub (x : Expression F) y := x - y

def nbits (a : ℕ) : ℕ :=
  if a = 0 then 1 else Nat.log2 a + 1

let block_words := bytesToWords input.buffer_data

Permutation.circuit state'

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

let trace_data := witnesses fib_relation_babybear init_row steps
  let json_data := Lean.toJson trace_data

def permute (state : Vector ℕ 16) : Vector ℕ 16 :=
  Vector.ofFn (fun i => state[msgPermutation[i]])

def rangeCheck (n : ℕ) (hn : 2^n < p) : FormalAssertion (F p) field where
  main x := do
    
    let _ ← toBits n hn x

(idx + 1, next_row)
    )
    (0, next_row)

instance : Fact (p > 512) := .mk (by admit /- proof elided -/
)

def formalFibTable : FormalTable (F p) RowType := {
  constraints := fibTable
  Spec := Spec

return bits

map
</all_available_defs>

<all_available_lemmas>
theorem bind_operations_eq (f : Circuit F α) (g : α → Circuit F β) (n : ℕ) :
  (f >>= g).operations n = f.operations n ++ (g (f.output n)).operations (n + f.localLength n)

theorem Fin.foldl_const_succ (n : ℕ) (f : Fin (n + 1) → α) (init : α) :
    Fin.foldl (n + 1) (fun _ i => f i) init = f (.last n)

theorem Fin.foldl_const (n : ℕ) (f : Fin n → α) (init : α) :
  Fin.foldl n (fun _ i => f i) init = match n with

theorem toBits_injective (n : ℕ) {x y : ℕ} : x < 2^n → y < 2^n →
    toBits n x = toBits n y → x = y

@[circuit_norm ↓]
theorem eval_fields {F : Type} [Field F] (env : Environment F) (x : Var (fields n) F) :
  ProvableType.eval env x = x.map (Expression.eval env)

omit [Fact (Nat.Prime p)] p_large_enough in
theorem soundness_to_u32 {x y z : U32 (F p)}
  (x_norm : x.Normalized) (y_norm : y.Normalized)
  (h_eq :
    z.x0.val = x.x0.val ^^^ y.x0.val ∧
    z.x1.val = x.x1.val ^^^ y.x1.val ∧
    z.x2.val = x.x2.val ^^^ y.x2.val ∧
    z.x3.val = x.x3.val ^^^ y.x3.val) : Spec { x, y } z

lemma eval_toArray_extract_eq {n : ℕ} (start finish : ℕ) {env : Environment (F p)}
    {v : Var (fields n) (F p)} {w : fields n (F p)}
    (h_eval : w = eval env v)
    (h_bounds : finish ≤ n) (h_start : start ≤ finish) :
    ProvableType.eval (α := fields (finish - start)) env
      ⟨v.toArray.extract start finish, by simp [Array.size_extract]; omega⟩ =
    ⟨w.toArray.extract start finish, by simp [Array.size_extract]; omega⟩

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

theorem MemoryAccessList.lastWriteValue_filter (accesses : MemoryAccessList)
    (h_sorted : accesses.isTimestampSorted) (addr : ℕ) (h_sorted' : ((MemoryAccessList.filterAddress accesses addr).isTimestampSorted))  :
    MemoryAccessList.lastWriteValue accesses h_sorted addr =
    MemoryAccessList.lastWriteValue (MemoryAccessList.filterAddress accesses addr) h_sorted' addr

@[circuit_norm]
lemma eval_mul (env : Environment F) (a b : Expression F) :
    Expression.eval env (Expression.mul a b) = (Expression.eval env a) * (Expression.eval env b)

theorem MemoryAccessList.isConsistentSingleAddress_iff (accesses : MemoryAccessList) (addr : ℕ) (h_sorted : accesses.isTimestampSorted)
    (h_eq : accesses.all (fun (_t, addr', _readValue, _writeValue) => addr' = addr)) :
    MemoryAccessList.isConsistentOnline accesses h_sorted ↔
    MemoryAccessList.isConsistentSingleAddress accesses h_sorted

lemma constraintsHold_append : ∀ {a b: List (FlatOperation F)}, ∀ {env : Environment F},
    ConstraintsHoldFlat env (a ++ b) ↔ ConstraintsHoldFlat env a ∧ ConstraintsHoldFlat env b

lemma finset_ssubset_univ_of_not_mem {α : Type*} [Fintype α] (s : Finset α) (x : α)
    (h : x ∉ s) :
    s ⊂ Finset.univ

@[circuit_norm]
theorem FormalCircuit.toSubcircuit_localLength
    {F : Type} [Field F] {Input Output : TypeMap} [ProvableType Input] [ProvableType Output]
    (circuit : FormalCircuit F Input Output) (n : ℕ) (input_var : Var Input F) :
    (circuit.toSubcircuit n input_var).localLength = circuit.localLength input_var

lemma assertion_localLength_eq (circuit : FormalAssertion F β) (input : Var β F) (offset : ℕ) :
  (circuit.toSubcircuit offset input).localLength = circuit.localLength input

theorem femtoCairoTableStatement
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p)
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p)) (h_memorySize : memorySize < p)
  (state : State (F p)) : ∀ n > 0, ∀ trace,
  (femtoCairoFormalTable program h_programSize memory h_memorySize state).statement n trace →
    match
      Spec.femtoCairoMachineBoundedExecution program memory (some {pc:=0, ap:=0, fp:=0}) (n - 1) with

theorem rotRight64_toBits (x r : ℕ) (h : x < 2^64):
    toBits 64 (rotRight64 x r) = (toBits 64 x).rotate r

lemma sum_nat_cast_nonneg {α : Type*} [Fintype α] (f : α → ℕ) :
    0 ≤ ∑ x : α, (f x : ℤ)

theorem getElem_mapFinRange {n} {create : Fin n → α} :
    ∀ (i : ℕ) (hi : i < n), (mapFinRange n create)[i] = create ⟨ i, hi ⟩

theorem varFromOffset_vector {F : Type} [Field F] {α : TypeMap} [NonEmptyProvableType α] (offset : ℕ) :
    varFromOffset (F:=F) (ProvableVector α n) offset
    = .mapRange n fun i => varFromOffset α (offset + (size α)*i)

@[ext]
lemma State.ext {F : Type} {s1 s2 : State F} (h1 : s1.pc = s2.pc) (h2 : s1.ap = s2.ap) (h3 : s1.fp = s2.fp) : s1 = s2

omit [Field F] in
lemma traceInputs_length {N : ℕ} (trace : TraceOfLength F (ProvablePair State Input) N) :
    (traceInputs trace).length = N

@[circuit_norm]
theorem fromElements_eval_toElements {env : Environment F} (x : α (Expression F)) :
  fromElements (Vector.map (Expression.eval env) (toElements x)) = eval env x

lemma ApplyRounds.circuit_assumptions_is :
  ApplyRounds.circuit.Assumptions (F := F p) = ApplyRounds.Assumptions

theorem not_lt (n : ℕ) {x : ℕ} (hx : x < n) : n - 1 - (x : ℤ) < n

theorem completeness_bool [p_neq_zero : NeZero p] (x y carry_in : F p) :
    x.val < 256 ->
    y.val < 256 ->
    carry_in.val < 2 ->
    let carry_out := FieldUtils.floorDiv (x + y + carry_in) 256
    IsBool carry_out

lemma two_off_eq_mod (offset : Fin 8) (h : offset.val ≠ 0):
    (2 ^ (8-offset.val) % 256) = 2 ^ (8-offset.val)

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem val_of_natToField_eq {n : ℕ} (lt : n < p) : (natToField n lt).val = n

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

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

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem table_soundness (table : InductiveTable F State Input) (input output : State F)
  (N : ℕ+) (trace : TraceOfLength F (ProvablePair State Input) N) (env : ℕ → ℕ → Environment F) :
  table.Spec input [] 0 rfl input → TableConstraintsHold (table.tableConstraints input output) trace env →
    table.Spec input (traceInputs trace.tail) (N-1) (traceInputs_length trace.tail) output

theorem MemoryAccessList.noTimestampDup_of_cons (head : MemoryAccess) (tail : MemoryAccessList)
    (h : Notimestampdup (head :: tail)) :
    Notimestampdup tail

lemma completeness_two {p : ℕ} [Fact p.Prime]
    (offset : ℕ) (env : Environment (F p)) (input_var : Var (fields 2) (F p))
    (input : fields 2 (F p))
    (h_local_witnesses : env.UsesLocalWitnessesCompleteness offset ((main input_var).operations offset))
    (h_env : input = eval env input_var)
    (h_assumptions : Assumptions 2 input) :
    Circuit.ConstraintsHold.Completeness env ((main input_var).operations offset)

lemma rotRight64_testBit (x r i : ℕ) (h : x < 2^64) :
    (rotRight64 x r).testBit i =
    if i < 64 - r % 64 then
      x.testBit (r % 64 + i)
    else (decide (i < 64) && x.testBit (i - (64 - r % 64)))

Nat.add_sub_self_left in Init.Data.Nat.Basic

theorem localLength_cons {a : Operation F} {as : Operations F} :
    localLength (a :: as) = a.localLength + as.localLength

lemma foldl_eq_sum_range {α : Type*} [AddCommMonoid α] : ∀ (n' : ℕ) (f' : Fin n' → α),
    Fin.foldl n' (fun acc i => acc + f' i) 0 = ∑ i ∈ Finset.range n', if h : i < n' then f' ⟨i, h⟩ else 0

theorem map_mapRange {n} {create : ℕ → α} {f : α → β} :
  Vector.map f (Vector.mapRange n create) =
    Vector.mapRange n (fun i => f (create i))

theorem completeness : Completeness (F p) elaborated Assumptions

lemma path_has_transition {S : Type*} [DecidableEq S] (path : List S)
    (h_len : path.length ≥ 2) :
    ∃ (t : Transition S), t ∈ path.zip path.tail

lemma extract_preserves_element {p n n1 : ℕ} (input : fields n (F p)) (i : ℕ) (hi : i < n1) (h_n1_lt : n1 ≤ n) :
    let input1 : fields n1 (F p) := ⟨input.toArray.extract 0 n1, by simp [Array.size_extract, Vector.size_toArray]; exact h_n1_lt⟩
    input1[i]'hi = input[i]'(by omega)

lemma fromUInt64_normalized (x : UInt64) : (fromUInt64 (p:=p) x).Normalized

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

theorem MemoryAccessList.filterAddress_sorted (accesses : MemoryAccessList)
    (h : accesses.isTimestampSorted) (addr : ℕ) :
    (MemoryAccessList.filterAddress accesses addr).isTimestampSorted

theorem test_conjunction_with_base_and_non_base {F : Type} [Field F] (env : Environment F) (x : F)
    (x_var y_var z_var : Var field F) (s1 s2 : Var SimpleStruct F)
    (h : (eval env (TestInputs.mk x_var y_var z_var) = TestInputs.mk 1 2 3 ∧ x = 7) ∧
         eval env s1 = eval env s2) :
    Expression.eval env x_var = 1

theorem getElem_eval_fields {F : Type} [Field F] {n : ℕ} {env : Environment F}
  (x : Var (fields n) F) (i : ℕ) (hi : i < n) :
    Expression.eval env x[i] = (eval env x)[i]

lemma chi_loop (state : Vector ℕ 25) :
    Specs.Keccak256.chi state = .mapFinRange 25 fun i => state[i] ^^^ ((not64 state[i + 5]) &&& state[i + 10])

theorem cast_apply' {α α' β : Type} (h : α = α') (f : α → β) (x : α') :
    (cast (h ▸ rfl) f : α' → β) x = f (cast (h ▸ rfl) x : α)

lemma and_xor_sum (x0 x1 y0 y1 : ℕ) (hx0 : x0 < 2^8) (hy0 : y0 < 2^8) :
  (x0 ^^^ (2^8 * x1)) &&& (y0 ^^^ (2^8 * y1)) = (x0 &&& y0) ^^^ 2^8 * (x1 &&& y1)

theorem completeness (a b c d : Fin 16) : Completeness (F p) (elaborated a b c d) Assumptions

theorem val_lt_two {p : ℕ} [Fact p.Prime] {x : F p} (h : IsBool x) : x.val < 2

theorem mapFinRange_zero {create : Fin 0 → α} : mapFinRange 0 create = #v[]

lemma sum_decrease {α : Type*} [Fintype α] [DecidableEq α] (f g : α → ℕ) (a : α)
    (h_a_decrease : g a < f a)
    (h_others_le : ∀ x, g x ≤ f x) :
    ∑ x : α, g x < ∑ x : α, f x

theorem one_land_of_IsBool (a : ℕ) (h : IsBool a) : 1 &&& a = a

@[circuit_norm] theorem ConstraintsHold.append_completeness {as bs : Operations F} :
  ConstraintsHold.Completeness env (as ++ bs)
  ↔ ConstraintsHold.Completeness env as ∧ ConstraintsHold.Completeness env bs

lemma val_two : (2 : F p).val = 2

lemma ApplyRouunds.circuit_spec_is :
  ApplyRounds.circuit.Spec (F := F p) = ApplyRounds.Spec

theorem test_eval_eq_struct_variable {F : Type} [Field F] (env : Environment F) (input : TestInputs F)
    (x_var y_var z_var : Var field F)
    (h : eval env (TestInputs.mk x_var y_var z_var) = input) :
    TestInputs.mk (Expression.eval env x_var) (Expression.eval env y_var) (Expression.eval env z_var) = input

theorem value_fromUInt32 (x : UInt32) : value (fromUInt32 (p:=p) x) = x.toNat

@[circuit_norm] theorem ConstraintsHold.append_soundness {as bs : Operations F} :
  ConstraintsHold.Soundness env (as ++ bs)
  ↔ ConstraintsHold.Soundness env as ∧ ConstraintsHold.Soundness env bs

@[table_norm, table_assignment_norm]
theorem bind_def {β : Type} (f : TableConstraint W S F α) (g : α → TableConstraint W S F β) :
  (f >>= g) = fun ctx =>
    let (a, ctx')

theorem cast_mapFinRange {n} {create : Fin n → α} (h : n = m) :
    mapFinRange n create = (mapFinRange m (fun i => create (i.cast h.symm))).cast h.symm

@[circuit_norm ↓ high]
theorem eval_pair {α β: TypeMap} [ProvableType α] [ProvableType β] (env : Environment F)
  (a : Var α F) (b : Var β F) :
    eval (α:=ProvablePair α β) env (a, b) = (eval env a, eval env b)

@[table_norm, table_assignment_norm]
theorem TableConstraint.assignVar_circuit : ∀ ctx (off : CellOffset W S) (v : Variable F),
  (assignVar off v ctx).snd.circuit = ctx.circuit

theorem ConstraintsHold.completeness_iff_forAll' {env : Environment F} {circuit : Circuit F α} {n : ℕ} :
  ConstraintsHold.Completeness env (circuit.operations n) ↔ circuit.forAll n {
    assert _ e := env e = 0,
    lookup _ l := l.table.Completeness (l.entry.map env),
    subcircuit _ _ s := s.Completeness env
  }

theorem test_struct_literal_eq_variable {F : Type} [Field F] (input : TestInputs F)
    (h : TestInputs.mk 1 2 3 = input) :
    input.x = 1

omit p_large_enough in
@[circuit_norm]
lemma value_zero :
    (0 : U32 (F p)) = U32.mk 0 0 0 0

theorem test_complex_eval {F : Type} [Field F] (env : Environment F)
    (a_var b_var c_var d_var e_var : Var field F)
    (h : eval env (TestInputs.mk (a_var + b_var) (c_var * d_var) e_var) = TestInputs.mk 5 6 7) :
    Expression.eval env (a_var + b_var) = 5 ∧
    Expression.eval env (c_var * d_var) = 6 ∧
    Expression.eval env e_var = 7

lemma map_take {α β : Type} {n : ℕ} (f : α → β) (xs : Vector α n) (i : ℕ) :
    (xs.map f).take i = (xs.take i).map f

theorem rotation64_bits_soundness {o : ℕ} (ho : o < 8) {x : U64 ℕ} :
    (rotRight64_u64 x o).valueNat = rotRight64 x.valueNat o

theorem test_multiple_eval_expressions {F : Type} [Field F] (env1 env2 : Environment F)
    (x1_var y1_var z1_var : Var field F) (a2_var b2_var : Var field F)
    (h1 : eval env1 (TestInputs.mk x1_var y1_var z1_var) = TestInputs.mk 1 2 3)
    (h2 : eval env2 (SimpleStruct.mk a2_var b2_var) = SimpleStruct.mk 4 5) :
    Expression.eval env1 x1_var = 1 ∧ Expression.eval env2 b2_var = 5

lemma countAsSecond_cons (hd : S) (tl : List S) (x : S) :
    countAsSecond (hd :: tl) x = (if tl.head? = some x then 1 else 0) + countAsSecond tl x

theorem soundness (offset : Fin 64) : Soundness (F p) (circuit := elaborated offset) Assumptions (Spec offset)

theorem fromElements_toElements {F} : (cs : List WithProvableType) → (xs : ProvableTypeList F cs) →
    componentsFromElements cs (componentsToElements cs xs) = xs

theorem toElements_fromElements {F} : (cs : List WithProvableType) → (xs : Vector F (combinedSize' cs)) →
    componentsToElements cs (componentsFromElements cs xs) = xs

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem soundness (offset : Fin 8) : Soundness (F p) (circuit := elaborated offset) Assumptions (Spec offset)

@[ext]
theorem ext {f g : Circuit F α}
  (h_output : ∀ n, f.output n = g.output n)
  (h_operations : ∀ n, f.operations n = g.operations n) :
    f = g
</all_available_lemmas>

<local_ctx>
import Clean.Circuit.Subcircuit

import Clean.Utils.Misc

variable {n m : ℕ} {F : Type} [Field F] {α β : Type}

namespace Circuit

variable {prop : Condition F}

namespace ForM

variable {circuit : α → Circuit F Unit} (xs : Vector α m) (constant : ConstantLength circuit) (n : ℕ)

end ForM

namespace MapM

variable {circuit : α → Circuit F β} {xs : Vector α m} [constant: ConstantLength circuit]
  {prop : Condition F}

end MapM

namespace FoldlM

@[reducible]
def prod (circuit : β → α → Circuit F β) : β × α → Circuit F β := fun t => circuit t.1 t.2

variable {env : Environment F} {prop : Condition F} {xs : Vector α m}
  {circuit : β → α → Circuit F β} {init : β} {constant : ConstantLength (prod circuit)}

def foldlAcc (n : ℕ) (xs : Vector α m) (circuit : β → α → Circuit F β) (init : β) (j : Fin m) : β :=
  Fin.foldl j (fun acc i => (circuit acc xs[i.val]).output (n + i*(circuit acc xs[i.val]).localLength)) init

variable {prop : Condition F}

section

variable {env : Environment F} {prop : Condition F} {m : ℕ}
  {Acc : ℕ → Type}
  {circuit : β → Fin m → Circuit F β} {init : β} {constant : ConstantLength (prod circuit)}

end

variable [Inhabited β] [Inhabited α] {h_const_out : ConstantOutput fun (t : β × α) => circuit t.1 t.2}
</local_ctx>

<target_theorem>
theorem operations_eq_const [NeZero m] (constant : ConstantLength (prod circuit))
    (h_const_out : ConstantOutput (prod circuit)) :
  (Vector.foldlM circuit init xs).operations n =
  (circuit init (xs[0]'(NeZero.pos m))).operations n ++
  (List.ofFn fun (⟨i, _⟩ : Fin (m - 1)) =>
    let k := (circuit default default).localLength
    let acc := (circuit default xs[i]).output (n + i*k)
    (circuit acc xs[i + 1]).operations (n + (i + 1)*k)).flatten :=
</target_theorem>

