diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index cc3d58f..4aec155 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -36,9 +36,10 @@ issues = [ [critical-next-actions] actions = [ "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", + "Run the empirical gate E1-E7 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", + "Proof ledger PROOF-STATUS.adoc (2026-11-09): R2-R10 and R12/R13 theory halves PROVEN in verisimdb/echo-types/tropical-types; R0, R1, R11, R15, R16 OPEN; R17 ASSUMED", + "File the cross-repo issues listed in docs/ROUTE-PLAN.adoc section 10", ] [maintenance-status] diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index ac653d2..c94d4f6 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -98,7 +98,7 @@ This repo follows the **Dual-Track** architecture: ├── src/ # Source code │ └── interface/ # Verified Interface Seams │ ├── abi/ # Idris2 ABI (The Spec) -│ ├── ffi/ # Zig FFI (The Bridge) +│ ├── ffi/ # Reserved for the FFI bridge (template deleted 2026-11-05; see its README) │ └── generated/ # C Headers (The Result) ├── container/ # Stapeln container ecosystem ├── docs/ # Technical depths diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 585bd50..f535447 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -11,7 +11,7 @@ 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 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`. +*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) aims at cardinality bounds and linearity, which VCL-total places at Levels 7-10; the gate ceiling today is L6, so Phase 5 is capped there until vcl-ut certifies higher levels from source. `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 diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index cbf206a..5315b64 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -3,10 +3,19 @@ === Current State * *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. +* *Languages*: Rust only. The unbuilt Zig FFI template was deleted on 2026-11-05 (see `src/interface/ffi/README.adoc`); no Idris2 source yet +* *Existing proofs*: none in this repository. No `.idr` file exists (the + template ABI was removed on 2026-03-29, see below). The proofs that DO + exist for squeakwell's invariants live in their estate homes — verisimdb + `formal/Recovery.v` (Rocq), echo-types `EchoPartialSection.agda` + + `EchoFibreIntersection.agda` (Agda), tropical-types + `Resource/HubCeiling.lean` (Lean) — and are ledgered per rung, with + receipts, in link:PROOF-STATUS.adoc[PROOF-STATUS.adoc] (2026-11-09). + These are *theory* results over abstract carriers. In particular the + Lean hub-ceiling lemmas hold for any resource algebra whose unit is top; + their application to squeakwell's f64 confidence scores (the quantisation + layer onto an ℕ-based `MinPlus` carrier, and the walk semantics of + `matStar`) is not proved anywhere and stays OPEN (ledger R6, R7 notes). * *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). diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..fac2438 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,192 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += squeakwell — Proof Status (ledger) +:toc: +:revdate: 2026-11-09 + +Requirements: link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc]. Ladder and repaired +statements: link:docs/ROUTE-PLAN.adoc[docs/ROUTE-PLAN.adoc] sections 3 and 6. +Estate rules: standards `3-practice/PROOF-POLICY.adoc`. Mathesis register: +`mathesis/docs/status/CROSS-PROVER-RECONCILIATION.adoc`. + +[IMPORTANT] +==== +A row says *PROVEN* or *PROVEN-WITH-AXIOMS* only where the named prover ran +on the named file in a recorded environment, with the receipt below. Nothing +in `src/` is covered by any row: the Rust engine is a stub and the Creusot +and Idris2 homes have no source yet. Grades are per theorem, not per repo. +==== + +== Status vocabulary + +PROVEN (kernel-checked, no axioms beyond the prover's logic) · +PROVEN-WITH-AXIOMS (kernel-checked; the axioms are listed) · TESTED (runnable +check, not a proof) · ASSUMED (used as a hypothesis, not discharged) · OPEN. + +== Ledger (one row per rung) + +[cols="1,4,2,2,3",options="header"] +|=== +|Rung |Statement (repaired form) |Home |Status |Artefact / receipt + +|R0 |Proptest laws for the resolve kernel; fill never overwrites; `mu` +lex-decreases or fixpoint; a case where conflicts rise after fill |squeakwell +`tests/` |OPEN |No property harness yet (`TEST-NEEDS.adoc`: fixed-input +fixtures only). + +|R1 |`weaken : SafetyCertificate s sch n -> CanWeakenStar n m -> +SafetyCertificate s sch m` |vcl-ut Idris2 |OPEN |Not started. + +|R2 |Identity persists through every recovery round, for every oracle |Rocq, +verisimdb `formal/Recovery.v` |PROVEN-WITH-AXIOMS |`step_preserves_id`, +`iter_preserves_id`. Axioms: none beyond Octad.v's parameters `mval`, `ident` +(`Print Assumptions` for both lemmas — receipt C1). + +|R3 |Guarded fill is inflationary on the information order and NOT monotone +on it |Agda source: echo-types `EchoPartialSection.agda`; Rocq recheck +`Recovery.v` |PROVEN (Agda) / PROVEN-WITH-AXIOMS (Rocq) |Agda: +`fill-guarded`, `fill-inflationary`, `FillNotMonotone.fill-not-monotone` +(pointwise, funext-free). Rocq: `fill_guarded`, `fill_inflationary`, +`fill_not_monotone` — all three on `mval`, `ident` only (no +`functional_extensionality_dep`; the counter-model is decided by `Nat.eqb` +on concrete octads, so no function equality is needed). Audit modalities by +chain prefix: verisimdb `Provenance.v`, not re-proved here. + +|R4 |Counter-model: filling can raise the conflict count |Rocq `Recovery.v` +|PROVEN-WITH-AXIOMS |`fill_can_raise_conflicts` (0 → 2 ordered conflicting +pairs) under hypotheses `conflict a a = false`, `conflict a b = true`. The +runnable witness in verisim-api `drift_compute.rs` is TESTED-level evidence, +not a proof. + +|R5 |`weightedResidueMeasure w : ResidueMeasure (List M) R` for any resource +algebra |Lean, tropical-types `Resource/HubCeiling.lean` |PROVEN +|`weightedResidueMeasure`, `weightedMeasure_append`; `#print axioms`: none. +Constant-weight instance `weighted_counts_events` (propext, Quot.sound). + +|R6 |Element lemma `a ⊠ b ⊑ a` when `one` is top; matrix and star corollaries +|Lean `HubCeiling.lean` |PROVEN / PROVEN-WITH-AXIOMS |`factor_le`, +`factor_le_right`, `zero_bot`, `join_bound`, `lsum_bound` (no axioms); +`single_hub_ceiling`, `single_hub_star_ceiling` (propext, Quot.sound). The +star corollary holds only under the explicit `IsStar` fixed-point hypothesis +(no walk semantics for `matStar` in Lean). `OneTop` discharged at MinPlus and +MinMax; refuted at MaxPlus (`maxplus_not_one_top`). + +|R7 |`reachGrade` monotone in the matrix and in the observed set; observed +node has full grade |Lean `HubCeiling.lean` |PROVEN / PROVEN-WITH-AXIOMS +|`lsum_filter_mono`, `reachGrade_mono_mat`, `reachGrade_mono_set` (no +axioms); `one_le_reachGrade` (propext, Quot.sound). + +|R8 |Multi-witness narrowing: binary iso, `Fin n` steps, count shrinks |Agda +echo-types `EchoFibreIntersection.agda` |PROVEN |`fibre-intersection-iso`, +`forget-left-witness`, `forget-right-witness`, `narrow-fin-step-to/from`, +`narrow-shrinks`. "Covering masks ⇒ subsingleton" dropped (needs +extensionality over opaque identifiers). + +|R9 |Permutation invariance of the merge fold under a semilattice resolve; +PUT kernel is a non-instance |Agda `EchoPartialSection.agda` (merge laws); +Rocq `Recovery.v` (fold) |PROVEN (Agda laws) / PROVEN-WITH-AXIOMS (Rocq fold) +|Agda: `merge-comm`, `merge-assoc`, `merge-idem` (pointwise, implications +from `resolve`). Rocq: `fold_merge_perm` (same-identifier batch, commutative ++ associative resolve; uses `functional_extensionality_dep` because `merge_swap` +rewrites octads as functions), `put_commutative_iff_trivial` (`mval` only). + +|R10 |Lexicographic progress and ≤ 9-round termination with explicit +hypotheses |Rocq `Recovery.v` |PROVEN-WITH-AXIOMS |`step_progress`, +`iter_bounded`, `iter_9_fixpoint`, `iter_9_no_conflicts`. Hypotheses +explicit: `conflict_refl`, `winner_some`. Axioms: `step_progress` and +`iter_9_fixpoint` use `functional_extensionality_dep` (octad-as-function +equalities); `iter_9_no_conflicts` uses `mval`, `ident` only. Not restated in Agda or Lean (needs +the finite octad and a conflict test); the ladder said "Agda source, Rocq and +Lean rechecks" — Rocq is the source for this rung. + +|R11 |Purity and permutation invariance of the Rust resolve kernel |squeakwell +Creusot |OPEN |No Creusot source; toolchain not installed. + +|R12 |Observation fidelity at fragment granularity |Agda +`EchoPartialSection.agda` |PROVEN (theory half) / OPEN (Creusot export +postcondition) |`restrict-fibre-agree` (`e : Echo (restrict T) obs` agrees +with `obs` on every observed modality), `restrict-blind`, `restrict-echo`. +`RepairJustification` on overruled fragments: not started. + +|R13 |Review-queue completeness over the enumerated candidate fibre |Agda +echo-types (`EchoFiberCount`, `EchoTruncation`, `EchoFibreIntersection`) +|PROVEN (theory half) / OPEN (Creusot queue predicate) |`hits_y ≡ 0 ⇔ +¬Echo`: `FiberSize-fin≡0⇒no-echo`, `no-echo⇒FiberSize-fin≡0` (pre-existing). +`hits_y ≥ 2 ⇒` two distinct echoes: `echo-not-prop` / +`preimages⇒distinct-echoes` (`EchoTruncation`, wired 2026-11-09). Narrowing +cannot grow the queue: `narrow-shrinks`. The engine predicate itself: OPEN. + +|R14 |Fibre-blind functionals are constant on the fibre |Agda echo-types +`EchoEntropy.agda` |PROVEN (pre-existing) |`entropy-blind-parametric` +(any functional of any fibre-determined distribution is witness-blind); +confidence ranks fibres, never selects within one. + +|R15 |Reintroduction-statement grading ≥ 1 implies every populated field +resolves |Idris2 wire contract in squeakwell |OPEN |`vclt-gate` v1 behaviour +is TESTED (live run in the 2026-11 survey); no Idris2 contract yet. + +|R16 |Additive `RepairJustification` extension reopens no theorem |vcl-ut +Idris2 |OPEN |Needs an `idris2 --build`. + +|R17 |`nconflicts o = 0 → every computable pairwise drift = 0` |Rocq, +verisimdb `Drift.v` |ASSUMED |Not stated; `Drift.v` D1/D2 untouched. + +|R18 |Enumerated candidate fibre as a Kripke world set (conjecture) |research +|OPEN |Unstatable until vcl-ut `Epistemic.idr` line 149 is fixed and +`Believes` is separated from `Knows`. +|=== + +== Receipts (2026-11-09, this session's environment) + +[cols="1,3,3",options="header"] +|=== +|Id |Toolchain and command |Result + +|C1 |Coq 8.18.0 (Ubuntu 24.04 apt). `cd verisimdb/formal && coqc -q Octad.v +&& coqc -q Recovery.v > Recovery.out`; whitelist +`awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Recovery.out \| sort -u` +|Exit 0 in 1.8 s. Union of assumptions over all twelve `Print Assumptions` +blocks: `mval`, `ident`, `functional_extensionality_dep` — identical to the +`Octad.v` whitelist. Per lemma (re-run 2026-11-09 after review): `mval`, +`ident` only for `fill_guarded`, `fill_inflationary`, `fill_not_monotone`, +`fill_can_raise_conflicts`, `normalise_no_conflicts`, `step_preserves_id`, +`iter_preserves_id`, `iter_9_no_conflicts`; `mval` only for +`put_commutative_iff_trivial`; `mval`, `ident`, `functional_extensionality_dep` +for `step_progress`, `iter_9_fixpoint`, `fold_merge_perm` (the three that +rewrite an octad as a function). The nine pre-existing modules also compile +and pass their Justfile whitelists. PR: +https://github.com/hyperpolymath/verisimdb/pull/350. + +|A1 |Agda 2.7.0.1 (echo-types `scripts/setup-agda.sh`, checksum-pinned), +agda-stdlib `8326c7475af1fa456ca04a0203c168d5d7ff842b`, absolute-zero +`f486c29903434589117fa0662c6f29b0f17d1d5f`. `agda --no-libraries -i +$AGDA_STDLIB -i $ABSOLUTE_ZERO_AGDA --safe --without-K --cubical-compatible +-i proofs/agda ` on `EchoPartialSection.agda`, +`EchoFibreIntersection.agda`, then `All.agda` and `Smoke.agda`. +|Both new modules exit 0 (warnings: `UnsupportedIndexedMatch` only, the same +class the existing suite emits). `All.agda` and `Smoke.agda` exit 0 before the +wiring; the post-wiring run is recorded in the echo-types PR. Zero postulates; +`scripts/kernel-guard.sh` PASS. + +|L1 |Lean 4.35.0 via elan (`lean-toolchain` pin). `cd tropical-types && lake +build`; then `lake env lean axcheck.lean` with `#print axioms` on every new +headline. +|`Build completed successfully (21 jobs)`. Axioms: none for `factor_le`, +`factor_le_right`, `zero_bot`, `join_bound`, `lsum_bound`, +`lsum_filter_mono`, `reachGrade_mono_mat`, `reachGrade_mono_set`, +`weightedResidueMeasure`, `weightedMeasure_append` (re-checked 2026-11-09); +`[propext, Quot.sound]` for the others. No +`sorry`, no `Classical.choice`. PR: +https://github.com/hyperpolymath/tropical-types/pull/67. +|=== + +== What is NOT covered + +* Nothing about the Rust in `src/` is proved. The engine is a stub (see + `EXPLAINME.adoc`); the Creusot rows (R11, the R12/R13 engineering halves) + and the Idris2 rows (R1, R15, R16) are OPEN. +* The empirical gate E1–E7 in the route plan has not been run. +* Cross-prover correspondence between the Agda and Rocq statements of R3/R9 is + a *refinement* (pointwise vs. function equality under + `functional_extensionality_dep`), recorded as BRIDGE-PENDING in the mathesis + register until a checked translation exists. diff --git a/README.adoc b/README.adoc index 6af0625..e96aae5 100644 --- a/README.adoc +++ b/README.adoc @@ -61,7 +61,7 @@ Damaged data (fragments, corruption, inconsistencies) Drift score: ~0.15 │ ▼ - PHASE 5 — CONVERGENCE (VCL-total Levels 7-10) + PHASE 5 — CONVERGENCE (gate ceiling L6; VCL-total Levels 7-10 are future vcl-ut work) Cardinality bounds, effect tracking, temporal consistency, linearity. 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). @@ -116,18 +116,27 @@ function: recovery is complete when cross-modal drift approaches zero. - Phase 1: Loose acceptance + schema inference - Phase 2: Cross-modal inference (fill missing modalities) - Phase 3: Conflict resolution (provenance + temporal + semantic arbitration) - - Phase 4: Type tightening (VCL-total levels 4-6) - - Phase 5: Convergence (VCL-total levels 7-10) - -* **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: + - Phase 4: Type tightening (VCL-total levels 4-6; gating planned, the stub does not yet invoke `vclt-gate`) + - Phase 5: Convergence (no gate level beyond Phase 4's planned L6 ceiling; VCL-total levels 7-10 are future vcl-ut work) + +* **Invariants** (`src/abi/mod.rs`) — the engine is designed so that the + following hold. No proof lives in this repository and the Rust engine itself + is unproved; the *theory* behind rungs R2–R10 (identity preservation through + every round, guarded fill inflationary but not monotone, the conflict-raising + counter-model, fold permutation invariance, bounded termination, the + fibre-intersection and hub-ceiling lemmas) is mechanised in its estate homes + and ledgered with prover receipts in link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]; + the prover homes per estate PROOF-POLICY are in `docs/ROUTE-PLAN.adoc`: - 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-UT integration** — Uses the `vclt-gate` binary (hyperpolymath/vcl-ut) as the certifier. - Each phase invokes progressively stricter VCL-total levels. +* **VCL-UT integration** (planned) — The `vclt-gate` binary (hyperpolymath/vcl-ut) + is the certifier. Phase 1 is to gate at L1–3 and Phase 4 at L4–6, the L6 + ceiling vcl-ut certifies from source today; Phase 5 adds no further gate level + (L7–10 are future vcl-ut work). The current engine stub prints the level names + and does not yet invoke the gate, so no phase certifies anything today. * **Output** — Reconstructed database in VeriSimDB format (all 8 modalities populated), with per-entity confidence scores, proof certificates, and @@ -235,10 +244,14 @@ function: recovery is complete when cross-modal drift approaches zero. == Status -**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`. +**Concept stage (2026-11-05; proof ledger 2026-11-09).** Architecture sketched, +phases defined, engine and client are stubs. No proof lives in this repository +and nothing about the Rust engine is proved; the first mechanised *theory* +results for the recovery invariants (rungs R2–R10) landed in verisimdb, +echo-types and tropical-types and are ledgered with receipts in +link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. The route to a working recovery, +the decisions still open, and what remains to 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. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 7f86888..eafd080 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 == TEST-NEEDS: squeakwell -=== Current State (2026-11-04) +=== Current State (2026-11-04; FFI row updated 2026-11-09) [width="100%",cols="40%,16%,44%",options="header",] |=== @@ -12,7 +12,7 @@ |*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 +|*Idris2 / Zig tests* |0 |No `.idr` files exist; the Zig FFI template was deleted on 2026-11-05 (`src/interface/ffi/README.adoc`) |=== All 23 tests pass (`cargo test`), but every one exercises a stub: the diff --git a/container/.gatekeeper.yaml b/container/.gatekeeper.yaml index 4aac671..430dfe1 100644 --- a/container/.gatekeeper.yaml +++ b/container/.gatekeeper.yaml @@ -1,6 +1,6 @@ # SPDX-License-Identifier: MPL-2.0 # -# Svalinn gatekeeper policy for {{PROJECT_NAME}} +# Svalinn gatekeeper policy for squeakwell # # Controls which operations are permitted through the edge gateway. # This template provides moderate security defaults — not wide-open test @@ -65,9 +65,9 @@ rate_limits: trust: # Only accept .ctp bundles signed by these keys. trusted_signers: - - key_id: "{{SERVICE_NAME}}-release" + - key_id: "squeakwell-release" algorithm: "Ed25519" - public_key_file: "/etc/svalinn/keys/{{SERVICE_NAME}}-release.pub" + public_key_file: "/etc/svalinn/keys/squeakwell-release.pub" # Require these attestations on all .ctp bundles. required_attestations: diff --git a/container/0.1-AI-MANIFEST.a2ml b/container/0.1-AI-MANIFEST.a2ml index ccb5bc5..7260e26 100644 --- a/container/0.1-AI-MANIFEST.a2ml +++ b/container/0.1-AI-MANIFEST.a2ml @@ -14,8 +14,8 @@ description: | provides Podman-Chainguard-stapeln templates that are customised via `just container-init` or `just init` during project bootstrap. - All files use {{PLACEHOLDER}} tokens that are substituted with project- - specific values during initialisation. + All files were rendered for squeakwell on 2026-11-09 (tokens substituted with project-specific values; + no tokens remain). purpose: | Provide a complete, security-first container deployment story for any @@ -128,7 +128,7 @@ invariants: --- ### [USAGE] initialisation: | - Run `just container-init` to substitute all {{PLACEHOLDER}} tokens with + Rendered 2026-11-09; `just container-init` would re-substitute tokens with project-specific values. This is also run as part of `just init`. development: | diff --git a/container/Containerfile b/container/Containerfile index ba85260..19b5783 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -1,136 +1,73 @@ # SPDX-License-Identifier: MPL-2.0 -# {{PROJECT_NAME}} Container Image +# squeakwell Container Image # -# Multi-stage build template for Chainguard Wolfi base images. -# Customise the builder stage for your language and copy the -# resulting binary/release into the minimal runtime stage. +# Multi-stage build on Chainguard Wolfi base images. Stage 1 compiles the +# squeakwell Rust CLI; stage 2 is a minimal runtime image that carries only +# the binary. squeakwell is a batch recovery tool, not a service: it opens +# no listening port, so there is no EXPOSE and no HTTP health check. The +# VeriSimDB instance it writes to is named at run time by VERISIMDB_URL. # # Build with Podman: -# podman build -t {{SERVICE_NAME}}:latest -f container/Containerfile . +# podman build -t squeakwell:latest -f container/Containerfile . # -# Run: -# podman run -p {{PORT}}:{{PORT}} {{SERVICE_NAME}}:latest -# -# Run with persistent volume: -# podman run -p {{PORT}}:{{PORT}} -v {{SERVICE_NAME}}-data:/data {{SERVICE_NAME}}:latest +# Run one recovery batch (working directory on a named volume): +# podman run --rm -v squeakwell-data-:/data -e VERISIMDB_URL \ +# -e SQUEAKWELL_BATCH_ID= squeakwell:latest recover --workdir /data # ============================================================================ # Stage 1: Builder # ============================================================================ -# -# Install build tools and compile the application. -# This stage is discarded after the build — only the compiled output -# is copied into the runtime stage. -# -# Language-specific examples (uncomment the one you need): -# -# --- Rust --- -# RUN apk add --no-cache rust pkgconf build-base -# COPY Cargo.toml Cargo.lock ./ -# COPY src/ ./src/ -# RUN cargo build --release -# # Output: /build/target/release/{{SERVICE_NAME}} -# -# --- Elixir --- -# RUN apk add --no-cache erl27-elixir-1.18 erlang-27 erlang-27-dev git build-base -# COPY mix.exs mix.lock ./ -# COPY lib/ ./lib/ -# COPY config/ ./config/ -# ENV MIX_ENV=prod -# RUN mix local.hex --force && mix local.rebar --force && \ -# mix deps.get --only prod && mix compile && mix release -# # Output: /build/_build/prod/rel/{{SERVICE_NAME}}/ -# -# --- Zig --- -# RUN apk add --no-cache zig build-base -# COPY build.zig build.zig.zon ./ -# COPY src/ ./src/ -# RUN zig build -Doptimize=ReleaseFast -# # Output: /build/zig-out/bin/{{SERVICE_NAME}} -# FROM cgr.dev/chainguard/wolfi-base:latest AS builder -# TODO: Install your language toolchain -RUN apk add --no-cache build-base +RUN apk add --no-cache build-base pkgconf rust WORKDIR /build -# TODO: Copy source files and build -COPY . . -# RUN +COPY Cargo.toml Cargo.lock ./ +COPY src/ ./src/ +COPY benches/ ./benches/ +RUN cargo build --release --locked --bin squeakwell +# Output: /build/target/release/squeakwell # ============================================================================ # Stage 2: Runtime # ============================================================================ -# -# Minimal production image. Only the compiled binary/release and runtime -# dependencies are included. No compilers, no source code, no build tools. -# FROM cgr.dev/chainguard/wolfi-base:latest # OCI image labels (compatible with cerro-torre .ctp bundle metadata) -LABEL org.opencontainers.image.title="{{PROJECT_NAME}}" \ - org.opencontainers.image.description="{{PROJECT_DESCRIPTION}}" \ - org.opencontainers.image.url="https://{{FORGE}}/{{OWNER}}/{{REPO}}" \ - org.opencontainers.image.source="https://{{FORGE}}/{{OWNER}}/{{REPO}}" \ - org.opencontainers.image.vendor="{{OWNER}}" \ - org.opencontainers.image.licenses="{{LICENSE}}" \ - org.opencontainers.image.authors="{{AUTHOR}} <{{AUTHOR_EMAIL}}>" \ - dev.cerrotorre.manifest="container/manifest.toml" \ - dev.cerrotorre.gatekeeper="container/.gatekeeper.yaml" \ - dev.stapeln.compose="container/compose.toml" - -# Install minimal runtime dependencies. -# Adjust this list for your application: -# - ca-certificates: TLS root certificates -# - curl: health check probe -# - libstdc++: C++ standard library (if needed by native deps) -# - ncurses: terminal UI (if needed, e.g. Elixir IEx) -RUN apk add --no-cache ca-certificates curl - -# Create non-root user for the application. -# Running as root inside containers is a security anti-pattern. -RUN addgroup -S appuser && adduser -S appuser -G appuser +LABEL org.opencontainers.image.title="squeakwell" \ + org.opencontainers.image.description="Database recovery through cross-modal constraint propagation on VeriSimDB" \ + org.opencontainers.image.url="https://github.com/hyperpolymath/squeakwell" \ + org.opencontainers.image.source="https://github.com/hyperpolymath/squeakwell" \ + org.opencontainers.image.vendor="hyperpolymath" \ + org.opencontainers.image.licenses="MPL-2.0" \ + org.opencontainers.image.authors="Jonathan D.A. Jewell " \ + dev.cerrotorre.manifest="container/manifest.toml" + +# ca-certificates: TLS roots for the https:// VERISIMDB_URL in production. +# Create the non-root user in the same layer. +RUN apk add --no-cache ca-certificates \ + && addgroup -S appuser && adduser -S appuser -G appuser WORKDIR /app -# TODO: Copy compiled binary/release from builder stage. -# Examples: -# COPY --from=builder /build/target/release/{{SERVICE_NAME}} /app/{{SERVICE_NAME}} -# COPY --from=builder /build/_build/prod/rel/{{SERVICE_NAME}} /app/release/ -# COPY --from=builder /build/zig-out/bin/{{SERVICE_NAME}} /app/{{SERVICE_NAME}} +COPY --from=builder /build/target/release/squeakwell /app/squeakwell -# Copy entrypoint script COPY container/entrypoint.sh /app/entrypoint.sh -RUN chmod +x /app/entrypoint.sh - -# Copy stapeln integration files (svalinn gatekeeper policy, cerro-torre manifest) -COPY container/.gatekeeper.yaml /etc/svalinn/gatekeeper.yaml COPY container/manifest.toml /app/manifest.toml -# Create data directory for persistent storage (mountable volume) -RUN mkdir -p /data && chown appuser:appuser /data +# Recovery working directories live under /data (mountable volume). +RUN chmod +x /app/entrypoint.sh \ + && mkdir -p /data && chown appuser:appuser /data \ + && chown -R appuser:appuser /app -# Set ownership of the application directory -RUN chown -R appuser:appuser /app - -# Environment variables — customise for your application -ENV APP_HOST=[::] -ENV APP_PORT={{PORT}} ENV APP_LOG_FORMAT=json ENV APP_DATA_DIR=/data -# Declare /data as a volume for persistent storage VOLUME ["/data"] -# Run as non-root USER appuser -# Expose the application port -EXPOSE {{PORT}} - -# Health check — the application must respond 2xx at /health -HEALTHCHECK --interval=30s --timeout=5s --start-period=10s --retries=3 \ - CMD curl -sf http://localhost:${APP_PORT}/health || exit 1 - +# Batch job: no EXPOSE, no HEALTHCHECK. Success is the exit code of one run. ENTRYPOINT ["/app/entrypoint.sh"] +CMD ["--help"] diff --git a/container/README.adoc b/container/README.adoc index 7a2ef6c..c1d1442 100644 --- a/container/README.adoc +++ b/container/README.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= {{PROJECT_NAME}} Container Templates += squeakwell Container Templates :toc: left :toclevels: 3 :sectnums: @@ -13,8 +13,9 @@ The stapeln stack provides verified container packaging, edge gateway policies, runtime monitoring, and supply-chain signing for Podman-based deployments using https://www.chainguard.dev/[Chainguard] Wolfi base images. -All files use `{{PLACEHOLDER}}` tokens that are replaced by `just container-init` -(or by the top-level `just init` during project bootstrap). +All files were rendered for squeakwell on 2026-11-09; no `{{PLACEHOLDER}}` +tokens remain. The `just container-init` recipe described below is how the +estate template is rendered when the files are re-pulled from the template. == File Reference diff --git a/container/compose.toml b/container/compose.toml index a14f8a0..1d43f8e 100644 --- a/container/compose.toml +++ b/container/compose.toml @@ -1,20 +1,24 @@ # SPDX-License-Identifier: MPL-2.0 # -# {{PROJECT_NAME}} selur-compose configuration +# squeakwell selur-compose configuration # -# Orchestrates the container stack as verified container bundles (.ctp). -# Uses selur zero-copy IPC between services on the same host. +# squeakwell is a batch recovery CLI, not a long-running service: it opens +# no port and needs no edge gateway. This stack runs ONE recovery batch as a +# verified .ctp container against the VeriSimDB named by VERISIMDB_URL, with +# the batch working directory on its own named volume. The k9 component in +# deploy.k9.ncl is the primary way to run batches; this file is the +# selur-compose equivalent for operators who already run a selur stack. # -# Usage: -# selur-compose up # Start all services -# selur-compose up --detach # Start in background -# selur-compose verify # Verify all .ctp signatures -# selur-compose ps # Check status -# selur-compose logs -f {{SERVICE_NAME}} # Stream logs -# selur-compose down # Stop all services +# Usage (both variables are required: compose substitutes an unset variable +# with the empty string, which would give an empty VERISIMDB_URL and a volume +# named "squeakwell-data-"; the entrypoint warns loudly in both cases): +# BATCH_ID=20261109T120000Z VERISIMDB_URL=https://verisim.example selur-compose up +# selur-compose verify # Verify the .ctp signature +# selur-compose logs squeakwell # Read the batch log +# selur-compose down # Remove the stopped batch container # # Fallback (when selur is not installed): -# podman compose --file compose.toml up --detach +# podman compose --file compose.toml up version = "1.0" @@ -22,49 +26,29 @@ version = "1.0" # Services # ============================================================================ -# Primary application service -[services.{{SERVICE_NAME}}] -image = "{{REGISTRY}}/{{SERVICE_NAME}}:latest.ctp" -ports = ["{{PORT}}:{{PORT}}"] -environment = { - APP_HOST = "[::]", - APP_PORT = "{{PORT}}", - APP_LOG_FORMAT = "json", - APP_DATA_DIR = "/data", -} -volumes = ["{{SERVICE_NAME}}-data:/data"] -restart = "always" -healthcheck = { test = "curl -sf http://localhost:{{PORT}}/health", interval = "30s", timeout = "5s", retries = 3 } - -# Svalinn edge gateway: validates requests, enforces policies, TLS termination -[services.svalinn] -image = "ghcr.io/hyperpolymath/svalinn:latest.ctp" -ports = ["443:443", "80:80"] -environment = { - SVALINN_BACKEND = "http://{{SERVICE_NAME}}:{{PORT}}", - SVALINN_POLICY_FILE = "/etc/svalinn/gatekeeper.yaml", - SVALINN_TLS_AUTO = "true", -} -volumes = ["svalinn-config:/etc/svalinn:ro"] -depends_on = ["{{SERVICE_NAME}}"] -restart = "always" -healthcheck = { test = "curl -sf http://localhost:80/health", interval = "30s", timeout = "5s", retries = 3 } +[services.squeakwell] +image = "ghcr.io/hyperpolymath/squeakwell:latest.ctp" +command = ["recover", "--workdir", "/data"] +# TOML 1.0: an inline table stays on one line with no trailing comma. +# SQUEAKWELL_BATCH_ID makes the VeriSimDB session id per batch; without it every +# batch would derive the same id from the shared mount path /data. +environment = { APP_LOG_FORMAT = "json", APP_DATA_DIR = "/data", VERISIMDB_URL = "${VERISIMDB_URL}", SQUEAKWELL_BATCH_ID = "${BATCH_ID}" } +# One volume per batch; see deploy.k9.ncl for the matching rollback rule. +volumes = ["squeakwell-data-${BATCH_ID}:/data"] +# A batch runs once; do not restart it. +restart = "no" # ============================================================================ # Volumes # ============================================================================ -[volumes.{{SERVICE_NAME}}-data] -driver = "local" - -[volumes.svalinn-config] +[volumes."squeakwell-data-${BATCH_ID}"] driver = "local" # ============================================================================ # Networks # ============================================================================ -# Use selur zero-copy IPC for inter-service communication on the same host. -# Falls back to standard bridge networking when selur driver is unavailable. +# Outbound only (to VERISIMDB_URL). No inter-service IPC is needed. [networks.default] -driver = "selur" +driver = "bridge" diff --git a/container/ct-build.sh b/container/ct-build.sh index a54a541..52ed8da 100755 --- a/container/ct-build.sh +++ b/container/ct-build.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 # -# {{PROJECT_NAME}} — Cerro Torre build, sign, and verify pipeline +# squeakwell — Cerro Torre build, sign, and verify pipeline # # Builds the container image, packages it as a verified .ctp bundle, # signs it with Ed25519, and verifies the result. Gracefully degrades @@ -18,8 +18,8 @@ # CT_KEY_ID=my-key ./ct-build.sh # Use specific signing key # # Environment variables: -# CT_KEY_ID — Signing key identifier (default: {{SERVICE_NAME}}-release) -# CT_REGISTRY — OCI registry to push to (default: {{REGISTRY}}) +# CT_KEY_ID — Signing key identifier (default: squeakwell-release) +# CT_REGISTRY — OCI registry to push to (default: ghcr.io/hyperpolymath) # CT_TAG — Image tag (default: latest) set -euo pipefail @@ -38,15 +38,15 @@ for arg in "$@"; do fi done -CT_KEY_ID="${CT_KEY_ID:-{{SERVICE_NAME}}-release}" -CT_REGISTRY="${CT_REGISTRY:-{{REGISTRY}}}" +CT_KEY_ID="${CT_KEY_ID:-squeakwell-release}" +CT_REGISTRY="${CT_REGISTRY:-ghcr.io/hyperpolymath}" CT_TAG="${CT_TAG:-latest}" -IMAGE_NAME="{{SERVICE_NAME}}" +IMAGE_NAME="squeakwell" FULL_IMAGE="${CT_REGISTRY}/${IMAGE_NAME}:${CT_TAG}" CTP_FILE="${SCRIPT_DIR}/${IMAGE_NAME}-${CT_TAG}.ctp" -echo "=== {{PROJECT_NAME}} Cerro Torre Build Pipeline ===" +echo "=== squeakwell Cerro Torre Build Pipeline ===" echo " Image: ${FULL_IMAGE}" echo " Key: ${CT_KEY_ID}" echo " Bundle: ${CTP_FILE}" @@ -152,8 +152,8 @@ echo "=== Build pipeline complete ===" echo " Image: ${FULL_IMAGE}" echo " Bundle: ${CTP_FILE}" echo "" -echo " To deploy with selur-compose:" -echo " cd container && selur-compose up" +echo " To run one recovery batch (per-batch volume, VERISIMDB_URL required):" +echo " podman run --rm -v squeakwell-data-:/data -e VERISIMDB_URL ${FULL_IMAGE} recover --workdir /data" echo "" echo " To verify at any time:" echo " ct verify ${CTP_FILE}" diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index 14a614a..8016bcb 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -73,7 +73,7 @@ K9! 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", + "Removes ONLY the named batch volume squeakwell-data- on rollback (never other batches)", "Writes recovery working directories under the mounted /data volume", ], @@ -81,8 +81,11 @@ K9! 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", + # The one-line recipes do not generate a default BATCH_ID (only + # scripts.deploy below does); they fail fast instead of running on an + # empty id, and they pass the id into the container as the session key. + deploy = "podman run --rm -v \"squeakwell-data-${BATCH_ID:?BATCH_ID must be set}:/data\" -e \"VERISIMDB_URL=${VERISIMDB_URL:?VERISIMDB_URL must be set}\" -e \"SQUEAKWELL_BATCH_ID=$BATCH_ID\" ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", + migrate = "container/ct-build.sh && podman run --rm -v \"squeakwell-data-${BATCH_ID:?BATCH_ID must be set}:/data\" -e \"VERISIMDB_URL=${VERISIMDB_URL:?VERISIMDB_URL must be set}\" -e \"SQUEAKWELL_BATCH_ID=$BATCH_ID\" ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", }, }, @@ -102,9 +105,12 @@ K9! image = "ghcr.io/hyperpolymath/squeakwell", entrypoint = "squeakwell", data_volume = "/data", + # One named volume per batch: squeakwell-data-. Rollback + # removes only that volume, so earlier batches are never destroyed. + batch_volume_prefix = "squeakwell-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). + # through this environment variable (an https:// URL in production; TLS + # is terminated by the VeriSimDB deployment, not by squeakwell). verisimdb_url_env = "VERISIMDB_URL", }, @@ -117,8 +123,8 @@ K9! # ───────────────────────────────────────────────────────────── 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. + # container/compose.toml is the selur-compose equivalent of this component + # (one batch, one volume); it is NOT invoked here. pre_deploy = m%" #!/bin/sh set -eu @@ -131,29 +137,40 @@ echo "K9: Validation passed." # 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. + # production). Each batch gets its own named volume + # squeakwell-data- (BATCH_ID defaults to a UTC timestamp) so a + # rollback can discard exactly one batch. deploy = m%" #!/bin/sh set -eu ENV="${1:-dev}" TAG="${IMAGE_TAG:-latest}" +# Default id: UTC second plus this shell's PID, so two batches started in the +# same second on one host still get distinct volumes. +BATCH_ID="${BATCH_ID:-$(date -u +%Y%m%dT%H%M%SZ)-$$}" +VOLUME="squeakwell-data-$BATCH_ID" : "${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 \ +# VERISIMDB_URL is not echoed: it may carry credentials or a token. +echo "K9: Running recovery batch $BATCH_ID against VERISIMDB_URL (volume $VOLUME)..." +podman run --rm -v "$VOLUME:/data" -e VERISIMDB_URL -e "SQUEAKWELL_BATCH_ID=$BATCH_ID" \ "ghcr.io/hyperpolymath/squeakwell:$TAG" recover --workdir /data -echo "K9: Batch for $ENV complete." +echo "K9: Batch $BATCH_ID for $ENV complete. To discard it, run this component's rollback script with BATCH_ID=$BATCH_ID (the container ran with --rm, so no stopped container holds the volume)." "%, # Rollback: a batch job leaves no running service; rolling back means - # discarding the data volume written by the last batch. + # discarding the working volume of ONE named batch. BATCH_ID is required + # so that no other batch can be removed by accident. rollback = m%" #!/bin/sh set -eu -echo "K9: Rolling back the last squeakwell batch (removing squeakwell-data volume)..." -podman volume rm squeakwell-data -echo "K9: Rollback complete." +: "${BATCH_ID:?BATCH_ID must name the batch to roll back (see the deploy output)}" +VOLUME="squeakwell-data-$BATCH_ID" +podman volume inspect "$VOLUME" >/dev/null +echo "K9: Rolling back squeakwell batch $BATCH_ID (removing volume $VOLUME only)..." +podman volume rm "$VOLUME" +echo "K9: Rollback of $BATCH_ID complete. Other batch volumes are untouched." "%, }, diff --git a/container/entrypoint.sh b/container/entrypoint.sh index a7a0369..daf8cba 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -1,63 +1,63 @@ #!/bin/sh # SPDX-License-Identifier: MPL-2.0 -# {{PROJECT_NAME}} container entrypoint +# squeakwell container entrypoint # -# Handles signal propagation, startup logging, and health check -# preparation before exec-ing into the main application process. +# squeakwell is a batch recovery CLI, not a long-running service. The +# entrypoint checks the working volume, logs the run parameters, and execs +# the binary with the caller's arguments so that PID 1 is squeakwell and +# signals from `podman stop` reach it directly. set -e -# --------------------------------------------------------------------------- -# Signal handling -# --------------------------------------------------------------------------- -# -# Trap SIGTERM and SIGINT so that the application can shut down gracefully -# when Podman sends stop signals (e.g. `podman stop`, `selur-compose down`). - -cleanup() { - echo "Received shutdown signal — stopping {{SERVICE_NAME}}..." - # If the main process is backgrounded, kill it here: - # kill "$MAIN_PID" 2>/dev/null || true - # wait "$MAIN_PID" 2>/dev/null || true - exit 0 +DATA_DIR="${APP_DATA_DIR:-/data}" + +echo "Starting squeakwell..." +echo " Data: ${DATA_DIR}" +echo " Log: ${APP_LOG_FORMAT:-json}" +# Never echo VERISIMDB_URL itself: a URL may carry userinfo credentials or a +# token in its query string, and container logs are widely readable. Log the +# scheme and host only (userinfo, path and query stripped). +redact_url() { + _url="$1" + case "$_url" in + *://*) _scheme="${_url%%://*}://"; _rest="${_url#*://}" ;; + *) _scheme=""; _rest="$_url" ;; + esac + # Cut path, query and fragment first: an '@' inside them (e.g. + # ?token=a@secret) must not be mistaken for the userinfo separator. + _rest="${_rest%%/*}" + _rest="${_rest%%\?*}" + _rest="${_rest%%#*}" + case "$_rest" in + *@*) _rest="${_rest##*@}" ;; + *) ;; + esac + printf '%s%s\n' "$_scheme" "$_rest" } -trap cleanup TERM INT - -# --------------------------------------------------------------------------- -# Startup logging -# --------------------------------------------------------------------------- -echo "Starting {{SERVICE_NAME}}..." -echo " Host: ${APP_HOST:-[::]}" -echo " Port: ${APP_PORT:-{{PORT}}}" -echo " Data: ${APP_DATA_DIR:-/data}" -echo " Log: ${APP_LOG_FORMAT:-json}" +if [ -z "${VERISIMDB_URL+set}" ]; then + echo " VeriSimDB: WARNING: the client falls back to http://localhost:8080 and" + echo " persistence errors are not fatal, so session and phase events" + echo " may not be recorded anywhere. Set VERISIMDB_URL for a real batch." +elif [ -z "${VERISIMDB_URL}" ]; then + echo " VeriSimDB: WARNING: VERISIMDB_URL is set to the empty string" + echo " (usually a compose file passing through an unset variable)." + echo " The client treats it as unset and falls back to http://localhost:8080;" + echo " session and phase events may not be recorded anywhere." +else + echo " VeriSimDB: $(redact_url "${VERISIMDB_URL}") (host only; userinfo, path and query not logged)" +fi +if [ -n "${SQUEAKWELL_BATCH_ID:-}" ]; then + echo " Batch: ${SQUEAKWELL_BATCH_ID}" +else + echo " Batch: (session id derived from the workdir path; set SQUEAKWELL_BATCH_ID" + echo " so concurrent batches do not share one VeriSimDB session)" +fi -# --------------------------------------------------------------------------- -# Health check preparation -# --------------------------------------------------------------------------- -# -# Ensure the data directory exists and is writable. # The VOLUME directive in the Containerfile creates /data, but a bind-mount # might replace it with an empty directory owned by root. - -if [ -d "${APP_DATA_DIR:-/data}" ]; then - if [ ! -w "${APP_DATA_DIR:-/data}" ]; then - echo "WARNING: ${APP_DATA_DIR:-/data} is not writable by $(whoami)" - fi +if [ -d "${DATA_DIR}" ] && [ ! -w "${DATA_DIR}" ]; then + echo "WARNING: ${DATA_DIR} is not writable by $(whoami)" fi -# --------------------------------------------------------------------------- -# Exec into main process -# --------------------------------------------------------------------------- -# -# Replace the entrypoint shell with the application process so that -# signals are delivered directly and PID 1 is the application. -# -# TODO: Replace the command below with your application binary. -# Examples: -# exec /app/{{SERVICE_NAME}} -# exec /app/release/bin/{{SERVICE_NAME}} start -# exec /app/{{SERVICE_NAME}} serve --host "${APP_HOST}" --port "${APP_PORT}" - -exec "$@" +exec /app/squeakwell "$@" diff --git a/container/manifest.toml b/container/manifest.toml index 2a4ec16..f7ec0ce 100644 --- a/container/manifest.toml +++ b/container/manifest.toml @@ -1,41 +1,45 @@ # SPDX-License-Identifier: MPL-2.0 # -# Cerro Torre manifest for {{PROJECT_NAME}} .ctp bundle +# Cerro Torre manifest for the squeakwell .ctp bundle # -# This manifest describes the container image for verified -# container packaging. Used by `ct pack` to create .ctp bundles. +# Describes the squeakwell container image for verified container +# packaging. Used by `ct pack` to create .ctp bundles. squeakwell is a +# batch recovery CLI: it listens on no port and exposes no HTTP endpoint. [metadata] -name = "{{SERVICE_NAME}}" -version = "{{VERSION}}" +name = "squeakwell" +version = "0.1.0" revision = 1 -summary = "{{PROJECT_DESCRIPTION}}" +summary = "Database recovery through cross-modal constraint propagation on VeriSimDB" description = """ -{{PROJECT_NAME}} — containerised service packaged as a verified -cerro-torre .ctp bundle with Ed25519 signing and full provenance -tracking. +squeakwell recovers a damaged database by treating VeriSimDB's eight +modalities as witnesses of one identity and propagating constraints between +them until the remaining drift is zero or the entity is queued for human +review. Packaged as a verified cerro-torre .ctp bundle with Ed25519 signing +and provenance tracking. Runs as a batch job against the VeriSimDB named by +VERISIMDB_URL. """ -license = "{{LICENSE}}" +license = "MPL-2.0" homepage = "https://github.com/hyperpolymath/squeakwell" -maintainer = "Jonathan D.A. Jewell <{{EMAIL}}>" +maintainer = "Jonathan D.A. Jewell " [provenance] upstream = "https://github.com/hyperpolymath/squeakwell" -import_date = {{CURRENT_DATE}}T00:00:00Z +import_date = 2026-11-09T00:00:00Z [dependencies] -runtime = ["ca-certificates", "curl"] -build = [] +runtime = ["ca-certificates"] +build = ["rust", "build-base", "pkgconf"] [build] -system = "podman" +system = "cargo" [build.environment] -APP_HOST = "[::]" -APP_PORT = "{{PORT}}" +APP_LOG_FORMAT = "json" +APP_DATA_DIR = "/data" [outputs] -primary = "{{SERVICE_NAME}}" +primary = "squeakwell" split = [] [attestations] @@ -51,12 +55,13 @@ no_new_privileges = true [security.capabilities] drop = ["ALL"] -add = ["NET_BIND_SERVICE"] +add = [] [security.network] -listen_tcp = [{{PORT}}] +# Batch client only: outbound HTTPS to VERISIMDB_URL, no listening sockets. +listen_tcp = [] [security.filesystem] read = ["/app/", "/data/"] write = ["/data/", "/tmp/"] -execute = ["/app/entrypoint.sh"] +execute = ["/app/entrypoint.sh", "/app/squeakwell"] diff --git a/container/vordr.toml b/container/vordr.toml index af38fc5..6ca7d23 100644 --- a/container/vordr.toml +++ b/container/vordr.toml @@ -1,10 +1,12 @@ # SPDX-License-Identifier: MPL-2.0 # -# Vordr runtime monitoring configuration for {{PROJECT_NAME}} +# Vordr runtime monitoring configuration for squeakwell # # Vordr watches container health, detects crashes, tracks resource usage, -# and emits structured logs. It runs alongside the application stack and -# provides runtime observability without requiring in-process agents. +# and emits structured logs. squeakwell is a batch recovery CLI with no HTTP +# endpoint, so there is no health probe here: vordr's value for squeakwell +# is crash detection (a non-zero exit of a recovery batch) and resource +# tracking while a batch runs. # # Usage: # vordr watch --config container/vordr.toml @@ -12,42 +14,31 @@ # vordr report [metadata] -name = "{{SERVICE_NAME}}" -version = "{{VERSION}}" +name = "squeakwell" +version = "0.1.0" # ============================================================================ # Health Monitoring # ============================================================================ # -# Vordr periodically probes these endpoints. If a probe fails beyond the -# failure_threshold, vordr emits an alert and (optionally) restarts the -# container via Podman. +# Disabled: a batch job has no /health or /ready endpoint. A batch that is +# still running is healthy; one that exited non-zero is a crash (below). [health] -# Primary health endpoint — must return 2xx. -endpoint = "http://localhost:{{PORT}}/health" -interval = "30s" -timeout = "5s" -failure_threshold = 3 - -# Readiness endpoint — checked during startup and after restarts. -readiness_endpoint = "http://localhost:{{PORT}}/ready" -readiness_timeout = "10s" - -# Action on failure: "alert" (log + notify) or "restart" (alert + podman restart). +enabled = false on_failure = "alert" # ============================================================================ # Crash Detection # ============================================================================ # -# Monitors container state via Podman. Detects OOM kills, segfaults, -# and unexpected exits. +# Monitors container state via Podman. A recovery batch exiting non-zero is +# the crash signal. Batches are not restarted automatically: a failed batch +# leaves its working directory on its own volume for inspection. [crash_detection] enabled = true -# Maximum restarts within the window before vordr stops restarting. -max_restarts = 5 +max_restarts = 0 restart_window = "10m" # ============================================================================ @@ -62,7 +53,7 @@ cpu_warn = 80 # Percentage — warn at 80% sustained CPU. cpu_critical = 95 # Percentage — critical alert at 95%. memory_warn = 75 # Percentage of memory limit. memory_critical = 90 -disk_warn = 80 # Percentage of volume usage. +disk_warn = 80 # Percentage of the batch volume's usage. disk_critical = 95 # Sample interval for resource metrics. @@ -71,30 +62,19 @@ sample_interval = "15s" # ============================================================================ # Log Output # ============================================================================ -# -# Vordr emits its own logs (not the application's) in structured format. [logging] format = "json" level = "info" -# Write vordr logs to stdout (captured by Podman) and optionally to file. output = "stdout" -# file = "/var/log/vordr/{{SERVICE_NAME}}.log" +# file = "/var/log/vordr/squeakwell.log" # ============================================================================ # Notifications (optional) # ============================================================================ -# -# Uncomment and configure to receive alerts via webhook or email. # [notifications.webhook] # url = "https://example.com/hooks/vordr" # method = "POST" # headers = { "Content-Type" = "application/json" } -# on = ["failure", "recovery", "resource_critical"] - -# [notifications.email] -# to = "{{EMAIL}}" -# from = "vordr@{{SERVICE_NAME}}.local" -# smtp = "smtp://localhost:25" # on = ["failure", "resource_critical"] diff --git a/docs/ROUTE-PLAN.adoc b/docs/ROUTE-PLAN.adoc index 39c3f31..e28b743 100644 --- a/docs/ROUTE-PLAN.adoc +++ b/docs/ROUTE-PLAN.adoc @@ -193,9 +193,18 @@ in each. * 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, + postulates. At recon time (2026-11-05) there was no partial-section or + multi-witness layer and `EchoTruncation.agda` was unwired from `All.agda` + (dead code under the repo's own discipline). *Update 2026-11-09:* all three + gaps are closed in echo-types PR #370 (open, not yet on `main`): + `EchoPartialSection.agda` (R3/R9 theory), `EchoFibreIntersection.agda` (R8) + and `EchoTruncation` wired into `All.agda`/`Smoke.agda`; see + `PROOF-STATUS.adoc`. Still missing there: the drift bridge R17. Not + echo-types work: R11 is a Creusot proof of the Rust resolve kernel that + lives in squeakwell, and the f64 confidence statement needs the + quantisation layer noted under R6/R7 (R18 is the separate Kripke-world + conjecture, gated on vcl-ut `Epistemic.idr`). + 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 diff --git a/src/engine/mod.rs b/src/engine/mod.rs index a975db0..73c1bca 100644 --- a/src/engine/mod.rs +++ b/src/engine/mod.rs @@ -42,20 +42,26 @@ pub struct EntityConfidence { pub review_reason: Option, } -/// Run the recovery process. +/// Run the five-phase recovery stub. +/// +/// No workdir data is read or repaired yet. `target_level` limits the level +/// messages within each phase; all five phases still run. `drift_threshold` +/// and `max_iterations` are recorded but do not yet control convergence. +/// The session ID uses a non-blank `SQUEAKWELL_BATCH_ID`, or otherwise the +/// workdir path, as described by [`session_id_for`]. /// /// Persists session snapshots and phase-transition events to VeriSimDB /// (collections: squeakwell:sessions, squeakwell:phase-events). All /// VeriSimDB calls are fail-open — the recovery completes even if -/// VeriSimDB is unreachable. +/// VeriSimDB is unreachable. Returns `Ok(())` after the phase loop. pub fn recover(workdir: &str, target_level: u8, drift_threshold: f64, max_iterations: u32) -> Result<()> { println!("SqueakWell: beginning recovery in {}", workdir); - // Use a stable session ID derived from the workdir path - let session_id = format!( - "sq:{}", - sha2_short(workdir) - ); + // Stable session ID: the batch id when the runner supplies one (every + // container batch mounts its volume at the same path, so the path alone + // would make distinct batches share one VeriSimDB session), else the + // workdir path. + let session_id = session_id_for(workdir, std::env::var("SQUEAKWELL_BATCH_ID").ok().as_deref()); let vdb = VeriSimDbClient::new(); @@ -127,6 +133,22 @@ pub fn recover(workdir: &str, target_level: u8, drift_threshold: f64, max_iterat Ok(()) } +/// Derive the VeriSimDB session ID for a recovery run. +/// +/// With a non-blank `batch_id` (the `SQUEAKWELL_BATCH_ID` environment +/// variable, set by `container/compose.toml` and `container/deploy.k9.ncl` +/// from `BATCH_ID`), returns `sq:b:` using the trimmed batch ID. +/// Otherwise returns `sq:` using the workdir path exactly as supplied, +/// so existing workdir sessions keep their IDs. Each hash is the first 12 +/// hexadecimal characters of SHA-256; distinct inputs can share a hash. +/// The prefixes keep batch and workdir session IDs separate. +pub fn session_id_for(workdir: &str, batch_id: Option<&str>) -> String { + match batch_id.map(str::trim).filter(|b| !b.is_empty()) { + Some(batch) => format!("sq:b:{}", sha2_short(batch)), + None => format!("sq:{}", sha2_short(workdir)), + } +} + /// Derive a short stable identifier from an arbitrary string. /// /// Returns the first 12 hex characters of SHA-256(input), giving 48 bits diff --git a/src/verisim.rs b/src/verisim.rs index abacb7e..80316b3 100644 --- a/src/verisim.rs +++ b/src/verisim.rs @@ -22,7 +22,10 @@ // // ## Environment variable // -// VERISIMDB_URL — override base URL (default: http://localhost:8080) +// VERISIMDB_URL — override base URL (default: http://localhost:8080). +// An empty value is treated as unset (compose files pass +// `${VERISIMDB_URL}` through verbatim, so "unset" arrives +// as ""). use anyhow::{Context, Result}; use serde_json::{json, Value}; @@ -43,14 +46,31 @@ pub struct VeriSimDbClient { impl VeriSimDbClient { /// Create a new client, reading `VERISIMDB_URL` from the environment. /// - /// Falls back to `http://localhost:8080` if the variable is unset. + /// Falls back to `http://localhost:8080` if the variable is unset, + /// non-Unicode or blank. Otherwise trims surrounding whitespace and + /// trailing slashes, as described by [`Self::from_env_value`]. pub fn new() -> Self { - let base_url = env::var("VERISIMDB_URL") - .unwrap_or_else(|_| "http://localhost:8080".to_owned()); + Self::from_env_value(env::var("VERISIMDB_URL").ok()) + } + + /// Build a client from the raw `VERISIMDB_URL` value (`None` = unset). + /// Trims surrounding whitespace, then uses `http://localhost:8080` for + /// absent or blank values. Removes trailing slashes from the resulting + /// base URL without validating it or making a network request. + pub fn from_env_value(value: Option) -> Self { + let base_url = value + .map(|s| s.trim().to_owned()) + .filter(|s| !s.is_empty()) + .unwrap_or_else(|| "http://localhost:8080".to_owned()); // Strip trailing slash for consistent URL construction Self { base_url: base_url.trim_end_matches('/').to_owned() } } + /// The base URL this client sends requests to (no trailing slash). + pub fn base_url(&self) -> &str { + &self.base_url + } + // ------------------------------------------------------------------------- // Public API // ------------------------------------------------------------------------- @@ -191,3 +211,25 @@ pub fn phase_event_doc(session_id: &str, phase: u8, iteration: u32, drift: f64) "timestamp": chrono::Utc::now().to_rfc3339(), }) } + +#[cfg(test)] +mod tests { + use super::VeriSimDbClient; + + #[test] + fn blank_url_falls_back_like_unset() { + let unset = VeriSimDbClient::from_env_value(None); + let empty = VeriSimDbClient::from_env_value(Some(String::new())); + let blank = VeriSimDbClient::from_env_value(Some(" ".to_owned())); + assert_eq!(unset.base_url(), "http://localhost:8080"); + assert_eq!(empty.base_url(), unset.base_url()); + assert_eq!(blank.base_url(), unset.base_url()); + } + + #[test] + fn set_url_is_kept_without_trailing_slash() { + let c = VeriSimDbClient::from_env_value(Some("https://verisim.example/".to_owned())); + assert_eq!(c.base_url(), "https://verisim.example"); + assert_eq!(c.doc_url("squeakwell:sessions", "sq:1"), "https://verisim.example/v1/squeakwell:sessions/sq%3A1"); + } +} diff --git a/tests/container_config_test.rs b/tests/container_config_test.rs new file mode 100644 index 0000000..b6c79a8 --- /dev/null +++ b/tests/container_config_test.rs @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: MPL-2.0 +//! The container stack definitions must be valid TOML 1.0. A multi-line +//! inline table with a trailing comma (the shape the estate template ships) +//! is rejected by TOML 1.0 parsers; this test pins the rendered files. + +use std::path::Path; + +fn parse(path: &str) -> toml::Value { + let full = Path::new(env!("CARGO_MANIFEST_DIR")).join(path); + let text = std::fs::read_to_string(&full).unwrap_or_else(|e| panic!("read {path}: {e}")); + toml::from_str(&text).unwrap_or_else(|e| panic!("{path} is not valid TOML: {e}")) +} + +#[test] +fn compose_toml_parses_and_names_the_batch_service() { + let v = parse("container/compose.toml"); + let svc = &v["services"]["squeakwell"]; + assert_eq!(svc["restart"].as_str(), Some("no")); + assert_eq!(svc["environment"]["APP_DATA_DIR"].as_str(), Some("/data")); + // The VeriSimDB target and the per-batch session key must both reach the + // container; without them the client falls back to localhost and every + // batch would share one session id. + assert_eq!(svc["environment"]["VERISIMDB_URL"].as_str(), Some("${VERISIMDB_URL}")); + assert_eq!(svc["environment"]["SQUEAKWELL_BATCH_ID"].as_str(), Some("${BATCH_ID}")); + assert!(svc.get("ports").is_none(), "a batch CLI exposes no ports"); + // One named volume per batch, mounted at the workdir, and declared. + let volumes: Vec<&str> = + svc["volumes"].as_array().expect("volumes array").iter().filter_map(|v| v.as_str()).collect(); + assert_eq!(volumes, vec!["squeakwell-data-${BATCH_ID}:/data"]); + assert!( + v["volumes"].get("squeakwell-data-${BATCH_ID}").is_some(), + "the per-batch volume must be declared under [volumes]" + ); +} + +#[test] +fn manifest_toml_parses_with_no_listening_sockets() { + let v = parse("container/manifest.toml"); + assert_eq!(v["metadata"]["name"].as_str(), Some("squeakwell")); + let listen = v["security"]["network"]["listen_tcp"].as_array().expect("listen_tcp array"); + assert!(listen.is_empty(), "squeakwell listens on no port"); +} + +#[test] +fn vordr_toml_parses_with_health_probe_disabled() { + let v = parse("container/vordr.toml"); + assert_eq!(v["health"]["enabled"].as_bool(), Some(false)); + assert_eq!(v["crash_detection"]["max_restarts"].as_integer(), Some(0)); +} + +#[test] +fn session_id_is_per_batch_when_a_batch_id_is_supplied() { + use squeakwell::engine::session_id_for; + // Two batches on the same mount path must not share a VeriSimDB session. + let a = session_id_for("/data", Some("20261109T120000Z-1")); + let b = session_id_for("/data", Some("20261109T120000Z-2")); + assert_ne!(a, b); + assert!(a.starts_with("sq:b:") && a.len() == 17); + // Batch and workdir IDs live in separate namespaces: matching inputs, + // including a workdir that spells out the old "batch:" prefix, never + // share a session. + assert_ne!(session_id_for("foo", None), session_id_for("/data", Some("foo"))); + assert_ne!(session_id_for("batch:foo", None), session_id_for("/data", Some("foo"))); + // Workdir IDs are unchanged in shape, so existing sessions stay reachable. + let w = session_id_for("/data", None); + assert!(w.starts_with("sq:") && !w.starts_with("sq:b:") && w.len() == 15); + // Without a batch id the id is a stable function of the workdir alone, + // and a blank batch id counts as absent. + assert_eq!(session_id_for("/data", None), session_id_for("/data", Some(" "))); + assert_ne!(session_id_for("/data", None), session_id_for("/other", None)); +}