Research proof index

Let $G$ be a finite vector space over $\mathbb F_q$, where $q\ge3$ is prime. If a nonempty set $A\subseteq G$ contains no nontrivial three-term arithmetic progression, then $\dim_{\mathbb F_q}G \le 2^{148}\,\mathcal L(\alpha)^9$, where $\alpha=|A|/|G|$ and $\mathcal L$ is the project's capped logarithm.

CMA-to-NMA reduction for Fiat-Shamir signatures built from a Sigma protocol. The reduction runs the CMA adversary with simulated signing transcripts and a managed random oracle, then appends a single explicit live random-oracle query for the forgery's hash point so that the verification challenge is part of the forkable transcript (the `nmaAdvFromCmaWithF...

Running the inner unifForward + roImpl simulator against a source computation with an nmaHashQueryBound Q can grow the internal queryLog by at most Q. Each source Sum.inr step consumes one unit of the nmaHashQueryBound budget, while roImpl appends to queryLog only on a cache miss, hence at most once per such step.

If two successful contextual forks select the same fork index, their forgery targets agree.

NMA-to-extraction via the forking lemma and special soundness. The parameter qH is the fork slot parameter passed to Fork.forkPoint qH, i.e., the number of Fin (qH + 1) candidate target positions over which the replay-forking lemma sums. It is not required to be a valid query bound on the adversary: callers may supply a wrapped adversary with up...

Completeness of the Fiat-Shamir signature scheme follows from completeness of the underlying Σ-protocol.