diff --git a/CoqOfRust/M.v b/CoqOfRust/M.v
index 9d784a149..fa95687dd 100644
--- a/CoqOfRust/M.v
+++ b/CoqOfRust/M.v
@@ -6,10 +6,14 @@ Require Export Coq.ZArith.ZArith.
 Require Export Lia.
 From Hammer Require Export Tactics.
 
-Import List.ListNotations.
+Export List.ListNotations.
 
-Local Open Scope list.
-Local Open Scope string.
+Global Open Scope char_scope.
+Global Open Scope string_scope.
+Global Open Scope list_scope.
+Global Open Scope type_scope.
+Global Open Scope Z_scope.
+Global Open Scope bool_scope.
 
 (** Activate the handling of modulo in `lia`. *)
 Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
@@ -62,6 +66,17 @@ Module List.
       | S index => x :: replace_at l index update
       end
     end.
+
+  Fixpoint replace_at_error {A : Set} (l : list A) (index : nat) (update : A) :
+      option (list A) :=
+    match l with
+    | [] => None
+    | x :: l =>
+      match index with
+      | O => Some (update :: l)
+      | S index => option_map (cons x) (replace_at_error l index update)
+      end
+    end.
 End List.
 
 Module IntegerKind.
@@ -120,44 +135,11 @@ Module Pointer.
     Definition t : Set := list Index.t.
   End Path.
 
-  Module Mutable.
-    Inductive t (Value A : Set) : Set :=
-    | Make {Address Big_A : Set}
-      (address : Address)
-      (path : Path.t)
-      (big_to_value : Big_A -> Value)
-      (projection : Big_A -> option A)
-      (injection : Big_A -> A -> option Big_A).
-    Arguments Make {_ _ _ _}.
-  End Mutable.
-
-  Module Core.
-    Inductive t (Value A : Set) : Set :=
-    | Immediate (value : Value)
-    | Mutable (mutable : Mutable.t Value A).
-    Arguments Immediate {_ _}.
-    Arguments Mutable {_ _}.
-  End Core.
-
-  Module Kind.
-    Inductive t : Set :=
-    | Ref
-    | MutRef
-    | ConstPointer
-    | MutPointer.
-
-    Definition to_ty_path (kind : t) : string :=
-      match kind with
-      | Ref => "&"
-      | MutRef => "&mut"
-      | ConstPointer => "*const"
-      | MutPointer => "*mut"
-      end.
-  End Kind.
-
   Inductive t (Value : Set) : Set :=
-  | Make {A : Set} (kind : Kind.t) (ty : Ty.t) (to_value : A -> Value) (core : Core.t Value A).
-  Arguments Make {_ _}.
+  | Immediate (value : Value)
+  | Mutable (address : nat) (path : Path.t).
+  Arguments Immediate {_}.
+  Arguments Mutable {_}.
 End Pointer.
 
 Module Value.
@@ -222,6 +204,16 @@ Module Value.
       end
     end.
 
+  Fixpoint read_path (value : Value.t) (path : Pointer.Path.t) : option Value.t :=
+    match path with
+    | [] => Some value
+    | index :: path =>
+      match read_index value index with
+      | Some value => read_path value path
+      | None => None
+      end
+    end.
+
   (** Update the part of a value at a certain [index], and return [None] if the index is of invalid
       shape. *)
   Definition write_index
@@ -257,6 +249,22 @@ Module Value.
       | _ => None
       end
     end.
+
+  Fixpoint write_path
+      (value : Value.t) (path : Pointer.Path.t) (update : Value.t) :
+      option Value.t :=
+    match path with
+    | [] => Some update
+    | index :: path =>
+      match read_index value index with
+      | Some sub_value =>
+        match write_path sub_value path update with
+        | Some sub_value => write_index value index sub_value
+        | None => None
+        end
+      | None => None
+      end
+    end.
 End Value.
 
 Module Primitive.
@@ -264,7 +272,6 @@ Module Primitive.
   | StateAlloc (value : Value.t)
   | StateRead (pointer : Pointer.t Value.t)
   | StateWrite (pointer : Pointer.t Value.t) (value : Value.t)
-  | GetSubPointer (pointer : Pointer.t Value.t) (index : Pointer.Index.t)
   | AreEqual (value1 value2 : Value.t)
   | GetFunction (path : string) (generic_tys : list Ty.t)
   | GetAssociatedFunction (ty : Ty.t) (name : string) (generic_tys : list Ty.t)
@@ -280,12 +287,17 @@ Module LowM.
   Inductive t (A : Set) : Set :=
   | Pure (value : A)
   | CallPrimitive (primitive : Primitive.t) (k : Value.t -> t A)
+  | CallGetSubPointer
+    (pointer : Pointer.t Value.t)
+    (index : Pointer.Index.t)
+    (k : option (Pointer.t Value.t) -> t A)
   | CallClosure (closure : Value.t) (args : list Value.t) (k : A -> t A)
   | Let (e : t A) (k : A -> t A)
   | Loop (body : t A) (k : A -> t A)
   | Impossible (message : string).
   Arguments Pure {_}.
   Arguments CallPrimitive {_}.
+  Arguments CallGetSubPointer {_}.
   Arguments CallClosure {_}.
   Arguments Let {_}.
   Arguments Loop {_}.
@@ -296,6 +308,8 @@ Module LowM.
     | Pure v => e2 v
     | CallPrimitive primitive k =>
       CallPrimitive primitive (fun v => let_ (k v) e2)
+    | CallGetSubPointer pointer index k =>
+      CallGetSubPointer pointer index (fun v => let_ (k v) e2)
     | CallClosure f args k =>
       CallClosure f args (fun v => let_ (k v) e2)
     | Let e k =>
@@ -595,7 +609,11 @@ Arguments copy /.
 Definition get_sub_pointer (r : Value.t) (index : Pointer.Index.t) : M :=
   match r with
   | Value.Pointer pointer =>
-    call_primitive (Primitive.GetSubPointer pointer index)
+    LowM.CallGetSubPointer pointer index (fun result =>
+    match result with
+    | Some sub_pointer => pure (Value.Pointer sub_pointer)
+    | None => break_match
+    end)
   | _ => impossible "cannot get sub-pointer"
   end.
 
diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt
index 30158991d..e9bf48e63 100644
--- a/CoqOfRust/blacklist.txt
+++ b/CoqOfRust/blacklist.txt
@@ -18,4 +18,5 @@ core/iter/adapters/flatten.v
 token-2022
 # Links that are not working yet
 core/links/cmp.v
-move_sui/links/
\ No newline at end of file
+move_sui/links/
+links/
diff --git a/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
index 01465d6af..50ff9bbb1 100644
--- a/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
@@ -1,6 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.simulations.M.
-Require Import CoqOfRust.lib.lib.
 
 Import simulations.M.Notations.
 
diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
index 8b7ff8a43..e06a345a8 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -604,7 +604,7 @@ Definition lens_state_store_loc_state (v : Value.t)
   |}.
 
 (* NOTE: State designed for `execute_instruction` *)
-Definition State := (Z * Locals.t * Interpreter.t).
+Definition State : Set := Z * Locals.t * Interpreter.t.
 
 (* NOTE: This function is for debugging purpose *)
 Definition debug_execute_instruction (pc : Z) 
diff --git a/CoqOfRust/stack/M.v b/CoqOfRust/stack/M.v
new file mode 100644
index 000000000..699be5666
--- /dev/null
+++ b/CoqOfRust/stack/M.v
@@ -0,0 +1,172 @@
+Require Import CoqOfRust.M.
+
+Module Stack.
+  Definition t : Set :=
+    list Value.t.
+
+  Module HasAllocWith.
+    Inductive t (stack_in : Stack.t) (value : Value.t) : Pointer.t Value.t -> Stack.t -> Prop :=
+    | Immediate : t stack_in value (Pointer.Immediate value) stack_in
+    | Mutable :
+      let address := List.length stack_in in
+      let pointer : Pointer.t Value.t := Pointer.Mutable address [] in
+      let stack_out := stack_in ++ [value] in
+      t stack_in value pointer stack_out.
+  End HasAllocWith.
+
+  Module HasReadWith.
+    Inductive t (stack_in : Stack.t) (value : Value.t) : Pointer.t Value.t -> Set :=
+    | Immediate : t stack_in value (Pointer.Immediate value)
+    | Mutable (address : nat) (path : Pointer.Path.t) (big_value : Value.t) :
+      let pointer := Pointer.Mutable address path in
+      List.nth_error stack_in address = Some big_value ->
+      Value.read_path big_value path = Some value ->
+      t stack_in value pointer.
+  End HasReadWith.
+
+  Module HasWriteWith.
+    Inductive t (stack_in : Stack.t) (value : Value.t) : Pointer.t Value.t -> Stack.t -> Prop :=
+    | Mutable (address : nat) (path : Pointer.Path.t) :
+      let pointer : Pointer.t Value.t := Pointer.Mutable address path in
+      let stack_out := stack_in ++ [value] in
+      t stack_in value pointer stack_out.
+  End HasWriteWith.
+
+  Definition get_sub_pointer
+      (stack_in : Stack.t)
+      (pointer : Pointer.t Value.t)
+      (index : Pointer.Index.t)
+      (value : Value.t)
+      (H_read : HasReadWith.t stack_in value pointer) :
+      option (Pointer.t Value.t) :=
+    match Value.read_index value index with
+    | Some sub_value =>
+      Some match pointer with
+      | Pointer.Immediate _ => Pointer.Immediate sub_value
+      | Pointer.Mutable address path =>
+        Pointer.Mutable address (path ++ [index])
+      end
+    | None => None
+    end.
+
+  (* Module HasSubPointerWith.
+    Inductive t (index : Pointer.Index.t) :
+        Pointer.t Value.t -> option (Pointer.t Value.t) -> Prop :=
+    | Immediate (value sub_value : Value.t) :
+      Value.read_index value index = Some sub_value ->
+      t index (Pointer.Immediate value) (Pointer.Immediate sub_value)
+    | Mutable (address : nat) (path : Pointer.Path.t) :
+      t index (Pointer.Mutable address path) (Pointer.Mutable address (path ++ [index])).
+  End HasSubPointerWith. *)
+End Stack.
+
+Module Run.
+  Reserved Notation "{{ stack_in | e ⇓ output | stack_out }}".
+
+  Inductive t (output : Value.t + Exception.t) (stack_out : Stack.t) : Stack.t -> M -> Prop :=
+  | Pure :
+    (* This should be the only case where the input and output stacks are the same. *)
+    {{ stack_out | LowM.Pure output ⇓ output | stack_out }}
+  | CallPrimitiveStateAlloc
+      (value : Value.t)
+      (pointer : Pointer.t Value.t)
+      (stack_in stack_in' : Stack.t)
+      (k : Value.t -> M) :
+    Stack.HasAllocWith.t stack_in value pointer stack_in' ->
+    {{ stack_in' | k (Value.Pointer pointer) ⇓ output | stack_out }} ->
+    {{ stack_in | LowM.CallPrimitive (Primitive.StateAlloc value) k ⇓ output | stack_out }}
+  | CallPrimitiveStateRead
+      (pointer : Pointer.t Value.t)
+      (value : Value.t)
+      (k : Value.t -> M)
+      (stack_in : Stack.t) :
+    Stack.HasReadWith.t stack_in value pointer ->
+    {{ stack_in | k value ⇓ output | stack_out }} ->
+    {{ stack_in | LowM.CallPrimitive (Primitive.StateRead pointer) k ⇓ output | stack_out }}
+  | CallPrimitiveStateWrite
+      (value : Value.t)
+      (pointer : Pointer.t Value.t)
+      (stack_in stack_in' : Stack.t)
+      (k : Value.t -> M) :
+    Stack.HasWriteWith.t stack_in value pointer stack_in' ->
+    {{ stack_in' | k (Value.Tuple []) ⇓ output | stack_out }} ->
+    {{ stack_in | LowM.CallPrimitive (Primitive.StateWrite pointer value) k ⇓ output | stack_out }}
+  | CallPrimitiveGetFunction
+      (name : string) (generic_consts : list Value.t) (generic_tys : list Ty.t)
+      (function : PolymorphicFunction.t)
+      (k : Value.t -> M)
+      (stack_in : Stack.t) :
+    let closure := Value.Closure (existS (_, _) (function generic_consts generic_tys)) in
+    M.IsFunction name function ->
+    {{ stack_in | k closure ⇓ output | stack_out }} ->
+    {{ stack_in |
+      LowM.CallPrimitive (Primitive.GetFunction name generic_tys) k ⇓ output
+    | stack_out }}
+  | CallPrimitiveGetAssociatedFunction
+      (ty : Ty.t) (name : string) (generic_consts : list Value.t) (generic_tys : list Ty.t)
+      (associated_function : PolymorphicFunction.t)
+      (k : Value.t -> M)
+      (stack_in : Stack.t) :
+    let closure := Value.Closure (existS (_, _) (associated_function generic_consts generic_tys)) in
+    M.IsAssociatedFunction ty name associated_function ->
+    {{ stack_in | k closure ⇓ output | stack_out }} ->
+    {{ stack_in |
+      LowM.CallPrimitive
+        (Primitive.GetAssociatedFunction ty name generic_tys) k ⇓
+      output
+    | stack_out }}
+  | CallPrimitiveGetTraitMethod
+      (trait_name : string) (self_ty : Ty.t) (trait_tys : list Ty.t)
+      (method_name : string) (generic_consts : list Value.t) (generic_tys : list Ty.t)
+      (method : PolymorphicFunction.t)
+      (k : Value.t -> M)
+      (stack_in : Stack.t) :
+    let closure := Value.Closure (existS (_, _) (method generic_consts generic_tys)) in
+    IsTraitMethod.t trait_name self_ty trait_tys method_name method ->
+    {{ stack_in | k closure ⇓ output | stack_out }} ->
+    {{ stack_in |
+      LowM.CallPrimitive
+        (Primitive.GetTraitMethod
+          trait_name
+          self_ty
+          trait_tys
+          method_name
+          generic_tys)
+        k ⇓
+      output
+    | stack_out }}
+  | CallGetSubPointer
+      (index : Pointer.Index.t)
+      (pointer : Pointer.t Value.t)
+      (value : Value.t)
+      (k : option (Pointer.t Value.t) -> M)
+      (stack_in : Stack.t)
+      (H_read : Stack.HasReadWith.t stack_in value pointer) :
+    let result := Stack.get_sub_pointer stack_in pointer index value H_read in
+    {{ stack_in | k result ⇓ output | stack_out }} ->
+    {{ stack_in | LowM.CallGetSubPointer pointer index k ⇓ output | stack_out }}
+  | CallClosure
+      (output_inter : Value.t + Exception.t)
+      (f : list Value.t -> M) (args : list Value.t)
+      (k : Value.t + Exception.t -> M)
+      (stack_in stack_inter : Stack.t) :
+    let closure := Value.Closure (existS (_, _) f) in
+    {{ stack_in | f args ⇓ output_inter | stack_inter }} ->
+    (* We do not de-allocate what was already there on the stack. *)
+    (* IsWritePreserved.t stack stack' -> *)
+    {{ stack_inter | k output_inter ⇓ output | stack_out }} ->
+    {{ stack_in | LowM.CallClosure closure args k ⇓ output | stack_out }}
+  (* Might be useful to avoid having rewritings that block the evaluation. *)
+  | Rewrite (e e' : M) (stack_in : Stack.t) :
+    e = e' ->
+    {{ stack_in | e' ⇓ output | stack_out }} ->
+    {{ stack_in | e ⇓ output | stack_out }}
+
+  where "{{ stack_in | e ⇓ output | stack_out }}" :=
+    (t output stack_out stack_in e).
+
+  (* Notation "{{ '_' | e ⇓ output_to_value }}" :=
+    (forall (stack : Stack.t),
+      {{ stack | e ⇓ output_to_value }}
+    ). *)
+End Run.
diff --git a/CoqOfRust/stack/core/option.v b/CoqOfRust/stack/core/option.v
new file mode 100644
index 000000000..94bb34ee9
--- /dev/null
+++ b/CoqOfRust/stack/core/option.v
@@ -0,0 +1,207 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.stack.M.
+Require Import CoqOfRust.core.option.
+
+Import Run.
+
+Definition t (A : Set) : Set :=
+  option A.
+
+Definition to_value {A : Set} (A_to_value : A -> Value.t) (x : t A) : Value.t :=
+  match x with
+  | Some x => Value.StructTuple "core::option::Option::Some" [A_to_value x]
+  | None => Value.StructTuple "core::option::Option::None" []
+  end.
+
+Module Impl_core_option_Option_T.
+  Definition Self (A : Set) : Set :=
+    t A.
+
+  Definition is_some {A : Set} (self : Self A) : bool :=
+    match self with
+    | Some _ => true
+    | None => false
+    end.
+
+  Lemma run_is_some {A : Set} (A_ty : Ty.t) (A_to_value : A -> Value.t)
+      (self_pointer : Pointer.t Value.t) (self : Self A)
+      (stack : Stack.t) :
+    let self_value : Value.t := to_value A_to_value self in
+    Stack.HasReadWith.t stack self_value self_pointer ->
+    {{ stack |
+      CoqOfRust.core.option.option.Impl_core_option_Option_T.is_some
+        A_ty [] [] [Value.Pointer self_pointer] ⇓
+      inl (Value.Bool (is_some self))
+    | stack }}.
+  Proof.
+    intros * H_self_pointer.
+    unfold option.option.Impl_core_option_Option_T.is_some.
+    eapply Run.CallPrimitiveStateAlloc. {
+      apply Stack.HasAllocWith.Immediate.
+    }
+    eapply Run.CallPrimitiveStateRead. {
+      apply Stack.HasReadWith.Immediate.
+    }
+    fold @LowM.let_.
+    cbn.
+    apply Run.CallGetSubPointer with (H_read := H_self_pointer).
+    destruct self as [self|]; cbn.
+    { eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      apply Run.Pure.
+    }
+    { eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      apply Run.Pure.
+    }
+  Qed.
+
+  Definition is_none {A : Set} (self : Self A) : bool :=
+    negb (is_some self).
+
+  Lemma run_is_none {A : Set} (A_ty : Ty.t) (A_to_value : A -> Value.t)
+      (self_pointer : Pointer.t Value.t) (self : Self A)
+      (stack : Stack.t) :
+    let self_value : Value.t := to_value A_to_value self in
+    Stack.HasReadWith.t stack self_value self_pointer ->
+    {{ stack |
+      CoqOfRust.core.option.option.Impl_core_option_Option_T.is_none
+        A_ty [] [] [Value.Pointer self_pointer] ⇓
+      inl (Value.Bool (is_none self))
+    | stack }}.
+  Proof.
+    intros * H_self_pointer.
+    unfold option.option.Impl_core_option_Option_T.is_none.
+    eapply Run.CallPrimitiveStateAlloc. {
+      apply Stack.HasAllocWith.Immediate.
+    }
+    eapply Run.CallPrimitiveGetAssociatedFunction. {
+      apply option.option.Impl_core_option_Option_T.AssociatedFunction_is_some.
+    }
+    fold @LowM.let_.
+    eapply Run.CallPrimitiveStateRead. {
+      apply Stack.HasReadWith.Immediate.
+    }
+    fold @LowM.let_.
+    eapply Run.CallClosure. {
+      apply run_is_some with (A_to_value := A_to_value).
+      apply H_self_pointer.
+    }
+    apply Run.Pure.
+  Qed.
+
+  Definition as_ref {A : Set} (self : Self A) : Self A :=
+    self.
+
+  Lemma run_as_ref {A : Set} (A_ty : Ty.t) (A_to_value : A -> Value.t)
+      (self_pointer : Pointer.t Value.t) (self : Self A)
+      (stack : Stack.t) :
+    let self_value : Value.t := to_value A_to_value self in
+    Stack.HasReadWith.t stack self_value self_pointer ->
+    {{ stack |
+      CoqOfRust.core.option.option.Impl_core_option_Option_T.as_ref
+        A_ty [] [] [Value.Pointer self_pointer] ⇓
+      inl self_value
+    | stack }}.
+  Proof.
+    intros * H_self_pointer.
+    unfold option.option.Impl_core_option_Option_T.as_ref.
+    eapply Run.CallPrimitiveStateAlloc. {
+      apply Stack.HasAllocWith.Immediate.
+    }
+    eapply Run.CallPrimitiveStateRead. {
+      apply Stack.HasReadWith.Immediate.
+    }
+    fold @LowM.let_.
+    apply Run.CallGetSubPointer with (H_read := H_self_pointer).
+    fold @LowM.let_.
+    destruct self as [self|]; cbn.
+    { eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      admit.
+    }
+    { eapply Run.CallPrimitiveStateRead. {
+        apply H_self_pointer.
+      }
+      cbn.
+      eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      apply Run.Pure.
+    }
+  Admitted.
+
+  Axiom expect_failed : forall {A : Set}, string -> A.
+
+  (*
+      pub const fn expect(self, msg: &str) -> T {
+          match self {
+              Some(val) => val,
+              None => expect_failed(msg),
+          }
+      }
+  *)
+  Definition expect {A : Set} (self : Self A) (msg : string) : A :=
+    match self with
+    | Some val => val
+    | None => expect_failed msg
+    end.
+
+  Lemma run_expect {A : Set} (A_ty : Ty.t) (A_to_value : A -> Value.t)
+      (self : Self A) (msg : string)
+      (stack : Stack.t) :
+    let self_value : Value.t := to_value A_to_value self in
+    {{ stack |
+      CoqOfRust.core.option.option.Impl_core_option_Option_T.expect
+        A_ty [] [] [self_value; Value.String msg] ⇓
+      inl (A_to_value (expect self msg))
+    | stack }}.
+  Proof.
+    intros.
+    unfold option.option.Impl_core_option_Option_T.expect.
+    eapply Run.CallPrimitiveStateAlloc. {
+      apply Stack.HasAllocWith.Immediate.
+    }
+    eapply Run.CallPrimitiveStateAlloc. {
+      apply Stack.HasAllocWith.Immediate.
+    }
+    destruct self as [self|]; cbn.
+    { eapply Run.CallGetSubPointer.
+      cbn.
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      apply Run.Pure.
+    }
+    { eapply Run.CallPrimitiveStateAlloc. {
+        apply Stack.HasAllocWith.Immediate.
+      }
+      eapply Run.CallPrimitiveStateRead. {
+        apply Stack.HasReadWith.Immediate.
+      }
+      apply Run.Pure.
+    }
+End Impl_core_option_Option_T.
diff --git a/third-party/move-sui b/third-party/move-sui
index 82e94dfbe..c18d595ff 160000
--- a/third-party/move-sui
+++ b/third-party/move-sui
@@ -1 +1 @@
-Subproject commit 82e94dfbe71d78f2e74463654a52d1041d738b28
+Subproject commit c18d595ff8a195cc56826bb1bf49ec9b0b9483e7
diff --git a/third-party/rust b/third-party/rust
index c6db1ca3c..fb4aebddd 160000
--- a/third-party/rust
+++ b/third-party/rust
@@ -1 +1 @@
-Subproject commit c6db1ca3c93ad69692a4c4b5542f26fda4bf3aec
+Subproject commit fb4aebddd18d258046ddb51fd41589295259a0fa