1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
//! CRC-32C integrity primitive for the OXGDB delta-log and superblock.
//!
//! The on-disk format binds every delta-log record and the superblock to a
//! CRC-32C (Castagnoli polynomial `0x1EDC6F41`) checksum so recovery can reject
//! torn or corrupted bytes deterministically. This module is the single source
//! of the checksum so the writer and reader agree on the exact algorithm. It
//! wraps the hardware-accelerated [`crc32c`] crate, which selects an
//! SSE4.2/ARMv8 implementation at runtime and falls back to a software table.
//!
//! # Performance
//!
//! `perf: unspecified`; the wrapper itself is `O(1)` and delegates an `O(n)`
//! scan to [`crc32c::crc32c`].
/// Computes the CRC-32C (Castagnoli) checksum over `bytes`.
///
/// The result is the value the OXGDB format stores little-endian in a record's
/// `crc32c` field. It is byte-order independent (the checksum is over the byte
/// sequence, not over multi-byte words), so it is stable across architectures.
///
/// # Performance
///
/// This function is `O(n)` in `bytes.len()`.
//
// kani-skip: delegates to the external `crc32c` crate whose runtime CPU-feature
// dispatch and unbounded scan are outside the model checker's reach; the known
// check vector, determinism, and single-bit-flip detection are proved by the
// unit tests below instead.
pub
/// Continues a CRC-32C (Castagnoli) checksum over `bytes`, seeded with the result
/// of a prior [`checksum`]/`checksum_append` call. Chaining
/// `checksum_append(checksum(a), b)` equals `checksum(&[a, b].concat())` because
/// [`checksum`] is itself `crc32c_append(0, ..)`; this lets a caller checksum two
/// non-contiguous slices (a record's header prefix and its trailing
/// ops+blob) without allocating a joined buffer on the data path.
///
/// # Performance
///
/// This function is `O(n)` in `bytes.len()`.
//
// kani-skip: delegates to the external `crc32c` crate whose runtime CPU-feature
// dispatch and unbounded scan are outside the model checker's reach, exactly as
// [`checksum`]; the seed-continuation algebra it relies on is the crate's
// documented contract and is exercised by the unit test below.
pub