Emitted `multiplicative_generator` predicate is unsatisfiable for actual generators (`g ^ P = 1` forces `g = 1`)

[LucidSamuel]

The extraction emits, as part of every extracted circuit's isValid preamble (src/extraction.rs, lines 716–717 on current main):

def multiplicative_generator (P: ℕ) (mult_gen: ZMod P) : Prop :=
  mult_gen ^ P = 1

This predicate looks mathematically off, by Fermat's little theorem, g ^ P = g in ZMod P for prime P (Mathlib: ZMod.pow_card), so g ^ P = 1 holds iff g = 1 ergo an actual multiplicative generator of (ZMod P)ˣ can never satisfy it. The intended condition is presumably mult_gen ^ (P - 1) = 1, or (stronger, and closer to the name) orderOf mult_gen = P - 1.

Kernel-checked witness, from a project that consumes Halva's output (scribe, RangeCheck.multiplicative_generator_forces_one):

theorem multiplicative_generator_forces_one
    {P : ℕ} (hP : Nat.Prime P) (g : ZMod P) :
    multiplicative_generator P g ↔ g = 1 := by
  haveI : Fact (Nat.Prime P) := ⟨hP⟩
  unfold multiplicative_generator
  constructor
  · intro h
    exact (ZMod.pow_card g).symm.trans h
  · intro h
    rw [h, one_pow]

-- 2 generates (ZMod 5)ˣ yet fails the predicate (2^5 = 2 ≠ 1):
example : ¬ multiplicative_generator 5 2 := by
  unfold multiplicative_generator
  decide