Add `BeforeWrite` semantics

[rtjoa]

Adds semantics for BeforeWrite, which allows us to delete writes that are shadowed by future writes. Example:

; As there are no writes in the second argument of outer-write,
; the assumption can go to both children. Otherwise it would only go
; to the second argument.
(Write
  (Snd (Write addr x) addr)
  y)
~~>
(Write
  (BeforeWrite addr
    (Snd (Write addr x) addr))
  (BeforeWrite addr
    y))

; As there are no writes in the second argument of (Snd (Write addr x)) addr,
; the first assumption can go to both children.
(BeforeWrite addr
  (Snd (Write addr x) addr))
~~>
(Snd
  (BeforeWrite addr (Write addr x))
  (BeforeWrite addr addr))

; We detected a shadowed write (as both write to the same address)!
(BeforeWrite addr (Write addr x))
~~>
(Empty)

[oflatt]

Closing for now