โปรโตคอลกู้ยืม XRPL เริ่มตรวจสอบความถูกต้องด้วย Lean 4

โปรโตคอลกู้ยืมใหม่บน XRP Ledger(XRPL) เริ่มเข้าสู่กระบวนการตรวจสอบทางคณิตศาสตร์ว่าเส้นทางเงินและกฎทางบัญชีทำงานตามที่กำหนดหรือไม่ แต่การตรวจสอบนี้ไม่ได้หมายความว่าความเสี่ยงจากการผิดนัดชำระหนี้หรือความน่าเชื่อถือของผู้กู้จะหมดไป

คอมมอน พรีฟิกซ์(Common Prefix) บริษัทวิจัยโปรโตคอล ระบุเมื่อวันที่ 17 กันยายนว่า กำลังตรวจสอบโปรโตคอลกู้ยืม XRPL อย่างเป็นทางการด้วยภาษา Lean 4 ซึ่งเป็นภาษาสำหรับการพิสูจน์ทฤษฎี เป้าหมายคือการตรวจสอบว่ากระบวนการฝากเงิน กู้ยืม ชำระคืน และไถ่ถอน ไม่ละเมิดกฎทางบัญชีและความปลอดภัยที่กำหนดไว้

การตรวจสอบอย่างเป็นทางการแตกต่างจากการทดสอบทั่วไปที่จำลองเพียงบางสถานการณ์ นักวิจัยไม่ได้พิสูจน์โค้ด C++ ของ xrpld ทั้งหมดโดยตรง แต่จำลองตรรกะหลักเป็นโมเดลใน Lean 4 และกำหนดคุณสมบัติที่โมเดลต้องปฏิบัติตาม

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

การดำเนินการครั้งนี้ไม่ได้หมายความว่าฟังก์ชันกู้ยืมของ XRPL เปิดใช้งานอย่างสมบูรณ์บนเมนเน็ตแล้ว เอกสารโอเพนซอร์สของ Ripple อธิบาย LendingProtocolV1_1 ว่าเป็น amendment ที่นำห้องนิรภัยแบบปิดและบัญชีแบบเกณฑ์เงินสดมาใช้ ขณะที่การนำไปใช้งานจริงยังต้องผ่านการลงคะแนนบนเมนเน็ตและกระบวนการฉันทามติ

บันทึกการเปิดตัว xrpld เวอร์ชัน 3.4.0 ที่เผยแพร่โดย XRPLF ระบุว่ามีฟังก์ชันที่เกี่ยวข้องกับ LendingProtocolV1_1 อยู่แล้ว อย่างไรก็ตาม การมีฟังก์ชันในโค้ดกับการเปิดใช้งาน amendment บนบัญชีแยกประเภทเป็นคนละขั้นตอน

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

เอกสารอย่างเป็นทางการของ XRPL เกี่ยวกับห้องนิรภัยสินทรัพย์เดี่ยวระบุเงื่อนไขการทำธุรกรรมในแต่ละระยะ โครงสร้างนี้ทำให้สถานะบนบัญชีแยกประเภทสะท้อนว่าเงินฝากถูกนำไปใช้ปล่อยกู้เมื่อใด และสามารถไถ่ถอนได้เมื่อใด

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

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

การตรวจสอบก่อนหน้านี้พบการละเมิดเงื่อนไขคงที่ของห้องนิรภัย ข้อผิดพลาดในการตรวจสอบการชำระคืนเงินกู้ ปัญหาการปัดเศษทางคณิตศาสตร์ และความแตกต่างระหว่างข้อกำหนด XLS กับการใช้งานจริง โดย RippleX ระบุในโพสต์สำหรับนักพัฒนาว่า การแก้ไขที่เกี่ยวข้องถูกรวมไว้ใน xrpld เวอร์ชัน 3.1.3 และ 3.2.0 แล้ว

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

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

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

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

จนกว่าจะยืนยันการเปิดใช้งานบนเมนเน็ตและขอบเขตการตรวจสอบขั้นสุดท้าย ยังไม่อาจสรุปได้ว่าความปลอดภัยของตลาดกู้ยืม XRPL ได้รับการพิสูจน์แล้ว ต่อไปต้องติดตามการอนุมัติ amendment LendingProtocolV1_1 และโครงสร้างการพิจารณาสินเชื่อนอกเชน