Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Separation between Felt, Binary, and Integer types #334

Open
bobbinth opened this issue Jul 3, 2023 · 0 comments
Open

Separation between Felt, Binary, and Integer types #334

bobbinth opened this issue Jul 3, 2023 · 0 comments
Labels
enhancement New feature or request parser

Comments

@bobbinth
Copy link
Contributor

bobbinth commented Jul 3, 2023

Currently, as far as the user is concerned, there is only one base type in AirScript: field element (and we can have vectors and matrixes of field elements). However, it would be good to have a slightly more sophisticated type system. Specifically, I'm thinking of having 3 base types:

  1. Field element - any value in our base field.
  2. Binary value - a field element which is either $0$ or $1$.
  3. Integer - which is a regular integer - maybe fixed to u32 type.

Binary value

Being able to determine if an element is a binary value is useful because some statements are only valid for binary values. Specifically:

  • Selectors for enf match statement can involve only binary values.
  • Logical operators !, &, and | can involve only binary values.

To specify that values in some column x can only be binary, we need to enforce the following constraint:

enf x^2 = x

It may be beneficial to add a "built-in evaluator" so that a user could do something like this:

enf is_binary(x)

Once we know that values are binary, any logical operators on them yield binary values. But if an expression involves a regular field element, the result would be a field element. For example, let's say we have columns x, y, and z:

enf is_binary(x)
enf is_binary(y)

let a = x & y    # a is binary
let b = x | !y   # b is binary
let c = x * z    # c is a field element
let d = x + z    # d is a field element

We should also probably introduce keywords felt and binary for function parameters and return types. For example, instead of:

fn foo(a: vector[2], b: scalar) -> vector[4]

We could do something like this:

fn foo(a: binary[2], b: felt) -> binary[4]

Integers

Currently, there are a few places where we implicitly assume that values are integers. For example, in something like:

let x = sum([a^i for (a, i) in (xyz, 0..5)

i is an integer.

More generally, I'm thinking integers would be used for:

  1. Iterable ranges.
  2. Indexing into vectors/matrixes.
  3. Exponents in exponentiation expressions.

If we limit the size of integers to u32 we can coerce any integer into a field element. However, we can't convert a field element into an integer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request parser
Projects
None yet
Development

No branches or pull requests

1 participant