chore: docstring review for ByteArray

This PR adds missing docstrings for ByteArray and makes existing ones
consistent with our style.

Author: david-christiansen

src/Init/Data/ByteArray/Basic.lean

@@ -13,6 +13,8 @@ import all Init.Data.UInt.BasicAux
 public import Init.Data.Option.Basic
 public import Init.Data.Array.Extract
 
+set_option doc.verso true
+
 @[expose] public section
 universe u
 
@@ -34,18 +36,40 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
+/--
+Retrieves the size of the array as a platform-specific fixed-width integer.
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports,
+there are in practice no {name}`ByteArray`s that have more elements that {name}`USize` can count.
+-/
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index
+is represented by a platform-specific fixed-width integer (either 32 or 64 bits).
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports, there are
+in practice no {name}`ByteArray`s for which {name}`uget` cannot retrieve all elements.
+-/
 @[extern "lean_byte_array_uget"]
 def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
+/--
+Retrieves the byte at the indicated index. Panics if the index is out of bounds.
+-/
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs[i]!
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.
+
+Use {name}`uget` for a more efficient alternative or {name}`get!` for a variant that panics if the
+index is out of bounds.
+-/
 @[extern "lean_byte_array_fget"]
 def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, _ => bs[i]
@@ -56,34 +80,61 @@ instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
 instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
   getElem xs i h := xs.uget i h
 
+/--
+Replaces the byte at the given index.
+
+The array is modified in-place if there are no other references to it.
+
+If the index is out of bounds, the array is returned unmodified.
+-/
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
+/--
+Replaces the byte at the given index.
+
+No bounds check is performed, but the function requires a proof that the index is in bounds. This
+proof can usually be omitted, and will be synthesized automatically.
+
+The array is modified in-place if there are no other references to it.
+-/
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
-@[extern "lean_byte_array_uset"]
+@[extern "lean_byte_array_uset", inherit_doc ByteArray.set]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
+/--
+Computes a hash for a {name}`ByteArray`.
+-/
 @[extern "lean_byte_array_hash"]
 protected opaque hash (a : @& ByteArray) : UInt64
 
 instance : Hashable ByteArray where
   hash := ByteArray.hash
 
+/--
+Returns {name}`true` when {name}`s` contains zero bytes.
+-/
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 
 /--
-  Copy the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in `dest`, growing `dest` if necessary.
-  If `exact` is `false`, the capacity will be doubled when grown. -/
+Copies the slice at `[srcOff, srcOff + len)` in {name}`src` to `[destOff, destOff + len)` in
+{name}`dest`, growing {name}`dest` if necessary. If {name}`exact` is {name}`false`, the capacity
+will be doubled when grown.
+-/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
   ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
+/--
+Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to a new
+{name}`ByteArray`.
+-/
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
@@ -114,6 +165,9 @@ theorem append_eq {a b : ByteArray} : a.append b = a ++ b := rfl
 theorem fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b := by
   simp [← append_eq_fastAppend]
 
+/--
+Converts a packed array of bytes to a linked list.
+-/
 def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
@@ -124,32 +178,46 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+/--
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
+
+The index is returned along with a proof that it is a valid index in the array.
+-/
+@[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
   let rec @[specialize] loop (i : Nat) :=
     if h : i < a.size then
-      if p a[i] then some i else loop (i+1)
+      if p a[i] then some ⟨i, h⟩ else loop (i+1)
     else
       none
     termination_by a.size - i
     decreasing_by decreasing_trivial_pre_omega
   loop start
 
-@[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
+/--
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
+
+The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
+-/
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
   let rec @[specialize] loop (i : Nat) :=
     if h : i < a.size then
-      if p a[i] then some ⟨i, h⟩ else loop (i+1)
+      if p a[i] then some i else loop (i+1)
     else
       none
     termination_by a.size - i
     decreasing_by decreasing_trivial_pre_omega
   loop start
 
 /--
-  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
-  This is similar to the `Array` version.
+An efficient implementation of {name}`ForIn.forIn` for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
 
-  TODO: avoid code duplication in the future after we improve the compiler.
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
 -/
+-- TODO: avoid code duplication in the future after we improve the compiler.
 @[inline] unsafe def forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -162,7 +230,11 @@ def toList (bs : ByteArray) : List UInt8 :=
       pure b
   loop 0 b
 
-/-- Reference implementation for `forIn` -/
+/--
+The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
+
+In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
+-/
 @[implemented_by ByteArray.forInUnsafe]
 protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
@@ -180,7 +252,13 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/-- See comment at `forInUnsafe` -/
+/--
+An efficient implementation of a monadic left fold on for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
 -- TODO: avoid code duplication.
 @[inline]
 unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
@@ -197,7 +275,14 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/-- Reference implementation for `foldlM` -/
+/--
+A monadic left fold on {name}`ByteArray` that iterates over an array from low to high indices,
+computing a running value.
+
+Each element of the array is combined with the value from the prior elements using a monadic
+function {name}`f`. The initial value {name}`init` is the starting value before any elements have
+been processed.
+-/
 @[implemented_by foldlMUnsafe]
 def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
   let fold (stop : Nat) (h : stop ≤ as.size) :=
@@ -215,11 +300,23 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
   else
     fold as.size (Nat.le_refl _)
 
+/--
+A left fold on {name}`ByteArray` that iterates over an array from low to high indices, computing a
+running value.
+
+Each element of the array is combined with the value from the prior elements using a function
+{name}`f`. The initial value {name}`init` is the starting value before any elements have been
+processed.
+
+{name}`ByteArray.foldlM` is a monadic variant of this function.
+-/
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
   Id.run <| as.foldlM (pure <| f · ·) init start stop
 
-/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
+set_option doc.verso false -- Awaiting intra-module forward reference support
+/--
+Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -243,6 +340,7 @@ structure Iterator where
   current byte is `(default : UInt8)`. -/
   idx : Nat
   deriving Inhabited
+set_option doc.verso true
 
 /-- Creates an iterator at the beginning of an array. -/
 def mkIterator (arr : ByteArray) : Iterator :=
@@ -260,16 +358,25 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/-- Number of bytes remaining in the iterator. -/
+/--
+The number of bytes remaining in the iterator.
+-/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- The byte at the current position.
+/-- True if the iterator is past the array's last byte. -/
+@[inline]
+def atEnd : Iterator → Bool
+  | ⟨arr, i⟩ => i ≥ arr.size
 
-On an invalid position, returns `(default : UInt8)`. -/
+/--
+The byte at the current position.
+
+On an invalid position, returns {lean}`(default : UInt8)`.
+-/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -278,27 +385,28 @@ def curr : Iterator → UInt8
     else
       default
 
-/-- Moves the iterator's position forward by one byte, unconditionally.
+/--
+Moves the iterator's position forward by one byte, unconditionally.
 
 It is only valid to call this function if the iterator is not at the end of the array, *i.e.*
-`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
+{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
+-/
 @[inline]
 def next : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i + 1⟩
 
-/-- Decreases the iterator's position.
+/--
+Decreases the iterator's position.
 
-If the position is zero, this function is the identity. -/
+If the position is zero, this function is the identity.
+-/
 @[inline]
 def prev : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i - 1⟩
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
-
-/-- True if the iterator is not past the array's last byte. -/
+/--
+True if the iterator is valid; that is, it is not past the array's last byte.
+-/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -324,27 +432,33 @@ def next' (it : Iterator) (_h : it.hasNext) : Iterator :=
 def hasPrev : Iterator → Bool
   | ⟨_, i⟩ => i > 0
 
-/-- Moves the iterator's position to the end of the array.
+/--
+Moves the iterator's position to the end of the array.
 
-Note that `i.toEnd.atEnd` is always `true`. -/
+Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
+-/
 @[inline]
 def toEnd : Iterator → Iterator
   | ⟨arr, _⟩ => ⟨arr, arr.size⟩
 
-/-- Moves the iterator's position several bytes forward.
+/--
+Moves the iterator's position several bytes forward.
 
 The resulting iterator is only valid if the number of bytes to skip is less than or equal to
-the number of bytes left in the iterator. -/
+the number of bytes left in the iterator.
+-/
 @[inline]
 def forward : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i + f⟩
 
 @[inherit_doc forward, inline]
 def nextn : Iterator → Nat → Iterator := forward
 
-/-- Moves the iterator's position several bytes back.
+/--
+Moves the iterator's position several bytes back.
 
-If asked to go back more bytes than available, stops at the beginning of the array. -/
+If asked to go back more bytes than available, stops at the beginning of the array.
+-/
 @[inline]
 def prevn : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i - f⟩

src/Init/Data/ByteArray/Bootstrap.lean

@@ -10,12 +10,19 @@ public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section
+set_option doc.verso true
 
 namespace ByteArray
 
 @[simp]
 theorem data_push {a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b := rfl
 
+/--
+Appends two byte arrays.
+
+In compiled code, calls to {name}`ByteArray.append` are replaced with the much more efficient
+{name (scope:="Init.Data.ByteArray.Basic")}`ByteArray.fastAppend`.
+-/
 @[expose]
 protected def append (a b : ByteArray) : ByteArray :=
   ⟨⟨a.data.toList ++ b.data.toList⟩⟩