Skip to content
This repository was archived by the owner on Jan 9, 2026. It is now read-only.
Merged
Show file tree
Hide file tree
Changes from 19 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions docs/en/pact-properties-api.md
Original file line number Diff line number Diff line change
Expand Up @@ -489,6 +489,19 @@ Supported in either invariants or properties.

Supported in either invariants or properties.

### hash {#FBoolHash}

```lisp
(hash s)
```

* takes `s`: `bool`
* produces `string`

BLAKE2b 256-bit hash of bool values

Supported in properties only.

## Object operators {#Object}

### at {#FObjectProjection}
Expand Down Expand Up @@ -635,6 +648,21 @@ List / string / object contains

Supported in either invariants or properties.

### enumerate {#FEnumerate}

```lisp
(enumerate from to step)
```

* takes `from`: `integer`
* takes `to`: `integer`
* takes `step`: `integer`
* produces [`integer`]

Returns a sequence of numbers as a list

Supported in either invariants or properties.

### reverse {#FReverse}

```lisp
Expand Down Expand Up @@ -759,6 +787,20 @@ reduce a list by applying `f` to each element and the previous result

Supported in either invariants or properties.

### hash {#FListHash}

```lisp
(hash xs)
```

* takes `xs`: [_a_]
* produces `string`
* where _a_ is of type `integer`, `decimal`, `bool`, or `string`

BLAKE2b 256-bit hash of lists

Supported in properties only.

## String operators {#String}

### length {#FStringLength}
Expand Down Expand Up @@ -845,6 +887,33 @@ drop the first `n` values from `xs` (dropped from the end if `n` is negative)

Supported in either invariants or properties.

### hash {#FStringHash}

```lisp
(hash s)
```

* takes `s`: `string`
* produces `string`

BLAKE2b 256-bit hash of string values

Supported in properties only.

### hash {#FNumericalHash}

```lisp
(hash s)
```

* takes `s`: _a_
* produces `string`
* where _a_ is of type `integer` or `decimal`

BLAKE2b 256-bit hash of numerical values

Supported in properties only.

## Temporal operators {#Temporal}

### add-time {#FTemporalAddition}
Expand Down
56 changes: 53 additions & 3 deletions src-tool/Pact/Analyze/Eval/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,16 @@ import Pact.Analyze.Types.Eval
import Pact.Analyze.Util (Boolean (..), vacuousMatch)
import qualified Pact.Native as Pact
import Pact.Types.Pretty (renderCompactString)
import Pact.Types.Hash (pactHash)
import Pact.Types.Util (AsString(asString))
import Data.Text.Encoding (encodeUtf8)
import qualified Data.Aeson as Aeson
import qualified Pact.Types.Lang as Pact
import qualified Pact.Types.PactValue as Pact
import Data.ByteString.Lazy.Char8 (toStrict)
import qualified Data.ByteString as BS
import Data.Functor ((<&>))
import qualified Data.Vector as V

-- | Bound on the size of lists we check. This may be user-configurable in the
-- future.
Expand Down Expand Up @@ -145,6 +155,12 @@ truncate63 i = ite (i .< lowerBound)
upperBound = literal bound
lowerBound = literal (- bound)

notStaticErr :: AnalyzeFailureNoLoc
notStaticErr = FailureMessage "Hash requires statically known content"

symHash :: BS.ByteString -> S Str
symHash = literalS . Str . T.unpack . asString . pactHash

evalCore :: forall m a.
(Analyzer m, SingI a) => Core (TermOf m) a -> m (S (Concrete a))
evalCore (Lit a)
Expand All @@ -171,11 +187,10 @@ evalCore (Enumerate from to step) = do
let
go :: (forall v. OrdSymbolic v => v -> v -> SBV Bool) -> SBV Integer -> SBV Integer -> SBV Integer -> SBV [Integer]
go cmp b e s = ite (b `cmp` e) (b SBVL..: go cmp (b + s) e s) SBVL.nil

let algPos = ite (from' .== to') (SBVL.singleton from')
(ite (step' .== 0) (SBVL.singleton from' )
(ite (from' + step' .> to') (SBVL.singleton from') (go (.<=) from' to' step')))

algNeg = ite (step' .== 0) (SBVL.singleton from' )
(ite (from' + step' .< to') (SBVL.singleton from') (go (.>=) from' to' step'))

Expand Down Expand Up @@ -231,6 +246,41 @@ evalCore (StrContains needle haystack) = do
_sSbv (coerceS @Str @String needle')
`SBVS.isInfixOf`
_sSbv (coerceS @Str @String haystack')

-- hash values
-- TODO (RS): we should add warnings to the stack, allowing
-- to return shims in case, the content is not statically known
evalCore (StrHash sT) = eval sT <&> unliteralS >>= \case
Nothing -> throwErrorNoLoc notStaticErr
Just (Str b) -> pure (symHash (encodeUtf8 (T.pack b)))

evalCore (IntHash iT) = eval iT <&> unliteralS >>= \case
Nothing -> throwErrorNoLoc notStaticErr
Just i -> pure (symHash (toStrict (Aeson.encode (Pact.PLiteral ( Pact.LInteger i)))))

evalCore (BoolHash bT) = eval bT <&> unliteralS >>= \case
Nothing -> throwErrorNoLoc notStaticErr
Just b -> pure (symHash (toStrict ( Aeson.encode b)))

evalCore (DecHash d) = eval d <&> unliteralS >>= \case
Nothing -> throwErrorNoLoc notStaticErr
Just d' -> pure (symHash (toStrict (Aeson.encode (Pact.PLiteral (Pact.LDecimal (toPact decimalIso d'))))))

evalCore (ListHash ty' xs) = do
result <- withSymVal ty' $ withSing ty' $ eval xs <&> unliteralS >>= \case
Nothing -> throwErrorNoLoc notStaticErr
Just xs'' -> traverse (reify ty') xs''
pure (symHash (toStrict (Aeson.encode (Pact.PList (V.fromList result)))))
where
reify :: forall b. Sing b -> Concrete b -> m Pact.PactValue
reify t c = case t of
SStr -> pure $ Pact.PLiteral . Pact.LString . T.pack . unStr $ c
SInteger -> pure $ Pact.PLiteral . Pact.LInteger $ c
SDecimal -> pure $ Pact.PLiteral . Pact.LDecimal . toPact decimalIso $ c
SBool -> pure $ Pact.PLiteral . Pact.LBool $ c
SList t' -> Pact.PList . V.fromList <$> traverse (reify t') c
_ -> throwErrorNoLoc (FailureMessage "Unsupported type, currently we support integer, decimal, string, and bool")

evalCore (ListContains ty needle haystack) = withSymVal ty $ do
S _ needle' <- withSing ty $ eval needle
S _ haystack' <- withSing ty $ eval haystack
Expand Down Expand Up @@ -267,7 +317,7 @@ evalCore (ListDistinct ty list) = withSymVal ty $ withSing ty $ withEq ty $ do
S _ list' <- eval list
pure $ sansProv (SBVL.reverse (bfoldr listBound (\a b -> ite (SBVL.elem a b) b (a SBVL..: b)) SBVL.nil list'))


evalCore (ListDrop ty n list) = withSymVal ty $ withSing ty $ do
S _ n' <- eval n
S _ list' <- eval list
Expand Down
36 changes: 1 addition & 35 deletions src-tool/Pact/Analyze/Eval/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,16 +15,14 @@ module Pact.Analyze.Eval.Term where
import Control.Applicative (ZipList (..))
import Control.Lens (At (at), Lens', preview, use,
view, (%=), (%~), (&), (+=), (.=),
(.~), (<&>), (?~), (?=), (^.),
(.~), (?~), (?=), (^.),
(^?), (<>~), _1, _2, _head,
_Just, ifoldlM)
import Control.Monad (void, when)
import Control.Monad.Except (Except, MonadError (throwError))
import Control.Monad.Reader (MonadReader (ask, local), runReaderT)
import Control.Monad.RWS.Strict (RWST (RWST, runRWST))
import Control.Monad.State.Strict (MonadState, modify', runStateT)
import qualified Data.Aeson as Aeson
import Data.ByteString.Lazy (toStrict)
import Data.Constraint (Dict (Dict), withDict)
import Data.Default (def)
import Data.Foldable (foldl', foldlM)
Expand All @@ -43,14 +41,10 @@ import qualified Data.SBV.Tuple as SBVT
import Data.String (fromString)
import Data.Text (Text, pack)
import qualified Data.Text as T
import Data.Text.Encoding (encodeUtf8)
import Data.Traversable (for)
import Data.Type.Equality ((:~:)(Refl))
import GHC.TypeLits

import qualified Pact.Types.Hash as Pact
import qualified Pact.Types.PactValue as Pact
import qualified Pact.Types.Persistence as Pact
import Pact.Types.Pretty (renderCompactString', pretty)
import Pact.Types.Runtime (tShow)
import qualified Pact.Types.Runtime as Pact
Expand Down Expand Up @@ -721,34 +715,6 @@ evalTerm = \case
Just time -> pure $ literalS $ fromPact timeIso time
_ -> throwErrorNoLoc "We can only analyze calls to `parse-time` with statically determined contents (both arguments)"

Hash value -> do
let sHash = literalS . Str . T.unpack . Pact.asString . Pact.pactHash
notStaticErr :: AnalyzeFailure
notStaticErr = AnalyzeFailure dummyInfo "We can only analyze calls to `hash` with statically determined contents"
case value of
-- Note that strings are hashed in a different way from the other types
Some SStr tm -> eval tm <&> unliteralS >>= \case
Nothing -> throwError notStaticErr
Just (Str str) -> pure $ sHash $ encodeUtf8 $ T.pack str

-- Everything else is hashed by first converting it to JSON:
Some SInteger tm -> eval tm <&> unliteralS >>= \case
Nothing -> throwError notStaticErr
Just int -> pure $ sHash $ toStrict $ Aeson.encode $ Pact.PLiteral $ Pact.LInteger int
Some SBool tm -> eval tm <&> unliteralS >>= \case
Nothing -> throwError notStaticErr
Just bool -> pure $ sHash $ toStrict $ Aeson.encode bool

-- In theory we should be able to analyze decimals -- we just need to be
-- able to convert them back into Decimal.Decimal decimals (from SBV's
-- Real representation). This is probably possible if we think about it
-- hard enough.
Some SDecimal _ -> throwErrorNoLoc "We can't yet analyze calls to `hash` on decimals"

Some (SList _) _ -> throwErrorNoLoc "We can't yet analyze calls to `hash` on lists"
Some (SObject _) _ -> throwErrorNoLoc "We can't yet analyze calls to `hash` on objects"
Some _ _ -> throwErrorNoLoc "We can't yet analyze calls to `hash` on non-{string,integer,bool}"

Pact steps -> local (inPact .~ sTrue) $ do
-- We execute through all the steps once (via a left fold), then we execute
-- all the rollbacks (via for), in reverse order.
Expand Down
69 changes: 68 additions & 1 deletion src-tool/Pact/Analyze/Feature.hs
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ data Feature
| FCeilingRound
| FFloorRound
| FModulus

-- Bitwise operators
| FBitwiseAnd
| FBitwiseOr
Expand Down Expand Up @@ -126,6 +127,11 @@ data Feature
| FStringToInteger
| FStringTake
| FStringDrop
-- Hash operators
| FStringHash
| FNumericalHash
| FBoolHash
| FListHash
-- Temporal operators
| FTemporalAddition
-- Quantification forms
Expand Down Expand Up @@ -959,7 +965,7 @@ doc FEnumerate = Doc
InvAndProp
"Returns a sequence of numbers as a list"
[ Usage
"(drop n xs)"
"(enumerate from to step)"
Map.empty
$ Fun
Nothing
Expand Down Expand Up @@ -1222,6 +1228,63 @@ doc FStringToInteger = Doc
(TyCon int)
]

-- Hash features

doc FStringHash = Doc
"hash"
CString
PropOnly
"BLAKE2b 256-bit hash of string values"
[ Usage
"(hash s)"
Map.empty
$ Fun
Nothing
[ ("s", TyCon str)]
(TyCon str)
]
doc FNumericalHash = Doc
"hash"
CString
PropOnly
"BLAKE2b 256-bit hash of numerical values"
[ let a = TyVar $ TypeVar "a"
in Usage
"(hash s)"
(Map.fromList [("a", OneOf [int, dec])])
$ Fun
Nothing
[ ("s", a)]
(TyCon str)
]
doc FBoolHash = Doc
"hash"
CLogical
PropOnly
"BLAKE2b 256-bit hash of bool values"
[ Usage
"(hash s)"
Map.empty
$ Fun
Nothing
[ ("s", TyCon bool)]
(TyCon str)
]
doc FListHash = Doc
"hash"
CList
PropOnly
"BLAKE2b 256-bit hash of lists"
[ let a = TyVar $ TypeVar "a"
in Usage
"(hash xs)"
(Map.fromList [("a", OneOf [int, dec, bool, str])])
$ Fun
Nothing
[ ("xs", TyList' a)
]
(TyCon str)
]
-- Temporal features

doc FTemporalAddition = Doc
Expand Down Expand Up @@ -1772,6 +1835,10 @@ PAT(SStringTake, FStringTake)
PAT(SStringDrop, FStringDrop)
PAT(SConcatenation, FConcatenation)
PAT(SStringToInteger, FStringToInteger)
PAT(SStringHash, FStringHash)
PAT(SNumericalHash, FNumericalHash)
PAT(SBoolHash, FBoolHash)
PAT(SListHash, FListHash)
PAT(STemporalAddition, FTemporalAddition)
PAT(SUniversalQuantification, FUniversalQuantification)
PAT(SExistentialQuantification, FExistentialQuantification)
Expand Down
10 changes: 10 additions & 0 deletions src-tool/Pact/Analyze/Parse/Prop.hs
Original file line number Diff line number Diff line change
Expand Up @@ -669,6 +669,16 @@ inferPreProp preProp = case preProp of
str' <- checkPreProp SStr str
pure $ Some SInteger $ CoreProp $ StrToInt str'

PreApp s [str] | s == SStringHash -> do
Some ty str' <- inferPreProp str
case ty of
SDecimal -> pure $ Some SStr $ CoreProp $ DecHash str'
SInteger -> pure $ Some SStr $ CoreProp $ IntHash str'
SStr -> pure $ Some SStr $ CoreProp $ StrHash str'
SBool -> pure $ Some SStr $ CoreProp $ BoolHash str'
SList ty' -> pure $ Some SStr $ CoreProp $ ListHash ty' str'
_ -> throwErrorIn preProp "`hash` works only with integer, decimals, strings, bools, and list of those"

PreApp s [str, base] | s == SStringToInteger -> do
str' <- checkPreProp SStr str
base' <- checkPreProp SInteger base
Expand Down
7 changes: 6 additions & 1 deletion src-tool/Pact/Analyze/PrenexNormalize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,12 @@ singFloat ty p = case p of
CoreProp (StrDrop s1 s2) -> PStrDrop <$> float s1 <*> float s2
CoreProp (StrConcat s1 s2) -> PStrConcat <$> float s1 <*> float s2
CoreProp (Typeof tya a) -> CoreProp . Typeof tya <$> singFloat tya a

-- hash
CoreProp (StrHash s) -> CoreProp . StrHash <$> float s
CoreProp (IntHash s) -> CoreProp . IntHash <$> float s
CoreProp (BoolHash s) -> CoreProp . BoolHash <$> float s
CoreProp (DecHash s) -> CoreProp . DecHash <$> float s
CoreProp (ListHash ty' s) -> CoreProp . ListHash ty' <$> singFloat (SList ty') s
-- time
CoreProp (IntAddTime time int) -> PIntAddTime <$> float time <*> float int
CoreProp (DecAddTime time dec) -> PDecAddTime <$> float time <*> float dec
Expand Down
Loading