Draft: more work on the simulations for the gas file

CoqOfRust/M.v

@@ -131,7 +131,9 @@ Module Pointer.
 
   Module Core.
     Inductive t (Value : Set) : Set :=
-    | Immediate (value : Value)
+    (** The immediate value is optional in case with have a sub-pointer of an immediate pointer for
+        an enum case that is not the current one. *)
+    | Immediate (value : option Value)
     | Mutable {Address : Set} (address : Address) (path : Path.t).
     Arguments Immediate {_}.
     Arguments Mutable {_ _}.
@@ -296,18 +298,36 @@ Module Primitive.
     (generic_tys : list Ty.t).
 End Primitive.
 
+Module Panic.
+  Inductive t : Set :=
+  | Make (message : string).
+End Panic.
+
+Module Exception.
+  Inductive t : Set :=
+  (** exceptions for Rust's `return` *)
+  | Return (value : Value.t) : t
+  (** exceptions for Rust's `continue` *)
+  | Continue : t
+  (** exceptions for Rust's `break` *)
+  | Break : t
+  (** escape from a match branch once we know that it is not valid *)
+  | BreakMatch : t
+  | Panic (panic : Panic.t) : t.
+End Exception.
+
 Module LowM.
   Inductive t (A : Set) : Set :=
   | Pure (value : A)
   | CallPrimitive (primitive : Primitive.t) (k : Value.t -> t A)
   | CallClosure (ty : Ty.t) (closure : Value.t) (args : list Value.t) (k : A -> t A)
-  | Let (ty : Ty.t) (e : t A) (k : A -> t A)
+  | LetAlloc (ty : Ty.t) (e : t (Value.t + Exception.t)) (k : Value.t + Exception.t -> t A)
   | Loop (ty : Ty.t) (body : t A) (k : A -> t A)
   | Impossible (message : string).
   Arguments Pure {_}.
   Arguments CallPrimitive {_}.
   Arguments CallClosure {_}.
-  Arguments Let {_}.
+  Arguments LetAlloc {_}.
   Arguments Loop {_}.
   Arguments Impossible {_}.
 
@@ -318,32 +338,14 @@ Module LowM.
       CallPrimitive primitive (fun v => let_ (k v) e2)
     | CallClosure ty f args k =>
       CallClosure ty f args (fun v => let_ (k v) e2)
-    | Let ty e k =>
-      Let ty e (fun v => let_ (k v) e2)
+    | LetAlloc ty e k =>
+      LetAlloc ty e (fun v => let_ (k v) e2)
     | Loop ty body k =>
       Loop ty body (fun v => let_ (k v) e2)
     | Impossible message => Impossible message
     end.
 End LowM.
 
-Module Panic.
-  Inductive t : Set :=
-  | Make (message : string).
-End Panic.
-
-Module Exception.
-  Inductive t : Set :=
-  (** exceptions for Rust's `return` *)
-  | Return (value : Value.t) : t
-  (** exceptions for Rust's `continue` *)
-  | Continue : t
-  (** exceptions for Rust's `break` *)
-  | Break : t
-  (** escape from a match branch once we know that it is not valid *)
-  | BreakMatch : t
-  | Panic (panic : Panic.t) : t.
-End Exception.
-
 Definition M : Set :=
   LowM.t (Value.t + Exception.t).
 
@@ -362,7 +364,7 @@ Definition let_user (ty : Ty.t) (e1 : Value.t) (e2 : Value.t -> Value.t) : Value
   e2 e1.
 
 Definition let_user_monadic (ty : Ty.t) (e1 : M) (e2 : Value.t -> M) : M :=
-  LowM.Let ty e1 (fun v1 =>
+  LowM.LetAlloc ty e1 (fun v1 =>
   match v1 with
   | inl v1 => e2 v1
   | inr error => LowM.Pure (inr error)
@@ -693,9 +695,14 @@ Definition get_trait_method
 
 Definition catch (ty : option Ty.t) (body : M) (handler : Exception.t -> M) : M :=
   (match ty with
-  | Some ty => LowM.Let ty
+  | Some ty => LowM.LetAlloc ty
   | None => LowM.let_
-  end) body (fun result =>
+  end)
+  (match ty with
+  | Some _ => let* body := body in M.read body
+  | None => body
+  end)
+  (fun result =>
   match result with
   | inl v => LowM.Pure (inl v)
   | inr exception => handler exception
@@ -910,13 +917,13 @@ Fixpoint run_constant (constant : M) : Value.t :=
       | Primitive.StateAlloc value =>
         Value.Pointer {|
           Pointer.kind := Pointer.Kind.Raw;
-          Pointer.core := Pointer.Core.Immediate value;
+          Pointer.core := Pointer.Core.Immediate (Some value);
         |}
       | Primitive.StateRead pointer =>
         match pointer with
         | Value.Pointer {|
             Pointer.kind := Pointer.Kind.Raw;
-            Pointer.core := Pointer.Core.Immediate value;
+            Pointer.core := Pointer.Core.Immediate (Some value);
           |} =>
           value
         | _ => Value.Error "expected an immediate raw pointer"
@@ -925,7 +932,7 @@ Fixpoint run_constant (constant : M) : Value.t :=
       end in
     run_constant (k value)
   | LowM.CallClosure _ _ _ _ => Value.Error "unexpected closure call"
-  | LowM.Let _ _ _ => Value.Error "unexpected let"
+  | LowM.LetAlloc _ _ _ => Value.Error "unexpected let-alloc"
   | LowM.Loop _ _ _ => Value.Error "unexpected loop"
   | LowM.Impossible _ => Value.Error "impossible"
   end.