Commit cfb700e9 authored by Ralf Jung's avatar Ralf Jung

state some stubs; add rrel abbreviation

parent 1f699d7a
......@@ -9,6 +9,8 @@ Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
Notation "r |==> r'" := (viewshift wsat r r') (at level 65, format "r |==> r'").
Notation rrel := (rrel vrel).
(** "modular" simulation relations dont make assumptions
about the global fn table.
This is very weak! A stronger version would, instead of universally quantifying the
......@@ -90,7 +92,7 @@ Qed.
(** Result relation properties *)
Lemma rrel_eq r (e1 e2: result) :
rrel vrel r e1 e2 e1 = e2.
rrel r e1 e2 e1 = e2.
Proof.
destruct e1, e2; simpl; [|done..|].
- intros ?. f_equal. by eapply vrel_eq.
......@@ -98,17 +100,27 @@ Proof.
Qed.
Lemma vrel_rrel r (v1 v2 : value) :
vrel r v1 v2 rrel vrel r #v1 #v2.
vrel r v1 v2 rrel r #v1 #v2.
Proof. done. Qed.
Lemma rrel_persistent r rs rt :
rrel r rs rt rrel (core r) rs rt.
Proof. destruct rs, rt; simpl; naive_solver eauto using vrel_persistent. Qed.
Lemma rrel_mono (r1 r2 : resUR) (VAL: r2) :
r1 r2 v1 v2, rrel vrel r1 v1 v2 rrel vrel r2 v1 v2.
r1 r2 v1 v2, rrel r1 v1 v2 rrel r2 v1 v2.
Proof.
intros Le v1 v2. destruct v1, v2; simpl; [|done..|].
- by apply vrel_mono.
- intros [VREL ?]. split; [|done]. move : VREL. by apply vrel_mono.
Qed.
Lemma rrel_with_eq r rs rt :
rrel r rs rt rrel r rs rt rs = rt.
Proof.
intros. split; first done. exact: rrel_eq.
Qed.
Lemma list_Forall_result_value (es: list result) (vs: list value) :
of_result <$> es = Val <$> vs es = ValR <$> vs.
Proof.
......@@ -126,7 +138,7 @@ Lemma list_Forall_result_value_2 (vs: list value) :
Proof. by rewrite -list_fmap_compose. Qed.
Lemma list_Forall_rrel_vrel r (es et: list result) :
Forall2 (rrel vrel r) es et
Forall2 (rrel r) es et
Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> es)
Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et)
vs vt, es = ValR <$> vs et = ValR <$> vt
......@@ -141,11 +153,11 @@ Proof.
Qed.
Lemma rrel_to_value r (v1: value) e2:
rrel vrel r #v1 e2 (v2: value), e2 = v2.
rrel r #v1 e2 (v2: value), e2 = v2.
Proof. destruct e2; [|done]. by eexists. Qed.
Lemma list_Forall_rrel_to_value r vs et :
Forall2 (rrel vrel r) (ValR <$> vs) et
Forall2 (rrel r) (ValR <$> vs) et
vt, et = ValR <$> vt Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et).
Proof.
revert vs. induction et as [|e et IH]; intros vs.
......@@ -159,7 +171,7 @@ Proof.
Qed.
Lemma list_Forall_rrel_vrel_2 r (es et: list result) :
Forall2 (rrel vrel r) es et
Forall2 (rrel r) es et
Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> es)
vs vt, es = ValR <$> vs et = ValR <$> vt
Forall (λ ei : expr, is_Some (to_value ei)) (of_result <$> et)
......@@ -174,7 +186,7 @@ Proof.
Qed.
Lemma list_Forall_rrel_vrel_3 r (vs: list value) (et: list result) :
Forall2 (rrel vrel r) (ValR <$> vs) et
Forall2 (rrel r) (ValR <$> vs) et
Forall (λ ei : expr, is_Some (to_value ei)) (Val <$> vs)
vt, et = ValR <$> vt
Forall (λ ei : expr, is_Some (to_value ei)) (Val <$> vt)
......
......@@ -54,7 +54,7 @@ Inductive sim_local_frames:
(fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
(λ r _ vs σs vt σt,
( c, σt.(scs) = c :: cids end_call_sat r c)
rrel vrel r vs vt))
rrel r vs vt))
: sim_local_frames
(r_f frame.(rc))
frame.(callids)
......@@ -73,7 +73,7 @@ Inductive sim_local_conf:
(LOCAL: sim_local_body wsat vrel fns fnt rc idx e_src σ_src e_tgt σ_tgt
(λ r _ vs σs vt σt,
( c, σt.(scs) = c :: cids end_call_sat r c)
rrel vrel r vs vt))
rrel r vs vt))
(KE_SRC: Ke_src = fill K_src e_src)
(KE_TGT: Ke_tgt = fill K_tgt e_tgt)
(WSAT: wsat (r_f rc) σ_src σ_tgt)
......@@ -134,7 +134,7 @@ Proof.
simplify_eq.
set Φ : resUR nat result state result state Prop :=
λ r2 _ vs2 σs2 vt2 σt2, rrel vrel r2 vs2 vt2
λ r2 _ vs2 σs2 vt2 σt2, rrel r2 vs2 vt2
c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1
σt.(scs) = c2 :: cids2
σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc)
......
......@@ -32,7 +32,7 @@ Proof.
intros. simpl. exists 1%nat.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
intros VALID.
have ?: rrel vrel (init_res r') vs vt.
have ?: rrel (init_res r') vs vt.
{ eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }
split; [|done].
exists O. split; [by rewrite -STACKT|].
......
......@@ -43,28 +43,11 @@ Definition prog_wf (prog: fn_env) :=
Section sem.
Context (fs ft: fn_env) `{!sim_local_funs_lookup fs ft}.
Context (css cst: call_id_stack).
Notation rrel := (rrel vrel).
(** Helper lemmas *)
Lemma rrel_with_eq r rs rt :
rrel r rs rt rrel r rs rt rs = rt.
Proof.
intros. split; first done. exact: rrel_eq.
Qed.
(** Well-formed two-substitutions. *)
Definition srel (r: resUR) (xs: gmap string (result * result)) : Prop :=
map_Forall (λ _ '(rs, rt), rrel r rs rt) xs.
Lemma rrel_persistent r rs rt :
rrel r rs rt rrel (core r) rs rt.
Proof. destruct rs, rt; simpl; naive_solver eauto using vrel_persistent. Qed.
Lemma rrel_mono r1 r2 rs rt :
r2 r1 r2
rrel r1 rs rt rrel r2 rs rt.
Proof. destruct rs, rt; simpl; intros; naive_solver eauto using vrel_mono. Qed.
Lemma srel_persistent r xs :
srel r xs srel (core r) xs.
Proof.
......@@ -326,7 +309,7 @@ Proof.
apply: res_end_call_sat; first done. exact: cmra_included_r.
- eapply rrel_mono; [done| |done]. exact: cmra_included_l.
}
destruct (subst_l_map _ _ _ _ _ _ _ (rrel vrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
destruct (subst_l_map _ _ _ _ _ _ _ (rrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
{ clear -Hrel. induction Hrel; eauto using Forall2. }
eapply sim_simplify, expr_wf_soundness; done.
Qed.
......
......@@ -1222,7 +1222,7 @@ Qed.
(** EndCall *)
Lemma end_call_tstep_src_tgt fs ft r_f r σs σt (rs rt: result) es' σs' :
rrel vrel r rs rt
rrel r rs rt
wsat (r_f r) σs σt
(EndCall rs, σs) ~{fs}~> (es', σs')
vs vt : value, rs = ValR vs rt = ValR vt reducible ft (EndCall rt) σt.
......@@ -1242,7 +1242,7 @@ Qed.
Lemma sim_body_end_call fs ft r n rs rt σs σt Φ :
(* return values are related *)
rrel vrel r rs rt
rrel r rs rt
(* The top of the call stack has no privately protected locations left *)
( c cids, σt.(scs) = c :: cids end_call_sat r c)
( c1 c2 cids1 cids2 vs vt,
......
......@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
(** Call - step over *)
Lemma sim_body_step_over_call fs ft
rc rv n fid rls rlt σs σt Φ
(RREL: Forall2 (rrel vrel rv) rls rlt)
(RREL: Forall2 (rrel rv) rls rlt)
(FUNS: sim_local_funs_lookup fs ft) :
( r' vls vlt vs vt σs' σt' (VRET: vrel r' vs vt)
(STACKS: σs.(scs) = σs'.(scs))
......
......@@ -13,7 +13,7 @@ From stbor.sim Require Import refl_step.
Definition fun_post_simple
initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
( c, cst = c::initial_call_id_stack end_call_sat r c)
rrel vrel r vs vt.
rrel r vs vt.
Definition sim_simple fs ft r n es css et cst
(Φ : resUR nat result call_id_stack result call_id_stack Prop) : Prop :=
......@@ -228,7 +228,7 @@ Qed.
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' rls rlt rv fs ft r r' n fid css cst Φ :
sim_local_funs_lookup fs ft
Forall2 (rrel vrel rv) rls rlt
Forall2 (rrel rv) rls rlt
r r' rv
( rret vs vt vls vlt,
rls = ValR <$> vls rlt = ValR <$> vlt
......@@ -244,7 +244,7 @@ Proof.
- intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.
Qed.
(** * Memory *)
(** * Memory: local *)
Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
( (l: loc) (tg: nat),
let rt := res_tag tg tkUnique in
......@@ -264,6 +264,26 @@ Lemma sim_simple_write_local fs ft r r' n l tg ty v v' css cst Φ :
: Φ.
Proof. intros Hty Hres HH σs σt <-<-. eapply sim_body_write_local_1; eauto. Qed.
Lemma sim_simple_read_local_l fs ft r r' n l tg ty s et css cst Φ :
tsize ty = 1%nat
r r' res_mapsto l 1 s tg
(r ⊨ˢ{n,fs,ft} (#[s], css) (et, cst) : Φ)
r ⊨ˢ{n,fs,ft}
(Copy (Place l (Tagged tg) ty), css) (et, cst)
: Φ.
Proof.
Admitted.
Lemma sim_simple_read_local_r fs ft r r' n l tg ty s es css cst Φ :
tsize ty = 1%nat
r r' res_mapsto l 1 s tg
(r ⊨ˢ{n,fs,ft} (es, css) (#[s], cst) : Φ)
r ⊨ˢ{n,fs,ft}
(es, css) (Copy (Place l (Tagged tg) ty), cst)
: Φ.
Proof.
Admitted.
Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ :
r r' res_mapsto l 1 s tg
arel rs s' s
......@@ -286,6 +306,42 @@ Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ :
Proof.
Admitted.
(** * Memory: shared *)
Lemma sim_simple_alloc_shared 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)
r ⊨ˢ{n,fs,ft} (Alloc T, css) (Alloc T, cst) : Φ.
Proof.
Admitted.
Lemma sim_simple_write_shared 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
r ⊨ˢ{n,fs,ft} (rs1 <- rs2, css) (rt1 <- rt2, cst) : Φ.
Proof.
intros [Hrel1 ?]%rrel_with_eq [Hrel2 ?]%rrel_with_eq. simplify_eq.
Admitted.
Lemma sim_simple_read_shared fs ft r n (rs rt: result) css cst Φ :
rrel r rs rt
( r' (v1 v2: result),
rrel r' v1 v2
Φ (r r') n v1 css v2 cst)
r ⊨ˢ{n,fs,ft} (Copy rs, css) (Copy rt, cst) : Φ.
Proof.
intros [Hrel ?]%rrel_with_eq. simplify_eq.
Admitted.
Lemma sim_simple_retag_shared 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) : Φ.
Proof.
intros [Hrel ?]%rrel_with_eq. simplify_eq.
Admitted.
(** * Pure *)
Lemma sim_simple_let fs ft r n x (vs1 vt1: expr) es2 et2 css cst Φ :
terminal vs1 terminal vt1
......
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