logicaffeine_kernel/interface/lean/
taint.rs

1//! The taint path of every assumption a refused result rests on: the declarations through which the
2//! target reaches it.
3//!
4//! Lean's `#print axioms` (`CollectAxioms`) names the axioms a declaration rests on and says nothing
5//! of how they are reached, so a refusal that names only `sorryAx` leaves the reader to find which
6//! dependency admitted a step. This walks the checked environment along exactly the edges
7//! `CollectAxioms` follows — a definition, theorem or opaque through its statement and its body or
8//! proof, an inductive through its statement and its constructors, a constructor through its
9//! statement, an axiom never (an axiom is a leaf: the axioms its own type mentions are not reached) —
10//! breadth first, so each path is a shortest one, and it takes a declaration's references in
11//! ascending Lean-name order, so the path is a function of the environment alone. A declaration the
12//! importer introduced (a sharing helper, whose name encodes no Lean name) is walked through and
13//! never printed: the path names Lean declarations only.
14//!
15//! Only the environment is read. A path is an explanation of a refusal the assumption policy already
16//! made; it never decides one.
17
18use super::intake;
19use super::package::ALLOWED_AXIOMS;
20use super::pipeline::Diagnostic;
21use super::{DiagnosticCode, ImportedContext};
22use crate::{Context, Term};
23use std::collections::{BTreeMap, BTreeSet, HashSet, VecDeque};
24
25/// One assumption and the Lean declarations through which the target reaches it, target first and
26/// the assumption last, in Lean's spelling.
27#[derive(Clone, Debug, PartialEq, Eq)]
28pub struct TaintPath {
29    pub assumption: String,
30    pub path: Vec<String>,
31}
32
33impl TaintPath {
34    /// `T.user → T.lemma → sorryAx`.
35    pub fn render(&self) -> String {
36        self.path.join(" → ")
37    }
38}
39
40/// The receipt stage whose refusal a taint path explains.
41pub const STAGE: &str = "assumption_policy";
42
43/// The taint path of each of `assumptions` (Lean names) from `target` (a kernel name), in the order
44/// `assumptions` lists them. An assumption the target does not reach through the environment has no
45/// path and is left out.
46pub fn taint_paths(
47    imported: &ImportedContext,
48    target: &str,
49    assumptions: &[String],
50) -> Vec<TaintPath> {
51    let wanted: BTreeMap<String, &String> = assumptions
52        .iter()
53        .filter_map(|lean| intake::kernel_name(lean).ok().map(|kernel| (kernel, lean)))
54        .collect();
55    let parents = breadth_first(imported, target, &wanted.keys().cloned().collect());
56    assumptions
57        .iter()
58        .filter_map(|lean| {
59            let kernel = intake::kernel_name(lean).ok()?;
60            let mut path = vec![kernel.clone()];
61            let mut at = kernel;
62            if at != target {
63                loop {
64                    at = parents.get(&at)?.clone();
65                    path.push(at.clone());
66                    if at == target {
67                        break;
68                    }
69                }
70            }
71            path.reverse();
72            Some(TaintPath {
73                assumption: lean.clone(),
74                path: path.iter().map(|k| intake::lean_name(k)).collect(),
75            })
76        })
77        .collect()
78}
79
80/// One `disallowed_assumption` diagnostic of the assumption-policy stage per assumption outside
81/// Lean's three standard axioms that `target` (a kernel name, printed as `target_lean`) rests on,
82/// naming its taint path. `assumptions` are the result's (Lean names).
83pub fn diagnostics(
84    imported: &ImportedContext,
85    target: &str,
86    target_lean: &str,
87    assumptions: &[String],
88) -> Vec<Diagnostic> {
89    let refused: Vec<String> = assumptions
90        .iter()
91        .filter(|a| !ALLOWED_AXIOMS.iter().any(|(allowed, _)| allowed == a))
92        .cloned()
93        .collect();
94    let paths = taint_paths(imported, target, &refused);
95    refused
96        .iter()
97        .map(|assumption| {
98            let message = match paths.iter().find(|p| &p.assumption == assumption) {
99                Some(path) => format!("taint path to {assumption}: {}", path.render()),
100                None => format!(
101                    "taint path to {assumption}: none found through the checked environment, although the target's \
102                     transitive assumptions include it"
103                ),
104            };
105            Diagnostic::new(STAGE, DiagnosticCode::DisallowedAssumption, message).with_declaration(target_lean)
106        })
107        .collect()
108}
109
110/// Breadth-first search from `target` until every name of `wanted` is reached (or the environment is
111/// exhausted). Returns each reached Lean declaration's predecessor.
112fn breadth_first(
113    ctx: &ImportedContext,
114    target: &str,
115    wanted: &BTreeSet<String>,
116) -> BTreeMap<String, String> {
117    let mut parents = BTreeMap::new();
118    let mut seen: HashSet<String> = HashSet::from([target.to_string()]);
119    let mut queue = VecDeque::from([target.to_string()]);
120    let mut remaining: BTreeSet<&String> = wanted.iter().filter(|w| w.as_str() != target).collect();
121    while let Some(name) = queue.pop_front() {
122        if remaining.is_empty() {
123            break;
124        }
125        for next in lean_references(ctx, &name) {
126            if seen.insert(next.clone()) {
127                parents.insert(next.clone(), name.clone());
128                remaining.remove(&next);
129                queue.push_back(next);
130            }
131        }
132    }
133    parents
134}
135
136/// The Lean declarations `name` refers to under `CollectAxioms`' edges, walking through importer
137/// declarations that encode no Lean name, deduplicated and in ascending Lean-name order.
138fn lean_references(imported: &ImportedContext, name: &str) -> Vec<String> {
139    let mut found: BTreeMap<String, String> = BTreeMap::new();
140    let mut internal_seen: HashSet<String> = HashSet::new();
141    let mut pending = direct_references(imported, name);
142    while let Some(next) = pending.pop() {
143        if intake::components(&next).is_some() {
144            found.entry(intake::lean_name(&next)).or_insert(next);
145        } else if next != name && internal_seen.insert(next.clone()) {
146            pending.extend(direct_references(imported, &next));
147        }
148    }
149    found.into_values().collect()
150}
151
152/// The constants `name`'s own declaration mentions under `CollectAxioms`' rule.
153fn direct_references(imported: &ImportedContext, name: &str) -> Vec<String> {
154    let ctx: &Context = imported;
155    let mut out = Vec::new();
156    if let Some((ty, body)) = imported.retained(name) {
157        constants(ty, &mut out);
158        constants(body, &mut out);
159    } else if let Some((_, ty, body)) = ctx.get_universe_poly(name) {
160        constants(ty, &mut out);
161        constants(body, &mut out);
162    } else if let Some(body) = ctx.get_definition_body(name) {
163        constants(body, &mut out);
164        if let Some(ty) = ctx.get_definition_type(name) {
165            constants(ty, &mut out);
166        }
167    } else if ctx.is_inductive(name) {
168        if let Some(ty) = ctx.get_global(name) {
169            constants(ty, &mut out);
170        }
171        out.extend(
172            ctx.get_constructors(name)
173                .into_iter()
174                .map(|(constructor, _)| constructor.to_string()),
175        );
176    } else if ctx.is_constructor(name) {
177        if let Some(ty) = ctx.get_global(name) {
178            constants(ty, &mut out);
179        }
180    }
181    out
182}
183
184/// Every constant a term mentions, `Global` and `Const` alike.
185fn constants(term: &Term, out: &mut Vec<String>) {
186    let mut stack = vec![term];
187    while let Some(term) = stack.pop() {
188        match term {
189            Term::Global(name) | Term::Const { name, .. } => out.push(name.clone()),
190            Term::Sort(_) | Term::Var(_) | Term::Lit(_) | Term::Hole => {}
191            Term::Pi {
192                param_type,
193                body_type,
194                ..
195            } => stack.extend([&**param_type, &**body_type]),
196            Term::Lambda {
197                param_type, body, ..
198            } => stack.extend([&**param_type, &**body]),
199            Term::App(function, argument) => stack.extend([&**function, &**argument]),
200            Term::Match {
201                discriminant,
202                motive,
203                cases,
204            } => {
205                stack.extend([&**discriminant, &**motive]);
206                stack.extend(cases.iter());
207            }
208            Term::Fix { body, .. } => stack.push(body),
209            Term::MutualFix { defs, .. } => stack.extend(defs.iter().map(|(_, body)| body)),
210            Term::Let {
211                ty, value, body, ..
212            } => stack.extend([&**ty, &**value, &**body]),
213            Term::Annotated { term, .. } => stack.push(term),
214        }
215    }
216}
logicaffeine_kernel/interface/lean/taint.rs

logicaffeine_kernel/interface/lean/
taint.rs
