Commit 4a59c6d7 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows

parents 003116b9 0294692b
......@@ -30,6 +30,8 @@ theories/sim/sflib.v
theories/sim/tactics.v
theories/sim/instance.v
theories/sim/body.v
theories/sim/refl_pure_step.v
theories/sim/refl_mem_step.v
theories/sim/refl_step.v
theories/sim/left_step.v
theories/sim/right_step.v
......
......@@ -66,6 +66,10 @@ Proof.
rewrite to_of_result. by eexists.
Qed.
Lemma of_result_list_expr (vl: list value) :
(of_result <$> (ValR <$> vl)) = Val <$> vl.
Proof. induction vl as [|v vl IH]; [done|]. by rewrite 3!fmap_cons IH. Qed.
(* Lemma subst_is_closed X x es e :
is_closed X es is_closed (x::X) e is_closed X (subst x es e).
Proof.
......
......@@ -186,6 +186,104 @@ Proof. apply never_stuck_tstep_tc'. Qed.
(** PURE STEP ----------------------------------------------------------------*)
(** Var *)
Lemma fill_var_decompose K e var:
fill K e = Var var
K = [] e = Var var.
Proof.
revert e.
induction K as [|Ki K IH]; [done|]. simpl; intros ? [? ?]%IH.
by destruct Ki.
Qed.
Lemma tstep_var_inv var e' σ σ' :
(Var var, σ) ~{fns}~> (e', σ') False.
Proof.
intros STEP. inv_tstep. symmetry in Eq.
destruct (fill_var_decompose _ _ _ Eq); subst.
simpl in HS. inv_head_step.
Qed.
(** Proj *)
Lemma fill_proj_decompose K e e1 e2:
fill K e = Proj e1 e2
K = [] e = Proj e1 e2
( K', K = K' ++ [ProjLCtx e2] fill K' e = e1)
( v1 K', K = K' ++ [ProjRCtx v1] fill K' e = e2 to_result e1 = Some v1).
Proof.
revert e e1 e2.
induction K as [|Ki K IH]; [by left|]. simpl.
intros e e1 e2 EqK. right.
destruct (IH _ _ _ EqK) as [[? _]|[[K0 [? Eq0]]|[r1 [K' [? Eq']]]]].
- subst. simpl in *. destruct Ki; try done.
+ simpl in EqK. simplify_eq. left. exists []. naive_solver.
+ right. simpl in EqK. inversion EqK; subst.
eexists _, []. naive_solver eauto using to_of_result.
- subst K. left. by exists (Ki :: K0).
- subst K. right. by exists r1, (Ki :: K').
Qed.
Lemma tstep_proj_inv e' (v i: result) σ σ'
(STEP: (Proj v i, σ) ~{fns}~> (e', σ')) :
vv iv (vi: scalar), v = ValR vv i = ValR [ScInt iv]
vv !! (Z.to_nat iv) = Some vi 0 iv e' = (Val [vi]%V) σ' = σ.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_proj_decompose _ _ _ _ Eq)
as [[? _]|[[K0 [? Eq0]]|[r1 [K' [? [Eq' Eq2]]]]]]; subst.
- simpl in Eq. subst e1'.
simpl in HS. inv_head_step.
have Eq1:= to_of_result v. rewrite -H0 /to_result in Eq1.
have Eq2:= to_of_result i. rewrite -H1 /to_result in Eq2. simplify_eq.
naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K0 e1') as [? Eq1'].
+ rewrite /= Eq0 to_of_result. by eexists.
+ by rewrite Eq1' in HS.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
(** Conc *)
Lemma fill_conc_decompose K e e1 e2:
fill K e = Conc e1 e2
K = [] e = Conc e1 e2
( K', K = K' ++ [ConcLCtx e2] fill K' e = e1)
( v1 K', K = K' ++ [ConcRCtx v1] fill K' e = e2 to_result e1 = Some v1).
Proof.
revert e e1 e2.
induction K as [|Ki K IH]; [by left|]. simpl.
intros e e1 e2 EqK. right.
destruct (IH _ _ _ EqK) as [[? _]|[[K0 [? Eq0]]|[r1 [K' [? Eq']]]]].
- subst. simpl in *. destruct Ki; try done.
+ simpl in EqK. simplify_eq. left. exists []. naive_solver.
+ right. simpl in EqK. inversion EqK; subst.
eexists _, []. naive_solver eauto using to_of_result.
- subst K. left. by exists (Ki :: K0).
- subst K. right. by exists r1, (Ki :: K').
Qed.
Lemma tstep_conc_inv e' (r1 r2: result) σ σ'
(STEP: (Conc r1 r2, σ) ~{fns}~> (e', σ')) :
v1 v2, r1 = ValR v1 r2 = ValR v2 e' = (Val (v1 ++ v2)) σ' = σ.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_conc_decompose _ _ _ _ Eq)
as [[? _]|[[K0 [? Eq0]]|[r' [K' [? [Eq' Eq2]]]]]]; subst.
- simpl in Eq. subst e1'.
simpl in HS. inv_head_step.
have Eq1:= to_of_result r1. rewrite -H0 /to_result in Eq1.
have Eq2:= to_of_result r2. rewrite -H1 /to_result in Eq2. simplify_eq.
naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K0 e1') as [? Eq1'].
+ rewrite /= Eq0 to_of_result. by eexists.
+ by rewrite Eq1' in HS.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
(** BinOp *)
Lemma fill_bin_op_decompose K e op e1 e2:
fill K e = BinOp op e1 e2
......@@ -256,6 +354,22 @@ Proof.
rewrite /= HS in TM2. by destruct TM2.
Qed.
Lemma tstep_bin_op_inv op (r1 r2: result) e' σ σ'
(STEP: (BinOp op r1 r2, σ) ~{fns}~> (e', σ')) :
l1 l2 l, bin_op_eval σ.(shp) op l1 l2 l e' = (#[l])%E σ' = σ.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_bin_op_decompose _ _ _ _ _ Eq)
as [[]|[[K' [? Eq']]|[v1 [K' [? [Eq' VAL]]]]]]; subst.
- clear Eq. simpl in HS. inv_head_step. naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
Lemma tstep_bin_op_red_r e1 σ1 e2 e2' σ2 op:
terminal e1
(e2, σ1) ~{fns}~>* (e2', σ2)
......@@ -451,6 +565,36 @@ Proof.
+ by rewrite /= HS in Eqv.
Qed.
(** Case *)
Lemma fill_case_decompose K e e1 el1:
fill K e = Case e1 el1
K = [] e = Case e1 el1
( K', K = K' ++ [CaseCtx el1] fill K' e = e1).
Proof.
revert e e1 el1.
induction K as [|Ki K IH]; [by left|]. simpl.
intros e e1 el1 EqK. right.
destruct (IH _ _ _ EqK) as [[? _]|[K' [? Eq']]].
- subst. simpl in *. destruct Ki; try done.
simpl in EqK. simplify_eq. exists []. naive_solver.
- subst K. by exists (Ki :: K').
Qed.
Lemma tstep_case_inv (rc: result) el e' σ σ'
(STEP: (Case rc el, σ) ~{fns}~> (e', σ')) :
(i: Z) e, 0 i el !! (Z.to_nat i) = Some e
rc = ValR [ScInt i] e' = e σ' = σ.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_case_decompose _ _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- simpl in *. inv_head_step. exists i, e2'. repeat split; auto.
have Eq1 := to_of_result rc. rewrite -H /to_result in Eq1. by simplify_eq.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
(** MEM STEP -----------------------------------------------------------------*)
(** Alloc *)
......
......@@ -77,8 +77,8 @@ Proof.
- induction H; first done. simpl. by f_equal.
Qed.
Lemma subst_map_subst map x (r: result) (e: expr) :
subst_map map (subst x r e) = subst_map (<[x:=r]>map) e.
Lemma subst_map_subst map x (r: value) (e: expr) :
subst_map map (subst x r e) = subst_map (<[x:=ValR r]>map) e.
Proof.
revert x r map; induction e using expr_ind; intros xx r map; simpl;
try (f_equal; eauto).
......@@ -97,11 +97,11 @@ Qed.
(** Turning list-subst into par-subst while preserving a pointwise property.
FIXME: There probably is a way to do this with a lemma that talks about
just one list... *)
Lemma subst_l_map (xbs : list binder) (xes xet : list result)
Lemma subst_l_map (xbs : list binder) (xes xet : list value)
(ebs ebt es et : expr) (R : result result Prop) :
subst_l xbs (of_result <$> xes) ebs = Some es
subst_l xbs (of_result <$> xet) ebt = Some et
Forall2 R xes xet
subst_l xbs (Val <$> xes) ebs = Some es
subst_l xbs (Val <$> xet) ebt = Some et
Forall2 R (ValR <$> xes) (ValR <$> xet)
map : gmap string (result * result),
es = subst_map (fst <$> map) ebs et = subst_map (snd <$> map) ebt
map_Forall (λ _ '(s, t), R s t) map.
......@@ -116,7 +116,7 @@ Proof.
inversion HR. simplify_eq/=. destruct a.
+ eapply IHxbs; eauto.
+ edestruct (IHxbs xes xet) as (map & ? & ? & ?); [done..|].
exists (<[s:=(ees, eet)]> map). subst es et.
exists (<[s:=(ValR ees, ValR eet)]> map). simplify_eq/=.
rewrite !subst_map_subst !fmap_insert.
split; first done. split; first done.
apply map_Forall_insert_2; done.
......
......@@ -2,7 +2,7 @@ From stbor.lang Require Import steps_inversion.
From stbor.sim Require Export local invariant.
Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
(sim_local_body wsat rrel fs ft r n%nat es%E σs et%E σt Φ)
(sim_local_body wsat vrel fs ft r n%nat es%E σs et%E σt Φ)
(at level 70, format "'[hv' r '/' ⊨{ n , fs , ft } '/ ' '[ ' ( es , '/' σs ) ']' '/' ≥ '/ ' '[ ' ( et , '/' σt ) ']' '/' : Φ ']'").
......@@ -14,7 +14,7 @@ fn table, allow giving a lower bound. But this is good enough for now.
This could be done in general, but we just do it for the instance. *)
Definition sim_mod_fun f1 f2 :=
fs ft, sim_local_funs_lookup fs ft
sim_local_fun wsat rrel fs ft end_call_sat f1 f2.
sim_local_fun wsat vrel fs ft end_call_sat f1 f2.
Definition sim_mod_funs (fns fnt: fn_env) :=
name fn_src, fns !! name = Some fn_src fn_tgt,
......@@ -67,7 +67,7 @@ Qed.
assumption. *)
Lemma sim_mod_funs_local fs ft :
sim_mod_funs fs ft
sim_local_funs wsat rrel fs ft end_call_sat.
sim_local_funs wsat vrel fs ft end_call_sat.
Proof.
intros Hmod. intros f fn_src Hlk.
destruct (Hmod _ _ Hlk) as (fn_tgt & ? & ? & ?). exists fn_tgt.
......@@ -84,3 +84,47 @@ Proof.
intros Hne (ebs & HCs & EQ). exists ebs, HCs.
rewrite lookup_insert_ne //.
Qed.
Lemma rrel_eq r (e1 e2: result) :
rrel vrel r e1 e2 e1 = e2.
Proof.
destruct e1, e2; simpl; [|done..|].
- intros ?. f_equal. by eapply vrel_eq.
- intros [VREL ?]. subst. apply vrel_eq in VREL. by simplify_eq.
Qed.
Lemma rrel_mono (r1 r2 : resUR) (VAL: r2) :
r1 r2 v1 v2, rrel vrel r1 v1 v2 rrel vrel 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 list_Forall_result_value (es: list result) (vs: list value) :
of_result <$> es = Val <$> vs es = ValR <$> vs.
Proof.
revert vs. induction es as [|e es IH]; intros vs.
{ intros Eq. symmetry in Eq. apply fmap_nil_inv in Eq. by subst vs. }
destruct vs as [|v vs]; [by intros ?%fmap_nil_inv|].
rewrite 3!fmap_cons. intros Eq.
inversion Eq as [Eq1].
rewrite (IH vs) //. f_equal.
have Eq2 := to_of_result e. rewrite Eq1 /= in Eq2. by simplify_eq.
Qed.
Lemma list_Forall_rrel_vrel r (es et: list result) :
Forall2 (rrel vrel 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
Forall2 (vrel r) vs vt.
Proof.
intros RREL [vs Eqs]%list_Forall_to_value [vt Eqt]%list_Forall_to_value.
exists vs, vt.
apply list_Forall_result_value in Eqs.
apply list_Forall_result_value in Eqt. subst es et.
do 2 (split; [done|]).
by rewrite -> Forall2_fmap in RREL.
Qed.
......@@ -101,16 +101,6 @@ Definition wsat (r: resUR) (σs σt: state) : Prop :=
(* Values passed among functions are public *)
Definition vrel (r: resUR) (v1 v2: value) := Forall2 (arel r) v1 v2.
Definition rrel (r: resUR) rs rt: Prop :=
match rs, rt with
| ValR vs, ValR vt => vrel r vs vt
| PlaceR ls ts Ts, PlaceR lt t_t Tt =>
(* Places are related like pointers, and the types must be equal. *)
vrel r [ScPtr ls ts] [ScPtr lt t_t] Ts = Tt
| _, _ => False
end.
(** Condition for resource before EndCall *)
(* The call id [c] to be end must not have any privately protected locations. *)
Definition end_call_sat (r: resUR) (c: call_id) : Prop :=
......@@ -148,14 +138,6 @@ Proof.
f_equal. by apply (arel_eq _ _ _ Eq1). by apply IH.
Qed.
Lemma rrel_eq r (e1 e2: result) :
rrel r e1 e2 e1 = e2.
Proof.
destruct e1, e2; simpl; [|done..|].
- intros ?. f_equal. by eapply vrel_eq.
- intros [VREL ?]. subst. apply vrel_eq in VREL. by simplify_eq.
Qed.
Lemma arel_mono (r1 r2 : resUR) (VAL: r2) :
r1 r2 s1 s2, arel r1 s1 s2 arel r2 s1 s2.
Proof.
......@@ -184,14 +166,6 @@ Lemma vrel_mono (r1 r2 : resUR) (VAL: ✓ r2) :
r1 r2 v1 v2, vrel r1 v1 v2 vrel r2 v1 v2.
Proof. intros Le v1 v2 VREL. by apply (Forall2_impl _ _ _ _ VREL), arel_mono. Qed.
Lemma rrel_mono (r1 r2 : resUR) (VAL: r2) :
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 priv_loc_mono (r1 r2 : resUR) (VAL: r2) :
r1 r2 l t, priv_loc r1 l t priv_loc r2 l t.
Proof.
......
......@@ -9,9 +9,18 @@ Set Default Proof Using "Type".
Section local.
Context {A: ucmraT}.
Variable (wsat: A state state Prop).
Variable (rrel: A result result Prop).
Variable (vrel: A value value Prop).
Variable (fs ft: fn_env).
Definition rrel (r: A) rs rt: Prop :=
match rs, rt with
| ValR vs, ValR vt => vrel r vs vt
| PlaceR ls ts Ts, PlaceR lt t_t Tt =>
(* Places are related like pointers, and the types must be equal. *)
vrel r [ScPtr ls ts] [ScPtr lt t_t] Ts = Tt
| _, _ => False
end.
Notation PRED := (A nat result state result state Prop)%type.
Notation SIM := (A nat expr state expr state PRED Prop)%type.
......@@ -122,10 +131,10 @@ Definition fun_post (esat: A → call_id → Prop) initial_call_id_stack
rrel r rs rt.
Definition sim_local_fun
(esat: A call_id Prop) (fn_src fn_tgt : function) : Prop :=
r es et (vl_src vl_tgt: list result) σs σt
(VALEQ: Forall2 (rrel r) vl_src vl_tgt)
(EQS: subst_l fn_src.(fun_args) (of_result <$> vl_src) fn_src.(fun_body) = Some es)
(EQT: subst_l fn_tgt.(fun_args) (of_result <$> vl_tgt) fn_tgt.(fun_body) = Some et),
r es et (vl_src vl_tgt: list value) σs σt
(VALEQ: Forall2 (vrel r) vl_src vl_tgt)
(EQS: subst_l fn_src.(fun_args) (Val <$> vl_src) fn_src.(fun_body) = Some es)
(EQT: subst_l fn_tgt.(fun_args) (Val <$> vl_tgt) fn_tgt.(fun_body) = Some et),
idx, sim_local_body r idx
(InitCall es) σs (InitCall et) σt
(fun_post esat σt.(scs)).
......
......@@ -46,15 +46,15 @@ Inductive sim_local_frames:
our local resource r and have world satisfaction *)
(WSAT' : wsat (r_f (frame.(rc) r')) σ_src' σ_tgt')
(* and the returned values are related w.r.t. (r r' r_f) *)
(VRET : rrel r' v_src v_tgt)
(VRET : rrel vrel r' v_src v_tgt)
(CIDS: σ_tgt'.(scs) = frame.(callids)),
idx', sim_local_body wsat rrel fns fnt
idx', sim_local_body wsat vrel fns fnt
(frame.(rc) r') idx'
(fill frame.(K_src) (of_result v_src)) σ_src'
(fill frame.(K_tgt) (of_result v_tgt)) σ_tgt'
(λ r _ vs σs vt σt,
( c, σt.(scs) = c :: cids end_call_sat r c)
rrel r vs vt))
rrel vrel r vs vt))
: sim_local_frames
(r_f frame.(rc))
frame.(callids)
......@@ -70,17 +70,17 @@ Inductive sim_local_conf:
rc idx e_src σ_src e_tgt σ_tgt
Ke_src Ke_tgt
(FRAMES: sim_local_frames r_f cids K_src K_tgt frames)
(LOCAL: sim_local_body wsat rrel fns fnt rc idx e_src σ_src e_tgt σ_tgt
(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 r vs vt))
rrel vrel 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)
: sim_local_conf idx Ke_src σ_src Ke_tgt σ_tgt.
Lemma sim_local_conf_sim
(FUNS: sim_local_funs wsat rrel fns fnt end_call_sat)
(FUNS: sim_local_funs wsat vrel fns fnt end_call_sat)
(idx:nat) (e_src:expr) (σ_src:state) (e_tgt:expr) (σ_tgt:state)
(SIM: sim_local_conf idx e_src σ_src e_tgt σ_tgt)
: sim fns fnt idx (e_src, σ_src) (e_tgt, σ_tgt)
......@@ -134,7 +134,7 @@ Proof.
simplify_eq.
set Φ : resUR nat result state result state Prop :=
λ r2 _ vs2 σs2 vt2 σt2, rrel r2 vs2 vt2
λ r2 _ vs2 σs2 vt2 σt2, rrel vrel 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)
......@@ -206,12 +206,17 @@ Proof.
destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & ?). subst e2 σ2.
destruct (FUNS _ _ Eqfs) as ([xlt2 ebt2 HCt2] & Eqft2 & Eql2 & SIMf).
rewrite Eqft2 in x3. simplify_eq.
apply list_Forall_rrel_vrel in VREL as (vs & vt & ? & ? & VREL); [|done..].
subst vl_src vl_tgt.
rewrite -list_fmap_compose in Eqss.
rewrite -list_fmap_compose in x4.
specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf].
esplits.
* left. eapply tc_rtc_l.
{ apply fill_tstep_rtc. eauto. }
{ econs. rewrite -fill_app. eapply (head_step_fill_tstep).
econs. eapply (CallBS _ _ _ _ xls ebs); eauto. }
econs. eapply (CallBS _ _ _ _ xls ebs); eauto.
rewrite -list_fmap_compose. eauto. }
* right. apply CIH. econs.
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss.
destruct (CONT r' v_src v_tgt σ_src' σ_tgt' VRET WSAT').
......
......@@ -10,7 +10,7 @@ Theorem sim_prog_sim_classical
prog_tgt
`{NSD: stuck_decidable_1 prog_src}
(MAINT: has_main prog_src)
(FUNS: sim_local_funs wsat rrel prog_src prog_tgt end_call_sat)
(FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat)
: behave_prog prog_tgt <1= behave_prog prog_src.
Proof.
destruct MAINT as (ebs & HCs & Eqs).
......@@ -32,7 +32,7 @@ Proof.
intros. simpl. exists 1%nat.
apply sim_body_result.
intros VALID.
have ?: rrel (init_res r') vs vt.
have ?: rrel vrel (init_res r') vs vt.
{ eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }
split; [|done].
exists O. split; [by rewrite -STACKT|].
......
......@@ -23,10 +23,10 @@ Definition value_wf (v: value) : Prop := Forall scalar_wf v.
Fixpoint expr_wf (e: expr) : Prop :=
match e with
(* Structural cases. *)
| Var _ | Alloc _ => True
| Val v => value_wf v
| Call f args => expr_wf f Forall id (map expr_wf args)
| Case e branches => expr_wf e Forall id (map expr_wf branches)
| Var _ | Alloc _ => True
| Deref e _ | Ref e | Copy e | Retag e _ =>
expr_wf e
| Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
......@@ -47,12 +47,12 @@ Context (css cst: call_id_stack).
Definition sem_steps := 10%nat.
Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop :=
n = sem_steps css' = css cst' = cst rrel r rs rt.
n = sem_steps css' = css cst' = cst rrel vrel r rs rt.
(** We define a "semantic well-formedness", in some context. *)
Definition sem_wf (r: resUR) es et :=
xs : gmap string (result * result),
map_Forall (λ _ '(rs, rt), rrel r rs rt) xs
map_Forall (λ _ '(rs, rt), rrel vrel r rs rt) xs
r ⊨ˢ{sem_steps,fs,ft}
(subst_map (fst <$> xs) es, css)
......@@ -142,7 +142,8 @@ Proof.
admit. (* end_call_sat *)
- done.
}
destruct (subst_l_map _ _ _ _ _ _ _ _ Hsubst1 Hsubst2 Hrel) as (map & -> & -> & Hmap).
destruct (subst_l_map _ _ _ _ _ _ _ (rrel vrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
{ clear -Hrel. induction Hrel; eauto using Forall2. }
eapply sim_simplify, expr_wf_soundness; [done..|].
admit. (* resource stuff. *)
Admitted.
......
This diff is collapsed.
From iris.algebra Require Import local_updates.
From stbor.lang Require Import steps_progress steps_inversion steps_retag.
From stbor.sim Require Export instance body.
Set Default Proof Using "Type".
(** PURE STEP ----------------------------------------------------------------*)
(** Call - step over *)
Lemma sim_body_step_over_call fs ft
rc rv n fid vls vlt σs σt Φ
(VREL: Forall2 (vrel rv) vls vlt)
(FUNS: sim_local_funs_lookup fs ft) :
( r' vs vt σs' σt' (VRET: rrel vrel r' vs vt)
(STACKS: σs.(scs) = σs'.(scs))
(STACKT: σt.(scs) = σt'.(scs)), n',
rc r' {n',fs,ft} (of_result vs, σs') (of_result vt, σt') : Φ)
rc rv {n,fs,ft}
(Call #[ScFnPtr fid] (Val <$> vls), σs) (Call #[ScFnPtr fid] (Val <$> vlt), σt) : Φ.
Proof.
intros CONT. pfold. intros NT r_f WSAT.
edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|].
apply tstep_call_inv in RED; last first.
{ apply list_Forall_to_value. eauto. }
destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ?). subst e2 σ2.
destruct (FUNS _ _ Eqfs) as ([xlt ebt HCt] & Eqft & Eql).
simpl in Eql.
destruct (subst_l_is_Some xlt (Val <$> vlt) ebt) as [est Eqst].
{ rewrite fmap_length -(Forall2_length _ _ _ VREL) -Eql
(subst_l_is_Some_length _ _ _ _ Eqss) fmap_length //. }
split; [|done|].
{ right. exists (EndCall (InitCall est)), σt.
eapply (head_step_fill_tstep _ []). econstructor. econstructor; try done.
apply list_Forall_to_value. eauto. }
eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
[] [] fid (ValR <$> vlt) (ValR <$> vls)); eauto.
{ by rewrite of_result_list_expr. }
{ by rewrite of_result_list_expr. }
{ eapply Forall2_fmap, Forall2_impl; eauto. }
intros r' ? ? σs' σt' VR WSAT' STACK.
destruct (CONT _ _ _ σs' σt' VR) as [n' ?]; [|done|exists n'; by left].
destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (?&?&?Eqcss&?).
destruct WSAT' as (?&?&?&?&?&SREL'&?). destruct SREL' as (?&?&?Eqcss'&?).
by rewrite Eqcss' Eqcss.
Qed.
(** Var *)
Lemma sim_body_var fs ft r n σs σt var Φ :
r {n,fs,ft} (Var var, σs) (Var var, σt) : Φ.
Proof.
pfold. intros NT r_f WSAT.
destruct (NT (Var var) σs) as [[]|[? [? RED%tstep_var_inv]]];
[constructor|done..].
Qed.
(** Proj *)
Lemma sim_body_proj fs ft r n (v i: result) σs σt Φ :
( vi vv iv, v = ValR vv i = ValR [ScInt iv]
vv !! (Z.to_nat iv) = Some vi 0 iv
Φ r n (ValR [vi]) σs (ValR [vi]) σt : Prop)
r {n,fs,ft} (Proj v i, σs) (Proj v i, σt) : Φ.
Proof.