Rule7.dfy

// doesn't validate

include "Rule3.dfy"

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)
  requires ValidSeq(xs)
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)
{
  var (start, end) := range;
  if end < start {
    r := xs;
    return;
  }

  var beforeHi := IndexAtOrBeforePlusOne(xs, start);
  if beforeHi > 0 { // does not go at front
    var (startBefore, endBefore) := xs[beforeHi-1];
    if endBefore+1 < start {
      r := InternalAdd2(xs, range);
    } else if endBefore < end {
      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];
      r := DeleteExtra(r, (startBefore,end));
    } else{
      r := xs;
    }
  }
  else // goes at front
  {
    r := InternalAdd2(xs, range);
  }
}

method IndexAtOrBeforePlusOne(xs: seq<NeIntRange>, start: int) returns (i: nat)
  requires ValidSeq(xs)
  ensures i <= |xs|
  ensures forall p | p in xs[..i] :: p.0 <= start
  ensures forall j: nat | j < i :: xs[j].0 <= start
  ensures forall j: nat | i <= j < |xs| :: start < xs[j].0
  ensures i > 0 ==> xs[i-1].0 <= start
  ensures forall j: nat :: j < |xs| && xs[j].0 == start ==> j + 1 == i
  ensures forall j: nat | j < |xs| :: xs[j].0 == start ==> j + 1 == i
{
  i := 0;
  while i < |xs| && xs[i].0 <= start
  {
    i := i + 1;
  }
}


ghost function RangeToSet(pair: IntRange): set<int>
{
  set i {:autotriggers false} | pair.0 <= i <= pair.1 :: i
}

ghost function SeqToSet(sequence: seq<NeIntRange>): set<int>
  decreases |sequence|
  requires ValidSeq(sequence)
{
  if |sequence| == 0 then {}
  else if |sequence| == 1 then RangeToSet(sequence[0])
  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])
}

method InternalAdd2(xs: seq<NeIntRange>, internalRange: NeIntRange) returns (r: seq<NeIntRange>)
  requires ValidSeq(xs)
  requires forall i : nat :: i < |xs| && xs[i].0 < internalRange.0 ==> xs[i].1+1 < internalRange.0
  requires forall i: nat :: i < |xs| ==> xs[i].0 != internalRange.0
  ensures ValidSeq(r)
  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(internalRange)
{
  var wasThere: bool;
  r, wasThere := InsertNe(xs, internalRange);
  assert(!wasThere); // in Rust code
  r := DeleteExtra(r, internalRange);
}

method DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)
  requires forall i:nat,j:nat :: i < j < |xs| ==> xs[i].0 < xs[j].0 // starts are sorted
  requires exists i: nat :: i < |xs| && xs[i] == internalRange && ValidSeq(xs[..i+1]) && ValidSeq(xs[i+1..]) // each half is valid
  requires forall i:nat,j:nat :: i < j < |xs| && xs[i] != internalRange && xs[j] != internalRange ==> !Touch(xs[i], xs[j]) // only special might touch
  ensures ValidSeq(r) // result must be valid
  ensures exists i: nat :: i < |xs| && xs[i] == internalRange && SeqToSet(xs[..i+1]) + SeqToSet(xs[i+1..]) == SeqToSet(r) // result must cover same set as the halves
{
  var (start, end) := internalRange;
  var indexAfter := IndexAtOrAfter(xs, start);
  var (startAfter, endAfter) := xs[indexAfter];
  var endNew := end;
  var deleteList := [];
  var indexDel := indexAfter+1;
  while indexDel < |xs|
  {
    var (startDelete, endDelete) := xs[indexDel];
    if startDelete <= end + 1 // e.g. touch?
    {
      endNew := Max(endNew, endDelete);
      deleteList := deleteList + [startDelete];
      indexDel := indexDel + 1;
    }
    else
    {
      break;
    }
  }

  if endNew > end
  {
    endAfter := endNew;
    r := xs[indexAfter :=  (start, endAfter)];
  }
  else
  {
    r := xs;
  }
  var r2 := DeleteFromList(r, deleteList, indexAfter+1, indexDel);
  r := r2;
}

method InsertNe(s: seq<NeIntRange>, pair: NeIntRange) returns (r: seq<NeIntRange>, wasThere: bool)
  requires ValidSeq(s)
  requires forall i:nat | i < |s| :: s[i].0 < pair.0 ==> s[i].1+1 < pair.0
  requires forall i:nat | i < |s| :: s[i].0 != pair.0
  ensures SortedMapFlat.Valid(r)
  ensures SortedMapFlat.KeyToSet(r) == SortedMapFlat.KeyToSet(s) + {pair.0}
  ensures pair in r
  ensures forall i:nat | i < |s| && s[i].0 != pair.0 :: s[i] in r
  ensures wasThere == (pair.0 in SortedMapFlat.KeyToSet(s))
  ensures exists i: nat :: i < |r| && r[i] == pair && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..])
  ensures exists i: nat :: i < |r| && r[i] == pair && SeqToSet(r[..i+1]) + SeqToSet(r[i+1..]) == SeqToSet(s) + RangeToSet(pair)
{
  var i := IndexAtOrAfter(s, pair.0);
  if i == |s| {
    r := s[..i] + [pair] + s[i..];
  }
  else
  {
    r := s[..i] + [pair] + s[i..];
  }
  wasThere := false;
}

method IndexAtOrAfter(xs: seq<NeIntRange>, start: int) returns (i: nat)
  requires forall i:nat,j:nat :: i < j < |xs| ==> xs[i].0 < xs[j].0
  ensures i <= |xs|
  ensures forall p | p in xs[..i] :: p.0 < start
  ensures forall j: nat | j < i :: xs[j].0 < start
  ensures forall j: nat | i <= j < |xs| :: start <= xs[j].0
{
  i := 0;
  while i < |xs| && xs[i].0 < start
  {
    i := i + 1;
  }
}

function DeleteFromList(r: seq<NeIntRange>, deleteList: seq<int>,
                        indexAfterOne: nat, indexDel: nat
) : seq<NeIntRange>
  requires 0 < indexAfterOne <= |r|
  requires indexAfterOne <= indexDel <= |r|
{
  r[..indexAfterOne] + (if indexDel < |r| then r[indexDel..] else [])
}

module SortedMapFlat {

  // Check if a sequence of integer pairs is sorted and distinct (by key)
  predicate Valid(sorted_seq: seq<(int,int)>) {
    forall i:nat, j:nat | i < j < |sorted_seq| :: sorted_seq[i].0 < sorted_seq[j].0
  }

  function KeyToSet(m: seq<(int,int)>): set<int>
  {
    set i | i in m :: i.0
  }

}