Global Memory Argument
To check consistency of memory between different shards, we utilize a multi-set hash function. This hash-function allows one to describe a set incrementally by adding hashes of its respective elements. For the global memory argument we use the classical offline memory-checking protocol of Blum et al. (Manuel Blum, William S. Evans, Peter Gemmell, Sampath Kannan, and Moni Naor. Checking the correctness of memories.) The assumption is that it is computationally infeasible to find two multi-sets that have the same hash value.
This approach reduces checking consistency of memories to checking that two sets a "write-set" and "read-set" are permutations of one another. To do so we hash the elements of the respective sets and check that the resulting hashes are equal. The hashes are furthermore added into a "global" table that is present in each shard, to check consistency with the memory used internally within the shard.
The multiset hash is obtained by using the Poseidon2 hash function to hash into an elliptic curve, and we use addition over the curve to combine hashes of different sets.