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

Sign Attempt run with Unit Cost eq

FiatShamirWithAbort.signAttempt_run_withUnitCost_eq

Plain-language statement

Unit-cost specialization of the run formula: each signing attempt run tags its output with a single unit of cost (cf. signAttempt_run_withAddCost_eq).

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Verify expected Query Cost eq

FiatShamirWithAbort.verify_expectedQueryCost_eq

Plain-language statement

Verification has expected weighted query cost equal to the cost of the single verification query when a signature is present, and 0 when the signature is none.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Almost Complete

Fischlin.almostComplete

Plain-language statement

Almost completeness of the Fischlin transform: if the underlying Σ-protocol is perfectly complete, then the signature scheme verifies with probability at least 1 - completenessError ρ b S t where t = FinEnum.card Chal is the challenge space size. Unlike the Fiat-Shamir transform (which is perfectly complete), the Fischlin transform has a non-zero comp...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Knowledge Soundness

Fischlin.knowledgeSoundness

Plain-language statement

Knowledge soundness of the Fischlin transform via online (straight-line) extraction (Fischlin 2005, Theorem 2). If the Σ-protocol is specially sound with unique responses, then for any cheating prover making at most Q hash queries, the probability that the verifier accepts but the online extractor fails to recover a valid witness is at most `(Q + 1) · (...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Run m Of Fn query hit

Fischlin.run_mOfFn_query_hit

Plain-language statement

Simulating the verifier's Fin.mOfFn of random-oracle re-queries on a cache that already stores every re-queried record is deterministic: each query is a cache hit returning the stored value, leaving the cache untouched. The result is the pure product of the per-repetition outputs f i (hash i), where hash i is the value cached at record i.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sign uses At Most Rho Card Omega Queries

Fischlin.sign_usesAtMostRhoCardOmegaQueries

Plain-language statement

Fischlin signing makes at most ρ * |Ω| random-oracle queries under unit-cost instrumentation.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record