Library sgoto

Require Import Wf_nat.
Require Import ssreflect ssrbool.
Require Import Lists_ext.
Require Import goto.

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.
Import goto_m.
Import 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.

Local Open Scope 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, { In l (sdom sc) } + { ~ In l (sdom sc) }.

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

Lemma not_in_sdom_sS' : forall m c d, ~ In m (sdom (c [+] d)) -> ~ 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 : forall sc1 sc2, wellformed (sc1 [+] sc2) -> wellformed sc1.

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

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

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

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

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

Lemma wellformed_ass' : forall 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 = uzip1 (U sc).

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

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

Lemma wellformed_wellformed_goto : forall 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.

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

Local Open Scope goto_scope.

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'', 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'', 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, ~ 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.

Local Open Scope while_cmd_scope.

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 : forall 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 : forall 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 : forall 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 : forall st l l' s',
  Some (l, st) >- sB l (jmp l') ---> s' -> s' = Some (l', st) /\ l <> l'.

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

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

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

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

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

Lemma exec_sgoto_inv_refl : forall sc l s s',
  Some (l, s) >- sc ---> s' -> ~ 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 : forall c l s l' s', Some (l, s) >- sC l c ---> Some (l', s') -> l <> l'.

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

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

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

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

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

Lemma redseq_trans_inv2 : forall 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 ->
    In l (sdom sc2) -> ~ In l' (sdom (sc1 [+] sc2)) ->
    (exists k, exists lk, exists sk, 0 < k <= n /\ ~ 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 : forall 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')) ->
~ 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 : forall 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 : forall sc0 sc1 sc2, wellformed ((sc0 [+] sc1) [+] sc2) ->
(sc0 [+] sc1) [+] sc2 ~= sc0 [+] (sc1 [+] sc2).

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

Lemma sem_equ_com' : forall 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 : forall sc0 sc1, sc0 [+] sc1 ~= sc1 [+] sc0.

End SGoto.