verify.yml

---
name: Verification tests

on: [push, pull_request]


jobs:
  build:
    name: Verify
    runs-on: ubuntu-latest  # container actions require GNU/Linux
    steps:
    - name: Checkout repository
      uses: actions/checkout@v4
      with:
        persist-credentials: false
        submodules: 'true'
    - name: Install opam dependencies
      run: sudo apt update -y && sudo apt install -y pkg-config git rsync tar unzip m4 time curl ocaml build-essential bubblewrap gawk libgmp-dev python2.7 python3 python3-distutils libmpfr-dev
    - name: Install opam
      run: curl "https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-x86_64-linux" -Lo /usr/local/bin/opam && chmod +x /usr/local/bin/opam
    - name: Setup opam
      run: opam init -y
    - name: Setup opam switch
      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: ls
      run: ls -la .
    - name: Install openssl dependency
      run: sudo apt update && sudo apt install libssl-dev -y
    - name: Install rustup
      run: curl --proto "=https" --tlsv1.2 -sSf https://sh.rustup.rs | bash /dev/stdin "-y"
    - name: Setup Rust toolchain
      run: source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-rust.sh
    - name: Install the RiscV target for RefinedRust's toolchain
      run: source "$HOME/.cargo/env" && cd ./verification/refinedrust/rr_frontend && rustup target add riscv64gc-unknown-none-elf
    - name: Install frontend
      run: source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-frontend.sh
    - name: Install Opam dependencies
      run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-coq.sh
    - name: Install RefinedRust type system
      run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-typesystem.sh
    - name: Install RefinedRust stdlib
      run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-stdlib.sh
    - name: Generate stdlib metadata
      run: eval $(opam env) && make -C verification/refinedrust/stdlib generate_stdlib
    - name: Exclude RefinedRust from dune build
      run: echo "(dirs :standard \ generated_code.bak refinedrust)" > verification/dune
    - name: install build dependencies
      run: sudo apt -qq -y install wget autoconf automake autotools-dev curl python3 libmpc-dev libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev libexpat-dev xz-utils
    - name: install OpenSBI dependencies
      run: sudo apt -qq -y install clang
    - name: install Buildroot dependencies
      run: sudo apt -qq -y install unzip sed binutils diffutils build-essential bash patch gzip bzip2 perl tar cpio unzip rsync file bc findutils
    - name: make setup
      run: source "$HOME/.cargo/env" && eval $(opam env) && make setup
    - name: make devtools
      run: source "$HOME/.cargo/env" && eval $(opam env) && make devtools
    - name: Translate specified files using RefinedRust and check proofs
      run: source "$HOME/.cargo/env" && eval $(opam env) && make verify