Integrate examples from the `example-archive` into the tutorial

[septract]

The example-archive directory has some nice examples that should be propagated back into the tutorial, with supporting text. In particular:

• [ ] linear search
• [ ] binary search (after fixing https://github.com/rems-project/cerberus/issues/231)

This issue migrated from https://github.com/GaloisInc/VERSE-Toolchain/issues/31

[septract]

cc @bcpierce00

[bcpierce00]

Do we have division now?

• B

On Tue, Jul 9, 2024 at 3:51 PM Mike Dodds @.***> wrote:

cc @bcpierce00 https://urldefense.com/v3/__https://github.com/bcpierce00__;!!IBzWLUs!SSkroFj-cnIHmeHrfvn6jdorzLrR2HeABGITwxT2jBHoNj56ImI0Fqkm1AsqXoJKLlA3O-mewXXKJJ_E0yE8bMYsItqt$

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2218551545__;Iw!!IBzWLUs!SSkroFj-cnIHmeHrfvn6jdorzLrR2HeABGITwxT2jBHoNj56ImI0Fqkm1AsqXoJKLlA3O-mewXXKJJ_E0yE8bHUXmkDP$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC2S2POYRQKMRGDNHQLZLQ5JBAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMJYGU2TCNJUGU__;!!IBzWLUs!SSkroFj-cnIHmeHrfvn6jdorzLrR2HeABGITwxT2jBHoNj56ImI0Fqkm1AsqXoJKLlA3O-mewXXKJJ_E0yE8bAsBs0iy$ . You are receiving this because you were mentioned.Message ID: @.***>

[septract]

No, so that example is pending the issue I pointed to. I think there's a draft PR from Apol but I don't know how far they have got

[bcpierce00]

I see that he's going back and forth with Dhruv about a PR, so hopefully soon...

On Wed, Jul 10, 2024 at 1:33 PM Mike Dodds @.***> wrote:

No, so that example is pending the issue I pointed to. I think there's a draft PR from Apol but I don't know how far they have got

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2221085527__;Iw!!IBzWLUs!VSpjCeEUOw3qW5VTNsL8smRi47RsUEgCIfvknVJ8stkJ22E4cwS4njpRqQX7VcMIJxM7j9jZ9oOYHA1x2LLM27uHt8Ha$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC6GJAHRUD7QMRQG6ALZLVV5NAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMRRGA4DKNJSG4__;!!IBzWLUs!VSpjCeEUOw3qW5VTNsL8smRi47RsUEgCIfvknVJ8stkJ22E4cwS4njpRqQX7VcMIJxM7j9jZ9oOYHA1x2LLM20eyfgUk$ . You are receiving this because you were mentioned.Message ID: @.***>

[bcpierce00]

This should be unblocked now I think…

On Wed, Jul 10, 2024 at 13:49 Benjamin Pierce @.***> wrote:

I see that he's going back and forth with Dhruv about a PR, so hopefully soon...

On Wed, Jul 10, 2024 at 1:33 PM Mike Dodds @.***> wrote:

No, so that example is pending the issue I pointed to. I think there's a draft PR from Apol but I don't know how far they have got

— Reply to this email directly, view it on GitHub < https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2221085527__;Iw!!IBzWLUs!VSpjCeEUOw3qW5VTNsL8smRi47RsUEgCIfvknVJ8stkJ22E4cwS4njpRqQX7VcMIJxM7j9jZ9oOYHA1x2LLM27uHt8Ha$>,

or unsubscribe < https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC6GJAHRUD7QMRQG6ALZLVV5NAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMRRGA4DKNJSG4__;!!IBzWLUs!VSpjCeEUOw3qW5VTNsL8smRi47RsUEgCIfvknVJ8stkJ22E4cwS4njpRqQX7VcMIJxM7j9jZ9oOYHA1x2LLM20eyfgUk$>

. You are receiving this because you were mentioned.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2221111773__;Iw!!IBzWLUs!QbVWqLCcvwB8nSKEgUEx7l-VZrn9Ifl1dQ4Gr90D_W9QQignAJgUqIDlHsqsdnN21HiUpt6P_RjpgYnvK0gnSkq3DBCE$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC6MADN25EISKTYMETLZLVX3FAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMRRGEYTCNZXGM__;!!IBzWLUs!QbVWqLCcvwB8nSKEgUEx7l-VZrn9Ifl1dQ4Gr90D_W9QQignAJgUqIDlHsqsdnN21HiUpt6P_RjpgYnvK0gnShCfnRu-$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[septract]

@bcpierce00 I could take a shot at writing these up? Might be a week or two until I get time. Is the best method to generate a PR and then ask you / @cp526 for review?

[cp526]

Sounds good to me.

[bcpierce00]

Sounds great to me too!

On Mon, Jul 22, 2024 at 9:17 AM Christopher Pulte @.***> wrote:

Sounds good to me.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2242939135__;Iw!!IBzWLUs!SeglQtr2dyEwbAoT-K-vRMKd0i8EDUP5ddDRqFBsBbElIO9IX-zECYDMsC7PHfC22yznO0guoElutSzJIGSmVBmHW1e5$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC74IOJGUIK7OOOUI7TZNUA7HAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBSHEZTSMJTGU__;!!IBzWLUs!SeglQtr2dyEwbAoT-K-vRMKd0i8EDUP5ddDRqFBsBbElIO9IX-zECYDMsC7PHfC22yznO0guoElutSzJIGSmVO8HwZJY$ . You are receiving this because you were mentioned.Message ID: @.***>

[bcpierce00]

If you want to discuss where they belong / how best to integrate, you know where to find us.

On Mon, Jul 22, 2024 at 10:20 AM Benjamin Pierce @.***> wrote:

Sounds great to me too!

On Mon, Jul 22, 2024 at 9:17 AM Christopher Pulte < @.***> wrote:

Sounds good to me.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/39*issuecomment-2242939135__;Iw!!IBzWLUs!SeglQtr2dyEwbAoT-K-vRMKd0i8EDUP5ddDRqFBsBbElIO9IX-zECYDMsC7PHfC22yznO0guoElutSzJIGSmVBmHW1e5$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC74IOJGUIK7OOOUI7TZNUA7HAVCNFSM6AAAAABKTQLKUWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBSHEZTSMJTGU__;!!IBzWLUs!SeglQtr2dyEwbAoT-K-vRMKd0i8EDUP5ddDRqFBsBbElIO9IX-zECYDMsC7PHfC22yznO0guoElutSzJIGSmVO8HwZJY$ . You are receiving this because you were mentioned.Message ID: @.***>