(** {1 McCarthy's "91" function}

authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
witness: Andrei Paskevich

*)

module McCarthy91

  use int.Int

  (** {2 Specification} *)

  function spec (x: int) : int = if x <= 100 then 91 else x-10

  (** {2 traditional recursive implementation} *)

  let rec f91 (n: int) : int
    ensures { result = spec n } variant { 101 - n }
  = if n <= 100 then
      f91 (f91 (n + 11))
    else
      n - 10

  (** {2 manually-optimized tail call} *)

  let rec f91_tco (n0: int) : int
    ensures { result = spec n0 } variant { 101 - n0 }
  = let ref n = n0 in
    while n <= 100 do
      invariant { n = n0 > 100 \/ n0 <= n <= 101 } variant { 101 - n }
      n <- f91_tco (n + 11)
    done;
    n - 10

  (** {2 non-recursive implementation using a while loop} *)

  use ref.Ref
  use int.Iter

  let f91_nonrec (n0: int): int
    ensures { result = spec n0 }
  = let ref e = 1 in
    let ref n = n0 in
    while e > 0 do
      invariant { e >= 0 /\ iter spec e n = spec n0 }
      variant   { 101 - n + 10 * e, e }
      if n > 100 then begin
        n <- n - 10;
        e <- e - 1
      end else begin
        n <- n + 11;
        e <- e + 1
      end
    done;
    n

  (** {2 irrelevance of control flow}

     We use a 'morally' irrelevant control flow from a recursive function
     to ease proof (the recursive structure does not contribute to the
     program execution). This is a technique for proving derecursified
     programs. See [verifythis_2016_tree_traversal] for a more
     complex example. *)

  exception Stop

  let f91_pseudorec (n0: int) : int
    ensures { result = spec n0 }
  = let ref e = 1 in
    let ref n = n0 in
    let bloc () : unit
      requires { e >= 0 }
      ensures { (old e) > 0 }
      ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
        else n = (old n) + 11 /\ e = (old e) + 1 }
      raises { Stop -> e = (old e) = 0 /\ n = (old n) }
    = if not (e > 0) then raise Stop;
      if n > 100 then begin
        n <- n - 10;
        e <- e - 1
      end else begin
        n <- n + 11;
        e <- e + 1
      end
    in
    let rec aux () : unit
      requires { e > 0 }
      variant { 101 - n }
      ensures { e = (old e) - 1 /\ n = spec (old n) }
      raises { Stop -> false }
    = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
    try aux (); bloc (); absurd
    with Stop -> n end


end

module McCarthyWithGhostMonitor


  use int.Int
  use ref.Ref

  function spec (x: int) : int = if x <= 100 then 91 else x-10

  (** {2 Variant using a general 'ghost coroutine' approach}

    Assume we want to prove the imperative code:
{h <pre>
e <- 1; r <- n;
loop
  if r > 100 { r <- r - 10; e <- e - 1; if e = 0 break }
        else { r <- r + 11; e <- e + 1 }
end-loop
</pre>}
we annotate the various program points:
{h <pre>
{ 0 } e <- 1;
{ 1 } r <- n;
      loop
{ 2 } if r > 100 then { 3 } r <- r - 10; { 4 } e <- e - 1; { 5 } if e=0 then break;
                 else { 6 } r <- r + 11; { 7 } e <- e + 1;
end-loop
{ 8 }
</pre>}

we define the small-step semantics of this code by the following [step] function

*)


  val ref pc : int
  val ref n : int
  val ref e : int
  val ref r : int

  val step () : unit
    requires { 0 <= pc < 8 }
    writes   { pc, e, r }
    ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = old r }
    ensures { old pc = 1 -> pc = 2 /\ e = old e /\ r = n }
    ensures { old pc = 2 /\ old r > 100 -> pc = 3 /\ e = old e /\ r = old r }
    ensures { old pc = 2 /\ old r <= 100 -> pc = 6 /\ e = old e /\ r = old r }
    ensures { old pc = 3 -> pc = 4 /\ e = old e /\ r = old r - 10 }
    ensures { old pc = 4 -> pc = 5 /\ e = old e - 1 /\ r = old r }
    ensures { old pc = 5 /\ old e = 0 -> pc = 8 /\ e = old e /\ r = old r }
    ensures { old pc = 5 /\ old e <> 0 -> pc = 2 /\ e = old e /\ r = old r }
    ensures { old pc = 6 -> pc = 7 /\ e = old e /\ r = old r + 11 }
    ensures { old pc = 7 -> pc = 2 /\ e = old e + 1 /\ r = old r }

  let rec monitor () : unit
    requires { pc = 2 /\ e > 0 }
    variant  { 101 - r }
    ensures  { pc = 5 /\ r = spec(old r) /\ e = old e - 1 }
  = step (); (* execution of 'if r > 100' *)
    if pc = 3 then begin
       step (); (* assignment r <- r - 10 *)
       step (); (* assignment e <- e - 1  *)
       end
    else begin
       step (); (* assignment r <- r + 11 *)
       step (); (* assignment e <- e + 1 *)
       monitor ();
       step (); (* 'if e=0' must be false *)
       monitor ()
       end

  let mccarthy ()
    requires { pc = 0 /\ n >= 0 }
    ensures { pc = 8 /\ r = spec n }
  = step (); (* assignment e <- 1 *)
    step (); (* assignment r <- n *)
    monitor (); (* loop *)
    step() (* loop exit *)

(** {2 a variant with not-so-small steps}

we annotate the important program points:
{h <pre>
{ 0 } e <- 1;
      r <- n;
      loop
{ 1 }   if r > 100 { r <- r - 10; e <- e - 1; { 2 } if e = 0 break; }
              else { r <- r + 11; e <- e + 1; }
      end-loop
end-while
{ 3 }
return r
</pre>}

we define the not-so-small-step semantics of this code by the following [next] function

*)

  val next () : unit
    requires { 0 <= pc < 3 }
    writes   { pc, e, r }
    ensures { old pc = 0 -> pc = 1 /\ e = 1 /\ r = n }
    ensures { old pc = 1 /\ old r > 100 ->
              pc = 2 /\ r = old r - 10 /\ e = old e - 1 }
    ensures { old pc = 1 /\ old r <= 100 ->
              pc = 1 /\ r = old r + 11 /\ e = old e + 1 }
    ensures { old pc = 2 /\ old e = 0 -> pc = 3 /\ r = old r /\ e = old e }
    ensures { old pc = 2 /\ old e <> 0 -> pc = 1 /\ r = old r /\ e = old e }

  (* [aux2] performs as may loop iterations as needed so as to reach program point 2
     from program point 1 *)
  let rec monitor2 () : unit
    requires { pc = 1 /\ e > 0 }
    variant  { 101 - r }
    ensures  { pc = 2 /\ r = spec(old r) /\ e = old e - 1 }
  = next ();
    if pc <> 2 then begin monitor2 (); next (); monitor2 () end


  let mccarthy2 ()
    requires { pc = 0 /\ n >= 0 }
    ensures { pc = 3 /\ r = spec n }
  = next (); (* assignments e <- 1; r <- n *)
    monitor2 (); (* loop *)
    next ()

end

module McCarthy91Mach

  use int.Int
  use mach.int.Int63

  function spec (x: int) : int = if x <= 100 then 91 else x-10

  let rec f91 (n: int63) : int63
    variant { 101 - n }
    ensures { result = spec n }
  = if n <= 100 then
      f91 (f91 (n + 11))
    else
      n - 10

  use mach.peano.Peano
  use mach.int.Refint63
  use int.Iter

  let f91_nonrec (n0: int63) : int63
    ensures { result = spec n0 }
  = let ref e = one in
    let ref n = n0 in
    while gt e zero do
      invariant { e >= 0 /\ iter spec e n = spec n0 }
      variant   { 101 - n + 10 * e, e:int }
      if n > 100 then begin
        n <- n - 10;
        e <- pred e
      end else begin
        n <- n + 11;
        e <- succ e
      end
    done;
    n

  exception Stop

  let f91_pseudorec (n0: int63) : int63
    ensures { result = spec n0 }
  = let ref e = one in
    let ref n = n0 in
    let bloc () : unit
      requires { e >= 0 }
      ensures { (old e) > 0 }
      ensures { if (old n) > 100 then n = (old n) - 10 /\ e = (old e) - 1
        else n = (old n) + 11 /\ e = (old e) + 1 }
      raises { Stop -> e = (old e) = 0 /\ n = (old n) }
    = if not (gt e zero) then raise Stop;
      if n > 100 then begin
        n := n - 10;
        e := pred e
      end else begin
        n := n + 11;
        e := succ e
      end
    in
    let rec aux () : unit
      requires { e > 0 }
      variant { 101 - n }
      ensures { e = (old e) - 1 /\ n = spec (old n) }
      raises { Stop -> false }
    = let u = n in bloc (); if u <= 100 then (aux (); aux ()) in
    try aux (); bloc (); absurd
    with Stop -> n end

end