feat: partial proof for about_fetch_decode_execute_loop

cs3234/labs/term-project.v

@@ -422,55 +422,129 @@ Inductive result_of_decoding_and_execution : Type :=
   OK : data_stack -> result_of_decoding_and_execution
 | KO : string -> result_of_decoding_and_execution.
 
-(* Informal specification of decode_execute : byte_code_instruction -> data_stack -> result_of_decoding_and_execution
 
- * given a nat n and a data_stack ds,
+(* Task 2:
+   implement decode_execute
+*)
+
+
+
+
+
+Definition specification_of_decode_execute (decode_execute : byte_code_instruction -> data_stack -> result_of_decoding_and_execution) :=
+  (* given a nat n and a data_stack ds,
    evaluating
      decode_execute (PUSH n) ds
-   should successfully return a stack where n is pushed on ds
+   should successfully return a stack where n is pushed on ds *)
-
+  (forall (n : nat)
- * given a data stack ds that contains at least two nats,
+     (ds : data_stack),
+      decode_execute (PUSH n) ds = OK (n :: ds))
+  /\
+    (* given a data stack ds that contains at least two nats,
    evaluating
      decode_execute ADD ds
    should
    - pop these two nats off the data stack,
    - add them,
    - push the result of the addition on the data stack, and
-   - successfully return the resulting data stack
+   - successfully return the resulting data stack *)
-
+  (forall (n1 n2 : nat)
-   if the data stack does not contain at least two nats,
+     (ds : data_stack),
+      decode_execute ADD (n2 :: n1 :: ds) = OK ((n1 + n2) :: ds)
+  )
+  /\
+ (* if the data stack does not contain at least two nats,
    evaluating
      decode_execute ADD ds
-   should return the error message "ADD: stack underflow"
+   should return the error message "ADD: stack underflow" *)
-
+  (forall (ds : data_stack),
- * given a data stack ds that contains at least two nats,
+      decode_execute ADD nil = KO ("ADD: stack underflow")
+  )
+  /\
+  (forall (n : nat)
+     (ds : data_stack),
+      decode_execute ADD nil = KO ("ADD: stack underflow")
+  )
+  /\
+ (* given a data stack ds that contains at least two nats,
    evaluating
      decode_execute SUB ds
    should
    - pop these two nats off the data stack,
    - subtract one from the other if the result is non-negative,
    - push the result of the subtraction on the data stack, and
-   - successfully return the resulting data stack
+   - successfully return the resulting data stack *)
-
+  (forall (n1 n2 : nat)
-   if the data stack does not contain at least two nats
+     (ds : data_stack),
-   evaluating
+      n1 <? n2 = true ->
-     decode_execute SUB ds
+      decode_execute SUB (n2 :: n1 :: ds) = KO (String.append "numerical underflow: -" (string_of_nat (n2 - n1))))
-   should return the error message "SUB: stack underflow"
+  /\
-
+ (* if the data stack contain at least two nats
-   if the data stack contain at least two nats
    and
-   if subtracting one nat from the other gives a negative result, 
+   if subtracting one nat from the other gives a negative result,
    evaluating
      decode_execute SUB ds
-   should return the same error message as the evaluator
+   should return the same error message as the evaluator *)
-*)
+  (forall (n1 n2 : nat)
-
+     (ds : data_stack),
-(* Task 2:
+      n1 <? n2 = false ->
-   implement decode_execute
+      decode_execute SUB (n2 :: n1 :: ds) = OK ((n2 - n1) :: ds))
-*)
+  /\
+ (* if the data stack does not contain at least two nats
+   evaluating
+     decode_execute SUB ds
+   should return the error message "SUB: stack underflow" *)
+  (forall (ds : data_stack),
+      decode_execute SUB nil = KO ("ADD: stack underflow")
+  )
+  /\
+  (forall (n : nat)
+     (ds : data_stack),
+      decode_execute SUB nil = KO ("ADD: stack underflow")
+  ).
 
 Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : result_of_decoding_and_execution :=
-  KO "to be implemented".
+  match bci with
+  | PUSH n => OK (n :: ds)
+  | ADD =>
+      match ds with
+      | n2 :: n1 :: ds' => OK ((n1 + n2) :: ds')
+      | _ => KO "ADD: stack underflow"
+      end
+  | SUB =>
+      match ds with
+      | n2 :: n1 :: ds' =>
+          if n1 <? n2
+          then KO (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))
+          else OK ((n2 - n1) :: ds')
+      | _ => KO "ADD: stack underflow"
+      end
+  end.
+
+Theorem decode_execute_satisfies_the_specification_of_decode_execute :
+  specification_of_decode_execute decode_execute.
+Proof.
+  unfold specification_of_decode_execute.
+  split; unfold decode_execute.
+  { reflexivity. }
+  split.
+  { reflexivity. }
+  split.
+  { reflexivity. }
+  split.
+  { reflexivity. }
+  split.
+  {  intros n1 n2 ds n1_lt_n2.
+     rewrite -> n1_lt_n2.
+     reflexivity. }
+  split.
+  {  intros n1 n2 ds n1_lt_n2.
+     rewrite -> n1_lt_n2.
+     reflexivity. }
+  split.
+  { reflexivity. }
+  reflexivity.
+Qed.
 
 (* ********** *)
 
@@ -495,10 +569,82 @@ Definition specification_of_fetch_decode_execute_loop (fetch_decode_execute_loop
       fetch_decode_execute_loop (bci :: bcis') ds =
       KO s).
 
+Theorem there_is_at_most_one_fetch_decode_execute_loop :
+  forall (f g : list byte_code_instruction -> data_stack -> result_of_decoding_and_execution),
+    specification_of_fetch_decode_execute_loop f ->
+    specification_of_fetch_decode_execute_loop g ->
+    forall (bcis : list byte_code_instruction)
+      (ds : data_stack),
+    f bcis ds = g bcis ds.
+Proof.
+  intros f g.
+  unfold specification_of_fetch_decode_execute_loop.
+  intros [S_f_nil [S_f_OK S_f_KO]] [S_g_nil [S_g_OK S_g_KO]] bcis.
+  induction bcis as [ | bci bcis' IHbcis' ]; intros ds.
+  - rewrite -> S_g_nil.
+    exact (S_f_nil ds).
+  - case (decode_execute bci ds) as [ ds' | s ] eqn:H_decode_execute.
+    + rewrite -> (S_f_OK bci bcis' ds ds' H_decode_execute).
+      rewrite -> (S_g_OK bci bcis' ds ds' H_decode_execute).
+      exact (IHbcis' ds').
+    + rewrite -> (S_g_KO bci bcis' ds s H_decode_execute).
+      exact (S_f_KO bci bcis' ds s H_decode_execute).
+Qed.
+
+Fixpoint fetch_decode_execute_loop (bcis : list byte_code_instruction) (ds : data_stack) : result_of_decoding_and_execution :=
+  match bcis with
+  | nil => OK ds
+  | bci :: bcis' =>
+      match (decode_execute bci ds) with
+      | OK ds' => fetch_decode_execute_loop bcis' ds'
+      | KO s => KO s
+      end
+  end.
+
+Lemma fold_unfold_fetch_decode_execute_loop_nil :
+  forall (ds : data_stack),
+    fetch_decode_execute_loop nil ds = OK ds.
+Proof.
+  fold_unfold_tactic fetch_decode_execute_loop.
+Qed.
+
+Lemma fold_unfold_fetch_decode_execute_loop_cons :
+  forall (bci : byte_code_instruction)
+    (bcis : list byte_code_instruction)
+    (ds : data_stack),
+    fetch_decode_execute_loop (bci :: bcis) ds =
+      match (decode_execute bci ds) with
+      | OK ds' => fetch_decode_execute_loop bcis ds'
+      | KO s => KO s
+      end.
+Proof.
+  fold_unfold_tactic fetch_decode_execute_loop.
+Qed.
+
+
+Theorem fetch_decode_execute_loop_satifies_the_specification :
+  specification_of_fetch_decode_execute_loop fetch_decode_execute_loop.
+Proof.
+  unfold specification_of_fetch_decode_execute_loop.
+  split.
+  { intros ds.
+    exact (fold_unfold_fetch_decode_execute_loop_nil ds). }
+split.
+  { intros bci bcis' ds ds' H_decode_execute.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+    rewrite -> H_decode_execute.
+    reflexivity.
+  }
+  intros bci bcis' ds s H_decode_execute.
+  rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+  rewrite -> H_decode_execute.
+  reflexivity.
+Qed.
+
 (* Task 3:
-   a. time permitting, prove that the definition above specifies at most one function;
+(DONE)   a. time permitting, prove that the definition above specifies at most one function;
-   b. implement this function; and
+(DONE)   b. implement this function; and
-   c. verify that your function satisfies the specification.
+(DONE)   c. verify that your function satisfies the specification.
 *)
 
 (* ********** *)
@@ -510,6 +656,30 @@ Definition specification_of_fetch_decode_execute_loop (fetch_decode_execute_loop
    in terms of executing bci1s and of executing bci2s.
 *)
 
+
+Proposition about_fetch_decode_execute_loop :
+  forall (bci1s bci2s : list byte_code_instruction)
+    (ds ds' : data_stack),
+    fetch_decode_execute_loop bci1s ds = OK ds' ->
+    fetch_decode_execute_loop (bci1s ++ bci2s) ds =
+      fetch_decode_execute_loop bci2s (ds').
+Proof.
+  intros bci1s.
+  induction bci1s as [ | bci bci1s' IHbci1s' ]; intros bci2s ds ds' H_fdel.
+  - rewrite -> fold_unfold_list_append_nil.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
+    injection H_fdel as ds_eq_ds'.
+    rewrite -> ds_eq_ds'.
+    reflexivity.
+  - rewrite -> fold_unfold_list_append_cons.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
+    case (decode_execute bci ds) as [ ds1 | s ] eqn:H_decode_execute.
+    + rewrite -> (IHbci1s' bci2s ds1 ds' H_fdel).
+      reflexivity.
+    + discriminate H_fdel.
+Qed.
+
 (* ********** *)
 
 Definition specification_of_run (run : target_program -> expressible_value) :=