hyperpolymath · hyperpolymath · Jun 6, 2026 · Jun 3, 2026 · Jun 3, 2026 · Jun 3, 2026
@@ -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"

@@ -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
 

@@ -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>

@@ -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

@@ -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 = {

@@ -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 = {

@@ -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.

@@ -35,6 +35,7 @@
 ;   shortcut.  Zero v1.0 violations.
 
 (axiom-triage
+  (project "007-lang")
   (generated "2026-04-27")
   (standard "v1.1-closure-permitted")
   (summary

@@ -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")

@@ -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"]

@@ -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,
+                },
+            ],
+        },
     }
 }
 

@@ -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")

@@ -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 {