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

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

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

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

def induct {motive : Operations F → Sort*}
  (empty : motive [])
  (witness : ∀ m c ops, motive ops → motive (.witness m c :: ops))
  (assert : ∀ e ops, motive ops → motive (.assert e :: ops))
  (lookup : ∀ l ops, motive ops → motive (.lookup l :: ops))
  (subcircuit : ∀ {n} (s : Subcircuit F n) ops, motive ops → motive (.subcircuit s :: ops))
    (ops : Operations F) : motive ops :=
  match ops with
  | [] => empty
  | .witness m c :: ops => witness m c ops (induct empty witness assert lookup subcircuit ops)
  | .assert e :: ops => assert e ops (induct empty witness assert lookup subcircuit ops)
  | .lookup l :: ops => lookup l ops (induct empty witness assert lookup subcircuit ops)
  | .subcircuit s :: ops => subcircuit s ops (induct empty witness assert lookup subcircuit 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

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

def FlatOperation.singleLocalLength : FlatOperation F → ℕ
  | .witness m _ => m
  | .assert _ => 0
  | .lookup _ => 0

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

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

Fintype in Mathlib.Data.Fintype.Defs

Lean.MonadLCtx in Lean.LocalContext

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

@[reducible, table_norm, table_assignment_norm]
instance : MonadLift (Circuit F) (TableConstraint W S F) where
  monadLift circuit ctx :=
    let (a, ops) := circuit ctx.circuit.localLength
    (a, {
      circuit := ctx.circuit ++ ops,
      assignment := assignmentFromCircuit ctx.assignment ops
    })

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

def fibRelationBabybear := fibRelation (p:=p_babybear)

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

def rhoPiConstants := rhoPiIndices.zip rhoPiShifts

def rotRight64_u64 : U64 ℕ → ℕ → U64 ℕ
  | ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩, o => ⟨
    (x0 / 2^o) + (x1 % 2^o) * 2^(8-o),
    (x1 / 2^o) + (x2 % 2^o) * 2^(8-o),
    (x2 / 2^o) + (x3 % 2^o) * 2^(8-o),
    (x3 / 2^o) + (x4 % 2^o) * 2^(8-o),
    (x4 / 2^o) + (x5 % 2^o) * 2^(8-o),
    (x5 / 2^o) + (x6 % 2^o) * 2^(8-o),
    (x6 / 2^o) + (x7 % 2^o) * 2^(8-o),
    (x7 / 2^o) + (x0 % 2^o) * 2^(8-o),
  ⟩

def femtoCairoMachineTransition
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p))
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p))
    (state : State (F p)) : Option (State (F p)) := do
  
  let { rawInstrType, op1, op2, op3 } ← fetchInstruction program state.pc

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

instance : ProvableStruct Input where
  components := [KeccakState, KeccakBlock]
  toComponents := fun { state, block } => .cons state (.cons block .nil)
  fromComponents := fun (.cons state (.cons block .nil)) => { state, block }

@[reducible] def CAPACITY := 8

instance {n : ℕ} : NonEmptyProvableType (fields (n + 1)) where
nonempty := Nat.zero_lt_succ n

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

soundness := by admit /- proof elided -/

List.take in Init.Data.List.Basic

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

structure StateTransitionInput (F : Type) where
  state : State F
  decoded : DecodedInstruction F
  v1 : F
  v2 : F
  v3 : F

example : Soundness (F p) testCircuit Assumptions Spec :=

StateM in Init.Control.State

def pushVarInput_offset (assignment : CellAssignment W S) (off : CellOffset W S) :
  (assignment.pushVarInput off).offset = assignment.offset + 1 :=

List.cons in Init.Prelude

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

instance : HAdd (Expression F) (field (Expression F)) (Expression F) where
  hAdd x (y : Expression F) := x + y

def twoRoundsWithPermute : FormalCircuit (F p) Round.Inputs Round.Inputs :=
  roundWithPermute.concat roundWithPermute (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  )

def circuit (n : ℕ) : FormalCircuit (F p) (Inputs n) (fields n) where
  main := main n

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 (Lookup F) where
  reprPrec l _ := "(Lookup " ++ l.table.name ++ " " ++ repr l.entry ++ ")"

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

structure Inputs (F : Type) where
  c : Vector F 4  
  s : Vector F 2

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

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

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

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

def DecodedInstructionType.isEncodedCorrectly (instrType : DecodedInstructionType (F p)) : Prop :=
  (instrType.isAdd = 1 ∧ instrType.isMul = 0 ∧ instrType.isStoreState = 0 ∧ instrType.isLoadState = 0) ∨
  (instrType.isAdd = 0 ∧ instrType.isMul = 1 ∧ instrType.isStoreState = 0 ∧ instrType.isLoadState = 0) ∨
  (instrType.isAdd = 0 ∧ instrType.isMul = 0 ∧ instrType.isStoreState = 1 ∧ instrType.isLoadState = 0) ∨
  (instrType.isAdd = 0 ∧ instrType.isMul = 0 ∧ instrType.isStoreState = 0 ∧ instrType.isLoadState = 1)

Id.run in Init.Control.Id

structure Inputs (n : ℕ) (F : Type) where
  c : ProvableVector (fields 8) n F  
  s : Vector F 3

UInt32.size in Init.Prelude

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

HEq in Init.Prelude

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

instance ExplicitCircuit.from_bind {f : Circuit F α} {g : α → Circuit F β}
    (f_explicit : ExplicitCircuit f) (g_explicit : ∀ a : α, ExplicitCircuit (g a)) : ExplicitCircuit (f >>= g) where
  output n :=
    let a := output f n
    output (g a) (n + localLength f n)

reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

let goal ← getMainGoal
    let target ← goal.getType
    let varsInGoal ← findStructVars target
    
    for fvarId in varsInGoal do
      if ← hasProvableStructInstance fvarId then
        result := fvarId :: result

computeNextState instr_type v1 v2 v3 state

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

Array.replicate in Init.Data.Array.Basic

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 applyRounds (chaining_value : Vector ℕ 8) (block_words : Vector ℕ 16) (counter : ℕ) (block_len : ℕ) (flags : ℕ) : Vector ℕ 16 :=
  
  let counter_low := counter % 2^32
  let counter_high := counter / 2^32

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

Soundness := fun (input, output) => circuit.Assumptions input → circuit.Spec input output
  Completeness := fun (input, output) => circuit.Assumptions input ∧ output = circuit.constantOutput input

List.getLast? in Init.Data.List.Basic

structure Inputs (n : ℕ) (F : Type) where
  c : ProvableVector (ProvablePair field field) n F  
  s : F

def induct {motive : List (FlatOperation F) → Sort*}
  (empty : motive [])
  (witness : ∀ m c ops, motive ops → motive (.witness m c :: ops))
  (assert : ∀ e ops, motive ops → motive (.assert e :: ops))
  (lookup : ∀ l ops, motive ops → motive (.lookup l :: ops))
    (ops : List (FlatOperation F)) : motive ops :=
  match ops with
  | [] => empty
  | .witness m c :: ops => witness m c ops (induct empty witness assert lookup ops)
  | .assert e :: ops => assert e ops (induct empty witness assert lookup ops)
  | .lookup l :: ops => lookup l ops (induct empty witness assert lookup ops)

Bool in Init.Prelude

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

instance explicit : ExplicitCircuits (Gadgets.Addition32Full.main (p:=pBabybear)) :=

instance elaborated : ElaboratedCircuit F M field where
  main
  localLength _ := 2 * size M
  localLength_eq := by admit /- proof elided -/

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

Fin.reduceEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin

def stateInitG : Vector ℕ 16 := #v[1321565287, 1539917118, 1918974978, 1109417770, 1286102396, 687960962, 441968613, 3595364146, 3111632159, 1102204962, 944689943, 3680149627, 3129663845, 3265095166, 606420953, 4183330326]
example : g stateInitG 0 1 2 3 4 5 = #v[3279123572, 367480655, 3947042124, 3663589532, 1286102396, 687960962, 441968613, 3595364146, 3111632159, 1102204962, 944689943, 3680149627, 3129663845, 3265095166, 606420953, 4183330326] := rfl

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

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

def circuit (n ops : ℕ) [hn : NeZero n] (hnout : 2^(nbits ((2^n - 1) * ops)) < p) :
    FormalCircuit (F p) (BinSumInput n ops) (fields (nbits ((2^n - 1) * ops))) where
  main input := main n ops input

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

def Spec {N : ℕ} (trace : TraceOfLength (F p) RowType N) : Prop :=
  trace.ForAllRowsOfTraceWithIndex fun row index =>
    (row.x.value = fib32 index) ∧
    (row.y.value = fib32 (index + 1)) ∧
    row.x.Normalized ∧ row.y.Normalized

def hasProvableStructInstance (type : Expr) : MetaM Bool := do
  let type' ← withTransparency .reducible (whnf type)
  
  match type' with
  | .app typeCtor _ =>
    try
      let instType ← mkAppM ``ProvableStruct #[typeCtor]
      match ← trySynthInstance instType with
      | .some _ => return true
      | _ => return false
    catch _ => return false
  | _ => return false

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 generateStructFieldNames (fvarId : FVarId) : MetaM AltVarNames := do
  let localDecl ← fvarId.getDecl
  let userName := localDecl.userName

toElements_fromElements {F : Type} : ∀ v : Vector F size, toElements (fromElements v) = v := by admit /- proof elided -/

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

def roundConstants : Vector (Fin 16 × Fin 16 × Fin 16 × Fin 16 × Fin 16 × Fin 16) 8 := #v[
  (0, 4, 8, 12, 0, 1),
  (1, 5, 9, 13, 2, 3),
  (2, 6, 10, 14, 4, 5),
  (3, 7, 11, 15, 6, 7),
  (0, 5, 10, 15, 8, 9),
  (1, 6, 11, 12, 10, 11),
  (2, 7, 8, 13, 12, 13),
  (3, 4, 9, 14, 14, 15)
]

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

def rotRight32_u32 : U32 ℕ → ℕ → U32 ℕ
  | ⟨ x0, x1, x2, x3 ⟩, o => ⟨
    (x0 / 2^o) + (x1 % 2^o) * 2^(8-o),
    (x1 / 2^o) + (x2 % 2^o) * 2^(8-o),
    (x2 / 2^o) + (x3 % 2^o) * 2^(8-o),
    (x3 / 2^o) + (x0 % 2^o) * 2^(8-o),
  ⟩

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

go e []

def MemoryAccess := ℕ × ℕ × ℕ × ℕ

soundness : InductiveTable.Soundness F State Input Spec step

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)

structure TestInputs (F : Type) where
  x : F
  y : F
  z : F

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

Spec _ _ i _ row : Prop :=
    row.x.value = fib32 i ∧
    row.y.value = fib32 (i + 1) ∧
    row.x.Normalized ∧ row.y.Normalized

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

let mux_out ← MultiMux1.circuit 1 { c := #v[(c[0], c[1])], s }
  return mux_out[0]

def take : {N : ℕ} → TraceOfLength F S N → (i : Fin (N + 1)) → TraceOfLength F S i
  | 0, ⟨ <+>, h0 ⟩, i => ⟨ <+>, i.val_eq_zero.symm ▸ rfl ⟩
  | N + 1, ⟨ rest +> row, h ⟩, ⟨ i, hi ⟩ =>
    if hi' : i = N + 1 then
      
      ⟨ rest +> row, hi' ▸ h ⟩
    else
      take ⟨ rest, Nat.succ_inj.mp h ⟩ ⟨ i, by admit /- proof elided -/
      ⟩

def inductPush {motive : {n : ℕ} → Vector α n → Sort u}
  (nil : motive #v[])
  (push: ∀ {n : ℕ} (as : Vector α n) (a : α), motive as → motive (as.push a))
  {n : ℕ} (v : Vector α n) : motive v :=
  match v with
  | ⟨ .mk [], (h : 0 = n) ⟩ =>
    cast (by admit /- proof elided -/
    ) nil
  | ⟨ .mk (a :: as), h ⟩ =>
    have hlen : as.length + 1 = n := by admit /- proof elided -/

def fourRoundsWithPermute : FormalCircuit (F p) Round.Inputs Round.Inputs :=
  twoRoundsWithPermute.concat twoRoundsWithPermute (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  )

instance : HMul F (field (Expression F)) (field (Expression F)) where
  hMul x y : Expression F := x * y

lc1 + isZero_out * (2^n : F p) === (2^n : F p) - input

List in Init.Prelude

def chainingValue : Vector ℕ 8 := #v[671114869, 2251103971, 1125212539, 2996205183, 1286164105, 2483632496, 367841012, 3199388477]

@[reducible] def KeccakBlock := ProvableVector U64 RATE

try
        
        let altVarNames ← generateStructFieldNames fvarId
        
        
        let casesResult ← currentGoal.cases fvarId #[altVarNames]

instance : ProvableStruct Inputs where
  components := [ProvableVector U32 8, ProvableVector U32 16, U32, U32, U32, U32]
  toComponents := fun { chaining_value, block_words, counter_high, counter_low, block_len, flags } =>
    .cons chaining_value (.cons block_words (.cons counter_high (.cons counter_low (.cons block_len (.cons flags .nil)))))
  fromComponents := fun (.cons chaining_value (.cons block_words (.cons counter_high (.cons counter_low (.cons block_len (.cons flags .nil)))))) =>
    { chaining_value, block_words, counter_high, counter_low, block_len, flags }

instance {α : TypeMap} [ProvableType α] : Inhabited (Circuit F (Var α F)) where
  default := witness default

contains_iff := by admit /- proof elided -/

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

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

instance {n : ℕ} [hn : NeZero n] : NonEmptyProvableType (fields n) where
  nonempty := Nat.pos_of_ne_zero hn.out

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

def Spec (a b c d : Fin 16) (input : Inputs (F p)) (out : BLAKE3State (F p)) :=
  let { state, x, y } := input
  out.value = g state.value a b c d x.value y.value ∧ out.Normalized

localLength _ := 2
  output _ i0 := var ⟨i0⟩

replaceMainGoal [currentGoal]

def add32 (a b : ℕ) : ℕ := (a + b) % 2^32

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

instance [Repr F] : Repr (TableOperation S F) where
  reprPrec op _ := match op with
    | .boundary i c => "boundary " ++ reprStr i ++ " " ++ reprStr c
    | .everyRow c => "everyRow " ++ reprStr c
    | .everyRowExceptLast c => "everyRowExceptLast " ++ reprStr c

def TimestampSortedMemoryAccessList := {accesses : MemoryAccessList // accesses.isTimestampSorted}

Finset.erase in Mathlib.Data.Finset.Erase

subcircuitsConsistent : ∀ acc x, ((step acc x).operations ((size State) + (size Input))).SubcircuitsConsistent ((size State) + (size Input))
    := 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]⟩

Spec := fun { enabled, inp } =>
    enabled = 1 → inp.1 = inp.2

Monad in Init.Prelude

class ProvableType (M : TypeMap) where
  size : ℕ
  toElements {F : Type} : M F -> Vector F size
  fromElements {F : Type} : Vector F size -> M F

-- Test single block processing
-- With the fix, 64 bytes now stay in the buffer (matching Python behavior)
example :
    let state := initialChunkState testCV 0
    let updated := updateChunk state testBlock64
    updated.blocks_compressed = 0 ∧ updated.block_buffer = testBlock64 :=

def fib8 : ℕ -> ℕ
  | 0 => 0
  | 1 => 1
  | (n + 2) => (fib8 n + fib8 (n + 1)) % 256

def recursiveRelation : TwoRowsConstraint RowType (F p) := do
  let curr ← TableConstraint.getCurrRow
  let next ← TableConstraint.getNextRow

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

Lean.Json.num in Lean.Data.Json.Basic

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

Zero.zero in Init.Prelude

Fin.xor in Init.Data.Fin.Basic

soundness := by admit /- proof elided -/

def fromBits {n : ℕ} (bits : Vector ℕ n) : ℕ :=
  Fin.foldl n (fun acc ⟨i, _⟩ => acc + bits[i] * 2^i) 0

Coe in Init.Coe

def blockWords : Vector ℕ 16 := #v[1260152445, 449952550, 2837099038, 716667674, 3544843723, 387900774, 3257147430, 2088822348, 4202301432, 2249467574, 1521610824, 186847680, 2726995727, 3572868764, 1936257617, 3338044720]

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

instance {F : Type} [Field F] : HasAssertEq (Expression F) F where
  assert_eq := Expression.assertEquals

instance : ToJson (TableOperation S F) where
  toJson
    | .boundary i c => Json.mkObj [
      ("type", Json.str "Boundary"),
      ("row", reprStr i),
      ("context", toJson c)
    ]
    | .everyRow c => Json.mkObj [
      ("type", Json.str "EveryRow"),
      ("context", toJson c)
    ]
    | .everyRowExceptLast c => Json.mkObj [
      ("type", Json.str "EveryRowExceptLast"),
      ("context", toJson c)
    ]

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

def round (state : Vector ℕ 16) (m : Vector ℕ 16) : Vector ℕ 16 :=
  roundConstants.foldl (fun state (a, b, c, d, i, j) =>
    g state a b c d m[i] m[j]
  ) state

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

Lean.Json.str in Lean.Data.Json.Basic

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

let out1 ← main input1
    let out2 ← main input2

Vector.attachWith in Init.Data.Vector.Attach

for fvarId in fvarIds do
      let localDecl ← fvarId.getDecl
      let userName := localDecl.userName

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

def Spec (input : Inputs (F p)) (out : BLAKE3State (F p)) :=
  let { state, chaining_value } := input
  out.value = finalStateUpdate state.value (chaining_value.map U32.value) ∧ out.Normalized

Spec
  | instruction, output =>
    match Spec.decodeInstruction instruction with
    | some (instr_type, mode1, mode2, mode3) =>
      output.instrType.val = instr_type ∧ output.instrType.isEncodedCorrectly ∧
      output.mode1.val = mode1 ∧ output.mode1.isEncodedCorrectly ∧
      output.mode2.val = mode2 ∧ output.mode2.isEncodedCorrectly ∧
      output.mode3.val = mode3 ∧ output.mode3.isEncodedCorrectly
    | none => False

localLength n :=
    let a := output f n
    localLength f n + localLength (g a) (n + localLength f n)

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

def splitIntoBlockWords (bytes : List ℕ) : (List (Vector ℕ 16) × List ℕ) :=
  splitIntoBlockWords.go bytes []
where

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

completeness := by admit /- proof elided -/

Nat.toUInt64 in Init.Data.UInt.BasicAux

instance : ProvableStruct Outputs where
  components := [field, field]
  toComponents := fun { low, high } => .cons low (.cons high .nil)
  fromComponents := fun (.cons low (.cons high .nil)) => { low, high }

instance {F : Type} [Field F] {n : ℕ} : HasAssignEq (Vector (Expression F) n) F :=
  inferInstanceAs (HasAssignEq (fields n (Expression F)) F)

instance {F : Type} [Field F] {α : TypeMap} [ProvableType α] :
  HasAssignEq (α (Expression F)) F where
  assignEq := fun rhs => do
    let witness ← ProvableType.witness fun env => eval env rhs
    witness === rhs
    return witness

Lean.Json in Lean.Data.Json.Basic

@[reducible]
def fieldPair : TypeMap := fun F => F × F

instance [Field F] : CoeFun (Environment F) (fun _ => (Expression F) → F) where
  coe env x := x.eval env

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

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

@[table_norm, table_assignment_norm]
def assign (off : CellOffset W S) : Expression F → TableConstraint W S F Unit
  
  | .var v => assignVar off v
  
  | x => do
    let new_var ← witnessVar x.eval
    assertZero (x - var new_var)
    assignVar off new_var

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

OfNat in Init.Prelude

private def isStructLiteral (e : Expr) : MetaM Bool := do
  
  try
    let type ← inferType e
    if ← hasProvableStructInstance type then
      
      isMkConstructor e
    else
      return false
  catch _ => return false

UInt64.ofNat in Init.Data.UInt.BasicAux

Nat.decLt in Init.Prelude

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

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)

structure DecodedAddressingMode (F : Type) where
  isDoubleAddressing : F
  isApRelative : F
  isFpRelative : F
  isImmediate : F

Vector.zero in Init.Data.Vector.Algebra

CoeDep in Init.Coe

def add8Table : List (TableOperation RowType (F p)) := [
  .everyRow add8Inline
]

def sixRoundsApplyStyle : FormalCircuit (F p) Round.Inputs Round.Inputs :=
  sixRoundsWithPermute.weakenSpec SixRoundsSpec (by admit /- proof elided -/
  )

def outLen : ℕ := 32

instance : ProvableType State where
  size := 3
  toElements := fun { pc, ap, fp } => #v[pc, ap, fp]
  fromElements := fun elements => {
    pc := elements[0],
    ap := elements[1],
    fp := elements[2]
  }

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

def FormalCircuit.concat
    {F : Type} [Field F]
    {Input Mid Output : TypeMap} [ProvableType Input] [ProvableType Mid] [ProvableType Output]
    (circuit1 : FormalCircuit F Input Mid)
    (circuit2 : FormalCircuit F Mid Output)
    (h_compat : ∀ input mid, circuit1.Assumptions input → circuit1.Spec input mid → circuit2.Assumptions mid)
    (h_localLength_stable : ∀ mid mid', circuit2.localLength mid = circuit2.localLength mid') :
    FormalCircuit F Input Output := {
  elaborated := {
    main := (circuit1 · >>= circuit2)
    localLength input := circuit1.localLength input + circuit2.localLength (circuit1.output input 0)
    localLength_eq := by admit /- proof elided -/

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

for (eqExpr, _, _) in equalities do
          
          if let some typeExpr := eqExpr.getArg? 0 then
            
            let typeExpr' ← whnf typeExpr
            match typeExpr'.getAppFn with
            | .const typeName _ =>
              
              let mkInjEqName := typeName ++ `mk ++ `injEq
              if env.contains mkInjEqName then
                
                
                if ← hasProvableStructInstance typeExpr' then
                  let lemmaIdent := mkIdent mkInjEqName
                  if !lemmasToApply.any (fun l => l.getId == mkInjEqName) then
                    lemmasToApply := lemmaIdent :: lemmasToApply
            | _ => pure ()

def femtoCairoStepElaboratedCircuit
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p)
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p)) (h_memorySize : memorySize < p) :
    ElaboratedCircuit (F p) State State where
    main := fun state => do
      
      let { rawInstrType, op1, op2, op3 } ← subcircuitWithAssertion (fetchInstructionCircuit program h_programSize) state.pc

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

LawfulMonad in Init.Control.Lawful.Basic

def main (ct : ℕ) (input : Vector (Expression (F p)) 254) := do
  let parts : fields 127 (Expression (F p)) <== Vector.ofFn fun i =>
    let clsb := (ct >>> (i.val * 2)) &&& 1
    let cmsb := (ct >>> (i.val * 2 + 1)) &&& 1
    let slsb := input[i.val * 2]
    let smsb := input[i.val * 2 + 1]

Array.mapM in Init.Data.Array.Basic

Prod.mk in Init.Prelude

def circuit : FormalCircuit (F p) field field where
  main
  localLength _ := 2

Lean.Elab.Tactic.withMainContext in Lean.Elab.Tactic.Basic
</all_available_defs>

<all_available_lemmas>
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 output_eq :
  (xs.foldlM circuit init).output n =
    Fin.foldl m (fun acc i => (circuit acc xs[i.val]).output (n + i * constant.localLength)) init

theorem xor_le_add {x y : ℕ} (hx : x < 256) (hy : y < 256) : x ^^^ y ≤ x + y

@[circuit_norm]
theorem forAll_empty {condition : Condition F} {n : ℕ} : forAll n condition [] = True

theorem completeness : Completeness (F p) elaborated Assumptions

theorem test_struct_literal_eq_literal {F : Type} [Field F]
    (h : (TestInputs.mk 1 2 3 : TestInputs F) = TestInputs.mk 4 5 6) :
    (1 : F) = 4

theorem funext_heq {α α' β : Type} (h : α = α') {f : α → β} {g : α' → β} :
    (∀ x : α, f x = g (cast h x)) → HEq f g

@[circuit_norm ↓]
theorem varFromOffset_field {F} (offset : ℕ) :
  varFromOffset (F:=F) field offset = var ⟨offset⟩

theorem cast_drop_append_of_eq_length {v : Vector α n} {w : Vector α m} :
    (v ++ w |>.drop n |>.cast (Nat.add_sub_self_left n m)) = w

lemma fromElements_eq_iff' {M : TypeMap} [ProvableType M] {F : Type} {B : Vector F (size M)} {A : M F} :
    A = fromElements B ↔ toElements A = B

@[circuit_norm ↓]
lemma mapFinRange.output_eq :
  (mapFinRange m body constant).output n =
    Vector.mapFinRange m fun i => (body i).output (n + i*(body 0).localLength)

theorem usesLocalWitnesses_iff_forAll (n : ℕ) {env : Environment F} {ops : Operations F} :
  env.UsesLocalWitnesses n ops ↔ ops.forAll n {
    witness n _ c := env.ExtendsVector (c env) n,
    subcircuit n _ s := FlatOperation.forAll n { witness n _ c := env.ExtendsVector (c env) n} s.ops
  }

private lemma ZMod_val_chunkEnd :
    ZMod.val (n:=p) ↑chunkEnd = 2

theorem bind_forAll' {f : Circuit F α} {g : α → Circuit F β} :
  (f >>= g).forAll n prop ↔
    f.forAll n prop ∧ ((g (f.output n)).forAll (n + f.localLength n) prop)

lemma sum_count_pairs_snd (xs : List (S × S)) (b : S) :
    ∑ a : S, List.count (a, b) xs = List.countP (fun p => p.2 = b) xs

lemma value_of_decomposedNat_of_small (x : ℕ) :
    x < 256^4 ->
    (decomposeNat (p:=p) x).value = x

theorem soundness : Soundness (F p) elaborated Assumptions Spec

lemma pushRow_offset (assignment : CellAssignment W S) (row : Fin W) :
  (assignment.pushRow row).offset = assignment.offset + size S

@[circuit_norm ↓]
lemma mapFinRange.forAll :
  Operations.forAll n prop (mapFinRange m body constant |>.operations n) ↔
    ∀ i : Fin m, (body i |>.forAll (n + i*(body 0).localLength) prop)

lemma nodup_transition_count_le_one (path : List S) (h_nodup : path.Nodup)
    (t : Transition S) :
    countTransitionInPath t path ≤ 1

theorem test_decompose_nested_hypothesis {F : Type} [Field F] (input : NestedInputs F)
    (h : input.first.x = 7) : input.second.y = input.second.y

@[circuit_norm ↓ high]
theorem eval_field {F : Type} [Field F] (env : Environment F) (x : Var field F) :
  ProvableType.eval env x = Expression.eval env x

lemma foldl_sum_val_bound {p : ℕ} [Fact p.Prime] {ops : ℕ} (f : Fin ops → ZMod p) (M : ℕ)
    (h_bound : ∀ j : Fin ops, (f j).val ≤ M) (h_no_overflow : ops * M < p) :
    (Fin.foldl ops (fun sum j => sum + f j) 0).val ≤ ops * M

theorem getElemFin_finRange {n} (i : Fin n) : (finRange n)[i] = i

theorem completeness : Completeness (F p) elaborated Assumptions

@[circuit_norm]
lemma FormalCircuit.concat_assumptions {F Input Mid Output} [Field F] [ProvableType Input] [ProvableType Mid] [ProvableType Output]
    (c1 : FormalCircuit F Input Mid) (c2 : FormalCircuit F Mid Output) p0 p1 :
    (c1.concat c2 p0 p1).Assumptions = c1.Assumptions

lemma head_pair_not_in_tail_zip {α : Type*} [DecidableEq α] (h : α) (t : List α)
    (h_not_in : h ∉ t) :
    ∀ h2, (h, h2) ∉ t.zip t.tail

theorem completeness : Completeness (F p) elaborated Assumptions

theorem equalityConstraint.soundness {row : State F × Input F} {input_state : State F} {env : Environment F} :
  Circuit.ConstraintsHold.Soundness (windowEnv (equalityConstraint Input input_state) ⟨<+> +> row, rfl⟩ env)
    (equalityConstraint Input input_state .empty).2.circuit
    ↔ row.1 = input_state

lemma h_div {o : ℕ} (ho : o < 8) {x0 x1 x2 x3 x4 x5 x6 x7 : ℕ} :
    (x0 + x1 * 256 + x2 * 256^2 + x3 * 256^3 + x4 * 256^4 + x5 * 256^5 + x6 * 256^6 + x7 * 256^7) / 2 ^ o
    = x0 / 2^o + x1 * 2^(8-o) + x2 * 256 * 2^(8-o) + x3 * 256^2 * 2^(8-o) + x4 * 256^3 * 2^(8-o) +
    x5 * 256^4 * 2^(8-o) + x6 * 256^5 * 2^(8-o) + x7 * 256^6 * 2^(8-o)

@[circuit_norm ↓]
lemma foldl.soundness [NeZero m] :
  ConstraintsHold.Soundness env (foldl xs init body const_out constant |>.operations n) ↔
    ConstraintsHold.Soundness env (body init (xs[0]'(NeZero.pos m)) |>.operations n) ∧
    ∀ (i : ℕ) (hi : i + 1 < m),
      let acc := (body default xs[i]).output (n + i*(body default default).localLength);
      ConstraintsHold.Soundness env (body acc xs[i + 1] |>.operations (n + (i + 1)*(body default default).localLength))

omit p_large_enough in
@[circuit_norm]
lemma value_zero_iff_zero {x : U32 (F p)} (hx : x.Normalized) :
    x.value = 0 ↔ x = U32.mk 0 0 0 0

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

lemma mapM_cons (xs : Vector α n) (body : α → Circuit F β) (x : α) :
  (Vector.cons x xs).mapM body = do
    let y ← body x
    let ys ← xs.mapM body
    return Vector.cons y ys

lemma acyclic_has_leaf (R : Run S) (root : S)
    (h_acyclic : R.isAcyclic)
    (h_has_out : ∃ y, R (root, y) > 0) :
    ∃ leaf, R.isLeaf root leaf

theorem soundness : Soundness (F p) elaborated Assumptions Spec

lemma two_cycle_contains_both_edges (R : Run S) (a b : S)
    (h_ne : a ≠ b)
    (h_edge1 : R (a, b) > 0) (h_edge2 : R (b, a) > 0) :
    ∀ t : Transition S, countTransitionInPath t [a, b, a] ≤ R t

theorem test_decompose_multiple_hypotheses {F : Type} [Field F] (a : TestInputs F) (b : TestInputs F)
    (h1 : a.x = b.y) (h2 : b.z = 10) : a.x = a.x

theorem rotRight64_lt (x r : ℕ) (h : x < 2^64) :
    rotRight64 x r < 2^64

lemma rotRight64_bytes_u64_eq (o : ℕ) (x : U64 ℕ) :
  rotRight64_bytes x.toLimbs o = (rotRight64_u64 x o).toLimbs

theorem map_localLength_eq (f : Circuit F α) (g : α → β) (n : ℕ) :
  (g <$> f).localLength n = f.localLength n

theorem MemoryAccessList.isConsistentSingleAddress_cons (head : MemoryAccess) (tail : MemoryAccessList)
    (h_sorted : isTimestampSorted (head :: tail)) (h_sorted' : tail.isTimestampSorted)
    (h : isConsistentSingleAddress (head :: tail) h_sorted) :
    isConsistentSingleAddress tail h_sorted'

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

lemma fieldFromBits_as_sum {n : ℕ} (bits : Vector (F p) n) :
    fieldFromBits bits =
    Fin.foldl n (fun acc k => acc + bits[k.val] * (2^k.val : F p)) 0

theorem test_decompose_mixed_auto {F : Type} [Field F] (a : TestInputs F) (b : NestedInputs F) :
    a.x + b.first.y = b.first.y + a.x

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

theorem operations_eq :
  (Vector.foldlM circuit init xs).operations n =
    (List.ofFn fun i => (circuit (foldlAcc n xs circuit init i) xs[i.val]).operations (n + i * constant.localLength)).flatten

theorem and_mul_two_pow {x y n : ℕ} : 2 ^ n * (x &&& y) =  2 ^ n * x &&&  2 ^ n * y

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

theorem pure_operations_eq (a : α) (n : ℕ) :
  (pure a : Circuit F α).operations n = []

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

lemma acyclic_has_leaf_aux (R : Run S) (root current : S)
    (path : List S)
    (h_acyclic : R.isAcyclic)
    (h_start : path.head? = some root)
    (h_end : path.getLast? = some current)
    (h_nonempty : path ≠ [])
    (h_contains : R.containsPath path)
    (h_has_out : ∃ y, y ∉ path ∧ R (current, y) > 0) :
    ∃ leaf, R.isLeaf root leaf

@[circuit_norm ↓]
lemma foldlRange.forAll :
  Operations.forAll n prop (foldlRange m init body constant |>.operations n) ↔
    ∀ i : Fin m,
      body (FoldlM.foldlAcc n (Vector.finRange m) body init i) i
      |>.forAll (n + i * (body default i).localLength) prop

theorem completeness (rc : UInt64) : Completeness (F p) (elaborated rc) Assumptions

theorem val_lt_p {p : ℕ} (x : ℕ) : (x < p) → (x : F p).val = x

theorem mod_lt {x : F p} {c : ℕ+} {lt : c < p} : (mod x c lt).val < c

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

lemma initial_state_and_messages_are_normalized
    (env : Environment (F p))
    (input_var : Var Inputs (F p))
    (block_words : BLAKE3State (F p))
    (chaining_value counter_high counter_low block_len flags)
    (h_input : eval env input_var = { chaining_value, block_words, counter_high, counter_low, block_len, flags })
    (h_normalized : Assumptions { chaining_value, block_words, counter_high, counter_low, block_len, flags }) :
    (eval env (initializeStateVector input_var)).Normalized ∧ ∀ (i : Fin 16), block_words[i].Normalized

theorem toChunks_push (m : ℕ+) {α : Type} (vs : Vector α (n*m)) (v : Vector α m) :
    have h : n * m + m = (n + 1) * m

theorem natToField_zero : natToField 0 (p_prime.elim.pos) = 0

lemma localWitnesses_append {F} {a b: List (FlatOperation F)} {env} :
    (localWitnesses env (a ++ b)).toArray = (localWitnesses env a).toArray ++ (localWitnesses env b).toArray

theorem ext_iff {x y : F p} : x = y ↔ x.val = y.val

theorem FormalAssertion.original_completeness (circuit : FormalAssertion F β) :
    ∀ (offset : ℕ) env (b_var : Var β F) (b : β F), eval env b_var = b → circuit.Assumptions b →
    -- if the environment uses default witness generators (original definition)
    env.UsesLocalWitnesses offset (circuit.main b_var |>.operations offset) →
    -- the spec implies that the constraints hold (original definition)
    circuit.Spec b → ConstraintsHold env (circuit.main b_var |>.operations offset)

lemma sum_countTransitionInPath_fst (cycle : List S) (x : S) :
    ∑ y : S, (countTransitionInPath (x, y) cycle : ℤ) = (countAsFirst cycle x : ℤ)

lemma rotRight64_bytes_u64_eq (o : ℕ) (x : U64 ℕ) :
  rotRight64_bytes x.toLimbs o = (rotRight64_u64 x o).toLimbs

theorem MemoryAccessList.filterAddress_cons (head : MemoryAccess) (tail : MemoryAccessList) (addr : ℕ) :
    MemoryAccessList.filterAddress (head :: tail) addr =
    match head with

lemma acyclic_containsPath_nodup (R : Run S) (path : List S)
    (h_acyclic : R.isAcyclic)
    (h_contains : R.containsPath path) :
    path.Nodup

lemma foldlAcc_cons_succ (i : Fin m) (x : α) [constant : ConstantLength (prod circuit)] :
  foldlAcc n (Vector.cons x xs) circuit init i.succ =
    foldlAcc (n + (circuit init x).localLength n) xs circuit ((circuit init x).output n) i

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

theorem forAll_iff_const [NeZero m] (constant : ConstantLength (prod circuit))
    (h_const_out : ConstantOutput (prod circuit)) :
  (xs.foldlM circuit init).forAll n prop ↔
  (circuit init (xs[0]'(NeZero.pos m))).forAll n prop ∧
  ∀ (i : ℕ) (hi : i + 1 < m),
    let acc := (circuit default xs[i]).output (n + i*(circuit default default).localLength);
    (circuit acc xs[i + 1]).forAll (n + (i + 1)*(circuit default default).localLength) prop

theorem completeness : Completeness (F p) elaborated Assumptions

omit [Fact (p > 2)] in
lemma inputLinearSum_eval_eq_sum {n ops : ℕ} [hn : NeZero n]
  (env : Environment (F p))
  (input : Var (BinSumInput n ops) (F p))
  (input_val : BinSumInput n ops (F p))
  (h_eval : eval env input = input_val) :
    Expression.eval env (inputLinearSum n ops input) =
    Fin.foldl ops (fun acc j => acc + fieldFromBits input_val[j.val]) 0

@[circuit_norm]
theorem FormalCircuit.toSubcircuit_soundness
    {F : Type} [Field F] {Input Output : TypeMap} [ProvableType Input] [ProvableType Output]
    (circuit : FormalCircuit F Input Output) (n : ℕ) (input_var : Var Input F) (env : Environment F) :
    (circuit.toSubcircuit n input_var).Soundness env =
    (circuit.Assumptions (eval env input_var) → circuit.Spec (eval env input_var) (eval env (circuit.output input_var n)))

lemma localWitnesses_toFlat {ops : Operations F} {env} :
  (localWitnesses env ops.toFlat).toArray = (ops.localWitnesses env).toArray

theorem mapFinRangeM_forAll_iff {circuit : Fin m → Circuit F β} [constant : ConstantLength circuit] :
  (Vector.mapFinRangeM m circuit).forAll n prop ↔
    ∀ i : Fin m, (circuit i).forAll (n + i*constant.localLength) prop

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

@[circuit_norm] theorem ConstraintsHold.bind_usesLocalWitnesses {f : Circuit F α} {g : α → Circuit F β} (n : ℕ) :
  env.UsesLocalWitnessesCompleteness n ((f >>= g).operations n)
  ↔ env.UsesLocalWitnessesCompleteness n (f.operations n) ∧
    env.UsesLocalWitnessesCompleteness (n + f.localLength n) ((g (f.output n)).operations (n + f.localLength n))

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

<local_ctx>
import Clean.Circuit.Basic

import Clean.Circuit.Provable

variable {F : Type} [Field F] {α β : Type}

namespace Operations

end Operations

namespace Circuit

end Circuit

namespace FlatOperation

end FlatOperation

namespace Environment

open FlatOperation (localLength localWitnesses)

end Environment

namespace Circuit

end Circuit

namespace Circuit

variable {α β : Type} {n : ℕ} {prop : Condition F} {env : Environment F}

end Circuit

namespace FlatOperation

end FlatOperation

namespace Operations
</local_ctx>

<target_theorem>
lemma forAll_toFlat_iff (n : ℕ) (condition : Condition F) (ops : Operations F) :
    FlatOperation.forAll n condition ops.toFlat ↔ ops.forAllFlat n condition :=
</target_theorem>

