Coq: re-verify 0 real gaps + fix build/verify from clean; add `just r… #401
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: Correspondence Validation | |
| on: | |
| push: | |
| branches: [main, develop] | |
| pull_request: | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| jobs: | |
| validate-correspondence: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@5b842231ba77f5c045dba54ac5560fed2db780e2 # nightly (2026-03-27) | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cache Rust dependencies | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: | | |
| ~/.cargo/bin/ | |
| ~/.cargo/registry/index/ | |
| ~/.cargo/registry/cache/ | |
| ~/.cargo/git/db/ | |
| impl/rust-cli/target/ | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Run correspondence validation | |
| run: bash scripts/validate-correspondence.sh | |
| working-directory: ${{ github.workspace }} | |
| - name: Upload validation report | |
| if: always() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 | |
| with: | |
| name: validation-report | |
| path: validation-report.md | |
| verify-proofs: | |
| name: verify-proofs (Coq build oracle) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Coq via apt | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y coq | |
| - name: Show Coq version | |
| run: coqc --version | |
| - name: Build Coq proofs (oracle) | |
| working-directory: proofs/coq | |
| run: | | |
| # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it. | |
| mkdir -p extracted | |
| coq_makefile -f _CoqProject -o Makefile | |
| make -j1 | |
| - name: Print Assumptions for top-level theorems | |
| working-directory: proofs/coq | |
| run: | | |
| # Coq disallows '-' in identifiers — use underscores in the helper file name. | |
| cat > /tmp/print_assumptions.v <<'EOF' | |
| Require Import ValenceShell.filesystem_composition. | |
| Require Import ValenceShell.copy_move_operations. | |
| Print Assumptions single_op_reversible. | |
| Print Assumptions operation_sequence_reversible. | |
| Print Assumptions reversible_creates_CNO. | |
| Print Assumptions copy_file_reversible. | |
| EOF | |
| coqc -R . ValenceShell /tmp/print_assumptions.v 2>&1 | tee print_assumptions.log | |
| echo "=== Print Assumptions surfaced (see job log above) ===" | |
| property-testing: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable | |
| - name: Run property-based tests | |
| run: | | |
| cd impl/rust-cli | |
| cargo test --lib -- --test-threads=1 prop_ | |
| env: | |
| PROPTEST_CASES: 1000 # More cases in CI | |
| - name: Run correspondence tests | |
| run: | | |
| cd impl/rust-cli | |
| cargo test --test correspondence_tests -- --nocapture |