add postcondition about return value and

prove it temporarily with admit