1,096 lượt đọc

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

từ tác giả Sin7Y2022/06/21

dài quá đọc không nổi

TinyRAM là một Máy tính Tập lệnh Rút gọn (RISC) đơn giản 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). 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.

Companies Mentioned

Coin Mentioned

featured image - 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

và : lệnh and ri rj A 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à 0 ^ {W} , hãy đặt flag thành 1, và nếu không thì đặt cờ thành 0.
hoặc lệnh or ri rj A 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à 0 ^ {W} , hãy đặt flag thành 1, và nếu không thì đặt cờ thành 0.
Lệnh xor xor ri rj A 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à 0 ^ {W} , hãy đặt flag thành 1, và nếu không thì đặt cờ thành 0.
not not ri A 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à 0 ^ {W} , hãy đặt flag thành 1, và nếu không thì đặt cờ thành 0.

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 flag thành 1 và nếu không thì đặt cờ thành 0.

Trong phần sau, U_ {W} đạ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. S_ {W} đạ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.

add: lệnh add ri rj A 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 G = [rj] _u + [A] _u . Ngoài ra, flag sẽ được đặt thành G_ {W} . G_ {W} là bit quan trọng nhất (MSB) của G.
sub: hướng dẫn sub ri rj A 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 G = [rj] _u + 2 ^ W - [A] _u . Ngoài ra, flag sẽ được đặt thành 1 − G_ {W} . G_ {W} là bit quan trọng nhất (MSB) của G.
lệnh mull mull ri rj A 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 G = [rj] _u ∗ [A] _u . Ngoài ra, flag sẽ được đặt thành 1 nếu
[rj] _u × [A] u ∉ U {W} , và nếu không thì đặt nó thành 0.
lệnh umulh umulh ri rj A 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 G = [rj] _u ∗ [A] _u . Ngoài ra, flag sẽ được đặt thành 1 nếu [rj] _u × [A] u ∉ U {W} , và nếu không thì đặt nó thành 0.
Lệnh smulh smulh ri rj A sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri. a_ {W − 1} là bit dấu của [rj] u ∗ [A] u, a {W − 2} ⋯ a {0} là W − 1 MSB của [rj] _u ∗ [A] _u . Ngoài ra, flag sẽ được đặt thành 1 nếu [rj] _u × [A] u ∉ S {W }, và nếu không thì đặt nó thành 0.

udiv thể udiv ri rj A sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri.

Nếu [A] u = 0, a {W − 1} ⋯ a_ {0} = 0 ^ W.

Nếu [A] u∣ ≠ 0, a {W − 1} ⋯ a_ {0} là mã nhị phân duy nhất của số nguyên Q, làm cho một số nguyên R ∈ {0,…, [A] _u - 1} , công thức [rj] _u = [A] _u × Q + R là khả thi. Ngoài ra, chỉ khi [A] _u = 0 , flag sẽ được đặt thành 1.

lệnh umod umod ri rj A sẽ lưu chuỗi W-bit a_ {W − 1} ⋯ a_ {0} vào ri.

Nếu [A] u = 0, a {W − 1} ⋯ a_ {0} = 0 ^ W.

Nếu [A] u∣ ≠ 0, a {W − 1} ⋯ a_ {0} là mã nhị phân duy nhất của số nguyên R, có phạm vi giá trị là

{0,…, [A] _u − 1} , làm cho công thức [rj] _u = [A] _u × Q + R có thể thay đổi được đối với một số giá trị Q. Ngoài ra, chỉ khi [A] _u = 0 , flag sẽ được đặt thành 1.

Hoạt động liên quan đến ca làm việc

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 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 shr shr 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].

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 cmpe cmpe ri A sẽ đặt cờ thành 1 nếu [ri] = [A], và nếu không thì đặt cờ thành 0
lệnh cmpa cmpa ri A sẽ đặt cờ thành 1 nếu [ri] _u> [A] _u , và nếu không thì đặt nó thành 0
lệnh cmpae cmpae ri A sẽ đặt cờ thành 1 nếu [ri] _u ≥ [A] _u , và nếu không thì đặt cờ thành 0
lệnh cmpg cmpg ri A sẽ đặt cờ thành 1 nếu [ri] _s> [A] _s , và nếu không thì đặt nó thành 0
lệnh cmpge cmpge ri A sẽ đặt cờ thành 1 nếu [ri] _S ≥ [A] _S , và nếu không thì đặt cờ thành 0

Hoạt động liên quan đến di chuyển

lệnh mov mov ri A sẽ lưu [A] vào thanh ghi ri.
lệnh cmov cmov ri A 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.

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à flag , nhưng sẽ sửa đổi pc .

jmp A hướng dẫn nhảy A sẽ lưu trữ [A] vào máy tính.
lệnh cjmp cjmp A sẽ lưu trữ [A] vào pc khi flag = 1, và nếu không thì tăng pc lên 1
cnjmp hướng dẫn cnjmp A sẽ lưu trữ [A] vào pc khi flag = 0 và nếu không thì tăng pc lên 1

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 store.b store A ri sẽ lưu trữ LSB của [ri] tại địa chỉ byte thứ [A] trong bộ nhớ.
Lệnh load.b load ri A 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 store.w store.w A ri sẽ lưu trữ [ri] ở vị trí từ được căn chỉnh với byte thứ [A] trong bộ nhớ.
Lệnh load.w load.w ri A đã lưu từ trong bộ nhớ của nó được căn chỉnh với byte [A] w vào thanh ghi ri.

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 read read ri A 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 flag = 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 flag = 1.

Vì TinyRAM chỉ có hai băng đầu vào, tất cả băng ngoại trừ hai đầu tiên được cho là trố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 flag = 1.

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.

câu trả lời hướng dẫn answer A 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.

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 S của giá trị tích bên trong đều phù hợp với các ràng buộc R1CS A_i, B_i , C_i biểu diễn vector hàng trong ma trận).

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

và công thức ràng buộc:

 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<FieldT>( { 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<FieldT>( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag"));

hoặc công thức ràng buộ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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag"));

không phải công thức ràng buộc:

 1 * （1 - b） = c

Các bước ràng buộc cụ thể như sau:

 this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { 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<FieldT>( { 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

add: công thức ràng buộc:
```
 1 * （a + b） = c
```
Các bước ràng buộc cụ thể như sau:
1. Ràng buộc quy trình tính toán, mã như sau:
```
 this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result"));
```
1. Ràng buộc kết quả giải mã và ràng buộc boolean
2. Ràng buộc kết quả mã hóa

sub: 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 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<FieldT> a, b, c; a.add_term(0, 1); for (size_t i = 0; i < this->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<FieldT>(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:
1. Những hạn chế của phép nhân tính toán
2. Ràng buộc của việc mã hóa kết quả tính toán
3. Gắn cờ các ràng buộc của kết quả tính toán
udiv và công thức ràng buộc umod:

 B * q + r = A r <= B

'B' là số chia, 'q' là thương và 'r' là số dư. Số dư không được vượt quá số chia. Các mã ràng buộc cụ thể như sau:

 /* B_inv * B = B_nonzero */ linear_combination<FieldT> 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<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination<FieldT> 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<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination<FieldT> 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<FieldT>(a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination<FieldT> 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<FieldT>(a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination<FieldT> 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<FieldT>(a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A<B_gadget<FieldT>(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 flag . So sánh các hướng dẫn bao gồm cmpe , cmpa , cmpae . cmpg và cmpge , 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 comparison_gadget sánh_gadget đã nhận ra của libsnark trong lõi quy trình ràng buộc của chúng.

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<FieldT>( {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<FieldT>( {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<FieldT>( {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 flag , 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:
```
 this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {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<FieldT>( {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<FieldT>( {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à flag nhưng sẽ sửa đổi 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<FieldT>( { ONE }, { pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, this->pc.packed + 1 - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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).

store.b và 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<FieldT>(opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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"));

load.b và 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<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum<FieldT>( pb_variable_array<FieldT>(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, flag được đặt thành 1
Nếu lệnh read 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
Đọc nội dung từ bên ngoài type1, flag được đặt thành 1
Cho dù result là 0 có nghĩa là flag là 0

Mã giới hạn:

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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à answer và giá trị arg2 là 0.

Mã giới hạn như sau:

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 ppt đánh giá tinyram , 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.

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.