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

flux_infer/
lean_encoding.rs
