Module Sem

Require Import List.
Require Import Arith.
Require Import ZArith.
Require Import Zwf.
Require Import Coq.Program.Equality.
Require Import Classical.
Require Import ClassicalDescription.
Require Import Sequences.

Ltac inv H := inversion H; clear H; subst.
Ltac omegaContradiction := exfalso; omega.
Open Scope Z_scope.

Part 1. The IMP language and its semantics


Definition ident := nat.

Definition eq_ident: forall (x y: ident), {x=y}+{x<>y} := eq_nat_dec.

Inductive expr : Type :=
  | Evar: ident -> expr
  | Econst: Z -> expr
  | Eadd: expr -> expr -> expr
  | Esub: expr -> expr -> expr.

Inductive bool_expr : Type :=
  | Bequal: expr -> expr -> bool_expr
  | Bless: expr -> expr -> bool_expr.

Inductive cmd : Type :=
  | Cskip: cmd
  | Cassign: ident -> expr -> cmd
  | Cseq: cmd -> cmd -> cmd
  | Cifthenelse: bool_expr -> cmd -> cmd -> cmd
  | Cwhile: bool_expr -> cmd -> cmd.

Execution states, associating values to variables.

Definition state := ident -> Z.

Definition initial_state: state := fun (x: ident) => 0.

Definition update (s: state) (x: ident) (n: Z) : state :=
  fun y => if eq_ident x y then n else s y.

Evaluation of expressions.

Fixpoint eval_expr (s: state) (e: expr) {struct e} : Z :=
  match e with
  | Evar x => s x
  | Econst n => n
  | Eadd e1 e2 => eval_expr s e1 + eval_expr s e2
  | Esub e1 e2 => eval_expr s e1 - eval_expr s e2
  end.

Definition eval_bool_expr (s: state) (b: bool_expr) : bool :=
  match b with
  | Bequal e1 e2 =>
      if Z_eq_dec (eval_expr s e1) (eval_expr s e2) then true else false
  | Bless e1 e2 =>
      if Z_lt_dec (eval_expr s e1) (eval_expr s e2) then true else false
  end.

Using the semantics of expressions: to evaluate a given expression

Eval compute in (
  let x : ident := O in
  let s : state := update initial_state x 12 in
  eval_expr s (Eadd (Evar x) (Econst 1))).

Using the semantics of expressions: to reason symbolically over a given expression

Remark expr_add_pos:
  forall s x, s x >= 0 -> eval_expr s (Eadd (Evar x) (Econst 1)) > 0.
Proof.

Using the semantics of expressions: to show a "meta" property

Fixpoint is_free (x: ident) (e: expr) {struct e} : Prop :=
  match e with
  | Evar y => x = y
  | Econst n => False
  | Eadd e1 e2 => is_free x e1 \/ is_free x e2
  | Esub e1 e2 => is_free x e1 \/ is_free x e2
  end.

Lemma eval_expr_domain:
  forall s1 s2 e,
  (forall x, is_free x e -> s1 x = s2 x) ->
  eval_expr s1 e = eval_expr s2 e.
Proof.

Reduction semantics


Inductive red: cmd * state -> cmd * state -> Prop :=

  | red_assign: forall x e s,
      red (Cassign x e, s) (Cskip, update s x (eval_expr s e))

  | red_seq_left: forall c1 c2 s c1' s',
      red (c1, s) (c1', s') ->
      red (Cseq c1 c2, s) (Cseq c1' c2, s')

  | red_seq_skip: forall c s,
      red (Cseq Cskip c, s) (c, s)

  | red_if_true: forall s b c1 c2,
      eval_bool_expr s b = true ->
      red (Cifthenelse b c1 c2, s) (c1, s)

  | red_if_false: forall s b c1 c2,
      eval_bool_expr s b = false ->
      red (Cifthenelse b c1 c2, s) (c2, s)

  | red_while_true: forall s b c,
      eval_bool_expr s b = true ->
      red (Cwhile b c, s) (Cseq c (Cwhile b c), s)

  | red_while_false: forall b c s,
      eval_bool_expr s b = false ->
      red (Cwhile b c, s) (Cskip, s).

Lemma red_deterministic:
  forall cs cs1, red cs cs1 -> forall cs2, red cs cs2 -> cs1 = cs2.
Proof.

The three possible outcomes of execution.

Definition terminates (c: cmd) (s s': state) : Prop :=
  star red (c, s) (Cskip, s').

Definition diverges (c: cmd) (s: state) : Prop :=
  infseq red (c, s).

Definition goes_wrong (c: cmd) (s: state) : Prop :=
  exists c', exists s',
  star red (c, s) (c', s') /\ c' <> Cskip /\ irred red (c', s').

Natural semantics, terminating case


Inductive exec: state -> cmd -> state -> Prop :=
  | exec_skip: forall s,
      exec s Cskip s

  | exec_assign: forall s x e,
      exec s (Cassign x e) (update s x (eval_expr s e))

  | exec_seq: forall s c1 c2 s1 s2,
      exec s c1 s1 -> exec s1 c2 s2 ->
      exec s (Cseq c1 c2) s2

  | exec_if: forall s be c1 c2 s',
      exec s (if eval_bool_expr s be then c1 else c2) s' ->
      exec s (Cifthenelse be c1 c2) s'

  | exec_while_loop: forall s be c s1 s2,
      eval_bool_expr s be = true ->
      exec s c s1 -> exec s1 (Cwhile be c) s2 ->
      exec s (Cwhile be c) s2

  | exec_while_stop: forall s be c,
      eval_bool_expr s be = false ->
      exec s (Cwhile be c) s.

Termination in natural semantics implies termination in reduction semantics.

Remark star_red_seq_left:
  forall c s c' s' c2,
  star red (c, s) (c', s') ->
  star red (Cseq c c2, s) (Cseq c' c2, s').
Proof.

Lemma exec_terminates:
  forall s c s', exec s c s' -> terminates c s s'.
Proof.

Termination in reduction semantics implies termination in natural semantics.

Lemma red_preserves_exec:
  forall c s c' s', red (c, s) (c', s') ->
  forall sfinal, exec s' c' sfinal -> exec s c sfinal.
Proof.

Lemma terminates_exec:
  forall s c s', terminates c s s' -> exec s c s'.
Proof.

Coinductive natural semantics for divergence


CoInductive execinf: state -> cmd -> Prop :=
  | execinf_seq_left: forall s c1 c2,
      execinf s c1 ->
      execinf s (Cseq c1 c2)

  | execinf_seq_right: forall s c1 c2 s1,
      exec s c1 s1 -> execinf s1 c2 ->
      execinf s (Cseq c1 c2)

  | execinf_if: forall s b c1 c2,
      execinf s (if eval_bool_expr s b then c1 else c2) ->
      execinf s (Cifthenelse b c1 c2)

  | execinf_while_body: forall s b c,
      eval_bool_expr s b = true ->
      execinf s c ->
      execinf s (Cwhile b c)

  | execinf_while_loop: forall s b c s1,
      eval_bool_expr s b = true ->
      exec s c s1 -> execinf s1 (Cwhile b c) ->
      execinf s (Cwhile b c).

Divergence in natural semantics implies divergence in reduction semantics.

Lemma execinf_red_step:
  forall c s,
  execinf s c -> exists c', exists s', red (c, s) (c', s') /\ execinf s' c'.
Proof.

Lemma execinf_diverges:
  forall c s, execinf s c -> diverges c s.
Proof.

Divergence in reduction semantics implies divergence in natural semantics.

Lemma diverges_star_inv:
  forall c s c' s',
  diverges c s -> star red (c, s) (c', s') -> diverges c' s'.
Proof.

Lemma diverges_seq_inversion:
  forall s c1 c2,
  diverges (Cseq c1 c2) s ->
  diverges c1 s \/ exists s', star red (c1, s) (Cskip, s') /\ diverges c2 s'.
Proof.

Lemma diverges_while_inversion:
  forall b c s,
  diverges (Cwhile b c) s ->
  eval_bool_expr s b = true /\
  (diverges c s \/ exists s', star red (c, s) (Cskip, s') /\ diverges (Cwhile b c) s').
Proof.

Lemma diverges_execinf:
  forall c s, diverges c s -> execinf s c.
Proof.

Definitional interpreter


Inductive result: Type :=
  | Bot: result
  | Res: state -> result.

Definition bind (r: result) (f: state -> result) : result :=
  match r with
  | Res s => f s
  | Bot => Bot
  end.

Fixpoint interp (n: nat) (c: cmd) (s: state) {struct n} : result :=
  match n with
  | O => Bot
  | S n' =>
      match c with
      | Cskip => Res s
      | Cassign x e => Res (update s x (eval_expr s e))
      | Cseq c1 c2 =>
          bind (interp n' c1 s) (fun s1 => interp n' c2 s1)
      | Cifthenelse b c1 c2 =>
          interp n' (if eval_bool_expr s b then c1 else c2) s
      | Cwhile b c1 =>
          if eval_bool_expr s b
          then bind (interp n' c1 s) (fun s1 => interp n' (Cwhile b c1) s1)
          else Res s
      end
  end.

A sample program and its execution. The program computes the quotient and remainder of variables a and b. In concrete syntax: 
       r := a; q := 0;
       while b < r + 1 do r := r - b; q := q + 1 done

Open Scope nat_scope.

Definition va : ident := 0.
Definition vb : ident := 1.
Definition vq : ident := 2.
Definition vr : ident := 3.

Open Scope Z_scope.

Definition prog :=
  Cseq (Cassign vr (Evar va))
  (Cseq (Cassign vq (Econst 0))
   (Cwhile (Bless (Evar vb) (Eadd (Evar vr) (Econst 1)))
      (Cseq (Cassign vr (Esub (Evar vr) (Evar vb)))
            (Cassign vq (Eadd (Evar vq) (Econst 1)))))).

Definition prog_init_state := update (update initial_state va 13) vb 3.

Definition test_prog :=
  match interp 100 prog prog_init_state with
  | Res s => Some(s vq)
  | Bot => None
  end.

Eval compute in test_prog.

The natural ordering over results.

Definition res_le (r1 r2: result) := r1 = Bot \/ r1 = r2.

The interp function is monotone in n with respect to this ordering.

Remark bind_mon:
  forall r1 f1 r2 f2,
  res_le r1 r2 -> (forall s, res_le (f1 s) (f2 s)) ->
  res_le (bind r1 f1) (bind r2 f2).
Proof.

Open Scope nat_scope.

Lemma interp_mon:
  forall n n' c s, n <= n' -> res_le (interp n c s) (interp n' c s).
Proof.

Corollary interp_Res_stable:
  forall n n' c s s',
  n <= n' -> interp n c s = Res s' -> interp n' c s = Res s'.
Proof.

It follows an equivalence between termination according to the natural semantics and the fact that interp n c s returns Res for a suitably large n.

Remark bind_Res_inversion:
  forall r f s, bind r f = Res s -> exists s1, r = Res s1 /\ f s1 = Res s.
Proof.

Lemma interp_exec:
  forall n c s s', interp n c s = Res s' -> exec s c s'.
Proof.

Hint Resolve Max.le_max_l Max.le_max_r.

Lemma exec_interp:
  forall s c s', exec s c s' -> exists n, interp n c s = Res s'.
Proof.

Corollary exec_interp_either:
  forall s c s' n, exec s c s' -> interp n c s = Bot \/ interp n c s = Res s'.
Proof.

Moreover, if s diverges according to the natural semantics, interp always returns Bot for all values of n.

Lemma execinf_interp:
  forall n s c, execinf s c -> interp n c s = Bot.
Proof.

Denotational semantics


The sequence n => interp n c s eventually stabilizes as n goes to infinity.

Lemma interp_limit:
  forall s c, exists r, exists m, forall n, m <= n -> interp n c s = r.
Proof.

Using an axiom of description, we can define a function associating the limit of the sequence n => interp n c s to each c, s. This is the denotation of c in s.

Definition interp_limit_dep (s: state) (c: cmd) :
  { r: result | exists m, forall n, m <= n -> interp n c s = r}.
Proof.

Definition denot (c: cmd) (s: state) : result := proj1_sig (interp_limit_dep s c).

Lemma denot_limit:
  forall c s, exists m, forall n, m <= n -> interp n c s = denot c s.
Proof.

Lemma denot_charact:
  forall c s m r,
  (forall n, m <= n -> interp n c s = r) ->
  denot c s = r.
Proof.

The denot function satisfies the expected equations for a denotational semantics.

Lemma denot_skip:
  forall s, denot Cskip s = Res s.
Proof.

Lemma denot_assign:
  forall x e s,
  denot (Cassign x e) s = Res (update s x (eval_expr s e)).
Proof.

Lemma denot_seq:
  forall c1 c2 s, denot (Cseq c1 c2) s = bind (denot c1 s) (fun s' => denot c2 s').
Proof.

Lemma denot_if:
  forall b c1 c2 s,
  denot (Cifthenelse b c1 c2) s = denot (if eval_bool_expr s b then c1 else c2) s.
Proof.

Lemma denot_while:
  forall b c s,
  denot (Cwhile b c) s =
  if eval_bool_expr s b
  then bind (denot c s) (fun s' => denot (Cwhile b c) s')
  else Res s.
Proof.

Lemma le_interp_denot:
  forall n c s, res_le (interp n c s) (denot c s).
Proof.

Lemma denot_while_least_fixed_point:
  forall b c (f: state -> result),
  (forall s,
   f s = if eval_bool_expr s b then bind (denot c s) (fun s' => f s') else Res s) ->
  (forall s, res_le (denot (Cwhile b c) s) (f s)).
Proof.

Using these equations, we can prove an equivalence result between

Lemma denot_exec:
  forall c s s', denot c s = Res s' -> exec s c s'.
Proof.

Lemma exec_denot:
  forall s c s', exec s c s' -> denot c s = Res s'.
Proof.

Lemma execinf_denot:
  forall s c, execinf s c -> denot c s = Bot.
Proof.

Lemma denot_execinf:
  forall s c, denot c s = Bot -> execinf s c.
Proof.

Part 2. Axiomatic semantics and program proof


Assertions over states.

Definition assertion := state -> Prop.

Definition aupdate (P: assertion) (x: ident) (e: expr) : assertion :=
  fun s => P (update s x (eval_expr s e)).

Definition atrue (be: bool_expr) : assertion :=
  fun s => eval_bool_expr s be = true.

Definition afalse (be: bool_expr) : assertion :=
  fun s => eval_bool_expr s be = false.

Definition aand (P Q: assertion) : assertion :=
  fun s => P s /\ Q s.

Definition aor (P Q: assertion) : assertion :=
  fun s => P s \/ Q s.

Definition aimp (P Q: assertion) : Prop :=
  forall s, P s -> Q s.

The rules of the axiomatic semantics, defining valid weak Hoare triples {P} c {Q}.

Inductive triple: assertion -> cmd -> assertion -> Prop :=
  | triple_skip: forall P,
      triple P Cskip P

  | triple_assign: forall P x e,
      triple (aupdate P x e) (Cassign x e) P

  | triple_seq: forall c1 c2 P Q R,
      triple P c1 Q -> triple Q c2 R ->
      triple P (Cseq c1 c2) R

  | triple_if: forall be c1 c2 P Q,
      triple (aand (atrue be) P) c1 Q ->
      triple (aand (afalse be) P) c2 Q ->
      triple P (Cifthenelse be c1 c2) Q

  | triple_while: forall be c P,
      triple (aand (atrue be) P) c P ->
      triple P (Cwhile be c) (aand (afalse be) P)

  | triple_consequence: forall c P Q P' Q',
      triple P' c Q' -> aimp P P' -> aimp Q' Q ->
      triple P c Q.

Semantic interpretation of weak Hoare triples in terms of concrete executions.

CoInductive finally: state -> cmd -> assertion -> Prop :=
  | finally_done: forall s (Q: assertion),
      Q s ->
      finally s Cskip Q

  | finally_step: forall c s c' s' Q,
      red (c, s) (c', s') -> finally s' c' Q ->
      finally s c Q.

Definition sem_triple (P: assertion) (c: cmd) (Q: assertion) :=
  forall s, P s -> finally s c Q.

Lemma finally_seq:
  forall c1 c2 s Q R,
  finally s c1 Q -> sem_triple Q c2 R -> finally s (Cseq c1 c2) R.
Proof.

Lemma finally_while:
  forall be c P,
  sem_triple (aand (atrue be) P) c P ->
  sem_triple P (Cwhile be c) (aand (afalse be) P).
Proof.

Lemma finally_consequence:
  forall s c Q Q', aimp Q Q' -> finally s c Q -> finally s c Q'.
Proof.

Every derivable Hoare triple is semantically valid.

Lemma triple_correct:
  forall P c Q, triple P c Q -> sem_triple P c Q.
Proof.

Axiomatic semantics for strong Hoare triples [P] c [Q].

Open Scope Z_scope.

Definition aequal (e: expr) (v: Z) : assertion :=
  fun (s: state) => eval_expr s e = v.
Definition alessthan (e: expr) (v: Z) : assertion :=
  fun (s: state) => 0 <= eval_expr s e < v.

Inductive Triple: assertion -> cmd -> assertion -> Prop :=
  | Triple_skip: forall P,
      Triple P Cskip P

  | Triple_assign: forall P x e,
      Triple (aupdate P x e) (Cassign x e) P

  | Triple_seq: forall c1 c2 P Q R,
      Triple P c1 Q -> Triple Q c2 R ->
      Triple P (Cseq c1 c2) R

  | Triple_if: forall be c1 c2 P Q,
      Triple (aand (atrue be) P) c1 Q ->
      Triple (aand (afalse be) P) c2 Q ->
      Triple P (Cifthenelse be c1 c2) Q

  | Triple_while: forall be c P measure,
      (forall v,
        Triple (aand (atrue be) (aand (aequal measure v) P))
               c
               (aand (alessthan measure v) P)) ->
      Triple P (Cwhile be c) (aand (afalse be) P)

  | Triple_consequence: forall c P Q P' Q',
      Triple P' c Q' -> aimp P P' -> aimp Q' Q ->
      Triple P c Q.

Semantic interpretation of strong Hoare triples in terms of concrete executions.

Definition sem_Triple (P: assertion) (c: cmd) (Q: assertion) :=
  forall s, P s -> exists s', exec s c s' /\ Q s'.

Lemma Triple_while_correct:
  forall (P: assertion) measure c b,
  (forall v : Z,
   sem_Triple (aand (atrue b) (aand (aequal measure v) P))
              c
              (aand (alessthan measure v) P)) ->
  forall v s,
  eval_expr s measure = v -> P s ->
  exists s', exec s (Cwhile b c) s' /\ (aand (afalse b) P) s'.
Proof.

Lemma Triple_correct:
  forall P c Q, Triple P c Q -> sem_Triple P c Q.
Proof.

Weakest precondition calculus & verification condition generation

Inductive acmd : Type :=
  | Askip: acmd
  | Aassign: ident -> expr -> acmd
  | Aseq: acmd -> acmd -> acmd
  | Aifthenelse: bool_expr -> acmd -> acmd -> acmd
  | Awhile: bool_expr -> assertion -> acmd -> acmd
  | Aassert: assertion -> acmd.

wp a Q computes the weakest precondition for command a with postcondition Q.

Fixpoint wp (a: acmd) (Q: assertion) {struct a} : assertion :=
  match a with
  | Askip => Q
  | Aassign x e => aupdate Q x e
  | Aseq a1 a2 => wp a1 (wp a2 Q)
  | Aifthenelse b a1 a2 => aor (aand (atrue b) (wp a1 Q)) (aand (afalse b) (wp a2 Q))
  | Awhile b P a1 => P
  | Aassert P => P
  end.

vcg a Q computes a logical formula which, if true, implies that the triple {wp a Q} a Q holds.

Fixpoint vcg (a: acmd) (Q: assertion) {struct a} : Prop :=
  match a with
  | Askip => True
  | Aassign x e => True
  | Aseq a1 a2 => vcg a1 (wp a2 Q) /\ vcg a2 Q
  | Aifthenelse b a1 a2 => vcg a1 Q /\ vcg a2 Q
  | Awhile b P a1 =>
      vcg a1 P /\
      aimp (aand (afalse b) P) Q /\
      aimp (aand (atrue b) P) (wp a1 P)
  | Aassert P =>
      aimp P Q
  end.

Definition vcgen (P: assertion) (a: acmd) (Q: assertion) : Prop :=
  aimp P (wp a Q) /\ vcg a Q.

Mapping annotated commands back to regular commands.

Fixpoint erase (a: acmd) {struct a} : cmd :=
  match a with
  | Askip => Cskip
  | Aassign x e => Cassign x e
  | Aseq a1 a2 => Cseq (erase a1) (erase a2)
  | Aifthenelse b a1 a2 => Cifthenelse b (erase a1) (erase a2)
  | Awhile b P a1 => Cwhile b (erase a1)
  | Aassert P => Cskip
  end.

Correctness of wp and vcg.

Lemma vcg_correct:
  forall a Q, vcg a Q -> triple (wp a Q) (erase a) Q.
Proof.

Theorem vcgen_correct:
  forall P a Q, vcgen P a Q -> triple P (erase a) Q.
Proof.

Example of verification.

Open Scope Z_scope.

Definition precondition : assertion :=
  fun s => s va >= 0 /\ s vb > 0.

Definition invariant : assertion :=
  fun s => s vr >= 0 /\ s vb > 0 /\ s va = s vb * s vq + s vr.

Definition postcondition : assertion :=
  fun s => s vq = s va / s vb.

The program is the earlier Euclidean division example annotated with a loop invariant. 
       r := a; q := 0;
       while b < r + 1 do {invariant}  r := r - b; q := q + 1 done
Definition aprog :=
  Aseq (Aassign vr (Evar va))
  (Aseq (Aassign vq (Econst 0))
   (Awhile (Bless (Evar vb) (Eadd (Evar vr) (Econst 1)))
      invariant
      (Aseq (Aassign vr (Esub (Evar vr) (Evar vb)))
            (Aassign vq (Eadd (Evar vq) (Econst 1)))))).

Lemma aprog_correct:
  triple precondition (erase aprog) postcondition.
Proof.

Part 3. Compilation to a virtual machine


The virtual machine


Instruction set.

Inductive instruction: Type :=
  | Iconst(n: Z) (* push integer n on stack *)
  | Ivar(x: ident) (* push value of variable x on stack *)
  | Isetvar(x: ident) (* pop a value, then assign it to variable x *)
  | Iadd (* pop two values, push their sum *)
  | Isub (* pop two values, push their difference *)
  | Ibranch(ofs: Z) (* advance PC by ofs *)
  | Ibne(ofs: Z) (* pop two values, and if not equal, advance PC by ofs *)
  | Ibge(ofs: Z) (* pop two values, and if greater or equal, advance PC by ofs *)
  | Ihalt. (* stop the machine *)

Definition code := list instruction.

Definition stack := list Z.

Open Scope Z_scope.

Semantics of the virtual machine.

Fixpoint code_at (c: code) (pc: Z) {struct c} : option instruction :=
  match c with
  | nil => None
  | i :: c' => if Z_eq_dec pc 0 then Some i else code_at c' (pc - 1)
  end.

A virtual machine state is a triple (program counter, stack, variable state).

Definition machine_state := (Z * stack * state)%type.

Inductive transition (c: code): machine_state -> machine_state -> Prop :=
  | trans_const: forall pc stk s n,
      code_at c pc = Some(Iconst n) ->
      transition c (pc, stk, s) (pc + 1, n :: stk, s)

  | trans_var: forall pc stk s x,
      code_at c pc = Some(Ivar x) ->
      transition c (pc, stk, s) (pc + 1, s x :: stk, s)

  | trans_setvar: forall pc stk s x n,
      code_at c pc = Some(Isetvar x) ->
      transition c (pc, n :: stk, s) (pc + 1, stk, update s x n)

  | trans_add: forall pc stk s n1 n2,
      code_at c pc = Some(Iadd) ->
      transition c (pc, n2 :: n1 :: stk, s) (pc + 1, (n1 + n2) :: stk, s)

  | trans_sub: forall pc stk s n1 n2,
      code_at c pc = Some(Isub) ->
      transition c (pc, n2 :: n1 :: stk, s) (pc + 1, (n1 - n2) :: stk, s)

  | trans_branch: forall pc stk s ofs pc',
      code_at c pc = Some(Ibranch ofs) ->
      pc' = pc + 1 + ofs ->
      transition c (pc, stk, s) (pc', stk, s)

  | trans_bne: forall pc stk s ofs n1 n2 pc',
      code_at c pc = Some(Ibne ofs) ->
      pc' = (if Z_eq_dec n1 n2 then pc + 1 else pc + 1 + ofs) ->
      transition c (pc, n2 :: n1 :: stk, s) (pc', stk, s)

  | trans_bge: forall pc stk s ofs n1 n2 pc',
      code_at c pc = Some(Ibge ofs) ->
      pc' = (if Z_lt_dec n1 n2 then pc + 1 else pc + 1 + ofs) ->
      transition c (pc, n2 :: n1 :: stk, s) (pc', stk, s).

Sequences of machine transitions.

Definition mach_terminates (c: code) (s_init s_fin: state) :=
  exists pc,
  code_at c pc = Some Ihalt /\
  star (transition c) (0, nil, s_init) (pc, nil, s_fin).

Definition mach_diverges (c: code) (s_init: state) :=
  infseq (transition c) (0, nil, s_init).

Definition mach_goes_wrong (c: code) (s_init: state) :=
  exists pc, exists stk, exists s,
  star (transition c) (0, nil, s_init) (pc, stk, s) /\
  irred (transition c) (pc, stk, s) /\
  (code_at c pc <> Some Ihalt \/ stk <> nil).

The compilation scheme


Compilation of an expression. This is the familiar translation to "reverse Polish notation" (RPN).

Fixpoint compile_expr (e: expr): code :=
  match e with
  | Evar x => Ivar x :: nil
  | Econst n => Iconst n :: nil
  | Eadd e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Iadd :: nil
  | Esub e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Isub :: nil
  end.

Compilation of a boolean expression. Jumps ofs forward if the boolean expression evaluates to false. Continues in sequence if it evaluates to true.

Definition compile_bool_expr (b: bool_expr) (ofs: Z): code :=
  match b with
  | Bequal e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Ibne ofs :: nil
  | Bless e1 e2 => compile_expr e1 ++ compile_expr e2 ++ Ibge ofs :: nil
  end.

Compilation of a command.

Definition length (c: code) : Z := Z_of_nat (List.length c).

Fixpoint compile_cmd (c: cmd): code :=
  match c with
  | Cskip => nil
  | Cassign x e => compile_expr e ++ Isetvar x :: nil
  | Cseq c1 c2 => compile_cmd c1 ++ compile_cmd c2
  | Cifthenelse b c1 c2 =>
      let code1 := compile_cmd c1 in
      let code2 := compile_cmd c2 in
      compile_bool_expr b (length code1 + 1)
      ++ code1
      ++ Ibranch (length code2)
      :: code2
  | Cwhile b c =>
      let code_c := compile_cmd c in
      let code_b := compile_bool_expr b (length code_c + 1) in
      code_b ++ code_c ++
      Ibranch (- (length code_b + length code_c + 1)) :: nil
  end.

Compilation of a command as a whole program.

Definition compile_program (c: cmd) : code :=
  compile_cmd c ++ Ihalt :: nil.

Some technical lemmas to help reason about compiled code.

Lemma length_cons:
  forall i c, length (i :: c) = length c + 1.
Proof.

Lemma length_app:
  forall c1 c2, length (c1 ++ c2) = length c1 + length c2.
Proof.

Lemma length_singleton:
  forall i, length (i :: nil) = 1.
Proof.

Ltac normalize :=
  repeat (rewrite length_singleton || rewrite length_app || rewrite length_cons);
  repeat rewrite Zplus_assoc.

Lemma code_at_app:
  forall i c2 c1 pc,
  pc = length c1 -> code_at (c1 ++ i :: c2) pc = Some i.
Proof.

Correctness of compilation


The code for an expression pushes its value on the stack.

Lemma compile_expr_correct:
  forall s e pc stk c1 c2,
  pc = length c1 ->
  star (transition (c1 ++ compile_expr e ++ c2))
       (pc, stk, s)
       (pc + length (compile_expr e), eval_expr s e :: stk, s).
Proof.

The code for a boolean expression falls through or branches to ofs, depending on the truth value of the expression.

Lemma compile_bool_expr_correct:
  forall s e pc stk ofs c1 c2,
  pc = length c1 ->
  star (transition (c1 ++ compile_bool_expr e ofs ++ c2))
       (pc, stk, s)
       (pc + length (compile_bool_expr e ofs)
           + (if eval_bool_expr s e then 0 else ofs),
        stk, s).
Proof.

The code for a terminating command updates the state as predicted by the natural semantics.

Lemma compile_cmd_correct_terminating:
  forall s c s', exec s c s' ->
  forall stk pc c1 c2,
  pc = length c1 ->
  star (transition (c1 ++ compile_cmd c ++ c2))
       (pc, stk, s)
       (pc + length (compile_cmd c), stk, s').
Proof.

The code for a diverging command performs infinitely many machine transitions.

Inductive diverging_state: code -> machine_state -> Prop :=
  | div_state_intro: forall s c c1 c2 pc stk,
      execinf s c -> pc = length c1 ->
      diverging_state (c1 ++ compile_cmd c ++ c2) (pc, stk, s).

Lemma diverging_state_productive:
  forall c s c1 c2 pc stk,
  execinf s c -> pc = length c1 ->
  exists st2,
     plus (transition (c1 ++ compile_cmd c ++ c2)) (pc, stk, s) st2
  /\ diverging_state (c1 ++ compile_cmd c ++ c2) st2.
Proof.

Lemma compile_cmd_correct_diverging:
  forall s c , execinf s c ->
  forall pc stk c1 c2,
  pc = length c1 ->
  infseq (transition (c1 ++ compile_cmd c ++ c2)) (pc, stk, s).
Proof.

In conclusion, we obtain the expected forward simulation result between IMP programs and their compiled VM code.

Theorem compile_program_correct:
  forall c s_init,
  (forall s_fin, terminates c s_init s_fin -> mach_terminates (compile_program c) s_init s_fin)
/\
  (diverges c s_init -> mach_diverges (compile_program c) s_init).
Proof.

Part 4. An example of optimizing program transformation: dead code elimination


Finite sets of variables, from the Coq standard library.

Require Import FSets.
Module VS := FSetAVL.Make(Nat_as_OT).
Module VSP := FSetProperties.Properties(VS).
Module VSdecide := FSetDecide.Decide(VS).
Import VSdecide.

Computation of free variables.

Fixpoint fv_expr (e: expr) : VS.t :=
  match e with
  | Evar x => VS.singleton x
  | Econst n => VS.empty
  | Eadd e1 e2 => VS.union (fv_expr e1) (fv_expr e2)
  | Esub e1 e2 => VS.union (fv_expr e1) (fv_expr e2)
  end.

Definition fv_bool_expr (b: bool_expr) : VS.t :=
  match b with
  | Bequal e1 e2 => VS.union (fv_expr e1) (fv_expr e2)
  | Bless e1 e2 => VS.union (fv_expr e1) (fv_expr e2)
  end.

Fixpoint fv_cmd (c: cmd) : VS.t :=
  match c with
  | Cskip => VS.empty
  | Cassign x e => fv_expr e
  | Cseq c1 c2 => VS.union (fv_cmd c1) (fv_cmd c2)
  | Cifthenelse b c1 c2 => VS.union (fv_bool_expr b) (VS.union (fv_cmd c1) (fv_cmd c2))
  | Cwhile b c => VS.union (fv_bool_expr b) (fv_cmd c)
  end.

Liveness analysis


Computing post-fixpoints.

Section FIXPOINT.

Variable F: VS.t -> VS.t.
Variable default: VS.t.

Fixpoint iter (n: nat) (x: VS.t) {struct n} : VS.t :=
  match n with
  | O => default
  | S n' =>
      let x' := F x in
      if VS.subset x' x then x else iter n' x'
  end.

Definition niter := 20%nat.

Definition fixpoint : VS.t := iter niter VS.empty.

Lemma fixpoint_charact:
  VS.Subset (F fixpoint) fixpoint \/ fixpoint = default.
Proof.

Hypothesis F_stable:
  forall x, VS.Subset x default -> VS.Subset (F x) default.

Lemma fixpoint_upper_bound:
  VS.Subset fixpoint default.
Proof.

End FIXPOINT.

Liveness analysis: live c a computes the set of variables live "before" c as a function of the set a of variables live "after".

Fixpoint live (c: cmd) (a: VS.t) {struct c} : VS.t :=
  match c with
  | Cskip => a
  | Cassign x e =>
      if VS.mem x a
      then VS.union (VS.remove x a) (fv_expr e)
      else a
  | Cseq c1 c2 => live c1 (live c2 a)
  | Cifthenelse b c1 c2 =>
      VS.union (fv_bool_expr b) (VS.union (live c1 a) (live c2 a))
  | Cwhile b c =>
      let a' := VS.union (fv_bool_expr b) a in
      let default := VS.union (fv_cmd (Cwhile b c)) a in
      fixpoint (fun x => VS.union a' (live c x)) default
  end.

Lemma live_upper_bound:
  forall c a,
  VS.Subset (live c a) (VS.union (fv_cmd c) a).
Proof.

Lemma live_while_charact:
  forall b c a,
  let a' := live (Cwhile b c) a in
  VS.Subset (fv_bool_expr b) a' /\ VS.Subset a a' /\ VS.Subset (live c a') a'.
Proof.

Dead code elimination


Turn assignments x := e to dead variables x into skip statements.

Fixpoint dce (c: cmd) (a: VS.t) {struct c}: cmd :=
  match c with
  | Cskip => Cskip
  | Cassign x e => if VS.mem x a then Cassign x e else Cskip
  | Cseq c1 c2 => Cseq (dce c1 (live c2 a)) (dce c2 a)
  | Cifthenelse b c1 c2 =>
      Cifthenelse b (dce c1 a) (dce c2 a)
  | Cwhile b c =>
      Cwhile b (dce c (live (Cwhile b c) a))
  end.

Example: 
   r := a;                 ===>   r := a;
   q := 0;                        skip;
   while b < r+1 do               while b < r+1 do
     r := r - b;                    r := r - b;
     q := q + 1;                    skip;
   done                           done
if q is not live after. If q is live, the program is unchanged.

Eval compute in (dce prog (VS.singleton vr)).

Eval compute in (dce prog (VS.singleton vq)).

Semantic correctness


Definition agree (a: VS.t) (s1 s2: state) : Prop :=
  forall x, VS.In x a -> s1 x = s2 x.

Lemma agree_mon:
  forall a a' s1 s2,
  agree a' s1 s2 -> VS.Subset a a' -> agree a s1 s2.
Proof.

Lemma eval_expr_agree:
  forall a s1 s2, agree a s1 s2 ->
  forall e, VS.Subset (fv_expr e) a -> eval_expr s1 e = eval_expr s2 e.
Proof.

Lemma eval_bool_expr_agree:
  forall a s1 s2, agree a s1 s2 ->
  forall b, VS.Subset (fv_bool_expr b) a -> eval_bool_expr s1 b = eval_bool_expr s2 b.
Proof.

Lemma agree_update_live:
  forall s1 s2 a x v,
  agree (VS.remove x a) s1 s2 ->
  agree a (update s1 x v) (update s2 x v).
Proof.

Lemma agree_update_dead:
  forall s1 s2 a x v,
  agree a s1 s2 -> ~VS.In x a ->
  agree a (update s1 x v) s2.
Proof.

Lemma dce_correct_terminating:
  forall s c s', exec s c s' ->
  forall a s1,
  agree (live c a) s s1 ->
  exists s1', exec s1 (dce c a) s1' /\ agree a s' s1'.
Proof.

Lemma dce_correct_diverging:
  forall s c, execinf s c ->
  forall a s1,
  agree (live c a) s s1 -> execinf s1 (dce c a).
Proof.
Generated by coq2html