Project-declaredLean 4.32.0
Simulate Q triple preserves invariant
OracleComp.ProgramLogic.StdDo.simulateQ_triple_preserves_invariant
Plain-language statement
Generic simulation triple: if every handler call handler t preserves an invariant I on the simulation state, then simulateQ handler oa preserves I for any oa : OracleComp spec Ī±. The invariant-only form (same I as pre- and post-condition, independent of return value) is the most common case; stronger per-call specs can be derived by instantiat...
program verificationseparation logiccryptography
Source project: VCVio
Person-level attribution pending.