Handle Constant Adds Better

[2over12]

Constant addition prior to a load ie. a.load.+x can be viewed as an access to a field. Currently we handle this by pushing adds through loads in the sketch graph, but this doesnt allow this property to be used between uninteresting variables in proofs.

ideally we'd have some sort of proof rule in the FSA:

x \in Z /\ Var a.load.+x /\  Var b /\  a.load.+x <= b
-------------------------------------------------------
a.load <= b.field_at.+x