Add contracts for SmallSort

[ShoyuVanilla]

Towards #56

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

@ShoyuVanilla Would you be able to revisit this PR?

[ShoyuVanilla]

@tautschnig I've tried some different approaches - mostly on my local repo, so not included in this draft - but most of them ran out of memory or took several tens of minutes due to the problem's complexities and kani's missing features. I'm planning to make some PRs to kani or learn verifast to deal with this. Would it be better to close this PR for now?

[tautschnig]

@tautschnig I've tried some different approaches - mostly on my local repo, so not included in this draft - but most of them ran out of memory or took several tens of minutes due to the problem's complexities and kani's missing features. I'm planning to make some PRs to kani or learn verifast to deal with this. Would it be better to close this PR for now?

Thank you for the immediate response! Entirely up to you how you deal with this PR, just wanted to make sure it hasn't been abandoned.

[rahulku]

Hi @ShoyuVanilla - any chance we can still push this through?

[ShoyuVanilla]

Hi @ShoyuVanilla - any chance we can still push this through?

Not for now. I need couple of months to study the related topics and VeriFast. (Actually, I'm quite new to these fields and studying Coq, Hoare and Separation Logic for now 😅) I'll close this for now and reopen with a new one when I'm ready. (I’m very willing to continue on this and other challenges)