therefore
Sign up
Open navigation

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

1 topic

3 results

Clear filters
Project-declaredLean 4.32.0

Tv Dist simulate Q with Caching with Programming le prob Event bad

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...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

With Caching Tracking Policy run' eq

OracleComp.ProgramLogic.Relational.withCachingTrackingPolicy_run'_eq'

Plain-language statement

run' projection corollary of withCachingTrackingPolicy_run_proj_eq'.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

With Programming empty run' eq

OracleComp.ProgramLogic.Relational.withProgramming_empty_run'_eq

Plain-language statement

run' projection corollary of withProgramming_empty_run_proj_eq.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record