Lower the semi-concrete executor

[skeuchel]

Currently the mutator for the semi-concrete executor uses the spatial specification monad
forall {A}, (A -> SCHeap -> Prop) -> SCHeap -> Prop, i.e. we use regular props on shallowly embedded heaps. There is a tight coupling between the symbolic and the semi-concrete mutator: the deeply-embedded heap always needs to be syntactically instantiable to the shallow one. I'm afraid that might bite us at some point when we want to run user-defined heuristics to automate spatial reasoning. One possibility would be to change it to forall {A P} {SepLogic P}, (A -> P) -> P, effectively running the semi-concrete executor at almost the same level as the Hoare triple-based program logic.