We provide here short technical reports that document specifications of some interfaces used in our research.
The TinyRAM architecture is a random-access machine designed to be a convenient tool for expressing the correctness of nondeterministic computations.
Specifically, TinyRAM is a reduced instruction set computer (RISC), with byte- and word-addressable random-access memory. It comes in two variants: one variant follows the Harvard architecture and the other follows the von Neumann architecture.
TinyRAM strikes a balance between two opposing goals:
Having an architecture that is expressive enough to allow for short and fast assembly code obtained by compiling programs written in high-level programming languages; and
Having an architecture that is minimalistic enough to allow for efficient reductions from the correctness of program executions to arithmetic circuit satisfiability (and other algebraic constraint satisfaction problems).
The need to express correctness of nondeterministic computations arises in various applications that utilize proof systems for achieving certain security properties (e.g., zero knowledge).
TinyRAM was introduced in [BCGTV, CRYPTO13] in order to express correctness of nondeterministic computations in the setting of succinct zero-knowledge proofs. More generally, TinyRAM can be used to express computations, e.g., in probabilistically-checkable proofs, and others.