Direct translation of JuvixCore to VampIR

[lukaszcz]

Implement a direct translation of JuvixCore to VampIR.

It can be assumed that we're translating a single main function of type Int -> ... -> Int -> Int which has the form \x1 ... \xn -> b where the body b can contain only:

• the variables x1,...,xn,
• integer constants,
• fully applied arithmetic operations and comparisons (OpInt* and OpEq from BuiltinOp in Core),
• if-then-else, i.e., case expressions on booleans,
• boolean constructors (with tags TagTrue and TagFalse),
• fully applied failure nodes (OpFail),
• let bindings of type Int at the top only (these should be translated to VampIR local definitions; see also Let hoisting #2033).

In particular, b doesn't contain lambdas, identifiers or inductive types other than booleans.

Ultimately, we should support arbitrary finite first-order data types in the type of the main function, with some fixed encoding to tuples of integers/field elements. It is easy to support Bool in addition to Int.

A quick and generally incorrect way of translating the failure nodes is to replace them with 0. The resulting VampIR programs will compile because Int is the only type. They will work correctly as long as the recursion limit is not reached. Perhaps this should be done at first. A proper way is to encode them with pairs (see B.7 in the Juvix-to-VampIR pipeline report).

Implementing booleans in VampIR is explained in the VampIR book (section Boolean logic). If-then-else with both branches integers can be implemented as:

def if b x y = b * x + (1 - b) * y;

Equality checking can be implemented as:

def isZero x = {
  def xi = fresh (1 | x);
  x * (1 - xi * x) = 0;
  1 - xi * x
};
def equal x y = isZero (x - y);

I'm not sure how we should implement less-than, but we can ignore it for now.

References

• VampIR book
• Juvix to VampIR pipeline report

[mariari]

I'm not sure how we should implement less-than, but we can ignore it for now.

you can do it by doing bitwise decomposition of numbers. It's a pain, but you'll need to fix the number of bits.

https://github.com/anoma/VampIR-Book/blob/main/src/section_4_3.md

is an example, We do 32 bits in GEB

[lukaszcz]

Thanks! For natural numbers I guess just checking a \ b = 0 would be better. Ultimately, I think the field should be exposed directly as a separate type Field with its own operations, and integers should be a different type Int (or Int32) with less-than comparisons based on bitwise decomposition.