mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

sepapps safe to cancel #396

Closed vfukala closed 9 months ago

vfukala commented 9 months ago

In LiveVerif: Making predicates_safe_to_cancel succeed if both the hypothesis and the conclusion is a sepapps and all the corresponding constituent predicates are safe to cancel (checked recursively). Adding a test for this (which would previously fail).

samuelgruetter commented 9 months ago

Looks great, thanks!