

(**

{1 In-place linked list reversal }

Version designed for the {h MPRI lecture ``Proof of Programs'' (http://www.lri.fr/~marche/MPRI-2-36-1/)}

This is an improved version of {h this
one}: it does not use any Coq proofs, but lemma functions instead.

*)

module InPlaceRev

  use map.Map
  use ref.Ref
  use int.Int
  use list.List
  use list.Quant as Q
  use list.Append
  use list.Mem
  use list.Length
  use export list.Reverse

  type loc

  val function eq_loc (l1 l2:loc) : bool
    ensures { result <-> l1 = l2 }

  val constant null : loc

  predicate disjoint (l1:list loc) (l2:list loc) =
    forall x:loc. not (mem x l1 /\ mem x l2)

  predicate no_repet (l:list loc) =
    match l with
    | Nil -> true
    | Cons x r -> not (mem x r) /\ no_repet r
    end

  let rec ghost mem_decomp (x: loc) (l: list loc)
    : (l1: list loc, l2: list loc)
    requires { mem x l }
    variant  { l }
    ensures  { l = l1 ++ Cons x l2 }
  = match l with
    | Nil -> absurd
    | Cons h t -> if eq_loc h x then (Nil,t) else
       let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
    end

  val acc (field: ref (map loc 'a)) (l:loc) : 'a
    requires { l <> null }
    reads { field }
    ensures { result = get !field l }

  val upd (field: ref (map loc 'a)) (l:loc) (v:'a):unit
    requires { l <> null }
    writes { field }
    ensures { !field = set (old !field) l v }

  inductive list_seg loc (map loc loc) (list loc) loc =
  | list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p
  | list_seg_cons: forall p q:loc, next:map loc loc, l:list loc.
      p <> null /\ list_seg (get next p) next l q ->
         list_seg p next (Cons p l) q

  let rec lemma list_seg_frame_ext (next1 next2:map loc loc)
    (p q r v: loc) (pM:list loc)
    requires { list_seg p next1 pM r }
    requires { next2 = set next1 q v }
    requires { not (mem q pM) }
    variant  { pM }
    ensures  { list_seg p next2 pM r }
  = match pM with
    | Nil -> ()
    | Cons h t ->
       assert { p = h };
       list_seg_frame_ext next1 next2 (get next1 p) q r v t
    end

  let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc)
    requires { list_seg p next l1 null }
    requires { list_seg p next l2 null }
    variant  { l1 }
    ensures  { l1 = l2 }
  = match l1,l2 with
    | Nil, Nil -> ()
    | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p)
    | _ -> absurd
    end

  let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc)
    requires { list_seg p next (l1 ++ Cons q l2) null }
    variant { l1 }
    ensures { list_seg q next (Cons q l2) null }
  = match l1 with
    | Nil -> ()
    | Cons _ r -> list_seg_sublistl next r l2 (get next p) q
    end

  let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc)
    requires { list_seg p next pM null }
    variant  { pM }
    ensures  { no_repet pM }
  = match pM with
    | Nil -> ()
    | Cons h t ->
      if mem h t then
         (* absurd case *)
         let (l1,l2) = mem_decomp h t in
         list_seg_sublistl next (Cons h l1) l2 p h;
         list_seg_functional next pM (Cons h l2) p;
         assert { length pM > length (Cons h l2) }
      else
        list_seg_no_repet next (get next p) t
    end

  let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc)
    requires { list_seg p next pM q }
    requires { list_seg q next qM r }
    variant  { pM }
    ensures  { list_seg p next (pM ++ qM) r }
  = match pM with
    | Nil -> ()
    | Cons _ t ->
      list_seg_append next (get next p) q r t qM
    end

  val next : ref (map loc loc)

  let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc
    requires { list_seg l1 !next l1M null }
    requires { list_seg l2 !next l2M null }
    requires { disjoint l1M l2M }
    ensures { list_seg result !next (l1M ++ l2M) null }
  =
    if eq_loc l1 null then l2 else
    let p = ref l1 in
    let ghost pM = ref l1M in
    let ghost l1pM = ref (Nil : list loc) in
    while not (eq_loc (acc next !p) null) do
      invariant { !p <> null }
      invariant { list_seg l1 !next !l1pM !p }
      invariant { list_seg !p !next !pM null }
      invariant { !l1pM ++ !pM = l1M }
      invariant { disjoint !l1pM !pM }
      variant   { !pM }
        match !pM with
        | Nil -> absurd
        | Cons h t ->
          pM := t;
          assert { disjoint !l1pM !pM };
          assert { not (mem h !pM) };
          l1pM := !l1pM ++ Cons h Nil;
        end;
        p := acc next !p
    done;
    upd next !p l2;
    assert { list_seg l1 !next !l1pM !p };
    assert { list_seg !p !next (Cons !p Nil) l2 };
    assert { list_seg l2 !next l2M null };
    l1

  let in_place_reverse (l:loc) (ghost lM:list loc) : loc
    requires { list_seg l !next lM null }
    ensures  { list_seg result !next (reverse lM) null }
  = let p = ref l in
    let ghost pM = ref lM in
    let r = ref null in
    let ghost rM = ref (Nil : list loc) in
    while not (eq_loc !p null) do
      invariant { list_seg !p !next !pM null }
      invariant { list_seg !r !next !rM null }
      invariant { disjoint !pM !rM }
      invariant { (reverse !pM) ++ !rM = reverse lM }
      variant   { !pM }
      let n = get !next !p in
      upd next !p !r;
      assert { list_seg !r !next !rM null };
      r := !p;
      p := n;
      match !pM with
      | Nil -> absurd
      | Cons h t -> rM := Cons h !rM; pM := t
      end
      done;
    !r

end

(** Using sequences instead of lists *)

module InPlaceRevSeq

  use int.Int
  use map.Map as Map
  use seq.Seq
  use seq.Mem
  use seq.Reverse

  type loc

  val function null: loc

  val function eq_loc (l1 l2:loc) : bool
    ensures { result <-> l1 = l2 }

  predicate disjoint (s1: seq 'a) (s2: seq 'a) =
    (* forall x:'a. not (mem x s1 /\ mem x s2) *)
    forall i1. 0 <= i1 < length s1 ->
    forall i2. 0 <= i2 < length s2 ->
    s1[i1] <> s2[i2]

  predicate no_repet (s: seq loc) =
    forall i. 0 <= i < length s -> not (mem s[i] s[i+1..])

  lemma non_empty_seq:
    forall s: seq 'a. length s > 0 ->
    s == cons s[0] s[1..]

  let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc)
    requires { mem x s }
    variant  { length s }
    ensures  { s == s1 ++ cons x s2 }
  =
    if eq_loc s[0] x then (empty, s[1..])
    else begin
      assert { s == cons s[0] s[1..] };
      let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2)
    end

  use ref.Ref

  type memory 'a = ref (Map.map loc 'a)

  val acc (field: memory 'a) (l:loc) : 'a
    requires { l <> null }
    reads    { field }
    ensures  { result = Map.get !field l }

  val upd (field: memory 'a) (l: loc) (v: 'a) : unit
    requires { l <> null }
    writes   { field }
    ensures  { !field = Map.set (old !field) l v }

  type next = Map.map loc loc

  predicate list_seg (next: next) (p: loc) (s: seq loc) (q: loc) =
    let n = length s in
    (forall i. 0 <= i < n -> s[i] <> null) /\
    (   (p = q /\ n = 0)
     \/ (1 <= n /\ s[0] = p /\ Map.get next s[n-1] = q /\
         forall i. 0 <= i < n-1 -> Map.get next s[i] = s[i+1]))

  lemma list_seg_frame_ext:
    forall next1 next2: next, p q r v: loc, pM: seq loc.
    list_seg next1 p pM r ->
    next2 = Map.set next1 q v ->
    not (mem q pM) ->
    list_seg next2 p pM r

  let rec lemma list_seg_functional (next: next) (l1 l2: seq loc) (p: loc)
    requires { list_seg next p l1 null }
    requires { list_seg next p l2 null }
    variant  { length l1 }
    ensures  { l1 == l2 }
  = if length l1 > 0 && length l2 > 0 then begin
      assert { l1[0] = l2[0] = p };
      list_seg_functional next l1[1..] l2[1..] (Map.get next p)
    end

  let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc)
    requires { list_seg next p l1 q }
    requires { length l1 > 0 }
    variant  { length l1 }
    ensures  { list_seg next (Map.get next p) l1[1..] q }
  = if length l1 > 1 then
      list_seg_tail next l1[1..] (Map.get next p) q

  let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc)
    requires { list_seg next p pM q }
    requires { list_seg next q qM r }
    variant  { length pM }
    ensures  { list_seg next p (pM ++ qM) r }
  =  if length pM > 0 then
      list_seg_append next (Map.get next p) q r pM[1..] qM

  lemma seq_tail_append:
    forall l1 l2: seq 'a.
    length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2

  let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc)
    requires { list_seg next p (l1 ++ cons q l2) null }
    variant  { length l1 }
    ensures  { list_seg next p l1 q }
  = if length l1 > 0 then begin
      list_seg_tail next (l1 ++ cons q l2) p null;
      list_seg_prefix next l1[1..] l2 (Map.get next p) q
    end

  let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc)
    requires { list_seg next p (l1 ++ cons q l2) null }
    variant  { length l1 }
    ensures  { list_seg next q (cons q l2) null }
  = assert { list_seg next p l1 q };
    if length l1 > 0 then begin
      list_seg_tail next l1 p q;
      list_seg_sublistl next l1[1..] l2 (Map.get next p) q
    end

  lemma get_tail:
    forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1]
  lemma tail_suffix:
    forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..]

  let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc)
    requires { list_seg next p pM null }
    variant  { length pM }
    ensures  { no_repet pM }
  = if length pM > 0 then begin
      let h = pM[0] in
      let t = pM[1..] in
      if mem h t then
         (* absurd case *)
         let (l1,l2) = mem_decomp h t in
         list_seg_sublistl next (cons h l1) l2 p h;
         list_seg_functional next pM (cons h l2) p;
         assert { length pM > length (cons h l2) }
      else begin
        assert { not (mem pM[0] pM[0+1..]) };
        list_seg_no_repet next (Map.get next p) t;
        assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) }
      end
    end

  val next : ref next

  let app (l1 l2: loc) (ghost l1M l2M: seq loc) : loc
    requires { list_seg !next l1 l1M null }
    requires { list_seg !next l2 l2M null }
    requires { disjoint l1M l2M }
    ensures  { list_seg !next result (l1M ++ l2M) null }
  =
    if eq_loc l1 null then l2 else
    let p = ref l1 in
    let ghost pM = ref l1M in
    let ghost l1pM = ref (empty : seq loc) in
    ghost list_seg_no_repet !next l1 l1M;
    while not (eq_loc (acc next !p) null) do
      invariant { !p <> null }
      invariant { list_seg !next l1 !l1pM !p }
      invariant { list_seg !next !p !pM null }
      invariant { !l1pM ++ !pM == l1M }
      invariant { disjoint !l1pM !pM }
      variant   { length !pM }
      assert { length !pM > 0 };
      assert { not (mem !p !l1pM) };
      let ghost t = !pM[1..] in
      ghost l1pM := !l1pM ++ cons !p empty;
      ghost pM := t;
      p := acc next !p
    done;
    upd next !p l2;
    assert { list_seg !next l1 !l1pM !p };
    assert { list_seg !next !p (cons !p empty) l2 };
    assert { list_seg !next l2 l2M null };
    l1

  let in_place_reverse (l:loc) (ghost lM: seq loc) : loc
    requires { list_seg !next l lM null }
    ensures  { list_seg !next result (reverse lM) null }
  = let p = ref l in
    let ghost pM = ref lM in
    let r = ref null in
    let ghost rM = ref (empty: seq loc) in
    while not (eq_loc !p null) do
      invariant { list_seg !next !p !pM null }
      invariant { list_seg !next !r !rM null }
      invariant { disjoint !pM !rM }
      invariant { (reverse !pM) ++ !rM == reverse lM }
      variant   { length !pM }
      let n = acc next !p in
      upd next !p !r;
      assert { list_seg !next !r !rM null };
      r := !p;
      p := n;
      rM := cons !pM[0] !rM;
      pM := !pM[1..]
    done;
    !r

end

(** This time with a fully automated proof.

    The key to a fully automated proof is to introduce an array of
    cells, called `cell` below, and then to resort to arithmetic and
    universal quantifiers to define lists (predicates `listLR` and
    `listRL` below).

    This proof requires no lemma function and no transformation.
    A single call to Z3 completes the proof in no time (0.04 s).
*)

module YetAnotherInPlaceRev

  use int.Int
  use map.Map

  type loc

  val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }

  val constant null : loc

  type mem = { mutable next: loc -> loc }

  val mem: mem

  let cdr (p: loc) : loc
    requires { p <> null }
    ensures  { result = mem.next p }
  = mem.next p

  let set_cdr (p: loc) (v: loc) : unit
    requires { p <> null }
    ensures  { mem.next = (old mem.next)[p <- v] }
  = let m = mem.next in
    mem.next <- fun x -> if x = p then v else m x

  predicate valid_cells (s: int -> loc) (n: int) =
    (forall i. 0 <= i < n -> s i <> null) &&
    (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)

  predicate listLR (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
    0 <= lo <= hi &&
    if lo = hi then l = null else
      l = s lo && m.next (s (hi-1)) = null &&
      forall k. lo <= k < hi-1 -> m.next (s k) = s (k+1)

  predicate listRL (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
    0 <= lo <= hi &&
    if lo = hi then l = null else
      m.next (s lo) = null && l = s (hi-1) &&
      forall k. lo < k < hi -> m.next (s k) = s (k-1)

  predicate frame (m1 m2: mem) (s: int -> loc) (n: int) =
    forall p. (forall i. 0 <= i < n -> p <> s i) ->
      m1.next p = m2.next p

  let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
    requires { valid_cells s n }
    requires { listLR mem s l 0 n }
    ensures  { listRL mem s r 0 n }
    ensures  { frame mem (old mem) s n }
  = let ref l = l in
    let ref p = null in
    let ghost ref i = 0 in
    while l <> null do
      invariant { if n = 0 then l = p = null else
                  i = 0     && p = null    && l = s 0
               || i = n     && p = s (n-1) && l = null
               || 0 < i < n && p = s (i-1) && l = s i }
      invariant { listRL mem s p 0 i }
      invariant { listLR mem s l i n }
      invariant { frame mem (old mem) s n }
      variant   { n - i }
      let tmp = l in
      l <- cdr l;
      set_cdr tmp p;
      p <- tmp;
      i <- i + 1
    done;
    return p

  let rec ghost predicate is_list (m: mem) (l: loc) (s: int -> loc) (n: int)
    requires { n >= 0 }
    variant  { n }
  = if n = 0 then l = null else
      l = s 0 <> null && is_list m (m.next l) (fun i -> s (i+1)) (n - 1)

  let rec lemma cells_of_list (l: loc) (s: int -> loc) (n: int)
    requires { n >= 0 }
    requires { is_list mem l s n }
    variant  { n }
    ensures  { valid_cells s n }
    ensures  { listLR mem s l 0 n }
  = if n <> 0 then cells_of_list (cdr l) (fun i -> s (i+1)) (n - 1)

  let rec lemma list_of_cells (r: loc) (s: int -> loc) (n: int)
    requires { n >= 0 }
    requires { valid_cells s n }
    requires { listRL mem s r 0 n }
    variant  { n }
    ensures  { is_list mem r (fun i -> s (n-1-i)) n }
  = if n <> 0 then list_of_cells (cdr r) s (n - 1)

  let list_reversal_final (ghost s) (ghost n: int) (l: loc) : (r: loc)
    requires { n >= 0 }
    requires { is_list mem l s n }
    ensures  { is_list mem r (fun i -> s (n-1-i)) n }
    ensures  { frame mem (old mem) s n }
  = cells_of_list l s n;
    let r = list_reversal s n l in
    list_of_cells r s n;
    r

end

(** On a null-terminated list, `list_reversal` terminates. We have shown it
    already e.g. in the previous module.

    But `list_reversal` actually terminates on *any* list, even when it
    contains a loop. Indeed, the code will reach the loop while reversing
    the initial segment, will reverse the loop, and then will restore the
    initial segment. So we end up with a list where only the loop has been
    reversed.

      before          +---o<--o<--+
                      v           |
          o-->o-->o-->o-->o-->o-->o

      after           +-->o-->o---+
                      |           V
          o-->o-->o-->o<--o<--o<--o

    In the module below, we show that `list_reversal` always terminates.
    This requires ruling out inifitely-long lists i.e. assuming a finite
    amount of memory.
*)
module Termination

  use int.Int
  use int.NumOf
  use map.Map

  type loc

  val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }

  val constant null : loc

  type mem = { mutable next: loc -> loc }

  val mem: mem

  let cdr (p: loc) : loc
    requires { p <> null }
    ensures  { result = mem.next p }
  = mem.next p

  let set_cdr (p: loc) (v: loc) : unit
    requires { p <> null }
    ensures  { mem.next = (old mem.next)[p <- v] }
  = let m = mem.next in
    mem.next <- fun x -> if x = p then v else m x

  (* Finite memory hypothesis: the list is entirely contained in a finite
     set `s` of `n` cells *)

  predicate valid_cells (s: int -> loc) (n: int) =
    (forall i. 0 <= i < n -> s i <> null) &&
    (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)

  predicate inside_memory (s: int -> loc) (n: int) (l: loc) =
    l = null || exists i. 0 <= i < n && l = s[i]

  predicate finite_memory (m: mem) (s: int -> loc) (n: int) =
    forall i. 0 <= i < n -> inside_memory s n (m.next s[i])

  (* The variant is lexicographic, as follows:

     - as long as we still discover new cells, we mark them with
       increasing numbers (with function `idx` below) and the number
       of unmarked cells decreases;

     - once we reach a marked cell, this means we are back in the initial
       segment and then the mark decreases.
  *)

  function seen (s: int -> loc) (idx: loc -> int) (lo hi: int) : int =
    numof (fun i -> idx s[i] > 0) lo hi

  let ghost set_idx (s: int -> loc) (n: int) (idx: loc -> int) (l: loc) (k: int)
    requires { valid_cells s n }
    requires { inside_memory s n l }
    requires { l <> null }
    requires { idx l = -1 }
    requires { k = seen s idx 0 n >= 0 }
    ensures  { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n }
  = assert { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n by
             exists il. 0 <= il < n && l = s[il] so
               seen s idx 0 n = seen s idx 0 il + seen s idx (il+1) n &&
               seen s idx[l <- k+1] 0 n =
                 seen s idx[l <- k+1] 0 il + 1 + seen s idx[l <- k+1] (il+1) n }

  let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
    requires { n >= 0 }
    requires { valid_cells s n }
    requires { finite_memory mem s n }
    requires { inside_memory s n l }
  = let ref l = l in
    let ref r = null in
    (* marking function: -1 for unmarked / 0 for null / >0 for marked *)
    let ghost ref idx = fun p -> if p = null then 0 else -1 in
    let ghost ref k = 0 in (* last mark *)
    while l <> null do
      invariant { inside_memory s n l }
      invariant { inside_memory s n r }
      invariant { finite_memory mem s n }
      invariant { k = seen s idx 0 n >= 0 }
      invariant { forall i. 0 <= i < n -> -1 <= idx s[i] <= k }
      invariant { forall p. idx p = 0 <-> p = null }
      invariant { if idx l = -1 then
                    idx r = k && forall i. 0 <= i < n ->
                    0 < idx s[i] -> idx (mem.next s[i]) = idx s[i] - 1
                  else forall i. 0 <= i < n ->
                    0 < idx s[i] <= idx l -> idx (mem.next s[i]) = idx s[i] - 1 }
      variant { n - k, 1 + idx l }
      if idx l = -1 then (set_idx s n idx l k; k <- k + 1; idx <- idx[l <- k]);
      let tmp = l in
      l <- cdr l;
      set_cdr tmp r;
      r <- tmp;
    done;
    return r

end
