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 FormalCircuit.toSubcircuit (circuit : FormalCircuit F β α)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

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

def FormalAssertion.toSubcircuit (circuit : FormalAssertion F β)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

{
    ops := ops.toFlat,
    Soundness env := circuit.Assumptions (eval env input_var) → circuit.Spec (eval env input_var),
    Completeness env := circuit.Assumptions (eval env input_var) ∧ circuit.Spec (eval env input_var),
    UsesLocalWitnesses _ := True,
    localLength := circuit.localLength input_var

imply_soundness := by admit /- proof elided -/

def GeneralFormalCircuit.toSubcircuit (circuit : GeneralFormalCircuit F β α)
    (n : ℕ) (input_var : Var β F) : Subcircuit F n :=
  let ops := circuit.main input_var |>.operations n
  have h_consistent : ops.SubcircuitsConsistent n := circuit.subcircuitsConsistent input_var n

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.Spec input output :=

@[circuit_norm]
def subcircuit (circuit : FormalCircuit F β α) (b : Var β F) : Circuit F (Var α F) :=
  fun offset =>
    let a := circuit.output b offset
    let subcircuit := circuit.toSubcircuit offset b
    (a, [.subcircuit subcircuit])

def ByteXorTable : Table (F p) fieldTriple := .fromStatic {
  name := "ByteXor"
  length := 256*256

row i :=
    let (x, y) := splitTwoBytes i
    (fromByte x, fromByte y, fromByte (x ^^^ y))

index := fun (x, y, _) => x.val * 256 + y.val

Spec := fun (x, y, z) =>
    x.val < 256 ∧ y.val < 256 ∧ z.val = x.val ^^^ y.val

contains_iff := by admit /- proof elided -/

def map {m : ℕ} (xs : Vector α m) (body : α → Circuit F β)
    (_constant : ConstantLength body := by admit /- proof elided -/
    ) : Circuit F (Vector β m) :=
  xs.mapM body

imply_soundness := by admit /- proof elided -/

@[reducible]
def TypeMap := Type → Type

@[reducible] def Var (M : TypeMap) (F : Type) := M (Expression F)

structure Table (F : Type) (Row : TypeMap) [ProvableType Row] where
  name : String
   
  Contains : Row F → Prop

Soundness : Row F → Prop
  Completeness : Row F → Prop

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

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

structure Lookup (F : Type) where
  table : RawTable F
  entry : Vector (Expression F) table.arity

@[circuit_norm]
def Table.toRaw (table : Table F Row) : RawTable F where
  name := table.name
  arity := size Row
  Contains row := table.Contains (fromElements row)
  Soundness row := table.Soundness (fromElements row)
  Completeness row := table.Completeness (fromElements row)
  imply_soundness row := table.imply_soundness (fromElements row)
  implied_by_completeness row := table.implied_by_completeness (fromElements row)

structure StaticTable (F : Type) (Row : TypeMap) [ProvableType Row] where
  name : String
  length : ℕ
  row : Fin length → Row F
  
  
  
  index : Row F → ℕ
  Spec : Row F → Prop
  contains_iff : ∀ t, (∃ i, t = row i) ↔ Spec t

def Contains (table : StaticTable F Row) (row : Row F) :=
  ∃ i : Fin table.length, row = table.row i

structure Variable (F : Type) where
  index : ℕ

inductive Expression (F : Type) where
  | var : Variable F -> Expression F
  | const : F -> Expression F
  | add : Expression F -> Expression F -> Expression F
  | mul : Expression F -> Expression F -> Expression F

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

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

@[reducible]
def TypeMap := Type → Type

@[reducible] def Var (M : TypeMap) (F : Type) := M (Expression F)

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

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

@[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 Circuit (F : Type) [Field F] (α : Type) := ℕ → α × List (Operation F)

@[reducible, circuit_norm]
def operations (circuit : Circuit F α) (offset : ℕ) : Operations F :=
  (circuit offset).2

@[reducible, circuit_norm]
def output (circuit : Circuit F α) (offset : ℕ) : α :=
  (circuit offset).1

@[reducible, circuit_norm]
def localLength (circuit : Circuit F α) (offset := 0) : ℕ :=
  Operations.localLength (circuit offset).2

@[circuit_norm]
def lookup {Row : TypeMap} [ProvableType Row] (table : Table F Row)  (entry : Row (Expression F)) : Circuit F Unit := fun _ =>
  ((), [.lookup { table := table.toRaw, entry := toElements entry }])

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

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

def Environment.UsesLocalWitnesses (env : Environment F) (offset : ℕ) (ops : Operations F) : Prop :=
  ops.forAllFlat offset { witness n _ compute := env.ExtendsVector (compute env) n }

class ElaboratedCircuit (F : Type) (Input Output : TypeMap) [Field F] [ProvableType Input] [ProvableType Output] where
  main : Var Input F → Circuit F (Var Output F)

localLength : Var Input F → ℕ

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

@[circuit_norm]
def Soundness (F : Type) [Field F] (circuit : ElaboratedCircuit F Input Output)
    (Assumptions : Input F → Prop) (Spec : Input F → Output 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) →
  
  let output := eval env (circuit.output input_var offset)
  Spec input output

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

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

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

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

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

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

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

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

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

class Witnessable (F : Type) [Field F] (value : outParam TypeMap) (var : TypeMap) [ProvableType value] where
  witness : ((Environment F) → value F) → Circuit F (var F)
  var_eq : var F = value (Expression F) := by admit /- proof elided -/

class ConstantLength (circuit : α → Circuit F β) where
  localLength : ℕ
  localLength_eq : ∀ (a : α) (n : ℕ), (circuit a).localLength n = localLength

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

@[reducible]
def TypeMap := Type → Type

@[reducible] def Var (M : TypeMap) (F : Type) := M (Expression F)

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

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

@[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 const (x : α F) : Var α F :=
  let values : Vector F _ := toElements x
  fromVars (values.map .const)

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

@[reducible] def field : TypeMap := id

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

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

instance ProvableType.fromStruct {α : TypeMap} [ProvableStruct α] : ProvableType α where
  size := combinedSize α
  toElements x :=
    toComponents x |> componentsToElements (components α) |>.cast combinedSize_eq.symm
  fromElements v :=
    v.cast combinedSize_eq |> componentsFromElements (components α) |> fromComponents
  fromElements_toElements x := by admit /- proof elided -/

def fromByte (x : Fin 256) : F p :=
  FieldUtils.natToField x.val (by admit /- proof elided -/
  )

contains_iff := by admit /- proof elided -/

def F p := ZMod p

def natToField (n : ℕ) (lt : n < p) : F p :=
  match p with
  | 0 => False.elim (Nat.not_lt_zero n lt)
  | _ + 1 => ⟨ n, lt ⟩

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

def concatTwoBytes (x y : Fin 256) : Fin (256 * 256) :=
  let i := x.val * 256 + y.val
  have i_lt : i < 256 * 256 := by admit /- proof elided -/

def fromByte (x : Fin 256) : F p :=
  FieldUtils.natToField x.val (by admit /- proof elided -/
  )

inductive FlatOperation (F : Type) where
  | witness : (m : ℕ) → (Environment F → Vector F m) → FlatOperation F
  | assert : Expression F → FlatOperation F
  | lookup : Lookup F → FlatOperation F

def ConstraintsHoldFlat (eval : Environment F) : List (FlatOperation F) → Prop
  | [] => True
  | op :: ops => match op with
    | assert e => (eval e = 0) ∧ ConstraintsHoldFlat eval ops
    | lookup { table, entry } =>
      table.Contains (entry.map eval) ∧ ConstraintsHoldFlat eval ops
    | _ => ConstraintsHoldFlat eval ops

@[circuit_norm]
def localLength : List (FlatOperation F) → ℕ
  | [] => 0
  | witness m _ :: ops => m + localLength ops
  | assert _ :: ops | lookup _ :: ops => localLength ops

@[circuit_norm]
def localWitnesses (env : Environment F) : (l : List (FlatOperation F)) → Vector F (localLength l)
  | [] => #v[]
  | witness _ compute :: ops => compute env ++ localWitnesses env ops
  | assert _ :: ops | lookup _ :: ops => localWitnesses env ops

@[circuit_norm]
def Environment.ExtendsVector (env : Environment F) (wit : Vector F n) (offset : ℕ) : Prop :=
  ∀ i : Fin n, env.get (offset + i.val) = wit[i.val]

structure Subcircuit (F : Type) [Field F] (offset : ℕ) where
  ops : List (FlatOperation F)

Soundness : Environment F → Prop
  Completeness : Environment F → Prop
  UsesLocalWitnesses : Environment F → Prop

localLength : ℕ

imply_soundness : ∀ env,
    ConstraintsHoldFlat env ops → Soundness env

implied_by_completeness : ∀ env, env.ExtendsVector (localWitnesses env ops) offset →
    Completeness env → ConstraintsHoldFlat env ops

imply_usesLocalWitnesses : ∀ env, env.ExtendsVector (localWitnesses env ops) offset →
    UsesLocalWitnesses env

localLength_eq : localLength = FlatOperation.localLength ops

inductive Operation (F : Type) [Field F] where
  | witness : (m : ℕ) → (compute : Environment F → Vector F m) → Operation F
  | assert : Expression F → Operation F
  | lookup : Lookup F → Operation F
  | subcircuit : {n : ℕ} → Subcircuit F n → Operation F

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

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

def toFlat : Operations F → List (FlatOperation F)
  | [] => []
  | .witness m c :: ops => .witness m c :: toFlat ops
  | .assert e :: ops => .assert e :: toFlat ops
  | .lookup l :: ops => .lookup l :: toFlat ops
  | .subcircuit s :: ops => s.ops ++ toFlat ops

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

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

@[circuit_norm]
def forAll (offset : ℕ) (condition : Condition F) : Operations F → Prop
  | [] => True
  | .witness m c :: ops => condition.witness offset m c ∧ forAll (m + offset) condition ops
  | .assert e :: ops => condition.assert offset e ∧ forAll offset condition ops
  | .lookup l :: ops => condition.lookup offset l ∧ forAll offset condition ops
  | .subcircuit s :: ops => condition.subcircuit offset s ∧ forAll (s.localLength + offset) condition ops

@[circuit_norm]
def SubcircuitsConsistent (offset : ℕ) (ops : Operations F) := ops.forAll offset {
  subcircuit offset {n} _ := n = offset
}

def FlatOperation.forAll (offset : ℕ) (condition : Condition F) : List (FlatOperation F) → Prop
  | [] => True
  | .witness m c :: ops => condition.witness offset m c ∧ forAll (m + offset) condition ops
  | .assert e :: ops => condition.assert offset e ∧ forAll offset condition ops
  | .lookup l :: ops => condition.lookup offset l ∧ forAll offset condition ops

def Operations.forAllFlat (n : ℕ) (condition : Condition F) (ops : Operations F) : Prop :=
  forAll n { condition with subcircuit n _ s := FlatOperation.forAll n condition s.ops } ops

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

Spec x := x.val < 2^two_exponent.val

let block_words := bytesToWords input.buffer_data

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

Spec : α F × α F → Prop
  | (x, y) => x = y

def numAux (assignment : CellAssignment W S) : ℕ :=
  assignment.vars.foldl (fun acc cell =>
    match cell with
    | .input _ => acc
    | .aux _ => acc + 1
  ) 0

def fromList (l : List α) : Vector α l.length := ⟨ .mk l, rfl ⟩

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

def fourRoundsApplyStyle : FormalCircuit (F p) Round.Inputs Round.Inputs :=
  fourRoundsWithPermute.weakenSpec FourRoundsSpec (by admit /- proof elided -/
  )

def main (offset : Fin 32) (x : Var U32 (F p)) : Circuit (F p) (Var U32 (F p)) := do
  let byte_offset : Fin 4 := ⟨ offset.val / 8, by admit /- proof elided -/
  ⟩
  let bit_offset : Fin 8 := ⟨ offset.val % 8, by admit /- proof elided -/
  ⟩

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

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

localLength_eq _ n := by admit /- proof elided -/

instance : ProvableStruct (Inputs M) where
  components := [field, M, M]
  toComponents := fun { selector, ifTrue, ifFalse } => .cons selector (.cons ifTrue (.cons ifFalse .nil))
  fromComponents := fun (.cons selector (.cons ifTrue (.cons ifFalse .nil))) => { selector, ifTrue, ifFalse }

def keccakPermutation (state : Vector ℕ 25): Vector ℕ 25 :=
  roundConstants.foldl keccakRound state

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

instance (α : TypeMap) [ProvableType α] : Witnessable F α (Var α) where
  witness := ProvableType.witness

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

def fromByte (x : Fin 256) : U32 (F p) :=
  ⟨ x.val, 0, 0, 0 ⟩

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

def Spec (x : F) (output : F) : Prop :=
  output = if x = 0 then 1 else 0

localLength _ := n + 2

def main (input : Expression (F p) × Expression (F p)) := do
  let a := input.1
  let b := input.2
  let out <== a + b - a*b
  return out

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

Add in Init.Prelude

def main (input : Var Inputs (F p)) : Circuit (F p) (Var BLAKE3State (F p)) := do
  let { state, chaining_value } := input

instance : ProvableStruct DecodedInstruction where
  components := [DecodedInstructionType, DecodedAddressingMode, DecodedAddressingMode, DecodedAddressingMode]
  toComponents := fun { instrType, mode1, mode2, mode3 } => .cons instrType (.cons mode1 (.cons mode2 (.cons mode3 .nil)))
  fromComponents := fun (.cons instrType (.cons mode1 (.cons mode2 (.cons mode3 .nil)))) => {
    instrType, mode1, mode2, mode3
  }

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

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

Assumptions := circuit.Assumptions
  Spec := circuit.Spec

instance elaborated : ElaboratedCircuit (F p) Inputs BLAKE3State where
  main := main
  localLength _ := 5376
  localLength_eq input i0 := by admit /- proof elided -/

assertZero ((1 - decoded.instrType.isLoadState) * (nextState.pc - (state.pc + 4)))
    assertZero ((1 - decoded.instrType.isLoadState) * (nextState.ap - state.ap))
    assertZero ((1 - decoded.instrType.isLoadState) * (nextState.fp - state.fp))

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

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

IsEmpty in Mathlib.Logic.IsEmpty

CoeFun in Init.Coe

soundness := by admit /- proof elided -/

InputAssumptions i block := block.Normalized

instance : Fact (pMersenne > 512) :=

computableWitnesses n input := by admit /- proof elided -/

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

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

def decomposeNat (x : ℕ) : U64 (F p) :=
  let x0 := x % 256
  let x1 : ℕ := (x / 256) % 256
  let x2 : ℕ := (x / 256^2) % 256
  let x3 : ℕ := (x / 256^3) % 256
  let x4 : ℕ := (x / 256^4) % 256
  let x5 : ℕ := (x / 256^5) % 256
  let x6 : ℕ := (x / 256^6) % 256
  let x7 : ℕ := (x / 256^7) % 256
  ⟨ x0, x1, x2, x3, x4, x5, x6, x7 ⟩

def absorbBlock (state : Vector ℕ 25) (block : Vector ℕ RATE) : Vector ℕ 25 :=
  
  let state' := Vector.mapFinRange 25 fun i => state[i] ^^^ (if _ : i.val < RATE then block[i] else 0)
  
  keccakPermutation state'

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

def len (_ : Vector α n) : ℕ := n

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)

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

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

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

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

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 fromLimbs {F} (v : Vector F 8) : U64 F := fromElements v

def main (n ops : ℕ)
    (inp : BinSumInput n ops (Expression (F p))) : Circuit (F p) (Vector (Expression (F p)) (nbits ((2^n - 1) * ops))) := do
  let nout := nbits ((2^n - 1) * ops)

for localDecl in ctx do
      if localDecl.isImplementationDetail then
        continue

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

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

Fin.castSucc in Init.Data.Fin.Basic

def toBits (n : ℕ) (x : ℕ) : Vector ℕ n :=
  .mapRange n fun i => if x.testBit i then 1 else 0

let sout <== parts.sum

instance : Fact (p > 512) :=

@[reducible, circuit_norm]
def forAll (circuit : Circuit F α) (n : ℕ) (prop : Condition F) :=
  (circuit.operations n).forAll n prop

HAnd in Init.Prelude

def Environment.AgreesBelow (n : ℕ) (env env' : Environment F) :=
  ∀ i < n, env.get i = env'.get i

def tail {M : ℕ} (trace : TraceOfLength F S M) : TraceOfLength F S (M - 1) :=
  ⟨ trace.val.tail, by admit /- proof elided -/
  ⟩

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

CommRing in Mathlib.Algebra.Ring.Defs

instance [DecidableEq F] : DecidableEq (field F) :=
  inferInstanceAs (DecidableEq F)

instance {α : TypeMap} [ProvableType α] : Zero (α F) where
  zero := fromElements (Vector.replicate _ 0)

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

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 assignment := ctx.assignment
  let generators := ctx.circuit.witnessGenerators

let out <== c.map fun (c0, c1) =>
    (c1 - c0) * s + c0
  return out

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

Assumptions input := input.val < 2^n

def main (input : Expression (F p)) := do
  let inp := input
  let out <== 1 + inp - 2*inp
  return out

Seq in Init.Prelude

ZMod.decidableEq in Mathlib.Data.ZMod.Defs

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

def circuit (n r : ℕ) [NeZero n] : FormalCircuit (F p) (fields n) (fields n) where
  main := main n r

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

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

def ProcessBlocksState.Normalized (state : ProcessBlocksState (F p)) : Prop :=
  (∀ i : Fin 8, state.chaining_value[i].Normalized) ∧
  state.chunk_counter.Normalized ∧
  state.blocks_compressed.Normalized

def var (b : Byte (F p)) := Expression.var b.1

def main (input : Expression (F p) × Expression (F p)) := do
  let diff := input.1 - input.2
  let out ← IsZero.circuit diff
  return out

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

let zeroU32 : Var U32 (F p) := ⟨0, 0, 0, 0⟩
  let blockLenU32 : Var U32 (F p) := ⟨(blockLen : F p), 0, 0, 0⟩

Bits2Num.main 254 input

MonadLift in Init.Prelude

def Run.hasCycle [DecidableEq S] (R : Run S) : Prop :=
  ∃ (cycle : List S), cycle.length ≥ 2 ∧
    cycle.head? = cycle.getLast? ∧
    R.containsPath cycle

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

let varType ← inferType (.fvar fvarId)
  let varType' ← whnf varType

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

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

partial def extractEqualities (e : Expr) : MetaM (List (Expr × Expr × Expr)) := do
  
  match e with
  | .app (.app (.const ``And _) left) right =>
    
    let leftEqs ← extractEqualities left
    let rightEqs ← extractEqualities right
    return leftEqs ++ rightEqs
  | _ =>
    
    if e.isAppOf `Eq then
      if let (some lhs, some rhs) := (e.getArg? 1, e.getArg? 2) then
        return [(e, lhs, rhs)]
    return []

instance : HSub (field (Expression F)) (Expression F) (Expression F) where
  hSub (x : Expression F) y := x - y

def Spec (input : Inputs (F p)) (out : Outputs (F p)) :=
  let ⟨x, y, carryIn⟩ := input
  out.z.val = (x.val + y.val + carryIn.val) % 256 ∧
  out.carryOut.val = (x.val + y.val + carryIn.val) / 256

Vector.toList in Init.Data.Vector.Basic

outParam in Init.Prelude

@[reducible]
def ProvableVector (α : TypeMap) (n : ℕ) := fun F => Vector (α F) n

@[reducible] def KeccakBlock := ProvableVector U64 RATE

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

reprStr in Init.Data.Repr

def Assumptions (input : U32 (F p)) := input.Normalized

let next_row := if h : idx < assignment.offset then
        let var := assignment.vars[idx]

nextStateCircuit { state, decoded, v1, v2, v3 }
    localLength := 30

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

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

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 : LawfulMonad (Circuit F) where
  bind_pure_comp {α β} (g : α → β) (f : Circuit F α) := by admit /- proof elided -/

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

List.count in Init.Data.List.Basic

def bits2bytes (x : ℕ) : ℕ :=
  (x + 7) / 8

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

@[circuit_norm]
def witnessVector (m : ℕ) (compute : Environment F → Vector F m) : Circuit F (Vector (Expression F) m) :=
  fun (offset : ℕ) =>
    let vars := varFromOffset (fields m) offset
    (vars, [.witness m compute])

class ExplicitCircuit (circuit : Circuit F α) where
   
  output : ℕ → α
  localLength : ℕ → ℕ
  operations : ℕ → Operations F

return nextState

def less_than_p (x : F p) : x.val < p :=

def circuit : FormalAssertion (F p) U32 where
  main
  Assumptions _ := True
  Spec inputs := inputs.Normalized

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

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

Vector.push in Init.Data.Vector.Basic

id in Init.Prelude

replaceMainGoal [currentGoal]

def pBabybear := 15 * 2^27 + 1

def TestAssumptions (_ : unit (F p)) : Prop := True

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

let input1 : Vector (Expression (F p)) n1 := input.take n1 |>.cast (by admit /- proof elided -/
    )
    let input2 : Vector (Expression (F p)) n2 := input.drop n1 |>.cast (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 }

soundness := by admit /- proof elided -/

def MemoryAccessList.isConsistentOnline (accesses : MemoryAccessList) (h : accesses.isTimestampSorted) : Prop := match accesses with
  | [] => True 
  | (_timestamp, addr, readValue, _writeValue) :: rest =>
    
    readValue = MemoryAccessList.lastWriteValue rest (List.Sorted.of_cons h) addr
    ∧ MemoryAccessList.isConsistentOnline rest (List.Sorted.of_cons h)

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

def witness (compute : Environment (F p) → F p) := do
  let x ← witnessVar compute
  lookup ByteTable (.var x)
  return Byte.mk x

structure Outputs (F : Type) where
  low : F
  high : F

def finalStateUpdate (state : Vector ℕ 16) (chaining_value : Vector ℕ 8) : Vector ℕ 16 :=
  #v[
    state[0] ^^^ state[8],
    state[1] ^^^ state[9],
    state[2] ^^^ state[10],
    state[3] ^^^ state[11],
    state[4] ^^^ state[12],
    state[5] ^^^ state[13],
    state[6] ^^^ state[14],
    state[7] ^^^ state[15],
    chaining_value[0] ^^^ state[8],
    chaining_value[1] ^^^ state[9],
    chaining_value[2] ^^^ state[10],
    chaining_value[3] ^^^ state[11],
    chaining_value[4] ^^^ state[12],
    chaining_value[5] ^^^ state[13],
    chaining_value[6] ^^^ state[14],
    chaining_value[7] ^^^ state[15]
  ]

let state_c ← Addition32.circuit ⟨state_c, state_d⟩

return fromVars resultVars

def TestAssumptions (_ : unit (F p)) : Prop := True

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

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

UInt16 in Init.Prelude

soundness : InductiveTable.Soundness F State Input Spec step

Assumptions input :=
    
    ∀ i (_ : i < 254), IsBool input[i]

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

Option in Init.Prelude

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

def Assumptions (input : U64 (F p)) := input.Normalized

Fin in Init.Prelude

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

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

BitVec in Init.Prelude

Fin.NatCast.instNatCast in Init.Data.Fin.Lemmas

@[reducible] def KeccakRow := ProvableVector U64 5

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

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

instance [Field F] : Inhabited (Expression F) where
  default := .const 0

Spec input output := output = input.rotate r

instance : HDiv (Expression F) F (Expression F) where
  hDiv e f := mul (f⁻¹ : F) e

let chunk_end_flag : Var U32 (F p) := ⟨(chunkEnd : F p), 0, 0, 0⟩
  let flags_with_start ← Or32.circuit { x := input.base_flags, y := start_flag }
  let final_flags ← Or32.circuit { x := flags_with_start, y := chunk_end_flag }

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

def boundaryFib : SingleRowConstraint RowType (F p) :=
  assignCurrRow { x := 0, y := 1 }

def fromLimbs {F} (v : Vector F 4) : U32 F := fromElements v

IsIrrefl in Mathlib.Order.Defs.Unbundled

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

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

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

completeness : InductiveTable.Completeness F State Input InputAssumptions InitialStateAssumptions Spec step

instance {x y : MemoryAccess} : Decidable (address_strict_timestamp_ordering x y) :=

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

Lean.Expr in Lean.Expr

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

instance : IsIrrefl MemoryAccess address_strict_timestamp_ordering :=

Finset.erase in Mathlib.Data.Finset.Erase

IO in Init.System.IO
</all_available_defs>

<all_available_lemmas>
theorem p_ne_zero : p ≠ 0

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

theorem natToField_eq {n : ℕ} {lt : n < p} (x : F p) (hx : x = natToField n lt) : x.val = n

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

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 two_val : (2 : F p).val = 2

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

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

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

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

lemma path_has_transition {S : Type*} [DecidableEq S] (path : List S)
    (h_len : path.length ≥ 2) :
    ∃ (t : Transition S), t ∈ path.zip path.tail

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

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

theorem MemoryAccessList.isConsistentSingleAddress_cons_forall (head : MemoryAccess) (tail : MemoryAccessList)
    (h_sorted : isTimestampSorted (head :: tail))
    : (∀ addr : ℕ, (filterAddress (head :: tail) addr).isConsistentSingleAddress (MemoryAccessList.filterAddress_sorted (head :: tail) h_sorted addr)) →
    (∀ addr : ℕ, isConsistentSingleAddress (filterAddress tail addr) (MemoryAccessList.filterAddress_sorted tail (by simp_all only [isTimestampSorted,
      List.sorted_cons]) addr))

@[circuit_norm]
theorem append_localLength {a b: Operations F} :
    (a ++ b).localLength = a.localLength + b.localLength

theorem Circuit.constraintsHold_toFlat_iff : ∀ {ops : Operations F}, ∀ {env : Environment F},
    ConstraintsHoldFlat env ops.toFlat ↔ ConstraintsHold env ops

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

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

theorem getElem_rotate {α : Type} {n : ℕ} {v : Vector α n} {off : ℕ} {i : ℕ} (hi : i < n) :
    (v.rotate off)[i] = v[(i + off) % n]'(Nat.mod_lt _ (Nat.pos_iff_ne_zero.mpr (Nat.ne_zero_of_lt hi)))

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

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

NeZero.pos in Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

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

theorem onlyAccessedBelow_all {ops : List (FlatOperation F)} (n : ℕ) :
  forAll n { witness n _ := Environment.OnlyAccessedBelow n } ops →
    Environment.OnlyAccessedBelow (n + localLength ops) (localWitnesses · ops)

lemma chi_loop (state : Vector ℕ 25) :
    Specs.Keccak256.chi state = .mapFinRange 25 fun i => state[i] ^^^ ((not64 state[i + 5]) &&& state[i + 10])

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

omit [Fact (Nat.Prime p)] p_large_enough in
theorem soundness_to_u64 {x y z : U64 (F p)}
  (x_norm : x.Normalized) (y_norm : y.Normalized)
  (h_eq :
    z.x0.val = x.x0.val ^^^ y.x0.val ∧
    z.x1.val = x.x1.val ^^^ y.x1.val ∧
    z.x2.val = x.x2.val ^^^ y.x2.val ∧
    z.x3.val = x.x3.val ^^^ y.x3.val ∧
    z.x4.val = x.x4.val ^^^ y.x4.val ∧
    z.x5.val = x.x5.val ^^^ y.x5.val ∧
    z.x6.val = x.x6.val ^^^ y.x6.val ∧
    z.x7.val = x.x7.val ^^^ y.x7.val) : Spec { x, y } z

lemma soundness : InductiveTable.Soundness (F p) ProcessBlocksState BlockInput Spec step

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

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

theorem foldlAcc_const (constant : ConstantLength (prod circuit))
  (h_const_out : ConstantOutput fun (t : β × α) => circuit t.1 t.2)
  (i : ℕ) (hi : i < m) :
  foldlAcc n xs circuit init ⟨ i, hi ⟩ = match i with

lemma containsPath_has_positive_transition (R : Run S) (path : List S)
    (h_contains : R.containsPath path) (t : Transition S)
    (h_in : t ∈ path.zip path.tail) :
    R t > 0

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

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

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

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 localLength_toFlat {ops : Operations F} :
    localLength ops.toFlat = ops.localLength

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

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

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

lemma forAll_append {condition : Condition F} {ops ops' : List (FlatOperation F)} (n : ℕ) :
  forAll n condition (ops ++ ops') ↔
    forAll n condition ops ∧ forAll (localLength ops + n) condition ops'

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

lemma getElem?_dynamicWitnesses_cons_right {op : FlatOperation F} {ops : List (FlatOperation F)} {init : List F} {i : ℕ} (hi : i < op.singleLocalLength) :
    (dynamicWitnesses (op :: ops) init)[init.length + i]?.getD 0 = (op.dynamicWitness init)[i]'(dynamicWitness_length (F:=F) ▸ hi)

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

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

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

theorem test_whole_struct_equality {F : Type} [Field F]
    (x : TestInputs F) (y : TestInputs F) (h : x = y) :
    x = y

lemma completeness : InductiveTable.Completeness (F p) ProcessBlocksState BlockInput InputAssumptions InitialStateAssumptions Spec step

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

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

lemma reachable_leaf_has_incoming_edge (R : Run S) (root leaf : S)
    (h_leaf : R.isLeaf root leaf)
    (h_ne : root ≠ leaf) :
    ∃ y, R (y, leaf) > 0

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

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

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

Nat.add_sub_self_left in Init.Data.Nat.Basic

lemma lift_val2 {x b : (F p)} (x_byte : x.val < 256) (b_bool : IsBool b) :
    (b * 256 + x).val = (b.val * 256 + x.val)

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

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

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

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

theorem toList_length_two {α : Type} (v : Vector α 2) :
    v.toList = [v[0], v[1]]

@[circuit_norm ↓]
theorem varFromOffset_fieldTriple {F} (offset : ℕ) :
  varFromOffset (F:=F) fieldTriple offset = (var ⟨offset⟩, var ⟨offset + 1⟩, var ⟨offset + 2⟩)

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

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

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

theorem completeness (rc : UInt64) : Completeness (F p) (elaborated rc) 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 forAll_flatten_abstract (circuit : Fin m → Circuit F β) (constant : ConstantLength circuit) :
  Operations.forAll n prop (List.ofFn fun i => (circuit i).operations (n + i * constant.localLength)).flatten
    ↔ ∀ (i : Fin m), (circuit i).forAll (n + i * constant.localLength) prop

lemma two_power_val {p : ℕ} {offset : Fin 8} [p_large_enough: Fact (p > 2^16 + 2^8)] :
    ((2 ^ (8 - offset.val) % 256 : ℕ) : F p).val = 2 ^ (8 - offset.val) % 256

lemma rotRight64_off_mod_64 (x : ℕ) (off1 off2 : ℕ) (h : off1 = off2 % 64) :
    rotRight64 x off1 = rotRight64 x off2

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

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

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

lemma sum_decrease {α : Type*} [Fintype α] [DecidableEq α] (f g : α → ℕ) (a : α)
    (h_a_decrease : g a < f a)
    (h_others_le : ∀ x, g x ≤ f x) :
    ∑ x : α, g x < ∑ x : α, f x

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

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

<local_ctx>
import Clean.Circuit.Basic

import Clean.Gadgets.Xor.ByteXorTable

import Clean.Utils.Primes

variable {p : ℕ} [Fact p.Prime] [p_large_enough: Fact (p > 512)]

namespace Gadgets.And.And8

open Xor (ByteXorTable)

open FieldUtils

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

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

def Spec (input : Inputs (F p)) (z : F p) :=
  let ⟨x, y⟩ := input
  z.val = x.val &&& y.val

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

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

<target_theorem>
theorem soundness : Soundness (F p) elaborated Assumptions Spec :=
</target_theorem>

