diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Abstr.v | 178 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 48 | ||||
-rw-r--r-- | src/hls/HashTree.v | 92 |
3 files changed, 261 insertions, 57 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index ec45007..f332905 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -753,7 +753,12 @@ Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := let (p2, h') := HN.encode_expression 1%positive pe2 h in equiv_check p1 p2. +Definition pred_eexpr_eqb: forall pe1 pe2: pred_eexpr, + {pe1 = pe2} + {pe1 <> pe2}. +Admitted. + Definition beq_pred_eexpr (pe1 pe2: pred_eexpr) : bool := + if pred_eexpr_eqb pe1 pe2 then true else let (p1, h) := EHN.encode_expression 1%positive pe1 (PTree.empty _) in let (p2, h') := EHN.encode_expression 1%positive pe2 h in equiv_check p1 p2. @@ -912,13 +917,23 @@ Lemma norm_expression_sem_pred2 : sem_pred_expr sem ctx pe v. Proof. Admitted.*) +Definition pred_expr_eqb: forall pe1 pe2: pred_expr, + {pe1 = pe2} + {pe1 <> pe2}. +Admitted. + Definition beq_pred_expr (pe1 pe2: pred_expr) : bool := + if pred_expr_eqb pe1 pe2 then true else let (np1, h) := HN.norm_expression 1 pe1 (PTree.empty _) in let (np2, h') := HN.norm_expression 1 pe2 h in forall_ptree (tree_equiv_check_el np2) np1 && forall_ptree (tree_equiv_check_None_el np1) np2. +Definition pred_pexpr_eqb: forall pe1 pe2: pred_pexpr, + {pe1 = pe2} + {pe1 <> pe2}. +Admitted. + Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool := + if pred_pexpr_eqb pe1 pe2 then true else let (np1, h) := hash_predicate 1 pe1 (PTree.empty _) in let (np2, h') := hash_predicate 1 pe2 h in equiv_check np1 np2. @@ -1535,3 +1550,166 @@ Lemma forest_pred_gso2 : r <> w -> (forest_preds (f #p w <- p)) ! r = (forest_preds f) ! r. Proof. intros. unfold set_forest_p. simpl. now rewrite PTree.gso by auto. Qed. + +Inductive state_lessdef : instr_state -> instr_state -> Prop := + state_lessdef_intro : + forall rs1 rs2 ps1 ps2 m1, + (forall x, rs1 !! x = rs2 !! x) -> + (forall x, ps1 !! x = ps2 !! x) -> + state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1). + +Lemma state_lessdef_refl x : state_lessdef x x. +Proof. destruct x; constructor; auto. Qed. + +Lemma state_lessdef_symm x y : state_lessdef x y -> state_lessdef y x. +Proof. destruct x; destruct y; inversion 1; subst; simplify; constructor; auto. Qed. + +Lemma state_lessdef_trans : + forall a b c, + state_lessdef a b -> + state_lessdef b c -> + state_lessdef a c. +Proof. + inversion 1; inversion 1; subst; simplify. + constructor; eauto; intros. rewrite H0. auto. +Qed. + +#[global] Instance Equivalence_state_lessdef : Equivalence state_lessdef := + { Equivalence_Reflexive := state_lessdef_refl; + Equivalence_Symmetric := state_lessdef_symm; + Equivalence_Transitive := state_lessdef_trans; + }. + +Section CORRECT. + +Context (prog: GibleSeq.program) (tprog : GiblePar.program). +Context (sp: val). + +Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. +Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. + +Definition mkctx a := mk_ctx a sp ge. + +Lemma sem_pred_exec_beq_correct : + forall A B (sem: ctx -> A -> B -> Prop) a b i p r, + PTree.beq beq_pred_pexpr a b = true -> + sem_pred_expr a sem (mkctx i) p r -> + sem_pred_expr b sem (mkctx i) p r. +Proof. Admitted. + +Lemma sem_pred_exec_beq_correct2 : + forall A B (sem: ctx -> A -> B -> Prop) a i ti p r, + state_lessdef i ti -> + sem_pred_expr a sem (mkctx i) p r -> + sem_pred_expr a sem (mkctx ti) p r. +Proof. Admitted. + +Lemma sem_expr_beq_correct : + forall pt i a b v, + beq_pred_expr a b = true -> + sem_pred_expr pt sem_value (mkctx i) a v -> + sem_pred_expr pt sem_value (mkctx i) b v. +Proof. + induction a. + - intros. inv H0. + unfold beq_pred_expr; intros. destruct_match; subst; auto. + repeat destruct_match. simplify. clear Heqs. clear n. + inv H0. + +Lemma sem_expr_beq_correct_mem : + forall pt i a b v, + beq_pred_expr a b = true -> + sem_pred_expr pt sem_mem (mkctx i) a v -> + sem_pred_expr pt sem_mem (mkctx i) b v. +Proof. Admitted. + +Lemma sem_expr_beq_correct_exit : + forall pt i a b v, + beq_pred_eexpr a b = true -> + sem_pred_expr pt sem_exit (mkctx i) a v -> + sem_pred_expr pt sem_exit (mkctx i) b v. +Proof. Admitted. + +Lemma sem_eexpr_beq_correct : + forall pt i a b v, + beq_pred_eexpr a b = true -> + sem_pred_expr pt sem_exit (mkctx i) a v -> + sem_pred_expr pt sem_exit (mkctx i) b v. +Proof. Admitted. + +Lemma sem_pexpr_state_lessdef : + forall i i' a v, + state_lessdef i i' -> + sem_pexpr (mkctx i) a v -> + sem_pexpr (mkctx i') a v. +Proof. Admitted. + +Lemma sem_pexpr_beq_correct : + forall i p1 p2 b, + beq_pred_pexpr p1 p2 = true -> + sem_pexpr (mkctx i) p1 b -> + sem_pexpr (mkctx i) p2 b. +Proof. Admitted. + +Lemma tree_beq_pred_pexpr : + forall a b x, + RTree.beq beq_pred_pexpr (forest_preds a) (forest_preds b) = true -> + beq_pred_pexpr a #p x b #p x = true. +Proof. + intros. unfold "#p". unfold get_forest_p'. + apply PTree.beq_correct with (x := x) in H. + destruct_match; destruct_match; auto. + unfold beq_pred_pexpr. destruct_match; auto. +Qed. + +Lemma tree_beq_pred_expr : + forall a b x, + RTree.beq beq_pred_expr (forest_regs a) (forest_regs b) = true -> + beq_pred_expr a #r x b #r x = true. +Proof. + intros. unfold "#r". + apply PTree.beq_correct with (x := (R_indexed.index x)) in H. + unfold RTree.get in *. + destruct_match; destruct_match; auto. + unfold beq_pred_expr. destruct_match; auto. +Qed. + +Lemma abstr_check_correct : + forall i i' a b cf ti, + check a b = true -> + sem (mkctx i) a (i', cf) -> + state_lessdef i ti -> + exists ti', sem (mkctx ti) b (ti', cf) /\ state_lessdef i' ti'. +Proof. + intros. unfold check in H. simplify. + inv H0. inv H6. inv H7. + eexists. split. { + constructor. + - constructor. intros. + eapply sem_pred_exec_beq_correct; eauto. + eapply sem_pred_exec_beq_correct2; eauto. + eapply sem_expr_beq_correct. eapply tree_beq_pred_expr; eauto. + eauto. + - constructor. intros. apply sem_pexpr_beq_correct with (p1 := a #p x). + apply tree_beq_pred_pexpr; auto. + apply sem_pexpr_state_lessdef with (i := i); auto. + - eapply sem_pred_exec_beq_correct; eauto. + eapply sem_pred_exec_beq_correct2; eauto. + eapply sem_expr_beq_correct_mem. eapply tree_beq_pred_expr; eauto. + eauto. + - eapply sem_pred_exec_beq_correct; eauto. + eapply sem_pred_exec_beq_correct2; eauto. + eapply sem_expr_beq_correct_exit; eauto. + } + constructor; auto. +Qed. + +(*| +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. +|*) + +End CORRECT. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 8c494e0..9c85d54 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -165,35 +165,6 @@ Proof. - rewrite forest_pred_gso2 in H1 by auto; eauto. Qed. -Inductive state_lessdef : instr_state -> instr_state -> Prop := - state_lessdef_intro : - forall rs1 rs2 ps1 ps2 m1, - (forall x, rs1 !! x = rs2 !! x) -> - (forall x, ps1 !! x = ps2 !! x) -> - state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1). - -Lemma state_lessdef_refl x : state_lessdef x x. -Proof. destruct x; constructor; auto. Qed. - -Lemma state_lessdef_symm x y : state_lessdef x y -> state_lessdef y x. -Proof. destruct x; destruct y; inversion 1; subst; simplify; constructor; auto. Qed. - -Lemma state_lessdef_trans : - forall a b c, - state_lessdef a b -> - state_lessdef b c -> - state_lessdef a c. -Proof. - inversion 1; inversion 1; subst; simplify. - constructor; eauto; intros. rewrite H0. auto. -Qed. - -#[global] Instance Equivalence_state_lessdef : Equivalence state_lessdef := - { Equivalence_Reflexive := state_lessdef_refl; - Equivalence_Symmetric := state_lessdef_symm; - Equivalence_Transitive := state_lessdef_trans; - }. - Definition check_dest i r' := match i with | RBop p op rl r => (r =? r')%positive @@ -2449,25 +2420,6 @@ execution, the values in the register map do not continue to change. exists x0. auto. Qed. - Lemma abstr_check_correct : - forall sp i i' a b cf ti, - check a b = true -> - sem (mk_ctx i sp ge) a (i', cf) -> - state_lessdef i ti -> - exists ti', sem (mk_ctx ti sp ge) b (ti', cf) - /\ state_lessdef i' ti'. - 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', abstract_sequence x = Some x' -> diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index 86bc598..7387401 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -163,6 +163,33 @@ Module HashTree(H: Hashable). (nkey, PTree.set nkey e h) end. + Definition hash_value2 (max: hash) (e: t * t) (h: hash_tree): (hash * hash) * hash_tree := + let (e1, e2) := e in + let (v1, h1) := hash_value max e1 h in + let (v2, h2) := hash_value max e2 h1 in + ((v1, v2), h2). + + Definition hash_value3 (max: hash) (e: t * t * t) (h: hash_tree): (hash * hash * hash) * hash_tree := + let '(e1, e2, e3) := e in + let (v1, h1) := hash_value max e1 h in + let (v2, h2) := hash_value max e2 h1 in + let (v3, h3) := hash_value max e3 h2 in + ((v1, v2, v3), h3). + + Definition hash_value4 (max: hash) (e: t * t * t * t) (h: hash_tree): (hash * hash * hash * hash) * hash_tree := + let '(e1, e2, e3, e4) := e in + let (v1, h1) := hash_value max e1 h in + let (v2, h2) := hash_value max e2 h1 in + let (v3, h3) := hash_value max e3 h2 in + let (v4, h4) := hash_value max e4 h3 in + ((v1, v2, v3, v4), h4). + + Definition hash_list (max: hash) (e: list t) (h: hash_tree): list hash * hash_tree := + fold_left (fun s e => + let (i, h') := hash_value max e (snd s) in + (fst s ++ i::nil, h') + ) e (nil, h). + Definition wf_hash_table h_tree := forall x c, h_tree ! x = Some c -> find_tree c h_tree = Some x. @@ -458,14 +485,28 @@ Module HashTree(H: Hashable). Module HashMonad := Statemonad(HashState). -End HashTree. - -Definition gt_1 {A} h := - forall x (y: A), h ! x = Some y -> 1 < x. - -Module HashTreeProperties (Import H: Hashable). - - Module Import HT := HashTree(H). + Definition gt_1 h := + forall x (y: t), h ! x = Some y -> 1 < x. + + Definition match_one (f: PTree.t t) lf := + forall y z, lf ! y = Some z -> f ! y = Some z. + + Definition match_all (f: PTree.t t) lf := + Forall (match_one f) lf. + + Lemma match_one_refl : + forall x, match_one x x. + Proof. unfold match_one; auto. Qed. + + Instance match_one_Reflexive : Reflexive match_one. + Proof. unfold Reflexive. auto using match_one_refl. Qed. + + Lemma match_one_trans : + forall x y z, match_one x y -> match_one y z -> match_one x z. + Proof. unfold match_one; auto. Qed. + + Instance match_one_Transitive : Transitive match_one. + Proof. unfold Transitive. eauto using match_one_trans. Qed. Lemma hash_value_gt : forall max v h, @@ -478,4 +519,37 @@ Module HashTreeProperties (Import H: Hashable). cbn [snd] in *. rewrite PTree.gso in H0; eauto. Qed. -End HashTreeProperties. + Lemma hash_value_in : + forall max f ht h ht', + hash_value max f ht = (h, ht') -> + ht' ! h = Some f. + Proof. + unfold hash_value. intros. + destruct_match. + - inv H. eapply find_tree_correct; eauto. + - inv H. rewrite PTree.gss. auto. + Qed. + + Lemma match_one_hash_value : + forall max x h h' y y', + hash_value max y h = (y', h') -> + match_one x h' -> + match_one x h. + Proof. + unfold match_one. + intros. + eapply H0; eauto. + eapply hash_constant; eauto. + Qed. + + Lemma hash_value_eq : + forall h v ht h', + wf_hash_table ht -> + ht ! h' = Some v -> + hash_value h v ht = (h', ht). + Proof. + intros. unfold hash_value. unfold wf_hash_table in *. apply H in H0. + rewrite H0; auto. + Qed. + +End HashTree. |