ci: introduce workflow for building proofs

Author: ligurio

.github/workflows/cflite_pr.yml

@@ -14,6 +14,7 @@ on:
     types: [opened, reopened, synchronize]
     paths-ignore:
       - 'cmake/BuildLua.cmake'
+      - 'proofs'
       - 'README.md'
       # Lua is not supported by OSS Fuzz,
       # https://github.com/google/oss-fuzz/issues/13782.

.github/workflows/oss-fuzz.yml

@@ -8,6 +8,7 @@ on:
     types: [opened, reopened, synchronize]
     paths:
       - '.github/workflows/oss-fuzz.yml'
+      - 'proofs'
       # Lua is not supported by OSS Fuzz,
       # https://github.com/google/oss-fuzz/issues/13782.
       - 'tests/capi/**'

.github/workflows/proofs.yaml

@@ -0,0 +1,52 @@
+name: Proofs
+
+on:
+  push:
+
+concurrency:
+  # Update of a developer branch cancels the previously scheduled workflow
+  # run for this branch. However, the 'main' branch and tag workflow runs
+  # are never canceled.
+  #
+  # We use a trick here: define the concurrency group as 'workflow run ID' +
+  # 'workflow run attempt' because it is a unique combination for any run.
+  # So it effectively discards grouping.
+  #
+  # Important: we cannot use `github.sha` as a unique identifier because
+  # pushing a tag may cancel a run that works on a branch push event.
+  group: ${{ (
+    github.ref == 'refs/heads/main' ||
+    startsWith(github.ref, 'refs/tags/')) &&
+    format('{0}-{1}', github.run_id, github.run_attempt) ||
+    format('{0}-{1}', github.workflow, github.ref) }}
+  cancel-in-progress: true
+
+jobs:
+  cbmc:
+    if: |
+      github.event_name == 'push' ||
+      github.event_name == 'pull_request' &&
+      github.event.pull_request.head.repo.full_name != github.repository
+    strategy:
+      matrix:
+        LUA:
+          - "lua"
+      fail-fast: false
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Setup common packages
+        run: |
+          sudo apt install -y cmake make cbmc
+
+      - name: Running CMake (PUC Rio Lua -current)
+        run: |
+          cmake -DCMAKE_C_COMPILER=goto-cc -DENABLE_CBMC_PROOFS=ON \
+                -DUSE_LUA=ON -DCMAKE_BUILD_TYPE=Debug \
+                -S . -B build
+        if: ${{ matrix.LUA == 'lua' }}
+
+      - name: Building
+        run: |
+          cmake --build build --parallel $(nproc) --target build_cbmc_proofs