diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-10 17:25:02 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-10 17:25:02 +0100 |
| commit | 8503a79715fb2d3766bc2cd6e102481f9fec61cd (patch) | |
| tree | 2974e1307e30b9cac56b7697742b2538b2212094 /src/hls/HTLgenspec.v | |
| parent | 12a8b9d3cf31b35dcaff13b9e7c2d38fbf432403 (diff) | |
| download | vericert-8503a79715fb2d3766bc2cd6e102481f9fec61cd.tar.gz vericert-8503a79715fb2d3766bc2cd6e102481f9fec61cd.zip | |
Get entire HTLgenspec proof passing
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 40 |
1 files changed, 26 insertions, 14 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 1ccd69a..5b95d28 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -33,7 +33,6 @@ Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. From Hammer Require Import Tactics. -From Hammer Require Import Hammer. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -829,16 +828,22 @@ Proof. simplify. inversion Htrans. replace (st_st s'). - repeat eexists; try (eapply map_incr_some; inversion Htrans; eauto with htlspec); try eauto with htlspec; admit. + repeat (eapply ex_intro). + repeat split; try (eapply map_incr_some; inversion Htrans; eauto with htlspec); try eauto with htlspec. + intros. + insterU H4. + destruct H4 as [r [? ?]]. + eexists. split; eauto with htlspec. + + eapply tr_code_return; eauto with htlspec. inversion Htrans. simplify. eexists. replace (st_st s'). repeat split; eauto with htlspec. Unshelve. eauto. -Admitted. -Hint Resolve tr_code_trans : htlspec. +Qed. +Hint Resolve tr_code_trans : htlspec. Hint Resolve PTree.elements_complete : htlspec. Theorem transl_module_correct : @@ -864,13 +869,20 @@ Proof. repeat unfold_match EQ9. monadInv EQ9. monadInv EQ7. - econstructor; eauto with htlspec. - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. -Admitted. + econstructor; eauto with htlspec; try lia; + try ( + multimatch goal with + | [ EQ : _ ?s = OK ?x _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (?x, _) _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ + end; + saturate_incr; + multimatch goal with + | [ INCR : st_prop (max_state f) _ |- _ ] => inversion INCR + end; + simplify; unfold Ple in *; lia + ). + monadInv EQ6. simpl in EQ7. + monadInv EQ7. + simplify. unfold Ple in *. lia. +Qed. |