hammer/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.
• H4d ✅ — La BÚSQUEDA: hammer compat <repo>. El filtrar del prototipo wawa-memo, ahora sobre el repo real y read-only (no construye ni toca nada). Responde la pregunta que arrancó §H4 — "cuando busco, ¿cuáles puedo adoptar?": evalúa cada paquete del repo contra el estado instalado y lo particiona en {compatibles, requieren-elección, incompatibles}, combinando la vía declarada (slots, H4b) con la observada (paths, H4c) — incompatible domina, colisión (de slot o de fichero) ⇒ elección, si no compatible. Verificado e2e real (tests/compat_gate.rs): un repo de dos paquetes se parte correctamente (uno choca de fichero con lo instalado ⇒ elección, otro limpio ⇒ compatible).
• H4e ✅ — requires OBSERVADOS: la versión contra la que el paquete se construyó. Cierra la simetría de H4c: además de observar lo que un paquete escribe, observamos de qué depende a una versión. La fuente observable, sin que el autor prometa nada: un paquete se construyó contra la versión de sus deps que hay en el repo (deps.runtime del .swm + expected_hash de cada dep en el índice); si el usuario tiene esa dep instalada a otro hash, la divergió ⇒ rechazo duro. Es el caso wayland derivado — el mismo que H4b captura cuando el autor declara requires, ahora leído del cierre.
  • compat::observed_requires(swm, index) + compat::version_conflicts(db, req) (reusan deps del .swm, expected_hash del índice y InstalledDb.hash — cero declaración nueva).
  • Cableado en install (rechazo duro, no lo salva --force-slots: es un requisito, no una elección) y en hammer compat (bucket incompatibles).
  • Verificado e2e real (tests/compat_gate.rs): hammer compat marca app INCOMPATIBLE porque su dep wayland-protocol está instalada a un hash divergido del repo — read-only, ve el source_patch sin construirlo. Con H4e, la vía observada es simétrica: lo que el paquete escribe (H4c) y de qué depende (H4e), ambas sin declaración. Lo que queda abierto: subir el grano del path-slot a superficies más ricas (un módulo wasm de wawa, un componente) y el 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)
                            └► H4d ✅ (`hammer compat <repo>`: la búsqueda que particiona un repo)
                                 └► H4e ✅ (requires OBSERVADOS: dep divergida = incompatible)
                                      └► [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.