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

1 topic

2 results

Clear filters
Project-declaredLean 4.32.0

Wp Except T bind

OracleComp.ProgramLogic.Loom.wp_ExceptT_bind

Plain-language statement

Quantitative Std.Do'.WP interpretation of OracleComp spec valued in ℝ≥0∞. The wpTrans is the existing MAlgOrdered.wp (i.e. expectation of post under evalDist); the EPost.nil argument is ignored since OracleComp has no first-class exception slot. The three WP axioms reduce to the existing MAlgOrdered.{wp_pure, wp_bind, wp_mono} equali...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Rel Triple' iff coupling Post

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.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record