[EXPERIMENT] solve for one column records

[qwang98]

Disclaimer: the code is almost entirely generated with Claude, but I instructed the analyses to perform and reviewed/debugged along the way to make sure the analyses matches the instruction.

Motivation:

• If we don't pass execution records with 1 column post optimization by deriving the column from other APC columns, we can save and additional ~15% from overall trace gen time, according to this prior analysis done: https://github.com/powdr-labs/powdr/pull/3484/files#diff-3b7b30c0f306feaee6ab561bc47d8f7331fa8fdb8622d1c21a55885c07938fb6
• Test if it's possible to derive these columns from constraints, essentially by implementing a simple solver.

Results:

1. Tested with the single APC in Keccak. Conclusion is that this mostly doesn't work due to bus interactions.
2. There are 87 such post-optimization columns in total (each corresponding to a record that can be potentially removed). Out of these:

• 5 is involved in any pre-optimization, during-optimization, and post-optimization constraints, which means that we start with only 5 columns that can be potentially solved via constraints alone. Out of the 5, only 1 is directly solvable by the constraints, for which I implemented a simple solver that iteratively solves constraints if there's only one unknown with degree 1.
• 82 only appear in bus interactions.

3. I analyzed the bus interactions, but I'm not sure how to derive constraints from them. Here's a break down of post-optimization bus interactions

• Bus 1 (MEMORY) has 129 sends and 129 receives: These already exclude register memory interactions, which are optimized to only have 2 left per register and are already added as constraints, so should be covered in the constraint solving step (the fact that we still performed pretty bad on that means that the added register memory constraints didn't help). I managed to exact match the address expression of 16 out of these 129 pairs, but suspect we can create equality constraint out of these, because we aren't guaranteed that bus send and receive have the same value (we were guaranteed in the register case that intra block receive that appear immediately after a same register send have the same value though).
• Bus 3 (VARIABLE_RANGE_CHECKER) has 568 sends: I dont think we can solve these as they are single sided lookups?
• Bus 6 (BITWISE_LOOKUP) has 906 sends: I don't think we can solve these as they are single sided lookups?

[qwang98]

These are all the columns that appear in a sub with length 1 in its corresponding original instruction.

These are records with only 1 post optimization column.

[qwang98]

These are all the constraints considered for solving. Basically they are:

• Start from ALL constraints that ever existed in history. These include pre-optimization constraints, during-optimization constraints (which come and go due to the optimizer), and post-optimization constraints.
• Filter these constraints to those where at least one singleton column appears (so it includes the target we intend to solve for)
• Filter the remaining constraints to those where all the algebraic references still exist post optimization (so that we don't solve from pre-optimization columns and potentially add records back)

[qwang98]

Note that columns not in the "singleton column" set are printed as known, because these are essentially APC trace buffer values that are populated as actual numbers via dummy trace subs (or direct to APC).

[qwang98]

Solvability is quite poor with the simple solver:

• Only 1 column can be solved.
• The rest are all degree 2 constraints. If we can solve these, we can remove 4 more columns/records, but this is still quite a small set out of the 87 singleton columns.

[qwang98]

This is the actual solving process. It's iterative (solve everything you can, put the solved columns to the "known" set, try to solve everything again), but stopped really short due to reasons mentioned above.

[qwang98]

Note the unsolvability analysis, most of which are due to the singleton column appearing in bus interactions only.