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 350 research declarations. Search 10,000 more complete Mathlib declarations.
350 results
Clear filtersOracleComp.ProgramLogic.Relational.relTriple_list_foldlM
Plain-language statement
Loop-invariant rule for bounded left folds over related input lists.
Source project: VCVio
Person-level attribution pending.
OracleComp.ProgramLogic.Relational.relTriple_prod
Plain-language statement
Core lift: two support-style unary postconditions combine into a relational coupling. The product coupling evalDist oa β evalDist ob witnesses the conjunction, using the canonical MonadLiftT (OracleComp spec) PMF to ensure neither side has failure mass.
Source project: VCVio
Person-level attribution pending.
OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT_of_triples
Plain-language statement
WriterT analogue of relTriple_simulateQ_run_of_triples (monoid variant). Given matching unary Std.Do.Triple specs for two WriterT-based handlers, a monoid-congruent writer relation R_writer (via hR_one and hR_mul), and a synchronization condition on per-query postconditions, derive a whole-program RelTriple on the full (output, writer) o...
Source project: VCVio
Person-level attribution pending.
OracleComp.ProgramLogic.Relational.relTriple'_iff_couplingPost
Plain-language statement
The eRHL-based relational triple RelTriple' agrees with the coupling-based CouplingPost: for any post-relation R, there is a coupling of π[oa] and π[ob] supported on R exactly when the eRHL judgement holds.
Source project: VCVio
Person-level attribution pending.
OracleComp.ProgramLogic.Relational.tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad'
Plain-language statement
Heterogeneous identical-until-bad bridge (output marginal). The TV-distance between the output marginal of so.withCaching and the output marginal of so.withProgramming policy is bounded by the probability that the bad flag of withProgramming policy fires during the run, for any base implementation so valued in OracleComp spec' with spec' u...
Source project: VCVio
Person-level attribution pending.
OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run'_eq'
Plain-language statement
run' projection corollary of withCachingTrackingPolicy_run_proj_eq'.
Source project: VCVio
Person-level attribution pending.