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, 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<T> OwnedDelta for OrSetDelta<T, u64> {
88    fn owned_payload(&self) -> OwnedPayload {
89        match self {
90            Self::Add { token, .. } => OwnedPayload::Add(*token),
91            Self::Remove { .. } => OwnedPayload::Remove,
92        }
93    }
94}
95
96/// Checked counter boundary for existing, unfenced replica adapters. This does
97/// not grant fencing: it checks the record author's coordinate before admission.
98pub fn check_counter_record(
99    writers: usize,
100    id: RecordId,
101    delta: &GCounterDelta,
102) -> Result<(), Refused> {
103    let ctx = WriteContext {
104        config: WriterConfig {
105            writers: writers as u64,
106            writer: 0,
107        },
108        held: true,
109        generation: 1,
110        current_generation: 1,
111        local: false,
112    };
113    if refuses(ctx, id, delta.owned_payload()) {
114        Err(Refused)
115    } else {
116        Ok(())
117    }
118}
safemesh_crdt/ownership.rs

safemesh_crdt/
ownership.rs
