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 CN crash caused by division / and modulus % cerberus#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: > ***@***.***> >