diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-30 14:39:31 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-30 14:39:31 +0100 |
| commit | dab4185f5724fd2dabc88fc50c68d322ffafb56b (patch) | |
| tree | 0bb034b55379a721bb026479fca5327890250d9d | |
| parent | 583f1e12247bbb3c5ede02e04020036e50464636 (diff) | |
| download | vericert-dab4185f5724fd2dabc88fc50c68d322ffafb56b.tar.gz vericert-dab4185f5724fd2dabc88fc50c68d322ffafb56b.zip | |
Clarify ireturn proof
| -rw-r--r-- | src/hls/HTLgenproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index f320ce0..403ba00 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -2311,10 +2311,10 @@ Section CORRECTNESS. eexists; split. - eapply Smallstep.plus_three. + (* Return to caller *) - repeat econstructor; eauto. + eapply HTL.step_return; repeat econstructor; eauto. + (* Join *) inv CONST. - econstructor; eauto. + eapply HTL.step_module; eauto. * big_tac; inv TF; simplify; not_control_reg. * big_tac; inv TF; simplify; not_control_reg. * big_tac; inv TF; simplify; not_control_reg. @@ -2323,12 +2323,12 @@ Section CORRECTNESS. rewrite fso by crush. rewrite fss. crush. * big_tac; inv TF; simplify; not_control_reg. - * repeat econstructor. simpl. + * (* datapath *) + repeat econstructor. simpl. rewrite AssocMap.fso by crush. rewrite AssocMap.fss. auto. - * simplify. - constructor. + * simplify. constructor. * big_tac; inv TF; simplify; not_control_reg. + simplify. eapply HTL.step_finish_reset with (fin:=fin). |