ArghDA M11: studio JSON freeze (reason/0.1) + Groove discovery manifest (#39)

## What & why

Closes the **one remaining open v0.1 milestone** (Groove service
manifest). Two deliverables:

### Studio JSON freeze (`reason/0.1`)

A JSON-contract test in `src/reason/mod.rs` pins the schema
arghda-studio / Groove consumers depend on — top-level
(`version`/`dag`/`nodes`/`edges`/`crt_roots`), per-node
(`id`/`self_verdict`/`effective`/`verdict_evidence`/`soundness`/`wired`),
per-edge (`from`/`to`/`junct`/`kind`). A rename now breaks a test: bump
the version, don't silently edit.

### Groove manifest (`src/groove.rs`, `arghda groove`)

Groove is the estate's HTTP service-discovery protocol. `GrooveManifest`
(`groove: "0.1"`; capabilities = live backend probes + CLI commands +
the frozen `dag/0.1` + `reason/0.1` schema versions). `arghda groove
[--output <path>]` emits it to stdout, or writes a `/.well-known/groove`
file (creating parent dirs).

arghda-core is a CLI, so it **emits** the manifest; serving it over HTTP
at `/.well-known/groove` is the host's (PanLL's) job — honest, no
embedded HTTP server. Backends are probed *live*, so the manifest
reflects what this machine can actually run.

## Verified (ran, not inferred)

- `cargo test` → **121 passing, 0 failed** (+1 groove unit, +1
reason-contract freeze).
- `cargo clippy -D warnings` clean · `cargo fmt --check` clean ·
`check-spdx.sh` OK.
- **Dogfooded:** `arghda groove` → all 6 backends runnable, schemas
`0.1`, commands listed; `arghda groove --output
/tmp/site/.well-known/groove` wrote the file.

## Milestone status

**The v0.1 spec is now closed** (Groove was the last open milestone),
and STATE records M11 = 100%. The engine-spine deliverable (M0–M7 + M11)
is complete bar **M7** (Echidna dispatch seam), which is the natural
next step. Beyond that: the M3/M4/M6 follow-ons and the heavy-prover
tail M8–M10.

---
_Generated by [Claude
Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -30,7 +30,7 @@ milestones = [
   { name = "Content-hash invalidation of proven (file-level + transitive-import closure via [proven] include_root)", completion = 100 },
   { name = "Operator config (.arghda/config.toml + --headline-pattern + --config)", completion = 100 },
   { name = "RSR / standards alignment (.machine_readable, README.adoc, EXPLAINME, LICENSE, .well-known)", completion = 100 },
-  { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 },
+  { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 100 },
 ]
 
 # "Flying Logic for provers/solvers" epic (v0.2+): generalise the Agda-only
@@ -51,7 +51,7 @@ milestones = [
   { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 },
-  { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 0 },
+  { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 },
 ]
 # M0 provisioning verified in-container 2026-07-01: agda 2.6.3 (+stdlib v2.3
 # +cubical lib), zig 0.15.2, z3 4.8.12, cvc5 1.2.0, lean 4.13.0 all report
@@ -60,6 +60,22 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M11 landed 2026-07-01: studio JSON freeze (reason/0.1) + Groove manifest —
+# closes the ONE open v0.1 milestone (Groove service manifest, was 0%). Two
+# deliverables. (1) Studio JSON freeze: a reason/0.1 JSON CONTRACT test in
+# src/reason/mod.rs pins the top-level (version/dag/nodes/edges/crt_roots) +
+# per-node (id/self_verdict/effective/verdict_evidence/soundness/wired) +
+# per-edge (from/to/junct/kind) keys — a rename now breaks a test (bump the
+# version, don't silently edit). (2) Groove: src/groove.rs `GrooveManifest`
+# (groove 0.1; service/description; capabilities = live backend probes +
+# commands + frozen schemas dag/0.1+reason/0.1). `arghda groove [--output
+# <path>]` emits it (stdout, or writes a `/.well-known/groove` file, creating
+# parent dirs). arghda-core is a CLI so it EMITS the manifest; serving it over
+# HTTP is the host's (PanLL's) job — honest. Backends probed live so the
+# manifest reflects this machine. 121 tests (88 lib + 33 integration; +1 groove
+# unit +1 reason-contract-freeze unit). Dogfooded: `arghda groove` → all 6
+# backends runnable, schemas 0.1; `--output` wrote /.well-known/groove.
+#
 # M6 landed 2026-07-01 (85%): the Lean4 backend — sixth backend. src/prover/
 # lean.rs: `lean <file>` elaboration. The honesty subtlety Lean forces: a green
 # exit does NOT mean proven (sorry is only a warning; exit 0). So the verdict is
@@ -184,10 +200,9 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M0-M6 DONE. SIX backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine essentially complete. Next:",
-  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds the manifest).",
-  "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome).",
-  "M6 follow-on (15%): lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.",
+  "M0-M6 + M11 DONE. The v0.1 spec is now CLOSED (Groove manifest was the last open milestone). Engine-spine deliverable (M0-M7 + M11) is complete bar M7. Six backends + reasoning graph + doctor + groove. Remaining:",
+  "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome) — completes the engine-spine deliverable.",
+  "M6 follow-on: lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.",
   "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.",
   "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).",
   "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.",
@@ -199,10 +214,11 @@ last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 0
 open-failures = 0
 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green
-# post-M6: 86 lib + 33 integration = 119 tests pass. `arghda doctor` dogfooded:
-# 6/6 backends runnable. All six dogfooded via real CLI: agda + agda-cubical +
-# idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded historically against
-# echo-types + agda-unused.
+# post-M11: 88 lib + 33 integration = 121 tests pass. `arghda doctor`/`groove`
+# dogfooded: 6/6 backends runnable; manifest emits + writes /.well-known/groove.
+# All six backends dogfooded via real CLI: agda + agda-cubical + idris2 + lean4
+# (Assistant), z3 + cvc5 (Solver). Dogfooded historically vs echo-types +
+# agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/groove.rs

@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Groove service-discovery manifest.
+//!
+//! Groove is the estate's HTTP-based service-discovery protocol: a capability
+//! provider publishes a manifest at `/.well-known/groove` so consumers (e.g.
+//! PanLL) can auto-detect it and wire it in without manual configuration.
+//!
+//! arghda-core is a CLI, not a server, so it *emits* the manifest (`arghda
+//! groove`) as JSON; serving it over HTTP at `/.well-known/groove` is the
+//! host's job (a web server, or the PanLL shell). Backend availability is
+//! probed live, so the manifest reflects what this machine can actually run —
+//! honest discovery, not a static advertisement.
+//!
+//! This is arghda's v0.1 manifest shape (`groove: "0.1"`); it announces the
+//! two frozen JSON schemas the visual layer consumes (`dag/0.1`,
+//! `reason/0.1`), the CLI commands, and the probed backends.
+
+use crate::prover::Probe;
+use serde::Serialize;
+
+/// The JSON-contract schema versions the visual layer (arghda-studio) and
+/// PanLL consume. Frozen — bump only on a breaking change.
+#[derive(Clone, Debug, Serialize)]
+pub struct Schemas {
+    pub dag: &'static str,
+    pub reason: &'static str,
+}
+
+/// What arghda announces it can do.
+#[derive(Clone, Debug, Serialize)]
+pub struct Capabilities {
+    /// Live probe of each known backend (id, kind, runnable, detail).
+    pub backends: Vec<Probe>,
+    /// The CLI verbs a consumer can drive.
+    pub commands: Vec<&'static str>,
+    /// The frozen output-schema versions.
+    pub schemas: Schemas,
+}
+
+/// The `/.well-known/groove` manifest for arghda.
+#[derive(Clone, Debug, Serialize)]
+pub struct GrooveManifest {
+    /// Groove manifest-schema version.
+    pub groove: &'static str,
+    pub service: &'static str,
+    pub description: &'static str,
+    pub capabilities: Capabilities,
+}
+
+/// Build the manifest from live backend probes.
+pub fn manifest(backends: Vec<Probe>) -> GrooveManifest {
+    GrooveManifest {
+        groove: "0.1",
+        service: "arghda",
+        description: "proof-workspace manager for provers and solvers",
+        capabilities: Capabilities {
+            backends,
+            commands: vec!["scan", "check", "dag", "reason", "doctor", "groove"],
+            schemas: Schemas {
+                dag: "0.1",
+                reason: "0.1",
+            },
+        },
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::prover::BackendKind;
+
+    fn probe(name: &str) -> Probe {
+        Probe {
+            backend: name.to_string(),
+            kind: BackendKind::Assistant,
+            runnable: true,
+            detail: "v1".to_string(),
+        }
+    }
+
+    #[test]
+    fn manifest_announces_frozen_schemas_and_backends() {
+        let m = manifest(vec![probe("agda"), probe("lean4")]);
+        assert_eq!(m.groove, "0.1");
+        assert_eq!(m.service, "arghda");
+        assert_eq!(m.capabilities.schemas.dag, "0.1");
+        assert_eq!(m.capabilities.schemas.reason, "0.1");
+        assert_eq!(m.capabilities.backends.len(), 2);
+        assert!(m.capabilities.commands.contains(&"reason"));
+        // It serialises to the expected discovery shape.
+        let v = serde_json::to_value(&m).unwrap();
+        assert_eq!(v["groove"], "0.1");
+        assert_eq!(v["capabilities"]["schemas"]["reason"], "0.1");
+        assert_eq!(v["capabilities"]["backends"][0]["backend"], "agda");
+    }
+}

src/lib.rs

@@ -15,6 +15,7 @@ pub mod dag;
 pub mod diagnostic;
 pub mod event;
 pub mod graph;
+pub mod groove;
 pub mod hash;
 pub mod lint;
 pub mod proven;
@@ -29,6 +30,7 @@ pub use dag::{build as build_dag, DagDocument};
 pub use diagnostic::{Diagnostic, LintReport, Severity};
 pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
+pub use groove::{manifest as groove_manifest, GrooveManifest};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
 pub use prover::{
     default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Lean, Outcome, Probe, Smt,

src/main.rs

@@ -4,8 +4,9 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend,
-    BackendKind, Idris2, Lean, LintRule, RuleConfig, Smt, State, Verdict, Workspace,
+    build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical,
+    Backend, BackendKind, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict,
+    Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -170,6 +171,15 @@ enum Cmd {
         #[arg(long)]
         json: bool,
     },
+    /// Emit the Groove service-discovery manifest (`/.well-known/groove`).
+    /// Announces arghda's capabilities (probed backends, CLI commands, and
+    /// the frozen `dag/0.1` + `reason/0.1` schemas) for PanLL discovery.
+    Groove {
+        /// Write the manifest to a file instead of stdout (e.g.
+        /// `<site>/.well-known/groove`).
+        #[arg(long)]
+        output: Option<PathBuf>,
+    },
 }
 
 fn main() -> Result<()> {
@@ -252,16 +262,41 @@ fn main() -> Result<()> {
         } => stale(&workspace, invalidate)?,
         Cmd::Watch { workspace } => watch(&workspace)?,
         Cmd::Doctor { json } => doctor(json)?,
+        Cmd::Groove { output } => groove(output.as_deref())?,
     }
     Ok(())
 }
 
-/// Probe every known backend and report which are actually runnable.
-fn doctor(json: bool) -> Result<()> {
-    let probes = KNOWN_BACKENDS
+/// Probe every known backend for runnability (shared by `doctor`/`groove`).
+fn probe_all() -> Result<Vec<Probe>> {
+    KNOWN_BACKENDS
         .iter()
         .map(|name| backend_for(name).map(|b| b.probe()))
-        .collect::<Result<Vec<_>>>()?;
+        .collect()
+}
+
+/// Emit the Groove service-discovery manifest (stdout, or `--output` file).
+fn groove(output: Option<&Path>) -> Result<()> {
+    let manifest = groove_manifest(probe_all()?);
+    let json = serde_json::to_string_pretty(&manifest)?;
+    match output {
+        Some(path) => {
+            if let Some(parent) = path.parent() {
+                std::fs::create_dir_all(parent)
+                    .with_context(|| format!("creating {}", parent.display()))?;
+            }
+            std::fs::write(path, format!("{json}\n"))
+                .with_context(|| format!("writing {}", path.display()))?;
+            println!("wrote Groove manifest to {}", path.display());
+        }
+        None => println!("{json}"),
+    }
+    Ok(())
+}
+
+/// Probe every known backend and report which are actually runnable.
+fn doctor(json: bool) -> Result<()> {
+    let probes = probe_all()?;
 
     if json {
         let payload = serde_json::json!({ "version": "0.1", "backends": probes });

src/reason/mod.rs

@@ -531,4 +531,65 @@ mod tests {
         assert!(wired.contains("Deep"));
         assert!(!wired.contains("Orphan"));
     }
+
+    // ── reason/0.1 JSON contract freeze (M11) ────────────────────────────
+    // The visual layer (arghda-studio) + Groove consumers depend on this
+    // shape. A rename here is a BREAKING change — bump the version, don't
+    // silently edit. This test pins the schema so that can't happen by
+    // accident.
+    #[test]
+    fn reason_json_contract_is_frozen_at_0_1() {
+        use crate::dag::{DagDocument, DagNode, LintSummary};
+        use crate::graph::Edge;
+        use crate::prover::Agda;
+        use std::path::PathBuf;
+
+        let dag = DagDocument {
+            version: "0.1",
+            include_root: PathBuf::from("/r"),
+            entry_modules: vec![PathBuf::from("/r/All.agda")],
+            generated_at: "t".to_string(),
+            nodes: vec![
+                DagNode {
+                    id: "All".to_string(),
+                    file: PathBuf::from("All.agda"),
+                    status: "clean",
+                    lint: LintSummary::default(),
+                    headlines: vec![],
+                },
+                DagNode {
+                    id: "Util".to_string(),
+                    file: PathBuf::from("Util.agda"),
+                    status: "clean",
+                    lint: LintSummary::default(),
+                    headlines: vec![],
+                },
+            ],
+            edges: vec![Edge {
+                from: "All".to_string(),
+                to: "Util".to_string(),
+                kind: "imports",
+            }],
+            blocked: vec![],
+        };
+        let doc = build(dag, &Agda, &BTreeMap::new(), &BTreeSet::new());
+        let v = serde_json::to_value(&doc).unwrap();
+
+        assert_eq!(v["version"], "0.1");
+        assert!(v["dag"].is_object(), "the DAG is embedded verbatim");
+        assert!(v["crt_roots"].is_array());
+        for k in [
+            "id",
+            "self_verdict",
+            "effective",
+            "verdict_evidence",
+            "soundness",
+            "wired",
+        ] {
+            assert!(v["nodes"][0].get(k).is_some(), "reason node missing `{k}`");
+        }
+        for k in ["from", "to", "junct", "kind"] {
+            assert!(v["edges"][0].get(k).is_some(), "reason edge missing `{k}`");
+        }
+    }
 }