Draft: experiments around stack semantics

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,14 +249,29 @@ 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.
   Inductive t : Set :=
   | 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.
 

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/
+move_sui/links/
+links/

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.
 

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) 

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.