ข่าว 
ข้อมูลเหรียญ 
แนะนำสื่อ 
ทีมวิจัยอีเธอเรียม(ETH)กำลังพัฒนาโครงการเพื่อใช้งาน Lean 4 ในการนำข้อกำหนดฉันทามติของการอัปเกรด Fulu, Gloas และ Heze มาใช้งาน พร้อมตรวจสอบความถูกต้องทางคณิตศาสตร์ เพื่อลดความเสี่ยงที่เชนจะแยกออกจากกันเนื่องจากไคลเอนต์หลายตัวตีความข้อกำหนดเดียวกันต่างกัน
Ethereum Protocol Fellowship(EPF) และทีมวิจัย Invisible Garden เปิดเผยความคืบหน้าของโครงการ ‘Etheorem’ ผ่านโพสต์บน Ethereum Research Forum เมื่อวันที่ 21 โครงการนี้มีเป้าหมายใช้งานข้อกำหนดฉันทามติของอีเธอเรียมในรูปแบบที่สามารถประมวลผลได้ด้วย Lean 4 ซึ่งเป็นภาษาสำหรับพิสูจน์ทฤษฎีบท พร้อมตรวจสอบตรรกะสำคัญทางคณิตศาสตร์ นอกเหนือจากการทดสอบโค้ด
อีเธอเรียมใช้โครงสร้างที่ให้ไคลเอนต์ฉันทามติจากทีมพัฒนาหลายทีมทำงานร่วมกัน แม้ไคลเอนต์แต่ละตัวจะนำข้อกำหนดเดียวกันไปใช้งาน แต่หากตีความตรรกะในรายละเอียดต่างกัน ผลการตัดสินความถูกต้องของบล็อกหรือการเลือกเชนอาจไม่เหมือนกัน Etheorem ตรวจสอบความแตกต่างในการตีความเหล่านี้ด้วยการตรวจสอบรูปแบบอย่างเป็นทางการ
โครงการได้นำข้อกำหนดฉันทามติที่เกี่ยวข้องกับการอัปเกรด Fulu, Gloas และ Heze มาใช้งานแล้ว โดยสามารถประมวลผลการเปลี่ยนสถานะและตรรกะการเลือกฟอร์กได้ พร้อมตรวจสอบผลลัพธ์ของการนำไปใช้โดยเปรียบเทียบกับชุดทดสอบฉันทามติอย่างเป็นทางการของอีเธอเรียม Fulu มีข้อกำหนดเกี่ยวกับการสุ่มตัวอย่างความพร้อมใช้งานของข้อมูล ส่วน Gloas มีองค์ประกอบที่เกี่ยวข้องกับ ePBS ซึ่งเป็นโครงสร้างการประมูลเพย์โหลดการประมวลผล ขณะที่ Heze สะท้อนโครงสร้างรายการรวมธุรกรรมเพื่อเสริมความต้านทานต่อการเซ็นเซอร์
พื้นฐานของ Etheorem คือไลบรารี SSZ(Simple Serialize) ชื่อ SizzLean ไลบรารีนี้ตรวจสอบคุณสมบัติบางส่วนที่จำเป็นต่อการทำซีเรียลไลซ์และดีซีเรียลไลซ์ข้อมูลฉันทามติ รวมถึงการคำนวณต้นไม้เมิร์เคิลภายใน Lean kernel ขอบเขตการตรวจสอบรวมถึงการยืนยันว่าข้อมูลที่ผ่านการซีเรียลไลซ์สามารถย้อนกลับเป็นค่าเดิมได้ ค่าที่แตกต่างกันไม่สามารถมีการเข้ารหัสเดียวกัน และขนาดการเข้ารหัสไม่เกินขีดจำกัดที่คำนวณไว้ล่วงหน้า
โครงการยังมุ่งลดความแตกต่างระหว่างโค้ดที่ผ่านการตรวจสอบกับโค้ดที่ใช้งานจริง โดยมีแนวคิดใช้คำจำกัดความของข้อกำหนดเดียวกันทั้งในสภาพแวดล้อมการพิสูจน์และสภาพแวดล้อมการประมวลผล เพื่อลดปัญหาที่ตรรกะซึ่งใช้ในการพิสูจน์แตกต่างจากตรรกะของไคลเอนต์จริง อย่างไรก็ตาม การตรวจสอบรูปแบบเป็นการตรวจสอบตรรกะภายในขอบเขตที่กำหนด จึงยังไม่ใช่ขั้นตอนทดแทนไคลเอนต์อีเธอเรียมทั้งหมด ก่อนหน้านี้ TokenPost เคยรายงานกรณีการตรวจสอบรูปแบบด้วย Lean 4 ในโปรโตคอลบล็อกเชน ซึ่งใช้การจำลองตรรกะสำคัญเป็นโมเดลเพื่อกำหนดขอบเขตการตรวจสอบ
การผ่านชุดทดสอบไม่ได้หมายความถึงเสถียรภาพในสภาพแวดล้อมการใช้งานจริงหรือการเปิดตัวอย่างเป็นทางการ โครงการระบุแผนขยายขอบเขตการพิสูจน์ในระยะต่อไป
ความคิดเห็น 0