Gate Z3 integration tests to tier-1 CI and simplify pytest step. #10
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
| name: Native Backends Tier 1 | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'ovk/**' | |
| - 'adapters/**' | |
| - 'scripts/ci/install_backend.sh' | |
| - 'tests/test_*native*' | |
| - 'tests/test_opa_optional_integration.py' | |
| - 'tests/test_z3_native_integration.py' | |
| - 'tests/test_cbmc_native_integration.py' | |
| - 'tests/test_cedar_native_integration.py' | |
| - '.github/workflows/native-backends-tier1.yml' | |
| pull_request: | |
| paths: | |
| - 'ovk/**' | |
| - 'adapters/**' | |
| - 'scripts/ci/install_backend.sh' | |
| - 'tests/test_*native*' | |
| - 'tests/test_opa_optional_integration.py' | |
| - 'tests/test_z3_native_integration.py' | |
| - 'tests/test_cbmc_native_integration.py' | |
| - 'tests/test_cedar_native_integration.py' | |
| - '.github/workflows/native-backends-tier1.yml' | |
| workflow_dispatch: | |
| jobs: | |
| native-backend-tier1: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: [opa, z3, cbmc, cedar] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Cache z3-solver wheel | |
| if: matrix.backend == 'z3' | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.cache/pip | |
| key: z3-solver-4.13.4.0-${{ runner.os }}-py3.11 | |
| - name: Cache cargo registry | |
| if: matrix.backend == 'cedar' | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| ~/.cargo/bin/cedar | |
| key: cedar-policy-cli-4.8.2-${{ runner.os }} | |
| - name: Install backend | |
| run: bash scripts/ci/install_backend.sh ${{ matrix.backend }} | |
| - name: Install package | |
| run: pip install -e '.[dev]' | |
| - name: Run native backend probe | |
| run: pytest tests/test_native_backends.py -m native_backend -v -k ${{ matrix.backend }} | |
| env: | |
| OVK_NATIVE_BACKEND: ${{ matrix.backend }} | |
| - name: Run per-backend integration tests | |
| run: | | |
| case "${{ matrix.backend }}" in | |
| opa) pytest tests/test_opa_optional_integration.py -v ;; | |
| z3) pytest tests/test_z3_native_integration.py -v ;; | |
| cbmc) pytest tests/test_cbmc_native_integration.py -v ;; | |
| cedar) pytest tests/test_cedar_native_integration.py -v ;; | |
| esac | |
| native-tier1-summary: | |
| runs-on: ubuntu-latest | |
| needs: native-backend-tier1 | |
| if: always() | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Install package | |
| run: pip install -e '.[dev]' | |
| - name: Write tier1 summary | |
| run: | | |
| python - <<'PY' >> "$GITHUB_STEP_SUMMARY" | |
| from ovk.core.native_backend_probe import probe_all_native_backends | |
| tier1 = {"opa", "z3", "cbmc", "cedar"} | |
| print("## Native Backend Tier 1 (required)") | |
| print("| Backend | Binary | Contract | Native Used | Fixture Match |") | |
| print("|---------|--------|----------|-------------|---------------|") | |
| for result in probe_all_native_backends(): | |
| if result.backend not in tier1: | |
| continue | |
| print( | |
| f"| {result.backend} | " | |
| f"{'yes' if result.binary_present else 'no'} | " | |
| f"{'ok' if result.contract_roundtrip_ok else 'fail'} | " | |
| f"{'yes' if result.native_binary_used else 'no'} | " | |
| f"{'yes' if result.fixture_matches_oracle else 'no'} |" | |
| ) | |
| PY |