0xMiden / 0xMiden/miden-vm

Require constant declarations to be typed

Aberta
#3,068 0 comentários 2 reações 2 responsáveis Reivindicada por @mooori Ver no GitHub
assembly
Linguagem predominante
Rust
Estrelas
772
Forks
352
Merge médio
1d 12h
PRs com merge (30d)
93

Descrição

> I think I'd like to solve this via typed constants, and remove these special sigils around strings - instead we'd just have something like `const FOO: string = "..."`, which would then be coerced to the correct type as needed (as this is currently unambiguous, so far as I'm aware).

_Originally posted by @bitwalker in [#2876](https://github.com/0xMiden/miden-vm/issues/2876#issuecomment-4307406967)_

---

This issue is to track implementation of typed constants in Miden Assembly.

Some additional specification details:

* The `string` type would not be represented in the `midenc-hir-type` system, as it is an AST-only type alias, whose exact representation depends on the context (i.e. used as an error message, an event name, or hashed to a word when used as an immediate). We would reject the type in other contexts (e.g. it would not be valid in type signatures).
* We would remove the separate `/` and `//` operators, and just use `/` - the semantics of `/` would then depend on the types of the operands (i.e. if the operands are felts, then `/` behaves as it does today; if they are non-felts, then normal integer division applies, i.e. the current `//` operator).
* I would suggest we allow two forms of implicit coercion: First, coercion of any integer type to a larger integer type (e.g. `u16` -> `u32` is allowed, but `u32` -> `u16` is not). Second, coercion of any integer type up to and including `u32`, to `felt`. Coercion would only apply in two contexts, and all others would be rejected with a type error:
a. When the constant is used as an immediate, and the constant can be coerced to the required immediate type
b. In binary expressions, the operand with the smallest type is coerced to the larger type.
* I would suggest we provide for explicit fallible conversion with an `as` operator, only valid in constant expressions, e.g. `const N: u32 = (X + Y ) as u32 + 1` would provide a way to reuse constants whose value is a valid instance of some smaller type. This would allow us to raise an error not only when that is not the case, but on invalid implicit conversions as well (e.g. attempting to use a `u64` value where a `felt` or `u32` is expected).
* We would assign types to instruction immediates, and require that constants used in immediate position be of compatible type (i.e. either exact match, or coercible according to the rules described above).
* We would remove special sigils like `event` which have been used to indicate how a string value in a constant can be used, as the type (and context) would now be sufficient.

The above will allow us to address a few outstanding issues:

* The need for special keywords like `event` to map strings to values (see #2876 for the latest proposed instance of this).
* The need for two different division operators (it is particularly easy to miss that `/` is actually felt division, not integer division)
* Improved handling of implicit overflow in constants

Furthermore, we gain the ability to type check portions of MASM programs with more precision (though this is not something we actually do currently, it does enable downstream tooling to better reason about MASM statically).

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.