content: {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE TemplateHaskell #-}
  module Copilot.Verifier.Log
    ( SupportsCopilotLogMessage
    , CopilotLogMessage(..)
    , VerificationStep(..)
    , StateRelationStep(..)
    , VerifierAssertion(..)
    , SomeSome(..)
    , StreamValueEquality(..)
    , TriggersInvokedCorrespondingly(..)
    , TriggerArgumentEquality(..)
    , RingBufferLoad(..)
    , RingBufferIndexLoad(..)
    , PointerArgumentLoad(..)
    , AccessorFunctionLoad(..)
    , GuardFunctionLoad(..)
    , UnknownFunctionLoad(..)
    , LLVMBadBehaviorCheck(..)
    , sayCopilot
    , copilotLogMessageToSayWhat
    ) where
  
  import Crux (SayLevel (..), SayWhat (..))
  import qualified Crux.Log as Log
  import Data.Aeson (ToJSON (..), Value (..))
  import Data.Aeson.TH (defaultOptions, deriveToJSON)
  import Data.Kind (Type)
  import qualified Data.Parameterized.Context as Ctx
  import qualified Data.Parameterized.Vector as PV
  import qualified Data.Parameterized.TraversableFC.WithIndex as PWI
  import Data.Text (Text)
  import qualified Data.Text as T
  import qualified Data.Vector as V
  import GHC.Generics (Generic)
  import qualified Prettyprinter as PP
  import qualified Prettyprinter.Render.Text as PP
  
  import qualified Copilot.Core.Expr as CE
  import qualified Copilot.Core.Type as CT
  import qualified Copilot.Theorem.What4 as CW4
  
  import qualified Lang.Crucible.Simulator as LCS
  import qualified Lang.Crucible.Types as LCT
  import qualified Lang.Crucible.LLVM.Errors as LCLE
  import qualified Lang.Crucible.LLVM.Errors.MemoryError as LCLEME
  import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as LCLEUB
  import qualified Lang.Crucible.LLVM.MemModel as LCLM
  import qualified Lang.Crucible.LLVM.MemModel.CallStack as LCLMCS
  import qualified What4.FunctionName as WF
  import qualified What4.Interface as WI
  import qualified What4.ProgramLoc as WPL
  
  data CopilotLogMessage where
    GeneratedCFile ::
         FilePath
         -- ^ The path of the generated C File
      -> CopilotLogMessage
    CompiledBitcodeFile ::
         String
         -- ^ The prefix to use in the compiled bitcode's directory
      -> FilePath
         -- ^ The name of the generated LLVM bitcode file
      -> CopilotLogMessage
    TranslatedToCrucible :: CopilotLogMessage
    GeneratingProofState :: CopilotLogMessage
    ComputingConditions :: VerificationStep -> CopilotLogMessage
    ProvingConditions :: VerificationStep -> CopilotLogMessage
    AllGoalsProved :: CopilotLogMessage
    OnlySomeGoalsProved ::
         Integer
         -- ^ Number of goals proved
      -> Integer
         -- ^ Number of total goals
      -> CopilotLogMessage
    SuccessfulProofSummary ::
         FilePath
         -- ^ Name of the generated C file.
      -> Integer
         -- ^ Number of goals proven during for the initial state of the proof.
      -> Integer
         -- ^ Number of goals proven during the bisimulation step of the proof.
      -> CopilotLogMessage
    NoisyVerbositySuggestion :: CopilotLogMessage
  
    -----
    -- Types of proof goals the verifier emits
    --
    -- The first three arguments to each constructor are:
    --
    -- * Which step of the verifier we are on
    -- * The current goal number (zero-indexed)
    -- * The total number of goals
    -----
  
    StreamValueEqualityProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> StreamValueEquality sym copilotType crucibleType
      -> CopilotLogMessage
  
    TriggersInvokedCorrespondinglyProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> TriggersInvokedCorrespondingly sym
      -> CopilotLogMessage
  
    TriggerArgumentEqualityProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> TriggerArgumentEquality sym copilotType crucibleType
      -> CopilotLogMessage
  
    RingBufferLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> RingBufferLoad sym copilotType crucibleType
      -> CopilotLogMessage
  
    RingBufferIndexLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> RingBufferIndexLoad sym
      -> CopilotLogMessage
  
    PointerArgumentLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> PointerArgumentLoad sym copilotType crucibleType
      -> CopilotLogMessage
  
    AccessorFunctionLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> AccessorFunctionLoad sym
      -> CopilotLogMessage
  
    GuardFunctionLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> GuardFunctionLoad sym
      -> CopilotLogMessage
  
    UnknownFunctionLoadProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> UnknownFunctionLoad sym
      -> CopilotLogMessage
  
    LLVMBadBehaviorCheckProofGoal ::
         WI.IsSymExprBuilder sym
      => VerificationStep
      -> Integer
      -> Integer
      -> LLVMBadBehaviorCheck sym
      -> CopilotLogMessage
  
  data VerificationStep
    = InitialState
    | StepBisimulation
    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
    = StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))
    | TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)
    | TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))
    | RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))
    | RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)
    | PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))
    | AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)
    | GuardFunctionLoadAssertion (GuardFunctionLoad sym)
    | UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)
    | LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)
  
  -- | Like @Some@ in @parameterized-utils@, but existentially closing over two
  -- type parameters instead of just one.
  data SomeSome (f :: j -> k -> Type) where
    SomeSome :: f x y -> SomeSome f
  
  -- | An assertion that an element in a Copilot stream is equal to the
  -- corresponding element in a C ring buffer.
  data StreamValueEquality sym copilotType crucibleType where
    StreamValueEquality ::
         sym
      -> StateRelationStep
         -- ^ When the values are checked for equality
      -> WPL.ProgramLoc
         -- ^ The locations of the values
      -> Text
         -- ^ The name of the buffer
      -> Integer
         -- ^ The offset from the buffer's index, which is used to compute the
         -- element of the buffer to load
      -> Integer
         -- ^ The number of elements in the buffer
      -> CT.Type copilotType
         -- ^ The Copilot type
      -> CW4.XExpr sym
         -- ^ The Copilot value
      -> LCT.TypeRepr crucibleType
         -- ^ The Crucible type
      -> LCS.RegValue sym crucibleType
         -- ^ The Crucible value
      -> StreamValueEquality sym copilotType crucibleType
  
  -- | An assertion that, given a Copilot trigger stream and its corresponding C
  -- trigger function on a particular time step, either both fired at the same
  -- time or both did not fire at all.
  data TriggersInvokedCorrespondingly sym where
    TriggersInvokedCorrespondingly ::
         WPL.ProgramLoc
         -- ^ The location of the trigger
      -> CE.Name
         -- ^ The trigger name
      -> WI.SymNat sym
         -- ^ The expected number of times the trigger was fired this step
         -- (should be either 1 or 0).
      -> WI.SymNat sym
         -- ^ The actual number of times the trigger was fired this step.
      -> TriggersInvokedCorrespondingly sym
  
  -- | An assertion that an argument to a Copilot trigger is equal to the
  -- corresponding argument to a C trigger function.
  data TriggerArgumentEquality sym copilotType crucibleType where
    TriggerArgumentEquality ::
         sym
      -> WPL.ProgramLoc
         -- ^ The locations of the arguments
      -> CE.Name
         -- ^ The trigger name
      -> Integer
         -- ^ The number of the argument (starting from 0)
      -> CT.Type copilotType
         -- ^ The Copilot type
      -> CW4.XExpr sym
         -- ^ The Copilot value
      -> LCT.TypeRepr crucibleType
         -- ^ The Crucible type
      -> LCS.RegValue sym crucibleType
         -- ^ The Crucible value
      -> TriggerArgumentEquality sym copilotType crucibleType
  
  -- | An assertion that a load from a ring buffer in C is valid.
  data RingBufferLoad sym copilotType crucibleType where
    RingBufferLoad ::
         sym
      -> StateRelationStep
         -- ^ When the ring buffer is loaded from
      -> WPL.ProgramLoc
         -- ^ The location of the buffer
      -> Text
         -- ^ The name of the buffer
      -> Integer
         -- ^ The offset from the buffer's index, which is used to compute the
         -- element of the buffer to load
      -> Integer
         -- ^ The number of elements in the buffer
      -> CT.Type copilotType
         -- ^ The Copilot type of the elements of the array
      -> LCT.TypeRepr crucibleType
         -- ^ The Crucible type of the elements of the array
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> RingBufferLoad sym copilotType crucibleType
  
  -- | An assertion that a load from a global variable representing a ring
  -- buffer's index in C is valid.
  data RingBufferIndexLoad sym where
    RingBufferIndexLoad ::
         sym
      -> StateRelationStep
         -- ^ When the index's global variable is loaded from
      -> WPL.ProgramLoc
         -- ^ The location of the global index
      -> Text
         -- ^ The name of the global index
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> RingBufferIndexLoad sym
  
  -- | An assertion that a load from a pointer argument to a trigger function in C
  -- is valid.
  data PointerArgumentLoad sym copilotType crucibleType where
    PointerArgumentLoad ::
         sym
      -> WPL.ProgramLoc
         -- ^ The location of the pointer
      -> CT.Type copilotType
         -- ^ The Copilot type of the underlying memory
      -> LCT.TypeRepr crucibleType
         -- ^ The Crucible type of the underlying memory
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> PointerArgumentLoad sym copilotType crucibleType
  
  -- | An assertion that a load occurring from somewhere in a stream accessor
  -- function in C (e.g., @s0_get@) is valid. This is a somewhat imprecise
  -- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
  -- happens because of an array index.)
  data AccessorFunctionLoad sym where
    AccessorFunctionLoad ::
         sym
      -> WPL.ProgramLoc
         -- ^ The location of the accessor function
      -> WF.FunctionName
         -- ^ The name of the accessor function
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> AccessorFunctionLoad sym
  
  -- | An assertion that a load occurring from somewhere in a trigger guard
  -- function in C (e.g., @even_guard@) is valid. This is a somewhat imprecise
  -- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
  -- happens because of an array index.)
  data GuardFunctionLoad sym where
    GuardFunctionLoad ::
         sym
      -> WPL.ProgramLoc
         -- ^ The location of the guard function
      -> WF.FunctionName
         -- ^ The name of the guard function
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> GuardFunctionLoad sym
  
  -- | An assertion that a load occurring in some function is valid. If you
  -- see this assertion, it is because the heuristics used to identify where
  -- load-related assertions come from could not identify a more precise cause
  -- for a load.
  data UnknownFunctionLoad sym where
    UnknownFunctionLoad ::
         sym
      -> WPL.ProgramLoc
         -- ^ The location of the function
      -> WF.FunctionName
         -- ^ The name of the function
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this load to be valid
      -> UnknownFunctionLoad sym
  
  -- | An assertion that checks that some form of bad behavior in LLVM does not
  -- occur. Bad behavior includes both undefined behavior and memory unsafety.
  data LLVMBadBehaviorCheck sym where
    LLVMBadBehaviorCheck ::
         sym
      -> WPL.ProgramLoc
         -- ^ The location of the check
      -> LCLMCS.CallStack
         -- ^ A call stack for the check, if one exists
      -> LCLE.BadBehavior sym
         -- ^ What type of LLVM bad behavior is being checked for
      -> WI.Pred sym
         -- ^ The assertion that must hold in order for this check to succeed
      -> LLVMBadBehaviorCheck sym
  
  -- Silly ToJSON instances. Crux is only requiring a ToJSON constraint for
  -- IDE-related functionality that we do not make use of, so the behavior of
  -- these instances aren't very important.
  
  instance ToJSON (StreamValueEquality sym copilotType crucibleType) where
    toJSON _ = String "StreamValueEquality"
  
  instance ToJSON (TriggersInvokedCorrespondingly sym) where
    toJSON _ = String "TriggersInvokedCorrespondingly"
  
  instance ToJSON (TriggerArgumentEquality sym copilotType crucibleType) where
    toJSON _ = String "TriggerArgumentEquality"
  
  instance ToJSON (RingBufferLoad sym copilotType crucibleType) where
    toJSON _ = String "RingBufferLoad"
  
  instance ToJSON (RingBufferIndexLoad sym) where
    toJSON _ = String "RingBufferIndexLoad"
  
  instance ToJSON (PointerArgumentLoad sym copilotType crucibleType) where
    toJSON _ = String "PointerArgumentLoad"
  
  instance ToJSON (AccessorFunctionLoad sym) where
    toJSON _ = String "AccessorFunctionLoad"
  
  instance ToJSON (GuardFunctionLoad sym) where
    toJSON _ = String "GuardFunctionLoad"
  
  instance ToJSON (UnknownFunctionLoad sym) where
    toJSON _ = String "UnknownFunctionLoad"
  
  instance ToJSON (LLVMBadBehaviorCheck sym) where
    toJSON _ = String "LLVMBadBehaviorCheck"
  
  type SupportsCopilotLogMessage msgs =
    (?injectCopilotLogMessage :: CopilotLogMessage -> msgs)
  
  sayCopilot ::
    Log.Logs msgs =>
    SupportsCopilotLogMessage msgs =>
    CopilotLogMessage ->
    IO ()
  sayCopilot msg =
    let ?injectMessage = ?injectCopilotLogMessage
     in Log.say msg
  
  copilotTag :: Text
  copilotTag = "copilot-verifier"
  
  -- copilotFail :: Text -> SayWhat
  -- copilotFail = SayWhat Fail copilotTag
  
  copilotSimply :: Text -> SayWhat
  copilotSimply = SayWhat Simply copilotTag
  
  copilotNoisily :: Text -> SayWhat
  copilotNoisily = SayWhat Noisily copilotTag
  
  -- copilotWarn :: Text -> SayWhat
  -- copilotWarn = SayWhat Warn copilotTag
  
  copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat
  copilotLogMessageToSayWhat (GeneratedCFile csrc) =
    copilotSimply $ "Generated " <> T.pack (show csrc)
  copilotLogMessageToSayWhat (CompiledBitcodeFile prefix bcFile) =
    copilotSimply $ "Compiled " <> T.pack prefix <> " into " <> T.pack bcFile
  copilotLogMessageToSayWhat TranslatedToCrucible =
    copilotSimply "Translated bitcode into Crucible"
  copilotLogMessageToSayWhat GeneratingProofState =
    copilotSimply "Generating proof state data"
  copilotLogMessageToSayWhat (ComputingConditions step) =
    copilotSimply $ "Computing " <> describeVerificationStep step <> " verification conditions"
  copilotLogMessageToSayWhat (ProvingConditions step) =
    copilotSimply $ "Proving " <> describeVerificationStep step <> " verification conditions"
  copilotLogMessageToSayWhat AllGoalsProved =
    copilotSimply "All obligations proved by concrete simplification"
  copilotLogMessageToSayWhat (OnlySomeGoalsProved numProvedGoals numTotalGoals) =
    copilotSimply $ T.unwords
      [ "Proved", T.pack (show numProvedGoals)
      , "of"
      , T.pack (show numTotalGoals), "total goals"
      ]
  copilotLogMessageToSayWhat (SuccessfulProofSummary cFileName initGoals bisimGoals) =
    copilotSimply $ T.unlines
      [ ""
      , "copilot-verifier has produced a mathematical proof that the behavior of"
      , "the generated C program (" <> T.pack cFileName
        <> ") precisely matches the behavior of"
      , "the Copilot specification. This proof shows that the behaviors match for"
      , "all possible moments in time, and in doing so, copilot-verifier examined"
      , "how the programs behave at the start of execution (the \"initial state\")"
      , "and at an arbitrary point of time in execution (the \"step bisimulation\")."
      , "copilot-verifier decomposed the overall proof into smaller goals, the"
      , "number of which depends on the size and complexity of the program. In this"
      , "example, there are " <> T.pack (show initGoals) <> " initial state goal(s)"
        <> " and " <> T.pack (show bisimGoals) <> " step bisimulation goal(s),"
      , "and copilot-verifier was able to prove all of them."
      ]
  copilotLogMessageToSayWhat NoisyVerbositySuggestion =
    copilotSimply $ T.unlines
      [ ""
      , "copilot-verifier is displaying an abridged summary of the verification results."
      , "copilot-verifier also includes a \"noisy\" mode that prints detailed"
      , "descriptions of each individual proof goal, including what type of goal it is,"
      , "why it needs to be proven, and where in the Copilot specification and/or C code"
      , "the proof goal originated from. To enable noisy mode, invoke the verifier with"
      , "the following options:"
      , ""
      , "```"
      , "verifyWithOptions (defaultVerifierOptions { verbosity = Noisy }) ..."
      , "```"
      ]
  copilotLogMessageToSayWhat
      (StreamValueEqualityProofGoal verifStep goalIdx numTotalGoals
        (StreamValueEquality
          sym stateRelStep loc
          bufName offset len
          copilotTy copilotVal
          crucibleTy crucibleVal)) =
    copilotNoisily $
    displayStateRelationProofGoal
      verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals
      "asserting the equality between two stream values"
      [ renderStrict $ ppProgramLoc loc
      , "* Ring buffer name: " <> bufName
      , "* Offset into buffer (from current index): " <> T.pack (show offset)
      , "* Number of elements in buffer: " <> T.pack (show len)
      , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")
      , "* Copilot value:"
      , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal
      , "* Crucible value:"
      , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal
      ]
  copilotLogMessageToSayWhat
      (TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals
        (TriggersInvokedCorrespondingly loc name expected actual)) =
    copilotNoisily $
    displayProofGoal
      step VerifierProvenance goalIdx numTotalGoals
      "asserting triggers fired in corresponding ways"
      [ renderStrict $ ppProgramLoc loc
      , "* Trigger name: " <> T.pack name
      , "* Expected number of times trigger was fired:"
      , renderStrict $ PP.indent 4 $ WI.printSymNat expected
      , "* Actual number of times trigger was fired:"
      , renderStrict $ PP.indent 4 $ WI.printSymNat actual
      ]
  copilotLogMessageToSayWhat
      (TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals
        (TriggerArgumentEquality
          sym loc
          triggerName argNum
          copilotTy copilotVal
          crucibleTy crucibleVal)) =
    copilotNoisily $
    displayProofGoal
      step VerifierProvenance goalIdx numTotalGoals
      "asserting the equality between two trigger arguments"
      [ renderStrict $ ppProgramLoc loc
      , "* Trigger name: " <> T.pack triggerName
      , "* Number of argument: " <> T.pack (show argNum)
      , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")
      , "* Copilot value:"
      , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal
      , "* Crucible value:"
      , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal
      ]
  copilotLogMessageToSayWhat
      (RingBufferLoadProofGoal verifStep goalIdx numTotalGoals
        (RingBufferLoad
          _sym stateRelStep loc bufName offset len copilotTy _crucibleTy p)) =
    copilotNoisily $
    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
      , "* Offset into buffer (from current index): " <> T.pack (show offset)
      , "* Number of elements in buffer: " <> T.pack (show len)
      , "* Copilot type of buffer elements:" <> T.pack (showsCopilotType 0 copilotTy "")
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (RingBufferIndexLoadProofGoal verifStep goalIdx numTotalGoals
        (RingBufferIndexLoad _sym stateRelStep loc idxName p)) =
    copilotNoisily $
    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
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (PointerArgumentLoadProofGoal step goalIdx numTotalGoals
        (PointerArgumentLoad
          _sym loc copilotTy _crucibleTy p)) =
    copilotNoisily $
    displayProofGoal
      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 "")
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (AccessorFunctionLoadProofGoal step goalIdx numTotalGoals
        (AccessorFunctionLoad _sym loc accessorName p)) =
    copilotNoisily $
    displayProofGoal
      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
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (GuardFunctionLoadProofGoal step goalIdx numTotalGoals
        (GuardFunctionLoad _sym loc accessorName p)) =
    copilotNoisily $
    displayProofGoal
      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
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (UnknownFunctionLoadProofGoal step goalIdx numTotalGoals
        (UnknownFunctionLoad _sym loc accessorName p)) =
    copilotNoisily $
      displayProofGoal
      step StepExecutionProvenance goalIdx numTotalGoals
      "asserting the validity of a memory load from an unknown function"
      [ renderStrict $ ppProgramLoc loc
      , "* Function name: " <> WF.functionName accessorName
      , "* Validity predicate:"
      , renderStrict $ PP.indent 4 $ WI.printSymExpr p
      ]
  copilotLogMessageToSayWhat
      (LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals
        (LLVMBadBehaviorCheck _sym loc stk bb p)) =
    let ppLoc = renderStrict $ ppProgramLoc loc
        ppCallStackLines =
          [ "* Call stack:"
          , "    " <> renderCallStack stk
          ]
        ppValidPredLines =
          [ "* Validity predicate:"
          , renderStrict $ PP.indent 4 $ WI.printSymExpr p
          ] in
    case bb of
      LCLE.BBUndefinedBehavior ub ->
        copilotNoisily $
        displayProofGoal
          step StepExecutionProvenance goalIdx numTotalGoals
          "asserting that LLVM undefined behavior does not occur"
          $ ppLoc : ppCallStackLines ++
          [ "* Undefined behavior description:"
          , renderStrict $ PP.indent 4 $ LCLEUB.ppDetails ub
          ] ++ ppValidPredLines
      LCLE.BBMemoryError me ->
        copilotNoisily $
        displayProofGoal
          step StepExecutionProvenance goalIdx numTotalGoals
          "asserting that LLVM memory unsafety does not occur"
          $ ppLoc : ppCallStackLines ++
          [ "* Memory unsafety description:"
          , renderStrict $ PP.indent 4 $ LCLEME.explain me
          ] ++ ppValidPredLines
  
  describeVerificationStep :: VerificationStep -> Text
  describeVerificationStep InitialState     = "initial state"
  describeVerificationStep StepBisimulation = "step bisimulation"
  
  -- | Display information about an emitted proof goal.
  displayProofGoal ::
       VerificationStep
    -> AssertionProvenance
    -> Integer
    -> Integer
    -> Text
    -> [Text]
    -> Text
  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)
                      <> " total)"
    , ""
    ]
    ++ ls ++ [banner]
    where
      banner = "====="
      displayStep =
        case step of
          InitialState ->
            "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
    [ "* Function:" PP.<+> PP.pretty (WPL.plFunction pl)
    , "  Position:" PP.<+> PP.pretty (WPL.plSourceLoc pl)
    ]
  
  renderCallStack :: LCLMCS.CallStack -> Text
  renderCallStack cs
    | T.null ppText
    = "<no call stack available>"
    | otherwise
    = ppText
    where
      ppText = renderStrict $ LCLMCS.ppCallStack cs
  
  showsCopilotType :: Int -> CT.Type tp -> ShowS
  showsCopilotType prec tp =
    case tp of
      CT.Bool     -> showString "Bool"
      CT.Int8     -> showString "Int8"
      CT.Int16    -> showString "Int16"
      CT.Int32    -> showString "Int32"
      CT.Int64    -> showString "Int64"
      CT.Word8    -> showString "Word8"
      CT.Word16   -> showString "Word16"
      CT.Word32   -> showString "Word32"
      CT.Word64   -> showString "Word64"
      CT.Float    -> showString "Float"
      CT.Double   -> showString "Double"
      CT.Array t  -> showParen (prec >= 11) $
                       showString "Array" .
                       showsPrec 11 (CT.typeSize tp) .
                       showsCopilotType 11 t
      CT.Struct x -> showString $ CT.typeName x
  
  ppCopilotValue :: WI.IsSymExprBuilder sym => CW4.XExpr sym -> PP.Doc a
  ppCopilotValue val =
    case val of
      CW4.XBool   b -> WI.printSymExpr b
      CW4.XInt8   i -> WI.printSymExpr i
      CW4.XInt16  i -> WI.printSymExpr i
      CW4.XInt32  i -> WI.printSymExpr i
      CW4.XInt64  i -> WI.printSymExpr i
      CW4.XWord8  w -> WI.printSymExpr w
      CW4.XWord16 w -> WI.printSymExpr w
      CW4.XWord32 w -> WI.printSymExpr w
      CW4.XWord64 w -> WI.printSymExpr w
      CW4.XFloat  f -> WI.printSymExpr f
      CW4.XDouble d -> WI.printSymExpr d
      CW4.XEmptyArray {} -> "[]"
      CW4.XArray  a   -> ppBracesWith ppCopilotValue (PV.toList a)
      CW4.XStruct s   -> ppBracketsWith ppCopilotValue s
  
  ppCrucibleValue :: WI.IsSymExprBuilder sym
                  => sym
                  -> LCT.TypeRepr tp
                  -> LCS.RegValue sym tp
                  -> PP.Doc a
  ppCrucibleValue sym tp val =
    case tp of
      LCLM.LLVMPointerRepr _ -> LCLM.ppPtr val
      LCT.FloatRepr _        -> WI.printSymExpr val
      LCT.VectorRepr tpr     -> ppBracketsWith (ppCrucibleValue sym tpr) (V.toList val)
      LCT.StructRepr ctx     -> withBraces $
                                PWI.itoListFC (\i (LCS.RV v) -> ppCrucibleValue sym (ctx Ctx.! i) v) val
      _ -> error $ "ppCrucibleValue: Unsupported type: " ++ show tp
  
  renderStrict :: PP.Doc a ->  Text
  renderStrict = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions
  
  ppBracketsWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
  ppBracketsWith f = PP.align . PP.list . map f
  
  ppBracesWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
  ppBracesWith f = withBraces . map f
  
  withBraces :: [PP.Doc a] -> PP.Doc a
  withBraces =
      PP.align
    . PP.encloseSep (PP.flatAlt "{ " "{") (PP.flatAlt " }" "}") ", "
  
  $(deriveToJSON defaultOptions ''CopilotLogMessage)
  