ArghDA M2: Cubical-Agda backend — the flag-profile island

.machine_readable/6a2/STATE.a2ml

@@ -42,7 +42,7 @@ milestones = [
 milestones = [
   { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes", completion = 80 },
   { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 },
-  { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 },
+  { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 100 },
   { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 },
   { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 },
   { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 },
@@ -60,6 +60,23 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M2 landed 2026-07-01: Cubical-Agda variant. Implemented as a SEPARATE backend
+# `AgdaCubical` (name "agda-cubical") rather than the plan's `Agda::cubical()`
+# constructor — a distinct type expresses the flag-profile ISLAND better (a
+# `--cubical --safe` file and a `--safe --without-K` file cannot import each
+# other; Agda enforces this at typecheck and arghda surfaces the resulting
+# Error honestly) and avoids churning ~19 `Agda` value-uses. `--cubical --safe`,
+# NOT `--without-K`. src/prover/agda.rs: `AgdaCubical` shares invoke_agda()
+# (adds `--cubical`) + the graph methods with `Agda`; differs in name/safe_mode/
+# lint pack. src/lint/safe_pragma.rs: `SafePragma` parameterised by required
+# flags — `standard()` = [--safe,--without-K], `cubical()` = [--cubical,--safe];
+# lint::agda_cubical_rules() swaps it in. Wired via `--backend agda-cubical`.
+# 107 tests (79 lib + 28 integration; +3 safe_pragma unit +1 cubical-identity
+# unit +3 cubical integration). Dogfooded REAL: `check --backend agda-cubical`
+# on a --cubical --safe file → proven-eligible; the standard `agda` backend on
+# the SAME file → rejected (missing-safe-pragma: missing --without-K). The
+# island distinction is demonstrated end-to-end.
+#
 # M5 landed 2026-07-01: SMT solver backends (Z3, CVC5) — the FIRST Solver-kind
 # backends, exercising the other half of the taxonomy. src/prover/smt.rs: one
 # `Smt { name, cmd }` type with `Smt::z3()`/`Smt::cvc5()`. Kind=Solver, ext
@@ -135,13 +152,13 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M1 (Backend trait) + M3 (reasoning graph) + M4 (Idris2) + M5 (Z3/CVC5) DONE. Both interaction models (Assistant + Solver) now real. Next:",
-  "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden). Small — extends the existing Agda backend.",
+  "M1 + M2 + M3 + M4 + M5 DONE. Five backends across both interaction models: agda, agda-cubical, idris2 (Assistant); z3, cvc5 (Solver). Next:",
+  "Finish M0: add the `arghda doctor` Rust subcommand — report which of the five backends are actually runnable (probe each binary), repoint `just doctor` at it, feed the Groove manifest. Closes the last M0 gap.",
   "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned.",
-  "Finish M0: add the `arghda doctor` Rust subcommand (report which backends are runnable — now agda/idris2/z3/cvc5) and repoint `just doctor` at it.",
+  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone).",
   "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).",
-  "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.",
+  "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.",
 ]
 
 [maintenance-status]
@@ -150,9 +167,9 @@ 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-M5: 75 lib + 25 integration = 100 tests pass. Dogfooded via real CLI on
-# all four backends: agda + idris2 (Assistant), z3 + cvc5 (Solver). Dogfooded
-# historically against echo-types + agda-unused.
+# post-M2: 79 lib + 28 integration = 107 tests pass. Dogfooded via real CLI on
+# all five backends: agda + agda-cubical + idris2 (Assistant), z3 + cvc5
+# (Solver). Dogfooded historically against echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

@@ -30,6 +30,8 @@ pub use diagnostic::{Diagnostic, LintReport, Severity};
 pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
-pub use prover::{default_backend, Agda, Backend, BackendKind, Idris2, Outcome, Smt, Verdict};
+pub use prover::{
+    default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Outcome, Smt, Verdict,
+};
 pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode};
 pub use workspace::{StaleEntry, State, Workspace};

src/lint/mod.rs

@@ -47,11 +47,10 @@ impl Default for RuleConfig {
     }
 }
 
-/// The standard lint pack, parameterised by operator config. Fails only if a
-/// supplied pattern (e.g. `headline_pattern`) is not a valid regex.
-pub fn rules_with_config(cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
+/// The Agda lint pack around a given `missing-safe-pragma` profile.
+fn agda_pack(cfg: &RuleConfig, safe: safe_pragma::SafePragma) -> Result<Vec<Box<dyn LintRule>>> {
     Ok(vec![
-        Box::new(safe_pragma::SafePragma),
+        Box::new(safe),
         Box::new(orphan_module::OrphanModule),
         Box::new(postulate::UnjustifiedPostulate),
         Box::new(escape_hatch::EscapeHatch),
@@ -62,6 +61,20 @@ pub fn rules_with_config(cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
     ])
 }
 
+/// The standard `--safe --without-K` Agda lint pack, parameterised by
+/// operator config. Fails only if a supplied pattern (e.g.
+/// `headline_pattern`) is not a valid regex.
+pub fn rules_with_config(cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
+    agda_pack(cfg, safe_pragma::SafePragma::standard())
+}
+
+/// The Cubical-Agda (`--cubical --safe`) lint pack — identical to the
+/// standard pack except the `missing-safe-pragma` rule requires `--cubical`
+/// instead of `--without-K`.
+pub fn agda_cubical_rules(cfg: &RuleConfig) -> Result<Vec<Box<dyn LintRule>>> {
+    agda_pack(cfg, safe_pragma::SafePragma::cubical())
+}
+
 /// The standard lint pack with default config. The default pattern is a
 /// known-good literal, so this is infallible.
 pub fn default_rules() -> Vec<Box<dyn LintRule>> {

src/lint/safe_pragma.rs

@@ -1,16 +1,43 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
+//! `missing-safe-pragma` (hard-block) — require the soundness OPTIONS pragma.
+//!
+//! Parameterised by the flags a file's `{-# OPTIONS … #-}` must carry.
+//! Standard Agda demands `--safe --without-K`; Cubical Agda demands
+//! `--cubical --safe` (cubical is incompatible with `--without-K`, so
+//! requiring it there would be wrong). Both profiles share the rule name so
+//! the reasoning graph / DAG treat them uniformly.
+
 use super::{LintContext, LintRule};
 use crate::diagnostic::{Diagnostic, LintReport, Severity};
 use anyhow::{Context, Result};
 use std::fs;
 use std::path::Path;
 
-pub struct SafePragma;
+/// Requires a specific set of flags in an OPTIONS pragma.
+pub struct SafePragma {
+    required: &'static [&'static str],
+}
 
 const HEAD_LINES_SCANNED: usize = 30;
 
+impl SafePragma {
+    /// Standard `--safe --without-K` Agda.
+    pub const fn standard() -> Self {
+        Self {
+            required: &["--safe", "--without-K"],
+        }
+    }
+
+    /// Cubical Agda: `--cubical --safe` (no `--without-K`).
+    pub const fn cubical() -> Self {
+        Self {
+            required: &["--cubical", "--safe"],
+        }
+    }
+}
+
 impl LintRule for SafePragma {
     fn name(&self) -> &'static str {
         "missing-safe-pragma"
@@ -20,37 +47,37 @@ impl LintRule for SafePragma {
         let contents =
             fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
 
-        let mut safe_seen = false;
-        let mut without_k_seen = false;
-
+        let mut seen = vec![false; self.required.len()];
         for line in contents.lines().take(HEAD_LINES_SCANNED) {
             if !line.trim_start().starts_with("{-#") {
                 continue;
             }
             if line.contains("OPTIONS") {
-                if line.contains("--safe") {
-                    safe_seen = true;
-                }
-                if line.contains("--without-K") {
-                    without_k_seen = true;
+                for (i, flag) in self.required.iter().enumerate() {
+                    if line.contains(flag) {
+                        seen[i] = true;
+                    }
                 }
             }
         }
 
-        if !safe_seen || !without_k_seen {
-            let missing = match (safe_seen, without_k_seen) {
-                (false, false) => "--safe and --without-K",
-                (false, true) => "--safe",
-                (true, false) => "--without-K",
-                _ => unreachable!(),
-            };
+        let missing: Vec<&str> = self
+            .required
+            .iter()
+            .zip(&seen)
+            .filter(|(_, &s)| !s)
+            .map(|(flag, _)| *flag)
+            .collect();
+
+        if !missing.is_empty() {
             report.push(Diagnostic {
                 rule: self.name().to_string(),
                 severity: Severity::HardBlock,
                 file: file.to_path_buf(),
                 message: format!(
                     "missing {} pragma in first {} lines",
-                    missing, HEAD_LINES_SCANNED
+                    missing.join(" and "),
+                    HEAD_LINES_SCANNED
                 ),
                 line: None,
             });
@@ -59,3 +86,60 @@ impl LintRule for SafePragma {
         Ok(())
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_with(rule: SafePragma, body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(rule)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn standard_requires_safe_and_without_k() {
+        let ok = lint_with(
+            SafePragma::standard(),
+            "{-# OPTIONS --safe --without-K #-}\nmodule M where\n",
+        );
+        assert!(ok.diagnostics.is_empty());
+        let bad = lint_with(SafePragma::standard(), "module M where\n");
+        assert!(bad.has_hard_block());
+    }
+
+    #[test]
+    fn standard_rejects_a_cubical_file() {
+        // A cubical file lacks --without-K, so the standard rule flags it.
+        let r = lint_with(
+            SafePragma::standard(),
+            "{-# OPTIONS --cubical --safe #-}\nmodule M where\n",
+        );
+        assert!(r.has_hard_block());
+        assert!(r.diagnostics[0].message.contains("--without-K"));
+    }
+
+    #[test]
+    fn cubical_accepts_cubical_and_rejects_without_k_only() {
+        let ok = lint_with(
+            SafePragma::cubical(),
+            "{-# OPTIONS --cubical --safe #-}\nmodule M where\n",
+        );
+        assert!(ok.diagnostics.is_empty(), "cubical pragma must pass");
+        // A standard --safe --without-K file lacks --cubical: flagged here.
+        let bad = lint_with(
+            SafePragma::cubical(),
+            "{-# OPTIONS --safe --without-K #-}\nmodule M where\n",
+        );
+        assert!(bad.has_hard_block());
+        assert!(bad.diagnostics[0].message.contains("--cubical"));
+    }
+}

src/main.rs

@@ -4,8 +4,8 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, build_reason, event, run_lints, unused, watcher, Agda, Backend, Idris2, LintRule,
-    RuleConfig, Smt, State, Workspace,
+    build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend, Idris2,
+    LintRule, RuleConfig, Smt, State, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -20,18 +20,21 @@ type RuleSet = Vec<Box<dyn LintRule>>;
 fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
     match name {
         "agda" => Ok(Box::new(Agda)),
+        "agda-cubical" => Ok(Box::new(AgdaCubical)),
         "idris2" => Ok(Box::new(Idris2)),
         "z3" => Ok(Box::new(Smt::z3())),
         "cvc5" => Ok(Box::new(Smt::cvc5())),
-        other => anyhow::bail!("unknown backend `{other}` (known: agda, idris2, z3, cvc5)"),
+        other => {
+            anyhow::bail!("unknown backend `{other}` (known: agda, agda-cubical, idris2, z3, cvc5)")
+        }
     }
 }
 
 #[derive(Parser)]
 #[command(
     name = "arghda",
     version,
-    about = "Proof-workspace manager for provers/solvers (Agda, Idris2, Z3, CVC5)"
+    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Z3, CVC5)"
 )]
 struct Cli {
     #[command(subcommand)]
@@ -58,7 +61,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Also run the external `agda-unused` analyser and re-emit its
@@ -77,7 +80,7 @@ enum Cmd {
         /// Include root (search path). Defaults to the file's directory.
         #[arg(long)]
         include_root: Option<PathBuf>,
-        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Emit the report as JSON.
@@ -100,7 +103,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
     },
@@ -123,7 +126,7 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Prover/solver backend: `agda` (default), `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Run the backend on every node to populate REAL prover verdicts