Commit 1736fe81 authored by Hai Dang's avatar Hai Dang

fix call again

parent 1dc9d71c
......@@ -535,19 +535,24 @@ Proof.
- subst K. right. exists (Ki :: K'). naive_solver.
Qed.
Lemma tstep_call_inv (fid: fn_id) el e' σ σ'
Lemma tstep_call_inv (fi: result) el e' σ σ'
(TERM: Forall (λ ei, is_Some (to_value ei)) el)
(STEP: (Call #[fid] el, σ) ~{fns}~> (e', σ')) :
xl e HC es, fns !! fid = Some (@FunV xl e HC)
subst_l xl el e = Some es e' = (EndCall (InitCall es)) σ' = σ.
(STEP: (Call fi el, σ) ~{fns}~> (e', σ')) :
fid xl e HC es,
fns !! fid = Some (@FunV xl e HC)
subst_l xl el e = Some es
fi = ValR [ScFnPtr fid]
e' = (EndCall (InitCall es)) σ' = σ.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_call_decompose _ _ _ _ Eq)
as [[]|[[K' [? Eq']]|[K' [v1 [vl [e2 [el2 [? Eq']]]]]]]]; subst.
- simpl in *. inv_head_step. naive_solver.
- simpl in *. inv_head_step; simplify_eq.
have Eq1 := to_of_result fi. rewrite -H /to_result in Eq1.
naive_solver.
- exfalso. simpl in *. apply result_head_stuck in HS.
destruct (fill_val (Λ:=bor_ectx_lang fns) K' e1') as [? Eqv].
+ rewrite /= Eq'. by eexists.
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite /= HS in Eqv.
- exfalso. simpl in *. destruct Eq' as [Eq1 Eq2].
apply result_head_stuck in HS.
......@@ -558,20 +563,24 @@ Proof.
+ by rewrite /= HS in Eqv.
Qed.
Lemma tstep_call_inv_result (fid: fn_id) el e' σ σ'
Lemma tstep_call_inv_result (fi: result) el e' σ σ'
(TERM: Forall (λ ei, is_Some (to_result ei)) el)
(STEP: (Call #[fid] el, σ) ~{fns}~> (e', σ')) :
xl e HC es, fns !! fid = Some (@FunV xl e HC)
subst_l xl el e = Some es e' = (EndCall (InitCall es)) σ' = σ
(STEP: (Call fi el, σ) ~{fns}~> (e', σ')) :
fid xl e HC es, fns !! fid = Some (@FunV xl e HC)
subst_l xl el e = Some es
fi = ValR [ScFnPtr fid]
e' = (EndCall (InitCall es)) σ' = σ
Forall (λ ei, is_Some (to_value ei)) el.
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_call_decompose _ _ _ _ Eq)
as [[]|[[K' [? Eq']]|[K' [v1 [vl [e2 [el2 [? Eq']]]]]]]]; subst.
- simpl in *. inv_head_step. naive_solver.
- simpl in *. inv_head_step; simplify_eq.
have Eq1 := to_of_result fi. rewrite -H /to_result in Eq1.
naive_solver.
- exfalso. simpl in *. apply result_head_stuck in HS.
destruct (fill_val (Λ:=bor_ectx_lang fns) K' e1') as [? Eqv].
+ rewrite /= Eq'. by eexists.
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite /= HS in Eqv.
- exfalso. simpl in *. destruct Eq' as [Eq1 Eq2].
apply result_head_stuck in HS.
......
......@@ -190,8 +190,8 @@ Proof.
{ inv STEP'0. ss. }
* right. apply CIH. econs; eauto.
+ (* call *)
exploit fill_step_inv_2; eauto. i. des; ss.
exploit tstep_call_inv_result.
exploit fill_step_inv_2; eauto. i. des; ss. subst.
exploit (tstep_call_inv_result fnt (ValR [ScFnPtr fid])).
{ instantiate (1:= (of_result <$> vl_tgt)).
by apply list_Forall_to_of_result. }
{ exact x2. }
......@@ -201,16 +201,17 @@ Proof.
eapply never_stuck_tstep_rtc; eauto.
by apply (never_stuck_fill_inv _ K_src0). }
edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|].
apply tstep_call_inv_result in RED; last first.
apply (tstep_call_inv_result fns (ValR [ScFnPtr fid])) in RED; last first.
{ by apply list_Forall_to_of_result. }
destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & ?). subst e2 σ2.
destruct RED as (fid' & xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & ? & ?).
subst. simplify_eq.
destruct (FUNS _ _ Eqfs) as ([xlt2 ebt2 HCt2] & Eqft2 & Eql2 & SIMf).
rewrite Eqft2 in x3. simplify_eq.
rewrite Eqft2 in x0. 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].
rewrite -list_fmap_compose in x3.
specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x3) as [idx2 SIMf].
esplits.
* left. eapply tc_rtc_l.
{ apply fill_tstep_rtc. eauto. }
......
......@@ -27,7 +27,7 @@ Proof.
- econs 1.
- ss.
- ss.
- eapply (sim_body_step_over_call _ _ init_res ε _ _ [] []); [done|..].
- eapply (sim_body_step_over_call _ _ init_res ε _ (ValR _) [] []); [done|..].
{ intros fid fn_src. specialize (FUNS fid fn_src). naive_solver. }
intros. simpl. exists 1%nat.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
......
......@@ -9,23 +9,25 @@ Set Default Proof Using "Type".
(** Call - step over *)
Lemma sim_body_step_over_call fs ft
rc rv n fid rls rlt σs σt Φ
rc rv n (fi: result) rls rlt σs σt Φ
(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)
( r' fid vls vlt vs vt σs' σt' (VRET: vrel r' vs vt)
(STACKS: σs.(scs) = σs'.(scs))
(STACKT: σt.(scs) = σt'.(scs))
(Eqfid: fi = ValR [ScFnPtr fid])
(Eqvls: rls = ValR <$> vls)
(Eqvlt: rlt = ValR <$> vlt), n',
rc r' {n',fs,ft} (Val vs, σs') (Val vt, σt') : Φ)
rc rv {n,fs,ft}
(Call #[ScFnPtr fid] (of_result <$> rls), σs) (Call #[ScFnPtr fid] (of_result <$> rlt), σt) : Φ.
(Call fi (of_result <$> rls), σs) (Call fi (of_result <$> rlt), σt) : Φ.
Proof.
intros CONT. pfold. intros NT r_f WSAT.
edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|].
apply tstep_call_inv_result in RED; last by apply list_Forall_to_of_result.
destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & VALs).
have VALs' := VALs. apply list_Forall_to_value in VALs' as [vls Eqvls].
destruct RED as (fid & xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ? & ? & VALs).
have VALs' := VALs.
apply list_Forall_to_value in VALs' as [vls Eqvls].
subst. rewrite Eqvls. rewrite Eqvls in VALs, Eqss.
apply list_Forall_result_value in Eqvls. subst rls.
destruct (list_Forall_rrel_vrel_3 _ _ _ RREL VALs) as (vlt & ? & VALt & VREL).
......@@ -43,7 +45,7 @@ Proof.
[] [] fid (ValR <$> vlt) (ValR <$> vls)); eauto.
{ by rewrite of_result_list_expr. }
intros r' ? ? σs' σt' VR WSAT' STACK.
destruct (CONT r' vls vlt v_src v_tgt σs' σt') as [n' ?];
destruct (CONT r' fid vls vlt v_src v_tgt σs' σt') as [n' ?];
[by apply vrel_rrel| |done..|exists n'; by left].
destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (?&?&?Eqcss&?).
destruct WSAT' as (?&?&?&?&?&SREL'&?). destruct SREL' as (?&?&?Eqcss'&?).
......
......@@ -226,16 +226,17 @@ Qed.
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' rls rlt rv fs ft r r' n fid css cst Φ :
Lemma sim_simple_call n' rls rlt rv fs ft r r' n (fi: result) css cst Φ :
sim_local_funs_lookup fs ft
Forall2 (rrel rv) rls rlt
r r' rv
( rret vs vt vls vlt,
( rret vs vt vls vlt fid,
fi = ValR [ScFnPtr fid]
rls = ValR <$> vls rlt = ValR <$> vlt
vrel rret vs vt
r' rret ⊨ˢ{n',fs,ft} (Val vs, css) (Val vt, cst) : Φ)
r ⊨ˢ{n,fs,ft}
(Call #[ScFnPtr fid] (of_result <$> rls), css) (Call #[ScFnPtr fid] (of_result <$> rlt), cst) : Φ.
(Call fi (of_result <$> rls), css) (Call fi (of_result <$> rlt), cst) : Φ.
Proof.
intros Hfns Hrel Hres HH σs σt <-<-. rewrite Hres.
apply: sim_body_step_over_call.
......
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