The tag structure does not make sense to me.
Namely
sig tag : Resource -> Bool -> Commitment | Nullifier
does not work for the case of a nullifier.
sig nullifier : Resource -> Nf-Key -> Nullifier
thus I’d be unsure what to put in this case:
def tag(a-resource, True) = nullifier(a-resource, ???)
Further, I’d argue the function tag is redundant.
Just say there are two ways of creating a tag, or call tag an alias like so:
Type Tag = Nullifier | Commitment