1010//! * exit non-zero → [`Verdict::Error`] (elaboration failed).
1111//! * exit 0, output mentions `sorry` → [`Verdict::Admitted`] (a hole rode
1212//! along on a green elaboration).
13- //! * exit 0, clean → [`Verdict::Unknown`] — the file elaborates, but without
14- //! a `#print axioms` audit arghda will NOT claim it proven (it could still
15- //! use `native_decide`, `sorryAx`, or other axioms). Promoting `Unknown` →
16- //! `Proven` via a per-declaration `#print axioms` audit is the follow-on.
13+ //! * exit 0, clean → run the **`#print axioms` audit** and promote honestly:
14+ //! `Proven` if every declaration depends only on the standard axioms
15+ //! (`propext`, `Classical.choice`, `Quot.sound`); `Postulated` if a
16+ //! non-standard axiom sneaks in (e.g. the one `native_decide` introduces —
17+ //! which a bare elaboration would NOT reveal); `Admitted` on `sorryAx`. If
18+ //! the audit can't run (no declarations, `lean` absent, or the file imports
19+ //! modules the bare temp-dir copy can't resolve), it stays `Verdict::Unknown`.
1720//! * binary absent → [`Verdict::Unavailable`].
1821//!
22+ //! The audit currently reaches import-free files (a temp-dir copy elaborates
23+ //! them without `LEAN_PATH`); auditing imported files needs `lake env`
24+ //! resolution — a documented follow-on.
25+ //!
1926//! Lean modules are dotted (`Mathlib.Data.Nat` ↔ `Mathlib/Data/Nat.lean`),
2027//! so [`crate::graph::module_name_of`] is reused. Imports are top-level
2128//! `import Mod` lines; Lean `open` is a *namespace* directive, not a
@@ -30,8 +37,14 @@ use anyhow::{Context, Result};
3037use std:: fs;
3138use std:: path:: { Path , PathBuf } ;
3239use std:: process:: Command ;
40+ use std:: time:: { SystemTime , UNIX_EPOCH } ;
3341use walkdir:: WalkDir ;
3442
43+ /// Lean's standard, trusted axioms — a proof depending only on these is
44+ /// sound (this is the mathlib convention). Anything else (sorryAx, or the
45+ /// axioms `native_decide` introduces) is not.
46+ const STANDARD_AXIOMS : & [ & str ] = & [ "propext" , "Classical.choice" , "Quot.sound" ] ;
47+
3548const TAIL_LINES : usize = 40 ;
3649
3750/// The Lean4 theorem prover.
@@ -63,7 +76,18 @@ impl Backend for Lean {
6376 Ok ( out) => {
6477 let mut combined = String :: from_utf8_lossy ( & out. stdout ) . into_owned ( ) ;
6578 combined. push_str ( & String :: from_utf8_lossy ( & out. stderr ) ) ;
66- let verdict = lean_verdict ( & combined, out. status . success ( ) ) ;
79+ let mut verdict = lean_verdict ( & combined, out. status . success ( ) ) ;
80+ // A clean elaboration is only `Unknown` on its own — run the
81+ // `#print axioms` audit to promote it honestly: Proven if every
82+ // declaration depends only on the standard axioms, Postulated
83+ // if a non-standard axiom (e.g. `native_decide`'s) sneaks in,
84+ // Admitted on sorryAx. If the audit can't run (imports need
85+ // lake, no declarations, tool absent) it stays `Unknown`.
86+ if verdict == Verdict :: Unknown {
87+ if let Some ( audited) = axiom_audit ( file) {
88+ verdict = audited;
89+ }
90+ }
6791 Ok ( Outcome {
6892 available : true ,
6993 exit_code : out. status . code ( ) ,
@@ -170,6 +194,124 @@ fn tail(s: &str, n: usize) -> String {
170194 lines[ start..] . join ( "\n " )
171195}
172196
197+ /// The declaration names in a Lean source that can depend on axioms
198+ /// (`theorem`/`lemma`/`def`/`abbrev`/`instance`), skipping leading
199+ /// attributes/modifiers and anonymous decls. Deliberately conservative: a
200+ /// missed name just isn't audited; a mis-parsed name makes `lean` error and
201+ /// the audit falls back to `Unknown` — it never yields a wrong verdict.
202+ fn decl_names ( src : & str ) -> Vec < String > {
203+ const KEYWORDS : & [ & str ] = & [ "theorem" , "lemma" , "def" , "abbrev" , "instance" ] ;
204+ const MODIFIERS : & [ & str ] = & [
205+ "private" ,
206+ "protected" ,
207+ "noncomputable" ,
208+ "partial" ,
209+ "unsafe" ,
210+ "scoped" ,
211+ "local" ,
212+ "mutual" ,
213+ ] ;
214+ let mut names = Vec :: new ( ) ;
215+ for line in src. lines ( ) {
216+ let tokens: Vec < & str > = line. split_whitespace ( ) . collect ( ) ;
217+ let mut i = 0 ;
218+ // Skip leading `@[..]` attributes and declaration modifiers.
219+ while let Some ( tk) = tokens. get ( i) {
220+ if tk. starts_with ( "@[" ) || MODIFIERS . contains ( tk) {
221+ i += 1 ;
222+ } else {
223+ break ;
224+ }
225+ }
226+ if tokens. get ( i) . is_some_and ( |tk| KEYWORDS . contains ( tk) ) {
227+ if let Some ( name_tok) = tokens. get ( i + 1 ) {
228+ let name: String = name_tok
229+ . chars ( )
230+ . take_while ( |c| c. is_alphanumeric ( ) || * c == '_' || * c == '.' || * c == '\'' )
231+ . collect ( ) ;
232+ if !name. is_empty ( ) {
233+ names. push ( name) ;
234+ }
235+ }
236+ }
237+ }
238+ names. dedup ( ) ;
239+ names
240+ }
241+
242+ /// Classify the combined output of a batch of `#print axioms` commands:
243+ /// any `sorryAx` ⇒ Admitted; else any non-standard axiom ⇒ Postulated; else
244+ /// (all clean or standard-only) ⇒ Proven.
245+ fn classify_axioms ( output : & str ) -> Verdict {
246+ let mut saw_nonstandard = false ;
247+ for line in output. lines ( ) {
248+ let Some ( open) = line. find ( "depends on axioms: [" ) else {
249+ continue ; // "does not depend on any axioms" ⇒ clean, skip
250+ } ;
251+ let rest = & line[ open + "depends on axioms: [" . len ( ) ..] ;
252+ let list = rest. split ( ']' ) . next ( ) . unwrap_or ( rest) ;
253+ for ax in list. split ( ',' ) {
254+ let ax = ax. trim ( ) ;
255+ if ax == "sorryAx" {
256+ return Verdict :: Admitted ;
257+ }
258+ if !ax. is_empty ( ) && !STANDARD_AXIOMS . contains ( & ax) {
259+ saw_nonstandard = true ;
260+ }
261+ }
262+ }
263+ if saw_nonstandard {
264+ Verdict :: Postulated
265+ } else {
266+ Verdict :: Proven
267+ }
268+ }
269+
270+ /// Run a `#print axioms` audit on `file`'s declarations. Copies the source
271+ /// into a fresh temp dir, appends `#print axioms <name>` per declaration,
272+ /// and runs `lean`. Returns the classified verdict, or `None` when the audit
273+ /// can't be trusted — no declarations, `lean` absent, or the copy fails to
274+ /// elaborate (e.g. it imports modules that need `lake env`/`LEAN_PATH`, which
275+ /// a bare temp dir lacks). `None` ⇒ the caller keeps the honest `Unknown`.
276+ fn axiom_audit ( file : & Path ) -> Option < Verdict > {
277+ let src = fs:: read_to_string ( file) . ok ( ) ?;
278+ let names = decl_names ( & src) ;
279+ if names. is_empty ( ) {
280+ return None ;
281+ }
282+
283+ let nanos = SystemTime :: now ( )
284+ . duration_since ( UNIX_EPOCH )
285+ . map ( |d| d. as_nanos ( ) )
286+ . unwrap_or ( 0 ) ;
287+ let dir = std:: env:: temp_dir ( ) . join ( format ! ( "arghda-audit-{}-{}" , std:: process:: id( ) , nanos) ) ;
288+ fs:: create_dir_all ( & dir) . ok ( ) ?;
289+
290+ let mut body = src;
291+ body. push ( '\n' ) ;
292+ for n in & names {
293+ body. push_str ( & format ! ( "#print axioms {n}\n " ) ) ;
294+ }
295+ let audit_file = dir. join ( "Audit.lean" ) ;
296+
297+ let verdict = match fs:: write ( & audit_file, & body) {
298+ Ok ( ( ) ) => match Command :: new ( "lean" ) . arg ( & audit_file) . output ( ) {
299+ // Only trust the audit if the copy elaborated cleanly; otherwise
300+ // (imports unresolved in the temp dir, etc.) stay Unknown.
301+ Ok ( out) if out. status . success ( ) => {
302+ let mut combined = String :: from_utf8_lossy ( & out. stdout ) . into_owned ( ) ;
303+ combined. push_str ( & String :: from_utf8_lossy ( & out. stderr ) ) ;
304+ Some ( classify_axioms ( & combined) )
305+ }
306+ _ => None ,
307+ } ,
308+ Err ( _) => None ,
309+ } ;
310+
311+ let _ = fs:: remove_dir_all ( & dir) ;
312+ verdict
313+ }
314+
173315#[ cfg( test) ]
174316mod tests {
175317 use super :: * ;
@@ -208,6 +350,52 @@ mod tests {
208350 assert ! ( !imports. iter( ) . any( |i| i. contains( "Ignored" ) ) ) ;
209351 }
210352
353+ #[ test]
354+ fn decl_names_parses_keywords_modifiers_attributes ( ) {
355+ let src = "\
356+ \n \
357+ \n \
358+ \n \
359+ \n \
360+ \n \
361+ \n \
362+ \n ";
363+ let names = decl_names ( src) ;
364+ assert ! ( names. contains( & "foo" . to_string( ) ) ) ;
365+ assert ! ( names. contains( & "bar" . to_string( ) ) ) ;
366+ assert ! ( names. contains( & "baz.qux" . to_string( ) ) , "dotted names kept" ) ;
367+ assert ! ( names. contains( & "qq" . to_string( ) ) , "modifier skipped" ) ;
368+ // `example` is anonymous → not audited; `#eval` is not a decl.
369+ assert ! ( !names. iter( ) . any( |n| n == "example" || n == "1" ) ) ;
370+ }
371+
372+ #[ test]
373+ fn classify_axioms_maps_the_ground_truthed_output ( ) {
374+ // The three shapes ground-truthed against Lean 4.13.0.
375+ assert_eq ! (
376+ classify_axioms( "'t' does not depend on any axioms" ) ,
377+ Verdict :: Proven
378+ ) ;
379+ assert_eq ! (
380+ classify_axioms( "'c' depends on axioms: [propext, Classical.choice, Quot.sound]" ) ,
381+ Verdict :: Proven ,
382+ ) ;
383+ assert_eq ! (
384+ classify_axioms( "'g' depends on axioms: [sorryAx]" ) ,
385+ Verdict :: Admitted
386+ ) ;
387+ assert_eq ! (
388+ classify_axioms( "'n' depends on axioms: [Lean.ofReduceBool]" ) ,
389+ Verdict :: Postulated ,
390+ "native_decide's axiom is non-standard ⇒ amber" ,
391+ ) ;
392+ // Mixed: any sorryAx dominates.
393+ assert_eq ! (
394+ classify_axioms( "'a' depends on axioms: [propext]\n 'b' depends on axioms: [sorryAx]" ) ,
395+ Verdict :: Admitted
396+ ) ;
397+ }
398+
211399 #[ test]
212400 fn verdict_is_honest_about_sorry_and_the_missing_audit ( ) {
213401 // A green elaboration is only Unknown without a #print axioms audit;
@@ -227,13 +415,14 @@ mod tests {
227415 std:: fs:: write ( & f, "theorem t : 1 = 1 := rfl\n " ) . unwrap ( ) ;
228416 let out = Lean . check_file ( & f, tmp. path ( ) ) . unwrap ( ) ;
229417 if out. available {
230- // Never fabricated Proven: a clean Lean file is Unknown (audit
231- // absent), a sorry file Admitted, a broken file Error.
418+ // Honest verdict invariant: never fabricated. With the axioms
419+ // audit a clean `rfl` proof is promoted to Proven; `ok` iff
420+ // Proven; and the value is always one of the real states.
232421 assert ! ( matches!(
233422 out. verdict,
234- Verdict :: Unknown | Verdict :: Admitted | Verdict :: Error
423+ Verdict :: Proven | Verdict :: Unknown | Verdict :: Admitted | Verdict :: Error
235424 ) ) ;
236- assert ! ( ! out. ok, "lean never reports `ok` without an axioms audit" ) ;
425+ assert_eq ! ( out. ok, out . verdict == Verdict :: Proven ) ;
237426 } else {
238427 assert_eq ! ( out. verdict, Verdict :: Unavailable ) ;
239428 }
0 commit comments