Add CI: lake build + field-file generator-reproduction checks

.github/workflows/ci.yml

@@ -0,0 +1,43 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    name: Build (lake)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      # Installs the toolchain from `lean-toolchain`, fetches the Mathlib cache,
+      # and runs `lake build` — which also runs the in-file `native_decide` sanity checks.
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+
+  generators:
+    name: Field-file generators reproduce
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      - name: Install PARI/GP
+        run: sudo apt-get update && sudo apt-get install -y --no-install-recommends pari-gp
+      # System python3 (preinstalled on ubuntu-latest) suffices; the generators are stdlib-only
+      # and shell out to `gp` for the factorizations.
+      - name: Regenerate the field files
+        run: |
+          python3 scripts/gen_pasta.py > CompElliptic/Fields/Pasta.lean
+          python3 scripts/gen_jubjub.py > CompElliptic/Fields/Jubjub.lean
+      - name: Fail if the regenerated files differ from the committed ones
+        run: git diff --exit-code CompElliptic/Fields/Pasta.lean CompElliptic/Fields/Jubjub.lean

.github/workflows/zizmor.yml

@@ -0,0 +1,39 @@
+name: Workflow audit
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - '.github/workflows/**'
+      - '.github/actions/**'
+  pull_request:
+    paths:
+      - '.github/workflows/**'
+      - '.github/actions/**'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  zizmor:
+    name: zizmor
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      - uses: zizmorcore/zizmor-action@5f14fd08f7cf1cb1609c1e344975f152c7ee938d # v0.5.6
+        with:
+          advanced-security: false
+          annotations: true
+          # Catch all findings, including `informational`. Known-safe
+          # patterns must be silenced via line-level
+          # `# zizmor: ignore[<rule>]` comments at the site, not by
+          # raising the threshold globally — otherwise a new template
+          # injection or unpinned use slips in silently with future
+          # workflow edits.
+          min-severity: informational

TODO.md

@@ -193,10 +193,17 @@ types + transport) has been consolidated into these and removed.
 
 ## Tooling and conventions
 
-- [ ] Add CI for CompElliptic (none exists yet): build the Lean library, and check that the
-  field-file generators reproduce their committed outputs unchanged — run `scripts/gen_pasta.py` /
-  `scripts/gen_jubjub.py` and `git diff --exit-code` the regenerated `Fields/*.lean`, so a hand-edit
-  can no longer silently drift from its generator (as `Fields/Pasta.lean` had).
+- [x] CI (`.github/workflows/ci.yml`): two independent jobs/checks. **Build (lake)** — `lean-action`
+  installs the toolchain, fetches the Mathlib cache, and runs `lake build` (which also runs the
+  in-file `native_decide` sanity checks). **Field-file generators reproduce** — installs PARI/GP,
+  re-runs `scripts/gen_pasta.py` / `scripts/gen_jubjub.py` over their committed outputs and
+  `git diff --exit-code`s `Fields/Pasta.lean` / `Fields/Jubjub.lean`, so a hand-edit can no longer
+  silently drift from its generator (as `Fields/Pasta.lean` had). They are separate checks so branch
+  protection can require the build but leave the (PARI/GP-dependent) generator check advisory —
+  configure that in the repo's branch-protection settings. All actions are SHA-pinned (with
+  `# vX.Y.Z` comments) and checkouts use `persist-credentials: false`; a separate `zizmor.yml`
+  (`zizmorcore/zizmor-action`, `min-severity: informational`) audits the workflows for unpinned uses,
+  credential persistence, template injection, and other GitHub-Actions issues — matching `zcash/ironwood`.
 - [ ] Script (under `scripts/`) to check, and update in place, the copyright/licence header on
   every source file (`*.lean`, `*.py`): verify each file starts with the canonical dual-licence
   header (Apache 2.0 or MIT, `LICENSE-APACHE` / `LICENSE-MIT`, `Authors:` line) in the right comment