User-Defined Checkers

Docs

Use TSA to check custom properties of your contracts.

A more advanced mode of TSA operation is the checking mode that allows users to implement their own checkers to validate specific contract specifications. This mode has its own specific format of the input files and a set of functions that are used to implement the checkers.

This page provides a short description of the checker structure and its special functions. For a complete guide and a full understanding of the process, refer to our tutorial on writing user-defined checkers (part 1, part 2).

Checker structure

Any custom checker consists of a checker file, list of analyzed smart contracts and some options. It could be then run with a Docker or JAR with custom-checker argument provided.

Checker file

The checker itself is a FunC file with implemented main method as an entrypoint for the analysis. For verifying safety properties of analyzed contracts, intrinsic functions are provided. The more detailed overview of these functions is provided below.

Usually, the checker file contains a set of assumptions for the input values that would be passed to a method of the first analyzed contract, call invocation of this method and then a set of assertions for the return values and/or the state of the contract after the method execution.

List of analyzed smart contracts

Analyzed smart contracts could be passed in different supported formats (Tact, FunC, Fift, BoC) and their order is important – the first contract in the list receives the contract_id equals to 1, the next – 2, and so on. These ids are then used in the tsa_call functions to specify the contract to call the method of, and in an inter-contract communication scheme if provided.

Checker functions

These intrinsic instructions are only valid in the checker contract. They are declared in the generated file tsa_functions.fc.

Calls Table

call signature	description
`int tsa_mk_int(int bits, int signed)`	create a symbolic integer value
`() tsa_forbid_failures()`	starts the assumption scope
`() tsa_allow_failures()`	ends the assumption scope
`() tsa_assert(int condition)`	creates an assumption
`() tsa_assert_not(int condition)`	creates an assumption
`forall A -> () tsa_fetch_value(A value, int value_id)`	captures the value and binds it to the index `value_id`; the captured value would be displayed in the output
`() tsa_send_internal_message(int contract_id, int input_id)`	sends an internal message to a contract with the given id; `input_id` might be used in `on_internal_message_send` handler
`() tsa_send_external_message(int contract_id, int input_id)`	sends an external message to a contract with the given id; `input_id` might be used in `on_external_message_send` handler
`cell tsa_get_c4(int contract_id)`	gets the c4 of the contract
`tsa_call_X_Y(args... , int contract_id, int method_id)`	call the method `method_id` of the specified smart contract with `Y` input parameters (passed in `args...`) that returns `X` values
`int tsa_get_balance(int contract_id)`	gets the balance of a contract `contract_id`
`() tsa_set_c4(int contract_id, cell value)`	sets the c4 of the contract (see notes)
`() tsa_make_address_random(slice address)`	see notes
`() tsa_make_slice_independent_from_random_addresses(slice independent_slice)`	see notes
`int tsa_input_was_accepted(int input_id)`	checks whether an ACCEPT instruction was called on handling the message with specified `input_id`; only valid for external messages
`() tsa_send_internal_message_with_body(slice body, int contract_id, int input_id)`	sends an internal message with a specified body
`() tsa_send_external_message_with_body(slice body, int contract_id, int input_id)`	sends an external message with a specified body

Notes

tsa_fetch_value should be called exactly once per execution with the same input_id.

An assumption implies that we only consider the executions that satisfy the assumptions. Thus, we filter out execution that fail the assertions or cause failures within an assumption scope. For example, when we perform a load_int instruction within the assumption scope, only the executions where the loading occurred without any exception (like cell underflow) would be considered.

tsa_set_c4 should only be used within the main or on_internal_message_send/on_external_message_send functions of a checker.

tsa_make_slice_independent_from_random_addresses and tsa_make_address_random represent the following semantic. Let addrs be slices tagged as random addresses and ss be slices tagged independent of random addresses. Then, during the final constraint solving (at the very end of symbolic execution), the concretization steps will be performed:

the full constraint set will be solved; if not satisfiable, the symbolic state is discarded as unreachable;
ss are concretized (i.e. fixed to the value from the model obtained in the previous step) and the updated constraint set is solved;
if still satisfiable, addrs are concretized to random standard addresses and the constraint is solved again.

Handlers

Handlers are functions that are invoked in a callback-like manner in response to an event. The event can usually be derived from the name of a handler.

Always use impure and method_id modifiers when declaring handlers.

On internal message send

Signature:

() on_internal_message_send(int balance, int msg_value, cell in_msg_full, slice msg_body, int input_id) impure method_id

Semantics

This handler is called after the message was sent by the checker to the receiver contract, but before its first instruction was executed. Its arguments are the same (with the addition of input_id) as those recv_internal would have after receiving the message.

This handler should be used to verify the input parameters of the recv_internal call in the context of the receiver contract.

Note

You probably do not want to verify the global state of contracts (e.g. its balance) in this handler, as it will be called on each of the sent messages. It is recommended to perform such checks before sending the message (i.e. before the call to tsa_send_internal_message).

On external message send

Signature:

() on_external_message_send(int balance, int msg_value, cell in_msg_full, slice msg_body, int input_id) impure method_id

Semantics

Same as for on_internal_message_send, but for external messages.

On out message

Signature

() on_out_message(int contract_message_number, cell msg_full, slice msg_body, int receiver_contract_id, int sender_contract_id) impure method_id

Semantics

This handler is called after the action phase of the contract on each message that was eventually sent into the network, regardless of whether the receiver is one of the contracts under test.

The contract_message_number is the order number of the message relative within the action phase it was sent in. Numeration starts with zero.

receiver_contract_id might be equal to -1 if the receiving contract was resolved to be not within the contracts under test.

On compute phase exit

Signature

() on_compute_phase_exit(cell c5, int exit_code, int compute_fee, int contract_id) impure method_id {

Semantics

This handler is called after the compute phase of the contract, no matter whether it ended successfully or with an exit code. The c5 argument contains an action list at the point of contract exit.

PreviousTSA Execution Exits Overview

NextInter-Contract Analysis