LTL helper functions

CHANGELOG.md

@@ -13,6 +13,24 @@
 - A new documentation file around optics, in `doc/OPTICS.md`
 - New `forceOutputs` primitives to force the creation of new utxos from a list
   of `TxSkel`. Initial distributions are now handled using this primitive.
+- Added `somewhere'`, `everywhere'` and `there'` which accept arbitrary `Ltl`
+  expressions. 
+- Added `labeled` helper, which applies a tweak to every transaction that's
+  been labeled with a certain value.
+- Added `Cooked.Ltl.Combinators` with `anyOf[']` and `allOf[']` helpers to 
+  make combining multiple Ltl expressions together simpler:
+
+  ```haskell
+  someTest = someTrace 
+    & everywhere' (anyOf 
+      [ UntypedTweak doubleSatAttack
+      , UntypedTweak addTokenAttack
+      , UntypedTweak customAttack ]
+      )
+
+  tweakOneWorkflow = someTrace 
+    & labeled @Text "SomeWorkflow" someTweak
+  ```
 
 ### Removed
 

cooked-validators.cabal

@@ -20,6 +20,7 @@ library
       Cooked.Attack.DupToken
       Cooked.InitialDistribution
       Cooked.Ltl
+      Cooked.Ltl.Combinators
       Cooked.MockChain
       Cooked.MockChain.AutoReferenceScripts
       Cooked.MockChain.Balancing

src/Cooked.hs

@@ -5,6 +5,7 @@ module Cooked (module X) where
 import Cooked.Attack as X
 import Cooked.InitialDistribution as X
 import Cooked.Ltl as X (Ltl (..), MonadModal (..), ltlDelay)
+import Cooked.Ltl.Combinators as X (delay)
 import Cooked.MockChain as X
 import Cooked.Pretty as X
 import Cooked.ShowBS as X

src/Cooked/Ltl.hs

@@ -69,6 +69,8 @@ data Ltl a
     LtlRelease (Ltl a) (Ltl a)
   deriving (Show)
 
+{-# DEPRECATED ltlDelay "Use Cooked.Ltl.Combinators.delay instead" #-}
+
 -- | Delays a Ltl formula by @n@ time steps when @n > 0@
 ltlDelay :: Integer -> Ltl a -> Ltl a
 ltlDelay n | n <= 0 = id

src/Cooked/Ltl/Combinators.hs

@@ -0,0 +1,57 @@
+-- | This module provides helpers for writing common LTL expressions.
+module Cooked.Ltl.Combinators
+  ( anyOf,
+    allOf,
+    anyOf',
+    allOf',
+    delay,
+    eventually,
+    eventually',
+    always,
+    always',
+  )
+where
+
+import Cooked.Ltl (Ltl (..))
+
+-- | Produce an Ltl expression which branches on any of the provided
+-- inputs. It will not attempt combinations, only one input will be
+-- applied in any branch. See 'LtlOr'.
+anyOf :: [a] -> Ltl a
+anyOf = anyOf' . map LtlAtom
+
+-- | Combine a set of Ltl expressions into one where any of them may succeed.
+-- Creates a branch for each input. See 'LtlOr' for the semantics of branching.
+anyOf' :: [Ltl a] -> Ltl a
+anyOf' = foldr LtlOr LtlFalsity
+
+-- | Produce an Ltl expression which applies all the provided inputs. All must
+-- apply for this to succeed. See 'LtlAnd'.
+allOf :: [a] -> Ltl a
+allOf = allOf' . map LtlAtom
+
+-- | Combine a set of Ltl expressions into one where all must succeed. See
+-- 'LtlAnd' for semantics of conjunction.
+allOf' :: [Ltl a] -> Ltl a
+allOf' = foldr LtlAnd LtlTruth
+
+-- | Delays a Ltl formula by @n@ time steps when @n > 0@
+delay :: Integer -> Ltl a -> Ltl a
+delay n | n <= 0 = id
+delay n = LtlNext . delay (n - 1)
+
+-- | Apply a modification once somewhere.
+eventually :: a -> Ltl a
+eventually = eventually' . LtlAtom
+
+-- | Apply an Ltl expression once somewhere.
+eventually' :: Ltl a -> Ltl a
+eventually' = LtlUntil LtlTruth
+
+-- | Apply a modification everywhere.
+always :: a -> Ltl a
+always = always' . LtlAtom
+
+-- | Apply an Ltl expression everywhere.
+always' :: Ltl a -> Ltl a
+always' = LtlRelease LtlFalsity

src/Cooked/MockChain/Staged.hs

@@ -12,27 +12,35 @@ module Cooked.MockChain.Staged
     MonadModalBlockChain,
     InterpMockChain,
     somewhere,
+    somewhere',
     runTweak,
     everywhere,
+    everywhere',
     withTweak,
     there,
+    there',
+    labelled,
+    labelled',
   )
 where
 
 import Cardano.Node.Emulator qualified as Emulator
 import Control.Applicative
-import Control.Monad (MonadPlus (..), msum)
+import Control.Monad (MonadPlus (..), guard, msum)
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
 import Cooked.InitialDistribution
 import Cooked.Ltl
+import Cooked.Ltl.Combinators (always', delay, eventually')
 import Cooked.MockChain.BlockChain
 import Cooked.MockChain.Direct
 import Cooked.Pretty.Hashable
 import Cooked.Skeleton
 import Cooked.Tweak.Common
 import Data.Default
+import Data.Set qualified as Set
+import Data.Text (Text)
 import Ledger.Slot qualified as Ledger
 import Ledger.Tx qualified as Ledger
 import Plutus.Script.Utils.Address qualified as Script
@@ -161,20 +169,80 @@ runTweakFrom initDist tweak = runMockChainTFrom initDist . runTweakInChain tweak
 -- with 'Tweak's
 type MonadModalBlockChain m = (MonadBlockChain m, MonadModal m, Modification m ~ UntypedTweak InterpMockChain)
 
+fromTweak :: Tweak m a -> Ltl (UntypedTweak m)
+fromTweak = LtlAtom . UntypedTweak
+
 -- | Apply a 'Tweak' to some transaction in the given Trace. The tweak must
 -- apply at least once.
 somewhere :: (MonadModalBlockChain m) => Tweak InterpMockChain b -> m a -> m a
-somewhere = modifyLtl . LtlUntil LtlTruth . LtlAtom . UntypedTweak
+somewhere = somewhere' . fromTweak
+
+-- | Apply an Ltl modification somewhere in the given Trace. The modification
+-- must apply at least once.
+somewhere' :: (MonadModal m) => Ltl (Modification m) -> m a -> m a
+somewhere' = modifyLtl . eventually'
 
 -- | Apply a 'Tweak' to every transaction in a given trace. This is also
 -- successful if there are no transactions at all.
 everywhere :: (MonadModalBlockChain m) => Tweak InterpMockChain b -> m a -> m a
-everywhere = modifyLtl . LtlRelease LtlFalsity . LtlAtom . UntypedTweak
+everywhere = everywhere' . fromTweak
+
+-- | Apply an Ltl modification everywhere it can be (including nowhere if it
+-- does not apply). If the modification branches, this will branch at every
+-- location the modification can be applied.
+everywhere' :: (MonadModal m) => Ltl (Modification m) -> m a -> m a
+everywhere' = modifyLtl . always'
 
 -- | Apply a 'Tweak' to the (0-indexed) nth transaction in a given
 -- trace. Successful when this transaction exists and can be modified.
 there :: (MonadModalBlockChain m) => Integer -> Tweak InterpMockChain b -> m a -> m a
-there n = modifyLtl . ltlDelay n . LtlAtom . UntypedTweak
+there n = there' n . fromTweak
+
+-- | Apply an Ltl modification to the (0-indexed) nth transaction in a
+-- given trace. Successful when this transaction exists and can be modified.
+there' :: (MonadModal m) => Integer -> Ltl (Modification m) -> m a -> m a
+there' n = modifyLtl . delay n
+
+-- | Apply a tweak to every transaction labelled with the given 'Text' value.
+-- See 'labelled'', 'TxSkelLabel' is an instrance of 'Data.String.IsString' which
+-- create 'Data.Text.Text' labels.
+--
+-- >
+-- > someEndpoint = do
+-- >   ...
+-- >   validateTxSkel' txSkelTemplate
+-- >      { txSkelLabels =
+-- >         [ "InitialMinting"
+-- >         , "AuctionWorkflow"
+-- >         , label SomeLabelType]
+-- >      }
+-- >
+-- > someTest = someEndpoint & labelled "ActionWorkflow" someTweak
+labelled :: (MonadModalBlockChain m) => Text -> Tweak InterpMockChain b -> m a -> m a
+labelled = labelled'
+
+-- | Apply a tweak to every transaction which has a specific label. This can
+-- be useful to apply a tweak to every transaction in a set of associated
+-- transactions.
+--
+-- >
+-- > someEndpoint = do
+-- >   ...
+-- >   validateTxSkel' txSkelTemplate
+-- >      { txSkelLabels =
+-- >         [ "InitialMinting"
+-- >         , "AuctionWorkflow"
+-- >         , label SomeLabelType]
+-- >      }
+-- >
+-- > someTest = someEndpoint & labelled' SomeLabelType someTweak
+labelled' :: (LabelConstrs lbl, MonadModalBlockChain m) => lbl -> Tweak InterpMockChain b -> m a -> m a
+labelled' lbl tweak = everywhere (hasLabel >> tweak)
+  where
+    hasLabel = do
+      -- using 'hasLabelTweak' causes a cyclic dependency
+      lbls <- viewTweak txSkelLabelL
+      guard (Set.member (TxSkelLabel lbl) lbls)
 
 -- | Apply a 'Tweak' to the next transaction in the given trace. The order of
 -- arguments is reversed compared to 'somewhere' and 'everywhere', because that

src/Cooked/Pretty/Class.hs

@@ -24,6 +24,7 @@ import Data.Maybe (catMaybes)
 import Data.Ratio
 import Data.Set (Set)
 import Data.Set qualified as Set
+import Data.Text (Text)
 import Numeric qualified
 import PlutusTx.Builtins.Internal qualified as PlutusTx
 import Prettyprinter (Doc, (<+>))
@@ -178,3 +179,6 @@ instance PrettyCooked () where
 
 instance PrettyCooked Rational where
   prettyCookedOpt opts q = "(" <+> prettyCookedOpt opts (numerator q) <+> "/" <+> prettyCookedOpt opts (denominator q) <+> ")"
+
+instance PrettyCooked Text where
+  prettyCookedOpt _ = PP.pretty

src/Cooked/Skeleton/Label.hs

@@ -4,10 +4,13 @@ module Cooked.Skeleton.Label
   ( LabelConstrs,
     TxSkelLabel (..),
     txSkelLabelTypedP,
+    label,
   )
 where
 
 import Cooked.Pretty.Class
+import Data.String (IsString (..))
+import Data.Text (pack)
 import Data.Typeable (cast)
 import Optics.Core
 import Type.Reflection
@@ -18,9 +21,17 @@ type LabelConstrs x = (PrettyCooked x, Show x, Typeable x, Eq x, Ord x)
 -- | Labels are arbitrary information that can be added to skeleton. They are
 -- meant to be pretty-printed. The common use case we currently have is to tag
 -- skeletons that have been modified by tweaks and automated attacks.
+--
+-- The 'IsString' instance will add a 'Data.Text.Text' label, which can
+-- be used with 'Cooked.MockChain.Staged.labelled' to apply tweaks
+-- to arbitrary transactions annotated with a label.
 data TxSkelLabel where
   TxSkelLabel :: (LabelConstrs x) => x -> TxSkelLabel
 
+-- | Helper for defining 'TxSkelLabel' values.
+label :: (LabelConstrs x) => x -> TxSkelLabel
+label = TxSkelLabel
+
 instance Eq TxSkelLabel where
   a == x = compare a x == EQ
 
@@ -43,3 +54,7 @@ txSkelLabelTypedP =
   prism
     TxSkelLabel
     (\txSkelLabel@(TxSkelLabel lbl) -> maybe (Left txSkelLabel) Right (cast lbl))
+
+-- | Turn a literal string into a 'Data.Text.Text' label, to be used with 'Cooked.MockChain.Staged.labelled'.
+instance IsString TxSkelLabel where
+  fromString = TxSkelLabel . pack

src/Cooked/Tweak/Common.hs

@@ -127,7 +127,7 @@ viewAllTweak optic = getTxSkel <&> toListOf optic
 
 -- | The tweak that sets a certain value in the 'TxSkel'.
 setTweak :: (MonadTweak m, Is k A_Setter) => Optic' k is TxSkel a -> a -> m ()
-setTweak optic newValue = getTxSkel >>= putTxSkel . set optic newValue
+setTweak optic = overTweak optic . const
 
 -- | The tweak that modifies a certain value in the 'TxSkel'.
 overTweak :: (MonadTweak m, Is k A_Setter) => Optic' k is TxSkel a -> (a -> a) -> m ()

src/Cooked/Tweak/Labels.hs

@@ -22,6 +22,6 @@ hasLabelTweak = (viewTweak txSkelLabelL <&>) . Set.member . TxSkelLabel
 
 -- | Removes a label from a 'TxSkel' when possible, fails otherwise
 removeLabelTweak :: (MonadTweak m, LabelConstrs x) => x -> m ()
-removeLabelTweak label = do
-  hasLabelTweak label >>= guard
-  overTweak txSkelLabelL . Set.delete $ TxSkelLabel label
+removeLabelTweak lbl = do
+  hasLabelTweak lbl >>= guard
+  overTweak txSkelLabelL . Set.delete $ TxSkelLabel lbl