Lurk Circuit Specification

$\global\def\var#1{\footnotesize{\textsf{#1}}}$ $\global\def\gad#1{\footnotesize{\textsf{#1}}}$ $\global\def\fun#1{\footnotesize{\textsf{#1}}}$ $\global\def\cir#1{\footnotesize{\text{#1}}}$ $\global\def\cirtitle#1{\footnotesize{\bold{#1}}~}$ $\global\def\cirio#1{\footnotesize{\bold{#1}}~}$ $\global\def\com#1{\footnotesize{\text{#1}}~}$

$\bf{Disclaimer}$: This spec is a work in progress. It is an ongoing project and will continue to be refined over time. Questions about the circuit can be posed in the Lurk Zulip server.

Introduction

Zero-Knowledge Proofs ¹ are cryptographic primitives that allow some entity (the prover) to prove to another party (the verifier) the validity of some statement or relation. Today there are many efficient constructions of NIZK proof systems, with different trade-offs, as well as several implementations of the proving systems.

Every proving system, as described in the zk-Interface ², can be divided into the backend, which is the portion of the software that contains the implementation of the underlying cryptographic protocol, and the frontend, which provides means to express statements in a convenient language, allowing to prove such statements in zero knowledge by compiling them into a low-level representation.

The backend of a proving system consists of the key generation, proving and verification algorithms. It proves statements where the instance and witness are expressed as variable assignments, and relations are expressed via low-level languages. The most common instance of such a low-level language is R1CS, a generalization of arithmetic circuits, introduced in ³ and used in many other proof systems (see ⁴, ⁵, ⁶, ⁷ among others).

Lurk is a proving frontend which accepts high-level statements written in the form of a Lisp dialect, and produces a low-level proof representation thereof specifically tailored to work well with a certain class of proving backends. Indeed, Lurk produces proof statements shaped as chained but distinct iterations of a single abstract state machine⁸ represented in R1CS. As the components of the low-level proof statement only differ in their assignment of inputs and outputs, Lurk’s outputs are particularly well suited to cryptographic backends that support recursion, or more generally proof aggregation. As an implementation, Lurk currently focuses on producing statements in R1CS, and supports two backends: Nova ⁹ and SnarkPack ¹⁰.

The Lurk frontend consists of the following:

• The specification of a high-level language for expressing statements.
• A compiler that converts relations expressed in the high-level language into the low-level relations suitable for some backends. This leverages a library of “gadgets” consisting of useful and hand-optimized building blocks for certain primitive statements.
• Instance reduction: conversion of the instance in a high-level statement to a low-level instance
• Witness reduction: conversion of the witness to a high-level statement to a lowlevel witness (e.g., assignment to witness variables).

Lurk decomposes relations expressed in its Lisp-like source language into iterations of an abstract state machine (ASM), which implements a deterministic interpreter for this language. The workings of the step function of this state machine is detailed in the reduction section below.

At a high level, Lurk’s ASM manages four constructs:

• a library of R1CS gadgets, which allow translating primitive blocks of the source language directly into arithmetic sub-circuits,
• a continuation stack, that allows deferring the evaluation of sub-parts of the current program, or upacking deferred part of the computation in the translation of the currently-selected portion of the AST is finished,
• a reduction strategy, that allows selecting sub-parts of the input AST for evaluation deterministically,
• a strict hashing discipline for Lurk programs, which allows the prover to memoize the translation of portions of the input program, while producing cryptographic hashes that bind the prover to a specific source program.

This step function proceeds repeatedly until the input program is fully evaluated.

Lurk

Lurk is a functional programming language based on Scheme and Common Lisp. An important aspect of its design is Continuation Passing Style (CPS)¹¹, where the control flow of programs can be managed through the use of continuations. Continuations are recursive data structures that can be used as part of a representation of generic computations. In particular, for each basic operation in a certain computation, a continuation is used as a pointer to the rest of the computation, i.e. it indicates what must happen after this basic operation is computed. Concretely, it takes the form of a stack of continuations that we will describe in greater detail later on. This technique allows us to divide a program into small parts and build a small circuit for each part. We will summarize the main concepts involved in the design of the language, which should enable the reader to understand how zero-knowledge proofs ^{7 9 12} are constructed in Lurk.

In this section, we provide a summary of Lurk’s main elements. An expression represents a computation involving literals, variables, operations and procedures. Variables are handled by an environment , which is responsible for binding variables to values. We also use continuations to indicate what must be done to finish the computation.

The system’s I/O is formed by an expression, an environment, and a continuation. Understanding these 3 elements is essential to comprehending Lurk. Each element is represented as a pointer, which is implemented using hash functions. In particular, we use Poseidon ¹³ to instantiate our pointers.

The environment has a list of bindings, which correspond to a mapping between variables and values at a certain point in time. The mapping of these local bindings is valid only for a specific evaluation of an expression. On the other hand, the global state is represented by the store, which behaves as a memory of the system. The store is global, while the environment is local.

Language overview

• t, nil: are self-evaluating and represent true and false, respectively.
• if: has the format (<test> <consequent> <alternate>) and represents a conditional expression. It must receive all 3 parameters, where the <test> is an expression used to select the result; the <consequent> is selected if the <test> evaluat es to non-nil; and <alternate> is selected otherwise. Unlike other programming languages, the <alternate> expression is mandatory.
• lambda: has the format (lambda <formals> <body>) and represents a procedure. The environment when the lambda expression is evaluated is used as a closure, which is extended with <formals>, a list of variables. The unique expression in the <body> is evaluated and returned as the result of the lambda expression.
• let: has the format (let <bindings> <body>) and represents an assignment expression, where <bindings> represents a list of pairs in the form (<variable>, <init>); and <body> is a unique expression.
• letrec: has the same format as <let> expressions, following the same rules, but also allowing recursion.
• quote: has the format (quote <datum>) or (’ <datum>) and evaluates to <datum>.
• atom: has the format (atom <e>), and it evaluates to t if <e> is not a list, and evaluates to nil otherwise.
• cons, strcons car, cdr: The expression (cons <a> <d>) produces a pair whose car is <a> and cdr is <d>. When <a> evaluates to a character and <d> evaluates to a string, we have that strcons <a> <d> produces to a string. In this situation we have that car <e> returns the first character when <e> is a string. Correspondingly, cdr <e> returns a string obtained from removing the first character from <e>.
• arithmetic operations: has the format (<op> <e1> <e2>), where <op> corresponds to an arithmetic operation (+, -, *, /). <e1> is evaluated before <e2> and the operation is carried out in the finite field that is used in the subjacent zero-knowledge backend.
• equality: has the format (<op> <e1> <e2>), where <op> can be either = or eq. The equality symbol = is used to compare expressions whose result is a number (finite field elements), while the symbol eq is used to compare pointers.
• emit: has the format (emit <e>) and is used to return the result of the evaluation of <e> as a public value, which can be used to define the instance of the zero-knowledge statement.
• begin: has the format (begin <e> ...). The sequence of expressions is evaluated from left to right and the last result is returned.
• current env: returns the current environment represented as an association list.
• eval: has the format (eval <exp>) or (eval <exp> <env>). The evaluation of <exp> is used as an expression in the environment obtained from the evaluation of <env>. If no <env> is provided, an empty environment is used.
• hide: has the format (hide <exp> <secret>). Return the commitment of <exp> using secret <secret>.
• commit: has the the format (commit <exp>). Compute the commitment of <exp>.
• secret: has the format (secret <comm>). Return the secret used to generate the commitment <comm>, if known.
• open: has the format (open <comm>). Return the value used to generate the commitment <comm>, if known.
• comm: has the format (comm <data>). Change the tag of <data> to comm.
• num: has the format (num <data>). Change the tag of <data> to num.
• char: has the format (char <data>). Change the tag of <data> to <char>.
• u64: has the format (u64 <num>). Coerce <num> to be a 64-bit unsigned integer.

Fibonacci example

Here is an example code snippet that implements the Fibonacci sequence. You can click the $\small\blacktriangleright$ button to display the output.

(letrec ((next (lambda (a b n target) (if (eq n
        target)
             a
                   (next b
                   (+ a b)
                   (+ 1 n)
                        target))))
               (fib (next 0 1 0)))
        (fib 10))

Iterations: 521
Result: 55

$$\rm{\small{Figure~1: Fibonacci~example}}$$

Circuit overview

In this section, we give a short description of Lurk’s circuit. Important concepts are introduced to help the reader better understand the purpose of certain components and how they interface with each other.

High-level description

A Lurk program consists of a sequence of reduction steps, or iterations, which are mapped to frames. A set of frames is grouped into a MultiFrame object. Each frame is represented by a CircuitFrame and a Circuit is a sequence of CircuitFrames where the output of one frame is connected to the input of the next, mimicking the evaluation of Lurk expressions. For instance, in the Fibonacci example above, we have 521 iterations, each one mapped into a frame.

In eval.rs, the function reduce_with_witness() computes reduction steps with their witnesses. We provide an implementation of this computation in the circuit using the functions $\cir{Reduce-expression}()$ and $\cir{Apply-Continuation}()$ in the file circuit_frame.rs. Global symbols are pre-computed Lurk symbols that can be easily compared with symbols found during expression evaluation.

To reduce an expression, we distinguish between two cases: atoms, such as symbols, and lists, which are more complicated expressions composed of an operation in the first position and other elements that can be atoms or nested lists. In $\cir{Reduce-Sym}()$, we reduce symbols using comparisons among symbols that require allocation of variables and pointers in the circuit, Boolean logic, and conditionals. For example, $\cir{Reduce-Sym}()$ is used to find the value of a variable. We update the environment and the store accordingly.

The cons function is a crucial building block in functional languages like Lurk. It concatenates car and cdr, allowing us to break down expressions into smaller pieces. In $\cir{Reduce-Cons}()$, we handle each possible Lurk expression that is constructed using cons. We allocate auxiliary variables in the circuit for later use and use a $\gad{CAR-CDR-NAMED}()$ gadget as a building block. We include a clause in a multicase gadget for each situation depending on the type of expression we are handling, and select the desired result based on the head of the expression using car. Finally, we return the result of the multicase.

Another important function is $\cir{Apply-Continuation}()$. In order to finish a reduction step, we must calculate the output of the frame. Each iteration has a continuation tag that requires a computation of the next expression, environment, continuation, and thunk. Therefore, we have to constrain the system to prove we are computing the correct elements, and we have to allocate pointers to use them later. This task is executed in 2 stages:

1. Some continuations require the calculation of new pointers, while others don’t. For those that need new pointers, since the implementation of pointers requires a hash computation and because hashes are expensive in the circuit, we use a multicase to select the appropriate hash preimage. Then we can compute the hashes just once. This allows us to avoid computing unnecessary hashes.
2. We then use another multicase to select the continuation results.

Gadgets

To construct the circuit, we use gadgets and auxiliary functions as building blocks. These gadgets are fragments of emitted code generated by the Lurk compiler, which represent the translation of primitive operations of the Lurk language into the low-level language accepted by cryptographic proof backends. Each gadget incorporates constraints that convey the semantics of the source language in the low-level language of arithmetic circuits. For instance, when we interpret an expression like $a + b$, the emitted gadget not only computes the addition but also takes into account the max values of $a$ and $b$ when interpreted as u64, along with the overflow semantics of their sum - even when the gadget manipulates primitive addition operations on 256-bit numbers.

Gadgets are denoted in all caps, and composition of gadgets is shown using a dark gray color. Full details of the gadgets, such as the number of constraints of each component and their implementation description, will be provided in the Low-level description section.

• Variable types: In the circuit we allow variable to have the following types:

1. AllocatedNum: represents a field element in the circuit.
2. AllocatedPtr: represents a pointer in the circuit, which is given by 2 AllocatedNums, denoted by $\var{tag}()$ and $\var{hash}()$ respectively.
3. AllocatedContPtr: represents a continuation pointer in the circuit. Silimilarly to AllocatedPtr, it is formed by 2 AllocatedNums.
4. Boolean: represents a bool in the circuit. It can be used both for allocated values or as constants. In the case it represents an allocated value, this value is enforced to be 0 or 1.

Some gadgets, such as $\gad{NOT}$, refer to other circuits - in this case the Boolean variable being negated. This reflects that arithmetic circuits have input and output variables, and can therefore be connected to each other. In this case, the circuit for $\gad{NOT}$ will have its input wired to the output of the circuit generating the Boolean variable passed as its argument.

• Syntax :

  • Let: creates a variable in the circuit.

  • Call: allocate a gadget inside a circuit, used when gadgets have no return values.

  • Return: defines the output of a circuit.

  • We use dot notation to access global variables:

    1. Let $\var{symbol-tag} = \var{globals.sym-tag}$.

  • We use dot notation to access gadget’s helper methods:

    1. Let $m = \gad{CASE-CLAUSES}()$.
    2. Call $m.\gad{ADD-CLAUSE}(k, c)$.

  • Tuples and vectors: syntactic sugar to manipulate circuit variables.

• Boolean operations: used to handle bit operations like conjunctions, disjunctions, negations, and bit decomposition.

  1. Let $o = \gad{AND}(i_1, i_2, \dots)$: Receives a variadic number of input variables of type Boolean and returns another Boolean representing the conjunction of the input variables.
  2. Let $o = \gad{OR}(i_1, i_2, \dots)$: Receives a variadic number of input variables of type Boolean and returns another Boolean representing the disjunction of the input variables.
  3. Let $\var{negated-b} = b.\gad{NOT}()$: Every variable $b$ of type Boolean has an auxiliary method called NOT, which receives no input and returns another Boolean representing the negation of $b$.

• Equality: allows equality tests of allocated variables.

  1. Let $\var{is-equal} = \gad{ALLOC-EQUAL}(a, b)$: The Boolean variable $\var{is-equal}$ is true if and only if $a$ is equal to $b$.
  2. $\gad{EQUAL}(a, b)$: enforces $a$ equal to $b$.
  3. Let $\var{is-zero} = \gad{ALLOC-IS-ZERO}(a)$: The Boolean variable $\var{is-zero}$ is true if and only if $a$ is zero.

• Pick: used for ternary operators.

  1. Let $a = \gad{PICK}(\var{cond}, a, b)$: If $\var{cond}$ is true, return $a$, otherwise return $b$.

• Implication: used for constraints in the form: if $\small{a}$ is true, then $\small{b}$ is true, where $\small{a}$ and $\small{b}$ are expressions that evaluate to Boolean values.

  1. Call $\gad{IMPLIES-EQUAL}(\var{cond}, a, b)$: If $\var{cond}$ is true, then $a$ is enforced to be equal to $b$.

• Arithmetic operations: used to constrain arithmetic operations $\rm{\footnotesize{(+,~-,~*,~/)}}$ in the subjacent finite field.

  1. Let $c = \gad{SUM}(a, b)$: $c$ is enforced to be $a + b$.
  2. Let $c = \gad{SUB}(a, b)$: $c$ is enforced to be $a - b$.
  3. Let $c = \gad{MUL}(a, b)$: $c$ is enforced to be $a . b$.
  4. Let $c = \gad{DIV}(a, b)$: $c$ is enforced to be $a . b^{-1}$.

• Pointers: formed by a tag, which allows us to identify the type of the pointer, and a hash that links the pointer to its content, which is given by the hash preimage.

  1. Let $a = \gad{ALLOC-PTR}(\var{pointer})$: Allocates a pointer in the circuit.

• Data: functions can allocate different types of data by using pointers. Later, data can be accessed non-deterministically by providing the witness that corresponds to the hash preimage.

  1. Let $\var{hash} = \gad{CONSTRUCT-CONS}(\var{car}, \var{cdr})$: Computes a hash function over $\var{car}$ and $\var{cdr}$.
  2. Let $\var{hash} = \gad{CONSTRUCT-FUN}(\var{args}, \var{body}, \var{env})$: Computes a hash function over $\var{args}$, $\var{body}$ and $\var{env}$.
  3. Let $\var{hash} = \gad{CONSTRUCT-LIST}(\var{args}[])$: Computes a hash function over args by using a sequence of cons.
  4. Let $\var{hash} = \gad{CONSTRUCT}(\var{comp1}, \var{comp2}, \var{comp3}, \var{comp4})$: computes a hash function over $\var{comp1}, \var{comp2}, \var{comp3}, \var{comp4}$.

• Multicase: used to select results based on certain selection tags. It is basically a set of cases that share the same set of selection tags. A multicase whose size is equal to 1 is the same as a regular case.

  1. Let $\var{case-clauses} = \gad{CASE-CLAUSES}()$: a list of clauses for a $\gad{CASE}$ gadget.
  2. Let $\var{result} = \gad{CASE}(\var{key}, \var{clauses}, \var{default})$: the result of using key to select a value from clauses. If no clause is found, return default.
  3. Let $\var{multicase-clauses} = \gad{MULTICASE-CLAUSES}()$: A list of clauses for a $\gad{MULTICASE}$ gadget.
  4. Let $\var{result} = \gad{MULTICASE}(\var{key}, \var{clauses}, \var{default})$: the result of using key to select a value from clauses. If no clause is found, return default.

Auxiliary circuits:

• Comparisons: computes the comparison of allocated variables.
• Enforce n bits: Enforce a certain allocated number can be represented using $n$ bits.

Circuit specification

This section describes the Lurk circuit in detail. We present the high-level algorithms first to help readers understand our architectural decisions, become familiar with the notation, and comprehend how components are interconnected. We then provide the low-level algorithms, which explain how we construct R1CS constraints for each building block in this document.

Backends

Currently, we support two backends: Groth16 ⁷ and Nova ⁹. Both are based on R1CS constraints, enabling us to create a single circuit that works with both backends. However, there is an essential difference between the two. Groth16 requires a trusted setup for each circuit, which we want to avoid since updating the circuit would require another ceremony for the new trusted setup. Conversely, Nova doesn’t need a trusted setup. Moreover, Nova allows recursive composition of proofs, making it a practical and exciting alternative. In particular, it fits well into the Lurk circuit since we can fold Lurk frames using Nova’s folding technique. Regrettably, recursive composition is beyond the scope of this document.

From the application layer perspective, the only difference between these systems is the underlying finite field. Specifically, it means that programs like $\rm{\footnotesize{(- 1 ~0)}}$ evaluate to different numbers in each case.

Next we summarize the main characteristics of each system:

• Groth16 ⁷ is implemented over the BLS12-381 elliptic curve. The subjacent Finite Field for Lurk applications is defined over the following prime: 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001
• Nova ⁹ is based on the cycle of elliptic curves named Pallas and Vesta ¹⁴. The underlying Finite Field is defined over the following prime: 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001

Lurk data are constructed using finite field elements. In subsequent sections we show how other data types are represented using these elements.

We denote the finite field by F in order to provide an homogeneous description of Lurk circuits, but it is important to note that, depending on the chosen backend, a different prime is used, which may lead to distinct behavior in some situations (as, for example, when modular reductions are involved).

Main concepts

Here we describe how Lurk evaluation works. Later we will show how the circuit implements the same components.

A Lurk expression is evaluated step-by-step by applying a reduction method. The next step to be applied is called a continuation. In this next example we see how a simple program is evaluated.

> (atom 42)
INFO lurk::eval > Frame: 0 Expr: (ATOM 42)
Env: NIL
Cont: Outermost

INFO lurk::eval > Frame: 1 Expr: 42
Env: NIL
Cont: Unop{ operator: Atom, continuation: Outermost }

INFO lurk::eval > Frame: 2 Expr: T
Env: NIL
Cont: Terminal

[2 iterations] => T

$$\rm{\small{Figure~2: Atom~example}}$$

The evaluation process begins by identifying the atom operation. Once the operation is detected, we can create a corresponding continuation, called unop, which is short for unary operation. In the second step, we evaluate the unique operand, the number 42, which results in itself. Next, we apply the atom operation to 42 and obtain the symbol T.

The continuation for the atom operation requires only one expression as input, which in this case is the number 42. We then need to find a way to return this to the caller, which is Frame 0. After this step, we can return the result of evaluating atom over 42, which is T, and terminate the computation since it is the outermost continuation.

The unary operator follows a specific structure, consisting of the operator and the continuation, which is represented as Lurk data by finite field elements. The continuation is represented by a tag and a pointer. To look up the pointer content, we use dictionaries, which are hash maps used to store data in a content-addressable way. A hash function is calculated over the content to generate an index, which is used to address the data efficiently. It is important to note that we do not use dictionaries in the circuit. Instead, we provide the witness that corresponds to the hash preimage and the result non-deterministically. Therefore, we do not need to look up any table to find the result since the result is already there.

Pointers

A pointer consists of two field elements: a tag and a raw pointer. The tag serves the purpose of distinguishing between different types of pointers, which is important because each tag corresponds to a distinct data structure behind the pointer. The content of the pointer has a structure that varies according to its type, and this type can be determined by the tag. The raw pointer is a dictionary index that can be used to efficiently access the content. Pointers are versatile and can be used to store Lurk expressions, allowing for the expression of recursive expressions. Additionally, pointers can be used to represent the environment, as described in the Environment Section.

A continuation pointer, denoted by $\rm{\footnotesize{cont}}$, is also defined as 2 field elements: a continuation tag and a raw pointer. It works in the same way as regular pointers, but it is restricted to continuations. While this differentiation is not necessary, it enhances the design organization by separating components based on their functionality. If we want continuations to be first class, we would have to treat them like regular pointers.

A raw pointer is a 32-bit integer (encoded naturally as a field element) that represents an index in some of the dictionaries managed by the store. This enables efficient recovery of the pointer’s content. If the raw pointer is negative, it encodes an opaque pointer, which implies that the store is not aware of it.

Expressions

Expressions are recursive data structures containing nested operations involving literal values, variables, and operations. It can represent arithmetic expressions like $\rm{\footnotesize{(+~10~32)}}$, or lambda expressions such as $\rm{\footnotesize{(lambda~(x)~x)}}$. An anonymous function that returns the received input argument. Here is a list of Lurk expressions:

• nil. The nil symbol is a self-evaluating expression. Since it is used frequently, we have a global pointer to represent it.
• cons(pointer, pointer). A cons expression receives two input arguments, which are given by generic pointers. Both expressions are concatenated, forming a new list, which is inserted into the store.
• comm(F, pointer). A comm operation receives as input a secret value, represented as a field element, and a second expression, which represents the content of the commitment. The output is a pointer to a field element, which is the commitment using Poseidon hash.
• sym(string). A Lurk symbol is given by a string, which may be either a restricted Lurk symbol like cons, car, cdr, if, or let, or a new symbol, defined using let or letrec. It could also be a local symbol, as, for example, in arguments of lambda expressions.
• fun(pointer, pointer, pointer). Each pointer represents the arguments, the body, and the closed environment, respectively.
• num(F). A num expression is represented by a field element, and the output is a pointer to it.
• str(string). A string expression is represented as a list of char, recursively interpreted as a cons(char, string), where the first element is some char, and the rest of the string is another string.
• thunk(pointer, cont). A thunk expression contains a pointer to an expression that must be evaluated before calling the continuation, which is the second argument. It is an important building block for constructing special continuations like tail, outermost, terminal, and error continuations.
• opaque(pointer). LurkIt allows for opaque pointers, where the content of the pointer is not known by the store. Such pointers can’t be resolved, and they are useful for manipulation of private data (for example).
• char(char). A char expression is represented by a char type, which is encoded as a field element naturally.

Figure 5 shows the tree structure of Lurk expressions.

Continuations

Continuations are data structures containing all the information necessary to continue some computation. Different continuations require different information. Two important continuations are unop and binop, which respectively denote the continuation for unary and binary operations. In order to evaluate the second argument of a binop we require a binop2 continuation.

• outermost. It is the continuation that points to the initial frame.
• call₀(cont). It is represented by a continuation pointer that contains the function to be called.
• call(pointer, pointer, cont), where the first argument corresponds to the unevaled argument, the second is the saved environment, and the third is the continuation. It creates a $\rm{\footnotesize{call\_2}}$ continuation that will be able to evaluate the argument and finish the call procedure.
• call₂(pointer, pointer, cont), where the first argument corresponds to the function to be called, the second is the saved environment, and the third is the continuation. It creates a tail continuation, which will evaluate the body of the function.
• tail(pointer, cont). A tail continuation allows nested tails that may be constructed after evaluation of recursive operations to be compressed down to a single step that returns the expected continuation, returning a thunk.
• cont-error. This represents the continuation after some error happened. It is equivalent to a terminal continuation, because if Lurk finds an error, then a cont-error is returned as the output of the Lurk program evaluation.
• lookup(pointer, cont). This continuation is responsible for doing lookups in the environment, returning a thunk.
• unop(operator, cont). The unary operator continuation doesn’t have an unevaluated argument, therefore it can be executed in a single step, returning a thunk.
• binop(operator, pointer, pointer, cont). This is the first step of a binary operator, where the unevaluated argument pointer is used to construct a $\rm{\footnotesize{binop2}}$ continuation.
• binop2(operator, pointer, cont). The second step of the binary operator can finish the work returning a thunk.
• if(pointer, cont). This continuation is used to select which unevaluated expression will be returned to be evaluated next, according to the conditional expression that is currently being evaluated.
• let(pointer, pointer, pointer, cont). The first argument represents a variable, the second is the body, the third is the saved environment, while the fourth is the continuation. We have that the continuation of a let expression is to extend the environment with the variable and return the body.
• letrec(pointer, pointer, pointer, cont). Similarly to let, but allowing recursion.
• dummy. A dummy continuation is useful for maintaining some invariants in the design, allowing us to control the call of the apply-continuation algorithm.
• terminal. It is the final continuation of a successful Lurk program evaluation.
• emit(pointer). This continuation is useful for creating intermediary publicly visible output of Lurk evaluations.

In the below Figures, we show the DAG structure of Lurk continuations. For each specific point in time, this DAG is just a stack of continuations, starting with the outermost continuation (see left part of Figure 6), growing and reducing the stack accordingly as we reduce expressions. As an example, we evaluate $\rm{\footnotesize{\lparen+~\lparen*~4~5\rparen~\lparen*~11~2\rparen\rparen}}$.

$$\rm{\small{Figure~6: Reduction~step~1}}$$

$$\rm{\small{Figure~7: Reduction~step~2}}$$

After we compute one reduction step over the input expression, we find a + operator at the head of the expression, which is one among many possible binary operations supported by Lurk. In order to evaluate the two input arguments of this binary operation, we need to create two continuations, respectively binop and binop2, saving context data to allow the calculation and saving the previous continuation to be able to return the control flow to the expected place.

The first step is to create a binop continuation, as shown in Figure 7, saving the second argument, which is not yet evaluated, such that we evaluate it in the next reduction step.

Because the first argument itself is the binary operation $\rm{\footnotesize{\lparen*~4~5\rparen}}$ (see Figure 7), we need to repeat the same logic again, creating a new binop continuation in the stack, saving the second expression, as before.

$$\rm{\small{Figure~8: Reduction~step~3}}$$

$$\rm{\small{Figure~9: Reduction~step~4}}$$

$$\rm{\small{Figure~10: Reduction~step~5}}$$

Now we have reached a point where the first argument of the binary operation is a self-evaluated expression: the number 4. We can then proceed by applying the continuation, which is responsible for removing itself from the continuation stack. I.e. the leaf binop continuation is removed and replaced with a binop2 continuation that will be applied when the second argument is evaluated. As a result, a thunk containing the evaluations of both arguments is created, such that the binary operation can finally be applied. We then return the control flow to the saved continuation, which is represented here as the previous continuation in the stack.

Since the result of the binary operation is the number 20, which is a self-evaluated expression, we can apply the continuation of the addition expression, creating a corresponding binop2.

Now we evaluate both input arguments of the first multiplication, producing a thunk containing all the information we need to proceed. For instance, we create a binop2 continuation containing the result 20.

$$\rm{\small{Figure~11: Reduction~step~6}}$$

$$\rm{\small{Figure~12: Reduction~step~7}}$$

$$\rm{\small{Figure~13: Reduction~step~8}}$$

Similarly, we evaluate the second multiplication following the same steps. Next, we evaluate the number 2, which is the first argument, and save the number 11 for the next reduction step.

Next, we evaluate the number 11, the second argument, and create a thunk to finish the calculation.

The thunk returns 42 as the result of the addition of 20 and 22 to the previous continuation, which is the outermost continuation. Therefore we simply replace it by the terminal continuation and finish the execution.

Environment

The environment is a data structure that contains pairs of variables and values, such that the variables of Lurk expressions can be evaluated. This simply means that variables are replaced by their values.

Next we show a LET expression, which allows us to create variables in the environment. Briefly, a LET expression receives as input argument a list of pairs (variable, value), and a body, which is an expression that will be evaluated right after the list of variables is inserted into the environment.

$$\rm{\small{Figure~14: Reduction~step~9}}$$

> (let ((a 1)) a)
 INFO  lurk::eval > Frame: 0
  Expr: (LET ((A 1)) A)
  Env: NIL
Cont: Outermost
 INFO  lurk::eval > Frame: 1
Expr: 1
Env: NIL
Cont: Let{ var: A, body: A, saved_env: NIL, continuation: Outermost }
 INFO  lurk::eval > Frame: 2
Expr: A
Env: ((A . 1))
Cont: Tail{ saved_env: NIL, continuation: Outermost }
 INFO  lurk::eval > Frame: 3
Expr: 1
Env: NIL
Cont: Terminal
[3 iterations] => 1

$$\rm{\small{Figure~15: LET~example}}$$

Store implementation

In this section, we explain how the store is implemented in Lurk. Although the store is not essential to constructing the circuit, understanding its implementation is useful because the circuit must have components that behave equivalently. We replace the store implementation with corresponding mechanisms in the circuit to preserve the same properties. It is important to note that the underlying hash functions used in the store and the circuit are completely different, and there is no connection between the hash maps used in the store implementation and the use of Poseidon in the circuit.

The store is a set of pointers that uses hash maps to implement content-addressable storage. These maps allow us to insert pointers in the set in constant time. A distinct set is created for each pointer tag, including continuation pointers. When a new pointer is created, its content is inserted into the set, and an index is generated. This index is used as a raw pointer, which is useful for accessing the content later.

The following are the sets defined in the Lurk store: cons, comm, fun, sym, num, str, thunk, call, call, call2, tail, lookup, unop, binop, binop2, if, let, letrec, and emit. The store provides a convenient interface to create and access its content, such as the get and intern functions for each set.

An opaque pointer has a negative raw pointer, therefore it can’t be used as an index in the store. Hence such pointers do not have known content.

How to implement the store in the circuit:

Instead of using hash maps, the circuit uses non-determinism to construct cryptographic hash relations in the form y = H(x), where before starting the construction of the circuit, the prover already knows both the preimage, x, and the result, y, of the hash function. In the circuit, the prover shows all the intermediate steps necessary to calculate y from x. Hence, Lurk objects are represented as a Merkle-DAG, where arrows are constructed using this one-way hash function. To show that a certain path in the Merkle-DAG is valid, we non-deterministically provide the sequence of hash relations that corresponds to the needed witness (instead of indexing the hash maps, as we did in the store implementation). The prover can still use the hash map to efficiently build the witness, but from the perspective of the verifier, there is no store.

Note In the context of zero-knowledge proofs, non-determinism refers to the use of non-deterministic auxiliary inputs to improve the efficiency of the verification process. While computing the value of a function can be computationally expensive, verifying whether an already computed answer is correct is typically less costly. Provers can use non-deterministic auxiliary inputs to provide additional information, but high-level programs that compute the answer often lack this information. The benefits of non-determinism can be illustrated with the example of deciding whether two n-element lists are sorted copies of each other. For more on non-determinism, see ¹⁵

Poseidon

Poseidon ¹³ is a hash function tailored for zero-knowledge proofs. Its input is a list of finite field elements, with the output given as a single field element. It is designed in a modular way, being appropriate in different scenarios, from Fiat-Shamir implementation to authenticated encryption ¹⁶.

Here we use it as a hash function to construct pointers, allowing us to have not only content addressable storage, but also a clean solution for recursion, since pointers can be used to represent expressions that contain other expressions in a natural way.

Poseidon circuit

Neptune ¹⁷ is a rust implementation of Poseidon, which allows efficient proof construction. In particular, the total number of constraints is 286 for the 4-ary instantiation, 334 for the 6-ary instantiation, and 385 for the 8-ary instantiation

Pointers in the circuit

While pointers are implemented outside the circuit using dictionaries, we need a different solution for zero-knowledge circuits. One solution is to use hash functions as for example occurs in the construction of Merkle Trees. Poseidon hash function is allegedly a good solution for Lurk pointers, since it can be implemented using a small number of R1CS constraints.

As shown previously, each possible expression or continuation can be represented using at most 8 field elements. Therefore, we designed the system to allow the hash preimage to be formed by at most 4 components, as shown in Figure 17

Next, we describe in detail how we construct pointers in the circuit. In summary, a cons operation requires the 4-ary hash, functions require the 6-ary hash, and generic pointers require 8-ary hash.

• Let $a = \gad{CONSTRUCT}(\var{cont-tag}, \var{components})$:
1. Call $\var{hash} = \gad{POSEIDON}(\var{components})$ - using the 8-ary hash.
2. Return $\var{ALLOC-PTR}(\var{cont-tag}, \var{hash})$.
• Let $\gad{CONSTRUCT-CONS}(\var{car}, \var{cdr})$:
1. Let $\var{hash} = \gad{POSEIDON}(\var{car}, \var{cdr})$, using the 4-ary hash.
2. Return $\gad{ALLOC-PTR}(\var{globals.cons-tag}, \var{hash})$.
• Let $\gad{CONSTRUCT-FUN}(\var{arg}, \var{body}, \var{closed-env})$:
  1. Call $\var{hash} = \gad{POSEIDON}(\var{arg}, \var{body}, \var{closed})$, using the 6-ary hash.
  2. Return $\gad{ALLOC-PTR}(\var{globals.fun-tag}, \var{hash})$.
• Let $\gad{CONSTRUCT-LIST}(\var{elts})$:
1. Let $\var{first} = \var{elts}[0]$.
2. Let $\var{rest-of-elts} = \var{elts}[1.~.~]$.
3. Call $\var{tail} = \gad{CONSTRUCT-LIST}(\var{rest-of-elts})$.
4. Return $\gad{CONSTRUCT-CONS}(\var{first}, \var{tail})$.
• Let $\gad{CONSTRUCT-THUNK}(\var{val}, \var{cont})$:

Error system

Lurk programs can generate error continuations, which indicate an unrecoverable situation. This error is used to finalize the computation. Therefore, it is possible to construct zero-knowledge proofs that a program generated this error. It is important to remark that the error doesn’t carry detailed information to identify the cause of the error. The error can happen for malformed programs, like unary operations that receive more than one argument, or binary operations that receive fewer than two arguments. It can also happen if someone tries to divide by zero. However, the zero-knowledge proofs do not reveal which kind of error occurred.

As an example, when we try to divide by zero, the final output continuation is Error, which is a global pointer used instead of Terminal, such that a verifier can recognize that this program didn’t finish successfully.

> (/ 42 0)
INFO lurk::eval > Frame: 0 Expr: (/ 42 0)
Env: NIL
Cont: Outermost

INFO lurk::eval > Frame: 1 Expr: 42
Env: NIL
Cont: Binop{ operator: Quotient, unevaled_args: (0), saved_env: NIL, continuation: Outermost }

INFO lurk::eval > Frame: 2 Expr: 0
Env: NIL
Cont: Binop2{ operator: Quotient, evaled_arg: 42, continuation: Outermost }

INFO lurk::eval > Frame: 3 Expr: 0
Env: NIL
Cont: Error

$$\rm{\small{Figure~18: Error~example}}$$

High-level algorithms

Now we can start to describe how Lurk programs are translated into R1CS constraints. The strategy is to follow a top-down approach, by first showing some high-level components and saying how they interact. Later we can present the low-level construction of constraints.

Self-evaluated expressions: Some expressions already are in the final stage of evaluation (as, for example, literal expressions like NIL, literal numbers, and characters). The complete list of self-evaluated expressions is given by the following tags: nil, num, fun, char, str, comm.

Unary expressions: As the name suggests, unary expressions correspond to operations that receive only one input argument, which in Lurk are given by expressions that must be evaluated before the unary operation is evaluated.

• atom. It returns $\tt{\footnotesize{true}}$ if and only if the input argument is not a list.
• car. This operation receives as input a list and returns its first element.
• cdr. Complementary to the previous item, it receives a list and returns everything except for the first element.
• emit. This operation emits an intermediary output expression, so that it can be externally viewed.
• commit. Creates a commitment to the received expression.
• open. It is used to open a commitment.
• secret. It returns the secret element used to create a given commitment.
• num. Interprets the finite field element as a number.
• u64. Interprets the finite field element as a 64-bit unsigned integer.
• comm. Interprets the finite field element as a commitment.
• char. Interprets the finite field element as a character.

Below is example of a unary expression evaluation.

> (atom 42)
INFO lurk::eval > Frame: 0 Expr: (ATOM 42)
Env: NIL
Cont: Outermost

INFO lurk::eval > Frame: 1 Expr: 42
Env: NIL
Cont: Unop{ operator: Atom, continuation: Outermost }

INFO lurk::eval > Frame: 2 Expr: T
Env: NIL
Cont: Terminal

$$\rm{\small{Figure~19: Unary~operation~example}}$$

As a first step, a unop continuation is created, pointing to the outermost continuation. Since 42 is a self-evaluated expression, we can continue the evaluation of this continuation, by returning T.

Binary expressions:

• +. Addition of the received elements.
• -. Subtraction of the received elements.
• *. Multiplication of the received elements.
• /. Division of the received elements.
• %. Modular reduction of received elements.
• >. Greater than.
• >=. Greater than or equal.
• >. Less than.
• <=. Less than or equal.
• =. Equality test between numbers.
• eq. Equality test between pointers.
• cons. Creates a list formed by the concatenation of the received elements.
• strcons. Creates a list formed by the concatenation of a char and a string.
• begin. Allows evaluation of multiple expressions, returning the result of the last one.
• hide. Uses the first argument as a secret to create a commitment to the second argument.

Here is an example showing how Lurk evaluates an addition:

> (+ 2 40)
INFO lurk::eval > Frame: 0 Expr: (+ 2 40)
Env: NIL
Cont: Outermost

INFO lurk::eval > Frame: 1 Expr: 2
Env: NIL
Cont: Binop{ operator: Sum, unevaled_args: (40), saved_env: NIL, continuation: Outermost }

INFO lurk::eval > Frame: 2 Expr: 40
Env: NIL
Cont: Binop2{ operator: Sum, evaled_arg: 2, continuation: Outermost }

INFO lurk::eval > Frame: 3 Expr: 42
Env: NIL
Cont: Terminal

[3 iterations] => 42

$$\rm{\small{Figure~20: Binary~operation~example}}$$

The addition expression is reduced by creating a binop continuation containing the second input argument. The first argument is a self-evaluated expression, after which we can create a binop2 continuation, where the second argument will be evaluated, and the sum of both results is returned as a terminal continuation.

Equality expressions: Equality operators are binary operations, therefore we have binop and binop2 continuations.

• =. Used to check equality of numbers.
• eq. Used to check equality of pointers.

Comparison expressions:

• >. Greater than operation.
• >=. Greater than or equal operation.
• <. Less than operation.
• <=. Less than or equal operation.

Conditional expression:

• if. Receives 3 expressions as arguments. If the first one evaluates to something different from nil, then the result is given by the evaluation of the second expression. Otherwise, the result is the evaluation of the third one.

Functional commitments

General work related to functional commitments can be found here ^{18 19 20}. Functional commitments having a function-privacy property, specifically, are described in this paper ²¹. We implement functional commitments as first-class Lurk operations. Specifically, we use cons in order to compute the hash of a function and a secret number. Later, we can prove this function evaluates to determined values. In order to construct functional commitments, we need some building blocks, which Lurk provides natively, and whose high-level description is the following:

• hide(secret, maybe-payload)

1. If there aren't exactly 2 input arguments, return error.
2. Otherwise, compute the commitment using all arguments as input of a 3-ary Poseidon instance.
3. Allocate a pointer to it.
4. Return this pointer.

• commit(payload)

1. If there isn’t exactly 1 input argument, return error.
2. Otherwise, compute the commitment, using zero as the value of the secret.
3. Allocate a pointer to it.
4. Return this pointer.

• open(commitment)

1. If there isn’t exactly 1 input argument, return error.
2. Otherwise, if the commitment is known, find the corresponding pair (secret, payload).
3. Allocate a pointer to the payload.
4. Return this pointer.

• secret(commitment)

1. If there isn’t exactly 1 input argument, return error.
2. Otherwise, if the commitment is known, find the corresponding pair (secret, payload).
3. Allocate a pointer to the secret.
4. Return this pointer.

• comm(value)

1. Take as input a pointer to the value, and it finds the field element given by value.hash().
2. Allocate a pointer whose tag is globals.comm-tag and the hash is given value.hash().
3. Return this pointer.

The commitment scheme is implemented by concatenating a pointer and a secret field element and computing the Poseidon hash function. Since functions are defined using lambda expressions, we obtain functional commitments basically for free.

Globals

We allocate constants in order to represent global data. For instance, we have global pointers, such as the terminal pointer, which can only be used in the last frame to indicate a program finished successfully. We also have an error pointer for programs that didn’t finish correctly. The first frame determines the outermost continuation, which has an outermost continuation pointer. Another important global pointer is the one that points to the symbol nil.

We also have global constants for each different tag in the system. Those constants are useful for comparing runtime data and determining which kind of pointer we are dealing with.

Beyond that, we have constants for Boolean variables. We pair $\tt{\footnotesize{true}}$ with 1 and $\tt{\footnotesize{false}}$ with 0. Finally, we have a constant of value 0 for default numbers.

Reduce expression

In this section, we explain the step-by-step reduction of complex expressions.

First, we provide an overview in Algorithm 3.1, which constructs multicase clauses selected based on the expression tag. Each distinct tag has a different reduction method, but the overall process remains the same. The result of the reduction provides a new triple of expression, environment, and continuation. Additionally, it determines whether we need to apply the continuation, resulting in a new IO consisting of the triple expression, environment, and continuation. For certain continuations, we need to create a thunk.

Reducing self-evaluated expressions is straightforward. The expression, environment, and continuation remain unchanged, but we must apply the continuation to the evaluated expression.

If the expression is a thunk, we need to verify hash consistency before applying the continuation.

If the expression is a symbol or a cons, we have two distinct scenarios that require detailed explanations. Therefore, we will dedicate a section to each scenario.

1. $\com{Compute and add clauses for self-evaluated expressions.}$
2. $\com{Compute and add thunk clause.}$
3. $\com{Compute and add sym clause.}$
4. $\com{Compute and add cons clause.}$
5. $\com{Get result from multicase gadget.}$
6. $\com{Apply continuation.}$
7. $\com{Make thunk.}$
8. $\com{Error handling.}$
9. Return $(\var{expr}, \var{env}, \var{cont})$.

Specifically, we do the following:

1. Let $\var{clauses} = \gad{MULTICASE-CLAUSES}()$.
2. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.nil},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
3. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.num},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
4. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.fun},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
5. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.char},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
6. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.str},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
7. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.comm},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
8. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.key},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
9. $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.u64},\var{expr},\var{env},\var{cont},\var{witness},\var{globals})$.
10. Let $\var{cont-is-terminal} = \gad{ALLOC-TAG-EQUAL}(\var{cont.tag}(), \var{globals.terminal-tag}())$.
11. Let $\var{cont-is-error} = \gad{ALLOC-TAG-EQUAL}(\var{cont.tag}(), \var{globals.error-tag}())$.
12. Let $\var{expr-is-thunk} = \gad{ALLOC-TAG-EQUAL}(\var{expr.tag}(), \var{globals.thunk-tag})$.
13. Let $(\var{expr-thunk-hash}, \var{expr-thunk-value}, \var{expr-thunk-continuation}) = \var{expr}.\gad{ALLOCATE-THUNK-COMPONENTS-UNCONSTRAINED}()$.
14. Call $\gad{IMPLIES-EQUAL}(\var{expr-is-thunk}, \var{expr-thunk-hash}, \var{expr.hash}())$.
15. Call $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.thunk}, \var{expr-thunk-value}, \var{env}, \var{expr-thunk-continuation}, \var{globals.true-num})$.
16. Let $\var{reduce-sym-not-dummy} = \gad{ALLOC-TAG-EQUAL}(\var{expr.tag}(), \var{globals.sym-tag})$.
17. Let $\var{cont-is-terminal-or-error} = \gad{OR}(\var{cont-is-terminal}, \var{cont-is-error})$.
18. Let $\var{cont-is-not-terminal-or-error} = \var{cont-is-terminal-or-error}.\gad{NOT}()$.
19. Let $\var{reduce-sym-not-dummy} = \gad{AND}(\var{reduce-sym-not-dummy}, \var{cont-is-not-terminal-or-error})$.
20. Let $(\var{result}, \var{sym-env}, \var{sym-cont}, \var{sym-apply-cont}) = \cir{Reduce-Sym}(\var{expr}, \var{env}, \var{cont}, \var{reduce-sym-not-dummy}, \var{witness}, \var{allocated-cons-witness}, \var{allocated-cont-witness})$.
21. Call $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.sym}, \var{sym-result}, \var{sym-env}, \var{sym-cont}, \var{sym-apply-cont})$.
22. Let $\var{expr-is-cons} = \gad{ALLOC-TAG-EQUAL}(\var{expr.tag}(), \var{globals.cons-tag})$.
23. Let $\var{reduce-cons-not-dummy} = \gad{AND}(\var{expr-is-cons}, \var{cont-is-not-terminal-or-error})$.
24. Let $(\var{cons-result}, \var{cons-env}, \var{cons-cont}, \var{cons-apply-cont}) = \var{Reduce-cons}(\var{expr}, \var{env}, \var{cont}, \var{reduce-cons-not-dummy}, \var{witness}, \var{allocated-cons-witness}, \var{allocated-cont-witness})$.
25. Call $\var{clauses}.\gad{ADD-CLAUSE}(\var{tag.cons}, \var{cons-result}, \var{cons-env}, \var{cons-cont}, \var{cons-apply-cont})$.
26. Let $\var{results} = \var{MULTICASE}(\var{expr.tag}(), \var{clauses})$.
27. Let $\var{first-result-expr0} = \var{results}[0])$.
28. Let $\var{first-result-expr} = \var{PICK}(\var{cont-is-terminal-or-error}, \var{globals.nil-ptr}, \var{first-result-expr0})$.
29. Let $\var{first-result-env} = \var{results}[1]$.
30. Let $\var{first-result-cont} = \var{results}[2]$.
31. Let $\var{first-result-apply-continuation} = \var{results}[6]$.
32. Let $\var{apply-continuation-boolean0} = \gad{ALLOC-IS-ZERO}(\var{first-result-apply-continuation}).\gad{NOT}()$.
33. Let $\var{apply-continuation-boolean} = \gad{AND}(\var{apply-continuation-boolean0}, \var{cont-is-not-terminal-or-error})$.
34. Let $\var{apply-continuation-results}=\cir{Apply-Continuation}(\var{expr},\var{env},\var{cont},\var{witness},\var{globals},\var{flag})$.
35. Let $\var{apply-continuation-make-thunk} = \var{apply-continuation-results}[3]$.
36. Let $\var{result-expr0} = \gad{PICK}(\var{apply-continuation-boolean}, \var{apply-continuation-results}[0], \var{first-result-expr})$.
37. Let $\var{result-env0} = \gad{PICK}(\var{apply-continuation-boolean}, \var{apply-continuation-results}[1], \var{first-result-env})$.
38. Let $\var{result-cont0} = \gad{PICK}(\var{apply-continuation-boolean}, \var{apply-continuation-results}[2], \var{first-result-cont})$.
39. Let $\var{make-thunk-num} = \gad{PICK}(\var{apply-continuation-boolean}, \var{apply-continuation-make-thunk}, \var{globals.false-num})$.
40. Let $\var{make-thunk-boolean} = \gad{ALLOC-IS-ZERO}(\var{make-thunk-num}).\gad{NOT}()$.
41. Let $\var{thunk-results} = \cir{Make-Thunk}(\var{result-cont0}, \var{result-expr0}, \var{result-env0}, \var{make-thunk-boolean}, \var{allocated-cont-witness})$.
42. Let $\var{result-expr-candidate} = \gad{PICK}(\var{make-thunk-boolean}, \var{thunk-results}[0], \var{result-expr0})$.
43. Let $\var{result-env-candidate} = \gad{PICK}(\var{make-thunk-boolean}, \var{thunk-results}[1], \var{result-env0})$.
44. Let $\var{result-cont-candidate} = \gad{PICK}(\var{make-thunk-boolean}, \var{thunk-results}[2], \var{result-cont0})$.
45. Let $\var{result-expr} = \gad{PICK}(\var{cont-is-terminal-or-error}, \var{expr}, \var{result-expr-candidate})$.
46. Let $\var{result-env} = \gad{PICK}(\var{cont-is-terminal-or-error}, \var{env}, \var{result-env-candidate})$.
47. Let $\var{result-cont} = \gad{PICK}(\var{cont-is-terminal-or-error}, \var{cont}, \var{result-cont-candidate})$.
48. Return $(\var{result-expr}, \var{result-env}, \var{result-cont})$.

Reduce symbol

To reduce symbol expressions, we must determine whether the symbol is a self-evaluated symbol or a variable that needs to be looked up in the environment. If it’s the latter, we must determine whether we have a regular or recursive environment. In a regular environment, we compare the given symbol with the first binding in the environment. If it’s the variable we’re looking for, we return the corresponding value in a thunk. Otherwise, we recursively call the lookup method in the remaining bindings in the environment. For a recursive environment, we follow the same strategy, but using closures when the value to be used is a function.

To carry out these steps, we first analyze whether the expression is a self-evaluated symbol, like NIL or T, or a variable name that we must look up in the environment. Distinguishing between these possibilities requires multiple booleans and using car-cdr to split the expression and environment in a way that lets us identify code paths leading to the end of the recursive lookup or error continuations.

Finally, we compute a boolean that identifies the control flow. In other words, we determine whether to apply the continuation or not. This boolean is crucial because we must always run the part of the circuit corresponding to apply_cont(), but we restrict the circuit to use dummy variables when this boolean value is false.

1. $\com{Calculate condition terms.}$
2. $\com{Calculate output predicate.}$
3. $\com{Calculate conditions.}$
4. $\com{Calculate implications.}$

The algorithm receives as input a triple $(\var{expr}, \var{env}, \var{cont})$, together with a variable called $\var{not-dummy}$, which is a Boolean whose value is false when the input expression is not a symbol. In this case, $\cir{Reduce-Sym}$ constraints are not actually used, which means those constraints will contain only dummy values. The algorithm also receives the witness, the store, and the globals as input.

The circuit described here mimics the evaluation of expressions whose tag is equal to $\var{globals.sym-tag}$. However, if we follow exactly the same steps as implemented in eval.rs, then some constraints would be unnecessarily repeated. Hence, in order to eliminate those constraints, we need to pay the price of making it a bit harder to guarantee that the circuit implementation corresponds to what is implemented in eval.rs. We clarify here the differences between both worlds, and show why they are equivalent.

• Circuit Reduce-Symbol( expr: AllocatedPtr, env: AllocatedPtr, cont: AllocatedPtr, not_dummy: Boolean, witness: Witness ):
1. Calculate condition terms:
1. Let $\var{output-expr} = \var{witness}.\var{prethunk-output-expr}$.
2. Let $\var{output-env} = \var{witness}.\var{prethunk-output-env}$.
3. Let $\var{output-cont} = \var{witness}.\var{prethunk-output-cont}$.
4. Let $\var{sym-is-nil} = \var{expr}.\gad{IS-NIL}()$.
5. Let $\var{sym-is-t} = \gad{ALLOC-EQUAL}(\var{expr}, \var{globals.t-ptr})$.
6. Let $\var{sym-is-nil-or-t} = \gad{OR}(\var{sym-is-nil}, \var{sym-is-t})$.
7. Let $\var{sym-is-self-evaluating} = \gad{AND}(\var{sym-is-nil-or-t}, \var{not-dummy})$.
8. Let $\var{sym-otherwise} = \gad{AND}(\var{sym-is-self-evaluating}.\gad{NOT}(), \var{not-dummy})$.
9. Let $\var{env-is-nil} = \var{env}.\gad{IS-NIL}()$
10. Let $\var{env-not-nil} = \var{env-is-nil}.\gad{NOT}()$.
11. Let $\var{env-not-dummy} = \var{sym-otherwise}$.
12. Let $(\var{binding}, \var{smaller-env}) = \gad{CAR-CDR-NAMED}(\var{env}, \var{names.env}, \var{allocated-cons-witness}, \var{env-not-dummy})$.
13. Let $\var{main} = \gad{AND}(\var{sym-otherwise}, \var{env-not-nil})$.
14. Let $\var{binding-is-nil} = \var{binding}.\gad{IS-NIL}()$.
15. Let $\var{binding-not-nil} = \var{binding-is-nil}.\gad{NOT}()$.
16. Let $\var{binding-is-cons} = \gad{IS-CONS}(\var{binding})$.
17. Let $\var{env-car-not-dummy} = \gad{AND}(\var{main}, \var{binding-is-cons})$.
18. Let $(\var{var-or-rec-binding}, \var{val-or-more-rec-env}) = \gad{CAR-CDR-NAMED}(\var{binding}, \var{names.env-car}, \var{allocated-cons-witness}, \var{env-car-not-dummy})$.
19. Let $\var{var-or-rec-binding-is-sym} = \gad{IS-SYM}(\var{var-or-rec-binding})$.
20. Let $\var{var-or-rec-binding-is-cons} = \gad{IS-CONS}(\var{var-or-rec-binding})$.
21. Let $\var{var-or-rec-binding-is-sym-or-cons} = \gad{OR}(\var{var-or-rec-binding-is-sym}, \var{var-or-rec-binding-is-cons})$.
22. Let $\var{with-binding} = \gad{AND}(\var{main}, \var{binding-not-nil})$.
23. Let $\var{with-sym-binding} = \gad{AND}(\var{with-binding}, \var{var-or-rec-binding-is-sym})$.
24. Let $\var{with-cons-binding} = \gad{AND}(\var{with-binding}, \var{var-or-rec-binding-is-cons})$.
25. Let $\var{with-other-binding} = \gad{AND}(\var{with-binding}, \var{var-or-rec-binding-is-sym-or-cons}.\gad{NOT}())$.
26. Let $v = \var{var-or-rec-binding}$.
27. Let $\var{val} = \var{val-or-more-rec-env}$.
28. Let $\var{v-is-expr1} = \gad{ALLOC-EQUAL}(\var{expr}, v)$.
29. Let $\var{envcaar-not-dummy} = \var{with-cons-binding}$.
30. Let $(\var{v2}, \var{val2}) = \gad{CAR-CDR-NAMED}(\var{globals}, \var{var-or-rec-binding}, \var{names.env-caar}, \var{allocated-cons-witness}, \var{envcaar-not-dummy})$.
31. Let $\var{val2-is-fun} = \gad{IS-FUN}(\var{val2})$.
32. Let $\var{v2-is-expr} = \gad{ALLOC-EQUAL}(\var{v2}, \var{expr})$.
33. Let $\var{v2-is-expr-real} = \gad{AND}(\var{v2-is-expr}, \var{envcaar-not-dummy})$.
34. Let $\var{extended-env-not-dummy} = \gad{AND}(\var{val2-is-fun}, \var{v2-is-expr-real})$.
35. Let $(\var{fun-hash}, \var{fun-arg}, \var{fun-body}, \var{fun-closed-env}) = \gad{ALLOCATE-MAYBE-FUN-UNCONSTRAINED}(\var{witness}.\fun{closure-to-extend}())$.
36. Call $\gad{IMPLIES-EQUAL}(\var{extended-env-not-dummy}, \var{fun-hash}, \var{val2.hash}())$.
37. Let $\var{rec-env} = \var{binding}$.
38. Let $\var{extended-env} = \gad{CONSTRUCT-CONS-NAMED}(\var{rec-env}, \var{fun-closed-env}, \var{names.extended-closure-env}, \var{allocated-cons-witness}, \var{extended-env-not-dummy})$.
39. Let $\var{extended-fun} = \gad{CONSTRUCT-FUN}(\var{fun-arg}, \var{fun-body}, \var{extended-env})$.
40. Let $\var{val-to-use} = \gad{PICK}(\var{val2-is-fun}, \var{extended-fun}, \var{val2})$.
41. Let $\var{smaller-rec-env} = \var{val-or-more-rec-env}$.
42. Let $\var{smaller-rec-env-is-nil} = \var{smaller-rec-env}.\gad{IS-NIL}()$.
43. Let $\var{smaller-rec-env-not-nil} = \var{smaller-rec-env-is-nil}.\gad{NOT}()$.
44. Let $\var{v2-not-expr} = \var{v2-is-expr}.\gad{NOT}()$.
45. Let $\var{otherwise-and-v2-not-expr} = \gad{AND}(\var{v2-not-expr}, \var{with-cons-binding})$.
46. Let $\var{smaller-rec-env-not-dummy} = \gad{AND}(\var{smaller-rec-env-not-nil}, \var{otherwise-and-v2-not-expr})$.
47. Let $\var{rec-extended-env} = \gad{CONSTRUCT-CONS-NAMED}(\var{smaller-rec-env}, \var{smaller-env}, \var{names.env-to-use}, \var{allocated-cons-witness}, \var{smaller-rec-env-not-dummy})$.
48. Let $\var{env-to-use} = \gad{PICK}(\var{smaller-rec-env-is-nil}, \var{smaller-env}, \var{rec-extended-env})$.
49. Let $\var{cont-is-lookup} = \gad{ALLOC-TAG-EQUAL}(\var{cont.tag}(), \var{globals.lookup-cont-tag}$.
50. Let $\var{needed-env-missing} = \gad{AND}(\var{sym-otherwise}, \var{env-is-nil})$.
51. Let $\var{needed-binding-missing} = \gad{AND}(\var{main}, \var{binding-is-nil})$.
52. Let $\var{with-sym-binding-matched} = \gad{AND}(\var{with-sym-binding}, \var{v-is-expr1})$.
53. Let $\var{with-sym-binding-unmatched} = \gad{AND}(\var{with-sym-binding}, \var{v-is-expr1}.\gad{NOT}())$.
54. Let $\var{with-sym-binding-unmatched-old-lookup} = \gad{AND}(\var{with-sym-binding-unmatched}, \var{cont-is-lookup})$.
55. Let $\var{with-sym-binding-unmatched-new-lookup} = \gad{AND}(\var{with-sym-binding-unmatched}, \var{cont-is-lookup}.\gad{NOT}())$.
56. Let $\var{with-cons-binding-matched} = \gad{AND}(\var{with-cons-binding}, \var{v2-is-expr})$.
57. Let $\var{with-cons-binding-unmatched} = \gad{AND}(\var{with-cons-binding}, \var{v2-is-expr}.\gad{NOT}())$.
58. Let $\var{with-cons-binding-unmatched-old-lookup} = \gad{AND}(\var{with-cons-binding-unmatched}, \var{cont-is-lookup})$.
59. Let $\var{with-cons-binding-unmatched-new-lookup} = \gad{AND}(\var{with-cons-binding-unmatched}, \var{cont-is-lookup}.\gad{NOT}())$.
60. Let $\var{lookup-continuation-not-dummy} = \gad{OR}(\var{with-sym-binding-unmatched-new-lookup}, \var{with-cons-binding-unmatched-new-lookup})$.
61. Let $\var{lookup-continuation} = \gad{CONSTRUCT-NAMED}(\var{names.lookup}, \var{globals.lookup-cont-tag}, (\var{env}, \var{cont}, \var{default-num-pair}, \var{default-num-pair}), \var{allocated-cont-witness}, \var{lookup-continuation-not-dummy})$.
2. Calculate output predicate:
1. Let$\var{output-expr-is-expr} = \gad{EQUAL}(\var{output-expr}, \var{expr})$.
2. Let $\var{output-env-is-env} = \gad{EQUAL}(\var{output-env}, \var{env})$.
3. Let $\var{output-cont-is-cont} = \gad{EQUAL}(\var{output-cont}, \var{cont})$.
4. Let $\var{output-cont-is-error} = \gad{EQUAL}(\var{output-cont}, \var{globals.error-ptr})$.
5. Let $\var{output-expr-is-val} = \var{EQUAL}(\var{output-expr}, \var{val})$.
6. Let $\var{output-env-is-smaller-env} = \gad{EQUAL}(\var{output-env}, \var{smaller-env})$.
7. Let $\var{output-cont-is-lookup} = \gad{EQUAL}(\var{output-cont}, \var{lookup-continuation})$.
8. Let $\var{output-expr-is-val-to-use} = \gad{EQUAL}(\var{output-expr}, \var{val-to-use})$.
9. Let $\var{output-env-is-env-to-use} = \gad{EQUAL}(\var{output-env}, \var{env-to-use})$.
3. Calculate conditions:
1. Let $\var{output-expr-should-be-expr} = \gad{OR}(\var{needed-env-missing}, \var{sym-is-self-evaluating}, \var{needed-binding-missing}, \var{with-sym-binding-unmatched}, \var{with-cons-binding-unmatched})$.
2. Let $\var{output-expr-should-be-val} = \var{with-sym-binding-matched}$.
3. Let $\var{output-expr-should-be-val-to-use} = \var{with-cons-binding-matched}$.
4. Let $\var{output-env-should-be-env} = \gad{OR}(\var{needed-binding-missing}, \var{needed-env-missing}, \var{sym-is-self-evaluating}, \var{with-sym-binding-matched}, \var{with-cons-binding-matched})$.
5. Let $\var{output-env-should-be-smaller-env} = \var{with-sym-binding-unmatched}$.
6. Let $\var{output-env-should-be-env-to-use} = \var{with-cons-binding-unmatched-new-lookup}$.
7. Let $\var{output-cont-should-be-cont} = \gad{OR}(\var{sym-is-self-evaluating}, \var{with-sym-binding-matched}, \var{with-sym-binding-unmatched-old-lookup}, \var{with-cons-binding-matched}, \var{with-cons-binding-unmatched-old-lookup})$.
8. Let $\var{output-cont-should-be-error} = \gad{OR}(\var{with-other-binding}, \var{needed-env-missing}, \var{needed-binding-missing})$.
4. Calculate implications:
1. Call $\gad{IMPLIES}(\var{output-expr-should-be-expr}, \var{output-expr-is-expr})$.
2. Call $\gad{IMPLIES}(\var{output-expr-should-be-val}, \var{output-expr-is-val})$.
3. Call $\gad{IMPLIES}(\var{output-expr-should-be-val-to-use}, \var{output-expr-is-val-to-use})$.
4. Call $\gad{IMPLIES}(\var{output-cont-should-be-error}, \var{output-expr-is-expr})$.
5. Call $\gad{IMPLIES}(\var{output-env-should-be-env}, \var{output-env-is-env})$.
6. Call $\gad{IMPLIES}(\var{output-env-should-be-smaller-env}, \var{output-env-is-smaller-env})$.
7. Call $\gad{IMPLIES}(\var{output-env-should-be-env-to-use}, \var{output-env-is-env-to-use})$.
8. Call $\gad{IMPLIES}(\var{output-cont-should-be-error}, \var{output-env-is-env})$.
9. Call $\gad{IMPLIES}(\var{output-cont-should-be-cont}, \var{output-cont-is-cont})$.
10. Call $\gad{IMPLIES}(\var{output-cont-should-be-error}, \var{output-cont-is-error})$.
11. Call $\gad{IMPLIES}(\var{lookup-continuation-not-dummy}, \var{output-cont-is-lookup})$.
12. Let $\var{apply-cont-bool} = \gad{OR}(\var{with-cons-binding-matched}, \var{with-sym-binding-matched}, \var{sym-is-self-evaluating})$.
13. Let $\var{apply-cont-num} = \gad{BOOLEAN-NUM}(\var{apply-cont-bool})$.
14. Return $(\var{output-expr}, \var{output-env}, \var{output-cont}, \var{apply-cont-num})$.

Reduce Cons

In this section we describe the $\cir{Reduce-Cons}()$ algorithm, which is responsible for taking a cons expression and reducing it to a triple (expr, env, cont) to be evaluated next, and determining if the continuation will be applied or not. In order to avoid calculating unnecessary hashes inside the circuit, we first use a multicase to select the preimage for the next continuation, then we compute – just once – the continuation pointer. Afterward, we use a second multicase to select the final result.

1. $\cirio{INPUT} \var{expr}, \var{env}, \var{cont}, \var{witness}$.
2. $\cirio{OUTPUT} \var{expr}, \var{env}, \var{cont}$.
3. $\com{Compute preimage clauses.}$
4. Let $\var{preimage} = \gad{MULTICASE}(\var{preimage-clauses})$.
5. $\com{Calculate newer continuation pointer.}$
6. $\com{Compute clauses.}$
7. $\var{result} = \gad{MULTICASE}(\var{clauses})$.
8. Return $\var{result}$.

In $\cir{Reduce-Sym}()$ we dealt with expressions that correspond to just one symbol. On the other hand, $\cir{Reduce-Cons}()$ allows us to reduce more complicated expressions, since a cons expression can represent unary and binary operations. In particular, those operations have a list of parameters that themselves can be symbols or cons expressions.

Here we can describe how to reduce cons expressions:

A $\tt{\footnotesize{cons}}$ expression can also be used to represent lambda, let, and letrec operations. The first thing we do with a cons operation is to split its arguments into head – the first element of the expression, which corresponds to the car operation – and the rest of the elements, which correspond to the cdr operation. Next, we describe how we calculate the constraints and how we add one clause to the multicase gadget for each possible head.

1. Let $(\var{head}, \var{rest}) = \cir{CAR-CDR-NAMED}(\var{expr}, \var{cons-names.expr}, \var{allocated-cons-witness}, \var{not-dummy})$.
2. Let $\var{head-is-lambda0} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.lambda-sym.hash}())$.
3. Let $\var{head-is-let} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.let-sym.hash}())$.
4. Let $\var{head-is-letrec} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.letrec-sym.hash}())$.
5. Let $\var{head-is-eval} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.eval-sym.hash}())$.
6. Let $\var{head-is-quote0} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.quote-sym.hash}())$.
7. Let $\var{head-is-cons} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.cons-sym.hash}())$.
8. Let $\var{head-is-hide} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.hide-sym.hash}())$.
9. Let $\var{head-is-commit} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.commit-sym.hash}())$.
10. Let $\var{head-is-open} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.open-sym.hash}())$.
11. Let $\var{head-is-secret} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.secret-sym.hash}())$.
12. Let $\var{head-is-num} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.num-sym.hash}())$.
13. Let $\var{head-is-u64} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.u64-sym.hash}())$.
14. Let $\var{head-is-comm} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.comm-sym.hash}())$.
15. Let $\var{head-is-char} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.char-sym.hash}())$.
16. Let $\var{head-is-begin} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.begin-sym.hash}())$.
17. Let $\var{head-is-car} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.car-sym.hash}())$.
18. Let $\var{head-is-cdr} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.cdr-sym.hash}())$.
19. Let $\var{head-is-atom} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.atom-sym.hash}())$.
20. Let $\var{head-is-emit} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.emit-sym.hash}())$.
21. Let $\var{head-is-plus} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.plus-sym.hash}())$.
22. Let $\var{head-is-minus} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.minus-sym.hash}())$.
23. Let $\var{head-is-times} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.times-sym.hash}())$.
24. Let $\var{head-is-div} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.div-sym.hash}())$.
25. Let $\var{head-is-mod} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.mod-sym.hash}())$.
26. Let $\var{head-is-numequal} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.numequal-sym.hash}())$.
27. Let $\var{head-is-eq} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.eq-sym.hash}())$.
28. Let $\var{head-is-less} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.less-sym.hash}())$.
29. Let $\var{head-is-less-equal} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.less-equal-sym.hash}())$.
30. Let $\var{head-is-greater} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.greater-sym.hash}())$.
31. Let $\var{head-is-greater-equal} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.greater-equal-sym.hash}())$.
32. Let $\var{head-is-if0} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.if-sym.hash}())$.
33. Let $\var{head-is-current-env0} = \gad{ALLOC-EQUAL}(\var{head.hash}(), \var{globals.current-env-sym.hash}())$.
34. Let $\var{head-is-a-sym} = \gad{IS-SYM}(\var{head})$.
35. Let $\var{head-is-fun} = \gad{IS-FUN}(\var{head})$.
36. Let $\var{head-is-a-cons} = \gad{IS-CONS}(\var{head})$.
37. Let $\var{head-is-binop0} = \gad{OR}(\var{head-is-cons}, \var{head-is-strcons}, \var{head-is-hide}, \var{head-is-begin}, \var{head-is-plus}, \var{head-is-minus}, \var{head-is-times}, \var{head-is-div}, \\ \var{head-is-mod}, \var{head-is-equal}, \var{head-is-eq}, \var{head-is-less}, \var{head-is-less-equal}, \var{head-is-greater}, \var{head-is-greater-equal}, \var{head-is-if}, \var{head-is-eval})$.
38. Let $\var{head-is-binop} = \gad{AND}(\var{head-is-binop0}, \var{head-is-a-sym})$.
39. Let $\var{head-is-unop0} = \gad{OR}(\var{head-is-car}, \var{head-is-cdr}, \var{head-is-commit}, \var{head-is-num}, \var{head-is-u64}, \var{head-is-comm}, \var{head-is-char}, \var{head-is-open}, \var{head-is-secret}, \var{head-is-atom}, \var{head-is-emit}, \var{head-is-eval}$.
40. Let $\var{head-is-let-or-letrec0} = \gad{OR}(\var{head-is-let}, \var{head-is-letrec})$.
41. Let $\var{head-is-let-or-letrec} = \gad{AND}(\var{head-is-let-or-letrec0}, \var{head-is-a-sym})$.
42. Let $\var{head-is-lambda} = \gad{AND}(\var{head-is-lambda0}, \var{head-is-a-sym})$.
43. Let $\var{head-is-quote} = \gad{AND}(\var{head-is-quote0}, \var{head-is-a-sym})$.
44. Let $\var{head-is-current-env} = \gad{AND}(\var{head-is-current-env0}, \var{head-is-a-sym})$.
45. Let $\var{head-is-if} = \gad{AND}(\var{head-is-if0}, \var{head-is-a-sym})$.
46. Let $\var{head-is-any} = \gad{OR}(\var{head-is-quote}, \var{head-is-if}, \var{head-is-lambda}, \var{head-is-current-env}, \var{head-is-let-or-letrec}, \var{head-is-unop},\var{head-is-binop})$.
47. Let $\var{head-potentially-fun-type} = \gad{OR}(\var{head-is-a-sym}, \var{head-is-a-cons}, \var{head-is-fun})$.
48. Let $\var{head-potentially-fun} = \gad{AND}(\var{head-potentially-fun-type}, \var{head-is-any}.\gad{not}())$.
49. Let $\var{rest-is-nil} = \var{rest}.\gad{IS-NIL}()$.
50. Let $\var{rest-is-cons} = \gad{IS-CONS}(\var{rest})$.
51. Let $\var{expr-cdr-not-dummy} = \gad{AND}(\var{not-dummy}, \var{rest-is-nil}.\gad{NOT}(), \var{rest-is-cons}, \var{head-is-any}, \var{head-is-current-env}.\gad{NOT}())$.
52. Let $\var{is-dotted-error} = \gad{AND}(\var{rest-is-nil}.\gad{NOT}(), \var{rest-is-cons}.\gad{NOT}(), \var{expr-cdr-not-dummy}.\gad{NOT}())$.
53. Let $(\var{arg1}, \var{more}) = \gad{CAR-CDR-NAMED}(\var{rest}, \var{cons-names.expr-cdr}, \var{allocated-cons-witness}, \var{expr-cdr-not-dummy})$.
54. Let $\var{more-is-nil} = \gad{ALLOC-EQUAL}(\var{more}, \var{globals.nil-ptr})$.
55. Let $\var{is-binop-missing-arg-error} = \gad{AND}(\var{head-is-binop}, \var{more-is-nil}, \var{head-is-begin}.\gad{NOT}(), \var{head-is-eval}.\gad{NOT}())$.
56. Let $\var{arg1-is-cons} = \gad{IS-CONS}(\var{arg1})$.
57. Let $\var{arg1-is-str} = \gad{IS-STR}(\var{arg1})$.
58. Let $\var{arg1-is-nil} = \var{arg1}.\gad{IS-NIL}()$.
59. Let $\var{expr-cadr-not-dummy0} = \gad{OR}(\var{arg1-is-cons}, \var{arg1-is-nil}, \var{arg1-is-str})$.
60. Let $\var{expr-cadr-not-dummy} = \gad{AND}(\var{expr-cdr-not-dummy}, \var{expr-cadr-not-dummy0}, \var{head-is-lambda})$.
61. Let $(\var{car-args}, \var{cdr-args}) = \gad{CAR-CDR-NAMED}(\var{arg1}, \var{cons-names.expr-cadr}, \var{allocated-cons-witness}, \var{expr-cadr-not-dummy})$.
62. Let $\var{end-is-nil} = \var{more}.\gad{IS-NIL}()$.