diff --git a/UnitTest/DataFlowFramework/DeadCodeAnalysis.lean b/UnitTest/DataFlowFramework/DeadCodeAnalysis.lean
index b44346792..cbb4d1b6f 100644
--- a/UnitTest/DataFlowFramework/DeadCodeAnalysis.lean
+++ b/UnitTest/DataFlowFramework/DeadCodeAnalysis.lean
@@ -6,8 +6,8 @@ open Veir
 
 -- TODO: Facts not initialized in the Dataflow Analysis Framework are implicitly assumed to be the pessimistic bottom state.
 -- We should not assume this implicitly, but rather encode this in the framework!!!!
-def isBlockLive (dfCtx : DataFlowContext) (block : BlockPtr) (irCtx : IRContext OpCode) : Bool :=
-  match dfCtx.getFact? .liveness (.InsertPoint (InsertPoint.atStart! block irCtx)) with
+def isBlockLive (dfCtx : DataFlowContext) (block : BlockPtr) (irCtx : WfIRContext OpCode) : Bool :=
+  match dfCtx.getFact? .liveness (.InsertPoint (InsertPoint.atStart! block irCtx.raw)) with
   | some fact => fact.live
   | none => false
 
@@ -18,7 +18,7 @@ def isEdgeLive (dfCtx : DataFlowContext) (src dst : BlockPtr) : Bool :=
 
 def checkNamedBlockLiveness
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (blockMap : HashMap String BlockPtr)
     (expected : Array (String × Bool)) : MismatchReport := Id.run do
   let mut report := #[]
diff --git a/UnitTest/DataFlowFramework/Dominance.lean b/UnitTest/DataFlowFramework/Dominance.lean
index 7027010dd..4a6ffdeb9 100644
--- a/UnitTest/DataFlowFramework/Dominance.lean
+++ b/UnitTest/DataFlowFramework/Dominance.lean
@@ -31,7 +31,7 @@ private def compareExpectedDominator
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some expectedBlock := recovered.blocks[expectedDom]?
     | return #[s!"dominators {expected.name}: missing block label {expectedDom}"]
   let shouldProperlyDom := expectedDom ≠ expected.name
@@ -55,7 +55,7 @@ private def compareObservedDominator
     (observedBlock : BlockPtr)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let observedByRelation := observedBlock.dominates block dfCtx irCtx
   let observedProperly := observedBlock.properlyDominates block dfCtx irCtx
   let mut report := #[]
@@ -76,7 +76,7 @@ private def compareImmediateDominator
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some block := recovered.blocks[expected.name]?
     | return #[s!"idom {expected.name}: missing block label"]
   let some observedIDom := block.immediateDominator? dfCtx irCtx
@@ -102,7 +102,7 @@ private def compareReachableDominators
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expectedDom in expected.doms.toArray do
     report := report ++ compareExpectedDominator
@@ -123,7 +123,7 @@ private def compareDominators
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some block := recovered.blocks[expected.name]?
     | return #[s!"dominators {expected.name}: missing block label"]
   let observedFact? := block.getDominatorFact? dfCtx irCtx
@@ -145,7 +145,7 @@ private def compareNamedDominators
     (recovered : RecoveredNames)
     (expectations : Array ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expected in expectations do
     report := report ++ compareDominators recovered expected dfCtx irCtx
@@ -156,9 +156,9 @@ private def compareNamedDominators
 private def getNamedOperation?
     (recovered : RecoveredNames)
     (name : String)
-    (irCtx : IRContext OpCode) : Option OperationPtr := do
+    (irCtx : WfIRContext OpCode) : Option OperationPtr := do
   let value ← recovered.values[name]?
-  value.getDefiningOp! irCtx
+  value.getDefiningOp! irCtx.raw
 
 /--
 Compare one expected operation dominance relation.
@@ -167,7 +167,7 @@ private def compareOperationDominance
     (recovered : RecoveredNames)
     (expected : ExpectedOperationDominance)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some dominator := getNamedOperation? recovered expected.dominator irCtx
     | return #[s!"op dominance {expected.dominator}->{expected.dominated}: missing dominator"]
   let some dominated := getNamedOperation? recovered expected.dominated irCtx
@@ -195,7 +195,7 @@ private def compareNamedOperationDominance
     (recovered : RecoveredNames)
     (expectations : Array ExpectedOperationDominance)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expected in expectations do
     report := report ++ compareOperationDominance recovered expected dfCtx irCtx
diff --git a/UnitTest/DataFlowFramework/Helpers.lean b/UnitTest/DataFlowFramework/Helpers.lean
index 786e498d6..16e4234e4 100644
--- a/UnitTest/DataFlowFramework/Helpers.lean
+++ b/UnitTest/DataFlowFramework/Helpers.lean
@@ -77,19 +77,19 @@ Collect all blocks reachable by recursively traversing nested regions in source
 -/
 partial def collectBlocksInSourceOrder
     (op : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (acc : Array BlockPtr := #[]) : Array BlockPtr := Id.run do
   let mut acc := acc
-  for region in (op.get! irCtx).regions do
-    let region := region.get! irCtx
+  for region in (op.get! irCtx.raw).regions do
+    let region := region.get! irCtx.raw
     let mut currentBlock := region.firstBlock
     while let some block := currentBlock do
       acc := acc.push block
-      let mut currentOp := (block.get! irCtx).firstOp
+      let mut currentOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := currentOp do
         acc := collectBlocksInSourceOrder nestedOp irCtx acc
-        currentOp := (nestedOp.get! irCtx).next
-      currentBlock := (block.get! irCtx).next
+        currentOp := (nestedOp.get! irCtx.raw).next
+      currentBlock := (block.get! irCtx.raw).next
   acc
 
 /--
@@ -99,22 +99,22 @@ operation results inside each region.
 -/
 partial def collectValuesInSourceOrder
     (top : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (acc : Array ValuePtr := #[]) : Array ValuePtr := Id.run do
   let mut acc := acc
-  for result in top.getResults! irCtx do
+  for result in top.getResults! irCtx.raw do
     acc := acc.push result
-  for region in (top.get! irCtx).regions do
-    let region := region.get! irCtx
+  for region in (top.get! irCtx.raw).regions do
+    let region := region.get! irCtx.raw
     let mut currentBlock := region.firstBlock
     while let some block := currentBlock do
-      for arg in block.getArguments! irCtx do
+      for arg in block.getArguments! irCtx.raw do
         acc := acc.push arg
-      let mut currentOp := (block.get! irCtx).firstOp
+      let mut currentOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := currentOp do
         acc := collectValuesInSourceOrder nestedOp irCtx acc
-        currentOp := (nestedOp.get! irCtx).next
-      currentBlock := (block.get! irCtx).next
+        currentOp := (nestedOp.get! irCtx.raw).next
+      currentBlock := (block.get! irCtx.raw).next
   acc
 
 /--
@@ -129,7 +129,7 @@ Recover block and SSA value maps by pairing MLIR source names with IR traversal
 -/
 def recoverNames
     (top : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (mlir : String) : Except String RecoveredNames := do
   let blockLabels := blockLabelsFromMlir mlir
   let blocks := collectBlocksInSourceOrder top irCtx
diff --git a/Veir/Analysis/DataFlow/DeadCodeAnalysis.lean b/Veir/Analysis/DataFlow/DeadCodeAnalysis.lean
index 91c5e814b..4cc7ce272 100644
--- a/Veir/Analysis/DataFlow/DeadCodeAnalysis.lean
+++ b/Veir/Analysis/DataFlow/DeadCodeAnalysis.lean
@@ -13,33 +13,33 @@ def mkDefault : LivenessFact :=
   { payload := { latticeElement := .dead } }
 
 def propagate (state : LivenessFact) (anchor : LatticeAnchor)
-  (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+  (dfCtx : DataFlowContext) (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := { dfCtx with workList := state.enqueueDependents dfCtx.workList }
   match anchor with
   | .InsertPoint point =>
     -- Only deal with block start insertion points!
-    if point.prev! irCtx ≠ none then
+    if point.prev! irCtx.raw ≠ none then
       panic! "Dead code propagate called on non block start insertion point"
 
     -- Reinvoke the analyses on the block itself
     for analysisKind in state.subscribers do
       dfCtx := dfCtx.enqueue (point, analysisKind)
 
-    let some block := point.block! irCtx
+    let some block := point.block! irCtx.raw
       | panic! "Dead Code propagate: block start insertion point without block"
 
     -- Reinvoke analyses on all operations in the block
     for analysisKind in state.subscribers do
-      let mut maybeOp := (block.get! irCtx).firstOp
+      let mut maybeOp := (block.get! irCtx.raw).firstOp
       while h : maybeOp.isSome do
         let op := maybeOp.get h
-        let some point := InsertPoint.after? op irCtx
+        let some point := InsertPoint.after? op irCtx.raw
           | panic! "Dead Code propagate: block operation without insertion point"
         dfCtx := dfCtx.enqueue (point, analysisKind)
-        maybeOp := (op.get! irCtx).next
+        maybeOp := (op.get! irCtx.raw).next
   | .CFGEdge edge =>
     for analysisKind in state.subscribers do
-      dfCtx := dfCtx.enqueue (InsertPoint.atStart! edge.target irCtx, analysisKind)
+      dfCtx := dfCtx.enqueue (InsertPoint.atStart! edge.target irCtx.raw, analysisKind)
   | _ =>
     pure ()
   dfCtx
@@ -65,9 +65,9 @@ def markEdgeLive
     (src : BlockPtr)
     (dst : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := dfCtx
-  let point := InsertPoint.atStart! dst irCtx
+  let point := InsertPoint.atStart! dst irCtx.raw
   dfCtx := dfCtx.modifyFactAndPropagate .liveness (.InsertPoint point) (fun fact =>
     (fact.setToLive, !fact.live)) irCtx
   dfCtx := dfCtx.modifyFactAndPropagate .liveness (.CFGEdge { source := src, target := dst }) (fun fact =>
@@ -78,12 +78,12 @@ def markEdgeLive
 def markEntryBlocksLive
     (op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := dfCtx
-  for regionPtr in (op.get! irCtx).regions do
-    let region := regionPtr.get! irCtx
+  for regionPtr in (op.get! irCtx.raw).regions do
+    let region := regionPtr.get! irCtx.raw
     if let some block := region.firstBlock then
-      let point := InsertPoint.atStart! block irCtx
+      let point := InsertPoint.atStart! block irCtx.raw
       dfCtx := dfCtx.modifyFactAndPropagate .liveness (.InsertPoint point) (fun fact =>
         (fact.setToLive, !fact.live)) irCtx
   dfCtx
@@ -95,9 +95,9 @@ an interface much like what MLIR has.
 -/
 private def isBranchOp
     (op : OperationPtr)
-    (irCtx : IRContext OpCode) : Bool :=
+    (irCtx : WfIRContext OpCode) : Bool :=
   -- TODO: Replace this `.test .test` check once VeIR has proper branch ops.
-  match (op.get! irCtx).opType with
+  match (op.get! irCtx.raw).opType with
   | .test .test => true
   | _ => false
 
@@ -106,15 +106,15 @@ Read a literal constant directly from the defining operation when possible.
 -/
 private def getLiteralConstant?
     (value : ValuePtr)
-    (irCtx : IRContext OpCode) : Option AbstractConstant :=
+    (irCtx : WfIRContext OpCode) : Option AbstractConstant :=
   match value with
   | .opResult result =>
     if result.index ≠ 0 then
       none
     else
-      match (result.op.get! irCtx).opType with
+      match (result.op.get! irCtx.raw).opType with
       | .arith .constant =>
-        let intAttr := (result.op.getProperties! irCtx Arith.constant).value
+        let intAttr := (result.op.getProperties! irCtx.raw Arith.constant).value
         some (.constant ⟨intAttr.type.bitwidth, Data.LLVM.Int.constant intAttr.type.bitwidth intAttr.value⟩)
       | _ =>
         none
@@ -129,8 +129,8 @@ code analysis remains useful without any external constant information.
 private def getOperandValues
     (op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext × Option (Array AbstractConstant) := Id.run do
-  let operands := (op.getOperands! irCtx).map fun operand =>
+    (irCtx : WfIRContext OpCode) : DataFlowContext × Option (Array AbstractConstant) := Id.run do
+  let operands := (op.getOperands! irCtx.raw).map fun operand =>
     match getLiteralConstant? operand irCtx with
     | some literal => literal
     | none => .top
@@ -150,18 +150,18 @@ TODO: Replace this once VeIR supports branch operators! For now, we treat
 private def getSuccessorForOperands?
     (op : OperationPtr)
     (operands : Array AbstractConstant)
-    (irCtx : IRContext OpCode) : Option BlockPtr :=
-  if op.getNumSuccessors! irCtx = 1 then
-    some (op.getSuccessor! irCtx 0)
-  else if op.getNumSuccessors! irCtx = 2 then
+    (irCtx : WfIRContext OpCode) : Option BlockPtr :=
+  if op.getNumSuccessors! irCtx.raw = 1 then
+    some (op.getSuccessor! irCtx.raw 0)
+  else if op.getNumSuccessors! irCtx.raw = 2 then
     match operands[0]? with
     | some (AbstractConstant.constant constant) =>
       match constant.value with
       | Data.LLVM.Int.val value =>
         if value = 0 then
-          some (op.getSuccessor! irCtx 1)
+          some (op.getSuccessor! irCtx.raw 1)
         else
-          some (op.getSuccessor! irCtx 0)
+          some (op.getSuccessor! irCtx.raw 0)
       | Data.LLVM.Int.poison =>
         none
     | _ =>
@@ -177,12 +177,12 @@ of both the operation results and any nested regions.
 def visitBranchOperation
     (branch : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   -- Try to deduce a single successor for the branch.
   let (dfCtx, operands?) := getOperandValues branch dfCtx irCtx
   let some operands := operands?
     | return dfCtx
-  let some parentBlock := (branch.get! irCtx).parent
+  let some parentBlock := (branch.get! irCtx.raw).parent
     | return dfCtx
 
   match getSuccessorForOperands? branch operands irCtx with
@@ -191,7 +191,7 @@ def visitBranchOperation
   | none =>
     -- Otherwise, mark all successors as executable and outgoing edges.
     let mut dfCtx := dfCtx
-    for successor in branch.getSuccessors! irCtx do
+    for successor in branch.getSuccessors! irCtx.raw do
       dfCtx := markEdgeLive parentBlock successor dfCtx irCtx
     dfCtx
 /--
@@ -200,11 +200,11 @@ Visit an operation and deduce which of its successors are live.
 private def visitOp
     (op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   -- If the parent block is not live, there is nothing to do.
-  if hParent : (op.get! irCtx).parent.isSome then
-    let parentBlock := (op.get! irCtx).parent.get hParent
-    let blockPoint := InsertPoint.atStart! parentBlock irCtx
+  if hParent : (op.get! irCtx.raw).parent.isSome then
+    let parentBlock := (op.get! irCtx.raw).parent.get hParent
+    let blockPoint := InsertPoint.atStart! parentBlock irCtx.raw
     match dfCtx.getFact? .liveness (.InsertPoint blockPoint) with
     | some liveFact =>
       -- If parent block not live, skip op.
@@ -219,7 +219,7 @@ private def visitOp
 
   -- TODO: If we have a live call op, add this as a live predecessor of the callee.
 
-  if op.getNumRegions! irCtx ≠ 0 then
+  if op.getNumRegions! irCtx.raw ≠ 0 then
     -- TODO: Check if we can reason about region control-flow.
 
     -- TODO: Check if this is a callable operation and use callsite information
@@ -231,16 +231,16 @@ private def visitOp
   -- TODO: If `op` is a region or callable return, visit the corresponding
   -- terminator semantics once VeIR has the necessary interfaces.
 
-  if op.getNumSuccessors! irCtx ≠ 0 then
-    if hParent : (op.get! irCtx).parent.isSome then
-      let parentBlock := (op.get! irCtx).parent.get hParent
+  if op.getNumSuccessors! irCtx.raw ≠ 0 then
+    if hParent : (op.get! irCtx.raw).parent.isSome then
+      let parentBlock := (op.get! irCtx.raw).parent.get hParent
 
       -- Check if we can reason about the control-flow.
       if isBranchOp op irCtx then
         dfCtx := visitBranchOperation op dfCtx irCtx
       else
         -- Conservatively mark all successors as live.
-        for successor in op.getSuccessors! irCtx do
+        for successor in op.getSuccessors! irCtx.raw do
           dfCtx := markEdgeLive parentBlock successor dfCtx irCtx
     else
       -- TODO: Handle standalone operations with successors if VeIR ever models them.
@@ -251,8 +251,8 @@ private def visitOp
 def visit
     (point : InsertPoint)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
-  match point.prev! irCtx with
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
+  match point.prev! irCtx.raw with
   | none => dfCtx
   | some op => visitOp op dfCtx irCtx
 
@@ -264,18 +264,18 @@ liveness, then recurse into nested regions.
 partial def initializeRecursively
     (op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := dfCtx
 
   -- Initialize the analysis by visiting every op with control-flow semantics.
-  if op.getNumRegions! irCtx ≠ 0 || op.getNumSuccessors! irCtx ≠ 0 then
+  if op.getNumRegions! irCtx.raw ≠ 0 || op.getNumSuccessors! irCtx.raw ≠ 0 then
     -- TODO: || isRegionOrCallableReturn op || isACallOpInterface op
 
     -- When the liveness of the parent block changes, make sure to re-invoke
     -- the analysis on the op.
-    if h : (op.get! irCtx).parent.isSome then
-      let parentBlock := (op.get! irCtx).parent.get h
-      let blockPoint := InsertPoint.atStart! parentBlock irCtx
+    if h : (op.get! irCtx.raw).parent.isSome then
+      let parentBlock := (op.get! irCtx.raw).parent.get h
+      let blockPoint := InsertPoint.atStart! parentBlock irCtx.raw
       dfCtx := dfCtx.modifyFact .liveness (.InsertPoint blockPoint) (fun fact =>
         fact.subscribe kind)
 
@@ -283,24 +283,24 @@ partial def initializeRecursively
     dfCtx := visitOp op dfCtx irCtx
 
   -- Recurse on nested operations.
-  for regionPtr in (op.get! irCtx).regions do
+  for regionPtr in (op.get! irCtx.raw).regions do
     -- TODO: If we haven't seen a symbol table yet, check if the current
     -- operation has one. If so, update the flag to allow for resolving
     -- callables in nested regions.
-    let region := regionPtr.get! irCtx
+    let region := regionPtr.get! irCtx.raw
     let mut maybeBlock := region.firstBlock
     while let some block := maybeBlock do
-      let mut maybeOp := (block.get! irCtx).firstOp
+      let mut maybeOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := maybeOp do
         dfCtx := initializeRecursively nestedOp dfCtx irCtx
-        maybeOp := (nestedOp.get! irCtx).next
-      maybeBlock := (block.get! irCtx).next
+        maybeOp := (nestedOp.get! irCtx.raw).next
+      maybeBlock := (block.get! irCtx.raw).next
   dfCtx
 
 def init
     (top : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   -- Mark the top level blocks as live.
   let dfCtx := markEntryBlocksLive top dfCtx irCtx
 
diff --git a/Veir/Analysis/DataFlow/DominanceAnalysis.lean b/Veir/Analysis/DataFlow/DominanceAnalysis.lean
index 784400e60..972f33837 100644
--- a/Veir/Analysis/DataFlow/DominanceAnalysis.lean
+++ b/Veir/Analysis/DataFlow/DominanceAnalysis.lean
@@ -46,8 +46,8 @@ Returns `none` when dominance analysis has not attached a dominator fact to that
 block entry.
 -/
 def getDominatorFact? [FactSpec .dominator] (block : BlockPtr) (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option DominatorFact :=
-  dfCtx.getFact? .dominator (.InsertPoint (InsertPoint.atStart! block irCtx))
+    (irCtx : WfIRContext OpCode) : Option DominatorFact :=
+  dfCtx.getFact? .dominator (.InsertPoint (InsertPoint.atStart! block irCtx.raw))
 
 /--
 Return the immediate dominator currently recorded for `block`.
@@ -57,7 +57,7 @@ returns `none` when the fact is missing or when the fact has no immediate
 dominator yet.
 -/
 def getIDom? [FactSpec .dominator] (block : BlockPtr) (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option BlockPtr :=
+    (irCtx : WfIRContext OpCode) : Option BlockPtr :=
   block.getDominatorFact? dfCtx irCtx >>= (·.iDom)
 
 end BlockPtr
@@ -71,9 +71,9 @@ Returns `none` when the region has no entry block or when region metadata has
 not been attached to that entry block.
 -/
 def getRegionMetadataFact? [FactSpec .regionMetadata] (region : RegionPtr) (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option RegionMetadataFact :=
-  (region.get! irCtx).firstBlock >>= 
-    dfCtx.getFact? .regionMetadata ∘ (InsertPoint.atStart! · irCtx)
+    (irCtx : WfIRContext OpCode) : Option RegionMetadataFact :=
+  (region.get! irCtx.raw).firstBlock >>= 
+    dfCtx.getFact? .regionMetadata ∘ (InsertPoint.atStart! · irCtx.raw)
 
 end RegionPtr
 
@@ -84,7 +84,7 @@ def mkDefault : DominatorFact :=
     payload := { iDom := none } }
 
 def propagate (fact : DominatorFact) (_anchor : LatticeAnchor) 
-    (dfCtx : DataFlowContext) (_irCtx : IRContext OpCode) : DataFlowContext :=
+    (dfCtx : DataFlowContext) (_irCtx : WfIRContext OpCode) : DataFlowContext :=
   { dfCtx with workList := fact.enqueueDependents dfCtx.workList }
 
 instance : FactSpec .dominator where
@@ -100,7 +100,7 @@ def mkDefault : RegionMetadataFact :=
     payload := { postOrderIndex := {} } }
 
 def propagate (_fact : RegionMetadataFact) (_anchor : LatticeAnchor) 
-    (dfCtx : DataFlowContext) (_irCtx : IRContext OpCode) : DataFlowContext :=
+    (dfCtx : DataFlowContext) (_irCtx : WfIRContext OpCode) : DataFlowContext :=
   dfCtx
 
 instance : FactSpec .regionMetadata where
@@ -120,10 +120,10 @@ postorder index used by `intersect`.
 -/
 private def collectPostOrder
     (region : RegionPtr)
-    (irCtx : IRContext OpCode) : Array BlockPtr × HashMap BlockPtr Nat := Id.run do
+    (irCtx : WfIRContext OpCode) : Array BlockPtr × HashMap BlockPtr Nat := Id.run do
   let mut postOrder : Array BlockPtr := #[]
   let mut postOrderIndex : HashMap BlockPtr Nat := {}
-  let some entry := (region.get! irCtx).firstBlock
+  let some entry := (region.get! irCtx.raw).firstBlock
     | return (postOrder, postOrderIndex)
   let mut stack : Array (BlockPtr × Bool) := #[(entry, false)]
   let mut seen : HashSet BlockPtr := ∅
@@ -141,8 +141,8 @@ private def collectPostOrder
       seen := seen.insert block
       stack := stack.push (block, true)
 
-      if let some terminator := (block.get! irCtx).lastOp then
-        for succ in terminator.getSuccessors! irCtx do
+      if let some terminator := (block.get! irCtx.raw).lastOp then
+        for succ in terminator.getSuccessors! irCtx.raw do
           if !seen.contains succ then
             stack := stack.push (succ, false)
   (postOrder, postOrderIndex)
@@ -151,51 +151,51 @@ private def collectPostOrder
 private def initializeRegion
     (region : RegionPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := dfCtx
-  let some entry := (region.get! irCtx).firstBlock
+  let some entry := (region.get! irCtx.raw).firstBlock
     | return dfCtx
   let (postOrder, postOrderIndex) := collectPostOrder region irCtx
   let reversePostOrder := postOrder.reverse
   dfCtx :=
-    dfCtx.modifyFact .regionMetadata (InsertPoint.atStart! entry irCtx) fun fact =>
+    dfCtx.modifyFact .regionMetadata (InsertPoint.atStart! entry irCtx.raw) fun fact =>
       fact.setPostOrderIndex postOrderIndex
 
   for block in reversePostOrder do
     let mut dependents := #[]
-    if let some terminator := (block.get! irCtx).lastOp then
-      for succ in terminator.getSuccessors! irCtx do
-        dependents := dependents.push (InsertPoint.atStart! succ irCtx, kind)
-    dfCtx := dfCtx.modifyFact .dominator (InsertPoint.atStart! block irCtx) fun fact =>
+    if let some terminator := (block.get! irCtx.raw).lastOp then
+      for succ in terminator.getSuccessors! irCtx.raw do
+        dependents := dependents.push (InsertPoint.atStart! succ irCtx.raw, kind)
+    dfCtx := dfCtx.modifyFact .dominator (InsertPoint.atStart! block irCtx.raw) fun fact =>
       (fact.setDependents dependents).setIDom
         (if block = entry then some entry else none)
-    dfCtx := dfCtx.enqueue (InsertPoint.atStart! block irCtx, kind)
+    dfCtx := dfCtx.enqueue (InsertPoint.atStart! block irCtx.raw, kind)
   dfCtx
 
 /-- Recursively initialize the analysis on nested regions. -/
 partial def initializeRecursively
     (op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := dfCtx
 
-  for region in op.getRegions! irCtx do
+  for region in op.getRegions! irCtx.raw do
     dfCtx := initializeRegion region dfCtx irCtx
 
-    let mut currentBlock := (region.get! irCtx).firstBlock
+    let mut currentBlock := (region.get! irCtx.raw).firstBlock
     while let some block := currentBlock do
-      let mut currentOp := (block.get! irCtx).firstOp
+      let mut currentOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := currentOp do
         dfCtx := initializeRecursively nestedOp dfCtx irCtx
-        currentOp := (nestedOp.get! irCtx).next
-      currentBlock := (block.get! irCtx).next
+        currentOp := (nestedOp.get! irCtx.raw).next
+      currentBlock := (block.get! irCtx.raw).next
 
   dfCtx
 
 def init
     (top : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext :=
+    (irCtx : WfIRContext OpCode) : DataFlowContext :=
   initializeRecursively top dfCtx irCtx
 
 /--
@@ -208,7 +208,7 @@ private def intersect
     (block1 block2 : BlockPtr)
     (postOrderIndex : HashMap BlockPtr Nat)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : BlockPtr := Id.run do
+    (irCtx : WfIRContext OpCode) : BlockPtr := Id.run do
   let mut finger1 := block1
   let mut finger2 := block2
   while finger1 ≠ finger2 do
@@ -228,21 +228,21 @@ repeatedly `intersect` that candidate with each other processed predecessor.
 private def computeImmediateDominator
     (block : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option BlockPtr := do
-  let region := ((block.get! irCtx).parent).get!
-  let entry := ((region.get! irCtx).firstBlock).get!
+    (irCtx : WfIRContext OpCode) : Option BlockPtr := do
+  let region := ((block.get! irCtx.raw).parent).get!
+  let entry := ((region.get! irCtx.raw).firstBlock).get!
   let metadata ← region.getRegionMetadataFact? dfCtx irCtx
   if block = entry then 
     return entry
 
-  let mut currentPredUse := (block.get! irCtx).firstUse
+  let mut currentPredUse := (block.get! irCtx.raw).firstUse
   let mut newIDom : Option BlockPtr := none
 
   while let some predUse := currentPredUse do
-    let predUseStruct := predUse.get! irCtx
+    let predUseStruct := predUse.get! irCtx.raw
     currentPredUse := predUseStruct.nextUse
     let predOp := predUseStruct.owner
-    let some predBlock := (predOp.get! irCtx).parent
+    let some predBlock := (predOp.get! irCtx.raw).parent
       | continue
     let some _ := predBlock.getIDom? dfCtx irCtx
       | continue
@@ -264,16 +264,16 @@ candidate and update the fact stored at that entry when the candidate changes.
 def visit
     (point : InsertPoint)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext :=
-  if point.prev! irCtx ≠ none then
+    (irCtx : WfIRContext OpCode) : DataFlowContext :=
+  if point.prev! irCtx.raw ≠ none then
     -- Dominance facts are attached only to block-entry insertion points.
     dfCtx
   else
-    let block := (point.block! irCtx).get!
+    let block := (point.block! irCtx.raw).get!
     match computeImmediateDominator block dfCtx irCtx with
     | none => dfCtx
     | some newIDom => 
-      let anchor := InsertPoint.atStart! block irCtx
+      let anchor := InsertPoint.atStart! block irCtx.raw
       dfCtx.modifyFactAndPropagate .dominator anchor (fun fact =>
        (fact.setIDom (some newIDom), some newIDom ≠ fact.iDom)) irCtx
 
diff --git a/Veir/Analysis/DataFlow/SparseFact.lean b/Veir/Analysis/DataFlow/SparseFact.lean
index d3783bdb1..c22e349d1 100644
--- a/Veir/Analysis/DataFlow/SparseFact.lean
+++ b/Veir/Analysis/DataFlow/SparseFact.lean
@@ -37,19 +37,19 @@ Propagate a sparse lattice update by revisiting dependents and all users of the
 updated SSA value for subscribed analyses.
 -/
 def propagate (state : Fact kind) (anchor : LatticeAnchor) 
-  (dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
+  (dfCtx : DataFlowContext) (irCtx : WfIRContext OpCode) : DataFlowContext := Id.run do
   let mut dfCtx := { dfCtx with workList := state.enqueueDependents dfCtx.workList }
   match anchor with
   | .ValuePtr ssaValue =>
-    let mut maybeUse := ssaValue.getFirstUse! irCtx
+    let mut maybeUse := ssaValue.getFirstUse! irCtx.raw
     while let some use := maybeUse do
-      let user := (use.get! irCtx).owner
-      match InsertPoint.after? user irCtx with
+      let user := (use.get! irCtx.raw).owner
+      match InsertPoint.after? user irCtx.raw with
       | some point =>
         for analysisKind in state.subscribers do
           dfCtx := dfCtx.enqueue (point, analysisKind)
       | none => pure ()
-      maybeUse := (use.get! irCtx).nextUse
+      maybeUse := (use.get! irCtx.raw).nextUse
   | _ =>
     pure ()
   dfCtx
diff --git a/Veir/Analysis/DataFlowFramework.lean b/Veir/Analysis/DataFlowFramework.lean
index c72e43132..31a0b46d0 100644
--- a/Veir/Analysis/DataFlowFramework.lean
+++ b/Veir/Analysis/DataFlowFramework.lean
@@ -1,6 +1,7 @@
 module
 
 public import Veir.Analysis.DataFlow.Facts
+public import Veir.IR.WellFormed
 
 open Std (DHashMap HashMap)
 
@@ -37,7 +38,7 @@ class FactSpec (kind : FactKind) where
   Hook that's called when the fact changes state. Typically used to
   enqueue a fact's dependents because it changed.
   -/
-  propagate : Fact kind → LatticeAnchor → DataFlowContext → IRContext OpCode → DataFlowContext
+  propagate : Fact kind → LatticeAnchor → DataFlowContext → WfIRContext OpCode → DataFlowContext
 
 namespace Fact
 
@@ -54,7 +55,7 @@ def propagate [FactSpec kind]
     (fact : Fact kind)
     (anchor : LatticeAnchor)
     (ctx : DataFlowContext)
-    (irCtx : IRContext OpCode) : DataFlowContext :=
+    (irCtx : WfIRContext OpCode) : DataFlowContext :=
   FactSpec.propagate (kind := kind) fact anchor ctx irCtx
 
 end Fact
@@ -72,11 +73,11 @@ structure DataFlowAnalysis where
   This often involves enqueueing some number of work items into the work list, such
   as every SSA value reachable from the top level operation pointer.
   -/
-  init : OperationPtr → DataFlowContext → IRContext OpCode → DataFlowContext
+  init : OperationPtr → DataFlowContext → WfIRContext OpCode → DataFlowContext
   /--
   The transfer function, visiting the given `InsertPoint`.
   -/
-  visit : InsertPoint → DataFlowContext → IRContext OpCode → DataFlowContext
+  visit : InsertPoint → DataFlowContext → WfIRContext OpCode → DataFlowContext
 
 namespace DataFlowContext
 
@@ -128,7 +129,7 @@ def modifyFactAndPropagate (kind : FactKind) [spec : FactSpec kind]
     (ctx : DataFlowContext)
     (anchor : LatticeAnchor)
     (f : Fact kind → Fact kind × Bool)
-    (irCtx : IRContext OpCode) : DataFlowContext :=
+    (irCtx : WfIRContext OpCode) : DataFlowContext :=
   let current := ctx.getOrMkFact kind anchor
   let (fact, changed) := f current
   let ctx := ctx.setFact kind anchor fact
@@ -151,7 +152,7 @@ Returns `Option` since `run` may run forever.
 TODO: Eventually prove via monotonicity that this is in fact impossible.
 -/
 partial def run (analyses : RegisteredAnalyses) (ctx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option DataFlowContext :=
+    (irCtx : WfIRContext OpCode) : Option DataFlowContext :=
   match ctx.workList.dequeue? with
   | none => some ctx
   | some ((point, analysisKind), workList) =>
@@ -169,7 +170,7 @@ Initialize the registered analyses and run the worklist solver to a fixpoint.
 Returns `some` whenever it terminates.
 -/
 def fixpointSolve (top : OperationPtr) (analyses : Array DataFlowAnalysis)
-    (irCtx : IRContext OpCode) : Option DataFlowContext := Id.run do
+    (irCtx : WfIRContext OpCode) : Option DataFlowContext := Id.run do
   let mut ctx := DataFlowContext.empty
   let mut registeredAnalyses : RegisteredAnalyses := ∅
   for analysis in analyses do
diff --git a/Veir/IR/Dominance.lean b/Veir/IR/Dominance.lean
index ff95fa532..ecbcd3851 100644
--- a/Veir/IR/Dominance.lean
+++ b/Veir/IR/Dominance.lean
@@ -18,12 +18,12 @@ escapes the IR hierarchy before reaching `region`, return `none`.
 private partial def normalizeInsertPoint
     (region : RegionPtr)
     (point : InsertPoint)
-    (irCtx : IRContext OpCode) : Option InsertPoint := do
-  let block ← point.block! irCtx
-  if (block.get! irCtx).parent = some region then
+    (irCtx : WfIRContext OpCode) : Option InsertPoint := do
+  let block ← point.block! irCtx.raw
+  if (block.get! irCtx.raw).parent = some region then
     return point
-  let parentRegion ← (block.get! irCtx).parent
-  let parentOp ← (parentRegion.get! irCtx).parent
+  let parentRegion ← (block.get! irCtx.raw).parent
+  let parentOp ← (parentRegion.get! irCtx.raw).parent
   normalizeInsertPoint region (.before parentOp) irCtx
 
 /--
@@ -36,7 +36,7 @@ upward until it either reaches `dominator` or the chain ends.
 private partial def BlockPtr.dominatesWithinRegion
     (dominator block : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool := Id.run do
+    (irCtx : WfIRContext OpCode) : Bool := Id.run do
   if dominator = block then
     true
   else
@@ -53,12 +53,12 @@ Iterates from `dominator` down the block until it either reaches
 -/
 private def OperationPtr.dominatesWithinBlock
     (dominator op : OperationPtr)
-    (irCtx : IRContext OpCode) : Bool := Id.run do
+    (irCtx : WfIRContext OpCode) : Bool := Id.run do
   let mut current := some dominator
   while let some operation := current do
     if operation = op then
       return true
-    current := (operation.get! irCtx).next
+    current := (operation.get! irCtx.raw).next
   false
 
 namespace InsertPoint
@@ -69,7 +69,7 @@ to lie in the same block.
 -/
 private def dominatesWithinBlock
     (dominator point : InsertPoint)
-    (irCtx : IRContext OpCode) : Bool := Id.run do
+    (irCtx : WfIRContext OpCode) : Bool := Id.run do
   if dominator = point then
     return true
   match dominator, point with
@@ -93,10 +93,10 @@ private def dominates
     (dominator : InsertPoint)
     (point : InsertPoint)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool := Id.run do
-  let some dominatorBlock := dominator.block! irCtx
+    (irCtx : WfIRContext OpCode) : Bool := Id.run do
+  let some dominatorBlock := dominator.block! irCtx.raw
     | return false
-  let some dominatorRegion := (dominatorBlock.get! irCtx).parent
+  let some dominatorRegion := (dominatorBlock.get! irCtx.raw).parent
     | return false
 
   -- If the point does not lie in the same region as `dominator`, scoot up
@@ -105,7 +105,7 @@ private def dominates
   -- doesn't properly dominate the point.
   let some point := normalizeInsertPoint dominatorRegion point irCtx
     | return false 
-  let some pointBlock := point.block! irCtx
+  let some pointBlock := point.block! irCtx.raw
     | return false
 
   if dominatorBlock = pointBlock then
@@ -122,7 +122,7 @@ private def properlyDominates
     (dominator : InsertPoint)
     (point : InsertPoint)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool :=
+    (irCtx : WfIRContext OpCode) : Bool :=
   dominator ≠ point && dominator.dominates point dfCtx irCtx
 
 
@@ -138,7 +138,7 @@ def immediateDominator?
     [FactSpec .dominator]
     (block : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Option BlockPtr :=
+    (irCtx : WfIRContext OpCode) : Option BlockPtr :=
   block.getIDom? dfCtx irCtx
 
 /--
@@ -148,8 +148,8 @@ def dominates
     [FactSpec .dominator]
     (dominator block : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool :=
-  (InsertPoint.atStart! dominator irCtx).dominates (InsertPoint.atStart! block irCtx) dfCtx irCtx
+    (irCtx : WfIRContext OpCode) : Bool :=
+  (InsertPoint.atStart! dominator irCtx.raw).dominates (InsertPoint.atStart! block irCtx.raw) dfCtx irCtx
 
 /--
 Dominance query between two blocks, where a block does not dominate itself.
@@ -158,9 +158,9 @@ def properlyDominates
     [FactSpec .dominator]
     (dominator block : BlockPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool :=
-  (InsertPoint.atStart! dominator irCtx).properlyDominates
-    (InsertPoint.atStart! block irCtx) dfCtx irCtx
+    (irCtx : WfIRContext OpCode) : Bool :=
+  (InsertPoint.atStart! dominator irCtx.raw).properlyDominates
+    (InsertPoint.atStart! block irCtx.raw) dfCtx irCtx
 
 end BlockPtr
 
@@ -172,7 +172,7 @@ Dominance query between two operations, where an operation dominates itself.
 def dominates
     (dominator op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool :=
+    (irCtx : WfIRContext OpCode) : Bool :=
   (InsertPoint.before dominator).dominates (InsertPoint.before op) dfCtx irCtx
 
 /--
@@ -181,7 +181,7 @@ Dominance query between two operations, where an operation does not dominate its
 def properlyDominates
     (dominator op : OperationPtr)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : Bool :=
+    (irCtx : WfIRContext OpCode) : Bool :=
   (InsertPoint.before dominator).properlyDominates (InsertPoint.before op) dfCtx irCtx
 
 end OperationPtr