PreTalent22.Compiler_in_class

From PreTalent22 Require Import Overture.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent22 Require Import Spl_completed SplVM_in_class.

Import ListNotations.

The compiler from SPL to SPLVM and its correctness

Our compiler is a simple recursive function that translates SPL programs to SPLVM programs (lists of SPLVM instructions).

Exercise (in class)

Prove the following lemma.

Fixpoint compile (e : expr) : VMProg :=
  match e with
  | Num n => [PushNum n]
  | Bool b => [PushBool b]
  | ITE c t f =>
      let vm_c := compile c in
      let vm_t := compile t in
      let vm_f := compile f in
      vm_c ++ [CJump (S (length vm_f))] ++ (vm_f ++ [Jump (length vm_t)]) ++ vm_t
  | And e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoAnd ]
  | Or e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoOr ]
  | Not e =>
      let vm_e := compile e in
      vm_e ++ [DoNot ]
  | Le e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoLe ]
  | Eq e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoEq ]
  | Add e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoAdd ]
  | Sub e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoSub ]
  | Mul e1 e2 =>
      let vm_e1 := compile e1 in
      let vm_e2 := compile e2 in
      vm_e1 ++ vm_e2 ++ [DoMul ]
  end.

(* Some test cases for the compilation function above. *)

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

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

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

Discuss in class

How can the compiler be correct (also see the correctness theorem below) when it is returning a result (the element on the top of the stack) in a case where the eval function returns Err?

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

The result relation

We define the relation that we expect to hold between the results obtained by the eval function on a program and the results we expect to get by running the corresponding virtual machine.

Inductive result_rel : result → stack_elem → Prop :=
| num_res_rel n : result_rel (NumRes n) (NumEl n)
| bool_res_rel b : result_rel (BoolRes b) (BoolEl b).

The following theorem states the correctness property for our compiler: when we run the compiled version of a program on the empty stack we get back a stack that contains the only the expected result.

Exercise (partly in class)

Prove the following Theorem.

Lemma compile_correct_gen e s :
  eval e ≠ Err →
  ∃ se , runVMProg s 0 (compile e) = (0, se :: s ) ∧ result_rel (eval e) se.
Proof.
  revert s.
  induction e; intros s He.
  - eexists; split; [reflexivity|constructor].
  - eexists; split; [reflexivity|constructor].
  - simpl in *.
    pose proof (when_bool_not_Err _ _ He) as He1.
    destruct (IHe1 s He1) as [se1 [Hse11 Hse12]].
    pose proof (when_bool_correct1 _ _ He) as [e1b He1b].
    rewrite He1b in He; simpl in He.
    destruct e1b.
    + destruct (IHe2 s He) as [se2 [Hse21 Hse22]].
      eexists; split.
      * rewrite runVMProg_app.
        rewrite Hse11.
        rewrite He1b in Hse12.
        inversion Hse12; subst.
        simpl.
        rewrite runVMProg_jump.
        -- apply Hse21.
        -- rewrite app_length; simpl. lia.
      * rewrite He1b; simpl. trivial.
    + destruct (IHe3 s He) as [se3 [Hse31 Hse32]].
      eexists; split.
      * rewrite runVMProg_app.
        rewrite Hse11.
        rewrite He1b in Hse12.
        inversion Hse12; subst.
        simpl.
        rewrite runVMProg_app.
        rewrite runVMProg_app.
        rewrite Hse31. simpl.
        rewrite runVMProg_whole_jump; trivial.
      * rewrite He1b; simpl. trivial.
  - simpl in *.
    pose proof (when_bool_not_Err _ _ He) as He1.
    destruct (IHe1 s He1) as [se1 [Hse11 Hse12]].
    pose proof (when_bool_correct1 _ _ He) as [e1b He1b].
    rewrite He1b in He; simpl in He.
    pose proof (when_bool_not_Err _ _ He) as He2.
    destruct (IHe2 (se1 :: s) He2) as [se2 [Hse21 Hse22]].
    pose proof (when_bool_correct1 _ _ He) as [e2b He2b].
    eexists; split.
    + rewrite runVMProg_app.
      rewrite Hse11.
      rewrite runVMProg_app.
      rewrite Hse21.
      rewrite He1b in Hse12.
      inversion Hse12; subst.
      rewrite He2b in Hse22.
      inversion Hse22; subst.
      simpl.
      reflexivity.
    + rewrite He1b, He2b. simpl. constructor.
Abort.

Theorem compile_correct e :
  eval e ≠ Err →
  ∃ se , runVMProg [] 0 (compile e) = (0, [se ]) ∧ result_rel (eval e) se.
Proof.
Abort.