def add_mask : MLIR.AST.Op 0

Equations

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

def bb0 : MLIR.AST.Region 0

Equations

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

def Γn {φ : ℕ} (n : ℕ) : Ctxt (InstCombine.MetaLLVM φ).Ty

Equations

• Γn n = ↑(List.replicate n (InstCombine.MTy.bitvec 32))

def op0 : MLIR.AST.Op 0

Equations

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

def op1 : MLIR.AST.Op 0

Equations

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

def op2 : MLIR.AST.Op 0

Equations

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

def op3 : MLIR.AST.Op 0

Equations

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

def op4 : MLIR.AST.Op 0

Equations

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

def opRet : MLIR.AST.Op 0

Equations

• opRet = MLIR.AST.Op.mk "llvm.return" [] [(MLIR.AST.SSAVal.SSAVal (MLIR.EDSL.IntToString 4), MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless 32)] [] (MLIR.AST.AttrDict.mk [])

def ops : List (MLIR.AST.Op 0)

Equations

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

def ops' : List (MLIR.AST.Op 0)

Equations

• ops' = [op0, op1, op2, op3, op4]

def com : (Γ : Ctxt (InstCombine.MetaLLVM 0).Ty) × (eff : EffectKind) × (ty : (InstCombine.MetaLLVM 0).Ty) × Com (InstCombine.MetaLLVM 0) Γ eff ty

Equations

• com = (Except.toOption (MLIR.AST.mkCom bb0)).get com.proof_1

theorem com_Γ : com.fst = Γn 1

theorem com_ty : com.snd.snd.fst = InstCombine.MTy.bitvec 32

def bb0IcomConcrete : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec 32)) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy (InstCombine.MTy.bitvec 32))

Equations

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

def GenericWidth (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> []) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

A simple example of a family of programs, generic over some bitwidth w

Equations

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

def bb0IcomGeneric (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

def one_inst_macro (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

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

Equations

• one_inst_com w = Com.var (ComWrappers.not w 0 ⋯) (Com.ret ⟨0, ⋯⟩)

def one_inst_stmt {w : ℕ} (e : LLVM.IntW w) : LLVM.not e ⊑ LLVM.not e

Equations

• ⋯ = ⋯

def one_inst_com_proof (w : ℕ) : (one_inst_com w ⊑ one_inst_com w) ⋯

Equations

• ⋯ = ⋯

def one_inst_macro_proof (w : ℕ) : (one_inst_macro w ⊑ one_inst_macro w) ⋯

Equations

• ⋯ = ⋯

def two_inst_macro (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

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

Equations

• two_inst_com w = Com.var (ComWrappers.not w 0 ⋯) (Com.var (ComWrappers.not w 1 ⋯) (Com.ret ⟨1, ⋯⟩))

def two_inst_stmt {w : ℕ} (e : LLVM.IntW w) : LLVM.not e ⊑ LLVM.not e

Equations

• ⋯ = ⋯

def two_inst_com_proof (w : ℕ) : (two_inst_com w ⊑ two_inst_com w) ⋯

Equations

• ⋯ = ⋯

def two_inst_macro_proof (w : ℕ) : (two_inst_macro w ⊑ two_inst_macro w) ⋯

Equations

• ⋯ = ⋯

def three_inst_macro (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

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

Equations

• three_inst_com w = Com.var (ComWrappers.not w 0 ⋯) (Com.var (ComWrappers.not w 0 ⋯) (Com.var (ComWrappers.not w 0 ⋯) (Com.ret ⟨0, ⋯⟩)))

def three_inst_stmt {w : ℕ} (e : LLVM.IntW w) : LLVM.not (LLVM.not (LLVM.not e)) ⊑ LLVM.not (LLVM.not (LLVM.not e))

Equations

• ⋯ = ⋯

def three_inst_com_proof (w : ℕ) : (three_inst_com w ⊑ three_inst_com w) ⋯

Equations

• ⋯ = ⋯

def three_inst_macro_proof (w : ℕ) : (three_inst_macro w ⊑ three_inst_macro w) ⋯

Equations

• ⋯ = ⋯

def one_inst_concrete_macro : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec 1)) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy (InstCombine.MTy.bitvec 1))

Equations

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

def one_inst_concrete_com : Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] EffectKind.pure (InstCombine.Ty.bitvec 1)

Equations

• one_inst_concrete_com = Com.var (ComWrappers.not 1 0 one_inst_concrete_com.proof_1) (Com.ret ⟨0, one_inst_concrete_com.proof_2⟩)

def one_inst_concrete_stmt {e : LLVM.IntW 1} : LLVM.not e ⊑ LLVM.not e

Equations

• ⋯ = ⋯

def one_inst_concrete_com_proof : (one_inst_concrete_com ⊑ one_inst_concrete_com) ⋯

Equations

• one_inst_concrete_com_proof = ⋯

def one_inst_concrete_macro_proof : (one_inst_concrete_macro ⊑ one_inst_concrete_macro) ⋯

Equations

• one_inst_concrete_macro_proof = ⋯

def two_inst_concrete_macro : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec 1)) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy (InstCombine.MTy.bitvec 1))

Equations

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

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

Equations

• two_inst_concrete_com w = Com.var (ComWrappers.not w 0 ⋯) (Com.var (ComWrappers.not w 1 ⋯) (Com.ret ⟨1, ⋯⟩))

def two_inst_concrete_stmt {w : ℕ} (e : LLVM.IntW w) : LLVM.not e ⊑ LLVM.not e

Equations

• ⋯ = ⋯

def two_inst_concrete_com_proof {w : ℕ} : (two_inst_concrete_com w ⊑ two_inst_concrete_com w) ⋯

Equations

• ⋯ = ⋯

def two_inst_concrete_macro_proof : (two_inst_concrete_macro ⊑ two_inst_concrete_macro) ⋯

Equations

• two_inst_concrete_macro_proof = ⋯

def three_inst_concrete_macro : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy <$> Ctxt.snoc [] (InstCombine.MTy.bitvec 1)) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[], ⋯⟩).mapTy (InstCombine.MTy.bitvec 1))

Equations

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

def three_inst_concrete_com : Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] EffectKind.pure (InstCombine.Ty.bitvec 1)

Equations

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

def three_inst_concrete_stmt (e : LLVM.IntW 1) : LLVM.not (LLVM.not (LLVM.not e)) ⊑ LLVM.not (LLVM.not (LLVM.not e))

Equations

• ⋯ = ⋯

def three_inst_concrete_com_proof : (three_inst_concrete_com ⊑ three_inst_concrete_com) ⋯

Equations

• three_inst_concrete_com_proof = ⋯

def three_inst_concrete_macro_proof : (three_inst_concrete_macro ⊑ three_inst_concrete_macro) ⋯

Equations

• three_inst_concrete_macro_proof = ⋯

def two_ne_macro (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> (Ctxt.snoc [] (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec 1))

Equations

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

def two_ne_stmt {w : ℕ} (a : LLVM.IntW w) (b : LLVM.IntW w) : LLVM.icmp LLVM.IntPredicate.ne b a ⊑ LLVM.icmp LLVM.IntPredicate.ne b a

Equations

• ⋯ = ⋯

def two_ne_macro_proof (w : ℕ) : (two_ne_macro w ⊑ two_ne_macro w) ⋯

Equations

• ⋯ = ⋯

def constant_macro (w : ℕ) : Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> []) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Equations

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

def constant_stmt {w : ℕ} : LLVM.add (LLVM.add (LLVM.add (LLVM.add (LLVM.const? 2) (LLVM.const? 1)) (LLVM.const? 0)) (LLVM.const? (-1))) (LLVM.const? (-2)) ⊑ LLVM.add (LLVM.add (LLVM.add (LLVM.add (LLVM.const? 2) (LLVM.const? 1)) (LLVM.const? 0)) (LLVM.const? (-1))) (LLVM.const? (-2))

Equations

• ⋯ = ⋯

def constant_macro_proof (w : ℕ) : (constant_macro w ⊑ constant_macro w) ⋯

Equations

• ⋯ = ⋯