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.

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.

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.

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.

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.

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.

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.

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.