Repository navigation
fix(test): model oracle test fails instead of skipping as a pass (P0-4) #82
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: MPL-2.0 | |
| name: Lean Verification Build | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'proofs/lean4/**' | |
| - 'impl/rust-cli/src/proof_refs.rs' | |
| - '.github/workflows/lean-verification.yml' | |
| pull_request: | |
| paths: | |
| - 'proofs/lean4/**' | |
| - 'impl/ocaml/**' | |
| - 'impl/rust-cli/**' | |
| workflow_dispatch: | |
| permissions: | |
| actions: read | |
| contents: read | |
| jobs: | |
| build-lean-extraction: | |
| name: Build and Test Lean Extraction Pipeline | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4 | |
| - name: Install Lean 4 | |
| run: | | |
| # Download the elan installer pinned to an immutable release tag, | |
| # verify its SHA-256, then execute it — no `curl | sh`. | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh | |
| echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310 elan-init.sh" | sha256sum -c - | |
| sh elan-init.sh -y | |
| rm -f elan-init.sh | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Verify Lean installation | |
| run: | | |
| source $HOME/.elan/env | |
| lean --version | |
| lean --print-prefix | |
| ls -la $(lean --print-prefix)/lib/lean/libleanshared.so | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b | |
| with: | |
| toolchain: stable | |
| - name: Cache Lean build | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: proofs/lean4/.lake | |
| key: ${{ runner.os }}-lean-${{ hashFiles('proofs/lean4/lakefile.lean', 'proofs/lean4/lean-toolchain') }} | |
| - name: Build Lean extraction | |
| run: | | |
| source $HOME/.elan/env | |
| cd proofs/lean4 | |
| lake build Extraction | |
| - name: Verify Lean extraction output | |
| run: | | |
| ls -lh proofs/lean4/.lake/build/ir/Extraction.c | |
| wc -l proofs/lean4/.lake/build/ir/Extraction.c | |
| - name: Build C wrapper library | |
| run: | | |
| source $HOME/.elan/env | |
| cd impl/ocaml | |
| lean_prefix="$(lean --print-prefix)" | |
| lean_include="$lean_prefix/include" | |
| lean_lib="$lean_prefix/lib/lean" | |
| gcc -shared -fPIC -o liblean_vsh.so \ | |
| lean_wrapper.c \ | |
| ../../proofs/lean4/.lake/build/ir/Extraction.c \ | |
| -I"$lean_include" \ | |
| -L"$lean_lib" \ | |
| -lleanshared \ | |
| -Wl,-rpath,"$lean_lib" | |
| - name: Verify shared library | |
| run: | | |
| ls -lh impl/ocaml/liblean_vsh.so | |
| ldd impl/ocaml/liblean_vsh.so | |
| nm -D impl/ocaml/liblean_vsh.so | grep vsh_safe || echo "Warning: vsh_safe functions not exported" | |
| - name: Cache Rust build | |
| uses: Swatinem/rust-cache@f0d9c3887740aee45f6153b24b3a6b815192ec16 # v2 | |
| with: | |
| workspaces: impl/rust-cli | |
| - name: Build Rust without Lean (baseline) | |
| run: | | |
| cd impl/rust-cli | |
| cargo build --release | |
| ls -lh target/release/vsh | |
| - name: Test Rust without Lean | |
| run: | | |
| cd impl/rust-cli | |
| cargo test | |
| cargo test --test correspondence_tests | |
| cargo test --test property_correspondence_tests | |
| - name: Build Lean model oracle (proof artifact as test oracle) | |
| run: | | |
| source $HOME/.elan/env | |
| cd proofs/lean4 | |
| lake build model_oracle | |
| ls -lh .lake/build/bin/model_oracle | |
| - name: Differential correspondence (proven Lean model vs Rust impl) | |
| run: | | |
| cd impl/rust-cli | |
| cargo test --test model_oracle_correspondence -- --ignored --nocapture | |
| - name: Report Rust binary size | |
| run: | | |
| echo "Rust binary: $(stat -c%s impl/rust-cli/target/release/vsh) bytes" | |
| - name: Upload artifacts | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 | |
| with: | |
| name: lean-extraction-artifacts | |
| path: | | |
| proofs/lean4/.lake/build/ir/Extraction.c | |
| impl/ocaml/liblean_vsh.so | |
| impl/rust-cli/target/release/vsh |