Log when proof goals arise before or after calling step(). Refs #52.

copilot-verifier/CHANGELOG

@@ -1,3 +1,7 @@
+2024-07-18
+        * 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)
 

copilot-verifier/src/Copilot/Verifier.hs

@@ -455,7 +455,8 @@ verifyInitialState cruxOpts adapters clRefs simctx mem initialState =
   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 +501,8 @@ verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod mo
         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 +517,8 @@ verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod mo
         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
 
@@ -838,13 +841,13 @@ assertStateRelation ::
   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 +885,7 @@ assertStateRelation bak clRefs mem prfst =
         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 +906,7 @@ assertStateRelation bak clRefs mem prfst =
                $ 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 +917,7 @@ assertStateRelation bak clRefs mem prfst =
                $ 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 ()

copilot-verifier/src/Copilot/Verifier/Log.hs

@@ -13,6 +13,7 @@ module Copilot.Verifier.Log
   ( SupportsCopilotLogMessage
   , CopilotLogMessage(..)
   , VerificationStep(..)
+  , StateRelationStep(..)
   , VerifierAssertion(..)
   , SomeSome(..)
   , StreamValueEquality(..)
@@ -187,6 +188,21 @@ data VerificationStep
   deriving stock Generic
   deriving anyclass ToJSON
 
+-- | 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 +227,8 @@ data SomeSome (f :: j -> k -> Type) where
 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 +289,10 @@ data TriggerArgumentEquality sym copilotType crucibleType where
 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 +313,10 @@ data RingBufferLoad sym copilotType crucibleType where
 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 +511,15 @@ copilotLogMessageToSayWhat NoisyVerbositySuggestion =
     , "```"
     ]
 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 goalIdx numTotalGoals
     "asserting the equality between two stream values"
     [ renderStrict $ ppProgramLoc loc
     , "* Ring buffer name: " <> bufName
@@ -544,12 +566,12 @@ copilotLogMessageToSayWhat
     , 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 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 +582,11 @@ copilotLogMessageToSayWhat
     , 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 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
@@ -684,6 +706,28 @@ displayProofGoal step goalIdx numTotalGoals why ls = T.unlines $
         StepBisimulation ->
           "transition step of bisimulation"
 
+-- | Display information about an emitted proof goal that involves checking the
+-- state relation.
+displayStateRelationProofGoal ::
+     VerificationStep
+  -> StateRelationStep
+  -> Integer
+  -> Integer
+  -> Text
+  -> [Text]
+  -> Text
+displayStateRelationProofGoal verifStep stateRelStep goalIdx numTotalGoals why =
+    displayProofGoal verifStep 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)