typedef struct {
  unsigned size ;
  unsigned capacity ;
  int *data ;
} svector ;

/*@ predicate valid_svector(svector sv) = ... ;

    predicate unchanged{L1, L2}(svector sv, integer from, integer to) = ... ;

    predicate shifted{L1, L2}(svector sv, integer shift, integer from, integer to) = ... ;
*/

int sv_back(svector* v){
  return v->data[v->size-1];
}

int sv_front(svector* v){
  return v->data[0];
}

int sv_get(svector* v, unsigned idx){
  return v->data[idx];
}

void sv_set(svector* v, unsigned idx, int value){
  v->data[idx] = value ;
}

void sv_copy(svector* src, svector* dst){
  for(unsigned i = 0 ; i < src->size; ++i){
    dst->data[i] = src->data[i];
  }
  dst->size = src->size ;
}

/*@ requires \valid(v) && valid_svector(*v) ;
    requires 0 <= from <= to <= v->size ;
    requires 0 <= from+shift <= to+shift <= v->size ;
    assigns v->data[from+shift .. to+shift-1] ;
    ensures shifted{Pre, Here}(*v, shift, from, to) ;
*/
void sv_shift(svector* v, int shift, unsigned from, unsigned to){
  // provide the body of the function + code annotations so that the proof succeeds
}

void sv_pop_back(svector* v){
  v->size -- ;
}

void sv_pop_front(svector* v){
  sv_shift(v, -1, 1, v->size);
  v->size -- ;
}

void sv_force_push_back(svector* v, int value){
  v->data[v->size] = value ;
  v->size++;
}

void sv_force_push_front(svector* v, int value){
  v->size++;
  sv_shift(v, 1, 0, v->size-1);
  v->data[0] = value ;
}

void sv_force_insert(svector* v, unsigned idx, int value){
  v->size++;
  sv_shift(v, 1, idx, v->size-1);
  v->data[idx] = value ;
}

int sv_push_back(svector* v, int value, int* new_buffer, unsigned size){
  if(v->size < v-> capacity){
    sv_force_push_back(v, value);
    return 0 ;
  } else {
    for(unsigned i = 0; i < v->size; i++){
      new_buffer[i] = v->data[i] ;
    }
    new_buffer[v->size] = value ;
    v->data = new_buffer ;
    v->size++ ;
    v->capacity = size ;
    return 1 ;
  }
}

int sv_push_front(svector* v, int value, int* new_buffer, unsigned size){
  if(v->size < v-> capacity){
    sv_force_push_front(v, value);
    return 0 ;
  } else {
    new_buffer[0] = value ;
    for(unsigned i = 0; i < v->size; i++){
      new_buffer[i+1] = v->data[i] ;
    }
    v->data = new_buffer ;
    v->size++ ;
    v->capacity = size ;
    return 1 ;
  }
}

unsigned adjacent_find(svector* v){
  if(1 < v->size){
    for(unsigned i = 0 ; i < v->size-1 ; i++){
      if(v->data[i] == v->data[i+1]) return i ;
    }
    return v->size ;
  }
  return v->size ;
}

// Bonus
void remove(svector* v, int x){
  unsigned k = 0;

  for(unsigned i = 0; i < v->size; i++){
    if (v->data[i] != x){
      v->data[k] = v->data[i];
      k++;
    }
  }

  v->size = k;
}