0xMiden / 0xMiden/air-script

Separation between Felt, Binary, and Integer types

Aberta
#334 0 comentários 0 reações 1 responsável Reivindicada por @Soulthym Ver no GitHub
parser
Linguagem predominante
Rust
Estrelas
96
Forks
39
Métricas de merge de PRs
Nenhum PR com merge em 30d

Descrição

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.

Guia de contribuição

Abrir o guia de contribuição

Avaliação

Esta issue ainda não foi avaliada.

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.