// Shuffling a deck of cards..
// December 2009
// Author: Levent Erkok, Galois, Inc.
// This file is in the public domain

// For details, see: http://en.wikipedia.org/wiki/Shuffle

bisect : {a b} (fin a) => [2*a]b -> ([a]b, [a]b);
bisect xs = (take (w, xs), drop (w, xs))
  where w = width xs / 2;

outShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;
outShuffle xs = join [| [x y] || x <- fh || y <- sh |]
  where (fh, sh) = bisect xs;

inShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;
inShuffle xs = join [| [y x] || x <- fh || y <- sh |]
  where (fh, sh) = bisect xs;

// Helper function; repeated applications of a function:
iterate : {a} (a -> a, a) -> [inf]a;
iterate (f, x) = [x] # iterate (f, f x);

outShuffles, inShuffles : {a b} (fin a) => [2*a]b -> [inf][2*a]b;
outShuffles xs = iterate(outShuffle, xs);
inShuffles  xs = iterate(inShuffle, xs);

// Represent the deck as 52 things each of which is 6 bits wide..
// This is not a perfect representation, but good enough..
type Deck = [52][6];

// Prove that 8 outShuffles restore the deck:
outShuffle8 : Deck -> Bit;
theorem outShuffle8: {deck}. outShuffles(deck) @ 8 == deck;

// No sequence of outShuffles will ever reverse a deck;
// In fact, the first card will never change.
// We can formally prove this as follows:
outShuffleFirstCard : Deck -> Bit;
theorem outShuffleFirstCard: {deck}. outShuffle deck @ 0 == deck @ 0;

// Prove that 26 inShuffles reverse the deck:
inShuffle26Rev : Deck -> Bit;
theorem inShuffle26Rev : {deck}. inShuffles(deck) @ 26 == reverse deck;

// Prove that 52 inShuffles restore the deck; this one is
// obvious after the previous theorem..
inShuffle52 : Deck -> Bit;
theorem inShuffle52: {deck}. inShuffles(deck) @ 52 == deck;

// Mongean shuffle
// Note the extra dummy constraint we need to add for the type
monge xs = reverse odds # evens
  where { w = width xs;
          evens = xs @@ [0 2 .. (w-1)];
          odds  = xs @@ [1 3 .. (w-1)]
        };

monges xs = iterate(monge, xs);

// Prove that 12 monge shuffles restore the deck:
monge12 : Deck -> Bit;
theorem monge12: {deck}. monges(deck) @ 12 == deck;