Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Basic

This module contains the definition of the BitVec fragment that bv_decide internally operates on as BVLogicalExpr. The preprocessing steps of bv_decide reduce all supported BitVec operations to the ones provided in this file. For verification purposes BVLogicalExpr.Sat and BVLogicalExpr.Unsat are provided.

The variable definition used by the bitblaster.

  • w : Nat

    The width of the BitVec variable.

  • var : Nat

    A numeric identifier for the BitVec variable.

  • idx : Fin self.w

    The bit that we take out of the BitVec variable by getLsb.

Instances For

    All supported binary operations on BVExpr.

    Instances For

      The semantics for BVBinOp.

      Equations
      Instances For
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_and {w : Nat} :
        and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_or {w : Nat} :
        or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_xor {w : Nat} :
        xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_add {w : Nat} :
        add.eval = fun (x1 x2 : BitVec w) => x1 + x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_mul {w : Nat} :
        mul.eval = fun (x1 x2 : BitVec w) => x1 * x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_udiv {w : Nat} :
        udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2
        @[simp]
        theorem Std.Tactic.BVDecide.BVBinOp.eval_umod {w : Nat} :
        umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

        All supported unary operators on BVExpr.

        • not : BVUnOp

          Bitwise not.

        • shiftLeftConst (n : Nat) : BVUnOp

          Shifting left by a constant value.

          This operation has a dedicated constant representation as shiftLeft can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

        • shiftRightConst (n : Nat) : BVUnOp

          Shifting right by a constant value.

          This operation has a dedicated constant representation as shiftRight can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

        • rotateLeft (n : Nat) : BVUnOp

          Rotating left by a constant value.

        • rotateRight (n : Nat) : BVUnOp

          Rotating right by a constant value.

        • arithShiftRightConst (n : Nat) : BVUnOp

          Arithmetic shift right by a constant value.

          This operation has a dedicated constant representation as shiftRight can take Nat as a shift amount. We can obviously not bitblast a Nat but still want to support the case where the user shifts by a constant Nat value.

        Instances For

          The semantics for BVUnOp.

          Equations
          Instances For
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_not {w : Nat} :
            not.eval = fun (x : BitVec w) => ~~~x
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftLeftConst {n w : Nat} :
            (shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftRightConst {n w : Nat} :
            (shiftRightConst n).eval = fun (x : BitVec w) => x >>> n
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft {n w : Nat} :
            (rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateRight {n w : Nat} :
            (rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_arithShiftRightConst {n w : Nat} :
            (arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n

            All supported expressions involving BitVec and operations on them.

            Instances For
              Equations
              Instances For

                Pack a BitVec with its width into a single parameter-less structure.

                Instances For
                  @[reducible, inline]

                  The notion of variable assignments for BVExpr.

                  Equations
                  Instances For

                    Get the value of a BVExpr.var from an Assignment.

                    Equations
                    Instances For

                      The semantics for BVExpr.

                      Equations
                      Instances For
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_var {assign : Assignment} {w idx : Nat} :
                        eval assign (var idx) = BitVec.truncate w (assign.get idx).bv
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_const {assign : Assignment} {w✝ : Nat} {val : BitVec w✝} :
                        eval assign (const val) = val
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_zeroExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} :
                        eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_extract {assign : Assignment} {start len a✝ : Nat} {expr : BVExpr a✝} :
                        eval assign (extract start len expr) = BitVec.extractLsb' start len (eval assign expr)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_bin {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinOp} {rhs : BVExpr a✝} :
                        eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_un {assign : Assignment} {op : BVUnOp} {a✝ : Nat} {operand : BVExpr a✝} :
                        eval assign (un op operand) = op.eval (eval assign operand)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_append {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
                        eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_replicate {assign : Assignment} {n a✝ : Nat} {expr : BVExpr a✝} :
                        eval assign (replicate n expr) = BitVec.replicate n (eval assign expr)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_signExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} :
                        eval assign (signExtend v expr) = BitVec.signExtend v (eval assign expr)
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_shiftLeft {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
                        eval assign (lhs.shiftLeft rhs) = eval assign lhs <<< eval assign rhs
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_shiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
                        eval assign (lhs.shiftRight rhs) = eval assign lhs >>> eval assign rhs
                        @[simp]
                        theorem Std.Tactic.BVDecide.BVExpr.eval_arithShiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
                        eval assign (lhs.arithShiftRight rhs) = (eval assign lhs).sshiftRight' (eval assign rhs)

                        Supported binary predicates on BVExpr.

                        Instances For

                          The semantics for BVBinPred.

                          Equations
                          Instances For
                            @[simp]
                            theorem Std.Tactic.BVDecide.BVBinPred.eval_eq {w : Nat} :
                            eq.eval = fun (x1 x2 : BitVec w) => x1 == x2

                            Supported predicates on BVExpr.

                            Instances For

                              Pack two BVExpr of equivalent width into one parameter-less structure.

                              Instances For
                                Equations
                                Instances For
                                  @[simp]
                                  theorem Std.Tactic.BVDecide.BVPred.eval_bin {assign : BVExpr.Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinPred} {rhs : BVExpr a✝} :
                                  eval assign (bin lhs op rhs) = op.eval (BVExpr.eval assign lhs) (BVExpr.eval assign rhs)
                                  @[simp]
                                  theorem Std.Tactic.BVDecide.BVPred.eval_getLsbD {assign : BVExpr.Assignment} {a✝ : Nat} {expr : BVExpr a✝} {idx : Nat} :
                                  eval assign (getLsbD expr idx) = (BVExpr.eval assign expr).getLsbD idx
                                  @[reducible, inline]

                                  Boolean substructure of problems involving predicates on BitVec as atoms.

                                  Equations
                                  Instances For

                                    The semantics of boolean problems involving BitVec predicates as atoms.

                                    Equations
                                    Instances For
                                      @[simp]
                                      @[simp]
                                      theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_gate {assign : BVExpr.Assignment} {g : Gate} {x y : BoolExpr BVPred} :
                                      eval assign (BoolExpr.gate g x y) = g.eval (eval assign x) (eval assign y)
                                      @[simp]
                                      theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_ite {assign : BVExpr.Assignment} {d l r : BoolExpr BVPred} :
                                      eval assign (d.ite l r) = bif eval assign d then eval assign l else eval assign r
                                      theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_and {x y : BVLogicalExpr} {assign : BVExpr.Assignment} (hx : x.Sat assign) (hy : y.Sat assign) :