0xMiden / 0xMiden/air-script

Separation between Felt, Binary, and Integer types

オープン
#334 コメント 0 件 リアクション 0 件 担当者 1 名 @Soulthym が担当を希望しています GitHub で見る
parser
主要言語
Rust
スター
96
フォーク
39
PR マージ指標
30日以内にマージされた PR はありません

説明

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.

コントリビューションガイド

コントリビューションガイドを開く

評価

この issue はまだ評価されていません。

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。