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).
• 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ó).
• 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.

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/00NN-content-addressed-code.md: qué se ganaría, qué unidad (¿AST de Rust? ¿un IR propio? ¿wasm por función?), y el punto de contacto realista con lo que ya existe — la procedencia por-función podría empezar como metadata en el .hammer/recipe.toml (qué símbolos exporta un artefacto, ya tenemos el parser ELF DT_NEEDED de Fase 6) sin cambiar la unidad de build. Registrar la visión, no comprometerse a la reescritura.
• H3b — (exploratorio, opcional) Un experimento aislado: una base content-addressed de funciones wasm (grano: un .wasm por función pura de H2), viendo si el modelo "insertar definición, nunca romper" se sostiene sobre el runtime de wawa. Es el subconjunto de Unison que nuestro stack ya podría soportar (wasm + BLAKE3 + determinismo H2), sin un lenguaje nuevo.

Frontera honesta. No prometer "una distro donde paquete = función = proceso" hasta que H3b demuestre que el grano fino se sostiene sobre wasm. Es la idea más disruptiva y la menos madura; tratarla como tal.

---

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)  [depende de H2 puro]

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 hasta que H3b lo demuestre sobre wasm. Design-doc primero.