Tiêu đề ban đầu được chuyển tiếp 'Vitalik giải thích Binius chi tiết: một hệ thống chứng minh hiệu quả dựa trên trường nhị phân'

Bài đăng này chủ yếu dành cho độc giả có kiến thức đề cập đến mật mã thời kỳ 2019, đặc biệt là SNARKs và STARKs. Nếu không, tôi khuyên bạn nên đọc những bài viết đó trước. Xin cảm ơn đặc biệt Justin Drake, Jim Posen, Benjamin Diamond và Radi Cojbasic đã đưa ra phản hồi và xem xét.

Trong hai năm qua, STARKs đã trở thành một công nghệ quan trọng và không thể thay thế để tạo ra các bằng chứng mật mã dễ xác minh của các tuyên bố rất phức tạp một cách hiệu quả (ví dụ: chứng minh rằng một khối Ethereum là hợp lệ). Một lý do chính là kích thước trường nhỏ: trong khi SNARKs dựa trên đường cong elip cần bạn làm việc trên các số nguyên 256-bit để đảm bảo an toàn đủ, STARKs cho phép bạn sử dụng kích thước trường nhỏ hơn nhiều, hiệu quả hơn: trước hết là trường Goldilocks (số nguyên 64-bit), sau đó là Mersenne31 và BabyBear (cả hai đều 31-bit). Nhờ những lợi ích về hiệu suất này, Plonky2, sử dụng Goldilocks, nhanh hơn hàng trăm lần trong việc chứng minh nhiều loại tính toán so với các phiên bản trước đó.

Một câu hỏi tự nhiên cần được đặt ra là: liệu chúng ta có thể đưa xu hướng này đến hồi kết logic của nó, xây dựng hệ thống chứng minh hoạt động nhanh hơn bằng cách hoạt động trực tiếp trên số không và số một không? Điều này chính xác là điều mà Binius đang cố gắng làm, bằng cách sử dụng một số mẹo toán học làm cho nó rất khác biệt so với SNARKs và STARKs của ba năm trước. Bài đăng này đi qua những lý do tại sao các trường nhỏ làm cho việc tạo chứng minh hiệu quả hơn, tại sao các trường nhị phân mạnh mẽ độc đáo, và những mẹo mà Binius sử dụng để làm cho việc chứng minh trên các trường nhị phân hoạt động hiệu quả như vậy.

Binius. By the end of this post, you should be able to understand every part of this diagram.

Tóm tắt: các trường hữu hạn

Một trong những nhiệm vụ quan trọng của một hệ thống chứng minh mật mã là hoạt động trên lượng dữ liệu lớn, đồng thời giữ cho các con số nhỏ. Nếu bạn có thể nén một tuyên bố về một chương trình lớn thành một phương trình toán học liên quan đến một số ít con số, nhưng những con số đó lớn như chương trình ban đầu, bạn chẳng có được gì cả.

Để thực hiện phép tính phức tạp với việc giữ cho số nhỏ, các nhà mật mã thường sử dụng toán học modulo. Chúng tôi chọn một số nguyên tố “modulus” p. Toán tử % có nghĩa là “lấy phần dư của”: 15 % 7=1, 53 % 10=3, vv (lưu ý rằng kết quả luôn là không âm, vì vậy ví dụ −1 % 10=9).

Bạn có thể đã thấy toán học modula, trong bối cảnh cộng và trừ thời gian (ví dụ: mấy giờ sau 9:00 là mấy giờ?). Nhưng ở đây, chúng ta không chỉ cộng và trừ theo modulo một số nào đó, chúng ta cũng nhân, chia và lấy lũy thừa.

Chúng tôi định nghĩa lại:

Các quy tắc trên đều tự nhất quán. Ví dụ, nếu p=7, thì:

5+3=1 (because 8%7=1)

1-3=5 (vì -2%7=5)

2*5=3

3/5=2

Một thuật ngữ tổng quát hơn cho loại cấu trúc này là một trường hữu hạn. Một trường hữu hạn là một cấu trúc toán học tuân theo các luật thông thường của toán học, nhưng nơi có một số lượng giá trị có hạn, và do đó mỗi giá trị có thể được biểu diễn trong một kích thước cố định.

Toán học modun (hoặc trường số nguyên tố) là loại trường hữu hạn phổ biến nhất, nhưng cũng có một loại khác: trường mở rộng. Bạn có thể đã từng thấy một trường mở rộng trước đó: số phức. Chúng ta “tưởng tượng” một phần tử mới, mà chúng ta gọi là 𝑖, và tuyên bố rằng nó thỏa mãn 𝑖2=−1. Sau đó, bạn có thể lấy bất kỳ kết hợp nào của số thông thường và 𝑖, và thực hiện phép toán với nó: (3𝑖+2)∗(2𝑖+4)= 6𝑖2+12𝑖+4𝑖+8=16𝑖+2. Chúng ta cũng có thể lấy các phần mở rộng của trường số nguyên tố. Khi chúng ta bắt đầu làm việc trên các trường nhỏ hơn, các phần mở rộng của trường số nguyên tố trở nên ngày càng quan trọng để bảo vệ an ninh, và các trường nhị phân (mà Binius sử dụng) phụ thuộc hoàn toàn vào các phần mở rộng để có tính ứng dụng thực tế.

Tóm tắt: arithmetization

Cách mà SNARKs và STARKs chứng minh những điều về các chương trình máy tính là thông qua việc chuyển đổi thành phép toán: bạn chuyển một tuyên bố về một chương trình mà bạn muốn chứng minh, thành một phương trình toán học liên quan đến đa thức. Một giải pháp hợp lệ cho phương trình tương ứng với một thực thi hợp lệ của chương trình.

Để đưa ra một ví dụ đơn giản, giả sử rằng tôi tính toán số Fibonacci thứ 100, và tôi muốn chứng minh cho bạn nó là gì. Tôi tạo một đa thức 𝐹 mã hóa các số Fibonacci: với 𝐹(0)=𝐹(1)=1, 𝐹(2)=2, 𝐹(3)=3, 𝐹(4)=5, và cứ tiếp tục như vậy trong 100 bước. Điều kiện mà tôi cần chứng minh là 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) trên phạm vi 𝑥={0,1…98}. Tôi có thể thuyết phục bạn điều này bằng cách cung cấp cho bạn phần dư:

nơi Z(x) = (x-0)(x-1)…(x-98). . Nếu tôi có thể chứng minh rằng có một hàm số F và H thỏa mãn phương trình này, thì F phải thỏa mãn F(x+2)-F(x+1)-F(x) trong dãy số. Nếu tôi còn kiểm tra thêm rằng F thỏa mãn F(0)=F(1)=1, thì F(100) sẽ thực sự là số Fibonacci thứ 100.

Nếu bạn muốn chứng minh một điều gì đó phức tạp hơn, sau đó bạn thay thế mối quan hệ “đơn giản” 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) bằng một phương trình phức tạp hơn, mà cơ bản nói “𝐹(𝑥+1) là đầu ra của việc khởi tạo một máy ảo với trạng thái 𝐹(𝑥), và chạy một bước tính toán”. Bạn cũng có thể thay thế số 100 bằng một số lớn hơn, ví dụ 100000000, để thực hiện nhiều bước hơn.

Tất cả SNARKs và STARKs đều dựa trên ý tưởng này của việc sử dụng một phương trình đơn giản trên đa thức (hoặc đôi khi là vectors và ma trận) để đại diện cho một số lượng lớn mối quan hệ giữa các giá trị cá nhân. Không phải tất cả đều liên quan đến việc kiểm tra sự tương đương giữa các bước tính toán kề nhau theo cách như trên: PLONK không, ví dụ, và R1CS cũng không. Nhưng nhiều trong số những phương pháp hiệu quả nhất đều làm như vậy, vì áp dụng cùng một kiểm tra (hoặc một vài kiểm tra giống nhau) nhiều lần giúp làm giảm thiểu chi phí thừa.

Plonky2: từ SNARKs và STARKs 256-bit đến 64-bit… chỉ STARKs

Năm năm trước, một tóm tắt hợp lý về các loại chứng minh không thông tin khác nhau như sau. Có hai loại chứng minh: (dựa trên đường cong elip) SNARKs và (dựa trên băm) STARKs. Về mặt kỹ thuật, STARKs là một loại của SNARK, nhưng trong thực tế, việc sử dụng thuật ngữ “SNARK” chỉ thường áp dụng cho loại dựa trên đường cong elip, và “STARK” để áp dụng cho các cấu trúc dựa trên băm. SNARKs nhỏ, và vì vậy bạn có thể xác minh chúng một cách nhanh chóng và dễ dàng đưa chúng lên chuỗi. STARKs lớn, nhưng họ không yêu cầu thiết lập đáng tin cậy, và họ chống lại lượng tử.

STARKs hoạt động bằng cách xử lý dữ liệu như một đa thức, tính toán các đánh giá của đa thức đó trên một số lượng lớn các điểm và sử dụng gốc Merkle của dữ liệu mở rộng đó làm "cam kết đa thức"

Một phần quan trọng của lịch sử ở đây là SNARKs dựa trên đường cong elip đã được sử dụng rộng rãi trước hết: mất đến khoảng năm 2018 STARKs mới trở nên hiệu quả đủ để sử dụng, nhờ vào FRI, và đến lúc đó Zcash đã hoạt động được hơn một năm. SNARKs dựa trên đường cong elip có một hạn chế quan trọng: nếu bạn muốn sử dụng SNARKs dựa trên đường cong elip, thì phép toán trong các phương trình này phải được thực hiện với số nguyên modulo số điểm trên đường cong elip. Đây là một con số lớn, thường gần 2256: ví dụ, đối với đường cong bn128, nó là 21888242871839275222246405745257275088548364400416034343698204186575808495617. Nhưng việc tính toán thực sự đang sử dụng các con số nhỏ: nếu bạn nghĩ về một chương trình “thực sự” bằng ngôn ngữ yêu thích của bạn, hầu hết những thứ mà nó đang làm việc với là các bộ đếm, chỉ số trong vòng lặp, vị trí trong chương trình, các bit đại diện cho Đúng hoặc Sai, và những thứ khác mà hầu như luôn chỉ có một vài chữ số.

Dù dữ liệu “ban đầu” của bạn được tạo ra từ các con số “nhỏ”, quá trình chứng minh yêu cầu tính các thương, mở rộng, kết hợp tuyến tính ngẫu nhiên và các biến đổi khác của dữ liệu, dẫn đến một số lượng đối tượng bằng hoặc lớn hơn, trên trung bình, như kích thước đầy đủ của trường của bạn. Điều này tạo ra một hiệu suất chìa khóa: để chứng minh một tính toán trên n giá trị nhỏ, bạn phải thực hiện thêm nhiều tính toán hơn trên n giá trị lớn hơn nhiều. Ban đầu, STARKs thừa kế thói quen sử dụng trường 256 bit từ SNARKs, và vì vậy gặp phải cùng một hiệu suất không hiệu quả.

Một phần mở rộng Reed-Solomon của một số đánh giá đa thức. Mặc dù các giá trị ban đầu nhỏ, các giá trị bổ sung đều tăng lên đến kích thước đầy đủ của trường (trong trường hợp này là 2 mũ 31 -1)

Năm 2022, Plonky2 được phát hành. Đổi mới chính của Plonky2 là thực hiện phép toán theo modulo của số nguyên tố nhỏ hơn: 2⁶⁴−2³²+1=18446744069414584321. Bây giờ, mỗi phép cộng hoặc nhân luôn có thể được thực hiện chỉ trong vài hướng dẫn trên một CPU, và băm tất cả dữ liệu lại với tốc độ nhanh hơn 4 lần so với trước. Nhưng điều này đi kèm với một điều: phương pháp này chỉ dành riêng cho STARK. Nếu bạn cố gắng sử dụng một SNARK, với một đường cong elliptic có kích thước nhỏ như vậy, đường cong elliptic trở nên không an toàn.

Để tiếp tục đảm bảo an toàn, Plonky2 cũng cần phải giới thiệu các trường mở rộng. Một kỹ thuật quan trọng trong việc kiểm tra phương trình toán học là “lấy mẫu tại một điểm ngẫu nhiên”: nếu bạn muốn kiểm tra xem 𝐻(𝑥)∗𝑍(𝑥) thực sự bằng 𝐹(𝑥+2)−𝐹(𝑥+1)−𝐹(𝑥) hay không, bạn có thể chọn một số tọa độ ngẫu nhiên 𝑟, cung cấp bằng chứng mở cam kết đa thức chứng minh 𝐻(𝑟), 𝑍(𝑟), 𝐹(𝑟), 𝐹(𝑟+1) và 𝐹(𝑟+2), sau đó thực sự kiểm tra xem 𝐻(𝑟)∗𝑍(𝑟) có bằng 𝐹(𝑟+2)−𝐹(𝑟+1)−𝐹(𝑟) hay không. Nếu kẻ tấn công có thể đoán được tọa độ trước, kẻ tấn công có thể lừa hệ thống bằng chứng - đó là lý do tại sao nó phải là ngẫu nhiên. Nhưng điều này cũng có nghĩa là tọa độ phải được lấy mẫu từ một tập hợp đủ lớn để kẻ tấn công không thể đoán được nó theo cách ngẫu nhiên. Nếu số dư gần bằng 2²⁵⁶, đây rõ ràng là trường hợp. Nhưng với mô đun là 2⁶⁴−2³²+1, chúng ta chưa đến đó, và nếu giảm xuống 2³¹−1, chắc chắn không phải vậy. Cố gắng làm giả một bằng chứng hai tỷ lần cho đến khi có may mắn hoàn toàn trong khả năng của một kẻ tấn công.

Để ngừng việc này, chúng tôi lấy mẫu 𝑟 từ một trường mở rộng. Ví dụ, bạn có thể xác định 𝑦 trong đó 𝑦³=5, và lấy các tổ hợp của 1, 𝑦 và 𝑦². Điều này tăng tổng số tọa độ trở lại khoảng 2⁹³. Số lượng lớn các đa thức được tính toán bởi người chứng minh không được chuyển vào trường mở rộng này; chúng chỉ sử dụng số nguyên modulo 2³¹−1, và vẫn có tất cả hiệu quả từ việc sử dụng trường nhỏ. Nhưng kiểm tra điểm ngẫu nhiên và tính toán FRI, lại nảy mình vào trường lớn này, để đạt được tính bảo mật cần thiết.

Từ số nguyên tố nhỏ đến nhị phân

Máy tính thực hiện phép toán bằng cách biểu diễn các số lớn dưới dạng chuỗi các số 0 và 1, và xây dựng “mạch điện” trên các bit đó để tính toán như phép cộng và nhân. Máy tính được tối ưu hóa đặc biệt cho việc tính toán với số nguyên 16-bit, 32-bit và 64-bit. Các mô đun như 2⁶⁴−2³²+1 and 2³¹−1 được chọn không chỉ vì chúng nằm trong ranh giới đó, mà còn vì chúng phù hợp tốt với những giới hạn đó: bạn có thể thực hiện phép nhân modulo 2⁶⁴−2³²+1 bằng cách thực hiện phép nhân 32 bit thường, và dịch chuyển và sao chép kết quả theo bit ở một số nơi; bài viết này giải thích một số mẹo tốt.

Tuy nhiên, điều tốt hơn hết là thực hiện các phép tính trực tiếp trong hệ nhị phân. Điều gì sẽ xảy ra nếu phép cộng có thể chỉ là phép XOR, mà không cần phải lo lắng về việc 'vận chuyển' sự tràn từ việc cộng 1 + 1 trong một vị trí bit sang vị trí bit tiếp theo? Điều gì sẽ xảy ra nếu phép nhân có thể được phân rã thành nhiều phần một cách song song? Và những lợi ích này sẽ đến cùng với việc biểu diễn các giá trị Đúng/Sai chỉ với một bit.

Việc bắt kịp những lợi ích của việc thực hiện tính toán nhị phân trực tiếp chính xác là điều mà Binius đang cố gắng thực hiện. Một bảng từ bài thuyết trình zkSummit của nhóm Binius cho thấy sự tăng cường hiệu suất:

Mặc dù có khoảng cách "kích thước" tương tự nhau, một phép toán trên trường nhị phân 32 bit mất ít hơn 5 lần tài nguyên tính toán so với một phép toán trên trường Mersenne 31 bit.

Từ đa thức một biến đến hypercubes

Giả sử rằng chúng ta bị thuyết phục bởi lý do này và muốn thực hiện mọi thứ qua các bit (số không và số một). Làm thế nào chúng ta thực sự cam kết với một đa thức đại diện cho một tỷ bit?

Ở đây, chúng ta đối mặt với hai vấn đề thực tế:

1. Để một đa thức biểu diễn nhiều giá trị, những giá trị đó cần được truy cập khi đánh giá đa thức: trong ví dụ Fibonacci của chúng tôi ở trên, 𝐹(0), 𝐹(1) … 𝐹(100), và trong một tính toán lớn hơn, các chỉ số sẽ lên đến hàng triệu. Và lĩnh vực mà chúng tôi sử dụng cần chứa các số lên đến kích thước đó.

2. Chứng minh bất cứ điều gì về một giá trị mà chúng ta đang cam kết trong cây Merkle (như tất cả các STARK làm) yêu cầu Reed-Solomon mã hóa nó: mở rộng n giá trị thành ví dụ. Giá trị 8n, sử dụng dự phòng để ngăn chặn một prover độc hại gian lận bằng cách giả mạo một giá trị ở giữa tính toán. Điều này cũng đòi hỏi phải có một trường đủ lớn: để mở rộng một triệu giá trị lên 8 triệu, bạn cần 8 triệu điểm khác nhau để đánh giá đa thức.

Một ý tưởng chính trong Binius là giải quyết hai vấn đề này một cách riêng biệt, và làm điều đó bằng cách biểu diễn cùng một dữ liệu theo hai cách khác nhau. Đầu tiên, đa thức chính nó. SNARKs dựa trên đường cong Elliptic, STARKs thời kỳ 2019, Plonky2 và các hệ thống khác nói chung xử lý với đa thức trên một biến: 𝐹(𝑥). Ngược lại, Binius lấy cảm hứng từ giao thức Spartan, và làm việc với đa thức đa biến: 𝐹(𝑥1,𝑥2…𝑥𝑘). Trên thực tế, chúng tôi biểu diễn toàn bộ dấu vết tính toán trên “đa diện” của các đánh giá, trong đó mỗi 𝑥𝑖 là hoặc 0 hoặc 1. Ví dụ, nếu chúng tôi muốn biểu diễn một dãy số Fibonacci, và chúng tôi vẫn sử dụng một trường đủ lớn để biểu diễn chúng, chúng tôi có thể tưởng tượng 16 số đầu tiên của chúng như sau:

Nghĩa là, 𝐹(0,0,0,0) sẽ là 1, 𝐹(1,0,0,0) cũng sẽ là 1, 𝐹(0,1,0,0) sẽ là 2, và cứ thế, cho đến khi chúng ta đến 𝐹(1,1,1,1)=987. Với một hypercube như vậy của các đánh giá, tồn tại đúng một đa tuyến tính (độ 1 trong mỗi biến) đa thức tạo ra các đánh giá đó. Vì vậy, chúng ta có thể nghĩ rằng tập hợp các đánh giá đó đang đại diện cho đa thức; chúng ta không bao giờ cần phải tính toán các hệ số thực sự.

Ví dụ này chỉ mang tính minh họa: trong thực tế, mục đích chính của việc đi đến một siêu khối là để cho phép chúng ta làm việc với từng bit cá nhân. Cách “Binius-native” đếm số Fibonacci sẽ là sử dụng một khối có số chiều cao hơn, sử dụng mỗi bộ ví dụ 16 bit để lưu trữ một số. Điều này yêu cầu một chút khéo léo để thực hiện phép cộng số nguyên trên cơ sở của các bit, nhưng với Binius, điều này không quá khó.

Bây giờ, chúng ta đến với mã hóa xóa. Cách hoạt động của STARKs là: bạn lấy 𝑛 giá trị, mở rộng Reed-Solomon chúng thành một số lượng giá trị lớn hơn (thường là 8𝑛, thường nằm giữa 2𝑛 và 32𝑛), sau đó chọn ngẫu nhiên một số nhánh Merkle từ phần mở rộng và thực hiện một loại kiểm tra nào đó trên chúng. Một siêu khối có độ dài 2 trong mỗi chiều. Do đó, việc mở rộng nó trực tiếp không thực tế: không đủ “không gian” để lấy mẫu các nhánh Merkle từ 16 giá trị. Vậy chúng ta phải làm gì thay vào đó? Chúng ta giả vờ rằng siêu khối là một hình vuông!

Simple Binius - một ví dụ

Xem ở đâycho một triển khai python của giao thức này.

Hãy xem qua một ví dụ, sử dụng các số nguyên thông thường làm trường hợp tiện lợi của chúng tôi (trong một triển khai thực tế điều này sẽ là các phần tử trường nhị phân). Đầu tiên, chúng ta lấy hypercube mà chúng ta muốn cam kết, và mã hóa nó như một hình vuông:

Bây giờ, chúng tôi mở rộng Reed-Solomon cho hình vuông. Đó là, chúng tôi xem xét mỗi hàng như là một đa thức bậc 3 được đánh giá tại x = {0, 1, 2, 3}, và đánh giá cùng một đa thức tại x = {4, 5, 6, 7}:

Lưu ý rằng các số tăng nhanh chóng! Đây là lý do tại sao trong một triển khai thực tế, chúng ta luôn sử dụng một trường hữu hạn cho điều này, thay vì sử dụng các số nguyên thông thường: nếu chúng ta sử dụng số nguyên modulo 11, ví dụ, sự mở rộng của hàng đầu tiên sẽ chỉ là [3, 10, 0, 6].

Nếu bạn muốn chơi với việc mở rộng và xác minh các con số ở đây cho chính mình, bạn có thể sử dụng mã mở rộng Reed-Solomon đơn giản của tôi ở đây.

Tiếp theo, chúng tôi xem xét phần mở rộng này như là các cột, và tạo một cây Merkle của các cột. Gốc của cây Merkle là sự cam kết của chúng tôi.

Bây giờ, giả sử rằng người chứng minh muốn chứng minh một đánh giá của đa thức này tại một số điểm r = {r0,r1,r2,r3}. Có một sắc thái trong Binius làm cho nó yếu hơn một chút so với các sơ đồ cam kết đa thức khác: người chứng minh không nên biết, hoặc có thể đoán, s, cho đến khi họ cam kết với gốc Merkle (nói cách khác, r phải là một giá trị giả ngẫu nhiên phụ thuộc vào gốc Merkle). Điều này làm cho lược đồ trở nên vô dụng đối với "tra cứu cơ sở dữ liệu" (ví dụ: "ok bạn đã cho tôi gốc Merkle, bây giờ chứng minh cho tôi P (0,0,1,0)!"). Nhưng các giao thức bằng chứng không có kiến thức thực tế mà chúng tôi sử dụng thường không cần "tra cứu cơ sở dữ liệu"; Họ chỉ cần kiểm tra đa thức tại một điểm đánh giá ngẫu nhiên. Do đó, hạn chế này là ổn cho mục đích của chúng tôi.

Giả sử chúng ta chọn 𝑟={1,2,3,4} (đa thức, ở điểm này, đánh giá là −137; bạn có thể xác nhận nóvới mã này). Bây giờ, chúng tôi bắt đầu quá trình thực sự tạo ra bằng chứng. Chúng tôi chia 𝑟 thành hai phần: phần đầu tiên {1,2} đại diện cho một tổ hợp tuyến tính của các cột trong một hàng, và phần thứ hai {3,4} đại diện cho một tổ hợp tuyến tính của các hàng. Chúng tôi tính một “tích tensor”, cả hai cho phần cột:

Và cho phần hàng:

Điều này có nghĩa là: một danh sách tất cả các sản phẩm có thể từ một giá trị từ mỗi tập hợp. Trong trường hợp hàng, chúng ta có:

[(1-r2)(1-r3), (1-r3), (1-r2)r3, r2*r3]

Sử dụng r={1,2,3,4} (vì vậy r2=3 và r3=4):

[(1-3)(1-4), 3(1-4),(1-3)4,34] = [6, -9 -8 -12]

Bây giờ, chúng ta tính toán một “hàng” mới 𝑡′, bằng cách lấy tổ hợp tuyến tính của các hàng hiện có. Đó là, chúng ta lấy:

Bạn có thể xem những gì đang diễn ra ở đây như một đánh giá một phần. Nếu chúng ta nhân tích tenxơ đầy đủ ⨂i = 03 (1−ri, ri) với vectơ đầy đủ của tất cả các giá trị, bạn sẽ nhận được đánh giá P (1,2,3,4) = −137. Ở đây chúng ta đang nhân một tích tensor từng phần chỉ sử dụng một nửa tọa độ đánh giá và chúng ta đang giảm một lưới gồm các giá trị N thành một hàng giá trị N. Nếu bạn đưa hàng này cho người khác, họ có thể sử dụng tích tensor của nửa tọa độ đánh giá còn lại để hoàn thành phần còn lại của phép tính.

Bằng chứng cung cấp cho người xác minh hàng mới này, 𝑡′, cũng như chứng minh Merkle của một số cột được chọn ngẫu nhiên. Điều này là dữ liệu 𝑂(𝑁). Trong ví dụ minh họa của chúng tôi, chúng tôi sẽ yêu cầu bằng chứng chỉ cung cấp cột cuối cùng; trong cuộc sống thực, bằng chứng sẽ cần cung cấp một vài chục cột để đạt được độ an toàn đủ.

Bây giờ, chúng tôi tận dụng tính tuần tự của các mã Reed-Solomon. Thuộc tính quan trọng mà chúng tôi sử dụng là: việc lấy tổ hợp tuyến tính của một mở rộng Reed-Solomon cho kết quả giống như một mở rộng Reed-Solomon của một tổ hợp tuyến tính. Loại “độc lập thứ tự” này thường xảy ra khi bạn có hai phép toán đều tuyến tính.

Người xác thực chính xác làm điều này. Họ tính toán phần mở rộng của 𝑡′, và họ tính toán cùng một tổ hợp tuyến tính của các cột mà bằng chứng đã tính toán trước đó (nhưng chỉ đối với các cột do bằng chứng cung cấp), và xác minh rằng hai quy trình này cho cùng một câu trả lời.

Trong trường hợp này, mở rộng 𝑡′ và tính toán cùng một tổ hợp tuyến tính ([6,−9,−8,12]) của cột, cả hai đều cho cùng một câu trả lời: −10746. Điều này chứng minh rằng Merkle root được xây dựng "một cách chân thành" (hoặc ít nhất là "gần đúng"), và nó khớp với 𝑡′: ít nhất là đa số lớn các cột tương thích với nhau và với 𝑡′.

Nhưng người xác minh vẫn cần kiểm tra thêm một điều nữa: thực sự kiểm tra đánh giá đa thức tại {r0.. r3}. Cho đến nay, không có bước nào của người xác minh thực sự phụ thuộc vào giá trị mà người chứng minh tuyên bố. Vì vậy, đây là cách chúng tôi thực hiện kiểm tra đó. Chúng tôi lấy tích tensor của những gì chúng tôi dán nhãn là "phần cột" của điểm đánh giá:

Trong ví dụ của chúng tôi, khi r={1,2,3,4} nên nửa của cột được chọn là {1,2}), điều này bằng:

Vì vậy bây giờ chúng ta lấy tổ hợp tuyến tính này của 𝑡′:

Điều này chính xác bằng câu trả lời bạn nhận được nếu bạn đánh giá đa thức trực tiếp.

Trên đây là khá gần với một mô tả đầy đủ về giao thức Binius "đơn giản". Điều này đã có một số lợi thế thú vị: ví dụ: vì dữ liệu được chia thành các hàng và cột, bạn chỉ cần một trường có kích thước bằng một nửa. Nhưng điều này không đến gần với việc nhận ra lợi ích đầy đủ của việc tính toán trong nhị phân. Đối với điều này, chúng tôi sẽ cần giao thức Binius đầy đủ. Nhưng trước tiên, chúng ta hãy hiểu sâu hơn về các trường nhị phân.

Trường nhị phân

Trường hợp nhỏ nhất có thể là phép toán modulo 2, đủ nhỏ để chúng ta có thể viết ra các bảng cộng và nhân của nó:

Chúng ta có thể tạo các trường nhị phân lớn hơn bằng cách mở rộng: nếu chúng ta bắt đầu với 𝐹2 (số nguyên modulo 2) và sau đó xác định 𝑥 sao cho 𝑥2=𝑥+1, chúng ta có bảng cộng và nhân sau đây:

Có vẻ như chúng ta có thể mở rộng trường nhị phân thành các kích thước rất lớn bằng cách lặp lại cấu trúc này. Khác với số phức trên số thực, nơi bạn có thể thêm một phần tử mới 𝑖, nhưng bạn không thể thêm thêm bất kỳ phần tử nào nữa (phân số tồn tại, nhưng chúng toán học kỳ lạ, ví dụ 𝑎𝑏≠𝑏𝑎), với các trường hữu hạn, bạn có thể tiếp tục thêm các phần mở rộng mới mãi mãi. Cụ thể, chúng ta xác định các phần tử như sau:

Và cứ thế. Điều này thường được gọi là xây dựng tháp, bởi vì mỗi sự mở rộng liên tục có thể được xem như việc thêm một tầng mới vào một tháp. Đây không phải là cách duy nhất để xây dựng các trường nhị phân có kích thước tùy ý, nhưng nó có một số ưu điểm độc đáo mà Binius tận dụng.

Chúng ta có thể biểu diễn những con số này dưới dạng danh sách các bit, ví dụ: 1100101010001111. Bit đầu tiên đại diện cho bội số của 1, bit thứ hai đại diện cho bội số của 𝑥0, sau đó các bit tiếp theo đại diện cho bội số của: 𝑥1, 𝑥1∗𝑥0, 𝑥2, 𝑥2∗𝑥0, và cứ tiếp tục như vậy. Phương pháp mã hóa này tốt vì bạn có thể phân rã nó:

Đây là một cách biểu diễn khá hiếm gặp, nhưng tôi thích biểu diễn các phần tử trường nhị phân dưới dạng số nguyên, lấy biểu diễn bit với bit quan trọng hơn ở bên phải. Đó là, 1=1, 𝑥₀=01=2, 1+𝑥₀=11=3, 1+𝑥₀+𝑥₂=11001000=19, và cứ tiếp tục như vậy. 1100101010001111 là, trong biểu diễn này, 61779.

Phép cộng trong một trường nhị phân chỉ là XOR (như phép trừ, nhớ rằng điều này có nghĩa là x+x=0 với mọi x). Để nhân hai phần tử x*y, có một thuật toán đệ quy rất đơn giản: chia mỗi số thành hai phần:

Sau đó, chia nhỏ phép nhân:

Phần cuối cùng là phần duy nhất hơi khó khăn một chút, vì bạn phải áp dụng quy tắc giảm và thay thế 𝑅𝑥∗𝑅𝑦∗𝑥𝑘2 bằng 𝑅𝑥∗𝑅𝑦∗(𝑥𝑘−1∗𝑥𝑘+1). Có nhiều cách hiệu quả hơn để thực hiện phép nhân, tương đương với thuật toán Karatsuba và biến đổi Fourier nhanh, nhưng tôi sẽ để đọc giả quan tâm tìm hiểu những cách đó.

Phép chia trong các trường nhị phân được thực hiện bằng cách kết hợp phép nhân và phép nghịch đảo. Cách 'đơn giản nhưng chậm' để thực hiện phép nghịch đảo là một ứng dụng của định lý nhỏ của Fermat tổng quát. Cũng có một thuật toán nghịch đảo phức tạp hơn nhưng hiệu quả hơn, mà bạn có thể tìm thấy ở đây. Bạn có thể sử dụng mã ở đâyđể chơi với phép cộng, nhân và chia trường nhị phân một cách tự mình.

Bảng cộng cho phần tử trường nhị phân bốn-bít (tức là các phần tử chỉ được tạo thành từ các kết hợp của 1, 𝑥₀，𝑥₁ và 𝑥₀𝑥₁).

Đúng: bảng nhân cho các phần tử trường nhị phân bốn bit.

Điều đẹp về loại trường nhị phân này là nó kết hợp một số phần tốt nhất của các số nguyên “thường” và toán học modulo. Giống như các số nguyên thông thường, các phần tử trường nhị phân không bị ràng buộc: bạn có thể mở rộng miễn là bạn muốn. Nhưng giống như toán học modulo, nếu bạn thực hiện các phép toán trên các giá trị trong một giới hạn kích thước nhất định, tất cả các câu trả lời của bạn cũng ở trong cùng một giới hạn. Ví dụ, nếu bạn lấy các lũy thừa liên tiếp của 42, bạn sẽ nhận được:

Sau 255 bước, bạn trở lại con số 42²⁵⁵ = 1. Giống như số nguyên dương và toán học modulo, chúng tuân theo các quy luật toán học thông thường: ab=ba, a(b+c)=a b+a*c, có ngay cả một số luật lệ mới kỳ lạ.

Cuối cùng, các trường nhị phân giúp xử lý bit dễ dàng: nếu bạn thực hiện phép toán với các số phù hợp 2^k bits, sau đó tất cả đầu ra của bạn cũng sẽ phù hợp 2 k bits. Điều này tránh được sự bối rối. Trong EIP-4844 của Ethereum, mỗi “block” của một blob phải là một module số học kỹ thuật số 52435875175126190479447740508185965837690552500527637822603658699938581184513, vì vậy việc mã hóa dữ liệu nhị phân đòi hỏi phải bỏ đi một số không gian và thực hiện thêm một kiểm tra để đảm bảo rằng mỗi phần tử lưu trữ một giá trị nhỏ hơn 2²⁴⁸Điều này cũng có nghĩa là các phép toán trên trường nhị phân diễn ra rất nhanh trên máy tính - cả CPU và lý thuyết các thiết kế FPGA và ASIC tối ưu.

Điều này có nghĩa là chúng ta có thể thực hiện một cái gì đó giống như việc mã hóa Reed-Solomon mà chúng ta đã thực hiện ở trên, một cách hoàn toàn tránh được sự “nổ” số nguyên, như chúng ta đã thấy trong ví dụ của mình, và một cách “nổ” rất mạnh mẽ. Cách “thuần túy”, loại tính toán mà máy tính tốt at. Thuộc tính “phân chia” của các trường nhị phân - cách chúng ta thực hiện nó 1100101010001111=11001010+10001111*x₃và sau đó chia nó theo nhu cầu của chúng tôi cũng quan trọng để đạt được sự linh hoạt lớn.

Full Binius

Xem ở đâyđể một triển khai python của giao thức này.

Bây giờ, chúng ta có thể đến với “Binius đầy đủ”, điều chỉnh “Binius đơn giản” để (i) hoạt động trên các trường nhị phân và (ii) cho phép chúng ta cam kết vào từng bit cụ thể. Giao thức này khá phức tạp để hiểu, vì nó liên tục chuyển đổi giữa cách nhìn khác nhau vào một ma trận bit; chắc chắn mất thời gian hơn để hiểu so với việc hiểu một giao thức mật mã như thường lệ của tôi. Nhưng một khi bạn hiểu về trường nhị phân, tin tốt là không có bất kỳ “toán khó” nào mà Binius phụ thuộc vào. Đây không phải là cặp đường cong elliptic, nơi có những hố thằn sâu hơn về hình học đại số để khám phá; ở đây, trường nhị phân là tất cả những gì bạn cần.

Hãy nhìn lại sơ đồ đầy đủ một lần nữa:

Tới thời điểm này, bạn nên quen thuộc với hầu hết các thành phần. Ý tưởng về việc “làm phẳng” một siêu khối thành lưới, ý tưởng về việc tính toán một tổ hợp hàng và một tổ hợp cột như là tích tensor của điểm đánh giá, và ý tưởng về việc kiểm tra sự tương đương giữa “mở rộng Reed-Solomon sau đó tính toán tổ hợp hàng”, và “tính toán tổ hợp hàng sau đó mở rộng Reed-Solomon”, đều trong Binius đơn giản.

Có gì mới trong "toàn bộ Binius"? Đơn giản là ba điều:

• Các giá trị cá nhân trong siêu khối và trong hình vuông phải là bit (0 hoặc 1)
• Quá trình mở rộng mã vào các bit khác nhau, bằng cách nhóm các bit vào các cột và tạm thời giả về chúng lón hơn.
• Sau bước kết hợp hàng, có bước "phân rã thành bit" từng phần tử, chuyển đổi phần mở rộng trở lại thành bit

Chúng tôi sẽ đi qua cả hai theo lần lượt. Đầu tiên, thủ tục mở rộng mới. Một mã Reed-Solomon có hạn chế cơ bản là nếu bạn đang mở rộng 𝑛 giá trị thành 𝑘∗𝑛 giá trị, bạn cần làm việc trong một trường có 𝑘∗𝑛 giá trị khác nhau mà bạn có thể sử dụng như tọa độ. Với 𝐹₂(hay còn gọi là bits), bạn không thể làm điều đó. Và vì vậy chúng tôi thực hiện việc “đóng gói” các 𝐹 kề nhau₂các phần tử lại với nhau thành các giá trị lớn hơn. Trong ví dụ này, chúng tôi đang đóng gói hai bit vào các phần tử trong {0,1,2,3}, vì phần mở rộng của chúng tôi chỉ có bốn điểm đánh giá và vì vậy đó là đủ cho chúng tôi. Trong một bằng chứng “thực sự”, chúng tôi có thể đóng gói 16 bit cùng một lúc. Sau đó, chúng tôi thực hiện mã Reed-Solomon trên các giá trị đã đóng gói này, và mở chúng ra trở lại thành các bit.

Bây giờ, kết hợp hàng. Để làm cho việc kiểm tra "đánh giá tại một điểm ngẫu nhiên" an toàn mật mã, chúng ta cần điểm đó được lấy mẫu từ một không gian khá lớn, lớn hơn nhiều so với siêu khối chính nó. Do đó, trong khi các điểm trong siêu khối là bit, các đánh giá bên ngoài siêu khối sẽ lớn hơn nhiều. Trong ví dụ của chúng tôi ở trên, "kết hợp hàng" kết thúc bằng [11,4,6,1].

Điều này đặt ra một vấn đề: chúng ta biết cách kết hợp các cặp bit thành một giá trị lớn hơn, sau đó thực hiện một phần mở rộng Reed-Solomon trên đó, nhưng làm thế nào để bạn làm điều tương tự với các cặp giá trị lớn hơn nhiều?

Bí quyết trong Binius là làm nó theo cách bit: chúng tôi nhìn vào từng bit của mỗi giá trị (ví dụ, với cái mà chúng tôi đánh dấu là “11”, đó là [1,1,0,1]), và sau đó chúng ta mở rộng theo hàng. Đó là, chúng tôi thực hiện quy trình mở rộng trên hàng 1 của mỗi phần tử, sau đó trên hàng 𝑥0, sau đó trên “𝑥”₁“ dòng, sau đó trên trục 𝑥₀∗𝑥₁ hàng, và cứ như vậy (vâng, trong ví dụ đồ chơi của chúng tôi, chúng tôi dừng lại ở đó, nhưng trong một bản triển khai thực tế, chúng tôi sẽ đi lên đến 128 hàng (hàng cuối cùng là 𝑥₆∗ …∗ 𝑥₀))

Tóm tắt:

• Chúng tôi lấy các bit trong siêu khối, và chuyển chúng thành lưới
• Sau đó, chúng tôi xử lý các nhóm bit kề nhau trên mỗi hàng như là các phần tử trường lớn hơn, và thực hiện phép tính trên chúng để mở rộng các hàng theo Reed-Solomon
• Sau đó, chúng tôi lấy một kết hợp hàng của mỗi cột bit, và nhận được một cột bit (cho các hình vuông lớn hơn 4x4, nhỏ hơn nhiều) cho mỗi hàng như đầu ra
• Sau đó, chúng tôi xem đầu ra như một ma trận và xem xét các bit của nó như là hàng một lần nữa

Tại sao điều này lại hoạt động? Trong toán học “bình thường”, khả năng thực hiện các phép toán tuyến tính theo bất kỳ thứ tự nào và đạt được kết quả giống nhau thường ngừng hoạt động nếu bạn bắt đầu cắt một số thành các chữ số. Ví dụ, nếu tôi bắt đầu với số 345, và nhân nó với 8 rồi nhân với 3, tôi được 8280, và nếu làm hai phép toán đó theo thứ tự ngược lại, tôi cũng được 8280. Nhưng nếu tôi chèn một phép toán “chia theo chữ số” giữa hai bước đó, nó sẽ ngừng hoạt động: nếu bạn làm 8x rồi 3x, bạn sẽ được:

Nhưng nếu bạn làm 3 lần, rồi sau đó là 8 lần, bạn sẽ nhận được:

Nhưng trong một lĩnh vực nhị phân được xây dựng với cấu trúc tháp, cách tiếp cận này hoạt động. Lý do nằm ở sự phân tách của chúng: nếu bạn nhân một giá trị lớn với một giá trị nhỏ, điều gì xảy ra trên mỗi đoạn giữ lại trên mỗi đoạn. Nếu chúng ta nhân 1100101010001111 với 11, điều này giống như sự phân tích yếu tố đầu tiên của 1100101010001111, đó chính là

Và sau đó nhân từng thành phần lẻ ra với 11.

Đặt tất cả vào một chỗ

Nói chung, các hệ thống chứng minh không có kiến thức hoạt động bằng cách đưa ra các tuyên bố về đa thức mà đồng thời đại diện cho các tuyên bố về các đánh giá cơ bản: giống như chúng ta đã thấy trong ví dụ về dãy Fibonacci, 𝐹(𝑋+2)−𝐹(𝑋+1)−𝐹(𝑋)=𝑍(𝑋)∗𝐻(𝑋) kiểm tra đồng thời tất cả các bước của việc tính Fibonacci. Chúng ta kiểm tra các tuyên bố về đa thức bằng cách chứng minh các đánh giá tại một điểm ngẫu nhiên. Việc kiểm tra này tại một điểm ngẫu nhiên đại diện cho việc kiểm tra toàn bộ đa thức: nếu phương trình đa thức không khớp, khả năng nó khớp tại một tọa độ ngẫu nhiên cụ thể là rất nhỏ.

Trong thực tế, một nguồn lớn của sự không hiệu quả đến từ việc trong các chương trình thực tế, hầu hết các số mà chúng ta đang làm việc đều rất nhỏ: chỉ số trong vòng lặp for, giá trị True/False, bộ đếm và các vấn đề tương tự. Nhưng khi chúng ta “mở rộng” dữ liệu bằng mã hóa Reed-Solomon để cung cấp sự dư thừa cần thiết để làm cho việc kiểm tra dựa trên chứng minh Merkle an toàn, hầu hết các giá trị “thêm” cuối cùng chiếm toàn bộ kích thước của một trường, ngay cả khi các giá trị ban đầu là nhỏ.

Để vượt qua điều này, chúng tôi muốn làm cho trường càng nhỏ càng tốt. Plonky2 đã giảm số bit từ 256 bit xuống còn 64 bit, và sau đó Plonky3 còn giảm xuống còn 31 bit. Nhưng ngay cả điều này cũng không phải là tối ưu. Với trường nhị phân, chúng ta có thể làm việc trên từng bit cá nhân. Điều này khiến việc mã hóa trở nên “dày đặc”: nếu dữ liệu cơ bản thực tế của bạn có n bit, thì mã hóa của bạn sẽ có n bit, và phần mở rộng sẽ có 8 * n bit, mà không có chi phí thêm.

Bây giờ, hãy nhìn vào biểu đồ lần thứ ba:

Trong Binius, chúng tôi cam kết đến một đa tuyến tính đa thức: một siêu khối 𝑃(x₀,x₁,…x_k), trong đó cá nhân đánh giá P (0,0 ... 0), P (0,0... 1) lên đến P (1,1,... 1) đang nắm giữ dữ liệu mà chúng tôi quan tâm. Để chứng minh một đánh giá tại một điểm, chúng tôi "diễn giải lại" cùng một dữ liệu dưới dạng hình vuông. Sau đó, chúng tôi mở rộng mỗi hàng, sử dụng mã hóa Reed-Solomon trên các nhóm bit, để cung cấp cho dữ liệu dự phòng cần thiết cho các truy vấn nhánh Merkle ngẫu nhiên được bảo mật. Sau đó, chúng tôi tính toán một tổ hợp tuyến tính ngẫu nhiên của các hàng, với các hệ số được thiết kế sao cho hàng kết hợp mới thực sự giữ đánh giá mà chúng tôi quan tâm. Cả hàng mới được tạo này (được diễn giải lại thành 128 hàng bit) và một vài cột được chọn ngẫu nhiên với các nhánh Merkle, đều được chuyển đến trình xác minh.

Người xác minh sau đó thực hiện một “kết hợp hàng của phần mở rộng” (hoặc chính xác hơn là một số cột của phần mở rộng), và một “phần mở rộng của kết hợp hàng”, và xác minh rằng hai phần này khớp nhau. Họ sau đó tính toán một kết hợp cột, và kiểm tra xem nó trả về giá trị mà người chứng minh đang tuyên bố. Và đó là hệ thống chứng minh của chúng ta (hoặc chính xác hơn là hệ thống cam kết đa thức, là khối xây dựng chính của hệ thống chứng minh).

Chúng ta đã không đề cập đến điều gì?

• Các thuật toán hiệu quả để mở rộng các hàng, cần thiết để thực sự tăng hiệu suất tính toán của bộ xác minh. Chúng tôi sử dụng các biến đổi Fourier nhanh trên các trường nhị phân, được mô tả Ở đây(mặc dù việc triển khai chính xác sẽ khác nhau, vì bài đăng này sử dụng một cấu trúc không hiệu quả hơn không dựa trên mở rộng đệ quy).
• Số học. Đa thức đơn biến thuận tiện vì bạn có thể làm những việc như F(X+2)-F(X+1)-F(X) = Z(X)*H(X) để liên hệ các bước liền kề trong phép tính. Trong một hypercube, "bước tiếp theo" ít được giải thích hơn nhiều so với "X + 1". Bạn có thể làm X + k, sức mạnh của k, nhưng hành vi nhảy này sẽ hy sinh nhiều lợi thế chính của Binius. Giải pháp được trình bày trong Binius paper (Xem Mục 4.3), nhưng điều này là một lỗ thỏ sâu trong chính nó.
• Làm thế nào để thực sự an toàn khi kiểm tra giá trị cụ thể. Ví dụ về Fibonacci yêu cầu kiểm tra các điều kiện biên của khóa: F(0)=F(1)=1 và giá trị của F(100). Nhưng với Binius “nguyên thủy”, việc kiểm tra tại các điểm đánh giá trước đã biết là không an toàn. Có những cách khá đơn giản để chuyển đổi kiểm tra đánh giá đã biết thành kiểm tra đánh giá không biết, bằng cách sử dụng những giao thức kiểm tra tổng; nhưng chúng tôi không bàn về những điều đó ở đây.
• Các giao thức tìm kiếm, một công nghệ khác đang ngày càng được sử dụng gần đây như một cách để tạo ra các hệ thống chứng minh siêu hiệu quả. Binius có thể kết hợp với các giao thức tìm kiếm cho nhiều ứng dụng.
• Vượt xa thời gian xác minh căn bậc hai. Căn bậc hai tốn kém: một bằng chứng Binius của bits khoảng 11 MB. Bạn có thể khắc phục điều này bằng cách sử dụng một hệ thống chứng minh khác để tạo ra một "chứng minh của một bằng chứng Binius", từ đó đạt được cả hiệu suất chứng minh của Binius trong câu lệnh chính và kích thước chứng minh nhỏ. Một lựa chọn khác là giao thức phức tạp hơn nhiều FRI-Binius, tạo ra một chứng minh có kích thước đa logarit (giống như FRI thông thường).
• Làm thế nào Binius ảnh hưởng đến việc gì được coi là “SNARK-friendly”. Tóm tắt cơ bản là, nếu bạn sử dụng Binius, bạn không cần quan tâm nhiều đến việc làm cho việc tính toán “arithmetic-friendly”: các băm “thường” không còn hiệu quả hơn các băm toán học truyền thống, phép nhân modulo hoặc modulo không còn là một nỗi đau đầu lớn so với phép nhân modulo , và cứ thế. Nhưng đây là một chủ đề phức tạp; rất nhiều thứ thay đổi khi mọi thứ được thực hiện trong hệ nhị phân.

Tôi mong đợi nhiều cải tiến hơn trong các kỹ thuật chứng minh dựa trên trường nhị phân trong những tháng sắp tới.

免责声明：

1. Bài viết này được tái bản từ [ Panews]. Chuyển tiêu đề gốc 'Vitalik解Binius：基于二进制字段的高效证明系统'. Tất cả bản quyền thuộc về tác giả gốc [GateVitalik Buterin*]. Nếu có ý kiến phản đối về việc tái bản, vui lòng liên hệ Cổng Họcđội ngũ, và họ sẽ xử lý nhanh chóng.
2. Bản Khai Báo Miễn Trừ Trách Nhiệm: Các quan điểm và ý kiến được thể hiện trong bài viết này chỉ thuộc về tác giả và không hình thành bất kỳ lời khuyên đầu tư nào.
3. Các bản dịch của bài viết sang các ngôn ngữ khác được thực hiện bởi nhóm Gate Learn. Trừ khi được nêu, việc sao chép, phân phối hoặc đạo văn các bài viết dịch là không được phép.