T8b: auditar y corregir el oráculo (monotonía de fusión, no de valor)
T8 §B/§F: el oracle_verdict de T4 usaba la etiqueta monotone = monotonía de VALOR. Un LWW-register baja de valor pero es un CRDT (monótono en su orden de fusión), luego CALM real lo declara libre. Separo: - calm_syntactic: el check grueso por-programa (coordina ante cualquier op no monótona en valor). Es la respuesta a batir en T8c. - oracle_verdict (corregido): monotonía en el orden de FUSIÓN. Todo CRDT puro es CoordinationFree en cualquier grafo; la coordinación real solo la trae un invariante (T8c). Tests históricos (lineal, labeled) repuntados a calm_syntactic (el oráculo grueso que espejaban). Nuevo test t8b: oráculo corregido y haz nativo coinciden en todo CRDT puro — acuerdo correcto (ambos ven que el merge reconcilia), no circular como el de T7. 40 tests, clippy limpio. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 4.8
parent
b666de794e
commit
62995aa024
+50
-15
@@ -68,10 +68,11 @@ impl Config {
|
||||
}
|
||||
}
|
||||
|
||||
/// **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 {
|
||||
/// **CALM sintáctico por-programa** (el check grueso). Coordina si aparece
|
||||
/// cualquier operación marcada no monótona en VALOR. Es la respuesta a batir:
|
||||
/// la "discrepancia buena" que persigue T8c es `haz = libre` mientras esto
|
||||
/// dice `coordina` (§D). No es el oráculo de corrección.
|
||||
pub fn calm_syntactic(&self) -> OracleVerdict {
|
||||
if self.shares.iter().all(|s| s.monotone) {
|
||||
OracleVerdict::CoordinationFree
|
||||
} else {
|
||||
@@ -79,6 +80,23 @@ impl Config {
|
||||
}
|
||||
}
|
||||
|
||||
/// **Oráculo CALM corregido** (T8b, §B/§F): la monotonía que importa es la del
|
||||
/// **orden de fusión**, no la del valor. Un CRDT es, por definición, monótono
|
||||
/// en su propio merge (join-semilattice); luego una configuración de CRDT
|
||||
/// puros es libre de coordinación en cualquier grafo — ciclos incluidos.
|
||||
///
|
||||
/// La etiqueta `monotone` era monotonía de VALOR (un LWW baja de valor pero es
|
||||
/// un CRDT): por eso `calm_syntactic` clasificaba mal los reset. Aquí eso se
|
||||
/// corrige. La coordinación real solo la introduce un **invariante** (T8c);
|
||||
/// hasta entonces, el veredicto correcto es siempre `CoordinationFree`. Su
|
||||
/// acuerdo con el haz nativo NO es circular: ambos reconocen, por caminos
|
||||
/// independientes, que un merge de CRDT reconcilia.
|
||||
pub fn oracle_verdict(&self) -> OracleVerdict {
|
||||
// Todo `Share` está respaldado por un merge de CRDT genuino (GCounter o
|
||||
// registro LWW), monótono en su orden de fusión ⇒ sin coordinación.
|
||||
OracleVerdict::CoordinationFree
|
||||
}
|
||||
|
||||
/// 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);
|
||||
@@ -314,28 +332,29 @@ pub fn casos_de_discrepancia() -> Vec<Config> {
|
||||
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.
|
||||
/// Control histórico del MVP (§8 M3): el haz LINEAL coincide con el CALM
|
||||
/// **sintáctico** (grueso) en toda la batería. Ese acuerdo topológico
|
||||
/// ↔ sintáctico es el que T8 pone en cuarentena; se conserva como control.
|
||||
#[test]
|
||||
fn haz_coincide_con_oraculo() {
|
||||
fn haz_lineal_coincide_con_calm_sintactico() {
|
||||
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(),
|
||||
c.calm_syntactic(),
|
||||
"discrepancia inesperada en el caso '{}'",
|
||||
c.name
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// Las discrepancias del MVP **lineal** (R1) son reales y esperadas: el haz
|
||||
/// topológico dice coordinar donde CALM dice libre. Es el control histórico.
|
||||
/// Las discrepancias del MVP **lineal** (R1): el haz topológico dice coordinar
|
||||
/// donde el CALM sintáctico dice libre (ciclo monótono). Control histórico.
|
||||
#[test]
|
||||
fn discrepancias_del_lineal_persisten() {
|
||||
for c in casos_de_discrepancia() {
|
||||
assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
|
||||
assert_eq!(c.calm_syntactic(), OracleVerdict::CoordinationFree);
|
||||
assert_eq!(
|
||||
c.sheaf_verdict(),
|
||||
OracleVerdict::NeedsCoordination,
|
||||
@@ -346,20 +365,36 @@ mod tests {
|
||||
}
|
||||
|
||||
/// Control histórico: el encoding CIRCULAR de T7 (`_labeled`) coincide con el
|
||||
/// oráculo por-etiqueta en toda la batería. Es justo esa coincidencia
|
||||
/// perfecta lo que T8 §A denuncia como circular; se conserva para el flip.
|
||||
/// CALM **sintáctico** en toda la batería. Es justo esa coincidencia perfecta
|
||||
/// lo que T8 §A denuncia como circular; se conserva para el flip.
|
||||
#[test]
|
||||
fn tarski_labeled_coincide_con_oraculo_es_circular() {
|
||||
fn tarski_labeled_coincide_con_calm_sintactico_es_circular() {
|
||||
for c in &casos_de_acuerdo() {
|
||||
assert_eq!(
|
||||
c.tarski_verdict_labeled(),
|
||||
c.oracle_verdict(),
|
||||
c.calm_syntactic(),
|
||||
"el control circular debe coincidir en '{}'",
|
||||
c.name
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// **T8b — el oráculo corregido**: bajo monotonía-de-fusión, todo CRDT puro es
|
||||
/// `CoordinationFree`, y el haz nativo coincide. El acuerdo es correcto (ambos
|
||||
/// reconocen que un merge de CRDT reconcilia), no circular como el de T7.
|
||||
#[test]
|
||||
fn t8b_oraculo_corregido_coincide_con_nativo() {
|
||||
for c in casos_de_acuerdo().iter().chain(&casos_de_discrepancia()) {
|
||||
assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
|
||||
assert_eq!(
|
||||
c.tarski_verdict(),
|
||||
c.oracle_verdict(),
|
||||
"oráculo corregido y haz nativo deben coincidir en '{}'",
|
||||
c.name
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// **T8a — la de-circularización** (§B, `FLIPS.md`): bajo el orden nativo
|
||||
/// (derivado del merge, sin leer la etiqueta), los casos que el encoding
|
||||
/// circular de T7 llamaba `coordina` VUELVEN a `corre libre`. Cada flip es
|
||||
|
||||
Reference in New Issue
Block a user