read_mem followed by halt leaves st0 unconstrained

[Sword-Smith]

The consistency of a value read from RAM is guaranteed by the memory table. But since padded rows do not influence the running product¹ which is used to calculate the terminal value, and since padded rows cannot be distinguished from the first halt, the running product will not be affected by the row containing the first halt. This means that the row containing the first halt should not be included when deriving the RAM table from the processor table. If this row is not included then its st0 value is not constrained if the previous instruction was a read_mem.

Since this st0 cannot be output, you could argue that this is not a problem. This st0 value will also not be part of any permutation argument/running product calculation, so the freedom that the prover has to set it shouldn't lead to soundness problems in the permutation proofs.

We have to avoid any validation logic that is conditioned on this st0 value though.

Footnotes

1. The reason that padded rows do not update the running product is that this would be incompatible with different number of padded rows in each table. And since the current idea is to have each table padded to the same height, to get a global omicron, we cannot let the padded rows count towards running products. ↩

[jan-ferdinand]

The reason that padded rows do not update the running product is that this would be incompatible with different number of padded rows in each table. And since the current idea is to have each table padded to the same height, to get a global omicron, we cannot let the padded rows count towards running products.

This is only true, and the described phenomenon only occurs, if the RAM Table has rows that the processor table does not have. With our current design, that is not the case. However, if we choose to address our memory table inconsistencies (see #12 and #24) by adding “interweaved” rows, then we do indeed have the situation you describe.

[jan-ferdinand]

I'm marking the issue as “invalid” until we have decided on a strategy to fix our memory table inconsistencies.

[jan-ferdinand]

With TIPs 0001 & 0003 underway (#80, #88), padding does not influence the correctness of Triton's memory.