tawasuyu/hifas

1//! `lattice` — estados de retículo y restricciones de Galois (Addendum §D, T5).
2//!
3//! La pista de retículos (Ghrist–Riess 2022): reemplaza los espacios vectoriales
4//! del MVP por **retículos** y las matrices por **conexiones de Galois**. No toca
5//! el motor lineal (`cohomology`), que sigue como oráculo topológico barato.
6//!
7//! Aquí viven las piezas de grado 0: los tipos de retículo (`Nat`, `ResetVal`) y
8//! la interfaz de restricción adjunta (`GaloisRestriction`). El Laplaciano de
9//! Tarski que las difunde a punto fijo llega en T6 (`tarski`).
10
11use std::cmp::Ordering;
12
13/// Un estado local con estructura de retículo acotado (Addendum §D).
14///
15/// `join` (∨) y `meet` (∧) deben ser asociativos, conmutativos, idempotentes y
16/// cumplir absorción; `bottom` (⊥) y `top` (⊤) son sus neutros/absorbentes.
17pub trait LatticeCell: Clone + PartialOrd {
18    /// Supremo ∨ (least upper bound).
19    fn join(&self, other: &Self) -> Self;
20    /// Ínfimo ∧ (greatest lower bound).
21    fn meet(&self, other: &Self) -> Self;
22    /// Elemento mínimo ⊥.
23    fn bottom() -> Self;
24    /// Elemento máximo ⊤.
25    fn top() -> Self;
26}
27
28/// Una casilla de `GCounter` como cadena ℕ con ⊤ = ∞ (Addendum §D.1).
29///
30/// Join = máximo, meet = mínimo. Monótono por construcción: nunca resta. El
31/// `GCounter` completo es el **producto** de estas cadenas (se arma en la stalk
32/// del haz de retículos en T6).
33#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
34pub struct Nat(pub u64);
35
36impl Nat {
37    /// Representación de ∞ (el ⊤ de la cadena).
38    pub const INF: Nat = Nat(u64::MAX);
39}
40
41impl LatticeCell for Nat {
42    fn join(&self, other: &Self) -> Self {
43        Nat(self.0.max(other.0))
44    }
45    fn meet(&self, other: &Self) -> Self {
46        Nat(self.0.min(other.0))
47    }
48    fn bottom() -> Self {
49        Nat(0)
50    }
51    fn top() -> Self {
52        Nat::INF
53    }
54}
55
56/// Un `ResettableRegister` como retículo donde el post-reset es **incomparable**
57/// al pre-reset (Addendum §D.1). Dos generaciones distintas no tienen refinamiento
58/// común no trivial: su join colapsa a ⊤ y su meet a ⊥. Ese colapso a ⊤ es la
59/// señal de obstrucción **real** (semántica, no topológica) de la §C.
60#[derive(Debug, Clone, PartialEq, Eq)]
61pub enum ResetVal {
62    /// ⊥.
63    Bottom,
64    /// Un valor concreto en una generación. Comparable solo dentro de su generación.
65    Gen { generation: u64, value: i64 },
66    /// ⊤ (colapso: no hay reconciliación no trivial).
67    Top,
68}
69
70impl PartialOrd for ResetVal {
71    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
72        use ResetVal::*;
73        match (self, other) {
74            (Bottom, Bottom) | (Top, Top) => Some(Ordering::Equal),
75            (Bottom, _) | (_, Top) => Some(Ordering::Less),
76            (_, Bottom) | (Top, _) => Some(Ordering::Greater),
77            (
78                Gen { generation: g1, value: v1 },
79                Gen { generation: g2, value: v2 },
80            ) => {
81                if g1 == g2 {
82                    Some(v1.cmp(v2))
83                } else {
84                    None // generaciones distintas: incomparables
85                }
86            }
87        }
88    }
89}
90
91impl LatticeCell for ResetVal {
92    fn join(&self, other: &Self) -> Self {
93        use ResetVal::*;
94        match (self, other) {
95            (Bottom, x) | (x, Bottom) => x.clone(),
96            (Top, _) | (_, Top) => Top,
97            (
98                Gen { generation: g1, value: v1 },
99                Gen { generation: g2, value: v2 },
100            ) => {
101                if g1 == g2 {
102                    Gen { generation: *g1, value: *v1.max(v2) }
103                } else {
104                    Top // incomparables → colapso
105                }
106            }
107        }
108    }
109
110    fn meet(&self, other: &Self) -> Self {
111        use ResetVal::*;
112        match (self, other) {
113            (Top, x) | (x, Top) => x.clone(),
114            (Bottom, _) | (_, Bottom) => Bottom,
115            (
116                Gen { generation: g1, value: v1 },
117                Gen { generation: g2, value: v2 },
118            ) => {
119                if g1 == g2 {
120                    Gen { generation: *g1, value: *v1.min(v2) }
121                } else {
122                    Bottom
123                }
124            }
125        }
126    }
127
128    fn bottom() -> Self {
129        ResetVal::Bottom
130    }
131    fn top() -> Self {
132        ResetVal::Top
133    }
134}
135
136/// Un mapa de restricción como **conexión de Galois** (Addendum §D): un par
137/// adjunto `(lower, upper)` que reemplaza a la matriz lineal del MVP.
138///
139/// Ley adjunta (monótona): `lower(a) ≤ b  ⟺  a ≤ upper(b)`. De ella se siguen
140/// que `lower` preserva joins y `upper` preserva meets, sin necesidad de restar.
141pub trait GaloisRestriction<A: LatticeCell, B: LatticeCell> {
142    /// `F_{v⊴e}`: sube el estado local a la arista. Preserva joins.
143    fn lower(&self, a: &A) -> B;
144    /// `F_{v⊴e}^*`: la adjunta; baja de la arista al vértice. Preserva meets.
145    fn upper(&self, b: &B) -> A;
146}
147
148/// La conexión de Galois identidad: comparten el mismo dato tal cual.
149#[derive(Debug, Clone, Copy, Default)]
150pub struct IdentityGalois;
151
152impl<L: LatticeCell> GaloisRestriction<L, L> for IdentityGalois {
153    fn lower(&self, a: &L) -> L {
154        a.clone()
155    }
156    fn upper(&self, b: &L) -> L {
157        b.clone()
158    }
159}
160
161/// Conexión de Galois no trivial sobre ℕ: `lower(a) = k·a`, `upper(b) = ⌊b/k⌋`.
162/// Es la adjunción clásica multiplicación/división: `k·a ≤ b ⟺ a ≤ ⌊b/k⌋`.
163#[derive(Debug, Clone, Copy)]
164pub struct ScaleGalois {
165    /// Factor de escala, `k ≥ 1`.
166    pub k: u64,
167}
168
169impl ScaleGalois {
170    /// Crea una escala con `k ≥ 1` (satura en 1 si se pasa 0).
171    pub fn new(k: u64) -> Self {
172        Self { k: k.max(1) }
173    }
174}
175
176impl GaloisRestriction<Nat, Nat> for ScaleGalois {
177    fn lower(&self, a: &Nat) -> Nat {
178        Nat(a.0.saturating_mul(self.k))
179    }
180    fn upper(&self, b: &Nat) -> Nat {
181        Nat(b.0 / self.k)
182    }
183}
184
185#[cfg(test)]
186mod tests {
187    use super::*;
188    use proptest::prelude::*;
189
190    /// Comprueba las cuatro leyes de retículo sobre una terna concreta.
191    fn leyes_de_reticulo<L: LatticeCell + std::fmt::Debug>(a: &L, b: &L, c: &L) {
192        // Conmutatividad.
193        assert_eq!(a.join(b), b.join(a));
194        assert_eq!(a.meet(b), b.meet(a));
195        // Asociatividad.
196        assert_eq!(a.join(b).join(c), a.join(&b.join(c)));
197        assert_eq!(a.meet(b).meet(c), a.meet(&b.meet(c)));
198        // Idempotencia.
199        assert_eq!(a.join(a), a.clone());
200        assert_eq!(a.meet(a), a.clone());
201        // Absorción.
202        assert_eq!(a.join(&a.meet(b)), a.clone());
203        assert_eq!(a.meet(&a.join(b)), a.clone());
204        // Neutros.
205        assert_eq!(a.join(&L::bottom()), a.clone());
206        assert_eq!(a.meet(&L::top()), a.clone());
207    }
208
209    fn nat_st() -> impl Strategy<Value = Nat> {
210        (0u64..10_000).prop_map(Nat)
211    }
212
213    fn reset_st() -> impl Strategy<Value = ResetVal> {
214        prop_oneof![
215            Just(ResetVal::Bottom),
216            Just(ResetVal::Top),
217            (0u64..4, -100i64..100)
218                .prop_map(|(generation, value)| ResetVal::Gen { generation, value }),
219        ]
220    }
221
222    proptest! {
223        #[test]
224        fn nat_es_reticulo(a in nat_st(), b in nat_st(), c in nat_st()) {
225            leyes_de_reticulo(&a, &b, &c);
226        }
227
228        #[test]
229        fn resetval_es_reticulo(a in reset_st(), b in reset_st(), c in reset_st()) {
230            leyes_de_reticulo(&a, &b, &c);
231        }
232
233        /// Generaciones distintas colapsan: su join es ⊤ y su meet es ⊥.
234        #[test]
235        fn reset_incomparable_colapsa(v1 in -100i64..100, v2 in -100i64..100) {
236            let a = ResetVal::Gen { generation: 0, value: v1 };
237            let b = ResetVal::Gen { generation: 1, value: v2 };
238            prop_assert!(a.partial_cmp(&b).is_none(), "gen distintas son incomparables");
239            prop_assert_eq!(a.join(&b), ResetVal::Top);
240            prop_assert_eq!(a.meet(&b), ResetVal::Bottom);
241        }
242
243        /// Ley adjunta de Galois para la identidad: trivial pero debe cumplirse.
244        #[test]
245        fn galois_identidad(a in nat_st(), b in nat_st()) {
246            let g = IdentityGalois;
247            prop_assert_eq!(g.lower(&a) <= b, a <= g.upper(&b));
248        }
249
250        /// Ley adjunta de Galois para la escala k·a ≤ b ⟺ a ≤ ⌊b/k⌋, y
251        /// monotonía de `lower`.
252        #[test]
253        fn galois_escala(a in 0u64..1000, a2 in 0u64..1000, b in 0u64..1000, k in 1u64..8) {
254            let g = ScaleGalois::new(k);
255            let (na, nb) = (Nat(a), Nat(b));
256            prop_assert_eq!(g.lower(&na) <= nb, na <= g.upper(&nb), "ley adjunta");
257            // Monotonía de lower: a ≤ a' ⟹ lower(a) ≤ lower(a').
258            let (lo, hi) = (Nat(a.min(a2)), Nat(a.max(a2)));
259            prop_assert!(g.lower(&lo) <= g.lower(&hi));
260        }
261    }
262}