Missing Aiur features

[gabriel-barrett]

Here's a list of missing features and optimizations in Aiur, not in order of importance.

1. assertCall: an operation for asserting that values are the output of a function call. In terms of constraints, this is equivalent to a pure lookup, without creating new columns. This is a quite useful operation for non-deterministic computation: a common pattern is to call a function unconstrained as a hint, then later do an assertion in case the hint was positive. In fact, the constrained call operation can be seen as the combination of the unconstrained call operation followed by assertCall.
2. Constant values and pointers. Constant definitions would look a bit like aliases, except that we should be able to also alocate constant pointers (so that you can have constant ADTs). To implement this at the protocol level, we require that these constant pointer allocations be part of the claim. Both prover and verifier have to add these allocations to the claim list
3. Return groups. As of now, functions are represented by a single circuit that might have multiple different ways/paths of providing (returning) the output. However, this is not a theoretical necessity. We could represent functions with multiple circuits, each one representing a different set of paths. "Hot" paths could be separated so we get leaner circuits, while "cold" paths could be grouped into a fat circuit. A nice way of achieving this is through the annotation of return sites that identify which group each site belongs to.
4. Precomputed tables. We should be able to define constant, global mappings/dictionaries in Aiur, mapping Aiur values to Aiur values (even custom values, though pointers are dangerous). In fact, it's even possible to have mutable global mappings, but this requires timestamps, like mutable memory (explained later).
5. Structs. Mostly for convenience, as we already have tuples.
6. Empty tag optimization. Enums of a single constructor should have no tag.
7. Null pointer optimization/Niche optimization. If we reserve the address 0 (by hardcoding the memory chip to start from 1), then we can remove the tag in a few places, like Option<&A>. There are more complicated cases that can be optimized, and the general algorithm is called "niche optimization".
8. Match lifting. It transforms matchContinue statements into a match statement by distributing the continuation block into the branches of the match statement. This should be used in a few cases. Namely, when the continuation does not itself have branching, or when there's exactly one branch that reaches the continuation. This might also be useful if there's a large branch that doesn't reach the continuation block, so that when you inline the continuation you share (most) of the columns and end up with fewer columns overall.
9. Match branch grouping. This is kind of a tricky optimization. The idea is to find equal branches in match statements and group the branches by combining the requirements of each branch using disjunction. This can be beneficial as it usually trades a selector for an auxiliary. In some situations, you'll end up with the same number of columns, but in other situations the auxiliary you get can be shared. The tricky thing is that disjunction is not trivial without the use of selectors themselves.
10. Mutable memory and mutable slices. It would be nice if Aiur functions could also mutate a global memory table. This requires timestamps, which act very much like a State monad, though I believe the easiest solution is to tag functions with a mutable tag. The reason the monad solution is more complicated is that nothing prevents an immutable function from producing an IO A value (even if it can't run it), which would represent a closure/partial application. The tag solution works like this: mutable functions can call both normal functions and mutable functions; normal functions cannot call mutable functions. Mutable functions have a hidden input parameter and output parameter, the initial timestamp and the final timestamp. Whenever a mutable function calls another function, it sends the last timestamp plus 1 to the callee, and as the callee returns a value with a new timestamp, it "updates" its timestamp to reflect the returned timestamp (this is all a compiler trick, by the way). Mutable entry functions should start with timestamp 0 in their claim. If you have multiple claims, then the timestamps should be in order.
11. Bytecode serialization. If execution turns out to be a bottleneck, then we could run it on serialized opcodes that look more like conventional bytecode.
12. Unconstrained (non-deterministic) match statements (i.e. choose). Dangerous, but could be useful in non-deterministic computations.
13. Circuit multiplicity: circuits that are used a lot should be able to be multiplied to reduce proof time/size. Multiplicity could be a property of the return group.