Certora verifica formalmente la actualización del token P de Solana como equivalente al token SPL

La reciente actualización del P-Token de Solana representa uno de los cambios de infraestructura más importantes de la historia de la red. La actualización reduce drásticamente los recursos informáticos necesarios para las operaciones con tokens, al tiempo que mantiene la compatibilidad con el actual programa de tokens SPL.

Para validar esta afirmación, la Fundación Solana encargó a Certora una verificación formal que demostrara la equivalencia de comportamiento entre la implementación del token SPL heredado y el nuevo programa P-Token basado en Pinocchio. La empresa de investigación y desarrollo Anza ha descrito previamente la verificación formal como "la garantía más sólida" de la equivalencia de P-Token, y los resultados de Certora proporcionan una validación adicional del papel de P-Token como sustituto "inmediato" de uno de los programas más utilizados de Solana.

Por qué es importante el programa de tokens

El programa de tokens SPL se sitúa en el centro de la economía de tokens de Solana. Se encarga de la creación de fichas, la gestión de cuentas de fichas, las transferencias, las quemaduras y la delegación para la gran mayoría de los activos de la red. Dado que casi todas las transacciones sin derecho a voto en Solana interactúan con los tokens de alguna forma, cualquier cambio en el programa de tokens tiene amplias implicaciones para el ecosistema.

P-Token introduce una nueva implementación basada en la biblioteca Pinocchio Rust. La actualización ofrece mejoras sustanciales en el rendimiento, reduciendo el consumo de computación en aproximadamente un 95-98% para muchas operaciones comunes. Las transferencias estándar de tokens, por ejemplo, pasan de 4.645 unidades de cálculo a sólo 76, mientras que las instrucciones transfer_checked disminuyen de 6.200 unidades de cálculo a 105.

Se calcula que este aumento de la eficiencia puede liberar entre un 12% y un 13% del espacio de bloques de la red, creando capacidad adicional sin aumentar los límites de bloques.

El reto de demostrar que es un sustituto "listo para usar

Aunque las mejoras de rendimiento atraen la atención, la compatibilidad sigue siendo el requisito más importante para una actualización de infraestructura de esta escala. Los monederos, dApps, protocolos y contratos inteligentes existentes dependen del comportamiento del programa SPL Token. Cualquier desviación inesperada podría causar problemas de integración o plantear riesgos para desarrolladores y usuarios.

P-Token no se limita a copiar el código base original. La nueva implementación adopta una arquitectura diferente, incluido el acceso a la cuenta de copia cero, rutas de ejecución optimizadas y funcionalidad adicional. Como resultado, los desarrolladores no podían confiar únicamente en las pruebas convencionales para establecer la compatibilidad.

En su lugar, Certora utilizó técnicas de verificación formal para analizar matemáticamente si los dos programas se comportaban de la misma manera en todas las entradas posibles dentro del ámbito de verificación definido.

¿Qué significa equivalencia para P-Token?

El marco de verificación de Certora evaluó tres categorías de resultados para cada instrucción analizada.

• En primer lugar, ninguno de los programas debe entrar en pánico durante la ejecución; es decir, el programa nunca debe bloquearse o abortar debido a un error, caso extremo, etc.

• En segundo lugar, si el programa SPL Token procesa con éxito una instrucción y devuelve Ok(()), P-Token también debe devolver Ok(()). En estos casos, ambos programas deben dejar los datos de la cuenta en un estado idéntico byte a byte después de la ejecución.

• En tercer lugar, si P-Token devuelve un error, el programa SPL Token debe devolver el mismo error en las mismas condiciones.

El marco de trabajo de Certora garantiza que, para cada estado de cuenta e instrucción de entrada posibles, el programa tenga éxito (Ok(()) o falle con elegancia (Err(e)), pero nunca se bloquee internamente. La implementación de P-Token está diseñada como un superconjunto de la funcionalidad de SPL Token, lo que significa que cualquier operación aceptada por SPL Token también debe ser aceptada por P-Token.

El esfuerzo de verificación identificó varias diferencias deliberadas entre los dos programas. P-Token permite la autorrevocación delegada, lo que permite a un delegado revocar su propia autoridad sin necesidad de que el propietario de la cuenta de token firme la transacción. SPL Token requiere la firma del propietario para la misma acción.

P-Token también amplía la compatibilidad con las autoridades multisig de Token-2022. Mientras que SPL Token rechaza estas cuentas, P-Token las acepta.

Una tercera diferencia tiene que ver con la gestión de errores cuando los datos de cuenta malformados contienen etiquetas COption no canónicas. SPL Token rechaza inmediatamente estas cuentas con un error InvalidAccountData. El proceso optimizado de carga de cuentas de P-Token profundiza en la lógica de la instrucción antes de generar un error, lo que puede producir resultados diferentes en función de la instrucción que se esté ejecutando.

Dado que estas diferencias eran intencionadas y estaban documentadas, Certora incorporó suposiciones en partes del proceso de verificación para mantener el análisis centrado en el límite de compatibilidad acordado.

Cómo funcionó la verificación

El Prover de Certora analiza el código fuente después de la compilación en una representación intermedia de bajo nivel. A continuación, los ingenieros escriben especificaciones formales utilizando el lenguaje de verificación de Certora para Rust, conocido como CVLR.

El arnés de verificación creó copias idénticas de la información de cuentas y los datos de instrucciones, lo que permitió al prover comparar ambos programas en las mismas condiciones. Utilizando técnicas de Satisfiability Modulo Theories, el sistema evaluó todas las entradas posibles simultáneamente en lugar de basarse en una colección limitada de casos de prueba.

El alcance incluyó todas las instrucciones compartidas entre SPL Token y P-Token, excluyendo AmountToUiAmount y UiAmountToAmount. La revisión también excluyó las tres nuevas instrucciones específicas de P-Token: batch, unwrap_lamports y withdraw_excess_lamports.

A lo largo del proceso, el prover generó una prueba de corrección o produjo contraejemplos concretos que destacaban las diferencias de comportamiento que requerían revisión.

Conclusiones y resultados

Certora informó de que no surgieron vulnerabilidades explotables durante el esfuerzo de verificación. El análisis confirmó que las propiedades "No Panics" y " Equivalence on Ok" se mantienen en todas las instrucciones del ámbito de aplicación sin necesidad de suposiciones adicionales. La propiedad de equivalencia en caso de error también se mantiene en todo el conjunto de instrucciones compartidas cuando se tienen en cuenta las tres diferencias de comportamiento intencionadas identificadas anteriormente.

Y lo que es más importante, la verificación demostró que siempre que ambos programas procesan con éxito la misma entrada, producen byte a byte idénticos estados de cuenta tras la operación. El proceso también puso de relieve cómo la verificación formal puede descubrir casos extremos que las pruebas tradicionales pueden pasar por alto.

Un hito importante para Solana Infrastructure

Los resultados de la verificación llegan poco después del despliegue de P-Token en la red principal, lo que proporciona una confianza adicional en una de las actualizaciones de infraestructura más importantes de Solana.

Mediante la combinación de un importante ahorro informático con una equivalencia de comportamiento formalmente verificada, la actualización pretende mejorar la eficiencia de la red sin interrumpir las aplicaciones y los activos que dependen del programa de tokens cada día.

Más información sobre SolanaFloor

Solana finalmente obtiene suscripciones Onchain nativas, desbloqueando nóminas, presupuestos de agentes de IA y facturación recurrente
Noble Mobile, del ex candidato presidencial estadounidense Andrew Yang, adquiere Helium Mobile - ¿Qué pasa con $HNT?

¿Cómo afectará a las criptomonedas la OPV de 2T$ de SpaceX?