Some parts of the language are not discussed in the tutorial

[peterohanley]

• [x] cn_function
• [x] pack
• [ ] bitwise functions (operators are not present in the logical language)
• [ ] instantiate ("extract for pure quantifiers")

[bcpierce00]

I've made a note of these at the end of tutorial.adoc

On Fri, Apr 26, 2024 at 12:08 PM peterohanley @.***> wrote:

• cn_function
• pack
• bitwise functions (operators are not present in the logical language)

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/4__;!!IBzWLUs!XU0VdtYNPl5m6Qam-p51cXbel4aYHCdmdSzvr8gPBD2lDAofrzAaOFZrNU7tQDXOcPVsDiz9gjmkqwkzQKeyAdvm59xF$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC3RHQJO4G2BYGQN74LY7J3ZNAVCNFSM6AAAAABG3BMS5SVHI2DSMVQWIX3LMV43ASLTON2WKOZSGI3DMMBZGQ4DMOI__;!!IBzWLUs!XU0VdtYNPl5m6Qam-p51cXbel4aYHCdmdSzvr8gPBD2lDAofrzAaOFZrNU7tQDXOcPVsDiz9gjmkqwkzQKeyATacaboi$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[dc-mak]

https://github.com/rems-project/cerberus/issues/230#issuecomment-2077777421

Just adding here so that it's logged somewhere. You can also have arguments, but the most common case is for constants.

[dc-mak]

And this (MIN/MAX{u,i}{8,16,32,64})... https://github.com/rems-project/cerberus/blob/02a6f66f57c9a28c683a3e3cb569a6300adae1a9/tests/cn/max_min_consts.c

[peterohanley]

It's possible sometimes to write Owned(p) instead of Owned<...>(p) but this is only used in a malloc example, never explicitly mentioned.

[samcowger]

I also don't see any mention of instantiate in the tutorial. It turned out to be necessary for a spec that I wanted to write, which I hope to include in the archive via #49. That example turned out to be a good way for me and @septract to learn about the semantics of instantiate - perhaps it (or something like it) would be a good addition to the tutorial as well.

[bcpierce00]

Would you be willing to write up the example in the style of the tutorial and add an exercise or two (or three) to give readers a chance to try it out themselves? (Just bullet points is fine if you are pressed for time, but it's really helpful to capture the experience of "oh, here's what I would have needed to be explained to understand how to use this for what I wanted..." from the inside!)

On Fri, Jul 19, 2024 at 7:24 PM Sam Cowger @.***> wrote:

I also don't see any mention of instantiate in the tutorial. It turned out to be necessary for a spec that I wanted to write, which I hope to include in the archive via #49 https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/pull/49__;!!IBzWLUs!QH6_ep_FZ98wtBDCrVPNgFG9q1RxiXlhaOgzYDEN15PuJbpr9osO-GoKEyc5EC-gSUAd-cmlrRd6zwQxUCnKpD8m2dcH$. That example turned out to be a good way for me and @septract https://urldefense.com/v3/__https://github.com/septract__;!!IBzWLUs!QH6_ep_FZ98wtBDCrVPNgFG9q1RxiXlhaOgzYDEN15PuJbpr9osO-GoKEyc5EC-gSUAd-cmlrRd6zwQxUCnKpBNIFW3v$ to learn about the semantics of instantiate - perhaps it (or something like it) would be a good addition to the tutorial as well.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/4*issuecomment-2240627504__;Iw!!IBzWLUs!QH6_ep_FZ98wtBDCrVPNgFG9q1RxiXlhaOgzYDEN15PuJbpr9osO-GoKEyc5EC-gSUAd-cmlrRd6zwQxUCnKpNsc21Vh$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC73VD3NNJDW7IR5W53ZNGN37AVCNFSM6AAAAABG3BMS5SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENBQGYZDONJQGQ__;!!IBzWLUs!QH6_ep_FZ98wtBDCrVPNgFG9q1RxiXlhaOgzYDEN15PuJbpr9osO-GoKEyc5EC-gSUAd-cmlrRd6zwQxUCnKpKHTj-T8$ . You are receiving this because you commented.Message ID: @.***>

[samcowger]

Sure, I'll do that.

[septract]

We have now disabled pack / unpack, and declared cn_function experimental. So I don't think we need to discuss them in the tutorial.

This still leaves bitwise functions and instantiate.