diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-22 00:42:14 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-22 00:42:14 +0100 |
| commit | 182b29c0db3c408f7bd7360af90e5b360d63222d (patch) | |
| tree | 632308217f2f0ba44a1de44db8caff500f05ac24 /src/hls/HTLgenproof.v | |
| parent | f2fc2ac70aeceec2f3f7137acba5c0bf7a342a17 (diff) | |
| download | vericert-182b29c0db3c408f7bd7360af90e5b360d63222d.tar.gz vericert-182b29c0db3c408f7bd7360af90e5b360d63222d.zip | |
Use new HTLgenspec in proof
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index a042561..c1298c1 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -29,6 +29,7 @@ Require Import compcert.lib.Maps. Require Import vericert.common.IntegerExtra. Require Import vericert.common.Vericertlib. Require Import vericert.common.ZExtra. +Require Import vericert.common.ListExtra. Require Import vericert.hls.Array. Require Import vericert.hls.AssocMap. Require vericert.hls.HTL. @@ -1434,6 +1435,29 @@ Section CORRECTNESS. exists m. crush. Qed. + Lemma param_mapping_correct : + forall fn (args : list reg) fn_params (externctrl : AssocMap.t (HTL.ident * HTL.controlsignal)), + length args = length fn_params -> + (forall n arg, nth_error args n = Some arg -> + exists r, List.nth_error fn_params n = Some r /\ + externctrl ! r = Some (fn, HTL.ctrl_param n)) -> + (forall n param, nth_error fn_params n = Some param -> + externctrl!param = Some (fn, HTL.ctrl_param n)). + Proof. + intros * Hlen Htr * Hfn_params. + + assert (H : exists arg, nth_error args n = Some arg). { + apply length_nth_error. + apply nth_error_length in Hfn_params. + lia. + } + destruct H as [ arg H ]. + edestruct (Htr _ _ H) as [? [? ?]]. + + enough (Some x = Some param) by crush. + congruence. + Qed. + Lemma transl_icall_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc', @@ -1524,15 +1548,15 @@ Section CORRECTNESS. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. * admit. - + eapply HTL.step_initcall; simplify. + + eapply HTL.step_initcall. * eassumption. * eassumption. - * (* params mapped *) admit. (** TODO: We might have to change the statement of step_initcall *) + * eauto using param_mapping_correct. * big_tac. assert (dst <= (RTL.max_reg_function f))%positive by (eapply RTL.max_reg_function_def; eauto). not_control_reg. - * admit. + * simpl; trivial. + eauto with htlproof. - econstructor; try solve [repeat econstructor; eauto with htlproof ]. + admit. |