Copilot.Verifier.Log

Documentation

type SupportsCopilotLogMessage msgs = ?injectCopilotLogMessage :: CopilotLogMessage -> msgs

data CopilotLogMessage where

Constructors

GeneratedCFile

Fields

• :: FilePath

  The path of the generated C File

• -> CopilotLogMessage

CompiledBitcodeFile

Fields

• :: 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

Fields

• :: Integer

  Number of goals proved

• -> Integer

  Number of total goals

• -> CopilotLogMessage

SuccessfulProofSummary

Fields

• :: 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

StreamValueEqualityProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> StreamValueEquality sym copilotType crucibleType -> CopilotLogMessage

TriggersInvokedCorrespondinglyProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggersInvokedCorrespondingly sym -> CopilotLogMessage

TriggerArgumentEqualityProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggerArgumentEquality sym copilotType crucibleType -> CopilotLogMessage

RingBufferLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferLoad sym copilotType crucibleType -> CopilotLogMessage

RingBufferIndexLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferIndexLoad sym -> CopilotLogMessage

PointerArgumentLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> PointerArgumentLoad sym copilotType crucibleType -> CopilotLogMessage

AccessorFunctionLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> AccessorFunctionLoad sym -> CopilotLogMessage

GuardFunctionLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> GuardFunctionLoad sym -> CopilotLogMessage

UnknownFunctionLoadProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> UnknownFunctionLoad sym -> CopilotLogMessage

LLVMBadBehaviorCheckProofGoal :: IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> LLVMBadBehaviorCheck sym -> CopilotLogMessage

Instances

ToJSON CopilotLogMessage

Defined in Copilot.Verifier.Log

Methods

toJSON :: CopilotLogMessage -> Value

toEncoding :: CopilotLogMessage -> Encoding

toJSONList :: [CopilotLogMessage] -> Value

toEncodingList :: [CopilotLogMessage] -> Encoding

omitField :: CopilotLogMessage -> Bool

data VerificationStep

Constructors

InitialState

StepBisimulation

Instances

ToJSON VerificationStep

Defined in Copilot.Verifier.Log

Methods

toJSON :: VerificationStep -> Value

toEncoding :: VerificationStep -> Encoding

toJSONList :: [VerificationStep] -> Value

toEncodingList :: [VerificationStep] -> Encoding

omitField :: VerificationStep -> Bool

Generic VerificationStep

Defined in Copilot.Verifier.Log

Associated Types

type Rep VerificationStep :: Type -> Type

Methods

from :: VerificationStep -> Rep VerificationStep x

to :: Rep VerificationStep x -> VerificationStep

type Rep VerificationStep

Defined in Copilot.Verifier.Log

type Rep VerificationStep = D1 ('MetaData "VerificationStep" "Copilot.Verifier.Log" "copilot-verifier-4.0-GSb3fayibgQ2pCUrJC8cca" 'False) (C1 ('MetaCons "InitialState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StepBisimulation" 'PrefixI 'False) (U1 :: Type -> Type))

data StateRelationStep

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.

Constructors

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.

Instances

ToJSON StateRelationStep

Defined in Copilot.Verifier.Log

Methods

toJSON :: StateRelationStep -> Value

toEncoding :: StateRelationStep -> Encoding

toJSONList :: [StateRelationStep] -> Value

toEncodingList :: [StateRelationStep] -> Encoding

omitField :: StateRelationStep -> Bool

Generic StateRelationStep

Defined in Copilot.Verifier.Log

Associated Types

type Rep StateRelationStep :: Type -> Type

Methods

from :: StateRelationStep -> Rep StateRelationStep x

to :: Rep StateRelationStep x -> StateRelationStep

type Rep StateRelationStep

Defined in Copilot.Verifier.Log

type Rep StateRelationStep = D1 ('MetaData "StateRelationStep" "Copilot.Verifier.Log" "copilot-verifier-4.0-GSb3fayibgQ2pCUrJC8cca" 'False) (C1 ('MetaCons "InitialStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PreStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PostStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type)))

data VerifierAssertion sym

Types of assertions that the verifier can make, which will count towards the total number of proof goals.

Constructors

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)

data SomeSome (f :: j -> k -> Type) where

Like Some in parameterized-utils, but existentially closing over two type parameters instead of just one.

Constructors

SomeSome :: f x y -> SomeSome f

data StreamValueEquality sym copilotType crucibleType where

An assertion that an element in a Copilot stream is equal to the corresponding element in a C ring buffer.

Constructors

StreamValueEquality

Fields

• :: sym
• -> StateRelationStep

  When the values are checked for equality

• -> 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

• -> Type copilotType

  The Copilot type

• -> XExpr sym

  The Copilot value

• -> TypeRepr crucibleType

  The Crucible type

• -> RegValue sym crucibleType

  The Crucible value

• -> StreamValueEquality sym copilotType crucibleType

Instances

ToJSON (StreamValueEquality sym copilotType crucibleType)

Defined in Copilot.Verifier.Log

Methods

toJSON :: StreamValueEquality sym copilotType crucibleType -> Value

toEncoding :: StreamValueEquality sym copilotType crucibleType -> Encoding

toJSONList :: [StreamValueEquality sym copilotType crucibleType] -> Value

toEncodingList :: [StreamValueEquality sym copilotType crucibleType] -> Encoding

omitField :: StreamValueEquality sym copilotType crucibleType -> Bool

data TriggersInvokedCorrespondingly sym where

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.

Constructors

TriggersInvokedCorrespondingly

Fields

• :: ProgramLoc

  The location of the trigger

• -> Name

  The trigger name

• -> SymNat sym

  The expected number of times the trigger was fired this step (should be either 1 or 0).

• -> SymNat sym

  The actual number of times the trigger was fired this step.

• -> TriggersInvokedCorrespondingly sym

Instances

ToJSON (TriggersInvokedCorrespondingly sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: TriggersInvokedCorrespondingly sym -> Value

toEncoding :: TriggersInvokedCorrespondingly sym -> Encoding

toJSONList :: [TriggersInvokedCorrespondingly sym] -> Value

toEncodingList :: [TriggersInvokedCorrespondingly sym] -> Encoding

omitField :: TriggersInvokedCorrespondingly sym -> Bool

data TriggerArgumentEquality sym copilotType crucibleType where

An assertion that an argument to a Copilot trigger is equal to the corresponding argument to a C trigger function.

Constructors

TriggerArgumentEquality

Fields

• :: sym
• -> ProgramLoc

  The locations of the arguments

• -> Name

  The trigger name

• -> Integer

  The number of the argument (starting from 0)

• -> Type copilotType

  The Copilot type

• -> XExpr sym

  The Copilot value

• -> TypeRepr crucibleType

  The Crucible type

• -> RegValue sym crucibleType

  The Crucible value

• -> TriggerArgumentEquality sym copilotType crucibleType

Instances

ToJSON (TriggerArgumentEquality sym copilotType crucibleType)

Defined in Copilot.Verifier.Log

Methods

toJSON :: TriggerArgumentEquality sym copilotType crucibleType -> Value

toEncoding :: TriggerArgumentEquality sym copilotType crucibleType -> Encoding

toJSONList :: [TriggerArgumentEquality sym copilotType crucibleType] -> Value

toEncodingList :: [TriggerArgumentEquality sym copilotType crucibleType] -> Encoding

omitField :: TriggerArgumentEquality sym copilotType crucibleType -> Bool

data RingBufferLoad sym copilotType crucibleType where

An assertion that a load from a ring buffer in C is valid.

Constructors

RingBufferLoad

Fields

• :: sym
• -> StateRelationStep

  When the ring buffer is loaded from

• -> 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

• -> Type copilotType

  The Copilot type of the elements of the array

• -> TypeRepr crucibleType

  The Crucible type of the elements of the array

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> RingBufferLoad sym copilotType crucibleType

Instances

ToJSON (RingBufferLoad sym copilotType crucibleType)

Defined in Copilot.Verifier.Log

Methods

toJSON :: RingBufferLoad sym copilotType crucibleType -> Value

toEncoding :: RingBufferLoad sym copilotType crucibleType -> Encoding

toJSONList :: [RingBufferLoad sym copilotType crucibleType] -> Value

toEncodingList :: [RingBufferLoad sym copilotType crucibleType] -> Encoding

omitField :: RingBufferLoad sym copilotType crucibleType -> Bool

data RingBufferIndexLoad sym where

An assertion that a load from a global variable representing a ring buffer's index in C is valid.

Constructors

RingBufferIndexLoad

Fields

• :: sym
• -> StateRelationStep

  When the index's global variable is loaded from

• -> ProgramLoc

  The location of the global index

• -> Text

  The name of the global index

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> RingBufferIndexLoad sym

Instances

ToJSON (RingBufferIndexLoad sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: RingBufferIndexLoad sym -> Value

toEncoding :: RingBufferIndexLoad sym -> Encoding

toJSONList :: [RingBufferIndexLoad sym] -> Value

toEncodingList :: [RingBufferIndexLoad sym] -> Encoding

omitField :: RingBufferIndexLoad sym -> Bool

data PointerArgumentLoad sym copilotType crucibleType where

An assertion that a load from a pointer argument to a trigger function in C is valid.

Constructors

PointerArgumentLoad

Fields

• :: sym
• -> ProgramLoc

  The location of the pointer

• -> Type copilotType

  The Copilot type of the underlying memory

• -> TypeRepr crucibleType

  The Crucible type of the underlying memory

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> PointerArgumentLoad sym copilotType crucibleType

Instances

ToJSON (PointerArgumentLoad sym copilotType crucibleType)

Defined in Copilot.Verifier.Log

Methods

toJSON :: PointerArgumentLoad sym copilotType crucibleType -> Value

toEncoding :: PointerArgumentLoad sym copilotType crucibleType -> Encoding

toJSONList :: [PointerArgumentLoad sym copilotType crucibleType] -> Value

toEncodingList :: [PointerArgumentLoad sym copilotType crucibleType] -> Encoding

omitField :: PointerArgumentLoad sym copilotType crucibleType -> Bool

data AccessorFunctionLoad sym where

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.)

Constructors

AccessorFunctionLoad

Fields

• :: sym
• -> ProgramLoc

  The location of the accessor function

• -> FunctionName

  The name of the accessor function

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> AccessorFunctionLoad sym

Instances

ToJSON (AccessorFunctionLoad sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: AccessorFunctionLoad sym -> Value

toEncoding :: AccessorFunctionLoad sym -> Encoding

toJSONList :: [AccessorFunctionLoad sym] -> Value

toEncodingList :: [AccessorFunctionLoad sym] -> Encoding

omitField :: AccessorFunctionLoad sym -> Bool

data GuardFunctionLoad sym where

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.)

Constructors

GuardFunctionLoad

Fields

• :: sym
• -> ProgramLoc

  The location of the guard function

• -> FunctionName

  The name of the guard function

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> GuardFunctionLoad sym

Instances

ToJSON (GuardFunctionLoad sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: GuardFunctionLoad sym -> Value

toEncoding :: GuardFunctionLoad sym -> Encoding

toJSONList :: [GuardFunctionLoad sym] -> Value

toEncodingList :: [GuardFunctionLoad sym] -> Encoding

omitField :: GuardFunctionLoad sym -> Bool

data UnknownFunctionLoad sym where

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.

Constructors

UnknownFunctionLoad

Fields

• :: sym
• -> ProgramLoc

  The location of the function

• -> FunctionName

  The name of the function

• -> Pred sym

  The assertion that must hold in order for this load to be valid

• -> UnknownFunctionLoad sym

Instances

ToJSON (UnknownFunctionLoad sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: UnknownFunctionLoad sym -> Value

toEncoding :: UnknownFunctionLoad sym -> Encoding

toJSONList :: [UnknownFunctionLoad sym] -> Value

toEncodingList :: [UnknownFunctionLoad sym] -> Encoding

omitField :: UnknownFunctionLoad sym -> Bool

data LLVMBadBehaviorCheck sym where

An assertion that checks that some form of bad behavior in LLVM does not occur. Bad behavior includes both undefined behavior and memory unsafety.

Constructors

LLVMBadBehaviorCheck

Fields

• :: sym
• -> ProgramLoc

  The location of the check

• -> CallStack

  A call stack for the check, if one exists

• -> BadBehavior sym

  What type of LLVM bad behavior is being checked for

• -> Pred sym

  The assertion that must hold in order for this check to succeed

• -> LLVMBadBehaviorCheck sym

Instances

ToJSON (LLVMBadBehaviorCheck sym)

Defined in Copilot.Verifier.Log

Methods

toJSON :: LLVMBadBehaviorCheck sym -> Value

toEncoding :: LLVMBadBehaviorCheck sym -> Encoding

toJSONList :: [LLVMBadBehaviorCheck sym] -> Value

toEncodingList :: [LLVMBadBehaviorCheck sym] -> Encoding

omitField :: LLVMBadBehaviorCheck sym -> Bool

sayCopilot :: Logs msgs => SupportsCopilotLogMessage msgs => CopilotLogMessage -> IO ()

copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat