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}