Skip to content

Add lemmas for creating later credits for non-pure steps (alternative)

Robbert Krebbers requested to merge robbert/twp_wp_step_lb into master

This is an alternative to !1034 (closed).

Add twp_wp_step_lb and use that to prove steps_lb later credit lemmas for HeapLang atomic instructions.

I only derived the version for Alloc, but the others should be similar.

Let's first see if we like this approach better.

Edited by Robbert Krebbers

Merge request reports