hyperpolymath · Nov 5, 2026 · Nov 5, 2026 · Nov 5, 2026 · Nov 5, 2026 · Nov 5, 2026
@@ -5,33 +5,40 @@
 [metadata]
 project = "squeakwell"
 version = "0.1.0"
-last-updated = "2026-03-20"
+last-updated = "2026-11-04"
 status = "active"
-session = "converted from scheme — 2026-04-11"
+session = "route plan + honest baseline — 2026-11-04"
 
 [project-context]
 name = "Squeakwell"
 purpose = """Database recovery through cross-modal constraint propagation"""
-completion-percentage = 5
+completion-percentage = 8
 
 [position]
-phase = "initial-scaffold"   # design | implementation | testing | maintenance | archived
+phase = "design"   # design | implementation | testing | maintenance | archived
 maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
-  # No milestones recorded
+  "M1 honest baseline: binary builds, manifests validate, invariants restated (2026-11-04)",
+  "M2 engine MVP: fixpoint loop over partial octads, golden dataset recovered, export to VeriSimDB",
+  "M3 proofs: verisimdb formal/Recovery.v + echo-types partial-section join module + Idris2 ABI contract",
 ]
 
 [blockers-and-issues]
 issues = [
-  "Project is in scaffold phase — no blockers yet",
+  "Engine, ingest and VeriSimDB client are stubs; no Idris2 proofs exist",
+  "VeriSimDB client targets /v1/<collection>/<id>, which verisim-api does not expose",
+  "VCL-UT certifies only L0-L6 from source (vcl-ut #25); phases 4-5 capped at L6",
+  "verisim-api keeps octad-aware drift and real regenerators private to the binary crate",
 ]
 
 [critical-next-actions]
 actions = [
-  "Implement codegen for primary use case",
-  "Write first working example end-to-end",
+  "Owner decisions taken 2026-11-05 (docs/ROUTE-PLAN.adoc section 9): compiler route; Agda-first; vcl-ut RECOVER verb; name kept; Zig FFI deleted",
+  "Run the empirical gate E1-E6 before the engine session",
+  "Re-target src/verisim.rs to real verisim-api routes",
+  "File the cross-repo issues listed in docs/ROUTE-PLAN.adoc section 12",
 ]
 
 [maintenance-status]

@@ -11,13 +11,13 @@ The README makes claims. This file backs them up.
 
 *From README:* "A database recovery and reconstruction tool that uses VeriSimDB's octad model and VCL-total's progressive type system to reassemble damaged, fragmented, or inconsistent datasets through cross-modal constraint propagation... Data that passes all 10 levels is formally verified as recovered."
 
-*Evidence:* The core reconstruction engine at `src/engine/` implements the 5-phase progressive constraint propagation: Phase 1 (Loose Constraints, VCL-total Levels 1-3) accepts anything structurally valid; Phase 2 (Cross-Modal Inference) uses populated modalities to infer missing ones (document text → graph edges via NER, graph edges → semantic annotations); Phase 3 (Conflict Resolution) arbitrates contradictions via provenance chains and temporal versions; Phase 4 (Tightening, VCL-total Levels 4-6) enforces null-safety and injection-proofing; Phase 5 (Convergence, VCL-total Levels 7-10) achieves cardinality bounds and linearity. The Idris2 type kernel at `src/abi/` provides formal proofs that constraint propagation is monotonic (data only gets more consistent) and conflict resolution is deterministic. Each entity is assigned a confidence score and proof certificate indicating which VCL-total levels it passes. **Caveat:** This is concept stage; only the architecture and proof framework are defined. Implementation of all 5 phases and integration with VeriSimDB/VCL-total is still in development.
+*Evidence:* The reconstruction engine at `src/engine/` is designed as 5-phase progressive constraint propagation: Phase 1 (Loose Constraints, VCL-total Levels 1-3) accepts anything structurally valid; Phase 2 (Cross-Modal Inference) uses populated modalities to infer missing ones (document text → graph edges via NER, graph edges → semantic annotations); Phase 3 (Conflict Resolution) arbitrates contradictions via provenance chains and temporal versions; Phase 4 (Tightening, VCL-total Levels 4-6) enforces null-safety and injection-proofing; Phase 5 (Convergence, VCL-total Levels 7-10) achieves cardinality bounds and linearity. `src/abi/mod.rs` states the invariants the engine must satisfy, in the form an honest mechanisation can target (lexicographic progress rather than monotone real-valued drift; identity preservation; purity of resolve; the VCL-UT ratchet; well-founded termination). **Caveat (2026-11-04):** this is concept stage. The engine, ingest and VeriSimDB client are stubs; no Idris2 proofs exist in this repository yet; VCL-UT can only certify levels L0–L6 from source today. The route to closing each of these gaps is `docs/ROUTE-PLAN.adoc`.
 
 === Claim 2: Eight Independent Representations (Octad Modalities) as Mutual Witnesses for Entity Identity
 
 *From README:* "When you have 8 independent representations of the same entity, damage to any one can be compensated by the others... Eight witnesses are better than one."
 
-*Evidence:* The design document in the README details the octad modality set: Document text (natural language), Graph edges (semantic relationships), Vector embeddings (latent space), Temporal history (version chains), Provenance metadata (hash chains), Spatial coordinates (geospatial data), Semantic types (formal schema), Tensor data (numerical arrays). The cross-modal inference logic at `src/engine/inference.rs` implements transformations: document text → graph edges via NER, document text → vector embedding via encoding, graph edges → semantic annotations via type inference, provenance → temporal ordering via hash-chain sequencing, spatial coords → graph proximity via spatial join, tensor data → vector projections via dimensionality reduction. When any modality is damaged or missing, others can reconstruct it. The drift score metric (starting ~0.8, converging to ~0.0) measures how far the octad is from perfect consistency. **Caveat:** NER and embedding quality depend on external models; this is not a pure reconstruction tool but leverages ML for inference hints.
+*Evidence:* The design document in the README details the octad modality set: Document text (natural language), Graph edges (semantic relationships), Vector embeddings (latent space), Temporal history (version chains), Provenance metadata (hash chains), Spatial coordinates (geospatial data), Semantic types (formal schema), Tensor data (numerical arrays). The planned cross-modal inference transformations are: document text → graph edges via NER, document text → vector embedding via encoding, graph edges → semantic annotations via type inference, provenance → temporal ordering via hash-chain sequencing, spatial coords → graph proximity via spatial join, tensor data → vector projections via dimensionality reduction. When any modality is damaged or missing, others can reconstruct it. Drift is an observable, not the convergence measure: the measure is the pair (missing modalities, unresolved conflicts), which is what actually decreases. **Caveat:** none of these transformations exist in this repository yet; VeriSimDB ships only deterministic baselines (Graph→Document relation text, Document→Vector feature hashing). NER and real embeddings depend on external models.
 
 == Technology Choices
 
@@ -48,20 +48,15 @@ Part of the -iser ecosystem for domain-specific query and recovery tools (TypedQ
 |===
 | Path | What's There
 
-| `src/main.rs` | CLI entry point and orchestration
-| `src/ingest/` | Ingest engine: accepts damaged databases, fragments, SQL dumps, JSON/CSV, corrupted binary files, partial WAL logs
-| `src/engine/` | Core reconstruction engine: 5-phase constraint propagation
-| `src/engine/inference.rs` | Cross-modal inference: document→graph, document→vector, graph→semantic, provenance→temporal, etc.
-| `src/engine/conflict_resolution.rs` | Conflict resolution: provenance + temporal + semantic arbitration
-| `src/engine/type_tightening.rs` | Type tightening: VCL-total levels 4-6 enforcement
-| `src/engine/convergence.rs` | Convergence: VCL-total levels 7-10 formal verification
-| `src/abi/` | Idris2 type kernel with formal proofs of monotonicity, determinism, soundness
-| `src/abi/constraints.idr` | Constraint propagation proofs
-| `src/abi/identity.idr` | Cross-modal entity identity preservation proofs
-| `src/abi/ratchet.idr` | Type ratchet soundness (data only gets more consistent)
-| `ffi/zig/src/` | C-ABI FFI bridge to Idris2 kernel (hyperpolymath standard)
-| `src/verisim_adapter.rs` | Integration with VeriSimDB octad model
-| `src/vcl_ut_adapter.rs` | Integration with VCL-total progressive type system
+| `src/main.rs` | CLI entry point; consumes the library crate
+| `src/lib.rs` | Library crate root: `abi`, `engine`, `ingest`, `manifest`, `verisim`
+| `src/ingest/mod.rs` | Ingest: format detection and octad working-directory layout (stub: no per-format handlers yet)
+| `src/engine/mod.rs` | 5-phase loop skeleton and status/confidence/review/export entry points (stub: no fixpoint, no measure)
+| `src/abi/mod.rs` | The five invariants, restated honestly; no proofs yet
+| `src/verisim.rs` | VeriSimDB HTTP client (currently targets routes `verisim-api` does not expose; re-targeting is Phase 1 work)
+| `src/interface/ffi/` | Deliberately empty: the unbuilt Zig template was deleted on 2026-11-05; an Idris2 ABI must exist first
+| `tests/` | 23 tests (unit, proptest, e2e) against the stubs
+| `docs/ROUTE-PLAN.adoc` | Architecture options, what else must be created across the estate, the proof ladder, the engineering session plan
 | `README.adoc` | Full architecture, design rationale, naming options
 |===
 

@@ -2,10 +2,17 @@
 
 === Current State
 
-* *LOC*: ~3,470
-* *Languages*: Rust, Idris2, Zig
-* *Existing ABI proofs*: `+src/interface/abi/*.idr+` (template-level)
-* *Dangerous patterns*: None detected
+* *LOC*: ~640 Rust (2026-11-05)
+* *Languages*: Rust; an unbuilt Zig FFI template; no Idris2 source yet
+* *Existing proofs*: none. No `.idr` file exists (the template ABI was removed
+  on 2026-03-29, see below). No proof ledger exists yet; one is required by
+  README-EXPLAINME-STANDARD section 5 before any proof is claimed.
+* *Prover homes per standards PROOF-POLICY*: Creusot for the Rust kernel
+  behaviour, Idris2 for the program/journal/gate wire contracts, Agda (echo-types)
+  as theory source rechecked in Rocq (verisimdb/formal) and Lean (tropical-types).
+  The rung-by-rung ladder is `docs/ROUTE-PLAN.adoc` section 6.
+* *Dangerous patterns*: fail-open `.ok()` on every VeriSimDB call in
+  `src/engine/mod.rs` (hides the wrong-route bug); to be removed
 
 === What Needs Proving
 
@@ -33,7 +40,10 @@ insufficient
 
 === Recommended Prover
 
-* *Idris2* for recovery correctness invariants
+* *Creusot* for the Rust resolve/fill/measure kernel (behavioural properties of
+  first-party Rust), *Idris2* for the wire contracts, *Agda → Rocq/Lean* for the
+  lattice and convergence theory. The README's earlier framing of Idris2 as the
+  home of "recovery correctness invariants" is superseded by PROOF-POLICY.
 
 === Priority
 

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-= Octad-Recover (working title — see naming section below)
+= squeakwell — database recovery through cross-modal constraint propagation
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toc: left
 :toclevels: 3
@@ -63,7 +63,8 @@ Damaged data (fragments, corruption, inconsistencies)
         ▼
   PHASE 5 — CONVERGENCE (VCL-total Levels 7-10)
   Cardinality bounds, effect tracking, temporal consistency, linearity.
-  Data that passes all 10 levels is formally verified as recovered.
+  The reintroduction statements for an entity are gate-admissible at level k
+  (ceiling 6 from VCL text; see docs/ROUTE-PLAN.adoc section 4.4).
   Drift score: approaches 0.0
         │
         ▼
@@ -118,13 +119,14 @@ function: recovery is complete when cross-modal drift approaches zero.
   - Phase 4: Type tightening (VCL-total levels 4-6)
   - Phase 5: Convergence (VCL-total levels 7-10)
 
-* **Idris2 type kernel** (`src/abi/`) — Formal proofs that:
+* **Invariants** (`src/abi/mod.rs`; no proofs exist yet, prover homes per
+  estate PROOF-POLICY are in `docs/ROUTE-PLAN.adoc`) — the engine is designed so that:
   - Constraint propagation is monotonic (data only gets more consistent)
   - Cross-modal inference preserves entity identity
   - Conflict resolution is deterministic (same input → same output)
   - Type ratchet is sound (passing level N implies passing levels 1..N-1)
 
-* **VCL-total integration** — Uses TypedQLiser as the type-checking layer.
+* **VCL-UT integration** — Uses the `vclt-gate` binary (hyperpolymath/vcl-ut) as the certifier.
   Each phase invokes progressively stricter VCL-total levels.
 
 * **Output** — Reconstructed database in VeriSimDB format (all 8 modalities
@@ -233,7 +235,12 @@ function: recovery is complete when cross-modal drift approaches zero.
 
 == Status
 
-**Concept stage.** Architecture sketched, phases defined, naming under discussion.
+**Concept stage (2026-11-05).** Architecture sketched, phases defined, engine and
+client are stubs, no proofs exist yet. The route to a working recovery and to the
+first mechanised results, the decisions still open, and what must be created in
+verisimdb, vcl-ut, echo-types and tropical-types are in `docs/ROUTE-PLAN.adoc`.
+The crate, repository and clade are named `squeakwell`; the naming table above
+is kept as the record of the alternatives.
 
 == License
 

@@ -3,30 +3,50 @@
 :toc:
 :icons: font
 
+squeakwell is a database recovery tool: fragments are scattered across
+VeriSimDB's eight modalities, which then act as witnesses that reconstruct
+and cross-check each other until the entity converges. VeriSimDB is the
+required underlying database. The detailed route (architecture options,
+proof ladder, session plan, decisions) is `docs/ROUTE-PLAN.adoc`.
+
 == Phase 0: Scaffold (COMPLETE)
 * [x] RSR template with full CI/CD
-* [x] CLI with subcommands
-* [x] Manifest parser
-* [x] Codegen stubs
-* [x] ABI module stubs
-* [x] README with architecture
+* [x] CLI with subcommands (`ingest`, `recover`, `status`, `confidence`,
+  `review`, `export`, `explain`)
+* [x] Stub engine, stub ingest, VeriSimDB client skeleton
+* [x] 23 tests against the stubs
+
+== Phase 1: Honest baseline (IN PROGRESS)
+* [x] Binary builds again (uses the library crate)
+* [x] K9 / DEED manifests validate; template placeholders removed from
+  the FFI and container files
+* [x] Invariants restated in `src/abi/mod.rs` in a mechanisable form
+* [ ] VeriSimDB client re-targeted to the real `verisim-api` routes
+* [ ] Hypatia critical findings on CI workflows cleared
 
-== Phase 1: Core Implementation
-* [ ] Implement target-language-specific code generation
-* [ ] Write Idris2 ABI proofs for core invariants
-* [ ] Build Zig FFI bridge
-* [ ] First working end-to-end example
-* [ ] Integration tests
+== Phase 2: Engine MVP (the ultracode engineering session)
+* [ ] Partial-octad model in-process (verisim-octad types)
+* [ ] Guarded fill + resolve fixpoint loop with the lexicographic measure
+* [ ] Deterministic baseline regenerators (Graph<->Document, Document->Vector)
+* [ ] Review queue = non-singleton fibres; export refuses unreviewed ambiguity
+* [ ] VCL-UT grading of each entity's canonical DECLARE / NORMALISE
+  transition (L0–L6 cap disclosed)
+* [ ] First end-to-end recovery of a golden damaged CSV+JSON dataset
+* [ ] Export to a running VeriSimDB with a provenance chain per entity
 
-== Phase 2: Polish
-* [ ] Error messages and diagnostics
-* [ ] Shell completions (bash, zsh, fish)
-* [ ] CI/CD for the generated artifacts
-* [ ] Performance benchmarks
-* [ ] Additional examples
+== Phase 3: Proofs (the theory ladder)
+* [ ] `verisimdb/formal/Recovery.v`: guarded fill, lexicographic progress,
+  termination, identity preservation
+* [ ] echo-types module: join-semilattice of partial sections (also closes
+  the gap CROSS-REPO-MAP already flags for merge R1–R3)
+* [ ] Idris2 ABI (`src/interface/abi/Recovery.idr`) quoting the Rocq
+  statements as the contract
+* [ ] tropical-types instance: bottleneck confidence for inference chains
+* [ ] Creusot annotations on the Rust resolve kernel
 
-== Phase 3: Ecosystem
-* [ ] PanLL panel integration
-* [ ] BoJ-server cartridge
-* [ ] VeriSimDB backing store for results
-* [ ] Publish to crates.io
+== Phase 4: Ecosystem
+* [ ] vcl-ut: RECOVER justification / confidence-carrying
+  `RepairJustification`
+* [ ] verisimdb: regenerate-and-return, octad-aware drift as a library,
+  client-chosen ids, proof-certificate attachment
+* [ ] PanLL panel, BoJ-server cartridge, crates.io release