tawasuyu/hifas
Motor en Rust para decidir, con demostración y no a ojo, cuándo un conjunto de réplicas local-first puede operar sin coordinación y cuándo no — y, cuando la respuesta es "sí, dentro de límites", proveer el mecanismo que lo garantiza.
T4/M3: oráculo CRDT/CALM, batería de validación y DISCREPANCIES
1//! `oracle` — evaluador CRDT/CALM de referencia, independiente del haz (§8 M3).
2//!
3//! Para cada configuración el oráculo dice, por CALM puro (monotonicidad de las
4//! operaciones compartidas), si es coordination-free — sin mirar el haz. El test
5//! maestro compara ese veredicto con el del haz para validar la Hipótesis H
6//! (§2.2). Donde discrepan (§11 R1) se documenta en `DISCREPANCIES.md`.
7
8use crate::cohomology::compute_with;
9use crate::gf2::Gf2Backend;
10use crate::sheaf::Sheaf;
11
12/// Predicción independiente del oráculo para una configuración.
13#[derive(Debug, Clone, Copy, PartialEq, Eq)]
14pub enum OracleVerdict {
15 /// El oráculo cree que la configuración es libre de coordinación.
16 CoordinationFree,
17 /// El oráculo cree que hace falta coordinar.
18 NeedsCoordination,
19}
20
21/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
22/// que lo toca es monótona.
23#[derive(Debug, Clone, Copy)]
24pub struct Share {
25 /// Primera réplica que comparte.
26 pub a: usize,
27 /// Segunda réplica que comparte.
28 pub b: usize,
29 /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
30 pub monotone: bool,
31}
32
33impl Share {
34 /// Dato compartido monótono (se funde solo).
35 pub fn monotona(a: usize, b: usize) -> Self {
36 Self { a, b, monotone: true }
37 }
38
39 /// Dato compartido no monótono (reset/overwrite → posible conflicto).
40 pub fn no_monotona(a: usize, b: usize) -> Self {
41 Self { a, b, monotone: false }
42 }
43}
44
45/// Una configuración de réplicas con sus datos compartidos.
46#[derive(Debug, Clone)]
47pub struct Config {
48 /// Nombre del caso (para reportes).
49 pub name: String,
50 /// Número de réplicas.
51 pub replicas: usize,
52 /// Datos compartidos.
53 pub shares: Vec<Share>,
54}
55
56impl Config {
57 /// Construye una configuración.
58 pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
59 Self {
60 name: name.into(),
61 replicas,
62 shares,
63 }
64 }
65
66 /// **Oráculo CALM (independiente del haz).** Coordination-free ⟺ toda
67 /// operación compartida es monótona. En cuanto aparece una no monótona
68 /// compartida, CALM exige coordinación.
69 pub fn oracle_verdict(&self) -> OracleVerdict {
70 if self.shares.iter().all(|s| s.monotone) {
71 OracleVerdict::CoordinationFree
72 } else {
73 OracleVerdict::NeedsCoordination
74 }
75 }
76
77 /// Codificación lineal de la configuración como haz (la codificación honesta
78 /// de la §2.3, sin colapsar ciclos monótonos):
79 /// - cada dato compartido → una arista de acuerdo (restricción identidad);
80 /// - una operación no monótona añade un segundo enlace en conflicto sobre el
81 /// mismo par → un 2-ciclo localizado (como la Corrida B de M1).
82 pub fn to_sheaf(&self) -> Sheaf {
83 let mut edges = Vec::new();
84 for s in &self.shares {
85 edges.push((s.a, s.b));
86 if !s.monotone {
87 edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
88 }
89 }
90 Sheaf::constant(self.replicas, &edges, 1)
91 }
92
93 /// **Veredicto del haz.** Coordination-free ⟺ `H¹ = 0`. Usa la aritmética
94 /// exacta `GF(2)`.
95 pub fn sheaf_verdict(&self) -> OracleVerdict {
96 let sheaf = self.to_sheaf();
97 let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
98 if coho.dim_h1 == 0 {
99 OracleVerdict::CoordinationFree
100 } else {
101 OracleVerdict::NeedsCoordination
102 }
103 }
104}
105
106/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
107///
108/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
109/// cualquier configuración con al menos una operación no monótona (→ ambos
110/// "coordina"). El test maestro verifica la coincidencia en todos.
111pub fn casos_de_acuerdo() -> Vec<Config> {
112 let mut casos = Vec::new();
113
114 // --- Monótonos acíclicos → CoordinationFree ---
115 // Caminos de longitud creciente.
116 for k in 2..=10 {
117 let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
118 casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
119 }
120 // Estrella (centro 0, hojas 1..=4).
121 casos.push(Config::new(
122 "estrella-monotona",
123 5,
124 (1..=4).map(|h| Share::monotona(0, h)).collect(),
125 ));
126 // Árbol binario.
127 casos.push(Config::new(
128 "arbol-binario-monotono",
129 5,
130 vec![
131 Share::monotona(0, 1),
132 Share::monotona(0, 2),
133 Share::monotona(1, 3),
134 Share::monotona(1, 4),
135 ],
136 ));
137 // Bosque desconexo (dos árboles).
138 casos.push(Config::new(
139 "bosque-monotono",
140 5,
141 vec![
142 Share::monotona(0, 1),
143 Share::monotona(1, 2),
144 Share::monotona(3, 4),
145 ],
146 ));
147 // Réplicas sin compartir nada (trivialmente libre).
148 casos.push(Config::new("aislado", 3, vec![]));
149
150 // --- Con operación no monótona → NeedsCoordination ---
151 // Par único con reset.
152 casos.push(Config::new(
153 "par-no-monotono",
154 2,
155 vec![Share::no_monotona(0, 1)],
156 ));
157 // Camino monótono con un reset en un tramo (localiza el nudo ahí).
158 for reset_edge in 0..3 {
159 let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
160 shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
161 casos.push(Config::new(
162 format!("camino-con-reset-en-{reset_edge}"),
163 4,
164 shares,
165 ));
166 }
167 // Dos resets independientes en partes distintas.
168 casos.push(Config::new(
169 "dos-resets-separados",
170 4,
171 vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
172 ));
173 // Estrella monótona con una hoja reseteada.
174 casos.push(Config::new(
175 "estrella-con-reset",
176 5,
177 vec![
178 Share::monotona(0, 1),
179 Share::monotona(0, 2),
180 Share::monotona(0, 3),
181 Share::no_monotona(0, 4),
182 ],
183 ));
184 // Árbol grande con reset en una rama.
185 casos.push(Config::new(
186 "arbol-con-reset",
187 6,
188 vec![
189 Share::monotona(0, 1),
190 Share::monotona(1, 2),
191 Share::monotona(2, 3),
192 Share::monotona(1, 4),
193 Share::no_monotona(4, 5),
194 ],
195 ));
196 // Todo no monótono.
197 casos.push(Config::new(
198 "todo-reset",
199 3,
200 vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
201 ));
202
203 casos
204}
205
206/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
207/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
208/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
209/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
210pub fn casos_de_discrepancia() -> Vec<Config> {
211 vec![
212 Config::new(
213 "triangulo-monotono",
214 3,
215 vec![
216 Share::monotona(0, 1),
217 Share::monotona(1, 2),
218 Share::monotona(2, 0),
219 ],
220 ),
221 Config::new(
222 "cuadrado-monotono",
223 4,
224 vec![
225 Share::monotona(0, 1),
226 Share::monotona(1, 2),
227 Share::monotona(2, 3),
228 Share::monotona(3, 0),
229 ],
230 ),
231 ]
232}
233
234#[cfg(test)]
235mod tests {
236 use super::*;
237
238 /// Test maestro (§8 M3): el veredicto del haz coincide con el del oráculo en
239 /// toda la batería de acuerdo, que tiene ≥20 casos.
240 #[test]
241 fn haz_coincide_con_oraculo() {
242 let casos = casos_de_acuerdo();
243 assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
244 for c in &casos {
245 assert_eq!(
246 c.sheaf_verdict(),
247 c.oracle_verdict(),
248 "discrepancia inesperada en el caso '{}'",
249 c.name
250 );
251 }
252 }
253
254 /// Las discrepancias conocidas (R1) son reales y esperadas: el haz dice
255 /// coordinar donde CALM dice libre. Si esto dejara de discrepar, la
256 /// codificación habría cambiado y hay que revisar `DISCREPANCIES.md`.
257 #[test]
258 fn discrepancias_conocidas_persisten() {
259 for c in casos_de_discrepancia() {
260 assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
261 assert_eq!(
262 c.sheaf_verdict(),
263 OracleVerdict::NeedsCoordination,
264 "el ciclo monótono '{}' debería producir una falsa obstrucción",
265 c.name
266 );
267 }
268 }
269}