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

Frontera honesta. No prometer "una distro donde paquete = función = proceso": H3b demostró que el núcleo del modelo (definir por hash, nombres como metadata, actualizar sin romper, componer por hash) se sostiene sobre wasm, no que el grano fino intra-función o el colapso total lo hagan. Es la idea más disruptiva; su núcleo ya está verde, su ambición máxima sigue abierta.

---

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]

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ó que su núcleo (definir por hash, nombres como metadata, actualizar sin romper, componer por hash) se sostiene sobre wasm; el colapso total (paquete = función = proceso, grano intra-función) sigue siendo ambición, no promesa.