fix: address the review findings left open when #98 merged

.github/workflows/dogfood-gate.yml

@@ -1,4 +1,4 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
@@ -71,7 +71,7 @@
       - name: Check for K9 files
         id: detect
         run: |
-          COUNT=$(find . \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path './.git/*' | wc -l)
+          COUNT=$(find . \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path './.git/*' -type f | wc -l)
           CONFIG_COUNT=$(find . \( -name '*.toml' -o -name '*.yaml' -o -name '*.yml' -o -name '*.json' \) \
             -not -path './.git/*' -not -path './node_modules/*' -not -path './.deno/*' \
             -not -name 'package-lock.json' -not -name 'Cargo.lock' -not -name 'deno.lock' | wc -l)
@@ -82,11 +82,15 @@
           fi
 
       - name: Validate K9 contracts
+        id: validate
         if: steps.detect.outputs.k9_count > 0
         run: bash .github/hooks/validate-k9.sh
       - name: Write summary
         run: |
           K9_COUNT="${{ steps.detect.outputs.k9_count }}"
+          # The hook skips the YAML session bindings, so report the files it
+          # actually validated, not every *.k9 path found.
+          VALIDATED="${{ steps.validate.outputs.files_scanned }}"
           CFG_COUNT="${{ steps.detect.outputs.config_count }}"
           if [ "$K9_COUNT" -eq 0 ]; then
             cat <<'EOF' >> "$GITHUB_STEP_SUMMARY"
@@ -99,7 +103,7 @@
           else
             echo "## K9 Contract Validation" >> "$GITHUB_STEP_SUMMARY"
             echo "" >> "$GITHUB_STEP_SUMMARY"
-            echo "Validated **${K9_COUNT}** K9 contract(s) against **${CFG_COUNT}** config file(s)." >> "$GITHUB_STEP_SUMMARY"
+            echo "Validated **${VALIDATED:-0}** of **${K9_COUNT}** K9 file(s) found. Counted **${CFG_COUNT}** config file(s), which K9 validation does not read." >> "$GITHUB_STEP_SUMMARY"
           fi
 
   # ---------------------------------------------------------------------------
@@ -376,7 +380,7 @@
           # eclexiaiser energy tracking?
           if [ -f "eclexiaiser.toml" ]; then
             SCORE=$((SCORE + 1))
             ECLEX_STATUS=":white_check_mark:"
           else
             ECLEX_STATUS=":ballot_box_with_check:"
           fi

CHANGELOG.adoc

@@ -34,6 +34,31 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
   `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment
   X1: reachability probe, HEAD by default, one-byte GET with `--get`).
 
+==== Fixed
+
+Findings from the last review of #98, which merged before they were
+addressed:
+
+* `build/setup.sh` — the Cargo fallback installs `just` into a named root
+  and puts that root's `bin` on `PATH`, so a distro Cargo without
+  `~/.cargo/bin` on `PATH` no longer fails setup after a successful install.
+* `tools/environments/probe-reachability.sh` — `--get` caps a body the
+  server sends despite the byte range (`range-ignored`); a non-GNU `ldd`
+  (FreeBSD) no longer stops the probe. `tests/probe_reachability_test.sh`
+  covers both.
+* `tools/proof-toolchain/toolchain.kyaml` — HOL Light's OCaml switch is a
+  locked runtime entry; Poly/ML takes the newest stable tag, since HOL4
+  names no version; Mizar names the i386 distribution it actually ships
+  (static binaries, needing IA32 emulation on the host).
+* `tools/environments/` and the environment proposal — the measurement adds
+  Cargo's real index and download hosts, which answer, so `cargo install`
+  is no longer reported as blocked by the refused crates.io API.
+* Proposals — PVS has a priority-1 owner (`awesome-hol`); X1 covers every
+  probeable environment class; `DRIFT` fields and the checker's lock hash
+  are named in the cartridge contracts.
+* `Justfile` `container-init` renders the `VERSION` placeholder; the dogfood gate's
+  summary counts the K9 files the hook validated, not every `*.k9` path.
+
 ==== Changed
 
 * `build/setup.sh` — when no system package provides `just`, setup runs

Justfile

@@ -385,10 +385,20 @@ container-init:
     read -rp "Container registry [ghcr.io/${OWNER:-hyperpolymath}]: " _REGISTRY
     REGISTRY="${_REGISTRY:-ghcr.io/${OWNER:-hyperpolymath}}"
 
+    read -rp "Service version (the K9 pedigree version) [0.1.0]: " _VERSION
+    VERSION="${_VERSION:-0.1.0}"
+    # The value lands inside quoted TOML and Nickel strings and a sed
+    # replacement, so allow only characters that are safe in all three.
+    if [[ ! "$VERSION" =~ ^[0-9A-Za-z._+-]+$ ]]; then
+        echo "Error: invalid version '$VERSION'. Use letters, digits, '.', '_', '+' or '-'." >&2
+        exit 1
+    fi
+
     echo ""
     echo "  Service: $SERVICE_NAME"
     echo "  Port:    $PORT"
     echo "  Registry: $REGISTRY"
+    echo "  Version: $VERSION"
     echo ""
     read -rp "Proceed? [Y/n] " CONFIRM
     [[ "${CONFIRM:-Y}" =~ ^[Nn] ]] && echo "Aborted." && exit 0
@@ -404,6 +414,7 @@ container-init:
         -e "s|${LB}SERVICE_NAME${RB}|${SERVICE_NAME}|g"
         -e "s|${LB}PORT${RB}|${PORT}|g"
         -e "s|${LB}REGISTRY${RB}|${REGISTRY}|g"
+        -e "s|${LB}VERSION${RB}|${VERSION}|g"
     )
 
     find container/ -type f | while read -r file; do

build/setup.sh

@@ -132,12 +132,28 @@ detect_platform() {
 # Cargo checks registry package checksums; --locked uses the release lockfile.
 # 1.56.0 matches the estate mise.lock pin and meets the estate floor (just >= 1.42,
 # standards 3-practice/provisioning/PROVISIONING-STANDARD.adoc).
+# The install root is CARGO_INSTALL_ROOT, then CARGO_HOME, then $HOME/.cargo
+# (using the first non-empty value). After a successful install, its bin
+# directory is added to PATH for this process if absent. Returns 1 if Cargo
+# is unavailable or installation fails.
 install_just_with_cargo() {
     if ! command -v cargo >/dev/null 2>&1; then
         fail "Install Cargo or just with your platform's package manager, then rerun setup."
         return 1
     fi
-    cargo install just --version 1.56.0 --locked
+    # Name the install root explicitly, so its bin directory is known: Cargo
+    # installs there but does not add it to this shell's PATH, and a distro
+    # Cargo often runs without ~/.cargo/bin on PATH.
+    cargo_root="${CARGO_INSTALL_ROOT:-${CARGO_HOME:-$HOME/.cargo}}"
+    cargo install just --version 1.56.0 --locked --root "$cargo_root" || return 1
+    case ":$PATH:" in
+        *":$cargo_root/bin:"*) ;;
+        *)
+            PATH="$cargo_root/bin:$PATH"
+            export PATH
+            warn "Added $cargo_root/bin to PATH for this run; add it to your shell profile too."
+            ;;
+    esac
 }
 
 install_just() {

docs/proposals/awesome-estate-maths-proving.adoc

@@ -149,7 +149,8 @@ Isabelle/jEdit and VSCode, Isabelle Zulip, IsaFoL.
 
 |`awesome-hol`
 |HOL4, HOL Light, HOL Zero, ProofPower, Candle, CakeML, OpenTheory, the
-HOL lineage; HOL Light's Flyspeck.
+HOL lineage; HOL Light's Flyspeck. A section on classical higher-order
+logic outside that lineage owns PVS and NASALib.
 |None (`awesome-provable` says "HOL" once).
 |Create
 |1
@@ -249,7 +250,8 @@ echidna's 12 core backends and every PROOF-POLICY route.
 === Where the small families go
 
 Mizar, Metamath, Naproche and Matita fold into
-`awesome-formalised-mathematics`; PVS and the leaner interactive provers
+`awesome-formalised-mathematics`; PVS is owned by `awesome-hol`, so a
+priority-1 list carries every core backend; the leaner interactive provers
 fold into the refreshed `awesome-provable` index; TLA+ is a section of
 `awesome-model-checking`; the hybrid-systems and real-algebra provers
 (KeYmaera X, dReal, QEPCAD, Redlog) appear in `awesome-mathematical-logic`

docs/proposals/boj-prover-solver-cartridges.adoc

@@ -99,7 +99,11 @@ hard-coded count.
 |`provers_check`
 |One prover: `PRESENT` with version and lock hash; `DRIFT` with observed
 version/hash, expected lock version/hash and the mismatch (not
-dispatchable); or `UNAVAILABLE` with the reason it could not run.
+dispatchable); or `UNAVAILABLE` with the reason it could not run. All of it
+comes from `provers.sh doctor --json`, which compares what it ran against
+`toolchain.lock.json`; `provers_check` adds nothing of its own. A `DRIFT`
+result carries `observed_version`, `observed_sha256`, `locked_version` and
+`locked_sha256`, and `mismatch` names which of the two differs.
 
 |`provers_prove`
 |`{file \| goal, prover?, timeout}` → `{verdict, trust_level, prover,
@@ -136,7 +140,9 @@ silently the latter.
 Every `solvers_sat` and `solvers_optimise` response carries `status:
 TESTED or PROVEN`, solver id, version and lock hash. `TESTED` carries the
 bounds and limits used. `PROVEN` requires a certificate reference and
-hash, the input hash, the independent checker's id and version, its
+hash, the input hash, the independent checker's id, version and
+`locked_sha256` (the lock's digest of its installed executable, so the
+exact checker binary is pinned), its
 successful check result, and any axioms used. An emitted certificate or
 unsat core alone does not establish `PROVEN`.
 

docs/proposals/environment-of-environments.adoc

@@ -15,8 +15,8 @@ are specified against the deed; the conversion of this repository's own
 files follows ruling D313.
 
 Status: proposal, 2026-10-27. Nothing here is built. The measured facts in
-<<measured>> were taken in one cloud agent session on that date and are
-reproducible with `tools/environments/probe-reachability.sh`.
+<<measured>> were taken in cloud agent sessions on 2026-10-27 and
+2026-11-04 and are reproducible with `tools/environments/probe-reachability.sh`.
 
 == The claim
 
@@ -43,7 +43,7 @@ report its real capabilities in one machine-readable form.
 |Surface |What it declares |Gap
 
 |`tools/proof-toolchain/toolchain.kyaml`
-|36 tools with roles under PROOF-POLICY, pins and smoke commands
+|37 tools with roles under PROOF-POLICY, pins and smoke commands
 |Declares tools, not environments. Covers the policy provers and their
 backends. Before E6 it covered 7 of echidna's 12 core backends; it now
 covers all 12 (see <<coverage>>).
@@ -77,15 +77,17 @@ so, not pass silently.
 |===
 
 [[measured]]
-== Measured facts from one agent session
-
-Taken 2026-10-27 in a Claude Code cloud session for this repository
-(Ubuntu 24.04.5, glibc 2.39, x86_64, outbound HTTPS through the session's
-agent proxy). The probe ran twice over the 22 URLs in
-`tools/environments/hosts.txt`: once with redirected HEAD requests, once
-with `--get`, a redirected GET for the first byte only. The code is the
-final response the proxy returned. Where the two methods differ, both are
-shown; elsewhere they agreed (200 to HEAD, 200 or 206 to GET).
+== Measured facts from agent sessions
+
+First taken 2026-10-27 and re-taken 2026-11-04 in Claude Code cloud
+sessions for this repository (Ubuntu 24.04.5, glibc 2.39, x86_64, outbound
+HTTPS through the session's agent proxy). The table is the 2026-11-04 run.
+The probe ran twice over the 24 URLs in `tools/environments/hosts.txt`:
+once with redirected HEAD requests, once with `--get`, a redirected GET for
+the first byte only, capped at 64 KiB for servers that ignore the range
+(`range-ignored`). The code is the final response the proxy returned.
+Where the two methods differ, both are shown; elsewhere they agreed (200
+to HEAD, 200 or 206 to GET).
 
 [cols="3,1,3",options="header"]
 |===
@@ -96,14 +98,16 @@ shown; elsewhere they agreed (200 to HEAD, 200 or 206 to GET).
 |`hackage.haskell.org` |200 |Reachable (Agda via cabal is possible in principle).
 |`static.rust-lang.org` (rustup-init) |200 |Reachable.
 |`releases.lean-lang.org` |200 |Reachable (elan toolchains).
-|`isabelle.in.tum.de`, `mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable.
+|`mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable.
+|`isabelle.in.tum.de` |200 (HEAD); 206 or reset (GET) |*Intermittent.* One GET of four succeeded; the others were reset during the TLS handshake. An install from it needs retries.
 |`ftp.gnu.org/gnu/guix` |200 |Reachable.
-|`smt-lib.org`, `www.tptp.org` |200 |Reachable.
+|`smt-lib.org`, `www.tptp.org` |200 |Reachable (TPTP ignores the byte range).
 |`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 (HEAD), 206 (GET, one byte) |*Reachable.* The request redirects to `release-assets.githubusercontent.com` and succeeds, and the first byte of the asset arrives. A full download was not attempted and no executable was run, so bundle transport is only partly verified.
-|`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files).
+|`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files; codeload ignores the byte range).
 |`github.com/Z3Prover/z3/releases/latest` |403 (HEAD and GET) |*Refused by the proxy.* The release landing page is not available, so "latest" cannot be discovered by scraping.
 |`api.github.com/repos/cvc5/cvc5/releases/latest` |403 (HEAD and GET) |Refused. Release discovery through the API is not available either.
-|`crates.io/api/v1/crates/just` |403 (HEAD and GET) |Refused. The API path cargo resolves through answers 403 to GET as well, so a cargo install from the registry is expected to fail here; one was not attempted.
+|`crates.io/api/v1/crates/just` |403 (HEAD and GET) |Refused. Cargo does not install through this API, so the refusal does not block `cargo install`.
+|`index.crates.io/ju/st/just`, `static.crates.io/crates/just/1.56.0/download` |200 (HEAD); 206 and 200 (GET) |*Reachable.* These are the sparse index and the download route `cargo install` requests (the index's `dl` plus `/{crate}/{version}/download`), so a Cargo install is expected to work here. One was not attempted. The download host ignores the byte range.
 |`ghcr.io/v2/`, `cgr.dev/v2/` |405 (HEAD), 401 (GET) |Registry answered; anonymous token flow not tested. The one case where the methods differ.
 |`cvc5.github.io` |200 |Reachable.
 |`downloads.sourceforge.net` (SBCL x86-64 Linux binary) |200 (HEAD), 206 (GET, one byte) |Reachable: the source the `sbcl` entry fetches.
@@ -215,10 +219,10 @@ sealed-container concern, per the 2026-05-18 packaging ruling.
 |Z3 |`z3` |Covered
 |CVC5 |`cvc5` |Covered
 |Metamath |none needed |Pure-Rust, in-process in echidna
-|HOL Light |`hol-light` |Covered (added 2026-10-27 on the owner's decision; opam)
+|HOL Light |`hol-light` with `hol-light-ocaml` |Covered (added 2026-10-27 on the owner's decision; opam, in a locked OCaml switch)
 |HOL4 |`hol4` with `polyml` |Covered (added 2026-10-27; source build on bundled Poly/ML)
 |ACL2 |`acl2` with `sbcl` |Covered (added 2026-10-27; tagged source from GitHub, built on bundled SBCL)
-|Mizar |`mizar` |Covered (added 2026-10-27; system distribution with its MML)
+|Mizar |`mizar` |Covered (added 2026-10-27; the static i386 distribution with its MML, so the host kernel needs IA32 emulation)
 |PVS |`pvs` with `sbcl` |Covered (added 2026-10-27; BSD-3-Clause source build on bundled SBCL)
 |===
 
@@ -282,9 +286,14 @@ impression.
 |Id |Experiment |Pass criterion
 
 |X1
-|Run `tools/environments/probe-reachability.sh` in each environment class:
-workstation, this session class, a GitHub-hosted runner, the devcontainer.
-|A reachability row per class in `environments.kyaml` `measured`, dated.
+|Run `tools/environments/probe-reachability.sh`, with and without `--get`,
+in each environment class that runs a shell: workstation, this session
+class, a GitHub-hosted runner, the devcontainer, a Guix shell and the
+sealed container (whose `--network=none` run must record every host
+unreachable). `boj-registered` is excluded: it is a server's view of the
+others, not a place a probe runs.
+|A dated `measured` block for each of the six probeable classes in
+`environments.kyaml`; `boj-registered` keeps an empty one.
 The design's host assumptions are replaced by measurements.
 
 |X2

tests/probe_reachability_test.sh

@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Test tools/environments/probe-reachability.sh with stub curl and ldd
+# executables, so no network is used. The stub curl reproduces what curl 8.5
+# was measured to do (2026-11-04) against servers that ignore a byte range:
+# with --max-filesize it stops and exits 63, still reporting the status code.
+# Checks: a non-GNU ldd does not stop the probe; --get passes the size cap
+# and reports a capped transfer as range-ignored; outcomes are classified;
+# --json is valid; an unknown argument exits 2. Needs jq.
+set -euo pipefail
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+probe="$repo_root/tools/environments/probe-reachability.sh"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+mkdir -p "$work/bin"
+cat > "$work/hosts.txt" <<'EOF'
+# comment line
+https://range-ignoring.test/big.bin
+https://honours-range.test/file
+https://refusing.test/api
+https://bad-cert.test/
+EOF
+
+# Stub curl: the URL is the last argument; -w '%{http_code}' output goes to
+# stdout, as with the real curl.
+cat > "$work/bin/curl" <<'SH'
+#!/bin/sh
+args="$*"
+for url in "$@"; do :; done
+case "$args" in *" -r 0-0 "*) mode=get ;; *" -I "*) mode=head ;; *) echo "stub curl: no method in: $args" >&2; exit 97 ;; esac
+if [ "$mode" = get ]; then
+    case "$args" in *"--max-filesize 65536"*) ;; *) echo "stub curl: GET without size cap" >&2; exit 97 ;; esac
+fi
+case "$url" in
+    https://range-ignoring.test/*) printf 200; [ "$mode" = get ] && exit 63; exit 0 ;;
+    https://honours-range.test/*)  [ "$mode" = get ] && printf 206 || printf 200; exit 0 ;;
+    https://refusing.test/*)       printf 403; exit 0 ;;
+    https://bad-cert.test/*)       printf 000; exit 60 ;;
+esac
+printf 000; exit 6
+SH
+# A FreeBSD-style ldd: exists, rejects --version.
+printf '#!/bin/sh\necho "ldd: illegal option -- -" >&2\nexit 1\n' > "$work/bin/ldd"
+chmod +x "$work/bin/curl" "$work/bin/ldd"
+
+run() { PATH="$work/bin:$PATH" HOSTS_FILE="$work/hosts.txt" bash "$probe" "$@"; }
+row() { grep -Eq "^$1 +$2 +$3\$" <<<"$4" || fail "expected '$1 $2 $3' in: $4"; }
+
+head_out="$(run)" || fail "HEAD probe exited non-zero with a non-GNU ldd"
+grep -q 'glibc' <<<"$head_out" && fail "non-GNU ldd reported as glibc"
+row 200 reachable 'https://range-ignoring\.test/big\.bin' "$head_out"
+row 403 refused 'https://refusing\.test/api' "$head_out"
+row 000 tls-failed 'https://bad-cert\.test/' "$head_out"
+
+get_out="$(run --get)" || fail "GET probe exited non-zero"
+row 200 range-ignored 'https://range-ignoring\.test/big\.bin' "$get_out"
+row 206 reachable 'https://honours-range\.test/file' "$get_out"
+
+json="$(run --json --get)" || fail "JSON probe exited non-zero"
+jq -e '.method == "get" and (.hosts | length) == 4 and
+       ([.hosts[].outcome] | sort) == ["range-ignored","reachable","refused","tls-failed"]' \
+    <<<"$json" >/dev/null || fail "JSON output wrong: $json"
+
+rc=0; run --bogus >/dev/null 2>&1 || rc=$?
+[ "$rc" -eq 2 ] || fail "unknown argument exited $rc, expected 2"
+
+echo 'PASS: probe tolerates non-GNU ldd, caps range-ignoring GETs, classifies outcomes'

tests/proof_smoke_wrappers_test.sh

@@ -17,7 +17,11 @@
     mizar-smoke.sh pvs-smoke.sh pvs_smoke.pvs; do
     [ -f "$prefix/share/smoke/$fixture" ] || { echo "FAIL: $fixture not installed" >&2; exit 1; }
 done
-chmod -R a-w "$prefix/share/smoke"  # a wrapper that writes here now fails
+# Record the whole prefix (smoke fixtures and the MML at share/mizar alike), so
+# a write anywhere under it is caught even when running as root, where
+# read-only permissions do not stop writes.
+snapshot() { (cd "$prefix" && find . -print0 | sort -z | xargs -0 stat -c '%n %s %y' 2>/dev/null); }
+before="$(snapshot)"
 
 expect() {  # expect pass|fail <description> <command...>
     local want="$1" what="$2"; shift 2
@@ -73,7 +77,5 @@
 expect fail "pvs no summary" pvs silent
 expect fail "pvs non-zero exit" pvs crash
 
-[ -z "$(find "$prefix/share/smoke" -newer "$prefix/share/smoke/pvs_smoke.pvs" ! -path "$prefix/share/smoke")" ] ||
-    { echo "FAIL: a wrapper wrote into the prefix" >&2; exit 1; }
-chmod -R u+w "$prefix"
+[ "$(snapshot)" = "$before" ] || { echo "FAIL: a wrapper wrote into the prefix" >&2; exit 1; }
 echo 'PASS: smoke installer and Mizar/PVS wrappers'