More progress on the proofs and build instructions

CoqOfPython/CoqOfPython.v

@@ -32,9 +32,32 @@ Module Dict.
   Definition t (Value : Set) : Set :=
     list (string * Value).
 
-  Parameter read : forall {Value : Set}, t Value -> string -> option Value.
+  Fixpoint read {Value : Set} (dict : t Value) (key : string) : option Value :=
+    match dict with
+    | [] => None
+    | (current_key, value) :: dict =>
+      if String.eqb current_key key then
+        Some value
+      else
+        read dict key
+    end.
+
+  Fixpoint update {Value : Set} (dict : t Value) (key : string) (value : Value) : t Value :=
+    match dict with
+    | [] => []
+    | (current_key, current_value) :: dict =>
+      if String.eqb current_key key then
+        (current_key, value) :: dict
+      else
+        (current_key, current_value) :: update dict key value
+    end.
 
-  Parameter write : forall {Value : Set}, t Value -> string -> Value -> t Value.
+  (** Starting from Python 3.7 the ordering in `dict` is guaranted to follow the insersion order. *)
+  Definition write {Value : Set} (dict : t Value) (key : string) (value : Value) : t Value :=
+    match read dict key with
+    | Some _ => update dict key value
+    | None => dict ++ [(key, value)]
+    end.
 End Dict.
 
 Module Globals.
@@ -211,9 +234,12 @@ End Exception.
 Definition M : Set :=
   LowM.t (Value.t + Exception.t).
 
-Parameter IsInGlobals : string -> Value.t -> string -> Prop.
+Parameter IsInGlobals : Globals.t -> string -> Value.t -> Prop.
 
-Parameter IsImported : string -> string -> string -> Prop.
+Definition IsImported (globals : Globals.t) (import : Globals.t) (name : string) : Prop :=
+  forall (value : Value.t),
+    IsInGlobals import name value ->
+    IsInGlobals globals name value.
 
 Module M.
   Definition pure (v : Value.t) : M :=
@@ -494,15 +520,18 @@ Module builtins.
 
   Definition type : Value.t :=
     make_klass [] [] [].
-  Axiom type_in_globals : IsInGlobals "builtins" type "type".
+  Axiom type_in_globals : IsInGlobals "builtins" "type" type.
 
   Definition int : Value.t :=
     make_klass [] [] [].
-  Axiom int_in_globals : IsInGlobals "builtins" int "int".
+  Axiom int_in_globals : IsInGlobals "builtins" "int" int.
 
   Definition str : Value.t :=
     make_klass [] [] [].
-  Axiom str_in_globals : IsInGlobals "builtins" str "str".
+  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))).

CoqOfPython/ethereum/arrow_glacier/bloom.v

@@ -140,6 +140,9 @@ Definition add_to_bloom : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom add_to_bloom_in_globals :
+  IsInGlobals globals "add_to_bloom" (make_function add_to_bloom).
+
 Definition logs_bloom : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "logs" ] in
@@ -209,3 +212,6 @@ Definition logs_bloom : Value.t -> Value.t -> M :=
       |)
     |) in
     M.pure Constant.None_)).
+
+Axiom logs_bloom_in_globals :
+  IsInGlobals globals "logs_bloom" (make_function logs_bloom).

CoqOfPython/ethereum/arrow_glacier/fork.v

@@ -253,6 +253,9 @@ Definition apply_fork : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom apply_fork_in_globals :
+  IsInGlobals globals "apply_fork" (make_function apply_fork).
+
 Definition get_last_256_block_hashes : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "chain" ] in
@@ -365,6 +368,9 @@ Definition get_last_256_block_hashes : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom get_last_256_block_hashes_in_globals :
+  IsInGlobals globals "get_last_256_block_hashes" (make_function get_last_256_block_hashes).
+
 Definition state_transition : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "chain"; "block" ] in
@@ -533,6 +539,9 @@ Definition state_transition : Value.t -> Value.t -> M :=
       )) |) in
     M.pure Constant.None_)).
 
+Axiom state_transition_in_globals :
+  IsInGlobals globals "state_transition" (make_function state_transition).
+
 Definition calculate_base_fee_per_gas : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "block_gas_limit"; "parent_gas_limit"; "parent_gas_used"; "parent_base_fee_per_gas" ] in
@@ -698,6 +707,9 @@ Definition calculate_base_fee_per_gas : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom calculate_base_fee_per_gas_in_globals :
+  IsInGlobals globals "calculate_base_fee_per_gas" (make_function calculate_base_fee_per_gas).
+
 Definition validate_header : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "header"; "parent_header" ] in
@@ -864,6 +876,9 @@ Definition validate_header : Value.t -> Value.t -> M :=
   |) in
     M.pure Constant.None_)).
 
+Axiom validate_header_in_globals :
+  IsInGlobals globals "validate_header" (make_function validate_header).
+
 Definition generate_header_hash_for_pow : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "header" ] in
@@ -920,6 +935,9 @@ Definition generate_header_hash_for_pow : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom generate_header_hash_for_pow_in_globals :
+  IsInGlobals globals "generate_header_hash_for_pow" (make_function generate_header_hash_for_pow).
+
 Definition validate_proof_of_work : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "header" ] in
@@ -1010,6 +1028,9 @@ Definition validate_proof_of_work : Value.t -> Value.t -> M :=
   |) in
     M.pure Constant.None_)).
 
+Axiom validate_proof_of_work_in_globals :
+  IsInGlobals globals "validate_proof_of_work" (make_function validate_proof_of_work).
+
 Definition check_transaction : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx"; "base_fee_per_gas"; "gas_available"; "chain_id" ] in
@@ -1143,6 +1164,9 @@ Definition check_transaction : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom check_transaction_in_globals :
+  IsInGlobals globals "check_transaction" (make_function check_transaction).
+
 Definition make_receipt : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx"; "error"; "cumulative_gas_used"; "logs" ] in
@@ -1240,6 +1264,9 @@ Definition make_receipt : Value.t -> Value.t -> M :=
       )) |) in
     M.pure Constant.None_)).
 
+Axiom make_receipt_in_globals :
+  IsInGlobals globals "make_receipt" (make_function make_receipt).
+
 Definition ApplyBodyOutput : Value.t :=
   builtins.make_klass
     []
@@ -1493,6 +1520,9 @@ Definition apply_body : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom apply_body_in_globals :
+  IsInGlobals globals "apply_body" (make_function apply_body).
+
 Definition validate_ommers : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "ommers"; "block_header"; "chain" ] in
@@ -1814,6 +1844,9 @@ Definition validate_ommers : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom validate_ommers_in_globals :
+  IsInGlobals globals "validate_ommers" (make_function validate_ommers).
+
 Definition pay_rewards : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "state"; "block_number"; "coinbase"; "ommers" ] in
@@ -1919,6 +1952,9 @@ Definition pay_rewards : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom pay_rewards_in_globals :
+  IsInGlobals globals "pay_rewards" (make_function pay_rewards).
+
 Definition process_transaction : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "env"; "tx" ] in
@@ -2395,6 +2431,9 @@ Definition process_transaction : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom process_transaction_in_globals :
+  IsInGlobals globals "process_transaction" (make_function process_transaction).
+
 Definition validate_transaction : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx" ] in
@@ -2451,6 +2490,9 @@ Definition validate_transaction : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom validate_transaction_in_globals :
+  IsInGlobals globals "validate_transaction" (make_function validate_transaction).
+
 Definition calculate_intrinsic_cost : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx" ] in
@@ -2616,6 +2658,9 @@ Definition calculate_intrinsic_cost : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom calculate_intrinsic_cost_in_globals :
+  IsInGlobals globals "calculate_intrinsic_cost" (make_function calculate_intrinsic_cost).
+
 Definition recover_sender : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "chain_id"; "tx" ] in
@@ -2908,6 +2953,9 @@ Definition recover_sender : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom recover_sender_in_globals :
+  IsInGlobals globals "recover_sender" (make_function recover_sender).
+
 Definition signing_hash_pre155 : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx" ] in
@@ -2942,6 +2990,9 @@ Definition signing_hash_pre155 : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom signing_hash_pre155_in_globals :
+  IsInGlobals globals "signing_hash_pre155" (make_function signing_hash_pre155).
+
 Definition signing_hash_155 : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx"; "chain_id" ] in
@@ -2990,6 +3041,9 @@ Definition signing_hash_155 : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom signing_hash_155_in_globals :
+  IsInGlobals globals "signing_hash_155" (make_function signing_hash_155).
+
 Definition signing_hash_2930 : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx" ] in
@@ -3027,6 +3081,9 @@ Definition signing_hash_2930 : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom signing_hash_2930_in_globals :
+  IsInGlobals globals "signing_hash_2930" (make_function signing_hash_2930).
+
 Definition signing_hash_1559 : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "tx" ] in
@@ -3064,6 +3121,9 @@ Definition signing_hash_1559 : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom signing_hash_1559_in_globals :
+  IsInGlobals globals "signing_hash_1559" (make_function signing_hash_1559).
+
 Definition compute_header_hash : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "header" ] in
@@ -3116,6 +3176,9 @@ Definition compute_header_hash : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom compute_header_hash_in_globals :
+  IsInGlobals globals "compute_header_hash" (make_function compute_header_hash).
+
 Definition check_gas_limit : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "gas_limit"; "parent_gas_limit" ] in
@@ -3216,6 +3279,9 @@ Definition check_gas_limit : Value.t -> Value.t -> M :=
     |) in
     M.pure Constant.None_)).
 
+Axiom check_gas_limit_in_globals :
+  IsInGlobals globals "check_gas_limit" (make_function check_gas_limit).
+
 Definition calculate_block_difficulty : Value.t -> Value.t -> M :=
   fun (args kwargs : Value.t) =>
     let- locals_stack := M.create_locals locals_stack args kwargs [ "block_number"; "block_timestamp"; "parent_timestamp"; "parent_difficulty"; "parent_has_ommers" ] in
@@ -3376,3 +3442,6 @@ Constant.int 1
       |)
     |) in
     M.pure Constant.None_)).
+
+Axiom calculate_block_difficulty_in_globals :
+  IsInGlobals globals "calculate_block_difficulty" (make_function calculate_block_difficulty).

CoqOfPython/ethereum/arrow_glacier/fork_types.v

@@ -99,3 +99,6 @@ Definition encode_account : Value.t -> Value.t -> M :=
       |)
     |) in
     M.pure Constant.None_)).
+
+Axiom encode_account_in_globals :
+  IsInGlobals globals "encode_account" (make_function encode_account).