Theorems about Bytes.* primitives

The runtime side of every primitive is its C function in bytes_ffi.c, but the Lean body is the spec: each @[extern]-tagged declaration has a definitional unfolding that the kernel can reduce. The theorems below establish the basic algebraic laws over those specs:

• Tier 1 — size preservation, OOB-noop, and store/load roundtrip for every width × endianness.
• Tier 2 — pointwise characterizations of copy/fill and reflection lemmas for equal/compare.
• Tier 3 — endianness symmetry: loadUNBE = (loadUNLE).byteSwap and the corresponding store laws.

Together these let you reason about Lean code that uses the primitives without having to unfold the cascaded set!s by hand.

This file is opt-in: import Bytes gets only the runtime API; import Bytes.Theorems brings the theorems in too.

Axiom footprint

In addition to the three standard axioms (propext, Quot.sound, Classical.choice), the bit-shuffling roundtrip and endianness theorems use bv_decide, which emits per-call _native.bv_decide.ax_* axioms backed by an externally-verified LRAT proof certificate. These are the standard cost of mechanised bit-vector reasoning and are accepted upstream.

Helpers on ByteArray

Stdlib's ByteArray.set! lacks the standard bang-version simp lemmas (stdlib's set/get lemmas are stated for Array.setIfInBounds/ getElem). The three lemmas below bridge them to ByteArray.set! and ByteArray.get!. They are local helpers — sound and reusable, but not the headline API.

@[simp]

theorem ByteArray.data_set! (a : ByteArray) (i : Nat) (b : UInt8) : (a.set! i b).data = a.data.set! i b

theorem ByteArray.get!_eq_data (a : ByteArray) (i : Nat) : a.get! i = a.data[i]!

@[simp]

theorem ByteArray.size_set! (a : ByteArray) (i : Nat) (b : UInt8) : (a.set! i b).size = a.size

theorem ByteArray.get!_set!_self (a : ByteArray) (i : Nat) (b : UInt8) (h : i < a.size) : (a.set! i b).get! i = b

theorem ByteArray.get!_set!_ne (a : ByteArray) (i j : Nat) (b : UInt8) (h : i ≠ j) : (a.set! i b).get! j = a.get! j

extract / append algebra (the get!-flavour lemmas Std skips)

Stdlib proves the corresponding [i]-flavour facts (getElem_append_left, extract_append, extract_extract, …), but production code that uses get!/extract directly needs the bang-version bridges below. The clamp specialisation extract_eq_extract_size_of_size_le and its append corollary extract_append_size_of_le close the gap: Std proves the clamp only for Array (extract_of_size_lt / extract_eq_self_of_le); the ByteArray version was missing.

theorem ByteArray.extract_eq_extract_size_of_size_le {a : ByteArray} {i j : Nat} (h : a.size ≤ j) : a.extract i j = a.extract i a.size

Extract clamps the end index at .size.

theorem ByteArray.extract_append_size_of_le {p extra : ByteArray} {t : Nat} (h : t ≤ p.size) : (p ++ extra).extract t (p ++ extra).size = p.extract t p.size ++ extra

Clamp+append fusion: when the start lies in the prefix, extracting through the end of the appended pair gives the prefix tail concatenated with the entire suffix.

theorem ByteArray.get!_append_left {a b : ByteArray} {i : Nat} (h : i < a.size) : (a ++ b).get! i = a.get! i

get! analogue of Std's getElem_append_left.

theorem ByteArray.get!_extract {a : ByteArray} {s e i : Nat} (h_lt : s + i < e) (h_size : s + i < a.size) : (a.extract s e).get! i = a.get! (s + i)

get! through extract: indices map via the start offset.

Tier 1 — size preservation

Stores never resize their argument. Trivial via the helper above plus the fact that the if-branches return data.set!-cascades or data itself.

@[simp]

theorem Bytes.storeU8_size (data : ByteArray) (off : Nat) (val : UInt8) : (storeU8 data off val).size = data.size

@[simp]

theorem Bytes.storeU16LE_size (data : ByteArray) (off : Nat) (val : UInt16) : (storeU16LE data off val).size = data.size

@[simp]

theorem Bytes.storeU16BE_size (data : ByteArray) (off : Nat) (val : UInt16) : (storeU16BE data off val).size = data.size

@[simp]

theorem Bytes.storeU32LE_size (data : ByteArray) (off : Nat) (val : UInt32) : (storeU32LE data off val).size = data.size

@[simp]

theorem Bytes.storeU32BE_size (data : ByteArray) (off : Nat) (val : UInt32) : (storeU32BE data off val).size = data.size

@[simp]

theorem Bytes.storeU64LE_size (data : ByteArray) (off : Nat) (val : UInt64) : (storeU64LE data off val).size = data.size

@[simp]

theorem Bytes.storeU64BE_size (data : ByteArray) (off : Nat) (val : UInt64) : (storeU64BE data off val).size = data.size

Tier 1 — OOB no-op

When the requested write would fall (partly) outside the buffer, the store returns data unchanged.

theorem Bytes.storeU8_oob (data : ByteArray) {off : Nat} (val : UInt8) (h : off ≥ data.size) : storeU8 data off val = data

theorem Bytes.storeU16LE_oob (data : ByteArray) {off : Nat} (val : UInt16) (h : off + 2 > data.size) : storeU16LE data off val = data

theorem Bytes.storeU16BE_oob (data : ByteArray) {off : Nat} (val : UInt16) (h : off + 2 > data.size) : storeU16BE data off val = data

theorem Bytes.storeU32LE_oob (data : ByteArray) {off : Nat} (val : UInt32) (h : off + 4 > data.size) : storeU32LE data off val = data

theorem Bytes.storeU32BE_oob (data : ByteArray) {off : Nat} (val : UInt32) (h : off + 4 > data.size) : storeU32BE data off val = data

theorem Bytes.storeU64LE_oob (data : ByteArray) {off : Nat} (val : UInt64) (h : off + 8 > data.size) : storeU64LE data off val = data

theorem Bytes.storeU64BE_oob (data : ByteArray) {off : Nat} (val : UInt64) (h : off + 8 > data.size) : storeU64BE data off val = data

Tier 1 — store/load roundtrip

Writing a value with storeUNXX and immediately reading it back with loadUNXX returns the original value, provided the write fits in the buffer. The single-byte case is direct; the multi-byte cases reduce to a chain of get!_set!_self/get!_set!_ne and a final bit-vector identity (bv_decide).

theorem Bytes.loadU8_storeU8_eq (data : ByteArray) (off : Nat) (val : UInt8) (h : off < data.size) : loadU8 (storeU8 data off val) off = val

theorem Bytes.loadU16LE_storeU16LE_eq (data : ByteArray) (off : Nat) (val : UInt16) (h : off + 2 ≤ data.size) : loadU16LE (storeU16LE data off val) off = val

theorem Bytes.loadU16BE_storeU16BE_eq (data : ByteArray) (off : Nat) (val : UInt16) (h : off + 2 ≤ data.size) : loadU16BE (storeU16BE data off val) off = val

theorem Bytes.loadU32LE_storeU32LE_eq (data : ByteArray) (off : Nat) (val : UInt32) (h : off + 4 ≤ data.size) : loadU32LE (storeU32LE data off val) off = val

theorem Bytes.loadU32BE_storeU32BE_eq (data : ByteArray) (off : Nat) (val : UInt32) (h : off + 4 ≤ data.size) : loadU32BE (storeU32BE data off val) off = val

theorem Bytes.loadU64LE_storeU64LE_eq (data : ByteArray) (off : Nat) (val : UInt64) (h : off + 8 ≤ data.size) : loadU64LE (storeU64LE data off val) off = val

theorem Bytes.loadU64BE_storeU64BE_eq (data : ByteArray) (off : Nat) (val : UInt64) (h : off + 8 ≤ data.size) : loadU64BE (storeU64BE data off val) off = val

Tier 2 — bulk op invariant helper

Nat.fold n f init is the spec primitive used by copy, fill, equal, and compare. Most of the bulk-op lemmas reduce to "this property is preserved by every step", so we prove that pattern once.

Tier 2 — copy and fill size preservation

@[simp]

theorem Bytes.copy_size (src : ByteArray) (srcOff : Nat) (dst : ByteArray) (dstOff len : Nat) : (copy src srcOff dst dstOff len).size = dst.size

@[simp]

theorem Bytes.fill_size (data : ByteArray) (off len : Nat) (val : UInt8) : (fill data off len val).size = data.size

Tier 2 — copy/fill/equal/compare OOB no-op

theorem Bytes.copy_oob_src (src : ByteArray) {srcOff : Nat} (dst : ByteArray) (dstOff len : Nat) (h : srcOff + len > src.size) : copy src srcOff dst dstOff len = dst

theorem Bytes.copy_oob_dst (src : ByteArray) (srcOff : Nat) (dst : ByteArray) {dstOff len : Nat} (h : dstOff + len > dst.size) : copy src srcOff dst dstOff len = dst

theorem Bytes.fill_oob (data : ByteArray) {off len : Nat} (val : UInt8) (h : off + len > data.size) : fill data off len val = data

theorem Bytes.equal_oob_a (a : ByteArray) {aOff : Nat} (b : ByteArray) (bOff len : Nat) (h : aOff + len > a.size) : equal a aOff b bOff len = false

theorem Bytes.equal_oob_b (a : ByteArray) (aOff : Nat) (b : ByteArray) {bOff len : Nat} (h : bOff + len > b.size) : equal a aOff b bOff len = false

theorem Bytes.compare_oob_a (a : ByteArray) {aOff : Nat} (b : ByteArray) (bOff len : Nat) (h : aOff + len > a.size) : compare a aOff b bOff len = Ordering.eq

theorem Bytes.compare_oob_b (a : ByteArray) (aOff : Nat) (b : ByteArray) {bOff len : Nat} (h : bOff + len > b.size) : compare a aOff b bOff len = Ordering.eq

Tier 2 — equal/compare reflexivity

equal a off a off len is true and compare a off a off len is .eq, provided the range fits. The fold accumulator is invariant: at every step both sides agree.

theorem Bytes.equal_self (a : ByteArray) (off len : Nat) (h : off + len ≤ a.size) : equal a off a off len = true

theorem Bytes.compare_self (a : ByteArray) (off len : Nat) (h : off + len ≤ a.size) : compare a off a off len = Ordering.eq

Tier 2 — copy / fill pointwise characterizations

Both copy and fill reduce to a Nat.fold of set! calls at distinct offsets, so we can characterize the result byte-by-byte: inside the written window the value is what was written, outside it the buffer is untouched. The two private fold helpers below capture the inductive content; the headline _get_in_range / _get_out_range theorems specialize to fill and copy.

theorem Bytes.fill_get_in_range (data : ByteArray) (off len : Nat) (val : UInt8) (h : off + len ≤ data.size) (k : Nat) (hk : k < len) : (fill data off len val).get! (off + k) = val

theorem Bytes.fill_get_out_range (data : ByteArray) (off len : Nat) (val : UInt8) (j : Nat) (hj : j < off ∨ j ≥ off + len) : (fill data off len val).get! j = data.get! j

theorem Bytes.copy_get_in_range (src : ByteArray) (srcOff : Nat) (dst : ByteArray) (dstOff len : Nat) (hsrc : srcOff + len ≤ src.size) (hdst : dstOff + len ≤ dst.size) (k : Nat) (hk : k < len) : (copy src srcOff dst dstOff len).get! (dstOff + k) = src.get! (srcOff + k)

theorem Bytes.copy_get_out_range (src : ByteArray) (srcOff : Nat) (dst : ByteArray) (dstOff len j : Nat) (hj : j < dstOff ∨ j ≥ dstOff + len) : (copy src srcOff dst dstOff len).get! j = dst.get! j

Tier 3 — endianness symmetry

loadUNBE reads the same bytes as loadUNLE but with the bytes reversed. We package that observation as loadUNBE = byteSwapN (loadUNLE) (and dually for stores). The byte-swap helpers below are proof-side conveniences; the runtime never calls them.

def Bytes.byteSwap16 (x : UInt16) : UInt16

16-bit byte swap: high byte ↔ low byte.

Equations

• Bytes.byteSwap16 x = x <<< 8 ||| x >>> 8

def Bytes.byteSwap32 (x : UInt32) : UInt32

32-bit byte swap: reverses the four bytes.

Equations

• Bytes.byteSwap32 x = (x &&& 255) <<< 24 ||| (x &&& 65280) <<< 8 ||| (x &&& 16711680) >>> 8 ||| (x &&& 4278190080) >>> 24

def Bytes.byteSwap64 (x : UInt64) : UInt64

64-bit byte swap: reverses the eight bytes.

Equations

• One or more equations did not get rendered due to their size.

theorem Bytes.loadU16BE_eq_byteSwap_loadU16LE (data : ByteArray) (off : Nat) : loadU16BE data off = byteSwap16 (loadU16LE data off)

theorem Bytes.loadU32BE_eq_byteSwap_loadU32LE (data : ByteArray) (off : Nat) : loadU32BE data off = byteSwap32 (loadU32LE data off)

theorem Bytes.loadU64BE_eq_byteSwap_loadU64LE (data : ByteArray) (off : Nat) : loadU64BE data off = byteSwap64 (loadU64LE data off)

theorem Bytes.storeU16BE_eq_storeU16LE_byteSwap (data : ByteArray) (off : Nat) (val : UInt16) : storeU16BE data off val = storeU16LE data off (byteSwap16 val)

theorem Bytes.storeU32BE_eq_storeU32LE_byteSwap (data : ByteArray) (off : Nat) (val : UInt32) : storeU32BE data off val = storeU32LE data off (byteSwap32 val)

theorem Bytes.storeU64BE_eq_storeU64LE_byteSwap (data : ByteArray) (off : Nat) (val : UInt64) : storeU64BE data off val = storeU64LE data off (byteSwap64 val)