minerva 0.2.0

Causal ordering for distributed systems
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167

//! The snapshot frame's encoder: greedy maximal-chain factoring over the
//! flat ascending locus list, emitting the fixed-width run table, the
//! rank-step columns, and the free-locus section (PRD 0023).
//!
//! The factoring is the frame's canonical form: the chain law
//! ([`chainable`]) is shared verbatim with the decode core, so a run is
//! exactly a maximal chain and every value has one spelling. This encoder
//! deliberately lives beside, not inside, the dual-homed decode core: an
//! encoder core with value-level bijection contracts is the recorded owed
//! tail (ruling R-18's, inherited by R-25), and keeping it here keeps the
//! proof surface honest about what is proven (the decode) and what is
//! pinned by the round-trip suites and the fuzz target (the bijection).

extern crate alloc;

use alloc::vec::Vec;

use super::pure::{
    ANCHOR_TAG_AFTER, ANCHOR_TAG_BEFORE, ANCHOR_TAG_ORIGIN, PureLocus, SNAPSHOT_WIRE_V1, chainable,
    rank_successor,
};

/// One factored region of the ascending locus list: a maximal chain of at
/// least two elements (`start .. start + len`), or a single free locus.
struct Region {
    /// The region's first position in the locus list.
    start: usize,
    /// The region's element count; a region of one is a free locus.
    len: usize,
}

/// Factors the ascending locus list into maximal chains and free loci by
/// one greedy left-to-right pass: a chain extends exactly while the next
/// locus is dot-consecutive on the same station and satisfies the chain
/// law, which is the unique factoring the decoder's split-chain refusal
/// demands.
fn factor(loci: &[PureLocus]) -> Vec<Region> {
    let mut regions = Vec::new();
    let mut start = 0usize;
    while start < loci.len() {
        let mut end = start + 1;
        while end < loci.len() {
            let previous = &loci[end - 1];
            let next = &loci[end];
            let consecutive = previous.station == next.station
                && previous.index < u64::MAX
                && next.index == previous.index + 1;
            if consecutive && chainable(previous, next) {
                end += 1;
            } else {
                break;
            }
        }
        regions.push(Region {
            start,
            len: end - start,
        });
        start = end;
    }
    regions
}

/// Emits one locus's anchor as its tag byte plus, for a dot anchor, the
/// 12-byte anchor dot (the v2 record shape, reused by the free section).
fn push_anchor(out: &mut Vec<u8>, locus: &PureLocus) {
    out.push(locus.anchor_tag);
    if locus.anchor_tag == ANCHOR_TAG_AFTER || locus.anchor_tag == ANCHOR_TAG_BEFORE {
        out.extend_from_slice(&locus.anchor_station.to_be_bytes());
        out.extend_from_slice(&locus.anchor_index.to_be_bytes());
    }
}

/// Emits one locus's rank as the 17-byte stamp frame: the version byte then
/// the four fields in payload order (physical, logical, kairotic, minting
/// station), which is byte-for-byte `Kairos::to_bytes` (pinned by test).
fn push_rank(out: &mut Vec<u8>, locus: &PureLocus) {
    out.push(super::pure::RANK_WIRE_V1);
    out.extend_from_slice(&locus.physical.to_be_bytes());
    out.extend_from_slice(&locus.logical.to_be_bytes());
    out.extend_from_slice(&locus.kairotic.to_be_bytes());
    out.extend_from_slice(&locus.rank_station.to_be_bytes());
}

/// Encodes the flat ascending locus list as one snapshot frame (without the
/// visible have-set suffix, which the caller appends): the header, the
/// fixed-width run table, the rank-step columns in run order, then the free
/// loci in the v2 record shape.
///
/// The caller (the shipped `to_snapshot_bytes`) supplies the skeleton's own
/// strictly ascending enumeration, so the factoring is deterministic and
/// the frame canonical. Infallible; the only allocation is the frame.
pub fn encode_loci(loci: &[PureLocus]) -> Vec<u8> {
    let regions = factor(loci);
    let mut run_count: u32 = 0;
    let mut free_count: u32 = 0;
    for region in &regions {
        if region.len >= 2 {
            run_count = run_count.saturating_add(1);
        } else {
            free_count = free_count.saturating_add(1);
        }
    }

    let mut out = Vec::new();
    out.push(SNAPSHOT_WIRE_V1);
    out.extend_from_slice(&run_count.to_be_bytes());
    out.extend_from_slice(&free_count.to_be_bytes());

    // The run table: one fixed-width row per maximal chain, in the list's
    // (ascending) order. An origin head zeroes its anchor-dot bytes so
    // every row is one width (the S189 fixed-width decision).
    for region in &regions {
        if region.len < 2 {
            continue;
        }
        let head = &loci[region.start];
        out.extend_from_slice(&head.station.to_be_bytes());
        out.extend_from_slice(&head.index.to_be_bytes());
        out.extend_from_slice(&u32::try_from(region.len).unwrap_or(u32::MAX).to_be_bytes());
        out.push(head.anchor_tag);
        if head.anchor_tag == ANCHOR_TAG_ORIGIN {
            out.extend_from_slice(&0u32.to_be_bytes());
            out.extend_from_slice(&0u64.to_be_bytes());
        } else {
            out.extend_from_slice(&head.anchor_station.to_be_bytes());
            out.extend_from_slice(&head.anchor_index.to_be_bytes());
        }
        push_rank(&mut out, head);
    }

    // The rank-step columns, one six-byte record per interior element:
    // zero spells the clock successor, a positive value the physical
    // advance (the chain law admitted no other shape, so the branch is
    // total).
    for region in &regions {
        if region.len < 2 {
            continue;
        }
        for k in 1..region.len {
            let previous = &loci[region.start + k - 1];
            let next = &loci[region.start + k];
            let (successor_physical, successor_logical) =
                rank_successor(previous.physical, previous.logical);
            let step = if next.physical == successor_physical && next.logical == successor_logical {
                0u64
            } else {
                next.physical - previous.physical
            };
            let step_bytes = step.to_be_bytes();
            out.extend_from_slice(&step_bytes[2..8]);
        }
    }

    // The free loci, in the v2 locus-record shape.
    for region in &regions {
        if region.len >= 2 {
            continue;
        }
        let locus = &loci[region.start];
        out.extend_from_slice(&locus.station.to_be_bytes());
        out.extend_from_slice(&locus.index.to_be_bytes());
        push_anchor(&mut out, locus);
        push_rank(&mut out, locus);
    }

    out
}