Ethereum xác minh quy tắc đồng thuận cho 3 nâng cấp bằng Lean 4

Nhóm nghiên cứu Ethereum(ETH) đang triển khai dự án hiện thực hóa và xác minh bằng toán học các quy tắc đồng thuận của ba nâng cấp Fulu, Gloas và Heze bằng Lean 4. Công việc này nhằm giảm nguy cơ chuỗi bị phân tách do các client diễn giải cùng một quy tắc theo những cách khác nhau.

Ethereum Protocol Fellowship (EPF) và nhóm nghiên cứu Invisible Garden đã công bố tiến độ dự án 'Etheorem' trong bài đăng trên diễn đàn Ethereum Research ngày 21. Etheorem hướng tới việc hiện thực hóa các quy tắc đồng thuận của Ethereum dưới dạng có thể thực thi bằng Lean 4, một ngôn ngữ chứng minh định lý, đồng thời xác minh bằng toán học các logic cốt lõi thay vì chỉ kiểm thử mã.

Ethereum sử dụng đồng thời nhiều client đồng thuận do các nhóm phát triển khác nhau xây dựng. Ngay cả khi cùng triển khai một quy tắc, các client vẫn có thể hiểu khác nhau về logic chi tiết, dẫn đến kết quả khác biệt trong việc xác định tính hợp lệ của block hoặc lựa chọn chuỗi. Etheorem kiểm tra những khác biệt trong cách diễn giải này bằng xác minh hình thức.

Dự án đã hiện thực hóa các quy tắc đồng thuận tương ứng với các nâng cấp Fulu, Gloas và Heze. Các quy tắc chuyển đổi trạng thái và logic lựa chọn fork có thể được thực thi, trong khi kết quả hiện thực hóa đang được đối chiếu với các bộ kiểm thử đồng thuận chính thức của Ethereum. Fulu bao gồm đặc tả liên quan đến lấy mẫu khả dụng dữ liệu, Gloas có các thành phần liên quan đến ePBS, cấu trúc đấu giá execution payload, còn Heze phản ánh cấu trúc danh sách bao gồm nhằm tăng khả năng chống kiểm duyệt.

Nền tảng của Etheorem là thư viện SSZ(Simple Serialize) SizzLean. Thư viện này xác minh trong Lean kernel một số thuộc tính cần thiết cho việc tuần tự hóa, giải tuần tự hóa dữ liệu đồng thuận và tính toán cây Merkle. Các mục được xác minh gồm khả năng đưa dữ liệu đã tuần tự hóa trở về giá trị ban đầu, bảo đảm các giá trị khác nhau không có cùng mã hóa và kiểm tra kích thước mã hóa không vượt quá giới hạn được tính toán trước.

Dự án cũng tập trung thu hẹp khoảng cách giữa mã đã được xác minh và mã thực thi thực tế. Ý tưởng là sử dụng cùng một định nghĩa quy tắc trong cả môi trường xác minh và môi trường thực thi, qua đó giảm nguy cơ logic dùng cho chứng minh khác với logic của client thực tế. Do xác minh hình thức chỉ kiểm tra logic trong phạm vi được áp dụng, đây chưa phải là giai đoạn thay thế toàn bộ client Ethereum. Trường hợp xác minh hình thức bằng Lean 4 đối với giao thức blockchain cũng được tiến hành bằng cách tái hiện logic cốt lõi dưới dạng mô hình để xác định phạm vi xác minh.

Việc vượt qua các bộ kiểm thử không đồng nghĩa với sự ổn định trong môi trường vận hành hay một bản phát hành chính thức. Dự án cho biết sẽ mở rộng phạm vi chứng minh trong thời gian tới.