sosy-lab/sv-witnesses

Add a way to specify witness format versions

MartinSpiessl opened this issue · 0 comments

Currently there is no way to see for which version of the witness format spec a witness was created.
This makes maintaining the format and interpreting the witnesses harder

Over time we add minor enhancements or bugfixes to the format. It would be beneficial to introduce a field in the witness that gives some clue about which version of the spec the witness implements. For example currently there is a problem with the control key that is actually not allowed in correctness witnesses, which might lead to the introduction of another key or redifinition of when this key is allowed, cf. #14. Another proposed change would be #22, where the need to make the architecture information more in line with the task definition format is brought up and which might lead to a new field being added. This field would then be OK to be missing in witnesses of older format versions, but should be enforced for witnesses with a newer format version.