diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 4359e323..1ce7ecfc 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,7 +8,7 @@ on: jobs: build: - runs-on: ubuntu-latest + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v3 with: diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 5db1a1c9..dd09b010 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -24,14 +24,10 @@ jobs: run: opam switch create refinedrust-ace --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda - name: Install coq run: eval $(opam env) && opam update && opam pin add coq 8.17.1 -y - #- name: Fix permissions - #run: chown -R 1000 . - name: ls run: ls -la . - name: Install openssl dependency run: sudo apt update && sudo apt install libssl-dev -y - - name: Pull RefinedRust - run: git clone https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git verification/refinedrust - name: Install rustup run: curl --proto "=https" --tlsv1.2 -sSf https://sh.rustup.rs | bash /dev/stdin "-y" - name: Setup Rust toolchain diff --git a/.gitmodules b/.gitmodules index 922dd6a4..64577a8f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,3 +7,6 @@ [submodule "security-monitor/opensbi"] path = security-monitor/opensbi url = https://github.com/riscv-software-src/opensbi.git +[submodule "verification/refinedrust"] + path = verification/refinedrust + url = https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git diff --git a/confidential-vms/linux_vm/configurations/qemu_riscv64_virt_defconfig b/confidential-vms/linux_vm/configurations/qemu_riscv64_virt_defconfig index b0671604..d7e4851c 100644 --- a/confidential-vms/linux_vm/configurations/qemu_riscv64_virt_defconfig +++ b/confidential-vms/linux_vm/configurations/qemu_riscv64_virt_defconfig @@ -77,4 +77,4 @@ BR2_PER_PACKAGE_DIRECTORIES=y BR2_VERBOSE=0 -BR2_PACKAGE_NVME=y \ No newline at end of file +BR2_PACKAGE_NVME=y diff --git a/verification/.gitignore b/verification/.gitignore index 4ee74ed8..a8276b4e 100644 --- a/verification/.gitignore +++ b/verification/.gitignore @@ -2,6 +2,5 @@ _opam _build log rustc-ice-* -refinedrust generated_code.bak _CoqProject diff --git a/verification/refinedrust b/verification/refinedrust new file mode 160000 index 00000000..00723737 --- /dev/null +++ b/verification/refinedrust @@ -0,0 +1 @@ +Subproject commit 00723737488d913a2e510b1a1698dbe975ad118e diff --git a/verification/setup.md b/verification/setup.md index 5442f9b6..fcdd39b8 100644 --- a/verification/setup.md +++ b/verification/setup.md @@ -11,10 +11,7 @@ This file documents the basic verification setup. For using the RefinedRust toolchain and checking the verified parts of the code, you need to install both the Coq proof assistant and RefinedRust Coq libraries as well as the RefinedRust frontend. First of all, open a terminal and navigate to the directory containing this file. -Then, clone the RefinedRust repository into a subdirectory: -``` -git clone https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev.git refinedrust -``` +Make sure that there is a subdirectory called `refinedrust` that is up-to-date. ### Installing Coq and the RefinedRust Coq libraries