proposition: Lemma reads_from_clock: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(l l': Label)(n: NId), (step_star (init p) h s /\ prec h l l' /\ label_is_put l /\ label_is_get l' /\ label_node l = label_orig_node l' /\ label_clock l = label_clock l' /\ In n nids) -> (let c := clock (label_post_state l) n in let c' := clock (label_post_state l') n in c <= c').
proof: Proof. intros p h s l l' ni. intros. destruct H as [H [H0 [H2 [H3 [H4 [H5 Hi]]]]]]. apply prec_in in H0. destruct H0 as [H0 H1]. assert (L := in_exec h (init p) s l' (conj H H1)). destruct L as [h1 [s1 [s2 [h2 L]]]]. open_conjs. assert (L := get_from_map s1 s2 l' (conj H3 H8)). pose (k := label_key l'). pose (n := label_node l'). assert (M := in_map_from_put_update p h1 s1 k n H7). destruct M as [M | M]. simpl in L. subst k. remember (label_key l') as k eqn: Hk . subst n. remember (label_node l') as n eqn: Hn . open_conjs. clear H12 H10. rewrite H11 in H13. clear H11. rewrite <- H5 in H13. assert (L := put_clock_gtz p h s l). depremise L. split_all; assumption. rewrite H13 in L. inversion L. destruct M as [lw [M | M]]; open_conjs. simpl in L. open_conjs. subst k. remember (label_key l') as k eqn: Hk. subst n. remember (label_node l') as n eqn: Hn. remember (alg_state (node_states s1 n)) as as1 eqn: A. rewrite <- H12 in *. clear H12. rewrite <- H13 in *. clear H13. rewrite <- H4 in *. rewrite <- H5 in *. assert (L := put_unique p h s l lw). depremise L. split_all. assumption. assumption. rewrite H6. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. subst lw. clear H11 H15 H16. subst c. subst c'. apply in_split in H10. destruct H10 as [h11 [h12 H10]]. rewrite H10 in H7. apply step_star_app in H7. destruct H7 as [s0 [H71 H72]]. apply step_star_end in H72. destruct H72 as [s0' [H72 H73]]. assert (N1 := label_poststate_state s0 s0' l H72). assert (N2 := label_poststate_state s1 s2 l' H8). rewrite N1; clear N1. rewrite N2; clear N2. rewrite H14 in *; rewrite <- Hn in *. assert (L := step_star_clock_nondec (h12 ++ [l']) s0' s2 n). simpl in L. depremise L. apply step_star_app_one. exists s1. split; assumption. specialize (L ni). assumption. simpl in L. open_conjs. subst k. remember (label_key l') as k eqn: Hk. subst n. remember (label_node l') as n eqn: Hn. remember (alg_state (node_states s1 n)) as as1 eqn: A. rewrite <- H12 in *. clear H12. rewrite <- H13 in *. clear H13. assert (L := in_exec h1 (init p) s1 lw (conj H7 H10)). destruct L as [h2' [s2' [s3' [h3' [L1 [L2 [L3 L4]]]]]]]. assert (M := update_clock s2' s3' lw (conj L3 H11)). simpl in M. destruct M as [m [M1 [M2 [M3 [M4 M5]]]]]. assert (N := message_pre_put p h2' s2' m). simpl in N. depremise N. split; assumption. destruct N as [lp [N1 [N2 [N3 [N4 N5]]]]]. assert (P := put_unique p h s l lp). depremise P. split_all. assumption. assumption. rewrite H6. apply in_app_iff. left. rewrite L1. apply in_app_iff. left. assumption. assumption. assumption. rewrite H4. rewrite H15. rewrite M2. rewrite N3. reflexivity. rewrite H5. rewrite H16. rewrite M3. rewrite N4. reflexivity. rewrite <- P in *. subst c. subst c'. rewrite <- N5. specialize (M5 ni). depremise M5. assumption. assert (E: clock (label_post_state lw) ni <= clock (label_post_state l') ni). assert (R := label_poststate_state s2' s3' lw L3); rewrite R; clear R. assert (R := label_poststate_state s1 s2 l' H8); rewrite R; clear R. rewrite H14. rewrite <- Hn. apply step_star_clock_nondec with (h := (h3' ++ [l'])). apply step_star_app_one. exists s1. split; assumption. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)