Forward leads to stack-overflow

Question

I'm trying to prove the correctness of an implementation of inserting a value in a sorted list. I have proved useful lemmas related to inserting a value in a sorted list and now I'm moving forward with "funspec".

The C code of the function:

void EnqueueLink(unsigned int *list, unsigned int id, unsigned int prio)
{
    unsigned int qAct = list[0];
    unsigned int lAct = 0;

    while ( (qAct != 0) && (FindPrio(qAct) >= prio) )
    {
        lAct = qAct;
        qAct = list[qAct];
    }

    /* Now we insert tAct between lAct and qAct and recompute the queue head.
    */
    list[lAct] = id;
    list[id] = qAct;
    // update task-head.
}

Some explanation without the loss of the semantics of the code: The function EnqueueLink takes 3 parameters. The first parameter is a (sorted) list, the second is some "id" which we want to sort according to its "prio"rity. The while loop parses the list until it finds the correct location (lAct).

I have defined the "funspecs" of this code:

Definition enqueue_spec : ident * funspec :=
DECLARE _EnqueueLink
WITH list : val, id: Z, prio: Z, sh : share, tasks : list Z
 PRE [ tptr tuint, tuint, tuint ]
  PROP  (writable_share sh; 0 <= prio <= Int.max_unsigned;
         Forall (fun x => 0 <= x <= Int.max_unsigned) tasks; LocallySorted Z.ge tasks)
  PARAMS (list; Vint(Int.repr id); Vint (Int.repr prio))
  SEP   (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr tasks)) taskActivations)
 POST [ tvoid ]
  PROP (LocallySorted Z.ge (insert id tasks)) RETURN ()
  SEP  (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr (insert tAct tasks))) taskActivations).

Definition Gprog := [enqueue_spec].

Lemma body_enqueuelink: semax_body Vprog Gprog f_EnqueueLink enqueue_spec.

Proof.

start_function. forward.

Admitted.

The "forward" tactic in the body_enqueuelink leads to stack-overflow (pun intended).

Explanation of the specification: I'm trying to prove that given a sorted list (of let's say tasks), this C function of inserting a new task renders a sorted list with the new task added.

It would be great to get some ideas on how to proceed from here. Since I'm quite new to VST, any help in validating the "funspecs" will be highly appreciated.

On the math side, I proved that a locally sorted list remains locally sorted after inserting an element using the following Fixpoint:

Fixpoint insert (x : Z) (l:list Z) : list Z :=
  match l with
  | nil => x :: nil 
  | (h :: t) =>
    match Z_ge_dec x h with
    | right _ => h :: (insert x t)
    | left _ => x :: (h :: t) end
  end.

Answer 1

That's an awfully large array, tarray tuint Int.max_unsigned. Perhaps you want an array of size N, where 0 < N <= Int.max_unsigned.

In particular: tarray tuint (Zlength tasks) where in the PROP you'll also want to say (0 < Zlength tasks) <= Int.max_unsigned.