File 4

Language semantics

Due2019-10-10 11:45AM
ReadingLF/dbp Imp, PLF/dbp Smallstep
Linkhttps://github.ccs.neu.edu/verifcomp/19/asgn/4.v
This assignment will get you started dealing with languages and semantics in Coq.

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.

Definition X := "X"%string.
Definition Y := "Y"%string.
Definition Z := "Z"%string.

Definition state := string -> nat.

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.
Definition bool_to_bexp (b : bool) : bexp :=
  if b then BTrue else BFalse.
Coercion bool_to_bexp : bool >-> bexp.

Bind Scope imp_scope with aexp.
Bind Scope imp_scope with bexp.
Delimit Scope imp_scope with imp.

Notation "x + y" := (APlus x y) (at level 50, left associativity) : imp_scope.
Notation "x - y" := (AMinus x y) (at level 50, left associativity) : imp_scope.
Notation "x * y" := (AMult x y) (at level 40, left associativity) : imp_scope.
Notation "x <= y" := (BLe x y) (at level 70, no associativity) : imp_scope.
Notation "x = y" := (BEq x y) (at level 70, no associativity) : imp_scope.
Notation "x && y" := (BAnd x y) (at level 40, left associativity) : imp_scope.
Notation "'~' b" := (BNot b) (at level 75, right associativity) : imp_scope.

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x
  | APlus a1 a2 => (aeval st a1) + (aeval st a2)
  | AMinus a1 a2 => (aeval st a1) - (aeval st a2)
  | AMult a1 a2 => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => (aeval st a1) == (aeval st a2)
  | BLe a1 a2 => (aeval st a1) <= (aeval st a2)
  | BNot b1 => negb (beval st b1)
  | BAnd b1 b2 => andb (beval st b1) (beval st b2)
  end.

Definition empty_st := fun (_ : string) => 0.
Definition extend_st a x (st : state) :=
  (fun (a' : string) => if String.eqb a a' then x
                     else st a).
Notation "a '!->' x" := (extend_st a x empty_st) (at level 100).
Notation "a '!->' x ';' s" := (extend_st a x s)
                                (at level 100, x at next level, right associativity).

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).
Bind Scope imp_scope with com.
Notation "'SKIP'" :=
   CSkip : imp_scope.
Notation "x '::=' a" :=
  (CAss x a) (at level 60) : imp_scope.
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity) : imp_scope.
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity) : imp_scope.
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=
  (CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.

Reserved Notation "st '=[' c ']=>' st'"
         (at level 40).

Inductive ceval : com -> state -> state -> Prop :=
| E_Skip : forall st,
    st =[ SKIP ]=> st
| E_Ass : forall st a1 n x,
    aeval st a1 = n ->
    st =[ x ::= a1 ]=> (x !-> n ; st)
  | E_Seq : forall c1 c2 st st' st'',
      st =[ c1 ]=> st' ->
      st' =[ c2 ]=> st'' ->
      st =[ c1 ;; c2 ]=> st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      st =[ c1 ]=> st' ->
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      st =[ c2 ]=> st' ->
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      st =[ WHILE b DO c END ]=> st
  | E_WhileTrue : forall st st' st'' b c,
      beval st b = true ->
      st =[ c ]=> st' ->
      st' =[ WHILE b DO c END ]=> st'' ->
      st =[ WHILE b DO c END ]=> st''
where "st =[ c ]=> st'" := (ceval c st st').

Exercise 1. Write a relation bevalR in the same style as aevalR in LF/dbp Imp.

Inductive bevalR: state -> bexp -> bool -> Prop :=
.

Exercise 2. Prove that it is equivalent to beval.

Lemma beval_iff_bevalR : forall st b bv,
  bevalR st b bv <-> beval st b = bv.
Proof.
Admittted.

Exercise 3.
Definition loop : com :=
  WHILE true DO
    SKIP
  END % imp.

Theorem loop_never_stops : forall st st',
  ~(st =[ loop ]=> st').
Proof.
Admitted.

Exercise 4.
Consider the following function:

Open Scope imp_scope.
Fixpoint no_whiles (c : com) : bool :=
  match c with
  | SKIP =>
      true
  | _ ::= _ =>
      true
  | c1 ;; c2 =>
      andb (no_whiles c1) (no_whiles c2)
  | TEST _ THEN ct ELSE cf FI =>
      andb (no_whiles ct) (no_whiles cf)
  | WHILE _ DO _ END =>
      false
  end.
Close Scope imp_scope.

This predicate yields true just on programs that have no while loops. Using Inductive, write a property no_whilesR such that no_whilesR c is provable exactly when c is a program with no while loops. Then prove its equivalence with no_whiles.

Inductive no_whilesR: com -> Prop :=
.

Exercise 5.
Theorem no_whiles_eqv:
   forall c, no_whiles c = true <-> no_whilesR c.
Proof.
Admitted.

Exercise 6.
Imp programs that don't involve while loops always terminate. State and prove a theorem no_whiles_terminating that says this.
Use either no_whiles or no_whilesR, as you prefer.

Theorem no_whiles_terminating : forall st c, no_whilesR c -> exists st', st =[ c ]=> st'.
Proof.
Admitted.

Stack machines

Exercise 7.
Old HP Calculators, programming languages like Forth and Postscript, and abstract machines like the Java Virtual Machine all evaluate arithmetic expressions using a stack. For instance, the expression 
      (2*3)+(3*(4-2))
would be written as 
      2 3 * 3 4 2 - * +
and evaluated like this (where we show the program being evaluated on the right and the contents of the stack on the left): 
      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |
The goal of this exercise is to write a small compiler that translates aexps into stack machine instructions.
The instruction set for our stack language will consist of the following instructions:
  • SPush n: Push the number n on the stack.
  • SLoad x: Load the identifier x from the store and push it on the stack
  • SPlus: Pop the two top numbers from the stack, add them, and push the result onto the stack.
  • SMinus: Similar, but subtract.
  • SMult: Similar, but multiply.

Inductive sinstr : Type :=
| SPush (n : nat)
| SLoad (x : string)
| SPlus
| SMinus
| SMult.

Write a function to evaluate programs in the stack language. It should take as input a state, a stack represented as a list of numbers (top stack item is the head of the list), and a program represented as a list of instructions, and it should return the stack after executing the program. Test your function on the examples below.
Note that the specification leaves unspecified what to do when encountering an SPlus, SMinus, or SMult instruction if the stack contains less than two elements. In a sense, it is immaterial what we do, since our compiler will never emit such a malformed program.

Fixpoint s_execute (st : state) (stack : seq nat)
                   (prog : seq sinstr)
  : seq nat. Admitted.

Example s_execute1 :
     s_execute empty_st [::]
       [:: SPush 5; SPush 3; SPush 1; SMinus]
     = [:: 2; 5].
Admitted.

Example s_execute2 :
     s_execute (X !-> 3) [:: 3;4]
       [:: SPush 4; SLoad X; SMult; SPlus]
   = [:: 15; 4].
Admitted.

Exercise 8.
Next, write a function that compiles an aexp into a stack machine program. The effect of running the program should be the same as pushing the value of the expression on the stack.

Fixpoint s_compile (e : aexp) : seq sinstr. Admitted.

After you've defined s_compile, use the following to test that it works.

Example s_compile1 :
  s_compile (X - (2 * Y))%imp
  = [:: SLoad X; SPush 2; SLoad Y; SMult; SMinus].
Admitted.

Exercise 9.
Now we'll prove the correctness of the compiler implemented in the previous exercise. Remember that the specification left unspecified what to do when encountering an SPlus, SMinus, or SMult instruction if the stack contains less than two elements. (In order to make your correctness proof easier you might find it helpful to go back and change your implementation!)
Prove the following theogrem. You will need to start by stating a more general lemma to get a usable induction hypothesis; the main theorem will then be a simple corollary of this lemma.

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [:: ] (s_compile e) = [:: aeval st e ].
Proof.
Admitted.