1  name: CI - Effects System Enforcement
  2  
  3  on:
  4    push:
  5      branches: [main, develop]
  6    pull_request:
  7      branches: [main, develop]
  8  
  9  env:
 10    CARGO_TERM_COLOR: always
 11    RUST_BACKTRACE: 1
 12  
 13  jobs:
 14    format:
 15      name: Format Check
 16      runs-on: ubuntu-latest
 17      steps:
 18        - uses: actions/checkout@v4
 19        - name: Install Rust
 20          uses: actions-rust-lang/setup-rust-toolchain@v1
 21          with:
 22            components: rustfmt
 23        - name: Check formatting
 24          run: cargo fmt --all -- --check
 25  
 26    clippy-effects-enforcement:
 27      name: Clippy - Effects System Enforcement
 28      runs-on: ubuntu-latest
 29      steps:
 30        - uses: actions/checkout@v4
 31        - name: Install Rust
 32          uses: actions-rust-lang/setup-rust-toolchain@v1
 33          with:
 34            components: clippy
 35        - name: Cache cargo registry
 36          uses: actions/cache@v3
 37          with:
 38            path: ~/.cargo/registry
 39            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
 40        - name: Cache cargo index
 41          uses: actions/cache@v3
 42          with:
 43            path: ~/.cargo/git
 44            key: ${{ runner.os }}-cargo-index-${{ hashFiles('**/Cargo.lock') }}
 45        - name: Cache cargo build
 46          uses: actions/cache@v3
 47          with:
 48            path: target
 49            key: ${{ runner.os }}-cargo-build-target-${{ hashFiles('**/Cargo.lock') }}
 50        - name: Run clippy with effects enforcement
 51          run: |
 52            cargo clippy --workspace --all-targets --verbose -- \
 53              -D warnings \
 54              -D clippy::disallowed_methods \
 55              -D clippy::disallowed_types \
 56              -D clippy::unwrap_used \
 57              -D clippy::expect_used \
 58              -D clippy::duplicated_attributes
 59  
 60    test:
 61      name: Test Suite
 62      runs-on: ubuntu-latest
 63      steps:
 64        - uses: actions/checkout@v4
 65        - name: Install Rust
 66          uses: actions-rust-lang/setup-rust-toolchain@v1
 67        - name: Install Quint
 68          run: npm install -g @informalsystems/quint@0.25.1
 69        - name: Cache cargo registry
 70          uses: actions/cache@v3
 71          with:
 72            path: ~/.cargo/registry
 73            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
 74        - name: Cache cargo index
 75          uses: actions/cache@v3
 76          with:
 77            path: ~/.cargo/git
 78            key: ${{ runner.os }}-cargo-index-${{ hashFiles('**/Cargo.lock') }}
 79        - name: Cache cargo build
 80          uses: actions/cache@v3
 81          with:
 82            path: target
 83            key: ${{ runner.os }}-cargo-build-target-${{ hashFiles('**/Cargo.lock') }}
 84        - name: Run tests
 85          run: cargo test --workspace --verbose
 86  
 87    check-effects-violations:
 88      name: Check for Effects System Violations
 89      runs-on: ubuntu-latest
 90      steps:
 91        - uses: actions/checkout@v4
 92        - name: Install ripgrep
 93          run: sudo apt-get update && sudo apt-get install -y ripgrep
 94        - name: Check for direct time usage
 95          run: |
 96            echo "Checking for direct time usage violations..."
 97  
 98            # Get files with violations
 99            files_with_violations=$(rg --type rust "SystemTime::now|Instant::now|chrono::Utc::now" crates/ \
100                --files-with-matches \
101                --glob '!**/aura-agent/**' \
102                --glob '!**/aura-effects/**' \
103                --glob '!**/aura-simulator/**' \
104                --glob '!**/aura-testkit/**' \
105                --glob '!**/aura-terminal/**' \
106                --glob '!**/tests/**' \
107                --glob '!**/integration/**' \
108                --glob '!**/demo/**' 2>/dev/null || true)
109  
110            violations=""
111            for file in $files_with_violations; do
112              # Skip files with allow attribute in test modules
113              if grep -q "#\[cfg(test)\]" "$file" && \
114                 grep -A 5 "#\[cfg(test)\]" "$file" | grep -q "#!\[allow(clippy::disallowed_methods)\]"; then
115                continue
116              fi
117  
118              # Get violations from this file, excluding comments
119              file_violations=$(rg "SystemTime::now|Instant::now|chrono::Utc::now" "$file" --line-number 2>/dev/null | \
120                  grep -v '^\s*//' | \
121                  grep -v ':\s*//' || true)
122  
123              if [ -n "$file_violations" ]; then
124                violations="$violations$file_violations"$'\n'
125              fi
126            done
127  
128            if [ -n "$violations" ]; then
129              echo "$violations"
130              echo "[ERROR] Found direct time usage! Use effects.now() instead."
131              exit 1
132            else
133              echo "[OK] No direct time usage violations found"
134            fi
135        - name: Check for direct randomness usage
136          run: |
137            echo "Checking for direct randomness usage violations..."
138            if rg --type rust "rand::random|thread_rng\(\)|OsRng::new" crates/ --line-number \
139                --glob '!**/aura-agent/**' \
140                --glob '!**/aura-effects/**' \
141                --glob '!**/aura-simulator/**' \
142                --glob '!**/aura-testkit/**' \
143                --glob '!**/tests/**'; then
144              echo "[ERROR] Found direct randomness usage! Use effects.random_bytes() or effects.rng() instead."
145              exit 1
146            else
147              echo "[OK] No direct randomness usage violations found"
148            fi
149        - name: Check for direct UUID usage
150          run: |
151            echo "Checking for direct UUID usage violations..."
152  
153            # Get files with violations
154            files_with_violations=$(rg --type rust "Uuid::new_v4\(\)" crates/ \
155                --files-with-matches \
156                --glob '!**/aura-effects/**' \
157                --glob '!**/aura-agent/**' \
158                --glob '!**/aura-simulator/**' \
159                --glob '!**/aura-testkit/**' \
160                --glob '!**/aura-quint/**' \
161                --glob '!**/aura-terminal/**' \
162                --glob '!**/tests/**' \
163                --glob '!**/aura-core/src/types/identifiers.rs' \
164                --glob '!**/aura-core/src/effects/quint.rs' \
165                --glob '!**/aura-composition/src/registry.rs' \
166                --glob '!**/aura-sync/src/services/maintenance.rs' \
167                --glob '!**/aura-sync/src/infrastructure/peers.rs' 2>/dev/null || true)
168  
169            violations=""
170            for file in $files_with_violations; do
171              # Skip files with allow attribute in test modules
172              if grep -q "#\[cfg(test)\]" "$file" && \
173                 grep -A 5 "#\[cfg(test)\]" "$file" | grep -q "#\[allow(clippy::disallowed_methods)\]"; then
174                continue
175              fi
176  
177              # Get violations from this file, excluding comments
178              file_violations=$(rg "Uuid::new_v4\(\)" "$file" --line-number 2>/dev/null | \
179                  grep -v '^\s*//' | \
180                  grep -v ':\s*//' || true)
181  
182              if [ -n "$file_violations" ]; then
183                violations="$violations$file_violations"$'\n'
184              fi
185            done
186  
187            if [ -n "$violations" ]; then
188              echo "$violations"
189              echo "[ERROR] Found direct UUID usage! Use effects.gen_uuid() instead."
190              exit 1
191            else
192              echo "[OK] No direct UUID usage violations found"
193            fi
194  
195    check-documentation-links:
196      name: Check Documentation Links
197      runs-on: ubuntu-latest
198      steps:
199        - uses: actions/checkout@v4
200        - name: Check markdown links
201          uses: gaurav-nelson/github-action-markdown-link-check@v1
202          with:
203            use-quiet-mode: "yes"
204            use-verbose-mode: "yes"
205            config-file: ".github/config/markdown-link-check.json"
206            base-branch: "main"
207  
208    build:
209      name: Build Check
210      runs-on: ubuntu-latest
211      steps:
212        - uses: actions/checkout@v4
213        - name: Install Rust
214          uses: actions-rust-lang/setup-rust-toolchain@v1
215        - name: Cache cargo registry
216          uses: actions/cache@v3
217          with:
218            path: ~/.cargo/registry
219            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
220        - name: Cache cargo index
221          uses: actions/cache@v3
222          with:
223            path: ~/.cargo/git
224            key: ${{ runner.os }}-cargo-index-${{ hashFiles('**/Cargo.lock') }}
225        - name: Cache cargo build
226          uses: actions/cache@v3
227          with:
228            path: target
229            key: ${{ runner.os }}-cargo-build-target-${{ hashFiles('**/Cargo.lock') }}
230        - name: Build workspace
231          run: cargo build --workspace --verbose
232  
233    unused-dependencies:
234      name: Check Unused Dependencies
235      runs-on: ubuntu-latest
236      continue-on-error: true  # Warning only - don't fail CI
237      steps:
238        - uses: actions/checkout@v4
239        - name: Install Rust nightly
240          uses: actions-rust-lang/setup-rust-toolchain@v1
241          with:
242            toolchain: nightly
243        - name: Install cargo-udeps
244          run: cargo install cargo-udeps --locked
245        - name: Cache cargo registry
246          uses: actions/cache@v3
247          with:
248            path: ~/.cargo/registry
249            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
250        - name: Cache cargo index
251          uses: actions/cache@v3
252          with:
253            path: ~/.cargo/git
254            key: ${{ runner.os }}-cargo-index-${{ hashFiles('**/Cargo.lock') }}
255        - name: Check for unused dependencies
256          run: |
257            echo "Checking for unused dependencies..."
258            echo "Note: This job is advisory only and won't fail CI"
259            echo ""
260            cargo +nightly udeps --all-targets 2>&1 || true
261  
262    lint-test:
263      name: Verify Lint Enforcement Works
264      runs-on: ubuntu-latest
265      steps:
266        - uses: actions/checkout@v4
267        - name: Install Rust
268          uses: actions-rust-lang/setup-rust-toolchain@v1
269          with:
270            components: clippy
271        - name: Test lint enforcement (should fail)
272          run: |
273            echo "Testing that our lints catch violations..."
274            # This should fail due to linting violations
275            if cargo check --manifest-path=<(cat << 'EOF'
276            [package]
277            name = "lint-test"
278            version = "0.1.0"
279            edition = "2021"
280  
281            [lints]
282            workspace = true
283  
284            [dependencies]
285            uuid = "1.0"
286            rand = "0.8"
287  
288            [[bin]]
289            name = "test"
290            path = "test_lints.rs"
291            EOF
292            ); then
293              echo "[ERROR] Lints should have failed but didn't!"
294              exit 1
295            else
296              echo "[OK] Lints correctly caught violations"
297            fi
298  
299    lean-proofs:
300      name: Lean Formal Verification
301      runs-on: ubuntu-latest
302      # Only run when Lean files or kernel code changes
303      if: |
304        github.event_name == 'push' ||
305        contains(github.event.pull_request.labels.*.name, 'verification') ||
306        contains(join(github.event.pull_request.changed_files, ' '), 'verification/lean') ||
307        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-journal') ||
308        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-core/src/time')
309      steps:
310        - name: Free disk space
311          run: |
312            echo "Disk space before cleanup:"
313            df -h /
314            # Aggressive cleanup to ensure enough space for Nix store + cache
315            sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
316            sudo rm -rf /usr/local/share/boost
317            sudo rm -rf /usr/share/swift
318            sudo rm -rf /opt/hostedtoolcache/Python /opt/hostedtoolcache/Ruby /opt/hostedtoolcache/go /opt/hostedtoolcache/node
319            sudo docker image prune --all --force || true
320            sudo apt-get clean || true
321            echo "Disk space after cleanup:"
322            df -h /
323        - uses: actions/checkout@v4
324        - name: Install Nix
325          uses: cachix/install-nix-action@v27
326          with:
327            nix_path: nixpkgs=channel:nixos-unstable
328        - name: Cache Nix store
329          uses: actions/cache@v3
330          with:
331            path: /nix/store
332            key: ${{ runner.os }}-nix-lean-${{ hashFiles('flake.lock') }}
333            restore-keys: |
334              ${{ runner.os }}-nix-lean-
335              ${{ runner.os }}-nix-
336        - name: Build Lean proofs
337          run: |
338            echo "Building Lean formal verification modules..."
339            nix develop --command bash -c "cd verification/lean && lake build"
340        - name: Check for incomplete proofs
341          run: |
342            echo "Checking for incomplete proofs (sorry usage)..."
343            if grep -r "sorry" verification/lean/Aura --include="*.lean" 2>/dev/null; then
344              echo "[WARNING] Found incomplete proofs (sorry). These should be resolved."
345              # Don't fail CI for now, just warn
346            else
347              echo "[OK] All proofs complete (no sorry found)"
348            fi
349        - name: Cleanup before cache save
350          if: always()
351          run: |
352            # Run nix garbage collection to reduce store size
353            nix-collect-garbage -d || true
354            echo "Disk space before cache save:"
355            df -h /
356  
357    differential-testing:
358      name: Lean Differential Testing
359      runs-on: ubuntu-latest
360      needs: [lean-proofs]
361      # Only run when Lean or kernel code changes
362      if: |
363        github.event_name == 'push' ||
364        contains(github.event.pull_request.labels.*.name, 'verification') ||
365        contains(join(github.event.pull_request.changed_files, ' '), 'verification/lean') ||
366        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-journal') ||
367        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-core/src/time') ||
368        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-testkit')
369      steps:
370        - name: Free disk space
371          run: |
372            echo "Disk space before cleanup:"
373            df -h /
374            # Aggressive cleanup to ensure enough space for Nix store + cache
375            sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
376            sudo rm -rf /usr/local/share/boost
377            sudo rm -rf /usr/share/swift
378            sudo rm -rf /opt/hostedtoolcache/Python /opt/hostedtoolcache/Ruby /opt/hostedtoolcache/go /opt/hostedtoolcache/node
379            sudo docker image prune --all --force || true
380            sudo apt-get clean || true
381            echo "Disk space after cleanup:"
382            df -h /
383        - uses: actions/checkout@v4
384        - name: Install Nix
385          uses: cachix/install-nix-action@v27
386          with:
387            nix_path: nixpkgs=channel:nixos-unstable
388        - name: Cache Nix store
389          uses: actions/cache@v3
390          with:
391            path: /nix/store
392            key: ${{ runner.os }}-nix-differential-${{ hashFiles('flake.lock') }}
393            restore-keys: |
394              ${{ runner.os }}-nix-differential-
395              ${{ runner.os }}-nix-
396        - name: Cache cargo registry
397          uses: actions/cache@v3
398          with:
399            path: ~/.cargo/registry
400            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
401        - name: Cache cargo build
402          uses: actions/cache@v3
403          with:
404            path: target
405            key: ${{ runner.os }}-cargo-build-target-${{ hashFiles('**/Cargo.lock') }}
406        - name: Build Lean oracle
407          run: |
408            echo "Building Lean oracle verifier..."
409            nix develop --command just lean-oracle-build
410        - name: Run differential tests
411          run: |
412            echo "Running differential tests (Rust vs Lean oracle)..."
413            nix develop --command just test-differential
414        - name: Cleanup before cache save
415          if: always()
416          run: |
417            # Clean up build artifacts before cache save to reduce cache size
418            rm -rf target/debug/deps target/debug/build target/debug/incremental || true
419            # Run nix garbage collection to reduce store size
420            nix-collect-garbage -d || true
421            echo "Disk space before cache save:"
422            df -h /
423  
424    quint-model-checking:
425      name: Quint Model Checking
426      runs-on: ubuntu-latest
427      # Only run when Quint specs or consensus code changes
428      if: |
429        github.event_name == 'push' ||
430        contains(github.event.pull_request.labels.*.name, 'verification') ||
431        contains(join(github.event.pull_request.changed_files, ' '), 'verification/quint') ||
432        contains(join(github.event.pull_request.changed_files, ' '), 'crates/aura-protocol/src/consensus')
433      steps:
434        - uses: actions/checkout@v4
435        - name: Setup Node.js
436          uses: actions/setup-node@v4
437          with:
438            node-version: '20'
439        - name: Install Quint
440          run: npm install -g @informalsystems/quint@0.25.1
441        - name: Typecheck Quint specs
442          run: |
443            echo "Typechecking all Quint specifications..."
444            cd verification/quint
445            for spec in *.qnt; do
446              echo "  Checking $spec..."
447              quint typecheck "$spec" || exit 1
448            done
449            echo "[OK] All Quint specs typecheck"
450        - name: Run Quint invariant verification
451          run: |
452            echo "Running Quint model checking on consensus specs..."
453            cd verification/quint
454  
455            # Verify core consensus invariants
456            echo "  Verifying consensus/core.qnt..."
457            quint verify --invariant=AllInvariants consensus/core.qnt --max-samples=1000 || exit 1
458  
459            # Verify adversary model
460            echo "  Verifying consensus/adversary.qnt..."
461            quint verify --invariant=InvariantByzantineThreshold consensus/adversary.qnt --max-samples=500 || exit 1
462  
463            # Verify liveness properties
464            echo "  Verifying consensus/liveness.qnt..."
465            quint verify --invariant=InvariantProgressUnderSynchrony consensus/liveness.qnt --max-samples=500 || exit 1
466  
467            echo "[OK] All Quint invariants pass model checking"
468  
469    kani-verification:
470      name: Kani Bounded Model Checking
471      runs-on: ubuntu-latest
472      # Only run on push to main or when explicitly requested via label
473      # Kani takes significant time (~30+ minutes) so we don't run on every PR
474      if: |
475        github.event_name == 'push' && github.ref == 'refs/heads/main' ||
476        contains(github.event.pull_request.labels.*.name, 'kani')
477      steps:
478        - name: Free disk space
479          run: |
480            echo "Disk space before cleanup:"
481            df -h /
482            sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
483            sudo rm -rf /usr/local/share/boost /usr/share/swift
484            sudo rm -rf /opt/hostedtoolcache/Python /opt/hostedtoolcache/Ruby /opt/hostedtoolcache/go /opt/hostedtoolcache/node
485            sudo docker image prune --all --force || true
486            sudo apt-get clean || true
487            echo "Disk space after cleanup:"
488            df -h /
489        - uses: actions/checkout@v4
490        - name: Install Rust nightly
491          uses: actions-rust-lang/setup-rust-toolchain@v1
492          with:
493            toolchain: nightly
494            components: rust-src
495        - name: Install CBMC
496          run: |
497            sudo apt-get update
498            sudo apt-get install -y cbmc
499        - name: Cache Kani installation
500          uses: actions/cache@v3
501          with:
502            path: ~/.cargo/bin/cargo-kani
503            key: ${{ runner.os }}-kani-0.56.0
504        - name: Install Kani
505          run: |
506            if ! command -v cargo-kani &> /dev/null; then
507              echo "Installing Kani verifier..."
508              cargo install --locked kani-verifier
509              cargo kani setup
510            else
511              echo "Kani already installed"
512            fi
513        - name: Cache cargo registry
514          uses: actions/cache@v3
515          with:
516            path: ~/.cargo/registry
517            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
518        - name: Cache cargo build
519          uses: actions/cache@v3
520          with:
521            path: target
522            key: ${{ runner.os }}-cargo-build-kani-${{ hashFiles('**/Cargo.lock') }}
523        - name: Run Kani proofs
524          run: |
525            echo "Running Kani bounded model checking on consensus core..."
526            echo "This verifies:"
527            echo "  - Invariant preservation (apply_share, trigger_fallback, fail_consensus)"
528            echo "  - Monotonicity (proposals never shrink, equivocators never removed)"
529            echo "  - Panic freedom (no panics on valid inputs)"
530            echo "  - Phase transitions (terminal states stable)"
531            echo "  - Agreement (commit matches threshold result)"
532            echo "  - Reference equivalence (production matches reference)"
533            echo ""
534  
535            # Run each harness with a timeout
536            # Using --default-unwind to limit loop unwinding
537            cargo kani --package aura-protocol \
538              --default-unwind 10 \
539              --output-format terse \
540              2>&1 | tee kani-output.log
541  
542            echo ""
543            echo "========================================"
544            echo "KANI VERIFICATION COMPLETE"
545            echo "========================================"
546        - name: Upload Kani results
547          if: always()
548          uses: actions/upload-artifact@v3
549          with:
550            name: kani-verification-results
551            path: kani-output.log
552  
553    consensus-conformance:
554      name: Consensus Conformance Tests
555      runs-on: ubuntu-latest
556      needs: [test]
557      steps:
558        - uses: actions/checkout@v4
559        - name: Install Rust
560          uses: actions-rust-lang/setup-rust-toolchain@v1
561        - name: Setup Node.js
562          uses: actions/setup-node@v4
563          with:
564            node-version: '20'
565        - name: Install Quint
566          run: npm install -g @informalsystems/quint@0.25.1
567        - name: Cache cargo registry
568          uses: actions/cache@v3
569          with:
570            path: ~/.cargo/registry
571            key: ${{ runner.os }}-cargo-registry-${{ hashFiles('**/Cargo.lock') }}
572        - name: Cache cargo build
573          uses: actions/cache@v3
574          with:
575            path: target
576            key: ${{ runner.os }}-cargo-build-conformance-${{ hashFiles('**/Cargo.lock') }}
577        - name: Generate fresh ITF traces
578          run: |
579            echo "Generating ITF traces from Quint spec..."
580            # Generate traces to the dedicated traces directory
581            quint run --out-itf=traces/consensus.itf.json verification/quint/consensus/core.qnt --max-steps=30 --max-samples=5
582            echo "[OK] Generated fresh ITF traces to traces/"
583        - name: Run ITF conformance tests
584          run: |
585            echo "Running ITF conformance tests..."
586            cargo test -p aura-testkit --test consensus_itf_conformance -- --nocapture
587        - name: Run differential tests
588          run: |
589            echo "Running differential tests (production vs reference)..."
590            cargo test -p aura-testkit --test consensus_differential -- --nocapture
591        - name: Report conformance status
592          if: always()
593          run: |
594            echo "========================================"
595            echo "CONSENSUS CONFORMANCE REPORT"
596            echo "========================================"
597            echo "ITF Conformance: Tests verify Rust pure core matches Quint spec"
598            echo "Differential: Tests verify production matches reference model"
599            echo "========================================"