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 rotRight64 (x : ℕ) (offset : ℕ) : ℕ :=
  let offset := offset % 64
  let low := x % (2^offset)
  let high := x / (2^offset)
  low * (2^(64-offset)) + high

structure U64 (T : Type) where
  x0 : T
  x1 : T
  x2 : T
  x3 : T
  x4 : T
  x5 : T
  x6 : T
  x7 : T
deriving DecidableEq

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

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

@[circuit_norm]
def FormalAssertion.Completeness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input unit)
    (Assumptions : Input F → Prop) (Spec : 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 → Spec input →
  
  ConstraintsHold.Completeness env (circuit.main input_var |>.operations offset)

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

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

One in Init.Prelude

return out

go e []

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

soundness : InductiveTable.Soundness F State Input Spec step

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

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

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

let block_words := bytesToWords input.buffer_data

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

let z ← witness fun eval => mod256 (eval (x + y + carryIn))
  lookup ByteTable z

List.insertionSort in Mathlib.Data.List.Sort

(a210 + a21 + a20 + a2) * s[2] + (a10 + a1 + a0 + a);

@[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 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 circuit : FormalCircuit (F p) fieldPair field where
  main
  localLength _ := 1
  localLength_eq := by admit /- proof elided -/

Zero.toOfNat0 in Init.Data.Zero

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

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

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

Lean.Elab.Tactic.evalTactic in Lean.Elab.Tactic.Basic

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

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

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

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

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

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

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

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

imply_soundness := by admit /- proof elided -/

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

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

Repr in Init.Data.Repr

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

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

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

HAnd in Init.Prelude

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

CommSemiring in Mathlib.Algebra.Ring.Defs

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

Assumptions := fun (x, y) => x.val < 2^n ∧ y.val < 2^n

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

HMul in Init.Prelude

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

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

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

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

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

def twoRoundsApplyStyle : FormalCircuit (F p) Round.Inputs Round.Inputs :=
  twoRoundsWithPermute.weakenSpec TwoRoundsSpec (by admit /- proof elided -/
  )

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

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

List.range in Init.Data.List.Basic

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 }

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

List.map in Init.Prelude

def toLimbs {F} (x : U64 F) : Vector F 8 := toElements x

List.zip in Init.Data.List.Basic

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

let state := #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_low, counter_high, block_len, flags
  ]

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

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

CharP in Mathlib.Algebra.CharP.Defs

def fib32json := Lean.toJson ((Tables.Fibonacci32Inductive.table (p:=pBabybear)).tableConstraints
  { x := U32.fromByte 0, y := U32.fromByte 1 }
  { x := U32.fromByte 0, y := U32.fromByte 0 })

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 s10 <== s[1] * s[0]

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

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

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

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

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

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

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

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

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

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

return U32.fromLimbs rotated

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

def fieldToBits (n : ℕ) (x : F p) : Vector (F p) n :=
  .map (↑) (toBits n x.val)

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

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
  ]

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

def decomposeNatExpr (x : ℕ) : U64 (Expression (F p)) :=
  let (⟨x0, x1, x2, x3, x4, x5, x6, x7⟩ : U64 (F p)) := decomposeNat x
  ⟨ x0, x1, x2, x3 , x4, x5, x6, x7 ⟩

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

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

UInt16.toNat in Init.Data.UInt.BasicAux

Nat.Prime in Mathlib.Data.Nat.Prime.Defs

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

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

localLength : Var Input F → ℕ

Ring in Mathlib.Algebra.Ring.Defs

List.drop in Init.Data.List.Basic

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

SeqLeft.seqLeft in Init.Prelude

let state_c ← Addition32.circuit ⟨state_c, state_d⟩

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

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

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

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

def DecodedInstructionType.val : DecodedInstructionType (F p) → ℕ := fun instrType =>
  if instrType.isAdd = 1 then 0
  else if instrType.isMul = 1 then 1
  else if instrType.isStoreState = 1 then 2
  else 3

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)

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

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

soundness := by admit /- proof elided -/

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

def exprToJson [ToJson F]: Expression F → Json
  | .var v => Json.mkObj [
    ("type", Json.str "var"),
    ("index", Json.num v.index)
  ]
  | .const c => Json.mkObj [
    ("type", Json.str "const"),
    ("value", toJson c)
  ]
  | .add x y => Json.mkObj [
    ("type", Json.str "add"),
    ("lhs", exprToJson x),
    ("rhs", exprToJson y)
  ]
  | .mul x y => Json.mkObj [
    ("type", Json.str "mul"),
    ("lhs", exprToJson x),
    ("rhs", exprToJson y)
  ]

HAdd in Init.Prelude

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

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

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

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

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

instance (p : ℕ) : ToJson (F p) where
  toJson x := toJson x.val

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

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

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

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

@[circuit_norm]
def Environment.UsesLocalWitnessesCompleteness (env : Environment F) (offset : ℕ) : List (Operation F) → Prop
  | [] => True
  | .witness m c :: ops => env.ExtendsVector (c env) offset ∧ env.UsesLocalWitnessesCompleteness (offset + m) ops
  | .assert _ :: ops => env.UsesLocalWitnessesCompleteness offset ops
  | .lookup _ :: ops => env.UsesLocalWitnessesCompleteness offset ops
  | .subcircuit s :: ops => s.UsesLocalWitnesses env ∧ env.UsesLocalWitnessesCompleteness (offset + s.localLength) ops

Fin in Init.Prelude

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 valueU32 (x : U32 (F p)) (h : x.Normalized) : UInt32 :=
  UInt32.ofNatLT x.value (value_lt_of_normalized h)

@[circuit_norm]
def toVars (var : M (Expression F)) := toElements var

Nat.twoStepInduction in Mathlib.Data.Nat.Init

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

def copyToVar (x : Expression F) : Circuit F (Variable F) := do
  let x' ← witnessVar x.eval
  assertZero (x - (var x'))
  return x'

contains_iff := by admit /- proof elided -/

@[reducible]
def unit (_ : Type) := Unit

def keyLen : ℕ := 32

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

@[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 Spec (state : KeccakState (F p)) (out_state : KeccakState (F p)) : Prop :=
  out_state.Normalized
  ∧ out_state.value = Specs.Keccak256.theta state.value

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

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

def circuit (a b c d : Fin 16) : FormalCircuit (F p) Inputs BLAKE3State := {
  elaborated a b c d with
  Assumptions
  Spec := Spec a b c d
  soundness := soundness a b c d
  completeness := completeness a b c d
}

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 circuit : FormalCircuit (F p) Inputs U32 where
  Assumptions
  Spec
  soundness
  completeness

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 ⟩

structure RawTable (F : Type) where
  name : String
  arity : ℕ
  Contains : Vector F arity → Prop
  Soundness : Vector F arity → Prop
  Completeness : Vector F arity → Prop
  imply_soundness : ∀ row, Contains row → Soundness row
  implied_by_completeness : ∀ row, Completeness row → Contains row

structure Inputs (F : Type) where
  state : BLAKE3State F
  message : Vector (U32 F) 16

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

HXor.hXor in Init.Prelude

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

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

Vector.instGetElemNatLt in Init.Data.Vector.Basic

def toBits (n : ℕ) (hn : 2^n < p) : GeneralFormalCircuit (F p) field (fields n) where
  main := main n
  localLength _ := n
  output _ i := varFromOffset (fields n) i

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

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

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

instance : IsIrrefl MemoryAccess address_strict_timestamp_ordering :=

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

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

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

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

ZMod.instField in Mathlib.Algebra.Field.ZMod

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

def testCircuit : ElaboratedCircuit (F p) unit unit :=
  { main := fun _ => pure (), output := fun _ _ => (), localLength := 0, output_eq := by simp }

Fin.foldl in Init.Data.Fin.Fold

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

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

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

def Condition.implies (c c': Condition F) : Condition F where
  witness n m compute := c.witness n m compute → c'.witness n m compute
  assert offset e := c.assert offset e → c'.assert offset e
  lookup offset l := c.lookup offset l → c'.lookup offset l
  subcircuit offset _ s := c.subcircuit offset s → c'.subcircuit offset s

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

def Spec (offset : Fin 8) (x : F p) (out : Outputs (F p)) :=
  let ⟨low, high⟩ := out
  (low.val = x.val % (2^offset.val) ∧ high.val = x.val / (2^offset.val))
  ∧ (low.val < 2^offset.val ∧ high.val < 2^(8-offset.val))

repr in Init.Data.Repr

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

UInt64.ofNat in Init.Data.UInt.BasicAux

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

instance : ProvableType fieldTriple where
  size := 3
  toElements := fun (x, y, z) => #v[x, y, z]
  fromElements := fun ⟨⟨[x, y, z]⟩, _ ⟩ => (x, y, z)

let out1 ← main input1
    let out2 ← main input2

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

Eq in Init.Prelude

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

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

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

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

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

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

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

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

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

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

Vector.mk in Init.Data.Vector.Basic

instance elaborated : ElaboratedCircuit (F p) KeccakState KeccakState where
  main
  localLength _ := 30912
  output _ i0 := stateVar i0 23

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

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)

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

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

let hasProvableStructInstance (fvarId : Lean.FVarId) : Lean.MetaM Bool := do
      let type ← inferType (.fvar fvarId)
      let type' ← withTransparency .reducible (whnf type)
      
      
      match type' with
      | .app typeCtor _ =>
        
        
        try
          let instType ← mkAppM ``ProvableStruct #[typeCtor]
          if let .some _ ← trySynthInstance instType then
            return true
          else
            return false
        catch _ => return false
      | _ => return false

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

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

Lean.getStructureInfo? in Lean.Structure

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

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

Array in Init.Prelude

if offset = 0 then
    return ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩
  else if offset = 1 then
    return ⟨ x1, x2, x3, x4, x5, x6, x7, x0 ⟩
  else if offset = 2 then
    return ⟨ x2, x3, x4, x5, x6, x7, x0, x1 ⟩
  else if offset = 3 then
    return ⟨ x3, x4, x5, x6, x7, x0, x1, x2 ⟩
  else if offset = 4 then
    return ⟨ x4, x5, x6, x7, x0, x1, x2, x3 ⟩
  else if offset = 5 then
    return ⟨ x5, x6, x7, x0, x1, x2, x3, x4 ⟩
  else if offset = 6 then
    return ⟨ x6, x7, x0, x1, x2, x3, x4, x5 ⟩
  else
    return ⟨ x7, x0, x1, x2, x3, x4, x5, x6 ⟩

let muxedCV ← Conditional.circuit (M := ProvableVector U32 8) {
    selector := input.block_exists
    ifTrue := newCV16.takeShort 8 (by admit /- proof elided -/
    )
    ifFalse := state.chaining_value
  }

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

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

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

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

IO in Init.System.IO

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

MonadLift in Init.Prelude

soundness : InductiveTable.Soundness F State Input Spec step

Finset.erase in Mathlib.Data.Finset.Erase

soundness := by admit /- proof elided -/

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

List.take in Init.Data.List.Basic

Vector.ofFn in Init.Data.Vector.Basic
</all_available_defs>

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

lemma Nat.pow_minus_one_mul {x y : ℕ} (hy : y > 0) : x ^ y = x * x ^ (y - 1)

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

lemma div_256_two_power {offset : ℕ} (ho : offset < 8) {i : ℕ} (h : i > 0):
    256^i / 2^offset = 256^(i-1) * 2^(8-offset)

lemma mul_div_256_off {offset : ℕ} (ho : offset < 8) {x : ℕ} (i : ℕ) (h : i > 0):
    (x * 256^i) / 2^offset = x * 256^(i-1) * 2^(8-offset)

lemma shifted_decomposition_eq {offset : ℕ} (ho : offset < 8) {x1 x2 : ℕ} :
    (x1 / 2 ^ offset + x2 % 2 ^ offset * 2 ^ (8-offset)) * 256 =
    (2^offset * (x1 / 2^offset) + (x2 % 2^offset) * 256) * 2^(8-offset)

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) + (x2 % 2^offset) * 256) * 2^(8-offset) * 256^(i-1)

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)

lemma soundness_simp {offset : ℕ} {x y : ℕ} :
    x % 2 ^ offset * 2 ^ (8-offset) * y + 2 ^ offset * (x / 2 ^ offset) * 2 ^ (8-offset) * y =
    x * y * 2^ (8-offset)

lemma soundness_simp' {offset : ℕ} {x : ℕ} :
    x % 2 ^ offset * 2 ^ (8-offset) + 2 ^ offset * (x / 2 ^ offset) * 2 ^ (8-offset) =
    x * 2^ (8-offset)

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

@[circuit_norm]
theorem bind_normalize {α β} (f : Circuit F α) (g : α → Circuit F β) : f.bind g = f >>= g

theorem completeness : Completeness (F p) elaborated Assumptions

theorem tableStatement (output : Row (F p)) : ∀ n > 0, ∀ trace,
    (formalTable output).statement n trace → output.y.value = fib32 n

theorem compose_computableWitnesses (circuit : ElaboratedCircuit F β α) (input : Var β F) (n : ℕ) :
  Environment.OnlyAccessedBelow n (eval · input) ∧ circuit.ComputableWitnesses →
    (circuit.main input).ComputableWitnesses n

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

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

lemma last_has_incoming_transition {α : Type*} (l : List α) (x : α)
    (h_len : l.length ≥ 2)
    (h_last : l.getLast? = some x) :
    ∃ y, (y, x) ∈ l.zip l.tail

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

lemma foldl_factor_const {α : Type*} [CommSemiring α] {n : ℕ} (f : Fin n → α) (c : α) (init : α) :
    Fin.foldl n (fun acc i => acc + f i * c) init =
    init + c * Fin.foldl n (fun acc i => acc + f i) 0

omit p_large_enough in
omit [Fact (Nat.Prime p)] in
@[circuit_norm]
lemma normalized_componentwise' (a b c d : field (F p)):
    (U32.mk a b c d).Normalized ↔
    (a.val < 256 ∧ b.val < 256 ∧ c.val < 256 ∧ d.val < 256)

lemma fieldFromBits_succ (n : ℕ) (bits : Vector (F p) (n + 1)) :
    fieldFromBits bits = fieldFromBits bits.pop + bits[n] * (2^n : F p)

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

theorem MemoryAccessList.filterAddress_addressTimestampSort_eq
    (accesses : MemoryAccessList)
    (h_sorted : accesses.isTimestampSorted)
    (h_nodup : accesses.Notimestampdup)
    (addr : ℕ) :
    (accesses.filterAddress addr).isConsistentSingleAddress
      (filterAddress_sorted accesses h_sorted addr) ↔
    (accesses.addressTimestampSort.filterAddress addr).isConsistentSingleAddress
      (filterAddress_sorted_from_addressTimestampSorted accesses.addressTimestampSort
        (addressTimestampSort_sorted accesses)
        (addressTimestampSort_noTimestampDup accesses h_nodup) addr)

lemma two_non_zero : (2 : F p) ≠ 0

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

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

theorem 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

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

theorem map_output_eq (f : Circuit F α) (g : α → β) (n : ℕ) :
  (g <$> f).output n = g (f.output 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 eval_decomposeNatExpr_small (env : Environment (F p)) (x : ℕ) :
    x < 256^4 ->
    (eval env (U32.decomposeNatExpr x)).value = x

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

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem fieldToBits_injective (n : ℕ) {x y : F p} : x.val < 2^n → y.val < 2^n →
    fieldToBits n x = fieldToBits n y → x = y

theorem completeness : Completeness (F p) elaborated Assumptions

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

theorem and_times_two_add_xor {x y : ℕ} (hx : x < 256) (hy : y < 256) : 2 * (x &&& y) + (x ^^^ y) = x + y

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

theorem soundness : Soundness (F p) elaborated Assumptions Spec

theorem soundness [DecidableEq F] : Soundness F (elaborated (F:=F) (M:=M)) Assumptions Spec

theorem MemoryAccessList.isConsistentOffline_of_cons
    (head : MemoryAccess) (tail : MemoryAccessList)
    (h_sorted : isAddressTimestampSorted (head :: tail))
    (h_offline : isConsistentOffline (head :: tail) h_sorted) :
    isConsistentOffline tail (isAddressTimestampSorted_of_cons head tail h_sorted)

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

theorem soundness : Soundness F elaborated Assumptions (Spec (F:=F))

lemma rotRight32_testBit_of_ge (x r i : ℕ) (h : x < 2^32) (hi : i ≥ 32 - r % 32) :
    (rotRight32 x r).testBit i = (decide (i < 32) && x.testBit (i - (32 - r % 32)))

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

theorem Composition.ofProductLength_mem_length {m : ℕ+} {α : Type} {l : List α} {hl : l.length = n * m.val}
  (comp : Composition l.length) (hcomp : comp = Composition.ofProductLength m hl) :
  ∀ li ∈ l.splitWrtComposition comp, li.length = m

lemma eval_vector_eq_get {M : TypeMap} [NonEmptyProvableType M] {n : ℕ} (env : Environment F)
    (vars : Vector (Var M F) n)
    (vals : Vector (M F) n)
    (h : (eval env vars : ProvableVector _ _ _) = (vals : ProvableVector _ _ _))
    (i : ℕ) (h_i : i < n) :
    eval env vars[i] = vals[i]

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

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

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

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

@[circuit_norm]
theorem forAll_append {condition : Condition F} {offset : ℕ} {as bs: Operations F} :
  forAll offset condition (as ++ bs) ↔
    forAll offset condition as ∧ forAll (as.localLength + offset) condition bs

lemma eval_foldl (env : Environment F) (n : ℕ)
    (f : Expression F → Fin n → Expression F) (init : Expression F)
    (hf : ∀ (e : Expression F) (i : Fin n),
      Expression.eval env (f e i) = Expression.eval env (f (Expression.const (Expression.eval env e)) i)) :
    Expression.eval env (Fin.foldl n f init) =
    Fin.foldl n (fun (acc : F) (i : Fin n) => Expression.eval env (f (Expression.const acc) i)) (Expression.eval env init)

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 foldlM_cons (x : α) :
  (Vector.cons x xs).foldlM circuit init = (do
    let init' ← circuit init x
    xs.foldlM circuit init')

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)

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

lemma tail_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).tail = (l.tail).take (n - 1)

theorem MemoryAccessList.filterAddress_empty_when_address_changes
    (head : MemoryAccess) (second : MemoryAccess) (tail : MemoryAccessList)
    (h_sorted : isAddressTimestampSorted (head :: second :: tail))
    (h_addr_ne : head.2.1 ≠ second.2.1) :
    filterAddress (second :: tail) head.2.1 = []

lemma localLength_cons {F} {op : FlatOperation F} {ops : List (FlatOperation F)} :
    localLength (op :: ops) = op.singleLocalLength + localLength ops

@[circuit_norm]
theorem eval_const {F : Type} [Field F] {α : TypeMap} [ProvableType α] {env : Environment F} {x : α F} :
    eval env (const x) = x

lemma zip_take_sublist (l1 l2 : List S) (n m : ℕ) :
    ((l1.take n).zip (l2.take m)).Sublist (l1.zip l2)

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

lemma forAll_toFlat_iff (n : ℕ) (condition : Condition F) (ops : Operations F) :
    FlatOperation.forAll n condition ops.toFlat ↔ ops.forAllFlat n condition

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

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

theorem inductPush_nil {motive : {n : ℕ} → Vector α n → Sort u}
  {nil : motive #v[]}
  {push : ∀ {n : ℕ} (as : Vector α n) (a : α), motive as → motive (as.push a)} :
    inductPush nil push #v[] = nil

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

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

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

lemma toBits_fromBits_aux {n : ℕ} (bits : Vector ℕ n)
  (h_bits : ∀ (i : ℕ) (hi : i < n), bits[i] = 0 ∨ bits[i] = 1) :
    (fromBits bits) < 2^n ∧ toBits n (fromBits bits) = bits

lemma eval_vector_take {M : TypeMap} [NonEmptyProvableType M] {n : ℕ} (env : Environment F)
    (vars : Var (ProvableVector M n) F) (i : ℕ) :
    (eval env (vars.take i) : ProvableVector _ _ _) = (eval env vars).take i

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

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

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

lemma fromByte_value {x : Fin 256} : (fromByte x).value (p:=p) = 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

lemma eval_vector_takeShort {M : TypeMap} [NonEmptyProvableType M] {n : ℕ} (env : Environment F)
    (vars : Var (ProvableVector M n) F) (i : ℕ) (h_i : i < n) :
    (eval env (vars.takeShort i h_i) : ProvableVector _ _ _) = (eval env vars).takeShort i h_i

@[circuit_norm ↓]
lemma mapFinRange.localLength_eq :
    (mapFinRange m body constant).localLength n = m * (body 0).localLength

lemma eval_fromLimbs {F} [Field F] {env : Environment F} {v : Vector (Expression F) 8} :
    eval env (U64.fromLimbs v) = .fromLimbs (v.map env)

lemma containsPath_take (R : Run S) (path : List S) (n : ℕ)
    (h_contains : R.containsPath path) :
    R.containsPath (path.take n)

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

Nat.add_sub_self_left in Init.Data.Nat.Basic

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

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

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

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

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

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

omit p_prime in
lemma two_pow_lt (n : ℕ) (hn : n ≤ 8) : 2^n < p

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

lemma sum_nat_cast_pos {α : Type*} [Fintype α] (f : α → ℕ) (a : α)
    (h_pos : f a > 0) :
    ∑ x : α, (f x : ℤ) > 0

theorem cast_take_append_of_eq_length {v : Vector α n} {w : Vector α m} :
    (v ++ w |>.take n |>.cast Nat.min_add_right_self) = v

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

lemma Vector.foldl_and_split {n1 n2 n3 : ℕ} (v : Vector ℕ n3)
    (v1 : Vector ℕ n1) (v2 : Vector ℕ n2) (h_sum : n1 + n2 = n3)
    (h_split : v = h_sum ▸ (v1 ++ v2)) :
    Vector.foldl (· &&& ·) 1 v =
    Vector.foldl (· &&& ·) 1 v1 &&& Vector.foldl (· &&& ·) 1 v2

omit p_large_enough in
lemma zify_bool {b : (F p)} (b_bool : IsBool b) : (↑(b.val) : ℤ) = 0 ∨ (↑(b.val) : ℤ) = 1

lemma cycle_netFlow_zero (cycle : List S) (x : S)
    (h_cycle : cycle.head? = cycle.getLast?) :
    Run.netFlow (fun t => countTransitionInPath t cycle) x = 0

theorem two_and_le_add {x y : ℕ} (hx : x < 256) (hy : y < 256) : 2 * (x &&& y) ≤ x + y

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

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

@[circuit_norm]
lemma FormalCircuit.weakenSpec_assumptions {F Input Output} [Field F] [ProvableType Input] [ProvableType Output]
    (c : FormalCircuit F Input Output) (WeakerSpec : Input F → Output F → Prop) h_spec_implication :
    (c.weakenSpec WeakerSpec h_spec_implication).Assumptions = c.Assumptions

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

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

<local_ctx>
import Clean.Utils.Field

import Clean.Utils.Bitwise

import Clean.Utils.Rotation

import Clean.Types.U64

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

variable [p_large_enough: Fact (p > 2^16 + 2^8)]

namespace Gadgets.Rotation64.Theorems

open Utils.Rotation

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

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

