copilot-language 4.2 → 4.3

raw patch · 7 files changed

+48/−27 lines, 7 filesdep ~copilot-coredep ~copilot-interpreterdep ~copilot-theoremPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core, copilot-interpreter, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +7/−0
• copilot-language.cabal +4/−4
• src/Copilot/Language/Analyze.hs +11/−2
• src/Copilot/Language/Operators/Array.hs +1/−14
• src/Copilot/Language/Operators/Projection.hs +1/−1
• src/Copilot/Language/Reify.hs +15/−3
• src/Copilot/Language/Spec.hs +9/−3

@@ -1,3 +1,10 @@+2025-03-07+        * Version bump (4.3). (#604)+        * Fix typo in documentation. (#587)+        * Record how a Property's underlying proposition is quantified. (#254)+        * Remove deprecated function Copilot.Language.Operators.Array.(.!!).+          (#599)+ 2025-01-07         * Version bump (4.2). (#577)         * Bump upper version constraint on containers. (#570)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             4.2+version:             4.3 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:@@ -42,9 +42,9 @@                , data-reify            >= 0.6  && < 0.7                , mtl                   >= 2.0  && < 3 -               , copilot-core          >= 4.2 && < 4.3-               , copilot-interpreter   >= 4.2 && < 4.3-               , copilot-theorem       >= 4.2 && < 4.3+               , copilot-core          >= 4.3 && < 4.4+               , copilot-interpreter   >= 4.3 && < 4.4+               , copilot-theorem       >= 4.3 && < 4.4    exposed-modules: Copilot.Language                  , Copilot.Language.Operators.BitWise

@@ -110,7 +110,11 @@ -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeProperty :: IORef Env -> Property -> IO ()-analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e+analyzeProperty refStreams (Property _ p) =+  -- Soundness note: it is OK to call `extractProp` here to drop the quantifier+  -- from the proposition `p`, as the analysis does not depend on what the+  -- quantifier is.+  analyzeExpr refStreams (extractProp p)  data SeenExtern = NoExtern                 | SeenFun@@ -291,7 +295,12 @@           env' args    propertyExts :: ExternEnv -> Property -> IO ExternEnv-  propertyExts env (Property _ stream) = collectExts refStreams stream env+  propertyExts env (Property _ p) =+    -- Soundness note: it is OK to call `extractProp` here to drop the+    -- quantifier from the proposition `p`. This is because we are simply+    -- gathering externs from `p`, and the presence of externs does not depend+    -- on what the quantifier is.+    collectExts refStreams (extractProp p) env    theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv   theoremExts env (p, _) = propertyExts env p

@@ -8,8 +8,7 @@  -- | Combinators to deal with streams carrying arrays. module Copilot.Language.Operators.Array-  ( (.!!)-  , (!)+  ( (!)   , (!!)   , (=:)   , (=$)@@ -33,18 +32,6 @@ (!) :: (KnownNat n, Typed t)     => Stream (Array n t) -> Stream Word32 -> Stream t arr ! n = Op2 (Index typeOf) arr n---- | Create a stream that carries an element of an array in another stream.------ This function implements a projection of the element of an array at a given--- position, over time. For example, if @s@ is a stream of type @Stream (Array--- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd--- element (starting from zero) of the arrays in @s@ at any point in time.-{-# DEPRECATED (.!!) "This function is deprecated in Copilot 4. Use (!)." #-}-(.!!) :: ( KnownNat n-         , Typed t-         ) => Stream (Array n t) -> Stream Word32 -> Stream t-(.!!) = (!)  -- | Pair a stream with an element accessor, without applying it to obtain the -- value of the element.

@@ -23,7 +23,7 @@ -- | Common interface to manipulate portions of a larger data structure. -- -- A projectable d s t means that it is possible to manipulate a sub-element s--- of type t carried in a stream of type d..+-- of type t carried in a stream of type d. class Projectable d s t | d s -> t where    -- | Unapplied projection or element access on a type.

@@ -4,6 +4,7 @@ -- specification.  {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs                     #-} {-# LANGUAGE Rank2Types                #-} {-# LANGUAGE Safe                      #-} @@ -105,11 +106,22 @@   -> IORef [Core.Stream]   -> Property   -> IO Core.Property-mkProperty refMkId refStreams refMap (Property name guard) = do-  w1 <- mkExpr refMkId refStreams refMap guard+mkProperty refMkId refStreams refMap (Property name p) = do+  p' <- mkProp refMkId refStreams refMap p   return Core.Property     { Core.propertyName  = name-    , Core.propertyExpr  = w1 }+    , Core.propertyProp  = p' }++-- | Transform a Copilot proposition into a Copilot Core proposition.+mkProp :: IORef Int+       -> IORef (Map Core.Id)+       -> IORef [Core.Stream]+       -> Prop a+       -> IO Core.Prop+mkProp refMkId refStreams refMap prop =+  case prop of+    Forall e -> Core.Forall <$> mkExpr refMkId refStreams refMap e+    Exists e -> Core.Exists <$> mkExpr refMkId refStreams refMap e  -- | Transform a Copilot stream expression into a Copilot Core expression. {-# INLINE mkExpr #-}

@@ -153,7 +153,7 @@ -- | A property, representing a boolean stream that is existentially or -- universally quantified over time. data Property where-  Property :: String -> Stream Bool -> Property+  Property :: String -> Prop a -> Property  -- | A proposition, representing the quantification of a boolean streams over -- time.@@ -170,6 +170,12 @@ exists = Exists  -- | Extract the underlying stream from a quantified proposition.+--+-- Think carefully before using this function, as this function will remove the+-- quantifier from a proposition. Universally quantified streams usually require+-- separate treatment from existentially quantified ones, so carelessly using+-- this function to remove quantifiers can result in hard-to-spot soundness+-- bugs. extractProp :: Prop a -> Stream Bool extractProp (Forall p) = p extractProp (Exists p) = p@@ -180,7 +186,7 @@ -- This function returns, in the monadic context, a reference to the -- proposition. prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)-prop name e = tell [PropertyItem $ Property name (extractProp e)]+prop name e = tell [PropertyItem $ Property name e]   >> return (PropRef name)  -- | A theorem, or proposition together with a proof.@@ -188,7 +194,7 @@ -- This function returns, in the monadic context, a reference to the -- proposition. theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)-theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]+theorem name e (Proof p) = tell [TheoremItem (Property name e, p)]   >> return (PropRef name)  -- | Construct a function argument from a stream.