Commit d76d1e88 authored by Hai Dang's avatar Hai Dang
Browse files

complete adequacy

parent 4af143aa
......@@ -77,6 +77,17 @@ Proof.
destruct cs' as [[]|c2|]; auto; try inversion 1.
Qed.
Lemma cmap_lookup_op_l_equiv_pub (cm1 cm2: cmapUR) c (VALID: (cm1 cm2)):
cm1 !! c Some (to_callStateR csPub)
(cm1 cm2) !! c Some (to_callStateR csPub).
Proof.
intros HL. move : (VALID c). rewrite lookup_op HL.
destruct (cm2 !! c) as [cs'|] eqn:Eqc; rewrite Eqc; [|done].
rewrite -Some_op Some_valid.
destruct cs' as [[]|c2|]; auto; try inversion 1.
rewrite /= Cinr_op. intros Eq2%agree_op_inv. by rewrite -Eq2 agree_idemp.
Qed.
Lemma cmap_insert_op_r (cm1 cm2: cmapUR) c T cs (VALID: (cm1 cm2)):
cm2 !! c = Some (to_callStateR (csOwned T))
cm1 <[c:=cs]> cm2 = <[c:=cs]> (cm1 cm2).
......@@ -90,6 +101,15 @@ Proof.
- do 2 (rewrite lookup_insert_ne //). by rewrite lookup_op.
Qed.
Lemma callStateR_exclusive_2 T mb :
mb Some (to_callStateR csPub) Some (to_callStateR (csOwned T)) False.
Proof.
destruct mb as [cs|]; [rewrite -Some_op|rewrite left_id];
intros Eq%Some_equiv_inj.
- destruct cs; inversion Eq.
- inversion Eq.
Qed.
Lemma ptrmap_insert_op_r (pm1 pm2: ptrmapUR) t h0 kh (VALID: (pm1 pm2)):
pm2 !! t = Some (to_tagKindR tkUnique, h0)
pm1 <[t:=kh]> pm2 = <[t:=kh]> (pm1 pm2).
......
......@@ -1059,7 +1059,7 @@ Lemma sim_body_step_over_call fs ft
(FT: ft !! fid = Some (@FunV xlt et HCt))
(VT : Forall (λ ei, is_Some (to_value ei)) elt)
(ST: subst_l xlt elt et = Some et') :
( r' vs vt σs' σt' (VRET: vrel r' vs vt), n',
( r' vs vt σs' σt' (VRET: vrel r' vs vt) (STACK: σt.(scs) = σt'.(scs)), n',
rc r' {n',fs,ft} (fill Ks (Val vs), σs') (fill Kt (Val vt), σt') : Φ)
rc rv {n,fs,ft}
(fill Ks (Call #[ScFnPtr fid] els), σs) (fill Kt (Call #[ScFnPtr fid] elt), σt) : Φ.
......@@ -1070,8 +1070,8 @@ Proof.
{ intros vt. by rewrite fill_not_result. }
eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
Ks _ fid elt els); eauto; [done|].
intros r' ? ? σs' σt' (vs&vt&?&?&VR). simplify_eq.
destruct (CONT _ _ _ σs' σt' VR) as [n' ?].
intros r' ? ? σs' σt' (vs&vt&?&?&VR) STACK. simplify_eq.
destruct (CONT _ _ _ σs' σt' VR STACK) as [n' ?].
exists n'. by left.
Qed.
......
......@@ -4,8 +4,12 @@ From stbor.sim Require Import sflib behavior global local invariant global_adequ
Set Default Proof Using "Type".
Lemma sim_prog_sim
prog_src `{NSD: e σ, Decision (never_stuck prog_src e σ)}
prog_src
prog_tgt
`{NSD: e σ, never_stuck prog_src e σ \/
exists e' σ', (e, σ) ~{prog_src}~>* (e', σ') /\
~ terminal e' /\
~ reducible prog_src e' σ'}
(FUNS: sim_local_funs wsat vrel_expr prog_src prog_tgt end_call_sat)
(MAINT: ebt HCt, prog_tgt !! "main" = Some (@FunV [] ebt HCt))
: behave_prog prog_tgt <1= behave_prog prog_src.
......@@ -14,34 +18,29 @@ Proof.
destruct (FUNS _ _ Eqt) as ([xls ebs HCs] & Eqs & Eql & SIMf).
apply nil_length_inv in Eql. subst xls.
specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [done..|].
unfold behave_prog. eapply (adequacy _ _ idx); [apply _| |by apply wf_init_state..].
unfold behave_prog. eapply (adequacy _ _ idx); [apply NSD| |by apply wf_init_state..].
eapply sim_local_conf_sim; eauto.
econs; swap 2 4.
- econs 1.
- ss.
- ss.
- eapply (sim_body_step_over_call _ _ [] [] init_res ε _ _ [] [] ebt ebt [] ).
done. done. done. done. done.
- eapply (sim_body_step_over_call _ _ [] [] init_res ε _ _ [] [] ebt ebt [] );
[done..|].
intros. simpl. exists 1%nat.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
intros.
intros VALID.
have ?: vrel_expr (init_res r') (of_result #vs) (of_result #vt).
{ do 2 eexists. do 2 (split; [done|]).
eapply vrel_mono; [done|apply cmra_included_r|done]. }
split; last split; [done| |done].
(*
eapply (sim_body_step_into_call _ _ _ _ _ [] ebs HCs [] ebs [] ebt HCt [] ebt);
[done..|].
eapply (sim_body_bind _ _ _ _ [EndCallCtx] [EndCallCtx] (InitCall ebs) (InitCall ebt)).
eapply sim_local_body_post_mono; [|exact SIM].
clear SIM. simpl.
intros r1 idx1 vs σs vt σt ([c Eqc] & ESAT & (v1 & v2 & Eq1 & Eq2 & VREL)).
rewrite Eq1 Eq2. eapply (sim_body_end_call); [done..|].
intros c1 c2 cids1 cids2 Eqcs1 Eqcs2 σs' σt' r' WF VREL'. split; [|done].
rewrite Eqc in Eqcs2. simplify_eq.
rewrite /end_call_sat /=.
intros ??. simplify_eq.
intros. *)
admit.
- instantiate (1:=init_res). rewrite right_id. apply wsat_init_state.
split; last split; last split; [done|..|done].
{ exists O. by rewrite -STACK. }
rewrite /end_call_sat -STACK.
intros c Eq. simpl in Eq. simplify_eq.
have HL: (init_res r').2 !! 0%nat Some (to_callStateR csPub).
{ apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
by rewrite /= lookup_singleton. }
split. { destruct ((init_res r').2 !! 0%nat). by eexists. by inversion HL. }
intros r_f VALIDf T HL2. exfalso.
move : HL2. rewrite lookup_op HL. apply callStateR_exclusive_2.
- instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
Qed.
Supports Markdown
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