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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456

//! The pure re-mint core of the epoch re-foundation fold: the
//! Creusot-provable half of [`Rhapsody::refound`](super::Rhapsody::refound),
//! discharging the R2 proof plan's deductive obligations (PRD 0024; the
//! division ruled in R-9 and the dual-homed shape landed by ruling R-18).
//!
//! This file is *dual-homed*: minerva compiles it contract-free (every proof
//! attribute is `#[cfg_attr(creusot, ...)]`, and `cfg(creusot)` is never set
//! by a normal build, so no proof dependency exists), and the detached
//! `proofs/` crate includes the same file by `#[path]` and compiles it under
//! `cargo creusot`, where the contracts come alive and Why3 discharges the
//! verification conditions. One source, two readings; the shipped fold in
//! `refound/mod.rs` drives this core's output through the spelling and store
//! folds, so the proven code is the running code, never a shadow.
//!
//! What the contracts state, in the charter's terms (PRD 0024 R2):
//!
//! * *Totality* under `#[check(terminates)]`: no reachable panic on any walk
//!   (every index and every tally increment discharges its VC), and every
//!   walk element is assigned (the output is index-aligned with the input).
//! * *Order preservation*: two walk elements of one station mint in walk
//!   order (`order(new) == translate(order(old))`, stated per station because
//!   the walk sequence itself is the cross-station order and it is preserved
//!   by index alignment).
//! * *The live-content bijection*: no two walk elements share a minted dot.
//! * *Consecutiveness*: a walk element sharing its predecessor's station
//!   mints the successor counter, the arithmetic fact under the born-coalesced
//!   pin (the shipped fold's inline chain step is licensed by exactly this).
//! * *Floor-perfection*, in predecessor form: every minted counter of two or
//!   more has its predecessor minted earlier for the same station, every
//!   tally row is itself minted, and every minted counter sits at or below
//!   its station's tally. Together with injectivity these say station `s`'s
//!   minted counters are exactly `1..=n_s`: the attained set is
//!   predecessor-closed down to one and reaches the tally, so it is gap-free
//!   by descending induction (a two-line argument recorded here because an
//!   SMT solver cannot induct, while each conjunct is a one-step witness
//!   transfer it discharges directly; the sampled `assert_fold_laws` bundle
//!   pins the expanded `1..=n_s` form on generated documents).
//!
//! The subset discipline (the S94 record): index-cursor reads, no iterator
//! adapters, derives gated off under `cfg(creusot)`, and a plain struct output
//! the shipped fold destructures. A private `BTreeMap` indexes the flat tally
//! vector, preserving logarithmic station lookup without making the proof
//! reason about tree internals; [`StationTallies`] owns both representations,
//! its opaque type invariant makes desynchronization unavailable to modular
//! proofs, and its `mint` operation states the exact vector transition. The
//! step that touches both vectors lives in its own function
//! ([`mint_one`]) so each obligation discharges in a small local task, and
//! every quantified contract keeps its variables anchored in sequence reads
//! (the predecessor form exists for exactly that: a `forall k` bound only by
//! arithmetic gives the prover no term to instantiate, the lesson this
//! file's first shape taught).

extern crate alloc;

use alloc::collections::BTreeMap;
use alloc::vec::Vec;

/// The pearlite vocabulary (`Int` in the quantifiers) and the loop-spec
/// macros, alive only under the proofs crate's `cargo creusot` compile; a
/// normal minerva build strips these imports with the rest of the proof
/// reading. Only the first loop-spec attribute on a loop expands as a macro
/// and so needs importing, here `variant`, which leads every loop; the
/// trailing `invariant`s are consumed as inert tokens by that same pass.
#[cfg(creusot)]
use ::creusot_std::macros::variant;
#[cfg(creusot)]
use ::creusot_std::prelude::{Int, Invariant};

/// The re-mint assignment: the fold's identity arithmetic, frozen.
///
/// `minted` is index-aligned with the input walk (`minted[i]` is walk element
/// `i`'s new dot); `live` carries each station's final tally `(s, n_s)`,
/// stations distinct, in first-appearance order. The shipped fold folds
/// `live` into the map's per-station range widths and zips `minted` against
/// the walk to spell loci; both facts it relies on are contracts here, never
/// conventions.
#[cfg_attr(not(creusot), derive(Debug, Clone, PartialEq, Eq))]
pub struct PureRemint {
    /// Walk element `i`'s minted dot `(station, counter)`, station preserved.
    pub minted: Vec<(u32, u64)>,
    /// Per-station final tallies `(station, n_s)`, stations distinct.
    pub live: Vec<(u32, u64)>,
}

/// Logarithmically indexed ownership boundary for the proof-facing tallies.
///
/// Both structures are private and only [`mint`](Self::mint) mutates them, so
/// no caller can construct a desynchronized index/vector pair. Its opaque
/// Creusot type invariant denotes that every map entry names the unique row
/// for its station and every row has that entry. The standard collection
/// operation is the narrow trusted seam; all arithmetic and sequence laws
/// above it remain proved.
struct StationTallies {
    positions: BTreeMap<u32, usize>,
    live: Vec<(u32, u64)>,
}

#[cfg(creusot)]
impl Invariant for StationTallies {
    #[::creusot_std::macros::logic(opaque)]
    fn invariant(self) -> bool {
        false
    }
}

impl StationTallies {
    #[cfg_attr(creusot, ::creusot_std::macros::trusted)]
    #[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
    #[cfg_attr(creusot, ::creusot_std::macros::ensures(result.invariant()))]
    #[cfg_attr(creusot, ::creusot_std::macros::ensures(result.live@.len() == 0))]
    const fn new() -> Self {
        Self {
            positions: BTreeMap::new(),
            live: Vec::new(),
        }
    }

    #[cfg_attr(creusot, ::creusot_std::macros::trusted)]
    #[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
    #[cfg_attr(creusot, ::creusot_std::macros::requires((*self).invariant()))]
    #[cfg_attr(creusot, ::creusot_std::macros::ensures((^self).invariant()))]
    #[cfg_attr(creusot, ::creusot_std::macros::requires(
        forall<p: Int, q: Int> 0 <= p && p < q && q < (*self).live@.len()
            ==> (*self).live@[p].0@ != (*self).live@[q].0@
    ))]
    #[cfg_attr(creusot, ::creusot_std::macros::requires(
        forall<q: Int> 0 <= q && q < (*self).live@.len()
            ==> 1 <= (*self).live@[q].1@ && (*self).live@[q].1@ < 18446744073709551615
    ))]
    #[cfg_attr(creusot, ::creusot_std::macros::ensures(
        ((^self).live@.len() == (*self).live@.len()
            && result@ >= 2
            && exists<q: Int> 0 <= q && q < (*self).live@.len()
                && (*self).live@[q].0@ == station@
                && result@ == (*self).live@[q].1@ + 1
                && (^self).live@[q].0@ == station@
                && (^self).live@[q].1@ == result@
                && forall<r: Int> 0 <= r && r < (*self).live@.len() && r != q
                    ==> (^self).live@[r] == (*self).live@[r])
        || ((^self).live@.len() == (*self).live@.len() + 1
            && result@ == 1
            && (^self).live@[(*self).live@.len()].0@ == station@
            && (^self).live@[(*self).live@.len()].1@ == 1
            && (forall<q: Int> 0 <= q && q < (*self).live@.len()
                ==> (*self).live@[q].0@ != station@)
            && forall<q: Int> 0 <= q && q < (*self).live@.len()
                ==> (^self).live@[q] == (*self).live@[q])
    ))]
    fn mint(&mut self, station: u32) -> u64 {
        if let Some(&position) = self.positions.get(&station) {
            debug_assert_eq!(self.live[position].0, station);
            let next = self.live[position].1 + 1;
            self.live[position].1 = next;
            next
        } else {
            let position = self.live.len();
            let old = self.positions.insert(station, position);
            debug_assert!(old.is_none());
            self.live.push((station, 1));
            1
        }
    }
}

/// One re-mint step: advance `station`'s tally and mint its new ceiling.
///
/// The whole effect is stated as contracts so the fold's loop invariants
/// re-establish from this function's postconditions alone: the tally table
/// keeps distinct stations, existing rows never move, shrink, or change
/// station, the minted vector grows by exactly the new ceiling, and the
/// witness families (predecessor closure, tally attainment, coverage)
/// transfer across the step. The tally bound (`requires`) is what makes the
/// increment total: a caller tallies at most once per walk element, so a
/// tally never reaches the dot space's ceiling.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
// Tallies are distinct by station, nonzero, and below the increment ceiling.
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<p: Int, q: Int> 0 <= p && p < q && q < (*tallies).live@.len()
        ==> (*tallies).live@[p].0@ != (*tallies).live@[q].0@
))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<q: Int> 0 <= q && q < (*tallies).live@.len()
        ==> 1 <= (*tallies).live@[q].1@ && (*tallies).live@[q].1@ < 18446744073709551615
))]
// Predecessor closure holds on entry.
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<j: Int> 0 <= j && j < minted@.len() && 2 <= minted@[j].1@
        ==> exists<j2: Int> 0 <= j2 && j2 < j
            && minted@[j2].0@ == minted@[j].0@
            && minted@[j2].1@ == minted@[j].1@ - 1
))]
// Tally attainment holds on entry: every tally row is minted.
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<q: Int> 0 <= q && q < (*tallies).live@.len()
        ==> exists<j: Int> 0 <= j && j < minted@.len()
            && minted@[j].0@ == (*tallies).live@[q].0@
            && minted@[j].1@ == (*tallies).live@[q].1@
))]
// Coverage holds on entry: every minted element sits at or below its
// station's tally.
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<j: Int> 0 <= j && j < minted@.len()
        ==> exists<q: Int> 0 <= q && q < (*tallies).live@.len()
            && (*tallies).live@[q].0@ == minted@[j].0@
            && minted@[j].1@ <= (*tallies).live@[q].1@
))]
// The mint: exactly one element appended, the station's new ceiling.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    (^minted)@.len() == minted@.len() + 1
        && (^minted)@[minted@.len()].0@ == station@
        && (^minted)@[minted@.len()].1@ == result@
        && forall<j: Int> 0 <= j && j < minted@.len()
            ==> (^minted)@[j] == minted@[j]
))]
// The tally step: either the station's found row advanced to `result`, or a
// fresh `(station, 1)` row was appended; rows never move, shrink, or change
// station either way.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    ((^tallies).live@.len() == (*tallies).live@.len()
        && result@ >= 2
        && exists<q: Int> 0 <= q && q < (*tallies).live@.len()
            && (*tallies).live@[q].0@ == station@
            && result@ == (*tallies).live@[q].1@ + 1
            && (^tallies).live@[q].0@ == station@
            && (^tallies).live@[q].1@ == result@
            && forall<r: Int> 0 <= r && r < (*tallies).live@.len() && r != q
                ==> (^tallies).live@[r] == (*tallies).live@[r])
    || ((^tallies).live@.len() == (*tallies).live@.len() + 1
        && result@ == 1
        && (^tallies).live@[(*tallies).live@.len()].0@ == station@
        && (^tallies).live@[(*tallies).live@.len()].1@ == 1
        && (forall<q: Int> 0 <= q && q < (*tallies).live@.len()
            ==> (*tallies).live@[q].0@ != station@)
        && forall<q: Int> 0 <= q && q < (*tallies).live@.len()
            ==> (^tallies).live@[q] == (*tallies).live@[q])
))]
// Stations stay distinct; existing rows keep their station and never shrink.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<p: Int, q: Int> 0 <= p && p < q && q < (^tallies).live@.len()
        ==> (^tallies).live@[p].0@ != (^tallies).live@[q].0@
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<q: Int> 0 <= q && q < (*tallies).live@.len()
        ==> (^tallies).live@[q].0@ == (*tallies).live@[q].0@
            && (*tallies).live@[q].1@ <= (^tallies).live@[q].1@
))]
// Predecessor closure transfers.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<j: Int> 0 <= j && j < (^minted)@.len() && 2 <= (^minted)@[j].1@
        ==> exists<j2: Int> 0 <= j2 && j2 < j
            && (^minted)@[j2].0@ == (^minted)@[j].0@
            && (^minted)@[j2].1@ == (^minted)@[j].1@ - 1
))]
// Tally attainment transfers.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<q: Int> 0 <= q && q < (^tallies).live@.len()
        ==> exists<j: Int> 0 <= j && j < (^minted)@.len()
            && (^minted)@[j].0@ == (^tallies).live@[q].0@
            && (^minted)@[j].1@ == (^tallies).live@[q].1@
))]
// Coverage transfers.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<j: Int> 0 <= j && j < (^minted)@.len()
        ==> exists<q: Int> 0 <= q && q < (^tallies).live@.len()
            && (^tallies).live@[q].0@ == (^minted)@[j].0@
            && (^minted)@[j].1@ <= (^tallies).live@[q].1@
))]
fn mint_one(minted: &mut Vec<(u32, u64)>, tallies: &mut StationTallies, station: u32) -> u64 {
    let counter = tallies.mint(station);
    #[cfg(creusot)]
    let sealed = ::creusot_std::macros::snapshot!(minted@);
    minted.push((station, counter));
    // The push bridges, stated once as ground equalities: the prefix is
    // unedited and the new element is the station's fresh ceiling, so every
    // witness transfer in the postconditions rides these instead of chasing
    // the sequence-extension axioms.
    #[cfg(creusot)]
    ::creusot_std::macros::proof_assert!(
        minted@.len() == (*sealed).len() + 1
            && minted@[(*sealed).len()].0@ == station@
            && minted@[(*sealed).len()].1@ == counter@
            && forall<j: Int> 0 <= j && j < (*sealed).len()
                ==> minted@[j] == (*sealed)[j]
    );
    counter
}

/// Assigns every walk element its re-minted dot: station `s`'s `k`-th walk
/// element mints `(s, k)`.
///
/// The input is the sealed stratum's effective live order (the `OrderWalk`
/// yields visible elements only, so tombstones never reach this function);
/// the output is the compaction half of the re-foundation's dot map and the
/// dot sequence the new store is born under. Everything the charter's R2
/// fold core owes deductively is a postcondition on this function; the
/// affine half above the ceilings is the sibling Kani harness's territory
/// (heap-free, in `refound/mod.rs`), per the R-9 division.
///
/// Floor-perfection is stated in its proof-shaped decomposition: counters
/// are predecessor-closed (every minted counter of two or more has its
/// predecessor minted earlier for the same station), every tally row is
/// attained, and every minted counter is bounded by its station's tally.
/// With injectivity, station `s`'s attained set therefore reaches `n_s`, is
/// closed downward to one, and repeats nothing: exactly `1..=n_s`.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
// Totality of the assignment: every walk element is minted, in place.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    result.minted@.len() == order@.len()
))]
// The re-mint is per original station: the station never changes.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int> 0 <= i && i < order@.len()
        ==> result.minted@[i].0@ == order@[i].0@
))]
// Counters are 1-based and bounded by the walk length.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int> 0 <= i && i < order@.len()
        ==> 1 <= result.minted@[i].1@ && result.minted@[i].1@ <= order@.len()
))]
// Order preservation: one station's elements mint in walk order.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int, j: Int> 0 <= i && i < j && j < order@.len()
        && order@[i].0@ == order@[j].0@
        ==> result.minted@[i].1@ < result.minted@[j].1@
))]
// The bijection's injective half: no two walk elements share a minted dot.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int, j: Int> 0 <= i && i < j && j < order@.len()
        ==> result.minted@[i].0@ != result.minted@[j].0@
            || result.minted@[i].1@ != result.minted@[j].1@
))]
// Consecutiveness: a same-station walk neighbour mints the successor
// counter (the born-coalesced arithmetic the inline chain step spells).
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int> 1 <= i && i < order@.len()
        && order@[i].0@ == order@[i - 1].0@
        ==> result.minted@[i].1@ == result.minted@[i - 1].1@ + 1
))]
// The tally table is a function: stations appear at most once in `live`,
// and every tally is nonzero and bounded by the walk length.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<p: Int, q: Int> 0 <= p && p < q && q < result.live@.len()
        ==> result.live@[p].0@ != result.live@[q].0@
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<p: Int> 0 <= p && p < result.live@.len()
        ==> 1 <= result.live@[p].1@ && result.live@[p].1@ <= order@.len()
))]
// Coverage: every minted counter sits at or below its station's tally, and
// the tally row exists.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int> 0 <= i && i < order@.len()
        ==> exists<p: Int> 0 <= p && p < result.live@.len()
            && result.live@[p].0@ == order@[i].0@
            && result.minted@[i].1@ <= result.live@[p].1@
))]
// Floor-perfection, predecessor half: minted counters are closed downward.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<j: Int> 0 <= j && j < result.minted@.len()
        && 2 <= result.minted@[j].1@
        ==> exists<j2: Int> 0 <= j2 && j2 < j
            && result.minted@[j2].0@ == result.minted@[j].0@
            && result.minted@[j2].1@ == result.minted@[j].1@ - 1
))]
// Floor-perfection, ceiling half: every tally row is attained.
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<p: Int> 0 <= p && p < result.live@.len()
        ==> exists<j: Int> 0 <= j && j < result.minted@.len()
            && result.minted@[j].0@ == result.live@[p].0@
            && result.minted@[j].1@ == result.live@[p].1@
))]
#[must_use]
pub fn remint(order: &[(u32, u64)]) -> PureRemint {
    let mut minted: Vec<(u32, u64)> = Vec::new();
    let mut tallies = StationTallies::new();

    let mut i: usize = 0;
    #[cfg_attr(creusot, variant(order@.len() - i@))]
    #[cfg_attr(creusot, invariant(i@ <= order@.len()))]
    #[cfg_attr(creusot, invariant(minted@.len() == i@))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int> 0 <= j && j < i@ ==> minted@[j].0@ == order@[j].0@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int> 0 <= j && j < i@
            ==> 1 <= minted@[j].1@ && minted@[j].1@ <= i@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int, k: Int> 0 <= j && j < k && k < i@
            && order@[j].0@ == order@[k].0@
            ==> minted@[j].1@ < minted@[k].1@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int> 1 <= j && j < i@ && order@[j].0@ == order@[j - 1].0@
            ==> minted@[j].1@ == minted@[j - 1].1@ + 1
    ))]
    #[cfg_attr(creusot, invariant(
        forall<p: Int, q: Int> 0 <= p && p < q && q < tallies.live@.len()
            ==> tallies.live@[p].0@ != tallies.live@[q].0@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<p: Int> 0 <= p && p < tallies.live@.len()
            ==> 1 <= tallies.live@[p].1@ && tallies.live@[p].1@ <= i@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int> 0 <= j && j < i@
            ==> exists<p: Int> 0 <= p && p < tallies.live@.len()
                && tallies.live@[p].0@ == order@[j].0@
                && minted@[j].1@ <= tallies.live@[p].1@
    ))]
    #[cfg_attr(creusot, invariant(
        forall<j: Int> 0 <= j && j < i@ && 2 <= minted@[j].1@
            ==> exists<j2: Int> 0 <= j2 && j2 < j
                && minted@[j2].0@ == minted@[j].0@
                && minted@[j2].1@ == minted@[j].1@ - 1
    ))]
    #[cfg_attr(creusot, invariant(
        forall<p: Int> 0 <= p && p < tallies.live@.len()
            ==> exists<j: Int> 0 <= j && j < i@
                && minted@[j].0@ == tallies.live@[p].0@
                && minted@[j].1@ == tallies.live@[p].1@
    ))]
    // The previous walk element's station row tallies exactly its counter
    // (the tally is the last assignment): the link consecutiveness rides.
    #[cfg_attr(creusot, invariant(
        i@ == 0 || exists<p: Int> 0 <= p && p < tallies.live@.len()
            && tallies.live@[p].0@ == minted@[i@ - 1].0@
            && tallies.live@[p].1@ == minted@[i@ - 1].1@
    ))]
    while i < order.len() {
        let station = order[i].0;
        let _ = mint_one(&mut minted, &mut tallies, station);
        i += 1;
    }

    PureRemint {
        minted,
        live: tallies.live,
    }
}

#[cfg(test)]
mod tests {
    use super::{Vec, remint};

    #[test]
    fn many_distinct_stations_remain_linearithmic() {
        const STATIONS: u32 = 16_384;
        let order: Vec<_> = (0..STATIONS).map(|station| (station, 1)).collect();

        let assignment = remint(&order);

        assert_eq!(assignment.minted, order);
        assert_eq!(assignment.live, order);
    }
}