Property and Invariant Functions¶

These are functions available in properties and invariants – not necessarily in executable Pact code. All of these functions are available in properties, but only a subset are available in invariants. As a general rule, invariants have vocabulary for talking about the shape of data, whereas properties also add vocabulary for talking about function inputs and outputs, and database interactions. Each function also explicitly says whether it’s available in just properties, or invariants as well.

Numerical operators¶

+¶

(+ x y)

takes x: a
takes y: a
produces a
where a is of type integer or decimal

Addition of integers and decimals.

Supported in either invariants or properties.

-¶

(- x y)

takes x: a
takes y: a
produces a
where a is of type integer or decimal

Subtraction of integers and decimals.

Supported in either invariants or properties.

*¶

(* x y)

takes x: a
takes y: a
produces a
where a is of type integer or decimal

Multiplication of integers and decimals.

Supported in either invariants or properties.

/¶

(/ x y)

takes x: a
takes y: a
produces a
where a is of type integer or decimal

Division of integers and decimals.

Supported in either invariants or properties.

^¶

(^ x y)

takes x: a
takes y: a
produces a
where a is of type integer or decimal

Exponentiation of integers and decimals.

Supported in either invariants or properties.

log¶

(log b x)

takes b: a
takes x: a
produces a
where a is of type integer or decimal

Logarithm of x base b.

Supported in either invariants or properties.

-¶

(- x)

takes x: a
produces a
where a is of type integer or decimal

Negation of integers and decimals.

Supported in either invariants or properties.

sqrt¶

(sqrt x)

takes x: a
produces a
where a is of type integer or decimal

Square root of integers and decimals.

Supported in either invariants or properties.

ln¶

(ln x)

takes x: a
produces a
where a is of type integer or decimal

Logarithm of integers and decimals base e.

Supported in either invariants or properties.

exp¶

(exp x)

takes x: a
produces a
where a is of type integer or decimal

Exponential of integers and decimals. e raised to the integer or decimal x.

Supported in either invariants or properties.

abs¶

(abs x)

takes x: a
produces a
where a is of type integer or decimal

Absolute value of integers and decimals.

Supported in either invariants or properties.

round¶

(round x)

takes x: decimal
produces integer

(round x prec)

takes x: decimal
takes prec: integer
produces integer

Banker’s rounding value of decimal x as integer, or to prec precision as decimal.

Supported in either invariants or properties.

ceiling¶

(ceiling x)

takes x: decimal
produces integer

(ceiling x prec)

takes x: decimal
takes prec: integer
produces integer

Rounds the decimal x up to the next integer, or to prec precision as decimal.

Supported in either invariants or properties.

floor¶

(floor x)

takes x: decimal
produces integer

(floor x prec)

takes x: decimal
takes prec: integer
produces integer

Rounds the decimal x down to the previous integer, or to prec precision as decimal.

Supported in either invariants or properties.

dec¶

(dec x)

takes x: integer
produces decimal

Casts the integer x to its decimal equivalent.

Supported in either invariants or properties.

mod¶

(mod x y)

takes x: integer
takes y: integer
produces integer

Integer modulus

Supported in either invariants or properties.

Bitwise operators¶

&¶

(& x y)

takes x: integer
takes y: integer
produces integer

Bitwise and

Supported in either invariants or properties.

|¶

(| x y)

takes x: integer
takes y: integer
produces integer

Bitwise or

Supported in either invariants or properties.

xor¶

(xor x y)

takes x: integer
takes y: integer
produces integer

Bitwise exclusive-or

Supported in either invariants or properties.

shift¶

(shift x y)

takes x: integer
takes y: integer
produces integer

Shift x y bits left if y is positive, or right by -y bits otherwise.

Supported in either invariants or properties.

~¶

(~ x)

takes x: integer
produces integer

Reverse all bits in x

Supported in either invariants or properties.

Logical operators¶

>¶

(> x y)

takes x: a
takes y: a
produces bool
where a is of type integer or decimal

True if x > y

Supported in either invariants or properties.

<¶

(< x y)

takes x: a
takes y: a
produces bool
where a is of type integer or decimal

True if x < y

Supported in either invariants or properties.

>=¶

(>= x y)

takes x: a
takes y: a
produces bool
where a is of type integer or decimal

True if x >= y

Supported in either invariants or properties.

<=¶

(<= x y)

takes x: a
takes y: a
produces bool
where a is of type integer or decimal

True if x <= y

Supported in either invariants or properties.

=¶

(= x y)

takes x: a
takes y: a
produces bool
where a is of type integer, decimal, string, time, bool, object, or keyset

True if x = y

Supported in either invariants or properties.

!=¶

(!= x y)

takes x: a
takes y: a
produces bool
where a is of type integer, decimal, string, time, bool, object, or keyset

True if x != y

Supported in either invariants or properties.

and¶

(and x y)

takes x: bool
takes y: bool
produces bool

Short-circuiting logical conjunction

Supported in either invariants or properties.

or¶

(or x y)

takes x: bool
takes y: bool
produces bool

Short-circuiting logical disjunction

Supported in either invariants or properties.

not¶

(not x)

takes x: bool
produces bool

Logical negation

Supported in either invariants or properties.

when¶

(when x y)

takes x: bool
takes y: bool
produces bool

Logical implication. Equivalent to (or (not x) y).

Supported in either invariants or properties.

and?¶

(and? f g a)

takes f: a -> bool
takes g: a -> bool
takes a: a
produces bool

and the results of applying both f and g to a

Supported in either invariants or properties.

or?¶

(or? f g a)

takes f: a -> bool
takes g: a -> bool
takes a: a
produces bool

or the results of applying both f and g to a

Supported in either invariants or properties.

hash¶

(hash s)

takes s: bool
produces string

BLAKE2b 256-bit hash of bool values

Supported in properties only.

Object operators¶

at¶

(at k o)

takes k: string
takes o: object
produces a

(at i l)

takes i: integer
takes o: list
produces bool

projection

Supported in either invariants or properties.

+¶

(+ x y)

takes x: object
takes y: object
produces object

Object merge

Supported in either invariants or properties.

drop¶

(drop keys o)

takes keys: [string]
takes o: object
produces object

drop entries having the specified keys from an object

Supported in either invariants or properties.

take¶

(take keys o)

takes keys: [string]
takes o: object
produces object

take entries having the specified keys from an object

Supported in either invariants or properties.

length¶

(length o)

takes o: object
produces integer

the number of key-value pairs in the object

Supported in either invariants or properties.

List operators¶

at¶

(at k l)

takes k: string
takes l: [a]
produces a

(at i l)

takes i: integer
takes o: list
produces bool

projection

Supported in either invariants or properties.

length¶

(length s)

takes s: [a]
produces integer

List length

Supported in either invariants or properties.

contains¶

(contains x xs)

takes x: a
takes xs: [a]
produces bool

(contains k o)

takes k: string
takes o: object
produces bool

(contains value string)

takes value: string
takes string: string
produces bool

List / string / object contains

Supported in either invariants or properties.

enumerate¶

(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¶

(reverse xs)

takes xs: [a]
produces [a]

reverse a list of values

Supported in either invariants or properties.

sort¶

(sort xs)

takes xs: [a]
produces [a]

sort a list of values

Supported in either invariants or properties.

drop¶

(drop n xs)

takes n: integer
takes xs: [a]
produces [a]

drop the first n values from the beginning of a list (or the end if n is negative)

Supported in either invariants or properties.

take¶

(take n xs)

takes n: integer
takes xs: [a]
produces [a]

take the first n values from xs (taken from the end if n is negative)

Supported in either invariants or properties.

make-list¶

(make-list n a)

takes n: integer
takes a: a
produces [a]

create a new list with n copies of a

Supported in either invariants or properties.

map¶

(map f as)

takes f: a -> b
takes as: [a]
produces [b]

apply f to each element in a list

Supported in either invariants or properties.

filter¶

(filter f as)

takes f: a -> bool
takes as: [a]
produces [a]

filter a list by keeping the values for which f returns true

Supported in either invariants or properties.

distinct¶

(distinct xs)

takes xs: [a]
produces [a]

returns a list of distinct values

Supported in either invariants or properties.

fold¶

(fold f a bs)

takes f: a -> b -> a
takes a: a
takes bs: [b]
produces a

reduce a list by applying f to each element and the previous result

Supported in either invariants or properties.

hash¶

(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¶

length¶

(length s)

takes s: string
produces integer

String length

Supported in either invariants or properties.

+¶

(+ s t)

takes s: string
takes t: string
produces string

(+ s t)

takes s: [a]
takes t: [a]
produces [a]

String / list concatenation

Supported in either invariants or properties.

str-to-int¶

(str-to-int s)

takes s: string
produces integer

(str-to-int b s)

takes b: integer
takes s: string
produces integer

String to integer conversion

Supported in either invariants or properties.

take¶

(take n s)

takes n: integer
takes s: string
produces string

take the first n values from xs (taken from the end if n is negative)

Supported in either invariants or properties.

drop¶

(drop n s)

takes n: integer
takes s: string
produces string

drop the first n values from xs (dropped from the end if n is negative)

Supported in either invariants or properties.

hash¶

(hash s)

takes s: string
produces string

BLAKE2b 256-bit hash of string values

Supported in properties only.

hash¶

(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¶

add-time¶

(add-time t s)

takes t: time
takes s: a
produces time
where a is of type integer or decimal

Add seconds to a time

Supported in either invariants or properties.

Quantification operators¶

forall¶

(forall (x:string) y)

binds x: a
takes y: r
produces r
where a is any type
where r is any type

Bind a universally-quantified variable

Supported in properties only.

exists¶

(exists (x:string) y)

binds x: a
takes y: r
produces r
where a is any type
where r is any type

Bind an existentially-quantified variable

Supported in properties only.

column-of¶

(column-of t)

takes t: table
produces type

The type of columns for a given table. Commonly used in conjunction with quantification; e.g.: (exists (col:(column-of accounts)) (column-written accounts col)).

Supported in properties only.

Transactional operators¶

abort¶

abort

of type bool

Whether the transaction aborts. This function is only useful when expressing propositions that do not assume transaction success. Propositions defined via property implicitly assume transaction success. We will be adding a new mode in which to use this feature in the future – please let us know if you need this functionality.

Supported in properties only.

success¶

success

of type bool

Whether the transaction succeeds. This function is only useful when expressing propositions that do not assume transaction success. Propositions defined via property implicitly assume transaction success. We will be adding a new mode in which to use this feature in the future – please let us know if you need this functionality.

Supported in properties only.

governance-passes¶

governance-passes

of type bool

Whether the governance predicate passes. For keyset-based governance, this is the same as something like (authorized-by 'governance-ks-name). Pact’s property checking system currently does not analyze the body of a capability when it is used for governance due to challenges around capabilities making DB modifications – the system currently assumes that a capability-based governance predicate is equally capable of succeeding or failing. This feature allows describing the scenarios where the predicate passes or fails.

Supported in properties only.

result¶

result

of type r
where r is any type

The return value of the function under test

Supported in properties only.

Database operators¶

table-written¶

(table-written t)

takes t: a
produces bool
where a is of type table or string

Whether a table is written in the function under analysis

Supported in properties only.

table-read¶

(table-read t)

takes t: a
produces bool
where a is of type table or string

Whether a table is read in the function under analysis

Supported in properties only.

cell-delta¶

(cell-delta t c r)

takes t: a
takes c: b
takes r: string
produces c
where a is of type table or string
where b is of type column or string
where c is of type integer or decimal

The difference in a cell’s value before and after the transaction

Supported in properties only.

column-delta¶

(column-delta t c)

takes t: a
takes c: b
produces c
where a is of type table or string
where b is of type column or string
where c is of type integer or decimal

The difference in a column’s total summed value before and after the transaction

Supported in properties only.

column-written¶

(column-written t c)

takes t: a
takes c: b
produces bool
where a is of type table or string
where b is of type column or string

Whether a column is written to in a transaction

Supported in properties only.

column-read¶

(column-read t c)

takes t: a
takes c: b
produces bool
where a is of type table or string
where b is of type column or string

Whether a column is read from in a transaction

Supported in properties only.

row-read¶

(row-read t r)

takes t: a
takes r: string
produces bool
where a is of type table or string

Whether a row is read in the function under analysis

Supported in properties only.

row-written¶

(row-written t r)

takes t: a
takes r: string
produces bool
where a is of type table or string

Whether a row is written in the function under analysis

Supported in properties only.

row-read-count¶

(row-read-count t r)

takes t: a
takes r: string
produces integer
where a is of type table or string

The number of times a row is read during a transaction

Supported in properties only.

row-write-count¶

(row-write-count t r)

takes t: a
takes r: string
produces integer
where a is of type table or string

The number of times a row is written during a transaction

Supported in properties only.

row-exists¶

(row-exists t r time)

takes t: a
takes r: string
takes time: one of {“before”,“after”}
produces bool
where a is of type table or string

Whether a row exists before or after a transaction

Supported in properties only.

read¶

(read t r)

takes t: a
takes r: string
takes time: one of {“before”,“after”}
produces object
where a is of type table or string

The value of a read before or after a transaction

Supported in properties only.

Authorization operators¶

authorized-by¶

(authorized-by k)

takes k: string
produces bool

Whether the named keyset/guard is satisfied by the executing transaction

Supported in properties only.

row-enforced¶

(row-enforced t c r)

takes t: a
takes c: b
takes r: string
produces bool
where a is of type table or string
where b is of type column or string

Whether the keyset in the row is enforced by the function under analysis

Supported in properties only.

is-principal¶

(is-principal s)

takes s: string
produces bool

Whether s conforms to the principal format without proving validity.

Supported in either invariants or properties.

typeof-principal¶

(typeof-principal s)

takes s: string
produces string

Return the protocol type of the given s value. If input value is not a principal type, then the empty string is returned.

Supported in either invariants or properties.

Function operators¶

identity¶

(identity a)

takes a: a
produces a
where a is of type table or string

identity returns its argument unchanged

Supported in either invariants or properties.

constantly¶

(constantly a)

takes a: a
takes b: b
produces a

constantly returns its first argument, ignoring the second

Supported in either invariants or properties.

compose¶

(compose f g)

takes f: a -> b
takes g: b -> c
produces c

compose two functions

Supported in either invariants or properties.

Other operators¶

where¶

(where field f obj)

takes field: string
takes f: a -> bool
takes obj: object
produces bool

utility for use in filter and select applying f to field in obj

Supported in either invariants or properties.

typeof¶

(typeof a)

takes a: a
produces string

return the type of a as a string

Supported in either invariants or properties.