File 10

20pts * Adding a feature to IMP

In this assignment you'll add a language feature to IMP and prove the compiler from it to the stack machine target correct.

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

First, some preliminaries

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.

5pts Exercise 1. Define your language feature and compiler. I'm including the existing language and compiler; make changes as needed. If you need to change the target language, please confirm with me that the change is okay. If it is a new instruction, it will probably be fine: send both the instruction syntax and the transition rule. If it is more extensive, it may be fine -- just check first.

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
  | Iswap2
  | 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_swap2 : forall pc stk s n1 n2 n3,
      instr_at C pc = Some(Iswap2) ->
      transition C (pc , n1 :: n2 :: n3 :: stk , s)
                 (pc + 1, n3 :: 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 assignments. You may need to use them again. You don't need to re-prove them! But if you add new lemmas, you do need to prove them, of course. If it's easier to keep track, feel free to paste in your proofs.

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.

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.
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.
Admitted.

Require Import Coq.Program.Equality.

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)).
Admitted.

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))).
Admitted.

15pts Exercise 2. Prove it correct! Likely you can re-use much of your proofs from last week (note that these definitions won't currently typecheck, as you need to add in the definitions), but since you may be changing some of them, I'm not fixing them.

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.