Library mapstos
Require Import ssreflect ssrbool.
Require Import ZArith_ext Lists_ext.
Require Import omegaz.
Require Import machine_int.
Import MachineInt.
Require Import mips_bipl.
Local Open Scope Z_scope.
Local Open Scope heap_scope.
Import expr_m.
Import assert_m.
Local Open Scope zarith_ext_scope.
Local Open Scope mips_assert_scope.
Lemma mapstos_decompose_generic : forall n lst nj lst1 (w : int 32) lst2 e s h ,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w::nil) ++ lst2 ->
(e |--> lst) s h ->
((e |--> lst1) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4)))) |--> lst2)) s h.
Proof.
move=> n lst nj.
move: nj n lst.
elim.
- move=> n lst [] // w lst2 e s h Hlst _ Hwlst2 Hsmh.
rewrite Hwlst2 /= in Hsmh.
move: Hsmh; apply monotony => h' // Hh'.
exists heap.emp; exists h'.
split; first by apply heap.disj_emp_L.
split; first by rewrite heap.union_emp_L.
split.
rewrite /=.
case: Hh' => p [Hp1 Hp2].
by rewrite Hp1 Zmult_comm Z_mod_mult.
move: Hh'; apply mapsto_ext => //.
by rewrite mult_0_r [Z_of_nat _]/= /= add_0.
- move=> n IH n' lst [|hd1 tl1] // w lst2 e s h Hlst; case=> Hlst1 Hlst1wlst2 Hsmh.
rewrite 2!assert_m.con_assoc_equiv.
rewrite Hlst1wlst2 in Hsmh.
case: Hsmh => [hw [htl1wlst2 [H1 [H2 [H3 H4]]]]].
exists hw, htl1wlst2.
split => //.
split => //.
split => //.
move: {IH}(IH (length (tl1 ++ w::lst2)) (tl1 ++ w::lst2) tl1 w lst2 _ s htl1wlst2
(refl_equal ((length (tl1 ++ w::lst2)) )) Hlst1 (refl_equal (tl1 ++ w :: lst2)) H4) => IH.
rewrite assert_m.con_assoc_equiv in IH.
move: IH; apply monotony => // h''.
apply monotony => h' //.
+ apply mapsto_ext => //.
set x := Z_of_nat _. set y := Z_of_nat _.
rewrite /= add_assoc /four32 add_Z2u //; last first.
by apply Zle_0_nat.
repeat f_equal.
rewrite /x /y.
by omegaz.
+ apply mapstos_ext => //.
set x := Z_of_nat _. set y := Z_of_nat _.
rewrite /= add_assoc /four32 add_Z2u //; last first.
by apply Zle_0_nat.
repeat f_equal.
rewrite /x /y.
by omegaz.
Qed.
Lemma mapstos_compose_generic : forall n lst nj lst1 (w : int 32) lst2 e e' e'' s h,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w :: nil) ++ lst2 ->
eval e' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj))))) s ->
eval e'' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s ->
((e |--> lst1) **
(e' |~> int_e w) **
(e'' |--> lst2)) s h ->
(e |--> lst) s h.
Proof.
move=> n lst nj.
move: nj n lst.
elim => //.
- move=> n lst [| _ _] // w lst2 e e' e'' s h Hlenlst _ Hlst He' He'' HP.
rewrite /= in Hlst HP.
rewrite Hlst.
move: HP => /=; apply monotony => h'.
case=> h1 [h2 [Hdisj [Hunion [[Hh11 Hh12] Hh2]]]].
rewrite /emp in Hh12; subst h1.
rewrite heap.union_emp_L in Hunion; subst h'.
move: Hh2; apply mapsto_ext => //.
by rewrite He' mult_0_r [Z_of_nat _]/= /= add_0.
apply mapstos_ext.
by rewrite He'' mult_0_r plus_0_l.
- move=> n IH n' lst [_|hd1 tl1] // w lst2 e e' e'' s h Hlenlst Hlentl1 Hlst He' He'' HP.
case:Hlentl1 => Hlentl1.
rewrite /= in HP *.
rewrite !assert_m.con_assoc_equiv in HP.
case: HP => [h1 [h2 [H7 [H8 [H9 H10 ] ] ] ] ].
rewrite Hlst /=.
exists h1; exists h2; repeat (split => //).
rewrite -!assert_m.con_assoc_equiv in H10.
destruct lst as [| hd tl] => //.
destruct n' as [| n'] => //.
case:Hlenlst => Hlenlst.
apply IH with (n0 := n') (lst1 := tl1) (w := w) (lst2 := lst2) (e' := e') (e'' := e'') => //.
+ case: Hlst=> X Y; subst hd.
by rewrite -Y.
+ rewrite He' [mult]lock /= -lock add_assoc /four32 add_Z2u //; last by apply Zle_0_nat.
repeat f_equal.
by omegaz.
+ rewrite He'' [mult]lock /= -lock add_assoc /four32 add_Z2u //; last by apply Zle_0_nat.
repeat f_equal.
by omegaz.
Qed.
Lemma decompose_equiv : forall l1 nj e w l2, length l1 = nj ->
(e |--> l1 ++ (w :: nil) ++ l2) =
(e |--> l1 **
add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w **
add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4)))) |--> l2).
Proof.
move=> l1 nj e w l2 len_l1.
apply assert_m.assert_ext; split => H.
- eapply mapstos_decompose_generic with (lst := l1 ++ (w :: nil) ++ l2); eauto.
- eapply mapstos_compose_generic with (nj := nj); eauto.
Qed.
Lemma mapstos_compose_last : forall lst1 n lst (w : int 32) nj (e e' : expr) s,
length lst = n -> length lst1 = nj ->
lst = lst1 ++ w::nil ->
eval e' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj))))) s ->
forall h,
((e |--> lst1) ** (e' |~> int_e w)) s h ->
(e |--> lst) s h.
Proof.
move=> lst1 n lst w nj e e' s Hn Hnj Hlst H2 h H3.
move: (mapstos_compose_generic n lst nj lst1 w nil e e' (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s h Hn Hnj Hlst H2 (refl_equal (eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s)) ) => X.
apply X => //; clear X.
exists h; exists heap.emp.
split; first by apply heap.disj_emp_R.
split; first by rewrite heap.union_emp_R.
split; first by assumption.
split; last by done.
case: H3 => h1 [h2 [Hdisj [Hunion [Hh1 [p [Hp1 Hp2]]]]]].
rewrite H2 in Hp1.
rewrite (_ : 0 = 0 mod 4) //.
have X4 : 0 < 4 by done.
apply (proj1 (eqmod_Zmod _ _ _ X4)).
apply eqmod_trans with (u2Z ([ add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) ]e_ s)%mips_expr); last first.
rewrite Hp1.
exists (Z_of_nat p); ring.
rewrite mult_comm /=.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4 + 4)))).
- apply eqmod_div with (2 ^^ 30).
rewrite (_ : 2 ^^ 30 * 4 = 2 ^^ 32) //.
by apply u2Z_add_eqmod.
- apply eqmod_sym.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4)))).
+ apply eqmod_div with (2 ^^ 30).
rewrite (_ : 2 ^^ 30 * 4 = 2 ^^ 32) //.
by apply u2Z_add_eqmod.
+ apply eqmod_sym.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4))) + 4).
* rewrite Zplus_comm.
apply eqmod_sym.
rewrite -Zplus_assoc Zplus_comm.
apply eqmod_compat_plus_R.
rewrite u2Z_Z2u_Zmod; last by apply Zle_0_nat.
rewrite u2Z_Z2u_Zmod; last by apply Zle_0_nat.
apply (proj2 (eqmod_Zmod _ _ _ X4)).
rewrite inj_plus.
rewrite {1}(_ : 4 = 1 * 4) //.
rewrite Z_mod_plus // -Zmod_div_mod //; last by apply Zdivide_intro with (2 ^^ 30).
rewrite -Zmod_div_mod //; last by apply Zdivide_intro with (2 ^^ 30).
by rewrite Zplus_mod /= Z_mod_same_full Zplus_0_r Zmod_mod.
* exists 1; ring.
Qed.
Lemma mapstos_decompose_last_P : forall n lst nj lst1 (w : int 32) e s h P,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w :: nil) ->
(e |--> lst ** P) s h ->
((e |--> lst1) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w) ** P) s h.
Proof.
move=> n lst nj lst1 w e s h P Hlst Hlst1 Hw HP.
rewrite Hw in HP.
case: HP => [h1 [h2 [H5 [H6 [H7 H8] ] ] ] ].
exists h1, h2.
split => //.
split => //.
split => //.
rewrite -Hw in H7.
move: (mapstos_decompose_generic _ _ _ _ _ _ _ _ _ Hlst Hlst1 Hw H7) => XX.
case: XX => h11 [h12 [Hdisj [Hunion [Hh11 Hh12]]]].
rewrite /= in Hh12.
case: Hh12 => Hh12 Hh12'.
rewrite /emp in Hh12'.
subst h12.
rewrite heap.union_emp_R in Hunion.
by subst h11.
Qed.
Lemma decompose_last_equiv2 : forall n e hd tl, length hd = n ->
(e |--> hd ++ tl :: nil) =
(e |--> hd ** add_e e (int_e (Z2u 32 (Z_of_nat (4 * n)))) |~> int_e tl ).
Proof.
move=> n e hd tl Hlen.
apply assert_m.assert_ext; split=> H.
- apply assert_m.con_emp.
eapply mapstos_decompose_last_P; last 2 first.
reflexivity.
by apply assert_m.con_emp'.
reflexivity.
done.
- by eapply mapstos_compose_last; eauto.
Qed.
Lemma decompose_last_equiv : forall e hd tl,
(e |--> hd ++ tl :: nil) =
(e |--> hd ** add_e e (int_e (Z2u 32 (Z_of_nat (4 * (length hd))))) |~> int_e tl ).
Proof.
move=> e hd tl.
apply assert_m.assert_ext; split=> H.
- apply assert_m.con_emp.
eapply mapstos_decompose_last_P; last 2 first.
reflexivity.
by apply assert_m.con_emp'.
reflexivity.
done.
- eapply mapstos_compose_last; last by apply H.
reflexivity.
done.
done.
by rewrite plus_0_r.
Qed.
Require Import ZArith_ext Lists_ext.
Require Import omegaz.
Require Import machine_int.
Import MachineInt.
Require Import mips_bipl.
Local Open Scope Z_scope.
Local Open Scope heap_scope.
Import expr_m.
Import assert_m.
Local Open Scope zarith_ext_scope.
Local Open Scope mips_assert_scope.
Lemma mapstos_decompose_generic : forall n lst nj lst1 (w : int 32) lst2 e s h ,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w::nil) ++ lst2 ->
(e |--> lst) s h ->
((e |--> lst1) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4)))) |--> lst2)) s h.
Proof.
move=> n lst nj.
move: nj n lst.
elim.
- move=> n lst [] // w lst2 e s h Hlst _ Hwlst2 Hsmh.
rewrite Hwlst2 /= in Hsmh.
move: Hsmh; apply monotony => h' // Hh'.
exists heap.emp; exists h'.
split; first by apply heap.disj_emp_L.
split; first by rewrite heap.union_emp_L.
split.
rewrite /=.
case: Hh' => p [Hp1 Hp2].
by rewrite Hp1 Zmult_comm Z_mod_mult.
move: Hh'; apply mapsto_ext => //.
by rewrite mult_0_r [Z_of_nat _]/= /= add_0.
- move=> n IH n' lst [|hd1 tl1] // w lst2 e s h Hlst; case=> Hlst1 Hlst1wlst2 Hsmh.
rewrite 2!assert_m.con_assoc_equiv.
rewrite Hlst1wlst2 in Hsmh.
case: Hsmh => [hw [htl1wlst2 [H1 [H2 [H3 H4]]]]].
exists hw, htl1wlst2.
split => //.
split => //.
split => //.
move: {IH}(IH (length (tl1 ++ w::lst2)) (tl1 ++ w::lst2) tl1 w lst2 _ s htl1wlst2
(refl_equal ((length (tl1 ++ w::lst2)) )) Hlst1 (refl_equal (tl1 ++ w :: lst2)) H4) => IH.
rewrite assert_m.con_assoc_equiv in IH.
move: IH; apply monotony => // h''.
apply monotony => h' //.
+ apply mapsto_ext => //.
set x := Z_of_nat _. set y := Z_of_nat _.
rewrite /= add_assoc /four32 add_Z2u //; last first.
by apply Zle_0_nat.
repeat f_equal.
rewrite /x /y.
by omegaz.
+ apply mapstos_ext => //.
set x := Z_of_nat _. set y := Z_of_nat _.
rewrite /= add_assoc /four32 add_Z2u //; last first.
by apply Zle_0_nat.
repeat f_equal.
rewrite /x /y.
by omegaz.
Qed.
Lemma mapstos_compose_generic : forall n lst nj lst1 (w : int 32) lst2 e e' e'' s h,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w :: nil) ++ lst2 ->
eval e' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj))))) s ->
eval e'' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s ->
((e |--> lst1) **
(e' |~> int_e w) **
(e'' |--> lst2)) s h ->
(e |--> lst) s h.
Proof.
move=> n lst nj.
move: nj n lst.
elim => //.
- move=> n lst [| _ _] // w lst2 e e' e'' s h Hlenlst _ Hlst He' He'' HP.
rewrite /= in Hlst HP.
rewrite Hlst.
move: HP => /=; apply monotony => h'.
case=> h1 [h2 [Hdisj [Hunion [[Hh11 Hh12] Hh2]]]].
rewrite /emp in Hh12; subst h1.
rewrite heap.union_emp_L in Hunion; subst h'.
move: Hh2; apply mapsto_ext => //.
by rewrite He' mult_0_r [Z_of_nat _]/= /= add_0.
apply mapstos_ext.
by rewrite He'' mult_0_r plus_0_l.
- move=> n IH n' lst [_|hd1 tl1] // w lst2 e e' e'' s h Hlenlst Hlentl1 Hlst He' He'' HP.
case:Hlentl1 => Hlentl1.
rewrite /= in HP *.
rewrite !assert_m.con_assoc_equiv in HP.
case: HP => [h1 [h2 [H7 [H8 [H9 H10 ] ] ] ] ].
rewrite Hlst /=.
exists h1; exists h2; repeat (split => //).
rewrite -!assert_m.con_assoc_equiv in H10.
destruct lst as [| hd tl] => //.
destruct n' as [| n'] => //.
case:Hlenlst => Hlenlst.
apply IH with (n0 := n') (lst1 := tl1) (w := w) (lst2 := lst2) (e' := e') (e'' := e'') => //.
+ case: Hlst=> X Y; subst hd.
by rewrite -Y.
+ rewrite He' [mult]lock /= -lock add_assoc /four32 add_Z2u //; last by apply Zle_0_nat.
repeat f_equal.
by omegaz.
+ rewrite He'' [mult]lock /= -lock add_assoc /four32 add_Z2u //; last by apply Zle_0_nat.
repeat f_equal.
by omegaz.
Qed.
Lemma decompose_equiv : forall l1 nj e w l2, length l1 = nj ->
(e |--> l1 ++ (w :: nil) ++ l2) =
(e |--> l1 **
add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w **
add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4)))) |--> l2).
Proof.
move=> l1 nj e w l2 len_l1.
apply assert_m.assert_ext; split => H.
- eapply mapstos_decompose_generic with (lst := l1 ++ (w :: nil) ++ l2); eauto.
- eapply mapstos_compose_generic with (nj := nj); eauto.
Qed.
Lemma mapstos_compose_last : forall lst1 n lst (w : int 32) nj (e e' : expr) s,
length lst = n -> length lst1 = nj ->
lst = lst1 ++ w::nil ->
eval e' s = eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj))))) s ->
forall h,
((e |--> lst1) ** (e' |~> int_e w)) s h ->
(e |--> lst) s h.
Proof.
move=> lst1 n lst w nj e e' s Hn Hnj Hlst H2 h H3.
move: (mapstos_compose_generic n lst nj lst1 w nil e e' (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s h Hn Hnj Hlst H2 (refl_equal (eval (add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj + 4))))) s)) ) => X.
apply X => //; clear X.
exists h; exists heap.emp.
split; first by apply heap.disj_emp_R.
split; first by rewrite heap.union_emp_R.
split; first by assumption.
split; last by done.
case: H3 => h1 [h2 [Hdisj [Hunion [Hh1 [p [Hp1 Hp2]]]]]].
rewrite H2 in Hp1.
rewrite (_ : 0 = 0 mod 4) //.
have X4 : 0 < 4 by done.
apply (proj1 (eqmod_Zmod _ _ _ X4)).
apply eqmod_trans with (u2Z ([ add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) ]e_ s)%mips_expr); last first.
rewrite Hp1.
exists (Z_of_nat p); ring.
rewrite mult_comm /=.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4 + 4)))).
- apply eqmod_div with (2 ^^ 30).
rewrite (_ : 2 ^^ 30 * 4 = 2 ^^ 32) //.
by apply u2Z_add_eqmod.
- apply eqmod_sym.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4)))).
+ apply eqmod_div with (2 ^^ 30).
rewrite (_ : 2 ^^ 30 * 4 = 2 ^^ 32) //.
by apply u2Z_add_eqmod.
+ apply eqmod_sym.
apply eqmod_trans with (u2Z (([ e ]e_ s)%mips_expr) + u2Z (Z2u 32 (Z_of_nat (nj * 4))) + 4).
* rewrite Zplus_comm.
apply eqmod_sym.
rewrite -Zplus_assoc Zplus_comm.
apply eqmod_compat_plus_R.
rewrite u2Z_Z2u_Zmod; last by apply Zle_0_nat.
rewrite u2Z_Z2u_Zmod; last by apply Zle_0_nat.
apply (proj2 (eqmod_Zmod _ _ _ X4)).
rewrite inj_plus.
rewrite {1}(_ : 4 = 1 * 4) //.
rewrite Z_mod_plus // -Zmod_div_mod //; last by apply Zdivide_intro with (2 ^^ 30).
rewrite -Zmod_div_mod //; last by apply Zdivide_intro with (2 ^^ 30).
by rewrite Zplus_mod /= Z_mod_same_full Zplus_0_r Zmod_mod.
* exists 1; ring.
Qed.
Lemma mapstos_decompose_last_P : forall n lst nj lst1 (w : int 32) e s h P,
length lst = n ->
length lst1 = nj ->
lst = lst1 ++ (w :: nil) ->
(e |--> lst ** P) s h ->
((e |--> lst1) **
(add_e e (int_e (Z2u 32 (Z_of_nat (4 * nj)))) |~> int_e w) ** P) s h.
Proof.
move=> n lst nj lst1 w e s h P Hlst Hlst1 Hw HP.
rewrite Hw in HP.
case: HP => [h1 [h2 [H5 [H6 [H7 H8] ] ] ] ].
exists h1, h2.
split => //.
split => //.
split => //.
rewrite -Hw in H7.
move: (mapstos_decompose_generic _ _ _ _ _ _ _ _ _ Hlst Hlst1 Hw H7) => XX.
case: XX => h11 [h12 [Hdisj [Hunion [Hh11 Hh12]]]].
rewrite /= in Hh12.
case: Hh12 => Hh12 Hh12'.
rewrite /emp in Hh12'.
subst h12.
rewrite heap.union_emp_R in Hunion.
by subst h11.
Qed.
Lemma decompose_last_equiv2 : forall n e hd tl, length hd = n ->
(e |--> hd ++ tl :: nil) =
(e |--> hd ** add_e e (int_e (Z2u 32 (Z_of_nat (4 * n)))) |~> int_e tl ).
Proof.
move=> n e hd tl Hlen.
apply assert_m.assert_ext; split=> H.
- apply assert_m.con_emp.
eapply mapstos_decompose_last_P; last 2 first.
reflexivity.
by apply assert_m.con_emp'.
reflexivity.
done.
- by eapply mapstos_compose_last; eauto.
Qed.
Lemma decompose_last_equiv : forall e hd tl,
(e |--> hd ++ tl :: nil) =
(e |--> hd ** add_e e (int_e (Z2u 32 (Z_of_nat (4 * (length hd))))) |~> int_e tl ).
Proof.
move=> e hd tl.
apply assert_m.assert_ext; split=> H.
- apply assert_m.con_emp.
eapply mapstos_decompose_last_P; last 2 first.
reflexivity.
by apply assert_m.con_emp'.
reflexivity.
done.
- eapply mapstos_compose_last; last by apply H.
reflexivity.
done.
done.
by rewrite plus_0_r.
Qed.