La mise à niveau du P-Token récemment déployée par Solana représente l'un des changements d'infrastructure les plus importants dans l'histoire du réseau. Cette mise à niveau réduit considérablement les ressources informatiques nécessaires aux opérations sur les jetons tout en préservant la compatibilité avec le programme de jetons SPL existant.
Pour valider cette affirmation, la Solana Foundation a engagé Certora pour effectuer une vérification formelle afin de prouver l'équivalence comportementale entre l'ancienne implémentation du jeton SPL et le nouveau programme P-Token basé sur Pinocchio. La société de recherche et développement Anza a précédemment décrit la vérification formelle comme "la garantie la plus forte" de l'équivalence de P-Token, et les résultats de Certora fournissent une validation supplémentaire du rôle de P-Token en tant que remplacement "drop-in" pour l'un des programmes les plus largement utilisés par Solana.
L'importance du programme de tokens
Le programme de jetons SPL est au centre de l'économie des jetons de Solana. Il gère la création de jetons, la gestion des comptes de jetons, les transferts, les brûlures et la délégation pour la grande majorité des actifs sur le réseau. Étant donné que presque toutes les transactions sans droit de vote sur Solana interagissent avec des jetons sous une forme ou une autre, tout changement apporté au programme de jetons a de vastes implications pour l'écosystème.
P-Token introduit une nouvelle implémentation basée sur la bibliothèque Pinocchio Rust. Cette mise à jour apporte des améliorations substantielles en termes de performances, réduisant la consommation de calcul d'environ 95 à 98 % pour de nombreuses opérations courantes. Les transferts de jetons standard, par exemple, passent de 4 645 unités de calcul à seulement 76, tandis que les instructions transfer_checked passent de 6 200 unités de calcul à 105.
Ces gains d'efficacité peuvent libérer environ 12 à 13 % de l'espace des blocs sur le réseau, créant ainsi une capacité supplémentaire sans augmenter les limites de blocs.
Le défi de prouver qu'il s'agit d'une solution de remplacement "prête à l'emploi"
Si les améliorations de performance attirent l'attention, la compatibilité reste l'exigence la plus importante pour une mise à niveau de l'infrastructure de cette ampleur. Les portefeuilles, dApps, protocoles et contrats intelligents existants s'appuient sur le comportement du programme de jetons SPL. Toute déviation inattendue pourrait causer des problèmes d'intégration ou poser des risques pour les développeurs et les utilisateurs.
P-Token ne se contente pas de copier la base de code originale. La nouvelle implémentation adopte une architecture différente, y compris un accès au compte sans copie, des chemins d'exécution optimisés et des fonctionnalités supplémentaires. Par conséquent, les développeurs ne pouvaient pas se fier uniquement aux tests conventionnels pour établir la compatibilité.
Certora a utilisé des techniques de vérification formelle pour analyser mathématiquement si les deux programmes se comportent de la même manière pour toutes les entrées possibles dans le périmètre de vérification défini.
Que signifie l'équivalence pour P-Token ?
Le cadre de vérification de Certora a évalué trois catégories de résultats pour chaque instruction analysée.
-
Premièrement, aucun programme ne doit jamais paniquer pendant l'exécution, c'est-à-dire que le programme ne doit jamais se bloquer ou s'interrompre à cause d'un bug, d'un cas de figure, etc.
-
Deuxièmement, si le programme SPL Token traite avec succès une instruction et renvoie Ok(()), P-Token doit également renvoyer Ok(()). Dans ce cas, les deux programmes doivent laisser les données du compte dans un état identique octet par octet après l'exécution.
-
Troisièmement, si P-Token renvoie une erreur, le programme SPL Token doit renvoyer la même erreur dans les mêmes conditions.
Le cadre de Certora garantit que pour chaque état de compte et instruction d'entrée possible, le programme réussit (Ok(())) ou échoue gracieusement (Err(e)), mais ne se bloque jamais en interne. La mise en œuvre de P-Token est conçue comme un surensemble de la fonctionnalité de SPL Token, ce qui signifie que toute opération acceptée par SPL Token doit également être acceptée par P-Token.
L'effort de vérification a permis d'identifier plusieurs différences délibérées entre les deux programmes. P-Token permet l'auto-révocation des délégués, ce qui permet à un délégué de révoquer sa propre autorité sans que le propriétaire du compte du jeton n'ait à signer la transaction. Le jeton SPL nécessite la signature du propriétaire pour la même action.
P-Token étend également la prise en charge des autorités multisig Token-2022. Alors que SPL Token rejette ces comptes, P-Token les accepte.
Une troisième différence concerne la gestion des erreurs lorsque des données de compte malformées contiennent des balises COption non canoniques. SPL Token rejette immédiatement ces comptes avec une erreur InvalidAccountData. Le processus optimisé de chargement des comptes de P-Token va plus loin dans la logique de l'instruction avant de générer une erreur, ce qui peut produire des résultats différents en fonction de l'instruction exécutée.
Ces différences étant intentionnelles et documentées, Certora a incorporé des hypothèses dans certaines parties du processus de vérification afin que l'analyse reste centrée sur la limite de compatibilité convenue.
Comment la vérification a fonctionné
Le Prover de Certora analyse le code source après la compilation dans une représentation intermédiaire de bas niveau. Les ingénieurs écrivent ensuite des spécifications formelles en utilisant le langage de vérification Certora pour Rust, connu sous le nom de CVLR.
Le harnais de vérification a créé des copies identiques des informations de compte et des données d'instruction, ce qui a permis au prouveur de comparer les deux programmes dans les mêmes conditions. En utilisant les techniques de Satisfiability Modulo Theories, le système a évalué simultanément toutes les entrées possibles plutôt que de s'appuyer sur une collection limitée de cas de test.
Le champ d'application comprenait toutes les instructions partagées entre SPL Token et P-Token, à l'exclusion de AmountToUiAmount et UiAmountToAmount. L'examen a également exclu les trois nouvelles instructions spécifiques au P-Token : batch, unwrap_lamports et withdraw_excess_lamports.
Tout au long du processus, le prouveur a soit généré une preuve de correction, soit produit des contre-exemples concrets mettant en évidence les différences de comportement nécessitant une révision.
Constatations et résultats
Certora a indiqué qu'aucune vulnérabilité exploitable n'est apparue au cours de l'effort de vérification. L'analyse a confirmé que les propriétés No Panics et Equivalence on Ok sont valables pour toutes les instructions concernées sans nécessiter d'hypothèses supplémentaires. La propriété Equivalence on Error est également valable pour l'ensemble des instructions partagées lorsque l'on tient compte des trois différences de comportement intentionnelles identifiées précédemment.
Plus important encore, la vérification a démontré que lorsque les deux programmes traitent avec succès la même entrée, ils produisent des états de compte post-opération identiques octet par octet. Le processus a également mis en évidence la manière dont la vérification formelle peut mettre en évidence des cas limites que les tests traditionnels risquent de manquer.
Une étape importante pour Solana Infrastructure
Les résultats de la vérification arrivent peu de temps après le déploiement de P-Token sur le réseau principal, ce qui renforce la confiance dans l'une des mises à niveau les plus importantes de l'infrastructure de Solana.
En combinant d'importantes économies de calcul avec une équivalence comportementale formellement vérifiée, la mise à niveau cherche à améliorer l'efficacité du réseau sans perturber les applications et les actifs qui dépendent du programme de jetons tous les jours.
En savoir plus sur SolanaFloor
Solana obtient enfin des abonnements Onchain natifs, débloquant les salaires, les budgets des agents AI et la facturation récurrente
Noble Mobile de l'ancien candidat à la présidence des États-Unis Andrew Yang acquiert Helium Mobile - Qu'advient-il de $HNT ?
Comment l'introduction en bourse de SpaceX, d'une valeur de 2 milliards de dollars, affectera-t-elle les crypto-monnaies ?
