Type System

The security guarantees of ZK-SecreC are reflected by its type system. Types are checked (and inferred in certain cases) during compile time, hence the type system is part of the static semantics of ZK-SecreC. We describe a static semantics that traces also effects (e.g., assertions and mutable variable updates) that expression evaluation can cause. Therefore it is really a type and effect system. The type system makes sure that the program can be translated into the circuit, and into Prover's and Verifier's local computations.

ZK-SecreC supports first-order polymorphism only. Therefore we can avoid explicit quantification in type rules. Most of the typing rules handle types as monomorphic.

We also do not discuss type synonyms here for simplicity, and omit some complicated issues of structs. Similarly, we ignore higher-order functions (functions that take functions as parameters) and data structures with functions stored in them because of complicated issues regarding effects of the involved functions. Nevertheless, ZK-SecreC actually allows the programmer to define and use higher-order functions and store functions in data structures. For programs involving these features, ZK-SecreC fails to provide the usual privacy guarantees.

Notation

Choice of symbols

We use the following Latin and Greek letters in type rules (often with numeric indices):

The notions referred to are mostly explained in the next subsubsection.

We denote the set of all natural numbers by N, the set of all integers by Z, the set of all truth values by B, and the set of all Unicode characters by C. If A is any set of characters then A^* denotes the set of all finite strings over alphabet A. Stated formally:

Notions

Recall that qualified types are triples of the form t s d consisting of a data type, a stage and a domain. Effects in our type system also consist of three parts: a stage effect, a domain effect and a boolean effect. A stage effect is just a stage where the effect arises. A domain effect is an upward closed set of domains. A set of domains is called upward closed if, whenever a domain belongs to it, all higher domains also belong to it, assuming the ordering @public < @verifier < @prover of growing privacy. There are four upward closed sets of domains, ordered by inclusion as ∅ ⊂ ⟨@prover⟩ ⊂ ⟨@verifier⟩ ⊂ ⟨@public⟩, where ⟨d⟩ denotes the set consisting of the domain d and all higher domains. Boolean effects are type level booleans, denoted by tt and ff. They are needed for keeping track of statements that are forbidden in the right-hand sides of match expressions. We write effect triples with commas in the form s,D,b.

Function types in ZK-SecreC are of the form q₀ -> … -> q_n−1 -> q where q₀,…,q_n−1 are the argument types and q is the result type. Data types in qualified types cannot be function types, so we do not have mutual dependencies here. In our type system, function types are equipped with the effect an execution of the function body can trigger and the vectorizability status of the function. So our function types w end up in the form q₀ -> … -> q_n−1 -> q ! o ∷ b.

Function signatures can also incorporate a tuple of constraints imposed on the argument types or the result type of the function or on the constituents of them (data types, stages, domains). Type constraints are conditions imposed on types. Atomic type constraints can be:

• Stage identities of the form pre s or post s where s is a stage variable;
• Domain inequalities of the form d₁ ≤ d₂ where d₁ and d₂ are type level expressions that denote domains;
• Applications of type predicates to 0 or more type level expressions, e.g., Field N.

Only atomic type constraints can occur in function signatures. A type constraint is either an atomic type constraint or the negation of an atomic type constraint. We denote the negation of a type constraint c as ⁓c. Negation carries its standard meaning in the case of stage identites and domain inequalities where negation applications can be reduced. For example, the negation of pre s is post s and vice versa, the negation of @prover ≤ d is d ≤ @verifier. In the case of other atomic predicates, negation is equivalent to absence of the constraint in constraint solving.

ZK-SecreC allows assignments to variables and also to particular cells of existing data structures. Hence in the left-hand sides of assignments, offset variables can occur which are variables with an empty or a non-empty finite sequence of lookups, e.g., y or a[i].2.

A variable environment is a finite set of associations of the following kinds of components:

• Variable typings written in the form x : q;
• Variable mutability statements in the form mut x : b where the boolean indicates if the variable is mutable or not.

Likewise, a local group function environment is a finite set of function typings in the form f : w. It is intended to contain only functions in the same group of mutually recursive functions with the current function, besides functions defined locally by lambda expressions and partial evaluation. A constraint environment is a set of type constraints. Usually, the constraints come from the signature of the current function. If the current code comes from a branch of a conditional expression where the condition is a type constraint then this constraint can also contribute to the environment. Depending on the branch, it contributes with itself or its negation.

A global function environment consists of all functions in the program. Finally, a struct environment associates types to pairs consisting of a struct application and a field label. The struct environment is determined by the struct definitions in the program. The types can be parametrized. As parameters of ZK-SecreC struct definitions scope over the whole definition, all field types of the same struct type must have the same parameters.

Auxiliary functions

Recall that we use the ordering @public < @verifier < @prover of growing privacy on domains. The corresponding greatest lower bound operation ∧ and least upper bound operation ∨ find the minimum and maximum, respectively, of two domains. We use ≤ on upward closed sets of domains to denote the superset order, and ∧ and ∨ to denote the corresponding greatest lower bound and least upper bound operations, i.e.,

Recall that ⟨d⟩ denotes the set consisting of the domain d and all higher domains. This way, ≤ on upward closed domain sets respects the order on domains, i.e., ⟨d₁⟩ ≤ ⟨d₂⟩ if and only if d₁ ≤ d₂. We also order stages as $post < $pre, reflecting the fact that data computed in the circuit are also computed locally in the corresponding domain in order to be ready to provide expanded instances/witnesses to the circuit. This subtyping relation is reasonable also in the trustability aspect: Leaking trustable data ($post) into the untrustable world ($pre) causes no harm. For conciseness, we extend the ⟨⋅⟩ notation to stages by

This is reasonable since computations in the stage $post contribute to building of the circuit and the circuit is public. We extend the operator ∧ to tuples pointwise.

We write Γ(x) for lookup of the type of variable x and Γ(mut x) for lookup of the mutability status of the variable x in the variable environment Γ. Likewise, Φ(f) denotes the type of f in the local group function environment Φ. We also denote the definition of function f in the global function environment Π by Π(f). Mutability flags are not explicitly inserted into global function environment but they can be found in the signature of functions; therefore we denote the mutability status of the ith parameter (counting from 0) of function f by Π(ref(f.i)). Locally defined functions are not in Π; but as locally defined functions cannot have mutable parameters, we consider Π(ref(f.i)) to be false if f is not in Π. We write Σ(r)(l) for the possibly parametrized type associated to struct name r and field label l, and by dom(Σ(r)), we denote the set of all field labels defined in the struct type r.

If Π is the global function environment then scc Π denotes the set of groups of mutually recursive functions in the environment. Each function is represented by its name in scc Π. Ways of computing scc Π are out of scope of this document.

By convention, we denote integer, boolean and string literals by n, b and s, respectively, where n, b and s are the mathematical values. For instance, if n=103 (the number) then n=103 (the numeral).

In ZK-SecreC, mutability of a variable propagates to all constituents of its value (if it is a data structure). Therefore, for deciding if an assignment is legal, one must find the variable whose mutability implies feasibility of the assignment. We denote this function by var. The formal definition goes as follows:

For other syntactic forms, var is undefined. Such forms (e.g., list slices and vector lookups and slices) are not allowed in the left-hand side of assignment.

Well-structured types

ZK-SecreC does not allow arbitrary combinations of stages and domains in qualified types. The acceptable combinations are those we call well-structured types. This notion basically means three conditions:

• The domain of a data structure cannot be higher than that of its constituents;
• The domain of a data structure that involves constituents at the stage $post must be @public.

Formally, the notion can be defined as follows: Let q=t s d be a qualified type. Then q is called well-structured if all the following conditions hold:

• If t=uint or t=bool (with infinite modulus) then s=$pre;
• If t=() or t is a tuple type or t is a struct type then s=$pre and, whenever t' s' d' is its field type, ⟨d⟩ ≤ ⟨s'⟩∧⟨d'⟩ and t' s' d' is well-structured;
• If t=list[t' s' d'] or t=arr[t' s' d'] for some qualified type t' s' d' then s=$pre and ⟨d⟩ ≤ ⟨s'⟩∧⟨d'⟩ and t' s' d' is well-structured.

The notion of well-structuredness establishes interaction between domains and stages. In addition, ZK-SecreC applies a restriction that all (direct or indirect) constituents of integer and boolean types within the same vector must be at the same stage.

Deep cast is the means for ensuring well-structured types in the process of domain casts. Formally, changing of types in the case of deep cast is defined by functions dcast and ddcast which are defined as follows, using the least upper bound operation (∨) for conciseness:

The most important difference between dcast and ddcast is in handling stages. While dcast leaves stages unchanged in the case of primitive types, ddcast replaces all stages with $pre. This difference is essential as changing the domain of an isolated value of a primitive type to a higher one always results in a well-structured type but this is not the case if the primitive type lies inside a structural type.

Sized types

A function can be declared vectorizable only if all its argument types and the result type are sized. A data type is called sized if all values in the type occupy the same amount of memory, i.e., are of the same size. More formally, a data type is sized if it is uint[N] or bool[N] for some (finite or infinite) modulus N, or a tuple type with all component types being sized, or a struct type where all component types are sized. Note that list types and vector types, as well as all types having such types as constituents, are not sized. The type constraint Sized of ZK-SecreC captures the notion of sized types.

A qualified type t s d is called sized if its data type t is sized. There are more restrictions the qualified types of function parameters must meet for vectorizability. For expressing them, several auxiliary notions of the highest stage or domain of atomic constituents are needed. They are measured in terms of upward closed sets of domains. The first one can be formally defined as

The second one differs by the base case which takes domains instead of stages into account but falls into ∅ immediately if a value at the stage $post is encountered:

The definitions above assume that qualified types passed as argument to atomstglub and atomdomlub are sized since, due to the intended use cases, defining them on other types does not make sense. They are parametrized by the struct environment, as is actually the notion of sized type, too. These two notions are joined in the third one that finds the lowest of the two:

Both atomstglub_Σ and atomlub_Σ are extended to function types (without effects etc.) in a similar way by

Depending on the particular case, function types must satisfy either atomstglub_Σ(q₀ -> … -> q_n−1 -> q)=@public or atomlub_Σ(q₀ -> … -> q_n−1 -> q)=@public; the former restriction is stronger since it requires all atomic types throughout the function type to be at stage $post while the latter one allows some argument types or the result type to have atomic types qualified as $pre @public.

For an instance, consider the type q₀ -> q₁ -> q where

We obtain

whence

Similarly, we obtain

Thus

giving

Typing assertions

Assertions of expression and statement typing

Technically, statements in ZK-SecreC are also expressions. Therefore we shall talk about expressions only.

Assertions of expression typing are of one of the forms

This assertion states that, in the context of environments Γ,Φ,Κ,Π,Σ, the expression e has either a qualified type q or a function type w and computing the expression can trigger an effect o. Note that the function type also contains an effect which is unrelated to the effect o produced by computing the expression (that in the function type is produced by executing the function body when arguments will be provided). Likewise, the stage in the qualified type and that in the effect are not necessarily the same. The stage in the qualified type associates to the return value whereas that in the effect associates to the computation process. For example, an assertion expression causes an effect at the stage $post since it affects construction of the circuit but its return value is of type () $pre @public. Although stage effects can be translated to domain effects via ⟨⋅⟩, we have to keep stage and domain effects separate because in branches of match expressions stage effects are suppressed whereas domain effects have their usual impact. The boolean effects do not relate to domains. Instead, they indicate if all operations needed for evaluating the expression are those allowed in branches of match expressions.

The behaviour of data types in the type rules is standard. The purpose of effects is to propagate knowledge about incumbrances down the proof tree. For instance, the boolean effect ff propagates from any premise to consequences transitively. The transitive propagation is achieved by the greatest lower bound operation (∧) connecting the effects of premises. In stage effects, it follows the stage ordering defined above, and in boolean effects, it means conjunction. In the case of domain effects, it means union of upward closed sets of domains which corresponds to the minimum operation on the underlying generator domains. By pointwise lifting of the greatest lower bound operation to triples, we can express greatest lower bound of effects o₁, o₂ as o₁∧o₂.

Assertions of function typing

Assertions of function typing used in the rules of expression typing are of the form

This assertion states that, in the context of environments Φ,Κ,Π,Σ, the function f is of type w. The function type w can be expanded as q₀ -> … -> q_n−1 -> q ! o ∷ b, telling that the function assumes arguments of types q₀,…,q_n−1, returns a result of type q, and can cause effect o. In addition, the type encodes its vectorizability status as boolean b.

In the rules of function typing, assertions of two more shapes are used:

The first assertion states a function typing if no local group function environment is given by the context. The second assertion assumes a substitution and states a function typing after applying this substitution to all definitions in the local group.

Constraint assertions

We use also constraint assertions of the form

Such assertion means that all constraints c₀,…,c_k−1 are logical consequences of the constraints in set Κ. Deciding the logical implications between constraints is out of scope of this document.

Primitive expressions

Variables, function names

The type of a variable is determined by the variable environment. Looking up a variable has no effect, which is reflected by the topmost in the corresponding order values $pre, ∅ and tt. The same holds for function names but, instead of lookup from variable environment, an assertion of function typing must be used as premise.

Literals

Integer literals and boolean literals have an integer and boolean type, respectively, with any stage and domain. The modulus N can be any positive integer or infinity. In other words, integer and boolean literals are stage, domain and modulus polymorphic. An integer or boolean literal has no domain or boolean effect, but it has an effect stemming from its stage. The latter fact is due to a wire of the circuit being added if the stage is $post.

String literals can only be domain polymorphic because they do not depend on moduli and values on circuit wires are not interpreted as ZK-SecreC strings.

Tuples

Tuple typing is based on component types solely. Constructing a new tuple has no effect other than those caused by computing the components.

Structs

Struct typing is similar to tuple typing but struct field types are associated to field names in the struct environment and must conform to it.

Lists

Like tuples and structs, list structure also does not redound to the circuit, but as the length of the list can be private information, the domain associated to a list type can be other than @public. Nevertheless, ZK-SecreC requires qualified types to be well-structured, and this must be taken into account when typing the empty list.

ZK-SecreC supports three more special syntaxes for constructing lists. These can be rewritten equivalently using other constructs of ZK-SecreC. Therefore we do not provide special type rules for them.

Compound expressions

Operator and function applications

Application of a function to empty argument collection needs special treatment since, technically, there is one argument whose type is the unit type. There are two rules for this case, depending on if the application is full or partial. In the case of full application, the effect in the function type is triggered, whereas in the case of partial application, it remains hibernated in the function type.

In the case of full application of a function to a non-empty argument collection, application to arguments of types specified in the function type results in a value of specified result type and causes an effect specified in the function type, besides the effects that appear during computation of the arguments. Partial application has similar differences as in the case of empty argument collection. Note that the function resulting from a partial application inherits the vectorization status of the original function.

Attention must be given to mutability of the arguments indicated by the keyword ref. For any expression e, let ref^ff(e) denote the expression e itself, whereas let ref^tt(e) denote the expression e preceded by the keyword ref. So the third rule tells that every argument that is going to substitute a parameter declared as mutable must be preceded by the keyword ref, while other arguments must not be preceded by this keyword. For an expression e to be passed as a mutable argument, e must be interpretable as an L-value and the variable through which the piece of memory is accessible must be mutable. This is established by the constraints Γ(mut(var e_i))≥b_i. (In the case var e_i not being well-defined, we consider Γ(mut(var e_i)) as ff.) Partial application of functions with mutable parameters is not allowed.

Vectorized applications

Vectorized application is allowed only if all parameters of the applied function are immutable and there is at least one argument vector to enable determining the length of the vectors involved. The type constraint Vectorization associates to the Iter plugin of Circuit-IR but, if the plugin is not supported, the compiler is able to unroll vectorized operations.

Lookups and slices

Lookups by index in a tuple and lookups by field name in a struct have the corresponding component or field type. No effects other than those caused by computing the tuple or struct are observed. In the case of list and vector lookups, things are more complicated because the index can be expressed as an arbitrary expression rather than a name or literal. The data type of the index must be uint[2⁶⁴] which allows indices to be represented in the 64 bit integer type in Rust. Note that the stage and domain of the index coincides with that of the list or vector. The only effects that can arise are those observed during computing the list and the index.

Besides lookups, lists and vectors also support slice syntax that allows one to denote a segment of a list or vector by specifying its lower and upper bounds. The typing rules are similar to those of list and vector lookups but the result type is the list or vector type rather than the element type. Note that the obvious equivalence e₁[e₂ .. e₃] ≡ let x = e₁; for i in e₂ .. e₃ {x[i]} holds in the case of lists only, because for loops can create lists but not vectors.

There are three more slice syntaxes that enable one to omit either the lower or the higher bound or both. A missing lower bound is interpreted as 0 whereas a missing higher bound is interpreted as the length of the list or vector.

Assignments

An assignment requires both sides to have the same qualified type. Moreover, the left-hand side must be mutable. This is determined by the variable environment which must contain evidence about mutability of the variable in the left-hand side. The value of an assignment belongs to the unit type. However, assignment adds an effect of the stage and the domain of the assigned value to those observed during evaluating the sides of the assignments.

Type annotations

ZK-SecreC strictly requires the types of formal parameters of functions to be explicit. Types of ordinary expressions do not have to be annotated but the programmer is allowed to do it. In this case, the type system requires the given type to be correct, i.e., to be able to be inferred using the typing rules. Type annotations cannot be used for type conversion. Type annotations do not cause additional effects.

The two rules differ by the form of the type (qualified or function type). ZK-SecreC actually allows the programmer to omit one or both qualifiers (which is not reflected in the rules for simplicity). An omitted stage is inferred by the compiler, while an omitted domain in a type annotation is equivalent to being annotated as @public. The same applies to types of formal parameters of functions.

Casts

Type casts can change the modulus of an integer or boolean, reinterpret booleans as integers, and raise a value to a higher stage or domain. Downcasting a value to a lower stage or domain is not possible. In particular, converting a value outside the circuit to a value on wire cannot be done by type cast. Also, casting integers to booleans is not allowed. Casting of domain involves deep cast. Although the function dcast is well-defined regardless of the new domain, the cast is allowed only if the new domain is at least as high as the old one.

Rules for converting between different moduli depend on whether both moduli are finite (N⋅M∈N) or not. Conversion between finite moduli requires the Convertible constraint. Type casts mostly leave the existing effect as it is but changing the modulus is reflected in the boolean effect, i.e., it forces it false.

Statements and expressions with blocks

Statements

In the first rule, ε denotes the empty statement. Non-empty statements can be built up using composition. In the first constituent of composition, one can define a new variable using the keyword let. The definition can be non-recursive or recursive, and a non-recursive definition can define a usual variable or a function name. If the first constituent of composition does not introduce a new variable then it must be of the unit type.

The rules concerning composition come in pairs because the second constituent of the composition can have a qualified type or a function type. The difference between rules in the same pair is purely formal.

In all cases with a new variable definition, the type of the right-hand side of the definition will become the type of the variable in the variable environment (or the type of the new function name if a function is defined) while establishing the type of the rest of the statement. Besides this typing, a mutability statement about the defined variable is added to the variable environment (unless a function is defined). In the second and the third rule, mut^ff x denotes the variable x itself, whereas mut^tt x denotes the variable x preceded by the keyword mut. In the case of a recursive definition which is the subject of the fourth and the fifth rule, typing of the variable must be used in typing of the first constituent of the composition, too. Recursively defined variables are not allowed to be mutable.

In all cases of composition, the only effects are those of the constituents, regardless of the stage and domain of the new variable defined.

Although this is not reflected in the typing rules, ZK-SecreC allows type annotations to be added to the new variables. In this case, the type given explicitly must coincide with the type derived by the rules. One qualifier or both can be omitted and, if so, the usual conventions explained about type annotations above apply. Sometimes, adding a type annotation is mandatory for successful compilation. For instance:

• When a struct with a finalizer is created, the compiler may be unable to find all necessary dependencies unless a type annotation is added;
• When a function is applied vectorized, the type of the result must usually be annotated.

Blocks

Any expression can be turned to a block by putting it into braces. This does not change the type and the effect of the expression.

Lambda expressions

For typing a lambda expression, the type of the body of the lambda expression is found in the environment where a typing of all parameters is added. Parameters of lambda expressions are immutable. Effects of the resulting function are those of the body of the lambda expression. Like for application, typing in the case of empty parameter collection must be given separately.

In the third rule, sieve^b fn means sieve fn if b=tt and just fn if b=ff. Functions declared as sieve are not allowed to be applied partially or to zero arguments, hence it would not make sense to allow the sieve modifier in other rules.

All parameter types and the result type of a function declared as sieve have to satisfy the constraint Sized, i.e., they must be sized types. To express this in the third typing rule, we use the boolean indicating the existence of the sieve modifier as a type constraint. Having the boolean ff there makes the whole implication vacuously true, whereas tt behaves as no-op. Analogously, the last premise of the third rule establishes that if a function has modifier sieve then its type q₀ -> … -> q_n−1 -> q must satisfy atomlub_Σ(q₀ -> … -> q_n−1 -> q)=@public.

The restriction imposed on vectorizability relies on auxiliary function atomlub_Σ while the restriction imposed on actual vectorized application uses the auxiliary function atomstglub_Σ. This implies that some vectorizable functions cannot be directly applied in a vectorized way. This makes sense since vectorizable functions, like other functions, can be applied partially. The result of a partial application of a vectorizable function is still vectorizable. So, for instance, a vectorizable function whose first argument has qualifiers $pre @public and the others are at the stage $post can be used for generating a new vectorizable function by applying it to one argument; the resulting function has all arguments at the stage $post, so it can be applied in a vectorized way.

ZK-SecreC allows the types of parameters of the lambda expression, as well as the result type, to be annotated. This is not reflected in the typing rules. Types given explicitly must coincide with those derived using the type rules. The usual conventions apply to omitted qualifiers.

Conditional expressions

The condition of a conditional expression in ZK-SecreC can be either an ordinary expression of boolean type or a type constraint. Typing rules differ depending on the nature of the condition.

The first typing rule captures the case with an ordinary boolean expression as condition. The boolean type can have a finite or infinite modulus. The condition must be at the stage $pre since the circuit is not able to do branching. The branches of the conditional must have equal qualified types. The type of the branches will become the type of the whole expression. The constraint ⟨d'⟩≤⟨s∧s₂∧s₃⟩∧⟨d⟩∧D₂∧D₃ concisely establishes the following restrictions:

• The domain of the condition must not be higher than the domain of the branches (⟨d'⟩≤⟨d⟩);
• The domain of the condition must not be higher than any domain in the upward closed set of domain effects of both branches (⟨d'⟩≤D₂∧D₃);
• If the branches are at the stage $post, or any of the branches have effects at the stage $post, then the domain of the condition must be @public (⟨d'⟩≤⟨s∧s₂∧s₃⟩).

These are key restrictions for providing the necessary guarantees of preserving privacy. For instance, violating the first restriction would allow the value of the branch chosen to reveal the value of the condition, i.e., leaking of the value of the condition to a lower domain. Likewise, violating the second restriction would allow the value of the condition to leak via effects of the branch chosen. The third restriction is also similar since having the value or the effect of any branch at the stage $post means modifying the circuit which is public.

The second typing rule deals with conditionals that use a type constraint for branching. The type constraint is added to the set of constraints when deriving the type of the first branch; analogously, the negation of the type constraint is added when deriving the type of the second branch. The conditional with a type constraint as condition does not require this kind of restriction since a type constraint does not have a domain. (Also, no branching takes place during run time.) Branching on the constraint Vectorization is not allowed. Since the compiler can handle vectorized operations regardless of the existence of the Iter plugin of Circuit-IR, deciding if Vectorization actually holds or not is not meaningfully possible.

A conditional with else branch omitted is semantically equivalent to a conditional with an empty else branch and otherwise coinciding with the given conditional.

The effects of the conditional are those of computing the condition and both branches.

For loops

The bounds of a for loop in ZK-SecreC must be integers with modulus 2⁶⁴. This design choice was made for enabling the compiler to translate loops using the Rust 64-bit integer type which is faster than integers of arbitrary size. The loop index will obtain the same type and is immutable. The bounds, as well as the loop index, must be at the stage $pre since the circuit has no means of branching or looping. The body of the loop is typed in the environment where the typing of the loop index has been added. The loop itself is of the list type whose element type coincides with the type of the loop body and the stage and domain coincide with those of the bounds. The constraint ⟨d'⟩≤⟨s∧s₃⟩∧⟨d⟩∧D₃ establishes the following restrictions:

• The domain of the bounds must not be higher than the domain of the body (⟨d'⟩≤⟨d⟩);
• The domain of the bounds must not be higher than any domain in the upward closed set of domain effects of the body (⟨d'⟩≤D₃);
• If the body is at the stage $post, or the body has effects at the stage $post, then the domain of the bounds must be @public (⟨d'⟩≤⟨s∧s₃⟩).

The purpose of these restrictions is similar to that of the restrictions in the typing rule of the conditional.

The effects of the for loop are those of computing the bounds and the body of the loop.

Zip expressions

The vectors that generate values for variables in zip expressions must have vector datatypes, i.e., types of the form arr[q] for a qualified type q. All vectors must be at the stage $pre and in the same domain which will become also the domain of the result vector. This restriction does not expand to elements of the vectors; elements of different vectors can have different stages and domains. The variables are included in the environment only for typing the body of the expression. They are not included in the environment when typing the subsequent generator vectors. The variables are immutable.

For using a zip expression, the Vectorization constraint must hold. A zip expression can have effects that arise during computing the generator vectors and the body of the expression.

The following semantic equivalence holds:

Wire expressions

A wire expression can be applied to a block with an integer or a boolean data type at the stage $pre. The result has the same data type and domain but with the stage $post. It requires the Field type predicate to hold on the modulus of the value that is written on wire.

While a wire expression does not create new domain effects, it has an effect at the stage $post and, if being used in the domain @verifier, it forces the boolean effect to false. The latter is because verifier inputs of the circuit are not allowed in the branches of match expressions.

Match expressions

Match expressions enable branching according to an integer value on wire. Such branching is based on the oblivious choice feature implemented in the Disjunction plugin of Circuit-IR. In the left-hand sides of the cases, ZK-SecreC allows patterns that can be literals, variables or underscores. Variables used as patterns can be referred to in the corresponding right-hand side, where they are immutable and their type equals that of the expression matched. An underscore means wildcard pattern that matches any value but does not enable referring to it in the right-hand side. The pattern typing and the corresponding mutability statement are added to the environment but they are usable only if the pattern is a variable.

There are three restrictions a match expression must satisfy. The first one states a match expression being valid only if the ObliviousChoice type constraint holds. This type constraint is associated to the availability of the Disjunction plugin of the Circuit-IR. The second restriction, ⟨d⟩≤⟨d'⟩∧D₀∧…∧D_n−1, resembles the analogous constraints in the typing rules for conditionals and for loops but involves only domain effects. The issues addressed by the constraints imposed on stage effects in the other rules are here handled by the Disjunction plugin. The third restriction, b₀∧…∧b_n−1=tt, states that the right-hand sides must not produce false boolean effects.

Match expressions do not cause effects other than those caused by computing the matched expression and the right-hand sides of the cases.

Function typing

When describing function typing, we assume that the program is divided into groups of mutually recursive functions. Typing of these groups is given separately.

General function typing

These rules establish two ways of deriving a function typing of the form Κ,Φ,Π,Σ ⊢ f : w used above: Reading from the current local group function environment, and deriving from the global function and struct definitions. If a function within the same group of mutually recursive functions or a locally defined function is called then the type must be read from the environment, otherwise it must be derived in place.

Typing of functions outside the local group

The only rule here establishes that, for deriving the type of a function at the global level, one must type all functions within its group of mutual recursive functions. More precisely, it states that in a program with given struct type definitions, a function can be given a specific type, provided that there exists a substitution ρ after applying of which this function can be typed with this type within its group of mutually recursive functions. Involving an arbitrary substitution allows a function to be given different monomorphic types in different cases.

Note the occurrence of typings of the members of the group of mutually recursive functions also in the premises. The function typings in the left-hand side are to be used for typing recursive calls in function bodies. The typing assertions do not become trivial because there is no rule that would allow the function typings in the left-hand side to be used for deducing the function types in the right-hand side directly. The first rule of the previous subsubsection does not apply as its conclusion has a different shape. Assertions of this form can be derived only using the rule described in the next subsubsection.

Mutually recursive functions

The first two typing rules capture the cases with an empty collection of parameters, whereas the last two rules deal with cases with at least one parameter. Furthermore, the typing rule depends on whether the result type given in the function definition is a qualified type or a function type. In all cases, typing of functions within its group of mutually recursive functions depends on a substitution ρ of monomorphic types for type variables. We assume that every function uses unique type variables. All rules specify that if a substitution is applied to the argument types, the return type and the constraints of the function, and the body can be typed with the resulting return type when the variable environment consists of the resulting typing of parameters and the resulting constraints are valid, then the function can be typed with the resulting function type.

The constraints obtained by applying the substitution to those in the original type of the function must be implied by the constraint set Κ. Although the constraints do not contain variables, they are not always resolvable without relying on external information such as a number being a supported field size. Such information must be given in Κ. The type system is not going to search it from outside resources.

In the third rule, the same restrictions and conventions apply as in the case of nameless (lambda) sieve functions.