theorem
AlivePaperExamples.shift_mul
{w : ℕ}
:
(Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩)
(Com.var (Expr.mk (InstCombine.MOp.const (MLIR.AST.Width.mvar ⟨0, ⋯⟩) 1) ⋯ ⋯ HVector.nil HVector.nil)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.shl) ⋯ ⋯
(⟨0, ⋯⟩::ₕ(⋯ ▸ ⟨0 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.mul) ⋯ ⋯
(⟨0, ⋯⟩::ₕ(⋯ ▸ ⟨0 + 1 + 1 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.ret ⟨0, ⋯⟩)))) ⊑ Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.shl) ⋯ ⋯
(⟨0 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.ret ⟨0, ⋯⟩)))
⋯
theorem
AlivePaperExamples.xor_sub
{w : ℕ}
:
(Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.sub) ⋯ ⋯
(⟨0 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.xor) ⋯ ⋯
(⟨0, ⋯⟩::ₕ(⋯ ▸ ⟨0 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.ret ⟨0, ⋯⟩))) ⊑ Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩) (Com.ret ⟨0, ⋯⟩))
⋯
theorem
AlivePaperExamples.bitvec_AddSub_1309
{w : ℕ}
:
(Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.and) ⋯ ⋯
(⟨0 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.or) ⋯ ⋯
(⟨0 + 1 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.add) ⋯ ⋯
(⟨0 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.ret ⟨0, ⋯⟩)))) ⊑ Com.changeDialect (InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩)
(Com.var
(Expr.mk (InstCombine.MOp.binary (MLIR.AST.Width.mvar ⟨0, ⋯⟩) InstCombine.MOp.BinaryOp.add) ⋯ ⋯
(⟨0 + 1, ⋯⟩::ₕ(⋯ ▸ ⟨0, ⋯⟩::ₕHVector.nil)) HVector.nil)
(Com.ret ⟨0, ⋯⟩)))
⋯