packages feed

copilot-verifier 3.20 → 4.0

raw patch · 13 files changed

+264/−68 lines, 13 filesdep ~basedep ~copilotdep ~copilot-c99

Dependency ranges changed: base, copilot, copilot-c99, copilot-core, copilot-language, copilot-prettyprinter, copilot-theorem, crucible, crucible-llvm, crux, crux-llvm, llvm-pretty, what4

Files

CHANGELOG view
@@ -1,3 +1,18 @@+2024-09-09+        * Version bump (4.0). (#69)+        * Support verifying programs that use array updates. (#63)+        * Support verifying programs that use struct updates. (#57)++2024-08-03+        * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)+        * Support GHC 9.4 through 9.8. (#65)++2024-07-30+        * When using `Noisy` verbosity, always log proof goals related to the+          core correspondence proof, even if the goals are trivial. (#51)+        * When using `Noisy` verbosity, log more information about which proof+          goals arise before or after calling the `step()` function. (#52)+ 2024-07-11         * Version bump (3.20). (#58)
README.md view
@@ -29,7 +29,7 @@ * Ensure that you have the `cabal` and `ghc` executables in your `PATH`. If you   don't already have them, we recommend using `ghcup` to install them:   https://www.haskell.org/ghcup/. We recommend `Cabal` 3.10 or newer, and one of-  GHC 8.10, 9.2, or 9.4.+  GHC 9.4, 9.6, or 9.8.  * Ensure that you have the `clang` and `llvm-link` utilities from LLVM in your   `PATH`. Currently, LLVM versions up to 16 are supported. LLVM binaries are
copilot-verifier.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          copilot-verifier-Version:       3.20+Version:       4.0 Author:        Galois Inc. Maintainer:    rscott@galois.com Copyright:     (c) Galois, Inc 2021-2024@@ -41,20 +41,20 @@      NondecreasingIndentation   build-depends:     aeson >= 1.5 && < 2.3,-    base >= 4.8 && < 4.18,+    base >= 4.8 && < 4.20,     bv-sized >= 1.0.0 && < 1.1,     bytestring,     containers >= 0.5.9.0,-    copilot-c99 >= 3.20 && < 3.21,-    copilot-core >= 3.20 && < 3.21,-    copilot-theorem >= 3.20 && < 3.21,-    crucible >= 0.7 && < 0.8,-    crucible-llvm >= 0.6 && < 0.7,-    crux >= 0.7 && < 0.8,-    crux-llvm >= 0.8 && < 0.9,+    copilot-c99 >= 4.0 && < 4.1,+    copilot-core >= 4.0 && < 4.1,+    copilot-theorem >= 4.0 && < 4.1,+    crucible >= 0.7.1 && < 0.8,+    crucible-llvm >= 0.7 && < 0.8,+    crux >= 0.7.1 && < 0.8,+    crux-llvm >= 0.9 && < 0.10,     filepath,     lens,-    llvm-pretty,+    llvm-pretty >= 0.12.1.0 && < 0.13,     mtl,     panic >= 0.3,     parameterized-utils >= 2.1.4 && < 2.2,@@ -62,7 +62,7 @@     text,     transformers,     vector,-    what4 >= 0.4+    what4 >= 1.6.1 && < 1.7  library   import: bldflags@@ -78,9 +78,9 @@   hs-source-dirs: examples   build-depends:     case-insensitive,-    copilot >= 3.20 && < 3.21,-    copilot-language >= 3.20 && < 3.21,-    copilot-prettyprinter >= 3.20 && < 3.21,+    copilot >= 4.0 && < 4.1,+    copilot-language >= 4.0 && < 4.1,+    copilot-prettyprinter >= 4.0 && < 4.1,     copilot-verifier   exposed-modules:     Copilot.Verifier.Examples@@ -116,6 +116,8 @@     Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge     Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap     Copilot.Verifier.Examples.ShouldPass.Structs+    Copilot.Verifier.Examples.ShouldPass.UpdateArray+    Copilot.Verifier.Examples.ShouldPass.UpdateStruct     Copilot.Verifier.Examples.ShouldPass.Voting     Copilot.Verifier.Examples.ShouldPass.WCV
examples/Copilot/Verifier/Examples.hs view
@@ -41,6 +41,8 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   as Pass.ShiftRTooLarge import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap    as Pass.SubSignedWrap import qualified Copilot.Verifier.Examples.ShouldPass.Structs                  as Structs+import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray              as UpdateArray+import qualified Copilot.Verifier.Examples.ShouldPass.UpdateStruct             as UpdateStruct import qualified Copilot.Verifier.Examples.ShouldPass.Voting                   as Voting import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV @@ -72,6 +74,8 @@     , example "Heater" (Heater.verifySpec verb)     , example "IntOps" (IntOps.verifySpec verb)     , example "Structs" (Structs.verifySpec verb)+    , example "UpdateArray" (UpdateArray.verifySpec verb)+    , example "UpdateStruct" (UpdateStruct.verifySpec verb)     , example "Voting" (Voting.verifySpec verb)     , example "WCV" (WCV.verifySpec verb)
examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs view
@@ -19,7 +19,7 @@       stream2 = extern "stream2" Nothing    _ <- prop "withinBounds" (forAll (stream2 < constW32 2))-  trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]+  trigger "streamIndex" ((stream1 ! stream2) == 1) [arg stream1, arg stream2]  verifySpec :: Verbosity -> IO () verifySpec verb = do
examples/Copilot/Verifier/Examples/ShouldPass/Array.hs view
@@ -31,7 +31,7 @@   -- It passes the current value of arr as an argument.   -- The prototype of 'func' would be:   -- void func (int8_t arg[3]);-  trigger "func" (arr .!! 0) [arg arr]+  trigger "func" (arr ! 0) [arg arr]  -- Compile the spec verifySpec :: Verbosity -> IO ()
examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs view
@@ -8,7 +8,7 @@ import qualified Prelude hiding ((++), (>))  spec :: Spec-spec = trigger "f" (stream .!! 0 > 0) [arg stream]+spec = trigger "f" (stream ! 0 > 0) [arg stream]   where     stream :: Stream (Array 2 Int16)     stream = [array [3,4]] ++ rest
examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs view
@@ -17,7 +17,7 @@   typeOf = Struct (S (Field 0))  spec :: Spec-spec = trigger "f" ((stream .!! 0)#field == 27) [arg stream]+spec = trigger "f" ((stream ! 0)#field == 27) [arg stream]   where     stream :: Stream (Array 2 S)     stream = [array [S (Field 27), S (Field 42)]] ++ stream
examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs view
@@ -61,15 +61,15 @@   -- Check equality, indexing into nested structs and arrays. Note that this is   -- trivial by equality.   void $ prop "Example 1" $ forAll $-    (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)+    (((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts)    -- Same as previous example, but get a different array index (so should be   -- false).   void $ prop "Example 2" $ forAll $-    (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)+    (((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)    -- Same as previous example, but in trigger form-  trigger "otherTrig" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))+  trigger "otherTrig" ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4))                       [arg battery]  verifySpec :: Verbosity -> IO ()
+ examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE DataKinds        #-}++-- | An example showing of using @copilot-verifier@ to verify a specification+-- involving arrays where individual elements are updated.+module Copilot.Verifier.Examples.ShouldPass.UpdateArray where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let pair :: Stream (Array 2 Word32)+      pair = extern "pair" Nothing++  -- Check equality, indexing into array and modifying the value. Note that+  -- this is trivial by equality.+  trigger "trig_1"+    (((pair !! 0 =$ (+1)) ! 0) == ((pair ! 0) + 1))+    [arg pair]++  -- Same as previous example, but get a different array index (so should be+  -- false).+  trigger "trig_2"+    (((pair !! 0 =$ (+1)) ! 1) == ((pair ! 0) + 1))+    [arg pair]++verifySpec :: Verbosity -> IO ()+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                   mkDefaultCSettings [] "updateArray"
+ examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE DataKinds        #-}++-- | An example showing of using @copilot-verifier@ to verify a specification+-- involving structs where individual fields are updated.+module Copilot.Verifier.Examples.ShouldPass.UpdateStruct where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++-- | Definition for `Volts`.+data Volts = Volts+  { numVolts :: Field "numVolts" Word32+  , flag     :: Field "flag"     Bool+  }++-- | `Struct` instance for `Volts`.+instance Struct Volts where+  typeName _ = "volts"+  toValues vlts = [ Value Word32 (numVolts vlts)+                  , Value Bool   (flag vlts)+                  ]++-- | `Volts` instance for `Typed`.+instance Typed Volts where+  typeOf = Struct (Volts (Field 0) (Field False))++data Battery = Battery+  { temp  :: Field "temp"  Word32+  , volts :: Field "volts" (Array 10 Volts)+  , other :: Field "other" (Array 10 (Array 5 Word32))+  }++-- | `Battery` instance for `Struct`.+instance Struct Battery where+  typeName _ = "battery"+  toValues battery = [ Value typeOf (temp battery)+                     , Value typeOf (volts battery)+                     , Value typeOf (other battery)+                     ]++-- | `Battery` instance for `Typed`. Note that `undefined` is used as an+-- argument to `Field`. This argument is never used, so `undefined` will never+-- throw an error.+instance Typed Battery where+  typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))++spec :: Spec+spec = do+  let battery :: Stream Battery+      battery = extern "battery" Nothing++  -- Update a struct field, then check it for equality.+  trigger "updateTrig"+    ((battery ## temp =$ (+1))#temp == (battery#temp + 1))+    [arg battery]++verifySpec :: Verbosity -> IO ()+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                   mkDefaultCSettings [] "updateStruct"
src/Copilot/Verifier.hs view
@@ -66,7 +66,8 @@   , pushAssumptionFrame, popUntilAssumptionFrame   , getProofObligations, clearProofObligations   , LabeledPred(..), abortExecBecause, AbortExecReason(..), addAssumption-  , addDurableProofObligation, assert, CrucibleAssumption(..), ppAbortExecReason+  , addDurableAssertion, addDurableProofObligation+  , CrucibleAssumption(..), ppAbortExecReason   , IsSymBackend(..), HasSymInterface(..)   , labeledPred, labeledPredMsg   -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg@@ -78,7 +79,7 @@ import Lang.Crucible.Simulator   ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..)   , defaultAbortHandler, runOverrideSim, partialValue, gpValue-  , GlobalVar, executeCrucible, OverrideSim, regValue+  , GlobalVar, executeCrucible, OverrideSim, ovrWithBackend, regValue   , readGlobal, modifyGlobal, callCFG, emptyRegMap, RegEntry(..)   , AbortedResult(..)   )@@ -455,7 +456,8 @@   do Log.sayCopilot $ Log.ComputingConditions Log.InitialState      frm <- pushAssumptionFrame bak -     assertStateRelation bak clRefs mem initialState+     assertStateRelation bak clRefs mem+       Log.InitialStateRelation initialState       popUntilAssumptionFrame bak frm @@ -500,7 +502,8 @@         mem' <- setupPrestate bak mem prfbundle          -- sanity check, verify that we set up the memory in the expected relation-        assertStateRelation bak clRefs mem' (CW4.preStreamState prfbundle)+        assertStateRelation bak clRefs mem'+          Log.PreStepStateRelation (CW4.preStreamState prfbundle)          -- set up trigger guard global variables         let halloc = simHandleAllocator simctx@@ -515,7 +518,8 @@         mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)          -- assert the poststate is in the relation-        assertStateRelation bak clRefs mem'' (CW4.postStreamState prfbundle)+        assertStateRelation bak clRefs mem''+          Log.PostStepStateRelation (CW4.postStreamState prfbundle)       popUntilAssumptionFrame bak frm @@ -554,14 +558,15 @@   CopilotLogRefs sym ->   (Name, GlobalVar NatType, Pred sym) ->   (Name, BoolExpr t, [(Some Type, CW4.XExpr sym)]) ->-  OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem+  OverrideTemplate (Crux sym) sym LLVM arch triggerOverride clRefs (_,triggerGlobal,_) (nm, _guard, args) =    let args' = map toTypeRepr args in    case Ctx.fromList args' of      Some argCtx ->       basic_llvm_override $       LLVMOverride decl argCtx UnitRepr $-        \memOps bak calledArgs ->+        \memOps calledArgs ->+          ovrWithBackend $ \bak ->           do let sym = backendGetSym bak              modifyGlobal triggerGlobal $ \count -> do                -- See Note [Global variables for trigger functions]@@ -644,7 +649,7 @@   L.Module ->   ModuleTranslation arch ->   [(Name, GlobalVar NatType, Pred sym)] ->-  [OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem] ->+  [OverrideTemplate (Crux sym) sym LLVM arch] ->   [Pred sym] {- User-provided property assumptions -} ->   [Pred sym] {- Side conditions related to partial operations -} ->   IO (MemImpl sym)@@ -699,7 +704,7 @@   runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)   runStep =     do -- set up built-in functions and trigger overrides-       register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx+       _ <- register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx        -- set up functions defined in the module        registerLazyModule sayTranslationWarning modTrans @@ -838,13 +843,13 @@   HasLLVMAnn sym =>   (?memOpts :: MemOptions) =>   (?lc :: TypeContext) =>-   bak ->   CopilotLogRefs sym ->   MemImpl sym ->+  Log.StateRelationStep ->   CW4.BisimulationProofState sym ->   IO ()-assertStateRelation bak clRefs mem prfst =+assertStateRelation bak clRefs mem stateRelStep prfst =   -- For each stream in the proof state, assert that the   -- generated ring buffer global contains the corresponding   -- values.@@ -882,7 +887,7 @@         modifyIORef' (verifierAssertionMapRef clRefs)           $ Map.insert bannIdxVal           $ Log.RingBufferIndexLoadAssertion-          $ Log.RingBufferIndexLoad sym locIdxVal (Text.pack idxName) pIdxVal+          $ Log.RingBufferIndexLoad sym stateRelStep locIdxVal (Text.pack idxName) pIdxVal          buflen'  <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)         typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))@@ -903,7 +908,7 @@                $ Map.insert bannv'                $ Log.RingBufferLoadAssertion                $ Log.SomeSome-               $ Log.RingBufferLoad sym locv' bufNameT i buflen ctp typeRepr pv'+               $ Log.RingBufferLoad sym stateRelStep locv' bufNameT i buflen ctp typeRepr pv'              eq <- computeEqualVals bak clRefs mem ctp v typeRepr v'              (ann, eq') <- annotateTerm sym eq              let shortmsg = "State equality condition: " ++ show nm ++ " index value " ++ show i@@ -914,7 +919,7 @@                $ Map.insert (BoolAnn ann)                $ Log.StreamValueEqualityAssertion                $ Log.SomeSome-               $ Log.StreamValueEquality sym loc bufNameT i buflen ctp v typeRepr v'+               $ Log.StreamValueEquality sym stateRelStep loc bufNameT i buflen ctp v typeRepr v'              addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))          return ()@@ -1236,8 +1241,13 @@ `if guard_cond then 1 else 0`. -} --- | Like @crucible-llvm@'s @doLoad@, but also returning the 'BoolAnn' and--- 'Pred' asserting the validity of the load.+-- | Like @crucible-llvm@'s @doLoad@, but with the following differences:+--+-- * This function returns the 'BoolAnn' and 'Pred' asserting the validity of+--   the load, which the verifier needs for logging purposes.+--+-- * This always generates a durable proof goal so that Crucible will always+--   record it, even if it is trivial. doLoadWithAnn ::   ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym   , ?memOpts :: MemOptions ) =>@@ -1256,24 +1266,29 @@   where     sym = backendGetSym bak --- | Like @crucible-llvm@'s @assertSafe@, but also returning the 'BoolAnn' and--- 'Pred' corresponding the assertion.+-- | Like @crucible-llvm@'s @assertSafe@, but with the following differences:+--+-- * This function returns the 'BoolAnn' and 'Pred' corresponding to the+--   assertion, which the verifier needs for logging purposes.+--+-- * This generates a durable assertion so that Crucible will always record it,+--   even if it is trivial. assertSafeWithAnn ::   IsSymBackend sym bak =>   bak ->   PartLLVMVal sym ->   IO (BoolAnn sym, Pred sym, LLVMVal sym)-assertSafeWithAnn bak partVal =+assertSafeWithAnn bak partVal = do+  loc <- getCurrentProgramLoc sym+  let err = SimError loc rsn   case partVal of     NoErr p v -> do       (ann, p') <- annotateTerm sym p-      assert bak p' rsn+      addDurableAssertion bak (LabeledPred p' err)       return (BoolAnn ann, p', v)     Err p -> do-      loc <- getCurrentProgramLoc sym-      let err = SimError loc rsn       (_ann, p') <- annotateTerm sym p-      addProofObligation bak (LabeledPred p' err)+      addDurableProofObligation bak (LabeledPred p' err)       abortExecBecause (AssertionFailure err)   where     rsn = AssertFailureSimError "Error during memory load" ""
src/Copilot/Verifier/Log.hs view
@@ -13,6 +13,7 @@   ( SupportsCopilotLogMessage   , CopilotLogMessage(..)   , VerificationStep(..)+  , StateRelationStep(..)   , VerifierAssertion(..)   , SomeSome(..)   , StreamValueEquality(..)@@ -187,6 +188,34 @@   deriving stock Generic   deriving anyclass ToJSON +-- | The provenance of an assertion.+data AssertionProvenance+  = VerifierProvenance+    -- ^ Assertions that the verifier directly makes to check the correspondence+    -- between the Copilot specification and the generated C code. Because these+    -- assertions are core to the proof that the verifier is computing, these+    -- assertions' proof goals are always logged, even if they are trivial.+  | StepExecutionProvenance+    -- ^ Assertions that arise during symbolic execution of the @step()@+    -- function as part of proving the memory safety of the generated C code.+    -- These assertions' proof goals are only logged if they are non-trivial,+    -- as there would be an excessive number of these proof goals otherwise.++-- | At what step of the proof are we checking the state relation? We record+-- this so that we can better distinguish between transition step–related+-- proof goals that arise before or after calling the @step()@ function.+data StateRelationStep+  = InitialStateRelation+    -- ^ Check the state relation for the initial state.+  | PreStepStateRelation+    -- ^ During the transition step of the proof, check the state relation+    -- before calling the @step()@ function.+  | PostStepStateRelation+    -- ^ During the transition step of the proof, check the state relation+    -- after calling the @step()@ function.+  deriving stock Generic+  deriving anyclass ToJSON+ -- | Types of assertions that the verifier can make, which will count towards -- the total number of proof goals. data VerifierAssertion sym@@ -211,6 +240,8 @@ data StreamValueEquality sym copilotType crucibleType where   StreamValueEquality ::        sym+    -> StateRelationStep+       -- ^ When the values are checked for equality     -> WPL.ProgramLoc        -- ^ The locations of the values     -> Text@@ -271,8 +302,10 @@ data RingBufferLoad sym copilotType crucibleType where   RingBufferLoad ::        sym+    -> StateRelationStep+       -- ^ When the ring buffer is loaded from     -> WPL.ProgramLoc-       -- ^ The location of the trigger+       -- ^ The location of the buffer     -> Text        -- ^ The name of the buffer     -> Integer@@ -293,8 +326,10 @@ data RingBufferIndexLoad sym where   RingBufferIndexLoad ::        sym+    -> StateRelationStep+       -- ^ When the index's global variable is loaded from     -> WPL.ProgramLoc-       -- ^ The location of the trigger+       -- ^ The location of the global index     -> Text        -- ^ The name of the global index     -> WI.Pred sym@@ -489,15 +524,15 @@     , "```"     ] copilotLogMessageToSayWhat-    (StreamValueEqualityProofGoal step goalIdx numTotalGoals+    (StreamValueEqualityProofGoal verifStep goalIdx numTotalGoals       (StreamValueEquality-        sym loc+        sym stateRelStep loc         bufName offset len         copilotTy copilotVal         crucibleTy crucibleVal)) =   copilotNoisily $-  displayProofGoal-    step goalIdx numTotalGoals+  displayStateRelationProofGoal+    verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals     "asserting the equality between two stream values"     [ renderStrict $ ppProgramLoc loc     , "* Ring buffer name: " <> bufName@@ -514,7 +549,7 @@       (TriggersInvokedCorrespondingly loc name expected actual)) =   copilotNoisily $   displayProofGoal-    step goalIdx numTotalGoals+    step VerifierProvenance goalIdx numTotalGoals     "asserting triggers fired in corresponding ways"     [ renderStrict $ ppProgramLoc loc     , "* Trigger name: " <> T.pack name@@ -532,7 +567,7 @@         crucibleTy crucibleVal)) =   copilotNoisily $   displayProofGoal-    step goalIdx numTotalGoals+    step VerifierProvenance goalIdx numTotalGoals     "asserting the equality between two trigger arguments"     [ renderStrict $ ppProgramLoc loc     , "* Trigger name: " <> T.pack triggerName@@ -544,12 +579,12 @@     , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal     ] copilotLogMessageToSayWhat-    (RingBufferLoadProofGoal step goalIdx numTotalGoals+    (RingBufferLoadProofGoal verifStep goalIdx numTotalGoals       (RingBufferLoad-        _sym loc bufName offset len copilotTy _crucibleTy p)) =+        _sym stateRelStep loc bufName offset len copilotTy _crucibleTy p)) =   copilotNoisily $-  displayProofGoal-    step goalIdx numTotalGoals+  displayStateRelationProofGoal+    verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from a stream's ring buffer in C"     [ renderStrict $ ppProgramLoc loc     , "* Ring buffer name: " <> bufName@@ -560,11 +595,11 @@     , renderStrict $ PP.indent 4 $ WI.printSymExpr p     ] copilotLogMessageToSayWhat-    (RingBufferIndexLoadProofGoal step goalIdx numTotalGoals-      (RingBufferIndexLoad _sym loc idxName p)) =+    (RingBufferIndexLoadProofGoal verifStep goalIdx numTotalGoals+      (RingBufferIndexLoad _sym stateRelStep loc idxName p)) =   copilotNoisily $-  displayProofGoal-    step goalIdx numTotalGoals+  displayStateRelationProofGoal+    verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from the index to a stream's ring buffer in C"     [ renderStrict $ ppProgramLoc loc     , "* Ring buffer index name: " <> idxName@@ -577,7 +612,7 @@         _sym loc copilotTy _crucibleTy p)) =   copilotNoisily $   displayProofGoal-    step goalIdx numTotalGoals+    step VerifierProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from a pointer argument to a trigger"     [ renderStrict $ ppProgramLoc loc     , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")@@ -589,7 +624,7 @@       (AccessorFunctionLoad _sym loc accessorName p)) =   copilotNoisily $   displayProofGoal-    step goalIdx numTotalGoals+    step StepExecutionProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from a stream accessor function"     [ renderStrict $ ppProgramLoc loc     , "* Accessor function name: " <> WF.functionName accessorName@@ -601,7 +636,7 @@       (GuardFunctionLoad _sym loc accessorName p)) =   copilotNoisily $   displayProofGoal-    step goalIdx numTotalGoals+    step StepExecutionProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from a trigger guard function"     [ renderStrict $ ppProgramLoc loc     , "* Guard function name: " <> WF.functionName accessorName@@ -613,7 +648,7 @@       (UnknownFunctionLoad _sym loc accessorName p)) =   copilotNoisily $     displayProofGoal-    step goalIdx numTotalGoals+    step StepExecutionProvenance goalIdx numTotalGoals     "asserting the validity of a memory load from an unknown function"     [ renderStrict $ ppProgramLoc loc     , "* Function name: " <> WF.functionName accessorName@@ -636,7 +671,7 @@     LCLE.BBUndefinedBehavior ub ->       copilotNoisily $       displayProofGoal-        step goalIdx numTotalGoals+        step StepExecutionProvenance goalIdx numTotalGoals         "asserting that LLVM undefined behavior does not occur"         $ ppLoc : ppCallStackLines ++         [ "* Undefined behavior description:"@@ -645,7 +680,7 @@     LCLE.BBMemoryError me ->       copilotNoisily $       displayProofGoal-        step goalIdx numTotalGoals+        step StepExecutionProvenance goalIdx numTotalGoals         "asserting that LLVM memory unsafety does not occur"         $ ppLoc : ppCallStackLines ++         [ "* Memory unsafety description:"@@ -659,15 +694,17 @@ -- | Display information about an emitted proof goal. displayProofGoal ::      VerificationStep+  -> AssertionProvenance   -> Integer   -> Integer   -> Text   -> [Text]   -> Text-displayProofGoal step goalIdx numTotalGoals why ls = T.unlines $+displayProofGoal step assertProv goalIdx numTotalGoals why ls = T.unlines $   [ banner   , "Emitted a proof goal (" <> why <> ")"   , "  During the " <> displayStep+  , "  Required for proving the " <> displayAssertProv   , "  Proof goal " <> T.pack (show goalIdx)                     <> " ("                     <> T.pack (show numTotalGoals)@@ -683,6 +720,35 @@           "initial bisimulation state step"         StepBisimulation ->           "transition step of bisimulation"+    displayAssertProv =+      case assertProv of+        VerifierProvenance ->+          "correspondence between the spec and C code"+        StepExecutionProvenance ->+          "memory safety of the generated step() function"++-- | Display information about an emitted proof goal that involves checking the+-- state relation.+displayStateRelationProofGoal ::+     VerificationStep+  -> StateRelationStep+  -> AssertionProvenance+  -> Integer+  -> Integer+  -> Text+  -> [Text]+  -> Text+displayStateRelationProofGoal verifStep stateRelStep assertProv goalIdx numTotalGoals why =+    displayProofGoal verifStep assertProv goalIdx numTotalGoals why'+  where+    why' :: Text+    why' =+      case stateRelStep of+        PreStepStateRelation  -> why <> " before calling step()"+        PostStepStateRelation -> why <> " after calling step()"+        -- `displayProofGoal` already makes a note of the fact that we're+        -- checking the initial state, so no need to do so again here.+        InitialStateRelation -> why  ppProgramLoc :: WPL.ProgramLoc -> PP.Doc a ppProgramLoc pl = PP.vcat