shared-context-engineering/.github/workflows/quint.yml at main · crocoder-dev/shared-context-engineering · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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