From 0dc4b58996c82cb1dcbf1a1b1d5af6a5841f214e Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 9 Nov 2026 13:03:53 +0000 Subject: [PATCH 1/7] fix(container): build the real squeakwell binary, per-batch rollback, honest wording MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the Codex review findings left on PR #78 after merge. P1 — container/deploy.k9.ncl: rollback removed the single squeakwell-data volume, destroying every batch ever run. Each batch now gets its own named volume squeakwell-data- (default: UTC timestamp); rollback requires BATCH_ID, inspects that one volume, and removes only it. P1 — container/Containerfile: the template never built anything. It now compiles the Rust CLI in a wolfi builder stage and copies the binary into the runtime stage. squeakwell is a batch job, so EXPOSE, HEALTHCHECK and APP_PORT are gone. entrypoint.sh execs /app/squeakwell with the caller's arguments. P2 — rendered every {{PLACEHOLDER}} in container/: ct-build.sh (registry ghcr.io/hyperpolymath, image squeakwell), manifest.toml (no listening sockets, no NET_BIND_SERVICE), vordr.toml (no HTTP health probe; crash detection on batch exit), compose.toml (one batch service, no ports, no gateway), .gatekeeper.yaml, container/README.adoc and its manifest. P2 — wording: README Phase 5 heading and bullet, EXPLAINME phase sentence (gate ceiling is L6 today), STATE.a2ml (E1-E7; route-plan section 10), PROOF-NEEDS and TEST-NEEDS no longer describe a Zig FFI template that was deleted on 2026-11-05. Verified: cargo test (23 pass), cargo clippy --all-targets (clean), sh -n / bash -n on both shell scripts. The image build itself was not run here (no podman in this environment). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- .machine_readable/descriptiles/STATE.a2ml | 4 +- EXPLAINME.adoc | 2 +- PROOF-NEEDS.adoc | 2 +- README.adoc | 4 +- TEST-NEEDS.adoc | 2 +- container/.gatekeeper.yaml | 6 +- container/0.1-AI-MANIFEST.a2ml | 6 +- container/Containerfile | 123 ++++++---------------- container/README.adoc | 7 +- container/compose.toml | 63 ++++------- container/ct-build.sh | 18 ++-- container/deploy.k9.ncl | 41 +++++--- container/entrypoint.sh | 64 +++-------- container/manifest.toml | 47 +++++---- container/vordr.toml | 52 +++------ 15 files changed, 161 insertions(+), 280 deletions(-) diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index cc3d58f..3decd67 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -36,9 +36,9 @@ 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", + "File the cross-repo issues listed in docs/ROUTE-PLAN.adoc section 10", ] [maintenance-status] 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..3ca7250 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -3,7 +3,7 @@ === Current State * *LOC*: ~640 Rust (2026-11-05) -* *Languages*: Rust; an unbuilt Zig FFI template; no Idris2 source yet +* *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. 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. diff --git a/README.adoc b/README.adoc index 6af0625..a13e531 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). @@ -117,7 +117,7 @@ function: recovery is complete when cross-modal drift approaches zero. - 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) + - Phase 5: Convergence (gate ceiling L6 today; VCL-total levels 7-10 are future vcl-ut work) * **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: diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 7f86888..f30a599 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -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..dcc4968 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -1,136 +1,75 @@ # 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 \ +# 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 rust build-base pkgconf 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 +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. +RUN apk add --no-cache ca-certificates # 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 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) +# Recovery working directories live under /data (mountable volume). RUN mkdir -p /data && chown appuser:appuser /data - -# 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..28cf762 100644 --- a/container/compose.toml +++ b/container/compose.toml @@ -1,20 +1,22 @@ # 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 +# 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 +24,30 @@ version = "1.0" # Services # ============================================================================ -# Primary application service -[services.{{SERVICE_NAME}}] -image = "{{REGISTRY}}/{{SERVICE_NAME}}:latest.ctp" -ports = ["{{PORT}}:{{PORT}}"] +[services.squeakwell] +image = "ghcr.io/hyperpolymath/squeakwell:latest.ctp" +command = ["recover", "--workdir", "/data"] environment = { - APP_HOST = "[::]", - APP_PORT = "{{PORT}}", APP_LOG_FORMAT = "json", APP_DATA_DIR = "/data", + VERISIMDB_URL = "${VERISIMDB_URL}", } -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 } +# 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..cfcf79a 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,8 @@ 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", + deploy = "podman run --rm -v squeakwell-data-$BATCH_ID:/data -e VERISIMDB_URL ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", + migrate = "container/ct-build.sh && podman run --rm -v squeakwell-data-$BATCH_ID:/data -e VERISIMDB_URL ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", }, }, @@ -102,9 +102,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 +120,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 +134,37 @@ 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}" +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 \ +echo "K9: Running recovery batch $BATCH_ID against $VERISIMDB_URL (volume $VOLUME)..." +podman run --rm -v "$VOLUME:/data" -e VERISIMDB_URL \ "ghcr.io/hyperpolymath/squeakwell:$TAG" recover --workdir /data -echo "K9: Batch for $ENV complete." +echo "K9: Batch $BATCH_ID for $ENV complete. Roll back with: BATCH_ID=$BATCH_ID k9-svc rollback" "%, # 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..c5c497a 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -1,63 +1,25 @@ #!/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 -} -trap cleanup TERM INT +DATA_DIR="${APP_DATA_DIR:-/data}" -# --------------------------------------------------------------------------- -# Startup logging -# --------------------------------------------------------------------------- +echo "Starting squeakwell..." +echo " Data: ${DATA_DIR}" +echo " Log: ${APP_LOG_FORMAT:-json}" +echo " VeriSimDB: ${VERISIMDB_URL:-}" -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}" - -# --------------------------------------------------------------------------- -# 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"] From 393ba213a14016983df13bb2a80982a06ac8f4d2 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 9 Nov 2026 13:57:35 +0000 Subject: [PATCH 2/7] =?UTF-8?q?docs(proofs):=20PROOF-STATUS=20ledger=20?= =?UTF-8?q?=E2=80=94=20per-rung=20status=20with=20prover=20receipts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the proof ledger README-EXPLAINME-STANDARD section 5 requires before any proof is claimed. One row per rung R0–R18 of docs/ROUTE-PLAN.adoc, with the estate status vocabulary (PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED / OPEN) and the artefact that backs each row: - R2, R4, R10 and the R9 fold: PROVEN-WITH-AXIOMS in Rocq (verisimdb formal/Recovery.v, Coq 8.18.0; axioms = Octad.v whitelist). - R3, R9 merge laws, R8, R12 theory half: PROVEN in Agda (echo-types EchoPartialSection.agda, EchoFibreIntersection.agda, Agda 2.7.0.1 with the pinned stdlib and absolute-zero). - R5, R6, R7: PROVEN / PROVEN-WITH-AXIOMS (propext, Quot.sound) in Lean (tropical-types Resource/HubCeiling.lean, Lean 4.35.0). - R13 theory half and R14: PROVEN by pre-existing echo-types lemmas (EchoFiberCount, EchoTruncation now wired, EchoEntropy). - R0, R1, R11, R15, R16, the Creusot halves of R12/R13, R18: OPEN. R17: ASSUMED. Receipts record toolchain, command, result and the PR carrying each artefact. Nothing in src/ is covered; the engine is still a stub. PROOF-NEEDS.adoc and STATE.a2ml point at the ledger. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- .machine_readable/descriptiles/STATE.a2ml | 1 + PROOF-NEEDS.adoc | 10 +- PROOF-STATUS.adoc | 182 ++++++++++++++++++++++ 3 files changed, 190 insertions(+), 3 deletions(-) create mode 100644 PROOF-STATUS.adoc diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 3decd67..4aec155 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -38,6 +38,7 @@ 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-E7 before the engine session", "Re-target src/verisim.rs to real verisim-api routes", + "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", ] diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 3ca7250..eb8d150 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -4,9 +4,13 @@ * *LOC*: ~640 Rust (2026-11-05) * *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. 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. +* *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). * *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..51cefe5 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,182 @@ +// 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` +(no `functional_extensionality_dep` on this row — see 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` (functional_extensionality_dep). 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), `put_commutative_iff_trivial`. + +|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`. 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. Assumptions over all twelve `Print Assumptions` blocks: +`mval`, `ident`, `functional_extensionality_dep` — identical to the +`Octad.v` whitelist. Rows R2, R4, R9 (fold), R10 use only `mval`/`ident`; +R3's `fill_not_monotone` and the R10 fixpoint lemmas that rewrite octads use +`functional_extensionality_dep`. 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`; `[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. From d0d3885d28cbd6905a98bc77c71647b184aea7b5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 9 Nov 2026 14:05:09 +0000 Subject: [PATCH 3/7] fix(container): valid TOML in compose.toml, honest entrypoint warning, review nits; pin TOML validity with a test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit review on #80 (5 inline + 2 summary findings) and the two SonarCloud Containerfile findings: - container/compose.toml: the environment inline table spanned lines and had a trailing comma, which TOML 1.0 rejects, so selur-compose could not have loaded the file. It is now one line. New tests/container_config_test.rs parses compose.toml, manifest.toml and vordr.toml with the toml crate and pins the batch-job shape (no ports, no listening sockets, health probe disabled, no restarts), so the template's multi-line shape cannot come back unnoticed. - container/entrypoint.sh: the "runs offline against the workdir" claim was wrong — the client falls back to localhost:8080 and persistence errors are swallowed. An unset VERISIMDB_URL now prints a warning that session and phase events may not be recorded anywhere. - container/deploy.k9.ncl: the default BATCH_ID gains the shell PID so two batches started in the same second get distinct volumes; the end-of-run hint no longer names a k9-svc subcommand that may not exist and notes that the --rm container leaves nothing holding the volume. - README.adoc: Phase 5 is stated as adding no gate tightening beyond the L6 ceiling Phase 4 already reaches. - TEST-NEEDS.adoc: snapshot heading records the 2026-11-09 FFI-row update. - 0-AI-MANIFEST.a2ml: src/interface/ffi/ is "reserved for the FFI bridge", not "Zig FFI (The Bridge)". - container/Containerfile (SonarCloud S7018, S7031): apk packages sorted; consecutive RUN instructions merged. Verified: cargo test (26 pass, incl. the 3 new), cargo clippy --all-targets clean, sh -n container/entrypoint.sh. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- 0-AI-MANIFEST.a2ml | 2 +- README.adoc | 2 +- TEST-NEEDS.adoc | 2 +- container/Containerfile | 16 +++++++-------- container/compose.toml | 7 ++----- container/deploy.k9.ncl | 6 ++++-- container/entrypoint.sh | 8 +++++++- tests/container_config_test.rs | 36 ++++++++++++++++++++++++++++++++++ 8 files changed, 59 insertions(+), 20 deletions(-) create mode 100644 tests/container_config_test.rs 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/README.adoc b/README.adoc index a13e531..5357b0d 100644 --- a/README.adoc +++ b/README.adoc @@ -117,7 +117,7 @@ function: recovery is complete when cross-modal drift approaches zero. - 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 (gate ceiling L6 today; VCL-total levels 7-10 are future vcl-ut work) + - Phase 5: Convergence (no further gate tightening today: Phase 4 already reaches the L6 ceiling; VCL-total levels 7-10 are future vcl-ut work) * **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: diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index f30a599..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",] |=== diff --git a/container/Containerfile b/container/Containerfile index dcc4968..f1386b7 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -19,7 +19,7 @@ # ============================================================================ FROM cgr.dev/chainguard/wolfi-base:latest AS builder -RUN apk add --no-cache rust build-base pkgconf +RUN apk add --no-cache build-base pkgconf rust WORKDIR /build @@ -45,23 +45,21 @@ LABEL org.opencontainers.image.title="squeakwell" \ dev.cerrotorre.manifest="container/manifest.toml" # ca-certificates: TLS roots for the https:// VERISIMDB_URL in production. -RUN apk add --no-cache ca-certificates - -# Create non-root user for the application. -RUN addgroup -S appuser && adduser -S appuser -G appuser +# 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 COPY --from=builder /build/target/release/squeakwell /app/squeakwell COPY container/entrypoint.sh /app/entrypoint.sh -RUN chmod +x /app/entrypoint.sh - COPY container/manifest.toml /app/manifest.toml # Recovery working directories live under /data (mountable volume). -RUN mkdir -p /data && chown appuser:appuser /data -RUN chown -R appuser:appuser /app +RUN chmod +x /app/entrypoint.sh \ + && mkdir -p /data && chown appuser:appuser /data \ + && chown -R appuser:appuser /app ENV APP_LOG_FORMAT=json ENV APP_DATA_DIR=/data diff --git a/container/compose.toml b/container/compose.toml index 28cf762..2216769 100644 --- a/container/compose.toml +++ b/container/compose.toml @@ -27,11 +27,8 @@ version = "1.0" [services.squeakwell] image = "ghcr.io/hyperpolymath/squeakwell:latest.ctp" command = ["recover", "--workdir", "/data"] -environment = { - APP_LOG_FORMAT = "json", - APP_DATA_DIR = "/data", - VERISIMDB_URL = "${VERISIMDB_URL}", -} +# TOML 1.0: an inline table stays on one line with no trailing comma. +environment = { APP_LOG_FORMAT = "json", APP_DATA_DIR = "/data", VERISIMDB_URL = "${VERISIMDB_URL}" } # 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. diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index cfcf79a..a7ba38e 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -142,7 +142,9 @@ echo "K9: Validation passed." set -eu ENV="${1:-dev}" TAG="${IMAGE_TAG:-latest}" -BATCH_ID="${BATCH_ID:-$(date -u +%Y%m%dT%H%M%SZ)}" +# 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..." @@ -150,7 +152,7 @@ cd container && ./ct-build.sh && cd .. echo "K9: Running recovery batch $BATCH_ID against $VERISIMDB_URL (volume $VOLUME)..." podman run --rm -v "$VOLUME:/data" -e VERISIMDB_URL \ "ghcr.io/hyperpolymath/squeakwell:$TAG" recover --workdir /data -echo "K9: Batch $BATCH_ID for $ENV complete. Roll back with: BATCH_ID=$BATCH_ID k9-svc rollback" +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 diff --git a/container/entrypoint.sh b/container/entrypoint.sh index c5c497a..0e42238 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -14,7 +14,13 @@ DATA_DIR="${APP_DATA_DIR:-/data}" echo "Starting squeakwell..." echo " Data: ${DATA_DIR}" echo " Log: ${APP_LOG_FORMAT:-json}" -echo " VeriSimDB: ${VERISIMDB_URL:-}" +if [ -n "${VERISIMDB_URL:-}" ]; then + echo " VeriSimDB: ${VERISIMDB_URL}" +else + 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." +fi # The VOLUME directive in the Containerfile creates /data, but a bind-mount # might replace it with an empty directory owned by root. diff --git a/tests/container_config_test.rs b/tests/container_config_test.rs new file mode 100644 index 0000000..a8dbe32 --- /dev/null +++ b/tests/container_config_test.rs @@ -0,0 +1,36 @@ +// 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")); + assert!(svc.get("ports").is_none(), "a batch CLI exposes no ports"); +} + +#[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)); +} From 0da63688720aca3db93b8c5448643eccbc59e92d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:28:53 +0000 Subject: [PATCH 4/7] fix(container): per-batch VeriSimDB session id, redacted URL logging, empty-URL handling; correct ledger axiom attributions Review round 2 on PR 80 (CodeRabbit): - engine: session id comes from SQUEAKWELL_BATCH_ID when set (compose and the k9 component pass BATCH_ID through), else from the workdir path as before. Every container batch mounts its volume at /data, so the path alone made distinct batches share one squeakwell:sessions document. `session_id_for` is public and unit-tested. - verisim client: an empty or blank VERISIMDB_URL is treated as unset (compose substitutes "" for an unset variable); `from_env_value` makes this testable. - entrypoint: never prints VERISIMDB_URL (userinfo / query tokens would reach container logs); logs scheme and host only, and distinguishes unset from set-but-empty. shellcheck clean. - deploy.k9.ncl: the one-line recipes fail fast on an unset BATCH_ID or VERISIMDB_URL instead of running on "squeakwell-data-", and pass the batch id into the container. - tests: compose test now pins VERISIMDB_URL, SQUEAKWELL_BATCH_ID, the per-batch volume mount and its declaration. - PROOF-STATUS: per-lemma Print Assumptions re-run. fill_not_monotone does NOT use functional_extensionality_dep (ledger said it did); fold_merge_perm, step_progress and iter_9_fixpoint DO (ledger said R9 fold and R10 did not). weightedMeasure_append confirmed axiom-free. - README / PROOF-NEEDS / ROUTE-PLAN: no proofs in this repo and the Rust engine is unproved, but the theory rungs are ledgered; VCL-UT gating is planned, not implemented, with the L6 ceiling; hub-ceiling results are theory only; the echo-types gaps are closed in the open PR 370. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- PROOF-NEEDS.adoc | 5 ++++ PROOF-STATUS.adoc | 32 ++++++++++++++-------- README.adoc | 29 ++++++++++++++------ container/Containerfile | 2 +- container/compose.toml | 8 ++++-- container/deploy.k9.ncl | 9 ++++--- container/entrypoint.sh | 32 +++++++++++++++++++--- docs/ROUTE-PLAN.adoc | 12 ++++++--- src/engine/mod.rs | 25 +++++++++++++---- src/verisim.rs | 49 +++++++++++++++++++++++++++++++--- tests/container_config_test.rs | 27 +++++++++++++++++++ 11 files changed, 190 insertions(+), 40 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index eb8d150..5315b64 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -11,6 +11,11 @@ `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 index 51cefe5..fac2438 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -40,15 +40,17 @@ 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` -(no `functional_extensionality_dep` on this row — see receipt C1). +(`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` (functional_extensionality_dep). Audit modalities by chain -prefix: verisimdb `Provenance.v`, not re-proved here. +`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 @@ -85,12 +87,15 @@ 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), `put_commutative_iff_trivial`. ++ 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`. Not restated in Agda or Lean (needs +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. @@ -140,11 +145,15 @@ verisimdb `Drift.v` |ASSUMED |Not stated; `Drift.v` D1/D2 untouched. |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. Assumptions over all twelve `Print Assumptions` blocks: -`mval`, `ident`, `functional_extensionality_dep` — identical to the -`Octad.v` whitelist. Rows R2, R4, R9 (fold), R10 use only `mval`/`ident`; -R3's `fill_not_monotone` and the R10 fixpoint lemmas that rewrite octads use -`functional_extensionality_dep`. The nine pre-existing modules also compile +|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. @@ -165,7 +174,8 @@ 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`; `[propext, Quot.sound]` for the others. No +`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. |=== diff --git a/README.adoc b/README.adoc index 5357b0d..3e7cbd0 100644 --- a/README.adoc +++ b/README.adoc @@ -119,15 +119,24 @@ function: recovery is complete when cross-modal drift approaches zero. - Phase 4: Type tightening (VCL-total levels 4-6) - Phase 5: Convergence (no further gate tightening today: Phase 4 already reaches the L6 ceiling; VCL-total levels 7-10 are future vcl-ut work) -* **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: +* **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/container/Containerfile b/container/Containerfile index f1386b7..19b5783 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -12,7 +12,7 @@ # # Run one recovery batch (working directory on a named volume): # podman run --rm -v squeakwell-data-:/data -e VERISIMDB_URL \ -# squeakwell:latest recover --workdir /data +# -e SQUEAKWELL_BATCH_ID= squeakwell:latest recover --workdir /data # ============================================================================ # Stage 1: Builder diff --git a/container/compose.toml b/container/compose.toml index 2216769..1d43f8e 100644 --- a/container/compose.toml +++ b/container/compose.toml @@ -9,7 +9,9 @@ # 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: +# 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 @@ -28,7 +30,9 @@ version = "1.0" 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. -environment = { APP_LOG_FORMAT = "json", APP_DATA_DIR = "/data", VERISIMDB_URL = "${VERISIMDB_URL}" } +# 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. diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index a7ba38e..cc73ae4 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -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-$BATCH_ID:/data -e VERISIMDB_URL ghcr.io/hyperpolymath/squeakwell:latest recover --workdir /data", - migrate = "container/ct-build.sh && podman run --rm -v squeakwell-data-$BATCH_ID:/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", }, }, @@ -150,7 +153,7 @@ VOLUME="squeakwell-data-$BATCH_ID" echo "K9: Building squeakwell image for $ENV..." cd container && ./ct-build.sh && cd .. echo "K9: Running recovery batch $BATCH_ID against $VERISIMDB_URL (volume $VOLUME)..." -podman run --rm -v "$VOLUME:/data" -e VERISIMDB_URL \ +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 $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)." "%, diff --git a/container/entrypoint.sh b/container/entrypoint.sh index 0e42238..edc8b2a 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -14,12 +14,38 @@ DATA_DIR="${APP_DATA_DIR:-/data}" echo "Starting squeakwell..." echo " Data: ${DATA_DIR}" echo " Log: ${APP_LOG_FORMAT:-json}" -if [ -n "${VERISIMDB_URL:-}" ]; then - echo " VeriSimDB: ${VERISIMDB_URL}" -else +# 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 + case "$_rest" in *@*) _rest="${_rest##*@}" ;; esac + _rest="${_rest%%/*}" + _rest="${_rest%%\?*}" + printf '%s%s\n' "$_scheme" "$_rest" +} + +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 # The VOLUME directive in the Containerfile creates /data, but a bind-mount diff --git a/docs/ROUTE-PLAN.adoc b/docs/ROUTE-PLAN.adoc index 39c3f31..657ea2b 100644 --- a/docs/ROUTE-PLAN.adoc +++ b/docs/ROUTE-PLAN.adoc @@ -193,9 +193,15 @@ 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 R11 Creusot half, the drift + bridge R17, and any statement about f64 confidence (R18). + 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..335a2b1 100644 --- a/src/engine/mod.rs +++ b/src/engine/mod.rs @@ -51,11 +51,11 @@ pub struct EntityConfidence { 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 +127,21 @@ 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-empty `batch_id` (the `SQUEAKWELL_BATCH_ID` environment +/// variable, set by `container/compose.toml` and `container/deploy.k9.ncl` +/// from `BATCH_ID`) the ID is `sq:`, so two batches that both +/// mount their volume at `/data` get distinct sessions. Without one it falls +/// back to `sq:`, which is stable across restarts of the same +/// working directory. +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:{}", sha2_short(&format!("batch:{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..c1d129d 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,30 @@ 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 or + /// empty (an empty base URL would make every request fail with a + /// relative-URI error, which is a worse failure mode than the documented + /// localhost fallback). 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). + /// Blank values fall back to the default exactly like an unset variable. + 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 +210,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 index a8dbe32..3a4b2a8 100644 --- a/tests/container_config_test.rs +++ b/tests/container_config_test.rs @@ -17,7 +17,20 @@ fn compose_toml_parses_and_names_the_batch_service() { 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] @@ -34,3 +47,17 @@ fn vordr_toml_parses_with_health_probe_disabled() { 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:") && a.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)); +} From a2086007f03f8b8b63109c5c33bdd613851484cf Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:59:11 +0000 Subject: [PATCH 5/7] fix(container,engine): no URL in deploy output, redaction order, session namespaces; route-plan R11/R18 labels CodeRabbit review of 0da6368 on PR 80 (seven findings, all verified): - deploy.k9.ncl: the deploy script no longer echoes VERISIMDB_URL (credentials or tokens would reach deployment logs). - entrypoint.sh redact_url: cut path, query and fragment BEFORE userinfo. The old order turned https://host/v1?token=prefix@secret into https://secret. Now https://host. shellcheck clean. - engine::session_id_for: batch IDs are now sq:b:, workdir IDs stay sq: (unchanged, so existing sessions keep their IDs). The old batch form hashed "batch:", so a workdir literally named "batch:foo" collided with batch "foo"; the two shapes cannot collide now. - tests: pin that matching batch/workdir inputs (incl. "batch:foo") never share a session and that workdir IDs keep their shape. - README: Phase 4 gating is planned (the stub does not call vclt-gate); Phase 5 adds no level beyond the planned L6 ceiling. - ROUTE-PLAN 2.4: R11 is a Creusot proof in squeakwell, not an echo-types half; the f64 confidence statement belongs to the R6/R7 quantisation gap; R18 is the separate Kripke-world conjecture. cargo test: 29 passed; clippy clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- README.adoc | 4 ++-- container/deploy.k9.ncl | 3 ++- container/entrypoint.sh | 5 ++++- docs/ROUTE-PLAN.adoc | 7 +++++-- src/engine/mod.rs | 11 ++++++----- tests/container_config_test.rs | 10 +++++++++- 6 files changed, 28 insertions(+), 12 deletions(-) diff --git a/README.adoc b/README.adoc index 3e7cbd0..e96aae5 100644 --- a/README.adoc +++ b/README.adoc @@ -116,8 +116,8 @@ 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 (no further gate tightening today: Phase 4 already reaches the L6 ceiling; VCL-total levels 7-10 are future vcl-ut work) + - 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 diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index cc73ae4..8016bcb 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -152,7 +152,8 @@ 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 recovery batch $BATCH_ID against $VERISIMDB_URL (volume $VOLUME)..." +# 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 $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)." diff --git a/container/entrypoint.sh b/container/entrypoint.sh index edc8b2a..aa30115 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -23,9 +23,12 @@ redact_url() { *://*) _scheme="${_url%%://*}://"; _rest="${_url#*://}" ;; *) _scheme=""; _rest="$_url" ;; esac - case "$_rest" in *@*) _rest="${_rest##*@}" ;; 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" } diff --git a/docs/ROUTE-PLAN.adoc b/docs/ROUTE-PLAN.adoc index 657ea2b..e28b743 100644 --- a/docs/ROUTE-PLAN.adoc +++ b/docs/ROUTE-PLAN.adoc @@ -199,8 +199,11 @@ in each. 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 R11 Creusot half, the drift - bridge R17, and any statement about f64 confidence (R18). + `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 diff --git a/src/engine/mod.rs b/src/engine/mod.rs index 335a2b1..dcc0531 100644 --- a/src/engine/mod.rs +++ b/src/engine/mod.rs @@ -131,13 +131,14 @@ pub fn recover(workdir: &str, target_level: u8, drift_threshold: f64, max_iterat /// /// With a non-empty `batch_id` (the `SQUEAKWELL_BATCH_ID` environment /// variable, set by `container/compose.toml` and `container/deploy.k9.ncl` -/// from `BATCH_ID`) the ID is `sq:`, so two batches that both -/// mount their volume at `/data` get distinct sessions. Without one it falls -/// back to `sq:`, which is stable across restarts of the same -/// working directory. +/// from `BATCH_ID`) the ID is `sq:b:`, so two batches that both +/// mount their volume at `/data` get distinct sessions. Without one it is +/// `sq:`, unchanged from before, so existing workdir sessions +/// keep their IDs. The two forms differ in shape (`sq:b:` vs `sq:`), so a +/// batch ID can never collide with a workdir ID whatever the inputs. 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:{}", sha2_short(&format!("batch:{batch}"))), + Some(batch) => format!("sq:b:{}", sha2_short(batch)), None => format!("sq:{}", sha2_short(workdir)), } } diff --git a/tests/container_config_test.rs b/tests/container_config_test.rs index 3a4b2a8..b6c79a8 100644 --- a/tests/container_config_test.rs +++ b/tests/container_config_test.rs @@ -55,7 +55,15 @@ fn session_id_is_per_batch_when_a_batch_id_is_supplied() { 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:") && a.len() == 15); + 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(" "))); From df33c8899bd39b8ce0689f4c3d43f818ad3a6e22 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:00:07 +0000 Subject: [PATCH 6/7] style(container): default branch on the userinfo case in redact_url SonarCloud (shell rule: case without a default) on PR 80. Behaviour is unchanged: a URL with no '@' after the path/query cut passes through. shellcheck clean; redaction re-checked on the leak case and two others. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8 --- container/entrypoint.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/container/entrypoint.sh b/container/entrypoint.sh index aa30115..daf8cba 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -28,7 +28,10 @@ redact_url() { _rest="${_rest%%/*}" _rest="${_rest%%\?*}" _rest="${_rest%%#*}" - case "$_rest" in *@*) _rest="${_rest##*@}" ;; esac + case "$_rest" in + *@*) _rest="${_rest##*@}" ;; + *) ;; + esac printf '%s%s\n' "$_scheme" "$_rest" } From 68c504255ad971b90d543c757ff6c8d7d1a42af4 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:30:15 +0000 Subject: [PATCH 7/7] docs(engine,verisim): clarify recovery stub, session ID hashing, and URL normalization --- src/engine/mod.rs | 22 ++++++++++++++-------- src/verisim.rs | 11 ++++++----- 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/src/engine/mod.rs b/src/engine/mod.rs index dcc0531..73c1bca 100644 --- a/src/engine/mod.rs +++ b/src/engine/mod.rs @@ -42,12 +42,18 @@ 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); @@ -129,13 +135,13 @@ pub fn recover(workdir: &str, target_level: u8, drift_threshold: f64, max_iterat /// Derive the VeriSimDB session ID for a recovery run. /// -/// With a non-empty `batch_id` (the `SQUEAKWELL_BATCH_ID` environment +/// 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`) the ID is `sq:b:`, so two batches that both -/// mount their volume at `/data` get distinct sessions. Without one it is -/// `sq:`, unchanged from before, so existing workdir sessions -/// keep their IDs. The two forms differ in shape (`sq:b:` vs `sq:`), so a -/// batch ID can never collide with a workdir ID whatever the inputs. +/// 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)), diff --git a/src/verisim.rs b/src/verisim.rs index c1d129d..80316b3 100644 --- a/src/verisim.rs +++ b/src/verisim.rs @@ -46,16 +46,17 @@ 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 or - /// empty (an empty base URL would make every request fail with a - /// relative-URI error, which is a worse failure mode than the documented - /// localhost fallback). + /// 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 { Self::from_env_value(env::var("VERISIMDB_URL").ok()) } /// Build a client from the raw `VERISIMDB_URL` value (`None` = unset). - /// Blank values fall back to the default exactly like an unset variable. + /// 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())