provable_contracts/discharge/
refinement.rs

1//! ONT-001 ONT-3b (#4073) — refinement: a Lean module earns L4 only when `formalization.yaml` names the Rust item it
2//! models (`model_of`), that item resolves in the workspace (ONT-3a's `syn` walk), the module's theorems are
3//! discharged (PVL-001 EV-8b), and the relation is `extraction` or `simulation`. `test_witnessed` earns L3. A
4//! statement with no model earns no L4: that closes PVL F5, "nothing checks the Rust implements what Lean proves".
5//!
6//! ```yaml
7//! models:
8//!   - module: ProvableContracts/Theorems/Softmax/Kernel.lean   # relative to the lean dir, as the summary lists it
9//!     model_of: trueno::softmax::softmax_row                   # a Rust path the workspace resolves
10//!     relation: { kind: extraction, evidence: "how the Lean model was obtained from the Rust" }
11//! ```
12
13use std::collections::{BTreeMap, BTreeSet};
14use std::path::Path;
15
16/// How the Lean model relates to the Rust item.
17#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
18pub enum Kind {
19    /// The Lean definition was extracted from the Rust (e.g. Aeneas/Charon).
20    Extraction,
21    /// A simulation proof relates the Lean model to the Rust semantics.
22    Simulation,
23    /// Only tests witness the correspondence.
24    TestWitnessed,
25}
26
27impl Kind {
28    #[must_use]
29    pub fn parse(s: &str) -> Option<Self> {
30        match s {
31            "extraction" => Some(Self::Extraction),
32            "simulation" => Some(Self::Simulation),
33            "test_witnessed" => Some(Self::TestWitnessed),
34            _ => None,
35        }
36    }
37
38    /// The highest verification level this relation can earn (spec Q1 default).
39    #[must_use]
40    pub fn level(self) -> u8 {
41        match self {
42            Self::Extraction | Self::Simulation => 4,
43            Self::TestWitnessed => 3,
44        }
45    }
46
47    #[must_use]
48    pub fn as_str(self) -> &'static str {
49        match self {
50            Self::Extraction => "extraction",
51            Self::Simulation => "simulation",
52            Self::TestWitnessed => "test_witnessed",
53        }
54    }
55}
56
57/// One `models:` entry.
58#[derive(Debug, Clone, PartialEq, Eq)]
59pub struct Model {
60    pub module: String,
61    pub model_of: String,
62    pub kind: Kind,
63    pub evidence: String,
64}
65
66/// `formalization.yaml`'s refinement record: the well-formed models, what was malformed, and the baseline.
67#[derive(Debug, Clone, Default, PartialEq, Eq)]
68pub struct Record {
69    pub models: Vec<Model>,
70    pub malformed: Vec<String>,
71    pub unrefined_baseline: Option<usize>,
72}
73
74/// Read `<lean_dir>/formalization.yaml`'s `models` and `unrefined_baseline`. `Err` only when the file is unreadable.
75pub fn load(lean_dir: &Path) -> Result<Record, String> {
76    let p = lean_dir.join("formalization.yaml");
77    let text = std::fs::read_to_string(&p).map_err(|e| format!("{}: {e}", p.display()))?;
78    let doc: serde_yaml::Value =
79        serde_yaml::from_str(&text).map_err(|e| format!("{}: {e}", p.display()))?;
80    Ok(parse(&doc))
81}
82
83fn parse(doc: &serde_yaml::Value) -> Record {
84    let mut rec = Record {
85        unrefined_baseline: doc
86            .get("unrefined_baseline")
87            .and_then(serde_yaml::Value::as_u64)
88            .and_then(|n| usize::try_from(n).ok()),
89        ..Record::default()
90    };
91    let entries = doc
92        .get("models")
93        .and_then(serde_yaml::Value::as_sequence)
94        .cloned()
95        .unwrap_or_default();
96    let mut seen = BTreeSet::new();
97    for (i, e) in entries.iter().enumerate() {
98        let s = |k: &str| e.get(k).and_then(serde_yaml::Value::as_str).map(str::trim);
99        let rel = |k: &str| {
100            e.get("relation")
101                .and_then(|r| r.get(k))
102                .and_then(serde_yaml::Value::as_str)
103                .map(str::trim)
104        };
105        let (Some(module), Some(model_of)) = (s("module"), s("model_of")) else {
106            rec.malformed
107                .push(format!("models[{i}] needs `module` and `model_of`"));
108            continue;
109        };
110        let Some(kind) = rel("kind").and_then(Kind::parse) else {
111            rec.malformed.push(format!(
112                "models[{i}] ({module}): relation.kind {:?} is not extraction, simulation or test_witnessed",
113                rel("kind")
114            ));
115            continue;
116        };
117        let evidence = rel("evidence").unwrap_or_default();
118        if module.is_empty() || !model_of.contains("::") || evidence.is_empty() {
119            rec.malformed.push(format!(
120                "models[{i}] ({module}): needs a module, a `crate::path::item` model_of and relation.evidence"
121            ));
122            continue;
123        }
124        if !seen.insert(module.to_string()) {
125            rec.malformed
126                .push(format!("models[{i}]: {module} is modelled twice"));
127            continue;
128        }
129        rec.models.push(Model {
130            module: module.into(),
131            model_of: model_of.into(),
132            kind,
133            evidence: evidence.into(),
134        });
135    }
136    rec
137}
138
139/// One model, judged.
140#[derive(Debug, Clone, PartialEq, Eq)]
141pub struct Judged {
142    pub model: Model,
143    /// `Err(why)`: `model_of` names no workspace item (a ghost formalization).
144    pub resolved: Result<(), String>,
145    /// The module is one the discharge summary lists.
146    pub in_tree: bool,
147}
148
149impl Judged {
150    /// The level this model grants its module: none unless it resolves and names a module in the tree.
151    #[must_use]
152    pub fn level(&self) -> Option<u8> {
153        (self.resolved.is_ok() && self.in_tree).then(|| self.model.kind.level())
154    }
155}
156
157/// Judge every model. `resolve` answers for a Rust path (`crate::module::item`); `tree_modules` are the summary's paths.
158pub fn judge(
159    models: &[Model],
160    tree_modules: &BTreeSet<String>,
161    mut resolve: impl FnMut(&str) -> Result<(), String>,
162) -> Vec<Judged> {
163    models
164        .iter()
165        .map(|m| Judged {
166            resolved: resolve(&m.model_of),
167            in_tree: tree_modules.contains(&m.module),
168            model: m.clone(),
169        })
170        .collect()
171}
172
173/// The modules whose model earns L4.
174#[must_use]
175pub fn l4_modules(judged: &[Judged]) -> BTreeSet<String> {
176    judged
177        .iter()
178        .filter(|j| j.level() == Some(4))
179        .map(|j| j.model.module.clone())
180        .collect()
181}
182
183/// The theorem-bearing modules (`module -> theorems`) that no L4 model covers.
184#[must_use]
185pub fn unrefined<'a>(
186    theorem_modules: &'a BTreeMap<String, Vec<String>>,
187    l4: &BTreeSet<String>,
188) -> Vec<&'a str> {
189    theorem_modules
190        .iter()
191        .filter(|(m, ts)| !ts.is_empty() && !l4.contains(*m))
192        .map(|(m, _)| m.as_str())
193        .collect()
194}
195
196/// A resolver over the workspace at `root` (ONT-3a's walk), as the closure [`judge`] takes.
197pub fn workspace_resolver(root: &Path) -> impl FnMut(&str) -> Result<(), String> {
198    let ws = crate::ontology::extract::code::Workspace::scan(root);
199    let mut cache: BTreeMap<String, Result<(), String>> = BTreeMap::new();
200    move |path: &str| {
201        cache
202            .entry(path.to_string())
203            .or_insert_with(|| {
204                let Some((module, item)) = path.rsplit_once("::") else {
205                    return Err(format!("`{path}` is not a crate::path::item"));
206                };
207                let mut r = crate::ontology::extract::code::Resolver::new(&ws);
208                r.resolve(module, item).map(|_| ()).map_err(|u| u.reason)
209            })
210            .clone()
211    }
212}
213
214#[cfg(test)]
215#[path = "refinement_tests.rs"]
216mod tests;
provable_contracts/discharge/refinement.rs

provable_contracts/discharge/
refinement.rs
