flux_infer/
lean_encoding.rs

1use std::{
2    fs::{self, OpenOptions},
3    io::{self, Write},
4    path::{Path, PathBuf},
5    process::{Command, Stdio},
6};
7
8use flux_common::{
9    bug,
10    dbg::{self, SpanTrace},
11    result::ResultExt,
12};
13use flux_config as config;
14use flux_middle::{
15    def_id::{FluxDefId, MaybeExternId},
16    global_env::GlobalEnv,
17    queries::QueryErr,
18    rty::{PrettyMap, local_deps},
19};
20use itertools::Itertools;
21use rustc_data_structures::fx::FxIndexSet;
22use rustc_hash::FxHashMap;
23use rustc_hir::def_id::DefId;
24use rustc_span::ErrorGuaranteed;
25
26use crate::{
27    fixpoint_encoding::{ConstDeps, InterpretedConst, KVarSolutions, SortDeps, fixpoint},
28    lean_format::{self, LeanCtxt, WithLeanCtxt, def_id_to_pascal_case, snake_case_to_pascal_case},
29};
30
31/// Helper macro to create Vec<String> from string-like values
32macro_rules! string_vec {
33    ($($s:expr),* $(,)?) => {
34        vec![$($s.to_string()),*]
35    };
36}
37
38fn vc_name(genv: GlobalEnv, def_id: DefId) -> String {
39    def_id_to_pascal_case(&def_id, &genv.tcx())
40}
41
42fn project() -> String {
43    config::lean_project().to_string()
44}
45
46fn namespaced<F>(f: &mut fs::File, w: F) -> io::Result<()>
47where
48    F: Fn(&mut fs::File) -> io::Result<()>,
49{
50    let namespace = "F";
51    writeln!(f, "\nnamespace {namespace}\n")?;
52    w(f)?;
53    writeln!(f, "\nend {namespace}")
54}
55
56// Via Gemini: https://gemini.google.com/share/9027e898b136
57/// Renames all files and directories from 'src' to 'dst'
58fn rename_dir_contents(src: &Path, dst: &Path) -> io::Result<()> {
59    // 1. Ensure the destination root exists
60    if !dst.exists() {
61        fs::create_dir_all(dst)?;
62    }
63
64    for entry in fs::read_dir(src)? {
65        let entry = entry?;
66        let file_type = entry.file_type()?;
67        let src_path = entry.path();
68        let dst_path = dst.join(entry.file_name());
69
70        if file_type.is_dir() {
71            // 2. If it's a directory, recurse
72            rename_dir_contents(&src_path, &dst_path)?;
73        } else {
74            // 3. If it's a file, rename (overwrites if exists)
75            // On Windows, this will fail if the target file is "in use"
76            // TODO: how to FORCE overwrite on Windows?
77            fs::rename(&src_path, &dst_path)?;
78        }
79    }
80    Ok(())
81}
82
83fn constant_deps(expr: &fixpoint::Expr, acc: &mut FxIndexSet<fixpoint::Var>) {
84    match expr {
85        fixpoint::Expr::Var(v) if matches!(v, fixpoint::Var::Const(..)) => {
86            acc.insert(*v);
87        }
88        fixpoint::Expr::App(func, _, args, _) => {
89            constant_deps(func, acc);
90            args.iter().for_each(|expr| constant_deps(expr, acc));
91        }
92        fixpoint::Expr::And(inner) | fixpoint::Expr::Or(inner) => {
93            inner.iter().for_each(|expr| constant_deps(expr, acc));
94        }
95        fixpoint::Expr::Atom(_, inner)
96        | fixpoint::Expr::BinaryOp(_, inner)
97        | fixpoint::Expr::Imp(inner)
98        | fixpoint::Expr::Iff(inner)
99        | fixpoint::Expr::Let(_, inner) => {
100            inner.iter().for_each(|expr| constant_deps(expr, acc));
101        }
102        fixpoint::Expr::IfThenElse(inner) => {
103            inner.iter().for_each(|expr| constant_deps(expr, acc));
104        }
105        fixpoint::Expr::Exists(_, inner)
106        | fixpoint::Expr::Neg(inner)
107        | fixpoint::Expr::Not(inner)
108        | fixpoint::Expr::IsCtor(_, inner) => {
109            constant_deps(inner, acc);
110        }
111        fixpoint::Expr::Var(..) | fixpoint::Expr::Constant(..) | fixpoint::Expr::ThyFunc(..) => {}
112    }
113}
114
115pub fn finalize(genv: GlobalEnv) -> io::Result<()> {
116    let project = project();
117    let src = genv.temp_dir().path().join(&project);
118    let dst = genv.lean_parent_dir().join(&project);
119    if src.exists() { rename_dir_contents(&src, &dst) } else { Ok(()) }
120}
121
122fn project_path(genv: GlobalEnv, kind: FileKind) -> PathBuf {
123    let project = project();
124    match kind {
125        FileKind::Flux => genv.temp_dir().path().join(project),
126        FileKind::User => genv.lean_parent_dir().join(project),
127    }
128}
129
130fn run_lean(genv: GlobalEnv, def_id: DefId) -> io::Result<()> {
131    let proof_path = LeanFile::Proof(def_id).path(genv);
132    let out = Command::new("lake")
133        .arg("--quiet")
134        .arg("--log-level=error")
135        .arg("lean")
136        .arg(proof_path)
137        .stdout(Stdio::piped())
138        .stderr(Stdio::piped())
139        .current_dir(project_path(genv, FileKind::User))
140        .spawn()?
141        .wait_with_output()?;
142    if out.stderr.is_empty() && out.stdout.is_empty() {
143        Ok(())
144    } else {
145        let stderr =
146            std::str::from_utf8(&out.stderr).unwrap_or("Lean exited with a non-zero return code");
147        Err(io::Error::other(stderr))
148    }
149}
150
151pub fn check_proof(genv: GlobalEnv, def_id: DefId) -> Result<(), ErrorGuaranteed> {
152    run_lean(genv, def_id)
153        .map_err(|_| {
154            let name = genv.tcx().def_path(def_id).to_string_no_crate_verbose();
155            let msg = format!("failed to check external proof for `crate{name}`");
156            let span = genv.tcx().def_span(def_id);
157            QueryErr::Emitted(genv.sess().dcx().handle().struct_span_err(span, msg).emit())
158        })
159        .emit(&genv)?;
160    Ok(())
161}
162
163/// Create a file at the given path, creating any missing parent directories.
164fn create_file_with_dirs<P: AsRef<Path>>(path: P) -> io::Result<Option<fs::File>> {
165    let path = path.as_ref();
166    if let Some(parent) = path.parent() {
167        fs::create_dir_all(parent)?;
168    }
169    match OpenOptions::new().write(true).create_new(true).open(path) {
170        Ok(file) => Ok(Some(file)),
171        Err(e) if e.kind() == io::ErrorKind::AlreadyExists => Ok(None),
172        Err(e) => Err(e),
173    }
174}
175
176#[derive(Eq, PartialEq, Hash, Debug, Clone)]
177pub enum FileKind {
178    /// Files that are only written by Flux
179    Flux,
180    /// Files that are modified by users
181    User,
182}
183
184/// Different kinds of Lean files
185#[derive(Eq, PartialEq, Hash, Debug, Clone)]
186pub enum LeanFile {
187    /// "Root" of the lean project, importing all the generated proofs
188    Basic,
189    /// "builtin" definitions
190    Fluxlib,
191    /// (human) opaque flux sorts, to be defined by the user in Lean
192    OpaqueSort(String),
193    /// (machine) sorts generated from flux definitions
194    Struct(String),
195    /// (human) opaque flux functions, to be defined by the user in Lean
196    OpaqueFun(String),
197    /// (machine) functions generated from flux definitions
198    Fun(String),
199    /// (machine) propositions holding the flux VCs
200    Vc(DefId),
201    /// (human) interactively written proofs of flux VCs
202    Proof(DefId),
203}
204
205impl LeanFile {
206    fn kind(&self) -> FileKind {
207        match self {
208            LeanFile::Basic
209            | LeanFile::Fluxlib
210            | LeanFile::Vc(_)
211            | LeanFile::Fun(_)
212            | LeanFile::Struct(_) => FileKind::Flux,
213            LeanFile::OpaqueSort(_) | LeanFile::OpaqueFun(_) | LeanFile::Proof(_) => FileKind::User,
214        }
215    }
216
217    fn segments(&self, genv: GlobalEnv) -> Vec<String> {
218        let project_name = snake_case_to_pascal_case(&project());
219        match self {
220            LeanFile::Basic => {
221                string_vec![project_name, "Basic"]
222            }
223            LeanFile::Fluxlib => {
224                string_vec![project_name, "Flux", "Prelude"]
225            }
226            LeanFile::OpaqueSort(name) => {
227                // let name = self.datasort_name(sort);
228                string_vec![project_name, "User", "Struct", name]
229            }
230            LeanFile::Struct(name) => {
231                // let name = self.datasort_name(sort);
232                string_vec![project_name, "Flux", "Struct", name]
233            }
234            LeanFile::OpaqueFun(name) => {
235                // let name = self.var_name(name);
236                string_vec![project_name, "User", "Fun", name]
237            }
238            LeanFile::Fun(name) => {
239                // let name = self.var_name(name);
240                string_vec![project_name, "Flux", "Fun", name]
241            }
242            LeanFile::Vc(def_id) => {
243                let name = vc_name(genv, *def_id);
244                string_vec![project_name, "Flux", "VC", name]
245            }
246            LeanFile::Proof(def_id) => {
247                let name = format!("{}Proof", vc_name(genv, *def_id));
248                string_vec![project_name, "User", "Proof", name]
249            }
250        }
251    }
252
253    /// All paths should be generated here
254    fn path(&self, genv: GlobalEnv) -> PathBuf {
255        let mut path = project_path(genv, self.kind());
256        for segment in self.segments(genv) {
257            path = path.join(segment);
258        }
259        path.set_extension("lean");
260        path
261    }
262
263    pub fn import(&self, genv: GlobalEnv) -> String {
264        format!("import {}", self.segments(genv).join("."))
265    }
266}
267
268pub struct LeanEncoder<'genv, 'tcx> {
269    genv: GlobalEnv<'genv, 'tcx>,
270    def_id: MaybeExternId,
271    pretty_var_map: PrettyMap<fixpoint::LocalVar>,
272    sort_deps: SortDeps,
273    fun_deps: Vec<fixpoint::FunDef>,
274    constants: ConstDeps,
275    kvar_solutions: KVarSolutions,
276    kvar_decls: Vec<fixpoint::KVarDecl>,
277    constraint: fixpoint::Constraint,
278    sort_files: FxHashMap<fixpoint::DataSort, LeanFile>,
279    fun_files: FxHashMap<FluxDefId, LeanFile>,
280    const_files: FxHashMap<fixpoint::Var, LeanFile>,
281}
282
283impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
284    fn lean_cx(&self) -> LeanCtxt<'_, 'genv, 'tcx> {
285        LeanCtxt {
286            genv: self.genv,
287            pretty_var_map: &self.pretty_var_map,
288            adt_map: &self.sort_deps.adt_map,
289            opaque_adt_map: &self.sort_deps.opaque_sorts,
290            kvar_solutions: &self.kvar_solutions,
291        }
292    }
293
294    fn datasort_name(&self, sort: &fixpoint::DataSort) -> String {
295        let name = format!("{}", WithLeanCtxt { item: sort, cx: &self.lean_cx() });
296        snake_case_to_pascal_case(&name)
297    }
298
299    fn lean_file_for_fun(&self, fun: &fixpoint::FunDef) -> LeanFile {
300        let name = self.var_name(&fun.name);
301        if fun.body.is_some() { LeanFile::Fun(name) } else { LeanFile::OpaqueFun(name) }
302    }
303
304    fn lean_file_for_interpreted_const(&self, const_: &InterpretedConst) -> LeanFile {
305        let name = self.var_name(&const_.0.name);
306        LeanFile::Fun(name)
307    }
308
309    fn var_name(&self, var: &fixpoint::Var) -> String {
310        let name = format!("{}", WithLeanCtxt { item: var, cx: &self.lean_cx() });
311        snake_case_to_pascal_case(&name)
312    }
313
314    fn open_classical(&self) -> &str {
315        "open Classical"
316    }
317
318    fn new(
319        genv: GlobalEnv<'genv, 'tcx>,
320        def_id: MaybeExternId,
321        pretty_var_map: PrettyMap<fixpoint::LocalVar>,
322        sort_deps: SortDeps,
323        fun_deps: Vec<fixpoint::FunDef>,
324        constants: ConstDeps,
325        kvar_solutions: KVarSolutions,
326        kvar_decls: Vec<fixpoint::KVarDecl>,
327        constraint: fixpoint::Constraint,
328    ) -> io::Result<Self> {
329        let mut encoder = Self {
330            genv,
331            def_id,
332            pretty_var_map,
333            sort_deps,
334            fun_deps,
335            constants,
336            kvar_decls,
337            kvar_solutions,
338            constraint,
339            fun_files: FxHashMap::default(),
340            sort_files: FxHashMap::default(),
341            const_files: FxHashMap::default(),
342        };
343        encoder.fun_files = encoder.fun_files();
344        encoder.sort_files = encoder.sort_files();
345        encoder.const_files = encoder.const_files();
346        Ok(encoder)
347    }
348
349    fn run(&self) -> io::Result<()> {
350        self.generate_lake_project_if_not_present()?;
351        self.generate_lib_if_absent()?;
352        self.generate_vc_file()?;
353        self.generate_proof_if_absent()?;
354        Ok(())
355    }
356
357    fn fun_files(&self) -> FxHashMap<FluxDefId, LeanFile> {
358        let mut res = FxHashMap::default();
359        for fun_def in &self.fun_deps {
360            let fixpoint::Var::Global(_, did) = fun_def.name else {
361                bug!("expected global var with id")
362            };
363            let name = self.var_name(&fun_def.name);
364            let file = LeanFile::Fun(name);
365            res.insert(did, file);
366        }
367        res
368    }
369
370    fn sort_files(&self) -> FxHashMap<fixpoint::DataSort, LeanFile> {
371        let mut res = FxHashMap::default();
372        for (_, sort) in &self.sort_deps.opaque_sorts {
373            let data_sort = sort.name.clone();
374            let name = self.datasort_name(&sort.name);
375            let file = LeanFile::OpaqueSort(name);
376            res.insert(data_sort, file);
377        }
378        for data_decl in &self.sort_deps.data_decls {
379            let data_sort = data_decl.name.clone();
380            let name = self.datasort_name(&data_decl.name);
381            let file = LeanFile::Struct(name);
382            res.insert(data_sort, file);
383        }
384        res
385    }
386
387    fn const_files(&self) -> FxHashMap<fixpoint::Var, LeanFile> {
388        let mut res = FxHashMap::default();
389        for (decl, _) in &self.constants.interpreted {
390            res.insert(decl.name, LeanFile::Fun(self.var_name(&decl.name)));
391        }
392        res
393    }
394
395    fn generate_lake_project_if_not_present(&self) -> io::Result<()> {
396        let path = project_path(self.genv, FileKind::User);
397        if !path.exists() {
398            Command::new("lake")
399                .current_dir(self.genv.lean_parent_dir())
400                .arg("new")
401                .arg(project())
402                .arg("lib")
403                .spawn()
404                .and_then(|mut child| child.wait())
405                .map(|_| ())?;
406        }
407        Ok(())
408    }
409
410    fn generate_opaque_sort_file_if_not_present(
411        &self,
412        sort: &fixpoint::SortDecl,
413    ) -> io::Result<()> {
414        let name = self.datasort_name(&sort.name);
415        let file = &LeanFile::OpaqueSort(name);
416
417        let path = file.path(self.genv);
418        if let Some(mut file) = create_file_with_dirs(path)? {
419            writeln!(file, "{}", &LeanFile::Fluxlib.import(self.genv))?;
420            writeln!(file, "{}", self.open_classical())?;
421            namespaced(&mut file, |f| {
422                writeln!(f, "def {} := sorry", WithLeanCtxt { item: sort, cx: &self.lean_cx() })
423            })?;
424            file.sync_all()?;
425        }
426        Ok(())
427    }
428
429    fn data_decl_dependencies(&self, data_decl: &fixpoint::DataDecl) -> Vec<&LeanFile> {
430        let name = &data_decl.name;
431        let mut acc = vec![];
432        data_decl.deps(&mut acc);
433        acc.into_iter()
434            .map(|data_sort| {
435                self.sort_files.get(&data_sort).unwrap_or_else(|| {
436                    panic!(
437                        "Missing sort file for dependency {:?} of data decl {:?}",
438                        data_sort, name
439                    )
440                })
441            })
442            .unique()
443            .collect()
444    }
445
446    fn generate_struct_file_if_not_present(
447        &self,
448        data_decl: &fixpoint::DataDecl,
449    ) -> io::Result<()> {
450        let name = self.datasort_name(&data_decl.name);
451        let file = &LeanFile::Struct(name);
452        let path = file.path(self.genv);
453        // No need to regenerate if created in this session; but otherwise regenerate as struct may have changed
454        if let Some(mut file) = create_file_with_dirs(path)? {
455            // import prelude
456            writeln!(file, "{}", &LeanFile::Fluxlib.import(self.genv))?;
457            // import sort dependencies
458            for dep in self.data_decl_dependencies(data_decl) {
459                writeln!(file, "{}", dep.import(self.genv))?;
460            }
461            writeln!(file, "{}", self.open_classical())?;
462
463            // write data decl
464            namespaced(&mut file, |f| {
465                writeln!(f, "{}", WithLeanCtxt { item: data_decl, cx: &self.lean_cx() })
466            })?;
467            file.sync_all()?;
468        }
469        Ok(())
470    }
471
472    fn sort_file(&self, sort: &fixpoint::DataSort) -> &LeanFile {
473        self.sort_files
474            .get(sort)
475            .unwrap_or_else(|| panic!("Missing sort file for sort {:?}", sort))
476    }
477
478    fn fun_file(&self, did: &FluxDefId) -> &LeanFile {
479        self.fun_files
480            .get(did)
481            .unwrap_or_else(|| panic!("Missing fun file for fun {:?}", did))
482    }
483
484    fn const_file(&self, name: &fixpoint::Var) -> &LeanFile {
485        self.const_files
486            .get(name)
487            .unwrap_or_else(|| panic!("Missing const file for const {name:?}"))
488    }
489
490    fn fun_def_dependencies(&self, did: FluxDefId, fun_def: &fixpoint::FunDef) -> Vec<&LeanFile> {
491        let mut res = vec![];
492
493        // 1. Collect the sort dependencies
494        let mut sorts = vec![];
495        fun_def.sort.deps(&mut sorts);
496        for data_sort in sorts {
497            res.push(self.sort_file(&data_sort));
498        }
499
500        // 2. Collect the fun dependencies
501        if !self.genv.normalized_info(did).uif {
502            let body = self.genv.inlined_body(did);
503            for dep_id in local_deps(&body) {
504                res.push(self.fun_file(&dep_id.to_def_id()));
505            }
506        }
507
508        let mut deps = FxIndexSet::default();
509        if let Some(body) = &fun_def.body {
510            constant_deps(&body.expr, &mut deps);
511        }
512        for (decl, _) in &self.constants.interpreted {
513            if deps.contains(&decl.name) {
514                res.push(self.const_file(&decl.name));
515            }
516        }
517        res
518    }
519
520    fn generate_fun_def_file_if_not_present(
521        &self,
522        did: FluxDefId,
523        fun_def: &fixpoint::FunDef,
524    ) -> io::Result<()> {
525        let path = self.lean_file_for_fun(fun_def).path(self.genv);
526        if let Some(mut file) = create_file_with_dirs(path)? {
527            // import prelude
528            writeln!(file, "{}", &LeanFile::Fluxlib.import(self.genv))?;
529            // import sort dependencies
530            for dep in self.fun_def_dependencies(did, fun_def) {
531                writeln!(file, "{}", dep.import(self.genv))?;
532            }
533            writeln!(file, "{}", self.open_classical())?;
534
535            // write fun def
536            namespaced(&mut file, |f| {
537                writeln!(f, "{}", WithLeanCtxt { item: fun_def, cx: &self.lean_cx() })
538            })?;
539            file.sync_all()?;
540        }
541        Ok(())
542    }
543
544    fn generate_interpreted_const_file_if_not_present(
545        &self,
546        interpreted_const: &InterpretedConst,
547    ) -> io::Result<()> {
548        let (const_decl, _) = interpreted_const;
549        let path = self
550            .lean_file_for_interpreted_const(interpreted_const)
551            .path(self.genv);
552        if let Some(mut file) = create_file_with_dirs(path)? {
553            // import prelude
554            writeln!(file, "{}", &LeanFile::Fluxlib.import(self.genv))?;
555
556            let mut sort_deps = vec![];
557            const_decl.sort.deps(&mut sort_deps);
558            for dep in sort_deps {
559                writeln!(file, "{}", self.sort_file(&dep).import(self.genv))?;
560            }
561
562            writeln!(file, "{}", self.open_classical())?;
563
564            namespaced(&mut file, |f| {
565                if let Some(comment) = &const_decl.comment {
566                    writeln!(f, "--{comment}")?;
567                }
568                writeln!(f, "{}", WithLeanCtxt { item: interpreted_const, cx: &self.lean_cx() })
569            })?;
570            file.sync_all()?;
571        }
572        Ok(())
573    }
574
575    fn generate_lib_if_absent(&self) -> io::Result<()> {
576        let path = LeanFile::Fluxlib.path(self.genv);
577        if let Some(mut file) = create_file_with_dirs(path)? {
578            writeln!(file, "-- FLUX LIBRARY [DO NOT MODIFY] --")?;
579            // TODO: Can't we write this from a single `write!` call?
580            writeln!(
581                file,
582                "def BitVec_shiftLeft {{ n : Nat }} (x s : BitVec n) : BitVec n := BitVec.shiftLeft x (s.toNat)"
583            )?;
584            writeln!(
585                file,
586                "def BitVec_ushiftRight {{ n : Nat }} (x s : BitVec n) : BitVec n := BitVec.ushiftRight x (s.toNat)"
587            )?;
588            writeln!(
589                file,
590                "def BitVec_sshiftRight {{ n : Nat }} (x s : BitVec n) : BitVec n := BitVec.sshiftRight x (s.toNat)"
591            )?;
592            writeln!(
593                file,
594                "def BitVec_uge {{ n : Nat }} (x y : BitVec n) := (BitVec.ult x y).not"
595            )?;
596            writeln!(
597                file,
598                "def BitVec_sge {{ n : Nat }} (x y : BitVec n) := (BitVec.slt x y).not"
599            )?;
600            writeln!(
601                file,
602                "def BitVec_ugt {{ n : Nat }} (x y : BitVec n) := (BitVec.ule x y).not"
603            )?;
604            writeln!(
605                file,
606                "def BitVec_sgt {{ n : Nat }} (x y : BitVec n) := (BitVec.sle x y).not"
607            )?;
608            writeln!(
609                file,
610                "def SmtMap (t0 t1 : Type) [Inhabited t0] [BEq t0] [Inhabited t1] : Type := t0 -> t1"
611            )?;
612            writeln!(
613                file,
614                "def SmtMap_default {{ t0 t1: Type }} (v : t1) [Inhabited t0] [BEq t0] [Inhabited t1] : SmtMap t0 t1 := fun _ => v"
615            )?;
616            writeln!(
617                file,
618                "def SmtMap_store {{ t0 t1 : Type }} [Inhabited t0] [BEq t0] [Inhabited t1] (m : SmtMap t0 t1) (k : t0) (v : t1) : SmtMap t0 t1 :=\n  fun x => if x == k then v else m x"
619            )?;
620            writeln!(
621                file,
622                "def SmtMap_select {{ t0 t1 : Type }} [Inhabited t0] [BEq t0] [Inhabited t1] (m : SmtMap t0 t1) (k : t0) := m k"
623            )?;
624        }
625        Ok(())
626    }
627
628    fn generate_vc_prelude(&self) -> io::Result<()> {
629        // 1. Generate lake project and lib file
630        self.generate_lib_if_absent()?;
631
632        // 2. Generate Opaque Struct Files
633        for (_, sort) in &self.sort_deps.opaque_sorts {
634            self.generate_opaque_sort_file_if_not_present(sort)?;
635        }
636        // 2. Generate Struct Files
637        for data_decl in &self.sort_deps.data_decls {
638            self.generate_struct_file_if_not_present(data_decl)?;
639        }
640        // 3. Generate Func Def Files
641        for fun_def in &self.fun_deps {
642            let fixpoint::Var::Global(_, did) = fun_def.name else {
643                bug!("expected global var with id")
644            };
645            self.generate_fun_def_file_if_not_present(did, fun_def)?;
646        }
647        // 4. Generate Const Decl Files
648        for const_decl in &self.constants.interpreted {
649            self.generate_interpreted_const_file_if_not_present(const_decl)?;
650        }
651        Ok(())
652    }
653
654    fn generate_vc_imports(&self, file: &mut fs::File) -> io::Result<()> {
655        writeln!(file, "{}", LeanFile::Fluxlib.import(self.genv))?;
656
657        for (_, sort) in &self.sort_deps.opaque_sorts {
658            let name = self.datasort_name(&sort.name);
659            writeln!(file, "{}", LeanFile::OpaqueSort(name).import(self.genv))?;
660        }
661
662        for data_decl in &self.sort_deps.data_decls {
663            let name = self.datasort_name(&data_decl.name);
664            writeln!(file, "{}", LeanFile::Struct(name).import(self.genv))?;
665        }
666
667        for fun_def in &self.fun_deps {
668            writeln!(file, "{}", self.lean_file_for_fun(fun_def).import(self.genv))?;
669        }
670
671        for const_decl in &self.constants.interpreted {
672            writeln!(
673                file,
674                "{}",
675                self.lean_file_for_interpreted_const(const_decl)
676                    .import(self.genv)
677            )?;
678        }
679
680        Ok(())
681    }
682
683    fn generate_vc_file(&self) -> io::Result<()> {
684        // 1. Generate imports
685        self.generate_vc_prelude()?;
686
687        // 2. Create file and add imports
688        let def_id = self.def_id.resolved_id();
689        let path = LeanFile::Vc(def_id).path(self.genv);
690        if let Some(mut file) = create_file_with_dirs(path)? {
691            self.generate_vc_imports(&mut file)?;
692            writeln!(file, "{}", self.open_classical())?;
693
694            let vc_name = vc_name(self.genv, def_id);
695            // 3. Write the VC
696            namespaced(&mut file, |f| {
697                write!(
698                    f,
699                    "{}",
700                    WithLeanCtxt {
701                        item: lean_format::LeanKConstraint {
702                            theorem_name: &vc_name,
703                            kvars: &self.kvar_decls,
704                            constr: &self.constraint,
705                        },
706                        cx: &self.lean_cx()
707                    }
708                )
709            })?;
710            file.sync_all()?;
711        }
712
713        Ok(())
714    }
715
716    fn generate_proof_if_absent(&self) -> io::Result<()> {
717        let def_id = self.def_id.resolved_id();
718        let vc_name = vc_name(self.genv, def_id);
719        let proof_name = format!("{vc_name}_proof");
720        let path = LeanFile::Proof(def_id).path(self.genv);
721
722        if let Some(mut file) = create_file_with_dirs(path)? {
723            writeln!(file, "{}", LeanFile::Fluxlib.import(self.genv))?;
724            writeln!(file, "{}", LeanFile::Vc(def_id).import(self.genv))?;
725            writeln!(file, "{}", self.open_classical())?;
726            namespaced(&mut file, |f| {
727                writeln!(f, "def {proof_name} : {vc_name} := by")?;
728                writeln!(f, "  unfold {vc_name}")?;
729                writeln!(f, "  sorry")
730            })?;
731            file.sync_all()?;
732        }
733        Ok(())
734    }
735
736    pub fn encode(
737        genv: GlobalEnv<'genv, 'tcx>,
738        def_id: MaybeExternId,
739        pretty_var_map: PrettyMap<fixpoint::LocalVar>,
740        sort_deps: SortDeps,
741        fun_deps: Vec<fixpoint::FunDef>,
742        constants: ConstDeps,
743        kvar_decls: Vec<fixpoint::KVarDecl>,
744        constraint: fixpoint::Constraint,
745        kvar_solutions: KVarSolutions,
746    ) -> io::Result<()> {
747        let encoder = Self::new(
748            genv,
749            def_id,
750            pretty_var_map,
751            sort_deps,
752            fun_deps,
753            constants,
754            kvar_solutions,
755            kvar_decls,
756            constraint,
757        )?;
758        encoder.run()?;
759        Ok(())
760    }
761}
762
763fn hyperlink_proof(genv: GlobalEnv, def_id: MaybeExternId) {
764    let vc_name = vc_name(genv, def_id.resolved_id());
765    let proof_name = format!("{vc_name}_proof");
766    let path = LeanFile::Proof(def_id.resolved_id()).path(genv);
767    if let Some(span) = genv.proven_externally(def_id.local_id()) {
768        let dst_span = SpanTrace::from_path(&path, 3, 5, proof_name.len());
769        dbg::hyperlink_json!(genv.tcx(), span, dst_span);
770    }
771}
772
773fn record_proof(genv: GlobalEnv, def_id: MaybeExternId) -> io::Result<()> {
774    let path = LeanFile::Basic.path(genv);
775
776    let mut file = match create_file_with_dirs(&path)? {
777        Some(mut file) => {
778            // First invocation: reset VCs
779            writeln!(file, "-- Flux Basic Imports [DO NOT MODIFY] --")?;
780            file
781        }
782        None => fs::OpenOptions::new().append(true).open(path)?,
783    };
784    writeln!(file, "{}", LeanFile::Proof(def_id.resolved_id()).import(genv))
785}
786
787/// We need to both hyperlink the proof (so users can easily jump to it)
788/// and record the proof in `Basic.lean` (so that it gets checked by `lake build`),
789/// regardless of whether the proof was cached.
790pub fn log_proof(genv: GlobalEnv, def_id: MaybeExternId) -> Result<(), ErrorGuaranteed> {
791    hyperlink_proof(genv, def_id);
792    record_proof(genv, def_id)
793        .map_err(|_| {
794            let name = genv
795                .tcx()
796                .def_path(def_id.resolved_id())
797                .to_string_no_crate_verbose();
798            let msg = format!("failed to record proof for `{name}`");
799            let span = genv.tcx().def_span(def_id);
800            QueryErr::Emitted(genv.sess().dcx().handle().struct_span_err(span, msg).emit())
801        })
802        .emit(&genv)?;
803    Ok(())
804}
flux_infer/lean_encoding.rs

flux_infer/
lean_encoding.rs
