{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.Verify where


import Debug.Trace (trace, traceShow, traceShowId)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified Hask.Utils

import qualified LinearScan.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Contravariant as Contravariant
import qualified LinearScan.Functor as Functor
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.IntSet as IntSet
import qualified LinearScan.Lens as Lens
import qualified LinearScan.List1 as List1
import qualified LinearScan.Loops as Loops
import qualified LinearScan.Maybe as Maybe
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.Resolve as Resolve
import qualified LinearScan.Ssr as Ssr
import qualified LinearScan.State0 as State0
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Vector0 as Vector0
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Fintype as Fintype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrnat as Ssrnat



#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
#endif


#ifdef __GLASGOW_HASKELL__
--unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
--unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

type PhysReg = Prelude.Int

data UseVerifier =
   VerifyDisabled
 | VerifyEnabled
 | VerifyEnabledStrict

type RegAllocations =
  Vector0.Vec ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))

data RegStateDesc =
   Build_RegStateDesc RegAllocations IntSet.IntSet

rsAllocs :: Prelude.Int -> RegStateDesc -> RegAllocations
rsAllocs maxReg r =
  case r of {
   Build_RegStateDesc rsAllocs0 rsStack0 -> rsAllocs0}

rsStack :: Prelude.Int -> RegStateDesc -> IntSet.IntSet
rsStack maxReg r =
  case r of {
   Build_RegStateDesc rsAllocs0 rsStack0 -> rsStack0}

data RegStateDescSet =
   Build_RegStateDescSet ([]
                         ((,) (Prelude.Maybe Blocks.VarId)
                         (Prelude.Maybe Blocks.VarId))) IntSet.IntSet

fromRegStateDesc :: Prelude.Int -> RegStateDesc -> RegStateDescSet
fromRegStateDesc maxReg x =
  Build_RegStateDescSet (Vector0.vec_to_seq maxReg (rsAllocs maxReg x))
    (rsStack maxReg x)

residency :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1) ->
             ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))
             -> a1
residency h x x0 =
  Lens._1 h x x0

reservation :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1)
               -> ((,) (Prelude.Maybe Blocks.VarId)
               (Prelude.Maybe Blocks.VarId)) -> a1
reservation h x x0 =
  Lens._2 h x x0

newRegStateDesc :: Prelude.Int -> RegStateDesc
newRegStateDesc maxReg =
  Build_RegStateDesc
    (Vector0.vconst maxReg ((,) Prelude.Nothing Prelude.Nothing))
    IntSet.emptyIntSet

data AllocError =
   VarNotAllocated Blocks.VarId
 | VarNotResident Blocks.VarId
 | VarNotResidentForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) 
 Prelude.Int
 | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) 
 Prelude.Int
 | PhysRegAlreadyReservedForVar Prelude.Int Blocks.VarId
 | RegAlreadyReservedToVar Prelude.Int Blocks.VarId Blocks.VarId
 | BlockWithoutPredecessors Blocks.BlockId
 | UnknownPredecessorBlock Blocks.BlockId Blocks.BlockId
 | LoopInResolvingMoves Resolve.ResolvingMoveSet

type RegStateSig = RegStateDesc

packRegState :: Prelude.Int -> RegStateDesc -> RegStateDesc
packRegState maxReg rd =
  rd

data VerifiedSig a =
   Build_VerifiedSig RegStateDesc (IntMap.IntMap RegStateSig) (IntMap.IntMap
                                                              RegStateSig) 
 (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) (IntMap.IntMap
                                               ((,) RegStateDescSet
                                               ([] AllocError))) a

verDesc :: Prelude.Int -> (VerifiedSig a1) -> RegStateDesc
verDesc maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verDesc0}

verInit :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig
verInit maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verInit0}

verFinal :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig
verFinal maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verFinal0}

verMoves :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap
            ([] Resolve.ResolvingMoveSet)
verMoves maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verMoves0}

verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap
             ((,) RegStateDescSet ([] AllocError))
verErrors maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verErrors0}

verExt :: Prelude.Int -> (VerifiedSig a1) -> a1
verExt maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verExt0}

newVerifiedSig :: Prelude.Int -> a1 -> VerifiedSig a1
newVerifiedSig maxReg i =
  Build_VerifiedSig (newRegStateDesc maxReg) IntMap.emptyIntMap
    IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap i

_verDesc :: Prelude.Int -> (Functor.Functor a2) ->
            (Contravariant.Contravariant a2) -> (RegStateDesc -> a2) ->
            (VerifiedSig a1) -> a2
_verDesc maxReg h h0 f s =
  Functor.fmap h (Prelude0.const s) (f (verDesc maxReg s))

_verState :: Prelude.Int -> (Functor.Functor a2) -> (RegStateDesc -> a2) ->
             (VerifiedSig a1) -> a2
_verState maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig ( x) (verInit maxReg s)
    (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verDesc maxReg s))

_verInit :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
            RegStateSig) -> a2) -> (VerifiedSig a1) -> a2
_verInit maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s) x
    (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verInit maxReg s))

_verFinal :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
             RegStateSig) -> a2) -> (VerifiedSig a1) -> a2
_verFinal maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) x (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verFinal maxReg s))

_verMoves :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
             ([] Resolve.ResolvingMoveSet)) -> a2) -> (VerifiedSig a1) -> a2
_verMoves maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) x (verErrors maxReg s)
    (verExt maxReg s)) (f (verMoves maxReg s))

_verErrors :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
              ((,) RegStateDescSet ([] AllocError))) -> a2) -> (VerifiedSig
              a1) -> a2
_verErrors maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s) x
    (verExt maxReg s)) (f (verErrors maxReg s))

_verExt :: Prelude.Int -> (Functor.Functor a2) -> (a1 -> a2) -> (VerifiedSig
           a1) -> a2
_verExt maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s)
    (verErrors maxReg s) x) (f (verExt maxReg s))

type Verified mType a a0 = State0.StateT (VerifiedSig a) mType a0

errorsT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([] AllocError)
           -> Verified a1 a2 ()
errorsT maxReg mDict pc errs =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Lens.applyStateT (\_ -> _verErrors maxReg) (\m ->
      Prelude0.flip (IntMap.coq_IntMap_insert pc) m
        (case IntMap.coq_IntMap_lookup pc m of {
          Prelude.Just p ->
           case p of {
            (,) d prevErrs -> (,) d ((Prelude.++) prevErrs errs)};
          Prelude.Nothing -> (,) (fromRegStateDesc maxReg st) errs})) mDict)
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

errorT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> AllocError ->
          Verified a1 a2 ()
errorT maxReg mDict pc err =
  errorsT maxReg mDict pc ((:) err [])

addMove :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
           Resolve.ResolvingMoveSet -> Verified a1 a2 ()
addMove maxReg mDict pc mv =
  Lens.applyStateT (\_ -> _verMoves maxReg)
    (IntMap.coq_IntMap_alter (\mxs -> Prelude.Just
      (case mxs of {
        Prelude.Just xs -> Seq.rcons xs mv;
        Prelude.Nothing -> (:) mv []})) pc) mDict

reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->
              Blocks.VarId -> Verified a1 a2 ()
reserveReg maxReg mDict pc reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce Prelude.Nothing)) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> reservation) (Prelude.Just var)))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        case Lens.view (Lens.stepdownl' (\_ -> reservation))
               (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
         Prelude.Just v ->
          Monad.when (State0.coq_StateT_Monad mDict)
            (Prelude.not
              (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v)
                (unsafeCoerce var)))
            (errorT maxReg mDict pc (RegAlreadyReservedToVar ( reg) v var));
         Prelude.Nothing ->
          Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg)))

isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->
              Verified a1 a2 (Prelude.Maybe Blocks.VarId)
isReserved maxReg mDict reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Applicative.pure (State0.coq_StateT_Applicative mDict)
      (Lens.view (Lens.stepdownl' (\_ -> reservation))
        (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                    UseVerifier -> PhysReg -> Blocks.VarId -> Verified 
                    a1 a2 ()
checkReservation maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    let {
     err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
             (Lens.view (Lens.stepdownl' (\_ -> reservation))
               (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
             ((Prelude.succ) 0))}
    in
    Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
      case res of {
       Prelude.Just var' ->
        Monad.unless (State0.coq_StateT_Monad mDict)
          (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var) var') err;
       Prelude.Nothing ->
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
      (isReserved maxReg mDict reg var))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier
              -> PhysReg -> Blocks.VarId -> Verified a1 a2 ()
releaseReg maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce (Prelude.Just var))) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> reservation) Prelude.Nothing))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        let {
         err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
                 (Lens.view (Lens.stepdownl' (\_ -> reservation))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                 ((Prelude.succ) ((Prelude.succ) 0)))}
        in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ ->
          case Lens.view (Lens.stepdownl' (\_ -> reservation))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
           Prelude.Just v -> err;
           Prelude.Nothing ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var))

assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
             PhysReg -> Blocks.VarId -> Verified a1 a2 ()
assignReg maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce (Prelude.Just var))) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> residency) (Prelude.Just var)))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        let {
         err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
                 (Lens.view (Lens.stepdownl' (\_ -> reservation))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                 ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))}
        in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ ->
          case Lens.view (Lens.stepdownl' (\_ -> reservation))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
           Prelude.Just v -> err;
           Prelude.Nothing ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg)))

isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->
              Verified a1 a2 (Prelude.Maybe Blocks.VarId)
isResident maxReg mDict reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Applicative.pure (State0.coq_StateT_Applicative mDict)
      (Lens.view (Lens.stepdownl' (\_ -> residency))
        (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkResidency :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                  UseVerifier -> PhysReg -> Blocks.VarId -> Verified 
                  a1 a2 ()
checkResidency maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
      let {
       err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg) res
               ((Prelude.succ) 0))}
      in
      case useVerifier of {
       VerifyEnabledStrict ->
        case res of {
         Prelude.Just var' ->
          Monad.unless (State0.coq_StateT_Monad mDict)
            (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var)
              (unsafeCoerce var')) err;
         Prelude.Nothing -> err};
       _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()})
      (isResident maxReg mDict reg var))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                 UseVerifier -> IntSet.IntSet -> Verified a1 a2 ()
checkLiveness maxReg mDict pc useVerifier vars =
  case useVerifier of {
   VerifyEnabledStrict ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      Monad.forM_ (State0.coq_StateT_Monad mDict)
        (IntSet.coq_IntSet_toList vars) (\var ->
        Monad.unless (State0.coq_StateT_Monad mDict)
          (Vector0.vfoldl_with_index maxReg (\reg b p ->
            (Prelude.||) b
              (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {
                Prelude.Just var0 -> Prelude.True;
                Prelude.Nothing -> Prelude.False})) Prelude.False
            (rsAllocs maxReg st))
          (errorT maxReg mDict pc (VarNotResident var))))
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict);
   _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}

verifyBlockBegin :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                    UseVerifier -> Prelude.Int -> IntSet.IntSet ->
                    Loops.LoopState -> Verified a1 a2 ()
verifyBlockBegin maxReg mDict pc useVerifier bid liveIns loops =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   VerifyEnabled ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
        Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
          Lens.applyStateT (\_ -> _verInit maxReg)
            (IntMap.coq_IntMap_insert bid allocs) mDict)
          (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))
        (checkLiveness maxReg mDict pc useVerifier liveIns))
      (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {
        Prelude.Just fwds ->
         Monad.forM_ (State0.coq_StateT_Monad mDict)
           (IntSet.coq_IntSet_toList fwds) (\pred ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->
             case IntMap.coq_IntMap_lookup pred exits of {
              Prelude.Just allocs ->
               Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;
              Prelude.Nothing ->
               errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})
             (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict));
        Prelude.Nothing ->
         case useVerifier of {
          VerifyEnabledStrict ->
           Monad.when (State0.coq_StateT_Monad mDict)
             ((Prelude.<=) ((Prelude.succ) 0)
               (IntSet.coq_IntSet_size liveIns))
             (errorT maxReg mDict pc (BlockWithoutPredecessors bid));
          _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}});
   VerifyEnabledStrict ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
        Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
          Lens.applyStateT (\_ -> _verInit maxReg)
            (IntMap.coq_IntMap_insert bid allocs) mDict)
          (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))
        (checkLiveness maxReg mDict pc useVerifier liveIns))
      (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {
        Prelude.Just fwds ->
         Monad.forM_ (State0.coq_StateT_Monad mDict)
           (IntSet.coq_IntSet_toList fwds) (\pred ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->
             case IntMap.coq_IntMap_lookup pred exits of {
              Prelude.Just allocs ->
               Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;
              Prelude.Nothing ->
               errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})
             (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict));
        Prelude.Nothing ->
         case useVerifier of {
          VerifyEnabledStrict ->
           Monad.when (State0.coq_StateT_Monad mDict)
             ((Prelude.<=) ((Prelude.succ) 0)
               (IntSet.coq_IntSet_size liveIns))
             (errorT maxReg mDict pc (BlockWithoutPredecessors bid));
          _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})}

verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                  UseVerifier -> Prelude.Int -> IntSet.IntSet -> Verified 
                  a1 a2 ()
verifyBlockEnd maxReg mDict pc useVerifier bid liveOuts =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   _ ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
        Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
          Lens.modifyStateT (\_ -> _verState maxReg)
            (packRegState maxReg (newRegStateDesc maxReg)) mDict)
          (Lens.applyStateT (\_ -> _verFinal maxReg)
            (IntMap.coq_IntMap_insert bid allocs) mDict))
        (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))
      (checkLiveness maxReg mDict pc useVerifier liveOuts)}

verifyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 
                a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]
                ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg)) -> Verified
                a3 a4 ()
verifyAllocs maxReg mDict oinfo pc useVerifier op allocs =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   VerifyEnabled ->
    Monad.forM_ (State0.coq_StateT_Monad mDict)
      (Blocks.opRefs maxReg mDict oinfo op) (\ref ->
      case Blocks.varId maxReg ref of {
       Prelude.Left reg ->
        Applicative.pure (State0.coq_StateT_Applicative mDict) ();
       Prelude.Right var ->
        case List1.maybeLookup
               (Eqtype.prod_eqType Ssrnat.nat_eqType
                 UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)
               (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {
         Prelude.Just reg ->
          case Blocks.varKind maxReg ref of {
           UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;
           UsePos.Temp ->
            checkReservation maxReg mDict pc useVerifier reg var;
           UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};
         Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}});
   VerifyEnabledStrict ->
    Monad.forM_ (State0.coq_StateT_Monad mDict)
      (Blocks.opRefs maxReg mDict oinfo op) (\ref ->
      case Blocks.varId maxReg ref of {
       Prelude.Left reg ->
        Applicative.pure (State0.coq_StateT_Applicative mDict) ();
       Prelude.Right var ->
        case List1.maybeLookup
               (Eqtype.prod_eqType Ssrnat.nat_eqType
                 UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)
               (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {
         Prelude.Just reg ->
          case Blocks.varKind maxReg ref of {
           UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;
           UsePos.Temp ->
            checkReservation maxReg mDict pc useVerifier reg var;
           UsePos.Output -> assignReg maxReg mDict pc useVerifier reg var};
         Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})}

verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                     UseVerifier -> ([] Resolve.ResolvingMove) -> Verified 
                     a1 a2 ([] Resolve.ResolvingMove)
verifyResolutions maxReg mDict pc useVerifier moves =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) moves;
   _ ->
    Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
        case mv of {
         Resolve.Move fromReg fromVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
                Monad.bind (State0.coq_StateT_Monad mDict) (\check ->
                  Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->
                    Applicative.pure (State0.coq_StateT_Applicative mDict)
                      (Seq.rcons acc mv))
                    (case useVerifier of {
                      VerifyEnabledStrict ->
                       Monad.when (State0.coq_StateT_Monad mDict)
                         (Maybe.isJust check)
                         (assignReg maxReg mDict pc useVerifier toReg
                           fromVar);
                      _ ->
                       assignReg maxReg mDict pc useVerifier toReg fromVar}))
                  (isResident maxReg mDict fromReg fromVar))
                (addMove maxReg mDict pc
                  (Resolve.weakenResolvingMove maxReg mv)))
              (reserveReg maxReg mDict pc toReg fromVar))
            (Monad.unless (State0.coq_StateT_Monad mDict)
              (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
                (unsafeCoerce fromReg) (unsafeCoerce toReg))
              (releaseReg maxReg mDict pc useVerifier fromReg fromVar));
         Resolve.Transfer fromReg fromVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
              Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
              (reserveReg maxReg mDict pc toReg fromVar))
            (Monad.unless (State0.coq_StateT_Monad mDict)
              (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
                (unsafeCoerce fromReg) (unsafeCoerce toReg))
              (releaseReg maxReg mDict pc useVerifier fromReg fromVar));
         Resolve.Spill fromReg toSpillSlot ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\check ->
              case Maybe.isJust check of {
               Prelude.True ->
                Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
                  Applicative.pure (State0.coq_StateT_Applicative mDict)
                    (Seq.rcons acc mv))
                  (addMove maxReg mDict pc
                    (Resolve.weakenResolvingMove maxReg mv));
               Prelude.False ->
                Applicative.pure (State0.coq_StateT_Applicative mDict) acc})
              (isResident maxReg mDict fromReg toSpillSlot))
            (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot);
         Resolve.Restore fromSpillSlot toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
                Applicative.pure (State0.coq_StateT_Applicative mDict)
                  (Seq.rcons acc mv))
                (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot))
              (addMove maxReg mDict pc
                (Resolve.weakenResolvingMove maxReg mv)))
            (reserveReg maxReg mDict pc toReg fromSpillSlot);
         Resolve.AllocReg toVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (reserveReg maxReg mDict pc toReg toVar);
         Resolve.FreeReg fromReg fromVar ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (releaseReg maxReg mDict pc useVerifier fromReg fromVar);
         Resolve.Looped x ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
              Applicative.pure (State0.coq_StateT_Applicative mDict)
                (Seq.rcons acc mv))
              (addMove maxReg mDict pc
                (Resolve.weakenResolvingMove maxReg mv)))
            (errorT maxReg mDict pc (LoopInResolvingMoves
              (Resolve.weakenResolvingMove maxReg x)))})
        (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}