Maximum Subarray Problem

This is a variant where empty segments are not allowed.

use int.Int
use array.Array
use array.ArraySum

(*
            lo              cl    hi            i
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   a | | | | | | | | | | | | | | | | | | | | | |?|?|?|?|?|?|?|?|?|?|
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
           |<----- maxsum ------>|
                           |<----- curmax ---->|
*)

let maximum_subarray (a: array int) : (s: int)
  requires { 1 <= length a }
  ensures  { forall l h. 0 <= l < h <= length a -> sum a l h <= s }
  ensures  { exists l h. 0 <= l < h <= length a /\ sum a l h  = s }
=
  (* the maximum in a[0..i[ is a[lo..hi[ *)
  let ref maxsum = a[0] in
  let ghost ref lo = 0 in
  let ghost ref hi = 1 in
  (* the maximum ending on i is a[cl..i[ *)
  let ref curmax = a[0] in
  let ghost ref cl = 0 in
  for i = 1 to length a - 1 do
    invariant { forall l. 0 <= l < i -> sum a l i <= curmax }
    invariant { 0 <= cl < i /\ sum a cl i = curmax }
    invariant { forall l h. 0 <= l < h <= i -> sum a l h <= maxsum }
    invariant { 0 <= lo < hi <= i /\ sum a lo hi = maxsum }
    curmax <- curmax + a[i];
    if curmax < a[i] then (
      curmax <- a[i]; cl <- i
    );
    if curmax > maxsum then (
      maxsum <- curmax; lo <- cl; hi <- i+1
    )
  done;
  return maxsum