Toccata

(*
  Unraveling a Card Trick
  Tony Hoare and Natarajan Shankar
  Time for Verification
  Lecture Notes in Computer Science, 2010, Volume 6200/2010, 195-201,
  DOI: 10.1007/978-3-642-13754-9_10
  http://www.springerlink.com/content/gn18673357154448/
*)

theory GilbreathCardTrickPure

  use export int.Int
  use option.Option
  use export list.List
  use export list.Length
  use export list.Append
  use export list.Reverse
  use list.Nth

  constant m: int
  axiom m_positive: 0 < m

  constant n: int
  axiom n_nonnegative: 0 <= n

  (* c is a riffle shuffle of a and b *)
  inductive shuffle (a b c: list 'a) =
  | Shuffle_nil_left:
      forall l: list 'a. shuffle l Nil l
  | Shuffle_nil_right:
      forall l: list 'a. shuffle Nil l l
  | Shuffle_cons_left:
      forall x: 'a, a b c: list 'a.
      shuffle a b c -> shuffle (Cons x a) b (Cons x c)
  | Shuffle_cons_right:
      forall x: 'a, a b c: list 'a.
      shuffle a b c -> shuffle a (Cons x b) (Cons x c)

  lemma shuffle_nil_nil_nil: shuffle Nil Nil (Nil: list 'a)

  lemma shuffle_sym:
     forall a b c: list 'a. shuffle a b c -> shuffle b a c

  lemma shuffle_length:
    forall a b c: list 'a. shuffle a b c -> length a + length b = length c

  (* the list l is composed of n blocks, each being 0,1,...,m-1 *)
  predicate suit_ordered (l: list int) =
    forall i j: int. 0 <= i < n -> 0 <= j < m -> nth (i * m + j) l = Some j

  (* the list l is a sequence of n blocks,
     each being a permutation of 0,1,...,m-1 *)
  predicate suit_sorted (l: list int) =
    (forall i v: int. nth i l = Some v -> 0 <= v < m) /\
    (forall i j1 j2: int. 0 <= i < n -> 0 <= j1 < m -> 0 <= j2 < m ->
     nth (i * m + j1) l <> nth (i * m + j2) l)

  (* TODO: prove it! *)
  axiom gilbreath_card_trick:
    forall a: list int. length a = n * m -> suit_ordered a ->
    forall c d: list int. a = c ++ d ->
    forall b: list int. shuffle c (reverse d) b -> suit_sorted b

end

(* a program implementing the card trick using stacks *)
module GilbreathCardTrick

  use GilbreathCardTrickPure
  use stack.Stack

  let shuffle (a b: t int)
    ensures { a.elts = Nil /\ b.elts = Nil /\
      shuffle (reverse (old a.elts)) (reverse (old b.elts)) result.elts }
  = let c = create () in
    let ghost a' = create () in
    let ghost b' = create () in
    while not (is_empty a && is_empty b) do
      invariant { reverse (old a.elts) = reverse a.elts ++ a'.elts }
      invariant { reverse (old b.elts) = reverse b.elts ++ b'.elts }
      invariant { shuffle a'.elts b'.elts c.elts }
      variant   { length a + length b }
      if not (is_empty a) && (is_empty b || any bool) then begin
        ghost (push (safe_top a) a');
        push (safe_pop a) c
      end else begin
        ghost (push (safe_top b) b');
        push (safe_pop b) c
      end
    done;
    c

  let card_trick (a: t int)
    requires { length a = n*m /\ suit_ordered a.elts }
    ensures { length result = n*m && suit_sorted result.elts }
  = (* cut a into c;d and reverse d in d_ *)
    let d_ = create () in
    let cut = any int ensures { 0 <= result <= n*m } in
    for i = 1 to cut do
      invariant { length a = n*m-i+1 /\ length d_ = i-1 /\
                  old a.elts = reverse d_.elts ++ a.elts }
      push (safe_pop a) d_
    done;
    assert { old a.elts = reverse d_.elts ++ a.elts };
    (* then suffle c (that is a) and d_ to get b *)
    shuffle a d_

end