From 875b9c6169beef76e7dd6930216ade9395b8f9e9 Mon Sep 17 00:00:00 2001
From: Claude <paraordinate@yahoo.co.uk>
Date: Wed, 3 Jun 2026 18:18:12 +0000
Subject: [PATCH 1/4] feat(typechecker): integrate echo-types as Layer 10
 reversibility (Echo residue)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Make 007's reversibility fragment type-checked. `reversible` / `irreversible`
/ `reverse` were checked identically; the type system now tracks an Echo
residue per body (reversible retains one, irreversible discards it, reverse
consumes one) and rejects a `reverse` with no residue as
ReverseWithoutResidue — enforcing OPERATIONAL-SEMANTICS §11.3, which was
previously unenforced.

Grounded in echo-types' keystone A ≃ Σ B (Echo f): irreversible + echo =
reversible. Mechanised in proofs/idris2/EchoResidue.idr (encodeDecode,
reverseAfterIrreversibleIllTyped, collapseHasNoSection; %default total,
zero believe_me).

- typechecker.rs: Type::Echo<T>, per-body residue stack on TypeEnv, split
  typing rule, per-function/per-handler residue isolation (no cross-body leak)
- agent_api.rs: agent-facing L10_REVERSE_WITHOUT_RESIDUE + mark_reversible /
  retain_echo remediations
- typechecker_tests.rs: 4 tests (880 oo7-core lib tests passing)
- spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4
- docs/echo-residue-integration.adoc: integration + phase-2 linear-undo rung

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
---
 CHANGELOG.md                             |   1 +
 crates/oo7-core/src/agent_api.rs         |  32 ++++
 crates/oo7-core/src/typechecker.rs       | 106 +++++++++++-
 crates/oo7-core/src/typechecker_tests.rs | 100 ++++++++++++
 docs/echo-residue-integration.adoc       | 120 ++++++++++++++
 proofs/idris2/EchoResidue.idr            | 198 +++++++++++++++++++++++
 spec/OPERATIONAL-SEMANTICS.adoc          |  27 ++++
 spec/TYPE-SYSTEM-SPEC.adoc               |  72 +++++++++
 8 files changed, 655 insertions(+), 1 deletion(-)
 create mode 100644 docs/echo-residue-integration.adoc
 create mode 100644 proofs/idris2/EchoResidue.idr

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 360b866..3379475 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,7 @@ All notable changes to this project will be documented in this file.
 ## [Unreleased] — 2026-04-10 consolidation pass
 
 ### Added
+- **Layer 10 — Reversibility (Echo residue): echo-types integrated into the type system.** `reversible`/`irreversible`/`reverse` are no longer checked identically: `Type::Echo<T>` residues are tracked per body (`reversible` retains one, `irreversible` discards it, `reverse` consumes one), and a `reverse` with no residue is `ReverseWithoutResidue` — enforcing OPERATIONAL-SEMANTICS §11.3, previously unenforced. Grounded in echo-types' keystone `A ≃ Σ B (Echo f)` and mechanised in `proofs/idris2/EchoResidue.idr` (`encodeDecode`, `reverseAfterIrreversibleIllTyped`, `collapseHasNoSection`; `%default total`, zero `believe_me`). Surfaced to agents via `agent_api` code `L10_REVERSE_WITHOUT_RESIDUE` (+`mark_reversible`/`retain_echo` remediations). 4 new typechecker tests (880 `oo7-core` lib tests passing). Spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4; design note `docs/echo-residue-integration.adoc` (incl. the phase-2 linear-undo-capability rung).
 - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`.
 - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status.
 - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches.
diff --git a/crates/oo7-core/src/agent_api.rs b/crates/oo7-core/src/agent_api.rs
index 81c515c..dfb49f9 100644
--- a/crates/oo7-core/src/agent_api.rs
+++ b/crates/oo7-core/src/agent_api.rs
@@ -627,6 +627,38 @@ fn type_error_to_agent_error(te: &typechecker::TypeError) -> AgentError {
                 },
             ],
         },
+
+        // L10 reversibility (echo-types residue tracking). Surfaced to the
+        // agent as an actionable choice: retain the reversal log, or stop
+        // trying to reverse an irreversible step. The residue IS the
+        // type-level shadow of the `trace` an irreversible step discards.
+        TypeErrorKind::ReverseWithoutResidue { detail } => AgentError {
+            code: "L10_REVERSE_WITHOUT_RESIDUE".to_string(),
+            level: 10,
+            message: te.message.clone(),
+            location: None,
+            context: serde_json::json!({ "detail": detail }),
+            remediations: vec![
+                Remediation {
+                    strategy: "mark_reversible".to_string(),
+                    description: "Wrap the operations to be undone in a \
+                         `reversible { ... }` block so an Echo residue (the \
+                         reversal log) is retained for `reverse` to replay"
+                        .to_string(),
+                    confidence: 0.85,
+                    patch: None,
+                },
+                Remediation {
+                    strategy: "retain_echo".to_string(),
+                    description: "If the step must stay `irreversible`, do not \
+                         `reverse` it; capture the inputs it discards (its Echo \
+                         residue) before the step and restore them explicitly"
+                        .to_string(),
+                    confidence: 0.6,
+                    patch: None,
+                },
+            ],
+        },
     }
 }
 
diff --git a/crates/oo7-core/src/typechecker.rs b/crates/oo7-core/src/typechecker.rs
index a3ce6b7..eb43db1 100644
--- a/crates/oo7-core/src/typechecker.rs
+++ b/crates/oo7-core/src/typechecker.rs
@@ -99,6 +99,15 @@ pub enum Type {
     Effectful(Box<Type>, Vec<String>),
     /// Path type: `Path(T1, T2)`.
     Path(Box<Type>, Box<Type>),
+    /// Echo residue type: `Echo<T>` — the residue ("reversal log") that a
+    /// `reversible` block retains, recording what an otherwise irreversible
+    /// step would discard. From echo-types (hyperpolymath/echo-types):
+    /// `Echo f y := Σ (x : A), f x = y`, with the keystone
+    /// `A ≃ Σ B (Echo f)` — irreversible computation plus its echo is
+    /// reversible. A `reverse` block is well-typed only when such a residue
+    /// is in scope. The keystone and the typing rule are mechanised in
+    /// proofs/idris2/EchoResidue.idr.
+    Echo(Box<Type>),
     /// Error recovery sentinel — propagates without cascading errors.
     Error,
 }
@@ -199,6 +208,7 @@ impl fmt::Display for Type {
             Type::Graded(grade, inner) => write!(f, "@graded({}) {}", grade, inner),
             Type::Effectful(base, effects) => write!(f, "{} !{{{}}}", base, effects.join(", ")),
             Type::Path(a, b) => write!(f, "Path({}, {})", a, b),
+            Type::Echo(inner) => write!(f, "Echo<{}>", inner),
             Type::Error => write!(f, "<error>"),
         }
     }
@@ -337,6 +347,17 @@ pub enum TypeErrorKind {
         /// The operation: "/" or "%"
         op: String,
     },
+    /// Reversibility violation (Kategoria Level 10, echo-types residue
+    /// tracking). A `reverse` block has no Echo residue in scope — it
+    /// either targets an `irreversible` block or has no preceding
+    /// `reversible` block to replay. spec/OPERATIONAL-SEMANTICS.adoc §11.3
+    /// requires this to be a compile-time error; the soundness ground is
+    /// echo-types' `A ≃ Σ B (Echo f)` (proofs/idris2/EchoResidue.idr): a
+    /// step is reversible only when its echo residue is retained.
+    ReverseWithoutResidue {
+        /// Human/agent-readable explanation of which residue is missing.
+        detail: String,
+    },
 }
 
 impl fmt::Display for TypeError {
@@ -489,6 +510,13 @@ pub struct TypeEnv {
     /// The witness is removed before the `else` branch (where `d` may be zero)
     /// and after the `if` statement.
     pub nonzero_witnesses: HashSet<String>,
+    /// L10 reversibility: the stack of Echo residues currently in scope
+    /// (echo-types residue tracking). A `reversible` block pushes a residue
+    /// (its reversal log); a `reverse` block consumes one; an `irreversible`
+    /// block pushes nothing (the residue is discarded). A `reverse` with an
+    /// empty stack is a ReverseWithoutResidue error — this enforces spec
+    /// §11.3 ("reverse of an irreversible block is a compile-time error").
+    echo_residues: Vec<Type>,
 }
 
 impl TypeEnv {
@@ -508,9 +536,28 @@ impl TypeEnv {
             warnings: Vec::new(),
             constants: HashMap::new(),
             nonzero_witnesses: HashSet::new(),
+            echo_residues: Vec::new(),
         }
     }
 
+    // -- Echo residue management (L10 reversibility, echo-types) --
+
+    /// A `reversible` block retains a reversal log — model it as pushing an
+    /// `Echo<T>` residue onto the scope. `inner` is the type the block's
+    /// reversal restores (Unit for now; the phased "linear undo-capability"
+    /// rung refines this to a consumed-exactly-once residue value).
+    fn push_echo_residue(&mut self, inner: Type) {
+        self.echo_residues.push(Type::Echo(Box::new(inner)));
+    }
+
+    /// A `reverse` block consumes the most recent Echo residue, if any.
+    /// Returns `None` when no residue is in scope — i.e. the `reverse`
+    /// targets an `irreversible` block (or has no preceding `reversible`
+    /// block), which is the ReverseWithoutResidue error.
+    fn take_echo_residue(&mut self) -> Option<Type> {
+        self.echo_residues.pop()
+    }
+
     // -- Scope management --
 
     /// Push a new scope onto the scope stack.
@@ -1722,9 +1769,15 @@ fn check_function_decl(fd: &FunctionDecl, env: &mut TypeEnv) {
         .map(|s| resolve_type_str(s, env))
         .unwrap_or(Type::Unit);
 
+    // Echo residues (L10) are scoped to this function body: a `reversible`
+    // here must not leak its reversal log to a `reverse` in another
+    // function. Cross-body (e.g. cross-handler) reversal is agent state,
+    // handled by the forthcoming linear-residue rung.
+    let saved_residues = std::mem::take(&mut env.echo_residues);
     for stmt in &fd.body {
         check_stmt(stmt, &ret_type, env);
     }
+    env.echo_residues = saved_residues;
 
     env.pop_scope();
     env.current_purity = old_purity;
@@ -1761,9 +1814,15 @@ fn check_agent_decl(ad: &AgentDecl, env: &mut TypeEnv) {
             let ty = resolve_type_str(ty_str, env);
             env.bind(name.clone(), ty, LinearStatus::Unrestricted);
         }
+        // Echo residues (L10) are scoped per handler body. Cross-handler
+        // reversal (a `reverse` in one handler replaying a `reversible` in
+        // another) is agent state, not a statically-scoped block residue —
+        // deferred to the linear-residue rung.
+        let saved_residues = std::mem::take(&mut env.echo_residues);
         for stmt in &handler.body {
             check_stmt(stmt, &Type::Unit, env);
         }
+        env.echo_residues = saved_residues;
         env.pop_scope();
     }
 
@@ -3294,7 +3353,51 @@ fn check_stmt(stmt: &ControlStmt, expected_ret: &Type, env: &mut TypeEnv) {
             // return without expression: must expect Unit.
         }
 
-        ControlStmt::Reversible(body) | ControlStmt::Irreversible(body) | ControlStmt::Reverse(body) => {
+        // L10 reversibility (echo-types residue tracking). The three blocks
+        // are no longer checked identically: `reversible` retains an Echo
+        // residue (its reversal log), `irreversible` discards it, and
+        // `reverse` is well-typed only if a residue is in scope to replay.
+        // This enforces spec/OPERATIONAL-SEMANTICS.adoc §11.3 and is
+        // mechanised in proofs/idris2/EchoResidue.idr.
+        ControlStmt::Reversible(body) => {
+            env.push_scope();
+            for s in body {
+                check_stmt(s, expected_ret, env);
+            }
+            env.pop_scope();
+            // The block's operations each have an inverse → an Echo residue
+            // becomes available to a later `reverse`.
+            env.push_echo_residue(Type::Unit);
+        }
+
+        ControlStmt::Irreversible(body) => {
+            env.push_scope();
+            for s in body {
+                check_stmt(s, expected_ret, env);
+            }
+            env.pop_scope();
+            // The residue is discarded: nothing is pushed, so a subsequent
+            // `reverse` targeting this block is ill-typed (§11.3).
+        }
+
+        ControlStmt::Reverse(body) => {
+            // A `reverse` replays a reversal log — well-typed only if an Echo
+            // residue is in scope (echo-types: reversal needs the echo).
+            if env.take_echo_residue().is_none() {
+                env.error(
+                    TypeErrorKind::ReverseWithoutResidue {
+                        detail: "`reverse` has no Echo residue in scope: it \
+                                 targets an `irreversible` block, or there is \
+                                 no preceding `reversible` block whose reversal \
+                                 log it can replay"
+                            .to_string(),
+                    },
+                    "cannot `reverse`: no Echo residue to replay — reversing an \
+                     irreversible (or absent) block is a compile-time error \
+                     (spec §11.3)"
+                        .to_string(),
+                );
+            }
             env.push_scope();
             for s in body {
                 check_stmt(s, expected_ret, env);
@@ -4276,6 +4379,7 @@ fn collect_warnings_for_type(ty: &Type, warnings: &mut Vec<TypeWarning>, errors:
         }
         // Recurse into composite types.
         Type::Linear(inner) => collect_warnings_for_type(inner, warnings, errors),
+        Type::Echo(inner) => collect_warnings_for_type(inner, warnings, errors),
         Type::List(inner) => collect_warnings_for_type(inner, warnings, errors),
         Type::Tuple(ts) => {
             for t in ts {
diff --git a/crates/oo7-core/src/typechecker_tests.rs b/crates/oo7-core/src/typechecker_tests.rs
index e4674db..602dca4 100644
--- a/crates/oo7-core/src/typechecker_tests.rs
+++ b/crates/oo7-core/src/typechecker_tests.rs
@@ -1670,3 +1670,103 @@ fn l4_proof_dispatch_generates_nonzero_idris2() {
     assert!(source.contains("%default total"));
 }
 
+// ============================================================
+// L10: Reversibility — Echo residue tracking (echo-types)
+// ============================================================
+//
+// echo-types' keystone `A ≃ Σ B (Echo f)` says a step is reversible only
+// when its echo residue is retained. The checker tracks an Echo residue
+// per body: `reversible` leaves one, `irreversible` discards it, and
+// `reverse` consumes one — a `reverse` with no residue is the
+// ReverseWithoutResidue error (spec/OPERATIONAL-SEMANTICS.adoc §11.3).
+// The rule and its soundness are mechanised in
+// proofs/idris2/EchoResidue.idr (reverseAfterIrreversibleIllTyped).
+
+fn has_reverse_without_residue(errs: &[crate::typechecker::TypeError]) -> bool {
+    errs.iter().any(|e| {
+        matches!(
+            &e.kind,
+            crate::typechecker::TypeErrorKind::ReverseWithoutResidue { .. }
+        )
+    })
+}
+
+#[test]
+fn l10_reverse_without_reversible_is_error() {
+    // A `reverse` with no preceding `reversible` block has no Echo residue.
+    let src = r#"@impure fn f() {
+        reverse {
+            let x = 1
+        }
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected reverse-without-residue error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "expected ReverseWithoutResidue, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn l10_reverse_of_irreversible_is_error() {
+    // An `irreversible` block discards its residue, so a following `reverse`
+    // targets nothing — spec §11.3 compile-time error.
+    let src = r#"@impure fn f() {
+        irreversible {
+            let x = 1
+        }
+        reverse {
+            let y = 2
+        }
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected reverse-of-irreversible error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "expected ReverseWithoutResidue, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn l10_reverse_after_reversible_ok() {
+    // A `reversible` block leaves a residue that the following `reverse`
+    // consumes — the reversibility rule is satisfied (no residue error).
+    let src = r#"@impure fn f() {
+        reversible {
+            let x = 1
+        }
+        reverse {
+            let y = 2
+        }
+    }"#;
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_reverse_without_residue(&errs),
+            "reverse after reversible must NOT raise ReverseWithoutResidue, got: {:?}",
+            errs
+        );
+    }
+}
+
+#[test]
+fn l10_residue_does_not_leak_across_functions() {
+    // A `reversible` in one function must not license a `reverse` in
+    // another — residues are scoped per body (soundness).
+    let src = r#"@impure fn a() {
+        reversible {
+            let x = 1
+        }
+    }
+    @impure fn b() {
+        reverse {
+            let y = 2
+        }
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected cross-function reverse to be an error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "residue must not leak across functions; expected ReverseWithoutResidue, got: {:?}",
+        errs
+    );
+}
+
diff --git a/docs/echo-residue-integration.adoc b/docs/echo-residue-integration.adoc
new file mode 100644
index 0000000..f65a0e7
--- /dev/null
+++ b/docs/echo-residue-integration.adoc
@@ -0,0 +1,120 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+= Echo Residue: integrating echo-types into 007's type system
+:toc: macro
+:icons: font
+
+toc::[]
+
+== Summary
+
+007 has three reversibility blocks — `reversible`, `irreversible`,
+`reverse` (OPERATIONAL-SEMANTICS §11). The specification already requires
+that "a `reverse` targeting an irreversible block is a compile-time error"
+(§11.3), but the type checker historically checked all three blocks
+*identically*, so the rule was unenforced.
+
+This work makes reversibility a checked feature of the type system by
+importing the *Echo residue* from echo-types
+(https://github.com/hyperpolymath/echo-types). It is **Layer 10** of the
+Kategoria stack (TYPE-SYSTEM-SPEC §"Layer 10").
+
+== Why echo-types is the right theory
+
+echo-types studies the fibre of a map as *structured loss*:
+
+[source]
+----
+Echo f y  :=  Σ (x : A) , (f x ≡ y)        -- the residue / fibre of f at y
+A         ≃   Σ (y : B) , Echo f y          -- keystone (EchoTotalCompletion)
+----
+
+The keystone says an irreversible `f : A → B` becomes *reversible* exactly
+when its echo residue travels with the output. That is precisely the
+reversal log of OPERATIONAL-SEMANTICS §11.1: **the reversal log IS the echo
+residue.** So reversibility is sound iff the residue is retained — which is
+the typing discipline below.
+
+== What landed (phase 1 — scoped enforcement)
+
+Mechanised and verified this session:
+
+[cols="1,3",options="header"]
+|===
+| Artefact | What
+
+| `proofs/idris2/EchoResidue.idr`
+| Idris2 port of the keystone (`encode`/`decode`,
+  `decodeEncode`/`encodeDecode` = `A ≃ Σ B (Echo f)`), type-safe reversal
+  (`reverseWithEcho`), the no-section result for a collapsing map
+  (`collapseHasNoSection`), and the typing-rule property
+  `reverseAfterIrreversibleIllTyped` (`ReverseOk Irrev` is uninhabited).
+  `%default total`, zero `believe_me`. `idris2 --check` clean.
+
+| `crates/oo7-core/src/typechecker.rs`
+| `Type::Echo(Box<Type>)` residue type; a per-body residue stack on
+  `TypeEnv`; `TypeErrorKind::ReverseWithoutResidue`; the split typing rule
+  for `reversible` / `irreversible` / `reverse`; per-function and
+  per-handler residue isolation (no cross-body leak).
+
+| `crates/oo7-core/src/agent_api.rs`
+| `ReverseWithoutResidue` → agent-facing `L10_REVERSE_WITHOUT_RESIDUE` with
+  remediations `mark_reversible` and `retain_echo`.
+
+| `crates/oo7-core/src/typechecker_tests.rs`
+| Four tests: reverse-without-reversible errs; reverse-of-irreversible
+  errs; reverse-after-reversible ok; residue does not leak across
+  functions. (Full `oo7-core` lib suite: 880 passing.)
+
+| `spec/TYPE-SYSTEM-SPEC.adoc`, `spec/OPERATIONAL-SEMANTICS.adoc`
+| Layer 10 typing rules (T-Reversible / T-Irreversible / T-Reverse /
+  T-Reverse-Err) and the §11.4 Echo-residue note.
+|===
+
+=== The typing rule
+
+A residue context `Ρ` is threaded per body. `reversible` pushes an
+`Echo<Unit>`; `irreversible` pushes nothing; `reverse` pops one, or errors
+if `Ρ` is empty. This is exactly the §11.3 compile-time error, now
+enforced and proof-backed.
+
+== Known limitation → the next rung (phase 2 — linear undo-capability)
+
+Phase 1 scopes residues *per body*. But `examples/reversibility.007`
+performs `reversible` in an `on receive` handler and `reverse` in a
+separate `on error` handler — **cross-handler** reversal. That residue is
+agent *state*, not a block-local value, so the static per-body rule cannot
+(soundly) validate it and conservatively rejects it.
+
+This is the motivating case for the planned refinement: model the residue
+as a first-class **linear** value.
+
+[cols="1,3",options="header"]
+|===
+| Aspect | Phase 2 design
+
+| Type | `Linear<Echo<T>>` — reuse 007's existing linear-handle machinery
+  (`Type::Linear`), so the residue is consumed *exactly once*.
+| `reversible` | yields a residue value bound in scope (or agent state).
+| `reverse h` | takes the residue handle `h`, consuming it; double-reverse
+  is a `LinearUsedTwice`, un-reversed residue is a `LinearNotConsumed`.
+| Cross-handler | the residue is stored in agent state between handler
+  invocations; a `reverse` in `on error` consumes the residue produced by
+  the `reversible` in `on receive` — statically tracked, because it is now
+  a value with a linear type.
+| Proof | extend `EchoResidue.idr` with the linear discipline; echo-types
+  already carries the linear strand (`EchoLinear.agda`), so the bridge is
+  to that module.
+|===
+
+The elegance: **echo residue = linear undo-capability** unifies
+echo-types' linear strand with 007's linear handles, and matches agent
+ergonomics (agents already reason in linear handles).
+
+== Cross-repo bridge (echo-types)
+
+`Type::Echo<T>` corresponds to echo-types' `Echo f y`, and 007's CNO layer
+(`proofs/agda/CNO.agda`) already bridges to `echo-types/EchoCNOBridge`. A
+direct Agda bridge from the 007 reversibility model to echo-types'
+`EchoTotalCompletion` / `EchoLinear` is the natural place to discharge the
+phase-2 proof obligations against the upstream library of record.
diff --git a/proofs/idris2/EchoResidue.idr b/proofs/idris2/EchoResidue.idr
new file mode 100644
index 0000000..87b7ea9
--- /dev/null
+++ b/proofs/idris2/EchoResidue.idr
@@ -0,0 +1,198 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+--
+-- Echo Residue — the type-system feature that makes 007's reversibility
+-- fragment sound.
+--
+-- BACKGROUND.
+--   007 has three reversibility constructs (spec/OPERATIONAL-SEMANTICS.adoc
+--   §11): `reversible { s }` (each op has an inverse, producing a reversal
+--   log), `reverse { s }` (replays that log backwards), and
+--   `irreversible { s }` (the log is discarded). The spec states in §11.3
+--   that "a `reverse` targeting an irreversible block is a compile-time
+--   error" — but until the Echo-residue integration the type checker did
+--   not enforce it (all three blocks were checked identically).
+--
+--   The principled reason WHY reversal needs the log is the echo-types
+--   result (hyperpolymath/echo-types, `Echo.agda` /
+--   `EchoTotalCompletion.agda`):
+--
+--       Echo f y := Sigma (x : A) , (f x = y)        -- the fibre / residue
+--       A  ~=  Sigma (y : B) , Echo f y              -- keystone (totality)
+--
+--   i.e. an irreversible map `f : A -> B` becomes *reversible* exactly when
+--   you carry its echo residue. `reversible` keeps the residue (the
+--   reversal log IS the echo); `irreversible` throws it away; so `reverse`
+--   is well-typed iff a residue is in scope. This module ports that result
+--   to Idris2 and pins the typing-rule property the Rust checker now
+--   enforces (see crates/oo7-core/src/typechecker.rs, Type::Echo and
+--   ControlStmt::Reverse).
+--
+-- This file carries ZERO `believe_me` / `assert_total` / `idris_crash`.
+
+module EchoResidue
+
+%default total
+
+-- ============================================================
+-- The Echo residue (the fibre of f over y)
+-- ============================================================
+
+||| `Echo f y` is the residue of the map `f` at the output `y`: an input
+||| `witness` together with a `proof` that `f witness = y`. This is the
+||| fibre of `f` over `y` — echo-types' `Echo f y := Sigma (x : A), f x = y`.
+public export
+data Echo : (f : a -> b) -> b -> Type where
+  ||| `MkEcho x prf` records the input `x` and a proof `prf : f x = y`
+  ||| that it lands on the indexed output `y`.
+  MkEcho : (x : a) -> (prf : f x = y) -> Echo f y
+
+||| Introduction: every input lands in its own fibre.
+public export
+echoIntro : {0 a, b : Type} -> (f : a -> b) -> (x : a) -> Echo f (f x)
+echoIntro f x = MkEcho x Refl
+
+||| The residue always witnesses the output it is indexed by.
+public export
+echoHits : {0 a, b : Type} -> (f : a -> b) -> (y : b) -> Echo f y -> (x : a ** f x = y)
+echoHits f y (MkEcho x prf) = (x ** prf)
+
+||| Extract the recorded input from a residue (single-level match so it
+||| reduces cleanly inside the round-trip proofs below).
+public export
+echoWitness : {0 a, b : Type} -> {0 f : a -> b} -> {0 y : b} -> Echo f y -> a
+echoWitness (MkEcho x _) = x
+
+-- ============================================================
+-- Total completion: A ~= Sigma B (Echo f)  (the keystone)
+-- ============================================================
+
+||| The total echo space of `f`: an output paired with a residue proving
+||| that output is actually hit. (Documentation alias; the round-trip
+||| signatures inline the dependent pair so the pattern matcher sees it
+||| directly.)
+public export
+TotalEcho : {b : Type} -> (f : a -> b) -> Type
+TotalEcho f = (y : b ** Echo f y)
+
+||| `encode` is the "make it reversible" direction: an input determines a
+||| point in the total echo space (its image, paired with itself as the
+||| residue witness).
+public export
+encode : {0 a, b : Type} -> (f : a -> b) -> a -> (y : b ** Echo f y)
+encode f x = (f x ** MkEcho x Refl)
+
+||| `decode` projects the original input back out of the carried residue.
+public export
+decode : {0 a, b : Type} -> (f : a -> b) -> (y : b ** Echo f y) -> a
+decode f (_ ** e) = echoWitness e
+
+||| ROUND-TRIP 1 — `decode . encode = id`. No information is lost when the
+||| echo is kept: this is the soundness of reversal-with-residue.
+public export
+decodeEncode : {0 a, b : Type} -> (f : a -> b) -> (x : a) ->
+               decode f (encode f x) = x
+decodeEncode f x = Refl
+
+||| ROUND-TRIP 2 — `encode . decode = id`. The total echo space faithfully
+||| represents the domain. With round-trip 1 this is the keystone
+||| equivalence `A ~= Sigma B (Echo f)` (echo-types `EchoTotalCompletion`).
+public export
+encodeDecode : {0 a, b : Type} -> (f : a -> b) ->
+               (t : (y : b ** Echo f y)) -> encode f (decode f t) = t
+encodeDecode f (y ** MkEcho x prf) = case prf of Refl => Refl
+
+-- ============================================================
+-- Type-safe reversal consumes the residue
+-- ============================================================
+
+||| `reverseWithEcho` is the well-typed reversal of an (otherwise
+||| irreversible) step: it recovers an input by *consuming* the echo
+||| residue. This is what `reverse { ... }` does to the reversal log.
+public export
+reverseWithEcho : {0 a, b : Type} -> (f : a -> b) -> (y : b) -> Echo f y -> a
+reverseWithEcho f y (MkEcho x _) = x
+
+||| Reversal is correct: the recovered input maps back to the same output.
+public export
+reverseWithEchoCorrect : {0 a, b : Type} -> (f : a -> b) -> (y : b) ->
+                         (e : Echo f y) -> f (reverseWithEcho f y e) = y
+reverseWithEchoCorrect f y (MkEcho x prf) = prf
+
+-- ============================================================
+-- Without the residue, a collapsing (irreversible) step has no inverse
+-- ============================================================
+
+||| A concrete collapsing map: `collapse` sends every Nat to the single
+||| unit value, discarding its input — the prototypical irreversible step.
+public export
+collapse : Nat -> Unit
+collapse _ = ()
+
+||| NO SECTION: there is no `g : Unit -> Nat` recovering the input of
+||| `collapse` from its output alone, because that would force the two
+||| distinct inputs `0` and `1` to be equal. This is echo-types'
+||| `no-section-of-collapsing-map` — the formal content of "reversing an
+||| irreversible block without its echo is impossible".
+public export
+collapseHasNoSection : (g : Unit -> Nat) -> Not ((x : Nat) -> g (collapse x) = x)
+collapseHasNoSection g sect = zeroNotOne (trans (sym (sect 0)) (sect 1))
+  where
+    zeroNotOne : the Nat 0 = the Nat 1 -> Void
+    zeroNotOne Refl impossible
+
+-- ============================================================
+-- The typing rule the checker enforces
+-- ============================================================
+
+||| The reversibility mode of a block, as the type checker sees it.
+public export
+data Reversibility : Type where
+  ||| `reversible { ... }` — the reversal log (echo residue) is retained.
+  Rev   : Reversibility
+  ||| `irreversible { ... }` — the residue is discarded.
+  Irrev : Reversibility
+
+||| Does a block of the given mode leave an echo residue in scope?
+public export
+leavesEcho : Reversibility -> Bool
+leavesEcho Rev   = True
+leavesEcho Irrev = False
+
+||| Well-typedness of `reverse` against a preceding block's mode. The
+||| only inhabitant is `RevOK` (residue present after `reversible`); there
+||| is deliberately NO constructor producing `ReverseOk Irrev`.
+public export
+data ReverseOk : Reversibility -> Type where
+  RevOK : ReverseOk Rev
+
+||| KEY TYPING PROPERTY — reversing an irreversible block is ill-typed:
+||| `ReverseOk Irrev` is uninhabited. This is precisely the static error
+||| the Rust checker now raises (TypeErrorKind::ReverseWithoutResidue),
+||| and it discharges spec §11.3's compile-time-error requirement.
+public export
+reverseAfterIrreversibleIllTyped : Not (ReverseOk Irrev)
+reverseAfterIrreversibleIllTyped RevOK impossible
+
+||| Conversely, reversing a reversible block is always well-typed.
+public export
+reverseAfterReversibleOk : ReverseOk Rev
+reverseAfterReversibleOk = RevOK
+
+||| And well-typed `reverse` happens exactly when the block left a residue.
+public export
+reverseOkIffLeavesEcho : (m : Reversibility) -> ReverseOk m -> leavesEcho m = True
+reverseOkIffLeavesEcho Rev RevOK = Refl
+
+-- ============================================================
+-- Summary (zero believe_me, zero sorry, %default total)
+-- ============================================================
+--
+-- echoIntro / echoHits          : the residue type and its intro
+-- encode / decode               : the totality maps
+-- decodeEncode / encodeDecode   : A ~= Sigma B (Echo f)  (keystone round-trips)
+-- reverseWithEcho(+Correct)     : type-safe reversal consumes the residue
+-- collapseHasNoSection          : no inverse without the echo (no-section)
+-- reverseAfterIrreversibleIllTyped : reverse-after-irreversible is a
+--                                    compile-time error (spec §11.3)
+-- reverseOkIffLeavesEcho        : reverse OK <=> a residue was retained
diff --git a/spec/OPERATIONAL-SEMANTICS.adoc b/spec/OPERATIONAL-SEMANTICS.adoc
index 78c9d69..416df8f 100644
--- a/spec/OPERATIONAL-SEMANTICS.adoc
+++ b/spec/OPERATIONAL-SEMANTICS.adoc
@@ -732,6 +732,33 @@ Each operation within a `reversible` block has an inverse:
     (* A `reverse` targeting this block is a compile-time error *)
 ```
 
+=== 11.4 Echo Residue (static enforcement of the reversal log)
+
+The reversal log `R` of §11.1 is, type-theoretically, an *Echo residue*.
+For an irreversible map `f : A → B` the residue is its fibre,
+`Echo f y := Σ (x : A), f x = y`, and the keystone of echo-types
+(hyperpolymath/echo-types) is
+
+```
+    A  ≃  Σ (y : B) , Echo f y          (* irreversible + echo = reversible *)
+```
+
+i.e. a step can be undone exactly when its echo residue is retained. This
+grounds the §11.3 compile-time error: a `reverse` is well-typed only when
+an Echo residue is in scope. The type checker (Layer 10, TYPE-SYSTEM-SPEC
+§"Layer 10") tracks one residue per body — `reversible` leaves a residue,
+`irreversible` discards it, `reverse` consumes one — and rejects a
+`reverse` with no residue (`ReverseWithoutResidue`). The rule and the
+keystone are mechanised in `proofs/idris2/EchoResidue.idr`
+(`reverseAfterIrreversibleIllTyped`, `encodeDecode`).
+
+NOTE: cross-handler reversal — a `reverse` in one handler replaying a
+`reversible` in another — is *agent state*, not a statically block-scoped
+residue, so the Layer-10 rule (scoped per body) does not yet validate it.
+That case is the motivation for the next rung, in which the residue is a
+first-class linear value threaded through agent state (see
+`docs/echo-residue-integration.adoc`).
+
 == 12. Choreography Projection Semantics
 
 === 12.1 Projection Function
diff --git a/spec/TYPE-SYSTEM-SPEC.adoc b/spec/TYPE-SYSTEM-SPEC.adoc
index 4c08aee..5a95fa8 100644
--- a/spec/TYPE-SYSTEM-SPEC.adoc
+++ b/spec/TYPE-SYSTEM-SPEC.adoc
@@ -660,6 +660,78 @@ linear let worker = spawn Agent(
 -- because these proofs are part of the hash
 ```
 
+== 11b. Layer 10: Reversibility (Echo Residue)
+
+Agent actions split into reversible and irreversible (OPERATIONAL-SEMANTICS
+§11). Layer 10 makes that split *type-checked*, grounded in echo-types
+(hyperpolymath/echo-types).
+
+=== 11b.1 The Echo residue type
+
+For a map `f : A -> B`, its *Echo residue* at an output `y` is the fibre
+
+```
+    Echo f y  :=  (x : A ** f x = y)        -- echo-types: Σ(x:A), f x = y
+```
+
+— the inputs that produce `y`, each with the proof that it does. In the
+checker this is the type `Echo<T>` (`Type::Echo`). The keystone of
+echo-types,
+
+```
+    A  ≅  (y : B ** Echo f y)               -- encode / decode round-trip
+```
+
+says an otherwise-irreversible `f` becomes reversible precisely when its
+echo residue is carried alongside the output. The residue *is* the
+reversal log of OPERATIONAL-SEMANTICS §11.1.
+
+=== 11b.2 Typing rules
+
+A residue context `Ρ` (a stack of in-scope Echo residues) is threaded
+through a body. The three reversibility blocks are no longer
+interchangeable:
+
+```
+    Ρ ⊢ s ok                         Ρ ⊢ s ok
+    ----------------- (T-Reversible)  ------------------ (T-Irreversible)
+    Ρ ⊢ reversible {s} ⊣ Ρ, Echo<Unit>   Ρ ⊢ irreversible {s} ⊣ Ρ
+
+    Ρ = Ρ', Echo<T>     Ρ' ⊢ s ok            Ρ has no residue
+    ------------------------------ (T-Reverse)  ------------------- (T-Reverse-Err)
+    Ρ ⊢ reverse {s} ⊣ Ρ'                      Ρ ⊢ reverse {s} : ERROR
+```
+
+`reversible` pushes a residue; `irreversible` pushes none (it discards the
+log); `reverse` consumes one. A `reverse` with an empty residue context is
+`ReverseWithoutResidue` — this is the compile-time error required by
+OPERATIONAL-SEMANTICS §11.3. Residues are scoped per body (a `reversible`
+in one function/handler does not license a `reverse` in another).
+
+The rules and the keystone equivalence are mechanised in
+`proofs/idris2/EchoResidue.idr` (`encodeDecode`, `decodeEncode`,
+`reverseAfterIrreversibleIllTyped`, `collapseHasNoSection`).
+
+=== 11b.3 Agent ergonomics
+
+Because 007 is written for agents, the residue is surfaced — not hidden.
+`ReverseWithoutResidue` is translated (agent_api) into the agent-facing
+code `L10_REVERSE_WITHOUT_RESIDUE` with two remediations (`mark_reversible`,
+`retain_echo`), so an agent that over-reaches for `reverse` is told exactly
+how to retain the echo it needs. Hermeneutically, the Echo residue is the
+type-level shadow of the `trace` an irreversible step discards: it names
+*what was lost*, which is precisely what an agent must weigh when deciding
+whether an action can be taken back.
+
+=== 11b.4 Next rung (linear undo-capability)
+
+Layer 10 as specified enforces reversal *within* a body. The planned
+refinement makes the residue a first-class **linear** value
+(`Linear<Echo<T>>`) — produced by `reversible`, consumed exactly once by
+`reverse`, threadable through agent state — which both reuses 007's linear
+handles and lets a `reverse` in one handler legitimately replay a
+`reversible` in another. See `docs/echo-residue-integration.adoc`.
+
 == 12. The Layers in Concert
 
 A single branch point in 007 exercises multiple layers simultaneously:

From db17a5ff3a3ef43768e9a855bf49ab6ac84dc56f Mon Sep 17 00:00:00 2001
From: Claude <paraordinate@yahoo.co.uk>
Date: Wed, 3 Jun 2026 21:40:05 +0000
Subject: [PATCH 2/4] fix(ci): resolve pre-existing CI gate failures at root
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Repo-wide CI breakage (red on every build, unrelated to but blocking PR #34):

- hypatia dep: ssh:// -> https:// + refresh the stale pinned rev in
  Cargo.lock (-> 79c7036). cargo could not authenticate to the SSH source,
  failing `cargo check` / test / E2E / hypatia at dependency resolution
  before any code compiled. https resolves anonymously; the dep stays
  feature-gated (hypatia-typed, non-default) so it is resolved, not built.
- eclexiaiser.toml: resolve a committed git merge-conflict (invalid TOML;
  kept the canonical project name "007-lang").
- grammar-guard (ci.yml): fix a false positive — anchor the Harvard
  invariant on data_ rule *definitions*, not any line co-mentioning
  data_ and a control construct. `agent_member = { data_block |
  control_block | state_decl }` is a legitimate union, not a violation.
- A2ML manifests (40 errors -> 0): add the required identity field to 35
  auto-generated proof sidecars and fix the runner template so future
  sidecars are born valid; add identity to 5 real manifests.
- K9 contracts (7 errors -> 0): add the `K9!` magic line + pedigree /
  signature fields to 4 .k9.ncl guard/contractile files.
- stapeln.toml: fix a malformed entrypoint array (invalid TOML).

Verified locally with the upstream validator actions
(a2ml-validate-action, k9-validate-action), `cargo check --all-targets`,
and tomllib. gitleaks (org GITLEAKS_LICENSE) and CodeQL-actions (GHAS)
failures are CI-infra, not repo content; flagged separately.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
---
 .github/workflows/ci.yml                           | 14 +++++++++++---
 .../contractiles/adjust/adjust.k9.ncl              |  1 +
 .../contractiles/intend/intend.k9.ncl              |  2 ++
 .machine_readable/svc/k9/harvard-guard.k9.ncl      |  8 ++++++++
 .machine_readable/svc/k9/methodology-guard.k9.ncl  |  8 ++++++++
 Cargo.lock                                         |  2 +-
 audits/axiom-triage.a2ml                           |  1 +
 cartridges/007-mcp/schemas/memory-tag-map.a2ml     |  1 +
 crates/oo7-core/Cargo.toml                         |  2 +-
 .../src/observability/debugger/FOLLOWUPS.a2ml      |  1 +
 daemon/src/manifest.a2ml                           |  1 +
 eclexiaiser.toml                                   |  7 -------
 oo7-control-plane/src/manifest.a2ml                |  1 +
 proofs/canonical-proof-suite/E1.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E10.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/E11.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/E2.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E3.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E4.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E5.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E6.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E7.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E8.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/E9.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M1.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M10.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/M11.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/M12.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/M13.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/M14.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/M2.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M3.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M4.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M5.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M6.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M7.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M8.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/M9.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S1.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S10.sidecar.a2ml      |  1 +
 proofs/canonical-proof-suite/S2.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S3.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S4.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S5.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S6.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S7.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S8.sidecar.a2ml       |  1 +
 proofs/canonical-proof-suite/S9.sidecar.a2ml       |  1 +
 scripts/canonical-proof-suite-runner.sh            |  1 +
 stapeln.toml                                       |  2 +-
 50 files changed, 74 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 55b6f4d..8621fd1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -52,9 +52,17 @@ jobs:
 
       - name: Harvard invariant check
         run: |
-          # Verify data_expr rules don't reference control constructs
-          if grep -n 'control_stmt\|control_expr\|control_block' crates/oo7-core/src/grammar.pest | grep -i 'data_'; then
-            echo "::error::HARVARD VIOLATION: data rules reference control constructs"
+          # Harvard invariant: a data-expression rule must not reference any
+          # control construct. We check the *definitions* of data_ rules
+          # (lines that start a `data_<name> = ...` production) for references
+          # to control_stmt / control_expr / control_block. A union rule such
+          # as `agent_member = { data_block | control_block | state_decl }`
+          # legitimately mentions both and is NOT a violation, so we anchor on
+          # the data_ rule head rather than flagging any line co-mentioning the
+          # two (which produced a false positive on agent_member).
+          if grep -nE '^[[:space:]]*data_[A-Za-z0-9_]+[[:space:]]*=' crates/oo7-core/src/grammar.pest \
+             | grep -E 'control_stmt|control_expr|control_block'; then
+            echo "::error::HARVARD VIOLATION: a data_ rule references control constructs"
             exit 1
           fi
           echo "Harvard invariant: OK"
diff --git a/.machine_readable/contractiles/adjust/adjust.k9.ncl b/.machine_readable/contractiles/adjust/adjust.k9.ncl
index 9ff26c9..513a6e3 100644
--- a/.machine_readable/contractiles/adjust/adjust.k9.ncl
+++ b/.machine_readable/contractiles/adjust/adjust.k9.ncl
@@ -1,3 +1,4 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # adjust.k9.ncl — K9 trust-tier component of the adjust trident
 # Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl
index 5b0c295..1a594a1 100644
--- a/.machine_readable/contractiles/intend/intend.k9.ncl
+++ b/.machine_readable/contractiles/intend/intend.k9.ncl
@@ -1,3 +1,4 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # intend.k9.ncl — K9 trust-tier component of the intend trident
 # Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
@@ -59,6 +60,7 @@ let base    = import "../_base.ncl" in
 
     security = {
       leash = 'Hunt,
+      signature_required = true,
       trust_level = "subprocess + filesystem-read",
       allow_network = false,
       allow_filesystem_write = false,   # evidence sinks are indirected
diff --git a/.machine_readable/svc/k9/harvard-guard.k9.ncl b/.machine_readable/svc/k9/harvard-guard.k9.ncl
index f542d9f..1ea15a4 100644
--- a/.machine_readable/svc/k9/harvard-guard.k9.ncl
+++ b/.machine_readable/svc/k9/harvard-guard.k9.ncl
@@ -1,3 +1,4 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
@@ -10,6 +11,13 @@
 let harvard_guard = {
   name = "harvard-guard",
   version = "1.0.0",
+  pedigree = {
+    name = "harvard-guard",
+    schema_version = "1.0.0",
+    security = {
+      leash = 'Yard,
+    },
+  },
   description = "Validates Harvard architecture separation in 007-lang parser",
 
   checks = {
diff --git a/.machine_readable/svc/k9/methodology-guard.k9.ncl b/.machine_readable/svc/k9/methodology-guard.k9.ncl
index b5f7e25..b732616 100644
--- a/.machine_readable/svc/k9/methodology-guard.k9.ncl
+++ b/.machine_readable/svc/k9/methodology-guard.k9.ncl
@@ -1,3 +1,4 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
@@ -10,6 +11,13 @@
 let methodology_guard = {
   name = "methodology-guard",
   version = "1.0.0",
+  pedigree = {
+    name = "methodology-guard",
+    schema_version = "1.0.0",
+    security = {
+      leash = 'Yard,
+    },
+  },
   description = "Validates that agent work respects declared methodology constraints for 007-lang",
 
   checks = {
diff --git a/Cargo.lock b/Cargo.lock
index 6c1b35a..ac86a25 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -887,7 +887,7 @@ checksum = "135b12329e5e3ce057a9f972339ea52bc954fe1e9358ef27f95e89716fbc5424"
 [[package]]
 name = "hypatia-client"
 version = "0.1.0"
-source = "git+ssh://git@github.com/hyperpolymath/hypatia.git?branch=main#210b92adeba44d2e6a6a3ede515b7791857def9d"
+source = "git+https://github.com/hyperpolymath/hypatia.git?branch=main#79c7036600c003100adbe8d1177c3fd1aa4aee8c"
 dependencies = [
  "libloading 0.9.0",
  "serde",
diff --git a/audits/axiom-triage.a2ml b/audits/axiom-triage.a2ml
index 69eb687..365e804 100644
--- a/audits/axiom-triage.a2ml
+++ b/audits/axiom-triage.a2ml
@@ -35,6 +35,7 @@
 ;   shortcut.  Zero v1.0 violations.
 
 (axiom-triage
+  (project "007-lang")
   (generated "2026-04-27")
   (standard "v1.1-closure-permitted")
   (summary
diff --git a/cartridges/007-mcp/schemas/memory-tag-map.a2ml b/cartridges/007-mcp/schemas/memory-tag-map.a2ml
index 10ea354..e4afca4 100644
--- a/cartridges/007-mcp/schemas/memory-tag-map.a2ml
+++ b/cartridges/007-mcp/schemas/memory-tag-map.a2ml
@@ -24,6 +24,7 @@
 ;; The adapter resolves those against $HOME at OnEnter time.
 
 (memory-tag-map
+  (project "007-lang")
   (version "0.1.0")
   (generated-for "007-lang")
   (last-reviewed "2026-04-20")
diff --git a/crates/oo7-core/Cargo.toml b/crates/oo7-core/Cargo.toml
index 9d6efbe..fafdf0c 100644
--- a/crates/oo7-core/Cargo.toml
+++ b/crates/oo7-core/Cargo.toml
@@ -47,7 +47,7 @@ libloading = { version = "0.8", optional = true }
 # path-based form. Pin via `rev = "..."` once a stable hypatia release
 # tag exists; for now branch=main is fine — the dep is only resolved
 # when the `hypatia-typed` feature is enabled.
-hypatia-client = { git = "ssh://git@github.com/hyperpolymath/hypatia.git", branch = "main", optional = true }
+hypatia-client = { git = "https://github.com/hyperpolymath/hypatia.git", branch = "main", optional = true }
 
 [features]
 default = ["backend-qbe", "backend-cranelift"]
diff --git a/crates/oo7-core/src/observability/debugger/FOLLOWUPS.a2ml b/crates/oo7-core/src/observability/debugger/FOLLOWUPS.a2ml
index 25cd63f..2f47b21 100644
--- a/crates/oo7-core/src/observability/debugger/FOLLOWUPS.a2ml
+++ b/crates/oo7-core/src/observability/debugger/FOLLOWUPS.a2ml
@@ -14,6 +14,7 @@
 ;; debugger substrate. Tickets here are NOT sign-off blockers.
 
 (followups
+  (project "007-lang")
   (version "1")
   (owner "T6 thread")
   (partner-doc "DESIGN-STEP-SEMANTICS.adoc")
diff --git a/daemon/src/manifest.a2ml b/daemon/src/manifest.a2ml
index c2ccc81..31cc974 100644
--- a/daemon/src/manifest.a2ml
+++ b/daemon/src/manifest.a2ml
@@ -2,6 +2,7 @@
 ; 007 Toolchain Groove Manifest MK2
 
 (groove-manifest
+  (project "007-lang")
   (version "2")
   (system
     (id "oo7-toolchain-mk2")
diff --git a/eclexiaiser.toml b/eclexiaiser.toml
index 0d25fd1..2475007 100644
--- a/eclexiaiser.toml
+++ b/eclexiaiser.toml
@@ -1,15 +1,8 @@
 # SPDX-License-Identifier: MPL-2.0
-<<<<<<< HEAD
 # eclexiaiser manifest for 007-lang
 
 [project]
 name = "007-lang"
-=======
-# eclexiaiser manifest for 007
-
-[project]
-name = "007"
->>>>>>> a3bda24 (chore: add eclexiaiser.toml energy-cost manifest)
 
 [[functions]]
 name = "main"
diff --git a/oo7-control-plane/src/manifest.a2ml b/oo7-control-plane/src/manifest.a2ml
index b89305e..7aff804 100644
--- a/oo7-control-plane/src/manifest.a2ml
+++ b/oo7-control-plane/src/manifest.a2ml
@@ -2,6 +2,7 @@
 ; 007 Toolchain Groove Manifest
 
 (groove-manifest
+  (project "007-lang")
   (version "1")
   (system
     (id "oo7-toolchain")
diff --git a/proofs/canonical-proof-suite/E1.sidecar.a2ml b/proofs/canonical-proof-suite/E1.sidecar.a2ml
index 657b595..db32477 100644
--- a/proofs/canonical-proof-suite/E1.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E1.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E1")
   (domain "engineering")
   (theorem "Lyapunov stability of n-dim LTI system: V_of P (traj_infty A x0 t) <= V_of P x0 for the explicit trajectory x(t) = exp(tA) x0, under positive_definite P and negative_definite (Aᵀ P + P A)")
diff --git a/proofs/canonical-proof-suite/E10.sidecar.a2ml b/proofs/canonical-proof-suite/E10.sidecar.a2ml
index e3751a1..089634c 100644
--- a/proofs/canonical-proof-suite/E10.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E10.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E10")
   (domain "engineering")
   (theorem "Weibull / bathtub-curve failure-rate bound (reliability engineering)")
diff --git a/proofs/canonical-proof-suite/E11.sidecar.a2ml b/proofs/canonical-proof-suite/E11.sidecar.a2ml
index 7954941..c8fc632 100644
--- a/proofs/canonical-proof-suite/E11.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E11.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E11")
   (domain "engineering")
   (theorem "Kirchhoff voltage + current laws for lumped-element circuits")
diff --git a/proofs/canonical-proof-suite/E2.sidecar.a2ml b/proofs/canonical-proof-suite/E2.sidecar.a2ml
index 2a6737a..36a7478 100644
--- a/proofs/canonical-proof-suite/E2.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E2.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E2")
   (domain "engineering")
   (theorem "Equivalence of two adder designs (ripple-carry vs carry-lookahead, single bit-width)")
diff --git a/proofs/canonical-proof-suite/E3.sidecar.a2ml b/proofs/canonical-proof-suite/E3.sidecar.a2ml
index 7f2ce9b..4e28730 100644
--- a/proofs/canonical-proof-suite/E3.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E3.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E3")
   (domain "engineering")
   (theorem "Bound on cantilever beam deflection (Euler-Bernoulli, single point load)")
diff --git a/proofs/canonical-proof-suite/E4.sidecar.a2ml b/proofs/canonical-proof-suite/E4.sidecar.a2ml
index 5e09dd7..6de8650 100644
--- a/proofs/canonical-proof-suite/E4.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E4.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E4")
   (domain "engineering")
   (theorem "Correctness of merge sort (output is sorted permutation of input)")
diff --git a/proofs/canonical-proof-suite/E5.sidecar.a2ml b/proofs/canonical-proof-suite/E5.sidecar.a2ml
index 515b35c..35751a8 100644
--- a/proofs/canonical-proof-suite/E5.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E5.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E5")
   (domain "engineering")
   (theorem "Needham-Schroeder fix re-scope: challenge-response key-binding under injective MAC (core cryptographic fact Lowe's fix relies on)")
diff --git a/proofs/canonical-proof-suite/E6.sidecar.a2ml b/proofs/canonical-proof-suite/E6.sidecar.a2ml
index ad55df2..fc56c67 100644
--- a/proofs/canonical-proof-suite/E6.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E6.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E6")
   (domain "engineering")
   (theorem "CSTR steady-state mass balance closure (chemical engineering)")
diff --git a/proofs/canonical-proof-suite/E7.sidecar.a2ml b/proofs/canonical-proof-suite/E7.sidecar.a2ml
index 98d629c..c8c4385 100644
--- a/proofs/canonical-proof-suite/E7.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E7.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E7")
   (domain "engineering")
   (theorem "Carnot efficiency upper bound for a heat engine between two reservoirs")
diff --git a/proofs/canonical-proof-suite/E8.sidecar.a2ml b/proofs/canonical-proof-suite/E8.sidecar.a2ml
index 26f0619..e69bd3b 100644
--- a/proofs/canonical-proof-suite/E8.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E8.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E8")
   (domain "engineering")
   (theorem "Nyquist-Shannon sampling theorem: 2W sufficient rate for bandlimited reconstruction")
diff --git a/proofs/canonical-proof-suite/E9.sidecar.a2ml b/proofs/canonical-proof-suite/E9.sidecar.a2ml
index 9439cce..40a3a5d 100644
--- a/proofs/canonical-proof-suite/E9.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/E9.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "E9")
   (domain "engineering")
   (theorem "Newton's method local quadratic convergence (numerical analysis)")
diff --git a/proofs/canonical-proof-suite/M1.sidecar.a2ml b/proofs/canonical-proof-suite/M1.sidecar.a2ml
index e0c17ef..b71cfe8 100644
--- a/proofs/canonical-proof-suite/M1.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M1.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M1")
   (domain "mathematics")
   (theorem "Infinitude of primes (Euclid)")
diff --git a/proofs/canonical-proof-suite/M10.sidecar.a2ml b/proofs/canonical-proof-suite/M10.sidecar.a2ml
index f985115..df8ae85 100644
--- a/proofs/canonical-proof-suite/M10.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M10.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M10")
   (domain "mathematics")
   (theorem "Connected sum of knots forms a commutative monoid with unknot as identity")
diff --git a/proofs/canonical-proof-suite/M11.sidecar.a2ml b/proofs/canonical-proof-suite/M11.sidecar.a2ml
index f36ad74..2bdf0e7 100644
--- a/proofs/canonical-proof-suite/M11.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M11.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M11")
   (domain "mathematics")
   (theorem "Pigeonhole principle (finite case, arbitrary surjection)")
diff --git a/proofs/canonical-proof-suite/M12.sidecar.a2ml b/proofs/canonical-proof-suite/M12.sidecar.a2ml
index ee6a7f5..e372c55 100644
--- a/proofs/canonical-proof-suite/M12.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M12.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M12")
   (domain "mathematics")
   (theorem "Dominated convergence theorem (Lebesgue integration)")
diff --git a/proofs/canonical-proof-suite/M13.sidecar.a2ml b/proofs/canonical-proof-suite/M13.sidecar.a2ml
index 5561480..94e597b 100644
--- a/proofs/canonical-proof-suite/M13.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M13.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M13")
   (domain "mathematics")
   (theorem "Hahn-Banach extension theorem (functional analysis)")
diff --git a/proofs/canonical-proof-suite/M14.sidecar.a2ml b/proofs/canonical-proof-suite/M14.sidecar.a2ml
index 97a484e..47f1c45 100644
--- a/proofs/canonical-proof-suite/M14.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M14.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M14")
   (domain "mathematics")
   (theorem "Max-flow / min-cut duality (graph theory)")
diff --git a/proofs/canonical-proof-suite/M2.sidecar.a2ml b/proofs/canonical-proof-suite/M2.sidecar.a2ml
index 8ed916a..1a586bb 100644
--- a/proofs/canonical-proof-suite/M2.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M2.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M2")
   (domain "mathematics")
   (theorem "Lagrange's theorem (group order divides)")
diff --git a/proofs/canonical-proof-suite/M3.sidecar.a2ml b/proofs/canonical-proof-suite/M3.sidecar.a2ml
index 5bbc027..371d261 100644
--- a/proofs/canonical-proof-suite/M3.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M3.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M3")
   (domain "mathematics")
   (theorem "Intermediate value theorem (continuous real-valued)")
diff --git a/proofs/canonical-proof-suite/M4.sidecar.a2ml b/proofs/canonical-proof-suite/M4.sidecar.a2ml
index 95081b1..60c465c 100644
--- a/proofs/canonical-proof-suite/M4.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M4.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M4")
   (domain "mathematics")
   (theorem "Compactness of [0,1] (Heine-Borel for closed unit interval)")
diff --git a/proofs/canonical-proof-suite/M5.sidecar.a2ml b/proofs/canonical-proof-suite/M5.sidecar.a2ml
index 1e47ffc..440b05a 100644
--- a/proofs/canonical-proof-suite/M5.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M5.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M5")
   (domain "mathematics")
   (theorem "Yoneda lemma (locally small categories)")
diff --git a/proofs/canonical-proof-suite/M6.sidecar.a2ml b/proofs/canonical-proof-suite/M6.sidecar.a2ml
index c58223e..c7276ca 100644
--- a/proofs/canonical-proof-suite/M6.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M6.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M6")
   (domain "mathematics")
   (theorem "Deduction theorem / modus ponens closure (propositional logic)")
diff --git a/proofs/canonical-proof-suite/M7.sidecar.a2ml b/proofs/canonical-proof-suite/M7.sidecar.a2ml
index 33e4f23..31845fe 100644
--- a/proofs/canonical-proof-suite/M7.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M7.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M7")
   (domain "mathematics")
   (theorem "Linearity of expectation (finite discrete random variables)")
diff --git a/proofs/canonical-proof-suite/M8.sidecar.a2ml b/proofs/canonical-proof-suite/M8.sidecar.a2ml
index a7fde0b..43663e5 100644
--- a/proofs/canonical-proof-suite/M8.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M8.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M8")
   (domain "mathematics")
   (theorem "Rank-nullity theorem for finite-dimensional linear maps")
diff --git a/proofs/canonical-proof-suite/M9.sidecar.a2ml b/proofs/canonical-proof-suite/M9.sidecar.a2ml
index d69c6a7..b649b4b 100644
--- a/proofs/canonical-proof-suite/M9.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/M9.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "M9")
   (domain "mathematics")
   (theorem "Unique factorization in a UFD (integers as base case)")
diff --git a/proofs/canonical-proof-suite/S1.sidecar.a2ml b/proofs/canonical-proof-suite/S1.sidecar.a2ml
index 3af1c8d..8bbd9a2 100644
--- a/proofs/canonical-proof-suite/S1.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S1.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S1")
   (domain "science")
   (theorem "Conservation of energy from time-translation invariance (Noether classical case)")
diff --git a/proofs/canonical-proof-suite/S10.sidecar.a2ml b/proofs/canonical-proof-suite/S10.sidecar.a2ml
index 4bd1436..dd7c540 100644
--- a/proofs/canonical-proof-suite/S10.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S10.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S10")
   (domain "science")
   (theorem "R_0 threshold for endemic-equilibrium existence (compartmental epidemiology)")
diff --git a/proofs/canonical-proof-suite/S2.sidecar.a2ml b/proofs/canonical-proof-suite/S2.sidecar.a2ml
index 926158d..c09eb06 100644
--- a/proofs/canonical-proof-suite/S2.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S2.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S2")
   (domain "science")
   (theorem "Gauss's law (Maxwell, differential form, vacuum)")
diff --git a/proofs/canonical-proof-suite/S3.sidecar.a2ml b/proofs/canonical-proof-suite/S3.sidecar.a2ml
index 0110d05..36d95af 100644
--- a/proofs/canonical-proof-suite/S3.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S3.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S3")
   (domain "science")
   (theorem "H-theorem re-scope: binary-distribution entropy proxy p*(1-p) is maximised at uniform p = 1/2 (value 1/4)")
diff --git a/proofs/canonical-proof-suite/S4.sidecar.a2ml b/proofs/canonical-proof-suite/S4.sidecar.a2ml
index c81f768..4a7211f 100644
--- a/proofs/canonical-proof-suite/S4.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S4.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S4")
   (domain "science")
   (theorem "Heisenberg uncertainty re-scope: discrete Cauchy-Schwarz on R^2 (finite-dimensional kernel of the operator-algebra derivation)")
diff --git a/proofs/canonical-proof-suite/S5.sidecar.a2ml b/proofs/canonical-proof-suite/S5.sidecar.a2ml
index 43f4c00..ab9354c 100644
--- a/proofs/canonical-proof-suite/S5.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S5.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S5")
   (domain "science")
   (theorem "Shannon source-coding (rate >= entropy is necessary)")
diff --git a/proofs/canonical-proof-suite/S6.sidecar.a2ml b/proofs/canonical-proof-suite/S6.sidecar.a2ml
index 099aae0..2781009 100644
--- a/proofs/canonical-proof-suite/S6.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S6.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S6")
   (domain "science")
   (theorem "Law of mass action: equilibrium condition for an elementary reaction")
diff --git a/proofs/canonical-proof-suite/S7.sidecar.a2ml b/proofs/canonical-proof-suite/S7.sidecar.a2ml
index 82830ba..227524a 100644
--- a/proofs/canonical-proof-suite/S7.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S7.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S7")
   (domain "science")
   (theorem "Lorentz-boost composition / relativistic velocity addition (special relativity)")
diff --git a/proofs/canonical-proof-suite/S8.sidecar.a2ml b/proofs/canonical-proof-suite/S8.sidecar.a2ml
index eb32e0a..924f34c 100644
--- a/proofs/canonical-proof-suite/S8.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S8.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S8")
   (domain "science")
   (theorem "Hardy-Weinberg equilibrium stability under random mating (population genetics)")
diff --git a/proofs/canonical-proof-suite/S9.sidecar.a2ml b/proofs/canonical-proof-suite/S9.sidecar.a2ml
index 54b57b6..b334571 100644
--- a/proofs/canonical-proof-suite/S9.sidecar.a2ml
+++ b/proofs/canonical-proof-suite/S9.sidecar.a2ml
@@ -2,6 +2,7 @@
 ;; Auto-generated by scripts/canonical-proof-suite-runner.sh
 ;; Edits to this file will be overwritten on the next runner pass.
 (canonical-proof-suite-sidecar
+  (project "007-lang")
   (id "S9")
   (domain "science")
   (theorem "Chandrasekhar mass upper bound for white-dwarf stars (astrophysics)")
diff --git a/scripts/canonical-proof-suite-runner.sh b/scripts/canonical-proof-suite-runner.sh
index 9431911..14d839b 100755
--- a/scripts/canonical-proof-suite-runner.sh
+++ b/scripts/canonical-proof-suite-runner.sh
@@ -400,6 +400,7 @@ run_one() {
     echo ";; Auto-generated by scripts/canonical-proof-suite-runner.sh"
     echo ";; Edits to this file will be overwritten on the next runner pass."
     echo "(canonical-proof-suite-sidecar"
+    echo "  (project \"007-lang\")"
     echo "  (id \"${id}\")"
     echo "  (domain \"${domain}\")"
     echo "  (theorem \"$(printf '%s' "${thm}" | sed 's/"/\\"/g')\")"
diff --git a/stapeln.toml b/stapeln.toml
index 546de2d..9bf4706 100644
--- a/stapeln.toml
+++ b/stapeln.toml
@@ -53,7 +53,7 @@ packages = ["ca-certificates", "curl"]
 copy-from = [
     { layer = "build", src = "/app/", dst = "/app/" },
 ]
-entrypoint = ["["/usr/local/bin/oo7"]"]
+entrypoint = ["/usr/local/bin/oo7"]
 user = "nonroot"
 
 # ── Security ───────────────────────────────────────────────────

From 5a80af50aaf273e1d9f41bc476dff9c6c6f9efc9 Mon Sep 17 00:00:00 2001
From: Claude <paraordinate@yahoo.co.uk>
Date: Wed, 3 Jun 2026 21:47:46 +0000
Subject: [PATCH 3/4] chore: gitignore generated INSTALL-SECURITY-REPORT.adoc

Generated by docs/internal/setup.sh during environment setup; an
ephemeral platform snapshot, not repo content. Mirrors the existing
/*_REPORT.md ignore for the .adoc variant.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 9500e9a..2c448dd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,6 +49,7 @@ oo7-control-plane/oo7_interpreter.h
 # Session debris (one-off reports, scripts)
 /*_SUMMARY.md
 /*_REPORT.md
+/*-REPORT.adoc
 /*_COMPLETE.md
 /apply_grammar_changes*.sh
 

From 47fce34b45f840da044cc79257b6b0eb1717e900 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 6 Jun 2026 20:33:04 +0100
Subject: [PATCH 4/4] ci: remove duplicate hypatia-scan.yml (covered by
 static-analysis-gate)

Fixes duplicate Hypatia scanning that causes failing check in PR #34.
static-analysis-gate.yml already contains a Hypatia neurosymbolic scan job.
---
 .github/workflows/hypatia-scan.yml | 29 -----------------------------
 1 file changed, 29 deletions(-)
 delete mode 100644 .github/workflows/hypatia-scan.yml

diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
deleted file mode 100644
index c68b9ed..0000000
--- a/.github/workflows/hypatia-scan.yml
+++ /dev/null
@@ -1,29 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Thin wrapper around hyperpolymath/standards hypatia-scan-reusable.yml.
-# See standards#191 for the reusable's purpose and design.
-
-name: Hypatia Security Scan
-
-on:
-  push:
-    branches: [main, master, develop]
-  pull_request:
-    branches: [main, master]
-  schedule:
-    - cron: '0 0 * * 0'
-  workflow_dispatch:
-
-# Estate guardrail: cancel superseded runs so re-pushes don't pile up.
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
-
-permissions:
-  contents: read
-  security-events: write
-  pull-requests: write
-
-jobs:
-  hypatia:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89
-    secrets: inherit