From f4a840b9778135c1673457ed986f2546ef01ac1e Mon Sep 17 00:00:00 2001 From: Tim Sheard Date: Mon, 4 Nov 2024 15:35:31 -0500 Subject: [PATCH] Improved the error messages when a Spec fails. The function explainSpec no longer drops explanations. Added guardTypeSpec, which catches errors earlier, so there is less noise. --- .../Constrained/Conway/ParametricSpec.hs | 1 + .../Constrained/Conway/WitnessUniverse.hs | 844 ++++++++++++++++++ .../src/Constrained/Base.hs | 257 ++++-- .../src/Constrained/Spec/Map.hs | 33 +- .../src/Constrained/Univ.hs | 24 +- 5 files changed, 1074 insertions(+), 85 deletions(-) create mode 100644 libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs index a0ed171c544..553aed10e73 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/ParametricSpec.hs @@ -84,6 +84,7 @@ class where irewardSpec :: Term fn AccountState -> Specification fn (InstantaneousRewards (EraCrypto era)) hasPtrs :: proxy era -> Term fn Bool + correctTxOut :: Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) -> Term fn (TxOut era) -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs new file mode 100644 index 00000000000..ea87e7c56ee --- /dev/null +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/WitnessUniverse.hs @@ -0,0 +1,844 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse where + +import qualified Cardano.Chain.Common as Byron +import Cardano.Crypto (SigningKey) +import Cardano.Crypto.Signing (toVerification) +import Cardano.Ledger.Address (BootstrapAddress (..), RewardAccount (..)) +import Cardano.Ledger.Allegra (Allegra) +import Cardano.Ledger.Allegra.Scripts ( + AllegraEraScript (..), + pattern RequireTimeExpire, + pattern RequireTimeStart, + ) +import Cardano.Ledger.Alonzo (Alonzo) +import Cardano.Ledger.Alonzo.Scripts (AsIx (..), PlutusPurpose (..)) +import Cardano.Ledger.Alonzo.TxWits (AlonzoEraTxWits (..), Redeemers (..), TxDats (..)) +import Cardano.Ledger.Babbage (Babbage) +import Cardano.Ledger.BaseTypes (Network (..), SlotNo (..)) +import Cardano.Ledger.Binary ( + DecCBOR (decCBOR), + EncCBOR (encCBOR), + ) +import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>)) +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Conway.TxCert +import Cardano.Ledger.Core +import Cardano.Ledger.Credential +import Cardano.Ledger.Crypto +import Cardano.Ledger.DRep (DRep (..)) +import Cardano.Ledger.Keys ( + BootstrapWitness, + GenDelegPair (..), + KeyHash (..), + KeyRole (..), + VKey, + WitVKey, + hashKey, + makeBootstrapWitness, + ) +import Cardano.Ledger.Mary (Mary) +import Cardano.Ledger.Plutus.Data (Data, hashData) +import Cardano.Ledger.Plutus.ExUnits (ExUnits (..)) +import Cardano.Ledger.PoolParams (PoolParams (..)) +import Cardano.Ledger.SafeHash (SafeHash, extractHash) +import Cardano.Ledger.Shelley (Shelley) +import Cardano.Ledger.Shelley.Scripts +import Cardano.Ledger.Shelley.TxCert +import Constrained hiding (Value) +import Constrained.Base (Pred (..), explainSpec, hasSize, rangeSize) + +-- import Constrained.Univ +import Control.DeepSeq (NFData (..), deepseq) +import Control.Monad (replicateM) +import qualified Data.List.NonEmpty as NE +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import qualified Data.Sequence.Strict as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import qualified Data.TreeDiff as Tree (Expr (..)) +import Data.Typeable +import GHC.Generics +import Lens.Micro +import System.IO.Unsafe +import Test.Cardano.Ledger.Allegra.TreeDiff () +import Test.Cardano.Ledger.Common (ToExpr (..)) +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger +import Test.Cardano.Ledger.Constrained.Preds.Universes (genAddrPair) +import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..), mkWitnessVKey) +import Test.Cardano.Ledger.Generic.PrettyCore +import Test.Cardano.Ledger.Generic.Proof (Reflect) +import qualified Test.Cardano.Ledger.Generic.Proof as Proof +import Test.QuickCheck hiding (forAll, witness) + +-- import Prettyprinter (Doc, Pretty (pretty),(<+>),viaShow) +-- import Data.String(fromString) + +-- =============================================== +-- Move these somewhere else? + +instance Era era => HasSimpleRep (TxDats era) where + type SimpleRep (TxDats era) = Map (DataHash (EraCrypto era)) (Data era) + toSimpleRep (TxDats m) = m + fromSimpleRep m = TxDats m + +instance (IsConwayUniv fn, Era era) => HasSpec fn (TxDats era) + +instance AlonzoEraScript era => HasSimpleRep (Redeemers era) where + type SimpleRep (Redeemers era) = Map (PlutusPurpose AsIx era) (Data era, ExUnits) + toSimpleRep (Redeemers m) = m + fromSimpleRep m = Redeemers m + +instance + ( IsConwayUniv fn + , Crypto (EraCrypto era) + , ShelleyEraScript era + , NativeScript era ~ MultiSig era + ) => + HasSpec fn (MultiSig era) + where + type TypeSpec fn (MultiSig era) = () + emptySpec = () + combineSpec _ _ = TrueSpec + genFromTypeSpec _ = pureGen $ genNestedMultiSig 2 + cardinalTypeSpec _ = TrueSpec + shrinkWithTypeSpec _ = shrink + conformsTo _ _ = True + toPreds _ _ = toPred True + +-- ======================================================================== +-- We need witnesses when the Tx has values of type 'hashtype' inside, because +-- the witnesses allows one to recover proof (ProofType hashtype era) that +-- the Tx author both knows, and controls, the thing that was Hashed, +-- i.e. (TypeHashed hashtype era). The witness (WitnessType hashtype era) +-- is NOT ALWAYS the same as the (ProofType hashtype era), since it can depend on +-- the Tx. All the strange class preconditions are required by conformance testing. + +-- deriving instance Typeable r => Generic (KeyHash r c) + +class + ( Eq (ProofType hashtype era) + , EncCBOR (ProofType hashtype era) + , ToExpr (ProofType hashtype era) + , NFData (ProofType hashtype era) + , NFData hashtype + , Eq hashtype + ) => + HasWitness hashtype era + where + type ProofType hashtype era + type WitnessType hashtype era + type TypeHashed hashtype era + hash :: TypeHashed hashtype era -> hashtype + mkWitness :: ProofType hashtype era -> WitnessType hashtype era + getTypeHashed :: ProofType hashtype era -> TypeHashed hashtype era + prettyHash :: hashtype -> PDoc + +-- ============================================================ + +-- | A WitBlock is desined to have five purposes +-- 1) To efficiently constrain objects to be witnessed when using constraint generators +-- the (Set hashtype) allows efficient constraints like :: (member_ t) (lit (wbHash witblock)) +-- 2) To efficiently compute witnesses from a 'hashtype' +-- the (Map hashtype (ProofType hashtype era)) can be used like this +-- case Map.lookup hash (wbMap witblock) of +-- Just base -> mkWitness base +-- Nothing -> error "Missing hash. perhaps generator did not constrain the hash to be witnessed?" +-- 3) When (HasWitness hashtype era) holds, the WitBlock can be computed from only [ProofType hashtype era] +-- using 'getTypeHashed'. This makes Gen and CBOR instances, especially easy. We compute only with +-- [ProofType hashtype era] and then reconstruct the rest +-- 4) WitBlock is a Monoid, so we can combine them easily +-- 5) We can easily to make (Gen (WitBlock t era)), so we can make them for testing. +data WitBlock t era where + WitBlock :: HasWitness t era => Set t -> Map t (ProofType t era) -> WitBlock t era + +wbHash :: WitBlock t era -> Set t +wbHash (WitBlock x _) = x +wbMap :: WitBlock t era -> Map t (ProofType t era) +wbMap (WitBlock _ y) = y + +-- | when we print a WitBlock, we are only interested in the hashes, not the witnesses +instance PrettyA (WitBlock t era) where + prettyA (WitBlock hashset _) = ppSet (prettyHash @t @era) hashset + +instance Show (WitBlock t era) where + show x = show (prettyA x) + +instance NFData (WitBlock t era) where + rnf (WitBlock x y) = deepseq (rnf x) (deepseq (rnf y) ()) + +instance Eq (WitBlock t era) where + (WitBlock x y) == (WitBlock a b) = x == a && y == b + +-- ========================================================================== +-- (HasWitness t era) Instances for several different types of hash and hashed types + +-- A short descriptive name for a long complicated thing +type BodyHash era = SafeHash (EraCrypto era) EraIndependentTxBody + +-- ======== +-- KeyHash and VKey +-- KeyPair seems to be missing a lot of instances, so we define them here + +instance (Typeable r, Crypto c) => EncCBOR (KeyPair r c) where + encCBOR (KeyPair x y) = encode $ Rec KeyPair !> To x !> To y + +deriving instance Typeable r => Eq (KeyPair r StandardCrypto) + +instance ToExpr (KeyPair r StandardCrypto) where + toExpr (KeyPair x y) = Tree.App "KeyPair" [toExpr x, Tree.App (take 10 (show y)) []] + +instance (Era era, EraCrypto era ~ c, c ~ StandardCrypto) => HasWitness (KeyHash 'Witness c) era where + type ProofType (KeyHash 'Witness c) era = KeyPair 'Witness c + type WitnessType (KeyHash 'Witness c) era = (BodyHash era -> WitVKey 'Witness c) + type TypeHashed (KeyHash 'Witness c) era = VKey 'Witness c + hash x = hashKey x + mkWitness keypair safehash = mkWitnessVKey safehash keypair + getTypeHashed (KeyPair x _) = x + prettyHash x = prettyA x + +-- ======== +-- ScriptHash and Scripts +-- NewScript needed because (Script era) is a type family, and hence can't have instances + +newtype NewScript era = NewScript {unNew :: Script era} +deriving newtype instance NFData (Script era) => NFData (NewScript era) +deriving newtype instance EraScript era => Eq (NewScript era) +deriving newtype instance EraScript era => EncCBOR (NewScript era) +instance (EraScript era, ToExpr (NativeScript era)) => ToExpr (NewScript era) where + toExpr (NewScript script) = case getNativeScript script of + Just s -> toExpr s + Nothing -> Tree.App "PlutusScript" [] + +instance + ( EraScript era + , NFData (Script era) + , EraCrypto era ~ c + , c ~ StandardCrypto + , ToExpr (NativeScript era) + ) => + HasWitness (ScriptHash c) era + where + type ProofType (ScriptHash c) era = NewScript era + type WitnessType (ScriptHash c) era = Script era + type TypeHashed (ScriptHash c) era = ProofType (ScriptHash c) era + hash (NewScript x) = hashScript x + mkWitness (NewScript script) = script + getTypeHashed x = x + prettyHash x = prettyA x + +-- ======== +-- BootstrapAddress and SigningKey +-- BootstrapAddress is a convoluted hash of the SigningKey, +-- understood only by the Byron programmers (don't ask) + +instance ToExpr SigningKey where toExpr sk = Tree.App (show sk) [] + +instance (Era era, EraCrypto era ~ c, c ~ StandardCrypto) => HasWitness (BootstrapAddress c) era where + type ProofType (BootstrapAddress c) era = SigningKey + type WitnessType (BootstrapAddress c) era = (BodyHash era -> BootstrapWitness (EraCrypto era)) + type TypeHashed (BootstrapAddress c) era = SigningKey + + -- \| Don't ask about this, its related to the magic genAddrPair, which, like + -- all things Byron, I don't understand. It generates a Byron address and + -- its signing key for test purposes, and the signing key, uniquely determines + -- the Byron address (for Testnet) as defined in method 'hash' below. I am certain, this + -- is not how Byron address work in real life, but it works for test purposes. + hash signkey = + let verificationKey = toVerification signkey + asd = Byron.VerKeyASD verificationKey + attrs = + Byron.AddrAttributes + (Just (Byron.HDAddressPayload "a compressed lenna.png")) + (Byron.NetworkTestnet 0) + in BootstrapAddress (Byron.makeAddress asd attrs) + mkWitness signkey bodyhash = + let bootAddr = hash @(BootstrapAddress c) @era signkey + in makeBootstrapWitness + (extractHash bodyhash) + signkey + (Byron.addrAttributes (unBootstrapAddress bootAddr)) + getTypeHashed signkey = signkey + prettyHash x = prettyA x + +-- ======== +-- DataHash and Data +-- note the type synonym +-- type (DataHash c) = SafeHash c EraIndependentData + +instance (EraScript era, EraCrypto era ~ c, c ~ StandardCrypto) => HasWitness (DataHash c) era where + type ProofType (DataHash c) era = Data era + type WitnessType (DataHash c) era = Data era + type TypeHashed (DataHash c) era = Data era + hash x = hashData x + mkWitness script = script + getTypeHashed x = x + prettyHash x = pcDataHash x + +-- ============================================== +-- The WitUniv type is 4 WitBlocks + +data WitUniv era + = WitUniv + { wvVKey :: WitBlock (KeyHash 'Witness (EraCrypto era)) era + , wvBoot :: WitBlock (BootstrapAddress (EraCrypto era)) era + , wvScript :: WitBlock (ScriptHash (EraCrypto era)) era + , wvDats :: WitBlock (DataHash (EraCrypto era)) era + } + deriving (Eq, NFData, Generic) + +-- Non deriveable instances for WitUniv + +instance Proof.Reflect era => PrettyA (WitUniv era) where + prettyA (WitUniv keys boot script dats) = + ppRecord + "WitnessUniverse" + [ ("keys", ppSet pcKeyHash (wbHash keys)) + , ("boot", ppSet pcByronAddress (wbHash boot)) + , ("scripts", ppSet pcScriptHash (wbHash script)) + , ("dats", ppSet ppSafeHash (wbHash dats)) + ] + +instance Proof.Reflect era => Show (WitUniv era) where show x = show (prettyA x) + +instance Era era => EncCBOR (WitUniv era) where + encCBOR (WitUniv w x y z) = encode $ Rec WitUniv !> To w !> To x !> To y !> To z + +-- ==================================================================== +-- Purpose 1) To efficiently constrain objects to be witnessed when using constraint generators +-- the (Set hashtype) allows efficient constraints like :: (member_ t) (lit (wbHash witblock)) + +explainWit :: HasSpec fn t => String -> WitUniv era -> Specification fn t -> Specification fn t +explainWit str (WitUniv (WitBlock s _) _ _ _) spec = + explainSpec + (pure ("While witnessing " ++ str ++ " with WitUniv of size " ++ show (Set.size s))) + spec + +witKeyHashSpec :: + forall fn era krole. + (Era era, IsConwayUniv fn, Typeable krole) => + WitUniv era -> Specification fn (KeyHash krole (EraCrypto era)) +witKeyHashSpec univ = + explainWit "(KeyHash r c)" univ $ + constrained $ + \ [var|keyhash|] -> + Assert (pure "witnessing (KeyHash r c)") $ member_ (coerce_ keyhash) (lit (wbHash (wvVKey univ))) + +witScriptHashSpec :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (ScriptHash (EraCrypto era)) +witScriptHashSpec univ = + explainWit "(ScriptHash c)" univ $ + constrained $ + \ [var|scripthash|] -> member_ scripthash (lit (wbHash (wvScript univ))) + +witBootstrapAddress :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (BootstrapAddress (EraCrypto era)) +witBootstrapAddress univ = + explainWit "(BootstrapAddress c)" univ $ + constrained $ + \ [var|bootAddr|] -> member_ bootAddr (lit (wbHash (wvBoot univ))) + +witCredSpec :: + forall fn era krole. + (IsConwayUniv fn, Era era, Typeable krole) => + WitUniv era -> Specification fn (Credential krole (EraCrypto era)) +witCredSpec univ = + explainWit "(Credential c)" univ $ + constrained $ \ [var|cred|] -> + [ (caseOn cred) + -- ScriptHash c -> Credential + (branchW 1 $ \ [var|scripthash|] -> satisfies scripthash (witScriptHashSpec univ)) + -- KeyHash kr c -> Credential + (branchW 1 $ \ [var|keyhash|] -> satisfies keyhash (witKeyHashSpec univ)) + ] + +witDRepSpec :: + forall fn era. + (IsConwayUniv fn, Era era) => + WitUniv era -> Specification fn (DRep (EraCrypto era)) +witDRepSpec univ = + explainWit "(DRep c)" univ $ + constrained $ \ [var|drep|] -> + [ (caseOn drep) + -- KeyHash kr c -> Drep + (branchW 3 $ \ [var|keyhash|] -> satisfies keyhash (witKeyHashSpec univ)) + -- ScriptHash c -> DRep + (branchW 3 $ \ [var|scripthash|] -> satisfies scripthash (witScriptHashSpec univ)) + -- DRepAlwaysObstain + (branchW 1 $ \_ -> assert True) + -- DRepAlwaysNoConfidence + (branchW 1 $ \_ -> assert True) + ] + +-- | Used only in Withdrawals, other RewardAccounts, not being withdrawn do not need witnessing +witRewardAccountSpec :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (RewardAccount (EraCrypto era)) +witRewardAccountSpec univ = + explainWit "(RewardAccount c)" univ $ + constrained $ \ [var|rewaccount|] -> + match rewaccount $ \ [var|network|] [var|raCred|] -> + [ assert $ network ==. lit (Testnet) + , satisfies raCred (witCredSpec @fn @era univ) + ] + +owners_ :: + (Crypto c, IsConwayUniv fn) => Term fn (PoolParams c) -> Term fn (Set (KeyHash 'Staking c)) +owners_ = sel @6 + +witPoolParamsSpec :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (PoolParams (EraCrypto era)) +witPoolParamsSpec univ = + explainWit "(PoolParams c)" univ $ + constrained $ \ [var|poolparams|] -> + [ forAll (owners_ poolparams) $ \ [var|ownerKeyHash|] -> satisfies ownerKeyHash (witKeyHashSpec univ) + , satisfies (owners_ poolparams) (hasSize (rangeSize 1 3)) + ] + +witGenDelegPairSpec :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (GenDelegPair (EraCrypto era)) +witGenDelegPairSpec univ = + explainWit "(GenDelegPair c)" univ $ + constrained $ \ [var|gdpair|] -> + match gdpair $ \ [var|keyhash|] [var|_hash|] -> satisfies keyhash (witKeyHashSpec univ) + +-- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials +witShelleyTxCert :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (ShelleyTxCert era) +witShelleyTxCert univ = + explainWit ("(ShelleyTxCert " ++ "typeRep (Proxy @era)" ++ ")") univ $ + constrained $ \ [var|txcert|] -> + (caseOn txcert) + ( branchW 5 $ \delegcert -> + (caseOn delegcert) + (branch $ \_register -> TruePred) + (branch $ \unregisterAuthor -> satisfies unregisterAuthor (witCredSpec univ)) + (branch $ \delegateAuthor _ -> satisfies delegateAuthor (witCredSpec univ)) + ) + ( branchW 3 $ \poolcert -> + (caseOn poolcert) + (branch $ \registerPoolParams -> satisfies registerPoolParams (witPoolParamsSpec univ)) + (branch $ \retirePoolAuthor _ -> satisfies retirePoolAuthor (witKeyHashSpec univ)) + ) + ( branchW 1 $ \genesiscert -> match genesiscert $ \authorkey _ _ -> satisfies authorkey (witKeyHashSpec univ) + ) + (branchW 1 $ \_mircert -> FalsePred (pure "NO MIR")) + +-- | Constrains all the Certificate Authors. Sometimes thay are keyHashes, and sometimes Credentials +witConwayTxCert :: + forall fn era. + (Era era, IsConwayUniv fn) => + WitUniv era -> Specification fn (ConwayTxCert era) +witConwayTxCert univ = + explainWit ("(ConwayTxCert " ++ "typeRep (Proxy @era)" ++ ")") univ $ + constrained $ \ [var|txcert|] -> + (caseOn txcert) + ( branch $ \delegcert -> + (caseOn delegcert) + ( branch $ \registerAuthor deposit -> + (caseOn deposit) + (branch $ \_ -> TruePred) + (branch $ \_ -> satisfies registerAuthor (witCredSpec univ)) + ) + (branch $ \unregisterAuthor _ -> satisfies unregisterAuthor (witCredSpec univ)) + (branch $ \delegateAuthor _ -> satisfies delegateAuthor (witCredSpec univ)) + (branch $ \registerdelegateAuthor _ _ -> satisfies registerdelegateAuthor (witCredSpec univ)) + ) + ( branch $ \poolcert -> + (caseOn poolcert) + (branch $ \registerPoolParams -> satisfies registerPoolParams (witPoolParamsSpec univ)) + (branch $ \retirePoolAuthor _ -> satisfies retirePoolAuthor (witKeyHashSpec univ)) + ) + ( branch $ \govcert -> + (caseOn govcert) + (branch $ \regdrepAuthor _ _ -> satisfies regdrepAuthor (witCredSpec univ)) + (branch $ \unregdrepAuthor _ -> satisfies unregdrepAuthor (witCredSpec univ)) + (branch $ \updatedrepAuthor _ -> satisfies updatedrepAuthor (witCredSpec univ)) + (branch $ \authorizeAuthor _ -> satisfies authorizeAuthor (witCredSpec univ)) + (branch $ \resignAuthor _ -> satisfies resignAuthor (witCredSpec univ)) + ) + +-- ===================================================================== +-- Purpose 2) To efficiently compute witnesses from a 'hashtype' +-- the (Map hashtype (ProofType hashtype era)) can be used like this +-- case Map.lookup hash (wbMap witblock) of +-- Just base -> mkWitness base +-- Nothing -> error "Missing hash. perhaps generator did not constrain the hash to be witnessed?" + +witnessBootAddr :: + forall era. + Proof.Reflect era => + BodyHash era -> BootstrapAddress (EraCrypto era) -> WitUniv era -> TxWits era +witnessBootAddr bodyhash bootaddr wu = case Map.lookup bootaddr (wbMap (wvBoot wu)) of + Just x -> + (mkBasicTxWits @era) + & bootAddrTxWitsL + .~ (Set.singleton (mkWitness @(BootstrapAddress (EraCrypto era)) @era x bodyhash)) + Nothing -> error ("missing BootstrapAddress in WitUnv " ++ show bootaddr) + +witnessKeyHash :: + forall era. + Reflect era => + BodyHash era -> KeyHash 'Witness (EraCrypto era) -> WitUniv era -> TxWits era +witnessKeyHash bodyhash keyhash wu = case Map.lookup keyhash (wbMap (wvVKey wu)) of + Just x -> + (mkBasicTxWits @era) + & addrTxWitsL + .~ (Set.singleton (mkWitness @(KeyHash 'Witness (EraCrypto era)) @era x bodyhash)) + Nothing -> error ("missing key hash in WitUnv " ++ show keyhash) + +witnessScriptHash :: + forall era. EraTxWits era => ScriptHash (EraCrypto era) -> WitUniv era -> TxWits era +witnessScriptHash scripthash wu = case Map.lookup scripthash (wbMap (wvScript wu)) of + Just (NewScript script) -> (mkBasicTxWits @era) & scriptTxWitsL .~ (Map.insert scripthash script Map.empty) + Nothing -> error ("missing script hash in WitUnv " ++ show scripthash) + +witnessDataHash :: + forall era. AlonzoEraTxWits era => DataHash (EraCrypto era) -> WitUniv era -> TxWits era +witnessDataHash datahash wu = case Map.lookup datahash (wbMap (wvDats wu)) of + Just d -> (mkBasicTxWits @era) & datsTxWitsL .~ TxDats (Map.insert datahash d Map.empty) + Nothing -> error ("missing data hash in WitUnv " ++ show datahash) + +-- ========================================================= +-- Purpose 3) When (HasWitness hashtype era) holds, the WitBlock can be computed from +-- only [ProofType hashtype era] using 'getTypeHashed'. This makes Gen and CBOR instances, +-- especially easy. We compute only with [ProofType hashtype era] and then reconstruct the rest + +-- | Reconstruct a (WitBlock t era) from only a [ProofType t era] +blockFromProofList :: forall t era. (Ord t, HasWitness t era) => [ProofType t era] -> WitBlock t era +blockFromProofList baselist = + WitBlock + (Set.fromList hashlist) + (Map.fromList (zip hashlist baselist)) + where + hashlist = map (hash @t @era . getTypeHashed @t @era) baselist + +-- =============================================================== +-- Purpose 4) WitBlock is a Monoid, so we can combine them easily + +instance Ord t => Semigroup (WitBlock t era) where + (WitBlock x y) <> (WitBlock a b) = WitBlock (x <> a) (y <> b) + +instance (Ord t, HasWitness t era) => Monoid (WitBlock t era) where + mempty = (WitBlock mempty mempty) + +-- | Easy to extend Monoid from WitBlock to WitUniv +instance Era era => Semigroup (WitUniv era) where + x <> y = + WitUniv + { wvVKey = wvVKey x <> wvVKey y + , wvBoot = wvBoot x <> wvBoot y + , wvScript = wvScript x <> wvScript y + , wvDats = wvDats x <> wvDats y + } + +instance + ( EraScript era + , NFData (Script era) + , ToExpr (NativeScript era) + , Reflect era + ) => + Monoid (WitUniv era) + where + mempty = WitUniv {wvVKey = mempty, wvBoot = mempty, wvScript = mempty, wvDats = mempty} + +-- ======================================================================= +-- Purpose 5) We can easily to make (Gen (WitBlock t era)), so we can make them for testing. +-- this is facilitated by the methods of the (HasWitness t era) instances +-- and the special property that WitBlock can be computed from [ProofList] + +genWitBlock :: + forall t era. (Ord t, HasWitness t era) => Int -> Gen (ProofType t era) -> Gen (WitBlock t era) +genWitBlock n g = blockFromProofList <$> vectorOf n g + +instance (Era era, Typeable t) => EncCBOR (WitBlock t era) where + encCBOR (WitBlock _ m) = encCBOR (Map.elems m) + +instance + (Ord t, Era era, HasWitness t era, DecCBOR (ProofType t era), Typeable t) => + DecCBOR (WitBlock t era) + where + decCBOR = blockFromProofList <$> decCBOR + +genWitUniv :: + forall era. + ( GenScript era + , EraCrypto era ~ StandardCrypto + ) => + Int -> Gen (WitUniv era) +genWitUniv n = + WitUniv + <$> genWitBlock n (arbitrary @(KeyPair 'Witness (EraCrypto era))) + <*> genWitBlock n (snd <$> genAddrPair Testnet) + <*> genWitBlock n (NewScript <$> genScript @era) + <*> genWitBlock n (arbitrary @(Data era)) + +-- Use this for small tests only (otherwise increase from 10 to something larger) +-- or use (genWitUniv n) instead of arbitrary for some bigger 'n' +instance + (ToExpr (NativeScript era), NFData (Script era), GenScript era, EraCrypto era ~ StandardCrypto) => + Arbitrary (WitUniv era) + where + arbitrary = genWitUniv 10 + +-- ================================================================================== +-- Generating random native-scripts in every era. Needed to generate a random WitUniv) + +genNestedMultiSig :: forall era. ShelleyEraScript era => Int -> Gen (NativeScript era) +genNestedMultiSig depth + | depth > 0 = + oneof $ + nonRecTimelocks ++ [requireAllOf depth, requireAnyOf depth, requireMOf depth] + | otherwise = oneof nonRecTimelocks + where + nonRecTimelocks = [requireSignature] + requireSignature = RequireSignature @era <$> genKeyHash + requireAllOf k = do + n <- choose (0, 4) + RequireAllOf . Seq.fromList <$> replicateM n (genNestedMultiSig @era (k - 1)) + requireAnyOf k = do + n <- choose (1, 4) + RequireAnyOf . Seq.fromList <$> replicateM n (genNestedMultiSig @era (k - 1)) + requireMOf k = do + n <- choose (0, 4) + m <- choose (0, n) + RequireMOf m . Seq.fromList <$> replicateM n (genNestedMultiSig @era (k - 1)) + genKeyHash :: Gen (KeyHash 'Witness (EraCrypto era)) + genKeyHash = arbitrary + +genNestedTimelock :: forall era. AllegraEraScript era => Int -> Gen (NativeScript era) +genNestedTimelock depth + | depth > 0 = + oneof $ + nonRecTimelocks ++ [requireAllOf depth, requireAnyOf depth, requireMOf depth] + | otherwise = oneof nonRecTimelocks + where + nonRecTimelocks = + [ requireSignature + , requireTimeStart (SlotNo minBound) + , requireTimeExpire (SlotNo maxBound) + ] + requireSignature = RequireSignature <$> genKeyHash + requireAllOf k = do + n <- choose (2, 3) -- lift nonNegativeSingleDigitInt + RequireAllOf . Seq.fromList <$> replicateM n (genNestedTimelock @era (k - 1)) + requireAnyOf k = do + n <- choose (2, 3) -- lift positiveSingleDigitInt + RequireAnyOf . Seq.fromList <$> replicateM n (genNestedTimelock @era (k - 1)) + requireMOf k = do + n <- choose (2, 3) -- lift nonNegativeSingleDigitInt + m <- choose (0, n) + RequireMOf m . Seq.fromList <$> replicateM n (genNestedTimelock @era (k - 1)) + requireTimeStart (SlotNo validFrom) = do + minSlotNo <- choose (minBound, validFrom) + pure $ RequireTimeStart (SlotNo minSlotNo) + requireTimeExpire (SlotNo validTill) = do + maxSlotNo <- choose (validTill, maxBound) + pure $ RequireTimeExpire (SlotNo maxSlotNo) + genKeyHash :: Gen (KeyHash 'Witness (EraCrypto era)) + genKeyHash = arbitrary + +-- ======================================================================= +-- Tools for Parametric Witnessing +-- ============================================================== + +-- | The class of things we know how to witness. This way you don't +-- have to remember long complicated names. +class Witnessed fn era t where + witness :: WitUniv era -> Term fn t -> Pred fn + +instance (IsConwayUniv fn, Era era, Typeable r, EraCrypto era ~ c) => Witnessed fn era (KeyHash r c) where + witness univ t = satisfies t (witKeyHashSpec univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (ScriptHash c) where + witness univ t = satisfies2 (pure "BAD-SCRIPT-HASH") t (witScriptHashSpec univ) + +instance (IsConwayUniv fn, Era era, Typeable r, EraCrypto era ~ c) => Witnessed fn era (Credential r c) where + witness univ t = satisfies t (witCredSpec univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (BootstrapAddress c) where + witness univ t = satisfies t (witBootstrapAddress univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (DRep c) where + witness univ t = satisfies t (witDRepSpec univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (RewardAccount c) where + witness univ t = satisfies t (witRewardAccountSpec univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (PoolParams c) where + witness univ t = satisfies t (witPoolParamsSpec univ) + +instance (IsConwayUniv fn, Era era, EraCrypto era ~ c) => Witnessed fn era (GenDelegPair c) where + witness univ t = satisfies t (witGenDelegPairSpec univ) + +instance (IsConwayUniv fn, Era era) => Witnessed fn era (ShelleyTxCert era) where + witness univ t = satisfies t (witShelleyTxCert univ) + +instance (IsConwayUniv fn, Era era) => Witnessed fn era (ConwayTxCert era) where + witness univ t = satisfies t (witConwayTxCert univ) + +instance (Era era, HasSpec fn t, Ord t, Witnessed fn era t) => Witnessed fn era (Set t) where + witness univ t = + forAll + t + ( \x -> + assertExplain (pure ("While witnessing " ++ show (typeRep (Proxy @(Set t))))) $ + witness univ x + ) + +instance (Era era, HasSpec fn t, HasSpec fn v, Ord t, Witnessed fn era t) => Witnessed fn era (Map t v) where + witness univ t = + assertExplain (pure ("While witnessing " ++ show (typeRep (Proxy @(Map t v))))) $ + forAll (dom_ t) (witness univ) + +instance (Era era, HasSpec fn t, Witnessed fn era t) => Witnessed fn era [t] where + witness univ t = + assertExplain (pure ("While witnessing " ++ show (typeRep (Proxy @([t]))))) $ + forAll t (witness univ) + +-- =================================================================== + +-- | Parametric TxCert +class (EraTxCert era, HasSpec fn (TxCert era)) => EraSpecTxCert fn era where + witTxCert :: WitUniv era -> Specification fn (TxCert era) + +instance IsConwayUniv fn => EraSpecTxCert fn Shelley where + witTxCert = witShelleyTxCert +instance IsConwayUniv fn => EraSpecTxCert fn Allegra where + witTxCert = witShelleyTxCert +instance IsConwayUniv fn => EraSpecTxCert fn Mary where + witTxCert = witShelleyTxCert +instance IsConwayUniv fn => EraSpecTxCert fn Alonzo where + witTxCert = witShelleyTxCert +instance IsConwayUniv fn => EraSpecTxCert fn Babbage where + witTxCert = witShelleyTxCert +instance IsConwayUniv fn => EraSpecTxCert fn Conway where + witTxCert = witConwayTxCert + +-- | Parametric Script +class (EraScript era, ToExpr (NativeScript era), NFData (Script era)) => GenScript era where + genScript :: Gen (Script era) + +instance GenScript Shelley where genScript = genNestedMultiSig 2 +instance GenScript Allegra where genScript = genNestedTimelock @Allegra 2 +instance GenScript Mary where genScript = genNestedTimelock @Mary 2 +instance GenScript Alonzo where genScript = fromNativeScript <$> genNestedTimelock @Alonzo 2 +instance GenScript Babbage where genScript = fromNativeScript <$> genNestedTimelock @Babbage 2 +instance GenScript Conway where genScript = fromNativeScript <$> genNestedTimelock @Conway 2 + +-- | Parametric WitUniv +-- Note that these are constant (but different) everytime the system starts +-- Mostly used in simple tests, and when debugging specs that fail +class EraUniverse era where + eraUniv :: WitUniv era + +instance EraUniverse Shelley where + eraUniv = unsafePerformIO (generate $ genWitUniv @Shelley 25) +instance EraUniverse Allegra where + eraUniv = unsafePerformIO (generate $ genWitUniv @Allegra 25) +instance EraUniverse Mary where + eraUniv = unsafePerformIO (generate $ genWitUniv @Mary 25) +instance EraUniverse Alonzo where + eraUniv = unsafePerformIO (generate $ genWitUniv @Alonzo 25) +instance EraUniverse Babbage where + eraUniv = unsafePerformIO (generate $ genWitUniv @Babbage 25) +instance EraUniverse Conway where + eraUniv = unsafePerformIO (generate $ genWitUniv @Conway 25) + +-- =============================================================== +-- examples +spec1 :: WitUniv Shelley -> Specification ConwayFn (Set (ScriptHash StandardCrypto)) +spec1 univ = + constrained $ \ [var|setHash|] -> [assert $ sizeOf_ setHash ==. 11, witness univ setHash] + +go1 :: IO () +go1 = do + univ <- generate $ genWitUniv @Shelley 5 + {- + -- print (witScriptHashSpec @ConwayFn univ) + print (spec1 univ) + case (spec1 univ) of + SuspendedSpec {} -> putStrLn "YES" + _ -> putStrLn "NO" + + putStrLn "\n\n(simplifySpec (spec1 univ))" + print (simplifySpec (spec1 univ)) + + putStrLn "\n\n(explainSpec (pure VVV) (simplifySpec(spec1 univ)))" + print (explainSpec (pure "VVV") (simplifySpec(spec1 univ))) -} + ans <- generate $ genFromSpec (spec1 univ) + putStrLn (show (prettyA ans)) + +spec2 :: + WitUniv Shelley -> + Set (ScriptHash StandardCrypto) -> + Specification ConwayFn (Set (ScriptHash StandardCrypto)) +spec2 univ big = + constrained $ \ [var|setHash|] -> + [ assert $ subset_ (lit big) setHash + , witness univ setHash + ] +go2 :: IO () +go2 = do + univ <- generate $ genWitUniv @Shelley 5 + big <- generate arbitrary + ans <- generate $ genFromSpec (spec2 univ big) + putStrLn (show (prettyA ans)) + +-- ================================================================= +explainSpec2 :: HasSpec fn a => NE.NonEmpty String -> Specification fn a -> Specification fn a +explainSpec2 es spec = case simplifySpec spec of + ErrorSpec es' -> ErrorSpec (es <> es') + TypeSpec tyspec cs1 -> case guardTypeSpec (NE.toList es) tyspec of + TypeSpec tyspec2 [] -> TypeSpec tyspec2 cs1 + other -> other + SuspendedSpec v p -> SuspendedSpec v (assertExplain es p) + MemberSpec xs -> constrained $ \x -> [assertExplain es $ satisfies x (MemberSpec xs)] + s -> s + +satisfies2 :: + forall fn a. HasSpec fn a => NE.NonEmpty String -> Term fn a -> Specification fn a -> Pred fn +satisfies2 _ _ TrueSpec = TruePred +satisfies2 nes e (MemberSpec nonempty) = assertExplain nes $ elem_ e (lit (NE.toList nonempty)) +satisfies2 nes t (SuspendedSpec x p) = assertExplain nes $ Subst x t p +satisfies2 nes e (TypeSpec s cant) + | null cant = toPreds e s + | otherwise = + Assert (pure (show e ++ " `notElem` " ++ show cant) <> nes) (not_ (elem_ e $ lit cant)) + <> toPreds e s +satisfies2 nes _ (ErrorSpec e) = FalsePred (nes <> e) diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 50373c9705f..c2fec1de39b 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -270,10 +270,10 @@ instance HasSpec fn a => Eq (Term fn a) where type HasSpecImpliesEq fn a f = HasSpec fn a => Eq (f a) :: Constraint deriving instance HasSpecImpliesEq fn a f => Eq (WithHasSpec fn f a) -instance (Ord a, HasSpec fn (Set a)) => Semigroup (Term fn (Set a)) where - (<>) = app unionFn +instance (Ord a, Show a, Typeable a, HasSpec fn (Set a)) => Semigroup (Term fn (Set a)) where + (<>) = app (unionFn @fn @a) -instance (Ord a, HasSpec fn (Set a)) => Monoid (Term fn (Set a)) where +instance (Ord a, Show a, Typeable a, HasSpec fn (Set a)) => Monoid (Term fn (Set a)) where mempty = Lit mempty data Binder fn a where @@ -911,6 +911,10 @@ class typeSpecOpt :: TypeSpec fn a -> [a] -> Specification fn a typeSpecOpt tySpec bad = TypeSpec tySpec bad + -- | This can be used to detect self inconsistencies in a (TypeSpec fn t) + guardTypeSpec :: [String] -> TypeSpec fn a -> Specification fn a + guardTypeSpec _ ty = typeSpec ty + -- | Prerequisites for the instance that are sometimes necessary -- when working with e.g. `Specification`s or functions in the universe. type Prerequisites fn a :: Constraint @@ -1389,6 +1393,66 @@ pattern SRight :: forall fn a. () => forall b c. (HasSpec fn c, a ~ Sum b c) => Term fn c -> Term fn a pattern SRight a <- App (extractFn @(SumFn fn) -> Just InjRight) (a :> Nil) +-- ============================== +-- Term patterns on function symbols on Sets, Lists + +pattern SubsetPat :: + forall fn a. + () => + forall b. + (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) => + Term fn (Set b) -> Term fn (Set b) -> Term fn a +pattern SubsetPat a b <- App (extractFn @(SetFn fn) -> Just Subset) (a :> b :> Nil) + where + SubsetPat x y = subset_ x y + +pattern DisjointPat :: + forall fn a. + () => + forall b. + (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) => + Term fn (Set b) -> Term fn (Set b) -> Term fn a +pattern DisjointPat a b <- App (extractFn @(SetFn fn) -> Just Disjoint) (a :> b :> Nil) + +pattern UnionPat :: + forall fn a. + () => + forall b. + (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Set b) => + Term fn (Set b) -> Term fn (Set b) -> Term fn a +pattern UnionPat a b <- App (extractFn @(SetFn fn) -> Just Union) (a :> b :> Nil) + +pattern MemberPat :: + forall fn a. + () => + forall b. + (HasSpec fn b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) => + Term fn b -> Term fn (Set b) -> Term fn a +pattern MemberPat a b <- App (extractFn @(SetFn fn) -> Just Member) (a :> b :> Nil) + +pattern ElemPat :: + forall fn a. + () => + forall b. + (HasSpec fn b, HasSpec fn [b], Show b, Typeable b, a ~ Bool) => + Term fn b -> Term fn [b] -> Term fn a +pattern ElemPat a b <- App (extractFn @(SetFn fn) -> Just Elem) (a :> b :> Nil) + +pattern AppendPat :: + forall fn a. + () => + forall b. + (HasSpec fn [b], Show b, Typeable b, a ~ [b]) => Term fn [b] -> Term fn [b] -> Term fn a +pattern AppendPat a b <- App (extractFn @(ListFn fn) -> Just AppendFn) (a :> b :> Nil) + +short :: forall a x. (Show a, Typeable a) => [a] -> Doc x +short [] = "[]" +short [x] = + let raw = show x + refined = if length raw <= 20 then raw else take 20 raw ++ " ... " + in "[" <+> fromString refined <+> "]" +short xs = "([" <+> viaShow (length xs) <+> "elements ...] @" <> viaShow (typeRep (Proxy @a)) <> ")" + prettyPlan :: HasSpec fn a => Specification fn a -> Doc ann prettyPlan (simplifySpec -> spec) | SuspendedSpec _ p <- spec @@ -1536,15 +1600,21 @@ normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec' -- Computing specs ------------------------------------------------------------------------ -fromGESpec :: HasCallStack => GE (Specification fn a) -> Specification fn a +fromGESpec :: (HasCallStack, HasSpec fn a) => GE (Specification fn a) -> Specification fn a fromGESpec ge = case ge of Result [] s -> s Result es s -> explainSpec (foldr1 (<>) es) s _ -> fromGE ErrorSpec ge -explainSpec :: NE.NonEmpty String -> Specification fn a -> Specification fn a -explainSpec es (ErrorSpec es') = ErrorSpec (es <> es') -explainSpec _ s = s +explainSpec :: HasSpec fn a => NE.NonEmpty String -> Specification fn a -> Specification fn a +explainSpec es spec = case spec of + ErrorSpec es' -> ErrorSpec (es <> es') + TypeSpec tyspec cs1 -> case guardTypeSpec (NE.toList es) tyspec of + TypeSpec tyspec2 [] -> TypeSpec tyspec2 cs1 + -- ErrorSpec es' -> ErrorSpec (es <> es') + other -> other + SuspendedSpec v p -> SuspendedSpec v (assertExplain es p) + s -> s regularize :: HasVariables fn t => Var a -> t -> Var a regularize v t = @@ -1586,19 +1656,29 @@ simplifySpec :: HasSpec fn a => Specification fn a -> Specification fn a simplifySpec spec = case regularizeNames spec of SuspendedSpec x p -> let optP = optimisePred p - in fromGESpec - $ explain - ( NE.fromList - [ show $ "Simplifying: " /> pretty spec - , show $ "optimisePred =>" /> pretty optP - ] - ) - $ computeSpecSimplified x optP + in fromGESpec $ + explain + (pure ("\nWhile calling simplifySpec on var " ++ show x)) + (computeSpecSimplified x optP) MemberSpec xs -> MemberSpec xs ErrorSpec es -> ErrorSpec es TypeSpec ts cant -> TypeSpec ts cant TrueSpec -> TrueSpec +combineBlock :: HasSpec fn a => Var a -> [Pred fn] -> GE (Specification fn a) +combineBlock v ps = do + pair <- foldM accum ([], TrueSpec) ps + case pair of + (es@(_ : _), ErrorSpec xs) -> pure $ ErrorSpec (NE.fromList es <> xs) + (es@(_ : _), spec) -> pure $ explainSpec (NE.fromList es) spec + (_, spec) -> pure spec + where + accum (es, spec) p@(Assert es1 _) = + do + spec2 <- computeSpecSimplified v p + pure (es ++ NE.toList es1, spec2 <> spec) + accum (es, spec) p = (\x -> (es, x <> spec)) <$> computeSpecSimplified v p + -- | Precondition: the `Pred fn` defines the `Var a` -- -- Runs in `GE` in order for us to have detailed context on failure. @@ -1612,14 +1692,15 @@ computeSpecSimplified x p = localGESpec $ case p of FalsePred es -> genError es Block ps -> do spec <- fold <$> mapM (computeSpecSimplified x) ps + -- combineBlock x ps case spec of SuspendedSpec y ps' -> pure $ SuspendedSpec y $ simplifyPred ps' s -> pure s Let t b -> pure $ SuspendedSpec x (Let t b) Exists k b -> pure $ SuspendedSpec x (Exists k b) Assert _ (Lit True) -> pure mempty - Assert _ (Lit False) -> genError1 (show p) - Assert _ t -> explain1 (show p) $ propagateSpec (equalSpec True) <$> toCtx x t + Assert nes (Lit False) -> genError (nes <> pure (show p)) + Assert nes t -> explain (nes <> pure (show p)) $ propagateSpec (equalSpec True) <$> toCtx x t ForAll (Lit s) b -> fold <$> mapM (\val -> computeSpec x $ unBind val b) (forAllToList s) ForAll t b -> do bSpec <- computeSpecBinderSimplified b @@ -1647,8 +1728,8 @@ computeSpecSimplified x p = localGESpec $ case p of -- we probably don't want to propagate the full "currently simplifying xyz" explanation. case s of SuspendedSpec x p -> pure $ SuspendedSpec x (explanation es p) - _ -> pure $ explainSpec es s - -- Impossible cases that should be ruled out by the dependency analysis and linearizer + _ -> pure $ explainSpec es s -- HERE + -- Impossible cases that should be ruled out by the dependency analysis and linearizer DependsOn {} -> fatalError $ NE.fromList @@ -2899,7 +2980,7 @@ preMapFoldSpec :: HasSpec fn a => fn '[a] b -> FoldSpec fn b -> FoldSpec fn a preMapFoldSpec _ NoFold = NoFold preMapFoldSpec f (FoldSpec g s) = FoldSpec (composeFn g f) s -combineFoldSpec :: MonadGenError m => FoldSpec fn a -> FoldSpec fn a -> m (FoldSpec fn a) +combineFoldSpec :: FoldSpec fn a -> FoldSpec fn a -> Either [String] (FoldSpec fn a) combineFoldSpec NoFold s = pure s combineFoldSpec s NoFold = pure s combineFoldSpec (FoldSpec (f :: fn as b) s) (FoldSpec (f' :: fn' as' b') s') @@ -2908,8 +2989,7 @@ combineFoldSpec (FoldSpec (f :: fn as b) s) (FoldSpec (f' :: fn' as' b') s') , f == f' = pure $ FoldSpec f (s <> s') | otherwise = - genError - (NE.fromList ["Can't combine fold specs on different functions", " " ++ show f, " " ++ show f']) + Left ["Can't combine fold specs on different functions", " " ++ show f, " " ++ show f'] conformsToFoldSpec :: forall fn a. [a] -> FoldSpec fn a -> Bool conformsToFoldSpec _ NoFold = True @@ -3413,16 +3493,15 @@ instance (BaseUniverse fn, HasSpec fn ()) => HasSpec fn Bool where guardSumSpec :: forall fn a b. (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) => + [String] -> SumSpec fn a b -> Specification fn (Sum a b) -guardSumSpec s@(SumSpecRaw tString _ sa sb) +guardSumSpec msgs s@(SumSpecRaw tString _ sa sb) | isErrorLike sa , isErrorLike sb = ErrorSpec $ - NE.fromList - [ "When combining SumSpec, all branches in a caseOn" ++ sumType tString ++ " simplify to False." - , show s - ] + NE.fromList $ + msgs ++ ["All branches in a caseOn" ++ sumType tString ++ " simplify to False.", show s] | otherwise = typeSpec s data SumSpec fn a b @@ -3486,7 +3565,7 @@ instance (HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) => HasSpec fn (Su emptySpec = mempty - combineSpec s s' = guardSumSpec (s <> s') + combineSpec s s' = guardSumSpec ["When combining SumSpecs", " " ++ show s, " " ++ show s'] (s <> s') conformsTo (SumLeft a) (SumSpec _ sa _) = conformsToSpec a sa conformsTo (SumRight b) (SumSpec _ _ sb) = conformsToSpec b sb @@ -3578,13 +3657,25 @@ instance (Ord a, HasSpec fn a) => Semigroup (SetSpec fn a) where instance (Ord a, HasSpec fn a) => Monoid (SetSpec fn a) where mempty = SetSpec mempty mempty TrueSpec -guardSetSpec :: (HasSpec fn a, Ord a) => SetSpec fn a -> Specification fn (Set a) -guardSetSpec (SetSpec must elem ((<> geqSpec 0) -> size)) +guardSetSpec :: (HasSpec fn a, Ord a) => [String] -> SetSpec fn a -> Specification fn (Set a) +guardSetSpec es (SetSpec must elem ((<> geqSpec 0) -> size)) | Just u <- knownUpperBound size , u < 0 = - ErrorSpec (pure ("guardSetSpec: negative size " ++ show u)) - | isErrorLike size = ErrorSpec (pure "guardSetSpec: error in size") - | otherwise = typeSpec $ SetSpec must elem size + ErrorSpec (("guardSetSpec: negative size " ++ show u) :| es) + | not (all (`conformsToSpec` elem) must) = + ErrorSpec (("Some 'must' items do not conform to 'element' spec: " ++ show elem) :| es) + | isErrorLike size = ErrorSpec ("guardSetSpec: error in size" :| es) + | isErrorLike (geqSpec (sizeOf must) <> size) = + ErrorSpec $ + ("Must set size " ++ show (sizeOf must) ++ ", is inconsistent with SetSpec size" ++ show size) :| es + | isErrorLike (maxSpec (cardinality elem) <> size) = + ErrorSpec $ + NE.fromList $ + [ "Cardinality of SetSpec elemSpec (" ++ show (elem) ++ ") = " ++ show (maxSpec (cardinality elem)) + , " This is inconsistent with SetSpec size (" ++ show size ++ ")" + ] + ++ es + | otherwise = typeSpec (SetSpec must elem size) instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where type TypeSpec fn (Set a) = SetSpec fn a @@ -3593,8 +3684,7 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where emptySpec = mempty - -- TODO: we need to check conformsTo for musts and elem specs - combineSpec s s' = guardSetSpec $ s <> s' + combineSpec s s' = guardSetSpec ["While combining 2 SetSpecs", " " ++ show s, " " ++ show s'] (s <> s') conformsTo s (SetSpec must es size) = and @@ -3664,13 +3754,22 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where ++ [ forAll s (\e -> satisfies e es) , satisfies (size_ s) size ] + guardTypeSpec = guardSetSpec instance Ord a => Forallable (Set a) a where fromForAllSpec (e :: Specification fn a) | Evidence <- prerequisites @fn @(Set a) = typeSpec $ SetSpec mempty e TrueSpec forAllToList = Set.toList -deriving instance HasSpec fn a => Show (SetSpec fn a) +prettySetSpec :: HasSpec fn a => SetSpec fn a -> Doc ann +prettySetSpec (SetSpec must elem size) = + parens + ( "SetSpec" + /> sep ["must=" <> short (Set.toList must), "elem=" <> pretty elem, "size=" <> pretty size] + ) + +instance HasSpec fn a => Show (SetSpec fn a) where + show x = show (prettySetSpec x) instance BaseUniverse fn => Functions (SetFn fn) fn where propagateSpecFun _ _ TrueSpec = TrueSpec @@ -3932,26 +4031,32 @@ instance instance HasSpec fn a => Pretty (ListSpec fn a) where pretty = prettyPrec 0 +guardListSpec :: HasSpec fn a => [String] -> ListSpec fn a -> Specification fn [a] +guardListSpec msg l@(ListSpec _hint must size elemS _fold) + | ErrorSpec es <- size = ErrorSpec $ (NE.fromList ("Error in size of ListSpec" : msg)) <> es + | Just u <- knownUpperBound size + , u < 0 = + ErrorSpec $ NE.fromList (["Negative size in guardListSpec", show size] ++ msg) + | not (all (`conformsToSpec` elemS) must) = + ErrorSpec $ + ( NE.fromList + (["Some items in the must list do not conform to 'element' spec.", " " ++ show elemS] ++ msg) + ) + | otherwise = typeSpec l + instance HasSpec fn a => HasSpec fn [a] where type TypeSpec fn [a] = ListSpec fn a type Prerequisites fn [a] = HasSpec fn a emptySpec = ListSpec Nothing [] mempty mempty NoFold - combineSpec (ListSpec msz must size elemS foldS) (ListSpec msz' must' size' elemS' foldS') = fromGESpec $ do + combineSpec l1@(ListSpec msz must size elemS foldS) l2@(ListSpec msz' must' size' elemS' foldS') = let must'' = nub $ must <> must' elemS'' = elemS <> elemS' - size'' = geqSpec 0 <> size <> size' - badSizeSpec - | isErrorLike size'' = True - | Just u <- knownUpperBound size'' - , u < 0 = - True - | otherwise = False - unless (all (`conformsToSpec` elemS'') must'') $ - genError1 "combineSpec ListSpec failed with " - when badSizeSpec $ - genError1 "error-like size spec in combineSpec ListSpec" - typeSpec . ListSpec (unionWithMaybe min msz msz') must'' size'' elemS'' - <$> combineFoldSpec foldS foldS' + size'' = size <> size' + foldeither = combineFoldSpec foldS foldS' + msg = ["Error in combineSpec for ListSpec", " " ++ show l1, " " ++ show l2] + in case foldeither of + Left foldmsg -> ErrorSpec (NE.fromList (msg ++ foldmsg)) + Right fold'' -> guardListSpec msg $ ListSpec (unionWithMaybe min msz msz') must'' size'' elemS'' fold'' genFromTypeSpec (ListSpec _ must _ elemS _) | any (not . (`conformsToSpec` elemS)) must = @@ -3980,6 +4085,8 @@ instance HasSpec fn a => HasSpec fn [a] where cardinalTypeSpec _ = TrueSpec + guardTypeSpec = guardListSpec + conformsTo xs (ListSpec _ must size elemS foldS) = sizeOf xs `conformsToSpec` size && all (`elem` xs) must @@ -4097,17 +4204,20 @@ instance Random (Ratio Integer) where emptyNumSpec :: Ord a => NumSpec fn a emptyNumSpec = mempty +guardNumSpec :: + (Ord n, HasSpec fn n, TypeSpec fn n ~ NumSpec fn n) => + [String] -> NumSpec fn n -> Specification fn n +guardNumSpec msg s@(NumSpecInterval (Just a) (Just b)) + | a > b = ErrorSpec ("NumSpec has low bound greater than hi bound" :| ((" " ++ show s) : msg)) + | a == b = equalSpec a +guardNumSpec _ s = typeSpec s + combineNumSpec :: (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec fn n) => NumSpec fn n -> NumSpec fn n -> Specification fn n -combineNumSpec s s' = case s <> s' of - s''@(NumSpecInterval (Just a) (Just b)) - | a > b -> - ErrorSpec (pure ("combineNumSpec has low bound greater than hi bound: " ++ show s'')) - | a == b -> equalSpec a - s'' -> typeSpec s'' +combineNumSpec s s' = guardNumSpec ["when combining two NumSpecs", " " ++ show s, " " ++ show s'] (s <> s') genFromNumSpec :: (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) => @@ -4171,6 +4281,7 @@ instance BaseUniverse fn => HasSpec fn Int where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Integer where type TypeSpec fn Integer = NumSpec fn Integer @@ -4181,6 +4292,7 @@ instance BaseUniverse fn => HasSpec fn Integer where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn (Ratio Integer) where type TypeSpec fn (Ratio Integer) = NumSpec fn (Ratio Integer) @@ -4191,6 +4303,7 @@ instance BaseUniverse fn => HasSpec fn (Ratio Integer) where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec _ = TrueSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Natural where type TypeSpec fn Natural = NumSpec fn Natural @@ -4207,6 +4320,7 @@ instance BaseUniverse fn => HasSpec fn Natural where cardinalTypeSpec (NumSpecInterval Nothing (Just hi)) = MemberSpec (pure (fromIntegral @Natural @Integer hi + 1)) cardinalTypeSpec _ = TrueSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Word8 where type TypeSpec fn Word8 = NumSpec fn Word8 @@ -4218,6 +4332,7 @@ instance BaseUniverse fn => HasSpec fn Word8 where toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec typeSpecOpt = notInNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Word16 where type TypeSpec fn Word16 = NumSpec fn Word16 @@ -4228,6 +4343,7 @@ instance BaseUniverse fn => HasSpec fn Word16 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Word32 where type TypeSpec fn Word32 = NumSpec fn Word32 @@ -4238,6 +4354,7 @@ instance BaseUniverse fn => HasSpec fn Word32 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Word64 where type TypeSpec fn Word64 = NumSpec fn Word64 @@ -4248,6 +4365,7 @@ instance BaseUniverse fn => HasSpec fn Word64 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Int8 where type TypeSpec fn Int8 = NumSpec fn Int8 @@ -4258,6 +4376,7 @@ instance BaseUniverse fn => HasSpec fn Int8 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Int16 where type TypeSpec fn Int16 = NumSpec fn Int16 @@ -4268,6 +4387,7 @@ instance BaseUniverse fn => HasSpec fn Int16 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Int32 where type TypeSpec fn Int32 = NumSpec fn Int32 @@ -4278,6 +4398,7 @@ instance BaseUniverse fn => HasSpec fn Int32 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Int64 where type TypeSpec fn Int64 = NumSpec fn Int64 @@ -4288,6 +4409,7 @@ instance BaseUniverse fn => HasSpec fn Int64 where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec = cardinalNumSpec + guardTypeSpec = guardNumSpec instance BaseUniverse fn => HasSpec fn Float where type TypeSpec fn Float = NumSpec fn Float @@ -4298,6 +4420,7 @@ instance BaseUniverse fn => HasSpec fn Float where conformsTo = conformsToNumSpec toPreds = toPredsNumSpec cardinalTypeSpec _ = TrueSpec + guardTypeSpec = guardNumSpec ----------------------------------------------------------------------------------- -- The Base Function universe defines operations on TypeSpec defined in the Base. @@ -4543,7 +4666,7 @@ data ListFn fn args res where fn '[a] b -> ListFn fn '[[a]] b SingletonList :: ListFn fn '[a] [a] - AppendFn :: ListFn fn '[[a], [a]] [a] + AppendFn :: (Typeable a, Show a) => ListFn fn '[[a], [a]] [a] deriving instance Show (ListFn fn args res) @@ -4678,8 +4801,8 @@ foldMapFn f = injectFn $ FoldMap @fn f singletonListFn :: forall fn a. HasSpec fn a => fn '[a] [a] singletonListFn = injectFn $ SingletonList @fn -appendFn :: forall fn a. HasSpec fn a => fn '[[a], [a]] [a] -appendFn = injectFn $ AppendFn @fn +appendFn :: forall fn a. (HasSpec fn a, Show a, Typeable a) => fn '[[a], [a]] [a] +appendFn = injectFn $ AppendFn @a @fn -- Number functions ------------------------------------------------------- @@ -4870,9 +4993,7 @@ member_ :: member_ = app memberFn subset_ :: - ( HasSpec fn a - , Ord a - ) => + (HasSpec fn (Set a), Ord a, Show a, Typeable a) => Term fn (Set a) -> Term fn (Set a) -> Term fn Bool @@ -5261,7 +5382,7 @@ instance PredLike Bool where instance BaseUniverse fn => PredLike (Term fn Bool) where type UnivConstr (Term fn Bool) fn' = fn ~ fn' toPredExplain es (Lit b) = toPredExplain es b - toPredExplain [] tm = Assert (pure "toPred Term") tm + toPredExplain [] tm = Assert (pure ("Not (" ++ show tm ++ ")")) tm toPredExplain es tm = Assert (NE.fromList es) tm ------------------------------------------------------------------------ @@ -5294,6 +5415,16 @@ instance HasSpec fn a => Pretty (WithPrec (Term fn a)) where pretty (WithPrec p t) = case t of Lit n -> fromString $ showsPrec p n "" V x -> viaShow x + SubsetPat (Lit n) y -> parensIf (p > 10) $ "subset_" <+> short (Set.toList n) <+> prettyPrec 10 y + SubsetPat y (Lit n) -> parensIf (p > 10) $ "subset_" <+> prettyPrec 10 y <+> short (Set.toList n) + DisjointPat (Lit n) y -> parensIf (p > 10) $ "disjoint_" <+> short (Set.toList n) <+> prettyPrec 10 y + DisjointPat y (Lit n) -> parensIf (p > 10) $ "disjoint_" <+> prettyPrec 10 y <+> short (Set.toList n) + UnionPat (Lit n) y -> parensIf (p > 10) $ "union_" <+> short (Set.toList n) <+> prettyPrec 10 y + UnionPat y (Lit n) -> parensIf (p > 10) $ "union_" <+> prettyPrec 10 y <+> short (Set.toList n) + MemberPat y (Lit n) -> parensIf (p > 10) $ "member_" <+> prettyPrec 10 y <+> short (Set.toList n) + ElemPat y (Lit n) -> parensIf (p > 10) $ "elem_" <+> prettyPrec 10 y <+> short n + AppendPat (Lit n) y -> parensIf (p > 10) $ "append_" <+> short n <+> prettyPrec 10 y + AppendPat y (Lit n) -> parensIf (p > 10) $ "append_" <+> prettyPrec 10 y <+> short n App f Nil -> viaShow f App f as | Just Equal <- extractFn @(EqFn fn) f diff --git a/libs/constrained-generators/src/Constrained/Spec/Map.hs b/libs/constrained-generators/src/Constrained/Spec/Map.hs index 6582b7c6994..2071b8f10c5 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Map.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Map.hs @@ -144,18 +144,27 @@ instance combineSpec (MapSpec mHint mustKeys mustVals size kvs foldSpec) - (MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = fromGESpec $ do - typeSpec - . MapSpec - -- This is min because that allows more compositionality - if a spec specifies a - -- low upper bound because some part of the spec will be slow it doesn't make sense - -- to increase it somewhere else because that part isn't slow. - (unionWithMaybe min mHint mHint') - (mustKeys <> mustKeys') - (nub $ mustVals <> mustVals') - (size <> size') - (kvs <> kvs') - <$> combineFoldSpec foldSpec foldSpec' + (MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = case combineFoldSpec foldSpec foldSpec' of + Left msgs -> + ErrorSpec $ + NE.fromList $ + [ "Error in combining FoldSpec in combineSpec for Map" + , " " ++ show foldSpec + , " " ++ show foldSpec' + ] + ++ msgs + Right foldSpec'' -> + typeSpec $ + MapSpec + -- This is min because that allows more compositionality - if a spec specifies a + -- low upper bound because some part of the spec will be slow it doesn't make sense + -- to increase it somewhere else because that part isn't slow. + (unionWithMaybe min mHint mHint') + (mustKeys <> mustKeys') + (nub $ mustVals <> mustVals') + (size <> size') + (kvs <> kvs') + foldSpec'' conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec) = and diff --git a/libs/constrained-generators/src/Constrained/Univ.hs b/libs/constrained-generators/src/Constrained/Univ.hs index b77efbd6a33..14317595bf0 100644 --- a/libs/constrained-generators/src/Constrained/Univ.hs +++ b/libs/constrained-generators/src/Constrained/Univ.hs @@ -26,6 +26,7 @@ import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) import Data.Set qualified as Set +import Data.Typeable class FunctionLike fn where -- | The semantics of a function is given by `sem` @@ -330,31 +331,34 @@ type family SumOver as where singletonFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[a] (Set a) singletonFn = injectFn $ Singleton @_ @fn -unionFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] (Set a) +unionFn :: + forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] (Set a) unionFn = injectFn $ Union @_ @fn -subsetFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool +subsetFn :: + forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] Bool subsetFn = injectFn $ Subset @_ @fn -memberFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[a, Set a] Bool +memberFn :: forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[a, Set a] Bool memberFn = injectFn $ Member @_ @fn -elemFn :: forall fn a. (Member (SetFn fn) fn, Eq a) => fn '[a, [a]] Bool +elemFn :: forall fn a. (Member (SetFn fn) fn, Eq a, Show a, Typeable a) => fn '[a, [a]] Bool elemFn = injectFn $ Elem @_ @fn -disjointFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool +disjointFn :: + forall fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) => fn '[Set a, Set a] Bool disjointFn = injectFn $ Disjoint @_ @fn fromListFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[[a]] (Set a) fromListFn = injectFn $ FromList @_ @fn data SetFn (fn :: [Type] -> Type -> Type) args res where - Subset :: Ord a => SetFn fn '[Set a, Set a] Bool - Disjoint :: Ord a => SetFn fn '[Set a, Set a] Bool - Member :: Ord a => SetFn fn '[a, Set a] Bool + Subset :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool + Disjoint :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] Bool + Member :: (Ord a, Show a, Typeable a) => SetFn fn '[a, Set a] Bool Singleton :: Ord a => SetFn fn '[a] (Set a) - Union :: Ord a => SetFn fn '[Set a, Set a] (Set a) - Elem :: Eq a => SetFn fn '[a, [a]] Bool + Union :: (Ord a, Show a, Typeable a) => SetFn fn '[Set a, Set a] (Set a) + Elem :: (Eq a, Show a, Typeable a) => SetFn fn '[a, [a]] Bool FromList :: Ord a => SetFn fn '[[a]] (Set a) deriving instance Show (SetFn fn args res)