Merge pull request #1526 from cryspen/rengine-def_id-names

Rust Engine: expose common `DefId`s in the Rust engine

Author: W95Psp

Cargo.lock

@@ -264,7 +264,10 @@ fn run_engine(
         input: haxmeta.items,
         impl_infos: haxmeta.impl_infos,
     };
-    let mut hax_engine_command = if let Backend::Lean { .. } = &engine_options.backend.backend {
+    let mut hax_engine_command = if let Backend::Lean { .. }
+    | Backend::GenerateRustEngineNames { .. } =
+        &engine_options.backend.backend
+    {
         find_rust_hax_engine(message_format)
     } else {
         find_hax_engine(message_format)

cli/subcommands/src/cargo_hax.rs

@@ -145,7 +145,12 @@ let run (options : Types.engine_options) : Types.output =
             failwith
               "The OCaml hax engine should never be called for lean. The Lean \
                backend uses the newer rust engine. Please report this issue on \
-               our GitHub repository: https://github.com/cryspen/hax.")
+               our GitHub repository: https://github.com/cryspen/hax."
+        | GenerateRustEngineNames ->
+            failwith
+              "The OCaml hax engine should never be called with \
+               `GenerateRustEngineNames`, it is an rust engine only internal \
+               command.")
   in
   {
     diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics;

engine/bin/lib.ml

@@ -185,6 +185,10 @@ pub enum Backend<E: Extension> {
     /// Use the Lean backend (warning: work in progress!)
     #[clap(hide = true)]
     Lean,
+    /// Extract `DefId`s of the crate as a Rust module tree.
+    /// This is a command that regenerates code for the rust engine.
+    #[clap(hide = true)]
+    GenerateRustEngineNames,
 }
 
 impl fmt::Display for Backend<()> {
@@ -196,6 +200,7 @@ impl fmt::Display for Backend<()> {
             Backend::Easycrypt { .. } => write!(f, "easycrypt"),
             Backend::ProVerif { .. } => write!(f, "proverif"),
             Backend::Lean { .. } => write!(f, "lean"),
+            Backend::GenerateRustEngineNames { .. } => write!(f, "generate_rust_engine_names"),
         }
     }
 }

hax-types/src/cli_options/mod.rs

@@ -45,6 +45,12 @@ expand *FLAGS:
     | ocamlformat --impl - \
     | just _pager
 
+# Regenerate names in the Rust engine. Writes to `rust-engine/src/names/generated.rs`.
+regenerate-names:
+  #!/usr/bin/env bash
+  OUTPUT_FILE=rust-engine/src/names/generated.rs
+  cargo hax -C --manifest-path engine/names/Cargo.toml \; into --output-dir $(dirname -- $OUTPUT_FILE) generate-rust-engine-names
+  rustfmt "$OUTPUT_FILE"
 
 # Format all the code
 fmt:

justfile

@@ -18,3 +18,4 @@ schemars.workspace = true
 serde-jsonlines = "0.5.0"
 serde_stacker = "0.1.12"
 pretty = "0.12"
+itertools.workspace = true

rust-engine/Cargo.toml

@@ -8,7 +8,8 @@ use crate::symbol::Symbol;
 use hax_rust_engine_macros::*;
 use std::fmt;
 
-mod global_id {
+/// The global identifiers of hax.
+pub mod global_id {
     use hax_frontend_exporter::{DefKind, DisambiguatedDefPathItem};
     use hax_rust_engine_macros::*;
 
@@ -123,8 +124,22 @@ mod global_id {
             }
         }
     }
-}
 
+    impl PartialEq<DefId> for GlobalId {
+        fn eq(&self, other: &DefId) -> bool {
+            if let Self::Concrete(concrete) = self {
+                &concrete.def_id.def_id == other
+            } else {
+                false
+            }
+        }
+    }
+    impl PartialEq<GlobalId> for DefId {
+        fn eq(&self, other: &GlobalId) -> bool {
+            other == self
+        }
+    }
+}
 /// Local identifier
 #[derive_group_for_ast]
 pub struct LocalId(pub Symbol);

rust-engine/src/ast/identifiers.rs

@@ -11,6 +11,7 @@
 pub mod ast;
 pub mod hax_io;
 pub mod lean;
+pub mod names;
 pub mod ocaml_engine;
 pub mod printer;
 pub mod symbol;

rust-engine/src/lib.rs

@@ -4,7 +4,7 @@ use hax_rust_engine::{
     ocaml_engine::{ExtendedToEngine, Response},
     printer::Allocator,
 };
-use hax_types::engine_api::File;
+use hax_types::{cli_options::Backend, engine_api::File};
 
 use pretty::{DocAllocator, DocBuilder};
 
@@ -13,22 +13,7 @@ fn krate_name(items: &Vec<Item>) -> String {
     head_item.ident.krate()
 }
 
-fn main() {
-    let ExtendedToEngine::Query(input) = hax_rust_engine::hax_io::read() else {
-        panic!()
-    };
-    let (value, _map) = input.destruct();
-
-    let query = hax_rust_engine::ocaml_engine::Query {
-        hax_version: value.hax_version,
-        impl_infos: value.impl_infos,
-        kind: hax_rust_engine::ocaml_engine::QueryKind::ImportThir { input: value.input },
-    };
-
-    let Some(Response::ImportThir { output: items }) = query.execute() else {
-        panic!()
-    };
-
+fn lean_backend(items: Vec<Item>) {
     let krate = krate_name(&items);
 
     // For now, the main function always calls the Lean backend
@@ -57,3 +42,39 @@ fn main() {
         sourcemap: None,
     }));
 }
+
+fn main() {
+    let ExtendedToEngine::Query(input) = hax_rust_engine::hax_io::read() else {
+        panic!()
+    };
+    let (value, _map) = input.destruct();
+
+    let query = hax_rust_engine::ocaml_engine::Query {
+        hax_version: value.hax_version,
+        impl_infos: value.impl_infos,
+        kind: hax_rust_engine::ocaml_engine::QueryKind::ImportThir { input: value.input },
+    };
+
+    let Some(Response::ImportThir { output: items }) = query.execute() else {
+        panic!()
+    };
+
+    match &value.backend.backend {
+        Backend::Fstar { .. }
+        | Backend::Coq { .. }
+        | Backend::Ssprove { .. }
+        | Backend::Easycrypt { .. }
+        | Backend::ProVerif { .. } => panic!(
+            "The Rust engine cannot be called with backend {}.",
+            value.backend.backend
+        ),
+        Backend::Lean => lean_backend(items),
+        Backend::GenerateRustEngineNames => hax_rust_engine::hax_io::write(
+            &hax_types::engine_api::protocol::FromEngine::File(File {
+                path: "generated.rs".into(),
+                contents: hax_rust_engine::names::codegen::export_def_ids_to_mod(items),
+                sourcemap: None,
+            }),
+        ),
+    }
+}