blob: 33376c19d3955f68641f5c4c78f5b30c29114b5f (
plain)
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(** Extension of Coq language with generic loops. *)
Require Export ImpIO.
Import Notations.
Local Open Scope impure.
(** While-loop iterations *)
Axiom loop: forall {A B}, A * (A -> ?? (A+B)) -> ?? B.
Extract Constant loop => "ImpLoopOracles.loop".
Section While_Loop.
(** Local Definition of "while-loop-invariant" *)
Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'.
Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false}
:= loop (A:={s | I s0 -> I s})
(s0,
fun s =>
match (cond s) with
| true =>
DO s' <~ mk_annot (body s) ;;
RET (inl (A:={s | I s0 -> I s }) s')
| false =>
RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s)
end).
Obligation 2.
unfold wli, wlp in * |-; eauto.
Qed.
Extraction Inline while.
End While_Loop.
Section Loop_Until_None.
(** useful to demonstrate a UNSAT property *)
(** Local Definition of "loop-until-None-invariant" *)
Let luni {S} (body: S -> ?? (option S)) (I: S -> Prop) := forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end.
Program Definition loop_until_None {S} body (I: S -> Prop | luni body I) s0: ?? ~(I s0)
:= loop (A:={s | I s0 -> I s})
(s0,
fun s =>
DO s' <~ mk_annot (body s) ;;
match s' with
| Some s1 => RET (inl (A:={s | I s0 -> I s }) s1)
| None => RET (inr (B:=~(I s0)) _)
end).
Obligation 2.
refine (H2 s _ _ H0). auto.
Qed.
Obligation 3.
intros X; refine (H1 s _ _ H). auto.
Qed.
Extraction Inline loop_until_None.
End Loop_Until_None.
(*********************************************)
(* A generic fixpoint from an equality test *)
Record answ {A B: Type} {R: A -> B -> Prop} := {
input: A ;
output: B ;
correct: R input output
}.
Arguments answ {A B}.
Definition msg: pstring := "wapply fails".
Definition beq_correct {A} (beq: A -> A -> ?? bool) :=
forall x y, WHEN beq x y ~> b THEN b=true -> x=y.
Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ?? answ R) (x:A): ?? B :=
DO a <~ k x;;
DO b <~ beq x (input a) ;;
assert_b b msg;;
RET (output a).
Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool) (k: A -> ?? answ R) x:
beq_correct beq
-> WHEN wapply beq k x ~> y THEN R x y.
Proof.
unfold beq_correct; wlp_simplify.
destruct exta; simpl; auto.
Qed.
Local Hint Resolve wapply_correct: wlp.
Global Opaque wapply.
Axiom xrec_set_option: recMode -> ?? unit.
Extract Constant xrec_set_option => "ImpLoopOracles.xrec_set_option".
(* TODO: generalizaton to get beq (and a Hash function ?) in parameters ? *)
Axiom xrec: forall {A B}, ((A -> ?? B) -> A -> ?? B) -> ?? (A -> ?? B).
Extract Constant xrec => "ImpLoopOracles.xrec".
Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop) :=
forall f x, WHEN recF f x ~> z THEN (forall x', WHEN f x' ~> y THEN R x' y) -> R x z.
Program Definition rec {A B} beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): ?? (A -> ?? B) :=
DO f <~ xrec (B:=answ R) (fun f x =>
DO y <~ mk_annot (recF (wapply beq f) x) ;;
RET {| input := x; output := `y |});;
RET (wapply beq f).
Obligation 1.
eapply H1; eauto. clear H H1.
wlp_simplify.
Qed.
Lemma rec_correct A B beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq):
WHEN rec beq recF R H1 H2 ~> f THEN forall x, WHEN f x ~> y THEN R x y.
Proof.
wlp_simplify.
Qed.
Hint Resolve rec_correct: wlp.
Global Opaque rec.
|
