diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 00:55:52 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 00:55:52 +0100 |
| commit | aea11ef02422b8302779676a31adcf6dafbff0dd (patch) | |
| tree | ac2c14ac90d85447548477d5bb435b2da0c03717 /src | |
| parent | bfb722caf2d46867779222b45615481e9020f0aa (diff) | |
| download | vericert-kvx-aea11ef02422b8302779676a31adcf6dafbff0dd.tar.gz vericert-kvx-aea11ef02422b8302779676a31adcf6dafbff0dd.zip | |
Proof of TransfHTLLink DONE
Diffstat (limited to 'src')
| -rw-r--r-- | src/translation/HTLgenproof.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2e91b99..12a1a70 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -127,7 +127,20 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) := Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2). Proof. - Admitted. + red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + apply link_prog_inv in H. + + unfold match_prog in *. + unfold main_is_internal in *. simplify. repeat (unfold_match H4). + repeat (unfold_match H3). simplify. + subst. rewrite H0 in *. specialize (H (AST.prog_main p2)). + exploit H. + apply Genv.find_def_symbol. exists b. split. + assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + apply Genv.find_def_symbol. exists b0. split. + assumption. Search Genv.find_def. apply Genv.find_funct_ptr_iff. eassumption. + intros. inv H3. inv H5. destruct H6. inv H5. +Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. |