Squashed commit of the following:

commit b404feb3
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 17:36:21 2019 +0200

    Bumped try_recv and recv to ofe st's

commit 4aa2399d
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 15:19:14 2019 +0200

    Finalised send proof

commit ae9857fc
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Wed Apr 17 14:58:34 2019 +0200

    Tweak.

commit 4d86571d
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Wed Apr 17 14:54:44 2019 +0200

    Work.

commit 0fedd453
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Wed Apr 17 12:55:52 2019 +0200

    Bumped Robbert feedback, WIP send st triple

commit f5672f9a
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 14:43:52 2019 +0200

    WIP

commit ef354c38
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:39:41 2019 +0200

    Lifted stype over OFEs. Fixed residuals in channel.v

commit 1a47979d
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:08:28 2019 +0200

    WIP

commit 605562ba
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue Apr 16 13:05:03 2019 +0200

    Test

commit 77eb6feb
Author: Robbert Krebbers <mail@robbertkrebbers.nl>
Date:   Mon Apr 15 16:24:13 2019 +0200

    Working.