takana etapa 5b: los 59 docs de diseño, runbooks y ADR
645 líneas. Los ADR entran porque en este repo SON documentos vivos, no registros inmutables: el 0013 tiene 5 commits, el 0009 dos. Eso se comprobó antes de decidir, no se asumió por convención general. EXCLUIDOS por ser REGISTRO o generado: docs/evidencia/ (6), el HANDOFF de la noche de KDE (1) y docs/state/ (24, se regenera solo). Reescribir un comando dentro de una evidencia la falsifica. Y el ADR 0016 se excluye de todo barrido, con un aviso adentro para el próximo que barra: habla SOBRE el renombre, así que necesita seguir diciendo 'hammer'. El barrido se lo llevó puesto y lo dejó titulado 'Renombre del sistema: takana → takana'; revertido. Congelados, verificados uno por uno con controles: /opt/hammer, /var/lib/hammer, /usr/bin/hammer, /mnt/vvv/hammer, la URL de gitea, hammer-farm.service, hammer-live-install.sh, BRIEFING-hammer.md, hammerd, hammer-recover y HAMMER_LIVE.
This commit is contained in:
@@ -1,8 +1,8 @@
|
||||
# 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,
|
||||
> (wawa · takana/BLAKE3 · wasm determinista · hifas) que propuso seis puentes. Tres caen del
|
||||
> lado de takana/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
|
||||
@@ -13,8 +13,8 @@
|
||||
|
||||
## 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
|
||||
El modelo de confianza de takana (SDD 09) es **"verificar, no confiar"**: el binario ajeno
|
||||
nunca viaja, viaja la receta, y `takana 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.*
|
||||
|
||||
@@ -36,12 +36,12 @@ dura es **reproducibilidad**: dos máquinas ⇒ mismo `artifact_hash`. Eso certi
|
||||
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
|
||||
tests, contratos, y —cuando el crate lo permita— pruebas tipo Kani/Creusot. takana 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
|
||||
**Por qué encaja aquí y no en otro lado.** takana 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
|
||||
@@ -51,7 +51,7 @@ 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
|
||||
- **H1b** ✅ — El checker: `takana 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).
|
||||
@@ -60,8 +60,8 @@ firmó.** H1 es esa idea, subida del boot al build.
|
||||
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`
|
||||
**Implementación:** la evidencia corre del lado del BUILD (no del agente — `takana-agent` no
|
||||
depende de `takana-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`
|
||||
@@ -89,7 +89,7 @@ por anti-entropy sin coordinar).
|
||||
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`
|
||||
**El gancho con takana.** 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.
|
||||
@@ -98,7 +98,7 @@ confiar" de SDD 09, ahora sobre runtime en vez de build.
|
||||
`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.
|
||||
spike de wawa, no de takana.
|
||||
|
||||
**Tickets (spike, no fase):**
|
||||
- **H2a** ✅ — Auditar determinismo del runtime wasm de wawa: enumerar toda fuente de no-determinismo
|
||||
@@ -149,15 +149,15 @@ 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
|
||||
**La visión.** Hoy takana 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
|
||||
y el store de takana, 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,
|
||||
**Por qué es design-doc y no ticket.** Es **otro modelo de datos**, no una extensión. takana y
|
||||
Unison content-addressan *cosas distintas*: takana 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
|
||||
@@ -238,7 +238,7 @@ proyecto, no una fase.
|
||||
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
|
||||
0/1/2 — ejecutable como evidencia `cmd-exit` en el sandbox de takana (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.
|
||||
|
||||
@@ -303,7 +303,7 @@ La definición dura de compatibilidad de una config `C` contra mi estado `E`:
|
||||
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
|
||||
- **H4b** ✅ — El modelo de slots **subido a la receta real de takana** (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
|
||||
@@ -311,13 +311,13 @@ La definición dura de compatibilidad de una config `C` contra mi estado `E`:
|
||||
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
|
||||
- `takana-core::compat::evaluar(estado, slots) → Veredicto` (el álgebra probada en `wawa-memo`,
|
||||
ahora sobre tipos de takana).
|
||||
- **El gate en `takana 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`.
|
||||
instalación detecte la colisión). `takana 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á).
|
||||
@@ -330,13 +330,13 @@ La definición dura de compatibilidad de una config `C` contra mi estado `E`:
|
||||
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
|
||||
- `takana 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
|
||||
- **Verificado e2e real** (`tests/compat_gate.rs`, shell-ea al binario `takana`): 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`,
|
||||
- **H4d** ✅ — **La BÚSQUEDA: `takana 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}**,
|
||||
@@ -354,8 +354,8 @@ La definición dura de compatibilidad de una config `C` contra mi estado `E`:
|
||||
- `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
|
||||
elección) y en `takana compat` (bucket incompatibles).
|
||||
- **Verificado e2e real** (`tests/compat_gate.rs`): `takana 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**
|
||||
@@ -420,9 +420,9 @@ 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`)
|
||||
└► H4b ✅ (slots en la receta/.swm real + gate en `takana install`)
|
||||
└► H4c ✅ (superficies OBSERVADAS: colisión de fichero, sin declarar slots)
|
||||
└► H4d ✅ (`hammer compat <repo>`: la búsqueda que particiona un repo)
|
||||
└► H4d ✅ (`takana compat <repo>`: la búsqueda que particiona un repo)
|
||||
└► H4e ✅ (requires OBSERVADOS: dep divergida = incompatible)
|
||||
└► [proceso] replay del MonotonicLog ──► plan OS-CRDT (otro agente)
|
||||
```
|
||||
|
||||
Reference in New Issue
Block a user