cml/
schedule.rs

1//! Base-k carry reduction schedule algorithm.
2
3/// Number of k-ary merges after appending an item at 0-based index `n`.
4///
5/// Controls the frontier stack reduction for a configured log arity `k >= 2`.
6///
7/// # Panics
8///
9/// Panics if `k < 2` as the arity must be at least 2.
10#[must_use]
11pub fn reduction_count(n: u64, k: u64) -> u32 {
12    assert!(k >= 2, "log arity k must be >= 2");
13    let mut count = 0;
14    let mut m = (n as u128) + 1; // 1-based index
15    let k_u128 = k as u128;
16    while m % k_u128 == 0 {
17        count += 1;
18        m /= k_u128;
19    }
20    count
21}
22
23#[cfg(test)]
24mod tests {
25    use super::*;
26
27    #[test]
28    fn test_reduction_count_k2() {
29        // Equivalent to EML's count_trailing_ones
30        let expected = vec![
31            0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, 4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0,
32            1, 0, 5,
33        ];
34        for (n, &exp) in expected.iter().enumerate() {
35            assert_eq!(reduction_count(n as u64, 2), exp, "failed for k=2, n={}", n);
36        }
37    }
38
39    #[test]
40    fn test_reduction_count_k3() {
41        let expected = vec![
42            0, 0, 1, 0, 0, 1, 0, 0, 2, 0, 0, 1, 0, 0, 1, 0, 0, 2, 0, 0, 1, 0, 0, 1, 0, 0, 3, 0, 0,
43            1, 0, 0,
44        ];
45        for (n, &exp) in expected.iter().enumerate() {
46            assert_eq!(reduction_count(n as u64, 3), exp, "failed for k=3, n={}", n);
47        }
48    }
49
50    #[test]
51    fn test_reduction_count_k4() {
52        let expected = vec![
53            0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0,
54            0, 0, 2,
55        ];
56        for (n, &exp) in expected.iter().enumerate() {
57            assert_eq!(reduction_count(n as u64, 4), exp, "failed for k=4, n={}", n);
58        }
59    }
60
61    #[test]
62    #[should_panic(expected = "log arity k must be >= 2")]
63    fn test_reduction_count_invalid_k() {
64        let _ = reduction_count(0, 1);
65    }
66
67    /// Rust twin of every Lean `#guard` in `proofs/lean/EMLProof/Kary.lean`
68    /// (`section SanityChecks`).
69    ///
70    /// These are the *same vectors*, transcribed value-for-value, so that
71    /// definitional drift between the Lean topology model and the Rust source
72    /// breaks a build on **either** side rather than going silent. Each Lean
73    /// `#guard` is reproduced below in source order; if one is added there, add
74    /// its twin here. Argument order differs by design: Lean takes the arity
75    /// first (`frontierForSizeT k n`, `reductionCount k n`,
76    /// `inclusionSkeleton k treeSize index`), the Rust API takes it last
77    /// (`frontier_for_size(n, k)`, `reduction_count(n, k)`) or first
78    /// (`inclusion_skeleton(k, tree_size, index)`).
79    ///
80    /// This guard couples both crates: `reduction_count` lives here in CML
81    /// (the frontier carry); `frontier_for_size` lives in the `spine` core; the
82    /// concrete MMR `mountain_skeleton` lives in CML (the log owns its topology
83    /// now). It stays where it can reach all three.
84    ///
85    /// The `inclusionSkeleton` Lean guards move to N54's mountain re-spec; here
86    /// the structural `frontier_for_size`/`reduction_count` parity is pinned, plus
87    /// the mountain skeleton's leaf → peak → bag shape on small cases.
88    #[test]
89    fn lean_guard_parity() {
90        use spine::{SkeletonStep, frontier_for_size};
91
92        use crate::mountain::mountain_skeleton;
93
94        let step = |position: usize, sibling_count: usize| SkeletonStep {
95            position,
96            sibling_count,
97        };
98
99        // frontierForSizeT k n  ⟷  frontier_for_size(n, k)
100        assert_eq!(frontier_for_size(5, 2), vec![(0u64, 2u32), (4, 0)]);
101        assert_eq!(frontier_for_size(5, 3), vec![(0, 1), (3, 0), (4, 0)]);
102        assert_eq!(frontier_for_size(0, 2), Vec::<(u64, u32)>::new());
103
104        // (List.range _).map (reductionCount k)  ⟷  reduction_count(n, k)
105        let rc2: Vec<u32> = (0..8).map(|n| reduction_count(n, 2)).collect();
106        assert_eq!(rc2, vec![0, 1, 0, 2, 0, 1, 0, 3]);
107        let rc3: Vec<u32> = (0..9).map(|n| reduction_count(n, 3)).collect();
108        assert_eq!(rc3, vec![0, 0, 1, 0, 0, 1, 0, 0, 2]);
109
110        // The MMR mountain skeleton: leaf → peak (within-mountain base-k digits)
111        // then bagPath (peak → root). A singleton tree promotes to the root.
112        assert_eq!(mountain_skeleton(2, 1, 0), Some(vec![]));
113        // n=5, k=2: peaks = mountains of [4, 1]. Leaf 4 is the lone size-1
114        // mountain (peak 1); empty peakPath, one bag step (2 peaks → 1 bag node,
115        // peak 1 at position 1, one sibling).
116        assert_eq!(mountain_skeleton(2, 5, 4), Some(vec![step(1, 1)]));
117        // n=4, k=2: one perfect mountain (height 2), no bag. Leaf 1: two digit
118        // steps inside the mountain, empty bagPath.
119        assert_eq!(
120            mountain_skeleton(2, 4, 1),
121            Some(vec![step(1, 1), step(0, 1)])
122        );
123        // n=4, k=3: peaks = mountains of [3, 1]. Leaf 3 is the lone peak 1; one
124        // bag step (2 peaks → 1 bag node, position 1).
125        assert_eq!(mountain_skeleton(3, 4, 3), Some(vec![step(1, 1)]));
126        assert_eq!(mountain_skeleton(2, 4, 4), None); // index out of range
127        assert_eq!(mountain_skeleton(1, 4, 0), None); // arity out of range
128    }
129}
cml/schedule.rs

cml/
schedule.rs
