provable_contracts/discharge/
summary.rs

1//! PVL-001 EV-8a (#4202) — `discharge-summary.json`, the one summary the tree can carry.
2//!
3//! `pv discharge run <lean-dir>` writes it as a SIBLING of `<lean-dir>` (`<staging-crate>/discharge-summary.json`),
4//! never inside it: a file inside the tree it hashes cannot carry that tree's sha, its own bytes being an input to
5//! it. It holds no timestamp and no commit sha, so a re-run over the same tree reproduces it byte for byte and a
6//! squash merge keeps it valid (`tree_sha` is `git rev-parse HEAD:<lean-dir>`, content-addressed). It is written
7//! on failure too: a RED run is a summary with RED fields, never a missing file.
8//!
9//! Its one consumer here is the `proved-is-derived` lint gate: a YAML `lean.status: proved` claim is DERIVED only
10//! when a GREEN summary lists its theorem. The summary is a claim until EV-9's job regenerates it and diffs
11//! (summary-fresh); a hand edit toward pass is caught there, not here.
12
13use std::collections::{BTreeMap, BTreeSet};
14use std::path::{Path, PathBuf};
15
16use serde::{Deserialize, Serialize};
17
18use super::{escapes, is_theorem, Report, Tree};
19
20/// The tracked summary's file name, beside `<lean-dir>`.
21pub const SUMMARY_FILE: &str = "discharge-summary.json";
22/// The full log's file name, inside `<lean-dir>`: untracked (`.gitignore`d).
23pub const LOG_FILE: &str = "discharge.json";
24
25/// One module the check covered: a file in the root's import cone.
26#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
27pub struct Module {
28    /// Relative to `<lean-dir>`.
29    pub path: String,
30    /// blake3 of the file's bytes, 64 hex digits.
31    pub blake3: String,
32    /// Its public theorems whose own declaration holds no escape (`sorry`, `admit`, …), as full names.
33    pub theorems: Vec<String>,
34}
35
36/// `discharge-summary.json`. Field order is the file's; `None` is `null` (the step never ran).
37#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
38pub struct Summary {
39    /// `git rev-parse HEAD:<lean-dir>`.
40    pub tree_sha: Option<String>,
41    /// `<lean-dir>/lean-toolchain`, trimmed.
42    pub toolchain: Option<String>,
43    /// The `mathlib` package's `rev` in `<lean-dir>/lake-manifest.json`.
44    pub mathlib_rev: Option<String>,
45    /// `build.sh`'s exit (rc 2 is its cache-miss decline). The Lean steps run only after a 0.
46    pub build_exit: Option<i32>,
47    /// `lake env lean Axioms.lean`.
48    pub lake_exit: Option<i32>,
49    /// `lake env leanchecker ProvableContracts` (124/137 on a timeout).
50    pub leanchecker_exit: Option<i32>,
51    /// `Axioms.lean` is its regeneration AND elaborated with rc 0.
52    pub axioms_ok: bool,
53    /// The escape scan, `--strict`, found nothing unlisted, stale, malformed or pending.
54    pub escapes_ok: bool,
55    /// `n/m` challenges the comparator closed; `None` when it never judged a row set.
56    pub challenges_closed: Option<String>,
57    /// The modules in the root's import cone, by path.
58    pub modules: Vec<Module>,
59}
60
61impl Summary {
62    /// Every Lean step ran and passed. Only a green summary derives anything.
63    #[must_use]
64    pub fn is_green(&self) -> bool {
65        self.build_exit == Some(0)
66            && self.lake_exit == Some(0)
67            && self.leanchecker_exit == Some(0)
68            && self.axioms_ok
69            && self.escapes_ok
70    }
71
72    /// The theorems this summary derives: every listed one when green, none otherwise.
73    #[must_use]
74    pub fn derived(&self) -> BTreeSet<&str> {
75        if !self.is_green() {
76            return BTreeSet::new();
77        }
78        self.modules
79            .iter()
80            .flat_map(|m| m.theorems.iter().map(String::as_str))
81            .collect()
82    }
83
84    /// The file's bytes: pretty JSON and a trailing newline, so a regeneration diffs clean.
85    #[must_use]
86    pub fn render(&self) -> String {
87        let mut s = serde_json::to_string_pretty(self)
88            .unwrap_or_else(|e| format!("{{\"error\": {:?}}}", e.to_string()));
89        s.push('\n');
90        s
91    }
92}
93
94/// `<lean-dir>`'s sibling `discharge-summary.json` (`${LEAN%/lean}/discharge-summary.json`).
95#[must_use]
96pub fn summary_path(lean_dir: &Path) -> PathBuf {
97    // `Path::new("").join(f)` is `f`: a bare `lean` (parent "") and a root (no parent) need no arm of their own.
98    lean_dir
99        .parent()
100        .unwrap_or_else(|| Path::new(""))
101        .join(SUMMARY_FILE)
102}
103
104/// Read a summary. `Err` names why (absent, unreadable, not a summary); the gate reads any `Err` as "derives nothing".
105pub fn load(path: &Path) -> Result<Summary, String> {
106    let raw = std::fs::read_to_string(path).map_err(|e| format!("{}: {e}", path.display()))?;
107    serde_json::from_str(&raw)
108        .map_err(|e| format!("{}: not a discharge summary: {e}", path.display()))
109}
110
111/// Does `derived` hold the claim's `lean.theorem`? The YAML names it exactly or without the `ProvableContracts.`
112/// root namespace (`Softmax.partition_of_unity` for `ProvableContracts.Softmax.partition_of_unity`); nothing looser.
113#[must_use]
114pub fn claim_derived(derived: &BTreeSet<&str>, theorem: &str) -> bool {
115    derived.contains(theorem) || derived.contains(format!("ProvableContracts.{theorem}").as_str())
116}
117
118/// The modules the root's import cone reaches, each with its blake3 and its escape-free public theorems. A file
119/// that cannot be read is listed with an empty hash: the summary records it, and it derives nothing.
120#[must_use]
121pub fn modules(tree: &Tree) -> Vec<Module> {
122    let cone = tree.cone();
123    let escaped: BTreeSet<(String, String)> = escapes(tree)
124        .into_iter()
125        .map(|e| (e.file, e.decl))
126        .collect();
127    let mut out: Vec<Module> = tree
128        .files
129        .iter()
130        .filter(|f| cone.contains(&f.module))
131        .map(|f| {
132            let bytes = std::fs::read(tree.dir.join(&f.rel));
133            let (blake3, readable) = match &bytes {
134                Ok(b) => (blake3::hash(b).to_hex().to_string(), true),
135                Err(_) => (String::new(), false),
136            };
137            let theorems = f
138                .decls
139                .iter()
140                .filter(|d| readable && is_theorem(d))
141                .filter(|d| !escaped.contains(&(f.rel.clone(), d.fqn.clone())))
142                .map(|d| d.fqn.clone())
143                .collect();
144            Module {
145                path: f.rel.clone(),
146                blake3,
147                theorems,
148            }
149        })
150        .collect();
151    out.sort_by(|a, b| a.path.cmp(&b.path));
152    out
153}
154
155/// `toolchain` and `mathlib_rev` from `<lean-dir>`'s own files.
156#[must_use]
157pub fn pins(lean_dir: &Path) -> (Option<String>, Option<String>) {
158    let toolchain = std::fs::read_to_string(lean_dir.join("lean-toolchain"))
159        .ok()
160        .map(|s| s.trim().to_string())
161        .filter(|s| !s.is_empty());
162    let mathlib = std::fs::read_to_string(lean_dir.join("lake-manifest.json"))
163        .ok()
164        .and_then(|raw| serde_json::from_str::<serde_json::Value>(&raw).ok())
165        .and_then(|doc| {
166            doc.get("packages")?
167                .as_array()?
168                .iter()
169                .find(|p| p.get("name").and_then(|n| n.as_str()) == Some("mathlib"))?
170                .get("rev")?
171                .as_str()
172                .map(str::to_string)
173        });
174    (toolchain, mathlib)
175}
176
177/// The summary of one run: `r` is the finished report (Lean steps included), `tree` the tree it judged (`None`
178/// when it could not be loaded — no module is then listed).
179#[must_use]
180pub fn summarize(
181    r: &Report,
182    tree: Option<&Tree>,
183    lean_dir: &Path,
184    tree_sha: Option<String>,
185    build_exit: Option<i32>,
186) -> Summary {
187    let (toolchain, mathlib_rev) = pins(lean_dir);
188    Summary {
189        tree_sha,
190        toolchain,
191        mathlib_rev,
192        build_exit,
193        lake_exit: r.lake_exit,
194        leanchecker_exit: r.leanchecker_exit,
195        axioms_ok: r.axioms_fresh == Some(true) && r.lake_exit == Some(0),
196        escapes_ok: r.escapes_ok == Some(true),
197        challenges_closed: r.challenges.map(|c| format!("{}/{}", c.closed, c.total)),
198        modules: tree.map(modules).unwrap_or_default(),
199    }
200}
201
202/// Where L4 credit comes from (EV-8b): a discharge summary beside the Lean base, or — with none to read — the
203/// ONT-2a scan of the tree's own `.lean` text, which the report labels `self-declared`.
204#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)]
205#[serde(rename_all = "kebab-case")]
206pub enum L4Source {
207    Discharge,
208    #[default]
209    SelfDeclared,
210}
211
212/// What a summary grants: the theorems it discharges, or none and the first reason why.
213#[derive(Debug, Clone, Default, PartialEq, Eq)]
214pub struct Discharged {
215    pub theorems: BTreeSet<String>,
216    /// `None` when the summary grants; otherwise why it grants nothing (`stale discharge`, `lake_exit 1`, …).
217    pub withheld: Option<String>,
218    /// Discharged theorems ONT-3b (#4073) dropped because no L4 model covers their module.
219    pub unrefined: BTreeSet<String>,
220    /// Every theorem the summary lists, by the module that proves it.
221    pub module_of: BTreeMap<String, String>,
222}
223
224impl Discharged {
225    /// Does this grant the equation's `lean_theorem`? Same naming rule as [`claim_derived`].
226    #[must_use]
227    pub fn grants(&self, theorem: &str) -> bool {
228        let t = theorem.trim().trim_matches('"');
229        self.theorems.contains(t) || self.theorems.contains(&format!("ProvableContracts.{t}"))
230    }
231
232    /// ONT-3b (#4073): keep only the theorems whose module an L4 model covers (`extraction`/`simulation`, resolving
233    /// `model_of`). The rest move to `unrefined`: discharged, but nothing ties the statement to the Rust.
234    pub fn require_refinement(&mut self, l4_modules: &BTreeSet<String>) {
235        let (kept, dropped) = std::mem::take(&mut self.theorems)
236            .into_iter()
237            .partition(|t| {
238                self.module_of
239                    .get(t)
240                    .is_some_and(|m| l4_modules.contains(m))
241            });
242        self.theorems = kept;
243        self.unrefined = dropped;
244    }
245}
246
247/// `n/m` with `n == m` and `m > 0`: every pinned statement was compared and closed.
248fn all_challenges_closed(closed: Option<&str>) -> bool {
249    let Some((n, m)) = closed.and_then(|c| c.split_once('/')) else {
250        return false;
251    };
252    matches!((n.trim().parse::<u32>(), m.trim().parse::<u32>()), (Ok(n), Ok(m)) if m > 0 && n == m)
253}
254
255/// L4 credit from a summary: its theorems, only when every Lean step exited 0, its `tree_sha` is the CURRENT Lean
256/// tree's, and every challenge closed. Anything else grants nothing, and says why — a stale or red summary is the
257/// andon, never a partial credit.
258#[must_use]
259pub fn discharged(s: &Summary, current_tree_sha: Option<&str>) -> Discharged {
260    let withheld = if s.tree_sha.is_none() || s.tree_sha.as_deref() != current_tree_sha {
261        Some(format!(
262            "stale discharge: summary tree_sha {} != current lean tree {}",
263            s.tree_sha.as_deref().unwrap_or("null"),
264            current_tree_sha.unwrap_or("unknown")
265        ))
266    } else if !s.is_green() {
267        Some(format!(
268            "red discharge: build_exit {:?}, lake_exit {:?}, leanchecker_exit {:?}, axioms_ok {}, escapes_ok {}",
269            s.build_exit, s.lake_exit, s.leanchecker_exit, s.axioms_ok, s.escapes_ok
270        ))
271    } else if !all_challenges_closed(s.challenges_closed.as_deref()) {
272        Some(format!(
273            "challenges not closed: {}",
274            s.challenges_closed.as_deref().unwrap_or("never judged")
275        ))
276    } else {
277        None
278    };
279    let theorems = if withheld.is_none() {
280        s.derived().into_iter().map(str::to_string).collect()
281    } else {
282        BTreeSet::new()
283    };
284    let module_of = s
285        .modules
286        .iter()
287        .flat_map(|m| m.theorems.iter().map(|t| (t.clone(), m.path.clone())))
288        .collect();
289    Discharged {
290        theorems,
291        withheld,
292        unrefined: BTreeSet::new(),
293        module_of,
294    }
295}
296
297/// `git rev-parse HEAD:./` in `lean_dir`: the tree a fresh summary must name. `None` outside a git checkout, or
298/// when the dir is not in HEAD.
299#[must_use]
300pub fn current_tree_sha(lean_dir: &Path) -> Option<String> {
301    let o = std::process::Command::new("git")
302        .args(["rev-parse", "HEAD:./"])
303        .current_dir(lean_dir)
304        .output()
305        .ok()?;
306    let sha = String::from_utf8_lossy(&o.stdout).trim().to_string();
307    (o.status.success() && !sha.is_empty()).then_some(sha)
308}
309
310#[cfg(test)]
311#[path = "summary_tests.rs"]
312mod tests;
provable_contracts/discharge/summary.rs

provable_contracts/discharge/
summary.rs
