diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-12 20:30:55 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-12 20:30:55 +0100 |
commit | 3113194b86597c770b83d8efb4c7980e1bc4a715 (patch) | |
tree | e984fecc92bb5169a034acac528ab2ed84899eff /src/hls/RTLBlockgenproof.v | |
parent | 70f440ee13ff95f67a9886c63061c5fd28d7f613 (diff) | |
download | vericert-3113194b86597c770b83d8efb4c7980e1bc4a715.tar.gz vericert-3113194b86597c770b83d8efb4c7980e1bc4a715.zip |
Completely finish RTLBlockgenproof
Diffstat (limited to 'src/hls/RTLBlockgenproof.v')
-rw-r--r-- | src/hls/RTLBlockgenproof.v | 83 |
1 files changed, 65 insertions, 18 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 875c582..642264f 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -35,6 +35,7 @@ Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import vericert.common.Vericertlib. +Require Import vericert.common.DecEq. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLBlockgen. @@ -325,6 +326,65 @@ whole execution (in one big step) of the basic block. | Some b' => 1 + length b' end. + Lemma check_valid_node_correct : + forall a b, check_valid_node a b = true -> valid_succ a b. + Proof. + intros. unfold valid_succ, check_valid_node in *. + destruct_match; try discriminate; eauto. + Qed. + + Lemma transl_entrypoint_exists : + forall f tf, + transl_function f = OK tf -> + valid_succ (fn_code tf) (fn_entrypoint tf). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + eauto using check_valid_node_correct. + Qed. + + Lemma ceq_eq : + forall A a (b: A) c, + ceq a b c = true -> + b = c. + Proof. + intros. unfold ceq in H. destruct_match; try discriminate. auto. + Qed. + + Ltac unfold_ands := + repeat match goal with + | H: _ && _ = true |- _ => apply andb_prop in H + | H: _ /\ _ |- _ => inv H + | H: ceq _ _ _ = true |- _ => apply ceq_eq in H; subst + end. + + Lemma transl_match_code' : + forall c tc b pc i, + check_code' c tc pc b i = true -> + match_block c tc pc b i. + Proof. + induction b; [crush|]. + intros. unfold check_code' in H. + do 4 (destruct_match; try discriminate); + try (repeat (destruct_match; try discriminate; []); unfold_ands; constructor; auto using check_valid_node_correct); + fold check_code' in *; + try (destruct_match; try discriminate; unfold_ands; econstructor; eauto); + apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct. + Qed. + + Lemma transl_match_code : + forall f tf, + transl_function f = OK tf -> + match_code f.(RTL.fn_code) tf.(fn_code). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + unfold match_code; intros. + eapply forall_ptree_true in Heqb0; eauto. + unfold check_code in *. + eauto using transl_match_code'. + Qed. + Lemma transl_initial_states : forall s1, RTL.initial_state prog s1 -> exists s2, RTLBlock.initial_state tprog s2 /\ match_states None s1 s2. @@ -751,18 +811,6 @@ whole execution (in one big step) of the basic block. unfold sem_extrap. intros. setoid_rewrite H5 in H8. crush. Qed. - Lemma transl_entrypoint_exists : - forall f tf, - transl_function f = OK tf -> - exists b, (fn_code tf) ! (fn_entrypoint tf) = Some b. - Proof. Admitted. - - Lemma transl_match_code : - forall f tf, - transl_function f = OK tf -> - match_code f.(RTL.fn_code) tf.(fn_code). - Proof. Admitted. - Lemma init_regs_equiv : forall b a, init_regs a b = RTL.init_regs a b. Proof. induction b; crush. Qed. @@ -781,9 +829,8 @@ whole execution (in one big step) of the basic block. inversion 1; subst; simplify. monadInv TF. inv H0. pose proof (transl_match_code _ _ EQ). - pose proof (transl_entrypoint_exists _ _ EQ). + pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1. simplify. - exploit transl_entrypoint_exists; eauto; simplify. destruct x0. apply sim_plus. do 3 econstructor. assert (fn_stacksize x = RTL.fn_stacksize f). @@ -802,14 +849,14 @@ whole execution (in one big step) of the basic block. repeat (destruct_match; try discriminate; []). inv EQ; auto. } unfold match_code in H0. - pose proof (H0 _ _ H3). + pose proof (H0 _ _ H2). econstructor; eauto. rewrite <- H1. eauto. rewrite H1. - rewrite init_regs_equiv. rewrite H4. eapply star_refl. + rewrite init_regs_equiv. rewrite H3. eapply star_refl. unfold sem_extrap; intros. - setoid_rewrite H2 in H7; simplify. - rewrite H4. eauto. + setoid_rewrite H2 in H6; simplify. + rewrite H3. eauto. Qed. Lemma transl_externalcall_correct: |