I think that the key question with relaxing this requirement (as you infer) is how logics would enforce exclusive constraint satisfaction. For example, suppose that I want to create two persistables I_0 and I_1, each with a logic which allows an A_0 and A_1 (other persistables, owned by me) to be consumed if and only if a B (another persistable) is created satisfying certain conditions (intuitively, I want to swap an A for a B, twice). I do not want it to be possible for someone to create a single B and claim both my A_0 and A_1 – these were intended to be independent, exclusive swaps.
If we use a cover, this seems like it would only be possible to enforce if we expose a way for logics to check that a specific other resource is not included elsewhere. Does this make sense / am I understanding your proposal correctly?
I’m coming around to this perspective – at least, parallelization and preprocessing, even if not strictly necessary for verification of state transition correctness, seem like very common patterns which developers will want to employ, and it would be nice to have a model which captures them. I think that this is also necessary for consistent levels of abstraction: at the moment, in order to compute over historical resources, “read” resources, etc. in resource logics, you’d need to process the underlying structure (e.g. commitments, nullifiers), which breaks the abstraction boundary that we want resource logics to have in the basic case of state transition verification.
If we want to go in this direction, the question [to me] is how to best synthesize these design requirements (the ability to check exclusive constraint satisfaction, on the one hand, and the ability to support read-only persistables / parallelization / pre-processing, on the other). The best idea I have at the moment is to put matters in the hands of the logics: allow logics to check (for persistables in their scopes) whether those persistables are also used elsewhere in the transaction. If we do that, however, it’s not clear to me what a “scope” is anymore, since logics can check something outside of their “scope” – then maybe we’d better just give up the concept of multiple persistables being “in” a scope altogether and instead have “one scope per persistable”, where the logic associated with that persistable can check whatever it wants about other persistables in the transaction (including exclusivity). Thoughts?