Timer

timer.dfy

datatype State = State(min: int)

predicate Init(s: State){
  s.min == 5
}

predicate EnabledDecreaseMin(s: State){
  s.min > 0
}

predicate DecreaseMin(s: State, t: State){
  EnabledDecreaseMin(s) && s.min - 1 == t.min
}

predicate Stutter(s: State, t: State){
  s.min == t.min
}

predicate Next(s: State, t: State){
  DecreaseMin(s, t) || Stutter(s, t)
}

function Increase(i: nat): nat {
  i+1
}

// I am using Chapter 8 WF definition from Specifying Systems
// []([](Enabled <A>_v) => <><A>_v)

ghost predicate WeakFairness(t: imap<nat, State>)
  requires forall i : nat :: i in t
{
   forall i: nat {:trigger EnabledDecreaseMin(t[i])} :: (
      (forall j: nat :: j >= i ==> EnabledDecreaseMin(t[j]))
      ==>
      (exists k: nat :: k >= i && DecreaseMin(t[k], t[Increase(k)]))
   )
}

function Identity(n: nat) : nat {
  n
}

ghost predicate Spec(t: imap<nat, State>){
   (forall i : nat :: i in t)
 && Init(t[0])
 && (forall i : nat {:trigger Identity(i)}:: Next(t[i], t[i+1]))
 && WeakFairness(t)
}

lemma Safety(t: imap<nat, State>, k: nat)
  requires Spec(t)
  ensures t[k].min >= 0
{
   var j: nat := 0;
   while j <= k
    invariant forall m : nat :: m <= j ==> t[m].min >= 0
   {
      if t[j].min > 0 {
         assert j == Identity(j);
         assert Next(t[j], t[j+1]);
         if Stutter(t[j], t[j+1]) {}
         else {
            assert t[j+1].min == t[j].min - 1;
         }
      }
      else {
        assert j == Identity(j);
        assert Stutter(t[j], t[j+1]);
      }
      j := j + 1;
   }
}

lemma SafetyDecreasing(t: imap<nat, State>, m: nat, n: nat)
  requires Spec(t)
  requires m <= n
  ensures t[m].min >= t[n].min
{

  var j: nat := m;
  while j <= n
    invariant forall k : nat :: m <= k <= j ==> t[m].min >= t[k].min
  {
    if t[j].min > 0 {
      assert j == Identity(j);
      assert Next(t[j], t[j+1]);
      if Stutter(t[j], t[j+1]) {
         calc {
           t[m].min >= t[j].min;
           t[m].min >= t[j+1].min;
         }
      }
      else {
        assert t[j+1].min == t[j].min - 1;
        calc {
           t[m].min >= t[j].min;
           t[m].min >= t[j+1].min;
        }
      }
    }
    else {
       assert j == Identity(j);
       assert Stutter(t[j], t[j+1]);
    }
    j := j + 1;
  }

}

lemma ExistsHelperLemma(t: imap<nat, State>, m: nat)
  requires forall i : nat :: i in t
  requires !(forall j : nat :: j >= m ==> EnabledDecreaseMin(t[j]))
  ensures exists k : nat :: k >= m && !EnabledDecreaseMin(t[k])
{}

lemma {:vcs_split_on_every_assert} Eventually(t: imap<nat, State>)
  requires Spec(t)
  ensures exists m : nat :: t[m].min == 0
{

  // We start with index k equal to 0 and try to find
  // index m at which timer will be 0.
   var r : nat := 0;

   while t[r].min > 0
    invariant t[r].min >= 0
    decreases t[r].min
   {
     if(forall j : nat :: j >= r ==> EnabledDecreaseMin(t[j])) {
        assert exists k: nat :: k >= r && DecreaseMin(t[k], t[Increase(k)]) by {
          assert r == Identity(r);
          assert EnabledDecreaseMin(t[r]);
          assert
            (forall j : nat :: j >= r ==> EnabledDecreaseMin(t[j])) ==>
            (exists k: nat :: k >= r && DecreaseMin(t[k], t[Increase(k)]));
        }
        var k :| k >= r && DecreaseMin(t[k], t[Increase(k)]);
        assert Increase(k) == k + 1;
        SafetyDecreasing(t, r, k);
        assert t[r].min >= t[k].min;
        assert t[k+1].min == t[k].min - 1;
        assert t[r].min >= t[k].min > t[k+1].min;
        r := k + 1;
        if t[r].min == 0 { return; }
     }
     else {
        assert !(forall j : nat :: j >= r ==> EnabledDecreaseMin(t[j]));
        ExistsHelperLemma(t, r);
        var k :| k >= r && !EnabledDecreaseMin(t[k]);
        assert t[k].min <= 0;
        Safety(t, k);
        return;
     }
   }
}