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 “K Ethereum Virtual Machine” (KEVM), una versión “correcta 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, “correcta 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 ‘conectar 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 “có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.