Insertion sort is stable

module InsertionSortStable

 use import int.Int
 use import ref.Ref
 use import array.Array
 use import array.ArrayPermut

 type eltpair 'a 'b = {v: 'a; attr: 'b}

 predicate sorted_sub (a : array (eltpair int int)) (l u: int) =
    forall i1 i2 : int.
       l <= i1 <= i2 < u -> a[i1].v <= a[i2].v

 predicate sorted (a : array (eltpair int int)) = sorted_sub a 0 (length a)

 predicate stable_sub (a : array (eltpair int int)) (l u: int) =
    forall i1 i2 : int.
       l <= i1 <= i2 < u -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr

 predicate stable (a : array (eltpair int int)) = stable_sub a 0 (length a)

 let swap (a: array (eltpair int int)) (i: int) (j: int) =
   requires { 0 <= i < length a /\ 0 <= j < length a }
   ensures { exchange (old a) a i j }
  let v = a[i] in
   a[i] <- a[j];
   a[j] <- v

 let insertionSortStable (a: array (eltpair int int)) =
   requires { stable a }
   ensures { stable a }
'L:
   for i = 1 to length a - 1 do
    invariant { stable a }
     let j = ref i in
     while !j > 0 && a[!j - 1].v > a[!j].v do
     invariant { 0 <= !j <= i }
(*   invariant { stable a }  *)
     invariant {forall i1 i2 : int. 0 <= i1 <= i2 < (length a) -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr }
       swap a (!j-1) !j;
       j := !j - 1
     done
   done

end