Cómo desarrollar una DApp de conocimiento cero

Perspectiva general

Para dar conformidad a esta aplicación se ha desarrollado con Turborepo un monorepositorio con tres espacios de trabajo principales.

Por una parte, un circuito zk-SNARK desarrollado con la librería Circom, por otra, un entorno de desarrollo de Hardhat de contratos inteligentes escritos en lenguaje Solidity (que actúan como verificadores de las pruebas) y, por último, una aplicación web escrita en TypeScript y desarrollada con Next.js.

Dado que la aplicación consiste en un juego de dos jugadores, se ha introducido también un agente de aprendizaje por refuerzo para el modelado en PyTorch de una política de juego capaz de actuar como uno de los jugadores.

En el diagrama de abajo intento concretar lo máximo posible el flujo de trabajo de esta aplicación, el cuál explicaré detenidamente en el transcurso de las siguientes secciones.

¿Qué es una zk-DApp?

Una zk-DApp es una aplicación descentralizada con la particularidad de que ofrece la opción de generar y validar pruebas de conocimiento cero. Este tipo de pruebas responden a un protocolo que posibilita que un verificador pueda asegurar la validez de una afirmación por parte de un probador, sin que éste tenga que revelar información que considere privada.

Existen diferentes clases de pruebas de conocimiento cero aunque en nuestro caso nos centraremos en el tipo zk-SNARK, acrónimo de zero-knowledege Succinct Non-interactive ARgument of Knowledge, el cuál tiene las siguientes propiedades:

• zero-knowledge: el verificador no tiene ningún conocimiento de la prueba salvo de si es válida o no.

• succinct: el tamaño de la prueba es pequeño y por lo tanto su tiempo de verificación es reducido.

• non-interactive: no necesita de interacción entre el probador y el verificador más allá de una única ronda de comunicación.

• argument of knowledge: prueba que consiste en una aserción criptográfica de que la afirmación del probador es válida.

Circuito zk-SNARK

Las pruebas zk-SNARK solamente se pueden generar directamente desde un circuito aritmético de campo finito F_p, es decir, un circuito capaz de realizar operaciones de suma y multiplicación en un campo finito de un tamaño determinado.

Por lo tanto, todas las operaciones son calculadas módulo a un valor concreto, por ejemplo, en Ethereum se necesita operar con circuitos aritméticos F_p tomando el número primo:

La conversión de un problema computacional a un circuito aritmético no siempre es aparente o evidente aunque, en la mayoría de los casos, sí es factible. La idea principal es reducir este problema a una serie de ecuaciones.

Por lo tanto, en este contexto podemos decir que el verificador de la prueba podrá comprobar criptográficamente que el probador conoce una información que cumple un sistema de ecuaciones.

En Circom, estas ecuaciones se llaman restricciones y deben ser únicamente ecuaciones cuadráticas del tipo a * b + c = 0, siendo a, b y c combinaciones lineales de señales, es decir, una restricción debe tener únicamente una multiplicación y una suma de una constante.

Las señales son las entradas y salidas de los circuitos, el cálculo de las cuales da como resultado el vector del testigo, por lo tanto cualquier salida es también una entrada al vector testigo. El testigo es, entonces, el conjunto de señales del circuito (de entrada, intermedias y de salida) y se utiliza para la generación de la prueba.

En resumen, Circom nos ayudará a crear un sistema de restricciones. Estas restricciones se llaman restricciones Rank 1 (R1CS).

El circuito tendrá dos cometidos principales, por un lado, (i) generar la prueba, para lo que se introducen las restricciones y, por otro lado, (ii) calcular el testigo, para lo que se resuelven las señales intermedias y la salida.

Como cada restricción o ecuación debe tener una multiplicación, implementar los problemas de esta manera reviste cierta complejidad, tanto es así que en ocasiones se requiere de señales auxiliares que pueden o no quedar restringidas pero a las que hay que asignarles un valor.

En Circom se considera peligroso asignar un valor a una señal sin que se genere una restricción, dado que un sistema puede quedar infrarestringido y resolver pruebas que no estén bien diseñadas, así que normalmente se harán ambas cosas a no ser que se trate de una expresión que no se pueda incluir en una restricción.

Por esta razón, Circom contiene operadores para la asignación de señales, para la generación de restricciones y, además, operadores que realizan ambas cosas:

1. Si queremos escribir una ecuación que solamente asigne el resultado de una multiplicación a una señal tendremos que escribir c <-- a * b.

2. Si solamente queremos restringir que la señal c sea el resultado de la multiplicación de a y b, escribiremos la expresión c === a * b.

3. Por último, si deseamos hacer ambas cosas a la vez podemos implementarlo con la ecuación c <== a * b, lo cual computará la multiplicación de a y b y asignará y restringirá el resultado a c.

A continuación, presentaré el circuito Circom para generar pruebas de conocimiento cero sobre información acerca de una partida determinada del juego de Conecta Cuatro.

Implementación del circuito

Nuestro circuito se utilizará para la generación del testigo y de la prueba para una partida del juego que ya se haya terminado y el resultado sea de victoria para uno de los jugadores.

Con este circuito el probador podrá probar al verificador que conoce cuál es el ganador y la combinación ganadora sin que tenga que revelar esta información.

El circuito debe cumplir los siguientes propósitos:

• asegurar que cada una de las celdas del tablero tiene el valor 0, 1 o 2.

• asegurar que solamente hay un ganador y que es el ganador que se introduce como entrada.

• asegurar que la combinación ganadora corresponde a la combinación que se introduce como entrada.

Para ello se definen tres entradas privadas: la observación del tablero, el ganador (1 o 2) y un array con los índices de las cuatro fichas consecutivas.

Como vemos, para crear un circuito genérico en Circom se utiliza un template, en el cual se pueden instanciar otros templates. En cambio, se utilizará el término main para definir el circuito o componente principal, que sirve de punto de entrada.

Para asegurarnos de que las celdas tengan valores correctos, se ha instanciado en una iteración for un circuito auxiliar, llamado AssertIsZeroOneOrTwo, al que le pasamos el valor de cada celda del tablero:

La ecuación que resuelve este problema es el polinomio de grado tres (x - 0) * (x - 1) * (x - 2) = 0, en cambio, dado que en Circom solamente podemos utilizar ecuaciones cuadráticas, primero asignamos el resultado de (x - 0) * (x - 1) a isCounterZeroOrOne para después multiplicarla por (x - 2) y restringir el resultado a cero, asegurándonos que la entrada x solo pueda valer 0, 1 o 2.

Si ejecutamos el script pnpm run print:constraints obtendremos todas las restricciones del circuito, lo que nos ayudará a entender mejor el funcionamiento del circuito y a depurar nuestra implementación.

Nos centraremos en las dos primeras restricciones que se corresponden a la primera iteración del for para row = 0 y col = 0, es decir, la comprobación de que la celda en el margen superior izquierdo del tablero equivale a 0, 1 o 2:

Considerando el campo finito de las operaciones en nuestro circuito aritmético, estas ecuaciones son equivalentes a:

Como main.board[0][0] equivale a la señal de entrada in, y haciendo un ejercicio sencillo de álgebra, tendríamos las siguientes ecuaciones, que se corresponden con las restricciones del circuito AssertIsZeroOneOrTwo:

Para que en la prueba se asegure que en el tablero solamente hay cuatro fichas consecutivas, debemos implementar un algoritmo en el que se itere por columnas y filas para cada orientación posible (horizontal, vertical, diagonal y anti diagonal).

Por ejemplo, para la orientación horizontal tendríamos la siguiente implementación.

Entonces, se itera por fila y columna y se comprueba que las tres fichas en orientación horizontal siguientes a los índices en esa iteración tienen el mismo valor. Para ello, asignamos una instancia del circuito de Circom ìsEqual a un componente y le pasamos dos entradas, una por cada ficha que comparemos.

De esta manera nos aseguramos de que si hay cuatro fichas horizontales consecutivas, tengan el mismo valor. Como ya hemos restringido previamente los valores del tablero a 0, 1 o 2, se podría dar el caso que las cuatro fichas tuviesen el mismo valor pero fuese cero, con lo que no sería una combinación ganadora, sino cuatro celdas vacías.

Para garantizar que el valor de las celdas no sea cero, en las líneas 25, 26 y 27 se pasa el valor de una de las celdas y cero a un circuito isEqual y añadimos la salida (que debe ser un cero para que haya cuatro fichas consecutivas) a la condición de la afirmación if siguiente.

Esta declaración aumentará en uno la variable horizontalWinnery asignará los índices de las fichas consecutivas al array checkedWinningCoordinates.

El circuito implementa esta lógica con las demás orientaciones, para lo cual la única diferencia consiste en editar los índices de las iteraciones y del tablero y, así, hacer referencia a las celdas deseadas para cada orientación.

Para completar el circuito debemos asegurarnos que solamente hay un ganador, que es el ganador que se especifica en la entrada privada y que la combinación ganadora corresponde también con la entrada privada del circuito, como podemos ver en el siguiente código.

Testeado del circuito

Circom también facilita la librería circom_tester que nos permite testear el circuito en lenguaje JavaScript, o TypeScript, mediante la abstracción del circuito utilizando la función wasmTester:

El objetivo del testeo es asegurarnos de que el circuito tenga éxito calculando un testigo a partir de unas entradas válidas (entradas que se corresponden con los valores del tablero) y que no lo tenga cuando las entradas, o al menos una de ellas, no sean válidas.

Por ejemplo, para asegurarnos del éxito del circuito al pasar entradas válidas implementamos el siguiente código en un describe de Mocha y comprobamos la generación del testigo:

Como vemos, este test debería ser exitoso porque solamente hay una combinación ganadora en el tablero, cuyo usuario corresponde al ganador especificado al igual que sus coordenadas, o indices en el array.

Además, se implementan otros tres tests en los que se intenta generar un testigo utilizando inputs inválidos.

Por último, se puede comprobar el resultado del test mediante pnpm run test --filter=circuits.

Generación de archivos

Para obtener el testigo y la prueba en el dispositivo, necesitamos la generación de un archivo binario wasm del circuito y una clave probatoria en formato zkey, que además servirá para la generación del verificador PLONK escrito en Solidity (que utilizaremos para verificar las pruebas desde la aplicación).

El esquema PLONK nos permite producir la clave probatoria sin tener que organizar una ceremonia de configuración confiable (trusted setup ceremony) para obtener valores random que nos permitan establecer un sistema probatorio de conocimiento cero seguro.

Este esquema también necesita de una ceremonia de configuración confiable, en cambio, en vez de ser una específica, se trata de una universal y actualizable.

Puede encontrar más información acerca del esquema PLONK en esta entrada del blog de iden3 y en esta publicación.

En resumen, se pueden utilizar archivos existentes de Perpetual Powers of Tau, en este enlace se listan los de Hermez, y obtener el archivo ptau válido para el número de restricciones que tenga nuestro circuito.

Para generar la clave probatoria también necesitaremos un archivo en formato r1cs (rank-1 constraint system) de nuestro circuito.

Tanto el archivo en formato wasm, para el cálculo del testigo, como el r1cs, se pueden obtener ejecutando el script pnpm run compile (o pnpm run compile --filter=circuits) que utiliza el compilador de circom con unas opciones para la generación de archivos:

El script circom compile mostrará el número de restricciones no lineales:

Para saber qué archivo ptau utilizar podemos empezar utilizando el archivo que soporta un número de restricciones inmediatamente superior al número de restricciones no lineales, es decir ptau para la potencia de 10 (2^10 restricciones como máximo), y pasar a intentar obtener tanto de la clave probatoria como del verificador PLONK.

Para ello utilizaremos el script pnpm run generate, el cual invocará en serie los siguientes scripts:

Al ejecutar este script obtenemos la siguiente salida:

Entiendo que a partir de la versión 0.7.0 de SnarkJS (hasta al menos la actual, es decir, la 0.7.2) se necesita la explicitación de, al menos, una señal pública, sea una entrada pública o la definición de una salida del circuito main, tras una refactorización del template utilizado para la generación de contratos verificadores en lenguaje Solidity.

En caso de no haber ninguna, el argumento con el array de señales públicas en la función verifyProof tendrá asignada una longitud de cero (Array with zero length specified) por defecto.

El archivo ptau elegido de 1024 restricciones se queda corto dado que, como podemos ver arriba sobresaltado, el cómputo hecho en el esquema PLONK para las restricciones da una cuenta de 1050, por lo que utilizaremos la potencia de 11:

Tras editar el script para utilizar el archivo ptau correcto podremos generar con éxito la clave probatoria y el verificador PLONK.

Existe una aplicación web llamada zkREPL que resulta muy útil durante el desarrollo de circuitos dado que nos permite compilar y poner a prueba un circuito en segundos sin instalaciones ni manejo de dependencias.

Contratos inteligentes

Una vez tenemos el contrato verificador, el cual se genera a partir de una plantilla de verificador PLONK de SnarkJS, necesitamos desarrollar un contrato que sirva de enlace entre la aplicación web y el verificador PLONK desplegado.

Es decir, desde nuestro aplicación se llamará a este contrato, el cual a su vez realizará una llamada al verificador. Una vez nuestro contrato obtenga un resultado, emitirá un evento con él, y nuestra interfaz de usuario lo obtendrá para poder mostrarlo.

Como vemos en la función del constructor, a continuación, para poder desplegar este contrato debemos desplegar antes el verificador y pasarle a este contrato su dirección.

De esta manera, cuando necesitemos verificar una prueba nuestro contrato podrá llamar la función verifyProof del verificador, como vemos en la linea 27, para acto seguido emitir un evento con el resultado.

El script de generación del contrato verificador generate:verifier-contract en el espacio de trabajo circuits guarda este contrato en apps/contracts/src.

Despliegue de los contratos

Por último, se despliegan los contratos en la red Sepolia con la finalidad de dar funcionalidad a la aplicación web una vez sea desplegada.

Interfaz de usuario

La simulación del juego se ha implementado en lenguaje TypeScript utilizando Next.js y permite disputar una partida de Conecta Cuatro en tres modalidades, usuario contra modelo de IA, modelo de IA contra usuario y usuario contra usuario. En esta sección explicaré como he desarrollado esta interfaz.

Implementación de la lógica del juego

Al elegir en el menú inicial una modalidad de juego se renderiza o bien el componente UserVsAIBoard o bien el componente UserVsUserBoard. Nos centraremos en el componente UserVsAIBoard para explicar la lógica de la aplicación dado que incluye, además, una sesión de inferencia para predecir una acción en el tablero.

Este componente incluye dos hooks, useAI y useGameOver, para tratar los turnos del modelo de IA y para intentar captar el momento en el que finaliza el juego (ya sea en empate o victoria), respectivamente.

Además, para mostrar el tablero tenemos el componente Board el cual permitirá al usuario formalizar su elección de juego.

El hook useGameOver contiene dos efectos con los que se comprueba, cada vez que cambian sus dependencias, si bien hay un ganador o si hay un empate.

En caso de que se termine el juego se actualiza un estado que persiste en la aplicación mediante Redux Toolkit. El estado contiene el tablero, el status del juego, el modo, turno, número de fichas jugadas y el ganador. De esta manera, se puede obtener el estado en cualquier componente con el hook useAppSelector sin tener que escribir props en cascada.

Durante cada turno del usuario, cada celda del tablero actuará como un botón habilitado cuyo evento al hacer clic consistirá en validar su posición en el tablero y, en el caso de que sea una posición legal para una ficha, se actualizará el tablero en el estado y se cambiará de turno.

Para tratar la lógica de alternancia en turnos consecutivos, en el turno de AI se invoca la función predict en un efecto del hook useAI como podemos ver a continuación:

Esta aplicación hace uso de un modelo ONNX desplegado en la aplicación web que es el resultado de un ejercicio de aprendizaje por refuerzo en el que se ha entrenado un agente DQN para optimizar una red neuronal, con capas convolucionales a la entrada y totalmente conectadas a la salida, que da conformidad a una política de juego para ambos turnos.

He escrito un cuaderno de Jupyter en el que intento explicar, paso a paso, cómo llevar a cabo esta tarea.

getPrediction provee de un índice de columna a partir del cual se calcula el índice de fila donde colocar la ficha. Para obtener esta predicción se utiliza la librería onnxruntime-web la cual permite realizar inferencias en tiempo real desde el dispositivo, utilizando un lenguaje que no es común en el ámbito de las ciencias de datos, como en este caso TypeScript.

Como vimos en el código de useAI arriba, getPrediction es el punto de entrada para crear una sesión de inferencia del modelo. Podemos ver el código de esta función a continuación.

Esta función tiene tres cometidos, (i) obtener una versión del tablero como tensor tipado Float32, (ii) pasárselo a runConnectFourModel para obtener un array con las predicciones del modelo para cada columna y, por último, (iii) asegurarse mediante la función getPredictedValidAction de que de entre todas las acciones que hay en el array se obtiene la opción válida (a partir de la última observación del tablero) con mayor probabilidad de éxito.

Esta última operación se podría evitar e implementar el juego de tal manera que si el modelo hiciese un error y diese mayor margen de éxito a un índice de columna en el que no caben más fichas, dar como terminada la partida y vencedor al jugador contrario.

En nuestro caso, se ha codificado el juego para que se tome la acción válida con mayor probabilidad de entre las predicciones del modelo.

La entrada que admite nuestro modelo tiene las dimensiones [1, 2, 6, 7] haciendo referencia al número de observaciones (batch size), al número de canales de la red convolucional, al espacio de la observación y al espacio de la acción.

Como vemos, para obtener el tensor indicado a partir de la observación de nuestro tablero de dimensiones [6, 7], no solamente debemos añadir una dimensión adicional para el número de muestras, sino que además debemos añadir otra para el número de canales.

El resultado será la transformación del tablero a una doble matriz binaria que indique las posiciones de las fichas de cada jugador.

Por ejemplo, esta transformación se traduciría en convertir el tablero a en los tableros b y c, correspondientes al jugador 1 y al jugador 2, respectivamente:

La lógica para esta transformación en TypeScript se implementa en la función getBoardTensor que consiste en una serie de iteraciones para la concatenación de todos los valores y su posterior conversión al tensor tipado.

Para obtener una inferencia de nuestro modelo ONNX, primero debemos crear la ort.InferenceSession pasándole la ruta al modelo y un objeto de configuración de la sesión, acto seguido se realiza la inferencia.

Por último, obtenemos el índice de la predicción válida de máximo valor en el array de valores de la inferencia del modelo, como vemos abajo en la función getPredictedValidAction:

Generación y verificación de la prueba

Una vez finalizada la partida y siempre y cuando uno de los jugadores haya salido victorioso y el usuario este conectado a la red Sepolia, la aplicación dará la opción al usuario, habilitando el botón Verify, de generar y verificar la prueba de conocimiento cero.

El componente que se renderiza al habilitarse el botón utiliza dos hooks de la librería Wagmi, useBlockNumber para la obtención del número del bloque actual de la red Sepolia y useContractWrite para realizar la transferencia de la prueba al contrato verificador.

El handler del evento al hacer clic en este botón principalmente genera el testigo y la prueba de conocimiento cero mediante la función generateProof y nos devuelve la prueba y un subset del testigo solamente con las señales públicas y la salida. Posteriormente, realiza una transferencia al contrato de verificación con una adaptación de esta información.

La librería SnarkJS nos permite calcular todas las señales públicas del circuito y la prueba en una misma función (fullProve) utilizando las entradas al circuito, el archivo wasm y la clave probatoria, estos dos últimos archivos generados previamente durante la generación de archivos en la sección de circuitos más arriba.

Por último, obtenemos el calldata mediante la función exportSolidityCallData, del cual obtenemos la representación de la prueba y de las señales públicas en hexadecimal para la transferencia al contrato.

Una vez se haya realizado la transferencia y cuando el hook para la obtención del número del bloque ya haya obtenido un resultado, se procede a obtener los eventos emitidos por el contrato:

Si useBlockNumber obtiene un resultado exitoso y devuelve el número del bloque actual, se obtendrán solamente los eventos desde ese bloque en la red Sepolia, en caso contrario se hará desde su génesis (BigInt(0)).

Para obtener estos eventos emitidos he implementado un hook que invoca la función para obtener los eventos del contrato periódicamente cada pollInterval, siempre y cuando se permita mediante la variable de control shouldStopPolling.

En nuestro caso se detendrá la obtención de eventos una vez se haya obtenido el resultado en el evento emitido de nuestra transacción con la prueba o una vez haya expirado un plazo de tiempo.

La lógica de la cuenta atrás consiste simplemente en un efecto con un setTimeout que se configura en 30 segundos:

Finalmente, se mostrará en una ventana modal el resultado obtenido del contrato o un mensaje de error:

Para mejor la experiencia del usuario, la consecución de todas esta serie de acciones es informada al usuario de la aplicación mediante mensajes en toasts en un margen de la pantalla mediante el hook useToast (que podemos encontrar en el espacio de trabajo ui en packages), como podemos ver a continuación en el caso de la obtención de eventos.

API pública

Como comentamos anteriormente, esta aplicación hace uso de un servicio de nodo de Infura para obtener información de la red Sepolia. Así, se consigue evitar errores inducidos por la limitación de peticiones (rate limiting) utilizando solamente el proveedor público.

Para no filtrar al cliente la clave API, que nos provee Infura, se ha implementado una ruta API como función serverless que nos permite insertar la clave en el lado del servidor.

Para ello se configura un jsonRpcProvider en el contexto de Wagmi cuyo endpoint es esta ruta.

Además, tambien se ha editado la configuración de seguridad de la clave mediante el uso de allowlists para elaborar una lista en la que solo se concede acceso al servicio de Infura mediante esta clave si la llamada es a la dirección del contrato.

Cada vez que la aplicación realiza una consulta a la red Sepolia, la petición del jsonRpcProvider será captada por un handler en nuestra ruta API, que enviará una nueva petición, esta vez al endpoint de Infura, ahora sí con la clave PROJECT_ID.

Finalmente, el handler de la ruta API devuelve la respuesta del proveedor de Infura a la petición que inicialmente realiza la librería Viem (que Wagmi utiliza entre bambalinas).

Para hacernos una idea de cómo es el flujo de peticiones al proveedor de Infura tras terminar una partida y generar la prueba para verificarla, vemos a continuación una captura de pantalla con los logs del servidor tras hacer click en Verify:

Vemos que se realizan cinco peticiones en total, la primera para obtener el número del bloque actual (eth_blockNumber), tras la cual se realiza la llamada al contrato para verificar la prueba (eth_call) y por último tres peticiones para obtener los eventos emitidos por el contrato (eth_getLogs).

Primero, podemos comprobar que la URL a la que se dirigen las peticiones es la ruta API que configuramos anteriormente.

Vemos abajo que la petición del bloque nos devuelve el número hexadecimal 0x470259, el cual se corresponde al bloque 4653657.

El payload de la llamada al contrato incluye los argumentos que requiere la función verifyProof del contrato inteligente, es decir la prueba y las señales públicas. La respuesta incluye el resultado 0x, que es simplemente un valor vacío.

Una vez se ha realizado la transacción (cuya llamada al contrato ha resultado en la emisión de un evento ProofVerification) y se ha obtenido un resultado del hook useBlockNumber, se procede a obtener los eventos emitidos desde el número de bloque 4653657.

Las primeras dos peticiones obtienen sendas respuestas con un array vacío, es decir, no contienen eventos:

Por esa razón se realiza una tercera petición, que devuelve un sólo evento.

La aplicación compara el hash de la transacción (transactionHash) que incluye este evento con el hash de la transacción de la llamada al contrato y, al ser el evento indicado, ya no se realizan más peticiones.

En este momento la aplicación muestra un mensaje con el resultado de la verificación. Si hubieran pasado 30 segundos y no se hubiera obtenido el evento correspondiente a la transacción de la verificación de la prueba, no se habrían realizado más peticiones y se habría mostrado un mensaje informando al usuario.

Despliegue de la aplicación

Se ha desplegado esta aplicación web en Vercel y se puede acceder a ella en este enlace. Si desea aprender a desplegar un monorepositorio de Turborepo en Vercel encontrará información en este artículo.