Laurel: allow modifies clauses to specify new field values

[julesmt]

Follow-up to #1374 (raised by @keyboardDrummer).

The single-ref frame puts heapOut on both sides and leaves the new value free:

data(heapOut) == update(data(heapIn), ref, select(data(heapOut), ref))

so callers pin values with extra postconditions. A syntax like

modifies o -> o with { x := 3 }

could lower to a heapIn-only RHS:

data(heapOut) == update(data(heapIn), ref, update(select(data(heapIn), ref), xField, 3))

filling the value in directly. Today's frame is sound; this is an ergonomics improvement.