-
Notifications
You must be signed in to change notification settings - Fork 0
/
Liveness.i.dfy
81 lines (73 loc) · 2.47 KB
/
Liveness.i.dfy
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
include "Temporal.s.dfy"
include "Lift.i.dfy"
module Temporal__Liveness_i {
import opened Temporal__Temporal_s
import opened Temporal__Lift_i
/*
// f happens infinitely often.
// once g happens, it is stable until h
// f && g ==> h
// thus g leadsto h
// (because g stays true until f happens, at which point f&&g==>h.)
lemma InferFromUntil(f:temporal, g:temporal, h:temporal)
requires sat(always(eventually(f)))
requires sat(always(until(g, h)))
requires sat(always(implies(and(f, g), h)))
ensures sat(leadsto(g, h))
{
// I don't know if this proof rule is actually right. I should
// probably read the inference rules in Specifying Systems...
}
lemma InferInfinitelyOften(f:temporal, g:temporal)
requires sat(always(eventually(f)))
requires sat(leadsto(f, g))
ensures sat(always(eventually(g)))
{
// I don't know if this proof rule is actually right. I should
// probably read the inference rules in Specifying Systems...
}
*/
lemma InferLeadsTo(f:temporal, g:temporal)
requires sat(WF(f))
requires sat(until(f, g))
ensures sat(leadsto(f, g))
{
assert sat(always(implies(f, eventually(g))));
}
lemma LeadsToInduction(f:temporal, g:temporal, h:temporal)
requires sat(leadsto(f, g));
requires sat(leadsto(g, h));
ensures sat(leadsto(f, h));
{
reveal_eventually();
assert sat(always(implies(f, eventually(g))));
forall j | 0 <= j
ensures implies(f, eventually(h))(j)
{
// Unpack the implies
if f(j) {
// Chain the eventually witnesses together
assert implies(f, eventually(g))(j);
var k :| j <= k && g(k);
assert implies(g, eventually(h))(k);
}
}
}
lemma AllRoadsLeadTo<T(!new)>(r: QuantifierConstraint<T>,
f: QuantifiedTemporal<T>, g: temporal)
requires sat(Exists(r, f))
requires sat(Forall(r, t => leadsto(f(t), g)))
ensures sat(always(eventually(g)))
{
reveal_eventually();
reveal_Exists();
forall j | 0 <= j
ensures eventually(g)(j)
{
// Find the t that we need at time j to get f(t).
var t :| r(t) && f(t)(j);
// Then chain f(t) over to eventually-g.
assert implies(f(t), eventually(g))(j);
}
}
}