From ce55a45993321a264831a1a07d024cab4c6767b7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 15 Jun 2026 08:51:45 +0000 Subject: [PATCH 1/6] feat: wide fixed-width integer load/store accessors on ByteArray This PR adds little- and big-endian UInt16/UInt32/UInt64 load and store accessors to ByteArray, reading or writing a fixed-width integer at a byte offset in a single native load/store rather than through a boxed Array UInt32 or hand-written byte assembly. For each width and endianness there are defaulting (`!`), Nat-with-proof, and USize-with-proof variants mirroring the existing byte accessors; the defaulting variants are all-or-nothing on bounds. Hot loops should use the USize-indexed `uget*`/`uset*` forms, since the Nat-indexed variants box the index (the module docstring says so). Lemmas in Init.Data.ByteArray.Lemmas establish the proof-carrying variants as the `!` model, size preservation, and round-trip (`get* (set* a off v) off = v`, with the bit-recombination identity discharged by getLsbD extensionality, no bv_decide). Disjointness is stated at the byte level: a wide write changes only the bytes in its own window, so a read of any width/endianness outside that window is unaffected. Tests in tests/elab/bytearray_pack.lean check the @[extern] C against the Lean model. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/Init/Data/ByteArray.lean | 1 + src/Init/Data/ByteArray/Lemmas.lean | 259 +++++++++++++++++- src/Init/Data/ByteArray/Pack.lean | 281 ++++++++++++++++++++ src/include/lean/lean.h | 84 ++++++ tests/elab/bytearray_pack.lean | 68 +++++ tests/elab/bytearray_pack.lean.out.expected | 0 6 files changed, 692 insertions(+), 1 deletion(-) create mode 100644 src/Init/Data/ByteArray/Pack.lean create mode 100644 tests/elab/bytearray_pack.lean create mode 100644 tests/elab/bytearray_pack.lean.out.expected diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index eeab7dd85f51..2a4a33a9f987 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -9,4 +9,5 @@ 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 diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index f7650aeda042..6817ba4dd958 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -7,10 +7,13 @@ module prelude public import Init.Data.ByteArray.Basic +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.UInt +import Init.Data.BitVec import Init.Omega public section @@ -405,4 +408,258 @@ 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 -end ByteArray +theorem get!_eq_getElem! (a : ByteArray) (i : Nat) : a.get! i = a[i]! := by + rw [getElem!_eq_data_getElem!]; rfl + +/-! ### `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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 \ No newline at end of file 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/include/lean/lean.h b/src/include/lean/lean.h index bdac8b809ded..e2ed85f7933a 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1128,6 +1128,90 @@ 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); } +/* 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_is_exclusive(a) ? a : lean_copy_byte_array(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_is_exclusive(a) ? a : lean_copy_byte_array(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 diff --git a/tests/elab/bytearray_pack.lean.out.expected b/tests/elab/bytearray_pack.lean.out.expected new file mode 100644 index 000000000000..e69de29bb2d1 From a9687de5fcd423ab98c1f2bc23b848f5db2c1770 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 26 Aug 2026 14:28:15 +1000 Subject: [PATCH 2/6] chore: remove empty bytearray_pack.lean.out.expected --- tests/elab/bytearray_pack.lean.out.expected | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 tests/elab/bytearray_pack.lean.out.expected diff --git a/tests/elab/bytearray_pack.lean.out.expected b/tests/elab/bytearray_pack.lean.out.expected deleted file mode 100644 index e69de29bb2d1..000000000000 From 5f9b9aed33ced2570e2f2021068d9d36c724a1e0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 26 Aug 2026 15:17:28 +1000 Subject: [PATCH 3/6] refactor: move wide-accessor lemmas to Init.Data.ByteArray.Pack.Lemmas Init.Data.String.Defs imports Init.Data.ByteArray.Lemmas, which places that module below the UInt/BitVec lemma layer; importing Init.Data.UInt and Init.Data.BitVec there closes an import cycle. Move the lemmas that need them into a new downstream module instead. --- src/Init/Data/ByteArray.lean | 1 + src/Init/Data/ByteArray/Lemmas.lean | 256 +-------------------- src/Init/Data/ByteArray/Pack/Lemmas.lean | 269 +++++++++++++++++++++++ 3 files changed, 271 insertions(+), 255 deletions(-) create mode 100644 src/Init/Data/ByteArray/Pack/Lemmas.lean diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean index 2a4a33a9f987..24692c3efcff 100644 --- a/src/Init/Data/ByteArray.lean +++ b/src/Init/Data/ByteArray.lean @@ -11,3 +11,4 @@ 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.Pack.Lemmas diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index 705046222d94..456fbdd0992d 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -7,13 +7,10 @@ module prelude public import Init.Data.ByteArray.Basic -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.UInt -import Init.Data.BitVec import Init.Omega public section @@ -411,255 +408,4 @@ private theorem getElem!_eq_data_getElem! (data : ByteArray) (i : Nat) : theorem get!_eq_getElem! (a : ByteArray) (i : Nat) : a.get! i = a[i]! := by rw [getElem!_eq_data_getElem!]; rfl -/-! ### `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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h] - simp only [size_set!, get!_eq_getElem!] - rw [if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 \ No newline at end of file +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..23726455624f --- /dev/null +++ b/src/Init/Data/ByteArray/Pack/Lemmas.lean @@ -0,0 +1,269 @@ +/- +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.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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h] + simp only [size_set!, get!_eq_getElem!] + rw [if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 [if_pos h₂, if_pos 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 From 00c99b9f999039aa056bd8ae7f7d2a662397190a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 26 Aug 2026 15:47:25 +1000 Subject: [PATCH 4/6] fix: restore the tactic and Array imports the moved lemmas relied on --- src/Init/Data/ByteArray/Pack/Lemmas.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Data/ByteArray/Pack/Lemmas.lean b/src/Init/Data/ByteArray/Pack/Lemmas.lean index 23726455624f..4cdc5dc7c337 100644 --- a/src/Init/Data/ByteArray/Pack/Lemmas.lean +++ b/src/Init/Data/ByteArray/Pack/Lemmas.lean @@ -7,6 +7,10 @@ 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 From 0c7cb7bb1e846168d2afed0d1f9f08e65116ca31 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 26 Aug 2026 16:36:31 +1000 Subject: [PATCH 5/6] chore: if_pos was deprecated in favour of ite_eq_left --- src/Init/Data/ByteArray/Pack/Lemmas.lean | 36 ++++++++++++------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/ByteArray/Pack/Lemmas.lean b/src/Init/Data/ByteArray/Pack/Lemmas.lean index 4cdc5dc7c337..88750b45e30b 100644 --- a/src/Init/Data/ByteArray/Pack/Lemmas.lean +++ b/src/Init/Data/ByteArray/Pack/Lemmas.lean @@ -43,9 +43,9 @@ 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -61,9 +61,9 @@ theorem getUInt16LE!_setUInt16LE!_self (a : ByteArray) (off : Nat) (v : UInt16) 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -79,9 +79,9 @@ theorem getUInt16BE!_setUInt16BE!_self (a : ByteArray) (off : Nat) (v : UInt16) 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -97,9 +97,9 @@ theorem getUInt32LE!_setUInt32LE!_self (a : ByteArray) (off : Nat) (v : UInt32) 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -115,9 +115,9 @@ theorem getUInt32BE!_setUInt32BE!_self (a : ByteArray) (off : Nat) (v : UInt32) 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -134,9 +134,9 @@ theorem getUInt64LE!_setUInt64LE!_self (a : ByteArray) (off : Nat) (v : UInt64) 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 [if_pos h] + rw [ite_eq_left h] simp only [size_set!, get!_eq_getElem!] - rw [if_pos h] + 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 @@ -205,7 +205,7 @@ theorem getUInt16LE!_setUInt16LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt16LE! o₁ v).getUInt16LE! o₂ = a.getUInt16LE! o₂ := by unfold getUInt16LE! simp only [size_setUInt16LE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + rw [ite_eq_left h₂, ite_eq_left h₂, getElem!_setUInt16LE!_of_outside _ _ _ _ (by omega), getElem!_setUInt16LE!_of_outside _ _ _ _ (by omega)] @@ -214,7 +214,7 @@ theorem getUInt16BE!_setUInt16BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt16BE! o₁ v).getUInt16BE! o₂ = a.getUInt16BE! o₂ := by unfold getUInt16BE! simp only [size_setUInt16BE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + rw [ite_eq_left h₂, ite_eq_left h₂, getElem!_setUInt16BE!_of_outside _ _ _ _ (by omega), getElem!_setUInt16BE!_of_outside _ _ _ _ (by omega)] @@ -223,7 +223,7 @@ theorem getUInt32LE!_setUInt32LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt32LE! o₁ v).getUInt32LE! o₂ = a.getUInt32LE! o₂ := by unfold getUInt32LE! simp only [size_setUInt32LE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + 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), @@ -234,7 +234,7 @@ theorem getUInt32BE!_setUInt32BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt32BE! o₁ v).getUInt32BE! o₂ = a.getUInt32BE! o₂ := by unfold getUInt32BE! simp only [size_setUInt32BE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + 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), @@ -245,7 +245,7 @@ theorem getUInt64LE!_setUInt64LE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt64LE! o₁ v).getUInt64LE! o₂ = a.getUInt64LE! o₂ := by unfold getUInt64LE! simp only [size_setUInt64LE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + 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), @@ -260,7 +260,7 @@ theorem getUInt64BE!_setUInt64BE!_of_disjoint (a : ByteArray) (o₁ o₂ : Nat) (a.setUInt64BE! o₁ v).getUInt64BE! o₂ = a.getUInt64BE! o₂ := by unfold getUInt64BE! simp only [size_setUInt64BE!, get!_eq_getElem!] - rw [if_pos h₂, if_pos h₂, + 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), From ae6bd28905559939c42cb1f89d24a930fdd834e2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 6 Oct 2026 12:48:28 +1100 Subject: [PATCH 6/6] fix: use lean_sarray_ensure_exclusive in wide ByteArray setters lean_copy_byte_array was removed from lean.h by #15052; follow the other ByteArray setters and use lean_sarray_ensure_exclusive. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/include/lean/lean.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 5748be28238d..6aed4d4f0db8 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1400,14 +1400,14 @@ static inline T lean_byte_array_get_uint##W##be(b_lean_obj_arg a, b_lean_obj_arg } \ 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_is_exclusive(a) ? a : lean_copy_byte_array(a); \ + 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_is_exclusive(a) ? a : lean_copy_byte_array(a); \ + 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; \