Repository: exo-lang/exo

Issue:
Deprecate effects if it's not used, or re-work analysis to use it

Discussion:
codecov[bot]: ## [Codecov](https://app.codecov.io/gh/exo-lang/exo/pull/672?dropdown=coverage&src=pr&el=h1&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) Report
Attention: Patch coverage is `82.76864%` with `178 lines` in your changes missing coverage. Please review.
> Project coverage is 85.23%. Comparing base [(`e115107`)](https://app.codecov.io/gh/exo-lang/exo/commit/e11510788aee241d0b55904c37a15f18fc213836?dropdown=coverage&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) to head [(`438b958`)](https://app.codecov.io/gh/exo-lang/exo/commit/438b95854af0134df55760f9ef7cbc8bdb0ece47?dropdown=coverage&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang).

| [Files](https://app.codecov.io/gh/exo-lang/exo/pull/672?dropdown=coverage&src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) | Patch % | Lines |
|---|---|---|
| [src/exo/boundscheck.py](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&filepath=src%2Fexo%2Fboundscheck.py&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang#diff-c3JjL2V4by9ib3VuZHNjaGVjay5weQ==) | 82.60% | [132 Missing :warning: ](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) |
| [src/exo/LoopIR.py](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&filepath=src%2Fexo%2FLoopIR.py&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang#diff-c3JjL2V4by9Mb29wSVIucHk=) | 76.34% | [44 Missing :warning: ](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) |
| [src/exo/LoopIR\_scheduling.py](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&filepath=src%2Fexo%2FLoopIR_scheduling.py&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang#diff-c3JjL2V4by9Mb29wSVJfc2NoZWR1bGluZy5weQ==) | 93.33% | [2 Missing :warning: ](https://app.codecov.io/gh/exo-lang/exo/pull/672?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang) |

<details><summary>Additional details and impacted files</summary>


```diff
@@            Coverage Diff             @@
##             main     #672      +/-   ##
==========================================
- Coverage   86.95%   85.23%   -1.72%     
==========================================
  Files          86       84       -2     
  Lines       20903    20771     -132     
==========================================
- Hits        18176    17705     -471     
- Misses       2727     3066     +339     
```

</details>

[:umbrella: View full report in Codecov by Sentry](https://app.codecov.io/gh/exo-lang/exo/pull/672?dropdown=coverage&src=pr&el=continue&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang).   
:loudspeaker: Have feedback on the report? [Share it here](https://about.codecov.io/codecov-pr-comment-feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=exo-lang).


Patch:
diff --git a/src/exo/API.py b/src/exo/API.py
index 03d7e72..6a010d2 100644
--- a/src/exo/API.py
+++ b/src/exo/API.py
@@ -13,7 +13,7 @@ from . import LoopIR as LoopIR
 from .LoopIR_compiler import run_compile, compile_to_strings
 from .LoopIR_unification import DoReplace, UnificationError
 from .configs import Config
-from .effectcheck import InferEffects, CheckEffects
+from .boundscheck import CheckBounds
 from .memory import Memory
 from .parse_fragment import parse_fragment
 from .pattern_match import match_pattern
@@ -170,8 +170,7 @@ class Procedure(ProcedureBase):
 
         if isinstance(proc, LoopIR.UAST.proc):
             proc = TypeChecker(proc).get_loopir()
-            proc = InferEffects(proc).result()
-            CheckEffects(proc)
+            CheckBounds(proc)
             Check_Aliasing(proc)
 
         assert isinstance(proc, LoopIR.LoopIR.proc)
@@ -226,27 +225,9 @@ class Procedure(ProcedureBase):
     #     introspection operations
     # -------------------------------- #
 
-    def check_effects(self):
-        self._loopir_proc = InferEffects(self._loopir_proc).result()
-        CheckEffects(self._loopir_proc)
-        return self
-
     def name(self):
         return self._loopir_proc.name
 
-    def show_effects(self):
-        self._loopir_proc = InferEffects(self._loopir_proc).result()
-        return str(self._loopir_proc.eff)
-
-    def show_effect(self, stmt_pattern):
-        self._loopir_proc = InferEffects(self._loopir_proc).result()
-        if match := match_pattern(
-            self._root(), stmt_pattern, call_depth=1, default_match_no=0
-        ):
-            assert len(match[0]) == 1, "Must match single statements"
-            return str(match[0][0]._node.eff)
-        raise SchedulingError("failed to find statement", pattern=stmt_pattern)
-
     def is_instr(self):
         return self._loopir_proc.instr is not None
 
@@ -381,7 +362,7 @@ class Procedure(ProcedureBase):
         p = self._loopir_proc
         assertion = parse_fragment(p, assertion, p.body[0], configs=configs)
         p = LoopIR.LoopIR.proc(
-            p.name, p.args, p.preds + [assertion], p.body, p.instr, p.eff, p.srcinfo
+            p.name, p.args, p.preds + [assertion], p.body, p.instr, p.srcinfo
         )
         return Procedure(p, _provenance_eq_Procedure=None)
 
diff --git a/src/exo/API_scheduling.py b/src/exo/API_scheduling.py
index 5f8e550..560315e 100644
--- a/src/exo/API_scheduling.py
+++ b/src/exo/API_scheduling.py
@@ -15,7 +15,6 @@ from .API_types import ExoType
 
 from .LoopIR_unification import DoReplace, UnificationError
 from .configs import Config
-from .effectcheck import CheckEffects
 from .memory import Memory
 from .parse_fragment import parse_fragment
 from .prelude import *
diff --git a/src/exo/LoopIR.py b/src/exo/LoopIR.py
index 7c413c1..f381eff 100644
--- a/src/exo/LoopIR.py
+++ b/src/exo/LoopIR.py
@@ -1,5 +1,5 @@
 import re
-from collections import ChainMap
+from collections import ChainMap, defaultdict
 from typing import Type
 
 from asdl_adt import ADT, validators
@@ -63,7 +63,6 @@ module LoopIR {
              expr*   preds,
              stmt*   body,
              instr?  instr,
-             effect? eff,
              srcinfo srcinfo )
 
     instr  = ( string c_instr,
@@ -84,7 +83,7 @@ module LoopIR {
          | Free( sym name, type type, mem mem )
          | Call( proc f, expr* args )
          | WindowStmt( sym name, expr rhs )
-         attributes( effect? eff, srcinfo srcinfo )
+         attributes( srcinfo srcinfo )
 
     loop_mode = Seq()
                 | Par()
@@ -130,7 +129,6 @@ module LoopIR {
     ext_types={
         "name": validators.instance_of(Identifier, convert=True),
         "sym": Sym,
-        "effect": (lambda x: validators.instance_of(Effects.effect)(x)),
         "mem": Type[Memory],
         "builtin": BuiltIn,
         "config": Config,
@@ -310,55 +308,6 @@ module CIR {
 )
 
 
-# --------------------------------------------------------------------------- #
-# Effects
-# --------------------------------------------------------------------------- #
-
-Effects = ADT(
-    """
-module Effects {
-    effect      = ( effset*     reads,
-                    effset*     writes,
-                    effset*     reduces,
-                    config_eff* config_reads,
-                    config_eff* config_writes,
-                    srcinfo     srcinfo )
-
-    -- JRK: the notation of this comprehension is confusing -
-    ---     maybe just use math:
-    -- this corresponds to `{ buffer : loc for *names in int if pred }`
-    effset      = ( sym         buffer,
-                    expr*       loc,    -- e.g. reading at (i+1,j+1)
-                    sym*        names,
-                    expr?       pred,
-                    srcinfo     srcinfo )
-
-    config_eff  = ( config      config, -- blah
-                    string      field,
-                    expr?       value, -- need not be supplied for reads
-                    expr?       pred,
-                    srcinfo     srcinfo )
-
-    expr        = Var( sym name )
-                | Not( expr arg )
-                | Const( object val )
-                | BinOp( binop op, expr lhs, expr rhs )
-                | Stride( sym name, int dim )
-                | Select( expr cond, expr tcase, expr fcase )
-                | ConfigField( config config, string field )
-                attributes( type type, srcinfo srcinfo )
-
-} """,
-    {
-        "sym": Sym,
-        "type": LoopIR.type,
-        "binop": validators.instance_of(Operator, convert=True),
-        "config": Config,
-        "srcinfo": SrcInfo,
-    },
-)
-
-
 # --------------------------------------------------------------------------- #
 # Extension methods
 # --------------------------------------------------------------------------- #
@@ -588,39 +537,6 @@ del basetype
 from . import LoopIR_pprint
 
 
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-
-
-# convert from LoopIR.expr to E.expr
-def lift_to_eff_expr(e):
-    if isinstance(e, LoopIR.Read):
-        assert len(e.idx) == 0
-        return Effects.Var(e.name, e.type, e.srcinfo)
-
-    elif isinstance(e, LoopIR.Const):
-        return Effects.Const(e.val, e.type, e.srcinfo)
-
-    elif isinstance(e, LoopIR.BinOp):
-        lhs = lift_to_eff_expr(e.lhs)
-        rhs = lift_to_eff_expr(e.rhs)
-        return Effects.BinOp(e.op, lhs, rhs, e.type, e.srcinfo)
-
-    elif isinstance(e, LoopIR.USub):
-        zero = Effects.Const(0, e.type, e.srcinfo)
-        arg = lift_to_eff_expr(e.arg)
-        return Effects.BinOp("-", zero, arg, e.type, e.srcinfo)
-
-    elif isinstance(e, LoopIR.StrideExpr):
-        return Effects.Stride(e.name, e.dim, e.type, e.srcinfo)
-
-    elif isinstance(e, LoopIR.ReadConfig):
-        cfg_val = e.config.lookup(e.field)[1]
-        return Effects.ConfigField(e.config, e.field, cfg_val, e.srcinfo)
-
-    assert False, f"bad case, e is {type(e)}"
-
-
 # --------------------------------------------------------------------------- #
 # --------------------------------------------------------------------------- #
 # Standard Pass Templates for Loop IR
@@ -1050,6 +966,16 @@ class GetReads(LoopIR_Do):
         super().do_e(e)
 
 
+class GetReadConfigs(LoopIR_Do):
+    def __init__(self):
+        self.readconfigs = []
+
+    def do_e(self, e):
+        if isinstance(e, LoopIR.ReadConfig):
+            self.readconfigs.append((e.config, e.field))
+        super().do_e(e)
+
+
 def get_reads_of_expr(e):
     gr = GetReads()
     gr.do_e(e)
@@ -1063,6 +989,13 @@ def get_reads_of_stmts(stmts):
     return gr.reads
 
 
+def get_readconfigs(stmts):
+    gr = GetReadConfigs()
+    for stmt in stmts:
+        gr.do_s(stmt)
+    return gr.readconfigs
+
+
 class GetWrites(LoopIR_Do):
     def __init__(self):
         self.writes = []
@@ -1092,6 +1025,29 @@ def get_writes_of_stmts(stmts):
     return gw.writes
 
 
+class GetWriteConfigs(LoopIR_Do):
+    def __init__(self):
+        self.writeconfigs = []
+
+    def do_s(self, s):
+        if isinstance(s, LoopIR.WriteConfig):
+            self.writeconfigs.append((s.config, s.field))
+        elif isinstance(s, LoopIR.Call):
+            self.writeconfigs += get_writeconfigs(s.f.body)
+
+        super().do_s(s)
+
+    # early exit
+    def do_e(self, e):
+        return
+
+
+def get_writeconfigs(stmts):
+    gw = GetWriteConfigs()
+    gw.do_stmts(stmts)
+    return gw.writeconfigs
+
+
 def is_const_zero(e):
     return isinstance(e, LoopIR.Const) and e.val == 0
 
@@ -1322,3 +1278,215 @@ class SubstArgs(LoopIR_Rewrite):
                 return (t2 or t).update(src_buf=src_buf.name)
 
         return t2
+
+
+# Data-flow dependencies between variable names
+# TODO: Refactor this using new AI based analysis
+
+# So, what is dependency analysis?
+# Or to put it another way, what extensional property(s)
+# does dependency analysis guarantee?
+#
+# Let B be a block of statements,
+#     s be a store, and
+#     x, y, … be names/symbols.
+# Let FV(B) be the set of names that are free in B
+#
+# Then, first observe that the "meaning" of B is
+#
+#   Exec[[B]] : (FV(B) -> Value) -> Store -> Store
+#
+# (note that (FV(B) -> Value) is a valuation/mapping specifying the values
+#       of all free variables)
+# (further note that Store = (Name -> Maybe Value) is a valuation/mapping
+#       of variables that models the heap/store)
+#
+# Then, (not x DependsOn y in B) for some y in FV(B) implies that
+#
+#   (Exec[[B]] (env[ y := v1 ]) s)[x] =
+#   (Exec[[B]] (env[ y := v2 ]) s)[x]
+#
+# for all v1, v2
+#
+# Or in other words, the meaning of B
+# w.r.t. its effect on x
+# is invariant to the value of y
+# when x does not depend on y in B
+
+
+class LoopIR_Dependencies(LoopIR_Do):
+    def __init__(self, buf_sym, stmts):
+        self._buf_sym = buf_sym
+        self._lhs = None
+        self._depends = defaultdict(set)
+        self._alias = dict()
+
+        # If `lhs` is not None, then `lhs` will become dependent
+        # on anything read.
+        self._lhs = None
+
+        # variables that affect whether or not the
+        # currently examined code is even running
+        self._context = set()
+
+        # If `control` is True, then anything read will be added
+        # to `context`.
+        self._control = False
+
+        self.do_stmts(stmts)
+
+    def result(self):
+        depends = self._depends[self._buf_sym]
+        new = list(depends)
+        done = []
+        while True:
+            if len(new) == 0:
+                break
+            sym = new.pop()
+            done.append(sym)
+            d = self._depends[sym]
+            depends.update(d)
+            new.extend(s for s in d if s not in done)
+
+        return depends
+
+    def do_s(self, s):
+        if isinstance(s, (LoopIR.Assign, LoopIR.Reduce)):
+            lhs = self._alias.get(s.name, s.name)
+            self._lhs = lhs
+            self._depends[lhs].add(lhs)
+            self._depends[lhs].update(self._context)
+            for i in s.idx:
+                self.do_e(i)
+            self.do_e(s.rhs)
+            self._lhs = None
+        elif isinstance(s, LoopIR.WriteConfig):
+            lhs = (s.config, s.field)
+            self._lhs = lhs
+            self._depends[lhs].add(lhs)
+            self._depends[lhs].update(self._context)
+            self.do_e(s.rhs)
+            self._lhs = None
+        elif isinstance(s, LoopIR.WindowStmt):
+            rhs_buf = self._alias.get(s.rhs.name, s.rhs.name)
+            self._alias[s.name] = rhs_buf
+            self._lhs = rhs_buf
+            self._depends[rhs_buf].add(rhs_buf)
+            self.do_e(s.rhs)
+            self._lhs = None
+
+        elif isinstance(s, LoopIR.If):
+            old_context = self._context
+            self._context = old_context.copy()
+
+            self._control = True
+            self.do_e(s.cond)
+            self._control = False
+
+            self.do_stmts(s.body)
+            self.do_stmts(s.orelse)
+
+            self._context = old_context
+
+        elif isinstance(s, LoopIR.For):
+            old_context = self._context
+            self._context = old_context.copy()
+
+            self._control = True
+            self._lhs = s.iter
+            self._depends[s.iter].add(s.iter)
+            self.do_e(s.lo)
+            self.do_e(s.hi)
+            self._lhs = None
+            self._control = False
+
+            self.do_stmts(s.body)
+
+            self._context = old_context
+
+        elif isinstance(s, LoopIR.Call):
+
+            def process_reads():
+                # now handle dependencies on buffers that might
+                # be read from in the sub-procedure
+                # and dependencies on other arguments
+                for faa, aa in zip(s.f.args, s.args):
+                    if faa.type.is_numeric():
+                        maybe_read = any(
+                            t[0] == faa.name for t in get_reads_of_stmts(s.f.body)
+                        )
+                    else:
+                        maybe_read = True
+
+                    if maybe_read:
+                        self.do_e(aa)
+
+                # additionally, we need to handle dependencies
+                # on configuration fields
+                for name in get_readconfigs(s.f.body):
+                    if self._lhs:
+                        self._depends[self._lhs].add(name)
+
+            # for every argument that represents a buffer being
+            # written to
+            for fa, a in zip(s.f.args, s.args):
+                maybe_write = fa.type.is_numeric() and any(
+                    t[0] == fa.name for t in get_writes_of_stmts(s.f.body)
+                )
+                if maybe_write:
+                    name = self._alias.get(a.name, a.name)
+                    self._lhs = name
+                    self._depends[name].add(name)
+                    self._depends[name].update(self._context)
+                    process_reads()
+                    self._lhs = None
+
+            # secondly, for every configuration field being written to
+            # by this sub-procedure, we need to determine dependencies
+            for name in get_writeconfigs(s.f.body):
+                self._lhs = name
+                self._depends[name].add(name)
+                self._depends[name].update(self._context)
+                process_reads()
+                self._lhs = None
+
+        elif isinstance(s, (LoopIR.Pass, LoopIR.Alloc)):
+            pass
+        else:
+            assert False, "bad case"
+
+    def do_e(self, e):
+        if isinstance(e, (LoopIR.Read, LoopIR.WindowExpr)):
+
+            def visit_idx(e):
+                if isinstance(e, LoopIR.Read):
+                    for i in e.idx:
+                        self.do_e(i)
+                else:
+                    for w in e.idx:
+                        if isinstance(w, LoopIR.Interval):
+                            self.do_e(w.lo)
+                            self.do_e(w.hi)
+                        else:
+                            self.do_e(w.pt)
+
+            name = self._alias.get(e.name, e.name)
+            if self._lhs:
+                self._depends[self._lhs].add(name)
+            if self._control:
+                self._context.add(name)
+
+            visit_idx(e)
+
+        elif isinstance(e, LoopIR.ReadConfig):
+            name = (e.config, e.field)
+            if self._lhs:
+                self._depends[self._lhs].add(name)
+            if self._control:
+                self._context.add(name)
+
+        else:
+            super().do_e(e)
+
+    def do_t(self, t):
+        pass
diff --git a/src/exo/LoopIR_dataflow.py b/src/exo/LoopIR_dataflow.py
deleted file mode 100644
index e6e4e00..0000000
--- a/src/exo/LoopIR_dataflow.py
+++ /dev/null
@@ -1,272 +0,0 @@
-from collections import defaultdict
-from weakref import WeakKeyDictionary
-
-from .LoopIR import LoopIR, LoopIR_Do
-
-_WC_Leaf = {}  # unique object to use as key....
-
-
-class WeakCache(WeakKeyDictionary):
-    def __init__(self):
-        self._tuple_dict = WeakKeyDictionary()
-        self._dict = WeakKeyDictionary()
-
-    def __contains__(self, key):
-        if isinstance(key, (tuple, list)):
-            lookup = self._tuple_dict
-            for k in key:
-                if k not in lookup:
-                    return False
-                else:
-                    lookup = lookup[k]
-            return _WC_Leaf in lookup
-        else:
-            return key in self._dict
-
-    def __getitem__(self, key):
-        if isinstance(key, (tuple, list)):
-            lookup = self._tuple_dict
-            for k in key:
-                lookup = lookup[k]
-            return lookup[_WC_Leaf]
-        else:
-            return self._dict[key]
-
-    def __setitem__(self, key, value):
-        if isinstance(key, (tuple, list)):
-            lookup = self._tuple_dict
-            for k in key:
-                if k not in lookup:
-                    lookup[k] = WeakKeyDictionary()
-                lookup = lookup[k]
-            lookup[_WC_Leaf] = value
-        else:
-            self._dict[key] = value
-
-
-#
-# So, what is dependency analysis?
-# Or to put it another way, what extensional property(s)
-# does dependency analysis guarantee?
-#
-# Let B be a block of statements,
-#     s be a store, and
-#     x, y, … be names/symbols.
-# Let FV(B) be the set of names that are free in B
-#
-# Then, first observe that the "meaning" of B is
-#
-#   Exec[[B]] : (FV(B) -> Value) -> Store -> Store
-#
-# (note that (FV(B) -> Value) is a valuation/mapping specifying the values
-#       of all free variables)
-# (further note that Store = (Name -> Maybe Value) is a valuation/mapping
-#       of variables that models the heap/store)
-#
-# Then, (not x DependsOn y in B) for some y in FV(B) implies that
-#
-#   (Exec[[B]] (env[ y := v1 ]) s)[x] =
-#   (Exec[[B]] (env[ y := v2 ]) s)[x]
-#
-# for all v1, v2
-#
-# Or in other words, the meaning of B
-# w.r.t. its effect on x
-# is invariant to the value of y
-# when x does not depend on y in B
-#
-
-
-# data-flow dependencies between variable names
-class LoopIR_Dependencies(LoopIR_Do):
-    def __init__(self, buf_sym, stmts):
-        self._buf_sym = buf_sym
-        self._lhs = None
-        self._depends = defaultdict(set)
-        self._alias = dict()
-
-        # If `lhs` is not None, then `lhs` will become dependent
-        # on anything read.
-        self._lhs = None
-
-        # variables that affect whether or not the
-        # currently examined code is even running
-        self._context = set()
-
-        # If `control` is True, then anything read will be added
-        # to `context`.
-        self._control = False
-
-        self.do_stmts(stmts)
-
-    def result(self):
-        depends = self._depends[self._buf_sym]
-        new = list(depends)
-        done = []
-        while True:
-            if len(new) == 0:
-                break
-            sym = new.pop()
-            done.append(sym)
-            d = self._depends[sym]
-            depends.update(d)
-            new.extend(s for s in d if s not in done)
-
-        return depends
-
-    def do_s(self, s):
-        if isinstance(s, (LoopIR.Assign, LoopIR.Reduce)):
-            lhs = self._alias.get(s.name, s.name)
-            self._lhs = lhs
-            self._depends[lhs].add(lhs)
-            self._depends[lhs].update(self._context)
-            for i in s.idx:
-                self.do_e(i)
-            self.do_e(s.rhs)
-            self._lhs = None
-        elif isinstance(s, LoopIR.WriteConfig):
-            lhs = (s.config, s.field)
-            self._lhs = lhs
-            self._depends[lhs].add(lhs)
-            self._depends[lhs].update(self._context)
-            self.do_e(s.rhs)
-            self._lhs = None
-        elif isinstance(s, LoopIR.WindowStmt):
-            rhs_buf = self._alias.get(s.rhs.name, s.rhs.name)
-            self._alias[s.name] = rhs_buf
-            self._lhs = rhs_buf
-            self._depends[rhs_buf].add(rhs_buf)
-            self.do_e(s.rhs)
-            self._lhs = None
-
-        elif isinstance(s, LoopIR.If):
-            old_context = self._context
-            self._context = old_context.copy()
-
-            self._control = True
-            self.do_e(s.cond)
-            self._control = False
-
-            self.do_stmts(s.body)
-            self.do_stmts(s.orelse)
-
-            self._context = old_context
-
-        elif isinstance(s, LoopIR.For):
-            old_context = self._context
-            self._context = old_context.copy()
-
-            self._control = True
-            self._lhs = s.iter
-            self._depends[s.iter].add(s.iter)
-            self.do_e(s.lo)
-            self.do_e(s.hi)
-            self._lhs = None
-            self._control = False
-
-            self.do_stmts(s.body)
-
-            self._context = old_context
-
-        elif isinstance(s, LoopIR.Call):
-
-            def process_reads():
-                # now handle dependencies on buffers that might
-                # be read from in the sub-procedure
-                # and dependencies on other arguments
-                for faa, aa in zip(s.f.args, s.args):
-                    if faa.type.is_numeric():
-                        maybe_read = self.analyze_eff(s.f.eff, faa.name, read=True)
-                    else:
-                        maybe_read = True
-
-                    if maybe_read:
-                        self.do_e(aa)
-
-                # additionally, we need to handle dependencies
-                # on configuration fields
-                for ce in s.f.eff.config_reads:
-                    name = (ce.config, ce.field)
-                    if self._lhs:
-                        self._depends[self._lhs].add(name)
-
-            # for every argument that represents a buffer being
-            # written to
-            for fa, a in zip(s.f.args, s.args):
-                maybe_write = fa.type.is_numeric() and self.analyze_eff(
-                    s.f.eff, fa.name, write=True
-                )
-                if maybe_write:
-                    name = self._alias.get(a.name, a.name)
-                    self._lhs = name
-                    self._depends[name].add(name)
-                    self._depends[name].update(self._context)
-                    process_reads()
-                    self._lhs = None
-
-            # secondly, for every configuration field being written to
-            # by this sub-procedure, we need to determine dependencies
-            for ce in s.f.eff.config_writes:
-                name = (ce.config, ce.field)
-                self._lhs = name
-                self._depends[name].add(name)
-                self._depends[name].update(self._context)
-                process_reads()
-                self._lhs = None
-
-        elif isinstance(s, (LoopIR.Pass, LoopIR.Alloc)):
-            pass
-        else:
-            assert False, "bad case"
-
-    def analyze_eff(self, eff, buf, write=False, read=False):
-        if read:
-            if any(es.buffer == buf for es in eff.reads):
-                return True
-        if write:
-            if any(es.buffer == buf for es in eff.writes):
-                return True
-        if read or write:
-            if any(es.buffer == buf for es in eff.reduces):
-                return True
-
-        return False
-
-    def do_e(self, e):
-        if isinstance(e, (LoopIR.Read, LoopIR.WindowExpr)):
-
-            def visit_idx(e):
-                if isinstance(e, LoopIR.Read):
-                    for i in e.idx:
-                        self.do_e(i)
-                else:
-                    for w in e.idx:
-                        if isinstance(w, LoopIR.Interval):
-                            self.do_e(w.lo)
-                            self.do_e(w.hi)
-                        else:
-                            self.do_e(w.pt)
-
-            name = self._alias.get(e.name, e.name)
-            if self._lhs:
-                self._depends[self._lhs].add(name)
-            if self._control:
-                self._context.add(name)
-
-            visit_idx(e)
-
-        elif isinstance(e, LoopIR.ReadConfig):
-            name = (e.config, e.field)
-            if self._lhs:
-                self._depends[self._lhs].add(name)
-            if self._control:
-                self._context.add(name)
-
-        else:
-            super().do_e(e)
-
-    def do_t(self, t):
-        pass
-
-    def do_eff(self, eff):
-        pass
diff --git a/src/exo/LoopIR_effects.py b/src/exo/LoopIR_effects.py
deleted file mode 100644
index 0a63ada..0000000
--- a/src/exo/LoopIR_effects.py
+++ /dev/null
@@ -1,644 +0,0 @@
-from .LoopIR import LoopIR, T, Effects
-from .prelude import *
-
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Printing Functions
-
-op_prec = {
-    "ternary": 5,
-    #
-    "or": 10,
-    #
-    "and": 20,
-    #
-    "<": 30,
-    ">": 30,
-    "<=": 30,
-    ">=": 30,
-    "==": 30,
-    #
-    "+": 40,
-    "-": 40,
-    #
-    "*": 50,
-    "/": 50,
-    "%": 50,
-    #
-    # unary - 60
-}
-
-
-@extclass(Effects.Var)
-@extclass(Effects.Not)
-@extclass(Effects.Const)
-@extclass(Effects.BinOp)
-@extclass(Effects.Stride)
-@extclass(Effects.Select)
-def __str__(self):
-    return _exprstr(self)
-
-
-del __str__
-
-
-def _exprstr(e, prec=0):
-    if isinstance(e, Effects.Var):
-        return str(e.name)
-    elif isinstance(e, Effects.Not):
-        return f"(not {e.arg})"
-    elif isinstance(e, Effects.Const):
-        return str(e.val)
-    elif isinstance(e, Effects.BinOp):
-        local_prec = op_prec[e.op]
-        lhs = _exprstr(e.lhs, prec=local_prec)
-        rhs = _exprstr(e.rhs, prec=local_prec + 1)
-        if local_prec < prec:
-            return f"({lhs} {e.op} {rhs})"
-        else:
-            return f"{lhs} {e.op} {rhs}"
-    elif isinstance(e, Effects.Stride):
-        return f"stride({e.name},{e.dim})"
-    elif isinstance(e, Effects.Select):
-        local_prec = op_prec["ternary"]
-        cond = _exprstr(e.cond)
-        tcase = _exprstr(e.tcase, prec=local_prec + 1)
-        fcase = _exprstr(e.fcase, prec=local_prec + 1)
-        if local_prec < prec:
-            return f"(({cond})? {tcase} : {fcase})"
-        else:
-            return f"({cond})? {tcase} : {fcase}"
-    elif isinstance(e, Effects.ConfigField):
-        return f"{e.config.name()}.{e.field}"
-    else:
-        assert False, "bad case"
-
-
-@extclass(Effects.effect)
-def __str__(self):
-    return _effect_as_str(self)
-
-
-del __str__
-
-
-def _effect_as_str(e):
-    assert isinstance(e, Effects.effect)
-
-    def name(sym):
-        return str(sym)
-
-    def esstr(es, tab="  "):
-        lines = []
-        buf = name(es.buffer)
-        loc = "(" + ",".join([str(l) for l in es.loc]) + ")"
-        if len(es.names) == 0:
-            names = ""
-        else:
-            names = f"for ({','.join([name(n) for n in es.names])}) in Z"
-
-        if es.pred is None:
-            lines.append(f"{tab}{{ {buf} : {loc} {names} }}")
-        else:
-            lines.append(f"{tab}{{ {buf} : {loc} {names} if")
-            tab += "  "
-            pred = str(es.pred)
-            lines.append(f"{tab}{pred} }}")
-
-        return "\n".join(lines)
-
-    def cestr(ce, tab="  "):
-        val, pred = "", ""
-        if ce.value:
-            val = f" = {ce.value}"
-        if ce.pred:
-            pred = f" if {ce.pred}"
-        return f"{ce.config.name()}.{ce.field}{val}{pred}"
-
-    eff_str = ""
-    if len(e.reads) > 0:
-        eff_str += "Reads:\n"
-        eff_str += "\n".join([esstr(es) for es in e.reads])
-        eff_str += "\n"
-    if len(e.writes) > 0:
-        eff_str += f"Writes:\n  "
-        eff_str += "\n".join([esstr(es) for es in e.writes])
-        eff_str += "\n"
-    if len(e.reduces) > 0:
-        eff_str += f"Reduces:\n  "
-        eff_str += "\n".join([esstr(es) for es in e.reduces])
-        eff_str += "\n"
-    if len(e.config_reads) > 0:
-        eff_str += f"Config Reads:\n"
-        eff_str += "\n".join([cestr(ce) for ce in e.config_reads])
-        eff_str += "\n"
-    if len(e.config_writes) > 0:
-        eff_str += f"Config Writes:\n"
-        eff_str += "\n".join([cestr(ce) for ce in e.config_writes])
-        eff_str += "\n"
-
-    return eff_str
-
-
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Substitution of Effect Variables in an effect
-
-
-@extclass(Effects.expr)
-def negate(self):
-    return negate_expr(self)
-
-
-del negate
-
-
-def negate_expr(e):
-    Tbool = T.bool
-    assert e.type == Tbool, "can only negate predicates"
-    if isinstance(e, Effects.Const):
-        return Effects.Const(not e.val, e.type, e.srcinfo)
-    elif isinstance(e, Effects.Var) or isinstance(e, Effects.ConfigField):
-        return Effects.Not(e, e.type, e.srcinfo)
-    elif isinstance(e, Effects.Not):
-        return e.arg
-    elif isinstance(e, Effects.BinOp):
-
-        def change_op(op, lhs=e.lhs, rhs=e.rhs):
-            return Effects.BinOp(op, lhs, rhs, e.type, e.srcinfo)
-
-        if e.op == "and":
-            return change_op("or", negate_expr(e.lhs), negate_expr(e.rhs))
-        elif e.op == "or":
-            return change_op("and", negate_expr(e.lhs), negate_expr(e.rhs))
-        elif e.op == ">":
-            return change_op("<=")
-        elif e.op == "<":
-            return change_op(">=")
-        elif e.op == ">=":
-            return change_op("<")
-        elif e.op == "<=":
-            return change_op(">")
-        elif e.op == "==":
-            if e.lhs.type is Tbool and e.rhs.type is Tbool:
-                l = Effects.BinOp("and", e.lhs, negate_expr(e.rhs), Tbool, e.srcinfo)
-                r = Effects.BinOp("and", negate_expr(e.lhs), e.rhs, Tbool, e.srcinfo)
-
-                return Effects.BinOp("or", l, r, Tbool, e.srcinfo)
-            elif e.lhs.type.is_indexable() and e.rhs.type.is_indexable():
-                return Effects.BinOp(
-                    "or", change_op("<"), change_op(">"), Tbool, e.srcinfo
-                )
-            else:
-                assert False, "TODO: add != support explicitly..."
-    elif isinstance(e, Effects.Select):
-        return Effects.Select(
-            e.cond, negate_expr(e.tcase), negate_expr(e.fcase), e.type, e.srcinfo
-        )
-    assert False, "bad case"
-
-
-@extclass(Effects.effect)
-@extclass(Effects.effset)
-@extclass(Effects.expr)
-def subst(self, env):
-    return eff_subst(env, self)
-
-
-del subst
-
-
-def eff_subst(env, eff):
-    if isinstance(eff, Effects.effset):
-        assert all(nm not in env for nm in eff.names)
-        buf = env[eff.buffer] if eff.buffer in env else eff.buffer
-        pred = eff_subst(env, eff.pred) if eff.pred else None
-        return Effects.effset(
-            buf, [eff_subst(env, e) for e in eff.loc], eff.names, pred, eff.srcinfo
-        )
-    elif isinstance(eff, Effects.config_eff):
-        value = eff_subst(env, eff.value) if eff.value else None
-        pred = eff_subst(env, eff.pred) if eff.pred else None
-        return Effects.config_eff(eff.config, eff.field, value, pred, eff.srcinfo)
-    elif isinstance(eff, Effects.Var):
-        return env[eff.name] if eff.name in env else eff
-    elif isinstance(eff, Effects.Not):
-        return Effects.Not(eff_subst(env, eff.arg), eff.type, eff.srcinfo)
-    elif isinstance(eff, Effects.Const):
-        return eff
-    elif isinstance(eff, Effects.BinOp):
-        return Effects.BinOp(
-            eff.op,
-            eff_subst(env, eff.lhs),
-            eff_subst(env, eff.rhs),
-            eff.type,
-            eff.srcinfo,
-        )
-    elif isinstance(eff, Effects.Stride):
-        name = env[eff.name] if eff.name in env else eff
-        return Effects.Stride(name, eff.dim, eff.type, eff.srcinfo)
-    elif isinstance(eff, Effects.Select):
-        return Effects.Select(
-            eff_subst(env, eff.cond),
-            eff_subst(env, eff.tcase),
-            eff_subst(env, eff.fcase),
-            eff.type,
-            eff.srcinfo,
-        )
-    elif isinstance(eff, Effects.ConfigField):
-        return eff
-    elif isinstance(eff, Effects.effect):
-        return Effects.effect(
-            [eff_subst(env, es) for es in eff.reads],
-            [eff_subst(env, es) for es in eff.writes],
-            [eff_subst(env, es) for es in eff.reduces],
-            [eff_subst(env, ce) for ce in eff.config_reads],
-            [eff_subst(env, ce) for ce in eff.config_writes],
-            eff.srcinfo,
-        )
-    else:
-        assert False, f"bad case: {type(eff)}"
-
-
-@extclass(Effects.effect)
-@extclass(Effects.effset)
-@extclass(Effects.expr)
-def config_subst(self, env):
-    return _subcfg(env, self)
-
-
-del config_subst
-
-
-def _subcfg(env, eff):
-    if isinstance(eff, Effects.effset):
-        return Effects.effset(
-            eff.buffer,
-            [_subcfg(env, e) for e in eff.loc],
-            eff.names,
-            _subcfg(env, eff.pred) if eff.pred else None,
-            eff.srcinfo,
-        )
-    elif isinstance(eff, Effects.config_eff):
-        value = _subcfg(env, eff.value) if eff.value else None
-        pred = _subcfg(env, eff.pred) if eff.pred else None
-        return Effects.config_eff(eff.config, eff.field, value, pred, eff.srcinfo)
-    elif isinstance(eff, (Effects.Var, Effects.Const)):
-        return eff
-    elif isinstance(eff, Effects.Not):
-        return Effects.Not(_subcfg(env, eff.arg), eff.type, eff.srcinfo)
-    elif isinstance(eff, Effects.BinOp):
-        return Effects.BinOp(
-            eff.op, _subcfg(env, eff.lhs), _subcfg(env, eff.rhs), eff.type, eff.srcinfo
-        )
-    elif isinstance(eff, Effects.Stride):
-        return eff
-    elif isinstance(eff, Effects.Select):
-        return Effects.Select(
-            _subcfg(env, eff.cond),
-            _subcfg(env, eff.tcase),
-            _subcfg(env, eff.fcase),
-            eff.type,
-            eff.srcinfo,
-        )
-    elif isinstance(eff, Effects.ConfigField):
-        if (eff.config, eff.field) in env:
-            return env[(eff.config, eff.field)]
-        else:
-            return eff
-    elif isinstance(eff, Effects.effect):
-        return Effects.effect(
-            [_subcfg(env, es) for es in eff.reads],
-            [_subcfg(env, es) for es in eff.writes],
-            [_subcfg(env, es) for es in eff.reduces],
-            [_subcfg(env, ce) for ce in eff.config_reads],
-            [_subcfg(env, ce) for ce in eff.config_writes],
-            eff.srcinfo,
-        )
-    else:
-        assert False, f"bad case: {type(eff)}"
-
-
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Querying of the effect of a block of already annotated statements
-
-
-def get_effect_of_stmts(body):
-    assert len(body) > 0
-    eff = eff_null(body[0].srcinfo)
-    for s in reversed(body):
-        if isinstance(s, LoopIR.Alloc):
-            eff = eff_remove_buf(s.name, eff)
-        elif s.eff is not None:
-            eff = eff_concat(s.eff, eff)
-    return eff
-
-
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Construction/Composition Functions
-
-
-def eff_null(srcinfo=null_srcinfo()):
-    return Effects.effect([], [], [], [], [], srcinfo)
-
-
-def eff_read(buf, loc, srcinfo=null_srcinfo()):
-    read = Effects.effset(buf, loc, [], None, srcinfo)
-    return Effects.effect([read], [], [], [], [], srcinfo)
-
-
-def eff_write(buf, loc, srcinfo=null_srcinfo()):
-    write = Effects.effset(buf, loc, [], None, srcinfo)
-    return Effects.effect([], [write], [], [], [], srcinfo)
-
-
-def eff_reduce(buf, loc, srcinfo=null_srcinfo()):
-    reduction = Effects.effset(buf, loc, [], None, srcinfo)
-    return Effects.effect([], [], [reduction], [], [], srcinfo)
-
-
-def eff_config_read(config, field, srcinfo=null_srcinfo()):
-    read = Effects.config_eff(config, field, None, None, srcinfo)
-    return Effects.effect([], [], [], [read], [], srcinfo)
-
-
-def eff_config_write(config, field, value, srcinfo=null_srcinfo()):
-    write = Effects.config_eff(config, field, value, None, srcinfo)
-    return Effects.effect([], [], [], [], [write], srcinfo)
-
-
-def _and_preds(a, b):
-    return (
-        a
-        if b is None
-        else b
-        if a is None
-        else Effects.BinOp("and", a, b, T.bool, a.srcinfo)
-    )
-
-
-def _or_preds(a, b):
-    return (
-        None if a is None or b is None else Effects.BinOp("or", a, b, T.bool, a.srcinfo)
-    )
-
-
-def eff_union(e1, e2, srcinfo=None):
-    srcinfo = srcinfo or e1.srcinfo
-
-    return Effects.effect(
-        e1.reads + e2.reads,
-        e1.writes + e2.writes,
-        e1.reduces + e2.reduces,
-        e1.config_reads + e2.config_reads,
-        e1.config_writes + e2.config_writes,
-        srcinfo,
-    )
-
-
-# handle complex logic for Configuration when computing
-#   EffectOf( s1 ; s2 ) in terms of EffectOf( s1 ) and EffectOf( s2 )
-def eff_concat(e1, e2, srcinfo=None):
-    srcinfo = srcinfo or e1.srcinfo
-
-    # Step 1: substitute references in e2 to fields written by e1
-    # value expression of config.field after this effect
-    def write_val(ce):
-        assert ce.value is not None
-        if not ce.pred:
-            return ce.value
-        else:
-            # TODO: Fix! I'm not sure what is the intent here..
-            old_val = Effects.ConfigField(ce.config, ce.field, T.bool, srcinfo)
-            return Effects.Select(ce.pred, ce.value, old_val, T.bool, srcinfo)
-
-    # substitute on the basis of writes in the first effect
-    env = {(ce.config, ce.field): write_val(ce) for ce in e1.config_writes}
-    e2 = e2.config_subst(env)
-
-    # Step 2: merge writes from the two effects to the same field
-    def merge_writes(config_writes_1, config_writes_2):
-        cws1 = {(w.config, w.field): w for w in config_writes_1}
-        cws2 = {(w.config, w.field): w for w in config_writes_2}
-        overlap = set(cws1.keys()).intersection(set(cws2.keys()))
-
-        def merge(w1, w2):
-            # in the case of the second write being unconditional
-            if w2.pred is None:
-                return w2
-            else:
-                typ = w1.config.lookup(w1.field)[1]
-                assert typ == w2.config.lookup(w2.field)[1]
-
-                pred = _or_preds(w1.pred, w2.pred)
-                val = Effects.Select(w2.pred, w2.value, w1.value, typ, w2.srcinfo)
-
-                return Effects.config_eff(w1.config, w1.field, val, pred, w2.srcinfo)
-
-        return (
-            [cws1[w] for w in cws1 if w not in overlap]
-            + [cws2[w] for w in cws2 if w not in overlap]
-            + [merge(cws1[key], cws2[key]) for key in overlap]
-        )
-
-    # Step 3: filter out config reads in e2 if they are just
-    #         reading the config value written in e1
-    def shadow_config_reads(config_writes, config_reads):
-        results = []
-        for read in config_reads:
-            assert read.value is None
-
-            # find the corresponding write
-            write = None
-            for w in config_writes:
-                if w.config == read.config and w.field == read.field:
-                    write = w
-                    break
-
-            # handle the shadowing
-            if write is None:
-                results.append(read)
-            elif write.pred is None:
-                # unconditional write, so remove the read
-                pass
-            else:
-                # conditional write, so guard the read
-                pred = _and_preds(read.pred, write.pred.negate())
-                results.append(
-                    Effects.config_eff(
-                        read.config, read.field, None, pred, read.srcinfo
-                    )
-                )
-
-        return results
-
-    def shadow_reads(writes, reads):
-        def shadow_read_by_write(write, read):
-            def boolop(op, lhs, rhs):
-                return Effects.BinOp(op, lhs, rhs, T.bool, write.srcinfo)
-
-            loc = []
-            for l1, l2 in zip(write.loc, read.loc):
-                loc += [boolop("==", l1, l2).negate()]
-
-            # construct loc predicate
-            if loc == []:
-                loc_e = Effects.Const(False, T.bool, write.srcinfo)
-            else:
-                loc_e = loc[0]
-            for l in loc[1:]:
-                loc_e = boolop("or", loc_e, l)
-
-            # loc_e /\ not write.pred
-            if write.pred is None:
-                pred = loc_e
-            else:
-                pred = boolop("or", loc_e, write.pred.negate())
-
-            pred = _and_preds(read.pred, pred)
-
-            read = Effects.effset(
-                read.buffer, read.loc, read.names + write.names, pred, read.srcinfo
-            )
-
-            return read
-
-        def shadow_read_by_writes(writes, read):
-            for w in writes:
-                # find that the write
-                if w.buffer == read.buffer:
-                    read = shadow_read_by_write(w, read)
-
-            return read
-
-        return [shadow_read_by_writes(writes, r) for r in reads]
-
-    config_reads = e1.config_reads + shadow_config_reads(
-        e1.config_writes, e2.config_reads
-    )
-    config_writes = merge_writes(e1.config_writes, e2.config_writes)
-
-    # TODO: Fix shadow_reads by introducing Exists
-    # reads           = (e1.reads + shadow_reads(e1.writes, e2.reads))
-    reads = e1.reads + e2.reads
-
-    return Effects.effect(
-        reads,
-        e1.writes + e2.writes,
-        e1.reduces + e2.reduces,
-        config_reads,
-        config_writes,
-        srcinfo,
-    )
-
-
-def eff_remove_buf(buf, e):
-    return Effects.effect(
-        [es for es in e.reads if es.buffer != buf],
-        [es for es in e.writes if es.buffer != buf],
-        [es for es in e.reduces if es.buffer != buf],
-        e.config_reads,
-        e.config_writes,
-        e.srcinfo,
-    )
-
-
-# handle conditional
-def eff_filter(pred, e):
-    def filter_es(es):
-        return Effects.effset(
-            es.buffer, es.loc, es.names, _and_preds(pred, es.pred), es.srcinfo
-        )
-
-    def filter_ce(ce):
-        return Effects.config_eff(
-            ce.config, ce.field, ce.value, _and_preds(pred, ce.pred), ce.srcinfo
-        )
-
-    return Effects.effect(
-        [filter_es(es) for es in e.reads],
-        [filter_es(es) for es in e.writes],
-        [filter_es(es) for es in e.reduces],
-        [filter_ce(ce) for ce in e.config_reads],
-        [filter_ce(ce) for ce in e.config_writes],
-        e.srcinfo,
-    )
-
-
-# handle for loop
-def eff_bind(bind_name, e, pred=None, config_pred=None):
-    assert isinstance(bind_name, Sym)
-
-    def bind_es(es):
-        return Effects.effset(
-            es.buffer,
-            es.loc,
-            [bind_name] + es.names,
-            _and_preds(pred, es.pred),
-            es.srcinfo,
-        )
-
-    def filter_ce(ce):
-        return Effects.config_eff(
-            ce.config, ce.field, ce.value, _and_preds(pred, config_pred), ce.srcinfo
-        )
-
-    return Effects.effect(
-        [bind_es(es) for es in e.reads],
-        [bind_es(es) for es in e.writes],
-        [bind_es(es) for es in e.reduces],
-        [filter_ce(ce) for ce in e.config_reads],
-        [filter_ce(ce) for ce in e.config_writes],
-        e.srcinfo,
-    )
-
-
-"""
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Free Variable check
-
-@extclass(Effects.effect)
-@extclass(Effects.effset)
-@extclass(Effects.config_eff)
-@extclass(Effects.expr)
-def has_FV(self, x):
-    return _is_FV(x, self)
-del has_FV
-
-def _is_FV(x, eff):
-    if isinstance(eff, Effects.effset):
-        if x in eff.names:
-            return False
-        return ( any( _is_FV(x, e) for e in eff.loc ) or
-                 (eff.pred is not None and is_FV(x, eff.pred)) )
-    elif isinstance(eff, Effects.config_eff):
-        return ( (eff.value is not None and _is_FV(x, eff.value)) or
-                 (eff.pred  is not None and _is_FV(x, eff.pred)) )
-    elif isinstance(eff, Effects.Var):
-        return x == eff.name
-    elif isinstance(eff, Effects.Const):
-        return False
-    elif isinstance(eff, Effects.Not):
-        return _is_FV(x, eff.arg)
-    elif isinstance(eff, Effects.BinOp):
-        return _is_FV(x, eff.lhs) or _is_FV(x, eff.rhs)
-    elif isinstance(eff, Effects.Stride):
-        return False
-    elif isinstance(eff, Effects.Select):
-        return (_is_FV(x, eff.cond) or
-                _is_FV(x, eff.tcase) or
-                _is_FV(x, eff.fcase))
-    elif isinstance(eff, Effects.ConfigField):
-        return False
-    elif isinstance(eff, Effects.effect):
-        return ( any( _is_FV(x, es) for es in eff.reads ) or
-                 any( _is_FV(x, es) for es in eff.writes ) or
-                 any( _is_FV(x, es) for es in eff.reduces ) or
-                 any( _is_FV(x, ce) for ce in eff.config_reads ) or
-                 any( _is_FV(x, ce) for ce in eff.config_writes ) )
-    else:
-        assert False, f"bad case: {type(eff)}"
-"""
diff --git a/src/exo/LoopIR_scheduling.py b/src/exo/LoopIR_scheduling.py
index 65de507..6f0187b 100644
--- a/src/exo/LoopIR_scheduling.py
+++ b/src/exo/LoopIR_scheduling.py
@@ -9,13 +9,13 @@ from .LoopIR import (
     LoopIR_Do,
     LoopIR_Compare,
     SubstArgs,
+    LoopIR_Dependencies,
     T,
     get_reads_of_expr,
     get_reads_of_stmts,
     get_writes_of_stmts,
     is_const_zero,
 )
-from .LoopIR_dataflow import LoopIR_Dependencies
 from .new_eff import (
     SchedulingError,
     Check_ReorderStmts,
@@ -597,7 +597,7 @@ def DoSplitWrite(sc):
         raise SchedulingError("Expected the rhs of the statement to be an addition.")
 
     s0 = s.update(rhs=s.rhs.lhs)
-    s1 = LoopIR.Reduce(s.name, s.type, s.idx, s.rhs.rhs, None, s.srcinfo)
+    s1 = LoopIR.Reduce(s.name, s.type, s.idx, s.rhs.rhs, s.srcinfo)
     ir, fwd = sc._replace([s0, s1])
     return ir, fwd
 
@@ -623,7 +623,6 @@ def DoFoldIntoReduce(assign):
         assign_s.type,
         assign_s.idx,
         assign_s.rhs.rhs,
-        None,
         assign_s.srcinfo,
     )
     return assign._replace([reduce_stmt])
@@ -716,7 +715,6 @@ def DoDivideWithRecompute(
             hi_i,
             body,
             LoopIR.Seq(),
-            None,
             srcinfo,
         )
 
@@ -804,7 +802,7 @@ def DoDivideLoop(
 
         def guard_wrapper(body):
             cond = boolop("<", idx_sub, N, T.bool)
-            return LoopIR.If(cond, body, [], None, srcinfo)
+            return LoopIR.If(cond, body, [], srcinfo)
 
         ir, fwd_wrap = fwd(loop_cursor).body()._wrap(guard_wrapper, "body")
         fwd = _compose(fwd_wrap, fwd)
@@ -817,7 +815,6 @@ def DoDivideLoop(
             inner_hi,
             body,
             loop.loop_mode,
-            None,
             srcinfo,
         )
 
@@ -856,12 +853,11 @@ def DoDivideLoop(
             Ntail,
             cut_body,
             loop.loop_mode,
-            None,
             srcinfo,
         )
         if tail_strategy == "cut_and_guard":
             cond = boolop(">", Ntail, LoopIR.Const(0, T.int, srcinfo), T.bool)
-            cut_s = LoopIR.If(cond, [cut_s], [], None, srcinfo)
+            cut_s = LoopIR.If(cond, [cut_s], [], srcinfo)
 
         ir, fwd_ins = fwd(loop_cursor).after()._insert([cut_s])
         fwd = _compose(fwd_ins, fwd)
@@ -904,7 +900,7 @@ def DoInline(call):
 
     def map_bind(nm, a):
         if isinstance(a, LoopIR.WindowExpr):
-            stmt = LoopIR.WindowStmt(nm, a, None, a.srcinfo)
+            stmt = LoopIR.WindowStmt(nm, a, a.srcinfo)
             win_binds.append(stmt)
             return LoopIR.Read(nm, [], a.type, a.srcinfo)
         return a
@@ -1149,7 +1145,7 @@ def DoConfigWrite(stmt_cursor, config, field, expr, before=False):
     assert isinstance(expr, (LoopIR.Read, LoopIR.StrideExpr, LoopIR.Const))
     s = stmt_cursor._node
 
-    cw_s = LoopIR.WriteConfig(config, field, expr, None, s.srcinfo)
+    cw_s = LoopIR.WriteConfig(config, field, expr, s.srcinfo)
 
     if before:
         ir, fwd = stmt_cursor.before()._insert([cw_s])
@@ -1174,7 +1170,7 @@ def DoBindConfig(config, field, expr_cursor):
     while not isinstance(c._node, LoopIR.stmt):
         c = c.parent()
 
-    cfg_write_s = LoopIR.WriteConfig(config, field, e, None, e.srcinfo)
+    cfg_write_s = LoopIR.WriteConfig(config, field, e, e.srcinfo)
     ir, fwd = c.before()._insert([cfg_write_s])
 
     mod_cfg = Check_DeleteConfigWrite(ir, [cfg_write_s])
@@ -1252,10 +1248,8 @@ def DoBindExpr(new_name, expr_cursors):
     init_c = get_enclosing_stmt_cursor(expr_cursors[0])
 
     new_name = Sym(new_name)
-    alloc_s = LoopIR.Alloc(new_name, expr.type.basetype(), DRAM, None, expr.srcinfo)
-    assign_s = LoopIR.Assign(
-        new_name, expr.type.basetype(), [], expr, None, expr.srcinfo
-    )
+    alloc_s = LoopIR.Alloc(new_name, expr.type.basetype(), DRAM, expr.srcinfo)
+    assign_s = LoopIR.Assign(new_name, expr.type.basetype(), [], expr, expr.srcinfo)
     ir, fwd = init_c.before()._insert([alloc_s, assign_s])
 
     new_read = LoopIR.Read(new_name, [], expr.type, expr.srcinfo)
@@ -1317,13 +1311,13 @@ def DoLiftScope(inner_c):
         def if_wrapper(body, insert_orelse=False):
             src = outer_s.srcinfo
             # this is needed because _replace expects a non-zero length block
-            orelse = [LoopIR.Pass(None, src)] if insert_orelse else []
-            return LoopIR.If(outer_s.cond, body, orelse, None, src)
+            orelse = [LoopIR.Pass(src)] if insert_orelse else []
+            return LoopIR.If(outer_s.cond, body, orelse, src)
 
         def orelse_wrapper(orelse):
             src = outer_s.srcinfo
-            body = [LoopIR.Pass(None, src)]
-            return LoopIR.If(outer_s.cond, body, orelse, None, src)
+            body = [LoopIR.Pass(src)]
+            return LoopIR.If(outer_s.cond, body, orelse, src)
 
         if isinstance(inner_s, LoopIR.If):
             if inner_s in outer_s.body:
@@ -2054,7 +2048,7 @@ class DoLiftAlloc(Cursor_Rewrite):
                 new_typ = T.Tensor(new_rngs, False, new_typ)
 
             # effect remains null
-            self.lifted_stmt = LoopIR.Alloc(s.name, new_typ, s.mem, None, s.srcinfo)
+            self.lifted_stmt = LoopIR.Alloc(s.name, new_typ, s.mem, s.srcinfo)
             self.access_idxs = idxs
             self.alloc_type = new_typ
 
@@ -2327,7 +2321,7 @@ def DoRemoveLoop(loop, unsafe_disable_check):
         cond = LoopIR.BinOp(">", s.hi, s.lo, T.bool, s.srcinfo)
 
         def wrapper(body):
-            return LoopIR.If(cond, body, [], None, s.srcinfo)
+            return LoopIR.If(cond, body, [], s.srcinfo)
 
         ir, fwd = loop.body()._wrap(wrapper, "body")
 
@@ -2464,7 +2458,6 @@ class DoFissionLoops:
             preds=self.orig_proc.preds,
             body=pre_body + post_body,
             instr=None,
-            eff=self.orig_proc.eff,
             srcinfo=self.orig_proc.srcinfo,
         )
 
@@ -2509,8 +2502,8 @@ class DoFissionLoops:
             if fission_body:
                 self.n_lifts -= 1
                 self.alloc_check(pre, post)
-                pre = LoopIR.If(s.cond, pre, [], None, s.srcinfo)
-                post = LoopIR.If(s.cond, post, s.orelse, None, s.srcinfo)
+                pre = LoopIR.If(s.cond, pre, [], s.srcinfo)
+                post = LoopIR.If(s.cond, post, s.orelse, s.srcinfo)
                 return [pre], [post]
 
             body = pre + post
@@ -2521,17 +2514,15 @@ class DoFissionLoops:
             if fission_orelse:
                 self.n_lifts -= 1
                 self.alloc_check(pre, post)
-                pre = LoopIR.If(s.cond, body, pre, None, s.srcinfo)
-                post = LoopIR.If(
-                    s.cond, [LoopIR.Pass(None, s.srcinfo)], post, None, s.srcinfo
-                )
+                pre = LoopIR.If(s.cond, body, pre, s.srcinfo)
+                post = LoopIR.If(s.cond, [LoopIR.Pass(s.srcinfo)], post, s.srcinfo)
                 return [pre], [post]
 
             orelse = pre + post
 
             # if we neither split the body nor the or-else,
             # then we need to gather together the pre and post.
-            single_stmt = LoopIR.If(s.cond, body, orelse, None, s.srcinfo)
+            single_stmt = LoopIR.If(s.cond, body, orelse, s.srcinfo)
 
         # TODO: may need to fix to support lo for backwards compatability
         elif isinstance(s, LoopIR.For):
@@ -2584,7 +2575,7 @@ class DoAddUnsafeGuard(Cursor_Rewrite):
             #                       self.cond, [s],
             #                       LoopIR.Const(True, T.bool, s.srcinfo))
             s1 = Alpha_Rename([s]).result()
-            return [LoopIR.If(self.cond, s1, [], None, s.srcinfo)]
+            return [LoopIR.If(self.cond, s1, [], s.srcinfo)]
 
         return super().map_s(sc)
 
@@ -2624,7 +2615,7 @@ def DoSpecialize(block_c, conds):
             raise SchedulingError("Invalid specialization condition.")
 
         then_br = Alpha_Rename(block).result()
-        else_br = [LoopIR.If(cond, then_br, else_br, None, block[0].srcinfo)]
+        else_br = [LoopIR.If(cond, then_br, else_br, block[0].srcinfo)]
 
     ir, fwd = block_c._replace(else_br)
     return ir, fwd
@@ -2682,7 +2673,7 @@ def DoFuseIf(f_cursor, s_cursor):
     body2 = if2.body
     orelse1 = if1.orelse
     orelse2 = if2.orelse
-    ifstmt = LoopIR.If(cond, body1 + body2, orelse1 + orelse2, None, if1.srcinfo)
+    ifstmt = LoopIR.If(cond, body1 + body2, orelse1 + orelse2, if1.srcinfo)
 
     ir, fwd = s_cursor.body()._move(f_cursor.body()[-1].after())
     if f_cursor.orelse():
@@ -2711,7 +2702,7 @@ def DoAddLoop(stmt_cursor, var, hi, guard, unsafe_disable_check):
             rdsym = LoopIR.Read(sym, [], T.index, s.srcinfo)
             zero = LoopIR.Const(0, T.int, s.srcinfo)
             cond = LoopIR.BinOp("==", rdsym, zero, T.bool, s.srcinfo)
-            body = [LoopIR.If(cond, body, [], None, s.srcinfo)]
+            body = [LoopIR.If(cond, body, [], s.srcinfo)]
 
         return LoopIR.For(
             sym,
@@ -2719,7 +2710,6 @@ def DoAddLoop(stmt_cursor, var, hi, guard, unsafe_disable_check):
             hi,
             body,
             LoopIR.Seq(),
-            None,
             s.srcinfo,
         )
 
@@ -2734,7 +2724,7 @@ def DoAddLoop(stmt_cursor, var, hi, guard, unsafe_disable_check):
 
 def DoInsertPass(gap):
     srcinfo = gap.parent()._node.srcinfo
-    ir, fwd = gap._insert([LoopIR.Pass(None, srcinfo=srcinfo)])
+    ir, fwd = gap._insert([LoopIR.Pass(srcinfo=srcinfo)])
     return ir, fwd
 
 
@@ -2824,12 +2814,8 @@ def DoExtractSubproc(block, subproc_name, include_asserts):
         if not include_asserts:
             subproc_preds = []
 
-        eff = None
-        # TODO: raise NotImplementedError("need to figure out effect of new closure")
-        subproc_ir = LoopIR.proc(
-            subproc_name, fnargs, subproc_preds, body, None, eff, info
-        )
-        call = LoopIR.Call(subproc_ir, args, None, info)
+        subproc_ir = LoopIR.proc(subproc_name, fnargs, subproc_preds, body, None, info)
+        call = LoopIR.Call(subproc_ir, args, info)
         return subproc_ir, call
 
     subproc_ir, call = make_closure()
@@ -3906,7 +3892,7 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
     basetyp = new_typ.basetype() if isinstance(new_typ, T.Tensor) else new_typ
     srcinfo = block[0].srcinfo
 
-    new_alloc = [LoopIR.Alloc(new_name, new_typ, mem, None, srcinfo)]
+    new_alloc = [LoopIR.Alloc(new_name, new_typ, mem, srcinfo)]
     ir, fwd = block_cursor[0].before()._insert(new_alloc)
 
     def get_inner_stmt(loop_nest_c):
@@ -3947,7 +3933,7 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
 
         # Construct the If statement and wrap the context statement
         def guard_wrapper(body):
-            return LoopIR.If(cond, body, [], None, srcinfo)
+            return LoopIR.If(cond, body, [], srcinfo)
 
         # You want to forward `ctxt_stmt_c` instead of relying on passing
         # the forwarded version. However, in all the current callees, the
@@ -4036,9 +4022,7 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
                     load_ridx.append(w)
             load_rhs = LoopIR.Read(buf_name, load_ridx, basetyp, srcinfo)
 
-        load_nest = [
-            LoopIR.Assign(new_name, basetyp, load_widx, load_rhs, None, srcinfo)
-        ]
+        load_nest = [LoopIR.Assign(new_name, basetyp, load_widx, load_rhs, srcinfo)]
 
         for i, n in reversed(list(zip(load_iter, shape))):
             loop = LoopIR.For(
@@ -4047,7 +4031,6 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
                 n,
                 load_nest,
                 LoopIR.Seq(),
-                None,
                 srcinfo,
             )
             load_nest = [loop]
@@ -4076,9 +4059,7 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
 
         store_rhs = LoopIR.Read(new_name, store_ridx, basetyp, srcinfo)
         store_stmt = LoopIR.Reduce if use_accum_zero else LoopIR.Assign
-        store_nest = [
-            store_stmt(buf_name, basetyp, store_widx, store_rhs, None, srcinfo)
-        ]
+        store_nest = [store_stmt(buf_name, basetyp, store_widx, store_rhs, srcinfo)]
 
         for i, n in reversed(list(zip(store_iter, shape))):
             loop = LoopIR.For(
@@ -4087,7 +4068,6 @@ def DoStageMem(block_cursor, buf_name, w_exprs, new_name, use_accum_zero=False):
                 n,
                 store_nest,
                 LoopIR.Seq(),
-                None,
                 srcinfo,
             )
             store_nest = [loop]
@@ -4206,7 +4186,6 @@ def DoUnrollBuffer(alloc_cursor, dim):
             buf_syms[itr],
             new_type,
             alloc_stmt.mem,
-            None,
             alloc_stmt.srcinfo,
         )
         new_allocs.append(alloc)
diff --git a/src/exo/LoopIR_unification.py b/src/exo/LoopIR_unification.py
index 93078ef..9a6e496 100644
--- a/src/exo/LoopIR_unification.py
+++ b/src/exo/LoopIR_unification.py
@@ -7,8 +7,15 @@ import pysmt
 from asdl_adt import ADT
 from pysmt import shortcuts as SMT
 
-from .LoopIR import LoopIR, T, LoopIR_Do, FreeVars, Alpha_Rename, comparision_ops
-from .LoopIR_dataflow import LoopIR_Dependencies
+from .LoopIR import (
+    LoopIR,
+    T,
+    LoopIR_Do,
+    FreeVars,
+    Alpha_Rename,
+    comparision_ops,
+    LoopIR_Dependencies,
+)
 from .LoopIR_scheduling import SchedulingError
 from .prelude import *
 from .new_eff import Check_Aliasing
@@ -83,7 +90,7 @@ def DoReplace(subproc, block_cursor):
     new_args = Unification(temp_subproc, stmts, live_vars).result()
 
     # but don't use a different LoopIR.proc for the callsite itself
-    new_call = LoopIR.Call(subproc, new_args, None, stmts[0].srcinfo)
+    new_call = LoopIR.Call(subproc, new_args, stmts[0].srcinfo)
 
     ir, fwd = block_cursor._replace([new_call])
     Check_Aliasing(ir)
@@ -460,9 +467,6 @@ class _Find_Mod_Div_Symbols(LoopIR_Do):
         else:
             assert False, "Bad case tupleify"
 
-    def do_eff(self, eff):
-        return
-
 
 class BufVar:
     def __init__(self, name, typ, use_win=True):
diff --git a/src/exo/effectcheck.py b/src/exo/boundscheck.py
similarity index 54%
rename from src/exo/effectcheck.py
rename to src/exo/boundscheck.py
index 63cf352..38f0e64 100644
--- a/src/exo/effectcheck.py
+++ b/src/exo/boundscheck.py
@@ -1,29 +1,478 @@
 from collections import ChainMap
+from asdl_adt import ADT, validators
 
 import pysmt
 from pysmt import shortcuts as SMT
 
-from .LoopIR import LoopIR
-from .LoopIR import T
-from .LoopIR import lift_to_eff_expr as lift_expr
-from .LoopIR_dataflow import LoopIR_Dependencies
-from .LoopIR_effects import Effects as E
-from .LoopIR_effects import (
-    eff_null,
-    eff_read,
-    eff_write,
-    eff_reduce,
-    eff_config_read,
-    eff_config_write,
-    eff_concat,
-    eff_union,
-    eff_remove_buf,
-    eff_filter,
-    eff_bind,
-)
+from .LoopIR import LoopIR, T, Operator, Config
 from .prelude import *
 
 
+# --------------------------------------------------------------------------- #
+# Effects for bounds checking
+# --------------------------------------------------------------------------- #
+
+E = ADT(
+    """
+module Effects {
+    effect      = ( effset*     reads,
+                    effset*     writes,
+                    effset*     reduces,
+                    config_eff* config_reads,
+                    config_eff* config_writes,
+                    srcinfo     srcinfo )
+
+    effset      = ( sym         buffer,
+                    expr*       loc,    -- e.g. reading at (i+1,j+1)
+                    sym*        names,
+                    expr?       pred,
+                    srcinfo     srcinfo )
+
+    config_eff  = ( config      config, -- blah
+                    string      field,
+                    expr?       value, -- need not be supplied for reads
+                    expr?       pred,
+                    srcinfo     srcinfo )
+
+    expr        = Var( sym name )
+                | Not( expr arg )
+                | Const( object val )
+                | BinOp( binop op, expr lhs, expr rhs )
+                | Stride( sym name, int dim )
+                | Select( expr cond, expr tcase, expr fcase )
+                | ConfigField( config config, string field )
+                attributes( type type, srcinfo srcinfo )
+
+} """,
+    {
+        "sym": Sym,
+        "type": LoopIR.type,
+        "binop": validators.instance_of(Operator, convert=True),
+        "config": Config,
+        "srcinfo": SrcInfo,
+    },
+)
+
+
+# --------------------------------------------------------------------------- #
+# --------------------------------------------------------------------------- #
+
+
+# convert from LoopIR.expr to E.expr
+def lift_expr(e):
+    if isinstance(e, LoopIR.Read):
+        assert len(e.idx) == 0
+        return E.Var(e.name, e.type, e.srcinfo)
+
+    elif isinstance(e, LoopIR.Const):
+        return E.Const(e.val, e.type, e.srcinfo)
+
+    elif isinstance(e, LoopIR.BinOp):
+        lhs = lift_expr(e.lhs)
+        rhs = lift_expr(e.rhs)
+        return E.BinOp(e.op, lhs, rhs, e.type, e.srcinfo)
+
+    elif isinstance(e, LoopIR.USub):
+        zero = E.Const(0, e.type, e.srcinfo)
+        arg = lift_expr(e.arg)
+        return E.BinOp("-", zero, arg, e.type, e.srcinfo)
+
+    elif isinstance(e, LoopIR.StrideExpr):
+        return E.Stride(e.name, e.dim, e.type, e.srcinfo)
+
+    elif isinstance(e, LoopIR.ReadConfig):
+        cfg_val = e.config.lookup(e.field)[1]
+        return E.ConfigField(e.config, e.field, cfg_val, e.srcinfo)
+
+    assert False, f"bad case, e is {type(e)}"
+
+
+# --------------------------------------------------------------------------- #
+# --------------------------------------------------------------------------- #
+# Substitution of Effect Variables in an effect
+
+
+@extclass(E.expr)
+def negate(self):
+    return negate_expr(self)
+
+
+del negate
+
+
+def negate_expr(e):
+    Tbool = T.bool
+    assert e.type == Tbool, "can only negate predicates"
+    if isinstance(e, E.Const):
+        return E.Const(not e.val, e.type, e.srcinfo)
+    elif isinstance(e, E.Var) or isinstance(e, E.ConfigField):
+        return E.Not(e, e.type, e.srcinfo)
+    elif isinstance(e, E.Not):
+        return e.arg
+    elif isinstance(e, E.BinOp):
+
+        def change_op(op, lhs=e.lhs, rhs=e.rhs):
+            return E.BinOp(op, lhs, rhs, e.type, e.srcinfo)
+
+        if e.op == "and":
+            return change_op("or", negate_expr(e.lhs), negate_expr(e.rhs))
+        elif e.op == "or":
+            return change_op("and", negate_expr(e.lhs), negate_expr(e.rhs))
+        elif e.op == ">":
+            return change_op("<=")
+        elif e.op == "<":
+            return change_op(">=")
+        elif e.op == ">=":
+            return change_op("<")
+        elif e.op == "<=":
+            return change_op(">")
+        elif e.op == "==":
+            if e.lhs.type is Tbool and e.rhs.type is Tbool:
+                l = E.BinOp("and", e.lhs, negate_expr(e.rhs), Tbool, e.srcinfo)
+                r = E.BinOp("and", negate_expr(e.lhs), e.rhs, Tbool, e.srcinfo)
+
+                return E.BinOp("or", l, r, Tbool, e.srcinfo)
+            elif e.lhs.type.is_indexable() and e.rhs.type.is_indexable():
+                return E.BinOp("or", change_op("<"), change_op(">"), Tbool, e.srcinfo)
+            else:
+                assert False, "TODO: add != support explicitly..."
+    elif isinstance(e, E.Select):
+        return E.Select(
+            e.cond, negate_expr(e.tcase), negate_expr(e.fcase), e.type, e.srcinfo
+        )
+    assert False, "bad case"
+
+
+@extclass(E.effect)
+@extclass(E.effset)
+@extclass(E.expr)
+def subst(self, env):
+    return eff_subst(env, self)
+
+
+del subst
+
+
+def eff_subst(env, eff):
+    if isinstance(eff, E.effset):
+        assert all(nm not in env for nm in eff.names)
+        buf = env[eff.buffer] if eff.buffer in env else eff.buffer
+        pred = eff_subst(env, eff.pred) if eff.pred else None
+        return E.effset(
+            buf, [eff_subst(env, e) for e in eff.loc], eff.names, pred, eff.srcinfo
+        )
+    elif isinstance(eff, E.config_eff):
+        value = eff_subst(env, eff.value) if eff.value else None
+        pred = eff_subst(env, eff.pred) if eff.pred else None
+        return E.config_eff(eff.config, eff.field, value, pred, eff.srcinfo)
+    elif isinstance(eff, E.Var):
+        return env[eff.name] if eff.name in env else eff
+    elif isinstance(eff, E.Not):
+        return E.Not(eff_subst(env, eff.arg), eff.type, eff.srcinfo)
+    elif isinstance(eff, E.Const):
+        return eff
+    elif isinstance(eff, E.BinOp):
+        return E.BinOp(
+            eff.op,
+            eff_subst(env, eff.lhs),
+            eff_subst(env, eff.rhs),
+            eff.type,
+            eff.srcinfo,
+        )
+    elif isinstance(eff, E.Stride):
+        name = env[eff.name] if eff.name in env else eff
+        return E.Stride(name, eff.dim, eff.type, eff.srcinfo)
+    elif isinstance(eff, E.Select):
+        return E.Select(
+            eff_subst(env, eff.cond),
+            eff_subst(env, eff.tcase),
+            eff_subst(env, eff.fcase),
+            eff.type,
+            eff.srcinfo,
+        )
+    elif isinstance(eff, E.ConfigField):
+        return eff
+    elif isinstance(eff, E.effect):
+        return E.effect(
+            [eff_subst(env, es) for es in eff.reads],
+            [eff_subst(env, es) for es in eff.writes],
+            [eff_subst(env, es) for es in eff.reduces],
+            [eff_subst(env, ce) for ce in eff.config_reads],
+            [eff_subst(env, ce) for ce in eff.config_writes],
+            eff.srcinfo,
+        )
+    else:
+        assert False, f"bad case: {type(eff)}"
+
+
+@extclass(E.effect)
+@extclass(E.effset)
+@extclass(E.expr)
+def config_subst(self, env):
+    return _subcfg(env, self)
+
+
+del config_subst
+
+
+def _subcfg(env, eff):
+    if isinstance(eff, E.effset):
+        return E.effset(
+            eff.buffer,
+            [_subcfg(env, e) for e in eff.loc],
+            eff.names,
+            _subcfg(env, eff.pred) if eff.pred else None,
+            eff.srcinfo,
+        )
+    elif isinstance(eff, E.config_eff):
+        value = _subcfg(env, eff.value) if eff.value else None
+        pred = _subcfg(env, eff.pred) if eff.pred else None
+        return E.config_eff(eff.config, eff.field, value, pred, eff.srcinfo)
+    elif isinstance(eff, (E.Var, E.Const)):
+        return eff
+    elif isinstance(eff, E.Not):
+        return E.Not(_subcfg(env, eff.arg), eff.type, eff.srcinfo)
+    elif isinstance(eff, E.BinOp):
+        return E.BinOp(
+            eff.op, _subcfg(env, eff.lhs), _subcfg(env, eff.rhs), eff.type, eff.srcinfo
+        )
+    elif isinstance(eff, E.Stride):
+        return eff
+    elif isinstance(eff, E.Select):
+        return E.Select(
+            _subcfg(env, eff.cond),
+            _subcfg(env, eff.tcase),
+            _subcfg(env, eff.fcase),
+            eff.type,
+            eff.srcinfo,
+        )
+    elif isinstance(eff, E.ConfigField):
+        if (eff.config, eff.field) in env:
+            return env[(eff.config, eff.field)]
+        else:
+            return eff
+    elif isinstance(eff, E.effect):
+        return E.effect(
+            [_subcfg(env, es) for es in eff.reads],
+            [_subcfg(env, es) for es in eff.writes],
+            [_subcfg(env, es) for es in eff.reduces],
+            [_subcfg(env, ce) for ce in eff.config_reads],
+            [_subcfg(env, ce) for ce in eff.config_writes],
+            eff.srcinfo,
+        )
+    else:
+        assert False, f"bad case: {type(eff)}"
+
+
+# --------------------------------------------------------------------------- #
+# --------------------------------------------------------------------------- #
+# Construction/Composition Functions
+
+
+def eff_null(srcinfo=null_srcinfo()):
+    return E.effect([], [], [], [], [], srcinfo)
+
+
+def eff_read(buf, loc, srcinfo=null_srcinfo()):
+    read = E.effset(buf, loc, [], None, srcinfo)
+    return E.effect([read], [], [], [], [], srcinfo)
+
+
+def eff_write(buf, loc, srcinfo=null_srcinfo()):
+    write = E.effset(buf, loc, [], None, srcinfo)
+    return E.effect([], [write], [], [], [], srcinfo)
+
+
+def eff_reduce(buf, loc, srcinfo=null_srcinfo()):
+    reduction = E.effset(buf, loc, [], None, srcinfo)
+    return E.effect([], [], [reduction], [], [], srcinfo)
+
+
+def eff_config_read(config, field, srcinfo=null_srcinfo()):
+    read = E.config_eff(config, field, None, None, srcinfo)
+    return E.effect([], [], [], [read], [], srcinfo)
+
+
+def eff_config_write(config, field, value, srcinfo=null_srcinfo()):
+    write = E.config_eff(config, field, value, None, srcinfo)
+    return E.effect([], [], [], [], [write], srcinfo)
+
+
+def _and_preds(a, b):
+    return (
+        a if b is None else b if a is None else E.BinOp("and", a, b, T.bool, a.srcinfo)
+    )
+
+
+def _or_preds(a, b):
+    return None if a is None or b is None else E.BinOp("or", a, b, T.bool, a.srcinfo)
+
+
+def eff_union(e1, e2, srcinfo=None):
+    srcinfo = srcinfo or e1.srcinfo
+
+    return E.effect(
+        e1.reads + e2.reads,
+        e1.writes + e2.writes,
+        e1.reduces + e2.reduces,
+        e1.config_reads + e2.config_reads,
+        e1.config_writes + e2.config_writes,
+        srcinfo,
+    )
+
+
+# handle complex logic for Configuration when computing
+#   EffectOf( s1 ; s2 ) in terms of EffectOf( s1 ) and EffectOf( s2 )
+def eff_concat(e1, e2, srcinfo=None):
+    srcinfo = srcinfo or e1.srcinfo
+
+    # Step 1: substitute references in e2 to fields written by e1
+    # value expression of config.field after this effect
+    def write_val(ce):
+        assert ce.value is not None
+        if not ce.pred:
+            return ce.value
+        else:
+            # TODO: Fix! I'm not sure what is the intent here..
+            old_val = E.ConfigField(ce.config, ce.field, T.bool, srcinfo)
+            return E.Select(ce.pred, ce.value, old_val, T.bool, srcinfo)
+
+    # substitute on the basis of writes in the first effect
+    env = {(ce.config, ce.field): write_val(ce) for ce in e1.config_writes}
+    e2 = e2.config_subst(env)
+
+    # Step 2: merge writes from the two effects to the same field
+    def merge_writes(config_writes_1, config_writes_2):
+        cws1 = {(w.config, w.field): w for w in config_writes_1}
+        cws2 = {(w.config, w.field): w for w in config_writes_2}
+        overlap = set(cws1.keys()).intersection(set(cws2.keys()))
+
+        def merge(w1, w2):
+            # in the case of the second write being unconditional
+            if w2.pred is None:
+                return w2
+            else:
+                typ = w1.config.lookup(w1.field)[1]
+                assert typ == w2.config.lookup(w2.field)[1]
+
+                pred = _or_preds(w1.pred, w2.pred)
+                val = E.Select(w2.pred, w2.value, w1.value, typ, w2.srcinfo)
+
+                return E.config_eff(w1.config, w1.field, val, pred, w2.srcinfo)
+
+        return (
+            [cws1[w] for w in cws1 if w not in overlap]
+            + [cws2[w] for w in cws2 if w not in overlap]
+            + [merge(cws1[key], cws2[key]) for key in overlap]
+        )
+
+    # Step 3: filter out config reads in e2 if they are just
+    #         reading the config value written in e1
+    def shadow_config_reads(config_writes, config_reads):
+        results = []
+        for read in config_reads:
+            assert read.value is None
+
+            # find the corresponding write
+            write = None
+            for w in config_writes:
+                if w.config == read.config and w.field == read.field:
+                    write = w
+                    break
+
+            # handle the shadowing
+            if write is None:
+                results.append(read)
+            elif write.pred is None:
+                # unconditional write, so remove the read
+                pass
+            else:
+                # conditional write, so guard the read
+                pred = _and_preds(read.pred, write.pred.negate())
+                results.append(
+                    E.config_eff(read.config, read.field, None, pred, read.srcinfo)
+                )
+
+        return results
+
+    config_reads = e1.config_reads + shadow_config_reads(
+        e1.config_writes, e2.config_reads
+    )
+    config_writes = merge_writes(e1.config_writes, e2.config_writes)
+
+    reads = e1.reads + e2.reads
+
+    return E.effect(
+        reads,
+        e1.writes + e2.writes,
+        e1.reduces + e2.reduces,
+        config_reads,
+        config_writes,
+        srcinfo,
+    )
+
+
+def eff_remove_buf(buf, e):
+    return E.effect(
+        [es for es in e.reads if es.buffer != buf],
+        [es for es in e.writes if es.buffer != buf],
+        [es for es in e.reduces if es.buffer != buf],
+        e.config_reads,
+        e.config_writes,
+        e.srcinfo,
+    )
+
+
+# handle conditional
+def eff_filter(pred, e):
+    def filter_es(es):
+        return E.effset(
+            es.buffer, es.loc, es.names, _and_preds(pred, es.pred), es.srcinfo
+        )
+
+    def filter_ce(ce):
+        return E.config_eff(
+            ce.config, ce.field, ce.value, _and_preds(pred, ce.pred), ce.srcinfo
+        )
+
+    return E.effect(
+        [filter_es(es) for es in e.reads],
+        [filter_es(es) for es in e.writes],
+        [filter_es(es) for es in e.reduces],
+        [filter_ce(ce) for ce in e.config_reads],
+        [filter_ce(ce) for ce in e.config_writes],
+        e.srcinfo,
+    )
+
+
+# handle for loop
+def eff_bind(bind_name, e, pred=None, config_pred=None):
+    assert isinstance(bind_name, Sym)
+
+    def bind_es(es):
+        return E.effset(
+            es.buffer,
+            es.loc,
+            [bind_name] + es.names,
+            _and_preds(pred, es.pred),
+            es.srcinfo,
+        )
+
+    def filter_ce(ce):
+        return E.config_eff(
+            ce.config, ce.field, ce.value, _and_preds(pred, config_pred), ce.srcinfo
+        )
+
+    return E.effect(
+        [bind_es(es) for es in e.reads],
+        [bind_es(es) for es in e.writes],
+        [bind_es(es) for es in e.reduces],
+        [filter_ce(ce) for ce in e.config_reads],
+        [filter_ce(ce) for ce in e.config_writes],
+        e.srcinfo,
+    )
+
+
 def _get_smt_solver():
     factory = pysmt.factory.Factory(pysmt.shortcuts.get_env())
     slvs = factory.all_solvers()
@@ -76,429 +525,10 @@ def loopir_subst(e, subst):
 
 # --------------------------------------------------------------------------- #
 # --------------------------------------------------------------------------- #
-# Annotation of an AST with Effects
-
-
-class InferEffects:
-    def __init__(self, proc):
-        self.orig_proc = proc
-
-        self._types = {}
-        for a in proc.args:
-            self._types[a.name] = a.type
-        self.rec_stmts_types(self.orig_proc.body)
-
-        body, eff = self.map_stmts(self.orig_proc.body)
-
-        self.proc = LoopIR.proc(
-            name=self.orig_proc.name,
-            args=self.orig_proc.args,
-            preds=self.orig_proc.preds,
-            body=body,
-            instr=self.orig_proc.instr,
-            eff=eff,
-            srcinfo=self.orig_proc.srcinfo,
-        )
-
-        self.effect = eff
-
-    def get_effect(self):
-        return self.effect
-
-    def result(self):
-        return self.proc
-
-    def rec_stmts_types(self, body):
-        assert len(body) > 0
-        for s in body:
-            self.rec_s_types(s)
-
-    def rec_s_types(self, stmt):
-        if isinstance(stmt, LoopIR.If):
-            self.rec_stmts_types(stmt.body)
-            if len(stmt.orelse) > 0:
-                self.rec_stmts_types(stmt.orelse)
-        elif isinstance(stmt, LoopIR.For):
-            self.rec_stmts_types(stmt.body)
-        elif isinstance(stmt, LoopIR.Alloc):
-            self._types[stmt.name] = stmt.type
-        elif isinstance(stmt, LoopIR.WindowStmt):
-            self._types[stmt.name] = stmt.rhs.type
-        else:
-            pass
-
-    def map_stmts(self, body):
-        assert len(body) > 0
-        eff = eff_null(body[0].srcinfo)
-        stmts = []
-        for s in reversed(body):
-            new_s = self.map_s(s)
-            stmts.append(new_s)
-            if isinstance(new_s, LoopIR.Alloc):
-                eff = eff_remove_buf(new_s.name, eff)
-            else:
-                eff = eff_concat(new_s.eff, eff)
-        return (list(reversed(stmts)), eff)
-
-    def map_s(self, stmt):
-        if isinstance(stmt, (LoopIR.Assign, LoopIR.Reduce)):
-            styp = type(stmt)
-            buf = stmt.name
-            loc = [lift_expr(idx) for idx in stmt.idx]
-            rhs_eff = self.eff_e(stmt.rhs)
-            if styp is LoopIR.Assign:
-                effects = eff_write(buf, loc, stmt.srcinfo)
-            else:  # Reduce
-                effects = eff_reduce(buf, loc, stmt.srcinfo)
-
-            effects = eff_concat(rhs_eff, effects)
-
-            return styp(
-                stmt.name,
-                stmt.type,
-                stmt.idx,
-                stmt.rhs,
-                effects,
-                stmt.srcinfo,
-            )
-
-        elif isinstance(stmt, LoopIR.WriteConfig):
-            rhs_eff = self.eff_e(stmt.rhs)
-            if stmt.rhs.type.is_numeric():
-                rhs = E.Var(Sym("opaque_rhs"), stmt.rhs.type, stmt.rhs.srcinfo)
-            else:
-                rhs = lift_expr(stmt.rhs)
-            cw_eff = eff_config_write(stmt.config, stmt.field, rhs, stmt.srcinfo)
-            eff = eff_concat(rhs_eff, cw_eff)
-            return LoopIR.WriteConfig(
-                stmt.config, stmt.field, stmt.rhs, eff, stmt.srcinfo
-            )
-
-        elif isinstance(stmt, LoopIR.If):
-            cond = lift_expr(stmt.cond)
-            body, body_effects = self.map_stmts(stmt.body)
-            body_effects = eff_filter(cond, body_effects)
-            orelse_effects = eff_null(stmt.srcinfo)
-            orelse = stmt.orelse
-            if len(stmt.orelse) > 0:
-                orelse, orelse_effects = self.map_stmts(stmt.orelse)
-                orelse_effects = eff_filter(cond.negate(), orelse_effects)
-            # union is appropriate because guards on effects are disjoint
-            effects = eff_union(body_effects, orelse_effects)
-
-            return LoopIR.If(stmt.cond, body, orelse, effects, stmt.srcinfo)
-
-        elif isinstance(stmt, LoopIR.For):
-            # pred is: stmt.lo <= bound < stmt.hi
-            bound = E.Var(stmt.iter, T.index, stmt.srcinfo)
-            lo = lift_expr(stmt.lo)
-            hi = lift_expr(stmt.hi)
-            lhs = E.BinOp("<=", lo, bound, T.bool, stmt.srcinfo)
-            rhs = E.BinOp("<", bound, hi, T.bool, stmt.srcinfo)
-            pred = E.BinOp("and", lhs, rhs, T.bool, stmt.srcinfo)
-            config_pred = E.BinOp("<", lo, hi, T.bool, stmt.srcinfo)
-
-            body, body_effect = self.map_stmts(stmt.body)
-            effects = eff_bind(
-                stmt.iter, body_effect, pred=pred, config_pred=config_pred
-            )
-
-            return stmt.update(body=body, eff=effects)
-
-        elif isinstance(stmt, LoopIR.Call):
-            assert stmt.f.eff is not None
-            # build up a substitution dictionary....
-            # sig is a LoopIR.fnarg, arg is a LoopIR.expr
-            subproc = InferEffects(stmt.f).result()
-            subst = {}
-            for sig, arg in zip(subproc.args, stmt.args):
-                if sig.type.is_numeric():
-                    if isinstance(arg.type, T.Window):
-                        pass  # handle below
-                    elif isinstance(arg, LoopIR.Read):
-                        subst[sig.name] = arg.name
-                    elif isinstance(arg, LoopIR.ReadConfig):
-                        pass  # ?
-                    else:
-                        assert False, "bad case"
-                elif sig.type.is_indexable() or sig.type is T.bool:
-                    # in this case we have a LoopIR expression...
-                    subst[sig.name] = lift_expr(arg)
-                elif sig.type.is_stridable():
-                    subst[sig.name] = lift_expr(arg)
-                    # pass
-                else:
-                    assert False, "bad case"
-
-            eff = subproc.eff
-            eff = eff.subst(subst)
-
-            # translate effects occuring on windowed arguments
-            for sig, arg in zip(subproc.args, stmt.args):
-                if sig.type.is_numeric():
-                    if isinstance(arg.type, T.Window):
-                        eff = self.translate_eff(eff, sig.name, arg.type)
-
-            return LoopIR.Call(stmt.f, stmt.args, eff, stmt.srcinfo)
-
-        elif isinstance(stmt, LoopIR.Pass):
-            return LoopIR.Pass(eff_null(stmt.srcinfo), stmt.srcinfo)
-        elif isinstance(stmt, LoopIR.Alloc):
-            return LoopIR.Alloc(
-                stmt.name, stmt.type, stmt.mem, eff_null(stmt.srcinfo), stmt.srcinfo
-            )
-        elif isinstance(stmt, LoopIR.WindowStmt):
-            return LoopIR.WindowStmt(
-                stmt.name, stmt.rhs, eff_null(stmt.srcinfo), stmt.srcinfo
-            )
-
-        else:
-            assert False, "Invalid statement"
-
-    # extract effects from this expression; return E.effect
-    def eff_e(self, e):
-        if isinstance(e, LoopIR.Read):
-            if e.type.is_numeric():
-                # we may assume that we're not in a call-argument position
-                assert e.type.is_real_scalar()
-                loc = [lift_expr(idx) for idx in e.idx]
-                eff = eff_read(e.name, loc, e.srcinfo)
-
-                # x[...], x
-                buf_typ = self._types[e.name]
-                if isinstance(buf_typ, T.Window):
-                    eff = self.translate_eff(eff, e.name, buf_typ)
-
-                return eff
-            else:
-                return eff_null(e.srcinfo)
-        elif isinstance(e, LoopIR.BinOp):
-            return eff_concat(self.eff_e(e.lhs), self.eff_e(e.rhs), srcinfo=e.srcinfo)
-        elif isinstance(e, LoopIR.USub):
-            return self.eff_e(e.arg)
-        elif isinstance(e, LoopIR.Const):
-            return eff_null(e.srcinfo)
-        elif isinstance(e, LoopIR.WindowExpr):
-            return eff_null(e.srcinfo)
-        elif isinstance(e, LoopIR.BuiltIn):
-            return eff_null(e.srcinfo)
-        elif isinstance(e, LoopIR.StrideExpr):
-            return eff_null(e.srcinfo)
-        elif isinstance(e, LoopIR.ReadConfig):
-            return eff_config_read(e.config, e.field, e.srcinfo)
-        else:
-            assert False, "bad case"
-
-    def translate_eff(self, eff, buf_name, win_typ):
-        assert isinstance(eff, E.effect)
-        assert isinstance(win_typ, T.Window)
-
-        def translate_set(es):
-            if es.buffer != buf_name:
-                return es
-            # otherwise, need to translate through the window
-            #   Let `i` = es.loc
-            #       `x` = es.buffer
-            # For a windowing operation `x = y[:,lo:hi,3]`
-            #   Let `j,k` be the indices into `y`.
-            # Then,
-            #   j == i + lo
-            #   k == 3
-            # which means we can get the transformed locations
-            # by simply adding the `lo` offsets from windowing operations
-            loc = es.loc
-            buf = buf_name
-            typ = win_typ
-            while isinstance(typ, T.Window):
-                buf = typ.src_buf
-                idx = typ.idx
-                typ = self._types[buf]
-                loc_i = 0
-                new_loc = []
-                for w_acc in idx:
-                    if isinstance(w_acc, LoopIR.Point):
-                        new_loc.append(lift_expr(w_acc.pt))
-                    elif isinstance(w_acc, LoopIR.Interval):
-                        j = E.BinOp(
-                            "+",
-                            loc[loc_i],
-                            lift_expr(w_acc.lo),
-                            T.index,
-                            w_acc.lo.srcinfo,
-                        )
-                        new_loc.append(j)
-                        loc_i += 1
-                assert loc_i == len(loc)
-                loc = new_loc
-
-            return E.effset(buf, loc, es.names, es.pred, es.srcinfo)
-
-        return E.effect(
-            [translate_set(es) for es in eff.reads],
-            [translate_set(es) for es in eff.writes],
-            [translate_set(es) for es in eff.reduces],
-            eff.config_reads,
-            eff.config_writes,
-            eff.srcinfo,
-        )
-
-
-# --------------------------------------------------------------------------- #
-# --------------------------------------------------------------------------- #
-# Check Bounds and Parallelism semantics for an effect-annotated AST
-
-#
-#   What is bounds checking?
-#
-#       (x : T)  ;  s
-#       s has effect e
-#       Also, we may assume certain things about the context
-#       Let us assume some CTXT_PRED
-#
-#       Then, x is memory safe iff. all accesses to x in s are "in-bounds"
-#       There is a relationship between buffer types (i.e. shapes)
-#       and effect-types, which says that the effect is "in-bounds"
-#       with respect to the buffer type (and you need to know the buffer name)
-#
-#       What we really want to check is that
-#           CTXT_PRED ==> IN_BOUNDS( x, T, e )
-#
-#       IN_BOUNDS( x, T, e ) =
-#           AND es in e: IN_BOUNDS( x, T, es )
-#       IN_BOUNDS( x, T, (y, ...) ) = TRUE
-#       IN_BOUNDS( x, T, (x, (i,j), nms, pred ) ) =
-#           forall nms in Z, pred ==> in_bounds(T, (i,j))
-#
-#
-#   (assert CTXT_PRED_1)
-#   (assert CTXT_PRED_2)
-#   (valid IN_BOUNDS( x, T, e ) )
-#   (valid IN_BOUNDS( y, T2, e2 ) )
-#
-#
-#   for i in par(0,n):
-#       ...
-#       y : R[n]
-#
-#       y[i] = 32
-#
-#       for j in par(0,n):
-#           if i+j < n:
-#               y[i+j] = 32
-#
-#   s has effect WRITE { y : (i+j) for j in int if 0 <= j < n and i+j < n }
-#
-#   CTXT_PRED is 0 <= i < n
-
-
-#
-#   What is parallelism checking?
-#
-#       In general the situation is that we have a parallel for loop
-#
-#       for i in par(0,n): s
-#
-#       s has effect e
-#
-#       We want to check that
-#           forall i0,i1: 0 <= i0 < i1 < n ==> COMMUTES( [i |-> i0]e,
-#                                                        [i |-> i1]e )
-#
-#       R, W, +
-#
-#       R commutes with R
-#       + commutes with +
-#       any two other effects do not commute
-#
-#       COMMUTES( (r0, w0, p0), (r1, w1, p1) ) =
-#           AND ( NOT_CONFLICTS( r0, w1 )
-#                 NOT_CONFLICTS( r0, p1 )
-#                 NOT_CONFLICTS( w0, r1 )
-#                 NOT_CONFLICTS( w0, w1 )
-#                 NOT_CONFLICTS( w0, p1 )
-#                 NOT_CONFLICTS( p0, r1 )
-#                 NOT_CONFLICTS( p0, w1 ) )
-#
-#       NOT_CONFLICTS( (x,...), (y,...) ) = TRUE
-#       NOT_CONFLICTS( (x, loc0, nms0, pred0), (x, loc1, nms1, pred1) ) =
-#           forall nms0, nms1: pred0 AND pred1 ==> loc0 != loc1
-#
-#       Let's try to re-develop these ideas in the setting where
-#       we assume that the two effects are identical except for
-#       our substitution
-#
-#       COMMUTES( i, n, e ) =
-#           forall i0,i1: 0 <= i0 < i1 < n ==>
-#                       COMMUTES( [i |-> i0]e, [i |-> i1]e )
-#
-#       COMMUTES( i, n, (r, w, p) ) =
-#           AND( NOT_CONFLICTS(i, n, r, w)
-#                NOT_CONFLICTS(i, n, r, p)
-#                NOT_CONFLICTS(i, n, w, w)
-#                NOT_CONFLICTS(i, n, w, p) )
-#
-#       NOT_CONFLICTS( i, n, (x,...), (y,...) ) = TRUE
-#       NOT_CONFLICTS( i, n, (x, loc0, nms0, pred0),
-#                            (x, loc1, nms1, pred1) ) =
-#           forall i0,i1: 0 <= i0 < i1 < n ==>
-#               forall nms0, nms1:
-#                   [sub i0,nms0]pred0 AND [sub i1,nms1]pred1 ==>
-#                   [sub i0,nms0]loc0 != [sub i1,nms1]loc1
-#
-#       cond ==> (x AND y)   ===   (cond ==> x) AND (cond ==> y)
-#
-#           AND ( forall _: _ ==> NOT_CONFLICTS( r0, w1 )
-#                 forall _: _ ==> NOT_CONFLICTS( r0, p1 )
-#                 forall _: _ ==> NOT_CONFLICTS( w0, r1 )
-#                 forall _: _ ==> NOT_CONFLICTS( w0, w1 )
-#                 forall _: _ ==> NOT_CONFLICTS( w0, p1 )
-#                 forall _: _ ==> NOT_CONFLICTS( p0, r1 )
-#                 forall _: _ ==> NOT_CONFLICTS( p0, w1 ) )
-#
-#
-
-
-#
-#   What is parallelism checking for Configuration Effects?
-#
-#   Recall that we want to check that
-#           forall i0,i1: 0 <= i0 < i1 < n ==> COMMUTES( [i |-> i0]e,
-#                                                        [i |-> i1]e )
-#
-#   Unlike for numeric buffers we need only be concerned with
-#       reads and writes: R & W
-#   If one loop iteration reads a configuration value set by another
-#       loop iteration, then we could have a problem.
-#   So as long as the reads and writes to configuration fields are
-#       disjoint, we should be fine.
-#
-#   Additionally, we've chosen to not handle quantification
-#       of loop iteration variables, so we need to show a lack of
-#       effect dependence on the loop iteration variables.
-#   As a consequence of this, two different loop iterations must have
-#       the same write effect, and so we may conclude that
-#       writes are guaranteed to commute with each other
-#
-#   First check that
-#       i \not\in FreeVars(cr0) U FreeVars(cw0)
-#
-#   Then, since there is no iteration variable dependence,
-#   we can simplify to
-#       COMMUTES( (cr, cw) ) = NOT_CONFLICTS( cr, cw )
-#
-#
-#       NOT_CONFLICTS( (c1,...), (c2,...) )         = TRUE
-#       NOT_CONFLICTS( (c1,f1,...), (c1,f2,...) )   = TRUE
-#       NOT_CONFLICTS( (c1,f1, _, pred1),
-#                      (c1,f1, _, pred2) ) = NOT pred1 or NOT pred2
-#
-#       (that is, there is no conflict when the predicates are disjoint)
-#
-#
+# Check if Alloc sizes and function arg sizes are actually larger than bounds
 
 
-# Check if Alloc sizes and function arg sizes are actually larger than bounds
-class CheckEffects:
+class CheckBounds:
     def __init__(self, proc):
         self.orig_proc = proc
 
@@ -532,8 +562,9 @@ class CheckEffects:
             # true while checking the rest of this procedure body
             self.solver.add_assertion(smt_p)
 
-        self.preprocess_stmts(self.orig_proc.body)
-        body_eff = self.map_stmts(self.orig_proc.body)
+        self.preprocess_stmts(proc.body)
+
+        body_eff = self.map_stmts(proc.body, self.rec_proc_types(proc))
 
         for arg in proc.args:
             if arg.type.is_numeric():
@@ -543,6 +574,7 @@ class CheckEffects:
                     self.check_pos_size(s)
                 # check the bounds
                 self.check_bounds(arg.name, shape, body_eff)
+
         self.pop()
 
         # do error checking here
@@ -551,6 +583,33 @@ class CheckEffects:
                 "Errors occurred during effect checking:\n" + "\n".join(self.errors)
             )
 
+    def rec_proc_types(self, proc):
+        type_env = {}
+        for a in proc.args:
+            type_env[a.name] = a.type
+        return type_env | self.rec_stmts_types(proc.body)
+
+    def rec_stmts_types(self, body):
+        assert len(body) > 0
+        type_env = {}
+        for s in body:
+            self.rec_s_types(s, type_env)
+        return type_env
+
+    def rec_s_types(self, stmt, type_env):
+        if isinstance(stmt, LoopIR.If):
+            type_env |= self.rec_stmts_types(stmt.body)
+            if len(stmt.orelse) > 0:
+                type_env |= self.rec_stmts_types(stmt.orelse)
+        elif isinstance(stmt, LoopIR.For):
+            type_env |= self.rec_stmts_types(stmt.body)
+        elif isinstance(stmt, LoopIR.Alloc):
+            type_env[stmt.name] = stmt.type
+        elif isinstance(stmt, LoopIR.WindowStmt):
+            type_env[stmt.name] = stmt.rhs.type
+        else:
+            pass
+
     def counter_example(self):
         smt_syms = [smt for sym, smt in self.env.items() if smt.get_type() == SMT.INT]
         val_map = self.solver.get_py_values(smt_syms)
@@ -789,140 +848,13 @@ class CheckEffects:
             for e in es:
                 self.check_in_bounds(sym, shape, e, y)
 
-    #       NOT_CONFLICTS( i, n, (x,...), (y,...) ) = TRUE
-    #       NOT_CONFLICTS( i, n, (x, loc0, nms0, pred0),
-    #                            (x, loc1, nms1, pred1) ) =
-    #           forall i0,i1: 0 <= i0 < i1 < n ==>
-    #               forall nms0, nms1:
-    #                   [sub i0,nms0]pred0 AND [sub i1,nms1]pred1 ==>
-    #                   [sub i0,nms0]loc0 != [sub i1,nms1]loc1
-    def not_conflicts(self, iter, hi, e1, e2):
-        if e1.buffer != e2.buffer:
-            return
-
-        self.push()
-        # determine name substitutions
-        iter1 = iter.copy()
-        iter2 = iter.copy()
-        iter1_smt = self.sym_to_smt(iter1)
-        iter2_smt = self.sym_to_smt(iter2)
-        iter_pred = SMT.And(
-            SMT.And(SMT.LE(SMT.Int(0), iter1_smt), SMT.LT(iter1_smt, iter2_smt)),
-            SMT.LT(iter2_smt, self.expr_to_smt(hi)),
-        )
-        self.solver.add_assertion(iter_pred)
-
-        sub1 = {nm: E.Var(nm.copy(), T.index, null_srcinfo()) for nm in e1.names}
-        sub1[iter] = E.Var(iter1, T.index, null_srcinfo())
-        sub2 = {nm: E.Var(nm.copy(), T.index, null_srcinfo()) for nm in e2.names}
-        sub2[iter] = E.Var(iter2, T.index, null_srcinfo())
-
-        if e1.pred is not None:
-            pred1 = e1.pred.subst(sub1)
-            self.solver.add_assertion(self.expr_to_smt(pred1))
-        if e2.pred is not None:
-            pred2 = e2.pred.subst(sub2)
-            self.solver.add_assertion(self.expr_to_smt(pred2))
-
-        loc1 = [self.expr_to_smt(i.subst(sub1)) for i in e1.loc]
-        loc2 = [self.expr_to_smt(i.subst(sub2)) for i in e2.loc]
-        loc_neq = SMT.Bool(False)
-        for i1, i2 in zip(loc1, loc2):
-            loc_neq = SMT.Or(loc_neq, SMT.NotEquals(i1, i2))
-
-        if not self.solver.is_valid(loc_neq):
-            eg = self.counter_example()
-            self.err(
-                e1,
-                f"data race conflict with statement on "
-                f"{e2.srcinfo} while accessing {e1.buffer} "
-                f"in loop over {iter}, when:\n  {eg}.",
-            )
-
-        self.pop()
-
-    def not_conflicts_config(self, e1, e2):
-        if e1.config == e2.config and e1.field == e2.field:
-            self.push()
-            pred1, pred2 = SMT.Bool(True), SMT.Bool(True)
-            if e1.pred:
-                pred1 = self.expr_to_smt(e1.pred)
-            if e2.pred:
-                pred2 = self.expr_to_smt(e2.pred)
-            disjoint = SMT.Not(SMT.And(pred1, pred2))
-
-            if not self.solver.is_valid(disjoint):
-                eg = self.counter_example()
-                self.err(
-                    e1,
-                    f"conflict on configuration variable "
-                    f"{e1.config.name()}.{e1.field} between "
-                    f"access at {e1.srcinfo} and access at "
-                    f"{e1.srcinfo}, occurs when:\n  {eg}.",
-                )
-
-            self.pop()
-
-    #       COMMUTES( i, n, (r, w, p) ) =
-    def check_commutes(self, iter, hi, eff, body):
-
-        # for numeric buffers
-        #           AND( NOT_CONFLICTS(i, n, r, w)
-        for r in eff.reads:
-            for w in eff.writes:
-                self.not_conflicts(iter, hi, r, w)
-        #                NOT_CONFLICTS(i, n, r, p)
-        for r in eff.reads:
-            for p in eff.reduces:
-                self.not_conflicts(iter, hi, r, p)
-        #                NOT_CONFLICTS(i, n, w, w)
-        for w1 in eff.writes:
-            for w2 in eff.writes:
-                if w1.buffer == w2.buffer:
-                    # If we're writing a loop invariant value to
-                    # the same buffer, that is safe
-                    if iter not in LoopIR_Dependencies(w1.buffer, body).result():
-                        continue
-
-                self.not_conflicts(iter, hi, w1, w2)
-
-        #                NOT_CONFLICTS(i, n, w, p) )
-        for w in eff.writes:
-            for p in eff.reduces:
-                self.not_conflicts(iter, hi, w, p)
-
-        # for configuration variables
-        for r in eff.config_reads:
-            for w in eff.config_writes:
-                self.not_conflicts_config(r, w)
-
-        return
-
-    def check_config_no_loop_depend(self, iter, eff, body):
-        for ce in eff.config_reads:
-            if iter in LoopIR_Dependencies((ce.config, ce.field), body).result():
-                self.err(
-                    ce,
-                    f"The read of config variable "
-                    f"{ce.config.name()}.{ce.field} depends on "
-                    f"the loop iteration variable {iter}",
-                )
-        for ce in eff.config_writes:
-            if iter in LoopIR_Dependencies((ce.config, ce.field), body).result():
-                self.err(
-                    ce,
-                    f"The value written to config variable "
-                    f"{ce.config.name()}.{ce.field} depends on "
-                    f"the loop iteration variable {iter}",
-                )
-
     def check_pos_size(self, expr):
         e_pos = SMT.LT(SMT.Int(0), self.expr_to_smt(expr))
         if not self.solver.is_valid(e_pos):
             eg = self.counter_example()
             self.err(
                 expr,
-                "expected expression to always be positive. "
+                f"expected expression {expr} to always be positive. "
                 f"It can be non positive when:\n  {eg}.",
             )
 
@@ -932,7 +864,7 @@ class CheckEffects:
             eg = self.counter_example()
             self.err(
                 expr,
-                "expected expression to always be non-negative. "
+                f"expected expression {expr} to always be non-negative. "
                 f"It can be negative when:\n  {eg}.",
             )
 
@@ -980,8 +912,9 @@ class CheckEffects:
             else:
                 pass
 
-    def map_stmts(self, body):
-        """Returns an effect for the argument `body`
+    def map_stmts(self, body, type_env):
+        """
+        Returns an effect for the argument `body`
         And also checks bounds/parallelism for any
         allocations/loops within `body`
         """
@@ -989,7 +922,28 @@ class CheckEffects:
         body_eff = eff_null(body[-1].srcinfo)
 
         for stmt in reversed(body):
-            if isinstance(stmt, LoopIR.For):
+            if isinstance(stmt, (LoopIR.Assign, LoopIR.Reduce)):
+                loc = [lift_expr(idx) for idx in stmt.idx]
+                rhs_eff = self.eff_e(stmt.rhs, type_env)
+                if isinstance(stmt, LoopIR.Assign):
+                    effects = eff_write(stmt.name, loc, stmt.srcinfo)
+                else:  # Reduce
+                    effects = eff_reduce(stmt.name, loc, stmt.srcinfo)
+
+                stmt_eff = eff_concat(rhs_eff, effects)
+                body_eff = eff_concat(stmt_eff, body_eff)
+
+            elif isinstance(stmt, LoopIR.WriteConfig):
+                rhs_eff = self.eff_e(stmt.rhs, type_env)
+                if stmt.rhs.type.is_numeric():
+                    rhs = E.Var(Sym("opaque_rhs"), stmt.rhs.type, stmt.rhs.srcinfo)
+                else:
+                    rhs = lift_expr(stmt.rhs)
+                cw_eff = eff_config_write(stmt.config, stmt.field, rhs, stmt.srcinfo)
+                stmt_eff = eff_concat(rhs_eff, cw_eff)
+                body_eff = eff_concat(stmt_eff, body_eff)
+
+            elif isinstance(stmt, LoopIR.For):
                 self.push()
 
                 def bd_pred(x, lo, hi, srcinfo):
@@ -1002,38 +956,49 @@ class CheckEffects:
                         E.BinOp("<", x, hi, T.bool, srcinfo),
                         T.bool,
                         srcinfo,
-                    )
+                    ), E.BinOp("<", lo, hi, T.bool, srcinfo)
 
                 # Check if for-loop bound is non-negative
                 # with the context, before adding assertion
                 iters = LoopIR.BinOp("-", stmt.hi, stmt.lo, T.index, stmt.srcinfo)
                 self.check_non_negative(lift_expr(iters))
 
-                self.solver.add_assertion(
-                    self.expr_to_smt(bd_pred(stmt.iter, stmt.lo, stmt.hi, stmt.srcinfo))
-                )
+                pred, config_pred = bd_pred(stmt.iter, stmt.lo, stmt.hi, stmt.srcinfo)
+                self.solver.add_assertion(self.expr_to_smt(pred))
+
+                child_eff = self.map_stmts(stmt.body, type_env)
 
-                self.map_stmts(stmt.body)
                 self.pop()
 
-                body_eff = eff_concat(stmt.eff, body_eff)
+                stmt_eff = eff_bind(
+                    stmt.iter, child_eff, pred=pred, config_pred=config_pred
+                )
+
+                body_eff = eff_concat(stmt_eff, body_eff)
 
             elif isinstance(stmt, LoopIR.If):
                 # first, do the if-branch
                 self.push()
-                self.solver.add_assertion(self.expr_to_smt(lift_expr(stmt.cond)))
-                self.map_stmts(stmt.body)
+                cond = lift_expr(stmt.cond)
+                self.solver.add_assertion(self.expr_to_smt(cond))
+                body_effects = self.map_stmts(stmt.body, type_env)
                 self.pop()
 
+                body_effects = eff_filter(cond, body_effects)
+                orelse_effects = eff_null(stmt.srcinfo)
+                orelse = stmt.orelse
+
                 # then the else-branch
                 if len(stmt.orelse) > 0:
                     self.push()
-                    neg_cond = lift_expr(stmt.cond).negate()
+                    neg_cond = cond.negate()
                     self.solver.add_assertion(self.expr_to_smt(neg_cond))
-                    self.map_stmts(stmt.orelse)
+                    orelse_effects = self.map_stmts(stmt.orelse, type_env)
+                    orelse_effects = eff_filter(cond.negate(), orelse_effects)
                     self.pop()
 
-                body_eff = eff_concat(stmt.eff, body_eff)
+                stmt_eff = eff_union(body_effects, orelse_effects)
+                body_eff = eff_concat(stmt_eff, body_eff)
 
             elif isinstance(stmt, LoopIR.Alloc):
                 shape = [lift_expr(s) for s in stmt.type.shape()]
@@ -1045,9 +1010,33 @@ class CheckEffects:
                 body_eff = eff_remove_buf(stmt.name, body_eff)
 
             elif isinstance(stmt, LoopIR.Call):
+
+                self.push()
+
+                bind = dict()
                 subst = dict()
+
                 for sig, arg in zip(stmt.f.args, stmt.args):
+                    # Add type assertion from the size signature
+                    if isinstance(sig.type, T.Size):
+                        pos_sz = SMT.LT(SMT.Int(0), self.sym_to_smt(sig.name))
+                        self.solver.add_assertion(pos_sz)
+
+                        # check the caller argument always be positive for sizes
+                        e_arg = lift_expr(arg)
+                        self.check_pos_size(e_arg)
+
+                    # Add type assertion from the caller types
+                    if arg.type.is_tensor_or_window() and not arg.type.is_win():
+                        self.assume_tensor_strides(sig, sig.name, arg.type.shape())
+
+                    # bind potential window-expression
+                    subst[sig.name] = arg
+
                     if sig.type.is_numeric():
+                        if isinstance(arg, LoopIR.Read):
+                            bind[sig.name] = arg.name
+
                         # need to check that the argument shape
                         # has all positive dimensions
                         arg_shape = [lift_expr(s) for s in arg.type.shape()]
@@ -1060,25 +1049,22 @@ class CheckEffects:
                         ]
                         self.check_call_shape_eqv(arg_shape, sig_shape, arg)
 
-                        # bind potential window-expression
-                        subst[sig.name] = arg
+                    else:
+                        bind[sig.name] = lift_expr(arg)
 
-                    elif (
-                        sig.type.is_indexable()
-                        or sig.type == T.bool
-                        or sig.type.is_stridable()
-                    ):
-                        # in this case we have a LoopIR expression...
-                        subst[sig.name] = arg
-                        if sig.type == T.size:
-                            e_arg = lift_expr(arg)
-                            self.check_pos_size(e_arg)
+                # map body of the subprocedure
+                self.preprocess_stmts(stmt.f.body)
+                eff = self.map_stmts(stmt.f.body, self.rec_proc_types(stmt.f))
+                eff = eff.subst(bind)
 
-                    else:
-                        assert False, "bad case"
+                # translate effects occuring on windowed arguments
+                for sig, arg in zip(stmt.f.args, stmt.args):
+                    if sig.type.is_numeric():
+                        if isinstance(arg.type, T.Window):
+                            eff = self.translate_eff(eff, sig.name, arg.type, type_env)
 
+                # Check that asserts are correct
                 for p in stmt.f.preds:
-                    # Check that asserts are correct
                     p_subst = loopir_subst(p, subst)
                     smt_pred = self.expr_to_smt(lift_expr(p_subst))
                     if not self.solver.is_valid(smt_pred):
@@ -1090,9 +1076,105 @@ class CheckEffects:
                             f" Assertion is false when:\n  {eg}",
                         )
 
-                body_eff = eff_concat(stmt.eff, body_eff)
+                self.pop()
+
+                body_eff = eff_concat(eff, body_eff)
+
+            elif isinstance(stmt, (LoopIR.Pass, LoopIR.WindowStmt)):
+                pass
 
             else:
-                body_eff = eff_concat(stmt.eff, body_eff)
+                assert False, "bad case!!"
 
         return body_eff  # Returns union of all effects
+
+    # extract effects from this expression; return E.effect
+    def eff_e(self, e, type_env):
+        if isinstance(e, LoopIR.Read):
+            if e.type.is_numeric():
+                # we may assume that we're not in a call-argument position
+                assert e.type.is_real_scalar()
+                loc = [lift_expr(idx) for idx in e.idx]
+                eff = eff_read(e.name, loc, e.srcinfo)
+
+                # x[...], x
+                buf_typ = type_env[e.name]
+                if isinstance(buf_typ, T.Window):
+                    eff = self.translate_eff(eff, e.name, buf_typ, type_env)
+
+                return eff
+            else:
+                return eff_null(e.srcinfo)
+        elif isinstance(e, LoopIR.BinOp):
+            return eff_concat(
+                self.eff_e(e.lhs, type_env),
+                self.eff_e(e.rhs, type_env),
+                srcinfo=e.srcinfo,
+            )
+        elif isinstance(e, LoopIR.USub):
+            return self.eff_e(e.arg, type_env)
+        elif isinstance(e, LoopIR.Const):
+            return eff_null(e.srcinfo)
+        elif isinstance(e, LoopIR.WindowExpr):
+            return eff_null(e.srcinfo)
+        elif isinstance(e, LoopIR.BuiltIn):
+            return eff_null(e.srcinfo)
+        elif isinstance(e, LoopIR.StrideExpr):
+            return eff_null(e.srcinfo)
+        elif isinstance(e, LoopIR.ReadConfig):
+            return eff_config_read(e.config, e.field, e.srcinfo)
+        else:
+            assert False, "bad case"
+
+    def translate_eff(self, eff, buf_name, win_typ, type_env):
+        assert isinstance(eff, E.effect)
+        assert isinstance(win_typ, T.Window)
+
+        def translate_set(es):
+            if es.buffer != buf_name:
+                return es
+            # otherwise, need to translate through the window
+            #   Let `i` = es.loc
+            #       `x` = es.buffer
+            # For a windowing operation `x = y[:,lo:hi,3]`
+            #   Let `j,k` be the indices into `y`.
+            # Then,
+            #   j == i + lo
+            #   k == 3
+            # which means we can get the transformed locations
+            # by simply adding the `lo` offsets from windowing operations
+            loc = es.loc
+            buf = buf_name
+            typ = win_typ
+            while isinstance(typ, T.Window):
+                buf = typ.src_buf
+                idx = typ.idx
+                typ = type_env[buf]
+                loc_i = 0
+                new_loc = []
+                for w_acc in idx:
+                    if isinstance(w_acc, LoopIR.Point):
+                        new_loc.append(lift_expr(w_acc.pt))
+                    elif isinstance(w_acc, LoopIR.Interval):
+                        j = E.BinOp(
+                            "+",
+                            loc[loc_i],
+                            lift_expr(w_acc.lo),
+                            T.index,
+                            w_acc.lo.srcinfo,
+                        )
+                        new_loc.append(j)
+                        loc_i += 1
+                assert loc_i == len(loc)
+                loc = new_loc
+
+            return E.effset(buf, loc, es.names, es.pred, es.srcinfo)
+
+        return E.effect(
+            [translate_set(es) for es in eff.reads],
+            [translate_set(es) for es in eff.writes],
+            [translate_set(es) for es in eff.reduces],
+            eff.config_reads,
+            eff.config_writes,
+            eff.srcinfo,
+        )
diff --git a/src/exo/internal_cursors.py b/src/exo/internal_cursors.py
index 6e3bed5..21ed814 100644
--- a/src/exo/internal_cursors.py
+++ b/src/exo/internal_cursors.py
@@ -339,7 +339,7 @@ class Block(Cursor):
         # TODO: refactor this; LoopIR should not be imported here
         from exo.LoopIR import LoopIR
 
-        pass_stmt = [LoopIR.Pass(None, self.parent()._node.srcinfo)]
+        pass_stmt = [LoopIR.Pass(self.parent()._node.srcinfo)]
         return self._replace([], empty_default=pass_stmt)
 
     def resolve_all(self):
diff --git a/src/exo/mem_analysis.py b/src/exo/mem_analysis.py
index 33e5f4b..0743503 100644
--- a/src/exo/mem_analysis.py
+++ b/src/exo/mem_analysis.py
@@ -37,7 +37,6 @@ class MemoryAnalysis:
             proc.preds,
             body,
             proc.instr,
-            proc.eff,
             proc.srcinfo,
         )
 
@@ -110,7 +109,7 @@ class MemoryAnalysis:
                 if nm in used:
                     rm += [(nm, typ, mem)]
             for (nm, typ, mem) in rm:
-                body += [LoopIR.Free(nm, typ, mem, None, b.srcinfo)]
+                body += [LoopIR.Free(nm, typ, mem, b.srcinfo)]
                 self.tofree[-1].remove((nm, typ, mem))
             body += [b]
 
@@ -161,7 +160,7 @@ class MemoryAnalysis:
             self.push()
             ebody = self.mem_stmts(s.orelse)
             self.pop()
-            return LoopIR.If(s.cond, body, ebody, None, s.srcinfo)
+            return LoopIR.If(s.cond, body, ebody, s.srcinfo)
         elif styp is LoopIR.For:
             self.push()
             body = self.mem_stmts(s.body)
diff --git a/src/exo/new_eff.py b/src/exo/new_eff.py
index f2a0de4..aaf113a 100644
--- a/src/exo/new_eff.py
+++ b/src/exo/new_eff.py
@@ -452,9 +452,6 @@ def possible_config_writes(stmts):
         def do_t(self, t):
             pass
 
-        def do_eff(self, eff):
-            pass
-
     return Find_RHS(stmts).result()
 
 
@@ -1416,7 +1413,6 @@ class ContextExtraction:
                     LoopIR.Read(bds_sym, [], T.bool, s.srcinfo),
                     s.body,
                     [],
-                    None,
                     s.srcinfo,
                 )
                 G_body = globenv([guard_body])
@@ -1434,9 +1430,7 @@ class ContextExtraction:
         old_i = LoopIR.Read(s.iter, [], T.index, s.srcinfo)
         new_i = LoopIR.Read(s.iter.copy(), [], T.index, s.srcinfo)
         pre_body = SubstArgs(s.body, {s.iter: new_i}).result()
-        pre_loop = LoopIR.For(
-            new_i.name, s.lo, old_i, pre_body, s.loop_mode, None, s.srcinfo
-        )
+        pre_loop = LoopIR.For(new_i.name, s.lo, old_i, pre_body, s.loop_mode, s.srcinfo)
         return globenv([pre_loop])
 
     def loop_posteff(self, s, hi):
@@ -1452,7 +1446,7 @@ class ContextExtraction:
         )
         post_body = SubstArgs(s.body, {s.iter: new_i}).result()
         post_loop = LoopIR.For(
-            new_i.name, old_plus1, hi, post_body, s.loop_mode, None, s.srcinfo
+            new_i.name, old_plus1, hi, post_body, s.loop_mode, s.srcinfo
         )
         return stmts_effs([post_loop])
 
@@ -1612,7 +1606,7 @@ def loop_globenv(i, lo_expr, hi_expr, body):
     assert isinstance(lo_expr, LoopIR.expr)
     assert isinstance(hi_expr, LoopIR.expr)
 
-    loop = [LoopIR.For(i, lo_expr, hi_expr, body, LoopIR.Seq(), None, null_srcinfo())]
+    loop = [LoopIR.For(i, lo_expr, hi_expr, body, LoopIR.Seq(), null_srcinfo())]
     return globenv(loop)
 
 
diff --git a/src/exo/prec_analysis.py b/src/exo/prec_analysis.py
index 671ed97..98a9cd9 100644
--- a/src/exo/prec_analysis.py
+++ b/src/exo/prec_analysis.py
@@ -231,6 +231,3 @@ class PrecisionAnalysis(LoopIR_Rewrite):
     # most of the sub-trees
     def map_t(self, t):
         return None
-
-    def map_eff(self, eff):
-        return None
diff --git a/src/exo/typecheck.py b/src/exo/typecheck.py
index 3c93eb8..0627169 100644
--- a/src/exo/typecheck.py
+++ b/src/exo/typecheck.py
@@ -64,7 +64,6 @@ class TypeChecker:
             preds=preds,
             body=body,
             instr=instr,
-            eff=None,
             srcinfo=proc.srcinfo,
         )
 
@@ -150,7 +149,7 @@ class TypeChecker:
             elif isinstance(rhs.type, T.Window):
                 assert isinstance(rhs, LoopIR.WindowExpr)
                 self.env[stmt.name] = rhs.type
-                return [LoopIR.WindowStmt(stmt.name, rhs, None, stmt.srcinfo)]
+                return [LoopIR.WindowStmt(stmt.name, rhs, stmt.srcinfo)]
             else:
                 self.err(
                     stmt,
@@ -169,7 +168,7 @@ class TypeChecker:
             assert typ.is_real_scalar() or typ is T.err
 
             IRnode = LoopIR.Assign if isinstance(stmt, UAST.Assign) else LoopIR.Reduce
-            return [IRnode(stmt.name, typ, idx, rhs, None, stmt.srcinfo)]
+            return [IRnode(stmt.name, typ, idx, rhs, stmt.srcinfo)]
 
         elif isinstance(stmt, UAST.WriteConfig):
             # Check that field is in config
@@ -217,11 +216,9 @@ class TypeChecker:
                 else:
                     assert False, "bad case"
 
-            return [
-                LoopIR.WriteConfig(stmt.config, stmt.field, rhs, None, stmt.srcinfo)
-            ]
+            return [LoopIR.WriteConfig(stmt.config, stmt.field, rhs, stmt.srcinfo)]
         elif isinstance(stmt, UAST.Pass):
-            return [LoopIR.Pass(None, stmt.srcinfo)]
+            return [LoopIR.Pass(stmt.srcinfo)]
 
         elif isinstance(stmt, UAST.If):
             cond = self.check_e(stmt.cond, is_index=True)
@@ -231,7 +228,7 @@ class TypeChecker:
             ebody = []
             if len(stmt.orelse) > 0:
                 ebody = self.check_stmts(stmt.orelse)
-            return [LoopIR.If(cond, body, ebody, None, stmt.srcinfo)]
+            return [LoopIR.If(cond, body, ebody, stmt.srcinfo)]
 
         elif isinstance(stmt, UAST.For):
             self.env[stmt.iter] = T.index
@@ -255,17 +252,9 @@ class TypeChecker:
 
             body = self.check_stmts(stmt.body)
             if isinstance(stmt.cond, UAST.SeqRange):
-                return [
-                    LoopIR.For(
-                        stmt.iter, lo, hi, body, LoopIR.Seq(), None, stmt.srcinfo
-                    )
-                ]
+                return [LoopIR.For(stmt.iter, lo, hi, body, LoopIR.Seq(), stmt.srcinfo)]
             elif isinstance(stmt.cond, UAST.ParRange):
-                return [
-                    LoopIR.For(
-                        stmt.iter, lo, hi, body, LoopIR.Par(), None, stmt.srcinfo
-                    )
-                ]
+                return [LoopIR.For(stmt.iter, lo, hi, body, LoopIR.Par(), stmt.srcinfo)]
             else:
                 assert False, "bad case"
 
@@ -275,7 +264,7 @@ class TypeChecker:
             mem = stmt.mem
             if mem is None:
                 mem = DRAM
-            return [LoopIR.Alloc(stmt.name, typ, mem, None, stmt.srcinfo)]
+            return [LoopIR.Alloc(stmt.name, typ, mem, stmt.srcinfo)]
 
         elif isinstance(stmt, UAST.Call):
             args = [
@@ -336,7 +325,7 @@ class TypeChecker:
                 else:
                     assert False, "bad argument type case"
 
-            return [LoopIR.Call(stmt.f, args, None, stmt.srcinfo)]
+            return [LoopIR.Call(stmt.f, args, stmt.srcinfo)]
         else:
             assert False, "not a loopir in check_stmts"
 
diff --git a/src/exo/win_analysis.py b/src/exo/win_analysis.py
index 1ff7786..1a8ed77 100644
--- a/src/exo/win_analysis.py
+++ b/src/exo/win_analysis.py
@@ -38,7 +38,7 @@ class WindowAnalysis(LoopIR_Rewrite):
 
             args = [promote_arg(a, sa) for a, sa in zip(args, s.f.args)]
 
-            return [LoopIR.Call(s.f, args, s.eff, s.srcinfo)]
+            return [LoopIR.Call(s.f, args, s.srcinfo)]
 
         return super().map_s(s)
 
@@ -49,6 +49,3 @@ class WindowAnalysis(LoopIR_Rewrite):
 
     def map_t(self, t):
         return t
-
-    def map_eff(self, eff):
-        return eff


Test patch:
diff --git a/tests/golden/test_effects/test_different_id.txt b/tests/golden/test_effects/test_different_id.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_div1.txt b/tests/golden/test_effects/test_div1.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_good_bound1.txt b/tests/golden/test_effects/test_good_bound1.txt
deleted file mode 100644
index 4edc68c..0000000
--- a/tests/golden/test_effects/test_good_bound1.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Reads:
-  { src : (8 * i + j) for (i,j) in Z if
-    0 <= i and i < (n + 7) / 8 and (n - 8 * i < 8 and (0 <= j and j < n - 8 * i)) }
-Writes:
-    { dst : (8 * i + j) for (i,j) in Z if
-    0 <= i and i < (n + 7) / 8 and (n - 8 * i < 8 and (0 <= j and j < n - 8 * i)) }
diff --git a/tests/golden/test_effects/test_index3.txt b/tests/golden/test_effects/test_index3.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_infereffects.txt b/tests/golden/test_effects/test_infereffects.txt
deleted file mode 100644
index 5a7d5d1..0000000
--- a/tests/golden/test_effects/test_infereffects.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-Writes:
-    { A : (i,j) for (i,j) in Z if
-    0 <= i and i < 10 and (0 <= j and j < 20) }
diff --git a/tests/golden/test_effects/test_infereffects2.txt b/tests/golden/test_effects/test_infereffects2.txt
deleted file mode 100644
index 5a7d5d1..0000000
--- a/tests/golden/test_effects/test_infereffects2.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-Writes:
-    { A : (i,j) for (i,j) in Z if
-    0 <= i and i < 10 and (0 <= j and j < 20) }
diff --git a/tests/golden/test_effects/test_mod1.txt b/tests/golden/test_effects/test_mod1.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_new_stride1.txt b/tests/golden/test_effects/test_new_stride1.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_race2.txt b/tests/golden/test_effects/test_race2.txt
deleted file mode 100644
index 5eb609f..0000000
--- a/tests/golden/test_effects/test_race2.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Reads:
-  { x : (i + 1,i) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
-Writes:
-    { x : (i,i) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
diff --git a/tests/golden/test_effects/test_race3.txt b/tests/golden/test_effects/test_race3.txt
deleted file mode 100644
index 73cac76..0000000
--- a/tests/golden/test_effects/test_race3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Reads:
-  { x : (i + 1,i + 0) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
-Writes:
-    { x : (i,i) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
diff --git a/tests/golden/test_effects/test_race4.txt b/tests/golden/test_effects/test_race4.txt
deleted file mode 100644
index e7f94aa..0000000
--- a/tests/golden/test_effects/test_race4.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Reads:
-  { z : (i,i) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
-Writes:
-    { z : (i,i) for (i) in Z if
-    0 <= i and i < n and i + 1 < n }
diff --git a/tests/golden/test_effects/test_seq_write1.txt b/tests/golden/test_effects/test_seq_write1.txt
deleted file mode 100644
index be5909b..0000000
--- a/tests/golden/test_effects/test_seq_write1.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-Reads:
-  { A : (i) for (i) in Z if
-    0 <= i and i < n }
diff --git a/tests/golden/test_effects/test_stride_assert1.txt b/tests/golden/test_effects/test_stride_assert1.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert10.txt b/tests/golden/test_effects/test_stride_assert10.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert11.txt b/tests/golden/test_effects/test_stride_assert11.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert3.txt b/tests/golden/test_effects/test_stride_assert3.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert6.txt b/tests/golden/test_effects/test_stride_assert6.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert7.txt b/tests/golden/test_effects/test_stride_assert7.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert8.txt b/tests/golden/test_effects/test_stride_assert8.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_stride_assert9.txt b/tests/golden/test_effects/test_stride_assert9.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_effects/test_write_write3.txt b/tests/golden/test_effects/test_write_write3.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/tests/golden/test_schedules/test_old_lift_alloc_config.txt b/tests/golden/test_schedules/test_old_lift_alloc_config.txt
new file mode 100644
index 0000000..42a3d2a
--- /dev/null
+++ b/tests/golden/test_schedules/test_old_lift_alloc_config.txt
@@ -0,0 +1,8 @@
+def bar(n: size, A: i8[n] @ DRAM):
+    assert n > 4
+    CFG.cfg = A[0]
+    win_stmt = A[0:4]
+    tmp_a: i8[n + 1] @ DRAM
+    for i in seq(0, n):
+        tmp_a[i] = A[i]
+    A[0] = CFG.cfg
\ No newline at end of file
diff --git a/tests/test_effects.py b/tests/test_bounds.py
similarity index 78%
rename from tests/test_effects.py
rename to tests/test_bounds.py
index 52ab5eb..1c9342c 100644
--- a/tests/test_effects.py
+++ b/tests/test_bounds.py
@@ -7,20 +7,18 @@ from exo.libs.memories import GEMM_SCRATCH
 from exo.stdlib.scheduling import SchedulingError
 
 
-# ------- Effect check tests ---------
+# ------- Bounds check tests ---------
 
 
-def test_seq_write1(golden):
+def test_seq_write1():
     @proc
     def foo(n: size, A: i8[n]):
         a: i8
         for i in seq(0, n):
             a = A[i]
 
-    assert foo.show_effects() == golden
 
-
-def test_new_stride1(golden):
+def test_new_stride1():
     @proc
     def foo(s: stride, scale: f32):
         assert s == 1
@@ -32,20 +30,16 @@ def test_new_stride1(golden):
         scale = 0.0
         foo(stride(A, 0), scale)
 
-    assert bar.show_effects() == golden
-
 
-def test_write_write3(golden):
+def test_write_write3():
     @proc
     def foo(n: size, A: i8[n]):
         a: i8
         for i in seq(0, n):
             a = 3.0
 
-    assert foo.show_effects() == golden
 
-
-def test_different_id(golden):
+def test_different_id():
     @proc
     def foo(n: size):
         for ihi in seq(0, n):
@@ -56,11 +50,8 @@ def test_different_id(golden):
             b: i8 @ DRAM
             b = 0.0
 
-    assert foo.show_effects() == golden
-
 
 # This is fine
-@pytest.mark.skip()
 def test_reduce_write1():
     @proc
     def foo(n: size, A: i8[n]):
@@ -72,7 +63,6 @@ def test_reduce_write1():
 
 
 # This is fine
-@pytest.mark.skip()
 def test_reduce_write2():
     @proc
     def foo(n: size, A: i8[n]):
@@ -84,9 +74,7 @@ def test_reduce_write2():
 
 
 def test_index1():
-    with pytest.raises(
-        TypeError, match="expected expression to always be non-negative"
-    ):
+    with pytest.raises(TypeError, match="to always be non-negative"):
 
         @proc
         def foo(n: index, m: index, A: i8[n, m]):
@@ -110,20 +98,16 @@ def test_index2():
                     a = A[i, j - 1]
 
 
-def test_index3(golden):
+def test_index3():
     @proc
     def foo():
         for i in seq(0, 0):
             a: i8
             a = 0.0
 
-    assert foo.show_effects() == golden
-
 
 def test_index4():
-    with pytest.raises(
-        TypeError, match="expected expression to always be non-negative"
-    ):
+    with pytest.raises(TypeError, match="to always be non-negative"):
 
         @proc
         def foo(n: index):
@@ -133,7 +117,7 @@ def test_index4():
 
 
 # For-loop bound non-negative check tests
-def test_good_bound1(golden):
+def test_good_bound1():
     @proc
     def good_bound1(n: size, dst: R[n] @ DRAM, src: R[n] @ DRAM):
         for i in seq(0, (n + 7) / 8):
@@ -143,8 +127,6 @@ def test_good_bound1(golden):
                 for j in seq(0, n - 8 * i):
                     dst[8 * i + j] = src[8 * i + j]
 
-    assert good_bound1.show_effects() == golden
-
 
 def test_bad_bound1():
     with pytest.raises(TypeError, match="Errors occurred during effect checking"):
@@ -266,18 +248,16 @@ def test_size1():
 
 
 # Data Race? No
-def test_race2(golden):
+def test_race2():
     @proc
     def foo(n: size, x: R[n, n]):
         for i in seq(0, n):
             if i + 1 < n:
                 x[i, i] = x[i + 1, i]
 
-    assert foo.show_effects() == golden
-
 
 # Data Race? No
-def test_race3(golden):
+def test_race3():
     @proc
     def foo(n: size, x: R[n, n]):
         y = x[1:, :]
@@ -285,8 +265,6 @@ def test_race3(golden):
             if i + 1 < n:
                 x[i, i] = y[i, i]
 
-    assert foo.show_effects() == golden
-
 
 # one big issue is aliasing in sub-procedure arguments
 def test_race4():
@@ -303,7 +281,7 @@ def test_race4():
             foo(n, z, z)
 
 
-def test_div1(golden):
+def test_div1():
     @proc
     def foo(n: size):
         assert n == 3
@@ -313,10 +291,8 @@ def test_div1(golden):
     def bar():
         foo(10 / 3)
 
-    assert bar.show_effects() == golden
 
-
-def test_mod1(golden):
+def test_mod1():
     @proc
     def foo(n: size):
         assert n == 1
@@ -326,11 +302,9 @@ def test_mod1(golden):
     def bar():
         foo(10 % 3)
 
-    assert bar.show_effects() == golden
-
 
 # Callee has a window but caller has a tensor case
-def test_stride_assert1(golden):
+def test_stride_assert1():
     @proc
     def foo(
         n: size,
@@ -347,8 +321,6 @@ def test_stride_assert1(golden):
     def bar(x: i8[30, 10] @ DRAM, y: i8[30, 16] @ GEMM_SCRATCH):
         foo(30, 10, x, y)
 
-    assert bar.show_effects() == golden
-
 
 # Both callee and caller has a window case
 def test_stride_assert2():
@@ -372,7 +344,7 @@ def test_stride_assert2():
 
 
 # Both callee and caller has a window case, but with top level assert
-def test_stride_assert3(golden):
+def test_stride_assert3():
     @proc
     def foo(
         n: size,
@@ -391,8 +363,6 @@ def test_stride_assert3(golden):
         assert stride(y, 1) == 1
         foo(30, 10, x, y)
 
-    assert bar.show_effects() == golden
-
 
 # callee is Tensor case and caller is a window case.
 # this will be an error because we don't know anything about incoming stride
@@ -427,17 +397,15 @@ def test_stride_assert5():
 
 
 # Tensor asserting last dimension is fine
-def test_stride_assert6(golden):
+def test_stride_assert6():
     @proc
     def bar(n: size, m: size, x: i8[n, m] @ DRAM):
         assert stride(x, 1) == 1
         pass
 
-    assert bar.show_effects() == golden
-
 
 # Test Tensor having insufficient information (sizes)
-def test_stride_assert7(golden):
+def test_stride_assert7():
     # with changes, this should not trigger an error
     # since it might be true, even if it is highly unlikely
     # i.e. this would have to be always called with m == 10
@@ -446,11 +414,9 @@ def test_stride_assert7(golden):
         assert stride(x, 0) == 10
         pass
 
-    assert bar.show_effects() == golden
-
 
 # Test Windowstmt
-def test_stride_assert8(golden):
+def test_stride_assert8():
     @proc
     def foo(
         n: size,
@@ -470,11 +436,9 @@ def test_stride_assert8(golden):
 
         foo(30, 10, xx, yy)
 
-    assert bar.show_effects() == golden
-
 
 # Test Windowexpr within call arg
-def test_stride_assert9(golden):
+def test_stride_assert9():
     @proc
     def foo(
         n: size,
@@ -491,11 +455,9 @@ def test_stride_assert9(golden):
     def bar(x: i8[8, 30, 10] @ DRAM, y: i8[50, 4, 100, 16] @ GEMM_SCRATCH):
         foo(30, 10, x[0, :, :], y[3, 1, 3:33, :])
 
-    assert bar.show_effects() == golden
-
 
 # Test Alloc
-def test_stride_assert10(golden):
+def test_stride_assert10():
     @proc
     def foo(
         n: size,
@@ -515,11 +477,9 @@ def test_stride_assert10(golden):
 
         foo(30, 10, x[0, :, :], y[3, 1, 3:33, :])
 
-    assert bar.show_effects() == golden
-
 
 # Test stride arguments
-def test_stride_assert11(golden):
+def test_stride_assert11():
     @proc
     def foo(
         n: size,
@@ -541,10 +501,8 @@ def test_stride_assert11(golden):
 
         foo(30, 10, stride(x, 1), x[0, :, :], y[3, 1, 3:33, :])
 
-    assert bar.show_effects() == golden
-
 
-def test_infereffects(golden):
+def test_partial_eval_bounds():
     @proc
     def foo(n: size, m: size, A: f32[n, m]):
         for i in seq(0, n):
@@ -556,78 +514,3 @@ def test_infereffects(golden):
     @proc
     def bar(A: f32[10, 20]):
         foo(A)
-
-    assert bar.show_effects() == golden
-
-
-def test_infereffects2(golden):
-    @proc
-    def foo(n: size, m: size, A: f32[n, m]):
-        for i in seq(0, n):
-            for j in seq(0, m):
-                A[i, j] = 0.0
-
-    foo = foo.partial_eval(10, 20)
-    assert foo.show_effects() == golden
-
-
-# are we testing a case of an else branch?
-
-# what if effset.pred is None?
-
-# size positivity checks
-
-# making sure asserts are checked
-# making sure asserts are used to prove other things
-
-# make sure that effects are getting translated through windowing
-# correctly
-
-# check that windowing is always in-bounds
-#   note checking above translation is maybe better done for data-races
-
-# stride assert
-
-# test basic commutativity properties exhaustively in combinations
-# R,W,+  R,W,+
-#
-# def foo():
-#   x : R
-#   for i in seq(0,2):
-#       x = 3
-#       y = x
-
-# for i in seq(0, n):
-#   x[2*i] = x[2*i+1]
-
-# https://en.wikipedia.org/wiki/Jacobi_method
-# red black gauss seidel
-# https://www.cs.cornell.edu/~bindel/class/cs5220-s10/slides/lec14.pdf
-# wavefront parallel
-"""
-# These are write shadow read tests
-
-# This should work!
-def test_nest_loop1():
-    @proc
-    def foo(n : size, m : size, A : i8[n]):
-        a : i8
-        a = 4.0
-        b : i8
-        for i in seq(0, n):
-            for j in seq(0, m):
-                a    = 0.0
-            b = a
-
-# This is fine
-def test_read_write2():
-    @proc
-    def foo(n : size, A : i8[n]):
-        a : i8[n]
-        a[0] = 4.0
-        for i in seq(0, n):
-            a[0]    = 0.0
-            A[i] = a[0]
-
-
-"""
diff --git a/tests/test_codegen.py b/tests/test_codegen.py
index b9ffbc3..bdc95a3 100644
--- a/tests/test_codegen.py
+++ b/tests/test_codegen.py
@@ -274,9 +274,7 @@ def test_alloc_nest(compiler, tmp_path):
                 res[i, j] = rloc[j]
 
     # Write effect printing to a file
-    (tmp_path / f"{alloc_nest.name()}_effect.atl").write_text(
-        str(alloc_nest.show_effects())
-    )
+    (tmp_path / f"{alloc_nest.name()}_effect.atl").write_text(str(alloc_nest))
 
     x = np.array([[1.0, 2.0, 3.0], [3.2, 4.0, 5.3]], dtype=np.float32)
     y = np.array([[2.6, 3.7, 8.9], [1.3, 2.3, 6.7]], dtype=np.float32)
diff --git a/tests/test_config.py b/tests/test_config.py
index ea19181..da02f36 100644
--- a/tests/test_config.py
+++ b/tests/test_config.py
@@ -371,120 +371,3 @@ def test_ld(golden):
     )
 
     assert f"{config_ld_i8}\n{ld_i8}" == golden
-
-
-"""
-
-    @proc
-    def ld_i8_v1_5(
-        n     : size,
-        m     : size,
-        scale : f32,
-        src   : [i8][n, m] @ DRAM,
-        dst   : [i8][n, 16] @ GEMM_SCRATCH,
-    ):
-        assert n <= 16
-        assert m <= 16
-        assert stride(src, 1) == 1
-        assert stride(dst, 0) == 16
-        assert stride(dst, 1) == 1
-        assert stride(src, 0) == ConfigLoad.src_stride
-
-        ConfigLoad.scale = scale
-        ConfigLoad.src_stride = stride(src, 0)
-
-        for i in seq(0, n):
-            for j in seq(0, m):
-                tmp : f32
-                tmp      = src[i,j]
-                tmp      = tmp * ConfigLoad.scale
-                dst[i,j] = tmp
-
-    @proc
-    def ld_i8_v2(
-        n     : size,
-        m     : size,
-        scale : f32,
-        src   : [i8][n, m] @ DRAM,
-        dst   : [i8][n, 16] @ GEMM_SCRATCH,
-    ):
-        assert n <= 16
-        assert m <= 16
-        assert stride(src, 1) == 1
-        assert stride(dst, 0) == 16
-        assert stride(dst, 1) == 1
-        assert stride(src, 0) == ConfigLoad.src_stride
-
-        config_ld_i8(scale, stride(src, 0))
-        do_ld_i8(n, m, src, dst)
-
-
-    new = (ld_i8.rename("new")
-                .replace(ld_i8, "for i in _:_")
-                .call_eqv(ld_i8_v2, "ld_i8(_, _, _, _, _)"))
-    print(new)
-
-
-
-
-def test_config_write3():
-    ConfigAB = new_config_f32()
-    @proc
-    def foo(n : size):
-        for i in seq(0, n):
-            ConfigAB.a = 3.0
-            ConfigAB.b = ConfigAB.a
-
-
-
-# This is fine
-def test_read_write2():
-    @proc
-    def foo(n : size, A : i8[n]):
-        a : i8
-        a = 4.0
-        for i in seq(0, n):
-            a    = 0.0
-            A[i] = a
-
-    foo.check_effects()
-
-
-
-def new_CONFIG_2f32():
-
-
-
-@proc
-def test_make_config(n: size, dst: R[n] @ DRAM, src: R[n] @ DRAM):
-    for i in seq(0, (n + 7) / 8):
-        if n - 8 * i >= 8:
-            pass
-        else:
-            for j in seq(0, n - 8 * i):
-                dst[8 * i + j] = src[8 * i + j]
-
-
-
-@instr("write_config({a}, {b})")
-def set_real_config( a : f32, b : f32):
-    REAL_CONFIG.a = a
-    REAL_CONFIG.b = b
-
-# st_config_ex
-@proc
-def set_config_a( a : f32 ):
-    DUMMY_CONFIG.a = a
-    set_real_config(DUMMY_CONFIG.a, DUMMY_CONFIG.b )
-
-# matmul_config_ex
-@proc
-def set_config_b( b : f32 ):
-    DUMMY_CONFIG.b = b
-    set_real_config(DUMMY_CONFIG.a, DUMMY_CONFIG.b )
-
-@instr("mvin...")
-def st_i8_v2( ..., stride : stride, ...)
-    set_config_a(stride)
-    do_st_i8(...)
-"""
diff --git a/tests/test_internal_cursors.py b/tests/test_internal_cursors.py
index 5949218..b7c941f 100644
--- a/tests/test_internal_cursors.py
+++ b/tests/test_internal_cursors.py
@@ -113,19 +113,19 @@ def test_gap_insert_pass(proc_foo, golden):
     c = _find_stmt(proc_foo, "x = 0.0")
     assn = c._node
     g = c.after()
-    foo2, _ = g._insert([LoopIR.Pass(None, assn.srcinfo)])
+    foo2, _ = g._insert([LoopIR.Pass(assn.srcinfo)])
     assert str(foo2) == golden
 
 
 def test_insert_root_front(proc_foo, golden):
     c = proc_foo._root()
-    foo2, _ = c.body().before()._insert([LoopIR.Pass(None, c._node.srcinfo)])
+    foo2, _ = c.body().before()._insert([LoopIR.Pass(c._node.srcinfo)])
     assert str(foo2) == golden
 
 
 def test_insert_root_end(proc_foo, golden):
     c = proc_foo._root()
-    foo2, _ = c.body().after()._insert([LoopIR.Pass(None, c._node.srcinfo)])
+    foo2, _ = c.body().after()._insert([LoopIR.Pass(c._node.srcinfo)])
     assert str(foo2) == golden
 
 
@@ -170,7 +170,7 @@ def test_block_replace(proc_bar, golden):
     c = _find_stmt(proc_bar, "for j in _: _")
     stmts = c.body()[1:4]
 
-    bar2, _ = stmts._replace([LoopIR.Pass(None, c._node.srcinfo)])
+    bar2, _ = stmts._replace([LoopIR.Pass(c._node.srcinfo)])
     assert str(bar2) == golden
 
 
@@ -184,7 +184,7 @@ def test_node_replace(proc_bar, golden):
     c = _find_stmt(proc_bar, "x = 3.0")
     assert isinstance(c, Node)
 
-    bar2, _ = c._replace([LoopIR.Pass(None, c._node.srcinfo)])
+    bar2, _ = c._replace([LoopIR.Pass(c._node.srcinfo)])
     assert str(bar2) == golden
 
 
@@ -355,7 +355,7 @@ def test_insert_forward_orelse():
     x2_old = _find_stmt(example_old, "x = 2.0")
     gap = x1_old.after()
 
-    stmt = [LoopIR.Pass(None, x1_old._node.srcinfo)]
+    stmt = [LoopIR.Pass(x1_old._node.srcinfo)]
 
     example_new, fwd = gap._insert(stmt)
     x2_new = _find_stmt(example_new, "x = 2.0")
@@ -438,8 +438,8 @@ def test_block_replace_forward_node(proc_bar, old, new):
     for_j = _find_stmt(proc_bar, "for j in _: _").body()
     bar_new, fwd = for_j[1:4]._replace(
         [
-            LoopIR.Pass(None, for_j.parent()._node.srcinfo),
-            LoopIR.Pass(None, for_j.parent()._node.srcinfo),
+            LoopIR.Pass(for_j.parent()._node.srcinfo),
+            LoopIR.Pass(for_j.parent()._node.srcinfo),
         ]
     )
 
@@ -629,7 +629,7 @@ def test_wrap_block(proc_bar, golden):
         src = body[0].srcinfo
         zero = LoopIR.Const(0, T.index, src)
         eight = LoopIR.Const(8, T.index, src)
-        return LoopIR.For(k, zero, eight, body, LoopIR.Seq(), None, src)
+        return LoopIR.For(k, zero, eight, body, LoopIR.Seq(), src)
 
     procs = []
     for i in range(0, 6):
@@ -654,7 +654,7 @@ def test_wrap_block_forward(proc_bar):
     def wrapper(orelse):
         src = orelse[0].srcinfo
         true = LoopIR.Const(True, T.bool, src)
-        return LoopIR.If(true, [LoopIR.Pass(None, src)], orelse, None, src)
+        return LoopIR.If(true, [LoopIR.Pass(src)], orelse, src)
 
     for i in range(0, 6):
         for j in range(i + 1, 6):
@@ -747,7 +747,7 @@ def test_insert_forwarding_for_blocks(proc_baz, golden):
     b_before = b_edit[:2]
     b_after = b_edit[2:]
 
-    _, fwd = c.after()._insert([LoopIR.Pass(None, c._node.srcinfo)])
+    _, fwd = c.after()._insert([LoopIR.Pass(c._node.srcinfo)])
 
     output = []
     output.append(_print_cursor(fwd(b_above)))  # above edit level
@@ -823,7 +823,7 @@ def test_block_replace_forwarding_for_blocks(proc_baz, golden):
     b_inside = b_edit[2:4]
 
     # replace 1:4 with two pass stmts
-    pass_ir = LoopIR.Pass(None, c[0]._node.srcinfo)
+    pass_ir = LoopIR.Pass(c[0]._node.srcinfo)
     _, fwd = c._replace([pass_ir, pass_ir])
 
     output = []
@@ -855,7 +855,7 @@ def test_node_replace_forwarding(proc_baz):
 
 def test_block_replace_forwarding_stmt_to_stmt(proc_baz):
     c = _find_stmt(proc_baz, "x = 0")
-    _, fwd = c._replace(LoopIR.Pass(None, c._node.srcinfo))
+    _, fwd = c._replace(LoopIR.Pass(c._node.srcinfo))
     assert isinstance(fwd(c)._node, LoopIR.Pass)
 
 
@@ -877,7 +877,7 @@ def test_wrap_forwarding_for_blocks(proc_baz, golden):
         src = body[0].srcinfo
         zero = LoopIR.Const(0, T.index, src)
         eight = LoopIR.Const(8, T.index, src)
-        return LoopIR.For(k, zero, eight, body, LoopIR.Seq(), None, src)
+        return LoopIR.For(k, zero, eight, body, LoopIR.Seq(), src)
 
     _, fwd = c._wrap(wrapper, "body")
 
diff --git a/tests/test_schedules.py b/tests/test_schedules.py
index eddc1a5..810f16d 100644
--- a/tests/test_schedules.py
+++ b/tests/test_schedules.py
@@ -4593,3 +4593,23 @@ def test_stage_mem_reduce2(golden):
 
     foo = stage_mem(foo, foo.body(), "result", "tmp")
     assert str(simplify(foo)) == golden
+
+
+def test_old_lift_alloc_config(golden):
+    @config
+    class CFG:
+        cfg: i8
+
+    @proc
+    def bar(n: size, A: i8[n]):
+        assert n > 4
+
+        CFG.cfg = A[0]
+        win_stmt = A[0:4]
+        for i in seq(0, n):
+            tmp_a: i8
+            tmp_a = A[i]
+        A[0] = CFG.cfg
+
+    bar = autolift_alloc(bar, "tmp_a : _", keep_dims=True)
+    assert str(bar) == golden