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>
InputAssumptions : ℕ → Input F → Prop := fun _ _ => True
  InitialStateAssumptions : State F → Prop := fun _ => True

def fromUInt32 (x : UInt32) : U32 (F p) :=
  decomposeNat x.toFin

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

def computeValueFromOffset (α : TypeMap) [ProvableType α] (offset : ℕ) (env : Environment F) : α F :=
  fromElements <| .mapRange _ fun i => env.get (offset + i)

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

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

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

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

example :
    let state := initialChunkState testCV 0
    let updated := updateChunk state testChunk65
    updated.blocks_compressed = 1 ∧ updated.block_buffer.length = 1 :=

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

instance : Fact (p > 2^16 + 2^8) := .mk (by admit /- proof elided -/
)

instance : ProvableStruct Inputs where
  components := [KeccakState, KeccakRow]
  toComponents := fun { state, d } => .cons state (.cons d .nil)
  fromComponents := fun (.cons state (.cons d .nil)) => { state, d }

def circuit : FormalCircuit (F p) (fields 254) field where
  main
  localLength input := (CompConstant.circuit ((p - 1) / 2)).localLength input

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

match casesResult.toList with
        | [subgoal] =>
          currentGoal := subgoal.mvarId
          decomposed := true
        | _ =>
          throwError s!"Unexpected result from cases on {userName}"
      catch e =>
        
        
        trace[Meta.Tactic] "Failed to decompose struct variable {userName}: {e.toMessageData}"
        continue

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

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

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

let isFirstBlock ← IsZero.circuit state.blocks_compressed

Fintype.card in Mathlib.Data.Fintype.Card

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

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

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

def rhoPiConstants := rhoPiIndices.zip rhoPiShifts

@[circuit_norm]
def eval (env : Environment F) (var : α (Expression F)) : α F :=
  toComponents var |> go (components α) |> fromComponents
where

Lean.Meta.inferType in Lean.Meta.Basic

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

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

localLength _ := n + 2

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

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

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

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

@[reducible] def field : TypeMap := id

Assumptions := fun { x, y, carryIn } =>
    x.val < 256 ∧ y.val < 256 ∧ IsBool carryIn

Id.run in Init.Control.Id

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

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

structure LookupCircuit (F : Type) [Field F] (α β : TypeMap) [ProvableType α] [ProvableType β]
    extends circuit : FormalCircuit F α β where
  name : String
  computableWitnesses : circuit.ComputableWitnesses

def initializeStateVector (input_var : Var Inputs (F p)) : Var BLAKE3State (F p) :=
  let { chaining_value, block_words, counter_high, counter_low, block_len, flags } := input_var
  #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],
    const (U32.fromUInt32 iv[0]), const (U32.fromUInt32 iv[1]),
    const (U32.fromUInt32 iv[2]), const (U32.fromUInt32 iv[3]),
    counter_low, counter_high, block_len, flags
  ]

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

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

def MemoryAccessList.Notimestampdup (accesses : MemoryAccessList) : Prop :=
  List.Pairwise timestamps_neq accesses

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

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

Lean.Meta.trySynthInstance in Lean.Meta.SynthInstance

localLength _ := 2
  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

def fibRelationBabybear := fibRelation (p:=p_babybear)

structure RawInstruction (F : Type) where
  rawInstrType : F
  op1 : F
  op2 : F
  op3 : F

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

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

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

let out1 ← main input1
    let out2 ← main input2

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

partial def circuitProofStartCore : TacticM Unit := do
  withMainContext do
    let goal ← getMainGoal
    let goalType ← goal.getType

Add in Init.Prelude

instance prime1009 : Fact (p1009.Prime) :=

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

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

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

def applyRounds (chaining_value : Vector ℕ 8) (block_words : Vector ℕ 16) (counter : ℕ) (block_len : ℕ) (flags : ℕ) : Vector ℕ 16 :=
  
  let counter_low := counter % 2^32
  let counter_high := counter / 2^32

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

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

HDiv in Init.Prelude

List.drop in Init.Data.List.Basic

Lean.FVarId in Lean.Expr

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

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

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

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 main (state : Var KeccakState (F p)) : Circuit (F p) (Var KeccakState (F p)) :=
  .map rhoPiConstants fun (i, s) =>
    Rotation64.circuit (-s) state[i.val]

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

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

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

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

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

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

@[reducible]
def psize (α : TypeMap) [NonEmptyProvableType α] : ℕ+ :=
  ⟨ size α, NonEmptyProvableType.nonempty⟩

def SevenRoundsSpec (input : Round.Inputs (F p)) (output : BLAKE3State (F p)) : Prop :=
  let final_state := applySevenRounds input.state.value (input.message.map U32.value)
  output.value = final_state ∧
  output.Normalized

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

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

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

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

UInt32.toNat in Init.Prelude

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

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

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

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 {α : TypeMap} [ProvableType α] : ExplicitCircuits (ProvableType.witness (α:=α) (F:=F)) where
  output _ n := varFromOffset α n
  localLength _ _ := size α
  operations c n := [.witness (size α) (toElements ∘ c)]

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

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

soundness : InductiveTable.Soundness F State Input Spec step

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

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

Finset in Mathlib.Data.Finset.Defs

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

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

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

def decodeInstructionCircuit : GeneralFormalCircuit (F p) field DecodedInstruction where
  main := fun instruction => do
    let bits ← Gadgets.ToBits.toBits 8 (by admit /- proof elided -/
    ) instruction
    return {
      instrType := {
        isAdd := (1 : Expression _) - bits[0] - bits[1] + bits[0] * bits[1],
        isMul := bits[0] - bits[0] * bits[1],
        isStoreState := bits[1] - bits[0] * bits[1],
        isLoadState := bits[0] * bits[1]
      },
      mode1 := {
        isDoubleAddressing := (1 : Expression _) - bits[2] - bits[3] + bits[2] * bits[3],
        isApRelative := bits[2] - bits[2] * bits[3],
        isFpRelative := bits[3] - bits[2] * bits[3],
        isImmediate := bits[2] * bits[3]
      },
      mode2 := {
        isDoubleAddressing := (1 : Expression _) - bits[4] - bits[5] + bits[4] * bits[5],
        isApRelative := bits[4] - bits[4] * bits[5],
        isFpRelative := bits[5] - bits[4] * bits[5],
        isImmediate := bits[4] * bits[5]
      },
      mode3 := {
        isDoubleAddressing := (1 : Expression _) - bits[6] - bits[7] + bits[6] * bits[7],
        isApRelative := bits[6] - bits[6] * bits[7],
        isFpRelative := bits[7] - bits[6] * bits[7],
        isImmediate := bits[6] * bits[7]
      }
    }
  localLength _ := 8

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

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

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

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

let state_c ← Addition32.circuit ⟨state[c], state_d⟩

def synthesizeValue : α F :=
  let zeros := Vector.fill (size α) 0
  fromElements zeros

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

List.replicate in Init.Data.List.Basic

DecidableEq in Init.Prelude

instance : ProvableStruct SimpleStruct where
  components := [field, field]
  toComponents := fun { a, b } => .cons a (.cons b .nil)
  fromComponents := fun (.cons a (.cons b .nil)) => { a, b }

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

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

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 fieldToBits (n : ℕ) (x : F p) : Vector (F p) n :=
  .map (↑) (toBits n x.val)

Nat.decLt in Init.Prelude

IsTrans in Mathlib.Order.Defs.Unbundled

Vector.extract in Init.Data.Vector.Basic

def rotRight64_eq_bv_rotate (x : ℕ) (h : x < 2^64) (offset : ℕ) :
    rotRight64 x offset = (x.toUInt64.toBitVec.rotateRight offset).toNat :=

instance : Fact (pBabybear > 2^16 + 2^8) :=

def circuit : FormalCircuit (F p) field (fields 254) where
  main
  localLength _ := 254 + 127 + 1 + 135 + 1 
  localLength_eq := by admit /- proof elided -/

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

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)

x === fieldFromBitsExpr bits
  return bits

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

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

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

HXor.hXor in Init.Prelude

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

Decidable in Init.Prelude

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

structure Variable (F : Type) where
  index : ℕ

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

Lean.Expr in Lean.Expr

Array.mapM in Init.Data.Array.Basic

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 8  
  s : Vector F 3

instance : ProvableStruct ProcessBlocksState where
  components := [ProvableVector U32 8, U32, U32]
  toComponents := fun { chaining_value, chunk_counter, blocks_compressed } =>
    .cons chaining_value (.cons chunk_counter (.cons blocks_compressed .nil))
  fromComponents := fun xss =>
    match xss with
    | .cons cv (.cons cc (.cons bc .nil)) =>
      { chaining_value := cv, chunk_counter := cc, blocks_compressed := bc }

def main (input : Var Inputs (F p)) : Circuit (F p) (Var U32 (F p))  := do
  let ⟨x, y⟩ := input
  let z ← witness fun env =>
    let z0 := (env x.x0).val ^^^ (env y.x0).val
    let z1 := (env x.x1).val ^^^ (env y.x1).val
    let z2 := (env x.x2).val ^^^ (env y.x2).val
    let z3 := (env x.x3).val ^^^ (env y.x3).val
    U32.mk z0 z1 z2 z3

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

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

let state_d ← Rotation32.circuit 8 <|
    ← Xor32.circuit ⟨state_d, state_a⟩

instance : IsIrrefl MemoryAccess address_strict_timestamp_ordering :=

def MemoryAccessList.isConsistentSingleAddress (accesses : MemoryAccessList) (h_sorted : accesses.isTimestampSorted) : Prop := match accesses with
  
  | [] => True
  
  | (_timestamp, _addr, readValue, _writeValue) :: [] => readValue = 0
  
  | (_t2, _addr2, readValue2, _writeValue2) :: (t1, addr1, readValue1, writeValue1) :: rest =>
    readValue2 = writeValue1 ∧
    MemoryAccessList.isConsistentSingleAddress ((t1, addr1, readValue1, writeValue1) :: rest) (List.Sorted.of_cons h_sorted)

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 z ← witness fun eval => mod256 (eval (x + y + carryIn))
  lookup ByteTable z

structure ProcessBlocksState (F : Type) where
  chaining_value : Vector (U32 F) 8    
  chunk_counter : U32 F                 
  blocks_compressed : U32 F

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

contains_iff := by admit /- proof elided -/

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

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

def every_row_two_rows_induction {P : Trace F S → Sort*}
    (zero : P (<+>))
    (one : ∀ row : Row F S, P (empty +> row))
    (more : ∀ curr next : Row F S,
      ∀ rest : Trace F S, P (rest) → P (rest +> curr) → P (rest +> curr +> next))
    : ∀ trace, P trace
  | <+> => zero
  | <+> +> first => one first
  | rest +> curr +> _ => more _ _ _
    (every_row_two_rows_induction zero one more (rest))
    (every_row_two_rows_induction zero one more (rest +> curr))

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

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

instance : Neg (Expression F) where
  neg e := mul (const (-1)) e

False.elim in Init.Prelude

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

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

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

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

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

let a10 := (ci[3] - ci[2] - ci[1] + ci[0]) * s10;
    let a1 := (ci[2] - ci[0]) * s[1];
    let a0 := (ci[1] - ci[0]) * s[0];
    let a := (ci[0]);

def main (n : ℕ) (x : Expression (F p)) := do
  
  let bits ← witnessVector n fun env => fieldToBits n (x.eval env)

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

def toString [Repr F] : Expression F → String
  | var v => reprStr v
  | const c => reprStr c
  | add x y => "(" ++ toString x ++ " + " ++ toString y ++ ")"
  | mul x y => "(" ++ toString x ++ " * " ++ toString y ++ ")"

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

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

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

Vector.finRange in Init.Data.Vector.FinRange

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

def main (input : Var Inputs (F p)) : Circuit (F p) (Var (ProvableVector U32 8) (F p)) := do

def circuit (c : ℕ) : FormalCircuit (F p) (fields 254) field where
  main := main c
  localLength _ := 127 + 1 + 135 + 1  
  localLength_eq := by admit /- proof elided -/

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

Vector in Init.Data.Vector.Basic

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

List.cons in Init.Prelude

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

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

def fib32Table : List (TableOperation RowType (F p)) := [
  .boundary (.fromStart 0) boundary,
  .everyRowExceptLast recursiveRelation,
]

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

instance elaborated [DecidableEq F] : ElaboratedCircuit F (Inputs M) M where
  main
  localLength _ := 0

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

@[table_assignment_norm, reducible]
def empty (W : ℕ+) : CellAssignment W S where
  offset := 0
  aux_length := 0
  vars := #v[]

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

def femtoCairoTable
    {programSize : ℕ} [NeZero programSize] (program : Fin programSize → (F p)) (h_programSize : programSize < p)
    {memorySize : ℕ} [NeZero memorySize] (memory : Fin memorySize → (F p)) (h_memorySize : memorySize < p)
    : InductiveTable (F p) State unit where
  step state _ := do
    femtoCairoStepCircuit program h_programSize memory h_memorySize state

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

Lean.MonadLCtx.getLCtx in Lean.LocalContext

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

Zero in Init.Prelude

HXor in Init.Prelude

@[reducible]
def fields (n : ℕ) := fun F => Vector F n

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

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

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

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

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

return { rawInstrType, op1, op2, op3 }

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

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

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

instance [CoeTail ℕ F] : CoeTail ℕ (field F) where
  coe n : F := n

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

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

ZMod.instField in Mathlib.Algebra.Field.ZMod

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

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

def testChunk65 : List ℕ := List.range 65

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

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

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

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

Prod.snd in Init.Prelude

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

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

def main (input : Vector (Expression (F p)) 254) :=
  
  CompConstant.circuit ((p - 1) / 2) input

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

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

let matching ← getMaxMatchingHyp declType

Mul in Init.Prelude

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

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

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

return isZero
</all_available_defs>

<all_available_lemmas>
Nat.add_sub_self_left in Init.Data.Nat.Basic

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

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

@[circuit_norm]
theorem FormalCircuit.toSubcircuit_usesLocalWitnesses
    {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).UsesLocalWitnesses env =
    (circuit.Assumptions (eval env input_var) → circuit.Spec (eval env input_var) (eval env (circuit.output input_var n)))

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

omit [Fact (Nat.Prime p)] p_large_enough in
lemma KeccakRow.normalized_value_ext (row : KeccakRow (F p)) (rhs : Vector ℕ 5) :
  (∀ i : Fin 5, row[i.val].Normalized ∧ row[i.val].value = rhs[i.val]) →
    row.Normalized ∧ row.value = rhs

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

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

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

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

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

omit [Fact (Nat.Prime p)] p_large_enough in
lemma vals_valueNat (x : U32 (F p)) : x.vals.valueNat = x.value

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

lemma rotRight32_testBit (x r i : ℕ) (h : x < 2^32) :
    (rotRight32 x r).testBit i =
    if i < 32 - r % 32 then
      x.testBit (r % 32 + i)
    else (decide (i < 32) && x.testBit (i - (32 - r % 32)))

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

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

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

lemma rotRight32_fin (x : ℕ) (offset : Fin 32) :
    rotRight32 x offset.val = x % (2^offset.val) * (2^(32-offset.val)) + x / (2^offset.val)

theorem forAll_iff_finRange {constant : ConstantLength (prod circuit)} :
  ((Vector.finRange m).foldlM circuit init).forAll n prop ↔
    ∀ i : Fin m, (circuit (foldlAcc n (Vector.finRange m) circuit init i) i)
    |>.forAll (n + i * (circuit init i).localLength) prop

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

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

lemma rhoPi_loop (state : Vector ℕ 25) :
    Specs.Keccak256.rhoPi state = rhoPiConstants.map fun (i, s) => rotLeft64 state[i.val] s

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)

lemma val_mul_floorDiv_self {x : F p} {c : ℕ+} (lt : c < p) : (c * (floorDiv x c)).val = c * (x.val / c)

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

theorem pure_output_eq (a : α) (n : ℕ) :
  (pure a : Circuit F α).output n = a

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

lemma leaf_has_incoming_and_negative_netFlow (R : Run S) (root leaf : S)
    (h_leaf : R.isLeaf root leaf)
    (h_root_out : ∃ y, R (root, y) > 0) :
    R.netFlow leaf < 0

theorem completeness : Completeness F elaborated Assumptions

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

@[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 acyclic_no_two_cycle (R : Run S) (a b : S)
    (h_acyclic : R.isAcyclic) (h_ne : a ≠ b)
    (h_edge1 : R (a, b) > 0) (h_edge2 : R (b, a) > 0) : False

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

theorem cast_heq {v : Vector α n} (h : n = m) : HEq (v.cast h) v

lemma rotRight32_bytes_u32_eq (o : ℕ) (x : U32 ℕ) :
  rotRight32_bytes x.toLimbs o = (rotRight32_u32 x o).toLimbs

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

lemma Vector.forM_toList (xs : Vector α n) {m : Type → Type} [Monad m] (body : α → m Unit) :
    xs.forM body = forM xs.toList body

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

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_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 fieldFromBits_succ (n : ℕ) (bits : Vector (F p) (n + 1)) :
    fieldFromBits bits = fieldFromBits bits.pop + bits[n] * (2^n : F p)

theorem completeness : Completeness (F p) elaborated Assumptions

theorem completeness : Completeness (F p) elaborated Assumptions

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

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

lemma foldl_to_sum {α : Type*} [AddCommMonoid α] : ∀ (n' : ℕ) (f' : Fin n' → α),
    Fin.foldl n' (fun acc i => acc + f' i) 0 = ∑ i : Fin n', f' i

@[circuit_norm]
theorem usesLocalWitnesses (α : TypeMap) [ProvableType α] (n : ℕ) (env : Environment F) (x y : Var α F) :
    ((circuit α).toSubcircuit n (x, y)).UsesLocalWitnesses env = True

lemma Vector.getElem_map_singleton_flatten {α β : Type} {n : ℕ} (v : Vector α n) (f : α → β) (i : ℕ) (hi : i < n) :
    (v.map (fun x => #v[f x])).flatten[i] = f (v[i])

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

theorem MemoryAccessList.addressTimestampSort_sorted (accesses : MemoryAccessList) :
    (MemoryAccessList.addressTimestampSort accesses).Sorted address_timestamp_ordering

theorem test_multiple_equalities {F : Type} [Field F] (input1 input2 : TestInputs F)
    (h1 : TestInputs.mk 1 2 3 = input1)
    (h2 : input2 = TestInputs.mk 4 5 6) :
    input1.x = 1 ∧ input2.y = 5

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem test_struct_in_function {F : Type} [Field F]
    (input : TestInputs F) (h : processStruct input = 10) :
    processStruct input = 10

@[circuit_norm ↓]
lemma forEach.localLength_eq :
    (forEach xs body constant).localLength n = m * (body default).localLength

theorem mul_nat_val_of_dvd {x : F p} (c : ℕ) (c_lt : c < p) {z : ℕ} :
    (c * x).val = c * z → (c * x).val = c * x.val

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

@[circuit_norm ↓ high]
theorem eval_pair_both_expr (env : Environment F)
  (a b : Expression F) :
    eval (α:=ProvablePair field field) env (a, b) = (Expression.eval env a, Expression.eval env b)

omit [Fact (p > 2)] in
lemma lc_eq {i0} {env} {n : ℕ} :
  (Expression.eval env <| Prod.fst <|
    Fin.foldl n (fun (lc1, e2) i => (lc1 + (var (F:=F p) ⟨ i0 + ↑i ⟩) * e2, e2 + e2)) (0, 1))
    = fieldFromBits (Vector.mapRange n fun i => env.get (i0 + i))

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

theorem completeness (off : Fin 4) : Completeness (F p) (elaborated off) Assumptions

theorem Circuit.subcircuitsConsistent_bind {α β : Type} (f : Circuit (F p) α) (g : α → Circuit (F p) β) (offset : ℕ)
    (hf : Operations.SubcircuitsConsistent offset (f.operations offset))
    (hg : Operations.SubcircuitsConsistent (offset + f.localLength offset)
          ((g (f.output offset)).operations (offset + f.localLength offset))) :
    Operations.SubcircuitsConsistent offset ((f >>= g).operations offset)

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

lemma foldl_isZero_eq_one_iff {n : ℕ} {vars : Vector (Expression F) n} {vals : Vector F n}
    {env : Environment F} {i₀ : ℕ}
    (h_eval : Vector.map (Expression.eval env) vars = vals)
    (h_isZero : ∀ (i : Fin n),
      IsZeroField.circuit.Assumptions (Expression.eval (F:=F) env vars[i]) →
        IsZeroField.circuit.Spec (Expression.eval (F:=F) env vars[i])
          (Expression.eval (F:=F) env
            (IsZeroField.circuit.output vars[i]
              (i₀ + i * IsZeroField.circuit.localLength vars[i])))) :
    Expression.eval env
      (Fin.foldl n
        (fun acc i => acc * (IsZeroField.circuit.output vars[i] (i₀ + i * IsZeroField.circuit.localLength vars[i]) : Var field F))
        1) =
    if ∀ (i : ℕ) (x : i < n), vals[i] = 0 then 1 else 0

@[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 divides_256_two_power {offset : ℕ} (ho : offset < 8) {x i : ℕ} (h : i > 0):
    (2^offset) ∣ x * (256 ^ i)

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

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

@[ext]
lemma ext {x y : U64 (F p)}
    (h0 : x.x0 = y.x0)
    (h1 : x.x1 = y.x1)
    (h2 : x.x2 = y.x2)
    (h3 : x.x3 = y.x3)
    (h4 : x.x4 = y.x4)
    (h5 : x.x5 = y.x5)
    (h6 : x.x6 = y.x6)
    (h7 : x.x7 = y.x7)
    : x = y

theorem floorDiv_lt {x : F p} {c : ℕ+} {d : ℕ} (h : x.val < c * d) : (floorDiv x c).val < d

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

theorem subcircuitsConsistent (n : ℕ) (input : Var (fields n) (F p)) (offset : ℕ) :
    Operations.SubcircuitsConsistent offset ((main input).operations offset)

theorem soundness (rc : UInt64) : Soundness (F p) (elaborated rc) Assumptions (Spec rc)

@[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 assignmentFromCircuit_vars (as : CellAssignment W S) (ops : Operations F) :
    (assignmentFromCircuit as ops).vars = (as.vars ++ (.mapRange ops.localLength fun i => .aux (as.aux_length + i) : Vector (Cell W S) _)
      ).cast (assignmentFromCircuit_offset ..).symm

theorem fromBits_toBits {n : ℕ} {x : ℕ} (hx : x < 2^n) :
    fromBits (toBits n x) = x

omit [Fact (Nat.Prime p)] p_large_enough in
lemma KeccakState.normalized_value_ext (state : KeccakState (F p)) (rhs : Vector ℕ 25) :
  (∀ i : Fin 25, state[i.val].Normalized ∧ state[i.val].value = rhs[i.val]) →
    state.Normalized ∧ state.value = rhs

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

omit [Fact (Nat.Prime p)] p_large_enough in
theorem value_lt_of_normalized {x : U32 (F p)} (hx : x.Normalized) : x.value < 2^32

theorem MemoryAccessList.addressTimestampSort_noTimestampDup
    (accesses : MemoryAccessList)
    (h_nodup : accesses.Notimestampdup) :
    accesses.addressTimestampSort.Notimestampdup

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

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

theorem mapM_push (as : Vector α n) {m : Type → Type} [Monad m] [LawfulMonad m] (f : α → m β) (a : α) :
    (as.push a).mapM f = (do
      let bs ← as.mapM f
      let b ← f a
      pure (bs.push b))

lemma fib_constraints (curr next : Row (F p) RowType) (aux_env : Environment (F p))
  : recursiveRelation.ConstraintsHoldOnWindow ⟨<+> +> curr +> next, rfl⟩ aux_env →
  curr.y = next.x ∧
  (curr.x.Normalized → curr.y.Normalized → next.y.value = (curr.x.value + curr.y.value) % 2^32 ∧ next.y.Normalized)

theorem soundness : Soundness (F p) elaborated Assumptions Spec

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

@[circuit_norm ↓]
lemma foldl.localLength_eq :
    (foldl xs init body const_out constant).localLength n = m * (body default default).localLength

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

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

theorem fieldFromBits_fieldToBits {n : ℕ} {x : F p} (hx : x.val < 2^n) :
    fieldFromBits (fieldToBits n x) = x

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

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

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

lemma fromByte_eq (x : F p) (x_lt : x.val < 256) : fromByte ⟨ x.val, x_lt ⟩ = x

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

omit [Fact (Nat.Prime p)] p_large_enough in
theorem value_xor_horner {x : U32 (F p)} (hx : x.Normalized) : x.value =
    x.x0.val ^^^ 2^8 * (x.x1.val ^^^ 2^8 * (x.x2.val ^^^ 2^8 * x.x3.val))

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

<local_ctx>
import Clean.Circuit.Basic

import Clean.Circuit.Provable

import Clean.Gadgets.Equality

import Clean.Utils.Field

import Clean.Utils.Primes

import Clean.Utils.Tactics

import Mathlib.Data.List.Sort

def MemoryAccess := ℕ × ℕ × ℕ × ℕ 

def MemoryAccessList := List MemoryAccess

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

def MemoryAccessList.isTimestampSorted (accesses : MemoryAccessList) : Prop :=
  accesses.Sorted timestamp_ordering

def MemoryAccessList.timestamps_neq (x y: MemoryAccess) : Prop :=
  match x, y with
  | (t_x, _a_x, _r_x, _w_x), (t_y, _a_y, _r_y, _w_y) => t_x ≠ t_y

def MemoryAccessList.Notimestampdup (accesses : MemoryAccessList) : Prop :=
  List.Pairwise timestamps_neq accesses

abbrev address_timestamp_ordering (x y : MemoryAccess) := match x, y with
| (t2, a2, _, _), (t1, a1, _, _) => if a1 = a2 then t1 ≤ t2 else a1 < a2

abbrev address_strict_timestamp_ordering (x y : MemoryAccess) := match x, y with
| (t2, a2, _, _), (t1, a1, _, _) => if a1 = a2 then t1 < t2 else a1 < a2

@[reducible]
def MemoryAccessList.isAddressTimestampSorted (accesses : MemoryAccessList) : Prop :=
  accesses.Sorted address_timestamp_ordering

@[reducible]
def MemoryAccessList.isAddressStrictTimestampSorted (accesses : MemoryAccessList) : Prop :=
  accesses.Sorted address_strict_timestamp_ordering
</local_ctx>

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

