From ca30dc084a3a8461cfa459f526f068c35fac17b5 Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Sat, 27 Apr 2024 17:13:14 +0800 Subject: [PATCH] feat: partial proof for about_fetch_decode_execute_loop --- cs3234/labs/term-project.v | 230 ++++++++++++++++++++++++++++++++----- 1 file changed, 200 insertions(+), 30 deletions(-) diff --git a/cs3234/labs/term-project.v b/cs3234/labs/term-project.v index 79d2b11..9ed317e 100644 --- a/cs3234/labs/term-project.v +++ b/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 - - * given a data stack ds that contains at least two nats, + should successfully return a stack where n is pushed on ds *) + (forall (n : nat) + (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 - - if the data stack does not contain at least two nats, + - successfully return the resulting data stack *) + (forall (n1 n2 : nat) + (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" - - * given a data stack ds that contains at least two nats, + should return the error message "ADD: stack underflow" *) + (forall (ds : data_stack), + 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 - - if the data stack does not contain at least two nats - evaluating - decode_execute SUB ds - should return the error message "SUB: stack underflow" - - if the data stack contain at least two nats + - successfully return the resulting data stack *) + (forall (n1 n2 : nat) + (ds : data_stack), + n1 + decode_execute SUB (n2 :: n1 :: ds) = KO (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))) + /\ + (* 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 -*) - -(* Task 2: - implement decode_execute -*) + should return the same error message as the evaluator *) + (forall (n1 n2 : nat) + (ds : data_stack), + n1 + 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 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; - b. implement this function; and - c. verify that your function satisfies the specification. +(DONE) a. time permitting, prove that the definition above specifies at most one function; +(DONE) b. implement this function; and +(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) :=