Address much stuff of the PR, throw exceptions at remaining places

16 files changed, 172 insertions, 112 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 1fbc916b..4f1e1506 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -219,13 +219,18 @@ type type_context = {
 
 type fun_context = {
   fun_decls : fun_decl FunDeclId.Map.t;
-  gid_conv : global_id_converter;
+}
+[@@deriving show]
+
+type global_context = {
+  global_decls : global_decl GlobalDeclId.Map.t;
 }
 [@@deriving show]
 
 type eval_ctx = {
   type_context : type_context;
   fun_context : fun_context;
+  global_context : global_context;
   type_vars : type_var list;
   env : env;
   ended_regions : RegionId.Set.t;
@@ -260,8 +265,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
   FunDeclId.Map.find fid ctx.fun_context.fun_decls
 
 (** TODO: make this more efficient with maps *)
-let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl =
-  ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid)
+let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl =
+  GlobalDeclId.Map.find gid ctx.global_context.global_decls
 
 (** Retrieve a variable's value in an environment *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5b39b0b7..2c53e45b 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -907,9 +907,12 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       | Func fun_id ->
           extract_function_call ctx fmt inside fun_id qualif.type_args args
       | Global global_id ->
+          failwith "TODO ExtractToFStar.ml:911"
+          (* Previous code:
           let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in
           let fun_id = Regular (A.Regular fid, None) in
           extract_function_call ctx fmt inside fun_id qualif.type_args args
+          *)
       | AdtCons adt_cons_id ->
           extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
       | Proj proj ->
@@ -1485,7 +1488,7 @@ let global_decl_to_body_name (decl : string) : string =
   assert (String.sub decl base_len 2 = "_c");
   (String.sub decl 0 base_len) ^ "_body"
 
-(** Print a definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+(** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
 let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
   (qualif : fun_decl_qualif) (name : string) (ty : ty)
   (extract_body : (F.formatter -> unit) Option.t)
@@ -1550,8 +1553,11 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (qualif : fun_decl_qualif) (def : fun_decl)
     : unit =
+  (* TODO Lookup LLBC decl *)
   (* Sanity checks for globals *)
-  assert (def.is_global);
+  assert (def.is_global_body);
+  failwith "TODO ExtractToFStar.ml:1559"
+  (* Previous code:
   assert (Option.is_none def.back_id);
   assert (List.length def.signature.inputs = 0);
   assert (List.length def.signature.doutputs = 1);
@@ -1578,6 +1584,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt ("eval_global " ^ body_name)
       ));
   F.pp_print_break fmt 0 0
+  *)
 
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index b1b8ccc2..034575c0 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -61,7 +61,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
              * (we check that it is successful in the extracted code: if it is
              *  not, it leads to a type-checking error in the generated files)
              *)
-            if f.is_global then () else
+            if f.is_global_body then () else
             can_fail := !can_fail || b
 
           method! visit_Assert env a =
@@ -98,7 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
             super#visit_Loop env loop
         end
       in
-      assert (not f.is_global || not use_state);
+      assert (not f.is_global_body || not use_state);
       (match f.body with
       | None ->
           (* Opaque function *)
@@ -108,7 +108,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
       (* We ignore on purpose functions that cannot fail: the result of the analysis
        * is not used yet to adjust the translation so that the functions which
        * syntactically can't fail don't use an error monad. *)
-      can_fail := not f.is_global
+      can_fail := not f.is_global_body
     in
     List.iter visit_fun d;
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f4f01ff8..3610d486 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -14,9 +14,9 @@ module SA = SymbolicAst
 let log = L.interpreter_log
 
 let compute_type_fun_contexts (m : M.llbc_module) :
-    C.type_context * C.fun_context =
+    C.type_context * C.fun_context * C.global_context =
   let type_decls_list, _ = M.split_declarations m.declarations in
-  let type_decls, fun_decls = M.compute_defs_maps m in
+  let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
   let type_decls_groups, _funs_defs_groups =
     M.split_declarations_to_group_maps m.declarations
   in
@@ -24,15 +24,20 @@ let compute_type_fun_contexts (m : M.llbc_module) :
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list
   in
   let type_context = { C.type_decls_groups; type_decls; type_infos } in
-  let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in
-  (type_context, fun_context)
-
-let initialize_eval_context (type_context : C.type_context)
-    (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx =
+  let fun_context = { C.fun_decls } in
+  let global_context = { C.global_decls } in
+  (type_context, fun_context, global_context)
+
+let initialize_eval_context
+    (type_context : C.type_context)
+    (fun_context : C.fun_context)
+    (global_context : C.global_context)
+    (type_vars : T.type_var list) : C.eval_ctx =
   C.reset_global_counters ();
   {
     C.type_context;
     C.fun_context;
+    C.global_context;
     C.type_vars;
     C.env = [ C.Frame ];
     C.ended_regions = T.RegionId.Set.empty;
@@ -51,8 +56,11 @@ let initialize_eval_context (type_context : C.type_context)
       - the list of symbolic values introduced for the input values
       - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun (type_context : C.type_context)
-    (fun_context : C.fun_context) (fdef : A.fun_decl) :
+let initialize_symbolic_context_for_fun
+    (type_context : C.type_context)
+    (fun_context : C.fun_context)
+    (global_context : C.global_context)
+    (fdef : A.fun_decl) :
     C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
@@ -67,7 +75,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
    * *)
   let sg = fdef.signature in
   (* Create the context *)
-  let ctx = initialize_eval_context type_context fun_context sg.type_params in
+  let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in
   (* Instantiate the signature *)
   let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
   let inst_sg = instantiate_fun_sig type_params sg in
@@ -204,7 +212,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
     - the symbolic AST generated by the symbolic execution
  *)
 let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
-    (type_context : C.type_context) (fun_context : C.fun_context)
+    (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) :
     V.symbolic_value list * SA.expression option =
   (* Debug *)
@@ -218,7 +226,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
 
   (* Create the evaluation context *)
   let ctx, input_svs, inst_sg =
-    initialize_symbolic_context_for_fun type_context fun_context fdef
+    initialize_symbolic_context_for_fun type_context fun_context global_context fdef
   in
 
   (* Create the continuation to finish the evaluation *)
@@ -285,8 +293,8 @@ module Test = struct
     assert (body.A.arg_count = 0);
 
     (* Create the evaluation context *)
-    let type_context, fun_context = compute_type_fun_contexts m in
-    let ctx = initialize_eval_context type_context fun_context [] in
+    let type_context, fun_context, global_context = compute_type_fun_contexts m in
+    let ctx = initialize_eval_context type_context fun_context global_context [] in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
@@ -330,7 +338,7 @@ module Test = struct
 
   (** 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)
+      (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context)
       (fdef : A.fun_decl) : unit =
     (* Debug *)
     log#ldebug
@@ -338,7 +346,7 @@ module Test = struct
 
     (* Evaluate *)
     let evaluate =
-      evaluate_function_symbolic config synthesize type_context fun_context fdef
+      evaluate_function_symbolic config synthesize type_context fun_context global_context fdef
     in
     (* Execute the forward function *)
     let _ = evaluate None in
@@ -368,12 +376,12 @@ module Test = struct
     in
     (* Filter the opaque functions *)
     let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
-    let type_context, fun_context = compute_type_fun_contexts m in
+    let type_context, fun_context, global_context = compute_type_fun_contexts m in
     let test_fun (def : A.fun_decl) : unit =
       (* 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 def
+      test_function_symbolic config synthesize type_context fun_context global_context def
     in
     List.iter test_fun no_loop_funs
 end
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 8f981174..6a0b81f3 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -832,8 +832,9 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
         (* Compose and apply *)
         comp cf_eval_rvalue cf_assign cf ctx
     | A.AssignGlobal { dst; global } ->
+        (* What codegen do we want ? *)
         let call : A.call = {
-          func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global);
+          func = A.Regular (failwith "TODO InterpretStatements.ml:837");
           region_args = [];
           type_args = [];
           args = [];
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 16733e20..aa9b0665 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -7,17 +7,6 @@ open Identifiers
 module FunDeclId = IdGen ()
 module GlobalDeclId = IdGen ()
 
-(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
-type global_id_converter = { fun_count : int }
-[@@deriving show]
-
-(** Converts a global id to its corresponding function id.
-    To do so, it adds the global id to the number of function declarations :
-    We have the bijection `global_id <=> fun_id + fun_id_count`.
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id =
-  FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count)
-
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
@@ -201,6 +190,14 @@ type fun_decl = {
   name : fun_name;
   signature : fun_sig;
   body : fun_body option;
-  is_global : bool;
+  is_global_body : bool;
+}
+[@@deriving show]
+
+type global_decl = {
+  def_id : GlobalDeclId.id;
+  body_id: FunDeclId.id;
+  name : global_name;
+  ty: ety;
 }
 [@@deriving show]
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index c157b667..f51c15be 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -540,7 +540,7 @@ let call_of_json (js : json) : (A.call, string) result =
         Ok { A.func; region_args; type_args; args; dest }
     | _ -> Error "")
 
-let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result =
+let rec statement_of_json (js : json) : (A.statement, string) result =
   combine_error_msgs js "statement_of_json"
     (match js with
     | `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
@@ -577,48 +577,49 @@ let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.st
         Ok (A.Continue i)
     | `String "Nop" -> Ok A.Nop
     | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json st1 gid_conv in
-        let* st2 = statement_of_json st2 gid_conv in
+        let* st1 = statement_of_json st1 in
+        let* st2 = statement_of_json st2 in
         Ok (A.Sequence (st1, st2))
     | `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
         let* op = operand_of_json op in
-        let* tgt = switch_targets_of_json tgt gid_conv in
+        let* tgt = switch_targets_of_json tgt in
         Ok (A.Switch (op, tgt))
     | `Assoc [ ("Loop", st) ] ->
-        let* st = statement_of_json st gid_conv in
+        let* st = statement_of_json st in
         Ok (A.Loop st)
     | _ -> Error "")
 
-and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
   combine_error_msgs js "switch_targets_of_json"
     (match js with
     | `Assoc [ ("If", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json st1 gid_conv in
-        let* st2 = statement_of_json st2 gid_conv in
+        let* st1 = statement_of_json st1 in
+        let* st2 = statement_of_json st2 in
         Ok (A.If (st1, st2))
     | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
         let* int_ty = integer_type_of_json int_ty in
         let* tgts =
-          list_of_json (pair_of_json
+            list_of_json (
+              pair_of_json
               (list_of_json scalar_value_of_json)
-              (fun js -> statement_of_json js gid_conv))
+              statement_of_json)
             tgts
         in
-        let* otherwise = statement_of_json otherwise gid_conv in
+        let* otherwise = statement_of_json otherwise in
         Ok (A.SwitchInt (int_ty, tgts, otherwise))
     | _ -> Error "")
 
-let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) : (A.fun_body, string) result =
   combine_error_msgs js "fun_body_of_json"
     (match js with
     | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] ->
         let* arg_count = int_of_json arg_count in
         let* locals = list_of_json var_of_json locals in
-        let* body = statement_of_json body gid_conv in
+        let* body = statement_of_json body in
         Ok { A.arg_count; locals; body }
     | _ -> Error "")
 
-let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
   combine_error_msgs js "fun_decl_of_json"
     (match js with
     | `Assoc
@@ -631,13 +632,24 @@ let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_dec
         let* def_id = A.FunDeclId.id_of_json def_id in
         let* name = fun_name_of_json name in
         let* signature = fun_sig_of_json signature in
-        let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
-        Ok { A.def_id; name; signature; body; is_global = false; }
+        let* body = option_of_json fun_body_of_json body in
+        Ok { A.def_id; name; signature; body; is_global_body = false; }
     | _ -> Error "")
 
+(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
+type global_id_converter = { fun_count : int }
+[@@deriving show]
+
+(** Converts a global id to its corresponding function id.
+    To do so, it adds the global id to the number of function declarations :
+    We have the bijection `global_id <=> fun_id + fun_id_count`.
+*)
+let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id =
+  A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count)
+
 (* Converts a global declaration to a function declaration.
  *)
-let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
+let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result =
   combine_error_msgs js "global_decl_of_json"
     (match js with
     | `Assoc
@@ -648,10 +660,10 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_
           ("body", body);
         ] ->
         let* global_id = A.GlobalDeclId.id_of_json def_id in
-        let def_id = A.global_to_fun_id gid_conv global_id in
+        let fun_id = global_to_fun_id gid_conv global_id in
         let* name = fun_name_of_json name in
         let* ty = ety_of_json ty in
-        let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
+        let* body = option_of_json fun_body_of_json body in
         let signature : A.fun_sig = {
           region_params = [];
           num_early_bound_regions = 0;
@@ -660,7 +672,8 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_
           inputs = [];
           output = TU.ety_no_regions_to_sty ty;
         } in
-        Ok { A.def_id; name; signature; body; is_global = true; }
+        Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; },
+            { A.def_id = fun_id; name; signature; body; is_global_body = true; })
     | _ -> Error "")
 
 let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
@@ -685,15 +698,18 @@ let fun_declaration_group_of_json (js : json) :
   combine_error_msgs js "fun_declaration_group_of_json"
     (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
-let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) :
+(* TODO Should a global declaration group be converted to its function bodies ?
+        It does not seems very clean.
+*)
+let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) :
     (M.fun_declaration_group, string) result =
   combine_error_msgs js "global_declaration_group_of_json"
     (g_declaration_group_of_json (fun js ->
         let* id = A.GlobalDeclId.id_of_json js in
-        Ok (A.global_to_fun_id gid_conv id)
+        Ok (global_to_fun_id gid_conv id)
       ) js)
 
-let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result
     =
   combine_error_msgs js "declaration_of_json"
     (match js with
@@ -726,19 +742,20 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
           ("globals", globals);
         ] ->
         let* fun_count = length_of_json_list functions in
-        let gid_conv = { A.fun_count = fun_count } in
+        let gid_conv = { fun_count } in
         let* name = string_of_json name in
         let* declarations =
           list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations
         in
-        let* types = list_of_json type_decl_of_json types in
-        let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in
+        let* types     = list_of_json type_decl_of_json types in
+        let* functions = list_of_json fun_decl_of_json functions in
         let* globals   = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+        let globals, global_bodies = List.split globals in
         Ok {
           M.name;
           declarations;
           types;
-          functions = functions @ globals;
-          gid_conv;
+          functions = functions @ global_bodies;
+          globals;
         }
     | _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index 149de020..2f640636 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -21,12 +21,12 @@ type llbc_module = {
   declarations : declaration_group list;
   types : type_decl list;
   functions : fun_decl list;
-  gid_conv : global_id_converter;
+  globals : global_decl list;
 }
 (** LLBC module - TODO: rename to crate *)
 
 let compute_defs_maps (m : llbc_module) :
-    type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t =
+    type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t =
   let types_map =
     List.fold_left
       (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
@@ -37,7 +37,12 @@ let compute_defs_maps (m : llbc_module) :
       (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
       FunDeclId.Map.empty m.functions
   in
-  (types_map, funs_map)
+  let globals_map =
+    List.fold_left
+      (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
+      GlobalDeclId.Map.empty m.globals
+  in
+  (types_map, funs_map, globals_map)
 
 (** Split a module's declarations between types and functions *)
 let split_declarations (decls : declaration_group list) :
diff --git a/src/Names.ml b/src/Names.ml
index 1308eccc..0db5291a 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -54,6 +54,8 @@ type type_name = name [@@deriving show, ord]
 
 type fun_name = name [@@deriving show, ord]
 
+type global_name = name [@@deriving show, ord]
+
 (** Filter the disambiguators equal to 0 in a name *)
 let filter_disambiguators_zero (n : name) : name =
   let pred (pe : path_elem) : bool =
diff --git a/src/Print.ml b/src/Print.ml
index 337116ec..6b11a3ff 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -13,6 +13,7 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
 
 let name_to_string (name : name) : string = Names.name_to_string name
 let fun_name_to_string (name : fun_name) : string = name_to_string name
+let global_name_to_string (name : global_name) : string = name_to_string name
 
 (** Pretty-printing for types *)
 module Types = struct
@@ -744,7 +745,8 @@ module LlbcAst = struct
       fun_name_to_string def.name
     in
     let global_decl_id_to_string def_id =
-      fun_decl_id_to_string (A.global_to_fun_id ctx.fun_context.gid_conv def_id)
+      let def = C.ctx_lookup_global_decl ctx def_id in
+      global_name_to_string def.name
     in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
@@ -762,7 +764,7 @@ module LlbcAst = struct
   let fun_decl_to_ast_formatter
       (type_decls : T.type_decl T.TypeDeclId.Map.t)
       (fun_decls : A.fun_decl A.FunDeclId.Map.t)
-      (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+      (global_decls : A.global_decl A.GlobalDeclId.Map.t)
       (fdef : A.fun_decl) :
       ast_formatter =
     let rvar_to_string r =
@@ -793,7 +795,8 @@ module LlbcAst = struct
       fun_name_to_string def.name
     in
     let global_decl_id_to_string def_id =
-      fun_decl_id_to_string (global_to_fun_id def_id)
+      let def = A.GlobalDeclId.Map.find def_id global_decls in
+      global_name_to_string def.name
     in
     {
       rvar_to_string;
@@ -1132,7 +1135,7 @@ module Module = struct
   let def_ctx_to_ast_formatter
       (type_context : T.type_decl T.TypeDeclId.Map.t)
       (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+      (global_context : A.global_decl A.GlobalDeclId.Map.t)
       (def : A.fun_decl) :
       PA.ast_formatter =
     let rvar_to_string vid =
@@ -1156,7 +1159,8 @@ module Module = struct
       fun_name_to_string def.name
     in
     let global_decl_id_to_string def_id =
-      fun_decl_id_to_string (global_to_fun_id def_id)
+      let def = A.GlobalDeclId.Map.find def_id global_context in
+      global_name_to_string def.name
     in
     let var_id_to_string vid =
       let var = V.VarId.nth (Option.get def.body).locals vid in
@@ -1187,21 +1191,20 @@ module Module = struct
   let fun_decl_to_string
       (type_context : T.type_decl T.TypeDeclId.Map.t)
       (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+      (global_context : A.global_decl A.GlobalDeclId.Map.t)
       (def : A.fun_decl) : string =
-    let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in
+    let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in
     PA.fun_decl_to_string fmt "" "  " def
 
   let module_to_string (m : M.llbc_module) : string =
-    let types_defs_map, funs_defs_map = M.compute_defs_maps m in
+    let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in
 
     (* The types *)
     let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
 
     (* The functions *)
     let fun_decls =
-      let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in
-      List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions
+      List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions
     in
 
     (* Put everything together *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index c13f967f..597330bf 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -62,6 +62,7 @@ let ast_to_type_formatter (fmt : ast_formatter) : type_formatter =
 
 let name_to_string = Print.name_to_string
 let fun_name_to_string = Print.fun_name_to_string
+let global_name_to_string = Print.global_name_to_string
 let option_to_string = Print.option_to_string
 let type_var_to_string = Print.Types.type_var_to_string
 let integer_type_to_string = Print.Types.integer_type_to_string
@@ -85,9 +86,10 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
    functions (there is a difference between the forward/backward functions...)
    while we only need those definitions to lookup proper names for the def ids.
 *)
-let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
+let mk_ast_formatter
+    (type_decls : T.type_decl TypeDeclId.Map.t)
     (fun_decls : A.fun_decl A.FunDeclId.Map.t)
-    (gid_conv : A.global_id_converter)
+    (global_decls : A.global_decl A.GlobalDeclId.Map.t)
     (type_params : type_var list) :
     ast_formatter =
   let type_var_id_to_string vid =
@@ -116,7 +118,8 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     fun_name_to_string def.name
   in
   let global_decl_id_to_string def_id =
-    fun_decl_id_to_string (A.global_to_fun_id gid_conv def_id)
+    let def = A.GlobalDeclId.Map.find def_id global_decls in
+    global_name_to_string def.name
   in
   {
     type_var_id_to_string;
diff --git a/src/Pure.ml b/src/Pure.ml
index b3be2040..5244b0bc 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -575,6 +575,6 @@ type fun_decl = {
           (to identify the forward/backward functions) later.
        *)
   signature : fun_sig;
-  is_global : bool;
+  is_global_body : bool;
   body : fun_body option;
 }
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index e58fec2a..7a10bb6b 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -83,14 +83,15 @@ type formatter = {
           - function id: this is especially useful to identify whether the
             function is an assumed function or a local function
           - function basename
+          - flag indicating if the function is a global
           - number of region groups
+          - region group information in case of a backward function
+            (`None` if forward function)
           - pair:
             - do we generate the forward function (it may have been filtered)?
             - the number of extracted backward functions (not necessarily equal
               to the number of region groups, because we may have filtered
               some of them)
-          - region group information in case of a backward function
-            (`None` if forward function)
           TODO: use the fun id for the assumed functions.
        *)
   decreases_clause_name : A.FunDeclId.id -> fun_name -> string;
@@ -599,7 +600,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let def_id = A.Regular def_id in
   let name =
-    ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs)
+    ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs)
   in
   (* Add the function name *)
   let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index a057b015..7d9e2906 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -70,7 +70,10 @@ type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdMap.t;  (** *)
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
-  gid_conv : A.global_id_converter;
+}
+
+type global_context = {
+  llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t;
 }
 
 type call_info = {
@@ -96,6 +99,7 @@ type call_info = {
 type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
+  global_context : global_context;
   fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   sg : fun_sig;
@@ -137,15 +141,15 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter =
   Print.LlbcAst.fun_decl_to_ast_formatter
     ctx.type_context.llbc_type_decls
     ctx.fun_context.llbc_fun_decls
-    (A.global_to_fun_id ctx.fun_context.gid_conv)
+    ctx.global_context.llbc_global_decls
     ctx.fun_decl
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
   let type_params = ctx.fun_decl.signature.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let gid_conv = ctx.fun_context.gid_conv in
-  PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params
+  let global_decls = ctx.global_context.llbc_global_decls in
+  PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
 
 let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
@@ -166,16 +170,16 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_params = sg.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let gid_conv = ctx.fun_context.gid_conv in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+  let global_decls = ctx.global_context.llbc_global_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let gid_conv = ctx.fun_context.gid_conv in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+  let global_decls = ctx.global_context.llbc_global_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
   PrintPure.fun_decl_to_string fmt def
 
 (* TODO: move *)
@@ -1666,7 +1670,6 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
   (* Lookup the signature *)
   let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in
   (* Translate the body, if there is *)
-  let is_global = def.A.is_global in
   let body =
     match body with
     | None -> None
@@ -1727,7 +1730,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         Some { inputs; inputs_lvs; body }
   in
   (* Assemble the declaration *)
-  let def = { def_id; back_id = bid; basename; signature; is_global; body } in
+  let def = { def_id; back_id = bid; basename; signature; is_global_body = def.is_global_body; body } in
   (* Debugging *)
   log#ldebug
     (lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index 9412b8b8..a6477e7f 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -63,10 +63,9 @@ let translate_function_to_symbolics (config : C.partial_config)
       ("translate_function_to_symbolics: "
       ^ Print.fun_name_to_string fdef.A.name));
 
-  let { type_context; fun_context } = trans_ctx in
+  let { type_context; fun_context; global_context } = trans_ctx in
   let fun_context = {
     C.fun_decls = fun_context.fun_decls;
-    C.gid_conv = fun_context.gid_conv;
   } in
 
   match fdef.body with
@@ -76,7 +75,8 @@ 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 config synthesize
+            type_context fun_context global_context
             fdef gid
         in
         (inputs, Option.get symb)
@@ -110,7 +110,7 @@ let translate_function_to_pure (config : C.partial_config)
     (lazy
       ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
 
-  let { type_context; fun_context } = trans_ctx in
+  let { type_context; fun_context; global_context } = trans_ctx in
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs, if the function is transparent *)
@@ -142,7 +142,10 @@ let translate_function_to_pure (config : C.partial_config)
       SymbolicToPure.llbc_fun_decls = fun_context.fun_decls;
       fun_sigs;
       fun_infos = fun_context.fun_infos;
-      gid_conv = fun_context.gid_conv;
+    }
+  in
+  let global_context = {
+      SymbolicToPure.llbc_global_decls = global_context.global_decls
     }
   in
   let ctx =
@@ -156,6 +159,7 @@ let translate_function_to_pure (config : C.partial_config)
       state_var;
       type_context;
       fun_context;
+      global_context;
       fun_decl = fdef;
       forward_inputs = [];
       (* Empty for now *)
@@ -293,14 +297,13 @@ let translate_module_to_pure (config : C.partial_config)
   log#ldebug (lazy "translate_module_to_pure");
 
   (* Compute the type and function contexts *)
-  let type_context, fun_context = compute_type_fun_contexts m in
+  let type_context, fun_context, global_context = compute_type_fun_contexts m in
   let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
   let fun_context = {
     fun_decls = fun_context.fun_decls;
     fun_infos;
-    gid_conv = m.gid_conv;
   } in
-  let trans_ctx = { type_context; fun_context } in
+  let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
   let type_decls = SymbolicToPure.translate_type_decls m.types in
@@ -495,7 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          if
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
-         then if def.is_global
+         then if def.is_global_body
           then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def
           else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
         )
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 047219ad..e77445cd 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -16,11 +16,16 @@ type type_context = C.type_context [@@deriving show]
 type fun_context = {
   fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
-  gid_conv : A.global_id_converter;
 }
 [@@deriving show]
 
-type trans_ctx = { type_context : type_context; fun_context : fun_context }
+type global_context = C.global_context [@@deriving show]
+
+type trans_ctx = {
+  type_context : type_context;
+  fun_context : fun_context;
+  global_context : global_context
+}
 
 type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list
 
@@ -40,16 +45,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
   let type_params = sg.type_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
-  let gid_conv = ctx.fun_context.gid_conv in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+  let global_decls = ctx.global_context.global_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
-  let gid_conv = ctx.fun_context.gid_conv in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
+  let global_decls = ctx.global_context.global_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
   PrintPure.fun_decl_to_string fmt def
 
 let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =