diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-11 14:55:21 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-11 14:55:21 +0100 |
commit | 92548d15a08abefe7ee3b68a37c637c4e4f69e03 (patch) | |
tree | 0a24bf5e3dbe649d14a3565bea308db08e673c7b /src | |
parent | 274cb94ca622a5f97442cf11e044b7eab041e94f (diff) | |
download | vericert-92548d15a08abefe7ee3b68a37c637c4e4f69e03.tar.gz vericert-92548d15a08abefe7ee3b68a37c637c4e4f69e03.zip |
Finish Inop proof for basic block generation
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/RTLBlockgenproof.v | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index ed16fe3..857e680 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -341,9 +341,6 @@ whole execution (in one big step) of the basic block. 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. @@ -353,18 +350,34 @@ whole execution (in one big step) of the basic block. Proof. induction l; crush. Qed. Lemma transl_Inop_correct_nj: - forall s f sp pc rs m stk' tf pc1 rs1 m1 b x pc', + forall s f sp pc rs m stk' tf pc1 rs1 m1 b pc', imm_succ pc pc' -> (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> match_states (Some (RBnop :: b)) (RTL.State s f sp pc rs m) (State stk' tf sp pc1 rs1 (PMap.init false) m1) -> (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - match_block (RTL.fn_code f) pc' b x -> exists b' s2', Smallstep.star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' /\ match_states b' (RTL.State s f sp pc' rs m) s2'. Proof. - intros s f sp pc rs m H stk' tf pc1 rs1 m1 b H0 x H1 H3. Admitted. + intros * H1 H2 H3 H4. + inv H3. simplify. pose proof CODE as CODE'. + unfold match_code3, match_code' in *. inv CODE. + pose proof (H _ _ H0). + do 3 econstructor. + eapply Smallstep.star_refl. + instantiate (1 := Some b). + econstructor; try eassumption. + do 2 econstructor; try eassumption. + inv H3; crush. + eapply Smallstep.star_right; eauto. + eapply RTL.exec_Inop; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + constructor; auto. + auto. + Qed. Lemma transl_Inop_correct_j: forall s f sp pc rs m pc' stk' tf pc1 rs1 m1 x, @@ -382,17 +395,16 @@ whole execution (in one big step) of the basic block. match_states b' (RTL.State s f sp pc' rs m) s2'. Proof. intros * H H0 H1 H4 H5 H8. - inv H0. - simplify. + inv H0. simplify. do 3 econstructor. apply Smallstep.star_one. econstructor. eassumption. eapply BB; [econstructor; constructor | eassumption]. setoid_rewrite <- H5. econstructor. econstructor. eassumption. eassumption. eauto. eassumption. - - (* apply Smallstep.star_refl. admit. *) - (* Admitted. *) - Admitted. + eapply Smallstep.star_refl. + unfold sem_extrap. intros. setoid_rewrite H8 in H3. + crush. + Qed. Definition imm_succ_dec pc pc' : {imm_succ pc pc'} + {~ imm_succ pc pc'}. Proof. |