diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 72 |
1 files changed, 52 insertions, 20 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index cf35abad..0cbc46e6 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -380,7 +380,7 @@ Global Opaque hSstore. Local Hint Resolve hSstore_correct: wlp. Definition hrs_sreg_get (hrs: ristate) r: ?? sval := - match PTree.get r hrs with + match PTree.get r (ris_sreg hrs) with | None => if ris_input_init hrs then hSinput r else hSundef | Some sv => RET sv end. @@ -629,15 +629,15 @@ Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval := match (ris_input_init hrs), sv with | true, Sinput r' _ => if Pos.eq_dec r r' - then PTree.remove r' hrs - else PTree.set r sv hrs + then PTree.remove r' (ris_sreg hrs) + else PTree.set r sv (ris_sreg hrs) | false, Sundef _ => - PTree.remove r hrs - | _, _ => PTree.set r sv hrs + PTree.remove r (ris_sreg hrs) + | _, _ => PTree.set r sv (ris_sreg hrs) end. Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx: - sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0). + sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv (ris_sreg hrs))) r0). Proof. unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl. destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto. @@ -703,10 +703,8 @@ Lemma hrs_init_correct: Proof. unfold hrs_init, sis_init; wlp_simplify. econstructor; simpl in *; eauto. - + split; destruct 1; econstructor; simpl in *; + split; destruct 1; econstructor; simpl in *; try rewrite H; try congruence; trivial. - + destruct 1; simpl in *. unfold ris_sreg_get; simpl. - intros; rewrite PTree.gempty; eauto. Qed. Local Hint Resolve hrs_init_correct: wlp. Global Opaque hrs_init. @@ -879,8 +877,7 @@ Proof. - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption. - rewrite OK_EQUIV; constructor; inv X; assumption. * intros X; inv X; simpl; apply MEM_EQ; constructor; auto. - * simpl. unfold ris_sreg_get. - intros;rewrite PTree.gempty. simpl; auto. + * simpl. unfold ris_sreg_get. auto. + constructor. * erewrite ok_hrset_red_sreg; eauto. inv H2. rewrite <- OK_EQUIV. @@ -1246,21 +1243,56 @@ Hint Resolve option_eq_check_correct:wlp. Import PTree. -Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit := +Fixpoint PTree_eq_check' {A} (d1 d2: PTree.tree' A): ?? unit := + match d1, d2 with + | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2 + | Node010 x1, Node010 x2 => + phys_check x1 x2 "PTree_eq_check': data physically differ" + | Node011 x1 r1, Node011 x2 r2 => + phys_check x1 x2 "PTree_eq_check': data physically differ" ;; + PTree_eq_check' r1 r2 + | Node100 l1, Node100 l2 => PTree_eq_check' l1 l2 + | Node101 l1 r1, Node101 l2 r2 => + PTree_eq_check' l1 l2 ;; + PTree_eq_check' r1 r2 + | Node110 l1 x1, Node110 l2 x2 => + phys_check x1 x2 "PTree_eq_check': data physically differ" ;; + PTree_eq_check' l1 l2 + | Node111 l1 x1 r1, Node111 l2 x2 r2 => + phys_check x1 x2 "PTree_eq_check': data physically differ" ;; + PTree_eq_check' l1 l2 ;; + PTree_eq_check' r1 r2 + | _, _ => FAILWITH "PTree_eq_check': different shapes" + end. + +Lemma PTree_eq_check'_correct A : forall (d1 d2: PTree.tree' A), + WHEN PTree_eq_check' d1 d2 ~> _ THEN d1 = d2. +Proof. + induction d1; destruct d2; cbn; wlp_simplify; try congruence. +Qed. + +Definition PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit := match d1, d2 with - | Leaf, Leaf => RET tt - | Node l1 o1 r1, Node l2 o2 r2 => - option_eq_check o1 o2;; - PTree_eq_check l1 l2;; - PTree_eq_check r1 r2 - | _, _ => FAILWITH "PTree_eq_check: some key is absent" + | Empty, Empty => RET tt + | Nodes m1, Nodes m2 => PTree_eq_check' m1 m2 + | _, _ => FAILWITH "PTree_eq_check: empty vs nonempty" end. +Lemma PTree_eq_check_correct' A : forall (d1 d2: PTree.tree A), + WHEN PTree_eq_check d1 d2 ~> _ THEN d1 = d2. +Proof. + Local Hint Resolve PTree_eq_check'_correct: wlp. + destruct d1 as [ | m1]; destruct d2 as [ | m2]; cbn; wlp_simplify. + congruence. +Qed. + Lemma PTree_eq_check_correct A d1: forall (d2: t A), WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2. Proof. - induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; - wlp_simplify. destruct x; simpl; auto. + Local Hint Resolve PTree_eq_check_correct': wlp. + intros. + wlp_simplify. + congruence. Qed. Global Opaque PTree_eq_check. Local Hint Resolve PTree_eq_check_correct: wlp. |