Commit 466140ab authored by Ralf Jung's avatar Ralf Jung

Conc, BinOp

parent f5deefa0
......@@ -86,6 +86,12 @@ Proof.
intros Hrel%srel_persistent ??. eapply srel_mono; done.
Qed.
Lemma vrel_core_mono r rf v1 v2 :
vrel r v1 v2 rf core r rf vrel rf v1 v2.
Proof.
intros Hrel%vrel_persistent ??. eapply vrel_mono; done.
Qed.
Lemma rrel_core_mono r rf r1 r2 :
rrel r r1 r2 rf core r rf rrel rf r1 r2.
Proof.
......@@ -203,8 +209,8 @@ Proof.
- eapply IHHwf2. done. }
intros r'' rs' rt' Hrel'.
admit. (* needs call lemma that works with any result. *)
- (* InitCall *) done.
- (* EndCall *) done.
- (* InitCall: can't happen *) done.
- (* EndCall: can't happen *) done.
- (* Proj *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
......@@ -221,9 +227,38 @@ Proof.
specialize (Hrel (Z.to_nat idx)).
rewrite Hidx in Hrel. inversion Hrel. simplify_eq/=.
constructor; last done. auto.
- (* Conc *) admit.
- (* BinOp *) admit.
- (* Place *) done.
- (* Conc *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe1; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
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_conc; [done..|].
intros v1 v2 ??. simplify_eq/=.
do 3 (split; first done). simpl.
apply Forall2_app.
+ eapply vrel_core_mono; first done; auto.
+ eapply vrel_mono; last done; auto.
- (* BinOp *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe1; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
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_bin_op; [done..|].
intros v1 v2 s ? ?? Heval. simplify_eq/=.
do 3 (split; first done). constructor; last done.
assert (arel (core r core r' r'') v1 v1) as Hrel_v1.
{ apply Forall2_cons_inv in Hrel as [??]. auto. }
inversion Heval; simpl; auto; []. do 2 (split; first done).
simplify_eq/=. apply Hrel_v1.
- (* Place: can't happen *) done.
- (* Deref *)
move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..].
......@@ -239,7 +274,7 @@ Proof.
- (* Copy *) admit.
- (* Write *) admit.
- (* Alloc *) admit.
- (* Free *) done.
- (* Free: can't happen *) done.
- (* Retag *) admit.
- (* Let *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
......
......@@ -332,6 +332,13 @@ Lemma sim_simple_conc fs ft r n (r1 r2: result) css cst Φ :
r ⊨ˢ{n,fs,ft} (Conc r1 r2, css) (Conc r1 r2, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_conc; eauto. Qed.
Lemma sim_simple_bin_op fs ft r n op (r1 r2: result) css cst Φ :
( s1 s2 s mem, r1 = ValR [s1] r2 = ValR [s2]
bin_op_eval mem op s1 s2 s
Φ r n (ValR [s]) css (ValR [s]) cst : Prop)
r ⊨ˢ{n,fs,ft} (BinOp op r1 r2, css) (BinOp op r1 r2, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_bin_op; eauto. Qed.
Lemma sim_simple_case fs ft r n (rc: result) els elt css cst Φ :
length els = length elt
( (es et: expr) (i: Z), 0 i
......
......@@ -25,11 +25,11 @@ Ltac reshape_expr e tac :=
| Proj ?e1 ?e2 => go (ProjLCtx e2 :: K) e1
| Conc (Val ?v1) ?e2 => go (ConcRCtx (ValR v1) :: K) e2
| Conc (of_result ?r1) ?e2 => go (ConcRCtx r1 :: K) e2
| Conc ?e1 ?e2 => go (ConcLCtx op e2 :: K) e1
| Conc ?e1 ?e2 => go (ConcLCtx e2 :: K) e1
| Copy ?e => go (CopyCtx :: K) e
| Write (Place ?l1 ?tg ?ty) ?e2 => go (WriteRCtx (PlaceR l1 tg ty) :: K) e2
| Write (of_result ?r1) ?e2 => go (WriteRCtx r1 :: K) e2
| Write ?e1 ?e2 => go (WriteLCtx op e2 :: K) e1
| Write ?e1 ?e2 => go (WriteLCtx e2 :: K) e1
| Free ?e => go (FreeCtx :: K) e
| Deref ?e ?T => go (DerefCtx T :: K) e
| Ref ?e => go (RefCtx :: K) e
......
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