Switch to `InsnKind` in the program table

[naure]

Idea extracted from discussions with @matthiasgoergens (thread).

All circuits support a single constant opcode/funct3/funct7, so they can be merged into a single constant with enum InsnKind.

This saves 1 fixed column, 1 fixed record field, and cleans up a bit.

Note: One day we might merge some opcode circuits together or split circuits for special cases, to improve the verifier or prover cost respectively. But that will probably not match the original opcode/etc classification. So there’s no drawback in removing it.

• [x] Double-check that opcode/funct3/funct7 are constants in all circuits.
• [x] Change the layout of the program table.
• [x] Change the calls to circuit_builder.lk_fetch.
• [x] Remove func7 from imm_internal.

[matthiasgoergens]

Thanks!

I see you added a 'speed' label. Specifically, this would speed up proving a bit. But more important is the simplification of the circuits. Speed is just a welcome side effect. :⁠-⁠)

Do we have a label for that as well?

Simpler circuits are easier to understand and audit. Less likely to hide bugs and harbour exploits.

[naure]

We do now (cleanup).

[matthiasgoergens]

So my suggestion is to make this table as simple as possible. And then use the same data structure (or as much as the same as possible) to drive both the circuits and the emulator.

See how this table is essentially the same as DecodedInstruction in 'decode statically' PR with the same fields. And together with the 'named struct fields' PR we can have actually the same struct on the level of Rust code.

[naure]

use the same data structure (or as much as the same as possible) to drive both the circuits and the emulator.

Of course. It is called DecodedInstruction. The circuits have an extra step, that is a serialization to a list of field elements: DecodedInstruction -> InsnRecord.

this table is essentially the same as DecodedInstruction

My goal is to completely separate the standard and stable emulator logic from weird ZK tricks that change every day.

I had just been postponing some needed cleanup. Now fixed here: https://github.com/scroll-tech/ceno/pull/536

Hope that clears it up.

[matthiasgoergens]

My goal is to completely separate the standard and stable emulator logic from weird ZK tricks that change every day.

I suggest that the goal should be to make the emulator use the same logic as the circuits. Because we need that logic anyway, and that way it gets an additional pass of tests (and the emulator is easier to test than the circuits.)

That's especially necessary because (a) as you say the ZK tricks might change, thus need special scrutiny, and (b) emulator speed isn't as crucial as circuit correctness. (Even emulator correctness is less important than circuit correctness.)

[naure]

That is not any of this works. Will explain some other time.