Replaced Apropos Property testing with PQ and PCB for MultiSig

Makefile

@@ -48,7 +48,7 @@ tag:
 	hasktags -x agora agora-bench agora-test agora-testlib agora-sample agora-purescript-bridge
 
 lint:
-	hlint agora agora-bench agora-test agora-testlib agora-sample agora-purescript-bridge
+	hlint agora agora-bench agora-test agora-testlib agora-specs agora-purescript-bridge
 
 PS_BRIDGE_OUTPUT_DIR := agora-purescript-bridge/
 ps_bridge:

agora-specs/Property/MultiSig.hs

@@ -0,0 +1,113 @@
+{- |
+Module     : Property.MultiSig
+Maintainer : seungheon.ooh@gmail.com
+Description: Property tests for 'MultiSig' functions
+
+Property model and tests for 'MultiSig' functions
+-}
+module Property.MultiSig (props) where
+
+import Agora.MultiSig (
+  MultiSig (MultiSig),
+  PMultiSig,
+  pvalidatedByMultisig,
+ )
+import Agora.Utils (tclet)
+import Data.Maybe (fromJust)
+import Data.Tagged (Tagged (Tagged))
+import Data.Universe (Finite (..), Universe (..))
+import Plutarch.Api.V1 (PScriptContext)
+import Plutarch.Context.Config (defaultConfig)
+import Plutarch.Context.Spending (
+  ValidatorUTXO (ValidatorUTXO),
+  inputSelfExtra,
+  signedWith,
+  spendingContext,
+ )
+import Plutus.V1.Ledger.Api (
+  ScriptContext (scriptContextTxInfo),
+  TxInfo (txInfoSignatories),
+ )
+import Spec.Generator (genAnyValue, genPubKeyHash)
+import Test.Tasty (TestTree)
+import Test.Tasty.Plutarch.Property (classifiedProperty)
+import Test.Tasty.QuickCheck (
+  Gen,
+  Property,
+  chooseInt,
+  listOf,
+  testProperty,
+  vectorOf,
+ )
+
+-- | apropos model for testing multisigs.
+type MultiSigModel = (MultiSig, ScriptContext)
+
+-- | Propositions that may hold true of a `MultiSigModel`.
+data MultiSigProp
+  = -- | Sufficient number of signatories in the script context.
+    MeetsMinSigs
+  | -- | Insufficient number of signatories in the script context.
+    DoesNotMeetMinSigs
+  deriving stock (Eq, Show, Ord)
+
+instance Universe MultiSigProp where
+  universe = [MeetsMinSigs, DoesNotMeetMinSigs]
+
+instance Finite MultiSigProp where
+  universeF = universe
+  cardinality = Tagged 2
+
+-- | Generate model with given proposition.
+genMultiSigProp :: MultiSigProp -> Gen MultiSigModel
+genMultiSigProp prop = do
+  size <- chooseInt (4, 20)
+  pkhs <- vectorOf size genPubKeyHash
+  vutxo <- pure . ValidatorUTXO () <$> genAnyValue
+  minSig <- chooseInt (1, length pkhs)
+  othersigners <- take 20 <$> listOf genPubKeyHash
+
+  let ms = MultiSig pkhs (toInteger minSig)
+
+  n <- case prop of
+    MeetsMinSigs -> chooseInt (minSig, length pkhs)
+    DoesNotMeetMinSigs -> chooseInt (0, minSig - 1)
+
+  let builder = foldr (<>) (inputSelfExtra mempty ()) (signedWith <$> take n pkhs <> othersigners)
+      ctx = fromJust $ spendingContext defaultConfig builder vutxo
+  pure (ms, ctx)
+
+-- | Classify model into propositions.
+classifyMultiSigProp :: MultiSigModel -> MultiSigProp
+classifyMultiSigProp (MultiSig keys (fromIntegral -> minsig), ctx)
+  | minsig <= length signer = MeetsMinSigs
+  | otherwise = DoesNotMeetMinSigs
+  where
+    signer = filter (`elem` keys) $ txInfoSignatories . scriptContextTxInfo $ ctx
+
+-- | Shrinker. Not used.
+shrinkMultiSigProp :: MultiSigModel -> [MultiSigModel]
+shrinkMultiSigProp = const []
+
+expected :: Term s (PBuiltinPair PMultiSig PScriptContext :--> PMaybe PBool)
+expected = plam $ \x -> unTermCont $ do
+  ms <- tclet $ pfstBuiltin # x
+  sc <- tclet $ psndBuiltin # x
+  multsig <- tcont $ pletFields @'["keys", "minSigs"] ms
+  let signers = pfromData $ pfield @"signatories" #$ pfromData (pfield @"txInfo" # sc)
+      validSigners = plength #$ pfilter # plam (\x -> pelem # x # multsig.keys) # signers
+  pure $ pcon $ PJust $ pfromData multsig.minSigs #<= validSigners
+
+actual :: Term s (PBuiltinPair PMultiSig PScriptContext :--> PBool)
+actual = plam $ \x -> unTermCont $ do
+  ms <- tclet $ pfstBuiltin # x
+  sc <- tclet $ psndBuiltin # x
+  pure $ pvalidatedByMultisig # ms # (pfield @"txInfo" # sc)
+
+prop :: Property
+prop = classifiedProperty genMultiSigProp shrinkMultiSigProp expected classifyMultiSigProp actual
+
+props :: [TestTree]
+props =
+  [ testProperty "MultiSig property" prop
+  ]

agora-specs/Spec/Generator.hs

@@ -0,0 +1,103 @@
+{- |
+Module     : Spec.Generator
+Maintainer : seungheon.ooh@gmail.com
+Description: Generic generators for property tests
+
+Shared generators for all Agora property tests
+-}
+module Spec.Generator (
+  -- * Credentials
+  genPubKeyHash,
+  genUserCredential,
+  genScriptCredential,
+  genCredential,
+  genAddress,
+
+  -- * Values
+  genValue,
+  genAssetClass,
+  genAnyValue,
+
+  -- * Tx info
+  genTxOut,
+  genTxInInfo,
+) where
+
+import Control.Applicative (Applicative (liftA2))
+import Data.ByteString.Char8 qualified as C (ByteString, pack)
+import Data.ByteString.Hash (sha2)
+import Plutus.V1.Ledger.Api (
+  Address (Address),
+  Credential (..),
+  DatumHash (DatumHash),
+  PubKeyHash (PubKeyHash),
+  TxInInfo (TxInInfo),
+  TxOut (..),
+  TxOutRef (TxOutRef),
+  ValidatorHash (ValidatorHash),
+  Value,
+  toBuiltin,
+ )
+import Plutus.V1.Ledger.Value (
+  AssetClass (AssetClass),
+  assetClassValue,
+  currencySymbol,
+  tokenName,
+ )
+import Test.QuickCheck (
+  Arbitrary (arbitrary),
+  Gen,
+  chooseAny,
+  elements,
+  listOf,
+  listOf1,
+  oneof,
+ )
+
+{- | Generate a random Hash
+Hashs cannot be shrunken; functions utilizing this function,
+therefore, cannot be shrunken as well.
+-}
+genHashByteString :: Gen C.ByteString
+genHashByteString = sha2 . C.pack . show <$> (chooseAny :: Gen Integer)
+
+-- TODO: How do I need to ensure uniqueness?
+
+-- | Random PubKeyHash
+genPubKeyHash :: Gen PubKeyHash
+genPubKeyHash = PubKeyHash . toBuiltin <$> genHashByteString
+
+-- | Random user credential.
+genUserCredential :: Gen Credential
+genUserCredential = PubKeyCredential . PubKeyHash . toBuiltin <$> genHashByteString
+
+-- | Random script credential.
+genScriptCredential :: Gen Credential
+genScriptCredential = ScriptCredential . ValidatorHash . toBuiltin <$> genHashByteString
+
+-- | Random credential: combination of user and script credential generators.
+genCredential :: Gen Credential
+genCredential = oneof [genUserCredential, genScriptCredential]
+
+genAddress :: Gen Address
+genAddress = flip Address Nothing <$> genCredential
+
+{- | Random Value of given AssetClass
+`genAnyValue` will create a random value with a random assetclass.
+-}
+genValue :: AssetClass -> Gen Value
+genValue ac = assetClassValue ac . abs <$> (arbitrary :: Gen Integer)
+
+genPrettyByteString :: Gen C.ByteString
+genPrettyByteString = C.pack <$> listOf1 (elements ['a' .. 'z'])
+
+genAssetClass :: Gen AssetClass
+genAssetClass =
+  AssetClass
+    <$> liftA2
+      (,)
+      (currencySymbol <$> genHashByteString)
+      (tokenName <$> genPrettyByteString)
+
+genAnyValue :: Gen Value
+genAnyValue = genAssetClass >>= genValue

agora-specs/Spec/Model/MultiSig.hs

@@ -1,194 +0,0 @@
-{- |
-Module     : Spec.Model.MultiSig
-Maintainer : emi@haskell.fyi
-Description: apropos-tx model and tests for 'MultiSig' functions
-
-apropos-tx model and tests for 'MultiSig' functions
--}
-module Spec.Model.MultiSig (
-  plutarchTests,
-  genTests,
-) where
-
-import Data.List (intersect)
-
---------------------------------------------------------------------------------
-
-import Plutus.V1.Ledger.Api (
-  Script,
-  ScriptContext (scriptContextPurpose),
-  ScriptPurpose (Spending),
-  TxInfo (
-    txInfoDCert,
-    txInfoData,
-    txInfoFee,
-    txInfoId,
-    txInfoInputs,
-    txInfoMint,
-    txInfoOutputs,
-    txInfoValidRange,
-    txInfoWdrl
-  ),
-  TxOutRef (TxOutRef),
-  scriptContextTxInfo,
-  txInfoSignatories,
- )
-import Plutus.V1.Ledger.Contexts (ScriptContext (ScriptContext), TxInfo (TxInfo))
-import Plutus.V1.Ledger.Crypto (PubKeyHash)
-import Plutus.V1.Ledger.Interval qualified as Interval
-import Plutus.V1.Ledger.Value qualified as Value
-
---------------------------------------------------------------------------------
-
-import Apropos (
-  Apropos (Apropos),
-  Formula (ExactlyOne, Var, Yes),
-  HasLogicalModel (..),
-  HasParameterisedGenerator,
-  LogicalModel (logic),
-  parameterisedGenerator,
-  runGeneratorTestsWhere,
-  (:+),
- )
-import Apropos.Gen (Gen, choice, int, linear, list)
-import Apropos.LogicalModel (Enumerable)
-import Apropos.LogicalModel.Enumerable (Enumerable (enumerated))
-import Apropos.Script (ScriptModel (expect, runScriptTestsWhere, script))
-import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.Hedgehog (fromGroup)
-
---------------------------------------------------------------------------------
-
-import Agora.MultiSig (MultiSig (..), validatedByMultisig)
-
---------------------------------------------------------------------------------
-
--- | apropos model for testing multisigs.
-data MultiSigModel = MultiSigModel
-  { ms :: MultiSig
-  -- ^ `MultiSig` value to be tested.
-  , ctx :: ScriptContext
-  -- ^ The `ScriptContext` of the transaction.
-  }
-  deriving stock (Eq, Show)
-
--- | Propositions that may hold true of a `MultiSigModel`.
-data MultiSigProp
-  = -- | Sufficient number of signatories in the script context.
-    MeetsMinSigs
-  | -- | Insufficient number of signatories in the script context.
-    DoesNotMeetMinSigs
-  deriving stock (Eq, Show, Ord)
-
-instance Enumerable MultiSigProp where
-  enumerated = [MeetsMinSigs, DoesNotMeetMinSigs]
-
-instance LogicalModel MultiSigProp where
-  -- Only logical relationship between the two propositions is
-  -- that exactly one of them holds for a given model.
-  logic = ExactlyOne [Var MeetsMinSigs, Var DoesNotMeetMinSigs]
-
-instance HasLogicalModel MultiSigProp MultiSigModel where
-  satisfiesProperty :: MultiSigProp -> MultiSigModel -> Bool
-  satisfiesProperty p m =
-    let minSigs = m.ms.minSigs
-        signatories = txInfoSignatories $ scriptContextTxInfo $ m.ctx
-        matchingSigs = intersect m.ms.keys signatories
-     in case p of
-          MeetsMinSigs -> length matchingSigs >= fromInteger minSigs
-          DoesNotMeetMinSigs -> length matchingSigs < fromInteger minSigs
-
-{- | Given a list of key hashes, returns a dummy `ScriptContext`,
-     with those hashes as signatories.
--}
-contextWithSignatures :: [PubKeyHash] -> ScriptContext
-contextWithSignatures sigs =
-  ScriptContext
-    { scriptContextTxInfo =
-        TxInfo
-          { txInfoInputs = []
-          , txInfoOutputs = []
-          , txInfoFee = Value.singleton "" "" 2
-          , txInfoMint = mempty
-          , txInfoDCert = []
-          , txInfoWdrl = []
-          , txInfoValidRange = Interval.always
-          , txInfoSignatories = sigs
-          , txInfoData = []
-          , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
-          }
-    , scriptContextPurpose = Spending (TxOutRef "" 0)
-    }
-
--- | Generator returning one of four dummy public key hashes.
-genPK :: Gen PubKeyHash
-genPK =
-  choice
-    [ pure "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
-    , pure "0b12051dd2da4b3629cebb92e2be111e0e99c63c04727ed55b74a296"
-    , pure "87f5f31e4d7437463cd901c4c9edb7a51903ac858661503e9d72f492"
-    , pure "f74ccaee8244264b3c73fce3b66bd2337de3db70efff4261d6ff145b"
-    ]
-
-instance HasParameterisedGenerator MultiSigProp MultiSigModel where
-  parameterisedGenerator s = do
-    -- Gen between one and four signatures for the `MultiSig`.
-    expectedSignatures <- list (linear 1 4) genPK
-
-    -- Gen the value of `MultiSig.minSigs`.
-    minSigs <- toInteger <$> int (linear 1 (length expectedSignatures))
-
-    -- Assign values to msig.
-    let msig = MultiSig expectedSignatures minSigs
-
-    actualSignaturesLength <-
-      -- If we would like to generate a MultiSig model which passes...
-      if MeetsMinSigs `elem` s
-        then -- ... have a sufficient number of signatories.
-          int (linear (fromInteger minSigs) (length expectedSignatures))
-        else -- ... have zero signatories.
-          pure 0
-
-    -- Get a list of signatories for the script context.
-    let actualSignatures = take actualSignaturesLength expectedSignatures
-
-    let ctx = contextWithSignatures actualSignatures
-
-    -- Return the generated model.
-    pure (MultiSigModel msig ctx)
-
-instance ScriptModel MultiSigProp MultiSigModel where
-  -- When the script runs, we want the model to meet the minimum signatures.
-  expect :: (MultiSigModel :+ MultiSigProp) -> Formula MultiSigProp
-  expect Apropos = Var MeetsMinSigs
-
-  -- Function making a valid script from the model and propositions.
-  script :: (MultiSigModel :+ MultiSigProp) -> MultiSigModel -> Script
-  script Apropos msm =
-    compile $
-      pif
-        (validatedByMultisig msm.ms # pconstant msm.ctx.scriptContextTxInfo)
-        (pcon PUnit)
-        perror
-
--- | Consistency tests for the 'HasParameterisedGenerator' instance of 'MultiSigModel'.
-genTests :: TestTree
-genTests =
-  testGroup "genTests" $
-    fromGroup
-      <$> [ runGeneratorTestsWhere
-              (Apropos :: MultiSigModel :+ MultiSigProp)
-              "Generator"
-              Yes
-          ]
-
--- | Tests for the 'ScriptModel' instance of 'MultiSigModel'.
-plutarchTests :: TestTree
-plutarchTests =
-  testGroup "plutarchTests" $
-    fromGroup
-      <$> [ runScriptTestsWhere
-              (Apropos :: MultiSigModel :+ MultiSigProp)
-              "ScriptValid"
-              Yes
-          ]

agora-test/Spec.hs

@@ -7,11 +7,11 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
+import Property.MultiSig qualified as MultiSig
 import Spec.AuthorityToken qualified as AuthorityToken
 import Spec.Effect.GovernorMutation qualified as GovernorMutation
 import Spec.Effect.TreasuryWithdrawal qualified as TreasuryWithdrawal
 import Spec.Governor qualified as Governor
-import Spec.Model.MultiSig qualified as MultiSig
 import Spec.Proposal qualified as Proposal
 import Spec.Stake qualified as Stake
 import Spec.Treasury qualified as Treasury
@@ -42,10 +42,5 @@ main = do
           Utils.tests
       , testGroup
           "Multisig tests"
-          [ testGroup
+          MultiSig.props
-              "MultiSig"
-              [ MultiSig.plutarchTests
-              , MultiSig.genTests
-              ]
-          ]
       ]

agora.cabal

@@ -121,12 +121,15 @@ common test-deps
     , apropos-tx
     , data-default-class
     , mtl
+    , plutarch-context-builder
+    , plutarch-quickcheck
     , QuickCheck
     , quickcheck-instances
     , tasty
     , tasty-hedgehog
     , tasty-hunit
     , tasty-quickcheck
+    , universe
 
 common exe-opts
   ghc-options: -threaded -rtsopts -with-rtsopts=-N -O0
@@ -174,6 +177,7 @@ library agora-testlib
 library agora-specs
   import:          lang, deps, test-deps
   exposed-modules:
+    Property.MultiSig
     Sample.Effect.GovernorMutation
     Sample.Effect.TreasuryWithdrawal
     Sample.Governor
@@ -184,8 +188,8 @@ library agora-specs
     Spec.AuthorityToken
     Spec.Effect.GovernorMutation
     Spec.Effect.TreasuryWithdrawal
+    Spec.Generator
     Spec.Governor
-    Spec.Model.MultiSig
     Spec.Proposal
     Spec.Stake
     Spec.Treasury

flake.nix

@@ -102,7 +102,7 @@
             {
               src = inputs.plutarch-context-builder;
               subdirs = [ "." ];
-            }            
+            }
             {
               src = inputs.apropos-tx;
               subdirs = [ "." ];
@@ -151,7 +151,7 @@
               # testing
               ps.tasty-quickcheck
               ps.plutarch-quickcheck
-              ps.plutarch-context-builder 
+              ps.plutarch-context-builder
               ps.apropos-tx
               ps.apropos
               ps.apropos