diff --git a/formal-verification/Seek.dfy b/formal-verification/Seek.dfy
new file mode 100644
index 0000000000000000000000000000000000000000..be4350da83e09b36f9839ea36f97e7c98facd685
--- /dev/null
+++ b/formal-verification/Seek.dfy
@@ -0,0 +1,251 @@
+// Types
+
+datatype Maybe<T> = Nothing | Just(value: T)
+datatype Seek = Seek(rating: nat, creationTime: nat)
+datatype Event = Event(time: nat, first: Seek, second: Seek)
+
+// Uninterpreted Methods
+
+function method GetTimeControls(seek: Seek): set<nat>
+
+predicate method CanPair(first: Seek, second: Seek)
+ ensures // trivial postcondition as reasoning hint
+ GetTimeControls(first) * GetTimeControls(second) == GetTimeControls(second) * GetTimeControls(first)
+ ensures
+ CanPair(first, second) <==>
+ first != second &&
+ |GetTimeControls(first) * GetTimeControls(second)| > 0
+
+// Helper Methods
+
+function method Abs(value: int): nat
+ ensures Abs(value) == value || Abs(value) == -value
+function method Min(first: nat, second: nat): nat
+ ensures Min(first, second) == first || Min(first, second) == second
+ ensures Min(first, second) <= first
+ ensures Min(first, second) <= second
+
+function method GetMatchTime(first: Seek, second: Seek): int
+ ensures GetMatchTime(first, second) == Abs(first.rating - second.rating) + Min(first.creationTime, second.creationTime)
+
+function method Earliest(events: set<Event>): Event
+ requires |events| > 0
+ ensures Earliest(events) in events
+ ensures
+ forall e | e in events ::
+ Earliest(events).time <= e.time
+
+// Class to Verify
+
+class Server {
+ ghost var oldestSeek: Maybe<Seek>;
+ var seeks: set<Seek>;
+ var events: set<Event>;
+ var now: nat;
+
+ predicate NoFutureSeeks()
+ reads this
+ {
+ forall s | s in this.seeks ::
+ s.creationTime <= this.now
+ }
+
+ predicate NoPastEvents()
+ reads this
+ {
+ forall e | e in this.events ::
+ e.time >= this.now
+ }
+
+ predicate NoReflexiveEvents()
+ reads this
+ {
+ forall e | e in this.events ::
+ e.first != e.second
+ }
+
+ predicate EventsWithDistinctFirstSeeks()
+ reads this
+ {
+ forall e | e in this.events ::
+ forall f | f in this.events ::
+ e != f ==>
+ e.first != f.first
+ }
+
+ predicate NoEarlyTimers()
+ reads this
+ {
+ forall e | e in this.events ::
+ (e.first in this.seeks && e.second in this.seeks) ==>
+ e.time == GetMatchTime(e.first, e.second)
+ }
+
+ predicate NoLateTimers()
+ reads this
+ {
+ forall s | s in this.seeks ::
+ forall t | t in this.seeks ::
+ CanPair(s, t) ==>
+ exists e | e in this.events ::
+ (e.first == s || e.first == t) &&
+ e.time <= GetMatchTime(s, t)
+ }
+
+ predicate SemiStable()
+ reads this
+ {
+ this.NoFutureSeeks() &&
+ this.NoPastEvents() &&
+ this.NoReflexiveEvents() &&
+ this.EventsWithDistinctFirstSeeks() &&
+ this.NoEarlyTimers()
+ }
+
+ predicate Stable()
+ reads this
+ {
+ this.NoFutureSeeks() &&
+ this.NoPastEvents() &&
+ this.NoReflexiveEvents() &&
+ this.EventsWithDistinctFirstSeeks() &&
+ this.NoEarlyTimers() &&
+ this.NoLateTimers()
+ }
+
+ constructor()
+ ensures this.Stable()
+ {
+ this.oldestSeek := Nothing();
+ this.seeks := {};
+ this.events := {};
+ this.now := 0;
+ }
+
+ method GetClosest(seek: Seek) returns (closest: Maybe<Seek>)
+ requires this.Stable()
+ ensures this.Stable()
+ ensures closest.Nothing? <==> !exists s | s in this.seeks :: CanPair(seek, s)
+ ensures closest.Nothing? || closest.value in this.seeks
+ ensures closest.Nothing? || CanPair(seek, closest.value)
+ ensures
+ closest.Nothing? ||
+ forall s | s in this.seeks ::
+ CanPair(seek, s) ==>
+ GetMatchTime(seek, closest.value) <= GetMatchTime(seek, s)
+ {
+ var result := Nothing;
+ var remaining := this.seeks;
+ while |remaining| > 0
+ invariant remaining <= this.seeks
+ invariant result.Nothing? <==> !exists s | s in this.seeks - remaining :: CanPair(seek, s)
+ invariant result.Nothing? || result.value in this.seeks
+ invariant result.Nothing? || CanPair(seek, result.value)
+ invariant
+ result.Nothing? ||
+ forall s | s in this.seeks - remaining ::
+ CanPair(seek, s) ==>
+ GetMatchTime(seek, result.value) <= GetMatchTime(seek, s)
+ {
+ var candidate :| candidate in remaining;
+ remaining := remaining - {candidate};
+ if CanPair(seek, candidate) && (result.Nothing? || GetMatchTime(seek, candidate) < GetMatchTime(seek, result.value)) {
+ result := Just(candidate);
+ }
+ }
+ return result;
+ }
+
+ method Pair(seek: Seek, closest: Seek)
+ requires this.SemiStable()
+ requires seek != closest
+ requires seek in this.seeks
+ requires closest in this.seeks
+ requires
+ forall s | s in this.seeks ::
+ forall t | t in this.seeks ::
+ CanPair(s, t) ==>
+ GetMatchTime(seek, closest) <= GetMatchTime(s, t)
+ ensures this.SemiStable()
+ ensures this.oldestSeek == old(this.oldestSeek)
+ ensures this.seeks == old(this.seeks) - {seek, closest}
+ ensures this.events == old(this.events)
+ ensures this.now == old(this.now)
+ modifies this
+ {
+ this.seeks := this.seeks - {seek, closest};
+ }
+
+ method AddSeek(seek: Seek)
+ requires this.Stable()
+ requires
+ forall s | s in seeks ::
+ s != seek
+ requires
+ forall e | e in this.events ::
+ e.first != seek
+ requires
+ forall e | e in this.events ::
+ (e.first in this.seeks && e.second == seek) ==>
+ e.time == GetMatchTime(e.first, e.second)
+ requires seek.creationTime <= this.now
+ ensures this.Stable()
+ modifies this
+ {
+ var closest := this.GetClosest(seek);
+ this.seeks := this.seeks + {seek};
+ if closest.Nothing? {
+ this.oldestSeek := Just(seek);
+ } else {
+ var matchTime := GetMatchTime(seek, closest.value);
+ if matchTime <= this.now {
+ this.Pair(seek, closest.value);
+ } else {
+ this.events := this.events + {Event(matchTime, seek, closest.value)};
+ }
+ }
+ }
+
+ method RemoveSeek(seek: Seek)
+ requires this.Stable()
+ ensures this.Stable()
+ modifies this
+ {
+ this.seeks := this.seeks - {seek};
+ }
+
+ method PlaceSeek(rating: nat)
+ requires this.Stable()
+ requires
+ forall s | s in seeks ::
+ s != Seek(rating, this.now)
+ requires
+ forall e | e in this.events ::
+ e.first != Seek(rating, this.now) && e.second != Seek(rating, this.now)
+ ensures this.Stable()
+ modifies this
+ {
+ this.AddSeek(Seek(rating, this.now));
+ }
+
+ method Tick()
+ requires this.Stable()
+ requires |this.events| > 0
+ ensures this.Stable()
+ modifies this
+ {
+ var event := Earliest(this.events);
+ this.events := this.events - {event};
+ this.now := event.time;
+ var seek := event.first;
+ var closest := event.second;
+ if seek in this.seeks {
+ if closest in this.seeks {
+ this.Pair(seek, closest);
+ } else {
+ this.seeks := this.seeks - {seek};
+ this.AddSeek(seek);
+ }
+ }
+ }
+}
diff --git a/formal-verification/seek.dfy b/formal-verification/seek.dfy
deleted file mode 100644
index a426e3e18390c9170f03d59b9e24f9e901760d06..0000000000000000000000000000000000000000
--- a/formal-verification/seek.dfy
+++ /dev/null
@@ -1,251 +0,0 @@
-// Types
-
-datatype Maybe<T> = Nothing | Just(value: T)
-datatype Seek = Seek(rating: nat, creation_time: nat)
-datatype Event = Event(time: nat, first: Seek, second: Seek)
-
-// Uninterpreted Methods
-
-function method get_time_controls(seek: Seek): set<nat>
-
-predicate method can_pair(first: Seek, second: Seek)
- ensures // trivial postcondition as reasoning hint
- get_time_controls(first) * get_time_controls(second) == get_time_controls(second) * get_time_controls(first)
- ensures
- can_pair(first, second) <==>
- first != second &&
- |get_time_controls(first) * get_time_controls(second)| > 0
-
-// Helper Methods
-
-function method abs(value: int): nat
- ensures abs(value) == value || abs(value) == -value
-function method min(first: nat, second: nat): nat
- ensures min(first, second) == first || min(first, second) == second
- ensures min(first, second) <= first
- ensures min(first, second) <= second
-
-function method get_match_time(first: Seek, second: Seek): int
- ensures get_match_time(first, second) == abs(first.rating - second.rating) + min(first.creation_time, second.creation_time)
-
-function method earliest(events: set<Event>): Event
- requires |events| > 0
- ensures earliest(events) in events
- ensures
- forall e | e in events ::
- earliest(events).time <= e.time
-
-// Class to Verify
-
-class Server {
- ghost var oldest_seek: Maybe<Seek>;
- var seeks: set<Seek>;
- var events: set<Event>;
- var now: nat;
-
- predicate no_future_seeks()
- reads this
- {
- forall s | s in this.seeks ::
- s.creation_time <= this.now
- }
-
- predicate no_past_events()
- reads this
- {
- forall e | e in this.events ::
- e.time >= this.now
- }
-
- predicate no_reflexive_events()
- reads this
- {
- forall e | e in this.events ::
- e.first != e.second
- }
-
- predicate events_with_distinct_first_seeks()
- reads this
- {
- forall e | e in this.events ::
- forall f | f in this.events ::
- e != f ==>
- e.first != f.first
- }
-
- predicate no_early_timers()
- reads this
- {
- forall e | e in this.events ::
- (e.first in this.seeks && e.second in this.seeks) ==>
- e.time == get_match_time(e.first, e.second)
- }
-
- predicate no_late_timers()
- reads this
- {
- forall s | s in this.seeks ::
- forall t | t in this.seeks ::
- can_pair(s, t) ==>
- exists e | e in this.events ::
- (e.first == s || e.first == t) &&
- e.time <= get_match_time(s, t)
- }
-
- predicate semistable()
- reads this
- {
- this.no_future_seeks() &&
- this.no_past_events() &&
- this.no_reflexive_events() &&
- this.events_with_distinct_first_seeks() &&
- this.no_early_timers()
- }
-
- predicate stable()
- reads this
- {
- this.no_future_seeks() &&
- this.no_past_events() &&
- this.no_reflexive_events() &&
- this.events_with_distinct_first_seeks() &&
- this.no_early_timers() &&
- this.no_late_timers()
- }
-
- constructor()
- ensures this.stable()
- {
- this.oldest_seek := Nothing();
- this.seeks := {};
- this.events := {};
- this.now := 0;
- }
-
- method get_closest(seek: Seek) returns (closest: Maybe<Seek>)
- requires this.stable()
- ensures this.stable()
- ensures closest.Nothing? <==> !exists s | s in this.seeks :: can_pair(seek, s)
- ensures closest.Nothing? || closest.value in this.seeks
- ensures closest.Nothing? || can_pair(seek, closest.value)
- ensures
- closest.Nothing? ||
- forall s | s in this.seeks ::
- can_pair(seek, s) ==>
- get_match_time(seek, closest.value) <= get_match_time(seek, s)
- {
- var result := Nothing;
- var remaining := this.seeks;
- while |remaining| > 0
- invariant remaining <= this.seeks
- invariant result.Nothing? <==> !exists s | s in this.seeks - remaining :: can_pair(seek, s)
- invariant result.Nothing? || result.value in this.seeks
- invariant result.Nothing? || can_pair(seek, result.value)
- invariant
- result.Nothing? ||
- forall s | s in this.seeks - remaining ::
- can_pair(seek, s) ==>
- get_match_time(seek, result.value) <= get_match_time(seek, s)
- {
- var candidate :| candidate in remaining;
- remaining := remaining - {candidate};
- if can_pair(seek, candidate) && (result.Nothing? || get_match_time(seek, candidate) < get_match_time(seek, result.value)) {
- result := Just(candidate);
- }
- }
- return result;
- }
-
- method pair(seek: Seek, closest: Seek)
- requires this.semistable()
- requires seek != closest
- requires seek in this.seeks
- requires closest in this.seeks
- requires
- forall s | s in this.seeks ::
- forall t | t in this.seeks ::
- can_pair(s, t) ==>
- get_match_time(seek, closest) <= get_match_time(s, t)
- ensures this.semistable()
- ensures this.oldest_seek == old(this.oldest_seek)
- ensures this.seeks == old(this.seeks) - {seek, closest}
- ensures this.events == old(this.events)
- ensures this.now == old(this.now)
- modifies this
- {
- this.seeks := this.seeks - {seek, closest};
- }
-
- method add_seek(seek: Seek)
- requires this.stable()
- requires
- forall s | s in seeks ::
- s != seek
- requires
- forall e | e in this.events ::
- e.first != seek
- requires
- forall e | e in this.events ::
- (e.first in this.seeks && e.second == seek) ==>
- e.time == get_match_time(e.first, e.second)
- requires seek.creation_time <= this.now
- ensures this.stable()
- modifies this
- {
- var closest := this.get_closest(seek);
- this.seeks := this.seeks + {seek};
- if closest.Nothing? {
- this.oldest_seek := Just(seek);
- } else {
- var match_time := get_match_time(seek, closest.value);
- if match_time <= this.now {
- this.pair(seek, closest.value);
- } else {
- this.events := this.events + {Event(match_time, seek, closest.value)};
- }
- }
- }
-
- method remove_seek(seek: Seek)
- requires this.stable()
- ensures this.stable()
- modifies this
- {
- this.seeks := this.seeks - {seek};
- }
-
- method seek(rating: nat)
- requires this.stable()
- requires
- forall s | s in seeks ::
- s != Seek(rating, this.now)
- requires
- forall e | e in this.events ::
- e.first != Seek(rating, this.now) && e.second != Seek(rating, this.now)
- ensures this.stable()
- modifies this
- {
- this.add_seek(Seek(rating, this.now));
- }
-
- method tick()
- requires this.stable()
- requires |this.events| > 0
- ensures this.stable()
- modifies this
- {
- var event := earliest(this.events);
- this.events := this.events - {event};
- this.now := event.time;
- var seek := event.first;
- var closest := event.second;
- if seek in this.seeks {
- if closest in this.seeks {
- this.pair(seek, closest);
- } else {
- this.seeks := this.seeks - {seek};
- this.add_seek(seek);
- }
- }
- }
-}