(* term-project.v *) (* LPP 2025 - CS3234 2024-2025, Sem2 *) (* Olivier Danvy *) (* Version of 14 Apr 2025 with more precise types *) (* was: *) (* Version of 11 Apr 2025 *) (* ********** *) (* Three program 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. (* ***** *) (* Practical reminders: *) 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. (* ********** *) (* A semantics for arithmetic expressions: *) Inductive source_msg : Type := Source_msg_numerical_underflow : nat -> source_msg. Inductive source_expressible_value : Type := Source_expressible_nat : nat -> source_expressible_value | Source_expressible_msg : source_msg -> source_expressible_value. (* ********** *) (* An evaluation function for arithmetic expressions: *) Definition specification_of_evaluate (evaluate : arithmetic_expression -> source_expressible_value) := (forall n : nat, evaluate (Literal n) = Source_expressible_nat n) /\ ((forall (ae1 ae2 : arithmetic_expression) (n1 n2 : nat), evaluate ae1 = Source_expressible_nat n1 -> evaluate ae2 = Source_expressible_nat n2 -> evaluate (Plus ae1 ae2) = Source_expressible_nat (n1 + n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (n1 : nat) (sm2 : source_msg), evaluate ae1 = Source_expressible_nat n1 -> evaluate ae2 = Source_expressible_msg sm2 -> evaluate (Plus ae1 ae2) = Source_expressible_msg sm2) /\ (forall (ae1 ae2 : arithmetic_expression) (sm1 : source_msg), evaluate ae1 = Source_expressible_msg sm1 -> evaluate (Plus ae1 ae2) = Source_expressible_msg sm1)) /\ ((forall (ae1 ae2 : arithmetic_expression) (n1 n2 : nat), evaluate ae1 = Source_expressible_nat n1 -> evaluate ae2 = Source_expressible_nat n2 -> n1 evaluate (Minus ae1 ae2) = Source_expressible_nat (n1 - n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (n1 n2 : nat), evaluate ae1 = Source_expressible_nat n1 -> evaluate ae2 = Source_expressible_nat n2 -> n1 evaluate (Minus ae1 ae2) = Source_expressible_msg (Source_msg_numerical_underflow (n2 - n1))) /\ (forall (ae1 ae2 : arithmetic_expression) (n1 : nat) (sm2 : source_msg), evaluate ae1 = Source_expressible_nat n1 -> evaluate ae2 = Source_expressible_msg sm2 -> evaluate (Minus ae1 ae2) = Source_expressible_msg sm2) /\ (forall (ae1 ae2 : arithmetic_expression) (sm1 : source_msg), evaluate ae1 = Source_expressible_msg sm1 -> evaluate (Minus ae1 ae2) = Source_expressible_msg sm1)). (* ***** *) (* Task 1: The evaluation function *) (* * Determine whether the specified evaluation function operates from left to right or from right to left, and then rename ``specification_of_evaluate`` to - ``specification_of_evaluate_ltr`` ("ltr" for "from left to right") or to - ``specification_of_evaluate_rtl`` ("rtl" for "from right to left"), as appropriate. * Provide an example of an arithmetic expression that gives one result when evaluated from left to right and another when evaluated from right to left. * Prove that the renamed specification is not ambiguous. * Implement a unit-test function -- naming it ``unit_test_for_evaluate_ltr`` or ``unit_test_for_evaluate_rtl``, as appropriate -- that provides code coverage. * Implement a function -- naming it ``evaluate_ltr`` or ``evaluate_rtl``, as appropriate -- that satisfies the renamed specification and verify that it passes the unit tests. * Conclude that the renamed specification is not vacuous. *) Fixpoint evaluate (ae : arithmetic_expression) : source_expressible_value := (* fake, but type-correct implementation *) Source_expressible_msg (Source_msg_numerical_underflow 0). Theorem evaluate_satisfies_the_specification_of_evaluate : specification_of_evaluate evaluate. Proof. Abort. (* ********** *) (* The source language: *) Inductive source_program : Type := Source_program : arithmetic_expression -> source_program. (* An interpreter for the source language: *) Definition specification_of_interpret (interpret : source_program -> source_expressible_value) := forall evaluate : arithmetic_expression -> source_expressible_value, specification_of_evaluate evaluate -> forall ae : arithmetic_expression, interpret (Source_program ae) = evaluate ae. (* ***** *) (* Task 2: The source interpreter *) (* * For naming consistency, rename ``specification_of_interpret`` to ``specification_of_interpret_ltr`` or ``specification_of_interpret_rtl``, as appropriate, and prove that this renamed specification is not ambiguous. * Implement a unit-test function for ``interpret`` -- naming it ``unit_test_for_interpret_ltr`` or ``unit_test_for_interpret_rtl``, as appropriate -- that calls either of ``unit_test_for_evaluate_ltr`` or ``unit_test_for_evaluate_rtl``, as appropriate -- reflecting the fact that ``interpret`` calls ``evaluate``. * Implement a function -- naming it ``interpret_ltr`` or ``interpret_rtl``, as appropriate -- that satisfies the renamed specification. * Conclude that the renamed specification is not vacuous. *) Definition interpret (sp : source_program) : source_expressible_value := (* fake, but type-correct implementation *) Source_expressible_msg (Source_msg_numerical_underflow 0). Theorem interpret_satisfies_the_specification_of_interpret : specification_of_interpret interpret. Proof. Abort. (* ********** *) (* Byte-code instructions: *) Inductive byte_code_instruction : Type := PUSH : nat -> byte_code_instruction | ADD : byte_code_instruction | SUB : byte_code_instruction. (* Data stack: *) Definition data_stack := list nat. (* A semantics for byte-code instructions: *) Inductive result_msg : Type := Result_msg_numerical_underflow : nat -> result_msg | Result_msg_stack_underflow : byte_code_instruction -> result_msg. Inductive result_of_decoding_and_execution : Type := OK : data_stack -> result_of_decoding_and_execution | KO : result_msg -> 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 result message "Result_msg_stack_underflow ADD" * 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 result message "Result_msg_stack_underflow SUB" 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 result message "Result_msg_numerical_underflow n", where n is the same number as in the corresponding source message in the evaluator *) (* Task 3: The decode-execute function *) Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : result_of_decoding_and_execution := (* fake, but type-correct implementation *) KO (Result_msg_numerical_underflow 0). (* ********** *) (* 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) (rm : result_msg), decode_execute bci ds = KO rm -> fetch_decode_execute_loop (bci :: bcis') ds = KO rm). (* Task 3: The virtual machine *) (* * For naming consistency, rename ``specification_of_fetch_decode_execute_loop`` to ``specification_of_fetch_decode_execute_loop_ltr`` or ``specification_of_fetch_decode_execute_loop_rtl``, as appropriate, and prove that this renamed specification is not ambiguous. * Implement a unit-test function for ``fetch_decode_execute_loop`` -- naming it ``unit_test_for_fetch_decode_execute_loop_ltr`` or ``unit_test_for_fetch_decode_execute_loop_rtl``, as appropriate -- that provides code coverage. * Implement a function -- naming it ``fetch_decode_execute_loop_ltr`` or ``fetch_decode_execute_loop_rtl``, as appropriate -- that satisfies the renamed specification and verify that it passes the unit tests. * Conclude that the renamed specification is not vacuous. *) Definition fetch_decode_execute_loop (bcis : list byte_code_instruction) (ds : data_stack) : result_of_decoding_and_execution := (* fake, but type-correct implementation *) KO (Result_msg_numerical_underflow 0). (* ********** *) (* Task 4: A Eureka lemma *) (* 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. *) (* ********** *) (* The target language: *) Inductive target_program : Type := Target_program : list byte_code_instruction -> target_program. (* A semantics for the target language: *) Inductive target_msg : Type := Target_msg_numerical_underflow : nat -> target_msg | Target_msg_stack_underflow : byte_code_instruction -> target_msg | Target_msg_stack_O : target_msg | Target_msg_stack_SS : target_msg. Inductive target_expressible_value : Type := Target_expressible_nat : nat -> target_expressible_value | Target_expressible_msg : target_msg -> target_expressible_value. (* ***** *) (* An interpreter for the target language: *) Definition specification_of_run (run : target_program -> target_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) = Target_expressible_msg Target_msg_stack_O) /\ (forall (bcis : list byte_code_instruction) (n : nat), fetch_decode_execute_loop bcis nil = OK (n :: nil) -> run (Target_program bcis) = Target_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) = Target_expressible_msg Target_msg_stack_SS) /\ (forall (bcis : list byte_code_instruction) (n : nat), fetch_decode_execute_loop bcis nil = KO (Result_msg_numerical_underflow n) -> run (Target_program bcis) = Target_expressible_msg (Target_msg_numerical_underflow n)) /\ (forall (bcis : list byte_code_instruction) (bci : byte_code_instruction), fetch_decode_execute_loop bcis nil = KO (Result_msg_stack_underflow bci) -> run (Target_program bcis) = Target_expressible_msg (Target_msg_stack_underflow bci)). (* Task 5: The target interpreter *) (* * For naming consistency, rename ``specification_of_run`` to ``specification_of_run_ltr`` or ``specification_of_tun_rtl``, as appropriate, and prove that this renamed specification is not ambiguous. * Implement a unit-test function for ``run`` -- naming it ``unit_test_for_run_ltr`` or ``unit_test_for_run_rtl``, as appropriate -- that calls either of ``unit_test_for_fetch_decode_execute_loop_ltr`` or ``unit_test_for_fetch_decode_execute_loop_rtl``, as appropriate, reflecting the fact that ``run`` calls ``fetch_decode_execute_loop``. (If that proves too complicated, just implement a stand-alone unit-test function.) * Implement a function -- naming it ``run_ltr`` or ``run_rtl``, as appropriate -- that satisfies the renamed specification. * Conclude that the renamed specification is not vacuous. *) Definition run (tp : target_program) : target_expressible_value := (* fake, but type-correct implementation *) Target_expressible_msg (Target_msg_numerical_underflow 0). Theorem run_satisfies_the_specification_of_run : specification_of_run run. Proof. Abort. (* ********** *) (* A translator from arithmetic expressions to byte-code instructions: *) Definition specification_of_translate (translate : arithmetic_expression -> list byte_code_instruction) := (forall n : nat, translate (Literal n) = PUSH n :: nil) /\ (forall ae1 ae2 : arithmetic_expression, translate (Plus ae1 ae2) = (translate ae1) ++ (translate ae2) ++ (ADD :: nil)) /\ (forall ae1 ae2 : arithmetic_expression, translate (Minus ae1 ae2) = (translate ae1) ++ (translate ae2) ++ (SUB :: nil)). (* Task 6: The translator from arithmetic expressions to byte-code instructions *) (* * For naming consistency, rename ``specification_of_translate`` to ``specification_of_translate_ltr`` or to ``specification_of_translate_rtl``, as appropriate. * Prove that the renamed specification is not ambiguous. * Implement a unit-test function -- naming it ``unit_test_for_translate_ltr`` or ``unit_test_for_translate_ltr``, as appropriate -- that provides code coverage. * Implement a function -- naming it ``translate_ltr`` or ``translate_rtl``, as appropriate -- that satisfies the renamed specification and verify that it passes the unit tests. * Conclude that the renamed specification is not vacuous. *) Definition translate (ae : arithmetic_expression) : list byte_code_instruction := (* fake, but type-correct implementation *) nil. (* ********** *) (* A compiler for source programs *) Definition specification_of_compile (compile : source_program -> target_program) := forall translate : arithmetic_expression -> list byte_code_instruction, specification_of_translate translate -> forall ae : arithmetic_expression, compile (Source_program ae) = Target_program (translate ae). (* Task 7: The compiler *) (* * For naming consistency, rename ``specification_of_compile`` to ``specification_of_compile_ltr`` or ``specification_of_compile_rtl``, as appropriate, and prove that this renamed specification is not ambiguous. * Implement a unit-test function for ``compile`` -- naming it ``unit_test_for_compile_ltr`` or ``unit_test_for_compile_rtl``, as appropriate -- that calls either of ``unit_test_for_translate_ltr`` or ``unit_test_for_compile_rtl_aux``, as appropriate -- reflecting the fact that ``compile`` calls ``translate``. * Implement a function -- naming it ``compile_ltr`` or ``compile_rtl``, as appropriate -- that satisfies the renamed specification. * Conclude that the renamed specification is not vacuous. *) Definition compile (sp : source_program) : target_program := (* fake, but type-correct implementation *) Target_program nil. Theorem compile_satisfies_the_specification_of_compile : specification_of_compile compile. Proof. Abort. (* ********** *) (* Task 8: An alternative compiler *) (* 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? *) Definition translate_acc (ae : arithmetic_expression) (a : list byte_code_instruction) : list byte_code_instruction := (* fake, but type-correct implementation *) a. Definition compile_alt (sp : source_program) : target_program := (* fake, but type-correct implementation *) Target_program nil. (* ********** *) (* Task 9: The capstone *) Theorem the_commuting_diagram_logically : (* forall interpret : source_program -> source_expressible_value, specification_of_interpret interpret -> forall compile : source_program -> target_program, specification_of_compile compile -> forall run : target_program -> target_expressible_value, specification_of_run run -> *) forall sp : source_program, (forall n : nat, interpret sp = Source_expressible_nat n -> run (compile sp) = Target_expressible_nat n) /\ (forall n : nat, interpret sp = Source_expressible_msg (Source_msg_numerical_underflow n) -> run (compile sp) = Target_expressible_msg (Target_msg_numerical_underflow n)). Proof. Abort. (* ***** *) Definition target_expressible_value_from_source_expressible_value (sev : source_expressible_value) : target_expressible_value := match sev with Source_expressible_nat n => Target_expressible_nat n | Source_expressible_msg sm => Target_expressible_msg (match sm with Source_msg_numerical_underflow n => Target_msg_numerical_underflow n end) end. Theorem the_commuting_diagram_equationally : (* forall interpret : source_program -> source_expressible_value, specification_of_interpret interpret -> forall compile : source_program -> target_program, specification_of_compile compile -> forall run : target_program -> target_expressible_value, specification_of_run run -> *) forall sp : source_program, target_expressible_value_from_source_expressible_value (interpret sp) = run (compile sp). Proof. Abort. (* ********** *) (* Byte-code verification *) (* The following verifier symbolically executes a byte-code program to check whether an 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 (tp : target_program) : bool := let '(Target_program bcis) := tp in match verify_aux bcis 0 with Some n => match n with 1 => true | _ => false end | _ => false end. (* Task 10: The byte-code verifier *) (* Prove that the compiler emits code that is accepted by the verifier. *) Theorem the_compiler_emits_well_behaved_code : forall sp : source_program, verify (compile sp) = true. Proof. Abort. (* Subsidiary question: What is the practical consequence of this theorem? *) (* ********** *) (* end of term-project.v *)