From d3da07fb3ea6629655399600ef2d3e50692c0566 Mon Sep 17 00:00:00 2001 From: sergio Date: Thu, 2 Jul 2026 10:00:08 -0400 Subject: [PATCH] =?UTF-8?q?docs:=20SDD=2015=20frontera=20AI-nativa=20?= =?UTF-8?q?=E2=80=94=20proof-carrying=20recipes,=20computo=20como=20dato,?= =?UTF-8?q?=20codigo=20por=20contenido?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/15-frontier-ai-native.md | 170 ++++++++++++++++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 docs/15-frontier-ai-native.md diff --git a/docs/15-frontier-ai-native.md b/docs/15-frontier-ai-native.md new file mode 100644 index 00000000..48108f01 --- /dev/null +++ b/docs/15-frontier-ai-native.md @@ -0,0 +1,170 @@ +# 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í. + +**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.