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

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

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

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

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

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

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

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

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

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

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
def IsBool {α : Type*} [Zero α] [One α] (x : α) : Prop := x = 0 ∨ x = 1

def F p := ZMod p

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

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

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

instance [Field F] : Inhabited (α F) where
  default := synthesizeValue

SeqRight in Init.Prelude

example : MemoryAccessList.isConsistentOnline [] (by admit /- proof elided -/
) := by admit /- proof elided -/

@[table_assignment_norm]
def pushVarAux (assignment : CellAssignment W S) : CellAssignment W S where
  offset := assignment.offset + 1
  aux_length := assignment.aux_length + 1
  vars := assignment.vars.push (.aux assignment.aux_length)

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

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)

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

def TwoRoundsSpec (input : Round.Inputs (F p)) (output : Round.Inputs (F p)) : Prop :=
  let (final_state, final_message) := applyTwoRounds 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)

def everyRowTwoRowsInduction' {P : (t : Trace F S) → t.len ≥ 2 → Sort*}
    (base : ∀ first second, P (<+> +> first +> second) (show 2 ≤ 2 by admit /- proof elided -/
    ))
    (more : ∀ (row : Row F S) (rest : Trace F S) (h : rest.len ≥ 2),
      P rest h → P (rest +> row) (Nat.le_succ_of_le h))
    : ∀ (trace : Trace F S) (h : trace.len ≥ 2), P trace h
  
  
  | <+> => by admit /- proof elided -/
  | <+> +> first => by admit /- proof elided -/
  | <+> +> first +> second => fun _ => base first second
  | rest +> prev +> curr +> next => fun h =>
    have h_len : 2 ≤ rest.len + 2 := by admit /- proof elided -/

def two_row_induction {prop : Row F S → ℕ → Prop}
    (zero : ∀ first_row : Row F S, prop first_row 0)
    (succ : ∀ (N : ℕ) (curr next : Row F S), prop curr N → prop next (N + 1))
    : ∀ N (trace : TraceOfLength F S N), ForAllRowsOfTraceWithIndex trace prop :=

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

def Spec (input : Inputs (F p)) (z : U32 (F p)) :=
  let ⟨x, y⟩ := input
  z.value = (x.value + y.value) % 2^32 ∧ z.Normalized

structure Inputs (F : Type) where
  state : BLAKE3State F
  x : U32 F
  y : U32 F

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

Fin.castSucc in Init.Data.Fin.Basic

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

completeness := by admit /- proof elided -/

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

Composition.blocks in Mathlib.Combinatorics.Enumerative.Composition

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

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

-- 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 :=

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

instance : Repr (Variable F) where
  reprPrec v _ := "var ⟨" ++ repr v.index ++ "⟩"

def p1009 := 1009

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

def iv : Vector UInt32 8 := #v[
  0x6a09e667,
  0xbb67ae85,
  0x3c6ef372,
  0xa54ff53a,
  0x510e527f,
  0x9b05688c,
  0x1f83d9ab,
  0x5be0cd19
]

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

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

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

instance : ProvableStruct Inputs where
  components := [fields 4, fields 2]
  toComponents := fun {c, s} => .cons c (.cons s .nil)
  fromComponents := fun (.cons c (.cons s .nil)) => ⟨c, s⟩

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

def circuit : FormalCircuit (F p) Inputs Outputs where
  main
  Assumptions
  Spec
  localLength _ := 2
  output _ i0 := { z := var ⟨i0⟩, carryOut := var ⟨i0 + 1⟩ }

Preorder in Mathlib.Order.Defs.PartialOrder

def processBlocksWords (state : ChunkState) (blocks : List (Vector ℕ 16)) : ChunkState :=
  blocks.foldl processBlockWords state

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

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

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

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

ZMod.val in Mathlib.Data.ZMod.Basic

UInt32 in Init.Prelude

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

@[reducible]
def BinSumInput (n ops : ℕ) := ProvableVector (fields n) ops

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

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

Finset in Mathlib.Data.Finset.Defs

@[circuit_norm]
def componentsToElements {F : Type} : (cs : List WithProvableType) → ProvableTypeList F cs → Vector F (combinedSize' cs)
  | [], .nil => #v[]
  | _ :: cs, .cons a as => toElements a ++ componentsToElements cs as

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

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

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
  ]

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

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

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

let out ← Num2Bits.arbitraryBitLengthCircuit nout lin

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

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

soundness : InductiveTable.Soundness F State Input Spec step

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

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

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

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

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

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

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

def rotRight64_bytes (xs : Vector ℕ 8) (o : ℕ) : Vector ℕ 8 :=
  .ofFn fun ⟨ i, hi ⟩ => xs[i] / 2^o + (xs[(i + 1) % 8] % 2^o) * 2^(8-o)

Assumptions _ := True
  Spec (x : F p) := x.val < 2^n

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

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

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

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

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

class ProvableStruct (α : TypeMap) where
  components : List WithProvableType
  toComponents {F : Type} : α F → ProvableTypeList F components
  fromComponents {F : Type} : ProvableTypeList F components → α F

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

let out1 ← main input1
    let out2 ← main input2

Prod.fst in Init.Prelude

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

let mut currentGoal := goal
    let mut decomposed := false

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

instance (T : Type) [Repr T] : Repr (U32 T) where
  reprPrec x _ := "⟨" ++ repr x.x0 ++ ", " ++ repr x.x1 ++ ", " ++ repr x.x2 ++ ", " ++ repr x.x3 ++ "⟩"

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

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

cond in Init.Prelude

def proverEnvironment (circuit : LookupCircuit F α β) (input : α F) : Environment F :=
  circuit.main (const input) |>.proverEnvironment

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

@[table_norm]
def ForAllRowsOfTraceWithIndex {N : ℕ}
    (trace : TraceOfLength F S N) (prop : Row F S → ℕ → Prop) : Prop :=
  trace.val.ForAllRowsOfTraceWithIndex prop

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

def Spec (input : Inputs (F p)) (out : BLAKE3State (F p)) :=
  let { chaining_value, block_words, counter_high, counter_low, block_len, flags } := input
  out.value = applyRounds
    (chaining_value.map U32.value)
    (block_words.map U32.value)
    (counter_low.value + 2^32 * counter_high.value)
    block_len.value
    flags.value ∧
  out.Normalized

Or.inr in Init.Prelude

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

let startFlagU32 : Var U32 (F p) :=  ⟨isFirstBlock * (Expression.const (F:=F p) chunkStart), 0, 0, 0⟩

Lean.Name in Init.Prelude

def stateInitRound : Vector ℕ 16 := #v[1048429017, 869689525, 3373747814, 3881173978, 867318181, 93804160, 1095841330, 3806666906, 1528071400, 2951122214, 4271188711, 3509256835, 40453064, 3578515354, 1456976626, 243768026]

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

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

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

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

def splitTwoBytes (i : Fin (256 * 256)) : Fin 256 × Fin 256 :=
  let x := i.val / 256
  let y := i.val % 256
  have x_lt : x < 256 := by admit /- proof elided -/

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

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

def keyLen : ℕ := 32

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

let state_b ← Rotation32.circuit 12 <|
    ← Xor32.circuit ⟨state[b], state_c⟩

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

instance : HAdd (field (Expression F)) (field (Expression F)) (field (Expression F)) where
  hAdd (a : Expression F) (b : Expression F) := a + b

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)

def main (input : Vector (Expression (F p)) 254) := do
  
  AliasCheck.circuit input

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

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

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

Vector.replicate in Init.Data.Vector.Basic

instance primeBabybear : Fact (pBabybear.Prime) :=

soundness := by admit /- proof elided -/

partial def SpecializeAuto (e_term : Lean.Term): Lean.Elab.Tactic.TacticM Unit := do
  let (e, mvarIds') ← elabTermWithHoles e_term none `specialize_auto (allowNaturalHoles := true)

Unit in Init.Prelude

localLength _ := 5
  Assumptions
  | {state, mode, offset} =>
    ∀ addr ∈ Spec.dataMemoryAddresses memory offset state.ap state.fp,
      addr.val < memorySize
  Spec
  | {state, offset, mode}, output =>
    DecodedAddressingMode.isEncodedCorrectly mode →
    match Spec.dataMemoryAccess memory offset (DecodedAddressingMode.val mode) state.ap state.fp with
      | some value => output = value
      | none => False 
  soundness := by admit /- proof elided -/

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

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

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

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

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

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

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

Lean.Meta.trySynthInstance in Lean.Meta.SynthInstance

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

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

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

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

def femtoCairoStepCircuit
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p)
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p)) (h_memorySize : memorySize < p)
    : GeneralFormalCircuit (F p) State State := {
      femtoCairoStepElaboratedCircuit program h_programSize memory h_memorySize with
      Assumptions := femtoCairoAssumptions,
      Spec := femtoCairoCircuitSpec program memory,
      soundness := femtoCairoStepCircuitSoundness program h_programSize memory h_memorySize,
      completeness := femtoCairoStepCircuitCompleteness program h_programSize memory h_memorySize,
    }

instance : Repr (Cell W S) where
  reprPrec cell _ := match cell with
    | .input off => ".input " ++ reprStr off
    | .aux i => ".aux " ++ reprStr i

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 applyTwoRounds (state : Vector ℕ 16) (message : Vector ℕ 16) : Vector ℕ 16 × Vector ℕ 16 :=
  let state1 := round state message
  let msg1 := permute message
  let state2 := round state1 msg1
  let msg2 := permute msg1
  (state2, msg2)

def Spec (initialState : ProcessBlocksState (F p)) (inputs : List (BlockInput (F p))) i (_ : inputs.length = i) (state : ProcessBlocksState (F p)) :=
    inputs.length < 2^32 →
    initialState.Normalized ∧
    (∀ input ∈ inputs, input.Normalized) ∧
    
    
    let validBlocks := inputs |>.filter (·.block_exists = 1)
    let blockWords := validBlocks.map (fun b => b.block_data.map (·.value))
    let finalState := processBlocksWords initialState.toChunkState blockWords
    
    state.toChunkState.blocks_compressed < inputs.length ∧
    state.toChunkState = finalState ∧
    state.Normalized

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

contains_iff := by admit /- proof elided -/

imply_soundness := by admit /- proof elided -/

def applySixRounds (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
  let state5 := round state4 msg4
  let msg5 := permute msg4
  let state6 := round state5 msg5
  let msg6 := permute msg5
  (state6, msg6)

return out

def initRow : RowType (F p_babybear) := { x := 0, y := 1 }

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

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

Vector.mk in Init.Data.Vector.Basic

structure DecodedInstructionType (F : Type) where
  isAdd : F
  isMul : F
  isStoreState : F
  isLoadState : F

instance : Zero (Expression F) where
  zero := const 0

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 }

inferInstanceAs in Init.Prelude

let equalities ← extractEqualities type

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

List.head? in Init.Data.List.Basic

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

def main (state : Var BLAKE3State (F p)) : Circuit (F p) (Var BLAKE3State (F p)) := do
  return Vector.ofFn (fun i => state[msgPermutation[i]])

def ProvableType.witnessAny (α: TypeMap) [ProvableType α] : Circuit F (Var α F) := do
  let offset ← getOffset
  witness (computeValueFromOffset α offset)

let state_c ← Addition32.circuit ⟨state_c, state_d⟩

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

let state_b ← Rotation32.circuit 7 <|
    ← Xor32.circuit ⟨state_b, state_c⟩

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

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

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

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

let carryOut ← witness fun eval => floorDiv256 (eval (x + y + carryIn))
  assertBool carryOut

def rotRight32_eq_bv_rotate (x : ℕ) (h : x < 2^32) (offset : ℕ) :
    rotRight32 x offset = (x.toUInt32.toBitVec.rotateRight offset).toNat :=

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

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

structure NestedInputs (F : Type) where
  first : TestInputs F
  second : TestInputs F

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

@[circuit_norm]
def assertZero (e : Expression F) : Circuit F Unit := fun _ =>
  ((), [.assert e])

Prod.mk in Init.Prelude

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

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

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 ⟩

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

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

NoZeroDivisors in Mathlib.Algebra.GroupWithZero.Defs

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 decodeInstruction (instr : (F p)) : Option (ℕ × ℕ × ℕ × ℕ) :=
  if instr.val ≥ 256 then
    none
  else
  let bits := fieldToBits 8 instr
  let type := bits[0].val + 2 * bits[1].val
  let mode1 := bits[2].val + 2 * bits[3].val
  let mode2 := bits[4].val + 2 * bits[5].val
  let mode3 := bits[6].val + 2 * bits[7].val
  some (type, mode1, mode2, mode3)

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

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

Vector.push in Init.Data.Vector.Basic

CoeOut in Init.Coe

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

let headConst? := goalType.getAppFn.constName?
    let isSoundness := headConst? == some ``Soundness ||
                       headConst? == some ``FormalAssertion.Soundness ||
                       headConst? == some ``GeneralFormalCircuit.Soundness
    let isCompleteness := headConst? == some ``Completeness ||
                          headConst? == some ``FormalAssertion.Completeness ||
                          headConst? == some ``GeneralFormalCircuit.Completeness

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

instance : ToJson (FlatOperation F) where
  toJson
    | FlatOperation.witness m _ => Json.mkObj [("witness", toJson m)]
    | FlatOperation.assert e => Json.mkObj [("assert", toJson e)]
    | FlatOperation.lookup l => Json.mkObj [("lookup", toJson l)]

def MemoryAccessList.filterAddress (accesses : MemoryAccessList) (addr : ℕ) : MemoryAccessList :=
  accesses.filter (fun (_timestamp, addr', _readValue, _writeValue) => addr' = addr)

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

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

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

instance : IsIrrefl MemoryAccess address_strict_timestamp_ordering :=

@[table_norm]
def ForAllRowsOfTrace {N : ℕ}
    (trace : TraceOfLength F S N) (prop : Row F S → Prop) : Prop :=
  inner trace.val prop
  where

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

IsAntisymm in Mathlib.Order.Defs.Unbundled

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

instance : HMul (field (Expression F)) (field (Expression F)) (field (Expression F)) where
  hMul (a : Expression F) (b : Expression F) := a * b

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

def Assumptions (input : Inputs (F p)) :=
  let { state, x, y } := input
  state.Normalized ∧ x.Normalized ∧ y.Normalized

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)

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

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

go e []

@[circuit_norm]
def varFromOffset (α : TypeMap) [ProvableStruct α] (offset : ℕ) : Var α F :=
  go (components α) offset |> fromComponents (F:=Expression F)
where

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

Vector.cast in Init.Data.Vector.Basic

structure MemoryReadInput (F : Type) where
  state : State F
  offset : F
  mode : DecodedAddressingMode F

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

repr in Init.Data.Repr

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

instance [Repr F] : Repr (TableConstraint W S F α) where
  reprPrec table _ := reprStr (table .empty).2

structure Inputs (F : Type) where
  state : ProcessBlocksState F          
  buffer_len : F                        
  buffer_data : Vector F 64             
  base_flags : U32 F

instance : Neg (Expression F) where
  neg e := mul (const (-1)) e
</all_available_defs>

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

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

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

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

lemma val_eq_256 [p_large_enough: Fact (p > 512)] : (256 : F p).val = 256

theorem byte_sum_do_not_wrap (x y : F p) [Fact (p > 512)]:
    x.val < 256 -> y.val < 256 -> (x + y).val = x.val + y.val

theorem byte_sum_le_bound (x y : F p) [Fact (p > 512)]:
    x.val < 256 -> y.val < 256 -> (x + y).val < 511

theorem byte_sum_and_bit_do_not_wrap (x y b : F p) [Fact (p > 512)]:
    x.val < 256 -> y.val < 256 -> b.val < 2 -> (b + x + y).val = b.val + x.val + y.val

theorem byte_sum_and_bit_do_not_wrap' (x y b : F p) [Fact (p > 512)]:
    x.val < 256 -> y.val < 256 -> b.val < 2 -> (x + y + b).val = x.val + y.val + b.val

theorem byte_sum_and_bit_lt_512 (x y b : F p) [Fact (p > 512)]:
    x.val < 256 -> y.val < 256 -> b.val < 2 -> (x + y + b).val < 512

theorem byte_plus_256_do_not_wrap (x : F p) [Fact (p > 512)]:
    x.val < 256 -> (x + 256).val = x.val + 256

lemma sum_nat_cast_zero_of_not_pos {α : Type*} [Fintype α] (f : α → ℕ)
    (h : ∀ x, ¬(f x > 0)) :
    ∑ x : α, (f x : ℤ) = 0

lemma constraintsHold_cons : ∀ {op : FlatOperation F}, ∀ {ops : List (FlatOperation F)}, ∀ {env : Environment F},
    ConstraintsHoldFlat env (op :: ops) ↔ ConstraintsHoldFlat env [op] ∧ ConstraintsHoldFlat env ops

lemma not_mem_implies_transition_not_in_zip_tail {α : Type*} (path : List α) (x y : α)
    (h_y_not_in : y ∉ path) :
    (x, y) ∉ path.zip path.tail

theorem completeness : Completeness (F p) elaborated Assumptions

theorem natToField_eq_natCast {n : ℕ} (lt : n < p) : ↑n = FieldUtils.natToField n lt

lemma drop_of_lt_length_nonempty {α : Type*} (path : List α) (i : ℕ)
    (h_i_lt : i < path.length) :
    path.drop i ≠ []

lemma sum_zero_of_all_zero {α : Type*} [Fintype α] (f : α → ℕ) (h : ∀ x, f x = 0) :
    ∑ x : α, (f x : ℤ) = 0

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

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

omit [Fact (Nat.Prime p)] p_large_enough in
lemma or_componentwise {x y : U32 (F p)} (x_norm : x.Normalized) (y_norm : y.Normalized) :
    x.value ||

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

lemma soundness_zero {p : ℕ} [Fact p.Prime]
    (offset : ℕ) (env : Environment (F p)) (input_var : Var (fields 0) (F p))
    (input : fields 0 (F p)) (_h_env : input = eval env input_var)
    (_h_assumptions : Assumptions 0 input)
    (_h_hold : Circuit.ConstraintsHold.Soundness env ((main input_var).operations offset)) :
    Spec 0 input (env ((main input_var).output offset))

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

theorem test_multiple_no_projection {F : Type} [Field F]
    (a : TestInputs F) (b : TestInputs F) (c : TestInputs F)
    (ha : a = ⟨1, 2, 3⟩) (hb : b = ⟨4, 5, 6⟩) (hc : c = ⟨7, 8, 9⟩) :
    a = ⟨1, 2, 3⟩ ∧ b = ⟨4, 5, 6⟩ ∧ c = ⟨7, 8, 9⟩

lemma rotRight64_testBit_of_ge (x r i : ℕ) (h : x < 2^64) (hi : i ≥ 64 - r % 64) :
    (rotRight64 x r).testBit i = (decide (i < 64) && x.testBit (i - (64 - r % 64)))

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 MemoryAccessList.eq_of_perm_of_sorted {l1 l2 l3 : MemoryAccessList} (h_l1_sorted: l1.isTimestampSorted)
    (h_l2_sorted : l2.isAddressTimestampSorted) (h_l3_sorted : l3.isAddressTimestampSorted)
    (h_perm1 : l1.Perm l2) (h_perm2 : l1.Perm l3) : l2 = l3

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 fieldFromBits_fieldToBits {n : ℕ} {x : F p} (hx : x.val < 2^n) :
    fieldFromBits (fieldToBits n x) = x

@[ext]
lemma ext {x y : U32 (F p)}
    (h0 : x.x0 = y.x0)
    (h1 : x.x1 = y.x1)
    (h2 : x.x2 = y.x2)
    (h3 : x.x3 = y.x3)
    : x = y

theorem fieldToBits_bits {n : ℕ} {x : F p} :
    ∀ i (_ : i < n), (fieldToBits n x)[i] = 0 ∨ (fieldToBits n x)[i] = 1

lemma netFlow_sub (R R' : Run S) (x : S)
    (h_valid : ∀ t, R' t ≤ R t) :
    Run.netFlow (fun t => R t - R' t) x = R.netFlow x - R'.netFlow x

theorem completeness : Completeness F (elaborated (M := M)) Assumptions

omit [Field F] in
@[circuit_norm ↓ high]
theorem varFromOffset_pair {α β: TypeMap} [ProvableType α] [ProvableType β] (offset : ℕ) :
    varFromOffset (F:=F) (ProvablePair α β) offset
    = (varFromOffset α offset, varFromOffset β (offset + size α))

lemma drop_take_cycle_same_endpoints (path : List S) (x : S) (n m : Fin path.length)
    (h_n_lt_m : n < m)
    (h_x_at_n : path[n] = x)
    (h_x_at_m : path[m] = x) :
    ((path.drop n.val).take (m.val - n.val + 1)).head? =
    ((path.drop n.val).take (m.val - n.val + 1)).getLast?

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

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

Nat.min_add_right_self in Init.Data.Nat.Lemmas

theorem soundness {p : ℕ} [Fact p.Prime] (n : ℕ) :
    ∀ (offset : ℕ) (env : Environment (F p)) (input_var : Var (fields n) (F p))
      (input : fields n (F p)),
    input = eval env input_var →
    Assumptions n input →
    Circuit.ConstraintsHold.Soundness env ((main input_var).operations offset) →
    Spec n input (env ((main input_var).output offset))

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

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

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

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

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

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'

theorem bind_localLength_eq (f : Circuit F α) (g : α → Circuit F β) (n : ℕ) :
    (f >>= g).localLength n = f.localLength n + (g (f.output n)).localLength (n + f.localLength n)

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

theorem completeness [DecidableEq F] : Completeness F (elaborated (F:=F) (M:=M)) Assumptions

theorem test_decompose_from_hypothesis {F : Type} [Field F] (input : TestInputs F)
    (h : input.x = 5) : input.y + input.z = input.z + input.y

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

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

lemma completeness_zero {p : ℕ} [Fact p.Prime]
    (offset : ℕ) (env : Environment (F p)) (input_var : Var (fields 0) (F p))
    (input : fields 0 (F p))
    (_h_local_witnesses : env.UsesLocalWitnessesCompleteness offset ((main input_var).operations offset))
    (_h_env : input = eval env input_var)
    (_h_assumptions : Assumptions 0 input) :
    Circuit.ConstraintsHold.Completeness env ((main input_var).operations offset)

theorem getElem_eval_toElements {F : Type} [Field F] {α : TypeMap} [ProvableType α]
  {env : Environment F} (x : α (Expression F)) (i : ℕ) (hi : i < size α) :
    Expression.eval env (toElements x)[i] = (toElements (eval env x))[i]

lemma table_soundness_aux (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 →
    trace.ForAllRowsWithPrevious (fun row i rest => table.Spec input (traceInputs rest) i (traceInputs_length rest) row.1)
    ∧ trace.lastRow.1 = output

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

@[circuit_norm]
theorem forAll_cons {condition : Condition F} {offset : ℕ} {op : Operation F} {ops : Operations F} :
  forAll offset condition (op :: ops) ↔
    condition.apply offset op ∧ forAll (op.localLength + offset) condition ops

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

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

theorem completeness : Completeness (F p) elaborated Assumptions

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

omit p_large_enough in
lemma boundary_step (first_row : Row (F p) RowType) (aux_env : Environment (F p)) :
  Circuit.ConstraintsHold.Soundness (boundaryFib.windowEnv ⟨<+> +> first_row, rfl⟩ aux_env) boundaryFib.operations
    → ZMod.val first_row.x = fib8 0 ∧ ZMod.val first_row.y = fib8 1

theorem forAll_cons {condition : Condition F} {offset : ℕ} {op : FlatOperation F} {ops : List (FlatOperation F)} :
  forAll offset condition (op :: ops) ↔
    condition.applyFlat offset op ∧ forAll (op.singleLocalLength + offset) condition ops

lemma rotRight32_testBit_of_lt (x r i : ℕ) (h : x < 2^32) (hi : i < 32 - r % 32) :
    (rotRight32 x r).testBit i = x.testBit (r % 32 + i)

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

lemma applyRounds_eq_applySevenRounds
    (chaining_value : Vector ℕ 8)
    (block_words : Vector ℕ 16)
    (counter : ℕ)
    (block_len : ℕ)
    (flags : ℕ) :
    applyRounds chaining_value block_words counter block_len flags =
    applySevenRounds
      (#v[
        chaining_value[0], chaining_value[1], chaining_value[2], chaining_value[3],
        chaining_value[4], chaining_value[5], chaining_value[6], chaining_value[7],
        iv[0].toNat, iv[1].toNat, iv[2].toNat, iv[3].toNat,
        counter % 2^32, counter / 2^32, block_len, flags
      ])
      block_words

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

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

theorem fromLimbs_toLimbs {F} (x : U64 F) :
    U64.fromLimbs x.toLimbs = x

lemma shifted_decomposition_eq'' {offset : ℕ} (ho : offset < 8) {x1 x2 i : ℕ} (hi : i > 0) :
    (x1 / 2 ^ offset + x2 % 2 ^ offset * 2 ^ (8-offset)) * 256^i =
    (2^offset * (x1 / 2^offset) * 2^(8-offset) * 256^(i-1) +
    (x2 % 2^offset) * 2^(8-offset) * 256^i)

theorem forAll_iff :
  (xs.mapM circuit).forAll n prop ↔
    ∀ (i : Fin m), (circuit xs[i.val]).forAll (n + i * constant.localLength) prop

lemma drop_take_length_ge_two {α : Type*} (path : List α) (n m : Fin path.length)
    (h_n_lt_m : n < m) :
    ((path.drop n.val).take (m.val - n.val + 1)).length ≥ 2

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

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

theorem MemoryAccessList.isConsistentSingleAddress_filterAddress_of_cons (head : MemoryAccess) (tail : MemoryAccessList)
    (addr : ℕ)
    (h_sorted : isTimestampSorted (head :: tail))
    (h : isConsistentSingleAddress (filterAddress (head :: tail) addr)
         (filterAddress_sorted (head :: tail) h_sorted addr)) :
    isConsistentSingleAddress (filterAddress tail addr)
      (filterAddress_sorted tail (isTimestampSorted_cons head tail h_sorted) addr)

theorem soundness : Soundness (F p) elaborated Assumptions Spec

lemma getLast_drop_take {α : Type*} (path : List α) (n k : ℕ)
    (h_n_lt : n < path.length)
    (h_bound : n + k ≤ path.length)
    (h_k_pos : k > 0) :
    ((path.drop n).take k).getLast? = path[n + k - 1]?

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

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

theorem getElem_eval_toVars {F : Type} [Field F] {α : TypeMap} [ProvableType α]
  {env : Environment F} (x : Var α F) (i : ℕ) (hi : i < size α) :
    Expression.eval env (toVars x)[i] = (toElements (eval env x))[i]

theorem test_equality_not_triggar {F : Type} [Field F]
    (a : TestInputs F) (_ : a = {x := 1, y := 2, z := 4}) :
    a = a

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

lemma toLimbs_map {α β : Type} (x : U32 α) (f : α → β) :
  toLimbs (map x f) = (toLimbs x).map f

theorem cons_push (x y : α) (xs : Vector α n) : (cons x xs).push y = cons x (xs.push y)

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

lemma mem_of_mem_zip_fst {α β : Type*} (l1 : List α) (l2 : List β) (a : α) (b : β) :
    (a, b) ∈ l1.zip l2 → a ∈ l1

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

lemma finFoldl_cons_succ (x : α) :
  Fin.foldl (m + 1) (fun acc i => (circuit acc (Vector.cons x xs)[i.val]).output (n + i * constant.localLength)) init
    = Fin.foldl m (fun acc i => (circuit acc xs[i.val]).output (n + constant.localLength + i * constant.localLength)) ((circuit init x).output n)

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

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

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

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

@[circuit_norm ↓]
lemma map.output_eq :
  (map xs body constant).output n =
    xs.mapIdx fun i x => (body x).output (n + i*(body default).localLength)

lemma sum_interchange {α : Type*} [CommSemiring α] {n ops : ℕ} (f : Fin ops → Fin n → α) (g : ℕ → α) :
    Fin.foldl n (fun acc k => acc + g k.val *
      Fin.foldl ops (fun acc' j => acc' + f j k) 0) 0 =
    Fin.foldl ops (fun acc j => acc +
      Fin.foldl n (fun acc' k => acc' + f j k * g k.val) 0) 0

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

@[circuit_norm ↓ high]
theorem eval_eq_eval {α : TypeMap} [ProvableStruct α] : ∀ (env : Environment F) (x : Var α F),
    ProvableType.eval env x = ProvableStruct.eval env x

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

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

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 soundness : Soundness (F p) elaborated Assumptions Spec
</all_available_lemmas>

<local_ctx>
import Clean.Utils.Field

import Clean.Gadgets.Boolean

namespace Gadgets.Addition8.Theorems

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

variable [p_large_enough: Fact (p > 512)]
</local_ctx>

<target_theorem>
theorem soundness (x y out carry_in carry_out : F p):
    x.val < 256 -> y.val < 256 ->
    out.val < 256 ->
    IsBool carry_in ->
    IsBool carry_out ->
    (x + y + carry_in + -out + -(carry_out * 256) = 0) ->
    (out.val = (x.val + y.val + carry_in.val) % 256
    ∧ carry_out.val = (x.val + y.val + carry_in.val) / 256) :=
</target_theorem>

