14 files changed, 416 insertions, 116 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 9664fbc4..97cd2c78 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -33,51 +33,199 @@ module T = Types
 module A = CfimAst
 open TypesUtils
 
-(** `T -> Box<T>` *)
-let box_new_sig : A.fun_sig =
-  let tvar_id_0 = T.TypeVarId.of_int 0 in
-  let tvar_0 = T.TypeVar tvar_id_0 in
-  {
-    region_params = [];
-    num_early_bound_regions = 0;
-    regions_hierarchy = [];
-    type_params = [ { index = tvar_id_0; name = "T" } ];
-    inputs = [ tvar_0 (* T *) ];
-    output = mk_box_ty tvar_0 (* Box<T> *);
-  }
-
-(** Helper for `Box::deref_shared` and `Box::deref_mut`.
-    Returns:
-    `&'a (mut) Box<T> -> &'a (mut) T`
- *)
-let box_deref_sig (is_mut : bool) : A.fun_sig =
-  let rvar_id_0 = T.RegionVarId.of_int 0 in
-  let rvar_0 = T.Var rvar_id_0 in
-  let rg_id_0 = T.RegionGroupId.of_int 0 in
-  let tvar_id_0 = T.TypeVarId.of_int 0 in
-  let tvar_0 = T.TypeVar tvar_id_0 in
-  let ref_kind = if is_mut then T.Mut else T.Shared in
-  (* The signature fields *)
-  let region_params = [ { T.index = rvar_id_0; name = Some "'a" } ] in
-  let regions_hierarchy =
-    [ { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } ]
-    (* <'a> *)
-  in
-  {
-    region_params;
-    num_early_bound_regions = 0;
-    regions_hierarchy;
-    type_params = [ { index = tvar_id_0; name = "T" } ] (* <T> *);
-    inputs =
-      [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) ref_kind (* &'a (mut) Box<T> *) ];
-    output = mk_ref_ty rvar_0 tvar_0 ref_kind (* &'a (mut) T *);
-  }
-
-(** `&'a Box<T> -> &'a T` *)
-let box_deref_shared_sig = box_deref_sig false
-
-(** `&'a mut Box<T> -> &'a mut T` *)
-let box_deref_mut_sig = box_deref_sig true
+module Sig = struct
+  (** A few utilities *)
+
+  let rvar_id_0 = T.RegionVarId.of_int 0
+
+  let rvar_0 : T.RegionVarId.id T.region = T.Var rvar_id_0
+
+  let rg_id_0 = T.RegionGroupId.of_int 0
+
+  let tvar_id_0 = T.TypeVarId.of_int 0
+
+  let tvar_0 : T.sty = T.TypeVar tvar_id_0
+
+  (** Region 'a of id 0 *)
+  let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" }
+
+  (** Region group: { parent={}; regions:{'a of id 0} } *)
+  let region_group_0 : T.region_var_group =
+    { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }
+
+  (** Type parameter `T` of id 0 *)
+  let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" }
+
+  let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) :
+      T.sty =
+    let ref_kind = if is_mut then T.Mut else T.Shared in
+    mk_ref_ty r ty ref_kind
+
+  (** `fn<T>(&'a mut T, T) -> T` *)
+  let mem_replace_sig : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] (* <'a> *) in
+    let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ]
+    in
+    let output = tvar_0 (* T *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** `fn<T>(T) -> Box<T>` *)
+  let box_new_sig : A.fun_sig =
+    {
+      region_params = [];
+      num_early_bound_regions = 0;
+      regions_hierarchy = [];
+      type_params = [ type_param_0 ] (* <T> *);
+      inputs = [ tvar_0 (* T *) ];
+      output = mk_box_ty tvar_0 (* Box<T> *);
+    }
+
+  (** Helper for `Box::deref_shared` and `Box::deref_mut`.
+      Returns:
+      `fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T`
+  *)
+  let box_deref_gen_sig (is_mut : bool) : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params = [ type_param_0 ] (* <T> *);
+      inputs =
+        [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ];
+      output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *);
+    }
+
+  (** `fn<'a, T>(&'a Box<T>) -> &'a T` *)
+  let box_deref_shared_sig = box_deref_gen_sig false
+
+  (** `fn<'a, T>(&'a mut Box<T>) -> &'a mut T` *)
+  let box_deref_mut_sig = box_deref_gen_sig true
+
+  (** `fn<T>() -> Vec<T>` *)
+  let vec_new_sig : A.fun_sig =
+    let region_params = [] in
+    let regions_hierarchy = [] in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs = [] in
+    let output = mk_vec_ty tvar_0 (* Vec<T> *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** `fn<T>(&'a mut Vec<T>, T)` *)
+  let vec_push_sig : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [
+        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
+        tvar_0 (* T *);
+      ]
+    in
+    let output = mk_unit_ty (* () *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** `fn<T>(&'a mut Vec<T>, usize, T)` *)
+  let vec_insert_sig : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [
+        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
+        mk_usize_ty (* usize *);
+        tvar_0 (* T *);
+      ]
+    in
+    let output = mk_unit_ty (* () *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** `fn<T>(&'a Vec<T>) -> usize` *)
+  let vec_len_sig : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ]
+    in
+    let output = mk_usize_ty (* usize *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** Helper:
+      `fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T`
+   *)
+  let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
+    (* The signature fields *)
+    let region_params = [ region_param_0 ] in
+    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
+    let type_params = [ type_param_0 ] (* <T> *) in
+    let inputs =
+      [
+        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
+        mk_usize_ty;
+        (* usize *)
+      ]
+    in
+    let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
+    {
+      region_params;
+      num_early_bound_regions = 0;
+      regions_hierarchy;
+      type_params;
+      inputs;
+      output;
+    }
+
+  (** `fn<T>(&'a Vec<T>, usize) -> &'a T` *)
+  let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false
+
+  (** `fn<T>(&'a mut Vec<T>, usize) -> &'a mut T` *)
+  let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
+end
 
 (** The list of assumed functions, and their signatures.
 
@@ -85,14 +233,28 @@ let box_deref_mut_sig = box_deref_sig true
  *)
 let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
   [
-    (BoxNew, box_new_sig);
-    (BoxDeref, box_deref_shared_sig);
-    (BoxDerefMut, box_deref_mut_sig);
+    (Replace, Sig.mem_replace_sig);
+    (BoxNew, Sig.box_new_sig);
+    (BoxDeref, Sig.box_deref_shared_sig);
+    (BoxDerefMut, Sig.box_deref_mut_sig);
+    (VecNew, Sig.vec_new_sig);
+    (VecPush, Sig.vec_push_sig);
+    (VecInsert, Sig.vec_insert_sig);
+    (VecLen, Sig.vec_len_sig);
+    (VecIndex, Sig.vec_index_shared_sig);
+    (VecIndexMut, Sig.vec_index_mut_sig);
   ]
 
 let assumed_names : (A.assumed_fun_id * Identifiers.name) list =
   [
+    (Replace, [ "core"; "mem"; "replace" ]);
     (BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]);
     (BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]);
     (BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]);
+    (VecNew, [ "alloc"; "vec"; "Vec"; "new" ]);
+    (VecPush, [ "alloc"; "vec"; "Vec"; "push" ]);
+    (VecInsert, [ "alloc"; "vec"; "Vec"; "insert" ]);
+    (VecLen, [ "alloc"; "vec"; "Vec"; "len" ]);
+    (VecIndex, [ "core"; "ops"; "index"; "Index"; "index" ]);
+    (VecIndexMut, [ "core"; "ops"; "index"; "IndexMut"; "index_mut" ]);
   ]
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 57122a51..2f8d3e69 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -16,7 +16,20 @@ type var = {
 [@@deriving show]
 (** A variable, as used in a function definition *)
 
-type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
+type assumed_fun_id =
+  | Replace  (** `core::mem::replace` *)
+  | BoxNew
+  | BoxDeref  (** `core::ops::deref::Deref::<alloc::boxed::Box::>::deref` *)
+  | BoxDerefMut
+      (** `core::ops::deref::DerefMut::<alloc::boxed::Box::>::deref_mut` *)
+  | BoxFree
+  | VecNew
+  | VecPush
+  | VecInsert
+  | VecLen
+  | VecIndex  (** `core::ops::index::Index::index<alloc::vec::Vec<T>, usize>` *)
+  | VecIndexMut
+      (** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *)
 [@@deriving show, ord]
 
 type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 3378f548..a1d5faaa 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -362,17 +362,19 @@ let binop_of_json (js : json) : (E.binop, string) result =
   | `String "Shr" -> Ok E.Shr
   | _ -> Error ("binop_of_json failed on:" ^ show js)
 
-let operand_constant_value_of_json (js : json) :
+let rec operand_constant_value_of_json (js : json) :
     (E.operand_constant_value, string) result =
   combine_error_msgs js "operand_constant_value_of_json"
     (match js with
     | `Assoc [ ("ConstantValue", cv) ] ->
         let* cv = constant_value_of_json cv in
         Ok (E.ConstantValue cv)
-    | `Assoc [ ("ConstantAdt", id) ] ->
-        let* id = T.TypeDefId.id_of_json id in
-        Ok (E.ConstantAdt id)
-    | `String "Unit" -> Ok E.Unit
+    | `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 operand_constant_value_of_json field_values
+        in
+        Ok (E.ConstantAdt (variant_id, field_values))
     | _ -> Error "")
 
 let operand_of_json (js : json) : (E.operand, string) result =
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 816870cd..9c6b8490 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -3,6 +3,8 @@ open Values
 
 type field_proj_kind =
   | ProjAdt of TypeDefId.id * VariantId.id option
+  | ProjOption of VariantId.id
+      (** Option is an assumed type, coming from the standard library *)
   | ProjTuple of int
 [@@deriving show]
 (* arity of the tuple *)
@@ -73,6 +75,8 @@ let all_binops =
     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
@@ -81,8 +85,7 @@ let all_binops =
  *)
 type operand_constant_value =
   | ConstantValue of constant_value
-  | ConstantAdt of TypeDefId.id
-  | Unit
+  | ConstantAdt of VariantId.id option * operand_constant_value list
 [@@deriving show]
 
 type operand =
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5d772c04..636c68d3 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -94,16 +94,35 @@ let fstar_keywords =
   in
   List.concat [ named_unops; named_binops; misc ]
 
-let fstar_assumed_adts : (assumed_ty * string) list = [ (Result, "result") ]
+let fstar_assumed_adts : (assumed_ty * string) list =
+  [ (Result, "result"); (Option, "option") ]
 
 let fstar_assumed_structs : (assumed_ty * string) list = []
 
 let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
-  [ (Result, result_return_id, "Return"); (Result, result_fail_id, "Fail") ]
+  [
+    (Result, result_return_id, "Return");
+    (Result, result_fail_id, "Fail");
+    (Option, option_some_id, "Some");
+    (Option, option_none_id, "None");
+  ]
 
 let fstar_assumed_functions :
     (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
-  []
+  let rg0 = Some T.RegionGroupId.zero in
+  [
+    (Replace, None, "mem_replace_fwd");
+    (Replace, rg0, "mem_replace_back");
+    (VecNew, None, "vec_new");
+    (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
+    (VecPush, rg0, "vec_push_back");
+    (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
+    (VecInsert, rg0, "vec_insert_back");
+    (VecLen, None, "vec_len");
+    (VecIndex, rg0, "vec_index");
+    (VecIndexMut, None, "vec_index_mut_fwd");
+    (VecIndexMut, rg0, "vec_index_mut_back");
+  ]
 
 let fstar_names_map_init =
   {
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index ce9489a9..17e74ad3 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -70,34 +70,30 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool)
   in
   comp cc read_place cf ctx
 
-(** Convert a constant operand value to a typed value *)
-let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
+(** Convert an operand constant operand value to a typed value *)
+let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     (cv : E.operand_constant_value) : V.typed_value =
-  (* Check the type while converting *)
+  (* Check the type while converting - we actually need some information
+   * contained in the type *)
   match (ty, cv) with
-  (* Unit *)
-  | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value
-  (* Adt with one variant and no fields *)
-  | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' ->
-      assert (def_id = def_id');
-      (* Check that the adt definition only has one variant with no fields,
-         compute the variant id at the same time. *)
+  (* Adt *)
+  | ( T.Adt (T.AdtId def_id, region_params, type_params),
+      ConstantAdt (variant_id, field_values) ) ->
+      assert (region_params = []);
+      (* Compute the types of the fields *)
       let def = C.ctx_lookup_type_def ctx def_id in
-      assert (List.length def.region_params = 0);
-      assert (List.length def.type_params = 0);
-      let variant_id =
-        match def.kind with
-        | Struct fields ->
-            assert (List.length fields = 0);
-            None
-        | Enum variants ->
-            assert (List.length variants = 1);
-            let variant_id = T.VariantId.zero in
-            let variant = T.VariantId.nth variants variant_id in
-            assert (List.length variant.fields = 0);
-            Some variant_id
+      assert (def.region_params = []);
+      let field_tys =
+        Subst.type_def_get_instantiated_field_etypes def variant_id type_params
       in
-      let value = V.Adt { variant_id; field_values = [] } in
+      (* Compute the field values *)
+      let field_values =
+        List.map
+          (fun (ty, v) -> operand_constant_value_to_typed_value ctx ty v)
+          (List.combine field_tys field_values)
+      in
+      (* Put together *)
+      let value = V.Adt { variant_id; field_values } in
       { value; ty }
   (* Scalar, boolean... *)
   | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
@@ -110,7 +106,7 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
       { 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) *)
-  | _, Unit | _, ConstantAdt _ | _, ConstantValue _ ->
+  | _, ConstantAdt _ | _, ConstantValue _ ->
       failwith "Improperly typed constant value"
 
 (** Prepare the evaluation of an operand.
@@ -151,7 +147,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand)
    fun ctx ->
     match op with
     | Expressions.Constant (ty, cv) ->
-        let v = constant_value_to_typed_value ctx ty cv in
+        let v = operand_constant_value_to_typed_value ctx ty cv in
         cf v ctx
     | Expressions.Copy p ->
         (* Access the value *)
@@ -186,7 +182,7 @@ let eval_operand (config : C.config) (op : E.operand)
   (* Evaluate *)
   match op with
   | Expressions.Constant (ty, cv) ->
-      let v = constant_value_to_typed_value ctx ty cv in
+      let v = operand_constant_value_to_typed_value ctx ty cv in
       cf v ctx
   | Expressions.Copy p ->
       (* Access the value *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 09f13240..c926c63a 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -350,6 +350,11 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   comp cf_pop cf_assign
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
+let eval_replace_concrete (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
+ fun cf ctx -> raise Unimplemented
+
+(** Auxiliary function - see [eval_non_local_function_call] *)
 let eval_box_new_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
  fun cf ctx ->
@@ -486,6 +491,11 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       cc cf ctx
   | _ -> failwith "Inconsistent state"
 
+(** Auxiliary function - see [eval_non_local_function_call] *)
+let eval_vec_function_concrete (config : C.config) (fid : A.assumed_fun id)
+    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
+ fun cf ctx -> raise Unimplemented
+
 (** Evaluate a non-local function call in concrete mode *)
 let eval_non_local_function_call_concrete (config : C.config)
     (fid : A.assumed_fun_id) (region_params : T.erased_region list)
@@ -539,13 +549,15 @@ let eval_non_local_function_call_concrete (config : C.config)
          * access to a body. *)
         let cf_eval_body : cm_fun =
           match fid with
-          | A.BoxNew -> eval_box_new_concrete config region_params type_params
-          | A.BoxDeref ->
-              eval_box_deref_concrete config region_params type_params
-          | A.BoxDerefMut ->
+          | A.Replace -> eval_replace config region_params type_params
+          | BoxNew -> eval_box_new_concrete config region_params type_params
+          | BoxDeref -> eval_box_deref_concrete config region_params type_params
+          | BoxDerefMut ->
               eval_box_deref_mut_concrete config region_params type_params
-          | A.BoxFree ->
+          | BoxFree ->
               (* Should have been treated above *) failwith "Unreachable"
+          | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
+              eval_vec_function_concrete config fid region_params type_params
         in
 
         let cc = comp cc cf_eval_body in
diff --git a/src/Print.ml b/src/Print.ml
index 8124df52..b31be6ae 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -68,7 +68,11 @@ module Types = struct
     match id with
     | T.AdtId id -> fmt.type_def_id_to_string id
     | T.Tuple -> ""
-    | T.Assumed aty -> ( match aty with Box -> "std::boxed::Box")
+    | T.Assumed aty -> (
+        match aty with
+        | Box -> "alloc::boxed::Box"
+        | Vec -> "alloc::vec::Vec"
+        | Option -> "core::option::Option")
 
   let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r T.ty) : string =
     match ty with
@@ -726,6 +730,10 @@ module CfimAst = struct
         match pe with
         | E.Deref -> "*(" ^ s ^ ")"
         | E.DerefBox -> "deref_box(" ^ s ^ ")"
+        | E.Field (E.ProjOption variant_id, fid) ->
+            assert (variant_id == T.option_some_id);
+            assert (fid == T.FieldId.zero);
+            "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string fid
         | E.Field (E.ProjTuple _, fid) ->
             "(" ^ s ^ ")." ^ T.FieldId.to_string fid
         | E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
@@ -768,18 +776,38 @@ module CfimAst = struct
     | E.Shl -> "<<"
     | E.Shr -> ">>"
 
-  let operand_constant_value_to_string (fmt : ast_formatter)
+  let rec operand_constant_value_to_string (fmt : ast_formatter)
       (cv : E.operand_constant_value) : string =
     match cv with
     | E.ConstantValue cv -> PV.constant_value_to_string cv
-    | E.ConstantAdt def_id -> fmt.type_def_id_to_string def_id
-    | E.Unit -> "()"
+    | 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) -> operand_constant_value_to_string fmt cv
+    | 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
+        ^ " : "
+        ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
+        ^ ")"
 
   let rvalue_to_string (fmt : ast_formatter) (rv : E.rvalue) : string =
     match rv with
@@ -856,12 +884,23 @@ module CfimAst = struct
           | A.Local fid -> fmt.fun_def_id_to_string fid ^ params
           | A.Assumed fid -> (
               match fid with
+              | A.Replace -> "core::mem::replace" ^ params
               | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new"
               | A.BoxDeref ->
                   "core::ops::deref::Deref<Box" ^ params ^ ">::deref"
               | A.BoxDerefMut ->
                   "core::ops::deref::DerefMut" ^ params ^ "::deref_mut"
-              | A.BoxFree -> "alloc::alloc::box_free" ^ params)
+              | A.BoxFree -> "alloc::alloc::box_free" ^ params
+              | A.VecNew -> "alloc::vec::Vec" ^ params ^ "::new"
+              | A.VecPush -> "alloc::vec::Vec" ^ params ^ "::push"
+              | A.VecInsert -> "alloc::vec::Vec" ^ params ^ "::insert"
+              | A.VecLen -> "alloc::vec::Vec" ^ params ^ "::len"
+              | A.VecIndex ->
+                  "core::ops::index::Index<alloc::vec::Vec" ^ params
+                  ^ ">::index"
+              | A.VecIndexMut ->
+                  "core::ops::index::IndexMut<alloc::vec::Vec" ^ params
+                  ^ ">::index_mut")
         in
         let dest = place_to_string fmt call.A.dest in
         indent ^ dest ^ " := move " ^ name_params ^ args
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 81ebcc7e..5c25f2bd 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -201,6 +201,10 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
   | pe :: p' -> (
       let s = projection_to_string fmt inside p' in
       match pe.pkind with
+      | E.ProjOption variant_id ->
+          assert (variant_id == T.option_some_id);
+          assert (pe.field_id == T.FieldId.zero);
+          "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id
       | E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
       | E.ProjAdt (adt_id, opt_variant_id) -> (
           let field_name =
@@ -321,10 +325,18 @@ let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : A.fun_id) : string
   | A.Local fid -> fmt.fun_def_id_to_string fid
   | A.Assumed fid -> (
       match fid with
+      | A.Replace -> "core::mem::replace"
       | A.BoxNew -> "alloc::boxed::Box::new"
       | A.BoxDeref -> "core::ops::deref::Deref::deref"
       | A.BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut"
-      | A.BoxFree -> "alloc::alloc::box_free")
+      | A.BoxFree -> "alloc::alloc::box_free"
+      | A.VecNew -> "alloc::vec::Vec::new"
+      | A.VecPush -> "alloc::vec::Vec::push"
+      | A.VecInsert -> "alloc::vec::Vec::insert"
+      | A.VecLen -> "alloc::vec::Vec::len"
+      | A.VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
+      | A.VecIndexMut ->
+          "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut")
 
 let fun_suffix (rg_id : T.RegionGroupId.id option) : string =
   match rg_id with
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 01ce3a4e..62822785 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -168,10 +168,16 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
       type_params
   | T.Assumed aty -> (
       match aty with
-      | T.Box ->
+      | T.Box | T.Vec ->
           assert (List.length region_params = 0);
           assert (List.length type_params = 1);
-          type_params)
+          type_params
+      | T.Option ->
+          assert (List.length region_params = 0);
+          assert (List.length type_params = 1);
+          if adt.V.variant_id = Some T.option_some_id then type_params
+          else if adt.V.variant_id = Some T.option_none_id then []
+          else failwith "Unrechable")
 
 (** Instantiate the type variables in an ADT definition, and return the list
     of types of the fields for the chosen variant *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index a1208f92..46d2205c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -184,10 +184,14 @@ let rec translate_sty (ty : T.sty) : ty =
       match type_id with
       | T.AdtId adt_id -> Adt (AdtId adt_id, tys)
       | T.Tuple -> mk_simpl_tuple_ty tys
-      | T.Assumed T.Box -> (
-          match tys with
-          | [ ty ] -> ty
-          | _ -> failwith "Box type with incorrect number of arguments"))
+      | T.Assumed aty -> (
+          match aty with
+          | T.Box | T.Vec | T.Option -> (
+              match tys with
+              | [ ty ] -> ty
+              | _ ->
+                  failwith
+                    "Box/vec/option type with incorrect number of arguments")))
   | TypeVar vid -> TypeVar vid
   | Bool -> Bool
   | Char -> Char
@@ -257,13 +261,15 @@ let rec translate_fwd_ty (types_infos : TA.type_infos) (ty : 'r T.ty) : ty =
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_tys
-      | T.Assumed T.Box -> (
+      | T.Assumed (T.Box | T.Vec | T.Option) -> (
           (* No general parametricity for now *)
           assert (not (List.exists (TypesUtils.ty_has_borrows types_infos) tys));
           match t_tys with
           | [ bty ] -> bty
           | _ ->
-              failwith "Unreachable: boxes receive exactly one type parameter"))
+              failwith
+                "Unreachable: box/vec/option receives exactly one type \
+                 parameter"))
   | TypeVar vid -> TypeVar vid
   | Bool -> Bool
   | Char -> Char
@@ -303,13 +309,14 @@ let rec translate_back_ty (types_infos : TA.type_infos)
           let type_id =
             match type_id with
             | T.AdtId id -> AdtId id
-            | T.Tuple | T.Assumed T.Box -> failwith "Unreachable"
+            | T.Tuple | T.Assumed (T.Box | T.Vec | T.Option) ->
+                failwith "Unreachable"
           in
           if inside_mut then
             let tys_t = List.filter_map translate tys in
             Some (Adt (type_id, tys_t))
           else None
-      | Assumed T.Box -> (
+      | Assumed (T.Box | T.Vec | T.Option) -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows types_infos ty));
           (* Eliminate the box *)
@@ -608,7 +615,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
       (* For now, only tuples can contain borrows *)
       let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
       match adt_id with
-      | T.AdtId _ | T.Assumed T.Box ->
+      | T.AdtId _ | T.Assumed (T.Box | T.Vec | T.Option) ->
           assert (field_values = []);
           None
       | T.Tuple ->
@@ -738,10 +745,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
           ctx adt_v.field_values
       in
       let field_values = List.filter_map (fun x -> x) field_values in
-      (* For now, only tuples can contain borrows *)
+      (* For now, only tuples can contain borrows - note that if we gave
+       * something like a `&mut Vec` to a function, we give give back the
+       * vector value upon visiting the "abstraction borrow" node *)
       let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
       match adt_id with
-      | T.AdtId _ | T.Assumed T.Box ->
+      | T.AdtId _ | T.Assumed (T.Box | T.Vec | T.Option) ->
           assert (field_values = []);
           (ctx, None)
       | T.Tuple ->
@@ -851,7 +860,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
 let fun_is_monadic (fun_id : A.fun_id) : bool =
   match fun_id with
   | A.Local _ -> true
-  | A.Assumed (A.BoxNew | BoxDeref | BoxDerefMut | BoxFree) -> false
+  | A.Assumed
+      ( A.Replace | A.BoxNew | BoxDeref | BoxDerefMut | BoxFree | VecNew
+      | VecPush | VecLen ) ->
+      false
+  | A.Assumed (A.VecInsert | VecIndex | VecIndexMut) -> true
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
@@ -1198,6 +1211,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       match branches with
       | [] -> failwith "Unreachable"
       | [ (variant_id, svl, branch) ] -> (
+          (* There is exactly one branch: no branching *)
           let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
           let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
           let branch = translate_expression branch ctx in
@@ -1263,7 +1277,17 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
               mk_let monadic
                 (mk_typed_lvalue_from_var var None)
                 (mk_value_expression scrutinee scrutinee_mplace)
-                branch)
+                branch
+          | T.Assumed T.Vec ->
+              (* We can't expand vector values: we can access the fields only
+               * through the functions provided by the API (note that we don't
+               * know how to expand a vector, because it has a variable number
+               * of fields!) *)
+              failwith "Can't expand a vector value"
+          | T.Assumed T.Option ->
+              (* We shouldn't get there in the "one-branch" case: options have
+               * two variants *)
+              failwith "Unreachable")
       | branches ->
           let translate_branch (variant_id : T.VariantId.id option)
               (svl : V.symbolic_value list) (branch : S.expression) :
diff --git a/src/Types.ml b/src/Types.ml
index cab46859..d7b9ab1b 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -88,7 +88,13 @@ let all_int_types = List.append all_signed_int_types all_unsigned_int_types
 
 type ref_kind = Mut | Shared [@@deriving show, ord]
 
-type assumed_ty = Box [@@deriving show, ord]
+type assumed_ty = Box | Vec | Option [@@deriving show, ord]
+
+(** The variant id for `Option::Some` *)
+let option_some_id = VariantId.of_int 0
+
+(** The variant id for `Option::None` *)
+let option_none_id = VariantId.of_int 1
 
 (** Type identifier for ADTs.
 
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index 5fa8fc15..5429d709 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -172,7 +172,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         in
         (* Continue exploring *)
         analyze expl_info ty_info rty
-    | Adt ((Tuple | Assumed Box), _, tys) ->
+    | Adt ((Tuple | Assumed (Box | Vec | Option)), _, tys) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
           (fun ty_info ty -> analyze expl_info ty_info ty)
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index e6e59a51..db10ed47 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -43,7 +43,10 @@ let ty_as_custom_adt (ty : 'r ty) : TypeDefId.id * 'r list * 'r ty list =
   | _ -> failwith "Unreachable"
 
 (** The unit type *)
-let mk_unit_ty : ety = Adt (Tuple, [], [])
+let mk_unit_ty : 'r ty = Adt (Tuple, [], [])
+
+(** The usize type *)
+let mk_usize_ty : 'r ty = Integer Usize
 
 (** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *)
 let ty_get_box (box_ty : ety) : ety =
@@ -65,6 +68,9 @@ let mk_ref_ty (r : 'r) (ty : 'r ty) (ref_kind : ref_kind) : 'r ty =
 (** Make a box type *)
 let mk_box_ty (ty : 'r ty) : 'r ty = Adt (Assumed Box, [], [ ty ])
 
+(** Make a vec type *)
+let mk_vec_ty (ty : 'r ty) : 'r ty = Adt (Assumed Vec, [], [ ty ])
+
 (** Check if a region is in a set of regions *)
 let region_in_set (r : RegionId.id region) (rset : RegionId.Set.t) : bool =
   match r with Static -> false | Var id -> RegionId.Set.mem id rset