فريق Plutus في Cardano ينجز نماذج الكلفة لوظائف Dijkstra الجديدة

أنهى فريق Plutus نماذج الكلفة لوظيفتي keepPolicies و dropPolicies وهما وظيفتان مدمجتان قيد التطوير لحقبة Dijkstra في Cardano. وفي تحديث بتاريخ 4 نوفمبر ذكر قائد هندسة البرمجيات Ziyang Liu أيضا اختبارات جديدة وتحديثات في المواصفات وإصلاحات في المترجم.

يشمل العمل كيفية تعامل العقود الذكية مع قيم الرموز وكيفية احتساب موارد التنفيذ. هذه تغييرات تطويرية لدعم التحضير لحقبة Dijkstra؛ ولا يعلن التقرير عن تفعيلها على Cardano mainnet.

وظائف جديدة لتصفية الرموز حسب السياسة

تنتمي الوظيفتان إلى CIP-0168 وهو مقترح يوسّع العمليات على BuiltinValue وهو نوع بيانات يُستخدم لتمثيل كميات الأصول داخل عقود Plutus الذكية. توفر الوظائف المدمجة عمليات تدعمها مباشرة منظومة التنفيذ.

تجمع Cardano الرموز الأصلية تحت معرّفات سياسات مرتبطة بقواعد إصدارها. تحتفظ keepPolicies بالأجزاء من قيمة المرتبطة بالمعرّفات المحددة، بينما تزيل dropPolicies تلك الأجزاء. يمكن لعقد يعالج عدة مجموعات من الرموز استخدام هذه الوظائف لعزل الأصول ذات الصلة بفحص معين.

تقيّد التغييرات المدمجة قائمة السياسات التي تقبلها كل من الوظيفتين إلى 256 معرفا. وتحدد نماذج الكلفة المنجزة كيفية احتساب التنفيذ بوحدات CPU والذاكرة، وهي جزء من ميزانية تنفيذ العقد الذكي.

اختبارات وإصلاحات في المترجم تعالج سلوك البرامج

أضاف الفريق 65 حالة مطابقة للوظائف المدمجة الجديدة في Value. تقارن هذه الاختبارات مخرجات التنفيذ بالنتيجة المتوقعة للمدخلات المحددة. كما جرى توثيق الوظائف الجديدة و multiIndexArray في مواصفة Plutus Core لتوفير مرجع وصفي لسلوكها.

يعالج تصحيح منفصل قضية constant folding وهو تحسين يحسب التعابير المناسبة أثناء الترجمة بدلا من تركها لوقت التنفيذ. كانت مراحل في المترجم المتأثرة تستطيع سابقا تبسيط بعض التعابير بطريقة تتجاهل على نحو غير صحيح الحسابات التي تفشل. يحافظ التصحيح على تلك الحسابات عندما لا تتوافر الشروط المطلوبة للتبسيط.

يصوّب التحديث أيضا ترجمة أنواع السياق في Plutus V4 التي تصف المعلومات المتاحة للبرامج عند التحقق من صحة المعاملات. إضافة إلى ذلك تم مواءمة نماذج الذاكرة لوظيفتي lookupCoin و valueContains مع معلمات نموذج الكلفة القائمة.

[NEWSBREAK]

تتسع الفحوص الشكلية مع استمرار التنفيذ

قدّم الفريق أداة تولد اختبارات التحقق من الأنواع في Agda انطلاقا من مجموعة المطابقة القائمة. تعد Agda لغة برمجة ومساعد إثبات يُستخدمان للتعبير عن النماذج الشكلية والتحقق من اتساقها. تتيح الأداة لحالات الاختبار المستخدمة بالفعل في التنفيذ أن تدعم الفحوص في ذلك الوسط الشكلي.

أضيفت الوظائف المدمجة الجديدة أيضا إلى الميتانظرية وهي الوصف الرياضي المستخدم للاستدلال حول برامج Plutus. وهي تظهر حاليا بوصفها مسلمات ما يعني أن النموذج يفترض سلوكها المحدد بينما يستمر العمل على التنفيذ. ويمدد تغيير مدمج آخر أداة تتحقق مما إذا كان تحسين في المترجم يحافظ على سلوك البرنامج.

يشمل العمل المتبقي تنفيذ المصفوفات وسلاسل البايت في النموذج الشكلي وتصحيح اعتماد تحسين منفصل في المترجم وتحسين آلة CEK التي تنفذ برامج Plutus Core. وتظل هذه البنود مدرجة كأعمال جارية في تقرير 4 نوفمبر.