diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
| commit | f8bd8cde25321a3a4a3195bf9189416194b3732e (patch) | |
| tree | 7773d41eebb8ad6e26d545cc81ad51d24d2bd6a4 /src/hls/IfConversionproof.v | |
| parent | c35404c110b7616b30eeb48fc4051dcb33d84f40 (diff) | |
| download | vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.tar.gz vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.zip | |
Clean up proofs
Diffstat (limited to 'src/hls/IfConversionproof.v')
| -rw-r--r-- | src/hls/IfConversionproof.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index e13db00..2d8cfac 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -673,7 +673,7 @@ Section CORRECTNESS. /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof using. induction x0; simplify. - - inv H1. inv H. exists nil. exists b'0. + - inv H1. inv H. exists (@nil instr). exists b'0. split; [|constructor]. rewrite app_nil_l. replace (RBexit x cf :: b'0) with ((RBexit x cf :: nil) ++ b'0) by auto. f_equal. simplify. destruct cf; auto. @@ -761,7 +761,7 @@ Section CORRECTNESS. /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof using. induction x0; simplify. - - inv H1. inv H. exists nil. exists b'0. + - inv H1. inv H. exists (@nil instr). exists b'0. split; [|constructor]. rewrite app_nil_l. f_equal. simplify. apply wf_transition_block_opt_prop in H0. rewrite H0. rewrite Pos.eqb_refl. auto. @@ -809,7 +809,7 @@ Section CORRECTNESS. econstructor; eauto. constructor; auto. + exploit exec_if_conv2; eauto; simplify. exploit step_cf_eq; eauto; simplify. - apply sim_plus. exists None. exists x4. + apply sim_plus. exists (@None (list instr)). exists x4. split. apply plus_one. econstructor; eauto. apply append. exists (mki rs' pr' m'). split; auto. apply step_list_2_eq; auto. @@ -838,7 +838,7 @@ Section CORRECTNESS. rewrite IS_B in H0; simplify. exploit step_cf_eq; eauto; simplify. apply sim_plus. - exists None. exists x. + exists (@None (list instr)). exists x. split; auto. unfold sem_extrap in *. inv SIM. @@ -861,14 +861,14 @@ Section CORRECTNESS. - eauto using match_some_correct. - eauto using match_none_correct. - apply sim_plus. remember (transf_function l f) as tf. symmetry in Heqtf. func_info. - exists None. eexists. split. + exists (@None (list instr)). eexists. split. apply plus_one. constructor; eauto. rewrite <- H1. eassumption. rewrite <- H4. rewrite <- H2. econstructor; auto. - - apply sim_plus. exists None. eexists. split. + - apply sim_plus. exists (@None (list instr)). eexists. split. apply plus_one. constructor; eauto. constructor; auto. - apply sim_plus. remember (transf_function None f) as tf. symmetry in Heqtf. func_info. - exists None. inv STK. inv H7. eexists. split. apply plus_one. constructor. + exists (@None (list instr)). inv STK. inv H7. eexists. split. apply plus_one. constructor. econstructor; auto. Qed. |