Module chain 

The journal’s hash chain as a decision (I18), apart from the I/O in journal.rs. Hashing stays outside: SHA-256 is trusted (P5), so each record enters as a Link carrying the head it claims to follow (prev) and the head after it (next, from journal::chain). What is proved here is everything else: a record follows exactly when its seq is the next one and its prev is the current head; a segment is accepted exactly when every record follows, and otherwise the first that does not is reported; and what the writer appends always follows.

Structs

Link

One record as the chain sees it.

Enums

Follows

Whether a record follows the chain, and if not, why.

Verdict

How a whole segment checked out.

Functions

follows

The check every read path applies to each record (journal::scan).

hash_eq

next_link

The seq and prev the writer gives the next record (journal::append): the next seq, and the current head.

verify

Check a segment (journal::verify_chain): accepts exactly a chained segment, and otherwise reports its first break.