• Robbert Krebbers's avatar
    Allow memory refinements to behave like simple renaming. · c5c0d373
    Robbert Krebbers authored
    Memory refinements now carry a boolean parameter that has the following
    meaning:
    
    [false] : Behave like a simple renaming of memories that merely allows to
              permute object identifiers. It does not allow to refine memories
              into a more defined version.
    [true]  : Behave like before. Objects can be injected, and memory contents can
              be refined into a more defined variant.
    
    We make refinements parametric in these two variant to avoid code duplication,
    and because the [false] variant is a special case of the [true] variant.
    
    For completeness of the executable semantics, we now use the [false] variant.
    c5c0d373
base.v 41.7 KB