From 1a8f0e01247ecaae5ecc6df49fc505513d7349c3 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Sun, 18 Jul 2021 20:21:41 -0700
Subject: [PATCH 1/4] Incorporate crucible fancy assumptions

---
 deps/crucible                                 |  2 +-
 deps/macaw                                    |  2 +-
 .../Verifier/SAW/Heapster/SAWTranslation.hs   |  2 ++
 .../src/Verifier/SAW/Heapster/TypeChecker.hs  |  1 +
 src/SAWScript/Crucible/Common.hs              |  2 +-
 src/SAWScript/Crucible/JVM/Builtins.hs        | 25 +++++++-------
 src/SAWScript/Crucible/JVM/Override.hs        | 10 +++---
 src/SAWScript/Crucible/LLVM/Builtins.hs       | 34 +++++++++++--------
 src/SAWScript/Crucible/LLVM/Override.hs       | 10 +++---
 src/SAWScript/Crucible/LLVM/X86.hs            |  4 +--
 src/SAWScript/X86.hs                          | 11 +++---
 src/SAWScript/X86Spec.hs                      | 13 +++----
 12 files changed, 65 insertions(+), 51 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index 584d47d384..168f000959 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 584d47d384104c06a92b3820882639e9898e4b0d
+Subproject commit 168f0009591833358b8dc8a9a3f76e09edeb3e4d
diff --git a/deps/macaw b/deps/macaw
index 135fb062bb..764de152ce 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 135fb062bb35a145ac21da816244d97e6d70f425
+Subproject commit 764de152ceb0166aa04ec1a0ddbb2806b2595926
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index c761009ecf..9da457a795 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -599,6 +599,8 @@ instance TransInfo info =>
       return $ error "translate: RealValRepr"
     [nuMP| ComplexRealRepr |] ->
       return $ error "translate: ComplexRealRepr"
+    [nuMP| SequenceRepr{} |] ->
+      return $ error "translate: SequenceRepr"
     [nuMP| BVRepr w |] ->
       returnType1 =<< bitvectorTransM (translate w)
 
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
index 3724d07053..2579b458b5 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
@@ -331,6 +331,7 @@ tcExpr WordMapRepr       {} e = tcError (pos e) "Expected wordmap"
 tcExpr StringMapRepr     {} e = tcError (pos e) "Expected stringmap"
 tcExpr SymbolicArrayRepr {} e = tcError (pos e) "Expected symbolicarray"
 tcExpr SymbolicStructRepr{} e = tcError (pos e) "Expected symbolicstruct"
+tcExpr SequenceRepr      {} e = tcError (pos e) "Expected sequencerepr"
 
 -- | Check for a unit literal
 tcUnit :: AstExpr -> Tc (PermExpr UnitType)
diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
index e6cca931a6..45f9681972 100644
--- a/src/SAWScript/Crucible/Common.hs
+++ b/src/SAWScript/Crucible/Common.hs
@@ -58,7 +58,7 @@ sawCoreState sym = pure (onlineUserState (W4.sbUserState sym))
 ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann)
                 -> AbortedResult Sym ext
                 -> PP.Doc ann
-ppAbortedResult _ (AbortedExec InfeasibleBranch _) =
+ppAbortedResult _ (AbortedExec InfeasibleBranch{} _) =
   PP.pretty "Infeasible branch"
 ppAbortedResult ppGP (AbortedExec abt gp) = do
   PP.vcat
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index 795da169d1..6032f84365 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -59,7 +59,6 @@ import qualified Data.Map as Map
 import           Data.Maybe (fromMaybe, isNothing)
 import           Data.Set (Set)
 import qualified Data.Set as Set
-import qualified Data.Sequence as Seq
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.Time.Clock (getCurrentTime, diffUTCTime)
@@ -132,6 +131,7 @@ import SAWScript.Crucible.JVM.Override
 import SAWScript.Crucible.JVM.ResolveSetupValue
 import SAWScript.Crucible.JVM.BuiltinsJVM ()
 
+type AssumptionReason = (W4.ProgramLoc, String)
 type SetupValue = MS.SetupValue CJ.JVM
 type Lemma = MS.ProvedSpec CJ.JVM
 type MethodSpec = MS.CrucibleMethodSpecIR CJ.JVM
@@ -276,7 +276,7 @@ verifyObligations ::
   JVMCrucibleContext ->
   MethodSpec ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   [(String, W4.ProgramLoc, Term)] ->
   TopLevel (SolverStats, Set TheoremNonce)
 verifyObligations cc mspec tactic assumes asserts =
@@ -333,7 +333,7 @@ verifyPrestate ::
   MethodSpec ->
   Crucible.SymGlobalState Sym ->
   IO ([(J.Type, JVMVal)],
-      [Crucible.LabeledPred Term Crucible.AssumptionReason],
+      [Crucible.LabeledPred Term AssumptionReason],
       Map AllocIndex JVMRefVal,
       Crucible.SymGlobalState Sym)
 verifyPrestate cc mspec globals0 =
@@ -511,7 +511,7 @@ setupPrestateConditions ::
   JVMCrucibleContext ->
   Map AllocIndex JVMRefVal ->
   [SetupCondition] ->
-  IO [Crucible.LabeledPred Term Crucible.AssumptionReason]
+  IO [Crucible.LabeledPred Term AssumptionReason]
 setupPrestateConditions mspec cc env = aux []
   where
     tyenv   = MS.csAllocations mspec
@@ -523,11 +523,11 @@ setupPrestateConditions mspec cc env = aux []
       do val1' <- resolveSetupVal cc env tyenv nameEnv val1
          val2' <- resolveSetupVal cc env tyenv nameEnv val2
          t     <- assertEqualVals cc val1' val2'
-         let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition")
+         let lp = Crucible.LabeledPred t (loc, "equality precondition")
          aux (lp:acc) xs
 
     aux acc (MS.SetupCond_Pred loc tm : xs) =
-      let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in
+      let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in
       aux (lp:acc) xs
 
     aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_
@@ -593,7 +593,7 @@ verifySimulate ::
   [Crucible.GenericExecutionFeature Sym] ->
   MethodSpec ->
   [(a, JVMVal)] ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   W4.ProgramLoc ->
   [Lemma] ->
   Crucible.SymGlobalState Sym ->
@@ -630,9 +630,10 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat =
                    mapM_ (registerOverride opts cc simctx top_loc)
                            (groupOn (view csMethodName) (map (view MS.psSpec) lemmas))
                    liftIO $ putStrLn "registering assumptions"
-                   liftIO $ do
-                     preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes
-                     Crucible.addAssumptions sym (Seq.fromList preds)
+                   liftIO $
+                     for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) ->
+                       do expr <- resolveSAWPred cc p
+                          Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr)
                    liftIO $ putStrLn "simulating function"
                    fnCall
           Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats)
@@ -731,14 +732,14 @@ verifyPoststate cc mspec env0 globals ret =
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
-     io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations)
+     io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations)
 
   where
     sym = cc^.jccBackend
 
     verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) =
       do st         <- sawCoreState sym
-         hypTerm    <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps)
+         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
          conclTerm  <- toSC sym st concl
          obligation <- scImplies sc hypTerm conclTerm
          return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, loc, obligation)
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
index 4d43bcc447..7e9c35f199 100644
--- a/src/SAWScript/Crucible/JVM/Override.hs
+++ b/src/SAWScript/Crucible/JVM/Override.hs
@@ -243,13 +243,15 @@ methodSpecHandler opts sc cc top_loc css h = do
                 case res of
                   Left (OF loc rsn)  ->
                     -- TODO, better pretty printing for reasons
-                    liftIO $ Crucible.abortExecBecause
-                      (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn)))
+                    liftIO
+                      $ Crucible.abortExecBecause
+                      $ Crucible.AssertionFailure
+                      $ Crucible.SimError loc
+                      $ Crucible.AssertFailureSimError "assumed false" (show rsn)
                   Right (ret,st') ->
                     do liftIO $ forM_ (st'^.osAssumes) $ \asum ->
                          Crucible.addAssumption (cc ^. jccBackend)
-                            (Crucible.LabeledPred asum
-                              (Crucible.AssumptionReason (st^.osLocation) "override postcondition"))
+                          $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
                        Crucible.writeGlobals (st'^.overrideGlobals)
                        Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
            , Just (W4.plSourceLoc (cs ^. MS.csLoc))
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 25a76c0196..e7a33e0f30 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -198,6 +198,8 @@ import SAWScript.Crucible.LLVM.Override
 import SAWScript.Crucible.LLVM.ResolveSetupValue
 import SAWScript.Crucible.LLVM.MethodSpecIR
 
+type AssumptionReason = (W4.ProgramLoc, String)
+
 type MemImpl = Crucible.MemImpl Sym
 
 data LLVMVerificationException
@@ -603,7 +605,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
 verifyObligations :: LLVMCrucibleContext arch
                   -> MS.CrucibleMethodSpecIR (LLVM arch)
                   -> ProofScript ()
-                  -> [Crucible.LabeledPred Term Crucible.AssumptionReason]
+                  -> [Crucible.LabeledPred Term AssumptionReason]
                   -> [(String, W4.ProgramLoc, Term)]
                   -> TopLevel (SolverStats, Set TheoremNonce)
 verifyObligations cc mspec tactic assumes asserts =
@@ -738,7 +740,7 @@ verifyPrestate ::
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   Crucible.SymGlobalState Sym ->
   IO ([(Crucible.MemType, LLVMVal)],
-      [Crucible.LabeledPred Term Crucible.AssumptionReason],
+      [Crucible.LabeledPred Term AssumptionReason],
       Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)),
       Crucible.SymGlobalState Sym)
 verifyPrestate opts cc mspec globals =
@@ -772,7 +774,7 @@ assumptionsContainContradiction ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel Bool
 assumptionsContainContradiction cc tactic assumptions =
   do
@@ -803,7 +805,7 @@ computeMinimalContradictingCore ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel ()
 computeMinimalContradictingCore cc tactic assumes =
   do
@@ -814,8 +816,9 @@ computeMinimalContradictingCore cc tactic assumes =
      findM (assumptionsContainContradiction cc tactic) cores >>= \case
       Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
       Just core ->
-        forM_ core $ \ assumption ->
-          printOutLnTop Warn (show . Crucible.ppAssumptionReason $ assumption ^. Crucible.labeledPredMsg)
+        forM_ core $ \assume ->
+          case assume^.Crucible.labeledPredMsg of
+            (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
      printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."
 
 -- | Checks whether the given list of assumptions contains a contradiction, and
@@ -824,7 +827,7 @@ checkAssumptionsForContradictions ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel ()
 checkAssumptionsForContradictions cc tactic assumes =
   whenM
@@ -953,7 +956,7 @@ setupPrestateConditions ::
   Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) ->
   Crucible.SymGlobalState Sym ->
   [MS.SetupCondition (LLVM arch)]            ->
-  IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term Crucible.AssumptionReason])
+  IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason])
 setupPrestateConditions mspec cc mem env = aux []
   where
     tyenv   = MS.csAllocations mspec
@@ -965,11 +968,11 @@ setupPrestateConditions mspec cc mem env = aux []
       do val1' <- resolveSetupVal cc mem env tyenv nameEnv val1
          val2' <- resolveSetupVal cc mem env tyenv nameEnv val2
          t     <- assertEqualVals cc val1' val2'
-         let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition")
+         let lp = Crucible.LabeledPred t (loc, "equality precondition")
          aux (lp:acc) globals xs
 
     aux acc globals (MS.SetupCond_Pred loc tm : xs) =
-      let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in
+      let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in
       aux (lp:acc) globals xs
 
     aux acc globals (MS.SetupCond_Ghost () _loc var val : xs) =
@@ -1155,7 +1158,7 @@ verifySimulate ::
   [Crucible.GenericExecutionFeature Sym] ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   [(Crucible.MemType, LLVMVal)] ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   W4.ProgramLoc ->
   [MS.ProvedSpec (LLVM arch)] ->
   Crucible.SymGlobalState Sym ->
@@ -1209,8 +1212,9 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as
            do mapM_ (registerOverride opts cc simCtx top_loc)
                     (groupOn (view csName) funcLemmas)
               liftIO $
-                do preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes
-                   Crucible.addAssumptions sym (Seq.fromList preds)
+                for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) ->
+                  do expr <- resolveSAWPred cc p
+                     Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr)
               Crucible.regValue <$> (Crucible.callBlock cfg entryId args')
      res <- Crucible.executeCrucible execFeatures initExecState
      case res of
@@ -1302,7 +1306,7 @@ verifyPoststate cc mspec env0 globals ret =
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
-     sc_obligations <- io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations)
+     sc_obligations <- io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations)
      return (sc_obligations, st)
 
   where
@@ -1310,7 +1314,7 @@ verifyPoststate cc mspec env0 globals ret =
 
     verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) =
       do st <- Common.sawCoreState sym
-         hypTerm <- toSC sym st =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps
+         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
          conclTerm  <- toSC sym st concl
          obligation <- scImplies sc hypTerm conclTerm
          return (unlines ["safety assertion:", show err], loc, obligation)
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 39a9924072..826f1d0f4d 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -475,13 +475,15 @@ methodSpecHandler opts sc cc top_loc css h = do
                 case res of
                   Left (OF loc rsn)  ->
                     -- TODO, better pretty printing for reasons
-                    liftIO $ Crucible.abortExecBecause
-                      (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn)))
+                    liftIO
+                      $ Crucible.abortExecBecause
+                      $ Crucible.AssertionFailure
+                      $ Crucible.SimError loc
+                      $ Crucible.AssertFailureSimError "assumed false" (show rsn)
                   Right (ret,st') ->
                     do liftIO $ forM_ (st'^.osAssumes) $ \asum ->
                          Crucible.addAssumption (cc^.ccBackend)
-                            (Crucible.LabeledPred asum
-                              (Crucible.AssumptionReason (st^.osLocation) "override postcondition"))
+                          $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
                        Crucible.writeGlobals (st'^.overrideGlobals)
                        Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
            , Just (W4.plSourceLoc (cs ^. MS.csLoc))
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 43f48450c2..88dbcfff99 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -914,8 +914,8 @@ assertPost globals env premem preregs = do
   st <- case result of
     Left err -> throwX86 $ show err
     Right (_, st) -> pure st
-  liftIO . forM_ (view O.osAssumes st) $ \p ->
-    C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition"
+  liftIO . forM_ (view O.osAssumes st) $
+    C.addAssumption sym . C.GenericAssumption (st ^. O.osLocation) "precondition"
   liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) ->
     C.addAssertion sym $ C.LabeledPred p r
 
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index 384d75b38f..01b143ff21 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -27,7 +27,7 @@ module SAWScript.X86
   ) where
 
 
-import Control.Lens (toListOf, folded, (^.))
+import Control.Lens ((^.))
 import Control.Exception(Exception(..),throwIO)
 import Control.Monad.IO.Class(liftIO)
 
@@ -72,7 +72,8 @@ import Lang.Crucible.Simulator.ExecutionTree
           )
 import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason)
 import Lang.Crucible.Backend
-          (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,proofGoalsToList)
+          (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,goalsToList
+          ,assumptionsPred)
 import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHandleMap,emptyHandleMap)
 
 
@@ -564,15 +565,15 @@ gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g)
 
 getGoals :: Sym -> IO [Goal]
 getGoals sym =
-  do obls <- proofGoalsToList <$> getProofObligations sym
+  do obls <- maybe [] goalsToList <$> getProofObligations sym
      st <- sawCoreState sym
      mapM (toGoal st) obls
   where
   toGoal st (ProofGoal asmps g) =
-    do as <- mapM (toSC sym st) (toListOf (folded . labeledPred) asmps)
+    do a1 <- toSC sym st =<< assumptionsPred sym asmps
        p  <- toSC sym st (g ^. labeledPred)
        let SimError loc msg = g^.labeledPredMsg
-       return Goal { gAssumes = as
+       return Goal { gAssumes = [a1]
                    , gShows   = p
                    , gLoc     = loc
                    , gMessage = msg
diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs
index 1c53e145d8..05ff826a3e 100644
--- a/src/SAWScript/X86Spec.hs
+++ b/src/SAWScript/X86Spec.hs
@@ -103,9 +103,9 @@ import qualified Lang.Crucible.LLVM.MemModel as Crucible
 
 import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError))
 import Lang.Crucible.Backend
-          (addAssumption, getProofObligations, proofGoalsToList
-          ,assert, AssumptionReason(..)
-          ,LabeledPred(..), ProofGoal(..), labeledPredMsg)
+          (addAssumption, getProofObligations, goalsToList
+          ,assert, CrucibleAssumption(..)
+          ,ProofGoal(..), labeledPredMsg)
 
 import Lang.Crucible.Simulator.ExecutionTree
 import Lang.Crucible.Simulator.OverrideSim
@@ -826,7 +826,8 @@ makeEquiv opts s (Pair (Rep t _) (Equiv xs ys)) =
      let same a =
            do p <- evalSame sym t v a
               let loc = mkProgramLoc "<makeEquiv>" InternalPos
-              addAssumption sym (LabeledPred p (AssumptionReason loc "equivalance class assumption"))
+              addAssumption sym
+                $ GenericAssumption loc "equivalance class assumption" p
 
      mapM_ same rest
 
@@ -847,7 +848,7 @@ addAsmp opts s (msg,p) =
 
     _ -> do p' <- evalProp opts p s
             let loc = mkProgramLoc "<addAssmp>" InternalPos -- FIXME
-            addAssumption (optsSym opts) (LabeledPred p' (AssumptionReason loc msg))
+            addAssumption (optsSym opts) (GenericAssumption loc msg p')
 
 setCryPost :: forall p. (Eval p, Crucible.HasLLVMAnn Sym) => Opts -> S p -> (String,Prop p) -> IO (S p)
 setCryPost opts s (_nm,p) =
@@ -1132,7 +1133,7 @@ debugPPReg r s =
 
 _debugDumpGoals :: Sym -> IO ()
 _debugDumpGoals sym =
-  do obls <- proofGoalsToList <$> getProofObligations sym
+  do obls <- maybe [] goalsToList <$> getProofObligations sym
      mapM_ sh (toList obls)
   where
   sh (ProofGoal _hyps g) = print (view labeledPredMsg g)

From 6ef2c2e8572679b8ff2291b1865ebb2c932babab Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Sun, 18 Jul 2021 20:29:20 -0700
Subject: [PATCH 2/4] Update crucible to get llvm debug information

---
 deps/crucible | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/deps/crucible b/deps/crucible
index 168f000959..f2abe5388c 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 168f0009591833358b8dc8a9a3f76e09edeb3e4d
+Subproject commit f2abe5388cee9f717af7a1dccf956a6896b47c51

From 0ffefe0a11faea35993f292aa7bca98e4c40cf95 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Mon, 19 Jul 2021 08:47:47 -0700
Subject: [PATCH 3/4] recompile salsa20.c to update debug information

---
 examples/salsa20/salsa20.bc | Bin 11968 -> 12032 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

diff --git a/examples/salsa20/salsa20.bc b/examples/salsa20/salsa20.bc
index 808474461be045342e3a2a861484595acf0b0ce0..bac4c70a9e7afd28d59c3f736e33af889cc93008 100644
GIT binary patch
literal 12032
zcmb_?dsti7mG3@!oFjyg4j^n{3w#9Fl^ucw*ciWJNeCMpk`aE@N!+o-E8t)d58L26
z=@AkUc1TC|(3G^9R@hET8aKg>Z^mDylaY9pIK(B1r{%hC0(R=_X55yvX+D3sndbiX
zk%VcQ`S0?fqqEmpd+oK>Ui-J#+DGq)7bg<@>G8RpM+ip<V=oE6zZL`~XjK|ZPWeM`
z)cx_jC+>AH1(ZZg8bZd@ge1yLM27Yvd^m6RN!x^?oaGDFpJM!)<w{k0rsAn8(NHS0
zpGvfk@&)>0mEnGMK~+zgXVjGKND1`vwo|g23DtSMP_ng0c#|op@*7r}R|WHr4edKA
zj88!BaRKAuyCAD4L8$3gq-LM><8s445Y(qs^!6tDM=SVq5hHU-VNFrwOeTvAGbWtq
zGOG%<5>}@6=9Jqn85#3rvf_EGT5OnDDc`{>(qt=7be-KHlt$J#(wLPKt7Mh@R!1`b
z^lLkW@4e7)<vU(M_1R#VAddP;&vUYnU{cx3<&_554PBOA``Vo^@W*&af>~~r4~vGt
zks#M;4zz^0!xMp`VBp9gcSH!Z3V|Xa&^{Ds$9=u8vxn;p1&S<ON4@W`iaToM!p325
z#?1jE=`z0S&K$NGrw5Ez#mr$-#`HkaxXCz;r;H`waRoZfoahR)_6Iua<sHF5t0B<d
z51H~dF#u7mWD?Bo%u9@L)s%5<API6VgEEkGd%!sE&3xaMd37f9U9a&LlR=7!>PQDw
zqf-?)Yz`EOfg@$ykx-yD7$`Dxhsy$o$t_#vM*~JNlJWjP(xfeOcp&4_K+?=?#=DV>
zTLZ=q2a+y%Gu|D@xEjuQKaz1(%(!GSPBOx^*^H|~#<hs?CVDZMS3?=Y-pr}H`g;OL
z>g9(91Bb;xQ7GWyIgH+US997uoG~1ML;lC^zRt2hn@4i&6jk_0|5y8Sm}(9yhMCM6
zIAqrNcgpm0M^%BAy)d8a?BI^lxx*v|iuk}$3)g1mIx$~m+~a1B=tvi)CiC)u@fIe9
z$^3{B1FasebAmfUR7X`@XK|pFPHUhQb2>=Fpp*R4Wt=l<Z;MIvhS5#CV9~OhwoKey
z9mtsTf)3p>CZ!t$0O&U{eKu|E#vQ-$YOe{gd$8SvK(cIZMoUg-UPHh{jF^|Na`hkr
zCQ#HLIAY<BB1l|;BhYQ$)zeOuJ;+Y5HPJ8*67`@jiT#+yw0w#cFGS2T7jw%cck^Uf
zqgiVzlh>DcHMS+<Fq@q$DhG@7+xfGMxzYTLpb8}^vlWb@9BV^`wUO$#_Vb!l_OxY%
zBH}j{2NM*PIpYeGbA{q9h1*S1*BlGWH{MZh4Ec&wT!%<wpr}6J!3yf<j`hfkJ-*^0
z`8v^;RO{3poYEeh(;f_J4_mpTF0Orwy(w~@5Z5Ab9aHQdMD8eJD8#i1v8S){T&u`!
z*Qt_IY)|&;)0s7PL(xgGRMvQP@!>LYxn}1MLU?GYSY$c-(?xP3;y(HpmOZ)4O;%bZ
zBcdemoRD8)WUd$sAw!~R_ev*EG>RBWAu2U5wt7zzmpMieNUp1Fw>Dj=5Se&C7gMt8
zTh?4+(8ee#l4#iRtisQPtucy~><tGmt@uF_c~TxD$*4-TA2$+<F-GADR63nlCl_a9
z6p^ZwR&UMtl1eV$9pVyVOi;;M<+HloN+RY`>vi}PWcKURlPiL~2`jdZD@xR-%p<<U
z`-h*_)T~H&cG3Bt<=nbt{biYTc(dWSxyx?$rI@)YwIyU#!>aR`>*J77s1l8%v&K3-
zv$?0F*gw*1m)25Se~acO(fyv+ej;iMHFkt)1{P19MJciQmQKnyPn2x#m2aNx=xz6K
z-^3Cs3wS)-QIGs^N5CTl(kGL(w}aYQi>}F{yD_Job7~9u(Tw+jXr_!|cV?aC_{N|4
zHcpkSzaZcAGv6k^eB<Pt{;-StW<9sA9<a!*69b+ga1-Ih9loQ4*dt<KKNh?}!q9$i
z?jPo~f0)t!C9J(|kylMnP%}<S*K2Mg;B3^Jammg8GFY;HqGWx)biFuI+*eZEBj4CJ
zvKoVa-nH?HeB;oF=I0Fo&t4#cuf3k@a0S`{&7na0<(;}e5Z#}g+7E-;8&=({puG(%
z1T*lFqRG1^<27&QwHf1wvl$;TnRSNB;-Qia&-pe^I&)%%V9|DP9sQLRp9FQ(1DOXh
zFS(7kOcZmUU^1z~ri?i^yQ|w*JUOy)sAMx7^7-(l4@)-opgGbzrVexh0-z5TznN?8
z_wKvFYj20OzjbQ=Y{`ziYs>s_cJcIV#`{p9EPdmUZ}SD;QvXPCZ^`<}kxdsP>nBEF
z<EF{73oR-RTD3@snf~i>?QNIt_cQFAp!=;w_gg{tsZ-m;Yj0SzX#RPI{oRcAL#Or*
zjlWKTkW2V(%`6j2dNk<?tp#O5wzv1>$#)zf-dwXOzrg<Opy^CUWsST%)0sGudw=%I
z@?7K7xk5RwC?Rd`#x{3>C9it*?zY<2w$-%<Yg^lEo7z_IY(CUlUAx-TQ0;E5S>5J7
za&KF8YlEkKb!~_Hpr^664K%51b)&oKQQ<H;H#9d1>+>vm`9fa&VP1V(fn|SNySx2R
z+y3@LO>GU2Hr3V$4NdJkLEpK%q@;A`PI|l5R$j4tN2%k8yR}Z(6BXvDtvd9mP~KG6
z9H$(qu6MWYZ)-SO>ntx3DryhcHm<H{sA_e$cCL2NR<ozJb#+Pe!GrFmnu>;|+Fi}f
zjj+XWf7|K@+|~cEb8lW-&10(%wY9EpXsT{JR8zZpe|x6~#_T@?or?Fj=heq<=5?h*
z{{I}LupmAPy?d;-v#q_g)_t(4p$ZywywFZ(l@LppwIW-kSleaYm96sQYhSjiqUeg=
z@&O+5{mc@|#PFJ3#7l@g4LMwR6K7>v1K})}1@iM^pCA;fsw`}FsjO1;%KQvK#mb^n
zSYu1CxFUfRL6V7fBz@B2DlZxlS6<bOyjD}FG5X%-HS#p8JStQt6T*%p*ZQV8rkM^)
zQrCtligF>^fC>P;)U{&Tn-R_r_#$MIR4g{Ur?GRB{B(q>wa7q}mP+|1JZp;$DhqOj
z$+8d^KFNezj6ZM5n`N6^>MDV)pGh&U_uvNq&ny+YHVpcf4$5neGmol264-*2{?NYZ
z>DyQLO^jaNH~!Jqgx7ne=GFHnKAOI?Z*qG0^3AQLDIw{KD`|(j`qjtU%CqljJF|4T
zO9K8E;Rc$JC#qY`z%1_QUQd6?W<bwS$@;00uA9d3XkLRX$&?Yr0`d;*qn_g?H=Xru
zd=3C5-yHI70$2q{sJ(81koRzts@NgnKXQDc=q1iVnRQG>lCz1@Hi>Vg!CGO%Bl59@
zkp1}1+BOlaT+)+HX>U1IJ}QeYm+IC|PkUhjLZhj<sk*kUq3Tc_{u^tX=osuH%QKcO
zBg-mA?GIo#&B`QG44GWjRe9%$>;1bGXXc(Bv%I9*KD+cO_n1fh#$4j7CtUjbE)>_L
zF{_T%SH4X-uUCQd$8%$pbI<Hki54`^&An4v@RI7`*)vZyjm@cNc<s{Of*xOSKmC8e
zPr@=wUh>uf-F^K%K0?Nq51a2q7N@odBz)0f=-zUtrb^2a!*^9@i28$yQHCKmQrvp`
z?3v^1&BXP#&?6f%UF<GD315;hqhg3ir-AlW{_fS|`v`IE$f4W5holg4jk<yk=l<+)
z)nX!vwLZQnAD+FnDQJC?PcKM0kjs`a&YFCiT0HTTcNe+xkD9YGR~OGVSZpf!+J2$_
zF?v&kn}ZgcLB6hE=!-0^;MWvGHYrS2xSt-baM<>qwWL<^i&joLc>h{;VY1SFa=1ca
z+k3{6YGVDnL8-CsecqC4<9}(^EaiJjNjA%oE?4Mh%x&azx*1%yd_q$@OSLnsSkfya
zVB2<=E%INK?LTmtXB%~-N7>l5^U}N$+ZzknCj2qBF~>ZcO=A1^g=~{?HvgJ=Hb!Fm
z*+RA{iLKXQB&sg&pV*h^vzfo*I)%>{BfU0v>RV<K?ujs>U@$j_J_FVFdt7w?jmwrv
zgMQ<AXnods+s|04L_tuomzOGbEPB8YA2sa#h_b&%*`>@E9+^`Vs)@DSR;M}f!{RcA
zJh`+>rJ;?zXw;=YDfH)?pQy@G65)BFkRAJny=Ms-Ns1^~+VG(9s>a7->@7AHjkEfi
z@z9;)g@Te8npCSSQs*Q|5}QRE*9~}5BnbHiG2JK2Rqr6;LtXX5lomWdFz$Khc8r^F
zBHdS&8$`Bh@5!%r_KsDniRBu<s|FhPme!#0mP?5A+VU5btR%#yd^X=a(Uq?xp>9JV
zt9+>J1wzs-=onO@;}qjot<Vs)XmOLNlHPP*SFUy^5jFi#XyUX*Np5{8v_#;vMytX>
zU`x$Fzl=<#7^x^dMCBw`kB1D2Z|TWQSCN<?cTJ0-E~eiS*OT3eJ)Y_r8uO}&C-QZ4
zeAqlFIm+ONn%+gaRV18Sa#}&37|#&$FGfo~?@RaD@4c{#h+37+fN>9;e_lp{+n}NS
z-Zwx_oN(1?)c=e3;XYX|CpL@tpj$;r<{b<v)2IuookQJyu<*@+jlM#dGktwK%(*@{
zz$}5h#sSES1yr9}nx@9ev(z+mAzS*0=0#}8`u~-c!>gm+r{UH6htRFXI~Y?VEAI!p
z2}zMxQEL8AuyWR^m~`4mMq{$T;-o#tLWrO`D|KvM-<~*s`^Oh#<T*avYqKqW;2siI
zHaTJZH_CoO-Qq=UO&@$64{}RxP`7*|=Nxs*WkGx0H69vFyqrctay#Lm={MS6Cgch`
z3Iji?((Gf1If;7vigL-t*btSA>t^72TgGIst#a{WxVKcf2vz`}r^i5*iv#x%^0p08
zuKu?W1Z-G;5rr|HxEDWr53w%hiYI)VApUk&8{#v+nD7dD`C`^YN!L9}(!bn;*!(v$
zy7p-4*tfdJVYG)DZC`!g9wMg7!28MRY9+ZS>JE&DrV{gAN-`lHrwo~3$kQI4;}B(5
zhF_r(H9ZKQdL5m?Tcr_*>WGR;0jCt0pPWYbTcSmg$`YlO%I-q_G9mUP$Y;8IUxNe!
z2~Q^VWT|LGJ~M+Q@M#tLgtiFdy|(1VzedC<Uni+-c!)_>M@WT%ysCJMJ{iH2A?Bp|
zWeb6G_iGT2uPWYwW-n45hF5o05-|xnir9(?h5SbpR{d+5L&CGe&zLfEzE0s;+Eb6=
zJ5^zm_Eft6j`kA1k{|8ER%)+E<|{3ueRQ9Y_EWlvO8cqW!S2F6-A7w%5ASbmXm4+<
zt!=7la5o(R{iU-vZpdf8FL#FIB4ZtulMPTt&U0-;$9ZuJwzaNhyFM_E+6cC<i0-qQ
z@B7yCgzhRe7TXjO?S&geqg9p2#Nyx1en?@jAD1r#dI6y3bC1n%gf9C_@nvFXZ{XRM
zKFV>I?FiVcOg=(jgY$FLj>I)ggww#o(hSWLgk<otItjwMOccU4Siv($XTi;#ScX|h
zx@^!N4&Px&4Z(7dh-5j%tlO?RIVPFk6rCjvgXJ{MT*qK)I@m@!Sf1z^4_%ax>xdwy
z(k0@=%86cE3+G!#teoHaJt+`eDnROWEx(13qclWkyb$Dx__4M!EzmNZK)OV<?xYK0
zlL68<2#WuVB3}tbz77#u-s-iT<h&4V#W^QE-+V+7q9wER=N3@YU{+HV4@mP)&paH+
zrSf-WX~=AH=4>UhDhI>r)%n@Pp)Yf%X{7nz4nArAQ$`gPyh57)+71uO03=cenjvp%
zG;i9!>4I!C(cI0OoOi4=8#+Db9Yr>@bvE&M)t=<w@ZyxQ6A^tAvv`l@N5RC`@yI@V
z&vEyj<k0ZfQ%25Zm36<8b1`jX)ot18MnNn_qBQMLk$Vs}CjDnKPX&rq#I-NWKm5s?
zB}Ns^W$d=kZknPg(t!2xzlg|Xdhho;=X|eZ&JiN6^$~TLbuX%OFUW(YsC#JNS>1id
z25~st9xwCKQj}+i`J_2rY4wg;&18Gdc01!-p6^kM+mCy9k_vu!MzccY7THw4rOcPm
z^#Yr!IGD6TC0`nk;lIy)q?E`{)15}EAtfH#KV{F;m=$Tv2I&Q%ovf?o0fLQIeezwl
zAw1jiIZY|zY$jb*l#S=_vb{pt?kr@>kFr&HD5PFma#6}k{x8@{=$#JhV6$<6#M6v(
z(HuxhZs?+;iPsfh3dQ7@fFasVTqr<!UoHfs>o>Zw5`_d+7t_r~cCMG!h0RJgDAAuq
zHz=BG2;LqU;cWmbS<VjtR<lorZP-g?Ij7Nhh-DHG-9du`$xKp@eF;`YR*peRG~DAM
zRYJF(h-$i{nUcRlcQi!?-78J`XiOIHTQQX1VFMzoumsg7XONEM_0*4t_=H#VSb|$A
zaSFuOEjc@ALSd&{K+Z(yZyp}CXm;bFllT+l;^{8P&uZzD5vN09K8?KQ1YM#%j@@b^
z+KH@??Jlc$o+d5W5PC){Y0@%)q(yYgvx;Td5BY?1dg6K}gpI&)-3*jJfkdaY%!NLN
zbBqe$KEjTsX~I~`_gknrl^9M+VY<uu801K9x_er)mMTeD&{%<A$ha=J2!?p53-ZZv
zH{?%?Q<E+VGN+tQnuVQ8_npq+0oU(RZTm+588dK=_e;se@?<0zlLh7qIIM3}gv0hz
zRQczNyBIQ<O~Eha*;S}$d!fyWmKSBD-D>E9H)H~o&0#70Rh)JrugsT_GUendLT=h5
zSCm_S9CJm#V}QEC8*_z)y25gNdm0hn4bgP8d>=U5rOe>LtevneoMZ({al!*>(YZPy
z>9axL<2x@o;G@&=wMyhT&ZRsOyW)iMG(!H5K)is@oUGm0fDKUYL8{y>(TWY2?w|&W
z&CfZWhn;QCAcAdq9#W%IQfg#A3G-^gfMjpVcVRQ<H(_r!lVR+sN21JXFuxvUHi21K
zrVt=6<T$G)K_(jzy<HDWGWee8%*e7a3+lc>__8kH83gch76PtH0+zSH@h*}mAiz+`
zJkCdFJqW9o=OeodE~82K-h>sH(9saF@|trVB#kG&W3V%%eLUnkE+AF~Y}j<qendgA
zw>Jsj8GgpC&Dl9!@Oc+>ivGC;Ld*-WUJf#_Uayj%T`A%EeV|FWu2m=|P&?9nz24nc
z-&WglG`g4H@a?{JcQ1dabdKA<QuFEwqJLwDVUOlCpZHT?_g`m9x`Exj!vXcki2;3`
zcTrthWZAKoER(BbJMZjqV*~in+)rfxT2<El@KAS>jOV_uVw_4K_~*7|$BywFL&17W
z=)NssXt|=)4z(<tpdjH4+yV4wbua%>hxAQsIX=fdG3V_<LKyn9RhDkAnJ63FVYnl=
zK5L&`M$~DngK@s-GO5LfyS+O|-#wZ>scLm0zZiCP1=%W#t<0BCr7p}hQoYe)v_6W?
zd_o*gv)Gpbc3VEAkVo*L=p5nRM_v%C<f^7<B`5y_F1k5fXeIZA=W`eoEd{gKbCf#0
zP{79=RGk+vL<N*crC?k@C=3CJ4tW91@m88cG{>Wvuv&$a`XmYl+h-G`Dve)58zwcf
z+*-unc*xw%03v(oGI_zu0+ws&GO={8Qz?mc6^~^ytiMWQNCLy1R-cnrFb;%cuR)LE
zl__FrX06_dk?y4<RYWk-gm{v6><9C=wTXHOu^d(nO^DQ$;9M_p&SH!h=Lw1P7covx
zlyf^O;M@q7PQN`FOEH<INjokgur0S@p!ULDP&0R%Bv9)gVxWc7mQE9SGZxk^>sE%;
zX91+VYTZf__LR5=pt4t;j7F}{OY4zUG%wD`SfTlTzIn$03SdLN8D)X*?W8WO$FykW
zT8%vLDOz%_+K1}b&=W&q#iHn%bi##$mLPVSrTpG?n2E7f<`?KpyxD6zukMM%@}AlC
z(oAfiGqK0CfzE`pA2YGHJA#>5Qw1^S=0Y)yiKvr+G1~&aPh5ebwkO{mEg8Ggv?voL
z=-NAA1$5n-dD=$zAgM4*)8k>HI$AQA3@91I35uYl_tXz!QA-H=@PG!W@6^hYp~k~*
z+9+@VO6rw5T8qh&F=zfLr#or>VfPwoFp)jT<GG%POAPrIT0oi8PQZrxZdn?3E*Btm
zpBt<~5ykuS>R-Wnwu8tdc%5Zq1&ZXDk(ES5%KQqC7*>qNaVo5PP2&=}hoA8#<?NU)
z80_*d#HoE)kMUYWiTlxBLhBG4twRLVA<0U)gjcC}CgByUP|~9=idPG3kSJ#D^ljOD
z7qgOvjiZqjcJetr=X%`v_yGzxNZ?$^kE0lX4I)QjiKaIv3{rOGr0Z4wIWEYLx|f`@
zEyE8A=&m<y{hgHb=R_+z3n>t)hDk^&Czj?u9xo?CM3u@~SqGfDxOiQ)^8#~)BjQ%N
zK`NJS0^0=&^B&*xI;l>^DUY7Ghhr6@?01Orb>e4)OsVLGSTBD`N1};H^Ux>Q2CS;V
z_+FgOBZT(3e$#9Fm~}$QC5#I3*5vsMLmIKrh9XlO;dzSv(ON+Kn_8d{bohM}Tp_(#
zjQVy|L7Av;Ynl&LHP*H^A8M+J)pkpLn}xf+Z8<*0{c0WC$&;|cmQ)OXF2MmG{Hcoj
z^U|j@QIyjIE8XvKq4-$sV&MUOJv?Ccy{L<CbVaKWxtCnG<V3JxQ|(T-f-9R<;y7@q
zl425DvP=rCM|n7bhSpcw)E%{H{;U|Wq<6Uc?B#u16ZEAmdRu<qw)DP|hrlMq6pf=V
z+g;t<c<5l$Lc4$csVFxP$0kgd6i1%NAIVe@i_Pg<i~jR=JK}bqSaK28elaJ-5xpRe
z#_HznzV+k#i1?t&wgx$92+(@^24;JMiI#KLZe*z^nlw?u6%YcH@L<wB2hIm+Dxa~$
zIL5=Bzrhq+kJHrlm5&gcets`v^WG&0)=e)Xyi)BRgx3}7?YVK3f*^<>d?FEk86^az
zV@4G`Jr#*mYT)eIBsxV6=yWHls<#NLo`tH{|0}A<uc6s@sAjLkRJ{hmcPZhYVygZ|
zI?9w(&5Wx00af)`s;Xr$D&>82`o2WC6(xKC!oNra!6*5MF<=pWLNy`2wFnLv=%?p>
zF(;U#l3f<W1Zv-87E9G?ov(fWHs1Z1t2oZk_XrectjT@0mHLwP`qGE=j`F^3?!K)p
zc=Wfip>`-LK$FfrnvY0<(TR5KyyH_*wjeg1nBqR@lQ0G^NxnKZF3{MJj)&#(*jU4&
z%9qx};HoWu8ynYYsc%xe3(rWgaX=F#ya$358{3nj1O!XmEwR}6PkQzt#l}m2l3ced
z9viurrBHCiV`FGMJRdAlYz$qA5_lFM-^0joZr$$j=u3bqdvSC@N@;|>d`apQf|NCM
ziY{)DbdMldoX^u>StXYU%sNDmM5u}qY#^XkM8aVUaNF{+XOFGL>4ozJbdtRkHD^9H
z&iz@^{TOsVL`NMepeHYWUZi!w4{5NRi+R8;<uQ_2PA!R57C|gM6j8#z3^Kp3Ium&h
za~Y2d`rOgyXwWA_W59&Agb#}pTu@NSXbiL*a^pR2Ycvilo%x*worTd@cx0;=?*gMZ
zG3_Ls_+eF$X1hGicK!Bc$L^=Ffis7Q?v3R-1;vtqIqri~oLoAuAl=Px%4KAQ>VSX~
zg|!A8Ei4H}fUTEe7*pZjO5dprB-3{)_5M=z2&*{H$CJsLIf}L;659R=cNA?Cm-wX=
z#%GV0_(AU<@l1D}GECq?OZ?o!Jjz3yxy`4(c2;^1;-?Jp!?g23J5o5{yAa1Yb-Dy`
zgod#%wqK5AB_i)!Ljk6~&q-*SQ|(++jx;fy&ffP{AuW>8v?wVJS)dfsb&05oMOqb~
z>6Vde^x*j&7ldT9EI?__YjeGA(7&CEQ{ru5Fuezp_%jqYO~@W`P++BRBu=kKqvst|
za<gXiMK*&i_7oI2x(0=L@op%fq<N~5Dv<Lu6u7(y3eclL^)@JQ(F7sG5eV6;(GW#s
zW~YxJe|+w1cy;h?@llQXN63Uj+v(m^67{K<9>R9Fp%IPtO7u0;4C&(>DB!0nqT|PL
z4{X{61rAaV{NUcW2mT2PcuHt)>4V+91_KsEWE&^FQ20gM+%aly@JDnxEj0H!HMdMd
zZL=b?j@lN=f#_i?ElPJmqLe?%PE)@`86Sx=3eaKZNm{6?V0tv^^Zi06TMGw;<}Dti
z7O$OxOPOR?G{QOrn#wa7Xl$r<I&5YMY@=%mIZW)&EkxhJ#@7@Bx<k)Pm`Z<dDXk~1
zU*V|4Z!4PH8xOl157oBSH`KMqF}2V>OXk;+Win!%p*ftD!Fu`D6!*jYSjjl&`$bsJ
zV7+{Aoo(tqtP$yuO?ttISRR8%r5AG7|3c$aS{!n^LTFO=@qbG-79b(^%CSQ_^OBCv
z!jzr9v>S{7=@Mwr1b>ShOhKbo^%tDX+CA`a3Pd=ildO;b8ap)hUZ6d)Y%~j-Sb`Mz
z8b5>DBnWCaErPsw;!}<c(Q-xet%Z05ti_)R_(b!O#5b&lo?)WRsa*6zOQ!kMiXZ<p
zFZaEoms1yoY=Xw&Cfq4=;(Nt9eR=BchZaB6u=H1*%M5<6p_fVT^QP~mqDYH?m51*F
zEuZCQK2eqhpA(foS9b{4MAdCwe@Nq1f5BgLnZ26c)M@@fIz^-w`{qG>r^x&2<2mCM
zv}sOG_dm)Ml^*@3KM5O@dJ^)#alZtgKjQ=Flzvx>uleWnKK>Ij;5)%k5)XY*4R3!z
zatKjDRx;Wqe5fBNU6l*m06h(DxJL@II6W^$FI_+<0wE=!W9ua}$)n>?eo9B(Bk5QR
zT6&C5<sSf@>WnQy`Uzc}zYTP%&y)DX^`Ub7pwsp<_|S=q^Y_K*&wq)27Ido51$-9j
za~^amKa9^p`NN=7pHJbVz$Y&M=b+Q~I`ogOBZ(d(d;@~N2^!|^Kj_@;-(TI_)YhIy
z_pA6>eO@zd#eM<N*m(G0UQN}bc{R28l~HT0)IL~yu&uT|&tqvQ&TA-IBPBdvdeO5`
zV7yPYr!(4TVMpmC3F9rS&}iocRfVL^-DF!DE|y=>`-S@~#R=*6PaVZY`-|4x>-OMx
zQuiKoS2wqH<l|>iMR}I_pIhyh<VJt!vH#0<MhRasRO<2NS6UJ=?z{PJe`l-2Mvawj
k7FsJ27MLrw7Zev#yESI8)L3Zoerj^X{;!@$%rGJU4{Y%1T>t<8

literal 11968
zcmch7eOwb)*8iPMm;{)F0fGeZWdL7LQ6~xVQndyWC~CAQNNKg}L|#M}Fo;sDeHjQK
zD!S3K7OQmwRTta3ixn-pcAG%7tQ%WYT5)SzsFr2-@v&HKS9jg+bM8!h>F)E#^ZEVp
zOJs5<bMLw5ocq1sbIy%ly21kyyfpCVoQ{wJAtKG>`ZAhE=pZ}^tYMK1o`t}lqB?eG
zYL9###pqLZ5w-LLKV`&N`L>mUHeHssD=^K&=rzeo?YscJd3<JoBRbZzM4%(0*Ns>7
zGz70~bG8}Jju0Scu@<4_@ENt$sJw`-*rK}r1+O4MUToAdH?q{Xxu8-M^j((vnnQg%
zOI^yVM|#zRMzxSqOV09|Qc&%z)266q`|MiNtR_>Gt9#Y~`>bA5N{=b3iJW!7Gz;Bf
zgTBvFy9U(X_EJM^&|t6nn_g;UME#cm^_?vBcfHg%F7;n})uqs3Kwaumf5WJU5OZ@x
zUFuNZ<kh!f6bdTElLif=W>a!|_v|Lp*x5a+qk2}Y9dw9lCTDk~&Z;HnI7wbT=)!s;
zUC<pyeXU)Ml^?+qT{8xK%LbLQ>hF2=kT~ychx+f(b1X8?>Fl0eYfl0F|2I*KgRtRT
z(6_w$4k+VNf6J)vJk+G!t^E-^_9_}L{K?1=?IrA1?7?wpwaKbXjWkAW%?HP7615E|
z-gvwvvxZd}!SVCJ?-ckwwAR?n(4q3yW=0uGU1KKF@+B4~gxJC&6a&xoF%AA~L7hA_
z_CPIMuGO|UG$EG8#=u&Sg?ZOKn%E^bhRDZzg9U;(!)~pKQ|dDiB@3t?KQHavXd=!V
zEI(rm5TYa3of9<j)H>tVR`#$qb1`Q&<peuw-i=}WtY!^yp?Ioa>*_Z$o{v!0IDfHK
zF3Yqig`UYMAf$$EO2B$1yyPNh-SwO0v?nSRRf3{2ZgXPsW}9~N3(bm`8pvduJ=sAf
z33gQ>IICCvqPTvQM#YP~Vm)|GP}rP`a#m5*OWhO{FEWZsr=o)OJw3)K)(MIyg3Ot0
ztT{s%<7F)K2xLUa#rzo|@PzoPPYz^6{KFmR*(e}zA$|$bi{yv|pW+u?J`rgHq&DA>
zO%S})My7p%sGgK=v|kq>j*;3fW-}=a`a0Dok47|XJN)82gNRR-+CuaW#bZ;rVD0cm
zgjbJ@Kq~muk8RdO1X~=9{u7@%D>uc=cPisD(+;J_&+tE`cgzfNI72f6cG+UdJ@Z=W
zpy{xq5!wg_d<t?RNsA*x7HWP{aBtf}H0&g_`GFO)$fHwV+q+;>1-YmEX!%YewIy)Y
z-c38Fteg_?#+1LmadhWK-GYk1`~`$SAo$l{)rX%=44+6|)1UqJ;F{l9%5F|*ym@5d
zjl!D;=^5{;b{r|WSvbA1bh?Eqva|Gkexw);74W|w8txkY>(K9q(Mlc_72tn7es^}B
z_SPLeU-t)Br?Zr4tPY{~(`r`}?Y*4yX>ZnrJ`M8LqZYY+lAYuxkhcppO`e<yOXbY5
z=&VHLAKoJ-t3e9tXA)}p5if#vNiqHhk`tLAU>jLO1+q`drnpJu?U@r_S3H#zOFrI4
zjLAeIl7T-&vf25#ZF<clqn@6)%FYEh@*^wPV6hM1RqlZ^{iyHY$qR!oT_C(3<dWXK
zn-1@NZPUDpsQh<gr*68}`bYcJy_@d6y`bW)?t85jsh_jU$vN8D5s|_Z@1N{2ysy_g
zbRAp@Kx;I-wea4jGEpc>8Ax`hJS2+JX-{jTgi{Ggry};uctY5NyNK^sW^AZfH)C~K
ze#wS{!Wk>pZ?qLw%viBub=i7@e#QFf#ZmIL0}A^j6Pfkr#Mdi_ax<u1Lm2=n4h)YK
z&9oh}g0=m|_2U>Ss<Hl>M+mj6GX0PXV8W#)*Qi|e=9oA=I){)~*znMOOY0TkLm7#Z
z{~q2TCe#4#`-uZX^N&@d<Q<<2IS3tq{SsPxxZmL<QV$dD6ymAnq;~cmy^s>oJfovM
zCE;NMmP;$ZTeNdeWE6bvZC1%#rN$`;U4{MU-?gD6^G|~FOC*qpBZmljza_%8kM@RN
zS@x!O*`BM*-i-Q>d*rgHjI@zP@D?oFRfu*qo~OPhkglIa745`fh=C+R6P3%~i{44r
zyiK~)$VDeBxGH@is?c*Q)~$VE-P#Rh1wXw(x)h{?HwSP1%tU<ULgi&w90Nq^r-VZR
zc3ypG=WjbtaVe+tDJS25B1ts-Cto0;`QPjow0l&3oT38$i3$#g3XVM%eTA&~E9nXX
z1+|o@;JUTzOOSX$iT|cgQU^a$P>e2K9R~D1+Hz|W=@#%brDMp&{dk2Mff+*OTyf%f
zr!ngQYLcO5;x?k5K1B12sG*<V*nZ?U=NH~Q^6~cnxJSkziiI}>7|M9)EWT2!YFv|}
zc4f0|PoOLU@U!V5e$MR9c<Q6v+@Xx!qlU!&_>(V?G4|hJWHcO0Wymse34z*yXf2Gs
zz|<NbKNDb_ii8N82CO?LQp@#oH-6uLad^1@+_|eg7rU<h?_Z)dD-nM4@Ge+W0@pPK
zi8Pu-ML9rv9zuK#6CAbc8MZAC6@ccveH~T8C|+<XUgZN04+I=*A5<zQwfY%2yT9yK
zd-SQm*9_#*DI#@#&h>Xq>z7Sv)gL`&aEwnnmc+cHKY6kv>3x-b+Vz@g7Dl<*Kj$K&
z%--{S#OL+a@GAGH9xA`YTDFR<EL>NydTkkNn4UOY&&I8{uBw=^B;Aspnw`GFkf@(g
zw7Se%GC4}Ng7ve9lc8jL?rsH>Ur|wE$R|kz8*Q_}nLLWC(sBAIS-Df{H1NYvVlKrQ
zva?Ou6&1J}i@Pnt-E^p8HJZs847#M01jI!tE0W3ibSChc%Yzy|-9z+W^|-FPJV0$F
zZ0{f)w<DbX8Ev73yf-73?TJDk)9M}D8)-H2QfXs87DC8eER{n)FWgwMeqEup6zOKd
zu4n@41gC=A3y@9pI^XOX_yZ=){@xPhRjX-49p$J*f@&-fxUs!EBI}lmqGnJO<x;VS
z4pFE+1m=ZEYs8bO@%}}0C{PCwgrME4N}W@pykRBNf>8SxBp|wBV=@^quHOZAxPW#%
zef`*gJ79orKxUsrG1;$?HgJV?K=C!*=^EHVc>2A_i##RT`_;+hbgpV8(j^*@0qLVC
z2m51nAiZB}Y*eXTDwnrDb$o+?C9#-%JIRKU#$#62f8}^d&ef|Rr>{h7sd*qLDGB5x
zMo~@dq8d>St)`7&MTB;?PH5g6B}7CBdsW@@naM}3S^hN>dPIE&T&U+dx?ZAPUQ_Hp
zUs^1zR8mrsJ~0WeRdci7*0<y$5Nrx@eNA=)USG$SXPq7ad(1++B8`pb;nirti&QhQ
zU-&vsTHa2=>+S37?duhNQ&OXf+Yu=ZdG6USN58rJ*}N#D%Imdwx1XnBsB97pedJNk
zRqWCAFlsSRf(|6<q?k|<UIYG#PII*iWYM%M3RVo(Dp*=8^oGj)bP3~<#V4|N5LyOX
zt-X2#`g>|<(Zdk%fuFtg)$z(i$;GjDk|UYWV^%J(HC}QJ_@xhddP=mtHOYZ`ajo<z
zXeQDbqNwBSMM;#`OJh;z>#L_d5M?l6QQ60=w!qeDU<$0d*Nb`vkf*;yJ5W;<xWu<7
z3d?<tP69HIQl4xex5i3FIw&3j=do(%wq&r87Hvdh1@I6(38FLtIKH8cfE5)3SF@_;
zc_e7BVn`}~*FXl$00S^2hl&1P5s@+KxYHsc`PZ;+6@bXV7`2F`{_7Z!1Axey;Xo0Q
zNqPX1E+vZUWxp0Ml3d%tMgiQFn$XZIim_#b7#6(6s(fOu_JNolaF)d$rxKl&G!yBQ
zksh4Y$1bu<FcARVfRgPNmAIE@F0Xz7lL6QoSFc{}=@U61@0z+T#VLVKkhmw-B!bSi
zJ;yoZ1D$cKB+YA4VdNy<5#Atue6x}BxmGV?_{v>!jXGHZ<n=R1L}YKT7yG98T2Ncc
zfHak35}8FB459h3Z^8TR+vmbup(0w1U(&+)g*2`Hc%e91(vL9NbJ9XqT1z$*KA2CB
zm+}kFZ$4ct&F5`7xChcUya{@}19-}+ZcW_c;jXhqmxt0ORu1WNlO{OpGD=D+OQ)Bv
zE!a>}IK8L@I61q1S&!e(+QfdlG9Zd2O&Ia><<@%mG$@79p25*Y8e&d^DY>@0F-=fx
ztWs1om(x&I{x?)|g4#f*jqP%e`M70t5$7j%vqyQ!IX$L1jpQ6}RpWY_Vv|y_F>|xc
zrg+gtR#t7cv6~~j!Ri|h^&l5i#sys)QIBM)4UA{Zm(ip9qsMev#};v0W}OyG;SO^4
zX{e8(TprO>@`_ExilpMr>)<MEwmCN2cqpY5m3RF>><hx?70S)!+Rf{lH*ajNj)x-n
z=79Qpm-+@OXAznK_MAoY68~w^FbmC^lpI4I8Ju!yCE530PU9y`quKJKDfaX)hC3(E
z-nH;wHOI0np}3DL=E|KJ=6=H$C!&q;eV~3}U}^#>ODJ+oTX5zs?N$a2%}wa~N6_|>
zCtI&gMEFY+f0vAoH=6rpu~+VlOUb>Sb)H8%3NFnppJOy!J@IW`7kocAIj5c3X_{#t
z!-7}^J0{nanfTAp%Va`#X%sO51_ponA$zHVF&kJTY&&EH8$3AglrM?L)fWYS@<zny
zWLW~?w}k0~b~fXec1DTNEe;`w|B$0{tld9N+vJv~8gOGDG)#8?F6{xgyoK)LYn(?w
zBr*g?4$_8Tt1;PQF>4vMF0>{1V=gq9sx^7d#kB^nxse#u7=jCp$!9FJ8Ohzed|j}s
zp_)KzM*a%*I{9C433?kYbG=%ItEN^VI%D)GqEV|wPU<&M;?H&BI^X$sxO6uX!J&mV
z%Ei|%R!Ks7u@L)T;POz2-YN>wXnaE6#X=m93(<uZVIgvzPe{8cWcYC*30R1v#M^lM
zjeo+^2TE8&{}_Q{DGIfvV$Flr!)0z8o`K6Z-terWT>fVkX`zP_dT=_2!77Ssrw(IL
zUM#BJXOBD78-bb}5#-mCcD#b>qhu64krtk<k5(4Z4ZlkM7_oKWm$}yON$x6>%yU-c
z)zfJ(&3#Wfg(erA74B{^3@iA~Xu-vIq2@wu1CPJEMhk9b8;#%wZEGDTJX=%Tg|v;v
zcA{Cwo|WBG@VlMO98yLYC{Nz(Xo60XkBYEp(J`6|feG_<_etY9=-QJO;6EUnSVSw|
z<I`m97U*)#zZ%rYf+G|3;@L(bb<|UtD4f&f8y)GvA+9RBhH}>uoHm#tu(lziLn$;b
z|E!=5oH||z7(ig2TRBB5_>))#P-dmlUw99OJJ0AsjD7`Kp_I#J;wh_W>-hO#tMg1b
z<*Fhpsa0^(R+kI2q;V9;-3W5Cw*405UgSY;uw91CR`8tic-(v$t78q6d|BoMqA_WG
ziHpKF%kj-irM==!G28&mi~)8AOfFg6B<B`5p;fAbmUi%@8^KL^^*;Ez9qhioJ%Wsx
zzP|}&(qMLQc=mkMtx7Y3DD(2!lL@b$%L4U0XKW#8j~fgdPFw9SczBSp{#J)PD-D4H
z&&N$8ayZ4zd}D9=#SpMFOChak!Xg;ko8AScbw~79kAYDe+#krf{Y(#d(^$#@98PKN
zucJ5>Oujh0cqGK=PvBlUY6g+xR2cG&eRbN?a&Bc7a>Z-hxYI`qP=W#=(jNHN3BoNZ
zY1sZG=yfAzlRtl&P~Ue2fv0{q@H3fK$06q^DjGlhy2_v5?b@SbZ?;zX3&U9b7h8_X
zjW*Cg`N7>hSzNRbL8i?}*o~$r>)z0@cVhB=2>GBYPo`blPA*XbGy=M62^(xz3Vnf{
zaVN(5pjTX;%=sh>t6Y`Ff?GAU{^Wox29_^Cy`MwV5x`j67*~UuIaK7oKZ0C2gW8RT
zgG8S%n~%co$Y7K`xP_rzfU^bdpkcZ00Ib-~fTKW2lz9cc3UFtJsSnCv>iaRtBybtY
zjs||K2F^N>%Wk(_dtG4b=8iFUM~x!Q!Gfw5@h3{3rI~b;$jF2%?{5eTcK4s!IHAWj
zXJ>c+@3#9IA3Uqseo5&G)@BZdp0_dc2F*`ipkH_;K)K|u+0b|V&4`*yIWN3Sod4SV
z<GRdOi1-j|M20ae@Iu~}i^<!KcU_!$cad^Y_7^8k(z4sl=d0<<p(%~i!eqDm-XCO*
z8bYgIURfj086>-zh@5Ed=_7j`GM{?6x;S|yJ%7;r$^f0W{a3=V<eeXm-n9a4GxsO1
zN8JN+v)3cP3zp!bSxWu#r>}D-TU4)y?)gMW=t^O+w*0lq=**sJadn~hYA(^oOXC(`
z#jr|6OX<wQ%ehNYH-9O~Cc33U`IKnd4+qg=Ip1Tua(~Qd7?>HWeTJazZ${CeTdBU*
zHT(SwjO_NnWrsK_``b|&VBND!H229XLD)GLm47Rp?GIk9r(ZAAnv7xLR<p;Pem;T)
zY1IavN-)dwCvL9AYSer1Tx2xLTexfwwmQ0d!=)1;><>9+dG?=&5<tE5ZXqXerP-51
zY&$I9o~{Fr^&6Ea_jX22oO}qJ_U!ytra2*9?rP4F(e{5?7JspVSdzSRM)G<7sX*W2
zeh(PHFDr{s5qyTqQ^mL_hqhT`uGY}HSTrF^UI_O%9>ReDj)x-?m48zBLY)}NYTFqx
z2z}Xxg8+wvz+KGku#>&+NUsbyFplI_@<^B@2ADtMZm-~O0NDzg;uy-p+xm&DBBB#c
zb4Wp{hfVC}0%2!3M2x!`1Sk#zmTM;qM+pI=_xU!6vlc{Daxlk!CIPk*Z|3B%8$`;!
zY24%Il=)Ahg+RQAdZK~i$I!=6<0Sb7k(g;r%)JKK&$D6bHdhzkfWXV>jh;rLTG1U3
z6rVcN3V~Q|LZC--zVUi07idgo5Q+d_{9w&{lB0JXW-bPQksB=kAuaQ%1D`9U1uL9b
zH;}NjbShlK%Eo34;3fG3J7%X_0~_NXgvM-0Z?0pYT@;*GzsrZM&wPz<CcY+pa|>pX
z)`u7KmWAT_!1hJvMx@D%*32g;O|Co3ATwI3vve9gl4tO8oY&y>!UxH)UJOoK8r||}
zx(BkAUrLEgmyLp)<*{_-u}nowSLoVoIzt;OMh2dG2M6rl`><yGg9Icf--Z1hEoCu9
zPH}0ycxey$mi9ZADgoy)!9F2k)OS5DL>IIYgy1ZwNO%N|2jjoDwG$$2BKF})UEje)
zN^yYP=ERkV$plXw!n!p-F19)-FbaihX5n;$MI1%!GM>XLo@yomlY)H7C|7(ctUaTH
zwRco~EYp@LM<-yOjgXHArZldM3*@=hW(u+frT>I!kTqDlkaHzqEjsv!A7mhz#W38f
zXEH!ut$F7tGzPHA`0Mim2V@x_bZ75pGPV%<$GDI9Wu>MAH2oU!Z3_(lvb`8*246BI
zX8@|HFt0MwK-FfNe@-w7cyQZiGA<fH=!y=x@Eqh6upJsaM@ONh1rQRRRzjfQxtL@b
z1c>Gdae&viaZCv5e-4f6Bp~Jp?uMySUcrMgX{~vI{O$p0nOo_LGPVTNV9Ve1<K0?8
z3^Bbm1gKEtUlT#f#@8Q1RBVSq3$d+ryyFCXy$d#E2c#uUp4+1!P}?ZU^f(Kc-sI^W
zh04KnZcF@hAy5n9((?7zK%q;3?ebWD6krDd&1Oxwa6A>kJYD1WccSS$gk)|@%ycw`
z)WcFul0&EjuF&Fb>4<2ATyXq*ohZJUWI&qeg?*l|aCDT|!=baGGQ1=>aC#_EAlZNN
zbo7oL$zhYvn_W&UcflSm4@qB+<ci0=#$m5HleLh8%rEeDs}6Z)Im&s|O{l>Ni~$8?
z6ApADZ;%Y<MRB)0el{W&57d+sj<F6{h1t=N{ein(N->S&!Tu#H8v=zNaJn#|`~z@u
zyyWCzI}gkPKmwcNwhT@~-;uDY@5;LY{se(e;~A#v+6e*VFOZj@TKGW;&dJbcO>Fn~
zW_A9h#9vB{uPS|wKY!+H-2TX+S#%wu@aKp0N^kyjg&6fF+9e8!$ifloS2aNX<C4kT
zuQCou-+y{?@?<H_&RqMHA4ea5MGBf0Xm41nlR{_bAS=fG;j;!v75pLQ{(d0A^nBEo
zx1`{Lqt%cJb@zV$nveD_Ct+m*7a96;A4JT%5jbL+4WrXQho=)v3-{(g=qz2~UYxx1
z7YQ{l`_!mh8xLXhM0uEt>;K2J@nVp@+EM6xdZH{g;~J3Y6^k^{FZV8z8pnTyB-4sG
zh>0%<FnjEF*WRoeoKaY|FPkSc&vR&(NVgv>OLsP>_x7Jh5WD3&wrIBo(WZj%EouBk
zO)#pEL!^eJqW@(gQ?%4x7nT`&btWu>__DGHg+Io_xTf^+FfRE;&czMj++K*0iK&@n
zS&f4lgP%PXFD>RsW|1y*Cxsc7@fXR_RVOmsO<*|kE4Ty!48~QJiwx(g#?PFOKdT)#
z+V||A_uv`-_%qKq&iCvderA09nLG}j(HV3P&gc&ccl@{ocyA>D)LS+CKg4yHT!mpu
zRpYvAiT3X@)(%|{8L3wZ2WHFcD*K1X;%|n{-`o{>U)mA1lO66Au;0zFZyL1>>h%LU
zn{0WN=+)yPwjX7k!cN%rn&uDD*{D&Ifo`Z+*-9L0*8z1|13p?I?eFHaTj7xSXZwkv
z+$JTq9B8P4nxj?on-5X^T_a3FXIR`gA|I3E{63(21?0h@iMX(s!nP3J5DjDt3xO4k
zb*mDD!FpF3q`mxZw-HlZSbZ-jF>&Eu*sCp(D&8X?lz^?xiOV3HCnSSX?}1X)0hf!>
zD2K$S%J@fhT9#F-;yKxW;oy+xcOU`p=`JMF>N_L*C<qSgA7jXOyRstDYEXr*n>15m
z$h?+$D*m)J(2kji2P<$vRTH+OPhv#AE@mbaDZiy_fOu<kR+N*4^LwpMPJ-o31k}i_
zVI6&_0asra0ty|GLQ5(OmbHd;vA!vuOI@JiXIJC;BMnn;M_1$lN+d7y)B~w&&^1-@
z2(C_zZdi&8Isj?wVjw^~*OIB?cViY?Zp~B){g}nxvAs$0)ng?Vv)Lc9SYF*=0@|lz
ze-_;!l@#b{z`2i$_^;l_JP^B`znmd4SoYr%*RkE-gkD~+gv|xT!s#&I)=qrc5B41p
zOZUriDcMf4iDPa4()XsdGk_U7kBpc2>VzNEAon~oKmA=aY|s7^FGB^PT?j0<@F5k%
zDWy!?9p_7oizZ2|SoE66qS>GOh{Cz-3>)kymG?}><pAX28%pPp9G$UFtRo6yNYk_v
zZ#^K)KQNiGHxyaSd5!f@b*B6}(9xa%iC9XFex_;1%hLQg`bR_h%(Y1Yq5{vn9QBm#
zc}!3^@g9>}G>yEd%uQ3e-fLduBdA}cO7yiGvx$`JJqMrv$6S0EkCC{AH#?*>e7Ts0
zci^mO#FvJ*xg$GeMgkVL-&pPkVT%J~JgQ8?ASe~v&x8rLYS}#;ii7_N;_@>CGQ*5X
zR@59U0MvQ%Oc;6&g6bf(Z7PoKaF~P7K7_yqz|fSovM$8M;+(}zZJmlVu-(5_jd}*+
zbj@mCoDOF&n4MqL5_|?u0%}y6XOJFX*U#Jha8ViswoEi-espnJI@7OskVo6s$LB7A
zV(Lnz9ts~Rp&lb9)K@G7ZCbd@5}my8%s69eLU!$yOlj28WlH$6aI#czT`ryBYm~*;
zu8%)?oN;lY<6u53i_m!Z1b@%Q|0zPOapW`Gp$UFn1IKy1nU(zd%l(*`#Z0)*=hw#S
zh^vI?*K_<SQlyeeV9+_flN96--<yf`3NgOpQ;lY~O@ThvGOL)Y1fzx`3&)Bg>vE_e
zE=UEzQh7L@7r(45{6-F+4{(5Uc@O0LX{nlw$xY_fO~%EVr-C)6jZLX3O(5uDeI}pD
zVI)1&T}saj#q`|t8*ITrxZuibZ^Qu!6Q`!&l{dl}#uHP*P$aDJh4RBVAG-vt(!(e#
z71*(iUP3_b*#<llYR^H#Eac$7ro?WaLbrpdQ{bFWfg0V5X#l|m6%0!Q^8f9847YY@
z{bIhKFbaH9wR{S|#|=k6Rm-NJKA^L%C=dt<UCCKt#KVT67ct6?fIuj}5~14~M}Vur
zO`xCKG$!z4m1&BEuXjX^Isj>JEg_s+z@!zg2SCl(eqPIrdp!WsWjFym$716IVEZTa
znSR1_(BP#K5LlJg3*EkoJRsv%+K_AX=rcG4`wD*aEremnF8ag;!(0L=o(RK)R8jf}
z4C7q~WyUeEom_(C78mRgWY@t2PvV|#EOtLr3!WgT2kLK<)EC?^2f)C}9FU1HK$Bs;
zidJGA>}>I!eVlzjIvw{gg~4gahEk)CQ%a?ykm&BEkCM602p^el@TGB6B*Z^c8t*%F
zD4qUbGlaPdIjJ39ruTI#OYn6oOZ0UsOZN3y`-HDg5U45QvK2o64VO*E;HK2c8dHiU
zZE;h2YLj`RCS$b*K>L5fW%rTCad}BQEbXbc=Lh+4Ic0v3h|9(0FZyt~xb#H{muu)d
zxF*853?b)8xI9RS-2j)14_1$T9G8n#Fbw1Jor^eo$GF^fkrZ*6w{NTumw9`~O1O*!
zff6p;J;oprm)64|P{L*2YA0;&N4U(hkCkxwwx|)tW$PUz;_{haD}1;N|FuHIW#>5~
zHV)%*y1thbak;z%1WLHP961c7?;~7Zb}B?%x~7O4tvxHa;^v@YT#bD87XqO6612|#
zg%Cm64g$eAWQS}g7W+i(Ci%n)8;HmAV8wli<Uw&b+b96b292<`5+3>gUwC{7#xSDj
z{|S%3dkl}5zs*gic}*ERALZlnnZpy6YX%lFeFJ;hHUfT{_3@*nHd6elM*NkgjTmI?
z!En@rf6;j90FIxhappbpH@Lu0E=Qg2agb+rr%4^&!W}w((xG4MP~+>+iaWgflMaq9
zEFsm`p#^t1@RJTb&>;b5c#D68+z<$9;dcrYfy49Lb5R^rt!C3d38Nn{&l~?8gaU8|
zSo|vLV_eY4dKHpy4QluM1a4--x4|RO82>8#UpC<H`n&khfWcX7as6D>0H<NKZ{5ck
zppM;lT>|%D&a2{4oO1KuNntz?S@P%OkOqo_t_we+HhkXQ)$$|K>f(@-#%yidKNtN~
zSp|(<b5UCiNHpEY6}%E3vm|$qLpeANcwoxYV2Tw?sq&fP!KOrkDf@k<+<IWjEuSeP
zRH_zy@X2k3aSZW^mcbG>VhIg%aRFgPVAra<q~H;tmjfR9L82{yE^#!35Mrs%ng+0@
z2Y2cH!Pli@E?T1mPY7*u#q_twZd3sk4BsQ2JA_rVGVUHJe1=Cbw-j*3#lrs$BM8;2
zXaLSx{9eVyIWFpQ&8WM5S)Fj9D4IY1yt27eE35pRE>F2os;@)w+e#-vCV4g+lD+Fv
z()d|9-+}ARv5MS(K;isDIe!A*vWiN4Ta*JmM=H(B7xgVWXG__62C|gCdYmivs|lJc
zo8$S$`~=J@aj+3SA8;^~q;Ou#JjS)Ey=-v=U|jr75-#@OG@XcA{$-3g0b@?^!P@%L
zA*iS19<kOGZsD47;LmU&zl00ap|vg4A>_cndKBpVgj%R3*rv&7f;<Tt+a{wNd`xo7
zLWrkhnNiI$K9j*^Rw|hdKDM0|jI*=R+saC4XtKq0&*9bxHWqYN!{4ZwWMA@AO<xR-
ts9!<^ri;H0v}7ulSTF^Z(-)8Sf5a}XUaARe&#HY^bFo?z3M2pX^*?hi$QS?s


From b73e82f0d82e6b02efcb030797ad4b444a68fc1d Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Mon, 19 Jul 2021 13:39:07 -0700
Subject: [PATCH 4/4] update crucible to ignore old dbg metadata

---
 deps/crucible | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/deps/crucible b/deps/crucible
index f2abe5388c..708719b32c 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit f2abe5388cee9f717af7a1dccf956a6896b47c51
+Subproject commit 708719b32c43a2dfd63a5b357d96676fda7ba4d8