-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathTopoSort.v
95 lines (82 loc) · 3.74 KB
/
TopoSort.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
(* *****************************************************************)
(* *)
(* Verified polyhedral AST generation *)
(* *)
(* Nathanaël Courant, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* *****************************************************************)
Require Import List.
Require Import Permutation.
Require Import Arith.
Require Import Misc.
Require Import Vpl.Impure.
Require Import Vpl.Debugging.
Require Import ImpureAlarmConfig.
Parameter topo_sort_untrusted : list (list bool) -> imp (list nat).
Definition check_toposort cstr out :=
if Permutation_dec _ Nat.eq_dec (n_range (length cstr)) out then
forallb (fun k2 => forallb (fun k1 => negb (nth (nth k2 out 0%nat) (nth (nth k1 out 0%nat) cstr nil) true)) (n_range k2)) (n_range (length cstr))
else
failwith CERT "topo_sort: not permutation" false.
Lemma check_toposort_correct_permutation :
forall cstr out, check_toposort cstr out = true -> Permutation (n_range (length cstr)) out.
Proof.
intros cstr out H. unfold check_toposort in H.
unfold Debugging.failwith in *.
destruct Permutation_dec; [auto|congruence].
Qed.
Lemma check_toposort_correct_sorted :
forall cstr out, check_toposort cstr out = true ->
forall k1 k2, (k1 < k2 < length cstr)%nat -> nth (nth k2 out 0%nat) (nth (nth k1 out 0%nat) cstr nil) true = false.
Proof.
intros cstr out H k1 k2 [Hk1 Hk2].
unfold check_toposort, Debugging.failwith in H. destruct Permutation_dec; [|congruence].
rewrite <- negb_true_iff.
rewrite forallb_forall in H. rewrite <- n_range_in in Hk2.
specialize (H k2 Hk2); rewrite forallb_forall in H. rewrite <- n_range_in in Hk1.
apply H; auto.
Qed.
Definition topo_sort cstr :=
BIND out <- topo_sort_untrusted cstr -;
if check_toposort cstr out then
pure out
else
failwith CERT "topo_sort: not good sort" (alarm "topo_sort verification failed" out).
Lemma topo_sort_permutation :
forall cstr, WHEN out <- topo_sort cstr THEN Permutation (n_range (length cstr)) out.
Proof.
intros cstr out Hout.
bind_imp_destruct Hout out1 Hout1.
destruct (check_toposort cstr out1) eqn:Hcheck.
- apply mayReturn_pure in Hout; rewrite Hout in *. apply check_toposort_correct_permutation; auto.
- apply mayReturn_alarm in Hout; tauto.
Qed.
Lemma topo_sort_sorted :
forall cstr, WHEN out <- topo_sort cstr THEN forall k1 k2, (k1 < k2 < length cstr)%nat ->
nth (nth k2 out 0%nat) (nth (nth k1 out 0%nat) cstr nil) true = false.
Proof.
intros cstr out Hout.
bind_imp_destruct Hout out1 Hout1.
destruct (check_toposort cstr out1) eqn:Hcheck.
- apply mayReturn_pure in Hout; rewrite Hout in *. apply check_toposort_correct_sorted; auto.
- apply mayReturn_alarm in Hout; tauto.
Qed.
Lemma topo_sort_indices_correct :
forall cstr, WHEN out <- topo_sort cstr THEN forall i, In i out -> (i < length cstr)%nat.
Proof.
intros cstr out Hout i Hin.
rewrite <- n_range_in.
eapply Permutation_in; [symmetry; apply topo_sort_permutation|]; eauto.
Qed.
Lemma topo_sort_length :
forall cstr, WHEN out <- topo_sort cstr THEN length out = length cstr.
Proof.
intros cstr out Hout.
erewrite Permutation_length; [|symmetry; eapply topo_sort_permutation; eauto].
rewrite n_range_length; eauto.
Qed.