From 6ab78d3c9db7e2d6acea33572a9e1faa598c43b8 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Sep 2019 17:58:34 +0200 Subject: Start of match_states --- backend/Duplicateproof.v | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 5cf6b368..a727155e 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -1,7 +1,7 @@ (** Correctness proof for code duplication *) -Require Import AST Linking Errors. -Require Import RTL Globalenvs Smallstep. -Require Import Duplicate. +Require Import AST Linking Errors Globalenvs Smallstep. +Require Import Coqlib. +Require Import RTL Duplicate. Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -20,6 +20,26 @@ Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Inductive match_nodes: node -> node -> Prop := + | match_node_intro: forall n, match_nodes n n + (* TODO - fill out the rest *) +. + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro: + forall res f sp pc rs f' pc' + (TRANSF: transf_function f = OK f') + (DUPLIC: match_nodes pc pc'), + match_stackframes (Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall st f sp pc rs m st' f' pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: transf_function f = OK f') + (DUPLIC: match_nodes pc pc'), + match_states (State st f sp pc rs m) (State st' f' sp pc' rs m). + Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. -- cgit