A diferencia de la mayoría de los lenguajes de programación, las expresiones de Simplicity se construyen a partir de una serie de combinadores, que arman expresiones a partir de otras más pequeñas. Estas expresiones representan funciones que toman una entrada y la convierten en una salida.Este es el programa de Simplicity más simple:

main := iden
Este programa toma una entrada vacía y produce una salida vacía. Hagamos algo más interesante tomando un bit e invirtiéndolo:

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

Aquí la expresión final de Simplicity es nuestra función main (principal). Leyendo de abajo hacia arriba, podemos ver que es la composición de varias funciones más pequeñas, que acaban conectándose en combinadores unit (unitarios). Los combinadores unitarios producen una salida vacía. Junto con iden, que toma una entrada arbitraria y la devuelve sin cambios, y witness (testigo), que devuelve un valor proporcionado externamente, los combinadores de unidades forman la base de toda expresión de Simplicity.En este fragmento de código, proporcionamos anotaciones de tipo para indicar qué datos fluyen de cada parte de la expresión a la siguiente. Aquí “1” representa el tipo de unidad, que es a lo que nos hemos estado refiriendo como “salida vacía”. “2” representa un bit, que podría tomar el valor de 0 o 1.No se preocupe si no siguió este fragmento en detalle. Solo lo usamos para mostrar visualmente el aspecto del código de Simplicity. Más adelante en esta publicación, analizaremos un programa más interesante con más atención.

Un lenguaje de especificación

En última instancia, todos los lenguajes de programación expresan la idea de combinar cálculos para construir otros mayores. Bitcoin Script (como Forth o PostScript) hace esto con una máquina de pila, en la que cada computación manipula una lista de objetos de datos sucesivamente. EVM de Ethereum usa una arquitectura de llamada a funciones en la que el código puede llamar a otros bloques de código (posiblemente en otros contratos), que toman datos como entrada y devuelven datos como salida. Este también es el modelo usado por casi todos los lenguajes de programación predominantes hoy en día.

Los lenguajes de programación usan efectos secundarios para interactuar con el mundo exterior, como la transacción que se está gastando. En EVM, los contratos también tienen acceso a bases de datos clave-valor, que les permiten mantener el estado a través de las transacciones sin pasarlo explícitamente.

Tanto en Bitcoin Script como en EVM, la inversión de bits puede hacerse con un único código de operación (la versión Bitcoin puede tomar muchas entradas diferentes, la mayoría de las cuales no se parecen a bits, mientras que la versión EVM actúa como bits pero siempre sobre 256 bits a la vez). Es razonable preguntar por qué el modelo de Simplicity conduce a tanta verbosidad para cosas tan simples.

Nuestro objetivo con Simplicity es especificar formalmente la semántica de los programas, tanto en lo que respecta a qué funciones representan como a qué recursos computacionales intervienen en su evaluación. Podría ser posible, en principio, especificar formalmente un lenguaje que opere como Bitcoin Script o EVM, pero la tarea sería extremadamente difícil, y el resultado sería casi igual de difícil de verificar. En su lugar, con Simplicity, definimos un pequeño conjunto de combinadores básicos, cada uno de los cuales refleja una manera matemáticamente fundamental de combinar funciones. La semántica del lenguaje resultante es tan pequeña que entraría en una camiseta.

En la práctica, para las cosas como la inversión de bits, este código solo se escribirá una vez y luego se reutilizará. De hecho, lo hemos escrito por usted y lo hemos integrado en el lenguaje. Al escribir su propio código, simplemente puede usar el atajo jet_not en lugar del código anterior. Hablaremos más sobre los jets en la próxima sección.

Al final, en la práctica, casi nadie escribirá el código de Simplicity. Simplicity proporciona una base bien definida para los programas de blockchain, pero es simplemente eso: una base. El verdadero trabajo se hará en lenguajes de alto nivel, que se compilarán en código de Simplicity junto con pruebas de su correcto funcionamiento.

Programas contra expresiones

Las expresiones que tienen valores de entrada y salida triviales tienen un nombre especial. Llamamos a estas expresiones programas. Desde el punto de vista matemático, solo existe una función que asigne una entrada trivial a una salida trivial, por lo que no es obvio que tales expresiones de simplicidad sean útiles en absoluto. Pero no solo son útiles, ¡sino que son las únicas expresiones de este tipo permitidas en la blockchain!

Entonces, ¿cuál es la estrategia? En realidad, hay dos: una es que los programas de Simplicity asignados en direcciones tienen espacios vacíos en ellos que solo se llenan cuando las monedas realmente se gastan; la otra es que los programas de Simplicity tienen efectos secundarios que les permiten acceder a los datos de la blockchain o abortar de forma temprana, saliendo así de los límites de las funciones matemáticas puras.

Hay dos maneras de especificar espacios vacíos en los programas de Simplicity: los combinadores de disconnect (desconectar) y witness (testigo). El combinador disconnect es un poco sutil, y hemos hablado de él en el pasado. Pero los testigos son muy simples: el combinador witness devuelve un valor de un tipo dado, denominado witness (como una firma digital, una preimagen hash o una opción específica de claves de firma).

También hay dos maneras en las que Simplicity soporta efectos secundarios: una es mediante la introspección de los datos de la transacción (de lo que también hablaremos más en un artículo posterior), y la otra es mediante aserciones. Las aserciones detienen la ejecución del programa. En Bitcoin Script, el código de operación VERIFY (VERIFICAR) se usa para las aserciones y permite que el programa falle si encuentra una firma u otros datos inválidos. EVM usa el código de operación STOP (DETENER) con el mismo fin.

Ahora podemos ver cómo un programa cuyos tipos de entrada y salida son nominalmente triviales puede realmente efectuar un cálculo útil: los testigos cumplen la función de entradas del programa, mientras que las aserciones proporcionan una salida “aprobado (pass)/no aprobado (fail)" del programa.

Consideremos otro ejemplo. Este es un programa que toma dos testigos y verifica si son iguales:

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

Podemos leer este programa de abajo hacia arriba: el programa en sí es una única expresión denominada main (principal), de tipo 1->1. Aquí, el “tipo” de una expresión indica qué tipo de valores toma como entrada y salida. El tipo 1 solo tiene un único valor, por lo que no describe información. El tipo 2 tiene dos valores posibles, por lo que puede representar un único bit, 2^32 es una cadena de 32 bits, y así sucesivamente.

A partir de la igualdad de abajo, vemos que main es la composición de las expresiones con los nombres cp3 y jt4. Entonces, cp3 es la composición de pr1 y jt2, y así sucesivamente. Se usan cinco combinadores en este programa:

• comp, o composición, toma dos expresiones y evalúa la segunda con la salida de la primera como entrada.
  
• pair (par) toma dos expresiones y produce una nueva expresión cuya salida es un par de valores: la parte de la izquierda es la salida de la primera expresión, y la parte de la derecha es la salida de la segunda.
  
• witness no toma ninguna entrada pero tiene un tipo polimórfico como su salida: su tipo es cualquier tipo que sea necesario para que el programa tenga sentido. Y el valor que arroja es uno proporcionado en el momento de evaluación.
  
• jet_eq_32 es un jet, lo que significa que es un único combinador que reemplaza una expresión de Simplicity más grande. La expresión reemplazada se llama su especificación, y un intérprete de Simplicity puede evaluar el jet evaluando la especificación o usando código máquina optimizado que tenga el mismo efecto. Este jet en particular toma dos valores de 32 bits y emite un único bit, que indica si los dos valores fueron iguales (1) o desiguales (0).
• jet_verify también es un jet. Este toma un único bit como entrada, y si ese bit es 0, aborta el programa. No tiene salida.

Conclusión

Esta es una entrada de blog pesada en la que vimos qué aspecto tiene el código de Simplicity y observamos que incluso las funcionalidades que parecen sencillas pueden parecer bastante complejas cuando se escriben explícitamente. Pero esta complejidad refleja lo que realmente está sucediendo adentro. Como lenguaje de especificación, Simplicity nos permite hacerlo todo explícito, de modo que podamos modelarlo matemáticamente, demostrar las propiedades esenciales que necesitamos para nuestras aplicaciones y, a continuación, encapsularlo, con la seguridad de que tenemos una base sólida como una roca para las cosas que creemos sobre nuestro código.

Simplicity tiene muchos más combinadores y muchos jets, de los que hablaremos en futuros artículos. A medida que desarrollemos el lenguaje, exploraremos más ejemplos prácticos y veremos qué significa “probar” propiedades de programas.

Mi próxima entrada presentará el concepto de compartir, que permite fusionar dos expresiones idénticas en una, e introduce algunas sutilezas relacionadas con lo que significa ser “idéntico”.

Únase a la conversación sobre Simplicity en GitHub para hacer preguntas, conectarse con la comunidad y compartir sus ideas. Y síganos en @blksresearch en Twitter para mantenerse al día sobre las últimas publicaciones de entradas en el blog de Simplicity.