Conditional endorsement series is unsafe

[deeglaze]

The shortcutting semantics is a short form of having multiple regular conditional endorsements that include negative conditions.
This violates the conditions of safe negation in Datalog (no negation allowed in the head of rules) because it makes the logic inconsistent.

You can order your processing such that

• the third alternate in a series condition is the first to match and add some endorsement.
• some more endorsements are added
• now the first alternate is the first to match and adds its endorsement.

What if now you reorder your triples such that the endorsements that satisfy the first alternate are added before the series is processed? You have a different result.

@andrew-draper are there restrictions you can think to add to your use case to restore consistency?

[henkbirkholz]

Any pointers that help to "see the issue" in current documents somewhere is useful here, I think (e.g., Andy's use case).

[nedmsmith]

The use cases I'm aware of don't anticipate more than one series match for a given Attester (TE). I think the inconsistency scenario only emerges if there are multiple series tuples that will match for a given TE. Since the series evaluation is within the context of the condition result, there isn't a generalized problem. The unspecified assumption is that only one series tuple can match.

This puts the burden on consistency on the shoulders of the triple/rim author. Is that OK?

If not, then the normative might change to say that all the series tuples will be evaluated. The trade-off is performance.

[deeglaze]

If there’s never any expectation that more than one case will match, then we should change the rule to be that all series variants are compared with no short-circuiting. That removes negation and should still satisfy the use case, no?

Edit:yes, agree with Ned on the last point. I don’t want to entrust consistency to the corim writer

[nedmsmith]

It turns out that order of the series matters for the use case to get the right answer.
If the series is ordered, say from a..n, and b is the record whose condition matches. If another verifier chose the ordering to be n..a, then records n..b would all match.

The use case author is counting on the triple series preserving order. Normally, in CDDL arrays are ordered. In some cases in the CoRIM spec array are overly constrained in that we specified array (aka SEQUENCE), but unordered arrays (SET) is what was intended.

I think I mischaracterized the consistency proposition when I asked: "should the Endorser be entrusted with consistency of the Verifier". A better characterization might be: "should the Verifier be free to break the CDDL imposed ordering semantics?"