diff --git a/cs3234/labs/term-project.v b/cs3234/labs/term-project.v new file mode 100644 index 0000000..79d2b11 --- /dev/null +++ b/cs3234/labs/term-project.v @@ -0,0 +1,658 @@ +(* term-project.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 12 Apr 2024 *) + +(* ********** *) + +(* Three language processors for arithmetic expressions. *) + +(* + group name: + + student name: + e-mail address: + student ID number: + + student name: + e-mail address: + student ID number: + + student name: + e-mail address: + student ID number: + + student name: + e-mail address: + student ID number: + + student name: + e-mail address: + student ID number: +*) + +(* ********** *) + +Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity. + +Require Import Arith Bool List String Ascii. + +(* ***** *) + +Check (1 =? 2). +Check Nat.eqb. +Check (Nat.eqb 1 2). + +Check (1 <=? 2). +Check Nat.leb. +Check (Nat.leb 1 2). + +Check (1 arithmetic_expression +| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression +| Minus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression. + +(* Source programs: *) + +Inductive source_program : Type := + Source_program : arithmetic_expression -> source_program. + +(* ********** *) + +(* Semantics: *) + +Inductive expressible_value : Type := + Expressible_nat : nat -> expressible_value +| Expressible_msg : string -> expressible_value. + +(* ********** *) + +(* With the assistance of Ravern *) +Definition specification_of_evaluate (evaluate : arithmetic_expression -> expressible_value) := + (forall n : nat, + evaluate (Literal n) = Expressible_nat n) + /\ + ((forall (ae1 ae2 : arithmetic_expression) + (s1 : string), + evaluate ae1 = Expressible_msg s1 -> + evaluate (Plus ae1 ae2) = Expressible_msg s1) + /\ + (forall (ae1 ae2 : arithmetic_expression) + (n1 : nat) + (s2 : string), + evaluate ae1 = Expressible_nat n1 -> + evaluate ae2 = Expressible_msg s2 -> + evaluate (Plus ae1 ae2) = Expressible_msg s2) + /\ + (forall (ae1 ae2 : arithmetic_expression) + (n1 n2 : nat), + evaluate ae1 = Expressible_nat n1 -> + evaluate ae2 = Expressible_nat n2 -> + evaluate (Plus ae1 ae2) = Expressible_nat (n1 + n2))) + /\ + ((forall (ae1 ae2 : arithmetic_expression) + (s1 : string), + evaluate ae1 = Expressible_msg s1 -> + evaluate (Minus ae1 ae2) = Expressible_msg s1) + /\ + (forall (ae1 ae2 : arithmetic_expression) + (n1 : nat) + (s2 : string), + evaluate ae1 = Expressible_nat n1 -> + evaluate ae2 = Expressible_msg s2 -> + evaluate (Minus ae1 ae2) = Expressible_msg s2) + /\ + (forall (ae1 ae2 : arithmetic_expression) + (n1 n2 : nat), + evaluate ae1 = Expressible_nat n1 -> + evaluate ae2 = Expressible_nat n2 -> + n1 + evaluate (Minus ae1 ae2) = Expressible_msg (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))) + /\ + (forall (ae1 ae2 : arithmetic_expression) + (n1 n2 : nat), + evaluate ae1 = Expressible_nat n1 -> + evaluate ae2 = Expressible_nat n2 -> + n1 + evaluate (Minus ae1 ae2) = Expressible_nat (n1 - n2))). + +Theorem there_is_at_most_one_evaluate_function : + forall f g : arithmetic_expression -> expressible_value, + specification_of_evaluate f -> + specification_of_evaluate g -> + forall ae : arithmetic_expression, + f ae = g ae. +Proof. + intros f g. + unfold specification_of_evaluate. + intros [S_f_Literal + [[S_f_Plus_msg [S_f_Plus_msg2 S_f_Plus_nat]] + [S_f_Minus_msg [S_f_Minus_msg2 [S_f_Minus_nat_lt S_f_Minus_nat_gte]]]]]. + intros [S_g_Literal + [[S_g_Plus_msg [S_g_Plus_msg2 S_g_Plus_nat]] + [S_g_Minus_msg [S_g_Minus_msg2 [S_g_Minus_nat_lt S_g_Minus_nat_gte]]]]]. + intros ae. + induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2 ]. + - rewrite -> S_g_Literal. + exact (S_f_Literal n). + - Check (f (Plus ae1 ae2) ). + case (f ae1) as [n1 | s1] eqn:H_f_ae1. + case (f ae2) as [n2 | s2] eqn:H_f_ae2. + + rewrite -> (S_f_Plus_nat ae1 ae2 n1 n2 H_f_ae1 H_f_ae2). + rewrite -> (S_g_Plus_nat ae1 ae2 n1 n2 (eq_sym IHae1) (eq_sym IHae2)). + reflexivity. + + rewrite -> (S_f_Plus_msg2 ae1 ae2 n1 s2 H_f_ae1 H_f_ae2). + rewrite -> (S_g_Plus_msg2 ae1 ae2 n1 s2 (eq_sym IHae1) (eq_sym IHae2)). + reflexivity. + + rewrite -> (S_f_Plus_msg ae1 ae2 s1 H_f_ae1). + rewrite -> (S_g_Plus_msg ae1 ae2 s1 (eq_sym IHae1)). + reflexivity. + - case (f ae1) as [n1 | s1] eqn:H_f_ae1. + case (f ae2) as [n2 | s2] eqn:H_f_ae2. + + case (n1 (S_f_Minus_nat_lt ae1 ae2 n1 n2 H_f_ae1 H_f_ae2 H_n1_lt_n2). + rewrite -> (S_g_Minus_nat_lt ae1 ae2 n1 n2 (eq_sym IHae1) (eq_sym IHae2) H_n1_lt_n2). + reflexivity. + * rewrite -> (S_f_Minus_nat_gte ae1 ae2 n1 n2 H_f_ae1 H_f_ae2 H_n1_lt_n2). + rewrite -> (S_g_Minus_nat_gte ae1 ae2 n1 n2 (eq_sym IHae1) (eq_sym IHae2) H_n1_lt_n2). + reflexivity. + + rewrite -> (S_f_Minus_msg2 ae1 ae2 n1 s2 H_f_ae1 H_f_ae2). + rewrite -> (S_g_Minus_msg2 ae1 ae2 n1 s2 (eq_sym IHae1) (eq_sym IHae2)). + reflexivity. + + rewrite -> (S_f_Minus_msg ae1 ae2 s1 H_f_ae1). + rewrite -> (S_g_Minus_msg ae1 ae2 s1 (eq_sym IHae1)). + reflexivity. +Qed. + +Check arithmetic_expression_ind. + +Lemma nat_ind2 : + forall P : nat -> Prop, + P 0 -> + P 1 -> + (forall k : nat, P k -> P (S k) -> P (S (S k))) -> + forall n : nat, P n. +Proof. + intros P H_P0 H_P1 H_PSS [ | [ | n'' ] ]. + - exact H_P0. + - exact H_P1. + - assert (both : forall m : nat, P m /\ P(S m)). + { intro m. + induction m as [ | m' [ IHm' IHSm' ] ]. + - exact (conj H_P0 H_P1). + - split. + + exact IHSm'. + + exact (H_PSS m' IHm' IHSm' ). + } + destruct (both n'') as [Pn'' PSn'']. + exact (H_PSS n'' Pn'' PSn''). +Qed. + +Fixpoint evaluate (ae : arithmetic_expression) : expressible_value := + match ae with + | Literal n => Expressible_nat n + | Plus ae1 ae2 => + match evaluate ae1 with + | Expressible_msg s1 => Expressible_msg s1 + | Expressible_nat n1 => + match evaluate ae2 with + | Expressible_msg s2 => Expressible_msg s2 + | Expressible_nat n2 => Expressible_nat (n1 + n2) + end + end + | Minus ae1 ae2 => + match evaluate ae1 with + | Expressible_msg s1 => Expressible_msg s1 + | Expressible_nat n1 => + match evaluate ae2 with + | Expressible_msg s2 => Expressible_msg s2 + | Expressible_nat n2 => + if n1 Expressible_msg s1 + | Expressible_nat n1 => + match (evaluate ae2) with + | Expressible_msg s2 => Expressible_msg s2 + | Expressible_nat n2 => Expressible_nat (n1 + n2) + end + end. + +Proof. + intros. + fold_unfold_tactic evaluate. +Qed. + +Lemma fold_unfold_evaluate_Minus : + forall (ae1 ae2 : arithmetic_expression), + evaluate (Minus ae1 ae2) = + match (evaluate ae1) with + | Expressible_msg s1 => Expressible_msg s1 + | Expressible_nat n1 => + match (evaluate ae2) with + | Expressible_msg s2 => Expressible_msg s2 + | Expressible_nat n2 => + if n1 fold_unfold_evaluate_Plus. + rewrite -> H_ae1. + reflexivity. } + split. + { intros ae1 ae2 n1 s2 H_ae1 H_ae2. + rewrite -> fold_unfold_evaluate_Plus. + rewrite -> H_ae1. + rewrite -> H_ae2. + reflexivity. } + { intros ae1 ae2 n1 n2 H_ae1 H_ae2. + rewrite -> fold_unfold_evaluate_Plus. + rewrite -> H_ae1. + rewrite -> H_ae2. + reflexivity. } + split. + { intros ae1 ae2 s1 H_ae1. + rewrite -> fold_unfold_evaluate_Minus. + rewrite -> H_ae1. + reflexivity. } + split. + { intros ae1 ae2 n1 s2 H_ae1 H_ae2. + rewrite -> fold_unfold_evaluate_Minus. + rewrite -> H_ae1. + rewrite -> H_ae2. + reflexivity. } + split. + { intros ae1 ae2 n1 n2 H_ae1 H_ae2 H_n1_le_n2. + rewrite -> fold_unfold_evaluate_Minus. + rewrite -> H_ae1. + rewrite -> H_ae2. + rewrite -> H_n1_le_n2. + reflexivity. } + intros ae1 ae2 n1 n2 H_ae1 H_ae2 H_n1_le_n2. + rewrite -> fold_unfold_evaluate_Minus. + rewrite -> H_ae1. + rewrite -> H_ae2. + rewrite -> H_n1_le_n2. + reflexivity. +Qed. + +Definition specification_of_interpret (interpret : source_program -> expressible_value) := + forall evaluate : arithmetic_expression -> expressible_value, + specification_of_evaluate evaluate -> + forall ae : arithmetic_expression, + interpret (Source_program ae) = evaluate ae. + +Definition there_is_at_most_one_interpret : + forall (f g : source_program -> expressible_value), + (specification_of_interpret f) -> + (specification_of_interpret g) -> + forall (ae : arithmetic_expression), + f (Source_program ae) = g (Source_program ae). +Proof. + intros f g. + unfold specification_of_interpret. + intros S_f S_g. + intros ae. + rewrite -> (S_g evaluate evaluate_satisfies_the_specification_of_evaluate ae). + exact (S_f evaluate evaluate_satisfies_the_specification_of_evaluate ae). +Qed. + +(* Task 1: + a. time permitting, prove that each of the definitions above specifies at most one function; + b. implement these two functions; and + c. verify that each of your functions satisfies its specification. +*) + + +Definition interpret (sp : source_program) : expressible_value := + match sp with + | Source_program ae => evaluate ae + end. + +Theorem interpret_satisfies_the_specification_of_interpret : + specification_of_interpret interpret. +Proof. + unfold specification_of_interpret. + intros eval S_evaluate ae. + unfold interpret. + exact (there_is_at_most_one_evaluate_function + evaluate eval + evaluate_satisfies_the_specification_of_evaluate S_evaluate ae). +Qed. + +(* ********** *) + +(* Byte-code instructions: *) + +Inductive byte_code_instruction : Type := + PUSH : nat -> byte_code_instruction +| ADD : byte_code_instruction +| SUB : byte_code_instruction. + +(* Target programs: *) + +Inductive target_program : Type := + Target_program : list byte_code_instruction -> target_program. + +(* Data stack: *) + +Definition data_stack := list nat. + +(* ********** *) + +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, + 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, + 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, + evaluating + decode_execute ADD ds + should return the error message "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 + and + 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 +*) + +Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : result_of_decoding_and_execution := + KO "to be implemented". + +(* ********** *) + +(* Specification of the virtual machine: *) + +Definition specification_of_fetch_decode_execute_loop (fetch_decode_execute_loop : list byte_code_instruction -> data_stack -> result_of_decoding_and_execution) := + (forall ds : data_stack, + fetch_decode_execute_loop nil ds = OK ds) + /\ + (forall (bci : byte_code_instruction) + (bcis' : list byte_code_instruction) + (ds ds' : data_stack), + decode_execute bci ds = OK ds' -> + fetch_decode_execute_loop (bci :: bcis') ds = + fetch_decode_execute_loop bcis' ds') + /\ + (forall (bci : byte_code_instruction) + (bcis' : list byte_code_instruction) + (ds : data_stack) + (s : string), + decode_execute bci ds = KO s -> + fetch_decode_execute_loop (bci :: bcis') ds = + KO s). + +(* 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. +*) + +(* ********** *) + +(* Food for thought: + For any lists of byte-code instructions bci1s and bci2s, + and for any data stack ds, + characterize the execution of the concatenation of bci1s and bci2s (i.e., bci1s ++ bci2s) with ds + in terms of executing bci1s and of executing bci2s. +*) + +(* ********** *) + +Definition 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 (bcis : list byte_code_instruction) + (n : nat), + fetch_decode_execute_loop bcis nil = OK (n :: nil) -> + run (Target_program bcis) = Expressible_nat n) + /\ + (forall (bcis : list byte_code_instruction) + (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 (bcis : list byte_code_instruction) + (s : string), + fetch_decode_execute_loop bcis nil = KO s -> + run (Target_program bcis) = Expressible_msg s). + +(* Task 4: + 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. +*) + +(* ********** *) + +Definition specification_of_compile_aux (compile_aux : arithmetic_expression -> list byte_code_instruction) := + (forall n : nat, + compile_aux (Literal n) = PUSH n :: nil) + /\ + (forall ae1 ae2 : arithmetic_expression, + compile_aux (Plus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil)) + /\ + (forall ae1 ae2 : arithmetic_expression, + compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)). + +(* 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 + c. verify that your function satisfies the specification. +*) + +Definition specification_of_compile (compile : source_program -> target_program) := + forall compile_aux : arithmetic_expression -> list byte_code_instruction, + specification_of_compile_aux compile_aux -> + forall ae : arithmetic_expression, + compile (Source_program ae) = Target_program (compile_aux ae). + +(* Task 6: + 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. +*) + +(* ********** *) + +(* Task 7: + implement an alternative compiler + using an auxiliary function with an accumulator + and that does not use ++ but :: instead, + and prove that it satisfies the specification. + + Subsidiary question: + Are your compiler and your alternative compiler equivalent? + How can you tell? +*) + +(* ********** *) + +(* Task 8 (the capstone): + Prove that interpreting an arithmetic expression gives the same result + as first compiling it and then executing the compiled program. +*) + +(* ********** *) + +(* Byte-code verification: + the following verifier symbolically executes a byte-code program + to check whether no underflow occurs during execution + and whether when the program completes, + there is one and one only natural number on top of the stack. + The second argument of verify_aux is a natural number + that represents the size of the stack. +*) + +Fixpoint verify_aux (bcis : list byte_code_instruction) (n : nat) : option nat := + match bcis with + | nil => + Some n + | bci :: bcis' => + match bci with + | PUSH _ => + verify_aux bcis' (S n) + | _ => + match n with + | S (S n') => + verify_aux bcis' (S n') + | _ => + None + end + end + end. + +Definition verify (p : target_program) : bool := + match p with + | Target_program bcis => + match verify_aux bcis 0 with + | Some n => + match n with + | 1 => + true + | _ => + false + end + | _ => + false + end + end. + +(* Task 9: + 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. +Proof. +Abort. +*) + +(* Subsidiary question: + What is the practical consequence of this theorem? +*) + +(* ********** *) + +(* end of term-project.v *)