0xMiden / 0xMiden/air-script

Sort boundary constraints

Open
#315 1 comment 0 reactions 0 assignees View on GitHub
Dominant language
Rust
Stars
96
Forks
39
PR merge metrics
No merged PRs in 30d

Description

The order in which the boundary constraints are defined is important. For example:

```
boundary_constraints:
enf p.last = 1
enf p.first = 1
```

Is not the same as:

```
boundary_constraints:
enf p.first = 1
enf p.last = 1
```

The first will emit the following code for the winterfell backend:

```
fn get_aux_assertions>(&self, aux_rand_elements: &AuxTraceRandElements) -> Vec> {
let mut result = Vec::new();
result.push(Assertion::single(0, 0, E::ONE));
result.push(Assertion::single(0, self.last_step(), E::ONE));
result
}
```

And the later

```
fn get_aux_assertions>(&self, aux_rand_elements: &AuxTraceRandElements) -> Vec> {
let mut result = Vec::new();
result.push(Assertion::single(0, self.last_step(), E::ONE));
result.push(Assertion::single(0, 0, E::ONE));
result
}
```

The issue is that the order of `Vec>` determines the order of the composition coefficients, so proofs of the two systems above are not interchangeable. Additionally, this may introduce bugs across different backends, since the order of the coefficients is implicitly defined and can easily become out of sync.

To fix the issue above an ordering is required. A proposal is to sort by `(trace, column_name, step)`, similar to https://github.com/0xPolygonMiden/air-script/issues/314

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.