[CN] Tag specs as proof/test only (to retire the ability to break them up across magic comments)

[dc-mak]

This is an artefact of prior versions and should probably be disallowed (verbose, less to explain, less to document, cleaner code...)

cerberus/tests/cn/swap.c

Lines 3 to 8 in f83846a

	/*@ requires take pairStart = each (i32 j; 0i32 <= j && j < 2i32)
	{Owned(array_shift(pair, j))}; @*/
	/*@ ensures take pairEnd = each (i32 j; 0i32 <= j && j < 2i32)
	{Owned(array_shift(pair, j))}; @*/
	/*@ ensures pairEnd[0i32] == pairStart[1i32]; @*/
	/*@ ensures pairEnd[1i32] == pairStart[0i32]; @*/

[septract]

I'm in favor, but I think many of the examples in the example-archive don't conform to this standard. So some upgrade would be needed.

(edit: since I figured it out, this is a regex to find such cases using VS Code search: @\*/[\s\n]*/\*@\s*)

[dc-mak]

Unfortunately this is now being used with #ifdefs to include Fuliminate specs that can't be used with proof. Perhaps the solution would be to add the ability to tag particular clauses as proof or test only. Suggestions for syntax welcome.
https://github.com/GaloisInc/VERSE-OpenSUT/blob/1cb98cb8cf6e19a7a84047632777004e31adb087/components/mission_key_management/client.c#L252

[septract]

Yes, I think a better solution would be to be able to name or tag properties somehow. Eg:

requires [tag1, tag2] 
  <whatever> 
ensures 
  <whatever> 

$ cn verify --tags=tag1 file.c

This raises the awkward question at what granularity we want to tag though? Should each requires / ensures be taggable? What if some subset of tags makes the CN ill-formed, eg by referring to a name which is suppressed?

[dc-mak]

How about this as a halfway house: only boolean-valued assertions can be tagged as runtime(..);, which behaves similar to assert, except we skip proving it on the proof side? This is strictly better than the status quo, easy to implement, and I believe it covers all the existing use cases.

[septract]

Does this cover all use cases? We both have situations where we can prove things but not test them (due to limitations in the cn test tool), and situations where we can test things but not prove them (less surprising).

Just to push back a bit more - is there an actual problem caused by allowing split specifications?

[dc-mak]

Does this cover all use cases? We both have situations where we can prove things but not test them (due to limitations in the cn test tool), and situations where we can test things but not prove them (less surprising).

I meant "I believe" more as a conjecture, which is that I don't think we have anything currently where the difference is a take X = ...;, just boolean valued expressions (open to examples). I did try to search the OpenSUT code for more examples, but I found it difficult to sort through the results.

Just to push back a bit more - is there an actual problem caused by allowing split specifications?

Fair question; aside from the code for "merging specifications" being a bit fiddly, no.

For context, I discovered the issue when I was trying to unify the syntax for predicates (which can't be split) and specifications (which can) related to #811. My suspicion is that if we keep this, it will surprise users at some point, because the parsing and splitting does not work the way one might expect.¹

Footnotes

1. What actually goes on is that two full specifications, including accesses, trusted etc. are parsed, and the combined. Thankfully, accesses repeated can be interpreted as their union, trusted is idempotent, and requires can be omitted so it give the illusion of continuity. If a user write an ensures and then a requires, it currently errors. ↩