Commit 973be934 authored by Ralf Jung's avatar Ralf Jung

lots of stubs for ex1

parent e1bfea41
...@@ -53,7 +53,7 @@ Notation "'Box<' T '>'" := (Reference RawPtr T%T) ...@@ -53,7 +53,7 @@ Notation "'Box<' T '>'" := (Reference RawPtr T%T)
(** Pointer operations *) (** Pointer operations *)
Notation "& e" := (Ref e%E) (at level 8, format "& e") : expr_scope. Notation "& e" := (Ref e%E) (at level 8, format "& e") : expr_scope.
Notation "*{ T } e" := (Deref (Proj (Copy e%E) #[0]) T%T) Notation "*{ T } e" := (Deref (Copy e%E) T%T)
(at level 9, format "*{ T } e") : expr_scope. (at level 9, format "*{ T } e") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
......
...@@ -6,6 +6,8 @@ Definition tag_in t (stk: stack) := ...@@ -6,6 +6,8 @@ Definition tag_in t (stk: stack) :=
pm opro, pm Disabled mkItem pm (Tagged t) opro stk. pm opro, pm Disabled mkItem pm (Tagged t) opro stk.
Definition tag_in_stack σ l t := Definition tag_in_stack σ l t :=
stk, σ.(sst) !! l = Some stk tag_in t stk. stk, σ.(sst) !! l = Some stk tag_in t stk.
Definition tag_on_top σt l tag : Prop :=
tg <$> (σt.(sst) !! l) = head = Some (Tagged tag).
(** Active protector preserving *) (** Active protector preserving *)
Definition active_preserving (cids: call_id_stack) (stk stk': stack) := Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
......
From stbor.sim Require Import local invariant refl tactics simple program. From stbor.sim Require Import local invariant refl tactics simple program refl_step right_step left_step.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -33,16 +33,16 @@ Proof. ...@@ -33,16 +33,16 @@ Proof.
simplify_eq/=. simplify_eq/=.
(* InitCall *) (* InitCall *)
apply sim_simple_init_call=> c /= {css}. apply sim_simple_init_call=> c /= {css}.
(* Alloc *) (* Alloc local *)
sim_apply sim_simple_alloc_local=> l t /=. sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let=>/=. sim_apply sim_simple_let=>/=.
(* Write *) (* Write local *)
rewrite (vrel_eq _ _ _ AREL). rewrite (vrel_eq _ _ _ AREL).
sim_apply sim_simple_write_local; [solve_sim..|]. sim_apply sim_simple_write_local; [solve_sim..|].
intros arg ->. simpl. intros arg ->. simpl.
sim_apply sim_simple_let=>/=. sim_apply sim_simple_let=>/=.
apply: sim_simple_result. apply: sim_simple_result.
(* Retag. *) (* Retag local *)
sim_apply sim_simple_let=>/=. sim_apply sim_simple_let=>/=.
destruct args as [|args args']; first by inversion AREL. destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL]. apply Forall2_cons_inv in AREL as [AREL ATAIL].
...@@ -55,8 +55,45 @@ Proof. ...@@ -55,8 +55,45 @@ Proof.
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=. intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
apply: sim_simple_result. simpl. apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=. sim_apply sim_simple_let=>/=.
(* Deref *) (* Copy local *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
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..|].
intros ???? Htop. simplify_eq/=.
sim_apply sim_body_let. simplify_eq/=.
(* Copy local (right) *)
sim_apply_r sim_body_copy_local_r; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (right) *)
sim_apply_r sim_body_deref_r. simpl.
sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
{ subst σt'. admit. (* show that tag_op_top is preserved. *) }
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
(* We can go back to simple mode! *)
eapply sim_simplify. { intros ?????? HH. exact HH. }
simplify_eq/=. rewrite Hσs Hσt. clear- AREL FREL LOOK.
(* Call *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Copy local (left). We drop to complex just because simple does not support this yet. *)
intros σs σt Hσs Hσt.
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (left) *)
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_result=>Hval. split.
- eexists. split; first done. admit. (* end_call_sat *)
- constructor; simpl; auto.
Admitted. Admitted.
(** Top-level theorem: Two programs that only differ in the (** Top-level theorem: Two programs that only differ in the
......
...@@ -44,9 +44,10 @@ Proof. ...@@ -44,9 +44,10 @@ Proof.
intros. eapply HΦ; done. intros. eapply HΦ; done.
Qed. Qed.
Lemma sim_body_bind fs ft r n Lemma sim_body_bind fs ft
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es et σs σt Φ : (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
r n σs σt Φ :
r {n,fs,ft} (es, σs) (et, σt) r {n,fs,ft} (es, σs) (et, σt)
: (λ r' n' es' σs' et' σt', : (λ r' n' es' σs' et' σt',
r' {n',fs,ft} (fill Ks es', σs') (fill Kt et', σt') : Φ) r' {n',fs,ft} (fill Ks es', σs') (fill Kt et', σt') : Φ)
...@@ -132,6 +133,26 @@ Proof. ...@@ -132,6 +133,26 @@ Proof.
pclearbot. right. by apply CIH. } pclearbot. right. by apply CIH. }
Qed. Qed.
Lemma sim_body_bind_r fs ft
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
r n es σs σt Φ :
r {n,fs,ft} (#[], σs) (et, σt)
: (λ r' n' _ _ et' σt',
r' {n',fs,ft} (es, σs) (fill Kt et', σt') : Φ)
r {n,fs,ft} (es, σs) (fill Kt et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_bind_l fs ft
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es
r n et σs σt Φ :
r {n,fs,ft} (es, σs) (#[], σt)
: (λ r' n' es' σs' _ _,
r' {n',fs,ft} (fill Ks es', σs') (et, σt) : Φ)
r {n,fs,ft} (fill Ks es, σs) (et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_bind_call r n fs ft es σs et σt (fns fnt: result) (pres pret: list result) posts postt Φ : Lemma sim_body_bind_call r n fs ft es σs et σt (fns fnt: result) (pres pret: list result) posts postt Φ :
r {n,fs,ft} (es, σs) (et, σt) r {n,fs,ft} (es, σs) (et, σt)
: (λ r' n' rs' σs' rt' σt', : (λ r' n' rs' σs' rt' σt',
......
...@@ -26,6 +26,7 @@ Definition cmapUR := gmapUR call_id callStateR. ...@@ -26,6 +26,7 @@ Definition cmapUR := gmapUR call_id callStateR.
Definition to_cmapUR (cm: cmap) : cmapUR := fmap to_callStateR cm. Definition to_cmapUR (cm: cmap) : cmapUR := fmap to_callStateR cm.
Definition tmap := gmap ptr_id (tag_kind * mem). Definition tmap := gmap ptr_id (tag_kind * mem).
Definition heaplet := gmap loc scalar.
Definition heapletR := gmapR loc (agreeR scalarC). Definition heapletR := gmapR loc (agreeR scalarC).
(* ptr_id TagKid x (loc Ag(Scalar)) *) (* ptr_id TagKid x (loc Ag(Scalar)) *)
Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR). Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
...@@ -352,7 +353,7 @@ Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed. ...@@ -352,7 +353,7 @@ Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
(** Resources that we own. *) (** Resources that we own. *)
Definition res_tag tg tk h : resUR := Definition res_tag tg tk (h: heaplet) : resUR :=
({[tg := (to_tagKindR tk, to_agree <$> h)]}, ε, ε). ({[tg := (to_tagKindR tk, to_agree <$> h)]}, ε, ε).
Definition res_callState (c: call_id) (cs: call_state) : resUR := Definition res_callState (c: call_id) (cs: call_state) : resUR :=
......
...@@ -5,6 +5,43 @@ From stbor.sim Require Export instance. ...@@ -5,6 +5,43 @@ From stbor.sim Require Export instance.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Section left.
Implicit Types Φ: resUR nat result state result state Prop.
Lemma sim_body_let_l fs ft r n x et es1 es2 vs1 σs σt Φ :
IntoResult es1 vs1
r {n,fs,ft} (subst' x es1 es2, σs) (et, σt) : Φ
r {n,fs,ft} (let: x := es1 in es2, σs) (et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_deref_l fs ft r n et (rt: result) l t T σs σt Φ :
IntoResult et rt
(Φ r n (PlaceR l t T) σs rt σt)
r {n,fs,ft} (Deref #[ScPtr l t] T, σs) (et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_copy_local_l fs ft r r' n l tg ty s et σs σt Φ :
tsize ty = 1%nat
r r' res_mapsto l 1 s tg
(r {n,fs,ft} (#[s], σs) (et, σt) : Φ)
r {n,fs,ft}
(Copy (Place l (Tagged tg) ty), σs) (et, σt)
: Φ.
Proof.
Admitted.
Lemma sim_body_copy_unique_l
fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) et σs σt Φ :
tsize T = 1%nat
r r' res_tag tg tkUnique h
h !! l = Some s
(r {n,fs,ft} (#[s], σs) (et, σt) : Φ : Prop)
r {n,fs,ft} (Copy (Place l (Tagged tg) T), σs) (et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_copy_left_1 Lemma sim_body_copy_left_1
fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ
(UNIQUE: r.(rtm) !! t Some (k, h)) (UNIQUE: r.(rtm) !! t Some (k, h))
...@@ -33,3 +70,5 @@ Proof. ...@@ -33,3 +70,5 @@ Proof.
{ (* follows COND *) admit. } { (* follows COND *) admit. }
{ (* follows COND *) admit. } { (* follows COND *) admit. }
Abort. Abort.
End left.
...@@ -255,7 +255,7 @@ Proof using Type*. ...@@ -255,7 +255,7 @@ Proof using Type*.
move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e). move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..]. eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq). intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
simplify_eq/=. eapply sim_simple_deref=>l t ?. simplify_eq/=. simplify_eq/=. apply: sim_simple_deref=>l t ?. simplify_eq/=.
do 3 (split; first done). done. do 3 (split; first done). done.
- (* Ref *) - (* Ref *)
move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e). move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
......
...@@ -5,6 +5,8 @@ From stbor.sim Require Export instance body. ...@@ -5,6 +5,8 @@ From stbor.sim Require Export instance body.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Section mem.
Implicit Types Φ: resUR nat result state result state Prop.
(** MEM STEP -----------------------------------------------------------------*) (** MEM STEP -----------------------------------------------------------------*)
...@@ -30,7 +32,7 @@ Lemma sim_body_alloc_local fs ft r n T σs σt Φ : ...@@ -30,7 +32,7 @@ Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
(S σt.(snp)) σt.(snc) in (S σt.(snp)) σt.(snc) in
let rt : resUR := res_tag σt.(snp) tkUnique in let rt : resUR := res_tag σt.(snp) tkUnique in
let r' : resUR := res_mapsto l (tsize T) σt.(snp) in let r' : resUR := res_mapsto l (tsize T) σt.(snp) in
Φ (r rt r') n (PlaceR l t T) σs' (PlaceR l t T) σt' : Prop Φ (r rt r') n (PlaceR l t T) σs' (PlaceR l t T) σt'
r {n,fs,ft} (Alloc T, σs) (Alloc T, σt) : Φ. r {n,fs,ft} (Alloc T, σs) (Alloc T, σt) : Φ.
Proof. Proof.
intros l t σs' σt' rt r' POST. intros l t σs' σt' rt r' POST.
...@@ -351,7 +353,7 @@ Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ ...@@ -351,7 +353,7 @@ Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ
α', memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize Tt) = Some α' α', memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize Tt) = Some α'
let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in
vrel (r r') vs vt Φ (r r') n (ValR vs) σs' (ValR vt) σt' : Prop) vrel (r r') vs vt Φ (r r') n (ValR vs) σs' (ValR vt) σt')
r {n,fs,ft} (Copy (Place l (Tagged t) Ts), σs) (Copy (Place l (Tagged t) Tt), σt) : Φ. r {n,fs,ft} (Copy (Place l (Tagged t) Ts), σs) (Copy (Place l (Tagged t) Tt), σt) : Φ.
Proof. Proof.
intros POST. pfold. intros POST. pfold.
...@@ -580,7 +582,7 @@ Lemma sim_body_write_local_1 fs ft r r' n l tg T v v' σs σt Φ : ...@@ -580,7 +582,7 @@ Lemma sim_body_write_local_1 fs ft r r' n l tg T v v' σs σt Φ :
let σs' := mkState (<[l := s]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in let σs' := mkState (<[l := s]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState (<[l := s]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in let σt' := mkState (<[l := s]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
Φ (r' res_mapsto l 1 s tg) n Φ (r' res_mapsto l 1 s tg) n
(ValR [%S]) σs' (ValR [%S]) σt' : Prop) (ValR [%S]) σs' (ValR [%S]) σt')
r {n,fs,ft} r {n,fs,ft}
(Place l (Tagged tg) T <- #v, σs) (Place l (Tagged tg) T <- #v, σt) : Φ. (Place l (Tagged tg) T <- #v, σs) (Place l (Tagged tg) T <- #v, σt) : Φ.
Proof. Proof.
...@@ -739,7 +741,7 @@ Lemma sim_body_write_related_values ...@@ -739,7 +741,7 @@ Lemma sim_body_write_related_values
( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize Tt) = Some α' ( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize Tt) = Some α'
let σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in let σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in let σt' := mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
Φ r' n ((#[])%V) σs' ((#[]%V)) σt' : Prop) Φ r' n (ValR []%S) σs' (ValR []%S) σt' : Prop)
r {n,fs,ft} r {n,fs,ft}
(Place l (Tagged tg) Ts <- #v, σs) (Place l (Tagged tg) Tt <- #v, σt) : Φ. (Place l (Tagged tg) Ts <- #v, σs) (Place l (Tagged tg) Tt <- #v, σt) : Φ.
Proof. Proof.
...@@ -1032,6 +1034,23 @@ Proof. ...@@ -1032,6 +1034,23 @@ Proof.
intros. simpl. by apply POST. intros. simpl. by apply POST.
Qed. Qed.
(** can probably be derived from [write_related_values]? *)
Lemma sim_body_write_owned
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
arel rs s s (* assuming to-write values are related *)
r' r'' rs
( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize T) = Some α'
let σs' := mkState (write_mem l [s] σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState (write_mem l [s] σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
tag_on_top σt l tg
Φ (r' res_tag tg tkUnique (<[l:=s]> h)) n (ValR []%S) σs' (ValR []%S) σt')
r {n,fs,ft}
(Place l (Tagged tg) T <- #[s], σs) (Place l (Tagged tg) T <- #[s], σt) : Φ.
Proof.
Admitted.
(** Retag *) (** Retag *)
Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp' Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp'
...@@ -1108,7 +1127,7 @@ Lemma sim_body_retag_default fs ft r n x xtag mut T σs σt Φ ...@@ -1108,7 +1127,7 @@ Lemma sim_body_retag_default fs ft r n x xtag mut T σs σt Φ
= Some (hs', αs', nps') = Some (hs', αs', nps')
let σs' := mkState hs' αs' σs.(scs) nps' σs.(snc) in let σs' := mkState hs' αs' σs.(scs) nps' σs.(snc) in
let σt' := mkState ht' αt' σt.(scs) npt' σt.(snc) in let σt' := mkState ht' αt' σt.(scs) npt' σt.(snc) in
Φ r n ((#[])%V) σs' ((#[]%V)) σt' : Prop) Φ r n (ValR []%S) σs' (ValR []%S) σt' : Prop)
r {n,fs,ft} r {n,fs,ft}
(Retag (Place x xtag Tr) Default, σs) (Retag (Place x xtag Tr) Default, σs)
(Retag (Place x xtag Tr) Default, σt) : Φ. (Retag (Place x xtag Tr) Default, σt) : Φ.
...@@ -1353,3 +1372,5 @@ Proof. ...@@ -1353,3 +1372,5 @@ Proof.
simplify_eq. split; [done|]. eexists. split; [|done]. by apply tc_once. } simplify_eq. split; [done|]. eexists. split; [|done]. by apply tc_once. }
subst. simpl. by exists vs, vt. subst. simpl. by exists vs, vt.
Qed. Qed.
End mem.
...@@ -5,6 +5,10 @@ From stbor.sim Require Export instance body. ...@@ -5,6 +5,10 @@ From stbor.sim Require Export instance body.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Section pure.
Implicit Types Φ: resUR nat result state result state Prop.
(** PURE STEP ----------------------------------------------------------------*) (** PURE STEP ----------------------------------------------------------------*)
(** Call - step over *) (** Call - step over *)
...@@ -88,7 +92,7 @@ Qed. ...@@ -88,7 +92,7 @@ Qed.
(** Conc *) (** Conc *)
Lemma sim_body_conc fs ft r n (r1 r2: result) σs σt Φ : Lemma sim_body_conc fs ft r n (r1 r2: result) σs σt Φ :
( v1 v2, r1 = ValR v1 r2 = ValR v2 ( v1 v2, r1 = ValR v1 r2 = ValR v2
Φ r n (ValR (v1 ++ v2)) σs (ValR (v1 ++ v2)) σt : Prop) Φ r n (ValR (v1 ++ v2)) σs (ValR (v1 ++ v2)) σt)
r {n,fs,ft} (Conc r1 r2, σs) (Conc r1 r2, σt) : Φ. r {n,fs,ft} (Conc r1 r2, σs) (Conc r1 r2, σt) : Φ.
Proof. Proof.
intros POST. pfold. intros NT r_f WSAT. split; [|done|]. intros POST. pfold. intros NT r_f WSAT. split; [|done|].
...@@ -110,7 +114,7 @@ Qed. ...@@ -110,7 +114,7 @@ Qed.
Lemma sim_body_bin_op fs ft r n op (r1 r2: result) σs σt Φ : Lemma sim_body_bin_op fs ft r n op (r1 r2: result) σs σt Φ :
( s1 s2 s, r1 = ValR [s1] r2 = ValR [s2] ( s1 s2 s, r1 = ValR [s1] r2 = ValR [s2]
bin_op_eval σt.(shp) op s1 s2 s bin_op_eval σt.(shp) op s1 s2 s
Φ r n (ValR [s]) σs (ValR [s]) σt : Prop) Φ r n (ValR [s]) σs (ValR [s]) σt)
r {n,fs,ft} (BinOp op r1 r2, σs) (BinOp op r1 r2, σt) : Φ. r {n,fs,ft} (BinOp op r1 r2, σs) (BinOp op r1 r2, σt) : Φ.
Proof. Proof.
intros POST. pfold. intros NT r_f WSAT. split; [|done|]. intros POST. pfold. intros NT r_f WSAT. split; [|done|].
...@@ -180,7 +184,7 @@ Qed. ...@@ -180,7 +184,7 @@ Qed.
(** Ref *) (** Ref *)
Lemma sim_body_ref fs ft r n (pl: result) σs σt Φ : Lemma sim_body_ref fs ft r n (pl: result) σs σt Φ :
( l t T, pl = PlaceR l t T ( l t T, pl = PlaceR l t T
Φ r n (ValR [ScPtr l t]) σs (ValR [ScPtr l t]) σt : Prop) Φ r n (ValR [ScPtr l t]) σs (ValR [ScPtr l t]) σt)
r {n,fs,ft} ((& pl)%E, σs) ((& pl)%E, σt) : Φ. r {n,fs,ft} ((& pl)%E, σs) ((& pl)%E, σt) : Φ.
Proof. Proof.
intros POST. pfold. intros POST. pfold.
...@@ -211,7 +215,7 @@ Qed. ...@@ -211,7 +215,7 @@ Qed.
(** Deref *) (** Deref *)
Lemma sim_body_deref fs ft r n (rf: result) T σs σt Φ : Lemma sim_body_deref fs ft r n (rf: result) T σs σt Φ :
( l t, rf = ValR [ScPtr l t] ( l t, rf = ValR [ScPtr l t]
Φ r n (PlaceR l t T) σs (PlaceR l t T) σt : Prop ) Φ r n (PlaceR l t T) σs (PlaceR l t T) σt)
r {n,fs,ft} (Deref rf T, σs) (Deref rf T, σt) : Φ. r {n,fs,ft} (Deref rf T, σs) (Deref rf T, σt) : Φ.
Proof. Proof.
intros POST. pfold. intros POST. pfold.
...@@ -236,3 +240,5 @@ Proof. ...@@ -236,3 +240,5 @@ Proof.
left. apply: sim_body_result. left. apply: sim_body_result.
intros. by eapply POST. intros. by eapply POST.
Qed. Qed.
End pure.
...@@ -5,13 +5,42 @@ From stbor.sim Require Export instance. ...@@ -5,13 +5,42 @@ From stbor.sim Require Export instance.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Lemma sim_body_copy_right_1 Section right.
fs ft (r: resUR) k (h: heapletR) n l t s es σs σt Φ Implicit Types Φ: resUR nat result state result state Prop.
(* we know we're going to read s *)
(UNIQUE: r.(rtm) !! t Some (k, h)) Lemma sim_body_let_r fs ft r n x es et1 et2 vt1 σs σt Φ :
(InD: h !! l Some (to_agree s)) IntoResult et1 vt1
(IN: tag_in_stack σt l t) : r {n,fs,ft} (es, σs) (subst' x et1 et2, σt) : Φ
(σt.(shp) !! l = Some s r {n,fs,ft} (es, σs) (#[s%S], σt) : Φ : Prop) r {S n,fs,ft} (es, σs) (let: x := et1 in et2, σt) : Φ.
r {n,fs,ft} (es, σs) (Copy (Place l (Tagged t) int), σt) : Φ. Proof.
Admitted.
Lemma sim_body_deref_r fs ft r n es (rs: result) l t T σs σt Φ :
IntoResult es rs
(Φ r n rs σs (PlaceR l t T) σt)
r {S n,fs,ft} (es, σs) (Deref #[ScPtr l t] T, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_copy_local_r fs ft r r' n l tg ty s es σs σt Φ :
tsize ty = 1%nat
r r' res_mapsto l 1 s tg
(r {n,fs,ft} (es, σs) (#[s], σt) : Φ)
r {S n,fs,ft}
(es, σs) (Copy (Place l (Tagged tg) ty), σt)
: Φ.
Proof.
Admitted.
Lemma sim_body_copy_unique_r
fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) es σs σt Φ :
tsize T = 1%nat
tag_on_top σt l tg
r r' res_tag tg tkUnique h
h !! l = Some s
(r {n,fs,ft} (es, σs) (#[s], σt) : Φ : Prop)
r {S n,fs,ft} (es, σs) (Copy (Place l (Tagged tg) T), σt) : Φ.
Proof. Proof.
Abort. Admitted.
End right.
...@@ -8,7 +8,7 @@ want to clean some stuff from your context. ...@@ -8,7 +8,7 @@ want to clean some stuff from your context.
*) *)
From stbor.sim Require Export body instance. From stbor.sim Require Export body instance.
From stbor.sim Require Import refl_step. From stbor.sim Require Import refl_step right_step left_step.
Definition fun_post_simple Definition fun_post_simple
initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst := initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
...@@ -167,9 +167,9 @@ Proof. ...@@ -167,9 +167,9 @@ Proof.
Qed. Qed.
Lemma sim_simple_bind fs ft Lemma sim_simple_bind fs ft
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
es et r n css cst Φ : r n css cst Φ :
r ⊨ˢ{n,fs,ft} (es, css) (et, cst) r ⊨ˢ{n,fs,ft} (es, css) (et, cst)
: (λ r' n' es' css' et' cst', : (λ r' n' es' css' et' cst',
r' ⊨ˢ{n',fs,ft} (fill Ks es', css') (fill Kt et', cst') : Φ) r' ⊨ˢ{n',fs,ft} (fill Ks es', css') (fill Kt et', cst') : Φ)
...@@ -268,17 +268,34 @@ Lemma sim_simple_copy_local_l fs ft r r' n l tg ty s et css cst Φ : ...@@ -268,17 +268,34 @@ Lemma sim_simple_copy_local_l fs ft r r' n l tg ty s et css cst Φ :
(Copy (Place l (Tagged tg) ty), css) (et, cst) (Copy (Place l (Tagged tg) ty), css) (et, cst)
: Φ. : Φ.
Proof. Proof.
Admitted. intros ?? Hold σs σt <- <-.
eapply sim_body_copy_local_l; eauto.