Anthony Hart

I've found that replacing `Inc` with the following definition fixes the inconsistency. ``` (Inc b) = (b (Zero Empty) (λx (One x)) (λx (Zero (Inc x)))) ``` The main difference,...

It's hanging because the circuit is too big. I looked at the size of the compiled circuits, and they are; fib_1: 24 constraints fib_2: 101 constraints fib_3: 752 constraints fib_4:...

As for why it's super-exponential, each fib_n calls fib(n-1) twice in addition to calling its continuation twice, which will generally include other fib calls. It's those continuations that make it...

To give further clarification, each call to isZero generates a new witness, and Vamp-IR doesn't know that many of the witnesses will be the same. They are inputs to the...

There are no efficient alternatives that I'm aware of. You could use lagrange interpolation, but that would result in an extraordinarily large polynomial. You could also use Fermat's little theorem,...

Something did occure to me about that Fermat's little theorem suggestion. You can calculate large exponents by breaking it down into smaller, reusable parts. For example, 2^64 = 2^32 *...

I've started writing the book, and my progress can be found [here](https://github.com/anoma/VampIR-Book). - https://github.com/anoma/VampIR-Book

I don't think this is a real issue. As it stands, `,` is a left-associative binary operation that produces a tuple. Unless that causes problems, I don't see any reason...

It looks like this overflows during parsing. If this doesn't happen for modules, that suggests that suggests that definitions are parsing let binding in a recursive way that modules aren't.

Increasing the stack size to 16 MB, which can be done using the following `main` function for example ``` fn main() { let builder = thread::Builder::new().stack_size(16 * 1024 * 1024);...