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>
Vector in Init.Data.Vector.Basic
Fin in Init.Prelude
String in Init.Prelude
Unit in Init.Prelude
List in Init.Prelude
Field in Mathlib.Algebra.Field.Defs
Bool in Init.Prelude
DecidableEq in Init.Prelude
FinEnum in Mathlib.Data.FinEnum
Hashable in Init.Prelude
Sum in Init.Core
Sum.inl in Init.Core
Sum.inr in Init.Core
Sum.elim in Init.Data.Sum.Basic
Empty in Init.Prelude
Empty.elim in Init.Core
id in Init.Prelude
Nat in Init.Prelude
Repr in Init.Data.Repr
Inhabited in Init.Prelude
Lean.ToExpr in Lean.ToExpr
Nat.max in Init.Data.Nat.Basic
Nat.min in Init.Data.Nat.Basic
BitVec in Init.Prelude
BitVec.ofBool in Init.Data.BitVec.Basic
BitVec.ofNat in Init.Prelude
BitVec.signExtend in Init.Data.BitVec.Basic
BitVec.adcb in Init.Data.BitVec.Bitblast
Prod in Init.Prelude
BitVec.carry in Init.Data.BitVec.Bitblast
Bool.atLeastTwo in Init.Data.BitVec.Bitblast

syntax "min" : MLIR.Pretty.uniform_op

macro_rules
  | `(mlir_op| $res:mlir_op_operand = const ($x)
      $[: $outer_type]? ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _)
      `(mlir_op| $res:mlir_op_operand = "const"()
          {val = $x:num : $outer_type} : ($outer_type) -> ($outer_type) )

macro_rules
  | `(mlir_op| $res:mlir_op_operand = li ($x)
     $[: $outer_type]?  ) => do
      let outer_type ← outer_type.getDM `(mlir_type| _ )
      `(mlir_op| $res:mlir_op_operand = "li"()
          {imm = $x:num : $outer_type } : ($outer_type) -> ($outer_type))

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithImmediate $reg1 , $x : $t)  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {imm = $x:num : $t} : ($t) -> ($t) )

macro_rules
| `(mlir_op| $res:mlir_op_operand = $op1:MLIR.Pretty.RV.opWithShamt $reg1 , $x  : $t )  => do
    let some opName := MLIR.EDSL.Pretty.extractOpName op1.raw
      | Macro.throwUnsupported
    `(mlir_op| $res:mlir_op_operand = $opName ($reg1) {shamt = $x:num : $t}  : ($t) -> ($t) )

inductive Circuit (α : Type u) : Type u
  | tru : Circuit α
  | fals : Circuit α
   
  | var : (positive: Bool) → α → Circuit α
  | and : Circuit α → Circuit α → Circuit α
  | or : Circuit α → Circuit α → Circuit α
  | xor : Circuit α → Circuit α → Circuit α
deriving Repr, DecidableEq

structure FSM (arity : Type) : Type 1 where
   
  ( α  : Type )
  [ i : FinEnum α ]
  [ h : Hashable α ]
  [ dec_eq : DecidableEq α ]
   
  ( initCarry : α → Bool )
   
  outputCirc : Circuit (α ⊕ arity)
  nextStateCirc : α → Circuit (α ⊕ arity)

def Var (Γ : Context Ty) (ty : Ty) : Type := { v : VarName // Γ.hasType v ty }

def composeBinaryAux'
    (p : FSM Bool)
    (qtrue : FSM α)
    (qfalse : FSM α) :
    FSM α :=
  p.compose (α)
    (λ _ => α)
    (λ _ i => i)
    (λ b => match b with
      | true => qtrue
      | false => qfalse)

def compose [FinEnum arity] [DecidableEq arity] [Hashable arity]
    (new_arity : Type)        
    (q_arity : arity → Type)  
    (vars : ∀ (a : arity), q_arity a → new_arity)
    
    
    (q : ∀ (a : arity), FSM (q_arity a)) : 
    FSM new_arity :=
  { α := p.α ⊕ (Σ a, (q a).α),
    i := by admit /- proof elided -/

def xor : FSM Bool :=
  { α := Empty,
    initCarry := Empty.elim,
    outputCirc := Circuit.var true (inr true) ^^^ Circuit.var true (inr false),
    nextStateCirc := Empty.elim
  }

def composeUnaryAux
    (p : FSM Unit)
    (q : FSM arity) :
    FSM arity :=
  p.compose
    arity
    _
    (λ _ => id)
    (λ _ => q)

def ls (b : Bool) : FSM Unit :=
  { α := Unit,
    initCarry := fun _ => b,
    nextStateCirc := fun () => Circuit.var true (inr ()),
    outputCirc := Circuit.var true (inl ())
  }

def latchImmediate (initVal : Bool) : FSM Bool where
  α := Unit
  initCarry := fun _ => initVal
  outputCirc :=
    let xval := Circuit.var true (inr false)
    let control := Circuit.var true (inr true)
    let state := Circuit.var true (inl ())
    Circuit.ite control xval state
  nextStateCirc := fun () =>
    let xval := Circuit.var true (inr false)
    let control := Circuit.var true (inr true)
    let state := Circuit.var true (inl ())
    Circuit.ite control xval state

def ite (cond t f : Circuit α) : Circuit α :=
  (cond &&& t) ||| (~~~ cond &&& f)

structure TermFSM (wcard tcard bcard ncard icard pcard : Nat) (t : Nondep.Term) where
  toFsmZext : FSM (StateSpace wcard tcard bcard ncard icard pcard)
  width : NatFSM wcard tcard bcard ncard icard pcard t.width

structure NatFSM (wcard tcard bcard ncard icard pcard : Nat) (v : Nondep.WidthExpr) where
  toFsm : FSM (StateSpace wcard tcard bcard ncard icard pcard)

inductive StateSpace (wcard tcard bcard ncard icard pcard : Nat)
| widthVar (v : Fin wcard)
| termVar (v : Fin tcard)
| predVar (v : Fin pcard)
| boolVar (v : Fin bcard)
deriving DecidableEq, Repr, Hashable

inductive Term
| ofNat (w : WidthExpr) (n : Nat) : Term
| var (v : Nat) (w : WidthExpr) : Term
| add (w : WidthExpr) (a b : Term) : Term
| zext (a : Term) (wnew : WidthExpr) : Term
| setWidth (a : Term) (wnew : WidthExpr) : Term
| sext (a : Term) (wnew : WidthExpr) : Term
| bor (w : WidthExpr) (a b : Term) : Term
| band (w : WidthExpr) (a b : Term) : Term
| bxor (w : WidthExpr) (a b : Term) : Term
| bnot (w : WidthExpr)  (a : Term) : Term
| boolVar (v : Nat) : Term
| boolConst (b : Bool) : Term
| shiftl (w : WidthExpr) (a : Term) (k : Nat) : Term
| bvOfBool (b : Term) : Term
| binWidthRel (k : WidthBinaryRelationKind) (wa wb : WidthExpr) : Term
| binRel (k : BinaryRelationKind) (w : WidthExpr)
    (a : Term) (b : Term) : Term
| or (p1 p2 : Term) : Term
| and (p1 p2 : Term) : Term
| pvar (v : Nat) : Term
| boolBinRel (k : BoolBinaryRelationKind)
    (a b : Term) : Term
deriving DecidableEq, Inhabited, Repr, Lean.ToExpr

inductive WidthExpr where
| const : Nat → WidthExpr
| var : Nat → WidthExpr
| max : WidthExpr → WidthExpr → WidthExpr
| min : WidthExpr → WidthExpr → WidthExpr
| addK : WidthExpr → Nat → WidthExpr
| kadd : Nat → WidthExpr → WidthExpr
deriving Inhabited, Repr, Hashable, DecidableEq, Lean.ToExpr

def Term.width (t : Term) : WidthExpr :=
  match t with

| .ofNat w _n => w
  | .var _v w => w
  | .add w _a _b => w
  | .zext _a wnew => wnew
  | .setWidth _a wnew => wnew
  | .sext _a wnew => wnew
  | .bor w _a _b => w
  | .band w _a _b => w
  | .bxor w _a _b => w
  | .bnot w _a => w
  | .boolVar _v => WidthExpr.const 1 
  | .boolConst _b => WidthExpr.const 1
  | .shiftl w _a _k => w
  | .bvOfBool _b => WidthExpr.const 1
  | binWidthRel _k wa wb => WidthExpr.const 0
  | binRel _k w _a _b => w
  | or _p1 _p2 => WidthExpr.const 0
  | and _p1 _p2 => WidthExpr.const 0
  | pvar _v => WidthExpr.const 0
  | boolBinRel _k _a _b => WidthExpr.const 0

inductive WidthExpr where
| const : Nat → WidthExpr
| var : Nat → WidthExpr
| max : WidthExpr → WidthExpr → WidthExpr
| min : WidthExpr → WidthExpr → WidthExpr
| addK : WidthExpr → Nat → WidthExpr
| kadd : (k : Nat) → (v : WidthExpr) → WidthExpr
deriving Inhabited, Repr, Hashable, DecidableEq, Lean.ToExpr

structure HNatFSMToBitstream {wcard : Nat} {v : WidthExpr wcard} {tcard : Nat} {bcard : Nat} {pcard : Nat}
   (fsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep v)) : Prop where
  heq :
    ∀ (wenv : Fin wcard → Nat)
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream),
    (henv : HWidthEnv fsmEnv wenv) →
      fsm.toFsm.eval fsmEnv =
      BitStream.ofNatUnary (v.toNat wenv)

def WidthExpr.toNat (e : WidthExpr wcard) (env : WidthExpr.Env wcard) : Nat :=
  match e with
  | .const n => n
  | .var v => env v
  | .min v w => Nat.min (v.toNat env) (w.toNat env)
  | .max v w => Nat.max (v.toNat env) (w.toNat env)
  | .addK v k => v.toNat env + k
  | .kadd k v => k + v.toNat env

inductive WidthExpr (wcard : Nat) : Type
| const (n : Nat) :  WidthExpr wcard
| var : (v : Fin wcard) → WidthExpr wcard
| min : (v w : WidthExpr wcard) → WidthExpr wcard
| max : (v w : WidthExpr wcard) → WidthExpr wcard
| addK : (v : WidthExpr wcard) → (k : Nat) → WidthExpr wcard
| kadd : (k : Nat) → (v : WidthExpr wcard) → WidthExpr wcard

abbrev WidthExpr.Env (wcard : Nat) : Type :=
  Fin wcard → Nat

structure HWidthEnv {wcard tcard : Nat}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (wenv : Fin wcard → Nat) : Prop where
    heq_width : ∀ (v : Fin wcard),
      fsmEnv (StateSpace.widthVar v) = BitStream.ofNatUnary (wenv v)

structure HPredicateEnv {wcard tcard bcard ncard icard pcard : Nat}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (penv : Fin pcard → Prop) : Prop where
    heq_width : ∀ (v : Fin pcard),
      fsmEnv (StateSpace.predVar v) = BitStream.ofProp (penv v)

def BitStream : Type := Nat → Bool

abbrev ofNatUnary (n : Nat) : BitStream :=
  fun i => decide (i < n)

structure HPredFSMToBitStream {pcard : Nat}
  {tctx : Term.Ctx wcard tcard}
  {p : Term bcard ncard icard pcard tctx .prop}
  (fsm : TermFSM wcard tcard bcard ncard icard pcard
    (.ofDepTerm p)) : Prop where
  heq :
    ∀ {wenv : WidthExpr.Env wcard}
      (benv : Term.BoolEnv bcard)
      (nenv : Term.NatEnv ncard)
      (ienv : Term.IntEnv icard)
      (penv : Predicate.Env pcard) (tenv : tctx.Env wenv)
      (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream),
      (htenv : HTermEnv fsmEnv tenv benv) →
      (hpenv : HPredicateEnv fsmEnv penv) →
        p.toBV benv nenv ienv penv tenv  ↔ (fsm.toFsmZext.eval fsmEnv = .negOne)

abbrev Term.Ctx (wcard : Nat) (tcard : Nat) : Type :=
  Fin tcard → WidthExpr wcard

def Term.BoolEnv (bcard : Nat) : Type := Fin bcard → Bool

def Term.IntEnv (icard : Nat) : Type := Fin icard → Nat

structure HTermFSMToBitStream {w : WidthExpr wcard}
  {tctx : Term.Ctx wcard tcard}
  {t : Term bcard ncard icard pcard tctx (.bv w)}
  (fsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm t)) : Prop where
  heq :
    ∀ {wenv : WidthExpr.Env wcard}
      (benv : Term.BoolEnv bcard)
      (nenv : Term.NatEnv ncard)
      (ienv : Term.IntEnv icard)
      (penv : Predicate.Env pcard) (tenv : tctx.Env wenv)
      (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream),
      (henv : HTermEnv fsmEnv tenv benv) →
        fsm.toFsmZext.eval fsmEnv =
        BitStream.ofBitVecZext (t.toBV benv nenv ienv penv tenv)

def Predicate.Env (pcard : Nat) : Type :=
  Fin pcard → Prop

inductive TermKind (wcard : Nat) : Type
| bool
| bv (w : WidthExpr wcard)  : TermKind wcard
| prop
| nat
| int

structure HTermEnv {wcard tcard bcard : Nat}
    {wenv : Fin wcard → Nat} {tctx : Term.Ctx wcard tcard}
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (tenv : tctx.Env wenv)
    (benv : Term.BoolEnv bcard) : Prop
  extends HWidthEnv fsmEnv wenv where
    heq_term : ∀ (v : Fin tcard),
      fsmEnv (StateSpace.termVar v) = BitStream.ofBitVecZext (tenv v)
    heq_bool : ∀ (v : Fin bcard),
      fsmEnv (StateSpace.boolVar v) = BitStream.ofBool (benv v)

noncomputable def BitStream.ofBool (b : Bool) : BitStream := fun _i => b

abbrev Term.Ctx.Env
  (tctx : Term.Ctx wcard tcard)
  (wenv : WidthExpr.Env wcard) :=
  (v : Fin tcard) → BitVec ((tctx v).toNat wenv)

abbrev ofBitVecZext {w} (x : BitVec w) : BitStream :=
  fun i => x.getLsbD i

def Term.NatEnv (ncard : Nat) : Type := Fin ncard → Nat

def Term.toBV {wenv : WidthExpr.Env wcard}
    {tctx : Term.Ctx wcard tcard}
    (benv : Term.BoolEnv bcard)
    (nenv : Term.NatEnv ncard)
    (ienv : Term.IntEnv icard)
    (penv : Predicate.Env pcard)
    (tenv : tctx.Env wenv)
    (t : Term bcard ncard icard pcard tctx k) : k.denote wenv :=
match t with
| .ofNat w n => BitVec.ofNat (w.toNat wenv) n
| .boolConst b => b
| .var v => tenv.get v.1 v.2
| .add (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a + b
| .zext a v => (a.toBV benv nenv ienv penv tenv).zeroExtend (v.toNat wenv)
| .setWidth a v => (a.toBV benv nenv ienv penv tenv).zeroExtend (v.toNat wenv)
| .sext a v => (a.toBV benv nenv ienv penv tenv).signExtend (v.toNat wenv)
| .bor a b (w := w) =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a ||| b
| .band (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a &&& b
| .bxor (w := w) a b =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    let b : BitVec (w.toNat wenv) := (b.toBV benv nenv ienv penv tenv)
    a ^^^ b
| .bnot (w := w) a =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    ~~~ a
| .boolVar v => benv v
| .shiftl (w := w) a k =>
    let a : BitVec (w.toNat wenv) := (a.toBV benv nenv ienv penv tenv)
    a <<< k
| .bvOfBool b => BitVec.ofBool (b.toBV benv nenv ienv penv tenv)

| .binWidthRel rel wa wb =>
  match rel with
  | .eq => wa.toNat wenv = wb.toNat wenv
  | .le => wa.toNat wenv ≤ wb.toNat wenv
| .binRel rel _w a b =>
  match rel with
  | .eq => a.toBV benv nenv ienv penv tenv = b.toBV benv nenv ienv penv tenv
  | .ne => a.toBV benv nenv ienv penv tenv ≠ b.toBV benv nenv ienv penv tenv
  | .ult => (a.toBV benv nenv ienv penv tenv).ult (b.toBV benv nenv ienv penv tenv) = true
  | .ule => (a.toBV benv nenv ienv penv tenv).ule (b.toBV benv nenv ienv penv tenv) = true
  | .slt => (a.toBV benv nenv ienv penv tenv).slt (b.toBV benv nenv ienv penv tenv) = true
  | .sle => (a.toBV benv nenv ienv penv tenv).sle (b.toBV benv nenv ienv penv tenv) = true
| .and p1 p2 => p1.toBV benv nenv ienv penv tenv  ∧ p2.toBV benv nenv ienv penv tenv
| .or p1 p2 => p1.toBV benv nenv ienv penv tenv ∨ p2.toBV benv nenv ienv penv tenv
| .boolBinRel rel a b =>
  match rel with
  
  | .eq => (a.toBV benv nenv ienv penv tenv) = (b.toBV benv nenv ienv penv tenv)
| .pvar v => penv v

inductive Term {wcard tcard : Nat} (bcard : Nat) (ncard : Nat) (icard : Nat) (pcard : Nat)
  (tctx : Term.Ctx wcard tcard) : TermKind wcard → Type

| ofNat (w : WidthExpr wcard) (n : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| var (v : Fin tcard) : Term bcard ncard icard pcard tctx (.bv (tctx v))
 
| add (a : Term bcard ncard icard pcard tctx (.bv w))
  (b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| shiftl (a : Term bcard ncard icard pcard tctx (.bv w)) (k : Nat) : Term bcard ncard icard pcard tctx (.bv w)
 
| bor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| band (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bxor (a b : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| bnot (a : Term bcard ncard icard pcard tctx (.bv w)) : Term bcard ncard icard pcard tctx (.bv w)
 
| zext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| setWidth (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| sext (a : Term bcard ncard icard pcard tctx (.bv w)) (v : WidthExpr wcard) : Term bcard ncard icard pcard tctx (.bv v)
 
| bvOfBool (b : Term bcard ncard icard pcard tctx .bool) : Term bcard ncard icard pcard tctx (.bv (.const 1))

| boolConst (b : Bool) : Term bcard ncard icard pcard tctx .bool
| boolVar (v : Fin bcard) : Term bcard ncard icard pcard tctx .bool
| binWidthRel (k : WidthBinaryRelationKind) (wa wb : WidthExpr wcard) :
    Term bcard ncard icard pcard tctx .prop
| binRel
    (k : BinaryRelationKind)
    (w : WidthExpr wcard)
    (a : Term bcard ncard icard pcard tctx (.bv w))
    (b : Term bcard ncard icard pcard tctx (.bv w)) :
    Term bcard ncard icard pcard tctx .prop
| and (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| or (p1 p2 : Term bcard ncard icard pcard tctx (.prop)) : Term bcard ncard icard pcard tctx (.prop)
| pvar (v : Fin pcard) : Term bcard ncard icard pcard tctx (.prop)

| boolBinRel
  (k : BoolBinaryRelationKind)
  (a b : Term bcard ncard icard pcard tctx .bool) :
  Term bcard ncard icard pcard tctx (.prop)

def Term.Ctx.Env.get {tcard : Nat}
  {wcard : Nat} {wenv : Fin wcard → Nat}
  {tctx : Term.Ctx wcard tcard}
  (tenv : tctx.Env wenv) (i : Nat) (hi : i < tcard) :
  BitVec ((tctx ⟨i, hi⟩).toNat wenv) :=
  tenv ⟨i, hi⟩

inductive BinaryRelationKind
| eq
| ne
| ule
| slt
| sle
| ult 
deriving DecidableEq, Repr, Inhabited, Lean.ToExpr

inductive WidthBinaryRelationKind
| eq
| le

deriving DecidableEq, Repr, Inhabited, Lean.ToExpr

abbrev ofBitVecSext {w} (x : BitVec w) : BitStream :=
  fun i => if i < w then x.getLsbD i else x.msb

abbrev zero   : BitStream := fun _ => false

def carry' (initCarry : Bool) (x y : BitStream) : BitStream :=
  fun n =>
  match n with
  | 0 => initCarry
  | n + 1 => (addAux' initCarry x y n).2

def addAux' (carryIn : Bool) (x y : BitStream) (i : Nat) :  Bool × Bool :=
  let carryIn : Bool := match i with
    | 0 => carryIn
    | i + 1 => (addAux' carryIn x y i).2
  Prod.swap (BitVec.adcb (x i) (y i) carryIn)

def foo2_after := [llvm|
{
^0(%arg46 : i32, %arg47 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.icmp "sgt" %arg46, %0 : i32
  %3 = llvm.sub %1, %arg47 : i32
  %4 = "llvm.select"(%2, %arg47, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %5 = llvm.add %arg46, %4 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

@[simp]
def casesOn_toCons
    {motive : (Γ : Ctxt Ty) → (t t' : Ty) → Ctxt.Var (Γ.cons t') t → Sort _}
    {Γ : Ctxt Ty} {t t' : Ty} (v : Γ.Var t)
    (base : {t t' : Ty} →
        {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' v.toCons)
    (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last _ _)) :
      Ctxt.Var.casesOn (motive := motive) (toCons (t' := t') v) base last = base v :=
  rfl

def binop_same_val_and : RISCVPeepholeRewrite [Ty.riscv (.bv)] where
  lhs := [LV| {
    ^entry (%x: !riscv.reg):
      %0 = and %x, %x : !riscv.reg
      ret %0 : !riscv.reg
  }]
  rhs := [LV| {
    ^entry (%x: !riscv.reg):
      ret %x : !riscv.reg
  }]

def lshrult_03_07_before := [llvm|
{
^0(%arg328 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(7 : i4) : i4
  %2 = llvm.lshr %arg328, %0 : i4
  %3 = llvm.icmp "ult" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def ne_umin2_before := [llvm|
{
^0(%arg42 : i32, %arg43 : i32):
  %0 = llvm.icmp "ult" %arg43, %arg42 : i32
  %1 = "llvm.select"(%0, %arg43, %arg42) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "ne" %1, %arg42 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def n9_wrong_x1_before := [llvm|
{
^0(%arg14 : i8, %arg15 : i8):
  %0 = llvm.mlir.constant(15 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(16 : i8) : i8
  %3 = llvm.mlir.constant(-16 : i8) : i8
  %4 = llvm.and %arg14, %0 : i8
  %5 = llvm.icmp "eq" %4, %1 : i8
  %6 = llvm.add %arg15, %2 : i8
  %7 = llvm.and %6, %3 : i8
  %8 = "llvm.select"(%5, %arg14, %7) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%8) : (i8) -> ()
}
]

def select_icmp_eq_pow2_before := [llvm|
{
^0(%arg13 : i8):
  %0 = llvm.mlir.constant(4 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.and %arg13, %0 : i8
  %3 = llvm.icmp "eq" %2, %1 : i8
  %4 = llvm.xor %arg13, %0 : i8
  %5 = "llvm.select"(%3, %arg13, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def alive_InstCombineShift__476_tgt  (w : Nat)  :=
[llvm( w )| {
^bb0(%Y : _, %X : _, %C : _, %C2 : _):
  %v1 = llvm.shl %Y, %C
  %v2 = llvm.shl %C2, %C
  %v3 = llvm.and %X, %v2
  %v4 = llvm.lshr %X, %C
  %v5 = llvm.and %v4, %C2
  %v6 = llvm.or %v5, %Y
  %v7 = llvm.or %v3, %v1
  llvm.return %v7
}]

def t3_c0_before := [llvm|
{
^0(%arg25 : i8, %arg26 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.sub %0, %arg25 : i8
  %2 = llvm.sub %1, %arg26 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

Function.comp in Init.Prelude

def c0_before := [llvm|
{
^0(%arg7 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.and %arg7, %0 : i8
  %2 = llvm.icmp "sle" %1, %arg7 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def ashrsgt_02_10_exact_after := [llvm|
{
^0(%arg75 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def Term.numVars (t : Term) : Nat := t.f.numVars

def band_land_right1_after := [llvm|
{
^0(%arg34 : i1, %arg35 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg34, %arg35, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def icmp_select_var_pred_ne_after := [llvm|
{
^0(%arg71 : i8, %arg72 : i8, %arg73 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "ne" %arg71, %0 : i8
  %3 = llvm.icmp "ne" %arg72, %arg73 : i8
  %4 = "llvm.select"(%2, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def sdiv_icmp6_after := [llvm|
{
^0(%arg8 : i64):
  %0 = llvm.mlir.constant(5) : i64
  %1 = llvm.icmp "eq" %arg8, %0 : i64
  "llvm.return"(%1) : (i1) -> ()
}
]

Lean.Expr.forallE in Lean.Expr

instance instEffToMonadRefinement :
    HRefinement (eff₁.toMonad m α) (eff₂.toMonad n β) where
  IsRefinedBy x y := coe_toMonad x ⊑ coe_toMonad y

def add_umin_constant_limit_before := [llvm|
{
^0(%arg55 : i32):
  %0 = llvm.mlir.constant(41 : i32) : i32
  %1 = llvm.mlir.constant(42 : i32) : i32
  %2 = llvm.add %arg55, %0 overflow<nuw> : i32
  %3 = llvm.icmp "ult" %2, %1 : i32
  %4 = "llvm.select"(%3, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def test_mul_nsw__nsw_is_safe_before := [llvm|
{
^0(%arg5 : i32):
  %0 = llvm.mlir.constant(-83886080 : i32) : i32
  %1 = llvm.mlir.constant(-83886079 : i32) : i32
  %2 = llvm.mlir.constant(9 : i32) : i32
  %3 = llvm.mlir.constant(-754974711 : i32) : i32
  %4 = llvm.or %arg5, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.mul %4, %2 overflow<nsw> : i32
  %7 = "llvm.select"(%5, %3, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def const_sub_add_const_after := [llvm|
{
^0(%arg30 : i32):
  %0 = llvm.mlir.constant(10 : i32) : i32
  %1 = llvm.sub %0, %arg30 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def pack (x : Stream α) (y : Stream Unit) : Stream α :=
  syncMap₂ (xs := x) (ys := y) (f := wrapReadyValue)

structure NFA'.correct2 (M : NFA' 2) (ζ : M.sa2) (L : BVRel) where
  cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2)
  cond2 q : q ∈ M.M.start ↔ ζ q .nil .nil
  cond3 q a w (bv1 bv2 : BitVec w) : q ∈ M.M.stepSet { q | ζ q bv1 bv2 } a ↔
              ζ q (BitVec.cons (a.getLsbD 0) bv1) (BitVec.cons (a.getLsbD 1) bv2)

Lean.instantiateMVars in Lean.MetavarContext

def sdiv_ult_smin_after := [llvm|
{
^0(%arg18 : i8, %arg19 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.sdiv %arg18, %arg19 : i8
  %2 = llvm.icmp "sgt" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def add_i32_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32), Ty.llvm (.bitvec 32)] where
  lhs := add_llvm_i32
  rhs := add_riscv_i32

def ashr_ugt_0_after := [llvm|
{
^0(%arg116 : i4):
  %0 = llvm.mlir.constant(1 : i4) : i4
  %1 = llvm.icmp "ugt" %arg116, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

def lshr_exact_add_negative_shift_positive_after := [llvm|
{
^0(%arg56 : i32):
  %0 = llvm.mlir.constant(4 : i32) : i32
  %1 = llvm.lshr exact %0, %arg56 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def icmp_ne_sext_sgt_zero_nofold_after := [llvm|
{
^0(%arg6 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "sgt" %arg6, %0 : i32
  %2 = llvm.sext %1 : i1 to i32
  %3 = llvm.icmp "ne" %arg6, %2 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def sle_swap_and_min_logical_after := [llvm|
{
^0(%arg212 : i8, %arg213 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.icmp "eq" %arg212, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def lshrugt_03_10_exact_before := [llvm|
{
^0(%arg179 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(-6 : i4) : i4
  %2 = llvm.lshr exact %arg179, %0 : i4
  %3 = llvm.icmp "ugt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def alive_AddSub_1152_tgt  :=
[sllvm| {
^bb0(%y : i1, %x : i1):
  %v1 = llvm.xor %x, %y : i1
  llvm.return %v1 : i1
}]

trace[Generalize] m! "lhs width: {lhsRes.width}; rhs width: {rhsRes.width}"
  if h : lhsRes.width = rhsRes.width then
    let rhsExpr := h ▸ rhsRes.bvExpr
    
    
    let bvLogicalExpr := BoolExpr.literal (FpPredicate.bin lhsRes.bvExpr FpBinaryPredKind.eq rhsExpr)
    trace[Generalize] m! "BVLogicalExpr: {bvLogicalExpr}"
    return some {lhs := lhs, rhs := rhs, state := state, logicalExpr := bvLogicalExpr}

instance : ToMessageData (ParsedInputState) where
  toMessageData s := printParsedFpExprState s

def slt_zero_ne_ne_b_before := [llvm|
{
^0(%arg2 : i32, %arg3 : i32):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.icmp "ne" %arg2, %arg3 : i32
  %2 = llvm.zext %1 : i1 to i32
  %3 = llvm.lshr %arg2, %0 : i32
  %4 = llvm.icmp "ne" %2, %3 : i32
  "llvm.return"(%4) : (i1) -> ()
}
]

def cadicalTimeoutSec : Nat := 1000

def ashr1_before := [llvm|
{
^0(%arg29 : i64):
  %0 = llvm.mlir.constant(8) : i64
  %1 = llvm.mlir.constant(2) : i64
  %2 = llvm.shl %arg29, %0 : i64
  %3 = llvm.ashr %2, %1 : i64
  "llvm.return"(%3) : (i64) -> ()
}
]

def test11_before := [llvm|
{
^0(%arg6 : i32, %arg7 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(128 : i32) : i32
  %2 = llvm.shl %arg6, %0 : i32
  %3 = llvm.add %2, %arg7 : i32
  %4 = llvm.and %3, %1 : i32
  %5 = llvm.mul %4, %2 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def MatchArgResult.toHom
    (map : MatchArgResult lets matchLets vs ws mapIn)
    (hvars : ∀ t (v : Var Δ_in t), ⟨t, v⟩ ∈ matchLets.varsOfVec ws) :
    Δ_in.Hom Γ_out :=
  map.val.toHom <| map.isTotal_of hvars

def testi64i32_after := [llvm|
{
^0(%arg8 : i64):
  %0 = llvm.mlir.constant(2147483648) : i64
  %1 = llvm.mlir.constant(4294967296) : i64
  %2 = llvm.add %arg8, %0 : i64
  %3 = llvm.icmp "ult" %2, %1 : i64
  "llvm.return"(%3) : (i1) -> ()
}
]

def test58_before := [llvm|
{
^0(%arg124 : i64):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.mlir.constant(128 : i32) : i32
  %2 = llvm.trunc %arg124 : i64 to i32
  %3 = llvm.lshr %2, %0 : i32
  %4 = llvm.or %3, %1 : i32
  %5 = llvm.zext %4 : i32 to i64
  "llvm.return"(%5) : (i64) -> ()
}
]

@[simp]
def liftUnop_unchanged' (k : Fin n) : liftUnop n k.castSucc = k.castLE (by simp) :=

@[simp_denote]
def select_riscv_32 := [LV| {
  ^entry (%cond : i1, %arg0: i32, %arg1: i32):
    %0 = "builtin.unrealized_conversion_cast" (%arg0) : (i32) -> (!i64)
    %1 = "builtin.unrealized_conversion_cast" (%arg1) : (i32) -> (!i64)
    %2 = "builtin.unrealized_conversion_cast" (%cond) : (i1) -> (!i64)
    %3 = snez %2 : !i64
    %4 = sub %0, %1 : !i64
    %5 = mul %4, %3 : !i64
    %6 = add %5, %1 : !i64
    %7 = "builtin.unrealized_conversion_cast" (%6) : (!i64) -> (i32)
    llvm.return %7 : i32
  }]

modify in Init.Prelude

def elabDefSignatureFor (dialect : Term) (alts : TSyntax ``matchAltsSig) : CommandElabM Unit := do
  let msg := (return m!"{exceptEmoji ·} Defining operation signature for {dialect} dialect")
  withTraceNode `LeanMLIR.Elab msg (collapsed := false) <| do
    let alts := getMatchAlts alts
    let alts ← do
      alts.mapM fun view => do
        trace[LeanMLIR.Elab] m!"Parsing match alternative with\n\
          \tpatterns: {view.patterns}\n\
          \tsignature: {view.rhs}"
        let rhs ← parseSignature view.rhs
        return { view with rhs }

Lean.Parser.sepBy in Lean.Parser.Basic

def test_add__all_are_safe_after := [llvm|
{
^0(%arg44 : i32):
  %0 = llvm.mlir.constant(1073741823 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.and %arg44, %0 : i32
  %3 = llvm.add %2, %1 overflow<nsw,nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def or_not_and_and_not_and_xor_commute3_after := [llvm|
{
^0(%arg280 : i32, %arg281 : i32, %arg282 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.and %arg281, %arg282 : i32
  %2 = llvm.xor %1, %0 : i32
  %3 = llvm.or %arg280, %2 : i32
  %4 = llvm.xor %arg282, %arg281 : i32
  %5 = llvm.and %4, %arg280 : i32
  %6 = llvm.xor %5, %3 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def add_nsw_poison_constant_fold_after := [llvm|
{
^0(%arg2 : i1, %arg3 : i8):
  %0 = llvm.mlir.constant(64 : i8) : i8
  %1 = llvm.mlir.constant(-127 : i8) : i8
  %2 = llvm.add %arg3, %0 overflow<nsw> : i8
  %3 = "llvm.select"(%arg2, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def bvExprToSubstitutionValue (map: Std.HashMap Nat BVExprWrapper) : Std.HashMap Nat (SubstitutionValue GenBVExpr) :=
      Std.HashMap.ofList (List.map (fun item => (item.fst, SubstitutionValue.genExpr item.snd.bvExpr)) map.toList)

def test32_before := [llvm|
{
^0(%arg254 : i32):
  %0 = llvm.mlir.constant(16 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.mlir.constant(1 : i32) : i32
  %3 = llvm.and %arg254, %0 : i32
  %4 = llvm.lshr %3, %1 : i32
  %5 = llvm.and %4, %2 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def test_invalid_simplify_other_after := [llvm|
{
^0(%arg204 : i8, %arg205 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(-1 : i8) : i8
  %2 = llvm.icmp "eq" %arg204, %0 : i8
  %3 = llvm.add %arg205, %1 : i8
  %4 = "llvm.select"(%2, %0, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def logic_and_logic_or_6_after := [llvm|
{
^0(%arg162 : i1, %arg163 : i1, %arg164 : i1):
  %0 = llvm.mlir.constant(true) : i1
  %1 = llvm.mlir.constant(false) : i1
  %2 = "llvm.select"(%arg164, %0, %arg163) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%arg162, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def lshrugt_03_01_exact_before := [llvm|
{
^0(%arg188 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(1 : i4) : i4
  %2 = llvm.lshr exact %arg188, %0 : i4
  %3 = llvm.icmp "ugt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def p0_after := [llvm|
{
^0(%arg17 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.icmp "ugt" %arg17, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def rem_euclid_i128_before := [llvm|
{
^0(%arg6 : i128):
  %0 = llvm.mlir.constant(8 : i128) : i128
  %1 = llvm.mlir.constant(0 : i128) : i128
  %2 = llvm.srem %arg6, %0 : i128
  %3 = llvm.icmp "slt" %2, %1 : i128
  %4 = llvm.add %2, %0 : i128
  %5 = "llvm.select"(%3, %4, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i128, i128) -> i128
  "llvm.return"(%5) : (i128) -> ()
}
]

def substitute_constant_and_eq_eq_commute_before := [llvm|
{
^0(%arg318 : i8, %arg319 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.icmp "eq" %arg318, %0 : i8
  %2 = llvm.icmp "eq" %arg318, %arg319 : i8
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]
</all_available_defs>

<all_available_lemmas>
BitVec.msb_eq_getLsbD_last in Init.Data.BitVec.Lemmas
BitVec.getElem_signExtend in Init.Data.BitVec.Lemmas
BitVec.of_length_zero in Init.Data.BitVec.Lemmas
BitVec.slt_eq_not_carry in Init.Data.BitVec.Bitblast

protected theorem carry'_eq_carry (x y : BitStream) (c : Bool)
    (x' y' : BitVec w)
    (hx : ∀ i, i < n → x'.getLsbD i = x i)
    (hy : ∀ i,  i < n → y'.getLsbD i = y i) :
    carry' c x y n = (BitVec.carry n x' y' c)

@[simp] theorem carry'_succ (initCarry : Bool) (x y : BitStream) :
    (carry' initCarry x y (i + 1)) =
    let out

theorem fold_nested_logic_zext_icmp_thm.extracted_1._1 : ∀ (x x_1 x_2 x_3 : BitVec 64),
  zeroExtend 8 (ofBool (x_2 <ₛ x_3)) &&& zeroExtend 8 (ofBool (x_3 <ₛ x_1)) ||

theorem test2_proof : test2_before ⊑ test2_after

theorem nonexact_ashr_eq_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬x ≥ ↑8 → ofBool ((BitVec.ofInt 8 (-128)).sshiftRight' x == -1#8) = ofBool (x == 7#8)

theorem t0_thm (e e_1 e_2 : IntW 8) : sub (sub e_2 e_1) e ⊑ sub e_2 (add e_1 e)

theorem t3_exact_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ¬(True ∧ x >>> 63#64 <<< 63#64 ≠ x ∨ 63#64 ≥ ↑64) → 0#64 - x.sshiftRight' 63#64 = x >>> 63#64

theorem e_119 :
    7 * y - 11 *  ~~~y + 9 *  ~~~(x ||| y) - 7 *  ~~~(x |||  ~~~y) + 8 * (x &&&  ~~~y) - 12 * (x &&& y) =  - 2 *  ~~~(x ^^^ y) - 3 * x

theorem masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_6_proof : masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_6_before ⊑ masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_6_after

theorem shl_nsw_add_nuw_proof : shl_nsw_add_nuw_before ⊑ shl_nsw_add_nuw_after

theorem shl_xor_xor_bad_mask_distribute_thm (e e_1 : IntW 8) :
  LLVM.xor (shl e_1 (const? 8 1)) (LLVM.xor (shl e (const? 8 1)) (const? 8 (-68))) ⊑
    LLVM.xor (shl (LLVM.xor e e_1) (const? 8 1)) (const? 8 (-68))

theorem mul8_low_A0_B0_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8),
  ¬(4#8 ≥ ↑8 ∨ 4#8 ≥ ↑8 ∨ 4#8 ≥ ↑8) →
    (x_1 >>> 4#8 * x + x >>> 4#8 * x_1) <<< 4#8 + (x_1 &&& 15#8) * (x &&& 15#8) = x * x_1

theorem reused_mul_nuw_xy_z_selectnonzero_ugt_thm.extracted_1._3 : ∀ (x x_1 : BitVec 8),
  ¬ofBool (x_1 != 0#8) = 1#1 → ¬ofBool (x_1 == 0#8) = 1#1 → ¬(True ∧ x.umulOverflow x_1 = true) → False

theorem icmp_slt_0_xor_icmp_sge_neg2_i32_fail_proof : icmp_slt_0_xor_icmp_sge_neg2_i32_fail_before ⊑ icmp_slt_0_xor_icmp_sge_neg2_i32_fail_after

theorem shift_xor_multiuse_cmp_proof : shift_xor_multiuse_cmp_before ⊑ shift_xor_multiuse_cmp_after

theorem test19a_proof : test19a_before ⊑ test19a_after

theorem test_add__none_are_safe_proof : test_add__none_are_safe_before ⊑ test_add__none_are_safe_after

theorem main3e_like_logical_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (x_2 &&& x_1 == 0#32) = 1#1 →
    ofBool (x_2 &&& x_1 != 0#32) = 1#1 → ofBool (x_2 &&& x == 0#32) = 1#1 → 0#32 = zeroExtend 32 1#1

theorem or_test1_proof : or_test1_before ⊑ or_test1_after

theorem e_52 :
    11 *  ~~~(x &&&  ~~~x) - 11 * (x ^^^ y) - 12 *  ~~~(x ||| y) - 1 * (x &&&  ~~~y) - 12 * (x &&& y) =  - 1 * (x |||  ~~~y)

theorem e_151 :
     - 6 *  ~~~(x ^^^ y) - 1 * y + 1 *  ~~~(x ||| y) - 4 *  ~~~(x |||  ~~~y) + 11 * (x &&&  ~~~y) + 13 * (x &&& y) = 11 * x - 5 *  ~~~(x &&&  ~~~y)

theorem sle_or_not_min_commute_logical_thm (e e_1 : IntW 8) :
  select (icmp IntPred.ne e_1 (const? 8 (-128))) (const? 1 1) (icmp IntPred.sle e_1 e) ⊑ const? 1 1

theorem e_1444 :
     - 1 *  ~~~t - 6 *  ~~~(z &&&  ~~~z) + 5 *  ~~~(z ^^^ t) - 7 *  ~~~z - 5 *  ~~~(z &&& t) + 7 * (z ^^^ t) - 1 * (z |||  ~~~t) + 15 *  ~~~(z ||| t) + 11 *  ~~~(z |||  ~~~t) + 2 * (z &&& t) =  - 6 * (z &&&  ~~~t)

theorem main11_logical_proof : main11_logical_before ⊑ main11_logical_after

theorem t5_ugt_slt_0_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬ofBool (143#32 <ᵤ x + 16#32) = 1#1 →
    ofBool (127#32 <ₛ x) = 1#1 ∨ ofBool (x <ₛ BitVec.ofInt 32 (-16)) = 1#1 → False

theorem t1_thm (e : IntW 8) :
  icmp IntPred.sge (sub (const? 8 0) e { «nsw» := true, «nuw» := false }) e ⊑
    icmp IntPred.slt e (const? 8 1)

theorem or_logic_or_logic_and_3_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), x_1 = 1#1 → ¬True → x_1 ||

theorem bools_multi_uses1_logical_proof : bools_multi_uses1_logical_before ⊑ bools_multi_uses1_logical_after

theorem t0_basic_thm (e e_1 : IntW 8) :
  icmp IntPred.ult (add e_1 e) e ⊑ icmp IntPred.ugt e_1 (LLVM.xor e (const? 8 (-1)))

theorem test10b_proof : test10b_before ⊑ test10b_after

theorem sub_inc_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), x_1 - (x + 1#8) = x_1 + (x ^^^ -1#8)

theorem icmp_slt_0_or_icmp_add_1_sge_100_i32_fail_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬31#32 ≥ ↑32 →
    x >>> 31#32 ||

theorem bools_logical_commute3_and2_thm.extracted_1._9 : ∀ (x x_1 x_2 : BitVec 1),
  x_2 = 1#1 → ¬x_1 = 1#1 → x_1 ^^^ 1#1 = 1#1 → 1#1 = x_2

theorem e_199 :
    3 * (x ||| y) - 11 *  ~~~(x &&&  ~~~y) + 4 *  ~~~(x ^^^ y) + 1 *  ~~~(x &&&  ~~~x) + 3 * y - 4 * (x &&&  ~~~y) =  - 6 *  ~~~(x ||| y) - 4 *  ~~~(x |||  ~~~y)

theorem masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_5_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 15#32 != 8#32) = 1#1 → 1#1 = ofBool (x &&& 15#32 != 8#32)

theorem scalar_i8_shl_ult_const_3_proof : scalar_i8_shl_ult_const_3_before ⊑ scalar_i8_shl_ult_const_3_after

theorem and_or2_thm.extracted_1._4 : ∀ (x x_1 x_2 : BitVec 1),
  (x_2 ^^^ 1#1) &&& x_1 = 1#1 → x_1 = 1#1 → x_2 = 1#1 → x = 1#1

@[simp] theorem dropUntilHom_toCons {v : Var Γ t} :
  dropUntilHom (v := v.toCons (t' := t')) = (dropUntilHom (v:=v)).consRight

theorem or_eq_with_diff_one_logical_thm.extracted_1._2 : ∀ (x : BitVec 8),
  ¬ofBool (x == 13#8) = 1#1 → ofBool (x == 14#8) = ofBool (x + BitVec.ofInt 8 (-13) <ᵤ 2#8)

theorem test10_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬16#32 ≥ ↑32 →
    ¬(16#32 ≥ ↑32 ∨ True ∧ (x >>> 16#32).umulOverflow 65535#32 = true) →
      zeroExtend 64 (x >>> 16#32) * 65535#64 = zeroExtend 64 (x >>> 16#32 * 65535#32)

theorem lshrult_03_06_exact_proof : lshrult_03_06_exact_before ⊑ lshrult_03_06_exact_after

theorem ashr_ugt_8_proof : ashr_ugt_8_before ⊑ ashr_ugt_8_after

theorem add_or_sub_comb_i32_commuted1_nuw_proof : add_or_sub_comb_i32_commuted1_nuw_before ⊑ add_or_sub_comb_i32_commuted1_nuw_after

theorem or_not_xor_common_op_commute3_proof : or_not_xor_common_op_commute3_before ⊑ or_not_xor_common_op_commute3_after

theorem lor_band_left2_proof : lor_band_left2_before ⊑ lor_band_left2_after

theorem ashr_x_by_const_cmp_sge_x_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ¬5#32 ≥ ↑32 → ofBool (x ≤ₛ x.sshiftRight' 5#32) = ofBool (x <ₛ 1#32)

theorem lsb_mask_sign_sext_thm (e : IntW 32) :
  ashr (LLVM.and (add e (const? 32 (-1))) (LLVM.xor e (const? 32 (-1)))) (const? 32 31) ⊑
    sext 32 (icmp IntPred.eq e (const? 32 0))

theorem ne_10_proof : ne_10_before ⊑ ne_10_after

theorem lt_unsigned_to_large_signed_proof : lt_unsigned_to_large_signed_before ⊑ lt_unsigned_to_large_signed_after

theorem sel_false_val_is_a_masked_ashr_of_true_val2_thm.extracted_1._3 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬2#32 ≥ ↑32 →
    ¬ofBool ((x_1 &&& BitVec.ofInt 32 (-2147483588)).sshiftRight' 2#32 == 0#32) = 1#1 →
      ¬(2#32 ≥ ↑32 ∨ zeroExtend 64 ((x_1 &&& BitVec.ofInt 32 (-2147483588)).sshiftRight' 2#32) ≥ ↑64) →
        2#32 ≥ ↑32 ∨
            True ∧ (x_1.sshiftRight' 2#32 &&& BitVec.ofInt 32 (-536870897)).msb = true ∨
              zeroExtend 64 (x_1.sshiftRight' 2#32 &&& BitVec.ofInt 32 (-536870897)) ≥ ↑64 →
          False

theorem n1_proof : n1_before ⊑ n1_after

theorem and_logic_and_logic_or_3_thm.extracted_1._4 : ∀ (x x_1 x_2 : BitVec 1),
  x_2 &&& x_1 = 1#1 → ¬x_1 = 1#1 → 1#1 = 0#1

theorem test_eq_11_and_15_add_10_proof : test_eq_11_and_15_add_10_before ⊑ test_eq_11_and_15_add_10_after

theorem test3_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 599),
  x = 1#1 → ¬70368744177664#599 = 0 → 46#599 ≥ ↑599 → False

theorem icmp_ne_zext_ne_non_boolean_proof : icmp_ne_zext_ne_non_boolean_before ⊑ icmp_ne_zext_ne_non_boolean_after

theorem e_1324 :
     - 1 * z - 1 * t + 7 * (z ^^^ t) - 11 *  ~~~(z &&&  ~~~z) - 11 *  ~~~(z ^^^ t) + 3 *  ~~~(z &&& t) - 3 * (z ||| t) + 19 *  ~~~(z ||| t) + 5 * (z &&&  ~~~t) =  - 5 *  ~~~(z |||  ~~~t) - 27 * (z &&& t)

theorem test65_proof : test65_before ⊑ test65_after

theorem add_eq_sll (a : Nat) : a + a = a <<< 1

theorem mul_select_sext_thm.extracted_1._2 : ∀ (x : BitVec 1), ¬x = 1#1 → 1#64 * signExtend 64 x = 0#64

theorem ashrslt_01_15_proof : ashrslt_01_15_before ⊑ ashrslt_01_15_after

theorem e_1552 :
     - 7 * (b ^^^ ( ~~~a ||| (b &&& c))) - 6 * (b ^^^ (a ||| (b &&& c))) + 1 * (b ^^^  ~~~(a &&& ( ~~~b ||| c))) - 11 * (b ^^^ ( ~~~a &&& (b ^^^ c))) + 5 * (a ||| (b ||| c)) + 6 *  ~~~(a ||| (b ||| c)) - 1 *  ~~~(a ||| ( ~~~b ||| c)) - 1 *  ~~~( ~~~a ||| (b ||| c)) + 11 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 12 * ( ~~~a &&& ( ~~~b &&& c)) + 6 * ( ~~~a &&& (b &&& c)) - 1 * (a &&& ( ~~~b &&& c)) + 3 * (a &&& (b &&& c)) =  - 2 *  ~~~( ~~~a &&& ( ~~~b ||| c))

theorem lshrugt_03_03_proof : lshrugt_03_03_before ⊑ lshrugt_03_03_after

theorem demorgan_nor_proof : demorgan_nor_before ⊑ demorgan_nor_after

theorem main7c_logical_proof : main7c_logical_before ⊑ main7c_logical_after
</all_available_lemmas>

<local_ctx>
import Blase.Fast.FiniteStateMachine

import Blase.Vars

import Blase.MultiWidth.Defs

import Blase.KInduction.KInduction

import Lean

namespace MultiWidth

def fsmMsb (x w : FSM α) : FSM α :=
  composeBinaryAux'
    (FSM.latchImmediate false)
    (qfalse := x)
    (qtrue := w)

def fsmCarry'' (initialCarryVal : Bool): FSM Bool :=
  let outputCirc :=
    let carry := Circuit.var true (Sum.inl ())
    let a := Circuit.var true (Sum.inr true)
    let b := Circuit.var true (Sum.inr false)
    
    ((a &&& b) ||| (a &&& carry) ||| (b &&& carry))
  { α := Unit,
    
    
    initCarry := fun () => initialCarryVal, 
    outputCirc := Circuit.var true (Sum.inl ()) ,
    nextStateCirc := fun () => outputCirc
  }

def fsmMsbEq (a : FSM α) (b : FSM α) : FSM α :=
  composeUnaryAux (FSM.ls false) <|
    composeBinaryAux' FSM.xor a b

def fsmTermSlt
  {wcard tcard : Nat}
  {w : Nondep.WidthExpr}
  {a b : Nondep.Term}
  (wfsm : NatFSM wcard tcard bcard ncard icard pcard w)
  (afsm : TermFSM wcard tcard bcard ncard icard pcard a)
  (bfsm : TermFSM wcard tcard bcard ncard icard pcard b)
  : FSM (StateSpace wcard tcard bcard ncard icard pcard) :=
    let afsm := afsm.toFsmZext
    let bfsm := bfsm.toFsmZext
    let afsm := fsmMsb afsm wfsm.toFsm
    let bfsm := fsmMsb bfsm wfsm.toFsm
    let carryFsm :=
      (~~~ (composeBinaryAux' (fsmCarry'' true)  afsm (~~~ bfsm)))
    let xorFsm := fsmMsbEq afsm bfsm
    let val := xorFsm ^^^ carryFsm
    val
</local_ctx>

<target_theorem>
theorem eval_fsmTermSlt_eq_decide_slt {wcard tcard : Nat}
    (tctx : Term.Ctx wcard tcard)
    {wenv : WidthExpr.Env wcard}
    (tenv : tctx.Env wenv)
    (benv : Term.BoolEnv bcard)
    (nenv : Term.NatEnv ncard)
    (ienv : Term.IntEnv icard)
    (w : WidthExpr wcard)
    (a : Term bcard ncard icard pcard tctx (.bv w))
    (b : Term bcard ncard icard pcard tctx (.bv w))
    (wfsm : NatFSM wcard tcard bcard ncard icard pcard (.ofDep w))
    (hwfsm : HNatFSMToBitstream wfsm)
    (afsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm a))
    (hafsm : HTermFSMToBitStream afsm)
    (bfsm : TermFSM wcard tcard bcard ncard icard pcard (.ofDepTerm b))
    (hbfsm : HTermFSMToBitStream bfsm)
    (fsmEnv : StateSpace wcard tcard bcard ncard icard pcard → BitStream)
    (henv : HTermEnv fsmEnv tenv benv)
    :
    ((fsmTermSlt
      wfsm
      afsm
      bfsm)).eval fsmEnv i =
       decide (((a.toBV benv nenv ienv penv tenv).signExtend i).slt
          ((b.toBV benv nenv ienv penv tenv).signExtend i)) :=
</target_theorem>

