Lvc.Coherence.Allocation

Require Import CSet Le.

Require Import Plus Util Map DecSolve.
Require Import Env EnvTy IL Annotation Liveness Coherence Alpha Restrict RenamedApart.
Require Import RenamedApart_Liveness.

Set Implicit Arguments.

Local Injectivity

Inductive definition of local injectivity of a renaming rho

Inductive locally_inj (rho:env var) : stmt → ann (set var) → Prop :=
| RNOpr x b lv e (al:ann (set var))
  : locally_inj rho b al
  → injective_on lv rho

  → locally_inj rho (stmtLet x e b) (ann1 lv al)
| RNIf x b1 b2 lv (alv1 alv2:ann (set var))
  : injective_on lv rho
  → locally_inj rho b1 alv1
  → locally_inj rho b2 alv2
  → locally_inj rho (stmtIf x b1 b2) (ann2 lv alv1 alv2)
| RNGoto l Y lv
  : injective_on lv rho
  → locally_inj rho (stmtApp l Y) (ann0 lv)
| RNReturn x lv
  : injective_on lv rho
  → locally_inj rho (stmtReturn x) (ann0 lv)
| RNExtern x f Y b lv (al:ann (set var))
  : locally_inj rho b al
  → injective_on lv rho

  → locally_inj rho (stmtExtern x f Y b) (ann1 lv al)
| RNLet s Z b lv (alvs alvb:ann (set var))
  : locally_inj rho s alvs
  → locally_inj rho b alvb
  → injective_on lv rho

  → locally_inj rho (stmtFun Z s b) (ann2 lv alvs alvb).

Some Properties

local injectivity can only hold if lv is a valid annotation

Lemma locally_inj_annotation (ϱ:env var) (s:stmt) (lv:ann (set var))
: locally_inj ϱ s lv → annotation s lv.

local injectivity respects functional equivalence (if the function itself is injective wrt. the underlying equivalence)

Global Instance locally_inj_morphism
: Proper (@fpeq _ _ eq _ _ ==> eq ==> eq ==> impl) locally_inj.

local injectivity means injectivity on the live variables

Lemma locally_injective s (slv:ann (set var)) ϱ
: locally_inj ϱ s slv
→ injective_on (getAnn slv) ϱ.

local injectivity is decidable

Definition locally_inj_dec (ϱ:env var) (s:stmt) (lv:ann (set var)) (an:annotation s lv)
  : {locally_inj ϱ s lv } + {¬ locally_inj ϱ s lv }.

Instance locally_inj_dec_inst (ϱ:env var) (s:stmt) (lv:ann (set var))
         `{Computable (annotation s lv)}
  : Computable (locally_inj ϱ s lv).

Renaming with a locally injective renaming yields a coherent program

Lemma rename_renamedApart_srd s ang ϱ (alv:ann (set var)) Lv
  : renamedApart s ang
  → (getAnn alv ) ⊆ fst (getAnn ang)
  → live_sound FunctionalAndImperative Lv s alv
  → locally_inj ϱ s alv
  → bounded (live_globals Lv) (fst (getAnn ang))
  → srd (map_lookup ϱ (restrict (live_globals Lv) (getAnn alv)))
        (rename ϱ s)
        (mapAnn (lookup_set ϱ) alv).

Lemma locally_inj_subset ϱ s alv alv´
: locally_inj ϱ s alv
  → ann_R Subset alv´ alv
  → locally_inj ϱ s alv´.

Lemma bounded_disjoint Lv u v
: bounded (live_globals Lv) u
  → disj u v
  → disjoint (live_globals Lv) v.

Lemma meet1_incl2 a b
: Subset1 (meet1 a b) b.

Lemma meet1_Subset1 s alv ang
: annotation s alv
  → annotation s ang
  → ann_R Subset1 (mapAnn2 meet1 alv ang) ang.

Lemma rename_renamedApart_srd´ s ang ϱ (alv:ann (set var)) Lv
  : renamedApart s ang
  → live_sound Imperative Lv s alv
  → locally_inj ϱ s alv
  → bounded (live_globals Lv) (fst (getAnn ang))
  → LabelsDefined.noUnreachableCode s
  → srd
        (map_lookup ϱ
           (restrict (live_globals Lv) (getAnn (mapAnn2 meet1 alv ang))))
        (rename ϱ s) (mapAnn (lookup_set ϱ) (mapAnn2 meet1 alv ang)).

Require Import LabelsDefined.

Theorem 6 from the paper.

The generalization to the paper version is that we do not bound by the free variables, but by a set that that contains the free variables and is disjoint with any variables occuring in binding positions in s; this set is fst (getAnn ang)

Lemma rename_renamedApart_srd´´ s ang ϱ (alv:ann (set var)) Lv
  : renamedApart s ang
    → live_sound Imperative Lv s alv
    → ann_R Subset1 alv ang
    → locally_inj ϱ s alv
    → bounded (live_globals Lv) (fst (getAnn ang))
    → noUnreachableCode s
    → srd (map_lookup ϱ (restrict (live_globals Lv) (getAnn alv)))
          (rename ϱ s)
          (mapAnn (lookup_set ϱ) alv).

Open Scope set_scope.

Renaming with a locally injective renaming yields an α-equivalent program

Lemma renamedApart_locally_inj_alpha s ϱ ϱ´ DL (slv:ann (set var)) ang
  : renamedApart s ang
  → locally_inj ϱ s slv
  → live_sound Functional DL s slv
  → inverse_on (getAnn slv) ϱ ϱ´
  → alpha ϱ ϱ´ s (rename ϱ s).

Lemma renamedApart_locally_inj_alpha´ s ϱ ϱ´ Lv alv ang
  : renamedApart s ang
  → live_sound Imperative Lv s alv
  → locally_inj ϱ s alv
  → bounded (live_globals Lv) (fst (getAnn ang))
  → LabelsDefined.noUnreachableCode s
  → inverse_on (getAnn alv) ϱ ϱ´
  → alpha ϱ ϱ´ s (rename ϱ s).

Theorem 7 from the paper

the generalization is analogous to the generalization in Theorem 6

Lemma renamedApart_locally_inj_alpha´´ s ϱ ϱ´ DL (slv:ann (set var)) ang
  : renamedApart s ang
  → locally_inj ϱ s slv
  → live_sound Imperative DL s slv
  → inverse_on (getAnn slv) ϱ ϱ´
  → ann_R Subset1 slv ang
  → bounded (live_globals DL) (fst (getAnn ang))
  → noUnreachableCode s
  → alpha ϱ ϱ´ s (rename ϱ s).

local injectivity only looks at variables occuring in the program

Lemma locally_inj_live_agree s ϱ ϱ´ ara alv LV
      (LS:live_sound FunctionalAndImperative LV s alv)
      (sd: renamedApart s ara)
      (inj: locally_inj ϱ s alv)
      (agr: agree_on eq (fst (getAnn ara) ∪ snd (getAnn ara)) ϱ ϱ´)
      (incl:getAnn alv ⊆ fst (getAnn ara))
: locally_inj ϱ´ s alv.