عن المشروع

SafeMesh هي مكتبة مفتوحة المصدر مصممة للمزامنة الخفيفة القابلة للتضمين للحالة باستخدام أنواع البيانات المكررة الخالية من التضارب (CRDTs). يتميز تميزها الأساسي باستخدام التحقق الرسمي: خصائص التقارب الأساسية لخمسة أنواع من CRDTs (G-Set، G-Counter، PN-Counter، OR-Set، وRGA/Text) مدعومة ببراهين تم التحقق منها بواسطة الآلة في Lean 4. يضمن ذلك ضمانات رياضية لتماسك البيانات عبر النسخ الموزعة. تم تنفيذ المكتبة في Rust بدون std، مما يجعلها مناسبة للبيئات ذات الموارد المحدودة وأنظمة التضمين. يوفر SafeMesh واجهة برمجة تطبيقات Rust الأساسية إلى جانب ارتباطات لـ C (عبر FFI)، وWASM/TypeScript، وPython. تسمح هذه الارتباطات للمطورين بدمج منطق CRDT الذي تم التحقق منه في تطبيقات الويب، والبرامج الأصلية، وبيئات البرمجة النصية دون إعادة تنفيذ منطق الدمج. تشمل الميزات الأساسية: - **التحقق الرسمي**: تم إثبات مجموعة delta-CRDT في Lean 4، مع عدم وجود أي مسلمات “sorry”، مما يضمن موثوقية عالية لتقارب الحالة. - **دعم متعدد اللغات**: يعرض نفس الأساس في Rust من خلال ABI لـ C، وWASM، وواجهات Python، مع ترميز بايت قياسي للنقل عبر السلك. - **أعمى للنقل**: يتعامل SafeMesh مع حالة CRDT وسجل الأحداث (الإضافة/الدمج/منذ)، لكن المستخدمين يجب أن يوفروا آلية النقل الخاصة بهم للتواصل عبر الشبكة. - **بنية الاختبار**: تتضمن اختبارات تفاضلية مقابل مجموعات بيانات Oracle التي تم إنشاؤها بواسطة Lean، ومضامين قوانين للأنواع المخصصة، وبوابات CI للحفاظ على سلامة البرهان. يحدد المشروع بوضوح نطاق ضماناته، ويميز بين CRDTs التي تم إثباتها وأنواع أخرى تم اختبارها لكنها لم تُثبت، مثل LWW Register وLWW Map. وهو مرخص بموجب Apache-2.0.