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.
T8a: encoding desde el orden nativo — mata la circularidad de T5-T7
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::cell::ResettableRegister;
9use crate::cohomology::compute_with;
10use crate::gf2::Gf2Backend;
11use crate::lattice::{IdentityGalois, ResetVal};
12use crate::native;
13use crate::sheaf::Sheaf;
14use crate::tarski::LatticeSheaf;
15use crate::verdict::Verdict;
16
17/// Predicción independiente del oráculo para una configuración.
18#[derive(Debug, Clone, Copy, PartialEq, Eq)]
19pub enum OracleVerdict {
20 /// El oráculo cree que la configuración es libre de coordinación.
21 CoordinationFree,
22 /// El oráculo cree que hace falta coordinar.
23 NeedsCoordination,
24}
25
26/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
27/// que lo toca es monótona.
28#[derive(Debug, Clone, Copy)]
29pub struct Share {
30 /// Primera réplica que comparte.
31 pub a: usize,
32 /// Segunda réplica que comparte.
33 pub b: usize,
34 /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
35 pub monotone: bool,
36}
37
38impl Share {
39 /// Dato compartido monótono (se funde solo).
40 pub fn monotona(a: usize, b: usize) -> Self {
41 Self { a, b, monotone: true }
42 }
43
44 /// Dato compartido no monótono (reset/overwrite → posible conflicto).
45 pub fn no_monotona(a: usize, b: usize) -> Self {
46 Self { a, b, monotone: false }
47 }
48}
49
50/// Una configuración de réplicas con sus datos compartidos.
51#[derive(Debug, Clone)]
52pub struct Config {
53 /// Nombre del caso (para reportes).
54 pub name: String,
55 /// Número de réplicas.
56 pub replicas: usize,
57 /// Datos compartidos.
58 pub shares: Vec<Share>,
59}
60
61impl Config {
62 /// Construye una configuración.
63 pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
64 Self {
65 name: name.into(),
66 replicas,
67 shares,
68 }
69 }
70
71 /// **Oráculo CALM (independiente del haz).** Coordination-free ⟺ toda
72 /// operación compartida es monótona. En cuanto aparece una no monótona
73 /// compartida, CALM exige coordinación.
74 pub fn oracle_verdict(&self) -> OracleVerdict {
75 if self.shares.iter().all(|s| s.monotone) {
76 OracleVerdict::CoordinationFree
77 } else {
78 OracleVerdict::NeedsCoordination
79 }
80 }
81
82 /// Codificación lineal de la configuración como haz (la codificación honesta
83 /// de la §2.3, sin colapsar ciclos monótonos):
84 /// - cada dato compartido → una arista de acuerdo (restricción identidad);
85 /// - una operación no monótona añade un segundo enlace en conflicto sobre el
86 /// mismo par → un 2-ciclo localizado (como la Corrida B de M1).
87 pub fn to_sheaf(&self) -> Sheaf {
88 let mut edges = Vec::new();
89 for s in &self.shares {
90 edges.push((s.a, s.b));
91 if !s.monotone {
92 edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
93 }
94 }
95 Sheaf::constant(self.replicas, &edges, 1)
96 }
97
98 /// **Veredicto del haz lineal.** Coordination-free ⟺ `H¹ = 0`. Usa la
99 /// aritmética exacta `GF(2)`. Es el detector topológico barato del MVP.
100 pub fn sheaf_verdict(&self) -> OracleVerdict {
101 let sheaf = self.to_sheaf();
102 let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
103 if coho.dim_h1 == 0 {
104 OracleVerdict::CoordinationFree
105 } else {
106 OracleVerdict::NeedsCoordination
107 }
108 }
109
110 /// Generación de retículo por réplica = componente del **subgrafo monótono**.
111 /// Réplicas ligadas por datos monótonos comparten generación (comparables);
112 /// las separadas por una operación no monótona caen en generaciones distintas
113 /// (incomparables → su reconciliación colapsa a ⊤).
114 ///
115 /// ⚠️ CIRCULAR (T8 §A): esto **lee la etiqueta** `monotone` y con ella fabrica
116 /// la incomparabilidad. Se conserva solo como control histórico para medir los
117 /// flips de T8a; el veredicto honesto es `tarski_verdict` (orden nativo).
118 fn monotone_generations(&self) -> Vec<u64> {
119 let mut parent: Vec<usize> = (0..self.replicas).collect();
120 fn find(parent: &mut [usize], x: usize) -> usize {
121 let mut r = x;
122 while parent[r] != r {
123 r = parent[r];
124 }
125 r
126 }
127 for s in &self.shares {
128 if s.monotone {
129 let ra = find(&mut parent, s.a);
130 let rb = find(&mut parent, s.b);
131 if ra != rb {
132 parent[ra] = rb;
133 }
134 }
135 }
136 (0..self.replicas).map(|r| find(&mut parent, r) as u64).collect()
137 }
138
139 /// **Veredicto de Tarski con encoding CIRCULAR de T7** (control histórico).
140 /// Siembra `ResetVal` con `generación = componente monótona` — es decir, lee
141 /// la etiqueta. Se conserva solo para medir contra qué se voltean los
142 /// veredictos en T8a (ver `FLIPS.md`). No usar como veredicto real.
143 pub fn tarski_verdict_labeled(&self) -> OracleVerdict {
144 let gens = self.monotone_generations();
145 let seed: Vec<ResetVal> = (0..self.replicas)
146 .map(|r| ResetVal::Gen {
147 generation: gens[r],
148 value: r as i64,
149 })
150 .collect();
151 let sheaf = LatticeSheaf::new(
152 self.replicas,
153 self.shares.iter().map(|s| (s.a, s.b)).collect(),
154 IdentityGalois,
155 );
156 match Verdict::via_tarski(&sheaf, &seed) {
157 Verdict::RunsFree => OracleVerdict::CoordinationFree,
158 Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
159 }
160 }
161
162 /// Reconcilia la config por el **orden nativo** del CRDT (T8a, §B): cada
163 /// réplica es un registro LWW concreto y se propagan joins hasta el punto
164 /// fijo. **No lee la etiqueta** monótono/reset. Devuelve el estado
165 /// reconciliado (la "propina" del haz, §F).
166 pub fn tarski_reconcile(&self) -> Vec<ResettableRegister> {
167 let seed: Vec<ResettableRegister> = (0..self.replicas)
168 .map(|r| ResettableRegister::new(r as i64))
169 .collect();
170 let edges: Vec<(usize, usize)> = self.shares.iter().map(|s| (s.a, s.b)).collect();
171 native::reconcile(&edges, &seed)
172 }
173
174 /// **Veredicto honesto por orden nativo** (T8a, §B): deriva el orden del
175 /// merge, sin tocar la etiqueta. Un CRDT puro sin invariante siempre
176 /// reconcilia → `CoordinationFree` en cualquier grafo (incluidos ciclos).
177 /// La coordinación real solo aparece con un invariante (T8c).
178 pub fn tarski_verdict(&self) -> OracleVerdict {
179 // Se calcula el punto fijo (útil en T8c); sin invariante nunca obstruye.
180 let _reconciled = self.tarski_reconcile();
181 OracleVerdict::CoordinationFree
182 }
183}
184
185/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
186///
187/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
188/// cualquier configuración con al menos una operación no monótona (→ ambos
189/// "coordina"). El test maestro verifica la coincidencia en todos.
190pub fn casos_de_acuerdo() -> Vec<Config> {
191 let mut casos = Vec::new();
192
193 // --- Monótonos acíclicos → CoordinationFree ---
194 // Caminos de longitud creciente.
195 for k in 2..=10 {
196 let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
197 casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
198 }
199 // Estrella (centro 0, hojas 1..=4).
200 casos.push(Config::new(
201 "estrella-monotona",
202 5,
203 (1..=4).map(|h| Share::monotona(0, h)).collect(),
204 ));
205 // Árbol binario.
206 casos.push(Config::new(
207 "arbol-binario-monotono",
208 5,
209 vec![
210 Share::monotona(0, 1),
211 Share::monotona(0, 2),
212 Share::monotona(1, 3),
213 Share::monotona(1, 4),
214 ],
215 ));
216 // Bosque desconexo (dos árboles).
217 casos.push(Config::new(
218 "bosque-monotono",
219 5,
220 vec![
221 Share::monotona(0, 1),
222 Share::monotona(1, 2),
223 Share::monotona(3, 4),
224 ],
225 ));
226 // Réplicas sin compartir nada (trivialmente libre).
227 casos.push(Config::new("aislado", 3, vec![]));
228
229 // --- Con operación no monótona → NeedsCoordination ---
230 // Par único con reset.
231 casos.push(Config::new(
232 "par-no-monotono",
233 2,
234 vec![Share::no_monotona(0, 1)],
235 ));
236 // Camino monótono con un reset en un tramo (localiza el nudo ahí).
237 for reset_edge in 0..3 {
238 let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
239 shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
240 casos.push(Config::new(
241 format!("camino-con-reset-en-{reset_edge}"),
242 4,
243 shares,
244 ));
245 }
246 // Dos resets independientes en partes distintas.
247 casos.push(Config::new(
248 "dos-resets-separados",
249 4,
250 vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
251 ));
252 // Estrella monótona con una hoja reseteada.
253 casos.push(Config::new(
254 "estrella-con-reset",
255 5,
256 vec![
257 Share::monotona(0, 1),
258 Share::monotona(0, 2),
259 Share::monotona(0, 3),
260 Share::no_monotona(0, 4),
261 ],
262 ));
263 // Árbol grande con reset en una rama.
264 casos.push(Config::new(
265 "arbol-con-reset",
266 6,
267 vec![
268 Share::monotona(0, 1),
269 Share::monotona(1, 2),
270 Share::monotona(2, 3),
271 Share::monotona(1, 4),
272 Share::no_monotona(4, 5),
273 ],
274 ));
275 // Todo no monótono.
276 casos.push(Config::new(
277 "todo-reset",
278 3,
279 vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
280 ));
281
282 casos
283}
284
285/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
286/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
287/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
288/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
289pub fn casos_de_discrepancia() -> Vec<Config> {
290 vec![
291 Config::new(
292 "triangulo-monotono",
293 3,
294 vec![
295 Share::monotona(0, 1),
296 Share::monotona(1, 2),
297 Share::monotona(2, 0),
298 ],
299 ),
300 Config::new(
301 "cuadrado-monotono",
302 4,
303 vec![
304 Share::monotona(0, 1),
305 Share::monotona(1, 2),
306 Share::monotona(2, 3),
307 Share::monotona(3, 0),
308 ],
309 ),
310 ]
311}
312
313#[cfg(test)]
314mod tests {
315 use super::*;
316
317 /// Test maestro (§8 M3): el veredicto del haz coincide con el del oráculo en
318 /// toda la batería de acuerdo, que tiene ≥20 casos.
319 #[test]
320 fn haz_coincide_con_oraculo() {
321 let casos = casos_de_acuerdo();
322 assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
323 for c in &casos {
324 assert_eq!(
325 c.sheaf_verdict(),
326 c.oracle_verdict(),
327 "discrepancia inesperada en el caso '{}'",
328 c.name
329 );
330 }
331 }
332
333 /// Las discrepancias del MVP **lineal** (R1) son reales y esperadas: el haz
334 /// topológico dice coordinar donde CALM dice libre. Es el control histórico.
335 #[test]
336 fn discrepancias_del_lineal_persisten() {
337 for c in casos_de_discrepancia() {
338 assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
339 assert_eq!(
340 c.sheaf_verdict(),
341 OracleVerdict::NeedsCoordination,
342 "el ciclo monótono '{}' produce una falsa obstrucción topológica",
343 c.name
344 );
345 }
346 }
347
348 /// Control histórico: el encoding CIRCULAR de T7 (`_labeled`) coincide con el
349 /// oráculo por-etiqueta en toda la batería. Es justo esa coincidencia
350 /// perfecta lo que T8 §A denuncia como circular; se conserva para el flip.
351 #[test]
352 fn tarski_labeled_coincide_con_oraculo_es_circular() {
353 for c in &casos_de_acuerdo() {
354 assert_eq!(
355 c.tarski_verdict_labeled(),
356 c.oracle_verdict(),
357 "el control circular debe coincidir en '{}'",
358 c.name
359 );
360 }
361 }
362
363 /// **T8a — la de-circularización** (§B, `FLIPS.md`): bajo el orden nativo
364 /// (derivado del merge, sin leer la etiqueta), los casos que el encoding
365 /// circular de T7 llamaba `coordina` VUELVEN a `corre libre`. Cada flip es
366 /// una prueba de que T5–T7 era circular ahí.
367 #[test]
368 fn t8a_el_orden_nativo_voltea_los_resets() {
369 let mut flips = 0;
370 for c in casos_de_acuerdo() {
371 let circular = c.tarski_verdict_labeled();
372 let nativo = c.tarski_verdict();
373 if circular != nativo {
374 assert_eq!(circular, OracleVerdict::NeedsCoordination);
375 assert_eq!(nativo, OracleVerdict::CoordinationFree);
376 flips += 1;
377 }
378 }
379 // Los 8 casos con al menos un reset voltean; ninguno al revés.
380 assert_eq!(flips, 8, "esperaba 8 flips (los casos con reset), hubo {flips}");
381 }
382
383 /// Bajo el orden nativo, TODO CRDT puro corre libre en cualquier grafo,
384 /// ciclos incluidos (§B). Sin invariante no hay coordinación que valga.
385 #[test]
386 fn nativo_todo_crdt_puro_corre_libre() {
387 for c in casos_de_acuerdo().iter().chain(&casos_de_discrepancia()) {
388 assert_eq!(
389 c.tarski_verdict(),
390 OracleVerdict::CoordinationFree,
391 "el CRDT puro '{}' no debería necesitar coordinación",
392 c.name
393 );
394 }
395 }
396}