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>
class HasAssignEq (β : Type) (F : outParam Type) [Field F] where
  assignEq : β → Circuit F β

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

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

structure Outputs (F : Type) where
  z: F
  carryOut: F

def F p := ZMod p

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

computeNextState instr_type v1 v2 v3 state

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

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

Assumptions input := ∀ i (_ : i < 254), input[i] = 0 ∨ input[i] = 1

def circuit : FormalCircuit (F p) Inputs field where
  main := fun { x, y } =>
    Addition8Full.circuit { x, y, carryIn := 0 }

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

instance {m : ℕ} : Witnessable F (Vector · m) (fun F => Vector (Expression F) m) where
  witness := witnessVector m

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

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

Lean.Elab.Tactic.getMainGoal in Lean.Elab.Tactic.Basic

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

HXor.hXor in Init.Prelude

def decomposeNatNat (x : ℕ) : U32 ℕ :=
  let x0 := x % 256
  let x1 : ℕ := (x / 256) % 256
  let x2 : ℕ := (x / 256^2) % 256
  let x3 : ℕ := (x / 256^3) % 256
  ⟨ x0, x1, x2, x3 ⟩

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

let fvarIds ← findProvableStructVars

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

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

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 : ProvableStruct RowType where
  components := [U32, U32]
  toComponents := fun { x, y } => .cons x (.cons y .nil)
  fromComponents := fun (.cons x (.cons y .nil)) => { x, y }
  combinedSize := 8

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

def boundary : SingleRowConstraint RowType (F p) := do
  let row ← TableConstraint.getCurrRow
  row.x === (const (U32.fromByte 0))
  row.y === (const (U32.fromByte 1))

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

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

List.cons in Init.Prelude

Permutation.circuit state'

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

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

def fibRelation : TwoRowsConstraint RowType (F p) := do
  let curr ← TableConstraint.getCurrRow
  let next_x ← copyToVar curr.y
  let next_y ← Gadgets.Addition8.circuit { x := curr.x, y := curr.y }
  assignVar (.next 0) next_x
  assign (.next 1) next_y

def circuit : FormalCircuit (F p) Inputs field where
  main := main

instance : ToJson (CellAssignment W S) where
  toJson assignment :=
    let aux_map := buildAuxMap assignment
    
    let vars := assignment.vars.mapIdx fun idx cell =>
      match cell with
      | Cell.input off => Cell.input off
      | Cell.aux _ =>
        let col := aux_map[idx]!
        if h: col < (size S)
          then Cell.input { row := 1, column := ⟨col, h⟩ }
          else cell

def computeNextState
    (instr_type : ℕ) (v1 : (F p)) (v2 : (F p)) (v3 : (F p))
    (state : State (F p)) :
    Option (State (F p)) :=
  match instr_type with
  
  | 0 => if v1 + v2 = v3 then
            some { pc := state.pc + 4, ap := state.ap, fp := state.fp }
         else
            none
  
  | 1 => if v1 * v2 = v3 then
            some { pc := state.pc + 4, ap := state.ap, fp := state.fp }
          else
            none
  
  | 2 => if v1 = state.pc ∧ v2 = state.ap ∧ v3 = state.fp then
            some { pc := state.pc + 4, ap := state.ap, fp := state.fp }
          else
            none
  
  | 3 => some { pc := v1, ap := v2, fp := v3 }
  
  | _ => none

Fin in Init.Prelude

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 }

def fib8json := Lean.toJson (Tables.Fibonacci8Table.fibTable (p:=pBabybear))

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

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

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

Lean.Meta.trySynthInstance in Lean.Meta.SynthInstance

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

def blockLen : ℕ := 64

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

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

def testChunk65 : List ℕ := List.range 65

instance {α β: TypeMap} [ProvableType α] [NonEmptyProvableType β] :
  NonEmptyProvableType (ProvablePair α β) where
  nonempty := by admit /- proof elided -/

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

LawfulMonad in Init.Control.Lawful.Basic

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

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

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

soundness := by admit /- proof elided -/

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

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

Neg in Init.Prelude

Or.inl in Init.Prelude

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)

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

Bits2Num.main 254 input

instance [Repr F] : Repr (FlatOperation F) where
  reprPrec
  | witness m _, _ => "(Witness " ++ reprStr m ++ ")"
  | assert e, _ => "(Assert " ++ reprStr e ++ " == 0)"
  | lookup l, _ => reprStr l

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

List.count in Init.Data.List.Basic

def main (input : Var Inputs (F p)) : Circuit (F p) (Var U32 (F p)) := do
  let ⟨x, y⟩ := input
  let ⟨z, _⟩ ← Addition32Full.circuit {x, y, carryIn := 0}
  return z

@[reducible]
def combinedSize' (cs : List WithProvableType) : ℕ := cs.map (fun x => x.provableType.size) |>.sum

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

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
  ]

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

Add in Init.Prelude

CommSemiring in Mathlib.Algebra.Ring.Defs

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

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

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

def roundWithPermute (acc : Vector ℕ 16 × Vector ℕ 16) (round_num : ℕ) : Vector ℕ 16 × Vector ℕ 16 :=
  let (state, block_words) := acc
  let new_state := round state block_words
  
  let new_block_words := if round_num < 6 then permute block_words else block_words
  (new_state, new_block_words)

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

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

for (_, lhs, rhs) in equalities do
        
        let lhsIsConstructor ← isMkConstructor lhs
        let rhsIsConstructor ← isMkConstructor rhs

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

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

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

def msgPermutation : Vector (Fin 16) 16 :=

instance [Repr F] : Repr (Expression F) where
  reprPrec e _ := toString e

replaceMainGoal [currentGoal]

@[reducible] def fieldVar (F : Type) := field (Expression F)

@[table_assignment_norm]
def pushVarsAux (assignment : CellAssignment W S) (n : ℕ) : CellAssignment W S where
  offset := assignment.offset + n
  aux_length := assignment.aux_length + n
  vars := assignment.vars ++ (.mapRange n fun i => .aux (assignment.aux_length + i) : Vector (Cell W S) n)

soundness : InductiveTable.Soundness F State Input Spec step

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

structure Inputs (F : Type) where
  enabled : F
  inp : fieldPair F

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

inferInstanceAs in Init.Prelude

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

def fetchInstructionCircuit
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p) :
    GeneralFormalCircuit (F p) field RawInstruction where
  main := fun pc => do
    let programTable := ReadOnlyTableFromFunction program h_programSize

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

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

HXor in Init.Prelude

replaceMainGoal [currentGoal]

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

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 circuit (n : ℕ) : FormalCircuit (F p) (Inputs n) (fields n) where
  main := main n

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

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

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

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

def Operations.witnessGenerators : (ops : Operations F) → Vector (Environment F → F) ops.localLength
  | [] => #v[]
  | .witness m c :: ops => Vector.mapFinRange m (fun i env => (c env)[i.val]) ++ witnessGenerators ops
  | .assert _ :: ops => witnessGenerators ops
  | .lookup _ :: ops => witnessGenerators ops
  | .subcircuit s :: ops => (s.localLength_eq ▸ FlatOperation.witnessGenerators s.ops) ++ witnessGenerators ops

let out1 ← main input1
    let out2 ← main input2

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

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

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

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

def FlatOperation.proverEnvironment (ops : List (FlatOperation F)) (init : List F) : Environment F :=
  .fromList (FlatOperation.dynamicWitnesses ops init)

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

instance {n : ℕ} : ProvableStruct (Inputs n) where
  components := [ProvableVector (fields 8) n, fields 3]
  toComponents := fun {c, s} => .cons c (.cons s .nil)
  fromComponents := fun (.cons c (.cons s .nil)) => ⟨c, s⟩

instance : ToJson (Operations F) where
  toJson ops := toJson ops.toList

@[reducible] def KeccakBlock := ProvableVector U64 RATE

def applyFourRounds (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
  let state3 := round state2 msg2
  let msg3 := permute msg2
  let state4 := round state3 msg3
  let msg4 := permute msg3
  (state4, msg4)

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

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

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

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

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

def main (input : Vector (Expression (F p)) 254) := do
  
  let comp_out ← CompConstant.circuit (p - 1) input
  comp_out === 0

def constantOutput (circuit : LookupCircuit F α β) (input : α F) : β F :=
  circuit.output (const input) 0 |> eval (circuit.proverEnvironment 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)

Spec input output :=
    
    
    output = if Utils.Bits.fromBits (input.map ZMod.val) > (p - 1) / 2 then 1 else 0

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

output_eq : ∀ n : ℕ, circuit.output n = output n := by admit /- proof elided -/

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

return U32.fromLimbs rotated

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

def ForAllRowsWithPrevious {N : ℕ}
    (trace : TraceOfLength F S N) (prop : Row F S → (i : ℕ) → TraceOfLength F S i → Prop) : Prop :=
  trace.val.ForAllRowsWithPrevious fun row rest => prop row rest.len ⟨ rest, rfl ⟩

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' }

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

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

def ProvablePair.toElements {α β: TypeMap} [ProvableType α] [ProvableType β] (pair : α F × β F) : Vector F (size α + size β) :=
  ProvableType.toElements (M:=ProvablePair α β) pair

def rhoPiConstants := rhoPiIndices.zip rhoPiShifts

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

def pBabybear := 15 * 2^27 + 1

instance : NonEmptyProvableType fieldPair where

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

@[reducible] def circuit32 input := Gadgets.Addition32Full.main (p:=pBabybear) input

localLength _ := nbits ((2^n - 1) * ops)
  localLength_eq := by admit /- proof elided -/

if lhsIsConstructor && !rhsIsConstructor then
          
          match rhs with
          | .fvar fvarId =>
            
            let varType ← inferType rhs
            if ← hasProvableStructInstance varType then
              structVarsToCase := fvarId :: structVarsToCase
          | _ => pure ()
        else if rhsIsConstructor && !lhsIsConstructor then
          
          match lhs with
          | .fvar fvarId =>
            
            let varType ← inferType lhs
            if ← hasProvableStructInstance varType then
              structVarsToCase := fvarId :: structVarsToCase
          | _ => pure ()

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

let 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 (n : ℕ) (hn : 2^(n+1) < p) : FormalCircuit (F p) fieldPair field where
  main := fun (x, y) =>
    LessThan.circuit n hn (y, x)

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

instance : NonEmptyProvableType U32 where
  nonempty := by admit /- proof elided -/

contains_iff := by admit /- proof elided -/

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

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

instance : ProvableStruct NestedInputs where
  components := [TestInputs, TestInputs]
  toComponents := fun { first, second } => .cons first (.cons second .nil)
  fromComponents := fun (.cons first (.cons second .nil)) => { first, second }

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 ⟩

localLength : Var Input F → ℕ

def valueU64 (x : U64 (F p)) (h : x.Normalized) : UInt64 :=
  UInt64.ofNatLT x.value (value_lt_of_normalized h)

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

Lean.MonadLCtx.getLCtx in Lean.LocalContext

def lookupCircuit : LookupCircuit (F p) Inputs Outputs := {
  circuit with
  name := "Addition8FullCarry"

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

instance : Sub (Expression F) where
  sub e₁ e₂ := add e₁ (-e₂)

Mul in Init.Prelude

UInt16 in Init.Prelude

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

instance : One (Expression F) where
  one := const 1

Fact in Mathlib.Logic.Basic

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

@[circuit_norm]
def ProvableVector.witness {α : TypeMap} [NonEmptyProvableType α] (m : ℕ)
    (compute : Environment F → Vector (α F) m) : Circuit F (Vector (α (Expression F)) m) :=
  ProvableType.witness (α:=ProvableVector α m) compute

def KeccakRow.normalized_iff (row : KeccakRow (F p)) :
    row.Normalized ↔
    row[0].Normalized ∧
    row[1].Normalized ∧
    row[2].Normalized ∧
    row[3].Normalized ∧
    row[4].Normalized :=

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

def main (x : Var ProcessBlocksState (F p)) : Circuit (F p) Unit := do
  Circuit.forEach x.chaining_value U32.AssertNormalized.circuit
  U32.AssertNormalized.circuit x.chunk_counter
  U32.AssertNormalized.circuit x.blocks_compressed

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

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

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

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

let state_a ← Addition32.circuit ⟨state[a], ← Addition32.circuit ⟨state[b], x⟩⟩

def FourRoundsSpec (input : Round.Inputs (F p)) (output : Round.Inputs (F p)) : Prop :=
  let (final_state, final_message) := applyFourRounds input.state.value (input.message.map U32.value)
  output.state.value = final_state ∧
  output.message.map U32.value = final_message ∧
  output.state.Normalized ∧
  (∀ i : Fin 16, output.message[i].Normalized)

class NonEmptyProvableType (M : TypeMap) extends ProvableType M where
  nonempty : size > 0 := by admit /- proof elided -/

def Assumptions (input : Inputs (F p)) :=
  let ⟨x, y, carryIn⟩ := input
  x.val < 256 ∧ y.val < 256 ∧ IsBool carryIn

UInt32.toNat 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

Sub in Init.Prelude

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

Lean.Meta.whnf in Lean.Meta.Basic

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

instance : ToJson (Lookup F) where
  toJson l := Json.mkObj [
    ("table", toJson l.table.name),
    ("entry", toJson l.entry.toArray),
  ]

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

@[table_norm, table_assignment_norm]
def assignNextRow {W : ℕ+} (next : Var S F) : TableConstraint W S F Unit :=
  let vars := toVars next
  forM (List.finRange (size S)) fun i =>
    assign (.next i) vars[i]

instance : ToJson (Expression F) where
  toJson := exprToJson

IO in Init.System.IO

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

output_eq n := by admit /- proof elided -/

Spec input output :=
    output = (if input = 0 then 1 else 0)

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

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

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

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

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

def update (v : Vector α n) (i : Fin n) (f : α → α) : Vector α n :=
  v.set i (f (v.get i))

instance (p : ℕ) [Fact p.Prime] : Inhabited (F p) := ⟨0⟩

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

instance elaborated : ElaboratedCircuit (F p) Inputs U32 where
  main := main
  localLength _ := 4
  output _ i0 := varFromOffset U32 i0

instance elaborated : ElaboratedCircuit (F p) Inputs U64 where
  main := main
  localLength _ := 8
  output _ i0 := varFromOffset U64 i0

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 ⟩

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

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

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

Fin.ofNat in Init.Data.Fin.Basic

example : ExplicitCircuit.localLength (circuit32 default) 0 = 8 :=

instance : ToJson (CellOffset W S) where
  toJson off := Json.mkObj [
    ("row", off.row),
    ("column", off.column)
  ]

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

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

Inv in Init.Prelude

CoeFun in Init.Coe

return out
</all_available_defs>

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

lemma acyclic_run_has_path_from_source_to_sink (R : Run S) (s d : S)
    (h_acyclic : R.isAcyclic)
    (h_source : R.netFlow s = 1)
    (h_others : ∀ x, x ≠ s → x ≠ d → R.netFlow x = 0) :
    ∃ (path : List S), path.head? = some s ∧ path.getLast? = some d ∧
      path ≠ [] ∧ R.containsPath path ∧ path.Nodup

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

theorem MemoryAccessList.isAddressTimestampSorted_of_cons (head : MemoryAccess) (tail : MemoryAccessList)
    (h : isAddressTimestampSorted (head :: tail)) :
    isAddressTimestampSorted tail

theorem soundness : Soundness (F p) elaborated Assumptions Spec

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

theorem toLimbs_fromLimbs {F} (v : Vector F 8) :
    (U64.fromLimbs v).toLimbs = v

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

lemma thetaC_loop (state : Vector ℕ 25) :
    Specs.Keccak256.thetaC state = .mapFinRange 5 fun i =>
      state[5*i.val] ^^^ state[5*i.val + 1] ^^^ state[5*i.val + 2] ^^^ state[5*i.val + 3] ^^^ state[5*i.val + 4]

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

theorem proverEnvironment_usesLocalWitnesses {ops : List (FlatOperation F)} (init : List F) :
  (∀ (env env' : Environment F),
    forAll init.length { witness n _ c := env.AgreesBelow n env' → c env = c env' } ops) →
    (proverEnvironment ops init).UsesLocalWitnessesFlat init.length ops

lemma Vector.mapRange_one {α : Type} (f : ℕ → α) :
  Vector.mapRange 1 f = #v[f 0]

theorem value_fromUInt64 (x : UInt64) : value (fromUInt64 (p:=p) x) = x.toNat

private theorem or_times_two_sub_xor {x y : ℕ} (hx : x < 256) (hy : y < 256) :
    2 * (x ||| y) = x + y + (x ^^^ y)

lemma Vector.toList_mapM (xs : Vector α n) {m : Type → Type} [monad: Monad m] [LawfulMonad m] (body : α → m β) :
    Vector.toList <$> (xs.mapM body) = xs.toList.mapM body

@[circuit_norm ↓]
lemma foldlRange.localLength_eq :
    (foldlRange m init body constant).localLength n =
      if h : m > 0 then m * (body default ⟨0, h⟩).localLength else 0

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

lemma boundary_constraints (first_row : Row (F p) RowType) (aux_env : Environment (F p)) :
  Circuit.ConstraintsHold.Soundness (windowEnv boundary ⟨<+> +> first_row, rfl⟩ aux_env) boundary.operations →
  first_row.x.value = fib32 0 ∧ first_row.y.value = fib32 1 ∧ first_row.x.Normalized ∧ first_row.y.Normalized

@[circuit_norm ↓]
lemma mapFinRange.soundness :
  ConstraintsHold.Soundness env (mapFinRange m body constant |>.operations n) ↔
    ∀ i : Fin m, ConstraintsHold.Soundness env (body i |>.operations (n + i*(body 0).localLength))

omit p_large_enough in
@[circuit_norm]
lemma eval_of_literal (env : Environment (F p)) (a b c d : Var field (F p)) :
    eval env (U32.mk a b c d) =
    U32.mk (eval env a) (eval env b) (eval env c) (eval env d)

theorem rotate_rotate {α : Type} {n : ℕ} (v : Vector α n) (off1 off2 : ℕ) :
    v.rotate (off1 + off2) = (v.rotate off1).rotate off2

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)

theorem MemoryAccessList.isConsistentOffline_iff_all_single_addresses (accesses : MemoryAccessList) (h_sorted : accesses.isAddressTimestampSorted) (h_nodup : accesses.Notimestampdup) :
    MemoryAccessList.isConsistentOffline accesses h_sorted ↔
    ∀ addr, MemoryAccessList.isConsistentSingleAddress (MemoryAccessList.filterAddress accesses addr) (filterAddress_sorted_from_addressTimestampSorted accesses h_sorted h_nodup addr)

lemma rotRight64_testBit_of_lt (x r i : ℕ) (h : x < 2^64) (hi : i < 64 - r % 64) :
    (rotRight64 x r).testBit i = x.testBit (r % 64 + i)

private lemma ZMod_val_64 :
    ZMod.val (n:=p) 64 = 64

@[circuit_norm ↓ high]
theorem eval_pair_right_vector_expr {n : ℕ} {α : TypeMap} [ProvableType α] (env : Environment F)
  (a : Var α F) (b : Vector (Expression F) n) :
    eval (α:=ProvablePair α (fields n)) env (a, b) = (eval env a, eval env b)

lemma ConstantLength.length_eq_default {circuit : α → Circuit F β} (_ : ConstantLength circuit) [Inhabited α] (a : α) (n : ℕ) :
   (circuit a).localLength n = (circuit default).localLength 0

theorem not_eq_val_not {a : F p} (ha : IsBool a) :
    (1 - 2*a + a).val = 1 - a.val

private theorem or_times_two_sub_xor' {x y : ℕ} (hx : x < 256) (hy : y < 256) :
    2 * (x ||| y) - x - y = (x ^^^ y)

theorem nor_eq_val_nor {a b : F p} (ha : IsBool a) (hb : IsBool b) :
    (a * b + 1 - a - b).val = 1 - (a.val ||| b.val)

lemma size_removeCycle_lt (R : Run S) (cycle : List S)
    (h_len : cycle.length ≥ 2)
    (h_contains : R.containsPath cycle)
    (_h_cycle : cycle.head? = cycle.getLast?) :
    (R.removeCycle cycle).size < R.size

lemma rotRight32_def (x : ℕ) (off : ℕ) (hx : x < 2^32) :
    rotRight32 x off = x >>> (off % 32) ||

lemma Fin.foldl_eq_foldl_finRange (n : ℕ) (f : α → Fin n → α) (init : α) :
    Fin.foldl n f init = (List.finRange n).foldl f init

theorem completeness : Completeness (F p) elaborated Assumptions

theorem MemoryAccessList.addressStrictTimestampSorted_of_AddressTimestampSorted_noTimestampDup
    (accesses : MemoryAccessList) (h_sorted : accesses.isAddressTimestampSorted)
    (h_no_timestamp_dup : accesses.Notimestampdup) :
    accesses.isAddressStrictTimestampSorted

theorem and_eq_val_and {a b : F p} (ha : IsBool a) (hb : IsBool b) :
    (a * b).val = a.val &&& b.val

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

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

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

lemma h_mod {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

theorem not_zify (n : ℕ) {x : ℕ} (hx : x < n) : ((n - 1 - x : ℕ) : ℤ) = ↑n - 1 - ↑x

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

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

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 drop_of_lt_length_nonempty {α : Type*} (path : List α) (i : ℕ)
    (h_i_lt : i < path.length) :
    path.drop i ≠ []

theorem ConstraintsHold.soundness_iff_forAll (n : ℕ) (env : Environment F) (ops : Operations F) :
  ConstraintsHold.Soundness env ops ↔ ops.forAll n {
    assert _ e := env e = 0,
    lookup _ l := l.table.Soundness (l.entry.map env),
    subcircuit _ _ s := s.Soundness env
  }

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

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

lemma h_x0_const {o : ℕ} (ho : o < 8) :
    2^(8-o) * 256^7 = 2^(64-o)

@[circuit_norm]
theorem FormalAssertion.toSubcircuit_usesLocalWitnesses
    {F : Type} [Field F] {Input : TypeMap} [ProvableType Input]
    (circuit : FormalAssertion F Input) (n : ℕ) (input_var : Var Input F) (env : Environment F) :
    (circuit.toSubcircuit n input_var).UsesLocalWitnesses env = True

theorem mapM_singleton (a : α) {m : Type → Type} [Monad m] [LawfulMonad m] (f : α → m β) :
    #v[a].mapM f = (do pure #v[←f a])

theorem MemoryAccessList.isConsistentOffline_implies_single_address
    (accesses : MemoryAccessList)
    (h_sorted : accesses.isAddressTimestampSorted)
    (h_nodup : accesses.Notimestampdup)
    (h_offline : accesses.isConsistentOffline h_sorted)
    (addr : ℕ) :
    (accesses.filterAddress addr).isConsistentSingleAddress
      (filterAddress_sorted_from_addressTimestampSorted accesses h_sorted h_nodup addr)

lemma Vector.foldlM_toList (xs : Vector α n) {m : Type → Type} [Monad m] (body : β → α → m β) (init : β) :
    xs.foldlM body init = xs.toList.foldlM body init

@[circuit_norm]
theorem one {α : Type*} [Zero α] [One α] : IsBool (1 : α)

theorem localLength_eq :
    (xs.foldlM circuit init).localLength n = m * constant.localLength

lemma h_div32 {o : ℕ} (ho : o < 8) {x0 x1 x2 x3: ℕ} :
    (x0 + x1 * 256 + x2 * 256^2 + x3 * 256^3) / 2^o
    = x0 / 2^o + x1 * 2^(8-o) + x2 * 256 * 2^(8-o) + x3 * 256^2 * 2^(8-o)

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

theorem can_replace_completeness {env} {ops : Operations F} {n : ℕ} (h : ops.SubcircuitsConsistent n) : env.UsesLocalWitnesses n ops →
    ConstraintsHold.Completeness env ops → ConstraintsHold env ops

theorem toBits_fromBits {n : ℕ} (bits : Vector ℕ n)
  (h_bits : ∀ (i : ℕ) (hi : i < n), bits[i] = 0 ∨ bits[i] = 1) :
    toBits n (fromBits bits) = bits

theorem not_bytewise_value_spec {x : U64 (F p)} (x_lt : x.Normalized) :
    (not64_bytewise_value x).value = not64 x.value
    ∧ (not64_bytewise_value x).Normalized

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

lemma countAsFirst_add_last_eq_countAsSecond_add_head (xs : List S) (x : S) :
    countAsFirst xs x + (if xs.getLast? = some x then 1 else 0) =
    countAsSecond xs x + (if xs.head? = some x then 1 else 0)

theorem or_is_bool {α : Type*} [Ring α] {x y : α} (hx : IsBool x) (hy : IsBool y) :
    IsBool (x - x*y + y)

lemma single_le_sum_of_nonneg {α : Type*} [Fintype α] (f : α → ℤ) (a : α)
    (h_nonneg : ∀ x, f x ≥ 0) :
    f a ≤ ∑ x : α, f x

lemma getElem_eval_toLimbs {F} [Field F] {env : Environment F} {x : U64 (Expression F)} {i : ℕ} (hi : i < 8) :
    Expression.eval env x.toLimbs[i] = (eval env x).toLimbs[i]

lemma extract_from_offset_preserves_element {p n n1 n2 : ℕ} (input : fields n (F p))
    (i : ℕ) (hi : i < n2) (h_sum : n1 + n2 = n) :
    let input2 : fields n2 (F p) := ⟨input.toArray.extract n1 n, by simp [Array.size_extract, Vector.size_toArray]; omega⟩
    input2[i]'hi = input[n1 + i]'(by omega)

lemma last_not_in_zip_tail {α : Type*} [DecidableEq α] (l : List α) (x : α)
    (h_nodup : l.Nodup)
    (h_last : l.getLast? = some x) :
    ∀ y : α, (x, y) ∉ l.zip l.tail

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

@[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 forAll_flatten (xs : Vector α m) {circuit : α → Circuit F β} (constant : ConstantLength circuit) :
  Operations.forAll n prop (List.ofFn fun (i : Fin m) => (circuit xs[i.val]).operations (n + i * constant.localLength)).flatten
    ↔ ∀ (i : Fin m), (circuit xs[i.val]).forAll (n + i * constant.localLength) prop

theorem soundness : Soundness (F p) elaborated Assumptions Spec

@[circuit_norm ↓]
lemma forEach.output_eq :
  (forEach xs body constant).output n = ()

theorem mul_val_of_dvd {x c : F p} :
    c.val ∣ (c * x).val → (c * x).val = c.val * x.val

theorem soundness : Soundness (F p) elaborated Assumptions Spec

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

theorem not64_eq_sub {x : ℕ} (x_lt : x < 2^64) :
    not64 x = 2^64 - 1 - x

theorem completeness (offset : Fin 8) : Completeness (F p) (elaborated offset) Assumptions

lemma fieldToBits_fieldFromBits_aux {n : ℕ} (hn : 2^n < p) (bits : Vector (F p) n)
  (h_bits : ∀ (i : ℕ) (hi : i < n), bits[i] = 0 ∨ bits[i] = 1) :
    (fieldFromBits bits).val < 2^n ∧ fieldToBits n (fieldFromBits bits) = bits

@[circuit_norm ↓]
lemma map.soundness :
  ConstraintsHold.Soundness env (map xs body constant |>.operations n) ↔
    ∀ i : Fin m, ConstraintsHold.Soundness env (body xs[i.val] |>.operations (n + i*(body default).localLength))

@[circuit_norm ↓ high]
theorem eval_pair_left_vector_expr {n : ℕ} {β : TypeMap} [ProvableType β] (env : Environment F)
  (a : Vector (Expression F) n) (b : Var β F) :
    eval (α:=ProvablePair (fields n) β) env (a, b) = (eval env a, eval env b)

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem soundness : Soundness (F p) elaborated Assumptions Spec

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

theorem rotation32_bits_soundness {o : ℕ} (ho : o < 8) {x : U32 ℕ} :
    (rotRight32_u32 x o).valueNat = rotRight32 x.valueNat o

theorem ext_iff {f g : Circuit F α} :
  (f = g) ↔ (∀ n, (f.output n = g.output n) ∧ (f.operations n = g.operations n))

theorem getElem_mapRange {n} {create : ℕ → α} :
    ∀ (i : ℕ) (hi : i < n), (mapRange n create)[i] = create i

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

@[circuit_norm ↓]
lemma foldl.output_eq [NeZero m] :
  (foldl xs init body const_out constant).output n =
    (body default (xs[m-1]'(Nat.pred_lt (NeZero.ne m)))).output (n + (m-1)*(body default default).localLength)

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)

theorem rotRight32_lt (x r : ℕ) (h : x < 2^32) :
    rotRight32 x r < 2^32

theorem ext {x y : F p} (h : x.val = y.val) : x = y

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

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

lemma divides_256_two_power {offset : ℕ} (ho : offset < 8) {x i : ℕ} (h : i > 0):
    (2^offset) ∣ x * (256 ^ i)

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

lemma Environment.usesLocalWitnesses_iff_flat {n : ℕ} {ops : Operations F} {env : Environment F} :
    env.UsesLocalWitnesses n ops ↔
    env.UsesLocalWitnessesFlat n ops.toFlat

lemma initialState_normalized : (initialState (p:=p)).Normalized

theorem floorDiv256_bool [Fact (p > 512)] {x : F p} (h : x.val < 512) :
  floorDiv256 x = 0 ∨ floorDiv256 x = 1

omit [Fact (Nat.Prime p)] p_large_enough in
lemma block_len_normalized (buffer_len : F p) (h : buffer_len.val ≤ 64) :
    (U32.mk buffer_len 0 0 0 : U32 (F p)).Normalized
</all_available_lemmas>

<local_ctx>
import Clean.Gadgets.Addition8.Addition8FullCarry

import Clean.Types.U32

import Clean.Utils.Field

import Clean.Gadgets.Boolean

variable {p : ℕ} [Fact p.Prime]

variable [p_large_enough: Fact (p > 512)]

namespace Gadgets.Addition32.Theorems
</local_ctx>

<target_theorem>
theorem add32_soundness {x0 x1 x2 x3 y0 y1 y2 y3 carry_in c0 c1 c2 c3 z0 z1 z2 z3 : F p}
    (x0_byte : x0.val < 256) (x1_byte : x1.val < 256) (x2_byte : x2.val < 256) (x3_byte : x3.val < 256)
    (y0_byte : y0.val < 256) (y1_byte : y1.val < 256) (y2_byte : y2.val < 256) (y3_byte : y3.val < 256)
    (z0_byte : z0.val < 256) (z1_byte : z1.val < 256) (z2_byte : z2.val < 256) (z3_byte : z3.val < 256)
    (carry_in_bool : IsBool carry_in) (c0_bool : IsBool c0)
    (c1_bool : IsBool c1) (c2_bool : IsBool c2) (c3_bool : IsBool c3)
    (h0 : x0 + y0 + carry_in = c0 * 256 + z0)
    (h1 : x1 + y1 + c0 = c1 * 256 + z1)
    (h2 : x2 + y2 + c1 = c2 * 256 + z2)
    (h3 : x3 + y3 + c2 = c3 * 256 + z3) :
    ZMod.val z0 + ZMod.val z1 * 256 + ZMod.val z2 * 256 ^ 2 + ZMod.val z3 * 256 ^ 3 =
      (ZMod.val x0 + ZMod.val x1 * 256 + ZMod.val x2 * 256 ^ 2 + ZMod.val x3 * 256 ^ 3 +
            (ZMod.val y0 + ZMod.val y1 * 256 + ZMod.val y2 * 256 ^ 2 + ZMod.val y3 * 256 ^ 3) +
          ZMod.val carry_in) %
        2 ^ 32 ∧
    ZMod.val c3 =
      (ZMod.val x0 + ZMod.val x1 * 256 + ZMod.val x2 * 256 ^ 2 + ZMod.val x3 * 256 ^ 3 +
            (ZMod.val y0 + ZMod.val y1 * 256 + ZMod.val y2 * 256 ^ 2 + ZMod.val y3 * 256 ^ 3) +
          ZMod.val carry_in) /
        2 ^ 32 :=
</target_theorem>

