diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c9b789dddf0e..31b0e8e24f17 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3011,6 +3011,12 @@ theorem toNat_shiftLeft_or_toNat_lt_two_pow_add {m n : Nat} (x : BitVec m) (y : ext simp [getElem_append] +theorem cast_append (h : w = w') (x : BitVec w) (y : BitVec v) : + x.cast h ++ y = (x ++ y).cast (by rw [h]) := by simp + +theorem append_cast (h : v = v') (x : BitVec w) (y : BitVec v) : + x ++ y.cast h = (x ++ y).cast (by rw [h]) := by simp + theorem setWidth_append {x : BitVec w} {y : BitVec v} : (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by ext i h diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 34e5950de2ea..e01cb3ac05ce 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -9,6 +9,7 @@ prelude import all Init.Data.UInt.BasicAux public import Init.Data.Array.DecidableEq public import Init.Data.List.Attach +public import Init.Data.BitVec.Basic import Init.Data.Array.Bootstrap import Init.Data.Array.Lemmas import Init.Omega @@ -20,13 +21,6 @@ universe u namespace ByteArray -@[extern "lean_sarray_dec_eq"] -def beq (lhs rhs : @& ByteArray) : Bool := - lhs.data == rhs.data - -instance : BEq ByteArray where - beq := beq - attribute [ext] ByteArray @[extern "lean_sarray_dec_eq"] @@ -133,7 +127,7 @@ Copies the slice at `[srcOff, srcOff + len)` in {name}`src` to `[destOff, destOf 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 := +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⟩ /-- @@ -326,6 +320,224 @@ processed. def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β := Id.run <| as.foldlM (pure <| f · ·) init start stop +/-- +Extracts {name}`nbytes` bytes out of {lean}`bs` starting at index {lean}`i` as a bitvector in +little-endian byte order. +-/ +def getBitVecLE (bs : ByteArray) (i : Nat) (nbytes : Nat) + (h : i + nbytes ≤ bs.size := by get_elem_tactic) : BitVec (8 * nbytes) := + go 0 (Nat.zero_le _) 0#0 +where + go (k : Nat) (hk : k ≤ nbytes) (acc : BitVec (8 * k)) : BitVec (8 * nbytes) := + if h : k < nbytes then + let b := bs[i + k] + go (k + 1) h ((b.toBitVec ++ acc).cast (by omega)) + else + acc.cast (by omega) + +/-- +Extracts {name}`nbytes` bytes out of {lean}`bs` starting at index {lean}`i` as a bitvector in +big-endian byte order. +-/ +def getBitVecBE (bs : ByteArray) (i : Nat) (nbytes : Nat) + (h : i + nbytes ≤ bs.size := by get_elem_tactic) : BitVec (8 * nbytes) := + go 0 (Nat.zero_le _) 0#0 +where + go (k : Nat) (hk : k ≤ nbytes) (acc : BitVec (8 * k)) : BitVec (8 * nbytes) := + if h : k < nbytes then + let b := bs[i + k] + go (k + 1) h ((acc ++ b.toBitVec).cast (by omega)) + else + acc.cast (by omega) + +/-- Writes {name}`val` into {lean}`bs` starting at index {lean}`i` in little-endian byte order. -/ +def setBitVecLE (bs : ByteArray) (i : Nat) (nbytes : Nat) (val : BitVec (8 * nbytes)) + (h : i + nbytes ≤ bs.size := by get_elem_tactic) : ByteArray := + go 0 (Nat.zero_le _) bs h +where + go (k : Nat) (hk : k ≤ nbytes) (acc : ByteArray) (h : i + nbytes ≤ acc.size) : ByteArray := + if h : k < nbytes then + let acc := acc.set (i + k) ⟨val.extractLsb' (8 * k) 8⟩ (by clear ‹_ ≤ bs.size› bs; omega) + go (k + 1) h acc (by simpa [acc, set, ← size_data]) + else + acc + +/-- Writes {name}`val` into {lean}`bs` starting at index {lean}`i` in big-endian byte order. -/ +def setBitVecBE (bs : ByteArray) (i : Nat) (nbytes : Nat) (val : BitVec (8 * nbytes)) + (h : i + nbytes ≤ bs.size := by get_elem_tactic) : ByteArray := + go 0 (Nat.zero_le _) bs h +where + go (k : Nat) (hk : k ≤ nbytes) (acc : ByteArray) (h : i + nbytes ≤ acc.size) : ByteArray := + if h : k < nbytes then + let acc := acc.set (i + k) ⟨val.extractLsb' (8 * (nbytes - k - 1)) 8⟩ + (by clear ‹_ ≤ bs.size› bs; omega) + go (k + 1) h acc (by simpa [acc, set, ← size_data]) + else + acc + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 16 bit little-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint16_le", simp] +def getUInt16LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + UInt16.ofBitVec (getBitVecLE bs i 2 h) + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 16 bit big-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint16_be", simp] +def getUInt16BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + UInt16.ofBitVec (getBitVecBE bs i 2 h) + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 32 bit little-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint32_le", simp] +def getUInt32LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + UInt32.ofBitVec (getBitVecLE bs i 4 h) + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 32 bit big-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint32_be", simp] +def getUInt32BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + UInt32.ofBitVec (getBitVecBE bs i 4 h) + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 64 bit little-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint64_le", simp] +def getUInt64LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + UInt64.ofBitVec (getBitVecLE bs i 8 h) + +/-- +Interprets the value in the byte array {name}`bs` starting at index {name}`i` +as a 64 bit big-endian unsigned integer. +-/ +@[extern "lean_byte_array_fget_uint64_be", simp] +def getUInt64BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + UInt64.ofBitVec (getBitVecBE bs i 8 h) + +/-- Writes the value into the byte array starting at index {name}`i` in little-endian byte order. -/ +@[extern "lean_byte_array_fset_uint16_le", simp] +def setUInt16LE (bs : ByteArray) (i : @& Nat) (val : UInt16) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecLE i 2 val.toBitVec + +/-- Writes the value into the byte array starting at index {name}`i` in big-endian byte order. -/ +@[extern "lean_byte_array_fset_uint16_be", simp] +def setUInt16BE (bs : ByteArray) (i : @& Nat) (val : UInt16) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecBE i 2 val.toBitVec + +/-- Writes the value into the byte array starting at index {name}`i` in little-endian byte order. -/ +@[extern "lean_byte_array_fset_uint32_le", simp] +def setUInt32LE (bs : ByteArray) (i : @& Nat) (val : UInt32) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecLE i 4 val.toBitVec + +/-- Writes the value into the byte array starting at index {name}`i` in big-endian byte order. -/ +@[extern "lean_byte_array_fset_uint32_be", simp] +def setUInt32BE (bs : ByteArray) (i : @& Nat) (val : UInt32) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecBE i 4 val.toBitVec + +/-- Writes the value into the byte array starting at index {name}`i` in little-endian byte order. -/ +@[extern "lean_byte_array_fset_uint64_le", simp] +def setUInt64LE (bs : ByteArray) (i : @& Nat) (val : UInt64) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecLE i 8 val.toBitVec + +/-- Writes the value into the byte array starting at index {name}`i` in big-endian byte order. -/ +@[extern "lean_byte_array_fset_uint64_be", simp] +def setUInt64BE (bs : ByteArray) (i : @& Nat) (val : UInt64) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + bs.setBitVecBE i 8 val.toBitVec + +def getBitVecLE! (bs : ByteArray) (i : Nat) (nbytes : Nat) : BitVec (8 * nbytes) := + if h : _ then bs.getBitVecLE i nbytes h else outOfBounds + +def getBitVecBE! (bs : ByteArray) (i : Nat) (nbytes : Nat) : BitVec (8 * nbytes) := + if h : _ then bs.getBitVecBE i nbytes h else outOfBounds + +def getUInt16LE! (bs : ByteArray) (i : Nat) : UInt16 := + if h : _ then bs.getUInt16LE i h else outOfBounds + +def getUInt16BE! (bs : ByteArray) (i : Nat) : UInt16 := + if h : _ then bs.getUInt16BE i h else outOfBounds + +def getUInt32LE! (bs : ByteArray) (i : Nat) : UInt32 := + if h : _ then bs.getUInt32LE i h else outOfBounds + +def getUInt32BE! (bs : ByteArray) (i : Nat) : UInt32 := + if h : _ then bs.getUInt32BE i h else outOfBounds + +def getUInt64LE! (bs : ByteArray) (i : Nat) : UInt64 := + if h : _ then bs.getUInt64LE i h else outOfBounds + +def getUInt64BE! (bs : ByteArray) (i : Nat) : UInt64 := + if h : _ then bs.getUInt64BE i h else outOfBounds + +def setBitVecLE! (bs : ByteArray) (i : Nat) (nbytes : Nat) (val : BitVec (8 * nbytes)) : ByteArray := + if h : _ then bs.setBitVecLE i nbytes val h else @outOfBounds _ ⟨bs⟩ + +def setBitVecBE! (bs : ByteArray) (i : Nat) (nbytes : Nat) (val : BitVec (8 * nbytes)) : ByteArray := + if h : _ then bs.setBitVecBE i nbytes val h else @outOfBounds _ ⟨bs⟩ + +def setUInt16LE! (bs : ByteArray) (i : Nat) (val : UInt16) : ByteArray := + if h : _ then bs.setUInt16LE i val h else @outOfBounds _ ⟨bs⟩ + +def setUInt16BE! (bs : ByteArray) (i : Nat) (val : UInt16) : ByteArray := + if h : _ then bs.setUInt16BE i val h else @outOfBounds _ ⟨bs⟩ + +def setUInt32LE! (bs : ByteArray) (i : Nat) (val : UInt32) : ByteArray := + if h : _ then bs.setUInt32LE i val h else @outOfBounds _ ⟨bs⟩ + +def setUInt32BE! (bs : ByteArray) (i : Nat) (val : UInt32) : ByteArray := + if h : _ then bs.setUInt32BE i val h else @outOfBounds _ ⟨bs⟩ + +def setUInt64LE! (bs : ByteArray) (i : Nat) (val : UInt64) : ByteArray := + if h : _ then bs.setUInt64LE i val h else @outOfBounds _ ⟨bs⟩ + +def setUInt64BE! (bs : ByteArray) (i : Nat) (val : UInt64) : ByteArray := + if h : _ then bs.setUInt64BE i val h else @outOfBounds _ ⟨bs⟩ + +/-- +Replaces the bytes in the range `[start, start + size)` within {name}`bs` with {name}`val`. +-/ +@[extern "lean_byte_array_fill"] +def fill (bs : ByteArray) (start size : @& Nat) (val : UInt8) + (h : start + size ≤ bs.size := by get_elem_tactic) : ByteArray := + (mk (Array.replicate size val)).copySlice 0 bs start size + +/-- +Returns true if and only if the bytes `[asOff, asOff + len)` in {name}`as` and +`[bsOff, bsOff + len)` in {name}`bs` contain the same data. +-/ +@[extern "lean_byte_array_slice_eq"] +def sliceEq' (as : @& ByteArray) (asOff : @& Nat) (bs : @& ByteArray) (bsOff len : @& Nat) + (h : asOff + len ≤ as.size := by get_elem_tactic) + (h' : bsOff + len ≤ bs.size := by get_elem_tactic) : Bool := + as.data.extract asOff (asOff + len) == bs.data.extract bsOff (bsOff + len) + +/-- +Returns true if and only if the slices `[asOff, asOff + len)` in {name}`as` and +`[bsOff, bsOff + len)` in {name}`bs` exist and contain the same data. +-/ +def sliceEq (as : ByteArray) (asOff : Nat) (bs : ByteArray) (bsOff : Nat) (len : Nat) : Bool := + ∃ h h', sliceEq' as asOff bs bsOff len h h' + set_option doc.verso false -- Awaiting intra-module forward reference support /-- Iterator over the bytes (`UInt8`) of a `ByteArray`. diff --git a/src/Init/Data/ByteArray/BootstrapLemmas.lean b/src/Init/Data/ByteArray/BootstrapLemmas.lean new file mode 100644 index 000000000000..3253a21dbaf8 --- /dev/null +++ b/src/Init/Data/ByteArray/BootstrapLemmas.lean @@ -0,0 +1,265 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Markus Himmel +-/ +module + +prelude +public import Init.Data.ByteArray.Basic +import Init.ByCases +import Init.Data.Array.Bootstrap +import Init.Data.Array.Extract +import Init.Data.Array.Lemmas +import Init.Omega + +public section + +namespace ByteArray + +-- At present the preferred normal form for empty byte arrays is `ByteArray.empty` +@[simp] +theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl + +@[simp] +theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl + +@[simp] +theorem data_empty : ByteArray.empty.data = #[] := rfl + +@[simp] +theorem data_extract {a : ByteArray} {b e : Nat} : + (a.extract b e).data = a.data.extract b e := by + simp [extract, copySlice] + by_cases b ≤ e + · rw [(by omega : b + (e - b) = e)] + · rw [Array.extract_eq_empty_of_le (by omega), Array.extract_eq_empty_of_le (by omega)] + +@[simp] +theorem extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by + ext1 + simp + +@[simp] +theorem extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by + ext1 + simp [Nat.min_le_left] + +theorem fastAppend_eq_copySlice {a b : ByteArray} : + a.fastAppend b = b.copySlice 0 a a.size b.size false := rfl + +@[simp] +theorem _root_.List.toByteArray_append {l l' : List UInt8} : + (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray := by + simp [List.toByteArray_append'] + +@[simp] +theorem toList_data_append {l l' : ByteArray} : + (l ++ l').data.toList = l.data.toList ++ l'.data.toList := by + simp [← append_eq] + +@[simp] +theorem data_append {l l' : ByteArray} : + (l ++ l').data = l.data ++ l'.data := by + simp [← Array.toList_inj] + +@[simp] +theorem size_empty : ByteArray.empty.size = 0 := by + simp [← ByteArray.size_data] + +@[simp] +theorem _root_.List.data_toByteArray {l : List UInt8} : + l.toByteArray.data = l.toArray := by + rw [List.toByteArray] + suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by + simpa using this l ByteArray.empty + intro a b + fun_induction List.toByteArray.loop a b with simp_all + +@[simp] +theorem _root_.List.size_toByteArray {l : List UInt8} : + l.toByteArray.size = l.length := by + simp [← ByteArray.size_data] + +@[simp] +theorem _root_.List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl + +@[simp] +theorem empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by + ext1 + simp + +@[simp] +theorem append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by + ext1 + simp + +@[simp, grind =] +theorem size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by + simp [← size_data] + +@[simp] +theorem size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by + refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩ + ext1 + simp [← Array.size_eq_zero_iff, h] + +theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} : + a[i] = a.data[i]'(by simpa [← size_data]) := rfl + +@[simp] +theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} + (hlt : i < a.size) : (a ++ b)[i] = a[i] := by + simp only [getElem_eq_getElem_data, data_append] + rw [Array.getElem_append_left (by simpa)] + +theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} + (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by + simp only [getElem_eq_getElem_data, data_append] + rw [Array.getElem_append_right (by simpa)] + simp + +@[simp] +theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} : + l.toByteArray[i]'h = l[i]'(by simp_all) := by + simp [ByteArray.getElem_eq_getElem_data] + +theorem _root_.List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} : + l[i]'h = l.toByteArray[i]'(by simp_all) := by + simp + +@[simp] +theorem size_extract {a : ByteArray} {b e : Nat} : + (a.extract b e).size = min e a.size - b := by + simp [← size_data] + +@[simp] +theorem extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by + rw [← size_eq_zero_iff, size_extract] + omega + +@[simp] +theorem extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by + simp only [extract_eq_empty_iff] + exact Nat.le_trans (Nat.min_le_left _ _) (by simp) + +@[simp] +theorem append_eq_empty_iff {a b : ByteArray} : + a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by + simp [← size_eq_zero_iff, size_append] + +@[simp] +theorem toByteArray_eq_empty {l : List UInt8} : + l.toByteArray = ByteArray.empty ↔ l = [] := by + simp [← ByteArray.size_eq_zero_iff] + +@[simp] +theorem append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) : + xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂ := by + simp [ByteArray.ext_iff, Array.append_right_inj] + +@[simp] +theorem append_left_inj {xs₁ xs₂ : ByteArray} (ys : ByteArray) : + xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂ := by + simp [ByteArray.ext_iff, Array.append_left_inj] + +@[simp] +theorem extract_append_extract {a : ByteArray} {i j k : Nat} : + a.extract i j ++ a.extract j k = a.extract (min i j) (max j k) := by + ext1 + simp + +theorem extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat) + (hi : i ≤ j) (hk : j ≤ k) : + a.extract i k = a.extract i j ++ a.extract j k := by + simp + rw [Nat.min_eq_left hi, Nat.max_eq_right hk] + +theorem append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by + simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at * + exact Array.append_inj_left h hl + +theorem extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) : + (a ++ b).extract i j = b := by + subst hi hj + ext1 + simp [← size_data] + +theorem extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) : + (a ++ b).extract 0 i = a := by + subst hi + ext1 + simp + +theorem extract_append_size_left {a b : ByteArray} {i : Nat} : + (a ++ b).extract i a.size = a.extract i a.size := by + ext1 + simp + +theorem extract_append_size_add {a b : ByteArray} {i j : Nat} : + (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j := by + ext1 + simp + +theorem extract_append {as bs : ByteArray} {i j : Nat} : + (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by + ext1 + simp + +theorem extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) : + (a ++ b).extract (k + i) (k + j) = b.extract i j := by + cases h + rw [extract_append_size_add] + +theorem extract_extract {a : ByteArray} {i j k l : Nat} : + (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j) := by + ext1 + simp + +theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) : + start + i < xs.size := by + rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h + apply Nat.sub_le_sub_right; apply Nat.min_le_right + +theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} + (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by + simp [getElem_eq_getElem_data] + +theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} : + a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by + simp [ByteArray.ext_iff, Array.extract_eq_extract_left] + +theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) : + a.extract i (i + 1) = [a[i]].toByteArray := by + ext + · simp + omega + · rename_i j hj hj' + obtain rfl : j = 0 := by simpa using hj' + simp [ByteArray.getElem_eq_getElem_data] + +theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) : + a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by + rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), + extract_add_one (by omega), extract_add_one (by omega)] + simp [← List.toByteArray_append] + +theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) : + a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by + rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), + extract_add_one (by omega), extract_add_two (by omega)] + simp [← List.toByteArray_append] + +theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) : + a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by + rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), + extract_add_one (by omega), extract_add_three (by omega)] + simp [← List.toByteArray_append] + +theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by + ext1 + simp + +@[simp] +theorem toList_empty : ByteArray.empty.toList = [] := by + simp [ByteArray.toList, ByteArray.toList.loop] diff --git a/src/Init/Data/ByteArray/Extra.lean b/src/Init/Data/ByteArray/Extra.lean index db6879d2fd55..c3facffa3c1a 100644 --- a/src/Init/Data/ByteArray/Extra.lean +++ b/src/Init/Data/ByteArray/Extra.lean @@ -1,45 +1,306 @@ /- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Copyright (c) 2025 Robin Arnez. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Robin Arnez -/ module prelude public import Init.Data.ByteArray.Basic -import Init.Data.String.Defs -import Init.Data.UInt.Basic +import Init.Data.ByteArray.Lemmas +import Init.Data.Array.Bootstrap +import Init.Data.Array.Lemmas +import Init.Omega +import Init.ByCases -set_option doc.verso true +@[expose] public section -/-- -Interprets a {name}`ByteArray` of size 8 as a little-endian {name}`UInt64`. +namespace ByteArray + +@[deprecated getUInt64LE! +typeChanged (since := "2026-03-29")] +def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 := + bs.getUInt64LE! 0 + +@[deprecated getUInt64BE! +typeChanged (since := "2026-03-29")] +def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 := + bs.getUInt64BE! 0 -Panics if the array's size is not 8. +def SetSizeResult.setoid (origSz sz : Nat) : Setoid { x : ByteArray // x.size = sz } where + r a b := ∀ (i : Nat) (hi : i < sz) (hi' : i < origSz), a.1[i] = b.1[i] + iseqv := { + refl _ _ _ _ := rfl + symm h i hi hi' := (h i hi hi').symm + trans h h' i hi hi' := (h i hi hi').trans (h' i hi hi') + } + +/-- +A byte array of size `sz` where only the first `origSize` bytes are defined and the others are +quotiented out. -/ -public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 := - assert! bs.size == 8 - (bs.get! 7).toUInt64 <<< 0x38 ||| - (bs.get! 6).toUInt64 <<< 0x30 ||| - (bs.get! 5).toUInt64 <<< 0x28 ||| - (bs.get! 4).toUInt64 <<< 0x20 ||| - (bs.get! 3).toUInt64 <<< 0x18 ||| - (bs.get! 2).toUInt64 <<< 0x10 ||| - (bs.get! 1).toUInt64 <<< 0x8 ||| - (bs.get! 0).toUInt64 +structure SetSizeResult (origSz sz : Nat) where + mk' :: value : Quotient (SetSizeResult.setoid origSz sz) + +def SetSizeResult.mk {origSz sz : Nat} (bs : ByteArray) (h : bs.size = sz) : + SetSizeResult origSz sz := ⟨Quotient.mk _ ⟨bs, h⟩⟩ /-- -Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`. +Low-level function for growing or shrinking a byte array. Note that the contents of the bytes +starting at index `size` are undefined when growing. -Panics if the array's size is not 8. +If `exact` is `false`, the capacity will be doubled when grown. -/ -public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 := - assert! bs.size == 8 - (bs.get! 0).toUInt64 <<< 0x38 ||| - (bs.get! 1).toUInt64 <<< 0x30 ||| - (bs.get! 2).toUInt64 <<< 0x28 ||| - (bs.get! 3).toUInt64 <<< 0x20 ||| - (bs.get! 4).toUInt64 <<< 0x18 ||| - (bs.get! 5).toUInt64 <<< 0x10 ||| - (bs.get! 6).toUInt64 <<< 0x8 ||| - (bs.get! 7).toUInt64 +@[extern "lean_byte_array_set_size"] +def setSize (bs : ByteArray) (size : @& Nat) (origSz : @& Nat) (h : bs.size = origSz) + (exact : Bool := false) : SetSizeResult origSz size := + .mk ⟨bs.data.take size ++ Array.replicate (size - bs.size) 0⟩ (by simp [← size_data]; omega) + +@[elab_as_elim, induction_eliminator] +theorem SetSizeResult.ind {origSz sz : Nat} {motive : SetSizeResult origSz sz → Prop} + (mk : ∀ b hb, motive (mk b hb)) (t : SetSizeResult origSz sz) : motive t := by + rcases t with ⟨x, hx⟩; apply mk + +theorem SetSizeResult.sound {origSz sz : Nat} {a ha b hb} + (h : ∀ i (hi : i < sz) (hi' : i < origSz), a[i] = b[i]) : @mk origSz sz a ha = mk b hb := by + simp only [mk, mk'.injEq] + exact Quotient.sound h + +@[inline] +def SetSizeResult.lift {origSz sz : Nat} {α : Sort u} (f : (b : ByteArray) → b.size = sz → α) + (h : ∀ a ha b hb, (∀ i (hi : i < sz) (hi' : i < origSz), a[i] = b[i]) → f a ha = f b hb) + (x : SetSizeResult origSz sz) : α := + x.value.lift (fun ⟨b, hb⟩ => f b hb) (fun ⟨a, ha⟩ ⟨b, hb⟩ => h a ha b hb) + +@[simp] +theorem SetSizeResult.lift_mk {origSz sz : Nat} {α : Sort u} {f h} {b hb} : + @lift origSz sz α f h (mk b hb) = f b hb := rfl + +@[inline] +def SetSizeResult.get {origSz sz : Nat} (x : SetSizeResult origSz sz) (i : Nat) + (hi : i < sz) (hi' : i < origSz) : UInt8 := + x.lift (fun b _ => b[i]) fun _ _ _ _ hab => hab i hi hi' + +instance : GetElem (SetSizeResult origSz sz) Nat UInt8 (fun _ i => i < sz ∧ i < origSz) where + getElem x i h := x.get i h.1 h.2 + +@[simp] +theorem SetSizeResult.getElem_mk {i : Nat} {hi} : + (@mk origSz sz b hb)[i]'hi = b[i] := rfl + +@[simp] +theorem SetSizeResult.getElem_setSize {b : ByteArray} {sz origSz h exact} {i : Nat} (hi) : + (b.setSize sz origSz h exact)[i]'hi = b[i] := by + rw [setSize] + simp only [Array.take_eq_extract, getElem_mk, getElem_eq_getElem_data] + rw [Array.getElem_append_left (by simp; omega)] + simp + +/-- Given the knowledge that `sz ≤ origSz`, extract the byte array out of `x`. -/ +@[inline] +def SetSizeResult.toByteArrayOfLe (x : SetSizeResult origSz sz) (h : sz ≤ origSz) : ByteArray := + x.lift (fun b _ => b) ?_ +where finally + intro a ha b hb hab + ext i hi + · simp [ha, hb] + · apply hab + · exact ha ▸ hi + · exact Nat.lt_of_lt_of_le (ha ▸ hi) h + +@[simp] +theorem SetSizeResult.size_toByteArrayOfLe {x : SetSizeResult origSz sz} (h) : + (x.toByteArrayOfLe h).size = sz := by + induction x with | _ x hx; exact hx + +@[simp] +theorem SetSizeResult.getElem_toByteArrayOfLe + {x : SetSizeResult origSz sz} {h} {i : Nat} (hi) : + (x.toByteArrayOfLe h)[i]'hi = x[i]'(by simp at hi; omega) := by + induction x; rfl + +/-- Returns all the defined bytes in `x`, i.e. the first `min origSz sz` bytes. -/ +def SetSizeResult.toByteArray (x : SetSizeResult origSz sz) : ByteArray := + x.lift (fun b hb => (b.setSize (min origSz sz) _ hb).toByteArrayOfLe (by omega)) ?_ +where finally + intro a ha b hb hab + apply ext_getElem + · simp + · simp only [size_toByteArrayOfLe, getElem_toByteArrayOfLe, getElem_setSize] + intro i h _ + exact hab i (by omega) (by omega) + +@[inline] +def SetSizeResult.push (x : SetSizeResult origSz sz) (b : UInt8) + (h : origSz < sz := by get_elem_tactic) : SetSizeResult (origSz + 1) sz := + x.lift (fun x _ => mk (x.set origSz b) (by simp [*])) ?_ +where finally + intro a ha b hb hab + apply sound + simp +contextual [Nat.lt_add_one_iff_lt_or_eq, or_imp, getElem_set, Nat.ne_of_gt, hab] + +private theorem SetSizeResult.pushBitVecLE_aux (h : origSz + nbytes ≤ sz) + (a : ByteArray) (ha : a.size = sz) (b : ByteArray) (hb : b.size = sz) + (hab : ∀ (i : Nat) (hi : i < sz), i < origSz → a[i] = b[i]) : + @mk (origSz + nbytes) sz (a.setBitVecLE origSz nbytes val) (by simpa using ha) = + mk (b.setBitVecLE origSz nbytes val) (by simpa using hb) := by + apply sound + intro i hi hi' + by_cases h : i < origSz + · simpa [getElem_setBitVecLE, Nat.not_le_of_lt h] using hab i hi h + · simp [getElem_setBitVecLE, hi', Nat.le_of_not_lt h] + +private theorem SetSizeResult.pushBitVecBE_aux (h : origSz + nbytes ≤ sz) + (a : ByteArray) (ha : a.size = sz) (b : ByteArray) (hb : b.size = sz) + (hab : ∀ (i : Nat) (hi : i < sz), i < origSz → a[i] = b[i]) : + @mk (origSz + nbytes) sz (a.setBitVecBE origSz nbytes val) (by simpa using ha) = + mk (b.setBitVecBE origSz nbytes val) (by simpa using hb) := by + apply sound + intro i hi hi' + by_cases h : i < origSz + · simpa [getElem_setBitVecBE, Nat.not_le_of_lt h] using hab i hi h + · simp [getElem_setBitVecBE, hi', Nat.le_of_not_lt h] + +@[inline] +def SetSizeResult.pushBitVecLE (x : SetSizeResult origSz sz) (nbytes : Nat) + (val : BitVec (8 * nbytes)) (h : origSz + nbytes ≤ sz := by get_elem_tactic) : + SetSizeResult (origSz + nbytes) sz := + x.lift (fun x _ => mk (x.setBitVecLE origSz nbytes val) (by simp [*])) (by apply pushBitVecLE_aux h) + +@[inline] +def SetSizeResult.pushBitVecBE (x : SetSizeResult origSz sz) (nbytes : Nat) + (val : BitVec (8 * nbytes)) (h : origSz + nbytes ≤ sz := by get_elem_tactic) : + SetSizeResult (origSz + nbytes) sz := + x.lift (fun x _ => mk (x.setBitVecBE origSz nbytes val) (by simp [*])) (by apply pushBitVecBE_aux h) + +@[inline] +def SetSizeResult.pushUInt16LE (x : SetSizeResult origSz sz) (val : UInt16) + (h : origSz + 2 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 2) sz := + x.lift (fun x _ => mk (x.setUInt16LE origSz val) (by simp [*])) (by apply pushBitVecLE_aux h) + +@[inline] +def SetSizeResult.pushUInt16BE (x : SetSizeResult origSz sz) (val : UInt16) + (h : origSz + 2 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 2) sz := + x.lift (fun x _ => mk (x.setUInt16BE origSz val) (by simp [*])) (by apply pushBitVecBE_aux h) + +@[inline] +def SetSizeResult.pushUInt32LE (x : SetSizeResult origSz sz) (val : UInt32) + (h : origSz + 4 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 4) sz := + x.lift (fun x _ => mk (x.setUInt32LE origSz val) (by simp [*])) (by apply pushBitVecLE_aux h) + +@[inline] +def SetSizeResult.pushUInt32BE (x : SetSizeResult origSz sz) (val : UInt32) + (h : origSz + 4 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 4) sz := + x.lift (fun x _ => mk (x.setUInt32BE origSz val) (by simp [*])) (by apply pushBitVecBE_aux h) + +@[inline] +def SetSizeResult.pushUInt64LE (x : SetSizeResult origSz sz) (val : UInt64) + (h : origSz + 8 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 8) sz := + x.lift (fun x _ => mk (x.setUInt64LE origSz val) (by simp [*])) (by apply pushBitVecLE_aux h) + +@[inline] +def SetSizeResult.pushUInt64BE (x : SetSizeResult origSz sz) (val : UInt64) + (h : origSz + 8 ≤ sz := by get_elem_tactic) : SetSizeResult (origSz + 8) sz := + x.lift (fun x _ => mk (x.setUInt64BE origSz val) (by simp [*])) (by apply pushBitVecBE_aux h) + +def pushBitVecLE (x : ByteArray) (nbytes : Nat) (val : BitVec (8 * nbytes)) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + nbytes) origSz rfl).pushBitVecLE nbytes val).toByteArrayOfLe (Nat.le_refl _) + +def pushBitVecBE (x : ByteArray) (nbytes : Nat) (val : BitVec (8 * nbytes)) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + nbytes) origSz rfl).pushBitVecBE nbytes val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt16LE (x : ByteArray) (val : UInt16) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 2) origSz rfl).pushUInt16LE val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt16BE (x : ByteArray) (val : UInt16) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 2) origSz rfl).pushUInt16BE val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt32LE (x : ByteArray) (val : UInt32) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 4) origSz rfl).pushUInt32LE val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt32BE (x : ByteArray) (val : UInt32) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 4) origSz rfl).pushUInt32BE val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt64LE (x : ByteArray) (val : UInt64) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 8) origSz rfl).pushUInt64LE val).toByteArrayOfLe (Nat.le_refl _) + +def pushUInt64BE (x : ByteArray) (val : UInt64) : ByteArray := + let origSz := x.size + ((x.setSize (origSz + 8) origSz rfl).pushUInt64BE val).toByteArrayOfLe (Nat.le_refl _) + +@[inline] +def SetSizeResult.fill (x : SetSizeResult origSz sz) (b : UInt8) (h : origSz ≤ sz) : + ByteArray := + x.lift (fun x _ => x.fill origSz (sz - origSz) b) ?_ +where finally + intro a ha b hb hab + apply ext_getElem + · simp [ha, hb] + · intro i hi hi' + simp only [size_fill, ha] at hi + simp only [getElem_fill, Nat.add_sub_cancel' h, hi, and_true] + split + · rfl + · apply hab <;> omega + +@[simp] +theorem SetSizeResult.size_fill {x : SetSizeResult origSz sz} {b h} : + (x.fill b h).size = sz := by + induction x with | _ x hx + simpa [fill] using hx + +theorem SetSizeResult.getElem_fill {x : SetSizeResult origSz sz} {b h} {i : Nat} {hi} : + (x.fill b h)[i]'hi = if h : i < origSz then x[i]'⟨by simpa using hi, h⟩ else b := by + induction x with | _ x hx + simp only [size_fill] at hi + simp [fill, ByteArray.getElem_fill, Nat.add_sub_cancel' h, hi, ← Nat.not_lt]; rfl + +def setSizeD (bs : ByteArray) (size : Nat) (exact : Bool := false) : ByteArray := + let prevSz := bs.size + let res := bs.setSize size prevSz rfl exact + if h : prevSz < size then res.fill 0 (Nat.le_of_lt h) else res.toByteArrayOfLe (Nat.not_lt.mp h) + +@[simp, grind =] +theorem size_setSizeD (bs : ByteArray) (size : Nat) (exact : Bool) : + (bs.setSizeD size exact).size = size := by + rw [setSizeD] + split <;> simp + +@[grind =] +theorem getElem_setSizeD {bs : ByteArray} {size : Nat} {exact : Bool} {i : Nat} + (h : i < (bs.setSizeD size exact).size) : + (bs.setSizeD size exact)[i] = if h : i < bs.size then bs[i] else 0 := by + rw [size_setSizeD] at h + simp only [setSizeD] + split + · simp [SetSizeResult.getElem_fill] + · rw [dite_eq_left (c := i < _) (by omega)] + simp + +/-- Creates an array that contains n repetitions of the byte v. -/ +def replicate (n : Nat) (v : UInt8) := + ((emptyWithCapacity n).setSize n 0 rfl).fill v (by simp) + +@[simp] +theorem data_replicate (size : Nat) (value : UInt8) : + (replicate size value).data = Array.replicate size value := by + simp only [replicate] + ext + · simp + · simp [← getElem_eq_getElem_data, SetSizeResult.getElem_fill] + +@[simp] +theorem size_replicate {n : Nat} {v : UInt8} : (replicate n v).size = n := by + simp [← size_data] + +@[simp] +theorem getElem_replicate {i : Nat} {n : Nat} {v : UInt8} (h : i < (replicate n v).size) : + (replicate n v)[i] = v := by + simp [getElem_eq_getElem_data] + +end ByteArray diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index cfb01253e78c..d3f2e2a6569f 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -6,264 +6,19 @@ Author: Markus Himmel module prelude -public import Init.Data.ByteArray.Basic +public import Init.Data.ByteArray.BootstrapLemmas import Init.ByCases import Init.Data.Array.Bootstrap import Init.Data.Array.Extract import Init.Data.Array.Lemmas +import Init.Data.BitVec.Bootstrap +import Init.Data.BitVec.Lemmas import Init.Omega public section namespace ByteArray --- At present the preferred normal form for empty byte arrays is `ByteArray.empty` -@[simp] -theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl - -@[simp] -theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl - -@[simp] -theorem data_empty : ByteArray.empty.data = #[] := rfl - -@[simp] -theorem data_extract {a : ByteArray} {b e : Nat} : - (a.extract b e).data = a.data.extract b e := by - simp [extract, copySlice] - by_cases b ≤ e - · rw [(by omega : b + (e - b) = e)] - · rw [Array.extract_eq_empty_of_le (by omega), Array.extract_eq_empty_of_le (by omega)] - -@[simp] -theorem extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by - ext1 - simp - -@[simp] -theorem extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by - ext1 - simp [Nat.min_le_left] - -theorem fastAppend_eq_copySlice {a b : ByteArray} : - a.fastAppend b = b.copySlice 0 a a.size b.size false := rfl - -@[simp] -theorem _root_.List.toByteArray_append {l l' : List UInt8} : - (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray := by - simp [List.toByteArray_append'] - -@[simp] -theorem toList_data_append {l l' : ByteArray} : - (l ++ l').data.toList = l.data.toList ++ l'.data.toList := by - simp [← append_eq] - -@[simp] -theorem data_append {l l' : ByteArray} : - (l ++ l').data = l.data ++ l'.data := by - simp [← Array.toList_inj] - -@[simp] -theorem size_empty : ByteArray.empty.size = 0 := by - simp [← ByteArray.size_data] - -@[simp] -theorem _root_.List.data_toByteArray {l : List UInt8} : - l.toByteArray.data = l.toArray := by - rw [List.toByteArray] - suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by - simpa using this l ByteArray.empty - intro a b - fun_induction List.toByteArray.loop a b with simp_all - -@[simp] -theorem _root_.List.size_toByteArray {l : List UInt8} : - l.toByteArray.size = l.length := by - simp [← ByteArray.size_data] - -@[simp] -theorem _root_.List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl - -@[simp] -theorem empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by - ext1 - simp - -@[simp] -theorem append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by - ext1 - simp - -@[simp, grind =] -theorem size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by - simp [← size_data] - -@[simp] -theorem size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by - refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩ - ext1 - simp [← Array.size_eq_zero_iff, h] - -theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} : - a[i] = a.data[i]'(by simpa [← size_data]) := rfl - -@[simp] -theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} - (hlt : i < a.size) : (a ++ b)[i] = a[i] := by - simp only [getElem_eq_getElem_data, data_append] - rw [Array.getElem_append_left (by simpa)] - -theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} - (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by - simp only [getElem_eq_getElem_data, data_append] - rw [Array.getElem_append_right (by simpa)] - simp - -@[simp] -theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} : - l.toByteArray[i]'h = l[i]'(by simp_all) := by - simp [ByteArray.getElem_eq_getElem_data] - -theorem _root_.List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} : - l[i]'h = l.toByteArray[i]'(by simp_all) := by - simp - -@[simp] -theorem size_extract {a : ByteArray} {b e : Nat} : - (a.extract b e).size = min e a.size - b := by - simp [← size_data] - -@[simp] -theorem extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by - rw [← size_eq_zero_iff, size_extract] - omega - -@[simp] -theorem extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by - simp only [extract_eq_empty_iff] - exact Nat.le_trans (Nat.min_le_left _ _) (by simp) - -@[simp] -theorem append_eq_empty_iff {a b : ByteArray} : - a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by - simp [← size_eq_zero_iff, size_append] - -@[simp] -theorem toByteArray_eq_empty {l : List UInt8} : - l.toByteArray = ByteArray.empty ↔ l = [] := by - simp [← ByteArray.size_eq_zero_iff] - -@[simp] -theorem append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) : - xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂ := by - simp [ByteArray.ext_iff, Array.append_right_inj] - -@[simp] -theorem append_left_inj {xs₁ xs₂ : ByteArray} (ys : ByteArray) : - xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂ := by - simp [ByteArray.ext_iff, Array.append_left_inj] - -@[simp] -theorem extract_append_extract {a : ByteArray} {i j k : Nat} : - a.extract i j ++ a.extract j k = a.extract (min i j) (max j k) := by - ext1 - simp - -theorem extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat) - (hi : i ≤ j) (hk : j ≤ k) : - a.extract i k = a.extract i j ++ a.extract j k := by - simp - rw [Nat.min_eq_left hi, Nat.max_eq_right hk] - -theorem append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by - simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at * - exact Array.append_inj_left h hl - -theorem extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) : - (a ++ b).extract i j = b := by - subst hi hj - ext1 - simp [← size_data] - -theorem extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) : - (a ++ b).extract 0 i = a := by - subst hi - ext1 - simp - -theorem extract_append_size_left {a b : ByteArray} {i : Nat} : - (a ++ b).extract i a.size = a.extract i a.size := by - ext1 - simp - -theorem extract_append_size_add {a b : ByteArray} {i j : Nat} : - (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j := by - ext1 - simp - -theorem extract_append {as bs : ByteArray} {i j : Nat} : - (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by - ext1 - simp - -theorem extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) : - (a ++ b).extract (k + i) (k + j) = b.extract i j := by - cases h - rw [extract_append_size_add] - -theorem extract_extract {a : ByteArray} {i j k l : Nat} : - (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j) := by - ext1 - simp - -theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) : - start + i < xs.size := by - rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h - apply Nat.sub_le_sub_right; apply Nat.min_le_right - -theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} - (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by - simp [getElem_eq_getElem_data] - -theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} : - a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by - simp [ByteArray.ext_iff, Array.extract_eq_extract_left] - -theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) : - a.extract i (i + 1) = [a[i]].toByteArray := by - ext - · simp - omega - · rename_i j hj hj' - obtain rfl : j = 0 := by simpa using hj' - simp [ByteArray.getElem_eq_getElem_data] - -theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) : - a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by - rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), - extract_add_one (by omega), extract_add_one (by omega)] - simp [← List.toByteArray_append] - -theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) : - a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by - rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), - extract_add_one (by omega), extract_add_two (by omega)] - simp [← List.toByteArray_append] - -theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) : - a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by - rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), - extract_add_one (by omega), extract_add_three (by omega)] - simp [← List.toByteArray_append] - -theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by - ext1 - simp - -@[simp] -theorem toList_empty : ByteArray.empty.toList = [] := by - simp [ByteArray.toList, ByteArray.toList.loop] - theorem copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} : ByteArray.copySlice src srcOff dest destOff len exact = dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by @@ -275,11 +30,26 @@ theorem data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} : (as.set i a h).data = as.data.set i a (by simpa) := by simp [set] +@[simp] +theorem size_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} : + (as.set i a h).size = as.size := by + simp [← size_data] + theorem set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} : as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by ext1 simpa using! Array.set_eq_push_extract_append_extract _ +theorem getElem_set {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} {j : Nat} + (hj : j < (as.set i a h).size) : + (as.set i a h)[j] = if i = j then a else as[j]'(by simpa using hj) := by + simp [getElem_eq_getElem_data, Array.getElem_set] + +@[simp] +theorem getElem_set_self {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} : + (as.set i a h)[i]'(by simpa using h) = a := by + simp [getElem_set] + @[simp] theorem append_toByteArray_singleton {as : ByteArray} {a : UInt8} : as ++ [a].toByteArray = as.push a := by @@ -328,6 +98,298 @@ theorem extract_eq_extract_iff_getElem {as bs : ByteArray} {i j len : Nat} · exact h k hk' · exact (by omega : k = len) ▸ h' +private theorem getBitVecLE.getElem_go {bs i n h k hk acc j hj} : + (go bs i n h k hk acc)[j]'hj = + if h : j < 8 * k then acc[j] else bs[i + j / 8].toBitVec[j % 8] := by + fun_induction go with + | case1 k _ acc hk b ih => + rw [ih]; split + · simp only [BitVec.getElem_cast, BitVec.getElem_append, b] + split + · rfl + · congr <;> omega + · rw [dite_eq_right (by omega)] + | case2 => rw [dite_eq_left (by omega), BitVec.getElem_cast] + +@[grind =] +theorem getElem_getBitVecLE {bs : ByteArray} {i nbytes : Nat} + (hi : i + nbytes ≤ bs.size) (hj : j < 8 * nbytes) : + (getBitVecLE bs i nbytes hi)[j]'hj = bs[i + j / 8].toBitVec[j % 8] := by + simp [getBitVecLE, getBitVecLE.getElem_go] + +@[simp] +theorem getBitVecLE_zero {bs : ByteArray} {i : Nat} (h) : + getBitVecLE bs i 0 h = 0#0 := BitVec.eq_nil _ + +theorem getBitVecLE_add {bs : ByteArray} {i : Nat} (m n : Nat) (h) : + getBitVecLE bs i (n + m) h = + (getBitVecLE bs (i + m) n ++ getBitVecLE bs i m).cast (by omega) := by + ext i hi + simp +contextual only [getElem_getBitVecLE, BitVec.getElem_cast, BitVec.getElem_append, + Nat.sub_mul_div, left_eq_dite_iff, Nat.not_lt, Nat.sub_mul_mod] + intro; congr 3; omega + +@[simp] +theorem getBitVecLE_one {bs : ByteArray} {i : Nat} (h) : + getBitVecLE bs i 1 h = bs[i].toBitVec := by + ext j hj + rw [ByteArray.getElem_getBitVecLE] + simp [Nat.div_eq_of_lt hj, Nat.mod_eq_of_lt hj] + +theorem getBitVecLE_add_one {bs : ByteArray} {i : Nat} {n : Nat} (h) : + getBitVecLE bs i (n + 1) h = getBitVecLE bs (i + 1) n ++ bs[i].toBitVec := by + rw [getBitVecLE_add]; simp + +theorem extractLsb'_getBitVecLE_eight {bs : ByteArray} {i : Nat} {n : Nat} {h} {k : Nat} + (hk : k < n) : (getBitVecLE bs i n h).extractLsb' (8 * k) 8 = bs[i + k].toBitVec := by + ext j hj + rw [BitVec.getElem_extractLsb', BitVec.getLsbD_eq_getElem (by omega), getElem_getBitVecLE] + simp [Nat.mul_add_div, Nat.div_eq_of_lt hj, Nat.mod_eq_of_lt hj] + +private theorem getBitVecBE.getMsbD_go {bs i n h k hk acc j} (hj : j < 8 * n) : + (go bs i n h k hk acc).getMsbD j = + if j < 8 * k then acc.getMsbD j else bs[i + j / 8].toBitVec.getMsbD (j % 8) := by + fun_induction go with + | case1 k _ acc hk b ih => + rw [ih]; split + · simp only [BitVec.getMsbD_cast, BitVec.getMsbD_append, b, ← Nat.not_lt, ite_not] + split + · rfl + · congr <;> omega + · rw [ite_eq_right (by omega)] + | case2 => rw [ite_eq_left (by omega), BitVec.getMsbD_cast] + +theorem getMsbD_getBitVecBE {bs : ByteArray} {i nbytes : Nat} + (hi : i + nbytes ≤ bs.size) (hj : j < 8 * nbytes) : + (getBitVecBE bs i nbytes hi).getMsbD j = bs[i + j / 8].toBitVec.getMsbD (j % 8) := by + simp [getBitVecBE, getBitVecBE.getMsbD_go, hj] + +@[grind =] +theorem getElem_getBitVecBE {bs : ByteArray} {i nbytes : Nat} + (hi : i + nbytes ≤ bs.size) (hj : j < 8 * nbytes) : + (getBitVecBE bs i nbytes hi)[j] = bs[i + nbytes - j / 8 - 1].toBitVec[j % 8] := by + rw [← BitVec.getLsbD_eq_getElem, BitVec.getLsbD_eq_getMsbD, getMsbD_getBitVecBE _ (by omega), + decide_eq_true hj, Bool.true_and, BitVec.getMsbD_eq_getLsbD, decide_eq_true (by omega), + Bool.true_and, BitVec.getLsbD_eq_getElem (by omega)] + congr <;> omega + +@[simp] +theorem getBitVecBE_zero {bs : ByteArray} {i : Nat} (h) : + getBitVecBE bs i 0 h = 0#0 := BitVec.eq_nil _ + +theorem getBitVecBE_add {bs : ByteArray} {i : Nat} (m n : Nat) (h) : + getBitVecBE bs i (n + m) h = + (getBitVecBE bs i m ++ getBitVecBE bs (i + m) n).cast (by omega) := by + apply BitVec.eq_of_getMsbD_eq + intro j hj + simp +contextual only [hj, getMsbD_getBitVecBE, BitVec.getMsbD_cast, BitVec.getMsbD_append, + Nat.sub_lt_iff_lt_add, ← Nat.mul_add, Nat.sub_mul_div, Nat.sub_mul_mod, ← dite_eq_ite, + not_false_eq_true, Nat.lt_of_not_le, right_eq_dite_iff] + intro; congr 3; omega + +@[simp] +theorem getBitVecBE_one {bs : ByteArray} {i : Nat} (h) : + getBitVecBE bs i 1 h = bs[i].toBitVec := by + apply BitVec.eq_of_getMsbD_eq + intro j hj + rw [ByteArray.getMsbD_getBitVecBE _ hj] + simp [Nat.div_eq_of_lt hj, Nat.mod_eq_of_lt hj] + +theorem getBitVecBE_add_one {bs : ByteArray} {i : Nat} {n : Nat} (h) : + getBitVecBE bs i (n + 1) h = + (bs[i].toBitVec ++ getBitVecBE bs (i + 1) n).cast (Nat.add_comm ..) := by + rw [getBitVecBE_add]; simp + +theorem extractLsb'_getBitVecBE_eight {bs : ByteArray} {i : Nat} {n : Nat} {h} {k : Nat} + (hk : k < n) : (getBitVecBE bs i n h).extractLsb' (8 * k) 8 = bs[i + n - k - 1].toBitVec := by + ext j hj + rw [BitVec.getElem_extractLsb', BitVec.getLsbD_eq_getElem (by omega), getElem_getBitVecBE] + simp [Nat.mul_add_div, Nat.div_eq_of_lt hj, Nat.mod_eq_of_lt hj] + +private theorem setBitVecLE.size_go : + (go i nbytes val k hk acc h).size = acc.size := by + fun_induction go <;> simp_all +zetaDelta + +@[simp, grind =] +theorem size_setBitVecLE {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} + {hi : i + nbytes ≤ bs.size} : (bs.setBitVecLE i nbytes val hi).size = bs.size := by + rw [setBitVecLE, setBitVecLE.size_go] + +private theorem setBitVecLE.getElem_go : + (go i nbytes val k hk acc h)[j]'hj = + if i + k ≤ j ∧ j < i + nbytes then UInt8.ofBitVec (val.extractLsb' (8 * (j - i)) 8) + else acc[j]'(by simpa [size_go] using hj) := by + fun_induction go with + | @case1 k _ acc h hk acc' ih => + unfold go + simp only [hk, ↓reduceDIte, ih, acc'] + split + · rw [ite_eq_left (by omega)] + split + · simp [show j = i + k by omega] + · rw [getElem_set, ite_eq_right (by omega)] + | case2 k hk acc h hk' => + unfold go + simp only [hk', ↓reduceDIte, right_eq_ite_iff, and_imp] + intros; omega + +@[grind =] +theorem getElem_setBitVecLE {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} {j : Nat} + {hi : i + nbytes ≤ bs.size} (hj : j < (bs.setBitVecLE i nbytes val hi).size) : + (bs.setBitVecLE i nbytes val hi)[j] = + if i ≤ j ∧ j < i + nbytes then UInt8.ofBitVec (val.extractLsb' (8 * (j - i)) 8) + else bs[j]'(by simpa using hj) := by + simp [setBitVecLE, setBitVecLE.getElem_go] + +@[simp] +theorem setBitVecLE_zero {bs : ByteArray} {i : Nat} {val hi} : + bs.setBitVecLE i 0 val hi = bs := by + apply ByteArray.ext_getElem <;> simp +contextual [getElem_setBitVecLE, Nat.not_lt_of_le] + +@[simp] +theorem setBitVecLE_one {bs : ByteArray} {i : Nat} {val hi} : + bs.setBitVecLE i 1 val hi = bs.set i (.ofBitVec val) hi := by + apply ByteArray.ext_getElem + · simp + · intro j hj hj' + simp only [getElem_setBitVecLE, getElem_set] + split + · simp [show i = j by omega] + · simp [show i ≠ j by omega] + +@[simp] +theorem setBitVecLE_cast {bs : ByteArray} {i : Nat} {n n'} {val : BitVec (8 * n)} {hi} + (hn : 8 * n = 8 * n') : bs.setBitVecLE i n' (val.cast hn) = bs.setBitVecLE i n val := by + rw [Nat.mul_right_inj (by decide)] at hn + subst hn; rfl + +theorem setBitVecLE_append {bs : ByteArray} {i : Nat} {n n' k} + {val : BitVec (8 * n)} {val' : BitVec (8 * n')} {hk} {hi} : + bs.setBitVecLE i k ((val ++ val').cast hk) hi = + (bs.setBitVecLE i n' val').setBitVecLE (i + n') n val (by simp; omega) := by + apply ByteArray.ext_getElem + · simp + · intro j hj hj' + simp only [getElem_setBitVecLE, ← apply_ite UInt8.ofBitVec, UInt8.ofBitVec.injEq, + BitVec.extractLsb'_cast] + symm; split + · rw [ite_eq_left (by omega), BitVec.extractLsb'_append_eq_of_le (by omega)]; congr; omega + split + · rw [ite_eq_left (by omega), BitVec.extractLsb'_append_eq_of_add_le (by omega)] + · rw [ite_eq_right (by omega)] + +theorem getBitVecLE_setBitVecLE_self {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} + {hi} : (bs.setBitVecLE i nbytes val hi).getBitVecLE i nbytes (by simpa using hi) = val := by + ext j hj + rw [getElem_getBitVecLE, getElem_setBitVecLE, ite_eq_left (by omega)] + simp [Nat.div_add_mod, hj] + +private theorem setBitVecBE.size_go : + (go i nbytes val k hk acc h).size = acc.size := by + fun_induction go <;> simp_all +zetaDelta + +@[simp, grind =] +theorem size_setBitVecBE {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} + {hi : i + nbytes ≤ bs.size} : (bs.setBitVecBE i nbytes val hi).size = bs.size := by + rw [setBitVecBE, setBitVecBE.size_go] + +private theorem setBitVecBE.getElem_go : + (go i nbytes val k hk acc h)[j]'hj = + if i + k ≤ j ∧ j < i + nbytes then + UInt8.ofBitVec (val.extractLsb' (8 * (i + nbytes - j - 1)) 8) + else acc[j]'(by simpa [size_go] using hj) := by + fun_induction go with + | @case1 k _ acc h hk acc' ih => + unfold go + simp only [hk, ↓reduceDIte, ih, acc'] + split + · rw [ite_eq_left (by omega)] + split + · simp [show j = i + k by omega]; congr 2; omega + · rw [getElem_set, ite_eq_right (by omega)] + | case2 k hk acc h hk' => + unfold go + simp only [hk', ↓reduceDIte, right_eq_ite_iff, and_imp] + intros; omega + +@[grind =] +theorem getElem_setBitVecBE {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} {j : Nat} + {hi : i + nbytes ≤ bs.size} (hj : j < (bs.setBitVecBE i nbytes val hi).size) : + (bs.setBitVecBE i nbytes val hi)[j] = + if i ≤ j ∧ j < i + nbytes then + UInt8.ofBitVec (val.extractLsb' (8 * (i + nbytes - j - 1)) 8) + else bs[j]'(by simpa using hj) := by + simp [setBitVecBE, setBitVecBE.getElem_go] + +@[simp] +theorem setBitVecBE_zero {bs : ByteArray} {i : Nat} {val hi} : + bs.setBitVecBE i 0 val hi = bs := by + apply ByteArray.ext_getElem <;> simp +contextual [getElem_setBitVecBE, Nat.not_lt_of_le] + +@[simp] +theorem setBitVecBE_one {bs : ByteArray} {i : Nat} {val hi} : + bs.setBitVecBE i 1 val hi = bs.set i (.ofBitVec val) hi := by + apply ByteArray.ext_getElem + · simp + · intro j hj hj' + simp only [getElem_setBitVecBE, getElem_set] + split + · simp [show i = j by omega] + · simp [show i ≠ j by omega] + +@[simp] +theorem setBitVecBE_cast {bs : ByteArray} {i : Nat} {n n'} {val : BitVec (8 * n)} {hi} + (hn : 8 * n = 8 * n') : bs.setBitVecBE i n' (val.cast hn) = bs.setBitVecBE i n val := by + rw [Nat.mul_right_inj (by decide)] at hn + subst hn; rfl + +theorem setBitVecBE_append {bs : ByteArray} {i : Nat} {n n' k} + {val : BitVec (8 * n)} {val' : BitVec (8 * n')} {hk} {hi} : + bs.setBitVecBE i k ((val ++ val').cast hk) hi = + (bs.setBitVecBE i n val).setBitVecBE (i + n) n' val' (by simp; omega) := by + apply ByteArray.ext_getElem + · simp + · intro j hj hj' + simp only [getElem_setBitVecBE, ← apply_ite UInt8.ofBitVec, UInt8.ofBitVec.injEq, + BitVec.extractLsb'_cast] + symm; split + · rw [ite_eq_left (by omega), BitVec.extractLsb'_append_eq_of_add_le (by omega)]; congr 2; omega + split + · rw [ite_eq_left (by omega), BitVec.extractLsb'_append_eq_of_le (by omega)]; congr; omega + · rw [ite_eq_right (by omega)] + +theorem getBitVecBE_setBitVecBE_self {bs : ByteArray} {i nbytes : Nat} {val : BitVec (8 * nbytes)} + {hi} : (bs.setBitVecBE i nbytes val hi).getBitVecBE i nbytes (by simpa using hi) = val := by + ext j hj + rw [getElem_getBitVecBE, getElem_setBitVecBE, ite_eq_left (by omega)] + simp only [BitVec.getElem_extractLsb'] + rw [show 8 * _ + j % 8 = j by omega] + simp [hj] + +@[simp] +theorem size_fill {bs : ByteArray} {start size : Nat} {val : UInt8} + (h : start + size ≤ bs.size) : (bs.fill start size val).size = bs.size := by + rw [← size_data] at h + simp [fill, copySlice, ← size_data] <;> omega + +theorem getElem_fill {bs : ByteArray} {start size : Nat} {val : UInt8} + (h : start + size ≤ bs.size) {i : Nat} (hi : i < (bs.fill start size val).size) : + (bs.fill start size val)[i] = + if start ≤ i ∧ i < start + size then val else bs[i]'(size_fill h ▸ hi) := by + have hstart : start ≤ bs.data.size := Nat.le_of_add_right_le h + have hsize : size ≤ bs.data.size := Nat.le_of_add_right_le (Nat.add_comm .. ▸ h) + simp only [fill, copySlice, Nat.zero_add, Array.size_replicate, Nat.sub_zero, Nat.min_self, + Nat.min_eq_left, Array.append_assoc, getElem_eq_getElem_data, Array.getElem_append, Array.size_extract, + hstart, Array.getElem_extract, Array.getElem_replicate] + split + · simp only [Nat.not_le_of_lt ‹_›, false_and, ↓reduceIte] + · rename_i h' + replace h' := Nat.le_of_not_lt h' + simp only [← Nat.sub_lt_iff_lt_add', h', true_and] + split + · rfl + · congr; omega + theorem getElem!_push_lt (data : ByteArray) (b : UInt8) (i : Nat) (hi : i < data.size) : (data.push b)[i]! = data[i]! := by have hi' : i < (data.push b).size := by diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index f134aa64f918..449d0f558619 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -122,7 +122,7 @@ def randBool {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen := (v = 1, g') initialize IO.stdGenRef : IO.Ref StdGen ← - let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8)) + let seed := UInt64.toNat ((← IO.getRandomBytes 8).getUInt64LE! 0) IO.mkRef (mkStdGen seed) /-- diff --git a/src/Init/Data/String/Decode.lean b/src/Init/Data/String/Decode.lean index 31be6729ed56..cee330ff5922 100644 --- a/src/Init/Data/String/Decode.lean +++ b/src/Init/Data/String/Decode.lean @@ -8,10 +8,10 @@ module prelude import Init.Data.Char.Lemmas public import Init.Data.ByteArray.Basic -import Init.Data.ByteArray.Lemmas public import Init.Data.UInt.Basic import Init.Data.BitVec.Bootstrap import Init.Data.BitVec.Lemmas +import Init.Data.ByteArray.Lemmas import Init.Data.Nat.Internal.Linear import Init.Data.Nat.MinMax import Init.Data.Option.Lemmas diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean index 440cd9a9d6db..908644957c57 100644 --- a/src/Init/Data/String/Defs.lean +++ b/src/Init/Data/String/Defs.lean @@ -7,7 +7,7 @@ module prelude public import Init.Data.String.PosRaw -import Init.Data.ByteArray.Lemmas +import Init.Data.ByteArray.BootstrapLemmas import Init.Omega /-! diff --git a/src/Init/Data/String/OrderInstances.lean b/src/Init/Data/String/OrderInstances.lean index 95e63da70118..32061ab909e9 100644 --- a/src/Init/Data/String/OrderInstances.lean +++ b/src/Init/Data/String/OrderInstances.lean @@ -30,7 +30,7 @@ scoped macro "order" : tactic => `(tactic| { end Internal -open Internal +open String.Internal namespace Pos.Raw diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index e46f44a15998..bb80fa0893e2 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -191,7 +191,7 @@ def keepAliveTimeMs : Nat := def new (wireFormat : Lsp.RpcWireFormat) : IO (UInt64 × RpcSession) := do /- We generate a random ID to ensure that session IDs do not repeat across re-initializations and worker restarts. Otherwise, the client may attempt to use outdated references. -/ - let newId ← ByteArray.toUInt64LE! <$> IO.getRandomBytes 8 + let newId := (← IO.getRandomBytes 8).getUInt64LE! 0 let newSesh := { objects := { wireFormat } expireTime := (← IO.monoMsNow) + keepAliveTimeMs diff --git a/src/Std/Http/Data/URI/Encoding.lean b/src/Std/Http/Data/URI/Encoding.lean index a55ec00998f6..1da2591943b1 100644 --- a/src/Std/Http/Data/URI/Encoding.lean +++ b/src/Std/Http/Data/URI/Encoding.lean @@ -12,6 +12,7 @@ import Init.Data.SInt.Lemmas import Init.Data.UInt.Lemmas import Init.Data.UInt.Bitwise import Init.Data.Array.Lemmas +import Init.Data.ByteArray.Lemmas public import Init.Data.String.Basic public import Std.Http.Internal.Char @@ -215,8 +216,7 @@ private theorem ByteArray.toList_toByteArray (ba : ByteArray) : | mk data => simp [List.toByteArray] apply ByteArray.ext - simp [List.toByteArray_loop_eq, ByteArray.empty] - decide + simp [List.toByteArray_loop_eq] theorem isValidUTF8_of_isAsciiByte (ba : ByteArray) (s : ba.data.all isAsciiByte) : ByteArray.IsValidUTF8 ba := by refine ⟨ba.data.toList.map Char.ofUInt8, ?_⟩ @@ -256,7 +256,7 @@ namespace EncodedString Creates an empty encoded string. -/ def empty : EncodedString r := - ⟨.empty, by simp []; exact fun i h => by contradiction⟩ + ⟨.empty, by simp⟩ instance : Inhabited (EncodedString r) where default := EncodedString.empty @@ -409,7 +409,7 @@ namespace EncodedQueryString Creates an empty encoded query string. -/ def empty : EncodedQueryString r := - ⟨.empty, by simp; intro a h; contradiction⟩ + ⟨.empty, by simp⟩ instance : Inhabited (EncodedQueryString r) where default := EncodedQueryString.empty diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean index fbd254b50956..434a14929abb 100644 --- a/src/Std/Time/Date/PlainDate.lean +++ b/src/Std/Time/Date/PlainDate.lean @@ -15,7 +15,7 @@ public section namespace Std namespace Time open Std.Time -open Internal +open Time.Internal open Lean set_option linter.all true diff --git a/src/Std/Time/Date/Unit/Basic.lean b/src/Std/Time/Date/Unit/Basic.lean index 3a43abaa7908..1c7d7ca4e350 100644 --- a/src/Std/Time/Date/Unit/Basic.lean +++ b/src/Std/Time/Date/Unit/Basic.lean @@ -22,7 +22,7 @@ to facilitate conversions and manipulations between them. namespace Std namespace Time -open Internal +open Time.Internal namespace Day.Offset diff --git a/src/Std/Time/Date/Unit/Day.lean b/src/Std/Time/Date/Unit/Day.lean index e4c6f436b794..79c24344f523 100644 --- a/src/Std/Time/Date/Unit/Day.lean +++ b/src/Std/Time/Date/Unit/Day.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Day -open Lean Internal +open Lean Time.Internal set_option linter.all true diff --git a/src/Std/Time/Date/Unit/Month.lean b/src/Std/Time/Date/Unit/Month.lean index 53f24c15df1f..1f7b03da7e1e 100644 --- a/src/Std/Time/Date/Unit/Month.lean +++ b/src/Std/Time/Date/Unit/Month.lean @@ -14,7 +14,7 @@ public section namespace Std namespace Time namespace Month -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Date/Unit/Week.lean b/src/Std/Time/Date/Unit/Week.lean index 6fd0bc81e738..18a1ea179ec3 100644 --- a/src/Std/Time/Date/Unit/Week.lean +++ b/src/Std/Time/Date/Unit/Week.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Week -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Date/Unit/Weekday.lean b/src/Std/Time/Date/Unit/Weekday.lean index 5afa5a4fec1c..9f1ebc8397fd 100644 --- a/src/Std/Time/Date/Unit/Weekday.lean +++ b/src/Std/Time/Date/Unit/Weekday.lean @@ -12,7 +12,7 @@ public section namespace Std namespace Time -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean index a68419fabacf..48a308fc70e8 100644 --- a/src/Std/Time/Date/Unit/Year.lean +++ b/src/Std/Time/Date/Unit/Year.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Year -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/HourMarker.lean b/src/Std/Time/Time/HourMarker.lean index b98717cb8ac9..7aadbe13a813 100644 --- a/src/Std/Time/Time/HourMarker.lean +++ b/src/Std/Time/Time/HourMarker.lean @@ -12,7 +12,7 @@ public section namespace Std namespace Time -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index 25d7f1481c9b..1f115b06d0f6 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -12,7 +12,7 @@ public section namespace Std namespace Time -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Basic.lean b/src/Std/Time/Time/Unit/Basic.lean index 6b2382f3c6fc..8e832cd1ddae 100644 --- a/src/Std/Time/Time/Unit/Basic.lean +++ b/src/Std/Time/Time/Unit/Basic.lean @@ -21,7 +21,7 @@ to facilitate conversions and manipulations between them. namespace Std namespace Time -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Hour.lean b/src/Std/Time/Time/Unit/Hour.lean index 874823e20e41..e970792c3dc9 100644 --- a/src/Std/Time/Time/Unit/Hour.lean +++ b/src/Std/Time/Time/Unit/Hour.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Hour -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Millisecond.lean b/src/Std/Time/Time/Unit/Millisecond.lean index b319b932688c..7c018ae3463d 100644 --- a/src/Std/Time/Time/Unit/Millisecond.lean +++ b/src/Std/Time/Time/Unit/Millisecond.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Millisecond -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Minute.lean b/src/Std/Time/Time/Unit/Minute.lean index a72193a8b53b..bc37540a7954 100644 --- a/src/Std/Time/Time/Unit/Minute.lean +++ b/src/Std/Time/Time/Unit/Minute.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Minute -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Nanosecond.lean b/src/Std/Time/Time/Unit/Nanosecond.lean index 626e760e7771..2003eaa4f783 100644 --- a/src/Std/Time/Time/Unit/Nanosecond.lean +++ b/src/Std/Time/Time/Unit/Nanosecond.lean @@ -13,7 +13,7 @@ public section namespace Std namespace Time namespace Nanosecond -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean index 6f81a7d7a8b4..a0472fc55c44 100644 --- a/src/Std/Time/Time/Unit/Second.lean +++ b/src/Std/Time/Time/Unit/Second.lean @@ -13,7 +13,7 @@ public import Std.Time.Time.Unit.Nanosecond namespace Std namespace Time namespace Second -open Internal +open Time.Internal set_option linter.all true diff --git a/src/Std/Time/Zoned/Database/Basic.lean b/src/Std/Time/Zoned/Database/Basic.lean index 9fdc2ba023f1..838a9d69128e 100644 --- a/src/Std/Time/Zoned/Database/Basic.lean +++ b/src/Std/Time/Zoned/Database/Basic.lean @@ -54,7 +54,7 @@ Converts a given time index into a `LocalTimeType` by using a time zone (`tz`) a -/ def convertLocalTimeType (index : Nat) (tz : TZif.TZifV1) (identifier : String) : Option LocalTimeType := do let localType ← tz.localTimeTypes[index]? - let offset := Offset.ofSeconds <| .ofInt localType.gmtOffset + let offset := Offset.ofSeconds <| .ofInt localType.gmtOffset.toInt let abbreviation := tz.abbreviations.getD index (offset.toIsoString true) let wallflag := convertWall (tz.stdWallIndicators.getD index true) let utLocal := convertUt (tz.utLocalIndicators.getD index true) @@ -73,7 +73,7 @@ Converts a transition. -/ def convertTransition (times: Array LocalTimeType) (index : Nat) (tz : TZif.TZifV1) : Option Transition := do let time := tz.transitionTimes[index]! - let time := Second.Offset.ofInt time + let time := Second.Offset.ofInt time.toInt let indice := tz.transitionIndices[index]! return { time, localTimeType := times[indice.toNat]! } diff --git a/src/Std/Time/Zoned/Database/TzIf.lean b/src/Std/Time/Zoned/Database/TzIf.lean index 116665f04417..05717ae4052b 100644 --- a/src/Std/Time/Zoned/Database/TzIf.lean +++ b/src/Std/Time/Zoned/Database/TzIf.lean @@ -8,6 +8,7 @@ module prelude public import Init.Data.Range.Polymorphic.Iterators public import Std.Internal.Parsec +public import Init.Data.SInt.Basic import Init.Data.Int.Repr public section @@ -22,10 +23,6 @@ open Std.Internal.Parsec Std.Internal.Parsec.ByteArray set_option linter.all true -local notation "Int32" => Int - -local notation "Int64" => Int - /-- Represents the header of a TZif file, containing metadata about the file's structure. -/ @@ -101,7 +98,7 @@ structure LeapSecond where /-- The correction applied during the leap second event in seconds. -/ - correction : Int64 + correction : Int32 deriving Repr, Inhabited /-- @@ -117,7 +114,7 @@ structure TZifV1 where /-- The array of transition times in seconds since the epoch. -/ - transitionTimes : Array Int32 + transitionTimes : Array Int64 /-- The array of local time type indices corresponding to each transition time. @@ -178,25 +175,6 @@ structure TZif where v2 : Option TZifV2 deriving Repr, Inhabited -private def toUInt32 (bs : ByteArray) : UInt32 := - assert! bs.size == 4 - (bs.get! 0).toUInt32 <<< 0x18 ||| - (bs.get! 1).toUInt32 <<< 0x10 ||| - (bs.get! 2).toUInt32 <<< 0x8 ||| - (bs.get! 3).toUInt32 - -private def toInt32 (bs : ByteArray) : Int32 := - let n := toUInt32 bs |>.toNat - if n < (1 <<< 31) - then Int.ofNat n - else Int.negOfNat (UInt32.size - n) - -private def toInt64 (bs : ByteArray) : Int64 := - let n := ByteArray.toUInt64BE! bs |>.toNat - if n < (1 <<< 63) - then Int.ofNat n - else Int.negOfNat (UInt64.size - n) - private def manyN (n : Nat) (p : Parser α) : Parser (Array α) := do let mut result := #[] for _ in *...n do @@ -204,10 +182,14 @@ private def manyN (n : Nat) (p : Parser α) : Parser (Array α) := do result := result.push x return result -private def pu64 : Parser UInt64 := ByteArray.toUInt64LE! <$> ByteSlice.toByteArray <$> take 8 -private def pi64 : Parser Int64 := toInt64 <$> ByteSlice.toByteArray <$> take 8 -private def pu32 : Parser UInt32 := toUInt32 <$> ByteSlice.toByteArray <$> take 4 -private def pi32 : Parser Int32 := toInt32 <$> ByteSlice.toByteArray <$> take 4 +private def pu64 : Parser UInt64 := do + let slice ← take 8 + return slice.byteArray.getUInt64BE! slice.start +private def pi64 : Parser Int64 := UInt64.toInt64 <$> pu64 +private def pu32 : Parser UInt32 := do + let slice ← take 4 + return slice.byteArray.getUInt32BE! slice.start +private def pi32 : Parser Int32 := UInt32.toInt32 <$> pu32 private def pu8 : Parser UInt8 := any private def pbool : Parser Bool := (· != 0) <$> pu8 @@ -227,12 +209,12 @@ private def parseLocalTimeType : Parser LocalTimeType := <*> pbool <*> pu8 -private def parseLeapSecond (p : Parser Int) : Parser LeapSecond := +private def parseLeapSecond (p : Parser Int64) : Parser LeapSecond := LeapSecond.mk <$> p <*> pi32 -private def parseTransitionTimes (size : Parser Int32) (n : UInt32) : Parser (Array Int32) := +private def parseTransitionTimes (size : Parser Int64) (n : UInt32) : Parser (Array Int64) := manyN (n.toNat) size private def parseTransitionIndices (n : UInt32) : Parser (Array UInt8) := @@ -258,7 +240,7 @@ private def parseAbbreviations (times : Array LocalTimeType) (n : UInt32) : Pars return strings -private def parseLeapSeconds (size : Parser Int) (n : UInt32) : Parser (Array LeapSecond) := +private def parseLeapSeconds (size : Parser Int64) (n : UInt32) : Parser (Array LeapSecond) := manyN (n.toNat) (parseLeapSecond size) private def parseIndicators (n : UInt32) : Parser (Array Bool) := @@ -267,11 +249,11 @@ private def parseIndicators (n : UInt32) : Parser (Array Bool) := private def parseTZifV1 : Parser TZifV1 := do let header ← parseHeader - let transitionTimes ← parseTransitionTimes pi32 header.timecnt + let transitionTimes ← parseTransitionTimes (Int32.toInt64 <$> pi32) header.timecnt let transitionIndices ← parseTransitionIndices header.timecnt let localTimeTypes ← parseLocalTimeTypes header.typecnt let abbreviations ← parseAbbreviations localTimeTypes header.charcnt - let leapSeconds ← parseLeapSeconds pi32 header.leapcnt + let leapSeconds ← parseLeapSeconds (Int32.toInt64 <$> pi32) header.leapcnt let stdWallIndicators ← parseIndicators header.isstdcnt let utLocalIndicators ← parseIndicators header.isutcnt diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index edb072aa3f11..06a261bd5933 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -20,6 +20,7 @@ Author: Leonardo de Moura #ifdef __cplusplus #include #include +#include #define _Atomic(t) std::atomic #define LEAN_USING_STD using namespace std; /* NOLINT */ extern "C" { @@ -1196,13 +1197,128 @@ LEAN_EXPORT lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b); static inline lean_object * lean_byte_array_uset(lean_obj_arg a, size_t i, uint8_t v) { lean_obj_res r; - if (lean_is_exclusive(a)) r = a; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; else r = lean_copy_byte_array(a); uint8_t * it = lean_sarray_cptr(r) + i; *it = v; return r; } +// The compiler should be able to compile these into single instructions +static inline uint16_t lean_byte_array_fget_uint16_be(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return ((uint16_t) ptr[0] << 8) | (uint16_t) ptr[1]; +} + +static inline uint16_t lean_byte_array_fget_uint16_le(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return (uint16_t) ptr[0] | ((uint16_t) ptr[1] << 8); +} + +static inline uint32_t lean_byte_array_fget_uint32_be(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return ((uint32_t) ptr[0] << 24) | ((uint32_t) ptr[1] << 16) | + ((uint32_t) ptr[2] << 8) | (uint32_t) ptr[3]; +} + +static inline uint32_t lean_byte_array_fget_uint32_le(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return (uint32_t) ptr[0] | ((uint32_t) ptr[1] << 8) | + ((uint32_t) ptr[2] << 16) | ((uint32_t) ptr[3] << 24); +} + +static inline uint64_t lean_byte_array_fget_uint64_be(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return ((uint64_t) ptr[0] << 56) | ((uint64_t) ptr[1] << 48) | + ((uint64_t) ptr[2] << 40) | ((uint64_t) ptr[3] << 32) | + ((uint64_t) ptr[4] << 24) | ((uint64_t) ptr[5] << 16) | + ((uint64_t) ptr[6] << 8) | (uint64_t) ptr[7]; +} + +static inline uint64_t lean_byte_array_fget_uint64_le(b_lean_obj_arg a, b_lean_obj_arg i) { + uint8_t* ptr = lean_sarray_cptr(a) + lean_unbox(i); + return (uint64_t) ptr[0] | ((uint64_t) ptr[1] << 8) | + ((uint64_t) ptr[2] << 16) | ((uint64_t) ptr[3] << 24) | + ((uint64_t) ptr[4] << 32) | ((uint64_t) ptr[5] << 40) | + ((uint64_t) ptr[6] << 48) | ((uint64_t) ptr[7] << 56); +} + +static inline lean_object * lean_byte_array_fset_uint16_be(lean_obj_arg a, b_lean_obj_arg i, uint16_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) (v >> 8); + *it++ = (uint8_t) v; + return r; +} + +static inline lean_object * lean_byte_array_fset_uint16_le(lean_obj_arg a, b_lean_obj_arg i, uint16_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) v; + *it++ = (uint8_t) (v >> 8); + return r; +} + +static inline lean_object * lean_byte_array_fset_uint32_be(lean_obj_arg a, b_lean_obj_arg i, uint32_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) (v >> 24); + *it++ = (uint8_t) (v >> 16); + *it++ = (uint8_t) (v >> 8); + *it++ = (uint8_t) v; + return r; +} + +static inline lean_object * lean_byte_array_fset_uint32_le(lean_obj_arg a, b_lean_obj_arg i, uint32_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) v; + *it++ = (uint8_t) (v >> 8); + *it++ = (uint8_t) (v >> 16); + *it++ = (uint8_t) (v >> 24); + return r; +} + +static inline lean_object * lean_byte_array_fset_uint64_be(lean_obj_arg a, b_lean_obj_arg i, uint64_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) (v >> 56); + *it++ = (uint8_t) (v >> 48); + *it++ = (uint8_t) (v >> 40); + *it++ = (uint8_t) (v >> 32); + *it++ = (uint8_t) (v >> 24); + *it++ = (uint8_t) (v >> 16); + *it++ = (uint8_t) (v >> 8); + *it++ = (uint8_t) v; + return r; +} + +static inline lean_object * lean_byte_array_fset_uint64_le(lean_obj_arg a, b_lean_obj_arg i, uint64_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + lean_unbox(i); + *it++ = (uint8_t) v; + *it++ = (uint8_t) (v >> 8); + *it++ = (uint8_t) (v >> 16); + *it++ = (uint8_t) (v >> 24); + *it++ = (uint8_t) (v >> 32); + *it++ = (uint8_t) (v >> 40); + *it++ = (uint8_t) (v >> 48); + *it++ = (uint8_t) (v >> 56); + return r; +} + static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) { if (!lean_is_scalar(i)) { return a; @@ -1220,6 +1336,25 @@ static inline lean_obj_res lean_byte_array_fset(lean_obj_arg a, b_lean_obj_arg i return lean_byte_array_uset(a, lean_unbox(i), b); } +LEAN_EXPORT lean_obj_res lean_byte_array_set_size(lean_obj_arg a, b_lean_obj_arg sz, b_lean_obj_arg orig_sz, uint8_t exact); + +#ifndef __cplusplus +void * memset(void * s, int c, size_t n); +int memcmp(const void * s1, const void * s2, size_t n); +#endif + +static inline lean_obj_res lean_byte_array_fill(lean_obj_arg a, b_lean_obj_arg b, b_lean_obj_arg s, uint8_t v) { + lean_obj_res r; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; + else r = lean_copy_byte_array(a); + memset(lean_sarray_cptr(r) + lean_unbox(b), v, lean_unbox(s)); + return r; +} + +static inline uint8_t lean_byte_array_slice_eq(b_lean_obj_arg b1, b_lean_obj_arg off1, b_lean_obj_arg b2, b_lean_obj_arg off2, b_lean_obj_arg len) { + return memcmp(lean_sarray_cptr(b1) + lean_unbox(off1), lean_sarray_cptr(b2) + lean_unbox(off2), lean_unbox(len)) == 0 ? 1 : 0; +} + /* FloatArray (special case of Array of Scalars) */ LEAN_EXPORT lean_obj_res lean_float_array_mk(lean_obj_arg a); @@ -1261,7 +1396,7 @@ LEAN_EXPORT lean_obj_res lean_float_array_push(lean_obj_arg a, double d); static inline lean_obj_res lean_float_array_uset(lean_obj_arg a, size_t i, double d) { lean_obj_res r; - if (lean_is_exclusive(a)) r = a; + if (LEAN_LIKELY(lean_is_exclusive(a))) r = a; else r = lean_copy_float_array(a); double * it = lean_float_array_cptr(r) + i; *it = d; diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 49213d7be079..81e023539c02 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2578,7 +2578,7 @@ extern "C" LEAN_EXPORT obj_res lean_copy_sarray(obj_arg a, size_t cap) { } obj_res lean_sarray_ensure_exclusive(obj_arg a) { - if (lean_is_exclusive(a)) { + if (LEAN_LIKELY(lean_is_exclusive(a))) { return a; } else { return lean_copy_sarray(a, lean_sarray_capacity(a)); @@ -2589,8 +2589,8 @@ obj_res lean_sarray_ensure_exclusive(obj_arg a) { If `exact` is false, double the capacity on copying. */ extern "C" LEAN_EXPORT obj_res lean_sarray_ensure_capacity(obj_arg a, size_t min_cap, bool exact) { size_t cap = lean_sarray_capacity(a); - if (min_cap <= cap) { - return a; + if (LEAN_LIKELY(min_cap <= cap)) { + return lean_sarray_ensure_exclusive(a); } else { return lean_copy_sarray(a, exact ? min_cap : min_cap * 2); } @@ -2627,7 +2627,7 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_data(obj_arg a) { } extern "C" LEAN_EXPORT obj_res lean_byte_array_push(obj_arg a, uint8 b) { - object * r = lean_sarray_ensure_exclusive(lean_sarray_ensure_capacity(a, lean_sarray_size(a) + 1, /* exact */ false)); + object * r = lean_sarray_ensure_capacity(a, lean_sarray_size(a) + 1, /* exact */ false); size_t & sz = lean_to_sarray(r)->m_size; uint8 * it = lean_sarray_cptr(r) + sz; *it = b; @@ -2635,7 +2635,18 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_push(obj_arg a, uint8 b) { return r; } - extern "C" LEAN_EXPORT obj_res lean_byte_array_copy_slice(b_obj_arg src, obj_arg o_src_off, obj_arg dest, obj_arg o_dest_off, obj_arg o_len, bool exact) { +extern "C" LEAN_EXPORT obj_res lean_byte_array_set_size(obj_arg a, b_obj_arg b, b_obj_arg n, uint8 exact) { + if (LEAN_LIKELY(lean_is_scalar(b))) { + size_t sz = lean_unbox(b); + object * r = lean_sarray_ensure_capacity(a, sz, exact); + lean_to_sarray(r)->m_size = sz; + return r; + } else { + lean_internal_panic_out_of_memory(); + } +} + +extern "C" LEAN_EXPORT obj_res lean_byte_array_copy_slice(b_obj_arg src, b_obj_arg o_src_off, obj_arg dest, b_obj_arg o_dest_off, b_obj_arg o_len, bool exact) { size_t ssz = lean_sarray_size(src); size_t dsz = lean_sarray_size(dest); size_t src_off = lean_nat_to_size_t(o_src_off); @@ -2648,7 +2659,7 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_push(obj_arg a, uint8 b) { dest_off = dsz; } size_t new_dsz = std::max(dsz, dest_off + len); - object * r = lean_sarray_ensure_exclusive(lean_sarray_ensure_capacity(dest, new_dsz, exact)); + object * r = lean_sarray_ensure_capacity(dest, new_dsz, exact); lean_to_sarray(r)->m_size = new_dsz; // `r` is exclusive, so the ranges definitely cannot overlap memcpy(lean_sarray_cptr(r) + dest_off, lean_sarray_cptr(src) + src_off, len); @@ -2690,7 +2701,7 @@ extern "C" LEAN_EXPORT obj_res lean_float_array_data(obj_arg a) { } extern "C" LEAN_EXPORT obj_res lean_float_array_push(obj_arg a, double d) { - object * r = lean_sarray_ensure_exclusive(lean_sarray_ensure_capacity(a, lean_sarray_size(a) + 1, /* exact */ false)); + object * r = lean_sarray_ensure_capacity(a, lean_sarray_size(a) + 1, /* exact */ false); size_t & sz = lean_to_sarray(r)->m_size; double * it = reinterpret_cast(lean_sarray_cptr(r)) + sz; *it = d; diff --git a/tests/elab/bytearray.lean b/tests/elab/bytearray.lean index 16f420bbe3ca..7f887643e971 100644 --- a/tests/elab/bytearray.lean +++ b/tests/elab/bytearray.lean @@ -1,3 +1,41 @@ +macro "#test " t:term : command => + `(#guard $t + example : $t := by decide_cbv) + +#test ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[4, 9, 5]⟩ 1 0 +#test ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[1, 2, 3]⟩ 0 3 +#test ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 1 3 +#test !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 0 3 +#test !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 0 1 +#test ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 3 1 +#test ByteArray.mk #[1, 2, 3] = ⟨#[1, 2, 3]⟩ +#test ByteArray.mk #[1, 2, 4] ≠ ⟨#[1, 2, 3]⟩ +#test ByteArray.mk #[] ≠ ⟨#[1, 2, 3]⟩ +#test ByteArray.mk #[1, 2, 3] ≠ ⟨#[]⟩ +#test ByteArray.mk #[] = ⟨#[]⟩ +#test ByteArray.mk #[0, 1, 5, 7] = ⟨#[0, 1, 5, 7]⟩ +#test ByteArray.mk #[0, 1, 5, 7] ≠ ⟨#[7, 5, 1, 0]⟩ +#test (ByteArray.replicate 10 42).data == #[42, 42, 42, 42, 42, 42, 42, 42, 42, 42] +#test (ByteArray.replicate 0 3).data == #[] +#test (ByteArray.replicate 3 0).data == #[0, 0, 0] +#test ((ByteArray.replicate 10 42).fill 3 5 0).data == #[42, 42, 42, 0, 0, 0, 0, 0, 42, 42] +#test (ByteArray.setSizeD ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] +#test (ByteArray.setSizeD ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] +#guard (ByteArray.setSizeD ⟨#[1, 2, 3, 4, 5, 6]⟩ 12345).size == 12345 + +#test ByteArray.getUInt16BE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0203 +#test ByteArray.getUInt16LE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0302 +#test ByteArray.getUInt32BE ⟨#[1, 2, 3, 4]⟩ 0 == 0x01020304 +#test ByteArray.getUInt32LE ⟨#[1, 2, 3, 4]⟩ 0 == 0x04030201 +#test ByteArray.getUInt64BE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x030405060708090A +#test ByteArray.getUInt64LE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x0A09080706050403 + +#test ByteArray.setUInt16BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 7, 8, 0, 0, 0]⟩ +#test ByteArray.setUInt16LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 8, 7, 0, 0, 0]⟩ +#test ByteArray.setUInt32BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 1, 5, 7, 8]⟩ +#test ByteArray.setUInt32LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 8, 7, 5, 1]⟩ +#test ByteArray.setUInt64BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[255, 3, 1, 4, 10, 11, 7, 8]⟩ +#test ByteArray.setUInt64LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[8, 7, 11, 10, 4, 1, 3, 255]⟩ def tst : IO Unit := do @@ -19,5 +57,5 @@ pure () #eval "abcd".hash #eval [97, 98, 99, 100].toByteArray.hash -#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x8877665544332211 -#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x1122334455667788 +#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.getUInt64LE! 0 == 0x8877665544332211 +#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.getUInt64BE! 0 == 0x1122334455667788