Require Import ZArith. Require Import List. Require Import util. Require Import machine_int. Import MachineInt. Require Import state. Require Import mips. Require Import mips_tactics. Open Local Scope asm_heap_scope. Open Local Scope mips_scope. Open Local Scope Z_scope. Lemma mapstos_decompose_generic : forall nj lst1 (w:int 32) lst2 n lst (e e' e'':expr) s, length lst = n -> length lst1 = nj -> lst = lst1 ++ (w::nil) ++ lst2 -> forall s' m h, u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 /\ eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\ eval e'' s = eval (add_e e' (int_e four32)) s -> (e |--> lst) s s' m h -> ((e |--> lst1) ** (e' |-> int_e w) ** (e'' |--> lst2)) s s' m h. induction nj. intros; destruct lst1; try discriminate. simpl. clear H0. simpl in H1. subst lst. rewrite sep.con_assoc_equiv. rewrite sep.con_com_equiv. rewrite sep.con_emp_equiv. simpl in H3. Decompose_sepcon H3 h1 h2. exists h1; exists h2. split; trivial. split; trivial. split. generalize H3; clear H3; apply mapsto_ext'. decompose [and] H2; clear H2. rewrite H5. simpl. unfold shl2. rewrite shl_zero. rewrite add_neutral. reflexivity. reflexivity. generalize H6; clear H6; apply mapstos_ext'. simpl. decompose [and] H2; clear H2. rewrite H7. simpl. rewrite H6. simpl. unfold shl2. rewrite shl_zero. rewrite add_neutral. reflexivity. intros. destruct lst1; try discriminate. simpl in H0; injection H0; clear H0; intro. destruct lst; try discriminate. simpl in H1; injection H1; clear H1; intros. subst i0. destruct n; try discriminate. simpl in H; injection H; clear H; intro. assert (Htmp: Z_of_nat nj + 1 <= Z_of_nat n). rewrite <-H. rewrite H1. rewrite length_app. rewrite inj_plus. rewrite H0. simpl length. rewrite Z_S. omega. (*end of assert*) simpl in H3. Decompose_sepcon H3 h1 h2. rewrite H1 in H8. lapply (IHnj lst1 w lst2 (length (lst1 ++ (w :: nil) ++ lst2)) (lst1 ++ (w :: nil) ++ lst2) (add_e e (int_e four32)) (add_e (add_e e (int_e four32)) (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) (add_e (add_e (add_e e (int_e four32)) (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) (int_e four32)) s (refl_equal (length (lst1 ++ (w :: nil) ++ lst2))) H0 (refl_equal (lst1 ++ (w :: nil) ++ lst2)) s' m h2). intro. simpl in H3. generalize (H3 H8); clear H3; intro. simpl. Decompose_sepcon H3 h21 h22. Decompose_sepcon H9 h211 h212. simpl. exists (h1 +++ h21); exists h22. split. Disjoint_heap. split. Equal_heap. split. exists (h1 +++ h211); exists h212. split. Disjoint_heap. split. Equal_heap. split. exists h1; exists h211. split. Disjoint_heap. split. reflexivity. split; trivial. generalize H15; clear H15; apply mapsto_ext'. simpl. decompose [and] H2; clear H2. rewrite H15. simpl. rewrite add_assoc. rewrite <-shl_S. cutrewrite (1=Z_of_nat 1). rewrite <-inj_plus. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. cutrewrite (S nj = nj + 1)%nat. reflexivity. rewrite S_to_plus_one. rewrite plus_comm. reflexivity. reflexivity. apply Zle_0_nat. Mult 2%nat. omega. Clean_beta1. rewrite Z_S in H9. generalize (min_u2Z (eval e s)); intro. omega. reflexivity. generalize H12; clear H12; apply mapstos_ext'. simpl. decompose [and] H2; clear H2. rewrite H16. simpl. rewrite H14. simpl. cutrewrite ( ((eval e s) (+) (shl2 (Z2u 32 (Zpos (P_of_succ_nat nj))))) = (((eval e s) (+) four32) (+) (shl2 (Z2u 32 (Z_of_nat nj)))) ). reflexivity. rewrite add_assoc. rewrite <-shl_S. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. cutrewrite (S nj = nj + 1)%nat. repeat rewrite inj_plus. simpl. reflexivity. rewrite S_to_plus_one. rewrite plus_comm. reflexivity. apply Zle_0_nat. Mult 2%nat. omega. Clean_beta1. rewrite Z_S in H9. generalize (min_u2Z (eval e s)); intro. omega. simpl eval. simpl length. rewrite <-H1. rewrite H. split. unfold four32. rewrite add_u2Z. rewrite Z2u_injection. rewrite Z_S in H2. omega. Constraint. rewrite Z2u_injection. rewrite Z_S in H2. decompose [and] H2; clear H2. Constraint_variable. Constraint. split. reflexivity. reflexivity. Qed. Lemma mapstos_compose_generic : forall nj lst1 (w:int 32) lst2 n lst (e e' e'':expr) s, length lst = n -> length lst1 = nj -> lst = lst1 ++ (w::nil) ++ lst2 -> forall s' m h, u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 /\ eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\ eval e'' s = eval (add_e e' (int_e four32)) s -> ((e |--> lst1) ** (e' |-> int_e w) ** (e'' |--> lst2)) s s' m h -> (e |--> lst) s s' m h. induction nj. intros; destruct lst1; try discriminate. clear H0. simpl in H1. simpl in H3. destruct lst; try discriminate. injection H1; clear H1; intros; subst i lst2. simpl. rewrite sep.con_assoc_equiv in H3. rewrite sep.con_com_equiv in H3. rewrite sep.con_emp_equiv in H3. Decompose_sepcon H3 h1 h2. exists h1; exists h2. split; trivial. split; trivial. split. generalize H3; clear H3; apply mapsto_ext'. decompose [and] H2; clear H2. rewrite H5. simpl. unfold shl2. rewrite shl_zero. rewrite add_neutral. reflexivity. reflexivity. generalize H6; clear H6; apply mapstos_ext'. simpl. decompose [and] H2; clear H2. rewrite H7. simpl. rewrite H6. simpl. unfold shl2. rewrite shl_zero. rewrite add_neutral. reflexivity. intros. destruct lst1; try discriminate. simpl in H0; injection H0; clear H0; intro. destruct lst; try discriminate. simpl in H1; injection H1; clear H1; intros; subst i0. simpl. simpl in H3. Decompose_sepcon H3 h1 h2. Decompose_sepcon H5 h11 h12. Decompose_sepcon H7 h111 h112. exists h111; exists (h112 +++ h12 +++ h2). split. Disjoint_heap. split. Equal_heap. split; trivial. destruct n; try discriminate. simpl in H; injection H; clear H; intro. apply IHnj with (n:=n) (lst1:=lst1) (w:=w) (lst2:=lst2) (e:=add_e e (int_e four32)) (e':=add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat (S nj)))))) (e'':=add_e (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat (S nj)))))) (int_e four32)); auto. simpl eval. decompose [and] H2; clear H2. rewrite Z_S in H7. split. unfold four32. rewrite add_u2Z. rewrite Z2u_injection. omega. Constraint. rewrite Z2u_injection. Constraint_variable. Constraint. split. rewrite add_assoc. rewrite <-shl_S. rewrite <-Z_of_nat_Zpos_P_of_succ_nat. rewrite inj_plus. simpl Z_of_nat. reflexivity. Constraint_constant. Mult 2%nat. omega. Clean_beta1. apply Zle_lt_trans with (4 * (Z_of_nat n + 1)). rewrite <-H. rewrite H1. rewrite length_app. simpl length. rewrite H0. rewrite inj_plus. omega. generalize (min_u2Z (eval e s)). omega. reflexivity. exists (h112 +++ h12); exists h2. split. Disjoint_heap. split. Equal_heap. split. exists h112; exists h12. split. Disjoint_heap. split. Equal_heap. split. auto. generalize H11; clear H11; apply mapsto_ext'. simpl. decompose [and] H2; clear H2. rewrite H13. simpl. reflexivity. reflexivity. generalize H8; clear H8; apply mapstos_ext'. simpl. decompose [and] H2; clear H2. rewrite H15. simpl. rewrite H13. simpl. reflexivity. Qed. Lemma mapstos_decompose_last : forall lst1 n lst (w:int 32) nj (e e':expr) s, length lst = n -> length lst1 = nj -> lst = lst1 ++ (w::nil) -> u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 /\ eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s -> forall s' m0 h, (e |--> lst) s s' m0 h -> ((e |--> lst1) ** (e' |-> int_e w)) s s' m0 h. intros. lapply (mapstos_decompose_generic nj lst1 w nil n lst e e' (add_e e' (int_e four32)) s H H0 H1 s' m0 h). intros. generalize (H4 H3); clear H4; intro H4. simpl in H4. rewrite sep.con_emp_equiv in H4. assumption. inversion_clear H2. split; trivial. simpl. split. rewrite H5. simpl. reflexivity. reflexivity. 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 -> u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 /\ eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s -> forall s' m0 h, ((e |--> lst1) ** (e' |-> int_e w)) s s' m0 h -> (e |--> lst) s s' m0 h. intros. eapply mapstos_compose_generic with (e':=e') (e'':=add_e e' (int_e four32)). apply H. apply H0. simpl. apply H1. inversion_clear H2. split; trivial. simpl. rewrite H5. simpl. split; reflexivity. simpl. rewrite sep.con_emp_equiv. assumption. Qed. Lemma mapstos_decompose_generic_P : forall nj lst1 (w:int 32) lst2 n lst (e e' e'':expr) s P, length lst = n -> length lst1 = nj -> lst = lst1 ++ (w::nil) ++ lst2 -> forall s' m h, u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 /\ eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\ eval e'' s = eval (add_e e' (int_e four32)) s -> (e |--> lst ** P) s s' m h -> ((e |--> lst1) ** (e' |-> int_e w) ** (e'' |--> lst2) ** P) s s' m h. intros. Decompose_sepcon H3 h1 h2. exists h1; exists h2. split; auto. split; auto. split; auto. eapply mapstos_decompose_generic. apply H. apply H0. auto. auto. auto. Qed. Lemma mapstos_decompose_app: forall nj lst1 lst2 n lst (e e':expr) s, length lst = n -> length lst1 = nj -> lst = lst1 ++ lst2 -> forall s' m h, u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 -> eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s -> (e |--> lst) s s' m h -> ((e |--> lst1) ** (e' |--> lst2)) s s' m h. intros. destruct lst2. rewrite <-app_nil_end in H1. subst lst1. simpl. generalize H4. apply sep.con_emp'. simpl. rewrite <-sep.con_assoc_equiv. eapply mapstos_decompose_generic. apply H. apply H0. simpl. assumption. split. assumption. split. assumption. reflexivity. assumption. Qed. Lemma mapstos_compose_app: forall nj lst1 lst2 n lst (e e':expr) s, length lst = n -> length lst1 = nj -> lst = lst1 ++ lst2 -> forall s' m h, u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 -> eval e' s = eval (add_e e (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s -> ((e |--> lst1) ** (e' |--> lst2)) s s' m h -> (e |--> lst) s s' m h. intros. destruct lst2. rewrite <-app_nil_end in H1. subst lst1. simpl in H4. generalize H4. apply sep.con_emp. eapply mapstos_compose_generic. apply H. apply H0. simpl. apply H1. split. assumption. split. apply H3. reflexivity. simpl in H4. rewrite sep.con_assoc_equiv. assumption. Qed. (* TODO: not used anywhere *) Lemma mapstos_lookup : forall n lst v s s' m h na, (int_e v |--> lst) s s' m h -> length lst = S n -> u2Z v = 4 * Z_of_nat na -> (4 * Z_of_nat na + 4 * Z_of_nat n < Zpower 2 32) -> forall nj, (nj <= n)%nat -> forall def_val, heap.lookup (na + nj)%nat h = Some (nth nj lst def_val). induction n. intros. destruct lst; try discriminate. destruct lst; try discriminate. simpl in H. rewrite sep.con_emp_equiv in H. destruct nj. simpl. rewrite <-plus_n_O. inversion_clear H. inversion_clear H4. rewrite H5. simpl eval in H. assert (Z_of_nat x = Z_of_nat na). omega. generalize (Z_of_nat_inj _ _ H4); clear H4; intro. subst x. apply heap.lookup_singleton. inversion H3. intros. destruct lst; try discriminate. simpl in H0; injection H0; clear H0; intro. simpl in H. destruct nj. simpl. rewrite <-plus_n_O. Decompose_sepcon H h1 h2. rewrite H6. apply heap.lookup_union. auto. inversion_clear H5. inversion_clear H. rewrite H7. simpl eval in H5. assert (Z_of_nat na = Z_of_nat x). omega. generalize (Z_of_nat_inj _ _ H); clear H; intro. subst x. apply heap.lookup_singleton. Decompose_sepcon H h1 h2. generalize (IHn lst (v (+) four32) s s' m h2 (na+1)%nat); intro. assert ((int_e (v (+) four32) |--> lst) s s' m h2). generalize H8; apply mapstos_ext'. auto. simpl. assert ( u2Z (v (+) four32) = 4 * (Z_of_nat (na + 1)) ). rewrite add_u2Z. simpl (u2Z four32). unfold four32. rewrite Z2u_injection. rewrite inj_plus. simpl (Z_of_nat 1). omega. cutrewrite (4=Zpower 2 2). split. simpl; omega. apply Zpower_2_lt. omega. auto. unfold four32. rewrite Z2u_injection. rewrite H1. rewrite S_to_plus_one in H2. rewrite inj_plus in H2. simpl (Z_of_nat 1) in H2. omega. cutrewrite (4=Zpower 2 2). split. simpl; omega. apply Zpower_2_lt. omega. auto. assert (nj<=n)%nat. omega. assert ( 4 * Z_of_nat (na + 1) + 4 * Z_of_nat n < Zpower 2 32 ). rewrite S_to_plus_one in H2. rewrite inj_plus in H2. rewrite inj_plus. omega. generalize (H H7 H0 H9 H11 nj H10 def_val); intro. rewrite H6. apply heap.lookup_union_R. auto. cutrewrite (na + S nj = na + 1 + nj)%nat; try auto||omega. Qed.