Library compile

Require Import ssreflect ssrbool.
Require Import Arith_ext Lists_ext.
Require while.
Require Import goto sgoto sgoto_hoare.

Module Compile (x : while.WHILE_HOARE_DETER).

Module Import sgoto_hoare_m := SGoto_Hoare x.
Import sgoto_m.
Import goto_deter_m.
Import goto_m.
Import x.

Module while_prop_m := while.While_Semop_Prop x.

Compilation from While to SGoto

This corresponds to Section 4 of [Saabas&Uustalu2007].

Compilation and Preservation/Reflection of Evaluations

Figure 5 (Rules of compilation from While to SGoto) in [Saabas&Uustalu2007]. A slight difference is that we do not remove nop instructions (they are sometimes important in MIPS assembly because of non-taken branch prediction).

Local Open Scope sgoto_scope.
Local Open Scope while_cmd_scope.

Import while.
Implicit Arguments ifte [cmd0 expr_b].
Implicit Arguments while [cmd0 expr_b].

Inductive compile : label -> @cmd cmd0 expr_b -> scode -> label -> Prop :=
| comp_cmd : forall l (c : cmd0), compile l c (sC l c) (S l)
| comp_seq : forall l l' l'' c d c' d',
  compile l c c' l'' -> compile l'' d d' l' -> compile l (c ; d) (c' [+] d') l'
| comp_ifte : forall l l' l'' t c d c' d',
  compile (S l'') c c' l' -> compile (S l) d d' l'' ->
  compile l (ifte t c d) (sB l (cjmp t (S l'')) [+] ((d' [+] sB l'' (jmp l')) [+] c')) l'
| comp_while : forall l l' t c prg, compile (S l) c prg l' ->
  compile l (while t c) (sB l (cjmp (neg t) (S l')) [+] (prg [+] sB l' (jmp l))) (S l').

Same as Figure 5 in [Saabas&Uustalu2007] but as a function, not a predicate.

Fixpoint compile_f l c {struct c} :=
match c with
  | cmd_cmd0 c => sC l c
  | seq c1 c2 =>
    let c1' := compile_f l c1 in
    let c2' := compile_f (l + length (sdom c1')) c2 in
    c1' [+] c2'
  | ifte t c1 c2 =>
    let c2' := compile_f (S l) c2 in
    let c1' := compile_f (l + length (sdom c2') + 2) c1 in
    sB l (cjmp t (l + length (sdom c2') + 2)) [+]
     ((c2' [+]
       sB ((S l) + length(sdom c2')) (jmp (l + length (sdom c2') + length (sdom c1') + 2))) [+]
       c1')
  | while t c =>
   let c' := compile_f (S l) c in
     sB l (cjmp (neg t) (l + length (sdom c') + 2)) [+]
     (c' [+]
     sB ((S l) + length (sdom c')) (jmp l))
end.

The above compilation-predicate and compilation-function are shown to be equivalent

Lemma compile_compile_f_cmd0 : forall (c : cmd0) l c' l',
  compile l c c' l' -> compile_f l c = c' /\ l' = S l.

Lemma compile_compile_f : forall c l c' l',
  compile l c c' l' -> compile_f l c = c' /\ l' = l + length (sdom c').

Lemma compile_f_compile_cmd0 : forall (c : cmd0) l c',
  compile_f l c = c' -> compile l c c' (l + length (sdom c')).

Lemma e_comp_ifte : forall l l' l'' t c d c' d' l'_ l''_ l_ c'_,
  compile l''_ c c' l'_ -> compile l_ d d' l'' ->
  c'_ = sB l (cjmp t (S l'')) [+] ((d' [+] sB l'' (jmp l')) [+] c') ->
  S l'' = l''_ -> l'_ = l' -> S l = l_ -> compile l (ifte t c d) c'_ l'.

Lemma e_comp_while : forall l l' t c prg c'_ l_ l'_, compile l_ c prg l' ->
  c'_ = sB l (cjmp (neg t) (S l')) [+] (prg [+] sB l' (jmp l)) ->
  S l = l_ -> S l' = l'_ -> compile l (while t c) c'_ l'_.

Lemma compile_f_compile : forall c l c',
  compile_f l c = c' -> compile l c c' (l + length (sdom c')).

Lemma compile_start_label_end_label : forall l c prg l', compile l c prg l' -> l < l'.

Lemma 13 (Totality and determinacy of compilation) in [Saabas&Uustalu2007]:

Lemma totality : forall l c, exists sc, exists l', compile l c sc l'.

Lemma determinacy : forall c l l' sc, compile l c sc l' ->
forall l'' sc', compile l c sc' l'' -> sc = sc' /\ l' = l''.

Lemma 14 (Domain of compiled code) in [Saabas&Uustalu2007]:

Lemma compile_sdom : forall c l sc l', compile l c sc l' ->
forall p, l <= p < l' -> In p (sdom sc).

Lemma compile_sdom' : forall c l sc l', compile l c sc l' ->
forall p, In p (sdom sc) -> l <= p < l'.

Various lemmas regarding the domain of the code and labels.

Lemma compile_sdom_open_right : forall sc l c l', compile l c sc l' -> ~ In l' (sdom sc).

Lemma compile_f_sdom_close_left : forall c sc l, compile_f l c = sc -> In l (sdom sc).

Lemma compile_sdom_close_left : forall l c sc l', compile l c sc l' -> In l (sdom sc).

Lemma compile_sdom_sS : forall c l l' c1 c2, compile l c (c1 [+] c2) l' ->
disj (sdom c1) (sdom c2).

Compilation always produces wellformed code:

Lemma compile_wellformed : forall c l sc l', compile l c sc l' -> wellformed sc.

Intermediate lemma for one-step instructions:

Lemma preservation_of_evaluations_cmd0 : forall (c : cmd0) s s',
  Some s -- c ---> Some s' -> forall l sc l', compile l c sc l' ->
    Some (l, s) >- sc ---> Some (l', s').

Lemma preservation_of_evaluations_cmd0_none : forall (c : cmd0) s,
  Some s -- c ---> None -> forall l sc l', compile l c sc l' ->
    Some (l, s) >- sc ---> None.

Ltac apply_compile_sdom_close_left :=
  match goal with
    | H : compile ?L ?C ?SC ?K |- In ?L (sdom ?SC) => eapply compile_sdom_close_left; eauto
    | |- In ?L (sdom (sB ?L _)) => simpl; auto
  end.

Ltac decompose_In :=
  match goal with
    | |- In ?L (sdom (sS ?SC0 ?SC1)) => simpl; apply in_or_app; try decompose_In
    | |- In ?L (sdom (sB ?L _)) => simpl; auto
    | |- In ?L (app ?D1 ?D2) => apply in_or_app; try decompose_In
    | |- In ?L (cons ?L (@nil label)) => simpl; auto
    | |- In ?L ?D1 \/ In ?L ?D2 => solve
        [ (left; try decompose_In) | (right; try decompose_In) ]
    | |- In ?L (sdom ?SC) => apply_compile_sdom_close_left
  end.

Lemma not_eq_false : forall A (a b : A), a <> b -> ~ (a = b \/ False ).

Lemma not_eq_P : forall A (a b : A) P, a <> b /\ ~ P -> ~ (a = b \/ P).

Ltac apply_compile_sdom_open_right :=
  match goal with
    | H : compile ?L ?C ?SC ?K |- ~ In ?K (sdom ?SC) => eapply compile_sdom_open_right; eauto
  end.

Ltac apply_compile_dom' :=
  match goal with
    | H : compile ?L ?C ?SC ?K |- ~ In ?M (sdom ?SC) =>
      let H1 := fresh in
        intro H1 ;
        generalize (compile_sdom' _ _ _ _ H _ H1) ; clear H ;
          let H2 := fresh in
          intro H2
  end.

Ltac apply_compile_start_label_end_label :=
  match goal with
    | H : compile ?L ?C ?SC ?K |- _ =>
      apply compile_start_label_end_label in H ;
          try apply_compile_start_label_end_label
  end.

Ltac not_in_sdom3_diff :=
  match goal with
    | |- ?L <> ?K => let H := fresh in intro H; solve [ omega |
        (subst L; apply_compile_start_label_end_label; omega) |
        (subst K; apply_compile_start_label_end_label; omega) ]
  end.

Ltac decompose_not_In :=
  match goal with
    | |- ~ In ?L (sdom (sS (sB ?L0 _) ?SC1)) =>
      simpl; apply not_eq_P; split; [ not_in_sdom3_diff | try decompose_not_In]
    | |- ~ In ?L (sdom (sS ?SC0 ?SC1)) =>
      simpl; apply not_in_app; [ try decompose_not_In | try decompose_not_In]
    | |- ~ In ?L (sdom (sB ?K _)) =>
      simpl; apply not_eq_false; not_in_sdom3_diff
    | |- ~ In ?L (app ?L0 ?L1) =>
      apply not_in_app; [ try decompose_not_In | try decompose_not_In]
    | |- ~ In ?L (cons ?L0 (@nil label)) =>
      simpl; apply not_eq_false; not_in_sdom3_diff
    | |- ~ In ?L (sdom ?SC) =>
      solve [ apply_compile_sdom_open_right |
        (apply_compile_dom'; apply_compile_start_label_end_label; omega) ]
  end.

Lemma preservation_of_evaluations' : forall c s s', s -- c ---> s' ->
  forall n c' m, compile n c c' m -> forall st, s = Some st ->
    (forall st', s' = Some st' -> Some (n, st) >- c' ---> Some (m, st')) /\
    (s' = None -> Some (n, st) >- c' ---> None ).

Theorem 15 (Preservation of evaluations) in [Saabas&Uustalu2007]:

Lemma preservation_of_evaluations : forall c s l sc s' l', compile l c sc l' ->
Some s -- c ---> Some s' -> Some (l, s) >- sc ---> Some (l + length (sdom sc), s').

Intermediate lemmas for commands:

Lemma reflection_of_evaluations_sC : forall l (c : cmd0) sc l', compile l c sc l' ->
  forall s lstar s', Some (l, s) >- sc ---> Some (lstar, s') ->
    lstar = l' /\ (Some s -- c ---> Some s').

Local Open Scope goto_scope.

Lemma reflection_of_evaluations_sC_none' : forall (c : cmd0),
  forall l s, c ||- Some (l, s) ---> None -> Some s -- c ----> None.

Lemma reflection_of_evaluations_sC_none'' : forall (c : cmd0),
  forall l s, Some (l, s) >- sC l c ---> None -> Some s -- c ----> None.

Lemma reflection_of_evaluations_sC_none''' : forall (c : cmd0) l s,
  Some (l, s) >- compile_f l c ---> None -> Some s -- c ----> None.

Lemma reflection_of_evaluations_sC_none : forall (c : cmd0) l s l' sc,
  compile l c sc l' -> Some (l, s) >- sc ---> None -> Some s -- c ----> None.

Theorem 16 (Preservation of evaluations) in [Saabas&Uustalu].

This proof is done by a nested induction to handle the while-case. We isolate this subcase by intermediate lemmas (one lemma for the error-free case and another lemma for the error case). Here follows the intermediate lemma for the error-free case; what will be the outer induction hypothesis in the main proof is given as an hypothesis to this intermediate lemma.

Lemma reflection_of_evaluations' : forall c_t
  (IHouter : forall l sc_t l' s s' lstar, compile l c_t sc_t l' ->
    Some (l, s) >- sc_t ---> Some (lstar, s') ->
    lstar = l' /\ Some s -- c_t ---> Some s') sc st st',
  st >- sc ---> st' ->
  forall l l' t, compile l (while t c_t) sc l' ->
    forall s lstar s' L, L = l \/ L = S l ->
      eval_b t s -> st = Some (L, s) -> st' = Some (lstar, s') ->
      lstar = l' /\ Some s -- while t c_t ---> Some s'.

Lemma reflection_of_evaluations'' : forall c_t
  (IHouter : forall l sc l', compile l c_t sc l' -> forall s,
    (forall lstar s', Some (l, s) >- sc ---> Some (lstar, s') ->
      lstar = l' /\ Some s -- c_t ---> Some s') /\
    (Some (l, s) >- sc ---> None -> Some s -- c_t ---> None )) sc st st',
  st >- sc ---> st' ->
  forall l l' t, compile l (while t c_t) sc l' ->
    forall s L, L = l \/ L = S l ->
      eval_b t s -> st = Some (L, s) -> st' = None ->
      Some s -- while t c_t ---> None.

Lemma reflection_of_evaluations : forall c l sc l', compile l c sc l' ->
  forall s, (forall lstar s',
    Some (l, s) >- sc ---> Some (lstar, s') -> lstar = l' /\ Some s -- c ---> Some s') /\
  (Some (l, s) >- sc ---> None -> Some s -- c ---> None ).

Preservation/Reflection of Derivable Hoare Triples

Theorem 17 (Preservation of derivable Hoare triples) in [Saabas&Uustalu]. The proof of this theorem makes use of the soundness of Hoare logic for While; this is the lemma soundness used below.

Local Open Scope while_hoare_scope.
Local Open Scope sgoto_hoare_scope.

Module while_hoare_prop_m := While_Hoare_Prop x.

Lemma preservation_hoare : forall P Q c, {{ P }} c {{ Q }} ->
  forall l sc l', compile l c sc l' ->
    [^ fun pc => fun s h => pc = l /\ P s h ^] sc [^ fun pc => fun s h => pc = l' /\ Q s h ^].
Proof.
move=> P Q c Hoare l sc l' Hcompile.
apply hoare_sgoto_complete; first by eapply compile_wellformed; eauto.
move=> l0 s h [-> HP] {l0}.
move/while_hoare_prop_m.soundness: Hoare.
case/(_ _ _ HP) => Herror_free HQ.
move/reflection_of_evaluations: Hcompile.
case/(_ (s, h)) => Hcompile1 Hcompile2.
split.
- by move=> X; apply Hcompile2 in X.
- move=> l'_ s' h' Hexec.
  case/Hcompile1 : Hexec => l'_l'.
  by move/HQ.
Qed.

Theorem 18 (Reflection of derivable Hoare triples). The proof of this theorem uses in particular the completeness of Hoare-logic for While.

Lemma reflection_hoare : forall l c sc l', compile l c sc l' ->
  forall P Q, [^ P ^] sc [^ Q ^] -> {{ P l }} c {{ Q l' }}.
Proof.
move=> l c sc l' Hcompile P Q.
move/hoare_sgoto_sound => Hoare_semantics.
apply while_hoare_prop_m.hoare_complete => s h.
case/Hoare_semantics => Herror_free HQ.
split.
- contradict Herror_free.
  by apply (proj2 (preservation_of_evaluations' _ _ _ Herror_free _ _ _ Hcompile _ (refl_equal _)) (refl_equal _)).
- move=> s' h'.
  move/(preservation_of_evaluations _ _ _ _ _ _ Hcompile) => Hexec.
  move/HQ : {HQ} Hexec => HQ.
  by case/compile_compile_f : Hcompile => _ ->.
Qed.

Bibliography: [Saabas&Uustalu] Ando Saabas and Tarmo Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Theor. Comput. Sci. 373(3): 273-302, Elsevier 2007. [Affeldt&Marti] Reynald Affeldt and Nicolas Marti. An Approach to Formal Verification of Arithmetic Functions in Assembly. ASIAN 2006. LNCS 4435, pp. 346-360, Springer 2008.

End Compile.