Update 4/26

Roughly halfway done, hitting more CN issues as porting more. Working with UCam to understand/resolve. Making extra content for the tutorial in the form of personal notes, to be added to the tutorial in the future.

CN workflow is currently:

• something doesn't work
• look hard at the HTML output
• magic happens (needs very expert insight)
• thing is fixed

Would be very helpful to surface more insights – not necessarily more detail, but more helpful information.

Notes:

• Santiago: Useful debug technique is finding a minimal example that reproduces the bug. Drop these in the CN MM channel!
• Iavor: Would be great to note down what the tool could/should have done to help in these tricky/stuck cases.
• Mike: Try making an error diary – write down the mistake/annoyance/friction.

@peterohanley can you open a draft PR with the code you have so far?

To clarify - an appropriate span of a commit is a single file with ported specs.

Currently blocked, waiting for CN improvements.

• [CN] Inconsistent assumptions when declaring a struct with scalar elements unchanged rems-project/cerberus#399
• [CN] accesses causes inconsistent assumptions (in loop constructs - for / while)  rems-project/cerberus#551

@peterohanley are the issues listed above resolved now?

Blocked on GaloisInc/VERSE-Toolchain#124

Due date 12/4