Migrate the proofs to Rocq 9.2; keep the published Coq 8.20.1 version in coq-legacy/

.github/workflows/check.yml

@@ -5,9 +5,15 @@ on: [push, pull_request, workflow_dispatch]
 permissions:
   contents: read
 jobs:
-  coqchk:
+  rocqchk:
     runs-on: ubuntu-latest
     timeout-minutes: 240
     steps:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       - run: docker build --no-cache --progress=plain --build-arg JOBS=2 .
+  coqchk-legacy:
+    runs-on: ubuntu-latest
+    timeout-minutes: 240
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - run: docker build --no-cache --progress=plain --build-arg JOBS=2 -f Dockerfile.legacy .

Dockerfile

@@ -2,11 +2,11 @@
 # SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
 #
 # One command: docker build .   (with BuildKit, add --progress=plain to see every line of the check)
-# The build runs check.sh; the build fails if any check fails. The base is the public Coq 8.20.1 image,
-# pinned by digest so every rebuild uses the same checker.
-FROM coqorg/coq:8.20.1@sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674
-WORKDIR /home/coq/bigmult
-COPY --chown=coq:coq coq/ coq/
-COPY --chown=coq:coq check.sh ./
+# The build runs check.sh; the build fails if any check fails. The base is the public Rocq 9.2 image,
+# pinned by digest so every rebuild uses the same checker. The Coq 8.20.1 version is checked by Dockerfile.legacy.
+FROM rocq/rocq-prover:9.2@sha256:33926fb3757b2b560c3844157bd64173a26b6d338a256be1ae5eec8df2019025
+WORKDIR /home/rocq/bigmult
+COPY --chown=rocq:rocq coq/ coq/
+COPY --chown=rocq:rocq check.sh ./
 ARG JOBS=2
 RUN JOBS=${JOBS} ./check.sh

Dockerfile.legacy

@@ -0,0 +1,12 @@
+# SPDX-License-Identifier: Apache-2.0
+# SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
+#
+# One command: docker build .   (with BuildKit, add --progress=plain to see every line of the check)
+# The build runs check-legacy.sh; the build fails if any check fails. The base is the public Coq 8.20.1 image,
+# pinned by digest so every rebuild uses the same checker.
+FROM coqorg/coq:8.20.1@sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674
+WORKDIR /home/coq/bigmult
+COPY --chown=coq:coq coq-legacy/ coq-legacy/
+COPY --chown=coq:coq check-legacy.sh ./
+ARG JOBS=2
+RUN JOBS=${JOBS} ./check-legacy.sh

README.md

@@ -36,13 +36,32 @@ cd bigmult
 docker build .
 ```
 
-The build compiles every proof from source in the public Coq 8.20.1 image, pinned by digest in the Dockerfile,
-then re-checks the whole development, together with the parts of Coq's standard library it uses, with coqchk,
-Coq's independent kernel checker. It fails unless coqchk accepts everything and reports no axioms, and its last
+The build compiles every proof from source in the public Rocq 9.2 image, pinned by digest in the Dockerfile,
+then re-checks the whole development, together with the parts of Rocq's standard library it uses, with rocqchk,
+Rocq's independent kernel checker. It fails unless rocqchk accepts everything and reports no axioms, and its last
 step prints the theorem exactly as the kernel states it, with the two definitions it is stated with (reproduced
 below). With BuildKit, add `--progress=plain` to see every line. The same build runs on every push, from
 `.github/workflows/check.yml`. If you run it, you are welcome to add a line to [REPRODUCTIONS.md](REPRODUCTIONS.md).
 
+## Rocq 9.2 and the Coq legacy version
+
+The proofs now build with Rocq 9.2 (`coq/`, checked by `docker build .`). The published Coq 8.20.1 version is kept
+verbatim in `coq-legacy/`, with its own one-command check, which uses the same pinned Coq 8.20.1 image as before:
+
+```
+docker build -f Dockerfile.legacy .
+```
+
+The changes from `coq-legacy/` to `coq/` are imports only: `From Coq Require ...` became `From Stdlib Require ...`,
+and the two fully qualified paths `Coq.Arith.Arith` and `Coq.ZArith.Zpow_facts` (in `range_field_pasta.v`) became
+`Stdlib.Arith.Arith` and `Stdlib.ZArith.Zpow_facts`. No definition, lemma or theorem statement, and no proof, was
+changed.
+
+The statement block below was captured from the Coq 8.20.1 check. Rocq 9.2 prints the same statement, except that
+argument-scope annotations are written with an underscore (`%_function_scope`, `%_list_scope` instead of
+`%function_scope`, `%list_scope`): a change in the printer, not in the theorem. The check scripts differ only in the tool names (`rocq makefile`, `rocqchk`, `rocq c` in place of
+`coq_makefile`, `coqchk`, `coqc`).
+
 ## The theorem, as the kernel states it
 
 <!-- STATEMENT:BEGIN (filled from the check's own output; never edited by hand) -->
@@ -187,6 +206,7 @@ zero-knowledge proof for each execution. None of those is in this repository, an
 
 | file | what it holds |
 |---|---|
+| `coq-legacy/` | the Coq 8.20.1 version as published, same layout as `coq/`; checked by `check-legacy.sh` |
 | `coq/spec/bm_rule.v` | the rule: `PRE_bm`, `REL_bm`, `adequate`, and facts about it |
 | `coq/constraints/gen/bm_model_gen.v` | the circuit's constraint model: the field prime, the 930 polynomial constraints, the 8 copy constraints |
 | `coq/constraints/gen/bm_scaffold_gen.v` | cells, assignments, evaluation, and the acceptance predicate `sat` |

check-legacy.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: Apache-2.0
+# SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
+#
+# Rebuilds every proof from source, then re-checks the whole development with coqchk, Coq's independent
+# kernel checker, including the parts of Coq's standard library it uses. Exits non-zero unless every file
+# compiles, coqchk accepts everything, and coqchk reports no axioms and no disabled kernel check.
+set -euo pipefail
+cd "$(dirname "$0")/coq-legacy/constraints"
+JOBS="${JOBS:-2}"
+Q=(-Q . Constraints -Q gen Generated -Q ../spec "")
+
+echo "== 1/3 compile"
+coq_makefile -f _CoqProject -o CoqMakefile
+make -f CoqMakefile -j"$JOBS"
+
+echo "== 2/3 independent kernel re-check (coqchk)"
+if ! coqchk -o "${Q[@]}" Constraints.bm_adequacy > coqchk.log 2>&1; then
+  cat coqchk.log; echo "FAIL: coqchk rejected the development"; exit 1
+fi
+summary="$(sed -n '/CONTEXT SUMMARY/,$p' coqchk.log)"
+[ -n "$summary" ] || { cat coqchk.log; echo "FAIL: coqchk printed no context summary"; exit 1; }
+printf '%s\n' "$summary"
+for field in "Axioms" "Constants/Inductives relying on type-in-type" \
+             "Constants/Inductives relying on unsafe (co)fixpoints" "Inductives whose positivity is assumed"; do
+  grep -qF "* $field: <none>" <<<"$summary" || { echo "FAIL: coqchk does not report '$field: <none>'"; exit 1; }
+done
+
+echo "== 3/3 the theorem, as the kernel states it, and the two definitions it is stated with"
+tmp="$(mktemp -d)"
+printf '%s\n' 'Require Import Constraints.bm_adequacy.' 'Check policy_adequacy_bm.' \
+              'Print bm_rule.adequate.' 'Print accepts_bm.' \
+              'Print Assumptions policy_adequacy_bm.' > "$tmp/Statement.v"
+coqc "${Q[@]}" "$tmp/Statement.v"
+echo "OK: all checks passed"

check.sh

@@ -2,34 +2,34 @@
 # SPDX-License-Identifier: Apache-2.0
 # SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
 #
-# Rebuilds every proof from source, then re-checks the whole development with coqchk, Coq's independent
-# kernel checker, including the parts of Coq's standard library it uses. Exits non-zero unless every file
-# compiles, coqchk accepts everything, and coqchk reports no axioms and no disabled kernel check.
+# Rebuilds every proof from source, then re-checks the whole development with rocqchk, Rocq's independent
+# kernel checker, including the parts of Rocq's standard library it uses. Exits non-zero unless every file
+# compiles, rocqchk accepts everything, and rocqchk reports no axioms and no disabled kernel check.
 set -euo pipefail
 cd "$(dirname "$0")/coq/constraints"
 JOBS="${JOBS:-2}"
 Q=(-Q . Constraints -Q gen Generated -Q ../spec "")
 
 echo "== 1/3 compile"
-coq_makefile -f _CoqProject -o CoqMakefile
-make -f CoqMakefile -j"$JOBS"
+rocq makefile -f _CoqProject -o RocqMakefile
+make -f RocqMakefile -j"$JOBS"
 
-echo "== 2/3 independent kernel re-check (coqchk)"
-if ! coqchk -o "${Q[@]}" Constraints.bm_adequacy > coqchk.log 2>&1; then
-  cat coqchk.log; echo "FAIL: coqchk rejected the development"; exit 1
+echo "== 2/3 independent kernel re-check (rocqchk)"
+if ! rocqchk -o "${Q[@]}" Constraints.bm_adequacy > rocqchk.log 2>&1; then
+  cat rocqchk.log; echo "FAIL: rocqchk rejected the development"; exit 1
 fi
-summary="$(sed -n '/CONTEXT SUMMARY/,$p' coqchk.log)"
-[ -n "$summary" ] || { cat coqchk.log; echo "FAIL: coqchk printed no context summary"; exit 1; }
+summary="$(sed -n '/CONTEXT SUMMARY/,$p' rocqchk.log)"
+[ -n "$summary" ] || { cat rocqchk.log; echo "FAIL: rocqchk printed no context summary"; exit 1; }
 printf '%s\n' "$summary"
 for field in "Axioms" "Constants/Inductives relying on type-in-type" \
              "Constants/Inductives relying on unsafe (co)fixpoints" "Inductives whose positivity is assumed"; do
-  grep -qF "* $field: <none>" <<<"$summary" || { echo "FAIL: coqchk does not report '$field: <none>'"; exit 1; }
+  grep -qF "* $field: <none>" <<<"$summary" || { echo "FAIL: rocqchk does not report '$field: <none>'"; exit 1; }
 done
 
 echo "== 3/3 the theorem, as the kernel states it, and the two definitions it is stated with"
 tmp="$(mktemp -d)"
 printf '%s\n' 'Require Import Constraints.bm_adequacy.' 'Check policy_adequacy_bm.' \
               'Print bm_rule.adequate.' 'Print accepts_bm.' \
               'Print Assumptions policy_adequacy_bm.' > "$tmp/Statement.v"
-coqc "${Q[@]}" "$tmp/Statement.v"
+rocq c "${Q[@]}" "$tmp/Statement.v"
 echo "OK: all checks passed"

coq-legacy/constraints/_CoqProject

@@ -0,0 +1,20 @@
+# SPDX-License-Identifier: Apache-2.0
+# SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
+-Q . Constraints
+-Q gen Generated
+-Q ../spec ""
+
+gen/bm_model_gen.v
+gen/bm_wires_gen.v
+gen/bm_scaffold_gen.v
+pfcs.v
+range_field.v
+range_field_pasta.v
+field_order_lift.v
+bits_kit.v
+../spec/bm_rule.v
+gen/bm_necessity_gen.v
+bm_semantic.v
+bm_model_facts.v
+bm_soundness.v
+bm_adequacy.v

coq-legacy/constraints/bits_kit.v

@@ -0,0 +1,105 @@
+(* SPDX-License-Identifier: Apache-2.0
+   SPDX-FileCopyrightText: 2026 Next Ridge Solutions Ltd
+
+   Bit decompositions (bits_of) and their weighted sums, facts about small residues modulo a positive
+   number, a computed modular inverse (finv), and small list utilities.
+
+   Scope: these results bind the formal (Coq) layer only; the generated constraint model's fidelity to the circuit implementation, and the implementation itself, are outside them. *)
+
+From Coq Require Import ZArith Lia List Znumtheory Zpow_facts.
+Import ListNotations. Open Scope Z_scope.
+Require Import Constraints.field_order_lift.
+
+Definition bits_of (d:Z) (j:nat) : Z := Z.b2z (Z.testbit d (Z.of_nat j)).
+
+Lemma bits_of_bool : forall d i, bits_of d i = 0 \/ bits_of d i = 1.
+Proof. intros d i. unfold bits_of, Z.b2z. destruct (Z.testbit d (Z.of_nat i)); auto. Qed.
+
+Lemma wpow_pow2 : forall n, wpow n = 2 ^ (Z.of_nat n).
+Proof.
+  induction n as [|n IH].
+  - reflexivity.
+  - cbn [wpow]. rewrite IH. rewrite Nat2Z.inj_succ.
+    rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
+    reflexivity.
+Qed.
+
+Lemma bitsum_bits_of : forall n d, 0 <= d -> bitsum (bits_of d) n = d mod (wpow n).
+Proof.
+  induction n as [|n IH]; intros d Hd.
+  - cbn [bitsum wpow]. rewrite Z.mod_1_r. reflexivity.
+  - pose proof (wpow_pos n) as Hw.
+    cbn [bitsum]. rewrite (IH d Hd).
+    replace (wpow (S n)) with (wpow n * 2) by (cbn [wpow]; ring).
+    rewrite (Z.rem_mul_r d (wpow n) 2) by lia.
+    unfold bits_of.
+    rewrite (Z.testbit_spec' d (Z.of_nat n)) by apply Nat2Z.is_nonneg.
+    rewrite <- wpow_pow2.
+    ring.
+Qed.
+
+Lemma bitsum64_bits_of : forall d, 0 <= d < 2^64 -> bitsum (bits_of d) 64 = d.
+Proof.
+  intros d [Hlo Hhi].
+  assert (H64 : wpow 64 = 2 ^ 64) by (rewrite wpow_pow2; reflexivity).
+  rewrite (bitsum_bits_of 64 d Hlo), H64.
+  apply Z.mod_small. lia.
+Qed.
+
+Lemma mul_le_neg : forall P m, 0 < P -> m <= -1 -> m * P <= -P.
+Proof.
+  intros P m HP Hm.
+  replace (-P) with ((-1)*P) by ring. apply Z.mul_le_mono_nonneg_r; lia.
+Qed.
+
+Lemma mul_ge_pos : forall P m, 0 < P -> 1 <= m -> P <= m * P.
+Proof.
+  intros P m HP Hm.
+  replace P with (1*P) at 1 by ring. apply Z.mul_le_mono_nonneg_r; lia.
+Qed.
+
+Lemma no_wrap_zero : forall P z, 0 < P -> -P < z -> z < P -> z mod P = 0 -> z = 0.
+Proof.
+  intros P z HP Hlo Hhi Hm.
+  destruct (Zmod_divide z P (ltac:(lia)) Hm) as [k Hk].
+  destruct (Z.le_gt_cases k (-1)) as [Hk1|Hk1].
+  - pose proof (mul_le_neg P k HP Hk1). lia.
+  - destruct (Z.eq_dec k 0) as [Hk0|Hk0].
+    + subst k. rewrite Z.mul_0_l in Hk. exact Hk.
+    + pose proof (mul_ge_pos P k HP (ltac:(lia))). lia.
+Qed.
+
+Lemma small_nonzero_residue : forall P z, 0 < P -> -P < z -> z < P -> z <> 0 -> z mod P <> 0.
+Proof.
+  intros P z HP Hlo Hhi Hnz Hm. apply Hnz. exact (no_wrap_zero P z HP Hlo Hhi Hm).
+Qed.
+
+Definition finv (P m : Z) : Z := Zpow_mod (m mod P) (P - 2) P.
+
+Definition drop_nth {A:Type} (n:nat) (l:list A) : list A :=
+  firstn n l ++ skipn (S n) l.
+
+Lemma drop_nth_length : forall (A:Type) (n:nat) (l:list A),
+  (n < length l)%nat -> length (drop_nth n l) = (length l - 1)%nat.
+Proof.
+  intros A n l Hn. unfold drop_nth.
+  rewrite app_length. rewrite firstn_length_le by lia. rewrite skipn_length. lia.
+Qed.
+
+Lemma drop_nth_incl : forall (A:Type) (n:nat) (l:list A) (x:A),
+  In x (drop_nth n l) -> In x l.
+Proof.
+  intros A n l x Hin. unfold drop_nth in Hin.
+  apply in_app_or in Hin. destruct Hin as [H|H].
+  - rewrite <- (firstn_skipn n l). apply in_or_app. left. exact H.
+  - rewrite <- (firstn_skipn (S n) l). apply in_or_app. right. exact H.
+Qed.
+
+Print Assumptions bits_of_bool.
+Print Assumptions wpow_pow2.
+Print Assumptions bitsum_bits_of.
+Print Assumptions bitsum64_bits_of.
+Print Assumptions no_wrap_zero.
+Print Assumptions small_nonzero_residue.
+Print Assumptions drop_nth_length.
+Print Assumptions drop_nth_incl.