Our compiler stack consists of Juvix, GEB, Vamp-IR, and Taiga. Juvix can compile to GEB and then to Vamp-IR or directly to Vamp-IR. Taiga can then call Vamp-IR functions to create or verify proofs as a part of its execution model.

### Status

Currently, we can take a Juvix program and compile it directly into Vamp-IR (bypassing GEB). Then Taiga can call Vamp-IR functions to `prove` or `verify` using the Vamp-IR circuit generated by Juvix. GEB is bypassed currently due to some missing features that are necessary to integrate GEB with Juvix.

### Strengths

This stack's primary strength is the uniformity in approach between the elements of the stack. The functional/category theoretic approach is present in each compiler, making the interface between elements simpler to maintain and modify. As a concrete example, the Vamp-IR compiler allows the inclusion of higher-order "intrinsic functions" like `map` and `fold` which correspond to those functorial operations in GEB and Juvix. We believe this uniform approach is the right one for meeting Anoma's needs.

Another strength of our stack is that the overall design sticks close to the mathematical objects we are trying to use. Juvix describes a simply-typed lambda calculus, Vamp-IR describes arithmetic circuits as systems of polynomials, GEB describes transformations between STLC and polynomials. While perhaps not the most friendly to developer onboarding, this approach allows quick integration of other tools (like Z3 for analyzing arithmetic circuits in Vamp-IR) and known PLT and compiler design techniques.

### Weaknesses

There are a few weaknesses in this compiler stack as it stands today.
1. GEB is not integrated into the stack because of some missing features, namely *modular arithmetic types* and *functor iteration*.
2. There are (mostly minor) changes that need to be made to the interfaces in the Vamp-IR library to accommodate Taiga's needs.
3. The *branching problem* (BP). The BP comes from a "normalization" step in the Juvix -> Vamp-IR compilation sequence. When functions with two or more recursive calls in the body are normalized into a form that Vamp-IR accepts, the resulting circuit contains an *enormous* number of constraints. Even very simple recursive functions of this kind compile to extremely large circuits that fail to compile due to memory constraints.
4. Far from optimal circuits in Vamp-IR
5. There is no end-to-end test of the entire stack, i.e. from Juvix to Taiga.

### Approaches to Addressing Weaknesses

Most of these weaknesses were already recognized before this report and are actively being addressed. The GEB team continues to iterate rapidly and add features. Taiga team members are communicative with the Vamp-IR team about needed features and changes to the Vamp-IR library interface. These improvements are typically minor changes which are quickly completed. The branching problem is more challenging to solve. Integrating GEB may have an effect on the BP but it is unclear at this point how much it will help. Compilation passes performing optimization steps (in the Juvix compiler, Vamp-IR compiler, or both) may reduce the extent of the blow up. Additionally, new compilation strategies such as VM-based compilation may avoid the BP. (See Lukasz's experimental VM-based compilation to Vamp-IR here: https://github.com/anoma/juvix/pull/2241.) The lack of end-to-end testing was identified during the preparation of this report. We are told the Taiga team is already working on a VP testing in Taiga. With an appropriate interface we should soon be able to perform an end-to-end test with a VP written in Juvix compiling through Vamp-IR and executed by Taiga.

### Next Steps and Priorities

The weaknesses above suggest our next steps and how to prioritize them. The issues can be divided into numerous small ones which can be solved relatively quickly and a few larger ones which require time and care. The issues with interfaces are small, numerous, concrete, straight-forward, and not particularly time-consuming to dispatch. They give an immediate pay-off by removing friction in the compiler stack and allowing our teams to test and iterate more quickly. The larger issues (the branching problem, GEB completion, represent major barriers to having a usable compiler stack and are very important, but they require more time and care. Therefore we recommend that the appropriate teams put the majority of their focus on these larger issues so that continual progress is made on them. However, when smaller interface issues arise the large problem(s) can be set aside briefly to dispatch interface issues which reduce the friction of development in the stack as a whole. Alternatively, a single team member or small subteam can focus on interface issues while the larger team remains focused on the bigger issues. Because the larger weaknesses in the compiler stack are also less concrete, teams working on them should take steps to concretize the problem as much as possible so that growth and progress can be seen.

### Further Reading
Our meeting notes and individual reports with more detail can be found here: https://hackmd.io/5C2MSUgbTfCJ4tLgZoIRgQ?both