def ComWrappers.const {Γ : Ctxt InstCombine.LLVM.Ty} (w : ℕ) (n : ℤ) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.const w n = Expr.mk (InstCombine.MOp.const (ConcreteOrMVar.concrete w) n) ⋯ ⋯ HVector.nil HVector.nil

def ComWrappers.not {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.not w l lp = Expr.mk (InstCombine.MOp.not (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕHVector.nil) HVector.nil

def ComWrappers.neg {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.neg w l lp = Expr.mk (InstCombine.MOp.neg (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕHVector.nil) HVector.nil

def ComWrappers.and {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.and w l r lp rp = Expr.mk (InstCombine.MOp.and (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.or {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.or w l r lp rp = Expr.mk (InstCombine.MOp.or (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.xor {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.xor w l r lp rp = Expr.mk (InstCombine.MOp.xor (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.shl {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.shl w l r lp rp = Expr.mk (InstCombine.MOp.shl (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.lshr {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.lshr w l r lp rp = Expr.mk (InstCombine.MOp.lshr (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.ashr {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.ashr w l r lp rp = Expr.mk (InstCombine.MOp.ashr (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.sub {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.sub w l r lp rp = Expr.mk (InstCombine.MOp.sub (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.add {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.add w l r lp rp = Expr.mk (InstCombine.MOp.add (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.mul {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.mul w l r lp rp = Expr.mk (InstCombine.MOp.mul (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.sdiv {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.sdiv w l r lp rp = Expr.mk (InstCombine.MOp.sdiv (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.udiv {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.udiv w l r lp rp = Expr.mk (InstCombine.MOp.udiv (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.srem {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.srem w l r lp rp = Expr.mk (InstCombine.MOp.srem (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.urem {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.urem w l r lp rp = Expr.mk (InstCombine.MOp.urem (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.icmp {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (pred : LLVM.IntPredicate) (l : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec 1)

Equations

• ComWrappers.icmp w pred l r lp rp = Expr.mk (InstCombine.MOp.icmp pred (ConcreteOrMVar.concrete w)) ComWrappers.icmp.proof_1 ⋯ (⟨l, lp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil)) HVector.nil

def ComWrappers.select {Γ : Ctxt (InstCombine.MTy 0)} (w : ℕ) (l : ℕ) (m : ℕ) (r : ℕ) (lp : autoParam (Γ.get? l = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete 1))) _auto✝) (mp : autoParam (Γ.get? m = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) (rp : autoParam (Γ.get? r = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w))) _auto✝) : Expr InstCombine.LLVM Γ EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• ComWrappers.select w l m r lp mp rp = Expr.mk (InstCombine.MOp.select (ConcreteOrMVar.concrete w)) ⋯ ⋯ (⟨l, lp⟩::ₕ(⟨m, mp⟩::ₕ(⟨r, rp⟩::ₕHVector.nil))) HVector.nil

def ComWrappers.test (w : ℕ) : Com InstCombine.LLVM [InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)

Equations

• One or more equations did not get rendered due to their size.