1# SDD 15 — Frontera AI-nativa: código por contenido, evidencia sobre confianza, cómputo como dato
2
3> Estado: propuesta (2026-07-02). Nace de una revisión externa de las 4 piezas del stack
4> (wawa · hammer/BLAKE3 · wasm determinista · hifas) que propuso seis puentes. Tres caen del
5> lado de hammer/wawa y se recogen aquí; los otros tres (fuente monótona en el kernel,
6> fork-consistency, OS-como-CRDT) viven en `tawasuyu/03_ukupacha/PLAN-OS-CRDT.md`.
7>
8> **Este doc NO reemplaza nada cerrado.** Fases 0–6 + bootstrap Stage 0–2 + los 6 swaps
9> reproducibles siguen siendo la base (ver `docs/10-roadmap.md`). Esto es *frontera*: apuestas
10> ordenadas de "extensión natural de lo que ya hacemos" a "otro modelo de datos, design-doc".
11
12---
13
14## 0. El principio que ya tenemos y hay que empujar
15
16El modelo de confianza de hammer (SDD 09) es **"verificar, no confiar"**: el binario ajeno
17nunca viaja, viaja la receta, y `hammer apply` **reproduce y compara** el `expected_hash`. La
18integración de IA (SDD 08 §4) es exactamente la arquitectura de frontera correcta: *la IA
19propone `.swm`; el sistema reproduce; el humano hace commit; la IA nunca promueve sola.*
20
21La revisión externa nombra esto bien: **la frontera de confianza no está en quien genera sino
22en quien verifica.** Las tres ideas de abajo *empujan esa misma frontera* a territorio nuevo,
23sin moverla de sitio. Ninguna pide confiar más en el modelo; todas piden **verificar más**.
24
25Nota de higiene (de la propia revisión, adoptada): nada aquí es "matemáticamente invulnerable".
26Es "verificado bajo supuestos nombrados" — reproducibilidad bajo toolchain fijado, determinismo
27del sandbox, el checker es pequeño y auditable. seL4 se formula así; nosotros también.
28
29---
30
31## H1 — Proof-carrying recipes: de "reproduce" a "trae evidencia que pasa" (la idea 4)
32
33**Qué ya hacemos.** El bucle agéntico (SDD 08 §2) es PLAN → BUILD → TRY → **VERIFY** → PROPOSE
34→ humano. Hoy VERIFY = "corre el test harness, escucha `BUILD_FAILED`/`CRASHED`". La garantía
35dura es **reproducibilidad**: dos máquinas ⇒ mismo `artifact_hash`. Eso certifica *identidad*,
36no *comportamiento*.
37
38**El salto.** Que la IA entregue, junto al `.swm`, **evidencia de comportamiento**: property
39tests, contratos, y —cuando el crate lo permita— pruebas tipo Kani/Creusot. hammer admite la
40mutación sólo si un **checker pequeño y confiable** confirma que la evidencia pasa. Proof-carrying
41code (Necula 1997), pero **el generador es un modelo**: el sistema mejora solo sin poder
42corromperse solo, porque la confianza vive en el checker, no en el generador.
43
44**Por qué encaja aquí y no en otro lado.** hammer ya tiene el sandbox hermético (bwrap) donde
45correr esa evidencia de forma reproducible, ya tiene el `Orchestrator` con paso VERIFY, y ya
46tiene procedencia (`.hammer/recipe.toml` sellado en el artefacto). La atestación por-hash de
47arje (concesiones matcheadas por hash de binario; ver `tawasuyu` `arje/SDD`) es el mismo patrón
48del lado del init: **el permiso deriva de una propiedad verificada del artefacto, no de quién lo
49firmó.** H1 es esa idea, subida del boot al build.
50
51**Tickets:**
52- **H1a** ✅ — Extender el `.swm` (SDD 06) con un bloque `evidence`: lista de `{kind, cmd, expected}`
53  donde `kind ∈ {proptest, contract, kani, cmd-exit}`. Serialización YAML estable + `verify_schema`.
54- **H1b** ✅ — El checker: `hammer swm-verify --evidence` corre cada ítem **dentro del sandbox
55  reproducible** y exige `expected`. Pequeño y auditable a propósito (no un framework: un runner
56  de comandos con hash del output). Falla ⇒ no se propone. Reusa `Sandbox::run` + el `log_tail`
57  ya existente (Fase 5).
58- **H1c** ✅ — Cablear al `Orchestrator`: VERIFY consume `evidence`; el `Proposal` lleva el
59  **veredicto de evidencia** además del diff. El humano ve "reproduce + estas N pruebas pasan",
60  no sólo "reproduce". **Frontera:** el checker confía en que las pruebas *cubren* lo que
61  importa — eso lo juzga el humano; H1 garantiza que *lo declarado pasa*, no que *lo declarado
62  basta*. Se dice así.
63  **Implementación:** la evidencia corre del lado del BUILD (no del agente — `hammer-agent` no
64  depende de `hammer-build`, separación PROPONE/CONSTRUYE). `proto::RecipeInline` lleva `evidence`
65  y `Event::BuildReady` lleva `verdict: Option<EvidenceVerdict>`; `hammerd::bus` la ejecuta tras
66  sellar el artefacto (`run_evidence` vía `swm_bridge::recipe_from_source_patch`) y adjunta el
67  veredicto; el `Orchestrator` lee el veredicto y, si `all_passed=false`, empuja `VerifyCheck::fail`
68  y **aborta antes de hidratar** (el artefacto queda sellado pero no toca el sistema).
69
70**Frontera honesta.** Property tests no son prueba; Kani/Creusot sí pero sólo cubren crates que
71se dejan. H1 **estratifica** la confianza (`cmd-exit` < `proptest` < `contract` < `kani`) y la
72reporta; no finge que todo es prueba formal.
73
74---
75
76## H2 — Cómputo como dato: memoización de ejecución sobre wasm determinista (la idea 5)
77
78**La observación.** Si wawa ejecuta wasm **determinista**, entonces
79`blake3(módulo) + blake3(entrada) → blake3(salida)` es una **función pura**. Nix memoiza
80*builds* por hash de entrada; esto memoiza **ejecución en runtime**. La caché de resultados es
81content-addressed y **compartible por la malla** vía la capa CRDT de
82`tawasuyu/shared/crdt` (es un `GSet`/`LwwMap` de `(módulo,entrada) → salida`, monótono ⇒ viaja
83por anti-entropy sin coordinar).
84
85**Los tres regalos gratis** que la revisión nombra bien:
861. **Caché global de cómputo** — la malla comparte resultados; un cómputo caro se hace una vez.
872. **Replay perfecto** — depuración con viaje en el tiempo: un proceso *es* su módulo + su log
88   de entradas (gancho directo con el `MonotonicLog` de PLAN-OS-CRDT E1).
893. **Migración de procesos como transferencia de datos** — mover un proceso = copiar `(módulo,
90   log de entradas)` y re-ejecutar; el estado se reconstruye determinísticamente.
91
92**El gancho con hammer.** La caché es un **recurso acotado ruteable**: `hifas::router`
93(`BudgetRouter`) reparte "créditos de cómputo" por la malla (PLAN-OS-CRDT E3c). Y la
94verificación de un resultado memoizado es *reproducir la ejecución* — el mismo "verificar, no
95confiar" de SDD 09, ahora sobre runtime en vez de build.
96
97**Precondición dura (la apuesta).** Requiere **determinismo total de wasm en wawa**: sin
98`float` no determinista, sin fuentes de entropía ocultas, orden de scheduling irrelevante para
99la salida. `wasmi` es determinista para el core, pero hay que **auditar y sellar** que ninguna
100capacidad expuesta (tiempo, random, I/O) filtre no-determinismo a la salida hasheada. Eso es un
101spike de wawa, no de hammer.
102
103**Tickets (spike, no fase):**
104- **H2a** ✅ — Auditar determinismo del runtime wasm de wawa: enumerar toda fuente de no-determinismo
105  alcanzable por una app (`wawa-kernel/src/wasm/`), y definir el subconjunto "puro" (módulo +
106  entrada explícita, sin syscalls no deterministas). Salida: un doc `wawa/SDD` §determinismo con
107  el veredicto honesto (qué es puro, qué no).
108  **Hecho (2026-07-03):** `tawasuyu/03_ukupacha/wawa/SDD-determinismo.md`. Veredicto: el subconjunto
109  puro **ya existe** en el código (`ejecutar_dinamico`/`_v2`, `wasm/mod.rs:335,430` — linker VACÍO +
110  reloj virtual + fuel/memoria fijos + wasmi 1.0 sin simd). H2a no era construirlo sino **sellarlo**:
111  contrato de clave `blake3(módulo)⊕blake3(entrada)⊕E` con `E` = hash-de-entorno (pin wasmi/features/
112  fuel/mem/ABI); único vector residual acotado = payload de NaN vía `reinterpret` (sólo cross-build,
113  irrelevante para H2b local). La superficie de capacidades (`env/*.rs`) reintroduce no-determinismo
114  o efectos ⇒ NO memoizable; sólo la vía linker-vacío lo es.
115- **H2b** ✅ — Prototipo de `blake3(módulo)+blake3(entrada) → blake3(salida)` como caché local
116  (un `LwwMap` de `shared/crdt`), sin malla todavía. Test: misma entrada ⇒ hit; recompute ⇒
117  byte-idéntico (o el determinismo está roto y H2a mintió).
118  **Hecho (2026-07-03):** crate `tawasuyu/03_ukupacha/wawa/wawa-memo` (host/std, standalone).
119  Reproduce fiel la vía pura del kernel (`ejecutar_dinamico_v2`: linker vacío + fuel 500k + 1 MiB
120  + wasmi sin simd + despacho polimórfico) y monta la clave del contrato §4 (`blake3(bytecode) ‖
121  blake3(entrada_le) ‖ E`, con `E` = hash de entorno que pinnea wasmi/features/fuel/mem/abi). El
122  test de §5 **da verde**: 9 módulos × 8 entradas ejecutados dos veces ⇒ `blake3(salida)`
123  byte-idéntico (H2a no mintió); Miss→Hit sirve valor idéntico al recomputado; las fallas
124  (`Trampa`/`SinCombustible`/`Carga`) se cachean (§4 regla 4); `E` distinta ⇒ clave distinta (§4
125  regla 2); y dos réplicas convergen al fundir el `LwwMap` (anti-entropy, preview de H2c). Como la
126  clave es content-addressed y la función pura, el LWW nunca tiene conflicto real ⇒ el mapa es
127  monótono y compartible sin coordinar. **Verde ⇒ H2c desbloqueado** (compartir por la malla).
128- **H2c** — (si H2b pasa) compartir la caché por la malla minga/agora. Frontera: envenenamiento
129  de caché por un peer ⇒ se **verifica reproduciendo** en el primer uso dudoso (no se confía en
130  el resultado ajeno; se confía en poder recomputarlo). Es el modelo de confianza de SDD 09
131  aplicado a runtime.
132  **Núcleo de confianza hecho (2026-07-03, en `wawa-memo`):** dos piezas que hacen *seguro* el
133  compartir, independientes del transporte. (1) **Sellado de portabilidad** (`sellado.rs`, §4
134  regla 3a): un escáner conservador del bytecode clasifica cada módulo `Portable` (enteros puros
135  ⇒ sin vector NaN ⇒ idéntico cross-arch) o `SoloLocal` (toca floats / no decodifica). Decodifica
136  los inmediatos correctamente (no confunde un `i32.const 0xBC` con el opcode `reinterpret_f32`).
137  (2) **Modelo de confianza** (`malla.rs`): `ingerir_ajeno` **verifica reproduciendo** una entrada
138  ofrecida por un peer y **rechaza** la envenenada (afirmar `Ok(99)` donde `cuadrado(6)=36`, o `Ok`
139  donde hay `Trampa`) — nunca entra a la caché local; el valor correcto sigue recomputable. Política
140  `ConfiarSiPortable` = optimización que confía sin recomputar sólo módulos `Portable` (descarta el
141  vector NaN, no la deshonestidad del peer — dicho explícito). **Diferido (es del otro agente):** el
142  transporte real (anti-entropy sobre minga/agora) vive en `PLAN-OS-CRDT.md` (E3). Tests: `h2c.rs`.
143
144**Frontera honesta.** Sin determinismo total (H2a), H2 no existe — es la apuesta. No prometer
145la caché de malla antes de que H2a dé verde. Y "cómputo puro" excluye lo interesante-con-I/O:
146la memoización cubre la parte funcional, no el proceso entero con efectos.
147
148---
149
150## H3 — Código direccionado por contenido estilo Unison (la idea 3) — DESIGN-DOC, no sprint
151
152**La visión.** Hoy hammer direcciona por hash el **artefacto** (binario) y la **receta**. wawa
153direcciona el **módulo wasm** y el **almacenamiento**. La idea 3 empuja al límite: direccionar
154**funciones por el hash de su AST** (Unison). La IA no editaría archivos —insertaría
155definiciones en una base content-addressed donde **nada se rompe por renombrar o actualizar**—
156y el store de hammer, los módulos wasm de wawa y el código fuente **colapsarían en un solo
157espacio de nombres: el hash**. Paquete, función y proceso = el mismo tipo de objeto.
158
159**Por qué es design-doc y no ticket.** Es **otro modelo de datos**, no una extensión. hammer y
160Unison content-addressan *cosas distintas*: hammer el artefacto compilado (grano grueso,
161lenguaje-agnóstico, encaja con "recetas sobre fuente upstream"); Unison el AST de cada función
162(grano fino, requiere un lenguaje y toolchain propios). Colapsarlos pide reescribir la unidad de
163compilación entera. El valor es real (fin del dependency-hell para la IA) pero el costo es un
164proyecto, no una fase.
165
166**Qué SÍ hacer ahora (el puente barato hacia la visión):**
167- **H3a** ✅ — Doc de diseño `docs/adr/0009-content-addressed-code.md` (2026-07-03): registra la
168  visión Unison y decide **no reescribir la unidad de compilación**. Puente barato = procedencia
169  por-símbolo como **metadata** (extender `parse_elf_needed`, `query.rs:298`, para emitir exports de
170  `.dynsym` además de `DT_NEEDED`), fuera de `hash_inputs` (misma disciplina que la evidencia de H1).
171  El grano fino real (función-por-hash) se difiere a H3b sobre **wasm**, gateado por H2.
172- **H3b** ✅ — (exploratorio) Base content-addressed de funciones **wasm** (grano: un `.wasm` por
173  función pura de H2), verificando si "insertar definición, nunca romper" se sostiene sobre el
174  runtime de wawa. Es el subconjunto de Unison que el stack *ya* soporta (wasm + BLAKE3 +
175  determinismo H2), sin un lenguaje nuevo.
176  **Hecho (2026-07-04, en `wawa-memo/src/base.rs` + `tests/h3b.rs`):** el módulo `base` monta la
177  `Base` content-addressed sobre el grano de H2. Cuatro propiedades Unison, todas verificadas
178  (8 tests verdes): **(1) identidad = `blake3(bytecode)`** — `definir` es idempotente y deduplica
179  (structural sharing); **(2) los nombres humanos son metadata separada** (`nombre → Id`) — nombrar
180  jamás toca `defs`; **(3) actualizar no rompe** (el corazón) — una referencia es un `Termino::Ref(Id)`,
181  un hash; "actualizar f" = insertar def nueva (hash nuevo) + rebindear el nombre, y todo lo que
182  apuntaba al hash viejo **evalúa idéntico** (v1 y v2 coexisten, ninguna se sobreescribe); **(4)
183  composición por hash** — un programa es un árbol de hashes (`Termino::Componer`), su identidad
184  `blake3(árbol)` es estable e **independiente del mapa de nombres**. Extras: una referencia
185  colgante **falla con `Carga` sin mentir** (el hash no se resuelve en silencio a otra cosa), las
186  fallas deterministas de H2 se propagan por la composición, y **evaluar reusa el `Memo`** (cada
187  hoja `Ref` se memoiza) — código direccionado por contenido + cómputo direccionado por contenido
188  = el mismo hash, la tesis de §H3 mostrada en pequeño. **Frontera:** NO es Unison entero (sin
189  grano intra-función, sin typechecking sobre la base, sin lenguaje); es el *subconjunto* que
190  wasm + BLAKE3 + H2 sostienen. Demuestra que el modelo **se sostiene**, no que hayamos colapsado
191  paquete = función = proceso (eso sigue siendo el design-doc de H3a).
192  **Puente H3b↔H2c (2026-07-04, `wawa-memo/src/programa.rs` + `tests/h3b_malla.rs`, 8 tests):**
193  cierra la tesis de §H3 uniendo el código-por-contenido de H3b con el modelo de confianza de H2c.
194  Un programa entero viaja por la malla como un `Paquete { defs, termino }` **seguro por
195  construcción**, en dos capas que tapan vectores distintos: **(1) integridad del código = el
196  hash** (nueva) — las defs no llevan hash declarado, su identidad se **deriva** al recibirlas;
197  una `Ref(H)` sólo se satisface con los bytes exactos que hashean a `H`, así que alterar o retener
198  una def deja su referencia colgante y **rechaza el paquete** sin firmar nada (el hash ES la
199  prueba de integridad; la base local queda intacta); **(2) verdad del resultado = reproducción**
200  (H2c sobre un programa entero) — que el código sea íntegro no dice qué computa, así que una
201  salida afirmada se **recomputa y compara** (`ingerir_paquete_verificando`), rechazando la
202  envenenada. `verificar_paquete` es la primitiva pura. Compartir *código* es tamper-evident por el
203  hash; compartir *resultados* es seguro por reproducción — juntos, la foto completa de «el hash es
204  el espacio de nombres común».
205
206- **H3c** ✅ — (exploratorio) **El grano intra-función: el linker de contenido** (2026-07-05,
207  `wawa-memo/src/enlace.rs` + `tests/h3c.rs`, 10 tests; 40 verdes en el crate). H3b dejó las
208  definiciones *opacas*: una función wasm no podía llamar a otra — la composición vivía sólo en el
209  árbol (`Termino::Componer`), fuera del bytecode. H3c mete la dependencia **dentro**: una
210  definición importa a otra **por hash** (`import "base" "h:<blake3-hex>"`), y el linker la
211  satisface únicamente con los bytes de la `Base` que hashean exacto a ese `Id` — el contrato de
212  `Termino::Ref`, ahora intra-bytecode. Consecuencias verificadas:
213  **(1) el Merkle-DAG de código** — el hash del callee está embebido en el bytecode del caller ⇒
214  la identidad del caller pinnea transitivamente el DAG entero; la dependencia ENTRA a la
215  identidad; **(2) actualizar no rompe, transitivamente** — «actualizar g» = def nueva + rebind;
216  toda f que embebía `h(g_v1)` sigue llamando los bytes exactos de siempre (v1/v2 coexisten);
217  **(3) los ciclos son imposibles por criptografía**, no por disciplina — un ciclo exigiría un
218  hash que depende del hash que lo contiene (invertir BLAKE3); el DAG es DAG por construcción,
219  idéntico a Unison; **(4) la memoización subsume el DAG** — la clave del compuesto
220  (`blake3(bytecode) ⊕ entrada ⊕ E`) ya cubre sus deps; un cierre INCOMPLETO jamás se cachea (el
221  colgante es un hecho de la base local, no del bytecode — cachearlo envenenaría réplicas);
222  `E` distingue el linker (`vacio` vs `base-v1`) para que los espacios de claves no colisionen;
223  **(5) los paquetes de malla llevan el cierre transitivo** — retener/alterar una dep profunda
224  (a dos aristas del árbol) tumba la ingesta con `RefColgante`, y la portabilidad del compuesto
225  hereda el veredicto más conservador de su DAG (`clasificar_cierre`). Política honesta: cada
226  subllamada corre en instancia fresca con fuel completo (pin en `E`); el presupuesto compuesto
227  no está acotado globalmente — suficiente para el *modelo*, no para un sandbox de producción.
228  Con H3c, de las dos ambiciones abiertas de H3 queda demostrado el **grano intra-función** (en
229  su forma wasm: función llama función por hash); lo aún abierto es el **colapso total**
230  paquete = función = proceso (el lado "proceso" = replay del MonotonicLog, plan OS-CRDT).
231  **Formato de viaje + checker standalone (2026-07-05, `wawa-memo` `formato.rs` +
232  `bin/wawa-verifica`, 5 tests; 45 en el crate):** el `Paquete` deja de ser sólo-memoria.
233  Serialización **canónica** versionada (`WAWA-PAQ1`): biyección bytes↔paquete (defs ordenadas
234  por Id, término con la misma serialización estructural que define su identidad, parseo
235  estricto — toda corrupción es un error determinista, nunca "mejor esfuerzo") ⇒
236  `blake3(bytes) = id_paquete` estable, la identidad del paquete entero en el mismo espacio de
237  nombres. Disciplina intacta: los bytes NO llevan hashes declarados — **el formato transporta,
238  el hash prueba** (la ingesta deriva identidades y rechaza el byte flipeado con `RefColgante`).
239  `wawa-verifica <paquete.wawa> <entrada> <esperado>` es el checker pequeño y auditable
240  (estilo H1) de la afirmación «este paquete con esta entrada produce este resultado»: exit
241  0/1/2 — ejecutable como evidencia `cmd-exit` en el sandbox de hammer (un `.swm` cuyo payload
242  es un programa wasm verificable = el puente concreto paquete↔función) o como gate de ingesta
243  de un peer. El transporte real (anti-entropy) sigue siendo del plan OS-CRDT.
244
245**Frontera honesta.** No prometer "una distro donde paquete = función = proceso": H3b+H3c
246demostraron el núcleo del modelo (definir por hash, nombres como metadata, actualizar sin romper
247— ahora también transitivo —, componer por hash *fuera y dentro* del bytecode) sobre wasm, no el
248colapso total ni el grano sub-función (el AST interno de una función sigue siendo opaco: el átomo
249es la función-módulo, no la expresión). Es la idea más disruptiva; su núcleo ya está verde, su
250ambición máxima sigue abierta.
251
252---
253
254## H4 — Configuraciones compartidas: compatibles, completas y seguras (la aplicación)
255
256**De dónde sale.** No de la revisión externa: del **uso**. Un usuario modifica su
257sistema; cada configuración suya es un *conjunto de modificaciones*. Quiere compartirlas
258por la malla y, al **buscar** una ajena, saber si puede adoptarla — que sea **compatible,
259completa y segura**. H4 aterriza toda la maquinaria de H2/H3 sobre ese caso concreto.
260
261**La observación que lo hace tratable.** "Compatible" parece semántica difusa, pero el
262usuario lo definió con dos ejemplos que el modelo trata **mecánicamente distinto**:
263
264- *Logo.* Ya cambié el logo; bajo una config que **también** cambia el logo. No es un
265  error: ambas **escriben la misma superficie** con contenido distinto. La resolución es
266  una **elección**, no un rechazo.
267- *Wayland.* Modifiqué el protocolo de Wayland; bajo algo que **depende de** el Wayland
268  stock. Su dependencia **no resuelve** contra mi versión ⇒ incompatible.
269
270Entonces "compatible" = **colisión sobre la misma superficie**, y son dos cosas: colisión
271de *escritura* (elección) y dependencia *insatisfecha* (rechazo). El eje nuevo que H4
272agrega es un **espacio de nombres de slots** que cada modificación **reclama** (escribe,
273`slot → Id`) y **requiere** (depende, `slot → Id` a una versión exacta). Con esos dos
274conjuntos, compatible queda **definido de forma dura**, y sus dos mitades **reusan
275primitivas ya verdes**:
276
277| propiedad del usuario | qué la garantiza | dónde (ya construido) |
278|---|---|---|
279| **segura** | verificar reproduciendo — rechaza el resultado envenenado | `verificar_paquete` (H2c) |
280| **completa** | cierre transitivo presente — sin referencia colgante | `ingerir_paquete` (H3c) |
281| **compatible** | requisitos resueltos + reclamos disjuntos | **H4, nuevo** |
282
283La definición dura de compatibilidad de una config `C` contra mi estado `E`:
284
285> (1) **Requisitos** (caso wayland): `∀ (slot, id) ∈ C.requiere : E[slot] = id`. Un slot que
286>     resuelve a otra versión (o falta) es **incompatible** — el análogo de sistema a la
287>     `RefColgante` de H3c: una superficie requerida que resuelve a otros bytes.
288> (2) **Reclamos** (caso logo): `∀ slot ∈ C.reclama : E[slot]` ausente **o** igual en `Id`.
289>     Un slot ya ocupado por otro contenido es **colisión = elección**, no error.
290
291**Tickets:**
292- **H4a** ✅ — (prototipo, `wawa-memo/src/compat.rs` + `tests/h4.rs`, 7 tests; **52 verdes**
293  en el crate) El modelo de slots corriendo. `Config { reclama, requiere }` sobre el mismo
294  espacio de hashes que H3; `evaluar(estado, config) → Veredicto ∈ {Compatible, Colision,
295  Incompatible}` es el chequeo **local y reproducible** ("verificar, no confiar" de SDD 09,
296  ahora sobre la topología de superficies). Verificado: el caso **logo** da `Colision` (y la
297  vía por defecto no pisa sin elección explícita); el caso **wayland** da `Incompatible`
298  (requisito que no resuelve, o ausente); la compatibilidad **entre dos configs**
299  (`conflicto`) es simétrica y ve tanto reclamos que se pisan como requisitos cruzados; y
300  `filtrar` **particiona una búsqueda** de la malla en `{compatibles, elegibles,
301  incompatibles}` — la respuesta concreta a "cuando busco, saber cuáles puedo adoptar". El
302  test de composición muestra que *compatible no basta*: la misma config puede pasar el
303  chequeo de slots y ser inservible por **incompleta** (paquete manipulado ⇒ `RefColgante`)
304  o **insegura** (resultado afirmado falso ⇒ recomputar lo rechaza) — las tres propiedades,
305  un solo hash.
306- **H4b** ✅ — El modelo de slots **subido a la receta real de hammer** (no ya un prototipo
307  host). Cambios:
308  - `Recipe` (y el `source_patch` del `.swm`) llevan un bloque **`slots`** con `claims`/
309    `requires` (`slot → b3:…`), **fuera de `hash_inputs`** — misma disciplina que la evidencia
310    de H1: declara topología, no identidad ⇒ no mueve el `artifact_hash` (test que lo ancla).
311    Viaja intacto por los dos sentidos del puente (`Recipe → .swm → Recipe`, test de round-trip).
312  - `InstalledDb` (Etapa F) registra los `claims` por paquete y expone `system_state() →
313    slot → hash`: el `Estado` que el gate consulta.
314  - `hammer-core::compat::evaluar(estado, slots) → Veredicto` (el álgebra probada en `wawa-memo`,
315    ahora sobre tipos de hammer).
316  - **El gate en `hammer install`**: antes de reconstruir o hidratar nada, evalúa el paquete
317    entrante contra el estado instalado. **Incompatible** (requisito sin resolver, caso wayland)
318    ⇒ aborta con un mensaje claro; **Colisión** (caso logo) ⇒ aborta pidiendo elección, salvo
319    `--force-slots`; **Compatible** ⇒ procede y registra los `claims` (para que la PRÓXIMA
320    instalación detecte la colisión). `hammer install --help` expone `--force-slots`.
321  Frontera que queda: definir el **espacio de slots** del sistema (qué es una "superficie": un
322  fichero, un módulo wasm de wawa, un componente) — ahí está el diseño real, no en el álgebra
323  (que ya está).
324- **H4c** ✅ — **Superficies OBSERVADAS: "no prometas, observá".** H4b confía en que el AUTOR
325  declare `slots`; la misma subida que hizo H1 (de *prometer* a *verificar*) aplica acá: la
326  superficie más común y observable de un paquete es **el conjunto de paths que escribe**, y
327  esos paths YA están declarados en el `.swm` (`target_bin` de cada source_patch, `path` de
328  cada file_drop) — se conocen **antes de hidratar**, así que el gate aborta sin tocar nada.
329  - `compat::output_paths(swm)` lee esos paths; `compat::path_collisions(db, name, paths)`
330    detecta cuáles ya posee **otro** paquete instalado (reusa `InstalledDb.files` + el nuevo
331    `owner_of` — cero declaración nueva en la receta). Reinstalar el mismo paquete sobre sus
332    propios paths NO colisiona (es upgrade).
333  - `hammer install` corre este chequeo **junto** al declarado: pisar el fichero de otro
334    paquete es el caso *logo* a nivel de fichero (elección) ⇒ aborta salvo `--force-slots`.
335  - **Verificado e2e real** (`tests/compat_gate.rs`, shell-ea al binario `hammer`): dos paquetes
336    escriben `/share/logo.png`; el segundo aborta con "COLISIÓN de fichero" **y no escribe nada**;
337    con `--force-slots` la elección se respeta y el fichero se escribe.
338  Con H4c, un paquete **sin declarar slots** ya participa del gate por lo que de verdad toca.
339- **H4d** ✅ — **La BÚSQUEDA: `hammer compat <repo>`.** El `filtrar` del prototipo `wawa-memo`,
340  ahora sobre el repo real y **read-only** (no construye ni toca nada). Responde la pregunta que
341  arrancó §H4 — *"cuando busco, ¿cuáles puedo adoptar?"*: evalúa **cada** paquete del repo contra
342  el estado instalado y lo particiona en **{compatibles, requieren-elección, incompatibles}**,
343  combinando la vía declarada (slots, H4b) con la observada (paths, H4c) — incompatible domina,
344  colisión (de slot o de fichero) ⇒ elección, si no compatible. **Verificado e2e real**
345  (`tests/compat_gate.rs`): un repo de dos paquetes se parte correctamente (uno choca de fichero
346  con lo instalado ⇒ elección, otro limpio ⇒ compatible).
347- **H4e** ✅ — **`requires` OBSERVADOS: la versión contra la que el paquete se construyó.** Cierra
348  la simetría de H4c: además de observar lo que un paquete *escribe*, observamos de qué *depende a
349  una versión*. La fuente observable, sin que el autor prometa nada: un paquete se construyó contra
350  la versión de sus deps que hay **en el repo** (`deps.runtime` del `.swm` + `expected_hash` de cada
351  dep en el índice); si el usuario tiene esa dep instalada a **otro** hash, la divergió ⇒ rechazo
352  duro. Es el **caso wayland derivado** — el mismo que H4b captura cuando el autor declara
353  `requires`, ahora leído del cierre.
354  - `compat::observed_requires(swm, index)` + `compat::version_conflicts(db, req)` (reusan `deps`
355    del `.swm`, `expected_hash` del índice y `InstalledDb.hash` — cero declaración nueva).
356  - Cableado en `install` (rechazo duro, no lo salva `--force-slots`: es un requisito, no una
357    elección) y en `hammer compat` (bucket incompatibles).
358  - **Verificado e2e real** (`tests/compat_gate.rs`): `hammer compat` marca `app` INCOMPATIBLE
359    porque su dep `wayland-protocol` está instalada a un hash divergido del repo — read-only, ve
360    el `source_patch` sin construirlo.
361  Con H4e, la vía observada es simétrica: **lo que el paquete escribe** (H4c) *y* **de qué depende**
362  (H4e), ambas sin declaración. Lo que queda abierto: subir el grano del path-slot a superficies
363  más ricas (un módulo wasm de wawa, un componente) y el **colapso** con el lado proceso.
364
365**Frontera honesta.** H4a demuestra el *álgebra* sobre hashes abstractos; lo que **no**
366resuelve es la **granularidad de los slots** — dos configs pueden no colisionar en el slot
367`wayland-protocol` pero sí en un byte compartido más fino si el slot está mal cortado. El
368modelo es correcto para cualquier corte; **elegir el corte** (grano de superficie) es H4b y
369es donde vive el juicio. Y la compatibilidad es **estructural** (¿resuelven los hashes?), no
370**semántica** (¿las dos modificaciones *tienen sentido* juntas?): esto último sigue fuera
371del alcance, como debe.
372
373---
374
375## La ambición, hasta el final: config = paquete = función = proceso
376
377H4 no es un anexo: es la **prueba de que la tesis de §H3 sirve para lo que un usuario hace
378de verdad.** Y empuja el colapso que H3 dejó abierto un paso más. Recapitulando lo que ya
379está verde y unificado bajo **un solo tipo de objeto — el hash**:
380
381- una **función** es `blake3(bytecode)` (H3b),
382- un **programa** es `blake3(árbol de hashes)` (H3b) con dependencias por hash *dentro* del
383  bytecode (H3c: el Merkle-DAG),
384- un **paquete** viaja como bytes canónicos con `blake3(bytes) = id` y se verifica standalone
385  (`wawa-verifica`, H3c),
386- y ahora una **configuración** es un conjunto de `(slot → hash)`: reclamos y requisitos que
387  se resuelven exactamente como las `Ref` de H3c (una dependencia insatisfecha *es* una
388  referencia colgante, sólo que a nivel de sistema).
389
390Es decir: **una config y un programa son el mismo objeto visto por dos lentes.** Un programa
391compone funciones por hash; una config compone superficies del sistema por hash. `RefColgante`
392gobierna la completitud de ambos; reproducir gobierna la seguridad de ambos. El colapso
393*paquete = función* ya no es aspiración — H4 lo mostró incluyendo la config como caso.
394
395**Lo que sigue abierto es el último lado: el proceso.** Un sistema configurado *corriendo* es
396un proceso, y un proceso —en la visión H2— *es* su módulo más su log de entradas
397(`MonotonicLog`, PLAN-OS-CRDT E1): mover o reconstruir un proceso = copiar `(módulo, log)` y
398re-ejecutar determinísticamente (H2, regalo 3). Si un **estado del sistema** es un
399`Estado = slot → Id` (H4) y su **historia** es un log monótono de configs aplicadas, entonces
400un sistema-en-ejecución colapsa al mismo objeto: **un hash del código + un log de entradas**,
401reproducible, migrable, memoizable. Ahí `config = paquete = función = proceso` deja de ser
402lema y es *el mismo tipo direccionado por contenido en las cuatro lentes*.
403
404Eso **no está construido** y no lo promete este doc: el lado "proceso" necesita el replay del
405`MonotonicLog` sobre estado real (efectos, I/O), que es exactamente lo que H2 excluye de "puro"
406y lo que vive en el plan OS-CRDT del otro agente. Pero la forma es clara y las tres primeras
407lentes ya coinciden en el hash. La ambición máxima —**una distro donde instalar una config,
408compilar una función, empaquetar y correr un proceso son la misma operación sobre el mismo
409espacio de nombres**— sigue siendo ambición; su núcleo, cada vez menos.
410
411---
412
413## Orden y dependencias
414
415```
416H1 (proof-carrying)  ── extensión natural del VERIFY actual ──► arrancable ya, alto valor
417H2a (auditar determinismo wasm)  ──► gate de todo H2 (spike wawa)
418   └► H2b (caché local) ──► H2c (caché de malla)  [sólo si H2a da verde]
419H3a (design-doc)  ──► registrar la visión, barato
420   └► H3b ✅ (experimento wasm-por-función)  [sobre H2 puro: núcleo Unison verde]
421        └► H3c ✅ (linker de contenido: imports por hash, Merkle-DAG intra-función)
422             └► H4a ✅ (config = conjunto de slots por hash: compatible/completa/segura)
423                  └► H4b ✅ (slots en la receta/.swm real + gate en `hammer install`)
424                       └► H4c ✅ (superficies OBSERVADAS: colisión de fichero, sin declarar slots)
425                            └► H4d ✅ (`hammer compat <repo>`: la búsqueda que particiona un repo)
426                                 └► H4e ✅ (requires OBSERVADOS: dep divergida = incompatible)
427                                      └► [proceso] replay del MonotonicLog  ──► plan OS-CRDT (otro agente)
428```
429
430Recomendación: **H1 primero** (empuja la frontera que ya tenemos, sin apuestas). **H2a** en
431paralelo como spike de wawa (decide si H2/H3b existen). **H3a** cuando haya un rato: es escribir,
432no construir. H2c y H3b son futuro condicionado a verdes previos.
433
434## Qué NO promete este doc
435
436- **No mueve la frontera de confianza.** Sigue en el verificador (checker H1, reproducción H2c);
437  la IA nunca se auto-promueve — SDD 08 §4 intacto.
438- **No reclama verificación formal del sistema.** H1 estratifica evidencia y la reporta;
439  "verificado bajo supuestos", no "invulnerable".
440- **No promete memoización de malla sin determinismo probado** (H2a es el gate).
441- **No promete el colapso Unison.** H3b (✅) demostró el *núcleo* (definir por hash, nombres
442  como metadata, actualizar sin romper, componer por hash), H3c (✅) el *grano intra-función*
443  (función llama función por hash: el Merkle-DAG de código) y H4a (✅) que una *config* es el
444  mismo objeto (superficies por hash; una dependencia insatisfecha = referencia colgante de
445  sistema). El colapso total (config = paquete = función = **proceso**, grano sub-función)
446  sigue siendo ambición, no promesa: falta el lado proceso (replay del `MonotonicLog`).
447- **No promete compatibilidad semántica.** H4 decide compatibilidad **estructural** (¿resuelven
448  los hashes de las superficies?), no si dos modificaciones *tienen sentido* juntas. Y el
449  **grano de los slots** (qué es una "superficie") es diseño abierto (H4b), no resuelto.