Assembly checking with aliasing

[andres-erbsen]

0xADE1A1DE/CryptOpt#167

Currently, the assembly checker assumes all inputs and outputs are disjoint. But the functions we are checking are sometimes used with overlapping inputs and outputs, e.g. x = x^2.

• arbitrary aliasing (array u64 xs px /\ array u64 ys py in separation logic), could be supported by resolving reads against either conjunct and keeping only the matching conjunct on writes
• we could support equal-or-disjoint pointers by explicitly checking both cases. Or perhaps some encoding like seps (map (fun i => u64 xs[i] (px+8*i) /\ u64 ys[i] (px+8*i)) (range(len xs)) could do it.