diff options
Diffstat (limited to 'src/hls/GiblePargenproof.v')
-rw-r--r-- | src/hls/GiblePargenproof.v | 135 |
1 files changed, 94 insertions, 41 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 36392d8..30d6a46 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2023 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -53,7 +53,8 @@ RTLPargenproof RTLBlock to abstract translation ================================ -Correctness of translation from RTLBlock to the abstract interpretation language. +Correctness of translation from RTLBlock to the abstract interpretation +language. |*) Definition is_regs i := match i with mk_instr_state rs _ _ => rs end. @@ -194,7 +195,8 @@ Definition check_dest i r' := | _ => false end. -Lemma check_dest_dec i r : {check_dest i r = true} + {check_dest i r = false}. +Lemma check_dest_dec i r : + {check_dest i r = true} + {check_dest i r = false}. Proof. destruct (check_dest i r); tauto. Qed. Fixpoint check_dest_l l r := @@ -209,7 +211,8 @@ Lemma check_dest_l_forall : Forall (fun x => check_dest x r = false) l. Proof. induction l; crush. Qed. -Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. +Lemma check_dest_l_dec i r : + {check_dest_l i r = true} + {check_dest_l i r = false}. Proof. destruct (check_dest_l i r); tauto. Qed. Lemma match_states_list : @@ -1880,7 +1883,13 @@ all be evaluable. forall xs x v, mfold_left update xs x = Some v -> exists y, x = Some y. - Proof. Admitted. + Proof. + induction xs; intros. + { cbn in *. inv H. eauto. } + cbn in *. unfold Option.bind in *. exploit IHxs; eauto. + intros. simplify. destruct x; crush. + eauto. + Qed. Lemma step_instr_term_exists : forall A B ge sp v x v2 cf, @@ -1888,14 +1897,6 @@ all be evaluable. exists p, x = RBexit p cf. Proof using. inversion 1; eauto. Qed. - Lemma abstr_fold_falsy : - forall A i sp ge f i' cf p f' ilist p', - @sem A (mk_ctx i sp ge) f (i', cf) -> - mfold_left update ilist (Some (p, f)) = Some (p', f') -> - eval_predf (is_ps i') p = false -> - sem (mk_ctx i sp ge) f' (i', cf). - Proof. Admitted. - Lemma eval_predf_update_true : forall i i' curr_p next_p f f_next instr sp, update (curr_p, f) instr = Some (next_p, f_next) -> @@ -2058,6 +2059,38 @@ all be evaluable. eauto using eval_predf_update_evaluable. Qed. +(*| +``abstr_fold_falsy``: This lemma states that when we are at the end of an +execution, the values in the register map do not continue to change. This +should mean that we can show the forest is still evaluable if it was evaluable +at any point at the end of the execution. +|*) + + Lemma abstr_fold_falsy : + forall A i sp ge f res p f' ilist p', + @sem A (mk_ctx i sp ge) f res -> + forest_evaluable (mk_ctx i sp ge) f -> + mfold_left update ilist (Some (p, f)) = Some (p', f') -> + eval_predf (is_ps (fst res)) p = false -> + sem (mk_ctx i sp ge) f' res /\ forest_evaluable (mk_ctx i sp ge) f'. + Proof. Admitted. + + (* Lemma abstr_fold_falsy_evaluable : *) + (* forall sp x i i' i'' cf f p f' curr_p *) + (* (FEVAL: forest_evaluable (mk_ctx i sp ge) f) *) + (* (VALID: valid_mem (is_mem i) (is_mem i')), *) + (* SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> *) + (* sem (mk_ctx i sp ge) f (i', Some cf) -> *) + (* mfold_left update x (Some (curr_p, f)) = Some (p, f') -> *) + (* eval_predf (is_ps i') curr_p = false -> *) + + Lemma forest_evaluable_lessdef : + forall A (ge: Genv.t A unit) sp st st' f, + forest_evaluable (mk_ctx st sp ge) f -> + state_lessdef st st' -> + forest_evaluable (mk_ctx st' sp ge) f. + Proof. Admitted. (* easy *) + Lemma abstr_fold_correct : forall sp x i i' i'' cf f p f' curr_p (FEVAL: forest_evaluable (mk_ctx i sp ge) f) @@ -2077,36 +2110,39 @@ all be evaluable. - (* inductive case *) exploit mfold_left_update_Some; eauto; intros Hexists; inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. - exploit eval_predf_update_true; eauto; intros EVALTRUE. + exploit eval_predf_update_true; (* TODO *) + eauto; intros EVALTRUE. rewrite EXEQ in H2. eapply IHx in H2; cbn [fst snd] in *. eauto. - eapply eval_predf_update_evaluable; eauto. + eapply eval_predf_update_evaluable; eauto. (* TODO *) transitivity (is_mem i'); auto. - eapply sem_update_valid_mem; eauto. + eapply sem_update_valid_mem; eauto. (* TODO *) eauto. - eapply sem_update_instr; eauto. eauto. eauto. + eapply sem_update_instr; eauto. eauto. eauto. (* MAIN TODO *) - (* terminal case *) exploit mfold_left_update_Some; eauto; intros Hexists; inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. rewrite EXEQ in H2. - exploit state_lessdef_sem; eauto; intros H; inversion H as [v [Hi LESSDEF]]; clear H. - exploit step_instr_lessdef_term; eauto; intros H; inversion H as [v2 [Hi2 LESSDEF2]]; clear H. + exploit state_lessdef_sem; (* TODO *) + eauto; intros H; inversion H as [v [Hi LESSDEF]]; clear H. + exploit step_instr_lessdef_term; (* TODO *) + eauto; intros H; inversion H as [v2 [Hi2 LESSDEF2]]; clear H. exploit step_instr_term_exists; eauto; inversion 1 as [? ?]; subst; clear H. erewrite eval_predf_lessdef in H1 by eassumption. - exploit sem_update_instr_term; eauto; intros [A B]. - exists v2. split. inv Hi2. - eapply abstr_fold_falsy; try eassumption. - split; auto. - split. - + exploit IHx. - 6: { eauto. } - admit. - admit. - admit. - admit. - admit. - admit. - admit. - Admitted. + exploit sem_update_instr_term; (* TODO *) + eauto; intros [A B]. + exists v2. + exploit abstr_fold_falsy. (* TODO *) + apply A. + eapply forest_evaluable_lessdef; (* TODO *) + try eassumption. + eapply eval_predf_update_evaluable. (* TODO *) + eassumption. eassumption. auto. + eassumption. cbn. inversion Hi2; subst. auto. intros. + inversion_clear H as [Hsem Hforest]. split. auto. split. auto. + split. eapply forest_evaluable_lessdef; (* TODO *) + try eassumption. + symmetry. auto. inversion H7; subst. auto. + Qed. Lemma sem_regset_empty : forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). @@ -2143,10 +2179,11 @@ all be evaluable. Proof. unfold abstract_sequence. intros. unfold Option.map in H0. destruct_match; try easy. - destruct p; simplify. - (*eapply abstr_fold_correct; eauto. - simplify. eapply sem_empty. auto. - Qed.*) Admitted. + destruct p as [p TMP]; simplify. + exploit abstr_fold_correct; eauto; crush. + { apply sem_empty. } + exists x0. auto. + Qed. Lemma abstr_check_correct : forall sp i i' a b cf ti, @@ -2155,7 +2192,17 @@ all be evaluable. state_lessdef i ti -> exists ti', sem (mk_ctx ti sp ge) b (ti', cf) /\ state_lessdef i' ti'. - Proof. Admitted. + Proof. + +(*| +Proof Sketch: + +Two abstract states can be equivalent, without it being obvious that they can +actually both be executed assuming one can be executed. One will therefore have +to add a few more assumptions to makes it possible to execute the other. +|*) + + Admitted. Lemma abstr_seq_reverse_correct : forall sp x i i' ti cf x', @@ -2181,7 +2228,7 @@ comparison, because there two abstract states can be equal without one being evaluable. |*) -Admitted. + Admitted. (*| This is the top-level lemma which uses the following proofs to complete the @@ -2231,7 +2278,13 @@ square: match_states s ts -> exists ts', step_cf_instr tge ts cf t ts' /\ match_states s' ts'. - Proof. Admitted. + Proof. + +(*| +Proof Sketch: Trivial because of structural equality. +|*) + + Admitted. Lemma match_states_stepBB : forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm', |