50 files changed, 36 insertions, 35 deletions

diff --git a/.gitignore b/.gitignore
index c0c6fed6..c0bbbf28 100644
--- a/.gitignore
+++ b/.gitignore
@@ -40,11 +40,11 @@ result
 # F*
 .depend
 *.hints
-tests/betree/obj/
-tests/betree_back_stateful/obj/
-tests/hashmap/obj/
-tests/hashmap_on_disk/obj/
-tests/misc/obj/
+tests/fstar/betree/obj/
+tests/fstar/betree_back_stateful/obj/
+tests/fstar/hashmap/obj/
+tests/fstar/hashmap_on_disk/obj/
+tests/fstar/misc/obj/
 
 # Misc
 /fstar-tests
diff --git a/Makefile b/Makefile
index 3f04ff09..6f35eaac 100644
--- a/Makefile
+++ b/Makefile
@@ -106,7 +106,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
 endif
 
 # The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(SUBDIR) $(OPTIONS)
+AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/fstar/$(SUBDIR) $(OPTIONS)
 
 
 # Add specific options to some tests
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1f91645b..c9723bd4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -66,11 +66,12 @@ let use_state = ref true (* TODO *)
        (st1, y)  <-- f_fwd x st0;
        ...
        x' <-- f_back x st0 y';
-    }]
+    ]}
 
     The second format is easier to reason about, but the first one is
     necessary to properly handle some Rust functions which use internal
-    mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}:
+    mutability such as
+    {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut}[RefCell::try_mut_borrow]}:
     in order to model this behaviour we would need a state, and calling the backward
     function would update the state by reinserting the updated value in it.
  *)
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToBackend.ml
index fc04ce90..fc04ce90 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToBackend.ml
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fda2b3a6..b0114baa 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -500,7 +500,7 @@ type fun_effect_info = {
       (** [true] if the function group is stateful. By *function group*, we mean
           the set [{ forward function } U { backward functions }].
 
-          We need this because of the option {!Config.backward_no_state_update}:
+          We need this because of the option {!val:Config.backward_no_state_update}:
           if it is [true], then in case of a backward function {!stateful} is [false],
           but we might need to know whether the corresponding forward function
           is stateful or not.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 132dc02e..30fc4989 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1083,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
 (** Decompose the monadic let-bindings.
 
-    See the explanations in {!Config.decompose_monadic_let_bindings}
+    See the explanations in {!val:Config.decompose_monadic_let_bindings}
  *)
 let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
     fun_decl =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 0f16b5b4..ff55f322 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -73,7 +73,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
   in
   fun id -> TypeVarId.Map.find id mp
 
-(** Retrieve the list of fields for the given variant of a {!type:Pure.type_decl}.
+(** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0171412b..79d1c913 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -343,7 +343,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
 let extract_definitions (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order *)
-  let export_type (qualif : ExtractToFStar.type_decl_qualif)
+  let export_type (qualif : ExtractToBackend.type_decl_qualif)
       (id : Pure.TypeDeclId.id) : unit =
     (* Retrive the declaration *)
     let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
@@ -353,8 +353,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       | Enum _ | Struct _ -> (false, qualif)
       | Opaque ->
           let qualif =
-            if config.interface then ExtractToFStar.TypeVal
-            else ExtractToFStar.AssumeType
+            if config.interface then ExtractToBackend.TypeVal
+            else ExtractToBackend.AssumeType
           in
           (true, qualif)
     in
@@ -363,7 +363,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     if
       (is_opaque && config.extract_opaque)
       || ((not is_opaque) && config.extract_transparent)
-    then ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def
+    then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def
   in
 
   (* Utility to check a function has a decrease clause *)
@@ -393,7 +393,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         (fun (_, (fwd, _)) ->
           let has_decr_clause = has_decreases_clause fwd in
           if has_decr_clause then
-            ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
+            ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt
               fwd)
         pure_ls;
     (* Extract the function definitions *)
@@ -413,12 +413,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          let is_opaque = Option.is_none fwd_def.Pure.body in
          let qualif =
            if is_opaque then
-             if config.interface then ExtractToFStar.Val
-             else ExtractToFStar.AssumeVal
-           else if not is_rec then ExtractToFStar.Let
+             if config.interface then ExtractToBackend.Val
+             else ExtractToBackend.AssumeVal
+           else if not is_rec then ExtractToBackend.Let
            else if is_mut_rec then
-             if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
-           else ExtractToFStar.LetRec
+             if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And
+           else ExtractToBackend.LetRec
          in
          let has_decr_clause =
            has_decreases_clause def && config.extract_decreases_clauses
@@ -428,7 +428,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
          then
-           ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
+           ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif
              has_decr_clause def)
        fls);
     (* Insert unit tests if necessary *)
@@ -436,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
-            ExtractToFStar.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+            ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
         pure_ls
   in
 
@@ -454,29 +454,29 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       ((not is_opaque) && config.extract_transparent)
       || (is_opaque && config.extract_opaque)
     then
-      ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body
+      ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body
         config.interface
   in
 
   let export_state_type () : unit =
     let qualif =
-      if config.interface then ExtractToFStar.TypeVal
-      else ExtractToFStar.AssumeType
+      if config.interface then ExtractToBackend.TypeVal
+      else ExtractToBackend.AssumeType
     in
-    ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
+    ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif
   in
 
   let export_decl (decl : A.declaration_group) : unit =
     match decl with
     | Type (NonRec id) ->
-        if config.extract_types then export_type ExtractToFStar.Type id
+        if config.extract_types then export_type ExtractToBackend.Type id
     | Type (Rec ids) ->
         (* Rk.: we shouldn't have (mutually) recursive opaque types *)
         if config.extract_types then
           List.iteri
             (fun i id ->
               let qualif =
-                if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
+                if i = 0 then ExtractToBackend.Type else ExtractToBackend.And
               in
               export_type qualif id)
             ids
@@ -569,12 +569,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * language, as well as some primitive names ("u32", etc.) *)
   let variant_concatenate_type_name = true in
   let fstar_fmt =
-    ExtractToFStar.mk_formatter trans_ctx crate.name
+    ExtractToBackend.mk_formatter trans_ctx crate.name
       variant_concatenate_type_name
   in
   let names_map =
     PureToExtract.initialize_names_map fstar_fmt
-      ExtractToFStar.fstar_names_map_init
+      ExtractToBackend.fstar_names_map_init
   in
   let ctx =
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
@@ -596,7 +596,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * sure there are no name clashes. *)
   let ctx =
     List.fold_left
-      (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def)
+      (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def)
       ctx trans_types
   in
 
@@ -612,13 +612,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         let is_global = (fst def).Pure.is_global_decl_body in
         if is_global then ctx
         else
-          ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
+          ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd
             gen_decr_clause def)
       ctx trans_funs
   in
 
   let ctx =
-    List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
+    List.fold_left ExtractToBackend.extract_global_decl_register_names ctx
       crate.globals
   in
 
diff --git a/compiler/dune b/compiler/dune
index 85f4b75b..10aa9b10 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -20,7 +20,7 @@
   Cps
   Expressions
   ExpressionsUtils
-  ExtractToFStar
+  ExtractToBackend
   FunsAnalysis
   Identifiers
   InterpreterBorrowsCore
diff --git a/tests/Makefile b/tests/fstar/Makefile
index a9c170f7..a9c170f7 100644
--- a/tests/Makefile
+++ b/tests/fstar/Makefile
diff --git a/tests/Makefile.template b/tests/fstar/Makefile.template
index a16b0edb..a16b0edb 100644
--- a/tests/Makefile.template
+++ b/tests/fstar/Makefile.template
diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index d48213d3..d48213d3 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index 07484711..07484711 100644
--- a/tests/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 9ba5d3e7..9ba5d3e7 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
diff --git a/tests/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
index dc49601a..dc49601a 100644
--- a/tests/betree/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree/BetreeMain.Opaque.fsti
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
index c81e3302..c81e3302 100644
--- a/tests/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fsti
diff --git a/tests/betree/Makefile b/tests/fstar/betree/Makefile
index a16b0edb..a16b0edb 100644
--- a/tests/betree/Makefile
+++ b/tests/fstar/betree/Makefile
diff --git a/tests/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 96138e46..96138e46 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
diff --git a/tests/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index d48213d3..d48213d3 100644
--- a/tests/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
diff --git a/tests/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
index 07484711..07484711 100644
--- a/tests/betree_back_stateful/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
diff --git a/tests/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index ea8344fa..ea8344fa 100644
--- a/tests/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
diff --git a/tests/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
index dc49601a..dc49601a 100644
--- a/tests/betree_back_stateful/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
diff --git a/tests/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
index c81e3302..c81e3302 100644
--- a/tests/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
diff --git a/tests/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile
index a16b0edb..a16b0edb 100644
--- a/tests/betree_back_stateful/Makefile
+++ b/tests/fstar/betree_back_stateful/Makefile
diff --git a/tests/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 96138e46..96138e46 100644
--- a/tests/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 3e51c6f1..3e51c6f1 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
diff --git a/tests/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index 4f3e37e9..4f3e37e9 100644
--- a/tests/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 6e67fca4..6e67fca4 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 21a46c73..21a46c73 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
diff --git a/tests/hashmap/Hashmap.Properties.fsti b/tests/fstar/hashmap/Hashmap.Properties.fsti
index 756ae687..756ae687 100644
--- a/tests/hashmap/Hashmap.Properties.fsti
+++ b/tests/fstar/hashmap/Hashmap.Properties.fsti
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/fstar/hashmap/Hashmap.Types.fst
index d53b8a42..d53b8a42 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/fstar/hashmap/Hashmap.Types.fst
diff --git a/tests/hashmap/Makefile b/tests/fstar/hashmap/Makefile
index a16b0edb..a16b0edb 100644
--- a/tests/hashmap/Makefile
+++ b/tests/fstar/hashmap/Makefile
diff --git a/tests/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 96138e46..96138e46 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 55685114..55685114 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
index b864e32a..b864e32a 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 82b44dbd..82b44dbd 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
diff --git a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
index 6e54ea10..6e54ea10 100644
--- a/tests/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
diff --git a/tests/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 4df039a8..4df039a8 100644
--- a/tests/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
index ce4d6485..ce4d6485 100644
--- a/tests/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
diff --git a/tests/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile
index a16b0edb..a16b0edb 100644
--- a/tests/hashmap_on_disk/Makefile
+++ b/tests/fstar/hashmap_on_disk/Makefile
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 96138e46..96138e46 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
diff --git a/tests/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 884d1778..884d1778 100644
--- a/tests/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
diff --git a/tests/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 68a0061e..68a0061e 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
diff --git a/tests/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti
index 7d86405a..7d86405a 100644
--- a/tests/misc/External.Opaque.fsti
+++ b/tests/fstar/misc/External.Opaque.fsti
diff --git a/tests/misc/External.Types.fsti b/tests/fstar/misc/External.Types.fsti
index 4a13a744..4a13a744 100644
--- a/tests/misc/External.Types.fsti
+++ b/tests/fstar/misc/External.Types.fsti
diff --git a/tests/misc/Makefile b/tests/fstar/misc/Makefile
index a16b0edb..a16b0edb 100644
--- a/tests/misc/Makefile
+++ b/tests/fstar/misc/Makefile
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 8161e7cd..8161e7cd 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
diff --git a/tests/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 424889ef..424889ef 100644
--- a/tests/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
diff --git a/tests/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 73e98884..73e98884 100644
--- a/tests/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
diff --git a/tests/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 96138e46..96138e46 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst