Library compile


Module Compile (x : while.WHILE_HOARE_DETER).

Module Import sgoto_hoare_m := SGoto_Hoare 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).



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 :=
 match c with
  | cmd_cmd0 c => sC l c
  | seq c1 c2 =>
    let c1' := compile_f l c1 in
    let c2' := compile_f (l + size (sdom c1')) c2 in
    c1' [+] c2'
  | ifte t c1 c2 =>
    let c2' := compile_f (S l) c2 in
    let c1' := compile_f (l + size (sdom c2') + 2) c1 in
    sB l (cjmp t (l + size (sdom c2') + 2)) [+]
     ((c2' [+]
       sB ((S l) + size (sdom c2')) (jmp (l + size (sdom c2') + size (sdom c1') + 2))) [+]
       c1')
  | while t c =>
   let c' := compile_f (S l) c in
     sB l (cjmp (neg t) (l + size (sdom c') + 2)) [+]
     (c' [+]
     sB ((S l) + size (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 + size (sdom c').

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


Lemma e_comp_ifte 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 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 + size (sdom c')).

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

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

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

Lemma determinacy 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 c l sc l' : compile l c sc l' ->
  forall p, l <= p < l' -> List.In p (sdom sc).

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

Various lemmas regarding the domain of the code and labels.

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

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

Lemma compile_sdom_close_left l c sc l' : compile l c sc l' -> List.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 (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 (c : cmd0) s :
  Some s -- c ---> None -> forall l sc l', compile l c sc l' ->
    Some (l, s) >- sc ---> None.



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

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






Lemma preservation_of_evaluations' 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 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 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').


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'' (c : cmd0) l s :
  Some (l, s) >- sC l c ---> None -> Some s -- c ----> None.

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

Lemma reflection_of_evaluations_sC_none (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.


Module while_hoare_prop_m := While_Hoare_Prop x.

Lemma preservation_hoare 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 ^].

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 l c sc l' : compile l c sc l' ->
  forall P Q, [^ P ^] sc [^ Q ^] -> {{ P l }} c {{ Q l' }}.

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.