asupersync_conformance/
lean_coverage_matrix.rs

1//! Lean proof coverage ontology and machine-readable matrix model.
2//!
3//! This module defines a deterministic schema for tracking Lean proof coverage
4//! across semantic rules, invariants, refinement obligations, and operational
5//! CI gates.
6
7use serde::{Deserialize, Serialize};
8use std::collections::{BTreeSet, HashSet};
9
10/// Stable schema version for Lean coverage matrix artifacts.
11pub const LEAN_COVERAGE_SCHEMA_VERSION: &str = "1.0.0";
12
13/// Canonical row types in the Lean coverage matrix.
14#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
15#[serde(rename_all = "snake_case")]
16pub enum CoverageRowType {
17    /// A small-step semantic rule or constructor-level proof obligation.
18    SemanticRule,
19    /// A project invariant (for example, no obligation leaks).
20    Invariant,
21    /// A Rust-to-Lean refinement obligation.
22    RefinementObligation,
23    /// A CI/operational gate proving proof health in automation.
24    OperationalGate,
25}
26
27/// Canonical status model for Lean coverage rows.
28#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
29#[serde(rename_all = "kebab-case")]
30pub enum CoverageStatus {
31    /// Work not started.
32    NotStarted,
33    /// Work actively in progress.
34    InProgress,
35    /// Work is blocked by a known blocker.
36    Blocked,
37    /// The proof is complete and locally validated.
38    Proven,
39    /// Proven and validated in CI automation.
40    ValidatedInCi,
41}
42
43/// Deterministic blocker taxonomy codes.
44#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
45pub enum BlockerCode {
46    /// Missing helper lemma(s) or dependency theorem(s).
47    #[serde(rename = "BLK_PROOF_MISSING_LEMMA")]
48    ProofMissingLemma,
49    /// Proof shape/tactic path mismatch after model evolution.
50    #[serde(rename = "BLK_PROOF_SHAPE_MISMATCH")]
51    ProofShapeMismatch,
52    /// Lean model/spec is incomplete or inconsistent with intended semantics.
53    #[serde(rename = "BLK_MODEL_GAP")]
54    ModelGap,
55    /// Rust runtime behavior diverges from formal model assumptions.
56    #[serde(rename = "BLK_IMPL_DIVERGENCE")]
57    ImplDivergence,
58    /// CI/build/toolchain infrastructure prevents validation.
59    #[serde(rename = "BLK_TOOLCHAIN_FAILURE")]
60    ToolchainFailure,
61    /// External dependency or sequencing blocker.
62    #[serde(rename = "BLK_EXTERNAL_DEPENDENCY")]
63    ExternalDependency,
64}
65
66/// Optional blocker payload when a row is blocked.
67#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
68pub struct CoverageBlocker {
69    /// Deterministic blocker code.
70    pub code: BlockerCode,
71    /// Human-readable blocker detail.
72    pub detail: String,
73}
74
75/// Evidence record for a coverage row.
76#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
77pub struct CoverageEvidence {
78    /// Lean theorem name associated with this row.
79    #[serde(default, skip_serializing_if = "Option::is_none")]
80    pub theorem_name: Option<String>,
81    /// Source file containing theorem/proof evidence.
82    #[serde(default, skip_serializing_if = "Option::is_none")]
83    pub file_path: Option<String>,
84    /// 1-based source line for the theorem/proof evidence.
85    #[serde(default, skip_serializing_if = "Option::is_none")]
86    pub line: Option<u32>,
87    /// Path to a generated proof artifact (log/manifest/report).
88    #[serde(default, skip_serializing_if = "Option::is_none")]
89    pub proof_artifact: Option<String>,
90    /// CI job identifier that validated the proof.
91    #[serde(default, skip_serializing_if = "Option::is_none")]
92    pub ci_job: Option<String>,
93    /// Reviewer identity for human validation/sign-off.
94    #[serde(default, skip_serializing_if = "Option::is_none")]
95    pub reviewer: Option<String>,
96}
97
98impl CoverageEvidence {
99    fn is_empty(&self) -> bool {
100        self.theorem_name.is_none()
101            && self.file_path.is_none()
102            && self.line.is_none()
103            && self.proof_artifact.is_none()
104            && self.ci_job.is_none()
105            && self.reviewer.is_none()
106    }
107}
108
109/// One row in the Lean proof coverage matrix.
110#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
111pub struct CoverageRow {
112    /// Stable row identifier (for example, `sem.cancel.request.wf`).
113    pub id: String,
114    /// Human-readable row title.
115    pub title: String,
116    /// Row type classification.
117    pub row_type: CoverageRowType,
118    /// Current coverage status.
119    pub status: CoverageStatus,
120    /// Free-form row description.
121    pub description: String,
122    /// Optional owner for coordination.
123    #[serde(default, skip_serializing_if = "Option::is_none")]
124    pub owner: Option<String>,
125    /// Stable IDs this row depends on.
126    #[serde(default)]
127    pub depends_on: Vec<String>,
128    /// Optional tags for query/filter.
129    #[serde(default)]
130    pub tags: Vec<String>,
131    /// Optional blocker payload.
132    #[serde(default, skip_serializing_if = "Option::is_none")]
133    pub blocker: Option<CoverageBlocker>,
134    /// Proof/CI evidence for this row.
135    #[serde(default)]
136    pub evidence: Vec<CoverageEvidence>,
137}
138
139/// Top-level Lean proof coverage matrix artifact.
140#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
141pub struct LeanCoverageMatrix {
142    /// Schema version for compatibility and migrations.
143    pub schema_version: String,
144    /// Matrix identifier for downstream references.
145    pub matrix_id: String,
146    /// Matrix title.
147    pub title: String,
148    /// Scope narrative and interpretation guidance.
149    pub scope: String,
150    /// Coverage rows.
151    pub rows: Vec<CoverageRow>,
152}
153
154impl LeanCoverageMatrix {
155    /// Parse a matrix from JSON text.
156    pub fn from_json_str(input: &str) -> Result<Self, serde_json::Error> {
157        serde_json::from_str(input)
158    }
159
160    /// Serialize the matrix into pretty-printed JSON.
161    pub fn to_pretty_json(&self) -> Result<String, serde_json::Error> {
162        serde_json::to_string_pretty(self)
163    }
164
165    /// Validate matrix structure and status/evidence consistency.
166    pub fn validate(&self) -> Result<(), Vec<String>> {
167        let mut errors = Vec::new();
168        if self.schema_version != LEAN_COVERAGE_SCHEMA_VERSION {
169            errors.push(format!(
170                "schema_version must be '{LEAN_COVERAGE_SCHEMA_VERSION}' (got '{}')",
171                self.schema_version
172            ));
173        }
174
175        if !is_valid_stable_id(&self.matrix_id) {
176            errors.push(format!(
177                "matrix_id '{}' must be lowercase stable-id format [a-z0-9._-]",
178                self.matrix_id
179            ));
180        }
181
182        let mut ids = HashSet::new();
183        let mut all_ids = BTreeSet::new();
184        for row in &self.rows {
185            if !is_valid_stable_id(&row.id) {
186                errors.push(format!(
187                    "row '{}' has invalid id format; use lowercase stable-id [a-z0-9._-]",
188                    row.title
189                ));
190            }
191            if !ids.insert(row.id.clone()) {
192                errors.push(format!("duplicate row id '{}'", row.id));
193            }
194            all_ids.insert(row.id.clone());
195        }
196
197        for row in &self.rows {
198            for dep in &row.depends_on {
199                if !all_ids.contains(dep) {
200                    errors.push(format!(
201                        "row '{}' depends_on missing row id '{}'",
202                        row.id, dep
203                    ));
204                }
205                if dep == &row.id {
206                    errors.push(format!("row '{}' cannot depend on itself", row.id));
207                }
208            }
209            if let Some(blocker) = &row.blocker
210                && blocker.detail.trim().is_empty()
211            {
212                errors.push(format!(
213                    "row '{}' has blocker '{:?}' with empty detail",
214                    row.id, blocker.code
215                ));
216            }
217
218            match row.status {
219                CoverageStatus::Blocked => {
220                    if row.blocker.is_none() {
221                        errors.push(format!(
222                            "row '{}' is blocked but missing blocker payload",
223                            row.id
224                        ));
225                    }
226                }
227                CoverageStatus::Proven | CoverageStatus::ValidatedInCi => {
228                    if row.evidence.is_empty() {
229                        errors.push(format!(
230                            "row '{}' is {:?} but has no evidence entries",
231                            row.id, row.status
232                        ));
233                    }
234                    if row.blocker.is_some() {
235                        errors.push(format!(
236                            "row '{}' is {:?} but still has blocker payload",
237                            row.id, row.status
238                        ));
239                    }
240                }
241                CoverageStatus::NotStarted | CoverageStatus::InProgress => {
242                    if row.blocker.is_some() {
243                        errors.push(format!(
244                            "row '{}' has blocker payload but status is {:?}",
245                            row.id, row.status
246                        ));
247                    }
248                }
249            }
250
251            if row.status == CoverageStatus::ValidatedInCi
252                && !row.evidence.iter().any(|e| e.ci_job.is_some())
253            {
254                errors.push(format!(
255                    "row '{}' is validated-in-ci but has no ci_job in evidence",
256                    row.id
257                ));
258            }
259
260            for (index, evidence) in row.evidence.iter().enumerate() {
261                if evidence.is_empty() {
262                    errors.push(format!(
263                        "row '{}' evidence[{index}] is empty; at least one evidence field is required",
264                        row.id
265                    ));
266                }
267                if evidence.line.is_some() && evidence.file_path.is_none() {
268                    errors.push(format!(
269                        "row '{}' evidence[{index}] has line but missing file_path",
270                        row.id
271                    ));
272                }
273            }
274        }
275
276        if errors.is_empty() {
277            Ok(())
278        } else {
279            Err(errors)
280        }
281    }
282}
283
284fn is_valid_stable_id(id: &str) -> bool {
285    if id.is_empty() {
286        return false;
287    }
288    id.bytes().all(|b| {
289        b.is_ascii_lowercase() || b.is_ascii_digit() || b == b'.' || b == b'_' || b == b'-'
290    })
291}
292
293#[cfg(test)]
294mod tests {
295    use super::{
296        BlockerCode, CoverageBlocker, CoverageEvidence, CoverageRow, CoverageRowType,
297        CoverageStatus, LEAN_COVERAGE_SCHEMA_VERSION, LeanCoverageMatrix,
298    };
299
300    fn valid_matrix() -> LeanCoverageMatrix {
301        LeanCoverageMatrix {
302            schema_version: LEAN_COVERAGE_SCHEMA_VERSION.to_string(),
303            matrix_id: "lean.coverage.v1".to_string(),
304            title: "Lean Coverage".to_string(),
305            scope: "Spec to implementation coverage".to_string(),
306            rows: vec![
307                CoverageRow {
308                    id: "sem.cancel.request.wf".to_string(),
309                    title: "cancel request preserves wf".to_string(),
310                    row_type: CoverageRowType::SemanticRule,
311                    status: CoverageStatus::ValidatedInCi,
312                    description: "requestCancel branch preserves well-formedness".to_string(),
313                    owner: Some("MagentaBridge".to_string()),
314                    depends_on: vec![],
315                    tags: vec!["cancel".to_string()],
316                    blocker: None,
317                    evidence: vec![CoverageEvidence {
318                        theorem_name: Some("requestCancel_preserves_wf".to_string()),
319                        file_path: Some("formal/lean/Asupersync.lean".to_string()),
320                        line: Some(2321),
321                        proof_artifact: Some("target/lean-e2e/manifest.json".to_string()),
322                        ci_job: Some("proof-checks".to_string()),
323                        reviewer: Some("FoggyMarsh".to_string()),
324                    }],
325                },
326                CoverageRow {
327                    id: "inv.no_obligation_leak".to_string(),
328                    title: "No obligation leaks".to_string(),
329                    row_type: CoverageRowType::Invariant,
330                    status: CoverageStatus::Blocked,
331                    description: "No leaked obligations after close".to_string(),
332                    owner: None,
333                    depends_on: vec!["sem.cancel.request.wf".to_string()],
334                    tags: vec![],
335                    blocker: Some(CoverageBlocker {
336                        code: BlockerCode::ProofMissingLemma,
337                        detail: "Need helper lemma for resolve obligation map".to_string(),
338                    }),
339                    evidence: vec![],
340                },
341            ],
342        }
343    }
344
345    #[test]
346    fn valid_matrix_passes_validation() {
347        let matrix = valid_matrix();
348        assert!(matrix.validate().is_ok());
349    }
350
351    #[test]
352    fn duplicate_ids_fail_validation() {
353        let mut matrix = valid_matrix();
354        matrix.rows[1].id = matrix.rows[0].id.clone();
355        let errors = matrix.validate().expect_err("should fail");
356        assert!(errors.iter().any(|e| e.contains("duplicate row id")));
357    }
358
359    #[test]
360    fn missing_dependency_fails_validation() {
361        let mut matrix = valid_matrix();
362        matrix.rows[1].depends_on = vec!["missing.row.id".to_string()];
363        let errors = matrix.validate().expect_err("should fail");
364        assert!(
365            errors
366                .iter()
367                .any(|e| e.contains("depends_on missing row id"))
368        );
369    }
370
371    #[test]
372    fn blocked_requires_blocker_payload() {
373        let mut matrix = valid_matrix();
374        matrix.rows[1].blocker = None;
375        let errors = matrix.validate().expect_err("should fail");
376        assert!(errors.iter().any(|e| e.contains("missing blocker payload")));
377    }
378
379    #[test]
380    fn validated_in_ci_requires_ci_job_evidence() {
381        let mut matrix = valid_matrix();
382        matrix.rows[0].evidence[0].ci_job = None;
383        let errors = matrix.validate().expect_err("should fail");
384        assert!(
385            errors
386                .iter()
387                .any(|e| e.contains("validated-in-ci but has no ci_job"))
388        );
389    }
390}
asupersync_conformance/lean_coverage_matrix.rs

asupersync_conformance/
lean_coverage_matrix.rs
