Constraint linearity in the resource machine

How are resources represented? Does this model consider the shielded case as well?

You mention slots but I don’t understand where they come from. They don’t belong to the stacks from what I understand

Is this model defined for a single logic or all logics from the tx?

So instead of checking that a certain resource satisfies the certain logic, we check that there is at least one resource satisfying the logic being processed now? If this model is defined for all logics from the tx being checked, it seems to me that the order in which the resources are loaded affects the results, e.g., if there are two resources R1 and R2 that satisfy logic L1 but only R1 also satisfies logic L2, the logic L1 is checked first and the resource R1 is on top of the stack, the resource R1 would satisfy the constraints from L1, go in the slot, and then the logic L2 will fail because there is only R2 left. And if R2 was on top of R1, it would work well - R2 would satisfy L1 and R1 would satisfy L2. What am I missing here? What happens then? Is it where the search comes in? What is search in this context? How the order in which resources and logics are loaded to the corresponding structures is determined?

Yeah I think it would be a good idea to specify this