From 9ed10ac64db95f2fe338b0a3c8a25663d896dbf0 Mon Sep 17 00:00:00 2001
From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com>
Date: Fri, 10 Jul 2026 02:52:26 +0400
Subject: [PATCH] Fix multiplicative_generator predicate: orderOf mult_gen = P
 - 1

The emitted predicate was mult_gen ^ P = 1, which is unsatisfiable for
actual generators: by Fermat's little theorem g ^ P = g in ZMod P for
prime P, so the predicate held only for mult_gen = 1. Since mult_gen
models halo2's Field::MULTIPLICATIVE_GENERATOR (a generator of the
multiplicative group, order P - 1), any circuit with a real generator
made Circuit.isValid unsatisfiable, and root_of_unity / delta lost
their intended meaning whenever isValid was used.

Emit orderOf mult_gen = P - 1 instead. orderOf resolves with the
imports the extraction already emits (verified against Mathlib via
Lean: the def compiles, and orderOf (2 : ZMod 5) = 4 = 5 - 1 is
kernel-checkable, so the new predicate is satisfiable by a real
generator where the old one was not).
---
 src/extraction.rs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/extraction.rs b/src/extraction.rs
index c4a1add..116fffd 100644
--- a/src/extraction.rs
+++ b/src/extraction.rs
@@ -713,8 +713,13 @@ pub fn print_preamble(namespace: &str, symbol_names: &[&str], cs: &ConstraintSys
     println!("  (2^S * T = P - 1) ∧");
     println!("  (∀ s' t': ℕ, 2^s' * t' = P - 1 → s' ≤ S)");
     
+    // `mult_gen` models halo2's Field::MULTIPLICATIVE_GENERATOR — a generator of
+    // the multiplicative group (ZMod P)ˣ, i.e. an element of order P - 1. The
+    // previous predicate `mult_gen ^ P = 1` was unsatisfiable for actual
+    // generators: by Fermat's little theorem g ^ P = g in ZMod P, so it forced
+    // mult_gen = 1 and made `isValid` unsatisfiable for real circuits.
     println!("def multiplicative_generator (P: ℕ) (mult_gen: ZMod P) : Prop :=");
-    println!("  mult_gen ^ P = 1");
+    println!("  orderOf mult_gen = P - 1");
     
     println!("structure Circuit (P: ℕ) (P_Prime: Nat.Prime P) where");
     println!("  Advice: ℕ → ℕ → ZMod P");