Re: [isabelle] Norrish's C-parser and structs

Hello Lars.

We think your problem can already be solved for the lift_t case via the theorem lift_t_hrs_mem_update_fld. The parser generates simp rules that will match the assumptions of this theorem.

If you are using primarily the h_val form, you might need to wrap this theorem a bit. This is a start:

lemma lift_t_h_val:
  "lift_t g hp p = Some x ==> h_val (hrs_mem hp) p = x"
  apply (cases hp)
  apply (rule lift_t_lift[unfolded lift_def])
  apply (simp add: hrs_mem_def)

thm lift_t_h_val[OF trans, OF lift_t_hrs_mem_update_fld[THEN fun_cong]]

The L4.verified project had a library file that contained a collection of rewrite rules for use in rewriting operations from the Tuch UMM model. Its release status is a bit cloudy because some of it is L4.verified-specific and lots of it was, in hindsight, a bad idea.

In particular, I think that our tendency to deal in lift_t rather than h_val + h_t_valid was a bit of a mistake, and I encourage you to keep h_val around. I also encourage you to be aware that many of the rules in the library are slanted toward reasoning about lift_t heaps.


I feel there should be a similar lemma for field updates, too. Maybe something along the lines of

lemma h_val_update:
  fixes h val f p
defines "h' ≡ hrs_mem_update (heap_update (Ptr &(p→f) :: 'b ptr) val) h"
  assumes fl: "field_ti TYPE('a::{mem_type}) f = Some t"
assumes "export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type}))"
  shows "h_val (hrs_mem h') p =
update_ti_t t (to_bytes val (replicate (size_td t) 0)) (h_val (hrs_mem h) p)"

Has somebody proved something similar already?

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.