Implement a Config.ml file which groups all the global options in references

16 files changed, 388 insertions, 492 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
new file mode 100644
index 00000000..f446872c
--- /dev/null
+++ b/compiler/Config.ml
@@ -0,0 +1,192 @@
+(** Define the global configuration options *)
+
+(** {0 Interpreter} *)
+
+(** Check that invariants are maintained whenever we execute a statement *)
+let check_invariants = ref true
+
+(** Expand all symbolic values containing borrows upon introduction - allows
+    to use restrict ourselves to a simpler model for the projectors over
+    symbolic values.
+    The interpreter fails if doing this requires to do a branching (because
+    we need to expand an enumeration with strictly more than one variant)
+    or if we need to expand a recursive type (because this leads to looping).
+ *)
+let greedy_expand_symbolics_with_borrows = true
+
+(** Experimental.
+
+    TODO: remove (always true now)
+
+    We sometimes want to temporarily break the invariant that there is no
+    bottom value below a borrow. If this value is true, we don't check
+    the invariant, and the rule becomes: we can't end a borrow *if* it contains
+    a bottom value. The consequence is that it becomes ok to temporarily
+    have bottom below a borrow, if we put something else inside before ending
+    the borrow.
+
+    For instance, when evaluating an assignment, we move the value which
+    will be overwritten then do some administrative tasks with the borrows,
+    then move the rvalue to its destination. We currently want to be able
+    to check the invariants every time we end a borrow/an abstraction,
+    meaning at intermediate steps of the assignment where the invariants
+    might actually be broken.
+ *)
+let allow_bottom_below_borrow = true
+
+(** If a function doesn't return any borrows, we can immediately call
+    its backward functions. If this option is on, whenever we call a
+    function *and* this function returns unit, we immediately end all the
+    abstractions which are introduced and don't contain loans. This can be
+    useful to make the code cleaner (the backward function is introduced
+    where the function call happened) and make sure all forward functions
+    with no return value are followed by a backward function.
+ *)
+let return_unit_end_abs_with_no_loans = true
+
+(** {0 Translation} *)
+
+(** Controls whether we need to use a state to model the external world
+    (I/O, for instance).
+ *)
+let use_state = ref true (* TODO *)
+
+(** Controls whether backward functions update the state, in case we use
+    a state ({!use_state}).
+
+    If they update the state, we generate code of the following style:
+    {[
+       (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
+       ...
+       (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
+    }]
+
+    Otherwise, we generate code of the following shape:
+    {[
+       (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]}:
+    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.
+ *)
+let backward_no_state_update = ref false
+
+(** Controls whether we split the generated definitions between different
+    files for the types, clauses and functions, or if we group them in
+    one file.
+ *)
+let split_files = ref true
+
+(** If true, treat the unit functions (function taking no inputs and returning
+    no outputs) as unit tests: evaluate them with the interpreter and check that
+    they don't panic.
+ *)
+let test_unit_functions = ref false
+
+(** If true, insert tests in the generated files to check that the
+    unit functions normalize to [Success _].
+
+    For instance, in F* it generates code like this:
+    {[
+      let _ = assert_norm (FUNCTION () = Success ())
+    ]}
+ *)
+let test_trans_unit_functions = ref false
+
+(** If [true], insert [decreases] clauses for all the recursive definitions.
+
+    The body of such clauses must be defined by the user.
+ *)
+let extract_decreases_clauses = ref true
+
+(** In order to help the user, we can generate "template" decrease clauses
+    (i.e., definitions with proper signatures but dummy bodies) in a
+    dedicated file.
+ *)
+let extract_template_decreases_clauses = ref false
+
+(** {0 Micro passes} *)
+
+(** Some provers like F* don't support the decomposition of return values
+    in monadic let-bindings:
+    {[
+      // NOT supported in F*
+      let (x, y) <-- f ();
+      ...
+    ]}
+
+    In such situations, we might want to introduce an intermediate
+    assignment:
+    {[
+      let tmp <-- f ();
+      let (x, y) = tmp in
+      ...
+    ]}
+ *)
+let decompose_monadic_let_bindings = ref false
+
+(** Controls the unfolding of monadic let-bindings to explicit matches:
+
+    [y <-- f x; ...]
+
+    becomes:
+
+    [match f x with | Failure -> Failure | Return y -> ...]
+
+
+    This is useful when extracting to F*: the support for monadic
+    definitions is not super powerful.
+    Note that when {!field:unfold_monadic_let_bindings} is true, setting
+    {!field:decompose_monadic_let_bindings} to true and only makes the code
+    more verbose.
+ *)
+let unfold_monadic_let_bindings = ref false
+
+(** Controls whether we try to filter the calls to monadic functions
+    (which can fail) when their outputs are not used.
+
+    The useless calls are calls to backward functions which have no outputs.
+    This case happens if the original Rust function only takes *shared* borrows
+    as inputs, and is thus pretty common.
+
+    We are allowed to do this only because in this specific case,
+    the backward function fails *exactly* when the forward function fails
+    (they actually do exactly the same thing, the only difference being
+    that the forward function can potentially return a value), and upon
+    reaching the place where we should introduce a call to the backward
+    function, we know we have introduced a call to the forward function.
+
+    Also note that in general, backward functions "do more things" than
+    forward functions, and have more opportunities to fail (even though
+    in the generated code, calls to the backward functions should fail
+    exactly when the corresponding, previous call to the forward functions
+    failed).
+
+    This optimization is done in {!SymbolicToPure}.  We might want to move it to
+    the micro-passes subsequent to the translation from symbolic to pure, but it
+    is really super easy to do it when going from symbolic to pure. Note that
+    we later filter the useless *forward* calls in the micro-passes, where it is
+    more natural to do.
+
+    See the comments for {!expression_contains_child_call_in_all_paths}
+    for additional explanations.
+ *)
+let filter_useless_monadic_calls = ref true
+
+(** If {!filter_useless_monadic_calls} is activated, some functions
+    become useless: if this option is true, we don't extract them.
+
+    The calls to functions which always get filtered are:
+    - the forward functions with unit return value
+    - the backward functions which don't output anything (backward
+      functions coming from rust functions with no mutable borrows
+      as input values - note that if a function doesn't take mutable
+      borrows as inputs, it can't return mutable borrows; we actually
+      dynamically check for that).
+ *)
+let filter_useless_functions = ref true
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 0c72392b..96749f07 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -182,63 +182,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
 type config = {
   mode : interpreter_mode;
       (** Concrete mode (interpreter) or symbolic mode (for synthesis) **)
-  check_invariants : bool;
-      (** Check that invariants are maintained whenever we execute a statement *)
-  greedy_expand_symbolics_with_borrows : bool;
-      (** Expand all symbolic values containing borrows upon introduction - allows
-          to use restrict ourselves to a simpler model for the projectors over
-          symbolic values.
-          The interpreter fails if doing this requires to do a branching (because
-          we need to expand an enumeration with strictly more than one variant)
-          or if we need to expand a recursive type (because this leads to looping).
-       *)
-  allow_bottom_below_borrow : bool;
-      (** Experimental.
-  
-          We sometimes want to temporarily break the invariant that there is no
-          bottom value below a borrow. If this value is true, we don't check
-          the invariant, and the rule becomes: we can't end a borrow *if* it contains
-          a bottom value. The consequence is that it becomes ok to temporarily
-          have bottom below a borrow, if we put something else inside before ending
-          the borrow.
-          
-          For instance, when evaluating an assignment, we move the value which
-          will be overwritten then do some administrative tasks with the borrows,
-          then move the rvalue to its destination. We currently want to be able
-          to check the invariants every time we end a borrow/an abstraction,
-          meaning at intermediate steps of the assignment where the invariants
-          might actually be broken.
-       *)
-  return_unit_end_abs_with_no_loans : bool;
-      (** If a function doesn't return any borrows, we can immediately call
-          its backward functions. If this option is on, whenever we call a
-          function *and* this function returns unit, we immediately end all the
-          abstractions which are introduced and don't contain loans. This can be
-          useful to make the code cleaner (the backward function is introduced
-          where the function call happened) and make sure all forward functions
-          with no return value are followed by a backward function.
-       *)
 }
 [@@deriving show]
 
-(** See {!config} *)
-type partial_config = {
-  check_invariants : bool;
-  greedy_expand_symbolics_with_borrows : bool;
-  allow_bottom_below_borrow : bool;
-  return_unit_end_abs_with_no_loans : bool;
-}
-
-let config_of_partial (mode : interpreter_mode) (config : partial_config) :
-    config =
-  {
-    mode;
-    check_invariants = config.check_invariants;
-    greedy_expand_symbolics_with_borrows =
-      config.greedy_expand_symbolics_with_borrows;
-    allow_bottom_below_borrow = config.allow_bottom_below_borrow;
-    return_unit_end_abs_with_no_loans = config.return_unit_end_abs_with_no_loans;
-  }
+let mk_config (mode : interpreter_mode) : config = { mode }
 
 type type_context = {
   type_decls_groups : type_declaration_group TypeDeclId.Map.t;
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 6f0e8074..304d0f2f 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -1,6 +1,5 @@
 open Aeneas.LlbcOfJson
 open Aeneas.Logging
-open Aeneas.Print
 module T = Aeneas.Types
 module A = Aeneas.LlbcAst
 module I = Aeneas.Interpreter
@@ -10,6 +9,7 @@ module Micro = Aeneas.PureMicroPasses
 module Print = Aeneas.Print
 module PrePasses = Aeneas.PrePasses
 module Translate = Aeneas.Translate
+open Aeneas.Config
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
@@ -30,25 +30,12 @@ let () =
 
   (* Read the command line arguments *)
   let dest_dir = ref "" in
-  let decompose_monads = ref false in
-  let unfold_monads = ref true in
-  let filter_useless_calls = ref true in
-  let filter_useless_functions = ref true in
-  let test_units = ref false in
-  let test_trans_units = ref false in
-  let no_decreases_clauses = ref false in
-  let no_state = ref false in
-  (* [backward_no_state_update]: see the comment for {!Translate.config.backward_no_state_update} *)
-  let backward_no_state_update = ref false in
-  let template_decreases_clauses = ref false in
-  let no_split_files = ref false in
-  let no_check_inv = ref false in
 
   let spec =
     [
       ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
       ( "-decompose-monads",
-        Arg.Set decompose_monads,
+        Arg.Set decompose_monadic_let_bindings,
         " Decompose the monadic let-bindings.\n\n\
         \         Introduces a temporary variable which is later decomposed,\n\
         \         when the pattern on the left of the monadic let is not a \n\
@@ -59,49 +46,49 @@ let () =
         \         `tmp <-- f (); let (x, y) = tmp in ...`\n\
         \        " );
       ( "-unfold-monads",
-        Arg.Set unfold_monads,
+        Arg.Set unfold_monadic_let_bindings,
         " Unfold the monadic let-bindings to matches" );
-      ( "-filter-useless-calls",
-        Arg.Set filter_useless_calls,
-        " Filter the useless function calls, when possible" );
-      ( "-filter-useless-funs",
-        Arg.Set filter_useless_functions,
-        " Filter the useless forward/backward functions" );
+      ( "-no-filter-useless-calls",
+        Arg.Clear filter_useless_monadic_calls,
+        " Do not filter the useless function calls, when possible" );
+      ( "-no-filter-useless-funs",
+        Arg.Clear filter_useless_functions,
+        " Do not filter the useless forward/backward functions" );
       ( "-test-units",
-        Arg.Set test_units,
+        Arg.Set test_unit_functions,
         " Test the unit functions with the concrete interpreter" );
       ( "-test-trans-units",
-        Arg.Set test_trans_units,
+        Arg.Set test_trans_unit_functions,
         " Test the translated unit functions with the target theorem\n\
         \                         prover's normalizer" );
       ( "-no-decreases-clauses",
-        Arg.Set no_decreases_clauses,
+        Arg.Clear extract_decreases_clauses,
         " Do not add decrease clauses to the recursive definitions" );
       ( "-no-state",
-        Arg.Set no_state,
+        Arg.Clear use_state,
         " Do not use state-error monads, simply use error monads" );
       ( "-backward-no-state-update",
         Arg.Set backward_no_state_update,
         " Forbid backward functions from updating the state" );
       ( "-template-clauses",
-        Arg.Set template_decreases_clauses,
+        Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a\n\
         \                         dedicated file. Incompatible with \
          -no-decreases-clauses" );
       ( "-no-split-files",
-        Arg.Set no_split_files,
+        Arg.Clear split_files,
         " Don't split the definitions between different files for types,\n\
         \                         functions, etc." );
       ( "-no-check-inv",
-        Arg.Set no_check_inv,
+        Arg.Clear check_invariants,
         " Deactivate the invariant sanity checks performed at every step of\n\
         \                         evaluation. Dramatically saves speed." );
     ]
   in
   (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
-  assert ((not !no_decreases_clauses) || not !template_decreases_clauses);
+  assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
   (* Sanity check: -backward-no-state-update ==> not -no-state *)
-  assert ((not !backward_no_state_update) || not !no_state);
+  assert ((not !backward_no_state_update) || !use_state);
 
   let spec = Arg.align spec in
   let filenames = ref [] in
@@ -169,46 +156,17 @@ let () =
       let m = PrePasses.apply_passes m in
 
       (* Some options for the execution *)
-      let eval_config =
-        {
-          C.check_invariants = not !no_check_inv;
-          greedy_expand_symbolics_with_borrows = true;
-          allow_bottom_below_borrow = true;
-          return_unit_end_abs_with_no_loans = true;
-        }
-      in
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_units then I.Test.test_unit_functions eval_config m;
+      if !test_unit_functions then I.Test.test_unit_functions m;
 
       (* Evaluate the symbolic interpreter on the functions, ignoring the
        * functions which contain loops - TODO: remove *)
       let synthesize = true in
-      I.Test.test_functions_symbolic eval_config synthesize m;
+      I.Test.test_functions_symbolic synthesize m;
 
       (* Translate the functions *)
-      let test_unit_functions = !test_trans_units in
-      let micro_passes_config =
-        {
-          Micro.decompose_monadic_let_bindings = !decompose_monads;
-          unfold_monadic_let_bindings = !unfold_monads;
-          filter_useless_monadic_calls = !filter_useless_calls;
-          filter_useless_functions = !filter_useless_functions;
-        }
-      in
-      let trans_config =
-        {
-          Translate.eval_config;
-          mp_config = micro_passes_config;
-          split_files = not !no_split_files;
-          test_unit_functions;
-          extract_decreases_clauses = not !no_decreases_clauses;
-          extract_template_decreases_clauses = !template_decreases_clauses;
-          use_state = not !no_state;
-          backward_no_state_update = !backward_no_state_update;
-        }
-      in
-      Translate.translate_module filename dest_dir trans_config m;
+      Translate.translate_module filename dest_dir m;
 
       (* Print total elapsed time *)
       log#linfo
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index e752594e..f776c7ff 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -208,7 +208,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
+let evaluate_function_symbolic (synthesize : bool)
     (type_context : C.type_context) (fun_context : C.fun_context)
     (global_context : C.global_context) (fdef : A.fun_decl)
     (back_id : T.RegionGroupId.id option) :
@@ -229,7 +229,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
   in
 
   (* Create the continuation to finish the evaluation *)
-  let config = C.config_of_partial C.SymbolicMode config in
+  let config = C.mk_config C.SymbolicMode in
   let cf_finish res ctx =
     match res with
     | Return ->
@@ -284,8 +284,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (config : C.partial_config) (crate : A.crate)
-      (fid : A.FunDeclId.id) : unit =
+  let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = A.FunDeclId.nth crate.functions fid in
     let body = Option.get fdef.body in
@@ -311,7 +310,7 @@ module Test = struct
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
 
     (* Create the continuation to check the function's result *)
-    let config = C.config_of_partial C.ConcreteMode config in
+    let config = C.mk_config C.ConcreteMode in
     let cf_check res ctx =
       match res with
       | Return ->
@@ -340,24 +339,24 @@ module Test = struct
         && List.length def.A.signature.inputs = 0
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (config : C.partial_config) (crate : A.crate) : unit =
+  let test_unit_functions (crate : A.crate) : unit =
     let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
     let test_unit_fun (def : A.fun_decl) : unit =
-      test_unit_function config crate def.A.def_id
+      test_unit_function crate def.A.def_id
     in
     List.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
-  let test_function_symbolic (config : C.partial_config) (synthesize : bool)
-      (type_context : C.type_context) (fun_context : C.fun_context)
-      (global_context : C.global_context) (fdef : A.fun_decl) : unit =
+  let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
+      (fun_context : C.fun_context) (global_context : C.global_context)
+      (fdef : A.fun_decl) : unit =
     (* Debug *)
     log#ldebug
       (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
 
     (* Evaluate *)
     let evaluate =
-      evaluate_function_symbolic config synthesize type_context fun_context
+      evaluate_function_symbolic synthesize type_context fun_context
         global_context fdef
     in
     (* Execute the forward function *)
@@ -380,8 +379,7 @@ module Test = struct
       TODO: for now we ignore the functions which contain loops, because
       they are not supported by the symbolic interpreter.
    *)
-  let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
-      (crate : A.crate) : unit =
+  let test_functions_symbolic (synthesize : bool) (crate : A.crate) : unit =
     (* Filter the functions which contain loops *)
     let no_loop_funs =
       List.filter
@@ -397,8 +395,8 @@ module Test = struct
       (* Execute the function - note that as the symbolic interpreter explores
        * all the path, some executions are expected to "panic": we thus don't
        * check the return value *)
-      test_function_symbolic config synthesize type_context fun_context
-        global_context def
+      test_function_symbolic synthesize type_context fun_context global_context
+        def
     in
     List.iter test_fun no_loop_funs
 end
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 585db0eb..3d8ca3bf 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -853,7 +853,7 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
   (* The complete sanity check: also check that after we ended a borrow,
    * the invariant is preserved *)
   let cf_check : cm_fun =
-    comp cf_check_disappeared (Invariants.cf_check_invariants config)
+    comp cf_check_disappeared Invariants.cf_check_invariants
   in
 
   (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *)
@@ -1011,7 +1011,7 @@ and end_abstraction_aux (config : C.config) (chain : borrow_or_abs_ids)
   in
 
   (* Sanity check: ending an abstraction must preserve the invariants *)
-  let cc = comp cc (Invariants.cf_check_invariants config) in
+  let cc = comp cc Invariants.cf_check_invariants in
 
   (* Apply the continuation *)
   cc cf ctx
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index fe9ccbf4..40c32ccc 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -719,7 +719,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
 
 let greedy_expand_symbolic_values (config : C.config) : cm_fun =
  fun cf ctx ->
-  if config.greedy_expand_symbolics_with_borrows then (
+  if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
     greedy_expand_symbolics_with_borrows config cf ctx)
   else cf ctx
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index a0fb97d1..5bc440e7 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -34,7 +34,7 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Small helper *)
   let rec expand : cm_fun =
    fun cf ctx ->
-    let v = read_place config access p ctx in
+    let v = read_place access p ctx in
     match
       find_first_primitively_copyable_sv_with_borrows
         ctx.type_context.type_infos v
@@ -55,10 +55,10 @@ let expand_primitively_copyable_at_place (config : C.config)
     We also check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
-let read_place (config : C.config) (access : access_kind) (p : E.place)
+let read_place (access : access_kind) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
-  let v = read_place config access p ctx in
+  let v = read_place access p ctx in
   (* Check that there are no bottoms in the value *)
   assert (not (bottom_in_value ctx.ended_regions v));
   (* Check that there are no reserved borrows in the value *)
@@ -82,7 +82,7 @@ let access_rplace_reorganize_and_read (config : C.config)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
-  let read_place = read_place config access p in
+  let read_place = read_place access p in
   (* Compose *)
   comp cc read_place cf ctx
 
@@ -263,7 +263,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
-      let cc = read_place config access p in
+      let cc = read_place access p in
       (* Copy the value *)
       let copy cf v : m_fun =
        fun ctx ->
@@ -284,14 +284,14 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
   | Expressions.Move p ->
       (* Access the value *)
       let access = Move in
-      let cc = read_place config access p in
+      let cc = read_place access p in
       (* Move the value *)
       let move cf v : m_fun =
        fun ctx ->
         (* Check that there are no bottoms in the value we are about to move *)
         assert (not (bottom_in_value ctx.ended_regions v));
         let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
-        let ctx = write_place config access p bottom ctx in
+        let ctx = write_place access p bottom ctx in
         cf v ctx
       in
       (* Compose and apply *)
@@ -575,7 +575,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
               ({ v with V.value = v' }, v)
         in
         (* Update the borrowed value in the context *)
-        let ctx = write_place config access p nv ctx in
+        let ctx = write_place access p nv ctx in
         (* Compute the rvalue - simply a shared borrow with a the fresh id.
          * Note that the reference is *mutable* if we do a two-phase borrow *)
         let rv_ty =
@@ -610,7 +610,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         (* Compute the value with which to replace the value at place p *)
         let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
         (* Update the value in the context *)
-        let ctx = write_place config access p nv ctx in
+        let ctx = write_place access p nv ctx in
         (* Continue *)
         cf rv ctx
       in
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index 2ea3c6df..a268ed1f 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -19,8 +19,7 @@ open InterpreterPaths
     This function doesn't reorganize the context to make sure we can read
     the place. If needs be, you should call {!update_ctx_along_read_place} first.
  *)
-val read_place :
-  C.config -> access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
+val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
 
 (** Auxiliary function.
 
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 63e03e31..1e1401df 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -310,8 +310,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-let try_read_place (config : C.config) (access : access_kind) (p : E.place)
-    (ctx : C.eval_ctx) : V.typed_value path_access_result =
+let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
+    V.typed_value path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
   let update v = v in
@@ -321,7 +321,7 @@ let try_read_place (config : C.config) (access : access_kind) (p : E.place)
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if config.check_invariants then
+      if !Config.check_invariants then
         if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
@@ -332,15 +332,15 @@ let try_read_place (config : C.config) (access : access_kind) (p : E.place)
           raise (Failure "Unexpected environment update"));
       Ok read_value
 
-let read_place (config : C.config) (access : access_kind) (p : E.place)
-    (ctx : C.eval_ctx) : V.typed_value =
-  match try_read_place config access p ctx with
+let read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
+    V.typed_value =
+  match try_read_place access p ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
-let try_write_place (_config : C.config) (access : access_kind) (p : E.place)
-    (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
+let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
+    (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
   let update _ = nv in
@@ -350,9 +350,9 @@ let try_write_place (_config : C.config) (access : access_kind) (p : E.place)
       (* We ignore the read value *)
       Ok ctx
 
-let write_place (config : C.config) (access : access_kind) (p : E.place)
-    (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  match try_write_place config access p nv ctx with
+let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  match try_write_place access p nv ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok ctx -> ctx
 
@@ -417,9 +417,9 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
 *)
-let expand_bottom_value_from_projection (config : C.config)
-    (access : access_kind) (p : E.place) (remaining_pes : int)
-    (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx =
+let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
+    (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety)
+    (ctx : C.eval_ctx) : C.eval_ctx =
   (* Debugging *)
   log#ldebug
     (lazy
@@ -464,7 +464,7 @@ let expand_bottom_value_from_projection (config : C.config)
              ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
   in
   (* Update the context by inserting the expanded value at the proper place *)
-  match try_write_place config access p' nv ctx with
+  match try_write_place access p' nv ctx with
   | Ok ctx -> ctx
   | Error _ -> raise (Failure "Unreachable")
 
@@ -472,7 +472,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
     (p : E.place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
-  match try_read_place config access p ctx with
+  match try_read_place access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       let cc =
@@ -501,7 +501,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
-  match try_read_place config access p ctx with
+  match try_read_place access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       (* Update the context *)
@@ -518,8 +518,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
             (* Expand the {!V.Bottom} value *)
             fun cf ctx ->
              let ctx =
-               expand_bottom_value_from_projection config access p remaining_pes
-                 pe ty ctx
+               expand_bottom_value_from_projection access p remaining_pes pe ty
+                 ctx
              in
              cf ctx
         | FailBorrow _ -> raise (Failure "Could not write to a borrow")
@@ -569,7 +569,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
   in
 
   (* First, retrieve the value *)
-  let v = read_place config access p ctx in
+  let v = read_place access p ctx in
   (* Inspect the value and update the context while doing so.
      If the context gets updated: perform a recursive call (many things
      may have been updated in the context: we need to re-read the value
@@ -590,8 +590,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
-  let v = read_place config access p ctx in
-  let ctx = write_place config access p (mk_bottom v.V.ty) ctx in
+  let v = read_place access p ctx in
+  let ctx = write_place access p (mk_bottom v.V.ty) ctx in
   let dummy_id = C.fresh_dummy_var_id () in
   let ctx = C.ctx_push_dummy_var ctx dummy_id v in
   (* Auxiliary function *)
@@ -624,7 +624,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
         (* Pop *)
         let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
         (* Reinsert *)
-        let ctx = write_place config access p v ctx in
+        let ctx = write_place access p v ctx in
         (* Sanity check *)
         assert (not (outer_loans_in_value v));
         (* Continue *)
@@ -648,7 +648,7 @@ let prepare_lplace (config : C.config) (p : E.place)
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
-    let v = read_place config access p ctx in
+    let v = read_place access p ctx in
     (* Sanity checks *)
     assert (not (outer_loans_in_value v));
     (* Continue *)
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 14baf128..6e9286cd 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -33,8 +33,7 @@ val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-val read_place :
-  C.config -> access_kind -> E.place -> C.eval_ctx -> V.typed_value
+val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value
 
 (** Update the value at a given place.
 
@@ -46,12 +45,7 @@ val read_place :
     overwrite it.
  *)
 val write_place :
-  C.config ->
-  access_kind ->
-  E.place ->
-  V.typed_value ->
-  C.eval_ctx ->
-  C.eval_ctx
+  access_kind -> E.place -> V.typed_value -> C.eval_ctx -> C.eval_ctx
 
 (** Compute an expanded tuple ⊥ value.
 
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 15962ee3..14dd59b1 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -39,12 +39,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
   let replace cf (v : V.typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows it may contain *)
-    let mv = InterpreterPaths.read_place config access p ctx in
+    let mv = InterpreterPaths.read_place access p ctx in
     let dummy_id = C.fresh_dummy_var_id () in
     let ctx = C.ctx_push_dummy_var ctx dummy_id mv in
     (* Update the destination to ⊥ *)
     let nv = { v with value = V.Bottom } in
-    let ctx = write_place config access p nv ctx in
+    let ctx = write_place access p nv ctx in
     log#ldebug
       (lazy
         ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
@@ -119,14 +119,14 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
    fun ctx ->
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows *)
-    let mv = InterpreterPaths.read_place config Write p ctx in
+    let mv = InterpreterPaths.read_place Write p ctx in
     let dest_vid = C.fresh_dummy_var_id () in
     let ctx = C.ctx_push_dummy_var ctx dest_vid mv in
     (* Write to the destination *)
     (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
     assert (not (bottom_in_value ctx.ended_regions rv));
     (* Update the destination *)
-    let ctx = write_place config Write p rv ctx in
+    let ctx = write_place Write p rv ctx in
     (* Debug *)
     log#ldebug
       (lazy
@@ -540,9 +540,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
   match (region_params, type_params, args) with
   | [], [ boxed_ty ], [ E.Move input_box_place ] ->
       (* Required type checking *)
-      let input_box =
-        InterpreterPaths.read_place config Write input_box_place ctx
-      in
+      let input_box = InterpreterPaths.read_place Write input_box_place ctx in
       (let input_ty = ty_get_box input_box.V.ty in
        assert (input_ty = boxed_ty));
 
@@ -783,7 +781,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
    * checking the invariants *)
   let cc = greedy_expand_symbolic_values config in
   (* Sanity check *)
-  let cc = comp cc (Inv.cf_check_invariants config) in
+  let cc = comp cc Inv.cf_check_invariants in
 
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
@@ -1279,7 +1277,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
    * (see the documentation of {!config} for more information)
    *)
   let cc =
-    if config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output
+    if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output
     then comp cc end_abs_with_no_loans
     else cc
   in
@@ -1382,7 +1380,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
      * checking the invariants *)
     let cc = greedy_expand_symbolic_values config in
     (* Sanity check *)
-    let cc = comp_check_ctx cc (Inv.check_invariants config) in
+    let cc = comp_check_ctx cc Inv.check_invariants in
     (* Continue *)
     cc (cf res)
   in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index ead064a4..9bd6b78b 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -301,15 +301,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     - borrows/loans can't contain ⊥ or reserved mut borrows
     - shared loans can't contain mutable loans
  *)
-let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) :
-    unit =
+let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
   let visitor =
     object
       inherit [_] C.iter_eval_ctx as super
 
       method! visit_Bottom info =
         (* No ⊥ inside borrowed values *)
-        assert (config.C.allow_bottom_below_borrow || not info.outer_borrow)
+        assert (Config.allow_bottom_below_borrow || not info.outer_borrow)
 
       method! visit_ABottom _info =
         (* ⊥ inside an abstraction is not the same as in a regular value *)
@@ -672,7 +671,7 @@ type sv_info = {
     - the union of the aproj_loans contains the aproj_borrows applied on the
       same symbolic values
  *)
-let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
+let check_symbolic_values (ctx : C.eval_ctx) : unit =
   (* Small utility *)
   let module M = V.SymbolicValueId.Map in
   let infos : sv_info M.t ref = ref M.empty in
@@ -781,17 +780,17 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
 
   M.iter check_info !infos
 
-let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
-  if config.C.check_invariants then (
+let check_invariants (ctx : C.eval_ctx) : unit =
+  if !Config.check_invariants then (
     log#ldebug (lazy "Checking invariants");
     check_loans_borrows_relation_invariant ctx;
-    check_borrowed_values_invariant config ctx;
+    check_borrowed_values_invariant ctx;
     check_typing_invariant ctx;
-    check_symbolic_values config ctx)
+    check_symbolic_values ctx)
   else log#ldebug (lazy "Not checking invariants (check is not activated)")
 
 (** Same as {!check_invariants}, but written in CPS *)
-let cf_check_invariants (config : C.config) : cm_fun =
+let cf_check_invariants : cm_fun =
  fun cf ctx ->
-  check_invariants config ctx;
+  check_invariants ctx;
   cf ctx
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9d604626..1bf3b903 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -8,64 +8,6 @@ module V = Values
 (** The local logger *)
 let log = L.pure_micro_passes_log
 
-(** A configuration to control the application of the passes *)
-type config = {
-  decompose_monadic_let_bindings : bool;
-      (** Some provers like F* don't support the decomposition of return values
-          in monadic let-bindings:
-          {[
-            // NOT supported in F*
-            let (x, y) <-- f ();
-            ...
-          ]}
-
-          In such situations, we might want to introduce an intermediate
-          assignment:
-          {[
-            let tmp <-- f ();
-            let (x, y) = tmp in
-            ...
-          ]}
-       *)
-  unfold_monadic_let_bindings : bool;
-      (** Controls the unfolding of monadic let-bindings to explicit matches:
-          
-          [y <-- f x; ...]
-
-          becomes:
-          
-          [match f x with | Failure -> Failure | Return y -> ...]
-
-          
-          This is useful when extracting to F*: the support for monadic
-          definitions is not super powerful.
-          Note that when {!field:unfold_monadic_let_bindings} is true, setting
-          {!field:decompose_monadic_let_bindings} to true and only makes the code
-          more verbose.
-       *)
-  filter_useless_monadic_calls : bool;
-      (** Controls whether we try to filter the calls to monadic functions
-          (which can fail) when their outputs are not used.
-          
-          See the comments for {!expression_contains_child_call_in_all_paths}
-          for additional explanations.
-          
-          TODO: rename to {!filter_useless_monadic_calls}
-       *)
-  filter_useless_functions : bool;
-      (** If {!filter_useless_monadic_calls} is activated, some functions
-          become useless: if this option is true, we don't extract them.
-
-          The calls to functions which always get filtered are:
-          - the forward functions with unit return value
-          - the backward functions which don't output anything (backward
-            functions coming from rust functions with no mutable borrows
-            as input values - note that if a function doesn't take mutable
-            borrows as inputs, it can't return mutable borrows; we actually
-            dynamically check for that).
-       *)
-}
-
 (** Small utility.
 
     We sometimes have to insert new fresh variables in a function body, in which
@@ -1003,10 +945,10 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
     symbolic to pure. Here, we remove the definitions altogether, because they
     are now useless
   *)
-let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) :
-    fun_decl option =
+let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option =
   if
-    config.filter_useless_functions && Option.is_some def.back_id
+    !Config.filter_useless_functions
+    && Option.is_some def.back_id
     && def.signature.output = mk_result_ty mk_unit_ty
   then None
   else Some def
@@ -1027,12 +969,12 @@ let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) :
     In such situation, we can remove the forward function definition
     altogether.
   *)
-let keep_forward (config : config) (trans : pure_fun_translation) : bool =
+let keep_forward (trans : pure_fun_translation) : bool =
   let fwd, backs = trans in
   (* Note that at this point, the output types are no longer seen as tuples:
    * they should be lists of length 1. *)
   if
-    config.filter_useless_functions
+    !Config.filter_useless_functions
     && fwd.signature.output = mk_result_ty mk_unit_ty
     && backs <> []
   then false
@@ -1141,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].
+    See the explanations in {!config.decompose_monadic_let_bindings}
  *)
 let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
     fun_decl =
@@ -1243,8 +1185,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
     [ctx]: used only for printing.
  *)
-let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
-    fun_decl option =
+let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl option =
   (* Debug *)
   log#ldebug
     (lazy
@@ -1274,7 +1215,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
    * Note that the calls to those functions should already have been removed,
    * when translating from symbolic to pure. Here, we remove the definitions
    * altogether, because they are now useless *)
-  let def = filter_if_backward_with_no_outputs config def in
+  let def = filter_if_backward_with_no_outputs def in
 
   match def with
   | None -> None
@@ -1304,7 +1245,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
           ("eliminate_box_functions:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Filter the useless variables, assignments, function calls, etc. *)
-      let def = filter_useless config.filter_useless_monadic_calls ctx def in
+      let def = filter_useless !Config.filter_useless_monadic_calls ctx def in
       log#ldebug
         (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
@@ -1323,7 +1264,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
       (* Decompose the monadic let-bindings - F* specific
        * TODO: remove? *)
       let def =
-        if config.decompose_monadic_let_bindings then (
+        if !Config.decompose_monadic_let_bindings then (
           let def = decompose_monadic_let_bindings ctx def in
           log#ldebug
             (lazy
@@ -1339,7 +1280,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
 
       (* Unfold the monadic let-bindings *)
       let def =
-        if config.unfold_monadic_let_bindings then (
+        if !Config.unfold_monadic_let_bindings then (
           let def = unfold_monadic_let_bindings ctx def in
           log#ldebug
             (lazy
@@ -1365,12 +1306,12 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
     because this function contains useful information to extract the backward
     functions: keeping it is not necessary but more convenient.
  *)
-let apply_passes_to_pure_fun_translation (config : config) (ctx : trans_ctx)
+let apply_passes_to_pure_fun_translation (ctx : trans_ctx)
     (trans : pure_fun_translation) : bool * pure_fun_translation =
   (* Apply the passes to the individual functions *)
   let forward, backwards = trans in
-  let forward = Option.get (apply_passes_to_def config ctx forward) in
-  let backwards = List.filter_map (apply_passes_to_def config ctx) backwards in
+  let forward = Option.get (apply_passes_to_def ctx forward) in
+  let backwards = List.filter_map (apply_passes_to_def ctx) backwards in
   let trans = (forward, backwards) in
   (* Compute whether we need to filter the forward function or not *)
-  (keep_forward config trans, trans)
+  (keep_forward trans, trans)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9d249cfb..74bc20ae 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -12,45 +12,6 @@ module FA = FunsAnalysis
 (** The local logger *)
 let log = L.symbolic_to_pure_log
 
-(* TODO: carrying configurations everywhere is super annoying.
-   Group everything in references in a [Config.ml] file (put aside the execution
-   mode, maybe).
-*)
-type config = {
-  filter_useless_back_calls : bool;
-      (** If [true], filter the useless calls to backward functions.
-       
-          The useless calls are calls to backward functions which have no outputs.
-          This case happens if the original Rust function only takes *shared* borrows
-          as inputs, and is thus pretty common.
-
-          We are allowed to do this only because in this specific case,
-          the backward function fails *exactly* when the forward function fails
-          (they actually do exactly the same thing, the only difference being
-          that the forward function can potentially return a value), and upon
-          reaching the place where we should introduce a call to the backward
-          function, we know we have introduced a call to the forward function.
-          
-          Also note that in general, backward functions "do more things" than
-          forward functions, and have more opportunities to fail (even though
-          in the generated code, calls to the backward functions should fail
-          exactly when the corresponding, previous call to the forward functions
-          failed).
-          
-          We might want to move this optimization to the micro-passes subsequent
-          to the translation from symbolic to pure, but it is really super easy
-          to do it when going from symbolic to pure.
-          Note that we later filter the useless *forward* calls in the micro-passes,
-          where it is more natural to do.
-       *)
-  backward_no_state_update : bool;
-      (** Controls whether backward functions update the state, in case we use
-          a state ({!use_state}).
-
-          See {!Translate.config.backward_no_state_update}.
-   *)
-}
-
 type type_context = {
   llbc_type_decls : T.type_decl TypeDeclId.Map.t;
   type_decls : type_decl TypeDeclId.Map.t;
@@ -528,15 +489,14 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
 
     [backward_no_state_update]: see {!config}
  *)
-let get_fun_effect_info (backward_no_state_update : bool)
-    (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id)
-    (gid : T.RegionGroupId.id option) : fun_effect_info =
+let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+    (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with
   | A.Regular fid ->
       let info = A.FunDeclId.Map.find fid fun_infos in
       let stateful_group = info.stateful in
       let stateful =
-        stateful_group && ((not backward_no_state_update) || gid = None)
+        stateful_group && ((not !Config.backward_no_state_update) || gid = None)
       in
       { can_fail = info.can_fail; stateful_group; stateful }
   | A.Assumed aid ->
@@ -553,9 +513,8 @@ let get_fun_effect_info (backward_no_state_update : bool)
     name (outputs for backward functions come from borrows in the inputs
     of the forward function) which we use as hints to generate pretty names.
  *)
-let translate_fun_sig (backward_no_state_update : bool)
-    (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id)
-    (types_infos : TA.type_infos) (sg : A.fun_sig)
+let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+    (fun_id : A.fun_id) (types_infos : TA.type_infos) (sg : A.fun_sig)
     (input_names : string option list) (bid : T.RegionGroupId.id option) :
     fun_sig_named_outputs =
   (* Retrieve the list of parent backward functions *)
@@ -606,20 +565,18 @@ let translate_fun_sig (backward_no_state_update : bool)
         List.filter_map (translate_back_ty_for_gid gid) [ sg.output ]
   in
   (* Is the function stateful, and can it fail? *)
-  let effect_info =
-    get_fun_effect_info backward_no_state_update fun_infos fun_id bid
-  in
+  let effect_info = get_fun_effect_info fun_infos fun_id bid in
   (* If the function is stateful, the inputs are:
      - forward:  [fwd_ty0, ..., fwd_tyn, state]
      - backward:
-       - if config.no_backward_state: [fwd_ty0, ..., fwd_tyn, state, back_ty, state]
+       - if {!Config.backward_no_state_update}: [fwd_ty0, ..., fwd_tyn, state, back_ty, state]
        - otherwise: [fwd_ty0, ..., fwd_tyn, state, back_ty]
 
        The backward takes the same state as input as the forward function,
        together with the state at the point where it gets called, if it is
        stateful.
 
-       See the comments for {!Translate.config.backward_no_state_update}
+       See the comments for {!Config.backward_no_state_update}
   *)
   let fwd_state_ty =
     (* For the forward state, we check if the *whole group* is stateful.
@@ -1134,17 +1091,16 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) :
   let abs_ancestors = list_ancestor_abstractions ctx abs in
   (call_info.forward, abs_ancestors)
 
-let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
-    : texpression =
+let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
   | S.Return opt_v -> translate_return opt_v ctx
   | Panic -> translate_panic ctx
-  | FunCall (call, e) -> translate_function_call config call e ctx
-  | EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx
-  | EvalGlobal (gid, sv, e) -> translate_global_eval config gid sv e ctx
-  | Assertion (v, e) -> translate_assertion config v e ctx
-  | Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx
-  | Meta (meta, e) -> translate_meta config meta e ctx
+  | FunCall (call, e) -> translate_function_call call e ctx
+  | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
+  | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx
+  | Assertion (v, e) -> translate_assertion v e ctx
+  | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
+  | Meta (meta, e) -> translate_meta meta e ctx
   | ForwardEnd e ->
       (* Update the current state with the additional state received by the backward
          function, if needs be *)
@@ -1153,7 +1109,7 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
         | None -> ctx
         | Some _ -> { ctx with state_var = ctx.back_state_var }
       in
-      translate_expression config e ctx
+      translate_expression e ctx
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
@@ -1213,8 +1169,8 @@ and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression
   (* TODO: we should use a [Return] function *)
   mk_result_return_texpression output
 
-and translate_function_call (config : config) (call : S.call) (e : S.expression)
-    (ctx : bs_ctx) : texpression =
+and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
+    texpression =
   (* Translate the function call *)
   let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
   let args =
@@ -1236,8 +1192,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
         (* Retrieve the effect information about this function (can fail,
          * takes a state as input, etc.) *)
         let effect_info =
-          get_fun_effect_info config.backward_no_state_update
-            ctx.fun_context.fun_infos fid None
+          get_fun_effect_info ctx.fun_context.fun_infos fid None
         in
         (* If the function is stateful:
          * - add the state input argument
@@ -1306,12 +1261,12 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
   let func = { e = Qualif func; ty = func_ty } in
   let call = mk_apps func args in
   (* Translate the next expression *)
-  let next_e = translate_expression config e ctx in
+  let next_e = translate_expression e ctx in
   (* Put together *)
   mk_let effect_info.can_fail dest_v call next_e
 
-and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
-    (ctx : bs_ctx) : texpression =
+and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
+    texpression =
   log#ldebug
     (lazy
       ("translate_end_abstraction: abstraction kind: "
@@ -1359,7 +1314,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
         (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty))
         variables_values;
       (* Translate the next expression *)
-      let next_e = translate_expression config e ctx in
+      let next_e = translate_expression e ctx in
       (* Generate the assignemnts *)
       let monadic = false in
       List.fold_right
@@ -1377,8 +1332,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
             raise (Failure "Unreachable")
       in
       let effect_info =
-        get_fun_effect_info config.backward_no_state_update
-          ctx.fun_context.fun_infos fun_id (Some abs.back_id)
+        get_fun_effect_info ctx.fun_context.fun_infos fun_id (Some abs.back_id)
       in
       let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
       (* Retrieve the original call and the parent abstractions *)
@@ -1459,7 +1413,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
        * if necessary *)
       let ctx, func = bs_ctx_register_backward_call abs back_inputs ctx in
       (* Translate the next expression *)
-      let next_e = translate_expression config e ctx in
+      let next_e = translate_expression e ctx in
       (* Put everything together *)
       let args_mplaces = List.map (fun _ -> None) inputs in
       let args =
@@ -1479,14 +1433,15 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
        * =================
        * We do a small optimization here: if the backward function doesn't
        * have any output, we don't introduce any function call.
-       * See the comment in [config].
+       * See the comment in {!Config.filter_useless_monadic_calls}.
        *
        * TODO: use an option to disallow backward functions from updating the state.
        * TODO: a backward function which only gives back shared borrows shouldn't
        * update the state (state updates should only be used for mutable borrows,
        * with objects like Rc for instance.
        *)
-      if config.filter_useless_back_calls && outputs = [] && nstate = None then (
+      if !Config.filter_useless_monadic_calls && outputs = [] && nstate = None
+      then (
         (* No outputs - we do a small sanity check: the backward function
          * should have exactly the same number of inputs as the forward:
          * this number can be different only if the forward function returned
@@ -1549,7 +1504,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
           assert (given_back.ty = input.ty))
         given_back_inputs;
       (* Translate the next expression *)
-      let next_e = translate_expression config e ctx in
+      let next_e = translate_expression e ctx in
       (* Generate the assignments *)
       let monadic = false in
       List.fold_right
@@ -1557,20 +1512,20 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
           mk_let monadic given_back (mk_texpression_from_var input_var) e)
         given_back_inputs next_e
 
-and translate_global_eval (config : config) (gid : A.GlobalDeclId.id)
-    (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression =
+and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
+    (e : S.expression) (ctx : bs_ctx) : texpression =
   let ctx, var = fresh_var_for_symbolic_value sval ctx in
   let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
   let global_expr = { id = Global gid; type_args = [] } in
   (* We use translate_fwd_ty to translate the global type *)
   let ty = ctx_translate_fwd_ty ctx decl.ty in
   let gval = { e = Qualif global_expr; ty } in
-  let e = translate_expression config e ctx in
+  let e = translate_expression e ctx in
   mk_let false (mk_typed_pattern_from_var var None) gval e
 
-and translate_assertion (config : config) (v : V.typed_value) (e : S.expression)
-    (ctx : bs_ctx) : texpression =
-  let next_e = translate_expression config e ctx in
+and translate_assertion (v : V.typed_value) (e : S.expression) (ctx : bs_ctx) :
+    texpression =
+  let next_e = translate_expression e ctx in
   let monadic = true in
   let v = typed_value_to_texpression ctx v in
   let args = [ v ] in
@@ -1580,8 +1535,8 @@ and translate_assertion (config : config) (v : V.typed_value) (e : S.expression)
   let assertion = mk_apps func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
 
-and translate_expansion (config : config) (p : S.mplace option)
-    (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression =
+and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
+    (exp : S.expansion) (ctx : bs_ctx) : texpression =
   (* Translate the scrutinee *)
   let scrutinee_var = lookup_var_for_symbolic_value sv ctx in
   let scrutinee = mk_texpression_from_var scrutinee_var in
@@ -1598,7 +1553,7 @@ and translate_expansion (config : config) (p : S.mplace option)
           (* The (mut/shared) borrow type is extracted to identity: we thus simply
            * introduce an reassignment *)
           let ctx, var = fresh_var_for_symbolic_value nsv ctx in
-          let next_e = translate_expression config e ctx in
+          let next_e = translate_expression e ctx in
           let monadic = false in
           mk_let monadic
             (mk_typed_pattern_from_var var None)
@@ -1615,7 +1570,7 @@ and translate_expansion (config : config) (p : S.mplace option)
           (* There is exactly one branch: no branching *)
           let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
           let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
-          let branch = translate_expression config branch ctx in
+          let branch = translate_expression branch ctx in
           match type_id with
           | T.AdtId adt_id ->
               (* Detect if this is an enumeration or not *)
@@ -1706,7 +1661,7 @@ and translate_expansion (config : config) (p : S.mplace option)
             in
             let pat_ty = scrutinee.ty in
             let pat = mk_adt_pattern pat_ty variant_id vars in
-            let branch = translate_expression config branch ctx in
+            let branch = translate_expression branch ctx in
             { pat; branch }
           in
           let branches =
@@ -1727,8 +1682,8 @@ and translate_expansion (config : config) (p : S.mplace option)
   | ExpandBool (true_e, false_e) ->
       (* We don't need to update the context: we don't introduce any
        * new values/variables *)
-      let true_e = translate_expression config true_e ctx in
-      let false_e = translate_expression config false_e ctx in
+      let true_e = translate_expression true_e ctx in
+      let false_e = translate_expression false_e ctx in
       let e =
         Switch
           ( mk_opt_mplace_texpression scrutinee_mplace scrutinee,
@@ -1742,12 +1697,12 @@ and translate_expansion (config : config) (p : S.mplace option)
           match_branch =
         (* We don't need to update the context: we don't introduce any
          * new values/variables *)
-        let branch = translate_expression config branch_e ctx in
+        let branch = translate_expression branch_e ctx in
         let pat = mk_typed_pattern_from_primitive_value (PV.Scalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
-      let otherwise = translate_expression config otherwise ctx in
+      let otherwise = translate_expression otherwise ctx in
       let pat_ty = Integer int_ty in
       let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
       let otherwise : match_branch =
@@ -1764,9 +1719,9 @@ and translate_expansion (config : config) (p : S.mplace option)
         List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches);
       { e; ty }
 
-and translate_meta (config : config) (meta : S.meta) (e : S.expression)
-    (ctx : bs_ctx) : texpression =
-  let next_e = translate_expression config e ctx in
+and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+    texpression =
+  let next_e = translate_expression e ctx in
   let meta =
     match meta with
     | S.Assignment (lp, rv, rp) ->
@@ -1779,8 +1734,7 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression)
   let ty = next_e.ty in
   { e; ty }
 
-let translate_fun_decl (config : config) (ctx : bs_ctx)
-    (body : S.expression option) : fun_decl =
+let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   (* Translate *)
   let def = ctx.fun_decl in
   let bid = ctx.bid in
@@ -1802,10 +1756,9 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
     match body with
     | None -> None
     | Some body ->
-        let body = translate_expression config body ctx in
+        let body = translate_expression body ctx in
         let effect_info =
-          get_fun_effect_info config.backward_no_state_update
-            ctx.fun_context.fun_infos (Regular def_id) bid
+          get_fun_effect_info ctx.fun_context.fun_infos (Regular def_id) bid
         in
         (* Sanity check *)
         type_check_texpression ctx body;
@@ -1902,8 +1855,8 @@ let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
     - optional names for the outputs values (we derive them for the backward
       functions)
  *)
-let translate_fun_signatures (backward_no_state_update : bool)
-    (fun_infos : FA.fun_info A.FunDeclId.Map.t) (types_infos : TA.type_infos)
+let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+    (types_infos : TA.type_infos)
     (functions : (A.fun_id * string option list * A.fun_sig) list) :
     fun_sig_named_outputs RegularFunIdMap.t =
   (* For every function, translate the signatures of:
@@ -1914,8 +1867,7 @@ let translate_fun_signatures (backward_no_state_update : bool)
       (sg : A.fun_sig) : (regular_fun_id * fun_sig_named_outputs) list =
     (* The forward function *)
     let fwd_sg =
-      translate_fun_sig backward_no_state_update fun_infos fun_id types_infos sg
-        input_names None
+      translate_fun_sig fun_infos fun_id types_infos sg input_names None
     in
     let fwd_id = (fun_id, None) in
     (* The backward functions *)
@@ -1923,8 +1875,8 @@ let translate_fun_signatures (backward_no_state_update : bool)
       List.map
         (fun (rg : T.region_var_group) ->
           let tsg =
-            translate_fun_sig backward_no_state_update fun_infos fun_id
-              types_infos sg input_names (Some rg.id)
+            translate_fun_sig fun_infos fun_id types_infos sg input_names
+              (Some rg.id)
           in
           let id = (fun_id, Some rg.id) in
           (id, tsg))
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 72322c73..453e02db 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -11,63 +11,6 @@ open TranslateCore
 (** The local logger *)
 let log = TranslateCore.log
 
-type config = {
-  eval_config : Contexts.partial_config;
-  mp_config : Micro.config;
-  use_state : bool;
-      (** Controls whether we need to use a state to model the external world
-          (I/O, for instance).
-       *)
-  backward_no_state_update : bool;
-      (** Controls whether backward functions update the state, in case we use
-          a state ({!use_state}).
-
-          If they update the state, we generate code of the following style:
-          {[
-             (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
-             ...
-             (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
-          }]
-
-          Otherwise, we generate code of the following shape:
-          {[
-             (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]}:
-          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.
-       *)
-  split_files : bool;
-      (** Controls whether we split the generated definitions between different
-          files for the types, clauses and functions, or if we group them in
-          one file.
-       *)
-  test_unit_functions : bool;
-      (** If true, insert tests in the generated files to check that the
-          unit functions normalize to [Success _].
-          
-          For instance, in F* it generates code like this:
-          {[
-            let _ = assert_norm (FUNCTION () = Success ())
-          ]}
-       *)
-  extract_decreases_clauses : bool;
-      (** If [true], insert [decreases] clauses for all the recursive definitions.
-
-          The body of such clauses must be defined by the user.
-       *)
-  extract_template_decreases_clauses : bool;
-      (** In order to help the user, we can generate "template" decrease clauses
-          (i.e., definitions with proper signatures but dummy bodies) in a
-          dedicated file.
-       *)
-}
-
 (** The result of running the symbolic interpreter on a function:
     - the list of symbolic values used for the input values
     - the generated symbolic AST
@@ -77,9 +20,8 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression
 (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
     for the forward function and the backward functions.
 *)
-let translate_function_to_symbolics (config : C.partial_config)
-    (trans_ctx : trans_ctx) (fdef : A.fun_decl) :
-    (symbolic_fun_translation * symbolic_fun_translation list) option =
+let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
+    : (symbolic_fun_translation * symbolic_fun_translation list) option =
   (* Debug *)
   log#ldebug
     (lazy
@@ -96,7 +38,7 @@ let translate_function_to_symbolics (config : C.partial_config)
       let synthesize = true in
       let evaluate gid =
         let inputs, symb =
-          evaluate_function_symbolic config synthesize type_context fun_context
+          evaluate_function_symbolic synthesize type_context fun_context
             global_context fdef gid
         in
         (inputs, Option.get symb)
@@ -119,9 +61,7 @@ let translate_function_to_symbolics (config : C.partial_config)
     of backward functions, we also provide names for the outputs.
     TODO: maybe we should introduce a record for this.
 *)
-let translate_function_to_pure (config : C.partial_config)
-    (mp_config : Micro.config) (backward_no_state_update : bool)
-    (trans_ctx : trans_ctx)
+let translate_function_to_pure (trans_ctx : trans_ctx)
     (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
     : pure_fun_translation =
@@ -134,7 +74,7 @@ let translate_function_to_pure (config : C.partial_config)
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs, if the function is transparent *)
-  let symbolic_trans = translate_function_to_symbolics config trans_ctx fdef in
+  let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in
   let symbolic_forward, symbolic_backwards =
     match symbolic_trans with
     | None -> (None, None)
@@ -210,21 +150,12 @@ let translate_function_to_pure (config : C.partial_config)
         { ctx with forward_inputs }
   in
 
-  (* The symbolic to pure config *)
-  let sp_config =
-    {
-      SymbolicToPure.filter_useless_back_calls =
-        mp_config.filter_useless_monadic_calls;
-      backward_no_state_update;
-    }
-  in
-
   (* Translate the forward function *)
   let pure_forward =
     match symbolic_forward with
-    | None -> SymbolicToPure.translate_fun_decl sp_config ctx None
+    | None -> SymbolicToPure.translate_fun_decl ctx None
     | Some (fwd_svs, fwd_ast) ->
-        SymbolicToPure.translate_fun_decl sp_config
+        SymbolicToPure.translate_fun_decl
           (add_forward_inputs fwd_svs ctx)
           (Some fwd_ast)
   in
@@ -247,7 +178,7 @@ let translate_function_to_pure (config : C.partial_config)
         let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in
 
         (* Translate *)
-        SymbolicToPure.translate_fun_decl sp_config ctx None
+        SymbolicToPure.translate_fun_decl ctx None
     | Some symbolic_backwards ->
         let input_svs, symbolic =
           T.RegionGroupId.nth symbolic_backwards back_id
@@ -259,8 +190,8 @@ let translate_function_to_pure (config : C.partial_config)
         in
         (* We need to ignore the forward inputs, and the state input (if there is) *)
         let fun_info =
-          SymbolicToPure.get_fun_effect_info backward_no_state_update
-            fun_context.fun_infos (A.Regular def_id) (Some back_id)
+          SymbolicToPure.get_fun_effect_info fun_context.fun_infos
+            (A.Regular def_id) (Some back_id)
         in
         let backward_inputs =
           (* We need to ignore the forward state and the backward state *)
@@ -313,7 +244,7 @@ let translate_function_to_pure (config : C.partial_config)
         in
 
         (* Translate *)
-        SymbolicToPure.translate_fun_decl sp_config ctx (Some symbolic)
+        SymbolicToPure.translate_fun_decl ctx (Some symbolic)
   in
   let pure_backwards =
     List.map translate_backward fdef.signature.regions_hierarchy
@@ -322,9 +253,7 @@ let translate_function_to_pure (config : C.partial_config)
   (* Return *)
   (pure_forward, pure_backwards)
 
-let translate_module_to_pure (config : C.partial_config)
-    (mp_config : Micro.config) (use_state : bool)
-    (backward_no_state_update : bool) (crate : A.crate) :
+let translate_module_to_pure (crate : A.crate) :
     trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
@@ -335,7 +264,7 @@ let translate_module_to_pure (config : C.partial_config)
   in
   let fun_infos =
     FA.analyze_module crate fun_context.C.fun_decls
-      global_context.C.global_decls use_state
+      global_context.C.global_decls !Config.use_state
   in
   let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
   let trans_ctx = { type_context; fun_context; global_context } in
@@ -372,22 +301,21 @@ let translate_module_to_pure (config : C.partial_config)
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
-    SymbolicToPure.translate_fun_signatures backward_no_state_update
-      fun_context.fun_infos type_context.type_infos sigs
+    SymbolicToPure.translate_fun_signatures fun_context.fun_infos
+      type_context.type_infos sigs
   in
 
   (* Translate all the *transparent* functions *)
   let pure_translations =
     List.map
-      (translate_function_to_pure config mp_config backward_no_state_update
-         trans_ctx fun_sigs type_decls_map)
+      (translate_function_to_pure trans_ctx fun_sigs type_decls_map)
       crate.functions
   in
 
   (* Apply the micro-passes *)
   let pure_translations =
     List.map
-      (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx)
+      (Micro.apply_passes_to_pure_fun_translation trans_ctx)
       pure_translations
   in
 
@@ -404,8 +332,6 @@ type gen_ctx = {
 }
 
 type gen_config = {
-  mp_config : Micro.config;
-  use_state : bool;
   extract_types : bool;
   extract_decreases_clauses : bool;
   extract_template_decreases_clauses : bool;
@@ -423,7 +349,7 @@ type gen_config = {
           declarations in an interface file, together with an implementation file
           if needed.
        *)
-  test_unit_functions : bool;
+  test_trans_unit_functions : bool;
 }
 
 (** Returns the pair: (has opaque type decls, has opaque fun decls) *)
@@ -538,7 +464,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
              has_decr_clause def)
        fls);
     (* Insert unit tests if necessary *)
-    if config.test_unit_functions then
+    if config.test_trans_unit_functions then
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
@@ -665,13 +591,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
 (** Translate a module and write the synthesized code to an output file.
     TODO: rename to translate_crate
  *)
-let translate_module (filename : string) (dest_dir : string) (config : config)
-    (crate : A.crate) : unit =
+let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
+    unit =
   (* Translate the module to the pure AST *)
-  let trans_ctx, trans_types, trans_funs =
-    translate_module_to_pure config.eval_config config.mp_config
-      config.use_state config.backward_no_state_update crate
-  in
+  let trans_ctx, trans_types, trans_funs = translate_module_to_pure crate in
 
   (* Initialize the extraction context - for now we extract only to F*.
    * We initialize the names map by registering the keywords used in the
@@ -796,30 +719,26 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     }
   in
 
-  let use_state = config.use_state in
-
   (* Extract one or several files, depending on the configuration *)
-  if config.split_files then (
+  if !Config.split_files then (
     let base_gen_config =
       {
-        mp_config = config.mp_config;
-        use_state;
         extract_types = false;
-        extract_decreases_clauses = config.extract_decreases_clauses;
+        extract_decreases_clauses = !Config.extract_decreases_clauses;
         extract_template_decreases_clauses = false;
         extract_fun_decls = false;
         extract_transparent = true;
         extract_opaque = false;
         extract_state_type = false;
         interface = false;
-        test_unit_functions = false;
+        test_trans_unit_functions = false;
       }
     in
 
     (* Check if there are opaque types and functions - in which case we need
      * to split *)
     let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in
-    let has_opaque_types = has_opaque_types || use_state in
+    let has_opaque_types = has_opaque_types || !Config.use_state in
 
     (* Extract the types *)
     (* If there are opaque types, we extract in an interface *)
@@ -831,7 +750,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         base_gen_config with
         extract_types = true;
         extract_opaque = true;
-        extract_state_type = use_state;
+        extract_state_type = !Config.use_state;
         interface = has_opaque_types;
       }
     in
@@ -840,10 +759,10 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
     (* Extract the template clauses *)
     let needs_clauses_module =
-      config.extract_decreases_clauses
+      !Config.extract_decreases_clauses
       && not (A.FunDeclId.Set.is_empty rec_functions)
     in
-    (if needs_clauses_module && config.extract_template_decreases_clauses then
+    (if needs_clauses_module && !Config.extract_template_decreases_clauses then
      let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
      let clauses_module = module_name ^ ".Clauses.Template" in
      let clauses_config =
@@ -880,7 +799,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       {
         base_gen_config with
         extract_fun_decls = true;
-        test_unit_functions = config.test_unit_functions;
+        test_trans_unit_functions = !Config.test_trans_unit_functions;
       }
     in
     let clauses_module =
@@ -892,18 +811,16 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   else
     let gen_config =
       {
-        mp_config = config.mp_config;
-        use_state;
         extract_types = true;
-        extract_decreases_clauses = config.extract_decreases_clauses;
+        extract_decreases_clauses = !Config.extract_decreases_clauses;
         extract_template_decreases_clauses =
-          config.extract_template_decreases_clauses;
+          !Config.extract_template_decreases_clauses;
         extract_fun_decls = true;
         extract_transparent = true;
         extract_opaque = true;
-        extract_state_type = use_state;
+        extract_state_type = !Config.use_state;
         interface = false;
-        test_unit_functions = config.test_unit_functions;
+        test_trans_unit_functions = !Config.test_trans_unit_functions;
       }
     in
     (* Add the extension for F* *)
diff --git a/compiler/dune b/compiler/dune
index 0d340d59..85f4b75b 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -14,6 +14,7 @@
  (modules
   Assumed
   Collections
+  Config
   ConstStrings
   Contexts
   Cps