diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-04 19:59:21 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-04 20:05:04 +0100 |
| commit | 4d7236541250808487820beec0b3f79ac2a901dc (patch) | |
| tree | b08c984b02b3b44744885af849d3a81bad479121 /src/hls/HTLgenproof.v | |
| parent | 95ef66d14377cbd88142b5ccb3d598fde6fec243 (diff) | |
| download | vericert-4d7236541250808487820beec0b3f79ac2a901dc.tar.gz vericert-4d7236541250808487820beec0b3f79ac2a901dc.zip | |
Correct lookup for called funcs, simplify tr_module
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index cba21b0..eb7326a 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -179,7 +179,7 @@ Inductive match_states (ge : RTL.genv) : 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 (AST.prog_main p) f = Errors.OK tf) eq p tp /\ + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\ main_is_internal p = true. Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): @@ -201,7 +201,7 @@ Proof. Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main p) f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp. Lemma match_prog_matches : forall p tp, match_prog p tp -> match_prog' p tp. @@ -386,9 +386,8 @@ Ltac not_control_reg := solve [ unfold Ple, Plt in *; try multimatch goal with - | [ H : forall r, - (exists x, _ ! r = Some x) -> (r > _)%positive /\ (_ > r)%positive - |- context[?r'] + | [ H : forall r, (exists x, _ ! r = Some x) -> (_ < r < _)%positive + |- context[?r'] ] => destruct (H r' ltac:(eauto)) end; lia @@ -467,7 +466,7 @@ Section CORRECTNESS. Admitted. Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog. + Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog. Proof. intros; apply match_prog_matches; assumption. Qed. Lemma symbols_preserved: @@ -478,7 +477,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 (AST.prog_main prog) f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -488,7 +487,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 (AST.prog_main prog) f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -3069,7 +3068,7 @@ Section CORRECTNESS. rewrite symbols_preserved; eauto. - eauto. - constructor; auto with htlproof. - apply transl_module_correct with (AST.prog_main prog). + apply transl_module_correct. assert (Some (AST.Internal x) = Some (AST.Internal m)) as Heqm. { rewrite <- H6. setoid_rewrite <- A. trivial. } inv Heqm. |