About the definition of s_execute

[jaewooklee93]

In our Assignment08_05.v, we have to prove the correctness of stack compiler

(* Assignment08_05.v *)

(** **** Exercise: 3 stars, advanced (stack_compiler_correct)  *)
(** The task of this exercise is to 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 may find it useful to go back and change your
    implementation!)

    Prove the following theorem, stating that the [compile] function
    behaves correctly.  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.

However, I think the definition of s_execute given in the Assignment08_00.v is inappropriate to make the proof of correctness easier;

(* Assignment08_00.v *)

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
                 : list nat :=
  match prog with
  | [] => stack
  | ins :: prog' => 
    match ins with
    | SPush n => s_execute st (n :: stack) prog'
    | SLoad x => s_execute st (st x :: stack) prog'
    | SPlus => 
      match stack with
      | na :: nb :: stack' => s_execute st (nb+na :: stack') prog'
      | _ => []
      end

because of the behavior at the error state. The definition you gave forces to stop the computation when invalid operations come in, but my desirable definition just ignores such invalid ops and keep going from the next ops.

Because of such slight difference at the error state, I cannot prove the following useful and intuitive Lemma with your definition, which is easily provable in my definition. execute (l1++l2) on stack = execute l2 on (execute l1 on stack) This lemma doesn't hold with your definition, the counterexample is l1=[SMult], l2=[SPush 0], stack=[]

So I want to modify your definition in Assignment08_00.v, but I think it is not allowed, but is there any possible way to alleviate this conflict between two def'ns?

[jeehoonkang]

I think I am gonna do:

• Define wellformed st stack prog: Prop that execution of prog with st and stack goes without ill-formed operations.
• Prove your lemma only for wellformed things.

Jeehoon

[jaewooklee93]

When I did this exercise by myself in the last week, it was relatively easy one which can be solved in 10 lines of codes, but now only the inductive definition of wellformed will may take at least 10 lines.

As comment said (In order to make your correctness proof easier you may find it useful to go back and change your implementation!), I think the intention of this exercise is to show the fact that the slight change of definition can lead us to much easier proof.

I will try to think more about this problem...

[jaewooklee93]

Finally, I solved this problem with defining a new interpreter which can track the liveness of program and simulate the original interpreter, but this solution takes more than 100 lines...

[jeehoonkang]

We updated the definition: 2b1591b9cf8b184dedceed37793573862836054d

[jaewooklee93]

Interestingly, my long proof continued to work well even though the definition of s_executed was changed. However, I also have replaced my previous submission with much compact proof of 5 lines.

[jeehoonkang]

@jaewooklee93 I believe that is because your proof did not rely on the altered part of the definition. It is the most pleasure thing that your proof is stripped down to 5 lines.

Jeehoon