Scilla Built Ins

Here we enumerate the built-in data types and their operations, as well as the standard library.

Primitive types

For built-in primitive data types and operations on them, check the following implementation.

Built-ins operations on primitive types currently supported

Strings

• eq s1 s1 : Is String s1 equal to String s2. Returns Bool.
• concat s1 s2 : Concatenate String s1 with String s2. Returns String.
• substr s1 i2 i2 : Extract sub-string of String s2 starting from position Uint32 i1 with length Uint32 i2. Returns String.
• to_string x1: Convert x1 to a string literal. Valid types of x1 are IntX, UintX, ByStrX and ByStr.

Crypto

Hash is represented by the data type ByStr32. In the below description, Any can be IntX, UintX, String, ByStrX or ByStr

• eq h1 h2: Is ByStr32 h1 equal to ByStr32 h2. Returns Bool.
• to_uint256 b: Convert b : ByStrX when X <= 32 into uint256.
• sha256hash x : The SHA256 hash of value Any x. Returns ByStr32 .
• schnorr_gen_key_pair: Generate a private key / public key pair. Returns Pair{ByStr32 ByStr33}.
• schnorr_sign privK pubK m: Signs a message ByStr m using the private and public keys ByStr32 privK and ByStr33 pubK. Returns the ByStr64 signature.
• schnorr_verify pubK m sig: Verifies that message ByStr m was signed by ByStr32 pubK with signature ByStr64 sig. Returns Bool.
• concat x1 x2: Concatenate x1 : ByStrX1 and x2 : ByStrX2 to result in a ByStr(X1+X2) value.

Maps

Keys can have types IntX, UintX, String, ByStr32 or ByStr20. Values can be of any type.

• put m k v: Insert key k and value v into Map m. Returns a new Map.
• get m k: In Map m, for key k, return the associated value as Option v. The returned value is None if k is not in the map m.
• remove k: Remove key k and it's associated value v from the map. Returns a new updated Map.
• contains k: Is key k and it's associated value v present in the map? Returns Bool.
• to_list m: Convert Map m into a List (Pair ('A) ('B)) where 'A and 'B are key and value types.

IntX/UintX

For most IntX and UintX operations, there are two integer inputs.

• eq i1 i2: Is i1 equal to i2. Returns Bool.
• add i1 i2: Add integer values i1 and i2. Returns an integer.
• sub i1 i2: Subtract i2 from i1. Returns an integer.
• mul i1 i2: Integer product of i1 and i2. Returns an integer.
• div i1 i2: Integer division of i1 div i2. Returns an integer.
• rem i1 i2: Integer remainder when i1 is divided by i2. Returns an integer.
• lt i1 i2: Is i1 lesser than i2. Returns Bool.
• pow i1 i2: i1 raised to the power i2. Returns an integer of i1's type. i2 is Uint32.
• to_nat i1: Convert Uint32 i1 value to Nat.
• to_(u)int(32/64/128/256): Convert a UintX/IntX or String (that represents a number) value to another UintX/IntX value. Returns Some IntX/UintX if conversion succeeded, None otherwise.

Addition, subtraction, multiplication, pow, division and reminder operations may raise integer overflow, underflow and division_by_zero errors.

Addresses

Addresses are represented by the data type ByStr20.

• eq a1 a2: Is ByStr20 a1 equal to ByStr20 a2. Returns Bool.

Block Numbers

• eq b1 b2: Is BNum b1 equal to BNum b2. Returns Bool.
• blt b1 b2: Is BNum b1 less than BNum b2. Returns Bool.
• badd b1 i1: Add UintX i1 to BNum b1. Returns BNum.
• bsub b1 b2: Subtract BNum b2 from BNum b1. Returns Int256.

Algebraic Data Types

Recursion primitives

At the moment, Scilla features the following folding principles (structural recursion primitives) for Nats and Lists:

nat_fold : forall 'T, ('T -> Nat -> 'T) -> 'T -> Nat -> 'T
list_foldl: forall 'A . forall 'B . ('B -> 'A -> 'B) -> 'B -> (List 'A) -> 'B
list_foldr: forall 'A . forall 'B . ('A -> 'B -> 'B) -> 'B -> (List 'A) -> 'B

Check the Tutorial for more intuition and examples.

Derived standard library

Here we enumerate a series of functions, which are implemented as a part of the standard library via the built-in functions and recursion primitives. Those are going to be verified and made available for any Scilla program, so the clients wouldn't have to reinvent a wheel every time.

• list_map : ('A -> 'B) -> List 'A -> : List 'B.

  Apply f : 'A -> 'B to every element of l : List 'A. Linear complexity.

• list_filter : ('A -> Bool) -> List 'A -> List 'A.

  Preserving the order of elements in l : List 'A, return new list containing only those elements that satisfy the predicate f : 'A -> Bool. Linear complexity.

• list_head : (List 'A) -> (Option 'A).

  Return the head element of a list l : List 'A as Some 'A, None if l is Nil (the empty list).

• list_tail : (List 'A) -> (Option List 'A).

  For input list l : List 'A, returns Some l', where l' is l except for it's head; returns Some Nil if l has only one element; returns None if l is empty.

• list_append : (List 'A -> List 'A -> List 'A).

  Append the second list to the first one and return a new List. Linear complexity (on first list).

• list_reverse : (List 'A -> List 'A).

  Return the reverse of the input list. Linear complexity.

• list_flatten : (List List 'A) -> List 'A.

  Concatenate a list of lists. Each element (List 'A) of the input (List List 'A) are all concatenated together (in the same order) to give the result. linear complexity over the total number of elements in all of the lists.

• list_length : List 'A -> Int32

  Number of elements in list. Linear complexity.

• list_eq : ('A -> 'A -> Bool) -> List 'A -> List 'A -> Bool.

  Takes a function f : 'A -> 'A -> Bool to compare elements of lists l1 : List 'A and l2 : List 'A and returns True iff all elements of the lists compare equal. Linear complexity.

• list_mem : ('A -> 'A -> Bool) -> 'A -> List 'A -> Bool.

  Checks whether an element a : 'A is in the list l : List'A. f : 'A -> 'A -> Bool should be provided for equality comparison. Linear complexity.

• list_forall : ('A -> Bool) -> List 'A -> Bool.

  Return True iff all elements of list l : List 'A satisfy predicate f : 'A -> Bool. Linear complexity.

• list_exists : ('A -> Bool) -> List 'A -> Bool.

  Return True if at least one element of list l : List 'A satisfies predicate f : 'A -> Bool. Linear complexity. Linear complexity.

• list_sort : ('A -> 'A -> Bool) -> List 'A -> List 'A.

  Stable sort the input list l : List 'A. Function flt : 'A -> 'A -> Bool provided must return True iff its first argument is lesser-than its second argument. Linear complexity.

• list_find : ('A -> Bool) -> 'A -> 'A .

  Return Some a, where a is the first element of l : List 'A that satisfies the predicate f : 'A -> Bool. Returns None iff none of the elements in l satisfy f. Linear complexity.

• list_zip : List 'A -> List 'B -> List (Pair 'A 'B).

  Combine corresponding elements of m1 : List 'A and m2 : List 'B into a Pair and return the resulting list. In case of different number of elements in the lists, the extra elements are ignored.

• list_zip_with : ('A -> 'B -> 'C) -> List 'A -> List 'B -> List 'C *). Linear complexity.

  Combine corresponding elements of m1 : List 'A and m2 : List 'B using f : 'A -> 'B -> 'C and return the resulting list of 'C. In case of different number of elements in the lists, the extra elements are ignored.

• list_unzip : List (Pair 'A 'B) -> Pair (List 'A) (List 'B).

  Convert a list l : Pair 'A 'B of Pairs into a Pair of lists. Linear complexity.

• list_nth : Int32 -> List 'A -> Option 'A.

  Returns Some 'A if n'th element exists in list. None otherwise. Linear complexity.

• nat_eq : Nat -> Nat -> Bool.

  Compare two natural numbers (Nat) for equality.

Conversions:

• list_to_map : List (Pair 'A 'B) -> Map 'A 'B

  Convert a list (l : Pair 'A 'B) of key-val pairs into a map (Map 'A 'B), overwriting duplicates.

• nat_to_int : Nat -> Uint32.

  Convert a natural number n : Nat into an integer.

• to_uintX and to_intX : IntX/UintX -> Option IntX/UintX. Conversion between integer types. All these utilities return Some IntX/UintX on success, None otherwise. A conversion is said to succeed if the source value can be represented in the destination type.

• intX_to_nat and uintX_to_nat : IntX/UintX -> Option Nat

  Convert signed and unsigned integers to Nat. Returns Some Nat on successful conversion, None otherwise. The built-in to_nat supports only converting Uint32 values to Nat. Hence these wrappers succeed only if the input value can be represented in Uint32.