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]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]
        @[simp]

        All supported unary operators on BVExpr.

        • not: Std.Tactic.BVDecide.BVUnOp

          Bitwise not.

        • shiftLeftConst: NatStd.Tactic.BVDecide.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: NatStd.Tactic.BVDecide.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: NatStd.Tactic.BVDecide.BVUnOp

          Rotating left by a constant value.

        • rotateRight: NatStd.Tactic.BVDecide.BVUnOp

          Rotating right by a constant value.

        • arithShiftRightConst: NatStd.Tactic.BVDecide.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_rotateLeft {n : Nat} {w : Nat} :
            (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n
            @[simp]
            theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateRight {n : Nat} {w : Nat} :
            (Std.Tactic.BVDecide.BVUnOp.rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n

            All supported expressions involving BitVec and operations on them.

            Instances For
              Equations
              Instances For
                Equations
                • Std.Tactic.BVDecide.BVExpr.instToString = { toString := Std.Tactic.BVDecide.BVExpr.toString }

                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

                    The semantics for BVExpr.

                    Equations
                    Instances For

                      Supported binary predicates on BVExpr.

                      Instances For

                        The semantics for BVBinPred.

                        Equations
                        Instances For
                          @[simp]

                          Supported predicates on BVExpr.

                          Instances For

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

                            Instances For
                              Equations
                              Instances For
                                @[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