#include <vcc.h>
#include <limits.h>

#define RADIX 256

typedef struct counter {
  _(ghost \natural count)
  unsigned lo;
  unsigned hi;
  _(invariant lo < RADIX && hi < RADIX)
  _(invariant count == hi * RADIX + lo)
} counter;

void init(counter* p) 
_(writes \span(p))
_(ensures \wrapped(p))
{
  _(ghost p->count = 0)
  p->lo = 0;
  p->hi = 0;
  _(wrap p)
}

void inc(counter *p)
_(requires \wrapped(p))
_(requires p->count < ((RADIX-1) * RADIX + (RADIX-1)))
_(ensures \wrapped(p))
_(writes p)
_(decreases 0)
{
  _(unwrap p)
  if(p->lo < RADIX-1)
    p->lo++;
  else {
    p->hi++;
    p->lo = 0;
  }
  _(ghost p->count = p->count + 1)
  _(wrap p)
}

void dec(counter *p)
_(requires \wrapped(p))
_(requires p->count > 0)
_(writes p)
_(ensures \wrapped(p))
_(decreases 0)
{
  _(unwrap p)
  if (p->lo > 0) {
    p->lo--;
  }
  else {
    p->lo = RADIX-1;
    p->hi--;
  }
  _(ghost p->count = p->count - 1)
  _(wrap p)
}