> for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences.

If you just require that the result be sorted, then this is a valid sort:

  def sorted(ls):
    return []

If you require that it be sorted and contain the same items (but don't check the count), then this is technically sufficient (I've abstracted the actual sort operation out):

  def sorted(ls):
    ls = list(set(ls)) # removes duplicates
    # perform sort
    return result

If you get to the right post-condition, it has to have the same items and the same count and be sorted, then it will satisfy this test:

  def sorted_postcondition(original, result):
    return all(x <= y for x, y in pairwise(result)) and Counter(original) == Counter(result) # Counter is being used as a multiset