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

flux_infer/
lean_encoding.rs
