Documentation

Std.Data.ByteArray

source
theorem ByteArray.ext {a : ByteArray} {b : ByteArray} :
a.data = b.data → a = b
source
theorem ByteArray.getElem_eq_data_getElem {i : Nat} (a : ByteArray) (h : i < ByteArray.size a) :
a[i] = a.data[i]

uget/uset #

source
@[simp]
theorem ByteArray.ugetElem_eq_getElem (a : ByteArray) {i : USize} (h : USize.toNat i < ByteArray.size a) :
a[i] = a[USize.toNat i]
source
@[simp]
theorem ByteArray.uset_eq_set (a : ByteArray) {i : USize} (h : USize.toNat i < ByteArray.size a) (v : UInt8) :
ByteArray.uset a i v h = ByteArray.set a { val := USize.toNat i, isLt := h } v

empty #

source
@[simp]
theorem ByteArray.mkEmpty_data (cap : Nat) :
(ByteArray.mkEmpty cap).data = #[]
source
@[simp]
theorem ByteArray.empty_data :
ByteArray.empty.data = #[]
source
@[simp]
theorem ByteArray.size_empty :
ByteArray.size ByteArray.empty = 0

push #

source
@[simp]
theorem ByteArray.push_data (a : ByteArray) (b : UInt8) :
(ByteArray.push a b).data = Array.push a.data b
source
@[simp]
theorem ByteArray.size_push (a : ByteArray) (b : UInt8) :
ByteArray.size (ByteArray.push a b) = ByteArray.size a + 1
source
@[simp]
theorem ByteArray.get_push_eq (a : ByteArray) (x : UInt8) :
(ByteArray.push a x)[ByteArray.size a] = x
source
theorem ByteArray.get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < ByteArray.size a) :
(ByteArray.push a x)[i] = a[i]

set #

source
@[simp]
theorem ByteArray.set_data (a : ByteArray) (i : Fin (ByteArray.size a)) (v : UInt8) :
(ByteArray.set a i v).data = Array.set a.data i v
source
@[simp]
theorem ByteArray.size_set (a : ByteArray) (i : Fin (ByteArray.size a)) (v : UInt8) :
ByteArray.size (ByteArray.set a i v) = ByteArray.size a
source
@[simp]
theorem ByteArray.get_set_eq (a : ByteArray) (i : Fin (ByteArray.size a)) (v : UInt8) :
(ByteArray.set a i v)[↑i] = v
source
theorem ByteArray.get_set_ne {j : Nat} (a : ByteArray) (i : Fin (ByteArray.size a)) (v : UInt8) (hj : j < ByteArray.size a) (h : ↑i ≠ j) :
(ByteArray.set a i v)[j] = a[j]
source
theorem ByteArray.set_set (a : ByteArray) (i : Fin (ByteArray.size a)) (v : UInt8) (v' : UInt8) :
ByteArray.set (ByteArray.set a i v) { val := ↑i, isLt := ⋯ } v' = ByteArray.set a i v'

copySlice #

source
@[simp]
theorem ByteArray.copySlice_data (a : ByteArray) (i : Nat) (b : ByteArray) (j : Nat) (len : Nat) (exact : Bool) :
(ByteArray.copySlice a i b j len exact).data = Array.extract b.data 0 j ++ Array.extract a.data i (i + len) ++ Array.extract b.data (j + min len (Array.size a.data - i)) (Array.size b.data)

append #

source
@[simp]
theorem ByteArray.append_eq (a : ByteArray) (b : ByteArray) :
ByteArray.append a b = a ++ b
source
@[simp]
theorem ByteArray.append_data (a : ByteArray) (b : ByteArray) :
(a ++ b).data = a.data ++ b.data
source
theorem ByteArray.size_append (a : ByteArray) (b : ByteArray) :
ByteArray.size (a ++ b) = ByteArray.size a + ByteArray.size b
source
theorem ByteArray.get_append_left {i : Nat} {a : ByteArray} {b : ByteArray} (hlt : i < ByteArray.size a) (h : optParam (i < ByteArray.size (a ++ b)) ⋯) :
(a ++ b)[i] = a[i]
source
theorem ByteArray.get_append_right {i : Nat} {a : ByteArray} {b : ByteArray} (hle : ByteArray.size a ≤ i) (h : i < ByteArray.size (a ++ b)) (h' : optParam (i - ByteArray.size a < ByteArray.size b) ⋯) :
(a ++ b)[i] = b[i - ByteArray.size a]

extract #

source
@[simp]
theorem ByteArray.extract_data (a : ByteArray) (start : Nat) (stop : Nat) :
(ByteArray.extract a start stop).data = Array.extract a.data start stop
source
@[simp]
theorem ByteArray.size_extract (a : ByteArray) (start : Nat) (stop : Nat) :
ByteArray.size (ByteArray.extract a start stop) = min stop (ByteArray.size a) - start
source
theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start : Nat} {stop : Nat} (h : i < ByteArray.size (ByteArray.extract a start stop)) :
start + i < ByteArray.size a
source
@[simp]
theorem ByteArray.get_extract {i : Nat} {a : ByteArray} {start : Nat} {stop : Nat} (h : i < ByteArray.size (ByteArray.extract a start stop)) :
(ByteArray.extract a start stop)[i] = a[start + i]

ofFn #

source
def ByteArray.ofFn {n : Nat} (f : Fin n → UInt8) :
ByteArray
  • ofFn f with f : Fin n → UInt8 returns the byte array whose ith element is f i. -
Equations
Instances For
    source
    @[simp]
    theorem ByteArray.ofFn_data {n : Nat} (f : Fin n → UInt8) :
    (ByteArray.ofFn f).data = Array.ofFn f
    source
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    ByteArray.size (ByteArray.ofFn f) = n
    source
    @[simp]
    theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ByteArray.size (ByteArray.ofFn f))) :
    ByteArray.get (ByteArray.ofFn f) i = f (Fin.cast ⋯ i)
    source
    @[simp]
    theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < ByteArray.size (ByteArray.ofFn f)) :
    (ByteArray.ofFn f)[i] = f { val := i, isLt := ⋯ }