From 05b1defd214dc4b47fa9e6951d80772aae7218ab Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 22 Oct 2026 16:18:52 +0000 Subject: [PATCH 1/4] docs: add Bactrian verification plan and preflight Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .machine_readable/bactrian/authorities.lock | 13 + docs/README.adoc | 1 + .../BACTRIAN-IMPLEMENTATION-PLAN.adoc | 292 +++++++++ .../BACTRIAN-VERIFICATION-SPEC.adoc | 618 ++++++++++++++++++ docs/status/BACTRIAN-ULTRAPLAN.adoc | 557 ++++++++++++++++ scripts/bactrian/doctor.sh | 117 ++++ tests/bactrian/doctor_test.sh | 51 ++ 7 files changed, 1649 insertions(+) create mode 100644 .machine_readable/bactrian/authorities.lock create mode 100644 docs/architecture/BACTRIAN-IMPLEMENTATION-PLAN.adoc create mode 100644 docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc create mode 100644 docs/status/BACTRIAN-ULTRAPLAN.adoc create mode 100755 scripts/bactrian/doctor.sh create mode 100755 tests/bactrian/doctor_test.sh diff --git a/.machine_readable/bactrian/authorities.lock b/.machine_readable/bactrian/authorities.lock new file mode 100644 index 0000000..a229090 --- /dev/null +++ b/.machine_readable/bactrian/authorities.lock @@ -0,0 +1,13 @@ +# SPDX-License-Identifier: MPL-2.0 +# Bactrian canonical authority lock, schema 1. +# TSV columns: authoritysource-revisioncanonical-artifact-sha256 +# UNPINNED is deliberate until the canonical source/artifact is checked and approved. +# Never replace an unknown revision or digest with a guessed value. +MPR UNPINNED UNPINNED +choreographic-types UNPINNED UNPINNED +secret-types UNPINNED UNPINNED +echo-types UNPINNED UNPINNED +epistemic-types UNPINNED UNPINNED +occupancy-types UNPINNED UNPINNED +tropical-types UNPINNED UNPINNED +ECHIDNA UNPINNED UNPINNED diff --git a/docs/README.adoc b/docs/README.adoc index dc7274f..96ca513 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -13,6 +13,7 @@ and CI fails if it goes stale, so prefer it over any hand-written listing. * link:onboarding/QUICKSTART-MAINTAINER.adoc[QUICKSTART-MAINTAINER] — maintaining one. * link:AI_INSTALLATION_GUIDE.adoc[AI_INSTALLATION_GUIDE] — for an AI agent instantiating the template. * link:EXPLAINME.adoc[EXPLAINME] — how the pieces actually work. +* link:status/BACTRIAN-ULTRAPLAN.adoc[Bactrian Ultra-Plan] — task-by-task implementation handoff, dependencies, acceptance evidence, and contributor rules. == The tracks diff --git a/docs/architecture/BACTRIAN-IMPLEMENTATION-PLAN.adoc b/docs/architecture/BACTRIAN-IMPLEMENTATION-PLAN.adoc new file mode 100644 index 0000000..ab085df --- /dev/null +++ b/docs/architecture/BACTRIAN-IMPLEMENTATION-PLAN.adoc @@ -0,0 +1,292 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Bactrian Implementation Plan +:toc: +:toclevels: 3 + +== Purpose + +This plan translates link:BACTRIAN-VERIFICATION-SPEC.adoc[the architecture and +soundness contract] into an orderable implementation backlog. The goal is not to +make an attractive `dune build @verify` alias that runs partial checks. The goal +is an end-to-end vertical slice whose final status cannot be confused with +preflight, testing, bounded evidence, or an incomplete warrant. For the +agent/maintainer handoff and individually actionable work packages, see the +link:../status/BACTRIAN-ULTRAPLAN.adoc[Bactrian Ultra-Plan]. + +== Repository reconnaissance and current state + +The checkout currently has no OCaml compiler, Dune, Why3, Apalache, Idris2, Zig, +Dedukti, Coq, Lean, or selected ECHIDNA command on `PATH`. It has template +Idris2/Zig ABI examples, but no Bactrian PPX, IR, Dune project, frontend, +proof-engine adapter, or authority pins. The canonical proof repositories and +artifact hashes have not been locally established in this worktree. Therefore +no proof-producing implementation can presently be compiled or tested here. + +The first executable contribution is deliberately modest and truthful: +`scripts/bactrian/doctor.sh` inventories tool and integration readiness, checks +the authority lock shape, and exits blocked until implementation exists. It +never parses OCaml or reports proof. `tests/bactrian/doctor_test.sh` tests that +contract. `.machine_readable/bactrian/authorities.lock` records upstream +identities as `UNPINNED`; these values must be replaced only after inspecting +the canonical source/artifacts and recording their real revisions and SHA-256 +digests. Do not infer a pin from a package name or a current branch head. + +=== First execution on a provisioned developer machine + +[source,sh] +---- +bash tests/bactrian/doctor_test.sh +scripts/bactrian/doctor.sh +---- + +The first command should pass. The second is expected to exit `2` with this +checkout's current blockers. To reach “preflight READY”, install and pin the +required toolchain, select the ECHIDNA adapter, approve real authority pins, and +implement the named Dune modules. Even then the doctor is only a readiness +check; only the full proof pipeline may issue proof status. + +== Target source tree + +Add components in this dependency order; do not start by wiring a broad CI +matrix around empty modules. + +[source,text] +---- +src/ + ppx/ compiler-libs PPX, source maps, post-expansion firewall + core/ versioned Core Spec IR and canonical serialization + frontend/ typed AST -> Core Spec IR; subset and totality checks + why3/ IR -> Why3 tasks, proof/certificate adapter + actors/ protocol model, K-CUT and Apalache adapters + abi/ OCaml binding manifest, Idris2/QTT and ZigProve import + driver/ Dune-facing CLI, statuses, cache keys and proof bundles +config/bactrian/ profile, runtime/backend target, trust policy +fixtures/ + accepted/ small positive examples, one feature per fixture + rejected/ unsupported syntax and soundness counterexamples + mutation/ expected killed mutants for vacuity/sensitivity checks +tests/bactrian/ unit, golden, integration, and fail-closed tests +---- + +Suggested modules are deliberately narrow: + +* `core/ir.ml`: typed IR data model, version, stable serialization, source map. +* `ppx/firewall.ml`: expansion provenance and rejection of unsupported AST + forms; no source-text grep used as a soundness boundary. +* `frontend/typed_ast.ml`: compiler-version-specific AST adapter, name + resolution, local call graph, capability and totality obligations. +* `why3/translate.ml`: only the approved pure fragment and explicit machine + integer semantics; unsupported nodes are errors. +* `actors/protocol.ml`: process transition model, queue HWM, links, monitors, + transport fault assumptions, and causal-reply check. +* `abi/manifest.ml`: binding signature/layout/ownership/source hashes and + target-runtime identity. +* `driver/status.ml`: typed state (`Preflight`, `Tested`, `Bounded`, + `Incomplete`, `Complete`, `Failed`); no implicit conversion to `Complete`. + +Compiler-libs node matching is isolated in `ppx/` and `frontend/`, allowing +compiler upgrades to be reviewed as semantic changes. Do not expose raw +`Parsetree` outside those modules. + +== Sequenced delivery plan + +=== Milestone 0 — Pin inputs and provision the build + +* Choose the first supported target explicitly: an OCaml native program + interacting with a named BEAM node/runtime adapter, or a specific + OCaml-on-BEAM runtime. “BEAM compatible” is not a target specification. +* Identify canonical Agda source repositories, theorem/module names, exact + commits, generated artifact paths, licenses, and artifact digests. Get these + from their owners/canonical map; do not guess repository URLs or commits. +* Identify the ECHIDNA invocation/API and the actual formats for strict + Dedukti witnesses, INCOMPLETE Warrant, batch Coq/Lean requests, and COMPLETE + Receipt. Make a tiny adapter contract test with a deliberately invalid + witness and a stale digest. +* Pin OCaml, Dune, Why3, SMT backend, Apalache, Idris2, Zig/ZigProve, + Dedukti, Coq, Lean, and runtime headers/toolchain in the repository's + reproducible provisioning mechanism. Record target triple and flags. +* Populate `authorities.lock` only after each pin's provenance has been + independently checked. The doctor must pass its pin-format checks, and a + separate lock test must detect missing, duplicate, stale, and altered rows. + +*Acceptance:* reproducible provisioning identifies exact versions; a clean +checkout can run the doctor; authority adapter rejects a modified artifact; +no source-verification status is emitted yet. + +=== Milestone 1 — Dune skeleton and fail-closed command model + +* Add `dune-project`, pinned opam package metadata, executable/library stanzas, + and a `bactrian` driver command with `doctor`, `check-ast`, and eventually + `verify` subcommands. +* Define textual statuses and stable exit codes. `doctor` may succeed for + readiness; `check-ast` may report syntactic acceptance; neither writes a + proof receipt. `verify` must fail until each mandatory obligation has a + checked witness and ECHIDNA COMPLETE Receipt. +* Establish `dune build @verify` as the single release-facing gate. It invokes + only locked, declared dependencies and exits nonzero for missing tools, + missing proof adapters, timeouts, unknown syntax, unproved VCs, or incomplete + receipts. Add a separate `@preflight` alias so partial success cannot be + mistaken for verification. +* Add deterministic build IDs from source hashes, compiler and PPX versions, + tool flags, IR schema, imported authority digests, target ABI and model + bounds. Initially disable proof caching until cache-key tests pass. + +*Acceptance:* clean build emits “blocked/incomplete” rather than success when +an engine is absent; stale artifacts cannot satisfy `@verify`; repeat runs +produce the same preflight report. + +=== Milestone 2 — Layer A smallest useful proof + +Implement an end-to-end accepted fragment in this order: + +. One monomorphic ADT, integer constants, constructors, exhaustive match, and + immutable records. +. Non-recursive pure `let` and local pure functions, with a resolved local + call graph. Reject unknown or external calls by default. +. `[@pre]` / `[@post]` parsing and a clearly versioned logic expression + language; contracts are not arbitrary OCaml evaluation. +. A small arithmetic semantics (start with mathematical integers; introduce + fixed-width arithmetic only with explicit overflow rules). +. Structural recursion plus a termination obligation; reject general + recursion until a well-founded-measure path is implemented. +. Why3 VC generation, solver execution, independently checked certificate or + proof reconstruction, and strict Dedukti witness production/checking. + +Every accepted fixture must have a corresponding rejected mutant. Cover +`Obj.magic`, `Unsafe_*`, aliased `Sys.command`, unknown PPX expansion, an +external declaration, hidden mutation, incomplete match, unsupported call, +recursive non-decrease, and contract vacuity. The typed-AST pass resolves +module aliases and opens; source grep is defense-in-depth only. + +*Acceptance:* one small function reaches ECHIDNA with a source-mapped VC and +checked receipt; mutating its postcondition makes the gate fail. Do not broaden +the subset until each existing fixture remains stable across a compiler pin. + +=== Milestone 3 — Capability and TINI integration + +* Map Core IR capability sets to MPR Sigma and reject authority by default. +* Map secret labels and observable outputs to `secret-types` TINI obligations. +* Invoke R5 composition on module and whole-program summaries, not only each + function in isolation. +* Transport evidence through `echo-types` / `epistemic-types` certificates, + validating exact theorem, assumptions, and hash provenance. + +*Acceptance:* a direct forbidden capability and an `fs.read` + `net.send` +composition are rejected; a permitted pure module is accepted; manifest drift +invalidates all derived artifacts. + +=== Milestone 4 — Layer B protocol vertical slice + +Start with exactly two roles, one request type, one correlated reply, a bounded +mailbox, and crash points around receive/commit/reply. Then: + +* Elaborate the concrete choreography syntax to transitions, including + selective receive and in-flight messages. +* Import `occupancy-types` HWM bounds and reject a capacity claim with no + arrival/service assumptions or overflow policy. +* Call the canonical K-CUT loss/knowledge interfaces and preserve their loss + residue and assumptions in the proof bundle. +* Run Apalache for bounded counterexample search with explicit bounds and + bounded-only status. Prove any promoted theorem via a checked abstraction or + inductive invariant; never promote BMC by itself. +* Add the killer test: commit happens, reply is lost; sender does not know + commit. Removing the reply must make the elaborator reject any + `remote_committed` assertion regardless of whether bounded search finds a + counterexample. + +*Acceptance:* correlated causal reply is the only transition that establishes +acknowledged commitment; lost reply leaves sender uncertain; HWM overflow and +crash traces are reported; loss/reordering assumptions are explicit. + +=== Milestone 5 — Layer C one primitive + +* Pick one pure deterministic Zig primitive whose input size has a finite + explicit bound. Define Idris2 QTT input/output, integer range, ownership, + error and linear-resource protocol. +* Generate the OCaml declaration and C header from the manifest; handwritten + `external` declarations remain rejected. +* Pin the runtime version and implement a wrapper that uses its actual GC root, + custom block, exception, and callback APIs. Do not assume + `caml_reserve_custom` is a public portable API; prove the selected adapter. +* Use ZigProve to link the exact implementation hash to the Idris2 signature + and postcondition. Test ABI layout, null/error handling, allocation failure, + finalization, double release, and exception/unwind paths. +* Prove MaxPlus cost with input-size and wrapper costs. Establish a sound + target-specific conversion to the scheduler's 1 ms budget. If not established, + disable scheduler-thread invocation and exercise the worker/nonblocking + path instead. + +*Acceptance:* mutation of symbol, signature, layout, ownership, source hash, or +cost bound is rejected; all GC and error paths are covered; no wall-clock +benchmark is treated as a WCET proof. + +=== Milestone 6 — Full proof transport and release gate + +* Define ECHIDNA adapter input/output schemas and bind every obligation to the + canonical IR hash and assumption set. +* Run ECHIDNA strict Dedukti validation followed by batch Coq + Lean checks. +* Validate INCOMPLETE Warrant versus COMPLETE Receipt state transitions and + receipt issuer/signature/checker identity. Invalid, stale, missing, or + mismatched receipts are rejected. +* Run `mutation.rs` for antecedent satisfiability, postcondition sensitivity, + causal-reply deletion, and ABI tampering. Mutation testing supplements—not + replaces—proof checking. +* Enable deterministic caches only after adversarial cache-key tests. + Release CI requires COMPLETE for all mandatory proof obligations; local + bounded or partial profile remains explicitly non-release. + +*Acceptance:* clean reproducible build reaches `dune build @verify`, produces a +COMPLETE receipt bound to source/toolchain/authority hashes, kills all required +mutations, and fails on any single missing checker or changed byte. + +== Implementation rules and decision log + +. **No fake green:** tool availability, parser acceptance, unit tests, SMT + `unsat`, bounded model checking, and a local Warrant are distinct statuses; + none alone means COMPLETE. +. **No fabricated upstream identity:** this branch records upstream authorities + by names supplied in the design, but not their repository locations, + revisions, theorem signatures, or hashes until those are verified. +. **No source grep as AST security:** the OCaml compiler frontend and expanded + typed AST define the input to the firewall. A text scanner may add warnings, + never admit code. +. **No runtime-general claim:** proofs name one compiler/runtime/target triple + at a time. Every upgrade re-runs ABI and semantic conformance suites. +. **No silent downgrade:** unsupported AST, missing assumptions, failed proof + reconstruction, bounded-only protocol evidence, or missing mutation tool + prevents COMPLETE. +. **One vertical slice first:** get a tiny sequential proof through full + receipt closure before implementing the distributed and ABI layers in + parallel. Keep the cross-layer interfaces versioned from the outset. + +== Immediate backlog + +[cols="1,3,2",options="header"] +|=== +| Order | Work item | Done when + +| 1 +| Run and refine `bash tests/bactrian/doctor_test.sh`; confirm blocked output is + accurate on a provisioned maintainer host. +| Test passes and never calls a blocked checkout “verified”. + +| 2 +| Owner/maintainer identifies canonical source locations and selects the first + OCaml/BEAM target and ECHIDNA adapter contract. +| Exact identities and interfaces can be recorded without guessing. + +| 3 +| Pin/install the compiler and Dune toolchain; create the Dune skeleton and + test `@preflight`/fail-closed `@verify` behavior. +| Reproducible build succeeds; `@verify` fails honestly before engine wiring. + +| 4 +| Implement compiler-libs firewall plus positive/negative AST fixtures. +| Aliases and expansion are checked; no text-only admission path exists. + +| 5 +| Deliver a tiny Layer A end-to-end proof and mutation campaign. +| Source -> IR -> VC -> `.dk` -> ECHIDNA COMPLETE succeeds on one fixture. + +|=== diff --git a/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc b/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc new file mode 100644 index 0000000..c294bc7 --- /dev/null +++ b/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc @@ -0,0 +1,618 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Bactrian: Architecture, Soundness Contract, and MVP Roadmap +:toc: +:toclevels: 3 + +== Status and scope + +This is the proposed architecture and implementation contract for Bactrian, a +verification suite for a deliberately restricted OCaml subset and OCaml code +that participates in BEAM-style actor protocols. It is not a claim that this +checkout already contains a working verifier or that the external estate +libraries named here have been vendored, built, or audited in this repository. +The current checkout contains Idris2 ABI scaffolding under +`src/interface/Abi/` and Zig build scaffolding, not a Bactrian PPX, Why3 +translator, Apalache adapter, ECHIDNA client, or proof receipt verifier. + +The design treats the named canonical Agda developments as upstream authorities +and consumes version-pinned artifacts from them. Bactrian MUST NOT fork or +silently restate their theorems. Integration becomes supported only when a +manifest pins each upstream commit, module/theorem name, artifact digest, and +checker version, and the CI gate verifies that manifest against the actual +artifacts. In particular, no local status document or PPX annotation by itself +constitutes a proof. + +== Goals and trust boundary + +Bactrian accepts source plus its complete preprocessing environment, compiles a +small, explicit language into a shared Idris2 Core Spec IR, and routes proof +obligations to the checker suited to each layer. The acceptance result is a +machine-readable proof bundle that links source spans and normalized-AST hashes +to obligations, solver/model-checker outputs, strict Dedukti witnesses, and the +final ECHIDNA receipt. + +The top-level judgment is intentionally layered: + +[source,text] +---- +Source --PPX firewall--> Normalized AST --elaboration--> Core Spec IR + Layer A: IR functional fragment --Why3/SMT--> strict .dk witness + Layer B: IR process protocol --K-CUT + Apalache--> strict .dk witness + Layer C: ABI manifest + Zig implementation --Idris2 QTT/ZigProve--> .dk witness + all witnesses --> ECHIDNA --> COMPLETE Receipt +---- + +Why3/SMT, Apalache, ZigProve, and local checks can produce evidence for a +candidate obligation, but they do not independently issue a COMPLETE result. +ECHIDNA's strict Dedukti check and batch Coq + Lean validation are the closure +boundary. Before that closure, the result is at most an INCOMPLETE Warrant. +Missing evidence, timeout, unsupported syntax, stale artifact, or disagreement +is a hard failure or an explicitly incomplete result, never a green proof. + +=== Three verification layers + +[cols="1,2,3,3",options="header"] +|=== +| Layer | Subject | Main engines | Soundness claim (conditional on checked artifacts) + +| A — Sequential functional OCaml subset +| Pure, total functions over supported ADTs and immutable values. +| OCaml compiler-libs AST gate; Why3 VC generation; SMT; strict `.dk` witness. +| Functional contracts hold for all values in the modeled domain. No claim +about effects, runtime scheduling, or code outside the accepted AST. + +| B — Actor, mailbox, and protocol layer +| State machines, sends/receives, crashes, bounded queues, and causal reply +protocols. +| `choreographic-types` K-CUT artifacts; Apalache bounded model checking; +Why3 where applicable; strict `.dk` witnesses. +| The modeled protocol respects its safety properties within the declared +fault and queue assumptions. Bounded checking alone is not an unbounded proof. + +| C — OCaml / Idris2 ABI / Zig foreign boundary +| C ABI signatures, ownership, roots/handles, layouts, and bounded native work. +| Idris2 `%default total` QTT specification; ZigProve; `tropical-types` +MaxPlus bounds; runtime adapter checks; ECHIDNA closure. +| The exact imported implementation satisfies the pinned ABI contract and +budget assumptions. No unverified FFI, runtime version, or binary substitution. +|=== + +== Existing tooling contrast + +Bactrian complements rather than replaces OCaml's type system and testing. + +* OCaml's standard type system, including GADTs and extensible type-indexed + encodings, establishes typing properties. It does not generally prove + functional postconditions, total termination, distributed causal knowledge, + mailbox bounds, or properties of a C/Zig implementation. +* `ppx_assert` and `ppx_inline_test` provide executable assertions and inline + tests. They observe selected executions; they are not universal proofs and + do not close a foreign ABI proof. +* `qcheck` and `crowbar` provide property-based testing and fuzzing. These are + valuable counterexample finders and remain complementary, but finite runs do + not establish universal correctness or K-CUT knowledge claims. +* Infer and SLAM are static-analysis approaches for finding classes of bugs + (with capabilities depending on frontend, configuration, and analysis). + Bactrian's distinction is an explicit restricted source semantics, named + proof obligations, imported proof witnesses, and an end-to-end checked + receipt—not a claim that those analyzers are ineffective or subsumed. + +The recommended development loop uses all of them: prove what is in scope, +run tests and fuzzers for implementation defects, and require the proof gate to +reject unsupported or unproved code. + +== Layer A — sequential functional subset + +=== Accepted language + +The initial subset is intentionally smaller than OCaml. The PPX operates on the +compiler-libs parsed and typed AST for one pinned OCaml compiler version; the +compiler version, PPX versions, command line, include paths, generated source, +and dependency interface hashes are part of the proof input. + +Accepted constructs in MVP: + +* algebraic data type declarations with finite, explicitly declared + constructors, including parameterized ADTs supported by the IR; +* exhaustive pattern matching over those ADTs and supported primitive values; +* immutable tuples, records, lists, and explicitly modeled persistent maps; +* `let` bindings, pure function application, and a small total primitive set + (integer arithmetic with explicit mathematical or checked machine semantics, + structural equality on supported types, and pure constructor operations); +* structurally recursive functions, or functions with an explicit natural + measure and a discharged well-founded decrease proof; +* pure helper functions whose complete transitive call graph is also accepted. + +Rejected unless separately modeled and proved: mutation and references, arrays, +exceptions as control flow, lazy values, objects, first-class modules, dynamic +loading, callbacks into unverified code, threads/domains, polymorphic +comparison/hash, native integers with unspecified overflow semantics, and all +ambient effects. Unsupported constructs fail closed; the PPX does not erase +them or approximate them. + +A totality check is not a syntax heuristic. Recursive calls are extracted into +termination VCs and discharged by Why3/SMT or a checked proof. Structural +recursion is accepted only when the recursive argument is a strict subterm +under the supported datatype semantics. The obligation records the measure and +each recursive call site. + +=== Deterministic PPX expansion firewall + +The PPX gate runs before proof translation and after all user PPX expansion. +It records a canonical serialization/hash of both the source and final AST, +checks deterministic expansion (same pinned inputs produce the same output), +and rejects an unknown or nondeterministic rewriter. A second audit of the +post-expansion AST is mandatory: scanning source text alone is insufficient. +The allowlist is semantic and node-based, not a list of suspicious spellings. + +The gate rejects, at minimum: + +* `Obj.magic`, `Obj` representation access, unsafe casts, and any identifier + or module under the configured `Unsafe_*` namespace family; +* `Sys.command`, `Unix.system`, process spawning, shell execution, and file, + system, port, or ambient process APIs not represented by an explicit + capability in the verified model; +* `external` declarations, `[%raw ...]`, Ctypes/dynamic symbols, and all FFI + bindings without an exact Layer C ABI manifest and receipt; +* unexpanded extensions, generated code without provenance, unknown PPX + rewriters, and compiler-libs nodes outside the versioned allowlist. + +Name resolution is performed on typed identifiers, including aliases and +module opens. The firewall also checks the transitive implementation/interface +closure: renaming `Sys.command` or hiding it behind a local module cannot +bypass the rule. Capability policy imports MPR's capability-footprint Sigma; +ambient `File`, `System`, `Port`, and `Sys.command` authority is denied unless +an explicitly modeled capability is present. Layer A's initial profile grants +none. + +=== Contracts and Face annotation surface + +The public contract surface is a PPX syntax that elaborates, rather than +executes. Expressions inside contracts belong to a restricted, pure logic +fragment with no effects and no unbounded quantification unsupported by the +backend. Logical values are translated to shared Core Spec IR, not evaluated +as OCaml callbacks. + +[source,ocaml] +---- +let[@pre x >= 0] + [@post fun result -> result >= 0] + normalize x = + [%cap pure] + if x = 0 then 0 else x +---- + +`[%cap ...]` declares the required capability footprint. `[@pre ...]` and +`[@post ...]` attach precondition and postcondition predicates to the nearest +function/value declaration. `[@secret ...]` labels data with its confidentiality +class and source for the TINI policy. The choreography extension is written in +source documentation as `[%\@choreography ...]` to make the intended Face +marker unambiguous; because `@` is not a valid OCaml extension-name character, +the concrete MVP parser spelling is `[%bactrian.choreography ...]`. A frontend +may reserve the former notation for a future lexer/parser, but must not claim it +is accepted by stock OCaml syntax. + +[source,ocaml] +---- +let[@pre delta >= 0] + [@post fun next -> next.version = state.version + 1] + apply_delta state delta = + [%cap pure] + { state with value = state.value + delta; + version = state.version + 1 } +---- + +Contract elaboration generates obligations for precondition well-formedness, +postcondition under precondition, termination, arithmetic semantics, and +capability non-escalation. Secret labels flow into TINI obligations. Composite +capabilities are checked with the canonical `secret-types` MPR R5 composition +rule so separate `fs.read` and `net.send` components cannot be composed into an +unapproved exfiltration corridor. + +=== Core Spec IR + +All three frontends elaborate to one versioned, typed IR. The minimum schema is: + +[source,text] +---- +Module(hash, compiler, ppx_chain, imports, declarations) +Decl(name, type, body, requires, ensures, decreases, capabilities, labels, span) +Expr = Var | Literal | Construct | Match | Let | Apply | PurePrim +Protocol = Role | State | Send | Receive | Timeout | Crash | Monitor | Choice +Foreign = AbiSymbol | IdrisTypeHash | ZigSourceHash | Layout | Ownership | Budget +Obligation(id, kind, formula, assumptions, source_map, provenance) +---- + +IR versions are immutable and hashed. Each obligation includes an explicit +assumption set, including integer model, mailbox/failure bounds, runtime ABI, +compiler and imported theorem digests. A proof without the matching assumption +and source hashes is invalid. Source maps preserve PPX expansion origins to the +user-authored location and generated node. + +== Layer B — actor protocols, mailboxes, and K-CUT + +=== Process transition model + +A process is modeled as `(pid, local_state, mailbox, status, links, monitors)`. +A transition is one of local pure state reduction, enqueue/send, dequeue/receive, +link or monitor update, timeout, crash, or restart. The scheduler is an explicit +transition relation; it does not assume FIFO across independent senders unless +the selected transport contract establishes that property. Per-sender ordering, +if guaranteed by the target runtime, is stated as an assumption and checked by +the adapter conformance tests. + +Mailboxes use selective receive: a receive transition scans for the first +message matching the source pattern and leaves unmatched messages queued. The +model records queue length and scan work separately. `occupancy-types` supplies +the canonical high-water-mark (HWM) queue bound. Every protocol must declare +its bound, enqueue/dequeue policy, overflow response, and whether queue capacity +is static, token-bucket bounded, or conditional on an arrival/service curve. +Unbounded arrival rates cannot be waved away by a finite Apalache bound. + +The model includes links (coupled exit/crash propagation when configured), +monitors (one-way termination notification), and explicit `DOWN`/exit +messages. A link or monitor is not a message acknowledgement and provides no +proof that a remote state transition committed. Crashes may occur between +receive, local state update, send, and persistence points; each is a separate +transition where relevant. + +=== Loss, reordering, and proof meaning + +Transport assumptions are protocol parameters, not implicit truths. The +fault model may allow loss, duplication, delay, and reordering, constrained only +by the specified delivery assumptions. Messages in flight are represented in +the global state, so asynchronous cut reasoning includes messages not yet +received. For permitted loss, a liveness theorem needs an explicit fairness, +retry, or failure-detection assumption; safety cannot infer eventual delivery. + +Bactrian imports `choreographic-types` rather than reconstructing its +`K-CUT-LOSS` and `K-CUT-WARRANT` results. K-CUT-LOSS tracks structured loss +residues for synchronous and asynchronous cuts, including in-flight messages. +K-CUT-WARRANT bounds what each role can know at a Kripke cut. The checker emits +an obligation that connects every generated protocol transition and cut to the +pinned canonical theorem interfaces and records the loss residue in the proof +bundle. `echo-types` and `epistemic-types` `ProofTransport` certificates carry +proof provenance across adapters; transport does not strengthen the theorem. + +==== Mandatory causal-reply rule + +The confirmed async falsifier is a hard elaboration rule: **a successful +asynchronous send does not establish that the receiver has received, applied, +or committed the requested state.** No contract, postcondition, or generated +knowledge claim may assert remote commitment on the basis of `send` return, +queue acceptance, a link, a monitor, or a timeout. + +The only supported commitment claim requires a verified causal path: the sender +issues a request with an identity; the receiver validates and commits it under +the modeled transition semantics; and a reply causally dependent on that commit +is delivered back to the sender. The reply carries enough correlation/version +information to rule out stale acknowledgements. Under message loss, the sender +may remain uncertain forever; the spec may state eventual acknowledgement only +with explicit delivery/fairness assumptions. A timeout or `DOWN` indicates +uncertainty/failure, never successful commit. The elaborator rejects a +`remote_committed` claim lacking this send -> receive -> commit -> causal reply +chain, even if bounded model checking happens not to find a counterexample. + +=== Apalache obligations + +Apalache checks finite instances of the transition system over declared bounds: +roles, message identities, state domains, queue HWM, and step depth. The report +contains the exact bound tuple, invariants, counterexample traces, and tool +version. For bounded safety, a complete search without counterexample means +only “no counterexample within these bounds”; it is not an unbounded proof. + +Promotion to a proof obligation requires one of: (a) a canonical Agda theorem +that covers the model by a checked refinement relation, or (b) an explicit +inductive invariant/abstraction proof whose obligations close in the proof +chain. Otherwise the result stays bounded evidence and the ECHIDNA bundle must +mark it incomplete. Liveness requires a fairness declaration and a proof +appropriate to it; finite bounded exploration alone cannot certify liveness. + +== Layer C — Idris2 and Zig verified foreign boundary + +=== Exact symbol import and proof chain + +Every OCaml external is generated from a single versioned ABI manifest. The +manifest binds the OCaml declaration and C symbol to: an Idris2 `%default +total` QTT signature; C widths, alignment, calling convention and ownership; +Zig implementation source and build hashes; the ZigProve theorem/receipt; and +the exported linker symbol. The OCaml PPX refuses handwritten or mismatched +`external` declarations. Build output embeds the manifest digest, and link-time +verification checks the resolved library digest/symbol table. + +The intended chain is: + +[source,text] +---- +OCaml external + wrapper + == exact signature/layout ==> +Idris2 Core Spec (QTT, total, ownership and pre/postconditions) + == implementation correspondence ==> +Zig function + ZigProve Receipt + == MaxPlus cost proof ==> +tropical-types bound + scheduler adapter policy + == all evidence imported ==> +ECHIDNA INCOMPLETE Warrant -> Coq + Lean batch -> COMPLETE Receipt +---- + +A file named `Receipt` is not trusted by filename. The verifier validates +issuer, theorem identity, source/build hashes, assumptions, and checker results. +If the estate's actual ZigProve output format lacks an implementation +correspondence or runtime-bound theorem, that theorem is a stated MVP blocker; +Bactrian must not synthesize the missing guarantee. + +=== Heap, roots, custom handles, and linearity + +The desired safety theorem is that the foreign function cannot corrupt the OCaml +GC heap and cannot retain or dereference an invalid OCaml value. The proof is +conditional on a pinned OCaml runtime ABI and a wrapper discipline: + +* OCaml values crossing into C are rooted using the runtime's supported root + macros/registration protocol for the entire interval in which they may move + or be collected. A raw `value` is not retained across an allocation or + callback unless rooted according to that runtime version. +* Foreign code does not inspect or mutate OCaml heap blocks directly, fabricate + tagged values, or retain unrooted pointers into the moving/collectable heap. + It operates on copied, validated unboxed data or opaque handles. +* Custom blocks and handles have an explicit state machine. A linear resource + token permits exactly one reserve/acquire and one release/finalize; aliasing, + double free, use-after-release, and finalizer races are excluded by the Idris2 + QTT interface and Zig implementation proof. +* `caml_reserve_custom` is treated as a requested runtime adapter operation, + not assumed to be a portable public OCaml API. Bactrian must implement and + verify a version-specific adapter against the actual target runtime API. Its + reservation token is linear, and allocation failure/GC/exception paths must + return or release the reservation exactly once. +* C entry points use the pinned runtime's required exception/root protocol + (for example, the appropriate `CAMLparam`/`CAMLlocal`/`CAMLreturn` discipline + where applicable). No OCaml exception or non-local exit may cross an + unprepared Zig frame. + +The proof obligation includes every success, error, allocation-failure, +exception, cancellation, and finalizer path. “Zig is memory-safe” is not itself +a proof about OCaml GC integration; the correspondence proof covers the actual +C ABI wrapper and runtime adapter as well as the Zig body. + +=== MaxPlus and scheduler budget + +`tropical-types` `MaxPlus` analysis supplies a compositional worst-case cost +bound. The imported primitive theorem must connect the verified Zig C-ABI +primitive's cost to the target runtime's unit and assumptions. The requested +scheduler/preemption slice target is at most 1 ms. A native call is admitted on +the scheduler thread only if its proven upper bound, including wrapper and +marshalling overhead, is no greater than the conservative budget available +within that slice. + +A MaxPlus bound measured in instructions, cycles, or abstract steps does not +automatically imply milliseconds. The target CPU, compiler flags, frequency +assumptions, cache/memory behavior, and cost-to-time calibration must be +explicitly justified and pinned. If those assumptions do not yield a sound +`<= 1 ms` bound, synchronous admission is forbidden. The generated wrapper +must dispatch the operation to a verified non-blocking continuation or a +managed worker/thread and return control to the scheduler; the worker's own +lifetime, cancellation, and callback protocol remain modeled obligations. + +Runtime monitoring can enforce a deadline by yielding/cancelling where safe, +but measurement is not a substitute for a WCET proof. For an operation that +cannot safely yield, only a sound static bound below the threshold permits +scheduler-thread execution. This ties `tropical-types` evidence to runtime +liveness without claiming that a mathematical cost bound alone proves system +liveness. + +== Worked dual example: VeriSimDB entity actor + +The following is design-level source: `[%bactrian.choreography ...]` and +contract attributes are proposed PPX syntax, not compilable stock OCaml today. +The example separates a pure entity transition (Layer A), its acknowledgement +protocol (Layer B), and hash/drift FFI (Layer C). + +[source,ocaml] +---- +type entity = { id : int64; version : int64; digest : int64 } +type request = Update of { request_id : int64; expected : int64; payload : bytes } +type reply = Committed of { request_id : int64; version : int64; digest : int64 } + | Rejected of { request_id : int64; actual : int64 } +type message = Apply of request | Result of reply + +(* This external is generated from the pinned ABI manifest; handwritten externals + are rejected. The opaque token owns copied bytes, never an OCaml heap pointer. *) +external hash_and_drift : bytes -> int64 -> (int64 * int64) + = "caml_bactrian_hash_and_drift" + +let[@pre old.version >= 0L] + [@post fun next -> next.version = old.version + 1L] + [@post fun next -> next.id = old.id] + next_entity old payload = + [%cap pure] + let (digest, drift) = hash_and_drift payload old.digest in + if drift < 0L then Error `Invalid_drift + else Ok { old with version = old.version + 1L; digest } + +[%bactrian.choreography + roles (client, entity_store); + mailbox entity_store hwm 64 overflow reject_newest; + transport { loss = possible; duplicate = possible; reorder = possible }; + protocol UpdateCommit = + client -> entity_store : Apply(request_id, expected, payload); + entity_store: receive Apply(id, expected, payload); + entity_store: if expected = state.version then + commit(next_entity(state, payload)); + send client : Committed(id, state.version, state.digest) + else send client : Rejected(id, state.version); + client: only Committed(id, v, d) causally following Apply(id, ...) + establishes acknowledged_commit(id, v, d); + crash_points after_receive, after_commit, before_reply, after_reply; +] +---- + +Layer A proves the pure state transition's pre/postconditions and termination. +In production, `bytes` must be replaced or refined to the exact immutable byte +representation accepted by the sequential subset. The native hash/drift +operation is not assumed pure merely because its OCaml declaration looks pure: +its ABI contract asserts deterministic output for the copied input and prior +digest, no retained OCaml pointers, bounded cost, and no hidden capabilities. + +Layer B checks all request/response interleavings within declared bounds. A +client send or successful enqueue is only `submitted`; it is not +`acknowledged_commit`. After `after_commit, before_reply`, the entity may have +committed while the client remains uncertain. Retries use the same request ID +and idempotency rule (or an explicit deduplication table with its own HWM bound) +to avoid double application. The reply is correlated with the request and +carries committed version/digest. If the reply is lost, the client retries or +queries status; it never infers success from the original send. + +Layer C admits `hash_and_drift` on the scheduler thread only when the exact +ZigProve artifact and MaxPlus bound include input-length-dependent cost and +wrapper overhead and prove the configured `<= 1 ms` budget. If the input size +or bound exceeds the threshold, the PPX-generated wrapper routes execution to +the verified worker path or rejects the call. Idris2 proves the ABI type, +integer range, ownership, and linear handle protocol; ZigProve proves the body +and implementation correspondence; the runtime adapter proof establishes GC +root/exception discipline for the pinned OCaml version. + +=== ECHIDNA mutation and vacuity gate + +For every nontrivial VC, `mutation.rs` performs a vacuity campaign before +accepting the obligation set: + +. Check that each precondition is satisfiable under the declared type/domain + assumptions; report intentionally unreachable cases separately. +. Mutate each postcondition (for example, `next.version = old.version + 1` to + `next.version = old.version`) and require the proof pipeline to produce a + counterexample or fail the mutated obligation. If the mutation still proves, + flag the contract as potentially vacuous, overconstrained, or disconnected + from the implementation. +. Mutate the choreography by removing the causal reply and require the + remote-commit claim to be rejected by the syntactic/IR causal rule, not merely + pass a bounded trace search. +. Mutate the ABI manifest (symbol, width, ownership, source hash) and require + the artifact-import gate to reject it. + +Mutation testing is evidence that gates are sensitive to selected defects; it +is not a proof of completeness. Mutation seeds and outcomes are included in the +ECHIDNA bundle. The VeriSimDB example cannot be marked complete if the +`mutation.rs` vacuity check is skipped, unavailable, or reports an unexplained +surviving mutation. + +== Dune engine and developer workflow + +The target user command is: + +[source,sh] +---- +dune build @verify +---- + +The alias is a deterministic, fail-closed dependency graph, conceptually: + +. Parse and typecheck with the pinned OCaml compiler and deterministic PPX + chain; save source, dependency, toolchain, and normalized-AST hashes. +. Run the post-expansion firewall and elaborate accepted units to Core Spec IR. +. Dispatch Layer A VCs to Why3/SMT, then translate/check strict Dedukti + witnesses; retain solver versions, options, timeouts, and proof terms. +. Dispatch Layer B transition systems to Apalache with explicit bounds; link + imported K-CUT/K-CUT-WARRANT artifacts and emit proof or bounded-evidence + status without promoting a bounded result to an unbounded theorem. +. Dispatch Layer C manifests to Idris2 and ZigProve; check ABI/layout, + ownership, implementation correspondence, and MaxPlus budget. +. Run ECHIDNA `mutation.rs` vacuity/mutation checks and proof-transport + validation. +. Submit the complete obligation bundle to ECHIDNA. Local outcome is + `INCOMPLETE Warrant` until strict Dedukti plus batch Coq and Lean checks yield + a `COMPLETE Receipt`. + +Each task writes content-addressed outputs under Dune's build directory, never +into source directories. Cache keys include all source/dependency hashes, +compiler and tool versions, flags, IR version, canonical theorem manifest, +solver/model bounds, and target ABI. Cache hits still validate artifact +signatures and dependency digests. Any skipped engine, timeout, unknown +obligation, or stale cache invalidates the final receipt. The alias reports +separate `proved`, `bounded-only`, `failed`, and `incomplete` counts and exits +nonzero unless policy permits the requested verification profile; CI release +policy requires COMPLETE for all mandatory obligations. + +Proposed integration shape (not yet implemented): Dune rules invoke a single +Bactrian driver with explicit targets for PPX validation, IR generation, +Why3, Apalache, ABI verification, and ECHIDNA. The driver emits Dune +`Dynamic` dependencies only from the locked manifest; it must not discover +ambient tools or network dependencies at build time. Proof artifacts and +third-party tools are pinned/available before the hermetic build starts. + +== MVP roadmap and acceptance gates + +[cols="1,2,3,2",options="header"] +|=== +| Phase | Deliverables | Exit gate | Explicitly not claimed + +| 0. Trust inventory and manifests +| Pin OCaml compiler/PPX behavior; define Core Spec IR schema; make manifests +for MPR, choreography, secret, echo/epistemic, occupancy, tropical, ECHIDNA, +Idris2, ZigProve and runtime adapter. +| Reproducible manifest validation against upstream artifacts; fixture showing +that stale or missing theorem digests fail closed. +| No source verification yet. + +| 1. Layer A vertical slice +| PPX firewall; ADT/immutable subset; contract parser; termination extraction; +Why3 translation; strict `.dk` handoff; first `dune build @verify` alias. +| Positive and negative fixtures; reject `Obj.magic`, `Unsafe_*`, `Sys.command`, +unknown PPXs, unverified FFI; mutation test kills incorrect postcondition. +| No effects, actors, or full OCaml support. + +| 2. Capabilities and information flow +| MPR Sigma import; `[%cap]`, `[@secret]`; TINI obligations; R5 composition +checks; ProofTransport provenance. +| Tests prove ambient authority denied and exfiltration composition rejected; +upstream theorem identities and hashes verified. +| No claim beyond imported lattice and modeled capabilities. + +| 3. Layer B bounded actor model +| Protocol Face syntax; process/mailbox/crash semantics; occupancy HWM; +Apalache adapter; K-CUT loss and knowledge linkage. +| Counterexample for lost reply after commit; mandatory rejection of commitment +without causal reply; bounds and bounded-only labels are accurate. +| Bounded Apalache result is not an unbounded theorem. + +| 4. Layer C ABI vertical slice +| Idris2 QTT signature generator; pinned runtime adapter; ZigProve import; +linear handles/roots; MaxPlus budget gate and worker fallback. +| Deliberately corrupted layout/ownership/source-hash fixtures rejected; +GC/exception path obligations close for a pinned runtime; 1 ms claim has +traceable calibrated assumptions or is not admitted. +| No portable guarantee across runtimes/architectures. + +| 5. ECHIDNA closure and release profile +| Complete bundle export; `mutation.rs`; strict Dedukti; batch Coq + Lean; +receipt validation; CI/release wiring. +| `dune build @verify` yields COMPLETE on the curated suite; mutations are +killed; clean rebuild reproduces hashes; any skipped checker fails the gate. +| No soundness claim for unmodeled code or assumptions. +|=== + +=== MVP ordering and engineering rule + +Build one end-to-end example before broad language support. The first vertical +slice should be a pure arithmetic/ADT transition plus a tiny causal request / +reply actor protocol and one deterministic Zig primitive with a deliberately +small bound. It should reach ECHIDNA closure before the implementation expands +the AST, supported runtime versions, or failure model. When an upstream +canonical package or checker is not available, create an explicit adapter +interface and a failing fixture; do not replace the missing theorem with a +local assertion or a prose “proof”. + +== Repository integration and immediate next actions + +This specification belongs under `docs/architecture/` and is the design +baseline for implementation issues. The immediate code work is to establish +locked source manifests and executable conformance fixtures, then implement +Phase 0 and the Layer A vertical slice. Existing `src/interface/Abi/` files +are useful scaffolding but are template artifacts: their simplified 64-bit +layout/platform assumptions and sample pointer wrappers are not sufficient for +the OCaml/BEAM target without a new, target-specific proof and runtime adapter. + +No BeAM runtime property is inferred from an OCaml-native target. The initial +MVP should name its target precisely (OCaml native process participating in a +BEAM node, or a particular OCaml-on-BEAM runtime). Actor semantics, scheduler +budget units, mailbox behavior, GC rules, and ABI are backend-specific and +must be supplied by that target's adapter manifest before claiming verification. diff --git a/docs/status/BACTRIAN-ULTRAPLAN.adoc b/docs/status/BACTRIAN-ULTRAPLAN.adoc new file mode 100644 index 0000000..aa3b52c --- /dev/null +++ b/docs/status/BACTRIAN-ULTRAPLAN.adoc @@ -0,0 +1,557 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Bactrian Ultra-Plan: Executable Handoff and Work Breakdown +:toc: +:toclevels: 4 + +== Mission and authority + +This is the working execution plan for the Bactrian repository. It converts the +link:../architecture/BACTRIAN-VERIFICATION-SPEC.adoc[verification specification] +and link:../architecture/BACTRIAN-IMPLEMENTATION-PLAN.adoc[implementation +plan] into ordered work packages that maintainers, researchers, and coding +agents can pick up without guessing at trust boundaries or claiming unfinished +proofs. + +Authority order: + +. The approved soundness contract is + `docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc`. +. This file controls sequencing, task ownership, evidence, and handoff. +. The architecture plan gives design rationale and detailed layer milestones. +. Current status is what a command or checked artifact demonstrates—not what a + roadmap percentage, issue title, or prior agent report says. + +The checkout is at **bootstrap / pre-MVP**. The readiness checker and tests +exist; there is no Dune project, OCaml frontend, Core Spec IR, proof engine, +Apalache/ECHIDNA adapter, or target-specific runtime proof. The canonical +authority rows remain `UNPINNED`. Those are real blockers, not paperwork to +edit away. Nothing in this plan certifies program verification. + +== Operating rules for every contributor + +=== Start-of-task checklist + +. Confirm branch and worktree before editing: ++ +[source,sh] +---- +git status --short +git branch --show-current +---- ++ +. Read this plan, the architecture spec, and the relevant authority's upstream + source before changing a theorem boundary or IR meaning. +. Run `bash tests/bactrian/doctor_test.sh` and + `scripts/bactrian/doctor.sh`; record the latter's blockers. Doctor is a + readiness inventory only. +. Select one work-package ID below. Check its prerequisites and avoid parallel + changes to shared IR, status, lock, or runtime interfaces without an agreed + schema. +. Write the failing test or fixture first wherever practical. Work against the + testable contract, not a presumed tool API. + +=== Non-negotiable evidence rules + +* Never replace `UNPINNED` with an invented revision, URL, theorem name, or + digest. Record provenance and independently check the artifact bytes. +* Never implement canonical Agda results a second time in OCaml, Idris2, or + TLA+. Build an adapter/refinement check to the actual upstream theorem. +* Never treat parser acceptance, tests, fuzzing, solver `unsat`, Apalache + bounded search, benchmark measurements, or an INCOMPLETE Warrant as a + COMPLETE proof. +* A soundness-critical uncertainty is a blocker. Stop and ask the maintainer + rather than introducing an undocumented assumption or changing the scope. +* Fail closed for unknown compiler AST nodes, PPX expansion, FFI symbols, + assumptions, manifest versions, and receipt states. +* An actor send is not a remote commit. Commitment knowledge requires a + correlated causal reply following modeled commit; loss of that reply leaves + the sender uncertain. +* Do not claim a `<= 1 ms` scheduler bound unless the MaxPlus theorem, runtime + cost unit, target assumptions, wrapper overhead, and admission/fallback path + are all checked. +* Keep generated solver output, caches, binaries, and downloaded proof bundles + out of Git unless a specific reproducible-artifact policy requires them. + +=== Work-package completion and handoff + +A package is DONE only when all of the following are in the PR or its linked +review evidence: + +. Acceptance tests pass locally and the exact commands are recorded. +. Negative and mutation fixtures show that the relevant gate rejects the + intended unsound case. +. Inputs, tool versions, assumptions, and output hashes are reproducible and + source-mapped. +. Documentation states limitations and any remaining bounded/incomplete + result accurately. +. The next package's interface is documented and versioned. + +Every handoff/PR description should include: + +[source,text] +---- +Work package(s): WP-xx +Scope / assumptions: +Changed files: +Commands run + results: +Proof status: preflight | tested | bounded-only | incomplete | complete | failed +Evidence hashes / receipt (if any): +Known blockers and next package: +---- + +“Complete” in this handoff format is a proof status and must include the validated +ECHIDNA COMPLETE Receipt and matching source/toolchain/authority hashes. A +merged implementation without that receipt remains unproved. + +== Dependency graph and release gates + +[source,text] +---- +WP-00 Target + trust inventory + -> WP-01 pinned toolchain + canonical artifacts + ECHIDNA contract + -> WP-02 Dune skeleton + typed status machine + -> WP-03 stable Core Spec IR + -> WP-04 AST gate + frontend + source maps + -> WP-05 contracts + termination + Why3 + Dedukti + first ECHIDNA receipt + -> WP-06 MPR capabilities + TINI/R5 + -> WP-07 actor protocol + occupancy + K-CUT + Apalache + -> WP-08 ABI manifest + Idris2/ZigProve + runtime adapter + -> WP-09 cross-layer mutation + final receipt/release profile +---- + +WP-06 through WP-08 may proceed in parallel only after WP-03 IR, WP-05's +minimal checked receipt path, and the Dune status contracts are stable. Changes +that alter those shared contracts require a version bump, migration note, and +all downstream adapter tests rerun. + +[cols="1,2,2,2",options="header"] +|=== +| Gate | Required result | Status name allowed | Release implication + +| G0 — checkout health +| Doctor and repository tests report real blockers; no false-ready claim. +| `preflight` / `blocked` +| No verification claim. + +| G1 — source accepted +| Pinned parser and PPX firewall accept a supported AST; source map and AST +hash are captured. +| `ast-accepted` +| No theorem proved. + +| G2 — obligation checked +| Every generated VC has a checked proof object or explicit counterexample; +solver status alone is insufficient. +| `proved-locally`, `failed`, `unknown` +| Not a release receipt. + +| G3 — distributed model explored +| Bounds, assumptions, and counterexamples are captured; K-CUT bridge/refinement +is checked before any unbounded promotion. +| `bounded-only` or `proved` +| Bounded-only blocks any requirement asking for an unbounded theorem. + +| G4 — boundary closed +| Exact ABI/source hashes, Idris2 QTT, ZigProve correspondence, runtime +adapter, ownership and cost obligations are checked. +| `boundary-checked` or `incomplete` +| No cross-boundary release claim until ECHIDNA closure. + +| G5 — receipt complete +| Strict Dedukti, Coq and Lean batch checks succeed; ECHIDNA validates receipt +identity, assumptions, and every input hash. +| `complete` +| Eligible for release only if all required profiles are complete. +|=== + +== Work packages + +Each package below is intended to become one small, reviewable PR or a bounded +set of coordinated PRs. Do not start a downstream package by fabricating its +upstream prerequisites. + +=== WP-00 — Select target, owners, and assurance boundary + +*Priority:* P0; blocking for runtime- and choreography-specific proofs. + +*Decisions / inputs required:* + +* Choose one target for MVP: (A) native OCaml process communicating with a + named BEAM implementation, or (B) a specific OCaml-on-BEAM runtime. Record + exact OCaml version, runtime/BEAM distribution, operating system, target + triple, scheduler semantics, GC model, and transport guarantees. +* Name one maintainer for semantic/IR changes, one for proof-chain integration, + and one for ABI/runtime integration (roles may be held by one person). +* Confirm where the canonical Agda repositories live and who can attest their + authoritative branch/revision. The names in this repository are not enough + to locate or authenticate a theorem. +* Select ECHIDNA's real executable/API, schema, authentication model, and + receipt verification path. Do not assume a command name from the design. + +*Outputs:* `config/bactrian/target.toml`; owner-approved assurance-boundary +record; source-location map for each dependency; signed or otherwise +independently verified provenance note. + +*Acceptance:* a fresh contributor can state what exact runtime is in scope and +what behavior is assumed. If no target or canonical map is available, keep WP-00 +blocked and work only on target-independent scaffolding. + +*Stop conditions:* request is “support all BEAM runtimes”; canonical theorem +source conflicts with its described result; no owner can approve target/runtime +assumptions. + +=== WP-01 — Pin tools, authorities, and integration formats + +*Priority:* P0; can begin in parallel with target-independent WP-02 design, +but must close before a proof result is trusted. + +*Tasks:* + +. Extend `.machine_readable/bactrian/authorities.lock` to record, for every + authority, canonical repository identity, exact source revision, theorem or + module identity, artifact path, artifact SHA-256, checker name/version, and + license/provenance. Preserve TSV simplicity or use a reviewed schema; do not + parse partially populated rows as valid. +. Pin tool versions and checksums for the OCaml compiler, Dune, Why3 and SMT + backend, Apalache, Idris2, Zig/ZigProve, Dedukti, Coq, Lean, and the selected + runtime headers. Use repository provisioning canon rather than an unpinned + install script. +. Define ECHIDNA request/response schemas for obligation bundles, + `INCOMPLETE Warrant`, and `COMPLETE Receipt`. Pin all checker identities and + signature/issuer validation rules. +. Add lock tests for absent, duplicate, malformed, unknown, changed-revision, + changed-digest, and wrong-checker rows. Make a one-byte mutation to a test + artifact fail. + +*Commands/evidence:* after Dune exists, `dune build @preflight`; before then +`bash tests/bactrian/doctor_test.sh`. Record tool versions and artifact hashes +in a reproducible build report. + +*Acceptance:* no row remains `UNPINNED`; source provenance and exact bytes are +independently validated; missing tools and stale dependencies produce failure; +invalid ECHIDNA evidence is rejected. + +*Never:* replace `UNPINNED` with zero hashes, use a branch name as a pin, or +state that a source revision alone proves a generated artifact's identity. + +=== WP-02 — Dune project and command/status shell + +*Priority:* P1; prerequisite for all executable OCaml components. + +*Files:* `dune-project`; package/opam manifest; `src/dune`; `src/driver/dune`; +`src/driver/main.ml`; `src/driver/status.ml`; `tests/dune`. + +*Tasks:* + +* Pin one OCaml and Dune version; make warnings fatal for Bactrian's own code. +* Implement CLI commands `doctor`, `check-ast`, and `verify`, with distinct + stable exit codes and structured text output. Keep public CLI output plain + and deterministic. +* Model statuses as a closed variant. Transitions into `Complete` require a + cryptographically/semantically validated receipt object; no string parsing + or “all subprocesses returned zero” shortcut can create it. +* Add `@preflight` for readiness and `@verify` as a fail-closed alias. At this + stage `@verify` must fail with a clear “verification pipeline not wired” + diagnostic, not pass due to empty target sets. +* Add tests proving empty source sets, missing adapters, subprocess timeouts, + unknown status values, and stale outputs fail. + +*Acceptance:* `dune build @preflight` can succeed only for checked prerequisites; +`dune build @verify` exits nonzero until a real complete proof pipeline exists. + +=== WP-03 — Stable Core Spec IR and provenance + +*Priority:* P1; should be reviewed before independent frontend/backend work. + +*Files:* `src/core/ir.ml`, `src/core/serialize.ml`, `src/core/hash.ml`, +`src/core/source_map.ml`, `tests/core/`. + +*Tasks:* + +* Encode declarations, ADTs, pure expressions, contracts, capabilities, + secrets, protocol transitions, foreign bindings, and obligations separately. +* Specify integer and equality semantics, typing rules, binder identity, source + spans, error reporting, and IR-version compatibility. +* Canonicalize serialization and hash the full dependency/provenance closure. + Include parser/PPX versions, authority digests, assumptions, target/runtime, + engine versions, flags, and model bounds in cache identity. +* Reject unknown IR tags, missing source maps, duplicate identifiers, malformed + hashes, and unsupported schema versions. + +*Acceptance:* golden IR fixtures are byte-deterministic; changing any semantic +input changes the identity; no backend can silently drop an obligation. + +=== WP-04 — Compiler-libs PPX firewall and typed frontend + +*Priority:* P1; source trust boundary; do not substitute regex scanning. + +*Files:* `src/ppx/`, `src/frontend/`, `fixtures/accepted/`, +`fixtures/rejected/`, `tests/frontend/`. + +*Tasks:* + +. Parse/typecheck with pinned compiler-libs; record compiler version, source + hash, interface hashes, and PPX expansion order. +. Capture generated-node provenance; require deterministic PPX output; reject + unknown PPX transformations and unexpanded extensions. +. Walk the final typed/expanded AST with an explicit node allowlist. Resolve + aliases, opens, local names, and transitive call graph. +. Reject `Obj.magic`, representation operations, `Unsafe_*`, `Sys.command`, + process/file/system/port authority, mutation, exceptions, dynamic loading, + unknown calls, and all unverified `external`/FFI declarations. +. Initially accept only ADTs, exhaustive match, immutable records/tuples/lists, + local pure functions, constants, and an explicit pure primitive allowlist. + Unknown AST forms fail closed after every compiler upgrade. + +*Required negative tests:* direct and aliased forbidden API; hidden call behind a +module alias; source PPX that expands to forbidden code; nondeterministic PPX; +raw FFI; unknown expression/structure node; unsupported effects. Also include +positive controls so the firewall does not merely reject all programs. + +*Acceptance:* final expanded typed AST is the sole admission source; each +rejection reports source span and expansion origin; no AST node is ignored. + +=== WP-05 — Contracts, totality, Why3 VCs, and first theorem + +*Priority:* P1; first end-to-end proof slice. + +*Tasks:* + +* Define the actual grammar/payload rules for `[%cap]`, `[@pre]`, `[@post]`, + `[@secret]`, and choreography extensions. Clarify OCaml parser limitations + and version the syntax. +* Translate only the accepted pure subset to the IR. Contracts are logic, not + executed OCaml closures. Reject effectful/unknown contract terms. +* Generate VCs for type preservation at the boundary, preconditions, + postconditions, exhaustive matching, arithmetic, and termination. +* Start with a monomorphic ADT and one non-recursive function. Define integer + model explicitly. Add structural termination only after the first proof is + checked end-to-end. +* Connect Why3 and the SMT solver to proof reconstruction or a separately + checked certificate path. A solver's `unsat` result alone is not a Dedukti + witness. +* Check strict `.dk` witness and source mapping; send one tiny obligation to + ECHIDNA before widening the language. + +*Mutation gate:* precondition must be satisfiable; a mutated postcondition must +fail; deleting an obligation must fail bundle completeness; unsupported +arithmetic must be rejected. + +*Acceptance:* at least one fixture reaches a validated ECHIDNA COMPLETE Receipt +whose hashes bind the source, AST, IR, VC, toolchain, and theorem manifest. +If the proof bridge does not yet exist, report `incomplete`, not `complete`. + +=== WP-06 — MPR capability footprints and TINI/R5 + +*Priority:* P2; depends on stable IR and authority pins. + +*Tasks:* + +* Elaborate `[%cap ...]` to MPR Sigma using the pinned Agda theorem/API. +* Deny ambient `File`, `System`, `Port`, and `Sys.command` authority by default. +* Attach `[@secret]` labels to the exact inputs, state, and observations. +* Build TINI obligations and invoke R5 composition at whole-program/component + boundaries; reject an `fs.read` + `net.send` corridor. +* Carry `ProofTransport` certificates with unchanged theorem assumptions and + hashes; transport must not strengthen conclusions. + +*Acceptance:* positive pure case closes; forbidden capability fails; composition +counterexample fails; artifact drift invalidates the receipt. + +=== WP-07 — Actor protocol frontend, occupancy, K-CUT, Apalache + +*Priority:* P2; depends on IR protocol schema, target selection, and canonical +K-CUT/occupancy pins. + +*Initial fixture:* two roles, one request, one correlated reply, one entity +state, mailbox HWM 2 or smaller, one commit transition, explicit crash points +before and after commit, and possible loss/delay/reordering. + +*Tasks:* + +. Parse choreography Face to an explicit transition system; no runtime actor + behavior inferred from source names. +. Model selective receive, unmatched queued messages, message-in-flight state, + queue growth/HWM, overflow policy, link and monitor semantics, timeouts, and + crash/restart transitions. +. Import `occupancy-types`; state arrival/service assumptions and prove or + model-check the queue bound. +. Enforce the causal reply rule in the IR checker: `send`, enqueue success, + link, monitor, timeout, or sender-local state cannot establish receiver + commitment. +. Import K-CUT-LOSS and K-CUT-WARRANT interfaces. Retain loss residues and + Kripke assumptions in the obligation record. +. Use Apalache with declared role/state/message/step/queue bounds. Label outputs + `bounded-only` unless a refinement/inductive argument upgrades the result. + +*Required killer trace:* receiver commits, reply is lost, sender remains +uncertain. Removing causal reply must fail the elaboration rule even if BMC +finds no counterexample. Include a stale reply/request ID mutant and queue +overflow trace. + +*Acceptance:* sound bounded evidence plus checked refinement to imported +canonical theorems where applicable; no unbounded claim from BMC alone. + +=== WP-08 — Idris2/QTT + ZigProve + OCaml GC ABI + +*Priority:* P2; depends on target runtime and runtime header pins. + +*Initial fixture:* one deterministic hash/drift primitive on a bounded input; +no callbacks; opaque handle or copied/unboxed input; one generated binding. + +*Tasks:* + +* Define manifest binding OCaml external, C symbol, Idris2 total QTT type, + layout/ownership/range constraints, Zig source/build hashes, proof digest, + runtime version, and cost theorem. +* Generate stub/header rather than accept handwritten FFI. Verify resolved + linker symbol and exact build hash. +* Use actual target runtime root/exception/custom-block APIs. Do not assume + `caml_reserve_custom` exists or is portable. Prove linear acquire/release, + GC root lifetime, failure paths, finalizer, exception/unwind behavior, and + absence of raw OCaml heap mutation. +* Import ZigProve correspondence for the exact body and MaxPlus cost, not just + memory safety of a nearby source file. +* Bound input size and wrapper overhead. Establish sound cost-unit conversion + to the 1 ms scheduler slice. If unavailable or over budget, force worker or + nonblocking path; do not rely on average timings. + +*Required mutations:* change symbol, C width/alignment, ownership, source hash, +Zig build flag, maximum input, cost theorem, and runtime version. Each must +invalidate the gate. + +*Acceptance:* one boundary fixture and all its exceptional paths are proven for +one named runtime/target. No cross-runtime generalization. + +=== WP-09 — ECHIDNA closure, mutations, cache, and release profile + +*Priority:* P3; final integration gate. + +*Tasks:* + +* Validate strict Dedukti witnesses, then batch Coq + Lean checks, then validate + ECHIDNA's COMPLETE Receipt; distinguish it from local INCOMPLETE Warrant. +* Check signer/issuer, checker versions, assumptions, obligation count, and + every content hash. Any omitted proof obligation fails closed. +* Integrate `mutation.rs` for vacuity, postcondition sensitivity, removed causal + reply, and ABI/hash corruption. Record surviving mutations and require + maintainer disposition. +* Add adversarial cache tests for source changes, dependency hash changes, + tool upgrades, assumptions, bounds, and runtime target changes. Enable cache + only after misses/hits are demonstrably sound. +* Wire `dune build @verify` in CI; release profile requires COMPLETE for all + mandatory obligations. Preserve bounded and incomplete developer profiles + as non-release. + +*Acceptance:* clean, repeatable build reaches COMPLETE on curated fixtures; +all required mutations are killed; one missing/stale/failed checker makes +`@verify` fail. + +== Cross-package test matrix + +|=== +| Area | Positive control | Negative control | Gate evidence + +| Tool/status +| Installed/pinned tools identified +| Missing checker and invalid receipt +| Preflight + status transition tests + +| PPX/frontend +| Supported pure ADT +| Alias-hidden `Sys.command`, `Obj.magic`, unknown PPX +| Typed AST fixture result and source span + +| Contracts/Why3 +| Correct total function and contract +| False postcondition, unsatisfiable precondition, nondecreasing recursion +| Checked VC/proof object and mutation result + +| Capabilities/TINI +| Pure public computation +| Ambient capability and composed exfiltration corridor +| Imported Sigma/TINI/R5 obligations + +| Actor protocol +| Commit + correlated causal reply +| Lost reply, stale reply, claim after send only +| Apalache trace plus K-CUT/refinement evidence + +| Occupancy +| Bounded arrivals and stated overflow action +| Unbounded sender claim or capacity overflow +| HWM invariant and assumptions + +| ABI/runtime +| Correct generated binding with valid roots/handles +| ABI mismatch, use-after-release, GC/exception failure mutant +| Idris2/ZigProve/runtime adapter evidence + +| Receipt/release +| All obligations and hashes agree +| Missing witness, stale digest, missing Coq/Lean checker +| Valid COMPLETE Receipt and cache mutation suite +|=== + +== Repository conventions and integration points + +* Keep the versioned verifier source under `src/`; do not expand the current + template ABI examples into a purported OCaml runtime proof. +* Keep canonical dependency pins under `.machine_readable/bactrian/`; tool + installation remains in the estate's pinned provisioning mechanism. +* Keep accepted/rejected examples and mutation seeds under `fixtures/` and + `tests/bactrian/`; every new supported syntax feature needs a positive case, + a negative soundness case, and source-map assertions. +* Use Dune build artifacts under `_build/`; never commit solver caches or + generated binary proof output by default. +* Update `docs/status/PROOF-STATUS.adoc`, `PROOF-NEEDS.adoc`, and + `ROADMAP.adoc` only when the corresponding checker/evidence was actually run. + A task being implemented is not proof progress. +* The future `@verify` alias is the release gate; `doctor.sh` is only the + bootstrap preflight and must never be aliased to a green verification target. + +== Active checklist + +This checklist starts from observed repository state and is intentionally +conservative. Mark a task complete only with a linked PR/commit and the +acceptance evidence above. + +* [x] Architecture specification and layered soundness contract documented. +* [x] Implementation sequence and module-level roadmap documented. +* [x] Preflight toolchain/authority checker implemented, with explicit + non-proof status. +* [x] Preflight tests cover blocked state, bad arguments, and duplicate lock + rows. +* [ ] WP-00 target/runtime, canonical-source locations, and ECHIDNA interface + approved. +* [ ] WP-01 toolchain and canonical artifacts independently pinned. +* [ ] WP-02 Dune status machine and fail-closed aliases implemented. +* [ ] WP-03 stable IR and provenance tests implemented. +* [ ] WP-04 post-expansion typed AST firewall implemented. +* [ ] WP-05 first sequential theorem reaches ECHIDNA COMPLETE. +* [ ] WP-06 capability and TINI/R5 integration checked. +* [ ] WP-07 protocol/K-CUT/Apalache vertical slice checked. +* [ ] WP-08 one OCaml/Idris2/Zig runtime boundary proved. +* [ ] WP-09 mutation/cache/release gate is complete. + +== First five actions + +. **Maintainer:** decide WP-00 target and name the canonical source locations + and ECHIDNA owner/interface. This is the only step that should not be guessed + by a coding agent. +. **Build/tooling contributor:** install and pin the OCaml compiler and Dune in + the sanctioned provisioning setup; add a minimal project and prove that an + empty `@verify` alias fails, while `@preflight` reports tools correctly. +. **Formal-methods contributor:** inspect and record actual exported theorem + signatures for the first Layer A authority path and define an artifact + verification test. Do not reprove Agda results. +. **OCaml contributor:** implement one compiler-libs AST adapter and a tiny + positive/negative firewall fixture pair under the chosen compiler version. +. **Integration contributor:** define ECHIDNA's actual request/receipt schema + and validate an invalid witness rejection before investing in a wider VC + translator. + +After these five actions, update the active checklist from observed evidence, +not from elapsed effort. Continue in dependency order; stop at any missing +canonical artifact or unresolved soundness assumption. diff --git a/scripts/bactrian/doctor.sh b/scripts/bactrian/doctor.sh new file mode 100755 index 0000000..fab9a00 --- /dev/null +++ b/scripts/bactrian/doctor.sh @@ -0,0 +1,117 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Bactrian dependency/readiness preflight. This command never verifies OCaml +# programs and never emits a proof receipt. +set -u + +usage() { + cat <<'EOF' +Usage: scripts/bactrian/doctor.sh [--help] + +Report whether this checkout has the tools and pinned authorities needed to +start the Bactrian MVP. Exit 0 means preflight-ready only; exit 2 means blocked. +This command is not a verifier and cannot establish a proof. +EOF +} + +case "${1-}" in + --help|-h) usage; exit 0 ;; + "") ;; + *) printf 'error: unknown argument: %s\n' "$1" >&2; usage >&2; exit 64 ;; +esac + +ROOT=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd) +blockers=0 + +ok() { printf ' [ready] %s\n' "$1"; } +missing() { printf ' [blocked] %s\n' "$1"; blockers=$((blockers + 1)); } + +printf 'Bactrian MVP preflight (not a proof check)\n' +printf 'Repository: %s\n\n' "$ROOT" +printf 'Required tools:\n' +for tool in dune ocamlc why3 apalache idris2 zig dkcheck coqc lean; do + if command -v "$tool" >/dev/null 2>&1; then + ok "$tool ($(command -v "$tool"))" + else + missing "$tool not found on PATH" + fi +done + +printf '\nECHIDNA integration:\n' +if [[ -n "${BACTRIAN_ECHIDNA_CMD-}" ]]; then + if [[ "$BACTRIAN_ECHIDNA_CMD" == */* ]]; then + if [[ -x "$BACTRIAN_ECHIDNA_CMD" ]]; then + ok "configured ECHIDNA command ($BACTRIAN_ECHIDNA_CMD)" + else + missing "BACTRIAN_ECHIDNA_CMD is not executable: $BACTRIAN_ECHIDNA_CMD" + fi + elif command -v "$BACTRIAN_ECHIDNA_CMD" >/dev/null 2>&1; then + ok "configured ECHIDNA command ($(command -v "$BACTRIAN_ECHIDNA_CMD"))" + else + missing "configured ECHIDNA command not found: $BACTRIAN_ECHIDNA_CMD" + fi +else + missing 'BACTRIAN_ECHIDNA_CMD is unset (ECHIDNA CLI/API adapter is not selected)' +fi + +printf '\nCanonical authority lock syntax (this does not verify artifacts):\n' +lock="$ROOT/.machine_readable/bactrian/authorities.lock" +if [[ ! -f "$lock" ]]; then + missing "authority lock absent: $lock" +else + declare -A expected=() + for name in MPR choreographic-types secret-types echo-types epistemic-types occupancy-types tropical-types ECHIDNA; do + expected["$name"]=0 + done + malformed=0 + while IFS=$'\t' read -r name revision digest extra || [[ -n "${name-}${revision-}${digest-}${extra-}" ]]; do + [[ -z "${name-}" || "$name" == \#* ]] && continue + if [[ -z "${revision-}" || -z "${digest-}" || -n "${extra-}" || ! ${expected["${name-}"]+present} ]]; then + printf ' [blocked] malformed or unexpected lock row: %s\n' "${name-}" + malformed=1 + continue + fi + if [[ "${expected[$name]}" -ne 0 ]]; then + printf ' [blocked] duplicate authority row: %s\n' "$name" + malformed=1 + continue + fi + expected["$name"]=1 + if [[ "$revision" =~ ^[0-9a-f]{40}([0-9a-f]{24})?$ && "$digest" =~ ^[0-9a-f]{64}$ ]]; then + ok "$name pin fields populated (format only; artifact provenance is not verified)" + elif [[ "$revision" == UNPINNED && "$digest" == UNPINNED ]]; then + missing "$name has not been pinned to a canonical source revision and digest" + else + printf ' [blocked] invalid pin for %s (expected 40/64-hex revision and 64-hex digest, or UNPINNED/UNPINNED)\n' "$name" + malformed=1 + fi + done < "$lock" + for name in "${!expected[@]}"; do + if [[ "${expected[$name]}" -eq 0 ]]; then + printf ' [blocked] missing authority row: %s\n' "$name" + malformed=1 + fi + done + if [[ "$malformed" -ne 0 ]]; then + blockers=$((blockers + 1)) + fi +fi + +printf '\nImplementation scaffold:\n' +for path in dune-project src/ppx/dune src/driver/dune; do + if [[ -f "$ROOT/$path" ]]; then + ok "$path present" + else + missing "$path absent (compiler/verifier integration not implemented)" + fi +done + +printf '\n' +if [[ "$blockers" -eq 0 ]]; then + printf 'Preflight READY: prerequisites are present. This is NOT verification and grants no proof status.\n' + exit 0 +fi +printf 'Preflight BLOCKED: %d readiness item(s) unresolved. No verification or proof status was produced.\n' "$blockers" +exit 2 diff --git a/tests/bactrian/doctor_test.sh b/tests/bactrian/doctor_test.sh new file mode 100755 index 0000000..974ed88 --- /dev/null +++ b/tests/bactrian/doctor_test.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +set -euo pipefail + +ROOT=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd) +doctor="$ROOT/scripts/bactrian/doctor.sh" + +help_output=$(bash "$doctor" --help) +grep -q 'cannot establish a proof' <<<"$help_output" + +set +e +output=$(bash "$doctor" 2>&1) +status=$? +set -e +if [[ "$status" -ne 2 ]]; then + printf 'expected blocked preflight exit 2, got %s\n%s\n' "$status" "$output" >&2 + exit 1 +fi +grep -q 'Bactrian MVP preflight (not a proof check)' <<<"$output" +grep -q 'Canonical authority lock syntax' <<<"$output" +grep -q 'No verification or proof status was produced' <<<"$output" + +set +e +bash "$doctor" --definitely-invalid >/dev/null 2>&1 +status=$? +set -e +if [[ "$status" -ne 64 ]]; then + printf 'expected usage exit 64 for invalid argument, got %s\n' "$status" >&2 + exit 1 +fi + +# Exercise malformed authority-lock handling without changing the checkout. +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT +mkdir -p "$tmp/scripts/bactrian" "$tmp/.machine_readable/bactrian" +cp "$doctor" "$tmp/scripts/bactrian/doctor.sh" +cp "$ROOT/.machine_readable/bactrian/authorities.lock" \ + "$tmp/.machine_readable/bactrian/authorities.lock" +printf 'MPR\tUNPINNED\tUNPINNED\n' >>"$tmp/.machine_readable/bactrian/authorities.lock" +set +e +output=$(bash "$tmp/scripts/bactrian/doctor.sh" 2>&1) +status=$? +set -e +if [[ "$status" -ne 2 ]] || ! grep -q 'duplicate authority row: MPR' <<<"$output"; then + printf 'malformed duplicate authority row was not rejected (exit %s):\n%s\n' \ + "$status" "$output" >&2 + exit 1 +fi + +printf 'PASS: Bactrian doctor reports blockers honestly and never presents preflight as proof.\n' From 755a15cf39a1f2e35dab545fc4c92f09502d4222 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Thu, 22 Oct 2026 16:30:06 +0000 Subject: [PATCH 2/4] docs(doctor): document usage and preflight status helpers --- scripts/bactrian/doctor.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/bactrian/doctor.sh b/scripts/bactrian/doctor.sh index fab9a00..325c67d 100755 --- a/scripts/bactrian/doctor.sh +++ b/scripts/bactrian/doctor.sh @@ -6,6 +6,7 @@ # programs and never emits a proof receipt. set -u +# Write command usage and preflight exit-status help to stdout. usage() { cat <<'EOF' Usage: scripts/bactrian/doctor.sh [--help] @@ -25,7 +26,9 @@ esac ROOT=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd) blockers=0 +# Print $1 as a ready item to stdout. ok() { printf ' [ready] %s\n' "$1"; } +# Print $1 as a blocked item to stdout and increment the global blockers count. missing() { printf ' [blocked] %s\n' "$1"; blockers=$((blockers + 1)); } printf 'Bactrian MVP preflight (not a proof check)\n' From 6f1cbc080793dceeaa2f3645d9e9e4c4ed81e829 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Thu, 22 Oct 2026 16:37:54 +0000 Subject: [PATCH 3/4] fix(bactrian): tighten preflight and spec examples --- .../BACTRIAN-VERIFICATION-SPEC.adoc | 13 +- scripts/bactrian/doctor.sh | 31 ++-- tests/bactrian/doctor_test.sh | 137 +++++++++++++----- 3 files changed, 132 insertions(+), 49 deletions(-) diff --git a/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc b/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc index c294bc7..1a06883 100644 --- a/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc +++ b/docs/architecture/BACTRIAN-VERIFICATION-SPEC.adoc @@ -421,13 +421,14 @@ external hash_and_drift : bytes -> int64 -> (int64 * int64) = "caml_bactrian_hash_and_drift" let[@pre old.version >= 0L] - [@post fun next -> next.version = old.version + 1L] - [@post fun next -> next.id = old.id] + [@post function Ok next -> next.version = Int64.add old.version 1L + | Error _ -> true] + [@post function Ok next -> next.id = old.id | Error _ -> true] next_entity old payload = [%cap pure] let (digest, drift) = hash_and_drift payload old.digest in if drift < 0L then Error `Invalid_drift - else Ok { old with version = old.version + 1L; digest } + else Ok { old with version = Int64.add old.version 1L; digest } [%bactrian.choreography roles (client, entity_store); @@ -437,8 +438,10 @@ let[@pre old.version >= 0L] client -> entity_store : Apply(request_id, expected, payload); entity_store: receive Apply(id, expected, payload); entity_store: if expected = state.version then - commit(next_entity(state, payload)); - send client : Committed(id, state.version, state.digest) + match next_entity(state, payload) with + | Error _ -> send client : Rejected(id, state.version) + | Ok next -> commit(next); + send client : Committed(id, next.version, next.digest) else send client : Rejected(id, state.version); client: only Committed(id, v, d) causally following Apply(id, ...) establishes acknowledged_commit(id, v, d); diff --git a/scripts/bactrian/doctor.sh b/scripts/bactrian/doctor.sh index 325c67d..b2d7fd5 100755 --- a/scripts/bactrian/doctor.sh +++ b/scripts/bactrian/doctor.sh @@ -69,10 +69,20 @@ else expected["$name"]=0 done malformed=0 - while IFS=$'\t' read -r name revision digest extra || [[ -n "${name-}${revision-}${digest-}${extra-}" ]]; do - [[ -z "${name-}" || "$name" == \#* ]] && continue - if [[ -z "${revision-}" || -z "${digest-}" || -n "${extra-}" || ! ${expected["${name-}"]+present} ]]; then - printf ' [blocked] malformed or unexpected lock row: %s\n' "${name-}" + # Match the raw row: tab is IFS whitespace, so read would collapse empty columns. + row_pattern=$'^([^\t]+)\t([^\t]+)\t([^\t]+)$' + while IFS= read -r row || [[ -n "$row" ]]; do + [[ -z "$row" || "$row" == \#* ]] && continue + if [[ ! "$row" =~ $row_pattern ]]; then + printf ' [blocked] malformed lock row (expected three nonempty TSV fields)\n' + malformed=1 + continue + fi + name=${BASH_REMATCH[1]} + revision=${BASH_REMATCH[2]} + digest=${BASH_REMATCH[3]} + if [[ ! ${expected["$name"]+present} ]]; then + printf ' [blocked] unexpected lock authority: %s\n' "$name" malformed=1 continue fi @@ -102,12 +112,15 @@ else fi fi -printf '\nImplementation scaffold:\n' -for path in dune-project src/ppx/dune src/driver/dune; do - if [[ -f "$ROOT/$path" ]]; then - ok "$path present" +printf '\nImplementation prerequisites (nonempty files only):\n' +for path in dune-project src/ppx/dune src/driver/dune \ + src/core/ir.ml src/ppx/firewall.ml src/frontend/typed_ast.ml \ + src/why3/translate.ml src/actors/protocol.ml src/abi/manifest.ml \ + src/driver/status.ml; do + if [[ -f "$ROOT/$path" && -s "$ROOT/$path" ]]; then + ok "$path present and nonempty" else - missing "$path absent (compiler/verifier integration not implemented)" + missing "$path absent or empty (compiler/verifier integration not implemented)" fi done diff --git a/tests/bactrian/doctor_test.sh b/tests/bactrian/doctor_test.sh index 974ed88..77a62d1 100755 --- a/tests/bactrian/doctor_test.sh +++ b/tests/bactrian/doctor_test.sh @@ -5,47 +5,114 @@ set -euo pipefail ROOT=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd) doctor="$ROOT/scripts/bactrian/doctor.sh" +bash_cmd=$(command -v bash) help_output=$(bash "$doctor" --help) grep -q 'cannot establish a proof' <<<"$help_output" -set +e -output=$(bash "$doctor" 2>&1) -status=$? -set -e -if [[ "$status" -ne 2 ]]; then - printf 'expected blocked preflight exit 2, got %s\n%s\n' "$status" "$output" >&2 - exit 1 -fi +# Control tools, pins, and implementation files independently of checkout readiness. +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT +mkdir -p "$tmp/scripts/bactrian" "$tmp/.machine_readable/bactrian" "$tmp/bin" +cp "$doctor" "$tmp/scripts/bactrian/doctor.sh" +fixture_doctor="$tmp/scripts/bactrian/doctor.sh" +lock="$tmp/.machine_readable/bactrian/authorities.lock" +printf '#!/bin/sh\nexit 0\n' >"$tmp/bin/tool" +chmod +x "$tmp/bin/tool" +for tool in dune ocamlc why3 apalache idris2 zig dkcheck coqc lean echidna; do + ln -s tool "$tmp/bin/$tool" +done +ln -s "$(command -v dirname)" "$tmp/bin/dirname" + +# Synthetic format-valid pins, never used as provenance or proof evidence. +printf -v revision '%040d' 1 +printf -v digest '%064d' 2 +authorities=(MPR choreographic-types secret-types echo-types epistemic-types occupancy-types tropical-types ECHIDNA) +for name in "${authorities[@]}"; do + printf '%s\t%s\t%s\n' "$name" "$revision" "$digest" +done >"$lock" +cp "$lock" "$tmp/valid.lock" + +run_doctor() { + local expected_status=$1 status + shift + if output=$(PATH="$tmp/bin" BACTRIAN_ECHIDNA_CMD=echidna "$bash_cmd" "$fixture_doctor" "$@" 2>&1); then + status=0 + else + status=$? + fi + if [[ "$status" -ne "$expected_status" ]]; then + printf 'expected preflight exit %s, got %s\n%s\n' "$expected_status" "$status" "$output" >&2 + exit 1 + fi +} + +run_doctor 2 grep -q 'Bactrian MVP preflight (not a proof check)' <<<"$output" grep -q 'Canonical authority lock syntax' <<<"$output" grep -q 'No verification or proof status was produced' <<<"$output" -set +e -bash "$doctor" --definitely-invalid >/dev/null 2>&1 -status=$? -set -e -if [[ "$status" -ne 64 ]]; then - printf 'expected usage exit 64 for invalid argument, got %s\n' "$status" >&2 - exit 1 -fi +run_doctor 64 --definitely-invalid -# Exercise malformed authority-lock handling without changing the checkout. -tmp=$(mktemp -d) -trap 'rm -rf "$tmp"' EXIT -mkdir -p "$tmp/scripts/bactrian" "$tmp/.machine_readable/bactrian" -cp "$doctor" "$tmp/scripts/bactrian/doctor.sh" -cp "$ROOT/.machine_readable/bactrian/authorities.lock" \ - "$tmp/.machine_readable/bactrian/authorities.lock" -printf 'MPR\tUNPINNED\tUNPINNED\n' >>"$tmp/.machine_readable/bactrian/authorities.lock" -set +e -output=$(bash "$tmp/scripts/bactrian/doctor.sh" 2>&1) -status=$? -set -e -if [[ "$status" -ne 2 ]] || ! grep -q 'duplicate authority row: MPR' <<<"$output"; then - printf 'malformed duplicate authority row was not rejected (exit %s):\n%s\n' \ - "$status" "$output" >&2 - exit 1 -fi - -printf 'PASS: Bactrian doctor reports blockers honestly and never presents preflight as proof.\n' +# Dune scaffolding alone must remain blocked even with all tools and pins present. +mkdir -p "$tmp/src/ppx" "$tmp/src/driver" +printf '(lang dune 3.0)\n' >"$tmp/dune-project" +printf '(library (name ppx))\n' >"$tmp/src/ppx/dune" +printf '(library (name driver))\n' >"$tmp/src/driver/dune" +run_doctor 2 +grep -q 'src/ppx/firewall.ml absent or empty' <<<"$output" + +modules=(src/core/ir.ml src/ppx/firewall.ml src/frontend/typed_ast.ml + src/why3/translate.ml src/actors/protocol.ml src/abi/manifest.ml src/driver/status.ml) +for path in "${modules[@]}"; do + mkdir -p "$tmp/$(dirname "$path")" + printf 'let available = true\n' >"$tmp/$path" +done +run_doctor 0 +grep -q 'Preflight READY:.*NOT verification and grants no proof status' <<<"$output" + +# Each named module is required; an empty module must also block readiness. +for path in "${modules[@]}"; do + mv "$tmp/$path" "$tmp/module.ml" + run_doctor 2 + grep -Fq "$path absent or empty" <<<"$output" + mv "$tmp/module.ml" "$tmp/$path" +done +: >"$tmp/src/driver/status.ml" +run_doctor 2 +grep -q 'src/driver/status.ml absent or empty' <<<"$output" +printf 'let available = true\n' >"$tmp/src/driver/status.ml" + +# Malformed MPR rows must fail shape validation before any pin-format checks. +for row in \ + "MPR" \ + $'MPR\t'"$revision" \ + $'\t'"$revision"$'\t'"$digest" \ + $'MPR\t\t'"$digest" \ + $'MPR\t'"$revision"$'\t' \ + $'MPR\t\t'"$revision"$'\t'"$digest" \ + $'MPR\t'"$revision"$'\t\t'"$digest" \ + $'MPR\t'"$revision"$'\t'"$digest"$'\t' \ + $'MPR\t'"$revision"$'\t'"$digest"$'\textra'; do + grep -v '^MPR' "$tmp/valid.lock" >"$lock" + printf '%s' "$row" >>"$lock" # Exercise the final row without a newline too. + run_doctor 2 + grep -q 'malformed lock row (expected three nonempty TSV fields)' <<<"$output" + if grep -q 'MPR pin fields populated' <<<"$output"; then + printf 'malformed MPR row reached pin-format checks:\n%s\n' "$output" >&2 + exit 1 + fi +done + +cp "$tmp/valid.lock" "$lock" +printf 'MPR\tUNPINNED\tUNPINNED\n' >>"$lock" +run_doctor 2 +grep -q 'duplicate authority row: MPR' <<<"$output" + +# Comments, blank lines, and a valid final row without a newline are permitted. +printf '# fixture lock\n\n' >"$lock" +grep -v '^MPR' "$tmp/valid.lock" >>"$lock" +printf 'MPR\t%s\t%s' "$revision" "$digest" >>"$lock" +run_doctor 0 + +printf 'PASS: Bactrian doctor checks controlled blocked/ready fixtures and rejects malformed locks.\n' From 70d18563eec47965708c338eabae898f9f3df9db Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 22 Oct 2026 16:49:58 +0000 Subject: [PATCH 4/4] docs: add CI baseline triage to Bactrian plan Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/status/BACTRIAN-ULTRAPLAN.adoc | 126 ++++++++++++++++++++++++---- 1 file changed, 110 insertions(+), 16 deletions(-) diff --git a/docs/status/BACTRIAN-ULTRAPLAN.adoc b/docs/status/BACTRIAN-ULTRAPLAN.adoc index aa3b52c..1821008 100644 --- a/docs/status/BACTRIAN-ULTRAPLAN.adoc +++ b/docs/status/BACTRIAN-ULTRAPLAN.adoc @@ -28,6 +28,54 @@ Apalache/ECHIDNA adapter, or target-specific runtime proof. The canonical authority rows remain `UNPINNED`. Those are real blockers, not paperwork to edit away. Nothing in this plan certifies program verification. +The repository also still contains the RSR template identity and many +unfilled project placeholders (`README.adoc` and the root deed are examples). +It must be decided whether this repository is intentionally serving as a +customized template or is to become the Bactrian product repository. Do not +mass-substitute template tokens, rename the deed, or remove template assets +until that boundary is confirmed by the maintainer. + +=== Baseline hazards found in the first PR validation (2026-10-22) + +The first hosted validation run exposed failures beyond the local preflight +suite. Treat them as open baseline work; merging or opening a PR does not turn a +failed check green. + +[cols="2,2,3",options="header"] +|=== +| Check | Observed failure | Next action / evidence + +| OpenSSF Compliance — no unfilled placeholder tokens +| `scripts/check-no-placeholders.sh .` reports 89 files with template tokens. +| Re-run on the base commit and this branch; confirm whether the repo is meant +to be instantiated. Preserve intentional archetype/template carriers and only +resolve product files after owner direction. The newly added Bactrian docs and +preflight files contain no `{{UPPER_SNAKE}}` tokens. + +| Canon lockstep +| `Compare this repo's declared pin` failed. +| Inspect the exact canonical pin source and compare base vs branch. Do not +replace a pin until the authoritative revision/artifact is verified. + +| RSR oracle — dogfood this repo +| `Compile the oracle` failed. +| Recover the job log, identify the failing compiler/input, and reproduce it on +the base commit before attributing it to Bactrian changes. + +| Estate audit +| `Required Files Gate` failed. +| Recover the detailed audit report and compare required files against the +repo's declared identity and intended template/product role. +|=== + +The available check-run metadata identifies the failing steps but the job-log +archive was unavailable to the workspace during this run. The recorded job +references are link:https://github.com/hyperpolymath/Bactrian/actions/runs/39815613568/job/119953305648[Canon lockstep], +link:https://github.com/hyperpolymath/Bactrian/actions/runs/39815613568/job/119953305493[RSR oracle], +link:https://github.com/hyperpolymath/Bactrian/actions/runs/39815613363/job/119953304259[estate audit], +and link:https://github.com/hyperpolymath/Bactrian/actions/runs/39815612574/job/119953301356[OpenSSF placeholder check]. +Run IDs are historical evidence, not a guarantee these checks are still failing. + == Operating rules for every contributor === Start-of-task checklist @@ -108,16 +156,17 @@ merged implementation without that receipt remains unproved. [source,text] ---- -WP-00 Target + trust inventory - -> WP-01 pinned toolchain + canonical artifacts + ECHIDNA contract - -> WP-02 Dune skeleton + typed status machine - -> WP-03 stable Core Spec IR - -> WP-04 AST gate + frontend + source maps - -> WP-05 contracts + termination + Why3 + Dedukti + first ECHIDNA receipt - -> WP-06 MPR capabilities + TINI/R5 - -> WP-07 actor protocol + occupancy + K-CUT + Apalache - -> WP-08 ABI manifest + Idris2/ZigProve + runtime adapter - -> WP-09 cross-layer mutation + final receipt/release profile +WP-00A Repository identity + CI baseline + -> WP-00 Target + trust inventory + -> WP-01 pinned toolchain + canonical artifacts + ECHIDNA contract + -> WP-02 Dune skeleton + typed status machine + -> WP-03 stable Core Spec IR + -> WP-04 AST gate + frontend + source maps + -> WP-05 contracts + termination + Why3 + Dedukti + first ECHIDNA receipt + -> WP-06 MPR capabilities + TINI/R5 + -> WP-07 actor protocol + occupancy + K-CUT + Apalache + -> WP-08 ABI manifest + Idris2/ZigProve + runtime adapter + -> WP-09 cross-layer mutation + final receipt/release profile ---- WP-06 through WP-08 may proceed in parallel only after WP-03 IR, WP-05's @@ -171,6 +220,45 @@ Each package below is intended to become one small, reviewable PR or a bounded set of coordinated PRs. Do not start a downstream package by fabricating its upstream prerequisites. +=== WP-00A — Reconcile repository identity and CI baseline + +*Priority:* P0; do this before product initialization, canonical pin edits, or +changes intended to make the failed hosted gates green. + +*Tasks:* + +. Ask the maintainer whether `hyperpolymath/Bactrian` is intentionally an + uninitialized RSR template, a Bactrian product repository, or a transition + repository with both roles. Record the decision and what files/assets must + remain as templates. +. Re-run the failing CI checks on the current base and compare their inputs + with the branch's changed files. Retrieve the job logs where available; the + previous workspace could read check metadata but could not fetch the log + archives. +. Triage Canon lockstep, RSR oracle compilation, estate-audit Required Files, + and OpenSSF placeholder failures independently. Distinguish a repository + baseline failure from a regression in changed files. +. For the 89 placeholder-bearing files, classify each as (a) intentional + template/archetype input, (b) shipped project file requiring initialization, + or (c) an invalid leftover. Apply only the correct canonical disposition; + do not blanket-replace tokens or weaken the checker. +. Preserve green controls: secret scan, CodeQL, Hypatia, documentation lint, + lock sync, and governance checks that already passed in that CI run. + +*Outputs:* a maintainer-approved repository-role decision, a check-by-check +baseline table with log links and reproduction status, and any narrowly scoped +follow-up change. Update the baseline-hazards table above with observed facts. + +*Acceptance:* each failed check is either fixed at source and green on a fresh +run, or explicitly documented as a known external/base blocker with owner and +next action. Do not mark the PR/release gate green while a required check is +failing or pending. + +*Stop conditions:* fixing a check requires renaming/removing template assets, +changing canonical pins, modifying branch protection, or broad placeholder +substitution without maintainer approval. Request that decision rather than +bypassing the check. + === WP-00 — Select target, owners, and assurance boundary *Priority:* P0; blocking for runtime- and choreography-specific proofs. @@ -523,6 +611,9 @@ acceptance evidence above. non-proof status. * [x] Preflight tests cover blocked state, bad arguments, and duplicate lock rows. +* [x] First PR's four failed CI steps and local placeholder reproduction + recorded as baseline hazards; root-cause triage remains open. +* [ ] WP-00A repository role and baseline CI failures reconciled. * [ ] WP-00 target/runtime, canonical-source locations, and ECHIDNA interface approved. * [ ] WP-01 toolchain and canonical artifacts independently pinned. @@ -537,20 +628,23 @@ acceptance evidence above. == First five actions -. **Maintainer:** decide WP-00 target and name the canonical source locations - and ECHIDNA owner/interface. This is the only step that should not be guessed - by a coding agent. +. **Maintainer / CI owner:** resolve WP-00A: decide whether this checkout is a + template or Bactrian product, then reproduce and classify the four failed + checks. Do not bulk-substitute placeholders or alter canonical pins before + that decision. +. **Maintainer / formal-methods owner:** decide WP-00 target and name the + canonical source locations and ECHIDNA owner/interface. This is the only + step that should not be guessed by a coding agent. . **Build/tooling contributor:** install and pin the OCaml compiler and Dune in the sanctioned provisioning setup; add a minimal project and prove that an empty `@verify` alias fails, while `@preflight` reports tools correctly. . **Formal-methods contributor:** inspect and record actual exported theorem signatures for the first Layer A authority path and define an artifact verification test. Do not reprove Agda results. -. **OCaml contributor:** implement one compiler-libs AST adapter and a tiny - positive/negative firewall fixture pair under the chosen compiler version. . **Integration contributor:** define ECHIDNA's actual request/receipt schema and validate an invalid witness rejection before investing in a wider VC - translator. + translator. Coordinate with the OCaml contributor on WP-04 after WP-00A and + WP-00 are resolved. After these five actions, update the active checklist from observed evidence, not from elapsed effort. Continue in dependency order; stop at any missing