Group the stack and heap kinds of pointers

CoqOfPython/CoqOfPython.v

@@ -64,6 +64,15 @@ Module Globals.
   Definition t : Set := string.
 End Globals.
 
+Module Klass.
+  Record t {Value M : Set} : Set := {
+    bases : list (Globals.t * string);
+    class_methods : list (string * (Value -> Value -> M));
+    methods : list (string * (Value -> Value -> M));
+  }.
+  Arguments t : clear implicits.
+End Klass.
+
 Module Data.
   (** This type is not accessible directly in Python, as only object are. We use this type
       internally to represent integers, closures, ... that can be made accessible in a special
@@ -81,10 +90,7 @@ Module Data.
   | Set_ (items : list Value)
   | Dict (dict : Dict.t Value)
   | Closure {Value M : Set} (f : Value -> Value -> M)
-  | Klass {Value M : Set}
-    (bases : list (Globals.t * string))
-    (class_methods : list (string * (Value -> Value -> M)))
-    (methods : list (string * (Value -> Value -> M))).
+  | Klass {Value M : Set} (klass : Klass.t Value M).
   Arguments Ellipsis {_}.
   Arguments Bool {_}.
   Arguments Integer {_}.
@@ -106,19 +112,32 @@ Module Object.
   Arguments t : clear implicits.
   Arguments Build_t {_}.
 
-  Fixpoint fields_of_optional_dict {Value : Set} (optional_dict : list (string * option Value)) :
+  Fixpoint fields_of_dict_option {Value : Set} (optional_dict : list (string * option Value)) :
       Dict.t Value :=
     match optional_dict with
     | [] => []
     | (name, Some value) :: optional_dict =>
-      Dict.write (fields_of_optional_dict optional_dict) name value
-    | (_, None) :: optional_dict => fields_of_optional_dict optional_dict
+      Dict.write (fields_of_dict_option optional_dict) name value
+    | (_, None) :: optional_dict => fields_of_dict_option optional_dict
     end.
 
-  Definition make {Value : Set} (optional_dict : list (string * option Value)) : t Value :=
+  Definition make_option {Value : Set} (optional_dict : list (string * option Value)) : t Value :=
     {|
       internal := None;
-      fields := fields_of_optional_dict optional_dict;
+      fields := fields_of_dict_option optional_dict;
+    |}.
+
+  Fixpoint fields_of_dict {Value : Set} (dict : list (string * Value)) : Dict.t Value :=
+    match dict with
+    | [] => []
+    | (name, value) :: dict =>
+      Dict.write (fields_of_dict dict) name value
+    end.
+
+  Definition make {Value : Set} (dict : list (string * Value)) : t Value :=
+    {|
+      internal := None;
+      fields := fields_of_dict dict;
     |}.
 
   (** When an object is just a wrapper around the [Data.t] type. *)
@@ -131,18 +150,29 @@ End Object.
 
 Module Pointer.
   Module Mutable.
+    Module Kind.
+      Inductive t : Set :=
+      | Stack (index : nat)
+      | Heap {Address : Set} (address : Address).
+    End Kind.
+
     Inductive t (Value : Set) : Set :=
-    | Stack {A : Set} (index : nat) (to_object : A -> Object.t Value)
-    | Heap {Address A : Set} (address : Address) (to_object : A -> Object.t Value).
-    Arguments Stack {_ _}.
-    Arguments Heap {_ _ _}.
+    | Make {A : Set} (kind : Kind.t) (to_object : A -> Object.t Value).
+    Arguments Make {_ _}.
   End Mutable.
 
   Inductive t (Value : Set) : Set :=
   | Imm (data : Object.t Value)
   | Mutable (mutable : Mutable.t Value).
   Arguments Imm {_}.
   Arguments Mutable {_}.
+
+  Definition stack {Value A : Set} (index : nat) (to_object : A -> Object.t Value) : t Value :=
+    Mutable (Mutable.Make (Mutable.Kind.Stack index) to_object).
+
+  Definition heap {Value A Address : Set} (address : Address) (to_object : A -> Object.t Value) :
+      t Value :=
+    Mutable (Mutable.Make (Mutable.Kind.Heap address) to_object).
 End Pointer.
 
 Module Value.
@@ -241,6 +271,11 @@ Definition IsImported (globals : Globals.t) (import : Globals.t) (name : string)
     IsInGlobals import name value ->
     IsInGlobals globals name value.
 
+(** The `builtins` module is accessible from anywhere. *)
+Axiom builtins_is_imported :
+  forall (globals : Globals.t) (name : string),
+  IsImported globals "builtins" name.
+
 Module M.
   Definition pure (v : Value.t) : M :=
     LowM.Pure (inl v).
@@ -507,31 +542,10 @@ Module Compare.
   Parameter not_in : Value.t -> Value.t -> M.
 End Compare.
 
-(** ** Builtins *)
-Module builtins.
-  Definition make_klass
-    (bases : list (string * string))
-    (class_methods : list (string * (Value.t -> Value.t -> M)))
-    (methods : list (string * (Value.t -> Value.t -> M))) :
-    Value.t :=
-  Value.Make "builtins" "type" (Pointer.Imm (Object.wrapper (
-    Data.Klass bases class_methods methods
-  ))).
-
-  Definition type : Value.t :=
-    make_klass [] [] [].
-  Axiom type_in_globals : IsInGlobals "builtins" "type" type.
-
-  Definition int : Value.t :=
-    make_klass [] [] [].
-  Axiom int_in_globals : IsInGlobals "builtins" "int" int.
-
-  Definition str : Value.t :=
-    make_klass [] [] [].
-  Axiom str_in_globals : IsInGlobals "builtins" "str" str.
-End builtins.
-
 Parameter make_list_concat : list Value.t -> M.
 
 Definition make_function (f : Value.t -> Value.t -> M) : Value.t :=
   Value.Make "builtins" "function" (Pointer.Imm (Object.wrapper (Data.Closure f))).
+
+Definition make_klass (klass : Klass.t Value.t M) : Value.t :=
+  Value.Make "builtins" "type" (Pointer.Imm (Object.wrapper (Data.Klass klass))).

CoqOfPython/builtins.v

@@ -0,0 +1,30 @@
+Require Import CoqOfPython.CoqOfPython.
+
+Definition globals : Globals.t := "builtins".
+
+Definition type : Value.t :=
+  make_klass {|
+    Klass.bases := [];
+    Klass.class_methods := [];
+    Klass.methods := [];
+  |}.
+Axiom type_in_globals : IsInGlobals "builtins" "type" type.
+
+Definition int : Value.t :=
+  make_klass {|
+    Klass.bases := [];
+    Klass.class_methods := [];
+    Klass.methods := [];
+  |}.
+Axiom int_in_globals : IsInGlobals "builtins" "int" int.
+
+Definition str : Value.t :=
+  make_klass {|
+    Klass.bases := [];
+    Klass.class_methods := [];
+    Klass.methods := [];
+  |}.
+Axiom str_in_globals : IsInGlobals "builtins" "str" str.
+
+Parameter len : Value.t -> Value.t -> M.
+Axiom len_in_globals : IsInGlobals globals "len" (make_function len).

CoqOfPython/ethereum/arrow_glacier/blocks.v

@@ -50,42 +50,38 @@ Axiom ethereum_arrow_glacier_fork_types_imports_Root :
 Axiom ethereum_arrow_glacier_transactions_imports_LegacyTransaction :
   IsImported globals "ethereum.arrow_glacier.transactions" "LegacyTransaction".
 
-Definition Header : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
-
-Definition Block : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
-
-Definition Log : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
-
-Definition Receipt : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
+Definition Header : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
+
+Definition Block : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
+
+Definition Log : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
+
+Definition Receipt : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.

CoqOfPython/ethereum/arrow_glacier/fork.v

@@ -216,15 +216,14 @@ Definition EMPTY_OMMER_HASH : Value.t := M.run ltac:(M.monadic (
   |)
 )).
 
-Definition BlockChain : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
+Definition BlockChain : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
 
 Definition apply_fork : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
@@ -1267,15 +1266,14 @@ Definition make_receipt : Value.t -> Value.t -> M :=
 Axiom make_receipt_in_globals :
   IsInGlobals globals "make_receipt" (make_function make_receipt).
 
-Definition ApplyBodyOutput : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
+Definition ApplyBodyOutput : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
 
 Definition apply_body : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>

CoqOfPython/ethereum/arrow_glacier/fork_types.v

@@ -55,15 +55,14 @@ Definition Bloom : Value.t := M.run ltac:(M.monadic (
   M.get_name (| globals, locals_stack, "Bytes256" |)
 )).
 
-Definition Account : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
+Definition Account : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
 
 Definition EMPTY_ACCOUNT : Value.t := M.run ltac:(M.monadic (
   M.call (|

CoqOfPython/ethereum/arrow_glacier/state.v

@@ -76,15 +76,14 @@ Axiom ethereum_arrow_glacier_trie_imports_trie_get :
 Axiom ethereum_arrow_glacier_trie_imports_trie_set :
   IsImported globals "ethereum.arrow_glacier.trie" "trie_set".
 
-Definition State : Value.t :=
-  builtins.make_klass
-    []
-    [
-
-    ]
-    [
-
-    ].
+Definition State : Value.t := make_klass {|
+  Klass.bases := [
+  ];
+  Klass.class_methods := [
+  ];
+  Klass.methods := [
+  ];
+|}.
 
 Definition close_state : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>