  This is a companion report for the OOPSLA 2023 paper of the same title,
presenting a detailed end-to-end account of the $\lambda^*_{\mathsf{G}}$ graph
IR, at a level of detail beyond a regular conference paper. Our first concern
is adequacy and soundness of $\lambda^*_{\mathsf{G}}$, which we derive from a
direct-style imperative functional language (a variant of Bao et al.'s
$\lambda^*$-calculus with reachability types and a simple effect system) by a
series of type-preserving translations into a calculus in monadic normalform
(MNF). Static reachability types and effects entirely inform
$\lambda^*_{\mathsf{G}}$'s dependency synthesis. We argue for its adequacy by
proving its functional properties along with dependency safety via progress and
preservation lemmas with respect to a notion of call-by-value (CBV) reduction
that checks the observed order of effects.
  Our second concern is establishing the correctness of
$\lambda^*_{\mathsf{G}}$'s equational rules that drive compiler optimizations
(e.g., DCE, $\lambda$-hoisting, etc.), by proving contextual equivalence using
logical relations. A key insight is that the functional properties of
dependency synthesis permit a logical relation on $\lambda^*_{\mathsf{G}}$ in
MNF in terms of previously developed logical relations for the direct-style
$\lambda^*$-calculus.
  Finally, we also include a longer version of the conference paper's section
on code generation and code motion for $\lambda^*_{\mathsf{G}}$ as implemented
in Scala~LMS.
