[Feature] Primitive Type Circuits

[gluax]

This PR is to have a list of requirements and objects for Primitive Type Circuits and goals.
In addition, it will allow people to retroactively review.

Objectives

Parse Primitives Into CircuitInit Expressions

• The following:

let f = 1u32;

should be roughly parsed as something like initially:

{
  "value": {
    "CircuitInit": {
      "name": "{\"name\":\"u32\",\"span\":\"{\\\"line_start\\\":2,\\\"line_stop\\\":2,\\\"col_start\\\":12,\\\"col_stop\\\":15,\\\"path\\\":\\\"src/main.leo\\\",\\\"content\\\":\\\"  let f = 1u32;\\\"}\"}",
      "members": [
        {
          "identifier": "{\"name\":\"data\",\"span\":\"{\\\"line_start\\\":2,\\\"line_stop\\\":2,\\\"col_start\\\":11,\\\"col_stop\\\":12,\\\"path\\\":\\\"src/main.leo\\\",\\\"content\\\":\\\"  let f = 1u32;\\\"}\"}",
          "expression": {
            "Value": {
              "Integer": [
                "U32",
                "1",
                {
                  "line_start": 2,
                  "line_stop": 2,
                  "col_start": 11,
                  "col_stop": 12,
                  "path": "src/main.leo",
                  "content": "  let f = 1u32;"
                }
              ]
            }
          }
        }
      ],
      "span": {
        "line_start": 2,
        "line_stop": 2,
        "col_start": 11,
        "col_stop": 12,
        "path": "src/main.leo",
        "content": "  let f = 1u32;"
      }
    }
  }
}

• Eventually, the following should work as well.

let f = 10u32 - 1u32;

Defining Primitive Circuits

• Should these circuits be shown in the AST(@acoglio, @bendyarm)?
• Should they be the regular Circuit we have defined now?
  • If so, what do we do for the span aspects on "injected" circuits?
  • Depends if we decide if they are displayed in the AST.
• Should have some easy way to be defined and looked up.
  • Macro to generate these Leo Types?
  • Way to define member functions on these Leo Types.
  • If they are displayed in AST, we just add them to the circuits as they are now. If not, we have a similar setup that's not visible.
• Needs to allow operators like +,-,*,-,**, etc., (when appropriate) to keep the same way of operations as current syntax.
  • This will also allow overloading on non-inbuilt circuits.
• Circuit shall be named after the types.
  • Meaning users cannot define circuits named after the primitives.
• Should only ever have one variable member - named internal or data.

We should discuss how these should work here so to keep it all in line.

[howardwu]

Can someone clarify for me if we're writing everything into an R1CS circuit at the moment?

[Protryon]

@howardwu Do you mean, are we compiling with R1CS circuit as a target? Yes. Not sure if I understood the question.

[gluax]

Blocks #948 and blocks #682.

[gluax]

@howardwu I think the idea is to parse as a circuit for semantic reasons and make it easier and more maintainable to implement methods and static variables on types. However, we could still target the basic underlying type as far as R1CS.

[acoglio]

I believe that the main reason for this is to have the following associated to built-in types like u32 or char:

• Instance methods.
• Static methods.
• Constants.
  If that's the case, we could have these without necessarily categorizing types like u32 or char as 'circuit types'.

I'm mainly talking about the user's view here, not necessarily the implementation. In other words, how the Leo documentation should describe and categorize things. Now we have scalar types (consisting of atomic values) and aggregate types (consisting of compound values); circuit types are aggregate types while u32, char, etc. are scalar types. Making u32, char, etc. into circuit types would "clash" a bit with that notion.

An important point is that u32, char, etc. would not have user-accessible instance member variables, because they are atomic.

For comparison, Rust has methods for struct types, for enum types, and for built-in types. So the notion of Rust method is orthogonal to the kind of type it refers to. Similarly, Leo could have a notion of method for different kinds of types (circuit, built-ins), without necessarily viewing all the types with methods as circuit types. Same for constants, such as u32::MAX.

Regarding the AST question, as also discussed (and perhaps agreed?) in a recent meeting, I vote for keeping (essentially) the same representation as we have now for scalar values, i.e. not introducing a "circuit layer", which is isomorphic anyways, and it has to be special because the internal member variable could not have a user-accessible type.

On a semi-related note, I've been wondering about the best way to standardize the nomenclature for 'method' vs. 'member function', and 'field' vs. 'member variable' or 'member constant' (we don't have the latter though). We have been avoiding 'field' to avoid confusion with the field type, but it is a fairly standard term. Just bringing all of this up for further thought.

[gluax]

@acoglio, essentially that's what I have in mind, but it's a bit more complex at a deeper look. The logic would be to still treat them as a circuit in AST and ASG. Otherwise, the code complexity is up a lot. However, we can still write them to theorems and the ir/compiler as their base types. Another complexity would be, though, is how we represent those instance/static methods and constants in the theorems as well. Does that make sense?

[acoglio]

@gluax I agree that it should be implemented in the way that makes things most simple and uniform, as you say; you know best what makes sense for the Leo compiler.

I'm mainly thinking of the user-level story and nomenclature. For instance, we could introduce a notion of 'named type' as a type that has a "name", which may be a circuit type or a scalar type, and then say that named types have methods (built-in/predefined for scalar types, user-defined for circuit types). The new ABNF grammar could look like this:

scalar-type = boolean-type / arithmetic-type / ... ; old rule -- boolean, uN, iN, address, field, group
circuit-type = identifier / %s"Self" ; old rule
named-type = circuit-type / scalar-type ; new rule
postfix-expression = ... ; old rule
                   / named-type "::" identifier function-arguments ; modified alternative, was circuit-type only before
                   / ...

Regarding how to extend the ACL2 formalization of Leo for this (I think this is what you meant by "represent in the theorems"), I would probably introduce this notion of named type in the ACL2 abstract syntax of Leo as well, and use that as the unifying notion for types that have methods (and constants). In other words, the treatment of circuit types and scalar types would be unified by the common notion of being named types. I think that this will work for the ACL2 formalization (we'll find out soon enough if that's not the case), and it might also work for the Leo compiler's Rust implementation, but there may be other considerations for the latter that I ignore. Anyways, something you might at least consider; happy to discuss it more, if of interest. Maybe that was your plan all along, and we are just discussing nomenclature here.

Weakly related to the above, is the lexical status of the scalar types. Currently they are keywords, while non-Self circuit types are identifiers. We could turn the scalar types into ("predefined") identifiers as well. But it's really just a lexical matter.

[gluax]

Closing this due to the new proposed #1248. See the new feature #1255.