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



Hi Lars,

On 11/01/13 03:59, Lars Noschinski wrote:
[...]
> This leaves me with the following subgoal, which I am not able to
> prove:
>
>   1. ⋀globals x a.
>         lift_t⇡c (hrs_mem (t_hrs_' globals), hrs_htd (t_hrs_' globals)) x = Some a ⟹
>         h_val (hrs_mem (t_hrs_' globals)) (Ptr &(x→[''cnt_C''])) = cnt_C a
>
> So, how do I relate the projections of an abstracted struct to a field
> with the pointer access to said field of the concrete struct?

I found to make much progress with Tuch's framework, I needed the
following lemma (the proof is long and ugly, most of it hastily clagged
from Tuch's proof of "lift_typ_heap_mono":

  lemma h_val_field_from_bytes:
    "\<lbrakk> field_ti TYPE('a::{mem_type}) f = Some t;
       export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type})) \<rbrakk> \<Longrightarrow>
      h_val (hrs_mem h) (Ptr &(pa\<rightarrow>f) :: 'b ptr) = from_bytes (access_ti\<^isub>0 t (h_val (hrs_mem h) pa))"
    apply (clarsimp simp: field_ti_def split: option.splits)
    apply (clarsimp simp: h_val_def)
    apply (frule field_lookup_export_uinfo_Some)
    apply (frule_tac bs="heap_list (hrs_mem h) (size_of TYPE('a)) (ptr_val pa)" in fi_fa_consistentD)
     apply simp
    apply (clarsimp simp: field_lvalue_def field_offset_def
        field_offset_untyped_def typ_uinfo_t_def field_names_def
        access_ti\<^isub>0_def)
    apply (subst drop_heap_list_le)
     apply(simp add: size_of_def)
     apply(drule td_set_field_lookupD)
     apply(drule td_set_offset_size)
     apply simp
    apply(subst take_heap_list_le)
     apply(simp add: size_of_def)
     apply(drule td_set_field_lookupD)
     apply(drule td_set_offset_size)
     apply simp
    apply (fold norm_bytes_def)
    apply (subgoal_tac "size_td a = size_of TYPE('b)")
     apply (clarsimp simp: norm)
    apply(clarsimp simp: size_of_def)
    apply(subst typ_uinfo_size [symmetric])
    apply(unfold typ_uinfo_t_def)
    apply(drule sym)
    apply simp
    done

I am not sure if there is already a better way of doing it, but I did
find using the above lemma made my own proofs easier.

For example, once this is in place, your proof can be finished as
follows:

  lemma "Γ  ⊢ ⦃ σ. foo σ n ´x ⦄ ´ret__unsigned :== CALL foo_cnt (´x) ⦃ ´ret__unsigned = n ⦄"
    apply vcg
    apply (clarsimp simp: lift_t_g split: option.split_asm)
    apply (intro conjI)
     apply (rule c_guard_field_lvalue)
       apply (simp add: lift_t_g split: option.split_asm)
      apply fastforce
     apply (simp add: typ_uinfo_t_def)
    apply (subst h_val_field_from_bytes)
      apply simp
     apply simp
    apply (clarsimp simp: lift_t_if split: split_if_asm)
    done

Hope this helps,
David


--




________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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