From e742e2a6910dbcbf95037b410e7005d031fbccc7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 3 Jun 2026 00:04:05 +0100
Subject: [PATCH 1/7] feat(abi): add Tier-2 Idris bindings + retire legacy
 Foreign + close L10 transitive cycle
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three closures from the standards#124 Phase-5 follow-up:

A. **VclTotal.ABI.Foreign → VclTotal.Legacy.Foreign.** The legacy
   `libvqlut` pipeline binding (Zig-side `achieved_level` assertion,
   no Idris certificate) is moved to `src/interface/legacy/` with a
   deprecation banner pointing at Tier-1 (recompute-PCC over wasm32)
   and Tier-2 (Ed25519 signed attestation). The stale corpus symlink
   `corpus/VclTotal/ABI/Foreign.idr` is removed (Foreign was never in
   the proof corpus). New consumers should target the honest paths.

B. **NEW `VclTotal.ABI.Tier2` at `src/interface/abi/Tier2.idr`.**
   Idris bindings to the honest C ABI `vclut_verify_wire`
   (`ffi/zig/src/lib.zig` → `src/interface/attest::vclut_rs_verify`).
   Exposes `verifyWire : List Bits8 → List Bits8 → List Bits8 → IO
   Tier2Verdict` with a `Verified SafetyLevel (List Bits8) | Rejected
   String` typed sum and fail-closed contract at every layer (seed
   width check, alloc failure → Rejected, negative `c_int` →
   Rejected, out-of-range level → defensive Rejected). The 65-byte
   attestation `[level:1][sig:64]` is returned on success.

C. **L10 transitive ENTAILS cycle decider** (`src/core/Decide.idr`).
   `hasCircularEntails` (direct A⊨B ∧ B⊨A only) is supplemented by
   `hasTransitiveCycle`, which computes the transitive closure of
   the ENTAILS edge list to a `length pairs` fuel bound (finite,
   total) and reports any (x,x). `epiNoCycle` now uses the
   transitive form. Closes the L10 hole that the direct check
   missed.

Verification:
- `idris2 --build verification/proofs/vclut-core.ipkg` -> 12/12
  modules build clean from a fresh `build/`. Only pre-existing
  benign `n`-shadowing warnings in `Layout.idr`.
- `VclTotal.ABI.Tier2` typechecks cleanly when wired through the
  corpus tree (not added to the manifest because it is FFI plumbing,
  not a proof; same policy as `ABI.Foreign` was).
- VERIFICATION-STANCE.adoc updated to record L10 closure
  (Phase 4b/5), Foreign retirement (no longer an OWED), and Tier2
  as the consumer-facing replacement.
- ABI-FFI-README.adoc directory diagrams updated.

Trust model deltas:
- Tier-1 (recompute) remains the strongest tier; Tier-2 is the
  honest C-ABI fallback; legacy is documented as deprecated.
- No new axioms; no proof-escape symbols
  (no believe_me/postulate/assert_/sorry/idris_crash) in any
  proof-corpus module.

Refs hyperpolymath/standards#124 (Phase 5 follow-up).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 docs/developer/ABI-FFI-README.adoc            |  28 ++-
 src/core/Decide.idr                           |  79 ++++++-
 src/interface/abi/Tier2.idr                   | 209 ++++++++++++++++++
 src/interface/{abi => legacy}/Foreign.idr     |  62 ++++--
 verification/proofs/VERIFICATION-STANCE.adoc  | 121 +++++++---
 .../proofs/corpus/VclTotal/ABI/Foreign.idr    |   1 -
 6 files changed, 434 insertions(+), 66 deletions(-)
 create mode 100644 src/interface/abi/Tier2.idr
 rename src/interface/{abi => legacy}/Foreign.idr (78%)
 delete mode 120000 verification/proofs/corpus/VclTotal/ABI/Foreign.idr

diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc
index af10cee..02565fd 100644
--- a/docs/developer/ABI-FFI-README.adoc
+++ b/docs/developer/ABI-FFI-README.adoc
@@ -1,3 +1,5 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = ABI/FFI Standards
 {{~ Aditionally delete this line and fill out the template below ~}}
 
@@ -17,10 +19,13 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
 ```
 ┌─────────────────────────────────────────────┐
 │  ABI Definitions (Idris2)                   │
-│  src/abi/                                   │
+│  src/interface/abi/                         │
 │  - Types.idr      (Type definitions)        │
 │  - Layout.idr     (Memory layout proofs)    │
-│  - Foreign.idr    (FFI declarations)        │
+│  - LayoutProofs.idr (Alignment proofs)      │
+│  - Tier2.idr      (Honest signed-attest)    │
+│  src/interface/legacy/                      │
+│  - Foreign.idr    (DEPRECATED FFI decls)    │
 └─────────────────┬───────────────────────────┘
                   │
                   │ generates (at compile time)
@@ -53,11 +58,20 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
 ```
 vcl_total/
 ├── src/
-│   ├── abi/                    # ABI definitions (Idris2)
-│   │   ├── Types.idr           # Core type definitions with proofs
-│   │   ├── Layout.idr          # Memory layout verification
-│   │   └── Foreign.idr         # FFI function declarations
-│   └── lib/                    # Core library (any language)
+│   ├── interface/
+│   │   ├── abi/                # Honest ABI definitions (Idris2)
+│   │   │   ├── Types.idr       # Core type definitions with proofs
+│   │   │   ├── Layout.idr      # Memory layout (paddingFor, alignUp)
+│   │   │   ├── LayoutProofs.idr # Alignment-divides + bounds proofs
+│   │   │   └── Tier2.idr       # Idris bindings → vclut_verify_wire
+│   │   │                       # (Ed25519 attestation, honest path)
+│   │   ├── legacy/             # Pre-Phase-5 plumbing (DEPRECATED)
+│   │   │   └── Foreign.idr     # Legacy libvqlut bindings (Zig
+│   │   │                       # asserts level; no Idris certificate)
+│   │   ├── attest/             # Tier-2 Rust: signed attestation
+│   │   ├── recompute-wasm/     # Tier-1 Rust: consumer-side recompute
+│   │   └── ffi/                # Legacy Zig multi-stage pipeline
+│   └── core/                   # Idris2 corpus (the certifier itself)
 │
 ├── ffi/
 │   └── zig/                    # FFI implementation (Zig)
diff --git a/src/core/Decide.idr b/src/core/Decide.idr
index a0b1882..d19d26a 100644
--- a/src/core/Decide.idr
+++ b/src/core/Decide.idr
@@ -1,6 +1,5 @@
--- SPDX-License-Identifier: AGPL-3.0-or-later
--- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| VCL-total Core Decide — canonical safety deciders (single source of truth)
 |||
 ||| Phase 2 of the standards#124 HOLE remediation de-vacuizes the Level
@@ -672,14 +671,70 @@ entailsPairs (EpReqEntails a1 a2 _ :: rest) =
   (agentId a1, agentId a2) :: entailsPairs rest
 entailsPairs (_ :: rest) = entailsPairs rest
 
-||| Direct circular ENTAILS (a⊨b and b⊨a). Full graph-cycle detection is
-||| OWED (disclosed); this catches the direct symmetry violation.
+||| Direct circular ENTAILS (a⊨b and b⊨a). Retained as a fast-path /
+||| historical name; the canonical L10 check is `hasTransitiveCycle`
+||| below, which subsumes this case.
 public export
 hasCircularEntails : List EpistemicRequirement -> Bool
 hasCircularEntails reqs =
   let pairs = entailsPairs reqs
   in any (\(a, b) => any (\(c, d) => a == d && b == c) pairs) pairs
 
+-- ═══════════════════════════════════════════════════════════════════════
+-- Transitive ENTAILS cycle detection (Phase 5 OWED → RESOLVED)
+-- ═══════════════════════════════════════════════════════════════════════
+--
+-- The Phase-4b L10 check restricted itself to direct (a⊨b, b⊨a) cycles
+-- with full graph-cycle detection explicitly OWED in
+-- VERIFICATION-STANCE.adoc. The closure below upgrades the check to
+-- arbitrary-length cycles via finite-fuel transitive closure.
+--
+-- All three functions are structurally total. No believe_me /
+-- postulate / assert_* — pure list recursion.
+
+||| One step of transitive closure: for each `(a, b)` and `(b, c)` in
+||| `pairs`, add `(a, c)`. Returns the union of `pairs` and the one-hop
+||| extension (`++` rather than dedup; the cycle check `any ((==) <$> fst
+||| <*> snd)` is duplicate-insensitive).
+private
+extendFrom : List (String, String) -> (String, String) -> List (String, String)
+extendFrom pairs (a, b) =
+  map (\q => (a, snd q)) (filter (\q => fst q == b) pairs)
+
+public export
+transStep : List (String, String) -> List (String, String)
+transStep pairs = pairs ++ concatMap (extendFrom pairs) pairs
+
+||| Iterate `transStep` `n` times.
+public export
+transCloseN : Nat -> List (String, String) -> List (String, String)
+transCloseN Z       ps = ps
+transCloseN (S k)   ps = transCloseN k (transStep ps)
+
+||| Transitive closure of an ENTAILS edge list, fuel-bounded by
+||| `length pairs`. For a graph with `m` distinct edges, every reachable
+||| `(a, b)` is present after at most `m` doubling steps; `m` linear
+||| steps suffice because each step extends paths by one hop and any
+||| simple cycle of length `n` requires `n ≤ m` edges. (Non-simple paths
+||| cannot introduce new `(v, v)` edges that simple paths miss.)
+public export
+transClose : List (String, String) -> List (String, String)
+transClose ps = transCloseN (length ps) ps
+
+||| True iff the ENTAILS graph contains *any* cycle (direct or
+||| transitive). A cycle exists iff some self-edge `(a, a)` appears in
+||| the transitive closure.
+|||
+||| Strictly stronger than `hasCircularEntails`: every direct cycle is
+||| also a length-2 transitive cycle, and additionally catches
+||| `a⊨b⊨c⊨a` and longer chains.
+public export
+hasTransitiveCycle : List EpistemicRequirement -> Bool
+hasTransitiveCycle reqs =
+  let pairs  = entailsPairs reqs
+      closed = transClose pairs
+  in any (\p => fst p == snd p) closed
+
 ||| L10 STRUCTURAL part: an EPISTEMIC clause is present, has ≥1 agent,
 ||| and every requirement-referenced agent is declared. This is exactly
 ||| the part of L10 that IS closed under relational join (`joinEpistemic`
@@ -695,17 +750,25 @@ epiStructOK stmt = case epistemicClause stmt of
       []       => True
       (_ :: _) => False
 
-||| L10 ACYCLIC part: no direct (a⊨b, b⊨a) ENTAILS cycle among the
-||| clause's requirements. This is the ONE L10 sub-property that is
+||| L10 ACYCLIC part: no ENTAILS cycle (direct *or* transitive) among
+||| the clause's requirements. This is the ONE L10 sub-property that is
 ||| provably NOT closed under join (two acyclic requirement sets can
 ||| union to a cyclic one), so it is isolated here and supplied as an
 ||| explicit composition side-condition (see `Composition.JoinSideCondition`
 ||| and the disclosure in VERIFICATION-STANCE.adoc) — never faked.
+|||
+||| Phase 5 upgrade: previously routed through `hasCircularEntails`
+||| (direct cycles only); now uses `hasTransitiveCycle` (finite-fuel
+||| transitive closure), closing the disclosed "full graph-cycle
+||| detection OWED" gap. The body signature is unchanged, so all
+||| consumers (Checker / Composition / Levels) and the side-condition
+||| machinery continue to work verbatim — the predicate is just
+||| strictly stronger.
 public export
 epiNoCycle : Statement -> Bool
 epiNoCycle stmt = case epistemicClause stmt of
   Nothing                     => False
-  Just (EpClause _ reqs)      => not (hasCircularEntails reqs)
+  Just (EpClause _ reqs)      => not (hasTransitiveCycle reqs)
 
 ||| L10 — EpistemicSafe: clause present, ≥1 agent, all requirement agents
 ||| declared, AND no direct ENTAILS cycle. Mirrors `Checker.checkLevel10`
diff --git a/src/interface/abi/Tier2.idr b/src/interface/abi/Tier2.idr
new file mode 100644
index 0000000..70c0d15
--- /dev/null
+++ b/src/interface/abi/Tier2.idr
@@ -0,0 +1,209 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+||| VCL-total Tier-2 Foreign Function Interface (signed attestation)
+|||
+||| Idris-side bindings to the *honest* C ABI exposed by the Zig shim
+||| `ffi/zig/src/lib.zig` (`vclut_verify_wire`), which calls into the
+||| Rust crate `src/interface/attest` (`vclut_rs_verify`) — see
+||| `src/interface/attest/ATTESTATION-FORMAT.adoc` for the wire
+||| contract and `docs/decisions/0002-ffi-attestation-trust-boundary.adoc`
+||| for the trust model rationale.
+|||
+||| **Architectural role.** This module replaces the level-asserting
+||| legacy path (`VclTotal.Legacy.Foreign.getSafetyLevel`, deprecated
+||| 2026-06-02). Where the legacy path returned a Zig-side integer
+||| with no Idris verification, this module returns a 65-byte
+||| Ed25519-signed attestation
+|||
+|||   `token = [level : Bits8] ++ [signature : Vect 64 Bits8]`
+|||
+||| over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`
+||| (`DOMAIN = "VCLT-ATTEST-v1\0\0"`). The certifier signs *iff* the
+||| conformance-pinned `vcltotal_parse::certified_level` lies in
+||| `0..=10` — **fail-closed**, never a token for an unestablished
+||| level.
+|||
+||| **Trust model (Tier-2 ceiling).** A C ABI erases types to machine
+||| words; it cannot transport a re-checkable dependent
+||| `SafetyCertificate`. Over a C ABI the honest ceiling is
+||| trusted-certifier attestation, and that ceiling is what this
+||| module exposes. The consumer's TCB is:
+|||   (1) the certifier holds its Ed25519 key genuinely,
+|||   (2) the certifier ran the conformance-pinned decider before
+|||       signing,
+|||   (3) the Ed25519-dalek + sha2 implementation in the Tier-2 crate.
+|||
+||| **Strictly weaker than Tier-1** (recompute-PCC over `wasm32`,
+||| `src/interface/recompute-wasm`), which trusts neither (1) nor (2)
+||| because the consumer re-runs the decision itself. Prefer Tier-1
+||| where wasm hosting is available; Tier-2 is the C-ABI fallback.
+|||
+||| **No proofs.** Like all FFI plumbing, this module contains no
+||| theorems — its safety properties live in the Tier-2 Rust crate's
+||| tests (`src/interface/attest/src/lib.rs::tests` — roundtrip + 5
+||| tamper variants + fail-closed + C-ABI). It is *not* in the
+||| Idris2 proof corpus (`vclut-core.ipkg`); see
+||| `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary model"
+||| for what the Tier-2 ceiling does and does not guarantee.
+
+module VclTotal.ABI.Tier2
+
+import VclTotal.ABI.Types
+import Data.Buffer
+import Data.List
+
+%default total
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- Public surface
+-- ═══════════════════════════════════════════════════════════════════════
+
+||| Tier-2 verification verdict.
+|||
+|||   * `Verified lvl token` — certifier signed level `lvl`, attestation
+|||     bytes are in `token` (always 65 bytes: 1 level + 64 signature).
+|||   * `Rejected reason` — fail-closed; the certifier did not establish
+|||     a level (decode failure, malformed input, level outside
+|||     `0..=10`, or any other reject path). Token is NOT emitted.
+public export
+data Tier2Verdict : Type where
+  Verified : SafetyLevel -> List Bits8 -> Tier2Verdict
+  Rejected : String -> Tier2Verdict
+
+||| The fixed Ed25519 attestation token width (`level : 1 byte`
+||| + `signature : 64 bytes`).
+public export
+attestationTokenSize : Nat
+attestationTokenSize = 65
+
+||| Ed25519 seed/secret-key byte width.
+public export
+ed25519SeedSize : Nat
+ed25519SeedSize = 32
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- C ABI declarations
+-- ═══════════════════════════════════════════════════════════════════════
+
+||| The honest Tier-2 entry point. Bound to the Zig shim
+||| `vclut_verify_wire` in `ffi/zig/src/lib.zig`, which calls
+||| `vclut_rs_verify` (`src/interface/attest/src/lib.rs`).
+|||
+||| ABI:
+|||
+|||   ```c
+|||   int32_t vclut_verify_wire(
+|||       const uint8_t* stmt_ptr,   size_t stmt_len,
+|||       const uint8_t* schema_ptr, size_t schema_len,
+|||       const uint8_t* sk_ptr,                       /* 32 bytes */
+|||       uint8_t*       out_ptr,    size_t out_cap   /* >= 65 */
+|||   );
+|||   ```
+|||
+||| Returns `0..=10` on success (writes the 65-byte attestation to
+||| `out_ptr`), `-1` on Reject (no write). Pointers must each describe
+||| a valid range of the stated length; the function never reads or
+||| writes outside the documented spans. See the Rust crate's `Safety`
+||| comment for the precise contract.
+export
+%foreign "C:vclut_verify_wire, libvclut_ffi"
+prim__vclutVerifyWire :
+  Buffer -> Int ->     -- stmt
+  Buffer -> Int ->     -- schema
+  Buffer ->            -- 32-byte Ed25519 seed
+  Buffer -> Int ->     -- out + cap
+  PrimIO Int
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- Internal helpers
+-- ═══════════════════════════════════════════════════════════════════════
+
+||| Marshal a `List Bits8` into a freshly-allocated `Buffer`. Returns
+||| `Nothing` on allocation failure.
+private
+listToBuffer : List Bits8 -> IO (Maybe Buffer)
+listToBuffer xs = do
+  let n = length xs
+  Just buf <- newBuffer (cast n) | Nothing => pure Nothing
+  go buf 0 xs
+  pure (Just buf)
+  where
+    go : Buffer -> Int -> List Bits8 -> IO ()
+    go _   _ []        = pure ()
+    go buf i (b :: bs) = do
+      setBits8 buf i b
+      go buf (i + 1) bs
+
+||| Read the entire contents of a `Buffer` of declared length `n` into
+||| a `List Bits8`. Reads bytes `[0, n)` in order.
+private
+bufferToList : Buffer -> Int -> IO (List Bits8)
+bufferToList buf n = go 0 []
+  where
+    go : Int -> List Bits8 -> IO (List Bits8)
+    go i acc =
+      if i >= n
+        then pure (reverse acc)
+        else do
+          b <- getBits8 buf i
+          assert_total (go (i + 1) (b :: acc))
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- Safe public wrapper
+-- ═══════════════════════════════════════════════════════════════════════
+
+||| Verify a wire-marshalled `(Statement, OctadSchema)` pair via the
+||| Tier-2 signed-attestation backend. On success returns
+||| `Verified level token` with the 65-byte attestation; on any
+||| reject path returns `Rejected reason` with a human-readable cause.
+|||
+||| @param stmtWire   v1 statement-wire bytes (see
+|||                   `src/interface/parse/WIRE-FORMAT.adoc`)
+||| @param schemaWire v1 schema-wire bytes (`VCLS` magic)
+||| @param sk         the certifier's 32-byte Ed25519 *seed* (NOT a
+|||                   public key — this is the signing key). Real
+|||                   provisioning is deployment via the estate token
+|||                   vault.
+|||
+||| **Fail-closed contract.** This wrapper returns `Rejected` on:
+|||   * `sk` not exactly 32 bytes;
+|||   * buffer allocation failure (out of memory);
+|||   * any negative `c_int` from the C backend (decode failure,
+|||     malformed input, level outside `0..=10`);
+|||   * a return value outside `0..=10` (defensive — the backend's
+|||     contract already constrains this, but we re-check on the way
+|||     out).
+export
+verifyWire :
+  (stmtWire   : List Bits8) ->
+  (schemaWire : List Bits8) ->
+  (sk         : List Bits8) ->
+  IO Tier2Verdict
+verifyWire stmtWire schemaWire sk = do
+  if length sk /= ed25519SeedSize
+    then pure (Rejected
+      "Ed25519 seed must be exactly 32 bytes")
+    else do
+      Just stmtBuf   <- listToBuffer stmtWire
+        | Nothing => pure (Rejected "stmt buffer alloc failed")
+      Just schemaBuf <- listToBuffer schemaWire
+        | Nothing => pure (Rejected "schema buffer alloc failed")
+      Just skBuf     <- listToBuffer sk
+        | Nothing => pure (Rejected "sk buffer alloc failed")
+      Just outBuf    <- newBuffer (cast attestationTokenSize)
+        | Nothing => pure (Rejected "out buffer alloc failed")
+      let stmtLen   : Int = cast (length stmtWire)
+      let schemaLen : Int = cast (length schemaWire)
+      let outCap    : Int = cast attestationTokenSize
+      rc <- primIO (prim__vclutVerifyWire
+        stmtBuf stmtLen schemaBuf schemaLen skBuf outBuf outCap)
+      if rc < 0
+        then pure (Rejected
+          "Tier-2 backend Rejected (fail-closed): no certified level")
+        else case intToSafetyLevel (cast rc) of
+          Nothing  => pure (Rejected
+            "Tier-2 backend returned out-of-range level — defensive Reject")
+          Just lvl => do
+            token <- bufferToList outBuf (cast attestationTokenSize)
+            pure (Verified lvl token)
diff --git a/src/interface/abi/Foreign.idr b/src/interface/legacy/Foreign.idr
similarity index 78%
rename from src/interface/abi/Foreign.idr
rename to src/interface/legacy/Foreign.idr
index ab7dc45..2a96208 100644
--- a/src/interface/abi/Foreign.idr
+++ b/src/interface/legacy/Foreign.idr
@@ -1,33 +1,51 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
-||| VCL-total Foreign Function Interface Declarations
+||| VCL-total Legacy Foreign Function Interface Declarations (DEPRECATED)
 |||
-||| Declares all C-compatible functions implemented in the Zig FFI layer.
-||| The pipeline processes queries through progressive safety levels:
+||| ⚠️  DEPRECATED 2026-06-02 (standards#124, Phase 5+ follow-up).
 |||
-|||   parse -> bind_schema -> check_types -> check_effects -> compile
+||| This module binds Idris to the *legacy* Zig pipeline in
+||| `src/interface/ffi/src/main.zig`
+||| (`vqlut_parse → vqlut_bind_schema → vqlut_check_types →
+||| vqlut_check_effects → vqlut_compile → vqlut_get_safety_level`).
+||| The `achieved_level` field returned by `vqlut_get_safety_level` is
+||| *set by the Zig pipeline itself* based on which stage succeeded —
+||| it is a Zig-side trusted assertion, NOT a transported dependent
+||| proof and NOT an Idris-certified verdict. A C ABI cannot carry a
+||| `SafetyCertificate` (inherent architectural limit). The real
+||| verification authority is the Idris2 corpus certifier
+||| (`VclTotal.Core.Checker.certifyRequested` / `certifiedLevel`).
 |||
-||| Each stage returns a handle to an intermediate representation.
-||| The final query plan carries proof of the highest achieved safety level.
+||| Use the new honest paths instead:
 |||
-||| All functions are declared here with type signatures.
-||| Implementations live in ffi/zig/src/main.zig
+|||   * **Tier-1 (recompute-PCC over `wasm32`)** — consumer re-runs
+|||     the certified decision via `src/interface/recompute-wasm`
+|||     (`vcl_recompute`), comparing its verdict against the
+|||     producer's claim. No trusted certifier. See
+|||     `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary
+|||     model — two tiers".
 |||
-||| HONEST SCOPE (standards#124, Phase 3d). `getSafetyLevel` decodes a
-||| level *tag* from an FFI integer; that integer is an *attestation*
-||| from a trusted certifier, NOT a transported dependent proof — a C
-||| ABI cannot carry a `SafetyCertificate` (inherent). The real
-||| verification authority is the Idris2 corpus certifier
-||| (`VclTotal.Core.Checker.certifyRequested` / `certifiedLevel`), which
-||| only yields a level behind a genuine machine-checked certificate.
-||| The Zig shim is *fail-closed* as of Phase 3d (no fabricated level).
-||| This module is FFI plumbing — it contains *no proofs* and is not in
-||| the proof corpus. The string→AST parser, C-ABI Statement
-||| marshalling, and Idris→C build are NAMED OWED in
-||| verification/proofs/VERIFICATION-STANCE.adoc (absent, not faked).
-
-module VclTotal.ABI.Foreign
+|||   * **Tier-2 (C-ABI Ed25519 signed attestation, FALLBACK)** —
+|||     producer signs `(sha256(stmt_wire), sha256(schema_wire),
+|||     level)`; consumer Ed25519-verifies. See `src/interface/attest`
+|||     (`vclut_rs_verify`) and the Idris bindings in
+|||     `VclTotal.ABI.Tier2` (`src/interface/abi/Tier2.idr`).
+|||
+||| This file is kept ONLY so external C/Zig callers that linked
+||| against the legacy `libvqlut` ABI before Phase 5 can still find an
+||| Idris-side description of the function signatures. No part of the
+||| proof corpus imports it (the stale `corpus/VclTotal/ABI/Foreign.idr`
+||| symlink was removed). New Idris consumers should target
+||| `VclTotal.ABI.Tier2`.
+|||
+||| HONEST SCOPE (legacy text retained for context). `getSafetyLevel`
+||| decodes a level *tag* from an FFI integer; that integer is an
+||| *attestation* from a trusted certifier, NOT a transported dependent
+||| proof. The Zig shim is *fail-closed* as of Phase 3d (no fabricated
+||| level). This module is FFI plumbing — it contains *no proofs*.
+
+module VclTotal.Legacy.Foreign
 
 import VclTotal.ABI.Types
 import VclTotal.ABI.Layout
diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc
index 9047faf..237b715 100644
--- a/verification/proofs/VERIFICATION-STANCE.adoc
+++ b/verification/proofs/VERIFICATION-STANCE.adoc
@@ -1,9 +1,9 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = VCL-ut Verification Stance (proof-backed)
 :toc:
 :sectnums:
 
-// SPDX-License-Identifier: AGPL-3.0-or-later
-// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 WARNING: vcl-ut is the interface between *hypatia* and *verisim*; both sides
 trust safety claims made here. This document states *precisely* what is and is
@@ -167,21 +167,57 @@ OWED section.
   `fieldWithin` (membership-quantified bound: any field *provably in*
   the layout, via `Data.Vect.Elem` and `Data.So.soAnd`, satisfies
   `foff + fsize <= cap` — the honest replacement for the deleted false
-  `offsetInBounds`/`?metavariable`). *Remaining sliver (precisely
-  scoped, NOT faked):* the additive `Layout.alignUp size a = size +
-  paddingFor size a` ↔ ceil `alignTo size a` equivalence for `a > 0`,
-  left as the documented `String` note `alignUpAdditiveEquivOWED`
-  (needs the `Data.Nat` Euclidean identity + the `Bool`↔`Prop` bridge
-  for `paddingFor`'s conditional) — a scope note, never a
-  `believe_me`.
-  `VclTotal.ABI.Foreign` is *deliberately still excluded* but is *not
-  unsound*: it contains **no proofs at all** — only `%foreign` C
-  declarations and `Maybe`/`Either` wrappers. Its gaps are (a) it does
-  not compile as-is (FFI plumbing: missing `Data.Bits`, etc.) and (b)
-  the architectural stub-FFI issue (the level tag is an *asserted
-  integer* from the Zig side, not a transported proof). That is genuine
-  Phase 3+ architecture (implement the Zig/Rust side; transport an
-  opaque proof token), OWED and disclosed — not a false proof.
+  `offsetInBounds`/`?metavariable`). *Phase 5 — partial advance on the
+  additive↔ceil sliver:* the previously-`String` OWED
+  `alignUpAdditiveEquivOWED` is replaced by a real proof
+  infrastructure that closes the substantive content for the
+  zero-remainder case:
+    * `EuclidView`/`euclid` — the Euclidean decomposition view, built
+      from `Data.Nat.Division.DivisionTheorem` + `boundModNatNZ`.
+    * `sIdentZero`/`sIdentSucc` — Euclidean identity refinements
+      tagged by the value of `modNatNZ s (S k) ItIsSucc`.
+    * `sPlusMinus` — the `r ≤ k` ⇒ `S r + (k - r) = S k` identity.
+    * `alignUpADividesZero` — `(modNatNZ s (S k) ItIsSucc = Z) ⇒
+      Divides (S k) (alignUpA s k)`. Genuine `Refl`-closed theorem
+      with witness `divNatNZ s (S k) ItIsSucc`, zero proof-escape.
++
+  The remaining residual is purely the non-zero remainder case's
+  *rewrite chain*: the math is `S r' + (k `minus` r') = S k` (closed
+  by `sPlusMinus` + `boundModNatNZ`), but the multi-step
+  `plusAssociative`/`plusCommutative` chain triggers an idris2 0.8.0
+  elaborator quirk (`FromString` mis-elaboration). Disclosed as
+  `alignUpADividesSuccOWED` — a precisely-scoped String stub that
+  names the obstruction. Strictly smaller than the original OWED
+  (which covered both cases) and is a toolchain-sequencing limit
+  rather than a missing lemma. Re-attempt under idris2 0.8.1+ or via
+  manual `replace` chaining; tracked at standards#124 follow-up.
++
+  The `Data.Nat.Division` dependency is now declared in
+  `verification/proofs/vclut-core.ipkg` (`depends = contrib`); the
+  bundled idris2-contrib package is pure stdlib and adds no new
+  trusted axioms.
+  `VclTotal.ABI.Foreign` *has been retired* (2026-06-02). It is now
+  `VclTotal.Legacy.Foreign` at `src/interface/legacy/Foreign.idr`,
+  flagged DEPRECATED at the top of the file, with the stale
+  `corpus/VclTotal/ABI/Foreign.idr` symlink deleted. The file is
+  retained ONLY so external C/Zig callers that linked the legacy
+  `libvqlut` ABI before Phase 5 can still find an Idris-side
+  description; no part of the proof corpus imports it and no other
+  Idris module in this repo imports it (`grep -r "import
+  VclTotal.ABI.Foreign"` → 0). The architectural "asserted integer
+  instead of transported proof" issue is no longer a stand-alone
+  OWED: the *honest* Idris-side path is now
+  **`VclTotal.ABI.Tier2`** at `src/interface/abi/Tier2.idr`, which
+  binds `vclut_verify_wire` (Zig shim → `vclut_rs_verify` in
+  `src/interface/attest`) and returns a 65-byte Ed25519-signed
+  attestation `[level:1][sig:64]` over `DOMAIN ‖ sha256(stmt_wire)
+  ‖ sha256(schema_wire) ‖ level`. Trust-model ceiling is the same
+  Tier-2 ceiling described under the boundary model below
+  (strictly weaker than Tier-1 recompute-PCC; strictly stronger
+  than the deprecated asserted-integer path). The `Tier2.idr`
+  module typechecks under idris2 0.8.0 (`--check` green) and
+  carries no proofs (it is plumbing); the safety properties live
+  in `src/interface/attest/src/lib.rs::tests`.
 . *(Phase 2 — RESOLVED) L2/L3/L5 predicates de-vacuized.* The
   content-free constructors (`ExprTypeSafe`/`WhereTypeSafe`,
   `AllNullableFieldsGuarded`'s `GuardedNull`, `AllSelectItemsTyped`'s
@@ -223,14 +259,23 @@ OWED section.
   *structural* part (clause present, ≥1 agent, every requirement agent
   declared) — proved by genuine superset monotonicity
   (`fuaSuperset`/`agentDeclaredAppL`/`agentDeclaredAppR` +
-  `fuaNilAppend`), no proof-escape. L10's no-direct-`ENTAILS`-cycle
+  `fuaNilAppend`), no proof-escape. L10's no-`ENTAILS`-cycle
   sub-property is *provably NOT* join-closed and remains carried by
   the explicit minimal `JoinSideCondition` (`epiNoCycle (composeJoin
   q1 q2) = True` only at `EpistemicSafe`; `Unit` elsewhere) — stated
-  in the TYPE, never faked. *Still future work (precisely):*
-  deepening the L9/L10 *predicates themselves* to the full
-  `checkLevelN` semantics (L9 ≠ `LinUnlimited`; L10 acyclic `ENTAILS`
-  as a predicate rather than a side-condition). And the
+  in the TYPE, never faked. *(Phase 5 follow-up — RESOLVED.)* The L9
+  predicate deepening landed in Phase 4b already (`L9_LinearSafe`
+  carries `linearEnforcedStmt stmt = True`, which rejects both
+  absence AND `LinUnlimited` — see `Levels.idr` line 249), so the
+  "L9 ≠ `LinUnlimited`" item was a stance-doc lag, not real debt.
+  The L10 *direct-only* cycle check was upgraded to full transitive
+  graph-cycle detection via finite-fuel transitive closure
+  (`Decide.transStep`/`transCloseN`/`transClose`/
+  `hasTransitiveCycle`); `epiNoCycle` now routes through
+  `hasTransitiveCycle`, which is strictly stronger than the previous
+  `hasCircularEntails` and catches `a⊨b⊨c⊨a` and longer chains. The
+  `JoinSideCondition`'s body-agnostic shape means the existing
+  `compositionPreservation` proof continues to work verbatim. The
   certificate is still *not transported across the FFI* (see the
   `ABI.Foreign` item) — the in-corpus certificate is not yet a runtime
   proof token handed to hypatia/verisim.
@@ -341,8 +386,10 @@ OWED section.
   (`%default total`, zero proof-escape, fuel-bounded;
   `WireConformance` `Refl`-pins it byte-for-byte to the Rust
   `to_wire*` encoder, P5b-2 #29 / P5c-1 #30). The *encode* direction
-  (Idris `Statement`/`OctadSchema`→wire) remains OWED (not needed by
-  the recompute tier — the producer encodes from Rust). (3) *RESOLVED:*
+  (Idris `Statement`/`OctadSchema`→wire) is *deferred-by-design*
+  (not OWED): the recompute tier's producer encodes from Rust, so an
+  Idris encoder would only duplicate the conformance-pinned Rust
+  encoder for no additional consumer-side guarantee. (3) *RESOLVED:*
   the decision-transport tier is delivered as Tier-1 recompute-`wasm32`
   (P5c-5 #32) with the faithful Rust decision port machine-pinned to
   the corpus (P5c-2/3/4 #31). (4) *RESOLVED:* the P5d C-ABI
@@ -361,8 +408,18 @@ OWED section.
   `vector.x` unresolved → Reject) is pinned Rust-side (decoded
   self-check) + by input-value conformance (`conform2`), not by Idris
   `Refl`; the find-free decision structure *is* `Refl`-pinned. (iii)
-  the L9/L10 predicate depth and the additive↔ceil `alignUp` sliver
-  remain as previously scoped.
+  the additive↔ceil `alignUp` sliver
+  remains as previously scoped (Nat-arithmetic Euclidean-identity
+  infrastructure is the unwritten dependency; the practical
+  alignment-divides guarantee is already machine-checked via the
+  canonical-form `alignToDivides` theorem, so closing the additive
+  equivalence is a documentation tightening, not a safety upgrade).
+  *L9/L10 predicate depth (item iii in earlier revisions) is no
+  longer a disclosed limit*: L9 was deepened in Phase 4b
+  (`linearEnforcedStmt` rejects `LinUnlimited`); L10 acyclicity now
+  uses full transitive-closure cycle detection
+  (`Decide.hasTransitiveCycle`), not just direct symmetry — see the
+  Phase-5 follow-up note in the L6–L10 join-closure entry above.
 
 == Consumer guidance (hypatia / verisim)
 
@@ -384,8 +441,16 @@ OWED section.
   checks on the strength of a vcl-ut FFI level tag.
 * `VclTotal.ABI.Layout` is now *sound + CI-gated* (unsound claims
   deleted, not faked); its genuine alignment/no-padding theorems are
-  OWED. `VclTotal.ABI.Foreign` contains *no proofs* (FFI plumbing) — do
-  not treat its returned level tag as a verified claim.
+  OWED. `VclTotal.Legacy.Foreign` (formerly `VclTotal.ABI.Foreign`,
+  retired 2026-06-02) contains *no proofs* (FFI plumbing) and its
+  returned level tag is a Zig-side trusted assertion, NOT a verified
+  claim — *do not use the legacy bindings*. The honest Idris-side
+  path is **`VclTotal.ABI.Tier2`**, which returns a Tier-2
+  Ed25519-signed attestation: still trust-the-certifier (the C-ABI
+  ceiling), but cryptographically bound and tamper-evident, with the
+  Rust crate's test suite enforcing the fail-closed contract. For
+  the strongest guarantee, use Tier-1 recompute-PCC over `wasm32`
+  (`src/interface/recompute-wasm`).
 * *Transport (DELIVERED — Tier-1 recompute-PCC, P5c, vcl-ut#25).* The
   guarantee is **not** "trust our attestation". You are shipped the
   `wasm32` module `src/interface/recompute-wasm` (`vcl_recompute`) +
diff --git a/verification/proofs/corpus/VclTotal/ABI/Foreign.idr b/verification/proofs/corpus/VclTotal/ABI/Foreign.idr
deleted file mode 120000
index 4370b86..0000000
--- a/verification/proofs/corpus/VclTotal/ABI/Foreign.idr
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../src/interface/abi/Foreign.idr
\ No newline at end of file

From 06d64fc64376036e1203aba18c12475d57520ea6 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 3 Jun 2026 00:19:49 +0100
Subject: [PATCH 2/7] licence(ipkg): align vclut-core.ipkg SPDX header to
 MPL-2.0

Owner-directed single-file SPDX edit. Sibling proof-corpus files
(Decide.idr, LayoutProofs.idr, VERIFICATION-STANCE.adoc) committed at
28aac38 under MPL-2.0; this file lagged at AGPL-3.0-or-later (and
PMPL-1.0-or-later before a parallel sweep flipped it). Aligning to the
current vcl-ut policy.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 verification/proofs/vclut-core.ipkg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/verification/proofs/vclut-core.ipkg b/verification/proofs/vclut-core.ipkg
index 22d9d4c..582a7e4 100644
--- a/verification/proofs/vclut-core.ipkg
+++ b/verification/proofs/vclut-core.ipkg
@@ -1,5 +1,5 @@
--- SPDX-License-Identifier: AGPL-3.0-or-later
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 --
 -- Machine-check package for the VclTotal proof corpus (Phase 1,
 -- hyperpolymath/standards#124). The shipped sources live at flat paths

From 05b294bba16585d91c3bedfc9977a4900daa4f6a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 3 Jun 2026 13:38:56 +0100
Subject: [PATCH 3/7] docs: add OpenSSF Best Practices registration badge

---
 README.adoc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/README.adoc b/README.adoc
index c5f65d6..7d337bf 100644
--- a/README.adoc
+++ b/README.adoc
@@ -9,6 +9,7 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 image:https://zenodo.org/badge/DOI/10.5281/zenodo.19329501.svg[DOI,link="https://doi.org/10.5281/zenodo.19329501"]
 image:https://img.shields.io/badge/believe__me-0-brightgreen[believe_me: 0]
 image:https://img.shields.io/badge/tests-49_pass-brightgreen[tests: 49 pass]
+image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/vcl-ut"]
 
 IMPORTANT: This project was renamed on 2026-04-05. Its former name used
 the letter sequence "V-Q-L-hyphen-U-T" (read: "vee-queue-ell-you-tee") and

From 8215aac843ef6a7bc26c0ef6ccf05bca0b50971c Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:30:49 +0100
Subject: [PATCH 4/7] chore: normalise license to MPL-2.0

---
 .github/workflows/backend-matrix.yml       | 2 ++
 .github/workflows/boj-build.yml            | 1 +
 .github/workflows/cargo-audit.yml          | 1 +
 .github/workflows/codeql.yml               | 1 +
 .github/workflows/dependabot-automerge.yml | 1 +
 .github/workflows/dogfood-gate.yml         | 6 ++++++
 .github/workflows/e2e.yml                  | 3 +++
 .github/workflows/governance.yml           | 1 +
 .github/workflows/hypatia-scan.yml         | 1 +
 .github/workflows/instant-sync.yml         | 1 +
 .github/workflows/mirror.yml               | 1 +
 .github/workflows/openssf-compliance.yml   | 1 +
 .github/workflows/parse-gate.yml           | 1 +
 .github/workflows/proof-corpus.yml         | 1 +
 .github/workflows/release.yml              | 3 +++
 .github/workflows/rhodibot.yml             | 1 +
 .github/workflows/rust-ci.yml              | 1 +
 .github/workflows/scorecard-enforcer.yml   | 2 ++
 .github/workflows/scorecard.yml            | 1 +
 .github/workflows/secret-scanner.yml       | 1 +
 .github/workflows/static-analysis-gate.yml | 3 +++
 Cargo.toml                                 | 2 +-
 22 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/backend-matrix.yml b/.github/workflows/backend-matrix.yml
index 68093dc..1674a3f 100644
--- a/.github/workflows/backend-matrix.yml
+++ b/.github/workflows/backend-matrix.yml
@@ -37,6 +37,7 @@ jobs:
   prep:
     name: Derive matrix from echidna provers.a2ml
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     outputs:
       provers: ${{ steps.parse.outputs.provers }}
       count:   ${{ steps.parse.outputs.count }}
@@ -73,6 +74,7 @@ jobs:
     name: Smoke (${{ matrix.prover }})
     needs: prep
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     strategy:
       fail-fast: false
       max-parallel: 3
diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
index dba7fc8..bda0eec 100644
--- a/.github/workflows/boj-build.yml
+++ b/.github/workflows/boj-build.yml
@@ -7,6 +7,7 @@ on:
 jobs:
   trigger-boj:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332 # v4.1.7
diff --git a/.github/workflows/cargo-audit.yml b/.github/workflows/cargo-audit.yml
index 357440d..e69f8bc 100644
--- a/.github/workflows/cargo-audit.yml
+++ b/.github/workflows/cargo-audit.yml
@@ -21,6 +21,7 @@ jobs:
   audit:
     name: Dependency audit
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     if: hashFiles('Cargo.lock') != ''
 
     steps:
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
index ab8ae8b..c9e9460 100644
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -23,6 +23,7 @@ permissions:
 jobs:
   analyze:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
       security-events: write
diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml
index 92b5254..6d98f9c 100644
--- a/.github/workflows/dependabot-automerge.yml
+++ b/.github/workflows/dependabot-automerge.yml
@@ -50,6 +50,7 @@ jobs:
     # Only run for PRs actually authored by Dependabot.
     if: github.actor == 'dependabot[bot]' && github.event.pull_request.user.login == 'dependabot[bot]'
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Fetch Dependabot metadata
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index a9b8da5..3807e9a 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -22,6 +22,7 @@ jobs:
   a2ml-validate:
     name: Validate A2ML manifests
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -66,6 +67,7 @@ jobs:
   k9-validate:
     name: Validate K9 contracts
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -115,6 +117,7 @@ jobs:
   empty-lint:
     name: Empty-linter (invisible characters)
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -179,6 +182,7 @@ jobs:
   groove-check:
     name: Groove manifest check
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -237,6 +241,7 @@ jobs:
   eclexiaiser-validate:
     name: Validate eclexiaiser manifest
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -300,6 +305,7 @@ print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
     if: always()
 
diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 271fd60..ad25275 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -9,6 +9,7 @@ jobs:
   e2e:
     name: E2E structural validation
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
       - name: Install Rust
@@ -19,6 +20,7 @@ jobs:
   property:
     name: Property and integration tests
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
       - name: Install Rust
@@ -31,6 +33,7 @@ jobs:
   aspect:
     name: Aspect tests
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
       - name: Run aspect tests
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 653ef98..bddff42 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -32,3 +32,4 @@ permissions:
 jobs:
   governance:
     uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main
+    timeout-minutes: 10
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index 9e384bc..36a631d 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -26,4 +26,5 @@ permissions:
 jobs:
   hypatia:
     uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@2569c10e831e293f9dd6580d82a494aca039deee
+    timeout-minutes: 10
     secrets: inherit
diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml
index 228dc43..01646a7 100644
--- a/.github/workflows/instant-sync.yml
+++ b/.github/workflows/instant-sync.yml
@@ -14,6 +14,7 @@ permissions:
 jobs:
   dispatch:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Trigger Propagation
         uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index 2083ca6..ee8ea02 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -12,4 +12,5 @@ permissions:
 jobs:
   mirror:
     uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@e6b2884722350515934d443daf23442f2195796f
+    timeout-minutes: 10
     secrets: inherit
diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml
index c2262ed..6f00e2a 100644
--- a/.github/workflows/openssf-compliance.yml
+++ b/.github/workflows/openssf-compliance.yml
@@ -16,6 +16,7 @@ permissions:
 jobs:
   openssf-compliance:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:
diff --git a/.github/workflows/parse-gate.yml b/.github/workflows/parse-gate.yml
index ad1761e..58a3258 100644
--- a/.github/workflows/parse-gate.yml
+++ b/.github/workflows/parse-gate.yml
@@ -28,6 +28,7 @@ jobs:
   parse-gate:
     name: vcltotal-parse — panic-free / clippy / tests
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
diff --git a/.github/workflows/proof-corpus.yml b/.github/workflows/proof-corpus.yml
index 9d0a66c..430aa20 100644
--- a/.github/workflows/proof-corpus.yml
+++ b/.github/workflows/proof-corpus.yml
@@ -32,6 +32,7 @@ jobs:
   machine-check:
     name: idris2 0.8.0 --build vclut-core
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index b80da1c..e179cb3 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -18,6 +18,7 @@ jobs:
   build:
     name: Build Artifacts
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:
@@ -42,6 +43,7 @@ jobs:
   changelog:
     name: Generate Changelog
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     outputs:
@@ -88,6 +90,7 @@ jobs:
     name: Create GitHub Release
     needs: [build, changelog]
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: write
     steps:
diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml
index a82f178..471d9d4 100644
--- a/.github/workflows/rhodibot.yml
+++ b/.github/workflows/rhodibot.yml
@@ -27,6 +27,7 @@ permissions:
 jobs:
   rhodibot:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
index 1b1b792..040a198 100644
--- a/.github/workflows/rust-ci.yml
+++ b/.github/workflows/rust-ci.yml
@@ -15,3 +15,4 @@ permissions:
 jobs:
   rust-ci:
     uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@cc5a372af1af1b202c17f1b21efd954e6c038bef
+    timeout-minutes: 10
diff --git a/.github/workflows/scorecard-enforcer.yml b/.github/workflows/scorecard-enforcer.yml
index 6933b78..57535d0 100644
--- a/.github/workflows/scorecard-enforcer.yml
+++ b/.github/workflows/scorecard-enforcer.yml
@@ -23,6 +23,7 @@ permissions:
 jobs:
   scorecard:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       security-events: write
       id-token: write  # For OIDC
@@ -61,6 +62,7 @@ jobs:
   # Check specific high-priority items
   check-critical:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index f99d361..d5b33eb 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -13,4 +13,5 @@ permissions: read-all
 jobs:
   analysis:
     uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@e0caf11508a3989574713c78f5f444f2ce5e33ef
+    timeout-minutes: 10
     secrets: inherit
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index 097d2af..c7761fe 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -16,4 +16,5 @@ permissions:
 jobs:
   scan:
     uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0
+    timeout-minutes: 10
     secrets: inherit
diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml
index 367699a..e5dc460 100644
--- a/.github/workflows/static-analysis-gate.yml
+++ b/.github/workflows/static-analysis-gate.yml
@@ -22,6 +22,7 @@ jobs:
   panic-attack-assail:
     name: panic-attack assail
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -130,6 +131,7 @@ jobs:
   hypatia-scan:
     name: Hypatia neurosymbolic scan
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout repository
@@ -242,6 +244,7 @@ jobs:
   deposit-findings:
     name: Deposit findings for gitbot-fleet
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     needs: [panic-attack-assail, hypatia-scan]
     if: always()
 
diff --git a/Cargo.toml b/Cargo.toml
index 0b607ec..84fa618 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 name = "vcl-total"
 version = "0.1.0"
 edition = "2021"
-license = "AGPL-3.0-or-later"
+license = "MPL-2.0"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 repository = "https://github.com/hyperpolymath/vql-ut"
 description = "VCL-total: 10-level type-safe query language for VeriSimDB"

From 91259c13950c3a063b87baf23af3f188a20e725b Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:53:55 +0100
Subject: [PATCH 5/7] chore: rename k9 directories to self-validating for
 clarity

---
 .machine_readable/MUST.contractile                 |  4 ++--
 .../contractiles/adjust/Adjustfile.a2ml            |  2 +-
 .../svc/{k9 => self-validating}/README.adoc        | 14 +++++++-------
 .../examples/ci-config.k9.ncl                      |  0
 .../examples/project-metadata.k9.ncl               |  0
 .../examples/setup-repo.k9.ncl                     |  2 +-
 .../{k9 => self-validating}/template-hunt.k9.ncl   |  0
 .../{k9 => self-validating}/template-kennel.k9.ncl |  0
 .../{k9 => self-validating}/template-yard.k9.ncl   |  0
 9 files changed, 11 insertions(+), 11 deletions(-)
 rename .machine_readable/svc/{k9 => self-validating}/README.adoc (89%)
 rename .machine_readable/svc/{k9 => self-validating}/examples/ci-config.k9.ncl (100%)
 rename .machine_readable/svc/{k9 => self-validating}/examples/project-metadata.k9.ncl (100%)
 rename .machine_readable/svc/{k9 => self-validating}/examples/setup-repo.k9.ncl (98%)
 rename .machine_readable/svc/{k9 => self-validating}/template-hunt.k9.ncl (100%)
 rename .machine_readable/svc/{k9 => self-validating}/template-kennel.k9.ncl (100%)
 rename .machine_readable/svc/{k9 => self-validating}/template-yard.k9.ncl (100%)

diff --git a/.machine_readable/MUST.contractile b/.machine_readable/MUST.contractile
index 7cbb85c..5824115 100644
--- a/.machine_readable/MUST.contractile
+++ b/.machine_readable/MUST.contractile
@@ -26,7 +26,7 @@
 ;     remain active until the feature is fully removed.
 ;
 ; Enforcement:
-;   K9 validators in contractiles/k9/ machine-check MUST constraints.
+;   K9 validators in contractiles/self-validating/ machine-check MUST constraints.
 ;   CI runs these on every PR. Violations block merge.
 ;
 ; ── End Definitions ──────────────────────────────────────────────
@@ -85,7 +85,7 @@
   ; (must "# Add project-specific invariants here")
 
   (enforcement
-    (k9-validator "contractiles/k9/must-check.k9.ncl")
+    (k9-validator "contractiles/self-validating/must-check.k9.ncl")
     (ci "quality.yml runs must-check on every PR")
   )
 )
diff --git a/.machine_readable/contractiles/adjust/Adjustfile.a2ml b/.machine_readable/contractiles/adjust/Adjustfile.a2ml
index 24f400f..571669e 100644
--- a/.machine_readable/contractiles/adjust/Adjustfile.a2ml
+++ b/.machine_readable/contractiles/adjust/Adjustfile.a2ml
@@ -181,7 +181,7 @@ These requirements ensure Burble is usable by everyone, regardless of ability.
 ### k9-accessibility-validator
 - description: Integrate K9 accessibility validator
 - status: planned
-- reference: /var/mnt/eclipse/repos/panll/contractiles/k9/validators/accessibility-baseline.k9.ncl
+- reference: /var/mnt/eclipse/repos/panll/contractiles/self-validating/validators/accessibility-baseline.k9.ncl
 - target: Q2 2026
 
 ### accessibility-testing
diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/self-validating/README.adoc
similarity index 89%
rename from .machine_readable/svc/k9/README.adoc
rename to .machine_readable/svc/self-validating/README.adoc
index eeb1229..48858ca 100644
--- a/.machine_readable/svc/k9/README.adoc
+++ b/.machine_readable/svc/self-validating/README.adoc
@@ -71,13 +71,13 @@ Choose the appropriate security level for your use case:
 [source,bash]
 ----
 # Kennel: Pure configuration
-cp .machine_readable/contractiles/k9/examples/project-metadata.k9.ncl config/metadata.k9.ncl
+cp .machine_readable/contractiles/self-validating/examples/project-metadata.k9.ncl config/metadata.k9.ncl
 
 # Yard: Validated configuration
-cp .machine_readable/contractiles/k9/examples/ci-config.k9.ncl .github/ci.k9.ncl
+cp .machine_readable/contractiles/self-validating/examples/ci-config.k9.ncl .github/ci.k9.ncl
 
 # Hunt: Full automation
-cp .machine_readable/contractiles/k9/examples/setup-repo.k9.ncl scripts/setup.k9.ncl
+cp .machine_readable/contractiles/self-validating/examples/setup-repo.k9.ncl scripts/setup.k9.ncl
 ----
 
 === 2. Validate Components
@@ -130,7 +130,7 @@ K9 contractiles integrate with other RSR standards:
 ⚠️ **Never run as root unless required** +
 ⚠️ **Sandbox external components**
 
-**See:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/docs/SECURITY-BEST-PRACTICES.adoc
+**See:** https://github.com/hyperpolymath/standards/blob/main/self-validating/docs/SECURITY-BEST-PRACTICES.adoc
 
 == Template Files
 
@@ -160,9 +160,9 @@ git clone https://github.com/hyperpolymath/standards.git
 
 == Learn More
 
-- **K9-SVC Specification:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/SPEC.adoc
-- **K9 User Guide:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/GUIDE.adoc
-- **Security Documentation:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/docs/SECURITY-FAQ.adoc
+- **K9-SVC Specification:** https://github.com/hyperpolymath/standards/blob/main/self-validating/SPEC.adoc
+- **K9 User Guide:** https://github.com/hyperpolymath/standards/blob/main/self-validating/GUIDE.adoc
+- **Security Documentation:** https://github.com/hyperpolymath/standards/blob/main/self-validating/docs/SECURITY-FAQ.adoc
 - **IANA Media Type:** `application/vnd.k9+nickel`
 
 == Contributing
diff --git a/.machine_readable/svc/k9/examples/ci-config.k9.ncl b/.machine_readable/svc/self-validating/examples/ci-config.k9.ncl
similarity index 100%
rename from .machine_readable/svc/k9/examples/ci-config.k9.ncl
rename to .machine_readable/svc/self-validating/examples/ci-config.k9.ncl
diff --git a/.machine_readable/svc/k9/examples/project-metadata.k9.ncl b/.machine_readable/svc/self-validating/examples/project-metadata.k9.ncl
similarity index 100%
rename from .machine_readable/svc/k9/examples/project-metadata.k9.ncl
rename to .machine_readable/svc/self-validating/examples/project-metadata.k9.ncl
diff --git a/.machine_readable/svc/k9/examples/setup-repo.k9.ncl b/.machine_readable/svc/self-validating/examples/setup-repo.k9.ncl
similarity index 98%
rename from .machine_readable/svc/k9/examples/setup-repo.k9.ncl
rename to .machine_readable/svc/self-validating/examples/setup-repo.k9.ncl
index d1fc8bb..c05a160 100644
--- a/.machine_readable/svc/k9/examples/setup-repo.k9.ncl
+++ b/.machine_readable/svc/self-validating/examples/setup-repo.k9.ncl
@@ -95,7 +95,7 @@ K9!
       commands = [
         "mkdir -p src/ docs/ tests/ scripts/",
         "mkdir -p .github/workflows/",
-        "mkdir -p .machine_readable/contractiles/k9/",
+        "mkdir -p .machine_readable/contractiles/self-validating/",
         "echo '✓ Directory structure created'",
       ],
     },
diff --git a/.machine_readable/svc/k9/template-hunt.k9.ncl b/.machine_readable/svc/self-validating/template-hunt.k9.ncl
similarity index 100%
rename from .machine_readable/svc/k9/template-hunt.k9.ncl
rename to .machine_readable/svc/self-validating/template-hunt.k9.ncl
diff --git a/.machine_readable/svc/k9/template-kennel.k9.ncl b/.machine_readable/svc/self-validating/template-kennel.k9.ncl
similarity index 100%
rename from .machine_readable/svc/k9/template-kennel.k9.ncl
rename to .machine_readable/svc/self-validating/template-kennel.k9.ncl
diff --git a/.machine_readable/svc/k9/template-yard.k9.ncl b/.machine_readable/svc/self-validating/template-yard.k9.ncl
similarity index 100%
rename from .machine_readable/svc/k9/template-yard.k9.ncl
rename to .machine_readable/svc/self-validating/template-yard.k9.ncl

From 233fc741233b332105db585e8e0c70a205b86cef Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 4 Jun 2026 18:05:12 +0100
Subject: [PATCH 6/7] chore: flatten self-validating directory structure

---
 .machine_readable/{svc => }/self-validating/README.adoc           | 0
 .../{svc => }/self-validating/examples/ci-config.k9.ncl           | 0
 .../{svc => }/self-validating/examples/project-metadata.k9.ncl    | 0
 .../{svc => }/self-validating/examples/setup-repo.k9.ncl          | 0
 .machine_readable/{svc => }/self-validating/template-hunt.k9.ncl  | 0
 .../{svc => }/self-validating/template-kennel.k9.ncl              | 0
 .machine_readable/{svc => }/self-validating/template-yard.k9.ncl  | 0
 7 files changed, 0 insertions(+), 0 deletions(-)
 rename .machine_readable/{svc => }/self-validating/README.adoc (100%)
 rename .machine_readable/{svc => }/self-validating/examples/ci-config.k9.ncl (100%)
 rename .machine_readable/{svc => }/self-validating/examples/project-metadata.k9.ncl (100%)
 rename .machine_readable/{svc => }/self-validating/examples/setup-repo.k9.ncl (100%)
 rename .machine_readable/{svc => }/self-validating/template-hunt.k9.ncl (100%)
 rename .machine_readable/{svc => }/self-validating/template-kennel.k9.ncl (100%)
 rename .machine_readable/{svc => }/self-validating/template-yard.k9.ncl (100%)

diff --git a/.machine_readable/svc/self-validating/README.adoc b/.machine_readable/self-validating/README.adoc
similarity index 100%
rename from .machine_readable/svc/self-validating/README.adoc
rename to .machine_readable/self-validating/README.adoc
diff --git a/.machine_readable/svc/self-validating/examples/ci-config.k9.ncl b/.machine_readable/self-validating/examples/ci-config.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/examples/ci-config.k9.ncl
rename to .machine_readable/self-validating/examples/ci-config.k9.ncl
diff --git a/.machine_readable/svc/self-validating/examples/project-metadata.k9.ncl b/.machine_readable/self-validating/examples/project-metadata.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/examples/project-metadata.k9.ncl
rename to .machine_readable/self-validating/examples/project-metadata.k9.ncl
diff --git a/.machine_readable/svc/self-validating/examples/setup-repo.k9.ncl b/.machine_readable/self-validating/examples/setup-repo.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/examples/setup-repo.k9.ncl
rename to .machine_readable/self-validating/examples/setup-repo.k9.ncl
diff --git a/.machine_readable/svc/self-validating/template-hunt.k9.ncl b/.machine_readable/self-validating/template-hunt.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/template-hunt.k9.ncl
rename to .machine_readable/self-validating/template-hunt.k9.ncl
diff --git a/.machine_readable/svc/self-validating/template-kennel.k9.ncl b/.machine_readable/self-validating/template-kennel.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/template-kennel.k9.ncl
rename to .machine_readable/self-validating/template-kennel.k9.ncl
diff --git a/.machine_readable/svc/self-validating/template-yard.k9.ncl b/.machine_readable/self-validating/template-yard.k9.ncl
similarity index 100%
rename from .machine_readable/svc/self-validating/template-yard.k9.ncl
rename to .machine_readable/self-validating/template-yard.k9.ncl

From a185ae9d8612e0f3ff78b9eb88fb0bdcb1d10a97 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 4 Jun 2026 18:55:22 +0100
Subject: [PATCH 7/7] chore: rename agent_instructions to bot_directives for
 spec alignment

---
 .../{agent_instructions => bot_directives}/README.adoc          | 2 +-
 .../{agent_instructions => bot_directives}/coverage.a2ml        | 0
 .../{agent_instructions => bot_directives}/debt.a2ml            | 0
 .../{agent_instructions => bot_directives}/methodology.a2ml     | 0
 4 files changed, 1 insertion(+), 1 deletion(-)
 rename .machine_readable/{agent_instructions => bot_directives}/README.adoc (94%)
 rename .machine_readable/{agent_instructions => bot_directives}/coverage.a2ml (100%)
 rename .machine_readable/{agent_instructions => bot_directives}/debt.a2ml (100%)
 rename .machine_readable/{agent_instructions => bot_directives}/methodology.a2ml (100%)

diff --git a/.machine_readable/agent_instructions/README.adoc b/.machine_readable/bot_directives/README.adoc
similarity index 94%
rename from .machine_readable/agent_instructions/README.adoc
rename to .machine_readable/bot_directives/README.adoc
index 9bc2e24..4e989c7 100644
--- a/.machine_readable/agent_instructions/README.adoc
+++ b/.machine_readable/bot_directives/README.adoc
@@ -32,7 +32,7 @@ Methodology-aware configuration for AI agents. Read by any AI agent
 == Relationship to Other Files
 
 * `AGENTIC.a2ml` says WHAT agents can do (permissions, gating)
-* `agent_instructions/` says HOW agents should work (methodology)
+* `bot_directives/` says HOW agents should work (methodology)
 * `bot_directives/` says what the gitbot-fleet does (fleet-specific)
 * `CLAUDE.md` says how Claude specifically should work (Claude-specific)
 
diff --git a/.machine_readable/agent_instructions/coverage.a2ml b/.machine_readable/bot_directives/coverage.a2ml
similarity index 100%
rename from .machine_readable/agent_instructions/coverage.a2ml
rename to .machine_readable/bot_directives/coverage.a2ml
diff --git a/.machine_readable/agent_instructions/debt.a2ml b/.machine_readable/bot_directives/debt.a2ml
similarity index 100%
rename from .machine_readable/agent_instructions/debt.a2ml
rename to .machine_readable/bot_directives/debt.a2ml
diff --git a/.machine_readable/agent_instructions/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml
similarity index 100%
rename from .machine_readable/agent_instructions/methodology.a2ml
rename to .machine_readable/bot_directives/methodology.a2ml