Bộ hướng dẫn TinyRAM là gì?

Giới thiệu TinyRAM là một Máy tính Tập lệnh Rút gọn đơn giản (RISC) với bộ nhớ truy cập ngẫu nhiên có địa chỉ cấp 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 (hv), và một theo kiến trúc von Neumann (vn) (trong bài viết này, chúng tôi chủ yếu tập trung vào kiến trúc von Neumann). Dự án Nghiên cứu về tính toàn vẹn và quyền riêng tư của Succinct (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ế để mang lại hiệu quả trong cài đặt này. Nó tạo ra sự cân bằng giữa hai yêu cầu đối lập - "đủ khả năng diễn đạt" và "tập hợp hướng dẫn nhỏ": Đủ khả năng diễn đạt để hỗ trợ mã lắp ráp ngắn, hiệu quả khi được biên dịch từ các ngôn ngữ lập trình cấp cao, Tập lệnh nhỏ để hỗ trợ xác minh đơn giản thông qua các mạch số học và xác minh hiệu quả bằng cách sử dụng các thuật toán và cơ chế mật mã của SCIPR. Trong bài viết này, chúng tôi sẽ bổ sung cho bài viết trước chứ không phải là phần giới thiệu TinyRAM lặp lại, sau đó tập trung vào phần giới thiệu các hướng dẫn và các ràng buộc mạch. Để biết phần giới thiệu cơ bản về TinyRAM, vui lòng tham khảo bài viết trước của chúng tôi: tinyram 简介 - 中文 TinyRAM Review-English Bộ hướng dẫn TinyRAM TinyRAM hỗ trợ 29 lệnh, mỗi lệnh được chỉ định bởi một opcode và tối đa 3 toán hạng. Toán hạng có thể là tên của một thanh ghi (tức là các số nguyên từ 0 đến K-1) hoặc một giá trị tức thời (tức là các chuỗi W-bit). Trừ khi được chỉ định khác, mỗi lệnh không sửa đổi cờ riêng biệt và tăng pc theo i (i% 2 ^ W) theo mặc định, i = 2W / 8 cho vnTinyRAM. Nói chung, toán hạng đầu tiên là thanh ghi đích để tính toán lệnh và các toán hạng khác chỉ định các tham số theo yêu cầu của lệnh. Cuối cùng, tất cả các lệnh cần một chu kỳ của máy để thực hiện. Hoạt động liên quan đến bit : lệnh sẽ lưu các bit và kết quả của [rj] và [A] trong thanh ghi ri. Ngoài ra, nếu kết quả là , hãy đặt thành 1, và nếu không thì đặt cờ thành 0. và and ri rj A 0 ^ {W} flag lệnh sẽ lưu trữ các bit và kết quả của [rj] và [A] trong thanh ghi ri. Ngoài ra, nếu kết quả là , hãy đặt thành 1, và nếu không thì đặt cờ thành 0. hoặc or ri rj A 0 ^ {W} flag sẽ lưu các bit và kết quả của [rj] và [A] trong thanh ghi ri. Ngoài ra, nếu kết quả là , hãy đặt thành 1, và nếu không thì đặt cờ thành 0. Lệnh xor xor ri rj A 0 ^ {W} flag sẽ lưu các bit và kết quả của [rj] và [A] trong thanh ghi ri. Ngoài ra, nếu kết quả là , hãy đặt thành 1, và nếu không thì đặt cờ thành 0. not not ri A 0 ^ {W} flag Hoạt động liên quan đến số nguyên Đây là các phép toán liên quan đến số nguyên không dấu và có dấu khác nhau. Trong mỗi cài đặt, nếu xảy ra lỗi hoặc lỗi tràn số học (chẳng hạn như chia cho 0), hãy đặt thành 1 và nếu không thì đặt cờ thành 0. flag Trong phần sau, đại diện cho một chuỗi các số nguyên {0 *,…, * $ 2 ^ {W} -1 $}; Các số nguyên này được tạo thành từ các chuỗi W-bit. đại diện cho một chuỗi các số nguyên {−2 ^ (W − 1),… 0, 1, $ 2 ^ $} {} W - 1-1. Các số nguyên này cũng được tạo thành từ các chuỗi W-bit. U_ {W} S_ {W} lệnh sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} ⋯ a_ {0} là W bit có ý nghĩa nhất (LSB) của . Ngoài ra, sẽ được đặt thành . là bit quan trọng nhất (MSB) của G. add: add ri rj A G = [rj] _u + [A] _u flag G_ {W} G_ {W} hướng dẫn sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} ⋯ a_ {0} là W bit nhỏ nhất có nghĩa (LSB) của . Ngoài ra, sẽ được đặt thành . là bit quan trọng nhất (MSB) của G. sub: sub ri rj A G = [rj] _u + 2 ^ W - [A] _u flag 1 − G_ {W} G_ {W} lệnh sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} ⋯ a_ {0} là bit W nhỏ nhất có nghĩa (LSB) của . Ngoài ra, sẽ được đặt thành 1 nếu mull mull ri rj A G = [rj] _u ∗ [A] _u flag , và nếu không thì đặt nó thành 0. [rj] _u × [A] {W} u ∉ U lệnh sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} ⋯ a_ {0} là W bit quan trọng nhất (MSB) của . Ngoài ra, sẽ được đặt thành 1 nếu , và nếu không thì đặt nó thành 0. umulh umulh ri rj A G = [rj] _u ∗ [A] _u flag [rj] _u × [A] {W} u ∉ U sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} là bit dấu của là W − 1 MSB của . Ngoài ra, sẽ được đặt thành 1 nếu }, và nếu không thì đặt nó thành 0. Lệnh smulh smulh ri rj A [rj] {W − 2} ⋯ a {0} u ∗ [A] u, a [rj] _u ∗ [A] _u flag [rj] _u × [A] {W u ∉ S sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. udiv thể udiv ri rj A Nếu [A] {W − 1} ⋯ a_ {0} = 0 ^ W. u = 0, a Nếu là mã nhị phân duy nhất của số nguyên Q, làm cho một số nguyên , công thức là khả thi. Ngoài ra, chỉ khi , sẽ được đặt thành 1. [A] {W − 1} ⋯ a_ {0} u∣ ≠ 0, a R ∈ {0,…, [A] _u - 1} [rj] _u = [A] _u × Q + R [A] _u = 0 flag lệnh sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. umod umod ri rj A Nếu [A] {W − 1} ⋯ a_ {0} = 0 ^ W. u = 0, a Nếu có phạm vi giá trị là [A] {W − 1} ⋯ a_ {0} u∣ ≠ 0, a là mã nhị phân duy nhất của số nguyên R, , làm cho công thức có thể thay đổi được đối với một số giá trị Q. Ngoài ra, chỉ khi , sẽ được đặt thành 1. {0,…, [A] _u − 1} [rj] _u = [A] _u × Q + R [A] _u = 0 flag Hoạt động liên quan đến ca làm việc sẽ lưu chuỗi bit W thu được bằng cách dịch chuyển sang trái [rj] cho [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 0. Ngoài ra, cờ được đặt thành MSB của [rj]. Lệnh shl shl ri rj A sẽ lưu chuỗi bit W thu được bằng cách dịch chuyển sang phải [rj] cho bit [A] u trong thanh ghi ri. Các vị trí trống sau khi dịch chuyển được lấp đầy bằng 0. Ngoài ra, cờ được đặt thành LSB của [rj]. Lệnh shr shr ri rj A Hoạt động liên quan đến so sánh Mỗi lệnh trong thao tác liên quan đến so sánh không sửa đổi bất kỳ thanh ghi nào; Kết quả so sánh sẽ được lưu trong . flag lệnh sẽ đặt cờ thành 1 nếu [ri] = [A], và nếu không thì đặt cờ thành 0 cmpe cmpe ri A lệnh sẽ đặt cờ thành 1 nếu , và nếu không thì đặt nó thành 0 cmpa cmpa ri A [ri] _u> [A] _u lệnh sẽ đặt cờ thành 1 nếu , và nếu không thì đặt cờ thành 0 cmpae cmpae ri A [ri] _u ≥ [A] _u lệnh sẽ đặt cờ thành 1 nếu , và nếu không thì đặt nó thành 0 cmpg cmpg ri A [ri] _s> [A] _s lệnh sẽ đặt cờ thành 1 nếu , và nếu không thì đặt cờ thành 0 cmpge cmpge ri A [ri] _S ≥ [A] _S Hoạt động liên quan đến di chuyển lệnh sẽ lưu [A] vào thanh ghi ri. mov mov ri A lệnh sẽ lưu [A] vào thanh ghi ri nếu flag = 1 và nếu không giá trị của thanh ghi ri sẽ không thay đổi. cmov cmov ri A Liên quan đến bước nhảy Các lệnh nhảy và nhảy có điều kiện này sẽ không sửa đổi thanh ghi và , nhưng sẽ sửa đổi . flag pc hướng dẫn A sẽ lưu trữ [A] vào máy tính. jmp A nhảy lệnh sẽ lưu trữ [A] vào pc khi = 1, và nếu không thì tăng pc lên 1 cjmp cjmp A flag hướng dẫn sẽ lưu trữ [A] vào pc khi = 0 và nếu không thì tăng pc lên 1 cnjmp cnjmp A flag Hoạt động liên quan đến bộ nhớ Đây là các hoạt động tải bộ nhớ đơn giản và các hoạt động lưu trữ, trong đó địa chỉ của bộ nhớ được xác định bởi số tức thời hoặc nội dung của thanh ghi. Đây là những phương pháp giải quyết duy nhất trong TinyRAM. (TinyRAM không hỗ trợ chế độ định địa chỉ “cơ sở + bù đắp” phổ biến). Lưu trữ lệnh sẽ lưu trữ LSB của [ri] tại địa chỉ byte thứ [A] trong bộ nhớ. store.b store A ri sẽ lưu nội dung của địa chỉ byte thứ [A] U trong bộ nhớ vào thanh ghi ri (điền 0 vào các byte phía trước). Lệnh load.b load ri A lệnh sẽ lưu trữ [ri] ở vị trí từ được căn chỉnh với byte thứ [A] trong bộ nhớ. store.w store.w A ri đã lưu từ trong bộ nhớ của nó được căn chỉnh với byte [A] w vào thanh ghi ri. Lệnh load.w load.w ri A Hoạt động liên quan đến đầu vào Hướng dẫn này là chỉ dẫn duy nhất có thể truy cập một trong hai cuộn băng. Băng thứ 0 được sử dụng cho đầu vào chính và băng đầu tiên cho đầu vào phụ của người dùng. lệnh sẽ lưu từ W-bit tiếp theo trên băng [A] U vào thanh ghi ri. Nói chính xác hơn, nếu băng [A] u có bất kỳ từ còn lại nào, từ tiếp theo sẽ được sử dụng và lưu trữ trong ri, và đặt = 0; Ngược lại (nếu không có từ nhập còn lại nào trên băng [A] u), hãy lưu trữ 0 ^ W thành ri và đặt = 1. read read ri A flag flag Vì TinyRAM chỉ có hai băng đầu vào, tất cả ngoại trừ hai đầu tiên được cho là trống. băng Cụ thể, nếu [A] u không phải là 0 hoặc 1, thì chúng ta lưu trữ 0 ^ W trong ri và đặt = 1. flag Hoạt động liên quan đến đầu ra Hướng dẫn này có nghĩa là chương trình đã hoàn tất quá trình tính toán của nó và không có hoạt động nào khác được phép. hướng dẫn sẽ làm cho máy trạng thái “đơ” (không tăng máy tính) hoặc “tạm dừng” (dừng tính toán) và quay trở lại [A] u. Sự lựa chọn giữa dừng hoặc dừng không được xác định. Giá trị trả về 0 được sử dụng để biểu thị sự chấp nhận. câu trả lời answer A Ràng buộc của Bộ hướng dẫn TinyRAM đã sử dụng ràng buộc R1CS để thực hiện các ràng buộc mạch và dạng cụ thể như sau: (Ai ∗ S) ∗ (Bi ∗ S) - Ci ∗ S = 0 Bây giờ, nếu chúng ta muốn chứng minh rằng chúng ta biết một nghiệm của phép tính ban đầu, chúng ta sẽ cần chứng minh rằng trong ma trận A, B và C, mọi vectơ hàng và vectơ nghiệm của giá trị tích bên trong đều phù hợp với các ràng buộc R1CS biểu diễn vector hàng trong ma trận). S A_i, B_i , C_i Mỗi ràng buộc R1CS có thể được biểu diễn bằng tổ hợp tuyến tính a, b hoặc c. Phép gán của 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ụ. Phần chính là cái mà chúng ta thường gọi là “tuyên bố” và phần bổ trợ là “nhân chứng”. Mỗi hệ thống ràng buộc R1CS chứa nhiều ràng buộc R1CS. Độ dài vectơ cho 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). TinyRAM đã sử dụng rất nhiều gadgte tùy chỉnh trong việc triển khai mã libsnark để thể hiện các ràng buộc vm cũng như thực thi opcode và các ràng buộc bộ nhớ. Mã cụ thể nằm trong thư mục gadgetslib1 / Gadgets / cpu_checkers / tinyram. Ràng buộc liên quan đến bit công thức ràng buộc: và a * b = c Ràng buộc R1CS của và xác minh tham số 1 và tham số 2 và kết quả tính toán là phép nhân từng bit. Các bước ràng buộc như sau: Ràng buộc quy trình tính toán và mã như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] }, { this->arg2val.bits[i] }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); Ràng buộc mã hóa kết quả Kết quả tính toán không phải là tất cả các ràng buộc bằng 0 (phù hợp với định nghĩa lệnh và quá trình chủ yếu là chuẩn bị cờ ràng buộc) /* the gadgets below are Fp specific: I * X = R (1-R) * X = 0 if X = 0 then R = 0 if X != 0 then R = 1 and I = X^{-1} */ Cờ hạn chế /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); công thức ràng buộc: hoặc (1 - a) * (1 - b) = (1 - c) Các bước ràng buộc cụ thể như sau: Ràng buộc quy trình tính toán và mã như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE, this->arg1val.bits[i] * (-1) }, { ONE, this->arg2val.bits[i] * (-1) }, { ONE, this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); Ràng buộc mã hóa kết quả Kết quả tính toán không phải là tất cả các ràng buộc bằng 0 (phù hợp với định nghĩa lệnh và quá trình này chủ yếu là để chuẩn bị cho cờ ràng buộc) Cờ hạn chế /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); công thức ràng buộc : xor c = a ^ b c = a + b - 2*a*b, (2*b)*a = a+b - c Các bước ràng buộc cụ thể như sau: Ràng buộc quy trình tính toán và mã như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] * 2}, { this->arg2val.bits[i] }, { this->arg1val.bits[i], this->arg2val.bits[i], this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); Ràng buộc mã hóa kết quả Kết quả tính toán không phải là tất cả các ràng buộc bằng 0 (phù hợp với định nghĩa lệnh và quá trình này chủ yếu là để chuẩn bị cho cờ ràng buộc) Cờ hạn chế /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); công thức ràng buộc: không phải 1 * （1 - b） = c Các bước ràng buộc cụ thể như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->arg2val.bits[i] * (-1) }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); Ràng buộc mã hóa kết quả Kết quả tính toán không phải là tất cả các ràng buộc bằng 0 (phù hợp với định nghĩa lệnh và quá trình này chủ yếu là để chuẩn bị cho cờ ràng buộc) Cờ hạn chế /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); Ràng buộc hoạt động liên quan đến số nguyên công thức ràng buộc: add: 1 * （a + b） = c Các bước ràng buộc cụ thể như sau: Ràng buộc quy trình tính toán, mã như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); Ràng buộc kết quả giải mã và ràng buộc boolean Ràng buộc kết quả mã hóa công thức ràng buộc: sub: Ràng buộc phụ phức tạp hơn một chút so với ràng buộc cộng, với một biến trung gian đại diện cho kết quả ab và 2 ^ w được thêm vào để đảm bảo rằng kết quả được tính dưới dạng một số nguyên dương và một dấu. Các bước ràng buộc cụ thể như sau: intermediate_result = 2^w + a -b Ràng buộc quy trình tính toán: /* intermediate_result = 2^w + (arg1val - arg2val) */ FieldT twoi = FieldT::one(); linear_combination a, b, c; a.add_term(0, 1); for (size_t i = 0; i pb.ap.w; ++i) { twoi = twoi + twoi; } b.add_term(0, twoi); b.add_term(this->arg1val.packed, 1); b.add_term(this->arg2val.packed, -1); c.add_term(intermediate_result, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a, b, c), FMT(this->annotation_prefix, " main_constraint")); Ràng buộc kết quả giải mã và ràng buộc boolean Dấu hiệu ràng buộc bit công thức ràng buộc : mull, umulh và smulh c = a * b Tất cả các ràng buộc liên quan đến Mull đều bao gồm các bước sau: Những hạn chế của phép nhân tính toán Ràng buộc của việc mã hóa kết quả tính toán Gắn cờ các ràng buộc của kết quả tính toán công thức ràng buộc umod: udiv và B * q + r = A r a1, b1, c1; a1.add_term(B_inv, 1); b1.add_term(this->arg2val.packed, 1); c1.add_term(B_nonzero, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination a2, b2, c2; a2.add_term(ONE, 1); a2.add_term(B_nonzero, -1); b2.add_term(this->arg2val.packed, 1); c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination a3, b3, c3; a3.add_term(this->arg2val.packed, 1); b3.add_term(udiv_result, 1); c3.add_term(A_aux, 1); c3.add_term(umod_result, -; this->pb.add_r1cs_constraint(r1cs_constraint (a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination a4, b4, c4; a4.add_term(this->arg1val.packed, 1); b4.add_term(B_nonzero, 1); c4.add_term(A_aux, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination a5, b5, c5; a5.add_term(udiv_result, 1); b5.add_term(ONE, 1); b5.add_term(B_nonzero, -1); c5.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A (B, r, less=B_nonzero, leq=ONE) */ r_less_B->generate_r1cs_constraints(); So sánh hoạt động Mỗi lệnh trong các thao tác so sánh sẽ không sửa đổi bất kỳ thanh ghi nào; Kết quả so sánh được lưu trong . So sánh các hướng dẫn bao gồm , , . và , có thể được chia thành hai loại: so sánh số có dấu và so sánh số không có dấu, cả hai đều sử dụng sánh_gadget đã nhận ra của libsnark trong lõi quy trình ràng buộc của chúng. flag cmpe cmpa cmpae cmpg cmpge comparison_gadget Công thức ràng buộc so sánh số không có dấu: cmpe_flag = cmpae_flag * (1-cmpa_flag) cmp và mã ràng buộc như sau: comparator.generate_r1cs_constraints(); this->pb.add_r1cs_constraint( r1cs_constraint ( {cmpae_result_flag}, {ONE, cmpa_result_flag * (-1)}, {cmpe_result_flag}), FMT(this->annotation_prefix, " cmpa_result_flag")); Công thức ràng buộc so sánh số có dấu: Ràng buộc số không dấu phức tạp hơn ràng buộc so sánh số có dấu vì có nhiều xử lý ràng buộc bit dấu hơn. Ràng buộc bit dấu như sau: /* negate sign bits */ this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg1val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg1val_sign}), FMT(this->annotation_prefix, " negated_arg1val_sign")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg2val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg2val_sign}), FMT(this->annotation_prefix, " negated_arg2val_sign")); Các bước còn lại giống như ràng buộc so sánh số có dấu. Di chuyển giới hạn hoạt động công thức ràng buộc : mov Ràng buộc mov tương đối đơn giản vì nó chỉ cần đảm bảo rằng [A] được lưu trữ trong thanh ghi ri. Thao tác mov sẽ không sửa đổi , do đó, ràng buộc cần đảm bảo rằng giá trị cờ không thay đổi. Mã ràng buộc như sau: flag this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " mov_result_flag")); công thức ràng buộc : cmov flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval Điều kiện ràng buộc của cmov phức tạp hơn mov, bởi vì các hành vi của mov liên quan đến sự thay đổi của giá trị cờ và cmov sẽ không sửa đổi cờ, do đó, ràng buộc cần đảm bảo rằng giá trị của cờ không thay đổi và mã như sau: /* flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval */ this->pb.add_r1cs_constraint( r1cs_constraint ( {this->flag}, {this->arg2val.packed, this->desval.packed * (-1)}, {this->result, this->desval.packed * (-1)}), FMT(this->annotation_prefix, " cmov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " cmov_result_flag")); Ràng buộc hoạt động nhảy Các lệnh nhảy và nhảy có điều kiện này sẽ không sửa đổi các thanh ghi và nhưng sẽ sửa đổi . flag pc rung rinh Giá trị pc phù hợp với kết quả thực thi của lệnh trong ràng buộc hoạt động Jmp và mã ràng buộc cụ thể như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) }, { this->result }), FMT(this->annotation_prefix, " jmp_result")); cjmp cjmp sẽ nhảy theo điều kiện cờ khi cờ = 1, và nếu không thì tăng pc lên 1. Công thức ràng buộc như sau: flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1 Mã ràng buộc như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) - this->pc.packed - 1, this->result - this->pc.packed - 1), FMT(this->annotation_prefix, " cjmp_result")); cnjmp Cnjmp sẽ nhảy theo điều kiện cờ. Nếu cờ = 0, PC sẽ nhảy và ngược lại, tăng pc lên 1. Công thức ràng buộc như sau: flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2 Mã ràng buộc như sau: this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, this->pc.packed + 1 - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end()))), FMT(this->annotation_prefix, " cnjmp_result")); Hạn chế hoạt động bộ nhớ Đây là các hoạt động tải và lưu trữ bộ nhớ đơn giản, trong đó địa chỉ của bộ nhớ được xác định bởi số tức thời hoặc nội dung của một thanh ghi. Đây là những phương pháp giải quyết duy nhất trong TinyRAM. (TinyRAM không hỗ trợ chế độ định địa chỉ “cơ sở + bù đắp” phổ biến). và store.b store.w Đối với store.w, lấy tất cả các giá trị của arg1val và đối với opcodes store.b, chỉ lấy phần cần thiết của arg1val (ví dụ: byte cuối cùng) và mã ràng buộc như sau: this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint (1 - (opcode_indicators[tinyram_opcode_STOREB] + opcode_indicators[tinyram_opcode_STOREW]), ls_prev_val_as_doubleword_variable->packed - ls_next_val_as_doubleword_variable->packed, 0), FMT(this->annotation_prefix, " non_store_instructions_dont_change_memory")); và load.b load.w Đối với hai hướng dẫn này, chúng tôi yêu cầu nội dung được tải từ bộ nhớ phải được lưu trữ trong lệnh_results và mã ràng buộc như sau: this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADB], memory_subcontents - instruction_results[tinyram_opcode_LOADB], 0), FMT(this->annotation_prefix, " handle_loadb")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADW], memory_subcontents - instruction_results[tinyram_opcode_LOADW], 0), FMT(this->annotation_prefix, " handle_loadw")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum ( pb_variable_array (desval->bits.begin(), desval->bits.begin() + 8)), 0), FMT(this->annotation_prefix, " handle_storeb")); Ràng buộc hoạt động đầu vào đọc Thao tác đọc liên quan đến băng và các ràng buộc cụ thể như sau: Khi hết đoạn băng trước và có nội dung cần đọc, thì băng sau không được phép đọc. Khi băng trước đó kết thúc và có nội dung để đọc, được đặt thành 1 flag Nếu lệnh hiện được sử dụng, thì nội dung bắt đọc phù hợp với nội dung đầu vào của băng read Đọc nội dung từ bên ngoài type1, được đặt thành 1 flag Cho dù là 0 có nghĩa là là 0 result flag Mã giới hạn: this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - next_tape1_exhausted, 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_next_tape1_exhausted")); this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint (read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (instruction_flags[tinyram_opcode_READ], instruction_results[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " read_flag_implies_result_0")); Ràng buộc hoạt động đầu ra Hướng dẫn này chỉ ra rằng chương trình đã hoàn thành quá trình tính toán của nó và do đó không cho phép hoạt động nào nữa câu trả lời Khi giá trị đầu ra của chương trình được chấp nhận, has_accepted được đặt thành 1 và giá trị trả về của chương trình được chấp nhận bình thường, có nghĩa là lệnh hiện tại là và giá trị arg2 là 0. answer Mã giới hạn như sau: this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, arg2val->packed, 0), FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero")); Khác Tất nhiên, ngoài một số ràng buộc liên quan đến lệnh đã đề cập ở trên, TinyRAM còn có một số ràng buộc về tính nhất quán của pc, codec tham số, kiểm tra bộ nhớ,… Các ràng buộc này được kết hợp thông qua hệ thống R1CS để tạo thành một hệ thống ràng buộc TinyRAM hoàn chỉnh. Do đó, đây là nguyên nhân gốc rễ tại sao một số lượng lớn các ràng buộc TinyRAM được tạo ra dưới dạng R1CS. Ở đây chúng tôi đề cập đến một hình , cho thấy mức tiêu thụ thời gian cần thiết để chuyển ERC20 để tạo ra bằng chứng thông qua TinyRAM. ppt đánh giá tinyram Có thể kết luận từ ví dụ trên: không thể xác minh tất cả các hoạt động EVM bằng vnTinyRam + zk-SNARks và nó chỉ phù hợp để xác minh tính toán một số lượng nhỏ các lệnh. VnTinyram có thể được sử dụng để xác minh opcode cho các loại tính toán từng phần của EVM.