[FEATURE] CN for encoding abstract state machines (ASMs)

[podhrmic]

Summary

Add syntactic sugar for handling ASMs in CN. This should translate to appropriate ghost variables / specs. The goal is to specify stateful behavior of code, and check that the implementation matches this behavior.

Do

• find a simple example based on the OpenSUT code (e.g. calling crypto operations in a specific order)
• review relevant ASM languages - specifically SRI-SAL, ASMETA and the graphical language Stateflow
• review relevant FSM languages (as FSM might be sufficient for our purposes) - such as SDL
• sketch notional CN syntax for such an example - do we need to explicitly model the ASM at the code level? Or should it be for example only visual, and then appropriate CN specs are autogenerated? How are errors reported?
• write down your findings and recommendations