Library C_bipl
Require Classical.
Require Import Permutation.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext String_ext Lists_ext Max_ext.
Require Import machine_int.
Import MachineInt.
Local Close Scope Z_scope.
Require Import C_types C_expr.
Require order finmap.
Module Int8 <: finmap.EQTYPE.
Definition A : eqType := int_8_eqType.
End Int8.
Require Import Permutation.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext String_ext Lists_ext Max_ext.
Require Import machine_int.
Import MachineInt.
Local Close Scope Z_scope.
Require Import C_types C_expr.
Require order finmap.
Module Int8 <: finmap.EQTYPE.
Definition A : eqType := int_8_eqType.
End Int8.
a heap is modelled as a list of bytes
Module hp := finmap.map order.NatOrder Int8.
Notation "k '+++' m" := (hp.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (hp.disj k m) (at level 79) : heap_scope.
Notation "k '[\m]' m" := (hp.difs k m) (at level 69) : heap_scope.
Notation "k '[<=m]' m" := (hp.inclu k m) (at level 69) : heap_scope.
Lemma cdom_proj_seq : forall h a n1 n2,
hp.dom h = seq_ext.ran a (n1 + n2) ->
hp.cdom (hp.proj h (seq_ext.ran (a + n1) n2)) = seq_ext.l2s (skipn n1 (seq_ext.s2l (hp.cdom h))).
Lemma take_drop_cdom : forall h a0 a b c,
hp.dom h = seq.cat (seq_ext.ran a0 a) (seq.cat (seq_ext.ran (a0 + a) b) (seq_ext.ran (a0 + a + b) c)) ->
seq.take b (seq.drop a (hp.cdom h)) =
hp.cdom (hp.proj h (seq_ext.ran (a0 + a) b)).
Local Open Scope heap_scope.
Module heap_prop_m := finmap.Map_Prop hp.
Definition chars2heap (a : nat) (l : list (int 8)) : hp.t :=
heap_prop_m.mk_finmap (seq_ext.l2s (combine (seq a (length l)) l)).
Lemma cdom_chars2heap : forall a l, seq_ext.s2l (hp.cdom (chars2heap a l)) = l.
Lemma dom_chars2heap : forall l a, hp.dom (chars2heap a l) = seq_ext.l2s (seq a (length l)).
Lemma chars2heap_app : forall (a b : list (int 8)) p,
chars2heap p (a ++ b) = chars2heap p a +++ chars2heap (p + length a) b.
Lemma disj_chars2heap : forall a l1 l2, chars2heap a l1 # chars2heap (a + length l1) l2.
Notation "k '+++' m" := (hp.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (hp.disj k m) (at level 79) : heap_scope.
Notation "k '[\m]' m" := (hp.difs k m) (at level 69) : heap_scope.
Notation "k '[<=m]' m" := (hp.inclu k m) (at level 69) : heap_scope.
Lemma cdom_proj_seq : forall h a n1 n2,
hp.dom h = seq_ext.ran a (n1 + n2) ->
hp.cdom (hp.proj h (seq_ext.ran (a + n1) n2)) = seq_ext.l2s (skipn n1 (seq_ext.s2l (hp.cdom h))).
Lemma take_drop_cdom : forall h a0 a b c,
hp.dom h = seq.cat (seq_ext.ran a0 a) (seq.cat (seq_ext.ran (a0 + a) b) (seq_ext.ran (a0 + a + b) c)) ->
seq.take b (seq.drop a (hp.cdom h)) =
hp.cdom (hp.proj h (seq_ext.ran (a0 + a) b)).
Local Open Scope heap_scope.
Module heap_prop_m := finmap.Map_Prop hp.
Definition chars2heap (a : nat) (l : list (int 8)) : hp.t :=
heap_prop_m.mk_finmap (seq_ext.l2s (combine (seq a (length l)) l)).
Lemma cdom_chars2heap : forall a l, seq_ext.s2l (hp.cdom (chars2heap a l)) = l.
Lemma dom_chars2heap : forall l a, hp.dom (chars2heap a l) = seq_ext.l2s (seq a (length l)).
Lemma chars2heap_app : forall (a b : list (int 8)) p,
chars2heap p (a ++ b) = chars2heap p a +++ chars2heap (p + length a) b.
Lemma disj_chars2heap : forall a l1 l2, chars2heap a l1 # chars2heap (a + length l1) l2.
get a chunk from a heap
Definition heap_get' (a : nat) (t : typ) (k : hp.t) : option value :=
let subheap := hp.proj k (seq_ext.l2s (seq a (sizeof t))) in
match chars2val t (seq_ext.s2l (hp.cdom subheap)) with
| (v, nil) => Some v
| (v, _) => None
end.
Definition heap_get (a : nat) (t : typ) (k : hp.t) : option value :=
match @seq_ext.inc hp.l (seq_ext.l2s (seq a (sizeof t))) (hp.dom k) with
| false => None
| true => heap_get' a t k
end.
Local Open Scope minC_types.
Lemma heap_get'_eqtm : forall g h a t t', map_ctxt g -> t =t g t= t' ->
heap_get' a t h = heap_get' a t' h.
Lemma heap_get_eqtm : forall g h a t t', map_ctxt g -> t =t g t= t' ->
heap_get a t h = heap_get a t' h.
Lemma heap_get_union_L : forall h1 h2 : hp.t, h1 # h2 ->
forall (n : hp.l) (z : value) t,
heap_get n t h1 = Some z -> heap_get n t (h1 +++ h2) = Some z.
let subheap := hp.proj k (seq_ext.l2s (seq a (sizeof t))) in
match chars2val t (seq_ext.s2l (hp.cdom subheap)) with
| (v, nil) => Some v
| (v, _) => None
end.
Definition heap_get (a : nat) (t : typ) (k : hp.t) : option value :=
match @seq_ext.inc hp.l (seq_ext.l2s (seq a (sizeof t))) (hp.dom k) with
| false => None
| true => heap_get' a t k
end.
Local Open Scope minC_types.
Lemma heap_get'_eqtm : forall g h a t t', map_ctxt g -> t =t g t= t' ->
heap_get' a t h = heap_get' a t' h.
Lemma heap_get_eqtm : forall g h a t t', map_ctxt g -> t =t g t= t' ->
heap_get a t h = heap_get a t' h.
Lemma heap_get_union_L : forall h1 h2 : hp.t, h1 # h2 ->
forall (n : hp.l) (z : value) t,
heap_get n t h1 = Some z -> heap_get n t (h1 +++ h2) = Some z.
update a chunk of a heap
Definition heap_upd (a : nat) (v : value) (t : typ) (k : hp.t) : hp.t :=
let lst := val2chars v t in
let k' := k [\m] seq_ext.l2s (seq a (length lst)) in
k' +++ chars2heap a lst.
Lemma dom_heap_upd : forall n v t h,
seq_ext.inc (hp.dom (chars2heap n (val2chars v t))) (hp.dom h) ->
hp.dom (heap_upd n v t h) = hp.dom h.
Lemma disj_heap_upd : forall z v t h1 h2, h1 # h2 ->
seq_ext.inc (seq_ext.ran z (sizeof t)) (hp.dom h1) ->
heap_upd z v t h1 # h2.
Lemma heap_upd_union_L : forall h1 h2, h1 # h2 -> forall n v t,
seq_ext.inc (seq_ext.ran n (sizeof t)) (hp.dom h1) ->
heap_upd n v t (h1 +++ h2) = (heap_upd n v t h1) +++ h2.
Lemma heap_upd_eqtm : forall g h a v t t', map_ctxt g ->
t =t g t= t' -> heap_upd a v t h = heap_upd a v t' h.
Definition assert := store -> hp.t -> Prop.
Require while.
Definition TT : assert := while.TT store hp.t.
Definition FF : assert := while.FF store hp.t.
Notation "P ===> Q" := (while.entails store hp.t P Q) (at level 90, no associativity) : minC_assert_scope.
Notation "P '//\\' Q" := (while.And store hp.t P Q) (at level 80, no associativity) : minC_assert_scope.
Notation "P <==> Q" := (while.equiv store hp.t P Q) (at level 90, no associativity) : minC_assert_scope.
Definition con (P Q : assert) : assert := fun s h =>
exists h1, exists h2,
h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : minC_assert_scope.
Local Open Scope minC_assert_scope.
let lst := val2chars v t in
let k' := k [\m] seq_ext.l2s (seq a (length lst)) in
k' +++ chars2heap a lst.
Lemma dom_heap_upd : forall n v t h,
seq_ext.inc (hp.dom (chars2heap n (val2chars v t))) (hp.dom h) ->
hp.dom (heap_upd n v t h) = hp.dom h.
Lemma disj_heap_upd : forall z v t h1 h2, h1 # h2 ->
seq_ext.inc (seq_ext.ran z (sizeof t)) (hp.dom h1) ->
heap_upd z v t h1 # h2.
Lemma heap_upd_union_L : forall h1 h2, h1 # h2 -> forall n v t,
seq_ext.inc (seq_ext.ran n (sizeof t)) (hp.dom h1) ->
heap_upd n v t (h1 +++ h2) = (heap_upd n v t h1) +++ h2.
Lemma heap_upd_eqtm : forall g h a v t t', map_ctxt g ->
t =t g t= t' -> heap_upd a v t h = heap_upd a v t' h.
Definition assert := store -> hp.t -> Prop.
Require while.
Definition TT : assert := while.TT store hp.t.
Definition FF : assert := while.FF store hp.t.
Notation "P ===> Q" := (while.entails store hp.t P Q) (at level 90, no associativity) : minC_assert_scope.
Notation "P '//\\' Q" := (while.And store hp.t P Q) (at level 80, no associativity) : minC_assert_scope.
Notation "P <==> Q" := (while.equiv store hp.t P Q) (at level 90, no associativity) : minC_assert_scope.
Definition con (P Q : assert) : assert := fun s h =>
exists h1, exists h2,
h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : minC_assert_scope.
Local Open Scope minC_assert_scope.
Extensionality of predicates can be safely added to Coq (see Coq FAQ)
Axiom assert_ext: forall P Q, P <==> Q -> P = Q.
Lemma con_com: forall P Q, P ** Q <==> Q ** P.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Lemma con_assoc : forall P Q R, (P ** Q) ** R <==> P ** (Q ** R).
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Module map_tac_m := finmap.Map_Tac hp.
Lemma con_TT_inv : forall P, P ** TT ** TT ===> P ** TT.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Lemma monotony : forall s s' h (P Q P' Q' : assert),
(forall h, P s h -> P' s' h) ->
(forall h, Q s h -> Q' s' h) ->
(P ** Q) s h -> (P' ** Q') s' h.
Definition emp : assert := fun s h => h = hp.emp.
Lemma con_emp: forall P, P ** emp ===> P.
Lemma con_emp': forall P, P ===> P ** emp.
Lemma con_emp_equiv : forall P, (P ** emp) = P.
Definition imp (P Q : assert) : assert := fun s h =>
forall h', h # h' -> P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : minC_assert_scope.
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Definition strictly_exact (P : assert) := forall s h h', P s h /\ P s h' -> h = h'.
Lemma strictly_exact_prop : forall P Q,
strictly_exact Q -> P //\\ (Q ** TT) ===> Q ** (Q -* P).
Local Open Scope minC_expr_scope.
Definition mapsto t (e e' : exp) (s : store) (h : hp.t) :=
exists p, [ e ]_ s = Some (pval p) /\
typof s e =ot _ctxt s ot= ptyp t /\
exists v, [ e' ]_ s = Some v /\
sizeof t = length (seq_ext.s2l (hp.cdom h)) /\
chars2val t (seq_ext.s2l (hp.cdom h)) = (v, nil) /\
seq_ext.s2l (hp.dom h) = seq (Zabs_nat (u2Z p)) (sizeof t).
Notation "e1 '|~' t '~>' e2" :=
(mapsto t e1 e2) (at level 77, no associativity) : minC_assert_scope.
Lemma mapsto_inv_len : forall e t e' s h, (e |~ t ~> e') s h ->
seq.size (hp.dom h) = sizeof t.
Lemma mapsto_inv_dom : forall e t e' s h, (e |~ t ~> e') s h ->
exists x, [e]_s = Some (pval x) /\
hp.dom h = seq_ext.ran (Zabs_nat (u2Z x)) (sizeof t).
Lemma mapsto_inv_cdom : forall e t e' s h, (e |~ t ~> e') s h ->
exists v, [e']_s = Some v /\
chars2val t (seq_ext.s2l (hp.cdom h)) = (v, nil).
Lemma singl_equal: forall t s h1 h2 e1 e2 e3 e4,
(e1 |~ t ~> e2) s h1 ->
(e3 |~ t ~> e4) s h2 ->
[ e1 ]_ s = [ e3 ]_ s -> [ e2 ]_ s = [ e4 ]_ s ->
h1 = h2.
Definition mapsto_char := mapsto (btyp uchar).
Notation "e1 '|~c~>' e2" := (mapsto_char e1 e2) (at level 77, no associativity) : minC_assert_scope.
Lemma strictly_exact_mapsto : forall e t e', strictly_exact (e |~ t ~> e').
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Lemma mapsto_styp_inv : forall x tg l vs s h p,
assoc_get tg (_ctxt s) = Some l ->
forall
(wf_tg : wft (styp tg l))
(l_vs : length l = length vs)
(l_vs2 : forallb (fun x => typ_val (fst x) (snd x))
(combine (uzip2 l) vs)),
(var_e x |~ styp tg l ~> cst_se tg l vs wf_tg l_vs l_vs2) s h ->
[var_e x]_ s = Some (pval p) ->
(u2Z p + Z_of_nat (sizeof (styp tg l)) < 2 ^^ ptr_len)%Z ->
forall i f t t' vi k,
ifind f (uzip1 l) = Some i ->
ith i vs = Some vi ->
assoc_get f l = Some t' ->
t =t _ctxt s t= t' ->
val2cst (_ctxt s) t vi = Some k ->
(var_e x .-> f |~ t ~> k ** TT) s h.
Lemma mapsto_ext : forall (s s' : store) h t (e1' : exp) e2' (e1 : exp) e2,
typof s e1 =ot _ctxt s ot= ptyp t ->
typof s e1' =ot _ctxt s ot= ptyp t ->
[ e1' ]_ s' = [ e1 ]_ s -> [ e2' ]_ s' = [ e2 ]_ s ->
(e1' |~ t ~> e2') s' h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_ext_weak : forall s h t e1' e2' e1 e2,
typof s e1 = typof s e1' ->
[ e1' ]_ s = [ e1 ]_ s -> [ e2' ]_ s = [ e2 ]_ s ->
(e1' |~ t ~> e2') s h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_ext_new2 : forall s (Hmap : map_ctxt (_ctxt s)) s' h t (Hcover : cover (_ctxt s) (ptyp t)) (e1' : exp) e2' (e1 : exp) e2,
typof s e1 =ot _ctxt s ot= ptyp t ->
typof s' e1' =ot _ctxt s' ot= ptyp t ->
[ e1' ]_ s' = [ e1 ]_ s -> [ e2' ]_ s' = [ e2 ]_ s ->
(e1' |~ t ~> e2') s' h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_strictly_exact' : forall t (e v : exp) (Q : assert) s h1 h2 h1_h2,
wft t -> h1_h2 = h1 +++ h2 -> h1 # h2 -> Q s h1_h2 ->
(e |~ t ~> v) s h1 -> (e |~ t ~> v -* Q) s h2.
Lemma con_com: forall P Q, P ** Q <==> Q ** P.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Lemma con_assoc : forall P Q R, (P ** Q) ** R <==> P ** (Q ** R).
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Module map_tac_m := finmap.Map_Tac hp.
Lemma con_TT_inv : forall P, P ** TT ** TT ===> P ** TT.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Lemma monotony : forall s s' h (P Q P' Q' : assert),
(forall h, P s h -> P' s' h) ->
(forall h, Q s h -> Q' s' h) ->
(P ** Q) s h -> (P' ** Q') s' h.
Definition emp : assert := fun s h => h = hp.emp.
Lemma con_emp: forall P, P ** emp ===> P.
Lemma con_emp': forall P, P ===> P ** emp.
Lemma con_emp_equiv : forall P, (P ** emp) = P.
Definition imp (P Q : assert) : assert := fun s h =>
forall h', h # h' -> P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : minC_assert_scope.
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Definition strictly_exact (P : assert) := forall s h h', P s h /\ P s h' -> h = h'.
Lemma strictly_exact_prop : forall P Q,
strictly_exact Q -> P //\\ (Q ** TT) ===> Q ** (Q -* P).
Local Open Scope minC_expr_scope.
Definition mapsto t (e e' : exp) (s : store) (h : hp.t) :=
exists p, [ e ]_ s = Some (pval p) /\
typof s e =ot _ctxt s ot= ptyp t /\
exists v, [ e' ]_ s = Some v /\
sizeof t = length (seq_ext.s2l (hp.cdom h)) /\
chars2val t (seq_ext.s2l (hp.cdom h)) = (v, nil) /\
seq_ext.s2l (hp.dom h) = seq (Zabs_nat (u2Z p)) (sizeof t).
Notation "e1 '|~' t '~>' e2" :=
(mapsto t e1 e2) (at level 77, no associativity) : minC_assert_scope.
Lemma mapsto_inv_len : forall e t e' s h, (e |~ t ~> e') s h ->
seq.size (hp.dom h) = sizeof t.
Lemma mapsto_inv_dom : forall e t e' s h, (e |~ t ~> e') s h ->
exists x, [e]_s = Some (pval x) /\
hp.dom h = seq_ext.ran (Zabs_nat (u2Z x)) (sizeof t).
Lemma mapsto_inv_cdom : forall e t e' s h, (e |~ t ~> e') s h ->
exists v, [e']_s = Some v /\
chars2val t (seq_ext.s2l (hp.cdom h)) = (v, nil).
Lemma singl_equal: forall t s h1 h2 e1 e2 e3 e4,
(e1 |~ t ~> e2) s h1 ->
(e3 |~ t ~> e4) s h2 ->
[ e1 ]_ s = [ e3 ]_ s -> [ e2 ]_ s = [ e4 ]_ s ->
h1 = h2.
Definition mapsto_char := mapsto (btyp uchar).
Notation "e1 '|~c~>' e2" := (mapsto_char e1 e2) (at level 77, no associativity) : minC_assert_scope.
Lemma strictly_exact_mapsto : forall e t e', strictly_exact (e |~ t ~> e').
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Lemma mapsto_styp_inv : forall x tg l vs s h p,
assoc_get tg (_ctxt s) = Some l ->
forall
(wf_tg : wft (styp tg l))
(l_vs : length l = length vs)
(l_vs2 : forallb (fun x => typ_val (fst x) (snd x))
(combine (uzip2 l) vs)),
(var_e x |~ styp tg l ~> cst_se tg l vs wf_tg l_vs l_vs2) s h ->
[var_e x]_ s = Some (pval p) ->
(u2Z p + Z_of_nat (sizeof (styp tg l)) < 2 ^^ ptr_len)%Z ->
forall i f t t' vi k,
ifind f (uzip1 l) = Some i ->
ith i vs = Some vi ->
assoc_get f l = Some t' ->
t =t _ctxt s t= t' ->
val2cst (_ctxt s) t vi = Some k ->
(var_e x .-> f |~ t ~> k ** TT) s h.
Lemma mapsto_ext : forall (s s' : store) h t (e1' : exp) e2' (e1 : exp) e2,
typof s e1 =ot _ctxt s ot= ptyp t ->
typof s e1' =ot _ctxt s ot= ptyp t ->
[ e1' ]_ s' = [ e1 ]_ s -> [ e2' ]_ s' = [ e2 ]_ s ->
(e1' |~ t ~> e2') s' h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_ext_weak : forall s h t e1' e2' e1 e2,
typof s e1 = typof s e1' ->
[ e1' ]_ s = [ e1 ]_ s -> [ e2' ]_ s = [ e2 ]_ s ->
(e1' |~ t ~> e2') s h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_ext_new2 : forall s (Hmap : map_ctxt (_ctxt s)) s' h t (Hcover : cover (_ctxt s) (ptyp t)) (e1' : exp) e2' (e1 : exp) e2,
typof s e1 =ot _ctxt s ot= ptyp t ->
typof s' e1' =ot _ctxt s' ot= ptyp t ->
[ e1' ]_ s' = [ e1 ]_ s -> [ e2' ]_ s' = [ e2 ]_ s ->
(e1' |~ t ~> e2') s' h -> (e1 |~ t ~> e2) s h.
Lemma mapsto_strictly_exact' : forall t (e v : exp) (Q : assert) s h1 h2 h1_h2,
wft t -> h1_h2 = h1 +++ h2 -> h1 # h2 -> Q s h1_h2 ->
(e |~ t ~> v) s h1 -> (e |~ t ~> v -* Q) s h2.
connective for arrays
Fixpoint mapstos (t : typ) (e : exp) (l : list exp) {struct l} : assert :=
match l with
| nil => emp
| e1 :: tl => (e |~ t ~> e1) ** mapstos t (add_pe e (cst32 (Z2u 32 1))) tl
end.
Notation "x '|%' t '%>' l" := (mapstos t x l) (at level 77) : minC_assert_scope.
Notation "e1 '|%c%>' e2" := (mapstos (btyp uchar) e1 e2) (at level 77, no associativity) : minC_assert_scope.
Require Import nodup.
Lemma mapstos_ext : forall t (e' e : exp) l (s : store) h,
typof s e' =ot _ctxt s ot= ptyp t ->
typof s e =ot _ctxt s ot= ptyp t ->
[ e' ]_ s = [ e ]_ s ->
(e' |% t %> l) s h -> (e |% t %> l) s h.
Lemma mapstos_ext_cst : forall n (cst : int n -> exp)
(Hcst : forall s s' a, [cst a]_s = [cst a]_s')
(j : ityp)
(e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp j) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp j) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |% btyp j %> map cst l) s' h -> (e |% btyp j %> map cst l) s h.
Lemma mapstos_ext_cst8 : forall (e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp uchar) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp uchar) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |%c%> map cst8 l) s' h -> (e |%c%> map cst8 l) s h.
Lemma mapstos_ext_cst32 : forall (e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp uint32) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp uint32) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |% btyp uint32 %> map cst32 l) s' h -> (e |% btyp uint32 %> map cst32 l) s h.
Local Open Scope zarith_ext_scope.
Local Open Scope Z_scope.
Lemma mapsto_styp_cons : forall h n s l tg t v vs e0 e1
(wft_ht : wft (styp tg (h :: t)))
(wft_t : wft (styp tg t)),
forall (t_vs : length (h :: t) = length (v :: vs))
(Hforall : forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 (h :: t)) (v :: vs))),
cover (_ctxt s) (ptyp (styp tg (h :: t))) ->
0 <= Z_of_nat n < 2 ^^ ptr_len ->
length l = sizeof (styp tg (h :: t)) ->
val2cst (_ctxt s) (snd h) v = Some e0 ->
val2cst (_ctxt s) (styp tg t) (sval vs) = Some e1 ->
(cst_pe (wft_styp_inv1 _ _ _ wft_ht) (Z2u ptr_len (Z_of_nat n)) |~ snd h ~> e0) s
(chars2heap n (firstn (sizeof (snd h)) l)) ->
(cst_pe wft_t (scale (Z2u ptr_len (Z_of_nat n)) (sizeof (snd h)) 1) |~ styp tg t ~> e1) s
(chars2heap (n + sizeof (snd h)) (skipn (sizeof (snd h)) l)) ->
(cst_pe wft_ht (Z2u ptr_len (Z_of_nat n)) |~ styp tg (h :: t) ~>
cst_se tg (h :: t) (v :: vs) wft_ht t_vs Hforall) s
(chars2heap n l).
Lemma mapsto_prop : forall s, complete (_ctxt s) ->
forall t l adr e (wft_t : wft t), cover (_ctxt s) t ->
sizeof t = length l ->
(0 <= Z_of_nat (adr + length l) < 2 ^^ ptr_len)%Z ->
val2cst (_ctxt s) t (fst (chars2val t l)) = Some e ->
(cst_pe wft_t (Z2u ptr_len (Z_of_nat adr)) |~ t ~> e) s (chars2heap adr l).
Local Close Scope Z_scope.
Lemma mapstos_prop : forall n s, complete (_ctxt s) -> forall l es,
length l = n ->
forall t (cover_t : cover (_ctxt s) t) a q (Hq : q <> O) (wf_t : wft t),
length l = q * sizeof t ->
(0 <= Z_of_nat (a + length l) < 2 ^^ ptr_len)%Z ->
vals2csts s.(_ctxt) t (chars2vals t l) = Some es ->
(cst_pe wf_t (Z2u ptr_len (Z_of_nat a)) |% t %> es)
s (chars2heap a l).
Lemma Z2s_Z2u : forall n a, (0 <= a < 2 ^^ n)%Z ->
Z2s (S n) a = Z2u (S n) a.
Qed.
Lemma mapstos_prop_char : forall l a s, complete (_ctxt s) ->
(0 <= Z_of_nat (a + (length l) * sizeof (btyp uchar)) < 2 ^^ ptr_len)%Z ->
(cst_pe wf_uchar (Z2u ptr_len (Z_of_nat a)) |%c%>
map cst8 l) s (chars2heap a l).
Local Open Scope Z_scope.
Lemma mapstos_app_sepcon_cst8: forall e l1 l2 s h,
Z_of_nat (List.length l1) + 1 < 2 ^^ 31 ->
wf_tstore (_tstore s) ->
typof s e =ot _ctxt s ot= ptyp (btyp uchar) ->
(e |%c%> map cst8 (l1 ++ l2)) s h ->
((e |%c%> map cst8 l1) ** (add_pe e (cst32 (Z2s _ (Z_of_nat (List.length l1)))) |%c%> map cst8 l2)) s h.
Local Close Scope Z_scope.
match l with
| nil => emp
| e1 :: tl => (e |~ t ~> e1) ** mapstos t (add_pe e (cst32 (Z2u 32 1))) tl
end.
Notation "x '|%' t '%>' l" := (mapstos t x l) (at level 77) : minC_assert_scope.
Notation "e1 '|%c%>' e2" := (mapstos (btyp uchar) e1 e2) (at level 77, no associativity) : minC_assert_scope.
Require Import nodup.
Lemma mapstos_ext : forall t (e' e : exp) l (s : store) h,
typof s e' =ot _ctxt s ot= ptyp t ->
typof s e =ot _ctxt s ot= ptyp t ->
[ e' ]_ s = [ e ]_ s ->
(e' |% t %> l) s h -> (e |% t %> l) s h.
Lemma mapstos_ext_cst : forall n (cst : int n -> exp)
(Hcst : forall s s' a, [cst a]_s = [cst a]_s')
(j : ityp)
(e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp j) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp j) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |% btyp j %> map cst l) s' h -> (e |% btyp j %> map cst l) s h.
Lemma mapstos_ext_cst8 : forall (e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp uchar) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp uchar) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |%c%> map cst8 l) s' h -> (e |%c%> map cst8 l) s h.
Lemma mapstos_ext_cst32 : forall (e e' : exp) l (s s' : store) h,
wf_tstore (_tstore s) ->
wf_tstore (_tstore s') ->
typof s e =ot _ctxt s ot= ptyp (btyp uint32) ->
typof s' e' =ot _ctxt s' ot= ptyp (btyp uint32) ->
[ e' ]_ s' = [ e ]_ s ->
(e' |% btyp uint32 %> map cst32 l) s' h -> (e |% btyp uint32 %> map cst32 l) s h.
Local Open Scope zarith_ext_scope.
Local Open Scope Z_scope.
Lemma mapsto_styp_cons : forall h n s l tg t v vs e0 e1
(wft_ht : wft (styp tg (h :: t)))
(wft_t : wft (styp tg t)),
forall (t_vs : length (h :: t) = length (v :: vs))
(Hforall : forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 (h :: t)) (v :: vs))),
cover (_ctxt s) (ptyp (styp tg (h :: t))) ->
0 <= Z_of_nat n < 2 ^^ ptr_len ->
length l = sizeof (styp tg (h :: t)) ->
val2cst (_ctxt s) (snd h) v = Some e0 ->
val2cst (_ctxt s) (styp tg t) (sval vs) = Some e1 ->
(cst_pe (wft_styp_inv1 _ _ _ wft_ht) (Z2u ptr_len (Z_of_nat n)) |~ snd h ~> e0) s
(chars2heap n (firstn (sizeof (snd h)) l)) ->
(cst_pe wft_t (scale (Z2u ptr_len (Z_of_nat n)) (sizeof (snd h)) 1) |~ styp tg t ~> e1) s
(chars2heap (n + sizeof (snd h)) (skipn (sizeof (snd h)) l)) ->
(cst_pe wft_ht (Z2u ptr_len (Z_of_nat n)) |~ styp tg (h :: t) ~>
cst_se tg (h :: t) (v :: vs) wft_ht t_vs Hforall) s
(chars2heap n l).
Lemma mapsto_prop : forall s, complete (_ctxt s) ->
forall t l adr e (wft_t : wft t), cover (_ctxt s) t ->
sizeof t = length l ->
(0 <= Z_of_nat (adr + length l) < 2 ^^ ptr_len)%Z ->
val2cst (_ctxt s) t (fst (chars2val t l)) = Some e ->
(cst_pe wft_t (Z2u ptr_len (Z_of_nat adr)) |~ t ~> e) s (chars2heap adr l).
Local Close Scope Z_scope.
Lemma mapstos_prop : forall n s, complete (_ctxt s) -> forall l es,
length l = n ->
forall t (cover_t : cover (_ctxt s) t) a q (Hq : q <> O) (wf_t : wft t),
length l = q * sizeof t ->
(0 <= Z_of_nat (a + length l) < 2 ^^ ptr_len)%Z ->
vals2csts s.(_ctxt) t (chars2vals t l) = Some es ->
(cst_pe wf_t (Z2u ptr_len (Z_of_nat a)) |% t %> es)
s (chars2heap a l).
Lemma Z2s_Z2u : forall n a, (0 <= a < 2 ^^ n)%Z ->
Z2s (S n) a = Z2u (S n) a.
Qed.
Lemma mapstos_prop_char : forall l a s, complete (_ctxt s) ->
(0 <= Z_of_nat (a + (length l) * sizeof (btyp uchar)) < 2 ^^ ptr_len)%Z ->
(cst_pe wf_uchar (Z2u ptr_len (Z_of_nat a)) |%c%>
map cst8 l) s (chars2heap a l).
Local Open Scope Z_scope.
Lemma mapstos_app_sepcon_cst8: forall e l1 l2 s h,
Z_of_nat (List.length l1) + 1 < 2 ^^ 31 ->
wf_tstore (_tstore s) ->
typof s e =ot _ctxt s ot= ptyp (btyp uchar) ->
(e |%c%> map cst8 (l1 ++ l2)) s h ->
((e |%c%> map cst8 l1) ** (add_pe e (cst32 (Z2s _ (Z_of_nat (List.length l1)))) |%c%> map cst8 l2)) s h.
Local Close Scope Z_scope.