0xMiden / 0xMiden/air-script

Separation between Felt, Binary, and Integer types

Ouverte
#334 0 commentaires 0 réactions 1 personne assignée Réclamée par @Soulthym Voir sur GitHub
parser
Langage dominant
Rust
Étoiles
96
Forks
39
Métriques de merge des PR
Aucune PR mergée en 30 j

Description

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.

Guide de contribution

Ouvrir le guide de contribution

Évaluation

Cette issue n'a pas encore été évaluée.

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.