Constrain first offset of a segment

[hratoanina]

There seems to be an issue with the Memory constraints. The rangecheck ensures that, when the offset changes (but not the context and the segment), the new offset is somewhat close to the previous one. However, when changing context and/or segment, we don't check that the initial offset is small. Without this check, it's possible to jump from (context_a, segment_a, offset_a) to (context_b, segment_b, -1), then to (context_b, segment_b, 0) without breaking any constraint.

This fix introduces a new column to hold offset when we change context and/or segment, and 0 otherwise. Range-checking this column should restore soundness. It's a bit of a waste since this column is literally addr_offset with filter column context_first_change + segment_first_change, but our lookup implementation doesn't support filters. It could be added as a feature, but this would require some non-trivial changes.

Opening it as a draft PR to discuss it and see if I'm missing something.

[Nashtare]

cc @pgebheim, we may need to inform the auditors on this.

[pgebheim]

On it

[sonarcloud[bot]]

Quality Gate passed

Kudos, no new issues were introduced!

0 New issues
0 Security Hotspots
No data about Coverage
No data about Duplication

See analysis details on SonarCloud