Đánh giá toàn diện giải pháp mở rộng L2 mới ra mắt của StarkWare “Recursive Proof”

Tiêu đề gốc: "STARK đệ quy"

Tác giả gốc: Gidi Kaempfer, Kỹ sư cốt lõi của StarkWare

Bản tổng hợp gốc: cộng đồng "StarkNet Chinese"

Tóm tắt

· Bằng chứng đệ quy trực tuyến trên mạng chính, sử dụng một bằng chứng để mở rộng các ứng dụng StarkEx và StarkNet

·

·  Bằng chứng đệ quy cải thiện khả năng mở rộng, giảm chi phí và độ trễ (hiếm khi khả năng mở rộng và độ trễ phát triển đồng thời mà không có sự đánh đổi)

·  Bằng chứng đệ quy tạo điều kiện cho L3 và những ứng dụng tuyệt vời khác

· Chúng ta hãy xem bài đăng trên blog về bằng chứng đệ quy , Cực hay

Mở rộng nhiều lần

Các bằng chứng đệ quy được cung cấp bởi Cairo Universal Computing hiện đang được sản xuất. Điều này đánh dấu sự cải thiện đáng kể về khả năng mở rộng quy mô L2 của STARK. Số lượng giao dịch được ghi vào Ethereum chỉ bằng một bằng chứng duy nhất có thể nhanh chóng nhân lên.  

Cho đến nay, bằng chứng STARK mở rộng quy mô bằng cách "tổng hợp" hàng chục hoặc thậm chí hàng trăm nghìn giao dịch thành một bằng chứng duy nhất được viết trên Ethereum. Thông qua đệ quy, nhiều chứng minh như vậy có thể được “tổng hợp” thành một chứng minh duy nhất.  

Phương pháp này hiện được sử dụng trong nhiều ứng dụng có trụ sở tại Cairo: những ứng dụng chạy trên công cụ mở rộng quy mô SaaS của StarkWare, StarkEx và chương trình Rollup StarkNet không được phép.

Lịch sử phát triển cho đến nay

Kể từ khi bằng chứng đầu tiên được tạo ra trên mainnet vào tháng 3 năm 2020 , STARK chứng tỏ rằng cho đến nay nó đã trải qua các giai đoạn phát triển khác nhau.

Tiện ích mở rộng STARK

Tháng 6 năm 2020, giải pháp tiện ích mở rộng STARK đầu tiên  StarkEx Đã triển khai trên mạng chính Ethereum. StarkEx có một bộ chứng minh thực hiện các phép tính lớn ngoài chuỗi, tạo ra bằng chứng STARK thể hiện độ chính xác của giao dịch và một trình xác thực xác minh tính chính xác của bằng chứng trên chuỗi. Lần triển khai đầu tiên được thực hiện thủ công từ đầu bởi các kỹ sư của StarkWare nên khả năng của StarkEx bị hạn chế rất nhiều. Cuối cùng, chúng tôi quyết định rằng chúng tôi cần một ngôn ngữ lập trình hỗ trợ tính toán chứng minh tổng quát. Thế là Cairo ra đời.

Ngôn ngữ lập trình Cairo

Vào mùa hè năm 2020, Cairo ra mắt trên mạng chính Ethereum. Cairo là Biểu diễn trung gian đại số CPU (AIR), chứa một AIR duy nhất được sử dụng để xác minh tập lệnh "CPU" tương ứng. Cairo mở ra cánh cửa cho việc mã hóa bằng chứng về logic kinh doanh phức tạp hơn, các câu lệnh có thể tính toán tùy ý, nhanh hơn và an toàn hơn. Một chương trình Cairo có thể chứng minh tính logic thực thi của ứng dụng tương ứng. Nhưng chương trình Cairo cũng có thể là tập hợp của nhiều ứng dụng như vậy, đó là SHARP.

SẮC NÉT

SẮC NÉT Nghĩa là, bộ chứng minh được chia sẻ (SHARed ProSver) có thể tổng hợp các giao dịch từ một số ứng dụng độc lập và chứng minh chúng bằng một bằng chứng STARK duy nhất. Các ứng dụng có thể kết hợp các lô giao dịch khác nhau để lấp đầy dung lượng của bằng chứng STARK nhanh hơn. Tốc độ xử lý giao dịch và độ trễ được cải thiện. Bằng chứng đệ quy là thế hệ tiếp theo của công nghệ tiên tiến, không chỉ cho một số logic mã hóa cứng mà còn cho điện toán đa năng.  

Để hiểu đầy đủ lợi ích của bằng chứng đệ quy, cần phải xem xét kỹ hơn cách SHARP đã thực hiện bằng chứng (không đệ quy) cho đến nay. Hình 1 mô tả một quy trình không đệ quy điển hình:

Hình 1: Quy trình chứng minh không đệ quy điển hình

Trong quy trình này, mệnh đề dần dần được hình thành. Khi công suất (hoặc thời gian) đạt đến một ngưỡng nhất định, một đề xuất kết hợp lớn (Tàu hỏa) sẽ được tạo ra. Mệnh đề kết hợp này chỉ có thể được chứng minh sau khi tất cả các mệnh đề riêng lẻ đã được tiếp nhận. Việc chứng minh này mất nhiều thời gian (xấp xỉ tổng thời gian cần thiết để chứng minh từng mệnh đề riêng lẻ). Việc chứng minh các mệnh đề cực lớn cuối cùng bị hạn chế bởi các tài nguyên tính toán sẵn có như bộ nhớ. Trước khi đệ quy, đây thực sự là một trở ngại lớn hạn chế khả năng mở rộng của bằng chứng STARK.  

Chứng minh đệ quy là gì?  

 Với bằng chứng STARK, thời gian cần thiết để chứng minh một mệnh đề gần như tuyến tính với thời gian cần thiết để thực hiện nó. Hơn nữa, nếu thời gian cần thiết để chứng minh một mệnh đề là T thì thời gian cần thiết để xác minh bằng chứng là xấp xỉ log(T), thường được gọi là "nén log". Nói cách khác, sử dụng STARK cho phép người dùng tốn ít thời gian hơn để xác minh các mệnh đề so với việc tính toán chúng.  

Cairo Cho phép biểu thị các mệnh đề tính toán chung có thể được xác minh bằng bằng chứng STARK và sau đó được xác minh bằng trình xác minh STARK tương ứng.

Đây chính là cơ hội để thực hiện đệ quy: giống như một chương trình Cairo có thể được viết để chứng minh tính đúng đắn của hàng nghìn giao dịch , Bạn cũng có thể viết chương trình Cairo để xác minh nhiều Bằng chứng STARK. Một bằng chứng có thể được tạo ra để xác minh tính hợp lệ của nhiều bằng chứng "ngược dòng". Đây là những gì chúng tôi gọi là bằng chứng đệ quy.  

Vì quá trình nén logarit và thời gian chứng minh gần như tuyến tính nên thời gian cần thiết để xác minh bằng chứng STARK tương đối ngắn (dự kiến chỉ mất vài phút trong tương lai gần ).  

Khi triển khai đệ quy, SHARP có thể xác minh các mệnh đề ngay khi chúng được nhận. Bằng chứng có thể được hợp nhất nhiều lần thành bằng chứng đệ quy ở nhiều chế độ khác nhau cho đến khi, tại một thời điểm nào đó, bằng chứng thu được được gửi đến hợp đồng trình xác thực trên chuỗi. Hình 2 là chế độ chứng minh đệ quy điển hình:

Hình 2: Quy trình chứng minh đệ quy điển hình

Trong ví dụ này, bốn mệnh đề được gửi tới SHARP (có thể xuất phát từ bốn ứng dụng khác nhau). Mỗi mệnh đề này đều được chứng minh song song. Sau đó, mỗi cặp bằng chứng sẽ được xác minh bằng một đề xuất xác minh đệ quy (chương trình Cairo xác minh bằng chứng STARK), dẫn đến một bằng chứng. Mệnh đề này được xác nhận bởi hai bằng chứng. Tiếp theo, hai bằng chứng được hợp nhất lại thông qua mệnh đề xác minh đệ quy. Điều này mang lại một bằng chứng xác nhận cả bốn mệnh đề ban đầu. Bằng chứng này cuối cùng có thể được gửi trực tuyến để xác minh bởi hợp đồng thông minh của trình xác thực Solidity.

Ưu điểm trực tiếp của bằng chứng đệ quy

Giảm chi phí trên chuỗi

Không còn nghi ngờ gì nữa, chúng tôi đã đạt được mục tiêu "nén" nhiều bằng chứng thành một, nghĩa là chi phí xác minh của mỗi giao dịch trên chuỗi sẽ thấp hơn đáng kể (trong đó mỗi đề xuất có thể chứa nhiều giao dịch) .  

Sử dụng các bằng chứng đệ quy có thể loại bỏ các rào cản về tài nguyên tính toán (chẳng hạn như bộ nhớ) mà cho đến nay đã hạn chế quy mô của các bằng chứng, bởi vì mỗi mệnh đề có khả năng hạn chế và có thể được chứng minh riêng lẻ. Do đó, khi sử dụng đệ quy, khả năng của đề xuất kết hợp hiệu quả đệ quy (Train) gần như vô hạn và chi phí của mỗi giao dịch có thể giảm đi vài bậc độ lớn.  

Trong thực tế, việc giảm chi phí phụ thuộc vào độ trễ có thể chấp nhận được (và tốc độ giao dịch đến). Ngoài ra, vì mỗi bằng chứng thường đi kèm với đầu ra dữ liệu trên chuỗi tương ứng nên lượng dữ liệu được ghi vào chuỗi cùng với một bằng chứng duy nhất cũng sẽ bị hạn chế. Tuy nhiên, việc giảm chi phí ở mức độ lớn hoặc thậm chí tiếp tục cải thiện hiệu suất là điều có thể dễ dàng đạt được.

Giảm độ trễ