From 9db69b471864cb9e3868dd2c82bc0e2df3955b51 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 20 Oct 2023 19:05:00 +0100 Subject: Fix more proofs moving to proving instructions --- src/hls/DHTLgen.v | 2 +- src/hls/DHTLgenproof.v | 258 ++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 247 insertions(+), 13 deletions(-) diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v index 49d2c87..d573dda 100644 --- a/src/hls/DHTLgen.v +++ b/src/hls/DHTLgen.v @@ -356,7 +356,7 @@ Definition transf_seq_block (ctrl: control_regs) (d: datapath) (ni: node * SubPa let (n, bb) := ni in match d ! n with | None => - do (_pred, stmnt) <- transf_parallel_block ctrl bb; + do (_pred, stmnt) <- transf_chained_block ctrl (Ptrue, Vskip) (concat bb); OK (PTree.set n stmnt d) | _ => Error (msg "DHTLgen: overwriting location") end. diff --git a/src/hls/DHTLgenproof.v b/src/hls/DHTLgenproof.v index e369507..bd8320e 100644 --- a/src/hls/DHTLgenproof.v +++ b/src/hls/DHTLgenproof.v @@ -1373,6 +1373,20 @@ Opaque Mem.alloc. forall A B f l m, @mfold_left A B f l (Error m) = Error m. Proof. now induction l. Qed. + Lemma mfold_left_cons: + forall A B f a l x y, + @mfold_left A B f (a :: l) x = OK y -> + exists x' y', @mfold_left A B f l (OK y') = OK y /\ f x' a = OK y' /\ x = OK x'. + Proof. + intros. + destruct x; [|now rewrite mfold_left_error in H]. + cbn in H. + replace (fold_left (fun (a : mon A) (b : B) => bind (fun a' : A => f a' b) a) l (f a0 a) = OK y) with + (mfold_left f l (f a0 a) = OK y) in H by auto. + destruct (f a0 a) eqn:?; [|now rewrite mfold_left_error in H]. + eauto. + Qed. + Lemma step_cf_instr_pc_ind : forall s f sp rs' pr' m' pc pc' cf t state, step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf t state -> @@ -1386,33 +1400,183 @@ Opaque Mem.alloc. ctrl_return := Pos.succ (Pos.succ (Pos.succ (max_resource_function f))) |}. - Lemma transl_step_state_correct_instr : - forall s f sp bb hw_pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa, + Lemma step_list_inter_not_term : + forall A step_i sp i cf l i' cf', + @step_list_inter A step_i sp (Iterm i cf) l (Iterm i' cf') -> + i = i' /\ cf = cf'. + Proof. now inversion 1. Qed. + + Lemma step_exec_concat2' : + forall sp i c a l cf, + SubParBB.step_instr_list ge sp (Iexec a) i (Iterm c cf) -> + SubParBB.step_instr_list ge sp (Iexec a) (i ++ l) (Iterm c cf). + Proof. + induction i. + - inversion 1. + - inversion 1; subst; clear H; cbn. + destruct i1. econstructor; eauto. eapply IHi; eauto. + exploit step_list_inter_not_term; eauto; intros. inv H. + eapply exec_term_RBcons; eauto. eapply exec_term_RBcons_term. + Qed. + + Lemma step_exec_concat' : + forall sp i c a b l, + SubParBB.step_instr_list ge sp (Iexec a) i (Iexec c) -> + SubParBB.step_instr_list ge sp (Iexec c) l b -> + SubParBB.step_instr_list ge sp (Iexec a) (i ++ l) b. + Proof. + induction i. + - inversion 1. eauto. + - inversion 1; subst. clear H. cbn. intros. econstructor; eauto. + destruct i1; [|inversion H6]. + eapply IHi; eauto. + Qed. + + Lemma step_exec_concat: + forall sp bb a b, + SubParBB.step ge sp a bb b -> + SubParBB.step_instr_list ge sp a (concat bb) b. + Proof. + induction bb. + - inversion 1. + - inversion 1; subst; clear H. + + cbn. eapply step_exec_concat'; eauto. + + cbn in *. eapply step_exec_concat2'; eauto. + Qed. + + Lemma transl_step_state_correct_instr_state : + forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf pc', (* (fn_code f) ! pc = Some bb -> *) mfold_left (transf_instr (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) -> eval_predf pr curr_p = true -> SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb - (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) -> - match_states (GibleSubPar.State s f sp hw_pc rs pr m) (DHTL.State s' m_ hw_pc asr asa) -> + (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) -> + step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.State s f sp pc' rs' pr' m') -> + match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) -> exists asr' asa', stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa') - /\ match_states (GibleSubPar.State s f sp hw_pc rs' pr' m') (DHTL.State s' m_ hw_pc asr' asa'). + /\ match_states (GibleSubPar.State s f sp pc' rs' pr' m') (DHTL.State s' m_ pc' asr' asa'). Proof. Admitted. - Lemma transl_step_state_correct_chained : - forall s f sp bb hw_pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa, + Lemma transl_step_state_correct_instr_return : + forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf v, + (* (fn_code f) ! pc = Some bb -> *) + mfold_left (transf_instr (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> + stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) -> + eval_predf pr curr_p = true -> + SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb + (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) -> + step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.Returnstate s v m') -> + match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) -> + exists asr' asa' retval, + stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa') + /\ val_value_lessdef v retval + /\ asr'!(m_.(DHTL.mod_finish)) = Some (ZToValue 1) + /\ asr'!(m_.(DHTL.mod_return)) = Some retval + /\ match_states (GibleSubPar.Returnstate s v m') (DHTL.Returnstate s' retval). + Proof. Admitted. + + Lemma transl_step_state_correct_chained_state : + forall s f sp bb pc pc' curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf, (* (fn_code f) ! pc = Some bb -> *) mfold_left (transf_chained_block (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) -> eval_predf pr curr_p = true -> SubParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb - (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) -> - match_states (GibleSubPar.State s f sp hw_pc rs pr m) (DHTL.State s' m_ hw_pc asr asa) -> + (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) -> + step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.State s f sp pc' rs' pr' m') -> + match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) -> exists asr' asa', stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa') - /\ match_states (GibleSubPar.State s f sp hw_pc rs' pr' m') (DHTL.State s' m_ hw_pc asr' asa'). - Proof. Admitted. + /\ match_states (GibleSubPar.State s f sp pc' rs' pr' m') (DHTL.State s' m_ pc' asr' asa'). + Proof. Abort. + + Lemma transl_step_through_cfi' : + forall bb ctrl curr_p stmnt next_p stmnt' p cf, + mfold_left (transf_instr ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> + In (RBexit p cf) bb -> + exists curr_p' stmnt'', translate_cfi ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt''. + Proof. + induction bb. + - inversion 2. + - intros * HFOLD HIN. + exploit mfold_left_cons; eauto. + intros (x' & y' & HFOLD' & HTRANSF & HSUBST). + inversion HSUBST. inv H0. clear HSUBST. + inv HIN; destruct y'; eauto. + cbn in HTRANSF. unfold Errors.bind in HTRANSF. repeat (destruct_match; try discriminate; []). + inv HTRANSF. eauto. + Qed. + + Lemma transl_step_through_cfi : + forall bb ctrl curr_p stmnt next_p stmnt' l p cf, + mfold_left (transf_chained_block ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> + In l bb -> + In (RBexit p cf) l -> + exists curr_p' stmnt'', translate_cfi ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt''. + Proof. + induction bb. + - inversion 2. + - intros * HFOLD HIN1 HIN2. + exploit mfold_left_cons; eauto. + intros (x' & y' & HFOLD' & HTRANSF & HSUBST). + destruct y'. inv HSUBST. + inv HIN1; eauto. + exploit transl_step_through_cfi'; eauto. + Qed. + + Lemma cf_in_bb_subparbb' : + forall sp bb a b cf, + SubParBB.step_instr_list ge sp (Iexec a) bb (Iterm b cf) -> + exists curr_p, In (RBexit curr_p cf) bb /\ truthy (is_ps b) curr_p. + Proof. + induction bb. + - intros. inv H. + - intros. inv H. + destruct i1. + + exploit IHbb; eauto. intros (curr_p & HIN & HTRY). + exists curr_p. split; auto. now apply in_cons. + + inv H4. exists p. inv H6; split; auto; now constructor. + Qed. + + Lemma cf_in_bb_subparbb : + forall sp bb a b cf, + SubParBB.step_instr_seq ge sp (Iexec a) bb (Iterm b cf) -> + exists l curr_p, In l bb /\ In (RBexit curr_p cf) l /\ truthy (is_ps b) curr_p. + Proof. + induction bb. + - intros. inv H. + - intros. inv H. + + exploit IHbb; eauto. intros (l & curr_p & HIN2 & HIN & HTRY). + exists l, curr_p. split; auto. now apply in_cons. + + exploit cf_in_bb_subparbb'; eauto. + intros (curr_p & HIN & HTR). + exists a, curr_p. split; auto. now constructor. + Qed. + + Lemma match_states_cf_events_translate_cfi: + forall T1 cf T2 p t ctrl stmnt, + translate_cfi ctrl p cf = OK stmnt -> + step_cf_instr ge T1 cf t T2 -> + t = Events.E0. + Proof. + intros * HGET HSTEP. + destruct cf; try discriminate; inv HSTEP; eauto. + Qed. + + Lemma match_states_cf_states_translate_cfi: + forall T1 cf T2 p t ctrl stmnt, + translate_cfi ctrl p cf = OK stmnt -> + step_cf_instr ge T1 cf t T2 -> + exists s f sp pc rs pr m, + T1 = GibleSubPar.State s f sp pc rs pr m + /\ ((exists pc', T2 = GibleSubPar.State s f sp pc' rs pr m) + \/ (exists v m' stk, Mem.free m stk 0 (fn_stacksize f) = Some m' /\ sp = Values.Vptr stk Ptrofs.zero /\ T2 = GibleSubPar.Returnstate s v m')). + Proof. + intros * HGET HSTEP. + destruct cf; try discriminate; inv HSTEP; try (now repeat econstructor). + Qed. Lemma one_ne_zero: Int.repr 1 <> Int.repr 0. @@ -1536,6 +1700,56 @@ Opaque Mem.alloc. repeat (destruct_match; try discriminate). inversion_clear H as []. auto. Qed. + Lemma match_states_ok_transl : + forall s f sp pc rs pr mem R1, + match_states (GibleSubPar.State s f sp pc rs pr mem) R1 -> + exists m asr asa s', transl_module f = OK m /\ R1 = DHTL.State s' m pc asr asa. + Proof. inversion 1; subst. now repeat eexists. Qed. + + Lemma transl_spec_in_output : + forall l ctrl d_in d_out pc stmnt, + mfold_left (transf_seq_block ctrl) l (OK d_in) = OK d_out -> + d_in ! pc = Some stmnt -> + d_out ! pc = Some stmnt. + Proof. + induction l; intros * HFOLD HIN. + - cbn in *; now (inversion HFOLD; subst). + - exploit mfold_left_cons; eauto. + intros (x' & y' & HFOLD_EXP & TRANSFSEQ & HINV). inv HINV. + unfold transf_seq_block in TRANSFSEQ. repeat (destruct_match; try discriminate; []). + destruct (peq pc n); subst. + + now rewrite Heqo in HIN. + + unfold Errors.bind2 in TRANSFSEQ. repeat (destruct_match; try discriminate; []). + inv TRANSFSEQ. eapply IHl; eauto. now rewrite PTree.gso by auto. + Qed. + + Lemma transl_spec_correct' : + forall l ctrl d_in d_out pc bb, + mfold_left (transf_seq_block ctrl) l (OK d_in) = OK d_out -> + In (pc, bb) l -> + exists pred' stmnt, transf_chained_block ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt) + /\ d_out ! pc = Some stmnt. + Proof. + induction l; [now inversion 2|]. + cbn -[mfold_left]. intros * HFOLD HIN. + exploit mfold_left_cons; eauto. + intros (x' & y' & HFOLD_EXP & TRANSFSEQ & HINV). inv HINV. + inversion_clear HIN as [HIN' | HIN']; eauto. + inversion HIN' as [HIN_CLEAR]; subst. clear HIN_CLEAR. + unfold transf_seq_block, Errors.bind2 in TRANSFSEQ. + repeat (destruct_match; try discriminate; []). + inversion TRANSFSEQ as []; subst. clear TRANSFSEQ. + exploit transl_spec_in_output; eauto. now rewrite PTree.gss. + Qed. + + Lemma transl_spec_correct : + forall ctrl d_in d_out pc bb c, + mfold_left (transf_seq_block ctrl) (PTree.elements c) (OK d_in) = OK d_out -> + c ! pc = Some bb -> + exists pred' stmnt, transf_chained_block ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt) + /\ d_out ! pc = Some stmnt. + Proof. intros. eapply transl_spec_correct'; eauto using PTree.elements_correct. Qed. + Lemma transl_step_state_correct : forall s f sp pc rs rs' m m' bb pr pr' state cf t, (fn_code f) ! pc = Some bb -> @@ -1545,7 +1759,27 @@ Opaque Mem.alloc. forall R1 : DHTL.state, match_states (GibleSubPar.State s f sp pc rs pr m) R1 -> exists R2 : DHTL.state, Smallstep.plus DHTL.step tge R1 t R2 /\ match_states state R2. - Proof. Admitted. + Proof. + intros * HIN HSTEP HCF * HMATCH. + exploit match_states_ok_transl; eauto. + intros (m0 & asr & asa & s' & HTRANSL & ?). subst. + unfold transl_module, Errors.bind, bind, ret in HTRANSL. + repeat (destruct_match; try discriminate; []). + exploit transl_spec_correct; eauto. + intros (pred' & stmnt0 & HTRANSF & HGET). + exploit step_exec_concat; eauto; intros HCONCAT. + exploit cf_in_bb_subparbb'; eauto. intros (exit_p & HINEXIT & HTRUTHY). + exploit transl_step_through_cfi'; eauto. intros (curr_p & _stmnt & HCFI). + exploit match_states_cf_states_translate_cfi; eauto. intros (s0 & f1 & sp0 & pc0 & rs0 & pr0 & m2 & HPARSTATE & HEXISTS). + exploit match_states_cf_events_translate_cfi; eauto; intros; subst. + inv HEXISTS. + - inv HPARSTATE. inv H. exploit transl_step_state_correct_instr_state; eauto. + constructor. intros (asr' & asa' & HSTMNTRUN & HMATCH'). + do 2 apply match_states_merge_empty_all in HMATCH'. + eexists. split; eauto. inv HMATCH. inv CONST. + apply Smallstep.plus_one. econstructor; eauto. + inv HTRANSL. auto. erewrite transl_module_ram_none by eauto. constructor. + inv HMATCH'. unfold state_st_wf in WF0. auto. Theorem transl_step_correct: forall (S1 : GibleSubPar.state) t S2, -- cgit