4.2. Certificates and subject binding🔗

Hex.ECPP.Cert has a terminal certificate constructor and an elliptic step. A step records the modulus, curve coefficients, a finite point, a discriminant inverse and an inverse transcript. Its scalar is always its child's subject. There is no separately claimed curve order or scalar in the raw certificate.

open Hex.ECPP
namespace HexECPPChapter

def smallCertificate : Cert := .base (.small 17)
#guard checkAt 17 smallCertificate
#guard !checkAt 19 smallCertificate

def curveCertificate : Cert :=
  .step 17 2 3 3 6 6 [10, 13, 3, 13]
    (.base (.small 11))
#guard checkAt 17 curveCertificate

def

Hex.ECPP.check : Hex.ECPP.Cert → Bool
Hex.ECPP.check : Hex.ECPP.Cert → Bool

A checked terminal Hex certificate or a checked ECPP step.

def

Hex.ECPP.checkAt (n : Nat) (cert : Hex.ECPP.Cert) : Bool
Hex.ECPP.checkAt (n : Nat)
  (cert : Hex.ECPP.Cert) : Bool

Bind acceptance to a caller supplied subject.

theorem

Hex.ECPP.checkAt_eq_true_iff {n : Nat} {cert : Hex.ECPP.Cert} :
  Hex.ECPP.checkAt n cert = true ↔
    cert.subject = n ∧ Hex.ECPP.check cert = true
Hex.ECPP.checkAt_eq_true_iff {n : Nat}
  {cert : Hex.ECPP.Cert} :
  Hex.ECPP.checkAt n cert = true ↔
    cert.subject = n ∧
      Hex.ECPP.check cert = true

Characterize subject-bound acceptance without unfolding the checker.

The checker rejects noncanonical residues, nonunit division witnesses, unconsumed inverses and both equality boundaries of the strict ECPP size bound. It derives the binary schedule from the child subject, performs checked affine additions and requires the final point to be infinity.

theorem

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

Scalar acceptance means infinity with no unused inverse witnesses.

theorem

Hex.ECPP.sizeBound_eq_true_iff {n q : Nat} :
  Hex.ECPP.sizeBound n q = true ↔
    n < (q - 1) * (q - 1) ∧ 16 * n * q < ((q - 1) * (q - 1) - n) ^ 2
Hex.ECPP.sizeBound_eq_true_iff
  {n q : Nat} :
  Hex.ECPP.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.