diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:16 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:44 +0100 |
commit | 7eeb169b982af90fac9873956e70d2c471555c31 (patch) | |
tree | 53a1a3a98bb5b1e38891ca77af17c10d852daea0 /src | |
parent | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (diff) | |
download | vericert-7eeb169b982af90fac9873956e70d2c471555c31.tar.gz vericert-7eeb169b982af90fac9873956e70d2c471555c31.zip |
Finish some proofs and remove unnecessary Admitted
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/GiblePargenproof.v | 48 | ||||
-rw-r--r-- | src/hls/GiblePargenproofCommon.v | 36 | ||||
-rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 2 | ||||
-rw-r--r-- | src/hls/GiblePargenproofEvaluable.v | 14 | ||||
-rw-r--r-- | src/hls/Predicate.v | 6 |
5 files changed, 74 insertions, 32 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index b774b48..ca2d8a2 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -941,12 +941,54 @@ have been evaluable. exists ts', step_cf_instr tge ts cf t ts' /\ match_states s' ts'. Proof. - (*| Proof Sketch: Trivial because of structural equality. |*) - - Admitted. + inversion 1; subst; clear H; inversion 1; subst; clear H. + - exploit find_function_translated; eauto; simplify. + econstructor; split. + + constructor; eauto using sig_transl_function. + + replace (rs' ## args) with (rs ## args). + now (repeat (constructor; auto)). + erewrite map_ext; auto. + - exploit find_function_translated; eauto; simplify. + econstructor; split. + + constructor; eauto using sig_transl_function. + unfold transl_function in TRANSL0. destruct_match; try discriminate. + inv TRANSL0. eauto. + + replace (rs' ## args) with (rs ## args). + now (repeat (constructor; auto)). + erewrite map_ext; auto. + - econstructor; split. + + econstructor; eauto using sig_transl_function. + eapply Events.eval_builtin_args_preserved; eauto. + eapply eval_builtin_args_eq; eauto. + auto. + + constructor; auto. + unfold regmap_setres; intros. destruct_match; auto. + subst. destruct (peq x0 x); subst. + * now rewrite ! PMap.gss. + * now rewrite ! PMap.gso by auto. + - econstructor; split. + + econstructor; eauto. eapply Op.eval_condition_lessdef; eauto. + replace (rs' ## args) with (rs ## args). + apply regs_lessdef_regs. + unfold regs_lessdef; auto. + erewrite map_ext; auto. + apply Mem.extends_refl. + + constructor; auto. + - econstructor; split. + + econstructor; eauto. now rewrite <- REG. + + constructor; auto. + - econstructor; split. + + econstructor; eauto. unfold transl_function in TRANSL0. + destruct_match; try discriminate. inv TRANSL0. eauto. + + replace (regmap_optget or Vundef rs') with (regmap_optget or Vundef rs). + constructor; auto. unfold regmap_optget. destruct_match; auto. + - econstructor; split. + + econstructor; eauto. + + constructor; auto. + Qed. Lemma match_states_stepBB : forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm', diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 0a09c23..345836f 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -309,38 +309,38 @@ Lemma prune_predicated_mutexcl : predicated_mutexcl y. Proof. unfold prune_predicated; intros. - Admitted. -#[local] Hint Resolve prune_predicated_mutexcl : mte. + Abort. +(*#[local] Hint Resolve prune_predicated_mutexcl : mte.*) Lemma app_predicated_mutexcl : forall A p (x: predicated A) y, predicated_mutexcl x -> predicated_mutexcl y -> predicated_mutexcl (app_predicated p x y). -Proof. Admitted. -#[local] Hint Resolve app_predicated_mutexcl : mte. +Proof. Abort. +(*#[local] Hint Resolve app_predicated_mutexcl : mte.*) Lemma seq_app_predicated_mutexcl : forall A B (f: predicated (A -> B)) y, predicated_mutexcl f -> predicated_mutexcl y -> predicated_mutexcl (seq_app f y). -Proof. Admitted. -#[local] Hint Resolve seq_app_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve seq_app_predicated_mutexcl : mte. *) Lemma all_predicated_mutexcl: forall f l, all_mutexcl f -> predicated_mutexcl (merge (list_translation l f)). -Proof. Admitted. -#[local] Hint Resolve all_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve all_predicated_mutexcl : mte. *) Lemma flap2_predicated_mutexcl : forall A B C (f: predicated (A -> B -> C)) x y, predicated_mutexcl f -> predicated_mutexcl (flap2 f x y). -Proof. Admitted. -#[local] Hint Resolve flap2_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve flap2_predicated_mutexcl : mte. *) Lemma all_mutexcl_set : forall f n r, @@ -370,11 +370,11 @@ Lemma all_mutexcl_maintained : Proof. destruct i; cbn -[seq_app]; intros; unfold Option.bind in *; repeat destr; inv H0. - trivial. - - apply prune_predicated_mutexcl in Heqo1; auto with mte. - - apply prune_predicated_mutexcl in Heqo0; auto with mte. - - apply prune_predicated_mutexcl in Heqo0; auto with mte. - apply app_predicated_mutexcl; auto with mte. - - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. - - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. - fold (get_forest x f). auto. -Qed. + (* - apply prune_predicated_mutexcl in Heqo1; auto with mte. *) + (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *) + (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *) + (* apply app_predicated_mutexcl; auto with mte. *) + (* - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. *) + (* - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. *) + (* fold (get_forest x f). auto. *) +Abort. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 91688a0..ee1c11c 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1114,7 +1114,7 @@ Section SEM_PRED_EXEC. End SEM_PRED_EXEC. Module HashExprNorm(HS: Hashable). - Module H := HashTree(HS). + Module H := hls.HashTree.HashTree(HS). Definition norm_tree: Type := PTree.t pred_op * H.hash_tree. diff --git a/src/hls/GiblePargenproofEvaluable.v b/src/hls/GiblePargenproofEvaluable.v index 84e7200..3bb9c66 100644 --- a/src/hls/GiblePargenproofEvaluable.v +++ b/src/hls/GiblePargenproofEvaluable.v @@ -284,7 +284,7 @@ Proof. unfold predicated_prod in *. exploit all_evaluable_map_and. 2: { eauto. } intros. 2: { eauto. } -Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *) +Abort. (* Requires simple lemma to prove, but this lemma is not needed. *) Lemma cons_pred_expr_evaluable : forall G (ctx: @ctx G) ps a b, @@ -294,8 +294,8 @@ Lemma cons_pred_expr_evaluable : Proof. unfold cons_pred_expr; intros. apply all_evaluable_predicated_map. - now apply all_evaluable_predicated_prod. -Qed. + (*now apply all_evaluable_predicated_prod.*) +Abort. Lemma fold_right_all_evaluable : forall G (ctx: @ctx G) ps n, @@ -303,10 +303,10 @@ Lemma fold_right_all_evaluable : all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n). Proof. induction n; cbn in *; intros. - - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod. - inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor. - - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable. -Qed. + - unfold cons_pred_expr. eapply all_evaluable_predicated_map. (*eapply all_evaluable_predicated_prod. + inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.*) admit. + - inv H. specialize (IHn H3). (*now eapply cons_pred_expr_evaluable.*) +Abort. Lemma merge_all_evaluable : forall G (ctx: @ctx G) ps, diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 99dfd77..86e992a 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -7,7 +7,7 @@ Require Import Coq.Logic.Decidable. Require Import vericert.common.Vericertlib. Require Import vericert.hls.Sat. -Require Import HashTree. +Require Import vericert.hls.HashTree. Declare Scope pred_op. @@ -603,7 +603,7 @@ Lemma stseytin_and_correct2 : sat_lit cur c <-> sat_lit p1 c /\ sat_lit p2 c. Proof. intros. split. intros. inv H1. unfold stseytin_and in *. - inv H0; try contradiction. Admitted. + inv H0; try contradiction. Abort. Lemma stseytin_or_correct : forall cur p1 p2 fm c, @@ -625,7 +625,7 @@ Lemma stseytin_or_correct2 : stseytin_or cur p1 p2 = fm -> sat_formula fm c -> sat_lit cur c <-> sat_lit p1 c \/ sat_lit p2 c. -Proof. Admitted. +Proof. Abort. Lemma xtseytin_correct : forall p next l n fm c, |