💻 computer science

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

تقدم هذه الورقة إجراء قرار جديداً وسليماً لنظرية SMT للمصفوفات الامتدادية مع المصفوفات الثابتة التي تدعم نطاقات فهرسة تعسفية، متجاوزةً بذلك القيود السابقة المتمثلة في الحالات المحدودة أو اللانهائية، وتبرهن على فعاليتها من خلال التنفيذ في برنامج الحل Bitwuzla.

المؤلفون الأصليون: Mathias Preiner, Aina Niemetz, Clark Barrett

نُشر 2026-05-20

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Mathias Preiner, Aina Niemetz, Clark Barrett

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك محقق تحاول حل لغز يتعلق بمكتبة ضخمة ولانهائية من الكتب (مصفوفة - array). كل كتاب له رقم خانة محدد (فهرس - index) ويحتوي على قصة (عنصر - element).

في عالم التحقق الحاسوبي، نحتاج غالبًا لطرح أسئلة مثل: "إذا غيرت القصة في الخانة 5، هل ستتغير القصة في الخانة 10؟" أو "هل هاتان المكتبتان متطابقتان تمامًا؟"

لفترة طويلة، كانت الأدوات المستخدمة للإجابة على هذه الأسئلة (تسمى SMT solvers) تعاني من نقطة ضعف كبرى؛ فقد كانت بارعة في التعامل مع المكتبات التي يمكنك تغيير كتب فردية فيها، لكنها كانت تواجه صعوبة عندما تبدأ المكتبة بـ "قصة افتراضية" مكتوبة على كل صفحة قبل أن تبدأ حتى.

المشكلة: معضلة "الصفحة البيضاء"

تخيل أن لديك مكتبة حيث يبدأ كل كتاب فيها بنفس القصة الافتراضية: "النهاية".

الطريقة القديمة: إذا أردت أن تخبر الحاسوب: "حسنًا، اجعل 'النهاية' موجودة في كل مكان، ولكن غير الخانة 5 لتصبح 'الفصل الأول'"، كان على الحاسوب أن يكتب قائمة ضخمة ومتداخلة: "غير الخانة 5، ثم غير الخانة 6، ثم غير الخانة 7..." وصولاً إلى اللانهاية.
النتيجة: جعل هذا الأمر الحاسوب بطيئًا، مرتبكًا، وعرضة للأخطاء. كان الأمر يشبه محاولة وصف جدار أبيض عبر سرد كل بكسل أبيض فيه بشكل فردي.

علاوة على ذلك، لم تكن الأدوات السابقة قادرة على التعامل مع مفهوم "القصة الافتراضية" هذه إلا إذا كانت المكتبة لانهائية. أما إذا كانت المكتبة محدودة (مثل رف صغير يحتوي على 4 خانات فقط)، فإن الأدوات القديمة كانت غالبًا ما تعطي إجابة خاطئة. لم تكن تستطيع استيعاب أنه إذا قمت باستبدال كل خانة في رف صغير، فإن "القصة الافتراضية" لم تعد ذات أهمية.

الحل: "الختم السحري"

قام مؤلفو هذه الورقة البحثية، ماتياس برينر، وآينا نيميتز، وكلارك باريت، ببناء إجراء قرار جديد (مجموعة جديدة من القواعد للمحقق) يسمى CAEXT.

فكر في حلهم كأنه ختم سحري.
بدلاً من سرد كل كتاب، يمكنك الآن القول: "هذا الرف بأكمله مختوم بقصة 'النهاية'".

الابتكار: يمكن لنظامهم الجديد التعامل مع هذا "الختم السحري" سواء كان الرف لانهائيًا أو مجرد رف محدود وصغير.
الحيلة: أدركوا أنه بالنسبة لرف محدود، تحتاج فقط للتحقق مما إذا كنت قد ختمت فوق كل خانة. إذا فعلت ذلك، فإن الرف أصبح الآن بالقصة الجديدة. أما إذا لم تفعل، فإن "القصة الافتراضية" لا تزال سارية على الأماكن الفارغة.

كيف يعمل الأمر (لعبة "الانتشار")

تصف الورقة طريقتهم بأنها لعبة تمرير العصا.

الإعداد: لديك رف عليه "ختم سحري" (مصفوفة ثابتة) وبعض التغييرات المحددة (تحديثات).
المطاردة: يحاول النظام تتبع مسار المعلومات. إذا غيرت الخانة 1، هل يؤثر ذلك على الخانة 2؟
التعارض: أحيانًا، يجد النظام تناقضًا. على سبيل المثال، قد يرى أن "الخانة 1 هي 'النهاية'" ولكنها أيضًا "الخانة 1 هي 'الفصل الأول'".
الحل: تسمح القواعد الجديدة للنظام بالقول: "انتظر، إذا كان الرف يحتوي على 4 خانات فقط، وقد غيرت 4 خانات مختلفة، فإن 'الختم السحري' قد اختفى تمامًا. الرف الآن هو مجرد القصص الجديدة".

تثبت الورقة رياضيًا أن مجموعة القواعد الجديدة هذه صحيحة (sound). وهذا يعني:

الصحة من حيث التفنيد (Refutational Soundness): إذا قال النظام "هذا مستحيل"، فهو صحيح بنسبة 100%. إنه لا يكذب أبدًا بشأن وجود تناقض.
الصحة من حيث القابلية للإشباع (Satisfiability Soundness): إذا قال النظام "هذا ممكن"، فهو صحيح بنسبة 100%. إنه لا يكذب أبدًا بشأن وجود حل.

الاختبار الواقعي

لم يكتفِ المؤلفون بكتابة النظرية فحسب؛ بل بنوا أداة تسمى Bitwuzla واختبروها مقابل أدوات كشف رائدة أخرى (مثل Z3 و cvc5 و MathSAT5).

النتائج: حلت أداتهم الجديدة عددًا أكبر بكثير من الألغاز مقارنة بالأدوات الأخرى.
"الخدعة": وجدوا أن الأدوات الأخرى، عند مواجهتها لألغاز "الرف المحدود" هذه، غالبًا ما تعطي إجابات خاطئة. فقد تقول إن لغزًا ما قابل للحل بينما هو ليس كذلك، أو العكس. أما Bitwuzla، باستخدام منطق "الختم السحري" الجديد، فقد أصابت في كل مرة.
أين استُخدمت: اختبروا ذلك في مشكلات واقعية مثل فحص تصميمات الأجهزة (hardware) والتحقق من العقود الذكية (الاتفاقيات الرقمية) على بلوكشين إيثيريوم (Ethereum).

الملخص

ببسا#ط، تقدم هذه الورقة طريقة أذكى للحواسيب للتفكير في هياكل البيانات التي تبدأ بقيمة افتراضية.

قبل: كانت الحواسيب بطيئة ومرتبكة عند التعامل مع "القيم الافتراضية" في مجموعات بيانات محدودة وصغيرة.
الآن: يعامل هذا الأسلوب الجديد هذه القيم الافتراضية كأنها "ختم سحري" يمكن تتبعه واستبداله بسهل، مما يعمل بشكل مثالي لكل من السيناريوهات اللانهائية والمحدودة.
الأثر: هذا يجعل الأدوات الحاسوبية المستخدمة للتحقق من البرمجيات الحساسة للسلامة (مثل السيارات ذاتية القيادة أو عقود البلوكشين) أسرع، وأكثر دقة، وقادرة على حل المشكلات التي كانت مستحيلة سابقًا.

ملخص تقني: إرضاء المصفوفات الثابتة الامتدادية لنموذج الإرضاء (Satisfiability Modulo Extensional Constant Arrays)

بيان المشكلة

تعد عملية الاستدلال على هياكل بيانات المصفوفات، لا سيما بالاقتران مع الأعداد الصحيحة الآلية (machine integers)، متطلباً أساسياً للتحقق من الأجهزة والبرمجيات. توفر نظرية المصفوفات الامتدادية القياسية في "إرضاء النموذج" (SMT)، كما هي معرفة في SMT-LIB ومؤطرة بواسطة مكارثي (McCarthy)، عوامل تشغيل select (القراءة) وstore (الكتابة) جنباً إلى جنب مع بديهية الامتدادية. ورغم كفاية هذه النظرية للعديد من مهام التحقق، إلا أنها تفتقر إلى الإيجاز عند نمذجة المصفوفات التي يتم تهيئتها بقيمة افتراضية (مثل الذاكرة المهيأة بالأصفار).

في النظرية القياسية، يجب التعبير عن هذه التهيئة عبر تعبيرات store متداخلة بعمق لكتابة القيمة الافتراضية في كل فهرس ذي صلة. يؤدي هذا إلى عدم دقة في النمذجة (حيث لا يمكن سوى استبدال الفهارس المحددة صراحةً) ويسبب عدم كفاءة شديدة في إجراءات الحل بسبب عمق سلاسل عمليات store.

إن توسيع النظرية لتشمل المصفوفات الثابتة (constant arrays)—وهي مصفوفات تخزن عنصراً واحداً في كل فهرس—يوفر حلاً موجزاً. ومع ذلك، فإن إجراءات القرار الحالية للمصفوفات الثابتة الامتدادية تقتقتصر على نطاقات الفهرسة اللانهائية. أما بالنسبة لـ نطاقات الفهرسة المحدودة، فإن أدوات حل SMT الحالية تدعم فقط الأجزاء غير الامتدادية، أو في حالة بعض الأدوات، تعطي إجابات غير صحيحة عند الاستدلال على الامتدادية فوق المصفوفات الثابتة ذات الفهارس المحدودة. يكمكم التحدي الجوهري في تحديد ما إذا كان يمكن جعل تسلسلين من عمليات store فوق مصفوفات ثابتة مختلفة ذات نطاقات محدودة متساويين عبر تحديث الفهارس بشكل كافٍ، وهي مشكلة لا تظهر في الحالة اللانهائية.

المنهجية

يقدم المؤلفون إجراء قرار جديد لنظرية المصفوفات الثابتة الامتدادية ( $T_{\langle A \rangle}$ ) يدعم نطاقات الفهرسة التعسفية، بما في ذلك النطاقات المحدودة. يتم صياغة الإجراء كحساب مجرد، CAEXT، والذي يعمم ويمدد إجراء "الاستدلال عند الطلب" (Lemmas on Demand - LOD) للمصفوفات الامتدادية (DPA) المقدم في أعمال سابقة.

حساب CAEXT

يعمل الحساب على التكوينات $\langle A, I, \pi \rangle$ ، حيث $A$ هي مجموعة من الليتيرالات المسطحة، و $I$ هو تفسير في النظرية الفارغة ( $T_E$ )، و $\pi$ هو خريطة لخطوات الانتشار. يتجنب الإجراء تقديم قراءات افتراضية لجميع الفهارس (وهو أمر غير ممكن للنطاقات اللنهائية ومكلف حاسوبياً للنطاقات المحدودة الكبيرة) عن طريق نشر القيم الافتراضية وتتبع الفهارس المحدثة.

تشمل المكونات الرئيسية للحساب:

الحساب الأساسي (AEXT): يعمم إجراء LOD للمصفوفات ذات الفهارس والعناصر ذات الأنواع المختلفة، مما يفصلها عن تركيبات النظرية المحددة. يقوم بنشر معلومات القراءة بناءً على بديهيات مكارثي للقراءة فوق الكتابة (row-eq, row-ne) وبديهية الامتدادية (ext).
توسعة المصفوفة الثابتة:
- نشر القيم الافتراضية: بدلاً من توليد قراءات لكل فهرس، يقوم الحساب بنشر القيمة الافتراضية $v$ للمصفوفة الثابتة $\langle v \rangle$ إلى المصفوفات الأخرى. كما يحافظ على مجموعة من الفهارس المحدثة $I(a, \langle v \rangle)$ ، والتي تمثل الفهارس التي تختلف فيها المصفوفة $a$ عن القيمة الافتراضية $\langle v \rangle$ على طول مسار الانتشار.
- كشف التعارض (CongC): عندما يتم نشر قيمتين افتراضيتين مختلفتين $v$ و $w$ إلى نفس المصفوفة $a$ ، يتحقق الحساب مما إذا كانت مجموعة الفهارس المحدثة $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ تغطي كامل نطاق الفهرس. إذا كان النطاق محدوداً ولم تغطِ الفهارس المحدثة جميع الفهارस الممكنة، ينشأ تعارض ما لم يكن $v \approx w$ .
- ترميز DistinctN: للتعامل بكفاءة مع الصيغة المكممة $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (للتحقق مما إذا كان هناك فهرس غير محدث)، تقوم عملية التنفيذ بترميز هذا كقيد distinctN متخصص. يتحقق هذا القيد مما إذا كانت مجموعة الفهارس المحدثة تحتوي على $n$ من القيم المتمايزة على الأقل، حيث $n$ هو حجم نطاق الفهرس.

التنفيذ

تم تنفيذ إجراء القرار في أداة حل SMT المتطورة Bitwuzla. يتكامل الإجراء بسلاسة مع بنية LOD الموجودة في Bitwuzla، حيث يوفر محلل المتجهات الثنائية (bit-vector solver) التفسير $I$ . يتضمن التنفيذ تحسينات مثل التوسع الكسول (lazy expansion) لقيود distinctN والبحث بالعرض (breadth-first search) لمسارات الانتشار لتقليل عبء الذاكرة.

المساهمات الرئيسية

تعميم LOD: يعمم المؤلفون إجراء LOD للمصفوفات الامتدادية ذات المتجهات الثنائية ثابتة الحجم إلى أنواع الفهارس والعناصر التعسفية.
حساب AEXT المجرد: يقدمون AEXT كحساب مجرد ومنفصل لنظرية المصفوفات الامتدادية، مستقل عن نموذج حل LOD.
توسعة المصفوفات الثابتة (CAEXT): يمددون AEXT للتعامل مع المصفوفات الثابتة الامتديدية، مع إثبات الصحة الاستدلالية (إذا تم الإبلاغ عن عدم الإرضاء Unsat، فإن المدخلات غير قابلة للإرضاء) وصحة الإرضاء (إذا تم الوصول إلى تكوين مشبع دون Unsat، فإن المدخلات قابلة للإرضاء).
التنفيذ والتقييم: تم تنفيذ الإجراء في Bitwuzla وتقييمه على مجموعات متنوعة من الاختبارات المرجعية، مما أظهر تحسينات كبيرة في الأداء مقارنة بـ Bitwazla الأساسي والأدوات الرائدة الأخرى (Z3, cvc5, MathSAT5).

النتائج

أُجري التقييم على خمس مجموعات من الاختبارات المرجعية: smtlib (المنطق المكمم)، mbqi (الاستعلامات الفرعية من التكميم القائم على النموذج)، k-ind (التحقق من النماذج العتادية التزايدي)، hevm (آلة إيثيريوم الافتراضية)، وcrafted (اختبارات اصطناعية مصممة خصيصاً لاختبار امتدادية المصفوفات الثابتة ذات الفهارس المحدودة).

الأداء: تفوق Bitwuzla باستخدام الإجراء الجديد (Bitwuzla⟨A⟩) بشكل كبير على جميع الأدوات الأخرى. في مجموعة smtlib، زاد عدد الاختبارات المرجعية التي تم حلها بمعامل قدره 5 أضعاف مقارنة بـ Bitwazla الأساسي (3,545 مقابل 717). وفي مجموعة mbqi، حل Bitwuzla⟨A⟩ جميع الاستعلامات البالغ عددها 4,147، بينما حل النسخة الأساسية 4 استعلامات فقط.
الصحة: في مجموعة crafted⟨A⟩ التي تشفر المساوات فوق المصفوفات الثابتة ذات الفهارس المحددة بقيم افتراضية مختلفة، كان Bitwuzla⟨A⟩ الأداة الوحيدة التي قدمت إجابات صحيحة لجميع الحالات. أما Z3 وMathSAT5 فقد قبلا المدخلات لكنهما قدما إجابات خاطئة لعدد كبير من الاختبارات. أما cvc5 وBitwazla الأساسي فقد رفضا المدخلات تماماً بسبب عدم دعمها.
التحقق من الصحة: تحقق المؤلفون من النماذج التي أنتجتها أدوات الحل على مجموعة crafted⟨A⟩. فقط Bitwuzla⟨A⟩ أنتج نماذج متسقة مع ادعاءات الإرضاء الخاصة به. أما Z3 وMathSAT5 فقد أنتجا نماذج تؤدي، عند إعادة تأكيدها في الصيغ الأصلية، إلى تناقضات.

الأهمية

يزعم البحث أن إجراء القرار المقترح يوسع قدرات الحل بشكل كبير لـ Bitwazla، مما يمكنه من التعامل مع المشكلات التي تتضمن مصفوفات ثابتة امتدادية ذات نطاقات فهرس محدودة، والتي كانت سابقاً غير قابلة للحل أو يتم التعامل معها بشكل غير صحيح من قبل الأدوات الأخرى.

يعالج هذا العمل فجوة حرجة في حل SMT: بينما تعد المصفوفات الثابتة نمط نمذجة قياسي لتهيئة الذاكرة، فإن أدوات الحل الحالية إما تفتقر إلى دعمها في النطاقات المحدودة أو تقدم نتائج غير سليمة. من خلال توفير إجراء قرار سليم وكامل لنظرية المصفوفات الثابتة الامتدادية الكاملة (سواء كانت محدودة أو لانهائية)، يتيح هذا العمل عمليات تحقق أكثر دقة وكفاءة في تطبيقات مثل التحقق من النماذج العتادية (hardware model checking) والتحقق من العقود الذكية (تحديداً آلة إيثيريوم الافتراضية). ويشير المؤلفون إلى أنه بينما ركز تقييمهم على النطاقات المحدودة، فإن الإجراء محايد تجاه بنية الحل الأساسية ويدعم حالات النطاق اللانهائي أيضاً بشكل كامل.