From d652078af3c0ed3ae3024abed5220d33c84f50e1 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Wed, 18 Dec 2024 15:50:48 -0800
Subject: [PATCH] properly track divergence points for single-sided nodes

ensures that when a two-sided node is split, the resulting
single-sided nodes mark the original node as the divergence point

previously this was checked at run-time. With the
'Quant' module we can enforce this statically by
restricting the allowed cases for divergence points
---
 src/Data/Quant.hs                       |  42 ++--
 src/Pate/Verification/PairGraph.hs      |  44 ++--
 src/Pate/Verification/PairGraph/Node.hs | 285 +++++++++++++++++-------
 src/Pate/Verification/StrongestPosts.hs |  51 +++--
 src/Pate/Verification/Widening.hs       |  89 ++++----
 5 files changed, 327 insertions(+), 184 deletions(-)

diff --git a/src/Data/Quant.hs b/src/Data/Quant.hs
index b45c9d19..afbfd9fc 100644
--- a/src/Data/Quant.hs
+++ b/src/Data/Quant.hs
@@ -80,6 +80,7 @@ module Data.Quant
     , pattern ExistsOne
     , pattern ExistsAll
     , IsExistsOr(..)
+    , ExistsOrCases(..)
     , TheOneK
     , IfIsOneK
     , coerceExists
@@ -367,11 +368,15 @@ instance KnownRepr QuantRepr tp => KnownRepr (QuantCoercion tp) tp where
     knownRepr = CoerceRefl knownRepr
 
 data QuantConversion (t1 :: QuantK k) (t2 :: QuantK k) where
+    ConvertRefl :: ReprOf x -> QuantConversion x x
+    ConvertNone :: ReprOf x -> ReprOf y -> QuantConversion x y
     ConvertExistsToAll :: QuantConversion ExistsK AllK
     ConvertExistsToOne :: ReprOf x -> QuantConversion ExistsK (OneK x)
 
 instance HasReprK k => IsRepr (QuantConversion (t1 :: QuantK k)) where
     withRepr x f = case x of
+        ConvertRefl repr -> withRepr repr $ f
+        ConvertNone repr1 repr2 -> withRepr repr1 $ withRepr repr2 $ f
         ConvertExistsToAll -> f
         ConvertExistsToOne repr -> withRepr repr $ f
 
@@ -451,16 +456,27 @@ pattern SomeSingle repr x <- ((\l -> toSingleQuant l >>= toSomeSingle) -> (Just
 
 type KnownConversion (tp1 :: QuantK k) (tp2 :: QuantK k) = KnownRepr (QuantConversion tp1) tp2
 
-
+{-
 instance KnownRepr (QuantConversion ExistsK) AllK where
     knownRepr = ConvertExistsToAll
 
 instance (KnownRepr (ReprOf :: k -> Type) (x :: k)) => KnownRepr (QuantConversion ExistsK) (OneK x) where
     knownRepr = ConvertExistsToOne knownRepr
+-}
+
+instance forall k x1 x2. (HasReprK k, KnownRepr QuantRepr (x1 :: QuantK k), KnownRepr QuantRepr x2) => KnownRepr (QuantConversion x1) x2 where
+  knownRepr = case (knownRepr :: QuantRepr x1, knownRepr :: QuantRepr x2) of
+    (QuantSomeRepr, QuantAllRepr) -> ConvertExistsToAll
+    (QuantSomeRepr, QuantOneRepr repr) -> ConvertExistsToOne repr
+    (x, y) | Just Refl <- testEquality x y -> ConvertRefl x
+    _ -> ConvertNone knownRepr knownRepr
+
 
 
 instance QuantConvertible (Quant (f :: k -> Type)) where
     applyQuantConversion qc q = case (qc, q) of
+        (ConvertRefl{}, _) -> Just q
+        (ConvertNone{}, _) -> Nothing
         (ConvertExistsToAll, QuantAny q') -> Just q'
         (ConvertExistsToAll, QuantExists{}) -> Nothing
         (ConvertExistsToOne repr, QuantAny q') -> Just (applyQuantCoercion (CoerceAllToOne repr) q')
@@ -495,13 +511,13 @@ data ExistsOrCases (tp1 :: QuantK k) (tp2 :: QuantK k) where
     ExistsOrRefl :: ExistsOrCases tp tp
     ExistsOrExists :: ExistsOrCases ExistsK tp
 
-type family IsExistsOrConstraint (tp1 :: QuantK k) (tp2 :: QuantK k) :: Constraint
+type family IsExistsOrConstraint (tp1 :: QuantK k) (tp2 :: QuantK k) :: Constraint where
+  IsExistsOrConstraint (OneK x) tp = (OneK x ~ tp)
+  IsExistsOrConstraint (AllK :: QuantK k) tp = ((AllK :: QuantK k) ~ tp)
+  IsExistsOrConstraint ExistsK _ = ()
 
-class IsExistsOrConstraint tp1 tp2 => IsExistsOr (tp1 :: QuantK k) (tp2 :: QuantK k) where
+class (IsExistsOr tp1 tp1, IsExistsOr tp2 tp2, IsExistsOrConstraint tp1 tp2) => IsExistsOr (tp1 :: QuantK k) (tp2 :: QuantK k) where
     isExistsOr :: ExistsOrCases tp1 tp2
-    
-type instance IsExistsOrConstraint (OneK x) tp = ((OneK x) ~ tp)
-type instance IsExistsOrConstraint (AllK :: QuantK k) tp = ((AllK :: QuantK k) ~ tp)
 
 instance IsExistsOr (OneK x) (OneK x) where
     isExistsOr = ExistsOrRefl
@@ -512,8 +528,6 @@ instance IsExistsOr AllK AllK where
 instance IsExistsOr ExistsK ExistsK where
     isExistsOr = ExistsOrRefl
 
-type instance IsExistsOrConstraint ExistsK x = ()
-
 instance IsExistsOr ExistsK (OneK k) where
     isExistsOr = ExistsOrExists
 
@@ -521,7 +535,7 @@ instance IsExistsOr ExistsK AllK where
     isExistsOr = ExistsOrExists
 
 data QuantAsAllProof (f :: k -> Type) (tp :: QuantK k) where
-    QuantAsAllProof :: (IsExistsOr tp AllK) => (forall x. ReprOf x -> f x) -> QuantAsAllProof f tp
+    QuantAsAllProof :: (IsExistsOr tp AllK, KnownRepr QuantRepr tp) => (forall x. ReprOf x -> f x) -> QuantAsAllProof f tp
 
 quantAsAll :: HasReprK k => Quant (f :: k -> Type) tp -> Maybe (QuantAsAllProof f tp)
 quantAsAll q = case q of
@@ -532,7 +546,7 @@ quantAsAll q = case q of
         Nothing -> Nothing
 
 -- | Pattern for creating or matching a universally quantified 'Quant', generalized over the existential cases
-pattern All :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall x. ReprOf x -> f x) -> Quant (f :: k -> Type) tp
+pattern All :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK, KnownRepr QuantRepr tp) => (forall x. ReprOf x -> f x) -> Quant (f :: k -> Type) tp
 pattern All f <- (quantAsAll -> Just (QuantAsAllProof f))
     where
         All f = case (isExistsOr :: ExistsOrCases tp AllK) of
@@ -540,7 +554,7 @@ pattern All f <- (quantAsAll -> Just (QuantAsAllProof f))
             ExistsOrRefl -> QuantAll (TMF.mapWithKey (\repr _ -> f repr) (allReprs @k))
 
 data QuantAsOneProof (f :: k -> Type) (tp :: QuantK k) where
-    QuantAsOneProof :: (IsExistsOr tp (OneK x), IfIsOneK tp (x ~ TheOneK tp)) => ReprOf x -> f x -> QuantAsOneProof f tp
+    QuantAsOneProof :: (IsExistsOr tp (OneK x), IfIsOneK tp (x ~ TheOneK tp), KnownRepr QuantRepr tp) => ReprOf x -> f x -> QuantAsOneProof f tp
 
 quantAsOne :: forall k f tp. HasReprK k => Quant (f :: k -> Type) (tp :: QuantK k) -> Maybe (QuantAsOneProof f tp)
 quantAsOne q = case q of
@@ -556,10 +570,10 @@ existsOrCases f g = case (isExistsOr :: ExistsOrCases tp tp') of
     ExistsOrRefl -> g
 
 -- | Pattern for creating or matching a singleton 'Quant', generalized over the existential cases
-pattern Single :: forall {k} f tp. (HasReprK k) => forall x. (IsExistsOr tp (OneK x), IfIsOneK tp (x ~ TheOneK tp)) => ReprOf x -> f x -> Quant (f :: k -> Type) tp
+pattern Single :: forall {k} f tp. (HasReprK k) => forall x. (IsExistsOr tp (OneK x), IfIsOneK tp (x ~ TheOneK tp), KnownRepr QuantRepr tp) => ReprOf x -> f x -> Quant (f :: k -> Type) tp
 pattern Single repr x <- (quantAsOne -> Just (QuantAsOneProof repr x))
     where
-        Single (repr :: ReprOf x) x = existsOrCases @tp @(OneK x) (QuantExists (Single repr x)) (QuantOne repr x)
+        Single (repr :: ReprOf x) x = existsOrCases @tp @(OneK x) (withRepr repr $ QuantExists (Single repr x)) (QuantOne repr x)
 
 
 {-# COMPLETE Single, All #-}
@@ -734,6 +748,8 @@ instance QuantCoercible f => QuantCoercible (Exists f) where
 
 instance QuantCoercible f => QuantConvertible (Exists f) where
   applyQuantConversion qc e = case (qc, e) of
+    (ConvertRefl{}, _) -> Just e
+    (ConvertNone{}, _) -> Nothing
     (ConvertExistsToAll, ExistsAllCtor x) -> Just $ TheAll x
     (ConvertExistsToOne repr, ExistsOneCtor repr' x) -> case testEquality repr repr' of
       Just Refl -> Just $ TheOne repr x
diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs
index 71fb0332..40b106b3 100644
--- a/src/Pate/Verification/PairGraph.hs
+++ b/src/Pate/Verification/PairGraph.hs
@@ -325,7 +325,7 @@ data PairGraph sym arch =
     -- | Mapping from singleton nodes to their "synchronization" point, representing
     --   the case where two independent program analysis steps have occurred and now
     --   their control-flows have re-synchronized
-  , pairGraphSyncData :: !(Map (GraphNode arch) (SyncData sym arch))
+  , pairGraphSyncData :: !(Map (GraphNode' arch Qu.AllK) (SyncData sym arch))
   , pairGraphPendingActs :: ActionQueue sym arch
   , pairGraphDomainRefinements ::
       !(Map (GraphNode arch) [DomainRefinement sym arch])
@@ -521,7 +521,7 @@ getSyncData ::
   (OrdF x, Ord (x bin)) =>
   L.Lens' (SyncData sym arch) (PPa.PatchPair (SetF x)) ->
   PBi.WhichBinaryRepr bin ->
-  GraphNode arch {- ^ The divergent node -}  ->
+  GraphNode' arch Qu.AllK {- ^ The divergent node -}  ->
   PairGraphM sym arch (Set (x bin))
 getSyncData lens bin nd = getPG $ syncDataSet nd bin lens
 
@@ -594,7 +594,7 @@ initFnBindings sym scope sne pg = do
 
 syncData ::
   forall sym arch.
-  GraphNode arch ->
+  GraphNode' arch Qu.AllK ->
   L.Lens' (PairGraph sym arch) (SyncData sym arch)
 syncData nd f pg = fmap set_ (f get_)
     where
@@ -609,7 +609,7 @@ syncData nd f pg = fmap set_ (f get_)
 syncDataSet ::
   forall k sym arch bin.
   (OrdF k, Ord (k bin)) =>
-  GraphNode arch ->
+  GraphNode' arch Qu.AllK ->
   PBi.WhichBinaryRepr bin ->
   L.Lens' (SyncData sym arch) (PPa.PatchPair (SetF k)) ->
   L.Lens' (PairGraph sym arch) (Set (k bin))
@@ -622,7 +622,7 @@ modifySyncData ::
   (OrdF x, Ord (x bin)) =>
   L.Lens' (SyncData sym arch) (PPa.PatchPair (SetF x)) ->
   PBi.WhichBinaryRepr bin ->
-  GraphNode arch -> 
+  GraphNode' arch Qu.AllK -> 
   (Set (x bin) -> Set (x bin)) ->
   PairGraphM sym arch ()
 modifySyncData lens bin dp f = setPG f $ syncDataSet dp bin lens
@@ -633,14 +633,14 @@ addToSyncData ::
   HasCallStack =>
   L.Lens' (SyncData sym arch) (PPa.PatchPair (SetF x)) ->
   PBi.WhichBinaryRepr bin ->
-  GraphNode arch {- ^ The divergent node -}  ->
+  GraphNode' arch Qu.AllK {- ^ The divergent node -}  ->
   x bin ->
   PairGraphM sym arch ()
 addToSyncData lens bin nd x = modifySyncData lens bin nd (Set.insert x)
 
 addSyncAddress ::
   forall sym arch bin.
-  GraphNode arch {- ^ The divergent node -}  ->
+  GraphNode' arch Qu.AllK {- ^ The divergent node -}  ->
   PBi.WhichBinaryRepr bin ->
   PAd.ConcreteAddress arch ->
   PairGraphM sym arch ()
@@ -648,7 +648,7 @@ addSyncAddress nd bin syncAddr = addToSyncData syncCutAddresses bin nd (PPa.With
 
 addDesyncExits ::
   forall sym arch.
-  GraphNode arch {- ^ The divergent node -}  ->
+  GraphNode' arch Qu.AllK {- ^ The divergent node -}  ->
   PPa.PatchPair (PB.BlockTarget arch) ->
   PairGraphM sym arch ()
 addDesyncExits dp blktPair = do
@@ -665,7 +665,7 @@ handleKnownDesync ::
   PPa.PatchPair (PB.BlockTarget arch) ->
   PairGraphM sym arch Bool
 handleKnownDesync priority ne blkt = fmap (fromMaybe False) $ tryPG $ do
-  let dp = GraphNode ne
+  dp <- toTwoSidedNode $ GraphNode ne
   desyncExitsO <- getSyncData syncDesyncExits PBi.OriginalRepr dp
   desyncExitsP <- getSyncData syncDesyncExits PBi.PatchedRepr dp
   case not (Set.null desyncExitsO) && not (Set.null desyncExitsP) of
@@ -678,7 +678,7 @@ handleKnownDesync priority ne blkt = fmap (fromMaybe False) $ tryPG $ do
 -- | Queue all the sync points to be processed (merged) for a given
 --   divergence
 getAllSyncPoints ::
-  GraphNode arch ->
+  GraphNode' arch Qu.AllK ->
   PairGraphM sym arch [PPa.PatchPair (SyncPoint arch)]
 getAllSyncPoints nd = do
   syncsO <- getSyncData syncPoints PBi.OriginalRepr nd
@@ -948,9 +948,9 @@ getReturnVectors gr fPair = fromMaybe mempty (Map.lookup fPair (pairGraphReturnV
 -- | Look up the current abstract domain for the given graph node.
 getCurrentDomain ::
   PairGraph sym arch ->
-  GraphNode arch ->
+  GraphNode' arch qbin ->
   Maybe (AbstractDomainSpec sym arch)
-getCurrentDomain pg nd = Map.lookup nd (pairGraphDomains pg)
+getCurrentDomain pg nd = withKnownBin nd $ Map.lookup (Qu.coerceToExists nd) (pairGraphDomains pg)
 
 getCurrentDomainM ::
   GraphNode arch ->
@@ -1044,8 +1044,8 @@ queueAncestors :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGr
 queueAncestors priority nd pg = 
   snd $ Set.foldr (queueNode' priority) (Set.singleton nd, pg) (getBackEdgesFrom pg nd)
 
-queueNode :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGraph sym arch
-queueNode priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__)
+queueNode :: NodePriority -> GraphNode' arch qbin -> PairGraph sym arch -> PairGraph sym arch
+queueNode priority nd__ pg__ = withKnownBin nd__ $ snd $ queueNode' priority (Qu.coerceToExists nd__) (Set.empty, pg__)
 
 -- | Calls 'queueNode' for 'ProcessNode' work items.
 --   For 'ProcessMerge' work items, queues up the merge if
@@ -1072,7 +1072,7 @@ queueWorkItem priority wi pg = case wi of
     Just{} -> addItemToWorkList wi priority pg
     Nothing -> queueNode priority (singleNodeDivergence sne) pg
 
-queueSplitAnalysis :: NodePriority -> NodeEntry arch -> PairGraphM sym arch ()
+queueSplitAnalysis :: NodePriority -> NodeEntry' arch qbin -> PairGraphM sym arch ()
 queueSplitAnalysis priority ne = do
   sneO <- toSingleNodeEntry PBi.OriginalRepr ne
   sneP <- toSingleNodeEntry PBi.PatchedRepr ne
@@ -1240,8 +1240,10 @@ hasWorkLeft pg = case RevMap.minView_value (pairGraphWorklist pg) of
   Just{} -> True
 
 isDivergeNode ::
-  GraphNode arch -> PairGraph sym arch -> Bool
-isDivergeNode nd pg = Map.member nd (pairGraphSyncData pg)
+  GraphNode' arch qbin -> PairGraph sym arch -> Bool
+isDivergeNode nd pg = withKnownBin nd $ case Qu.convertQuant nd of
+  Just nd' -> Map.member nd' (pairGraphSyncData pg)
+  Nothing -> False
 
 -- | Given a pair graph, chose the next node in the graph to visit
 --   from the work list, updating the necessary bookeeping.  If the
@@ -1387,7 +1389,7 @@ pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg
 
 -- | Compute a merged node for two diverging nodes
 -- FIXME: do we need to support mismatched node kinds here?
-combineNodes :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (GraphNode arch)
+combineNodes :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (GraphNode' arch Qu.AllK)
 combineNodes node1 node2 = do
   let ndPair = PPa.mkPair (singleEntryBin node1) (Qu.AsSingle node1) (Qu.AsSingle node2)
   Qu.AsSingle nodeO <- PPa.get PBi.OriginalRepr ndPair
@@ -1581,11 +1583,11 @@ isSyncExit sne blkt@(PB.BlockTarget{}) = do
     True -> return Nothing
     False -> isCutAddressFor (GraphNode sne) (PB.targetRawPC blkt) >>= \case
       True -> do
-        let sne_tgt = mkSingleNodeEntry (singleToNodeEntry sne) (PB.targetCall blkt)
+        let sne_tgt = mkSingleNodeEntry sne (PB.targetCall blkt)
         return $ Just $ SyncAtExit sne sne_tgt
       False -> case PB.targetReturn blkt of
         Just ret -> do
-          let sne_tgt = mkSingleNodeEntry (singleToNodeEntry sne) ret
+          let sne_tgt = mkSingleNodeEntry sne ret
           let sync = SyncAtExit sne sne_tgt
           -- special case where this block target
           -- has already been marked as a sync exit for this node, but
@@ -1672,7 +1674,7 @@ addReturnPointSync priority ne blktPair = case asSingleNodeEntry ne of
         case (not isExcept) &&
           Set.member (PPa.WithBin (singleEntryBin sne) (PB.concreteAddress ret)) cuts of
             True -> do
-              let syncExit = mkSingleNodeEntry (singleToNodeEntry sne) ret
+              let syncExit = mkSingleNodeEntry sne ret
               queueExitMerges priority (SyncAtExit sne syncExit)
             False -> return ()
       Nothing -> return ()
diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs
index 34812875..ede18e6d 100644
--- a/src/Pate/Verification/PairGraph/Node.hs
+++ b/src/Pate/Verification/PairGraph/Node.hs
@@ -45,7 +45,6 @@ module Pate.Verification.PairGraph.Node (
   , returnToEntry
   , functionEntryOf
   , returnOfEntry
-  , toSingleReturn
   , toSingleNode
   , toSingleGraphNode
   , isSingleNode
@@ -71,6 +70,9 @@ module Pate.Verification.PairGraph.Node (
   , singleNodeRepr
   , singleNodeDivergePoint
   , singleNodeDivergence
+  , withKnownBin
+  , toTwoSidedNode
+  , asSingleNode
   ) where
 
 import           Prettyprinter ( Pretty(..), sep, (<+>), Doc )
@@ -93,6 +95,7 @@ import Data.Parameterized.Classes
 import Pate.Panic
 import qualified Pate.Address as PAd
 import Data.Kind (Type)
+import Data.Parameterized.WithRepr
 
 -- | Nodes in the program graph consist either of a pair of
 --   program points (GraphNode), or a synthetic node representing
@@ -118,10 +121,29 @@ instance TestEquality (GraphNode' arch) where
 instance OrdF (GraphNode' arch) where
   compareF nd1 nd2 = lexCompareF (nodeRepr nd1) (nodeRepr nd2) $ fromOrdering $ compare nd1 nd2
 
+coerceContext :: Qu.QuantCoercion t1 t2 -> GraphNode' arch t1 -> CallingContext' arch t1 -> CallingContext' arch t2
+coerceContext qc nd x@(CallingContext' cctx dp) = case qc of
+  Qu.CoerceAllToOne repr -> CallingContext' cctx (DivergePointSingle repr nd)
+  Qu.CoerceToExists _ -> CallingContext' cctx (divergePointExists dp)
+  Qu.CoerceRefl{} -> x
+
 instance Qu.QuantCoercible (GraphNode' arch) where
-  coerceQuant = \case
-    GraphNode ne -> GraphNode (Qu.coerceQuant ne)
-    ReturnNode nr -> ReturnNode (Qu.coerceQuant nr)
+  applyQuantCoercion qc nd = case nd of
+    GraphNode (NodeEntry cctx blks) -> GraphNode (NodeEntry (coerceContext qc nd cctx) (Qu.applyQuantCoercion qc blks))
+    ReturnNode (NodeReturn cctx fns) -> ReturnNode (NodeReturn (coerceContext qc nd cctx) (Qu.applyQuantCoercion qc fns))
+
+instance Qu.QuantConvertible (CallingContext' arch) where
+  applyQuantConversion qc (CallingContext' cctx dp) = CallingContext' <$> pure cctx <*> Qu.applyQuantConversion qc dp
+
+instance Qu.QuantConvertible (GraphNode' arch) where
+  convertQuant = \case
+    GraphNode (NodeEntry cctx blks) -> (\cctx' blks' -> GraphNode (NodeEntry cctx' blks')) <$> Qu.convertQuant cctx <*> Qu.convertQuant blks
+    ReturnNode (NodeReturn cctx fns) -> (\cctx' fns' -> ReturnNode (NodeReturn cctx' fns')) <$> Qu.convertQuant cctx <*> Qu.convertQuant fns
+
+withKnownBin :: GraphNode' arch qbin -> ((KnownRepr Qu.QuantRepr qbin, Qu.IsExistsOr qbin qbin) => a) -> a
+withKnownBin nd f = case graphNodeBlocks nd of
+  Qu.All{} -> f
+  Qu.Single{} -> f
 
 instance PA.ValidArch arch => JSON.ToJSON (GraphNode' arch bin) where
   toJSON = \case
@@ -135,13 +157,13 @@ instance PA.ValidArch arch => W4S.W4Serializable sym (NodeEntry' arch bin) where
   w4Serialize r = return $ JSON.toJSON r
 
 data NodeContent arch (f :: PB.WhichBinary -> Type) (qbin :: QuantK PB.WhichBinary) = 
-  NodeContent { nodeContentCtx :: CallingContext arch, nodeContent :: Quant f qbin }
+  NodeContent { nodeContentCtx :: CallingContext' arch qbin, nodeContent :: Quant f qbin }
 
 deriving instance (forall x. Eq (f x)) => Eq (NodeContent arch f qbin)
 deriving instance (forall x. Ord (f x)) => Ord (NodeContent arch f qbin)
 
 instance (forall x. Eq (f x)) => TestEquality (NodeContent arch f) where
-  testEquality (NodeContent cctx1 x1) (NodeContent cctx2 x2) | cctx1 == cctx2, Just Refl <- testEquality x1 x2 = Just Refl
+  testEquality (NodeContent cctx1 x1) (NodeContent cctx2 x2) | Just Refl <- testEquality x1 x2, cctx1 == cctx2 = Just Refl
   testEquality _ _ = Nothing
 
 instance (forall x. Ord (f x)) => OrdF (NodeContent arch f) where
@@ -150,10 +172,7 @@ instance (forall x. Ord (f x)) => OrdF (NodeContent arch f) where
 type NodeEntry' arch = NodeContent arch (PB.ConcreteBlock arch)
 type NodeEntry arch = NodeEntry' arch ExistsK
 
-instance Qu.QuantCoercible (NodeEntry' arch) where
-  coerceQuant (NodeEntry cctx blks) = NodeEntry cctx (Qu.coerceQuant blks)
-
-pattern NodeEntry :: CallingContext arch -> Quant (PB.ConcreteBlock arch) bin -> NodeEntry' arch bin
+pattern NodeEntry :: CallingContext' arch bin -> Quant (PB.ConcreteBlock arch) bin -> NodeEntry' arch bin
 pattern NodeEntry ctx bp = NodeContent ctx bp
 {-# COMPLETE NodeEntry #-}
 
@@ -163,7 +182,7 @@ nodeEntryRepr ne = Qu.quantToRepr $ nodeBlocks ne
 nodeBlocks :: NodeEntry' arch bin -> Quant (PB.ConcreteBlock arch) bin
 nodeBlocks = nodeContent
 
-graphNodeContext :: NodeEntry' arch bin -> CallingContext arch
+graphNodeContext :: NodeEntry' arch bin -> CallingContext' arch bin
 graphNodeContext = nodeContentCtx
 
 type NodeReturn' arch = NodeContent arch (PB.FunctionEntry arch)
@@ -179,21 +198,18 @@ nodeRepr :: GraphNode' arch qbin -> Qu.QuantRepr qbin
 nodeRepr (GraphNode ne) = nodeEntryRepr ne
 nodeRepr (ReturnNode rn) = nodeReturnRepr rn
 
-returnNodeContext :: NodeReturn' arch bin -> CallingContext arch
+returnNodeContext :: NodeReturn' arch bin -> CallingContext' arch bin
 returnNodeContext = nodeContentCtx
 
-pattern NodeReturn :: CallingContext arch -> Quant (PB.FunctionEntry arch) bin -> NodeReturn' arch bin
+pattern NodeReturn :: CallingContext' arch bin -> Quant (PB.FunctionEntry arch) bin -> NodeReturn' arch bin
 pattern NodeReturn ctx bp = NodeContent ctx bp
 {-# COMPLETE NodeReturn #-}
 
-instance Qu.QuantCoercible (NodeReturn' arch) where
-  coerceQuant (NodeReturn cctx fns) = NodeReturn cctx (Qu.coerceQuant fns)
-
 graphNodeBlocks :: GraphNode' arch bin -> Quant (PB.ConcreteBlock arch) bin
 graphNodeBlocks (GraphNode ne) = nodeBlocks ne
 graphNodeBlocks (ReturnNode ret) = Qu.map PB.functionEntryToConcreteBlock (nodeFuns ret)
 
-nodeContext :: GraphNode' arch qbin  -> CallingContext arch
+nodeContext :: GraphNode' arch qbin  -> CallingContext' arch qbin
 nodeContext (GraphNode nd) = nodeContentCtx nd
 nodeContext (ReturnNode ret) = nodeContentCtx ret
 
@@ -205,35 +221,126 @@ pattern GraphNodeReturn blks <- (ReturnNode (NodeContent _ blks))
 
 {-# COMPLETE GraphNodeEntry, GraphNodeReturn #-}
 
+data DivergePoint arch (tp :: Qu.QuantK PB.WhichBinary) where
+  DivergePointSingle :: PB.WhichBinaryRepr bin -> GraphNode' arch Qu.AllK -> DivergePoint arch (Qu.OneK bin)
+  DivergePointTwoSided ::  GraphNode' arch Qu.AllK -> DivergePoint arch Qu.AllK
+  NoDivergePointCtor :: DivergePoint arch Qu.AllK
+  SomeDivergePoint :: Maybe (GraphNode' arch Qu.AllK) -> DivergePoint arch Qu.ExistsK
+
+divergePointExists :: DivergePoint arch tp -> DivergePoint arch Qu.ExistsK
+divergePointExists = \case
+  DivergePointSingle _ nd -> SomeDivergePoint (Just nd)
+  DivergePointTwoSided nd -> SomeDivergePoint (Just nd)
+  NoDivergePointCtor -> SomeDivergePoint Nothing
+  x@SomeDivergePoint{} -> x
+
+instance Qu.QuantConvertible (DivergePoint arch) where
+  applyQuantConversion qc dp = case (qc, dp) of
+    (Qu.ConvertExistsToAll, SomeDivergePoint (Just nd)) -> Just $ (DivergePointTwoSided nd)
+    (Qu.ConvertExistsToAll, SomeDivergePoint Nothing) -> Just $ NoDivergePointCtor
+    (Qu.ConvertExistsToOne repr, SomeDivergePoint (Just nd)) -> Just $ (DivergePointSingle repr nd)
+    (Qu.ConvertExistsToOne{}, SomeDivergePoint Nothing) -> Nothing
+    (Qu.ConvertRefl _, _) -> Just dp
+    (Qu.ConvertNone{},_) -> Nothing
+
+
+deriving instance Eq (DivergePoint arch tp)
+deriving instance Ord (DivergePoint arch tp)
+
+data DivergePointProof arch tp where
+  DivergePointProof :: (KnownRepr Qu.QuantRepr tp, Qu.IsExistsOr tp tp) => GraphNode' arch Qu.AllK -> DivergePointProof arch tp
+
+divergePointProof :: DivergePoint arch tp -> Maybe (DivergePointProof arch tp)
+divergePointProof = \case
+  DivergePointSingle repr nd -> withRepr repr $ Just $ DivergePointProof nd
+  DivergePointTwoSided nd -> Just $ DivergePointProof nd
+  NoDivergePointCtor -> Nothing
+  SomeDivergePoint (Just nd) -> Just $ DivergePointProof nd
+  SomeDivergePoint Nothing -> Nothing
+
+pattern DivergePoint :: forall arch tp. () => (KnownRepr Qu.QuantRepr tp, Qu.IsExistsOr tp tp) => GraphNode' arch Qu.AllK -> DivergePoint arch tp
+pattern DivergePoint nd <- (divergePointProof -> Just (DivergePointProof nd)) where
+  DivergePoint nd = case knownRepr :: Qu.QuantRepr tp of
+    Qu.QuantOneRepr repr -> DivergePointSingle repr nd
+    Qu.QuantAllRepr -> DivergePointTwoSided nd
+    Qu.QuantSomeRepr -> SomeDivergePoint (Just (Qu.coerceQuant nd))
+
+data NoDivergePointProof arch tp where
+  NoDivergePointProof :: (Qu.IsExistsOr tp Qu.AllK, KnownRepr Qu.QuantRepr tp) => NoDivergePointProof arch tp
+
+noDivergePointProof :: DivergePoint arch tp -> Maybe (NoDivergePointProof arch tp)
+noDivergePointProof = \case
+  NoDivergePointCtor -> Just NoDivergePointProof
+  SomeDivergePoint Nothing -> Just NoDivergePointProof
+  _ -> Nothing
+
+pattern NoDivergePoint :: forall arch tp. () => (KnownRepr Qu.QuantRepr tp, Qu.IsExistsOr tp Qu.AllK) => DivergePoint arch tp
+pattern NoDivergePoint <- (noDivergePointProof -> Just NoDivergePointProof) where
+  NoDivergePoint = case knownRepr :: Qu.QuantRepr tp of
+    Qu.QuantAllRepr -> NoDivergePointCtor
+    Qu.QuantSomeRepr -> SomeDivergePoint Nothing
+
+{-# COMPLETE NoDivergePoint, DivergePoint #-}
+
+divergePointNode :: DivergePoint arch tp -> Maybe (GraphNode' arch Qu.AllK)
+divergePointNode = \case
+  DivergePoint nd -> Just nd
+  NoDivergePoint -> Nothing
+
+divergePoint :: CallingContext' arch tp -> Maybe (GraphNode' arch Qu.AllK)
+divergePoint cctx = divergePointNode $ divergePoint' cctx
+
+
 -- | Additional context used to distinguish function calls
 --   "Freezing" one binary in a node indicates that it should not continue
 --   execution until the other binary has returned
-data CallingContext arch = CallingContext { _ctxAncestors :: [PB.BlockPair arch], divergePoint :: Maybe (GraphNode arch) }
+data CallingContext' arch (tp :: Qu.QuantK PB.WhichBinary) = CallingContext' { ctxAncestors :: [PB.BlockPair arch], divergePoint' :: DivergePoint arch tp }
   deriving (Eq, Ord)
 
+type CallingContext arch = CallingContext' arch Qu.ExistsK
 
-instance PA.ValidArch arch => Pretty (CallingContext arch) where
+data CallingContextProof arch tp where
+  CallingContextProof :: (Qu.IsExistsOr tp2 tp1, KnownRepr Qu.QuantRepr tp1, KnownRepr Qu.QuantRepr tp2) => [PB.BlockPair arch] -> DivergePoint arch tp1 -> CallingContextProof arch tp2
+
+callingContextProof :: CallingContext' arch tp -> CallingContextProof arch tp
+callingContextProof cctx = let dp = divergePoint' cctx in case dp of
+  DivergePoint{} -> CallingContextProof (ctxAncestors cctx) dp
+  NoDivergePoint -> CallingContextProof (ctxAncestors cctx) dp
+
+pattern CallingContext :: forall arch tp2. () => forall tp1. (Qu.IsExistsOr tp2 tp1, KnownRepr Qu.QuantRepr tp2, KnownRepr Qu.QuantRepr tp1) => [PB.BlockPair arch] -> DivergePoint arch tp1 -> CallingContext' arch tp2
+pattern CallingContext blks dp <- (callingContextProof -> CallingContextProof blks dp) where
+  CallingContext blks (dp :: DivergePoint arch tp1) = case Qu.isExistsOr @_ @tp2 @tp1 of
+    Qu.ExistsOrExists -> case dp of
+      DivergePoint nd -> CallingContext' blks (SomeDivergePoint (Just (Qu.coerceQuant nd)))
+      NoDivergePoint -> CallingContext' blks (SomeDivergePoint Nothing)
+    Qu.ExistsOrRefl -> CallingContext' blks dp
+
+
+{-# COMPLETE CallingContext #-}
+
+instance PA.ValidArch arch => Pretty (CallingContext' arch qbin) where
   pretty (CallingContext bps mdivisionPoint) =
     let
       bs = [ pretty bp | bp <- bps ]
       divP = case mdivisionPoint of
-        Just _p -> [] -- ["Diverged at:", pretty p] -- too noisy
-        Nothing -> []
+        DivergePoint _p -> [] -- ["Diverged at:", pretty p] -- too noisy
+        NoDivergePoint -> []
     in sep (((zipWith (<+>) ( "via:" : repeat "<-") bs)) ++ divP)
 
-instance PA.ValidArch arch => JSON.ToJSON (CallingContext arch) where
-  toJSON (CallingContext bps mdivisionPoint) = JSON.object [ "ancestors" JSON..= bps, "divergedAt" JSON..= mdivisionPoint]
+instance PA.ValidArch arch => JSON.ToJSON (CallingContext' arch qbin) where
+  toJSON (CallingContext bps mdivisionPoint) = JSON.object [ "ancestors" JSON..= bps, "divergedAt" JSON..= divergePointNode mdivisionPoint]
 
 getDivergePoint :: GraphNode arch -> Maybe (GraphNode arch)
-getDivergePoint nd = case nd of
-  GraphNode (NodeEntry ctx _) -> divergePoint ctx
-  ReturnNode (NodeReturn ctx _) -> divergePoint ctx
+getDivergePoint nd = case nodeContext nd of
+  CallingContext _ (DivergePoint dp) -> Just (Qu.coerceQuant dp)
+  CallingContext _ NoDivergePoint -> Nothing
+
 
-rootEntry :: PB.BinaryPair (PB.ConcreteBlock arch) qbin -> NodeEntry' arch qbin
-rootEntry pPair = NodeEntry (CallingContext [] Nothing) pPair
+rootEntry :: PPa.PatchPair (PB.ConcreteBlock arch) -> NodeEntry arch
+rootEntry pPair = NodeEntry (CallingContext [] (SomeDivergePoint Nothing)) pPair
 
-rootReturn :: PB.BinaryPair (PB.FunctionEntry arch) qbin -> NodeReturn' arch qbin
-rootReturn pPair = NodeReturn (CallingContext [] Nothing) pPair
+rootReturn :: PPa.PatchPair (PB.FunctionEntry arch) -> NodeReturn arch
+rootReturn pPair = NodeReturn (CallingContext [] (SomeDivergePoint Nothing)) pPair
 
 addContext :: PB.BinaryPair (PB.ConcreteBlock arch) qbin1 -> NodeEntry' arch qbin2 -> NodeEntry' arch qbin2
 addContext newCtx' ne@(NodeEntry (CallingContext ctx d) blks) = 
@@ -247,13 +354,13 @@ addContext newCtx' ne@(NodeEntry (CallingContext ctx d) blks) =
 -- Strip diverge points from two-sided nodes. This is used so that
 -- merged nodes (which are two-sided) can meaningfully retain their
 -- diverge point, but it will be stripped on any subsequent nodes.
-mkNextContext :: Quant a (bin :: QuantK PB.WhichBinary) -> CallingContext arch -> CallingContext arch
+mkNextContext :: Quant a (bin :: QuantK PB.WhichBinary) -> CallingContext' arch bin -> CallingContext' arch bin
 mkNextContext q cctx = case q of
   Qu.All{} -> dropDivergePoint cctx
   Qu.Single{} -> cctx
-
-dropDivergePoint :: CallingContext arch -> CallingContext arch
-dropDivergePoint  (CallingContext cctx _) = CallingContext cctx Nothing
+ 
+dropDivergePoint :: Qu.IsExistsOr qbin Qu.AllK => CallingContext' arch qbin -> CallingContext' arch qbin
+dropDivergePoint  (CallingContext cctx _) = CallingContext cctx NoDivergePointCtor
 
 mkNodeEntry :: NodeEntry arch -> PB.BlockPair arch -> NodeEntry arch
 mkNodeEntry node pPair = NodeEntry (mkNextContext pPair (graphNodeContext node)) pPair
@@ -266,41 +373,38 @@ mkNodeReturn :: NodeEntry arch -> PB.FunPair arch -> NodeReturn arch
 mkNodeReturn node fPair = NodeReturn (mkNextContext fPair (graphNodeContext node)) fPair
 
 mkMergedNodeEntry :: 
-  GraphNode arch -> 
+  GraphNode' arch Qu.AllK -> 
   PB.ConcreteBlock arch PB.Original ->
   PB.ConcreteBlock arch PB.Patched -> 
-  NodeEntry arch
-mkMergedNodeEntry nd blkO blkP = NodeEntry (CallingContext cctx (Just nd)) (PPa.PatchPair blkO blkP)
+  NodeEntry' arch Qu.AllK
+mkMergedNodeEntry nd blkO blkP = NodeEntry (CallingContext cctx (DivergePoint nd)) (Qu.All $ \case PB.OriginalRepr -> blkO; PB.PatchedRepr -> blkP)
   where
     CallingContext cctx _ = nodeContext nd
 
 mkMergedNodeReturn :: 
-  GraphNode arch -> 
+  GraphNode' arch Qu.AllK -> 
   PB.FunctionEntry arch PB.Original ->
   PB.FunctionEntry arch PB.Patched -> 
-  NodeReturn arch
-mkMergedNodeReturn nd fnO fnP = NodeReturn (CallingContext cctx (Just nd)) (PPa.PatchPair fnO fnP)
+  NodeReturn' arch Qu.AllK
+mkMergedNodeReturn nd fnO fnP = NodeReturn (CallingContext cctx (DivergePoint nd)) (Qu.All $ \case PB.OriginalRepr -> fnO; PB.PatchedRepr -> fnP)
   where
     CallingContext cctx _ = nodeContext nd
 
-
--- | Project the given 'NodeReturn' into a singleton node for the given binary
-toSingleReturn :: PPa.PatchPairM m => PB.WhichBinaryRepr bin -> GraphNode arch -> NodeReturn arch -> m (NodeReturn arch)
-toSingleReturn bin divergedAt (NodeReturn ctx fPair) = do
-  fPair' <- PPa.toSingleton bin fPair
-  return $ NodeReturn (ctx {divergePoint = Just divergedAt}) fPair'
-
 -- | Project the given 'NodeEntry' into a singleton node for the given binary
-toSingleNode:: PPa.PatchPairM m => PB.WhichBinaryRepr bin -> NodeEntry arch -> m (NodeEntry arch)
-toSingleNode bin node@(NodeEntry ctx bPair) = do
-  fPair' <- PPa.toSingleton bin bPair
-  return $ NodeEntry (ctx {divergePoint = Just (GraphNode node)}) fPair'
+toSingleNode:: forall m arch bin qbin. PPa.PatchPairM m => PB.WhichBinaryRepr bin -> NodeEntry' arch qbin -> m (NodeEntry arch)
+toSingleNode bin divergedAt = toSingleGraphNode bin (GraphNode divergedAt) >>= \case
+  GraphNode nd -> return nd
+  _ -> PPa.throwPairErr
+
+toSingleGraphNode :: forall m arch bin qbin. PPa.PatchPairM m => PB.WhichBinaryRepr bin -> GraphNode' arch qbin -> m (GraphNode arch)
+toSingleGraphNode bin node = withKnownBin node $ withRepr bin $ case Qu.convertQuant node of
+  Just (nd :: GraphNode' arch Qu.AllK) | (sgn :: SingleGraphNode arch bin) <- Qu.coerceQuant nd -> return $ Qu.coerceToExists sgn
+  Nothing -> case Qu.convertQuant node of
+    Just (nd :: SingleGraphNode arch bin) -> return $ Qu.coerceToExists nd
+    Nothing -> PPa.throwPairErr
 
-toSingleGraphNode :: PPa.PatchPairM m => PB.WhichBinaryRepr bin -> GraphNode arch -> m (GraphNode arch)
-toSingleGraphNode bin node = case node of
-  GraphNode ne -> GraphNode <$> toSingleNode bin ne
-  ReturnNode nr -> ReturnNode <$> toSingleReturn bin node nr  
 
+  
 isSingleNodeEntry :: 
   PPa.PatchPairM m => 
   NodeEntry arch -> 
@@ -332,11 +436,11 @@ eqUptoDivergePoint ::
   GraphNode arch ->
   Bool
 eqUptoDivergePoint (GraphNode (NodeEntry ctx1 blks1)) (GraphNode (NodeEntry ctx2 blks2))
-  | (ctx1{divergePoint = Nothing} == ctx2{divergePoint = Nothing})
+  | (ctxAncestors ctx1 == ctxAncestors ctx2)
   , blks1 == blks2
   = True
 eqUptoDivergePoint (ReturnNode (NodeReturn ctx1 blks1)) (ReturnNode (NodeReturn ctx2 blks2))
-  | (ctx1{divergePoint = Nothing} == ctx2{divergePoint = Nothing})
+  | (ctxAncestors ctx1 == ctxAncestors ctx2)
   , blks1 == blks2
   = True
 eqUptoDivergePoint _ _ = False
@@ -350,6 +454,11 @@ splitGraphNode nd = do
   nodeP <- PPa.getC PB.PatchedRepr nodes
   return (nodeO, nodeP)
 
+toTwoSidedNode :: PPa.PatchPairM m => GraphNode' arch qbin -> m (GraphNode' arch Qu.AllK)
+toTwoSidedNode nd = withKnownBin nd $ case Qu.convertQuant nd of
+  Just (nd' :: GraphNode' arch Qu.AllK) -> return nd'
+  Nothing -> PPa.throwPairErr
+
 -- | Get the node corresponding to the entry point for the function
 returnToEntry :: NodeReturn' arch bin -> NodeEntry' arch bin
 returnToEntry (NodeReturn ctx fns) = NodeEntry (mkNextContext fns ctx) (Qu.map PB.functionEntryToConcreteBlock fns)
@@ -393,7 +502,7 @@ instance PA.ValidArch arch => Show (GraphNode' arch qbin) where
   show e = show (pretty e)
 
 tracePrettyNode ::
-  PA.ValidArch arch => GraphNode arch -> String -> Doc a
+  PA.ValidArch arch => GraphNode' arch qbin -> String -> Doc a
 tracePrettyNode nd msg = case nd of
   GraphNode e -> case (functionEntryOf e == e,msg) of
     (True,"") -> "Function Entry" <+> pretty e
@@ -425,9 +534,6 @@ instance PA.ValidArch arch => JSON.ToJSON (NodeReturn' arch bin) where
   -- HMS.fromList [ ("data", JSON.Object content) ]
 
 
-
-
-
 instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "node" where
   type TraceNodeType '(sym, arch) "node" = GraphNode arch
   type TraceNodeLabel "node" = String
@@ -452,10 +558,10 @@ instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "entryno
 
 type SingleNodeEntry arch bin = NodeEntry' arch (Qu.OneK bin)
 
-pattern SingleNodeEntry :: CallingContext arch -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin
+pattern SingleNodeEntry :: CallingContext' arch (Qu.OneK bin) -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin
 pattern SingleNodeEntry cctx blk <- ((\l -> case l of NodeEntry cctx (Qu.Single _ blk) -> (cctx,blk)) -> (cctx,blk))
   where
-    SingleNodeEntry cctx blk = NodeEntry cctx (Qu.Single (PB.blockBinRepr blk) blk)
+    SingleNodeEntry cctx blk = NodeEntry cctx (withRepr (PB.blockBinRepr blk) $ Qu.Single (PB.blockBinRepr blk) blk)
 
 {-# COMPLETE SingleNodeEntry #-}
 
@@ -465,27 +571,30 @@ singleEntryBin (nodeEntryRepr -> Qu.QuantOneRepr repr) = repr
 singleNodeAddr :: SingleNodeEntry arch bin -> PPa.WithBin (PAd.ConcreteAddress arch) bin
 singleNodeAddr se = PPa.WithBin (singleEntryBin se) (PB.concreteAddress (singleNodeBlock se))
 
-mkSingleNodeEntry :: NodeEntry' arch qbin -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin
+mkSingleNodeEntry :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin
 mkSingleNodeEntry node blk = SingleNodeEntry (graphNodeContext node) blk
 
 
-singleNodeDivergePoint :: SingleGraphNode arch bin -> GraphNode arch
-singleNodeDivergePoint sgn = case divergePoint (nodeContext sgn) of
-  Just dp -> dp
-  Nothing -> panic Verifier "singleNodeDivergePoint" ["missing diverge point for SingleNodeEntry"]
-
+singleNodeDivergePoint :: SingleGraphNode arch bin -> GraphNode' arch Qu.AllK
+singleNodeDivergePoint sgn = case divergePoint' (nodeContext sgn) of
+  DivergePoint nd -> nd
 
-singleNodeDivergence :: SingleNodeEntry arch bin -> GraphNode arch
+singleNodeDivergence :: SingleNodeEntry arch bin -> GraphNode' arch Qu.AllK
 singleNodeDivergence sne = singleNodeDivergePoint (GraphNode sne)
 
 
 asSingleNodeEntry :: PPa.PatchPairM m => NodeEntry' arch qbin -> m (Some (Qu.AsSingle (NodeEntry' arch)))
-asSingleNodeEntry (NodeEntry cctx blks) = do
-  Pair _ blk <- PPa.asSingleton blks
-  case divergePoint cctx of
-    Just{} -> return $ Some (Qu.AsSingle $ SingleNodeEntry cctx blk)
+asSingleNodeEntry nd = asSingleNode (GraphNode nd) >>= \case
+  Some (Qu.AsSingle (GraphNode nd')) -> return $ Some (Qu.AsSingle nd')
+  _ -> PPa.throwPairErr
+
+asSingleNode:: PPa.PatchPairM m => GraphNode' arch qbin -> m (Some (Qu.AsSingle (GraphNode' arch)))
+asSingleNode nd = case graphNodeBlocks nd of
+  Qu.All{} -> PPa.throwPairErr
+  Qu.Single (repr :: PB.WhichBinaryRepr bin) _ -> withRepr repr $ case Qu.convertQuant nd of
+    Just (nd' :: GraphNode' arch (Qu.OneK bin)) -> return $ Some (Qu.AsSingle nd')
     Nothing -> PPa.throwPairErr
-
+  
 singleNodeBlock :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin
 singleNodeBlock (SingleNodeEntry _ blk) = blk
 
@@ -496,30 +605,34 @@ singleNodeBlock (SingleNodeEntry _ blk) = blk
 toSingleNodeEntry :: 
   PPa.PatchPairM m => 
   PB.WhichBinaryRepr bin -> 
-  NodeEntry arch -> 
+  NodeEntry' arch qbin -> 
   m (SingleNodeEntry arch bin)
 toSingleNodeEntry bin ne = do
   case toSingleNode bin ne of
-    Just (NodeEntry cctx bPair) -> do
-      blk <- PPa.get bin bPair
-      return $ SingleNodeEntry cctx blk
+    Just ne' -> do
+      Some (Qu.AsSingle sne) <- asSingleNodeEntry ne'
+      case testEquality (nodeEntryRepr sne) (Qu.QuantOneRepr bin) of
+        Just Refl -> return sne
+        Nothing -> PPa.throwPairErr
     _ -> PPa.throwPairErr
 
 singleToNodeEntry :: SingleNodeEntry arch bin -> NodeEntry arch
-singleToNodeEntry sne = Qu.coerceQuant sne
+singleToNodeEntry sne = case singleToGraphNode (GraphNode sne) of
+  GraphNode sne' -> sne'
+  ReturnNode _ -> error "singleToNodeEntry: unexpected node kind swap" 
 
 singleToGraphNode :: SingleGraphNode arch bin -> GraphNode arch
-singleToGraphNode sgn = Qu.coerceQuant sgn
+singleToGraphNode sgn = withRepr (singleNodeRepr sgn) $ Qu.coerceQuant sgn
 
 combineSingleEntries' :: 
   SingleNodeEntry arch PB.Original -> 
   SingleNodeEntry arch PB.Patched ->
   Maybe (NodeEntry arch)
 combineSingleEntries' (SingleNodeEntry cctxO blksO) (SingleNodeEntry cctxP blksP) = do
-  GraphNode divergeO <- divergePoint $ cctxO
-  GraphNode divergeP <- divergePoint $ cctxP
+  divergeO <- divergePoint $ cctxO
+  divergeP <- divergePoint $ cctxP
   guard $ divergeO == divergeP
-  return $ mkNodeEntry divergeO (PPa.PatchPair blksO blksP)
+  return $ mkNodeEntry' (Qu.coerceQuant divergeO) (PPa.PatchPair blksO blksP)
 
 -- | Create a combined two-sided 'NodeEntry' based on
 --   a pair of single-sided entries. The given entries
@@ -537,10 +650,10 @@ combineSingleEntries sne1 sne2 = case singleEntryBin sne1 of
 
 type SingleNodeReturn arch bin = NodeReturn' arch (Qu.OneK bin)
 
-pattern SingleNodeReturn :: CallingContext arch -> PB.FunctionEntry arch bin -> SingleNodeReturn arch bin
+pattern SingleNodeReturn :: CallingContext' arch (Qu.OneK bin) -> PB.FunctionEntry arch bin -> SingleNodeReturn arch bin
 pattern SingleNodeReturn cctx fn <- ((\l -> case l of NodeReturn cctx (Qu.Single _ fn) -> (cctx,fn)) -> (cctx,fn))
   where
-    SingleNodeReturn cctx fn = NodeReturn cctx (Qu.Single (PB.functionBinRepr fn) fn)
+    SingleNodeReturn cctx fn = NodeReturn cctx (withRepr (PB.functionBinRepr fn) $ Qu.Single (PB.functionBinRepr fn) fn)
 
 type SingleGraphNode arch bin = GraphNode' arch (Qu.OneK bin)
 
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index b1419958..ce36929d 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -404,10 +404,11 @@ addIntraBlockCut segOff blk = fnTrace "addIntraBlockCut" $ do
     _ -> throwHere $ PEE.MissingBlockAtAddress segOff (map MD.pblockAddr pblks) repr blk
 
 chooseDesyncPoint ::
-  GraphNode arch ->
+  GraphNode' arch Qu.AllK ->
   PairGraph sym arch ->
   EquivM sym arch (PairGraph sym arch)
-chooseDesyncPoint nd pg0 = do
+chooseDesyncPoint dp pg0 = do
+  let nd = Qu.coerceToExists dp
   divergePair@(PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do
     blk <- PPa.get bin (graphNodeBlocks nd)
     pblks <- PD.lookupBlocks blk
@@ -425,10 +426,11 @@ chooseDesyncPoint nd pg0 = do
 -- | Given a source divergent node, pick a synchronization point where
 --   control flow should again match between the two binaries
 chooseSyncPoint :: 
-  GraphNode arch -> 
+  GraphNode' arch Qu.AllK -> 
   PairGraph sym arch -> 
   EquivM sym arch (PairGraph sym arch)
-chooseSyncPoint nd pg0 = do
+chooseSyncPoint dp pg0 = do
+  let nd = Qu.coerceToExists dp
   (PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do
     blk <- PPa.get bin (graphNodeBlocks nd)
     pblks <- PD.lookupBlocks blk
@@ -436,7 +438,7 @@ chooseSyncPoint nd pg0 = do
     return $ (divergeSingle, Some blk, pblks)
   cuts <- pickCutPoints True syncMsg [divergeO, divergeP]
   execPG pg0 $ forM_ cuts $ \(Some (PPa.WithBin bin addr)) -> do
-    addSyncAddress nd bin addr
+    addSyncAddress dp bin addr
   where
     syncMsg = "Choose a synchronization point:"
 
@@ -583,10 +585,11 @@ initSingleSidedDomain ::
   SingleNodeEntry arch bin ->
   PairGraph sym arch ->
   EquivM sym arch (PairGraph sym arch)
-initSingleSidedDomain sne pg0 = withRepr bin $ withSym $ \sym -> withPG_ pg0 $ do
+initSingleSidedDomain sne pg0 = withRepr bin $ withRepr (PBi.flipRepr bin) $ withSym $ \sym -> withPG_ pg0 $ do
   priority <- lift $ thisPriority
   
-  let nd = singleNodeDivergePoint (GraphNode sne)
+  let dp = singleNodeDivergePoint (GraphNode sne)
+  let nd = Qu.coerceToExists dp
   nd' <- case Qu.convertQuant nd of
     Just (nd' :: GraphNode' arch Qu.AllK) -> return nd'
     Nothing -> fail $ "Unexpected single-sided diverge point: " ++ show nd
@@ -634,7 +637,7 @@ initSingleSidedDomain sne pg0 = withRepr bin $ withSym $ \sym -> withPG_ pg0 $ d
         -- Should we lower the priority here? Is it possible to get caught in a loop otherwise?
         -- Formally we should be able to find all relevant nodes based on which bindings
         -- we're missing
-        liftPG $ getAllSyncPoints nd >>= \syncs -> forM_ syncs $ \syncPair -> do
+        liftPG $ getAllSyncPoints dp >>= \syncs -> forM_ syncs $ \syncPair -> do
           sp <- PPa.get (PBi.flipRepr bin) syncPair
           modify $ queueAncestors pr (GraphNode $ singleToNodeEntry (syncPointNode sp))
  
@@ -672,7 +675,7 @@ handleProcessSplit sne pg = withPG pg $ do
   priority <- lift $ thisPriority
   case getCurrentDomain pg divergeNode of
     Nothing -> do
-      liftPG $ modify $ queueAncestors (priority PriorityDomainRefresh) divergeNode
+      liftPG $ modify $ queueAncestors (priority PriorityDomainRefresh) (Qu.coerceToExists divergeNode)
       return Nothing
     Just{} -> do
       let nd = GraphNode (singleToNodeEntry sne)
@@ -763,6 +766,8 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do
     Nothing -> throwHere $ PEE.IncompatibleSingletonNodes blkO blkP
   
   let dp = singleNodeDivergence sneO
+  let nd = Qu.coerceToExists dp
+
   let syncNode = GraphNode syncNodeEntry
   let snePair = Qu.QuantEach (\case PBi.OriginalRepr -> sneO; PBi.PatchedRepr -> sneP)
   let pre_refines = getDomainRefinements syncNode pg
@@ -770,16 +775,16 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do
   -- we start with two scopes: one representing the program state at the point of divergence: 'init_scope',
   -- and one representing the program state at the merge point
   
-  pg_final <- withFreshScope (graphNodeBlocks dp) $ \(splitScope :: PS.SimScope sym arch init) -> do
+  pg_final <- withFreshScope (graphNodeBlocks nd) $ \(splitScope :: PS.SimScope sym arch init) -> do
     withFreshScope blkPair $ \(mergeScope :: PS.SimScope sym arch merge) -> do
       ((sbundlePair@(PPa.PatchPair sbundleO sbundleP)), pg') <- mergeBundles splitScope mergeScope snePair pg
-      dpDomSpec <- evalPG pg $ getCurrentDomainM dp
+      dpDomSpec <- evalPG pg $ getCurrentDomainM nd
       -- domain at the divergence point
       dpDom <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair splitScope) dpDomSpec
-      noop <- noopBundle splitScope (graphNodeBlocks dp)
+      noop <- noopBundle splitScope (graphNodeBlocks nd)
 
 
-      withValidInit splitScope (graphNodeBlocks dp) $ 
+      withValidInit splitScope (graphNodeBlocks nd) $ 
         withPredomain splitScope noop dpDom $
         withValidInit (singleBundleScope sbundleO) (singleBundleBlocks sbundleO) $
         withValidInit (singleBundleScope sbundleP) (singleBundleBlocks sbundleP) $
@@ -1224,8 +1229,9 @@ mergeBundles splitScope mergeScope snePair pg = withSym $ \sym -> withPG pg $ do
   PS.compositeScopeCases mergeScope splitScope $ \bin scope -> do
     let sne = Qu.quantEach snePair bin
     let dp = singleNodeDivergence sne
+    let nd = Qu.coerceToExists dp
     let bin_other = PBi.flipRepr bin
-    dpBlk <- PPa.get bin_other (graphNodeBlocks dp)
+    dpBlk <- PPa.get bin_other (graphNodeBlocks nd)
     let sneBlk = singleNodeBlock sne
     let blks = PPa.mkPair bin sneBlk dpBlk
     bundle <- lift $ noopBundle scope blks
@@ -1493,9 +1499,9 @@ withConditionsAssumed ::
 withConditionsAssumed scope bundle d node gr0 f = do
   foldr go f' [minBound..maxBound]
   where 
-    f' = withSym $ \sym -> case node of
-      GraphNode ne | Just (Some sne) <- asSingleNodeEntry ne -> 
-        lookupFnBindings scope sne gr0 >>= \case
+    f' = withSym $ \sym -> case asSingleNode node of
+      Just (Some (Qu.AsSingle snode)) -> 
+        lookupFnBindings scope snode gr0 >>= \case
           Just binds -> do
             bindsPred <- IO.liftIO $ PFn.toPred sym binds
             emitTraceLabel @"expr" "Bindings" (Some bindsPred)
@@ -2986,7 +2992,8 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi
       emitTrace @"message" $ "Known desynchronization point. Queue split analysis."
       return $ st{ branchGraph = gr1 }
     False -> do
-      let divergeNode = GraphNode currBlock
+      divergeNode <- toTwoSidedNode $ GraphNode currBlock
+      let someDivergeNode = Qu.coerceToExists divergeNode
       let pg = gr1
       let msg = "Control flow desynchronization found at: " ++ show divergeNode
       a <- case mchoice of
@@ -3015,20 +3022,20 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi
           pg1 <- chooseDesyncPoint divergeNode pg
           -- drop domains from any outgoing edges, since the set of outgoing edges
           -- from this node will likely change
-          let pg2 = dropPostDomains divergeNode (priority PriorityDomainRefresh) pg1
+          let pg2 = dropPostDomains someDivergeNode (priority PriorityDomainRefresh) pg1
           -- re-queue the node after picking a de-synchronization point
           let pg3 = queueNode (priority PriorityHandleActions) divergeNode pg2
           return $ st'{ branchGraph = pg3 }
         IsInfeasible condK -> do
-          gr2 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockO) condK pg
-          gr3 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockP) condK gr2
+          gr2 <- pruneCurrentBranch scope (someDivergeNode, GraphNode currBlockO) condK pg
+          gr3 <- pruneCurrentBranch scope (someDivergeNode, GraphNode currBlockP) condK gr2
           return $ st'{ branchGraph = gr3 }
         DeferDecision -> do
           -- add this back to the work list at a low priority
           -- this allows, for example, the analysis to determine
           -- that this is unreachable (potentially after refinements) and therefore
           -- doesn't need synchronization
-          Just pg1 <- return $ addToWorkList divergeNode (priority PriorityDeferred) pg
+          Just pg1 <- return $ addToWorkList someDivergeNode (priority PriorityDeferred) pg
           return $ st'{ branchGraph = pg1 }
         AlignControlFlow condK -> withSym $ \sym -> do
           traces <- bundleToInstrTraces bundle
diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs
index 14ba3ba0..e56d9f56 100644
--- a/src/Pate/Verification/Widening.hs
+++ b/src/Pate/Verification/Widening.hs
@@ -39,7 +39,7 @@ module Pate.Verification.Widening
   ) where
 
 import           GHC.Stack
-import           Control.Lens ( (.~), (&), (^.) )
+import           Control.Lens ( (.~), (&), (^.), (%~) )
 import           Control.Monad (when, forM_, unless, filterM, foldM, void)
 import           Control.Monad.IO.Class
 import qualified Control.Monad.IO.Unlift as IO
@@ -107,7 +107,7 @@ import qualified Pate.TraceCollection as PTc
 import           Pate.Verification.PairGraph
 import qualified Pate.Verification.ConditionalEquiv as PVC
 import qualified Pate.Verification.Validity as PVV
-import           Pate.Verification.PairGraph.Node ( GraphNode(..), pattern GraphNodeEntry, pattern GraphNodeReturn, nodeFuns, graphNodeBlocks )
+import           Pate.Verification.PairGraph.Node ( GraphNode, GraphNode'(..), pattern GraphNodeEntry, pattern GraphNodeReturn, nodeFuns, graphNodeBlocks, asSingleNode, singleNodeDivergence, singleNodeDivergePoint, singleNodeRepr )
 import qualified Pate.Verification.StrongestPosts.CounterExample as CE
 
 import qualified Pate.AssumptionSet as PAs
@@ -132,6 +132,8 @@ import Pate.Verification.Domain (universalDomain)
 import qualified Data.Parameterized.TraversableF as TF
 import qualified Data.IORef as IO
 import qualified Data.Parameterized.TraversableFC as TFC
+import qualified Data.Quant as Qu
+import qualified Pate.Verification.FnBindings as PFn
 
 -- | Generate a fresh abstract domain value for the given graph node.
 --   This should represent the most information we can ever possibly
@@ -829,47 +831,50 @@ propagateBindings ::
   GraphNode arch {- ^ to -} ->
   PairGraph sym arch ->
   EquivM sym arch (Maybe (PairGraph sym arch))
-propagateBindings scope bundle from to gr0 = withSym $ \sym -> case (from,to) of
-  (GraphNode fromE, GraphNode toE)
-    | Just (Some fromSNE) <- asSingleNodeEntry fromE
-    , Just  (Some toSNE) <- asSingleNodeEntry toE
-    -- nodes are both single-sided and the same side
-    , Just Refl <- testEquality (singleEntryBin fromSNE) (singleEntryBin toSNE)
-    -- nodes have the same divergence point
-    , fromDP <- singleNodeDivergePoint fromSNE
-    , dp <- singleNodeDivergePoint toSNE
-    , fromDP == dp
-    -- 'to' node has defined bindings that need to be propagated
-    , Just (PS.AbsT toBindsSpec) <- MapF.lookup toSNE (gr0 ^. (syncData dp . syncBindings))
-    -> do
-      let outVars = PS.bundleOutVars scope bundle
-      toBinds <- liftIO $ PS.bindSpec sym outVars toBindsSpec
-      lookupFnBindings scope fromSNE gr0 >>= \case
-        -- 'from' has existing binds so we check if we actually need to propagate
-        -- FIXME: can we check this without the solver? do we need to check it?
-        Just fromBinds -> do
-          emitTrace @"debug" "Propagating and merging with existing bindings"
-          fromBindsPred <- IO.liftIO $ PFn.toPred sym fromBinds
-          withAssumption fromBindsPred $ do
-            toBindsPred <- IO.liftIO $ PFn.toPred sym toBinds
-            not_toBindsPred <- liftIO $ W4.notPred sym toBindsPred
-            goalTimeout <- CMR.asks (PC.cfgGoalTimeout . envConfig)
-            isPredSat' goalTimeout not_toBindsPred >>= \case
-              Just False -> do
-                emitTraceLabel @"expr" (ExprLabel $ "Proved bindings") (Some toBindsPred)
-                return Nothing
-              _ -> do
-                -- FIXME: use 'addFnBindings' instead? needs to take a mux condition
-                pathCond <- scopedPathCondition scope
-                bindsCombined <- IO.liftIO $ PFn.mux sym pathCond toBinds fromBinds
-                return $ Just $ gr0 & (syncData dp . syncBindings) %~ MapF.insert fromSNE (PS.AbsT $ PS.mkSimSpec scope bindsCombined)
-        -- 'from' has no binds so we propagate unconditionally
-        Nothing -> do
-          -- FIXME: do we care about the path condition here?
-          emitTrace @"debug" "Propagating bindings"
-          return $ Just $ gr0 & (syncData dp . syncBindings) %~ MapF.insert fromSNE (PS.AbsT $ PS.mkSimSpec scope toBinds)
+propagateBindings scope bundle from to gr0 = withSym $ \sym -> case (asSingleNode from,asSingleNode to) of
+  (Just (Some (Qu.AsSingle fromS)), Just (Some (Qu.AsSingle toS))) ->
+    case testEquality (singleNodeRepr fromS) (singleNodeRepr toS) of
+      Nothing -> do
+        fail $ "Unexpected mismatched single-sided nodes" ++ show from ++ " vs. " ++ show to
+      Just Refl -> do
+        let dp = singleNodeDivergePoint fromS
+        unless (dp == singleNodeDivergePoint toS) $
+          fail $ "Unexpected mismatched divergence points" ++ show from ++ "vs. " ++ show to
+        case MapF.lookup (Qu.AsSingle toS) (gr0 ^. (syncData dp . syncBindings)) of
+          -- no bindings to propagate, nothing to do
+          Nothing -> do
+            emitTrace @"debug" "No bindings to propagate"
+            return Nothing
+          -- 'to' node has defined bindings that need to be propagated
+          Just (PS.AbsT toBindsSpec) -> do
+            let outVars = PS.bundleOutVars scope bundle
+            toBinds <- liftIO $ PS.bindSpec sym outVars toBindsSpec
+            lookupFnBindings scope fromS gr0 >>= \case
+              -- 'from' has existing binds so we check if we actually need to propagate
+              -- FIXME: can we check this without the solver? do we need to check it?
+              Just fromBinds -> do
+                emitTrace @"debug" "Propagating and merging with existing bindings"
+                fromBindsPred <- IO.liftIO $ PFn.toPred sym fromBinds
+                withAssumption fromBindsPred $ do
+                  toBindsPred <- IO.liftIO $ PFn.toPred sym toBinds
+                  not_toBindsPred <- liftIO $ W4.notPred sym toBindsPred
+                  goalTimeout <- CMR.asks (PC.cfgGoalTimeout . envConfig)
+                  isPredSat' goalTimeout not_toBindsPred >>= \case
+                    Just False -> do
+                      emitTraceLabel @"expr" (ExprLabel $ "Proved bindings") (Some toBindsPred)
+                      return Nothing
+                    _ -> do
+                      -- FIXME: use 'addFnBindings' instead? needs to take a mux condition
+                      pathCond <- scopedPathCondition scope
+                      bindsCombined <- IO.liftIO $ PFn.mux sym pathCond toBinds fromBinds
+                      return $ Just $ gr0 & (syncData dp . syncBindings) %~ MapF.insert (Qu.AsSingle fromS) (PS.AbsT $ PS.mkSimSpec scope bindsCombined)
+              -- 'from' has no binds so we propagate unconditionally
+              Nothing -> do
+                -- FIXME: do we care about the path condition here?
+                emitTrace @"debug" "Propagating bindings"
+                return $ Just $ gr0 & (syncData dp . syncBindings) %~ MapF.insert (Qu.AsSingle fromS) (PS.AbsT $ PS.mkSimSpec scope toBinds)
   _ -> do
-    emitTrace @"debug" "No bindings to propagate"
+    emitTrace @"debug" "Not a pair of single-sided nodes"
     return Nothing
 
 -- | Propagate the given condition kind backwards (from 'to' node to 'from' node).