//  Time to verify: 0m37.716s (note that this is almost 5 minutes via SSH)
//  Corresponds to the packet pile in PacketPile.java
//  Abstractions:
//      In practice, packet pile would store a buffer of blood packets
//      This version of the proof will abstract each blood packet to
//      just the expiry date, since the functions we prove in this file
//      will only see blood packets as expiry date integers.

class PacketPile
{
    var buf: array<int>; // int represents expiry date of blood packet
    var count: int;
    var low: int;
    // bloodStatuses


    predicate Valid()
    reads this, this.buf;
    {
        buf != null &&
        0 <= count <= buf.Length &&
        0 <= low <= buf.Length &&
        Sorted(buf, 0, count) // Sorted by expiry date
    }

    method Init(size: int, low1: int)
    modifies this;
    requires 0 <= low1 <= size;
    ensures Valid();
    ensures fresh(buf);
    ensures count == 0;
    ensures low == low1;
    {
        buf := new int[size];
        count := 0; // initially 0 packets
        low := low1;
    }

    method popAtIndex(index: int) returns (el: int)
    modifies this.buf, this`count;
    requires Valid(); ensures Valid();
    requires 0 <= index < count;
    ensures count == old(count) - 1;
    ensures el == old(buf[index]);
    ensures buf[..count] == old(buf[..index]) + old(buf[index+1..old(count)]); // Putting RHS into predicate fails(?)

    // Excluding String dest since we aren't dealing with actual bloodpacket objects
    method doRequest(nPackets: int, useBy: int) returns (result: array<int>)
    modifies this.buf, this`count;
    requires Valid();
    requires nPackets > 0;
    ensures Valid();
    ensures result != null;
    ensures forall i :: 0 <= i < result.Length ==> result[i] >= useBy;
    ensures 0 <= result.Length <= old(count);
    ensures CountGE(old(buf)[..old(count)],useBy) < nPackets ==> result.Length == 0; // If not enough, return nothinf
    ensures CountGE(old(buf)[..old(count)],useBy) >= nPackets ==> count == old(count) - nPackets;
    ensures CountGE(old(buf)[..old(count)],useBy) >= nPackets ==> result.Length == nPackets; // If enough, then returns some amount
    // ensures CountGE(buf[..],useBy) >= nPackets ==> result[0]// If enough, return the oldest possible
    // Oldest <==> Just before result it too early // what if result[0]
        // Everything before is too early
        // THere exists an index such hat everything befor eis tpoo early
    // ensures CountGE(old(buf)[..old(count)]),useBy) >= nPackets ==>
    //     exists lo :: 0 <= lo <= i+nPackets <= old(count) && (
    //         (forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]) < useBy) &&
    //         (forall j :: 0 <= j < nPackets ==> result[j] == old(buf[j+lo]))
    //     );
    {
        result := new int[nPackets];
        var lo := 0;
        while (lo < count && buf[lo] < useBy)
        decreases count - lo;
        invariant old(buf) == buf;
        invariant forall i :: 0 <= i < count ==> buf[i] == old(buf[i]);
        invariant old(count) == count;
        invariant 0 <= lo <= count;
        invariant forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
        invariant forall j :: 0 <= j < lo ==> buf[j] < useBy;
        invariant Valid();
        invariant Sorted(buf,0,count);
        invariant CountGE(buf[..lo],useBy) == 0;
        invariant count <= buf.Length;
        {
            // assert CountGE(buf[..i],useBy) == 0;
            // assert buf[i] < useBy;
            // assert count > 0;
            // assert CountGE(buf[..i+1],useBy) == if |buf[..i+1]| == 0 then 0 else
            //                                 (if buf[..i+1][|buf[..i+1]|-1] >= useBy then 1 else 0) + CountGE(buf[..i+1][..|buf[..i+1]|-1], useBy);

            // assert |buf[..i+1]| == i+1 != 0;
            // assert CountGE(buf[..i+1],useBy) == (if buf[..i+1][|buf[..i+1]|-1] >= useBy then 1 else 0) + CountGE(buf[..i+1][..|buf[..i+1]|-1], useBy);
            // assert |buf[..i+1]|-1 == i;
            // assert buf[..i+1][|buf[..i+1]|-1] == buf[i] < useBy;
            // assert (if buf[..i+1][|buf[..i+1]|-1] >= useBy then 1 else 0) == 0;

            // assert CountGE(buf[..i+1],useBy) == 0 + CountGE(buf[..i+1][..i], useBy);
            assert buf[..lo+1][..lo] == buf[..lo];
            // assert CountGE(buf[..i+1],useBy) == 0 + CountGE(buf[..i], useBy);
            // assert CountGE(buf[..i+1],useBy) == CountGE(buf[..i],useBy);
            lo := lo + 1;
        }
        assert CountGE(buf[..lo],useBy) == 0;
        assert forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
        assert forall j :: 0 <= j < lo ==> buf[j] < useBy;

        // if (count - i < nPackets)
        if (lo == count) {
            assert CountGE(buf[..count],useBy) == 0 < nPackets;
            result := new int [0];
        } else {
            assert (lo < count);
            assert (buf[lo] >= useBy);
            assert (useBy <= buf[lo]);
            assert Sorted(buf,0,count);
            assert forall j :: lo <= j < count ==> buf[j] >= useBy;
            assert CountGE(buf[..lo],useBy) == 0;
            var found := 0;

            while (lo + found < count && found < nPackets)
            decreases count - (lo + found);
            invariant Valid();
            invariant useBy <= buf[lo];
            invariant old(buf) == buf;
            invariant forall i :: 0 <= i < count ==> buf[i] == old(buf[i]);
            invariant old(count) == count;
            invariant 0 <= lo <= count;
            invariant lo <= lo + found <= count <= buf.Length;
            invariant 0 <= found <= nPackets;

            invariant forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
            invariant forall j :: 0 <= j < lo ==> buf[j] < useBy;

            invariant Sorted(buf,0,count);
            invariant allGE(buf,lo,lo+found,useBy);


            // Now you've found how many that are possible
            if (found >= nPackets) {

                // Good
                // We formalise this as 'good', that there are enough packets
                assert 0 <= count <= buf.Length;

                assert allGE(buf,lo,lo+found,useBy);

                assert buf[..lo+found] == buf[..lo] + buf[lo..lo+found];
                assert CountGE(buf[lo..lo+found],useBy) == nPackets;
                assert CountGE(buf[..lo],useBy) == 0;
                distCountGE(buf[..lo],buf[lo..lo+found],useBy);
                assert CountGE(buf[..lo+found],useBy) == nPackets;

                assert buf[..count] == buf[..lo+found] + buf[lo+found..count];
                assert CountGE(buf[lo+found..count],useBy) >= 0;
                distCountGE(buf[..lo+found],buf[lo+found..count],useBy);
                assert CountGE(buf[..count],useBy) >= nPackets;

                result := new int[nPackets];
                assert old(buf) == buf;
                assert allGE(buf,lo,lo+found,useBy);
                assert CountGE(buf[..count],useBy) >= nPackets;

                assert !(CountGE(old(buf)[..old(count)],useBy) < nPackets);

                var i := 0;
                while (i < nPackets)
                decreases nPackets - i;
                invariant Valid();
                invariant buf == old(buf);
                invariant forall i :: 0 <= i < count ==> buf[i] == old(buf[i]);
                invariant useBy <= buf[lo];
                invariant allGE(buf,lo,lo+found,useBy);
                invariant 0 <= count <= buf.Length && CountGE(buf[..count],useBy) >= nPackets;
                invariant 0 <= i <= nPackets;
                invariant lo <= lo + i <= lo + nPackets <= count;
                invariant Sorted(buf,0,count);
                invariant forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
                invariant forall j :: 0 <= j < lo ==> buf[j] < useBy;
                invariant forall j :: 0 <= j < i ==> result[j] >= useBy;
                invariant forall j :: 0 <= j < i ==> result[j] == buf[lo+j];
                invariant count == old(count);
                {
                    assert useBy <= buf[lo] <= buf[lo+i];
                    assert forall j :: 0 <= j < i ==> result[j] == buf[lo+j];
                    result[i] := buf[lo+i];
                    assert forall j :: 0 <= j <= i ==> result[j] == buf[lo+j];
                    i := i + 1;
                }
                assert CountGE(buf[..count],useBy) >= nPackets ==> result.Length == nPackets;
                assert count <= buf.Length;

                assert 0 <= lo <= old(count);
                assert forall j :: 0 <= j < lo ==> buf[j] < useBy;
                assert forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
                assert forall j :: 0 <= j < nPackets ==> result[j] == old(buf[lo+j]);

                assert lo + nPackets <= old(count);

                // Now that you have the correct ones we assert that this came from a continuous subset:


                assert lo + nPackets <= old(count);
                assert 0 <= lo <= old(count);
                assert forall j :: 0 <= j < nPackets ==> result[j] == old(buf[lo+j]);
                assert forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
                assert forall j :: 0 <= j < lo ==> buf[j] < useBy;

                i := 0;
                while (i < nPackets)
                invariant Valid();
                invariant count == old(count) - i;
                invariant 0 <= lo <= old(count) - nPackets <= count;
                invariant buf.Length != 0;
                invariant forall j :: 0 <= j < nPackets ==> result[j] == old(buf[lo+j]);
                invariant forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]);
                invariant forall j :: 0 <= j < lo ==> buf[j] < useBy;
                {
                    var p := popAtIndex(lo);
                    i := i + 1;
                }
                assert CountGE(buf[..old(count)],useBy) >= nPackets ==> count == old(count) - nPackets;
                assert CountGE(buf[..old(count)],useBy) >= nPackets ==> (forall j :: 0 <= j < nPackets ==> result[j] == old(buf[lo+j]));
                assert CountGE(buf[..old(count)],useBy) >= nPackets ==> (forall j :: 0 <= j < lo ==> buf[j] == old(buf[j]));
                assert CountGE(buf[..old(count)],useBy) >= nPackets ==> (forall j :: 0 <= j < lo ==> buf[j] < useBy);
            } else {
                assert found < nPackets;
                assert lo + found == count;
                assert buf[..count] == buf[..lo] + buf[lo..count];
                assert CountGE(buf[lo..count],useBy) == found;
                assert CountGE(buf[..lo],useBy) == 0;
                distCountGE(buf[..lo],buf[lo..count],useBy);
                assert CountGE(buf[..count],useBy) == found < nPackets;
                result := new int[0];
            }
        }
    }
}

predicate Sorted(a: array<int>, low: int, high: int)
reads a;
requires a != null;
requires 0 <= low <= high <= a.Length;
{
    forall i, j :: low <= i < j < high ==> a[i] <= a[j]
}

// Counts greater than or equal to key
function CountGE(a: seq<int>, key: int): nat
decreases |a|;
ensures 0 <= CountGE(a, key) <= |a|;
{
    if |a| == 0 then 0 else
    (if a[|a|-1] >= key then 1 else 0) + CountGE(a[..|a|-1], key)
}

lemma distCountGE(a: seq<int>, b: seq<int>, key: int)
decreases |b|;
ensures CountGE(a,key) + CountGE(b,key) == CountGE(a+b,key);
{
    if (|b| == 0) {
        assert a + b == a;
    } else {
        distCountGE(a,b[0..|b|-1],key);
        // assert CountGE(a,key) + CountGE(b[..|b|-1],key) == CountGE(a+b[..|b|-1],key);
        // assert b[..|b|-1] + [b[|b|-1]] == b;
        // assert CountGE(b,key) == CountGE(b[..|b|-1],key) + (if b[|b|-1] >= key then 1 else 0);
        assert a + b[..|b|-1] + [b[|b|-1]] == a + b;
    }
}

lemma inclusiveGE(a: array<int>, lo: int, hi: int, key: int)
requires a != null;
requires 0 <= lo <= hi < a.Length;
requires forall i:: lo <= i < hi ==> a[i] >= key;
requires a[hi] >= key;
ensures forall i:: lo <= i <= hi ==> a[i] >= key;
{

}

predicate allGE(a: array<int>, lo: int, hi: int, key: int)
requires a != null;
reads a;
requires 0 <= lo <= hi <= a.Length;
{
    forall i:: lo <= i < hi ==> a[i] >= key
}

predicate oldestPossible(a: seq<int>, b: seq<int>, a': seq<int>, needed: int, size: int, key: int)
requires 0 <= needed;
requires |a| == |a'|;
requires |b| == needed;
{
    exists k :: 0 <= k <= |a| &&
        k + needed <= |a| &&
        forall j :: 0 <= j < needed ==> b[j] == a[k+j] &&
        forall j :: 0 <= j < k ==> a[j] == a'[j] &&
        forall j :: 0 <= j < k ==> a[j] < key
}

function DualRange(a: array<int>, low: int, mid1: int, mid2: int, high: int): seq<int>
reads a;
requires a != null;
requires 0 <= low <= mid1 <= mid2 <= high <= a.Length;
{
    a[low..mid1] + a[mid2..high]
}