การแนะนำ

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

การแนะนำ

Tinyram เป็นเครื่องเข้าถึงโดยสุ่ม RISC อย่างง่ายพร้อมหน่วยความจำเข้าถึงโดยสุ่มแบบไบต์แอดเดรสได้และเทปอินพุต TinyRAM มีสองรูปแบบ: หนึ่งรูปแบบตามสถาปัตยกรรม Harvard และอีกรูปแบบหนึ่งตามสถาปัตยกรรม von Neumann (ในบทความนี้เราจะกล่าวถึงสถาปัตยกรรม von Neumann เป็นหลัก)

โครงการ Concise Computational Integrity and Privacy Research (SCIPR) ได้สร้างกลไกเพื่อพิสูจน์การดำเนินการที่ถูกต้องของโปรแกรม TinyRAM และ TinyRAM ได้รับการออกแบบให้มีประสิทธิภาพในกรณีนี้ มันสร้างความสมดุลระหว่างสิ่งที่ตรงกันข้ามของ "การแสดงออกเพียงพอ" และ "เรียบง่ายเพียงพอ":

• การแสดงออกที่เพียงพอเพื่อรองรับรหัสแอสเซมบลีที่สั้นและมีประสิทธิภาพเมื่อคอมไพล์จากภาษาโปรแกรมระดับสูงรู้เบื้องต้นเกี่ยวกับ TinyRam

รู้เบื้องต้นเกี่ยวกับ TinyRam

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

ชุดคำสั่ง Tinyram

Tinyram มีทั้งหมด 29 คำสั่ง และแต่ละคำสั่งประกอบด้วย opcode และตัวถูกดำเนินการสูงสุดสามตัว ตัวถูกดำเนินการสามารถเป็นชื่อของรีจิสเตอร์ (จำนวนเต็มระหว่าง 0 ถึง K-1) หรือค่าทันที (สตริงของ W บิต) คำแนะนำจะไม่แก้ไขแฟล็กทีละรายการ เว้นแต่จะระบุไว้เป็นอย่างอื่น แต่ละคำสั่งจะเพิ่ม pc ขึ้น i (i % 2^W) ตามค่าเริ่มต้น สำหรับ vnTinyram i= 2W/8

โดยทั่วไป ตัวถูกดำเนินการตัวแรกคือรีจิสเตอร์เป้าหมายสำหรับการคำนวณคำสั่ง ส่วนตัวถูกดำเนินการอื่นๆ จะระบุพารามิเตอร์ที่คำสั่งต้องการ และสุดท้าย คำสั่งทั้งหมดต้องการรอบการทำงานของเครื่องหนึ่งรอบ

การจัดการบิต

การดำเนินการจำนวนเต็ม

• shlนี่คือการดำเนินการจำนวนเต็มที่ไม่ได้ลงนามและลงนาม ในแต่ละกรณี แฟล็กจะถูกตั้งค่าเป็น 1 หากเกิดเลขคณิตเกินหรือข้อผิดพลาด (เช่น การหารด้วยศูนย์) และตั้งค่าเป็น 0 มิฉะนั้น

• shrเปลี่ยนการทำงาน

คำสั่ง shl ri rj A เก็บสตริง W-bit ที่ได้จากการเลื่อน [rj] ไปทางซ้ายโดย [A]u bit ลงใน ri register ตำแหน่งที่ว่างหลังจากการขยับจะถูกเติมด้วย 0 วินาที นอกจากนี้ยังตั้งค่าสถานะเป็นบิตที่สำคัญที่สุดของ [rj]

คำสั่ง shr ri rj A เก็บสตริง W-bit ที่ได้จากการเลื่อนขวา [rj] โดย [A]u บิตใน ri register ตำแหน่งที่ว่างหลังจากการขยับจะถูกเติมด้วย 0 วินาที นอกจากนี้แฟล็กยังตั้งค่าเป็นบิตที่มีนัยสำคัญน้อยที่สุดของ [rj]

การดำเนินการเปรียบเทียบ

• movแต่ละคำแนะนำในการดำเนินการเปรียบเทียบไม่ได้แก้ไขการลงทะเบียนใด ๆ ผลลัพธ์ของการเปรียบเทียบจะถูกเก็บไว้ในแฟล็ก

• cmovการดำเนินการย้าย

คำสั่ง mov ri A เก็บ [A] ไว้ใน ri register

คำสั่ง cmov ri A ถ้าแฟล็ก = 1 ให้เก็บ [A] ไว้ในรีจิสเตอร์ ri มิฉะนั้นค่าของรีจิสเตอร์ ri จะไม่เปลี่ยนแปลง

• jmpการดำเนินการกระโดด

• cjmpคำแนะนำการกระโดดและการข้ามแบบมีเงื่อนไขเหล่านี้ไม่ได้แก้ไขการลงทะเบียนและแฟล็ก แต่แก้ไขพีซี

• cnjmp คำสั่ง jmp A เก็บ [A] ลงในพีซี

คำสั่ง cjmp A เก็บ [A] ใน pc ภายใต้เงื่อนไขของ flag = 1 มิฉะนั้น pc จะเพิ่มขึ้น 1

คำสั่ง cnjmp A เก็บ [A] ใน pc ภายใต้เงื่อนไขของ flag = 0 มิฉะนั้น pc จะเพิ่มขึ้นทีละ 1

การทำงานของหน่วยความจำ

การดำเนินการเหล่านี้เป็นการโหลดและจัดเก็บหน่วยความจำอย่างง่าย โดยที่แอดเดรสของหน่วยความจำถูกกำหนดโดยค่าทันทีหรือเนื้อหาของรีจิสเตอร์ นี่เป็นโหมดการกำหนดแอดเดรสเพียงโหมดเดียวใน Tinyram (tinyram ไม่รองรับโหมดการกำหนดแอดเดรส "base+offset" ทั่วไป)

การดำเนินการอินพุต

การทำงานของเอาต์พุต

คำสั่งนี้บ่งชี้ว่าโปรแกรมเสร็จสิ้นการคำนวณแล้ว ดังนั้นจึงไม่อนุญาตให้ดำเนินการใดๆ เพิ่มเติม

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

ข้อจำกัดของชุดคำสั่ง

Tinyram ใช้รูปแบบข้อจำกัด R1CS สำหรับข้อจำกัดวงจร รูปแบบเฉพาะมีดังนี้:

ข้อจำกัด R1CS สามารถมีการแสดงชุดค่าผสมเชิงเส้นสามชุดของ a, b และ c การกำหนดตัวแปรทั้งหมดในระบบ R1CS สามารถแบ่งออกเป็นสองส่วน: อินพุตหลักและอินพุตเสริม หลักคือสิ่งที่เรามักเรียกว่า "คำสั่ง" ผู้ช่วยคือ "พยาน"

ระบบข้อจำกัด R1CS ประกอบด้วยข้อจำกัด R1CS หลายรายการ ความยาวเวกเตอร์ของแต่ละข้อจำกัดคงที่ (ขนาดอินพุตหลัก + ขนาดอินพุตเสริม + 1)

• andTinyram ใช้แกดเจ็ตที่กำหนดเองจำนวนมากในการติดตั้งโค้ดของ libsnark เพื่อแสดงข้อจำกัดของ vm และข้อจำกัดของการดำเนินการและหน่วยความจำ opcode รหัสเฉพาะอยู่ในโฟลเดอร์ gadgetslib1/gadgets/cpu_checkers/tinyram

ข้อ จำกัด การจัดการบิต

สูตรข้อจำกัด:

ข้อจำกัด R1CS ของและตรวจสอบพารามิเตอร์ 1 และพารามิเตอร์ 2 และผลการคำนวณทีละบิตสำหรับการคำนวณการคูณ ขั้นตอนข้อจำกัด มีดังนี้:

1. ข้อจำกัดของกระบวนการคำนวณ มีรหัสดังนี้

2. ข้อจำกัดในการเข้ารหัสผลลัพธ์

• or3. ผลการคำนวณไม่ใช่ข้อจำกัด 0 ทั้งหมด (ให้สอดคล้องกับคำจำกัดความของคำสั่ง กระบวนการนี้ส่วนใหญ่เป็นการเตรียมการสำหรับธงข้อจำกัด)

ข้อจำกัด 4.flag

สูตรข้อจำกัด:

ขั้นตอนข้อจำกัดเฉพาะมีดังนี้:

1. ข้อจำกัดของกระบวนการคำนวณ มีรหัสดังนี้

2. ข้อจำกัดในการเข้ารหัสผลลัพธ์ (เหมือนด้านบน)

• xor3. ผลการคำนวณไม่ใช่ข้อจำกัด 0 ทั้งหมด (ให้สอดคล้องกับคำจำกัดความของคำสั่ง กระบวนการนี้ส่วนใหญ่เป็นการเตรียมการสำหรับธงข้อจำกัด) (เหมือนกับข้างต้น)

ข้อจำกัด 4.flag (เช่นเดียวกับด้านบน)

สูตรข้อจำกัด:

ขั้นตอนข้อจำกัดเฉพาะมีดังนี้:

•not1. ข้อจำกัดของกระบวนการคำนวณ มีรหัสดังนี้

ขั้นตอนที่ 2, 3, 4 เช่นเดียวกับด้านบน

สูตรข้อจำกัด:

ขั้นตอนข้อจำกัดเฉพาะมีดังนี้:

•addขั้นตอนที่ 2, 3, 4 เช่นเดียวกับด้านบน

ข้อจำกัดการจัดการจำนวนเต็ม

: สูตรข้อจำกัด:

ขั้นตอนข้อจำกัดเฉพาะมีดังนี้:

1. ข้อจำกัดของกระบวนการคำนวณ มีรหัสดังนี้

•sub2. ถอดรหัสข้อจำกัดผลลัพธ์และข้อจำกัดบูลีน
3. ข้อ จำกัด ของผลลัพธ์การเข้ารหัส

: สูตรข้อจำกัด:

ข้อจำกัดย่อยซับซ้อนกว่า add เล็กน้อย ตัวแปรกลางใช้แทนผลลัพธ์ของ a - b ในขณะเดียวกัน 2^w ถูกเพิ่มในผลลัพธ์เพื่อให้แน่ใจว่าการคำนวณผลลัพธ์จะแสดงในรูปของ จำนวนเต็มบวกและสัญลักษณ์ ขั้นตอนข้อจำกัดเฉพาะมีดังนี้:

1. ข้อจำกัดของกระบวนการคำนวณ

•mull 、umulh、smulh2. ถอดรหัสข้อจำกัดผลลัพธ์และข้อจำกัดบูลีน

3. ลงนามข้อ จำกัด บิต

สูตรข้อจำกัด:

ข้อจำกัดที่เกี่ยวข้องกับ Mull เกี่ยวข้องกับขั้นตอนต่อไปนี้

1. คำนวณข้อจำกัดการคูณ

•udiv 、umod2. ข้อ จำกัด การเข้ารหัสผลการคำนวณ

สูตรข้อจำกัด:

B คือตัวหาร q คือผลหาร และ r คือเศษ ผลรวมที่เหลือต้องเป็นไปตามเงื่อนไขที่ไม่เกินตัวหาร รหัสข้อจำกัดเฉพาะมีดังนี้:

• shl、shrชื่อเรื่องรอง

ข้อจำกัดในการทำงานกะ

สูตรจำกัดcmpe、 cmpa 、cmpae、cmpg、cmpgeการดำเนินการเปรียบเทียบ

. คำแนะนำในการเปรียบเทียบสามารถแบ่งออกเป็น 2 ประเภท ได้แก่ การเปรียบเทียบหมายเลขที่ลงนามและการเปรียบเทียบหมายเลขที่ไม่ได้ลงนาม แกนของกระบวนการข้อจำกัดของทั้งสองใช้การเปรียบเทียบ_gadget ที่ใช้งานใน libsnark

ขั้นตอนที่เหลือจะเหมือนกับข้อจำกัดการเปรียบเทียบที่เซ็นชื่อ

• movชื่อเรื่องรอง

ย้ายข้อ จำกัด การดำเนินงาน

• cmovสูตรข้อจำกัด:

สูตรข้อจำกัด:

ข้อจำกัดของ cmov นั้นซับซ้อนกว่าของ mov ลักษณะการทำงานหลักของ mov นั้นเกี่ยวข้องกับการเปลี่ยนแปลงของค่าแฟล็ก ในขณะเดียวกัน cmov จะไม่แก้ไขแฟล็ก ดังนั้น ข้อจำกัดจำเป็นต้องตรวจสอบให้แน่ใจว่าค่าของแฟล็กไม่ ไม่เปลี่ยนแปลง รหัสของ cmov เป็นดังนี้:

ชื่อเรื่องรอง

• jmp

ข้อ จำกัด การดำเนินการกระโดด

• cjmp

คำแนะนำการกระโดดและการข้ามแบบมีเงื่อนไขเหล่านี้ไม่ได้แก้ไขการลงทะเบียนและแฟล็ก แต่แก้ไขพีซี

การดำเนินการ Jmp จำกัดค่า pc ให้สอดคล้องกับผลการดำเนินการคำสั่ง รหัส จำกัด เฉพาะมีดังนี้:

cjmp กระโดดตามเงื่อนไขแฟล็ก แฟล็ก = 1 เพื่อกระโดด มิฉะนั้น pc จะเพิ่มขึ้น 1

• cnjmp

สูตรข้อจำกัดมีดังนี้:

รหัสข้อจำกัดมีดังนี้:

cnjmp กระโดดตามเงื่อนไขการตั้งค่าสถานะ ตั้งค่าสถานะ = 0 เพื่อข้าม มิฉะนั้น pc จะเพิ่มขึ้น 1

สูตรข้อจำกัดมีดังนี้:

ข้อ จำกัด ในการทำงานของหน่วยความจำ

• store.b และ store.w

การดำเนินการเหล่านี้เป็นการโหลดและจัดเก็บหน่วยความจำอย่างง่าย โดยที่แอดเดรสของหน่วยความจำถูกกำหนดโดยค่าทันทีหรือเนื้อหาของรีจิสเตอร์ นี่เป็นโหมดการกำหนดแอดเดรสเพียงโหมดเดียวใน Tinyram (tinyram ไม่รองรับโหมดการกำหนดแอดเดรส "base+offset" ทั่วไป)

และ

สำหรับ store.w จะใช้ค่าของ arg1val ทั้งหมด และสำหรับ store.b นั้น opcode จะใช้เฉพาะส่วนที่จำเป็นของ arg1val เท่านั้น (เช่น ไบต์สุดท้าย) โค้ดข้อจำกัดมีดังนี้:

• load.b และ load.w

• read

เนื้อหาที่เราต้องการโหลดจากหน่วยความจำจะถูกจัดเก็บไว้ใน command_results รหัสข้อจำกัดมีดังนี้:

ป้อนข้อ จำกัด ในการดำเนินงาน

การดำเนินการอ่านเกี่ยวข้องกับเทป และกฎข้อจำกัดเฉพาะคือ:

1. เนื้อหาในเทปที่แล้วถูกอ่าน ไม่มีเนื้อหาให้อ่าน และเทปต่อไปจะไม่ถูกอ่าน

2. เนื้อหาในเทปที่แล้วถูกอ่าน ไม่มีเนื้อหาให้อ่าน และตั้งค่าสถานะเป็น 1

3. หากอ่านคำสั่งที่กำลังดำเนินการอยู่ เนื้อหาที่อ่านต่อการอ่านจะสอดคล้องกับเนื้อหาอินพุตของเทป

5. ผลลัพธ์ไม่ใช่ 0 ซึ่งหมายความว่าแฟล็กเป็น 0

รหัสข้อจำกัด:

ชื่อเรื่องรอง

• answer

ข้อ จำกัด การทำงานของเอาต์พุต

เมื่อค่าเอาต์พุตของโปรแกรมได้รับการยอมรับ has_accepted จะถูกตั้งค่าเป็น 1 และค่าที่ส่งคืนของโปรแกรมสามารถยอมรับได้ตามปกติ หมายความว่าคำสั่งปัจจุบันคือคำตอบและค่า arg2 คือ 0

อื่น

รหัสข้อจำกัดมีดังนี้:

อื่นแน่นอน นอกจากข้อจำกัดเกี่ยวกับคำสั่งบางอย่างที่กล่าวถึงข้างต้นแล้ว Tinyram ยังมีข้อจำกัดต่างๆ เช่น ความสอดคล้องของพีซี การเข้ารหัสและถอดรหัสพารามิเตอร์ และการตรวจสอบหน่วยความจำ ข้อจำกัดเหล่านี้รวมกันผ่านระบบ R1CS เพื่อสร้างระบบข้อจำกัดของ Tinyram ที่สมบูรณ์ นี่จึงเป็นสาเหตุหลักของข้อจำกัดจำนวนมากที่สร้างโดย Tinyram ในรูปแบบของ R1CSนี่คือคำพูด

จากตัวอย่างในรูปด้านบน สรุปได้ว่า เป็นไปไม่ได้ที่จะตรวจสอบการดำเนินการ EVM ทั้งหมดโดยใช้ vnTinyram + zk-SNARKs และเหมาะสำหรับการตรวจสอบความถูกต้องการคำนวณของคำสั่งจำนวนเล็กน้อยเท่านั้น คุณสามารถใช้ vnTinyram เพื่อ ตรวจสอบ opcode ของประเภทการคำนวณ EVM บางประเภท

เกี่ยวกับเรา

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

เกี่ยวกับเรา

GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon