concrete & symbolic evaluation work with new LLBC format

24 files changed, 380 insertions, 308 deletions

diff --git a/Makefile b/Makefile
index 4dc1475b..0fc3fcf4 100644
--- a/Makefile
+++ b/Makefile
@@ -48,7 +48,7 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk
 trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
 trans-nll-betree_nll: SUBDIR:=misc
 
-trans-constants: TRANS_OPTIONS += -no-split-files -no-state -no-decreases-clauses
+trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
 
 trans-external: TRANS_OPTIONS +=
diff --git a/src/Contexts.ml b/src/Contexts.ml
index bbf5b8f3..1fbc916b 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,7 +1,6 @@
 open Types
 open Values
 open LlbcAst
-open FunIdentifier
 module V = Values
 open ValuesUtils
 module M = Modules
@@ -218,7 +217,11 @@ type type_context = {
 }
 [@@deriving show]
 
-type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
+type fun_context = {
+  fun_decls : fun_decl FunDeclId.Map.t;
+  gid_conv : global_id_converter;
+}
+[@@deriving show]
 
 type eval_ctx = {
   type_context : type_context;
@@ -256,6 +259,10 @@ let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
 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)
+
 (** Retrieve a variable's value in an environment *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
   (* We take care to stop at the end of current frame: different variables
diff --git a/src/Expressions.ml b/src/Expressions.ml
index f1a4a8c3..6645a77f 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -1,6 +1,5 @@
 open Types
 open Values
-open FunIdentifier
 
 type field_proj_kind =
   | ProjAdt of TypeDeclId.id * VariantId.id option
@@ -73,31 +72,11 @@ let all_binops =
     Shr;
   ]
 
-(** Constant value for an operand
-
-    It is a bit annoying, but rustc treats some ADT and tuple instances as
-    constants when generating MIR:
-    - an enumeration with one variant and no fields is a constant.
-    - a structure with no field is a constant.
-    - sometimes, Rust stores the initialization of an ADT as a constant
-      (if all the fields are constant) rather than as an aggregated value
-
-    For our translation, we use the following enumeration to encode those
-    special cases in assignments. They are converted to "normal" values
-    when evaluating the assignment (which is why we don't put them in the
-    [ConstantValue] enumeration).
- *)
-type operand_constant_value =
-  | ConstantValue of constant_value
-  | ConstantId of FunDeclId.id
-  | ConstantAdt of VariantId.id option * operand_constant_value list
-[@@deriving show]
-
 (* TODO: symplify the operand constant values *)
 type operand =
   | Copy of place
   | Move of place
-  | Constant of ety * operand_constant_value
+  | Constant of ety * constant_value
 [@@deriving show]
 
 (** An aggregated ADT.
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index b85c146b..b89579b5 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,7 +6,6 @@ open PureUtils
 open TranslateCore
 open PureToExtract
 open StringUtils
-open FunIdentifier
 module F = Format
 
 (** A qualifier for a type definition.
@@ -315,7 +314,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string =
+  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string =
     let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
     let suffix = "_decreases" in
diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml
deleted file mode 100644
index 956fce3f..00000000
--- a/src/FunIdentifier.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-open Identifiers
-module FunDeclId = IdGen ()
-module GlobalDeclId = IdGen ()
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index cf2e0bd6..dc205eb9 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -9,7 +9,6 @@
 
 open LlbcAst
 open Modules
-open FunIdentifier
 
 type fun_info = {
   can_fail : bool;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 702aeea6..5affea4c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,5 +1,4 @@
 open Cps
-open FunIdentifier
 open InterpreterUtils
 open InterpreterProjectors
 open InterpreterBorrows
@@ -25,7 +24,7 @@ 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 } 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)
@@ -256,9 +255,9 @@ module Test = struct
       environment.
    *)
   let test_unit_function (config : C.partial_config) (m : M.llbc_module)
-      (fid : FunDeclId.id) : unit =
+      (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
-    let fdef = FunDeclId.nth m.functions fid in
+    let fdef = A.FunDeclId.nth m.functions fid in
     let body = Option.get fdef.body in
 
     (* Debug *)
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index ee26d00d..57ee0526 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -71,68 +71,23 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool)
   in
   comp cc read_place cf ctx
 
-(** Convert an operand constant operand value to a typed value *)
-let rec eval_operand_constant_value (ty : T.ety)
-    (cv : E.operand_constant_value) (cf : V.typed_value -> m_fun) : m_fun =
-  fun ctx ->
-    (* Check the type while converting - we actually need some information
-    * contained in the type *)
-    log#ldebug
-      (lazy
-        ("eval_operand_constant_value:" ^ "\n- ty: "
-      ^ ety_to_string ctx ty ^ "\n- cv: "
-        ^ operand_constant_value_to_string ctx cv));
-    match (ty, cv) with
-    (* Adt *)
-    | ( T.Adt (adt_id, region_params, type_params),
-        ConstantAdt (variant_id, field_values) ) ->
-        assert (region_params = []);
-        (* Compute the types of the fields *)
-        let field_tys =
-          match adt_id with
-          | T.AdtId def_id ->
-              let def = C.ctx_lookup_type_decl ctx def_id in
-              assert (def.region_params = []);
-              Subst.type_decl_get_instantiated_field_etypes def variant_id
-                type_params
-          | T.Tuple -> type_params
-          | T.Assumed _ -> failwith "Unreachable"
-        in
-        let adt_cf = fun fields ctx ->
-          let value = V.Adt { variant_id; field_values = fields } in
-          cf { value; ty } ctx
-        in
-        (* Map the field values & types to the continuation above *)
-        fold_left_apply_continuation
-          (fun (ty, v) cf ctx -> eval_operand_constant_value ty v cf ctx)
-          (List.combine field_tys field_values)
-          adt_cf ctx
-    (* Scalar, boolean... *)
-    | T.Bool, ConstantValue (Bool v)   -> cf { V.value = V.Concrete (Bool v);   ty } ctx
-    | T.Char, ConstantValue (Char v)   -> cf { V.value = V.Concrete (Char v);   ty } ctx
-    | T.Str,  ConstantValue (String v) -> cf { V.value = V.Concrete (String v); ty } ctx
-    | T.Integer int_ty, ConstantValue (V.Scalar v) ->
-        (* Check the type and the ranges *)
-        assert (int_ty = v.int_ty);
-        assert (check_scalar_value_in_range v);
-        cf { V.value = V.Concrete (V.Scalar v); ty } ctx
-    (* Constant expression identifier *)
-    | ty, ConstantId id ->
-        let dest = mk_fresh_symbolic_value V.FunCallRet (ety_no_regions_to_rty ty) in
-
-        (* Call the continuation *)
-        let expr = cf (mk_typed_value_from_symbolic_value dest) ctx in
-        
-        (* TODO Should it really be a new call ID ? *)
-        let call = SA.Fun (LA.Regular id, C.fresh_fun_call_id ()) in
-          
-        S.synthesize_function_call call [] [] [] []
-          dest None(*TODO meta-info*) expr
-
-    (* Remaining cases (invalid) - listing as much as we can on purpose
-      (allows to catch errors at compilation if the definitions change) *)
-    | _, ConstantAdt _ | _, ConstantValue _ ->
-        failwith "Improperly typed constant value"
+(** Convert a constant operand value to a typed value *)
+let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_value =
+  (* Check the type while converting -
+   * we actually need some information contained in the type *)
+  match (ty, cv) with
+  (* Scalar, boolean... *)
+  | T.Bool, (Bool v)   -> { V.value = V.Concrete (Bool v);   ty }
+  | T.Char, (Char v)   -> { V.value = V.Concrete (Char v);   ty }
+  | T.Str,  (String v) -> { V.value = V.Concrete (String v); ty }
+  | T.Integer int_ty, (V.Scalar v) ->
+      (* Check the type and the ranges *)
+      assert (int_ty = v.int_ty);
+      assert (check_scalar_value_in_range v);
+      { V.value = V.Concrete (V.Scalar v); ty }
+  (* Remaining cases (invalid) - listing as much as we can on purpose
+    (allows to catch errors at compilation if the definitions change) *)
+  | _, _ -> failwith "Improperly typed constant value"
 
 (** Prepare the evaluation of an operand.
 
@@ -172,7 +127,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand)
    fun ctx ->
     match op with
     | Expressions.Constant (ty, cv) ->
-        eval_operand_constant_value ty cv cf ctx
+        cf (typecheck_constant_value ty cv) ctx
     | Expressions.Copy p ->
         (* Access the value *)
         let access = Read in
@@ -205,7 +160,7 @@ let eval_operand (config : C.config) (op : E.operand)
      ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) -> eval_operand_constant_value ty cv cf ctx
+  | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c7308720..e5564d59 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -7,7 +7,6 @@ module A = LlbcAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
-open FunIdentifier
 module Inv = Invariants
 module S = SynthesizeSymbolic
 open Errors
@@ -822,6 +821,15 @@ 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 } ->
+        let call : A.call = {
+          func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global);
+          region_args = [];
+          type_args = [];
+          args = [];
+          dest = { var_id = dst; projection = [] };
+        } in
+        eval_function_call config call cf ctx
     | A.FakeRead p ->
         let expand_prim_copy = false in
         let cf_prepare = prepare_rplace config expand_prim_copy Read p in
@@ -1002,7 +1010,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
         call.args call.dest
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
@@ -1080,7 +1088,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
   cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
@@ -1301,7 +1309,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
   match config.mode with
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 7a2e22f7..47323cc2 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -33,8 +33,6 @@ let typed_value_to_string = PA.typed_value_to_string
 
 let typed_avalue_to_string = PA.typed_avalue_to_string
 
-let operand_constant_value_to_string = PA.operand_constant_value_to_string
-
 let place_to_string = PA.place_to_string
 
 let operand_to_string = PA.operand_to_string
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 4324586d..16733e20 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -2,7 +2,21 @@ open Names
 open Types
 open Values
 open Expressions
-open FunIdentifier
+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 *)
@@ -34,6 +48,12 @@ type assumed_fun_id =
 type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
 [@@deriving show, ord]
 
+type assign_global = {
+  dst : VarId.id;
+  global : GlobalDeclId.id;
+}
+[@@deriving show]
+
 type assertion = { cond : operand; expected : bool } [@@deriving show]
 
 type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
@@ -75,6 +95,8 @@ class ['self] iter_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
+    method visit_assign_global : 'env -> assign_global -> unit = fun _ _ -> ()
+
     method visit_place : 'env -> place -> unit = fun _ _ -> ()
 
     method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
@@ -97,6 +119,8 @@ class ['self] map_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
+    method visit_assign_global : 'env -> assign_global -> assign_global = fun _ x -> x
+
     method visit_place : 'env -> place -> place = fun _ x -> x
 
     method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
@@ -118,6 +142,7 @@ class ['self] map_statement_base =
 
 type statement =
   | Assign of place * rvalue
+  | AssignGlobal of assign_global
   | FakeRead of place
   | SetDiscriminant of place * VariantId.id
   | Drop of place
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index bc4236cf..84e8e00f 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -1,6 +1,5 @@
 open LlbcAst
 open Utils
-open FunIdentifier
 module T = Types
 
 (** Check if a [statement] contains loops *)
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 14333088..a074ed1e 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -11,7 +11,6 @@
 open Yojson.Basic
 open Names
 open OfJsonBasic
-open FunIdentifier
 module T = Types
 module V = Values
 module S = Scalars
@@ -19,6 +18,7 @@ module M = Modules
 module E = Expressions
 module A = LlbcAst
 module TU = TypesUtils
+module AU = LlbcAstUtils
 
 (* The default logger *)
 let log = Logging.llbc_of_json_logger
@@ -227,14 +227,6 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result =
           }
     | _ -> Error "")
 
-(* Converts a global ID to its corresponding function ID.
-   To do so, it adds the global ID to the number of function declarations.
-*)
-let global_id_of_json (js: json) (fun_count: int) : (FunDeclId.id, string) result =
-  combine_error_msgs js "global_id_of_json"
-    (let* gid = FunDeclId.id_of_json js in
-      Ok (FunDeclId.of_int ((FunDeclId.to_int gid) + fun_count)))
-
 let var_of_json (js : json) : (A.var, string) result =
   combine_error_msgs js "var_of_json"
     (match js with
@@ -308,23 +300,6 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
         raise (Failure ("Scalar value not in range: " ^ V.show_scalar_value sv)));
       res
 
-let constant_value_of_json (js : json) : (V.constant_value, string) result =
-  combine_error_msgs js "constant_value_of_json"
-    (match js with
-    | `Assoc [ ("Scalar", scalar_value) ] ->
-        let* scalar_value = scalar_value_of_json scalar_value in
-        Ok (V.Scalar scalar_value)
-    | `Assoc [ ("Bool", v) ] ->
-        let* v = bool_of_json v in
-        Ok (V.Bool v)
-    | `Assoc [ ("Char", v) ] ->
-        let* v = char_of_json v in
-        Ok (V.Char v)
-    | `Assoc [ ("String", v) ] ->
-        let* v = string_of_json v in
-        Ok (V.String v)
-    | _ -> Error "")
-
 let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
   combine_error_msgs js "field_proj_kind_of_json"
     (match js with
@@ -403,25 +378,30 @@ let binop_of_json (js : json) : (E.binop, string) result =
   | `String "Shr" -> Ok E.Shr
   | _ -> Error ("binop_of_json failed on:" ^ show js)
 
-let rec operand_constant_value_of_json (js : json) (fun_count : int) :
-    (E.operand_constant_value, string) result =
-  combine_error_msgs js "operand_constant_value_of_json"
+let constant_value_of_json (js : json) : (V.constant_value, string) result =
+  combine_error_msgs js "constant_value_of_json"
     (match js with
+    (* This indirection is because Charon still export the type OperandConstantValue,
+      * which had other variants than ConstantValue before.
+      *)
     | `Assoc [ ("ConstantValue", `List [ cv ]) ] ->
-        let* cv = constant_value_of_json cv in
-        Ok (E.ConstantValue cv)
-    | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] ->
-        let* variant_id = option_of_json T.VariantId.id_of_json variant_id in
-        let* field_values =
-          list_of_json (fun js -> operand_constant_value_of_json js fun_count) field_values
-        in
-        Ok (E.ConstantAdt (variant_id, field_values))
-    | `Assoc [ ("ConstantIdentifier", `List [gid]) ] ->
-        let* id = global_id_of_json gid fun_count in
-        Ok (E.ConstantId id)
-    | _ -> Error "")
-
-let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
+        (match cv with
+          | `Assoc [ ("Scalar", scalar_value) ] ->
+              let* scalar_value = scalar_value_of_json scalar_value in
+              Ok (V.Scalar scalar_value)
+          | `Assoc [ ("Bool", v) ] ->
+              let* v = bool_of_json v in
+              Ok (V.Bool v)
+          | `Assoc [ ("Char", v) ] ->
+              let* v = char_of_json v in
+              Ok (V.Char v)
+          | `Assoc [ ("String", v) ] ->
+              let* v = string_of_json v in
+              Ok (V.String v)
+          | _ -> Error "")
+    | _ -> Error "")
+  
+let operand_of_json (js : json) : (E.operand, string) result =
   combine_error_msgs js "operand_of_json"
     (match js with
     | `Assoc [ ("Copy", place) ] ->
@@ -432,7 +412,7 @@ let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
         Ok (E.Move place)
     | `Assoc [ ("Const", `List [ ty; cv ]) ] ->
         let* ty = ety_of_json ty in
-        let* cv = operand_constant_value_of_json cv fun_count in
+        let* cv = constant_value_of_json cv in
         Ok (E.Constant (ty, cv))
     | _ -> Error "")
 
@@ -455,11 +435,11 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
         Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys))
     | _ -> Error "")
 
-let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result =
+let rvalue_of_json (js : json) : (E.rvalue, string) result =
   combine_error_msgs js "rvalue_of_json"
     (match js with
     | `Assoc [ ("Use", op) ] ->
-        let* op = operand_of_json op fun_count in
+        let* op = operand_of_json op in
         Ok (E.Use op)
     | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
         let* place = place_of_json place in
@@ -467,19 +447,19 @@ let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result =
         Ok (E.Ref (place, borrow_kind))
     | `Assoc [ ("UnaryOp", `List [ unop; op ]) ] ->
         let* unop = unop_of_json unop in
-        let* op = operand_of_json op fun_count in
+        let* op = operand_of_json op in
         Ok (E.UnaryOp (unop, op))
     | `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] ->
         let* binop = binop_of_json binop in
-        let* op1 = operand_of_json op1 fun_count in
-        let* op2 = operand_of_json op2 fun_count in
+        let* op1 = operand_of_json op1 in
+        let* op2 = operand_of_json op2 in
         Ok (E.BinaryOp (binop, op1, op2))
     | `Assoc [ ("Discriminant", place) ] ->
         let* place = place_of_json place in
         Ok (E.Discriminant place)
     | `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] ->
         let* aggregate_kind = aggregate_kind_of_json aggregate_kind in
-        let* ops = list_of_json (fun js -> operand_of_json js fun_count) ops in
+        let* ops = list_of_json operand_of_json ops in
         Ok (E.Aggregate (aggregate_kind, ops))
     | _ -> Error "")
 
@@ -502,18 +482,18 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result =
   combine_error_msgs js "fun_id_of_json"
     (match js with
     | `Assoc [ ("Regular", id) ] ->
-        let* id = FunDeclId.id_of_json id in
+        let* id = A.FunDeclId.id_of_json id in
         Ok (A.Regular id)
     | `Assoc [ ("Assumed", fid) ] ->
         let* fid = assumed_fun_id_of_json fid in
         Ok (A.Assumed fid)
     | _ -> Error "")
 
-let assertion_of_json (js : json) (fun_count : int) : (A.assertion, string) result =
+let assertion_of_json (js : json) : (A.assertion, string) result =
   combine_error_msgs js "assertion_of_json"
     (match js with
     | `Assoc [ ("cond", cond); ("expected", expected) ] ->
-        let* cond = operand_of_json cond fun_count in
+        let* cond = operand_of_json cond in
         let* expected = bool_of_json expected in
         Ok { A.cond; expected }
     | _ -> Error "")
@@ -547,7 +527,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
           }
     | _ -> Error "")
 
-let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
+let call_of_json (js : json) : (A.call, string) result =
   combine_error_msgs js "call_of_json"
     (match js with
     | `Assoc
@@ -561,18 +541,22 @@ let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
         let* func = fun_id_of_json func in
         let* region_args = list_of_json erased_region_of_json region_args in
         let* type_args = list_of_json ety_of_json type_args in
-        let* args = list_of_json (fun js -> operand_of_json js fun_count) args in
+        let* args = list_of_json operand_of_json args in
         let* dest = place_of_json dest in
         Ok { A.func; region_args; type_args; args; dest }
     | _ -> Error "")
 
-let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) result =
+let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result =
   combine_error_msgs js "statement_of_json"
     (match js with
     | `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
         let* place = place_of_json place in
-        let* rvalue = rvalue_of_json rvalue fun_count in
+        let* rvalue = rvalue_of_json rvalue in
         Ok (A.Assign (place, rvalue))
+    | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] ->
+        let* dst = V.VarId.id_of_json dst in
+        let* global = A.GlobalDeclId.id_of_json global in
+        Ok (A.AssignGlobal { dst; global })
     | `Assoc [ ("FakeRead", place) ] ->
         let* place = place_of_json place in
         Ok (A.FakeRead place)
@@ -584,10 +568,10 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
         let* place = place_of_json place in
         Ok (A.Drop place)
     | `Assoc [ ("Assert", assertion) ] ->
-        let* assertion = assertion_of_json assertion fun_count in
+        let* assertion = assertion_of_json assertion in
         Ok (A.Assert assertion)
     | `Assoc [ ("Call", call) ] ->
-        let* call = call_of_json call fun_count in
+        let* call = call_of_json call in
         Ok (A.Call call)
     | `String "Panic" -> Ok A.Panic
     | `String "Return" -> Ok A.Return
@@ -599,48 +583,48 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
         Ok (A.Continue i)
     | `String "Nop" -> Ok A.Nop
     | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json st1 fun_count in
-        let* st2 = statement_of_json st2 fun_count in
+        let* st1 = statement_of_json st1 gid_conv in
+        let* st2 = statement_of_json st2 gid_conv in
         Ok (A.Sequence (st1, st2))
     | `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
-        let* op = operand_of_json op fun_count in
-        let* tgt = switch_targets_of_json tgt fun_count in
+        let* op = operand_of_json op in
+        let* tgt = switch_targets_of_json tgt gid_conv in
         Ok (A.Switch (op, tgt))
     | `Assoc [ ("Loop", st) ] ->
-        let* st = statement_of_json st fun_count in
+        let* st = statement_of_json st gid_conv in
         Ok (A.Loop st)
     | _ -> Error "")
 
-and switch_targets_of_json (js : json) (fun_count : int) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (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 fun_count in
-        let* st2 = statement_of_json st2 fun_count in
+        let* st1 = statement_of_json st1 gid_conv in
+        let* st2 = statement_of_json st2 gid_conv 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 scalar_value_of_json)
-              (fun js -> statement_of_json js fun_count))
+              (fun js -> statement_of_json js gid_conv))
             tgts
         in
-        let* otherwise = statement_of_json otherwise fun_count in
+        let* otherwise = statement_of_json otherwise gid_conv in
         Ok (A.SwitchInt (int_ty, tgts, otherwise))
     | _ -> Error "")
 
-let fun_body_of_json (js : json) (fun_count : int) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (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 fun_count in
+        let* body = statement_of_json body gid_conv in
         Ok { A.arg_count; locals; body }
     | _ -> Error "")
 
-let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
   combine_error_msgs js "fun_decl_of_json"
     (match js with
     | `Assoc
@@ -650,20 +634,16 @@ let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result
           ("signature", signature);
           ("body", body);
         ] ->
-        let* def_id = FunDeclId.id_of_json def_id in
+        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 fun_count) body 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; }
     | _ -> Error "")
 
-
 (* Converts a global declaration to a function declaration.
-   
-A.fun_sig
-ety_no_regions_to_rty
-*)
-let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) result =
+ *)
+let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
   combine_error_msgs js "global_decl_of_json"
     (match js with
     | `Assoc
@@ -673,10 +653,11 @@ let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) resu
           ("type_", type_);
           ("body", body);
         ] ->
-        let* def_id = global_id_of_json def_id fun_count in
+        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* name = fun_name_of_json name in
         let* type_ = ety_of_json type_ in
-        let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in
+        let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
         let signature : A.fun_sig = {
           region_params = [];
           num_early_bound_regions = 0;
@@ -708,14 +689,17 @@ let type_declaration_group_of_json (js : json) :
 let fun_declaration_group_of_json (js : json) :
     (M.fun_declaration_group, string) result =
   combine_error_msgs js "fun_declaration_group_of_json"
-    (g_declaration_group_of_json FunDeclId.id_of_json js)
+    (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
-let global_declaration_group_of_json (js : json) (fun_count: int) :
+let global_declaration_group_of_json (js : json) (gid_conv : A.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 -> global_id_of_json js fun_count) js)
+    (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)
+      ) js)
 
-let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result
     =
   combine_error_msgs js "declaration_of_json"
     (match js with
@@ -726,7 +710,7 @@ let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_grou
         let* decl = fun_declaration_group_of_json decl in
         Ok (M.Fun decl)
     | `Assoc [ ("Global", `List [ decl ]) ] ->
-        let* decl = global_declaration_group_of_json decl fun_count in
+        let* decl = global_declaration_group_of_json decl gid_conv in
         Ok (M.Fun decl)
     | _ -> Error "")
 
@@ -748,12 +732,19 @@ 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* name = string_of_json name in
         let* declarations =
-          list_of_json (fun js -> declaration_group_of_json js fun_count) 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 fun_count) functions in
-        let* globals   = list_of_json (fun js -> global_decl_of_json js fun_count) globals in
-        Ok { M.name; declarations; types; functions = functions @ globals }
+        let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in
+        let* globals   = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+        Ok {
+          M.name;
+          declarations;
+          types;
+          functions = functions @ globals;
+          gid_conv;
+        }
     | _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index 6d0cf70c..b0e8878d 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,6 +1,5 @@
 open Types
 open LlbcAst
-open FunIdentifier
 
 type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
 [@@deriving show]
@@ -21,6 +20,7 @@ type llbc_module = {
   declarations : declaration_group list;
   types : type_decl list;
   functions : fun_decl list;
+  gid_conv : global_id_converter;
 }
 (** LLBC module - TODO: rename to crate *)
 
diff --git a/src/Print.ml b/src/Print.ml
index 9e2ff3cd..722f76ce 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,5 +1,4 @@
 open Names
-open FunIdentifier
 module T = Types
 module TU = TypesUtils
 module V = Values
@@ -686,7 +685,8 @@ module LlbcAst = struct
     var_id_to_string : V.VarId.id -> string;
     adt_field_names :
       T.TypeDeclId.id -> T.VariantId.id option -> string list option;
-    fun_decl_id_to_string : FunDeclId.id -> string;
+    fun_decl_id_to_string : A.FunDeclId.id -> string;
+    global_decl_id_to_string : A.GlobalDeclId.id -> string;
   }
 
   let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
@@ -743,6 +743,9 @@ module LlbcAst = struct
       let def = C.ctx_lookup_fun_decl ctx def_id in
       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)
+    in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
       r_to_string = ctx_fmt.PV.r_to_string;
@@ -753,10 +756,14 @@ module LlbcAst = struct
       adt_field_names = ctx_fmt.PV.adt_field_names;
       adt_field_to_string;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
-  let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
-      (fun_decls : A.fun_decl FunDeclId.Map.t) (fdef : A.fun_decl) :
+  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)
+      (fdef : A.fun_decl) :
       ast_formatter =
     let rvar_to_string r =
       let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -782,9 +789,12 @@ module LlbcAst = struct
     let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in
     let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in
     let fun_decl_id_to_string def_id =
-      let def = FunDeclId.Map.find def_id fun_decls in
+      let def = A.FunDeclId.Map.find def_id fun_decls in
       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)
+    in
     {
       rvar_to_string;
       r_to_string;
@@ -795,6 +805,7 @@ module LlbcAst = struct
       adt_field_names;
       adt_field_to_string;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
   let rec projection_to_string (fmt : ast_formatter) (inside : string)
@@ -860,36 +871,13 @@ module LlbcAst = struct
     | E.Shl -> "<<"
     | E.Shr -> ">>"
 
-  let rec operand_constant_value_to_string (fmt : ast_formatter)
-      (cv : E.operand_constant_value) : string =
-    match cv with
-    | E.ConstantId id -> fmt.fun_decl_id_to_string id
-    | E.ConstantValue cv -> PV.constant_value_to_string cv
-    | E.ConstantAdt (variant_id, field_values) ->
-        (* This is a bit annoying, because we don't have context information
-         * to convert the ADT to a value, so we do the best we can in the
-         * simplest manner. Anyway, those printing utilitites are only used
-         * for debugging, and complex constant values are not common.
-         * We might want to store type information in the operand constant values
-         * in the future.
-         *)
-        let variant_id = option_to_string T.VariantId.to_string variant_id in
-        let field_values =
-          List.map (operand_constant_value_to_string fmt) field_values
-        in
-        "ConstantAdt " ^ variant_id ^ " {"
-        ^ String.concat ", " field_values
-        ^ "}"
-
   let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
     match op with
     | E.Copy p -> "copy " ^ place_to_string fmt p
     | E.Move p -> "move " ^ place_to_string fmt p
     | E.Constant (ty, cv) ->
-        (* For clarity, we also print the typing information: see the comment in
-         * [operand_constant_value_to_string] *)
         "("
-        ^ operand_constant_value_to_string fmt cv
+        ^ PV.constant_value_to_string cv
         ^ " : "
         ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
         ^ ")"
@@ -950,6 +938,8 @@ module LlbcAst = struct
     match st with
     | A.Assign (p, rv) ->
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
+    | A.AssignGlobal { dst; global } ->
+        indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
     | A.FakeRead p -> "fake_read " ^ place_to_string fmt p
     | A.SetDiscriminant (p, variant_id) ->
         (* TODO: improve this to lookup the variant name by using the def id *)
@@ -1139,8 +1129,11 @@ module Module = struct
 
   (** Generate an [ast_formatter] by using a definition context in combination
       with the variables local to a function's definition *)
-  let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) :
+  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)
+      (def : A.fun_decl) :
       PA.ast_formatter =
     let rvar_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1159,9 +1152,12 @@ module Module = struct
       name_to_string def.name
     in
     let fun_decl_id_to_string def_id =
-      let def = FunDeclId.Map.find def_id fun_context in
+      let def = A.FunDeclId.Map.find def_id fun_context in
       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)
+    in
     let var_id_to_string vid =
       let var = V.VarId.nth (Option.get def.body).locals vid in
       PA.var_to_string var
@@ -1183,13 +1179,17 @@ module Module = struct
       var_id_to_string;
       adt_field_names;
       fun_decl_id_to_string;
+      global_decl_id_to_string;
     }
 
   (** This function pretty-prints a function definition by using a definition
       context *)
-  let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : string =
-    let fmt = def_ctx_to_ast_formatter type_context fun_context def in
+  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)
+      (def : A.fun_decl) : string =
+    let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in
     PA.fun_decl_to_string fmt "" "  " def
 
   let module_to_string (m : M.llbc_module) : string =
@@ -1200,7 +1200,8 @@ module Module = struct
 
     (* The functions *)
     let fun_decls =
-      List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions
+      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
     in
 
     (* Put everything together *)
@@ -1257,11 +1258,6 @@ module EvalCtxLlbcAst = struct
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_avalue_to_string fmt v
 
-  let operand_constant_value_to_string (ctx : C.eval_ctx)
-      (cv : E.operand_constant_value) : string =
-    let fmt = PA.eval_ctx_to_ast_formatter ctx in
-    PA.operand_constant_value_to_string fmt cv
-
   let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
     let fmt = PA.eval_ctx_to_ast_formatter ctx in
     PA.place_to_string fmt op
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 8864dafe..ea9bf2ab 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -2,7 +2,6 @@
 
 open Pure
 open PureUtils
-open FunIdentifier
 module T = Types
 module V = Values
 module E = Expressions
@@ -44,7 +43,7 @@ type ast_formatter = {
   adt_field_to_string :
     TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
   adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
-  fun_decl_id_to_string : FunDeclId.id -> string;
+  fun_decl_id_to_string : A.FunDeclId.id -> string;
 }
 
 let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -86,7 +85,7 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
    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)
-    (fun_decls : A.fun_decl FunDeclId.Map.t) (type_params : type_var list) :
+    (fun_decls : A.fun_decl A.FunDeclId.Map.t) (type_params : type_var list) :
     ast_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
@@ -110,7 +109,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls
   in
   let fun_decl_id_to_string def_id =
-    let def = FunDeclId.Map.find def_id fun_decls in
+    let def = A.FunDeclId.Map.find def_id fun_decls in
     fun_name_to_string def.name
   in
   {
diff --git a/src/Pure.ml b/src/Pure.ml
index 256a872a..42f56fed 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -1,6 +1,5 @@
 open Identifiers
 open Names
-open FunIdentifier
 module T = Types
 module V = Values
 module E = Expressions
@@ -567,7 +566,7 @@ type fun_body = {
 }
 
 type fun_decl = {
-  def_id : FunDeclId.id;
+  def_id : A.FunDeclId.id;
   back_id : T.RegionGroupId.id option;
   basename : fun_name;
       (** The "base" name of the function.
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 55a8853a..195eb879 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -6,7 +6,6 @@
 
 open Pure
 open TranslateCore
-open FunIdentifier
 module C = Contexts
 module RegionVarId = T.RegionVarId
 module F = Format
@@ -93,7 +92,7 @@ type formatter = {
             (`None` if forward function)
           TODO: use the fun id for the assumed functions.
        *)
-  decreases_clause_name : FunDeclId.id -> fun_name -> string;
+  decreases_clause_name : A.FunDeclId.id -> fun_name -> string;
       (** Generates the name of the definition used to prove/reason about
           termination. The generated code uses this clause where needed,
           but its body must be defined by the user.
@@ -357,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let fun_name =
         match fid with
         | A.Regular fid ->
-            Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
+            Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
         | A.Assumed aid -> A.show_assumed_fun_id aid
       in
       let fun_kind =
@@ -370,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let fun_name =
         match fid with
         | A.Regular fid ->
-            Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
+            Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
         | A.Assumed aid -> A.show_assumed_fun_id aid
       in
       "decreases clause for function: " ^ fun_name
@@ -445,7 +444,7 @@ let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get (FunId (id, rg)) ctx
 
-let ctx_get_local_function (id : FunDeclId.id) (rg : RegionGroupId.id option)
+let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get_function (A.Regular id) rg ctx
 
@@ -476,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
     (ctx : extraction_ctx) : string =
   ctx_get (VariantId (def_id, variant_id)) ctx
 
-let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) :
+let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (ctx : extraction_ctx) :
     string =
   ctx_get (DecreasesClauseId (A.Regular def_id)) ctx
 
@@ -574,7 +573,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   (* Lookup the LLBC def to compute the region group information *)
   let def_id = def.def_id in
   let llbc_def =
-    FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
+    A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
   in
   let sg = llbc_def.signature in
   let num_rgs = List.length sg.regions_hierarchy in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 711e438b..4b0a04ca 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -210,12 +210,6 @@ let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place
   (* There is nothing to do *)
   p
 
-(** Apply a type substitution to an operand constant value *)
-let operand_constant_value_substitute (_tsubst : T.TypeVarId.id -> T.ety)
-    (op : E.operand_constant_value) : E.operand_constant_value =
-  (* There is nothing to do *)
-  op
-
 (** Apply a type substitution to an operand *)
 let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
     E.operand =
@@ -225,9 +219,7 @@ let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
   | E.Move p -> E.Move (p_subst p)
   | E.Constant (ety, cv) ->
       let rsubst x = x in
-      E.Constant
-        ( ty_substitute rsubst tsubst ety,
-          operand_constant_value_substitute tsubst cv )
+      E.Constant ( ty_substitute rsubst tsubst ety, cv )
 
 (** Apply a type substitution to an rvalue *)
 let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
@@ -289,6 +281,7 @@ let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
       let p = place_substitute tsubst p in
       let rvalue = rvalue_substitute tsubst rvalue in
       A.Assign (p, rvalue)
+  | A.AssignGlobal g -> A.AssignGlobal g
   | A.FakeRead p ->
       let p = place_substitute tsubst p in
       A.FakeRead p
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 2b416cc1..927684bc 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -2,7 +2,6 @@ open Errors
 open LlbcAstUtils
 open Pure
 open PureUtils
-open FunIdentifier
 module Id = Identifiers
 module M = Modules
 module S = SymbolicAst
@@ -68,9 +67,10 @@ type fun_sig_named_outputs = {
 }
 
 type fun_context = {
-  llbc_fun_decls : A.fun_decl FunDeclId.Map.t;
+  llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdMap.t;  (** *)
-  fun_infos : FA.fun_info FunDeclId.Map.t;
+  fun_infos : FA.fun_info A.FunDeclId.Map.t;
+  gid_conv : A.global_id_converter;
 }
 
 type call_info = {
@@ -134,8 +134,11 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
 
 (* TODO: move *)
 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 ctx.fun_decl
+  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.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
@@ -196,12 +199,12 @@ let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
   TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
 
-let bs_ctx_lookup_llbc_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
+let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
     =
-  FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
+  A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
 
 (* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id)
+let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
     (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
   let id = (A.Regular def_id, back_id) in
   (RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg
@@ -472,11 +475,11 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
   List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
 
 (** Small utility. *)
-let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t)
+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 = FunDeclId.Map.find fid fun_infos in
+      let info = A.FunDeclId.Map.find fid fun_infos in
       let input_state = info.stateful in
       let output_state = input_state && gid = None in
       { can_fail = true; input_state; output_state }
@@ -494,7 +497,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t)
     name (outputs for backward functions come from borrows in the inputs
     of the forward function).
  *)
-let translate_fun_sig (fun_infos : FA.fun_info FunDeclId.Map.t)
+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 =
@@ -1744,7 +1747,7 @@ 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 (fun_infos : FA.fun_info FunDeclId.Map.t)
+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 =
diff --git a/src/Translate.ml b/src/Translate.ml
index 1577753c..d4d79355 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,6 +1,5 @@
 open InterpreterStatements
 open Interpreter
-open FunIdentifier
 module L = Logging
 module T = Types
 module A = LlbcAst
@@ -65,7 +64,10 @@ let translate_function_to_symbolics (config : C.partial_config)
       ^ Print.fun_name_to_string fdef.A.name));
 
   let { type_context; fun_context } = trans_ctx in
-  let fun_context = { C.fun_decls = fun_context.fun_decls } in
+  let fun_context = {
+    C.fun_decls = fun_context.fun_decls;
+    C.gid_conv = fun_context.gid_conv;
+  } in
 
   match fdef.body with
   | None -> None
@@ -100,7 +102,8 @@ let translate_function_to_symbolics (config : C.partial_config)
 let translate_function_to_pure (config : C.partial_config)
     (mp_config : Micro.config) (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_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+    (fdef : A.fun_decl)
     : pure_fun_translation =
   (* Debug *)
   log#ldebug
@@ -139,6 +142,7 @@ 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 ctx =
@@ -291,7 +295,11 @@ let translate_module_to_pure (config : C.partial_config)
   (* Compute the type and function contexts *)
   let type_context, fun_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 } 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
 
   (* Translate all the type definitions *)
@@ -352,8 +360,8 @@ type gen_ctx = {
   m : M.llbc_module;
   extract_ctx : PureToExtract.extraction_ctx;
   trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
-  trans_funs : (bool * pure_fun_translation) FunDeclId.Map.t;
-  functions_with_decreases_clause : FunDeclId.Set.t;
+  trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
+  functions_with_decreases_clause : A.FunDeclId.Set.t;
 }
 (** Extraction context *)
 
@@ -389,7 +397,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
       ctx.trans_types
   in
   let has_opaque_funs =
-    FunDeclId.Map.exists
+    A.FunDeclId.Map.exists
       (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
         Option.is_none t_fwd.body)
       ctx.trans_funs
@@ -428,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
 
   (* Utility to check a function has a decrease clause *)
   let has_decreases_clause (def : Pure.fun_decl) : bool =
-    FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
+    A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
   in
 
   (* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -524,14 +532,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
             ids
     | Fun (NonRec id) ->
         (* Lookup *)
-        let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+        let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
         (* Translate *)
         export_functions false [ pure_fun ]
     | Fun (Rec ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+          List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids
         in
         (* Translate *)
         export_functions true pure_funs
@@ -623,7 +631,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
-    FunDeclId.Set.of_list
+    A.FunDeclId.Set.of_list
       (List.concat
          (List.map
             (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
@@ -645,7 +653,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       (fun ctx (keep_fwd, def) ->
         (* Note that we generate a decrease clause for all the recursive functions *)
         let gen_decr_clause =
-          FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
+          A.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
         in
         ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
           gen_decr_clause def)
@@ -675,7 +683,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
   in
   let trans_funs =
-    FunDeclId.Map.of_list
+    A.FunDeclId.Map.of_list
       (List.map
          (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
            (fd.def_id, (keep_fwd, (fd, bdl))))
@@ -762,7 +770,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     (* Extract the template clauses *)
     let needs_clauses_module =
       config.extract_decreases_clauses
-      && not (FunDeclId.Set.is_empty rec_functions)
+      && not (A.FunDeclId.Set.is_empty rec_functions)
     in
     (if needs_clauses_module && config.extract_template_decreases_clauses then
      let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 3d3887ce..ccaa9e22 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -1,7 +1,6 @@
 (** Some utilities for the translation *)
 
 open InterpreterStatements
-open FunIdentifier
 module L = Logging
 module T = Types
 module A = LlbcAst
@@ -15,8 +14,9 @@ let log = L.translate_log
 type type_context = C.type_context [@@deriving show]
 
 type fun_context = {
-  fun_decls : A.fun_decl FunDeclId.Map.t;
-  fun_infos : FA.fun_info FunDeclId.Map.t;
+  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]
 
@@ -50,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
   PrintPure.fun_decl_to_string fmt def
 
-let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string =
+let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =
   Print.fun_name_to_string
-    (FunDeclId.Map.find id ctx.fun_context.fun_decls).name
+    (A.FunDeclId.Map.find id ctx.fun_context.fun_decls).name
diff --git a/src/main.ml b/src/main.ml
index 6b1083f5..93b094fd 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -124,21 +124,21 @@ let () =
    * command-line arguments *)
   (* By setting a level for the main_logger_handler, we filter everything *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  main_log#set_level EL.Info;
-  llbc_of_json_logger#set_level EL.Info;
-  pre_passes_log#set_level EL.Info;
-  interpreter_log#set_level EL.Info;
-  statements_log#set_level EL.Info;
-  paths_log#set_level EL.Info;
-  expressions_log#set_level EL.Info;
-  expansion_log#set_level EL.Info;
-  borrows_log#set_level EL.Info;
-  invariants_log#set_level EL.Info;
-  pure_utils_log#set_level EL.Info;
-  symbolic_to_pure_log#set_level EL.Info;
-  pure_micro_passes_log#set_level EL.Info;
-  pure_to_extract_log#set_level EL.Info;
-  translate_log#set_level EL.Info;
+  main_log#set_level EL.Debug;
+  llbc_of_json_logger#set_level EL.Debug;
+  pre_passes_log#set_level EL.Debug;
+  interpreter_log#set_level EL.Debug;
+  statements_log#set_level EL.Debug;
+  paths_log#set_level EL.Debug;
+  expressions_log#set_level EL.Debug;
+  expansion_log#set_level EL.Debug;
+  borrows_log#set_level EL.Debug;
+  invariants_log#set_level EL.Debug;
+  pure_utils_log#set_level EL.Debug;
+  symbolic_to_pure_log#set_level EL.Debug;
+  pure_micro_passes_log#set_level EL.Debug;
+  pure_to_extract_log#set_level EL.Debug;
+  translate_log#set_level EL.Debug;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match llbc_module_of_json json with
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
new file mode 100644
index 00000000..9611c778
--- /dev/null
+++ b/tests/misc/Constants.fst
@@ -0,0 +1,119 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [constants] *)
+module Constants
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [constants::X0] *)
+let x0_fwd : result u32 = Return 0
+
+(** [core::num::u32::{8}::MAX] *)
+assume val core_num_u32_max_fwd : result u32
+
+(** [constants::X1] *)
+let x1_fwd : result u32 = Return 4294967295
+
+(** [constants::X2] *)
+let x2_fwd : result u32 = Return 3
+
+(** [constants::incr] *)
+let incr_fwd (n : u32) : result u32 =
+  begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::X3] *)
+let x3_fwd : result u32 =
+  begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::mk_pair0] *)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
+
+(** [constants::Pair] *)
+type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
+
+(** [constants::mk_pair1] *)
+let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
+  Return (Mkpair_t x y)
+
+(** [constants::P0] *)
+let p0_fwd : result (u32 & u32) =
+  begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::P1] *)
+let p1_fwd : result (pair_t u32 u32) =
+  begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::P2] *)
+let p2_fwd : result (u32 & u32) = Return (0, 1)
+
+(** [constants::P3] *)
+let p3_fwd : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+
+(** [constants::Wrap] *)
+type wrap_t (t : Type0) = { wrap_val : t; }
+
+(** [constants::Wrap::{0}::new] *)
+let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
+  Return (Mkwrap_t val0)
+
+(** [constants::Y] *)
+let y_fwd : result (wrap_t i32) =
+  begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+
+(** [constants::unwrap_y] *)
+let unwrap_y_fwd : result i32 =
+  begin match y_fwd with | Fail -> Fail | Return w -> Return w.wrap_val end
+
+(** [constants::YVAL] *)
+let yval_fwd : result i32 =
+  begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::get_z1::Z1] *)
+let get_z1_z1_fwd : result i32 = Return 3
+
+(** [constants::get_z1] *)
+let get_z1_fwd : result i32 =
+  begin match get_z1_z1_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::add] *)
+let add_fwd (a : i32) (b : i32) : result i32 =
+  begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q1] *)
+let q1_fwd : result i32 = Return 5
+
+(** [constants::Q2] *)
+let q2_fwd : result i32 =
+  begin match q1_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q3] *)
+let q3_fwd : result i32 =
+  begin match q2_fwd with
+  | Fail -> Fail
+  | Return i ->
+    begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end
+  end
+
+(** [constants::get_z2] *)
+let get_z2_fwd : result i32 =
+  begin match get_z1_fwd with
+  | Fail -> Fail
+  | Return i ->
+    begin match q3_fwd with
+    | Fail -> Fail
+    | Return i0 ->
+      begin match add_fwd i i0 with
+      | Fail -> Fail
+      | Return i1 ->
+        begin match q1_fwd with
+        | Fail -> Fail
+        | Return i2 ->
+          begin match add_fwd i2 i1 with
+          | Fail -> Fail
+          | Return i3 -> Return i3
+          end
+        end
+      end
+    end
+  end
+