Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersFiatShamir.Fork.runTrace_target_eq_of_mem_contextFork
Plain-language statement
If two successful contextual forks select the same fork index, their forgery targets agree.
Source project: VCVio
Person-level attribution pending.
FiatShamir.nma_to_hard_relation_bound
Project documentation
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...
Source project: VCVio
Person-level attribution pending.
FiatShamir.perfectlyCorrect
Plain-language statement
Completeness of the Fiat-Shamir signature scheme follows from completeness of the underlying Σ-protocol.
Source project: VCVio
Person-level attribution pending.
FiatShamir.sign_expectedQueryCost_eq_outputExpectation
Plain-language statement
Fiat-Shamir signing has expected weighted query cost equal to the expectation of the queried commitment cost over the output signature distribution.
Source project: VCVio
Person-level attribution pending.
FiatShamir.simulatedNmaAdv_hashQueryBound
Plain-language statement
Hash-query bound for simulatedNmaAdv: if the CMA adversary makes at most qS signing-oracle queries and qH random-oracle queries, the NMA reduction makes at most qH live hash queries. The qS signing queries are absorbed into the managed cache rather than issued live.
Source project: VCVio
Person-level attribution pending.
FiatShamir.Stateful.cma_advantage_le_fork_bound_of_h5
Project documentation
Native stateful top-level chain, assuming the H5 replay-forking boundary. This theorem carries the H1/H2/H3/H4 arithmetic directly in the stateful chain. The bound is in terms of the verify-wrapped adversary nmaAdvFromCmaWithFinalQuery at fork slot parameter qH.
Source project: VCVio
Person-level attribution pending.