Documentation

Batteries.Data.ByteArray

source
theorem ByteArray.ext {x y : ByteArray} (data : x.data = y.data) :
x = y
source
instance ByteArray.instDecidableEq_batteries :
DecidableEq ByteArray
Equations
source
theorem ByteArray.getElem_eq_data_getElem {i : Nat} (a : ByteArray) (h : i < a.size) :
a[i] = a.data[i]

uget/uset #

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

empty #

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

push #

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

set #

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

copySlice #

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

append #

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

extract #

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

ofFn #

source
@[inline]
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_zero (f : Fin 0 → UInt8) :
    ofFn f = empty
    source
    theorem ByteArray.ofFn_succ {n : Nat} (f : Fin (n + 1) → UInt8) :
    ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f (Fin.last n))
    source
    @[simp]
    theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).data = Array.ofFn f
    source
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).size = n
    source
    @[simp]
    theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ofFn f).size) :
    (ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)
    source
    @[simp]
    theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ofFn f).size) :
    (ofFn f)[i] = f ⟨i, ⋯⟩

    map/mapM #

    source
    @[inline]
    unsafe def ByteArray.mapMUnsafe {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
    m ByteArray

    Unsafe optimized implementation of mapM.

    This function is unsafe because it relies on the implementation limit that the size of an array is always less than USize.size.

    Equations
    Instances For
      source
      @[specialize #[]]
      unsafe def ByteArray.mapMUnsafe.loop {m : Type → Type u_1} [Monad m] (f : UInt8 → m UInt8) (a : ByteArray) (k s : USize) :
      m ByteArray

      Inner loop for mapMUnsafe.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implemented_by ByteArray.mapMUnsafe]
        def ByteArray.mapM {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
        m ByteArray

        mapM f a applies the monadic function f to each element of the array.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[inline]
          def ByteArray.map (a : ByteArray) (f : UInt8 → UInt8) :
          ByteArray

          map f a applies the function f to each element of the array.

          Equations
          Instances For