diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 19:11:52 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-11 19:11:52 +0000 |
| commit | e9de87c29c446a4e0169f55131a678535630ff18 (patch) | |
| tree | b923b8e5fdd483db7df217a1bd3d2e543a3f99da /src | |
| parent | 489b93c3e257e37f45c1f0eafeff950b97249c3f (diff) | |
| download | vericert-e9de87c29c446a4e0169f55131a678535630ff18.tar.gz vericert-e9de87c29c446a4e0169f55131a678535630ff18.zip | |
Add proof of empty items
Proof that correct items are returned from an empty forest.
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/Scheduleoracle.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 2c60e96..1625238 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -362,6 +362,16 @@ Proof. congruence. Qed. +Definition empty : forest := Rtree.empty _. + +Lemma get_empty: + forall r, empty#r = Ebase r. +Proof. + intros r. unfold get_forest. + destruct (Rtree.get r empty) eqn:Heq; auto. + rewrite Rtree.gempty in Heq. discriminate. +Qed. + (*| We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |