provable_contracts/ontology/extract/
lean.rs

1//! ONT-001 §3.7, §5 ONT-4b2 — `extract:lean`: the in-tree Lean theorems become `ont:Statement` nodes.
2//!
3//! The focus objects are the `theorem` declarations under `<lean base>/ProvableContracts/Theorems/<Domain>/*.lean`
4//! — the same files, the same `sorry` rule and the same name forms ONT-2a's grounding scan reads
5//! ([`crate::proof_status`]), so what the graph says about a theorem and what `proof-status` credits agree by
6//! construction. The base is the first of [`crate::proof_status::LEAN_THEOREM_BASES`] that exists under the
7//! repo root (the contract dir's parent), never the process cwd.
8//!
9//! Each statement carries `lean:name`, `lean:domain`, `lean:file`, `lean:module`, `lean:sorryFree` (a FILE with
10//! `sorry` grounds nothing — an admitted proof is not a proof, ONT-2a) and `lean:discharge` (`grounded` |
11//! `admitted`). `lean:modelOf` → `contract/<stem>` for every contract whose `lean_theorem:` reference (in
12//! `equations.*` or `proof_obligations[]`) names this theorem, its file or its domain in one of ONT-2a's accepted
13//! forms — the reference is the contract's own text, matched, never inferred. A reference matching nothing is
14//! counted (`refs_unresolved`) so a shape can require every claimed theorem to exist; PVL-001's
15//! `formalization.yaml` (`relation.kind`, capstones) is not read here — it does not exist in this tree yet, and
16//! the row that lands it extends this reader.
17//!
18//! IRI: `https://ont.paiml.dev/v1alpha1/world/<Domain>.<File>.<theorem>`. No blank nodes; byte-ordered walk.
19
20use std::collections::{BTreeMap, BTreeSet};
21use std::path::{Path, PathBuf};
22
23use crate::ontology::rdf::{iri, ont, Graph, Term, PROV_ENTITY, RDF_TYPE};
24use crate::proof_status::{camel_case, first_camel_word, LEAN_THEOREM_BASES};
25
26/// A `lean:*` vocabulary term.
27#[must_use]
28pub fn lean(name: &str) -> String {
29    ont(&format!("lean/{name}"))
30}
31
32/// One `theorem` declaration.
33#[derive(Debug, Clone, PartialEq, Eq)]
34pub struct Statement {
35    pub domain: String,
36    pub stem: String,
37    pub name: String,
38    /// Repo-relative file.
39    pub file: String,
40    pub sorry_free: bool,
41}
42
43impl Statement {
44    /// `ProvableContracts.Theorems.<Domain>.<File>`.
45    #[must_use]
46    pub fn module(&self) -> String {
47        format!("ProvableContracts.Theorems.{}.{}", self.domain, self.stem)
48    }
49
50    /// The names a contract may cite this theorem by — the forms ONT-2a's scan registers for its theorem, its
51    /// file and its domain.
52    #[must_use]
53    pub fn accepted_names(&self) -> BTreeSet<String> {
54        let mut names = BTreeSet::new();
55        for label in [self.domain.as_str(), self.stem.as_str()] {
56            names.insert(format!("Theorems.{label}"));
57            names.insert(label.to_string());
58            names.insert(label.to_lowercase());
59        }
60        let camel = camel_case(&self.name);
61        names.insert(format!("Theorems.{camel}"));
62        names.insert(camel.clone());
63        let first = first_camel_word(&camel);
64        if first.len() >= 3 {
65            names.insert(format!("Theorems.{first}"));
66            names.insert(first);
67        }
68        names
69    }
70}
71
72/// Counts reported beside the graph.
73#[derive(Debug, Clone, Default, PartialEq, Eq)]
74pub struct LeanStats {
75    /// The base directory used, repo-relative; `None` when no base exists (no `lean` triples, by measurement).
76    pub base: Option<String>,
77    pub files: usize,
78    pub statements: usize,
79    pub sorry_free: usize,
80    /// Statements with at least one `lean:modelOf` edge.
81    pub modeled: usize,
82    /// `(contract stem, reference)` pairs that name no theorem, file or domain in the tree.
83    pub refs_unresolved: Vec<(String, String)>,
84}
85
86/// The first Lean base that exists under `root`.
87#[must_use]
88pub fn base_under(root: &Path) -> Option<PathBuf> {
89    LEAN_THEOREM_BASES
90        .iter()
91        .map(|b| root.join(b))
92        .find(|p| p.join("ProvableContracts/Theorems").is_dir())
93}
94
95/// Every `theorem <name>` in one file's text, in order.
96#[must_use]
97pub fn theorems_in(content: &str) -> Vec<String> {
98    let mut out = Vec::new();
99    for line in content.lines() {
100        let Some(pos) = line.find("theorem ") else {
101            continue;
102        };
103        let name: String = line[pos + 8..]
104            .chars()
105            .take_while(|c| c.is_alphanumeric() || *c == '_')
106            .collect();
107        if !name.is_empty() {
108            out.push(name);
109        }
110    }
111    out
112}
113
114/// The statements of one file.
115#[must_use]
116pub fn statements_of(domain: &str, stem: &str, rel: &str, content: &str) -> Vec<Statement> {
117    let sorry_free = !content.contains("sorry");
118    theorems_in(content)
119        .into_iter()
120        .map(|name| Statement {
121            domain: domain.to_string(),
122            stem: stem.to_string(),
123            name,
124            file: rel.to_string(),
125            sorry_free,
126        })
127        .collect()
128}
129
130/// Walk `<base>/ProvableContracts/Theorems/<Domain>/*.lean` in byte order.
131fn walk(root: &Path, base: &Path, stats: &mut LeanStats) -> Vec<Statement> {
132    let theorems = base.join("ProvableContracts/Theorems");
133    let mut domains: Vec<PathBuf> = std::fs::read_dir(&theorems)
134        .map(|rd| {
135            rd.flatten()
136                .map(|e| e.path())
137                .filter(|p| p.is_dir())
138                .collect()
139        })
140        .unwrap_or_default();
141    domains.sort();
142    let mut out = Vec::new();
143    for domain_dir in domains {
144        let domain = domain_dir
145            .file_name()
146            .unwrap_or_default()
147            .to_string_lossy()
148            .to_string();
149        let mut files: Vec<PathBuf> = std::fs::read_dir(&domain_dir)
150            .map(|rd| {
151                rd.flatten()
152                    .map(|e| e.path())
153                    .filter(|p| p.extension().is_some_and(|e| e == "lean"))
154                    .collect()
155            })
156            .unwrap_or_default();
157        files.sort();
158        for file in files {
159            let Ok(content) = std::fs::read_to_string(&file) else {
160                continue;
161            };
162            stats.files += 1;
163            let stem = file
164                .file_stem()
165                .unwrap_or_default()
166                .to_string_lossy()
167                .to_string();
168            let rel = file
169                .strip_prefix(root)
170                .unwrap_or(&file)
171                .to_string_lossy()
172                .replace('\\', "/");
173            out.extend(statements_of(&domain, &stem, &rel, &content));
174        }
175    }
176    out
177}
178
179/// Every `lean_theorem:` reference a contract document makes, from `equations.*` and `proof_obligations[]`,
180/// trimmed of quotes; `none` and empty are not references.
181#[must_use]
182pub fn references_of(doc: &serde_yaml::Value) -> Vec<String> {
183    let mut refs = Vec::new();
184    let mut push = |v: Option<&serde_yaml::Value>| {
185        if let Some(s) = v.and_then(serde_yaml::Value::as_str) {
186            let s = s.trim().trim_matches('"');
187            if !s.is_empty() && s != "none" && !s.starts_with("none ") {
188                refs.push(s.to_string());
189            }
190        }
191    };
192    if let Some(eqs) = doc.get("equations").and_then(serde_yaml::Value::as_mapping) {
193        for (_, eq) in eqs {
194            push(eq.get("lean_theorem"));
195        }
196    }
197    if let Some(obs) = doc
198        .get("proof_obligations")
199        .and_then(serde_yaml::Value::as_sequence)
200    {
201        for ob in obs {
202            push(ob.get("lean_theorem"));
203        }
204    }
205    refs.sort();
206    refs.dedup();
207    refs
208}
209
210/// A reference matches a statement when one of the statement's accepted names equals the reference, the
211/// reference without `Theorems.`, or the reference lowercased — ONT-2a's three tries.
212#[must_use]
213pub fn reference_matches(reference: &str, accepted: &BTreeSet<String>) -> bool {
214    accepted.contains(reference)
215        || accepted.contains(reference.strip_prefix("Theorems.").unwrap_or(reference))
216        || accepted.contains(&reference.to_lowercase())
217}
218
219/// The statement IRI.
220#[must_use]
221pub fn statement_iri(s: &Statement) -> String {
222    iri("world", &format!("{}.{}.{}", s.domain, s.stem, s.name))
223}
224
225/// One statement into `g`, with its `modelOf` edges.
226pub fn emit(g: &mut Graph, s: &Statement, model_of: &[String]) {
227    let n = statement_iri(s);
228    g.insert(n.clone(), RDF_TYPE, Term::iri(ont("Statement")));
229    g.insert(n.clone(), RDF_TYPE, Term::iri(PROV_ENTITY));
230    g.insert(n.clone(), lean("name"), Term::string(&s.name));
231    g.insert(n.clone(), lean("domain"), Term::string(&s.domain));
232    g.insert(n.clone(), lean("file"), Term::string(&s.file));
233    g.insert(n.clone(), lean("module"), Term::string(s.module()));
234    g.insert(n.clone(), lean("sorryFree"), Term::boolean(s.sorry_free));
235    g.insert(
236        n.clone(),
237        lean("discharge"),
238        Term::string(if s.sorry_free { "grounded" } else { "admitted" }),
239    );
240    for stem in model_of {
241        g.insert(n.clone(), lean("modelOf"), Term::iri(iri("contract", stem)));
242    }
243}
244
245/// The statements of the tree under `contract_dir`'s parent, joined to the contracts that cite them, into `g`.
246pub fn extract(contract_dir: &Path, g: &mut Graph) -> LeanStats {
247    let root_buf = super::repo_root(contract_dir);
248    let root = root_buf.as_path();
249    let mut stats = LeanStats::default();
250    let Some(base) = base_under(root) else {
251        return stats;
252    };
253    stats.base = Some(
254        base.strip_prefix(root)
255            .unwrap_or(&base)
256            .to_string_lossy()
257            .replace('\\', "/"),
258    );
259    let statements = walk(root, &base, &mut stats);
260    let accepted: Vec<BTreeSet<String>> =
261        statements.iter().map(Statement::accepted_names).collect();
262    // contract stem → its references; reference → the statements it names
263    let mut model_of: BTreeMap<usize, BTreeSet<String>> = BTreeMap::new();
264    for (stem, _rel, doc) in super::pv_contract::documents(contract_dir) {
265        for reference in references_of(&doc) {
266            let mut hit = false;
267            for (i, names) in accepted.iter().enumerate() {
268                if reference_matches(&reference, names) {
269                    model_of.entry(i).or_default().insert(stem.clone());
270                    hit = true;
271                }
272            }
273            if !hit {
274                stats.refs_unresolved.push((stem.clone(), reference));
275            }
276        }
277    }
278    for (i, s) in statements.iter().enumerate() {
279        let contracts: Vec<String> = model_of
280            .get(&i)
281            .map(|set| set.iter().cloned().collect())
282            .unwrap_or_default();
283        stats.statements += 1;
284        if s.sorry_free {
285            stats.sorry_free += 1;
286        }
287        if !contracts.is_empty() {
288            stats.modeled += 1;
289        }
290        emit(g, s, &contracts);
291    }
292    stats
293}
294
295/// Positive control (`pc_extract.lean`, in memory every gate run): a file with `sorry` must ground nothing, a
296/// file without must, and a reference that names nothing must be unresolved — a reader that credited every
297/// claim would make every self-declared L4 a Pass.
298#[must_use]
299pub fn positive_control() -> bool {
300    let admitted = statements_of(
301        "Softmax",
302        "Core",
303        "x.lean",
304        "theorem softmax_sums : True := by sorry\n",
305    );
306    let grounded = statements_of(
307        "Softmax",
308        "Core",
309        "x.lean",
310        "theorem softmax_sums : True := trivial\n",
311    );
312    let (Some(a), Some(g)) = (admitted.first(), grounded.first()) else {
313        return false;
314    };
315    let names = g.accepted_names();
316    !a.sorry_free
317        && g.sorry_free
318        && reference_matches("Theorems.Softmax", &names)
319        && reference_matches("Theorems.SoftmaxSums", &names)
320        && !reference_matches("Theorems.NothingOfTheSort", &names)
321}
322
323#[cfg(test)]
324mod tests {
325    use super::*;
326
327    #[test]
328    fn theorems_and_sorry_are_read_as_ont_2a_reads_them() {
329        let src = "namespace X\ntheorem relu_nonneg (x : Float) : True := trivial\n  theorem two_words : True := by\n  sorry\n";
330        let st = statements_of("Relu", "Core", "lean/Relu/Core.lean", src);
331        assert_eq!(st.len(), 2);
332        assert_eq!(st[0].name, "relu_nonneg");
333        assert!(
334            !st[0].sorry_free,
335            "a file with sorry grounds nothing, whatever line the sorry is on"
336        );
337        let names = st[0].accepted_names();
338        for n in [
339            "Theorems.Relu",
340            "Relu",
341            "relu",
342            "Theorems.Core",
343            "Theorems.ReluNonneg",
344            "ReluNonneg",
345        ] {
346            assert!(names.contains(n), "{n} missing from {names:?}");
347        }
348        assert!(reference_matches("Theorems.ReluNonneg", &names));
349        assert!(reference_matches("relu", &names));
350        assert!(!reference_matches("Theorems.Gelu", &names));
351    }
352
353    #[test]
354    fn references_come_from_equations_and_obligations_and_none_is_not_one() {
355        let doc: serde_yaml::Value = serde_yaml::from_str(
356            "equations:\n  a:\n    lean_theorem: Theorems.A\n  b:\n    lean_theorem: none — L4 not declared\nproof_obligations:\n  - lean_theorem: \"Theorems.B\"\n  - lean_theorem: none\n  - id: x\n",
357        )
358        .expect("yaml");
359        assert_eq!(
360            references_of(&doc),
361            vec!["Theorems.A".to_string(), "Theorems.B".to_string()]
362        );
363    }
364
365    #[test]
366    fn the_positive_control_fires() {
367        assert!(positive_control());
368    }
369
370    #[test]
371    fn a_tree_without_a_lean_base_yields_no_triples_and_says_so() {
372        let dir = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
373            .join("../../tests/fixtures/ont/relations-ok");
374        let mut g = Graph::new();
375        let stats = extract(&dir, &mut g);
376        assert_eq!(stats.base, None);
377        assert_eq!(stats.statements, 0);
378        assert!(g.is_empty());
379    }
380
381    #[test]
382    fn the_real_tree_is_extracted_deterministically_with_model_of_edges() {
383        // The repo's own Lean tree: the one witness the row has today.
384        let dir = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../contracts");
385        let mut g = Graph::new();
386        let stats = extract(&dir, &mut g);
387        assert_eq!(
388            stats.base.as_deref(),
389            Some("crates/aprender-contracts-staging/lean")
390        );
391        assert!(stats.statements > 100, "{stats:?}");
392        assert!(stats.modeled > 0, "{stats:?}");
393        let nt = g.to_ntriples();
394        assert!(nt.contains("/world/"), "{}", &nt[..200]);
395        assert!(nt.contains("lean/modelOf> <https://ont.paiml.dev/v1alpha1/contract/"));
396        assert!(!nt.contains("_:"));
397        let mut g2 = Graph::new();
398        extract(&dir, &mut g2);
399        assert_eq!(nt, g2.to_ntriples());
400    }
401}
provable_contracts/ontology/extract/lean.rs

provable_contracts/ontology/extract/
lean.rs
