On Interactive Juvix Usage - Resource Costs and Decisions

Protocol Design
1

Towards a concrete goal

In building Anoma there are many interesting things we may do to fulfill our goal of building a decentralized operating system. Further, we have chosen a strategy of successive prototypes to help achieve this goal, in doing so we place shorter term priorities of features over a holistic. Due to this we need to operate efficiently with what little time we do have to achieve both our long term and short term goals. This post lays out some concrete plans we have for Juvix that can fulfill our short term demands while meeting our long term dreams.

  1. I believe Juvix should prioritize:
    1. Continuing work on the RM backends for Nock, Cairo Etc.
    2. Focus on operating in Anoma on her terms.
    3. Focus on tooling when what we have is unacceptable for a certain task.
    4. General evolution of applications and various libraries to support people in this endeavor.
  2. I believe the following work has a lower priority due to short term constraints and less thought out plans on how we can practically leverage them:
    1. Juvix Core as a usable IR
    2. Lean verification of core programs

Out of the priorities only 1.2. has been verbally communicated and should be written down as to why at length. the other items in section 1. have already been mostly agreed upon and written up at length and thus deserve no extra special attention.

I believe we should also justify why topics in 2. still matter but have a lower priority of focus.

On focusing on operating within Anoma on her terms

The general thesis of this topic is that Anoma is a live operating system, and that we should have Juvix integrated into her in a way that gives value to both Juvix and users who wish to utilize Juvix.

I believe the first major goal in this process is to have the Juvix interactive interpreter be fully integrated with the Chambers (Anoma Client). This is both high leverage and achievable.

The goal on the surface seems quite absurd and far fetched, after all Juvix is a static batch language, how can we integrate the Juvix interpreter which doesn’t even compile down!

The answer is that Anoma is a decent computing platform with the ability to save and interpret code, giving it an inherit advantage to make even “dead” languages “live”!

The requirements from Juvix are thus:

  1. Be able to provide units of code to be saved in storage
  2. Have the current interpreter loop talk to the Chambers (client) rather

We already want 1. as this will drastically reduce the size of code needed to uploaded to the Court (Node) and Chambers (Client) by over 2 orders of magnitude (goes from 10-100KBS to an order of bytes) being a huge win for costs while also demonstrating that the node can effectively store user code. The unit here would be a module, as we can effectively store each module as a nock core.

The only extra work will be be for 2., and I don’t believe this is too much effort, as if we have 1. then it’s just a matter of having:

  1. Juvix initiate a full compilation cycle
  2. Juvix uploading to the Chambers (Client) via Juvix interop: Local environment flow
  3. Hashing the given compiled modules to effectively find where to reference them from within the interpreter.
  4. Have every interpreter send really do a grpc request to the client to evaluate some given nock.

We gain a lot from this, as we can have users do normal “data science” work within Juvix, I.E. grab all the resources of a certain kind and do analysis on it. Thus we can show that Anoma isn’t just “upload contracts”, but rather “here is an ecosystem that one can play around with”.

Since the major work for this is work we require in the short term, this ends up aligning both with our longer term vision and short term demands. I heard an estimate of the module compilation changes will take 1 month. Meaning that we can achieve this plan in a 3 month period depending on how busy we get with our other priorities. Further all these ideas are clear and easy to work through with teamwork on the engineering team.

Juvix Core as a usable IR and Lean verification of core programs

Juvix Core as a usable IR would let us store Juvix Core programs within the Court and Chambers. This is quite nice as this opens up the way to Lean verification of core programs in that we can store the code online and show a proof that the compilation is done correctly and that one juvix program has many different binaries that can be deployed on various RM we have.

While the vision roughly makes sense, my objection for prioritization is two fold:

  1. The details of this plan are unknown to engineering and I believe specs.
  2. I’m not sure long term if Juvix Core is the IR we should store online.
  3. I’m not sure what doing this now with Juvix Core buys us.

The first reason makes it hard to realize within a short time frame as we need to understand the full process and tradeoffs that are made. Further architecture discussions will need to happen within Engineering to give a fully realized model and then discussions with Juvix will then happen. As this is a new flow and user experience that can be derived in system.

The second reason is an argument that Juvix, the compiler, is not in system in any way, it’s a foreign entity, so if we have core programs stored online, what does that give us? To the system it’s an opaque thing as we can’t operate on it. Thus if I wanted to say verify that the proof actually corresponds to the core program, I’d have to leave the dominion of Anoma and check it from outside, making the UX more painful and not realizing what we want in the long term. Thus I’d argue we’ll have to undo this work as I don’t think it makes sense with our long term plans.

The third argument is an argument from I’m unsure what it really buys us. Not uploading core programs doesn’t hurt much, we will already store juvix modules online (see the first item I say we should focus on) and will store cairo circuits online, in which case juvix when we compile her programs can just note it and link it without having to upload it every time. Meaning we lose no capabilities, just some convince and and UX that I believe to be under defined anyways. Thus I’d argue this is still an interesting concept to explore but currently is not well aligned enough with our long term goals nor thought out to satisfy short term demands.

1 Like
2

As far as I recall, extending modular compilation in Juvix to go down to the Nock level was not explicitly discussed as one of the priorities during the last HH, but I can reprioritise on it if that’s needed for the short term (actually, slowly started working on that). Currently, modular compilation works down to the Core level - later everything is bundled together. Because initially the Juvix compiler was not designed with this in mind, it is tedious and time-consuming to make compilation modular, but possible.

I think these are two separate things. Indeed, it is less clear to me what storing Core programs in Anoma brings, but this is not a hard requirement for the verifiable compilation project.

I understand the “Lean verification” project as a way of increasing the confidence that your programs have indeed been compiled correctly. What we’ve discussed initially was the idea of proving the compilation process correct in general (a la CompCert or CakeML), but this is far from feasible with the resources we have. Verifying concrete compiler runs (with some user input) is the next best thing that’s feasible. We’ve discussed this as a better alternative to telling people: “Hey, we’ve run many tests on the compiler, so trust us, we didn’t miscompile your program!” From this perspective, JuvixCore comes in mostly in that it is a central IR in the compiler and as such plays an important part in verifying the compiler runs. Then, from the perspective of a user interested in verifying that the compiler executed correctly for their program, it would be good to have some Core-related tooling, because they might need to do some Core-related Lean proving (less of it as proof automation improves). This Core tooling exists and needs only minor improvements.

The work that’s been planned for this quarter, and that I made significant progress toward but haven’t yet completed, was making a proof-of-concept prototype for the compiler run verification framework which would include only Core and one or two transformations on it, without much proof automation (the user needs to write the proofs in Lean themselves). The up-front investment needed for this (in terms of Lean proofs / definitions that need to be written beforehand) turned out to be a bit higher than I expected, but still manageable.

Resorting to external tooling, at least to create the proof, doesn’t seem to be entirely avoidable. The automated tactics to help users in proving correctness of compiler runs will never be fully perfect, so in most real-world scenarios you’d need to do at least minimal Lean proving to produce the proof you want.

I remember one idea was that the final Lean proof could be somehow converted to a ZK-proof, stored in Anoma and later verified, but that’s more far-in-the-future and there hasn’t been any serious attempt to make this part any more precise. This seems to be the point where some “coordination” with Anoma would be needed, and indeed, for now I’m not entirely clear how this would look like.

That’s my understanding of the discussions on the verification topic we’ve had at the HH.

In summary, there seem to be two aspects to it:

  1. Developing a verification framework for concrete compiler runs. This is useful independently of whether you ultimately upload these proofs somewhere or not, as a “step up” from compiler testing in terms of compilation correctness guarantees. No significant interaction with Anoma the system is needed here. I see it more as a (major) compiler feature. Whether we want this or we’re fine with the “Hey, we have tests, so just trust us we didn’t miscompile!” approach is a different question, but my impression from the discussions we had was that this is indeed a long-term issue, and an initial basic prototype was put on the list of Q1 priorities.
  2. Making some sort of ZK-proof out of the finished Lean proof of compilation correctness for a given program, storing it as a witness in the Anoma system, so that other people can independently verify it (without running Lean and having access to the full original program?). That’s more up-in-the-air and this probably requires significant involvement of specs and engineering. No detailed work has been done or planned for this. Also, I’m not sure if you actually need/want to store full Core programs for this, perhaps just some kind of statement about what’s been proven? Perhaps you don’t want to store Core programs for the shielded case? And that’s also one of the reasons you might want a ZK-proof instead of just sending over your full Lean proof?

Note that 1 has independent value and doesn’t require 2 (but, as I understood, ultimately having 2 as well would be better).

1 Like
3

Thanks for the write-ups. In general, I agree that we should prioritize integration with Anoma and the developer experience thereof in the immediate term (@mariari’s first set of priorities).

This discussion to me demonstrates a need for a clearer description of the various possible flavors of verifiable compilation and standardized IRs and what they allow us to achieve in the resource machine and Anoma more generally. This relates to the broader topic of RM interoperability, which we also need to figure out for the v0.3 specs. I will organize a discussion on this topic next week - probably with @vveiln @kike @xuyang @ArtemG, maybe other folks from specs, and one representative from Juvix - @Lukasz would you be up for this? The aim of that discussion would just be to produce a clearer set of options and requirements, after which we can re-evaluate priorities (and perhaps then in the context of a larger planning session at HHH 2025.Q1).

1 Like
4

Yes, let’s discuss this next week