Library Compiler

Compiler from GC to IC

We show the correctness of a compiler from GC to IC.
Require Import Facts States GCSemantics ICSemantics.
Set Implicit Arguments.
Unset Strict Implicit.

Module Compiler (Sigma : State).
Module GCSem := GCSemantics.GCSemantics Sigma.
Module ICSem := ICSemantics.ICSemantics Sigma.
Export ICSem.
Export GCSem.

Definition of the compiler

Definition simple s := if s is Jump _ then true else false.

Definition LetDef (s : term) (t : {bind term}) : term :=
  if simple s then t.[s/] else Def s.[ren (+1)] t.

Definition flatmap (f : cmdterm) (u : term) : gcterm :=
  fix rec G := match G with
  | [::]u
  | (b,s) :: GIf b (f s) (rec G)

Definition abort : term := Def (Jump 0) (Jump 0).

Fixpoint comp (u : term) (s : cmd) : term :=
  match s with
    | Skipu
    | Assn aAct a u
    | Seq s tcomp (comp u t) s
    | Case [::]abort
    | Case ((_,s) :: G) ⇒ LetDef u (flatmap (comp (Jump 0)) (comp (Jump 0) s) G)
    | Do GDef (flatmap (comp (Jump 0)) u.[ren (+1)] G) (Jump 0)
Local Notation compile := (comp (Jump 0)).

Semantics for let

Lemma fix_weaken Q s x :
  Fix (fun Pwp (P .: Q) s.[ren (+1)]) x wp Q s x.
  split. apply: wp_fix. by rewrite wp_ren. movewps.
  apply: fix_fold. by rewrite wp_ren.

Lemma wp_let Q s t x :
  wp Q (LetDef s t) x wp (wp Q s .: Q) t x.
  rewrite/LetDef. case: ifP_/=. rewrite wp_subst. by apply: wp_equiv ⇒ -[].
  apply: wp_equiv ⇒ -[]//=y. by rewrite fix_weaken.

Guarded Commands in IC via flattening.

Section Flatten.

Variable (Q : NPred state) (f : cmdterm) (u : term) (x : state).
Implicit Types (G : gc).

Lemma flatmap_sound G :
  ( (b : guard) (s : cmd), (b, s) \in Gb xwp Q (f s) x) →
  (~~G xwp Q u x) →
  wp Q (flatmap f u G) x.
  elim: G ⇒ //=[|[e s]G ih]h1 h2/=. exact: h2. case: ifPnp.
  - apply: h1 p. exact: mem_head.
  - apply: ih ⇒ [b t|]h3. apply: h1. exact: mem_behead. apply: h2.
      by rewrite gtest_cons negb_or p.

Lemma flatmap_soundT G :
  ( (b : guard) (s : cmd), (b, s) \in Gb xwp Q (f s) x) →
  G x
  wp Q (flatmap f u G) x.
  moveh1 h2. apply: flatmap_sound h1 _. by rewrite h2.

Lemma flatmap_soundF G :
  ~~G xwp Q u xwp Q (flatmap f u G) x.
  movegt h. apply: flatmap_sound ⇒ // b s h1 h2. exfalso.
  move/gtestP: gt ⇒ []; eauto.

End Flatten.

Compiler correctness

Lemma compile_correct´ (P : Pred state) (x : state) (s : cmd) :
  wps P s x
   (Q : NPred state) (u : term),
    P <<= wp Q u
    wp Q (comp u s) x.
  elim⇒ {P s x}/=[|||P [//|[e s]G]x h _ ih Q k hk|
    P G x I gt _ ih1 _ ih2 Q k hk|P G x gt Qa Q k hk]; eauto.
  - apply/wp_let. apply: flatmap_sound ⇒ [b t h1/ih{ih}ih|/negbTE hG].
    + apply: ih ⇒ //. by rewrite inE h1 orbT.
    + apply: (ih e s) ⇒ //=. by rewrite inE eqxx.
      move: h. by rewrite gtest_cons hG orbF.
  - apply: fix_fold. apply: flatmap_soundT gtb s h1 h2.
    apply: ih1 h1 h2 _ _ _beta ib /=. exact: ih2.
  - apply: fix_fold. apply: flatmap_soundF ⇒ //.
    rewrite wp_weaken. exact: hk.

Theorem compile_correct (Q : Pred state) (s : cmd) :
  wps Q s <<= wp (Q .: @Bot _) (compile s).
Proof. movex/compile_correct´. exact. Qed.

End Compiler.