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>
Eq in Init.Prelude
id in Init.Prelude
BitVec in Init.Prelude
Nat in Init.Prelude
BitVec.cast in Init.Data.BitVec.Basic
BitVec.extractLsb in Init.Data.BitVec.Basic
BitVec.ofNat in Init.Prelude
Prod in Init.Prelude
BitVec.extractLsb' in Init.Data.BitVec.Basic
BitVec.setWidth in Init.Data.BitVec.Basic

class DCast (α : Sort*) (β : α → Sort*) where
  dcast : ∀ {a a' : α}, a = a' → β a → β a'
  dcast_id : ∀ {a : α}, dcast (Eq.refl a) = id

def isRead : MemoryOp ι α → Prop
  | read _ => True
  | _ => False

instance : Mul (UniPoly R) := ⟨UniPoly.mul⟩

List.ofFn in Init.Data.List.OfFn

def Option.doubleBind_v2 {α β γ : Type} (f : α → β → Option γ)
    (x : Option α) (y : Option β) : Option γ := do
  let a ← x
  let b ← y
  f a b

def implGroupEqOracle [BEq G] :
    QueryImpl (GroupEqOracle ι) (StateT (GroupValTable ι G) Option) where
  impl | query _ ⟨i, j⟩ => fun table =>
    match table i, table j with
    | some g₁, some g₂ => some (g₁ == g₂, table)
    | _, _ => none

hℓ_bound : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    Fintype.card (Gen_α i j).parℓ = 2
  hℓ_bound' : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    Fintype.card (parℓ_type i j) = 2

def duplexSpongeHybridOracle : OracleSpec pSpec.ChallengeIdx :=
  fun i =>
    ⟨StmtIn × ((j : pSpec.MessageIdx) → (j.1 < i.1) → Vector U (pSpec.Lₚᵢ j)),
    Vector U (pSpec.Lᵥᵢ i)⟩

instance : SliceLT (ProtocolSpec n) ℕ
    (fun _ stop => stop ≤ n)
    (fun _ stop _ => ProtocolSpec stop)
    where
  sliceLT := fun v stop h => take stop h v

def numPermQueriesChallenge (i : pSpec.ChallengeIdx) : Nat :=
  Nat.ceil ((challengeSize i : ℚ) / SpongeSize.R)

instance {s} : LawfulFunctor (fun α => LeafData α s) :=

sumcheckFinalCheck ∧ finalFoldingProp

protected def OracleVerifier.id :
    OracleVerifier oSpec Statement OStatement Statement OStatement !p[] where
  verify := fun stmt _ => pure stmt
  embed := Function.Embedding.inl
  hEq := fun _ => rfl

instance {pSpec : ProtocolSpec n} {Statement : Type}
    [DecidableEq Statement]
    [∀ i, DecidableEq (pSpec.Message i)]
    [∀ i, DecidableEq (pSpec.Challenge i)] :
    OracleSpec.DecidableEq (srChallengeOracle Statement pSpec) where
  domain_decidableEq' := fun i => by admit /- proof elided -/

HMod.hMod in Init.Prelude

def FullData.EquivIndexFun {α : Type} (s : Skeleton) :
    FullData α s ≃ (SkeletonNodeIndex s → α) where
  toFun := fun tree idx => tree.get idx
  invFun := fun f => FullData.ofFun s f
  left_inv := by admit /- proof elided -/

private def sum_choose_K_i (B : Finset (Fin n → F)) (i : Fin n) : ℚ :=
  ∑ (α : F), choose_2 (K B i α)

def principalIdeal {F : Type} [Semiring F] (f : F) : Ideal F := Ideal.span {f}

instance : Zero (Cayley T) where
  zero := zero

structure InterleavedCode (κ ι : Type*) [Fintype κ] [Fintype ι] (F : Type*) [Semiring F] where
  MF : MatrixSubmodule κ ι F
  LC : LinearCode ι F

inductive FullData (α : Type) : Skeleton → Type
  | leaf (value : α) : FullData α Skeleton.leaf
  | internal {left right} (value : α)
      (leftData : FullData α left)
      (rightData : FullData α right) :
      FullData α (Skeleton.internal left right)
  deriving Repr

def churchAnd (p q : ChurchBool α) : ChurchBool α :=
  fun x y => p (q x y) y

structure SumcheckMultiplierParam (L : Type) [CommRing L] (ℓ : ℕ) (Context : Type := Unit) where
  multpoly : (ctx: Context) → MultilinearPoly L ℓ

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

def oracleVerifier : OracleVerifier oSpec Statement OStatement Unit (OStatement ⊕ᵥ OStatement)
    (pSpec OStatement) where

ReaderT in Init.Prelude

def pSpecFullNonLastBlock (bIdx : Fin (ℓ / ϑ - 1)) :=
  (pSpecFoldRelaySequence (L:=L) (n:=ϑ - 1) ++ₚ
      pSpecFoldCommit 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        ⟨↑bIdx * ϑ + (ϑ - 1), by admit /- proof elided -/
          ⟩)

noncomputable def queryOracleVerifier :
  OracleVerifier
    (oSpec := []ₒ)
    (StmtIn := FinalSumcheckStatementOut (L:=L) (ℓ:=ℓ))
    (OStmtIn := OracleStatement 𝔽q β (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (
    Fin.last ℓ))
    (StmtOut := Bool)
    (OStmtOut := fun _ : Empty => Unit)
    (pSpec := pSpecQuery 𝔽q β γ_repetitions (h_ℓ_add_R_rate := h_ℓ_add_R_rate)) where
  verify := fun (stmt: FinalSumcheckStatementOut (L:=L) (ℓ:=ℓ))
    (challenges: (pSpecQuery 𝔽q β γ_repetitions (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).Challenges) => do
    
    let c := stmt.final_constant
    let fold_challenges : Fin γ_repetitions → sDomain 𝔽q β h_ℓ_add_R_rate 0 :=
      challenges ⟨0, by admit /- proof elided -/
      ⟩

is_rbr_knowledge_sound :
    OracleProof.rbrKnowledgeSoundness (pure ()) ⟨isEmptyElim⟩ relation vectorIOP.verifier ε_rbr

Fin.castSuccEmb in Mathlib.Data.Fin.Embedding

instance : Fact (Nat.Prime SCALAR_FIELD_CARD) := ⟨ScalarField_is_prime⟩

instance {α : Type u} : Slice (List α) Nat Nat (fun _ _ _ => True) (fun _ _ _ _ => List α) where
  slice xs start stop _ := xs.extract start stop

C : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), Set ((indexPowT (S i) (P.φ i) j) → F)
  hcode : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), (C i j) = (Gen_α i j).C

def fullRound (params : Params) (state : Vector KoalaBear.Field params.width)
    (roundConstants : Vector KoalaBear.Field params.width) : Vector KoalaBear.Field params.width :=
  
  let stateWithConstants := state.zipWith (·+·) roundConstants
  
  let stateAfterSbox := stateWithConstants.map (fun x => x ^ sBoxDegree)
  
  externalLinearLayer params stateAfterSbox

def Reduction.liftContext
    (lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
    (R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec) :
      Reduction oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut pSpec where
  prover := R.prover.liftContext lens
  verifier := R.verifier.liftContext lens.stmt

Algebra in Mathlib.Algebra.Algebra.Defs

instance : HasSucc (Cayley T) where
  succ' := succ

noncomputable def relayRbrExtractor (i : Fin ℓ) :
  Extractor.RoundByRound []ₒ
    (StmtIn := (Statement (L := L) Context i.succ) × (∀ j, OracleStatement 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc j))
    (WitIn := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
    (WitOut := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
    (pSpec := pSpecRelay)
    (WitMid := fun _messageIdx => Witness (L := L) 𝔽q β
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) where
  eqIn := rfl
  extractMid := fun _ _ _ witMidSucc => witMidSucc
  extractOut := fun _ _ witOut => witOut

Polynomial.support in Mathlib.Algebra.Polynomial.Basic

noncomputable def Xⱼ (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) : L[X] :=
  (Finset.univ : Finset (Fin ℓ)).prod
    (fun i => (normalizedW 𝔽q β (Fin.castLE h_ℓ i))^(Nat.getBit i j))

@[simp]
abbrev OracleStatement.AfterSendEvalClaim : R1CS.MatrixIdx ⊕ R1CS.MatrixIdx ⊕ Fin 1 → Type :=
  Sum.elim (EvalClaim R) (OracleStatement.AfterFirstSumcheck R pp)

Fin.tail in Mathlib.Data.Fin.Tuple.Basic

def take (j : Fin (k + 1)) (messages : MessagesUpTo k pSpec) :
    MessagesUpTo (j.castLE (by admit /- proof elided -/
    )) pSpec :=
  fun i => messages ⟨i.val.castLE (by admit /- proof elided -/
  ), i.property⟩

@[reducible]
def pSpec : ProtocolSpec 1 :=
  ⟨!v[.V_to_P], !v[Fin l → evalDomain D x 0]⟩

@[reducible]
def rateSegment (state : CanonicalSpongeState U) : Vector U SpongeSize.R :=
  
  (Vector.take state SpongeSize.R).cast (by admit /- proof elided -/
  )

Fin in Init.Prelude

@[simp]
def 𝕏 (k : ℕ) : BTField (k+1) := Z (k+1)

instance : Zero AssocNat where
  zero := zero

def coeffsToBitVec {n : ℕ} (coeffs : List (ZMod 2)) : BitVec n :=
  let val := List.foldr (fun c acc => acc * 2 + c.val) 0 (coeffs.take n)
  BitVec.ofNat n val

Lean.Name in Init.Prelude

HomogeneousPow in Init.Prelude

def fillNextUnits (state : FSVerifierState U H) (count : Nat) :
    Except DomainSeparatorMismatch (FSVerifierState U H × Array U) := do
  
  let bytesNeeded := count * HasSize.size U UInt8
  if state.nargString.size < bytesNeeded then
    .error {
      message := s!"Insufficient transcript remaining, need {bytesNeeded} bytes,
        got {state.nargString.size}" }
  else
    
    let readBytes := state.nargString.extract 0 bytesNeeded
    let remaining := state.nargString.extract bytesNeeded state.nargString.size
    
    let units := Array.range count |>.mapM (fun i =>
      let unitBytes := readBytes.extract (i * HasSize.size U UInt8) (HasSize.size U UInt8)
      DeserializeOption.deserialize unitBytes)
    match units with
    | some unitsArray =>
      
      let newHashState ← state.hashState.absorb unitsArray
      .ok ({ hashState := newHashState, nargString := remaining }, unitsArray)
    | none =>
      .error { message := "Failed to deserialize units from NARG string" }

@[ext]
structure VectorSpec (n : ℕ) where
  dir : Fin n → Direction
  length : Fin n → Nat

alias Prover.trivial := Prover.id
alias Verifier.trivial := Verifier.id
alias Reduction.trivial := Reduction.id
alias OracleProver.trivial := OracleProver.id
alias OracleVerifier.trivial := OracleVerifier.id
alias OracleReduction.trivial := OracleReduction.id

verify := fun stmt _ => relComp stmt

def bivPolyHom {F : Type} [CommRing F] [IsDomain F] :
  Polynomial (F[X]) →+* Polynomial (RatFunc F) := Polynomial.mapRingHom (univPolyHom)

instance {s} : Functor (fun α => FullData α s) where
  map f x := x.map f

noncomputable def polyQuotient (S : Finset F) (fPoly : F[X]) : F[X] :=
    (fPoly - (ansPoly S (fun s => fPoly.eval s))) / (vanishingPoly S)

instance irreducible_quadratic_defining_poly_of_traceMap_eq_1
  {F : Type*} [Field F] [Fintype F] [CharP F 2] (s : F) [NeZero s] (k : ℕ)
  (trace_map_prop : TraceMapProperty F s k)
  (fintypeCard : Fintype.card F = 2 ^ (2 ^ k))
  : Irreducible (definingPoly s) :=

Real in Mathlib.Data.Real.Basic

@[inline] def lagrangeToMonoLevel {n : ℕ} (j : Fin n) : Vector R (2 ^ n) → Vector R (2 ^ n) :=
  fun v =>
    let stride : ℕ := 2 ^ j.val  
    Vector.ofFn (fun i : Fin (2 ^ n) =>
      if (BitVec.ofFin i).getLsb j then
        v[i] - v[i - stride]'(Nat.sub_lt_of_lt i.isLt)
      else
        v[i])

@[reducible]
noncomputable def fullOracleProof :
  OracleProof []ₒ
    (Statement := Statement (L := L) (ℓ:=ℓ) (SumcheckBaseContext L ℓ) 0)
    (OStatement := OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ 0)
    (Witness := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ:=ℓ) 0)
    (pSpec:=fullPSpec 𝔽q β γ_repetitions (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)) :=
  fullOracleReduction 𝔽q β γ_repetitions (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑)

def combined : Prop :=
  capacitySegmentDup trace ∨ notFunction trace

def churchFalse : ChurchBool α := fun _ y => y

def getFirstOracle {i : Fin (ℓ + 1)}
    (oStmt : (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i j)) :
    sDomain 𝔽q β h_ℓ_add_R_rate 0 → L :=

alias «𝒟_Σ» := duplexSpongeHybridOracle

OracleComp.liftComp in VCVio.OracleComp.Coercions.SubSpec

instance instOneConcreteBTField (k : ℕ) : One (ConcreteBTField k) where
  one := one

@[inline]
def seqCompose {m : ℕ}
    (Stmt : Fin (m + 1) → Type) {ιₛ : Fin (m + 1) → Type} (OStmt : (i : Fin (m + 1)) → ιₛ i → Type)
    (Wit : Fin (m + 1) → Type) {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    (P : (i : Fin m) →
      OracleProver oSpec (Stmt i.castSucc) (OStmt i.castSucc) (Wit i.castSucc)
        (Stmt i.succ) (OStmt i.succ) (Wit i.succ) (pSpec i)) :
    OracleProver oSpec (Stmt 0) (OStmt 0) (Wit 0) (Stmt (Fin.last m)) (OStmt (Fin.last m))
      (Wit (Fin.last m)) (seqCompose pSpec) :=
  Prover.seqCompose (fun i => Stmt i × (∀ j, OStmt i j)) Wit P

def knowledgeSoundness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut))
    (verifier : Verifier oSpec StmtIn StmtOut pSpec) (knowledgeError : ℝ≥0) : Prop :=
  ∃ extractor : Extractor.Straightline oSpec StmtIn WitIn WitOut pSpec,
  ∀ stmtIn : StmtIn,
  ∀ witIn : WitIn,
  ∀ prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec,
    letI reduction := Reduction.mk prover verifier
    [fun ⟨stmtIn, witIn, stmtOut, witOut⟩ =>
      (stmtIn, witIn) ∉ relIn ∧ (stmtOut, witOut) ∈ relOut
    | do
      let s ← init
      (simulateQ (impl ++ₛₒ challengeQueryImpl : QueryImpl _ (StateT σ ProbComp))
        <| do
      let ⟨⟨⟨transcript, ⟨_, witOut⟩⟩, stmtOut⟩, proveQueryLog, verifyQueryLog⟩ ←
        reduction.runWithLog stmtIn witIn
      let extractedWitIn ←
        liftComp (extractor stmtIn witOut transcript proveQueryLog.fst verifyQueryLog) _
      return (stmtIn, extractedWitIn, stmtOut, witOut)).run' s] ≤ knowledgeError

List.cons in Init.Prelude

instance : Fintype (pSpec.MessageIdx) := Subtype.fintype (fun i => pSpec.dir i = .P_to_V)

def oracleVerifier : OracleVerifier oSpec (StmtIn R) (OStmtIn R deg) (StmtOut R) (OStmtOut R deg)
    (pSpec R deg) where
  verify := fun target chal => do
    let evals : Vector R m ← (Vector.finRange m).mapM
      (fun i => query (spec := [OStmtIn R deg]ₒ) () (D i))
    guard (evals.sum = target)
    
    pure (sorry, chal default)
  embed := .inl
  hEq := fun i => by admit /- proof elided -/

@[reducible]
noncomputable def fullOracleVerifier :
  OracleVerifier (oSpec:=[]ₒ)
    (StmtIn := Statement (L := L) (ℓ:=ℓ) (SumcheckBaseContext L ℓ) 0)
    (OStmtIn:= OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ 0)
    (StmtOut := Bool)
    (OStmtOut := fun _ : Empty => Unit)
    (pSpec := fullPSpec 𝔽q β γ_repetitions (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)) :=
  OracleVerifier.append (oSpec:=[]ₒ)
    (Stmt₁ := Statement (L := L) (SumcheckBaseContext L ℓ) 0)
    (Stmt₂ := FinalSumcheckStatementOut (L:=L) (ℓ:=ℓ))
    (Stmt₃ := Bool)
    (OStmt₁ := OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ 0)
    (OStmt₂ := OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (Fin.last ℓ))
    (OStmt₃ := fun _ : Empty => Unit)
    (pSpec₁ := pSpecCoreInteraction 𝔽q β (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
    (pSpec₂ := pSpecQuery 𝔽q β γ_repetitions (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
    (V₁ := CoreInteraction.coreInteractionOracleVerifier 𝔽q β
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ϑ:=ϑ))
    (V₂ := QueryPhase.queryOracleVerifier 𝔽q β γ_repetitions
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ϑ:=ϑ))

instance : Unique (Transcript 0 pSpec) where
  default := fun i => Fin.elim0 i
  uniq := fun T => by admit /- proof elided -/

@[reducible, inline, specialize, simp]
def Message (pSpec : ProtocolSpec n) (i : MessageIdx pSpec) := pSpec.«Type» i.val

def verifyEqOne (n a' : Q(ℕ)) (a : Q(ZMod $n)) (_ : Q(($a' : ZMod $n) = $a)) :
    MetaM Q($a ^ ($n - 1) = 1) := do
  let p : Q(ZMod $n) := q($a ^ ($n - 1))
  let .isNat _ c hc ← Tactic.ReduceModChar.normIntNumeral n p
    q(CommRing.toRing) q(ZMod.charP $n) | failure
  assumeInstancesCommute
  haveI : $p =Q $a ^ ($n - 1) := ⟨⟩
  haveI : $c =Q 1 := ⟨⟩
  return q(ZMod.bla $a (.refl _) $hc)

def modSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j, n j)) : Fin (n (divSum k)) :=
  ⟨k - ∑ j, n (Fin.castLE (divSum k).isLt.le j), by admit /- proof elided -/
    ⟩

def BacktrackSequence.Index (trace : QueryLog (duplexSpongeChallengeOracle StmtIn U))
    (state : CanonicalSpongeState U) (seq : BacktrackSequence trace state) :
    Fin trace.length × (Fin seq.inputState.length → Fin trace.length) :=
  
  
  
  (⟨trace.findIdx sorry, sorry⟩, sorry)

example : !v[1, 2] ++ᵛ !v[3, 4] = !v[1, 2, 3, 4] := rfl
example : (0 : ℕ) ::ᵛ !v[1, 2] = !v[0, 1, 2] := rfl
example : !v[1, 2] :+ᵛ (3 : ℕ) = !v[1, 2, 3] := rfl

def canonical (p : UniPoly R) := p.trim = p

def AlgebraTowerEquiv.algebraMapLeftUp (e : AlgebraTowerEquiv A B) (i j : ι)
    (h : i ≤ j) : (B i) →+* (A j) :=

private def Fi (B : Finset (Fin n → F)) (i : Fin n) (α : F) : Finset (Fin n → F) :=
  { x | x ∈ B ∧ x i = α }

CanLift in Mathlib.Tactic.Lift

Unique in Mathlib.Logic.Unique

def tileCoeffs (a : Fin (2 ^ ℓ) → L) : Fin (2^(ℓ + R_rate)) → L :=
  fun v => a (Fin.mk (v.val % (2^ℓ)) (Nat.mod_lt v.val (pow_pos (zero_lt_two) ℓ)))

@[ext]
structure OracleVerifier {ι : Type} (oSpec : OracleSpec ι)
    (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type)
    (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type)
    {n : ℕ} (pSpec : ProtocolSpec n)
    [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)]
    [Oₘ : ∀ i, OracleInterface (pSpec.Message i)]
    where

class Extractor.Lens.IsKnowledgeSound
    {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
    {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type}
    (outerRelIn : Set (OuterStmtIn × OuterWitIn))
    (innerRelIn : Set (InnerStmtIn × InnerWitIn))
    (outerRelOut : Set (OuterStmtOut × OuterWitOut))
    (innerRelOut : Set (InnerStmtOut × InnerWitOut))
    (compatStmt : OuterStmtIn → InnerStmtOut → Prop)
    (compatWit : OuterWitOut → InnerWitIn → Prop)
    (lens : Extractor.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                            OuterWitIn OuterWitOut InnerWitIn InnerWitOut) where

@[simp]
instance BTFieldIsDomain (k : ℕ) : IsDomain (BTField k) := inferInstance

noncomputable def commitOracleVerifier (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) :
  OracleVerifier
    (oSpec := []ₒ)
    (StmtIn := Statement (L := L) Context i.succ)
    (OStmtIn := OracleStatement 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc)
    (Oₘ := fun i => by admit /- proof elided -/
    )
    
    (StmtOut := Statement (L := L) Context i.succ)
    (OStmtOut := OracleStatement 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
    (pSpec := pSpecCommit 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) where

Equivalence in Init.Core

HSMul in Init.Prelude

def leq {α : Type} (m n : ChurchNat α) : ChurchBool α :=
  isZero (ChurchNat.sub m n)

instance instDCast : DCast Nat ProtocolSpec where
  dcast h := ProtocolSpec.cast h
  dcast_id := cast_id

def β (R : F[X][X][Y]) (t : ℕ) : 𝒪 H :=
  (β_regular R H (Nat.le_refl _) t).choose

Nat.and_distrib_right in Init.Data.Nat.Bitwise.Lemmas

@[inline] def pred [Zero T] [ToNat T] (a : Cayley T) : Cayley T :=
  match (↑a : Nat) with
  | 0 => zero
  | Nat.succ n => ofNat n

USize.ofNat in Init.Data.UInt.BasicAux

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

instance : Fact (Nat.Prime baseFieldSize) := ⟨BaseField_is_prime⟩

LinearOrder in Mathlib.Order.Defs.LinearOrder

noncomputable def xPoly
  {S : Finset ι} (f : ι → F) (φ : ι ↪ F) (k : ℕ) (x : indexPow S φ k) : Polynomial F :=
  let dom := powFiber S φ k x
  let emb : { y // y ∈ dom } → F := φ ∘ Subtype.val
  let g : { y // y ∈ dom } → F := f ∘ Subtype.val
  Lagrange.interpolate univ emb g

def fappend {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A}
    (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) :
    (i : Fin (m + n)) → F (Fin.vappend α β i) :=
  match n with
  | 0 => u
  | k + 1 => fconcat (fappend u (fun i => v (Fin.castSucc i))) (v (Fin.last k))

@[simp]
def evalDomain (i : ℕ) : Subgroup Fˣ :=
  Subgroup.zpowers (DIsCyclicC.gen ^ (2 ^ i))

OracleSpec.range in VCVio.OracleComp.OracleSpec

def closePtsOnAffineLine {ι : Type*} [Fintype ι]
                         (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) :=
  {x : ι → F | x ∈ Affine.line u v ∧ distFromCode x (ReedSolomon.code α deg) ≤ e}

@[simps]
def refl (pSpec : ProtocolSpec n) : Equiv pSpec pSpec where
  round_eq := rfl
  dir_eq := fun _ => rfl
  typeEquiv := fun _ => _root_.Equiv.refl _

proj_knowledgeSound : ∀ outerStmtIn innerStmtOut outerWitOut,
    compatStmt outerStmtIn innerStmtOut →
    (lens.stmt.lift outerStmtIn innerStmtOut, outerWitOut) ∈ outerRelOut →
    (innerStmtOut, lens.wit.proj (outerStmtIn, outerWitOut)) ∈ innerRelOut

@[reducible, simp]
def oraclePSpec : ProtocolSpec 1 := ⟨!v[.P_to_V], !v[Witness]⟩

UInt64.ofFin in Init.Data.UInt.Basic

noncomputable def ElocPolyF (ωs f : Fin n → F) (p : Polynomial F) : Polynomial F :=
  ElocPoly n (liftF ωs) (liftF f) p

def renameMessage (pSpec : ProtocolSpec n) (NewMessage : pSpec.MessageIdx → Type) :
    ProtocolSpec n :=
  ⟨ pSpec.dir,
    fun i => if h : pSpec.dir i = Direction.P_to_V then NewMessage ⟨i, h⟩ else pSpec.«Type» i⟩

instance [ProverFirst pSpec] : Unique (pSpec.MessageIdx) where
  default := ⟨0, by admit /- proof elided -/
  ⟩
  uniq := fun ⟨i, _⟩ => by admit /- proof elided -/

Units.val in Mathlib.Algebra.Group.Units.Defs

inductive Skeleton :
    (n : ℕ) → (ar : Fin n → ℕ) → Type where
  | leaf {ar0 : Fin 0 → ℕ} : Skeleton 0 ar0
  | node {n : ℕ} {ar : Fin (n+1) → ℕ}
      (children : Fin (ar 0) →
        Skeleton n (fun i => ar i.succ)) :
      Skeleton (n+1) ar

instance : IsCyclic G :=
  isCyclic_of_prime_card PrimeOrder.hCard

def QuotientUniPoly (R : Type*) [Ring R] [BEq R] := Quotient (@instSetoidUniPoly R _)

instance instDCast₁₂ : DCast (β a) (γ a) where
  dcast hb c := dcast₂ (Eq.refl a) (by admit /- proof elided -/
  ) c
  dcast_id := by admit /- proof elided -/

instance : VAdd (ι → F) (AffineSubspace F (ι → F)) := AffineSubspace.pointwiseVAdd

instance (s : Finset σ) : Fintype { x : σ | x ∈ s } :=

Fintype.card in Mathlib.Data.Fintype.Card

noncomputable def batchOracleReduction :
  OracleReduction []ₒ
    Unit (OracleStatement D x m) (Witness F s d m)
    ((Fin m → F) × Fri.Spec.Statement F (0 : Fin (k + 1)))
    (OracleStatement D x m)
    (Fri.Spec.Witness F s d (0 : Fin (k + 2)))
    (batchSpec F m) where
  prover := batchProver D x s d m
  verifier := batchVerifier (k := k) D x m

instance instOracleInterfaceMessagePSpec : ∀ i, OracleInterface ((pSpec R deg).Message i) :=
  instOracleInterfaceMessageAppend

instance : Fact (Nat.Prime (PrimeOrder.p G)) :=
  PrimeOrder.hPrime

noncomputable def fullRbrKnowledgeError (i : (fullPSpec 𝔽q β γ_repetitions (ϑ := ϑ)
    (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).ChallengeIdx) : ℝ≥0 :=
  Sum.elim (f := CoreInteraction.coreInteractionOracleRbrKnowledgeError 𝔽q β (ϑ:=ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
    (g := QueryPhase.queryRbrKnowledgeError 𝔽q β γ_repetitions (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
    (ChallengeIdx.sumEquiv.symm i)

h : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    hasMutualCorrAgreement (Gen_α i j)
      (BStar i j (C i j) (Gen_α i j).parℓ)
      (errStar i j (C i j) (Gen_α i j).parℓ)

def Prover.duplexSpongeFiatShamir (P : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) :
    NonInteractiveProver (∀ i, pSpec.Message i) (oSpec ++ₒ duplexSpongeChallengeOracle StmtIn U)
      StmtIn WitIn StmtOut WitOut where
  PrvState := fun i => match i with
    | 0 => StmtIn × P.PrvState 0
    | _ => P.PrvState (Fin.last n)
  input := fun ctx => ⟨ctx.1, P.input ctx⟩
  
  sendMessage | ⟨0, _⟩ => fun ⟨stmtIn, state⟩ => do
    let ⟨messages, _, state⟩ ← P.runToRoundDSFS (Fin.last n) stmtIn state
    return ⟨messages, state⟩
  
  receiveChallenge | ⟨0, h⟩ => nomatch h
  output := fun st => (P.output st).liftComp _

def BinaryTowerAux (k : ℕ) : (Σ' (F : Type 0), BinaryTowerResult F k) :=
  match k with
  | 0 => 
    let curBTField := GF(2)
    let newList : List.Vector (GF(2)) 1 := List.Vector.cons (1 : GF(2)) List.Vector.nil
    let specialElement : GF(2) := newList.1.headI
    let firstElementOfVecIsSpecialElement : newList.1.headI = specialElement := rfl
    let specialElementIs1 : specialElement = 1 := by admit /- proof elided -/

def Reduction.addSalt (R : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec)
    (saltComp : (i : pSpec.MessageIdx) → R.prover.PrvState i.1.castSucc →
      OracleComp oSpec (Salt i)) :
    Reduction oSpec StmtIn WitIn StmtOut WitOut (pSpec.addSalt Salt) where
  prover := R.prover.addSalt Salt saltComp
  verifier := R.verifier.addSalt Salt

instance : SubSpec [pSpec₂.Challenge]ₒ ([(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) where
  monadLift | query i t => instSubSpecOfProtocolSpecAppendChallenge.monadLift (query (Sum.inr i) t)

def outputRelation :
    Set
      (
        (Fri.Spec.Statement F (0 : Fin (k + 1)) ×
        (∀ j, Fri.Spec.OracleStatement D x s (0 : Fin (k + 1)) j)) ×
        Fri.Spec.Witness F s d (0 : Fin (k + 2))
      ) := sorry

def relOut : Set ((Unit × (∀ i, (Sum.elim OStatement OStatement) i)) × Unit) :=
  setOf (fun ⟨⟨(), oracles⟩, _⟩ => oracles (.inl default) = oracles (.inr default))

instance : ∀ i, SelectableType ((pSpecSumcheckFold 𝔽q β (ϑ:=ϑ)
  (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).Challenge i) := instSelectableTypeChallengeAppend

instance : ∀ j, OracleInterface ((fullPSpec 𝔽q β γ_repetitions (ϑ:=ϑ)
  (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).Message j) := instOracleInterfaceMessageAppend

exp : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), (parℓ_type i j) ↪ ℕ

hEq := sorry

private noncomputable def evenPart' (f : Polynomial F) : Polynomial F :=
  match f with
  | ⟨⟨supp, f, pr⟩⟩ => ⟨⟨erase_odd supp, fun n => if Even n then f n else 0, by admit /- proof elided -/
  ⟩⟩

for rep in (List.finRange γ_repetitions) do
      let mut c_cur : L := 0 
      let v := fold_challenges rep

instance [VerifierFirst pSpec] [h : VCVCompatible (pSpec.«Type» 0)] :
    ∀ i, VCVCompatible (pSpec.Challenge i)
  | ⟨0, _⟩ => inferInstance

Rat in Init.Data.Rat.Basic

def SkeletonNodeIndex.parent {s : Skeleton} (idx : SkeletonNodeIndex s) :
    Option (SkeletonNodeIndex s) :=
  match idx with
  | SkeletonNodeIndex.ofLeaf => none
  | SkeletonNodeIndex.ofInternal => none
  | SkeletonNodeIndex.ofLeft (.ofLeaf) => some .ofInternal
  | SkeletonNodeIndex.ofLeft (.ofInternal) => some .ofInternal
  | SkeletonNodeIndex.ofLeft idxLeft =>
    idxLeft.parent.map (SkeletonNodeIndex.ofLeft)
  | SkeletonNodeIndex.ofRight (.ofLeaf) => some .ofInternal
  | SkeletonNodeIndex.ofRight (.ofInternal) => some .ofInternal
  | SkeletonNodeIndex.ofRight idxRight =>
    idxRight.parent.map (SkeletonNodeIndex.ofRight)

structure Selector (𝓡 : Type*) where
   
  qL : 𝓡
   
  qR : 𝓡
   
  qO : 𝓡
   
  qM : 𝓡
   
  qC : 𝓡
deriving DecidableEq

Div in Init.Prelude

Finset.Ico in Mathlib.Order.Interval.Finset.Defs

List.Vector.get in Mathlib.Data.Vector.Defs

return none
</all_available_defs>

<all_available_lemmas>
Nat.sub_add_cancel in Init.Data.Nat.Basic
Nat.sub_zero in Init.Data.Nat.Basic
BitVec.ofNat_toNat in Init.Data.BitVec.Bootstrap
BitVec.setWidth_eq in Init.Data.BitVec.Lemmas
BitVec.toNat_setWidth in Init.Data.BitVec.Bootstrap
Nat.and_two_pow_sub_one_eq_mod in Init.Data.Nat.Bitwise.Lemmas
Nat.shiftRight_zero in Init.Data.Nat.Bitwise.Basic
Nat.add_sub_self_left in Init.Data.Nat.Basic
Nat.mul_two in Init.Data.Nat.Basic
Nat.pow_succ in Init.Data.Nat.Basic
Nat.succ_eq_add_one in Init.Data.Nat.Basic
Nat.two_pow_pos in Init.Data.Nat.Basic
Prod.ext_iff in Init.Ext

theorem one_le_two_pow_n (n : ℕ) : 1 ≤ 2 ^ n

@[simp]
theorem dcast_eq : dcast (Eq.refl a) b = b

theorem one_le_sub_consecutive_two_pow (n : ℕ): 1 ≤ 2^(n+1) - 2^n

theorem dcast_symm (ha : a = a') (hb : dcast ha b = b') : dcast (ha.symm) b' = b

theorem findIdxRev?_eq_some {cond} {as : Array α} (h : ∃ i, ∃ hi : i < as.size, cond as[i]) :
  ∃ k : Fin as.size, findIdxRev? cond as = some k

theorem Fin.sum_univ_odd_even {n : ℕ} {M : Type*} [AddCommMonoid M] (f : ℕ → M) :
    (∑ i : Fin (2 ^ n), f (2 * i)) + (∑ i : Fin (2 ^ n), f (2 * i + 1))
    = ∑ i: Fin (2 ^ (n+1)), f i

private lemma Fis_cover_B : B = Finset.univ.biUnion (Fi B i)

lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0)

@[simp] theorem add_zero {a : AssocNat} : a + 0 = a

theorem mapM_single (f : α → m β) (a : α) : List.mapM f [a] = return [← f a]

theorem towerEquiv_commutes_left (i j : ℕ) (h : i ≤ j) : ∀ r : ConcreteBTField i,
  (AlgebraTower.algebraMap i j h) ((towerEquiv i).ringEquiv r) =
  (towerEquiv j).ringEquiv ((AlgebraTower.algebraMap i j h) r)

lemma cast_mul (m n : ℕ) {x y : ConcreteBTField m} (h_eq : m = n) :
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) (x * y)) =
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) x) *
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) y)

theorem vappend_assoc {p : ℕ} (u : Fin m → α) (v : Fin n → α) (w : Fin p → α) :
    (vappend (vappend u v) w) = (vappend u (vappend v w)) ∘ Fin.cast (add_assoc m n p)

theorem BitVec.dcast_bitvec_eq {l r val : ℕ} (h_width_eq : l = r) :
    dcast h_width_eq (BitVec.ofNat l val) = BitVec.ofNat r val

protected lemma a_lemma_im_not_proud_of_OLD {v a : Fin n → F}
  (h_card : 2 ≤ Fintype.card F)
  :
  |(1 : ℚ) - ((1 : ℚ) + (1 : ℚ) / ((Fintype.card F : ℚ) - 1)) * ↑Δ₀(v, a) / ↑n

lemma num_eq_highBits_xor_lowBits {n: ℕ} (numLowBits: ℕ) :
  n = getHighBits numLowBits n ^^^ getLowBits numLowBits n

lemma not_outOfOrder_of_not_combined (h : ¬ E trace) : ¬ E_time trace state

theorem split_Z {k : ℕ} (h_pos : k > 0) :
    split h_pos (Z k) = (one (k:=k - 1), zero (k:=k - 1))

omit [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 in
lemma get_sDomain_basis (i : Fin r) (h_i : i < ℓ + R_rate) :
    ∀ (k : Fin (ℓ + R_rate - i)),
    (sDomain_basis 𝔽q β h_ℓ_add_R_rate
      i (by omega)) k = eval (β ⟨i + k.val, by omega⟩) (normalizedW 𝔽q β i)

lemma towerRingHomForwardMap_split_eq (k : ℕ) (h_pos : k > 0) (x : ConcreteBTField k) :
  let p := split (k:=k) (h:=h_pos) x
  towerRingHomForwardMap (k:=k) (x) =
    BinaryTower.join_via_add_smul (k:=k) (h_pos:=h_pos)
      (hi_btf := towerRingHomForwardMap (k:=k-1) (p.1))
      (lo_btf := towerRingHomForwardMap (k:=k-1) (p.2))

@[simp]
lemma widthDiv4_mul_4_eq_width : params.widthDiv4 * 4 = params.width

lemma testBit_false_eq_getBit_eq_0 (k n : Nat) :
  (n.testBit k = false) = ((Nat.getBit k n) = 0)

theorem intermediateNormVpoly_comp_qmap (i : Fin (ℓ))
    (k : Fin (ℓ - i - 1)) : -- corresponds to intermediateNormVpoly_comp

theorem nsmul_raw_succ (n : ℕ) (p : UniPoly Q) :
  nsmul_raw (n + 1) p = add_raw (nsmul_raw n p) p

@[simp]
theorem happend_empty {α : Fin m → Sort u} {β : Fin 0 → Sort u} (v : (i : Fin m) → α i) :
    happend v !h⟨β⟩[] = v

@[simp]
theorem fflatten_zero {A : Sort u} {F : A → Sort v} {n : Fin 0 → ℕ}
    {α : (i : Fin 0) → (j : Fin (n i)) → A}
    {v : (i : Fin 0) → (j : Fin (n i)) → F (α i j)} : fflatten v = !h[]

lemma rootMultiplicity_W (i : Fin r) (a : L) :
    rootMultiplicity a (W 𝔽q β i) = if a ∈ (U 𝔽q β i : Set L) then 1 else 0

lemma erase_odd_def {s : Finset ℕ} :
    erase_odd s = s.filter Even

lemma lin_shift_card [Field F] [Fintype F]
  :
  B.card = ({ x - v | x ∈ B} : Finset _).card

Polynomial.degree_sum_le in Mathlib.Algebra.Polynomial.Degree.Definitions

@[simp]
theorem vappend_left (u : Fin m → α) (v : Fin n → α) (i : Fin m) :
    vappend u v (castAdd n i) = u i

Nat.add_sub_cancel in Init.Data.Nat.Basic

@[simp]
theorem InternalData.rightSubtree_internal {α} {s_left s_right : Skeleton}
    (value : α) (left : InternalData α s_left) (right : InternalData α s_right) :
    (InternalData.internal value left right).rightSubtree = right

@[simp]
lemma dotProduct_cons [AddCommMonoid R] [Mul R] (a : R) (b : Vector R n) (c : R) (d : Vector R n) :
  dotProduct (cons a b) (cons c d) = a * c + dotProduct b d

@[grind _=_]
lemma weightedDegree_eq_natWeightedDegree {u v : ℕ} :
  f ≠ 0 → weightedDegree f u v = natWeightedDegree f u v

lemma eqRec_fun_eqRec_sort_eq_self {α : Sort*} {β : α → Sort u} {a a' : α}
    (h : a = a') (h' : β a = β a') (b : β a) :
  b = h ▸ h' ▸ b

lemma liftF_ne_zero_of_lt {i : ℕ} (h : i < n) : liftF f' i ≠ 0 ↔ f' ⟨i, h⟩ ≠ 0

theorem support_C_mul_le (p : MvPolynomial σ R) (r : R) : (C r * p).support ⊆ p.support

theorem prime_7 : Nat.Prime 7

have h_pb'_dim : bCast.dim = 2 := by
      dsimp [bCast]
      rw [PowerBasis.dim_of_eq_rec (r1:=r1) (r:=r) (h_r:=h_r) (b:=b)]
      exact h_pb_dim

Nat.pow_lt_pow_right in Init.Data.Nat.Lemmas

lemma zero_is_0 {k : ℕ} : (zero (k:=k)) = (0 : ConcreteBTField k)

@[simp]
theorem cast_dir_idx {hn} (hSpec : pSpec₁.cast hn = pSpec₂) {i : Fin n₁} :
    pSpec₂.dir (Fin.cast hn i) = pSpec₁.dir i

@[simp]
theorem toNat_succ (n : ChurchNat ℕ) : toNat (succ n) = n.toNat.succ

theorem append_getLast_dropLast {α : Type u} (l : List α) (h : l ≠ []) :
  l.dropLast ++ [l.getLast h] = l

theorem append_completeness (R₁ : Reduction oSpec Stmt₁ Wit₁ Stmt₂ Wit₂ pSpec₁)
    (R₂ : Reduction oSpec Stmt₂ Wit₂ Stmt₃ Wit₃ pSpec₂)
    {completenessError₁ completenessError₂ : ℝ≥0}
    (h₁ : R₁.completeness init impl rel₁ rel₂ completenessError₁)
    (h₂ : R₂.completeness init impl rel₂ rel₃ completenessError₂) :
      (R₁.append R₂).completeness init impl
        rel₁ rel₃ (completenessError₁ + completenessError₂)

private lemma errors_are_roots_of_E {i : Fin n}
  (h : f i ≠ p.eval (ωs i)) : (E ωs f p e).eval (ωs i) = 0

lemma out_of_dom_smpl_1
  {δ l : ℝ≥0} {s : ℕ} {f : ι → F} {degree : ℕ} {φ : ι ↪ F}
  (C : Set (ι → F)) (hC : C = code φ degree)
  (h_decodable : listDecodable C δ l)
  (h_nonempty : Nonempty (domainComplement φ)) :
  listDecodingCollisionProbability φ f δ s degree h_nonempty ≤
    ((l * (l-1) / 2)) * ((degree - 1) / (Fintype.card F - Fintype.card ι))^s

theorem induction_tail {n : ℕ} {motive : Fin (n + 2) → Sort*} {zero : motive 0}
    {succ : ∀ i : Fin (n + 1), motive i.castSucc → motive i.succ} {i : Fin (n + 1)} :
      induction (motive := motive) zero succ i.succ =
        induction (motive := Fin.tail motive) (succ 0 zero) (fun j x => succ j.succ x) i

theorem cast_injective : Function.Injective (MessageIdx.cast hn hSpec)

theorem stir_rbr_soundness
    [SelectableType F] {s : ℕ}
    {P : Params ι F} {φ : (i : Fin (M + 1)) → (ι i ↪ F)}
    [h_nonempty : ∀ i : Fin (M + 1), Nonempty (ι i)]
    {hParams : ParamConditions ι P} {Dist : Distances M}
    {Codes : CodeParams ι P Dist}
    (h_not_code : ∀ f₀ : (ι 0) → F, f₀ ∉ (Codes.C 0))
    (hδ₀Le : ∀ f₀ : (ι 0) → F, Dist.δ 0 ≤ (δᵣ(f₀, (Codes.C 0)) : ℝ) ∧
      Dist.δ 0 < (1 - Bstar (rate (code (P.φ 0) P.deg))))
    (hδᵢ : ∀ {j : Fin (M + 1)}, j ≠ 0 →
        Dist.δ j < (1 - rate (code (P.φ j) (degree ι P j))
          - 1 / Fintype.card (ι j) : ℝ) ∧
        Dist.δ j < (1 - Bstar (rate (code (P.φ j) (degree ι P j)))))
    (ε_fold : ℝ≥0) (ε_out : Fin M → ℝ≥0) (ε_shift : Fin M → ℝ≥0) (ε_fin : ℝ≥0) :
    ∃ n : ℕ,
    -- There exists an `n`-message vector IOPP,
    ∃ vPSpec : ProtocolSpec.VectorSpec n,
    -- such that there are `2 * M + 2` challenges from the verifier to the prover,
    Fintype.card (vPSpec.ChallengeIdx) = 2 * M + 2 ∧
    -- ∃ vector IOPP π with the aforementioned `vPSpec`, and for
    -- `Statement = Unit, Witness = Unit, OracleStatement(ι₀, F)` such that
    ∃ π : VectorIOP Unit (OracleStatement (ι 0) F) Unit vPSpec F,
    let ε_rbr : vPSpec.ChallengeIdx → ℝ≥0

lemma BTField.cast_mul (m n : ℕ) {x y : BTField m} (h_eq : m = n) :
  (cast (by exact BTField.cast_BTField_eq m n h_eq) (x * y)) =
  (cast (by exact BTField.cast_BTField_eq m n h_eq) x) *
  (cast (by exact BTField.cast_BTField_eq m n h_eq) y)

theorem rbrKnowledgeSoundness_implies_knowledgeSoundness
    (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut))
    (verifier : Verifier oSpec StmtIn StmtOut pSpec)
    (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) :
      rbrKnowledgeSoundness init impl relIn relOut verifier rbrKnowledgeError →
        knowledgeSoundness init impl relIn relOut verifier (∑ i, rbrKnowledgeError i)

lemma towerRingHomForwardMap_backwardMap_eq (k : ℕ) (x : BTField k) :
  towerRingHomForwardMap (k:=k) (towerRingHomBackwardMap (k:=k) x) = x

@[simp]
lemma foldr'_zero {α : Type u} (f : (i : Fin 0) → α → α) (x : α) :
    foldr' 0 f x = x

theorem snoc_ne_zero_of_left (h : s ≠ 0) : snoc s y ≠ 0

@[simp]
theorem oracleReduction_completeness (h : init.neverFails) :
    (oracleReduction oSpec Statement OStatement pred).perfectCompleteness init impl
    (toRelInput pred hPred) Set.univ

lemma concrete_mul_zero
  (prevBTFieldProps : ConcreteBTFieldProps (k := k - 1))
  (a : ConcreteBTField k) : concrete_mul a (zero (k:=k)) = zero (k:=k)

theorem liftContext_runWithLog
    {lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
    {outerStmtIn : OuterStmtIn} {outerWitIn : OuterWitIn}
    {P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec} :
      (P.liftContext lens).runWithLog outerStmtIn outerWitIn
      = do
        let ⟨⟨fullTranscript, innerCtxOut⟩, queryLog⟩ ←
          P.runWithLog.uncurry (lens.proj (outerStmtIn, outerWitIn))
        return ⟨⟨fullTranscript, lens.lift (outerStmtIn, outerWitIn) innerCtxOut⟩, queryLog⟩

@[simp]
protected lemma elocPoly_zero : ElocPoly 0 ωs f p = 1

private lemma comp_x_square_coeff_pos_deg {f : Polynomial F} {n : ℕ} (h : 0 < f.degree) :
  (f.comp (X * X)).coeff n = if Even n then f.coeff (n / 2) else 0

@[simp]
theorem dflatten_zero {n : Fin 0 → ℕ} {motive : (k : Fin (vsum n)) → Sort*}
    {v : (i : Fin 0) → (j : Fin (n i)) → motive (embedSum i j)} :
    dflatten (motive := motive) v = fun k => Fin.elim0 k

@[simp]
lemma Rhs_zero_eq_neg : Rhs 0 ωs f i = -f i

theorem singleEqPolynomial_zeroOne_C (r : Fin 2) (x : Fin 2) :
    (singleEqPolynomial (r : R) (C x) : MvPolynomial σ R) = if x = r then 1 else 0

theorem neg_add_cancel [LawfulBEq R] (p : UniPoly R) : -p + p = 0

theorem minDist [Field F] [DecidableEq F] (inj : Function.Injective α) [NeZero n] (h : n ≤ m) :
  minDist ((ReedSolomon.code ⟨α, inj⟩ n) : Set (Fin m → F)) = m - n + 1

theorem append_rbrKnowledgeSoundness (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁)
    (V₂ : OracleVerifier oSpec Stmt₂ OStmt₂ Stmt₃ OStmt₃ pSpec₂)
    {rbrKnowledgeError₁ : pSpec₁.ChallengeIdx → ℝ≥0}
    {rbrKnowledgeError₂ : pSpec₂.ChallengeIdx → ℝ≥0}
    (h₁ : V₁.rbrKnowledgeSoundness init impl rel₁ rel₂ rbrKnowledgeError₁)
    (h₂ : V₂.rbrKnowledgeSoundness init impl rel₂ rel₃ rbrKnowledgeError₂) :
      (V₁.append V₂).rbrKnowledgeSoundness init impl rel₁ rel₃
        (Sum.elim rbrKnowledgeError₁ rbrKnowledgeError₂ ∘ ChallengeIdx.sumEquiv.symm)

Nat.lt_trans in Init.Prelude

Nat.sub_mul in Init.Data.Nat.Basic

lemma oracle_block_k_next_le (i : Fin (ℓ + 1)) (j : Fin (toOutCodewordsCount ℓ ϑ i))
    (hj : j.val + 1 < toOutCodewordsCount ℓ ϑ i) : j.val * ϑ + ϑ ≤ i

theorem fullOracleVerifier_rbrKnowledgeSoundness :
  (fullOracleVerifier 𝔽q β γ_repetitions (ϑ:=ϑ)
    (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).rbrKnowledgeSoundness init impl
    (relIn := roundRelation (mp := BBF_SumcheckMultiplierParam) 𝔽q β (ϑ:=ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑) 0)
    (relOut := acceptRejectOracleRel)
    (rbrKnowledgeError := fullRbrKnowledgeError 𝔽q β γ_repetitions (ϑ:=ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate))

lemma mem_support_coeff_finSuccEquivNth {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ ((finSuccEquivNth R p f).coeff i).support ↔ x.insertNth p i ∈ f.support

lemma extract_start_zero_eq_take {n : ℕ} {α : Fin n → Sort*} (stop : ℕ) (h : stop ≤ n)
    (v : (i : Fin n) → α i) : extract 0 stop (Nat.zero_le _) h v = take stop h v

@[simp]
theorem OracleReduction.id_perfectCompleteness
    {rel : Set ((StmtIn × ∀ i, OStmtIn i) × WitIn)}
    (hInit : init.neverFails) :
    (OracleReduction.id : OracleReduction oSpec _ _ _ _ _ _ _).perfectCompleteness
      init impl rel rel

lemma add_two_pow_of_getBit_eq_zero_lt_two_pow {n m i : ℕ} (h_n: n < 2^m) (h_i: i < m)
  (h_getBit_at_i_eq_zero: getBit i n = 0) :
  n + 2^i < 2^m

theorem getBit_repr {ℓ : Nat} : ∀ j, j < 2^ℓ →
  j = ∑ k ∈ Finset.Icc 0 (ℓ-1), (getBit k j) * 2^k

theorem eq_zero_or_eq_one {a : ConcreteBTField 0} : a = zero ∨ a = one

theorem toNat_ofNat (n : ℕ) : toNat (ofNat n) = n

lemma schwartz_zippel' {p : MvPolynomial σ R} (hp : p ≠ 0) (S : σ → Finset R) :
    #{x ∈ Finset.pi p.vars S | eval (extendDomain x) p = 0} / ∏ i ∈ p.vars, (#(S i) : ℚ≥0)
      ≤ ∑ i ∈ p.vars, (p.degreeOf i / #(S i) : ℚ≥0)

theorem liftContext_knowledgeSoundness [Inhabited InnerStmtOut] [Inhabited InnerWitIn]
    {outerRelIn : Set (OuterStmtIn × OuterWitIn)} {outerRelOut : Set (OuterStmtOut × OuterWitOut)}
    {innerRelIn : Set (InnerStmtIn × InnerWitIn)} {innerRelOut : Set (InnerStmtOut × InnerWitOut)}
    {knowledgeError : ℝ≥0}
    {stmtLens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut}
    {witLens : Witness.InvLens OuterStmtIn OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
    (V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
    [lensKS : Extractor.Lens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut
      (V.compatStatement stmtLens) (fun _ _ => True) ⟨stmtLens, witLens⟩]
    (h : V.knowledgeSoundness init impl innerRelIn innerRelOut knowledgeError) :
      (V.liftContext stmtLens).knowledgeSoundness init impl outerRelIn outerRelOut
        knowledgeError

lemma oodSampling_crs_eq_rs
    {f : ι → F} {m s : ℕ} {φ : ι ↪ F} [Smooth φ]
    (l δ : ℝ≥0) (hδLe : δ ≤ 1)
    {C : Set (ι → F)} (hcode : C = smoothCode φ m ∧ listDecodable C δ l) :
    Pr_{ let rs ←$ᵖ (Fin s → F) }[ (∃ σ : Fin s → F,
                        let w : Fin s → MvPolynomial (Fin (m + 1)) F :=
                          fun i =>
                            let ri := rs i
                            let rVec := fun j : Fin m => ri ^ (2^(j : ℕ))
                            MvPolynomial.X (Fin.last m) * rename Fin.castSucc (eqPolynomial rVec)
                        let multiCRSCode := multiConstrainedCode φ m s w σ
                        ∃ u u' : ι → F, u ≠ u' ∧
                          u ∈ relHammingBall multiCRSCode f δ ∧
                          u' ∈ relHammingBall multiCRSCode f δ)]
    =
    Pr_{ let rs ←$ᵖ (Fin s → F) }[ (∃ u u' : smoothCode φ m,
                        u.val ≠ u'.val ∧
                        u.val ∈ relHammingBall C f δ ∧
                        u'.val ∈ relHammingBall C f δ ∧
                        ∀ i : Fin s,
                          let ri := rs i
                          let rVec := fun j : Fin m => ri ^ (2^(j : ℕ))
                          (mVdecode u).eval (rVec) = (mVdecode u').eval (rVec))]

@[simp]
theorem cast_id :
    OracleProver.cast rfl rfl =
      (id : OracleProver oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec₁ → _)

theorem oracleReduction_perfectCompleteness (hInit : init.neverFails) :
    (oracleReduction R n deg D oSpec i).perfectCompleteness init impl
      (relationRound R n deg D i.castSucc) (relationRound R n deg D i.succ)

@[simp]
lemma OracleVerifier.id_rbrKnowledgeSoundness
    {rel : Set ((Statement × ∀ i, OStatement i) × Witness)} :
    (OracleVerifier.id : OracleVerifier oSpec Statement OStatement _ _ _).rbrKnowledgeSoundness
      init impl rel rel 0

lemma aeval_eq' {A : Type w} [CommSemiring A] [Algebra R A] (f : P →ₐ[R] A) (p : P) :
    f p = aeval (f X) p

theorem PowerBasis_cast_dest_eq (k n m : ℕ) (h_k_le_n : k ≤ n)
  (h_k_le_m : k ≤ m) (h_eq : m = n) :
  letI instLeftAlgebra := ConcreteBTFieldAlgebra (l:=k) (r:=m) (h_le:=h_k_le_m)
  letI instRightAlgebra := ConcreteBTFieldAlgebra (l:=k) (r:=n) (h_le:=h_k_le_n)
  @PowerBasis (ConcreteBTField k) (ConcreteBTField m) _ _ instLeftAlgebra =
  @PowerBasis (ConcreteBTField k) (ConcreteBTField n) _ _ instRightAlgebra

theorem correlatedAgreement_affine_spaces {k : ℕ} [NeZero k] {u : Fin (k + 1) → ι → F}
  {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} (hδ : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
  (hproximity :
    Pr_{let y ← $ᵖ (u 0 +ᵥ affineSpan F (Finset.univ.image (Fin.tail u)).toSet)}[
        Code.relHammingDistToCode (ι := ι) (F := F) y (ReedSolomon.code domain deg) ≤ δ
    ] > errorBound δ deg domain) :
  correlatedAgreement (ReedSolomon.code domain deg) δ u

theorem add_zero {n : ℕ} (a : CNat (n + 1)) : a + 0 = a

@[simp]
theorem reduction_completeness (h : init.neverFails)
    (hRel : ∀ stmtIn witIn, (stmtIn, witIn) ∈ relIn ↔
      (mapStmt stmtIn, mapWit stmtIn witIn) ∈ relOut) :
    (reduction oSpec mapStmt mapWit).perfectCompleteness init impl relIn relOut

lemma aeval_eq' {A : Type y} [CommSemiring A] [Algebra R A] {F : Type z} [FunEquiv F σ A]
    (f : P →ₐ[R] A) (p : P) : f p = aeval (fun s => f (X s) : F) p

@[simp]
theorem append_cast_left {n m : ℕ} {pSpec : ProtocolSpec n} {pSpec' : ProtocolSpec m} (n' : ℕ)
    (h : n + m = n' + m) :
      dcast h (pSpec ++ₚ pSpec') = (dcast (Nat.add_right_cancel h) pSpec) ++ₚ pSpec'

theorem rightpad_eq_rightpad_append_replicate_of_ge
  (l : List α) (m n : Nat) (h : n ≤ m) :
    rightpad m unit l = rightpad n unit l ++ replicate (m - max n l.length) unit

theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀ (j : Fin (2  ^ (r - l))),
  multilinearBasis (l:=l) (r:=r) (h_le:=h_le) j =
    (Finset.univ : Finset (Fin (r - l))).prod (fun i =>
      (binaryAlgebraTower (l:=l + i + 1) (r:=r) (h_le:=by omega)).algebraMap (
        (𝕏 (l + i)) ^ (Nat.getBit i j)))

@[simp]
theorem list_nonempty (k : ℕ) : (list k).1 ≠ []

lemma getBit_of_lt_two_pow {n: ℕ} (a: Fin (2^n)) (k: ℕ) :
  getBit k a = if k < n then getBit k a else 0

@[simp]
lemma eval₂AlgHom_apply {A B : Type*} [CommSemiring A] [CommSemiring B] [MvPolynomialLike σ A P]
    [Algebra R A] [IsScalarTower R A P] [Algebra R B]
    (f : A →ₐ[R] B) (g : σ → B) (p : P) :
    (eval₂AlgHom f g) p = eval₂ f g p

@[simp]
lemma natDegree_truncate [φ : NeZero n] : (truncate p n).natDegree < n

@[csimp]
theorem vappend_eq_append : @vappend = @append

theorem oracleVerifier_rbrKnowledgeSoundness [Fintype R] :
    (oracleVerifier R deg D oSpec).rbrKnowledgeSoundness init impl
    (inputRelation R deg D) (outputRelation R deg) (fun _ => (deg : ℝ≥0) / (Fintype.card R))

theorem pow_zero {a : CNat 50} : a ^ 0 = 1

lemma addSalt_Challenge (i : pSpec.ChallengeIdx) :
    (pSpec.addSalt Salt).Challenge i = pSpec.Challenge i

Nat.zero_add in Init.Data.Nat.Basic

omit h_β₀_eq_1 in
theorem sDomainFin_bijective (i : Fin r) (h_i : i < ℓ + R_rate)
: Function.Bijective
  (sDomainFinEquiv 𝔽q β h_ℓ_add_R_rate i h_i)

@[simp]
theorem reduction_completeness (h : init.neverFails) :
    (reduction oSpec Statement Witness).perfectCompleteness init impl relIn (toRelOut relIn)
</all_available_lemmas>

<local_ctx>
import ArkLib.Data.Classes.DCast

import ArkLib.Data.FieldTheory.BinaryField.Tower.Basic

namespace ConcreteBinaryTower

open Polynomial

def ConcreteBTField : ℕ → Type := fun k => BitVec (2 ^ k)

section BitVecDCast

instance BitVec.instDCast : DCast Nat BitVec where
  dcast h := BitVec.cast h
  dcast_id := by admit /- proof elided -/

end BitVecDCast

section ConversionUtils

def fromNat {k : ℕ} (n : Nat) : ConcreteBTField k :=
  BitVec.ofNat (2 ^ k) n

instance ConcreteBTField.instDCast_local : DCast ℕ ConcreteBTField where
  dcast h_k_eq term_k1 := BitVec.cast (congrArg (fun n => 2 ^ n) h_k_eq) term_k1
  dcast_id := by admit /- proof elided -/

end ConversionUtils

section NumericLemmas

end NumericLemmas

section FieldOperationsAndInstances

def split {k : ℕ} (h : k > 0) (x : ConcreteBTField k) :
    ConcreteBTField (k - 1) × ConcreteBTField (k - 1) :=
  let lo_bits : BitVec (2 ^ (k - 1) - 1 - 0 + 1) :=
    BitVec.extractLsb (hi := 2 ^ (k - 1) - 1) (lo := 0) x
  let hi_bits : BitVec (2 ^ k - 1 - 2 ^ (k - 1) + 1) :=
    BitVec.extractLsb (hi := 2 ^ k - 1) (lo := 2 ^ (k - 1)) x
  have h_lo : 2 ^ (k - 1) - 1 - 0 + 1 = 2 ^ (k - 1) := by admit /- proof elided -/
</local_ctx>

<target_theorem>
theorem split_bitvec_eq_iff_fromNat {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k)
  (hi_btf lo_btf : ConcreteBTField (k - 1)) :
  split h_pos x = (hi_btf, lo_btf) ↔
  (hi_btf = fromNat (k:=k - 1) (x.toNat >>> 2 ^ (k - 1)) ∧
  lo_btf = fromNat (k:=k - 1) (x.toNat &&& (2 ^ (2 ^ (k - 1)) - 1))) :=
</target_theorem>

