CI: build with warnings as errors, axiom audit, zizmor; style rules

.github/dependabot.yml

@@ -0,0 +1,11 @@
+version: 2
+updates:
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly
+    cooldown:
+      default-days: 7
+    groups:
+      github-actions:
+        patterns: ["*"]

.github/workflows/ci.yml

@@ -0,0 +1,40 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+permissions: {}
+
+concurrency:
+  group: ci-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: Build and audit
+    runs-on: ubuntu-latest
+    timeout-minutes: 180
+    permissions:
+      contents: read
+    steps:
+      - name: Check out the repository
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Check the sources
+        run: scripts/check-sources.sh
+
+      - name: Build, failing on any warning
+        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1
+        with:
+          auto-config: "false"
+          build: "true"
+          build-args: "--wfail"
+          use-mathlib-cache: "true"
+
+      - name: Audit the axioms of the endpoints
+        run: scripts/check-axioms.sh

.github/workflows/zizmor.yml

@@ -0,0 +1,30 @@
+name: Workflow security
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+permissions: {}
+
+concurrency:
+  group: zizmor-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  zizmor:
+    name: zizmor
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    permissions: {}
+    steps:
+      - name: Check out the repository
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Audit the workflows
+        uses: zizmorcore/zizmor-action@cc914d7f3750a2d13d75c7f184a1060aa0e9d482 # v0.6.4
+        with:
+          advanced-security: "false"
+          version: "1.30.1"

AGENTS.md

@@ -233,6 +233,17 @@ globally; use `letI` or a wrapper carrier.
 - Keep executable cryptographic code and security proofs in separate layers;
   do not unfold a complete cipher or hash implementation in a security theorem.
 
+## Style
+
+- Follow Mathlib's [style guide](https://leanprover-community.github.io/contribute/style.html)
+  and [naming conventions](https://leanprover-community.github.io/contribute/naming.html),
+  except where this file says otherwise: no copyright headers, the sources' terminology for
+  public names, the documentation policy below.
+- Lines have at most 100 characters.
+- New and changed code passes Mathlib's standard linter set:
+  `lake env lean -Dweak.linter.mathlibStandardSet=true <file>` reports nothing. The set is not
+  yet enabled in the lakefile, because older code does not pass it.
+
 ## Naming and ownership
 
 - Do not mark a declaration `private` unless that exact exception was approved.
@@ -275,16 +286,19 @@ its library root.
 ## Verification
 
 ```bash
-lake build
-rg -n '\bsorry\b|\badmit\b|^\s*axiom\b' src
-rg -n 'maxHeartbeats|maxRecDepth|native_decide|bv_decide|decide \+native' src
+scripts/check-sources.sh
+lake build --wfail
+scripts/check-axioms.sh
 git diff --check
 ```
 
-The audit files `src/Tests/Axioms/Systems.lean`, `src/Tests/Axioms/CC.lean`,
-`src/Tests/Axioms/Commons.lean`, `src/Tests/DSL/Axioms.lean`,
-`src/Tests/Substitution/Axioms.lean` and `src/Tests/AuthenticatedEncryption.lean` print the
-axioms of the important endpoints (`lake env lean <file>`). The accepted envelope is `propext`,
-`Classical.choice` and `Quot.sound`; any other axiom, including `sorryAx`, is a
-failure. For changes to public declarations used downstream, also build
-`chachapoly-cc`.
+`scripts/check-sources.sh` rejects axiom declarations, native evaluation (`native_decide`,
+`bv_decide`), `implemented_by`/`extern` bindings and heartbeat or recursion-depth overrides.
+`lake build --wfail` fails on any warning, including `declaration uses 'sorry'`.
+`scripts/check-axioms.sh` runs every file under `src/Tests` that prints axioms
+(`#print axioms`) and checks the envelope: `propext`, `Classical.choice` and `Quot.sound`;
+any other axiom, including `sorryAx`, is a failure. CI (`.github/workflows/ci.yml`) runs these
+three on every pull request and on `main`, and `.github/workflows/zizmor.yml` audits the
+workflows with zizmor. Actions are pinned to commit hashes, which Dependabot updates.
+
+For changes to public declarations used downstream, also build `chachapoly-cc`.

scripts/check-axioms.sh

@@ -0,0 +1,44 @@
+#!/usr/bin/env bash
+# Runs every file under `src/Tests` that prints axioms and fails if an audited endpoint depends
+# on an axiom other than `propext`, `Classical.choice` and `Quot.sound` (`sorryAx` included).
+# Expects the library to be built (`lake build`).
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+allowed='^(propext|Classical\.choice|Quot\.sound)$'
+status=0
+total=0
+
+files=()
+while IFS= read -r file; do
+  files+=("$file")
+done < <(grep -rl '#print axioms' src/Tests | sort)
+if [[ ${#files[@]} -eq 0 ]]; then
+  echo "error: no axiom audits found under src/Tests"
+  exit 1
+fi
+
+for file in "${files[@]}"; do
+  if ! output=$(lake env lean "$file" 2>&1); then
+    echo "$output"
+    echo "error: $file does not compile"
+    status=1
+    continue
+  fi
+  # A message may wrap over several lines; join them before matching.
+  joined=$(tr '\n' ' ' <<<"$output")
+  audited=$(grep -oE "depends on axioms|does not depend on any axioms" <<<"$joined" \
+    | wc -l | tr -d ' ' || true)
+  total=$((total + audited))
+  outside=$(grep -oE "depends on axioms: \[[^]]*\]" <<<"$joined" \
+    | sed -E 's/.*\[//; s/\]$//' | tr ',' '\n' | tr -d ' ' | grep -vE "$allowed" | sort -u || true)
+  if [[ -n $outside ]]; then
+    echo "error: $file: axioms outside the envelope: $(tr '\n' ' ' <<<"$outside")"
+    status=1
+  fi
+  echo "$file: $audited endpoints"
+done
+
+echo "axioms: $total endpoints in ${#files[@]} files"
+exit $status

scripts/check-sources.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# Fails if the sources declare an axiom, evaluate natively, bind compiled code, or raise a
+# resource limit. `sorry` and `admit` are caught by `lake build --wfail`.
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+status=0
+
+check() {
+  local what=$1 pattern=$2
+  local hits
+  hits=$(grep -rnE "$pattern" src || true)
+  if [[ -n $hits ]]; then
+    echo "$hits"
+    echo "error: $what"
+    status=1
+  fi
+}
+
+check "axiom declarations" '^[[:space:]]*((private|protected)[[:space:]]+)?axiom[[:space:]]'
+check "native evaluation" 'native_decide|bv_decide|decide \+native|Lean\.ofReduceBool'
+check "compiled code bindings" '@\[(implemented_by|extern)'
+check "resource limits" 'maxHeartbeats|maxRecDepth|synthInstance\.maxSize'
+
+if [[ $status -eq 0 ]]; then
+  echo "sources: no axiom declarations, native evaluation, code bindings or limit overrides"
+fi
+exit $status