diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-05-16 11:35:31 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-05-16 11:35:31 +0100 |
| commit | 51d25ab7feeaca959d35fbd4fa905f8ce003e07b (patch) | |
| tree | 7005c02d88e7bcfcdf8403b8b83ee05de322b762 | |
| parent | becbab413e16e40069329d8e7f21dc92e2e4c4e4 (diff) | |
| download | vericert-kvx-51d25ab7feeaca959d35fbd4fa905f8ce003e07b.tar.gz vericert-kvx-51d25ab7feeaca959d35fbd4fa905f8ce003e07b.zip | |
Minimise the proof a bit
| -rw-r--r-- | src/hls/RTLPargenproof.v | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 8ecaba2..9cfee3a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -284,25 +284,19 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl. - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - eapply eval_builtin_args_eq. eapply REG. - eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. - eauto. - (econstructor; eauto with rtlgp). - intros. - unfold regmap_setres. destruct res. - destruct (Pos.eq_dec x0 x); subst. - repeat rewrite Regmap.gss; auto. - repeat rewrite Regmap.gso; auto. - eapply REG. eapply REG. + induction 1; repeat semantics_simpl; + try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. + { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + eapply eval_builtin_args_eq. eapply REG. + eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. + eauto. + intros. + unfold regmap_setres. destruct res. + destruct (Pos.eq_dec x0 x); subst. + repeat rewrite Regmap.gss; auto. + repeat rewrite Regmap.gso; auto. + eapply REG. eapply REG. } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. constructor; eauto. |