original.name="Complex_Valid_10"
======
>>> main.whiley
// This is something of a performance test for the verifier because of
// the relatively large constants involved.  In particular, assigning
// a large constant array of 52 items to a variable with a type
// invariant.
//
// I suppose we could consider this a stretch goal of sorts.  In
// particular, it'll be an exciting day when Whiley can verify this in
// any reasonable amount of time...
type nat is (int x) where x >= 0

// =======================================
// Card Definition
// =======================================

// Suites
final int HEARTS = 1
final int CLUBS = 2
final int DIAMONDS = 3
final int SPADES = 4

// Ordinals
final int TWO = 2
final int THREE = 3
final int FOUR = 4
final int FIVE = 5
final int SIX = 6
final int SEVEN = 7
final int EIGHT = 8
final int NINE = 9
final int TEN = 10
final int JACK = 11
final int QUEEN = 12
final int KING = 13
final int ACE = 14

type Card is { int suite, int ordinal }
// Suite between hearts and clubs
where HEARTS <= suite && suite <= SPADES
// Ordinal between 2 and ACE (high)
where 2 <= ordinal && ordinal <= ACE

// Define a "comparator" for cards
property lessThan(Card c1, Card c2) -> bool:
    return (c1.suite < c2.suite) || (c1.suite == c1.suite && c1.ordinal < c2.ordinal)

property sorted(Card[] cards) -> bool:
    return |cards| == 0 || all { i in 1..|cards| | lessThan(cards[i-1],cards[i]) }

// =======================================
// Card Constants
// =======================================

final Card TWO_HEARTS = { suite: HEARTS, ordinal: TWO }
final Card THREE_HEARTS = { suite: HEARTS, ordinal: THREE }
final Card FOUR_HEARTS = { suite: HEARTS, ordinal: FOUR }
final Card FIVE_HEARTS = { suite: HEARTS, ordinal: FIVE }
final Card SIX_HEARTS = { suite: HEARTS, ordinal: SIX }
final Card SEVEN_HEARTS = { suite: HEARTS, ordinal: SEVEN }
final Card EIGHT_HEARTS = { suite: HEARTS, ordinal: EIGHT }
final Card NINE_HEARTS = { suite: HEARTS, ordinal: NINE }
final Card TEN_HEARTS = { suite: HEARTS, ordinal: TEN }
final Card JACK_HEARTS = { suite: HEARTS, ordinal: JACK }
final Card QUEEN_HEARTS = { suite: HEARTS, ordinal: QUEEN }
final Card KING_HEARTS = { suite: HEARTS, ordinal: KING }
final Card ACE_HEARTS = { suite: HEARTS, ordinal: ACE }

final Card TWO_CLUBS = { suite: CLUBS, ordinal: TWO }
final Card THREE_CLUBS = { suite: CLUBS, ordinal: THREE }
final Card FOUR_CLUBS = { suite: CLUBS, ordinal: FOUR }
final Card FIVE_CLUBS = { suite: CLUBS, ordinal: FIVE }
final Card SIX_CLUBS = { suite: CLUBS, ordinal: SIX }
final Card SEVEN_CLUBS = { suite: CLUBS, ordinal: SEVEN }
final Card EIGHT_CLUBS = { suite: CLUBS, ordinal: EIGHT }
final Card NINE_CLUBS = { suite: CLUBS, ordinal: NINE }
final Card TEN_CLUBS = { suite: CLUBS, ordinal: TEN }
final Card JACK_CLUBS = { suite: CLUBS, ordinal: JACK }
final Card QUEEN_CLUBS = { suite: CLUBS, ordinal: QUEEN }
final Card KING_CLUBS = { suite: CLUBS, ordinal: KING }
final Card ACE_CLUBS = { suite: CLUBS, ordinal: ACE }

final Card TWO_DIAMONDS = { suite: DIAMONDS, ordinal: TWO }
final Card THREE_DIAMONDS = { suite: DIAMONDS, ordinal: THREE }
final Card FOUR_DIAMONDS = { suite: DIAMONDS, ordinal: FOUR }
final Card FIVE_DIAMONDS = { suite: DIAMONDS, ordinal: FIVE }
final Card SIX_DIAMONDS = { suite: DIAMONDS, ordinal: SIX }
final Card SEVEN_DIAMONDS = { suite: DIAMONDS, ordinal: SEVEN }
final Card EIGHT_DIAMONDS = { suite: DIAMONDS, ordinal: EIGHT }
final Card NINE_DIAMONDS = { suite: DIAMONDS, ordinal: NINE }
final Card TEN_DIAMONDS = { suite: DIAMONDS, ordinal: TEN }
final Card JACK_DIAMONDS = { suite: DIAMONDS, ordinal: JACK }
final Card QUEEN_DIAMONDS = { suite: DIAMONDS, ordinal: QUEEN }
final Card KING_DIAMONDS = { suite: DIAMONDS, ordinal: KING }
final Card ACE_DIAMONDS = { suite: DIAMONDS, ordinal: ACE }

final Card TWO_SPADES = { suite: SPADES, ordinal: TWO }
final Card THREE_SPADES = { suite: SPADES, ordinal: THREE }
final Card FOUR_SPADES = { suite: SPADES, ordinal: FOUR }
final Card FIVE_SPADES = { suite: SPADES, ordinal: FIVE }
final Card SIX_SPADES = { suite: SPADES, ordinal: SIX }
final Card SEVEN_SPADES = { suite: SPADES, ordinal: SEVEN }
final Card EIGHT_SPADES = { suite: SPADES, ordinal: EIGHT }
final Card NINE_SPADES = { suite: SPADES, ordinal: NINE }
final Card TEN_SPADES = { suite: SPADES, ordinal: TEN }
final Card JACK_SPADES = { suite: SPADES, ordinal: JACK }
final Card QUEEN_SPADES = { suite: SPADES, ordinal: QUEEN }
final Card KING_SPADES = { suite: SPADES, ordinal: KING }
final Card ACE_SPADES = { suite: SPADES, ordinal: ACE }

// =======================================
// DECK
// =======================================

type Deck is (Card[] cards)
// Exactly 52 cards in a deck
where |cards| == 52
// No two cards are the same in a deck
where all { i in 0..|cards|, j in 0..|cards| | (i != j) ==> (cards[i] != cards[j]) }

// A real test of verifier performance!!
final Deck deck = [
        // Hearts
        TWO_HEARTS,
        THREE_HEARTS,
        FOUR_HEARTS,
        FIVE_HEARTS,
        SIX_HEARTS,
        SEVEN_HEARTS,
        EIGHT_HEARTS,
        NINE_HEARTS,
        TEN_HEARTS,
        JACK_HEARTS,
        QUEEN_HEARTS,
        KING_HEARTS,
        ACE_HEARTS,
        // Clubs
        TWO_CLUBS,
        THREE_CLUBS,
        FOUR_CLUBS,
        FIVE_CLUBS,
        SIX_CLUBS,
        SEVEN_CLUBS,
        EIGHT_CLUBS,
        NINE_CLUBS,
        TEN_CLUBS,
        JACK_CLUBS,
        QUEEN_CLUBS,
        KING_CLUBS,
        ACE_CLUBS,
        // Diamonds
        TWO_DIAMONDS,
        THREE_DIAMONDS,
        FOUR_DIAMONDS,
        FIVE_DIAMONDS,
        SIX_DIAMONDS,
        SEVEN_DIAMONDS,
        EIGHT_DIAMONDS,
        NINE_DIAMONDS,
        TEN_DIAMONDS,
        JACK_DIAMONDS,
        QUEEN_DIAMONDS,
        KING_DIAMONDS,
        ACE_DIAMONDS,
        // Spades
        TWO_SPADES,
        THREE_SPADES,
        FOUR_SPADES,
        FIVE_SPADES,
        SIX_SPADES,
        SEVEN_SPADES,
        EIGHT_SPADES,
        NINE_SPADES,
        TEN_SPADES,
        JACK_SPADES,
        QUEEN_SPADES,
        KING_SPADES,
        ACE_SPADES
    ]

// =======================================
// RANDOM
// =======================================
type Random is {nat index, nat[] sequence}
// index is valid position in random sequence
where index < |sequence|
// Sequence is valid card index
where all { i in 0..|sequence| | sequence[i] < 52 }

function Random(nat[] sequence) -> Random
requires |sequence| > 0
requires all { i in 0..|sequence| | sequence[i] < 52 }:
    return { index: 0, sequence: sequence }

function next(Random r) -> (nat index, Random nr)
ensures index < 52:
    // Get item from random sequence
    nat result = r.sequence[r.index]
    // Move to next item
    nat tmp = r.index + 1
    // Check for overflow
    if tmp == |r.sequence|:
        tmp = 0
    //
    r.index = tmp
    //
    return result, r

// =======================================
// SHUFFLE
// =======================================

function swap(Deck deck, nat from, nat to) -> Deck
requires from < 52 && to < 52:
    // Create copy of deck, which is necessary to temporarily break the
    // invariant.
    Card[] tmp = deck
    // Swap two cards around    
    tmp[from] = deck[to]
    tmp[to] = deck[from]
    //
    return deck

// "Randomly" shuffle the deck
function shuffle(Deck deck, Random rand, nat count) -> Deck:
    //
    nat i = 0
    //
    while i < count:
       nat from
       nat to    
       (from,rand) = next(rand)
       (to,rand) = next(rand)
       deck = swap(deck,from,to)
       i = i + 1
    //
    return deck
    
// =======================================
// TEST
// =======================================

public export method test():
    // Not a very long "random" sequence
    Random rand = Random([51,43,33,45,22,21,6,0,11,12,14])
    // Shuffle the deck ten times
    Deck d = shuffle(deck,rand,10)
    //
    assert |d| == 52
---