diff options
| -rw-r--r-- | src/translation/HTLgenproof.v | 58 |
1 files changed, 53 insertions, 5 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 898fafd..7a4ec34 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -16,14 +16,62 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Import HTLgenspec. +From coqup Require Import HTLgenspec Value AssocMap. From coqup Require HTL Verilog. -From compcert Require RTL. +From compcert Require RTL Registers Globalenvs AST. -Parameter match_assocset : RTL.regset -> Verilog.assocset -> Prop. +Import AssocMapNotation. + +Inductive match_assocmaps : RTL.regset -> assocmap -> Prop := +| match_assocmap : forall r rs am, + val_value_lessdef (Registers.Regmap.get r rs) am#r -> + match_assocmaps rs am. Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st, - match_assocset rs assoc -> + match_assocmaps rs assoc -> + tr_module f m -> match_states (RTL.State sf f sp st rs mem) - (HTL.State m st assoc). + (HTL.State m st assoc) +| match_returnstate : forall v v' stack m, + val_value_lessdef v v' -> + match_states (RTL.Returnstate stack v m) (HTL.Returnstate v'). + +Inductive match_program : RTL.program -> HTL.module -> Prop := + match_program_intro : + forall ge p b m f, + ge = Globalenvs.Genv.globalenv p -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) -> + tr_module f m -> + match_program p m. + +Section CORRECTNESS. + + Variable prog : RTL.program. + Variable tprog : HTL.module. + + Hypothesis TRANSL : match_program prog tprog. + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : HTL.genv := HTL.genv_empty. + + (** The proof of semantic preservation for the translation of instructions + is a simulation argument based on diagrams of the following form: +<< + I /\ P + code st rs ---------------- State m st assoc + || | + || | + || | + \/ v + code st rs' --------------- State m st assoc' + I /\ Q +>> + where [tr_code c data control fin rtrn st] is assumed to hold. + *) + + Definition transl_code_prop : Prop := + HTL.step tge (HTL.State) + +End CORRECTNESS. |