• Robbert Krebbers's avatar
    Allow frozen pointer annotations to be refined. · 26917d00
    Robbert Krebbers authored
    The refinement relation on addresses allows union references to be refined:
    
      (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2
    
    The result is that frozen values are below their unfrozen variant, which made
    it possible to prove that constant propagation (see constant_propagation.v) can
    be performed on the level of the memory model.
    26917d00
list.v 143 KB