diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-20 10:42:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-20 10:42:00 +0100 |
| commit | 684a250e27c7bbbad6b8a60e789dc7d90a9ce16c (patch) | |
| tree | 2e9f92716c11f32858dc10cecdc86e113bb162a2 | |
| parent | 2388d026b3bdba82139a04136aab47468e04ee2c (diff) | |
| download | vericert-684a250e27c7bbbad6b8a60e789dc7d90a9ce16c.tar.gz vericert-684a250e27c7bbbad6b8a60e789dc7d90a9ce16c.zip | |
Finish Giblesubpargenproof
| -rw-r--r-- | src/hls/GibleSubPargenproof.v | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/src/hls/GibleSubPargenproof.v b/src/hls/GibleSubPargenproof.v index ab2fef6..c975dfd 100644 --- a/src/hls/GibleSubPargenproof.v +++ b/src/hls/GibleSubPargenproof.v @@ -319,8 +319,12 @@ Section CORRECTNESS. Proof. induction a; intros. - cbn in *. inv H. - - inv H. - Admitted. + - inv H. destruct i1; destruct i. + + econstructor. eapply step_list_ge; eauto. + eapply IHa; eauto. + + inv H6. eapply exec_RBterm; eauto. eapply step_list_ge; eauto. + eapply exec_RBterm; eauto. eapply step_list_ge; eauto. + Qed. Lemma transl_spec_not_in': forall bb pc fresh code_start fresh' code_end pc' y, @@ -397,10 +401,13 @@ Section CORRECTNESS. - cbn in HTRANSL. repeat (destruct_match; try discriminate). inv HTRANSL. exploit transl_spec_not_in'. unfold transl_block. rewrite HFOLD. cbn. eauto. rewrite PTree.gss. eauto. intros. eapply H2 in H. - econstructor. split. - + apply Smallstep.plus_one. econstructor; eauto. - eapply step_instr_seq_with_exit'; eauto. - Admitted. + exploit step_cf_instr_ge; eauto. + inv H3. econstructor; eauto. + intros (tst' & HSTEP & HMATCH). + econstructor. split; eauto. + apply Smallstep.plus_one. econstructor; eauto. + eapply step_instr_seq_with_exit'; eauto. + Qed. Lemma transl_spec': forall l fresh fresh' code_start code_end pc bb, @@ -465,7 +472,6 @@ Section CORRECTNESS. - cbn in *. intros * HMATCH. inv HMATCH. cbn in *. inv TF. econstructor. split. + apply Smallstep.plus_one. econstructor. eapply Events.external_call_symbols_preserved; eauto. - eapply senv_preserved. + now constructor. - cbn in *. intros * HMATCH. inv HMATCH. inv STK. inv H1. econstructor; split. |