Documentation

Init.Data.SInt.IntToBitVec

← Mathematical handbook

theorem ISize.toBitVec32_eq_toBitVec (a : ISize) (h : System.Platform.numBits = 32) :

a.toBitVec32 h = BitVec.cast h a.toBitVec

theorem ISize.toBitVec64_eq_toBitVec (a : ISize) (h : System.Platform.numBits = 64) :

a.toBitVec64 h = BitVec.cast h a.toBitVec

`numBits = 32` #

theorem ISize.le_iff_toBitVec32_sle {a b : ISize} (h : System.Platform.numBits = 32) :

a ≤ b ↔ (a.toBitVec32 h).sle (b.toBitVec32 h) = true

theorem ISize.lt_iff_toBitVec32_slt {a b : ISize} (h : System.Platform.numBits = 32) :

a < b ↔ (a.toBitVec32 h).slt (b.toBitVec32 h) = true

theorem ISize.eq_iff_toBitVec32_eq {a b : ISize} (h : System.Platform.numBits = 32) :

a = b ↔ a.toBitVec32 h = b.toBitVec32 h

theorem ISize.ne_iff_toBitVec32_ne {a b : ISize} (h : System.Platform.numBits = 32) :

a ≠ b ↔ a.toBitVec32 h ≠ b.toBitVec32 h

theorem ISize.toBitVec32_ofNat (h : System.Platform.numBits = 32) (n : Nat) :

(OfNat.ofNat n).toBitVec32 h = BitVec.ofNat 32 n

theorem ISize.toBitVec32_ofInt (i : Int) (h : System.Platform.numBits = 32) :

(ofInt i).toBitVec32 h = BitVec.ofInt 32 i

theorem ISize.toBitVec32_add {a b : ISize} (h : System.Platform.numBits = 32) :

(a + b).toBitVec32 h = a.toBitVec32 h + b.toBitVec32 h

theorem ISize.toBitVec32_sub {a b : ISize} (h : System.Platform.numBits = 32) :

(a - b).toBitVec32 h = a.toBitVec32 h - b.toBitVec32 h

theorem ISize.toBitVec32_mul {a b : ISize} (h : System.Platform.numBits = 32) :

(a * b).toBitVec32 h = a.toBitVec32 h * b.toBitVec32 h

theorem ISize.toBitVec32_div {a b : ISize} (h : System.Platform.numBits = 32) :

(a / b).toBitVec32 h = (a.toBitVec32 h).sdiv (b.toBitVec32 h)

theorem ISize.toBitVec32_mod {a b : ISize} (h : System.Platform.numBits = 32) :

(a % b).toBitVec32 h = (a.toBitVec32 h).srem (b.toBitVec32 h)

theorem ISize.toBitVec32_neg {a : ISize} (h : System.Platform.numBits = 32) :

(-a).toBitVec32 h = -a.toBitVec32 h

theorem ISize.toBitVec32_not {a : ISize} (h : System.Platform.numBits = 32) :

(~~~a).toBitVec32 h = ~~~a.toBitVec32 h

theorem ISize.toBitVec32_and (a b : ISize) (h : System.Platform.numBits = 32) :

(a &&& b).toBitVec32 h = a.toBitVec32 h &&& b.toBitVec32 h

theorem ISize.toBitVec32_or (a b : ISize) (h : System.Platform.numBits = 32) :

(a ||| b).toBitVec32 h = a.toBitVec32 h ||| b.toBitVec32 h

theorem ISize.toBitVec32_xor (a b : ISize) (h : System.Platform.numBits = 32) :

(a ^^^ b).toBitVec32 h = a.toBitVec32 h ^^^ b.toBitVec32 h

theorem ISize.toBitVec32_shiftLeft (a b : ISize) (h : System.Platform.numBits = 32) :

(a <<< b).toBitVec32 h = a.toBitVec32 h <<< (b.toBitVec32 h).smod 32

theorem ISize.toBitVec32_shiftRight (a b : ISize) (h : System.Platform.numBits = 32) :

(a >>> b).toBitVec32 h = (a.toBitVec32 h).sshiftRight' ((b.toBitVec32 h).smod 32)

theorem ISize.toBitVec32_abs (a : ISize) (h : System.Platform.numBits = 32) :

a.abs.toBitVec32 h = (a.toBitVec32 h).abs

theorem ISize.toBitVec32_toInt8 (n : ISize) (h : System.Platform.numBits = 32) :

n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt16 (n : ISize) (h : System.Platform.numBits = 32) :

n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt32 (n : ISize) (h : System.Platform.numBits = 32) :

n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt64 (n : ISize) (h : System.Platform.numBits = 32) :

n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec32 h)

theorem ISize.toBitVec32_toUSize (n : ISize) (h : System.Platform.numBits = 32) :

n.toUSize.toBitVec32 h = n.toBitVec32 h

theorem USize.toBitVec32_toISize (n : USize) (h : System.Platform.numBits = 32) :

n.toISize.toBitVec32 h = n.toBitVec32 h

theorem Int8.toBitVec32_toISize (n : Int8) (h : System.Platform.numBits = 32) :

n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int16.toBitVec32_toISize (n : Int16) (h : System.Platform.numBits = 32) :

n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int32.toBitVec32_toISize (n : Int32) (h : System.Platform.numBits = 32) :

n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int64.toBitVec32_toISize (n : Int64) (h : System.Platform.numBits = 32) :

n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem ISize.toBitVec32_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 32) :

(ofBitVec n).toBitVec32 h = BitVec.cast h n

theorem ISize.toBitVec32_minValue (h : System.Platform.numBits = 32) :

minValue.toBitVec32 h = BitVec.intMin 32

theorem ISize.toBitVec32_maxValue (h : System.Platform.numBits = 32) :

maxValue.toBitVec32 h = BitVec.intMax 32

theorem Bool.toBitVec32_toISize {b : Bool} (h : System.Platform.numBits = 32) :

b.toISize.toBitVec32 h = BitVec.setWidth 32 (BitVec.ofBool b)

`numBits = 64` #

theorem ISize.le_iff_toBitVec64_sle {a b : ISize} (h : System.Platform.numBits = 64) :

a ≤ b ↔ (a.toBitVec64 h).sle (b.toBitVec64 h) = true

theorem ISize.lt_iff_toBitVec64_slt {a b : ISize} (h : System.Platform.numBits = 64) :

a < b ↔ (a.toBitVec64 h).slt (b.toBitVec64 h) = true

theorem ISize.eq_iff_toBitVec64_eq {a b : ISize} (h : System.Platform.numBits = 64) :

a = b ↔ a.toBitVec64 h = b.toBitVec64 h

theorem ISize.ne_iff_toBitVec64_ne {a b : ISize} (h : System.Platform.numBits = 64) :

a ≠ b ↔ a.toBitVec64 h ≠ b.toBitVec64 h

theorem ISize.toBitVec64_ofNat (h : System.Platform.numBits = 64) (n : Nat) :

(OfNat.ofNat n).toBitVec64 h = BitVec.ofNat 64 n

theorem ISize.toBitVec64_ofInt (i : Int) (h : System.Platform.numBits = 64) :

(ofInt i).toBitVec64 h = BitVec.ofInt 64 i

theorem ISize.toBitVec64_add {a b : ISize} (h : System.Platform.numBits = 64) :

(a + b).toBitVec64 h = a.toBitVec64 h + b.toBitVec64 h

theorem ISize.toBitVec64_sub {a b : ISize} (h : System.Platform.numBits = 64) :

(a - b).toBitVec64 h = a.toBitVec64 h - b.toBitVec64 h

theorem ISize.toBitVec64_mul {a b : ISize} (h : System.Platform.numBits = 64) :

(a * b).toBitVec64 h = a.toBitVec64 h * b.toBitVec64 h

theorem ISize.toBitVec64_div {a b : ISize} (h : System.Platform.numBits = 64) :

(a / b).toBitVec64 h = (a.toBitVec64 h).sdiv (b.toBitVec64 h)

theorem ISize.toBitVec64_mod {a b : ISize} (h : System.Platform.numBits = 64) :

(a % b).toBitVec64 h = (a.toBitVec64 h).srem (b.toBitVec64 h)

theorem ISize.toBitVec64_neg {a : ISize} (h : System.Platform.numBits = 64) :

(-a).toBitVec64 h = -a.toBitVec64 h

theorem ISize.toBitVec64_not {a : ISize} (h : System.Platform.numBits = 64) :

(~~~a).toBitVec64 h = ~~~a.toBitVec64 h

theorem ISize.toBitVec64_and (a b : ISize) (h : System.Platform.numBits = 64) :

(a &&& b).toBitVec64 h = a.toBitVec64 h &&& b.toBitVec64 h

theorem ISize.toBitVec64_or (a b : ISize) (h : System.Platform.numBits = 64) :

(a ||| b).toBitVec64 h = a.toBitVec64 h ||| b.toBitVec64 h

theorem ISize.toBitVec64_xor (a b : ISize) (h : System.Platform.numBits = 64) :

(a ^^^ b).toBitVec64 h = a.toBitVec64 h ^^^ b.toBitVec64 h

theorem ISize.toBitVec64_shiftLeft (a b : ISize) (h : System.Platform.numBits = 64) :

(a <<< b).toBitVec64 h = a.toBitVec64 h <<< (b.toBitVec64 h).smod 64

theorem ISize.toBitVec64_shiftRight (a b : ISize) (h : System.Platform.numBits = 64) :

(a >>> b).toBitVec64 h = (a.toBitVec64 h).sshiftRight' ((b.toBitVec64 h).smod 64)

theorem ISize.toBitVec64_abs (a : ISize) (h : System.Platform.numBits = 64) :

a.abs.toBitVec64 h = (a.toBitVec64 h).abs

theorem ISize.toBitVec64_toInt8 (n : ISize) (h : System.Platform.numBits = 64) :

n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt16 (n : ISize) (h : System.Platform.numBits = 64) :

n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt32 (n : ISize) (h : System.Platform.numBits = 64) :

n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt64 (n : ISize) (h : System.Platform.numBits = 64) :

n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec64 h)

theorem ISize.toBitVec64_toUSize (n : ISize) (h : System.Platform.numBits = 64) :

n.toUSize.toBitVec64 h = n.toBitVec64 h

theorem USize.toBitVec64_toISize (n : USize) (h : System.Platform.numBits = 64) :

n.toISize.toBitVec64 h = n.toBitVec64 h

theorem Int8.toBitVec64_toISize (n : Int8) (h : System.Platform.numBits = 64) :

n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int16.toBitVec64_toISize (n : Int16) (h : System.Platform.numBits = 64) :

n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int32.toBitVec64_toISize (n : Int32) (h : System.Platform.numBits = 64) :

n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int64.toBitVec64_toISize (n : Int64) (h : System.Platform.numBits = 64) :

n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem ISize.toBitVec64_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 64) :

(ofBitVec n).toBitVec64 h = BitVec.cast h n

theorem ISize.toBitVec64_minValue (h : System.Platform.numBits = 64) :

minValue.toBitVec64 h = BitVec.intMin 64

theorem ISize.toBitVec64_maxValue (h : System.Platform.numBits = 64) :

maxValue.toBitVec64 h = BitVec.intMax 64

theorem Bool.toBitVec64_toISize {b : Bool} (h : System.Platform.numBits = 64) :

b.toISize.toBitVec64 h = BitVec.setWidth 64 (BitVec.ofBool b)