I'm trying to make full code verification for cycle sort function on C. With ASCL annotations we need to "proof" that code is valid. Result is structured in Why3 GUI. I need to cover all goals/theories in safety and behavior sections and current result is:

Safety: 67/68. Need to proof one "loop variant decrease" goal

Behavior: 32/39

Also you can see the results on screenshots

And here is current version of my code:

 /*@ predicate sorted(int *array, integer first, integer last) =
   @    \forall integer i;
   @        first < i < last ==> array[i - 1] <= array[i];
*/

/*@
  @ requires array != \null; 
  @ requires \valid(array + (0 .. size-1));
  @ requires size >= 0; 
  @ assigns array[0..size-1]; 
  @
  @ ensures \forall integer i; 0 <= i < size ==> array[i] >= \old(array[i]);
  @ ensures sorted(array, 0, size);
  */
void sorting(int *array, int size) {
    int bound, idx, x, i, tmp;

    /*@ loop invariant 0 <= bound <= size - 2; 
      @ loop variant size - bound;    
      @*/
    for (bound = 0; bound <= size - 2; bound++) {
        /* @assert bound < size; */ 
        x = array[bound];
        idx = bound;

        /*@ loop invariant bound + 1 <= i <= size;
          @ loop invariant idx >= bound;                           
          @ loop invariant idx <= size-1;                          
          @ loop assigns i, idx;
          @ loop variant size - i;   
          @*/
        for (i = bound + 1; i < size; i++) {
            /*@ assert i < size; @*/
              
            if (array[i] < x) {
                /*@ assert idx + 1 < size; @*/
                idx++;
            }
        }

        if (idx == bound) {
            continue;
        }

        
        /*@ loop invariant idx >= bound && idx < size; 
          @ loop assigns idx;
          @ loop variant size - idx;
        @ */
        while (x == array[idx]) {
            /*@ assert bound <= idx < size; */ 
            idx += 1;
            /*@ assert idx < size; */
        }

        if (idx != bound) {
            /*@ assert idx < size; */
            tmp = array[idx];
            array[idx] = x;
            x = tmp;
        }
    
    /*@
      @ loop invariant bound <= idx < size;
      @ loop assigns idx, tmp, x, i, array[bound .. size-1];
      @ loop variant idx - bound;
    @ */
    
        while (idx != bound) {
            /*@ assert bound <= idx < size;  */
            idx = bound;

            /*@ loop invariant bound < i <= size;     
              @ loop invariant idx >= bound;
              @ loop invariant idx <= size-1;
              @ loop assigns i, idx; 
              @ loop variant size - i;         
             @*/
            for (i = bound + 1; i < size; i++) {
                if (array[i] < x) {
                    /*@ assert idx + 1 < size; */
                    idx += 1;
                }
            }
         
            /*@ assert idx < size; */
            /*@ 
              @ loop invariant idx >= bound && idx < size;
              @ loop assigns idx;
              @ loop variant size - idx;  
              @ */
            while (x == array[idx]) {
                /*@ assert idx + 1 < size; */
                idx += 1;
                /*@ assert idx < size;  */
            }
            /* @assert idx < size; */
            if (x != array[idx]) {
                /* @assert idx < size; */
                tmp = array[idx];
                /* @assert idx < size; */
                array[idx] = x;
                x = tmp;
            }
        }
    }
}

The same code with line numeration

Probably some of annotations are redundant but still this is the best result I have got. As for safety goal "40. Loop variant decrease" I believe it's somewhere in the middle of code, but I can't interpret color highlighting on screenshot. I tried to recount formulas for loop variants and tried many of them but it never leads to reaching goal #40 (furthermore some of proven goals become unproven)

Also I tried to make it in axiomatioc way. Example:

/*@ axiomatic Permut {
  @ predicate permut{L1,L2}(int *t1, int *t2, integer n);
  @     axiom permut_refl{L}:
  @         \forall int *t, integer n; permut{L,L}(t,t,n);
  @     axiom permut_sym{L1,L2}:
  @         \forall int *t1, *t2, integer n;
  @             permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n);
  @     axiom permut_trans{L1,L2,L3}:
  @         \forall int *t1, *t2, *t3, integer n;
  @             permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n)
  @             ==> permut{L1,L3}(t1,t3,n);
  @     axiom permut_exchange{L1,L2}:
  @         \forall int *t1, *t2, integer i, j, n;
  @         swap{L1, L2}(t1, t2, i, j, n) ==> permut{L1,L2}(t1,t2,n);
  @ }
  @*/

But it doesnt make any better. Plus using axioms is kind of cheating for verification, so they are undesirable

Probably, ACSL lemmas are the key but I can't construct any valid lemma that helps.

Have you any ideas what annotations I may add to make verification results better?