diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-21 08:58:45 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-21 08:58:45 +0100 |
| commit | 2dbba9848094bd29f00692529764f1541e27d21a (patch) | |
| tree | 0861b0416b189c11bf6f7477ed20190081ebb36e | |
| parent | 9a9a6510ab9a3bf7b17093501584bc06ea0e4dfd (diff) | |
| download | vericert-2dbba9848094bd29f00692529764f1541e27d21a.tar.gz vericert-2dbba9848094bd29f00692529764f1541e27d21a.zip | |
Work on smallstep proof
| -rw-r--r-- | src/hls/RTLBlockgenproof.v | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index d62ccf9..b191c09 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -29,6 +29,7 @@ Require Import compcert.common.Errors. Require Import compcert.common.Globalenvs. Require Import compcert.lib.Maps. Require Import compcert.backend.Registers. +Require compcert.common.Smallstep. Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. @@ -222,17 +223,36 @@ Section CORRECTNESS. inversion 2; crush. subst. inv H. inv STK. econstructor. Qed. + Compute (hd_error (list_drop 3 (1::2::3::4::5::nil))). + Compute (nth_error (1::2::3::4::5::nil) 3). + + Lemma hd_nth_equiv: + forall A n (l: list A), hd_error (list_drop n l) = nth_error l n. + Proof. induction n; destruct l; crush. Qed. + + Lemma hd_error_Some_exists: + forall A (l: list A) n, hd_error l = Some n -> l = n :: tl l. + Proof. induction l; crush. Qed. + Lemma transl_Inop_correct: forall s f sp pc rs m pc', (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> forall s2, match_states (RTL.State s f sp pc rs m) s2 -> - exists s2', Smallstep.plus step tge s2 Events.E0 s2' + exists s2', Smallstep.star step tge s2 Events.E0 s2' /\ match_states (RTL.State s f sp pc' rs m) s2'. Proof. intros s f sp pc rs m pc' H. inversion 1; simplify. inv H1. inv H0. inv BB0. inv PC0. - - + - inv H2. inv H5. inv H2. rewrite <- hd_nth_equiv in H6. + assert (bb_body x = bb0). + { rewrite H5 in H0. inv H0. auto. } + subst. + apply hd_error_Some_exists in H6. rewrite H6. + rewrite H1 in H. simplify. + destruct i'; crush. + econstructor. split. + Admitted. Lemma transl_Iop_correct: |