ระบบพิสูจน์สิ้นเชิงของ Miden

Sin7y

特邀专栏作者

2022-10-11 08:38

บทความนี้มีประมาณ 2722 คำ การอ่านทั้งหมดใช้เวลาประมาณ 4 นาที

บทความนี้อธิบายรายละเอียดของสถาปัตยกรรมระบบพิสูจน์ miden

ชื่อระดับแรก

สถาปัตยกรรมระบบพิสูจน์ Miden

miden เป็นการใช้งาน zkvm โดยใช้เทคโนโลยี strark เลเยอร์ด้านล่างขึ้นอยู่กับไลบรารี zkp ของ Winterfell เพื่อสร้างการพิสูจน์ที่ชัดเจนและตรวจสอบการพิสูจน์ เส้นประในรูปที่ 1 ด้านล่างเป็นฟังก์ชันหลักที่ Miden นำมาใช้ จะเห็นได้ว่ามีส่วนประกอบหลักๆ อยู่ 3 ส่วนด้วยกัน

1. ชุดของคอมไพเลอร์ไวยากรณ์คำศัพท์ ตัววิเคราะห์คำศัพท์ และตัวแยกวิเคราะห์ไวยากรณ์ในรูปที่ 1 ด้านล่าง พวกเขาสามารถตั้งโปรแกรมคำสั่งประกอบที่กำหนดโดย miden เป็น opcode และค่า op ที่มีอยู่ใน codeblock และ block

3. ชุดของ AIR (Algebraic Intermediate Representation) ที่ตรงตามข้อกำหนดการพิสูจน์โดยสิ้นเชิง AIR ในรูปที่ 1 ด้านล่าง ใช้เพื่อจำกัดกระบวนการดำเนินการของเครื่องเสมือนของ miden

ชื่อระดับแรก

การออกแบบโครงสร้าง AIR

ข้อจำกัดของ AIR แบ่งออกเป็นสองส่วน: สแต็กและตัวถอดรหัส:

รูปที่ 3 แสดงข้อจำกัดของตัวถอดรหัส ในหมู่พวกเขา op_counter, op_sponge, cf_op_bits, ld_op_bits, hd_op_bits เป็นความยาวคอลัมน์คงที่ ในหมู่พวกเขา op_sponge ใช้เพื่อจำกัดลำดับและความถูกต้องของการดำเนินการคำสั่ง cf_op_bits จำกัด 3 บิต flow_ops ld_op_bits, hd_op_bits จำกัด 5 บิตต่ำและสูง 2 บิตของ user_ops ตามลำดับ การรวมกันของ ld_op_bits และ hd_op_bits ถือเป็น user_op ที่ดำเนินการ และยังใช้เป็นตัวเลือกสำหรับข้อจำกัดสถานะแต่ละขั้นตอนของสแต็ก

ชื่อระดับแรก

อินสแตนซ์การดำเนินการของ Miden VM

ส่วนนี้จะแสดงตรรกะ miden อย่างง่ายเพื่อแสดงกระบวนการดำเนินการของ vm และการสร้างการติดตามการดำเนินการของสิ้นเชิง

ส่วนรหัส 1 ด้านล่างเป็นส่วนรหัสที่จะดำเนินการ:

ตรรกะที่ดำเนินการคือกด 3 และ 5 ลงบนสแต็ก จากนั้นอ่านธงจากเทป กำหนดว่าแฟล็กเป็น 1 หรือ 0 หากเป็น 1 ให้รัน if.true branch เพื่อนำเลข 3 และ 5 สองตัวที่ผลักออกจากสแต็ก มาบวกกันเพื่อให้ได้ 8 แล้วดันกลับเข้าไปในสแต็ก หากเป็น 0 ให้เรียกใช้สาขาอื่นเพื่อดึงตัวเลขสองตัว 3 และ 5 ที่ถูกผลักออกจากสแต็กและคูณพวกมันเพื่อให้ได้ 15 จากนั้นดัน 15 กลับเข้าไปในสแต็ก

รหัสคำสั่งสุดท้ายหลังจากแบ่งส่วนของรหัสโดยตัววิเคราะห์คำศัพท์และไวยากรณ์ของ miden มีดังนี้ ส่วนของรหัส 2:

รูปที่ 4 ด้านล่างแสดงกระบวนการ vm รันโค้ดเซกเมนต์ 2 ตรงกลางคือแผนผังลำดับงานของ executor ที่กำลังเรียกใช้ opcode เส้นประทางด้านซ้ายชี้ไปที่ร่องรอยการถอดรหัสที่สร้างขึ้นโดยการใช้โค้ด และเส้นประทางด้านขวาชี้ไปที่ การติดตามสแต็กที่สร้างขึ้นโดยการเรียกใช้โค้ด

ในหมู่พวกเขาตัวดำเนินการจะถูกดำเนินการทีละตัวตามบล็อกรหัส ในตัวอย่างนี้ span block จะถูกดำเนินการก่อน จากนั้นดำเนินการโครงสร้าง if-else-end ในขั้นตอนที่ 32 เพื่อเข้าสู่บล็อก swtich และกดแฮชฟองน้ำที่สร้างโดยขั้นตอนสุดท้ายของบล็อกช่วงก่อนหน้าลงใน ctx_stack และหลังจากดำเนินการบล็อก swtich แล้ว ที่ขั้นตอน 49 ป๊อปเข้าไปใน ฟองน้ำ.

หมายเหตุ: เอกสารนี้อธิบายเวอร์ชันล่าสุดของสาขาหลักสำหรับโครงการ miden ในปัจจุบัน สาขาถัดไปของ miden ได้ออกแบบคำสั่งจำนวนมากใหม่ และ AIR ปรับใช้ข้อจำกัดเพียงเล็กน้อยเท่านั้น

ข้อ จำกัด ของสแต็ก

คำสั่งแบบมีเงื่อนไข

Choose

Constrain:

ข้อความ

add

Constrain:

mul

Constrain:

inv

Constrain:

neg

Constrain:

คำสั่งบูลีน

not

Constrain:

and

Constrain:

คำสั่งแฮช

RESCR

ข้อความ

ครอบครอง 6 การลงทะเบียน

Constrain:

คำสั่งเปรียบเทียบ

Constrain:

cmp

ข้อความ

A: [0,1,0,1]

B: [0,0,1,1]

ต้องเปรียบเทียบ 4 ครั้ง

Constrain:

ข้อความ

dup.n

Constrain:

swap

Constrain:

ROLL4

Constrain:

ชื่อระดับแรก

ข้อจำกัดในการถอดรหัส

การดำเนินการรหัสผู้ใช้

op_bits

ข้อความ

ข้อจำกัดสำหรับ cf_op_bits, ld_op_bits, hd_op_bits

ข้อ จำกัด 1: แต่ละบิตสามารถเป็น 0 หรือ 1 เท่านั้น

ข้อจำกัด 2: เมื่อ op_counter ไม่ใช่ 0, ld_ops และ hd_ops จะเป็น 0 พร้อมกันไม่ได้

ข้อจำกัด 3: เมื่อ cf_op_bits เป็น hacc สถานะ op_counter จะเพิ่มขึ้นทีละ 1

ข้อจำกัดที่ 4: คำสั่ง BEGIN, LOOP, BREAK และ WRAP ต้องการการจัดตำแหน่ง 16 ตำแหน่ง

ข้อ จำกัด 6: คำสั่ง PUSH ต้องการการจัดตำแหน่ง 8

hacc

hacc ใช้เป็น flowOps การดำเนินการคำสั่งนี้แต่ละครั้งจะทำให้สถานะของฟองน้ำเปลี่ยนไป ซึ่งจำเป็นต้องจำกัด

การตัดสินแบบมีเงื่อนไข

t_end

ข้อความ

ข้อจำกัดที่เป็นจุดสิ้นสุดของสาขาจริงของ if แบ่งออกเป็นสองส่วน:

ข้อจำกัด 1: ข้อจำกัดของสถานะฟองน้ำ ค่าที่ด้านบนของป็อปอัพสแต็กจะเท่ากับ new_sponge_0 ฟองน้ำหลังจากดำเนินการขั้นตอนสุดท้ายของสาขาจริงของ if เท่ากับ new_sponge_1 new_sponge_3 เท่ากับ 0

ข้อ จำกัด 3: ข้อ จำกัด ของ loop_stack สถานะของ loop_stack จะไม่เปลี่ยนแปลง

f_end

ข้อความ

เนื่องจากข้อจำกัดที่ส่วนท้ายของสาขาปลอมของ if จะแบ่งออกเป็นสองส่วน:

Sin7y ก่อตั้งขึ้นในปี 2564 และประกอบด้วยนักพัฒนาบล็อกเชนชั้นนำ เราเป็นทั้งผู้บ่มเพาะโครงการและทีมวิจัยเทคโนโลยีบล็อกเชน สำรวจเทคโนโลยีที่สำคัญและล้ำสมัยที่สุด เช่น EVM, Layer2, cross-chain, การประมวลผลเพื่อความเป็นส่วนตัว และโซลูชันการชำระเงินอัตโนมัติ