Documentation

SSA.Experimental.Bits.AutoStructs.Tactic

source
theorem AutoStructs.eval_sub {x : AutoStructs.Term} {y : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
(x.sub y).evalNat vars = x.evalNat vars - y.evalNat vars
source
theorem AutoStructs.eval_add {x : AutoStructs.Term} {y : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
(x.add y).evalNat vars = x.evalNat vars + y.evalNat vars
source
theorem AutoStructs.eval_neg {x : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
x.neg.evalNat vars = -x.evalNat vars
source
theorem AutoStructs.eval_not {x : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
x.not.evalNat vars = ~~~x.evalNat vars
source
theorem AutoStructs.eval_and {x : AutoStructs.Term} {y : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
(x.and y).evalNat vars = x.evalNat vars &&& y.evalNat vars
source
theorem AutoStructs.eval_xor {x : AutoStructs.Term} {y : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
(x.xor y).evalNat vars = x.evalNat vars ^^^ y.evalNat vars
source
theorem AutoStructs.eval_or {x : AutoStructs.Term} {y : AutoStructs.Term} {w : ℕ} {vars : ℕ → BitVec w} :
(x.or y).evalNat vars = x.evalNat vars ||| y.evalNat vars
source
theorem AutoStructs.sat_and {x : AutoStructs.Formula} {y : AutoStructs.Formula} {w : ℕ} {vars : ℕ → BitVec w} :
(AutoStructs.Formula.binop AutoStructs.Binop.and x y).sat' vars ↔ x.sat' vars ∧ y.sat' vars
source
theorem AutoStructs.sat_or {x : AutoStructs.Formula} {y : AutoStructs.Formula} {w : ℕ} {vars : ℕ → BitVec w} :
(AutoStructs.Formula.binop AutoStructs.Binop.or x y).sat' vars ↔ x.sat' vars ∨ y.sat' vars
source
theorem AutoStructs.sat_impl {x : AutoStructs.Formula} {y : AutoStructs.Formula} {w : ℕ} {vars : ℕ → BitVec w} :
(AutoStructs.Formula.binop AutoStructs.Binop.impl x y).sat' vars ↔ x.sat' vars → y.sat' vars
source
theorem AutoStructs.sat_iff {x : AutoStructs.Formula} {y : AutoStructs.Formula} {w : ℕ} {vars : ℕ → BitVec w} :
(AutoStructs.Formula.binop AutoStructs.Binop.equiv x y).sat' vars ↔ (x.sat' vars ↔ y.sat' vars)
source
theorem AutoStructs.sat_neg {x : AutoStructs.Formula} {w : ℕ} {vars : ℕ → BitVec w} :
(AutoStructs.Formula.unop AutoStructs.Unop.neg x).sat' vars ↔ ¬x.sat' vars
source
theorem AutoStructs.sat_eq {w : ℕ} {vars : ℕ → BitVec w} (t1 : AutoStructs.Term) (t2 : AutoStructs.Term) :
(AutoStructs.Formula.atom AutoStructs.Relation.eq t1 t2).sat' vars ↔ t1.evalNat vars = t2.evalNat vars
source
theorem AutoStructs.sat_slt {w : ℕ} {vars : ℕ → BitVec w} (t1 : AutoStructs.Term) (t2 : AutoStructs.Term) :
(AutoStructs.Formula.atom (AutoStructs.Relation.signed AutoStructs.RelationOrdering.lt) t1 t2).sat' vars ↔ (t2.evalNat vars >ₛ t1.evalNat vars) = true
source
theorem AutoStructs.sat_sle {w : ℕ} {vars : ℕ → BitVec w} (t1 : AutoStructs.Term) (t2 : AutoStructs.Term) :
(AutoStructs.Formula.atom (AutoStructs.Relation.signed AutoStructs.RelationOrdering.le) t1 t2).sat' vars ↔ (t2.evalNat vars ≥ₛ t1.evalNat vars) = true
source
theorem AutoStructs.sat_ult {w : ℕ} {vars : ℕ → BitVec w} (t1 : AutoStructs.Term) (t2 : AutoStructs.Term) :
(AutoStructs.Formula.atom (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.lt) t1 t2).sat' vars ↔ (t2.evalNat vars >ᵤ t1.evalNat vars) = true
source
theorem AutoStructs.sat_ule {w : ℕ} {vars : ℕ → BitVec w} (t1 : AutoStructs.Term) (t2 : AutoStructs.Term) :
(AutoStructs.Formula.atom (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.le) t1 t2).sat' vars ↔ (t2.evalNat vars ≥ᵤ t1.evalNat vars) = true
source
def AutoStructs.Term.toExpr (t : AutoStructs.Term) :
Lean.Expr
Equations
Instances For
    source
    def AutoStructs.Relation.toExpr (rel : AutoStructs.Relation) :
    Lean.Expr
    Equations
    Instances For
      source
      def AutoStructs.Binop.toExpr (rel : AutoStructs.Binop) :
      Lean.Expr
      Equations
      Instances For
        source
        def AutoStructs.Unop.toExpr (rel : AutoStructs.Unop) :
        Lean.Expr
        Equations
        Instances For
          source
          def AutoStructs.Formula.toExpr (φ : AutoStructs.Formula) :
          Lean.Expr
          Equations
          Instances For
            source
            instance instToExprFormula :
            Lean.ToExpr AutoStructs.Formula
            Equations
            source
            structure Tactic.State :
            Type
            Instances For
              source
              instance Tactic.instInhabitedState :
              Inhabited Tactic.State
              Equations
              source
              @[reducible, inline]
              abbrev Tactic.M (α : Type) :
              Type
              Equations
              Instances For
                source
                def Tactic.addAsVar (e : Lean.Expr) :
                Tactic.M AutoStructs.Term
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Tactic.checkBVs (es : List Lean.Expr) :
                  Tactic.M Bool
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def Tactic.parseTerm (e : Lean.Expr) :
                    Tactic.M AutoStructs.Term
                    source
                    partial def Tactic.parseFormula (e : Lean.Expr) :
                    Tactic.M AutoStructs.Formula
                    source
                    axiom Tactic.automaton_axiom (A : Prop) :
                    A
                    source
                    def Tactic.mkFinLit (m : ℕ) (n : ℕ) :
                    Lean.MetaM Lean.Expr
                    Equations
                    Instances For
                      source
                      def Tactic.mkBitVecLit0 (w : Lean.Expr) :
                      Lean.MetaM Lean.Expr
                      Equations
                      Instances For
                        source
                        def Tactic.listExprExpr (es : List Lean.Expr) (type : Lean.Expr) :
                        Lean.Expr
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Tactic.arrayExprExpr (es : Array Lean.Expr) (type : Lean.Expr) :
                          Lean.Expr
                          Equations
                          Instances For
                            source
                            def Tactic.makeEnv (es : Array Lean.Expr) (w : Lean.Expr) :
                            Lean.MetaM Lean.Expr
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Tactic.tacticBv_automata_inner :
                              Lean.ParserDescr
                              Equations
                              Instances For
                                source
                                def Tactic.tacticBv_automata' :
                                Lean.ParserDescr
                                Equations
                                Instances For
                                  source
                                  theorem dfadfa (w : ℕ) (x : BitVec w) :
                                  (0 >ₛ x) = true ↔ x.msb = true
                                  source
                                  theorem and_ule_not_xor (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  (~~~(x ^^^ y) ≥ᵤ x &&& y) = true
                                  source
                                  theorem xor_ule_or (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  (x ||| y ≥ᵤ x ^^^ y) = true
                                  source
                                  theorem ult_iff_not_ule (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  (y >ᵤ x) = true ↔ ¬(x ≥ᵤ y) = true
                                  source
                                  theorem sub_neg_sub (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  x - y = -(y - x)
                                  source
                                  theorem eq_iff_not_sub_or_sub (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  x = y ↔ (~~~(x - y ||| y - x)).msb = true
                                  source
                                  theorem lt_iff_sub_xor_xor_and_sub_xor (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                  (y >ₛ x) = true ↔ (x - y ^^^ (x ^^^ y) &&& (x - y ^^^ x)).msb = true