diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-02 19:06:27 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-02 19:06:27 +0100 |
| commit | e9076031a8f759b10606e8507490ed8c68b16a43 (patch) | |
| tree | b162c15a3687719fd2f82802ab4180de9959bbe4 | |
| parent | 2b0c8766b4e99772777763e96e13747454672814 (diff) | |
| download | vericert-kvx-e9076031a8f759b10606e8507490ed8c68b16a43.tar.gz vericert-kvx-e9076031a8f759b10606e8507490ed8c68b16a43.zip | |
Add proof to final_states
| -rw-r--r-- | src/translation/HTLgenproof.v | 4 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 4 |
2 files changed, 5 insertions, 3 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 3dd645e..a8177cf 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -476,7 +476,9 @@ Section CORRECTNESS. (r : Integers.Int.int), match_states s1 s2 -> Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. - Proof. Admitted. + Proof. + intros. inv H0. inv H. inv H4. constructor. trivial. + Qed. Hint Resolve transl_final_states : htlproof. Theorem transf_program_correct: diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index fffbb81..bf38b29 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -19,7 +19,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. -From compcert Require Events Globalenvs Smallstep Integers. +From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. Import HexNotationValue. @@ -98,7 +98,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, - value_int_eqb retval retvali = true -> + retvali = valueToInt retval -> final_state (Returnstate retval) retvali. Definition semantics (m : program) := |