[FEATURE] Write CN specs for selected Lynx code

[podhrmic]

Summary

Look at the files of interest from LynxOS and the desired properties referenced by Will, and try to implement CN specs for each example.

The examples / code has to stay in https://gitlab-int.galois.com/verse/lynxos178

Acceptance Criteria

All examples/files of interest have been examined. Document each example as you walk through the following steps:

1. run CN on the file/function of interest and look for undefined behavior (UB)
2. add specs such that no UB occurs
3. add specs for other properties and/or summarize if/why such properties cannot be written
4. if you encounter CN bugs, open CN issues

[podhrmic]

It would be valuable to write enough specs to see how we would approach verification of the code, specifically the portion where the child objects have pointers to their parents.