triton-vm
triton-vm copied to clipboard
TritonVM
Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
(Originally posted by @sshine.) The definition of `hv` helper variable registers is not explicitly mentioned in the sections for each instruction. Extract the way `hv` helper variables are set in...
AIR for the XEATs - [ ] program - [x] instruction - [ ] processor - [ ] opStack - [ ] RAM - [ ] jumpStack - [ ]...
The current set of binary instructions available in Triton VM, `and` and `xor`, is functionally complete, but not [minimally so](https://en.wikipedia.org/wiki/Functional_completeness#Minimal_functionally_complete_operator_sets). Replacing them by either `nand` or `nor` - does not...
(Originally posted by @sshine.) Consider cross-table boundary constraints: We currently don't have a section like `ext_difference_constraints()`. In `.prove()`, however, we do call `.quotient()` / `.quotient_degree_bound()` on each `PermArg`; that seems...
(Originally posted by @sshine.) - [ ] Create an overview of the most memory-wasteful areas of the code. - [ ] Avoid generating entire co-set domains - [ ] Avoid...
There are multiple ways to achieve the current functionality of the U32 Table. Let's explore the effects of different designs on both TritonVM as a whole and the recursive verifier...
Currently, executing instructions like `lt` (and a few others) leads to an increase of the relevant coprocessor's AET, e.g., the U32 Table. Most importantly, this happens _even if_ the instruction...
Let's discuss ways to check the low-degreeness of the last codeword in FRI and analyze which of the approaches is the least complex one with regards to recursive proof verification....
In order to keep the degree of the AIR polynomials low, we group instructions exhibiting the same behavior in certain aspects, allowing to (de)select for those aspects. This is achieved...
Except for the Hash Table, all constraints are represented as multivariate polynomials using the `MPolynomial` struct. This representation is both more reflective of the underlying maths that makes STARKs work...
