Writing general heap proofs with locales (Autocorres)

[Torrencem]

So I have a bunch of theorems that use autocorres heap constructs (in particular "heap_w32, heap_w32_update, etc.") that I would like to use across multiple runs of AutoCorres. The way it looks like this is done internally is with the "valid_typ_heap" function.

However, as is written here (page 154), this is a good use case for locales. So, to start with, I have the locale:

locale heap_abs =
  fixes st :: "'s ⇒ 't"
    and getter :: "'t ⇒ word32 ptr ⇒ word32"
    and setter :: "((word32 ptr ⇒ word32) ⇒ (word32 ptr ⇒ word32)) ⇒ 't ⇒ 't"
    and vgetter :: "'t ⇒ word32 ptr ⇒ bool"
    and vsetter :: "((word32 ptr ⇒ bool) ⇒ (word32 ptr ⇒ bool)) ⇒ 't ⇒ 't"
    and t_hrs :: "'s ⇒ heap_raw_state"
    and t_hrs_update :: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's"
  assumes is_valid_typ_heap: "valid_typ_heap st getter setter vgetter vsetter t_hrs t_hrs_update"

This is alright for my use cases (meaning I can transfer my proofs into the locale no problem). Then when I want to create an interpretation of this to use with a specific C file, I can write (in a given file after loading AutoCorres):

interpretation H: heap_abs 
  "lift_global_heap :: globals ⇒ lifted_globals"
  "heap_w32 :: lifted_globals ⇒ word32 ptr ⇒ word32"
  "heap_w32_update :: ((word32 ptr ⇒ word32) ⇒ (word32 ptr ⇒ word32)) ⇒ lifted_globals ⇒ lifted_globals"
  "is_valid_w32 :: lifted_globals ⇒ word32 ptr ⇒ bool"
  "is_valid_w32_update :: ((word32 ptr ⇒ bool) ⇒ (word32 ptr ⇒ bool)) ⇒ lifted_globals ⇒ lifted_globals"
  "t_hrs_' :: globals ⇒ heap_raw_state"
  "t_hrs_'_update :: (heap_raw_state ⇒ heap_raw_state) ⇒ globals ⇒ globals"

The problem is proving this interpretation is correct. I know through much reading and troubleshooting that internally, AutoCorres proves that:

valid_typ_heap lift_global_heap heap_w32 heap_w32_update
    is_valid_w32 is_valid_w32_update t_hrs_' t_hrs_'_update

However, I see no way to convince isabelle of that fact. Until now, I had manually re-proved the valid_typ_heap condition, but this is very fragile, and breaks when, for example, new types are introduced to the C file. Is there any way I could access the valid_typ_heap proof to prove my interpretation here?

Are there any other suggestions for writing these general proofs? Using valid_typ_heap as a precondition is too restrictive in general, as it makes it much more difficult to generalize constructs such as functions that would otherwise live within the locale.

[mbrcknl]

Sorry for the slow reply. It's an excellent question!

It looks like the function which proves valid_typ_heap is mk_valid_typ_heap_thm in heap_lift.ML. It's used to produce theorems for all lifted heaps, and these are returned from lifted_globals_lemmas along with some others. prepare_heap_lift incorporates those theorems into a structure, which it also ultimately returns. The top-level do_autocorres function passes that structure through to HeapLift.translate, where the valid_typ_heap theorems are used perform heap abstraction on function definitions. But those valid_typ_heap theorems are never stored in the theory context.

And I guess that's the problem you're describing: Autocorres doesn't give you a way to get hold of those theorems.

I can see two or three ways to attack this:

1. Refactor heap_lift.ML so that it saves additional theorems into the local theory context as it generates them.
2. Factor out the ML tactic so you can use it elsewhere.
3. Duplicate the logic of the ML tactic as an Isar method.

The third might be the most straightforward. The ML tactic is found in the first part of lifted_globals_lemmas. It looks like it's roughly equivalent to the following:

method prove_valid_typ_heap =
  (rule valid_typ_heapI,
   (fastforce simp: valid_typ_heap_simps | ((intros conjI ext)?, clarsimp simp: valid_typ_heap_simps))+)[1]

You'll need to figure out how to construct valid_typ_heap_simps to match the ss ruleset in lifted_globals_lemmas. As you pointed out, that ruleset will depend on the particular C you've parsed, but hopefully you can find a way to construct a ruleset that's robust to changes in the C.

Let us know if that helps you get started.

[mbrcknl]

Oh, I should acknowledge @vjackson725, who pointed me to the start of that trail.