(** {1 Arrays with bounded-size integers}

    Note: We currently duplicate code to get the various modules below
    but we should eventually be able to implement a single module and
    then to clone it.  *)

(** {2 Arrays with 32-bit indices} *)

module Array32

  use int.Int
  use mach.int.Int32
  use map.Map as M

  type array [@extraction:array] 'a = private {
    mutable ghost elts : int -> 'a;
                length : int32;
  } invariant { 0 <= length }

  function ([]) (a: array 'a) (i: int) : 'a = a.elts i

  val ([]) (a: array 'a) (i: int32) : 'a
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { result = a[i] }

  val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { a.elts = M.set (old a.elts) i v }

  (** unsafe get/set operations with no precondition *)

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int32)
    ensures { 0 <= i < a.length }
    ensures { result = a[i] }
    raises  { OutOfBounds -> i < 0 \/ i >= a.length }
  = if i < of_int 0 || i >= length a then raise OutOfBounds;
    a[i]

  let defensive_set (a: array 'a) (i: int32) (v: 'a)
    ensures { 0 <= i < a.length }
    ensures { a.elts = M.set (old a.elts) i v }
    raises  { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
  = if i < of_int 0 || i >= length a then raise OutOfBounds;
    a[i] <- v

  val make [@extraction:array_make] (n: int32) (v: 'a) : array 'a
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i:int. 0 <= i < n -> result[i] = v }
    ensures  { result.length = n }

  val append (a1: array 'a) (a2: array 'a) : array 'a
    ensures { result.length = a1.length + a2.length }
    ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < a2.length ->
              result[a1.length + i] = a2[i] }

  val sub (a: array 'a) (ofs: int32) (len: int32) : array 'a
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < len ->
               result[i] = a[ofs + i] }

  val copy (a: array 'a) : array 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < result.length -> result[i] = a[i] }

  val fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a) : unit writes {a}
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs \/
        ofs + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. ofs <= i < ofs + len ->
               a[i] = v }

  val blit (a1: array 'a) (ofs1: int32)
                 (a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2}
    requires { 0 <= ofs1 /\ 0 <= len }
    requires { ofs1 + len <= a1.length }
    requires { 0 <= ofs2 /\
               ofs2 + len <= a2.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a2[i] = a1[ofs1 + i - ofs2] }

  val self_blit (a: array 'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
    writes {a}
    requires { 0 <= ofs1 /\ 0 <= len /\
               ofs1 + len <= a.length }
    requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a[i] = (old a)[ofs1 + i - ofs2] }

end

(** {2 Arrays with 31-bit indices} *)

module Array31

  use int.Int
  use mach.int.Int31
  use map.Map as M

  type array 'a = private {
    mutable ghost elts : int -> 'a;
                length : int31;
  } invariant { 0 <= length }

  function ([]) (a: array 'a) (i: int) : 'a = a.elts i

  val ([]) (a: array 'a) (i: int31) : 'a
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { result = a[i] }

  val ([]<-) (a: array 'a) (i: int31) (v: 'a) : unit writes {a}
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { a.elts = M.set (old a.elts) i v }

  (** unsafe get/set operations with no precondition *)

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int31)
    ensures { 0 <= i < a.length }
    ensures { result = a[i] }
    raises  { OutOfBounds -> i < 0 \/ i >= a.length }
  = if i < of_int 0 || i >= length a then raise OutOfBounds;
    a[i]

  let defensive_set (a: array 'a) (i: int31) (v: 'a)
    ensures { 0 <= i < a.length }
    ensures { a.elts = M.set (old a.elts) i v }
    raises  { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
  = if i < of_int 0 || i >= length a then raise OutOfBounds;
    a[i] <- v

  val make (n: int31) (v: 'a) : array 'a
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i:int. 0 <= i < n -> result[i] = v }
    ensures  { result.length = n }

  val append (a1: array 'a) (a2: array 'a) : array 'a
    ensures { result.length = a1.length + a2.length }
    ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < a2.length ->
              result[a1.length + i] = a2[i] }

  val sub (a: array 'a) (ofs: int31) (len: int31) : array 'a
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < len ->
               result[i] = a[ofs + i] }

  val copy (a: array 'a) : array 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < result.length -> result[i] = a[i] }

  val fill (a: array 'a) (ofs: int31) (len: int31) (v: 'a) : unit writes {a}
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs \/
        ofs + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. ofs <= i < ofs + len ->
               a[i] = v }

  val blit (a1: array 'a) (ofs1: int31)
                 (a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2}
    requires { 0 <= ofs1 /\ 0 <= len }
    requires { ofs1 + len <= a1.length }
    requires { 0 <= ofs2 /\
               ofs2 + len <= a2.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a2[i] = a1[ofs1 + i - ofs2] }

  val self_blit (a: array 'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
    writes {a}
    requires { 0 <= ofs1 /\ 0 <= len /\
               ofs1 + len <= a.length }
    requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a[i] = (old a)[ofs1 + i - ofs2] }

end

(** {2 Arrays with 63-bit indices}

    Contrary to arrays from module `Array`, the contents of the array
    is here modeled as a sequence. It makes it easier to resuse existing
    functions over sequences. (We may consider doing this for regular arrays
    as well in the future.)

    A coercion is declared so that an array `a` can be used
    as a sequence. As a consequence, notation `a[i]` in the logic is
    directly that of sequences. You have to import module `seq.Seq` to be
    able to use it.
*)

module Array63

  use int.Int
  use mach.int.Int63
  use seq.Seq

  type array 'a = private {
    mutable ghost elts : seq 'a;
                length : int63;
  } invariant { 0 <= length = Seq.length elts }

  meta coercion function elts

  val ([]) (a: array 'a) (i: int63) : 'a
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { result = a[i] }

  val ([]<-) (a: array 'a) (i: int63) (v: 'a) : unit writes {a}
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { a.elts = (old a.elts)[i <- v] }

  (** unsafe get/set operations with no precondition *)

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int63)
    ensures { 0 <= i < a.length }
    ensures { result = a[i] }
    raises  { OutOfBounds -> i < 0 \/ i >= a.length }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i]

  let defensive_set (a: array 'a) (i: int63) (v: 'a)
    ensures { 0 <= i < a.length }
    ensures { a.elts = (old a.elts)[i <- v] }
    raises  { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v

  val make (n: int63) (v: 'a) : array 'a
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i:int. 0 <= i < n -> result[i] = v }
    ensures  { result.length = n }

  val append (a1: array 'a) (a2: array 'a) : array 'a
    ensures { result.length = a1.length + a2.length }
    ensures { forall i:int. 0 <= i < a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < a2.length ->
              result[a1.length + i] = a2[i] }

  val sub (a: array 'a) (ofs: int63) (len: int63) : array 'a
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

  val copy (a: array 'a) : array 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < result.length -> result[i] = a[i] }

  val fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a) : unit
    writes   { a }
    requires { 0 <= ofs /\ 0 <= len }
    requires { ofs + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs \/
        ofs + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. ofs <= i < ofs + len ->
               a[i] = v }

  val blit (a1: array 'a) (ofs1: int63)
                 (a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2}
    requires { 0 <= ofs1 /\ 0 <= len }
    requires { ofs1 + len <= a1.length }
    requires { 0 <= ofs2 /\
               ofs2 + len <= a2.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a2[i] = a1[ofs1 + i - ofs2] }

  val self_blit (a: array 'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
    writes {a}
    requires { 0 <= ofs1 /\ 0 <= len /\
               ofs1 + len <= a.length }
    requires { 0 <= ofs2 /\ ofs2 + len <= a.length }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/
       ofs2 + len <= i < a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len ->
      a[i] = (old a)[ofs1 + i - ofs2] }

  let init (n: int63) (f: int63 -> 'a) : array 'a
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i: int63. 0 <= i < n -> result[i] = f i }
    ensures  { length result = n }
  = let a = make n (f 0) in
    for i = 1 to n - 1 do
      invariant { forall j: int63. 0 <= j < i -> a[j] = f j }
      a[i] <- f i
    done;
    a

end

module Array63Exchange

  use int.Int
  use mach.int.Int63
  use Array63
  use seq.Exchange as SE

  predicate exchange (a1 a2: array 'a) (i j: int) =
    SE.exchange a1.elts a2.elts i j
  (** `exchange a1 a2 i j` means that arrays `a1` and `a2` only differ
      by the swapping of elements at indices `i` and `j` *)

end

module Array63Swap

  use int.Int
  use mach.int.Int63
  use Array63
  use export Array63Exchange

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

end

module Array63Permut

  use int.Int
  use mach.int.Int63
  use Array63
  use seq.Seq
  use seq.SeqEq
  use seq.Permut as SP
  use Array63Exchange

  predicate permut (a1 a2: array 'a) (l u: int) =
    SP.permut a1.elts a2.elts l u
  (** `permut a1 a2 l u` is true when the segment
      `a1(l..u-1)` is a permutation of the segment `a2(l..u-1)`.
      Values outside of the interval `(l..u-1)` are ignored. *)

  predicate array_eq (a1 a2: array 'a) (l u: int) =
    seq_eq_sub a1.elts a2.elts l u

  predicate permut_sub (a1 a2: array 'a) (l u: int) =
    seq_eq_sub a1.elts a2.elts 0 l /\
    permut a1 a2 l u /\
    seq_eq_sub a1.elts a2.elts u (length a1)
  (** `permut_sub a1 a2 l u` is true when the segment
      `a1(l..u-1)` is a permutation of the segment `a2(l..u-1)`
      and values outside of the interval `(l..u-1)` are equal. *)

  predicate permut_all (a1 a2: array 'a) =
    SP.permut a1.elts a2.elts 0 a1.length
  (** `permut_all a1 a2 l u` is true when array `a1` is a permutation
      of array `a2`. *)

  (** we can always enlarge the interval *)
  lemma permut_sub_weakening:
    forall a1 a2: array 'a, l1 u1 l2 u2: int.
    permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
    permut_sub a1 a2 l2 u2

  lemma exchange_permut_sub:
    forall a1 a2: array 'a, i j l u: int.
    exchange a1 a2 i j -> l <= i < u -> l <= j < u ->
    0 <= l -> u <= length a1 -> permut_sub a1 a2 l u

  lemma exchange_permut_all:
    forall a1 a2: array 'a, i j: int.
    exchange a1 a2 i j -> permut_all a1 a2

end

(** {2 Arrays of 63-bit integers}

    Here the model is simply a sequence of integers (of type `int`),
    instead of being a sequence of values of type `int63`.

    As a consequence, we have to provide the additional information
    that each of the element fits within the bounds of 63-bit integers.

    Caveat: type `array63` below is not compatible with type
    `Array63.array int63`.
*)

module ArrayInt63

  use int.Int
  use mach.int.Int63
  use seq.Seq

  type array63 = private {
    mutable ghost elts: seq int;
            ghost size: int;
  } invariant { 0 <= size = length elts <= max_int }
    invariant { forall i. 0 <= i < length elts -> in_bounds elts[i] }

  meta coercion function elts

  val length (a: array63) : int63
    ensures { to_int result = a.length }

  val ([]) (a: array63) (i: int63) : int63
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { to_int result = a[i] }

  val ([]<-) (a: array63) (i: int63) (v: int63) : unit
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    writes   { a }
    ensures  { a.elts = (old a.elts)[i <- to_int v] }

  val ghost set (a: array63) (i: int63) (v: int63) : array63
    requires { [@expl:index in array bounds] 0 <= i < a.length }
    ensures  { result.length = a.length }
    ensures  { result.elts = a.elts[i <- to_int v] }

  val make (n: int63) (v: int63) : array63
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i. 0 <= i < n -> result[i] = to_int v }
    ensures  { result.length = n }

  val copy (a: array63) : array63
    ensures  { result.length = a.length }
    ensures  { forall i. 0 <= i < result.length -> result[i] = a[i] }

  let sub (a: array63) (ofs: int63) (len: int63) : array63
    requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
    ensures  { length result = len }
    ensures  { forall i. 0 <= i < len -> result[i] = a[ofs + i] }
  =
    let b = make len 0 in
    for i = 0 to len - 1 do
      invariant { forall k. 0 <= k < i -> b[k] = a[ofs+k] }
      b[i] <- a[ofs + i];
    done;
    b

  use seq.Exchange

  let swap (a:array63) (i j:int63) : unit
    requires { 0 <= i < length a /\ 0 <= j < length a }
    writes   { a }
    ensures  { exchange (old a) a i j }
  = let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

  let init (n: int63) (f: int63 -> int63) : array63
    requires { [@expl:array creation size] n >= 0 }
    ensures  { forall i: int63. 0 <= i < n -> result[i] = f i }
    ensures  { length result = n }
  =
    let a = make n 0 in
    for i = 0 to n - 1 do
      invariant { forall k: int63. 0 <= k < i -> a[k] = f k }
      a[i] <- f i
    done;
    a

end