Commit aebc4604 authored by Hai Dang's avatar Hai Dang Committed by Jeehoon Kang
Browse files

Prove the global adequacy

parent ac71fcd9
......@@ -13,8 +13,10 @@ theories/lang/steps_progress.v
theories/lang/steps_inversion.v
theories/lang/examples.v
theories/sim/global.v
theories/sim/global_adequacy.v
theories/sim/cmra.v
theories/sim/invariant.v
theories/sim/local.v
theories/sim/adequacy.v
theories/sim/local_adequacy.v
theories/sim/sflib.v
theories/opt/foo.v
......@@ -59,6 +59,8 @@ Inductive tstep (fns: fn_env) (eσ1 eσ2 : expr * state) : Prop :=
Notation "x ~{ fn }~> y" := (tstep fn x y) (at level 70, format "x ~{ fn }~> y").
Notation "x ~{ fn }~>* y" := (rtc (tstep fn) x y)
(at level 70, format "x ~{ fn }~>* y").
Notation "x ~{ fn }~>+ y" := (tc (tstep fn) x y)
(at level 70, format "x ~{ fn }~>+ y").
(*=================================== UNUSED =================================*)
(* Implicit Type (ρ: cfg bor_lang). *)
......
From Paco Require Import paco.
From stbor.lang Require Import steps_wf.
From stbor.sim Require Import global.
Set Default Proof Using "Type".
(** Behaviors ----------------------------------------------------------------*)
Inductive behavior := | Term (v: value) | Stuck | Diverges.
Inductive behaviors (fns: fn_env)
(step: fn_env expr * state expr * state Prop)
(cfg: expr * state) : behavior Prop :=
| behaviors_term v
(TERMINAL: to_result cfg.1 = Some (ValR v)) :
behaviors fns step cfg (Term v)
| behaviors_stuck
(NT: ¬ terminal cfg.1)
(NS: cfg', ¬ step fns cfg cfg') :
behaviors fns step cfg Stuck
(* | behaviors_diverges
(DIV: diverges step cfg) :
behaviors step cfg Diverges *)
| behaviors_step cfg' ov
(STEP: step fns cfg cfg')
(NEXT: behaviors fns step cfg' ov):
behaviors fns step cfg ov
.
(* If c1 ->* c2 -b-> v then c1 -b-> v *)
Lemma rtc_step_behavior fns step c1 c2 v
(STEPS: rtc (step fns) c1 c2) (BEH: behaviors fns step c2 v):
behaviors fns step c1 v.
Proof.
induction STEPS as [|c1 c2 c3 S1 S2 IH]; [done|]. specialize (IH BEH).
econstructor 3; eauto.
Qed.
Lemma sim_adequacy fns fnt (cfg_src cfg_tgt: expr * state)
(NO_UB: no_UB fns cfg_src)
(SIM: sim fns fnt cfg_src cfg_tgt) :
behaviors fns tstep cfg_tgt <1= behaviors fnt tstep cfg_src.
Proof.
intros ov BEH. revert cfg_src NO_UB SIM.
induction BEH as [cfg_tgt(* |cfg_tgt *)|cfg_tgt v|cfg_tgt cfg_tgt' ov STEP BEH IH];
intros cfg_src NO_UB SIM.
- punfold SIM.
(* destruct (SIM WFS WFT) as [? (* ? *) TERM ?]; [naive_solver|].
destruct TERM as (eσ2 & TS & TERM' & VAL); [by eexists|].
apply (rtc_step_behavior _ _ _ _ TS).
constructor. by apply VAL.
- punfold SIM. destruct (SIM WFS WFT) as [SU]; [naive_solver|].
destruct SU as (eσ2 & TS' & IN & NR).
+ split; [by apply expr_terminal_False|].
intros ???? PRIM. eapply (NS (e', σ')). econstructor; eauto.
+ apply (rtc_step_behavior _ _ _ _ TS').
constructor 2; [by apply expr_terminal_False|].
intros ? RED. inversion RED. by apply (NR _ _ _ _ PRIM).
(* - punfold SIM. destruct (SIM WFS WFT SIM0) as (SU & DIV & ?); [naive_solver|].
constructor. by apply DIV. *)
- punfold SIM.
destruct (SIM WFS WFT) as [SU (* DIV *) TERM TS]; [naive_solver|].
destruct (TS cfg_tgt' STEP) as (eσ & STEP' & TS').
eapply rtc_step_behavior; first by apply STEP'.
eapply IH; simpl.
+ by apply (rtc_tstep_wf _ _ STEP').
+ by apply (tstep_wf _ _ STEP).
+ clear -STEP' NO_UB. induction STEP'. done.
apply IHSTEP'. admit.
+ by inversion TS'. *)
Abort.
......@@ -16,7 +16,7 @@ Proof.
- move => e1 e2 e3 S1 S2 v3 /S2 /S1 //.
Qed.
Notation SIM_CONFIG := (expr * state expr * state Prop)%type.
Notation SIM_CONFIG := (nat -> expr * state expr * state Prop)%type.
(* This is a simulation between two expressions without any interference.
It corresponds to a sequential simulation. *)
......@@ -24,7 +24,7 @@ Notation SIM_CONFIG := (expr * state → expr * state → Prop)%type.
Section sim.
Variable (fns fnt: fn_env).
Record sim_base (sim: SIM_CONFIG) (eσ1_src eσ1_tgt: expr * state) : Prop := mkSimBase {
Record sim_base (sim: SIM_CONFIG) (idx1: nat) (eσ1_src eσ1_tgt: expr * state) : Prop := mkSimBase {
(* (1) If [eσ1_tgt] gets stuck, [eσ1_src] can also get stuck. *)
sim_stuck :
stuck (Λ:= bor_lang fnt) eσ1_tgt.1 eσ1_tgt.2 eσ2_src,
......@@ -38,31 +38,26 @@ Record sim_base (sim: SIM_CONFIG) (eσ1_src eσ1_tgt: expr * state) : Prop := mk
(* (4) If [eσ1_tgt] steps to [eσ2_tgt] with 1 step,
then exists [eσ2_src] s.t. [eσ1_src] steps to [eσ2_src] with * step. *)
sim_step :
eσ2_tgt, eσ1_tgt ~{fnt}~> eσ2_tgt eσ2_src,
eσ1_src ~{fns}~>* eσ2_src sim eσ2_src eσ2_tgt;
eσ2_tgt, eσ1_tgt ~{fnt}~> eσ2_tgt idx2 eσ2_src,
(eσ1_src ~{fns}~>+ eσ2_src \/ ((idx2 < idx1)%nat /\ eσ1_src = eσ2_src))
sim idx2 eσ2_src eσ2_tgt;
}.
Definition no_UB (eσ: expr * state) : Prop :=
¬ ( eσ', eσ ~{fns}~>* eσ' stuck (Λ:= bor_lang fns) eσ'.1 eσ'.2).
(* Generator for the actual simulation *)
Definition _sim
(sim : SIM_CONFIG) (eσ1_src eσ1_tgt: expr * state) : Prop :=
Wf eσ1_src.2 Wf eσ1_tgt.2
(* If [eσ1_src] gets UB, we can have UB in the target, thus any [eσ1_tgt] is
acceptable. Otherwise ... *)
no_UB eσ1_src sim_base sim eσ1_src eσ1_tgt.
(sim : SIM_CONFIG) (idx1: nat) (eσ1_src eσ1_tgt: expr * state) : Prop :=
Wf eσ1_src.2 Wf eσ1_tgt.2 sim_base sim idx1 eσ1_src eσ1_tgt.
Lemma _sim_mono : monotone2 (_sim).
Lemma _sim_mono : monotone3 (_sim).
Proof.
intros eσ_src eσ_tgt r r' TS LE WF1 WF2 NUB.
destruct (TS WF1 WF2 NUB) as [SU (* DI *) TE ST]. repeat split; auto.
intros eσ2_tgt ONE. destruct (ST _ ONE) as (eσ2_src & STEP1 & Hr).
exists eσ2_src. split; [done|]. by apply LE.
intros idx1 eσ_src eσ_tgt r r' TS LE WF1 WF2.
destruct (TS WF1 WF2) as [SU (* DI *) TE ST]. repeat split; auto.
intros eσ2_tgt ONE. destruct (ST _ ONE) as (idx2 & eσ2_src & STEP1 & Hr).
exists idx2, eσ2_src. split; [done|]. by apply LE.
Qed.
(* Global simulation *)
Definition sim : SIM_CONFIG := paco2 _sim bot2.
Definition sim : SIM_CONFIG := paco3 _sim bot3.
End sim.
......
From Coq Require Import Program.Equality Lia.
From Paco Require Import paco.
From stbor.lang Require Import steps_wf.
From stbor.sim Require Import global invariant sflib.
Set Default Proof Using "Type".
(** Behaviors ----------------------------------------------------------------*)
Section BEHAVIOR.
Context {Config State Value: Type}
(step: forall (conf:Config) (s s':State), Prop)
(term: forall (conf:Config) (s:State) (val:Value), Prop)
.
Inductive observation: Type :=
| obs_term (retval:Value)
| obs_inftau
.
Inductive behmatch
(conf:Config)
(behave: forall (s:State) (obs:observation), Prop)
: forall (s:State) (obs:observation), Prop :=
| beh_stuck
s obs
(NT: forall val, ¬ term conf s val)
(NS: s', ¬ step conf s s')
: behmatch conf behave s obs
| beh_term
s v
(TERM: term conf s v)
: behmatch conf behave s (obs_term v)
| beh_inftau
s s'
(STEP: step conf s s')
(INF: behave s' obs_inftau)
: behmatch conf behave s obs_inftau
.
Hint Constructors behmatch.
Inductive behave_ (conf:Config) behave (s:State) (obs:observation): Prop :=
| behave_intro
s'
(TAU: rtc (step conf) s s')
(MAT: behmatch conf behave s' obs)
.
Hint Constructors behave_.
Lemma behave_mon conf: monotone2 (behave_ conf).
Proof.
repeat intro. destruct IN. destruct MAT; eauto.
Qed.
Hint Resolve behave_mon: paco.
Definition behave (conf:Config): forall (s:State) (obs:observation), Prop := paco2 (behave_ conf) bot2.
End BEHAVIOR.
Hint Constructors behmatch.
Hint Constructors behave_.
Hint Resolve behave_mon: paco.
Definition init_expr := (Call #["main"] []).
Definition init_state := (mkState [] O O).
Definition term (prog:fn_env) (s:expr * state) (v:value): Prop :=
to_result s.1 = Some (ValR v).
Definition behave_prog (prog:fn_env) (obs:@observation value): Prop :=
behave tstep term prog (init_expr, init_state) obs.
(* TODO: move *)
Lemma tc_inv_l
A (R:relation A) x z
(TC: tc R x z):
exists y, rtc R x y /\ R y z.
Proof.
induction TC.
- esplits; eauto. reflexivity.
- des. esplits; [|by eauto]. eapply rtc_l; eauto.
Qed.
(* TODO: move *)
Lemma strong_induction
(P : nat -> Prop)
(IH: forall (n:nat) (IH: forall (k:nat) (LT: (k < n)%nat), P k), P n):
forall n : nat, P n.
Proof.
i. cut (forall (m k:nat), (k < m -> P k)%nat); [by eauto|].
induction m.
- i. nia.
- i. apply lt_le_S in H. inv H; eauto.
Qed.
Lemma adequacy
prog_src prog_tgt idx conf_src conf_tgt
(SIM: sim prog_src prog_tgt idx conf_src conf_tgt)
: behave tstep term prog_tgt conf_tgt <1= behave tstep term prog_src conf_src.
Proof.
revert idx conf_src conf_tgt SIM. pcofix CIH. intros.
punfold PR. inv PR.
rename x2 into obs. rename s' into conf'_tgt. revert idx conf_src SIM MAT.
dependent induction TAU; cycle 1.
- rename x into conf_tgt.
rename y into conf'_tgt.
rename z into conf''_tgt.
i. punfold SIM. exploit SIM.
{ admit. (* WF *) }
{ admit. (* WF *) }
clear SIM. intro SIM. inv SIM.
exploit sim_step; eauto. i. des.
+ inv x0; ss.
rename eσ2_src into conf'_src.
exploit IHTAU; eauto.
intro BEH. punfold BEH. inv BEH.
pfold. econs; [|by eauto]. etrans; eauto. apply tc_rtc. ss.
+ inv x0; ss.
rename eσ2_src into conf'_src.
exploit IHTAU; eauto.
- intros idx. revert x.
induction idx using strong_induction. i.
punfold SIM. exploit SIM.
{ admit. (* WF *) }
{ admit. (* WF *) }
clear SIM. intro SIM. inv SIM. inv MAT.
+ exploit sim_stuck; eauto.
{ admit. (* property of stuck *) }
i. des.
pfold. econs; eauto.
admit. (* property of stuck *)
+ exploit sim_terminal; eauto. i. des.
pfold. econs; eauto.
econs 2.
admit. (* property of terminal *)
+ pclearbot. exploit sim_step; eauto. i. des.
* inv x1; ss.
exploit CIH; eauto. i.
apply tc_inv_l in x0. des.
pfold. econs; eauto.
* inv x1; ss. exploit IH; eauto.
punfold INF. inv INF. inv TAU; eauto.
econs 3; eauto.
Admitted.
From Coq Require Import Program.Equality Lia.
From Paco Require Import paco.
From stbor.lang Require Import steps_wf.
From stbor.sim Require Import global invariant sflib.
Set Default Proof Using "Type".
This diff is collapsed.
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