yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity
d2e87aec97
nus/cs3234/labs/term-project.v
Yadunand Prem d2e87aec97
maybe good?
2024-04-28 15:58:30 +08:00

868 lines
26 KiB
Coq
Raw Blame History

(* term-project.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* 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 <? 2).
Check Nat.ltb.
Check (Nat.ltb 1 2).
(* caution: only use natural numbers up to 5000 -- caveat emptor *)
Definition string_of_nat (q0 : nat) : string :=
let s0 := String (ascii_of_nat (48 + (q0 mod 10))) EmptyString
in if q0 <? 10
then s0
else let q1 := q0 / 10
in let s1 := String (ascii_of_nat (48 + (q1 mod 10))) s0
in if q1 <? 10
then s1
else let q2 := q1 / 10
in let s2 := String (ascii_of_nat (48 + (q2 mod 10))) s1
in if q2 <? 10
then s2
else let q3 := q2 / 10
in let s2 := String (ascii_of_nat (48 + (q3 mod 10))) s2
in if q3 <? 10
then s2
else "00000".
Compute (string_of_nat 100).
(* ********** *)
Lemma fold_unfold_list_append_nil :
forall (V : Type)
(v2s : list V),
nil ++ v2s = v2s.
Proof.
fold_unfold_tactic List.app.
Qed.
Lemma fold_unfold_list_append_cons :
forall (V : Type)
(v1 : V)
(v1s' v2s : list V),
(v1 :: v1s') ++ v2s = v1 :: v1s' ++ v2s.
Proof.
fold_unfold_tactic List.app.
Qed.
(* ********** *)
(* Arithmetic expressions: *)
Inductive arithmetic_expression : Type :=
Literal : nat -> 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 <? n2 = true ->
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 <? n2 = false ->
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 <? n2) eqn:H_n1_lt_n2.
* rewrite -> (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 <? n2
then Expressible_msg (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))
else Expressible_nat (n1 - n2)
end
end
end.
Lemma fold_unfold_evaluate_Literal :
forall (n : nat),
evaluate (Literal n) = Expressible_nat n.
Proof.
intros.
fold_unfold_tactic evaluate.
Qed.
Lemma fold_unfold_evaluate_Plus :
forall (ae1 ae2 : arithmetic_expression),
evaluate (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.
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 <? n2
then Expressible_msg (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))
else Expressible_nat (n1 - n2)
end
end.
Proof.
intros.
fold_unfold_tactic evaluate.
Qed.
Theorem evaluate_satisfies_the_specification_of_evaluate :
specification_of_evaluate evaluate.
Proof.
unfold specification_of_evaluate.
split.
exact fold_unfold_evaluate_Literal.
split.
split.
{ intros ae1 ae2 s1 H_ae1.
rewrite -> 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.
(* 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 *)
(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 *)
(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" *)
(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 *)
(forall (n1 n2 : nat)
(ds : data_stack),
n1 <? n2 = true ->
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,
evaluating
decode_execute SUB ds
should return the same error message as the evaluator *)
(forall (n1 n2 : nat)
(ds : data_stack),
n1 <? n2 = false ->
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 :=
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.
(* ********** *)
(* 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).
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:
(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.
*)
(* ********** *)
(* 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.
*)
Proposition about_fetch_decode_execute_loop :
forall (bci1s bci2s : list byte_code_instruction)
(ds : data_stack),
(forall (ds' : data_stack),
fetch_decode_execute_loop bci1s ds = OK ds' ->
fetch_decode_execute_loop (bci1s ++ bci2s) ds = fetch_decode_execute_loop bci2s (ds'))
/\
(forall (s : string),
fetch_decode_execute_loop bci1s ds = KO s ->
fetch_decode_execute_loop (bci1s ++ bci2s) ds = KO s).
Proof.
intros bci1s bci2s.
induction bci1s as [ | bci bci1s' IHbci1s' ]; intros ds.
- split.
+ intros 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.
+ intros s H_fdel.
rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
discriminate H_fdel.
- split.
+ intros ds' H_fdel.
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.
* destruct (IHbci1s' ds1) as [IH_ok _].
exact (IH_ok ds' H_fdel).
* discriminate H_fdel.
+ intros s H_fdel.
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 | s1 ] eqn:H_decode_execute.
* destruct (IHbci1s' ds1) as [_ IH_ko].
exact (IH_ko s H_fdel).
* exact H_fdel.
Qed.
(* ********** *)
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).
Theorem there_is_at_most_one_run_function :
forall (f g : target_program -> expressible_value),
specification_of_run f ->
specification_of_run g ->
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 _].
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).
(* 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 *)
Reference in New Issue View Git Blame Copy Permalink