Refine type inference

This issue a follow-up on #334
In https://github.com/0xMiden/air-script/pull/423, while implementing typing rules for binary operations https://github.com/0xMiden/air-script/blob/4c83b58e182f1fed2ec7a2d42bf543a6318c971a/typing/src/types.rs#L437-L643 (`=+-*^`), I've noticed a few cases related to `uint` that could be refined further:
- multiplication of `uint * !bool`
- addition of `uint + bool|felt`
- substraction of `bool|felt - uint`
- exponentiation by `0`

This is due to the type system not tracking constant values (types of `uint`).

This proposal aims to improve the overall precision of the type-system.

## Cases and analysis

### Multiplication by `uint`

First on multiplication, here are the current type inference rules:

```
vvvv
a * b || felt | bool | uint | _ | ?
=========||======|======|======|======|=====
felt || felt | felt | felt | felt | felt
bool || felt | bool | uint | _ | ?
uint || felt | uint | uint | _ | ? <<<<
_ || felt | _ | _ | _ | ?
? || felt | ? | ? | ? | ?
```

Note that the boolean is special as it is used in selectors, it needs to reflect the type of the branch it represents, hence it is always the other type.

Let's focus on uint. Since binops like `+-*` are type symmetric, let's consider the `uint` column, and ignore the untyped cases `?` and `_`:

- `uint * felt -> felt`
- `uint * bool -> uint`
- `uint * uint -> uint`

now, while that is technically correct, it does erase some information.
Namely, since uints are values that are provably constant, we know that instances of `0` and `1` are `uint`, but inference should conserve the type of the value getting multiplied if 1, or return the type of 0 otherwise.

If we consider `uint` cases, denoted `type:0` and `type:1`, we could refine `uint` multiplication where the value is known to be `0` or `1`:

- `uint:0 * T -> uint:0`
- `uint:1 * T -> T`

For example:

```
expr | current | proposed
---------------|---------|---------
uint:0 * felt | felt | uint:0 *
uint:0 * bool | uint | uint:0 *
uint:0 * uint | uint | uint:0 *
uint:1 * felt | felt | felt
uint:1 * bool | uint | bool *
uint:1 * uint | uint | uint
uint:>1 * felt | felt | felt
uint:>1 * bool | uint | uint
uint:>1 * uint | uint | uint
```

I've marked with an asterisk `*` the row affected by the change

Of course, we would need to distiguish uint on the rhs between `uint:0`, `uint:1`, and `uint`, as well as forward the rhs type when it's a `uint` != 0.

### Addition of a `uint`

Now onto addition, here are the current rules:

```
vvvv
a + b || felt | bool | uint | _ | ?
=========||======|======|======|======|=====
felt || felt | felt | felt | felt | felt
bool || felt | felt | felt | felt | felt
uint || felt | felt | uint | _ | ? <<<<
_ || felt | felt | _ | _ | ?
? || felt | felt | ? | ? | ?
```

It's symmetric again, let's consider the `uint` column, ignoring untyped cases:

- `uint + felt -> felt`
- `uint + bool -> felt`
- `uint + uint -> uint`

Again, that loses some information when `uint` is a `0` or `1`.

Proposed rules:

- `uint:0 + T -> T`
- `uint + felt -> felt`
- `uint + bool -> felt`
- `uint + uint -> uint`

The only difference is when the lhs (or rhs if synmetric) is known to be `0`.

For example:

```
expr | current | proposed
---------------|---------|---------
uint:0 + felt | felt | felt
uint:0 + bool | felt | bool *
uint:0 + uint | uint | uint
uint:>0 + felt | felt | felt
uint:>0 + bool | felt | felt
uint:>0 + uint | uint | uint
```

Similarly, we should consider the symmetric case when implementing so as to not lose type information on the rhs.

### Substraction by `uint`
This is identical to the addition case currently, but would lose the symmetry as noted in: https://github.com/massalabs/air-script/blob/4c83b58e182f1fed2ec7a2d42bf543a6318c971a/typing/src/types.rs#L536-L546

### Exponentiation by `0` or `1`
Exponentiation is simpler as it only considers cases where the rhs is unknown or constant.

```
vvvv
a ^ b || felt | bool | uint | _ | ?
=========||======|======|======|======|=====
felt || err | err | felt | _ | ?
bool || err | err | bool | _ | ?
uint || err | err | uint | _ | ?
_ || err | err | _ | _ | ?
? || err | err | ? | ? | ?
```

Let's ignore unknown cases and focus on the uint column:

- `T ^ uint -> T`

Now, if we consider the case uint:0, we should get:

- `uint:0 ^ uint:0 -> err`
- `T ^ uint:0 -> uint:1`
- `T ^ uint:>0 -> T`

The only differences are when exponentiating by 0, and an error for `0 ^ 0`

For example:

```
expr | current | proposed
----------------|---------|---------
uint:0 ^ uint:0 | uint | err
felt ^ uint:0 | felt | uint:1
bool ^ uint:0 | bool | uint:1
uint ^ uint:0 | uint | uint:1
felt ^ uint:>0 | felt | felt
bool ^ uint:>0 | bool | bool
uint ^ uint:>0 | uint | uint
```

## Proposed changes:

I can think of 2 options:

### differentiate uint into 3 cases
This will add a lot of cases to handle correctly so is tedious, but should be easy.
It also would make adding the second option harder down the line

### subtyping based on felt/int + known values:
This is a little harder to add, but should have less inherent complexity.
It boils down to:
- only tracking unknowns and felt/int cases in the ScalarType enum, making bool a property of the ScalarType
- now track known values as an additional field `possible_values` on ScalarType:
```rust
enum TypeConstraint {
Any,
OneOf(Vec),
}
```
- is_bool sets the possible values [0, 1] on felts.
- If the type is felt and possible values include only 0 and 1: treat as a bool
- If the type is uint and values == [0], treat as uint:0
- If the type is uint and values == [1], treat as uint:1

Note: a uint, since constant, always only has a single possible value.
Note 2: a felt `f` provably constrained to a single constant value `v` with `enf f = v` **could now be treated as a constant uint**
Note 3: This approach makes it trivial to report new missing constraints, simply match on the TypeConstraint enum and check the presence of the corresponding enf constraint after all transformations are done.

## Conclusion

I tend to prefer the second option, as it is easier to extend and unifies uint/felt logic (you can think const vs variable).

Mainly, it would allow tracking that a felt is constrained to a set of values other than (0,1) and be casted to a uint if constrained to a single value

I think it could also pave the way to formally prove that a circuit is not underconstrained, altho that would require a few changes: this TypeConstraint would only work for short sets of values and not general constraint equations, we would need to add a more general form, something like this

```rust

struct TypeProperty {
one_of: Vec,
other_constraints: Vec,
}

enum TypeConstraint {
Eq(Expr),
NotEq(Expr),
Sup(Expr),
SupEq(Expr),
...
}
```