Module ownership 

Transcription of SafeMesh.RecordKernel ownership rules. The existing Lean corpus binds these decisions to their specification; no Lean runtime is used.

Structs

Refused

WriteContext

Facts supplied by the local fence, not by a remote packet. Public for oracle conformance; constructing these facts does not grant a local writer lease.

WriterConfig

Enums

OwnedPayload

An add mints exactly one token at its record ID. Removes reference observed tokens, including other writers’ tokens, and do not mint tokens.

Traits

OwnedDelta

Extract only the ownership-relevant facts from the existing wire payload.

Functions

allocate_token

Pure allocation rule, evaluated with checked bounded arithmetic. The record sequence starts at one; configuration must be identical across a replica set.

check_counter_record

Checked counter boundary for existing, unfenced replica adapters. This does not grant fencing: it checks the record author’s coordinate before admission.

next_sequence

refuses

The sole Rust transcription of the packet-A refusal predicate. Every local and incoming operation in LocalReplica passes here before M1 admission.