Currently all of the verifier code assumes that there are always two programs in scope: an original and a patched program. To support "single-stepping" the verifier to consider transitions of only the original or patched program (i.e. to handle divergent control flow) we can generalize the ubiquitous PatchPair datatype to support singleton entries.
Currently this datatype is functor-like in that it provides interfaces to map or fold over its contents, but it still allows its contents to be directly inspected. To generalize this, we need to disallow inspecting PatchPair contents directly and require that all client code use interface functions that are agnostic of trivial (singleton) vs. non-trivial PatchPairs.
Many such interface functions are already defined and in use, but new interface functions will need to be introduced to handle cases where this abstraction boundary is violated.
Currently all of the verifier code assumes that there are always two programs in scope: an original and a patched program. To support "single-stepping" the verifier to consider transitions of only the original or patched program (i.e. to handle divergent control flow) we can generalize the ubiquitous
PatchPairdatatype to support singleton entries. Currently this datatype is functor-like in that it provides interfaces to map or fold over its contents, but it still allows its contents to be directly inspected. To generalize this, we need to disallow inspectingPatchPaircontents directly and require that all client code use interface functions that are agnostic of trivial (singleton) vs. non-trivial PatchPairs. Many such interface functions are already defined and in use, but new interface functions will need to be introduced to handle cases where this abstraction boundary is violated.