class Duplicates0 {
  // 3. we can do fast set checks if we know the bounds on the elements
  method find(s: seq<int>) returns (b:bool)
    requires forall i in s :: 0 <= i && i < 100;
  {
    var b [b == (exists i in [0..|s|] :: s[i] in s[..i]) ];
  }
}

class Duplicates1 refines Duplicates0 {
  refines find(s: seq<int>) returns (b: bool)
  {
    b := false;
    // 0. need a loop
    // 1. need a set data structure
    var i := 0;
    var d := new Set0;
    call d.init();

    // 6. use a witness from the loop
    ghost var w;

    while (i < |s|) 
      invariant 0 <= i && i <= |s|;
      // 5. add loop invariants using value of Set.add: equivalence as a set 
      invariant acc(d.rep);
      // 6. assert equivalent as sets of d.rep and s[..i]
      invariant forall n in d.rep :: n in s[..i];
      invariant forall n in [0..i] :: s[n] in d.rep;
      // 7. devise termination conditions to satisfy the spec
      invariant b ==> 0 <= w && w < |s| && s[w] in s[..w];
      invariant !b ==> (forall j,k in [0..i] :: j != k ==> s[j] != s[k]);
    {
      call r := d.add(s[i]);
      assert r ==> d.rep[0] == s[i]; // help out sequence axioms

      if (! r) {
        b := true;
        w := i;
      } 

      i := i + 1;
    }
  }
}

class Set0 {
  var rep: seq<int>;

  method init()
    requires acc(rep);
    ensures acc(rep) && |rep| == 0;
  {
    rep := nil<int>;
  }

  method add(i) returns (b:bool) 
    requires acc(rep);
    requires 0 <= i && i < 100;
    ensures acc(rep);
    ensures (i in old(rep)) ==> !b && rep == old(rep);
    ensures (i !in old(rep)) ==> b && rep == [i] ++ old(rep);
  {
    // 2. need a way to compute whether element is in the set
    var c:bool [c <==> i in old(rep)];
    if (c) {
      b := false;
    } else {
      b := true;
      rep := [i] ++ rep;
      assert rep[0] == i;
    }
  }
}

class Set1 refines Set0 {
  var bitset: seq<bool>;

  // 4. represent a set as a bitset (provided representation invariant of the uppermost class)
  replaces rep by acc(bitset) && 
    /** representation invariant */ (forall i in rep :: 0 <= i && i < 100) && |bitset| == 100 && 
    /** coupling invariant */ (forall j in [0..100] :: bitset[j] <==> (j in rep)) 

      
  refines init() 
  {
    var i := 0;
    bitset := nil<bool>;
    while (i < 100) 
      invariant i <= 100 && acc(bitset);
      invariant |bitset| == i;
      invariant forall b in bitset :: ! b;
    {
      bitset := [false] ++ bitset;
      i := i + 1;
    } 
  }

  transforms add(i) returns (b: bool)
  {
    replaces c by {var c:bool := this.bitset[i]}
    if {
      *
    } else {
      replaces * by {
        b := true;
        var s:seq<bool> := [true] ++ this.bitset[i+1..]; 
        assert s[0] == true; // help out sequence axioms
        s := this.bitset[..i] ++ s;

        this.bitset := s;        
      }
    }
  }
}