Random permutation circuit

General
#1

Just created a circom circuit for randomly permuting an array of field elements.

Permuting 50 elements takes only 4.3K constraints.

6 Likes
#2

We also have a similar tool (Challenge API) in the PSE/halo2 which we use to perform the RLC of the EVM words for example, or more importantly, the computation of the keccack table parameters as input RLC and output RLC. It allows further usage I think as it allows the randomness used in the permutation to be based on the witnesses themseleves. There’s an example on how to do a random vector permutation in https://github.com/halo2_proofs/examples/shuffle.rs

Han coded the example so he will know better. We could try to get some nubers also if you’re interested!!

1 Like
#3

@jbaylina What algorithm (if any) is this based off of?

2 Likes
#4

It’s just an inspirational moment after seeing a twit.

I’ve not researched if there is some thing similar (probably it is because the algorithm is quite naive). But the idea is quite similar:

Imagine you want to shuffle 4 cards in0, in1, in2, in3

You select for 4 groups of 4,3,2,1 random field elements. We call this elements selectos s_i_j

Example:

[s0_0, s0_1, s0_2, s0_3] = [0,1,0,0]
[s1_0, s1_1, s1_2] = [0,0,1]
[s2_0, s2_1] = [1,0]
[s3_0] = [1]

Conditions:
Field elements must be binary. s_i_j * (s_i_j -1 ) === 0
One and only one field element in a group must be 1. IE the addition of the field elements in a group is 1.

s0_0 + s0_1 + s0_2 + s0_3 === 1
s1_0 + s1_1 + s1_2 === 1
s2_0 + s2_1 === 1
s3_0 === 1

You now which element is selected:

n0 = 0 * 0 + 1 * 1 + 2 * 0 + 3 * 0 = 1
n1 = 0 * 0 + 1 * 0 + 2 * 1 = 2
n2 = 0 * 1 + 1 * 0 = 0
n3 = 0 * 1

So we add the last conditions:

trunc250(hash) === n0 + n14 + n243 + n3 432 + rem4321

hash is truncated to 250 bits and rem is range checked to the bits so that there is no overflow.

With this list of selectors we can easily select the element from the origin and compose the set of the remaining:

out0 = s_0_0 * in0 + s_0_1 * in1 + s_0_2 * in2 + s_0_3*in3
im0_0 = s_0_0 * (in3 - in0) + in0
im0_1 = s_0_1 * (in3 - in1) + in1
im0_2 = s_0_2 * (in3 - in2) + in2

Now the second step:
out1 = s_1_0 * im0_0 + s_1_1 * im0_1 + s_1_2 * im_0_2
im1_0 = s_1_0 * (im_0_2 - im_0_0) + im_0_0
im1_1 = s_1_1 * (im_0_2 - im_0_1) + im_0_1

3rd step
out2 = s_2_0 * im1_0 + s_2_1 * im_1_1
im2_0 = s_2_0 * (im_1_1 - im_1_0) + im_1_0

Last step
out3 = s_3_0 * im2_0

1 Like