Certora round 3: refresh drifted specs, conservation slices, CI gate

.github/workflows/certora.yaml

@@ -1,9 +1,19 @@
 name: Certora
 
-# Formal verification lane. Runs on demand, on a weekly schedule, and on PRs that touch
-# contracts or the Certora workspace. NOT a required PR gate yet (no branch protection):
-# it stays informational until prover runtimes and false-positive rates are understood
-# across the full matrix (see docs/testing/certora-followup.md "CI maturation").
+# Formal verification lane. Three jobs with different gating intent:
+#
+#   certora-check   — compile + CVL type-check every conf. No CERTORAKEY, no cloud,
+#                     deterministic and fast. This is the lane's REQUIRED-gate candidate:
+#                     it catches spec/contract signature drift (the failure that left
+#                     ClusterPayoutOracle.spec stale behind three contract commits).
+#   spec-freshness  — on PRs, fail if a contract with Certora coverage changed without
+#                     its spec being reviewed (bypass with [spec-ok] in the PR title/body).
+#   certora         — the full cloud prover matrix. Needs the CERTORAKEY secret and runs
+#                     for minutes-to-hours, so it stays NON-gating (informational) until
+#                     runtimes/false-positive rates are understood; promote the fast confs
+#                     (math, cluster-payout-oracle, loop-reputation, protocol-config,
+#                     mul-div-lemma) to required cloud runs once stable. See
+#                     docs/testing/certora-round3-plan.md (Track G).
 
 on:
   workflow_dispatch:
@@ -25,16 +35,97 @@ env:
   SOLC_VERSION: "0.8.35"
 
 jobs:
+  # ---------------------------------------------------------------------------
+  # Required-gate candidate: compile + CVL type-check, no secret, no cloud run.
+  # ---------------------------------------------------------------------------
+  certora-check:
+    runs-on: ubuntu-latest
+    name: certora-check (compile + typecheck)
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          submodules: true
+
+      - uses: ./.github/actions/setup-foundry
+
+      - name: Use preinstalled Java 21
+        # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs
+        # Java >= 19; the runner's default java is older. Point at the GitHub-hosted
+        # runner's preinstalled JDK 21 rather than apt-installing one that is not the
+        # default on PATH.
+        run: |
+          echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV"
+          echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH"
+      - name: Verify Java
+        run: java --version
+
+      - name: Install Certora CLI and solc
+        run: |
+          python3 -m pip install --upgrade pip
+          python3 -m pip install "certora-cli${CERTORA_CLI_VERSION}" solc-select
+          solc-select install "$SOLC_VERSION"
+          solc-select use "$SOLC_VERSION"
+          certoraRun --version
+          solc --version
+
+      - name: Compile + type-check every conf
+        working-directory: packages/foundry
+        run: |
+          set -uo pipefail
+          failed=()
+          for conf in certora/confs/*.conf; do
+            [ "$(basename "$conf")" = "base.conf" ] && continue
+            echo "::group::$conf"
+            if certoraRun "$conf" --compilation_steps_only; then
+              echo "OK: $conf"
+            else
+              echo "::error::compile/type-check failed: $conf"
+              failed+=("$conf")
+            fi
+            echo "::endgroup::"
+          done
+          if [ "${#failed[@]}" -ne 0 ]; then
+            echo "Type-check failed for: ${failed[*]}"
+            exit 1
+          fi
+          echo "All confs compiled and type-checked."
+
+  # ---------------------------------------------------------------------------
+  # PR guard: a covered contract may not change without its spec being reviewed.
+  # ---------------------------------------------------------------------------
+  spec-freshness:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'pull_request'
+    name: spec-freshness
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          fetch-depth: 0
+
+      - name: Check spec freshness vs. contract changes
+        env:
+          BASE_REF: ${{ github.base_ref }}
+          SPEC_FRESHNESS_OVERRIDE: "${{ github.event.pull_request.title }} ${{ github.event.pull_request.body }}"
+        run: |
+          git fetch --no-tags --depth=1 origin "$BASE_REF"
+          git diff --name-only "origin/${BASE_REF}...HEAD" \
+            | python3 packages/foundry/certora/scripts/check_spec_freshness.py --changed-stdin
+
+  # ---------------------------------------------------------------------------
+  # Full cloud prover matrix (non-gating; needs the CERTORAKEY secret).
+  # ---------------------------------------------------------------------------
   certora:
     runs-on: ubuntu-latest
     strategy:
       fail-fast: false
       matrix:
         conf:
           - certora/confs/math.conf
+          - certora/confs/mul-div-lemma.conf
           - certora/confs/cluster-payout-oracle.conf
           - certora/confs/round-voting-engine.conf
           - certora/confs/round-reward-distributor.conf
+          - certora/confs/round-reward-distributor-conservation.conf
           - certora/confs/no-double-claim.conf
           - certora/confs/round-voting-engine-lifecycle.conf
           - certora/confs/launch-distribution-pool.conf
@@ -45,8 +136,10 @@ jobs:
           - certora/confs/launch-distribution-pool-cap.conf
           - certora/confs/launch-distribution-pool-conservation.conf
           # NOTE: question-reward-escrow.conf and question-reward-escrow-claim.conf are
-          # intentionally excluded — both exceed certora-cli's 15-minute output window on
-          # this 1,490-line + 11-library contract. Run them manually with a larger budget.
+          # intentionally excluded from the proof matrix — both exceed certora-cli's
+          # 15-minute output window on this 1,490-line + 11-library contract. Run them
+          # manually with a larger budget. (They are still compile/type-checked by the
+          # certora-check job above.)
     name: ${{ matrix.conf }}
     steps:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
@@ -55,11 +148,16 @@ jobs:
 
       - uses: ./.github/actions/setup-foundry
 
-      - name: Install Java 21
+      - name: Use preinstalled Java 21
+        # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs
+        # Java >= 19; the runner's default java is older. Point at the GitHub-hosted
+        # runner's preinstalled JDK 21 rather than apt-installing one that is not the
+        # default on PATH.
         run: |
-          sudo apt-get update
-          sudo apt-get install -y --no-install-recommends openjdk-21-jre-headless
-          java --version
+          echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV"
+          echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH"
+      - name: Verify Java
+        run: java --version
 
       - name: Install Certora CLI and solc
         run: |

docs/testing/certora-escalation-internal-summary-via-ir.md

@@ -0,0 +1,80 @@
+# Certora escalation — internal-function summaries under solc_optimize + solc_via_ir
+
+This is a ready-to-file support/forum write-up for the one genuinely tooling-blocked item
+in the RateLoop Certora lane (Track A). It is parked here, not chased, because — as
+verified below — there is no working path in certora-cli 8.13.1, which is the latest
+release. File it upstream and re-test on each certora-cli bump.
+
+## Summary
+
+Several high-value properties (single-use refund on `RoundVotingEngine`, per-commit
+no-double-claim on `QuestionRewardPoolEscrow`) require summarizing an **internal**
+commit-resolution function deterministically. certora-cli 8.13.1 cannot apply
+internal-function summaries when the contract is compiled with `solc_optimize` +
+`solc_via_ir`, emitting:
+
+```
+Cannot apply summaries for internal functions ... when compiling using solc_optimize and solc_via_ir
+```
+
+and (relatedly, for the auto-finder):
+
+```
+Failed to generate auto finder for <fn> ...
+WARNING: Cannot apply summaries for internal functions with unnamed argument when compiling using solc_optimize and solc_via_ir
+```
+
+These contracts genuinely require `via_ir`: building them on the legacy pipeline fails with
+`Stack too deep. Try compiling with --via-ir`. So `via_ir` cannot be dropped, and the
+internal summary cannot be applied — there is no intersection.
+
+## Environment
+
+- certora-cli: 8.13.1 (latest as of 2026-05-19; confirmed on PyPI / Prover changelog)
+- solc: 0.8.35 + `via_ir`, optimizer runs = 100, evm = cancun
+- `yul_optimizer_steps` set to solc 0.8.34's step string (certora-cli does not natively map
+  0.8.35's via_ir Yul steps — a separate, minor gap)
+
+## Real-world repro cases in this repo
+
+Both are committed and reproduce the warning under `make certora-check`
+(`certoraRun <conf> --compilation_steps_only`):
+
+- `packages/foundry/certora/confs/round-voting-engine-lifecycle.conf` — the single-use
+  refund property routes through the engine's internal `_resolveClaimCommit`.
+- `packages/foundry/certora/confs/question-reward-escrow-claim.conf` — the per-commit
+  no-double-claim routes through `QuestionRewardPoolEscrow._resolveQuestionRewardClaim`
+  (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733), which is
+  internal — not an external call summarizable the way `NoDoubleClaim.spec` summarizes the
+  distributor→engine external `resolveClaimCommit`.
+
+## What was already tried (and did not work)
+
+Recorded from the round-2 empirical validation (docs/testing/certora-next-steps.md):
+
+| Attempt | Result |
+|---|---|
+| `function_finder_mode: relaxed` (valid key in 8.13.1) | internal summary still not applied |
+| `use_memory_safe_autofinders` conf key | rejected — not a valid key in 8.13.1 |
+| Drop via_ir (`solc_via_ir: false`) so internal summaries work | compile error: `Stack too deep. Try compiling with --via-ir` |
+| Re-expose the internal fn as external on a harness | does not intercept — the call inside the contract is to the internal function directly |
+
+## The ask
+
+Add support for applying CVL internal-function summaries (or a sound equivalent) when a
+contract is compiled with `solc_optimize` + `solc_via_ir`. Failing that, guidance on a
+supported pattern for deterministically modeling an internal resolver in a via_ir-required
+contract.
+
+## What we did instead (so the properties are not silently uncovered)
+
+- Proved the **resolution-independent state gates** the single-use properties build on:
+  refunds revert unless the round is terminal-but-not-settled; refunded pools reject
+  claims (`RoundVotingEngineLifecycle.spec`, `QuestionRewardPoolEscrow.spec`).
+- Proved the **cross-contract** no-double-claim where the resolver IS external
+  (`NoDoubleClaim.spec`).
+- The remaining single-use refund / per-commit no-double-claim are defense-in-depth on
+  flag-guarded paths already exercised by the Foundry test suite.
+
+Treat this as a tooling escalation, not an engineering task, until a certora-cli release
+maps internal summaries under via_ir.