Library goto

Require Import Lists_ext.
Require Import ssreflect ssrbool.
Require while.

Goto: A Low-level Language

This section corresponds to Section 2 in [Saabas&Uustalu2007].

Module Goto (while_semop_m : while.WHILE_SEMOP).

Import while_semop_m.

Syntax and (Small-step) Semantics of Goto

Definition label := nat.

Lemma label_dec : forall (l l' : label), { l = l' } + { l <> l' }.

Definition lstate := option (label * state).

For the operational semantics of one-step, non-branching instructions of Goto, we use the one-step commands (type cmd0 and operational semantics noted -- ---->) .

Local Open Scope while_cmd_scope.

Reserved Notation " c ||- s ---> t " (at level 82, no associativity).
Inductive exec0_label : lstate -> cmd0 -> lstate -> Prop :=
| exec0_label_cmd0 : forall s c s', Some s -- c ----> Some s' ->
forall l, exec0_label (Some (l, s)) c (Some (S l, s'))
| exec0_label_err : forall s c, Some s -- c ----> None ->
forall l, exec0_label (Some (l, s)) c None
where " c ||- s ---> t " := (exec0_label s c t) : goto_scope.

Local Open Scope goto_scope.

Branches may be conditional or not. For conditional branches, we use a language of boolean expressions (type expr_b) :

Inductive branch : Type := jmp : label -> branch | cjmp : expr_b -> label -> branch.

Reserved Notation "c ||- s |>> t" (at level 82, no associativity).

Note that branches never cause errors:

Inductive exec_branch : label * state -> branch -> label * state -> Prop :=
| exec_jmp : forall l s l', jmp l' ||- (l, s) |>> (l', s)
| exec_cjmp_true : forall l s t l', eval_b t s -> cjmp t l' ||- (l, s) |>> (l', s)
| exec_cjmp_false : forall l s t l', ~ eval_b t s -> cjmp t l' ||- (l, s) |>> (S l, s)
where "c ||- s |>> t" := (exec_branch s c t) : goto_scope.

Unstructured programs are lists of labeled (branching or not) instructions. They are wellformed when no instruction has two labels:

Inductive insn : Type := C : cmd0 -> insn | B : branch -> insn.

Definition code := list (label * insn).

Reserved Notation "c ||- s ->> t" (at level 82, no associativity).

Definition wellformed_goto (c : code) : Prop :=
  forall l i i', In (l, i) c -> In (l, i') c -> i = i'.

Lemma wellformed_goto_app : forall c, wellformed_goto c ->
  forall c1 c2, c = c1 ++ c2 -> wellformed_goto c1 /\ wellformed_goto c2.

Lemma dom_In_wf : forall c, wellformed_goto c -> forall p i, In (p, i) c ->
  forall c1 c2, c = c1 ++ c2 -> In p (uzip1 c1) -> In (p, i) c1.

Lemma dom_In_wf2 : forall c, wellformed_goto c -> forall p i, In (p, i) c ->
  forall c1 c2, c = c1 ++ c2 -> In p (uzip1 c2) -> In (p, i) c2.

We can now define the semantics of Goto. The type below corresponds to Figure 1 (Small-step semantics rules of Goto) in [Saabas&Uustalu2007]:

Inductive exec_goto : code -> lstate -> lstate -> Prop :=
| exec_goto_cmd0 : forall l i s s' c, In (l, C i) c ->
  i ||- Some (l, s) ---> Some s' -> c ||- Some (l, s) ->> Some s'
| exec_goto_cmd0_err : forall l i s c, In (l, C i) c ->
  i ||- Some (l, s) ---> None -> c ||- Some (l, s) ->> None
| exec_goto_branch : forall l j s s' c, In (l, B j) c ->
  j ||- (l, s) |>> s' -> c ||- Some (l, s) ->> Some s'
where "c ||- s ->> t" := (exec_goto c s t) : goto_scope.

Lemma cmd0_labels : forall c l s l' s', c ||- Some (l, s) ---> Some (l', s') ->
  l <> l'.

Properties

Lemma 3 (Extension of the domain) in [Saabas&Uustalu2007]:

Lemma exec_goto_extension_right' : forall c s s' i, c ||- s ->> s' ->
  c ++ i :: nil ||- s ->> s'.

Lemma exec_goto_extension_right : forall c' s s' c, c ||- s ->> s' -> c ++ c' ||- s ->> s'.

Lemma exec_goto_contraction_right_ : forall c st st', c ||- st ->> st' ->
forall c1 c2 l s l' s', c = c1 ++ c2 -> st = Some (l,s) -> st' = Some (l',s') ->
  In l (uzip1 c1) -> ~ In l (uzip1 c2) ->
   c1 ||- st ->> st'.

Lemma exec_goto_contraction_right : forall c1 c2, wellformed_goto (c1 ++ c2) ->
  forall l s l' s', c1 ++ c2 ||- Some (l, s) ->> Some (l', s') ->
    In l (uzip1 c1) -> c1 ||- Some (l, s) ->> Some (l', s').

Lemma exec_goto_extension_left : forall c s s' i, c ||- s ->> s' -> i :: c ||- s ->> s'.

Lemma exec_goto_contraction_left_ : forall c st st', c ||- st ->> st' ->
forall c1 c2 l s l' s', c = c1 ++ c2 -> st = Some (l, s) -> st' = Some (l', s') ->
  In l (uzip1 c2) -> ~ In l (uzip1 c1) -> c2 ||- st ->> st'.

Lemma exec_goto_contraction_left : forall c1 c2, wellformed_goto (c1 ++ c2) ->
forall l s l' s', c1 ++ c2 ||- Some (l, s) ->> Some (l', s') ->
  In l (uzip1 c2) -> c2 ||- Some (l, s) ->> Some (l', s').

Reflexive, Transitive Closure Predicates

Reflexive, transitive closure, to be used in Theorem 6 (Preservation of evaluations as stuck reduction sequences) of [Saabas&Uustalu2007]:

Reserved Notation " c ||- s '--->*' t " (at level 82, no associativity).

Inductive redseqs : code -> lstate -> lstate -> Prop :=
| redseqs_refl : forall s c, c ||- s --->* s
| redseqs_trans : forall s s' s'' c, c ||- s --->* s' -> c ||- s' ->> s'' -> c ||- s --->* s''
where " c ||- s '--->*' t " := (redseqs c s t) : goto_scope.

Lemma redseqs_inv_nil : forall s s', nil ||- s --->* s' -> s = s'.

Lemma redseqs_transitivity' : forall c s' s'', c ||- s' --->* s'' ->
  forall s, c ||- s --->* s' -> c ||- s --->* s''.

Lemma redseqs_transitivity : forall c s s', c ||- s --->* s' ->
  forall s'', c ||- s' --->* s'' -> c ||- s --->* s''.

Lemma redseqs_extension_left'' : forall c s' s'', c ||- s' --->* s'' ->
  forall l i l' st', s' = Some (l', st') -> (l, i) :: c ||- s' --->* s''.

Lemma redseqs_extension_left' : forall c l' s' s'', c ||- Some (l', s') --->* s'' ->
forall l i, (l, i) :: c ||- Some (l', s') --->* s''.

Lemma redseqs_extension_left : forall c l s s' c',
  c ||- Some (l, s) --->* s' -> c' ++ c ||- Some (l, s) --->* s'.

Lemma redseqs_extension_right''' : forall c st' st'', redseqs c st' st'' ->
forall l i l' s' , st' = Some (l', s') -> redseqs (c ++ (l, i) :: nil) st' st''.

Lemma redseqs_extension_right'' : forall c l' s' s'', redseqs c (Some (l', s')) s'' ->
  forall l i, redseqs (c ++ (l, i) :: nil) (Some (l', s')) s''.

Lemma redseqs_extension_right' : forall c l s s' c',
  redseqs c (Some (l, s)) s' -> redseqs (c ++ rev c') (Some (l, s)) s'.

Lemma redseqs_extension_right : forall c l s s' c',
  c ||- Some (l, s) --->* s' -> c ++ c' ||- Some (l, s) --->* s'.

Reflexive, transitive closure with explicit index k, to be used in Theorem 7 (Reflection of stuck reduction sequences as evaluations):

Inductive redseq (c : code) : nat -> lstate -> lstate -> Prop :=
| zero_red : forall s, redseq c O s s
| more_red : forall n s s' s'', c ||- s ->> s' -> redseq c n s' s'' -> redseq c (S n) s s''.

Lemma more_red' : forall c n s s', redseq c n s s' -> forall s'', c ||- s' ->> s'' -> redseq c (S n) s s''.

Lemma red_seqs_red_seq : forall p s s', redseqs p s s' -> exists n, redseq p n s s'.

Lemma redseq_nil : forall k ST ST', redseq nil k ST ST' -> ST = ST'.

Lemma redseq_inv_refl' : forall c k st st', redseq c k st st' ->
  forall l s, st = Some (l, s) -> ~ In l (uzip1 c) -> st = st'.

Lemma redseq_sC_refl : forall k c st st', redseq c k st st' ->
  forall l s l' s' p i, st = Some (l, s) -> st' = Some (l', s') ->
    c = (p, C i) :: nil -> p <> l -> st = st'.

Lemma redseq_sC_inv : forall k c st st', redseq c k st st' ->
  forall l s l' s' i, st = Some (l, s) -> st' = Some (l', s') ->
    l <> l' -> c = (l, C i) :: nil -> i ||- st ---> st'.

Lemma redseq_self_jump : forall k l s l' s', l <> l' ->
  ~ redseq ((l, B (jmp l)) :: nil) k (Some (l, s)) (Some (l', s')).

Lemma redseq_self_cjmp : forall k t l s l' s', l <> l' -> eval_b t s ->
  ~ redseq ((l, B (cjmp t l)) :: nil) k (Some (l, s)) (Some (l', s')).

The following two lemmas express, in the particular case of branches, a property similar to Lemma 2 (Stuck states) in [Saabas&Uustalu2007]. They are used in the proof of Theorem 7 (Reflection of stuck reduction sequences as evaluations) in lieu of Lemma 2.

Lemma redseq_out_of_domain_jump : forall k p m l s l' s', p <> l ->
redseq ((p, B (jmp m)) :: nil) k (Some (l, s)) (Some (l', s')) -> l = l' /\ s = s'.

Lemma redseq_out_of_domain_cjmp : forall k p t m l s l' s', p <> l ->
redseq ((p, B (cjmp t m)) :: nil) k (Some (l, s)) (Some (l', s')) -> l = l' /\ s = s'.

End Goto.

Module Goto_Deter (while_semop_deter_m : while.WHILE_SEMOP_DETER).

Module Import goto_m := Goto while_semop_deter_m.

Import while_semop_deter_m.

Local Open Scope while_cmd_scope.
Local Open Scope goto_scope.

Properties

Lemma 1 (Determinacy) in [Saabas&Uustalu2007]:

Lemma exec0_label_deter : forall s c s', c ||- s ---> s' ->
forall s'', c ||- s ---> s'' -> s' = s''.

Lemma branch_deter : forall s c s', c ||- s |>> s' ->
forall s'', c ||- s |>> s'' -> s' = s''.

Lemma exec_goto_deter : forall c, wellformed_goto c ->
forall s s', c ||- s ->> s' -> forall s'', c ||- s ->> s'' -> s' = s''.

End Goto_Deter.