การตรวจสอบอย่างเป็นทางการขั้นสูงของการพิสูจน์ความรู้เป็นศูนย์: วิธีพิสูจน์ความทรงจำที่ไม่มีความรู้

ในบล็อกชุดนี้เกี่ยวกับ การตรวจสอบอย่างเป็นทางการขั้นสูงของการพิสูจน์ความรู้เป็นศูนย์ เราได้พูดคุยถึง วิธีตรวจสอบคำสั่ง ZK และ ให้ข้อมูลเชิงลึกเกี่ยวกับช่องโหว่ ZK สองรายการ ด้วยการตรวจสอบคำสั่ง zkWasm ทุกคำสั่งอย่างเป็นทางการ เราพบและแก้ไขช่องโหว่ทั้งหมด ทำให้เราสามารถตรวจสอบความปลอดภัยทางเทคนิคและความถูกต้องของวงจร zkWasm ทั้งหมดได้อย่างเต็มที่ ดังที่แสดงใน รายงานสาธารณะ และ ฐานโค้ด

แม้ว่าเราได้สาธิตกระบวนการตรวจสอบคำสั่ง zkWasm และแนะนำแนวคิดเบื้องต้นของโปรเจ็กต์ที่เกี่ยวข้องแล้ว ผู้อ่านที่คุ้นเคยกับการตรวจสอบอย่างเป็นทางการอาจสนใจที่จะทำความเข้าใจการตรวจสอบยืนยัน zkVM ด้วยระบบ ZK ขนาดเล็กอื่นๆ หรือ VM ที่มีโค้ดไบต์ประเภทอื่นๆ ที่เป็นเอกลักษณ์ บน. ในบทความนี้ เราจะพูดคุยเชิงลึกถึงประเด็นทางเทคนิคบางประการที่พบในการตรวจสอบระบบย่อยหน่วยความจำ zkWasm หน่วยความจำเป็นส่วนที่มีเอกลักษณ์ที่สุดของ zkVM และการจัดการสิ่งนี้มีความสำคัญต่อการตรวจสอบความถูกต้องของ zkVM อื่นๆ ทั้งหมด

การตรวจสอบอย่างเป็นทางการ: เครื่องเสมือน (VM) กับเครื่องเสมือน ZK (zkVM)

เป้าหมายสูงสุดของเราคือการตรวจสอบความถูกต้องของ zkWasm ซึ่งคล้ายกับทฤษฎีบทความถูกต้องของตัวแปล bytecode ทั่วไป (VM เช่น ตัวแปล EVM ที่ใช้โดยโหนด Ethereum) นั่นคือแต่ละขั้นตอนการดำเนินการของล่ามจะสอดคล้องกับขั้นตอนทางกฎหมายตามความหมายในการดำเนินงานของภาษา ดังแสดงในรูปด้านล่าง หากสถานะปัจจุบันของโครงสร้างข้อมูลของล่าม bytecode คือ SL และสถานะนี้ถูกทำเครื่องหมายเป็นสถานะ SH ในข้อกำหนดระดับสูงของเครื่อง Wasm จากนั้นเมื่อล่ามก้าวเข้าสู่สถานะ SL จะมี จะต้องเป็นสถานะระดับสูงทางกฎหมายที่สอดคล้องกัน SH และข้อกำหนด Wasm กำหนดว่า SH ต้องก้าวไปสู่ SH

ในทำนองเดียวกัน zkVM มีทฤษฎีบทความถูกต้องที่คล้ายกัน: แต่ละแถวใหม่ในตารางการดำเนินการ zkWasm จะสอดคล้องกับขั้นตอนทางกฎหมายตามความหมายในการดำเนินงานของภาษา ดังแสดงในรูปด้านล่าง หากสถานะปัจจุบันของแถวของโครงสร้างข้อมูลในตารางดำเนินการคือ SR และสถานะนี้แสดงเป็นสถานะ SH ในข้อกำหนดระดับสูงของเครื่อง Wasm ดังนั้นสถานะ SR ของ แถวถัดไปในตารางดำเนินการจะต้องสอดคล้องกับสถานะระดับสูง SH และข้อกำหนด Wasm กำหนดว่า SH ต้องก้าวไปที่ SH

เป็นไปตามข้อกำหนดของสถานะระดับสูงและขั้นตอน Wasm นั้นสอดคล้องกันไม่ว่าจะใน VM หรือ zkVM และดังนั้นจึงสามารถใช้ประสบการณ์การตรวจสอบก่อนหน้านี้ด้วยล่ามภาษาการเขียนโปรแกรมหรือคอมไพเลอร์ สิ่งที่ทำให้การตรวจสอบ zkVM พิเศษคือประเภทของโครงสร้างข้อมูลที่ประกอบขึ้นเป็นสถานะระดับต่ำของระบบ

อันดับแรก ดังที่เราระบุไว้ใน โพสต์บล็อกที่แล้ว ตัวพิสูจน์ zk โดยพื้นฐานแล้วคือการดำเนินการจำนวนเต็มแบบโมดูโลจำนวนเฉพาะขนาดใหญ่ ในขณะที่ข้อกำหนด Wasm และล่ามปกติจะจัดการกับจำนวนเต็ม 32 บิตหรือ 64 บิต การใช้งาน zkVM ส่วนใหญ่เกี่ยวข้องกับสิ่งนี้ ดังนั้นการประมวลผลที่เกี่ยวข้องจึงต้องดำเนินการในระหว่างการตรวจสอบด้วย อย่างไรก็ตาม นี่เป็นปัญหา ท้องถิ่น: โค้ดแต่ละบรรทัดมีความซับซ้อนมากขึ้นเนื่องจากการดำเนินการทางคณิตศาสตร์ที่ต้องจัดการ แต่โครงสร้างโดยรวมของโค้ดและการพิสูจน์ไม่เปลี่ยนแปลง

ข้อแตกต่างที่สำคัญอีกประการหนึ่งคือวิธีจัดการโครงสร้างข้อมูลที่มีขนาดไดนามิก ในล่ามโค้ดไบต์ปกติ หน่วยความจำ สแต็กข้อมูล และสแต็กการเรียกทั้งหมดถูกนำมาใช้เป็นโครงสร้างข้อมูลที่ไม่แน่นอน ในทำนองเดียวกัน ข้อกำหนด Wasm แสดงถึงหน่วยความจำเป็นประเภทข้อมูลด้วยวิธีรับ/ตั้งค่า ตัวอย่างเช่น ล่าม EVM ของ Geth มีประเภทข้อมูล หน่วยความจำ ซึ่งใช้เป็นอาร์เรย์ไบต์ที่แสดงถึงหน่วยความจำกายภาพ และเขียนและอ่านผ่านเมธอด Set 32 และ GetPtr เพื่อที่จะใช้ คำสั่งการจัดเก็บหน่วยความจำ Geth เรียก `Set 32` เพื่อแก้ไขหน่วยความจำกายภาพ

func opMstore (pc *uint 64, ล่าม *EVMInterpreter, ขอบเขต *ScopeContext) ([] ไบต์, ข้อผิดพลาด) {

// ค่าป๊อปของสแต็ก

mStart, val := ขอบเขต.Stack.pop(), ขอบเขต.Stack.pop()

ขอบเขต Memory.Set 32 (mStart.Uint 64 (), val)

กลับไม่มีเลย

-

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

อย่างไรก็ตาม ด้วย zkVM สิ่งต่างๆ จะซับซ้อนมากขึ้น

ตารางหน่วยความจำของ zkWasm และเลเยอร์นามธรรมของหน่วยความจำ

ใน zkVM มีคอลัมน์บนตารางการดำเนินการสำหรับข้อมูลขนาดคงที่ (คล้ายกับการลงทะเบียนใน CPU) แต่ไม่สามารถใช้เพื่อจัดการโครงสร้างข้อมูลที่มีขนาดไดนามิกได้ ซึ่งจะดำเนินการโดยการค้นหาตารางเสริม ตารางการดำเนินการของ zkWasm มีคอลัมน์ EID ซึ่งมีค่าเป็น 1, 2, 3... และมีตารางเสริม 2 ตาราง ตารางหน่วยความจำ และตารางข้าม ซึ่งใช้เพื่อแสดงข้อมูลหน่วยความจำและ call stack ตามลำดับ

ต่อไปนี้เป็นตัวอย่างของการใช้โปรแกรมถอนเงิน:

ยอดเงินคงเหลือ;

เป็นโมฆะหลัก () {

ยอดคงเหลือ = 100;

จำนวน = 10;

ยอดคงเหลือ -= จำนวน; // ถอนออก

-

เนื้อหาและโครงสร้างของตารางดำเนินการค่อนข้างเรียบง่าย มีขั้นตอนการดำเนินการ 6 ขั้นตอน (EID 1 ถึง 6) แต่ละขั้นตอนจะมีบรรทัดที่แสดง opcode และหากคำสั่งเป็นหน่วยความจำที่อ่านหรือเขียน ที่อยู่และข้อมูล:

แต่ละแถวในตารางหน่วยความจำประกอบด้วยที่อยู่ ข้อมูล EID เริ่มต้น และ EID สิ้นสุด EID เริ่มต้นคือ EID ของขั้นตอนการดำเนินการที่เขียนข้อมูลนี้ไปยังที่อยู่นี้ และ EID ที่สิ้นสุดคือ EID ของขั้นตอนการดำเนินการถัดไปที่จะเขียนที่อยู่นี้ (และมีการนับด้วย ซึ่งจะกล่าวถึงรายละเอียดในภายหลัง) สำหรับวงจรคำสั่งการอ่านหน่วยความจำ Wasm นั้น จะใช้ข้อจำกัดการค้นหาเพื่อให้แน่ใจว่ามีรายการที่เหมาะสมในตาราง โดยที่ EID ของคำสั่งการอ่านอยู่ใน มีตั้งแต่ต้นจนจบภายใน (ในทำนองเดียวกัน แต่ละแถวของตารางการข้ามจะสอดคล้องกับเฟรมของ call stack และแต่ละแถวจะมีป้ายกำกับด้วย EID ของขั้นตอนคำสั่งการโทรที่สร้างขึ้น)

ระบบหน่วยความจำนี้แตกต่างอย่างมากจากตัวแปล VM ปกติ: แทนที่จะเป็นหน่วยความจำที่ไม่แน่นอนซึ่งได้รับการอัพเดตแบบเพิ่มหน่วย ตารางหน่วยความจำประกอบด้วยประวัติของการเข้าถึงหน่วยความจำทั้งหมดตลอดการติดตามการดำเนินการ เพื่อให้การทำงานของโปรแกรมเมอร์ง่ายขึ้น zkWasm ได้จัดเตรียมเลเยอร์นามธรรมที่นำมาใช้ผ่านฟังก์ชันการป้อนข้อมูลที่สะดวกสบายสองฟังก์ชัน พวกเขาคือ:

alloc_memory_table_lookup_write_cell

และ

Alloc_memory_table_lookup_read_cell

พารามิเตอร์มีดังนี้:

ตัวอย่างเช่น โค้ดที่ใช้คำสั่งการจัดเก็บหน่วยความจำใน zkWasm มีการเรียกไปยังฟังก์ชัน write alloc:

ให้ memory_table_lookup_heap_write1 = ตัวจัดสรร

.alloc_memory_table_lookup_write_cell_with_value(

ร้านค้าเขียน res 1,

ข้อ จำกัด_builder,

วันอีด,

ย้าย |____|. Constant_from! (LocationType::Heap เป็น 64)

ย้าย |meta|.load_block_index.expr(meta), // ที่อยู่

ย้าย |____|. คงที่_จาก! (0) // เป็น 32 บิต

ย้าย |____|. เปิดใช้งานคงที่_จาก! (1), // (เสมอ)

-

ให้ store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;

ฟังก์ชัน `alloc` มีหน้าที่รับผิดชอบในการจัดการข้อจำกัดการค้นหาระหว่างตารางและข้อจำกัดทางคณิตศาสตร์ที่เกี่ยวข้องกับรายการตาราง `eid` ปัจจุบันในตารางหน่วยความจำ จากนี้ โปรแกรมเมอร์สามารถถือว่าตารางเหล่านี้เป็นหน่วยความจำธรรมดา และค่าของ `store_value_in_heap1` ถูกกำหนดให้กับที่อยู่ `load_block_index` หลังจากที่โค้ดถูกดำเนินการ

ในทำนองเดียวกัน คำแนะนำในการอ่านหน่วยความจำจะถูกนำไปใช้โดยใช้ฟังก์ชัน `read_alloc` ในลำดับการดำเนินการตัวอย่างข้างต้น มีข้อจำกัดในการอ่านสำหรับแต่ละคำสั่งในการโหลด และข้อจำกัดในการเขียนสำหรับคำสั่งร้านค้าแต่ละคำสั่ง และข้อจำกัดแต่ละรายการจะเป็นไปตามรายการในตารางหน่วยความจำ

mtable_lookup_write (แถว 1.eid, แถว 1.store_addr, แถว 1.store_value)

⇐ (แถว 1.eid= 1 ∧ แถว 1.store_addr=balance ∧ แถว 1.store_value= 100 ∧ ...)

mtable_lookup_write (แถว 2.eid, แถว 2.store_addr, แถว 2.store_value)

⇐ (แถว 2.eid= 2 ∧ แถว 2.store_addr=amount ∧ แถว 2.store_value= 10 ∧ ...)

mtable_lookup_read (แถว 3.eid, แถว 3.load_addr, แถว 3.load_value)

⇐ ( 2<แถว 3.eid≤ 6 ∧ แถว 3.load_addr=amount ∧ แถว 3.load_value= 100 ∧ ...)

mtable_lookup_read(แถว 4.eid, แถว 4.load_addr, แถว 4.load_value)

⇐ ( 1<แถว 4.eid≤ 6 ∧ แถว 4.load_addr=balance ∧ แถว 4.load_value= 10 ∧ ...)

mtable_lookup_write (แถว 6.eid, แถว 6.store_addr, แถว 6.store_value)

⇐ (แถว 6.eid= 6 ∧ แถว 6.store_addr=balance ∧ แถว 6.store_value= 90 ∧ ...)

โครงสร้างของการตรวจสอบอย่างเป็นทางการควรสอดคล้องกับนามธรรมที่ใช้ในซอฟต์แวร์ที่กำลังตรวจสอบ เพื่อให้การพิสูจน์เป็นไปตามตรรกะเดียวกันกับโค้ด สำหรับ zkWasm หมายความว่าเราจำเป็นต้องตรวจสอบวงจรตารางหน่วยความจำและฟังก์ชัน จัดสรรเซลล์อ่าน/เขียน เป็นโมดูลซึ่งมีอินเทอร์เฟซเหมือนกับหน่วยความจำตัวแปร ด้วยอินเทอร์เฟซดังกล่าว การตรวจสอบวงจรคำสั่งแต่ละวงจรสามารถทำได้ในลักษณะที่คล้ายคลึงกับล่ามทั่วไป ในขณะที่ความซับซ้อนของ ZK เพิ่มเติมถูกห่อหุ้มไว้ในโมดูลระบบย่อยหน่วยความจำ

ในการตรวจสอบ เราได้นำแนวคิดที่ว่า ตารางหน่วยความจำสามารถถือได้ว่าเป็นโครงสร้างข้อมูลที่ไม่แน่นอน กล่าวคือ เขียนฟังก์ชัน `memory_at type` ซึ่งจะสแกนตารางหน่วยความจำทั้งหมดและสร้างการแมปข้อมูลที่อยู่ที่เกี่ยวข้อง (ช่วงค่าของตัวแปร `ประเภท` ในที่นี้คือข้อมูลหน่วยความจำ Wasm สามประเภทที่แตกต่างกัน ได้แก่ ฮีป สแต็กข้อมูล และตัวแปรโกลบอล) จากนั้น เราจะพิสูจน์ว่าข้อจำกัดของหน่วยความจำที่สร้างโดยฟังก์ชันจัดสรรนั้นเทียบเท่ากับการใช้ชุดและรับ ฟังก์ชั่น การเปลี่ยนแปลงข้อมูลที่ทำโดยการแมปข้อมูลที่อยู่ที่เกี่ยวข้อง เราสามารถพิสูจน์ได้:

• สำหรับแต่ละอีด หากมีข้อจำกัดดังต่อไปนี้

memory_table_lookup_read_cell ประเภทค่าออฟเซ็ต eid

แต่

รับ (ประเภท memory_at eid) offset = ค่าบางค่า

• และหากมีข้อจำกัดดังต่อไปนี้

memory_table_lookup_write_cell ประเภทค่าออฟเซ็ต eid

แต่

memory_at (eid+ 1) type = set (memory_at eid type) ค่าออฟเซ็ต

หลังจากนี้ การตรวจสอบแต่ละคำสั่งจะขึ้นอยู่กับการดำเนินการรับและตั้งค่าบนแผนที่ข้อมูลที่อยู่ ซึ่งคล้ายกับล่ามโค้ดไบต์ที่ไม่ใช่ ZK

กลไกการนับการเขียนหน่วยความจำของ zkWasm

อย่างไรก็ตาม คำอธิบายแบบง่ายข้างต้นไม่ได้เปิดเผยเนื้อหาทั้งหมดของตารางหน่วยความจำและตารางข้าม ภายใต้กรอบของ zkVM ตารางเหล่านี้อาจถูกจัดการโดยผู้โจมตีซึ่งสามารถจัดการคำสั่งโหลดหน่วยความจำได้อย่างง่ายดายเพื่อส่งคืนค่าที่กำหนดเองโดยการแทรกแถวข้อมูล

ตามตัวอย่างโปรแกรมถอนเงิน ผู้โจมตีมีโอกาสที่จะแทรกข้อมูลเท็จลงในยอดคงเหลือของบัญชีโดยปลอมการดำเนินการเขียนหน่วยความจำที่ 110 ดอลลาร์ก่อนดำเนินการถอน กระบวนการนี้สามารถทำได้โดยการเพิ่มแถวข้อมูลลงในตารางหน่วยความจำและแก้ไขค่าของเซลล์ที่มีอยู่ในตารางหน่วยความจำและตารางดำเนินการ ซึ่งจะส่งผลให้มีการถอนเงิน ฟรี เนื่องจากยอดเงินในบัญชีจะยังคงอยู่ที่ $100 หลังจากการดำเนินการ

เพื่อให้แน่ใจว่าตารางหน่วยความจำ (และตารางข้าม) มีเฉพาะรายการที่ถูกต้องซึ่งสร้างโดยคำสั่งการเขียนหน่วยความจำ (และการโทรและส่งคืน) ที่ถูกดำเนินการจริง zkWasm ใช้กลไกการนับพิเศษเพื่อตรวจสอบจำนวนรายการ โดยเฉพาะตารางหน่วยความจำมีคอลัมน์เฉพาะที่คอยติดตามจำนวนรายการทั้งหมดที่เขียนลงในหน่วยความจำ ในเวลาเดียวกัน ตารางดำเนินการยังมีตัวนับเพื่อนับจำนวนการดำเนินการเขียนหน่วยความจำที่คาดหวังสำหรับแต่ละคำสั่ง ตรวจสอบให้แน่ใจว่าจำนวนทั้งสองนั้นสอดคล้องกันโดยการตั้งค่าข้อจำกัดด้านความเท่าเทียมกัน ตรรกะของวิธีนี้ใช้งานง่ายมาก ทุกครั้งที่ดำเนินการเขียนในหน่วยความจำ จะถูกนับหนึ่งครั้ง และควรมีบันทึกที่สอดคล้องกันในตารางหน่วยความจำ ดังนั้นผู้โจมตีจึงไม่สามารถแทรกรายการเพิ่มเติมใด ๆ ในตารางหน่วยความจำได้

ข้อความเชิงตรรกะข้างต้นค่อนข้างคลุมเครือ และในกระบวนการพิสูจน์ด้วยเครื่องจักร จะต้องมีการทำให้แม่นยำยิ่งขึ้น ขั้นแรก เราต้องแก้ไขคำสั่งของการเขียนบทแทรกหน่วยความจำที่กล่าวถึงข้างต้น เรากำหนดฟังก์ชัน `mops_at eid type` เพื่อนับรายการในตารางหน่วยความจำด้วย `eid` และ `type` ที่กำหนด (คำสั่งส่วนใหญ่จะสร้าง 0 หรือ 1 รายการใน eid) ข้อความที่สมบูรณ์ของทฤษฎีบทมีข้อกำหนดเบื้องต้นเพิ่มเติมที่ระบุว่าไม่มีรายการตารางหน่วยความจำปลอม:

หากมีข้อจำกัดดังต่อไปนี้

(ค่าออฟเซ็ตประเภท memory_table_lookup_write_cell eid)

และมีการกำหนดข้อจำกัดใหม่ดังต่อไปนี้

(ประเภท mops_at eid) = 1

แต่

(memory_at(eid+ 1) type) = set (memory_at eid type) ค่าออฟเซ็ต

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

เพื่อพิสูจน์สิ่งนี้ เราใช้วิธีการจากบนลงล่างเพื่อจำกัดจำนวนรายการตารางหน่วยความจำที่สอดคล้องกับคำสั่งที่กำหนด ซึ่งรวมถึงสามขั้นตอน ขั้นแรก เราประเมินจำนวนรายการที่ควรสร้างสำหรับคำแนะนำในลำดับการดำเนินการตามประเภทคำสั่ง เราเรียกจำนวนการเขียนที่คาดหวังตั้งแต่ขั้นตอนที่ i จนถึงจุดสิ้นสุดของการดำเนินการว่า `instructions_mops i` และจำนวนรายการที่สอดคล้องกันในตารางหน่วยความจำตั้งแต่คำสั่ง ith จนถึงจุดสิ้นสุดของการดำเนินการ `cum_mops (eid i)` ด้วยการวิเคราะห์ข้อจำกัดการค้นหาของแต่ละคำสั่ง เราสามารถพิสูจน์ได้ว่าคำสั่งดังกล่าวสร้างรายการได้ไม่น้อยไปกว่าที่คาดไว้ และด้วยเหตุนี้เราจึงสามารถสรุปได้ว่าแต่ละส่วน [i... numRows] ที่ติดตามจะสร้างรายการไม่น้อยไปกว่าที่คาดไว้:

Lemma cum_mops_bound: สำหรับทั้งหมดพรรณี

0 ≤ ฉัน ->

i + Z.of_nat n = etable_numRow ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ Instructions_mops ใน n

ประการที่สอง หากคุณสามารถแสดงว่าตารางไม่มีรายการมากกว่าที่คาดไว้ ตารางก็จะมีจำนวนรายการที่ถูกต้องซึ่งชัดเจน

เล็มมา cum_mops_equal : forall ni,

0 ≤ ฉัน ->

i + Z.of_nat n = etable_numRow ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ Instructions_mops ใน ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = Instructions_mops i n.

ตอนนี้ดำเนินการขั้นตอนที่สาม ทฤษฎีบทความถูกต้องของเราระบุว่าสำหรับ n ใดๆ cum_mops และ Instruction_mops จะสอดคล้องกันเสมอตั้งแต่แถว n จนถึงจุดสิ้นสุดของตาราง:

เล็มมา cum_mops_equal : forall n,

0 <= Z.of_nat n < etable_numRow ->

MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) = Instructions_mops (Z.of_nat n)

การยืนยันทำได้โดยการสรุป n แถวแรกในตารางคือข้อจำกัดความเท่าเทียมกันของ zkWasm ซึ่งบ่งชี้ว่าจำนวนรายการทั้งหมดในตารางหน่วยความจำถูกต้อง เช่น cum_mops 0 = Instructions_mops 0 สำหรับบรรทัดต่อไปนี้ สมมติฐานอุปนัยบอกเรา:

cum_mops n = Instructions_mops n

และเราหวังว่าจะพิสูจน์ได้

cum_mops (n+ 1) = Instructions_mops (n+ 1)

ให้ความสนใจที่นี่

cum_mops n = mop_at n + cum_mops (n+ 1)

และ

Instruction_mops n = Instruction_mops n + Instructions_mops (n+ 1)

ดังนั้นเราจึงได้

mops_at n + cum_mops (n+ 1) = Instruction_mops n + Instruction_mops (n+ 1)

ก่อนหน้านี้ เราได้แสดงให้เห็นแล้วว่าแต่ละคำสั่งจะสร้างรายการไม่ต่ำกว่าจำนวนที่คาดไว้ เช่น

mops_at n ≥ Instruction_mops n

จึงสามารถสรุปได้

cum_mops (n+ 1) ≤ Instructions_mops (n+ 1)

ที่นี่เราจำเป็นต้องใช้บทแทรกที่สองด้านบน

(การใช้บทแทรกที่คล้ายกันในการตรวจสอบตารางการข้าม สามารถพิสูจน์ได้ว่าคำสั่งการโทรแต่ละรายการสามารถสร้างรายการตารางการข้ามได้อย่างแม่นยำ ดังนั้นเทคนิคการพิสูจน์นี้จึงสามารถใช้ได้โดยทั่วไป อย่างไรก็ตาม เรายังต้องมีการตรวจสอบเพิ่มเติมเพื่อพิสูจน์ว่าการส่งคืนความถูกต้องของ คำสั่ง eid ที่ส่งคืนนั้นแตกต่างจาก eid ของคำสั่งการโทรที่สร้าง call frame ดังนั้นเราจึงต้องมี คุณสมบัติไม่เปลี่ยนแปลงเพิ่มเติม เพื่อประกาศว่าค่า eid จะเพิ่มขึ้นในทิศทางเดียวระหว่างลำดับการดำเนินการ)

การอธิบายกระบวนการพิสูจน์อย่างละเอียดนั้นเป็นเรื่องปกติของการตรวจสอบอย่างเป็นทางการ และเป็นสาเหตุที่การตรวจสอบโค้ดเฉพาะเจาะจงมักใช้เวลานานกว่าการเขียน แต่มันคุ้มไหม? ในกรณีนี้ถือว่าคุ้มค่าเพราะเราพบข้อผิดพลาดร้ายแรงในกลไกการนับตารางกระโดดระหว่างการพิสูจน์ จุดบกพร่องนี้ได้รับการอธิบายโดยละเอียดใน บทความที่แล้ว โดยสรุปแล้ว โค้ดเวอร์ชันเก่าถือเป็นทั้งคำสั่งการโทรและการส่งคืน และผู้โจมตีสามารถสร้างการกระโดดปลอมโดยการเพิ่มคำสั่งส่งคืนเพิ่มเติมให้กับลำดับการดำเนินการของรายการตาราง . แม้ว่ากลไกการนับที่ไม่ถูกต้องอาจตอบสนองสัญชาตญาณว่าทุกคำสั่งที่เรียกและส่งคืนนั้นนับ แต่ปัญหาก็เกิดขึ้นเมื่อเราพยายามปรับแต่งสัญชาตญาณนี้ให้กลายเป็นประโยคทฤษฎีบทที่แม่นยำยิ่งขึ้น

ทำให้กระบวนการพิสูจน์เป็นแบบโมดูลาร์

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

นอกจากนี้ ยังมีปัจจัยอีกประการหนึ่งที่ต้องพิจารณา โปรเจ็กต์ zkWasm มีขนาดค่อนข้างใหญ่ ดังนั้นงานการตรวจสอบจึงต้องแยกส่วนเพื่อให้วิศวกรตรวจสอบหลายคนสามารถแบ่งงานได้ ดังนั้นจึงจำเป็นต้องให้ความสนใจเป็นพิเศษกับความซับซ้อนเมื่อทำการแยกโครงสร้างการพิสูจน์กลไกการนับ ตัวอย่างเช่น สำหรับคำสั่ง LocalGet มีสองทฤษฎีบทดังต่อไปนี้:

ทฤษฎีบท opcode_mops_correct_local_get : สำหรับทั้งหมด i,

0 <= ฉัน ->

etable_values eid_cell i > 0 ->

opcode_mops_correct LocalGet i.

ทฤษฎีบท LocalGetOp_correct : forall i st y xs,

0 <= ผม ->

etable_values enabled_cell i = 1 ->

mops_at_correct ฉัน ->

etable_values (ops_cell LocalGet) i = 1 ->

state_rel ฉัน st ->

wasm_stack st = xs ->

(etable_values offset_cell i) > 1 ->

nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = y บางตัว ->

state_rel (i+ 1) (update_stack (incr_iid st) (y::xs))

คำสั่งทฤษฎีบทแรก

opcode_mops_correct LocalGet i

เมื่อขยาย หมายความว่าคำสั่งจะสร้างรายการตารางหน่วยความจำอย่างน้อยหนึ่งรายการที่บรรทัด i (หมายเลข 1 ระบุไว้ในข้อกำหนดเฉพาะ LocalGet opcode ของ zkWasm)

ทฤษฎีบทที่สองคือทฤษฎีบทความถูกต้องสมบูรณ์สำหรับการสอนซึ่งอ้างอิงถึง

mops_at_correct ฉัน

ตามสมมติฐาน หมายความว่าคำสั่งสร้างรายการตารางหน่วยความจำเพียงรายการเดียว

วิศวกรตรวจสอบสามารถพิสูจน์ทฤษฎีบททั้งสองนี้ได้อย่างอิสระ จากนั้นจึงรวมทฤษฎีเหล่านี้เข้ากับข้อพิสูจน์เกี่ยวกับตารางดำเนินการเพื่อพิสูจน์ความถูกต้องของทั้งระบบ เป็นที่น่าสังเกตว่าการพิสูจน์แต่ละคำสั่งสามารถดำเนินการได้ที่ระดับข้อจำกัดในการอ่าน/เขียน โดยไม่ต้องทราบถึงการใช้งานเฉพาะของตารางหน่วยความจำ ดังนั้นโครงการจึงแบ่งออกเป็น 3 ส่วนที่สามารถจัดการได้อย่างอิสระ

สรุป

การตรวจสอบวงจรสำหรับ zkVM ทีละบรรทัดไม่มีความแตกต่างโดยพื้นฐานจากการตรวจสอบแอปพลิเคชัน ZK ในโดเมนอื่นๆ เนื่องจากทั้งสองต้องการเหตุผลที่คล้ายกันเกี่ยวกับข้อจำกัดทางคณิตศาสตร์ ในระดับสูง การตรวจสอบ zkVM ต้องใช้วิธีการตรวจสอบอย่างเป็นทางการหลายวิธีเดียวกันกับที่ใช้สำหรับล่ามภาษาโปรแกรมและคอมไพเลอร์ ข้อแตกต่างหลักที่นี่คือสถานะของเครื่องเสมือนที่มีขนาดไดนามิก อย่างไรก็ตาม สามารถลดผลกระทบของความแตกต่างเหล่านี้ให้เหลือน้อยที่สุดได้ด้วยการจัดโครงสร้างโครงสร้างการตรวจสอบอย่างระมัดระวังเพื่อให้ตรงกับเลเยอร์นามธรรมที่ใช้ในการนำไปใช้งาน ช่วยให้แต่ละคำสั่งเป็นโมดูลอิสระตามอินเทอร์เฟซการรับการตั้งค่า เช่นเดียวกับการตรวจสอบทางเคมีของล่ามทั่วไป