nucleus/.github/workflows/kani-nightly.yml at b3fc95c63afb4e9455b2d31f3659331a6fda098c · coproduct-opensource/nucleus · 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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
name: Kani BMC

on:
  push:
    branches: ["main"]
    paths:
      - "crates/portcullis/src/**"
      - "crates/ck-*/src/**"
      - ".kani-minimum-proofs"
      - ".github/workflows/kani-nightly.yml"
  pull_request:
    paths:
      - "crates/portcullis/src/**"
      - "crates/ck-*/src/**"
      - ".kani-minimum-proofs"
      - ".github/workflows/kani-nightly.yml"
  schedule:
    - cron: "17 3 * * *"
  workflow_dispatch:

permissions:
  contents: read

jobs:
  # Fast tier: 5 lightweight harnesses — runs on every PR and push
  # The 3 normalize_* harnesses use build_ordered_permissions() which creates
  # a massive symbolic state space (24 symbolic capabilities + obligations).
  # They require 15+ minutes each and are verified in the nightly full tier.
  kani-fast:
    name: Kani
    runs-on: ubuntu-24.04
    timeout-minutes: 15
    if: github.event_name != 'schedule'
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
      - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
        with:
          cache-on-failure: true
      - name: Cache Kani toolchain
        uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3
        with:
          path: ~/.kani
          key: kani-toolchain-${{ runner.os }}-${{ hashFiles('.github/workflows/kani-nightly.yml') }}
      - name: Run Kani (fast harnesses)
        uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
        with:
          args: >-
            -p portcullis
            --solver cadical
            --harness proof_capability_distributive
            --harness proof_exposureset_monoid_identity
            --harness proof_exposureset_uninhabitable_iff_count_three
            --harness proof_operation_exposure_completeness
            --harness proof_clinejection_blocked
      - name: Proof count regression gate
        run: |
          PROOF_COUNT=$(grep -c '#\[kani::proof\]' crates/portcullis/src/kani.rs)
          MINIMUM=$(cat .kani-minimum-proofs | tr -d '[:space:]')
          echo "Kani proof harnesses: $PROOF_COUNT (minimum: $MINIMUM)"
          if [ "$PROOF_COUNT" -lt "$MINIMUM" ]; then
            echo "::error::Kani proof count regression: $PROOF_COUNT < $MINIMUM"
            exit 1
          fi
      - name: Summary
        if: always()
        run: |
          PROOF_COUNT=$(grep -c '#\[kani::proof\]' crates/portcullis/src/kani.rs)
          MINIMUM=$(cat .kani-minimum-proofs | tr -d '[:space:]')
          echo "## Kani BMC Results (fast tier)" >> "$GITHUB_STEP_SUMMARY"
          echo "" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Harnesses verified:** 5 / $PROOF_COUNT (fast tier)" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Solver:** CaDiCaL" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Minimum required:** $MINIMUM" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Full suite:** nightly + workflow_dispatch" >> "$GITHUB_STEP_SUMMARY"

  # Constitutional Kernel (fast): 4 concrete-policy proofs — no symbolic BTreeSet
  # These use only concrete BTreeSets + symbolic u64, finishing in <10 min.
  # The 7 symbolic BTreeSet proofs (capability, governance, I/O axes) run nightly.
  kani-constitutional:
    name: Kani (constitutional kernel)
    runs-on: ubuntu-24.04
    timeout-minutes: 15
    if: github.event_name != 'schedule'
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
      - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
        with:
          cache-on-failure: true
      - name: Cache Kani toolchain
        uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3
        with:
          path: ~/.kani
          key: kani-toolchain-${{ runner.os }}-${{ hashFiles('.github/workflows/kani-nightly.yml') }}
      - name: Run Kani (constitutional kernel — fast tier)
        uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
        with:
          args: >-
            -p ck-kernel
            --solver cadical
            --harness proof_budget_escalation_detected
            --harness proof_capability_escalation_detected_bitmask
            --harness proof_io_confinement_detected_bitmask
            --harness proof_combined_monotonicity_complete
            --harness proof_capability_subset_transitive
      - name: Summary
        if: always()
        run: |
          TOTAL=$(grep -c '#\[kani::proof\]' crates/ck-kernel/src/kani.rs)
          echo "## Kani BMC — Constitutional Kernel (fast tier)" >> "$GITHUB_STEP_SUMMARY"
          echo "" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Harnesses verified:** 5 / $TOTAL (fast tier — pure bitmask)" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Proved:** budget escalation, capability non-escalation, I/O confinement, combined monotonicity, lattice transitivity" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Nightly:** 11 symbolic BTreeSet proofs via admit() pipeline" >> "$GITHUB_STEP_SUMMARY"

  # Constitutional Kernel (full): all 11 harnesses including symbolic BTreeSet proofs
  # symbolic_set() proofs take 5-15 min each due to BTreeSet node machinery.
  kani-constitutional-full:
    name: Kani (constitutional kernel full)
    runs-on: ubuntu-24.04
    timeout-minutes: 60
    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
      - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
        with:
          cache-on-failure: true
      - name: Cache Kani toolchain
        uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3
        with:
          path: ~/.kani
          key: kani-toolchain-${{ runner.os }}-${{ hashFiles('.github/workflows/kani-nightly.yml') }}
      - name: Run Kani (constitutional kernel — all harnesses)
        uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
        with:
          args: "-p ck-kernel --solver cadical"
      - name: Summary
        if: always()
        run: |
          TOTAL=$(grep -c '#\[kani::proof\]' crates/ck-kernel/src/kani.rs)
          echo "## Kani BMC — Constitutional Kernel (full)" >> "$GITHUB_STEP_SUMMARY"
          echo "" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Harnesses verified:** $TOTAL / $TOTAL (all)" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Proved:** ALL constitutional invariants including symbolic BTreeSet proofs" >> "$GITHUB_STEP_SUMMARY"

  # Full tier: all harnesses including normalize_* — nightly and on-demand only
  # normalize_* harnesses each take 15+ minutes due to large symbolic state space
  kani-full:
    name: Kani (full)
    runs-on: ubuntu-24.04
    timeout-minutes: 60
    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
      - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
        with:
          cache-on-failure: true
      - name: Cache Kani toolchain
        uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3
        with:
          path: ~/.kani
          key: kani-toolchain-${{ runner.os }}-${{ hashFiles('.github/workflows/kani-nightly.yml') }}
      - name: Run Kani (all harnesses)
        uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
        with:
          args: "-p portcullis --solver cadical"
      - name: Proof count regression gate
        run: |
          PROOF_COUNT=$(grep -c '#\[kani::proof\]' crates/portcullis/src/kani.rs)
          MINIMUM=$(cat .kani-minimum-proofs | tr -d '[:space:]')
          echo "Kani proof harnesses: $PROOF_COUNT (minimum: $MINIMUM)"
          if [ "$PROOF_COUNT" -lt "$MINIMUM" ]; then
            echo "::error::Kani proof count regression: $PROOF_COUNT < $MINIMUM"
            exit 1
          fi
      - name: Summary
        if: always()
        run: |
          PROOF_COUNT=$(grep -c '#\[kani::proof\]' crates/portcullis/src/kani.rs)
          MINIMUM=$(cat .kani-minimum-proofs | tr -d '[:space:]')
          echo "## Kani BMC Results (full suite)" >> "$GITHUB_STEP_SUMMARY"
          echo "" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Harnesses verified:** $PROOF_COUNT / $PROOF_COUNT (all)" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Solver:** CaDiCaL" >> "$GITHUB_STEP_SUMMARY"
          echo "- **Minimum required:** $MINIMUM" >> "$GITHUB_STEP_SUMMARY"