Merge branch 'main' into lean-printer

Author: franziskuskiefer

.github/workflows/charon.yml

@@ -1,5 +1,6 @@
 on:
   pull_request:
+  workflow_dispatch:
 
 jobs:
   charon:

README.md

@@ -122,7 +122,7 @@ Quicklinks:
 ## Hacking on Hax
 The documentation of the internal crate of hax and its engine can be
 found [here for the engine](https://hax.cryspen.com/engine/index.html)
-and [here for the frontent](https://hax.cryspen.com/frontend/index.html).
+and [here for the frontend](https://hax.cryspen.com/frontend/index.html).
 
 ### Edit the sources (Nix)
 

engine/bin/lib.ml

@@ -186,7 +186,7 @@ let parse_id_table_node (json : Yojson.Safe.t) :
   in
   (table, value)
 
-let load_table (check_version : bool) : Yojson.Safe.t =
+let load_table ?(check_version = true) : Yojson.Safe.t =
   let table, json =
     Hax_io.read_json () |> Option.value_exn |> parse_id_table_node
   in
@@ -212,7 +212,7 @@ Please reinstall hax.
   json
 
 let parse_options () =
-  let json = load_table true in
+  let json = load_table ~check_version:true in
   let options = [%of_yojson: Types.engine_options] json in
   Profiling.enabled := options.backend.profile;
   options
@@ -258,7 +258,7 @@ module ExportFStarAst = Export_ast.Make (Fstar_backend.InputLanguage)
 let driver_for_rust_engine () : unit =
   let query : Rust_engine_types.query =
     (* TODO: support for table *)
-    (* let json = load_table false in *)
+    (* let json = load_table ~check_version:false in *)
     let json = Hax_io.read_json () |> Option.value_exn in
     [%of_yojson: Rust_engine_types.query] json
   in

frontend/exporter/src/traits/resolution.rs

@@ -13,7 +13,7 @@ use rustc_trait_selection::traits::ImplSource;
 
 use crate::{self_predicate, traits::utils::erase_and_norm};
 
-use super::utils::{implied_predicates, required_predicates, ToPolyTraitRef};
+use super::utils::{implied_predicates, normalize_bound_val, required_predicates, ToPolyTraitRef};
 
 #[derive(Debug, Clone)]
 pub enum PathChunk<'tcx> {
@@ -281,7 +281,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let mut new_candidates = Vec::new();
         for mut candidate in candidates {
             // Normalize and erase all lifetimes.
-            candidate.pred = erase_and_norm(tcx, self.typing_env, candidate.pred);
+            candidate.pred = normalize_bound_val(tcx, self.typing_env, candidate.pred);
             if let Entry::Vacant(entry) = self.candidates.entry(candidate.pred) {
                 entry.insert(candidate.clone());
                 new_candidates.push(candidate);
@@ -421,7 +421,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let tcx = self.tcx;
         let drop_trait = tcx.lang_items().drop_trait().unwrap();
 
-        let erased_tref = erase_and_norm(self.tcx, self.typing_env, *tref);
+        let erased_tref = normalize_bound_val(self.tcx, self.typing_env, *tref);
         let trait_def_id = erased_tref.skip_binder().def_id;
 
         let impl_source = shallow_resolve_trait_ref(tcx, self.typing_env.param_env, erased_tref);

frontend/exporter/src/traits/utils.rs

@@ -167,14 +167,17 @@ pub fn implied_predicates<'tcx>(
     }
 }
 
-/// Erase all regions. Largely copied from `tcx.erase_regions`.
-pub fn erase_all_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T
+/// Erase free regions from the given value. Largely copied from `tcx.erase_regions`, but also
+/// erases bound regions that are bound outside `value`, so we can call this function inside a
+/// `Binder`.
+fn erase_free_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T
 where
     T: TypeFoldable<TyCtxt<'tcx>>,
 {
     use rustc_middle::ty;
     struct RegionEraserVisitor<'tcx> {
         tcx: TyCtxt<'tcx>,
+        depth: u32,
     }
 
     impl<'tcx> TypeFolder<TyCtxt<'tcx>> for RegionEraserVisitor<'tcx> {
@@ -190,33 +193,53 @@ where
         where
             T: TypeFoldable<TyCtxt<'tcx>>,
         {
-            // Empty the binder
-            Binder::dummy(t.skip_binder().fold_with(self))
+            let t = self.tcx.anonymize_bound_vars(t);
+            self.depth += 1;
+            let t = t.super_fold_with(self);
+            self.depth -= 1;
+            t
         }
 
-        fn fold_region(&mut self, _r: ty::Region<'tcx>) -> ty::Region<'tcx> {
-            // We erase bound regions despite it being possibly incorrect. `for<'a> fn(&'a
-            // ())` and `fn(&'free ())` are different types: they may implement different
-            // traits and have a different `TypeId`. It's unclear whether this can cause us
-            // to select the wrong trait reference.
-            self.tcx.lifetimes.re_erased
+        fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
+            // We don't erase bound regions that are bound inside the expression we started with,
+            // but we do erase those that point "outside of it".
+            match r.kind() {
+                ty::ReBound(dbid, _) if dbid.as_u32() < self.depth => r,
+                _ => self.tcx.lifetimes.re_erased,
+            }
         }
     }
-    value.fold_with(&mut RegionEraserVisitor { tcx })
+    value.fold_with(&mut RegionEraserVisitor { tcx, depth: 0 })
 }
 
-// Lifetimes are irrelevant when resolving instances.
+// Normalize and erase lifetimes, erasing more lifetimes than normal because we might be already
+// inside a binder and rustc doesn't like that.
 pub fn erase_and_norm<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, x: T) -> T
 where
     T: TypeFoldable<TyCtxt<'tcx>> + Copy,
 {
-    erase_all_regions(
+    erase_free_regions(
         tcx,
         tcx.try_normalize_erasing_regions(typing_env, x)
             .unwrap_or(x),
     )
 }
 
+/// Given our currently hacky handling of binders, in order for trait resolution to work we must
+/// empty out the binders of trait refs. Specifically it's so that we can reconnect associated type
+/// constraints with the trait ref they come from, given that the projection in question doesn't
+/// track the right binder currently.
+pub fn normalize_bound_val<'tcx, T>(
+    tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
+    x: Binder<'tcx, T>,
+) -> Binder<'tcx, T>
+where
+    T: TypeFoldable<TyCtxt<'tcx>> + Copy,
+{
+    Binder::dummy(erase_and_norm(tcx, typing_env, x.skip_binder()))
+}
+
 pub trait ToPolyTraitRef<'tcx> {
     fn to_poly_trait_ref(&self) -> PolyTraitRef<'tcx>;
 }

rust-engine/README.md

@@ -1,14 +1,15 @@
-This crate should implement an AST for which:
- 1. Valid (cargo check) pretty-printed Rust can be produced out of it.
- 2. The Rust THIR AST from the frontend can be imported into this AST.
- 3. The AST defined in the OCaml engine can be imported into this AST.
- 4. This AST can be exported to the OCaml engine.
- 5. This AST should be suitable for AST transformations.
+# Hax Rust Engine
+
+This crate implements an alternative engine for Rust: the main one is implemented in OCaml and is located in `/engine`.
+This Rust engine is designed so that it can re-use some bits of the OCaml engine.
+
+The plan is to slowly deprecate the OCaml engine, rewrite most of its components and drop it.
 
 ## Usage
-The following command will run hax with the rust engine instead of the ocaml one.
-For now, this will create a dummy lean file, regardless the backend provided.
+The Rust engine supports only one backend for now: `Lean`.
+The Lean backend is currently empty and produces only a dummy file.
 
+To run it, use the follwing command:
 ```bash
-HAX_ENGINE_BINARY=hax-rust-engine cargo hax into fstar
+cargo hax into lean
 ```

rust-engine/src/ast.rs

@@ -1418,7 +1418,7 @@ pub enum ItemKind {
     /// A resugared item.
     /// This variant is introduced before printing only.
     /// Phases must not produce this variant.
-    Resugared(ResugaredTyKind),
+    Resugared(ResugaredItemKind),
 
     /// Item that is not implemented yet
     NotImplementedYet,

rust-engine/src/ocaml_engine.rs

@@ -46,7 +46,7 @@ pub enum Response {
     },
 }
 
-/// Extends the common `ToEngine` messages with one extra case: `Input`.
+/// Extends the common `ToEngine` messages with one extra case: `Query`.
 #[derive(::serde::Deserialize, ::serde::Serialize)]
 #[serde(untagged)]
 pub enum ExtendedToEngine {
@@ -94,12 +94,13 @@ impl Query {
                 .expect("Could not write on stdin"),
         );
 
-        // TODO: send a table here
+        // TODO: send a table here (see https://github.com/cryspen/hax/issues/1536)
         send!(stdin, self);
 
         let mut response = None;
         let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
         // TODO: this should be streaming (i.e. use a `LineAsEOF` reader wrapper that consumes a reader until `\n` occurs)
+        //       See https://github.com/cryspen/hax/issues/1537.
         for slice in stdout.split(b'\n') {
             let msg = (|| {
                 let slice = slice.ok()?;