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

Draft: more links for the Revm interpreter #562

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Draft: more links for the Revm interpreter #562

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c1bb45b
revm: add links for the default of the gas
clarus Jun 1, 2024
f7944e4
revm: definition of clone impl per method
clarus Jun 1, 2024
2190c07
links: more progress of the gas linking
clarus Jun 2, 2024
ceab62a
links: group the to_value and to_ty again
clarus Jun 2, 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
  •  
  •  
  •  
12 changes: 6 additions & 6 deletions .github/workflows/rust.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ jobs:
cargo build
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate the core library"
Expand All @@ -73,7 +73,7 @@ jobs:
cargo build
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate Revm"
Expand All @@ -86,28 +86,28 @@ jobs:
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/interpreter/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/interpreter/ --include='*/' --include='*.v' --exclude='*'
cd ..
# precompile
cd precompile
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/precompile/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/precompile/ --include='*/' --include='*.v' --exclude='*'
cd ..
# primitives
cd primitives
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/primitives/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/primitives/ --include='*/' --include='*.v' --exclude='*'
cd ..
# revm
cd revm
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/revm/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/revm/ --include='*/' --include='*.v' --exclude='*'
cd ..
cd ../../..
endGroup
Expand Down
47 changes: 0 additions & 47 deletions CoqOfRust/CoqOfRust.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,50 +40,3 @@ Parameter pointer_coercion : string -> Value.t -> Value.t.
Parameter InlineAssembly : Value.t.

Parameter UnsupportedLiteral : Value.t.

(** There is an automatic instanciation of the function traits for closures and functions. *)
Module FunctionTraitAutomaticImpl.
Axiom FunctionImplementsFn :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::Fn"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
end
)) ].

Axiom FunctionImplementsFnMut :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::FnMut"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_mut", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
end
)) ].

Axiom FunctionImplementsFnOnce :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::FnOnce"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_once", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
M.call_closure self args
| _, _ => M.impossible
end
)) ].
End FunctionTraitAutomaticImpl.
Loading
Loading