0xMiden / 0xMiden/air-script

Separation between Felt, Binary, and Integer types

未关闭
#334 0 条评论 0 个 reaction 已指派 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 摘要。