diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index deb6a1a..cc3d58f 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -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//, 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] diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 696d577..585bd50 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -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 |=== diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index c51c86c..cbf206a 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -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 diff --git a/README.adoc b/README.adoc index 2f4c07d..6af0625 100644 --- a/README.adoc +++ b/README.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Octad-Recover (working title — see naming section below) += squeakwell — database recovery through cross-modal constraint propagation Jonathan D.A. Jewell :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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 3c517e7..5c85fae 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -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 diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 883cb6a..7f86888 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -1,57 +1,70 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == TEST-NEEDS: squeakwell -=== CRG Grade: C — ACHIEVED 2026-04-04 +=== Current State (2026-11-04) -=== Current State - -[width="100%",cols="40%,26%,34%",options="header",] +[width="100%",cols="40%,16%,44%",options="header",] |=== |Category |Count |Details -|*Source modules* |12 |Rust (main, lib, manifest/mod, engine/mod, -ingest/mod, abi/mod) + Idris2 ABI (3) + Zig FFI (3) +|*Source modules* |6 Rust |`main`, `lib`, `engine`, `ingest`, `manifest`, `abi` (comment-only), `verisim` +|*Unit tests* |10 |`tests/unit_test.rs` — ingest format detection, workdir layout, stub engine entry points +|*Property tests* |5 |`tests/property_test.rs` (fixed-input fixtures, no proptest crate) — ingest determinism, octad directory completeness, stub recovery terminates, level monotonic, query functions stable +|*E2E tests* |8 |`tests/e2e_test.rs` — CLI subcommands against the stub engine +|*Benchmarks* |3 |`benches/squeakwell_bench.rs` (criterion) — measure stub dispatch only +|*Fuzz tests* |0 |`tests/fuzz/` holds a placeholder, no harness +|*Idris2 / Zig tests* |0 |No `.idr` files exist; Zig FFI is an unbuilt template +|=== -|*Unit tests* |0 |Zero. No #[test] in any source file +All 23 tests pass (`cargo test`), but every one exercises a stub: the +engine runs a 5-phase loop that prints phase names and persists +placeholder drift values. Green here means "the scaffold is wired", not +"recovery works". -|*Integration tests* |0 |None +=== What's Missing -|*E2E tests* |0 |None +==== Engine (CRITICAL — blocks everything else) -|*Benchmarks* |0 |None +* [ ] Fixpoint loop over partial octads (guarded fill, resolve, measure); + `max_iterations` is parsed but never used +* [ ] Lexicographic measure `(|missing|, nconflicts)` and a test that it + strictly decreases or the state is a fixpoint (the Progress invariant in + `src/abi/mod.rs`) +* [ ] Proptest laws for `resolve`: commutative, associative, idempotent, + permutation-invariant (the join-semilattice conditions that make + verisimdb `Octad.v` merge theorems apply) +* [ ] Golden damaged-dataset fixtures (CSV + JSON fragments with deleted + and contradicted fields) with expected review-queue contents -|*Fuzz tests* |0 |placeholder.txt only -|=== +==== VeriSimDB integration -=== What’s Missing +* [ ] Client targets real `verisim-api` routes (`POST /octads`, + `PUT /octads/{id}`, `/normalizer/trigger/{id}`, `/drift/entity/{id}`); + today it PUTs to `/v1//`, which does not exist +* [ ] Integration test against a running `verisim-api` (podman), gated + behind a feature or env var -==== EVERYTHING (CRITICAL) +==== VCL-UT integration -* [ ] Zero tests of any kind for 6 Rust modules -* [ ] No test for manifest parsing -* [ ] No test for engine processing -* [ ] No test for ingest pipeline -* [ ] No test for ABI layer +* [ ] Grade recovered entities through `vclt-gate` (or link + `vcltotal-parse`) and assert the L0–L6 cap is reported, never faked ==== Aspect Tests -* [ ] *Security*: Audio/sound processing tool with zero security tests -* [ ] *Performance*: No benchmarks for audio processing throughput -* [ ] *Concurrency*: No tests for concurrent audio stream handling -* [ ] *Error handling*: No tests for malformed audio input, codec -failures - -==== Benchmarks Needed - -* [ ] Audio processing latency -* [ ] Ingest throughput -* [ ] Memory usage under load +* [ ] *Security*: ingest of hostile dumps (path traversal in fragment + names, oversized rows, malformed UTF-8) +* [ ] *Integrity*: export emits only entities whose enumerated fibre is a + singleton; every non-singleton fibre is in the review queue and an export + attempt on it is a hard error +* [ ] *Performance*: convergence iterations vs. number of fragments + (bench), ingest throughput +* [ ] *Observability*: phase events carry real drift and measure values ==== Self-Tests -* [ ] No self-diagnostic mode - -=== FLAGGED ISSUES - -* *12 source files, 0 tests* – completely untested -* *fuzz/placeholder.txt* – fake fuzz testing claim +* [ ] `squeakwell doctor` self-diagnostic (verisim reachability, gate + binary present, workdir sanity) === Priority: P0 (CRITICAL) + +See `docs/ROUTE-PLAN.adoc` for the empirical experiments that gate the +engineering work. diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index 0ad0d04..14a614a 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -1,5 +1,6 @@ +K9! # SPDX-License-Identifier: MPL-2.0 -# deploy.k9.ncl — {{PROJECT_NAME}} deployment component (Hunt level) +# deploy.k9.ncl — squeakwell deployment component (Hunt level) # # k9-svc deployment specification with full pedigree (L1-L5). # Security Level: 'Hunt (requires cryptographic handshake for execution). @@ -7,145 +8,154 @@ # WARNING: This component can execute shell commands! # It requires explicit authorisation via the Leash system. # +# squeakwell is a command-line recovery tool, not a long-running service: +# the "deployment" here builds and verifies the container image that +# carries the CLI and runs it as a batch job against a VeriSimDB instance. +# # Usage: -# nickel typecheck container/deploy.k9.ncl # k9-svc validate container/deploy.k9.ncl # k9-svc deploy container/deploy.k9.ncl --env production +# +# Note: the first line is the K9 magic marker required by the K9 validator; +# plain `nickel typecheck` does not apply to K9 files (k9-svc strips the +# marker before handing the record to Nickel). -# The component's pedigree (self-description across five layers) -let component_pedigree = { +{ # ───────────────────────────────────────────────────────────── - # L1: The Snout — Identity + # Pedigree (self-description across five layers) # ───────────────────────────────────────────────────────────── - metadata = { - name = "{{SERVICE_NAME}}-deploy", - version = "{{VERSION}}", - breed = "application/vnd.k9+nickel", - magic_number = "K9!", - description = "{{PROJECT_NAME}} deployment component (Hunt level)", - }, + pedigree = { + schema_version = "1.0.0", + component_type = "deployment", + + # L1: The Snout — Identity + metadata = { + name = "squeakwell-deploy", + version = "0.1.0", + breed = "application/vnd.k9+nickel", + magic_number = "K9!", + description = "squeakwell container build, verify and batch-run component (Hunt level)", + author = "Jonathan D.A. Jewell ", + }, - # ───────────────────────────────────────────────────────────── - # L2: The Scent — Target Environment - # ───────────────────────────────────────────────────────────── - target = { - os = 'Linux, - is_edge = false, - requires_podman = true, - min_memory_mb = 256, - }, + # L2: The Scent — Target Environment + target = { + os = 'Linux, + is_edge = false, + requires_podman = true, + min_memory_mb = 256, + }, - # ───────────────────────────────────────────────────────────── - # L3: The Leash — Security - # ───────────────────────────────────────────────────────────── - security = { - trust_level = 'Hunt, - allow_network = true, - allow_filesystem_write = true, - allow_subprocess = true, - # In production, replace with a real Ed25519 signature. - signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", - }, + # L3: The Leash — Security + security = { + leash = 'Hunt, + trust_level = "full-system-access", + allow_network = true, + allow_filesystem_write = true, + allow_subprocess = true, + signature_required = true, + # In production, replace with a real Ed25519 signature. + signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", + }, - # ───────────────────────────────────────────────────────────── - # L4: The Gut — Self-Validation - # ───────────────────────────────────────────────────────────── - validation = { - checksum = "sha256:placeholder", - pedigree_version = "1.0.0", - hunt_authorized = false, # Must be set true after handshake + # L4: The Gut — Self-Validation + validation = { + checksum = "sha256:placeholder", + pedigree_version = "1.0.0", + hunt_authorized = false, # Must be set true after handshake + }, + + warnings = [ + "This component has full system access", + "Only run from trusted sources with verified signatures", + "Review all recipes before execution", + ], + side_effects = [ + "Builds the squeakwell container image via container/ct-build.sh", + "Runs one recovery batch with podman against the VeriSimDB named by VERISIMDB_URL", + "Removes the squeakwell-data volume on rollback", + "Writes recovery working directories under the mounted /data volume", + ], + + # L5: The Muscle — Deployment Recipes + recipes = { + install = "container/ct-build.sh", + validate = "podman run --rm ghcr.io/hyperpolymath/squeakwell:latest --version", + deploy = "podman run --rm -v squeakwell-data:/data -e VERISIMDB_URL ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", + migrate = "container/ct-build.sh && podman run --rm -v squeakwell-data:/data -e VERISIMDB_URL ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", + }, }, # ───────────────────────────────────────────────────────────── - # L5: The Muscle — Deployment Recipes + # Deployment configuration # ───────────────────────────────────────────────────────────── - recipes = { - install = "just container-build", - validate = "just container-verify", - deploy = "just container-up", - migrate = "just container-build && just container-up", - }, -} in - -# Deployment configuration -let deployment = { - # Target environments (dev / staging / production) - environments = { - dev = { - replicas = 1, - memory = "256Mi", - cpu = "100m", - image_tag = "dev", + deployment = { + # Target environments (dev / staging / production) + environments = { + dev = { replicas = 1, memory = "256Mi", cpu = "100m", image_tag = "dev" }, + staging = { replicas = 1, memory = "512Mi", cpu = "250m", image_tag = "staging" }, + production = { replicas = 1, memory = "1Gi", cpu = "500m", image_tag = "latest" }, }, - staging = { - replicas = 2, - memory = "512Mi", - cpu = "250m", - image_tag = "staging", - }, - production = { - replicas = 3, - memory = "1Gi", - cpu = "500m", - image_tag = "latest", - }, - }, - # Container configuration - container = { - image = "{{REGISTRY}}/{{SERVICE_NAME}}", - port = {{PORT}}, - health_check = "/health", - readiness_check = "/ready", - }, + # Container configuration (batch job: no listening port) + container = { + image = "ghcr.io/hyperpolymath/squeakwell", + entrypoint = "squeakwell", + data_volume = "/data", + # The VeriSimDB instance the recovery writes to is supplied at run time + # through this environment variable (an https:// URL in production; the + # svalinn gateway in container/compose.toml terminates TLS). + verisimdb_url_env = "VERISIMDB_URL", + }, - # Deployment strategy - strategy = { - type = "rolling", - max_surge = 1, - max_unavailable = 0, + # Deployment strategy + strategy = { type = "recreate" }, }, -} in -# Deployment scripts (executed at Hunt level) -let scripts = { - # Pre-deployment validation - pre_deploy = m%" + # ───────────────────────────────────────────────────────────── + # Scripts (executed at Hunt level) + # ───────────────────────────────────────────────────────────── + scripts = { + # Pre-deployment validation: the image exists and the CLI answers. + # container/compose.toml (the long-running service stack) is NOT used by + # this component: squeakwell is a batch job. + pre_deploy = m%" #!/bin/sh set -eu -echo "K9: Pre-deployment validation for {{SERVICE_NAME}}..." -cd container && selur-compose verify || podman compose --file compose.toml config +TAG="${IMAGE_TAG:-latest}" +echo "K9: Pre-deployment validation for squeakwell:$TAG..." +podman image inspect "ghcr.io/hyperpolymath/squeakwell:$TAG" >/dev/null +podman run --rm "ghcr.io/hyperpolymath/squeakwell:$TAG" --version echo "K9: Validation passed." "%, - # Deployment script - deploy = m%" + # Deployment: build and verify the image, then run one recovery batch + # against the VeriSimDB named by VERISIMDB_URL (must be set; https in + # production). The working directory lives on the squeakwell-data volume. + deploy = m%" #!/bin/sh set -eu ENV="${1:-dev}" -echo "K9: Deploying {{SERVICE_NAME}} to $ENV environment..." -cd container -./ct-build.sh -selur-compose up --detach || podman compose --file compose.toml up --detach -echo "K9: Deployment to $ENV complete." +TAG="${IMAGE_TAG:-latest}" +: "${VERISIMDB_URL:?VERISIMDB_URL must be set (https:// in production)}" +echo "K9: Building squeakwell image for $ENV..." +cd container && ./ct-build.sh && cd .. +echo "K9: Running one recovery batch against $VERISIMDB_URL..." +podman run --rm -v squeakwell-data:/data -e VERISIMDB_URL \ + "ghcr.io/hyperpolymath/squeakwell:$TAG" recover --workdir /data +echo "K9: Batch for $ENV complete." "%, - # Rollback script - rollback = m%" + # Rollback: a batch job leaves no running service; rolling back means + # discarding the data volume written by the last batch. + rollback = m%" #!/bin/sh set -eu -echo "K9: Rolling back {{SERVICE_NAME}} deployment..." -cd container -selur-compose down || podman compose --file compose.toml down +echo "K9: Rolling back the last squeakwell batch (removing squeakwell-data volume)..." +podman volume rm squeakwell-data echo "K9: Rollback complete." "%, -} in - -# Export the component -{ - pedigree = component_pedigree, - deployment = deployment, - scripts = scripts, + }, # Security check: this component requires Hunt level required_level = 'Hunt, diff --git a/docs/ROUTE-PLAN.adoc b/docs/ROUTE-PLAN.adoc new file mode 100644 index 0000000..39c3f31 --- /dev/null +++ b/docs/ROUTE-PLAN.adoc @@ -0,0 +1,960 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += squeakwell Route Plan: proof pathways and the engineering route onto VeriSimDB +:toc: left +:toclevels: 3 +:icons: font +:revdate: 2026-11-05 + +[.lead] +squeakwell recovers damaged datasets by scattering fragments across VeriSimDB's +eight modalities and letting them cross-check and reconstruct each other. +VeriSimDB is the required underlying database. This document answers four +questions: what is the fastest route down the proof pathways, what is the +fastest engineering route, what else has to be created across the estate, and +how an ultracode engineering session should be run. It replaces the aspirational +wording in `README.adoc` where the two disagree. + +== 0. Provenance of this plan + +What this plan rests on, so nothing here is taken for more than it is: + +* Six reader agents read squeakwell, verisimdb (Rust crates and `formal/*.v`), + vcl-ut, echo-types, tropical-types and the estate `standards`/mathesis policy, + citing file and line. Four design agents each produced a full architecture. + Three judges scored them under the elegance, dependability/privacy and + speed/testability lenses. Fourteen adversarial refuters attacked the proposed + theorem ladder; twelve claims were refuted *as packaged* and repaired, two + survived. The repaired statements are the ones recorded here. +* Verified by running: `cargo check -p verisim-octad -p verisim-drift + -p verisim-normalizer` succeeds (165 crate units, about 37 s warm cache); + `vcltotal-parse` builds standalone (2 s); the `vclt-gate` binary certifies + `DECLARE … WHERE … = $1 LIMIT 1` at level 6 and `NORMALISE 'e' FROM + AUTHORITATIVE DOCUMENT` at level 4, rejects `EFFECTS { Write }` at L0, and + spawns in about 3 ms; squeakwell builds and passes its 23 tests. +* Not verified by running: no Rocq/Coq, Agda, Lean, Idris2, Creusot, Isabelle or + podman is installed in the planning environment. Every statement about a + proof is from reading the source. Per `standards/3-practice/PROOF-POLICY.adoc` + section 5, every proof row for squeakwell is therefore OPEN until a prover + actually runs. + +== 1. The answer in one page + +**Engineering route (fastest honest path to a working recovery).** +Build squeakwell as a *compiler from fragments to a certified VCL transition +program*, with a *local-first pure kernel* in front of it. Fragments are typed +and classified in-process (guarded fill, pure resolve, the lexicographic +measure), contradictions are held locally, and only agreed values are lowered +to a running `verisim-api` over its real routes. Every round is printed as a +canonical `.vcl` script, every statement is certified by the `vclt-gate` binary +before it is executed, every executed line becomes a provenance record on the +entity's hash chain, and the loop re-synthesises from the server's own drift +report until the program is empty. This is Architecture D with Architecture A's +kernel grafted in (section 4). Two of three judges chose D; the third chose B +and its grafts are the upstream asks in section 5. The MVP needs **no change in +verisimdb or vcl-ut**; everything on its critical path exists today. + +**Proof pathway (fastest honest path to a first mechanised result).** +Do not try to prove the README's five invariants: one is false (drift is not +monotone under fill), two are vacuous as written (determinism as reflexivity, +termination as "or `max_iterations`"), one belongs to vcl-ut (the ratchet) and +one conflates a provable identity fact with an unprovable oracle claim. Prove +the repaired statements in section 3 in this order: + +. **Rung 0 (today, Rust)**: property tests for the resolve-kernel laws, guarded + fill, and the lexicographic measure, with the mandatory counter-model test + that *finds* a case where conflicts rise after fill. +. **Rung 1 (hours, Rocq)**: `verisimdb/formal/Recovery.v`: guarded fill, + normalise, identity preservation, the counter-model to drift monotonicity, + and lexicographic progress with the hypotheses the refuters showed are + needed (`conflict_sym`, winner-relative conflict count). +. **Rung 2 (one to two sessions, Agda)**: `echo-types/proofs/agda/EchoPartialSection.agda`, + the join-semilattice of partial sections that `verisimdb/formal/CROSS-REPO-MAP.adoc` + already flags as the one missing abstraction. The Rocq file then becomes an + instantiation, as the owner's standing directive requires. +. **Rung 3 (hours each, Lean)**: the two small tropical-types lemmas that + survived refutation: the free-monoid residue measure and the reachability + grade with its monotonicity facts. +. **Rung 4 (after the kernel exists, Creusot)**: purity and permutation + invariance of the Rust resolve kernel, and the export postcondition. +. **Rung 5 (after the wire format is stable, Idris2)**: the engineering + contract for the program IR, journal and gate request/response. + +**What else must be created**: section 5 lists it per repository. The largest +single item is the echo-types module; the most valuable upstream ask is a +`propose`/`apply` pair on verisimdb's normalizer that carries a +`RepairJustification`, because today the server picks the repair target itself. + +**Decisions only the owner can take**: section 9. The default arm is labelled +in each. + +== 2. Ground truth, per repository + +=== 2.1 squeakwell (this repository) + +[cols="2,5"] +|=== +| Item | State on 2026-11-05 + +| Rust | About 640 lines; `main` consumes the library crate; `engine` is a + print-only five-phase loop (no fixpoint, `max_iterations` parsed and unused, + drift hard-coded to 1.0 in phase events); `ingest` creates eight directories; + `manifest` is three comment lines; `abi` is comments only. +| VeriSimDB client | `src/verisim.rs` PUTs to `/v1//`, a route + `verisim-api` does not have. Every call is swallowed with `.ok()`, so the + wrong routes never surfaced in tests. +| Tests | 23 pass (8 e2e, 5 property-style with hand-rolled cases, 10 unit), + all against the stubs. No proptest crate. Benches exercise stubs. +| Proofs | None. No `.idr` file exists; the template ABI was removed on + 2026-03-29. `PROOF-NEEDS.adoc` still claims template-level proofs and about + 3,470 lines of code; both are wrong and are corrected on this branch. +| Templates | About 60 unrendered `{{…}}` placeholders remain outside the FFI + directory (root `Containerfile`, `.envrc`, `.github/*`, `docs/developer/ABI-FFI-README.adoc`, + quickstarts, `www/.well-known`). `build.zig` references an include file and a + bench that do not exist. +| CI | Dogfood Gate K9 check failed on `container/deploy.k9.ncl` (fixed on this + branch). Static Analysis Gate is green on `main` since the descriptile move. + SonarCloud flagged one new vulnerability (curl without `--proto`) on PR 76; + fixed on this branch. +|=== + +=== 2.2 verisimdb (the required substrate) + +[cols="2,5"] +|=== +| Item | Finding (file and line as read) + +| Partial octads | First-class. `Octad` has `Option` for graph, vector, tensor, + semantic, document and spatial, and `u64` counters for temporal and + provenance (`verisim-octad/src/lib.rs` 282-305); `OctadInput` is all-Option. + `OctadConfig.require_complete` is never read anywhere. +| Drift as a library | `verisim-drift` scores raw parts, never an `Octad`, and + returns `0.0` for empty inputs (`calculator.rs` 42-44 and siblings): **absence + reads as zero drift**. The honest octad-aware layer with `computable:false` + per absent modality lives only in `verisim-api/src/drift_compute.rs`, private + to the binary, reachable through `GET /drift/entity/{id}`. +| Regeneration | `RegenerationEngine::regenerate` returns a summary string; the + default `SummaryRegenerator` reports repaired with drift 0.0 while mutating + nothing (`regeneration.rs` 536-544). Real regenerators are in + `verisim-api/src/regenerator.rs`: Graph→Document (appends a `Relations:` + section), Document→Vector (FNV-1a feature hashing, deterministic, not + semantic), Document/Vector→Tensor. No Document→Graph, no merge. +| Conflict resolution | `ConflictResolver::resolve` is stateful, keyed by + conflict id, returns a winning modality name, never a merged value. + `LastWriterWins` takes the caller's last list element (`conflict.rs` 688-692, + confirmed by its own test); `resolved_at = Utc::now()`; `AutoMerge` returns + `None` despite its documentation. +| API | `POST /octads` always generates a UUID (no client id, no upsert); + `PUT /octads/{id}` 404s when missing and under-reports presence in its + response; `OctadResponse` carries flags and counts, not content; + `POST /normalizer/trigger/{id}` picks the repair target itself; + `/proofs/generate` is a SHA-256 commitment or Merkle inclusion, explicitly not + zero-knowledge, with no entity linkage; `/vcl/execute` dispatches only + SELECT, SEARCH, INSERT, DELETE, SHOW, COUNT, EXPLAIN (`vcl.rs` 97-103). The + lifecycle verbs are the semantic model, not the in-repo grammar. +| Defaults | Auth disabled (`auth.rs` 40-47), bind on all interfaces, in-memory + store unless the persistent feature is built. +| `formal/Octad.v` | octad = ident × (modality → option mval); `project` + idempotent and composes as meet; `merge resolve` commutative, associative and + idempotent iff `resolve` is; `enrich` **overwrites** an existing value; all + `*_preserves_id` are reflexivity. +| `formal/Normalizer.v` | `modality` and `octad` are abstract Parameters, + incompatible with `Octad.v`'s inductive record; `drifted` is a global + constant; `normalize_idempotent` holds under two winner axioms. N1 + (drift decrease) is explicitly deferred in the file. +| `formal/Drift.v` | Scores are clamped to [0,1]; `le` has reflexivity only + (no transitivity, no well-foundedness). No `drift(octad)` exists anywhere in + `formal/`. +| Cross-repo map | Every foundation theorem is mapped to an echo-types module; + the one flagged missing abstraction is the join-semilattice of partial + sections. +|=== + +=== 2.3 vcl-ut (the certifier) + +* Every level L0–L10 is a predicate over a `Statement` (plus `OctadSchema`) or + a `Transition`; none mentions a value or an octad. "Data that passes level N" + is a category error. The honest claim is: *the reintroduction statement for + entity e is gate-admissible at level k, and e's populated fields are + schema-bound.* +* From VCL text only L0–L6 are reachable (issue #25, fail-closed). Transitions + have a hard ceiling of 4 (`Transition.idr` 183-185) and do not check modality + presence: `NORMALISE e FROM AUTHORITATIVE TENSOR` on a tensor-less entity is + admissible. Exit 0 is not "repair justified". +* The `vclt-gate` binary is the frozen v1 seam; verisimdb's Elixir executor + already calls it. Linking `vcltotal-parse` as a crate bypasses the trusted + seam (its Rust decider carries no proofs). Use the binary; use the crate only + as a test oracle. +* `Epistemic.idr` line 149 discards the atom in `satisfies (PAtom _)`, and + `PBelieves` evaluates identically to `PKnows`; no module imports the Kripke + semantics. Any L10 story built on it today is vacuous. + +=== 2.4 echo-types and tropical-types (the owner's types) + +* echo-types: `Echo f y := Σ x. f x ≡ y` and the finite fibre-count, + decidability and no-section lemmas are mechanised, `--safe --without-K`, zero + postulates. Missing: any partial-section or multi-witness layer. + `EchoTruncation.agda` is unwired from `All.agda` and so counts as dead code + under the repo's own discipline. Retracted and gated: the graded comonad, + the cone universal property, any 2-categorical shape, EI-2 (gate G-001). + Hard limit the theory itself states: any fibre-determined functional is + witness-blind, so a confidence score may rank fibres but never choose a + member of one. +* tropical-types: `Resource.Closure` defines the Kleene star `matStar` + parametrically over any `ResourceAlgebra` with monotonicity, `I ⊑ A*` and a + bound certificate, instantiated at `MinMax` (bottleneck) and `MinPlus` + (product on quantised −log confidence). It proves **no walk semantics**; + that exists only in Isabelle, over naturals, for max-plus and min-plus, and + the Isabelle status is self-contradictory inside the repo. Carriers are + ℕ-based: a quantisation layer is needed for f64 confidence. + `hub_ceiling` is over `List TransportClass` and does not transfer literally. + +=== 2.5 Estate policy (standards @ e064539, mathesis) + +First-party Rust behaviour is verified with Creusot, never a parallel model. +Idris2 carries API, ABI and wire-format contracts. Theory lives in Agda as +source of truth, rechecked in Rocq and Lean. Existing Rocq proofs of theory are +target-only evidence until an Agda source exists and the statements are +compared. Status vocabulary: PROVEN, PROVEN-WITH-AXIOMS, TESTED (with bounds), +ASSUMED, OPEN; a row is only as strong as its weakest dependency. Python is +banned with no exceptions, which rules out any ML regenerator the README +alludes to. squeakwell has no row in the mathesis catalogue because it has no +proof files of its own. + +== 3. The invariants, restated honestly + +[cols="1,2,3,2"] +|=== +| Invariant (README) | Verdict | Repaired statement | Home + +| MonotonicConvergence + `drift(i+1) ≤ drift(i)` +| **False.** Runnable witness: a Document-only octad reports + `graph_document_drift {0.0, computable:false}`; add one graph edge whose + target is not in the text and it becomes `{0.5, computable:true}`. +| Progress on a lexicographic measure `mu(o) = (|missing o|, nconflicts o)` + over naturals: `step o = o ∨ mu(step o) a) o + (mk_octad (oid o) (oracle o))` so the observed value wins, and all oracles + passed as arguments, never declared as Parameters. Plus: guarded fill never + changes an observed value on the six content modalities; the two audit + modalities (provenance, temporal) move by chain prefix, not by equality. +| Rocq `formal/Recovery.v`. + +| DeterministicResolution + `resolve(c,I) = resolve(c,I)` +| **Vacuous** (reflexivity). The Rust is order-dependent: LWW takes the + caller's last element; `ModalityPriority` falls back to `.first()` for + modalities not in the list. +| A pure Rust kernel `resolve(policy, &[(Modality, Ts, Mval)]) -> Option` + with `#[ensures(result == spec_resolve(policy, xs@))]`, body free of clock, + RNG and statics; `ModalityPriority` permutation-invariant given a total order + on `Modality` as tie-break; `LastWriter` permutation-invariant only with + timestamps carried in the input and a total tie-break; equality on + observable fields only. +| Creusot on `src/engine/resolve.rs` (squeakwell). + +| TypeRatchetSoundness + `passes(e,n) → ∀ m ≤ n. passes(e,m)` +| **Belongs to vcl-ut**, and is Statement-indexed, not data-indexed. Holds by + constructor shape; the projection function is unwritten. Transitions have no + level index at all (`certifiedTransitionLevel` is the constant 4). +| `weaken : SafetyCertificate s sch n -> CanWeakenStar n m -> SafetyCertificate + s sch m` (about 23 clauses). squeakwell's `passes(e, k)` is defined as: the + canonical reintroduction statements for e certify at level ≥ k; capped at 6 + from text, 4 for transitions. +| Idris2 `vcl-ut/src/core/Levels.idr`; quoted contract in squeakwell's ABI. + +| TerminationGuarantee + `∃ i. drift < θ ∨ i = max_iterations` +| **Vacuous** (satisfied by `i := max_iterations`); no loop exists. +| Well-foundedness of `mu` on nat×nat gives termination without fuel; + `max_iterations` is an operational budget and a `NotConverged` error, not the + argument. +| Same file as Progress. + +| "Never export corrupt data" (PROOF-NEEDS) +| Not statable over `project M` (normalise legitimately overwrites a drifted + observed value, so the repaired octad leaves that fibre). +| At fragment granularity: let `T ⊆ dom(obs)` be the fragments Phase 3 accepts + as authoritative (an output of recovery, recorded in provenance; every + overruled fragment carries a `RepairJustification`). Every exported octad e + satisfies `restrict_T e = obs|_T`, i.e. `e : Echo restrict_T (obs|_T)`. + Review-queue completeness is stated over the *enumerated candidate fibre* + (`FiberSize-fin (obs ∘ cand_y) y`), not over the mask fibre, and needs a + concrete `mval` with decidable equality. +| Agda `EchoRecovery` audience record (source); Creusot export postcondition. +|=== + +== 4. Architecture + +=== 4.1 The four options as judged + +Scores are 1–10 from the three judges (elegance E, dependability/privacy D, +speed-to-first-recovery S). All four honour the hard requirement that +VeriSimDB is the underlying database. + +[cols="2,1,1,1,4"] +|=== +| Option | E | D | S | Decisive finding + +| A. Library-coupled: verisim crates in-process, server at export +| 7/7/6 | 6/7/7 | 5/5/5 +| Best offline testability and data minimisation; but re-implements two + private server semantics (computability flags, hash embedding) with no + compile-time tie, and `verisim-normalizer` pulls `verisim-octad` and all + eight modality crates, so the "light" fallback does not exist. + +| B. Server-driven: every fragment is an octad in verisim-api +| 8/7/8 | 7/5/8 | 4/4/3 +| Cleanest separation and the strongest form of the requirement; but the MVP + is blocked on six upstream route additions, has zero offline test surface, + and writes every raw and contradictory value to an unauthenticated, + all-interfaces server before any review. + +| C. Hybrid with the session dogfooded as an octad +| 5/6/5 | 6/5/6 | 4/4/5 +| The `verify` subcommand and the fibre trichotomy are good; the dogfood + layer fills modalities with semantically void content (hash-embedding of + review text, an 8×8 drift tensor) and leaks the review queue to the server + every iteration. + +| D. Compiler: fragments → certified VCL program → lowered to REST +| 7/8/7 | 7/7/8 | 5/6/8 +| Dissolves the README's category error (the certified object *is* a + statement), replay is a testable WAL-style property, fail-closed round abort + on a missing gate, values never enter statement text. Weaknesses: verisimdb + executes none of the lifecycle verbs, so the lowering is a second semantics + guarded only by replay tests; NORMALISE lowering is intent-lossy today; + round-0 lowers all fragments before review unless A's classification is + grafted in front. +|=== + +=== 4.2 Recommendation + +Per estate doctrine 15 the most elegant correct long-term option is the +default arm, and it must be labelled: **D with A's kernel in front (default +arm)**. Named here as *the compiler route*. + +* From D: the program IR and canonical printer, the gate client on the frozen + binary seam, the lowering with bindings and statement-hash provenance, the + round-based journal with `replay` and `diff`, intent/effect reconciliation, + round abort on `GateUnavailable`. +* From A: local-first fragment typing, the pure resolve kernel with its law + tests, guarded fill, the lexicographic measure and the mandatory + counter-model test, `quality: Option` that is `None` when nothing is + computable, the constructor that refuses verisimdb's `SummaryRegenerator`, + the id-map written before any dependent write. +* From C: the fibre trichotomy (size 0/1/n) as the export gate with confidence + as ranking only, and the `verify` subcommand that rebuilds status from the + id-map and the server alone. +* From B: the upstream asks (section 5.1), filed with measured numbers from + the MVP run rather than argued. + +Why not B outright, although one judge preferred it: its MVP cannot run +without verisimdb changes the squeakwell owner does not control, and it has no +offline test surface, which is exactly what an ultracode session needs to +validate within one sitting. Why not A outright: it duplicates private server +semantics and its `--allow-offline` switch reintroduces fail-open. The compiler +route keeps the server as the only drift authority and keeps squeakwell's own +code to typing, synthesis, lowering and journalling. + +Alternatives rated for the record (elegance/correctness first, then +dependability): + +. **D-only** (no local kernel, lower everything at round 0): most elegant on + paper, loses on privacy and on recovery power until verisimdb grows + `propose`/`apply`. Second. +. **A-only**: dependable offline, slower to a first recovery, duplicates + semantics. Third. +. **B**: correct end state for the server, but blocked. Fourth today, first + once section 5.1 lands upstream; the compiler route converges to it. + +=== 4.3 Components and data flow + +.... + fragments (CSV, JSON, embeddings, provenance, versions) + │ + ▼ + ┌──────────────┐ typing: entity keys, OctadSchema fields, presence vectors, + │ src/fragments│ candidate lists per field, damage mask + └──────┬───────┘ + ▼ + ┌──────────────┐ pure kernel (A graft): guarded fill with deterministic + │ src/kernel │ regenerators, resolve(policy, frags) -> winner + justification, + │ fill/resolve│ mu = (|missing|, nconflicts), fibre trichotomy, review queue + │ measure │ (no network, proptest laws, Creusot targets) + └──────┬───────┘ + ▼ + ┌──────────────┐ round-N.vcl: DECLARE / ASSERT / NORMALISE … WHERE … = $n + │ src/program │ params-N.json carries the values; canonical printer; + │ IR + synth │ requested level ≤ 6 by construction + └──────┬───────┘ + ▼ + ┌──────────────┐ vclt-gate binary (pinned commit), stdin JSON, 2 s timeout, + │ src/gate │ exit 0 → execute, 1 → review, 2 → abort the round + └──────┬───────┘ certs-N.jsonl with the gate's commit hash + ▼ + ┌──────────────┐ REST plan on real routes: POST /octads, PUT /octads/{id}, + │ src/lower │ POST /normalizer/trigger/{id}, POST /provenance/{id}/record + │ │ (event keyed by SHA-256 of the statement), presence pre-check, + └──────┬───────┘ intent/effect reconciliation → effects-N.jsonl + ▼ + ┌──────────────┐ GET /drift/entity/{id} (computable flags), GET after PUT, + │ verisim-api │ GET /provenance/{id}/verify; fixed threshold, `le` boundary + └──────┬───────┘ + ▼ + re-synthesise next round until the program is empty, or NotConverged +.... + +Journal on disk: `session.json`, `bindings.json` (symbolic name → UUID, written +before any dependent write), `round-N.vcl`, `params-N.json`, `certs-N.jsonl`, +`effects-N.jsonl`, `review-N.vcl`. Everything the user will read contains ids, +hashes, counts, levels and exit codes, never recovered values. + +Crash between create and binding: a crash after `POST /octads` succeeds but +before `bindings.json` is written would leave an unbound octad and a resume +could create a duplicate. The binding is therefore written in two phases: an +*intent* record (deterministic entity key, also placed in +`OctadRequest.metadata`) before the POST, and a *confirmation* with the UUID +after it. On resume an unconfirmed intent is reconciled by searching the +server for its metadata key before any new create; once the client-chosen id +item in section 5.1 lands, the intent phase collapses into `POST /octads/{id}`. +T14 carries this as a done-when. + +=== 4.4 The honest grading rule + +For each entity e squeakwell emits one `DECLARE . FROM OCTAD 'e' +WHERE . = $n LIMIT 1` per populated field and, for each repair, a +`NORMALISE 'e' FROM AUTHORITATIVE `. The gate verdict on those statements +is what squeakwell reports: `gate_level 6` means the field names resolve in the +recovered schema and the statement shape passes L0–L6; `4` means the transition +is admissible. It says nothing about the values (they travel in `$n`), L2 is +near-vacuous on parsed input, and L7–L10 are reported as *not expressible from +text (vcl-ut #25)*, never as achieved. Phase 5 is re-scoped from "levels 7–10" +to: fixpoint reached, gate-admissible at 6/4, provenance chain verifies, server +drift agrees with local expectation. Repaired values themselves are unverified +until the server can return modality content (`GET /octads/{id}/full`). + +=== 4.5 Aspects the design must honour regardless of option + +* **Fail-closed.** Remove every `.ok()` on client calls; `recover` refuses to + start without `GET /health`; a missing or timed-out gate aborts the round + before any network effect; no offline switch for `recover`. +* **No silent green.** Raw `verisim-drift` calculators are never used without a + computable flag; `quality` is `Option`; server-dependent tests *skip with + a message*, never pass, when the server or gate is absent. +* **Integrity and provenance.** GET after every PUT (the server under-reports + presence on update); one provenance record per executed statement keyed by + its SHA-256; `GET /provenance/{id}/verify` before export; the server's actor + string is client-supplied, so the chain is tamper-evident, not authenticated. + Flags, counts and statement-hash provenance do not verify the *value* a + `NORMALISE` repair produced: repaired values stay unverified until + `GET /octads/{id}/full` exists upstream (section 5.1); until then export + labels them `derived` and the plan says so. +* **Privacy.** Fragments, params and the review queue stay in the workdir; + only agreed, singleton-fibre values are lowered; bind the recovery server to + loopback or the podman network, enable auth, build the persistent image with + a retention policy; the FNV hash-embedding is a content fingerprint and is + labelled non-semantic. +* **Security of the gate seam.** Spawn `vclt-gate` by absolute pinned path, no + shell, stdin JSON only; record its commit hash in every certificate. +* **Licensing.** squeakwell, verisimdb and `vcltotal-parse` are MPL-2.0; + echo-types carries an AGPL-3.0-or-later text in `LICENSES/` that must be + checked before any Agda is vendored; pin every git dependency by revision. +* **Language policy.** No Python, Go or TypeScript anywhere, including + regenerators: only deterministic regeneration ships. + +== 5. What else must be created, per repository + +=== 5.1 verisimdb + +[cols="3,3,1"] +|=== +| Item | Why | Size + +| `POST /normalizer/propose/{id}` and `POST /normalizer/apply/{id}` carrying a + `RepairJustification`, by splitting `StoreRegenerator` compute from + write-back and adding `propose_from` to `ModalityRegenerator` +| Today the server picks the target itself and commits on call; the certified + program's justification is advisory. This is the single most valuable ask; + file it with the measured intent/effect disagreement rate from the MVP. +| M (~150 LOC + handler) + +| Client-chosen id: `POST /octads/{id}` or `Option` on `OctadRequest`, with + `OctadStore::create_with_id` +| Deterministic keys and crash-resume; today journal loss orphans UUIDs. +| S (~40 LOC) + +| `GET /octads/{id}/full` returning modality content, and fix `update()` + presence under-reporting +| A recovery engine must read witness values; today only flags and counts + come back. +| S (~80 LOC) + +| Octad-aware drift as a library (`drift_compute.rs` behind an optional + `verisim-octad` dependency) +| Raw calculators read absence as zero drift; the honest layer is private. +| M (~450 LOC relocation) + +| Deterministic Document→Graph (parse the `Relations:` section) and + Semantic→Graph regenerators +| The only Graph-recovery paths that can exist without ML; today none exist. +| S (~120 LOC) + +| Pure value-level resolve kernel (`mcombine` of `Octad.v`) next to + `conflict.rs`; fix the `AutoMerge` doc/code mismatch +| The Coq merge laws have no Rust counterpart; `ConflictResolver` is stateful. +| S (~80 LOC) + +| `PUT /normalizer/config {threshold_policy: fixed, boundary: le}`; proof + attachment `POST /octads/{id}/proofs` into the semantic modality +| Adaptive thresholds make convergence a moving target; proofs have no entity + linkage. +| S–M + +| `formal/Recovery.v` (rung 1) and functorising `Normalizer.v` so it and + `Octad.v` can coexist in one `Require` chain; fix the CROSS-REPO-MAP rows that + cite the unwired `EchoTruncation` +| No `drift(octad)`, no fill/resolve composition, no measure exists in + `formal/`. +| 150–250 lines Rocq +|=== + +=== 5.2 vcl-ut + +* `weaken`/`weakenStar` in `Levels.idr` (rung for the ratchet; additive). +* Additive `RepairJustification` constructors: `LastWriter` and + `Reconstructed Modality Residue` with `data Residue = Unique | Finite Nat | + Unbounded` (mirrors `FiberSize-fin`; a nat grade doubles as the tropical + bottleneck loss). Reopens no theorem; wire tags 3 and 4; one conformance + fixture each. Validate with `idris2 --build verification/proofs/vclut-core.ipkg`. +* Fix `Epistemic.idr` line 149 (atom discarded) and separate `PBelieves` from + `PKnows`; a Transition-indexed certificate is the prerequisite for the L10 + conjecture in section 6. +* Gate batching (reserved `schema_version`) and exporting the schema-JSON + builder from the library; today it lives only in the binary. + +=== 5.3 echo-types + +* `proofs/agda/EchoPartialSection.agda` (250–400 lines): `PartialSection P := + (b : B) → Maybe (P b)` over `EchoDisplayed.Displayed`; `Defined`/`dom`; + pointwise information order with refl/trans (antisymmetry only under the + funext parameter); `resolveJoin` through the exact `mcombine` table; + conditional `join-comm/assoc/idem`; `restrict` with idempotence and + compose-as-meet; `restrict-fibre-char`; guarded fill as inflationary + operator; Kleene fixpoint on `Fin 8`. Same OPTIONS header as siblings, zero + postulates, wired into `All.agda` and pinned in `Smoke.agda`. +* `EchoFibreIntersection.agda` (60–120 lines): binary narrowing as a + funext-free one-liner, the `Fin n` form by induction; `narrow-shrinks`. +* Wire `EchoTruncation.agda` into `All.agda`; add the generic one-line + `fibre-blind` lemma (today only the `collapse : Bool → ⊤` instance exists). +* An `EchoRecovery` audience record in the `EchoProvenance` pattern, over + fragment positions and the accepted set `T`. + +=== 5.4 tropical-types + +* `Resource/HubCeiling.lean`: `factor_le`, `zero_bot`, `join_bound`, + `lsum_bound`, and the star corollary under an explicit `IsStar` hypothesis; + discharged at `MinMax` and `MinPlus`, not `MaxPlus`. +* `reachGrade (A) (S) (m) := lsum ((allFins n).filter S |>.map (matStar A · m))` + with `reachGrade_mono_mat`, `reachGrade_mono_set` (needs a new + `lsum_filter_mono`) and `one ⊑ reachGrade A S m` when `S m`. +* The generic `weightedResidueMeasure` (free-monoid homomorphism; only + `one_mul` and `mul_assoc` are used). +* Reconcile the self-contradictory Isabelle status and add an Isabelle CI job + or an explicit "unverified" banner. Walk semantics for `matStar` in Lean is a + large item and is not on squeakwell's critical path. + +=== 5.5 standards and mathesis + +* Add a squeakwell row to the mathesis catalogue once a proof file exists. +* A `PROOF-STATUS.adoc` ledger in squeakwell with every row OPEN, prover home + per policy, and the dependency rows (verisim-api routes, vclt-gate contract) + as ASSUMED with pinned commits. +* No `DATA-FORMAT-ROUTING` document exists in `standards`; do not cite one. + +=== 5.6 squeakwell + +The task graph in section 8 is the list. The items that are not features: +re-target the client to real routes; remove the fail-open `.ok()`s; make the +stub return `NotImplemented` rather than printing "recovery complete"; resolve +the remaining placeholders; either delete `src/interface/ffi` or make +`build.zig` reference files that exist; rewrite `PROOF-NEEDS.adoc` to the +policy split; fix the one clippy warning; add proptest as a dev-dependency or +stop calling the hand-rolled tests property tests. + +== 6. The proof ladder + +Rungs are ordered fastest-first. "Status" is the status *after* adversarial +refutation. Every row is OPEN in the ledger until the named prover runs. + +[cols="1,3,2,2,1"] +|=== +| Rung | Statement (repaired form) | Builds on | Home | Effort + +| R0 | Proptest laws: resolve comm/assoc/idem under the chosen kernel, + permutation invariance (expected to FAIL for caller-order LWW and the fp + Merge strategy, PASS for ModalityPriority with a total tie-break); fill never + overwrites an observed value on content modalities; `mu` lex-decreases or the + state is a fixpoint; the suite must *find* a case where conflicts rise after + fill. | — | squeakwell `tests/` | hours + +| R1 | `weaken : SafetyCertificate s sch n -> CanWeakenStar n m -> + SafetyCertificate s sch m` (Statement-indexed; transitions have no level + index) | `Levels.idr` 279-387 | vcl-ut Idris2 | hours + +| R2 | `oid (iter step n o) = oid o` with fill as left-biased merge against the + oracle's proposal, all oracles as arguments | `Octad.v` `*_preserves_id` | + verisimdb Rocq `Recovery.v` | hours + +| R3 | Guarded fill is inflationary on the six content modalities; audit + modalities move by chain prefix | `Octad.v` `present`/`missing`, + `Provenance.v` `append_record` | Agda source, Rocq recheck | half a day + +| R4 | Counter-model theorem: `∃ o. nconflicts o < nconflicts (fill o)` | + `drift_compute.rs` 218-263 (runnable witness) | Rocq | hours + +| R5 | `weightedResidueMeasure w : ResidueMeasure (List M) R` for any + `ResourceAlgebra` (free-monoid hom; survived refutation) | + `EchoBridge.lean` 53-104 | tropical-types Lean | hours + +| R6 | Element lemma `a ⊠ b ⊑ a` when `one` is top; star corollary only under + `IsStar`; `verisim-normalizer`'s FromAuthoritative-from-Document is a + single-hub topology | `ParametricLaws.lean`, `Closure.lean` | tropical-types + Lean | half a day + +| R7 | `reachGrade` monotone in the matrix and in the observed set; observed + modality has full grade (survived; needs `lsum_filter_mono`) | `Closure.lean` + 107-335 | tropical-types Lean | half a day + +| R8 | Multi-witness narrowing: binary one-liner, `Fin n` by induction; "covering + masks ⇒ subsingleton" fails over opaque `ident` and is dropped | + `Echo.agda`, `EchoFiberCount.agda` | echo-types Agda | half a session + +| R9 | Permutation-invariance of `fold (merge resolve)` under a semilattice + `resolve`, by Permutation induction; the only kernel reachable today (PUT + overwrite, `resolve a b = b`) is a non-instance | `Octad.v` 239-309 | Rocq + corollary + Agda twin | one day + +| R10 | Lexicographic progress and ≤ 9-step termination with explicit + `conflict_refl`, `conflict_sym`, `winner_present`, `winner_stable`, + `fill_guarded`, and winner-relative `nconflicts` | `Octad.v`, restated + `Normalizer.v` axioms | Agda source, Rocq and Lean rechecks | 1–2 days + +| R11 | Purity and permutation invariance of the Rust resolve kernel as Creusot + `#[ensures]` against a `#[logic] spec_resolve`; Modality gets a derived total + order; timestamps as `u64` | `conflict.rs` counterexamples | squeakwell + Creusot | 1–2 days incl. toolchain + +| R12 | Observation fidelity at fragment granularity: exported `e : Echo + restrict_T (obs|_T)`, overruled fragments carry a `RepairJustification` | + `Echo.agda`, `EchoProvenance` pattern | Agda record + Creusot export + postcondition | one session + +| R13 | Review-queue completeness over the enumerated candidate fibre: + `hits_y ≡ 0 ⇔ ¬Echo`, `hits_y ≥ 2 ⇒ queued`, `exported ⇒ hits_y ≡ 1`; + needs decidable equality on a concrete `mval` | `EchoFiberCount.agda`, + `EchoTruncation.agda` (wire it) | Agda + Creusot queue predicate | one session + +| R14 | Fibre-blind functionals are constant on the fibre (generic one-line + `refl`); witness-reading confidences are not covered, so confidence ranks + fibres and never selects within one | `EchoEntropy.agda` 258-262 | echo-types + Agda | hours + +| R15 | Reintroduction-statement grading: `∀ f ∈ populated(e). certified_level(stmt(e, f), sch) ≥ 1` + (one DECLARE per populated field) implies every populated field resolves in + the schema; ceiling 6 from text, 4 + for transitions; values never inspected | `vclt-gate` contract v1 | Idris2 + wire contract in squeakwell | small-medium + +| R16 | Additive `RepairJustification` extension reopens no theorem (needs an + `idris2 --build` to confirm) | `Transition.idr` 58-185 | vcl-ut Idris2 | small + +| R17 | Bridge: `nconflicts o = 0 → every computable pairwise drift = 0`; pin + `ThresholdPolicy::Fixed` and `le` boundaries; do not add `le_trans` axioms to + `Drift.v` | `Drift.v` D1/D2 | Rocq, status ASSUMED | hours + +| R18 | *Conjecture*: the enumerated candidate fibre as the Kripke world set + for a Transition-indexed L10 certificate; unstatable until `Epistemic.idr` + line 149 is fixed, `Believes` is separated from `Knows`, and squeakwell has a + completeness argument for its enumeration (else the honest modality is + Believes, KD45) | `Epistemic.idr`, `EchoEpistemic.agda` | research | large +|=== + +**Prover homes per policy.** Theory (R3, R8, R9, R10, R12, R13, R14) is Agda +source of truth in echo-types, rechecked in Rocq inside `verisimdb/formal/` and +in Lean; engineering contracts (R1, R15, R16) are Idris2; first-party Rust +behaviour (R11, the export postcondition, the queue predicate) is Creusot. +Rocq files that exist before the Agda source are target-only evidence. + +**Alternative proof paths, rated** (elegance and correctness first, then +dependability): + +. **Agda-first exactly as above (default arm).** Most elegant: one abstraction + closes both the CROSS-REPO-MAP gap and squeakwell's progress theorem. Slowest + to a first green light because Agda is not installed anywhere in the estate's + CI for this repo. +. **Rocq-first** (`Recovery.v` before the Agda module, cross-documented as + instantiation-first per the standing directive's second clause). Fastest + mechanised result (hours once `coqc` exists, `nix shell nixpkgs#coq` is the + cheapest route). Loses only the policy's source-of-truth ordering, which the + directive explicitly allows when noted. +. **Lean-first via tropical-types** (R5–R7). Lightest toolchain (`elan` + + `lake build`, no Mathlib). Proves the confidence algebra, not the recovery + invariants; good second track in parallel, not a substitute. +. **TLA+ or Alloy model of the fixpoint loop.** Cheap and finds counter-models + fast, but it is a parallel model, which PROOF-POLICY forbids as a substitute + for Creusot on the Rust; acceptable as a design-time oracle only. +. **Property tests only (R0) and stop.** Dependable and immediate; leaves every + ledger row TESTED with bounds, never PROVEN. The floor, not the plan. + +== 7. The empirical gate (before bigger work) + +Each experiment has a metric and a pass criterion; results go into +`docs/EXPERIMENTS.adoc` with run counts. Server-dependent experiments skip with +a message when `SQUEAKWELL_VERISIM_URL` or `SQUEAKWELL_VCLT_GATE` is unset. + +[cols="1,3,3"] +|=== +| Id | Experiment | Pass criterion + +| E1 | Gate throughput: spawn `vclt-gate` for 1,000 statements | p95 ≤ 50 ms; + 1,000 statements ≤ 60 s; else draft the batching escalation to vcl-ut + +| E2 | Absence honesty: raw `verisim-drift` calculators on empty inputs + (negative control) vs the squeakwell layer | raw returns 0.0 (documented + hazard reproduced); squeakwell `quality` is `None`; 1,000 cases + +| E3 | Kernel laws: resolve comm/assoc/idem and permutation invariance + (10,000 cases); guarded fill never overwrites, `|missing|` non-increasing + (10,000); lex progress and ≤ 9 steps (1,000 runs); the counter-model search + finds ≥ 1 case where conflicts rise after fill | 0 violations; ≥ 1 + counter-model found (the test fails if none is found) + +| E4 | Ground truth on `tests/fixtures/damaged-small` (about 20 entities, two + sources, four damage classes) | expected numbers declared up front: all + graph-dropped entities recovered by ASSERT from the other source; the server + path repairs the graph/document-inconsistent ones (and the direction mismatch + is logged); deleted titles and contradicted bodies land in review; zero + fabricated values + +| E5 | Replay determinism: the same journal against two fresh persistent + servers | flags, counts, computable scores and chain lengths agree modulo + UUID and timestamps; local FNV embedding equals the server's bit-for-bit + +| E6 | Gate honesty: 100 % of DECLAREs at 6, NORMALISEs at 4; `EFFECTS` rejected + at L0; a tensor-less NORMALISE admitted and *recorded as evidence* that exit + 0 ≠ repair justified; exit 2 aborts the round before any network effect | + all as stated + +| E7 | Build weight: cold `cargo build` with the chosen dependency set | under + two minutes; no `verisim-*` or `vcltotal-parse` in non-dev dependencies on + the compiler route +|=== + +== 8. The ultracode engineering session + +=== 8.1 Shape + +One session, multi-agent, pipelined. Agents own files, not phases; every task +has a `done_when` that is a command or a grep. Phases: *honest baseline* +(sequential, one agent), *kernel and fixtures* (parallel), *program, gate, +client* (parallel), *lowering and loop* (sequential), *tests, benches, docs* +(parallel), *upstream filings and proof skeletons* (parallel, background). +Cutoff: the session ends when E1–E7 are recorded, whatever their verdict; a +red experiment is a result, not a failure of the session. + +Agent roles: one *kernel* agent (fill, resolve, measure, R0 tests), one +*program* agent (IR, printer, synthesis, golden text), one *seam* agent (gate +client, verisim client, lowering), one *fixture* agent (damaged-small, ground +truth, damage manifest), one *proof-skeleton* agent (Recovery.v draft, +EchoPartialSection.agda draft, Program.idr, Creusot annotations, all marked +"not run here"), one *docs and filings* agent, and a *verifier* agent that only +runs the experiments and refuses to pass anything it did not run. + +=== 8.2 Task graph + +[cols="1,4,2,1,1"] +|=== +| Id | Task | Depends on | Repo | Parallel + +| T01 | Honest baseline: this plan, the honesty commit, clippy warning, + `PROOF-STATUS.adoc` with all rows OPEN, README title and claims, PROOF-NEEDS + split, placeholders outside FFI, Zig decision | — | squeakwell | no +| T02 | Engine stub honesty: `NotImplemented` instead of prose, no fabricated + drift, no `.ok()`, `max_iterations` used or dropped; tests assert the honest + behaviour | T01 | squeakwell | yes +| T03 | Fixture `tests/fixtures/damaged-small`: entities.csv, entities.json, + ground-truth.json, damage-manifest.json, README of expected outcomes | + — | squeakwell | yes +| T04 | `just e2e-deps`: build `vclt-gate` from a pinned vcl-ut commit, podman + image of `verisim-api` (persistent), env vars, honest reporting of what could + not be installed | — | squeakwell | yes +| T05 | `src/fragments`: readers, typing to `OctadSchema`, presence vectors, + candidate lists, gate schema JSON | T03 | squeakwell | yes +| T06 | `src/kernel/resolve.rs`: pure kernel (ModalityPriority, LastWriter + with input timestamps, Union), `nconflicts`, winner; E3(a) tests incl. the + caller-order LWW negative control | T01 | squeakwell | yes +| T07 | `src/kernel/fill.rs`: guarded fill; deterministic regenerators + Document→Vector (FNV port, labelled non-semantic), Graph↔Document + `Relations:`, Semantic→Graph; refuses `SummaryRegenerator`; E3(b) | T01 | + squeakwell | yes +| T08 | `src/kernel/measure.rs`: `mu`, fibre trichotomy, review predicate, + `quality: Option`; E3(c)(d) | T06, T07 | squeakwell | no +| T09 | `src/program`: IR with `SymRef`, params, `RepairJustification`, + requested level ≤ 6 by construction; canonical printer; stability tests | + — | squeakwell | yes +| T10 | `src/gate`: subprocess client per contract v1, exit mapping, 2 s + timeout, certificates with gate commit hash; the four verified cases as + tests | T04, T09 | squeakwell | yes +| T11 | `src/verisim.rs` rewrite: real routes, typed responses with computable + flags, errors propagate, GET after PUT; smoke test behind env var | T04 | + squeakwell | yes +| T12 | `src/program/synth.rs`: round-0 and round-n rules; no NORMALISE for + targets with no server path; golden `round-0.vcl` for the fixture | T05, T08, + T09 | squeakwell | no +| T13 | `src/lower`: certified program → REST plan → execution; bindings + written first; presence pre-check; statement-hash provenance; intent/effect + reconciliation; MERGE refused | T10, T11, T09 | squeakwell | no +| T14 | `src/journal`: round files, `replay`, `diff`, crash-resume including the + two-phase binding (intent before create, confirmation after) and the + unconfirmed-intent reconciliation; done when a kill between create and + confirmation resumes without a duplicate octad | T13 | squeakwell | no +| T15 | `src/engine`: compile–gate–execute–observe–resynthesise loop; fixed + threshold; `mu` trajectory; `NotConverged`; round abort on `GateUnavailable` + | T12, T13, T14 | squeakwell | no +| T16 | `src/review` and `src/export`: review `.vcl` stub; export with + derivation tags observed/derived/unresolved; hard error on exporting a review + entity; `verify` subcommand | T15 | squeakwell | no +| T17 | `tests/e2e_recovery.rs`: E2–E6 as assertions; skips without + dependencies | T16 | squeakwell | no +| T18 | Benches: E1 gate throughput, E7 cold build; replace stub benches | + T10, T14 | squeakwell | yes +| T19 | Upstream issues with file:line evidence and E1/E4 numbers: verisimdb + (propose/apply, create-with-id, `/full`, drift library, Document→Graph, + resolve kernel, fixed threshold, Recovery.v), vcl-ut (weaken, the RECOVER verb + with evidence slot and Residue payload, Epistemic 149, batching, schema builder), echo-types + (EchoPartialSection, EchoFibreIntersection, wire EchoTruncation), + tropical-types (HubCeiling, reachGrade, Isabelle status) | T17, T18 | + elsewhere | yes +| T20 | `verisimdb/formal/Recovery.v` draft with Justfile recipe and + Print-Assumptions whitelist; marked unbuilt if `coqc` absent | T06 | + verisimdb | yes +| T21 | `echo-types` drafts `EchoPartialSection.agda`, `EchoFibreIntersection.agda`; + `All.agda`/`Smoke.agda` wiring; marked "awaiting agda check" | T06 | + echo-types | yes +| T22 | `src/interface/abi/Program.idr`: IR wire format, journal round-trip, + gate request/response; ledger row says whether idris2 ran | T14 | squeakwell + | yes +| T23 | Creusot contracts on `resolve.rs`, `fill.rs`, export; extern specs for + verisim types as ASSUMED rows | T08, T16 | squeakwell | yes +| T24 | Close-out: README/EXPLAINME rewritten to the compiler route with + measured numbers; naming ADR stub; STATE.a2ml; mathesis pointer | T17, T18, + T19 | squeakwell | no +|=== + +Critical path: T01 → T06/T07 → T08 → T12 → T13 → T14 → T15 → T16 → T17 → T24. +Everything else runs beside it. + +=== 8.3 Stop conditions and reporting + +* No agent may mark a ledger row above OPEN unless it ran the prover and names + its version. +* No test counts as passed if it skipped. +* The session report lists E1–E7 with numbers, the measured intent/effect + agreement rate, the review-queue contents on the fixture, and every + file:line the upstream issues cite. + +== 9. Decisions for the owner + +Decided by the owner on 2026-11-05 through the selector. The default arm per +doctrine 15 is marked; where the owner departed from it, the departure is +recorded with its consequence. + +. **Coupling arm: the compiler route (D with A's kernel).** Default arm, + accepted. Option B-first would have waited on six verisimdb routes; A-only + would have duplicated two private server semantics; C added session mapping + and a privacy leak channel for no recovery power. +. **Proof source of truth: Agda first in echo-types.** Default arm, accepted. + `EchoPartialSection.agda` lands first; `verisimdb/formal/Recovery.v` is its + instantiation and the statements are compared per PROOF-POLICY section 3. + Consequence: the first mechanised result waits on an Agda toolchain being + installed where agents run (section 10); the R0 property tests are the + interim evidence. +. **vcl-ut extension: Option 2, a `RECOVER` verb with an evidence slot.** + *Departure from the default arm* (additive `RepairJustification` + constructors). The owner chose the verb. Consequence: `TRecover SubjectRef + RepairJustification (Maybe Expr) SafetyLevel` and `Grammar.Verb VRecover` + reopen the totality cases in `transitionEvidence`, `transitionLevel`, + `transitionVerb`, `subjectsDistinct`, `decTransition`, `enc_transition` and + the gate's `transition_shape`; `certifiedSubjectsDistinct` survives if + `transitionAdmissible` keeps its conjunctive shape. The evidence slot gives + `RECOVER e WHERE drift < $1` the L4 injection-polarity check that NORMALISE + lacks. A rung above 4 still needs a new decider and soundness lemma in the + `Transition.idr` reflection style (for example `residueBounded`). The + additive `Residue` constructors of Option 1 ride inside the same change as the + justification payload, so Option 2 strictly contains Option 1. The upstream + issue (section 10) is filed as Option 2 with this list of reopened cases; + until it lands, squeakwell lowers `RECOVER` lines to `NORMALISE FROM + AUTHORITATIVE` and records the downgrade in the certificate log. +. **The L10 conjecture: parked** behind the three vcl-ut fixes it needs; + squeakwell's epistemic output is labelled Believes (KD45) until a + completeness argument for the enumeration exists. +. **Name: `squeakwell` is kept.** The "Octad-Recover" working title is retired; + the README's naming table stays as the record of the alternatives considered. +. **Zig FFI: `src/interface/ffi` is deleted.** A one-paragraph README records + that an Idris2 ABI must exist before a C-ABI bridge means anything. + +== 10. Beyond this repository + +Issues to file once the MVP numbers exist (T19), one per line: + +* verisimdb: normalizer `propose`/`apply` with `RepairJustification`; client + id on create; `GET /octads/{id}/full` and the update under-report; drift as a + library; Document→Graph and Semantic→Graph regenerators; value-level resolve + kernel and the `AutoMerge` doc/code mismatch; fixed-threshold config and `le` + boundary; `formal/Recovery.v` and the `Normalizer.v` functorisation; the + CROSS-REPO-MAP rows that cite unwired echo-types modules; auth-on and + loopback defaults for recovery deployments. +* vcl-ut: `weaken`; the `RECOVER` verb with evidence slot (owner's choice, Option 2, + carrying the `Residue` payload); `Epistemic.idr` line 149 + and Believes/Knows; batching; exported schema-JSON builder; register + squeakwell as a gate consumer. +* echo-types: `EchoPartialSection`; `EchoFibreIntersection`; wire + `EchoTruncation`; generic fibre-blind lemma; `EchoRecovery` record; check the + AGPL text in `LICENSES/` before any vendoring. +* tropical-types: `HubCeiling.lean`; `reachGrade` and `lsum_filter_mono`; + generic `weightedResidueMeasure`; reconcile the Isabelle status and add a CI + job or banner. +* standards: a note in PROOF-POLICY that `verisimdb/formal/*.v` is target-only + evidence for recovery theory until the Agda source lands. +* mathesis: catalogue row for squeakwell once a proof file exists. +* Toolchains where agents and CI run: `coqc`, `agda` with stdlib, `elan`/`lake`, + `idris2`, Creusot with Why3; record each in `setup.sh`, `guix.scm` and the + container, or record their absence in the ledger. + +== 11. What changed in the README's story + +* "Data that passes all 10 levels is formally verified as recovered" becomes + "the reintroduction statements for e are gate-admissible at level k (≤ 6)". +* "Drift converges monotonically to zero" becomes "the lexicographic measure + decreases; drift is observed, never the criterion, and can rise during fill". +* "Idris2 type kernel with proofs of monotonicity and determinism" becomes + "no proofs yet; the repaired statements and their prover homes are in + section 3 and 6; the ledger is `PROOF-STATUS.adoc`". +* "NER and embeddings via ML" becomes "deterministic regeneration only; + Document→Vector is a hash fingerprint labelled non-semantic". +* Phase 5 becomes the fixpoint-plus-gate-plus-provenance criterion. diff --git a/setup.sh b/setup.sh index f75b158..c347949 100755 --- a/setup.sh +++ b/setup.sh @@ -165,7 +165,7 @@ install_just_release() ( trap 'rm -rf "$just_tmp"' 0 trap 'exit 1' 1 2 3 15 just_archive="$just_tmp/just.$just_extension" - curl -fsSL "https://github.com/casey/just/releases/download/$just_version/just-$just_version-$just_target.$just_extension" \ + curl --proto "=https" --tlsv1.2 -fsSL "https://github.com/casey/just/releases/download/$just_version/just-$just_version-$just_target.$just_extension" \ -o "$just_archive" || exit 1 if command -v sha256sum >/dev/null 2>&1; then diff --git a/src/abi/mod.rs b/src/abi/mod.rs index 13cad94..fecea4f 100644 --- a/src/abi/mod.rs +++ b/src/abi/mod.rs @@ -2,28 +2,60 @@ // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) // // ABI module for SqueakWell. -// Idris2 proofs for recovery correctness: // -// MonotonicConvergence: -// ∀ phase p, iteration i. -// drift(p, i+1) ≤ drift(p, i) -// Constraint propagation never increases drift. +// STATUS (2026-11-04): no Idris2 proofs exist in this repository yet. The +// template ABI was removed on 2026-03-29 because it gave a false impression +// of formal verification (see PROOF-NEEDS.adoc). This file records the +// invariants the engine is designed to satisfy, in the form that an honest +// mechanisation can actually target. The proof route, prover homes and +// the rungs that already exist upstream are in docs/ROUTE-PLAN.adoc. +// +// The five invariants, restated after adversarial review against +// verisimdb/formal/*.v and vcl-ut/src/core/*.idr: +// +// Progress (replaces "MonotonicConvergence"): +// Real-valued drift is NOT monotone under fill-then-resolve: filling a +// missing modality turns an unmeasurable pair into a measurable, +// possibly disagreeing one, so drift can rise in Phase 2. The honest +// measure is lexicographic on naturals: +// mu(o) = (|missing o|, nconflicts o) +// and the theorem is: step o = o \/ mu(step o) Some only) is inflationary on the information +// order of partial octads and never overwrites an observed value. It is +// NOT monotone on that order: for x below y, fill x may infer a value +// that y already holds differently. Resolve copies the winner and never +// un-fills. Fixpoint within <= 8 fill steps (modality_cardinality) +// plus one resolve pass (normalize_idempotent). // // IdentityPreservation: -// ∀ entity e, modality m₁ m₂. -// infer(e, m₁) consistent_with observe(e, m₂) -// Cross-modal inference preserves entity identity. +// Every recovery operation preserves the entity identifier +// (verisimdb Octad.v: project_preserves_id, merge_preserves_id, +// enrich_preserves_id — a 3-line induction gives the iterated form), +// and guarded fill never overwrites an observed value. "Inferred agrees +// with observed" is NOT a theorem; disagreement is exactly what Phase 3 +// resolves and what the review queue records. // // DeterministicResolution: -// ∀ conflict c, input I. -// resolve(c, I) = resolve(c, I) -// Same conflict + same input → same resolution. No randomness. +// resolve is a pure function of its inputs and invariant under +// permutation of the fragment list (no clock, no caller ordering). +// This holds for ModalityPriority; LastWriterWins needs explicit +// timestamps carried IN the input, not caller order. // // TypeRatchetSoundness: -// ∀ entity e, level n. -// passes(e, n) → ∀ m ≤ n. passes(e, m) -// Passing level N implies passing all levels below N. +// Certified level N implies certified at every level below N. Already +// proven for VCL-UT statements and transitions (Levels.idr); squeakwell +// only instantiates it, by grading the canonical DECLARE / NORMALISE +// transition that would reintroduce each recovered entity. Only L0-L6 +// are expressible from VCL source today (vcl-ut #25), so the ratchet is +// capped at L6 until that gap closes. +// +// Termination (replaces "TerminationGuarantee"): +// The lexicographic measure is well-founded on nat*nat, so the loop +// reaches a fixpoint without needing max_iterations; max_iterations is +// an operational budget, not the termination argument. // -// TerminationGuarantee: -// ∀ workload w. ∃ i. drift(w, i) < threshold ∨ i = max_iterations -// Recovery always terminates (either converges or gives up). +// Soundness of the output ("never export corrupt data") is stated +// separately, in echo-types vocabulary: every exported entity inhabits the +// fibre of the damage map over the accepted fragments, every exported entity +// has a singleton enumerated fibre (hits_y = 1), and every non-singleton +// fibre is in the review queue and is refused by export. diff --git a/src/interface/ffi/README.adoc b/src/interface/ffi/README.adoc index 8fe57d3..859004a 100644 --- a/src/interface/ffi/README.adoc +++ b/src/interface/ffi/README.adoc @@ -1 +1,12 @@ -= ffi Logic +// SPDX-License-Identifier: CC-BY-SA-4.0 += ffi (deliberately empty) + +The Zig C-ABI bridge template that lived here was deleted on 2026-11-05 by +owner decision (`docs/ROUTE-PLAN.adoc` section 9). It was never built: its +`build.zig` referenced an include file and a bench that did not exist, and +there is no Idris2 ABI for it to bridge. Under the hyperpolymath ABI-FFI +standard the truth lives in `../abi/` as Idris2 and the Zig implementation +follows it; until `src/interface/abi/Program.idr` (the program IR, journal and +gate wire contracts, task T22 in the route plan) exists, a bridge here would +describe nothing. This directory and its manifest are kept so the interface +unit's `canonical_locations` stay valid. diff --git a/src/interface/ffi/build.zig b/src/interface/ffi/build.zig deleted file mode 100644 index 4a2e049..0000000 --- a/src/interface/ffi/build.zig +++ /dev/null @@ -1,94 +0,0 @@ -// {{PROJECT}} FFI Build Configuration -// SPDX-License-Identifier: MPL-2.0 - -const std = @import("std"); - -pub fn build(b: *std.Build) void { - const target = b.standardTargetOptions(.{}); - const optimize = b.standardOptimizeOption(.{}); - - // Shared library (.so, .dylib, .dll) - const lib = b.addSharedLibrary(.{ - .name = "{{project}}", - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }); - - // Set version - lib.version = .{ .major = 0, .minor = 1, .patch = 0 }; - - // Static library (.a) - const lib_static = b.addStaticLibrary(.{ - .name = "{{project}}", - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }); - - // Install artifacts - b.installArtifact(lib); - b.installArtifact(lib_static); - - // Generate header file for C compatibility - const header = b.addInstallHeader( - b.path("include/{{project}}.h"), - "{{project}}.h", - ); - b.getInstallStep().dependOn(&header.step); - - // Unit tests - const lib_tests = b.addTest(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = optimize, - }); - - const run_lib_tests = b.addRunArtifact(lib_tests); - - const test_step = b.step("test", "Run library tests"); - test_step.dependOn(&run_lib_tests.step); - - // Integration tests - const integration_tests = b.addTest(.{ - .root_source_file = b.path("test/integration_test.zig"), - .target = target, - .optimize = optimize, - }); - - integration_tests.linkLibrary(lib); - - const run_integration_tests = b.addRunArtifact(integration_tests); - - const integration_test_step = b.step("test-integration", "Run integration tests"); - integration_test_step.dependOn(&run_integration_tests.step); - - // Documentation - const docs = b.addTest(.{ - .root_source_file = b.path("src/main.zig"), - .target = target, - .optimize = .Debug, - }); - - const docs_step = b.step("docs", "Generate documentation"); - docs_step.dependOn(&b.addInstallDirectory(.{ - .source_dir = docs.getEmittedDocs(), - .install_dir = .prefix, - .install_subdir = "docs", - }).step); - - // Benchmark (if needed) - const bench = b.addExecutable(.{ - .name = "{{project}}-bench", - .root_source_file = b.path("bench/bench.zig"), - .target = target, - .optimize = .ReleaseFast, - }); - - bench.linkLibrary(lib); - - const run_bench = b.addRunArtifact(bench); - - const bench_step = b.step("bench", "Run benchmarks"); - bench_step.dependOn(&run_bench.step); -} diff --git a/src/interface/ffi/src/0.4-AI-MANIFEST.a2ml b/src/interface/ffi/src/0.4-AI-MANIFEST.a2ml deleted file mode 100644 index 5b5f1b1..0000000 --- a/src/interface/ffi/src/0.4-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 ---- -### [META] -id: "src-unit" -level: 4 -parent: "../0.3-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Src logic at level 4. diff --git a/src/interface/ffi/src/README.adoc b/src/interface/ffi/src/README.adoc deleted file mode 100644 index a5c0c6d..0000000 --- a/src/interface/ffi/src/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Src Logic diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig deleted file mode 100644 index 6b233bc..0000000 --- a/src/interface/ffi/src/main.zig +++ /dev/null @@ -1,274 +0,0 @@ -// {{PROJECT}} FFI Implementation -// -// This module implements the C-compatible FFI declared in src/abi/Foreign.idr -// All types and layouts must match the Idris2 ABI definitions. -// -// SPDX-License-Identifier: MPL-2.0 - -const std = @import("std"); - -// Version information (keep in sync with project) -const VERSION = "0.1.0"; -const BUILD_INFO = "{{PROJECT}} built with Zig " ++ @import("builtin").zig_version_string; - -/// Thread-local error storage -threadlocal var last_error: ?[]const u8 = null; - -/// Set the last error message -fn setError(msg: []const u8) void { - last_error = msg; -} - -/// Clear the last error -fn clearError() void { - last_error = null; -} - -//============================================================================== -// Core Types (must match src/abi/Types.idr) -//============================================================================== - -/// Result codes (must match Idris2 Result type) -pub const Result = enum(c_int) { - ok = 0, - @"error" = 1, - invalid_param = 2, - out_of_memory = 3, - null_pointer = 4, -}; - -/// Library handle (opaque to prevent direct access) -pub const Handle = opaque { - // Internal state hidden from C - allocator: std.mem.Allocator, - initialized: bool, - // Add your fields here -}; - -//============================================================================== -// Library Lifecycle -//============================================================================== - -/// Initialize the library -/// Returns a handle, or null on failure -export fn {{project}}_init() ?*Handle { - const allocator = std.heap.c_allocator; - - const handle = allocator.create(Handle) catch { - setError("Failed to allocate handle"); - return null; - }; - - // Initialize handle - handle.* = .{ - .allocator = allocator, - .initialized = true, - }; - - clearError(); - return handle; -} - -/// Free the library handle -export fn {{project}}_free(handle: ?*Handle) void { - const h = handle orelse return; - const allocator = h.allocator; - - // Clean up resources - h.initialized = false; - - allocator.destroy(h); - clearError(); -} - -//============================================================================== -// Core Operations -//============================================================================== - -/// Process data (example operation) -export fn {{project}}_process(handle: ?*Handle, input: u32) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Example processing logic - _ = input; - - clearError(); - return .ok; -} - -//============================================================================== -// String Operations -//============================================================================== - -/// Get a string result (example) -/// Caller must free the returned string -export fn {{project}}_get_string(handle: ?*Handle) ?[*:0]const u8 { - const h = handle orelse { - setError("Null handle"); - return null; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return null; - } - - // Example: allocate and return a string - const result = h.allocator.dupeZ(u8, "Example result") catch { - setError("Failed to allocate string"); - return null; - }; - - clearError(); - return result.ptr; -} - -/// Free a string allocated by the library -export fn {{project}}_free_string(str: ?[*:0]const u8) void { - const s = str orelse return; - const allocator = std.heap.c_allocator; - - const slice = std.mem.span(s); - allocator.free(slice); -} - -//============================================================================== -// Array/Buffer Operations -//============================================================================== - -/// Process an array of data -export fn {{project}}_process_array( - handle: ?*Handle, - buffer: ?[*]const u8, - len: u32, -) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; - }; - - const buf = buffer orelse { - setError("Null buffer"); - return .null_pointer; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Access the buffer - const data = buf[0..len]; - _ = data; - - // Process data here - - clearError(); - return .ok; -} - -//============================================================================== -// Error Handling -//============================================================================== - -/// Get the last error message -/// Returns null if no error -export fn {{project}}_last_error() ?[*:0]const u8 { - const err = last_error orelse return null; - - // Return C string (static storage, no need to free) - const allocator = std.heap.c_allocator; - const c_str = allocator.dupeZ(u8, err) catch return null; - return c_str.ptr; -} - -//============================================================================== -// Version Information -//============================================================================== - -/// Get the library version -export fn {{project}}_version() [*:0]const u8 { - return VERSION.ptr; -} - -/// Get build information -export fn {{project}}_build_info() [*:0]const u8 { - return BUILD_INFO.ptr; -} - -//============================================================================== -// Callback Support -//============================================================================== - -/// Callback function type (C ABI) -pub const Callback = *const fn (u64, u32) callconv(.C) u32; - -/// Register a callback -export fn {{project}}_register_callback( - handle: ?*Handle, - callback: ?Callback, -) Result { - const h = handle orelse { - setError("Null handle"); - return .null_pointer; - }; - - const cb = callback orelse { - setError("Null callback"); - return .null_pointer; - }; - - if (!h.initialized) { - setError("Handle not initialized"); - return .@"error"; - } - - // Store callback for later use - _ = cb; - - clearError(); - return .ok; -} - -//============================================================================== -// Utility Functions -//============================================================================== - -/// Check if handle is initialized -export fn {{project}}_is_initialized(handle: ?*Handle) u32 { - const h = handle orelse return 0; - return if (h.initialized) 1 else 0; -} - -//============================================================================== -// Tests -//============================================================================== - -test "lifecycle" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - try std.testing.expect({{project}}_is_initialized(handle) == 1); -} - -test "error handling" { - const result = {{project}}_process(null, 0); - try std.testing.expectEqual(Result.null_pointer, result); - - const err = {{project}}_last_error(); - try std.testing.expect(err != null); -} - -test "version" { - const ver = {{project}}_version(); - const ver_str = std.mem.span(ver); - try std.testing.expectEqualStrings(VERSION, ver_str); -} diff --git a/src/interface/ffi/test/0.4-AI-MANIFEST.a2ml b/src/interface/ffi/test/0.4-AI-MANIFEST.a2ml deleted file mode 100644 index e02427f..0000000 --- a/src/interface/ffi/test/0.4-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 ---- -### [META] -id: "test-unit" -level: 4 -parent: "../0.3-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Test logic at level 4. diff --git a/src/interface/ffi/test/README.adoc b/src/interface/ffi/test/README.adoc deleted file mode 100644 index f6f38bf..0000000 --- a/src/interface/ffi/test/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Test Logic diff --git a/src/interface/ffi/test/integration_test.zig b/src/interface/ffi/test/integration_test.zig deleted file mode 100644 index 0341994..0000000 --- a/src/interface/ffi/test/integration_test.zig +++ /dev/null @@ -1,182 +0,0 @@ -// {{PROJECT}} Integration Tests -// SPDX-License-Identifier: MPL-2.0 -// -// These tests verify that the Zig FFI correctly implements the Idris2 ABI - -const std = @import("std"); -const testing = std.testing; - -// Import FFI functions -extern fn {{project}}_init() ?*opaque {}; -extern fn {{project}}_free(?*opaque {}) void; -extern fn {{project}}_process(?*opaque {}, u32) c_int; -extern fn {{project}}_get_string(?*opaque {}) ?[*:0]const u8; -extern fn {{project}}_free_string(?[*:0]const u8) void; -extern fn {{project}}_last_error() ?[*:0]const u8; -extern fn {{project}}_version() [*:0]const u8; -extern fn {{project}}_is_initialized(?*opaque {}) u32; - -//============================================================================== -// Lifecycle Tests -//============================================================================== - -test "create and destroy handle" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - try testing.expect(handle != null); -} - -test "handle is initialized" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - const initialized = {{project}}_is_initialized(handle); - try testing.expectEqual(@as(u32, 1), initialized); -} - -test "null handle is not initialized" { - const initialized = {{project}}_is_initialized(null); - try testing.expectEqual(@as(u32, 0), initialized); -} - -//============================================================================== -// Operation Tests -//============================================================================== - -test "process with valid handle" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - const result = {{project}}_process(handle, 42); - try testing.expectEqual(@as(c_int, 0), result); // 0 = ok -} - -test "process with null handle returns error" { - const result = {{project}}_process(null, 42); - try testing.expectEqual(@as(c_int, 4), result); // 4 = null_pointer -} - -//============================================================================== -// String Tests -//============================================================================== - -test "get string result" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - const str = {{project}}_get_string(handle); - defer if (str) |s| {{project}}_free_string(s); - - try testing.expect(str != null); -} - -test "get string with null handle" { - const str = {{project}}_get_string(null); - try testing.expect(str == null); -} - -//============================================================================== -// Error Handling Tests -//============================================================================== - -test "last error after null handle operation" { - _ = {{project}}_process(null, 0); - - const err = {{project}}_last_error(); - try testing.expect(err != null); - - if (err) |e| { - const err_str = std.mem.span(e); - try testing.expect(err_str.len > 0); - } -} - -test "no error after successful operation" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - _ = {{project}}_process(handle, 0); - - // Error should be cleared after successful operation - // (This depends on implementation) -} - -//============================================================================== -// Version Tests -//============================================================================== - -test "version string is not empty" { - const ver = {{project}}_version(); - const ver_str = std.mem.span(ver); - - try testing.expect(ver_str.len > 0); -} - -test "version string is semantic version format" { - const ver = {{project}}_version(); - const ver_str = std.mem.span(ver); - - // Should be in format X.Y.Z - try testing.expect(std.mem.count(u8, ver_str, ".") >= 1); -} - -//============================================================================== -// Memory Safety Tests -//============================================================================== - -test "multiple handles are independent" { - const h1 = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(h1); - - const h2 = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(h2); - - try testing.expect(h1 != h2); - - // Operations on h1 should not affect h2 - _ = {{project}}_process(h1, 1); - _ = {{project}}_process(h2, 2); -} - -test "double free is safe" { - const handle = {{project}}_init() orelse return error.InitFailed; - - {{project}}_free(handle); - {{project}}_free(handle); // Should not crash -} - -test "free null is safe" { - {{project}}_free(null); // Should not crash -} - -//============================================================================== -// Thread Safety Tests (if applicable) -//============================================================================== - -test "concurrent operations" { - const handle = {{project}}_init() orelse return error.InitFailed; - defer {{project}}_free(handle); - - const ThreadContext = struct { - h: *opaque {}, - id: u32, - }; - - const thread_fn = struct { - fn run(ctx: ThreadContext) void { - _ = {{project}}_process(ctx.h, ctx.id); - } - }.run; - - var threads: [4]std.Thread = undefined; - for (&threads, 0..) |*thread, i| { - thread.* = try std.Thread.spawn(.{}, thread_fn, .{ - ThreadContext{ .h = handle, .id = @intCast(i) }, - }); - } - - for (threads) |thread| { - thread.join(); - } -} diff --git a/tests/e2e_test.rs b/tests/e2e_test.rs index ff04bcc..d8dcd43 100644 --- a/tests/e2e_test.rs +++ b/tests/e2e_test.rs @@ -5,7 +5,6 @@ // Each test exercises the complete ingest → recover → export flow using a // temporary working directory so nothing leaks between tests. -use std::path::Path; use tempfile::TempDir; // ─── Helpers ────────────────────────────────────────────────────────────────