Lvc.Coherence.Coherence

Definition of Coherence: srd

Inductive srd : list (option (set var)) → stmt → ann (set var) → Prop :=
| srdExp DL x e s lv al
    : srd (restrict DL (lv \{{x }})) s al
    → srd DL (stmtLet x e s) (ann1 lv al)
  | srdIf DL e s t lv als alt
    : srd DL s als
    → srd DL t alt
    → srd DL (stmtIf e s t) (ann2 lv als alt)
  | srdRet e DL lv
    : srd DL (stmtReturn e) (ann0 lv)
  | srdGoto DL lv G´ f Y
    : get DL (counted f) (Some G´)
    → srd DL (stmtApp f Y) (ann0 lv)
| srdExtern DL x f Y s lv al
    : srd (restrict DL (lv \{{x }})) s al
    → srd DL (stmtExtern x f Y s) (ann1 lv al)
  | srdLet DL s t Z lv als alt
    : srd (restrict (Some (getAnn als \ of_list Z)::DL) (getAnn als \ of_list Z))
          s als
    → srd (Some (getAnn als \ of_list Z)::DL) t alt
    → srd DL (stmtFun Z s t) (ann2 lv als alt).

Definition srd_dec DL s a
: Computable (srd DL s a).

Lemma srd_monotone (DL DL´ : list (option (set var))) s a
: srd DL s a
   → PIR2 (fstNoneOrR Equal) DL DL´
   → srd DL´ s a.

Lemma srd_monotone2 (DL DL´ : list (option (set var))) s a
: srd DL s a
   → PIR2 (fstNoneOrR (flip Subset)) DL DL´
   → srd DL´ s a.

Note that this lemma also builds the liveness annotation: It exploits that we can always claim more variables live

Definition rd_agree (DL:list (option (set var)))
           L (E:onv val)
  := ∀ n blk G´, get L n blk → get DL n (Some G´) →
                      agree_on eq G´ E (F.block_E blk).

Lemma rd_agree_update DL L E G x v
(RA:rd_agree DL L E)
  : rd_agree (restrict DL (G \ {{x }})) L (E [x <- v ]).

Lemma rd_agree_update_list DL L E E´ (G G´:set var) Z n vl
(RA:rd_agree DL L E)
(ZD:of_list Z ∩ G´ [=] ∅)
(LEQ:length Z = length vl)
(AG:agree_on eq G´ E E´)
: rd_agree (restrict (drop n DL) G´) (drop n L) (E´[Z <-- vl ]).

Inductive approxF
  : list (option (set var)) → list (set var × list var) → F.block → Prop :=
  approxI´ AL DL o Z E s
  : (∀ G, o = Some G → of_list Z ∩ G [=] ∅ ∧
           ∃ a, getAnn a [=] (G ∪ of_list Z )
                ∧ srd (restrict (Some G ::AL) G) s a
                ∧ live_sound Imperative DL s a)
     → approxF (o ::AL) DL (F.blockI E Z s).

Stability under restriction

The rough slogan of what we show here is that the set of coherent states is closed under reduction

Lemma srd_preservation (E E´:onv val) L L´ s s´ DL (G:set var) DA a e
  (SRD:srd DA s a)
  (RA:rd_agree DA L E)
  (A: AIR21 approxF DA DL L)
  (LV:live_sound Imperative DL s a)
  (S:F.step (L , E , s ) e (L´,E´,s´))
  : ∃ DA´ DL´ a´, srd DA´ s´ a´
                   ∧ rd_agree DA´ L´ E´
                   ∧ AIR21 approxF DA´ DL´ L´.

context coherence for imperative states (not required in the soundess proof)

Inductive approxI
  : list (option (set var)) → list (set var × list var) → I.block → Prop :=
  approxII´ AL DL o Z s i
  : (∀ G, o = Some G → of_list Z ∩ G [=] ∅ ∧
           ∃ a, getAnn a [=] (G ∪ of_list Z )
                ∧ srd (restrict (Some G ::AL) G) s a
                ∧ live_sound i DL s a)
     → approxI (o ::AL) DL (I.blockI Z s).

Lemma approxI_restrict AL DL L G
: AIR21 approxI AL DL L
  → AIR21 approxI (restrict AL G) DL L.

Lemma srd_preservation_I (E E´:onv val) L L´ s s´ DL (G:set var) DA a e i
  (SRD:srd DA s a)
  (A: AIR21 approxI DA DL L)
  (LV:live_sound i DL s a)
  (S:I.step (L , E , s ) e (L´,E´,s´))
  : ∃ DL´ DA´ a´, srd DA´ s´ a´ ∧ AIR21 approxI DA´ DL´ L´.

stripB removes the environment from a closure

Definition stripB (b:F.block) : I.block :=
  match b with
    | F.blockI E Z s ⇒ I.blockI Z s
  end.

Definition strip := List.map stripB.

Lemma drop_strip n L
  : drop n (strip L) = strip (drop n L).

The Bisimulation candidate.

Inductive srdSim : F.state → I.state → Prop :=
  | srdSimI (E EI:onv val) L s AL DL a
  (SRD:srd AL s a)
  (RA:rd_agree AL L E)
  (A: AIR21 approxF AL DL L)
  (AG:agree_on eq (getAnn a) E EI)
  (LV:live_sound Imperative DL s a)
  (ER:PIR2 eqReq AL DL)
  : srdSim (L , E , s ) (strip L , EI ,s ).

The bisimulation is indeed a bisimulation

Lemma srdSim_sim σ1 σ2
: srdSim σ1 σ2 → bisim σ1 σ2.