Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Beginning of semantics #5

Merged
merged 5 commits into from
May 13, 2024
Merged

Beginning of semantics #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
14790dd
wip
clarus May 11, 2024
d537d38
Add definitions to read in the locals
clarus May 12, 2024
71868b6
Definition of a simulation for the add function
clarus May 12, 2024
c6d3d85
Add a definition for a Run.t predicate
clarus May 12, 2024
6d0e196
Progress towards the verification of the add function
clarus May 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
340 changes: 261 additions & 79 deletions CoqOfPython/CoqOfPython.v
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 7 additions & 5 deletions CoqOfPython/ethereum/__init__.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
Require Import CoqOfPython.CoqOfPython.

Definition globals : string := "ethereum.__init__".
Definition globals : Globals.t := "ethereum.__init__".

Definition locals_stack : list Locals.t := [].

Definition expr_1 : Value.t :=
Constant.str "
Expand Down Expand Up @@ -37,14 +39,14 @@ Definition EVM_RECURSION_LIMIT : Value.t := M.run ltac:(M.monadic (

Definition expr_27 : Value.t :=
M.call (|
M.get_field (| M.get_name (| globals, "sys" |), "setrecursionlimit" |),
M.get_field (| M.get_name (| globals, locals_stack, "sys" |), "setrecursionlimit" |),
make_list [
M.call (|
M.get_name (| globals, "max" |),
M.get_name (| globals, locals_stack, "max" |),
make_list [
M.get_name (| globals, "EVM_RECURSION_LIMIT" |);
M.get_name (| globals, locals_stack, "EVM_RECURSION_LIMIT" |);
M.call (|
M.get_field (| M.get_name (| globals, "sys" |), "getrecursionlimit" |),
M.get_field (| M.get_name (| globals, locals_stack, "sys" |), "getrecursionlimit" |),
make_list [],
make_dict []
|)
Expand Down
6 changes: 4 additions & 2 deletions CoqOfPython/ethereum/arrow_glacier/__init__.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
Require Import CoqOfPython.CoqOfPython.

Definition globals : string := "ethereum.arrow_glacier.__init__".
Definition globals : Globals.t := "ethereum.arrow_glacier.__init__".

Definition locals_stack : list Locals.t := [].

Definition expr_1 : Value.t :=
Constant.str "
Expand All @@ -13,7 +15,7 @@ Axiom ethereum_fork_criteria_imports_ByBlockNumber :

Definition FORK_CRITERIA : Value.t := M.run ltac:(M.monadic (
M.call (|
M.get_name (| globals, "ByBlockNumber" |),
M.get_name (| globals, locals_stack, "ByBlockNumber" |),
make_list [
Constant.int 13773000
],
Expand Down
4 changes: 3 additions & 1 deletion CoqOfPython/ethereum/arrow_glacier/blocks.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
Require Import CoqOfPython.CoqOfPython.

Definition globals : string := "ethereum.arrow_glacier.blocks".
Definition globals : Globals.t := "ethereum.arrow_glacier.blocks".

Definition locals_stack : list Locals.t := [].

Definition expr_1 : Value.t :=
Constant.str "
Expand Down
68 changes: 36 additions & 32 deletions CoqOfPython/ethereum/arrow_glacier/bloom.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
Require Import CoqOfPython.CoqOfPython.

Definition globals : string := "ethereum.arrow_glacier.bloom".
Definition globals : Globals.t := "ethereum.arrow_glacier.bloom".

Definition locals_stack : list Locals.t := [].

Definition expr_1 : Value.t :=
Constant.str "
Expand Down Expand Up @@ -37,8 +39,9 @@ Axiom ethereum_arrow_glacier_fork_types_imports_Bloom :
IsImported globals "ethereum.arrow_glacier.fork_types" "Bloom".

Definition add_to_bloom : Value.t -> Value.t -> M :=
fun (args kwargs : Value.t) => ltac:(M.monadic (
let _ := M.set_locals (| args, kwargs, [ "bloom"; "bloom_entry" ] |) in
fun (args kwargs : Value.t) =>
let- locals_stack := M.create_locals locals_stack args kwargs [ "bloom"; "bloom_entry" ] in
ltac:(M.monadic (
let _ := Constant.str "
Add a bloom entry to the bloom filter (`bloom`).

Expand All @@ -56,29 +59,29 @@ Definition add_to_bloom : Value.t -> Value.t -> M :=
let _ := M.assign_local (|
"hash" ,
M.call (|
M.get_name (| globals, "keccak256" |),
M.get_name (| globals, locals_stack, "keccak256" |),
make_list [
M.get_name (| globals, "bloom_entry" |)
M.get_name (| globals, locals_stack, "bloom_entry" |)
],
make_dict []
|)
|) in
let _ :=
M.for_ (|
M.get_name (| globals, "idx" |),
M.get_name (| globals, locals_stack, "idx" |),
make_tuple [ Constant.int 0; Constant.int 2; Constant.int 4 ],
ltac:(M.monadic (
let _ := M.assign_local (|
"bit_to_set" ,
BinOp.bit_and (|
M.call (|
M.get_field (| M.get_name (| globals, "Uint" |), "from_be_bytes" |),
M.get_field (| M.get_name (| globals, locals_stack, "Uint" |), "from_be_bytes" |),
make_list [
M.slice (|
M.get_name (| globals, "hash" |),
M.get_name (| globals, "idx" |),
M.get_name (| globals, locals_stack, "hash" |),
M.get_name (| globals, locals_stack, "idx" |),
BinOp.add (|
M.get_name (| globals, "idx" |),
M.get_name (| globals, locals_stack, "idx" |),
Constant.int 2
|),
Constant.None_
Expand All @@ -93,13 +96,13 @@ Definition add_to_bloom : Value.t -> Value.t -> M :=
"bit_index" ,
BinOp.sub (|
Constant.int 2047,
M.get_name (| globals, "bit_to_set" |)
M.get_name (| globals, locals_stack, "bit_to_set" |)
|)
|) in
let _ := M.assign_local (|
"byte_index" ,
BinOp.floor_div (|
M.get_name (| globals, "bit_index" |),
M.get_name (| globals, locals_stack, "bit_index" |),
Constant.int 8
|)
|) in
Expand All @@ -110,23 +113,23 @@ Definition add_to_bloom : Value.t -> Value.t -> M :=
BinOp.sub (|
Constant.int 7,
BinOp.mod_ (|
M.get_name (| globals, "bit_index" |),
M.get_name (| globals, locals_stack, "bit_index" |),
Constant.int 8
|)
|)
|)
|) in
let _ := M.assign (|
M.get_subscript (|
M.get_name (| globals, "bloom" |),
M.get_name (| globals, "byte_index" |)
M.get_name (| globals, locals_stack, "bloom" |),
M.get_name (| globals, locals_stack, "byte_index" |)
|),
BinOp.bit_or (|
M.get_subscript (|
M.get_name (| globals, "bloom" |),
M.get_name (| globals, "byte_index" |)
M.get_name (| globals, locals_stack, "bloom" |),
M.get_name (| globals, locals_stack, "byte_index" |)
|),
M.get_name (| globals, "bit_value" |)
M.get_name (| globals, locals_stack, "bit_value" |)
|)
|) in
M.pure Constant.None_
Expand All @@ -138,8 +141,9 @@ Definition add_to_bloom : Value.t -> Value.t -> M :=
M.pure Constant.None_)).

Definition logs_bloom : Value.t -> Value.t -> M :=
fun (args kwargs : Value.t) => ltac:(M.monadic (
let _ := M.set_locals (| args, kwargs, [ "logs" ] |) in
fun (args kwargs : Value.t) =>
let- locals_stack := M.create_locals locals_stack args kwargs [ "logs" ] in
ltac:(M.monadic (
let _ := Constant.str "
Obtain the logs bloom from a list of log entries.

Expand All @@ -159,27 +163,27 @@ Definition logs_bloom : Value.t -> Value.t -> M :=
(* At stmt: unsupported node type: AnnAssign *)
let _ :=
M.for_ (|
M.get_name (| globals, "log" |),
M.get_name (| globals, "logs" |),
M.get_name (| globals, locals_stack, "log" |),
M.get_name (| globals, locals_stack, "logs" |),
ltac:(M.monadic (
let _ := M.call (|
M.get_name (| globals, "add_to_bloom" |),
M.get_name (| globals, locals_stack, "add_to_bloom" |),
make_list [
M.get_name (| globals, "bloom" |);
M.get_field (| M.get_name (| globals, "log" |), "address" |)
M.get_name (| globals, locals_stack, "bloom" |);
M.get_field (| M.get_name (| globals, locals_stack, "log" |), "address" |)
],
make_dict []
|) in
let _ :=
M.for_ (|
M.get_name (| globals, "topic" |),
M.get_field (| M.get_name (| globals, "log" |), "topics" |),
M.get_name (| globals, locals_stack, "topic" |),
M.get_field (| M.get_name (| globals, locals_stack, "log" |), "topics" |),
ltac:(M.monadic (
let _ := M.call (|
M.get_name (| globals, "add_to_bloom" |),
M.get_name (| globals, locals_stack, "add_to_bloom" |),
make_list [
M.get_name (| globals, "bloom" |);
M.get_name (| globals, "topic" |)
M.get_name (| globals, locals_stack, "bloom" |);
M.get_name (| globals, locals_stack, "topic" |)
],
make_dict []
|) in
Expand All @@ -197,9 +201,9 @@ Definition logs_bloom : Value.t -> Value.t -> M :=
|) in
let _ := M.return_ (|
M.call (|
M.get_name (| globals, "Bloom" |),
M.get_name (| globals, locals_stack, "Bloom" |),
make_list [
M.get_name (| globals, "bloom" |)
M.get_name (| globals, locals_stack, "bloom" |)
],
make_dict []
|)
Expand Down
Loading
Loading