SecTeal ❯_

SecTeal (Secure Teal) is the programming language for Algorand stateless smart contracts (stateless ASC1) derived from the formal model of Algorand presented in [OMITTED]. The model abstracts stateless smart contracts by means of a language of expressions that evaluate to true or false.

Such an interpretation enables a natural interpretation of the semantics of a smart contract in Algorand, whose evaluation reverts to true or false, consequently authorising or refusing a transaction in the Algorand blockchain.

Such abstract approach lends itself to both express contracts' intended behaviour in a simple, logical way, and support formal verification of contracts' properties.

This page provides a compiler from SecTeal to Teal, the native, layer-one, smart contract language of Algorand.

This is part of an ongoing research effort aiming to develop general formal verification of smart contracts, with Algorand as a case study.

SecTeal language (grammar). This is an experimental prototype that works on strict syntactic rules dictating how you need to write your smart contracts. The following grammar defines the expression accepted by the compiler (spaces must be respected):

exp ::= val        a value
  | (exp ◦ exp)      ◦∈{+,−,<,=,>,∗,/,%,and,or}
  | not (exp)      negation
  | txlen          number of tx in the atomic group
  | txpos            index of current tx in the atomic group
  | txid(INT)         identifier ofn-th tx in the atomic group
  | tx(INT).FIELD      value of n-th tx's field
  | arglen          number of arguments of the current tx
  | arg(INT)       n-th argument of the current tx
  | H(exp)       Hash
  | versig(exp1, exp2, exp3)       signature verification

val :: = byte base64 BYTE
  | int BYTE
  | addr BYTE

BYTE :: = [a-z0-9]+      any sequence of letters and digits
INT :: = [0-9]+         any sequence of digits
FIELD :: = 'snd' | 'rcv' | 'crcv' | 'val' | 'fv' | 'lv' | 'lx' | 'type' | 'asst' | 'asstval' | 'asstsnd' | 'asstrcv' | 'casstrcv' | 'fee' | 'note'


[1] M. Bartoletti, A. Bracciali, C. Lepore, A. Scalas, R. Zunino “A formal model of Algorand smart contracts”. In N. Borisov and C. Diaz (eds) Proceedings of 25th International Conference on Financial Cryptography and Data Security 2021. March, 1-5, 2021, Online. Lecture Notes in Computer Science, Springer, 2021. To appear. (preliminary version at https://arxiv.org/abs/2009.12140".

Compile Your Own Example

Insert your contract as an expression from the grammar exp on a single line, respecting space rules (see examples) and press Compile (see text in the box as an example). You will get the Teal (executable) code corresponding to your SecTeal contract.

USE AT YOUR OWN RISK! still an under dev prototype.

Select an Example

This is a first simple example. The scenario shows a check on the receiver address.

Check receiver:

(tx(0).rcv = addr ZZAF5ARA4MEC5PVDOP64JM5O5MQST63Q2KOY2FLYFLXXD3PFSNJJBYAFZM)