diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index 3558d9d89863..16ffd5a154c4 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -9,5 +9,7 @@ prelude public import Init.Data.ByteArray.Basic public import Init.Data.ByteArray.Bootstrap public import Init.Data.ByteArray.Extra +public import Init.Data.ByteArray.Pack public import Init.Data.ByteArray.Lemmas public import Init.Data.ByteArray.Lex +public import Init.Data.ByteArray.Pack.Lemmas diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index cfb01253e78c..456fbdd0992d 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -405,4 +405,7 @@ private theorem getElem!_eq_data_getElem! (data : ByteArray) (i : Nat) : · next hij => subst hij; exact getElem_set!_self data i v h · next hij => exact getElem_set!_ne data i j v hij hj +theorem get!_eq_getElem! (a : ByteArray) (i : Nat) : a.get! i = a[i]! := by + rw [getElem!_eq_data_getElem!]; rfl + end ByteArray diff --git a/src/Init/Data/ByteArray/Pack.lean b/src/Init/Data/ByteArray/Pack.lean new file mode 100644 index 000000000000..46ad3bf059a9 --- /dev/null +++ b/src/Init/Data/ByteArray/Pack.lean @@ -0,0 +1,281 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +module + +prelude +public import Init.Data.ByteArray.Basic +public import Init.Data.UInt.Basic + +/-! +# Wide fixed-width integer load/store on `ByteArray` + +Accessors that read and write a `UInt16` / `UInt32` / `UInt64` at a *byte* offset +of a `ByteArray`, in explicit little- or big-endian order, operating directly on +the underlying contiguous buffer rather than via an `Array UInt32` (a pointer-sized +slot per element, with an unbox on each read) or shifts-and-ors written in Lean. +The `@[extern]` implementations are portable byte assembly, which optimizing +compilers can lower to a wide (possibly unaligned) load or store. + +For each width `W` and endianness `E` there are three read and three write +variants, mirroring `ByteArray.get!`/`get`/`uget` and `set!`/`set`/`uset`: + +* `getUIntWE!` / `setUIntWE!` — `Nat` offset, no proof. All-or-nothing on bounds: + a read returns `0` and a write leaves the array unchanged unless the whole + `W/8`-byte window fits. These are the proof-level specification; the + proof-carrying variants below are definitionally equal to them. +* `getUIntWE` / `setUIntWE` — `Nat` offset with an in-bounds proof. +* `ugetUIntWE` / `usetUIntWE` — `USize` offset with an in-bounds proof. + +In a hot loop, prefer the `USize`-indexed `ugetUIntWE` / `usetUIntWE` forms: their +index is a machine word, whereas the `Nat`-indexed variants do their index +arithmetic on `Nat`, which is markedly slower. +-/ + +@[expose] public section + +namespace ByteArray + +/-! ## UInt16 -/ + +/-- Reads the little-endian `UInt16` at byte offset `off`, or `0` if `off + 2 > a.size`. -/ +@[extern "lean_byte_array_get_uint16le"] +def getUInt16LE! (a : @& ByteArray) (off : @& Nat) : UInt16 := + if off + 2 ≤ a.size then + (a.get! off).toUInt16 ||| + (a.get! (off+1)).toUInt16 <<< 0x8 + else 0 + +/-- Reads the big-endian `UInt16` at byte offset `off`, or `0` if `off + 2 > a.size`. -/ +@[extern "lean_byte_array_get_uint16be"] +def getUInt16BE! (a : @& ByteArray) (off : @& Nat) : UInt16 := + if off + 2 ≤ a.size then + (a.get! off).toUInt16 <<< 0x8 ||| + (a.get! (off+1)).toUInt16 + else 0 + +/-- Writes `v` as a little-endian `UInt16` at byte offset `off`; unchanged if `off + 2 > a.size`. -/ +@[extern "lean_byte_array_set_uint16le"] +def setUInt16LE! (a : ByteArray) (off : @& Nat) (v : UInt16) : ByteArray := + if off + 2 ≤ a.size then + (a.set! off v.toUInt8).set! (off+1) (v >>> 0x8).toUInt8 + else a + +/-- Writes `v` as a big-endian `UInt16` at byte offset `off`; unchanged if `off + 2 > a.size`. -/ +@[extern "lean_byte_array_set_uint16be"] +def setUInt16BE! (a : ByteArray) (off : @& Nat) (v : UInt16) : ByteArray := + if off + 2 ≤ a.size then + (a.set! off (v >>> 0x8).toUInt8).set! (off+1) v.toUInt8 + else a + +/-- Reads the little-endian `UInt16` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint16le"] +def getUInt16LE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 2 ≤ a.size := by get_elem_tactic) → UInt16 + | a, i, _ => a.getUInt16LE! i + +/-- Reads the big-endian `UInt16` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint16be"] +def getUInt16BE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 2 ≤ a.size := by get_elem_tactic) → UInt16 + | a, i, _ => a.getUInt16BE! i + +/-- Reads the little-endian `UInt16` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint16le"] +def ugetUInt16LE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 2 ≤ a.size := by get_elem_tactic) → UInt16 + | a, i, _ => a.getUInt16LE! i.toNat + +/-- Reads the big-endian `UInt16` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint16be"] +def ugetUInt16BE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 2 ≤ a.size := by get_elem_tactic) → UInt16 + | a, i, _ => a.getUInt16BE! i.toNat + +/-- Writes `v` as a little-endian `UInt16` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint16le"] +def setUInt16LE : (a : ByteArray) → (i : @& Nat) → (v : UInt16) → (h : i + 2 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt16LE! i v + +/-- Writes `v` as a big-endian `UInt16` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint16be"] +def setUInt16BE : (a : ByteArray) → (i : @& Nat) → (v : UInt16) → (h : i + 2 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt16BE! i v + +/-- Writes `v` as a little-endian `UInt16` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint16le"] +def usetUInt16LE : (a : ByteArray) → (i : USize) → (v : UInt16) → (h : i.toNat + 2 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt16LE! i.toNat v + +/-- Writes `v` as a big-endian `UInt16` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint16be"] +def usetUInt16BE : (a : ByteArray) → (i : USize) → (v : UInt16) → (h : i.toNat + 2 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt16BE! i.toNat v + +/-! ## UInt32 -/ + +/-- Reads the little-endian `UInt32` at byte offset `off`, or `0` if `off + 4 > a.size`. -/ +@[extern "lean_byte_array_get_uint32le"] +def getUInt32LE! (a : @& ByteArray) (off : @& Nat) : UInt32 := + if off + 4 ≤ a.size then + (a.get! off).toUInt32 ||| + (a.get! (off+1)).toUInt32 <<< 0x8 ||| + (a.get! (off+2)).toUInt32 <<< 0x10 ||| + (a.get! (off+3)).toUInt32 <<< 0x18 + else 0 + +/-- Reads the big-endian `UInt32` at byte offset `off`, or `0` if `off + 4 > a.size`. -/ +@[extern "lean_byte_array_get_uint32be"] +def getUInt32BE! (a : @& ByteArray) (off : @& Nat) : UInt32 := + if off + 4 ≤ a.size then + (a.get! off).toUInt32 <<< 0x18 ||| + (a.get! (off+1)).toUInt32 <<< 0x10 ||| + (a.get! (off+2)).toUInt32 <<< 0x8 ||| + (a.get! (off+3)).toUInt32 + else 0 + +/-- Writes `v` as a little-endian `UInt32` at byte offset `off`; unchanged if `off + 4 > a.size`. -/ +@[extern "lean_byte_array_set_uint32le"] +def setUInt32LE! (a : ByteArray) (off : @& Nat) (v : UInt32) : ByteArray := + if off + 4 ≤ a.size then + (((a.set! off v.toUInt8).set! (off+1) (v >>> 0x8).toUInt8).set! (off+2) + (v >>> 0x10).toUInt8).set! (off+3) (v >>> 0x18).toUInt8 + else a + +/-- Writes `v` as a big-endian `UInt32` at byte offset `off`; unchanged if `off + 4 > a.size`. -/ +@[extern "lean_byte_array_set_uint32be"] +def setUInt32BE! (a : ByteArray) (off : @& Nat) (v : UInt32) : ByteArray := + if off + 4 ≤ a.size then + (((a.set! off (v >>> 0x18).toUInt8).set! (off+1) (v >>> 0x10).toUInt8).set! (off+2) + (v >>> 0x8).toUInt8).set! (off+3) v.toUInt8 + else a + +/-- Reads the little-endian `UInt32` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint32le"] +def getUInt32LE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 4 ≤ a.size := by get_elem_tactic) → UInt32 + | a, i, _ => a.getUInt32LE! i + +/-- Reads the big-endian `UInt32` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint32be"] +def getUInt32BE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 4 ≤ a.size := by get_elem_tactic) → UInt32 + | a, i, _ => a.getUInt32BE! i + +/-- Reads the little-endian `UInt32` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint32le"] +def ugetUInt32LE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 4 ≤ a.size := by get_elem_tactic) → UInt32 + | a, i, _ => a.getUInt32LE! i.toNat + +/-- Reads the big-endian `UInt32` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint32be"] +def ugetUInt32BE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 4 ≤ a.size := by get_elem_tactic) → UInt32 + | a, i, _ => a.getUInt32BE! i.toNat + +/-- Writes `v` as a little-endian `UInt32` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint32le"] +def setUInt32LE : (a : ByteArray) → (i : @& Nat) → (v : UInt32) → (h : i + 4 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt32LE! i v + +/-- Writes `v` as a big-endian `UInt32` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint32be"] +def setUInt32BE : (a : ByteArray) → (i : @& Nat) → (v : UInt32) → (h : i + 4 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt32BE! i v + +/-- Writes `v` as a little-endian `UInt32` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint32le"] +def usetUInt32LE : (a : ByteArray) → (i : USize) → (v : UInt32) → (h : i.toNat + 4 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt32LE! i.toNat v + +/-- Writes `v` as a big-endian `UInt32` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint32be"] +def usetUInt32BE : (a : ByteArray) → (i : USize) → (v : UInt32) → (h : i.toNat + 4 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt32BE! i.toNat v + +/-! ## UInt64 -/ + +/-- Reads the little-endian `UInt64` at byte offset `off`, or `0` if `off + 8 > a.size`. -/ +@[extern "lean_byte_array_get_uint64le"] +def getUInt64LE! (a : @& ByteArray) (off : @& Nat) : UInt64 := + if off + 8 ≤ a.size then + (a.get! off).toUInt64 ||| + (a.get! (off+1)).toUInt64 <<< 0x8 ||| + (a.get! (off+2)).toUInt64 <<< 0x10 ||| + (a.get! (off+3)).toUInt64 <<< 0x18 ||| + (a.get! (off+4)).toUInt64 <<< 0x20 ||| + (a.get! (off+5)).toUInt64 <<< 0x28 ||| + (a.get! (off+6)).toUInt64 <<< 0x30 ||| + (a.get! (off+7)).toUInt64 <<< 0x38 + else 0 + +/-- Reads the big-endian `UInt64` at byte offset `off`, or `0` if `off + 8 > a.size`. -/ +@[extern "lean_byte_array_get_uint64be"] +def getUInt64BE! (a : @& ByteArray) (off : @& Nat) : UInt64 := + if off + 8 ≤ a.size then + (a.get! off).toUInt64 <<< 0x38 ||| + (a.get! (off+1)).toUInt64 <<< 0x30 ||| + (a.get! (off+2)).toUInt64 <<< 0x28 ||| + (a.get! (off+3)).toUInt64 <<< 0x20 ||| + (a.get! (off+4)).toUInt64 <<< 0x18 ||| + (a.get! (off+5)).toUInt64 <<< 0x10 ||| + (a.get! (off+6)).toUInt64 <<< 0x8 ||| + (a.get! (off+7)).toUInt64 + else 0 + +/-- Writes `v` as a little-endian `UInt64` at byte offset `off`; unchanged if `off + 8 > a.size`. -/ +@[extern "lean_byte_array_set_uint64le"] +def setUInt64LE! (a : ByteArray) (off : @& Nat) (v : UInt64) : ByteArray := + if off + 8 ≤ a.size then + (((((((a.set! off v.toUInt8).set! (off+1) (v >>> 0x8).toUInt8).set! (off+2) + (v >>> 0x10).toUInt8).set! (off+3) (v >>> 0x18).toUInt8).set! (off+4) + (v >>> 0x20).toUInt8).set! (off+5) (v >>> 0x28).toUInt8).set! (off+6) + (v >>> 0x30).toUInt8).set! (off+7) (v >>> 0x38).toUInt8 + else a + +/-- Writes `v` as a big-endian `UInt64` at byte offset `off`; unchanged if `off + 8 > a.size`. -/ +@[extern "lean_byte_array_set_uint64be"] +def setUInt64BE! (a : ByteArray) (off : @& Nat) (v : UInt64) : ByteArray := + if off + 8 ≤ a.size then + (((((((a.set! off (v >>> 0x38).toUInt8).set! (off+1) (v >>> 0x30).toUInt8).set! (off+2) + (v >>> 0x28).toUInt8).set! (off+3) (v >>> 0x20).toUInt8).set! (off+4) + (v >>> 0x18).toUInt8).set! (off+5) (v >>> 0x10).toUInt8).set! (off+6) + (v >>> 0x8).toUInt8).set! (off+7) v.toUInt8 + else a + +/-- Reads the little-endian `UInt64` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint64le"] +def getUInt64LE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 8 ≤ a.size := by get_elem_tactic) → UInt64 + | a, i, _ => a.getUInt64LE! i + +/-- Reads the big-endian `UInt64` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fget_uint64be"] +def getUInt64BE : (a : @& ByteArray) → (i : @& Nat) → (h : i + 8 ≤ a.size := by get_elem_tactic) → UInt64 + | a, i, _ => a.getUInt64BE! i + +/-- Reads the little-endian `UInt64` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint64le"] +def ugetUInt64LE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 8 ≤ a.size := by get_elem_tactic) → UInt64 + | a, i, _ => a.getUInt64LE! i.toNat + +/-- Reads the big-endian `UInt64` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uget_uint64be"] +def ugetUInt64BE : (a : @& ByteArray) → (i : USize) → (h : i.toNat + 8 ≤ a.size := by get_elem_tactic) → UInt64 + | a, i, _ => a.getUInt64BE! i.toNat + +/-- Writes `v` as a little-endian `UInt64` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint64le"] +def setUInt64LE : (a : ByteArray) → (i : @& Nat) → (v : UInt64) → (h : i + 8 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt64LE! i v + +/-- Writes `v` as a big-endian `UInt64` at byte offset `i`. Requires the window to be in bounds. -/ +@[extern "lean_byte_array_fset_uint64be"] +def setUInt64BE : (a : ByteArray) → (i : @& Nat) → (v : UInt64) → (h : i + 8 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt64BE! i v + +/-- Writes `v` as a little-endian `UInt64` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint64le"] +def usetUInt64LE : (a : ByteArray) → (i : USize) → (v : UInt64) → (h : i.toNat + 8 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt64LE! i.toNat v + +/-- Writes `v` as a big-endian `UInt64` at byte offset `i` (`USize`). Requires the window to be in bounds. -/ +@[extern "lean_byte_array_uset_uint64be"] +def usetUInt64BE : (a : ByteArray) → (i : USize) → (v : UInt64) → (h : i.toNat + 8 ≤ a.size := by get_elem_tactic) → ByteArray + | a, i, v, _ => a.setUInt64BE! i.toNat v + +end ByteArray diff --git a/src/Init/Data/ByteArray/Pack/Lemmas.lean b/src/Init/Data/ByteArray/Pack/Lemmas.lean new file mode 100644 index 000000000000..88750b45e30b --- /dev/null +++ b/src/Init/Data/ByteArray/Pack/Lemmas.lean @@ -0,0 +1,273 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Kim Morrison +-/ +module + +prelude +public import Init.Data.ByteArray.Pack +import Init.ByCases +import Init.Data.Array.Bootstrap +import Init.Data.Array.Extract +import Init.Data.Array.Lemmas +import Init.Data.ByteArray.Lemmas +import Init.Data.UInt +import Init.Data.BitVec +import Init.Omega + +public section + +namespace ByteArray + +/-! ### `size` is preserved by writes -/ + +@[simp] theorem size_setUInt16LE! (a : ByteArray) (off : Nat) (v : UInt16) : + (a.setUInt16LE! off v).size = a.size := by unfold setUInt16LE!; split <;> simp +@[simp] theorem size_setUInt16BE! (a : ByteArray) (off : Nat) (v : UInt16) : + (a.setUInt16BE! off v).size = a.size := by unfold setUInt16BE!; split <;> simp +@[simp] theorem size_setUInt32LE! (a : ByteArray) (off : Nat) (v : UInt32) : + (a.setUInt32LE! off v).size = a.size := by unfold setUInt32LE!; split <;> simp +@[simp] theorem size_setUInt32BE! (a : ByteArray) (off : Nat) (v : UInt32) : + (a.setUInt32BE! off v).size = a.size := by unfold setUInt32BE!; split <;> simp +@[simp] theorem size_setUInt64LE! (a : ByteArray) (off : Nat) (v : UInt64) : + (a.setUInt64LE! off v).size = a.size := by unfold setUInt64LE!; split <;> simp +@[simp] theorem size_setUInt64BE! (a : ByteArray) (off : Nat) (v : UInt64) : + (a.setUInt64BE! off v).size = a.size := by unfold setUInt64BE!; split <;> simp + +/-! ### Round-trip: reading back a written value + +These reduce the read of the freshly-written bytes to a fixed-width +bit-recombination identity, discharged by `getLsbD` extensionality. -/ + +theorem getUInt16LE!_setUInt16LE!_self (a : ByteArray) (off : Nat) (v : UInt16) + (h : off + 2 ≤ a.size) : (a.setUInt16LE! off v).getUInt16LE! off = v := by + unfold getUInt16LE! setUInt16LE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt16.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt16.toBitVec_or, UInt16.toBitVec_shiftLeft, UInt16.toBitVec_shiftRight, + UInt16.toBitVec_toUInt8, UInt8.toBitVec_toUInt16, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +theorem getUInt16BE!_setUInt16BE!_self (a : ByteArray) (off : Nat) (v : UInt16) + (h : off + 2 ≤ a.size) : (a.setUInt16BE! off v).getUInt16BE! off = v := by + unfold getUInt16BE! setUInt16BE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt16.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt16.toBitVec_or, UInt16.toBitVec_shiftLeft, UInt16.toBitVec_shiftRight, + UInt16.toBitVec_toUInt8, UInt8.toBitVec_toUInt16, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +theorem getUInt32LE!_setUInt32LE!_self (a : ByteArray) (off : Nat) (v : UInt32) + (h : off + 4 ≤ a.size) : (a.setUInt32LE! off v).getUInt32LE! off = v := by + unfold getUInt32LE! setUInt32LE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt32.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt32.toBitVec_or, UInt32.toBitVec_shiftLeft, UInt32.toBitVec_shiftRight, + UInt32.toBitVec_toUInt8, UInt8.toBitVec_toUInt32, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> by_cases h1 : i < 16 <;> by_cases h2 : i < 24 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +theorem getUInt32BE!_setUInt32BE!_self (a : ByteArray) (off : Nat) (v : UInt32) + (h : off + 4 ≤ a.size) : (a.setUInt32BE! off v).getUInt32BE! off = v := by + unfold getUInt32BE! setUInt32BE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt32.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt32.toBitVec_or, UInt32.toBitVec_shiftLeft, UInt32.toBitVec_shiftRight, + UInt32.toBitVec_toUInt8, UInt8.toBitVec_toUInt32, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> by_cases h1 : i < 16 <;> by_cases h2 : i < 24 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +theorem getUInt64LE!_setUInt64LE!_self (a : ByteArray) (off : Nat) (v : UInt64) + (h : off + 8 ≤ a.size) : (a.setUInt64LE! off v).getUInt64LE! off = v := by + unfold getUInt64LE! setUInt64LE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt64.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt64.toBitVec_or, UInt64.toBitVec_shiftLeft, UInt64.toBitVec_shiftRight, + UInt64.toBitVec_toUInt8, UInt8.toBitVec_toUInt64, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> by_cases h1 : i < 16 <;> by_cases h2 : i < 24 <;> by_cases h3 : i < 32 <;> + by_cases h4 : i < 40 <;> by_cases h5 : i < 48 <;> by_cases h6 : i < 56 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +theorem getUInt64BE!_setUInt64BE!_self (a : ByteArray) (off : Nat) (v : UInt64) + (h : off + 8 ≤ a.size) : (a.setUInt64BE! off v).getUInt64BE! off = v := by + unfold getUInt64BE! setUInt64BE! + rw [ite_eq_left h] + simp only [size_set!, get!_eq_getElem!] + rw [ite_eq_left h] + simp (disch := (first | omega | (simp only [size_set!]; omega))) only + [getElem!_set!_self, getElem!_set!_ne] + apply UInt64.toBitVec_inj.mp + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [UInt64.toBitVec_or, UInt64.toBitVec_shiftLeft, UInt64.toBitVec_shiftRight, + UInt64.toBitVec_toUInt8, UInt8.toBitVec_toUInt64, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', + BitVec.getLsbD_or, BitVec.getLsbD_shiftLeft, BitVec.getLsbD_ushiftRight, + BitVec.getLsbD_setWidth, BitVec.toNat_umod] + by_cases h0 : i < 8 <;> by_cases h1 : i < 16 <;> by_cases h2 : i < 24 <;> by_cases h3 : i < 32 <;> + by_cases h4 : i < 40 <;> by_cases h5 : i < 48 <;> by_cases h6 : i < 56 <;> + first | omega | (cases hb : v.toBitVec[i] <;> simp_all <;> omega) + +/-! ### Disjoint-window invariance + +`getElem!_setUIntWE!_of_outside` is the general fact: a wide write changes only +the bytes in its own `[o, o + W/8)` window, so a read of any byte — and hence a +read of any width or endianness — that lies entirely outside that window is +unaffected. The `_of_disjoint` lemmas below specialize this to a read of the +same width and endianness. -/ + +theorem getElem!_setUInt16LE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt16) + (h : j < o ∨ o + 2 ≤ j) : (a.setUInt16LE! o v)[j]! = a[j]! := by + unfold setUInt16LE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getElem!_setUInt16BE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt16) + (h : j < o ∨ o + 2 ≤ j) : (a.setUInt16BE! o v)[j]! = a[j]! := by + unfold setUInt16BE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getElem!_setUInt32LE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt32) + (h : j < o ∨ o + 4 ≤ j) : (a.setUInt32LE! o v)[j]! = a[j]! := by + unfold setUInt32LE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getElem!_setUInt32BE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt32) + (h : j < o ∨ o + 4 ≤ j) : (a.setUInt32BE! o v)[j]! = a[j]! := by + unfold setUInt32BE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getElem!_setUInt64LE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt64) + (h : j < o ∨ o + 8 ≤ j) : (a.setUInt64LE! o v)[j]! = a[j]! := by + unfold setUInt64LE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getElem!_setUInt64BE!_of_outside (a : ByteArray) (o j : Nat) (v : UInt64) + (h : j < o ∨ o + 8 ≤ j) : (a.setUInt64BE! o v)[j]! = a[j]! := by + unfold setUInt64BE! + split + · simp (disch := (first | omega | (simp only [size_set!]; omega))) only [getElem!_set!_ne] + · rfl + +theorem getUInt16LE!_setUInt16LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt16) + (h₂ : o₂ + 2 ≤ a.size) (hd : o₂ + 2 ≤ o₁ ∨ o₁ + 2 ≤ o₂) : + (a.setUInt16LE! o₁ v).getUInt16LE! o₂ = a.getUInt16LE! o₂ := by + unfold getUInt16LE! + simp only [size_setUInt16LE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt16LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt16LE!_of_outside _ _ _ _ (by omega)] + +theorem getUInt16BE!_setUInt16BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt16) + (h₂ : o₂ + 2 ≤ a.size) (hd : o₂ + 2 ≤ o₁ ∨ o₁ + 2 ≤ o₂) : + (a.setUInt16BE! o₁ v).getUInt16BE! o₂ = a.getUInt16BE! o₂ := by + unfold getUInt16BE! + simp only [size_setUInt16BE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt16BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt16BE!_of_outside _ _ _ _ (by omega)] + +theorem getUInt32LE!_setUInt32LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt32) + (h₂ : o₂ + 4 ≤ a.size) (hd : o₂ + 4 ≤ o₁ ∨ o₁ + 4 ≤ o₂) : + (a.setUInt32LE! o₁ v).getUInt32LE! o₂ = a.getUInt32LE! o₂ := by + unfold getUInt32LE! + simp only [size_setUInt32LE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt32LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32LE!_of_outside _ _ _ _ (by omega)] + +theorem getUInt32BE!_setUInt32BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt32) + (h₂ : o₂ + 4 ≤ a.size) (hd : o₂ + 4 ≤ o₁ ∨ o₁ + 4 ≤ o₂) : + (a.setUInt32BE! o₁ v).getUInt32BE! o₂ = a.getUInt32BE! o₂ := by + unfold getUInt32BE! + simp only [size_setUInt32BE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt32BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt32BE!_of_outside _ _ _ _ (by omega)] + +theorem getUInt64LE!_setUInt64LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt64) + (h₂ : o₂ + 8 ≤ a.size) (hd : o₂ + 8 ≤ o₁ ∨ o₁ + 8 ≤ o₂) : + (a.setUInt64LE! o₁ v).getUInt64LE! o₂ = a.getUInt64LE! o₂ := by + unfold getUInt64LE! + simp only [size_setUInt64LE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64LE!_of_outside _ _ _ _ (by omega)] + +theorem getUInt64BE!_setUInt64BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (v : UInt64) + (h₂ : o₂ + 8 ≤ a.size) (hd : o₂ + 8 ≤ o₁ ∨ o₁ + 8 ≤ o₂) : + (a.setUInt64BE! o₁ v).getUInt64BE! o₂ = a.getUInt64BE! o₂ := by + unfold getUInt64BE! + simp only [size_setUInt64BE!, get!_eq_getElem!] + rw [ite_eq_left h₂, ite_eq_left h₂, + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega), + getElem!_setUInt64BE!_of_outside _ _ _ _ (by omega)] + +end ByteArray diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index b949bea21e1b..6aed4d4f0db8 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1353,6 +1353,90 @@ LEAN_EXPORT bool lean_byte_array_lt(b_lean_obj_arg s1, b_lean_obj_arg s2); LEAN_EXPORT uint8_t lean_byte_array_compare(b_lean_obj_arg s1, b_lean_obj_arg s2); static inline uint8_t lean_byte_array_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_byte_array_lt(s1, s2); } +/* Wide fixed-width unsigned-integer load/store on ByteArray. + + `i` is a *byte* offset into the array. The byte-shift assembly below is + endian-correct on any host (it constructs the little-/big-endian value from + individual bytes, independent of the machine's byte order), and optimizing + compilers can lower it to a wide (possibly unaligned) load or store. The + `uget`/`fget`/`uset`/`fset` variants assume the caller has checked + that the whole `W/8`-byte window `[i, i + W/8)` is in bounds (matching + `lean_byte_array_uget`); the `get`/`set` variants perform an all-or-nothing + bounds check (overflow-safe) and default to `0` / leave the array unchanged + when the window does not fit. */ + +#define LEAN_BYTE_ARRAY_DEFINE_UINT(W, T) \ +static inline T lean_byte_array_uget_uint##W##le(b_lean_obj_arg a, size_t i) { \ + assert(lean_sarray_size(a) >= (W)/8 && i <= lean_sarray_size(a) - (W)/8); \ + const uint8_t * p = lean_sarray_cptr(a) + i; \ + T r = 0; \ + for (unsigned k = 0; k < (W)/8; k++) r |= (T)p[k] << (8u*k); \ + return r; \ +} \ +static inline T lean_byte_array_uget_uint##W##be(b_lean_obj_arg a, size_t i) { \ + assert(lean_sarray_size(a) >= (W)/8 && i <= lean_sarray_size(a) - (W)/8); \ + const uint8_t * p = lean_sarray_cptr(a) + i; \ + T r = 0; \ + for (unsigned k = 0; k < (W)/8; k++) r = (T)(r << 8) | (T)p[k]; \ + return r; \ +} \ +static inline T lean_byte_array_fget_uint##W##le(b_lean_obj_arg a, b_lean_obj_arg i) { \ + return lean_byte_array_uget_uint##W##le(a, lean_unbox(i)); \ +} \ +static inline T lean_byte_array_fget_uint##W##be(b_lean_obj_arg a, b_lean_obj_arg i) { \ + return lean_byte_array_uget_uint##W##be(a, lean_unbox(i)); \ +} \ +static inline T lean_byte_array_get_uint##W##le(b_lean_obj_arg a, b_lean_obj_arg i) { \ + if (!lean_is_scalar(i)) return 0; \ + size_t idx = lean_unbox(i), sz = lean_sarray_size(a); \ + if (sz < (W)/8 || idx > sz - (W)/8) return 0; \ + return lean_byte_array_uget_uint##W##le(a, idx); \ +} \ +static inline T lean_byte_array_get_uint##W##be(b_lean_obj_arg a, b_lean_obj_arg i) { \ + if (!lean_is_scalar(i)) return 0; \ + size_t idx = lean_unbox(i), sz = lean_sarray_size(a); \ + if (sz < (W)/8 || idx > sz - (W)/8) return 0; \ + return lean_byte_array_uget_uint##W##be(a, idx); \ +} \ +static inline lean_object * lean_byte_array_uset_uint##W##le(lean_obj_arg a, size_t i, T v) { \ + assert(lean_sarray_size(a) >= (W)/8 && i <= lean_sarray_size(a) - (W)/8); \ + lean_obj_res r = lean_sarray_ensure_exclusive(a); \ + uint8_t * p = lean_sarray_cptr(r) + i; \ + for (unsigned k = 0; k < (W)/8; k++) p[k] = (uint8_t)(v >> (8u*k)); \ + return r; \ +} \ +static inline lean_object * lean_byte_array_uset_uint##W##be(lean_obj_arg a, size_t i, T v) { \ + assert(lean_sarray_size(a) >= (W)/8 && i <= lean_sarray_size(a) - (W)/8); \ + lean_obj_res r = lean_sarray_ensure_exclusive(a); \ + uint8_t * p = lean_sarray_cptr(r) + i; \ + for (unsigned k = 0; k < (W)/8; k++) p[k] = (uint8_t)(v >> (8u*((W)/8 - 1u - k))); \ + return r; \ +} \ +static inline lean_object * lean_byte_array_fset_uint##W##le(lean_obj_arg a, b_lean_obj_arg i, T v) {\ + return lean_byte_array_uset_uint##W##le(a, lean_unbox(i), v); \ +} \ +static inline lean_object * lean_byte_array_fset_uint##W##be(lean_obj_arg a, b_lean_obj_arg i, T v) {\ + return lean_byte_array_uset_uint##W##be(a, lean_unbox(i), v); \ +} \ +static inline lean_object * lean_byte_array_set_uint##W##le(lean_obj_arg a, b_lean_obj_arg i, T v) { \ + if (!lean_is_scalar(i)) return a; \ + size_t idx = lean_unbox(i), sz = lean_sarray_size(a); \ + if (sz < (W)/8 || idx > sz - (W)/8) return a; \ + return lean_byte_array_uset_uint##W##le(a, idx, v); \ +} \ +static inline lean_object * lean_byte_array_set_uint##W##be(lean_obj_arg a, b_lean_obj_arg i, T v) { \ + if (!lean_is_scalar(i)) return a; \ + size_t idx = lean_unbox(i), sz = lean_sarray_size(a); \ + if (sz < (W)/8 || idx > sz - (W)/8) return a; \ + return lean_byte_array_uset_uint##W##be(a, idx, v); \ +} + +LEAN_BYTE_ARRAY_DEFINE_UINT(16, uint16_t) +LEAN_BYTE_ARRAY_DEFINE_UINT(32, uint32_t) +LEAN_BYTE_ARRAY_DEFINE_UINT(64, uint64_t) + +#undef LEAN_BYTE_ARRAY_DEFINE_UINT + /* FloatArray (special case of Array of Scalars) */ LEAN_EXPORT lean_obj_res lean_float_array_mk(lean_obj_arg a); diff --git a/tests/elab/bytearray_pack.lean b/tests/elab/bytearray_pack.lean new file mode 100644 index 000000000000..eeec2bb9a55a --- /dev/null +++ b/tests/elab/bytearray_pack.lean @@ -0,0 +1,68 @@ +/-! +Tests for the wide fixed-width integer accessors on `ByteArray` +(`Init.Data.ByteArray.Pack`). These `#guard`s evaluate the accessors on concrete +inputs, checking values, endianness, the all-or-nothing out-of-bounds behaviour, +and round-trip — complementing the spec-level lemmas in +`Init.Data.ByteArray.Lemmas`. +-/ + +def a : ByteArray := [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray + +-- Values + endianness (defaulting `!` reads). +#guard a.getUInt16LE! 0 == 0x2211 +#guard a.getUInt16BE! 0 == 0x1122 +#guard a.getUInt32LE! 0 == 0x44332211 +#guard a.getUInt32BE! 0 == 0x11223344 +#guard a.getUInt32LE! 2 == 0x66554433 +#guard a.getUInt64LE! 0 == 0x8877665544332211 +#guard a.getUInt64BE! 0 == 0x1122334455667788 +#guard a.getUInt16LE! 6 == 0x8877 + +-- Proof-carrying `uget`/`get` go through different externs; check they agree. +#guard a.ugetUInt32LE 0 (by decide) == 0x44332211 +#guard a.ugetUInt32BE 0 (by decide) == 0x11223344 +#guard a.getUInt32LE 2 (by decide) == 0x66554433 +#guard a.ugetUInt64LE 0 (by decide) == 0x8877665544332211 + +-- All-or-nothing out-of-bounds: a partial window reads as `0`. +#guard a.getUInt32LE! 5 == 0 -- 5 + 4 > 8 +#guard a.getUInt32LE! 8 == 0 +#guard a.getUInt16LE! 7 == 0 -- 7 + 2 > 8 +#guard a.getUInt32LE! 1000000 == 0 -- huge offset +#guard a.getUInt64LE! 1 == 0 -- 1 + 8 > 8 +#guard a.getUInt32LE! (2 ^ 100) == 0 -- non-scalar (bignum) offset + +-- Round-trip: read back what was written. +#guard (a.setUInt16LE! 0 0xBEEF).getUInt16LE! 0 == 0xBEEF +#guard (a.setUInt16BE! 0 0xBEEF).getUInt16BE! 0 == 0xBEEF +#guard (a.setUInt32LE! 0 0xDEADBEEF).getUInt32LE! 0 == 0xDEADBEEF +#guard (a.setUInt32BE! 1 0xDEADBEEF).getUInt32BE! 1 == 0xDEADBEEF +#guard (a.setUInt64LE! 0 0x0123456789ABCDEF).getUInt64LE! 0 == 0x0123456789ABCDEF +#guard (a.usetUInt32LE 0 0xCAFEBABE (by decide)).ugetUInt32LE 0 (by decide) == 0xCAFEBABE + +-- Byte order on write: little-endian writes the low byte first. +#guard (a.setUInt16LE! 0 0xBEEF).get! 0 == 0xEF +#guard (a.setUInt16LE! 0 0xBEEF).get! 1 == 0xBE +#guard (a.setUInt16BE! 0 0xBEEF).get! 0 == 0xBE + +-- All-or-nothing write: an out-of-range write leaves the array unchanged. +#guard (a.setUInt32LE! 5 0xDEADBEEF) == a +#guard (a.setUInt64LE! 1 0) == a +#guard (a.setUInt32LE! 1000000 0xFF) == a +#guard (a.setUInt32LE! (2 ^ 100) 0xFF) == a -- non-scalar (bignum) offset + +-- Size is preserved by writes. +#guard (a.setUInt32LE! 0 0xDEADBEEF).size == a.size + +-- Round-trip for big-endian writes too. +#guard (a.setUInt32BE! 0 0xDEADBEEF).getUInt32BE! 0 == 0xDEADBEEF +#guard (a.setUInt64BE! 0 0x0123456789ABCDEF).getUInt64BE! 0 == 0x0123456789ABCDEF +#guard (a.setUInt16BE! 0 0xBEEF).get! 1 == 0xEF + +-- Exact upper boundary: a window ending exactly at `size` is in bounds. +#guard a.getUInt32LE! 4 == 0x88776655 -- 4 + 4 = 8 = size +#guard (a.setUInt32LE! 4 0xDEADBEEF).getUInt32LE! 4 == 0xDEADBEEF + +-- Disjoint windows do not interfere. +#guard (a.setUInt16LE! 0 0xFFFF).getUInt16LE! 2 == a.getUInt16LE! 2 +#guard (a.setUInt32LE! 4 0xFFFFFFFF).getUInt32LE! 0 == a.getUInt32LE! 0