Consolidate the various approaches we have to projecting from the kernel heap

[michaelmcinerney]

We currently have at least two approaches to performing heap projections, namely the pred_map style, and the |> (opt_map) style.

The pred_map style uses locales together with collections of simplification rules to define and reason with the heap projections, whereas |> is a much more lightweight approach. Given the difficulty of extending the pred_map approach to chains of heaps which have not already been defined, we do prefer the |> approach, which has adequate and simple simplification rules, as well. We face problems especially with lemmas and goals that contain both approaches.

We should consolidate on the |> approach. This in particular would require rewriting all the invariants for MCS given in DetSchedInvs_AI.thy.

Once we have consolidated on the |> approach, we should remove lemmas in DetSchedSchedule_AI.thy in MCS which include misc in the name. These are lemmas which show that some function preserves all properties of a large collection of heaps. These are difficult to update when the abstract specification changes, or when invariants change. A better approach would be to show that functions preserve individual heaps (perhaps via crunch) and then to make greater use of lifting lemmas.

More ambitious projects include

• making greater use of these heap projections in the abstract specification, and
• phrasing invariants which use obj_at/obj_at' in terms of |> and |< (opt_pred).

[Xaphiosis]

I support this motion, and agree that it is the most sensible first step. If we got this, would it be clear that the hoare_lift_Pf blocks will be able to go away? (you didn't mention those, and they were the inspiration for my pushing for an issue)

[michaelmcinerney]

I support this motion, and agree that it is the most sensible first step. If we got this, would it be clear that the hoare_lift_Pf blocks will be able to go away? (you didn't mention those, and they were the inspiration for my pushing for an issue)

Yes, those hoare_lift_Pf blocks only occur in the misc lemmas. We might need a bit of finesse in how we handle the replacements for these misc lemmas: crunch is a great tool, but we may want a way to give crunch a large collection of heaps, and it would be nice if it were easier to spot which of the two dozen or so properties we're crunching is leading to a failure.

[Xaphiosis]

Oh, I thought for some reason it also happened in non-misc lemmas. They certainly seemed to make a more common appearance.

Also, looking through issues I found one that's semi-related to this: #633

[michaelmcinerney]

Oh, I thought for some reason it also happened in non-misc lemmas. They certainly seemed to make a more common appearance.

I suppose they also do occur in lemmas with postconditions of valid_sched_pred_strong and valid_sched_pred, but those are really just abbreviations for a bunch of heaps too. I guess the name "misc" just means "almost like valid_sched_pred_strong or something, but not quite, so it's miscellaneous". So maybe these two predicates should be removed too, and we should use lifting rules instead.

[Xaphiosis]

Ewww. Definitely something we should keep in our sights to improve upon then. I hope the memory of our discussion about lifting rules will remain in your head in case it's ever useful, because until the pred_map/opt_map consolidation my ideas don't really help.