Ethereum, Lean 4 ile üç yükseltmenin konsensüs doğrulamasını yapıyor

Ethereum(ETH) araştırma ekipleri, Lean 4 kullanarak Fulu, Gloas ve Heze yükseltmelerinin konsensüs spesifikasyonlarını uygulamak ve matematiksel olarak doğrulamak için bir proje yürütüyor. Çalışma, farklı istemcilerin aynı spesifikasyonu farklı yorumlamasından kaynaklanabilecek zincir bölünmesi riskini azaltmayı amaçlıyor.

Ethereum Protocol Fellowship (EPF) ve Invisible Garden araştırma ekipleri, 21'inde Ethereum Research Forum'da yayımladıkları gönderide 'Etheorem' projesinin ilerleyişini açıkladı. Etheorem, teorem ispatlama dili Lean 4 ile Ethereum konsensüs spesifikasyonunu çalıştırılabilir biçimde uygulamayı ve kod testlerinin ötesine geçerek temel mantığı matematiksel olarak doğrulamayı hedefliyor.

Ethereum, farklı geliştirme ekipleri tarafından oluşturulan birden fazla konsensüs istemcisinin birlikte kullanıldığı bir yapıya sahip. İstemciler aynı spesifikasyonu uygulasa bile ayrıntılı mantığın farklı yorumlanması, blok geçerliliği ve zincir seçimi sonuçlarının değişmesine yol açabiliyor. Etheorem bu yorum farklılıklarını biçimsel doğrulama yoluyla inceliyor.

Proje, Fulu, Gloas ve Heze yükseltmelerine ait konsensüs spesifikasyonlarını uyguladı. Durum geçişleri ve çatallanma seçimi mantığı çalıştırılabilirken, uygulama sonuçları Ethereum'un resmi konsensüs test vektörleriyle karşılaştırılarak kontrol ediliyor. Fulu, veri kullanılabilirliği örneklemesine ilişkin spesifikasyonları; Gloas, yürütme yükü açık artırması yapısı ePBS ile ilgili unsurları; Heze ise sansüre direnç amacı taşıyan dahil etme listesi yapısını içeriyor.

Etheorem'in temelinde SSZ(Simple Serialize) kütüphanesi SizzLean bulunuyor. Kütüphane, konsensüs verilerinin serileştirilmesi, seri durumdan çıkarılması ve Merkle ağacı hesaplamaları için gereken bazı özellikleri Lean çekirdeğinde doğruluyor. Doğrulanan unsurlar arasında serileştirilmiş verilerin özgün değerlerine geri dönebilmesi, farklı değerlerin aynı kodlamaya sahip olmaması ve kodlama boyutunun önceden hesaplanan sınırı aşmaması yer alıyor.

Proje, doğrulanmış kod ile gerçek çalışma kodu arasındaki farkı azaltmaya da odaklanıyor. Aynı spesifikasyon tanımının hem doğrulama hem de çalışma ortamında kullanılmasıyla, ispatlarda kullanılan mantıkla gerçek istemcilerin mantığının farklılaşması riskinin azaltılması amaçlanıyor. Biçimsel doğrulama, yalnızca kapsama alanındaki mantığı incelediği için bu aşama tüm Ethereum istemcisinin yerine geçmiyor. Blockchain protokollerinde Lean 4 biçimsel doğrulama örneği de temel mantığın bir modelle yeniden oluşturulması ve doğrulama kapsamının belirlenmesi yöntemiyle yürütüldü.

Test vektörlerinin geçilmesi, çalışma ortamında istikrar veya resmi sürüm anlamına gelmiyor. Proje, gelecekte doğrulama kapsamını genişletmeyi planlıyor.