From 71a71181652349060deb85d2b00076571607a286 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 09:10:00 +0000 Subject: [PATCH 01/16] docs(proposals): environment-of-environments design and the awe-estate maths/proving lists Two proposals and one measured artefact set, as groundwork for roadmap M2. docs/proposals/environment-of-environments.adoc: how bofj-kitt becomes the environment of environments. An environment manifest beside the toolchain manifest (E1), one capability record with one producer and named consumers (E2), every environment-specific file rendered from the two manifests (E3), the agent-session leg (E4), BoJ registration through Groove capabilities (E5), and coverage of echidna's 12 core backends, of which the toolchain manifest lacks five (E6). Options A-D rated for elegance, dependability and security; experiments X1-X5 with pass criteria; the Idris2 route for the capability record under PROOF-POLICY. docs/proposals/awesome-estate-maths-proving.adoc: the awesome lists to create in stuff-of-awe for maths, proving and solving, cut by tool family from echidna's 141-variant roster (21 lists, 13 at priority 1), what folds where, and the tools echidna's ProverKind itself lacks, starting with the ones PROOF-POLICY names (Creusot, Kani, Aeneas, Lambdapi-as-checker, agda2dedukti, Yices). tools/environments/: environments.kyaml (seven environment classes with a `measured` block), probe-reachability.sh (HEAD-only reachability probe, text or JSON) and hosts.txt. The agent-session entry carries the 2026-10-27 measurement: opam.ocaml.org and alire.ada.dev reachable, GitHub release pages and api.github.com refused (403), fetched-binary execution denied by session policy. These contradict two assumptions in tools/proof-toolchain/DESIGN.adoc, which now points at the measurement. Validated: asciidoctor --failure-level WARN on every touched .adoc; the kyaml parses with yq (7 environments); the probe ran in this session (20 hosts, JSON validated with jq); scripts/check-no-md-in-docs.sh passes. scripts/check-root-shape.sh fails on ARCHITECTURE.adoc and MAINTAINERS, which predates this change (commit 8b81ae2). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .machine_readable/6a2/STATE.a2ml | 1 + CHANGELOG.adoc | 15 + .../awesome-estate-maths-proving.adoc | 431 ++++++++++++++++++ .../environment-of-environments.adoc | 355 +++++++++++++++ tools/environments/README.adoc | 42 ++ tools/environments/environments.kyaml | 32 ++ tools/environments/hosts.txt | 33 ++ tools/environments/probe-reachability.sh | 94 ++++ tools/proof-toolchain/DESIGN.adoc | 8 + 9 files changed, 1011 insertions(+) create mode 100644 docs/proposals/awesome-estate-maths-proving.adoc create mode 100644 docs/proposals/environment-of-environments.adoc create mode 100644 tools/environments/README.adoc create mode 100644 tools/environments/environments.kyaml create mode 100644 tools/environments/hosts.txt create mode 100755 tools/environments/probe-reachability.sh diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index fc79819..9acf9b4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -39,6 +39,7 @@ actions = [ "M1 — fill the remaining ~75 placeholder-token files (container/, .devcontainer/, .github/*)", "M1 — restore a full SECURITY policy once PGP material exists", "M2 — specify the kit's first capability and its BoJ integration contract", + "M2 — decide the proposals in docs/proposals/environment-of-environments.adoc (E1–E6, X1–X5) and docs/proposals/awesome-estate-maths-proving.adoc", ] [maintenance-status] diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ca1c652..ea426c7 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,3 +7,18 @@ Changelog], and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] + +==== Added + +* `docs/proposals/environment-of-environments.adoc` — how the kit becomes + the environment of environments: an environment manifest beside the + toolchain manifest, one capability record, rendered projections, the + agent-session leg, BoJ registration, and coverage of echidna's core + backends; with measured reachability from one agent session and the + experiments to run before building. +* `docs/proposals/awesome-estate-maths-proving.adoc` — the awesome lists to + create in `stuff-of-awe` for maths, proving and solving, derived from + echidna's prover roster, and the tools echidna itself lacks. +* `tools/environments/` — `environments.kyaml` (environment classes with a + `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment + X1: HEAD-only reachability probe). diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc new file mode 100644 index 0000000..bccfd75 --- /dev/null +++ b/docs/proposals/awesome-estate-maths-proving.adoc @@ -0,0 +1,431 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Awesome lists for maths, proving and solving in the stuff-of-awe estate +:toc: +:toclevels: 3 +:sectnums: + +Status: proposal, 2026-10-27. The roster below was read from echidna's +`crates/echidna-core/src/prover_kind.rs` (141 variants), its +`docs/PROVER_COUNT.adoc` (12 core, 105 implementation files, 46 +type-discipline variants with no binary) and `src/rust/provers/` (the binary +each backend spawns). The existing lists were read from the `stuff-of-awe` +organisation on the same date. + +This proposal lives in bofj-kitt because the kit is where the estate decides +which provers an environment carries; the lists are the human index of the +same roster. Nothing here creates a repository; see <>. + +== What the awe estate holds today + +Eleven repositories, all in `stuff-of-awe`: + +[cols="2,1,3",options="header"] +|=== +|Repository |Lines |Maths or proving coverage + +|`awesome-provable` |338 |General index, 2018-era content: Coq, Isabelle, +"HOL", Lean (as a Microsoft Research project), Idris, Agda, Viper, seL4, +CompCert. No Lean 4, no Rocq, no solver of any kind. +|`awesome-coq` |598 |Strong; carries coq-community content and already +names Rocq tooling. +|`awesome-agda` |73 |Thin; one mention of Cubical Agda, nothing on the +standard library versions, 1lab, UniMath or agda2dedukti. +|`awesome-idris2` |large |Strong; the estate's own. +|`awesome-haskell`, `awesome-ocaml`, `awesome-fsharp`, `awesome-gleam` +(fork), `awesome-zig` (fork), `awesome-nickel`, `awesome-ipfs` |— |Language +and infrastructure lists; not proving. +|=== + +Of echidna's 12 core backends, the estate's lists name 5 (Agda, Coq, +Isabelle, Lean, the HOL family) and none of the solvers (Z3, CVC5). Of the +remaining 129 variants, the lists name Idris2, Viper and nothing else. + +The upstream `sindresorhus/awesome` index, read on the same date, has +entries for Coq, Idris, Math, Theoretical Computer Science, Computational +Geometry, Julia, Scientific Computing, JAX and R, and *no* entry for Lean, +Agda, Isabelle, TLA+, SAT or SMT, constraint programming, model checking, +logic or formal verification in general. The gap is real upstream, not only +in the estate. + +== The rule for cutting lists + +One list per *family of reasoning tool*, not per tool and not per echidna +tier. echidna's tiers are CI cadence (every PR, nightly, smoke), which is +no help to a reader. Families are what a reader searches for: "an SMT +solver", "a model checker", "a logical framework". The exceptions are the +anchor systems of echidna's core, where a per-system list is what the +upstream community expects and where the estate already has three (Coq, +Agda, Idris2). + +Where a maintained upstream list exists, fork it, as the estate did for +`awesome-zig` and `awesome-gleam`, and specialise. Where none exists, +create. Each new repository takes the shape `awesome-nickel` has (README, +EXPLAINME, governance, the estate CI set, the Idris2 link-validation tests). + +== Proposed lists + +Priority: *1* covers echidna's core or a PROOF-POLICY route; *2* covers +the extended roster; *3* is the maths side the estate has no list for. + +[cols="2,3,2,1,1",options="header"] +|=== +|List |Scope and echidna members |Upstream |Fork or create |Priority + +|`awesome-smt` +|SMT solvers and formats: Z3, CVC5, Alt-Ergo, OpenSMT, SMT-RAT, dReal, +Yices, Boolector, Bitwuzla, MathSAT, SMTInterpol; SMT-LIB, Alethe, LFSC, +SMTCoq; SMT-COMP. +|None dedicated (`awesome-sat-solvers` is SAT only). +|Create +|1 + +|`awesome-atp` +|Automated theorem provers: Vampire, E, SPASS, iProver, Zipperposition, +Leo-III, Satallax, Lash, AgsyHOL, Twee, Prover9/Mace4, leanCoP, ileanCoP, +nanoCoP, Princess, MetiTarski, MizAR; TPTP/TSTP; CASC; Sledgehammer as the +bridge to ITPs. +|None. +|Create +|1 + +|`awesome-sat` +|SAT solvers and proof formats: CaDiCaL, Kissat, MiniSat, Varisat, CreuSAT; +DRAT, LRAT, FRAT; SAT competition; encodings. +|`awesome-sat-solvers` exists (owner to confirm before forking). +|Fork if licence allows, else create +|2 + +|`awesome-model-checking` +|SPIN, NuSMV and nuXmv, TLC, TLAPS, Apalache, Alloy, PRISM, Storm, UPPAAL +and Stratego, ProB, CBMC, ESBMC, JBMC, SeaHorn, Kind 2, Ivy, CPAchecker, +Ultimate; TLA+ as a section. +|None (hohieuai and ElNiak `awesome-formal-verification` cover it as one +section of a general list). +|Create +|1 + +|`awesome-program-verifiers` +|Auto-active and deductive verifiers: Dafny, Why3, Cameleer, Frama-C, +Boogie, Viper with Prusti, Gobra and Nagini, KeY, F*, SPARK/GNATprove, +Stainless, LiquidHaskell, Creusot, Kani, Verus, Aeneas and Charon. This is +the tool list; `awesome-provable` becomes the umbrella index that points +at it. +|`awesome-provable` (ours, stale). +|Create, and refresh `awesome-provable` as the index +|1 + +|`awesome-logical-frameworks` +|Twelf, Abella, Beluga, Dedukti, Lambdapi, λProlog (Teyjus, Elpi), Minlog, +Nuprl, agda2dedukti; proof interchange: OpenTheory, Dedukti, TPTP, Alethe, +Lean export. This is the PROOF-POLICY §2 transport route. +|None. +|Create +|1 + +|`awesome-type-systems` +|The disciplines echidna routes through `typed_wasm`: substructural +(linear, affine, relevant, ordered, uniqueness, bunched), modal, temporal, +session and choreographic, effect rows and coeffects, gradual, refinement, +indexed, homotopy and cubical; Arend, Cubical Agda, Cedille, Matita, Lego; +HoTT libraries (UniMath, HoTT-Agda, 1lab, cubical); the estate's TypeLL, +Katagoria and tropical-resource-typing. +|None (`awesome-type-theory` does not exist). +|Create +|1 + +|`awesome-isabelle` +|Isabelle/HOL and Isabelle/ZF, the AFP, Sledgehammer, Nitpick, Nunchaku, +Isabelle/jEdit and VSCode, Isabelle Zulip, IsaFoL. +|None. +|Create +|1 + +|`awesome-hol` +|HOL4, HOL Light, HOL Zero, ProofPower, Candle, CakeML, OpenTheory, the +HOL lineage; HOL Light's Flyspeck. +|None (`awesome-provable` says "HOL" once). +|Create +|1 + +|`awesome-lean` +|Lean 4, Lean 3 legacy and the mathlib3 to mathlib4 port pairs echidna +uses, Mathlib, Aesop, Lake, elan, LeanDojo, Lean Copilot, verso, the Lean +FRO; a section on proving without Mathlib, which PROOF-POLICY §2 requires. +|`saviorand/awesome-lean`, `pdehaye/awesome-lean`. +|Fork saviorand (check licence), then specialise +|1 + +|`awesome-acl2` +|ACL2, ACL2s, the community books, Milawa, the ACL2 workshop series. +|None. +|Create (small) +|2 + +|`awesome-formalised-mathematics` +|Libraries and corpora: Mathlib, the AFP, the Mizar Mathematical Library, +set.mm and Metamath Zero, math-comp, UniMath, ACL2 books; Mizar, Naproche +and ForTheL; benchmarks: miniF2F, ProofNet, PutnamBench; Xena, Formal +Abstracts. Mirrors echidna's 20 corpus adapters. +|None. +|Create +|1 + +|`awesome-neurosymbolic-proving` +|LeanDojo and ReProver, Lean Copilot, AlphaProof and AlphaGeometry, HTPS, +GPT-f, TacticToe, CoqGym and ASTactic, Proverbot9001, Thor, Magnushammer, +Baldur, DeepSeek-Prover, Goedel-Prover; premise selection and GNN ranking; +autoformalization. The field echidna's Julia layer sits in. +|None. +|Create +|1 + +|`awesome-constraint-solving` +|MiniZinc, Chuffed, OR-Tools and CP-SAT, GLPK, SCIP, HiGHS, Gecode, Picat, +Choco, Clingo (ASP), Z3 optimisation; MiniZinc Challenge. +|None (`awesome-constraint-programming` does not exist). +|Create +|2 + +|`awesome-security-protocol-verification` +|Tamarin, ProVerif, CryptoVerif, EasyCrypt, Maude-NPA, Scyther, Verifpal, +Squirrel, Jasmin, hacspec, SSProve. +|None. +|Create +|2 + +|`awesome-hardware-verification` +|ABC, GPUVerify, Faial, Yosys and SymbiYosys, Kind 2, Bluespec, Chisel +formal. +|`ben-marshall/awesome-open-hardware-verification`. +|Fork +|3 + +|`awesome-ontology-reasoning` +|Description-logic reasoners: ELK, Konclude, HermiT, Pellet and Openllet, +FaCT++; OWL API, Protégé. Ties to the template's `docs/theory/ontologies/`. +|None. +|Create +|2 + +|`awesome-mathematical-logic` +|Proof theory, model theory, modal and description logic (MetTeL2), +rewriting and termination (CSI, AProVE, TTT2, Maude), dynamic logic +(KeYmaera X), real algebra (QEPCAD, Redlog). +|None. +|Create +|3 + +|`awesome-computer-algebra` +|SageMath, Maxima, GAP, PARI/GP, Singular, Macaulay2, FriCAS, Reduce +(Redlog's host), Oscar.jl and Nemo.jl, Symbolica. +|None in the upstream index. +|Create +|3 + +|`awesome-math` +|Learning resources for mathematics. +|`rossant/awesome-math`. +|Fork +|3 + +|`awesome-category-theory` +|nLab, Catlab.jl, agda-categories, 1lab, applied category theory, string +diagrams. +|To check before creating. +|Check, then create +|3 +|=== + +Twenty-one lists; thirteen at priority 1, which together name every one of +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 +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` +with cross-links from `awesome-smt`. A list with fewer than about twenty +entries is a section, not a repository. + +[[echidna-gaps]] +== What echidna should cover anyway + +Reading the roster against the tools the lists above name shows what +`ProverKind` lacks. Grouped by why it matters: + +[cols="1,3",options="header"] +|=== +|Group |Missing from `ProverKind` + +|*PROOF-POLICY names them* (highest priority: the estate's own mapping +cannot be dispatched through its own prover platform) +|Creusot, Kani, Aeneas (with Charon), Lambdapi as a checker (Dedukti has a +variant, Lambdapi only an exchange format), agda2dedukti as a translator, +Yices (in the kit manifest as a backend). + +|*SMT* +|Boolector, Bitwuzla, MathSAT, SMTInterpol, Yices. + +|*Model checking* +|Apalache, Kind 2, Ivy, CPAchecker, Ultimate Automizer, ESBMC, JBMC. + +|*Program verification* +|Verus, Prusti, Gobra, Nagini, VeriFast. + +|*Type theory and HOL* +|Cedille and Lego (named in `PROVER_COUNT.adoc` tier 3 but absent from the +enum: documentation drift), Beluga, Candle, HOL Zero, ProofPower, Metamath +Zero. + +|*Security protocols* +|Maude-NPA, Scyther, Verifpal, Squirrel. + +|*Rewriting and termination* +|TTT2, Maude, NaTT. + +|*Ontology reasoning* +|HermiT, Pellet and Openllet, FaCT++. + +|*Constraints* +|Gecode, Picat, Clingo, HiGHS. +|=== + +Two further points belong in echidna rather than in a list: + +* `PROVER_COUNT.adoc` tier 3 names Cedille, Lego and CVC4; none has a + variant. The canonical count file is drifting from the enum it describes. +* `provers.a2ml` records only a slug per variant. The binary each backend + spawns is readable only from the Rust source. A `binary` field per entry + would let the kit's capability record and the lists above be rendered + from one registry. + +== Options compared + +[cols="1,3,1,1,1",options="header"] +|=== +|Option |Shape |Elegance / correctness |Dependability |Security / privacy + +|*A. Family lists* (recommended) +|Twenty-one repositories as above, thirteen first. +|High. Each list has a reader-facing scope and a single family; coverage +of the roster is checkable. +|Medium. Twenty-one repositories to keep from rotting; the estate CI set +(link checks, governance) does most of that. +|Neutral. Lists carry no secrets; CC0 content, as `awesome-idris2`. + +|*B. One list per echidna tier* +|Ten repositories mirroring `PROVER_COUNT.adoc`. +|Low. Tiers are CI cadence; a reader does not search by "nightly". +|Medium. +|Neutral. + +|*C. One `awesome-provers` mega-list* +|A single repository with every family as a section. +|Low. Reproduces `ElNiak/awesome-formal-verification`; sections of a +thousand lines are not curated, they are dumped. +|Low. One file, every contributor conflict. +|Neutral. + +|*D. Alternative path: rendered lists* +|A per-tool registry (echidna `provers.a2ml` with `binary`, `homepage`, +`family`, `licence`, `formats`, kit manifest id) and one renderer in +bofj-kitt that emits each list's tool table; curated prose stays +hand-written around it. The same `render` pattern as `provers.sh render`. +|Highest. The lists cannot drift from the roster; a new `ProverKind` +variant appears in the right list on the next render. +|Medium until the registry is filled; high after. The renderer is one +shell script over `yq` and `jq`. +|Neutral; the registry is public data. +|=== + +Recommendation: A for the repositories, with D as the way their tool +tables are produced once the registry fields exist in echidna. Start with +the thirteen priority-1 lists; hand-curate their prose; render their tool +tables as soon as `provers.a2ml` carries the fields. + +== Experiments before the first batch + +[cols="1,3,2",options="header"] +|=== +|Id |Experiment |Pass criterion + +|Y1 +|Run `lychee` over the eleven existing READMEs to baseline link rot before +adding twenty-one more. +|A dated rot percentage per list; a budget for the CI link gate. + +|Y2 +|Render one list's tool table (`awesome-smt`) from a hand-filled registry +fragment for its eleven tools, and diff against a hand-written table. +|Identical content; the renderer is adopted for the rest. + +|Y3 +|Check the licence of `saviorand/awesome-lean` and `awesome-sat-solvers` +and whether their maintainers accept upstream pull requests. +|Fork decisions become facts; a list whose upstream rejects contributions +is created, not forked. + +|Y4 +|Submit one of the created lists to `sindresorhus/awesome` to learn the +acceptance bar (the index has no formal-methods entry today). +|Accepted, or the review's objections are folded into the template the +other lists use. +|=== + +== The formal route + +The lists are data about tools, and the one property worth stating +formally is *coverage*: every variant of `ProverKind` is named by exactly +one priority-1 or priority-2 list, and every tool the kit manifest names +is in a list. With the registry of option D that is a finite relation and +the check is a test (`TESTED`), the same kind of check `awesome-nickel` +already runs in Idris2 over its links. It is not worth a theorem; it is +worth a gate. + +== Aspects + +Maintenance:: Twenty-one repositories is the real cost. The estate CI set +(governance, link check, Idris2 validation tests) is what keeps a list from +becoming a 2018 snapshot like `awesome-provable`. Do not create a list +without it. +Licensing:: Lists are CC0 (as `awesome-idris2`) so they can be forked and +merged upstream freely; `awesome-coq` carries coq-community content under +its upstream licence and must keep saying so. +Attribution:: Forked lists keep upstream history and the original +maintainers in `MAINTAINERS`. +Accessibility:: Each list is one AsciiDoc file with a table of contents; +no images carry information. +Template fit:: The standards spec-templates put `awesome-idris2` and +`awesome-nickel` on the `cli-tool` archetype with ABI-1..5 proofs. A list +has no ABI. The template needs a `list` or `docs` archetype before +twenty-one more lists inherit the wrong obligations. + +== Beyond this repository + +* `stuff-of-awe`: twenty-one repositories to create or fork, and two to + refresh (`awesome-provable`, `awesome-agda`). +* `hyperpolymath/echidna`: the <> as issues; the + `PROVER_COUNT.adoc` tier-3 drift; the `binary` and registry fields in + `provers.a2ml`. +* `hyperpolymath/standards`: a `list` archetype in + `docs/proofs/spec-templates/`; estate-board rows for the new + repositories; a decision on the `stuff-of-awe` organisation's place in + the clade index. +* `hyperpolymath/rsr-template-repo`: an awesome-list mint profile so each + new list starts with the `awesome-nickel` shape rather than being + hand-copied. +* `sindresorhus/awesome`: the submissions in Y4. + +[[decisions]] +== Decisions needed + +. Confirm option A and the thirteen priority-1 lists as the first batch, + or trim. +. Confirm `stuff-of-awe` as the organisation for all of them (the estate + board still lists the existing lists under `hyperpolymath/`). +. Whether `awesome-lean` and `awesome-sat` are forks (pending Y3) or fresh. +. Whether to open the echidna gap issues now, or after the first batch of + lists exists to cite. diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc new file mode 100644 index 0000000..5656d33 --- /dev/null +++ b/docs/proposals/environment-of-environments.adoc @@ -0,0 +1,355 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += bofj-kitt as the environment of environments +:toc: +:toclevels: 3 +:sectnums: + +Status: proposal, 2026-10-27. Nothing here is built. The measured facts in +<> were taken in one cloud agent session on that date and are +reproducible with `tools/environments/probe-reachability.sh`. + +== The claim + +The estate runs proofs and builds in several *kinds* of environment: the +workstation, cloud agent sessions, CI runners, dev containers, Guix shells, +sealed containers, and the hosts that echidna, echidnabot and proof-burrower +dispatch to. Each kind installs tools its own way, reaches a different set +of hosts, and reports what it holds in a different way, or not at all. + +bofj-kitt already owns one half of the answer: the proof-toolchain manifest +(`tools/proof-toolchain/toolchain.kyaml`) declares *which tools* exist. The +other half is missing: nothing declares *which environments* exist, what +each one can reach and run, and how it reports back. Adding that second +declaration, and making both the only inputs from which every +environment-specific file is rendered, is what makes bofj-kitt the +environment of environments: one place that describes every environment +class, projects the same declared toolchain onto each, and makes each +report its real capabilities in one machine-readable form. + +== What exists today + +[cols="1,2,2",options="header"] +|=== +|Surface |What it declares |Gap + +|`tools/proof-toolchain/toolchain.kyaml` +|29 tools with roles under PROOF-POLICY, pins and smoke commands +|Declares tools, not environments. Covers the policy provers and their +backends; covers 7 of echidna's 12 core backends (see <>). + +|`tools/proof-toolchain/DESIGN.adoc` +|One relocatable bundle at `/opt/hyperpolymath/provers`, `provers.sh +install\|doctor\|render` +|Design only. Its statements about what agent sessions can reach were not +measured and are partly contradicted by <>. + +|`tools/workstation/env.sh` +|Toolchain homes and `PATH` for one workstation +|Hand-maintained; nothing records versions; not rendered from a manifest. + +|`.devcontainer/`, `container/`, `build/guix.scm` +|Template scaffolding with 30 unfilled tokens +|None of them name a single prover. They are three more hand-written +projections of an environment that is declared nowhere. + +|`.machine_readable/integrations/groove.a2ml` +|BoJ/Groove service manifest +|`capabilities` is empty, so a BoJ server cannot learn which provers an +environment offers. + +|`build/just/proofs.just` +|`proof-check-*` recipes +|Each recipe probes a binary with `command -v`; a missing prover is a SKIP +that reads like a pass. PROOF-POLICY §6 says a leg that cannot run must say +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). HEAD or GET to the root of each host; the code is what the +proxy returned. + +[cols="3,1,3",options="header"] +|=== +|Host |HTTP |Reading + +|`opam.ocaml.org` |200 |Reachable. DESIGN.adoc assumes sessions cannot reach it. +|`alire.ada.dev` |200 |Reachable. Same assumption contradicted. +|`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. +|`ftp.gnu.org/gnu/guix` |200 |Reachable. +|`smt-lib.org`, `www.tptp.org` |200 |Reachable. +|`github.com/Z3Prover/z3/releases/latest` |403 |*Refused by the proxy.* DESIGN.adoc assumes release assets are the one thing every session can fetch. +|`api.github.com/repos/cvc5/cvc5/releases/latest` |403 |Refused. Release discovery through the API is not available here. +|`crates.io/api/v1/crates/just` |403 |Refused (cargo installs from the registry would fail). +|`ghcr.io/v2/`, `cgr.dev/v2/` |401 |Registry answered; anonymous token flow not tested. +|`www.cs.utexas.edu/~moore/acl2/` |TLS failure |Host certificate not in the session CA bundle. +|=== + +A second experiment, installing Z3 from a GitHub release asset into a +scratch prefix and running `z3 --version`, was *refused by the session's +execution policy* before any bytes moved: downloading and executing an +external binary is denied in this session class. + +Two conclusions follow, and both change the design: + +. *Reachability is a property of an environment instance, not of its + class.* The same "agent session" class reached opam here and could not + reach GitHub releases. The kit must measure, not assume: `doctor` grows a + `probe` that records which hosts answered, and the capability report + carries it. +. *Execution policy is a second axis beside network policy.* An + environment may be able to fetch a bundle and still be forbidden to run + it. The environment declaration needs an `execute-downloaded` field, and + the install step needs a fallback that does not execute fetched binaries + (a Guix profile, a prebuilt image, or declining the leg honestly). + +== The proposal + +Six enhancements, in build order. Each stands on its own; later ones consume +earlier ones. + +=== E1. Declare the environments + +Add `tools/environments/environments.kyaml`, one entry per environment +class, in the same KYAML style as the toolchain manifest: identity, how +tools get in (bundle, Guix, mise, image), the prefix, whether fetched +binaries may run, which container runtime exists, who consumes the +capability report, and a `measured` block that `probe` fills in. A first +cut is committed with this proposal. + +=== E2. One capability report, one producer, one consumer contract + +`provers.sh doctor --json` becomes the single producer of an +*environment capability record*: the environment id, the toolchain lock +hash, each tool as `PRESENT `, `DRIFT`, or `UNAVAILABLE `, +and the probe results. One JCS-canonical I-JSON object, as DESIGN.adoc +already specifies, with the environment fields added. + +Its consumers are already named across the estate: echidna and echidnabot +(which `ProverKind` backends a host can serve), proof-burrower (whether +`echidna prove` has a prover to talk to), the BoJ server (Groove +`capabilities`), and `proof-check-*` (a leg that is `UNAVAILABLE` is +reported, never skipped). Each consumer reads the same record, so the +answer to "which provers does this environment have" is computed once. + +=== E3. Render every projection from the two manifests + +`provers.sh render` already regenerates the workstation index from the +toolchain manifest. Extend it to render, per environment class, the files +that are hand-written today: the `env.sh` `PATH` entries, the Guix +`manifest.scm` subset, the devcontainer feature list, a CI job-matrix +fragment, and the session setup-script snippet. The rule is the one the +design already states: what a machine *has* is `doctor`'s job; what a +machine *should have* is rendered, never hand-edited. + +=== E4. The agent-session leg + +Cloud sessions are the environment class the estate controls least and uses +most. Add a session-start hook under `.claude/` that runs `provers.sh +install` where policy allows and `provers.sh doctor --json` always, writing +the capability record to `.session/`. A session that cannot install says so +in the record, which PROOF-POLICY §6 requires, instead of a `SKIP` in a +recipe. The install step honours `execute-downloaded` from E1. + +=== E5. Register capabilities with the BoJ server + +Fill `capabilities` in `groove.a2ml` from the capability record at +registration time, so a remote caller sees which provers an environment +offers before dispatching to it. This is the "register" verb the README +promises and the first concrete BoJ integration surface (roadmap M2). + +=== E6. Close the gap to echidna's core roster + +The kit covers the PROOF-POLICY provers. echidna's default API exposes a +core of 12 backends; the kit's manifest lacks 5 of them. Add HOL Light, +HOL4, ACL2 and Mizar as `exception:recorded` entries (PVS is a licensed +binary and goes in the sealed-container tail), so an environment the kit +provisions can serve echidna's whole core. The extended roster (141 +`ProverKind` variants over 105 implementation files) stays echidna's +sealed-container concern, per the 2026-05-18 packaging ruling. + +[[coverage]] +=== Coverage of echidna's core 12 by the toolchain manifest + +[cols="1,1,2",options="header"] +|=== +|echidna core backend |Manifest entry |Status + +|Agda |`agda-2.6.3`, `agda-2.6.4.3` |Covered +|Coq (Rocq) |`rocq` |Covered +|Lean 4 |`lean` |Covered (no Mathlib, per policy) +|Isabelle/HOL |`isabelle` |Covered (supplementary role) +|Z3 |`z3` |Covered +|CVC5 |`cvc5` |Covered +|Metamath |none needed |Pure-Rust, in-process in echidna +|HOL Light |none |*Missing* (OCaml; opam reachable here) +|HOL4 |none |*Missing* (Poly/ML) +|ACL2 |none |*Missing* (SBCL; upstream host failed TLS here) +|Mizar |none |*Missing* (binary release) +|PVS |none |*Missing*, licensed binary: sealed-container tail +|=== + +== Options compared + +[cols="1,3,1,1,1",options="header"] +|=== +|Option |Shape |Elegance / correctness |Dependability |Security / privacy + +|*A. Two manifests, one record* (recommended; E1–E6) +|Environments and tools declared once; every projection rendered; one +capability record consumed everywhere. +|High. One source of truth; drift becomes impossible by construction rather +than by review. +|High once built. Measured, not assumed; degrades to an honest +`UNAVAILABLE`. +|High. Lock hashes every input; no telemetry; registration is opt-in by +`BOJ_SERVER_URL`. + +|*B. Guix everywhere* +|Each environment is a Guix profile from `manifest.scm`. +|High where it applies; Guix is already the primary packager. +|Low for the tail: Guix does not carry Idris2, Creusot, agda2dedukti or the +licensed provers, and no agent session here can run `guix`. +|High (reproducible by hash). + +|*C. Containers everywhere* +|Every environment is a Wolfi image; sessions and CI pull it. +|Medium. Clean, but a container is an opaque projection; drift hides inside +it. +|Medium. Agent sessions cannot run a container engine; CI can. +|High (sealed, signed with cerro-torre). + +|*D. Alternative path: one OCI artifact as the transport* +|Publish the bundle tree as an OCI artifact (ORAS) and let every target +unpack it without a runtime: tarball and image stop being two artefacts. +|High. Removes the "asset first, image second" split in DESIGN.adoc. +|Unknown here: `ghcr.io` and `cgr.dev` answered 401 and the anonymous token +flow was not tested. Worth one experiment (X3). +|High (content-addressed, signable with cosign). +|=== + +Recommendation: build A, and run X3 before deciding whether D replaces A's +two-artefact transport. B remains the preferred *installer* inside A on +hosts that have Guix; C remains A's escape hatch for the tail. + +== Experiments before building + +Each experiment has a pass criterion so the result is a fact, not an +impression. + +[cols="1,3,2",options="header"] +|=== +|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. +The design's host assumptions are replaced by measurements. + +|X2 +|Install Z3 and CVC5 from release assets into the fixed prefix on a +GitHub-hosted runner and on the workstation; run the manifest `verify` +command for each. +|Both report `PRESENT` at the locked version from the same bytes; the +bundle's SHA-256 matches on both hosts. + +|X3 +|Push the same tree as an OCI artifact with ORAS to `ghcr.io`; pull it +anonymously from a session and from a runner without a container engine. +|Anonymous pull succeeds in both, or the 401 is shown to need a token, in +which case D is rejected for sessions. + +|X4 +|Build the bundle in a builder image with glibc 2.35 and run `doctor` on +Ubuntu 22.04, Ubuntu 24.04 (glibc 2.39, measured here) and Wolfi. +|`doctor` passes on all three. If it does not, the lock's glibc floor is +raised and the unsupported target is named. + +|X5 +|Give `proof-check-*` a planted missing prover and a planted broken proof. +|The missing prover yields `UNAVAILABLE` in the record and a non-zero exit +where PROOF-POLICY §6 requires it; the broken proof fails. Both directions +verified, as LANGUAGE-POLICY §3 asks of any gate. +|=== + +== The formal route + +PROOF-POLICY §1 maps interface contracts to Idris2. The capability record +*is* an interface: several languages produce or consume it (shell here, Rust +in echidna and proof-burrower, the BoJ cartridge). So the record gets an +Idris2 type under `verification/proofs/idris2/` with the properties that +matter to its consumers: the status vocabulary is closed (`PRESENT`, +`DRIFT`, `UNAVAILABLE`), encoding to I-JSON and back is a round trip, and +the record is total over the manifest (every manifest entry appears exactly +once). That replaces the template's ABI-1..5 placeholders with proofs about +something this repository actually ships, which is what roadmap M4 asks for. + +The closure rule in DESIGN.adoc ("the bundle is complete only if nothing a +tool needs at run time comes from the host") is a statement about the +`needs` graph in the manifest: every edge's target is itself an entry, and +the graph is acyclic. That is a small, implementation-independent theorem +and belongs in Agda under the policy; until it exists, a test that walks the +graph is the `TESTED` stand-in and is recorded as such. + +== Aspects + +Security:: The lock records SHA-256 of every input. echidna's solver +integrity manifest (`config/solver-manifest.toml`) wants SHAKE3-512 and +currently ships `PLACEHOLDER_COMPUTE_ON_FIRST_RUN` for every solver, which +is trust-on-first-use and defeats the check. The lock should carry both +digests so echidna can verify kit-installed binaries against a value that +was computed where the bytes were built, not where they were first run. +Observability:: One record, one schema, one producer; consumers add nothing +of their own. BoJ registration is the only place the record leaves the +host. +Privacy:: No telemetry. Registration happens only when `BOJ_SERVER_URL` +is set, and the record contains tool versions and probe results, never +paths under `$HOME` or user identity. +Reproducibility:: Guix stays primary; the bundle is pinned in the lock; +`rustup` and `elan` are set never to fetch on demand. +Portability:: The measured glibc here is 2.39. Picking the builder floor +at 2.35 covers Ubuntu 22.04 runners as well; X4 decides. +Honesty:: Every leg that cannot run is reported, with the reason. This is +the one behaviour that must hold in every environment class. + +== Beyond this repository + +Things this proposal touches that live elsewhere, so they can be tracked +rather than lost: + +* `hyperpolymath/standards` PROOF-POLICY §6 names the Guix manifest, the + container and the setup script as the three toolchain routes. Once E2 + exists it should name the capability record as the thing each route must + produce. +* `hyperpolymath/echidna`: read the capability record instead of probing + binaries; add the SHA-256 column to `solver-manifest.toml` and drop the + first-run placeholders; `provers.a2ml` carries only a slug per backend, + so the binary each backend needs is not machine-readable anywhere. +* `hyperpolymath/echidnabot` README still says "12 provers" against + echidna's 141 variants; the capability record would let it say what the + host has instead of a number. +* `hyperpolymath/proof-burrower` `docs/ECHIDNA-INTEGRATION.adoc` can cite + the record for "is Isabelle here". +* `hyperpolymath/rsr-template-repo`: the `proof-check-*` recipes that `SKIP` + on a missing prover are inherited by every repo; the fix belongs in the + template. +* The BoJ server's `ssg-mcp` cartridge needs a field for the record. + +== Decisions needed + +. Whether the agent-session install step may execute fetched binaries at + all, given the policy measured here. If not, the session leg is + `doctor`-only and the session's provers come from a prebuilt image or + from a mise/Guix path the platform allows. +. Whether HOL Light, HOL4, ACL2 and Mizar join the manifest now (E6) or + wait for an echidna consumer that needs them. +. Whether X3 runs before the first bundle release, so the transport is + chosen once. diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc new file mode 100644 index 0000000..7309661 --- /dev/null +++ b/tools/environments/README.adoc @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Environments: what the kit provisions, and what each can reach + +The proof toolchain manifest (`../proof-toolchain/toolchain.kyaml`) says +*which tools* the estate uses. This directory says *which environments* +those tools are projected onto, and records what each environment was +measured to reach. Design: `docs/proposals/environment-of-environments.adoc`. + +[cols="1,3",options="header"] +|=== +|File |What it is + +|`environments.kyaml` +|One entry per environment class (workstation, agent session, CI runner, +devcontainer, Guix shell, sealed container, BoJ-registered view): how tools +get in, whether fetched binaries may run, which container runtime exists, +who reads its capability record, and a `measured` block. + +|`probe-reachability.sh` +|Sends one HEAD request per URL in `hosts.txt` and prints the HTTP status +this environment saw, as text or as one JSON object. Downloads nothing, +executes nothing. Its output is what goes into an entry's `measured` block, +with the date. + +|`hosts.txt` +|The hosts the toolchain manifest's `method` column fetches from. +|=== + +== Reading a `measured` block + +`reachable` means a HEAD request returned 2xx or 3xx. `refused` is a 403 +from the environment's proxy. `auth-required` is a 401: the host answered +and wants a token, which the probe does not supply. `tls-failed` means the +host's certificate is not in the environment's CA bundle. Container +registries answer `405` to a HEAD on `/v2/` and `401` to a GET; the probe +reports the HEAD result as `http-405`, which means "the registry answered". +`execute-downloaded: false` under `measured` means the environment's policy +refused to run a fetched binary when that was tried; it is recorded only +when it was actually tried. + +A block is a fact about one environment instance on one date. It is never +copied from one environment class to another. diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml new file mode 100644 index 0000000..6baef89 --- /dev/null +++ b/tools/environments/environments.kyaml @@ -0,0 +1,32 @@ +# SPDX-License-Identifier: MPL-2.0 +# Environment manifest: the classes of environment the kit provisions and +# makes report their capabilities (docs/proposals/environment-of-environments.adoc, +# enhancement E1). Hand-edited, except each entry's `measured` block, which +# tools/environments/probe-reachability.sh fills in and dates. +# +# Fields: +# id stable name used in the capability record +# kind host | cloud-session | ci-runner | container | guix-shell | remote +# installs how tools get in, in order of preference: +# guix | mise | bundle (provers.sh install) | image | none +# prefix where the toolchain bundle unpacks ($PREFIX in toolchain.kyaml) +# execute-downloaded may this environment run a binary it fetched? true | false | +# policy (decided per instance; the probe records what it found) +# container-runtime podman | docker | none +# report who reads this environment's capability record +# measured dated facts from a probe run; never typed by hand +{ + schema: 1, + policy: "standards 3-practice/PROOF-POLICY.adoc §6; 3-practice/provisioning/PROVISIONING-STANDARD.adoc", + toolchain: "../proof-toolchain/toolchain.kyaml", + record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, + environments: [ + {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", reachable: ["opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com (releases)", "api.github.com", "crates.io"], auth-required: ["ghcr.io", "cgr.dev"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: false}}, + {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, + {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, + {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, + {id: "sealed-container", kind: "container", installs: ["image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "podman", report: ["echidna dispatcher"], notes: "echidna .containerization/Containerfile.wave3 pattern; licensed or not-in-Guix provers live here", measured: {}}, + {id: "boj-registered", kind: "remote", installs: ["none"], prefix: "", execute-downloaded: false, container-runtime: "none", report: ["boj-server"], notes: "not an environment the kit provisions: the view a BoJ server holds of any of the above after registration (groove.a2ml capabilities)", measured: {}}, + ], +} diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt new file mode 100644 index 0000000..3e804da --- /dev/null +++ b/tools/environments/hosts.txt @@ -0,0 +1,33 @@ +# Hosts the proof toolchain is fetched from (tools/proof-toolchain/toolchain.kyaml +# `method` column), one URL per line. '#' starts a comment. +# Probed by probe-reachability.sh with HEAD requests only. + +# Release assets and source archives +https://github.com/Z3Prover/z3/releases/latest +https://api.github.com/repos/cvc5/cvc5/releases/latest +https://codeload.github.com/hyperpolymath/bofj-kitt/tar.gz/main +https://raw.githubusercontent.com/hyperpolymath/bofj-kitt/main/README.adoc + +# Package registries the manifest's methods use +https://opam.ocaml.org/ +https://alire.ada.dev/ +https://hackage.haskell.org/ +https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init +https://crates.io/api/v1/crates/just +https://releases.lean-lang.org/ +https://ftp.gnu.org/gnu/guix/ + +# Prover homes with their own downloads +https://isabelle.in.tum.de/ +https://mizar.uwb.edu.pl/ +https://pvs.csl.sri.com/ +https://www.cs.utexas.edu/~moore/acl2/ +https://cvc5.github.io/ + +# Container registries (401 means the registry answered and wants a token) +https://ghcr.io/v2/ +https://cgr.dev/v2/ + +# Standards bodies for the exchange formats +https://smt-lib.org/ +https://www.tptp.org/ diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh new file mode 100755 index 0000000..f452566 --- /dev/null +++ b/tools/environments/probe-reachability.sh @@ -0,0 +1,94 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# probe-reachability.sh — measure which toolchain hosts this environment can +# reach (experiment X1 in docs/proposals/environment-of-environments.adoc). +# +# Sends one HEAD request per host and prints the HTTP status the environment +# saw. It downloads nothing and executes nothing it fetched. The result is a +# fact about THIS environment instance on THIS date; copy it into the +# matching `measured` block of environments.kyaml rather than assuming it +# holds elsewhere. +# +# Usage: +# tools/environments/probe-reachability.sh # text table +# tools/environments/probe-reachability.sh --json # one JSON object +# HOSTS_FILE=my-hosts.txt tools/environments/probe-reachability.sh +# +# Exit code is 0 whenever the probe ran; reachability is reported, not +# judged. Exit 2 when curl is missing or the hosts file cannot be read. + +set -euo pipefail + +HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +HOSTS_FILE="${HOSTS_FILE:-$HERE/hosts.txt}" +TIMEOUT="${PROBE_TIMEOUT:-15}" +MODE="text" +if [ "${1:-}" = "--json" ]; then + MODE="json" +fi + +if ! command -v curl >/dev/null 2>&1; then + echo "probe-reachability: curl is not on PATH" >&2 + exit 2 +fi +if [ ! -r "$HOSTS_FILE" ]; then + echo "probe-reachability: cannot read hosts file $HOSTS_FILE" >&2 + exit 2 +fi + +# classify — one word per outcome. +classify() { + local code="$1" rc="$2" + if [ "$rc" -eq 60 ]; then + echo "tls-failed" + elif [ "$rc" -ne 0 ] || [ "$code" = "000" ]; then + echo "unreachable" + elif [ "$code" = "401" ]; then + echo "auth-required" + elif [ "$code" = "403" ]; then + echo "refused" + elif [ "${code:0:1}" = "2" ] || [ "${code:0:1}" = "3" ]; then + echo "reachable" + else + echo "http-$code" + fi +} + +date_utc="$(date -u +%Y-%m-%dT%H:%M:%SZ)" +platform="$(uname -s)/$(uname -m)" +if command -v ldd >/dev/null 2>&1; then + # awk reads all of ldd's output, so no SIGPIPE under pipefail. + platform="$platform glibc $(ldd --version 2>/dev/null | awk 'NR==1{print $NF}')" +fi + +if [ "$MODE" = "text" ]; then + printf 'probe-reachability %s (%s)\n' "$date_utc" "$platform" + printf '%-6s %-14s %s\n' "HTTP" "OUTCOME" "URL" +fi + +rows=() +while IFS= read -r line; do + line="${line%%#*}" + line="${line#"${line%%[![:space:]]*}"}" + line="${line%"${line##*[![:space:]]}"}" + [ -z "$line" ] && continue + rc=0 + code="$(curl -sS -I -o /dev/null -w '%{http_code}' --max-time "$TIMEOUT" "$line" 2>/dev/null)" || rc=$? + outcome="$(classify "$code" "$rc")" + if [ "$MODE" = "text" ]; then + printf '%-6s %-14s %s\n' "$code" "$outcome" "$line" + else + rows+=("$(printf '{"url":"%s","http":"%s","outcome":"%s"}' "$line" "$code" "$outcome")") + fi +done < "$HOSTS_FILE" + +if [ "$MODE" = "json" ]; then + joined="" + for r in "${rows[@]}"; do + if [ -z "$joined" ]; then joined="$r"; else joined="$joined,$r"; fi + done + printf '{"probe":"reachability","date":"%s","platform":"%s","hosts":[%s]}\n' \ + "$date_utc" "$platform" "$joined" +fi diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index 771f546..409d882 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -12,6 +12,14 @@ which of them it has. Status: design, not built. Nothing here installs anything yet; the build steps are in <>. +See also `../environments/` and +`docs/proposals/environment-of-environments.adoc`: the environment classes +this toolchain is projected onto, with measured reachability. Those +measurements (2026-10-27) contradict two assumptions below: the agent +session probed there *could* reach `opam.ocaml.org` and `alire.ada.dev`, +and *could not* fetch GitHub release assets. Reachability is measured per +environment, not assumed per class. + == The problem it solves The same tools are installed four different ways today, and each way fails From 4d97441ec6b4ee9fc45f39fd1f5180e753efd8ee Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 09:21:23 +0000 Subject: [PATCH 02/16] fix(environments): measure the release-asset path, record every probed host, and correct the priority-1 count Review findings on #98, each verified before changing anything: - The reachability claim was drawn from a release landing page and the API, not from an asset. hosts.txt now carries a concrete Z3 asset URL and the probe follows redirects: the asset answers 302 to release-assets.githubusercontent.com and then 200, so a concrete release asset is fetchable from this session. Only the landing page and api.github.com are refused. The proposal's measured table, its first conclusion and the DESIGN.adoc pointer now say so: the asset transport holds, and what cannot run from a session is `pin: resolve` discovery, so install must read the asset URL from the lock. - environments.kyaml records every URL in hosts.txt (21), and execute-downloaded is `denied-before-download` with a note, because running a fetched binary was never observed. The README defines the three values and separates registry 401/405 from the token flow. - The probe loop accepts a final line with no trailing newline. - The awesome-lists proposal says eleven priority-1 lists (the table's count), and its coverage property distinguishes one owning list per tool from cross-references. - STATE.a2ml last-updated set to 2026-10-27. Validated: asciidoctor --failure-level WARN on every touched .adoc, yq on the manifest, bash -n and a live probe run (21 hosts; asset 200), check-no-md-in-docs passes. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .machine_readable/6a2/STATE.a2ml | 2 +- .../awesome-estate-maths-proving.adoc | 23 +++++++----- .../environment-of-environments.adoc | 35 ++++++++++++------- tools/environments/README.adoc | 22 ++++++++---- tools/environments/environments.kyaml | 2 +- tools/environments/hosts.txt | 7 +++- tools/environments/probe-reachability.sh | 7 ++-- tools/proof-toolchain/DESIGN.adoc | 11 +++--- 8 files changed, 73 insertions(+), 36 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 9acf9b4..a59aca4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -8,7 +8,7 @@ [metadata] project = "bofj-kitt" version = "0.3.0" -last-updated = "2026-07-16" +last-updated = "2026-10-27" status = "active" # active | paused | archived [project-context] diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc index bccfd75..1c9763d 100644 --- a/docs/proposals/awesome-estate-maths-proving.adoc +++ b/docs/proposals/awesome-estate-maths-proving.adoc @@ -237,7 +237,7 @@ diagrams. |3 |=== -Twenty-one lists; thirteen at priority 1, which together name every one of +Twenty-one lists; eleven at priority 1, which together name every one of echidna's 12 core backends and every PROOF-POLICY route. === Where the small families go @@ -343,7 +343,7 @@ shell script over `yq` and `jq`. Recommendation: A for the repositories, with D as the way their tool tables are produced once the registry fields exist in echidna. Start with -the thirteen priority-1 lists; hand-curate their prose; render their tool +the eleven priority-1 lists; hand-curate their prose; render their tool tables as soon as `provers.a2ml` carries the fields. == Experiments before the first batch @@ -378,12 +378,17 @@ other lists use. == The formal route The lists are data about tools, and the one property worth stating -formally is *coverage*: every variant of `ProverKind` is named by exactly -one priority-1 or priority-2 list, and every tool the kit manifest names -is in a list. With the registry of option D that is a finite relation and -the check is a test (`TESTED`), the same kind of check `awesome-nickel` -already runs in Idris2 over its links. It is not worth a theorem; it is -worth a gate. +formally is *coverage*. Each tool has one *owning* list, the entry that +carries its description; any other list may mention it as a +cross-reference (Z3 in `awesome-constraint-solving` for its optimiser, +Sledgehammer in `awesome-atp`, TPTP in `awesome-logical-frameworks`). The +property is then: every variant of `ProverKind` has exactly one owning +entry across the priority-1 and priority-2 lists, cross-references are +unlimited but must point at the owner, and every tool the kit manifest +names has an owner. With the registry of option D (an `owner` field per +tool) that is a finite relation and the check is a test (`TESTED`), the +same kind of check `awesome-nickel` already runs in Idris2 over its links. +It is not worth a theorem; it is worth a gate. == Aspects @@ -422,7 +427,7 @@ twenty-one more lists inherit the wrong obligations. [[decisions]] == Decisions needed -. Confirm option A and the thirteen priority-1 lists as the first batch, +. Confirm option A and the eleven priority-1 lists as the first batch, or trim. . Confirm `stuff-of-awe` as the organisation for all of them (the estate board still lists the existing lists under `hyperpolymath/`). diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index 5656d33..c597d10 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/docs/proposals/environment-of-environments.adoc @@ -42,7 +42,8 @@ backends; covers 7 of echidna's 12 core backends (see <>). |One relocatable bundle at `/opt/hyperpolymath/provers`, `provers.sh install\|doctor\|render` |Design only. Its statements about what agent sessions can reach were not -measured and are partly contradicted by <>. +measured; <> confirms the asset transport and contradicts the +opam and Alire claim. |`tools/workstation/env.sh` |Toolchain homes and `PATH` for one workstation @@ -85,25 +86,35 @@ proxy returned. |`isabelle.in.tum.de`, `mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable. |`ftp.gnu.org/gnu/guix` |200 |Reachable. |`smt-lib.org`, `www.tptp.org` |200 |Reachable. -|`github.com/Z3Prover/z3/releases/latest` |403 |*Refused by the proxy.* DESIGN.adoc assumes release assets are the one thing every session can fetch. -|`api.github.com/repos/cvc5/cvc5/releases/latest` |403 |Refused. Release discovery through the API is not available here. +|`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 |*Reachable.* The asset download path redirects to `release-assets.githubusercontent.com` and the bytes are served. DESIGN.adoc's "release asset first" transport holds here. +|`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files). +|`github.com/Z3Prover/z3/releases/latest` |403 |*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 |Refused. Release discovery through the API is not available either. |`crates.io/api/v1/crates/just` |403 |Refused (cargo installs from the registry would fail). -|`ghcr.io/v2/`, `cgr.dev/v2/` |401 |Registry answered; anonymous token flow not tested. +|`ghcr.io/v2/`, `cgr.dev/v2/` |401 (GET), 405 (HEAD) |Registry answered; anonymous token flow not tested. +|`cvc5.github.io` |200 |Reachable. |`www.cs.utexas.edu/~moore/acl2/` |TLS failure |Host certificate not in the session CA bundle. |=== -A second experiment, installing Z3 from a GitHub release asset into a -scratch prefix and running `z3 --version`, was *refused by the session's -execution policy* before any bytes moved: downloading and executing an -external binary is denied in this session class. +A second experiment, installing Z3 from that release asset into a scratch +prefix and running `z3 --version`, was *refused by the session's execution +policy* before any bytes moved: a step that downloads and executes an +external binary is denied in this session class. Whether a fetched binary +would run was therefore not observed; the manifest records +`denied-before-download`, not `false`. Two conclusions follow, and both change the design: . *Reachability is a property of an environment instance, not of its - class.* The same "agent session" class reached opam here and could not - reach GitHub releases. The kit must measure, not assume: `doctor` grows a - `probe` that records which hosts answered, and the capability report - carries it. + class, and of a path, not of a host.* The same "agent session" class + reached opam here, which the design assumed it could not; it fetched a + concrete release asset, which the design assumed and which holds; and it + could not reach the release landing page or the API, so a `pin: + resolve` entry (which discovers "latest" through the API) cannot be + resolved from a session. The lock must carry the concrete asset URL, + and `install` must read the lock, never the API. The kit must measure, + not assume: `doctor` grows a `probe` that records which paths answered, + and the capability report carries it. . *Execution policy is a second axis beside network policy.* An environment may be able to fetch a bundle and still be forbidden to run it. The environment declaration needs an `execute-downloaded` field, and diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index 7309661..18b0646 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -31,12 +31,22 @@ with the date. `reachable` means a HEAD request returned 2xx or 3xx. `refused` is a 403 from the environment's proxy. `auth-required` is a 401: the host answered and wants a token, which the probe does not supply. `tls-failed` means the -host's certificate is not in the environment's CA bundle. Container -registries answer `405` to a HEAD on `/v2/` and `401` to a GET; the probe -reports the HEAD result as `http-405`, which means "the registry answered". -`execute-downloaded: false` under `measured` means the environment's policy -refused to run a fetched binary when that was tried; it is recorded only -when it was actually tried. +host's certificate is not in the environment's CA bundle. A container +registry's `/v2/` endpoint may answer `401` (wants a token) or `405` +(method not allowed for HEAD); both mean the registry answered, and +neither says whether an anonymous token flow would succeed. The manifest +records such hosts under `registry-answered` with the codes seen. + +`execute-downloaded` under `measured` takes one of three values: +`true` (a fetched binary was run), `false` (a fetched binary was present +and the environment refused to run it), or `denied-before-download` (the +attempt was stopped before any bytes moved, so running was never +observed). It is recorded only when an attempt was actually made. + +A probe of a GitHub release *landing page* or of `api.github.com` says +nothing about release *assets*: the asset download path redirects to +`release-assets.githubusercontent.com`, which the probe follows +separately. Record the asset outcome, not the landing page's. A block is a fact about one environment instance on one date. It is never copied from one environment class to another. diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml index 6baef89..d71fccf 100644 --- a/tools/environments/environments.kyaml +++ b/tools/environments/environments.kyaml @@ -22,7 +22,7 @@ record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, environments: [ {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, - {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", reachable: ["opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com (releases)", "api.github.com", "crates.io"], auth-required: ["ghcr.io", "cgr.dev"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: false}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (22 URLs, every one probed)", reachable: ["github.com release asset download (302 to release-assets.githubusercontent.com, then 200)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest)", "api.github.com", "crates.io"], registry-answered: ["ghcr.io (GET 401, HEAD 405)", "cgr.dev (GET 401, HEAD 405)"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed"}}, {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt index 3e804da..3a6f7a6 100644 --- a/tools/environments/hosts.txt +++ b/tools/environments/hosts.txt @@ -2,9 +2,14 @@ # `method` column), one URL per line. '#' starts a comment. # Probed by probe-reachability.sh with HEAD requests only. -# Release assets and source archives +# Release assets and source archives. The asset download URL is the path +# `provers.sh install` would use; the landing page and the API are discovery +# only, so a result on them says nothing about assets. https://github.com/Z3Prover/z3/releases/latest https://api.github.com/repos/cvc5/cvc5/releases/latest +https://github.com/Z3Prover/z3/releases/download/z3-4.13.4/z3-4.13.4-x64-glibc-2.35.zip +# The asset above redirects to release-assets.githubusercontent.com; the +# probe follows redirects, so one line measures the whole download path. https://codeload.github.com/hyperpolymath/bofj-kitt/tar.gz/main https://raw.githubusercontent.com/hyperpolymath/bofj-kitt/main/README.adoc diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index f452566..9332c2c 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -69,13 +69,16 @@ if [ "$MODE" = "text" ]; then fi rows=() -while IFS= read -r line; do +# `|| [ -n "$line" ]` keeps a final line that has no trailing newline. +while IFS= read -r line || [ -n "$line" ]; do line="${line%%#*}" line="${line#"${line%%[![:space:]]*}"}" line="${line%"${line##*[![:space:]]}"}" [ -z "$line" ] && continue rc=0 - code="$(curl -sS -I -o /dev/null -w '%{http_code}' --max-time "$TIMEOUT" "$line" 2>/dev/null)" || rc=$? + # -L follows redirects so a release asset is measured at its final + # host, not at the 302 GitHub answers with; the code is the last one. + code="$(curl -sS -I -L -o /dev/null -w '%{http_code}' --max-time "$TIMEOUT" "$line" 2>/dev/null)" || rc=$? outcome="$(classify "$code" "$rc")" if [ "$MODE" = "text" ]; then printf '%-6s %-14s %s\n' "$code" "$outcome" "$line" diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index 409d882..2f99c00 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -15,10 +15,13 @@ steps are in <>. See also `../environments/` and `docs/proposals/environment-of-environments.adoc`: the environment classes this toolchain is projected onto, with measured reachability. Those -measurements (2026-10-27) contradict two assumptions below: the agent -session probed there *could* reach `opam.ocaml.org` and `alire.ada.dev`, -and *could not* fetch GitHub release assets. Reachability is measured per -environment, not assumed per class. +measurements (2026-10-27) refine the assumptions below: the agent session +probed there *could* reach `opam.ocaml.org` and `alire.ada.dev`; it +*could* fetch a concrete GitHub release asset, as assumed; and it *could +not* reach release landing pages or `api.github.com`, so a `pin: +resolve` entry cannot be resolved from a session and `install` must read +the concrete asset URL from the lock. Reachability is measured per +environment and per path, not assumed per class. == The problem it solves From f72449c70a04953a1646409283cd9402f719b4cb Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 09:26:11 +0000 Subject: [PATCH 03/16] docs(proposals): BoJ cartridges for proving, solving and code verification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Third proposal, from the owner's ask for a BoJ cartridge that gives agents access to the estate's provers and solvers from the store. What exists was read first: the store's proof-mcp (eight lifecycle tools, seven hand-typed backends, a Zig adapter that answers "forwarded" and a mod.js that posts to a port nothing serves), echidna-llm-mcp, proof-lsp, toolchain-mcp, echidna's own crates/echidna-mcp (three tools, standalone, which ADR-0002 rules out as a front door), and the live bridge (rest-unavailable, stdio-only). Proposed: three cartridges cut by input kind and answer kind, on one seam, the capability record from the environment-of-environments proposal: provers-mcp (verdict + trust level + certificate), solvers-mcp (model, unsat proof, optimum, bounded check), and code-verifiers-mcp (a PROOF-POLICY §5 ledger with receipt; the home for Creusot, Kani, Aeneas, SPARK and the arriving Quintessence, Apodeixis.jl, atoma and bactarin). proof-mcp stays as the lifecycle layer and composes provers-mcp under ADR-0014. Options A-D rated; experiments Z1-Z6 with pass criteria; the Idris2 and Agda routes named; decisions listed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .machine_readable/6a2/STATE.a2ml | 2 +- CHANGELOG.adoc | 4 + .../boj-prover-solver-cartridges.adoc | 384 ++++++++++++++++++ 3 files changed, 389 insertions(+), 1 deletion(-) create mode 100644 docs/proposals/boj-prover-solver-cartridges.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a59aca4..ea7b206 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -39,7 +39,7 @@ actions = [ "M1 — fill the remaining ~75 placeholder-token files (container/, .devcontainer/, .github/*)", "M1 — restore a full SECURITY policy once PGP material exists", "M2 — specify the kit's first capability and its BoJ integration contract", - "M2 — decide the proposals in docs/proposals/environment-of-environments.adoc (E1–E6, X1–X5) and docs/proposals/awesome-estate-maths-proving.adoc", + "M2 — decide the proposals in docs/proposals/environment-of-environments.adoc (E1–E6, X1–X5), docs/proposals/awesome-estate-maths-proving.adoc and docs/proposals/boj-prover-solver-cartridges.adoc (Z1–Z6)", ] [maintenance-status] diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ea426c7..b3ff2e0 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -19,6 +19,10 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. * `docs/proposals/awesome-estate-maths-proving.adoc` — the awesome lists to create in `stuff-of-awe` for maths, proving and solving, derived from echidna's prover roster, and the tools echidna itself lacks. +* `docs/proposals/boj-prover-solver-cartridges.adoc` — three BoJ cartridges + (`provers-mcp`, `solvers-mcp`, `code-verifiers-mcp`) on the capability + record seam, what the store's `proof-mcp` becomes, and where + Quintessence, Apodeixis.jl, atoma and bactarin land. * `tools/environments/` — `environments.kyaml` (environment classes with a `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment X1: HEAD-only reachability probe). diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc new file mode 100644 index 0000000..0db194d --- /dev/null +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -0,0 +1,384 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += BoJ cartridges for proving, solving and code verification +:toc: +:toclevels: 3 +:sectnums: + +Status: proposal, 2026-10-27. Companion to +`environment-of-environments.adoc` (the capability record these cartridges +advertise from) and `awesome-estate-maths-proving.adoc` (the roster they +expose). The store state below was read from `hyperpolymath/boj-server-cartridges` +and the BoJ stdio bridge on that date. + +== The gap, confirmed + +Nothing public gives an agent MCP access to a *roster* of provers and +solvers. What exists upstream is per-tool: a Lean language-server MCP, a +handful of single-solver wrappers. The estate is the only place with a +141-variant dispatcher (echidna), a declared toolchain (this kit), and a +cartridge store with a formal-verification domain. The pieces exist; they +are not joined. + +[cols="2,3,2",options="header"] +|=== +|Surface |What it does today |Why it is not the answer + +|`proof-mcp` (store, `domains/formal-verification`) +|Eight session-lifecycle tools over a state machine (idle, loading, +verifying, verified, failed) for seven backends: Lean, Coq, Agda, Isabelle, +Idris2, Z3, CVC5. Idris2 ABI with proofs; Zig FFI and adapter. +|Its adapter answers every tool with `" forwarded"` and its `mod.js` +posts to a REST backend on port 7707 that nothing serves. The store lists +it as `available: true`, which is a catalogue claim, not a running prover. +Seven backends is a hand-typed list. + +|`echidna-llm-mcp` (store) +|Routes `consult` and `suggest_tactics` to an LLM. +|Advice, not proof. Opt-in by API key; must stay separate from anything +that returns a verdict. + +|`proof-lsp` (store) +|IDE integration: diagnostics, hover, completion for four assistants. +|Editor protocol, not dispatch. + +|`toolchain-mcp` (store, `domains/languages`) +|Mints and provisions LSP, DAP, BSP and language servers per workspace. +|Language toolchains, not provers; but its mint/provision/status shape is +the right model for provisioning a prover set from the kit's bundle. + +|`crates/echidna-mcp` (echidna repository) +|A standalone `rmcp` server with three tools: `prove` (file, prover, +timeout), `check_prover`, `list_provers`. Shells out to the `echidna` +binary. +|It is the right backend and the wrong front door: BoJ ADR-0002 rules out +standalone MCP servers in the estate, so this surface must enter BoJ as a +cartridge. Its tool descriptions also hard-code "105 provers", the +drift `PROVER_COUNT.adoc` warns against. + +|BoJ bridge (live) +|`boj_health` reports `rest-unavailable`, stdio-only, pending the Elixir +rewrite. Catalogue tools answer from a static manifest. +|Any cartridge built now must work through the stdio bridge and the +ADR-0006 `boj_cartridge_invoke` ABI, not through REST. +|=== + +== The proposal: three cartridges on one seam + +Three cartridges, cut by *what the input is and what the answer means*, +not by which binary runs. They share one seam: the capability record from +`environment-of-environments.adoc` (E2), which says what the host can +actually dispatch, so no cartridge ever advertises a tool it cannot run. + +=== `provers-mcp`: proving + +Input is a proof artefact (a `.agda`, `.v`, `.lean`, `.thy`, `.idr`, `.p`, +`.mm` file or a goal string); the answer is a verdict with a trust level +and, where the backend produces one, a certificate. + +[cols="1,3",options="header"] +|=== +|Tool |Contract + +|`provers_list` +|The provers this host can dispatch, read from the capability record +(`PRESENT` entries only), each with its echidna `ProverKind` slug, role +under PROOF-POLICY, version and lock hash. Never a hard-coded count. + +|`provers_check` +|One prover: present, version, drift against the lock, or the reason it +is unavailable. + +|`provers_prove` +|`{file \| goal, prover?, timeout}` → `{verdict, trust_level, prover, +certificate?, axioms, raw}`. Dispatches through `echidna prove --format +json`; the five-level trust hierarchy and the axiom scan are echidna's. + +|`provers_portfolio` +|Same input, two or more provers; returns each verdict and the combined +trust level (level 5 only when two independent small-kernel systems agree +with certificates, per echidna's `confidence.rs`). + +|`provers_recheck` +|The PROOF-POLICY §2 route: an Agda proof transported through Dedukti to +Rocq and Lean, with `transported` or `re-proved` recorded per leg and the +statement comparison named. Needs the kit's `transport` entries present. + +|`provers_exchange` +|Translate between Dedukti, Lambdapi, TPTP, SMT-LIB, OpenTheory, SMTCoq +through echidna's exchange layer. No verdict; a translation and its hash. + +|`provers_certificate` +|Check a certificate (Alethe, DRAT, LRAT, TSTP, Lean or Rocq kernel +export) independently of the prover that produced it. +|=== + +=== `solvers-mcp`: solving + +Input is a problem (SMT-LIB, DIMACS, MiniZinc, LP, a TLA+ or Promela +model); the answer is a model, a proof of unsatisfiability, an optimum, or +a bounded model-checking result with its bounds. Solver results are +`TESTED` with bounds or `PROVEN` with a checked certificate, never +silently the latter. + +[cols="1,3",options="header"] +|=== +|Tool |Contract + +|`solvers_list`, `solvers_check` +|As for provers, over echidna tiers 8, 9 and 10 and the kit's `backend` +entries (Z3, CVC5, Yices, Alt-Ergo, E, Vampire). + +|`solvers_sat` +|`{problem, format, solver?, want: model \| unsat_core \| certificate}` → +the requested artefact plus timing. Portfolio across Z3, CVC5 and Alt-Ergo +with disagreement flagged, as echidna's `portfolio.rs` does. + +|`solvers_optimise` +|MiniZinc, Chuffed, OR-Tools, GLPK, SCIP: objective, bound, solution, +proof of optimality where the solver emits one. + +|`solvers_model_check` +|TLC, SPIN, NuSMV, Alloy, PRISM, Storm, UPPAAL, ProB: the property, the +bounds, the counter-example if any. Reported as `TESTED` with bounds, per +PROOF-POLICY §4. + +|`solvers_certificate` +|Alethe, DRAT, LRAT, LFSC checking, shared with `provers_certificate` +through one implementation. +|=== + +=== `code-verifiers-mcp`: verifying code in its own language + +Input is a source tree with contracts; the answer is a proof ledger in +the PROOF-POLICY §5 vocabulary (`PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`, +`ASSUMED`, `OPEN`) with a receipt. This is the cartridge for the tools that +sit *on* code rather than on proof files: Creusot and Kani for Rust, SPARK +for Ada, Aeneas for Rust-to-model, Dafny, Why3 and Cameleer, F*, and the +estate's own verifiers as they arrive: Quintessence (Elixir/OTP, three +layers, already producing TrustLevel 4 certificates), Apodeixis.jl (Julia; +today a fail-closed policy audit, verifier planned), atoma and bactarin +(no initialised repository yet; atoma is still the untouched template and +bactarin has no repository in the estate listing). + +[cols="1,3",options="header"] +|=== +|Tool |Contract + +|`verifiers_list` +|The language-to-verifier mapping this host can serve, from PROOF-POLICY +§1 and the capability record: Rust → Creusot (+ Kani, Aeneas), Ada → SPARK, +Elixir → Quintessence, Julia → Apodeixis.jl, and the §4 exceptions. + +|`verifiers_verify` +|`{path, language?, tool?, obligations?}` → the ledger: one row per +obligation with status, tool, version, provers used, axioms, and the +`ASSUMED` boundary rows for third-party code (§1.1). + +|`verifiers_obligations` +|List the verification conditions a tool generates for a path, without +discharging them. Lets an agent see the proof surface before paying for it. + +|`verifiers_receipt` +|The hashed receipt for a ledger: inputs, tool and prover versions by lock +hash, bounds for `TESTED` rows. Quintessence's SHA-256 binary receipt and +Apodeixis's planned warrant-to-receipt pipeline are the two estate +instances of this shape; the cartridge defines the common one. + +|`verifiers_mutate` +|Run echidna's mutation engine (or Quintessence's six-kind one) over a +specification and report the mutation score against the 95% default. +|=== + +Why a third cartridge rather than a section of `provers-mcp`: the input +is code, the mapping is by language, the output is a ledger rather than a +verdict, and the future estate tools all land here. Keeping it separate +means Quintessence, Apodeixis.jl, atoma and bactarin each add one +`verifiers_list` row and one dispatch arm, with no change to the proving +or solving surfaces. + +=== What `proof-mcp` becomes + +Keep it, and make it honest: `proof-mcp` is the *lifecycle* layer (slots, +state machine, the Idris2 proofs it already has); its `proof_verify` +composes `provers_prove` under ADR-0014's composition contract instead of +posting to a port nothing serves. Its backend list is replaced by a read of +`provers_list`. The alternative, deleting it, throws away a proved state +machine for no gain. + +== Options compared + +[cols="1,3,1,1,1",options="header"] +|=== +|Option |Shape |Elegance / correctness |Dependability |Security / privacy + +|*A. Three cartridges on one seam* (recommended) +|`provers-mcp`, `solvers-mcp`, `code-verifiers-mcp`; `proof-mcp` as +lifecycle over them; all advertise from the capability record. +|High. Each surface has one input kind and one answer kind; the roster is +never typed by hand. +|High once the kit's `doctor` exists; until then the cartridges can run +against echidna's own `check-prover`. +|High. Shield tier; sandboxed execution (echidna's Podman or bwrap +executor, ADR-0009's local provider); no LLM in the verdict path. + +|*B. One `echidna-mcp` cartridge* +|Port the three tools of `crates/echidna-mcp` into the store as they are. +|Low. Satisfies ADR-0002 in an afternoon, but "prove this file with this +prover" is the whole surface: no portfolio, no ledger, no solving, and the +hard-coded "105". +|Medium. Nothing to maintain beyond echidna. +|Medium. Inherits echidna's sandbox only if `echidna prove` is called with +it on. + +|*C. One `formal-methods-mcp` mega-cartridge* +|Every tool of A in one cartridge. +|Low. One `cartridge.json` with twenty tools across three answer kinds; +the ledger and verdict vocabularies get mixed. +|Medium. +|Medium. One tier for tools with very different blast radius. + +|*D. Alternative path: the store is the manifest* +|Render each cartridge's `cartridge.json` tool catalogue and the `prover` +enum in its input schemas from echidna's `provers.a2ml` and the kit's +capability record, with one `invoke(prover, input)` tool per cartridge +whose schema is generated. Same `render` pattern as `provers.sh render`. +|Highest for drift (a new `ProverKind` variant appears in the schema on +the next render) and lowest for readability of the tool list. +|Medium until `provers.a2ml` carries the `binary` and `family` fields the +awesome-lists proposal asks for. +|High. Same as A. +|=== + +Recommendation: A, with D's generated `prover` enum adopted inside A's +input schemas as soon as the registry fields exist. B is the right +*first step* of A, not an alternative to it: port `crates/echidna-mcp` +into `provers-mcp` first, then grow. + +== Experiments before building + +[cols="1,3,2",options="header"] +|=== +|Id |Experiment |Pass criterion + +|Z1 +|Run `crates/echidna-mcp` over stdio against a host with only Z3 present; +call `list_provers`, `check_prover`, `prove` on a one-line SMT-LIB file. +|`prove` returns `verified: true` for a satisfiable goal; `check_prover` +says `Lean` is unavailable rather than failing. This is the backend +contract the cartridge wraps. + +|Z2 +|Replace `proof-mcp`'s `mod.js` POST to port 7707 with a subprocess call +to `echidna prove --format json`, and call `proof_verify` through the +stdio bridge. +|The verdict reaches the caller; the Zig adapter's `"forwarded"` stub is +retired. Proves the cartridge can be real without the Elixir REST port. + +|Z3 +|Scaffold `provers-mcp` from `templates/gossamer-mcp`, write its +`cartridge.json`, run the store's `just validate` and +`scripts/typecheck-proofs.sh`. +|Manifest validates against `cartridge-v1.json` at the pinned SHA; the +Idris2 ABI type-checks with zero `believe_me`. + +|Z4 +|Feed the same theorem to Z3 and CVC5, then to Lean and Rocq, through +`provers_portfolio`. +|The SMT pair reports level 3 at most; the kernel pair reports level 5 +only with certificates. The trust mapping is observed, not assumed. + +|Z5 +|Compose `proof-mcp.proof_verify` → `provers-mcp.provers_prove` and run +the ADR-0014 composition check on the typed boundary. +|The composition is admitted by the typed contract or the ADR names what +is missing; either outcome is the fact the cartridge needs. + +|Z6 +|`verifiers_verify` on Quintessence's own 15-case suite and on a Creusot +example crate. +|Both produce a ledger in the §5 vocabulary with a receipt; the Creusot +rows name Why3 and the provers by lock hash. +|=== + +== The formal route + +Three things here are interface contracts, so under PROOF-POLICY §1 they +are Idris2: + +* The `prover` argument's type. Derive it from echidna's `ProverKind` (the + `.machine_readable/provers.a2ml` slugs) so an unknown prover is rejected + at the ABI boundary, not discovered as a runtime string mismatch. The + cartridge template already puts the ABI in Idris2. +* The capability record, shared with `environment-of-environments.adoc`: + one `EnvCapability` type consumed by `provers_list`, `solvers_list` and + `verifiers_list`, so the three cartridges cannot disagree about what the + host holds. +* The ledger row. The §5 vocabulary is a closed sum type; a `TESTED` row + carries bounds and a `PROVEN` row carries a certificate reference by + construction. + +One theory statement is worth an Agda file: echidna's five trust levels +form a chain, and a portfolio's level is the meet of its members' levels +except for the one case (two independent small-kernel systems, both with +certificates) that lifts to level 5. Stating that as a lattice property and +rechecking it in Rocq and Lean per §2 is small, and it is the property an +agent relies on when it reads `trust_level: 5`. + +== Aspects + +Security:: The cartridges execute untrusted proof and problem files. +Shield tier; every dispatch runs under echidna's sandbox (Podman +`--network=none`, read-only, limits; bwrap fallback; the unsandboxed mode +refused rather than defaulted). ADR-0009's `sandbox-mcp` local provider is +the same mechanism once it exists. +Privacy:: Proof content can be proprietary. The verdict path has no +network egress and no LLM; `echidna-llm-mcp` stays a separate, opt-in +cartridge. Receipts carry hashes, not content. +Honesty:: Every list is read from the capability record. A prover the +host lacks is `UNAVAILABLE` with a reason, never a stub answer. The +store's `available: true` must mean a process answered, which today it +does not for `proof-mcp`. +Licensing:: PVS, Imandra and other non-free backends are dispatchable only +where installed; the cartridge reports them unavailable elsewhere and +never bundles them. +Observability:: Receipts hashed with BLAKE3 as echidna's certificates +are; the kit lock's SHA-256 named per tool so a receipt pins the exact +binary. +Composition:: ADR-0014 applies: `proof-mcp` composing `provers-mcp` is the +first real cross-cartridge call in the store and the right test case for +that ADR. + +== Beyond this repository + +* `hyperpolymath/boj-server-cartridges`: three new cartridges under + `domains/formal-verification/`; `proof-mcp` rewired to compose rather + than POST to port 7707; its backend list replaced by a capability read. +* `hyperpolymath/echidna`: `crates/echidna-mcp` either becomes the + `provers-mcp` backend contract or is retired under ADR-0002; `list-provers + --format json` should emit slug, family, binary and tier so the cartridge + schemas can be rendered; the hard-coded "105" in its tool descriptions + is the drift `PROVER_COUNT.adoc` names. +* `hyperpolymath/boj-server`: ADR-0014's composition contract gets its + first instance; the catalogue's `available` flag needs a liveness + meaning. +* `hyperpolymath/quintessence` and `hyperpolymath/Apodeixis.jl`: a + `verify --format json` command whose output is the §5 ledger row shape, + so `code-verifiers-mcp` dispatches to both without adapters. +* `hyperpolymath/atoma`: still the uninitialised RSR template (README + tokens unfilled); it needs an identity before it can be a verifier row. +* `bactarin`: no repository exists in the estate listing yet. +* `hyperpolymath/standards`: the cartridge spec's domain list may want + `proving`, `solving` and `code-verification` as named domains rather + than one `formal-verification`. + +== Decisions needed + +. Three cartridges (A) or the one-cartridge first step (B) now, growing + into A. +. Whether `proof-mcp` is kept as the lifecycle layer or retired. +. Whether `crates/echidna-mcp` is retired once `provers-mcp` exists, per + ADR-0002. +. Whether to open the cartridge scaffolds in `boj-server-cartridges` now + (experiment Z3) or after the kit's `doctor` ships, since the cartridges' + honesty depends on the capability record. From 9d8bb8d153e7785beea187a5a38bceaf14361fae Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 09:31:48 +0000 Subject: [PATCH 04/16] feat(proof-toolchain): add HOL Light, HOL4, ACL2 and Mizar (E6); record the owner's rulings Owner decisions of 2026-10-27 on #98: - E6 accepted: hol-light, hol4 (with a bundled polyml runtime), acl2 (with a bundled sbcl runtime) and mizar join toolchain.kyaml as exception:recorded entries, resolve or resolve-stable pins, smoke fixtures that land with the bundle build. The kit now declares eleven of echidna's twelve core backends; PVS stays in the sealed-container tail. DESIGN.adoc's roles table and the coverage table in the environment-of-environments proposal say so. - Awesome lists: refresh awesome-provable and awesome-agda first and run the link-rot baseline (Y1) before creating any repository; the eleven priority-1 lists are the batch after that. - Format: A2ML is retired by the deed format and coordination.k9 by k9-coordination (grammars in standards 1-formats/deed/spec/abnf and 2-protocols/k9-coordination/spec/abnf). Each proposal now carries a format note: .a2ml names locate today's content; every proposed field targets the deed. Validated: the manifest parses with yq (36 tools, every `needs` edge resolves to an entry), asciidoctor --failure-level WARN on every proposal, DESIGN.adoc and CHANGELOG.adoc, check-no-md-in-docs passes. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- CHANGELOG.adoc | 5 ++++ .../awesome-estate-maths-proving.adoc | 22 ++++++++++++---- .../boj-prover-solver-cartridges.adoc | 9 +++++++ .../environment-of-environments.adoc | 26 ++++++++++++++----- tools/proof-toolchain/DESIGN.adoc | 4 +-- tools/proof-toolchain/toolchain.kyaml | 6 +++++ 6 files changed, 59 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index b3ff2e0..2b650b5 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -23,6 +23,11 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. (`provers-mcp`, `solvers-mcp`, `code-verifiers-mcp`) on the capability record seam, what the store's `proof-mcp` becomes, and where Quintessence, Apodeixis.jl, atoma and bactarin land. +* `tools/proof-toolchain/toolchain.kyaml` — HOL Light, HOL4, ACL2 and + Mizar as `exception:recorded` entries, with Poly/ML and SBCL as their + bundled runtimes (E6, owner decision 2026-10-27): the kit now declares + eleven of echidna's twelve core backends; PVS stays in the + sealed-container tail. * `tools/environments/` — `environments.kyaml` (environment classes with a `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment X1: HEAD-only reachability probe). diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc index 1c9763d..109d177 100644 --- a/docs/proposals/awesome-estate-maths-proving.adoc +++ b/docs/proposals/awesome-estate-maths-proving.adoc @@ -12,6 +12,12 @@ type-discipline variants with no binary) and `src/rust/provers/` (the binary each backend spawns). The existing lists were read from the `stuff-of-awe` organisation on the same date. +Format note: echidna's prover registry is cited as `provers.a2ml` +because that is the file today. A2ML is retired in favour of the deed +format (standards `1-formats/deed/spec/abnf/deed.abnf`); the `binary`, +`family` and `owner` fields proposed below target echidna's deed once +the `.a2ml` to `.deed` conversion (ruling D313) lands there. + This proposal lives in bofj-kitt because the kit is where the estate decides which provers an environment carries; the lists are the human index of the same roster. Nothing here creates a repository; see <>. @@ -342,9 +348,14 @@ shell script over `yq` and `jq`. |=== Recommendation: A for the repositories, with D as the way their tool -tables are produced once the registry fields exist in echidna. Start with -the eleven priority-1 lists; hand-curate their prose; render their tool -tables as soon as `provers.a2ml` carries the fields. +tables are produced once the registry fields exist in echidna. + +Decided 2026-10-27 (owner): *refresh the existing lists first.* +`awesome-provable` (2018 content) and `awesome-agda` (73 lines) are brought +up to date before any repository is created, and experiment Y1's link-rot +numbers are in hand before the first batch is cut. The eleven priority-1 +lists remain the proposed first batch after that; hand-curate their prose; +render their tool tables as soon as echidna's registry carries the fields. == Experiments before the first batch @@ -427,8 +438,9 @@ twenty-one more lists inherit the wrong obligations. [[decisions]] == Decisions needed -. Confirm option A and the eleven priority-1 lists as the first batch, - or trim. +. Decided 2026-10-27: refresh `awesome-provable` and `awesome-agda` + first and run Y1; the eleven priority-1 lists are the batch after that, + to be confirmed or trimmed with the rot numbers in hand. . Confirm `stuff-of-awe` as the organisation for all of them (the estate board still lists the existing lists under `hyperpolymath/`). . Whether `awesome-lean` and `awesome-sat` are forks (pending Y3) or fresh. diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index 0db194d..a8a9847 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -5,6 +5,15 @@ :toclevels: 3 :sectnums: +Format note: where this document names an `.a2ml` file it is locating +today's content. A2ML is retired in favour of the deed format (grammar: +standards `1-formats/deed/spec/abnf/deed.abnf`) and `coordination.k9` by +k9-coordination (`2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.2.abnf`); +ruling D313 makes the `.a2ml` to `.deed` conversion a tooling front end +rather than a hand sweep. Every new field proposed here (the registry's +`binary`, `family` and `owner` fields, the capability record's home) +targets the deed, not A2ML. + Status: proposal, 2026-10-27. Companion to `environment-of-environments.adoc` (the capability record these cartridges advertise from) and `awesome-estate-maths-proving.adoc` (the roster they diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index c597d10..8b74e74 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/docs/proposals/environment-of-environments.adoc @@ -5,6 +5,15 @@ :toclevels: 3 :sectnums: +Format note: `.a2ml` files are named here only to locate today's +content (`groove.a2ml`, `STATE.a2ml`). A2ML is retired in favour of the +deed format (standards `1-formats/deed/spec/abnf/deed.abnf`) and +`coordination.k9` by k9-coordination +(`2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.2.abnf`). +The capability record and the Groove `capabilities` field proposed below +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 <> were taken in one cloud agent session on that date and are reproducible with `tools/environments/probe-reachability.sh`. @@ -200,13 +209,18 @@ 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 |none |*Missing* (OCaml; opam reachable here) -|HOL4 |none |*Missing* (Poly/ML) -|ACL2 |none |*Missing* (SBCL; upstream host failed TLS here) -|Mizar |none |*Missing* (binary release) +|HOL Light |`hol-light` |Covered (added 2026-10-27 on the owner's decision; opam) +|HOL4 |`hol4` with `polyml` |Covered (added 2026-10-27; source build on bundled Poly/ML) +|ACL2 |`acl2` with `sbcl` |Covered (added 2026-10-27; the bundle build fetches it, since its host failed TLS from a session) +|Mizar |`mizar` |Covered (added 2026-10-27; system distribution with its MML) |PVS |none |*Missing*, licensed binary: sealed-container tail |=== +E6 was decided on 2026-10-27: the four entries above are in the manifest +with `resolve` or `resolve-stable` pins and smoke fixtures that land with +the bundle build, so the kit now declares eleven of echidna's twelve core +backends and names the twelfth's home. + == Options compared [cols="1,3,1,1,1",options="header"] @@ -360,7 +374,7 @@ rather than lost: all, given the policy measured here. If not, the session leg is `doctor`-only and the session's provers come from a prebuilt image or from a mise/Guix path the platform allows. -. Whether HOL Light, HOL4, ACL2 and Mizar join the manifest now (E6) or - wait for an echidna consumer that needs them. +. Decided 2026-10-27: HOL Light, HOL4, ACL2 and Mizar join the manifest + now (E6); the entries are in `toolchain.kyaml`. . Whether X3 runs before the first bundle release, so the transport is chosen once. diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index 2f99c00..e1acc87 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -157,8 +157,8 @@ plus the supporting tools the mapped provers need. |`policy:recheck` |Rocq (`coqc`), Lean (elan with pinned toolchains; no Mathlib) |`transport` |agda2dedukti, Dedukti (`dkcheck`), Lambdapi. agda2dedukti tracks particular Agda versions; the manifest records which Agda it accepts. |`exception:rust` |Kani; Aeneas with Charon (PROOF-POLICY §4.1) -|`exception:recorded` |TLA+ (`tlc`); Isabelle (supplementary only) -|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin) and a Java runtime for the `tlc` launcher, bundled rather than taken from the host +|`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2 and Mizar (supplementary only). The last four were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set; PVS, the remaining core backend, is a licensed binary and belongs to the sealed-container tail, not the bundle. +|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, Poly/ML for HOL4 and SBCL for ACL2, bundled rather than taken from the host |`backend` |Z3, CVC5, Yices, Alt-Ergo, E prover, Vampire |=== diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml index abfb9a0..c9b25ca 100644 --- a/tools/proof-toolchain/toolchain.kyaml +++ b/tools/proof-toolchain/toolchain.kyaml @@ -43,6 +43,12 @@ {id: "tlc", role: "exception:recorded", method: "release asset (tlaplus tla2tools.jar) plus a bundled tlc launcher (java -cp $PREFIX/lib/tla/tla2tools.jar tlc2.TLC, absolute so it runs from any directory)", pin: "resolve-stable", verify: "tlc -h", needs: ["jre"], notes: "pin a stable tagged release with its sha256 in the lock; v1.8.0 is a rolling prerelease rebuilt on every master commit"}, {id: "jre", role: "runtime", method: "release asset (Eclipse Temurin JRE, Java 17 or later)", pin: "resolve-stable", verify: "java -version", notes: "bundled so the tlc launcher does not depend on a host Java"}, {id: "isabelle", role: "exception:recorded", method: "release asset", pin: "resolve", verify: "isabelle version", notes: "supplementary evidence only"}, + {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and checks the theorem echo; it lands with the bundle build. Supplementary evidence only, as Isabelle"}, + {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly --version", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, + {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure; it lands with the bundle build. Supplementary evidence only"}, + {id: "sbcl", role: "runtime", method: "release asset (sbcl/sbcl Linux x86_64 binary)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 is built on; bundled so acl2 does not depend on a host Lisp"}, + {id: "acl2", role: "exception:recorded", method: "release asset (acl2/acl2 tagged source) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books are not bundled; a consumer that needs them records that as its own entry. The upstream download host failed TLS from one agent session (environments.kyaml), so the bundle build fetches it, not the session. Supplementary evidence only"}, + {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML)", pin: "resolve-stable", verify: "makeenv $PREFIX/share/smoke/smoke.miz && verifier $PREFIX/share/smoke/smoke.miz", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. Supplementary evidence only"}, {id: "z3", role: "backend", method: "release asset", pin: "resolve", verify: "z3 --version"}, {id: "cvc5", role: "backend", method: "release asset", pin: "resolve", verify: "cvc5 --version"}, {id: "yices", role: "backend", method: "release asset (SRI-CSL yices2)", pin: "resolve-stable", verify: "yices --version"}, From bbffdce424f16b44ac400ca2b391d446fbd844f9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:28:54 +0000 Subject: [PATCH 05/16] Update docs/proposals/boj-prover-solver-cartridges.adoc Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- docs/proposals/boj-prover-solver-cartridges.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index a8a9847..4d86560 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = BoJ cartridges for proving, solving and code verification :toc: From 49b3d001dbee23b5c48f074bee1a3a2af2c66039 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:29:51 +0000 Subject: [PATCH 06/16] Update tools/proof-toolchain/toolchain.kyaml Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- tools/proof-toolchain/toolchain.kyaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml index c9b25ca..4e2ebc9 100644 --- a/tools/proof-toolchain/toolchain.kyaml +++ b/tools/proof-toolchain/toolchain.kyaml @@ -44,7 +44,7 @@ {id: "jre", role: "runtime", method: "release asset (Eclipse Temurin JRE, Java 17 or later)", pin: "resolve-stable", verify: "java -version", notes: "bundled so the tlc launcher does not depend on a host Java"}, {id: "isabelle", role: "exception:recorded", method: "release asset", pin: "resolve", verify: "isabelle version", notes: "supplementary evidence only"}, {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and checks the theorem echo; it lands with the bundle build. Supplementary evidence only, as Isabelle"}, - {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly --version", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, + {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure; it lands with the bundle build. Supplementary evidence only"}, {id: "sbcl", role: "runtime", method: "release asset (sbcl/sbcl Linux x86_64 binary)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 is built on; bundled so acl2 does not depend on a host Lisp"}, {id: "acl2", role: "exception:recorded", method: "release asset (acl2/acl2 tagged source) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books are not bundled; a consumer that needs them records that as its own entry. The upstream download host failed TLS from one agent session (environments.kyaml), so the bundle build fetches it, not the session. Supplementary evidence only"}, From e994160a0a8da80f4d04b2d10322b104b40fe4e0 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:34:20 +0000 Subject: [PATCH 07/16] fix(k9): exclude session YAML bindings and align components with K9-SVC validation --- .github/hooks/validate-k9.sh | 19 ++- .machine_readable/svc/k9/README.adoc | 21 +++- .../svc/k9/methodology-guard.k9.ncl | 15 +++ container/README.adoc | 5 +- container/deploy.k9.ncl | 115 ++++++++--------- tests/workflows/validate_k9_test.sh | 116 ++++++++++++++++++ 6 files changed, 227 insertions(+), 64 deletions(-) create mode 100644 tests/workflows/validate_k9_test.sh diff --git a/.github/hooks/validate-k9.sh b/.github/hooks/validate-k9.sh index c83e290..e6138e7 100755 --- a/.github/hooks/validate-k9.sh +++ b/.github/hooks/validate-k9.sh @@ -4,13 +4,17 @@ # # validate-k9.sh — K9 configuration file validation script # -# Scans for .k9 and .k9.ncl files and validates: +# Scans for K9-SVC .k9 and .k9.ncl components and validates: # 1. K9! magic number on line 1 # 2. Pedigree block presence with required fields (name, version) # 3. Security level is one of: kennel, yard, hunt (case-insensitive) # 4. Hunt-level files must have a signature or signature_required field # 5. SPDX-License-Identifier header presence # +# The two YAML session-management bindings (coordination.k9 and +# session/custom-checks.k9) use a separate format. Keep their paths and +# contents intact; they are not K9-SVC components (see EXPLAINME.adoc). +# # Environment variables: # INPUT_PATH — Directory to scan (default: .) # INPUT_STRICT — Promote warnings to errors (default: false) @@ -26,6 +30,7 @@ set -euo pipefail # --------------------------------------------------------------------------- SCAN_PATH="${INPUT_PATH:-.}" +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" STRICT="${INPUT_STRICT:-false}" PATHS_IGNORE_RAW="${INPUT_PATHS_IGNORE:-}" GITHUB_OUTPUT_FILE="${GITHUB_OUTPUT:-/dev/null}" @@ -301,11 +306,19 @@ mapfile -t k9_candidates < <(find "$SCAN_PATH" \( -name '*.k9' -o -name '*.k9.nc # Apply paths-ignore filter k9_files=() SKIPPED=0 +SESSION_BINDINGS=0 for _f in "${k9_candidates[@]}"; do if path_ignored "$_f"; then SKIPPED=$((SKIPPED + 1)) continue fi + # Match the actual repository files, not substrings or basenames: a + # component named coordination.k9 elsewhere must still be validated. + if [[ "$_f" -ef "$REPO_ROOT/coordination.k9" || \ + "$_f" -ef "$REPO_ROOT/session/custom-checks.k9" ]]; then + SESSION_BINDINGS=$((SESSION_BINDINGS + 1)) + continue + fi k9_files+=("$_f") done @@ -313,6 +326,10 @@ if [[ $SKIPPED -gt 0 ]]; then echo "::notice::Skipped ${SKIPPED} file(s) matching paths-ignore" fi +if [[ $SESSION_BINDINGS -gt 0 ]]; then + echo "::notice::Excluded ${SESSION_BINDINGS} session-management binding(s); these use YAML, not K9-SVC" +fi + if [[ ${#k9_files[@]} -eq 0 ]]; then echo "::notice::No K9 files found in ${SCAN_PATH}" echo "files_scanned=0" >> "$GITHUB_OUTPUT_FILE" 2>/dev/null || true diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc index 005ce58..7fc713d 100644 --- a/.machine_readable/svc/k9/README.adoc +++ b/.machine_readable/svc/k9/README.adoc @@ -82,10 +82,23 @@ cp .machine_readable/contractiles/k9/examples/setup-repo.k9.ncl scripts/setup.k9 === 2. Validate Components +Each K9-SVC component starts with `K9!`, followed by its Nickel payload. +The repository gate checks the marker, pedigree and security declaration: + +[source,bash] +---- +bash .github/hooks/validate-k9.sh +---- + +`coordination.k9` and `session/custom-checks.k9` are YAML bindings for the +central session-management standards, as described in `EXPLAINME.adoc`. +They retain their existing format and are excluded by exact repository file +identity. Other `.k9` files still receive the K9-SVC checks. + [source,bash] ---- -# Validate Nickel syntax and contracts -nickel typecheck config/metadata.k9.ncl +# Validate Nickel syntax and contracts after removing the K9! marker +tail -n +2 config/metadata.k9.ncl | nickel typecheck # Verify Hunt-level signature (if signed) ./must verify scripts/setup.k9.ncl @@ -96,10 +109,10 @@ nickel typecheck config/metadata.k9.ncl [source,bash] ---- # Kennel: Export as JSON -nickel export config/metadata.k9.ncl > metadata.json +tail -n +2 config/metadata.k9.ncl | nickel export > metadata.json # Yard: Evaluate with validation -nickel eval .github/ci.k9.ncl +tail -n +2 .github/ci.k9.ncl | nickel eval # Hunt: Run with Just (dry-run first!) ./must --dry-run run scripts/setup.k9.ncl diff --git a/.machine_readable/svc/k9/methodology-guard.k9.ncl b/.machine_readable/svc/k9/methodology-guard.k9.ncl index 6bd7c4a..4eacd02 100644 --- a/.machine_readable/svc/k9/methodology-guard.k9.ncl +++ b/.machine_readable/svc/k9/methodology-guard.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -8,6 +9,20 @@ # Usage: k9 validate methodology-guard let methodology_guard = { + pedigree = { + schema_version = "1.0.0", + metadata = { + name = "methodology-guard", + version = "1.0.0", + }, + security = { + leash = 'Kennel, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + }, + name = "methodology-guard", version = "1.0.0", description = "Validates that agent work respects declared methodology constraints", diff --git a/container/README.adoc b/container/README.adoc index 08d9f83..be59a41 100644 --- a/container/README.adoc +++ b/container/README.adoc @@ -154,8 +154,9 @@ For k9-svc managed deployments: [source,bash] ---- -# Validate the deployment component -nickel typecheck container/deploy.k9.ncl +# After container-init has rendered the placeholders, validate the Nickel +# payload (the first line is the K9! format marker). +tail -n +2 container/deploy.k9.ncl | nickel typecheck # Deploy (requires Hunt-level authorisation) k9-svc deploy container/deploy.k9.ncl --env production diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index 5e6a6e0..583a4e6 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # deploy.k9.ncl — bofj-kitt deployment component (Hunt level) # @@ -8,65 +9,10 @@ # It requires explicit authorisation via the Leash system. # # Usage: -# nickel typecheck container/deploy.k9.ncl +# tail -n +2 container/deploy.k9.ncl | nickel typecheck # k9-svc validate container/deploy.k9.ncl # k9-svc deploy container/deploy.k9.ncl --env production -# The component's pedigree (self-description across five layers) -let component_pedigree = { - # ───────────────────────────────────────────────────────────── - # L1: The Snout — Identity - # ───────────────────────────────────────────────────────────── - metadata = { - name = "{{SERVICE_NAME}}-deploy", - version = "{{VERSION}}", - breed = "application/vnd.k9+nickel", - magic_number = "K9!", - description = "bofj-kitt deployment component (Hunt level)", - }, - - # ───────────────────────────────────────────────────────────── - # L2: The Scent — Target Environment - # ───────────────────────────────────────────────────────────── - target = { - os = 'Linux, - is_edge = false, - requires_podman = true, - min_memory_mb = 256, - }, - - # ───────────────────────────────────────────────────────────── - # L3: The Leash — Security - # ───────────────────────────────────────────────────────────── - security = { - trust_level = 'Hunt, - allow_network = true, - allow_filesystem_write = true, - allow_subprocess = true, - # In production, replace with a real Ed25519 signature. - signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", - }, - - # ───────────────────────────────────────────────────────────── - # L4: The Gut — Self-Validation - # ───────────────────────────────────────────────────────────── - validation = { - checksum = "sha256:placeholder", - pedigree_version = "1.0.0", - hunt_authorized = false, # Must be set true after handshake - }, - - # ───────────────────────────────────────────────────────────── - # L5: The Muscle — Deployment Recipes - # ───────────────────────────────────────────────────────────── - recipes = { - install = "just container-build", - validate = "just container-verify", - deploy = "just container-up", - migrate = "just container-build && just container-up", - }, -} in - # Deployment configuration let deployment = { # Target environments (dev / staging / production) @@ -143,7 +89,62 @@ echo "K9: Rollback complete." # Export the component { - pedigree = component_pedigree, + # The component's pedigree (self-description across five layers) + pedigree = { + # ───────────────────────────────────────────────────────────── + # L1: The Snout — Identity + # ───────────────────────────────────────────────────────────── + metadata = { + name = "{{SERVICE_NAME}}-deploy", + version = "{{VERSION}}", + breed = "application/vnd.k9+nickel", + magic_number = "K9!", + description = "bofj-kitt deployment component (Hunt level)", + }, + + # ───────────────────────────────────────────────────────────── + # L2: The Scent — Target Environment + # ───────────────────────────────────────────────────────────── + target = { + os = 'Linux, + is_edge = false, + requires_podman = true, + min_memory_mb = 256, + }, + + # ───────────────────────────────────────────────────────────── + # L3: The Leash — Security + # ───────────────────────────────────────────────────────────── + security = { + leash = 'Hunt, + trust_level = 'Hunt, + signature_required = true, + allow_network = true, + allow_filesystem_write = true, + allow_subprocess = true, + # In production, replace with a real Ed25519 signature. + signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", + }, + + # ───────────────────────────────────────────────────────────── + # L4: The Gut — Self-Validation + # ───────────────────────────────────────────────────────────── + validation = { + checksum = "sha256:placeholder", + pedigree_version = "1.0.0", + hunt_authorized = false, # Must be set true after handshake + }, + + # ───────────────────────────────────────────────────────────── + # L5: The Muscle — Deployment Recipes + # ───────────────────────────────────────────────────────────── + recipes = { + install = "just container-build", + validate = "just container-verify", + deploy = "just container-up", + migrate = "just container-build && just container-up", + }, + }, deployment = deployment, scripts = scripts, diff --git a/tests/workflows/validate_k9_test.sh b/tests/workflows/validate_k9_test.sh new file mode 100644 index 0000000..73fe59f --- /dev/null +++ b/tests/workflows/validate_k9_test.sh @@ -0,0 +1,116 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Regression tests for K9-SVC validation and session-binding compatibility. + +set -euo pipefail + +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +TEST_ROOT="$(mktemp -d)" +trap 'rm -rf "$TEST_ROOT"' EXIT + +# Exercise the real hook in an isolated repository, including its two +# repository-relative session bindings. No Nickel evaluation is needed. +mkdir -p "$TEST_ROOT/repo/.github/hooks" "$TEST_ROOT/repo/session" "$TEST_ROOT/scan" +cp "$REPO_ROOT/.github/hooks/validate-k9.sh" "$TEST_ROOT/repo/.github/hooks/" +cp "$REPO_ROOT/coordination.k9" "$TEST_ROOT/repo/" +cp "$REPO_ROOT/session/custom-checks.k9" "$TEST_ROOT/repo/session/" +VALIDATOR="$TEST_ROOT/repo/.github/hooks/validate-k9.sh" +export INPUT_PATHS_IGNORE="" INPUT_STRICT=false +export GITHUB_OUTPUT="$TEST_ROOT/output" + +expect_status() { + local label="$1" expected="$2" actual=0 + shift 2 + "$@" > "$TEST_ROOT/log" 2>&1 || actual=$? + if [[ "$actual" != "$expected" ]]; then + cat "$TEST_ROOT/log" >&2 + echo "FAIL: $label (expected exit $expected, got $actual)" >&2 + exit 1 + fi + echo "PASS: $label" +} + +expect_log() { + if ! grep -Fq "$1" "$TEST_ROOT/log"; then + cat "$TEST_ROOT/log" >&2 + echo "FAIL: expected diagnostic: $1" >&2 + exit 1 + fi +} + +cat > "$TEST_ROOT/valid.k9" <<'EOF' +K9! +# SPDX-License-Identifier: MPL-2.0 +{ + pedigree = { + schema_version = "1.0.0", + security = { + leash = 'Kennel, + }, + metadata = { + name = "test-component", + version = "1.0.0", + }, + }, +} +EOF + +# Resolve exemptions against the hook's repository, regardless of cwd or +# whether INPUT_PATH is relative, absolute, a subdirectory, or a single file. +cd "$TEST_ROOT/repo" +expect_status "session YAML bindings retain their format" 0 bash "$VALIDATOR" +expect_log "Excluded 2 session-management binding(s)" +expect_log "No K9 files found" +cd "$TEST_ROOT" +expect_status "absolute scan from another directory" 0 env INPUT_PATH="$TEST_ROOT/repo" INPUT_STRICT=true bash "$VALIDATOR" +expect_log "Excluded 2 session-management binding(s)" +expect_status "session subdirectory scan" 0 env INPUT_PATH=repo/session bash "$VALIDATOR" +expect_log "Excluded 1 session-management binding(s)" +expect_status "single binding scan" 0 env INPUT_PATH=repo/coordination.k9 bash "$VALIDATOR" +expect_log "Excluded 1 session-management binding(s)" + +# Only the two actual session files are exempt. Namesakes elsewhere remain +# subject to normal K9-SVC checks, including when scanned outside the repo. +cp "$TEST_ROOT/repo/coordination.k9" "$TEST_ROOT/scan/coordination.k9" +expect_status "unrelated coordination.k9 is validated" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Missing K9! magic number" +mv "$TEST_ROOT/scan/coordination.k9" "$TEST_ROOT/scan/custom-checks.k9" +expect_status "unrelated custom-checks.k9 is validated" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Missing pedigree block" +rm "$TEST_ROOT/scan/custom-checks.k9" + +cp "$TEST_ROOT/valid.k9" "$TEST_ROOT/scan/component.k9" +expect_status "nested metadata is accepted in strict mode" 0 env INPUT_PATH=scan INPUT_STRICT=true bash "$VALIDATOR" +expect_log "Files scanned: 1" + +tail -n +2 "$TEST_ROOT/valid.k9" > "$TEST_ROOT/scan/component.k9" +expect_status "missing component marker still fails" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Missing K9! magic number" + +printf 'K9!\n# SPDX-License-Identifier: MPL-2.0\n{}\n' > "$TEST_ROOT/scan/component.k9" +expect_status "missing component pedigree still fails" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Missing pedigree block" + +sed '/name =/d' "$TEST_ROOT/valid.k9" > "$TEST_ROOT/scan/component.k9" +expect_status "missing pedigree name still fails" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Pedigree block missing 'name'" + +sed "s/'Kennel/'Invalid/" "$TEST_ROOT/valid.k9" > "$TEST_ROOT/scan/component.k9" +expect_status "invalid security level still fails" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Invalid security level" + +sed "s/'Kennel/'Hunt/" "$TEST_ROOT/valid.k9" > "$TEST_ROOT/scan/component.k9" +expect_status "Hunt without signature declaration still fails" 1 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Hunt-level K9 file must include" +sed -i '/leash =/a\ signature_required = true,' "$TEST_ROOT/scan/component.k9" +expect_status "Hunt with signature requirement is accepted" 0 env INPUT_PATH=scan INPUT_STRICT=true bash "$VALIDATOR" + +sed '/SPDX-License-Identifier/d' "$TEST_ROOT/valid.k9" > "$TEST_ROOT/scan/component.k9" +expect_status "non-strict warning remains advisory" 0 env INPUT_PATH=scan bash "$VALIDATOR" +expect_log "Missing SPDX-License-Identifier" +expect_status "strict mode still promotes warnings" 1 env INPUT_PATH=scan INPUT_STRICT=true bash "$VALIDATOR" + +expect_status "explicit paths-ignore remains supported" 0 env INPUT_PATH=scan INPUT_STRICT=true INPUT_PATHS_IGNORE=component.k9 bash "$VALIDATOR" +expect_log "Skipped 1 file(s) matching paths-ignore" + +echo "K9 validation regression tests passed." From d6f02955762dbb26ec88548bd8387030ca37a597 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:37:30 +0000 Subject: [PATCH 08/16] fix(ci): correct K9 metadata validation, allow required root files, and install just via pinned Cargo fallback --- .github/hooks/validate-k9.sh | 29 ++++- .machine_readable/root-allow.txt | 2 + .machine_readable/svc/k9/README.adoc | 6 + .../svc/k9/methodology-guard.k9.ncl | 14 +++ build/setup.sh | 23 ++-- container/deploy.k9.ncl | 112 +++++++++--------- tests/k9_validation_test.sh | 66 +++++++++++ tests/setup_install_test.sh | 61 ++++++++++ 8 files changed, 249 insertions(+), 64 deletions(-) create mode 100644 tests/k9_validation_test.sh create mode 100644 tests/setup_install_test.sh diff --git a/.github/hooks/validate-k9.sh b/.github/hooks/validate-k9.sh index c83e290..4306337 100755 --- a/.github/hooks/validate-k9.sh +++ b/.github/hooks/validate-k9.sh @@ -4,7 +4,9 @@ # # validate-k9.sh — K9 configuration file validation script # -# Scans for .k9 and .k9.ncl files and validates: +# Scans K9-SVC .k9 and .k9.ncl files and validates: +# The two legacy YAML session bindings documented in EXPLAINME.adoc and +# session/README.adoc are a separate format, outside this SVC validator. # 1. K9! magic number on line 1 # 2. Pedigree block presence with required fields (name, version) # 3. Security level is one of: kennel, yard, hunt (case-insensitive) @@ -26,6 +28,8 @@ set -euo pipefail # --------------------------------------------------------------------------- SCAN_PATH="${INPUT_PATH:-.}" +SCAN_PATH="${SCAN_PATH%/}" +SCAN_PATH="${SCAN_PATH:-/}" STRICT="${INPUT_STRICT:-false}" PATHS_IGNORE_RAW="${INPUT_PATHS_IGNORE:-}" GITHUB_OUTPUT_FILE="${GITHUB_OUTPUT:-/dev/null}" @@ -53,6 +57,25 @@ path_ignored() { return 1 } +# Recognise only the repo's two documented legacy session bindings, by +# relative path AND their YAML section markers. Other .k9 files still require +# the SVC header and pedigree. A K9! marker always opts into SVC validation. +legacy_session_binding() { + local file="$1" relative="${1#"$SCAN_PATH"/}" + if grep -q '^K9!$' "$file"; then + return 1 + fi + case "$relative" in + coordination.k9) + grep -q '^session_management:' "$file" && grep -q '^signals:' "$file" + ;; + session/custom-checks.k9) + grep -q '^version:' "$file" && grep -q '^checks:' "$file" + ;; + *) return 1 ;; + esac +} + # Counters FILES_SCANNED=0 ERRORS=0 @@ -306,6 +329,10 @@ for _f in "${k9_candidates[@]}"; do SKIPPED=$((SKIPPED + 1)) continue fi + if legacy_session_binding "$_f"; then + echo "::notice file=${_f}::Legacy YAML session binding; not a K9-SVC component (see session/README.adoc)" + continue + fi k9_files+=("$_f") done diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index ebc6adb..48066d4 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -16,6 +16,8 @@ README.adoc README.md # GitHub landing page (.md renders on GitHub/Glama; see PR #35) AUDIT.adoc EXPLAINME.adoc +ARCHITECTURE.adoc # Repository layout required by the Central Estate Required Files gate. +MAINTAINERS # Conventional owner record required by the Central Estate audit. 0-AI-MANIFEST.a2ml # thin pointer to .machine_readable/0.1-AI-MANIFEST.a2ml LICENSE LICENSES/ # REUSE-convention license texts (MPL-2.0, CC-BY-SA-4.0) diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc index 005ce58..8582947 100644 --- a/.machine_readable/svc/k9/README.adoc +++ b/.machine_readable/svc/k9/README.adoc @@ -7,6 +7,12 @@ K9 contractiles are self-validating components that combine configuration, validation, and deployment logic in a single file format. They implement the RSR principle of "self-describing artifacts" by embedding contracts and orchestration directly in the component. +The K9-SVC metadata gate (`bash .github/hooks/validate-k9.sh`) checks the +`K9!` header, pedigree and security metadata. The legacy YAML session bindings +`coordination.k9` and `session/custom-checks.k9`, documented in +`session/README.adoc`, use a separate format. The gate reports these separately; +it does not validate their YAML syntax or migrate their session protocol. + == The Three Security Levels K9 components declare their trust requirements using "The Leash" security model: diff --git a/.machine_readable/svc/k9/methodology-guard.k9.ncl b/.machine_readable/svc/k9/methodology-guard.k9.ncl index 6bd7c4a..650f5f7 100644 --- a/.machine_readable/svc/k9/methodology-guard.k9.ncl +++ b/.machine_readable/svc/k9/methodology-guard.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -8,6 +9,19 @@ # Usage: k9 validate methodology-guard let methodology_guard = { + pedigree = { + schema_version = "1.0.0", + metadata = { + name = "methodology-guard", + version = "1.0.0", + }, + security = { + leash = 'Yard, + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + }, name = "methodology-guard", version = "1.0.0", description = "Validates that agent work respects declared methodology constraints", diff --git a/build/setup.sh b/build/setup.sh index cdc1639..2a6f892 100755 --- a/build/setup.sh +++ b/build/setup.sh @@ -6,9 +6,8 @@ # Then hands off to `just setup` for project-specific configuration. # # Usage: -# curl -fsSL https://raw.githubusercontent.com/hyperpolymath/bofj-kitt/main/setup.sh | sh -# # or after cloning: -# ./setup.sh +# # After cloning and reviewing this script: +# sh build/setup.sh # # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) @@ -129,6 +128,16 @@ detect_platform() { } # ── Install just ── +# Use the repository's documented Cargo route when a system package is absent. +# Cargo checks registry package checksums; --locked uses the release lockfile. +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.40.0 --locked +} + install_just() { if command -v just >/dev/null 2>&1; then ok "just already installed: $(just --version 2>/dev/null | head -1)" @@ -140,8 +149,8 @@ install_just() { case "$PKG_MGR" in dnf) sudo dnf install -y just ;; apt) sudo apt-get install -y just 2>/dev/null || { - # just not in older apt repos — use installer - curl -fsSL https://just.systems/install.sh | bash -s -- --to /usr/local/bin + # just is absent from some older apt repositories. + install_just_with_cargo } ;; pacman) sudo pacman -S --noconfirm just ;; apk) sudo apk add just ;; @@ -152,8 +161,8 @@ install_just() { guix) guix install just ;; nix) nix-env -iA nixpkgs.just ;; *) - info "Using just installer script..." - curl -fsSL https://just.systems/install.sh | bash -s -- --to /usr/local/bin + info "Installing just with Cargo..." + install_just_with_cargo ;; esac diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index 5e6a6e0..c8afa9e 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # deploy.k9.ncl — bofj-kitt deployment component (Hunt level) # @@ -12,61 +13,6 @@ # k9-svc validate container/deploy.k9.ncl # k9-svc deploy container/deploy.k9.ncl --env production -# The component's pedigree (self-description across five layers) -let component_pedigree = { - # ───────────────────────────────────────────────────────────── - # L1: The Snout — Identity - # ───────────────────────────────────────────────────────────── - metadata = { - name = "{{SERVICE_NAME}}-deploy", - version = "{{VERSION}}", - breed = "application/vnd.k9+nickel", - magic_number = "K9!", - description = "bofj-kitt deployment component (Hunt level)", - }, - - # ───────────────────────────────────────────────────────────── - # L2: The Scent — Target Environment - # ───────────────────────────────────────────────────────────── - target = { - os = 'Linux, - is_edge = false, - requires_podman = true, - min_memory_mb = 256, - }, - - # ───────────────────────────────────────────────────────────── - # L3: The Leash — Security - # ───────────────────────────────────────────────────────────── - security = { - trust_level = 'Hunt, - allow_network = true, - allow_filesystem_write = true, - allow_subprocess = true, - # In production, replace with a real Ed25519 signature. - signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", - }, - - # ───────────────────────────────────────────────────────────── - # L4: The Gut — Self-Validation - # ───────────────────────────────────────────────────────────── - validation = { - checksum = "sha256:placeholder", - pedigree_version = "1.0.0", - hunt_authorized = false, # Must be set true after handshake - }, - - # ───────────────────────────────────────────────────────────── - # L5: The Muscle — Deployment Recipes - # ───────────────────────────────────────────────────────────── - recipes = { - install = "just container-build", - validate = "just container-verify", - deploy = "just container-up", - migrate = "just container-build && just container-up", - }, -} in - # Deployment configuration let deployment = { # Target environments (dev / staging / production) @@ -143,7 +89,61 @@ echo "K9: Rollback complete." # Export the component { - pedigree = component_pedigree, + # The component's pedigree (self-description across five layers) + pedigree = { + # ───────────────────────────────────────────────────────────── + # L1: The Snout — Identity + # ───────────────────────────────────────────────────────────── + metadata = { + name = "{{SERVICE_NAME}}-deploy", + version = "{{VERSION}}", + breed = "application/vnd.k9+nickel", + magic_number = "K9!", + description = "bofj-kitt deployment component (Hunt level)", + }, + + # ───────────────────────────────────────────────────────────── + # L2: The Scent — Target Environment + # ───────────────────────────────────────────────────────────── + target = { + os = 'Linux, + is_edge = false, + requires_podman = true, + min_memory_mb = 256, + }, + + # ───────────────────────────────────────────────────────────── + # L3: The Leash — Security + # ───────────────────────────────────────────────────────────── + security = { + leash = 'Hunt, + trust_level = 'Hunt, + allow_network = true, + allow_filesystem_write = true, + allow_subprocess = true, + # In production, replace with a real Ed25519 signature. + signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT", + }, + + # ───────────────────────────────────────────────────────────── + # L4: The Gut — Self-Validation + # ───────────────────────────────────────────────────────────── + validation = { + checksum = "sha256:placeholder", + pedigree_version = "1.0.0", + hunt_authorized = false, # Must be set true after handshake + }, + + # ───────────────────────────────────────────────────────────── + # L5: The Muscle — Deployment Recipes + # ───────────────────────────────────────────────────────────── + recipes = { + install = "just container-build", + validate = "just container-verify", + deploy = "just container-up", + migrate = "just container-build && just container-up", + }, + }, deployment = deployment, scripts = scripts, diff --git a/tests/k9_validation_test.sh b/tests/k9_validation_test.sh new file mode 100644 index 0000000..ca43ef6 --- /dev/null +++ b/tests/k9_validation_test.sh @@ -0,0 +1,66 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Regression checks for K9-SVC validation alongside legacy session bindings. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +fixture_root="$(mktemp -d)" +trap 'rm -rf "$fixture_root"' EXIT +mkdir -p "$fixture_root/session" +cp "$repo_root/coordination.k9" "$fixture_root/coordination.k9" +cp "$repo_root/session/custom-checks.k9" "$fixture_root/session/custom-checks.k9" +cp "$repo_root/.machine_readable/svc/k9/template-kennel.k9.ncl" "$fixture_root/component.k9" + +validate() { + INPUT_PATH="$fixture_root/" INPUT_STRICT=true \ + bash "$repo_root/.github/hooks/validate-k9.sh" > "$fixture_root/result.log" +} + +expect_failure() { + if validate; then + echo "FAIL: $1 unexpectedly passed" >&2 + exit 1 + fi + grep -qF "$2" "$fixture_root/result.log" +} + +# The integration files coexist with SVC components, without changing YAML. +validate +grep -qF 'Files scanned: 1' "$fixture_root/result.log" + +# Unknown .k9 files cannot claim the legacy session exception. +cp "$fixture_root/coordination.k9" "$fixture_root/unrecognised.k9" +expect_failure 'unknown YAML file' 'Missing K9! magic number' +rm "$fixture_root/unrecognised.k9" + +# A recognised name alone cannot exempt an incomplete binding. +cp "$fixture_root/coordination.k9" "$fixture_root/original.txt" +sed '/^signals:/d' "$fixture_root/original.txt" > "$fixture_root/coordination.k9" +expect_failure 'incomplete session binding' 'Missing K9! magic number' +mv "$fixture_root/original.txt" "$fixture_root/coordination.k9" + +# A SVC component at a session path must still be checked as SVC. +cp "$fixture_root/coordination.k9" "$fixture_root/original.txt" +{ + printf 'K9!\n' + cat "$fixture_root/original.txt" +} > "$fixture_root/coordination.k9" +expect_failure 'SVC without pedigree at session path' 'Missing pedigree block' +mv "$fixture_root/original.txt" "$fixture_root/coordination.k9" + +# Existing SVC guarantees remain enforced. +cp "$fixture_root/component.k9" "$fixture_root/original.txt" +sed '1d' "$fixture_root/original.txt" > "$fixture_root/component.k9" +expect_failure 'missing SVC header' 'Missing K9! magic number' +cp "$fixture_root/original.txt" "$fixture_root/component.k9" +sed '/name =/d' "$fixture_root/original.txt" > "$fixture_root/component.k9" +expect_failure 'missing pedigree identity' "Pedigree block missing 'name' field" +sed "s/leash = 'Kennel/leash = 'Invalid/" "$fixture_root/original.txt" > "$fixture_root/component.k9" +expect_failure 'invalid security level' 'Invalid security level' +sed "s/leash = 'Kennel/leash = 'Hunt/" "$fixture_root/original.txt" > "$fixture_root/component.k9" +expect_failure 'unsigned Hunt component' "Hunt-level K9 file must include a 'signature'" + +# The repository's real Nickel components also pass strict metadata checks. +INPUT_PATH="$repo_root" INPUT_STRICT=true \ + bash "$repo_root/.github/hooks/validate-k9.sh" > "$fixture_root/result.log" +echo 'PASS: K9 schema dispatch and security regressions' diff --git a/tests/setup_install_test.sh b/tests/setup_install_test.sh new file mode 100644 index 0000000..2513f22 --- /dev/null +++ b/tests/setup_install_test.sh @@ -0,0 +1,61 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Test installer fallback paths without networking or installing dependencies. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +fixture_root="$(mktemp -d)" +trap 'rm -rf "$fixture_root"' EXIT + +# Source the actual functions without running setup's main routine. +sed '/^main "\$@"$/d' "$repo_root/build/setup.sh" > "$fixture_root/functions.sh" + +for manager in apt unknown; do + FIXTURE_ROOT="$fixture_root" MANAGER="$manager" sh -eu <<'SH' +. "$FIXTURE_ROOT/functions.sh" +PKG_MGR="$MANAGER" +installed=false +command() { + case "$2" in + just) [ "$installed" = true ] ;; + cargo) return 0 ;; + *) return 1 ;; + esac +} +sudo() { return 1; } # Simulate an apt repository without just. +curl() { echo 'Unexpected download' >&2; exit 99; } +cargo() { + if [ "$*" != 'install just --version 1.40.0 --locked' ]; then + echo "Unexpected Cargo arguments: $*" >&2 + exit 98 + fi + installed=true +} +just() { printf 'just 1.40.0\n'; } +install_just +[ "$installed" = true ] +SH +done + +# No Cargo: return a failure without attempting remote shell execution. +FIXTURE_ROOT="$fixture_root" sh -eu <<'SH' +. "$FIXTURE_ROOT/functions.sh" +PKG_MGR=unknown +command() { return 1; } +curl() { echo 'Unexpected download' >&2; exit 99; } +if install_just; then + echo 'FAIL: installation without Cargo unexpectedly succeeded' >&2 + exit 1 +fi +SH + +# An already installed just must not trigger an installation. +FIXTURE_ROOT="$fixture_root" sh -eu <<'SH' +. "$FIXTURE_ROOT/functions.sh" +command() { [ "$2" = just ]; } +just() { printf 'just 1.40.0\n'; } +cargo() { echo 'Unexpected install' >&2; exit 99; } +sudo() { echo 'Unexpected install' >&2; exit 99; } +install_just +SH +echo 'PASS: setup uses verified package installation paths' From 35cbc000d1eea31bf606be62195fe1419d9a9607 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:38:00 +0000 Subject: [PATCH 09/16] docs(environments): clarify reachability probe classification and error handling --- tools/environments/probe-reachability.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index 9332c2c..047b4f2 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -38,7 +38,12 @@ if [ ! -r "$HOSTS_FILE" ]; then exit 2 fi -# classify — one word per outcome. +# classify — print one outcome label to stdout. +# Takes the final HTTP status after redirects and curl's exit code. Exit 60 +# yields tls-failed; any other non-zero exit or HTTP 000 yields unreachable, +# regardless of the HTTP status. With a zero exit, 401 yields auth-required, +# 403 yields refused, 2xx/3xx yields reachable, and all other codes yield +# http-. A failed probe is reported as a label, not an error status. classify() { local code="$1" rc="$2" if [ "$rc" -eq 60 ]; then From 8691de911e8eb865960e2c6070e0eced283dad7e Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 11:38:52 +0000 Subject: [PATCH 10/16] fix(proof-toolchain): add core prover smoke fixtures and installer, correct reachability claims, and tighten cartridge verification and sandbox contracts --- .../boj-prover-solver-cartridges.adoc | 40 ++++++++++++----- .../environment-of-environments.adoc | 35 ++++++++------- tools/environments/README.adoc | 3 ++ tools/environments/environments.kyaml | 4 +- tools/proof-toolchain/DESIGN.adoc | 45 ++++++++++++------- tools/proof-toolchain/install-smoke.sh | 16 +++++++ tools/proof-toolchain/smoke/acl2-smoke.lisp | 8 ++++ tools/proof-toolchain/smoke/hol-light-refl.sh | 19 ++++++++ tools/proof-toolchain/smoke/hol4-smoke.sml | 8 ++++ tools/proof-toolchain/smoke/smoke.miz | 11 +++++ tools/proof-toolchain/toolchain.kyaml | 8 ++-- 11 files changed, 147 insertions(+), 50 deletions(-) create mode 100644 tools/proof-toolchain/install-smoke.sh create mode 100644 tools/proof-toolchain/smoke/acl2-smoke.lisp create mode 100644 tools/proof-toolchain/smoke/hol-light-refl.sh create mode 100644 tools/proof-toolchain/smoke/hol4-smoke.sml create mode 100644 tools/proof-toolchain/smoke/smoke.miz diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index 4d86560..984b3a2 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -92,11 +92,14 @@ and, where the backend produces one, a certificate. |`provers_list` |The provers this host can dispatch, read from the capability record (`PRESENT` entries only), each with its echidna `ProverKind` slug, role -under PROOF-POLICY, version and lock hash. Never a hard-coded count. +under PROOF-POLICY, version and lock hash. `DRIFT` entries are not +dispatchable and are excluded, as are `UNAVAILABLE` entries. Never a +hard-coded count. |`provers_check` -|One prover: present, version, drift against the lock, or the reason it -is unavailable. +|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. |`provers_prove` |`{file \| goal, prover?, timeout}` → `{verdict, trust_level, prover, @@ -130,6 +133,13 @@ a bounded model-checking result with its bounds. Solver results are `TESTED` with bounds or `PROVEN` with a checked certificate, never 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 +successful check result, and any axioms used. An emitted certificate or +unsat core alone does not establish `PROVEN`. + [cols="1,3",options="header"] |=== |Tool |Contract @@ -140,12 +150,15 @@ entries (Z3, CVC5, Yices, Alt-Ergo, E, Vampire). |`solvers_sat` |`{problem, format, solver?, want: model \| unsat_core \| certificate}` → -the requested artefact plus timing. Portfolio across Z3, CVC5 and Alt-Ergo +the requested artefact plus timing, explicit status and the metadata +defined above. Portfolio across Z3, CVC5 and Alt-Ergo with disagreement flagged, as echidna's `portfolio.rs` does. |`solvers_optimise` |MiniZinc, Chuffed, OR-Tools, GLPK, SCIP: objective, bound, solution, -proof of optimality where the solver emits one. +proof of optimality where the solver emits one, plus timing, explicit +status and the metadata defined above. `PROVEN` requires the certificate +check to establish optimality for the reported objective and bound. |`solvers_model_check` |TLC, SPIN, NuSMV, Alloy, PRISM, Storm, UPPAAL, ProB: the property, the @@ -226,8 +239,9 @@ machine for no gain. lifecycle over them; all advertise from the capability record. |High. Each surface has one input kind and one answer kind; the roster is never typed by hand. -|High once the kit's `doctor` exists; until then the cartridges can run -against echidna's own `check-prover`. +|Depends on the kit's `doctor` producing `EnvCapability`; echidna's +`check-prover` is not a substitute. Only experiment Z3 (scaffolding and +static validation) may precede `doctor`. |High. Shield tier; sandboxed execution (echidna's Podman or bwrap executor, ADR-0009's local provider); no LLM in the verdict path. @@ -237,8 +251,9 @@ executor, ADR-0009's local provider); no LLM in the verdict path. prover" is the whole surface: no portfolio, no ledger, no solving, and the hard-coded "105". |Medium. Nothing to maintain beyond echidna. -|Medium. Inherits echidna's sandbox only if `echidna prove` is called with -it on. +|Shield tier required. Every cartridge invocation must run in the sandbox, +whether or not `echidna prove` receives a sandbox flag; refuse invocation +if the required sandbox executor is unavailable. |*C. One `formal-methods-mcp` mega-cartridge* |Every tool of A in one cartridge. @@ -337,10 +352,11 @@ agent relies on when it reads `trust_level: 5`. == Aspects Security:: The cartridges execute untrusted proof and problem files. -Shield tier; every dispatch runs under echidna's sandbox (Podman +Shield tier; every cartridge invocation runs under echidna's sandbox (Podman `--network=none`, read-only, limits; bwrap fallback; the unsandboxed mode -refused rather than defaulted). ADR-0009's `sandbox-mcp` local provider is -the same mechanism once it exists. +refused regardless of any `echidna prove` sandbox flag). If the required +sandbox executor is unavailable, refuse to run. ADR-0009's `sandbox-mcp` +local provider is the same mechanism once it exists. Privacy:: Proof content can be proprietary. The verdict path has no network egress and no LLM; `echidna-llm-mcp` stays a separate, opt-in cartridge. Receipts carry hashes, not content. diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index 8b74e74..2f3c932 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/docs/proposals/environment-of-environments.adoc @@ -51,8 +51,8 @@ backends; covers 7 of echidna's 12 core backends (see <>). |One relocatable bundle at `/opt/hyperpolymath/provers`, `provers.sh install\|doctor\|render` |Design only. Its statements about what agent sessions can reach were not -measured; <> confirms the asset transport and contradicts the -opam and Alire claim. +measured; <> confirms HEAD reachability of the asset path and +contradicts the opam and Alire claim for that session. |`tools/workstation/env.sh` |Toolchain homes and `PATH` for one workstation @@ -80,8 +80,10 @@ so, not pass silently. 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). HEAD or GET to the root of each host; the code is what the -proxy returned. +agent proxy). The probe sends redirected HEAD requests to the URLs in +`tools/environments/hosts.txt`; the code is the final response the proxy +returned. The registry GET codes below are separate manual measurements, +not output from `probe-reachability.sh`. [cols="3,1,3",options="header"] |=== @@ -95,12 +97,12 @@ proxy returned. |`isabelle.in.tum.de`, `mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable. |`ftp.gnu.org/gnu/guix` |200 |Reachable. |`smt-lib.org`, `www.tptp.org` |200 |Reachable. -|`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 |*Reachable.* The asset download path redirects to `release-assets.githubusercontent.com` and the bytes are served. DESIGN.adoc's "release asset first" transport holds here. +|`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 (HEAD) |*Reachable.* The HEAD request redirects to `release-assets.githubusercontent.com` and succeeds. No asset body was downloaded or executable run; bundle transport remains unverified. |`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files). |`github.com/Z3Prover/z3/releases/latest` |403 |*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 |Refused. Release discovery through the API is not available either. |`crates.io/api/v1/crates/just` |403 |Refused (cargo installs from the registry would fail). -|`ghcr.io/v2/`, `cgr.dev/v2/` |401 (GET), 405 (HEAD) |Registry answered; anonymous token flow not tested. +|`ghcr.io/v2/`, `cgr.dev/v2/` |401 (manual GET), 405 (probe HEAD) |Registry answered; anonymous token flow not tested. |`cvc5.github.io` |200 |Reachable. |`www.cs.utexas.edu/~moore/acl2/` |TLS failure |Host certificate not in the session CA bundle. |=== @@ -116,14 +118,14 @@ Two conclusions follow, and both change the design: . *Reachability is a property of an environment instance, not of its class, and of a path, not of a host.* The same "agent session" class - reached opam here, which the design assumed it could not; it fetched a - concrete release asset, which the design assumed and which holds; and it - could not reach the release landing page or the API, so a `pin: - resolve` entry (which discovers "latest" through the API) cannot be - resolved from a session. The lock must carry the concrete asset URL, - and `install` must read the lock, never the API. The kit must measure, - not assume: `doctor` grows a `probe` that records which paths answered, - and the capability report carries it. + reached opam here, which the design assumed it could not; a redirected + HEAD request to a concrete release asset succeeded, without measuring a + download; and it could not reach the release landing page or the API, + so a `pin: resolve` entry (which discovers "latest" through the API) + cannot be resolved through those paths in this session. The lock must + carry the concrete asset URL, and `install` must read the lock, never + the API. The kit must measure, not assume: `doctor` grows a `probe` that + records which paths answered, and the capability report carries it. . *Execution policy is a second axis beside network policy.* An environment may be able to fetch a bundle and still be forbidden to run it. The environment declaration needs an `execute-downloaded` field, and @@ -217,8 +219,9 @@ sealed-container concern, per the 2026-05-18 packaging ruling. |=== E6 was decided on 2026-10-27: the four entries above are in the manifest -with `resolve` or `resolve-stable` pins and smoke fixtures that land with -the bundle build, so the kit now declares eleven of echidna's twelve core +with `resolve` or `resolve-stable` pins and smoke fixtures under +`tools/proof-toolchain/smoke/`, installed before verification by the bundle +build, so the kit now declares eleven of echidna's twelve core backends and names the twelfth's home. == Options compared diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index 18b0646..95165d7 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -47,6 +47,9 @@ A probe of a GitHub release *landing page* or of `api.github.com` says nothing about release *assets*: the asset download path redirects to `release-assets.githubusercontent.com`, which the probe follows separately. Record the asset outcome, not the landing page's. +Successful HEAD reachability does not establish that asset bytes were +downloaded or an executable ran. Record GET or download results separately +as manual measurements; the probe does not produce them. A block is a fact about one environment instance on one date. It is never copied from one environment class to another. diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml index d71fccf..21b313b 100644 --- a/tools/environments/environments.kyaml +++ b/tools/environments/environments.kyaml @@ -14,7 +14,7 @@ # policy (decided per instance; the probe records what it found) # container-runtime podman | docker | none # report who reads this environment's capability record -# measured dated facts from a probe run; never typed by hand +# measured dated probe facts; manual measurements labelled separately { schema: 1, policy: "standards 3-practice/PROOF-POLICY.adoc §6; 3-practice/provisioning/PROVISIONING-STANDARD.adoc", @@ -22,7 +22,7 @@ record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, environments: [ {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, - {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (22 URLs, every one probed)", reachable: ["github.com release asset download (302 to release-assets.githubusercontent.com, then 200)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest)", "api.github.com", "crates.io"], registry-answered: ["ghcr.io (GET 401, HEAD 405)", "cgr.dev (GET 401, HEAD 405)"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed"}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (21 URLs, every one probed)", reachable: ["github.com release asset HEAD (302 to release-assets.githubusercontent.com, then 200)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest)", "api.github.com", "crates.io"], registry-answered: ["ghcr.io (manual GET 401, probe HEAD 405)", "cgr.dev (manual GET 401, probe HEAD 405)"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed"}}, {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index e1acc87..9b4da16 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -9,17 +9,19 @@ obligation is decided by `3-practice/PROOF-POLICY.adoc` in `standards`; this kit decides how those tools get onto a machine and how a machine reports which of them it has. -Status: design, not built. Nothing here installs anything yet; the build -steps are in <>. +Status: design, not built. The core smoke-fixture installer exists; tool +installation and the bundle build remain planned in <>. See also `../environments/` and `docs/proposals/environment-of-environments.adoc`: the environment classes this toolchain is projected onto, with measured reachability. Those measurements (2026-10-27) refine the assumptions below: the agent session -probed there *could* reach `opam.ocaml.org` and `alire.ada.dev`; it -*could* fetch a concrete GitHub release asset, as assumed; and it *could -not* reach release landing pages or `api.github.com`, so a `pin: -resolve` entry cannot be resolved from a session and `install` must read +probed there *could* reach `opam.ocaml.org`, `alire.ada.dev` and the tested +GitHub source archive URL. A redirected HEAD request to a concrete GitHub +release asset succeeded; downloading its body and running it were not +observed. That session *could not* reach the tested release landing page +or `api.github.com`, so a `pin: resolve` entry cannot be resolved through +those paths in that session and `install` must read the concrete asset URL from the lock. Reachability is measured per environment and per path, not assumed per class. @@ -32,10 +34,12 @@ differently: through rustup, cargo, elan, pack, Alire and opam, with full network. It works, but nothing records which versions it holds. * *Online agent sessions* (Claude Code cloud sessions, claude.ai skills) - cannot reach `opam.ocaml.org`, `alire.ada.dev`, or GitHub source - archives. They can reach GitHub *release assets*. So Creusot's Why3 back - ends, Lambdapi, Dedukti, agda2dedukti and Idris2 cannot be built there at - all, and every session that needs them fails or reports a leg it never ran. + were initially assumed unable to reach `opam.ocaml.org`, `alire.ada.dev` + or GitHub source archives, with only GitHub release assets reachable. + The 2026-10-27 probes above contradict the first three assumptions for + that session. Whether Creusot's Why3 back ends, Lambdapi, Dedukti, + agda2dedukti or Idris2 can be built depends on each session's measured + paths, dependencies and execution policy; no build was tested there. * *CI runners* have the network but not the time: a cold opam build of Creusot's back ends or of agda2dedukti costs tens of minutes per job. * *Dispatchers* (echidna, echidnabot, proof-burrower) need binaries at known @@ -68,12 +72,17 @@ SHA-256 of the produced bundle and image digest. Never hand-edited. `/opt/hyperpolymath/provers`, then publishes `provers--x86_64-linux.tar.zst` as a GitHub release asset of this repo and an OCI image (Wolfi base) containing the same tree, both pinned in the -lock. +lock. Before any verification, the build must run +`sh tools/proof-toolchain/install-smoke.sh /opt/hyperpolymath/provers` +from the checkout root to install the four core-backend fixtures under +`$PREFIX/share/smoke/`; an installation failure stops the build. |`provers.sh install` |Fetches the bundle named in the lock, checks its SHA-256, and unpacks it at the prefix. The same command serves the workstation, a session's setup -script, and a CI job. A release asset is reachable from all three. +script, and a CI job, where network and execution policy permit. The +2026-10-27 session measured HEAD reachability only; bundle download and +execution must be checked separately on each supported target. |`provers.sh doctor` |Reports each manifest entry as `PRESENT `, `DRIFT != `, @@ -114,10 +123,11 @@ The lock records the builder image digest and the glibc minimum. === Why a release asset first, image second -Agent sessions can download a release asset but usually cannot run a -container engine. CI and the dispatchers can run containers. So the tarball -is the primary artefact and the image wraps the same tree, rather than the -other way round. +The 2026-10-27 agent session reached a release asset with HEAD, while its +download-and-run experiment was denied before download. The tarball targets +sessions whose network and execution policies allow it; a successful HEAD +alone does not establish that. CI and the dispatchers can run containers. +The tarball is the primary artefact and the image wraps the same tree. == The closure rule @@ -190,7 +200,8 @@ that shares the name; the manifest names it `echidna-solidity` if it stays. . `provers.sh doctor`, text and JSON. Useful at once on the workstation, before any bundle exists. . The bundle build workflow and `provers.sh install`. It produces the first - release asset and image and writes the lock. + release asset and image and writes the lock. Run `install-smoke.sh` as + specified above before the manifest's `verify` commands. . Consumers: the session setup-script snippet, the CI usage pattern, the echidna capability read, and proof-craft's switch to `provers.sh`. diff --git a/tools/proof-toolchain/install-smoke.sh b/tools/proof-toolchain/install-smoke.sh new file mode 100644 index 0000000..fd3ee1e --- /dev/null +++ b/tools/proof-toolchain/install-smoke.sh @@ -0,0 +1,16 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# Install core-backend smoke inputs before the bundle's verify phase. +set -eu + +if [ "$#" -ne 1 ] || [ -z "$1" ]; then + echo "usage: sh install-smoke.sh PREFIX" >&2 + exit 2 +fi + +smoke_dir="$(CDPATH='' cd -- "$(dirname -- "$0")/smoke" && pwd)" +destination="$1/share/smoke" +install -d "$destination" +for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz; do + install -m 644 "$smoke_dir/$fixture" "$destination/$fixture" +done diff --git a/tools/proof-toolchain/smoke/acl2-smoke.lisp b/tools/proof-toolchain/smoke/acl2-smoke.lisp new file mode 100644 index 0000000..2751204 --- /dev/null +++ b/tools/proof-toolchain/smoke/acl2-smoke.lisp @@ -0,0 +1,8 @@ +; SPDX-License-Identifier: MPL-2.0 +(in-package "ACL2") + +; LD returns a proof error instead of continuing to a successful exit. +(mv-let (erp val state) + (ld '((defthm bofj-smoke-reflexivity (equal x x) :rule-classes nil)) + :ld-error-action :return) + (mv (good-bye (if (and (not erp) (eq val :eof)) 0 1)) state)) diff --git a/tools/proof-toolchain/smoke/hol-light-refl.sh b/tools/proof-toolchain/smoke/hol-light-refl.sh new file mode 100644 index 0000000..97acebc --- /dev/null +++ b/tools/proof-toolchain/smoke/hol-light-refl.sh @@ -0,0 +1,19 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# A toplevel can exit zero after a proof error: require a checked theorem. +set -eu + +transcript="$(mktemp)" +trap 'rm -f "$transcript"' EXIT +trap 'exit 1' HUP INT TERM +prover_exit=0 +hol_light >"$transcript" 2>&1 <<'EOF' || prover_exit=$? +let smoke = REFL `T`;; +if concl smoke = `T = T` then + print_endline "\nBOFJ_HOL_LIGHT_SMOKE_OK" +else failwith "reflexivity smoke failed";; +EOF +if [ "$prover_exit" -ne 0 ] || ! grep -qx 'BOFJ_HOL_LIGHT_SMOKE_OK' "$transcript"; then + cat "$transcript" >&2 + exit 1 +fi diff --git a/tools/proof-toolchain/smoke/hol4-smoke.sml b/tools/proof-toolchain/smoke/hol4-smoke.sml new file mode 100644 index 0000000..b78e06e --- /dev/null +++ b/tools/proof-toolchain/smoke/hol4-smoke.sml @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Check a kernel theorem and propagate proof failures to the caller. *) +val _ = + ((if aconv (concl (REFL ``T``)) ``T = T`` then + OS.Process.exit OS.Process.success + else + OS.Process.exit OS.Process.failure) + handle _ => OS.Process.exit OS.Process.failure); diff --git a/tools/proof-toolchain/smoke/smoke.miz b/tools/proof-toolchain/smoke/smoke.miz new file mode 100644 index 0000000..a1389a7 --- /dev/null +++ b/tools/proof-toolchain/smoke/smoke.miz @@ -0,0 +1,11 @@ +:: SPDX-License-Identifier: MPL-2.0 +environ + +begin + +theorem + for x being object holds x = x +proof + let x be object; + thus thesis; +end; diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml index c9b25ca..3c2c20b 100644 --- a/tools/proof-toolchain/toolchain.kyaml +++ b/tools/proof-toolchain/toolchain.kyaml @@ -15,6 +15,8 @@ # field, and every run must pass, so one missing toolchain fails the entry. # Smoke fixtures named by verify commands live in smoke/ beside this file and # are installed to $PREFIX/share/smoke/ by the bundle build. +# For hol-light, hol4, acl2 and mizar, run `sh install-smoke.sh "$PREFIX"` +# from this directory before verification (see DESIGN.adoc). { schema: 1, prefix: "/opt/hyperpolymath/provers", @@ -43,9 +45,9 @@ {id: "tlc", role: "exception:recorded", method: "release asset (tlaplus tla2tools.jar) plus a bundled tlc launcher (java -cp $PREFIX/lib/tla/tla2tools.jar tlc2.TLC, absolute so it runs from any directory)", pin: "resolve-stable", verify: "tlc -h", needs: ["jre"], notes: "pin a stable tagged release with its sha256 in the lock; v1.8.0 is a rolling prerelease rebuilt on every master commit"}, {id: "jre", role: "runtime", method: "release asset (Eclipse Temurin JRE, Java 17 or later)", pin: "resolve-stable", verify: "java -version", notes: "bundled so the tlc launcher does not depend on a host Java"}, {id: "isabelle", role: "exception:recorded", method: "release asset", pin: "resolve", verify: "isabelle version", notes: "supplementary evidence only"}, - {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and checks the theorem echo; it lands with the bundle build. Supplementary evidence only, as Isabelle"}, - {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly --version", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, - {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure; it lands with the bundle build. Supplementary evidence only"}, + {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"}, + {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, + {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure. Supplementary evidence only"}, {id: "sbcl", role: "runtime", method: "release asset (sbcl/sbcl Linux x86_64 binary)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 is built on; bundled so acl2 does not depend on a host Lisp"}, {id: "acl2", role: "exception:recorded", method: "release asset (acl2/acl2 tagged source) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books are not bundled; a consumer that needs them records that as its own entry. The upstream download host failed TLS from one agent session (environments.kyaml), so the bundle build fetches it, not the session. Supplementary evidence only"}, {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML)", pin: "resolve-stable", verify: "makeenv $PREFIX/share/smoke/smoke.miz && verifier $PREFIX/share/smoke/smoke.miz", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. Supplementary evidence only"}, From 2aa18487614afb10fa89fe85b25514ee506a3dbd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 14:00:23 +0000 Subject: [PATCH 11/16] fix(proof-toolchain): add PVS, correct SBCL/ACL2 sources, self-contained Mizar smoke, GET probe - toolchain.kyaml: PVS joins as a BSD-3-Clause source build on the bundled SBCL, so the kit declares all twelve of echidna's core backends. SBCL comes from its official x86-64 Linux binary distribution (sbcl.org's platform table, served from SourceForge); ACL2 from its tagged GitHub source via codeload, with the stale utexas TLS reasoning removed. - smoke: mizar-smoke.sh sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file; pvs-smoke.sh and pvs_smoke.pvs prove one lemma with proveit and require the success summary. install-smoke.sh installs both. tests/proof_smoke_wrappers_test.sh checks the installer and both wrappers against stub provers. - probe-reachability.sh: --get sends a one-byte ranged GET. Re-measured all 22 hosts with HEAD and GET: the three refusals (release landing page, api.github.com, crates.io) are 403 to GET too; only the registries differ (HEAD 405, GET 401). Docs and the measured block say which method produced each code. - build/setup.sh: the Cargo fallback pins just 1.56.0, the estate mise.lock version, above the just >= 1.42 floor (1.40.0 was below it). - SPDX MPL-2.0 on the remaining new files, per the repository rule. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- CHANGELOG.adoc | 28 +++++-- build/setup.sh | 4 +- .../awesome-estate-maths-proving.adoc | 2 +- .../boj-prover-solver-cartridges.adoc | 6 +- .../environment-of-environments.adoc | 55 +++++++------ tests/proof_smoke_wrappers_test.sh | 79 +++++++++++++++++++ tests/setup_install_test.sh | 6 +- tools/environments/README.adoc | 21 +++-- tools/environments/environments.kyaml | 2 +- tools/environments/hosts.txt | 6 +- tools/environments/probe-reachability.sh | 34 +++++--- tools/proof-toolchain/DESIGN.adoc | 23 +++--- tools/proof-toolchain/install-smoke.sh | 3 +- tools/proof-toolchain/smoke/mizar-smoke.sh | 35 ++++++++ tools/proof-toolchain/smoke/pvs-smoke.sh | 20 +++++ tools/proof-toolchain/smoke/pvs_smoke.pvs | 11 +++ tools/proof-toolchain/toolchain.kyaml | 9 ++- 17 files changed, 271 insertions(+), 73 deletions(-) create mode 100755 tests/proof_smoke_wrappers_test.sh create mode 100644 tools/proof-toolchain/smoke/mizar-smoke.sh create mode 100644 tools/proof-toolchain/smoke/pvs-smoke.sh create mode 100644 tools/proof-toolchain/smoke/pvs_smoke.pvs diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 2b650b5..ef5f17a 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -23,11 +23,27 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. (`provers-mcp`, `solvers-mcp`, `code-verifiers-mcp`) on the capability record seam, what the store's `proof-mcp` becomes, and where Quintessence, Apodeixis.jl, atoma and bactarin land. -* `tools/proof-toolchain/toolchain.kyaml` — HOL Light, HOL4, ACL2 and - Mizar as `exception:recorded` entries, with Poly/ML and SBCL as their - bundled runtimes (E6, owner decision 2026-10-27): the kit now declares - eleven of echidna's twelve core backends; PVS stays in the - sealed-container tail. +* `tools/proof-toolchain/toolchain.kyaml` — HOL Light, HOL4, ACL2, Mizar + and PVS as `exception:recorded` entries, with Poly/ML and SBCL as their + bundled runtimes (E6, owner decision 2026-10-27; PVS added after review + showed its SBCL source build is BSD-3-Clause): the kit now declares all + twelve of echidna's core backends. Smoke fixtures and wrappers are under + `tools/proof-toolchain/smoke/`, installed by `install-smoke.sh` and + tested against stub provers by `tests/proof_smoke_wrappers_test.sh`. * `tools/environments/` — `environments.kyaml` (environment classes with a `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment - X1: HEAD-only reachability probe). + X1: reachability probe, HEAD by default, one-byte GET with `--get`). + +==== Changed + +* `build/setup.sh` — when no system package provides `just`, setup runs + `cargo install just --version 1.56.0 --locked` (the estate mise.lock pin, + above the `just` >= 1.42 floor) instead of piping a remote installer to + `bash`; covered by `tests/setup_install_test.sh`. +* `.github/hooks/validate-k9.sh` — skips the two YAML session bindings + (`coordination.k9`, `session/custom-checks.k9`) by file identity and + section markers rather than reporting them as malformed K9-SVC + components; `container/deploy.k9.ncl` and + `.machine_readable/svc/k9/methodology-guard.k9.ncl` gain the `K9!` magic + line and a pedigree block. The lasting fix is to migrate those bindings to + the k9-coordination grammar in `standards`. diff --git a/build/setup.sh b/build/setup.sh index 2a6f892..ab40d83 100755 --- a/build/setup.sh +++ b/build/setup.sh @@ -130,12 +130,14 @@ detect_platform() { # ── Install just ── # Use the repository's documented Cargo route when a system package is absent. # 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). 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.40.0 --locked + cargo install just --version 1.56.0 --locked } install_just() { diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc index 109d177..b9068a6 100644 --- a/docs/proposals/awesome-estate-maths-proving.adoc +++ b/docs/proposals/awesome-estate-maths-proving.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = Awesome lists for maths, proving and solving in the stuff-of-awe estate :toc: diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index 984b3a2..072d8f9 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -364,9 +364,9 @@ Honesty:: Every list is read from the capability record. A prover the host lacks is `UNAVAILABLE` with a reason, never a stub answer. The store's `available: true` must mean a process answered, which today it does not for `proof-mcp`. -Licensing:: PVS, Imandra and other non-free backends are dispatchable only -where installed; the cartridge reports them unavailable elsewhere and -never bundles them. +Licensing:: Imandra, SRI's Allegro build of PVS and other non-free +backends are dispatchable only where installed; the cartridge reports them +unavailable elsewhere and never bundles them. Observability:: Receipts hashed with BLAKE3 as echidna's certificates are; the kit lock's SHA-256 named per tool so a receipt pins the exact binary. diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index 2f3c932..11c48d6 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/docs/proposals/environment-of-environments.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = bofj-kitt as the environment of environments :toc: @@ -43,15 +43,16 @@ report its real capabilities in one machine-readable form. |Surface |What it declares |Gap |`tools/proof-toolchain/toolchain.kyaml` -|29 tools with roles under PROOF-POLICY, pins and smoke commands +|36 tools with roles under PROOF-POLICY, pins and smoke commands |Declares tools, not environments. Covers the policy provers and their -backends; covers 7 of echidna's 12 core backends (see <>). +backends. Before E6 it covered 7 of echidna's 12 core backends; it now +covers all 12 (see <>). |`tools/proof-toolchain/DESIGN.adoc` |One relocatable bundle at `/opt/hyperpolymath/provers`, `provers.sh install\|doctor\|render` |Design only. Its statements about what agent sessions can reach were not -measured; <> confirms HEAD reachability of the asset path and +measured; <> confirms HEAD and one-byte GET reachability of the asset path and contradicts the opam and Alire claim for that session. |`tools/workstation/env.sh` @@ -80,10 +81,11 @@ so, not pass silently. 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 sends redirected HEAD requests to the URLs in -`tools/environments/hosts.txt`; the code is the final response the proxy -returned. The registry GET codes below are separate manual measurements, -not output from `probe-reachability.sh`. +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). [cols="3,1,3",options="header"] |=== @@ -97,14 +99,15 @@ not output from `probe-reachability.sh`. |`isabelle.in.tum.de`, `mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable. |`ftp.gnu.org/gnu/guix` |200 |Reachable. |`smt-lib.org`, `www.tptp.org` |200 |Reachable. -|`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 (HEAD) |*Reachable.* The HEAD request redirects to `release-assets.githubusercontent.com` and succeeds. No asset body was downloaded or executable run; bundle transport remains unverified. +|`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). -|`github.com/Z3Prover/z3/releases/latest` |403 |*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 |Refused. Release discovery through the API is not available either. -|`crates.io/api/v1/crates/just` |403 |Refused (cargo installs from the registry would fail). -|`ghcr.io/v2/`, `cgr.dev/v2/` |401 (manual GET), 405 (probe HEAD) |Registry answered; anonymous token flow not tested. +|`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. +|`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. -|`www.cs.utexas.edu/~moore/acl2/` |TLS failure |Host certificate not in the session CA bundle. +|`downloads.sourceforge.net` (SBCL x86-64 Linux binary) |200 (HEAD), 206 (GET, one byte) |Reachable: the source the `sbcl` entry fetches. +|`www.cs.utexas.edu/~moore/acl2/` |TLS failure (HEAD and GET) |Host certificate not in the session CA bundle. The `acl2` entry fetches from GitHub instead, so this does not block it. |=== A second experiment, installing Z3 from that release asset into a scratch @@ -119,8 +122,8 @@ Two conclusions follow, and both change the design: . *Reachability is a property of an environment instance, not of its class, and of a path, not of a host.* The same "agent session" class reached opam here, which the design assumed it could not; a redirected - HEAD request to a concrete release asset succeeded, without measuring a - download; and it could not reach the release landing page or the API, + request to a concrete release asset succeeded and returned its first + byte, without measuring a full download; and it could not reach the release landing page or the API, so a `pin: resolve` entry (which discovers "latest" through the API) cannot be resolved through those paths in this session. The lock must carry the concrete asset URL, and `install` must read the lock, never @@ -190,10 +193,11 @@ promises and the first concrete BoJ integration surface (roadmap M2). === E6. Close the gap to echidna's core roster The kit covers the PROOF-POLICY provers. echidna's default API exposes a -core of 12 backends; the kit's manifest lacks 5 of them. Add HOL Light, -HOL4, ACL2 and Mizar as `exception:recorded` entries (PVS is a licensed -binary and goes in the sealed-container tail), so an environment the kit -provisions can serve echidna's whole core. The extended roster (141 +core of 12 backends; the kit's manifest lacked 5 of them. Add HOL Light, +HOL4, ACL2, Mizar and PVS as `exception:recorded` entries, so an +environment the kit provisions can serve echidna's whole core. PVS is +BSD-3-Clause and builds on SBCL; only SRI's Allegro build carries a +click-through licence, and the bundle does not use it. The extended roster (141 `ProverKind` variants over 105 implementation files) stays echidna's sealed-container concern, per the 2026-05-18 packaging ruling. @@ -213,16 +217,17 @@ sealed-container concern, per the 2026-05-18 packaging ruling. |Metamath |none needed |Pure-Rust, in-process in echidna |HOL Light |`hol-light` |Covered (added 2026-10-27 on the owner's decision; opam) |HOL4 |`hol4` with `polyml` |Covered (added 2026-10-27; source build on bundled Poly/ML) -|ACL2 |`acl2` with `sbcl` |Covered (added 2026-10-27; the bundle build fetches it, since its host failed TLS from a session) +|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) -|PVS |none |*Missing*, licensed binary: sealed-container tail +|PVS |`pvs` with `sbcl` |Covered (added 2026-10-27; BSD-3-Clause source build on bundled SBCL) |=== -E6 was decided on 2026-10-27: the four entries above are in the manifest +E6 was decided on 2026-10-27: the five entries above are in the manifest with `resolve` or `resolve-stable` pins and smoke fixtures under `tools/proof-toolchain/smoke/`, installed before verification by the bundle -build, so the kit now declares eleven of echidna's twelve core -backends and names the twelfth's home. +build, so the kit now declares all twelve of echidna's core backends. +None of the five has been built or run yet; they are declared, with +smoke checks, until the bundle build exists. == Options compared diff --git a/tests/proof_smoke_wrappers_test.sh b/tests/proof_smoke_wrappers_test.sh new file mode 100755 index 0000000..497e300 --- /dev/null +++ b/tests/proof_smoke_wrappers_test.sh @@ -0,0 +1,79 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Test the proof-toolchain smoke installer and the Mizar and PVS wrappers +# against stub prover binaries. This checks the wrappers' pass/fail logic and +# that they never write into the installed prefix; it does not run Mizar or PVS. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +work="$(mktemp -d)" +trap 'rm -rf "$work"' EXIT + +prefix="$work/prefix" +stubs="$work/stubs" +mkdir -p "$stubs" "$prefix/share/mizar" +sh "$repo_root/tools/proof-toolchain/install-smoke.sh" "$prefix" +for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz \ + 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 + +expect() { # expect pass|fail + local want="$1" what="$2"; shift 2 + if "$@" >/dev/null 2>&1; then got=pass; else got=fail; fi + if [ "$got" != "$want" ]; then + echo "FAIL: $what: expected $want, got $got" >&2 + exit 1 + fi +} + +# Stub Mizar: makeenv checks MIZFILES and the article path; verifier writes +# the .err file the mode under test asks for. +cat > "$stubs/makeenv" <<'SH' +#!/bin/sh +[ "$MIZFILES" = "$EXPECT_MIZFILES" ] && [ "$1" = text/smoke ] && [ -f text/smoke.miz ] +SH +cat > "$stubs/verifier" <<'SH' +#!/bin/sh +case "$STUB_MODE" in + ok) : > text/smoke.err ;; + errors) echo '5 7 4' > text/smoke.err ;; + no-err) : ;; + crash) exit 3 ;; +esac +SH +chmod +x "$stubs/makeenv" "$stubs/verifier" +mizar() { STUB_MODE="$1" EXPECT_MIZFILES="$prefix/share/mizar" MIZFILES=/host/mml \ + PATH="$stubs:$PATH" sh "$prefix/share/smoke/mizar-smoke.sh" "$prefix"; } +expect pass "mizar clean article" mizar ok +expect fail "mizar article errors" mizar errors +expect fail "mizar no error file" mizar no-err +expect fail "mizar verifier crash" mizar crash +expect fail "mizar missing PREFIX" sh "$prefix/share/smoke/mizar-smoke.sh" +expect fail "mizar missing MML" env PATH="$stubs:$PATH" STUB_MODE=ok \ + sh "$prefix/share/smoke/mizar-smoke.sh" "$work/no-such-prefix" + +# Stub PVS: proveit prints the summary the mode under test asks for. +cat > "$stubs/proveit" <<'SH' +#!/bin/sh +[ "$1" = --force ] && [ "$2" = pvs_smoke.pvs ] && [ -f pvs_smoke.pvs ] || exit 9 +mkdir -p pvsbin +case "$STUB_MODE" in + ok) echo 'Grand Totals: 1 proofs, 1 attempted, 1 succeeded (0.01 s)' ;; + unproved) echo 'Grand Totals: 1 proofs, 1 attempted, 0 succeeded (0.01 s)' ;; + silent) : ;; + crash) echo 'Grand Totals: 1 proofs, 1 attempted, 1 succeeded (0.01 s)'; exit 4 ;; +esac +SH +chmod +x "$stubs/proveit" +pvs() { STUB_MODE="$1" PATH="$stubs:$PATH" sh "$prefix/share/smoke/pvs-smoke.sh"; } +expect pass "pvs proved" pvs ok +expect fail "pvs unproved" pvs unproved +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" +echo 'PASS: smoke installer and Mizar/PVS wrappers' diff --git a/tests/setup_install_test.sh b/tests/setup_install_test.sh index 2513f22..cbde0d5 100644 --- a/tests/setup_install_test.sh +++ b/tests/setup_install_test.sh @@ -25,13 +25,13 @@ command() { sudo() { return 1; } # Simulate an apt repository without just. curl() { echo 'Unexpected download' >&2; exit 99; } cargo() { - if [ "$*" != 'install just --version 1.40.0 --locked' ]; then + if [ "$*" != 'install just --version 1.56.0 --locked' ]; then echo "Unexpected Cargo arguments: $*" >&2 exit 98 fi installed=true } -just() { printf 'just 1.40.0\n'; } +just() { printf 'just 1.56.0\n'; } install_just [ "$installed" = true ] SH @@ -53,7 +53,7 @@ SH FIXTURE_ROOT="$fixture_root" sh -eu <<'SH' . "$FIXTURE_ROOT/functions.sh" command() { [ "$2" = just ]; } -just() { printf 'just 1.40.0\n'; } +just() { printf 'just 1.56.0\n'; } cargo() { echo 'Unexpected install' >&2; exit 99; } sudo() { echo 'Unexpected install' >&2; exit 99; } install_just diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index 95165d7..b77c827 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 = Environments: what the kit provisions, and what each can reach The proof toolchain manifest (`../proof-toolchain/toolchain.kyaml`) says @@ -17,9 +17,9 @@ get in, whether fetched binaries may run, which container runtime exists, who reads its capability record, and a `measured` block. |`probe-reachability.sh` -|Sends one HEAD request per URL in `hosts.txt` and prints the HTTP status -this environment saw, as text or as one JSON object. Downloads nothing, -executes nothing. Its output is what goes into an entry's `measured` block, +|Sends one HEAD request per URL in `hosts.txt` (or, with `--get`, one GET +for the first byte only) and prints the HTTP status this environment saw, +as text or as one JSON object. Keeps no body, executes nothing. Its output is what goes into an entry's `measured` block, with the date. |`hosts.txt` @@ -28,7 +28,7 @@ with the date. == Reading a `measured` block -`reachable` means a HEAD request returned 2xx or 3xx. `refused` is a 403 +`reachable` means the request returned 2xx or 3xx (206 for a ranged GET). `refused` is a 403 from the environment's proxy. `auth-required` is a 401: the host answered and wants a token, which the probe does not supply. `tls-failed` means the host's certificate is not in the environment's CA bundle. A container @@ -37,6 +37,10 @@ registry's `/v2/` endpoint may answer `401` (wants a token) or `405` neither says whether an anonymous token flow would succeed. The manifest records such hosts under `registry-answered` with the codes seen. +Proxies and hosts can answer HEAD and GET differently, as the registries +do. Confirm a HEAD `refused` with `--get` before recording it, and say in +the `measured` block which method produced each code. + `execute-downloaded` under `measured` takes one of three values: `true` (a fetched binary was run), `false` (a fetched binary was present and the environment refused to run it), or `denied-before-download` (the @@ -47,9 +51,10 @@ A probe of a GitHub release *landing page* or of `api.github.com` says nothing about release *assets*: the asset download path redirects to `release-assets.githubusercontent.com`, which the probe follows separately. Record the asset outcome, not the landing page's. -Successful HEAD reachability does not establish that asset bytes were -downloaded or an executable ran. Record GET or download results separately -as manual measurements; the probe does not produce them. +A successful HEAD, or a one-byte GET, does not establish that a full +download is permitted or that an executable ran. Record full downloads and +execution attempts separately as manual measurements; the probe does not +produce them. A block is a fact about one environment instance on one date. It is never copied from one environment class to another. diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml index 21b313b..da6fa40 100644 --- a/tools/environments/environments.kyaml +++ b/tools/environments/environments.kyaml @@ -22,7 +22,7 @@ record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, environments: [ {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, - {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (21 URLs, every one probed)", reachable: ["github.com release asset HEAD (302 to release-assets.githubusercontent.com, then 200)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest)", "api.github.com", "crates.io"], registry-answered: ["ghcr.io (manual GET 401, probe HEAD 405)", "cgr.dev (manual GET 401, probe HEAD 405)"], tls-failed: ["www.cs.utexas.edu"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed"}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (22 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io (HEAD and GET 403)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed. The later one-byte GET shows asset bytes can flow, not that a full download or a run is permitted"}}, {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt index 3a6f7a6..b0719b6 100644 --- a/tools/environments/hosts.txt +++ b/tools/environments/hosts.txt @@ -1,6 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 # Hosts the proof toolchain is fetched from (tools/proof-toolchain/toolchain.kyaml # `method` column), one URL per line. '#' starts a comment. -# Probed by probe-reachability.sh with HEAD requests only. +# Probed by probe-reachability.sh with HEAD requests, or with --get using a +# one-byte ranged GET. # Release assets and source archives. The asset download URL is the path # `provers.sh install` would use; the landing page and the API are discovery @@ -28,6 +30,8 @@ https://mizar.uwb.edu.pl/ https://pvs.csl.sri.com/ https://www.cs.utexas.edu/~moore/acl2/ https://cvc5.github.io/ +# SBCL's official x86-64 Linux binary, which the sbcl entry fetches +https://downloads.sourceforge.net/project/sbcl/sbcl/2.6.9/sbcl-2.6.9-x86-64-linux-binary.tar.bz2 # Container registries (401 means the registry answered and wants a token) https://ghcr.io/v2/ diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index 047b4f2..cf94992 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -5,8 +5,11 @@ # probe-reachability.sh — measure which toolchain hosts this environment can # reach (experiment X1 in docs/proposals/environment-of-environments.adoc). # -# Sends one HEAD request per host and prints the HTTP status the environment -# saw. It downloads nothing and executes nothing it fetched. The result is a +# Sends one HEAD request per host (or, with --get, one GET for the first +# byte only, discarded) and prints the HTTP status the environment saw. Some +# hosts and proxies answer HEAD differently from GET, so a refusal seen with +# HEAD should be confirmed with --get before it is recorded. It executes +# nothing it fetched. The result is a # fact about THIS environment instance on THIS date; copy it into the # matching `measured` block of environments.kyaml rather than assuming it # holds elsewhere. @@ -14,10 +17,12 @@ # Usage: # tools/environments/probe-reachability.sh # text table # tools/environments/probe-reachability.sh --json # one JSON object +# tools/environments/probe-reachability.sh --get # GET, first byte only # HOSTS_FILE=my-hosts.txt tools/environments/probe-reachability.sh # # Exit code is 0 whenever the probe ran; reachability is reported, not -# judged. Exit 2 when curl is missing or the hosts file cannot be read. +# judged. Exit 2 when curl is missing, the hosts file cannot be read, or an +# argument is not recognised. set -euo pipefail @@ -25,8 +30,19 @@ HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" HOSTS_FILE="${HOSTS_FILE:-$HERE/hosts.txt}" TIMEOUT="${PROBE_TIMEOUT:-15}" MODE="text" -if [ "${1:-}" = "--json" ]; then - MODE="json" +METHOD="head" +for arg in "$@"; do + case "$arg" in + --json) MODE="json" ;; + --get) METHOD="get" ;; + *) echo "probe-reachability: unknown argument $arg" >&2; exit 2 ;; + esac +done +if [ "$METHOD" = "get" ]; then + # -r 0-0 asks for one byte; the body goes to /dev/null either way. + request=(-r 0-0) +else + request=(-I) fi if ! command -v curl >/dev/null 2>&1; then @@ -69,7 +85,7 @@ if command -v ldd >/dev/null 2>&1; then fi if [ "$MODE" = "text" ]; then - printf 'probe-reachability %s (%s)\n' "$date_utc" "$platform" + printf 'probe-reachability %s %s (%s)\n' "$METHOD" "$date_utc" "$platform" printf '%-6s %-14s %s\n' "HTTP" "OUTCOME" "URL" fi @@ -83,7 +99,7 @@ while IFS= read -r line || [ -n "$line" ]; do rc=0 # -L follows redirects so a release asset is measured at its final # host, not at the 302 GitHub answers with; the code is the last one. - code="$(curl -sS -I -L -o /dev/null -w '%{http_code}' --max-time "$TIMEOUT" "$line" 2>/dev/null)" || rc=$? + code="$(curl -sS "${request[@]}" -L -o /dev/null -w '%{http_code}' --max-time "$TIMEOUT" "$line" 2>/dev/null)" || rc=$? outcome="$(classify "$code" "$rc")" if [ "$MODE" = "text" ]; then printf '%-6s %-14s %s\n' "$code" "$outcome" "$line" @@ -97,6 +113,6 @@ if [ "$MODE" = "json" ]; then for r in "${rows[@]}"; do if [ -z "$joined" ]; then joined="$r"; else joined="$joined,$r"; fi done - printf '{"probe":"reachability","date":"%s","platform":"%s","hosts":[%s]}\n' \ - "$date_utc" "$platform" "$joined" + printf '{"probe":"reachability","method":"%s","date":"%s","platform":"%s","hosts":[%s]}\n' \ + "$METHOD" "$date_utc" "$platform" "$joined" fi diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index 9b4da16..bb7b6cc 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -18,9 +18,10 @@ this toolchain is projected onto, with measured reachability. Those measurements (2026-10-27) refine the assumptions below: the agent session probed there *could* reach `opam.ocaml.org`, `alire.ada.dev` and the tested GitHub source archive URL. A redirected HEAD request to a concrete GitHub -release asset succeeded; downloading its body and running it were not -observed. That session *could not* reach the tested release landing page -or `api.github.com`, so a `pin: resolve` entry cannot be resolved through +release asset succeeded, and a one-byte ranged GET of it returned 206; +a full download and running it were not observed. That session *could not* +reach the tested release landing page or `api.github.com` (403 to both HEAD +and GET), so a `pin: resolve` entry cannot be resolved through those paths in that session and `install` must read the concrete asset URL from the lock. Reachability is measured per environment and per path, not assumed per class. @@ -74,15 +75,16 @@ SHA-256 of the produced bundle and image digest. Never hand-edited. and an OCI image (Wolfi base) containing the same tree, both pinned in the lock. Before any verification, the build must run `sh tools/proof-toolchain/install-smoke.sh /opt/hyperpolymath/provers` -from the checkout root to install the four core-backend fixtures under +from the checkout root to install the core-backend smoke fixtures under `$PREFIX/share/smoke/`; an installation failure stops the build. |`provers.sh install` |Fetches the bundle named in the lock, checks its SHA-256, and unpacks it at the prefix. The same command serves the workstation, a session's setup script, and a CI job, where network and execution policy permit. The -2026-10-27 session measured HEAD reachability only; bundle download and -execution must be checked separately on each supported target. +2026-10-27 session measured HEAD reachability and a one-byte GET only; a +full bundle download and execution must be checked separately on each +supported target. |`provers.sh doctor` |Reports each manifest entry as `PRESENT `, `DRIFT != `, @@ -123,8 +125,9 @@ The lock records the builder image digest and the glibc minimum. === Why a release asset first, image second -The 2026-10-27 agent session reached a release asset with HEAD, while its -download-and-run experiment was denied before download. The tarball targets +The 2026-10-27 agent session reached a release asset with HEAD and with a +one-byte GET, while its download-and-run experiment was denied before +download. The tarball targets sessions whose network and execution policies allow it; a successful HEAD alone does not establish that. CI and the dispatchers can run containers. The tarball is the primary artefact and the image wraps the same tree. @@ -167,8 +170,8 @@ plus the supporting tools the mapped provers need. |`policy:recheck` |Rocq (`coqc`), Lean (elan with pinned toolchains; no Mathlib) |`transport` |agda2dedukti, Dedukti (`dkcheck`), Lambdapi. agda2dedukti tracks particular Agda versions; the manifest records which Agda it accepts. |`exception:rust` |Kani; Aeneas with Charon (PROOF-POLICY §4.1) -|`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2 and Mizar (supplementary only). The last four were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set; PVS, the remaining core backend, is a licensed binary and belongs to the sealed-container tail, not the bundle. -|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, Poly/ML for HOL4 and SBCL for ACL2, bundled rather than taken from the host +|`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2, Mizar and PVS (supplementary only). The last five were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set. PVS is built from its BSD-3-Clause sources on the bundled SBCL; SRI's click-through licence covers only its Allegro build, which the bundle does not use. +|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host |`backend` |Z3, CVC5, Yices, Alt-Ergo, E prover, Vampire |=== diff --git a/tools/proof-toolchain/install-smoke.sh b/tools/proof-toolchain/install-smoke.sh index fd3ee1e..627a460 100644 --- a/tools/proof-toolchain/install-smoke.sh +++ b/tools/proof-toolchain/install-smoke.sh @@ -11,6 +11,7 @@ fi smoke_dir="$(CDPATH='' cd -- "$(dirname -- "$0")/smoke" && pwd)" destination="$1/share/smoke" install -d "$destination" -for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz; do +for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz \ + mizar-smoke.sh pvs-smoke.sh pvs_smoke.pvs; do install -m 644 "$smoke_dir/$fixture" "$destination/$fixture" done diff --git a/tools/proof-toolchain/smoke/mizar-smoke.sh b/tools/proof-toolchain/smoke/mizar-smoke.sh new file mode 100644 index 0000000..04edba3 --- /dev/null +++ b/tools/proof-toolchain/smoke/mizar-smoke.sh @@ -0,0 +1,35 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# Verify smoke.miz against the bundled MML from a scratch directory, so a +# doctor run never writes into the installed prefix. +# Usage: sh mizar-smoke.sh PREFIX +set -eu + +if [ "$#" -ne 1 ] || [ -z "$1" ]; then + echo "usage: sh mizar-smoke.sh PREFIX" >&2 + exit 2 +fi + +smoke_dir="$(CDPATH='' cd -- "$(dirname -- "$0")" && pwd)" +# Closure rule: always the bundle's MML, never a host MIZFILES. +MIZFILES="$1/share/mizar" +export MIZFILES +if [ ! -d "$MIZFILES" ]; then + echo "mizar smoke: MIZFILES $MIZFILES is not a directory" >&2 + exit 1 +fi + +work="$(mktemp -d)" +trap 'rm -rf "$work"' EXIT +trap 'exit 1' HUP INT TERM +mkdir "$work/text" +cp "$smoke_dir/smoke.miz" "$work/text/smoke.miz" +cd "$work" +makeenv text/smoke +verifier text/smoke +# Mizar reports article errors in the .err file, not only in its exit status. +if [ ! -f text/smoke.err ] || [ -s text/smoke.err ]; then + echo "mizar smoke: verifier left errors (or no error file)" >&2 + cat text/smoke.err >&2 2>/dev/null || true + exit 1 +fi diff --git a/tools/proof-toolchain/smoke/pvs-smoke.sh b/tools/proof-toolchain/smoke/pvs-smoke.sh new file mode 100644 index 0000000..c645f47 --- /dev/null +++ b/tools/proof-toolchain/smoke/pvs-smoke.sh @@ -0,0 +1,20 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# Prove pvs_smoke.pvs in batch mode from a scratch directory (PVS writes +# pvsbin/ and .pvscontext beside the file). proveit's exit status is not +# documented to reflect unproved formulas, so require the summary line. +set -eu + +smoke_dir="$(CDPATH='' cd -- "$(dirname -- "$0")" && pwd)" +work="$(mktemp -d)" +trap 'rm -rf "$work"' EXIT +trap 'exit 1' HUP INT TERM +cp "$smoke_dir/pvs_smoke.pvs" "$work/pvs_smoke.pvs" +cd "$work" +prover_exit=0 +proveit --force pvs_smoke.pvs >transcript 2>&1 || prover_exit=$? +if [ "$prover_exit" -ne 0 ] || + ! grep -Eq 'Grand Totals: 1 proofs?, 1 attempted, 1 succeeded' transcript; then + cat transcript >&2 + exit 1 +fi diff --git a/tools/proof-toolchain/smoke/pvs_smoke.pvs b/tools/proof-toolchain/smoke/pvs_smoke.pvs new file mode 100644 index 0000000..7abc98d --- /dev/null +++ b/tools/proof-toolchain/smoke/pvs_smoke.pvs @@ -0,0 +1,11 @@ +% SPDX-License-Identifier: MPL-2.0 +% One reflexivity lemma; its ProofLite script below is installed by proveit. +pvs_smoke: THEORY +BEGIN + x: VAR int + smoke_refl: LEMMA x = x + + %|- smoke_refl : PROOF + %|- (grind) + %|- QED +END pvs_smoke diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml index 3c2c20b..ba12637 100644 --- a/tools/proof-toolchain/toolchain.kyaml +++ b/tools/proof-toolchain/toolchain.kyaml @@ -15,7 +15,7 @@ # field, and every run must pass, so one missing toolchain fails the entry. # Smoke fixtures named by verify commands live in smoke/ beside this file and # are installed to $PREFIX/share/smoke/ by the bundle build. -# For hol-light, hol4, acl2 and mizar, run `sh install-smoke.sh "$PREFIX"` +# For hol-light, hol4, acl2, mizar and pvs, run `sh install-smoke.sh "$PREFIX"` # from this directory before verification (see DESIGN.adoc). { schema: 1, @@ -48,9 +48,10 @@ {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"}, {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure. Supplementary evidence only"}, - {id: "sbcl", role: "runtime", method: "release asset (sbcl/sbcl Linux x86_64 binary)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 is built on; bundled so acl2 does not depend on a host Lisp"}, - {id: "acl2", role: "exception:recorded", method: "release asset (acl2/acl2 tagged source) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books are not bundled; a consumer that needs them records that as its own entry. The upstream download host failed TLS from one agent session (environments.kyaml), so the bundle build fetches it, not the session. Supplementary evidence only"}, - {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML)", pin: "resolve-stable", verify: "makeenv $PREFIX/share/smoke/smoke.miz && verifier $PREFIX/share/smoke/smoke.miz", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. Supplementary evidence only"}, + {id: "sbcl", role: "runtime", method: "release archive (the official x86-64 Linux binary distribution that sbcl.org's platform table links, served from downloads.sourceforge.net; sbcl/sbcl on GitHub carries source tags only)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 and PVS are built on; bundled so neither depends on a host Lisp. One pin serves both, and the lock records the version each was built with"}, + {id: "acl2", role: "exception:recorded", method: "tagged source archive (acl2/acl2 on GitHub, fetched from codeload.github.com) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books (books/, licensed separately) are not bundled; a consumer that needs them records that as its own entry. The entry never fetches from the legacy www.cs.utexas.edu home. Supplementary evidence only"}, + {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML), with the MML installed at $PREFIX/share/mizar", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/mizar-smoke.sh $PREFIX", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. The smoke script sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file. Supplementary evidence only"}, + {id: "pvs", role: "exception:recorded", method: "source build (SRI-CSL/PVS tagged release, BSD-3-Clause) on the bundled SBCL, headless, exposed as bin/pvs and bin/proveit", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/pvs-smoke.sh", needs: ["sbcl"], notes: "added 2026-10-27 (E6, completing echidna's core twelve). The SBCL source build is redistributable; SRI's click-through licence covers only its Allegro build, which is not used. NASALib is not bundled; a consumer that needs it records it as its own entry. The smoke script proves one lemma with proveit in a scratch directory and requires the summary to report it succeeded. Supplementary evidence only"}, {id: "z3", role: "backend", method: "release asset", pin: "resolve", verify: "z3 --version"}, {id: "cvc5", role: "backend", method: "release asset", pin: "resolve", verify: "cvc5 --version"}, {id: "yices", role: "backend", method: "release asset (SRI-CSL yices2)", pin: "resolve-stable", verify: "yices --version"}, From 187e28f6cc3a6acbd1835cd9597325defd6ff4cf Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:35:31 +0000 Subject: [PATCH 12/16] fix: address the review findings left open when #98 merged - 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. The test now uses stub executables and a real PATH lookup. - probe-reachability.sh: --get caps a body sent despite the byte range at 64 KiB and reports it as range-ignored; a non-GNU ldd (FreeBSD) no longer stops the probe. New tests/probe_reachability_test.sh runs it against a local server. - toolchain.kyaml: HOL Light's OCaml switch is a locked runtime entry; Poly/ML takes the newest stable tag (HOL4 names no version); Mizar names its real i386 distribution, whose binaries are static (checked with file(1)) and need IA32 emulation on the host. - Measurement re-taken 2026-11-04 over 24 hosts: Cargo's sparse index and crate download answer, so cargo install is no longer reported as blocked by the refused crates.io API; Isabelle is intermittent. - Proposals: PVS owned by awesome-hol (priority 1); X1 covers every probeable class; DRIFT field names and the checker lock hash stated. - container-init renders {{VERSION}}; the dogfood gate summary counts the K9 files the hook validated; the smoke test checks the whole prefix. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .github/workflows/dogfood-gate.yml | 6 +- CHANGELOG.adoc | 25 ++++++++ Justfile | 5 ++ build/setup.sh | 14 +++- .../awesome-estate-maths-proving.adoc | 6 +- .../boj-prover-solver-cartridges.adoc | 9 ++- .../environment-of-environments.adoc | 43 ++++++++----- tests/probe_reachability_test.sh | 64 +++++++++++++++++++ tests/proof_smoke_wrappers_test.sh | 10 +-- tests/setup_install_test.sh | 45 +++++++------ tools/environments/README.adoc | 12 +++- tools/environments/environments.kyaml | 2 +- tools/environments/hosts.txt | 4 ++ tools/environments/probe-reachability.sh | 20 ++++-- tools/proof-toolchain/DESIGN.adoc | 6 +- tools/proof-toolchain/toolchain.kyaml | 7 +- 16 files changed, 219 insertions(+), 59 deletions(-) create mode 100644 tests/probe_reachability_test.sh diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 3f3f321..36e017d 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -82,11 +82,15 @@ jobs: 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 @@ jobs: 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, against **${CFG_COUNT}** config file(s)." >> "$GITHUB_STEP_SUMMARY" fi # --------------------------------------------------------------------------- diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ef5f17a..760190e 100644 --- a/CHANGELOG.adoc +++ b/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 `{{VERSION}}`; 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 diff --git a/Justfile b/Justfile index 93a23bf..23df655 100644 --- a/Justfile +++ b/Justfile @@ -385,10 +385,14 @@ 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}" + 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 +408,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 diff --git a/build/setup.sh b/build/setup.sh index ab40d83..ae7380c 100755 --- a/build/setup.sh +++ b/build/setup.sh @@ -137,7 +137,19 @@ install_just_with_cargo() { 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() { diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc index b9068a6..66fbbfb 100644 --- a/docs/proposals/awesome-estate-maths-proving.adoc +++ b/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` diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index 072d8f9..871937d 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/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,8 @@ 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 lock hash +(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`. diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index 11c48d6..95a3315 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/docs/proposals/environment-of-environments.adoc @@ -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 <>). @@ -79,13 +79,15 @@ 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). +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/…/just-1.56.0.crate` |200 (HEAD); 206 and 200 (GET) |*Reachable.* These are the sparse index and crate download `cargo install` uses, 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 diff --git a/tests/probe_reachability_test.sh b/tests/probe_reachability_test.sh new file mode 100644 index 0000000..3b0a231 --- /dev/null +++ b/tests/probe_reachability_test.sh @@ -0,0 +1,64 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Test tools/environments/probe-reachability.sh against a local HTTP server: +# a non-GNU ldd must not stop the probe, a GET to a server that ignores the +# byte range must be capped and reported as range-ignored, and an unknown +# argument must exit 2. Needs python3 and curl; touches no outside host. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +probe="$repo_root/tools/environments/probe-reachability.sh" +work="$(mktemp -d)" +server_pid="" +cleanup() { + if [ -n "$server_pid" ]; then kill "$server_pid" 2>/dev/null || true; fi + rm -rf "$work" +} +trap cleanup EXIT + +fail() { echo "FAIL: $*" >&2; exit 1; } + +# python's http.server ignores Range and sends Content-Length, which is the +# case the size cap must catch. 1 MiB is far above the probe's 64 KiB cap. +mkdir -p "$work/www" "$work/bin" +head -c 1048576 /dev/zero > "$work/www/big.bin" +printf 'small\n' > "$work/www/small.txt" +port="$(python3 -I -c 'import socket; s=socket.socket(); s.bind(("127.0.0.1",0)); print(s.getsockname()[1]); s.close()')" +(cd "$work/www" && exec python3 -I -m http.server "$port" --bind 127.0.0.1) >/dev/null 2>&1 & +server_pid=$! +for _ in $(seq 50); do + curl -s -o /dev/null --noproxy '*' "http://127.0.0.1:$port/small.txt" && break + sleep 0.1 +done + +printf '# comment\nhttp://127.0.0.1:%s/big.bin\nhttp://127.0.0.1:%s/small.txt\n' "$port" "$port" > "$work/hosts.txt" + +# 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/ldd" + +run() { + env -u HTTPS_PROXY -u HTTP_PROXY -u https_proxy -u http_proxy NO_PROXY='*' \ + PATH="$work/bin:$PATH" HOSTS_FILE="$work/hosts.txt" PROBE_TIMEOUT=10 \ + bash "$probe" "$@" +} + +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" +grep -Eq '^200 +reachable +http://127\.0\.0\.1:[0-9]+/big\.bin$' <<<"$head_out" || + fail "HEAD of big.bin not reachable: $head_out" + +get_out="$(run --get)" || fail "GET probe exited non-zero" +grep -Eq '^200 +range-ignored +http://127\.0\.0\.1:[0-9]+/big\.bin$' <<<"$get_out" || + fail "GET of a range-ignoring server not capped as range-ignored: $get_out" +grep -Eq '^200 +reachable +http://127\.0\.0\.1:[0-9]+/small\.txt$' <<<"$get_out" || + fail "small GET body not reachable: $get_out" + +json="$(run --json --get)" || fail "JSON probe exited non-zero" +python3 -I -c 'import json,sys; d=json.loads(sys.argv[1]); assert d["method"]=="get"; assert {h["outcome"] for h in d["hosts"]}=={"range-ignored","reachable"}' "$json" || + fail "JSON output invalid: $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, rejects unknown arguments' diff --git a/tests/proof_smoke_wrappers_test.sh b/tests/proof_smoke_wrappers_test.sh index 497e300..8e89bba 100755 --- a/tests/proof_smoke_wrappers_test.sh +++ b/tests/proof_smoke_wrappers_test.sh @@ -17,7 +17,11 @@ for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz \ 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 local want="$1" what="$2"; shift 2 @@ -73,7 +77,5 @@ expect fail "pvs unproved" pvs unproved 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' diff --git a/tests/setup_install_test.sh b/tests/setup_install_test.sh index cbde0d5..fd6bcc2 100644 --- a/tests/setup_install_test.sh +++ b/tests/setup_install_test.sh @@ -10,30 +10,37 @@ trap 'rm -rf "$fixture_root"' EXIT # Source the actual functions without running setup's main routine. sed '/^main "\$@"$/d' "$repo_root/build/setup.sh" > "$fixture_root/functions.sh" +# Cargo fallback, with stub executables and a real PATH lookup. Cargo's +# install root is deliberately NOT on PATH, as with a distro Cargo: setup must +# install into a known root and put its bin directory on PATH itself. +mkdir -p "$fixture_root/bin" +cat > "$fixture_root/bin/cargo" <<'SH' +#!/bin/sh +expected="install just --version 1.56.0 --locked --root $CARGO_HOME" +if [ "$*" != "$expected" ]; then + echo "Unexpected Cargo arguments: $*" >&2 + exit 98 +fi +mkdir -p "$CARGO_HOME/bin" +printf '#!/bin/sh\necho "just 1.56.0"\n' > "$CARGO_HOME/bin/just" +chmod +x "$CARGO_HOME/bin/just" +SH +printf '#!/bin/sh\nexit 1\n' > "$fixture_root/bin/sudo" # an apt repository without just +chmod +x "$fixture_root/bin/cargo" "$fixture_root/bin/sudo" + for manager in apt unknown; do - FIXTURE_ROOT="$fixture_root" MANAGER="$manager" sh -eu <<'SH' + rm -rf "$fixture_root/cargo-home" + FIXTURE_ROOT="$fixture_root" MANAGER="$manager" CARGO_HOME="$fixture_root/cargo-home" \ + PATH="$fixture_root/bin:/usr/bin:/bin" sh -eu <<'SH' . "$FIXTURE_ROOT/functions.sh" PKG_MGR="$MANAGER" -installed=false -command() { - case "$2" in - just) [ "$installed" = true ] ;; - cargo) return 0 ;; - *) return 1 ;; - esac -} -sudo() { return 1; } # Simulate an apt repository without just. curl() { echo 'Unexpected download' >&2; exit 99; } -cargo() { - if [ "$*" != 'install just --version 1.56.0 --locked' ]; then - echo "Unexpected Cargo arguments: $*" >&2 - exit 98 - fi - installed=true -} -just() { printf 'just 1.56.0\n'; } install_just -[ "$installed" = true ] +case ":$PATH:" in + *":$CARGO_HOME/bin:"*) ;; + *) echo "FAIL: $CARGO_HOME/bin was not added to PATH" >&2; exit 1 ;; +esac +[ "$(just --version)" = 'just 1.56.0' ] SH done diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index b77c827..691083a 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -18,8 +18,10 @@ who reads its capability record, and a `measured` block. |`probe-reachability.sh` |Sends one HEAD request per URL in `hosts.txt` (or, with `--get`, one GET -for the first byte only) and prints the HTTP status this environment saw, -as text or as one JSON object. Keeps no body, executes nothing. Its output is what goes into an entry's `measured` block, +for the first byte only, capped at 64 KiB when the server ignores the +range) and prints the HTTP status this environment saw, as text or as one +JSON object. Keeps no body, executes nothing. `tests/probe_reachability_test.sh` +checks it against a local server. Its output is what goes into an entry's `measured` block, with the date. |`hosts.txt` @@ -28,7 +30,11 @@ with the date. == Reading a `measured` block -`reachable` means the request returned 2xx or 3xx (206 for a ranged GET). `refused` is a 403 +`reachable` means the request returned 2xx or 3xx (206 for a ranged GET). +`range-ignored` means a `--get` request was answered with the whole body, +so curl stopped at the 64 KiB cap: the host answered and serves the file, +but cannot resume a download. A host that answers some tries and resets +others is recorded under `intermittent` with the counts seen. `refused` is a 403 from the environment's proxy. `auth-required` is a 401: the host answered and wants a token, which the probe does not supply. `tls-failed` means the host's certificate is not in the environment's CA bundle. A container diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml index da6fa40..a9f13ed 100644 --- a/tools/environments/environments.kyaml +++ b/tools/environments/environments.kyaml @@ -22,7 +22,7 @@ record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, environments: [ {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, - {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (22 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io (HEAD and GET 403)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed. The later one-byte GET shows asset bytes can flow, not that a full download or a run is permitted"}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-11-04", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (24 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET capped at 64 KiB)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com (GET range-ignored: answers 200 with the whole archive, capped)", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "index.crates.io (Cargo's sparse index)", "static.crates.io (crate download; GET range-ignored, capped)", "releases.lean-lang.org", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org (GET range-ignored, capped)"], intermittent: ["isabelle.in.tum.de (HEAD 200; GET 206 on 1 of 4 tries, the rest reset during the TLS handshake, curl exit 35)"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io/api (HEAD and GET 403; Cargo does not use it to install)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the 2026-10-27 Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was not observed. One-byte GETs show asset bytes can flow, not that a full download or a run is permitted. On 2026-11-04 the Mizar distribution was downloaded and inspected with file(1) without being run"}}, {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt index b0719b6..b9a3b2f 100644 --- a/tools/environments/hosts.txt +++ b/tools/environments/hosts.txt @@ -21,6 +21,10 @@ https://alire.ada.dev/ https://hackage.haskell.org/ https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init https://crates.io/api/v1/crates/just +# What `cargo install` actually uses: the sparse index and the crate download. +# A refusal of the API above says nothing about these. +https://index.crates.io/ju/st/just +https://static.crates.io/crates/just/just-1.56.0.crate https://releases.lean-lang.org/ https://ftp.gnu.org/gnu/guix/ diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index cf94992..54df3bb 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -39,8 +39,11 @@ for arg in "$@"; do esac done if [ "$METHOD" = "get" ]; then - # -r 0-0 asks for one byte; the body goes to /dev/null either way. - request=(-r 0-0) + # -r 0-0 asks for one byte. A server may ignore the range and send the + # whole body, so --max-filesize caps the transfer: curl aborts (exit 63) + # before reading a body whose length is declared above the cap, or once a + # chunked body passes it. The body goes to /dev/null either way. + request=(-r 0-0 --max-filesize 65536) else request=(-I) fi @@ -56,7 +59,9 @@ fi # classify — print one outcome label to stdout. # Takes the final HTTP status after redirects and curl's exit code. Exit 60 -# yields tls-failed; any other non-zero exit or HTTP 000 yields unreachable, +# yields tls-failed; exit 63 with a status (the --get size cap tripped +# because the host ignored the range) yields range-ignored, a host that +# answered; any other non-zero exit or HTTP 000 yields unreachable, # regardless of the HTTP status. With a zero exit, 401 yields auth-required, # 403 yields refused, 2xx/3xx yields reachable, and all other codes yield # http-. A failed probe is reported as a label, not an error status. @@ -64,6 +69,8 @@ classify() { local code="$1" rc="$2" if [ "$rc" -eq 60 ]; then echo "tls-failed" + elif [ "$rc" -eq 63 ] && [ "$code" != "000" ]; then + echo "range-ignored" elif [ "$rc" -ne 0 ] || [ "$code" = "000" ]; then echo "unreachable" elif [ "$code" = "401" ]; then @@ -81,7 +88,12 @@ date_utc="$(date -u +%Y-%m-%dT%H:%M:%SZ)" platform="$(uname -s)/$(uname -m)" if command -v ldd >/dev/null 2>&1; then # awk reads all of ldd's output, so no SIGPIPE under pipefail. - platform="$platform glibc $(ldd --version 2>/dev/null | awk 'NR==1{print $NF}')" + # Only GNU ldd knows --version (FreeBSD's does not), so the C library + # version is optional and its failure must not stop the probe. + libc="$(ldd --version 2>/dev/null | awk 'NR==1 && /GNU|GLIBC/{print $NF}')" || libc="" + if [ -n "$libc" ]; then + platform="$platform glibc $libc" + fi fi if [ "$MODE" = "text" ]; then diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index bb7b6cc..15204fa 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -88,7 +88,9 @@ supported target. |`provers.sh doctor` |Reports each manifest entry as `PRESENT `, `DRIFT != `, -or `UNAVAILABLE `, as text and as one JCS object. It never reports a +or `UNAVAILABLE `, as text and as one JCS object. In the object a +`DRIFT` entry carries `observed_version`, `observed_sha256`, +`locked_version`, `locked_sha256` and `mismatch`. It never reports a tool it could not run as present (PROOF-POLICY §6). |`provers.sh render` @@ -171,7 +173,7 @@ plus the supporting tools the mapped provers need. |`transport` |agda2dedukti, Dedukti (`dkcheck`), Lambdapi. agda2dedukti tracks particular Agda versions; the manifest records which Agda it accepts. |`exception:rust` |Kani; Aeneas with Charon (PROOF-POLICY §4.1) |`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2, Mizar and PVS (supplementary only). The last five were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set. PVS is built from its BSD-3-Clause sources on the bundled SBCL; SRI's click-through licence covers only its Allegro build, which the bundle does not use. -|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host +|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, the OCaml switch HOL Light runs in, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host |`backend` |Z3, CVC5, Yices, Alt-Ergo, E prover, Vampire |=== diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml index ba12637..bb84eaa 100644 --- a/tools/proof-toolchain/toolchain.kyaml +++ b/tools/proof-toolchain/toolchain.kyaml @@ -45,12 +45,13 @@ {id: "tlc", role: "exception:recorded", method: "release asset (tlaplus tla2tools.jar) plus a bundled tlc launcher (java -cp $PREFIX/lib/tla/tla2tools.jar tlc2.TLC, absolute so it runs from any directory)", pin: "resolve-stable", verify: "tlc -h", needs: ["jre"], notes: "pin a stable tagged release with its sha256 in the lock; v1.8.0 is a rolling prerelease rebuilt on every master commit"}, {id: "jre", role: "runtime", method: "release asset (Eclipse Temurin JRE, Java 17 or later)", pin: "resolve-stable", verify: "java -version", notes: "bundled so the tlc launcher does not depend on a host Java"}, {id: "isabelle", role: "exception:recorded", method: "release asset", pin: "resolve", verify: "isabelle version", notes: "supplementary evidence only"}, - {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"}, - {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"}, + {id: "hol-light-ocaml", role: "runtime", method: "opam switch at $PREFIX/opam/hol-light holding the OCaml compiler and the camlp5, zarith (or num) and ledit versions that the pinned hol_light opam file selects for that compiler series", pin: "from hol-light opam", verify: "$PREFIX/opam/hol-light/bin/ocaml -version", notes: "HOL Light's launcher starts this OCaml toplevel with the checkpointed image, so the switch is part of the closure: every package in it is locked with its version and hash, and camlp5 stays inside the cap the hol_light opam file sets for the chosen OCaml series"}, + {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) into the hol-light-ocaml switch, with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", needs: ["hol-light-ocaml"], notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"}, + {id: "polyml", role: "runtime", method: "source build (polyml/polyml, tagged release) into the prefix, with libpolyml and libpolymain found through the bundle's run path", pin: "resolve-stable", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML. HOL4 recommends Poly/ML but names no version, so the newest stable tag is taken and the lock records the version HOL4 was built and smoke-tested with"}, {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure. Supplementary evidence only"}, {id: "sbcl", role: "runtime", method: "release archive (the official x86-64 Linux binary distribution that sbcl.org's platform table links, served from downloads.sourceforge.net; sbcl/sbcl on GitHub carries source tags only)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 and PVS are built on; bundled so neither depends on a host Lisp. One pin serves both, and the lock records the version each was built with"}, {id: "acl2", role: "exception:recorded", method: "tagged source archive (acl2/acl2 on GitHub, fetched from codeload.github.com) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books (books/, licensed separately) are not bundled; a consumer that needs them records that as its own entry. The entry never fetches from the legacy www.cs.utexas.edu home. Supplementary evidence only"}, - {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML), with the MML installed at $PREFIX/share/mizar", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/mizar-smoke.sh $PREFIX", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. The smoke script sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file. Supplementary evidence only"}, + {id: "mizar", role: "exception:recorded", method: "release archive (the i386-linux system distribution from mizar.uwb.edu.pl/~softadm/current, which carries the matching MML; Mizar publishes no x86_64 Linux build), with the MML installed at $PREFIX/share/mizar", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/mizar-smoke.sh $PREFIX", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. The smoke script sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file. Its binaries are statically linked 32-bit i386 executables (checked with file(1) on 8.1.15: no shared libraries), so no 32-bit userland is bundled, but the host kernel must run i386 code (IA32 emulation); where it cannot, the smoke check fails and doctor reports UNAVAILABLE. Supplementary evidence only"}, {id: "pvs", role: "exception:recorded", method: "source build (SRI-CSL/PVS tagged release, BSD-3-Clause) on the bundled SBCL, headless, exposed as bin/pvs and bin/proveit", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/pvs-smoke.sh", needs: ["sbcl"], notes: "added 2026-10-27 (E6, completing echidna's core twelve). The SBCL source build is redistributable; SRI's click-through licence covers only its Allegro build, which is not used. NASALib is not bundled; a consumer that needs it records it as its own entry. The smoke script proves one lemma with proveit in a scratch directory and requires the summary to report it succeeded. Supplementary evidence only"}, {id: "z3", role: "backend", method: "release asset", pin: "resolve", verify: "z3 --version"}, {id: "cvc5", role: "backend", method: "release asset", pin: "resolve", verify: "cvc5 --version"}, From e67a298a77d3854042bc299107f779f2d8d69824 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:36:51 +0000 Subject: [PATCH 13/16] test(probe): drop Python from the reachability probe test Python is banned estate-wide. The test now drives the probe with stub curl and ldd executables, offline: the stub reproduces curl 8.5's measured exit 63 for a server that ignores the byte range, and fails if --get omits the size cap. JSON is checked with jq. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- tests/probe_reachability_test.sh | 86 +++++++++++++++++--------------- tools/environments/README.adoc | 7 +-- 2 files changed, 50 insertions(+), 43 deletions(-) diff --git a/tests/probe_reachability_test.sh b/tests/probe_reachability_test.sh index 3b0a231..b085369 100644 --- a/tests/probe_reachability_test.sh +++ b/tests/probe_reachability_test.sh @@ -1,64 +1,70 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 -# Test tools/environments/probe-reachability.sh against a local HTTP server: -# a non-GNU ldd must not stop the probe, a GET to a server that ignores the -# byte range must be capped and reported as range-ignored, and an unknown -# argument must exit 2. Needs python3 and curl; touches no outside host. +# 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)" -server_pid="" -cleanup() { - if [ -n "$server_pid" ]; then kill "$server_pid" 2>/dev/null || true; fi - rm -rf "$work" -} -trap cleanup EXIT - +trap 'rm -rf "$work"' EXIT fail() { echo "FAIL: $*" >&2; exit 1; } -# python's http.server ignores Range and sends Content-Length, which is the -# case the size cap must catch. 1 MiB is far above the probe's 64 KiB cap. -mkdir -p "$work/www" "$work/bin" -head -c 1048576 /dev/zero > "$work/www/big.bin" -printf 'small\n' > "$work/www/small.txt" -port="$(python3 -I -c 'import socket; s=socket.socket(); s.bind(("127.0.0.1",0)); print(s.getsockname()[1]); s.close()')" -(cd "$work/www" && exec python3 -I -m http.server "$port" --bind 127.0.0.1) >/dev/null 2>&1 & -server_pid=$! -for _ in $(seq 50); do - curl -s -o /dev/null --noproxy '*' "http://127.0.0.1:$port/small.txt" && break - sleep 0.1 -done - -printf '# comment\nhttp://127.0.0.1:%s/big.bin\nhttp://127.0.0.1:%s/small.txt\n' "$port" "$port" > "$work/hosts.txt" +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/ldd" +chmod +x "$work/bin/curl" "$work/bin/ldd" -run() { - env -u HTTPS_PROXY -u HTTP_PROXY -u https_proxy -u http_proxy NO_PROXY='*' \ - PATH="$work/bin:$PATH" HOSTS_FILE="$work/hosts.txt" PROBE_TIMEOUT=10 \ - bash "$probe" "$@" -} +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" -grep -Eq '^200 +reachable +http://127\.0\.0\.1:[0-9]+/big\.bin$' <<<"$head_out" || - fail "HEAD of big.bin not reachable: $head_out" +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" -grep -Eq '^200 +range-ignored +http://127\.0\.0\.1:[0-9]+/big\.bin$' <<<"$get_out" || - fail "GET of a range-ignoring server not capped as range-ignored: $get_out" -grep -Eq '^200 +reachable +http://127\.0\.0\.1:[0-9]+/small\.txt$' <<<"$get_out" || - fail "small GET body not reachable: $get_out" +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" -python3 -I -c 'import json,sys; d=json.loads(sys.argv[1]); assert d["method"]=="get"; assert {h["outcome"] for h in d["hosts"]}=={"range-ignored","reachable"}' "$json" || - fail "JSON output invalid: $json" +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, rejects unknown arguments' +echo 'PASS: probe tolerates non-GNU ldd, caps range-ignoring GETs, classifies outcomes' diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index 691083a..1c7c27f 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -20,9 +20,10 @@ who reads its capability record, and a `measured` block. |Sends one HEAD request per URL in `hosts.txt` (or, with `--get`, one GET for the first byte only, capped at 64 KiB when the server ignores the range) and prints the HTTP status this environment saw, as text or as one -JSON object. Keeps no body, executes nothing. `tests/probe_reachability_test.sh` -checks it against a local server. Its output is what goes into an entry's `measured` block, -with the date. +JSON object. Keeps no body, executes nothing. Its output is what goes +into an entry's `measured` block, with the date. +`tests/probe_reachability_test.sh` checks it offline with stub `curl` and +`ldd` executables. |`hosts.txt` |The hosts the toolchain manifest's `method` column fetches from. From d8c51b8f50672dc67537dfed97a45237c23d93d1 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:39:04 +0000 Subject: [PATCH 14/16] docs(changelog): avoid a literal template token in the Fixed entry The OpenSSF placeholder check reads any {{NAME}} in CHANGELOG.adoc as an unfilled template token; name the VERSION placeholder in words instead. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- CHANGELOG.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 760190e..df3954f 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -56,7 +56,7 @@ addressed: * 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 `{{VERSION}}`; the dogfood gate's +* `Justfile` `container-init` renders the `VERSION` placeholder; the dogfood gate's summary counts the K9 files the hook validated, not every `*.k9` path. ==== Changed From 5fa359ceba3987d627f482b3c230c5fcb62cba99 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:49:44 +0000 Subject: [PATCH 15/16] fix: address CodeRabbit's review of the #98 follow-up - hosts.txt and the measurement: probe Cargo's real download route, static.crates.io/crates/just/1.56.0/download (the index dl plus /{crate}/{version}/download), which answers; the .crate path is gone. - setup test: unset CARGO_INSTALL_ROOT, and run the fallback with a PATH of stubs plus linked utilities only, so a system just cannot short-circuit it. - container-init: reject a VERSION that is unsafe inside quoted TOML, Nickel and a sed replacement, before any file is changed. - dogfood gate: count only regular *.k9 files, and say config files are counted, not validated. - Docs: the measurement is from two sessions; range-ignored does not prove a host cannot resume; the GET cap was measured on curl 8.5.0; the lock records each tool's executable digest, which a PROVEN result cites as locked_sha256. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .github/workflows/dogfood-gate.yml | 4 ++-- Justfile | 6 ++++++ docs/proposals/boj-prover-solver-cartridges.adoc | 5 +++-- docs/proposals/environment-of-environments.adoc | 8 ++++---- tests/setup_install_test.sh | 12 +++++++++++- tools/environments/README.adoc | 7 +++++-- tools/environments/environments.kyaml | 2 +- tools/environments/hosts.txt | 4 +++- tools/environments/probe-reachability.sh | 4 +++- tools/proof-toolchain/DESIGN.adoc | 6 ++++-- 10 files changed, 42 insertions(+), 16 deletions(-) diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 36e017d..27e0ef6 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -71,7 +71,7 @@ jobs: - 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) @@ -103,7 +103,7 @@ jobs: else echo "## K9 Contract Validation" >> "$GITHUB_STEP_SUMMARY" echo "" >> "$GITHUB_STEP_SUMMARY" - echo "Validated **${VALIDATED:-0}** of **${K9_COUNT}** K9 file(s) found, 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 # --------------------------------------------------------------------------- diff --git a/Justfile b/Justfile index 23df655..17dea27 100644 --- a/Justfile +++ b/Justfile @@ -387,6 +387,12 @@ container-init: 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" diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc index 871937d..daaf53f 100644 --- a/docs/proposals/boj-prover-solver-cartridges.adoc +++ b/docs/proposals/boj-prover-solver-cartridges.adoc @@ -140,8 +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, version and lock hash -(so the exact checker binary is pinned), 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`. diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc index 95a3315..cdcc969 100644 --- a/docs/proposals/environment-of-environments.adoc +++ b/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 -<> were taken in one cloud agent session on that date and are -reproducible with `tools/environments/probe-reachability.sh`. +<> 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 @@ -77,7 +77,7 @@ so, not pass silently. |=== [[measured]] -== Measured facts from one agent session +== 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 @@ -107,7 +107,7 @@ to HEAD, 200 or 206 to GET). |`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. Cargo does not install through this API, so the refusal does not block `cargo install`. -|`index.crates.io/ju/st/just`, `static.crates.io/…/just-1.56.0.crate` |200 (HEAD); 206 and 200 (GET) |*Reachable.* These are the sparse index and crate download `cargo install` uses, so a Cargo install is expected to work here. One was not attempted. The download host ignores the byte range. +|`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. diff --git a/tests/setup_install_test.sh b/tests/setup_install_test.sh index fd6bcc2..352af63 100644 --- a/tests/setup_install_test.sh +++ b/tests/setup_install_test.sh @@ -2,6 +2,8 @@ # SPDX-License-Identifier: MPL-2.0 # Test installer fallback paths without networking or installing dependencies. set -euo pipefail +# install_just_with_cargo prefers CARGO_INSTALL_ROOT; the stub expects CARGO_HOME. +unset CARGO_INSTALL_ROOT repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" fixture_root="$(mktemp -d)" @@ -28,10 +30,18 @@ SH printf '#!/bin/sh\nexit 1\n' > "$fixture_root/bin/sudo" # an apt repository without just chmod +x "$fixture_root/bin/cargo" "$fixture_root/bin/sudo" +# The fallback run gets only the utilities it needs, linked into one +# directory, so a just installed on this machine cannot satisfy the lookup +# before the Cargo stub runs. +mkdir -p "$fixture_root/sysbin" +for tool in sh mkdir chmod head; do + ln -s "$(command -v "$tool")" "$fixture_root/sysbin/$tool" +done + for manager in apt unknown; do rm -rf "$fixture_root/cargo-home" FIXTURE_ROOT="$fixture_root" MANAGER="$manager" CARGO_HOME="$fixture_root/cargo-home" \ - PATH="$fixture_root/bin:/usr/bin:/bin" sh -eu <<'SH' + PATH="$fixture_root/bin:$fixture_root/sysbin" "$fixture_root/sysbin/sh" -eu <<'SH' . "$FIXTURE_ROOT/functions.sh" PKG_MGR="$MANAGER" curl() { echo 'Unexpected download' >&2; exit 99; } diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc index 1c7c27f..15f9cab 100644 --- a/tools/environments/README.adoc +++ b/tools/environments/README.adoc @@ -33,8 +33,11 @@ into an entry's `measured` block, with the date. `reachable` means the request returned 2xx or 3xx (206 for a ranged GET). `range-ignored` means a `--get` request was answered with the whole body, -so curl stopped at the 64 KiB cap: the host answered and serves the file, -but cannot resume a download. A host that answers some tries and resets +so curl stopped at the 64 KiB cap: the host answered and ignored the +range. The probe does not inspect the body, so this does not show the +file is served (an error page over 64 KiB looks the same). +The probe asks only for the first byte, so it does not show whether the +host can resume a download. A host that answers some tries and resets others is recorded under `intermittent` with the counts seen. `refused` is a 403 from the environment's proxy. `auth-required` is a 401: the host answered and wants a token, which the probe does not supply. `tls-failed` means the diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml index a9f13ed..be0bac3 100644 --- a/tools/environments/environments.kyaml +++ b/tools/environments/environments.kyaml @@ -22,7 +22,7 @@ record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"}, environments: [ {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}}, - {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-11-04", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (24 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET capped at 64 KiB)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com (GET range-ignored: answers 200 with the whole archive, capped)", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "index.crates.io (Cargo's sparse index)", "static.crates.io (crate download; GET range-ignored, capped)", "releases.lean-lang.org", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org (GET range-ignored, capped)"], intermittent: ["isabelle.in.tum.de (HEAD 200; GET 206 on 1 of 4 tries, the rest reset during the TLS handshake, curl exit 35)"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io/api (HEAD and GET 403; Cargo does not use it to install)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the 2026-10-27 Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was not observed. One-byte GETs show asset bytes can flow, not that a full download or a run is permitted. On 2026-11-04 the Mizar distribution was downloaded and inspected with file(1) without being run"}}, + {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-11-04", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (24 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET capped at 64 KiB)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com (GET range-ignored: answers 200 with the whole archive, capped)", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "index.crates.io (Cargo's sparse index)", "static.crates.io/crates/just/1.56.0/download (the route Cargo downloads from; GET range-ignored, capped)", "releases.lean-lang.org", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org (GET range-ignored, capped)"], intermittent: ["isabelle.in.tum.de (HEAD 200; GET 206 on 1 of 4 tries, the rest reset during the TLS handshake, curl exit 35)"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io/api (HEAD and GET 403; Cargo does not use it to install)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the 2026-10-27 Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was not observed. One-byte GETs show asset bytes can flow, not that a full download or a run is permitted. On 2026-11-04 the Mizar distribution was downloaded and inspected with file(1) without being run"}}, {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}}, {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}}, {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}}, diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt index b9a3b2f..040ba9d 100644 --- a/tools/environments/hosts.txt +++ b/tools/environments/hosts.txt @@ -24,7 +24,9 @@ https://crates.io/api/v1/crates/just # What `cargo install` actually uses: the sparse index and the crate download. # A refusal of the API above says nothing about these. https://index.crates.io/ju/st/just -https://static.crates.io/crates/just/just-1.56.0.crate +# The download is the index's "dl" (https://static.crates.io/crates) plus +# /{crate}/{version}/download, which is the route Cargo requests. +https://static.crates.io/crates/just/1.56.0/download https://releases.lean-lang.org/ https://ftp.gnu.org/gnu/guix/ diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index 54df3bb..42f8974 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -42,7 +42,9 @@ if [ "$METHOD" = "get" ]; then # -r 0-0 asks for one byte. A server may ignore the range and send the # whole body, so --max-filesize caps the transfer: curl aborts (exit 63) # before reading a body whose length is declared above the cap, or once a - # chunked body passes it. The body goes to /dev/null either way. + # chunked body passes it (measured with curl 8.5.0; an older curl may + # enforce the cap only on a declared length, and --max-time still bounds + # the transfer). The body goes to /dev/null either way. request=(-r 0-0 --max-filesize 65536) else request=(-I) diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc index 15204fa..9344108 100644 --- a/tools/proof-toolchain/DESIGN.adoc +++ b/tools/proof-toolchain/DESIGN.adoc @@ -65,8 +65,10 @@ proves it runs. Roles are listed below. |`toolchain.lock.json` |Tool-owned lock, written only by the bundle build (I-JSON, JCS). Records the -resolved version, the source URL and the SHA-256 of every input, and the -SHA-256 of the produced bundle and image digest. Never hand-edited. +resolved version, the source URL and the SHA-256 of every input, the +SHA-256 of each tool's installed entry-point executable (the value +`doctor` compares as `locked_sha256`), and the SHA-256 of the produced +bundle and image digest. Never hand-edited. |Bundle build (CI) |A workflow on a full-network runner builds every tool into the fixed prefix From 918faf3d629ef8c7a27a55b7e52cae15e99c9d5c Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Wed, 4 Nov 2026 23:12:52 +0000 Subject: [PATCH 16/16] docs: clarify Cargo install root selection and reachability classification --- build/setup.sh | 4 ++++ tools/environments/probe-reachability.sh | 7 +++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/build/setup.sh b/build/setup.sh index ae7380c..e5197af 100755 --- a/build/setup.sh +++ b/build/setup.sh @@ -132,6 +132,10 @@ 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." diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh index 42f8974..68d93f1 100755 --- a/tools/environments/probe-reachability.sh +++ b/tools/environments/probe-reachability.sh @@ -61,10 +61,9 @@ fi # classify — print one outcome label to stdout. # Takes the final HTTP status after redirects and curl's exit code. Exit 60 -# yields tls-failed; exit 63 with a status (the --get size cap tripped -# because the host ignored the range) yields range-ignored, a host that -# answered; any other non-zero exit or HTTP 000 yields unreachable, -# regardless of the HTTP status. With a zero exit, 401 yields auth-required, +# yields tls-failed; exit 63 with a code other than 000 yields range-ignored. +# Any remaining non-zero exit or HTTP 000 yields unreachable. With a zero +# exit, 401 yields auth-required, # 403 yields refused, 2xx/3xx yields reachable, and all other codes yield # http-. A failed probe is reported as a label, not an error status. classify() {