mutation-trace protocol #22
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: Quint | |
| on: | |
| pull_request: | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| detect: | |
| name: Detect Quint changes | |
| runs-on: ubuntu-latest | |
| outputs: | |
| quint: ${{ steps.changes.outputs.quint }} | |
| steps: | |
| - name: Harden the runner (Audit all outbound calls) | |
| uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0 | |
| with: | |
| egress-policy: audit | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Detect Quint changes | |
| id: changes | |
| env: | |
| EVENT_NAME: ${{ github.event_name }} | |
| BASE_SHA: ${{ github.event.pull_request.base.sha }} | |
| HEAD_SHA: ${{ github.event.pull_request.head.sha }} | |
| run: | | |
| if [ "$EVENT_NAME" = "workflow_dispatch" ]; then | |
| echo "quint=true" >> "$GITHUB_OUTPUT" | |
| exit 0 | |
| fi | |
| if git diff --name-only "$BASE_SHA" "$HEAD_SHA" | grep -Eq '(\.qnt$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then | |
| echo "quint=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "quint=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: No Quint-relevant changes | |
| if: steps.changes.outputs.quint != 'true' | |
| run: echo "No Quint-relevant changes; validation skipped." | |
| quint-checks: | |
| name: Quint checks | |
| needs: detect | |
| if: needs.detect.outputs.quint == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - name: Harden the runner (Audit all outbound calls) | |
| uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0 | |
| with: | |
| egress-policy: audit | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Install Nix | |
| uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - name: Enable Magic Nix Cache | |
| uses: DeterminateSystems/magic-nix-cache-action@908b263ff629f4cc17666315b7fd3ec127c6244d # v14 | |
| with: | |
| use-flakehub: false | |
| use-gha-cache: true | |
| - name: Typecheck Quint spec | |
| run: nix run .#quint -- typecheck spec/mutation_cursor.qnt | |
| - name: Run Quint tests | |
| run: nix run .#quint -- test spec/mutation_cursor.qnt | |
| - name: Randomized Quint safety check | |
| run: > | |
| nix run .#quint -- | |
| run spec/mutation_cursor.qnt | |
| --step=verifyStep | |
| --invariants SafetyCore SafetyAttribution SafetyHistory | |
| --max-samples=5000 | |
| --max-steps=20 | |
| gate: | |
| name: Quint gate | |
| if: always() | |
| needs: | |
| - detect | |
| - quint-checks | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check Quint result | |
| env: | |
| CHANGED: ${{ needs.detect.outputs.quint }} | |
| DETECT_RESULT: ${{ needs.detect.result }} | |
| CHECK_RESULT: ${{ needs.quint-checks.result }} | |
| run: | | |
| if [ "$DETECT_RESULT" != "success" ]; then | |
| echo "Quint change detection failed (result: $DETECT_RESULT)." | |
| exit 1 | |
| fi | |
| case "$CHANGED" in | |
| false) | |
| echo "No Quint-relevant changes; validation skipped." | |
| exit 0 | |
| ;; | |
| true) | |
| ;; | |
| *) | |
| echo "Quint change detection produced an invalid result: $CHANGED" | |
| exit 1 | |
| ;; | |
| esac | |
| if [ "$CHECK_RESULT" != "success" ]; then | |
| echo "Quint validation failed (result: $CHECK_RESULT)." | |
| exit 1 | |
| fi |