safemesh_crdt/
ownership.rs

1// Copyright (C) 2026 Ben Cassie
2// SPDX-License-Identifier: Apache-2.0
3//! Transcription of SafeMesh.RecordKernel ownership rules. The existing Lean
4//! corpus binds these decisions to their specification; no Lean runtime is used.
5use crate::{GCounterDelta, OrSetDelta, PnCounterDelta, RecordId};
6
7#[derive(Clone, Copy, Debug, PartialEq, Eq)]
8pub struct WriterConfig {
9    pub writers: u64,
10    pub writer: u64,
11}
12
13#[derive(Clone, Copy, Debug, PartialEq, Eq)]
14pub struct Refused;
15
16impl WriterConfig {
17    pub fn validate(self) -> Result<(), Refused> {
18        if self.writer < self.writers {
19            Ok(())
20        } else {
21            Err(Refused)
22        }
23    }
24}
25
26/// Facts supplied by the local fence, not by a remote packet. Public for oracle
27/// conformance; constructing these facts does not grant a local writer lease.
28#[derive(Clone, Copy, Debug)]
29pub struct WriteContext {
30    pub config: WriterConfig,
31    pub held: bool,
32    pub generation: u64,
33    pub current_generation: u64,
34    pub local: bool,
35}
36
37/// An add mints exactly one token at its record ID. Removes reference observed
38/// tokens, including other writers' tokens, and do not mint tokens.
39#[derive(Clone, Copy, Debug)]
40pub enum OwnedPayload {
41    Counter(u64),
42    Add(u64),
43    Remove,
44}
45
46pub fn next_sequence(last: u64) -> Option<u64> {
47    last.checked_add(1)
48}
49
50/// Pure allocation rule, evaluated with checked bounded arithmetic. The record
51/// sequence starts at one; configuration must be identical across a replica set.
52pub fn allocate_token(writers: u64, author: u64, sequence: u64) -> Option<u64> {
53    if author >= writers || sequence == 0 {
54        return None;
55    }
56    sequence.checked_mul(writers)?.checked_add(author)
57}
58
59/// The sole Rust transcription of the packet-A refusal predicate. Every local
60/// and incoming operation in LocalReplica passes here before M1 admission.
61pub fn refuses(ctx: WriteContext, id: RecordId, payload: OwnedPayload) -> bool {
62    !(ctx.config.writer < ctx.config.writers
63        && ctx.held
64        && ctx.generation > 0
65        && ctx.generation == ctx.current_generation
66        && id.replica < ctx.config.writers
67        && id.sequence > 0
68        && (!ctx.local || id.replica == ctx.config.writer)
69        && match payload {
70            OwnedPayload::Counter(coordinate) => coordinate == id.replica,
71            OwnedPayload::Add(token) => {
72                allocate_token(ctx.config.writers, id.replica, id.sequence) == Some(token)
73            }
74            OwnedPayload::Remove => true,
75        })
76}
77
78/// Extract only the ownership-relevant facts from the existing wire payload.
79pub trait OwnedDelta {
80    fn owned_payload(&self) -> OwnedPayload;
81}
82impl OwnedDelta for GCounterDelta {
83    fn owned_payload(&self) -> OwnedPayload {
84        OwnedPayload::Counter(self.replica as u64)
85    }
86}
87impl OwnedDelta for PnCounterDelta {
88    fn owned_payload(&self) -> OwnedPayload {
89        match self {
90            Self::Inc { replica, .. } | Self::Dec { replica, .. } => {
91                OwnedPayload::Counter(*replica as u64)
92            }
93        }
94    }
95}
96impl<T> OwnedDelta for OrSetDelta<T, u64> {
97    fn owned_payload(&self) -> OwnedPayload {
98        match self {
99            Self::Add { token, .. } => OwnedPayload::Add(*token),
100            Self::Remove { .. } => OwnedPayload::Remove,
101        }
102    }
103}
104
105/// Checked counter boundary for existing, unfenced replica adapters. This does
106/// not grant fencing: it checks the record author's coordinate before admission.
107pub fn check_counter_record<D: OwnedDelta>(
108    writers: usize,
109    id: RecordId,
110    delta: &D,
111) -> Result<(), Refused> {
112    let ctx = WriteContext {
113        config: WriterConfig {
114            writers: writers as u64,
115            writer: 0,
116        },
117        held: true,
118        generation: 1,
119        current_generation: 1,
120        local: false,
121    };
122    if refuses(ctx, id, delta.owned_payload()) {
123        Err(Refused)
124    } else {
125        Ok(())
126    }
127}
safemesh_crdt/ownership.rs

safemesh_crdt/
ownership.rs
