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

flux_infer/
lean_encoding.rs
