copilot-verifier 0.1 → 3.19

raw patch · 9 files changed

+146/−82 lines, 9 filesdep ~copilotdep ~copilot-c99dep ~copilot-core

Dependency ranges changed: copilot, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem

Files

• CHANGELOG +7/−0
• CHANGELOG.md +0/−5
• README.md +10/−4
• copilot-verifier.cabal +19/−18
• examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs +1/−1
• examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs +2/−2
• examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs +36/−41
• src/Copilot/Verifier.hs +32/−11
• src/Copilot/Verifier/Log.hs +39/−0

@@ -0,0 +1,7 @@+2024-03-08+        * Version bump (3.19). (#53)+        * Provide more detailed feedback upon a successful run of the verifier.+        * Make the examples build with Copilot 3.19. (#53)++2024-02-06+        * Initial release of `copilot-verifier`.

@@ -1,5 +0,0 @@-# Release history for copilot-verifier--## 0.1 (February 2024)--* Initial release of `copilot-verifier.

@@ -1,9 +1,11 @@+[![Build Status](https://github.com/Copilot-Language/copilot-verifier/workflows/copilot-verifier/badge.svg)](https://github.com/Copilot-Language/copilot-verifier/actions?query=workflow%3Acopilot-verifier)+[![Version on Hackage](https://img.shields.io/hackage/v/copilot-verifier.svg)](https://hackage.haskell.org/package/copilot-verifier)+ # Copilot Verifier -This "Copilot Verifier" is an add-on to the-[Copilot Stream DSL](https://copilot-language.github.io)-for verifying the correctness of C code generated-by the `copilot-c99` package.+Copilot Verifier is an add-on to the [Copilot Stream+DSL](https://copilot-language.github.io) for verifying the correctness of C+code generated by the `copilot-c99` package.  The main idea of the verifier is to use the [Crucible symbolic simulator](https://github.com/galoisinc/crucible)@@ -14,6 +16,10 @@ verification conditions are then dispatched to SMT solvers to be automatically solved.  We will have more to say about exactly what is meant by this correspondence below.++Copilot Verifier is described in the ICFP 2023 paper [_Trustworthy Runtime+Verification via Bisimulation (Experience+Report)_](https://dl.acm.org/doi/abs/10.1145/3607841).  ## Building 

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          copilot-verifier-Version:       0.1+Version:       3.19 Author:        Galois Inc. Maintainer:    rscott@galois.com Copyright:     (c) Galois, Inc 2021-2024@@ -10,17 +10,18 @@ Category:      Language Synopsis:      System for verifying the correctness of generated Copilot programs Description:-  @copilot-verifier@ is an add-on to the <https://copilot-language.github.io-  Copilot Stream DSL> for verifying the correctness of C code generated by the-  @copilot-c99@ package.+  @copilot-verifier@ is an add-on to the [Copilot Stream+  DSL](https://copilot-language.github.io) for verifying the correctness of C+  code generated by the @copilot-c99@ package.   .-  @copilot-verifier@ uses the <https://github.com/galoisinc/crucible Crucible-  symbolic simulator> to interpret the semantics of the generated C program and-  and to produce verification conditions sufficient to guarantee that the-  meaning of the generated program corresponds in a precise way to the meaning-  of the original stream specification. The generated verification conditions-  are then dispatched to SMT solvers to be automatically solved.-extra-doc-files: CHANGELOG.md, README.md+  @copilot-verifier@ uses the [Crucible symbolic+  simulator](https://github.com/galoisinc/crucible) to interpret the semantics+  of the generated C program and and to produce verification conditions+  sufficient to guarantee that the meaning of the generated program corresponds+  in a precise way to the meaning of the original stream specification. The+  generated verification conditions are then dispatched to SMT solvers to be+  automatically solved.+extra-doc-files: CHANGELOG, README.md  source-repository head   type:     git@@ -44,13 +45,13 @@     bv-sized >= 1.0.0 && < 1.1,     bytestring,     containers >= 0.5.9.0,-    copilot >= 3.18.1 && < 3.19,-    copilot-c99 >= 3.18.1 && < 3.19,-    copilot-core >= 3.18.1 && < 3.19,-    copilot-libraries >= 3.18.1 && < 3.19,-    copilot-language >= 3.18.1 && < 3.19,-    copilot-prettyprinter >= 3.18.1 && < 3.19,-    copilot-theorem >= 3.18.1 && < 3.19,+    copilot >= 3.19 && < 3.20,+    copilot-c99 >= 3.19 && < 3.20,+    copilot-core >= 3.19 && < 3.20,+    copilot-libraries >= 3.19 && < 3.20,+    copilot-language >= 3.19 && < 3.20,+    copilot-prettyprinter >= 3.19 && < 3.20,+    copilot-theorem >= 3.19 && < 3.20,     crucible >= 0.7 && < 0.8,     crucible-llvm >= 0.6 && < 0.7,     crux >= 0.7 && < 0.8,

@@ -10,7 +10,7 @@ data S = S { field :: Field "field" Int16 }  instance Struct S where-  typename _ = "s"+  typeName _ = "s"   toValues s = [Value Int16 (field s)]  instance Typed S where

@@ -24,7 +24,7 @@  -- | `Struct` instance for `Volts`. instance Struct Volts where-  typename _ = "volts"+  typeName _ = "volts"   toValues vlts = [ Value Word16 (numVolts vlts)                   , Value Bool   (flag vlts)                   ]@@ -41,7 +41,7 @@  -- | `Battery` instance for `Struct`. instance Struct Battery where-  typename _ = "battery"+  typeName _ = "battery"   toValues battery = [ Value typeOf (temp battery)                      , Value typeOf (volts battery)                      , Value typeOf (other battery)

@@ -9,13 +9,12 @@ module Copilot.Verifier.Examples.ShouldPass.WCV where  import Language.Copilot-import qualified Copilot.Theorem.What4 as CT+-- import qualified Copilot.Theorem.What4 as CT import Copilot.Compile.C99 import Copilot.Verifier ( Verbosity, VerifierOptions(..)                         , defaultVerifierOptions, verifyWithOptions ) -import qualified Prelude as P-import Data.Foldable (forM_)+-- import Data.Foldable (forM_) import qualified Control.Monad as Monad  @@ -38,44 +37,6 @@ type Vect2 = (Stream Double, Stream Double)  ------------------------------------ External streams for relative position and velocity.------------------------------------- | The relative x velocity between ownship and the intruder.-vx :: Stream Double-vx = extern "relative_velocity_x" Nothing---- | The relative y velocity between ownship and the intruder.-vy :: Stream Double-vy = extern "relative_velocity_y" Nothing---- | The relative z velocity between ownship and the intruder.-vz :: Stream Double-vz = extern "relative_velocity_z" Nothing---- | The relative velocity as a 2D vector.-v :: (Stream Double, Stream Double)-v = (vx, vy)----- | The relative x position between ownship and the intruder.-sx :: Stream Double-sx = extern "relative_position_x" Nothing---- | The relative y position between ownship and the intruder.-sy :: Stream Double-sy = extern "relative_position_y" Nothing---- | The relative z position between ownship and the intruder.-sz :: Stream Double-sz = extern "relative_position_z" Nothing---- | The relative position as a 2D vector.-s :: (Stream Double, Stream Double)-s = (sx, sy)-- ------------------ -- The following section contains basic libraries for working with vectors. ------------------@@ -169,7 +130,41 @@   (norm s <= dthr) ||   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr)) +spec :: Spec spec = do+  -- External streams for relative position and velocity.+  let -- The relative x velocity between ownship and the intruder.+      vx :: Stream Double+      vx = extern "relative_velocity_x" Nothing++      -- The relative y velocity between ownship and the intruder.+      vy :: Stream Double+      vy = extern "relative_velocity_y" Nothing++      -- The relative z velocity between ownship and the intruder.+      vz :: Stream Double+      vz = extern "relative_velocity_z" Nothing++      -- The relative velocity as a 2D vector.+      v :: (Stream Double, Stream Double)+      v = (vx, vy)+++      -- The relative x position between ownship and the intruder.+      sx :: Stream Double+      sx = extern "relative_position_x" Nothing++      -- The relative y position between ownship and the intruder.+      sy :: Stream Double+      sy = extern "relative_position_y" Nothing++      -- The relative z position between ownship and the intruder.+      sz :: Stream Double+      sz = extern "relative_position_z" Nothing++      -- The relative position as a 2D vector.+      s :: (Stream Double, Stream Double)+      s = (sx, sy)   Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))   -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))   trigger "well_clear_violation" (wcv tep s sz v vz) []

@@ -255,7 +255,7 @@      Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile       -- Run the main verification procedure-     verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile+     verifyBitcode opts csettings properties spec cruxOpts llvmOpts csrc bcFile   -- | Do the (surprisingly large amount) of options munging necessary to set up@@ -325,9 +325,10 @@   Spec        {- ^ The input Copilot specification -} ->   CruxOptions {- ^ Crux options -} ->   LLVMOptions {- ^ CruxLLVM options -} ->+  FilePath    {- ^ Path to the generated C file (for logging purposes only) -} ->   FilePath    {- ^ Path to the bitcode file to verify -} ->   IO ()-verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile =+verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile =   do -- Set up the expression builder and symbolic backend      halloc <- newHandleAllocator      sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator@@ -383,13 +384,28 @@           -- First check that the initial state of the program matches the starting           -- segment of the associated Copilot streams.           let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts-          verifyInitialState cruxOptsInit adapters clRefs simctx initialMem-             (CW4.initialStreamState proofStateBundle)+          initGoals <-+            verifyInitialState cruxOptsInit adapters clRefs simctx initialMem+              (CW4.initialStreamState proofStateBundle)            -- Now, the real meat. Carry out the bisimulation step of the proof.           let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts-          verifyStepBisimulation opts cruxOptsTrans adapters csettings-             clRefs simctx llvmMod trans memVar initialMem proofStateBundle+          bisimGoals <-+            verifyStepBisimulation opts cruxOptsTrans adapters csettings+              clRefs simctx llvmMod trans memVar initialMem proofStateBundle++          Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals bisimGoals+          -- We only want to inform users about Noisy if the verbosity level is+          -- sufficiently low. Crux's logging framework isn't particularly+          -- suited to doing this, as it assumes that all log messages enabled+          -- for low verbosity levels should also be enabled for higher+          -- verbosity levels. That is a reasonable assumption most of the time,+          -- but not here.+          --+          -- To compensate, we hack around the issue by manually checking the+          -- verbosity level before logging the message.+          when (verbosity opts < Noisy) $+            Log.sayCopilot Log.NoisyVerbositySuggestion   where     -- If @logSmtInteractions@ is enabled, enable offline solver output in the     -- supplied 'CruxOptions' with the supplied file template. Otherwise, return@@ -433,7 +449,7 @@   SimCtxt Crux sym LLVM ->   MemImpl sym ->   CW4.BisimulationProofState sym ->-  IO ()+  IO Integer verifyInitialState cruxOpts adapters clRefs simctx mem initialState =   withBackend simctx $ \bak ->   do Log.sayCopilot $ Log.ComputingConditions Log.InitialState@@ -473,7 +489,7 @@   GlobalVar Mem ->   MemImpl sym ->   CW4.BisimulationProofBundle sym ->-  IO ()+  IO Integer verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod modTrans memVar mem prfbundle =   withBackend simctx $ \bak ->   do Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation@@ -1279,7 +1295,7 @@   CopilotLogRefs sym ->   Log.VerificationStep ->   SimCtxt Crux sym LLVM ->-  IO ()+  IO Integer proveObls cruxOpts adapters clRefs step simctx =   withBackend simctx $ \bak ->   do let sym = backendGetSym bak@@ -1300,6 +1316,9 @@ summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList obls) -} +-- | Compute the number of goals that were proven during verification, logging+-- the goals as they are proven. If all goals are proven successfully, return+-- the number of goals. Otherwise, log the failing proof goals and abort. presentResults ::   Log.Logs msgs =>   Log.SupportsCopilotLogMessage msgs =>@@ -1309,15 +1328,17 @@   LLVMAnnMap sym ->   Log.VerificationStep ->   (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) ->-  IO ()+  IO Integer presentResults sym vaMap laMap step (num, goals)   | numTotalGoals == 0-  = Log.sayCopilot Log.AllGoalsProved+  = do Log.sayCopilot Log.AllGoalsProved+       pure 0      -- All goals were proven   | numProvedGoals == numTotalGoals   = do traverse_ (logVerifierAssertions sym vaMap laMap step num) goals        printGoals+       pure numProvedGoals      -- There were some unproved goals, so fail with exit code 1   | otherwise

@@ -81,6 +81,15 @@     -> 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@@ -448,6 +457,36 @@     [ "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 step goalIdx numTotalGoals