// ----------------------------------------------------------------------------
// Sorting arrays by the Insertion Sort Algorithm
// ----------------------------------------------------------------------------

//****************************************
//CONSTANTS
//****************************************
val N:ℕ;
val M:ℕ;

//****************************************
//VARIABLES
//****************************************
type nat = ℕ[M];
type array = Array[N,nat];
type index = ℕ[N-1];

//****************************************
//SUPPORTING STATEMENTS
//****************************************
//isSorted(a:array,m:index,n:index)
//  states if all elements from m to n are sorted
pred isSorted(a:array,m:index,n:index) <=>
  ∀i:index.(m ≤ i ∧ i ≤ n-1) => a[i] ≤ a[i+1];
//isPermutationOf(a:array,b:array)
//  states if a is a permutation of the input array
pred isPermutationOf(a:array,b:array) <=>
  ∃p:Array[N,index].
    (∀i:index,j:index. i ≠ j => p[i] ≠ p[j])
    ∧(∀i:index. a[i] = b[p[i]]);
    
//isPartEqual(a:array,b:array,m:index,n:index)
//  states if a and b from m to n are equal
pred isPartEqual(a:array,b:array,m:index,n:index) <=>
  (∀i:index. (m ≤ i ∧ i ≤ n) => a[i] = b[i]);

//****************************************
//CONDITIONS
//****************************************
//pre-Condition
//  (*) trivial
pred pre(a:array) <=> true;

//post-Condition of the inner loop
//  (*) resulting array is sorted
//  (*) a is a permutation of the input array
pred post(a:array,result:array) <=> 
  isSorted(result,0,N-1)
  ∧ isPermutationOf(a,result);

//invariant of the inner loop
//  (*) elements to the left of i are sorted 
//  (*) elements right of i are unchanced
//  (*) b is a permutation of a
pred inv_outer(a:array,b:array,i:Int[1,N-1+1]) <=>
  isSorted(b,0,i-1)
  ∧ (i<N-1 => isPartEqual(a,b,i+1,N-1))
  ∧ isPermutationOf(a,b);

//termination term of the outer loop
//  it terminates after at most N-1 iterations
fun termin_outer(i:Int[1,N-1+1]):index = N-i;

//loop condition of the outer loop 
pred loop_cond_outer(i:Int[1,N-1+1]) <=>
  i≤N-1;

//post-Condition of the inner loop
//  (*) elements left of i are sorted
//  (*) elements right of i are unchanced
//  (*) b is a permutation of a
pred post_inner(a:array,b:array,i:Int[1,N-1+1])<=>
  isSorted(b,0,i)
  ∧ (i+1<N-1 => isPartEqual(a,b,i+1,N-1))
  ∧ isPermutationOf(a,b);

//invariant of the inner loop
//  (*) elements left of j+1 are sorted
//  (*) elements right of j+1 are sorted
//  (*) j+1 is smaller as its right neighbour
//  (*) the array without j+1 is sorted.
//  (*) elements right of i are unchanced
//  (*) b is a permutation of a
pred inv_inner(a:array,b:array,j:Int[-1,N-2],i:Int[1,N-1],x:nat) <=>
  j ≤ i-1
  ∧ x = b[j+1]
  ∧ (j ≥ 0 => isSorted(b,0,j))
  ∧ (j+2 < i => isSorted(b,j+2,i))
  ∧ (j+2 ≤ i => x < b[j+2])
  ∧ (j+2 ≤ i ∧ j ≥ 0 => b[j]≤b[j+2])
  ∧ (i+1<N-1 => isPartEqual(a,b,i+1,N-1))
  ∧ isPermutationOf(a,b);
  
//termination term of the inner loop
//  it terminates after at most N-1 iterations
fun termin_inner(j:Int[-1,N-1-1]):index = j+1;

//loop condition of the inner loop
pred loop_cond_inner(j:Int[-1,N-1-1],b:array,x:nat) <=>
  j ≥ 0 ∧ b[j] > x;

//****************************************
//VERIFICATION CONDITIONS
//****************************************
//Verification Condition 1 of the outer loop
//   given the precondition,
//   (*) invariant holds before the loop started
theorem VC_begin_outer(a:array,b:array,i:Int[1,N-1+1])
  requires pre(a);
  <=> b = a ∧ i=1 => inv_outer(a,b,i);

//Verification Condition 2 of the outer loop
//  given the precondition,
//  (*) invariant is preserved by every loop iteration
//  (*) termination term decreases at every iteration
theorem VC_iter_outer(a:array,b:array,i:Int[1,N-1+1])
  requires pre(a);
  <=> inv_outer(a,b,i) ∧ loop_cond_outer(i)
    => (∀c:array.post_inner(b,c,i) => inv_outer(a,c,i+1))
    ∧ termin_outer(i+1) < termin_outer(i);

//Verification Condition 3 of the outer loop
//  given the precondition,
//  (*) on termination invariant implies postcondition
theorem VC_end_outer(a:array,b:array,i:Int[1,N-1+1])
  requires pre(a);
  <=> inv_outer(a,b,i) ∧ ¬loop_cond_outer(i) => post(a,b);

//Verification Condition 4 of the outer loop
//  given the precondition,
//  (*) termination term is never negative
theorem VC_termin_outer(a:array,b:array,i:Int[1,N-1])
  requires inv_outer(a,b,i);
  <=> inv_outer(a,b,i) => termin_outer(i)≥0;
  
//Verification Condition 1 of the inner loop
//   given the precondition,
//   (*) invariant holds before the loop started
theorem VC_begin_inner(a:array,b:array,i:Int[1,N-1],j:Int[-1,N-2],x:nat)
  requires inv_outer(a,b,i);
  <=> j = i-1 ∧ x = b[i] => inv_inner(a,b,j,i,x);

//Verification Condition 2 of the inner loop
//  given the precondition,
//  (*) invariant is preserved by every loop iteration
//  (*) termination term decreases at every iteration
theorem VC_iter_inner(a:array,b:array,i:Int[1,N-1],j:Int[-1,N-2],x:nat)
  requires inv_outer(a,b,i);
  <=> inv_inner(a,b,j,i,x) ∧ loop_cond_inner(j,b,x)
    => inv_inner(a,b with [j+1]=b[j] with [j]=x,j-1,i,x)
    ∧ termin_inner(j-1) < termin_inner(j);

//Verification Condition 3 of the inner loop
//  given the precondition,
//  (*) on termination invariant implies postcondition
theorem VC_end_inner(a:array,b:array,i:Int[1,N-1],j:Int[-1,N-2],x:nat)
  requires inv_outer(a,b,i);
  <=> inv_inner(a,b,j,i,x) ∧ ¬loop_cond_inner(j,b,x) => post_inner(a,b,i);

//Verification Condition 4 of the inner loop
//  given the precondition,
//  (*) termination term is never negative
theorem VC_termin_inner(a:array,b:array,i:Int[1,N-1],j:Int[-1,N-2],x:nat)
  requires inv_outer(a,b,i);
  <=> inv_inner(a,b,j,i,x) => termin_inner(j)≥0;

//****************************************
//IMPLEMENTATION
//****************************************
//proc insertionSort(a:array): array
//  sorts an array
proc insertionSort(a:array): array
  requires pre(a);
  ensures post(a,result);
{
  var b:array := a;
  for var i:Int[1,N-1+1] := 1; i≤N-1; i := i+1 do
    invariant inv_outer(a,b,i);
    decreases termin_outer(i);
  {
    var x:nat := b[i];
    for var j:Int[-1,N-1-1] := i-1; j ≥ 0 ∧ b[j] > x; j := j-1 do
      invariant inv_inner(a,b,j,i,x);
      decreases termin_inner(j);
    {
      b[j+1] := b[j];
      b[j] := x;
    }
  }
  return b;
}