Các Kỹ Thuật Phát Triển Mạch Từ Halo2

Chức Năng

flowchart LR Người Chứng Minh-->|Nhập/Xuất/Chứng Nhận|Người Xác Thực ‍♂️Người Chứng Minh: Cung cấp Nhập/Xuất/Chứng Nhận 👩‍💼 Người Xác Thực: Không tái thực hiện tính toán, nhưng tin rằng kết quả tính toán đúng

  1. Giai Đoạn Chuẩn Bị (Phát Triển)
  • ‍💻Phát Triển Viên: Định nghĩa hằng số
  • ‍💻Phát Triển Viên: Gửi khóa cho 💁‍♂️Người Chứng Minh và 👩‍💼Người Xác Thực
  1. Giai Đoạn Xác Thực
  • ‍♂️Người Chứng Minh: Điền vào quá trình tính toán
  • ‍♂️Người Chứng Minh: Tạo chứng nhận
  • ‍💼Người Xác Thực: Xác thực chứng nhận

Khó Khăn - Sự Khác Biệt Giữa Phát Triển Mạch Và Phát Triển Thông Thường

  • ‍💻Phát Triển Thông Thường: Sử dụng biến, nhánh, vòng lặp, hàm để thiết kế logic
  • ‍💻Phát Triển Mạch: Sử dụng bảng, mô tả mối quan hệ giữa các ô để định nghĩa ràng buộc
  • Đại Số Hóa
  • Quá Trình Tính Toán

Luật Chơi

Phép Tính Trong Trường Hữu Hạn

  • Chứng chỉ nhỏ hơn p
  • Ví dụ p=3
  • Thì 2 + 2 = 1 (mod 3)
  • p thường là một số rất lớn, ví dụ 254bit

Bố Trí Quá Trình Tính Toán Sử Dụng Bảng

  • Ô: Có thể điền phần tử trường
  • Cột: Cột bổ sung sẽ tăng chi phí xác thực/chứng nhận thêm
  • Hàng: Sử dụng bao nhiêu tùy ý, thường giới hạn trong 2^18 hàng.

Loại Cột

  • Advice: Cột hướng dẫn (nhập), dùng bởi 💁‍♂️Người Chứng Minh, điền dữ liệu riêng tư trong giai đoạn chứng nhận, chỉ 💁‍♂️Người Chứng Minh nhìn thấy.
  • Fixed: Cột hằng số, 👨‍💻Phát Triển Viên đặt giá trị cố định trong giai đoạn phát triển, 👩‍💼Người Xác Thực nhìn thấy
  • Instance: Cột thực thể (xuất), dùng bởi 💁‍♂️Người Chứng Minh, điền dữ liệu công khai trong giai đoạn chứng nhận, 👩‍💼Người Xác Thực nhìn thấy
  1. Giai Đoạn Phát Triển
  • ‍💻Phát Triển Viên thiết lập cột Fixed
  1. Giai Đoạn Chứng Nhận
  • ‍♂️Người Chứng Minh điền quá trình tính toán
  • Điền cột Advice
  • Điền cột Instance
  • Tạo chứng nhận
  1. Giai Đoạn Xác Thực
  • Xác thực cột Fixed, cột Instance (kết quả) và chứng nhận

Ràng Buộc: Giá Trị Trong Ô Là Hiệu Lực?

Ràng Buộc Cửa Tùy Chỉnh: Định Nghĩa Ràng Buộc Trong Đa Thức

// Ví dụ đa thức tùy chỉnh
function custom_gate(x) {
    return (x - 1) * (x - 2) * (x - 3);
}
  • Trong ràng buộc cửa, biểu thức chứa Selector là cột Fixed, ví dụ 0 hoặc 1, để vô hiệu hóa hoặc kích hoạt ràng buộc cửa trên dòng đó.
  • Trong ràng buộc cửa, có thể tham chiếu đến ô trước hoặc sau, thậm chí ô cách 20 dòng, nhưng tốn kém kzg opening.

Ví Dụ Ràng Buộc Cửa Tùy Chỉnh - Dãy Fibonacci

Có thể sử dụng 4 cột

Hoặc cũng có thể sử dụng 3 cột

Ràng Buộc Sao Chép / Kiểm Tra Bằng Nhau

  • Ràng buộc sao chép liên kết hai ô, giá trị phân phối phải giống nhau.
  • Ràng buộc rẻ nhất. Sử dụng càng nhiều càng tốt.
  • Vị trí ô được xác định trong giai đoạn chuẩn bị, không thể thay đổi khi chứng nhận.

Quy Tắc: Người Chứng Minh Có Thể Ác Ý

Kỹ Thuật

Giới Hạn Tùy Chọn

Giới Hạn Giá Trị Ô

  • Muốn: Giá trị ô chỉ có thể là 1, 2, 3
  • Biểu Thức Cửa: (x-1)*(x-2)*(x-3) = 0

Chuyển Đổi If-else

def foo(a: int, b: int, happy: bool):
    if happy:
        return a + b
    else:
        return a * b

Biểu Thức Cửa: `happy * (a+b) + (1-happy) * (a*b) - output = 0`

Chuyển Đổi Vòng Lặp For

def foo(n: int):
    r = 0
    for _ in range(n):
        r += 5
    return r

Quá Trình Tính Toán

  • Không có hàng vô hạn để lưu trữ n, do đó phải giới hạn giá trị tối đa của n, ví dụ 5
  • Sao chép ô
  • r0 == const0: Giá trị ban đầu của r đặt trong cột Fixed
  • r5 === out1: Cột đầu tiên của int/out là đầu vào (Người Xác Thực), thứ hai là đầu ra (Người Xác Thực), tức kết quả hàng tối đa và giá trị xuất tương đương.

Thêm Một Cột Selector Chỉ Người Chứng Minh Thấy Được

s: Cột chọn (Advice) - chỉ Người Chứng Minh thấy r: Kết quả bước (Advice) - chỉ Người Chứng Minh thấy in/out: Đầu vào/Đầu ra (Instance) - Người Xác Thực thấy, chỉ sử dụng hai hàng

  • Biểu Thức Ràng Buộc Cửa: s * (r_next -r - 5) * (1-s)(r_next - r) = 0

Tức là: - Nếu chọn 1: Kết quả hàng tiếp theo = Kết quả hàng hiện tại + 5 - Nếu chọn 0: Kết quả hàng tiếp theo = Kết quả hàng hiện tại

Nhưng điều này có lỗ hổng - nếu dòng selector = 0 không liên tục, ví dụ:

Kỹ Thuật Chuyển Đổi Trạng Thái

stateDiagram-v2 direction LR [] --> Add [] --> Pad Add --> Add Add --> Pad Pad --> Pad Pad --> [*] > Add: Tính toán+5

Pad: Điền kết quả cuối cùng

Biểu Thức Ràng Buộc Cửa:

  • s *(r_next-r-5)*(1-s)(r_next-r)=0

Selector s nên là kiểu boolean

  • s * (1-s) == 0

Nếu selector hiện tại là 0, thì selector hàng tiếp theo cũng phải là 0

  • (1-s) s_next = 0

Điểm Cuối: Thêm Kiểm Tra Đầu Vào

  • Đầu vào in là dãy số nguyên liên tiếp hoặc không thay đổi: s (in_next -in -1) + (1-s)(in_next-in)=0
  • Kết quả hàng tiếp theo là hàng hiện tại +5 hoặc không thay đổi: s *(r_next-r-5)*(1-s)(r_next-r)=0
  • Selector s nên là boolean: s * (1-s) == 0
  • Nếu selector hiện tại là 0, thì selector hàng tiếp theo cũng phải là 0: (1-s) s_next = 0

Tại Sao Chúng Ta Làm Tất Cả Điều Này?

  • Trong CPU, chúng ta có tập lệnh, mỗi chu kỳ chạy một lệnh.
  • Khi có if/else, chỉ thực hiện một đường dẫn.
  • Trong mạch số học, không có vòng lặp! Phải "phẳng" tất cả các đường dẫn khả thi và "chạy" đồng thời, loại bỏ đường dẫn không cần bằng nhân với 0.

Mang Đi Không Cần Cảm Ơn

  • Thách thức đối với nhà phát triển mạch
  • Sử dụng "theo dõi tính toán" thay vì thực thi: Cần phẳng hóa đường dẫn
  • Sử dụng đại số trường thay vì bit và byte: Cần xử lý toán học và phương trình.
  • Sử dụng tư duy xác thực: Cần ngăn chặn người chứng minh gian lận
  • Kỹ thuật
  • ràng buộc if-else giá trị boolean và ràng buộc s*(true path) +(1-s)*(false path)
  • Vòng lặp phức tạp: Nhận diện chuyển đổi trạng thái và thiết kế ràng buộc.

Thẻ: Halo2 MạchSốHọc RàngBuộcCửa VòngLặp

Đăng vào ngày 11 tháng 6 lúc 08:04

Thẻ Phổ Biến

©2026 Thành phố Cuồng loạn