search

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

Document Limited LiveVerif Automation Experienced In Crit-Bit #430

Closed vfukala closed 2 months ago

vfukala commented 2 months ago

During my crit-bit tree development using Live Verification, I came across some proofs that I thought the framework should ideally be able to do on its own but actually couldn't.

I haven't figured out a way of properly fixing this, so I at least extracted the code to near-minimal examples -- those are the content of this PR.

samuelgruetter commented 2 months ago

Thanks, good to have these documented in stand-alone files!