Library sgoto


SGoto, A Structured Version

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

Module SGoto (while_semop_deter_m : while.WHILE_SEMOP_DETER).

Module Import goto_deter_m := Goto_Deter while_semop_deter_m.

Natural Semantics Rules of SGoto


Inductive scode : Type :=
| sO : scode
| sC : label -> cmd0 -> scode
| sB : label -> branch -> scode
| sS : scode -> scode -> scode.


Notation "c '[+]' d" := (sS c d) (at level 69, right associativity) : sgoto_scope.


Fixpoint sdom sc :=
  match sc with
    | sO => nil | sC l _ => l :: nil | sB l _ => l :: nil
    | sc1 [+] sc2 => sdom sc1 ++ sdom sc2
  end.

Lemma sdom_dec : forall sc, { sdom sc = nil } + { sdom sc <> nil }.

Lemma lbl_sdom_dec : forall sc l, { List.In l (sdom sc) } + { ~ List.In l (sdom sc) }.

Lemma not_in_sdom_sS m c d : ~ List.In m (sdom (c [+] d)) -> ~ List.In m (sdom d).

Lemma not_in_sdom_sS' m c d : ~ List.In m (sdom (c [+] d)) -> ~ List.In m (sdom c).

Structured code is wellformed when instructions all have different labels:

Inductive wellformed : scode -> Prop :=
| wf_sO : wellformed sO
| wf_sC : forall x y, wellformed (sC x y)
| wf_sB : forall x y, wellformed (sB x y)
| wf_sS : forall sc1 sc2, disj (sdom sc1) (sdom sc2) ->
  wellformed sc1 -> wellformed sc2 -> wellformed (sc1 [+] sc2).

Lemma wellformed_inv_L sc1 sc2 : wellformed (sc1 [+] sc2) -> wellformed sc1.

Lemma wellformed_inv_R sc1 sc2 : wellformed (sc1 [+] sc2) -> wellformed sc2.

Lemma wellformed_In_L sc0 sc1 l : wellformed (sc0 [+] sc1) ->
 List.In l (sdom sc0) -> ~ List.In l (sdom sc1).

Lemma wellformed_In_R sc0 sc1 l : wellformed (sc0 [+] sc1) ->
 List.In l (sdom sc1) -> ~ List.In l (sdom sc0).

Lemma wellformed_neu sc : wellformed sc -> wellformed (sc [+] sO).

Lemma wellformed_ass sc0 sc1 sc2 :
  wellformed ((sc0 [+] sc1) [+] sc2) -> wellformed (sc0 [+] sc1 [+] sc2).

Lemma wellformed_ass' sc0 sc1 sc2 :
  wellformed (sc0 [+] sc1 [+] sc2) -> wellformed ((sc0 [+] sc1) [+] sc2).

The forgetful function forgets the structure of the code, effectively turning a piece of SGoto code into a piece of Goto code:

Fixpoint U sc :=
  match sc with
    | sO => nil | sC l c => (l, C c) :: nil | sB l b => (l, B b) :: nil
    | sc1 [+] sc2 => U sc1 ++ U sc2
  end.

Lemma sdom_dom : forall sc, sdom sc = unzip1 (U sc).

Lemma In_U_In_sdom sc l i : List.In (l, i) (U sc) -> List.In l (sdom sc).

Lemma U_ass sc0 sc1 sc2 : U ((sc0 [+] sc1) [+] sc2) = U (sc0 [+] sc1 [+] sc2).

Lemma wellformed_wellformed_goto sc : wellformed sc -> wellformed_goto (U sc).

We can now define the semantics of SGoto. The inductive type below corresponds to Figure 2 (Natural semantics rules of SGoto) in [Saabas&Uustalu2007]. Note that there is an additional constructor for error propagation.
printing >-

Reserved Notation "s >- p ---> t" (at level 70, no associativity).


Inductive exec_sgoto : scode -> lstate -> lstate -> Prop :=
| exec_sgoto_none : forall c, None >- c ---> None
| exec_sgoto_cmd0 : forall l c s s', c ||- Some (l, s) ---> s' -> Some (l, s) >- sC l c ---> s'
| exec_sgoto_jmp : forall l s l', l <> l' -> Some (l, s) >- sB l (jmp l') ---> Some (l', s)
| exec_sgoto_cjmp_true : forall l s b l',
  eval_b b s -> l <> l' -> Some (l, s) >- sB l (cjmp b l') ---> Some (l', s)
| exec_sgoto_cjmp_false : forall l s b l',
  ~~ eval_b b s -> Some (l, s) >- sB l (cjmp b l') ---> Some (S l, s)
| exec_sgoto_seq0 : forall sc1 sc2 l s s' s'', List.In l (sdom sc1) -> Some (l, s) >- sc1 ---> s' ->
  s' >- sc1 [+] sc2 ---> s'' -> Some (l, s) >- sc1 [+] sc2 ---> s''
| exec_sgoto_seq1 : forall sc1 sc2 l s s' s'', List.In l (sdom sc2) -> Some (l, s) >- sc2 ---> s' ->
  s' >- sc1 [+] sc2 ---> s'' -> Some (l, s) >- sc1 [+] sc2 ---> s''
| exec_sgoto_refl : forall sc l s, ~ List.In l (sdom sc) -> Some (l, s) >- sc ---> Some (l, s)
where "s >- p ---> t" := (exec_sgoto p s t) : sgoto_scope.

Properties

Inversion properties:

Lemma exec_sgoto_nil : forall c s, sdom c = nil -> s >- c ---> s.


Lemma exec_sgoto_inv_cmd' : forall c st st', st >- c ---> st' ->
  forall i l s l' s' l0, c = sC l0 i -> st = Some (l, s) -> st' = Some (l', s') ->
    l = l0 -> l' = S l /\ Some s -- i ---> Some s'.

Lemma exec_sgoto_inv_cmd c l s l' s' :
  Some (l, s) >- sC l c ---> Some (l', s') ->
  l' = S l /\ Some s -- c ---> Some s'.

Lemma exec_sgoto_inv_cjmp_true l s t l' s' :
  Some (l, s) >- sB l (cjmp t l') ---> s' ->
  eval_b t s -> s' = Some (l', s) /\ l' <> l.

Lemma exec_sgoto_inv_cjmp_false l s t l' s' :
  Some (l, s) >- sB l (cjmp t l') ---> s' ->
  ~~ eval_b t s -> s' = Some (S l, s).

Lemma exec_sgoto_inv_jmp st l l' s' :
  Some (l, st) >- sB l (jmp l') ---> s' -> s' = Some (l', st) /\ l <> l'.

Lemma exec_sgoto_inv_seq0' sc st st'' : st >- sc ---> st'' ->
  forall l s, st = Some (l, s) -> forall sc0 sc1, sc = sc0 [+] sc1 ->
    List.In l (sdom sc0) -> ~ List.In l (sdom sc1) ->
    exists st', Some (l, s) >- sc0 ---> st' /\ st' >- sc ---> st''.

Lemma exec_sgoto_inv_seq0 sc0 sc1 l s s'' :
  Some (l, s) >- sc0 [+] sc1 ---> s'' -> List.In l (sdom sc0) -> ~ List.In l (sdom sc1) ->
  exists s', Some (l, s) >- sc0 ---> s' /\ s' >- sc0 [+] sc1 ---> s''.

Lemma exec_sgoto_inv_seq1' sc st st'' : st >- sc ---> st'' ->
 forall l s, st = Some (l, s) -> forall sc0 sc1, sc = sc0 [+] sc1 ->
   List.In l (sdom sc1) -> ~ List.In l (sdom sc0) ->
   exists st', Some (l, s) >- sc1 ---> st' /\ st' >- sc ---> st''.

Lemma exec_sgoto_inv_seq1 sc0 sc1 l s s'' :
  Some (l, s) >- sc0 [+] sc1 ---> s'' -> List.In l (sdom sc1) -> ~ List.In l (sdom sc0) ->
  exists s', Some (l, s) >- sc1 ---> s' /\ s' >- sc0 [+] sc1 ---> s''.

Lemma exec_sgoto_inv_refl' sc st st' : st >- sc ---> st' ->
  forall l s, st = Some (l, s) -> ~ List.In l (sdom sc) -> st = st'.

Lemma exec_sgoto_inv_refl sc l s s' :
  Some (l, s) >- sc ---> s' -> ~ List.In l (sdom sc) -> Some (l, s) = s'.

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

Lemma determinacy : forall c, wellformed c -> forall s s', s >- c ---> s' ->
  forall s'', s >- c ---> s'' -> s' = s''.

Intermediate lemma:

Lemma postlabels_cmd c l s l' s' : Some (l, s) >- sC l c ---> Some (l', s') -> l <> l'.

Lemma 5 (Postlabels) in [Saabas&Uustalu2007]:

Lemma postlabels c s l' s' : s >- c ---> Some (l', s') -> ~ List.In l' (sdom c).

Theorem 6 (Preservation of evaluations as stuck reduction sequences) in [Saabas&Uustalu2007].

Lemma preservation sc s s' : s >- sc ---> s' -> U sc ||- s --->* s'.


Lemma redseq_trans_inv c n st st' : wellformed_goto c ->
  redseq c n st st' -> forall l s l' s' sc1 sc2,
    st = Some (l, s) -> st' = Some (l', s') -> c = U sc1 ++ U sc2 ->
    List.In l (sdom sc1) -> ~ List.In l' (sdom (sc1 [+] sc2)) ->
    (exists k, exists lk, exists sk, 0 < k <= n /\ ~ List.In lk (sdom sc1) /\
      redseq (U sc1) k st (Some (lk, sk)) /\ redseq c (n - k) (Some (lk, sk)) st').

Lemma redseq_trans_inv2 c n st st' : wellformed_goto c ->
  redseq c n st st' -> forall l s l' s' sc1 sc2,
    st = Some (l, s) -> st' = Some (l', s') -> c = U sc1 ++ U sc2 ->
    List.In l (sdom sc2) -> ~ List.In l' (sdom (sc1 [+] sc2)) ->
    (exists k, exists lk, exists sk, 0 < k <= n /\ ~ List.In lk (sdom sc2) /\
      redseq (U sc2) k st (Some (lk, sk)) /\ redseq c (n - k) (Some (lk, sk)) st').

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

Theorem 7 (Reflection of stuck reduction sequences as evaluations) in [Saabas&Uustalu2007]. Nested induction whose inner induction is noetherian.

Lemma reflection_of_stuck_redseq : forall sc k l s l' s',
  wellformed_goto (U sc) -> redseq (U sc) k (Some (l, s)) (Some (l', s')) ->
  ~ List.In l' (sdom sc) -> Some (l, s) >- sc ---> Some (l', s').

Semantic Equivalence


Definition sem_equ sc0 sc1 := forall s s', Some s >- sc0 ---> Some s' <-> Some s >- sc1 ---> Some s'.


Notation "c '~=' d" := (sem_equ c d) (at level 70, right associativity) : sgoto_scope.

Theorem 8 (Neutrality wrt phrase structure) in [Saabas&Uustalu2007]:

Lemma neutrality sc0 sc1 : wellformed sc0 -> U sc0 = U sc1 ->
  forall s s', Some s >- sc0 ---> Some s' -> Some s >- sc1 ---> Some s'.

Corollary 9 (Partial commutative monoidal structure) in [Saabas&Uustalu2007].

Lemma sem_equ_ass sc0 sc1 sc2 : wellformed ((sc0 [+] sc1) [+] sc2) ->
  (sc0 [+] sc1) [+] sc2 ~= sc0 [+] (sc1 [+] sc2).

Lemma sem_equ_neu sc : wellformed sc -> sc [+] sO ~= sc.

Lemma sem_equ_com' sc sc' sc0 sc1 : sc = sc0 [+] sc1 ->
  sc' = sc1 [+] sc0 -> forall s s', s >- sc ---> s' -> s >- sc' ---> s'.

Interestingly, commutativity does not require well-formedness:

Lemma sem_equ_com sc0 sc1 : sc0 [+] sc1 ~= sc1 [+] sc0.

End SGoto.