Block machine witgen: Always run default sequence after the cached sequence

[georgwiese]

Fixes #1559 (alternative to #1560)

With this PR, we always run the "default" sequence iterator, even if we have a cached sequence (which is still run before). This way, if the cached sequence was not sufficient to solve the entire block, the default solving sequence will have another attempt.

The reason this doesn't lead to a dramatic performance degradation is because since #1528, we skip identities that have been completed. In the typical case, the cached sequence will have completed most identities.

The reason this is better than #1560 is because the cached sequence typically makes progress with every identity, whereas the default iterator does not.

Benchmark

I ran the RISC-V Keccak example 3 times. It looks like the time spent in block machines increases by roughly 20%. Given that this fixes a bug and the overall time spent in block machines is small (even in the bitwise-heavy Keccak example), I think it's worth it!

Main

 == Witgen profile (1766802 events)
   44.5% (    4.4s): FixedLookup
   36.3% (    3.6s): Main Machine
    9.7% ( 964.7ms): Secondary machine 0: main_binary (BlockMachine)
    6.8% ( 669.3ms): witgen (outer code)
    2.4% ( 236.0ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  32.6ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 183.7µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.907174375s

 == Witgen profile (1766802 events)
   41.0% (    3.8s): FixedLookup
   39.0% (    3.6s): Main Machine
   10.2% ( 951.7ms): Secondary machine 0: main_binary (BlockMachine)
    6.9% ( 644.2ms): witgen (outer code)
    2.5% ( 231.5ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  32.1ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 183.4µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.295457333s

 == Witgen profile (1766802 events)
   43.7% (    4.2s): FixedLookup
   37.0% (    3.6s): Main Machine
   10.0% ( 963.6ms): Secondary machine 0: main_binary (BlockMachine)
    6.6% ( 636.3ms): witgen (outer code)
    2.4% ( 234.7ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  29.0ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 190.8µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.677017958s

This branch

 == Witgen profile (1986686 events)
   43.3% (    4.3s): FixedLookup
   36.2% (    3.6s): Main Machine
   11.5% (    1.1s): Secondary machine 0: main_binary (BlockMachine)
    6.0% ( 600.2ms): witgen (outer code)
    2.7% ( 273.3ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  28.6ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 203.4µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.975125084s

 == Witgen profile (1986686 events)
   40.4% (    3.9s): FixedLookup
   37.2% (    3.6s): Main Machine
   12.1% (    1.2s): Secondary machine 0: main_binary (BlockMachine)
    7.1% ( 687.7ms): witgen (outer code)
    2.9% ( 276.7ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  30.3ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 197.3µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.619824375s

 == Witgen profile (1986686 events)
   42.4% (    4.2s): FixedLookup
   36.1% (    3.6s): Main Machine
   11.9% (    1.2s): Secondary machine 0: main_binary (BlockMachine)
    6.6% ( 654.9ms): witgen (outer code)
    2.8% ( 276.6ms): Secondary machine 2: main_shift (BlockMachine)
    0.3% (  29.1ms): Secondary machine 1: main_memory (DoubleSortedWitnesses)
    0.0% ( 202.3µs): Secondary machine 3: main_split_gl (BlockMachine)
  ---------------------------
    ==> Total: 9.957052209s

[georgwiese]

This code tried to solve the same problem.

Disadvantages of the old approach:

• process_result.is_success() returns true if it was able to complete the outer query. But there might still be cells in the block that could not be solved. They will be set to 0, which might violate some constraints. This causes the issue described in Witgen produces wrong witness when reordering constraints #1559.
• If this block does get executed, the block processor is invoked again from scratch, forgetting any progress it has made already in the first call.

[Schaeff]

This change makes the machine less readable in my opinion. Also in my example it was triggered by the lookup being after was_lt, does this also trigger it?

[georgwiese]

Yes, I think I did the same and when trying to undo the change, I put it in the wrong place. Fixed now!