diff options
-rw-r--r-- | flake.nix | 23 | ||||
-rw-r--r-- | src/hls/GibleSeq.v | 15 | ||||
-rw-r--r-- | src/hls/IfConversionproof.v | 124 |
3 files changed, 125 insertions, 37 deletions
@@ -8,6 +8,9 @@ pkgs = nixpkgs.legacyPackages.x86_64-linux; ncoq = pkgs.coq_8_14; ncoqPackages = pkgs.coqPackages_8_14; + dpkgs = nixpkgs.legacyPackages.x86_64-darwin; + dncoq = dpkgs.coq_8_14; + dncoqPackages = dpkgs.coqPackages_8_14; in { devShell.x86_64-linux = pkgs.mkShell { buildInputs = with pkgs; @@ -29,5 +32,25 @@ python3Packages.sphinx_rtd_theme ]; }; + devShell.x86_64-darwin = dpkgs.mkShell { + buildInputs = with dpkgs; + [ dncoq + dune_2 + gcc + dncoq.ocaml + dncoq.ocamlPackages.findlib + dncoq.ocamlPackages.menhir + dncoq.ocamlPackages.ocamlgraph + dncoq.ocamlPackages.menhirLib + + dncoq.ocamlPackages.ocp-indent + dncoq.ocamlPackages.utop + + dncoqPackages.serapi + python3 + python3Packages.alectryon + python3Packages.sphinx_rtd_theme + ]; + }; }; } diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 9e2cfc5..2a04a55 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -84,6 +84,11 @@ Lemma step_instr_false : ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0). Proof. destruct a; unfold not; intros; inv H. Qed. +Lemma step_list_false : + forall A B ge sp a i0 s, + ~ step_list (@step_instr A B ge) sp s a (Iexec i0). +Proof. destruct a; unfold not; intros; inv H. Qed. + Lemma step_list2_false : forall A B ge l0 sp i c i0', ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0'). @@ -125,11 +130,11 @@ Qed. #[local] Notation "'mki'" := (mk_instr_state) (at level 1). Lemma exec_rbexit_truthy : - forall A B bb ge sp rs pr m rs' pr' m' pc', - @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) -> + forall A B bb ge sp rs pr m rs' pr' m' cf, + @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> exists p b1 b2, truthy pr' p - /\ bb = b1 ++ (RBexit p (RBgoto pc')) :: b2 + /\ bb = b1 ++ (RBexit p cf) :: b2 /\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')). Proof. induction bb; crush. @@ -184,9 +189,9 @@ Qed. Lemma append3 : forall A B l0 l1 sp ge s1 s2 s3, - step_list2 (step_instr ge) sp s1 l0 s2 -> + step_list2 (step_instr ge) sp s1 l0 (Iexec s2) -> @SeqBB.step A B ge sp s1 (l0 ++ l1) s3 -> - @SeqBB.step A B ge sp s2 l1 s3. + @SeqBB.step A B ge sp (Iexec s2) l1 s3. Proof. induction l0; crush. inv H. auto. inv H0. inv H. assert (i1 = (Iexec state')) by (eapply exec_determ; eauto). subst. eauto. diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index de44118..ca4d18b 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -133,6 +133,7 @@ Section CORRECTNESS. (* This can be improved with a recursive relation for a more general structure of the if-conversion proof. *) (IS_B: f.(fn_code)!pc = Some b) + (IS_TB: forall b', f.(fn_code)!pc0 = Some b' -> tf.(fn_code)!pc0 = if_conv_replace) (EXTRAP: sem_extrap tf pc0 sp (Iexec (mki rs p m)) (Iexec (mki rs0 p0 m0)) b) (SIM: step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)), match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0) @@ -282,9 +283,9 @@ Section CORRECTNESS. Proof. intros; simplify. do 3 econstructor; eauto. Qed. Lemma step_instr : - forall sp s s' a, - step_instr ge sp (Iexec s) a (Iexec s') -> - step_instr tge sp (Iexec s) a (Iexec s'). + forall sp s1 s2 a, + step_instr ge sp s1 a s2 -> + step_instr tge sp s1 a s2. Proof. inversion 1; subst; econstructor; eauto. - now rewrite <- eval_op_eq. @@ -292,12 +293,6 @@ Section CORRECTNESS. - now rewrite <- eval_addressing_eq. Qed. - Lemma step_instr_term : - forall sp s s' a cf, - Gible.step_instr ge sp (Iexec s) a (Iterm s' cf) -> - Gible.step_instr tge sp (Iexec s) a (Iterm s' cf). - Proof. inversion 1; subst; constructor; auto. Qed. - Lemma seqbb_eq : forall bb sp rs pr m rs' pr' m' cf, SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> @@ -306,7 +301,17 @@ Section CORRECTNESS. induction bb; crush; inv H. - econstructor; eauto. apply step_instr; eassumption. destruct state'. eapply IHbb; eauto. - - constructor; apply step_instr_term; auto. + - constructor; apply step_instr; auto. + Qed. + + Lemma step_list_2_eq : + forall bb sp a b, + step_list2 (Gible.step_instr ge) sp a bb b -> + step_list2 (Gible.step_instr tge) sp a bb b. + Proof. + induction bb; crush; inv H. + - econstructor; eauto. + - econstructor; eauto. now apply step_instr. Qed. Lemma fn_all_eq : @@ -365,16 +370,36 @@ Section CORRECTNESS. Qed. Lemma exec_if_conv : - forall bb sp rs pr m rs' pr' m' pc' b' tb, - SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') (RBgoto pc')) -> - if_conv_replace pc' b' bb tb -> - exists p b rb, - tb = b ++ (map (map_if_convert p) b') ++ rb - /\ SeqBB.step ge sp (Iexec (mki rs pr m)) b (Iexec (mki rs' pr' m')). + forall A B ge sp pc' b' tb i i' x0 x x1, + step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') -> + if_conv_replace pc' b' (x0 ++ RBexit x (RBgoto pc') :: x1) tb -> + exists b rb, + tb = b ++ (map (map_if_convert x) b') ++ rb + /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). + Proof. + Admitted. + + Lemma exec_if_conv2 : + forall A B ge sp pc' b' tb i i' x0 x x1 cf, + step_list2 (@Gible.step_instr A B ge) sp (Iexec i) x0 (Iexec i') -> + cf <> RBgoto pc' -> + if_conv_replace pc' b' (x0 ++ RBexit x cf :: x1) tb -> + exists b rb, + tb = b ++ RBexit x cf :: rb + /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof. + Admitted. + + Lemma map_truthy_step: + forall sp rs' m' pr' x b' i c, + truthy pr' x -> + SeqBB.step tge sp (Iexec (mki rs' pr' m')) b' (Iterm i c) -> + SeqBB.step tge sp (Iexec (mki rs' pr' m')) (map (map_if_convert x) b') (Iterm i c). + Proof. + intros * H1 H2. Admitted. - Lemma temp2: + Lemma match_none_correct : forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk', (fn_code f) ! pc = Some bb -> SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> @@ -393,19 +418,53 @@ Section CORRECTNESS. do 3 econstructor. apply plus_one. econstructor; eauto. apply seqbb_eq; eauto. eauto. - simplify. - destruct (cf_dec cf pc'); subst. inv H1. - exploit exec_if_conv; eauto; simplify. - exploit exec_rbexit_truthy; eauto; simplify. - apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m). - simplify; try (unfold ltof; auto). apply star_refl. - constructor; auto. unfold sem_extrap; simplify. - - Lemma step_cf_matches : - forall b s cf t s' ts, - step_cf_instr ge s cf t s' -> - match_states b s ts -> - exists b' ts', step_cf_instr tge ts cf t ts' /\ match_states b' s' ts'. - Proof. Admitted. + destruct (cf_dec cf pc'); subst. + + inv H1. + exploit exec_rbexit_truthy; eauto; simplify. + exploit exec_if_conv; eauto; simplify. + apply sim_star. exists (Some b'). exists (State stk' (transf_function f) sp pc rs pr m). + simplify; try (unfold ltof; auto). apply star_refl. + constructor; auto. unfold sem_extrap; simplify. + destruct out_s. exfalso; eapply step_list_false; eauto. + apply append. exists (mki rs' pr' m'). split. + eapply step_list_2_eq; eauto. + apply append2. eapply map_truthy_step; eauto. + econstructor; eauto. constructor; auto. + + exploit exec_rbexit_truthy; eauto; simplify. + exploit exec_if_conv2; eauto; simplify. + exploit step_cf_eq; eauto; simplify. + apply sim_plus. exists None. exists x4. + split. apply plus_one. econstructor; eauto. + apply append. exists (mki rs' pr' m'). split; auto. + apply step_list_2_eq; auto. + constructor. constructor; auto. auto. + Qed. + + Lemma match_some_correct: + forall t s1' s f sp pc rs m pr rs' m' bb pr' cf stk' b0 pc1 rs1 p0 m1, + step ge (State s f sp pc rs pr m) t s1' -> + (fn_code f) ! pc = Some bb -> + SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) -> + step_cf_instr ge (State s f sp pc rs' pr' m') cf t s1' -> + Forall2 match_stackframe s stk' -> + (fn_code f) ! pc = Some b0 -> + sem_extrap (transf_function f) pc1 sp (Iexec (mki rs pr m)) (Iexec (mki rs1 p0 m1)) b0 -> + step ge (State s f sp pc1 rs1 p0 m1) E0 (State s f sp pc rs pr m) -> + exists b' s2', + (plus step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' \/ + star step tge (State stk' (transf_function f) sp pc1 rs1 p0 m1) t s2' /\ + ltof (option SeqBB.t) measure b' (Some b0)) /\ match_states b' s1' s2'. + Proof. + intros * H H0 H1 H2 STK IS_B EXTRAP SIM. + rewrite IS_B in H0; simplify. + exploit step_cf_eq; eauto; simplify. + apply sim_plus. + exists None. exists x. + split; auto. + unfold sem_extrap in *. + inv SIM. + pose proof (transf_spec_correct f pc1) as X. inv X. + eapply plus_two. econstructor; eauto. Lemma transf_correct: forall s1 t s1', @@ -418,8 +477,9 @@ Section CORRECTNESS. Proof using TRANSL. inversion 1; subst; simplify; match goal with H: context[match_states] |- _ => inv H end. - - admit. - - eauto using temp2. Admitted. + - + - eauto using match_none_correct. + - Admitted. (* - *) |