gioser

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.

Rust 24Markdown 15TOML 1358 Definiciones

⎇ main src/verdict.rs Rust · 192 líneas · 7.1 KB Historia Quién tocó qué crudo

T9a: invariante global + certificado de escrow 89c62aa71 · Sergio ·

1//! `verdict` — traducción del resultado topológico a lenguaje de sistemas (§6.5).
2//!
3//! `H¹ = 0 → corre libre` vs `H¹ ≠ 0 → coordina aquí`, con localización.
4
5use std::collections::BTreeSet;
6use std::fmt;
7
8use crate::cohomology::Cohomology;
9use crate::escrow::SpendResult;
10use crate::lattice::{GaloisRestriction, LatticeCell};
11use crate::nerve::ReplicaId;
12use crate::sheaf::Sheaf;
13use crate::tarski::{LatticeSheaf, TarskiLaplacian};
14
15/// Umbral para considerar no nula una componente del vector de obstrucción.
16const SUPPORT_EPS: f64 = 1e-9;
17
18/// Un nudo: una obstrucción localizada entre réplicas/aristas concretas.
19#[derive(Debug, Clone, PartialEq)]
20pub struct Knot {
21    /// Réplicas implicadas en el nudo.
22    pub replicas: Vec<ReplicaId>,
23    /// Aristas del ciclo obstruido (índices en el nervio).
24    pub edges: Vec<usize>,
25}
26
27/// El veredicto final en lenguaje de sistemas.
28#[derive(Debug, Clone, PartialEq)]
29pub enum Verdict {
30    /// `H¹ = 0`: fusión libre de coordinación.
31    RunsFree,
32    /// `H¹ ≠ 0`: hace falta coordinar, con los nudos localizados.
33    NeedsCoordination {
34        /// Los nudos detectados (uno por generador del cokernel).
35        knots: Vec<Knot>,
36    },
37}
38
39impl Verdict {
40    /// Diagnostica la configuración a partir del haz y su cohomología.
41    ///
42    /// Si `H¹ = 0` → `RunsFree`. Si no, cada vector de la base del cokernel es un
43    /// nudo independiente: las aristas con soporte no nulo lo forman, y sus
44    /// extremos son las réplicas implicadas (§7 paso 5).
45    pub fn diagnose(sheaf: &Sheaf, coho: &Cohomology) -> Verdict {
46        if coho.dim_h1 == 0 {
47            return Verdict::RunsFree;
48        }
49
50        // Offsets de cada arista dentro de C¹ (donde vive el vector de obstrucción).
51        let mut edge_offsets = Vec::with_capacity(sheaf.edge_stalks.len());
52        let mut acc = 0;
53        for &d in &sheaf.edge_stalks {
54            edge_offsets.push(acc);
55            acc += d;
56        }
57
58        let mut knots = Vec::new();
59        for basis_vec in &coho.obstruction_basis {
60            let mut edges = Vec::new();
61            let mut replicas = BTreeSet::new();
62            for (e, (&off, &d)) in edge_offsets.iter().zip(&sheaf.edge_stalks).enumerate() {
63                let touches = basis_vec[off..off + d].iter().any(|x| x.abs() > SUPPORT_EPS);
64                if touches {
65                    edges.push(e);
66                    let (u, v) = sheaf.edge_endpoints[e];
67                    replicas.insert(u);
68                    replicas.insert(v);
69                }
70            }
71            knots.push(Knot {
72                replicas: replicas.into_iter().map(ReplicaId).collect(),
73                edges,
74            });
75        }
76
77        Verdict::NeedsCoordination { knots }
78    }
79
80    /// Diagnostica por **difusión de Tarski** sobre un haz de retículos
81    /// (Addendum §C, T7): se harmoniza la siembra a punto fijo y se lee.
82    ///
83    /// - **RunsFree** si el punto fijo reconcilia sin colapsar: ninguna arista
84    ///   queda en ⊤ y ningún vértice colapsa. La difusión preserva lo local.
85    /// - **NeedsCoordination** si hay colapso a ⊤: obstrucción semántica real.
86    ///   La localización (R-L1, difusa) son las aristas cuyo desacuerdo
87    ///   *sobrevive* al punto fijo, y sus réplicas.
88    pub fn via_tarski<L, R>(sheaf: &LatticeSheaf<L, R>, seed: &[L]) -> Verdict
89    where
90        L: LatticeCell + PartialEq,
91        R: GaloisRestriction<L, L>,
92    {
93        let harm = TarskiLaplacian::new(sheaf).harmonize(seed);
94        let top = L::top();
95        let r = &sheaf.restriction;
96
97        let mut edges = Vec::new();
98        let mut replicas = BTreeSet::new();
99        // Aristas cuyo desacuerdo sobrevive al punto fijo (colapsan a ⊤).
100        for (i, &(a, b)) in sheaf.edges.iter().enumerate() {
101            if r.lower(&harm[a]).join(&r.lower(&harm[b])) == top {
102                edges.push(i);
103                replicas.insert(a);
104                replicas.insert(b);
105            }
106        }
107        // Vértices colapsados a ⊤ (por si un colapso no dejara arista superviviente).
108        for (v, h) in harm.iter().enumerate() {
109            if *h == top {
110                replicas.insert(v);
111            }
112        }
113
114        if replicas.is_empty() {
115            Verdict::RunsFree
116        } else {
117            Verdict::NeedsCoordination {
118                knots: vec![Knot {
119                    replicas: replicas.into_iter().map(ReplicaId).collect(),
120                    edges,
121                }],
122            }
123        }
124    }
125
126    /// Veredicto por **escrow** (T9, §D/§E): un gasto dentro de presupuesto es
127    /// `Local` → `RunsFree` (cero coordinación, correcto **incluso particionado**);
128    /// agotarlo pide un **rebalanceo edge-local** → `NeedsCoordination` localizado
129    /// en la réplica seca. NUNCA declara "libre global" a ciegas (mata el punto
130    /// ciego de T8). Las aristas del rebalanceo las rellena el `BudgetRouter` (T9b).
131    pub fn via_escrow(replica: usize, spend: &SpendResult) -> Verdict {
132        match spend {
133            SpendResult::Local => Verdict::RunsFree,
134            SpendResult::NeedsRebalance { .. } => Verdict::NeedsCoordination {
135                knots: vec![Knot {
136                    replicas: vec![ReplicaId(replica)],
137                    edges: Vec::new(),
138                }],
139            },
140        }
141    }
142}
143
144impl fmt::Display for Verdict {
145    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
146        match self {
147            Verdict::RunsFree => write!(f, "H¹ = 0 → corre libre (sin jefe)"),
148            Verdict::NeedsCoordination { knots } => {
149                write!(f, "H¹ ≠ 0 → coordina aquí")?;
150                for knot in knots {
151                    let reps: Vec<usize> = knot.replicas.iter().map(|r| r.0).collect();
152                    write!(f, "\n    · nudo entre réplicas {reps:?} (aristas {:?})", knot.edges)?;
153                }
154                Ok(())
155            }
156        }
157    }
158}
159
160#[cfg(test)]
161mod tests {
162    use super::*;
163    use crate::cohomology::compute_with;
164    use crate::gf2::Gf2Backend;
165
166    #[test]
167    fn arbol_corre_libre() {
168        let sheaf = Sheaf::constant(3, &[(0, 1), (1, 2)], 1);
169        let coho = compute_with(&sheaf, &Gf2Backend).unwrap();
170        assert_eq!(Verdict::diagnose(&sheaf, &coho), Verdict::RunsFree);
171    }
172
173    #[test]
174    fn dos_triangulos_reportan_dos_nudos() {
175        // Dos triángulos que comparten la arista (1,2): b₁ = 2 → dos ciclos
176        // obstruidos, luego dos nudos (uno por generador del cokernel).
177        let edges = [(0, 1), (0, 2), (1, 2), (1, 3), (2, 3)];
178        let sheaf = Sheaf::constant(4, &edges, 1);
179        let coho = compute_with(&sheaf, &Gf2Backend).unwrap();
180        match Verdict::diagnose(&sheaf, &coho) {
181            Verdict::NeedsCoordination { knots } => {
182                assert_eq!(knots.len(), 2, "todos los ciclos obstruidos, no solo uno");
183                // Cada nudo es un ciclo real: al menos 3 aristas y 3 réplicas.
184                for k in &knots {
185                    assert!(k.edges.len() >= 3);
186                    assert!(k.replicas.len() >= 3);
187                }
188            }
189            Verdict::RunsFree => panic!("dos ciclos deberían obstruir"),
190        }
191    }
192}