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 169 research declarations. Search 10,000 more complete Mathlib declarations.
169 results
Clear filtersOracleComp.transcript_countQ_le_of_isPerIndexQueryBound
Plain-language statement
Per-index query bound. If oa respects a per-index budget qb, then for every oracle index t the transcript contains at most qb t queries to t.
Source project: VCVio
Person-level attribution pending.
OracleComp.transcript_countQ_le_of_isQueryBoundP
Plain-language statement
Predicate query bound. If oa makes at most n queries matching p, the transcript contains at most n p-matching entries (QueryLog.countQ).
Source project: VCVio
Person-level attribution pending.
OracleComp.withQueryLog_self_log_eq
Plain-language statement
Self-log fixed point. The two log layers produced by oa.withQueryLog.withQueryLog agree on every support point: simulating the logging oracle over oa.withQueryLog records exactly the queries that the inner withQueryLog already recorded, since withQueryLog does not add new queries to the underlying OracleComp.
Source project: VCVio
Person-level attribution pending.
OracleSpec.QueryLog.getQueryValue?_eq_getAt?
Plain-language statement
Query-log lookup is the OracleSpec specialization of dependent lookup on PolyFun traces.
Source project: VCVio
Person-level attribution pending.
PFunctor.DynSystem.DynComputation.unroll_wrap
Plain-language statement
Fuelled unrolling commutes with interface transport along a lens: the unrolled query tree of the wrapped machine is the lens-translated unrolled tree. The syntactic (FreeM-level) content of interface wrapping, from which handler-level wrapping laws follow by FreeM.liftM naturality without touching machine states.
Source project: VCVio
Person-level attribution pending.
PRFScheme.prf_implies_uf_cma
Plain-language statement
Boneh-Shoup Theorem 6.2. PRF security implies UF-CMA security for the derived MAC: for any forger A, the constructed distinguisher macToPRFReduction prf A satisfies UF_CMA_Advantage(A) ≤ prfAdvantage(prf, B) + 1/|R|.
Source project: VCVio
Person-level attribution pending.