PreTalent23.SplVM_before_third_session

From PreTalent23 Require Import Overture.
From Coq.Lists Require Import List.

This enables list notations: [] for the empty list and h :: t for the cons operation. Here, h is the head (the first element) of the list and t is the tail (the rest) of the list.

Import ListNotations.

A stack-based virtual machine

We introduce a simple stack-based machine that can be used to compute the results of SPL programs.

Stacks and stack elements

We are importing the list library as we will use lists as stacks. The idea is that the head of the list is the top of the stack.

We first define the element that can be pushed and popped on the stack of our stack-based virtual machine.

Inductive stack_elem :=
| NumEl (n : nat)
| BoolEl (b : bool).

Definition stack := list stack_elem.

Useful functions for working with stack

These functions play a role similar to the functions when_num and when_bool that we used for results in defining SPL's definition. These functions are examples of polymorphic (and dependent) functions: they take an argument A which is the type of the end result of the function. They take a function, which is applied if the top of the stack is suitable, and an element of type A which will be returned if the top of the stack is not suitable. Note that the first argument A appears in braces. This indicates that this argument is an implicit argument meaning that the user does not need to provide this argument explicitly; it can be inferred from the types of other arguments. Furthermore, note that we have not given any type for A. However, Coq can infer that the type of this argument should be a universe as A is later used as a type itself.

Definition pop_num {A} (s : stack) (a : A) (f : nat → stack → A) : A :=
  match s with
  | [] => a (* Stack is empty *)
  | se :: s' => (* top of the stack is the stack element se and the rest of the stack is s' *)
      match se with
      | NumEl n => f n s'
      | _ => a
      end
  end.

Definition pop_bool {A} (s : stack) (a : A) (f : bool → stack → A) : A :=
  match s with
  | [] => a (* Stack is empty *)
  | se :: s' => (* top of the stack is the stack element se and the rest of the stack is s' *)
      match se with
      | BoolEl b => f b s'
      | _ => a
      end
  end.

VM instructions and programs

The Instructions of the virtual machine simply manipulate the stack machine.

A VM program is simply a list of instructions which are executed one after another.

Definition VMProg := list VMInstr.

(* Example add23 := Add (Num 2) (Num 3). *)
Example add23 := [PushNum 2; PushNum 3; DoAdd ].

(* Example if3le5 := ITE ((Le (Num 3) (Num 5))) (Num 2) (Num 3). *)
Example if3le5 := [PushNum 3; PushNum 5; DoLe ; CJump 2; PushNum 3; Jump 1; PushNum 2].

(* Example bad_prog := ITE (Num 3) (Num 4) (Num 5). *)
Example bad_prog := [PushNum 3; CJump 2; PushNum 5; Jump 1; PushNum 4].

(* Example sub74 := Sub (Num 7) (Num 4). *)
Example sub74 := [PushNum 7; PushNum 4; DoSub ].

A definitional interpreter for the VM

We first define a function which performs the effects of a single instruction. This function takes a stack s and an instruction i and returns a pair consisting of a number (how much to jump; this is zero in most cases) and the stack after the performing the instruction.

Exercise (in class)

Complete the following definition.

Definition runVMInstr (s : stack) (i : VMInstr) : nat * stack :=
  match i with
  | PushNum n => (0, (NumEl n) :: s )
  | PushBool b => (0, (BoolEl b) :: s )
  | Jump j => (j, s )
  | CJump j =>
      pop_bool s (0, s ) (λ b s', if b then (j, s') else (0, s'))
  | DoAnd =>
      pop_bool s (0, s ) (λ b2 s', pop_bool s' (0, s') (λ b1 s'', (0, BoolEl (b1 && b2) :: s'')))
  | DoOr =>
      pop_bool s (0, s ) (λ b2 s', pop_bool s' (0, s') (λ b1 s'', (0, BoolEl (b1 || b2) :: s'')))
  | DoNot =>
      pop_bool s (0, s ) (λ b s', (0, BoolEl (negb b) :: s'))
  | DoLe =>
      pop_num s (0, s ) (λ n2 s', pop_num s' (0, s') (λ n1 s'', (0, BoolEl (Nat.leb n1 n2) :: s'')))
  | DoEq =>
      pop_num s (0, s ) (λ n2 s', pop_num s' (0, s') (λ n1 s'', (0, BoolEl (Nat.eqb n1 n2) :: s'')))
  | DoAdd =>
      pop_num s (0, s ) (λ n2 s', pop_num s' (0, s') (λ n1 s'', (0, NumEl (n1 + n2) :: s'')))
  | DoSub =>
      pop_num s (0, s ) (λ n2 s', pop_num s' (0, s') (λ n1 s'', (0, NumEl (n1 - n2) :: s'')))
  | DoMul =>
      pop_num s (0, s ) (λ n2 s', pop_num s' (0, s') (λ n1 s'', (0, NumEl (n1 * n2) :: s'')))
  end.

The definitional interpreter for programs is a function that takes a stack, the number of instructions to skip (caused presumably by a prior jump) and the stack at the end of evaluation.

Fixpoint runVMProg (s : stack) (skip : nat) (p : VMProg) : nat * stack :=
  match p with
  | [] => (skip , s ) (* we have reached the end of the program *)
  | vmi :: p' =>
      match skip with
      | 0 => (* if we don't have to jump over any instructions. *)
          let (sk, s') := runVMInstr s vmi in
          runVMProg s' sk p'
      | S skip' => (* if we are (still) jumping over instructions. *)
          runVMProg s skip' p'
      end
  end.

Discuss in class

Why is the recursive function above terminating?

Eval compute in runVMProg [] 0 add23. (* Should print: (0, [NumEl 5]) *)

Eval compute in runVMProg [] 0 if3le5. (* Should print: (0, [NumEl 2#]) *)

Eval compute in runVMProg [] 0 bad_prog. (* Should print: (0, [NumEl 5; NumEl 3]) *)

Eval compute in runVMProg [] 0 sub74. (* Should print: (0, [NumEl 3]) *)

The following two lemmas are important lemmas that we will use in verifying our compiler from SPL to SPLVM.

Exercise (in class)

Prove the following lemma.

Lemma runVMProg_app s skip p1 p2 :
runVMProg s skip (p1 ++ p2) = let (skip', s') := runVMProg s skip p1 in runVMProg s' skip' p2.
Proof.
Admitted.

Exercise

Prove the following lemma.

Lemma runVMProg_jump s skip p1 p2 :
length p1 = skip → runVMProg s skip (p1 ++ p2) = runVMProg s 0 p2.
Proof.
Admitted.