diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-11 16:11:22 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-11 16:11:22 +0100 |
| commit | b66c1d482292c15e3d7907262cf1c94edabdd40e (patch) | |
| tree | f9f8040471ab1e32eacb57e29a86838e7f8f86ae /mppa_k1c/PostpassScheduling.v | |
| parent | bc162e5d2be64ea3f552a61155211c2d6a1beb76 (diff) | |
| download | compcert-kvx-b66c1d482292c15e3d7907262cf1c94edabdd40e.tar.gz compcert-kvx-b66c1d482292c15e3d7907262cf1c94edabdd40e.zip | |
Proving verified_schedule_size axiom
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 69 |
1 files changed, 58 insertions, 11 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 11e53a5d..5fec35fb 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -82,19 +82,66 @@ Fixpoint concat_all (lbb: list bblock) : res bblock := Definition verify_schedule (bb bb' : bblock) : res unit := OK tt.
-Program Definition verified_schedule (bb : bblock) : res (list bblock) :=
- let bb' := {| header := nil; body := body bb; exit := exit bb |} in
- let lbb := schedule bb' in
- do tbb <- concat_all lbb;
- do check <- verify_schedule bb' tbb;
- match (head lbb) with
- | None => Error (msg "PostpassScheduling.verified_schedule: empty schedule")
- | Some fst => OK ({| header := header bb; body := body fst; exit := exit fst |} :: tail lbb)
- end.
+Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").
+
+Lemma verify_size_size:
+ forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.
+Proof.
+ intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.
+ apply Z.eqb_eq. assumption.
+Qed.
+
+Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
Next Obligation.
destruct bb; simpl. assumption.
-Qed. Next Obligation.
- destruct fst; simpl. assumption.
+Qed.
+
+Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
+Next Obligation.
+ destruct bb; simpl. assumption.
+Qed.
+
+Lemma stick_header_size:
+ forall h bb, size (stick_header h bb) = size bb.
+Proof.
+ intros. destruct bb. unfold stick_header. simpl. reflexivity.
+Qed.
+
+Definition stick_header_code (h : list label) (lbb : list bblock) :=
+ match (head lbb) with
+ | None => Error (msg "PostpassScheduling.stick_header: empty schedule")
+ | Some fst => OK ((stick_header h fst) :: tail lbb)
+ end.
+
+Lemma hd_tl_size:
+ forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).
+Proof.
+ destruct lbb.
+ - intros. simpl in H. discriminate.
+ - intros. simpl in H. inv H. simpl. reflexivity.
+Qed.
+
+Lemma stick_header_code_size:
+ forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.
+Proof.
+ intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.
+ inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.
+Qed.
+
+Definition verified_schedule (bb : bblock) : res (list bblock) :=
+ let bb' := no_header bb in
+ let lbb := schedule bb' in
+ do tbb <- concat_all lbb;
+ do sizecheck <- verify_size bb lbb;
+ do schedcheck <- verify_schedule bb' tbb;
+ stick_header_code (header bb) lbb.
+
+Lemma verified_schedule_size:
+ forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.
+Proof.
+ intros. monadInv H. erewrite <- stick_header_code_size; eauto.
+ apply verify_size_size.
+ destruct x0; try discriminate. assumption.
Qed.
Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
|