Ways to reduce SMT proof size

[xxuejie]

Here we keep track of several ways to reduce SMT proof size, for anyone who might want to give it a try :P

Command packing

Right now, each command takes a whole byte, while we only have 5 different commands. This means for every command byte, at least half the byte will be wasted without real information.

We can use 4 bits to represent a command, and pack 2 consecutive commands in a single byte. There might be padding bits for the very last command in case the number of commands is odd, but we can still save almost half of the original bytes used to store commands.

Packing zero bits.

If we look into the structure of the actual proof, we might notice the following structure:

0x51 (Q): hash stack top item with sibling node in proof (zero)
    Zero count: 170
    Proof: c51c489eac7f7fc47d5ddde35eba3331115bfe57e10c4f5d898eb5087256a997
    Zero: 8100461f7b93b06b71d44c7ded86d97d1cfc77b5aa0100000000000000000000
0x4F (O): hash stack top item with n zero values
    Zero values: 3
0x51 (Q): hash stack top item with sibling node in proof (zero)
    Zero count: 174
    Proof: fb9f5b7f8d10734e371ad96424fff9ad6daf3466a9072d8bb33874e305ba9612
    Zero: 8100c83b474f5b591837211c74d60bb1e5c681959f3b00000000000000000000
0x51 (Q): hash stack top item with sibling node in proof (zero)
    Zero count: 1
    Proof: 0acd0ab6471db23e270665a05581d66e7e18fddc55bef1a61945b82bfd3dccfb
    Zero: 0000000000000000000000000000000000000000000000000000000000000000
0x4F (O): hash stack top item with n zero values
    Zero values: 71
0x51 (Q): hash stack top item with sibling node in proof (zero)
    Zero count: 247
    Proof: fb2ce517fa510d3f4303ab23756091f000550d327acdcc456ffee809386839b3
    Zero: 387bc1c0e4aee6167d125b9083a839ceb726d28d5dfe552d35282fbdf1170300

There are different variations on the 0x51 (Q) command:

• Zero bits have a significant amount of trailing(or leading) zeros
• Zero bits contain only zero
• Zero bits mostly contain non-zero bytes

In current version of the proof, we use full 32 bytes to store zero_bits data, which can be quite wasteful if a significant part of zero_bits are all zero. We can exploit this in the following way:

Add a new command QT (Q with trailing zero), the payload for this command, will be the following:

<QT command byte> <trailing_zero_bytes> <non_zero_bytes>

trailing_zero_bytes will be a single value, denoting how many trailing bytes in the zero_bits structure contain only zero. non_zero_bytes is raw bytes of 256 - trailing_zero_bytes, containing the leading non-zero part for zero_bits structure.

We can also add a mirroring QL (Q with leading zero) command, denoting a Q command whose zero_bits structure has a lot of leading zeros.

Those 2 commands can help us reduce the bytes for Q commands with a lot of zeros in zero_bits. Notice with those 2 new commands, the total number of command types is now 7, which can also fit in 4 bits.

Conclusion

A rough calculation shows that the above 2 optimizations can reduce a non-trival SMT proof (~16K) by 10%, which can be worthwhile in certain cases.