use control instead of k #42
This file contains 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: CI | |
| on: [push] | |
| jobs: | |
| foundry-test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| submodules: recursive | |
| - uses: foundry-rs/foundry-toolchain@v1 | |
| with: | |
| version: nightly | |
| - name: Install forge-std | |
| run: | | |
| forge install foundry-rs/forge-std --no-commit | |
| forge remappings > remappings.txt | |
| - name: Run non-Kontrol tests | |
| run: | | |
| forge test --no-match-path "src/test/kontrol/*" -vvv | |
| - name: Run snapshot without Kontrol tests | |
| run: forge snapshot --no-match-path "src/test/kontrol/*" | |
| kontrol-verification: | |
| runs-on: ubuntu-latest | |
| needs: foundry-test | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| submodules: recursive | |
| - name: Setup Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.10' | |
| cache: 'pip' | |
| - name: Install Kontrol | |
| run: | | |
| python3 -m pip install --upgrade pip | |
| pip install kontrol | |
| - name: Install Foundry | |
| uses: foundry-rs/foundry-toolchain@v1 | |
| with: | |
| version: nightly | |
| - name: Build Contracts | |
| run: | | |
| forge build --build-info --force | |
| ls -la out/ | |
| - name: Run Kontrol Verification | |
| run: | | |
| # Create results directory | |
| mkdir -p verification-results | |
| # Run verification for each specification | |
| for spec in src/test/kontrol/*.k; do | |
| if [ -f "$spec" ]; then | |
| echo "Verifying $(basename "$spec")..." | |
| kontrol prove "$spec" \ | |
| --contract-dir ./src/contracts \ | |
| --output-dir ./verification-results \ | |
| --verbose || { | |
| echo "Verification failed for $spec" | |
| exit 1 | |
| } | |
| fi | |
| done | |
| echo "Verification completed successfully!" | |
| - name: Upload Verification Results | |
| if: always() | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: kontrol-verification-results | |
| path: verification-results/ | |
| retention-days: 5 |