The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL
تقدم هذه الورقة نظرية Isabelle/HOL ميكانيكية تُعرف دالة حفظ حالة عابرة للمجالات تضمن السلامة، والحيويّة، والتقارب، والاتساق الهرمي للإجراءات التنظيمية على الأصول المرمزة عبر مجالات موزعة، تم التحقق من صحتها من خلال ثمانية عشر تفسيراً ونموذج شجرة معاملات عودي.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
في العالم المالي الحديث، غالبًا ما توجد القيمة ليس في شكل نقد مادي أو ذهب، بل كرموز رقمية مسجلة على شبكة من أجهزة الكمبيوتر تُعرف باسم "البلوكشين". يمكن لهذه الشبكات أن تعمل بشكل مستقل، مثل جزر منفصلة، ومع ذلك فهي غالبًا ما تحتاج إلى مشاركة المعلومات حول نفس الأصل. تخيل بنكًا في بلد ما يقوم بتجميد أصل رقمي بناءً على أمر قانوني. إذا كان هذا الأصل موجودًا أيضًا في شبكة مختلفة في بلد آخر، فيجب أن يتم التجميد هناك أيضًا، بشكل فوري وكامل. إذا لم يسري الإجراء على "الجزيرة" الأخرى، فستُفتح ثغرة؛ حيث يمكن لفاعل سيئ أن ينقل الأصل إلى الجزيرة التي لا يزال فيها حرًا، مما يؤدي فعليًا إلى التهرب من القانون. يُعرف هذا باسم "المراجحة التنظيمية"، وهو ما يقوض النظام بأكمله للتمويل الرقمي. ولكي تكون هذه الأنظمة جديرة بالثقة، يجب أن تنتشر عملية واحدة للتجميد أو المصادرة عبر كل الشبكات المتصلة في وقت واحد، بحيث لا تترك مجالًا للتنفيذ الجزئي أو الهروب.
لقد تصدى باحث في مختبرات "أوراكلايزر" (Oraclizer Labs) لهذه المشكلة من خلال بناء نموذج رياضي صارم يثبت إمكانية عمل مثل هذا النظام. هو لم يكتفِ بكتابة برنامج كمبيوتر، بل صاغ نظرية رسمية باستخدام أداة متخصصة تُسمى "Isabelle/HOL"، والتي تعمل بمثابة آلة حاسبة فائقة الدقة للمنطق. كان هدفه هو التحقق من أنه إذا اتُّخذ إجراء تنظيمي على شبكة واحدة، فمن المضمون أن ينعكس على جميع الشبكات الأخرى، وأن هذه العملية ستكتمل دائمًا دون أن تتعثر، حتى لو كانت بعض أجهزة الكمبيوتر في الشبكة تتصرف بشكل خبيث. عامل الباحث الشبكات المختلفة كدومينات (نطاقات) متميزة، واعتبر قواعد نقل الأصول بينها كخريطة مهيكلة. وقد أثبت أن هذه الخريطة تتبع قوانين منطقية صارمة، مما يضمن أن حالة الأصل -سواء كانت نشطة أو مجمدة أو مصادرة- تظل متسقة في كل مكان.
جوهر اكتشافه هو مفهوم يسميه "الفانكتور" (Functor)، وهو وسيلة لوصف كيفية تحول نظام ما إلى نظام آخر مع الحفاظ على هيكله الأساسي سليمًا. في هذه الحالة، أظهر الباحث أن عملية مزامنة الحالات التنظيمية عبر سلاسل الكتل المختلفة تسلك سلوك آلة مثالية. فإذا بدأت بإجراء صحيح، مثل تجميد أصل، وطبقته عبر الشبكة، فإن النتيجة مضمونة بأن تكون إجراءً صحيحًا في كل مكان. لقد أثبت أن هذا النظام يحافظ على "الحالات النهائية"، مما يعني أنه بمجرد مصادرة أصل بشكل دائم، لا يمكن عكس هذه الحالة أو محوها بواسطة عملية المزامنة. إنه طريق ذو اتجاه واحد للنهائية: فالمصادرة المسجلة على سلسلة واحدة تصبح حقيقة دائمة على جميع السلاسل، ولا توجد طريقة رياضية تجعل النظام يعكسها بالخطأ أو يخلق مصادرة وهمية من العدم.
ومع ذلك، فإن إثبات أن النظام يعمل بشكل صحيح هو نصف المعركة فقط. فقد تعين على الباحث أيضًا إثبات أن النظام يعمل بالفعل في الوقت المناسب، حتى عندما تسوء الأمور. في الشبكة اللامركزية، قد يتم التحكم في بعض أجهزة الكمبيوتر من قبل مهاجمين يحاولون تعطيل العملية. قام الباحث بنمذجة سيناريو يمكن فيه لثلث أجهزة الكمبيوتر أن تكون غير صادقة. وقد أثبت أنه طالما أن أجهزة الكمبيوتر الصادقة تفوق غير الصادقة بهامش محدد، فإن النظام سيصل دائمًا إلى قرار. وأثبت أن النظام لن يظل عالقًا في انتظار إشارة لا تأتي أبدًا، وأن الأوامر المتضاربة -مثل محاولة سلطتين مختلفتين تجميد نفس الأصل في وقت واحد- سيتم حلها بترتيب حتمي ومتوقع بناءً على الأولوية. وهذا يضمن عدم تجاهل أي طلب إلى أجل غير مسمى، وهي خاصية تُعرف باسم "حرية الجوع" (Starvation Freedom).
ولجعل هذه الضمانات قوية، بنى الباحث بنية تحتية متعددة الطبقات. بدأ بنموذج أساسي لكيفية تغير حالة أصل واحد، ثم توسع ليشمل التعامل مع أصول متعددة وشبكات متعددة. كما أدخل نظام "الدرجات"، الذي يسمح للأصول المختلفة بمتطلبات مزامنة متفاوتة. فبعض الأصول قد تحتاج فقط إلى مراقبتها على الشبكات الأخرى، بينما تتطلب أصول أخرى رابطًا ذريًا وثيقًا حيث تتغير الحالة بشكل فوري ومتطابق في كل مكان. وقد أثبت أن هذا التسلسل الهرمي آمن: فإذا تم إعداد نظام للتعامل مع درجة عالية من المزامنة، فسيقوم تلقائيًا باستيفاء متطلبات الدرجات الأدنى أيضًا. تتيح هذه المرونة تكييف النظام مع الاحتياجات التنظيمية المختلفة دون كسر ضمانات السلامة الأساسية.
كما ربط الباحث نموذجه الجديد بطريقة معروفة وموجودة لتأمين هياكل البيانات، تُعرف باسم "ميركل فانكتور" (Merkle Functor). تضمن هذه الطريقة الموجودة عدم التلاعب بالبيانات، لكنها كانت محدودة سابقًا بشبكة واحدة. نجح الباحث في رفع طبقة الأمان هذه لتعمل عبر شبكات متعددة، مما خلق جسرًا بين قواعد المزامنة الجديدة والإثباتات التشفيرية الراسخة. وهذا يعني أن النظام لا يحافظ فقط على اتساق القواعد، بل يوفر أيضًا ضمانًا رياضيًا بأن البيانات التي تتم مزامنتها أصلية ولم يتم التلاعب بها من قبل مهاجم. وقد اختبر نظريته مقابل نموذج محدد لشجرة معاملات مستخدمة في بروتوكول حقيقي يُسمى "كانتون" (Canton)، موضحًا أن قواعده المجردة يمكن تطبيقها على هيكل ملموس ومعقد.
والأهم من ذلك، أن الباحث كان حريصًا على تحديد ما لا يفعله نموذجه. فهو لم يدّعِ حل كل مشكلة في تكنولوجيا البلوكشين. يفترض نموذجه أن عملية المزامنة تحدث بشكل فوري وذري، مما يعني أنها تكتمل بالكامل أو لا تكتمل على الإطلاق، دون أن تتعثر في المنتصف. كما أقر بأن الشبكات في العالم الحقيقي تعاني من تأخيرات، وأن أجهزة الكمبيوتر يمكن أن تفشل بطرق لا تحاكيها نماذجه. وأشار أيضًا إلى أنه لم يثبت أن نموذجه الرياضي يطابق تمامًا كود الكمبيوتر الذي سيعمل على خادم حقيقي؛ فهذه الخطوة تظل تحديًا مستقبليًا. ومع ذلك، وضمن الحدود التي وضعها، يوفر عمله أساسًا كاملًا وموثقًا. لقد أظهر أنه يمكن تصميم نظام تكون فيه الإجراءات التنظيمية ذرية عبر نطاقات مختلفة، حيث تضمن الرياضيات الاتساق، ويظل النظام حيًا ومستجيبًا حتى في مواجهة الجهات الفاعلة الخبيثة.
تكمي أهمية هذا العمل في قدرته على تحويل مشكلة معقدة وعالية المخاطر إلى مجموعة من الحقائق القابلة للإثبات. قبل هذا البحث، كان ضمان تطبيق التجميد التنظيمي في كل مكان يعتمد إلى حد كبير على الثقة وأفضل الممارسات الهندسية. أما الآن، فهناك إثبات رسمي بأن مثل هذا النظام ممكن، وأنه سيتصرف تمامًا كما هو مخطط له تحت ظروف محددة ومعرفة جيدًا. لقد قدم الباحث مخططًا لبناء أنظمة مالية رقمية يمكن فيها إنفاذ القانون بنفس الدقة واليقين اللذين تقوم عليهما الرياضيات. ومن خلال فصل سلامة القواعد عن سرعة الشبكة، أنشأ إطارًا يمكن إعادة استخدامه لأنواع أخرى من المزامنة عبر النطاقات، مما قد يمتد إلى ما وراء التمويل ليشمل أي مجال يتطلب اتساق الحالة عبر أنظمة متعددة. والنتيجة هي طمأنينة هادئة ولكنها قوية: في عالم الجزر الرقمية، من الممكن بناء جسر لا ينكسر، ولا يكذب، ولا يترك بابًا مفتوحًا ليتسلل منه القانون.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.