Source-pinned research

Research proof index

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 150 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

150 results

Clear filters
Project-declaredLean 4.32.0

Signed Candidate Adv cma Sign Hash Query Bound

FiatShamir.Stateful.signedCandidateAdv_cmaSignHashQueryBound

Plain-language statement

Candidate production, with signing queries logged before final verification, preserves the source adversary signing/hash query budget.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Fs Abort Sign Loop cache invariant

FiatShamirWithAbort.fsAbortSignLoop_cache_invariant

Plain-language statement

When the simulated signing loop produces some (w, z), the random-oracle cache contains a challenge c at (msg, w) satisfying ids.verify pk w c z = true. This is proved by induction on the loop counter: each abort iteration preserves the invariant (the cache only grows), and a successful iteration writes exactly the challenge used in verification.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sign expected Queries eq sum abort Prefix Probabilities

FiatShamirWithAbort.sign_expectedQueries_eq_sum_abortPrefixProbabilities

Plain-language statement

The expected number of signing queries is the sum, over prefixes of the retry loop, of the probability that every attempt in the prefix aborts.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sign Attempt expected Query Cost eq output Expectation

FiatShamirWithAbort.signAttempt_expectedQueryCost_eq_outputExpectation

Plain-language statement

The expected weighted query cost of one signing attempt is the expectation of the queried commitment cost over the attempt output distribution.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record