diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 16:08:09 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 18:33:53 +0100 |
| commit | ed97c6d4edeac9cab96be17b74ef02373ed36888 (patch) | |
| tree | eae4e8641e972428e7e2520d5d0342e6fdbbc5b8 /src/hls/HTLgenproof.v | |
| parent | 2c5f867a347637cf1b651da7d041d9670493f540 (diff) | |
| download | vericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.tar.gz vericert-ed97c6d4edeac9cab96be17b74ef02373ed36888.zip | |
Tie all modules' clock to main
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 2b9fb0a..8c2d4af 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -136,7 +136,7 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := Hint Constructors match_states : htlproof. 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 /\ + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp /\ main_is_internal p = true. Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): @@ -158,7 +158,7 @@ Proof. 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. + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp. Lemma match_prog_matches : forall p tp, match_prog p tp -> match_prog' p tp. @@ -355,10 +355,11 @@ Section CORRECTNESS. Variable prog : RTL.program. Variable tprog : HTL.program. + Hypothesis TRANSL : match_prog prog tprog. Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog. Proof. intros; apply match_prog_matches; assumption. Qed. Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. @@ -372,7 +373,7 @@ Section CORRECTNESS. forall (b: Values.block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -382,7 +383,7 @@ Section CORRECTNESS. forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef (AST.prog_main prog) f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -2759,7 +2760,7 @@ Section CORRECTNESS. apply H6. constructor. - apply transl_module_correct. + apply transl_module_correct with (AST.prog_main prog). assert (Some (AST.Internal x) = Some (AST.Internal m)). replace (AST.fundef HTL.module) with (HTL.fundef). rewrite <- H6. setoid_rewrite <- A. trivial. |