diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 21:13:49 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 21:13:49 +0100 |
| commit | 4a35f89eca3650e80470cf9ac6e0dc4ea3c9f6e8 (patch) | |
| tree | 97bab03d2e44f09500415c2d96ce20ffa3c098da | |
| parent | 52d3374aecc7eca80233edb3f1c6802b44e89f5a (diff) | |
| download | vericert-4a35f89eca3650e80470cf9ac6e0dc4ea3c9f6e8.tar.gz vericert-4a35f89eca3650e80470cf9ac6e0dc4ea3c9f6e8.zip | |
Get HTLgenproof to compile with RAM inference
| -rw-r--r-- | src/hls/HTLgenproof.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index c2cbbf8..232c52c 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1194,6 +1194,7 @@ Section CORRECTNESS. + inv CONST; assumption. + repeat constructor. + repeat constructor. + + constructor. + big_tac. - inv CONST. inv MARR. simplify. big_tac. constructor; rewrite AssocMap.gso; crush. @@ -1223,6 +1224,7 @@ Section CORRECTNESS. - inv CONST. assumption. - repeat econstructor. - repeat econstructor. intuition eauto. + - constructor. - big_tac. assert (Ple res0 (RTL.max_reg_function f)) by eauto using RTL.max_reg_function_def. @@ -1489,9 +1491,11 @@ Section CORRECTNESS. * repeat econstructor; eauto. * repeat econstructor; eauto. * eapply fork_exec. + * constructor. * trivial. * trivial. - * eapply AssocMapExt.merge_correct_1. + * big_tac. + eapply AssocMapExt.merge_correct_1. rewrite assign_all_out. -- big_tac. not_control_reg. @@ -1536,6 +1540,7 @@ Section CORRECTNESS. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. * repeat econstructor. + * constructor. * simpl. apply AssocMapExt.merge_correct_2. big_tac. @@ -1595,7 +1600,7 @@ Section CORRECTNESS. + eapply HTL.step_module; try solve [ repeat econstructor; eauto ]. * repeat econstructor. apply return_val_exec_spec. * big_tac. - * inversion wf. + * inversion wf1. eapply H10. eapply AssocMapExt.elements_iff. eauto. @@ -1657,6 +1662,8 @@ Section CORRECTNESS. rewrite fss. crush. * big_tac; inv TF; simplify; not_control_reg. * repeat econstructor. + * replace (HTL.mod_ram m0) with (@None HTL.ram) by (inv TF; trivial). + constructor. * big_tac; inv TF; simplify; not_control_reg. + trivial. - simpl. |