package formal

// Insertion sorts a in ascending order, in place. This is a monomorphized
// (non-generic, plain []int, inlined swap) copy of sort.Insertion, annotated so
// the Gobra verifier can prove -- with the Viper/Z3 backend -- BOTH:
//
//   1. memory safety: every index access is in bounds (the permission
//      invariants "forall k :: 0<=k<len(a) ==> acc(&a[k])" carry write access
//      to every element through both loops), and
//   2. functional correctness (ordering): on return, a is sorted ascending
//      (the postcondition "forall p<q :: a[p] <= a[q]").
//
// The permutation half of correctness (that the output is a rearrangement of
// the input) is left to the property tests + the paper proof in
// docs/verification.md; proving it here would require ghost multiset state.
//
//@ requires forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
//@ ensures  forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
//@ ensures  forall p, q int :: 0 <= p && p < q && q < len(a) ==> a[p] <= a[q]
func Insertion(a []int) {
	i := 0
	//@ invariant 0 <= i && i <= len(a)
	//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
	// The prefix a[0..i) is already fully sorted.
	//@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q]
	for i < len(a) {
		j := i
		//@ invariant 0 <= j && j <= i && i < len(a)
		//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
		// a[0..i] is sorted once position j is ignored as either endpoint...
		//@ invariant forall p, q int :: 0 <= p && p < q && q <= i && p != j && q != j ==> a[p] <= a[q]
		// ...and the in-flight element a[j] is <= everything to its right.
		//@ invariant forall q int :: j < q && q <= i ==> a[j] <= a[q]
		for j > 0 && a[j] < a[j-1] {
			tmp := a[j]
			a[j] = a[j-1]
			a[j-1] = tmp
			j = j - 1
		}
		i = i + 1
	}
}