Group-hash indifferentiability: security games, rejection-sampling simulator, and concrete endpoints by daira · Pull Request #199 · zcash/ironwood

daira · 2026-08-15T15:26:37Z

The ironwood side of the indifferentiability arc (#198): the one-oracle game, the collapse of the full two-oracle game onto it, the rejection-sampling simulator, and concrete endpoints at the deployed mappings. The counting side is daira/CompElliptic#27, and the Weil-bound reduction above it is daira/CompElliptic#29, both merged; the pin references CompElliptic main at the #29 merge.

The headline. pallas_/vesta_indiffFromRO (Indiff.lean): every q-query adaptive distinguisher between the real per-query law and the ideal one is moved by at most q/2^120, in both directions and against every acceptance event. The only inputs are the two CharSumBounded bounds at 100·#F — Weil's theorem at the branch covers. The parametric forms keep the _of_weilBounded suffix.

The route (each module's doc has the detail):

Sampler.lean — the single-query core: the one-squeeze bias in both worlds is bounded by the regularity distance.
Pasta.lean — the deployed instantiation under the named WeilBounded hypothesis, with the zero-repair transport at (4·#F − 2)/(#F)², and the simulator's counting input deployedFibreBound = 11.
MultiOracleComp.lean / TwoOracle.lean — indexed query trees with per-index budgets; the two-oracle game collapses computably onto the one-oracle core at the folded budget.
Model.lean — the PMFEventBiasLE combinators the arc composes with.
Simulator.lean — the capped rejection sampler behind the ideal law, with exact costs: round-count tail (1 − p)^k, geometric round law, two-sided output bias (1 − p)^K, exactness on empty fibres, and convergence to the fibre sampler as K → ∞.
Indiff.lean — the compositions: indiffFromRO_of_regularity (a regularity-distance budget of β gives indifferentiability at q·β), the capped variant charging simLawBias per query, and the concrete endpoints (β := 1/2^120 − 4/#F makes the transport term telescope; the rest is exact arithmetic at the deployed sizes).

The book page teaches the argument to a general mathematical audience and states the what-is-proved/what-is-modelled boundary; its Conclusion gives the advantage as the single term q/2^120.

Census: the arc's top-level leaves are pinned, with their native_decide owners named — the Pasta base-field structures, and the curve-group order certificates at the concrete endpoints and the simulator pins; the census module doc's CompElliptic owner tally ends at six.

What stays cited: Weil's theorem at the two branch covers — stating it needs function-field vocabulary tracked at daira/CompElliptic#30. The consuming games' oracle access is #188.

The first commit adopts CompElliptic's absorbed CompEllipticExtras (daira/CompElliptic#12) in place of ironwood's copies.

🤖 Claude Fable 5, Claude Opus 4.8 (1M context)

daira

Self-ACK, only minor nits.

daira

Self-reACK

dannywillems

Mostly comments. First batch. Include daira/CompElliptic#31

Update the two passages that described the constant as calculated-only: the calculation is now proven on paper —modulo results cited as established mathematics— in CompElliptic's design/weil-constant-derivation.md. What CompElliptic#28 tracks is formalizing the calculation in Lean; Weil's theorem itself stays a cited input, since formalizing it would require machinery not present in Mathlib. This replaces the vaguer "remaining steps to a fully rigorous account" wording, which could be misread as including a formalization of Weil's theorem. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The regularity section now shows where the number comes from: the formal budget condition ε² ≥ (#G − 1)·C⁴/(#F)² accepts any ε just above C²·√#G/#F, and at the deployed sizes that is about 2^6.8 · 2^127 / 2^254 ≈ 2^{-120}. The Conclusion's mention now points back to that arithmetic. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The pin moves from the head of indiff-counting (CompElliptic PR zcash#27) to the head of weil-covers (PR zcash#29, stacked on zcash#27): the reduction of the deployed Weil bound to Weil's theorem at the two branch covers, with the per-curve endpoints taking only the CharSumBounded inputs. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

pallas/vesta_indiffFromRO now denote the concrete endpoints: from Weil's theorem at the two branch covers alone —the CharSumBounded inputs of CompElliptic's Hashing/WeilInstance.lean— q queries distinguish the group hash from a random oracle with advantage at most q/2^120. The former parametric statements keep doing the modular work under the names pallas/vesta_indiffFromRO_of_weilBounded, which say what they consume; the plain names belong to what consumers should cite. The census pins keep their text and now pin the concrete endpoints. The parametric endpoints conclude with advantage q·(ε + 4/#F). We instantiate ε := 1/2^120 - 4/#F, so that ε + 4/#F telescopes to exactly 1/2^120: the subtraction pre-pays the zero-repair transport inside the budget, and no slack is lost at that step. Two side conditions remain, both checked by norm_num as exact rational arithmetic on the card numerals (~508 bits after squaring): * ε ≥ 0 — the transport 4/#F ≈ 2^{-252} is far below 2^{-120}; * the budget check (#G - 1)·(21/2)⁴/#F² ≤ ε² — the regularity distance is about 2^{-120.2}, a headroom factor of about 1.16. The proofs avoid pin-sensitive lemma names: the Nat.card bridges go through simp's default set, and the endpoint conclusion is applied in fully-introduced form. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Update the four passages that described the Weil constant as proven-on-paper only: * the Calculating-the-Weil-constant section now records that the calculation is formalized down to Weil's theorem at the two branch covers, which stays the cited input (its statement needs genus, places, and covers vocabulary that Mathlib does not yet have); * the trust-boundary bullet names the CharSumBounded inputs as the unformalized boundary; * the Conclusion states the concrete advantage q/2^120 at the renamed endpoints, with the budget arithmetic; * the remaining-work bullet tracks the vocabulary boundary rather than the whole formalization. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Bump the CompElliptic pin to main at the merge of PR zcash#29 (2c04440), the reduction of the deployed Weil bound to Weil's theorem at the branch covers. Above the previously pinned commit, this adds: * WeilSupport.lean — the squarefreeness lemma's inputs, the Eisenstein patterns, and the monodromy square exclusions; * the CharacterSum realness lemmas; * the design doc's woven references, with their CI checks (the reference checker and the sage identities); * the review round's docstring, module-doc, script-naming, and margin corrections; * the full FFSTV citation at its first use; * census pins for every declaration the design doc cites, with the reference checker's matching third direction; * the checker's path-suffix citation resolution — restricted to the relevant modules, with ambiguous citations required to qualify themselves and every potential referent required to be pinned. Nothing this development consumes changed; ironwood's census is unaffected. The book page catches up: the calculation passage notes that the paper proof's checkable inputs are machine-checked and cited at their points of use, and the closing bullet no longer says the supporting facts remain — that scope of CompElliptic#28 is delivered, with the function-field vocabulary still tracked at CompElliptic#30. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The branch maps were called g and h, but g is RFC 9380's name for the curve equation's right-hand side (y² = g(x) = x³ + A·x + B, §6.6.2), which the scaling-defect display also uses. The RFC has no name for the branch functions; its x1 and x2 are the two candidate abscissae, not the values of these point-valued maps. As the two branches of the mapping f they are now f₁ and f₂ — distinct from the design doc's abscissa functions x₁, x₂, which keep their names. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

It was called ε, colliding with the conventional total in "(q, ε)-indifferentiable"; the composition line now reads q·β. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

A reader landing on the f₁/f₂ cases directly can miss that u is transformed before it becomes an x-coordinate. Point at CompElliptic's Hashing/SimplifiedSWU.lean, which defines the mapping step by step with the spec's own intermediate names. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

"Exact computation on small curves" now points at CompElliptic's scripts/sswu-small-curve-stats.sage, the committed form of that computation. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

\cdot served both as multiplication and as the argument-placeholder dot. Separating them was necessary to fix the multiplication sense's spacing, which was too tight in scriptstyle contexts; macros.txt now defines \mul (a multiplication dot with consistent spacing) and \argument (the placeholder), and the group-hash page uses them by role. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Pull the budget paragraph out of the regularity discussion so it no longer interleaves with the DFT aside, and let the Weil-constant section own it: the named hypothesis and its constant C come first, then the budget β that `sum_abs_prob_dev_le` (now the linked formalization pointer) derives from C — stated as what it is, a bound on the previous section's regularity distance. The mapping's character sum is written plain S, with subscripts reserved for the covering sums S_{C_j}, which are defined at first use. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The budget paragraph linked the formalization but did not say where (#G − 1)·C⁴/(#F)² comes from. It is the DFT aside's pipeline with the constants tracked: (C²·#F)² per nontrivial frequency, Parseval's 1/#G, Cauchy–Schwarz's #G cancelling it, and the probability normalization's (#F)⁴. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The section used C = 21/2 without saying why: the hypothesis wants |S(χ)| ≤ C·√#F, and the extra half over the 10 absorbs the calculated bound's trailing +1 — in square-root-free form, (10√#F + 1)² ≤ (21/2)²·#F, with margin about 2^{126} at the deployed sizes. The deployed-sizes sentence points forward to it. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The bare `Hashing/*.lean` mentions — TwoTermUniformity and PastaSSWU at the top, BranchCovers, WeilInstance, and WeilSupport in the Weil-constant section and the Conclusion — now link to their files, matching the page's other CompElliptic links. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

"Out of scope for CompElliptic#28" describes a scope boundary of an issue that closes just before this page lands. Keep only the live tracker: the vocabulary is CompElliptic#30. The Conclusion's "the delivered scope of zcash#28" already reads historically and stays. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

One sentence carried the paper proof, the formalization boundary, the per-cover inputs with their defining aside, and the machine-checked claim. Four sentences now carry one each. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The book's β rename left the code using ε in two roles. The regularity-specific budgets in Sampler.lean, Pasta.lean, and Indiff.lean become β, matching the book. The generic interfaces (PMFEventBiasLE, PMFWeightedBiasLE, and the multi-oracle composition) become ρ rather than ε: ε carries a "this probability is small" implication that need not hold for the generic lemmas — they do not care whether it is small. mapQuery's answer translator, which already used ρ, becomes τ (completing the π/σ/τ trio). IndiffFromRO's total stays δ. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The passage read as though a uniform-looking mapping frees the security arguments from considering non-uniformity. It does not — what indifferentiability buys is paying for it once, with a concrete protocol-independent figure, at most q/2^{120} after q queries. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

dannywillems

ACK - I got a bit lost in side quests as I am onboarding on CompElliptic and this repo. I don't want to block future patches on top of this one. The patch is already relatively huge.

The scope bullet still described the modelling as a plan, starting with an indifferentiability proof. That step is delivered by the arc this branch is stacked on (zcash#199): the deployed hash-to-curve is proven indifferentiable from a random oracle onto the group, with a concrete advantage bound, presented in the Group-Hash Indifferentiability chapter. What remains for the ledger games is adversary oracle access to the hash-to-curve, tracked at zcash#188. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

daira force-pushed the fv/indiff-sampler branch from 26a76c0 to 79e5f61 Compare August 15, 2026 16:23

daira mentioned this pull request Aug 15, 2026

chore(book): fix pinned journey #195

Merged

daira force-pushed the fv/indiff-sampler branch 4 times, most recently from b01b5b5 to 6c67576 Compare August 16, 2026 02:47

daira changed the title ~~Group-hash indifferentiability: the fibre sampler, the single-query bias, and the book page~~ Group-hash indifferentiability: the game side, up to the two-oracle collapse Aug 16, 2026

daira force-pushed the fv/indiff-sampler branch 4 times, most recently from bca0944 to 2f4279e Compare August 16, 2026 19:03

daira changed the title ~~Group-hash indifferentiability: the game side, up to the two-oracle collapse~~ Group-hash indifferentiability: the game side and the rejection-sampling simulator Aug 16, 2026

daira force-pushed the fv/indiff-sampler branch from 9e81f03 to a3792b9 Compare August 16, 2026 21:49