sui: add translation of the Move code in the CI

formal-land · Aug 27, 2024 · 4a1709e · 4a1709e
1 parent 02aac92
commit 4a1709e
Show file tree

Hide file tree

Showing 65 changed files with 375,235 additions and 2 deletions.
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -111,6 +111,47 @@ jobs:
             cd ..
             cd ../../..
           endGroup
+          startGroup "Translate Move Sui"
+            cd third-party/move-sui
+            cp ../../rust-toolchain ./
+            cd crates
+            # move-abstract-stack
+            cd move-abstract-stack
+            cargo build
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --exclude='*'
+            cd ..
+            # move-binary-format
+            cd move-binary-format
+            cargo build
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --exclude='*'
+            cd ..
+            # move-bytecode-verifier
+            cd move-bytecode-verifier
+            cargo build
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --exclude='*'
+            cd ..
+            # move-bytecode-verifier-meter
+            cd move-bytecode-verifier-meter
+            cargo build
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --exclude='*'
+            cd ..
+            # move-core-types
+            cd move-core-types
+            cargo build
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --exclude='*'
+            cd ..
+            cd ../../..
+          endGroup
           startGroup "Check that the diff is empty (excluding submodules)"
             git -c color.ui=always diff --exit-code --ignore-submodules=dirty
           endGroup

diff --git a/.gitmodules b/.gitmodules
@@ -7,3 +7,6 @@
 [submodule "third-party/revm"]
 	path = third-party/revm
 	url = https://github.com/bluealloy/revm.git
+[submodule "third-party/move-sui"]
+	path = third-party/move-sui
+	url = https://github.com/move-language/move-sui.git