Skip to content

revm: add rust files and more links admitted #695

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

Merged
merged 3 commits into from
Mar 28, 2025
Merged

revm: add rust files and more links admitted #695

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bb85d8b
revm: add rust files and more links admitted
clarus Mar 28, 2025
598c4b8
links: add more links axioms for the instructions
clarus Mar 28, 2025
0f916d0
links: add automated generation of report for the instructions
clarus Mar 28, 2025
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
  •  
  •  
  •  
34 changes: 20 additions & 14 deletions .github/workflows/rust.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,12 @@ jobs:
# ./generate_ink_example.sh
# cd ..
# endGroup
# Generate markdown with progress on links for instructions
startGroup "Generate markdown with progress on links for instructions"
cd CoqOfRust/revm/revm_interpreter/instructions/links
python count_admitted.py > progress_on_links.md
cd ../../../../..
endGroup
startGroup "Save space"
cargo clean
endGroup
Expand All @@ -69,7 +75,7 @@ jobs:
time cargo build
touch src/lib.rs
time cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate the core library"
Expand All @@ -79,7 +85,7 @@ jobs:
touch src/lib.rs
export RUST_MIN_STACK=800000000
time cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ../../../..
endGroup
startGroup "Save space"
Expand All @@ -100,42 +106,42 @@ jobs:
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_bytecode/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_bytecode/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ..
# context/interface
cd context/interface
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../../CoqOfRust/revm/revm_context_interface/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../../CoqOfRust/revm/revm_context_interface/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ../..
# interpreter
cd interpreter
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_interpreter/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_interpreter/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ..
# precompile
cd precompile
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_precompile/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_precompile/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ..
# primitives
cd primitives
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_primitives/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_primitives/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ..
# specification
cd specification
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust --with-json
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_specification/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/revm/revm_specification/ --include='*/' --include='*.v' --include='*.rs' --include='*.json' --exclude='*'
cd ..
cd ../../..
endGroup
Expand All @@ -145,7 +151,7 @@ jobs:
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../CoqOfRust/ruint/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../CoqOfRust/ruint/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ../..
endGroup
startGroup "Translate Move Sui"
Expand All @@ -157,35 +163,35 @@ jobs:
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ..
# move-binary-format
cd move-binary-format
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ..
# move-bytecode-verifier
cd move-bytecode-verifier
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ..
# move-bytecode-verifier-meter
cd move-bytecode-verifier-meter
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ..
# move-core-types
cd move-core-types
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --exclude='*'
rsync -rcv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ..
cd ../../..
endGroup
Expand Down
Loading
Loading