Documentation

Projects.Util.UInt8

def UInt8.ofBit (b : Bit) :

Equations

UInt8.ofBit Bit.B₀ = 0
UInt8.ofBit Bit.B₁ = 1

Instances For

def UInt8.lowestBit (x : UInt8) :

Equations

x.lowestBit = Bit.ofBool (decide (Odd x.toNat))

Instances For

def UInt8.ofBits (bs : List Bit) :

Equations

UInt8.ofBits bs = List.foldr (fun (bit : Bit) (x : UInt8) => x <<< 1 ||| UInt8.ofBit bit) 0 bs

Instances For

def UInt8.toBits (x : UInt8) :

Equations

x.toBits = List.map (fun (n : ℕ) => (x >>> UInt8.ofNat n).lowestBit) (List.range 8)

Instances For

@[simp]

theorem UInt8.mk_eq_mk_iff {x y : BitVec 8} :

{ toBitVec := x } = { toBitVec := y } ↔ x = y

theorem UInt8.eq_iff_mk {x y : UInt8} :

x = y ↔ x.toBitVec = y.toBitVec

@[simp]

theorem UInt8.ofNatLT_eq_ofNatLT_iff {n m : ℕ} {hn : n < size} {hm : m < size} :

ofNatLT n hn = ofNatLT m hm ↔ n = m

@[simp]

theorem UInt8.ofBit_eq_mk {b : Bit} :

ofBit b = { toBitVec := BitVec.ofBit 8 b }

@[simp]

theorem UInt8.lowestBit_mk {x : BitVec 8} :

{ toBitVec := x }.lowestBit = x.lowestBit

theorem UInt8.or_eq_mk {x y : UInt8} :

x ||| y = { toBitVec := x.toBitVec ||| y.toBitVec }

@[simp]

theorem UInt8.ofBits_eq_mk {bs : List Bit} :

ofBits bs = { toBitVec := BitVec.ofBits 8 bs }

@[simp]

theorem UInt8.toBitVec_eq_iff {x y : UInt8} :

x.toBitVec = y.toBitVec ↔ x = y

@[simp]

theorem UInt8.toBits_eq_mk {x : UInt8} :

x.toBits = x.toBitVec.toBits

@[simp]

theorem UInt8.one_shl_one :

1 <<< 1 = 2

@[instance_reducible]

instance UInt8.instLinearOrder_projects :

LinearOrder UInt8

Equations

UInt8.instLinearOrder_projects = { toLE := instLEUInt8, toLT := instLTUInt8, le_refl := @UInt8.instLinearOrder_projects._proof_1, le_trans := @UInt8.instLinearOrder_projects._proof_2, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, toMin := instMinUInt8, toMax := instMaxUInt8, toOrd := UInt8.instOrd, le_total := ⋯, toDecidableLE := fun {x y : UInt8} => inferInstance, toDecidableEq := decidableEqOfDecidableLE, toDecidableLT := decidableLTOfDecidableLE, min_def := @UInt8.instLinearOrder_projects._proof_3, max_def := @UInt8.instLinearOrder_projects._proof_4, compare_eq_compareOfLessAndEq := UInt8.instLinearOrder_projects._proof_5 }

@[simp]

theorem UInt8.ofBits_snoc {bs : List Bit} {b : Bit} :

ofBits (bs ++ [b]) = ofBits bs ||| if bs.length < 8 then ofBit b <<< ofNat bs.length else 0

@[simp]

theorem UInt8.ofNat_eq_zero_iff {n : ℕ} :

ofNat n = 0 ↔ n % 256 = 0

@[simp]

theorem UInt8.ofNat_eq_one_iff {n : ℕ} :

ofNat n = 1 ↔ n % 256 = 1

@[simp]

theorem UInt8.one_shiftLeft_ne_zero {n : ℕ} :

1 <<< ofNat n ≠ 0

@[simp]

theorem UInt8.one_shiftLeft_eq_one_iff {n : ℕ} :

1 <<< ofNat n = 1 ↔ n % 8 = 0

@[simp]

theorem UInt8.one_shiftLeft_eq_one_iff' {x : UInt8} :

1 <<< x = 1 ↔ x.toNat % 8 = 0