takana/docs/15-frontier-ai-native.md

SDD 15 — Frontera AI-nativa: código por contenido, evidencia sobre confianza, cómputo como dato

Estado: propuesta (2026-07-02). Nace de una revisión externa de las 4 piezas del stack (wawa · hammer/BLAKE3 · wasm determinista · hifas) que propuso seis puentes. Tres caen del lado de hammer/wawa y se recogen aquí; los otros tres (fuente monótona en el kernel, fork-consistency, OS-como-CRDT) viven en tawasuyu/03_ukupacha/PLAN-OS-CRDT.md.

Este doc NO reemplaza nada cerrado. Fases 0–6 + bootstrap Stage 0–2 + los 6 swaps reproducibles siguen siendo la base (ver docs/10-roadmap.md). Esto es frontera: apuestas ordenadas de "extensión natural de lo que ya hacemos" a "otro modelo de datos, design-doc".

---

0. El principio que ya tenemos y hay que empujar

El modelo de confianza de hammer (SDD 09) es "verificar, no confiar": el binario ajeno nunca viaja, viaja la receta, y hammer apply reproduce y compara el expected_hash. La integración de IA (SDD 08 §4) es exactamente la arquitectura de frontera correcta: la IA propone .swm; el sistema reproduce; el humano hace commit; la IA nunca promueve sola.

La revisión externa nombra esto bien: la frontera de confianza no está en quien genera sino en quien verifica. Las tres ideas de abajo empujan esa misma frontera a territorio nuevo, sin moverla de sitio. Ninguna pide confiar más en el modelo; todas piden verificar más.

Nota de higiene (de la propia revisión, adoptada): nada aquí es "matemáticamente invulnerable". Es "verificado bajo supuestos nombrados" — reproducibilidad bajo toolchain fijado, determinismo del sandbox, el checker es pequeño y auditable. seL4 se formula así; nosotros también.

---

H1 — Proof-carrying recipes: de "reproduce" a "trae evidencia que pasa" (la idea 4)

Qué ya hacemos. El bucle agéntico (SDD 08 §2) es PLAN → BUILD → TRY → VERIFY → PROPOSE → humano. Hoy VERIFY = "corre el test harness, escucha BUILD_FAILED/CRASHED". La garantía dura es reproducibilidad: dos máquinas ⇒ mismo artifact_hash. Eso certifica identidad, no comportamiento.

El salto. Que la IA entregue, junto al .swm, evidencia de comportamiento: property tests, contratos, y —cuando el crate lo permita— pruebas tipo Kani/Creusot. hammer admite la mutación sólo si un checker pequeño y confiable confirma que la evidencia pasa. Proof-carrying code (Necula 1997), pero el generador es un modelo: el sistema mejora solo sin poder corromperse solo, porque la confianza vive en el checker, no en el generador.

Por qué encaja aquí y no en otro lado. hammer ya tiene el sandbox hermético (bwrap) donde correr esa evidencia de forma reproducible, ya tiene el Orchestrator con paso VERIFY, y ya tiene procedencia (.hammer/recipe.toml sellado en el artefacto). La atestación por-hash de arje (concesiones matcheadas por hash de binario; ver tawasuyu arje/SDD) es el mismo patrón del lado del init: el permiso deriva de una propiedad verificada del artefacto, no de quién lo firmó. H1 es esa idea, subida del boot al build.

Tickets:

• H1a ✅ — Extender el .swm (SDD 06) con un bloque evidence: lista de {kind, cmd, expected} donde kind ∈ {proptest, contract, kani, cmd-exit}. Serialización YAML estable + verify_schema.
• H1b ✅ — El checker: hammer swm-verify --evidence corre cada ítem dentro del sandbox reproducible y exige expected. Pequeño y auditable a propósito (no un framework: un runner de comandos con hash del output). Falla ⇒ no se propone. Reusa Sandbox::run + el log_tail ya existente (Fase 5).
• H1c ✅ — Cablear al Orchestrator: VERIFY consume evidence; el Proposal lleva el veredicto de evidencia además del diff. El humano ve "reproduce + estas N pruebas pasan", no sólo "reproduce". Frontera: el checker confía en que las pruebas cubren lo que importa — eso lo juzga el humano; H1 garantiza que lo declarado pasa, no que lo declarado basta. Se dice así. Implementación: la evidencia corre del lado del BUILD (no del agente — hammer-agent no depende de hammer-build, separación PROPONE/CONSTRUYE). proto::RecipeInline lleva evidence y Event::BuildReady lleva verdict: Option<EvidenceVerdict>; hammerd::bus la ejecuta tras sellar el artefacto (run_evidence vía swm_bridge::recipe_from_source_patch) y adjunta el veredicto; el Orchestrator lee el veredicto y, si all_passed=false, empuja VerifyCheck::fail y aborta antes de hidratar (el artefacto queda sellado pero no toca el sistema).

Frontera honesta. Property tests no son prueba; Kani/Creusot sí pero sólo cubren crates que se dejan. H1 estratifica la confianza (cmd-exit < proptest < contract < kani) y la reporta; no finge que todo es prueba formal.

---

H2 — Cómputo como dato: memoización de ejecución sobre wasm determinista (la idea 5)

La observación. Si wawa ejecuta wasm determinista, entonces blake3(módulo) + blake3(entrada) → blake3(salida) es una función pura. Nix memoiza builds por hash de entrada; esto memoiza ejecución en runtime. La caché de resultados es content-addressed y compartible por la malla vía la capa CRDT de tawasuyu/shared/crdt (es un GSet/LwwMap de (módulo,entrada) → salida, monótono ⇒ viaja por anti-entropy sin coordinar).

Los tres regalos gratis que la revisión nombra bien:

1. Caché global de cómputo — la malla comparte resultados; un cómputo caro se hace una vez.
2. Replay perfecto — depuración con viaje en el tiempo: un proceso es su módulo + su log de entradas (gancho directo con el MonotonicLog de PLAN-OS-CRDT E1).
3. Migración de procesos como transferencia de datos — mover un proceso = copiar (módulo, log de entradas) y re-ejecutar; el estado se reconstruye determinísticamente.

El gancho con hammer. La caché es un recurso acotado ruteable: hifas::router (BudgetRouter) reparte "créditos de cómputo" por la malla (PLAN-OS-CRDT E3c). Y la verificación de un resultado memoizado es reproducir la ejecución — el mismo "verificar, no confiar" de SDD 09, ahora sobre runtime en vez de build.

Precondición dura (la apuesta). Requiere determinismo total de wasm en wawa: sin float no determinista, sin fuentes de entropía ocultas, orden de scheduling irrelevante para la salida. wasmi es determinista para el core, pero hay que auditar y sellar que ninguna capacidad expuesta (tiempo, random, I/O) filtre no-determinismo a la salida hasheada. Eso es un spike de wawa, no de hammer.

Tickets (spike, no fase):

• H2a ✅ — Auditar determinismo del runtime wasm de wawa: enumerar toda fuente de no-determinismo alcanzable por una app (wawa-kernel/src/wasm/), y definir el subconjunto "puro" (módulo + entrada explícita, sin syscalls no deterministas). Salida: un doc wawa/SDD §determinismo con el veredicto honesto (qué es puro, qué no). Hecho (2026-07-03): tawasuyu/03_ukupacha/wawa/SDD-determinismo.md. Veredicto: el subconjunto puro ya existe en el código (ejecutar_dinamico/_v2, wasm/mod.rs:335,430 — linker VACÍO + reloj virtual + fuel/memoria fijos + wasmi 1.0 sin simd). H2a no era construirlo sino sellarlo: contrato de clave blake3(módulo)⊕blake3(entrada)⊕E con E = hash-de-entorno (pin wasmi/features/ fuel/mem/ABI); único vector residual acotado = payload de NaN vía reinterpret (sólo cross-build, irrelevante para H2b local). La superficie de capacidades (env/*.rs) reintroduce no-determinismo o efectos ⇒ NO memoizable; sólo la vía linker-vacío lo es.
• H2b ✅ — Prototipo de blake3(módulo)+blake3(entrada) → blake3(salida) como caché local (un LwwMap de shared/crdt), sin malla todavía. Test: misma entrada ⇒ hit; recompute ⇒ byte-idéntico (o el determinismo está roto y H2a mintió). Hecho (2026-07-03): crate tawasuyu/03_ukupacha/wawa/wawa-memo (host/std, standalone). Reproduce fiel la vía pura del kernel (ejecutar_dinamico_v2: linker vacío + fuel 500k + 1 MiB
  • wasmi sin simd + despacho polimórfico) y monta la clave del contrato §4 (blake3(bytecode) ‖ blake3(entrada_le) ‖ E, con E = hash de entorno que pinnea wasmi/features/fuel/mem/abi). El test de §5 da verde: 9 módulos × 8 entradas ejecutados dos veces ⇒ blake3(salida) byte-idéntico (H2a no mintió); Miss→Hit sirve valor idéntico al recomputado; las fallas (Trampa/SinCombustible/Carga) se cachean (§4 regla 4); E distinta ⇒ clave distinta (§4 regla 2); y dos réplicas convergen al fundir el LwwMap (anti-entropy, preview de H2c). Como la clave es content-addressed y la función pura, el LWW nunca tiene conflicto real ⇒ el mapa es monótono y compartible sin coordinar. Verde ⇒ H2c desbloqueado (compartir por la malla).
• H2c — (si H2b pasa) compartir la caché por la malla minga/agora. Frontera: envenenamiento de caché por un peer ⇒ se verifica reproduciendo en el primer uso dudoso (no se confía en el resultado ajeno; se confía en poder recomputarlo). Es el modelo de confianza de SDD 09 aplicado a runtime. Núcleo de confianza hecho (2026-07-03, en wawa-memo): dos piezas que hacen seguro el compartir, independientes del transporte. (1) Sellado de portabilidad (sellado.rs, §4 regla 3a): un escáner conservador del bytecode clasifica cada módulo Portable (enteros puros ⇒ sin vector NaN ⇒ idéntico cross-arch) o SoloLocal (toca floats / no decodifica). Decodifica los inmediatos correctamente (no confunde un i32.const 0xBC con el opcode reinterpret_f32). (2) Modelo de confianza (malla.rs): ingerir_ajeno verifica reproduciendo una entrada ofrecida por un peer y rechaza la envenenada (afirmar Ok(99) donde cuadrado(6)=36, o Ok donde hay Trampa) — nunca entra a la caché local; el valor correcto sigue recomputable. Política ConfiarSiPortable = optimización que confía sin recomputar sólo módulos Portable (descarta el vector NaN, no la deshonestidad del peer — dicho explícito). Diferido (es del otro agente): el transporte real (anti-entropy sobre minga/agora) vive en PLAN-OS-CRDT.md (E3). Tests: h2c.rs.

Frontera honesta. Sin determinismo total (H2a), H2 no existe — es la apuesta. No prometer la caché de malla antes de que H2a dé verde. Y "cómputo puro" excluye lo interesante-con-I/O: la memoización cubre la parte funcional, no el proceso entero con efectos.

---

H3 — Código direccionado por contenido estilo Unison (la idea 3) — DESIGN-DOC, no sprint

La visión. Hoy hammer direcciona por hash el artefacto (binario) y la receta. wawa direcciona el módulo wasm y el almacenamiento. La idea 3 empuja al límite: direccionar funciones por el hash de su AST (Unison). La IA no editaría archivos —insertaría definiciones en una base content-addressed donde nada se rompe por renombrar o actualizar— y el store de hammer, los módulos wasm de wawa y el código fuente colapsarían en un solo espacio de nombres: el hash. Paquete, función y proceso = el mismo tipo de objeto.

Por qué es design-doc y no ticket. Es otro modelo de datos, no una extensión. hammer y Unison content-addressan cosas distintas: hammer el artefacto compilado (grano grueso, lenguaje-agnóstico, encaja con "recetas sobre fuente upstream"); Unison el AST de cada función (grano fino, requiere un lenguaje y toolchain propios). Colapsarlos pide reescribir la unidad de compilación entera. El valor es real (fin del dependency-hell para la IA) pero el costo es un proyecto, no una fase.

Qué SÍ hacer ahora (el puente barato hacia la visión):

• H3a ✅ — Doc de diseño docs/adr/0009-content-addressed-code.md (2026-07-03): registra la visión Unison y decide no reescribir la unidad de compilación. Puente barato = procedencia por-símbolo como metadata (extender parse_elf_needed, query.rs:298, para emitir exports de .dynsym además de DT_NEEDED), fuera de hash_inputs (misma disciplina que la evidencia de H1). El grano fino real (función-por-hash) se difiere a H3b sobre wasm, gateado por H2.

• H3b ✅ — (exploratorio) Base content-addressed de funciones wasm (grano: un .wasm por función pura de H2), verificando si "insertar definición, nunca romper" se sostiene sobre el runtime de wawa. Es el subconjunto de Unison que el stack ya soporta (wasm + BLAKE3 + determinismo H2), sin un lenguaje nuevo. Hecho (2026-07-04, en wawa-memo/src/base.rs + tests/h3b.rs): el módulo base monta la Base content-addressed sobre el grano de H2. Cuatro propiedades Unison, todas verificadas (8 tests verdes): (1) identidad = blake3(bytecode) — definir es idempotente y deduplica (structural sharing); (2) los nombres humanos son metadata separada (nombre → Id) — nombrar jamás toca defs; (3) actualizar no rompe (el corazón) — una referencia es un Termino::Ref(Id), un hash; "actualizar f" = insertar def nueva (hash nuevo) + rebindear el nombre, y todo lo que apuntaba al hash viejo evalúa idéntico (v1 y v2 coexisten, ninguna se sobreescribe); (4) composición por hash — un programa es un árbol de hashes (Termino::Componer), su identidad blake3(árbol) es estable e independiente del mapa de nombres. Extras: una referencia colgante falla con Carga sin mentir (el hash no se resuelve en silencio a otra cosa), las fallas deterministas de H2 se propagan por la composición, y evaluar reusa el Memo (cada hoja Ref se memoiza) — código direccionado por contenido + cómputo direccionado por contenido = el mismo hash, la tesis de §H3 mostrada en pequeño. Frontera: NO es Unison entero (sin grano intra-función, sin typechecking sobre la base, sin lenguaje); es el subconjunto que wasm + BLAKE3 + H2 sostienen. Demuestra que el modelo se sostiene, no que hayamos colapsado paquete = función = proceso (eso sigue siendo el design-doc de H3a). Puente H3b↔H2c (2026-07-04, wawa-memo/src/programa.rs + tests/h3b_malla.rs, 8 tests): cierra la tesis de §H3 uniendo el código-por-contenido de H3b con el modelo de confianza de H2c. Un programa entero viaja por la malla como un Paquete { defs, termino } seguro por construcción, en dos capas que tapan vectores distintos: (1) integridad del código = el hash (nueva) — las defs no llevan hash declarado, su identidad se deriva al recibirlas; una Ref(H) sólo se satisface con los bytes exactos que hashean a H, así que alterar o retener una def deja su referencia colgante y rechaza el paquete sin firmar nada (el hash ES la prueba de integridad; la base local queda intacta); (2) verdad del resultado = reproducción (H2c sobre un programa entero) — que el código sea íntegro no dice qué computa, así que una salida afirmada se recomputa y compara (ingerir_paquete_verificando), rechazando la envenenada. verificar_paquete es la primitiva pura. Compartir código es tamper-evident por el hash; compartir resultados es seguro por reproducción — juntos, la foto completa de «el hash es el espacio de nombres común».

• H3c ✅ — (exploratorio) El grano intra-función: el linker de contenido (2026-07-05, wawa-memo/src/enlace.rs + tests/h3c.rs, 10 tests; 40 verdes en el crate). H3b dejó las definiciones opacas: una función wasm no podía llamar a otra — la composición vivía sólo en el árbol (Termino::Componer), fuera del bytecode. H3c mete la dependencia dentro: una definición importa a otra por hash (import "base" "h:<blake3-hex>"), y el linker la satisface únicamente con los bytes de la Base que hashean exacto a ese Id — el contrato de Termino::Ref, ahora intra-bytecode. Consecuencias verificadas: (1) el Merkle-DAG de código — el hash del callee está embebido en el bytecode del caller ⇒ la identidad del caller pinnea transitivamente el DAG entero; la dependencia ENTRA a la identidad; (2) actualizar no rompe, transitivamente — «actualizar g» = def nueva + rebind; toda f que embebía h(g_v1) sigue llamando los bytes exactos de siempre (v1/v2 coexisten); (3) los ciclos son imposibles por criptografía, no por disciplina — un ciclo exigiría un hash que depende del hash que lo contiene (invertir BLAKE3); el DAG es DAG por construcción, idéntico a Unison; (4) la memoización subsume el DAG — la clave del compuesto (blake3(bytecode) ⊕ entrada ⊕ E) ya cubre sus deps; un cierre INCOMPLETO jamás se cachea (el colgante es un hecho de la base local, no del bytecode — cachearlo envenenaría réplicas); E distingue el linker (vacio vs base-v1) para que los espacios de claves no colisionen; (5) los paquetes de malla llevan el cierre transitivo — retener/alterar una dep profunda (a dos aristas del árbol) tumba la ingesta con RefColgante, y la portabilidad del compuesto hereda el veredicto más conservador de su DAG (clasificar_cierre). Política honesta: cada subllamada corre en instancia fresca con fuel completo (pin en E); el presupuesto compuesto no está acotado globalmente — suficiente para el modelo, no para un sandbox de producción. Con H3c, de las dos ambiciones abiertas de H3 queda demostrado el grano intra-función (en su forma wasm: función llama función por hash); lo aún abierto es el colapso total paquete = función = proceso (el lado "proceso" = replay del MonotonicLog, plan OS-CRDT). Formato de viaje + checker standalone (2026-07-05, wawa-memo formato.rs + bin/wawa-verifica, 5 tests; 45 en el crate): el Paquete deja de ser sólo-memoria. Serialización canónica versionada (WAWA-PAQ1): biyección bytes↔paquete (defs ordenadas por Id, término con la misma serialización estructural que define su identidad, parseo estricto — toda corrupción es un error determinista, nunca "mejor esfuerzo") ⇒ blake3(bytes) = id_paquete estable, la identidad del paquete entero en el mismo espacio de nombres. Disciplina intacta: los bytes NO llevan hashes declarados — el formato transporta, el hash prueba (la ingesta deriva identidades y rechaza el byte flipeado con RefColgante). wawa-verifica <paquete.wawa> <entrada> <esperado> es el checker pequeño y auditable (estilo H1) de la afirmación «este paquete con esta entrada produce este resultado»: exit 0/1/2 — ejecutable como evidencia cmd-exit en el sandbox de hammer (un .swm cuyo payload es un programa wasm verificable = el puente concreto paquete↔función) o como gate de ingesta de un peer. El transporte real (anti-entropy) sigue siendo del plan OS-CRDT.

Frontera honesta. No prometer "una distro donde paquete = función = proceso": H3b+H3c demostraron el núcleo del modelo (definir por hash, nombres como metadata, actualizar sin romper — ahora también transitivo —, componer por hash fuera y dentro del bytecode) sobre wasm, no el colapso total ni el grano sub-función (el AST interno de una función sigue siendo opaco: el átomo es la función-módulo, no la expresión). Es la idea más disruptiva; su núcleo ya está verde, su ambición máxima sigue abierta.

---

H4 — Configuraciones compartidas: compatibles, completas y seguras (la aplicación)

De dónde sale. No de la revisión externa: del uso. Un usuario modifica su sistema; cada configuración suya es un conjunto de modificaciones. Quiere compartirlas por la malla y, al buscar una ajena, saber si puede adoptarla — que sea compatible, completa y segura. H4 aterriza toda la maquinaria de H2/H3 sobre ese caso concreto.

La observación que lo hace tratable. "Compatible" parece semántica difusa, pero el usuario lo definió con dos ejemplos que el modelo trata mecánicamente distinto:

• Logo. Ya cambié el logo; bajo una config que también cambia el logo. No es un error: ambas escriben la misma superficie con contenido distinto. La resolución es una elección, no un rechazo.
• Wayland. Modifiqué el protocolo de Wayland; bajo algo que depende de el Wayland stock. Su dependencia no resuelve contra mi versión ⇒ incompatible.

Entonces "compatible" = colisión sobre la misma superficie, y son dos cosas: colisión de escritura (elección) y dependencia insatisfecha (rechazo). El eje nuevo que H4 agrega es un espacio de nombres de slots que cada modificación reclama (escribe, slot → Id) y requiere (depende, slot → Id a una versión exacta). Con esos dos conjuntos, compatible queda definido de forma dura, y sus dos mitades reusan primitivas ya verdes:

propiedad del usuario	qué la garantiza	dónde (ya construido)
segura	verificar reproduciendo — rechaza el resultado envenenado	verificar_paquete (H2c)
completa	cierre transitivo presente — sin referencia colgante	ingerir_paquete (H3c)
compatible	requisitos resueltos + reclamos disjuntos	H4, nuevo

La definición dura de compatibilidad de una config C contra mi estado E:

(1) Requisitos (caso wayland): ∀ (slot, id) ∈ C.requiere : E[slot] = id. Un slot que resuelve a otra versión (o falta) es incompatible — el análogo de sistema a la RefColgante de H3c: una superficie requerida que resuelve a otros bytes. (2) Reclamos (caso logo): ∀ slot ∈ C.reclama : E[slot] ausente o igual en Id. Un slot ya ocupado por otro contenido es colisión = elección, no error.

Tickets:

• H4a ✅ — (prototipo, wawa-memo/src/compat.rs + tests/h4.rs, 7 tests; 52 verdes en el crate) El modelo de slots corriendo. Config { reclama, requiere } sobre el mismo espacio de hashes que H3; evaluar(estado, config) → Veredicto ∈ {Compatible, Colision, Incompatible} es el chequeo local y reproducible ("verificar, no confiar" de SDD 09, ahora sobre la topología de superficies). Verificado: el caso logo da Colision (y la vía por defecto no pisa sin elección explícita); el caso wayland da Incompatible (requisito que no resuelve, o ausente); la compatibilidad entre dos configs (conflicto) es simétrica y ve tanto reclamos que se pisan como requisitos cruzados; y filtrar particiona una búsqueda de la malla en {compatibles, elegibles, incompatibles} — la respuesta concreta a "cuando busco, saber cuáles puedo adoptar". El test de composición muestra que compatible no basta: la misma config puede pasar el chequeo de slots y ser inservible por incompleta (paquete manipulado ⇒ RefColgante) o insegura (resultado afirmado falso ⇒ recomputar lo rechaza) — las tres propiedades, un solo hash.
• H4b ✅ — El modelo de slots subido a la receta real de hammer (no ya un prototipo host). Cambios:
  • Recipe (y el source_patch del .swm) llevan un bloque slots con claims/ requires (slot → b3:…), fuera de hash_inputs — misma disciplina que la evidencia de H1: declara topología, no identidad ⇒ no mueve el artifact_hash (test que lo ancla). Viaja intacto por los dos sentidos del puente (Recipe → .swm → Recipe, test de round-trip).
  • InstalledDb (Etapa F) registra los claims por paquete y expone system_state() → slot → hash: el Estado que el gate consulta.
  • hammer-core::compat::evaluar(estado, slots) → Veredicto (el álgebra probada en wawa-memo, ahora sobre tipos de hammer).
  • El gate en hammer install: antes de reconstruir o hidratar nada, evalúa el paquete entrante contra el estado instalado. Incompatible (requisito sin resolver, caso wayland) ⇒ aborta con un mensaje claro; Colisión (caso logo) ⇒ aborta pidiendo elección, salvo --force-slots; Compatible ⇒ procede y registra los claims (para que la PRÓXIMA instalación detecte la colisión). hammer install --help expone --force-slots. Frontera que queda: definir el espacio de slots del sistema (qué es una "superficie": un fichero, un módulo wasm de wawa, un componente) — ahí está el diseño real, no en el álgebra (que ya está).
• H4c ✅ — Superficies OBSERVADAS: "no prometas, observá". H4b confía en que el AUTOR declare slots; la misma subida que hizo H1 (de prometer a verificar) aplica acá: la superficie más común y observable de un paquete es el conjunto de paths que escribe, y esos paths YA están declarados en el .swm (target_bin de cada source_patch, path de cada file_drop) — se conocen antes de hidratar, así que el gate aborta sin tocar nada.
  • compat::output_paths(swm) lee esos paths; compat::path_collisions(db, name, paths) detecta cuáles ya posee otro paquete instalado (reusa InstalledDb.files + el nuevo owner_of — cero declaración nueva en la receta). Reinstalar el mismo paquete sobre sus propios paths NO colisiona (es upgrade).
  • hammer install corre este chequeo junto al declarado: pisar el fichero de otro paquete es el caso logo a nivel de fichero (elección) ⇒ aborta salvo --force-slots.
  • Verificado e2e real (tests/compat_gate.rs, shell-ea al binario hammer): dos paquetes escriben /share/logo.png; el segundo aborta con "COLISIÓN de fichero" y no escribe nada; con --force-slots la elección se respeta y el fichero se escribe. Con H4c, un paquete sin declarar slots ya participa del gate por lo que de verdad toca. Lo que queda abierto es derivar la otra mitad (los requires observados: de qué depende el paquete) y subir el grano del path-slot a superficies más ricas (un módulo wasm de wawa, un componente), además del colapso con el lado proceso.

Frontera honesta. H4a demuestra el álgebra sobre hashes abstractos; lo que no resuelve es la granularidad de los slots — dos configs pueden no colisionar en el slot wayland-protocol pero sí en un byte compartido más fino si el slot está mal cortado. El modelo es correcto para cualquier corte; elegir el corte (grano de superficie) es H4b y es donde vive el juicio. Y la compatibilidad es estructural (¿resuelven los hashes?), no semántica (¿las dos modificaciones tienen sentido juntas?): esto último sigue fuera del alcance, como debe.

---

La ambición, hasta el final: config = paquete = función = proceso

H4 no es un anexo: es la prueba de que la tesis de §H3 sirve para lo que un usuario hace de verdad. Y empuja el colapso que H3 dejó abierto un paso más. Recapitulando lo que ya está verde y unificado bajo un solo tipo de objeto — el hash:

• una función es blake3(bytecode) (H3b),
• un programa es blake3(árbol de hashes) (H3b) con dependencias por hash dentro del bytecode (H3c: el Merkle-DAG),
• un paquete viaja como bytes canónicos con blake3(bytes) = id y se verifica standalone (wawa-verifica, H3c),
• y ahora una configuración es un conjunto de (slot → hash): reclamos y requisitos que se resuelven exactamente como las Ref de H3c (una dependencia insatisfecha es una referencia colgante, sólo que a nivel de sistema).

Es decir: una config y un programa son el mismo objeto visto por dos lentes. Un programa compone funciones por hash; una config compone superficies del sistema por hash. RefColgante gobierna la completitud de ambos; reproducir gobierna la seguridad de ambos. El colapso paquete = función ya no es aspiración — H4 lo mostró incluyendo la config como caso.

Lo que sigue abierto es el último lado: el proceso. Un sistema configurado corriendo es un proceso, y un proceso —en la visión H2— es su módulo más su log de entradas (MonotonicLog, PLAN-OS-CRDT E1): mover o reconstruir un proceso = copiar (módulo, log) y re-ejecutar determinísticamente (H2, regalo 3). Si un estado del sistema es un Estado = slot → Id (H4) y su historia es un log monótono de configs aplicadas, entonces un sistema-en-ejecución colapsa al mismo objeto: un hash del código + un log de entradas, reproducible, migrable, memoizable. Ahí config = paquete = función = proceso deja de ser lema y es el mismo tipo direccionado por contenido en las cuatro lentes.

Eso no está construido y no lo promete este doc: el lado "proceso" necesita el replay del MonotonicLog sobre estado real (efectos, I/O), que es exactamente lo que H2 excluye de "puro" y lo que vive en el plan OS-CRDT del otro agente. Pero la forma es clara y las tres primeras lentes ya coinciden en el hash. La ambición máxima —una distro donde instalar una config, compilar una función, empaquetar y correr un proceso son la misma operación sobre el mismo espacio de nombres— sigue siendo ambición; su núcleo, cada vez menos.

---

Orden y dependencias

H1 (proof-carrying)  ── extensión natural del VERIFY actual ──► arrancable ya, alto valor
H2a (auditar determinismo wasm)  ──► gate de todo H2 (spike wawa)
   └► H2b (caché local) ──► H2c (caché de malla)  [sólo si H2a da verde]
H3a (design-doc)  ──► registrar la visión, barato
   └► H3b ✅ (experimento wasm-por-función)  [sobre H2 puro: núcleo Unison verde]
        └► H3c ✅ (linker de contenido: imports por hash, Merkle-DAG intra-función)
             └► H4a ✅ (config = conjunto de slots por hash: compatible/completa/segura)
                  └► H4b ✅ (slots en la receta/.swm real + gate en `hammer install`)
                       └► H4c ✅ (superficies OBSERVADAS: colisión de fichero, sin declarar slots)
                            └► [proceso] replay del MonotonicLog  ──► plan OS-CRDT (otro agente)

Recomendación: H1 primero (empuja la frontera que ya tenemos, sin apuestas). H2a en paralelo como spike de wawa (decide si H2/H3b existen). H3a cuando haya un rato: es escribir, no construir. H2c y H3b son futuro condicionado a verdes previos.

Qué NO promete este doc

• No mueve la frontera de confianza. Sigue en el verificador (checker H1, reproducción H2c); la IA nunca se auto-promueve — SDD 08 §4 intacto.
• No reclama verificación formal del sistema. H1 estratifica evidencia y la reporta; "verificado bajo supuestos", no "invulnerable".
• No promete memoización de malla sin determinismo probado (H2a es el gate).
• No promete el colapso Unison. H3b (✅) demostró el núcleo (definir por hash, nombres como metadata, actualizar sin romper, componer por hash), H3c (✅) el grano intra-función (función llama función por hash: el Merkle-DAG de código) y H4a (✅) que una config es el mismo objeto (superficies por hash; una dependencia insatisfecha = referencia colgante de sistema). El colapso total (config = paquete = función = proceso, grano sub-función) sigue siendo ambición, no promesa: falta el lado proceso (replay del MonotonicLog).
• No promete compatibilidad semántica. H4 decide compatibilidad estructural (¿resuelven los hashes de las superficies?), no si dos modificaciones tienen sentido juntas. Y el grano de los slots (qué es una "superficie") es diseño abierto (H4b), no resuelto.