Certora verifieert officieel Solana's P-Token Upgrade als gelijkwaardig aan SPL Token

Solana's onlangs geïmplementeerde P-Token upgrade is een van de belangrijkste infrastructuurveranderingen in de geschiedenis van het netwerk. De upgrade vermindert drastisch de computermiddelen die nodig zijn voor tokenoperaties terwijl de compatibiliteit met het bestaande SPL Token-programma behouden blijft.

Om deze bewering te valideren heeft de Solana Foundation Certora in de arm genomen om een formele verificatie uit te voeren om gedragsgelijkwaardigheid aan te tonen tussen de bestaande SPL Token implementatie en het nieuwe Pinocchio gebaseerde P-Token programma. Onderzoeks- en ontwikkelingsfirma Anza heeft de formele verificatie eerder beschreven als "de sterkste garantie" voor de gelijkwaardigheid van P-Token, en de resultaten van Certora bieden een verdere validatie voor de rol van P-Token als een "drop-in" vervanging voor een van Solana's meest gebruikte programma's.

Waarom het Token-programma belangrijk is

Het SPL Token programma vormt het centrum van Solana's tokeneconomie. Het zorgt voor de creatie van munten, het beheer van tokenaccounts, transfers, burns en delegatie voor de overgrote meerderheid van de activa op het netwerk. Omdat bijna elke niet-stemgerechtigde transactie op Solana op de een of andere manier met tokens te maken heeft, heeft elke verandering in het tokenprogramma brede implicaties voor het ecosysteem.

P-Token introduceert een nieuwe implementatie gebouwd op de Pinocchio Rust bibliotheek. De upgrade levert aanzienlijke prestatieverbeteringen op en vermindert het rekenverbruik met ongeveer 95-98% voor veel voorkomende bewerkingen. Standaard token transfers, bijvoorbeeld, dalen van 4.645 rekeneenheden naar slechts 76, terwijl transfer_checked instructies dalen van 6.200 rekeneenheden naar 105.

Deze efficiëntiewinst kan naar schatting 12-13% van de blokruimte op het netwerk vrijmaken, waardoor extra capaciteit wordt gecreëerd zonder de bloklimieten te verhogen.

De uitdaging om een "Drop-In" vervanging te bewijzen

Hoewel prestatieverbeteringen de aandacht trekken, blijft compatibiliteit de belangrijkste vereiste voor een infrastructuurupgrade van deze omvang. Bestaande wallets, dApps, protocollen en smart contracts vertrouwen op het gedrag van het SPL Token programma. Elke onverwachte afwijking kan integratieproblemen veroorzaken of risico's opleveren voor ontwikkelaars en gebruikers.

P-Token kopieert niet simpelweg de originele codebase. De nieuwe implementatie gebruikt een andere architectuur, inclusief zero-copy accounttoegang, geoptimaliseerde uitvoeringspaden en extra functionaliteit. Als gevolg hiervan konden ontwikkelaars niet alleen vertrouwen op conventionele testen om compatibiliteit vast te stellen.

In plaats daarvan gebruikte Certora formele verificatietechnieken om wiskundig te analyseren of de twee programma's zich op dezelfde manier gedragen bij alle mogelijke invoer binnen het gedefinieerde verificatiebereik.

Wat betekent gelijkwaardigheid voor P-Token?

Certora's verificatie raamwerk evalueerde drie uitkomstcategorieën voor elke geanalyseerde instructie.

• Ten eerste mag geen van beide programma's ooit in paniek raken tijdens de uitvoering; d.w.z. het programma mag nooit crashen of afbreken als gevolg van een bug, edge case, enz.

• Ten tweede, als het SPL Token programma met succes een instructie verwerkt en Ok()) retourneert, moet P-Token ook Ok()) retourneren. In die gevallen moeten beide programma's accountgegevens in een byte-voor-byte identieke staat achterlaten na uitvoering.

• Ten derde, als P-Token een fout teruggeeft, moet het SPL Token programma dezelfde fout teruggeven onder dezelfde omstandigheden.

Certora's raamwerk zorgt ervoor dat voor elke mogelijke input account status en instructie, het programma ofwel slaagt (Ok()) of netjes faalt (Err(e)), maar nooit intern crasht. De implementatie van P-Token is ontworpen als een superset van SPL Token functionaliteit, wat betekent dat elke bewerking die door SPL Token wordt geaccepteerd ook door P-Token moet worden geaccepteerd.

Tijdens de verificatie werden verschillende opzettelijke verschillen tussen de twee programma's geïdentificeerd. P-Token staat delegate self-revocation toe, waardoor een delegate zijn eigen autoriteit kan intrekken zonder dat de eigenaar van de tokenrekening de transactie hoeft te ondertekenen. SPL Token vereist de handtekening van de eigenaar voor dezelfde actie.

P-Token breidt ook de ondersteuning voor Token-2022 multisig autoriteiten uit. Terwijl SPL Token deze accounts weigert, accepteert P-Token ze wel.

Een derde verschil betreft de foutafhandeling wanneer misvormde accountgegevens niet-canonieke COption-tags bevatten. SPL Token weigert zulke accounts onmiddellijk met een InvalidAccountData foutmelding. Het geoptimaliseerde accountlaadproces van P-Token reikt dieper in de instructielogica voordat een fout wordt gegenereerd, wat verschillende resultaten kan opleveren afhankelijk van de instructie die wordt uitgevoerd.

Omdat deze verschillen opzettelijk waren en gedocumenteerd, nam Certora aannames op in delen van het verificatieproces om de analyse gericht te houden op de overeengekomen compatibiliteitsgrens.

Hoe de verificatie werkte

De Prover van Certora analyseert de broncode na compilatie in een tussenrepresentatie op laag niveau. Engineers schrijven vervolgens formele specificaties met behulp van de Certora Verification Language for Rust, bekend als CVLR.

Het verificatieharnas maakt identieke kopieën van accountinformatie en instructiedata, waardoor de prover beide programma's onder dezelfde omstandigheden kan vergelijken. Met behulp van Satisfiability Modulo Theories-technieken evalueerde het systeem alle mogelijke invoer tegelijkertijd in plaats van te vertrouwen op een beperkte verzameling testgevallen.

Het toepassingsgebied omvatte elke instructie die gedeeld werd tussen SPL Token en P-Token, met uitzondering van AmountToUiAmount en UiAmountToAmount. De review omvatte ook niet de drie nieuwe P-Token specifieke instructies: batch, unwrap_lamports en withdraw_excess_lamports.

Gedurende het hele proces genereerde de prover ofwel een bewijs van juistheid of produceerde concrete tegenvoorbeelden die gedragsverschillen benadrukten die herzien moesten worden.

Bevindingen en resultaten

Certora rapporteerde dat er geen exploiteerbare kwetsbaarheden naar voren kwamen tijdens de verificatie. De analyse bevestigde dat de eigenschappen No Panics en Equivalence on Ok gelden voor alle instructies binnen het toepassingsgebied zonder dat aanvullende aannames nodig zijn. De Equivalence on Error-eigenschap geldt ook voor de gedeelde instructieset wanneer rekening wordt gehouden met de drie opzettelijke gedragsverschillen die eerder zijn geïdentificeerd.

Het belangrijkste is dat de verificatie aantoonde dat wanneer beide programma's met succes dezelfde invoer verwerken, ze byte-voor-byte identieke post-operatie account states produceren. Het proces liet ook zien hoe formele verificatie randgevallen kan blootleggen die traditionele tests mogelijk over het hoofd zien.

Een belangrijke mijlpaal voor Solana Infrastructuur

De verificatieresultaten komen kort na de implementatie van P-Token op mainnet, wat extra vertrouwen geeft in een van Solana's meest ingrijpende infrastructuurupgrades.

Door grote besparingen op rekenkracht te combineren met formeel geverifieerde gedragsgelijkwaardigheid, probeert de upgrade de netwerkefficiëntie te verbeteren zonder de toepassingen en activa te verstoren die elke dag afhankelijk zijn van het tokenprogramma.

Lees meer op SolanaFloor

Solana krijgt eindelijk Native Onchain Subscriptions, Unlocking Payroll, AI Agent Budgets, and Recurring Billing
Voormalig Amerikaans presidentskandidaat Andrew Yang's Noble Mobile neemt Helium Mobile over - Wat gebeurt er met $HNT?

Hoe zal de $2T IPO van SpaceX van invloed zijn op crypto?