Validation of the Compiler for the Stack Machine (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Imp.html.html)

coq_stackcomp.v

(*******************************************************)
(** //// Validation of the Stack Machine Compiler //// *)
(*******************************************************)

Require Import List.

(* Definition : Identifiers *)
Inductive id : Type :=
    | Id : nat -> id.

(* Definition : states *)
Definition state : Type := id -> nat.

(* Definition : Arithmetic expressions *)
Inductive aexp : Type :=
    | ANum   : nat -> aexp
    | AId    : id -> aexp
    | APlus  : aexp -> aexp -> aexp
    | AMinus : aexp -> aexp -> aexp
    | AMult  : aexp -> aexp -> aexp.

(* Definition : Evaluation of arithmetic expressions *)
Fixpoint aeval (st : state) (e : aexp) : nat :=
    match e 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.

(* Definition : Stack instructions *)
Inductive sinstr : Type :=
    | SPush  : nat -> sinstr
    | SLoad  : id -> sinstr
    | SPlus  : sinstr
    | SMinus : sinstr
    | SMult  : sinstr.

(* Definition : Execution of stack instructions *)
Fixpoint s_execute (st : state) (op_stack : option (list nat))
                   (prog : list sinstr)
                   : option (list nat) :=
    match op_stack with
    | None => None
    | Some stack =>
          match prog with
          | nil => Some stack
          | i :: prog' =>
                match i with
                | SPush n =>
                      s_execute st (Some (n :: stack)) prog'
                | SLoad X =>
                      s_execute st (Some (st X :: stack)) prog'
                | SPlus =>
                      match stack with
                      | nil => None
                      | _ :: nil => None
                      | n2 :: n1 :: stack' =>
                            s_execute st (Some (n1 + n2 :: stack'))
                                      prog'
                      end
                | SMinus =>
                      match stack with
                      | nil => None
                      | _ :: nil => None
                      | n2 :: n1 :: stack' =>
                            s_execute st (Some (n1 - n2 :: stack'))
                                      prog'
                      end
                | SMult =>
                      match stack with
                      | nil => None
                      | _ :: nil => None
                      | n2 :: n1 :: stack' =>
                            s_execute st (Some (n1 * n2 :: stack'))
                                      prog'
                      end
                end
          end
    end.

(* Definition : Compiler *)
Fixpoint s_compile (a : aexp) : list sinstr :=
    match a with
    | ANum n => SPush n :: nil 
    | AId X => SLoad X :: nil
    | APlus  a1 a2 => s_compile a1 ++ s_compile a2 ++ SPlus :: nil
    | AMinus a1 a2 => s_compile a1 ++ s_compile a2 ++ SMinus :: nil
    | AMult  a1 a2 => s_compile a1 ++ s_compile a2 ++ SMult :: nil
    end.

(* Lemma : In case the execution of the head seucceeds *)
Lemma s_compile_cons_success :
    forall (st : state) (stack stack' : list nat)
           (i : sinstr) (is : list sinstr),
    s_execute st (Some stack) (i :: nil) = Some stack' ->
    s_execute st (Some stack) (i :: is) =
    s_execute st (Some stack') is.
Proof.
    intros st stack stack' i is H.
    induction i as [n | X | | |];
    
        (* Cases : i = SPush n , SLoad X *)
        try(
            simpl in *;
            rewrite H;
            reflexivity
        );
    
        (* Cases : i = SPlus, SMinus, SMult *)
        induction stack as [| n2 stack2 _];
        
            (* Case : stack = nil *)
            try(
                simpl in H;
                discriminate
            );
         
            (* Case : stack = n2 :: stack2 *)
            induction stack2 as [| n1 stack1 _];
            
                (* Case : stack2 = nil *)
                try(
                    simpl in H;
                    discriminate
                );
            
                (* Case : stack2 = n1 :: stack1 *)
                simpl in *;
                rewrite H;
                reflexivity.
Qed.

(* Lemma : In case the execution of the head fails *)
Lemma s_compile_cons_failure :
    forall (st : state) (stack : list nat)
           (i : sinstr) (is : list sinstr),
    s_execute st (Some stack) (i :: nil) = None ->
    s_execute st (Some stack) (i :: is) = None.
Proof.
    intros st stack i is H.
    induction i as [n | X | | |];
    
        (* Cases : i = SPush n, SLoad X *)
        try(
            simpl in H;
            discriminate
        );
    
        (* Cases : i = SPlus, SMinus, SMult *)
        induction stack as [| n2 stack' _];
        
            (* Case : stack = nil *)
            try(
                simpl;
                reflexivity
            );
        
            (* Case : stack = n2 :: stack' *)
            induction stack' as [| n1 stack'' _];
            
                (* Case : stack' = nil *)
                try(
                    simpl;
                    reflexivity
                );
            
                (* Case : stack' = n2 :: n1 :: stack'' *)
                simpl in H;
                discriminate.
Qed.

(* Lemma : Compiling sequential instructions *)
Lemma s_compile_app : forall (st : state) (stack stack' : list nat)
                             (is1 is2 : list sinstr),
                      s_execute st (Some stack) is1 = Some stack' ->
                      s_execute st (Some stack) (is1 ++ is2) =
                      s_execute st (Some (stack')) is2.
Proof.
    intros st stack stack' is1 is2.
    generalize dependent stack'.
    generalize dependent stack.
    induction is1 as [| i is1' H_is1'].
    
        (* Case : is1 = nil *)
        intros stack stack' H.
        simpl in *.
        rewrite H.
        reflexivity.
    
        (* Case : is1 = i :: is1' *)
        intros stack stack' H.
        rewrite <- app_comm_cons.
        remember (s_execute st (Some stack) (i :: nil)) as op1.
        destruct op1 as [stack1 |].
        
            (* Case : s_execute st (Some stack) (i :: nil) =
                      Some stack1 *)
            symmetry in Heqop1.
            rewrite (s_compile_cons_success _ _ stack1 _ _ Heqop1).
            apply H_is1'.
            rewrite <- (s_compile_cons_success
                            _ stack _ i _ Heqop1).
            apply H.
        
            (* Case : s_execute st (Some stack) (i :: nil) = None *)
            symmetry in Heqop1.
            apply (s_compile_cons_failure _ _ _ is1') in Heqop1.
            rewrite Heqop1 in H.
            discriminate.
Qed.

(* Validation of the compiler (general form) *)
Lemma s_compile_correct' : forall (st : state) (stack : list nat)
                                  (a : aexp),
                           s_execute st (Some stack) (s_compile a) =
                           Some (aeval st a :: stack).
Proof.
    intros st stack a.
    generalize dependent stack.
    induction a as [n | X | a1 H1 a2 H2 | a1 H1 a2 H2 |
                    a1 H1 a2 H2];
    
        (* Cases : a = ANum n, AId X *)
        try(
            intro stack;
            simpl;
            reflexivity
        );
    
        (* Cases : a = APlus a1 a2, AMinus a1 a2, AMult a1 a2 *)
        intro stack;
        simpl;
        specialize H1 with stack; 
        rewrite (s_compile_app _ _ (aeval st a1 :: stack) _ _ H1);
        specialize H2 with (aeval st a1 :: stack);
        rewrite (s_compile_app
                     _ _ (aeval st a2 :: aeval st a1 :: stack)
                     _ _ H2);
        simpl;
        reflexivity.
Qed.

(* Validation of the compiler *)
Theorem s_compile_correct : forall (st : state) (a : aexp),
                            s_execute st (Some nil) (s_compile a) =
                            Some (aeval st a :: nil).
Proof.
    intros st a.
    apply s_compile_correct'.
Qed.