diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-01 09:12:43 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-01 09:12:43 +0000 |
| commit | 352c05e9350f84dc8fe3ba5d10b7b76c184e5f84 (patch) | |
| tree | 01da4a92cc07d759d069f070ee99753dfd2891dd /src/hls/RTLPargenproof.v | |
| parent | 04db0fb8a8a891200fd4767d780efc5a897f72a0 (diff) | |
| download | vericert-352c05e9350f84dc8fe3ba5d10b7b76c184e5f84.tar.gz vericert-352c05e9350f84dc8fe3ba5d10b7b76c184e5f84.zip | |
Add work on RTLPargenproof.v
Diffstat (limited to 'src/hls/RTLPargenproof.v')
| -rw-r--r-- | src/hls/RTLPargenproof.v | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index bb1cf97..fc3272a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(*Require Import compcert.backend.Registers. +Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -36,20 +36,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: - forall f tf res sp pc rs rs', + forall f tf res sp pc rs rs' ps ps', transl_function f = OK tf -> (forall x, rs !! x = rs' !! x) -> - match_stackframes (Stackframe res f sp pc rs) - (Stackframe res tf sp pc rs'). + (forall x, ps !! x = ps' !! x) -> + match_stackframes (Stackframe res f sp pc rs ps) + (Stackframe res tf sp pc rs' ps). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m sf' tf + forall sf f sp pc rs rs' m sf' tf ps ps' (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: forall x, rs !! x = rs' !! x), - match_states (State sf f sp pc rs m) - (State sf' tf sp pc rs' m) + (REG: forall x, rs !! x = rs' !! x) + (REG: forall x, ps !! x = ps' !! x), + match_states (State sf f sp pc rs ps m) + (State sf' tf sp pc rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), @@ -284,7 +286,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl; + (*induction 1; repeat semantics_simpl; try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). eapply eval_builtin_args_eq. eapply REG. @@ -301,7 +303,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. constructor; eauto. } - Qed. + Qed.*) Admitted. Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, @@ -377,4 +379,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. -*) |