Skip to content
Rust

Draft: more work on the simulations for the gas file #2386

Sign in to view logs

Draft: more work on the simulations for the gas file

Draft: more work on the simulations for the gas file #2386

Workflow file for this run

.github/workflows/rust.yml at 450a617
name: Rust
on:
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]
env:
CARGO_TERM_COLOR: always
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Download Git submodules
run: git submodule update --init --recursive
- uses: coq-community/docker-coq-action@v1
with:
custom_image: coqorg/coq:8.20-ocaml-4.14-flambda
custom_script: |
startGroup "Install dependencies"
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
source "$HOME/.cargo/env"
rustup toolchain install nightly-2024-12-07-x86_64-unknown-linux-gnu
cargo --version
sudo ln -s `which python3` /usr/bin/python
opam install -y --deps-only CoqOfRust/coq-of-rust.opam
endGroup
startGroup "Build"
sudo chown -R $(whoami) .
rustup component add rust-src rustc-dev llvm-tools-preview
cargo build --verbose
endGroup
startGroup "Install"
cargo install --path lib/
endGroup
startGroup "Format check"
cargo fmt --check
endGroup
startGroup "Lint"
cargo clippy --all-targets --all-features -- -D warnings
endGroup
startGroup "Translate Rust examples"
python run_tests.py
endGroup
startGroup "Pre-process the smart contracts"
cd contracts
python source_to_generated.py
cd generated
for dir in * ; do cd $dir ; cargo check ; cd .. ; done
cd ../..
endGroup
# We disable for now this translation as this makes a panic!
# startGroup "Translate Ink! library"
# cd CoqOfRust
# ./generate_ink_example.sh
# cd ..
# endGroup
startGroup "Save space"
cargo clean
endGroup
startGroup "Translate the alloc library"
cd third-party/rust/library/alloc
cp ../../../../rust-toolchain ./
time cargo build
touch src/lib.rs
time cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate the core library"
cd third-party/rust/library/core
cp ../../../../rust-toolchain ./
time cargo build
touch src/lib.rs
export RUST_MIN_STACK=800000000
time cargo coq-of-rust
rsync -rcv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Save space"
cd third-party/rust/library/alloc
cargo clean
cd ../../../..
cd third-party/rust/library/core
cargo clean
cd ../../../..
endGroup
startGroup "Translate Revm"
cd third-party/revm
cp ../../rust-toolchain ./
cd crates
# We compile each library twice to avoid errors. TODO: investigate why this is needed
# bytecode
cd bytecode
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='*'
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='*'
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='*'
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='*'
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='*'
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='*'
cd ..
cd ../../..
endGroup
startGroup "Translate ruint"
cd third-party/uint
cp ../../rust-toolchain ./
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -rcv src/ ../../CoqOfRust/ruint/ --include='*/' --include='*.v' --exclude='*'
cd ../..
endGroup
startGroup "Translate Move Sui"
cd third-party/move-sui
cp ../../rust-toolchain ./
cd crates
# move-abstract-stack
cd move-abstract-stack
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='*'
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='*'
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='*'
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='*'
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='*'
cd ..
cd ../../..
endGroup
startGroup "Generate Rocq files from Python"
cd CoqOfRust
make generate
cd ..
endGroup
startGroup "Check that the diff is empty (excluding submodules)"
git -c color.ui=always diff --exit-code --ignore-submodules=dirty
endGroup
startGroup "Compile Coq translations"
cd CoqOfRust
python ./make_and_detect_warnings.py
cd ..
endGroup