馃嚜馃嚫 Visi贸n general de KEVM

:es: Traducci贸n al espa帽ol de Virtual Machines - KEVM overview por Rodrigo.

Publicado en cardano.org.


A medida que Cardano prospera y evoluciona, la red est谩 ampliando su alcance e interoperabilidad, creando nuevas v铆as de cooperaci贸n. Ahora estamos abriendo las puertas de Cardano a la comunidad de Solidity/Ethereum, a trav茅s de una plataforma compatible e interoperable usando su c贸digo nativo.

Tal framework crear谩 un puente permanente que permitir谩 a los desarrolladores trabajar sin problemas en ambos ecosistemas, ahora y en el futuro. Para ello, estamos reiniciando y acelerando el programa 鈥淜 Ethereum Virtual Machine鈥 (KEVM), una versi贸n 鈥渃orrecta por construcci贸n鈥 de la M谩quina Virtual de Ethereum (EVM) especificada en el framework K.

El framework K es una plataforma sem谩ntica utilizada para crear lenguajes de programaci贸n y m谩quinas virtuales formalmente verificadas. K permite a los desarrolladores definir o implementar la sem谩ntica formal de un lenguaje de programaci贸n de forma intuitiva y modular. K tambi茅n genera una m谩quina virtual ejecutable, 鈥渃orrecta por construcci贸n鈥 a partir de su especificaci贸n formal, que es lo suficientemente r谩pida y potente para ejecutar programas reales y contratos inteligentes. A largo plazo, en asociaci贸n con nuestros amigos de Runtime Verification, queremos construir un entorno K en el que podamos 鈥榗onectar y usar鈥 nuevas m谩quinas virtuales.

En este enlace, los desarrolladores que deseen utilizar KEVM encontrar谩n informaci贸n e instrucciones. Permite a los desarrolladores experimentar con cualquier contrato inteligente que pueda ser ejecutado en la EVM, y ofrece una mejor seguridad y rendimiento. K es un medio para verificar formalmente el software, de modo que el c贸digo puede ser comprobado autom谩ticamente en busca de cualquier defecto, y se puede probar que funciona exactamente como deber铆a.

Esperamos tu apoyo y tus comentarios. Si deseas unirte al programa de desarrolladores dedicados de KEVM, por favor, rellena nuestra breve encuesta y nos pondremos en contacto contigo a su debido tiempo.

Raz贸n de la KEVM

El devnet de KEVM se basa en el framework K, un sistema para especificar los lenguajes y las m谩quinas virtuales, y luego derivar herramientas para estos lenguajes, como int茅rpretes, verificadores de tipos, verificadores de equivalencia y depuradores. Puede utilizarse para crear herramientas de an谩lisis tanto est谩ticas como din谩micas.

KEVM es una especificaci贸n de la EVM (M谩quina Virtual de Ethereum) en K.

KEVM tambi茅n es un int茅rprete para EVM, derivado autom谩ticamente de la especificaci贸n de KEVM. Se podr铆a decir que la especificaci贸n K de EVM es el 鈥渃贸digo fuente鈥 del int茅rprete. Pero es mucho m谩s que eso. KEVM puede ser usado para probar que los contratos inteligentes son correctos. Esto se hace especificando las propiedades deseadas de un contrato en K, combinando el contrato con la especificaci贸n KEVM, y luego usando el framework K para verificar esas propiedades. KEVM puede utilizarse para comprobar errores como los sobreflujos y subflujos de enteros, los sobreflujos y subflujos de pilas, la salida de gas, y otras propiedades gen茅ricas del contrato. Tambi茅n puede verificar propiedades m谩s espec铆ficas para contratos concretos.

Cuando ejecutas un contrato inteligente en la devnet usando la billetera de la devnet, la devnet enviar谩 el contrato al int茅rprete de KEVM para ser ejecutado. Este int茅rprete es la 煤nica parte de la devnet que se basa en el framework K. Pero debido a que el int茅rprete se genera a partir de la especificaci贸n K, puedes usar K (y KEVM) para verificar tus contratos inteligentes antes de enviarlos a la devnet. En este sentido, la devnet est谩 relacionada con todo el framework K.

Usando la Devnet de KEVM

KEVM es una m谩quina virtual de contrato inteligente de alta calidad, formalmente verificada. La devnet de KEVM se implementa en Mantis, el cliente de Ethereum Classic que cumple con los est谩ndares y que ha sido dise帽ado dentro de las especificaciones del framework K. La especificaci贸n K define la sem谩ntica formal de elementos como la configuraci贸n y las reglas de transici贸n de la EVM. El framework K proporciona la plataforma dentro de la cual trabajar y tambi茅n proporciona un ejecutable.

KEVM es una m谩quina basada en pilas, en contraposici贸n a una m谩quina basada en registros. La principal diferencia entre estas dos arquitecturas est谩 en la forma en que los operandos y sus resultados se almacenan y recuperan.

Para ponerlo en marcha es necesario instalar Mazo y empezar a compilar los contratos inteligentes. Luego puedes empezar a experimentar e identificar cualquier punto d茅bil en tus contratos inteligentes.

Conjunto de habilidades requeridos para usar la Devnet

Para usar el dispositivo KEVM se requieren las siguientes habilidades:

  • Familiaridad con la escritura de contratos inteligentes en Solidity. Necesitar谩s un conjunto de contratos inteligentes bien definidos para usarlos en la devnet.
  • Conocimiento avanzado del protocolo de llamada de procedimiento remoto JSON (RPC).
    No es necesario registrarse para usar la devnet.
1 Like