We concluded that the pre tags approach to verifying functions is preferable to the conditionals within the abstracts. It makes the benefits (of no state setup) we would have gotten from the symmetric paradigm irrelevant (for now) because we do not look at the tags when the function is being simulated (but only when it is being verified).
NOTE: we still need to figure out if there are logical inconsistencies introduced by this approach
We concluded that the pre tags approach to verifying functions is preferable to the conditionals within the abstracts. It makes the benefits (of no state setup) we would have gotten from the symmetric paradigm irrelevant (for now) because we do not look at the tags when the function is being simulated (but only when it is being verified).
NOTE: we still need to figure out if there are logical inconsistencies introduced by this approach