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.
Rust 24Markdown 15TOML 1358 Definitions
T4/M3: oráculo CRDT/CALM, batería de validación y DISCREPANCIES
- oracle: Config/Share, oracle_verdict (CALM independiente: free ⟺ toda
op compartida monótona), to_sheaf (codificación honesta: reset → 2-ciclo
en conflicto), sheaf_verdict (H¹ vía GF(2)).
- Batería casos_de_acuerdo() (21 casos ≥20) + test maestro: el haz coincide
con el oráculo en todo el régimen de acuerdo.
- casos_de_discrepancia() + test: datos monótonos sobre grafo cíclico donde
el haz ve una falsa obstrucción topológica (Hipótesis H falla, dirección
conservadora). Documentado en DISCREPANCIES.md — el 'oro científico' de R1.
- tests/properties.rs (proptest, §9): (1) monótono sobre bosque → H¹=0,
(2) añadir arista no reduce H¹ ni aumenta H⁰, (3) haz constante reproduce
los números de Betti (H⁰=componentes, H¹=E−V+C) sobre grafos aleatorios.
24 tests pasan (incl. 3 propiedades), clippy limpio. Cierra el MVP: M0–M3.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
diff --git a/DISCREPANCIES.md b/DISCREPANCIES.md
new file mode 100644
index 0000000..c1ec23d
--- /dev/null
+++ b/DISCREPANCIES.md
@@ -0,0 +1,65 @@
+# Discrepancias haz ↔ oráculo CALM
+
+Registro de los casos donde el veredicto cohomológico (`H¹`) **no** coincide con
+el oráculo CRDT/CALM. Como dice el SDD (§8, §11 R1), esto no es un bug a esconder:
+es el resultado científico del proyecto — dónde y por qué la Hipótesis H (§2.2)
+se rompe bajo la codificación lineal del MVP.
+
+Reproducibles con el test `oracle::tests::discrepancias_conocidas_persisten` y los
+casos de `oracle::casos_de_discrepancia()`.
+
+## Resumen
+
+| Caso | Oráculo (CALM) | Haz (`H¹`) | ¿Coinciden? |
+|---|---|---|---|
+| `triangulo-monotono` | corre libre | `H¹ = 1` → coordina | ❌ |
+| `cuadrado-monotono` | corre libre | `H¹ = 1` → coordina | ❌ |
+| (general) dato **monótono** sobre grafo de compartición **cíclico** | corre libre | `H¹ = b₁ ≠ 0` | ❌ |
+
+En cambio, **coinciden** en todo el régimen de `oracle::casos_de_acuerdo()`
+(≥20 casos): sharing monótono acíclico y cualquier configuración con al menos
+una operación no monótona.
+
+## La discrepancia, en detalle
+
+**El caso.** Tres réplicas comparten un dato **monótono** (p.ej. un `GCounter`)
+en un triángulo: 0—1, 1—2, 2—0. Todas las operaciones son monótonas.
+
+**Qué dice CALM (oráculo).** Un `GCounter` se funde por máximo casilla a casilla;
+el join siempre existe y es único. No hay operación que retracte conocimiento,
+luego la configuración es **coordination-free**. El ciclo en el grafo de
+compartición es irrelevante: más caminos para difundir la misma información
+monótona no crean un conflicto.
+
+**Qué dice el haz.** La codificación lineal del MVP modela cada dato compartido
+como una restricción de **acuerdo** (identidad). Sobre el triángulo, el haz
+constante tiene `dim H¹ = b₁ = E − V + C = 3 − 3 + 1 = 1`. El motor reporta una
+obstrucción y pide coordinar.
+
+**Por qué ocurre (§2.3, R1).** La cohomología de haces es **lineal**; los
+retículos de los CRDTs son **de orden** (join-semilattices). Al aplanar el orden
+a álgebra lineal, el haz pierde la información de que la fusión monótona *siempre*
+pega las secciones locales. Lo que le queda es la topología pura del grafo, y la
+topología de un ciclo tiene `H¹ ≠ 0` con independencia de los datos. El haz
+"ve" así una obstrucción **topológica** donde CALM no ve ninguna **semántica**.
+
+Dicho de otro modo: bajo esta codificación, `H¹ = 0 ⟺ el grafo de compartición
+es acíclico`, un enunciado **puramente topológico** que solo coincide con CALM
+cuando el ciclo, de existir, transporta una operación no monótona (y por eso la
+codificación honesta añade un segundo enlace en conflicto solo en ese caso).
+
+## Consecuencia para la Hipótesis H
+
+La Hipótesis H (`H¹ = 0 ⟺ coordination-free`) **se sostiene** en el MVP para
+configuraciones cuyo sharing monótono es acíclico, y **falla** para datos
+monótonos sobre grafos cíclicos. La dirección que falla es conservadora: el haz
+pide coordinación de más (falsos positivos), nunca de menos. No hemos observado
+el fallo inverso (haz dice "libre" donde CALM dice "coordina").
+
+## Camino de salida (fuera del MVP, §2.3 / §11 Q2)
+
+La cura propuesta por el diseño es abandonar los haces valuados en espacios
+vectoriales y pasar a **haces valuados en retículos / posets** (la generalización
+"de Tarski"), donde la fusión monótona es parte de la estructura y no se pierde al
+linealizar. Ahí un ciclo de acuerdos monótonos debería tener obstrucción trivial.
+Es la extensión de investigación sin fecha del plan de hitos.
diff --git a/src/oracle.rs b/src/oracle.rs
index e88996e..426abc0 100644
--- a/src/oracle.rs
+++ b/src/oracle.rs
@@ -1,10 +1,13 @@
//! `oracle` — evaluador CRDT/CALM de referencia, independiente del haz (§8 M3).
//!
-//! Para cada caso de prueba dice, por un camino independiente (monotonicidad de
-//! las operaciones + estructura del grafo), si es coordination-free. El test
-//! maestro de M3 comprueba que el veredicto del haz coincide con este.
-//!
-//! M0: solo la forma. La batería de ≥20 casos y la lógica llegan en T4.
+//! Para cada configuración el oráculo dice, por CALM puro (monotonicidad de las
+//! operaciones compartidas), si es coordination-free — sin mirar el haz. El test
+//! maestro compara ese veredicto con el del haz para validar la Hipótesis H
+//! (§2.2). Donde discrepan (§11 R1) se documenta en `DISCREPANCIES.md`.
+
+use crate::cohomology::compute_with;
+use crate::gf2::Gf2Backend;
+use crate::sheaf::Sheaf;
/// Predicción independiente del oráculo para una configuración.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -14,3 +17,253 @@ pub enum OracleVerdict {
/// El oráculo cree que hace falta coordinar.
NeedsCoordination,
}
+
+/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
+/// que lo toca es monótona.
+#[derive(Debug, Clone, Copy)]
+pub struct Share {
+ /// Primera réplica que comparte.
+ pub a: usize,
+ /// Segunda réplica que comparte.
+ pub b: usize,
+ /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
+ pub monotone: bool,
+}
+
+impl Share {
+ /// Dato compartido monótono (se funde solo).
+ pub fn monotona(a: usize, b: usize) -> Self {
+ Self { a, b, monotone: true }
+ }
+
+ /// Dato compartido no monótono (reset/overwrite → posible conflicto).
+ pub fn no_monotona(a: usize, b: usize) -> Self {
+ Self { a, b, monotone: false }
+ }
+}
+
+/// Una configuración de réplicas con sus datos compartidos.
+#[derive(Debug, Clone)]
+pub struct Config {
+ /// Nombre del caso (para reportes).
+ pub name: String,
+ /// Número de réplicas.
+ pub replicas: usize,
+ /// Datos compartidos.
+ pub shares: Vec<Share>,
+}
+
+impl Config {
+ /// Construye una configuración.
+ pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
+ Self {
+ name: name.into(),
+ replicas,
+ shares,
+ }
+ }
+
+ /// **Oráculo CALM (independiente del haz).** Coordination-free ⟺ toda
+ /// operación compartida es monótona. En cuanto aparece una no monótona
+ /// compartida, CALM exige coordinación.
+ pub fn oracle_verdict(&self) -> OracleVerdict {
+ if self.shares.iter().all(|s| s.monotone) {
+ OracleVerdict::CoordinationFree
+ } else {
+ OracleVerdict::NeedsCoordination
+ }
+ }
+
+ /// Codificación lineal de la configuración como haz (la codificación honesta
+ /// de la §2.3, sin colapsar ciclos monótonos):
+ /// - cada dato compartido → una arista de acuerdo (restricción identidad);
+ /// - una operación no monótona añade un segundo enlace en conflicto sobre el
+ /// mismo par → un 2-ciclo localizado (como la Corrida B de M1).
+ pub fn to_sheaf(&self) -> Sheaf {
+ let mut edges = Vec::new();
+ for s in &self.shares {
+ edges.push((s.a, s.b));
+ if !s.monotone {
+ edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
+ }
+ }
+ Sheaf::constant(self.replicas, &edges, 1)
+ }
+
+ /// **Veredicto del haz.** Coordination-free ⟺ `H¹ = 0`. Usa la aritmética
+ /// exacta `GF(2)`.
+ pub fn sheaf_verdict(&self) -> OracleVerdict {
+ let sheaf = self.to_sheaf();
+ let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
+ if coho.dim_h1 == 0 {
+ OracleVerdict::CoordinationFree
+ } else {
+ OracleVerdict::NeedsCoordination
+ }
+ }
+}
+
+/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
+///
+/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
+/// cualquier configuración con al menos una operación no monótona (→ ambos
+/// "coordina"). El test maestro verifica la coincidencia en todos.
+pub fn casos_de_acuerdo() -> Vec<Config> {
+ let mut casos = Vec::new();
+
+ // --- Monótonos acíclicos → CoordinationFree ---
+ // Caminos de longitud creciente.
+ for k in 2..=10 {
+ let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
+ casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
+ }
+ // Estrella (centro 0, hojas 1..=4).
+ casos.push(Config::new(
+ "estrella-monotona",
+ 5,
+ (1..=4).map(|h| Share::monotona(0, h)).collect(),
+ ));
+ // Árbol binario.
+ casos.push(Config::new(
+ "arbol-binario-monotono",
+ 5,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(0, 2),
+ Share::monotona(1, 3),
+ Share::monotona(1, 4),
+ ],
+ ));
+ // Bosque desconexo (dos árboles).
+ casos.push(Config::new(
+ "bosque-monotono",
+ 5,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(1, 2),
+ Share::monotona(3, 4),
+ ],
+ ));
+ // Réplicas sin compartir nada (trivialmente libre).
+ casos.push(Config::new("aislado", 3, vec![]));
+
+ // --- Con operación no monótona → NeedsCoordination ---
+ // Par único con reset.
+ casos.push(Config::new(
+ "par-no-monotono",
+ 2,
+ vec![Share::no_monotona(0, 1)],
+ ));
+ // Camino monótono con un reset en un tramo (localiza el nudo ahí).
+ for reset_edge in 0..3 {
+ let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
+ shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
+ casos.push(Config::new(
+ format!("camino-con-reset-en-{reset_edge}"),
+ 4,
+ shares,
+ ));
+ }
+ // Dos resets independientes en partes distintas.
+ casos.push(Config::new(
+ "dos-resets-separados",
+ 4,
+ vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
+ ));
+ // Estrella monótona con una hoja reseteada.
+ casos.push(Config::new(
+ "estrella-con-reset",
+ 5,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(0, 2),
+ Share::monotona(0, 3),
+ Share::no_monotona(0, 4),
+ ],
+ ));
+ // Árbol grande con reset en una rama.
+ casos.push(Config::new(
+ "arbol-con-reset",
+ 6,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(1, 2),
+ Share::monotona(2, 3),
+ Share::monotona(1, 4),
+ Share::no_monotona(4, 5),
+ ],
+ ));
+ // Todo no monótono.
+ casos.push(Config::new(
+ "todo-reset",
+ 3,
+ vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
+ ));
+
+ casos
+}
+
+/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
+/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
+/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
+/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
+pub fn casos_de_discrepancia() -> Vec<Config> {
+ vec![
+ Config::new(
+ "triangulo-monotono",
+ 3,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(1, 2),
+ Share::monotona(2, 0),
+ ],
+ ),
+ Config::new(
+ "cuadrado-monotono",
+ 4,
+ vec![
+ Share::monotona(0, 1),
+ Share::monotona(1, 2),
+ Share::monotona(2, 3),
+ Share::monotona(3, 0),
+ ],
+ ),
+ ]
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ /// Test maestro (§8 M3): el veredicto del haz coincide con el del oráculo en
+ /// toda la batería de acuerdo, que tiene ≥20 casos.
+ #[test]
+ fn haz_coincide_con_oraculo() {
+ let casos = casos_de_acuerdo();
+ assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
+ for c in &casos {
+ assert_eq!(
+ c.sheaf_verdict(),
+ c.oracle_verdict(),
+ "discrepancia inesperada en el caso '{}'",
+ c.name
+ );
+ }
+ }
+
+ /// Las discrepancias conocidas (R1) son reales y esperadas: el haz dice
+ /// coordinar donde CALM dice libre. Si esto dejara de discrepar, la
+ /// codificación habría cambiado y hay que revisar `DISCREPANCIES.md`.
+ #[test]
+ fn discrepancias_conocidas_persisten() {
+ for c in casos_de_discrepancia() {
+ assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
+ assert_eq!(
+ c.sheaf_verdict(),
+ OracleVerdict::NeedsCoordination,
+ "el ciclo monótono '{}' debería producir una falsa obstrucción",
+ c.name
+ );
+ }
+ }
+}
diff --git a/tests/properties.rs b/tests/properties.rs
new file mode 100644
index 0000000..f5c552a
--- /dev/null
+++ b/tests/properties.rs
@@ -0,0 +1,115 @@
+//! Invariantes basadas en propiedades (§9), que `proptest` intenta romper.
+//!
+//! Tres invariantes:
+//! 1. Solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0`.
+//! 2. Añadir una arista: `H¹` no decrece y `H⁰` no crece.
+//! 3. El haz constante reproduce los números de Betti del grafo.
+//!
+//! La invariante 1 se acota a **bosques** a propósito: sobre grafos cíclicos la
+//! codificación lineal ve la obstrucción topológica aunque el dato sea monótono
+//! (§11 R1) — esa discrepancia está documentada, no es un bug.
+
+use proptest::prelude::*;
+use sheafsync::cohomology::compute_with;
+use sheafsync::gf2::Gf2Backend;
+use sheafsync::oracle::{Config, OracleVerdict, Share};
+use sheafsync::sheaf::Sheaf;
+
+/// `(dim H⁰, dim H¹)` del haz constante `d=1` sobre `(n, edges)`.
+fn coho(n: usize, edges: &[(usize, usize)]) -> (usize, usize) {
+ let sheaf = Sheaf::constant(n, edges, 1);
+ let c = compute_with(&sheaf, &Gf2Backend).unwrap();
+ (c.dim_h0, c.dim_h1)
+}
+
+/// Número de componentes conexas por union-find.
+fn componentes(n: usize, edges: &[(usize, usize)]) -> usize {
+ let mut parent: Vec<usize> = (0..n).collect();
+ fn find(parent: &mut [usize], x: usize) -> usize {
+ let mut r = x;
+ while parent[r] != r {
+ r = parent[r];
+ }
+ // compresión de caminos
+ let mut c = x;
+ while parent[c] != c {
+ let next = parent[c];
+ parent[c] = r;
+ c = next;
+ }
+ r
+ }
+ for &(a, b) in edges {
+ let ra = find(&mut parent, a);
+ let rb = find(&mut parent, b);
+ if ra != rb {
+ parent[ra] = rb;
+ }
+ }
+ (0..n).filter(|&x| find(&mut parent, x) == x).count()
+}
+
+/// Grafo aleatorio: `n` vértices y una lista de aristas (posibles multiaristas).
+fn grafo() -> impl Strategy<Value = (usize, Vec<(usize, usize)>)> {
+ (2usize..=6).prop_flat_map(|n| {
+ let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
+ (Just(n), prop::collection::vec(arista, 0..10))
+ })
+}
+
+/// Grafo aleatorio más una arista extra dentro del mismo rango de vértices.
+fn grafo_y_arista() -> impl Strategy<Value = (usize, Vec<(usize, usize)>, (usize, usize))> {
+ (2usize..=6).prop_flat_map(|n| {
+ let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
+ (Just(n), prop::collection::vec(arista.clone(), 0..10), arista)
+ })
+}
+
+proptest! {
+ /// Invariante 3: haz constante ⟹ `H⁰ = #componentes`, `H¹ = E − V + C`.
+ #[test]
+ fn haz_constante_reproduce_betti((n, edges) in grafo()) {
+ let (h0, h1) = coho(n, &edges);
+ let c = componentes(n, &edges);
+ let e = edges.len();
+ prop_assert_eq!(h0, c, "H⁰ debe contar componentes");
+ // E − V + C ≥ 0 siempre; lo calculamos sin subdesbordar.
+ prop_assert_eq!(h1 + n, e + c, "H¹ debe ser el primer número de Betti");
+ }
+
+ /// Invariante 2: añadir una arista no reduce `H¹` ni aumenta `H⁰`.
+ #[test]
+ fn anadir_arista_no_reduce_h1_ni_aumenta_h0((n, edges, extra) in grafo_y_arista()) {
+ let (h0, h1) = coho(n, &edges);
+ let mut mas = edges.clone();
+ mas.push(extra);
+ let (h0b, h1b) = coho(n, &mas);
+ prop_assert!(h1b >= h1, "H¹ no debe decrecer al añadir una arista");
+ prop_assert!(h0b <= h0, "H⁰ no debe crecer al añadir una arista");
+ }
+
+ /// Invariante 1: solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0` y el
+ /// oráculo y el haz coinciden en "corre libre".
+ #[test]
+ fn monotono_sobre_bosque_corre_libre((n, edges) in grafo()) {
+ // Quedarnos solo con las aristas que conectan componentes nuevas → bosque.
+ let mut parent: Vec<usize> = (0..n).collect();
+ fn find(parent: &mut [usize], x: usize) -> usize {
+ let mut r = x;
+ while parent[r] != r { r = parent[r]; }
+ r
+ }
+ let mut bosque = Vec::new();
+ for (a, b) in edges {
+ let ra = find(&mut parent, a);
+ let rb = find(&mut parent, b);
+ if ra != rb {
+ parent[ra] = rb;
+ bosque.push(Share::monotona(a, b));
+ }
+ }
+ let config = Config::new("bosque-aleatorio", n, bosque);
+ prop_assert_eq!(config.oracle_verdict(), OracleVerdict::CoordinationFree);
+ prop_assert_eq!(config.sheaf_verdict(), OracleVerdict::CoordinationFree);
+ }
+}