From 14b2d103d014a7015568e466b6cd67db85058682 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 29 Apr 2025 17:09:36 +0200 Subject: [PATCH 01/14] begin stuff --- .../Data/ByteArray/AdditionalOperations.lean | 421 ++++++++++++++++++ src/Init/Data/ByteArray/Basic.lean | 14 +- src/Init/Data/Nat/Internal.lean | 35 ++ src/include/lean/lean.h | 18 +- src/runtime/object.cpp | 25 +- 5 files changed, 497 insertions(+), 16 deletions(-) create mode 100644 src/Init/Data/ByteArray/AdditionalOperations.lean create mode 100644 src/Init/Data/Nat/Internal.lean diff --git a/src/Init/Data/ByteArray/AdditionalOperations.lean b/src/Init/Data/ByteArray/AdditionalOperations.lean new file mode 100644 index 000000000000..38bacdbbe0ca --- /dev/null +++ b/src/Init/Data/ByteArray/AdditionalOperations.lean @@ -0,0 +1,421 @@ +/- +Copyright (c) 2025 Robin Arnez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Robin Arnez +-/ +module + +prelude +import Init.Data.ByteArray.Basic +import Init.Data.Array.Lemmas +import Init.Data.UInt.Lemmas +import Init.Data.Nat.Internal + +set_option linter.missingDocs true + +namespace ByteArray + +private theorem helperLemma {x : USize} {y z : Nat} {a b : Nat} + (h : x.toNat + y ≤ z := by assumption) (h' : a + b ≤ y := by decide) : + (x + USize.ofNat a).toNat + b ≤ z := by + simp only [USize.toNat_add, USize.toNat_ofNat', Nat.add_mod_mod] + refine Nat.le_trans ?_ h + refine Nat.le_trans (Nat.add_le_add_right (Nat.mod_le ..) _) ?_ + rw [Nat.add_assoc] + exact Nat.add_le_add_left h' _ + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 16 bit little-endian unsigned integer. +-/ +def ugetUInt16LE (bs : ByteArray) (i : USize) + (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + let lo := bs.uget i (Nat.lt_of_add_right_lt h) + let hi := bs.uget (i + 1) (helperLemma (b := 1)) + lo.toUInt16 ||| (hi.toUInt16 <<< 8) + +set_option linter.unusedVariables.funArgs false in +@[inline] +private unsafe def getUInt16LEImpl (bs : ByteArray) (i : Nat) + (h : i + 2 ≤ bs.size) : UInt16 := + ugetUInt16LE bs (Nat.Internal.unbox i lcProof) lcProof + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 16 bit little-endian unsigned integer. +-/ +--@[implemented_by getUInt16LEImpl] +def getUInt16LE (bs : ByteArray) (i : Nat) (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + let lo := bs[i] + let hi := bs[i + 1] + lo.toUInt16 ||| (hi.toUInt16 <<< 8) + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 16 bit big-endian unsigned integer. +-/ +def ugetUInt16BE (bs : ByteArray) (i : USize) + (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + let hi := bs.uget i (Nat.lt_of_add_right_lt h) + let lo := bs.uget (i + 1) (helperLemma (b := 1)) + lo.toUInt16 ||| (hi.toUInt16 <<< 8) + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 32 bit little-endian unsigned integer. +-/ +def ugetUInt32LE (bs : ByteArray) (i : USize) + (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + --let b1 := bs.uget i (Nat.lt_of_add_right_lt h) + --let b2 := bs.uget (i + 1) helperLemma + --let b3 := bs.uget (i + 2) helperLemma + --let b4 := bs.uget (i + 3) helperLemma + --b1.toUInt32 ||| (b2.toUInt32 <<< 8) ||| (b3.toUInt32 <<< 16) ||| (b4.toUInt32 <<< 24) + let lo := bs.ugetUInt16LE i (Nat.le_of_add_right_le (k := 2) h) + let hi := bs.ugetUInt16LE (i + 2) helperLemma + lo.toUInt32 ||| (hi.toUInt32 <<< 16) + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 32 bit big-endian unsigned integer. +-/ +def ugetUInt32BE (bs : ByteArray) (i : USize) + (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + --let b4 := bs.uget i (Nat.lt_of_add_right_lt h) + --let b3 := bs.uget (i + 1) helperLemma + --let b2 := bs.uget (i + 2) helperLemma + --let b1 := bs.uget (i + 3) helperLemma + --b1.toUInt32 ||| (b2.toUInt32 <<< 8) ||| (b3.toUInt32 <<< 16) ||| (b4.toUInt32 <<< 24) + let hi := bs.ugetUInt16BE i (Nat.le_of_add_right_le (k := 2) h) + let lo := bs.ugetUInt16BE (i + 2) helperLemma + lo.toUInt32 ||| (hi.toUInt32 <<< 16) + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 64 bit little-endian unsigned integer. +-/ +def ugetUInt64LE (bs : ByteArray) (i : USize) + (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + --let b1 := bs.uget i (Nat.lt_of_add_right_lt h) + --let b2 := bs.uget (i + 1) helperLemma + --let b3 := bs.uget (i + 2) helperLemma + --let b4 := bs.uget (i + 3) helperLemma + --let b5 := bs.uget (i + 4) helperLemma + --let b6 := bs.uget (i + 5) helperLemma + --let b7 := bs.uget (i + 6) helperLemma + --let b8 := bs.uget (i + 7) helperLemma + --b1.toUInt64 ||| (b2.toUInt64 <<< 8) ||| (b3.toUInt64 <<< 16) ||| (b4.toUInt64 <<< 24) ||| + -- (b5.toUInt64 <<< 32) ||| (b2.toUInt64 <<< 40) ||| (b3.toUInt64 <<< 48) ||| (b4.toUInt64 <<< 56) + let lo := bs.ugetUInt32LE i (Nat.le_of_add_right_le (k := 4) h) + let hi := bs.ugetUInt32LE (i + 4) helperLemma + lo.toUInt64 ||| (hi.toUInt64 <<< 32) + +/-- +Interprets the value in the byte array `bs` starting at index `i` +as a 64 bit big-endian unsigned integer. +-/ +def ugetUInt64BE (bs : ByteArray) (i : USize) + (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + --let b8 := bs.uget i (Nat.lt_of_add_right_lt h) + --let b7 := bs.uget (i + 1) helperLemma + --let b6 := bs.uget (i + 2) helperLemma + --let b5 := bs.uget (i + 3) helperLemma + --let b4 := bs.uget (i + 4) helperLemma + --let b3 := bs.uget (i + 5) helperLemma + --let b2 := bs.uget (i + 6) helperLemma + --let b1 := bs.uget (i + 7) helperLemma + --b1.toUInt64 ||| (b2.toUInt64 <<< 8) ||| (b3.toUInt64 <<< 16) ||| (b4.toUInt64 <<< 24) ||| + -- (b5.toUInt64 <<< 32) ||| (b2.toUInt64 <<< 40) ||| (b3.toUInt64 <<< 48) ||| (b4.toUInt64 <<< 56) + let hi := bs.ugetUInt32BE i (Nat.le_of_add_right_le (k := 4) h) + let lo := bs.ugetUInt32BE (i + 4) helperLemma + lo.toUInt64 ||| (hi.toUInt64 <<< 32) + +@[simp] +theorem size_uset {bs : ByteArray} {i : USize} {val : UInt8} (h : i.toNat < bs.size) : + (bs.uset i val).size = bs.size := by + simp only [size, uset, Array.uset, Array.size_set] + +local macro "set_tac" : tactic => `(tactic| + ((try simp +zetaDelta only [size_uset]); first | exact helperLemma | exact helperLemma (b := 1))) + +/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ +def usetUInt16LE (bs : ByteArray) (i : USize) (val : UInt16) + (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := uset bs i val.toUInt8 (Nat.lt_of_add_right_lt h) + let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by simpa [bs] using helperLemma (b := 1)) + bs + +@[simp] +theorem size_usetUInt16LE {bs : ByteArray} {i : USize} {val : UInt16} + (h : i.toNat + 2 ≤ bs.size) : (bs.usetUInt16LE i val).size = bs.size := by + simp [usetUInt16LE] + +/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ +def usetUInt16BE (bs : ByteArray) (i : USize) (val : UInt16) + (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := uset bs i (val >>> 8).toUInt8 (Nat.lt_of_add_right_lt h) + let bs := uset bs (i + 1) val.toUInt8 (by simpa [bs] using helperLemma (b := 1)) + bs + +@[simp] +theorem size_usetUInt16BE {bs : ByteArray} {i : USize} {val : UInt16} + (h : i.toNat + 2 ≤ bs.size) : (bs.usetUInt16BE i val).size = bs.size := by + simp [usetUInt16BE] + +/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ +def usetUInt32LE (bs : ByteArray) (i : USize) (val : UInt32) + (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + /-let bs := uset bs i val.toUInt8 (Nat.lt_of_add_right_lt h) + let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by set_tac) + let bs := uset bs (i + 2) (val >>> 16).toUInt8 (by set_tac) + let bs := uset bs (i + 3) (val >>> 24).toUInt8 (by set_tac)-/ + let bs := usetUInt16LE bs i val.toUInt16 (Nat.le_of_add_right_le (k := 2) h) + let bs := usetUInt16LE bs (i + 2) (val >>> 16).toUInt16 (by simpa [bs] using helperLemma) + bs + +@[simp] +theorem size_usetUInt32LE {bs : ByteArray} {i : USize} {val : UInt32} + (h : i.toNat + 4 ≤ bs.size) : (bs.usetUInt32LE i val).size = bs.size := by + simp [usetUInt32LE] + +/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ +def usetUInt32BE (bs : ByteArray) (i : USize) (val : UInt32) + (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + /-let bs := uset bs i (val >>> 24).toUInt8 (by set_tac) + let bs := uset bs (i + 1) (val >>> 16).toUInt8 (by set_tac) + let bs := uset bs (i + 2) (val >>> 8).toUInt8 (by set_tac) + let bs := uset bs (i + 3) val.toUInt8 (by set_tac)-/ + let bs := usetUInt16BE bs i (val >>> 16).toUInt16 (Nat.le_of_add_right_le (k := 2) h) + let bs := usetUInt16BE bs (i + 2) val.toUInt16 (by simpa [bs] using helperLemma) + bs + +@[simp] +theorem size_usetUInt32BE {bs : ByteArray} {i : USize} {val : UInt32} + (h : i.toNat + 4 ≤ bs.size) : (bs.usetUInt32BE i val).size = bs.size := by + simp [usetUInt32BE] + +/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ +def usetUInt64LE (bs : ByteArray) (i : USize) (val : UInt64) + (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + /-let bs := uset bs i val.toUInt8 (by set_tac) + let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by set_tac) + let bs := uset bs (i + 2) (val >>> 16).toUInt8 (by set_tac) + let bs := uset bs (i + 3) (val >>> 24).toUInt8 (by set_tac) + let bs := uset bs (i + 4) (val >>> 32).toUInt8 (by set_tac) + let bs := uset bs (i + 5) (val >>> 40).toUInt8 (by set_tac) + let bs := uset bs (i + 6) (val >>> 48).toUInt8 (by set_tac) + let bs := uset bs (i + 7) (val >>> 56).toUInt8 (by set_tac)-/ + let bs := usetUInt32LE bs i val.toUInt32 (Nat.le_of_add_right_le (k := 4) h) + let bs := usetUInt32LE bs (i + 4) (val >>> 32).toUInt32 (by simpa [bs] using helperLemma) + bs + +@[simp] +theorem size_usetUInt64LE {bs : ByteArray} {i : USize} {val : UInt64} + (h : i.toNat + 8 ≤ bs.size) : (bs.usetUInt64LE i val).size = bs.size := by + simp [usetUInt64LE] + +/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ +def usetUInt64BE (bs : ByteArray) (i : USize) (val : UInt64) + (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + /-let bs := uset bs (i + 7) val.toUInt8 (by set_tac) + let bs := uset bs (i + 6) (val >>> 8).toUInt8 (by set_tac) + let bs := uset bs (i + 5) (val >>> 16).toUInt8 (by set_tac) + let bs := uset bs (i + 4) (val >>> 24).toUInt8 (by set_tac) + let bs := uset bs (i + 3) (val >>> 32).toUInt8 (by set_tac) + let bs := uset bs (i + 2) (val >>> 40).toUInt8 (by set_tac) + let bs := uset bs (i + 1) (val >>> 48).toUInt8 (by set_tac) + let bs := uset bs i (val >>> 56).toUInt8 (by set_tac)-/ + let bs := usetUInt32BE bs i (val >>> 32).toUInt32 (Nat.le_of_add_right_le (k := 4) h) + let bs := usetUInt32BE bs (i + 4) val.toUInt32 (by simpa [bs] using helperLemma) + bs + +@[simp] +theorem size_usetUInt64BE {bs : ByteArray} {i : USize} {val : UInt64} + (h : i.toNat + 8 ≤ bs.size) : (bs.usetUInt64BE i val).size = bs.size := by + simp [usetUInt64BE] + +theorem size_def (bs : ByteArray) : bs.size = bs.data.size := rfl + +@[simp] +theorem data_extract (bs : ByteArray) (b e : Nat) : + (bs.extract b e).data = bs.data.extract b e := by + simp only [extract, copySlice, empty, emptyWithCapacity, Array.extract_zero, Array.empty_append, + Nat.zero_add, Array.extract_empty, Array.append_empty] + by_cases h : b ≤ e + · rw [Nat.add_sub_cancel' h] + · rw [Nat.sub_eq_zero_of_le (Nat.le_of_not_le h), Nat.add_zero] + simp only [Nat.le_refl, Array.extract_empty_of_stop_le_start, Nat.le_of_not_le h] + +@[simp] +theorem size_extract (bs : ByteArray) (b e : Nat) : + (bs.extract b e).size = min e bs.size - b := by + simp [size_def] + +@[simp] +theorem data_append (as bs : ByteArray) : + (as ++ bs).data = as.data ++ bs.data := by + change (as.append bs).data = _ + simp only [ByteArray.append, copySlice, size_def, Array.extract_size, Nat.zero_add, Nat.sub_zero, + Nat.min_self, Nat.le_add_right, Array.extract_empty_of_size_le_start, Array.append_assoc, + Array.append_right_inj, Array.append_right_eq_self] + +@[simp] +theorem size_append (as bs : ByteArray) : (as ++ bs).size = as.size + bs.size := by + simp [size_def] + +@[simp] +theorem size_mk (xs : Array UInt8) : size (mk xs) = xs.size := rfl + +theorem getElem_def {xs : ByteArray} {i : Nat} (h : i < xs.size) : xs[i] = xs.data[i] := rfl + +/-- +Low-level function for growing or shrinking a byte array. + +Note: the contents of the bytes at the end are undefined when growing which is why +this function returns a `Squash`. + +If `exact` is `false`, the capacity will be doubled when grown. +-/ +@[extern "lean_byte_array_set_size"] +def setSize' (bs : ByteArray) (size : @& Nat) (exact : Bool := false) : + Squash { b : ByteArray // b.size = size ∧ ∀ (i : Nat) h h', b[i]'h = bs[i] } := by + let b := bs.extract 0 size ++ mk (Array.replicate (size - bs.size) 0) + refine Squash.mk ⟨b, ?_⟩ + have hsize : b.size = size := by simp [b] <;> omega + constructor + · exact hsize + · intro i h h' + rw [hsize] at h + rw [size_def] at h' + simp [b, getElem_def, h, h', Nat.lt_min] + +/-- +Replaces the bytes in the range `[start, start + size)` within `bs` with `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 + +@[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_def] at h + simp [fill', copySlice, size_def] <;> 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_def, 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 + +@[ext] +theorem ext {as bs : ByteArray} (h : as.size = bs.size) + (h' : ∀ (i : Nat) h h', as[i]'h = bs[i]) : as = bs := by + rcases as with ⟨xs⟩ + rcases bs with ⟨ys⟩ + congr + exact Array.ext h h' + +/-- +Grows or shrinks a byte array. When growing, additional bytes are filled with zeroes. +-/ +def setSize (bs : ByteArray) (size : Nat) (exact : Bool := false) : ByteArray := + Quot.liftOn (setSize' bs size exact) + (fun bs' => if h : bs.size < size then bs'.1.fill' bs.size (size - bs.size) 0 else bs'.1) + (fun a b _ => by + dsimp + split + · ext + · simp [a.2, b.2] + · simp only [getElem_fill'] + split + · rfl + · rename_i hsize i h h' h'' + simp only [size_fill', a.2.1] at h + simp only [Nat.le_of_lt hsize, Nat.add_sub_cancel', h, and_true, Nat.not_le] at h'' + rw [a.2.2 i _ h'', b.2.2 i _ h''] + · ext + · simp [a.2, b.2] + · rename_i hbs i h h' + replace hbs := Nat.le_of_not_lt hbs + rw [a.2.1] at h + rw [a.2.2 i _ (Nat.lt_of_lt_of_le h hbs), + b.2.2 i _ (Nat.lt_of_lt_of_le h hbs)]) + +@[simp] +theorem size_setSize (bs : ByteArray) (size : Nat) (exact : Bool) : + (bs.setSize size exact).size = size := by + rw [setSize] + rcases bs.setSize' size exact with ⟨bs⟩ + dsimp [Quot.liftOn] + split <;> simp [bs.2] + +theorem getElem_setSize {bs : ByteArray} {size : Nat} {exact : Bool} {i : Nat} + (h : i < (bs.setSize size exact).size) : + (bs.setSize size exact)[i] = if h : i < bs.size then bs[i] else 0 := by + rw [size_setSize] at h + simp only [setSize] + have ⟨q, hq⟩ : { a // bs.setSize' size exact = a } := ⟨_, rfl⟩ + rcases q with ⟨a⟩ + simp only [Quot.liftOn, hq] + split + · simp only [getElem_fill'] + split + · rename_i h + rw [dif_neg (Nat.not_lt_of_le h.1)] + · rename_i h h' h'' + simp only [Nat.le_of_lt h', Nat.add_sub_cancel', h, and_true, Nat.not_le] at h'' + rw [a.2.2 i _ h'', dif_pos h''] + · rename_i h h' + replace h' := Nat.lt_of_lt_of_le h (Nat.le_of_not_lt h') + rw [a.2.2 i _ h', dif_pos h'] + +theorem getElem_setSize_eq_getElem {bs : ByteArray} {size : Nat} {exact : Bool} {i : Nat} + {h : i < (bs.setSize size exact).size} (h' : i < bs.size) : + (bs.setSize size exact)[i] = bs[i] := by + simp only [getElem_setSize, h', ↓reduceDIte] + +theorem setSize'_eq_setSize (bs : ByteArray) (size : Nat) (exact : Bool) : + bs.setSize' size exact = Squash.mk ⟨bs.setSize size exact, + size_setSize .., @getElem_setSize_eq_getElem bs size exact⟩ := + Subsingleton.allEq .. + +/-- +Creates an array that contains n repetitions of the byte v. +-/ +def replicate (n : Nat) (v : UInt8) := + Quot.liftOn ((emptyWithCapacity n).setSize' n) + (fun x => x.1.fill' 0 n v) + (fun a b _ => by + ext + · simp [a.2, b.2] + · rename_i h + simp only [size_fill', b.2] at h + simp [getElem_fill', h]) + +@[simp] +theorem _root_.Array.extract_size' {xs : Array α} {size : Nat} (h : size = xs.size) : + xs.extract 0 size = xs := by + rw [h, Array.extract_size] + +@[simp] +theorem data_replicate (size : Nat) (value : UInt8) : + (replicate size value).data = Array.replicate size value := by + simp only [replicate] + cases (emptyWithCapacity size).setSize' size using Quot.ind with | mk a => ?_ + simp [Quot.liftOn, fill', copySlice, ← size_def, Array.extract_empty_of_size_le_start, a.2] + +end ByteArray diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index df1425eafa6b..7ed4727b3c54 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -86,10 +86,12 @@ 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. -/ +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. +-/ @[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⟩ def extract (a : ByteArray) (b e : Nat) : ByteArray := @@ -132,10 +134,10 @@ def toList (bs : ByteArray) : List UInt8 := 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. +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. - TODO: avoid code duplication in the future after we improve the compiler. +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 diff --git a/src/Init/Data/Nat/Internal.lean b/src/Init/Data/Nat/Internal.lean new file mode 100644 index 000000000000..870751d29358 --- /dev/null +++ b/src/Init/Data/Nat/Internal.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2025 Robin Arnez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Robin Arnez +-/ +module + +prelude +import Init.Data.UInt.Basic + +@[inline] +private unsafe def Nat.Internal.isScalarImpl (x : Nat) : Bool := + ptrAddrUnsafe x &&& 1 == 1 + +/-- +Low-level function that returns whether the provided number is a "small natural number". + +Small natural numbers are not allocated on the heap but instead have +their value encoded directly in their pointer address. +-/ +@[implemented_by isScalarImpl] +def Nat.Internal.isScalar (x : Nat) : Bool := + x < USize.size / 2 + +set_option linter.unusedVariables.funArgs false in +@[inline] +private unsafe def Nat.Internal.unboxImpl (x : Nat) (h : isScalar x) : USize := + ptrAddrUnsafe x >>> 1 + +/-- +Low-level function that returns the `USize` value of a small natural number (see `isScalar`). +-/ +@[implemented_by unboxImpl] +def Nat.Internal.unbox (x : Nat) (h : isScalar x) : USize := + USize.ofNat x diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 34fee1550b7f..82e75927ebf5 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -839,7 +839,7 @@ static inline lean_obj_res lean_copy_array(lean_obj_arg a) { } static inline lean_obj_res lean_ensure_exclusive_array(lean_obj_arg a) { - if (lean_is_exclusive(a)) return a; + if (LEAN_LIKELY(lean_is_exclusive(a))) return a; return lean_copy_array(a); } @@ -969,7 +969,7 @@ 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; @@ -993,6 +993,18 @@ 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, uint8_t exact); + +void * memset(void * ptr, int c, size_t n); + +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), lean_unbox(s), v); + return r; +} + /* FloatArray (special case of Array of Scalars) */ LEAN_EXPORT lean_obj_res lean_float_array_mk(lean_obj_arg a); @@ -1034,7 +1046,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 068d0c264dc8..e5fd9b007eb6 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2337,7 +2337,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)); @@ -2348,8 +2348,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); } @@ -2386,7 +2386,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; @@ -2394,7 +2394,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, 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); @@ -2407,7 +2418,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); @@ -2449,7 +2460,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; From 5cff12b494234c20098dfed932cf64670554ab2a Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 29 Apr 2025 19:05:46 +0200 Subject: [PATCH 02/14] more stuff --- src/Init/Data/ByteArray.lean | 1 + .../Data/ByteArray/AdditionalOperations.lean | 33 +++++++++++++++++++ src/Init/Data/String/Extra.lean | 2 +- src/include/lean/lean.h | 9 +++-- tests/lean/run/bytearray.lean | 22 +++++++++++++ 5 files changed, 64 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/bytearray.lean diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index 2e513d63f46e..d7ea86170112 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -7,3 +7,4 @@ module prelude import Init.Data.ByteArray.Basic +import Init.Data.ByteArray.AdditionalOperations diff --git a/src/Init/Data/ByteArray/AdditionalOperations.lean b/src/Init/Data/ByteArray/AdditionalOperations.lean index 38bacdbbe0ca..850f0da40769 100644 --- a/src/Init/Data/ByteArray/AdditionalOperations.lean +++ b/src/Init/Data/ByteArray/AdditionalOperations.lean @@ -418,4 +418,37 @@ theorem data_replicate (size : Nat) (value : UInt8) : cases (emptyWithCapacity size).setSize' size using Quot.ind with | mk a => ?_ simp [Quot.liftOn, fill', copySlice, ← size_def, Array.extract_empty_of_size_le_start, a.2] +/-- +Return true iff the slices `[asOff, asOff + len)` in `as` and `[bsOff, bsOff + len)` in +`bs` contain the same data. +-/ +@[extern "lean_byte_array_slice_eq"] +def sliceEq' (as : @& ByteArray) (asOff : @& Nat) (bs : @& ByteArray) (bsOff : @& Nat) (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 whether two byte arrays are equal. + +The notation `==` is preferred over using this function directly. +-/ +protected def beq (as bs : ByteArray) : Bool := + if h : as.size = bs.size then + sliceEq' as 0 bs 0 as.size + else + false + +protected theorem beq_iff_eq {as bs : ByteArray} : as.beq bs ↔ as = bs := by + dsimp [ByteArray.beq] + split + · rename_i h + simp [sliceEq', ← size_def, h] + exact ⟨fun h => (h ▸ rfl : mk as.data = mk bs.data), fun h => h ▸ rfl⟩ + · rename_i h + simp [ne_of_apply_ne size h] + +instance : DecidableEq ByteArray := fun _ _ => + decidable_of_decidable_of_iff ByteArray.beq_iff_eq + end ByteArray diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 6104d9bd17bd..3f79c84e336f 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -6,7 +6,7 @@ Author: Leonardo de Moura module prelude -import Init.Data.ByteArray +import Init.Data.ByteArray.Basic import Init.Data.UInt.Lemmas namespace String diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 82e75927ebf5..03dc82887fcb 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -995,16 +995,21 @@ static inline lean_obj_res lean_byte_array_fset(lean_obj_arg a, b_lean_obj_arg i LEAN_EXPORT lean_obj_res lean_byte_array_set_size(lean_obj_arg a, b_lean_obj_arg sz, uint8_t exact); -void * memset(void * ptr, int c, size_t n); +void * memset(void * s, int c, size_t n); +int memcmp(const void * s1, const void * s2, size_t n); 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), lean_unbox(s), v); + 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); diff --git a/tests/lean/run/bytearray.lean b/tests/lean/run/bytearray.lean new file mode 100644 index 000000000000..73b5b607db69 --- /dev/null +++ b/tests/lean/run/bytearray.lean @@ -0,0 +1,22 @@ +import Init.Data.ByteArray.AdditionalOperations + +#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[4, 9, 5]⟩ 1 0 +#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[1, 2, 3]⟩ 0 3 +#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 1 3 +#guard !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 0 3 +#guard !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 0 1 +#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 3 1 +#guard ByteArray.mk #[1, 2, 3] = ⟨#[1, 2, 3]⟩ +#guard ByteArray.mk #[1, 2, 4] ≠ ⟨#[1, 2, 3]⟩ +#guard ByteArray.mk #[] ≠ ⟨#[1, 2, 3]⟩ +#guard ByteArray.mk #[1, 2, 3] ≠ ⟨#[]⟩ +#guard ByteArray.mk #[] = ⟨#[]⟩ +#guard ByteArray.mk #[0, 1, 5, 7] = ⟨#[0, 1, 5, 7]⟩ +#guard ByteArray.mk #[0, 1, 5, 7] ≠ ⟨#[7, 5, 1, 0]⟩ +#guard (ByteArray.replicate 10 42).data == #[42, 42, 42, 42, 42, 42, 42, 42, 42, 42] +#guard (ByteArray.replicate 0 3).data == #[] +#guard (ByteArray.replicate 3 0).data == #[0, 0, 0] +#guard ((ByteArray.replicate 10 42).fill' 3 5 0).data == #[42, 42, 42, 0, 0, 0, 0, 0, 42, 42] +#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] +#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] +#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 12345).size == 12345 From dd131bad63d063a9763b5ff387167f78cb9c42cb Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 29 Apr 2025 19:18:46 +0200 Subject: [PATCH 03/14] fix stuff --- src/include/lean/lean.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 03dc82887fcb..cc24a6eda794 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -995,8 +995,10 @@ static inline lean_obj_res lean_byte_array_fset(lean_obj_arg a, b_lean_obj_arg i LEAN_EXPORT lean_obj_res lean_byte_array_set_size(lean_obj_arg a, b_lean_obj_arg 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; From 9b6a907d266e65dc16c7744708567aa32d7bfe7f Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 29 Apr 2025 19:27:32 +0200 Subject: [PATCH 04/14] more fix --- src/include/lean/lean.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index cc24a6eda794..f1c97f1dcb7f 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -19,6 +19,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" { From b2ee2e5ac2ff4a5295b3aefbe7137d9da7aba1c9 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 29 Apr 2025 22:04:16 +0200 Subject: [PATCH 05/14] expand test --- tests/lean/run/bytearray.lean | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/bytearray.lean b/tests/lean/run/bytearray.lean index 73b5b607db69..93f2414b5cb4 100644 --- a/tests/lean/run/bytearray.lean +++ b/tests/lean/run/bytearray.lean @@ -1,5 +1,3 @@ -import Init.Data.ByteArray.AdditionalOperations - #guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[4, 9, 5]⟩ 1 0 #guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[1, 2, 3]⟩ 0 3 #guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 1 3 @@ -20,3 +18,17 @@ import Init.Data.ByteArray.AdditionalOperations #guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] #guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] #guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 12345).size == 12345 + +#guard ByteArray.ugetUInt16BE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0203 +#guard ByteArray.ugetUInt16LE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0302 +#guard ByteArray.ugetUInt32BE ⟨#[1, 2, 3, 4]⟩ 0 == 0x01020304 +#guard ByteArray.ugetUInt32LE ⟨#[1, 2, 3, 4]⟩ 0 == 0x04030201 +#guard ByteArray.ugetUInt64BE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x030405060708090A +#guard ByteArray.ugetUInt64LE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x0A09080706050403 + +#guard ByteArray.usetUInt16BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 7, 8, 0, 0, 0]⟩ +#guard ByteArray.usetUInt16LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 8, 7, 0, 0, 0]⟩ +#guard ByteArray.usetUInt32BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 1, 5, 7, 8]⟩ +#guard ByteArray.usetUInt32LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 8, 7, 5, 1]⟩ +#guard ByteArray.usetUInt64BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[255, 3, 1, 4, 10, 11, 7, 8]⟩ +#guard ByteArray.usetUInt64LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[8, 7, 11, 10, 4, 1, 3, 255]⟩ From cec171adb2fce022196eeb74361897dec3649a25 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Mon, 28 Jul 2025 11:38:27 +0200 Subject: [PATCH 06/14] cleanup everything and use native implementations --- .../Data/ByteArray/AdditionalOperations.lean | 279 ++++++++---------- src/Init/Data/ByteArray/Basic.lean | 7 - src/Init/Data/Nat/Internal.lean | 8 +- src/include/lean/lean.h | 115 ++++++++ 4 files changed, 238 insertions(+), 171 deletions(-) diff --git a/src/Init/Data/ByteArray/AdditionalOperations.lean b/src/Init/Data/ByteArray/AdditionalOperations.lean index 850f0da40769..f1e1d839a1b5 100644 --- a/src/Init/Data/ByteArray/AdditionalOperations.lean +++ b/src/Init/Data/ByteArray/AdditionalOperations.lean @@ -6,46 +6,25 @@ Author: Robin Arnez module prelude -import Init.Data.ByteArray.Basic -import Init.Data.Array.Lemmas -import Init.Data.UInt.Lemmas -import Init.Data.Nat.Internal +public import Init.Data.ByteArray.Basic +public import Init.Data.Array.Lemmas +public import Init.Data.UInt.Lemmas +public import Init.Data.Nat.Internal +public import Init.Grind set_option linter.missingDocs true -namespace ByteArray - -private theorem helperLemma {x : USize} {y z : Nat} {a b : Nat} - (h : x.toNat + y ≤ z := by assumption) (h' : a + b ≤ y := by decide) : - (x + USize.ofNat a).toNat + b ≤ z := by - simp only [USize.toNat_add, USize.toNat_ofNat', Nat.add_mod_mod] - refine Nat.le_trans ?_ h - refine Nat.le_trans (Nat.add_le_add_right (Nat.mod_le ..) _) ?_ - rw [Nat.add_assoc] - exact Nat.add_le_add_left h' _ +public section -/-- -Interprets the value in the byte array `bs` starting at index `i` -as a 16 bit little-endian unsigned integer. --/ -def ugetUInt16LE (bs : ByteArray) (i : USize) - (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := - let lo := bs.uget i (Nat.lt_of_add_right_lt h) - let hi := bs.uget (i + 1) (helperLemma (b := 1)) - lo.toUInt16 ||| (hi.toUInt16 <<< 8) - -set_option linter.unusedVariables.funArgs false in -@[inline] -private unsafe def getUInt16LEImpl (bs : ByteArray) (i : Nat) - (h : i + 2 ≤ bs.size) : UInt16 := - ugetUInt16LE bs (Nat.Internal.unbox i lcProof) lcProof +namespace ByteArray /-- Interprets the value in the byte array `bs` starting at index `i` as a 16 bit little-endian unsigned integer. -/ ---@[implemented_by getUInt16LEImpl] -def getUInt16LE (bs : ByteArray) (i : Nat) (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := +@[extern "lean_byte_array_fget_uint16_le"] +def getUInt16LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := let lo := bs[i] let hi := bs[i + 1] lo.toUInt16 ||| (hi.toUInt16 <<< 8) @@ -54,185 +33,144 @@ def getUInt16LE (bs : ByteArray) (i : Nat) (h : i + 2 ≤ bs.size := by get_elem Interprets the value in the byte array `bs` starting at index `i` as a 16 bit big-endian unsigned integer. -/ -def ugetUInt16BE (bs : ByteArray) (i : USize) - (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := - let hi := bs.uget i (Nat.lt_of_add_right_lt h) - let lo := bs.uget (i + 1) (helperLemma (b := 1)) +@[extern "lean_byte_array_fget_uint16_be"] +def getUInt16BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := + let hi := bs[i] + let lo := bs[i + 1] lo.toUInt16 ||| (hi.toUInt16 <<< 8) /-- Interprets the value in the byte array `bs` starting at index `i` as a 32 bit little-endian unsigned integer. -/ -def ugetUInt32LE (bs : ByteArray) (i : USize) - (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := - --let b1 := bs.uget i (Nat.lt_of_add_right_lt h) - --let b2 := bs.uget (i + 1) helperLemma - --let b3 := bs.uget (i + 2) helperLemma - --let b4 := bs.uget (i + 3) helperLemma - --b1.toUInt32 ||| (b2.toUInt32 <<< 8) ||| (b3.toUInt32 <<< 16) ||| (b4.toUInt32 <<< 24) - let lo := bs.ugetUInt16LE i (Nat.le_of_add_right_le (k := 2) h) - let hi := bs.ugetUInt16LE (i + 2) helperLemma +@[extern "lean_byte_array_fget_uint32_le"] +def getUInt32LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + let lo := bs.getUInt16LE i + let hi := bs.getUInt16LE (i + 2) lo.toUInt32 ||| (hi.toUInt32 <<< 16) /-- Interprets the value in the byte array `bs` starting at index `i` as a 32 bit big-endian unsigned integer. -/ -def ugetUInt32BE (bs : ByteArray) (i : USize) - (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := - --let b4 := bs.uget i (Nat.lt_of_add_right_lt h) - --let b3 := bs.uget (i + 1) helperLemma - --let b2 := bs.uget (i + 2) helperLemma - --let b1 := bs.uget (i + 3) helperLemma - --b1.toUInt32 ||| (b2.toUInt32 <<< 8) ||| (b3.toUInt32 <<< 16) ||| (b4.toUInt32 <<< 24) - let hi := bs.ugetUInt16BE i (Nat.le_of_add_right_le (k := 2) h) - let lo := bs.ugetUInt16BE (i + 2) helperLemma +@[extern "lean_byte_array_fget_uint32_be"] +def getUInt32BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := + let hi := bs.getUInt16BE i + let lo := bs.getUInt16BE (i + 2) lo.toUInt32 ||| (hi.toUInt32 <<< 16) /-- Interprets the value in the byte array `bs` starting at index `i` as a 64 bit little-endian unsigned integer. -/ -def ugetUInt64LE (bs : ByteArray) (i : USize) - (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := - --let b1 := bs.uget i (Nat.lt_of_add_right_lt h) - --let b2 := bs.uget (i + 1) helperLemma - --let b3 := bs.uget (i + 2) helperLemma - --let b4 := bs.uget (i + 3) helperLemma - --let b5 := bs.uget (i + 4) helperLemma - --let b6 := bs.uget (i + 5) helperLemma - --let b7 := bs.uget (i + 6) helperLemma - --let b8 := bs.uget (i + 7) helperLemma - --b1.toUInt64 ||| (b2.toUInt64 <<< 8) ||| (b3.toUInt64 <<< 16) ||| (b4.toUInt64 <<< 24) ||| - -- (b5.toUInt64 <<< 32) ||| (b2.toUInt64 <<< 40) ||| (b3.toUInt64 <<< 48) ||| (b4.toUInt64 <<< 56) - let lo := bs.ugetUInt32LE i (Nat.le_of_add_right_le (k := 4) h) - let hi := bs.ugetUInt32LE (i + 4) helperLemma +@[extern "lean_byte_array_fget_uint64_le"] +def getUInt64LE (bs : @& ByteArray) (i : @& Nat) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + let lo := bs.getUInt32LE i + let hi := bs.getUInt32LE (i + 4) lo.toUInt64 ||| (hi.toUInt64 <<< 32) /-- Interprets the value in the byte array `bs` starting at index `i` as a 64 bit big-endian unsigned integer. -/ -def ugetUInt64BE (bs : ByteArray) (i : USize) - (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := - --let b8 := bs.uget i (Nat.lt_of_add_right_lt h) - --let b7 := bs.uget (i + 1) helperLemma - --let b6 := bs.uget (i + 2) helperLemma - --let b5 := bs.uget (i + 3) helperLemma - --let b4 := bs.uget (i + 4) helperLemma - --let b3 := bs.uget (i + 5) helperLemma - --let b2 := bs.uget (i + 6) helperLemma - --let b1 := bs.uget (i + 7) helperLemma - --b1.toUInt64 ||| (b2.toUInt64 <<< 8) ||| (b3.toUInt64 <<< 16) ||| (b4.toUInt64 <<< 24) ||| - -- (b5.toUInt64 <<< 32) ||| (b2.toUInt64 <<< 40) ||| (b3.toUInt64 <<< 48) ||| (b4.toUInt64 <<< 56) - let hi := bs.ugetUInt32BE i (Nat.le_of_add_right_le (k := 4) h) - let lo := bs.ugetUInt32BE (i + 4) helperLemma +@[extern "lean_byte_array_fget_uint64_be"] +def getUInt64BE (bs : @& ByteArray) (i : @& Nat) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := + let hi := bs.getUInt32BE i + let lo := bs.getUInt32BE (i + 4) lo.toUInt64 ||| (hi.toUInt64 <<< 32) -@[simp] +@[simp, grind =] theorem size_uset {bs : ByteArray} {i : USize} {val : UInt8} (h : i.toNat < bs.size) : (bs.uset i val).size = bs.size := by - simp only [size, uset, Array.uset, Array.size_set] + simp [size, uset] -local macro "set_tac" : tactic => `(tactic| - ((try simp +zetaDelta only [size_uset]); first | exact helperLemma | exact helperLemma (b := 1))) +@[simp, grind =] +theorem size_set {bs : ByteArray} {i : Nat} {val : UInt8} (h : i < bs.size) : + (bs.set i val).size = bs.size := by + simp [size, set] /-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -def usetUInt16LE (bs : ByteArray) (i : USize) (val : UInt16) - (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := uset bs i val.toUInt8 (Nat.lt_of_add_right_lt h) - let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by simpa [bs] using helperLemma (b := 1)) +@[extern "lean_byte_array_fset_uint16_le"] +def setUInt16LE (bs : ByteArray) (i : @& Nat) (val : UInt16) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.set i val.toUInt8 + let bs := bs.set (i + 1) (val >>> 8).toUInt8 (by grind) bs -@[simp] -theorem size_usetUInt16LE {bs : ByteArray} {i : USize} {val : UInt16} - (h : i.toNat + 2 ≤ bs.size) : (bs.usetUInt16LE i val).size = bs.size := by - simp [usetUInt16LE] +@[simp, grind =] +theorem size_setUInt16LE {bs : ByteArray} {i : Nat} {val : UInt16} + (h : i + 2 ≤ bs.size) : (bs.setUInt16LE i val).size = bs.size := by + simp [setUInt16LE] /-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -def usetUInt16BE (bs : ByteArray) (i : USize) (val : UInt16) - (h : i.toNat + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := uset bs i (val >>> 8).toUInt8 (Nat.lt_of_add_right_lt h) - let bs := uset bs (i + 1) val.toUInt8 (by simpa [bs] using helperLemma (b := 1)) +@[extern "lean_byte_array_fset_uint16_be"] +def setUInt16BE (bs : ByteArray) (i : @& Nat) (val : UInt16) + (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.set i (val >>> 8).toUInt8 + let bs := bs.set (i + 1) val.toUInt8 (by grind) bs -@[simp] -theorem size_usetUInt16BE {bs : ByteArray} {i : USize} {val : UInt16} - (h : i.toNat + 2 ≤ bs.size) : (bs.usetUInt16BE i val).size = bs.size := by - simp [usetUInt16BE] +@[simp, grind =] +theorem size_setUInt16BE {bs : ByteArray} {i : Nat} {val : UInt16} + (h : i + 2 ≤ bs.size) : (bs.setUInt16BE i val).size = bs.size := by + simp [setUInt16BE] /-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -def usetUInt32LE (bs : ByteArray) (i : USize) (val : UInt32) - (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := - /-let bs := uset bs i val.toUInt8 (Nat.lt_of_add_right_lt h) - let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by set_tac) - let bs := uset bs (i + 2) (val >>> 16).toUInt8 (by set_tac) - let bs := uset bs (i + 3) (val >>> 24).toUInt8 (by set_tac)-/ - let bs := usetUInt16LE bs i val.toUInt16 (Nat.le_of_add_right_le (k := 2) h) - let bs := usetUInt16LE bs (i + 2) (val >>> 16).toUInt16 (by simpa [bs] using helperLemma) +@[extern "lean_byte_array_fset_uint32_le"] +def setUInt32LE (bs : ByteArray) (i : @& Nat) (val : UInt32) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.setUInt16LE i val.toUInt16 + let bs := bs.setUInt16LE (i + 2) (val >>> 16).toUInt16 (by grind) bs -@[simp] -theorem size_usetUInt32LE {bs : ByteArray} {i : USize} {val : UInt32} - (h : i.toNat + 4 ≤ bs.size) : (bs.usetUInt32LE i val).size = bs.size := by - simp [usetUInt32LE] +@[simp, grind =] +theorem size_setUInt32LE {bs : ByteArray} {i : Nat} {val : UInt32} + (h : i + 4 ≤ bs.size) : (bs.setUInt32LE i val).size = bs.size := by + simp [setUInt32LE] /-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -def usetUInt32BE (bs : ByteArray) (i : USize) (val : UInt32) - (h : i.toNat + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := - /-let bs := uset bs i (val >>> 24).toUInt8 (by set_tac) - let bs := uset bs (i + 1) (val >>> 16).toUInt8 (by set_tac) - let bs := uset bs (i + 2) (val >>> 8).toUInt8 (by set_tac) - let bs := uset bs (i + 3) val.toUInt8 (by set_tac)-/ - let bs := usetUInt16BE bs i (val >>> 16).toUInt16 (Nat.le_of_add_right_le (k := 2) h) - let bs := usetUInt16BE bs (i + 2) val.toUInt16 (by simpa [bs] using helperLemma) +@[extern "lean_byte_array_fset_uint32_be"] +def setUInt32BE (bs : ByteArray) (i : @& Nat) (val : UInt32) + (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.setUInt16BE i (val >>> 16).toUInt16 + let bs := bs.setUInt16BE (i + 2) val.toUInt16 (by grind) bs -@[simp] -theorem size_usetUInt32BE {bs : ByteArray} {i : USize} {val : UInt32} - (h : i.toNat + 4 ≤ bs.size) : (bs.usetUInt32BE i val).size = bs.size := by - simp [usetUInt32BE] +@[simp, grind =] +theorem size_setUInt32BE {bs : ByteArray} {i : Nat} {val : UInt32} + (h : i + 4 ≤ bs.size) : (bs.setUInt32BE i val).size = bs.size := by + simp [setUInt32BE] /-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -def usetUInt64LE (bs : ByteArray) (i : USize) (val : UInt64) - (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := - /-let bs := uset bs i val.toUInt8 (by set_tac) - let bs := uset bs (i + 1) (val >>> 8).toUInt8 (by set_tac) - let bs := uset bs (i + 2) (val >>> 16).toUInt8 (by set_tac) - let bs := uset bs (i + 3) (val >>> 24).toUInt8 (by set_tac) - let bs := uset bs (i + 4) (val >>> 32).toUInt8 (by set_tac) - let bs := uset bs (i + 5) (val >>> 40).toUInt8 (by set_tac) - let bs := uset bs (i + 6) (val >>> 48).toUInt8 (by set_tac) - let bs := uset bs (i + 7) (val >>> 56).toUInt8 (by set_tac)-/ - let bs := usetUInt32LE bs i val.toUInt32 (Nat.le_of_add_right_le (k := 4) h) - let bs := usetUInt32LE bs (i + 4) (val >>> 32).toUInt32 (by simpa [bs] using helperLemma) +@[extern "lean_byte_array_fset_uint64_le"] +def setUInt64LE (bs : ByteArray) (i : @& Nat) (val : UInt64) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.setUInt32LE i val.toUInt32 + let bs := bs.setUInt32LE (i + 4) (val >>> 32).toUInt32 (by grind) bs -@[simp] -theorem size_usetUInt64LE {bs : ByteArray} {i : USize} {val : UInt64} - (h : i.toNat + 8 ≤ bs.size) : (bs.usetUInt64LE i val).size = bs.size := by - simp [usetUInt64LE] +@[simp, grind =] +theorem size_setUInt64LE {bs : ByteArray} {i : Nat} {val : UInt64} + (h : i + 8 ≤ bs.size) : (bs.setUInt64LE i val).size = bs.size := by + simp [setUInt64LE] /-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -def usetUInt64BE (bs : ByteArray) (i : USize) (val : UInt64) - (h : i.toNat + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := - /-let bs := uset bs (i + 7) val.toUInt8 (by set_tac) - let bs := uset bs (i + 6) (val >>> 8).toUInt8 (by set_tac) - let bs := uset bs (i + 5) (val >>> 16).toUInt8 (by set_tac) - let bs := uset bs (i + 4) (val >>> 24).toUInt8 (by set_tac) - let bs := uset bs (i + 3) (val >>> 32).toUInt8 (by set_tac) - let bs := uset bs (i + 2) (val >>> 40).toUInt8 (by set_tac) - let bs := uset bs (i + 1) (val >>> 48).toUInt8 (by set_tac) - let bs := uset bs i (val >>> 56).toUInt8 (by set_tac)-/ - let bs := usetUInt32BE bs i (val >>> 32).toUInt32 (Nat.le_of_add_right_le (k := 4) h) - let bs := usetUInt32BE bs (i + 4) val.toUInt32 (by simpa [bs] using helperLemma) +@[extern "lean_byte_array_fset_uint64_be"] +def setUInt64BE (bs : ByteArray) (i : @& Nat) (val : UInt64) + (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := + let bs := bs.setUInt32BE i (val >>> 32).toUInt32 + let bs := bs.setUInt32BE (i + 4) val.toUInt32 (by grind) bs -@[simp] -theorem size_usetUInt64BE {bs : ByteArray} {i : USize} {val : UInt64} - (h : i.toNat + 8 ≤ bs.size) : (bs.usetUInt64BE i val).size = bs.size := by - simp [usetUInt64BE] +@[simp, grind =] +theorem size_setUInt64BE {bs : ByteArray} {i : Nat} {val : UInt64} + (h : i + 8 ≤ bs.size) : (bs.setUInt64BE i val).size = bs.size := by + simp [setUInt64BE] theorem size_def (bs : ByteArray) : bs.size = bs.data.size := rfl @@ -333,8 +271,9 @@ theorem ext {as bs : ByteArray} (h : as.size = bs.size) Grows or shrinks a byte array. When growing, additional bytes are filled with zeroes. -/ def setSize (bs : ByteArray) (size : Nat) (exact : Bool := false) : ByteArray := + let prevSize := bs.size Quot.liftOn (setSize' bs size exact) - (fun bs' => if h : bs.size < size then bs'.1.fill' bs.size (size - bs.size) 0 else bs'.1) + (fun bs' => if h : prevSize < size then bs'.1.fill' prevSize (size - prevSize) 0 else bs'.1) (fun a b _ => by dsimp split @@ -355,7 +294,7 @@ def setSize (bs : ByteArray) (size : Nat) (exact : Bool := false) : ByteArray := rw [a.2.2 i _ (Nat.lt_of_lt_of_le h hbs), b.2.2 i _ (Nat.lt_of_lt_of_le h hbs)]) -@[simp] +@[simp, grind =] theorem size_setSize (bs : ByteArray) (size : Nat) (exact : Bool) : (bs.setSize size exact).size = size := by rw [setSize] @@ -418,16 +357,34 @@ theorem data_replicate (size : Nat) (value : UInt8) : cases (emptyWithCapacity size).setSize' size using Quot.ind with | mk a => ?_ simp [Quot.liftOn, fill', copySlice, ← size_def, Array.extract_empty_of_size_le_start, a.2] +@[simp] +theorem size_replicate {n : Nat} {v : UInt8} : (replicate n v).size = n := by + simp [size_def] + +@[simp] +theorem getElem_replicate {i : Nat} {n : Nat} {v : UInt8} (h : i < (replicate n v).size) : + (replicate n v)[i] = v := by + simp [getElem_def] + +-- TODO: `pushUIntN{LE/BE}` + /-- -Return true iff the slices `[asOff, asOff + len)` in `as` and `[bsOff, bsOff + len)` in +Returns true if and only if the slices `[asOff, asOff + len)` in `as` and `[bsOff, bsOff + len)` in `bs` contain the same data. -/ @[extern "lean_byte_array_slice_eq"] -def sliceEq' (as : @& ByteArray) (asOff : @& Nat) (bs : @& ByteArray) (bsOff : @& Nat) (len : @& Nat) +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 `as` and `[bsOff, bsOff + len)` in +`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' + /-- Returns whether two byte arrays are equal. diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 1172eb868b4a..b8ff23f2dbaf 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -23,13 +23,6 @@ attribute [extern "lean_byte_array_data"] ByteArray.data namespace ByteArray -deriving instance BEq for ByteArray - -attribute [ext] ByteArray - -instance : DecidableEq ByteArray := - fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm - @[extern "lean_mk_empty_byte_array"] def emptyWithCapacity (c : @& Nat) : ByteArray := { data := #[] } diff --git a/src/Init/Data/Nat/Internal.lean b/src/Init/Data/Nat/Internal.lean index 870751d29358..8630d1d6b177 100644 --- a/src/Init/Data/Nat/Internal.lean +++ b/src/Init/Data/Nat/Internal.lean @@ -6,7 +6,9 @@ Author: Robin Arnez module prelude -import Init.Data.UInt.Basic +public import Init.Data.UInt.Basic + +public section @[inline] private unsafe def Nat.Internal.isScalarImpl (x : Nat) : Bool := @@ -18,7 +20,7 @@ Low-level function that returns whether the provided number is a "small natural Small natural numbers are not allocated on the heap but instead have their value encoded directly in their pointer address. -/ -@[implemented_by isScalarImpl] +@[implemented_by isScalarImpl, expose] def Nat.Internal.isScalar (x : Nat) : Bool := x < USize.size / 2 @@ -30,6 +32,6 @@ private unsafe def Nat.Internal.unboxImpl (x : Nat) (h : isScalar x) : USize := /-- Low-level function that returns the `USize` value of a small natural number (see `isScalar`). -/ -@[implemented_by unboxImpl] +@[implemented_by unboxImpl, expose] def Nat.Internal.unbox (x : Nat) (h : isScalar x) : USize := USize.ofNat x diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index e11845fa1f75..641c3f96268d 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -980,6 +980,121 @@ static inline lean_object * lean_byte_array_uset(lean_obj_arg a, size_t i, uint8 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; From 5871632b8a67a4e02eca228c450b7a3b3432b223 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Mon, 28 Jul 2025 12:34:57 +0200 Subject: [PATCH 07/14] fix test --- tests/lean/run/bytearray.lean | 66 +++++++++++++++++++---------------- 1 file changed, 35 insertions(+), 31 deletions(-) diff --git a/tests/lean/run/bytearray.lean b/tests/lean/run/bytearray.lean index 93f2414b5cb4..9e36b7b4d001 100644 --- a/tests/lean/run/bytearray.lean +++ b/tests/lean/run/bytearray.lean @@ -1,34 +1,38 @@ -#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[4, 9, 5]⟩ 1 0 -#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[1, 2, 3]⟩ 0 3 -#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 1 3 -#guard !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 0 ⟨#[0, 1, 2, 3]⟩ 0 3 -#guard !ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 0 1 -#guard ByteArray.sliceEq' ⟨#[1, 2, 3]⟩ 2 ⟨#[0, 1, 2, 3]⟩ 3 1 -#guard ByteArray.mk #[1, 2, 3] = ⟨#[1, 2, 3]⟩ -#guard ByteArray.mk #[1, 2, 4] ≠ ⟨#[1, 2, 3]⟩ -#guard ByteArray.mk #[] ≠ ⟨#[1, 2, 3]⟩ -#guard ByteArray.mk #[1, 2, 3] ≠ ⟨#[]⟩ -#guard ByteArray.mk #[] = ⟨#[]⟩ -#guard ByteArray.mk #[0, 1, 5, 7] = ⟨#[0, 1, 5, 7]⟩ -#guard ByteArray.mk #[0, 1, 5, 7] ≠ ⟨#[7, 5, 1, 0]⟩ -#guard (ByteArray.replicate 10 42).data == #[42, 42, 42, 42, 42, 42, 42, 42, 42, 42] -#guard (ByteArray.replicate 0 3).data == #[] -#guard (ByteArray.replicate 3 0).data == #[0, 0, 0] -#guard ((ByteArray.replicate 10 42).fill' 3 5 0).data == #[42, 42, 42, 0, 0, 0, 0, 0, 42, 42] -#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] -#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] +macro "#test " t:term : command => + `(#guard $t + example : $t := by decide) + +#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.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] +#test (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] #guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 12345).size == 12345 -#guard ByteArray.ugetUInt16BE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0203 -#guard ByteArray.ugetUInt16LE ⟨#[1, 2, 3, 4]⟩ 1 == 0x0302 -#guard ByteArray.ugetUInt32BE ⟨#[1, 2, 3, 4]⟩ 0 == 0x01020304 -#guard ByteArray.ugetUInt32LE ⟨#[1, 2, 3, 4]⟩ 0 == 0x04030201 -#guard ByteArray.ugetUInt64BE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x030405060708090A -#guard ByteArray.ugetUInt64LE ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]⟩ 2 == 0x0A09080706050403 +#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 -#guard ByteArray.usetUInt16BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 7, 8, 0, 0, 0]⟩ -#guard ByteArray.usetUInt16LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 3 0x0708 == ⟨#[0, 0, 0, 8, 7, 0, 0, 0]⟩ -#guard ByteArray.usetUInt32BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 1, 5, 7, 8]⟩ -#guard ByteArray.usetUInt32LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 4 0x01050708 == ⟨#[0, 0, 0, 0, 8, 7, 5, 1]⟩ -#guard ByteArray.usetUInt64BE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[255, 3, 1, 4, 10, 11, 7, 8]⟩ -#guard ByteArray.usetUInt64LE ⟨#[0, 0, 0, 0, 0, 0, 0, 0]⟩ 0 0xff0301040a0b0708 == ⟨#[8, 7, 11, 10, 4, 1, 3, 255]⟩ +#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]⟩ From be2609dd3ccd5ad3bf20a5d430cfca1a6657749f Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sat, 28 Mar 2026 12:32:40 +0100 Subject: [PATCH 08/14] oops --- tests/elab/bytearray.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/elab/bytearray.lean b/tests/elab/bytearray.lean index f3a3613c13a7..33629daeb536 100644 --- a/tests/elab/bytearray.lean +++ b/tests/elab/bytearray.lean @@ -1,4 +1,3 @@ -<<<<<<< HEAD:tests/lean/run/bytearray.lean macro "#test " t:term : command => `(#guard $t example : $t := by decide) From 7652e78e8211f68f605460cc3e693b1fa9722340 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sun, 29 Mar 2026 14:22:29 +0200 Subject: [PATCH 09/14] rework --- src/Init/Data/BitVec/Lemmas.lean | 6 + .../Data/ByteArray/AdditionalOperations.lean | 604 +++++++----------- src/Init/Data/ByteArray/Basic.lean | 230 +++++++ src/Init/Data/ByteArray/Lemmas.lean | 320 ++++++++++ src/Std/Internal/Http/Data/URI/Encoding.lean | 8 +- src/include/lean/lean.h | 2 +- src/runtime/object.cpp | 2 +- 7 files changed, 809 insertions(+), 363 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index fa38317602ea..9672f2527961 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2876,6 +2876,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/AdditionalOperations.lean b/src/Init/Data/ByteArray/AdditionalOperations.lean index f1e1d839a1b5..d82df4f42fb5 100644 --- a/src/Init/Data/ByteArray/AdditionalOperations.lean +++ b/src/Init/Data/ByteArray/AdditionalOperations.lean @@ -7,405 +7,295 @@ module prelude public import Init.Data.ByteArray.Basic -public import Init.Data.Array.Lemmas -public import Init.Data.UInt.Lemmas -public import Init.Data.Nat.Internal -public import Init.Grind +import Init.Data.ByteArray.Lemmas +import Init.Data.Array.Bootstrap +import Init.Data.Array.Lemmas +import Init.Omega +import Init.ByCases -set_option linter.missingDocs true - -public section +@[expose] public section namespace ByteArray -/-- -Interprets the value in the byte array `bs` starting at index `i` -as a 16 bit little-endian unsigned integer. --/ -@[extern "lean_byte_array_fget_uint16_le"] -def getUInt16LE (bs : @& ByteArray) (i : @& Nat) - (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := - let lo := bs[i] - let hi := bs[i + 1] - lo.toUInt16 ||| (hi.toUInt16 <<< 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') + } /-- -Interprets the value in the byte array `bs` starting at index `i` -as a 16 bit big-endian unsigned integer. +A byte array of size `sz` where only the first `origSize` bytes are defined and the others are +quotiented out. -/ -@[extern "lean_byte_array_fget_uint16_be"] -def getUInt16BE (bs : @& ByteArray) (i : @& Nat) - (h : i + 2 ≤ bs.size := by get_elem_tactic) : UInt16 := - let hi := bs[i] - let lo := bs[i + 1] - lo.toUInt16 ||| (hi.toUInt16 <<< 8) +structure SetSizeResult (origSz sz : Nat) where + mk' :: value : Quotient (SetSizeResult.setoid origSz sz) -/-- -Interprets the value in the byte array `bs` starting at index `i` -as a 32 bit little-endian unsigned integer. --/ -@[extern "lean_byte_array_fget_uint32_le"] -def getUInt32LE (bs : @& ByteArray) (i : @& Nat) - (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := - let lo := bs.getUInt16LE i - let hi := bs.getUInt16LE (i + 2) - lo.toUInt32 ||| (hi.toUInt32 <<< 16) +def SetSizeResult.mk {origSz sz : Nat} (bs : ByteArray) (h : bs.size = sz) : + SetSizeResult origSz sz := ⟨Quotient.mk _ ⟨bs, h⟩⟩ /-- -Interprets the value in the byte array `bs` starting at index `i` -as a 32 bit big-endian unsigned integer. --/ -@[extern "lean_byte_array_fget_uint32_be"] -def getUInt32BE (bs : @& ByteArray) (i : @& Nat) - (h : i + 4 ≤ bs.size := by get_elem_tactic) : UInt32 := - let hi := bs.getUInt16BE i - let lo := bs.getUInt16BE (i + 2) - lo.toUInt32 ||| (hi.toUInt32 <<< 16) - -/-- -Interprets the value in the byte array `bs` starting at index `i` -as a 64 bit little-endian unsigned integer. --/ -@[extern "lean_byte_array_fget_uint64_le"] -def getUInt64LE (bs : @& ByteArray) (i : @& Nat) - (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := - let lo := bs.getUInt32LE i - let hi := bs.getUInt32LE (i + 4) - lo.toUInt64 ||| (hi.toUInt64 <<< 32) +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. -/-- -Interprets the value in the byte array `bs` starting at index `i` -as a 64 bit big-endian unsigned integer. +If `exact` is `false`, the capacity will be doubled when grown. -/ -@[extern "lean_byte_array_fget_uint64_be"] -def getUInt64BE (bs : @& ByteArray) (i : @& Nat) - (h : i + 8 ≤ bs.size := by get_elem_tactic) : UInt64 := - let hi := bs.getUInt32BE i - let lo := bs.getUInt32BE (i + 4) - lo.toUInt64 ||| (hi.toUInt64 <<< 32) - -@[simp, grind =] -theorem size_uset {bs : ByteArray} {i : USize} {val : UInt8} (h : i.toNat < bs.size) : - (bs.uset i val).size = bs.size := by - simp [size, uset] - -@[simp, grind =] -theorem size_set {bs : ByteArray} {i : Nat} {val : UInt8} (h : i < bs.size) : - (bs.set i val).size = bs.size := by - simp [size, set] - -/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -@[extern "lean_byte_array_fset_uint16_le"] -def setUInt16LE (bs : ByteArray) (i : @& Nat) (val : UInt16) - (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.set i val.toUInt8 - let bs := bs.set (i + 1) (val >>> 8).toUInt8 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt16LE {bs : ByteArray} {i : Nat} {val : UInt16} - (h : i + 2 ≤ bs.size) : (bs.setUInt16LE i val).size = bs.size := by - simp [setUInt16LE] - -/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -@[extern "lean_byte_array_fset_uint16_be"] -def setUInt16BE (bs : ByteArray) (i : @& Nat) (val : UInt16) - (h : i + 2 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.set i (val >>> 8).toUInt8 - let bs := bs.set (i + 1) val.toUInt8 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt16BE {bs : ByteArray} {i : Nat} {val : UInt16} - (h : i + 2 ≤ bs.size) : (bs.setUInt16BE i val).size = bs.size := by - simp [setUInt16BE] - -/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -@[extern "lean_byte_array_fset_uint32_le"] -def setUInt32LE (bs : ByteArray) (i : @& Nat) (val : UInt32) - (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.setUInt16LE i val.toUInt16 - let bs := bs.setUInt16LE (i + 2) (val >>> 16).toUInt16 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt32LE {bs : ByteArray} {i : Nat} {val : UInt32} - (h : i + 4 ≤ bs.size) : (bs.setUInt32LE i val).size = bs.size := by - simp [setUInt32LE] - -/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -@[extern "lean_byte_array_fset_uint32_be"] -def setUInt32BE (bs : ByteArray) (i : @& Nat) (val : UInt32) - (h : i + 4 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.setUInt16BE i (val >>> 16).toUInt16 - let bs := bs.setUInt16BE (i + 2) val.toUInt16 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt32BE {bs : ByteArray} {i : Nat} {val : UInt32} - (h : i + 4 ≤ bs.size) : (bs.setUInt32BE i val).size = bs.size := by - simp [setUInt32BE] - -/-- Writes the value into the byte array starting at index `i` in little-endian byte order. -/ -@[extern "lean_byte_array_fset_uint64_le"] -def setUInt64LE (bs : ByteArray) (i : @& Nat) (val : UInt64) - (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.setUInt32LE i val.toUInt32 - let bs := bs.setUInt32LE (i + 4) (val >>> 32).toUInt32 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt64LE {bs : ByteArray} {i : Nat} {val : UInt64} - (h : i + 8 ≤ bs.size) : (bs.setUInt64LE i val).size = bs.size := by - simp [setUInt64LE] - -/-- Writes the value into the byte array starting at index `i` in big-endian byte order. -/ -@[extern "lean_byte_array_fset_uint64_be"] -def setUInt64BE (bs : ByteArray) (i : @& Nat) (val : UInt64) - (h : i + 8 ≤ bs.size := by get_elem_tactic) : ByteArray := - let bs := bs.setUInt32BE i (val >>> 32).toUInt32 - let bs := bs.setUInt32BE (i + 4) val.toUInt32 (by grind) - bs - -@[simp, grind =] -theorem size_setUInt64BE {bs : ByteArray} {i : Nat} {val : UInt64} - (h : i + 8 ≤ bs.size) : (bs.setUInt64BE i val).size = bs.size := by - simp [setUInt64BE] - -theorem size_def (bs : ByteArray) : bs.size = bs.data.size := rfl +@[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 data_extract (bs : ByteArray) (b e : Nat) : - (bs.extract b e).data = bs.data.extract b e := by - simp only [extract, copySlice, empty, emptyWithCapacity, Array.extract_zero, Array.empty_append, - Nat.zero_add, Array.extract_empty, Array.append_empty] - by_cases h : b ≤ e - · rw [Nat.add_sub_cancel' h] - · rw [Nat.sub_eq_zero_of_le (Nat.le_of_not_le h), Nat.add_zero] - simp only [Nat.le_refl, Array.extract_empty_of_stop_le_start, Nat.le_of_not_le h] +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 -@[simp] -theorem size_extract (bs : ByteArray) (b e : Nat) : - (bs.extract b e).size = min e bs.size - b := by - simp [size_def] +@[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' -@[simp] -theorem data_append (as bs : ByteArray) : - (as ++ bs).data = as.data ++ bs.data := by - change (as.append bs).data = _ - simp only [ByteArray.append, copySlice, size_def, Array.extract_size, Nat.zero_add, Nat.sub_zero, - Nat.min_self, Nat.le_add_right, Array.extract_empty_of_size_le_start, Array.append_assoc, - Array.append_right_inj, Array.append_right_eq_self] +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 size_append (as bs : ByteArray) : (as ++ bs).size = as.size + bs.size := by - simp [size_def] +theorem SetSizeResult.getElem_mk {i : Nat} {hi} : + (@mk origSz sz b hb)[i]'hi = b[i] := rfl @[simp] -theorem size_mk (xs : Array UInt8) : size (mk xs) = xs.size := rfl - -theorem getElem_def {xs : ByteArray} {i : Nat} (h : i < xs.size) : xs[i] = xs.data[i] := rfl - -/-- -Low-level function for growing or shrinking a byte array. - -Note: the contents of the bytes at the end are undefined when growing which is why -this function returns a `Squash`. - -If `exact` is `false`, the capacity will be doubled when grown. --/ -@[extern "lean_byte_array_set_size"] -def setSize' (bs : ByteArray) (size : @& Nat) (exact : Bool := false) : - Squash { b : ByteArray // b.size = size ∧ ∀ (i : Nat) h h', b[i]'h = bs[i] } := by - let b := bs.extract 0 size ++ mk (Array.replicate (size - bs.size) 0) - refine Squash.mk ⟨b, ?_⟩ - have hsize : b.size = size := by simp [b] <;> omega - constructor - · exact hsize - · intro i h h' - rw [hsize] at h - rw [size_def] at h' - simp [b, getElem_def, h, h', Nat.lt_min] +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; rfl + +/-- 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 + dsimp only + ext i hi + · simp [ha, hb] + · apply hab + · exact ha ▸ hi + · exact Nat.lt_of_lt_of_le (ha ▸ hi) h -/-- -Replaces the bytes in the range `[start, start + size)` within `bs` with `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 +@[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 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_def] at h - simp [fill', copySlice, size_def] <;> 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_def, 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] +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 + dsimp only + 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 + dsimp only + 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 - · congr; omega + · apply hab <;> omega -@[ext] -theorem ext {as bs : ByteArray} (h : as.size = bs.size) - (h' : ∀ (i : Nat) h h', as[i]'h = bs[i]) : as = bs := by - rcases as with ⟨xs⟩ - rcases bs with ⟨ys⟩ - congr - exact Array.ext h h' - -/-- -Grows or shrinks a byte array. When growing, additional bytes are filled with zeroes. --/ -def setSize (bs : ByteArray) (size : Nat) (exact : Bool := false) : ByteArray := - let prevSize := bs.size - Quot.liftOn (setSize' bs size exact) - (fun bs' => if h : prevSize < size then bs'.1.fill' prevSize (size - prevSize) 0 else bs'.1) - (fun a b _ => by - dsimp - split - · ext - · simp [a.2, b.2] - · simp only [getElem_fill'] - split - · rfl - · rename_i hsize i h h' h'' - simp only [size_fill', a.2.1] at h - simp only [Nat.le_of_lt hsize, Nat.add_sub_cancel', h, and_true, Nat.not_le] at h'' - rw [a.2.2 i _ h'', b.2.2 i _ h''] - · ext - · simp [a.2, b.2] - · rename_i hbs i h h' - replace hbs := Nat.le_of_not_lt hbs - rw [a.2.1] at h - rw [a.2.2 i _ (Nat.lt_of_lt_of_le h hbs), - b.2.2 i _ (Nat.lt_of_lt_of_le h hbs)]) +@[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_setSize (bs : ByteArray) (size : Nat) (exact : Bool) : - (bs.setSize size exact).size = size := by - rw [setSize] - rcases bs.setSize' size exact with ⟨bs⟩ - dsimp [Quot.liftOn] - split <;> simp [bs.2] - -theorem getElem_setSize {bs : ByteArray} {size : Nat} {exact : Bool} {i : Nat} - (h : i < (bs.setSize size exact).size) : - (bs.setSize size exact)[i] = if h : i < bs.size then bs[i] else 0 := by - rw [size_setSize] at h - simp only [setSize] - have ⟨q, hq⟩ : { a // bs.setSize' size exact = a } := ⟨_, rfl⟩ - rcases q with ⟨a⟩ - simp only [Quot.liftOn, hq] +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 only [getElem_fill'] - split - · rename_i h - rw [dif_neg (Nat.not_lt_of_le h.1)] - · rename_i h h' h'' - simp only [Nat.le_of_lt h', Nat.add_sub_cancel', h, and_true, Nat.not_le] at h'' - rw [a.2.2 i _ h'', dif_pos h''] - · rename_i h h' - replace h' := Nat.lt_of_lt_of_le h (Nat.le_of_not_lt h') - rw [a.2.2 i _ h', dif_pos h'] - -theorem getElem_setSize_eq_getElem {bs : ByteArray} {size : Nat} {exact : Bool} {i : Nat} - {h : i < (bs.setSize size exact).size} (h' : i < bs.size) : - (bs.setSize size exact)[i] = bs[i] := by - simp only [getElem_setSize, h', ↓reduceDIte] - -theorem setSize'_eq_setSize (bs : ByteArray) (size : Nat) (exact : Bool) : - bs.setSize' size exact = Squash.mk ⟨bs.setSize size exact, - size_setSize .., @getElem_setSize_eq_getElem bs size exact⟩ := - Subsingleton.allEq .. + · simp [SetSizeResult.getElem_fill] + · rw [dif_pos (c := i < _) (by omega)] + simp -/-- -Creates an array that contains n repetitions of the byte v. --/ +/-- Creates an array that contains n repetitions of the byte v. -/ def replicate (n : Nat) (v : UInt8) := - Quot.liftOn ((emptyWithCapacity n).setSize' n) - (fun x => x.1.fill' 0 n v) - (fun a b _ => by - ext - · simp [a.2, b.2] - · rename_i h - simp only [size_fill', b.2] at h - simp [getElem_fill', h]) - -@[simp] -theorem _root_.Array.extract_size' {xs : Array α} {size : Nat} (h : size = xs.size) : - xs.extract 0 size = xs := by - rw [h, Array.extract_size] + ((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] - cases (emptyWithCapacity size).setSize' size using Quot.ind with | mk a => ?_ - simp [Quot.liftOn, fill', copySlice, ← size_def, Array.extract_empty_of_size_le_start, a.2] + 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_def] + 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_def] - --- TODO: `pushUIntN{LE/BE}` - -/-- -Returns true if and only if the slices `[asOff, asOff + len)` in `as` and `[bsOff, bsOff + len)` in -`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 `as` and `[bsOff, bsOff + len)` in -`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' - -/-- -Returns whether two byte arrays are equal. - -The notation `==` is preferred over using this function directly. --/ -protected def beq (as bs : ByteArray) : Bool := - if h : as.size = bs.size then - sliceEq' as 0 bs 0 as.size - else - false - -protected theorem beq_iff_eq {as bs : ByteArray} : as.beq bs ↔ as = bs := by - dsimp [ByteArray.beq] - split - · rename_i h - simp [sliceEq', ← size_def, h] - exact ⟨fun h => (h ▸ rfl : mk as.data = mk bs.data), fun h => h ▸ rfl⟩ - · rename_i h - simp [ne_of_apply_ne size h] - -instance : DecidableEq ByteArray := fun _ _ => - decidable_of_decidable_of_iff ByteArray.beq_iff_eq + simp [getElem_eq_getElem_data] end ByteArray diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 3559fa75571c..1cb9b51848fc 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 @@ -313,6 +314,235 @@ 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' + +/-- +Returns whether two byte arrays are equal. + +The notation `==` is preferred over using this function directly. +-/ +protected def beq (as bs : ByteArray) : Bool := + if h : as.size = bs.size then + sliceEq' as 0 bs 0 as.size + else + false + 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/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index 02cc3efb3de8..2c2b537b4fd3 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -11,6 +11,8 @@ 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 @@ -275,11 +277,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 + simpa using Array.getElem_set h hj + +@[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,4 +345,307 @@ 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 [dif_neg (by omega)] + | case2 => rw [dif_pos (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]; rfl + +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; rfl + +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 [if_neg (by omega)] + | case2 => rw [if_pos (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]; rfl + +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; rfl + +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 [if_pos (by omega)] + split + · simp [show j = i + k by omega] + · rw [getElem_set, if_neg (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 [if_pos (by omega), BitVec.extractLsb'_append_eq_of_le (by omega)]; congr; omega + split + · rw [if_pos (by omega), BitVec.extractLsb'_append_eq_of_add_le (by omega)] + · rw [if_neg (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, if_pos (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 [if_pos (by omega)] + split + · simp [show j = i + k by omega]; congr 2; omega + · rw [getElem_set, if_neg (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 [if_pos (by omega), BitVec.extractLsb'_append_eq_of_add_le (by omega)]; congr 2; omega + split + · rw [if_pos (by omega), BitVec.extractLsb'_append_eq_of_le (by omega)]; congr; omega + · rw [if_neg (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, if_pos (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]; rfl + · 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 + +protected theorem beq_iff_eq {as bs : ByteArray} : as.beq bs ↔ as = bs := by + dsimp [ByteArray.beq] + split + · rename_i h + simp [sliceEq', h, Array.extract_eq_self_of_le, ← ByteArray.ext_iff] + · rename_i h + simp [ne_of_apply_ne size h] + +instance : DecidableEq ByteArray := fun _ _ => + decidable_of_decidable_of_iff ByteArray.beq_iff_eq + end ByteArray diff --git a/src/Std/Internal/Http/Data/URI/Encoding.lean b/src/Std/Internal/Http/Data/URI/Encoding.lean index c34b14394ae6..695e2ac8e681 100644 --- a/src/Std/Internal/Http/Data/URI/Encoding.lean +++ b/src/Std/Internal/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 +public import Init.Data.ByteArray.Lemmas public import Init.Data.String public import Std.Internal.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/include/lean/lean.h b/src/include/lean/lean.h index 67d88505b55e..953c5879538d 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1154,7 +1154,7 @@ 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, uint8_t exact); +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); diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index e1641f477205..63ba6b83aea8 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2534,7 +2534,7 @@ 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_set_size(obj_arg a, b_obj_arg b, uint8 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); From c5809797b58bd3d0049fb7923170121c807c8dae Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sun, 29 Mar 2026 14:27:29 +0200 Subject: [PATCH 10/14] remove old extra --- .../Data/ByteArray/AdditionalOperations.lean | 8 ++++ src/Init/Data/ByteArray/Extra.lean | 45 ------------------- 2 files changed, 8 insertions(+), 45 deletions(-) delete mode 100644 src/Init/Data/ByteArray/Extra.lean diff --git a/src/Init/Data/ByteArray/AdditionalOperations.lean b/src/Init/Data/ByteArray/AdditionalOperations.lean index d82df4f42fb5..d4694303be4f 100644 --- a/src/Init/Data/ByteArray/AdditionalOperations.lean +++ b/src/Init/Data/ByteArray/AdditionalOperations.lean @@ -17,6 +17,14 @@ import Init.ByCases namespace ByteArray +@[deprecated getUInt64LE! (since := "2026-03-29")] +def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 := + bs.getUInt64LE! 0 + +@[deprecated getUInt64BE! (since := "2026-03-29")] +def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 := + bs.getUInt64BE! 0 + 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 := { diff --git a/src/Init/Data/ByteArray/Extra.lean b/src/Init/Data/ByteArray/Extra.lean deleted file mode 100644 index db6879d2fd55..000000000000 --- a/src/Init/Data/ByteArray/Extra.lean +++ /dev/null @@ -1,45 +0,0 @@ -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura --/ -module - -prelude -public import Init.Data.ByteArray.Basic -import Init.Data.String.Defs -import Init.Data.UInt.Basic - -set_option doc.verso true - -/-- -Interprets a {name}`ByteArray` of size 8 as a little-endian {name}`UInt64`. - -Panics if the array's size is not 8. --/ -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 - -/-- -Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`. - -Panics if the array's size is not 8. --/ -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 From 9804331f78514612f07ded7e394171fe5a2984d3 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sun, 29 Mar 2026 14:27:54 +0200 Subject: [PATCH 11/14] rename --- src/Init/Data/ByteArray/{AdditionalOperations.lean => Extra.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/Init/Data/ByteArray/{AdditionalOperations.lean => Extra.lean} (100%) diff --git a/src/Init/Data/ByteArray/AdditionalOperations.lean b/src/Init/Data/ByteArray/Extra.lean similarity index 100% rename from src/Init/Data/ByteArray/AdditionalOperations.lean rename to src/Init/Data/ByteArray/Extra.lean From 9b8f305efe2148f1ab6363969add0a86c2a7285c Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sun, 29 Mar 2026 15:05:30 +0200 Subject: [PATCH 12/14] fixes --- src/Init/Data/ByteArray.lean | 1 - src/Init/Data/Random.lean | 2 +- src/Lean/Server/FileWorker/Utils.lean | 2 +- src/Std/Internal/Async/Select.lean | 6 ++-- src/Std/Time/Zoned/Database/Basic.lean | 4 +-- src/Std/Time/Zoned/Database/TzIf.lean | 50 +++++++++----------------- 6 files changed, 23 insertions(+), 42 deletions(-) diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index e63dbba17bc3..eeab7dd85f51 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -7,7 +7,6 @@ module prelude public import Init.Data.ByteArray.Basic -public import Init.Data.ByteArray.AdditionalOperations public import Init.Data.ByteArray.Bootstrap public import Init.Data.ByteArray.Extra public import Init.Data.ByteArray.Lemmas 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/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index 824a52e3de86..bab3f08a17fe 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -86,7 +86,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/Internal/Async/Select.lean b/src/Std/Internal/Async/Select.lean index 996a160039cb..fc877f50ecaf 100644 --- a/src/Std/Internal/Async/Select.lean +++ b/src/Std/Internal/Async/Select.lean @@ -128,7 +128,7 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d if selectables.isEmpty then throw <| .userError "Selectable.one requires at least one Selectable" - let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8)) + let seed := UInt64.toNat ((← IO.getRandomBytes 8).getUInt64LE! 0) let gen := mkStdGen seed let selectables := shuffleIt selectables gen @@ -187,7 +187,7 @@ def Selectable.tryOne (selectables : Array (Selectable α)) : Async (Option α) if selectables.isEmpty then return none - let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8)) + let seed := UInt64.toNat ((← IO.getRandomBytes 8).getUInt64LE! 0) let gen := mkStdGen seed let selectables := shuffleIt selectables gen @@ -206,7 +206,7 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α) if selectables.isEmpty then throw <| .userError "Selectable.one requires at least one Selectable" - let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8)) + let seed := UInt64.toNat ((← IO.getRandomBytes 8).getUInt64LE! 0) let gen := mkStdGen seed let selectables := shuffleIt selectables gen diff --git a/src/Std/Time/Zoned/Database/Basic.lean b/src/Std/Time/Zoned/Database/Basic.lean index 51a1193c84f6..e4ce3e79ae0e 100644 --- a/src/Std/Time/Zoned/Database/Basic.lean +++ b/src/Std/Time/Zoned/Database/Basic.lean @@ -52,7 +52,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) @@ -71,7 +71,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 d17bc15f714d..fcb563023583 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. @@ -177,25 +174,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 @@ -203,10 +181,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 @@ -226,12 +208,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) := @@ -257,7 +239,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) := @@ -266,11 +248,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 From 0f152480328618dec10c9a41c16a96c8e233684f Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Sun, 29 Mar 2026 18:52:58 +0200 Subject: [PATCH 13/14] fix test --- src/Init/Data/Nat/Internal.lean | 37 --------------------------------- tests/elab/bytearray.lean | 14 ++++++------- 2 files changed, 7 insertions(+), 44 deletions(-) delete mode 100644 src/Init/Data/Nat/Internal.lean diff --git a/src/Init/Data/Nat/Internal.lean b/src/Init/Data/Nat/Internal.lean deleted file mode 100644 index 8630d1d6b177..000000000000 --- a/src/Init/Data/Nat/Internal.lean +++ /dev/null @@ -1,37 +0,0 @@ -/- -Copyright (c) 2025 Robin Arnez. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Robin Arnez --/ -module - -prelude -public import Init.Data.UInt.Basic - -public section - -@[inline] -private unsafe def Nat.Internal.isScalarImpl (x : Nat) : Bool := - ptrAddrUnsafe x &&& 1 == 1 - -/-- -Low-level function that returns whether the provided number is a "small natural number". - -Small natural numbers are not allocated on the heap but instead have -their value encoded directly in their pointer address. --/ -@[implemented_by isScalarImpl, expose] -def Nat.Internal.isScalar (x : Nat) : Bool := - x < USize.size / 2 - -set_option linter.unusedVariables.funArgs false in -@[inline] -private unsafe def Nat.Internal.unboxImpl (x : Nat) (h : isScalar x) : USize := - ptrAddrUnsafe x >>> 1 - -/-- -Low-level function that returns the `USize` value of a small natural number (see `isScalar`). --/ -@[implemented_by unboxImpl, expose] -def Nat.Internal.unbox (x : Nat) (h : isScalar x) : USize := - USize.ofNat x diff --git a/tests/elab/bytearray.lean b/tests/elab/bytearray.lean index 33629daeb536..7f887643e971 100644 --- a/tests/elab/bytearray.lean +++ b/tests/elab/bytearray.lean @@ -1,6 +1,6 @@ macro "#test " t:term : command => `(#guard $t - example : $t := by decide) + 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 @@ -18,10 +18,10 @@ macro "#test " t:term : command => #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.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 3).data == #[1, 2, 3] -#test (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 10).data == #[1, 2, 3, 4, 5, 6, 0, 0, 0, 0] -#guard (ByteArray.setSize ⟨#[1, 2, 3, 4, 5, 6]⟩ 12345).size == 12345 +#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 @@ -57,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 From 40d9379be60638e4265fc5ef82e88d7a24204742 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Sep 2026 14:35:36 +1000 Subject: [PATCH 14/14] chore: mark the ByteArray deprecations as changing type MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `getUInt64LE!` and `getUInt64BE!` take an offset, so they are `ByteArray → Nat → UInt64` where the deprecated definitions are `ByteArray → UInt64`. The check for this landed after the branch was last built. Co-Authored-By: Claude Opus 5 (1M context) --- src/Init/Data/ByteArray/Extra.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/ByteArray/Extra.lean b/src/Init/Data/ByteArray/Extra.lean index 03995226c9fb..c3facffa3c1a 100644 --- a/src/Init/Data/ByteArray/Extra.lean +++ b/src/Init/Data/ByteArray/Extra.lean @@ -17,11 +17,11 @@ import Init.ByCases namespace ByteArray -@[deprecated getUInt64LE! (since := "2026-03-29")] +@[deprecated getUInt64LE! +typeChanged (since := "2026-03-29")] def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 := bs.getUInt64LE! 0 -@[deprecated getUInt64BE! (since := "2026-03-29")] +@[deprecated getUInt64BE! +typeChanged (since := "2026-03-29")] def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 := bs.getUInt64BE! 0