File 9

Small step IMP compiler

In this assignment you'll prove the continuation based small step imp compiler correct, and start working on your own language extension.

Due	2019-11-14 11:45AM
Link	https://github.ccs.neu.edu/verifcomp/19/asgn/9.v

First, a lot of premilinaries

Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
From Coq Require Import Strings.String.
From Coq Require Import ZArith.ZArith.
Require Import Psatz.

Ltac invert H := inversion H; subst; eauto.

Inductive Rstar {T : Type} (P : T -> T -> Prop) : T -> T -> Prop :=
| RRefl : forall a, Rstar P a a
| RStep : forall a b c, P a b -> Rstar P b c -> Rstar P a c
.

Hint Constructors Rstar.

Lemma RTrans {T : Type} {P : T -> T -> Prop} {a b c : T} : Rstar P a b -> Rstar P b c -> Rstar P a c.
Proof.
  elim; eauto.
Qed.
Inductive Rplus {T : Type} (R : T -> T -> Prop) : T -> T -> Prop :=
  | Rplus_left: forall a b c,
      R a b -> Rstar R b c -> Rplus R a c.
Hint Constructors Rplus.

Lemma Rplus_one {T : Type} (R : T -> T -> Prop):
  forall a b, R a b -> Rplus R a b.
Proof.
  eauto.
Qed.

Lemma Rplus_star {T : Type} (R : T -> T -> Prop):
  forall a b,
  Rplus R a b -> Rstar R a b.
Proof.
  intros. inversion H. eauto.
Qed.

Lemma Rplus_Rstar_trans {T : Type} (R : T -> T -> Prop):
  forall a b c, Rplus R a b -> Rstar R b c -> Rplus R a c.
Proof.
  intros. inversion H. eauto using RTrans.
Qed.

Lemma Rstar_Rplus_trans {T : Type} (R : T -> T -> Prop):
  forall a b c, Rstar R a b -> Rplus R b c -> Rplus R a c.
Proof.
  intros. inversion H0. inversion H; eauto using RTrans.
Qed.

Lemma Rplus_right {T : Type} (R : T -> T -> Prop):
  forall a b c, Rstar R a b -> R b c -> Rplus R a c.
Proof.
  eauto using Rstar_Rplus_trans, Rplus_one.
Qed.

Definition ident := string.

Inductive aexp : Type :=
  | CONST (n: Z)
  | VAR (x: ident)
  | PLUS (a1: aexp) (a2: aexp)
  | MINUS (a1: aexp) (a2: aexp). Hint Constructors aexp.

Definition store : Type := ident -> Z.

Fixpoint aeval (s: store) (a: aexp) : Z :=
  match a with
  | CONST n => n
  | VAR x => s x
  | PLUS a1 a2 => aeval s a1 + aeval s a2
  | MINUS a1 a2 => aeval s a1 - aeval s a2
  end.

Inductive bexp : Type :=
  | TRUE
  | FALSE
  | EQUAL (a1: aexp) (a2: aexp)
  | LESSEQUAL (a1: aexp) (a2: aexp)
  | NOT (b1: bexp)
  | AND (b1: bexp) (b2: bexp). Hint Constructors bexp.

Fixpoint beval (s: store) (b: bexp) : bool :=
  match b with
  | TRUE => true
  | FALSE => false
  | EQUAL a1 a2 => (aeval s a1 =? aeval s a2)%Z
  | LESSEQUAL a1 a2 => (aeval s a1 <=? aeval s a2)%Z
  | NOT b1 => negb (beval s b1)
  | AND b1 b2 => beval s b1 && beval s b2
  end.

Definition NOTEQUAL (a1 a2: aexp) : bexp := NOT (EQUAL a1 a2).

Definition GREATEREQUAL (a1 a2: aexp) : bexp := LESSEQUAL a2 a1.

Definition GREATER (a1 a2: aexp) : bexp := NOT (LESSEQUAL a1 a2).

Definition LESS (a1 a2: aexp) : bexp := GREATER a2 a1.

Definition OR (b1 b2: bexp) : bexp := NOT (AND (NOT b1) (NOT b2)).

Inductive com: Type :=
| SKIP
| ASSIGN (x: ident) (a: aexp)
| SEQ (c1: com) (c2: com)
| IFTHENELSE (b: bexp) (c1: com) (c2: com)
| WHILE (b: bexp) (c1: com)
.
Hint Constructors com.

Infix ";;" := SEQ (at level 80, right associativity).

Definition update (x: ident) (v: Z) (s: store) : store :=
  fun y => if string_dec x y then v else s y.

Inductive cont : Type :=
  | Kstop
  | Kseq (c: com) (k: cont)
  | Kwhile (b: bexp) (c: com) (k: cont).
Hint Constructors cont.
Inductive step: com * cont * store -> com * cont * store -> Prop :=
  | step_assign: forall x a k s,
      step (ASSIGN x a, k, s) (SKIP, k, update x (aeval s a) s)
  | step_seq: forall c1 c2 s k,
      step (SEQ c1 c2, k, s) (c1, Kseq c2 k, s)
  | step_ifthenelse: forall b c1 c2 k s,
      step (IFTHENELSE b c1 c2, k, s) ((if beval s b then c1 else c2), k, s)
  | step_while_done: forall b c k s,
      beval s b = false ->
      step (WHILE b c, k, s) (SKIP, k, s)
  | step_while_true: forall b c k s,
      beval s b = true ->
      step (WHILE b c, k, s) (c, Kwhile b c k, s)
  | step_skip_seq: forall c k s,
      step (SKIP, Kseq c k, s) (c, k, s)
  | step_skip_while: forall b c k s,
      step (SKIP, Kwhile b c k, s) (WHILE b c, k, s)
.
Hint Constructors step.

Definition irred {A : Type} (R : A -> A -> Prop) (a : A) := forall b, ~(R a b).

Inductive instr : Type :=
  | Iconst (n: Z)
  | Ivar (x: ident)
  | Isetvar (x: ident)
  | Iadd
  | Iopp
  | Iswap
  | Idup
  | Ipop
  | Iibranch
  | Ibranch (d: Z)
  | Ibeq (d1: Z) (d0: Z)
  | Ible (d1: Z) (d0: Z)
  | Ihalt. Hint Constructors instr.

Definition code := seq instr.

Definition codelen (c: code) : Z := Z.of_nat (size c).

Definition stack : Type := seq Z.

Definition config : Type := (Z * stack * store)%type.

Fixpoint instr_at (C: code) (pc: Z) : option instr :=
  match C with
  | nil => None
  | i :: C' => if pc =? 0 then Some i else instr_at C' (pc - 1)
  end % Z.

Open Scope Z.

Inductive transition (C: code): config -> config -> Prop :=
  | trans_const: forall pc stk s n,
      instr_at C pc = Some(Iconst n) ->
      transition C (pc , stk , s)
                   (pc + 1, n :: stk, s)
  | trans_var: forall pc stk s x,
      instr_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,
      instr_at C pc = Some(Isetvar x) ->
      transition C (pc , n :: stk, s)
                   (pc + 1, stk , update x n s)
  | trans_add: forall pc stk s n1 n2,
      instr_at C pc = Some(Iadd) ->
      transition C (pc , n2 :: n1 :: stk , s)
                   (pc + 1, (n1 + n2) :: stk, s)
  | trans_opp: forall pc stk s n,
      instr_at C pc = Some(Iopp) ->
      transition C (pc , n :: stk , s)
                 (pc + 1, (- n) :: stk, s)
  | trans_swap : forall pc stk s n1 n2,
      instr_at C pc = Some(Iswap) ->
      transition C (pc , n1 :: n2 :: stk , s)
                 (pc + 1, n2 :: n1 :: stk, s)
  | trans_dup : forall pc stk s n,
            instr_at C pc = Some(Idup) ->
      transition C (pc , n :: stk , s)
                 (pc + 1, n :: n :: stk, s)
  | trans_pop : forall pc stk s n,
            instr_at C pc = Some(Ipop) ->
      transition C (pc , n :: stk , s)
                 (pc + 1, stk, s)
  | trans_ibranch: forall pc stk s i pc',
      instr_at C pc = Some(Iibranch) ->
      pc' = pc + 1 + i ->
      transition C (pc , i :: stk, s)
                   (pc', stk, s)
  | trans_branch: forall pc stk s d pc',
      instr_at C pc = Some(Ibranch d) ->
      pc' = pc + 1 + d ->
      transition C (pc , stk, s)
                   (pc', stk, s)
  | trans_beq: forall pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = Some(Ibeq d1 d0) ->
      pc' = pc + 1 + (if n1 =? n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                   (pc', stk , s)
  | trans_ble: forall pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = Some(Ible d1 d0) ->
      pc' = pc + 1 + (if n1 <=? n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                 (pc', stk , s).
Hint Constructors transition.

Fixpoint compile_aexp (a: aexp) : code :=
  match a with
  | CONST n => Iconst n :: nil
  | VAR x => Ivar x :: nil
  | PLUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iadd :: nil
  | MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iopp :: Iadd :: nil
  end.

Fixpoint compile_bexp (b: bexp) (d1: Z) (d0: Z) : code :=
  match b with
  | TRUE => if d1 =? 0 then nil else Ibranch d1 :: nil
  | FALSE => if d0 =? 0 then nil else Ibranch d0 :: nil
  | EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ibeq d1 d0 :: nil
  | LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Ible d1 d0 :: nil
  | NOT b1 => compile_bexp b1 d0 d1
  | AND b1 b2 =>
      let code2 := compile_bexp b2 d1 d0 in
      let code1 := compile_bexp b1 0 (codelen code2 + d0) in
      code1 ++ code2
  end.

Fixpoint compile_com (c: com) : code :=
  match c with
  | SKIP =>
      nil
  | ASSIGN x a =>
      compile_aexp a ++ Isetvar x :: nil
  | SEQ c1 c2 =>
      compile_com c1 ++ compile_com c2
  | IFTHENELSE b ifso ifnot =>
      let code_ifso := compile_com ifso in
      let code_ifnot := compile_com ifnot in
      compile_bexp b 0 (codelen code_ifso + 1)
      ++ code_ifso
      ++ Ibranch (codelen code_ifnot)
      :: code_ifnot
  | WHILE b body =>
      let code_body := compile_com body in
      let code_test := compile_bexp b 0 (codelen code_body + 1) in
      code_test
      ++ code_body
      ++ Ibranch (- (codelen code_test + codelen code_body + 1)) :: nil
  end.

Definition compile_program (p: com) : code :=
  compile_com p ++ Ihalt :: nil.

Inductive code_at: code -> Z -> code -> Prop :=
  | code_at_intro: forall C1 C2 C3 pc,
      pc = codelen C1 ->
      code_at (C1 ++ C2 ++ C3) pc C2.

These were all proved in the prior assignment. You may need to use them again.

Lemma codelen_cons:
  forall i c, codelen (i :: c) = codelen c + 1.
Proof.
Admitted.

Lemma codelen_app:
  forall c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2.
Proof.
Admitted.

Lemma instr_at_app:
  forall i c2 c1 pc,
  pc = codelen c1 ->
  instr_at (c1 ++ i :: c2) pc = Some i.
Proof.
Admitted.

Lemma code_at_head:
  forall C pc i C',
  code_at C pc (i :: C') ->
  instr_at C pc = Some i.
Proof.
Admitted.

Lemma code_at_tail:
  forall C pc i C',
  code_at C pc (i :: C') ->
  code_at C (pc + 1) C'.
Proof.
Admitted.

Lemma code_at_app_left:
  forall C pc C1 C2,
  code_at C pc (C1 ++ C2) ->
  code_at C pc C1.
Proof.
Admitted.

Lemma code_at_app_right:
  forall C pc C1 C2,
  code_at C pc (C1 ++ C2) ->
  code_at C (pc + codelen C1) C2.
Proof.
Admitted.

Lemma code_at_app_right2:
  forall C pc C1 C2 C3,
  code_at C pc (C1 ++ C2 ++ C3) ->
  code_at C (pc + codelen C1) C2.
Proof.
Admitted.

Lemma code_at_nil:
  forall C pc C1,
  code_at C pc C1 -> code_at C pc nil.
Proof.
Admitted.

Lemma instr_at_code_at_nil:
  forall C pc i, instr_at C pc = Some i -> code_at C pc nil.
Proof.
Admitted.

Lemma compile_aexp_correct:
  forall C s a pc stk,
  code_at C pc (compile_aexp a) ->
  Rstar (transition C)
       (pc, stk, s)
       (pc + codelen (compile_aexp a), aeval s a :: stk, s).
Proof.
Admitted.

Lemma compile_bexp_correct:
  forall C s b d1 d0 pc stk,
  code_at C pc (compile_bexp b d1 d0) ->
  Rstar (transition C)
       (pc, stk, s)
       (pc + codelen (compile_bexp b d1 d0) + (if beval s b then d1 else d0), stk, s).
Proof.
Admitted.

Now the new stuff

Inductive compile_cont (C: code): cont -> Z -> Prop :=
  | ccont_stop: forall pc,
      instr_at C pc = Some Ihalt ->
      compile_cont C Kstop pc
  | ccont_seq: forall c k pc pc',
      code_at C pc (compile_com c) ->
      pc' = pc + codelen (compile_com c) ->
      compile_cont C k pc' ->
      compile_cont C (Kseq c k) pc
  | ccont_while: forall b c k pc d pc' pc'',
      instr_at C pc = Some(Ibranch d) ->
      pc' = pc + 1 + d ->
      code_at C pc' (compile_com (WHILE b c)) ->
      pc'' = pc' + codelen (compile_com (WHILE b c)) ->
      compile_cont C k pc'' ->
      compile_cont C (Kwhile b c k) pc
  | ccont_branch: forall d k pc pc',
      instr_at C pc = Some(Ibranch d) ->
      pc' = pc + 1 + d ->
      compile_cont C k pc' ->
      compile_cont C k pc.
Hint Constructors compile_cont.
Inductive sim (C: code): com * cont * store -> config -> Prop :=
  | sim_intro: forall c k st pc,
      code_at C pc (compile_com c) ->
      compile_cont C k (pc + codelen (compile_com c)) ->
      sim C (c, k, st) (pc, nil, st).
Hint Constructors sim.
Fixpoint com_size (c: com) : nat :=
  match c with
  | SKIP => 1
  | ASSIGN x a => 1
  | (c1 ;; c2) => (com_size c1 + com_size c2 + 1)%coq_nat
  | IFTHENELSE b c1 c2 => (com_size c1 + com_size c2 + 1)%coq_nat
  | WHILE b c1 => (com_size c1 + 1)%coq_nat
  end.
Remark com_size_nonzero: forall c, (com_size c > 0)%coq_nat.
Proof.
  induction c; cbn; lia.
Qed.
Fixpoint cont_size (k: cont) : nat :=
  match k with
  | Kstop => 0
  | Kseq c k' => (com_size c + cont_size k')%coq_nat
  | Kwhile b c k' => cont_size k'
  end.
Definition measure (impconf: com * cont * store) : nat :=
  match impconf with (c, k, m) => (com_size c + cont_size k)%coq_nat end.

Require Import Coq.Program.Equality.

Lemma compile_cont_Kstop_inv:
  forall C pc s,
  compile_cont C Kstop pc ->
  exists pc',
  Rstar (transition C) (pc, nil, s) (pc', nil, s)
  /\ instr_at C pc' = Some Ihalt.
Proof.
  move=> C pc s H.
  remember Kstop as k.
  elim: H Heqk => //.
  - intros. exists pc0; split; eauto.
  - intros. subst. case: (H2 erefl) => [pc'' [A B]].
    exists pc''; split; eauto. apply: RStep; eauto. apply: trans_branch; eauto.
Qed.

These two were done in class, here for reference in case you didn't finish

Lemma compile_cont_Kseq_inv:
  forall C c k pc s,
  compile_cont C (Kseq c k) pc ->
  exists pc',
  Rstar (transition C) (pc, nil, s) (pc', nil, s)
  /\ code_at C pc' (compile_com c)
  /\ compile_cont C k (pc' + codelen(compile_com c)).
Proof.
  intros. dependent induction H.
- exists pc; split. apply RRefl. split; congruence.
- edestruct IHcompile_cont as (pc'' & A & B). eauto.
  exists pc''; split; auto. eapply RStep; eauto. eapply trans_branch; eauto.
Qed.

Lemma compile_cont_Kwhile_inv:
  forall C b c k pc s,
  compile_cont C (Kwhile b c k) pc ->
  exists pc',
  Rplus (transition C) (pc, nil, s) (pc', nil, s)
  /\ code_at C pc' (compile_com (WHILE b c))
  /\ compile_cont C k (pc' + codelen(compile_com (WHILE b c))).
Proof.
  intros. dependent induction H.
- exists (pc + 1 + d); split.
  apply Rplus_one. eapply trans_branch; eauto.
  split; congruence.
- edestruct IHcompile_cont as (pc'' & A & B & D). eauto.
  exists pc''; split; auto. eapply Rplus_left. eapply trans_branch; eauto. apply Rplus_star; auto.
Qed.

Exercise 1. Prove sim_skip. You may have done this in class -- that's fine!

Lemma sim_skip:
  forall C k s pc,
  compile_cont C k pc ->
  sim C (SKIP, k, s) (pc, nil, s).
Admitted.

Exercise 2. Prove simulation_step. I'm giving you the beginning of the proof, which doesn't need induction! inversion / helper lemmas are enough.

Lemma simulation_step:
  forall C impconf1 impconf2 machconf1,
  step impconf1 impconf2 ->
  sim C impconf1 machconf1 ->
  exists machconf2,
      (Rplus (transition C) machconf1 machconf2
       \/ (Rstar (transition C) machconf1 machconf2
           /\ (measure impconf2 < measure impconf1)%coq_nat))
   /\ sim C impconf2 machconf2.
Proof.
  move=> C impconf1 impconf2 machconf1 st mat.
  invert st; invert mat; simpl in *.
Admitted.

Exercise 3. Prove that the simulation extends to sequences of steps. Note that this does require induction.

Lemma simulation_steps:
  forall C impconf1 impconf2, Rstar step impconf1 impconf2 ->
  forall machconf1, sim C impconf1 machconf1 ->
  exists machconf2,
     Rstar (transition C) machconf1 machconf2
     /\ sim C impconf2 machconf2.
Proof.
Admitted.

Exercise 4. Next show that the initial configurations are in the simulation relation.

Lemma sim_initial_configs:
forall c s,
sim (compile_program c) (c, Kstop, s) (0, nil, s).
Proof.
Admitted.

Exercise 5. Finally, prove that the compiler is correct, given these previous lemmas. Note that this should not be a very long proof!

Definition machine_terminates (C: code) (s_init: store) (s_final: store) : Prop :=
  exists pc, Rstar (transition C) (0, nil, s_init) (pc, nil, s_final)
        /\ instr_at C pc = Some Ihalt.

Theorem compile_program_correct_terminating:
  forall c s s',
  Rstar step (c, Kstop, s) (SKIP, Kstop, s') ->
  machine_terminates (compile_program c) s s'.
Proof.
Admitted.

NOTE FOR EXERCISES 6&7: depending on the feature you want to add, this can get really hard! A suggestion for something that should be interesting but not terribly difficult is to add multiplication to the source: you can implement it with a series of instructions, similarly to how substraction is implemented by negation and addition, except the series of instructions will be much more involved. A much more challenging feature to add would be BREAK -- adding it to the source semantics is pretty straightforward, compiling it is tricky but doable, but getting the simulation relation right is quite subtle. But, I don't want to imply these are the only (or even best) options: this assignment is totally open ended, so you can add whatever you'd like!

With that in mind, I've added a few features to the target language: indirect branch (which branches to the address on the stack, and possibly is useful), and a bunch of basic stack manipulation operations, but if there is some operation that you need, run it by me first but probably adding it will be fine. If I say yes and you do that, redefine the instr inductive type here and use that in your compile_com' function below.

Exercise 6.

Add some feature to the source language: this means aexp, bexp, com, or adding another type of expression that is then used in one of those. The majority of this part of the assignment (updating your proofs of correctness) will be completed next week, but for this week, you need to design the feature and implement the compiler below. If your change affects aexps or bexps, you may need a new compile_aexp', etc, as well.

Fixpoint compile_com' (c: com) : code. Admitted.

Exercise 7.

Update the simulation relation to account for your new feature, and thus your new compile function. Depending on your feature, this may be highly non-trivial. If you want to start figuring out if you simulation relation makes sense, drop in your proofs from Exercises 2 and 4 and see if you can get a few cases to go through.

Inductive sim' (C: code): com * cont * store -> config -> Prop := .