From 8948274c565137651a85173f24d5fb3845f49f4b Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Sun, 5 May 2024 12:24:07 +0800 Subject: [PATCH] feat: finish term project --- cs3234/labs/term-project.v | 715 ++++++++++++++++++++++++++++++++++++- 1 file changed, 696 insertions(+), 19 deletions(-) diff --git a/cs3234/labs/term-project.v b/cs3234/labs/term-project.v index 1ad6de2..3ccaa4d 100644 --- a/cs3234/labs/term-project.v +++ b/cs3234/labs/term-project.v @@ -7,6 +7,7 @@ (* Three language processors for arithmetic expressions. *) + (* group name: @@ -488,7 +489,7 @@ Definition specification_of_decode_execute (decode_execute : byte_code_instructi (forall (n1 n2 : nat) (ds : data_stack), n1 - decode_execute SUB (n2 :: n1 :: ds) = OK ((n2 - n1) :: ds)) + decode_execute SUB (n2 :: n1 :: ds) = OK ((n1 - n2) :: ds)) /\ (* if the data stack does not contain at least two nats evaluating @@ -516,7 +517,7 @@ Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : resu | n2 :: n1 :: ds' => if n1 KO "ADD: stack underflow" end end. @@ -725,6 +726,7 @@ Definition specification_of_run (run : target_program -> expressible_value) := run (Target_program bcis) = Expressible_msg s). +(* Since this is talking mostly about the data stack, thats where we will work from *) Theorem there_is_at_most_one_run_function : forall (f g : target_program -> expressible_value), specification_of_run f -> @@ -732,16 +734,93 @@ Theorem there_is_at_most_one_run_function : forall (t: target_program), f t = g t. Proof. - intros f g. - unfold specification_of_run. - intros S_f S_g [bcis]. - case (fetch_decode_execute_loop bcis nil) as [ds | s] eqn:H_fdel. - - destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _]. + intros f g S_f S_g [bcis]. + (* This was the tricky part in my understanding. We are operating on the result of FDEL. Thus, we + check every case of fdel and work from there *) + case (fetch_decode_execute_loop bcis nil) as [[| n [| n' ds'']] | s] eqn:H_fdel. + - unfold specification_of_run in S_f,S_g. + destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _]. destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_g_nil _]. - case ds as [ | n ds' ] eqn:H_ds. - + rewrite -> (S_g_nil bcis H_fdel). - exact (S_f_nil bcis H_fdel). - + Check (S_f_nil bcis). + rewrite -> (S_g_nil bcis H_fdel). + exact (S_f_nil bcis H_fdel). + - unfold specification_of_run in S_f,S_g. + destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_f_one _]]. + destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_g_one _]]. + rewrite -> (S_g_one bcis n H_fdel). + exact (S_f_one bcis n H_fdel). + - unfold specification_of_run in S_f,S_g. + destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_f_mult _]]]. + destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_g_mult _]]]. + rewrite -> (S_g_mult bcis n n' ds'' H_fdel). + exact (S_f_mult bcis n n' ds'' H_fdel). + - unfold specification_of_run in S_f,S_g. + destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_f_KO]]]. + destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_g_KO]]]. + rewrite -> (S_g_KO bcis s H_fdel). + exact (S_f_KO bcis s H_fdel). +Qed. + + +Definition run (p : target_program) : expressible_value := + match p with + Target_program bcis => + match (fetch_decode_execute_loop bcis nil) with + | OK nil => Expressible_msg "no result on the data stack" + | OK (n :: nil) => Expressible_nat n + | OK (n :: n' :: ds'') => Expressible_msg "too many results on the data stack" + | KO s => Expressible_msg s + end + end. + + +Theorem run_satisfies_the_specification_of_run : + specification_of_run run. +Proof. + unfold specification_of_run. + intros fdel. + intros S_fdel. + split. + { intros bcis H_fdel. + unfold run. + rewrite -> (there_is_at_most_one_fetch_decode_execute_loop + fetch_decode_execute_loop fdel + fetch_decode_execute_loop_satifies_the_specification S_fdel + bcis nil + ). + rewrite -> H_fdel. + reflexivity. } + split. + { intros bcis n H_fdel. + unfold run. + rewrite -> (there_is_at_most_one_fetch_decode_execute_loop + fetch_decode_execute_loop fdel + fetch_decode_execute_loop_satifies_the_specification S_fdel + bcis nil + ). + rewrite -> H_fdel. + reflexivity. + } + split. + { intros bcis n n' ds'' H_fdel . + unfold run. + rewrite -> (there_is_at_most_one_fetch_decode_execute_loop + fetch_decode_execute_loop fdel + fetch_decode_execute_loop_satifies_the_specification S_fdel + bcis nil + ). + rewrite -> H_fdel. + reflexivity. + } + intros bcis s H_fdel . + unfold run. + rewrite -> (there_is_at_most_one_fetch_decode_execute_loop + fetch_decode_execute_loop fdel + fetch_decode_execute_loop_satifies_the_specification S_fdel + bcis nil + ). + rewrite -> H_fdel. + reflexivity. +Qed. (* Task 4: @@ -762,6 +841,71 @@ Definition specification_of_compile_aux (compile_aux : arithmetic_expression -> (forall ae1 ae2 : arithmetic_expression, compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)). +Theorem there_is_at_most_one_compile_aux_function : + forall (f g : arithmetic_expression -> list byte_code_instruction), + (specification_of_compile_aux f) -> + (specification_of_compile_aux g) -> + forall (ae : arithmetic_expression), + f ae = g ae. +Proof. + intros f g S_f S_g ae. + destruct S_f as [S_f_Literal [S_f_Plus S_f_Minus]]. + destruct S_g as [S_g_Literal [S_g_Plus S_g_Minus]]. + induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2 ]. + - rewrite -> S_g_Literal. + exact (S_f_Literal n). + - rewrite -> S_g_Plus. + rewrite -> S_f_Plus. + rewrite -> IHae1. + rewrite -> IHae2. + reflexivity. + - rewrite -> S_g_Minus. + rewrite -> S_f_Minus. + rewrite -> IHae1. + rewrite -> IHae2. + reflexivity. +Qed. + +Fixpoint compile_aux (ae : arithmetic_expression) : (list byte_code_instruction) := + match ae with + | Literal n => PUSH n :: nil + | Plus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil) + | Minus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil) + end. + +Lemma fold_unfold_compile_aux_Literal : + forall (n : nat), + compile_aux (Literal n) = PUSH n :: nil. +Proof. + fold_unfold_tactic compile_aux. +Qed. + +Lemma fold_unfold_compile_aux_Plus : + forall (ae1 ae2 : arithmetic_expression), + compile_aux (Plus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil). +Proof. + fold_unfold_tactic compile_aux. +Qed. + +Lemma fold_unfold_compile_aux_Minus : + forall (ae1 ae2 : arithmetic_expression), + compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil). +Proof. + fold_unfold_tactic compile_aux. +Qed. + +Theorem compile_aux_satifies_the_specification_of_compile_aux : + specification_of_compile_aux compile_aux. +Proof. + unfold specification_of_compile_aux. + split. + { exact fold_unfold_compile_aux_Literal.} + split. + { exact fold_unfold_compile_aux_Plus.} + exact fold_unfold_compile_aux_Minus. +Qed. + + (* Task 5: a. time permitting, prove that the definition above specifies at most one function; b. implement this function using list concatenation, i.e., ++; and @@ -774,6 +918,37 @@ Definition specification_of_compile (compile : source_program -> target_program) forall ae : arithmetic_expression, compile (Source_program ae) = Target_program (compile_aux ae). +Theorem there_is_at_most_one_compile_function : + forall (f g : source_program -> target_program), + (specification_of_compile f) -> + (specification_of_compile g) -> + forall (sp : source_program), + f sp = g sp. +Proof. + intros f g. + unfold specification_of_compile. + intros S_f S_g [ae]. + rewrite -> (S_g compile_aux compile_aux_satifies_the_specification_of_compile_aux ae). + exact (S_f compile_aux compile_aux_satifies_the_specification_of_compile_aux ae). +Qed. + +Definition compile (sp : source_program) : target_program := + match sp with + | Source_program ae => Target_program (compile_aux ae) + end. + +Theorem compile_satifies_the_specification_of_compile : + specification_of_compile compile. +Proof. + unfold specification_of_compile, compile. + intros compile_aux' S_compile_aux' ae. + rewrite -> (there_is_at_most_one_compile_aux_function + compile_aux' compile_aux + S_compile_aux' compile_aux_satifies_the_specification_of_compile_aux ae). + reflexivity. +Qed. + + (* Task 6: a. time permitting, prove that the definition above specifies at most one function; b. implement this function; and @@ -782,6 +957,120 @@ Definition specification_of_compile (compile : source_program -> target_program) (* ********** *) +Fixpoint compile_alt_aux_acc (ae : arithmetic_expression) (acc : list byte_code_instruction) : (list byte_code_instruction) := + match ae with + | Literal n => PUSH n :: acc + | Plus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc))) + | Minus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc))) + end. + +Lemma fold_unfold_compile_alt_aux_acc_Literal : + forall (n : nat) + (acc : list byte_code_instruction), + compile_alt_aux_acc (Literal n) acc = PUSH n :: acc. +Proof. + fold_unfold_tactic compile_alt_aux_acc. +Qed. + +Lemma fold_unfold_compile_alt_aux_acc_Plus : + forall (ae1 ae2 : arithmetic_expression) + (acc : list byte_code_instruction), + compile_alt_aux_acc (Plus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc))). +Proof. + fold_unfold_tactic compile_alt_aux_acc. +Qed. + +Lemma fold_unfold_compile_alt_aux_acc_Minus : + forall (ae1 ae2 : arithmetic_expression) + (acc : list byte_code_instruction), + compile_alt_aux_acc (Minus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc))). +Proof. + fold_unfold_tactic compile_alt_aux_acc. +Qed. + +Definition compile_alt_aux (ae : arithmetic_expression) : list byte_code_instruction := + compile_alt_aux_acc ae nil. + +Lemma about_compile_alt_aux_acc : + forall (ae : arithmetic_expression) + (ds : list byte_code_instruction), + compile_alt_aux_acc ae ds = compile_alt_aux_acc ae nil ++ ds. + Proof. + intros ae. + induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]. + - intro ds. + Check (fold_unfold_compile_alt_aux_acc_Literal n ds). + rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n ds). + rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil). + rewrite -> fold_unfold_list_append_cons. + rewrite -> fold_unfold_list_append_nil. + reflexivity. + - intro ds. + rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2). + rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2). + rewrite -> (IHae2 (ADD :: ds)). + rewrite -> (IHae2 (ADD :: nil)). + rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: ds)). + rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)). + rewrite <- 2 app_assoc. + rewrite -> fold_unfold_list_append_cons. + rewrite -> fold_unfold_list_append_nil. + reflexivity. + - intro ds. + rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2). + rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2). + rewrite -> (IHae2 (SUB :: ds)). + rewrite -> (IHae2 (SUB :: nil)). + rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: ds)). + rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)). + rewrite <- 2 app_assoc. + rewrite -> fold_unfold_list_append_cons. + rewrite -> fold_unfold_list_append_nil. + reflexivity. +Qed. + +Theorem compile_alt_aux_satisifes_the_specification_of_compile_aux : + specification_of_compile_aux compile_alt_aux. +Proof. + unfold specification_of_compile_aux, compile_alt_aux. + split. + { intros n. + rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil). + reflexivity. } + split. + { intros ae1 ae2. + rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2 nil). + Check about_compile_alt_aux_acc. + rewrite -> (about_compile_alt_aux_acc ae2 (ADD :: nil)). + rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)). + + reflexivity. } + intros ae1 ae2. + rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2 nil). + Check about_compile_alt_aux_acc. + rewrite -> (about_compile_alt_aux_acc ae2 (SUB :: nil)). + rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)). + reflexivity. +Qed. + +Definition compile_alt (sp : source_program) : target_program := + match sp with + | Source_program ae => Target_program (compile_alt_aux ae) + end. + +Theorem compile_alt_satisfies_the_specificiation_of_compile : + specification_of_compile compile_alt. +Proof. + unfold specification_of_compile, compile_alt. + intros compile_aux' S_compile_aux ae. + rewrite -> (there_is_at_most_one_compile_aux_function + compile_aux' compile_alt_aux + S_compile_aux compile_alt_aux_satisifes_the_specification_of_compile_aux + ae + ). + reflexivity. +Qed. + (* Task 7: implement an alternative compiler using an auxiliary function with an accumulator @@ -795,8 +1084,155 @@ Definition specification_of_compile (compile : source_program -> target_program) (* ********** *) +Theorem the_commuting_diagram_evaluate_nat : + forall (ae : arithmetic_expression) + (n : nat) + (ds : data_stack), + evaluate ae = Expressible_nat n -> + fetch_decode_execute_loop (compile_aux ae) ds = OK (n :: ds). +Proof. + intro ae. + induction ae as [n | ae1 IHae1 ae2 IHae2| ae1 IHae1 ae2 IHae2]; + intros n' ds H_eval. + - rewrite -> fold_unfold_compile_aux_Literal. + rewrite -> fold_unfold_fetch_decode_execute_loop_cons. + unfold decode_execute. + rewrite -> fold_unfold_fetch_decode_execute_loop_nil. + rewrite -> fold_unfold_evaluate_Literal in H_eval. + injection H_eval as n_is_n'. + rewrite -> n_is_n'. + reflexivity. + - rewrite -> fold_unfold_compile_aux_Plus. + rewrite -> fold_unfold_evaluate_Plus in H_eval. + (* I need the 2 statements evaluate ae1 = Expressible_nat n *) + case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1. + + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2. + * injection H_eval as n1_plus_n2_is_n'. + Search fetch_decode_execute_loop. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append_ae1 _]. + rewrite -> (H_fdel_append_ae1 + (n1::ds) + (IHae1 n1 ds eq_refl) + ). + destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD :: nil) (n1 :: ds)) as [H_fdel_append_ae2 _]. + rewrite -> (H_fdel_append_ae2 + (n2::n1::ds) + (IHae2 n2 (n1::ds) eq_refl) + ). + rewrite -> fold_unfold_fetch_decode_execute_loop_cons. + unfold decode_execute. + rewrite -> fold_unfold_fetch_decode_execute_loop_nil. + rewrite -> n1_plus_n2_is_n'. + reflexivity. + * discriminate H_eval. + + discriminate H_eval. + - rewrite -> fold_unfold_compile_aux_Minus. + rewrite -> fold_unfold_evaluate_Minus in H_eval. + case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1. + + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2. + * case (n1 (H_fdel_append_ae1 + (n1::ds) + (IHae1 n1 ds eq_refl) + ). + destruct (about_fetch_decode_execute_loop + (compile_aux ae2) + (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _]. + rewrite -> (H_fdel_append_ae2 + (n2::n1::ds) + (IHae2 n2 (n1::ds) eq_refl) + ). + rewrite -> fold_unfold_fetch_decode_execute_loop_cons. + unfold decode_execute. + rewrite -> H_n1_lt_n2. + rewrite -> fold_unfold_fetch_decode_execute_loop_nil. + rewrite <- n1_minus_n2_is_n'. + reflexivity. + * discriminate H_eval. + + discriminate H_eval. +Qed. + +Theorem the_commuting_diagram_evaluate_msg : + forall (ae : arithmetic_expression) + (s : string) + (ds : data_stack), + evaluate ae = Expressible_msg s -> + fetch_decode_execute_loop (compile_aux ae) ds = KO s. + Proof. + intro ae. + induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intros s ds H_eval. + - rewrite -> fold_unfold_evaluate_Literal in H_eval. + discriminate H_eval. + - rewrite -> fold_unfold_evaluate_Plus in H_eval. + case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1. + + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2. + * discriminate H_eval. + * rewrite -> fold_unfold_compile_aux_Plus. + injection H_eval as s2_is_s. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append _]. + rewrite -> (H_fdel_append (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)). + destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD::nil) (n1::ds)) as [_ H_fdel_append_KO]. + rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)). + rewrite -> s2_is_s. + reflexivity. + + injection H_eval as s1_is_s. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [_ H_fdel_append_KO]. + rewrite -> fold_unfold_compile_aux_Plus. + rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)). + rewrite -> s1_is_s. + reflexivity. + - rewrite -> fold_unfold_evaluate_Minus in H_eval. + case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1. + + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2. + * case (n1 fold_unfold_compile_aux_Minus. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _]. + rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)). + destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _]. + rewrite -> (H_fdel_append_ae2 (n2::n1::ds) (the_commuting_diagram_evaluate_nat ae2 n2 (n1::ds) H_eval_ae2)). + rewrite -> fold_unfold_fetch_decode_execute_loop_cons. + unfold decode_execute. + rewrite -> H_n1_lt_n2. + injection H_eval as n1_lt_n2_msg. + simpl (KO ("numerical underflow: -" ++ string_of_nat (n2 - n1))). + rewrite -> n1_lt_n2_msg. + reflexivity. + ++ discriminate H_eval. + * injection H_eval as s2_is_s. + ++ rewrite -> fold_unfold_compile_aux_Minus. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _]. + rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)). + destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB::nil) (n1::ds)) as [_ H_fdel_append_KO]. + rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)). + rewrite -> s2_is_s. + reflexivity. + + injection H_eval as s1_is_s. + rewrite -> fold_unfold_compile_aux_Minus. + destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [_ H_fdel_append_KO]. + rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)). + rewrite -> s1_is_s. + reflexivity. + Qed. + +Theorem the_commuting_diagram : + forall (sp : source_program), + interpret sp = run (compile sp). +Proof. + intros [ae]. + unfold interpret, compile,run. + case evaluate as [n | s] eqn:H_eval. + - rewrite -> (the_commuting_diagram_evaluate_nat ae n nil H_eval). + reflexivity. + - rewrite -> (the_commuting_diagram_evaluate_msg ae s nil H_eval). + reflexivity. +Qed. (* Task 8 (the capstone): - Prove that interpreting an arithmetic expression gives the same result + as first compiling it and then executing the compiled program. *) @@ -829,6 +1265,33 @@ Fixpoint verify_aux (bcis : list byte_code_instruction) (n : nat) : option nat : end end. +Definition fold_unfold_verify_aux_nil : + forall (n : nat), + verify_aux nil n = Some n. +Proof. + fold_unfold_tactic verify_aux. +Qed. + +Definition fold_unfold_verify_aux_cons : + forall (bci : byte_code_instruction) + (bcis : list byte_code_instruction) + (n : nat), + verify_aux (bci :: bcis) n = + match bci with + | PUSH _ => + verify_aux bcis (S n) + | _ => + match n with + | S (S n') => + verify_aux bcis (S n') + | _ => + None + end + end. +Proof. + fold_unfold_tactic verify_aux. +Qed. + Definition verify (p : target_program) : bool := match p with | Target_program bcis => @@ -849,19 +1312,233 @@ Definition verify (p : target_program) : bool := Prove that the compiler emits code that is accepted by the verifier. *) - -(* -Theorem the_compiler_emits_well_behaved_code : - forall ae : arithmetic_expression, - verify (compile ae) = true. +Lemma about_verify_aux_some : + forall (bci1s bci2s : list byte_code_instruction) + (n n' : nat), + (verify_aux bci1s n) = Some n' -> + (verify_aux (bci1s ++ bci2s) n) = (verify_aux bci2s n'). Proof. -Abort. -*) + intros bci1s. + induction bci1s as [ | bci bci1s' IHbci1s' ]. + - intros bci2s n n' H_verify_aux. + rewrite -> fold_unfold_verify_aux_nil in H_verify_aux. + injection H_verify_aux as n_is_n'. + rewrite -> fold_unfold_list_append_nil. + rewrite -> n_is_n'. + reflexivity. + - intros bci2s n n' H_verify_aux. + rewrite -> fold_unfold_list_append_cons. + rewrite -> fold_unfold_verify_aux_cons. + case bci as [ x | | ] eqn:H_bci. + + rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + rewrite -> (IHbci1s' bci2s (S n) n' H_verify_aux). + reflexivity. + + case n as [ | [ | n'' ] ]. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + discriminate H_verify_aux. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + discriminate H_verify_aux. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux). + reflexivity. + + case n as [ | [ | n'' ] ]. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + discriminate H_verify_aux. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + discriminate H_verify_aux. + * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux. + rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux). + reflexivity. +Qed. + +Lemma compile_aux_emits_one_value : + forall (ae : arithmetic_expression) + (n : nat), + verify_aux (compile_aux ae) n = Some (S n). +Proof. + intro ae. + induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intro n'. + - rewrite -> fold_unfold_compile_aux_Literal. + rewrite -> fold_unfold_verify_aux_cons. + rewrite -> fold_unfold_verify_aux_nil. + reflexivity. + - rewrite -> fold_unfold_compile_aux_Plus. + rewrite -> (about_verify_aux_some + (compile_aux ae1) + (compile_aux ae2 ++ ADD :: nil) + n' (S n') + (IHae1 n')). + rewrite -> (about_verify_aux_some + (compile_aux ae2) + (ADD :: nil) + (S n') (S (S n')) + (IHae2 (S n'))). + rewrite -> fold_unfold_verify_aux_cons. + rewrite -> fold_unfold_verify_aux_nil. + reflexivity. + - rewrite -> fold_unfold_compile_aux_Minus. + rewrite -> (about_verify_aux_some + (compile_aux ae1) + (compile_aux ae2 ++ SUB :: nil) + n' (S n') + (IHae1 n')). + rewrite -> (about_verify_aux_some + (compile_aux ae2) + (SUB :: nil) + (S n') (S (S n')) + (IHae2 (S n'))). + rewrite -> fold_unfold_verify_aux_cons. + rewrite -> fold_unfold_verify_aux_nil. + reflexivity. +Qed. + + + +Theorem the_compiler_emits_well_behaved_code : + forall sp : source_program, + verify (compile sp) = true. +Proof. + intros [ae]. + unfold verify, compile. +rewrite -> (compile_aux_emits_one_value ae 0). +reflexivity. +Qed. + (* Subsidiary question: What is the practical consequence of this theorem? *) +Definition alternative_specification_of_run (run : target_program -> expressible_value) := + forall fetch_decode_execute_loop : list byte_code_instruction -> data_stack -> result_of_decoding_and_execution, + specification_of_fetch_decode_execute_loop fetch_decode_execute_loop -> + forall (bcis : list byte_code_instruction), + (fetch_decode_execute_loop bcis nil = OK nil -> + run (Target_program bcis) = Expressible_msg "no result on the data stack") + /\ + (forall (n : nat), + fetch_decode_execute_loop bcis nil = OK (n :: nil) -> + run (Target_program bcis) = Expressible_nat n) + /\ + (forall (n n' : nat) + (ds'' : data_stack), + fetch_decode_execute_loop bcis nil = OK (n :: n' :: ds'') -> + run (Target_program bcis) = Expressible_msg "too many results on the data stack") + /\ + (forall (s : string), + fetch_decode_execute_loop bcis nil = KO s -> + run (Target_program bcis) = Expressible_msg s). + +Theorem run_satisfies_the_alternative_specification_of_run : + alternative_specification_of_run run. +Proof. + unfold alternative_specification_of_run. + intros fdel' S_fdel' bcis. + split. + { intros H_fdel_nil. + unfold run. + rewrite <- (there_is_at_most_one_fetch_decode_execute_loop + fdel' fetch_decode_execute_loop + S_fdel' fetch_decode_execute_loop_satifies_the_specification + bcis nil + ). + rewrite -> H_fdel_nil. + reflexivity. } + split. + { intros n H_fdel_one. + unfold run. + rewrite <- (there_is_at_most_one_fetch_decode_execute_loop + fdel' fetch_decode_execute_loop + S_fdel' fetch_decode_execute_loop_satifies_the_specification + bcis nil + ). + rewrite -> H_fdel_one. + reflexivity. + } + split. + { intros n n' ds H_fdel_many. + unfold run. + rewrite <- (there_is_at_most_one_fetch_decode_execute_loop + fdel' fetch_decode_execute_loop + S_fdel' fetch_decode_execute_loop_satifies_the_specification + bcis nil + ). + rewrite -> H_fdel_many. + reflexivity. + } + intros s H_fdel_KO. + unfold run. + rewrite <- (there_is_at_most_one_fetch_decode_execute_loop + fdel' fetch_decode_execute_loop + S_fdel' fetch_decode_execute_loop_satifies_the_specification + bcis nil + ). + rewrite -> H_fdel_KO. + reflexivity. +Qed. (* ********** *) +Theorem there_is_at_most_one_run_function_with_this_alternative : + forall run1 run2 : target_program -> expressible_value, + alternative_specification_of_run run1 -> + alternative_specification_of_run run2 -> + forall tp : + + target_program, + run1 tp = run2 tp. +Proof. + intros run1 run2 S_run1 S_run2 [bcis]. + + case (fetch_decode_execute_loop bcis nil) as [ ds | s] eqn:H_fdel. + - case ds as [ | n ds' ] eqn:H_ds. + + destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run1_nil _]. + destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run2_nil _]. + rewrite -> (H_run1_nil H_fdel). + rewrite -> (H_run2_nil H_fdel). + reflexivity. + + case ds' as [ | n' ds'' ] eqn:H_ds'. + * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run1_one _]]. + destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run2_one _]]. + rewrite -> (H_run1_one n H_fdel). + rewrite -> (H_run2_one n H_fdel). + reflexivity. + * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run1_many _]]]. + destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run2_many _]]]. + rewrite -> (H_run1_many n n' ds'' H_fdel). + rewrite -> (H_run2_many n n' ds'' H_fdel). + reflexivity. + - destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run1_KO]]]. + destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run2_KO]]]. + rewrite -> (H_run1_KO s H_fdel). + rewrite -> (H_run2_KO s H_fdel). + reflexivity. +Qed. + +Proposition equivalence_of_the_two_specifications : + forall run : target_program -> expressible_value, + specification_of_run run <-> alternative_specification_of_run run. +Proof. + intro run'. + unfold specification_of_run. + unfold alternative_specification_of_run. + split. + - intro S_run. + assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification). + destruct S_run as [S_run_nil [S_run_one [S_run_many S_run_KO]]]. + intros fdel S_fdel bcis. + rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis). + split. + { intros H_fdel_nil. + rewrite -> (S_run_nil bcis H_fdel_nil). + reflexivity. } + split. + { intros n H_fdel_one. + rewrite -> (S_run_one bcis n H_fdel_one). + reflexivity. } + split. + { intros n n' H_fdel_many. + rewrite -> (S_run_many bcis n n' H_fdel_many). + reflexivity. } + split. + (* end of term-project.v *)