It is written in the specs: Instance 3 and 4 are the tags of the other resources in the action, Witness 1 and 2 are the resource objects.
S is not intended to be a part of any resource, but maybe we could indeed put it in the value of the ephemeral resource. I didn’t think of that, but I will think about it when specifying how those logics work.
To address the more general question: I’m just zooming in that specific question of signature verification mechanism. Specifying which part of the input is available to the prover, which - to verifier, and what the constraint is. I think it is worthy to explicitly specify these details and not keep them in the head.
It is in some sense redundant (because this constraint is a part of the KL logic), but my personal preference is to extract things that require more thinking into separate posts to give them the deserved attention and not get distracted by the complexity of the whole thing.