Expression of the Blake3 permutation

[storojs72]

Hi there!

I'm working on a Blake3 implemented as a Binius circuit (IrreducibleOSS/binius#16). I'm currently thinking about way of writing a gadget for the Blake3 permutation. In order to define a proving system (Binius) constraint I need to know the expression the produces equivalent outputs for a given inputs of a MSG_PERMUTATION lookup.

For example the Rijendael S-Box has following expression (they call it "affine transformation"):

This expression can be naturally turned into the proving system constraint. I haven't found such expression in the specification and after some digging and reading several related posts on Math.StackExchange, my understanding on this is that getting similar expression for the S-box defined as a lookup is not a trivial task. Does anyone know such an expression for Blake3 if it ever exists?