La mayoría de los cálculos de interés son generalmente “con estado” (stateful) — es decir, necesitan pasar por una serie de pasos para producir el resultado final.

A veces, no necesitamos demostrar que ejecutamos el cálculo, sino solo mostrar el resultado. Por ejemplo, si A es una lista, podemos probar que B es la versión ordenada de la lista A demostrando que B es una permutación de A, y que todos los elementos de B están en orden. No hay necesidad de demostrar que ejecutamos cada paso del algoritmo de ordenamiento correctamente. Ya hemos mostrado cómo probar que los elementos de una lista están en orden, pero probar de manera eficiente que una lista es una permutación de la otra es sorprendentemente complicado, por lo que presentaremos esa técnica más adelante.

En general, hay muchos cálculos realistas que no permiten simplemente probar que el resultado es correcto. Notablemente, probar que ejecutamos correctamente sha256("RareSkills") requiere ejecutar realmente cada paso de la función hash correctamente.

Dado que las funciones hash son un poco intimidantes, introducimos el concepto de cálculo con estado mostrando cómo probar que llevamos a cabo Selection Sort en una lista correctamente. Como se señaló anteriormente, este enfoque es “excesivo” porque es más simple probar que la lista de salida es una permutación ordenada de la entrada — no importa qué algoritmo usamos para ordenar la lista.

Sin embargo, de todos modos mostramos el algoritmo Selection Sort ya que consideramos que es una introducción amena al cálculo con estado.

Selection Sort funciona de la siguiente manera:

• iterando a través de la lista
• en cada índice i, comparando el valor en i con la sublista que contiene i y cada elemento delante (i..n-1 inclusive)
• intercambiando el elemento en i con el mínimo de la sublista i..n-1

Selection Sort se ilustra en la siguiente animación:

Dado que las señales son inmutables en los circuitos ZK, cada vez que hacemos un intercambio (swap), necesitamos crear una nueva lista. Por ejemplo, si ordenáramos [5,2,3,4], la secuencia de transiciones de estado sería:

1. i = 0, [5,2,3,4] —> swap —> [2,5,3,4]
2. i = 1, [2,5,3,4] —> swap —> [2,3,5,4]
3. i = 2, [2,3,5,4] —> swap —> [2,3,4,5]

Para probar que ejecutamos Selection Sort correctamente, necesitamos probar que en la iteración i, intercambiamos el elemento en i con el mínimo de la sublista i…n - 1. Ya hemos construido la mayoría de los componentes necesarios para esto en los capítulos anteriores:

• Podemos probar que un cierto elemento es el mínimo de una lista, y que está en un índice determinado.
• Podemos probar que intercambiamos dos elementos en una lista.

En este capítulo, simplemente combinamos estos componentes. Para empezar, construimos un template que prueba que identificamos correctamente el índice del valor mínimo en una sublista:

Copy
template GetMinAtIdx(n) {
  signal input in[n];
  
  // compute and constrain min and idx
  // to be the min value in the list
  // and the index of the minimum value
  signal output min;
  signal output idx;

  // compute the minimum and its index
  // outside of the constraints
  var minv = in[0];
  var idxv = 0;
  for (var i = 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // constrain that min is ≤ all others
  component lte[n];
  for (var i = 0 ; i < n; i++) {
    lte[i] = LessEqThan(252);
    lte[i].in[0] <== min;
    lte[i].in[1] <== in[i];
    lte[i].out === 1;
  }
  
  // assert min is really at in[idx]
  component qs = QuinSelector(n);
  qs.index <== idx;
  for (var i = 0; i < n; i++) {
    qs.in[i] <== in[i];
  }
  qs.out === min;
}

Una iteración del algoritmo de ordenamiento

El primer paso en Selection Sort es intercambiar el elemento en el índice 0 con el elemento mínimo de toda la lista (que podría ser el elemento en el índice 0). A continuación se muestra el código para intercambiar el número en un índice particular con el elemento mínimo que está delante de él.

Copy
template Swap(n) {
  signal input in[n];
  signal input s;
  signal input t;
  signal output out[n];

  // NEW CODE to detect if s == t
  signal sEqT;
  sEqT <== IsEqual()([s, t]);

  // get the value at s
  component qss = QuinSelector(n);
  qss.index <== s;
  for (var i = 0; i < n; i++) {
    qss.in[i] <== in[i];
  }

  // get the value at t
  component qst = QuinSelector(n);
  qst.index <== t;
  for (var i = 0; i < n; i++) {
    qst.in[i] <== in[i];
  }

  component IdxEqS[n];
  component IdxEqT[n];
  component IdxNorST[n];
  signal branchS[n];
  signal branchT[n];
  signal branchNorST[n];
  for (var i = 0; i < n; i++) {
    dxEqS[i] = IsEqual();
    dxEqS[i].in[0] <== i;
    dxEqS[i].in[1] <== s;

    dxEqT[i] = IsEqual();
    dxEqT[i].in[0] <== i;
    dxEqT[i].in[1] <== t;

    / if IdxEqS[i].out + IdxEqT[i].out
    / equals 0, then it is not i ≠ s and i ≠ t
    dxNorST[i] = IsZero();
    dxNorST[i].in <== IdxEqS[i].out + IdxEqT[i].out;

    / if we are at index s, write in[t]
    / if we are at index t, write in[s]
    / else write in[i]
    ranchS[i] <== IdxEqS[i].out * qst.out;
    ranchT[i] <== IdxEqT[i].out * qss.out;
    ranchNorST[i] <== IdxNorST[i].out * in[i];
    
    / multiply branchS by zero if s equals t
    ut[i] <==  (1-sEqT) * (branchS[i]) + branchT[i] + branchNorST[i];
  }
}

template Select(n, start) {
  // unsorted list
  signal input in[n];
  
  // index start swapped with the min
  signal output out[n];

  // we will define GetMinAtIdxStartingAt in the next codeblock
  component minIdx0 = GetMinAtIdxStartingAt(n, start);
  for (var i = 0; i < n; i++) {
      minIdx0.in[i] <== in[i];
  }

  component Swap0 = Swap(n);
  Swap0.s <== start; // swap 0 with the min
  Swap0.t <== minIdx0.idx; // with the min (could be idx 0)
  for (var i = 0; i < n; i++) {
      Swap0.in[i] <== in[i];
  }

  // copy to out
  for (var i = 0; i < n; i++) {
      out[i] <== Swap0.out[i];
  }
}

Por supuesto, deberíamos parametrizar esto porque vamos a repetir este proceso para los índices 0…n - 2. Para hacer esto, modificaremos GetMinAtIdx para considerar solo los valores después de un índice start:

Copy
// formerly GetMinAtIdx
template GetMinAtIdxStartingAt(n, start) {
  signal input in[n];
  signal output min;
  signal output idx;

  // only look for values start and later
  var minv = in[start];
  var idxv = start;
  for (var i = start + 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // only compare to values start and later
  component lt[n];
  
  // CHANGES HERE: LOOP FROM START TO N-1
  for (var i = start ; i < n; i++) {
    lt[i] = LessEqThan(252);
    lt[i].in[0] <== min;
    lt[i].in[1] <== in[i];
    lt[i].out === 1;
  }

  // Quin Selector -- ensure that
  // assert min is really at in[idx]
  component qs = QuinSelector(n);
  qs.index <== idx;
  for (var i = 0; i < n; i++) {
    qs.in[i] <== in[i];
  }
  qs.out === min;
}

Algoritmo Final

Para probar que llevamos a cabo Selection Sort correctamente, simplemente repetimos el template anterior n - 2 veces.

Copy
include "circomlib/comparators.circom";

// ----QUIN SELECTOR ----
template CalculateTotal(n) {
  signal input in[n];
  signal output out;

  signal sums[n];

  sums[0] <== in[0];

  for (var i = 1; i < n; i++) {
    sums[i] <== sums[i-1] + in[i];
  }

  out <== sums[n-1];
}

// from https://github.com/darkforest-eth/circuits/blob/master/perlin/QuinSelector.circom
template QuinSelector(choices) {
  signal input in[choices];
  signal input index;
  signal output out;
  
  // Ensure that index < choices
  component lessThan = LessThan(4);
  lessThan.in[0] <== index;
  lessThan.in[1] <== choices;
  lessThan.out === 1;

  component calcTotal = CalculateTotal(choices);
  component eqs[choices];

  // For each item, check whether its index equals the input index.
  for (var i = 0; i < choices; i ++) {
    eqs[i] = IsEqual();
    eqs[i].in[0] <== i;
    eqs[i].in[1] <== index;

    // eqs[i].out is 1 if the index matches. As such, at most one input to
    // calcTotal is not 0.
    calcTotal.in[i] <== eqs[i].out * in[i];
  }

  // Returns 0 + 0 + 0 + item
  out <== calcTotal.out;
}

// Given array in[n]
// swap the items at index
// s and t
template Swap(n) {
  signal input in[n];
  signal input s;
  signal input t;
  signal output out[n];

  // NEW CODE to detect if s == t
  signal sEqT;
  sEqT <== IsEqual()([s, t]);

  // get the value at s
  component qss = QuinSelector(n);
  qss.index <== s;
  for (var i = 0; i < n; i++) {
    qss.in[i] <== in[i];
  }

  // get the value at t
  component qst = QuinSelector(n);
  qst.index <== t;
  for (var i = 0; i < n; i++) {
    qst.in[i] <== in[i];
  }

  component IdxEqS[n];
  component IdxEqT[n];
  component IdxNorST[n];
  signal branchS[n];
  signal branchT[n];
  signal branchNorST[n];
  for (var i = 0; i < n; i++) {
    IdxEqS[i] = IsEqual();
    IdxEqS[i].in[0] <== i;
    IdxEqS[i].in[1] <== s;

    IdxEqT[i] = IsEqual();
    IdxEqT[i].in[0] <== i;
    IdxEqT[i].in[1] <== t;

    // if IdxEqS[i].out + IdxEqT[i].out
    // equals 0, then it is not i ≠ s and i ≠ t
    IdxNorST[i] = IsZero();
    IdxNorST[i].in <== IdxEqS[i].out + IdxEqT[i].out;

    // if we are at index s, write in[t]
    // if we are at index t, write in[s]
    // else write in[i]
    branchS[i] <== IdxEqS[i].out * qst.out;
    branchT[i] <== IdxEqT[i].out * qss.out;
    branchNorST[i] <== IdxNorST[i].out * in[i];
    
    // multiply branchS by zero if s equals t
    out[i] <==  (1-sEqT) * (branchS[i]) + branchT[i] + branchNorST[i];
  }
}

// Find the smallest element starting
// at index start
template GetMinAtIdxStartingAt(n, start) {
  signal input in[n];
  signal output min;
  signal output idx;

  // only look for values start and later
  var minv = in[start];
  var idxv = start;
  for (var i = start + 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // only compare to values start and later
  component lt[n];
  
  // CHANGES HERE: LOOP FROM START TO N-1
  for (var i = start ; i < n; i++) {
    lt[i] = LessEqThan(252);
    lt[i].in[0] <== min;
    lt[i].in[1] <== in[i];
    lt[i].out === 1;
  }

  // Quin Selector -- ensure that
  // assert min is really at in[idx]
  component qs = QuinSelector(n);
  qs.index <== idx;
  for (var i = 0; i < n; i++) {
    qs.in[i] <== in[i];
  }
  qs.out === min;
}

// Given an array in, swap
// start with the smallest element
// in front of it
template Select(n, start) {
  // unsorted list
  signal input in[n];
  
  // index 0 swapped with the min
  signal output out[n];

  component minIdx0 = GetMinAtIdxStartingAt(n, start);
  for (var i = 0; i < n; i++) {
    minIdx0.in[i] <== in[i];
  }

  component Swap0 = Swap(n);
  Swap0.s <== start; // swap 0 with the min
  Swap0.t <== minIdx0.idx; // with the min (could be idx 0)
  for (var i = 0; i < n; i++) {
    Swap0.in[i] <== in[i];
  }

  // copy to out
  for (var i = 0; i < n; i++) {
    out[i] <== Swap0.out[i];
  }
}

// ---- CORE ALGORITHM ----
template SelectionSort(n) {
  assert(n > 0);

  signal input in[n];
  signal output out[n];

  signal intermediateStates[n][n];

  component SSort[n - 1];
  for (var i = 0; i < n; i++) {
    // copy the input to the first row of
    // intermediateStates. Note that we can do
    // if(i == 0) because i is not a signal
    // and i is known at compile time
    if (i == 0) {
      for (var j = 0; j < n; j++) {
        intermediateStates[0][j] <== in[j];
      }
    }

    else {
      // select sort n items starting at i - 1
      // for i = 1, we compare item at 0 to
      // the rest of the list
      SSort[i - 1] = Select(n, i - 1);
      
      // load in the intermediate state i -1
      for (var j = 0; j < n; j++) {
        SSort[i - 1].in[j] <== intermediateStates[i - 1][j];
      }
      // write the sorted result to row i
      for (var j = 0; j < n; j++) {
        SSort[i - 1].out[j] ==> intermediateStates[i][j];
      }
    }
  }

  // write the final state to the ouput
  for (var i = 0; i < n; i++) {
    intermediateStates[n-1][i] ==> out[i];
  }
}

component main = SelectionSort(9);

/* INPUT = {"in": [3,1,8,2,4,0,1,2,4]} */

Conclusión

El concepto de un “estado intermedio” y probar que nos movimos entre estados intermedios correctamente es fundamental para la verificación de la mayoría de los algoritmos ZK que se prueban en la práctica, especialmente las funciones hash y las Máquinas Virtuales ZK. El algoritmo Selection Sort presentado en este capítulo proporciona una introducción amena al cálculo con estado.