Giới thiệu
tiêu đề cấp đầu tiên
Giới thiệu
Tinyram là một cỗ máy truy cập ngẫu nhiên RISC đơn giản với bộ nhớ truy cập ngẫu nhiên có thể định địa chỉ byte và các băng đầu vào. Có hai biến thể của TinyRAM: một theo kiến trúc Harvard và một theo kiến trúc von Neumann (trong bài này chúng ta chủ yếu thảo luận về kiến trúc von Neumann).
Dự án Nghiên cứu tính toàn vẹn và quyền riêng tư của máy tính ngắn gọn (SCIPR) đã xây dựng các cơ chế để chứng minh việc thực thi chính xác các chương trình TinyRAM và TinyRAM được thiết kế để hoạt động hiệu quả trong trường hợp này. Nó tạo ra sự cân bằng giữa các mặt đối lập của "đủ biểu cảm" và "đủ đơn giản":
• Đủ biểu cảm để hỗ trợ mã hợp ngữ ngắn và hiệu quả khi được biên dịch từ ngôn ngữ lập trình cấp cao.Giới thiệu về TinyRam
Giới thiệu về TinyRam
tiêu đề cấp đầu tiên
Tập lệnh Tinyram
Tinyram có tổng cộng 29 lệnh và mỗi lệnh bao gồm một mã lệnh và tối đa ba toán hạng. Toán hạng có thể là tên của một thanh ghi (một số nguyên từ 0 đến K-1) hoặc một giá trị tức thời (chuỗi W bit). Trừ khi có quy định khác, các hướng dẫn không sửa đổi các cờ riêng lẻ. Mỗi lệnh tăng pc lên i (i % 2^W) theo mặc định, đối với vnTinyram i= 2W/8.
Nói chung, toán hạng đầu tiên là thanh ghi đích để tính toán lệnh, các toán hạng khác chỉ định các tham số theo yêu cầu của lệnh và cuối cùng, tất cả các lệnh yêu cầu một chu kỳ của máy để thực thi.
thao tác bit
phép toán số nguyên
• shlĐây là các phép toán số nguyên không dấu và có dấu khác nhau. Trong mỗi trường hợp, cờ được đặt thành 1 nếu xảy ra lỗi hoặc tràn số học (chẳng hạn như chia cho 0) và thành 0 nếu không.
• shrhoạt động thay đổi
Lệnh shl ri rj A lưu trữ chuỗi W-bit thu được bằng cách dịch trái [rj] bởi [A]u bit vào thanh ghi ri. Các vị trí trống sau khi dịch chuyển được lấp đầy bằng các số 0. Ngoài ra, cờ được đặt thành bit quan trọng nhất của [rj].
Lệnh shr ri rj A lưu trữ chuỗi W-bit thu được bằng cách dịch phải [rj] bởi [A]u bit trong thanh ghi ri. Các vị trí trống sau khi dịch chuyển được lấp đầy bằng các số 0. Ngoài ra, cờ được đặt thành bit ít quan trọng nhất của [rj].
thao tác so sánh
• movMỗi hướng dẫn trong thao tác so sánh không sửa đổi bất kỳ thanh ghi nào; kết quả so sánh được lưu trữ trong cờ.
• cmovdi chuyển hoạt động
Lệnh mov ri A lưu [A] vào thanh ghi ri.
Lệnh cmov ri A Nếu cờ = 1, lưu [A] vào thanh ghi ri. Nếu không, giá trị của thanh ghi ri sẽ không bị thay đổi.
• jmpThao tác nhảy
• cjmpCác hướng dẫn nhảy và nhảy có điều kiện này không sửa đổi các thanh ghi và cờ nhưng sửa đổi máy tính.
• cnjmp Lệnh jmp A lưu trữ [A] vào máy tính.
Lệnh cjmp A lưu trữ [A] trong pc với điều kiện cờ = 1, nếu không thì pc được tăng thêm 1.
Lệnh cnjmp A lưu trữ [A] trong pc với điều kiện cờ = 0, nếu không thì pc được tăng thêm 1.
hoạt động bộ nhớ
Đây là các hoạt động lưu trữ và tải bộ nhớ đơn giản, trong đó địa chỉ của bộ nhớ được xác định bởi một giá trị tức thời hoặc nội dung của một thanh ghi. Đây là các chế độ địa chỉ duy nhất trong tinyram. (tinyram không hỗ trợ chế độ địa chỉ "base+offset" phổ biến).
hoạt động đầu vào
hoạt động đầu ra
Lệnh này cho biết chương trình đã tính toán xong nên không được phép thực hiện thêm thao tác nào nữa.
tiêu đề cấp đầu tiên
ràng buộc tập lệnh
Tinyram sử dụng dạng ràng buộc R1CS cho các ràng buộc mạch, dạng cụ thể như sau:
Một ràng buộc R1CS có thể có ba biểu diễn tổ hợp tuyến tính của a, b và c. Việc gán tất cả các biến trong hệ thống R1CS có thể được chia thành hai phần: đầu vào chính và đầu vào phụ. Chính là những gì chúng ta thường gọi là "tuyên bố". phụ trợ là "nhân chứng".
Một hệ thống ràng buộc R1CS chứa nhiều ràng buộc R1CS. Độ dài vectơ của mỗi ràng buộc là cố định (kích thước đầu vào chính + kích thước đầu vào phụ + 1).
• andTinyram sử dụng rất nhiều tiện ích tùy chỉnh trong quá trình triển khai mã của libsnark để thể hiện các ràng buộc của vm và các ràng buộc của bộ nhớ và thực thi opcode. Mã cụ thể nằm trong thư mục gadgetslib1/gadgets/cpu_checkers/tinyram.
ràng buộc thao tác bit
Công thức ràng buộc:
R1CS ràng buộc và xác minh tham số 1 và tham số 2 và kết quả tính toán từng chút một cho phép tính nhân.Các bước ràng buộc như sau:
1. Quá trình tính toán ràng buộc, mã như sau:
2. Ràng buộc mã hóa kết quả
• or3. Kết quả tính toán không phải là tất cả 0 ràng buộc (giữ phù hợp với định nghĩa của hướng dẫn, quá trình này chủ yếu là để chuẩn bị cho cờ ràng buộc)
ràng buộc 4.flag
Công thức ràng buộc:
Các bước ràng buộc cụ thể như sau:
1. Quá trình tính toán ràng buộc, mã như sau:
2. Ràng buộc mã hóa kết quả (tương tự như trên)
• xor3. Kết quả tính toán không phải là tất cả các ràng buộc 0 (hãy tuân theo định nghĩa của hướng dẫn, quá trình này chủ yếu là để chuẩn bị cho cờ ràng buộc) (tương tự như trên)
4.flag ràng buộc (giống như trên)
Công thức ràng buộc:
Các bước ràng buộc cụ thể như sau:
•not1. Quá trình tính toán ràng buộc, mã như sau:
Bước 2, 3, 4 như trên
Công thức ràng buộc:
Các bước ràng buộc cụ thể như sau:
•addBước 2, 3, 4 như trên
Ràng buộc thao tác số nguyên
: Công thức ràng buộc:
Các bước ràng buộc cụ thể như sau:
1. Quá trình tính toán ràng buộc, mã như sau:
•sub2. Giải mã ràng buộc kết quả và ràng buộc boolean
3. Các ràng buộc về kết quả mã hóa
: Công thức ràng buộc:
Ràng buộc phụ phức tạp hơn một chút so với add. Một biến trung gian được sử dụng để biểu thị kết quả của a - b. Đồng thời, 2^w được thêm vào kết quả để đảm bảo rằng phép tính kết quả được thể hiện dưới dạng số nguyên dương và ký hiệu. Các bước ràng buộc cụ thể như sau:
1. Ràng buộc quy trình tính toán
•mull 、umulh、smulh2. Giải mã ràng buộc kết quả và ràng buộc boolean
3. Ràng buộc bit dấu
Công thức ràng buộc:
Các ràng buộc liên quan đến Mull bao gồm các bước sau
1. Tính toán các ràng buộc nhân
•udiv 、umod2. Ràng buộc mã hóa kết quả tính toán
Công thức ràng buộc:
B là số chia, q là thương và r là số dư. Tổng còn lại phải đáp ứng điều kiện là nó không thể vượt quá số chia. Mã ràng buộc cụ thể như sau:
• shl、shrtiêu đề phụ
ràng buộc hoạt động thay đổi
công thức ràng buộccmpe、 cmpa 、cmpae、cmpg、cmpgethao tác so sánh
. Các hướng dẫn so sánh có thể được chia thành hai loại, cụ thể là so sánh các số có dấu và so sánh các số không dấu. Cốt lõi của quy trình ràng buộc của cả hai sử dụng so sánh_gadget được triển khai trong libsnark.
Phần còn lại của quy trình giống như đối với các ràng buộc so sánh có dấu
• movtiêu đề phụ
di chuyển các ràng buộc hoạt động
• cmovCông thức ràng buộc:
Công thức ràng buộc:
Các ràng buộc của cmov phức tạp hơn của mov, hành vi chính của mov liên quan đến việc thay đổi giá trị của cờ, đồng thời, cmov sẽ không sửa đổi cờ, vì vậy ràng buộc cần đảm bảo rằng giá trị của cờ không thay đổi không thay đổi Mã của cmov như sau:
tiêu đề phụ
• jmp
Ràng buộc thao tác nhảy
• cjmp
Các hướng dẫn nhảy và nhảy có điều kiện này không sửa đổi các thanh ghi và cờ nhưng sửa đổi máy tính.
Hoạt động Jmp ràng buộc giá trị pc nhất quán với kết quả thực hiện lệnh. Mã ràng buộc cụ thể như sau:
cjmp nhảy theo điều kiện cờ, cờ = 1 để nhảy, ngược lại pc tăng 1
• cnjmp
Công thức ràng buộc như sau:
Mã ràng buộc như sau:
cnjmp nhảy theo điều kiện cờ, cờ = 0 để nhảy, ngược lại pc tăng 1
Công thức ràng buộc như sau:
Ràng buộc hoạt động bộ nhớ
• store.b Và store.w
Đây là các hoạt động lưu trữ và tải bộ nhớ đơn giản, trong đó địa chỉ của bộ nhớ được xác định bởi một giá trị tức thời hoặc nội dung của một thanh ghi. Đây là các chế độ địa chỉ duy nhất trong tinyram. (tinyram không hỗ trợ chế độ địa chỉ "base+offset" phổ biến).
Và
Đối với store.w, giá trị của toàn bộ arg1val được lấy và đối với store.b, opcode sẽ chỉ lấy phần cần thiết của arg1val (ví dụ: byte cuối cùng). Mã ràng buộc như sau:
• load.b và load.w
• read
Đối với hai hướng dẫn này, nội dung mà chúng tôi yêu cầu tải từ bộ nhớ được lưu trữ trong hướng dẫn_kết quả.Mã ràng buộc như sau:
Các ràng buộc hoạt động đầu vào
Thao tác đọc có liên quan đến băng và các quy tắc ràng buộc cụ thể là:
1. Nội dung trong băng trước đã được đọc, không có nội dung để đọc, và băng tiếp theo sẽ không được đọc.
2. Nội dung trong băng trước đã được đọc, không có nội dung để đọc và cờ được đặt thành 1
3. Nếu lệnh đang thực hiện được đọc, thì nội dung được đọc bằng cách đọc phù hợp với nội dung đầu vào của băng
5. Kết quả không phải là 0, có nghĩa là cờ là 0
Mã ràng buộc:
tiêu đề phụ
• answer
Ràng buộc hoạt động đầu ra
Khi giá trị đầu ra của chương trình được chấp nhận, has_accepted sẽ được đặt thành 1 và giá trị trả về của chương trình có thể được chấp nhận bình thường có nghĩa là lệnh hiện tại là answner và giá trị arg2 là 0.
khác
Mã ràng buộc như sau:
Từ ví dụ trong hình trên, có thể kết luận rằng không thể xác minh tất cả các hoạt động của EVM bằng vnTinyram + zk-SNARKs và nó chỉ phù hợp để xác minh tính toán xác minh của một số ít hướng dẫn. Bạn có thể sử dụng vnTinyram để xác minh opcode của một số kiểu tính toán của EVM.
về chúng tôi
tiêu đề cấp đầu tiên
về chúng tôi
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
IOS
Android