def Hex.ECPP.replayBits (n a b q : Nat) (Q : Point) (bits : Nat) : Point → List Nat → Option (Point × List Nat)

Replay the remaining bits of q, from high index to low index.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ECPP.replayBits n a b q Q 0 x✝¹ x✝ = some (x✝¹, x✝)

def Hex.ECPP.replay (n a b q : Nat) (Q : Point) (inverses : List Nat) : Option (Point × List Nat)

Calculate q • Q by binary doubling and addition modulo n, verifying the supplied inverse for every division. Return the resulting point and any unused inverses, or none if a required arithmetic check fails.

Equations

• Hex.ECPP.replay n a b q Q inverses = Hex.ECPP.replayBits n a b q Q (HexArith.bitLength q) Hex.ECPP.Point.infinity inverses

def Hex.ECPP.replayDone (n a b q : Nat) (Q : Point) (inverses : List Nat) : Bool

Verify q • Q = O modulo n, with every supplied inverse used exactly once. The certificate for q and the curve's nonsingularity are checked separately by check.

Equations

• Hex.ECPP.replayDone n a b q Q inverses = match Hex.ECPP.replay n a b q Q inverses with | some (Hex.ECPP.Point.infinity, []) => true | x => false

theorem Hex.ECPP.replayBits_facts {n a b q : Nat} (Q : Point) (bits : Nat) (R S : Point) (ws rest : List Nat) : Point.canonical n R = true → Point.onCurve n a b R = true → replayBits n a b q Q bits R ws = some (S, rest) → Point.canonical n S = true ∧ Point.onCurve n a b S = true

Every point returned by an accepted replay prefix is a canonical point on the supplied curve. The induction follows the actual bit schedule.

theorem Hex.ECPP.replay_facts {n a b q : Nat} {Q S : Point} {ws rest : List Nat} (h : replay n a b q Q ws = some (S, rest)) : Point.canonical n S = true ∧ Point.onCurve n a b S = true

A successful scalar replay returns canonical coordinates satisfying the curve equation.

theorem Hex.ECPP.replayDone_eq_true_iff {n a b q : Nat} {Q : Point} {inverses : List Nat} : replayDone n a b q Q inverses = true ↔ replay n a b q Q inverses = some (Point.infinity, [])

Scalar acceptance means infinity with no unused inverse witnesses.

theorem Hex.ECPP.bit_mod_succ (q k : Nat) : q % 2 ^ (k + 1) = q % 2 ^ k + (q.testBit k).toNat * 2 ^ k

The next binary digit extends the truncated scalar by its positional value.

def Hex.ECPP.sizeBound (n q : Nat) : Bool

Check the auxiliary prime size needed for the Hasse-bound argument. For q ≥ 2, this is the exact integer form of q > (n^(1/4) + 1)²: require n < (q - 1)² and 16*n*q < ((q - 1)² - n)². Strict inequalities are necessary to exclude a prime divisor of n at most √n.

Equations

• Hex.ECPP.sizeBound n q = if n < (q - 1) * (q - 1) then have c := (q - 1) * (q - 1) - n; decide (16 * n * q < c * c) else false

theorem Hex.ECPP.sizeBound_first {n q : Nat} (h : sizeBound n q = true) : n < (q - 1) * (q - 1)

Acceptance implies positivity of the difference before natural subtraction.

theorem Hex.ECPP.sizeBound_second {n q : Nat} (h : sizeBound n q = true) : 16 * n * q < ((q - 1) * (q - 1) - n) * ((q - 1) * (q - 1) - n)

Acceptance implies the second strict integer ECPP inequality.

theorem Hex.ECPP.sizeBound_eq_true_iff {n q : Nat} : sizeBound n q = true ↔ n < (q - 1) * (q - 1) ∧ 16 * n * q < ((q - 1) * (q - 1) - n) ^ 2

Both strict inequalities, including the guard before subtraction, exactly characterize arithmetic size acceptance.