Skip to main content

mkit_core/
delta.rs

1//! Delta instruction stream — implements the versioned format required
2//! by `docs/specs/SPEC-DELTA.md`.
3//!
4//! Stream layout (SPEC-DELTA §2):
5//!
6//! ```text
7//! [u8  stream_version == 0x01]
8//! [u32 LE base_len]            length of the base object
9//! [u32 LE result_len]          expected length of the reconstruction
10//! [instructions ...]           sequence of opcodes
11//! ```
12//!
13//! Two opcodes (SPEC-DELTA §3):
14//!
15//! * `0x80` (COPY): `[opcode][u32 LE offset][u16 LE length]` = 7 bytes.
16//!   `length` MUST be `>= 1` and `offset + length <= base_len`. The
17//!   remaining 7 low bits of the opcode are reserved and MUST be 0 in v1.
18//! * `0x01..=0x7F` (INSERT): the opcode byte is the literal length (1..127),
19//!   followed by that many literal bytes. Long literals are split into
20//!   multiple INSERTs; there is no extended-length form in v1.
21//!
22//! `0x00` is **reserved** and MUST be rejected.
23
24use crate::object::MkitError;
25
26/// The specific kind of structural corruption a v1 delta stream failed
27/// on (MKIT-13), carried by [`MkitError::DeltaCorrupt`]. `#[non_exhaustive]`
28/// so a future delta-stream kind (v2, say) can add a corruption variant
29/// without that being a breaking change for downstream `match`es.
30#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)]
31#[non_exhaustive]
32pub enum DeltaCorruption {
33    /// The stream's declared `base_len` header field does not match the
34    /// actual length of the base object passed to `decode`.
35    #[error("declared base_len {declared} does not match the actual base length {actual}")]
36    BaseLenMismatch { declared: u32, actual: usize },
37    /// A `COPY` opcode had one or more of its reserved low 7 bits set.
38    #[error("COPY opcode {0:#04x} has reserved low bits set")]
39    ReservedOpcodeBits(u8),
40    /// The reserved `0x00` opcode appeared in the instruction stream.
41    #[error("opcode 0x00 is reserved and must not appear in the instruction stream")]
42    ZeroOpcode,
43    /// A `COPY` opcode declared a zero-length copy, which SPEC-DELTA §3
44    /// forbids (`length` MUST be `>= 1`).
45    #[error("COPY opcode declared a zero-length copy")]
46    ZeroLengthCopy,
47    /// A `COPY` opcode's `offset + length` exceeds the base length (or
48    /// overflows while computing it), reading past the end of the base.
49    #[error("COPY offset {offset} + length {length} exceeds base_len {base_len} (or overflowed)")]
50    CopyPastBase {
51        offset: u32,
52        length: u16,
53        base_len: usize,
54    },
55    /// Applying the next instruction would emit more bytes than the
56    /// stream's declared `result_len`.
57    #[error(
58        "emitting {requested} more byte(s) after {emitted} would exceed the declared result_len {result_len}"
59    )]
60    ResultLenOverrun {
61        emitted: usize,
62        requested: usize,
63        result_len: usize,
64    },
65    /// The instruction stream ended having emitted fewer bytes than the
66    /// declared `result_len`.
67    #[error("stream ended after emitting {actual} byte(s), declared result_len is {expected}")]
68    ResultLenUnderrun { expected: usize, actual: usize },
69}
70
71/// Shorthand: wrap a [`DeltaCorruption`] as the corresponding
72/// [`MkitError`] variant, so `decode`'s error sites stay one-liners.
73fn corrupt(kind: DeltaCorruption) -> MkitError {
74    MkitError::DeltaCorrupt(kind)
75}
76
77/// Version byte at offset 0 of every v1 delta stream.
78pub const STREAM_VERSION: u8 = 0x01;
79/// `COPY` opcode — top bit set, low seven bits reserved (must be zero).
80pub const OP_COPY: u8 = 0x80;
81/// Maximum bytes encodable in a single `INSERT` opcode.
82pub const MAX_INSERT_LEN: usize = 127;
83/// Fixed prefix size: 1 byte version + 4 byte `base_len` + 4 byte `result_len`.
84pub const HEADER_LEN: usize = 1 + 4 + 4;
85
86/// Block size for the writer's hash index. Power of two for cheap
87/// alignment math. Not part of the wire format — readers don't care.
88const BLOCK_SIZE: usize = 16;
89
90/// [`std::collections::HashMap`] pre-configured with `rustc_hash`'s
91/// `FxHasher` for `encode`'s block-hash index, whose keys are already
92/// the output of [`block_hash`] (FNV-1a over 16 bytes) — `std`'s
93/// default `SipHash`-1-3 hasher spends extra cycles on a keyed,
94/// hash-flooding-resistant design this index doesn't need *if* it's
95/// seeded per call (see [`random_seed`]'s docs for the "if").
96///
97/// Seeded via [`rustc_hash::FxSeededState`] rather than the crate's
98/// bare `FxBuildHasher`/`BuildHasherDefault<FxHasher>` (both always
99/// start from a fixed, compile-time state): `block_hash` is itself
100/// unkeyed, so an attacker who controls `base`'s bytes could otherwise
101/// solve for many distinct blocks whose `block_hash` outputs all land
102/// in the same table bucket under a known, fixed seed, degrading this
103/// index's build from O(n) to O(n²) — the exact hash-flooding attack
104/// `SipHash` exists to prevent. `encode` reseeds via [`random_seed`] on
105/// every call, denying an attacker the one thing that attack needs: a
106/// bucket mapping it can predict in advance.
107type FxIndexMap = std::collections::HashMap<u64, u32, rustc_hash::FxSeededState>;
108
109/// A fresh random seed for [`FxIndexMap`], drawn from `std`'s own
110/// randomized hasher — the same source `HashMap`'s default `SipHash`
111/// hasher seeds itself from — rather than pulling in `rustc-hash`'s
112/// optional `rand` feature (and its `rand` dependency) just for one
113/// `usize` per `encode()` call. Called once per `encode()` call, not
114/// once per lookup — cheap relative to building an index of up to
115/// thousands of entries.
116fn random_seed() -> usize {
117    use std::hash::{BuildHasher, Hasher};
118    // Any subset of these 64 random bits is still a valid, still-random
119    // seed, including the truncated one a 32-bit `usize` gets here — the
120    // cast doesn't need to be lossless.
121    #[allow(clippy::cast_possible_truncation)]
122    let seed = std::collections::hash_map::RandomState::new()
123        .build_hasher()
124        .finish() as usize;
125    seed
126}
127
128/// Multiplier applied to `stream.len()` when bounding the decoder's
129/// initial `Vec::with_capacity`. The worst-case expansion of a COPY op
130/// is 7 bytes of stream → `u16::MAX` output bytes (≈ 9363×), but in
131/// practice stream-sized * 256 dwarfs real deltas and still keeps the
132/// attacker's reach tiny: a 9-byte stream can only request ≤ 2304
133/// bytes of pre-allocation, independent of `base.len()` or the
134/// declared `result_len`. The final `result_len` self-consistency
135/// check still catches inflated payloads.
136pub(crate) const CAP_MULTIPLIER: usize = 256;
137
138/// Compute the decoder's initial capacity hint.
139///
140/// This is a small, explicitly attacker-resistant helper, exposed to
141/// the crate so that the regression test can pin down the bound
142/// without reaching into `decode`. The hint is the smaller of:
143///
144/// * the declared `result_len` (can't exceed declared output), and
145/// * `stream.len() * CAP_MULTIPLIER` (attacker bounded by on-wire size).
146///
147/// Crucially, `base.len()` does NOT appear here: letting the base size
148/// influence the cap would let an attacker pair a small delta stream with
149/// a large base to pre-reserve a huge output buffer (a ~1 GiB
150/// attacker-controlled allocation), so the cap is bounded only by the
151/// declared output length and the on-wire stream size.
152#[inline]
153pub(crate) fn compute_cap_hint(result_len: usize, _base_len: usize, stream_len: usize) -> usize {
154    result_len.min(stream_len.saturating_mul(CAP_MULTIPLIER))
155}
156
157/// Build a v1 delta stream that reconstructs `result` from `base`.
158///
159/// The writer is a rolling-polynomial-hash-on-16-byte-blocks scan (see
160/// `block_hash`/`roll_forward`). Any conformant writer is
161/// acceptable; this one is greedy. Output is always at least
162/// [`HEADER_LEN`] bytes.
163///
164/// # Errors
165///
166/// Returns [`MkitError::DeltaLengthOverflow`] if either `base.len()`
167/// or `result.len()` exceeds `u32::MAX`. SPEC-PACKFILE caps individual
168/// payloads under this bound, so this is a programmer error rather
169/// than a normal runtime condition — but silently saturating (the
170/// old behaviour) produced a stream that `decode()` rejected with a
171/// confusing "length mismatch" far from the actual source.
172///
173/// # Panics
174///
175/// Panics only on invariant violations in the writer's bookkeeping
176/// (insert-buffer length > 127, match length > `u16::MAX`); both are
177/// guarded above and unreachable for any valid input.
178pub fn encode(base: &[u8], result: &[u8]) -> Result<Vec<u8>, MkitError> {
179    check_length_bounds(base.len(), result.len())?;
180
181    let mut out = Vec::with_capacity(HEADER_LEN + result.len());
182    write_header(&mut out, base.len(), result.len());
183
184    // Build hash table: hash(block) -> first-seen position. We cap
185    // `base.len()` at `u32::MAX` for COPY offsets — bases over 4 GiB
186    // are out of scope for v1 (SPEC-PACKFILE caps individual payloads).
187    let num_blocks = base.len() / BLOCK_SIZE;
188    let mut index: FxIndexMap = FxIndexMap::with_capacity_and_hasher(
189        num_blocks,
190        rustc_hash::FxSeededState::with_seed(random_seed()),
191    );
192    for i in 0..num_blocks {
193        let pos = i * BLOCK_SIZE;
194        if let Ok(pos_u32) = u32::try_from(pos) {
195            let block = &base[pos..pos + BLOCK_SIZE];
196            let h = block_hash(block);
197            index.entry(h).or_insert(pos_u32);
198        } else {
199            break; // base too large for u32 offsets; fall back to all-INSERT
200        }
201    }
202
203    let mut insert_buf: Vec<u8> = Vec::with_capacity(MAX_INSERT_LEN);
204    let mut ti = 0usize;
205    // Rolling hash of `result[ti..ti + BLOCK_SIZE]`, `None` when it needs a
206    // fresh (non-incremental) `block_hash` — after a COPY jumps `ti`
207    // forward, or once fewer than `BLOCK_SIZE` bytes remain. Kept `Some`
208    // across consecutive miss steps so each one-byte advance rolls the
209    // hash in O(1) instead of recomputing it from scratch (see
210    // `roll_forward`'s doc comment for why this is safe).
211    let mut window_hash: Option<u64> = None;
212    while ti < result.len() {
213        let mut matched = false;
214        if ti + BLOCK_SIZE <= result.len() {
215            let target_block = &result[ti..ti + BLOCK_SIZE];
216            let h = *window_hash.get_or_insert_with(|| block_hash(target_block));
217            if let Some(&base_pos) = index.get(&h) {
218                let base_pos_usize = base_pos as usize;
219                if &base[base_pos_usize..base_pos_usize + BLOCK_SIZE] == target_block {
220                    flush_insert(&mut out, &mut insert_buf);
221
222                    // Greedy forward extension, capped at u16::MAX.
223                    let mut match_len = BLOCK_SIZE;
224                    while base_pos_usize + match_len < base.len()
225                        && ti + match_len < result.len()
226                        && base[base_pos_usize + match_len] == result[ti + match_len]
227                        && match_len < u16::MAX as usize
228                    {
229                        match_len += 1;
230                    }
231                    // match_len is bounded by u16::MAX above.
232                    emit_copy(
233                        &mut out,
234                        base_pos,
235                        u16::try_from(match_len).expect("<= u16::MAX"),
236                    );
237                    ti += match_len;
238                    // The window jumped past wherever it was rolled to —
239                    // recompute from scratch next time it's needed.
240                    window_hash = None;
241                    matched = true;
242                }
243            }
244        } else {
245            window_hash = None;
246        }
247        if !matched {
248            insert_buf.push(result[ti]);
249            // Roll the window forward by the one byte we just consumed,
250            // as long as a full window still fits ahead of the new `ti`
251            // and we had a hash to roll (the branch above already
252            // reset `window_hash` after a COPY's byte-comparison
253            // extension, so this only fires for a genuine byte-by-byte
254            // miss scan).
255            window_hash = window_hash.and_then(|h| {
256                (ti + BLOCK_SIZE < result.len())
257                    .then(|| roll_forward(h, result[ti], result[ti + BLOCK_SIZE]))
258            });
259            ti += 1;
260            if insert_buf.len() == MAX_INSERT_LEN {
261                flush_insert(&mut out, &mut insert_buf);
262            }
263        }
264    }
265    flush_insert(&mut out, &mut insert_buf);
266    Ok(out)
267}
268
269/// Validate that `base_len` and `result_len` both fit in the v1 wire
270/// format's `u32` cap. Extracted as a helper so tests can exercise
271/// the bound without actually allocating multi-gigabyte buffers.
272pub(crate) fn check_length_bounds(base_len: usize, result_len: usize) -> Result<(), MkitError> {
273    if u32::try_from(base_len).is_err() {
274        return Err(MkitError::DeltaLengthOverflow {
275            field: "base_len",
276            len: base_len,
277        });
278    }
279    if u32::try_from(result_len).is_err() {
280        return Err(MkitError::DeltaLengthOverflow {
281            field: "result_len",
282            len: result_len,
283        });
284    }
285    Ok(())
286}
287
288/// Apply a v1 delta stream to `base`, returning the reconstructed bytes.
289/// Verifies header version, base length, COPY bounds, and the final
290/// `result_len`.
291///
292/// # Errors
293///
294/// Returns [`MkitError::UnsupportedObjectVersion`] for stream version
295/// other than `0x01`, [`MkitError::UnexpectedEof`] for truncated input,
296/// and [`MkitError::DeltaCorrupt`] (carrying a [`DeltaCorruption`]) for
297/// any other corruption (zero opcode, COPY past base, length mismatch at
298/// end-of-stream, reserved bits set, etc.) — distinct from
299/// [`MkitError::TrailingData`], which is reserved for the unrelated
300/// "non-empty trailing bytes after a complete object" condition in
301/// `serialize.rs` (MKIT-13).
302///
303/// # Panics
304///
305/// Slice-to-fixed-array conversions in this function are guarded by
306/// the preceding bounds checks; the `expect` calls trip only if the
307/// compiler's slice-bounds elision is wrong.
308pub fn decode(base: &[u8], stream: &[u8]) -> Result<Vec<u8>, MkitError> {
309    decode_inner(base, stream, None)
310}
311
312/// Pack unpack charges and reserves the entire declared target fallibly
313/// before calling this path. The op checks prevent any subsequent growth.
314pub(crate) fn decode_preallocated(
315    base: &[u8],
316    stream: &[u8],
317    output: Vec<u8>,
318) -> Result<Vec<u8>, MkitError> {
319    decode_inner(base, stream, Some(output))
320}
321
322fn decode_inner(base: &[u8], stream: &[u8], output: Option<Vec<u8>>) -> Result<Vec<u8>, MkitError> {
323    if stream.len() < HEADER_LEN {
324        return Err(MkitError::UnexpectedEof);
325    }
326    if stream[0] != STREAM_VERSION {
327        return Err(MkitError::UnsupportedObjectVersion);
328    }
329    let base_len = u32::from_le_bytes(stream[1..5].try_into().expect("4 bytes")) as usize;
330    let result_len = u32::from_le_bytes(stream[5..9].try_into().expect("4 bytes")) as usize;
331    if base_len != base.len() {
332        // `base_len` was decoded from a `u32` field above, so this cast
333        // back is lossless.
334        #[allow(clippy::cast_possible_truncation)]
335        let declared = base_len as u32;
336        return Err(corrupt(DeltaCorruption::BaseLenMismatch {
337            declared,
338            actual: base.len(),
339        }));
340    }
341
342    // Bound the pre-allocation against attacker-controlled length fields.
343    // See [`compute_cap_hint`]: the hint is strictly a function of
344    // `stream.len()` (with `result_len` as an upper bound) — `base.len()`
345    // MUST NOT appear, because a 1 GiB base + 9-byte crafted stream
346    // otherwise triggers a ≈ 1 GiB allocation. The final `result_len`
347    // equality check below still enforces wire-level self-consistency.
348    let cap_hint = compute_cap_hint(result_len, base.len(), stream.len());
349    let mut out = output.unwrap_or_else(|| Vec::with_capacity(cap_hint));
350    let mut pos = HEADER_LEN;
351    while pos < stream.len() {
352        let op = stream[pos];
353        pos += 1;
354        if op & 0x80 != 0 {
355            // COPY. Reserved low seven bits MUST be zero in v1.
356            if op & 0x7F != 0 {
357                return Err(corrupt(DeltaCorruption::ReservedOpcodeBits(op)));
358            }
359            if pos + 6 > stream.len() {
360                return Err(MkitError::UnexpectedEof);
361            }
362            let offset_u32 = u32::from_le_bytes(stream[pos..pos + 4].try_into().expect("4 bytes"));
363            let offset = offset_u32 as usize;
364            pos += 4;
365            let length_u16 = u16::from_le_bytes(stream[pos..pos + 2].try_into().expect("2 bytes"));
366            let length = length_u16 as usize;
367            pos += 2;
368            if length == 0 {
369                return Err(corrupt(DeltaCorruption::ZeroLengthCopy));
370            }
371            let copy_past_base = || {
372                corrupt(DeltaCorruption::CopyPastBase {
373                    offset: offset_u32,
374                    length: length_u16,
375                    base_len: base.len(),
376                })
377            };
378            // Use checked math: an attacker-controlled offset could
379            // overflow `usize` on 32-bit targets when added to length, so
380            // reject the input rather than wrapping or clamping.
381            let end = offset.checked_add(length).ok_or_else(copy_past_base)?;
382            if end > base.len() {
383                return Err(copy_past_base());
384            }
385            // Don't overshoot the declared result_len.
386            if out.len().checked_add(length).is_none_or(|v| v > result_len) {
387                return Err(corrupt(DeltaCorruption::ResultLenOverrun {
388                    emitted: out.len(),
389                    requested: length,
390                    result_len,
391                }));
392            }
393            out.extend_from_slice(&base[offset..end]);
394        } else if op > 0 {
395            // INSERT. opcode IS the literal length (1..=127).
396            let length = op as usize;
397            if pos + length > stream.len() {
398                return Err(MkitError::UnexpectedEof);
399            }
400            if out.len().checked_add(length).is_none_or(|v| v > result_len) {
401                return Err(corrupt(DeltaCorruption::ResultLenOverrun {
402                    emitted: out.len(),
403                    requested: length,
404                    result_len,
405                }));
406            }
407            out.extend_from_slice(&stream[pos..pos + length]);
408            pos += length;
409        } else {
410            // 0x00 reserved.
411            return Err(corrupt(DeltaCorruption::ZeroOpcode));
412        }
413    }
414    if out.len() != result_len {
415        return Err(corrupt(DeltaCorruption::ResultLenUnderrun {
416            expected: result_len,
417            actual: out.len(),
418        }));
419    }
420    Ok(out)
421}
422
423// --- helpers ---
424
425fn write_header(out: &mut Vec<u8>, base_len: usize, result_len: usize) {
426    // `check_length_bounds` has already been called by `encode`, so
427    // both fit in u32. The `expect()`s are invariant-preserving
428    // rather than user-facing: reaching them means the caller
429    // bypassed `encode`.
430    let bl: u32 = u32::try_from(base_len).expect("base_len <= u32::MAX (checked)");
431    let rl: u32 = u32::try_from(result_len).expect("result_len <= u32::MAX (checked)");
432    out.push(STREAM_VERSION);
433    out.extend_from_slice(&bl.to_le_bytes());
434    out.extend_from_slice(&rl.to_le_bytes());
435}
436
437fn emit_copy(out: &mut Vec<u8>, offset: u32, length: u16) {
438    out.push(OP_COPY);
439    out.extend_from_slice(&offset.to_le_bytes());
440    out.extend_from_slice(&length.to_le_bytes());
441}
442
443fn flush_insert(out: &mut Vec<u8>, buf: &mut Vec<u8>) {
444    if buf.is_empty() {
445        return;
446    }
447    debug_assert!(buf.len() <= MAX_INSERT_LEN);
448    out.push(u8::try_from(buf.len()).expect("<= 127"));
449    out.extend_from_slice(buf);
450    buf.clear();
451}
452
453/// Multiplier for `block_hash`'s polynomial hash. [`roll_forward`] slides
454/// the window by algebraic cancellation (subtracting the outgoing byte's
455/// `ROLL_M_POW_BLOCK`-scaled contribution back out), an identity that
456/// holds for any `ROLL_M` value under wrapping `u64` arithmetic — no
457/// modular inverse of `ROLL_M` is needed. `encode` only ever trusts a
458/// `block_hash` hit after re-checking the actual bytes (`base[..] ==
459/// target_block`), so this constant's only real job is spreading
460/// distinct blocks across hash-table buckets well; this is the
461/// fractional part of the golden ratio scaled to 64 bits, a standard
462/// avalanche-friendly constant (as used in e.g. Fibonacci hashing).
463const ROLL_M: u64 = 0x9E37_79B9_7F4A_7C15;
464
465/// `ROLL_M` raised to `BLOCK_SIZE`, precomputed at compile time. This is
466/// the coefficient [`roll_forward`] needs to cancel out a window's
467/// outgoing byte (see its derivation there).
468const ROLL_M_POW_BLOCK: u64 = {
469    let mut r: u64 = 1;
470    let mut i = 0;
471    while i < BLOCK_SIZE {
472        r = r.wrapping_mul(ROLL_M);
473        i += 1;
474    }
475    r
476};
477
478/// Polynomial hash of a `BLOCK_SIZE`-byte window: `block[0] *
479/// ROLL_M^(BLOCK_SIZE-1) + block[1] * ROLL_M^(BLOCK_SIZE-2) + ... +
480/// block[BLOCK_SIZE-1] * ROLL_M^0`, wrapping in `u64`. `encode` calls
481/// this directly (O(`BLOCK_SIZE`)) once per non-overlapping block while
482/// building the base index, and once per COPY match/resync while
483/// scanning `result` — everywhere else in that scan, [`roll_forward`]
484/// slides an already-computed hash forward in O(1) instead.
485fn block_hash(block: &[u8]) -> u64 {
486    let mut h: u64 = 0;
487    for &b in block {
488        h = h.wrapping_mul(ROLL_M).wrapping_add(u64::from(b));
489    }
490    h
491}
492
493/// Slide a `block_hash` window forward by one byte: given the hash of
494/// `result[ti..ti+BLOCK_SIZE]`, `old = result[ti]` (leaving the window)
495/// and `new = result[ti+BLOCK_SIZE]` (entering it), returns the hash of
496/// `result[ti+1..ti+1+BLOCK_SIZE]` — without rescanning the other
497/// `BLOCK_SIZE-1` bytes. This is what turns `encode`'s byte-by-byte miss
498/// scan from O(n * `BLOCK_SIZE`) into O(n): a plain rescan recomputes the
499/// full window on every failed match, but a full window's hash only
500/// needs to change by the one byte that left and the one that arrived.
501///
502/// Derivation: writing `h = Σ block[i] * ROLL_M^(BLOCK_SIZE-1-i)`,
503/// multiplying by `ROLL_M` shifts every term's exponent up by one and
504/// introduces `old`'s contribution at the new top exponent
505/// (`ROLL_M^BLOCK_SIZE`, i.e. `ROLL_M_POW_BLOCK`) while leaving a
506/// dangling zero-exponent slot for `new`:
507///
508/// ```text
509/// h * ROLL_M = old * ROLL_M_POW_BLOCK + Σ_{i=1..BLOCK_SIZE-1} block[i] * ROLL_M^(BLOCK_SIZE-i)
510/// h'         =                          Σ_{i=1..BLOCK_SIZE-1} block[i] * ROLL_M^(BLOCK_SIZE-i)  + new
511///           = h * ROLL_M - old * ROLL_M_POW_BLOCK + new
512/// ```
513///
514/// All arithmetic wraps, matching `block_hash`; the derivation above is
515/// exact algebraic cancellation, not a modular inverse, so it holds for
516/// any `ROLL_M` (see its doc comment) under wrapping `u64` arithmetic.
517fn roll_forward(h: u64, old: u8, new: u8) -> u64 {
518    h.wrapping_mul(ROLL_M)
519        .wrapping_sub(u64::from(old).wrapping_mul(ROLL_M_POW_BLOCK))
520        .wrapping_add(u64::from(new))
521}
522
523// =========================================================================
524// Tests
525// =========================================================================
526
527#[cfg(test)]
528mod tests {
529    use super::*;
530
531    fn header(base_len: u32, result_len: u32) -> [u8; HEADER_LEN] {
532        let mut h = [0u8; HEADER_LEN];
533        h[0] = STREAM_VERSION;
534        h[1..5].copy_from_slice(&base_len.to_le_bytes());
535        h[5..9].copy_from_slice(&result_len.to_le_bytes());
536        h
537    }
538
539    /// `random_seed` and `FxSeededState` are the two pieces of this
540    /// module's own contribution to `FxIndexMap` — `FxHasher`'s mixing
541    /// quality is `rustc_hash`'s own tested contract, not this module's
542    /// to re-verify. What this module must get right: two seeds drawn
543    /// from `random_seed()` actually differ (or `encode`'s index would
544    /// be no better than a fixed-seed `FxHasher`, exactly the
545    /// hash-flooding gap `FxIndexMap`'s docs describe), and
546    /// `FxSeededState` wires a seed through consistently enough for a
547    /// `HashMap` to find keys it just inserted.
548    #[test]
549    fn random_seed_differs_across_calls_and_seeds_a_usable_map() {
550        use std::hash::BuildHasher;
551
552        fn hash_u64_with(state: &rustc_hash::FxSeededState, i: u64) -> u64 {
553            state.hash_one(i)
554        }
555
556        // Astronomically likely to differ by chance alone (1 in 2^64 not
557        // to), so a single inequality here is a meaningful regression
558        // signal for "reseeding isn't happening", not a flaky test.
559        let seed_a = random_seed();
560        let seed_b = random_seed();
561        assert_ne!(
562            seed_a, seed_b,
563            "random_seed() returned the same value twice in a row"
564        );
565
566        let a = rustc_hash::FxSeededState::with_seed(seed_a);
567        let b = rustc_hash::FxSeededState::with_seed(seed_b);
568        assert_ne!(
569            hash_u64_with(&a, 42),
570            hash_u64_with(&b, 42),
571            "two different seeds produced the same hash for the same key"
572        );
573        // Within one seed (i.e. one `encode()` call's index), hashing
574        // must still be internally consistent.
575        assert_eq!(hash_u64_with(&a, 42), hash_u64_with(&a, 42));
576    }
577
578    #[test]
579    fn identity_roundtrip() {
580        let data = b"0123456789abcdef".repeat(4); // 64 bytes
581        let stream = encode(&data, &data).unwrap();
582        let restored = decode(&data, &stream).unwrap();
583        assert_eq!(restored, data);
584    }
585
586    /// `roll_forward` must agree with a fresh `block_hash` of the slid
587    /// window at every step, for every starting offset — this is the
588    /// correctness property `encode`'s miss-scan optimization depends
589    /// on. Covers pseudo-random bytes (no accidental periodicity that
590    /// could mask a rolling-hash bug) sliding across a buffer several
591    /// times `BLOCK_SIZE` long.
592    #[test]
593    fn roll_forward_matches_direct_block_hash() {
594        let data: Vec<u8> = (0..256u32)
595            .map(|i| i.wrapping_mul(2_654_435_761).to_le_bytes()[0])
596            .collect();
597        assert!(data.len() > BLOCK_SIZE * 4);
598
599        let mut h = block_hash(&data[0..BLOCK_SIZE]);
600        for start in 0..data.len() - BLOCK_SIZE - 1 {
601            let direct = block_hash(&data[start + 1..start + 1 + BLOCK_SIZE]);
602            h = roll_forward(h, data[start], data[start + BLOCK_SIZE]);
603            assert_eq!(
604                h, direct,
605                "rolled hash diverged from direct block_hash at start={start}"
606            );
607        }
608    }
609
610    #[test]
611    fn pure_insert_roundtrip() {
612        let base = b"aaa";
613        let target = b"zzz";
614        let stream = encode(base, target).unwrap();
615        // After the 9-byte header, the very next byte is the INSERT length.
616        assert_eq!(stream[HEADER_LEN] & 0x80, 0);
617        assert_eq!(stream[HEADER_LEN], 3);
618        let restored = decode(base, &stream).unwrap();
619        assert_eq!(restored, target);
620    }
621
622    #[test]
623    fn pure_copy_full_base() {
624        let base: Vec<u8> = (0..16u8).cycle().take(128).collect();
625        let target = &base[..64];
626        // Hand-build a stream that is exactly one COPY(0, 64).
627        let mut stream = header(
628            u32::try_from(base.len()).unwrap(),
629            u32::try_from(target.len()).unwrap(),
630        )
631        .to_vec();
632        stream.push(OP_COPY);
633        stream.extend_from_slice(&0u32.to_le_bytes());
634        stream.extend_from_slice(&64u16.to_le_bytes());
635        assert_eq!(stream.len(), HEADER_LEN + 7);
636        let restored = decode(&base, &stream).unwrap();
637        assert_eq!(restored, target);
638    }
639
640    #[test]
641    fn near_duplicate_yields_smaller_delta() {
642        let v1 = include_str!("delta.rs"); // any sizable text
643        let mut v2 = String::from(v1);
644        v2.push_str("\n// trailing edit\n");
645        let stream = encode(v1.as_bytes(), v2.as_bytes()).unwrap();
646        let restored = decode(v1.as_bytes(), &stream).unwrap();
647        assert_eq!(restored, v2.as_bytes());
648        assert!(stream.len() < v2.len(), "delta should be smaller than v2");
649    }
650
651    #[test]
652    fn rejects_zero_opcode() {
653        let mut stream = header(0, 0).to_vec();
654        stream.push(0x00);
655        let err = decode(&[], &stream).unwrap_err();
656        assert!(matches!(
657            err,
658            MkitError::DeltaCorrupt(DeltaCorruption::ZeroOpcode)
659        ));
660    }
661
662    #[test]
663    fn rejects_unknown_version() {
664        let mut bytes = header(0, 0);
665        bytes[0] = 0x02;
666        let err = decode(&[], &bytes).unwrap_err();
667        assert!(matches!(err, MkitError::UnsupportedObjectVersion));
668    }
669
670    #[test]
671    fn rejects_truncated_header() {
672        let bytes = [0x01u8, 0x00, 0x00];
673        let err = decode(&[], &bytes).unwrap_err();
674        assert!(matches!(err, MkitError::UnexpectedEof));
675    }
676
677    #[test]
678    fn rejects_truncated_copy() {
679        let mut stream = header(16, 16).to_vec();
680        stream.push(OP_COPY);
681        stream.extend_from_slice(&0u32.to_le_bytes()); // missing 2-byte length
682        let err = decode(&[0u8; 16], &stream).unwrap_err();
683        assert!(matches!(err, MkitError::UnexpectedEof));
684    }
685
686    #[test]
687    fn rejects_truncated_insert() {
688        let mut stream = header(0, 10).to_vec();
689        stream.push(10); // claim 10 literal bytes
690        stream.extend_from_slice(b"abc"); // only 3 supplied
691        let err = decode(&[], &stream).unwrap_err();
692        assert!(matches!(err, MkitError::UnexpectedEof));
693    }
694
695    #[test]
696    fn rejects_copy_past_base_end() {
697        let base = b"short"; // 5 bytes
698        let mut stream = header(u32::try_from(base.len()).unwrap(), 100).to_vec();
699        stream.push(OP_COPY);
700        stream.extend_from_slice(&0u32.to_le_bytes());
701        stream.extend_from_slice(&100u16.to_le_bytes());
702        let err = decode(base, &stream).unwrap_err();
703        assert!(matches!(
704            err,
705            MkitError::DeltaCorrupt(DeltaCorruption::CopyPastBase { .. })
706        ));
707    }
708
709    #[test]
710    fn rejects_copy_with_zero_length() {
711        let base = [0u8; 16];
712        let mut stream = header(16, 16).to_vec();
713        stream.push(OP_COPY);
714        stream.extend_from_slice(&0u32.to_le_bytes());
715        stream.extend_from_slice(&0u16.to_le_bytes());
716        let err = decode(&base, &stream).unwrap_err();
717        assert!(matches!(
718            err,
719            MkitError::DeltaCorrupt(DeltaCorruption::ZeroLengthCopy)
720        ));
721    }
722
723    #[test]
724    fn rejects_base_len_mismatch() {
725        let stream = header(16, 0).to_vec();
726        let err = decode(&[0u8; 8], &stream).unwrap_err();
727        assert!(matches!(
728            err,
729            MkitError::DeltaCorrupt(DeltaCorruption::BaseLenMismatch {
730                declared: 16,
731                actual: 8
732            })
733        ));
734    }
735
736    #[test]
737    fn rejects_result_len_mismatch_at_end() {
738        // INSERTs sum to 5 but header says result_len = 3.
739        let mut stream = header(0, 3).to_vec();
740        stream.push(5);
741        stream.extend_from_slice(b"hello");
742        let err = decode(&[], &stream).unwrap_err();
743        assert!(matches!(
744            err,
745            MkitError::DeltaCorrupt(DeltaCorruption::ResultLenOverrun { .. })
746        ));
747    }
748
749    #[test]
750    fn rejects_huge_result_len_without_preallocating() {
751        // Regression: a 9-byte header claiming result_len = u32::MAX MUST NOT
752        // trigger a 4 GiB `Vec::with_capacity`. The pre-allocation is now
753        // capped against the stream+base size. The decoder still returns an
754        // error (`ResultLenUnderrun`) because no ops follow — but the point
755        // is that it does so without first reserving 4 GiB of virtual memory.
756        let stream = header(0, u32::MAX);
757        let err = decode(&[], &stream).unwrap_err();
758        assert!(matches!(
759            err,
760            MkitError::DeltaCorrupt(DeltaCorruption::ResultLenUnderrun { .. })
761        ));
762    }
763
764    #[test]
765    fn rejects_copy_with_reserved_low_bits() {
766        let base = [0u8; 16];
767        let mut stream = header(16, 4).to_vec();
768        stream.push(OP_COPY | 0x01); // reserved bit set
769        stream.extend_from_slice(&0u32.to_le_bytes());
770        stream.extend_from_slice(&4u16.to_le_bytes());
771        let err = decode(&base, &stream).unwrap_err();
772        assert!(matches!(
773            err,
774            MkitError::DeltaCorrupt(DeltaCorruption::ReservedOpcodeBits(0x81))
775        ));
776    }
777
778    #[test]
779    fn empty_base_pure_insert() {
780        let target = b"all new content here!";
781        let stream = encode(b"", target).unwrap();
782        let restored = decode(b"", &stream).unwrap();
783        assert_eq!(restored, target);
784    }
785
786    #[test]
787    fn cap_hint_does_not_scale_with_base_len() {
788        // G5 regression: the decoder's pre-allocation must be bounded by
789        // `stream.len()`, not by `base.len()`. Previously a 9-byte stream
790        // with a 1 GiB base could drive `Vec::with_capacity` to ~1 GiB.
791        //
792        // Assert: for a huge base + tiny stream, cap_hint is tiny.
793        let huge_base = 1usize << 30; // 1 GiB
794        let tiny_stream = 9usize; // just the header
795        let declared_result = u32::MAX as usize;
796        let cap = super::compute_cap_hint(declared_result, huge_base, tiny_stream);
797        assert!(
798            cap <= tiny_stream.saturating_mul(CAP_MULTIPLIER),
799            "cap_hint {cap} must be bounded by stream.len() * CAP_MULTIPLIER, \
800             not by base.len()",
801        );
802        assert!(
803            cap < 1024 * 1024,
804            "cap_hint {cap} must stay well below 1 MiB for a 9-byte stream",
805        );
806    }
807
808    /// MKIT-13: structural delta corruption must be reported as
809    /// [`MkitError::DeltaCorrupt`], not the generic [`MkitError::TrailingData`]
810    /// (which SPEC-DELTA §10 reserves for the genuine trailing-bytes-after-
811    /// a-complete-object case in `serialize.rs`). This collects one crafted
812    /// stream per corruption kind `decode()` rejects; every one of them must
813    /// come back as something other than `TrailingData`.
814    #[test]
815    fn delta_corruption_is_not_reported_as_trailing_data() {
816        // base_len mismatch.
817        let base_len_mismatch = header(16, 0).to_vec();
818        // reserved COPY opcode bits set.
819        let mut reserved_bits = header(16, 4).to_vec();
820        reserved_bits.push(OP_COPY | 0x01);
821        reserved_bits.extend_from_slice(&0u32.to_le_bytes());
822        reserved_bits.extend_from_slice(&4u16.to_le_bytes());
823        // zero opcode.
824        let mut zero_opcode = header(0, 0).to_vec();
825        zero_opcode.push(0x00);
826        // zero-length COPY.
827        let mut zero_length_copy = header(16, 16).to_vec();
828        zero_length_copy.push(OP_COPY);
829        zero_length_copy.extend_from_slice(&0u32.to_le_bytes());
830        zero_length_copy.extend_from_slice(&0u16.to_le_bytes());
831        // COPY past base end.
832        let mut copy_past_base = header(5, 100).to_vec();
833        copy_past_base.push(OP_COPY);
834        copy_past_base.extend_from_slice(&0u32.to_le_bytes());
835        copy_past_base.extend_from_slice(&100u16.to_le_bytes());
836        // result_len overrun via a mid-stream COPY (out.len() would exceed
837        // result_len even though the COPY itself stays within base bounds).
838        let mut copy_result_overrun = header(16, 4).to_vec();
839        copy_result_overrun.push(OP_COPY);
840        copy_result_overrun.extend_from_slice(&0u32.to_le_bytes());
841        copy_result_overrun.extend_from_slice(&8u16.to_le_bytes());
842        // result_len mismatch at end-of-stream (INSERT sums to less than
843        // declared result_len).
844        let mut result_len_underrun = header(0, 3).to_vec();
845        result_len_underrun.push(5);
846        result_len_underrun.extend_from_slice(b"hello");
847
848        let cases: &[(&str, Vec<u8>, &[u8])] = &[
849            ("base_len_mismatch", base_len_mismatch, &[0u8; 8]),
850            ("reserved_bits", reserved_bits, &[0u8; 16]),
851            ("zero_opcode", zero_opcode, &[]),
852            ("zero_length_copy", zero_length_copy, &[0u8; 16]),
853            ("copy_past_base", copy_past_base, b"short"),
854            ("copy_result_overrun", copy_result_overrun, &[0u8; 16]),
855            ("result_len_underrun", result_len_underrun, &[]),
856        ];
857        for (name, stream, base) in cases {
858            let err = decode(base, stream).expect_err(&format!("{name} must be rejected"));
859            assert!(
860                !matches!(err, MkitError::TrailingData),
861                "{name} must not be reported as TrailingData, got {err:?}"
862            );
863        }
864
865        // Well-formed streams are unaffected.
866        let data = b"0123456789abcdef".repeat(4);
867        let stream = encode(&data, &data).unwrap();
868        assert_eq!(decode(&data, &stream).unwrap(), data);
869    }
870
871    /// `encode()` used to saturate `base_len`/`result_len` to
872    /// `u32::MAX` for inputs over 4 GiB, silently producing a stream
873    /// that `decode()` would reject with a confusing "length mismatch".
874    /// Now `check_length_bounds` errors out explicitly with
875    /// `DeltaLengthOverflow` so misuse surfaces at the call site.
876    #[test]
877    fn check_length_bounds_rejects_over_u32() {
878        // base_len above u32::MAX.
879        let over = (u32::MAX as usize).saturating_add(1);
880        assert!(matches!(
881            check_length_bounds(over, 0),
882            Err(MkitError::DeltaLengthOverflow { .. })
883        ));
884        // result_len above u32::MAX.
885        assert!(matches!(
886            check_length_bounds(0, over),
887            Err(MkitError::DeltaLengthOverflow { .. })
888        ));
889        // Exactly at u32::MAX is fine.
890        assert!(check_length_bounds(u32::MAX as usize, u32::MAX as usize).is_ok());
891        // Small is fine.
892        assert!(check_length_bounds(1, 1).is_ok());
893    }
894
895    // `encode`'s miss-scan now rolls its window hash forward instead of
896    // recomputing it from scratch (see `roll_forward`) — a change that
897    // only ever *should* affect performance, never which bytes come out
898    // the other end of `decode`. Property-test the round trip across
899    // arbitrary `(base, result)` pairs, including base/result lengths
900    // that straddle `BLOCK_SIZE`'s alignment, to catch any off-by-one
901    // in the rolled window's bookkeeping that the hand-picked examples
902    // above might miss.
903    proptest::proptest! {
904        #[test]
905        fn proptest_encode_decode_roundtrip(
906            base in proptest::collection::vec(proptest::num::u8::ANY, 0..4096),
907            result in proptest::collection::vec(proptest::num::u8::ANY, 0..4096),
908        ) {
909            let stream = encode(&base, &result).unwrap();
910            let restored = decode(&base, &stream).unwrap();
911            proptest::prop_assert_eq!(restored, result);
912        }
913
914        /// A `result` that is a near-duplicate of `base` (base plus one
915        /// small edit) is the realistic push-diff shape and the one most
916        /// likely to exercise a rolled-vs-fresh hash mismatch at a COPY
917        /// match's resync boundary.
918        #[test]
919        fn proptest_encode_decode_roundtrip_near_duplicate(
920            base in proptest::collection::vec(proptest::num::u8::ANY, 1..4096),
921            edit_pos_permille in 0u64..1000,
922            patch in proptest::collection::vec(proptest::num::u8::ANY, 0..64),
923        ) {
924            let mut result = base.clone();
925            let edit_pos = (base.len() as u64 * edit_pos_permille / 1000) as usize;
926            result.splice(edit_pos..edit_pos, patch);
927
928            let stream = encode(&base, &result).unwrap();
929            let restored = decode(&base, &stream).unwrap();
930            proptest::prop_assert_eq!(restored, result);
931        }
932    }
933}
934
935/// Kani proof harnesses (`cargo kani -p mkit-core --no-default-features
936/// -Z stubbing --harness delta_`; with the default `pack-zstd` feature's
937/// C `zstd` dependency linked in, CBMC ran out of memory on most
938/// harnesses of this crate).
939/// Bounds are stated per harness; `kani::cover!` sites show every
940/// asserted property has a reachable, non-vacuous `Ok` path.
941#[cfg(kani)]
942mod kani_proofs {
943    use super::*;
944
945    /// Stream bound: header (9) + one COPY (7) + one 1-byte INSERT (2)
946    /// + 2 spare bytes, so every opcode kind and every error arm is reachable.
947    const MAX_STREAM: usize = 20;
948    /// Base bound.
949    const MAX_BASE: usize = 4;
950    /// Every instruction consumes >= 2 stream bytes (INSERT) or ends the
951    /// loop, so `decode`'s loop runs <= (S - 9) / 2 + 1 times; +1 for the
952    /// exit test. A tight unwind matters: CBMC cost grows sharply with
953    /// every surplus (infeasible) unrolling.
954    const fn unwind_for(s: usize) -> usize {
955        (s - HEADER_LEN) / 2 + 2
956    }
957    // Keep the literal `#[kani::unwind(..)]` values below in sync.
958    const _: [(); 7] = [(); unwind_for(MAX_STREAM)];
959    const _: [(); 5] = [(); unwind_for(16)];
960
961    /// Coarse outcome class shared by `decode` and the spec model.
962    #[derive(Debug, PartialEq, Eq)]
963    enum Class {
964        Eof,
965        Version,
966        Corrupt,
967    }
968
969    fn class_of(e: &MkitError) -> Class {
970        match e {
971            MkitError::UnexpectedEof => Class::Eof,
972            MkitError::UnsupportedObjectVersion => Class::Version,
973            MkitError::DeltaCorrupt(_) => Class::Corrupt,
974            _ => panic!("decode returned an error kind outside SPEC-DELTA §2/§4"),
975        }
976    }
977
978    /// Direct transcription of the SPEC-DELTA §4 reference pseudo-code
979    /// (streams shorter than the §2 header are truncation → Eof).
980    fn spec_apply(base: &[u8], s: &[u8]) -> Result<Vec<u8>, Class> {
981        if s.len() < 9 {
982            return Err(Class::Eof);
983        }
984        if s[0] != 0x01 {
985            return Err(Class::Version);
986        }
987        let le32 = |p: usize| u32::from_le_bytes([s[p], s[p + 1], s[p + 2], s[p + 3]]) as u64;
988        if base.len() as u64 != le32(1) {
989            return Err(Class::Corrupt);
990        }
991        let result_len = le32(5);
992        let mut out = Vec::new();
993        let mut pos = 9usize;
994        while pos < s.len() {
995            let op = s[pos];
996            pos += 1;
997            if op & 0x80 != 0 {
998                if op & 0x7F != 0 {
999                    return Err(Class::Corrupt);
1000                }
1001                if pos + 6 > s.len() {
1002                    return Err(Class::Eof);
1003                }
1004                let offset = le32(pos);
1005                let length = u64::from(u16::from_le_bytes([s[pos + 4], s[pos + 5]]));
1006                pos += 6;
1007                if length == 0
1008                    || offset + length > base.len() as u64
1009                    || out.len() as u64 + length > result_len
1010                {
1011                    return Err(Class::Corrupt);
1012                }
1013                out.extend_from_slice(&base[offset as usize..(offset + length) as usize]);
1014            } else if op > 0 {
1015                let n = op as usize;
1016                if pos + n > s.len() {
1017                    return Err(Class::Eof);
1018                }
1019                if out.len() as u64 + n as u64 > result_len {
1020                    return Err(Class::Corrupt);
1021                }
1022                out.extend_from_slice(&s[pos..pos + n]);
1023                pos += n;
1024            } else {
1025                return Err(Class::Corrupt);
1026            }
1027        }
1028        if out.len() as u64 != result_len {
1029            return Err(Class::Corrupt);
1030        }
1031        Ok(out)
1032    }
1033
1034    /// Symbolic `(base, stream)` with `base.len() <= B`, `stream.len() <= S`.
1035    fn any_input<const B: usize, const S: usize>() -> ([u8; B], usize, [u8; S], usize) {
1036        (
1037            kani::any(),
1038            kani::any_where(|&n| n <= B),
1039            kani::any(),
1040            kani::any_where(|&n| n <= S),
1041        )
1042    }
1043
1044    /// No panic / overflow / OOB for every `base` (<= 4 B) and `stream`
1045    /// (<= 20 B); on `Ok`, output length equals the header `result_len`
1046    /// (SPEC-DELTA §2).
1047    #[kani::proof]
1048    #[kani::unwind(7)] // unwind_for(MAX_STREAM)
1049    fn delta_decode_no_panic() {
1050        let (b, bl, s, sl) = any_input::<MAX_BASE, MAX_STREAM>();
1051        let stream = &s[..sl];
1052        let got = decode(&b[..bl], stream);
1053        if let Ok(out) = &got {
1054            let declared = u32::from_le_bytes([stream[5], stream[6], stream[7], stream[8]]);
1055            assert_eq!(out.len(), declared as usize);
1056        }
1057        // Non-vacuity: success through each opcode kind is reachable.
1058        kani::cover!(got.is_ok() && sl > HEADER_LEN, "ok_nonempty");
1059        kani::cover!(
1060            got.is_ok() && stream.get(HEADER_LEN) == Some(&OP_COPY),
1061            "ok_copy"
1062        );
1063        kani::cover!(
1064            matches!(
1065                got,
1066                Err(MkitError::DeltaCorrupt(
1067                    DeltaCorruption::ResultLenOverrun { .. }
1068                ))
1069            ),
1070            "overrun"
1071        );
1072    }
1073
1074    /// Checks one stream length; returns the first opcode on `Ok`.
1075    fn spec_at<const S: usize>() -> Option<u8> {
1076        let b: [u8; 3] = kani::any();
1077        let bl: usize = kani::any_where(|&n| n <= 3);
1078        let s: [u8; S] = kani::any();
1079        let base = &b[..bl];
1080        let got = decode(base, &s);
1081        match (&got, &spec_apply(base, &s)) {
1082            (Ok(out), Ok(expected)) => {
1083                assert_eq!(out, expected);
1084            }
1085            (Err(e), Err(c)) => {
1086                assert_eq!(&class_of(e), c);
1087            }
1088            _ => panic!("decode and SPEC-DELTA §4 model disagree on accept/reject"),
1089        }
1090        got.ok().and_then(|_| s.get(HEADER_LEN).copied())
1091    }
1092
1093    /// Spec conformance (`base` <= 3 B): for every stream of 8 or 9
1094    /// bytes (one short of the §2 header, and the bare header) the
1095    /// outcome (bytes, or error class) agrees with the SPEC-DELTA §4
1096    /// reference algorithm. Two stream lengths per harness: 0..=16 or
1097    /// 0..=11 in one harness ran out of memory, so 0..=7 (truncation,
1098    /// like 8) and 12..=15 (truncated COPY operands) are left to
1099    /// `delta_decode_no_panic` and the fuzz target.
1100    #[kani::proof]
1101    #[kani::unwind(7)] // max(unwind_for(16), 6-byte output memcmp + 1)
1102    fn delta_spec_header() {
1103        let _ = spec_at::<8>();
1104        let _ = spec_at::<9>();
1105    }
1106
1107    /// As above for 10 and 11 bytes: one opcode byte, then a 1-byte
1108    /// INSERT.
1109    #[kani::proof]
1110    #[kani::unwind(7)]
1111    fn delta_spec_insert() {
1112        let _ = spec_at::<10>();
1113        kani::cover!(spec_at::<11>() == Some(1), "ok_insert");
1114    }
1115
1116    /// As above for a 16-byte stream: header + one COPY instruction.
1117    #[kani::proof]
1118    #[kani::unwind(7)]
1119    fn delta_spec_copy() {
1120        kani::cover!(spec_at::<16>() == Some(OP_COPY), "ok_copy");
1121    }
1122
1123    /// Canary: the checker must falsify a wrong length law (output one
1124    /// byte longer than declared). Proves the `Ok` length assertion
1125    /// above is not trivially satisfied.
1126    #[kani::proof]
1127    #[kani::unwind(7)] // unwind_for(MAX_STREAM)
1128    #[kani::should_panic]
1129    fn delta_decode_canary_wrong_length() {
1130        let stream_buf: [u8; MAX_STREAM] = kani::any();
1131        let stream_len: usize = kani::any_where(|&n| n <= MAX_STREAM);
1132        let stream = &stream_buf[..stream_len];
1133        if let Ok(out) = decode(&[], stream) {
1134            let declared = u32::from_le_bytes([stream[5], stream[6], stream[7], stream[8]]);
1135            assert_eq!(out.len(), declared as usize + 1);
1136        }
1137    }
1138
1139    /// Fixed seed for the writer's block index: the seed only chooses
1140    /// hash-table buckets, never the emitted stream, and `std`'s
1141    /// `RandomState` is expensive to model.
1142    fn fixed_seed() -> usize {
1143        0
1144    }
1145
1146    /// One round-trip at concrete lengths `B`, `R` (concrete lengths let
1147    /// CBMC constant-fold the writer's block-index loop away).
1148    fn roundtrip_at<const B: usize, const R: usize>() {
1149        let b: [u8; B] = kani::any();
1150        let r: [u8; R] = kani::any();
1151        let stream = encode(&b, &r).expect("small lengths fit u32");
1152        assert_eq!(decode(&b, &stream).expect("own stream decodes"), &r);
1153    }
1154
1155    /// `decode(base, encode(base, result)) == result` for every
1156    /// `base`, `result` of <= 3 bytes (each length pair checked at its
1157    /// concrete size; below `BLOCK_SIZE`, so the writer emits header +
1158    /// INSERTs only — COPY emission is covered by the proptest
1159    /// round-trip in `tests`).
1160    #[kani::proof]
1161    #[kani::stub(random_seed, fixed_seed)]
1162    #[kani::unwind(5)]
1163    fn delta_encode_decode_roundtrip() {
1164        macro_rules! each_r {
1165            ($b:literal) => {
1166                roundtrip_at::<$b, 0>();
1167                roundtrip_at::<$b, 1>();
1168                roundtrip_at::<$b, 2>();
1169                roundtrip_at::<$b, 3>();
1170            };
1171        }
1172        each_r!(0);
1173        each_r!(1);
1174        each_r!(2);
1175        each_r!(3);
1176    }
1177}