Email Gateway (Aug 19 2022 at 09:53): Email Gateway (Aug 19 2022 at 09:53):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I am using Michael Norrish's C-parser (in the version shipped with
autocorres-0.1) to import a C-program to Isabelle, but I have some
problems dealing with structs: I start with the following C-file
struct foo_t {
unsigned cnt;
};
unsigned foo_cnt(struct foo_t *x) {
return x->cnt;
}
and want to prove that the value returned by foo_cnt is the value of the
field cnt_C of the abstracted version of the struct:
abbreviation "c_lift s ≡ lift_t⇡c (hst_mem s, hst_htd s)"
fun foo where
"foo h n p = (case c_lift h p of Some g ⇒ cnt_C g = n | None ⇒ False)"
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)
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?
-- Lars
Email Gateway (Aug 19 2022 at 09:53):From: David Greenaway <david.greenaway@nicta.com.au>
Hi Lars,
Email Gateway (Aug 19 2022 at 09:54):From: Lars Noschinski <noschinl@in.tum.de>
Hi David,
[...]
Thanks for this lemma; this allows me indeed to make some progress.
-- Lars
Email Gateway (Aug 19 2022 at 10:18):From: Lars Noschinski <noschinl@in.tum.de>
This Lemma has been very useful for me. Maybe it should be part of the
Framework?
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
Email Gateway (Aug 19 2022 at 10:20):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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)
done
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.
Yours,
Thomas.
Last updated: Apr 26 2024 at 08:19 UTC