Great question! There are a few different options for establishing this correspondence, and I’m not yet sure which one is best (there may also be others I haven’t thought of). For simplicity, I’ll just talk about the resource machine and the EVM here, but the patterns should generalize.
I also want to note that the questions of assets and VMs are distinct - one could have “1 ETH” just as a normal resource in the resource machine, secured by the Ethereum main chain (as terminal controller), where proofs are just published to the protocol adapter in order to consume that resource.
Option 1: EVM state as a single resource
This is the simplest option, and probably the most natural for integrating resource machine applications with current EVM chains. In this option, an entire EVM state is kept (committed to, but probably stored elsewhere) in a single resource, and every time that resource is consumed/recreated, the EVM state transition function is run to check validity - so many smart contracts live “within” a resource. An invariant like the one you mention (token swap) could be checked by reading e.g. ERC20.balanceOf in the consumed & created resources and comparing them.
Option 2: One resource per smart contract
This is a fancier option which allows for parallelism, but will require some additional plumbing. In this option, the state of each smart contract is kept (committed to, but probably stored elsewhere) in a resource dedicated to that smart contract, and every time the state of that smart contract is changed, the EVM state transition function is run to check validity - but only for the state changes of that contract. An invariant like the one you mention could be checked in a similar way, where multiple resources may be involved. This option is more complex as the updates to the EVM chain must be mapped to updates to multiple resources (instead of a single one).