البادئة المشتركة تقوم رسميًا بالتحقق من بروتوكول الإقراض #XRP لإثباته رياضيًا بأنه لا يمكن استنزافه أو أن يصبح معسرًا أو أن يخرق قواعده.
يركّز العمل على بروتوكول الإقراض الذي تم تقديمه عبر XLS-66. شرحت البادئة المشتركة نهجها في سلسلة من ستة أجزاء، بما في ذلك سبب اختيارها Lean 4 لعملية التحقق.
قالت البادئة المشتركة إن التحقق الصوري يتجاوز الاختبار البرمجي العادي، إذ يستخدم الرياضيات لإثبات أن النظام يعمل بشكل صحيح في جميع الحالات الممكنة.
وقال مُدقِّق «سِجِل XRP»، المعروف أيضًا باسم حسين زنغانا، إن التحقق الصوري يُستخدم بالفعل في الأنظمة عالية الخطورة مثل تقنيات الدفاع العسكرية، وبرمجيات مراقبة حركة الطيران، وأنظمة التحكم في الطيران، ومحطات الطاقة النووية.
وأوضح أن هذا النهج يستخدم الرياضيات لإظهار أن النظام يظل صالحًا عبر جميع المدخلات الممكنة، وليس فقط الحالات التي اختبرها المطورون.
استعرضت البادئة المشتركة عدة أدوات، منها Dafny وLean 4 وTLA+ وP. وقررت المجموعة أن TLA+ وP لم يكونا مناسبين جيدًا للأسئلة المحددة التي احتاجت إلى الإجابة عنها بشأن بروتوكول الإقراض.
ومن أحد الأسباب التي جعلتها تختار Lean 4 أنه لا يعتمد على مُحلِّل SMT. وقد وجدت البادئة المشتركة أن مُحلِّل Dafny قد تنتهي مهلة عمله أحيانًا عند التعامل مع الحسابات الرياضية المعقدة المطلوبة للتحقق. يتطلب Lean عملاً أكبر يدويًا، لكن هذا أيضًا يجعل الأخطاء أسهل لاكتشافها وتصحيحها من قِبل المطورين.
#CryptoNewsCommunity
يركّز العمل على بروتوكول الإقراض الذي تم تقديمه عبر XLS-66. شرحت البادئة المشتركة نهجها في سلسلة من ستة أجزاء، بما في ذلك سبب اختيارها Lean 4 لعملية التحقق.
قالت البادئة المشتركة إن التحقق الصوري يتجاوز الاختبار البرمجي العادي، إذ يستخدم الرياضيات لإثبات أن النظام يعمل بشكل صحيح في جميع الحالات الممكنة.
وقال مُدقِّق «سِجِل XRP»، المعروف أيضًا باسم حسين زنغانا، إن التحقق الصوري يُستخدم بالفعل في الأنظمة عالية الخطورة مثل تقنيات الدفاع العسكرية، وبرمجيات مراقبة حركة الطيران، وأنظمة التحكم في الطيران، ومحطات الطاقة النووية.
وأوضح أن هذا النهج يستخدم الرياضيات لإظهار أن النظام يظل صالحًا عبر جميع المدخلات الممكنة، وليس فقط الحالات التي اختبرها المطورون.
استعرضت البادئة المشتركة عدة أدوات، منها Dafny وLean 4 وTLA+ وP. وقررت المجموعة أن TLA+ وP لم يكونا مناسبين جيدًا للأسئلة المحددة التي احتاجت إلى الإجابة عنها بشأن بروتوكول الإقراض.
ومن أحد الأسباب التي جعلتها تختار Lean 4 أنه لا يعتمد على مُحلِّل SMT. وقد وجدت البادئة المشتركة أن مُحلِّل Dafny قد تنتهي مهلة عمله أحيانًا عند التعامل مع الحسابات الرياضية المعقدة المطلوبة للتحقق. يتطلب Lean عملاً أكبر يدويًا، لكن هذا أيضًا يجعل الأخطاء أسهل لاكتشافها وتصحيحها من قِبل المطورين.
#CryptoNewsCommunity