Chapter 30 — Verification lab: evidence preservation invariants
Lesson map
Lesson 30 published. Map, example, EX008.
flowchart TD
N0["Learning outcomes and connection"]
N1["30.1 Invariants for an evidence pipeline"]
N2["30.2 Fault model"]
N3["30.3 The lab"]
N4["30.4 Explaining the results"]
N5["30.5 From lab to continuous verification"]
N6["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6
N6 --> EX["Worked example"]
EX --> Q["Exercise EX008"]
Logical drawing
flowchart LR
N0["Learning outcomes and connection"]
N1["30.1 Invariants for an evidence pipeline"]
N2["30.2 Fault model"]
N3["30.3 The lab"]
N4["30.4 Explaining the results"]
N5["30.5 From lab to continuous verification"]
N6["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> Q["EX008"]
[Learning outcomes and connection]
|
v
[30.1 Invariants for an evidence pipeline]
|
v
[30.2 Fault model]
|
v
[30.3 The lab]
|
v
[30.4 Explaining the results]
|
v
[30.5 From lab to continuous verification]
|
v
[Chapter synthesis]
|
v
[Worked example] --> [Exercise EX008]
Learning outcomes and connection
After this lab you can (1) state evidence-preservation invariants precisely; (2) implement them as executable checks; (3) inject duplicate, delayed, reordered and corrupted inputs; and (4) explain each failed check by its mechanism and fix. It builds on Chapters 4, 9, 22 and 28 and prepares Chapters 40, 45 and 47.
30.1 Invariants for an evidence pipeline
- I1 Raw first: every received record is stored raw before any processing.
- I2 Outcome completeness: every receipt has exactly one recorded outcome — stored, duplicate or rejected.
- I3 Integrity: every stored payload matches its content hash.
- I4 No distinct loss: every distinct payload received is either stored or explicitly rejected with reason.
- I5 Idempotence: re-ingesting the same input changes nothing.
- I6 Audit completeness: every state change appears in the audit log.
These are properties over all inputs, not examples. Testing them under hostile input is a form of the verification-by-property approach of Chapter 9 and of fault injection in Chapter 40.
30.2 Fault model
Inputs are duplicated (at-least-once delivery), delayed and reordered (network and buffering), corrupted (content does not match its claimed hash) and conflicting — the same record ID with different content, which happens when a source re-emits a corrected event or when an attacker injects a look-alike. Lab 30 injects one of each kind of fault into a stream of 20 records: two duplicates, one conflicting r5 and one corrupted r99, all shuffled with seed 30. A design that defends against only one of these kinds can still pass checks written for the others.
30.3 The lab
"""Lab 30 (synthetic): evidence-preservation invariants under duplicate, delayed and corrupted input."""
import hashlib, random
def h(b): return hashlib.sha256(b).hexdigest()
class Pipeline:
def __init__(self, dedupe_by_hash=True):
self.raw, self.store, self.audit, self.rejects, self.dedupe = [], {}, [], [], dedupe_by_hash
def ingest(self, rec_id, payload, claimed_sha):
self.raw.append((rec_id, payload)) # I1 raw copy first
self.audit.append(("received", rec_id))
if h(payload) != claimed_sha:
self.rejects.append(rec_id); self.audit.append(("rejected", rec_id)); return
key = h(payload) if self.dedupe else rec_id
if key in self.store: self.audit.append(("duplicate", rec_id)); return
self.store[key] = (rec_id, payload); self.audit.append(("stored", rec_id))
def check(p, n_sent):
res = {}
res["I1 raw count == sent"] = len(p.raw) == n_sent
res["I2 every receipt has an outcome"] = sum(1 for a in p.audit if a[0] == "received") == \
sum(1 for a in p.audit if a[0] in {"rejected", "duplicate", "stored"})
res["I3 stored payloads match their hash"] = all(h(v[1]) == k for k, v in p.store.items()) if p.dedupe else True
res["I4 no distinct payload lost"] = len({h(pl) for _, pl in p.raw} - {h(v[1]) for v in p.store.values()} - {h(pl) for rid, pl in p.raw if rid in p.rejects}) == 0
return res
rng = random.Random(30)
recs = [(f"r{i}", f"event {i}".encode()) for i in range(20)]
stream = [(rid, pl, h(pl)) for rid, pl in recs]
stream += [stream[3], stream[7]] # duplicates
stream.append(("r5", b"event 5 CHANGED", h(b"event 5 CHANGED"))) # same id, different content
stream.append(("r99", b"tampered", h(b"original"))) # corrupted
rng.shuffle(stream) # delayed / reordered
for mode in (True, False):
p = Pipeline(dedupe_by_hash=mode)
for s in stream: p.ingest(*s)
print("dedupe by", "content hash" if mode else "record id", "| stored", len(p.store), "| rejects", p.rejects)
for k, v in check(p, len(stream)).items(): print(f" {'PASS' if v else 'FAIL'} {k}")
Expected output:
dedupe by content hash | stored 21 | rejects ['r99']
PASS I1 raw count == sent
PASS I2 every receipt has an outcome
PASS I3 stored payloads match their hash
PASS I4 no distinct payload lost
dedupe by record id | stored 20 | rejects ['r99']
PASS I1 raw count == sent
PASS I2 every receipt has an outcome
PASS I3 stored payloads match their hash
FAIL I4 no distinct payload lost
The lab builds a stream of 24 receipts: twenty distinct records r0–r19, duplicates of two of them, a second r5 with changed content, and an r99 whose payload does not match its claimed hash. It shuffles the stream with seed 30 and feeds it to two pipeline variants that differ only in their deduplication key, content hash or record ID. The check function then evaluates I1 to I4 on each variant; I5 and I6 are left to the exercises. The expected output shows 21 stored items under content-hash deduplication and 20 under record-ID deduplication, and only the second variant fails I4.
30.4 Explaining the results
With deduplication by content hash, all invariants pass: both versions of r5 are stored as distinct items and the corrupted r99 is rejected with its raw copy retained. With deduplication by record ID, I4 fails: whichever version of r5 arrives second is classified as a duplicate and its distinct content is lost from the store, although the raw copy (I1) still holds it. The mechanism: identity was defined by a label the source controls, not by content. The fix: deduplicate by content hash; when the same record ID appears with different content, store both and raise a conflict event for review. This mirrors EX008 at pipeline scale.
Note what the checks do not prove: that the source was honest, that no records were lost before reaching the pipeline, or that the shuffle explored every ordering. Use sequence numbers and heartbeats at sources (Chapter 3) for upstream loss and run many seeds for ordering.
30.5 From lab to continuous verification
Run the invariant checks continuously in production as reconciliation jobs: counts of received vs outcomes per hour (I2), sampled hash verification (I3), and conflict-rate metrics. A failed invariant in production is an incident about the response platform itself.
For HVSS, the I4 failure from Lab 30 would surface in production as a conflict-rate metric: the same record ID arriving with different content, as r5 did, raised as a conflict event for review. An hourly I2 reconciliation would likewise detect receipts with no recorded outcome before a case reviewer finds the gap.
30.6 Errors and limits
- Deduplication by source-controlled identifiers.
- Invariants checked only on clean test data.
- One random seed taken as coverage.
- Raw copies kept but never reconciled against the store.
Lab 30 contains a small, concrete instance of each error in this list. The record-ID pipeline trusted a label that the source controls, and lost the changed r5 from the store as a result. A clean stream of twenty distinct records would have passed all four checks in both modes. The single shuffle with seed 30 explored one ordering of 24 receipts. The raw copy still held the lost r5, yet only a reconciliation of raw against store revealed the loss.
Exercises — chapter 30
EX059 — Add I5. Objective: implement idempotence. Inputs: Lab 30. Steps: add a check that ingesting the entire stream a second time leaves store unchanged and adds only duplicate or rejected outcomes; run for both modes. Expected evidence: code and output. Rubric: 3 = correct check with both modes passing I5 and explanation; 2 = check only; 1 = attempt; 0 = none.
EX060 — Conflict events. Objective: repair the failing design. Inputs: Lab 30, record-ID mode. Steps: modify ingestion so that a known record ID with different content is stored under a new key and emits a conflict audit event; rerun; show I4 passing. Expected evidence: code and output. Rubric: 3 = I4 passes with conflict event logged; 2 = passes without event; 1 = attempt; 0 = none.
Chapter synthesis
Evidence preservation is verified by invariants under hostile input: raw first, complete outcomes, integrity, no distinct loss, idempotence and audit completeness. Each failure has a mechanism; content-based identity and explicit conflict handling fix the common one.
Continue studying — chapter 30 of 50
← Chapter 29 · Course chapter index · Chapter 31 →
Continue to the next authored lesson.