sergio/hammer
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
e72a630d3150f6aa95d506531dce39a412a6d260
hammer/docs/15-frontier-ai-native.md
T

21 KiB
Raw Blame History

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.

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)

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) y H3c (✅) el grano intra-función (función llama función por hash: el Merkle-DAG de código); el colapso total (paquete = función = proceso, grano sub-función) sigue siendo ambición, no promesa.
Reference in New Issue View Git Blame Copy Permalink