Module protocol 

Protocol decision kernels — the load-bearing guards of the snapshot export/import protocol, extracted as pure functions so the PRODUCTION code and the exhaustive model checker (tests/model.rs) execute the same logic, not two hand-synchronized copies of it.

Every function here is a guard whose correctness the machine-checked theorems depend on. The call sites:

kernel	production	model
pointer_publish_allowed	transport::swap_pointer	Act::Publish
payload_prunable	transport::ObjectStoreTransport::prune	Act::Prune
resume_window_ok	nats resume paths (check_resume_window)	Act::Resume

Because the model transitions call these very functions, a change to any guard is re-verified against the full bounded state space on the next cargo test --test model — the guards cannot drift from the proof. The mutation tests in tests/model.rs additionally prove each guard is load-bearing: substituting a broken variant makes the checker produce a counterexample.

Kernels operate on plain u64 ranks (a WatchCursor’s revision, with revisionless cursors ranked 0 by the callers) so they stay free of I/O types and usable from the checker’s u8-bounded state space.

Enums

PointerState

What the publisher observed at the pointer key before deciding.

Functions

payload_prunable

THE prune guard: may this payload object be deleted, given the current pointer’s rank?

pointer_publish_allowed

THE monotonic pointer guard: may candidate_rank be published over the observed current pointer?

resume_window_ok

THE cursor-expiry guard: is resuming from revision sound, given the stream’s first retained sequence?