Commit d9a5618d authored by Ralf Jung's avatar Ralf Jung

consistent lemma naming: unique for lemmas thta need tkUnique; public for lemmas that don't

parent 6db2900a
......@@ -61,7 +61,7 @@ Proof.
sim_apply sim_simple_deref=>l' t' ?. simplify_eq/=.
(* Write unique. We need to drop to complex mode, to preserve some local state info. *)
intros σs σt Hσs Hσt.
sim_apply sim_body_write_owned; [solve_sim..|].
sim_apply sim_body_write_unique; [solve_sim..|].
intros ???? Htop. simplify_eq/=.
sim_apply sim_body_let. simplify_eq/=.
(* Copy local (right) *)
......
......@@ -268,7 +268,7 @@ Proof using Type*.
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
eapply sim_simple_valid_post.
eapply sim_simple_copy_shared; [by auto..|].
eapply sim_simple_copy_public; [by auto..|].
intros r'' v1 v2 Hrel'' Hval. simplify_eq/=.
do 3 (split; first done). auto.
- (* Write *)
......@@ -280,12 +280,12 @@ Proof using Type*.
eapply sim_simple_frame_more_core.
eapply sim_simple_post_mono, IHe2; [|by auto..].
intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
simplify_eq/=. eapply sim_simple_write_shared; [auto..|].
simplify_eq/=. eapply sim_simple_write_public; [auto..|].
do 3 (split; first done). constructor; done.
- (* Alloc *)
move=>Hwf xs Hxswf /=.
eapply sim_simple_valid_post.
eapply sim_simple_alloc_shared=>l tg /= Hval.
eapply sim_simple_alloc_public=>l tg /= Hval.
do 3 (split; first done).
simpl. split; last done. constructor; last done.
eapply arel_mono, arel_ptr; auto.
......@@ -294,7 +294,7 @@ Proof using Type*.
move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
eapply sim_simple_retag_shared; [by auto..|].
eapply sim_simple_retag_public; [by auto..|].
do 3 (split; first done). constructor; done.
- (* Let *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
......
......@@ -941,7 +941,7 @@ Proof.
Qed.
(** can probably be derived from [write_related_values]? *)
Lemma sim_body_write_owned
Lemma sim_body_write_unique
fs ft (r r' r'' rs: resUR) h n l tg T s σs σt Φ:
tsize T = 1%nat
r r' res_tag tg tkUnique h
......
......@@ -319,7 +319,7 @@ Proof.
Admitted.
(** * Memory: shared *)
Lemma sim_simple_alloc_shared fs ft r n T css cst Φ :
Lemma sim_simple_alloc_public fs ft r n T css cst Φ :
( (l: loc) (tg: nat),
let rt := res_tag tg tkPub in
Φ (r rt) n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst)
......@@ -327,7 +327,7 @@ Lemma sim_simple_alloc_shared fs ft r n T css cst Φ :
Proof.
Admitted.
Lemma sim_simple_write_shared fs ft r n (rs1 rs2 rt1 rt2: result) css cst Φ :
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) css cst Φ :
rrel r rs1 rt1
rrel r rs2 rt2
Φ r n (ValR [%S]) css (ValR [%S]) cst
......@@ -339,7 +339,7 @@ Proof.
Qed.
Lemma sim_simple_copy_shared fs ft r n (rs rt: result) css cst Φ :
Lemma sim_simple_copy_public fs ft r n (rs rt: result) css cst Φ :
rrel r rs rt
( r' (v1 v2: value),
(* this post-condition is weak, we can return related values *)
......@@ -351,7 +351,7 @@ Proof.
eapply sim_body_copy_public; eauto.
Qed.
Lemma sim_simple_retag_shared fs ft r n (rs rt: result) k css cst Φ :
Lemma sim_simple_retag_public fs ft r n (rs rt: result) k css cst Φ :
rrel r rs rt
(Φ r n (ValR [%S]) css (ValR [%S]) cst)
r ⊨ˢ{n,fs,ft} (Retag rs k, css) (Retag rt k, cst) : Φ.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment