diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-02-12 19:33:19 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-02-12 19:33:19 +0000 |
| commit | 6452ba3029054ef26fc12cde7e05861bd58fdacb (patch) | |
| tree | 33ce03c795a886af27f982a88bdd74e5dad451e5 /src/hls/Gible.v | |
| parent | e5db7d1259c32a886182c21201e6db3d567e7f96 (diff) | |
| download | vericert-6452ba3029054ef26fc12cde7e05861bd58fdacb.tar.gz vericert-6452ba3029054ef26fc12cde7e05861bd58fdacb.zip | |
Finish sem_update_instr finally
Diffstat (limited to 'src/hls/Gible.v')
| -rw-r--r-- | src/hls/Gible.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 0603269..cc35640 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -158,6 +158,20 @@ Definition predset := PMap.t bool. Definition eval_predf (pr: predset) (p: pred_op) := sat_predicate p (fun x => pr !! (Pos.of_nat x)). +Lemma sat_pred_agree0 : + forall a b p, + (forall x, x <> 0%nat -> a x = b x) -> + sat_predicate p a = sat_predicate p b. +Proof. + induction p; auto; intros. + - destruct p. cbn. assert (Pos.to_nat p <> 0%nat) by lia. + apply H in H0. now rewrite H0. + - specialize (IHp1 H). specialize (IHp2 H). + cbn. rewrite IHp1. rewrite IHp2. auto. + - specialize (IHp1 H). specialize (IHp2 H). + cbn. rewrite IHp1. rewrite IHp2. auto. +Qed. + #[global] Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. Proof. @@ -190,6 +204,26 @@ Proof. erewrite IHp1; try eassumption; erewrite IHp2; eauto. Qed. +Lemma eval_predf_not_PredIn : + forall ps p b op, + ~ PredIn p op -> + eval_predf (ps # p <- b) op = eval_predf ps op. +Proof. + induction op; auto. + - intros. destruct p0. cbn. rewrite Pos2Nat.id. + destruct (peq p p0); subst. + { exfalso; apply H; constructor. } + rewrite Regmap.gso; auto. + - intros. cbn. unfold eval_predf in *. rewrite IHop1. + rewrite IHop2. auto. + unfold not; intros; apply H; constructor; tauto. + unfold not; intros; apply H; constructor; tauto. + - intros. cbn. unfold eval_predf in *. rewrite IHop1. + rewrite IHop2. auto. + unfold not; intros; apply H; constructor; tauto. + unfold not; intros; apply H; constructor; tauto. +Qed. + Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) |