Reality Code Engine: شكل واحد بلا فقد لبرمجة أصلية ومُتحقَّق منها ومنخفضة الطاقة

الإصدار 1.4، 13 أكتوبر 2026. المواصفة: المسودة الحالية (وثيقة المسودة 0.7، إصدار اللغة 0.8)، من openIE-dev/rce 2a0ec68. التغييرات في 1.4: عدد اختبارات المحرك هو الاختبارات المتمايزة الـ 589 التي يشغّلها cargo test --release (طبع الإصدار 1.3 العدد 596، وهو مجموع make check الذي يعدّ 7 اختبارات برهان مرتين)؛ ويذكر القسم 3.7 أن المواصفة 2.7 تعطي الآن قاعدة التكلفة لكل موضع استدعاء من C.15؛ ويُعرض المقترِح الحتمي في القسم 5.5 بـ 87 متطابقة مقدَّمة و9 مقبولة و78 مرفوضة، من اختبار المحرك؛ ويحمل Software Heritage وRosetta Code في القسم 7 المراجع [129] إلى [131]، مع إعادة قراءة عدّادات الأرشيف؛ وتُضاف تسعة أشكال توضيحية (الأشكال التوضيحية 5 إلى 10 و12 و13 و15)، وصار الشكلان التوضيحيان 5 و6 السابقان الشكلين التوضيحيين 11 و14. التغييرات في 1.3: تُنسب تكاليف الطرائق المتدرجة بالحجم إلى إصدار اللغة 0.7 (كانت موصوفة تحت 0.6 في 1.2)، وتُذكر قاعدة كل موضع استدعاء للبرامج مختلطة الإصدارات، وتُعاد الفحوص عند التزام المحرك 1eb5f02. البيانات والشيفرة: research.openie.dev/data/. ساحة التجريب (المدقق المرجعي): openie-dev.github.io/rce. العرض التوضيحي للمحرك: /demos/rce-engine/. ملف PDF بصيغة LaTeX: /pdfs/latex/rce.pdf (المصدر).

التصحيحات وحالة قابلية إعادة الإنتاج (17 أكتوبر 2026). أُضيفت هذه الملاحظة بعد قراءة للورقة مقابل المستودعات العامة. الأرقام التي تتأثر بها مدرجة هنا، وفيما عدا ذلك لم يتغير النص أدناه. كل عدد أدناه مأخوذ من src/data/rce-facts.json، الذي يُنتجه scripts/claim-counts.py في openIE-dev/rce عند e416fd0، باستثناء عددَي Lean، فقد أُخذا عند 4304048.

• لغة واحدة (18 أكتوبر 2026). في الفرع الرئيسي العام لـ rce (4a3dc1f) لغة واحدة ونص واحد. وسطر # rce-version: وسمُ إصدار مُتسامَح معه ومُتجاهَل لا يدخل في التجزئة، ووسم الإصدار يسمّي التزامًا واحدًا بعينه للمواصفة (C.15). والبنية التي لا ينفّذها المدقق تُرفض بوصفها محجوزة غير منفَّذة (W-RES-1، الملحق F.12)، لا بحسب الإصدار؛ وهناك قائمة واحدة للكلمات المحجوزة. لذا فإن القسم 3.7 والشكل التوضيحي 5، اللذين يصفان بوابات الإصدار (الإصدارات من 0.5 إلى 0.9)، يصفان مسودات أقدم ولم يعودا ساريين. والاستدعاء الفاشل يستعيد وسائطه من نوع &mut (F.4.4)، وهذا يحل محل قاعدة الكتابة الراجعة في المبرهنة T33. والأعداد أدناه أُخذت عند e416fd0، قبل هذا التغيير، ولم يُعَد تشغيلها. وتغيّر برهان T33 مع القاعدة: فقد خرجت المبرهنات الملغاة الخاصة بالكتابة الراجعة عند كل نتيجة من الشجرة المدقَّقة (الفرع الرئيسي العام لـ rce عند 95ead2e)، وصارت T33 تبرهن استعادة F.4.4؛ ويُبلغ التدقيق 4875 مبرهنة مع المسلّمات القياسية وحدها.
• أسماء المكتبة (rce-stdlib، 18 أكتوبر 2026). لأن قائمة الكلمات المحجوزة عامة، أُعيدت تسمية أسماء المكتبة التي صارت محجوزة فيها: label إلى lbl، وnode إلى nd، وgroup إلى grp، وchild إلى chd، وbudget إلى bud، وrestart إلى rst، وreplicated إلى repl، وct إلى ctext، وsession إلى sess، وprotocol إلى proto، وpar إلى parl، وoffer إلى offr، وchoose إلى chse. والنوعان Json (الوحدة enc) وUrl (الوحدة net.url) صارا JsonDoc وUrlParts، لذا يجب على البرنامج الذي يستورد enc.Json أو net.url.Url أن يستخدم الأسماء الجديدة. وطول النص .len() لقيمة من نوع text هو .len_bytes() (بالبايتات) أو .len_chars().
• الإصدارات والأعداد عند e416fd0. وثيقة المواصفة هي المسودة 0.9 (علنية منذ cdae5cf). وقبل 18 أكتوبر كان المدقق المرجعي يقبل إصدارات اللغة من 0.5 إلى 0.9، ويرفض، بحسب الإصدار، أجزاء الإصدار 0.9 التي لم يكن ينفّذها (الملحق F.12). والمبرهنات من T1 إلى T56 مُصاغة؛ والمبرهنات من T42 إلى T56 (الملحق F) مُصاغة وغير مُبرهنة. وهناك 58 وحدة Lean و59 برنامجًا مثالًا (57 في المستوى الأعلى و2 في حزم). والأشكال التوضيحية والتعليقات في هذه الورقة التي تذكر المسودة 0.7 أو إصدار اللغة 0.8 أو T1 إلى T34 أو 31 ملفًا أو 51 مثالًا تصف المستودع عند الالتزامات الأقدم التي تسمّيها، ولا تصف هذه الورقة المسودة 0.9 بما يتجاوز هذه الملاحظة.
• عدد مبرهنات Lean. يوجد عددان مختلفان. يحوي المصدر 1,116 تصريحًا من نوع theorem وlemma عند e416fd0 (885 عند 4304048). ويعدّ التدقيق (scripts/lean-audit.sh) كل ثابت مبرهنة في بيئة النواة، بما في ذلك الثوابت التي يولّدها المُفصِّل (elaborator)، وأعطى 4,877 في إعادة تشغيل على المستودع العام عند e416fd0، حيث يكتمل lake build على 58 ملفًا في spec/lean/RCE/ من دون أي sorry ومع المسلّمات القياسية فقط (2,949 على 46 ملفًا عند 4304048). والعدد 2,192 المذكور أدناه هو عدد التدقيق عند التزام المحرك 1eb5f02 على 31 وحدة. ولا يقول أيّ من العددين شيئًا عن عدد المبرهنات المُبرهنة بشأن مقيِّم Rust.
• قابل لإعادة الإنتاج من المستودعات العامة اليوم: بناء Lean وتدقيق المسلّمات، وفحص المواصفة (جداول القواعد النحوية ومدوّنات الأمثلة)، والمدقق المرجعي واختباراته، ومتجهات JSON القانونية.
• غير قابل لإعادة الإنتاج بعدُ من المستودعات العامة: تشغيل المنظومة على 10,000 شكل (bench/ecosystem ليس في المستودعات العامة)، ونتائج Kani، واختبارات المحرك الـ 589، ومعدلات الإصلاح في القسم 6، وأي رقم لـ Defects4J. وهي معروضة هنا بوصفها تشغيلات أجراها المؤلفون أنفسهم، وينبغي أن تُقرأ على هذا النحو إلى أن تُنشر المصادر والبذور.
• معيار الدحض RCE-F0. انظر الملاحظة في القسم 2.3 أدناه.

الملخص

تصف هذه الورقة Reality Code Engine (RCE)، وهو نظام يُكتب فيه البرنامج مرة واحدة في صورة آلة حالات تُسمّى الشكل (Form)، وتُولَّد منه الشيفرة بلغات أخرى. وتعرض الورقة ما قيس على 10,000 شكل وعلى مجموعات بيانات علنية للأخطاء البرمجية، وتبيّن كيف يمكن إثبات خطأ ادعاءاتها.

بكلمات بسيطة

1. يُكتب البرنامج مرة واحدة، في شكل واحد دقيق، ويُنتج الحاسوب منه البرنامج نفسه بلغات كثيرة.
2. لأن الشكل لا يسمح إلا بما صُرِّح به، تُرفض المدخلات المعطوبة عند الباب بدلًا من إصلاحها لاحقًا.
3. الإصلاح الذي يجتاز الفحوص يُحفظ ويُعاد استخدامه، فلا تكلّف المشكلة نفسها وقتًا أو طاقة مرتين.

1. الأطروحة

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

Reality Code Engine (RCE) نقطة واحدة في هذا الفضاء، وهذه الورقة تصفها وتقيسها. يُنمذج RCE البرنامج بوصفه آلة حالات دالية قائمة على قاعدة بيانات. قاس Lopes وزملاؤه أن نحو 70% من الشيفرة على GitHub نُسخ مستنسخة من ملفات سابقة [33]، ولذلك يحاول RCE أولًا استرجاع ملاءمة موجودة وتكييفها وفحصها، ولا يستدعي نموذجًا إلا حين لا يغلق المهمةَ شيءٌ أرخص.

الادعاء الجوهري. RCE منظومة شيفرة كاملة تُؤلَّف فيها البرامج أصلًا انطلاقًا من النية. تُكتب النية مرة واحدة، في صورة شكل: حالة، ومجموعة من الأحداث، وانتقال نقي وكلّي. والشكل ترميز بلا فقد لتلك النية. وكل هدف (مخطط الحالات statechart، وRust، وPython، وXState، وSCXML، وWASM) إسقاط للشكل، وكل إسقاط يعيد تشغيل أثر الشكل بايتًا ببايت. لا يمكن كتابة حالة لم يصرّح بها الشكل، ويُرفض عند الدخول كل مُدخل يقع خارج عقده. ولذلك لا يمكن لبرنامج داخل المنظومة أن ينحرف عن نيته كما ينحرف برنامج بلغة شائعة عن تعليقاته أو اختباراته أو تطبيقاته الأخرى، ولا يحتاج إلى مقارنة فروق أو تتبع أخطاء بعد وقوعها. وكل ملاءمة تجتاز البوابة تُخزَّن ويُعاد استخدامها، فتتراكم المنظومة كلما نمت (§2.4). والشيفرة المكتوبة بلغات أخرى باب واحد للدخول: فهي تدخل بالرفع (§6).

تواجه كل نقطة في الفضاء البوابة نفسها. البوابة هي الصحة: محمول الاكتمال للمهمة $C(z)$، وهو هنا اختبارات المهمة أو برهان أو أثر توافق. ومن بين التشغيلات التي تجتاز البوابة تُرتَّب الأنظمة بالطاقة المنفقة بالجول حتى الإنجاز، $J^{\ast }$. الصحة قيد، لا درجة.

تعمل آليات RCE، المسماة تروسًا، بترتيب التكلفة، وأول ترس يجتاز البوابة يغلق المهمة.

تُوسم أرقام الطاقة بحسب مصدرها. est_j تقدير تحليلي. reported_j عدّاد لنظام التشغيل أو عدّاد على الشريحة. measured_j محجوز لعدّاد جداري، وهو فارغ في كل نتيجة هنا.

2. فضاء تصميم البرمجة المستقلة

النية عالية الإنتروبيا. عبارة “اجعل صفحة الدفع أسرع” تحمل معاني كثيرة: تحميلًا أقصر للصفحة، أو خطوات أقل، أو موافقة أسرع على البطاقة، أو سلة مخزنة مؤقتًا، أو سرعة أكبر على فئة واحدة من الأجهزة. السياق ضمني ولا يُكتب أبدًا. قاس Shannon الإنجليزية المطبوعة بنحو 0.6 إلى 1.3 بت لكل حرف [1]. الحروف قابلة للتنبؤ. المعنى ليس كذلك.

كل تحويل يفقد معلومات. تصير النية مواصفة، فيضيع السياق. وتصير المواصفة واحدة من مئات اللغات السطحية، فتضيع البدائل والحالات الحدية. ويصير المصدر تمثيلًا وسيطًا (IR)، فتضيع الأسماء والأسلوب وأسباب المؤلف. ويصير التمثيل الوسيط شيفرة آلة، فتصير الأنواع أحجامًا والحلقات قفزات.

الأرضية منخفضة الإنتروبيا. ينتهي كل برنامج إلى تحميلات وتخزينات وعمليات حسابية وقفزات. والوجهة لا تتسع إلا لأشكال قليلة، فتنحني الشيفرة نحوها. التقارب مقصود في التصميم.

الحدود هي حيث يتباعد المعنى. يعطي السطر نفسه أجوبة مختلفة عند الأطراف. في Python تكون قيمة -3 % 2 هي 1، وقيمة -7 / 2 هي -3.5. وفي C تكون قيمة -3 % 2 هي -1، وقيمة -7 / 2 هي -3، والفيضان في الأعداد ذات الإشارة غير معرَّف. والنظام الذي يعيد توليد الشيفرة عند كل حد يخمّن عند كل حد.

المحاور مصوغة كمقادير.

المحور	أحد الطرفين	الطرف الآخر	موضع RCE
الطاقة لكل نتيجة صحيحة	تُدفع كاملة من جديد في كل مهمة	تُدفع مرة لكل حالة جديدة، ثم أرضية المعالج	عند الأرضية في المهام المغطاة
الإنتروبيا المحسومة وقت التشغيل، والحتمية	التوزيع الكامل للموجِّه، وعينة جديدة في كل مرة	المتبقي الذي لا تغطيه أي ملاءمة مخزنة فقط، ومُخرَج حتمي واحد	المتبقي فقط؛ وكل إسقاط حتمي
قوة التحقق	يُقبل المُخرَج بالمعاينة	اختبارات وتغطية وشهادة برهان	البوابة الكاملة على كل نتيجة
إعادة الاستخدام والتراكم	كل نتيجة تُستخدم مرة واحدة	كل ملاءمة مقبولة تُخزَّن ويُعاد استخدامها	كل ملاءمة تجتاز البوابة تُخزَّن
الاعتماد على النموذج	نموذج في كل مهمة	لا نموذج	نموذج في الترس الأخير فقط

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

يرسم الشكل التوضيحي 2 المحاور الخمسة ويضع عليها الفئات الرئيسية من المناهج.

2.1 البرمجة نظرية ترميز

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

المقياس. عرّف Shannon إنتروبيا المصدر وسعة القناة [40]، وقاس الإنجليزية المطبوعة بنحو 0.6 إلى 1.3 بت لكل حرف [1]. وقدّم Kolmogorov، في مقال بالروسية في Problemy Peredachi Informatsii عام 1965، ثلاث مقاربات لكمية المعلومات وجعل المقاربة الخوارزمية أولاها: المعلومات في شيء ما هي طول أقصر برنامج ينتجه [41]. وكان Solomonoff قد وصل إلى الشيء نفسه بوصفه نظرية في الاستدلال الاستقرائي [42]، وبيّن Chaitin أن حجم البرنامج يخضع لمتطابقات مماثلة صوريًا لمتطابقات Shannon [43]. وحوّل Rissanen الفكرة إلى قاعدة لاختيار النماذج، هي طول الوصف الأدنى [44]. ومعًا يقولون إن البرنامج كلمة رمزية: وصف لسلوك، وأقصر وصف صحيح هو الأرضية. وقاعدة الاستخلاص في RCE، أي الاحتفاظ بالملاءمة الأقل استهلاكًا بالجول بين الملاءمات المتكافئة (القضية 3)، هي تلك القاعدة مع الجول بدل البت.

الشيفرة تقع في النظام منخفض الإنتروبيا، وقد قاس الناس ذلك. وجد Hindle وBarr وSu وGabel وDevanbu أن الشيفرة “very repetitive, and in fact even more so than natural languages”، أي شديدة التكرار بل أشد من اللغات الطبيعية، بإنتروبيا متقاطعة أدنى تحت نماذج n-gram نفسها [35]. ووجد Gabel وSu أن معظم أسطر أي مشروع موجودة في مكان آخر [34]، ووجد Lopes et al. أن معظم الملفات على GitHub نسخ مستنسخة [33]. ووجد Tu وSu وDevanbu أن الشيفرة محلية أيضًا: ما كُتب قريبًا يتنبأ بما يأتي بعده [46]. ووجد Ray وزملاؤه أن الأسطر المعيبة أقل طبيعية، بإنتروبيا أعلى، وأن الإنتروبيا تنخفض حين يُصلح الخطأ [45]. وفي 2025 استخدم Yang وKolak وHellendoorn وMartins تغيّر الإنتروبيا الذي تُحدثه الرقعة لترتيب مرشحي الإصلاح ولفصل الرقع الصحيحة عن الرقع المفرطة في الملاءمة للاختبارات [51]. ومسح Allamanis وBarr وDevanbu وSutton هذا الحقل تحت اسم الطبيعية [47]. وليست النتيجة نتيجة إنجليزية فقط. فقد عرضها Prem Devanbu في كلمة رئيسية في مؤتمر هندسة البرمجيات في الهند عام 2013 [50]. وقاس Sridhara وSinha وMani في IBM Research India المصنوعات اللغوية الطبيعية المحيطة بالشيفرة في المؤتمر نفسه، فوجدوا أن رسائل الالتزام هي الأكثر انتظامًا وأن نصوص Stack Overflow تسلك سلوك الإنجليزية العادية [49]. وفي الصين نشرت مجلة Journal of Software (软件学报) عام 2022 مراجعة لبحوث طبيعية الشيفرة، تذكر مقياس الإنتروبيا المتقاطعة والنتيجة القائلة إن الشيفرة المعيبة أعلى إنتروبيا [48]. وفي اليابان استخدم Doi وHigo وArima وShimonaka وKusumoto في جامعة أوساكا طبيعية n-gram، أولًا في تقرير تقني لـ IEICE باليابانية ثم في ICPC 2018، للتمييز بين ملفات المصدر المولَّدة آليًا والمكتوبة بيد البشر [73, 74]. والشيفرة المولَّدة أدنى على سلم الإنتروبيا من الشيفرة البشرية، لأن المولِّد تحويل ثابت. وفي البرازيل بنت أطروحة الدكتوراه لـ Arrebola اقتراح الشيفرة على نماذج n-gram ونماذج المواضيع مقسّمة بحسب المشروع والمشرف، وقيّمته بالإنتروبيا المتقاطعة، أي البتات اللازمة لترميز الرمز التالي [75]. والنظامان ظاهران في مستودع واحد: النص النثري المحيط بالشيفرة عالي الإنتروبيا، والشيفرة منخفضة الإنتروبيا.

المقياس مهم. قارن Febres وJaffé وGershenson، من فنزويلا والمكسيك، نصوصًا إنجليزية وإسبانية ونصوص برامج بتنوّع المفردات نسبةً إلى طول الرسالة، فوجدوا نص البرامج أكثر تنوعًا [76]. ووجد Rahman وPalani وRigby أن جزءًا كبيرًا من قابلية التنبؤ بالشيفرة في نماذج n-gram يأتي من رموز البنية النحوية، وأن الشيفرة تبقى تكرارية، وإن بدرجة أقل مما أُبلغ أولًا، بعد إزالتها، وأن استخدام واجهات API هو الجزء الأكثر تكرارًا [77]. والنتيجتان كلتاهما تشحذان الادعاء ولا تقلبانه. فتنوّع الرموز ليس قابلية للتنبؤ، والنظام منخفض الإنتروبيا خاصية للتوزيع الشرطي للخطوة التالية، وهو ما يثبّته الانتقال الحتمي. ولهذا السبب يعتمد الترس G0 في RCE على الأشكال لا على الرموز السطحية.

النية تقع في النظام عالي الإنتروبيا. بيّن Zave وJackson أن المتطلب عبارة عن البيئة، وأن المواصفة عبارة عند الواجهة، وأن الفجوة بينهما لا تملؤها إلا معرفة المجال التي كثيرًا ما تبقى غير مكتوبة [64]. وقسم Brooks صعوبة البرمجيات إلى جوهر وعرض: الجوهر هو البناء المفاهيمي، ومعظمه مواصفة وتصميم لا تمثيل [61]. وجادل Naur بأن البرنامج هو الجزء المرئي من نظرية يحملها مبرمجوه، وأن تلك النظرية لا يمكن استعادتها كاملة من النص [62]. وإذا قُرئ الثلاثة عبر Shannon قالوا الشيء نفسه. فالنية تحمل من عدم اليقين أكثر مما يحمل أي برنامج واحد، وكتابة البرنامج هي الفعل الذي يزيله. وما يبقى في رأس المبرمج بعد كتابة الشيفرة هو الجزء من النية الذي لم ترمّزه الشيفرة.

التحويل تنقيح، والتنقيح تضييق. أعطى Hoare البرامج منطقًا يكون فيه البرنامج صحيحًا نسبةً إلى شرط مسبق وشرط لاحق [54]. وعلّم Wirth التنقيح التدريجي: تفكيك المهمة إلى تعليمات بقرارات متتالية، يثبّت كل منها خيارًا تركته المواصفة مفتوحًا [53]. وجعلت الأوامر المحروسة عند Dijkstra الخيارات المفتوحة صريحة بوصفها لاحتمية، واشتقت البرامج من المواصفات بإزالتها [52]. وفي ميونخ بنى مشروع CIP لـ Bauer وWössner تطوير البرامج بوصفه سلسلة من التحويلات الحافظة للصحة من المواصفة إلى البرنامج [58]. وفي فرنسا حملت طريقة B لـ Abrial ثم Event-B التنقيح إلى النطاق الصناعي، مع التزامات برهان عند كل خطوة [55, 56]. وفي فنلندا أعطى Back وvon Wright التنقيح حسابه القائم على نظرية الشبكيات [57]. وفي كل منها تدل المواصفة على مجموعة من السلوكيات المقبولة، وكل خطوة تنقيح تقلّص المجموعة، حتى يبقى سلوك حتمي واحد. هذا خفض للإنتروبيا مع برهان عند كل خطوة. وشكل RCE هو العنصر الأخير في تلك السلسلة: انتقال كلّي وحتمي $\delta$ على حالات قاعدة البيانات، مع حسم كل خيار (§3.2).

التركيب بحث يضيّق فضاء فرضيات. يتعلم FlashFill لـ Gulwani برنامجًا للسلاسل النصية من أمثلة قليلة للمدخلات والمخرجات بتمثيل مجموعة كل البرامج المتسقة وتقاطعها مع كل مثال جديد [59]. ويصوغ Gulwani وPolozov وSingh تركيب البرامج عمومًا بوصفه بحثًا في فضاء من البرامج تقيّده النية [60]، ويملأ أسلوب التخطيط (sketching) لدى Solar-Lezama الثغرات في برنامج جزئي بمحلّل [27]. وكل مثال أو قيد قياس يزيل فرضيات. ومقياس Shannon يعدّ كم قياسًا من هذا النوع نحتاج. والترس G2 في RCE هو ذلك الترس.

ما ينتجه التحويل له شكل واحد. برهن Gurevich أن كل خوارزمية تسلسلية تلتقطها آلة حالات مجردة عند مستوى تجريدها الخاص [2]. وجعل Codd الحالة علاقة [5]، ويجعل مصدر الأحداث (event sourcing) الحالةَ طيًّا لسجل لا يُضاف إليه إلا من آخره [14]. وبحسب Curry وHoward، البرهان برنامج والقضية نوع [18, 72]، فالملاءمة المتحقَّق منها برهان على مواصفتها. هذه هي أسباب قلة الأشكال في النظام منخفض الإنتروبيا: الوجهة آلة حالات على قاعدة بيانات، أيًّا كانت اللغة السطحية.

الإنتروبيا المنخفضة تتحلل من دون بوابة. لاحظ Lehman على مدى عقود من الأنظمة الكبيرة أن البرنامج المستخدَم يجب أن يستمر في التغير، وأن تعقيده ينمو ما لم يُبذل عمل لخفضه [63]. وقاس Torres وBaltes وTreude وWagner الإنتروبيا البنيوية والنصية عبر تواريخ الالتزامات في 25 مشروعًا، فوجدوا أنهما ترتفعان معًا [78]. تتدفق الإنتروبيا عائدةً إلى الشيفرة من البيئة. والنظام الذي يُبقي الشيفرة في النظام منخفض الإنتروبيا يحتاج إلى بوابة على كل تغيير، وبوابة RCE هي الصحة (§4.3).

المترجمات تقوم أصلًا بترميز المصدر. شحن Franz وKistler البرامج في صورة أشجار نحوية مجردة مضغوطة وولّدوا شيفرة أصلية عند التحميل، وهذا ترميز مصدر لبرنامج على قواعده النحوية الخاصة [67]. واستنتج Fraser نماذج إحصائية للشيفرة من مدوّنة نصية لضغطها [68]. وبيّن Futamura عام 1971، في المجلة اليابانية Systems, Computers, Controls، أن تخصيص مفسِّر لبرنامج ما يعطي برنامجًا مترجَمًا، وأن تخصيص المخصِّص يعطي مترجمًا [70]. وطوّر Ershov في نوفوسيبيرسك الفكرة نفسها تحت اسم الحساب المختلط [71]. ويحسب التفسير المجرد لدى الزوجين Cousot وصفًا سليمًا أقل معلومات لكل سلوك لبرنامج ما [69]. أما التشبيه بترميز القناة فهو قراءة هذه الورقة لا مبرهنة مستشهد بها: الأنواع والاختبارات والبراهين تضيف تكرارًا مفحوصًا بحيث يُكتشف البرنامج الخاطئ قبل تشغيله، كما يكتشف فحص التكافؤ كلمة تالفة.

المحو هو موضع إنفاق الجول. بيّن Landauer أن الخطوة غير القابلة للعكس منطقيًا، أي محو بت واحد، تبدد على الأقل $k_{B}T\ln 2$ [65]. وبيّن Bennett أن الحساب يمكن مبدئيًا أن يُجعل قابلًا للعكس منطقيًا، فيكون المحو، لا الحساب، هو حامل الحد [66]. وتحويل نية عالية الإنتروبيا إلى برنامج واحد منخفض الإنتروبيا يطرح كل بديل سمحت به النية. وهذا الطرح محو لمعلومات عن البدائل، وله أرضية ديناميكية حرارية. يدفع RCE ثمن الطرح مرة لكل حالة جديدة ويخزّن النتيجة، فلا تمحو الحالة المتكررة شيئًا جديدًا.

2.2 كيف يحوّل RCE، وأين يقع كل ترس

إذا قُرئت المهمة بوصفها نظرية ترميز فهي تصل كرسالة يكون عدم اليقين الباقي فيها هو ما لا تحسمه أي ملاءمة مخزنة. يزيل كل ترس عدم اليقين بسعر مختلف، والتروس مرتبة بحسب ذلك السعر (§4.2).

الترس	ما يفعله بعدم اليقين	نسبه في الحجة أعلاه
G0 البحث	يتعرّف أن النية رُمّزت من قبل؛ ويحسمها بالاسترجاع، عند أرضية المعالج	التكرار والنسخ المستنسخة [33, 34, 35]؛ المحلية [46]
G1 القواعد	يطبّق إعادة كتابة محروسة معروفة؛ ويحسم متبقيًا متكررًا من دون بحث	التحويل الحافظ للصحة [52, 58]؛ التنقيح مع التزامات البرهان [55, 56]
G2 التركيب	يبحث في فضاء فرضيات ويضيّقه بالأمثلة والقيود والمحلّل	تركيب البرامج بوصفه بحثًا [27, 59, 60]
G3 إلى G5 النماذج	يأخذ عينة من توزيع متعلَّم على الشيفرة حين لا يغلق أي ترس أدنى الفجوة؛ مقترِح فقط	نماذج الإنتروبيا المتقاطعة للشيفرة [35, 47]
البوابة	لا تقبل مرشحًا إلا مع اختبارات وتغطية وشهادة برهان	منطق Hoare [54]؛ Curry-Howard [18, 72]
الترقية	تخزّن الملاءمة المقبولة، فيكلّف المتبقي نفسه G0 في المرة التالية	طول الوصف الأدنى [44]؛ محو Landauer مدفوع مرة واحدة [65]

تختلف المواضع على محاور القسم 2 في موضع دفع ثمن التحويل. فالنهج الذي يأخذ عينة من التوزيع الكامل للموجِّه في كل مهمة يدفع ثمن الجانب عالي الإنتروبيا من جديد في كل مرة. والنهج الذي يخزّن الملاءمات المقبولة ويعيد استخدامها لا يدفع إلا ثمن المتبقي، ومرة واحدة فقط. ومعظم الأنظمة تقع بين هذين الطرفين، ويقع RCE عند طرف إعادة الاستخدام.

2.3 المنظومة عند N كبير

يُقاس ادعاء §1 مباشرة. سُجّل المقياس المرجعي مسبقًا قبل التشغيل (bench/ecosystem/PREREG.json). يكتب مولِّد ذو بذرة 10,000 شكل، كل منها مصدر، وقاعدة جسمها حدّ حسابي عشوائي بعمق يصل إلى 3 على ثمانية مؤثرات، ومصبّ. المحرك مجمّد عند الالتزام a079967، ولا يُستدعى أي نموذج.

الخاصية	ما يُفحص لكل شكل	N	تتحقق	استدعاءات النموذج
ترميز بلا فقد	التمثيل الوسيط للشكل إلى JSON قانوني إلى التمثيل الوسيط للشكل إلى JSON قانوني هو الدالة المحايدة	10,000	10,000	0
إسقاط حتمي	ترجمتان تعطيان البايتات نفسها؛ وإسقاطا XState وSCXML للشكل الأصلي وللشكل بعد الذهاب والإياب متطابقان بايتًا ببايت	10,000	10,000	0
إسقاط أمين، Python	وحدة Python المولَّدة تطبع الأثر المرجعي بايتًا ببايت على 40 حدثًا ذا بذرة	10,000	9,999	0
البوابة عند الدخول، المدخلات	خمسة أنواع من الحمولات المعيبة (نوع خاطئ، null، حقل مفقود، فارغ، متداخل) تُرفض كلها، ولا نتيجة مقبولة	10,000	10,000	0
البوابة عند الدخول، المواصفات	تُرفض قبل الترجمة المواصفةُ التي فيها تدفق إلى عقدة غير مصرّح بها	10,000	10,000	0

يعرض الشكل التوضيحي 3 الأعداد نفسها.

RCE-F0 وإخفاقة Python. يصوغ القسم 9 المعيار RCE-F0 هكذا: في تشغيل مسجل مسبقًا من 10,000 شكل على الأقل، يطبع أي إسقاط أثرًا يختلف عن الأثر المرجعي للشكل، أو يُقبل أي مُدخل معيب. وهذا التشغيل مسجل مسبقًا، وفيه 10,000 شكل، ولم تطبع وحدة Python واحدة مولَّدة الأثر المرجعي، فالملاحظة كما هي مكتوبة تستوفي شرط RCE-F0. وتعرض الورقة الإخفاقة واختبار الانحدار أدناه، ولا تقدّم لها سببًا جذريًا. اقرأ نص RCE-F0 كما صيغ: الادعاء الذي يدحضه هو أن الإسقاطات أمينة، ولم يستوفِ إسقاط Python في هذا التشغيل ذلك الادعاء على شكل واحد. وأما هل تأتي الإخفاقة من المولِّد أم من حزمة الاختبار فمسألة مفتوحة هنا. وكون الشكل نفسه يُعاد تشغيله على نحو متطابق تحت 32 بذرة تجزئة لا يحسم ذلك.

تُعدّ إخفاقة Python الوحيدة إخفاقة؛ ويُعاد تشغيل الشكل نفسه والأحداث نفسها على نحو متطابق تحت 32 بذرة تجزئة في اختبار الانحدار tests/form_ecosystem_regress.rs. الطاقة هنا est_j فقط؛ واستغرق التشغيل كله 393 ثانية من وقت المعالج على نواة واحدة. الأشكال المولَّدة صغيرة، فهذا الجدول يقيس الترميز والإسقاطات والبوابة. أما الأشكال المرفوعة من برامج حقيقية فتُقاس وفق بروتوكول §8.7.

2.4 تحسين ذاتي تكراري متحقَّق منه ومحكوم ببوابة

عرّف Good (1965) [111] الآلة فائقة الذكاء بأنها آلة تستطيع تصميم آلات أفضل، فيتكرر التحسين. وصاغ Yudkowsky (2013) [113] المسألة بوصفها مسألة عوائد: هل تجعل كل وحدة تحسين الوحدةَ التالية أرخص أم أغلى. وقدّمت آلة Gödel لدى Schmidhuber (2007) [112] جوابًا صوريًا بضمان: يعيد برنامج كتابة أي جزء من نفسه، بما في ذلك بحثه الخاص، فقط بعد أن يبرهن أن إعادة الكتابة تحسّن منفعته المتوقعة. ومبرهنة Löb (1955) [114] هي العقبة التي يواجهها مُبرهِن يثق بنفسه، وقد سمّاها Yudkowsky وHerreshoff (2013) [115] عقبة Löb: لا يستطيع نظام عمومًا أن يبرهن سلامة خلَف يستخدم نظام البرهان الخاص به. والأنظمة الحديثة تتخلى عن شرط البرهان وتختار بالدرجة المقيسة: STOP (Zelikman et al., 2023) [116] يحسّن السقالة التي تحسّن الشيفرة، وآلة Darwin Gödel (Zhang et al., 2025) [117] تحتفظ بأرشيف من وكلاء البرمجة المعدَّلين ذاتيًا مختارين بدرجة المقياس المرجعي، وAlphaEvolve (Novikov et al., 2025) [118] يطوّر برامج تحت مقيِّمات آلية، وVoyager (Wang et al., 2023) [119] ينمّي مكتبة من المهارات المتحقَّق منها تعيد المهام اللاحقة استخدامها.

يأخذ RCE بنية آلة Gödel ومكتبة Voyager، مع فرقين يتجنبان العقبة بالنسبة إلى الأشياء التي يرقّيها. أولًا، الشيء الذي يتحسن ليس المُبرهِن. يرقّي RCE المعالجات وإعادات الكتابة والتروس، ويُفحص كل منها مقابل نواة ثابتة معتمدة على حدة: حزم اختبار Kani وترميز SMT لا يتغيران أبدًا بالترقية، فلا تحتاج أي خطوة إلى الثقة بنظام برهان خلَف. ثانيًا، البوابة برهان على الصحة عند الحد، لا درجة. فقد ترتفع الدرجة بينما ينكسر افتراض في الواجهة؛ أما البرهان عند الحد فلا يجتازه تغيير يكسره.

القضية R1 (صحة رتيبة). إذا اجتاز كل تغيير مرقّى فحص حدّه، وبقيت فحوص الحدود الأخرى دون تغيير، فإن كل خاصية أثبتتها تلك الفحوص قبل الترقية تبقى صحيحة بعدها.

القضية R2 (التراكم). لتكن حمولة العمل مجموعة متعددة من المهام، وليغلق معالج مرقّى كل مهمة من شكله. عندئذ يكون عدد التصعيدات في الدورة t غير متزايد في t، والتصحيح المرقّى قبل الدورة 1 يخفض التصعيدات التراكمية لكل أفق بمقدار التصعيدات التي يغلقها في كل دورة لاحقة. وفي حمولة العمل المرجعية للعرض التوضيحي للمحرك، تنخفض التصعيدات التراكمية على ثماني دورات من 21 إلى 15 مع تصحيح واحد عند المصبّات، وتبلغ الصفر في الدورة الأخيرة في الحالتين، مع إغلاق كل مهمة إغلاقًا صحيحًا ومن دون رفض أي ترقية.

يرسم الشكل التوضيحي 4 آلية القضيتين R1 وR2 مع مجاميع حمولة العمل المرجعية.

القضية R3 (تكلفة متناقصة). بما أن المعالج المرقّى يُنفَّذ بدل استدعاء النموذج، وتكلفته هي عدد عمليات المعالج مسعّرةً بجدول الركيزة، فإن طاقة الدورة تنخفض نحو طاقة المعالجات وحدها كلما انخفضت التصعيدات نحو الصفر.

تعطي إسقاطات Futamura (1971، وأعيد نشرها 1999) [120] والترجمة الفائقة (supercompilation) لدى Turchin (1986) [121] نهاية هذه العملية. تخصيص مفسِّر لبرنامج يعطي برنامجًا مترجَمًا؛ وتخصيص المخصِّص يعطي مترجمًا. وترقيات RCE تخصّص مسار التصعيد العام للأشكال التي تقع فعلًا، فيتقارب المحرك نحو البرنامج المتبقي لحمولة عمله: الجزء من الحساب الذي لا يزال على نموذج أو إنسان أن يقدّمه. والتحسين الذاتي التكراري تحت بوابة هو ذلك التقارب، مصنوعًا بخطوات مفحوصة. وتشغّل طبقة Compounding في RCE engine demo حمولة العمل هذه في المتصفح.

3. الشكل

3.1 أقوى صياغة صورية لعبارة “الشكل نفسه”

يُذكر نطاق المبرهنة أولًا. تغطي مسلّمات Gurevich التسلسلية الخوارزميات التسلسلية؛ أما الخوارزميات المتوازية والتفاعلية فتحتاج إلى مسلّمات Blass وGurevich الإضافية [3]. ويجادل Blass وDershowitz وGurevich بأنه لا توجد علاقة تكافؤ واحدة على الخوارزميات تلائم كل غرض [79]، ويعرض Moschovakis وVardi الجدل حول ماهية الخوارزمية [80, 81]. ومعالج الويب الذي يقوم بالإدخال والإخراج يقع خارج المبرهنة التسلسلية. ويعالج الشكل التفاعل كما يعالجه الخط التفاعلي: كل مُدخل حدث في $E$، وآلة الحالات تخطو عليه. فعبارة “شكل واحد” اختيار نمذجي يستند إلى المبرهنة التسلسلية ويمتد بالاصطلاح، مع سوابق إنتاجية في معمارية Elm [83]، وتواريخ أحداث سير العمل الدائمة [84]، ودلاليات التدفقات مثل Flo [82]. وقضايا القسم 3.4 مصوغة لذلك الاختيار.

مبرهنة آلة الحالات المجردة (ASM) لدى Gurevich هي أقوى صياغة صورية لكون كل خوارزمية ذات شكل واحد [2]. آلة الحالات المجردة آلة حالاتها بنى من الرتبة الأولى، وخطوتها مجموعة منتهية من التحديثات المحروسة. يذكر Gurevich ثلاث مسلّمات. الزمن التسلسلي: للخوارزمية حالات وحالات ابتدائية وخريطة خطوة واحدة $\tau$. الحالة المجردة: الحالات بنى من الرتبة الأولى على مفردات ثابتة واحدة، مغلقة تحت التماثل. الاستكشاف المحدود: مجموعة منتهية من الحدود تقرر كل خطوة. ونص مبرهنته الرئيسية (المبرهنة 6.13): “For every sequential algorithm A, there exists an equivalent sequential abstract state machine B”، أي لكل خوارزمية تسلسلية A توجد آلة حالات مجردة تسلسلية مكافئة B. ويوسّعها Blass وGurevich إلى الخوارزميات المتوازية [3]. ويضيف Dershowitz وGurevich بديهية رابعة، هي أن العمليات الابتدائية قابلة للحساب، ويشتقان منها أطروحة Church [4].

3.2 تعريفات

التعريف 1 (الشكل). البرنامج صفّ مرتّب

$P=(S,E,\delta ,D,\lambda )$

• $S={\Sigma }_c\times {\Sigma }_d$، فضاء الحالات: بنى على مفردات ثابتة $\Sigma$، مقسومة إلى مناطق تحكم ${\Sigma }_c$ وبيانات ${\Sigma }_d$. وتحمل ${\Sigma }_d$ الساعة المنطقية وعدد المدخلات والعلاقات ذات الأنواع (وفي اللغة، المناطق المصرّح بها أيضًا). وكل حالة نسخة قاعدة بيانات بمعنى Codd [5].
• $E$، أبجدية الأحداث، بما فيها نبضة الساعة المنطقية.
• $\delta :S\times E\to S\times O^{\ast }$، الانتقال: كلّي وحتمي ونقي، مكتوب كمجموعة منتهية من التحديثات المحروسة “if $\phi$ then $f(\bar{t}):=t_0$”، وكل خطوة تقرأ مجموعة محدودة من المواقع. وهو يعيد الحالة التالية ومخرجات الخطوة. ونكتب ${\delta }_1={\pi }_1\circ \delta$ لمكوّنه الخاص بالحالة.
• $D$، السجل الدائم: متتالية من الإدخالات $\{seq,event,prev\_hash,state\_hash,hash\}$، حيث $state\_hash$ هي SHA-256 للتمثيل القانوني بصيغة JSON للحالة بعد الخطوة، و$hash$ هي SHA-256 للتمثيل القانوني بصيغة JSON للحقول الأربعة الأولى، وأول $prev\_hash$ هو 64 صفرًا. والسجل سلسلة تجزئة، فتغيير أي إدخال سابق يغيّر كل $hash$ لاحقة.
• $\lambda ={\pi }_2\circ \delta :S\times E\to O^{\ast }$، خريطة المخرجات. آلة Mealy تقرأ الوسيطين كليهما [6]؛ وآلة Moore تقرأ الحالة فقط [7].

التعريف 2 (الشكل والملاءمة). الشكل هو هيئة الصف المرتب مع أربعة ثوابت: $\delta$ حتمية ونقية؛ والاستكشاف محدود؛ والمفردات ثابتة؛ والحالة طيّ للسجل،

$\mathrm{state}(D)=\mathrm{foldl}({\delta }_1,s_0,D).$

وقد يحمل السجل أيضًا نتيجة كل إدخال ومخرجاته وحالته. وهذه مشتقة: لا تدخل في التجزئة، ويجب أن تساوي إعادة التشغيل (T1 وT3 في §3.7). وهناك نوعان متمايزان من الرفض. ففي ملف تعريف المحرك يُطبَّق كل حدث، والمُدخل الذي يخفق في عقده ينتج مخرج reject وصف خطأ. وفي اللغة يترك الحدث المرفوض الحالة دون تغيير (T8) ويُسجَّل بوصفه مرفوضًا.

والملاءمة هي البيانات التي تملأ الهيئة: المفردات $\Sigma$، والأبجديتان $E$ و$O$، وبرنامج القواعد $\Pi$ الذي يعرّف $\delta$، وقواعد المخرجات التي تعرّف $\lambda$، والبيانات الابتدائية $s_0$. وبمصطلحات Gurevich الملاءمة هي المفردات وبرنامج ASM والبنى الابتدائية. وبمصطلحات Codd تكون $\Sigma$ هي المخطط و$s_0$ هي النسخة. وبمصطلحات خطوط المنتجات الملاءمة اختيار للخصائص [8]. وبمصطلحات التركيب الموجَّه بالنحو (SyGuS) الملاءمة حدّ من قواعد نحوية يستوفي مواصفة [9].

التعريف 3 (تكافؤ الملاءمات). تتكافأ ملاءمتان حين تتساوى متتاليتا مخرجاتهما تحت $\lambda$ لكل متتالية أحداث $L$.

التعريف 4 (لغة الملاءمة). قواعد نحوية تدل حدودها على ملاءمات. لغات البرمجة ووثائق SCXML وتكوينات XState ومواصفات .rce كلها لغات ملاءمة. وتكون لغة الملاءمة تامة حين يكون لكل برنامج ASM على $\Sigma$ حدّ فيها.

التعريف 5 (إسقاط التحكم). نقسم $\Sigma ={\Sigma }_c\cup {\Sigma }_d$ إلى رموز تحكم منتهية وعلاقات بيانات. ومخطط الحالات لـ $P$ هو إسقاط $\delta$ على ${\Sigma }_c$: الحالات قيم ${\Sigma }_c$، والانتقالات تحمل حدثًا وحارسًا على ${\Sigma }_d$، والأفعال تحديثات على ${\Sigma }_d$. وتعطي مخططات الحالات لدى Harel التسلسل الهرمي والمناطق المتعامدة [10].

التعريف 6 (الرسم الإلكتروني للملاءمة). لملاءمة $F$ ومجموعة $R$ من إعادات الكتابة السليمة، يكون الرسم الإلكتروني للملاءمة (e-graph) $EG(F,R)$ هو الرسم الإلكتروني المشبَع لحدود قواعد $F$ تحت $R$ [11, 12]. وكل صنف إلكتروني يحوي ملاءمات متكافئة بحسب التعريف 3.

التعريف 7 (تكلفة الجول). ${\mathrm{cost}}_J(t)$ هي الطاقة المقدَّرة (est_j) لتشغيل الحد $t$ مرة واحدة على ركيزة مسمّاة، مرجَّحة بالعدد المتوقع من التشغيلات.

3.3 لماذا “آلة حالات دالية قائمة على قاعدة بيانات”

البنية العلائقية المنتهية نسخة قاعدة بيانات، فحالة Gurevich قاعدة بيانات وكل خطوة معاملة محدودة. قاعدة بيانات: $S$ بنية علائقية. دالية: $\delta$ و$\lambda$ نقيتان. آلة حالات: التشغيلات طيّات لـ $\delta$ على الأحداث. ويرسم Moseley وMarks الخط نفسه في المعمارية [13]. ويرسمه مصدر الأحداث في حالة التطبيق: “Capture all changes to an application state as a sequence of events”، أي التقط كل التغييرات على حالة التطبيق كمتتالية من الأحداث [14]. ويرسمه Dedalus في المنطق، حيث الحالة القابلة للتغيير علاقة مفهرسة بالزمن [15].

3.4 قضايا

القضية 1 (الشكل يلتقط كل خوارزمية تسلسلية). لكل خوارزمية تسلسلية $A$ توجد نسخة شكل $P$ تشغيلاتها هي تشغيلات $A$.

مخطط البرهان. تعطي المبرهنة 6.13 آلة ASM $B$ بحالات $A$ وحالاتها الابتدائية وخريطة خطوتها الواحدة. نضع $E=\{\epsilon \}$، و$\delta (s,\epsilon )={\tau }_B(s)$، و$D=(s_0,{\epsilon }^n)$، و$\lambda$ الدالة المحايدة. الطيّ بعد $n$ نبضة هو ${\tau }_A^n(s_0)$. وبحسب النتيجة 3.3 لدى Gurevich، لـ $P$ و$A$ التشغيلات نفسها. ∎

القضية 1b (البرامج التفاعلية). نوسّع $\Sigma$ برمز إدخال صفري المحلات يُضبط على $e$ قبل كل خطوة؛ عندئذ تكون $\delta (s,e)=\tau (s[in:=e])$ خوارزمية تسلسلية على المفردات الموسّعة، وتنطبق القضية 1. والبناء من عندنا.

القضية 1c (قابلية الحساب). تحت بديهية Dershowitz وGurevich، تحسب كل نسخة شكل دالة قابلة للحساب بآلة Turing [4, 16, 17]. لا يضيف الشكل قوة. بل يعطي كل برنامج في الصنف شكلًا واحدًا.

القضية 1d (البراهين ملاءمات). “For each proof of a given proposition, there is a program of the corresponding type”، أي لكل برهان لقضية معطاة يوجد برنامج من النوع المقابل [18]. النوع مواصفة، والبرهان ملاءمة تستوفيها. وبوابة الصحة هي وجود ذلك البرهان أو اختبار قبول ناجح.

القضية 2 (مولِّد واحد). دالة واحدة $G:\mathrm{Fit}\to \mathrm{Program}$ تولّد برنامجًا قابلًا للتشغيل لكل ملاءمة ولا تقرأ أي مجال. الأساس: كل برنامج نسخة شكل، فتُصدر $G$ مخزنًا ذا أنواع، ونوع أحداث، وقواعد مترجمة، وسجلًا مع طيّ، وموزّع مخرجات. ومولّدات الهياكل مثل مولّدات Rails وJHipster وYeoman هي $G$ مقيّدة بلغات ملاءمة صغيرة. وتبدأ هندسة خطوط المنتجات من “the systematic discovery and exploitation of commonality across related software systems”، أي الاكتشاف والاستثمار المنهجيين للقواسم المشتركة بين أنظمة برمجية مترابطة [8]؛ والقاسم المشترك هو الشكل.

القضية 3 (الاستخلاص بأقل طاقة). الاستخلاص بـ ${\mathrm{cost}}_J$ يعيد الحدّ الأقل استهلاكًا بالجول الذي يجده المستخلِص في الصنف الإلكتروني لـ $F$. مخطط البرهان. إعادات الكتابة سليمة، فلكل حدّ في الصنف الإلكتروني السلوك المرصود لـ $F$ ويجتاز البوابة نفسها. والاستخلاص يقلّل التكلفة إلى أدنى حد، والتكلفة بالجول. ∎ هذا هو Mixture of Limits (مزيج الحدود) مطبَّقًا على الشيفرة: احتفظ بالملاءمة الدنيا التي تؤدي المهمة، والباقي هدر.

القضية 4 (حتمية إعادة التشغيل). إذا لم تقرأ $\delta$ ساعة جدارية، ورتّبت التحديثات من دون أسماء، وسجّلت كل مُدخل، فإن إعادتي تشغيل لـ $D$ واحد تعطيان تجزئات حالة متطابقة عند كل خطوة.

القضية 5 (إسقاط مخطط الحالات سليم). أسقِط كل حالة من تشغيل ما على ${\Sigma }_c$. النتيجة تشغيل لمخطط الحالات المُصدَر تحت الأحداث نفسها.

القضية 6 (ميزانية التنسيق). القواعد الموسومة بأنها رتيبة تعمل على النسخ المتماثلة من دون تنسيق؛ ولا تحتاج نقطة تنسيق إلا القواعد غير الرتيبة. الأساس: مبرهنة CALM، “the programs that have consistent, coordination-free distributed implementations are exactly the programs that can be expressed in monotonic logic”، أي أن البرامج التي لها تطبيقات موزعة متسقة وخالية من التنسيق هي بالضبط البرامج التي يمكن التعبير عنها بمنطق رتيب [19].

يُشتق الوسم من القاعدة ولا يُصرَّح به أبدًا، ويرفض فحص التمثيل الوسيط (IR) أي شكل يختلف وسمه المخزَّن عن الوسم المشتق (المواصفة، الملحق D.5):

ما تحويه القاعدة	الوسم	السبب
لا حلّ (resolve) ولا قراءة ولا ربط ولا مسح	رتيبة	كتاباتها لا تفعل إلا إضافة مفاتيح وزيادة عدّادات
حلّ (resolve)	غير رتيبة	يحذف صفوف التصعيد
قراءة لمصبّها الخاص	غير رتيبة	قراءة ثم تعديل ثم كتابة
ربط بمفتاح	غير رتيبة	قد يكون الصف المربوط غائبًا الآن وحاضرًا لاحقًا، أو مكتوبًا فوقه
مسح	غير رتيبة	يرصد العلاقة كلها، بما في ذلك ما هو غائب

الوسم سليم وغير تام: فالربط مع علاقة لا تقبل إلا الإدراج سيكون رتيبًا، لكن ملف التعريف لا يبرهن أن علاقةً ما لا تقبل إلا الإدراج، فلا يدّعي الوسم ذلك. ويكون الشكل خاليًا من التنسيق حين تكون كل قاعدة فيه رتيبة. وكل قراءة وربط ومسح يرى الحالة عند دخول الحدث، فلا تعتمد الحالة اللاحقة لحدث مُدخل على الترتيب الذي تعمل به قواعد المصبّات المختلفة؛ وحده ترتيب المخرجات يعتمد عليه، وهو مثبَّت بتجزئة المحتوى.

القضية 7 (الذكاء بوصفه مشتقة بالنسبة إلى الجول). ليعدّ $X$ المهام التي تجتاز البوابة، و$J$ الجول المنفقة. تُقرأ $\iota =dX/dJ$ بأثر رجعي من $D$، الذي يسجّل كل حدث وest_j الخاصة به. والاستخلاص تحت ${\mathrm{cost}}_J$ يُبقي البوابة ثابتة ولا يرفع $J$، فلا يخفض $\iota$ عند $X$ متساوٍ.

3.5 الرسم والرسم الإلكتروني ومخطط الحالات

البنية	جزء الشكل	ما الذي تقرره
مخطط الحالات	حرّاس $\delta$ على ${\Sigma }_c$	أي انتقال ينطلق
رسم تدفق البيانات	تبعيات القراءة والكتابة لـ $\delta$ و$\lambda$ (شبكات عمليات Kahn [20])	ما الذي يعمل، وبأي ترتيب
الرسم الإلكتروني	صنف تكافؤ الملاءمة	أي ملاءمة متكافئة تعمل

مخطط الحالات والرسم يصفان ملاءمة واحدة. والرسم الإلكتروني يصف كل ملاءمة مكافئة لها. والاستخلاص يختار بينها بالجول.

3.6 منظومة واحدة، بلا فقد، وأطروحة الشمولية

بلا فقد بالبناء. تثبّت مبرهنة ترميز المصدر لدى Shannon أرضية الترميز بلا فقد عند إنتروبيا المصدر [40]. والشكل ترميز بلا فقد للنية بمعنى ضيق قابل للفحص: التسلسل القانوني للشكل تبايني، فالشكلان اللذان يختلفان في أي حالة أو حدث أو انتقال لهما تجزئتا هيئة مختلفتان، وفك ترميز التسلسل يعيد الشكل نفسه. وكل إسقاط إلى هدف دالة في الشكل وحده. والتحويلات ثنائية الاتجاه تجعل الذهاب والإياب دقيقًا. يعرّف Foster وGreenwald وMoore وPierce وSchmitt العدسة بأنها زوج من دالتي get وput مع شروط ذهاب وإياب تجعل العرض ومصدره متوافقين [122]، ويوسّع Hofmann وPierce وWagner الشروط إلى العدسات المتناظرة [123]، ويمسح Czarnecki وزملاؤه شروط الاتساق نفسها عبر هندسة النماذج وقواعد البيانات ولغات البرمجة [124]. وشرط الذهاب والإياب في RCE هو شرط GetPut على مستوى البرنامج كله: ارفع إسقاطًا عائدًا فتبقى تجزئة الهيئة دون تغيير.

صحيح بالبناء. اقترح Dijkstra عام 1968 أن يُطوَّر البرنامج وبرهانه معًا، بحيث تُصمَّم الصحة فيه بدل أن تُختبر [125]. وحمل Hall وChapman هذا النهج إلى نظام آمن تجاري مع مواصفة صورية وتنقيح عند كل خطوة [126]. وقاعدة Minsky في البرمجة الدالية ذات الأنواع، اجعل الحالات غير القانونية غير قابلة للتمثيل، تقول الشيء نفسه على مستوى الأنواع: النوع الذي لا يستطيع حمل قيمة سيئة يزيل الحاجة إلى فحصها [127]. وتشترط البرمجة الدالية الكلية لدى Turner أن تنتهي كل دالة على كل مُدخل، فيدل البرنامج على دالة رياضية بلا إخفاق خفي [128]. وشكل RCE كلّي بمعنى Turner، وأنواع عقده تجعل الحالات غير المصرّح بها غير قابلة للتمثيل بمعنى Minsky، وسلسلة التنقيح في §2.1 تنتهي إليه بمعنى Dijkstra. والنتيجة هي المذكورة في §1: يُرفض الخطأ عند الدخول، فلا يبقى ما يُقارن أو يُتتبع بعد وقوعه.

أطروحة الشمولية. مصوغةً بمصطلحات النظرية، الأطروحة أن هناك شكلًا شاملًا واحدًا. تُؤلَّف البرامج فيه أصلًا، وكل لغة قائمة يمكن الوصول إليها منه بوصفها إسقاطًا أمينًا، وكل برنامج قائم يدخله بالرفع. وتعطي أطروحة Gurevich الأساس: كل خوارزمية تسلسلية تلتقطها، خطوة بخطوة، آلة حالات مجردة عند مستوى تجريدها الخاص [2]، وكذلك الخوارزميات المتوازية [3]. والشكل آلة من هذا النوع على حالة قاعدة بيانات.

القضية U1 (الالتقاط). إذا كان برنامج بلغة $L$ خوارزمية تسلسلية أو متوازية بمعنى Gurevich، فهناك شكل يحاكيه انتقاله خطوة بخطوة عند مستوى تجريد البرنامج [2, 3].

القضية U2 (الإسقاط الأمين). إذا حفظ الإسقاط ${\pi }_L$ لشكل إلى $L$ أثرَ الشكل على كل مُدخل في العقد، فإن الشكل وإسقاطه قابلان للتبادل عند كل مراقب للأثر، ولا تضيف $L$ شيئًا ينقص الشكل.

القضية U3 (الرفع بالبناء). لكل لغة برمجة مستخدمة قواعد نحوية صورية، ومحلّل نحوي ينتج شجرة نحوية ملموسة، وشجرة نحوية مجردة، ودلاليات تثبّتها مواصفتها أو تطبيقها المرجعي. ويُبنى الرفع ${\lambda }_L$ لكل لغة على ثلاث مراحل: القواعد النحوية، ثم الشجرة النحوية المجردة، ثم الشكل، مع إعطاء كل بنية في $L$ قاعدتها في الشكل بحسب دلاليات $L$. والرفع المبني على هذا النحو يحقق ${\pi }_L({\lambda }_L(p))\equiv p$ في السلوك و${\lambda }_L({\pi }_L(F))=F$ في تجزئة الهيئة، فالزوج عدسة بمعنى [122]، ويُحفظ البرنامج المكتوب بـ $L$ بوصفه شكلًا بلا فقد.

القضية U4 (الاستبدال). إذا تحققت U2 وU3 للغة $L$، فلا حاجة إلى كتابة أي برنامج بـ $L$: يُكتب مرة واحدة بوصفه شكلًا ويُصدر بـ $L$ حيث تتطلب منصةٌ ذلك.

U1 مبرهنة. وU2 تُفحص لكل هدف بالاختبار التفاضلي (§5.1) وعند N كبير في §2.3. وU3 بناء، يُبنى لغةً لغةً من القواعد النحوية صعودًا، ويذكر §8.7 كيف يُقاس البناء أثناء إنشائه.

3.7 اللغة: الإصداران 0.6 و0.7، والتكاليف، وحالة المبرهنات

تُعرَّف لغة RCE بمواصفة مكتوبة، هي حاليًا وثيقة المسودة 0.7 عند إصدار اللغة 0.8 (/rce/spec/؛ والمصدر في مستودع rce). وتختار كل وحدة (module) إصدار لغتها بتعليق في سطرها الأول. والوحدة التي تخلو منه هي الإصدار 0.5، لغة الأقسام 2 إلى 10. والوحدة التي تصرّح بـ # rce-version: 0.6 تحصل أيضًا على الملحق C: par وfor ... par وwith budget ومجموعات العمل (workgroups) وLVars والجلسات والمراقِبون (supervisors). والوحدة التي تصرّح بـ # rce-version: 0.7 لها لغة الإصدار 0.6 مع فرق واحد، هو تكلفة طرائق المكتبة القياسية أدناه (الملحق C.15). ويعرّف الملحق D ملف تعريف المحرك، أي مواصفات المعالجات والملاءمات التي يشغّلها محرك هذه الورقة. ولا ترى وحدة الإصدار 0.5 الملحق C أبدًا، فيُقبل كل برنامج صالح بالإصدار 0.5 دون تغيير.

الميزانيات تعدّ العمل. تحتسب كتلة with budget على كل عملية تكلفة ثابتة من جدول الملحق C.6.4، وتتوقف بالفخ budget حين ينفد العدّ. والعدّ وكيل عن العمل، لا قياس للزمن أو الطاقة؛ وest_j منفصل.

العملية	التكلفة
استدعاء دالة مستخدم أو إغلاق (closure)، $c_{call}$	4
طريقة المكتبة القياسية على مستقبِل بحجم $n$، وحجم الوسيط الأول $k$	4 في الإصدار 0.6؛ $4+w(m,n,k)$ في الإصدار 0.7
إرسال أو استقبال على قناة	8
spawn	32
فرع par واحد أو قطعة for ... par واحدة	16
حرفيّة قائمة أو خريطة، أو استيعاب (comprehension)، بـ $n$ نتيجة؛ [x; n]	$4+n$
الفهرسة والتقطيع والوصول إلى العضو؛ والعوامل الأحادية؛ وand وor؛ وعوامل الأعداد الصحيحة والقيم المنطقية والنصوص ومقارناتها	1
+ و- و* للأعداد العشرية	2
/ و% للأعداد العشرية	8

الأحجام هي طول النص بالبايتات في UTF-8، وطول القائمة، وعدد إدخالات الخريطة؛ وأي قيمة أخرى حجمها 0. ويُثبَّت عمل الطريقة $w$ بفئة تعقيدها في المقيِّم المرجعي: $n+k$ للطرائق الخطية على النصوص والقوائم والخرائط (والخرائط قوائم ترابط مرتبة)، و$n\lceil {\log }_{2}n\rceil$ لـ sort (و0 حين $n\le 1$)، و0 لبقية الطرائق. وتُحتسب الاستدعاءات التي تجريها map وfilter وfold لوسيطها الدالي استدعاءاتٍ إضافةً إلى ذلك. ويتشبّع الحساب عند أكبر عدد صحيح بـ 128 بت، ولا تتناقص $w$ أبدًا حين تكبر $n$ أو $k$. ويحسب المقيِّم المرجعي وأوقات تشغيل Rust وPython وJavaScript المُصدَرة الدالة نفسها، ويفحص اختبار أن فخ الميزانية يقع على العملية نفسها في الأربعة كلها.

أي إصدار يحكم التكلفة. يجوز لبرنامج أن يجمع وحدات بإصدارات مختلفة. وتُثبَّت تكلفة استدعاء الطريقة بالإصدار المصرّح به للوحدة التي تحوي تعبير الاستدعاء، بما في ذلك استدعاء داخل إغلاق مكتوب فيها، لا بإصدار الدالة الجاري تشغيلها، ولا بإصدار مستدعيها، ولا بإصدار الوحدة الأولى في البرنامج. والقاعدة معجمية، فربط الوحدات لا يغيّر أي تكلفة؛ وتذكر المواصفة 2.7 القاعدة نفسها وتحيل إلى C.15. وتفحصها اختبارات عند الحد في الاتجاهين على المقيِّم المرجعي وعلى برامج Rust وPython وJavaScript المُصدَرة: فدالة بالإصدار 0.6 تحت with budget تستدعي دالة مستوردة بالإصدار 0.7 ترتّب قائمة من 8 عناصر يُحتسب عليها 24 أكثر من الاستدعاء نفسه لدالة مطابقة بالإصدار 0.6.

حالة المبرهنات. تذكر المواصفة المبرهنات T1 إلى T34 وتسجّل حالة كل منها بدقة. والبراهين مكتوبة بـ Lean 4 (v4.12.0، من دون Mathlib) على حساب نواتي (core calculus). والكلمات المستخدمة لمستوى النتيجة هي هذه. مُبرهَنة تعني برهانًا بـ Lean عن الدلاليات النواتية للغة. مُبرهَنة على دلاليات تعني برهانًا بـ Lean على دلاليات الخطوة الصغيرة لنواة من RCE. نموذج يعني برهانًا بـ Lean عن نموذج مجرد غير موصول بدلاليات RCE ولا بالمقيِّم المرجعي. متجهات تعني أن نتائج المقيِّم المرجعي على برامج مولَّدة تُفحص مقابل النموذج بنواة Lean، وهذا تطابق على عينات، لا برهان عن المقيِّم. مختبَرة تعني اختبارًا تفاضليًا على مدخلات مذكورة. مفحوصة آليًا تعني أنها مقرَّرة ببرنامج، مثل باني جداول LALR(1).

	العبارة	المستوى
T1	الحتمية: نتيجة واحدة لكل حالة وحدث؛ ونتيجة واحدة لكل نبضة في دلاليات التزامن	مُبرهَنة
T2	كلّية $\delta$، مع حدّ صريح لخطوات التقييم؛ والاستدعاء الذاتي البنيوي وتركيب الحدود على طول مخطط الاستدعاءات	مُبرهَنة (نواة التعابير في Lean لا تحوي استدعاءات لدوال المستخدم؛ والاستدعاء الذاتي والتركيب مُبرهَنان على نموذجين منفصلين)
T3	حالة وقت التشغيل هي $\mathrm{foldl}({\delta }_1,s_0,D)$، وإعادة التشغيل تعيد إنتاج كل تجزئة وكل مخرج	مُبرهَنة
T4	التقدّم، بما في ذلك النبضات (تتحرك مهمة ما، أو ينتهي التشغيل أو يبلغ عن Deadlock)	مُبرهَنة
T5	الحفظ (preservation)، بما في ذلك نطاق الأعداد الصحيحة لكل حقل مكتوب	مُبرهَنة
T6	سلامة الذاكرة، ومسارات الاستعارة كاملة، ولا مشاركة قابلة للتغيير بين المهام	مُبرهَنة لنواة الملكية ولدلاليات مزوَّدة بأدوات قياس لمسارات الاستعارة
T7	استقلال تجزئات السجل والمعرّفات وخيارات select عن الأسماء	مُبرهَنة
T8	الذرّية: الحدث المرفوض يترك الحالة دون تغيير	مُبرهَنة
T9-F	أهداف التمثيل الوسيط للشكل (Rust وWASM وPython وXState وSCXML) تطبع الأثر المرجعي	مختبَرة
T9-L	مُصدِرات البرامج (rust وpython وjs) تتفق مع المقيِّم المرجعي	مُبرهَنة لمُصدِر Rust على نواة، بوصفها ترجمة متحقَّقًا منها إلى MiniRust، وهو تضمين عميق لمجموعة Rust الجزئية المُصدَرة؛ وأن rustc ينفّذ MiniRust أمر موثوق به ومختبَر؛ والمُصدِرات الأخرى مختبَرة
T10	القواعد النحوية غير ملتبسة	مفحوصة آليًا (LALR(1)، 0 تعارضات، للإصدارين كليهما) ومأخوذة منها عينات بمولِّد مدخلات عشوائية (fuzzer)
T11	عدالة select	مُبرهَنة على نموذج التدوير
T12	المقبض الخطي يُستهلك مرة واحدة بالضبط على كل مسار	مُبرهَنة على نموذج العبارات
T13	عمليات f32 تعطي البتات نفسها على الأهداف التي تتفق على IEEE 754	مُبرهَنة للضرب؛ وللجمع والطرح والقسمة فإن خاصية التقريب الواحد هي مبرهنة Figueroa، مستشهَد بها وغير مؤتمتة
T14	حساب u64 المفحوص دقيق ضمن النطاق	مُبرهَنة
T15	المكرِّرات تنتهي، وتحترم حدّ الحلقة، ومتسقة البادئات	مُبرهَنة
T16 إلى T31	تزامن الإصدار 0.6: حتمية par، والتبديل، والاختزالات، والخلو من الجمود، والمهل، ومجموعات العمل، والساعات المتجهية، والأولويات، والنطاقات، والفاعلون (actors)، والجلسات، وLVars، والدفعات الذرية، والنسخ المتماثلة	مُبرهَنة على دلاليات: T16 وT17 وT19a وT20 وT23؛ ومُبرهَنة على نموذج للتشغيلات: T24؛ ومُبرهَنة على حساب الجلسات: T28؛ ونموذج: T18 وT19b وT21 وT22 وT25 وT26 وT31؛ ونموذج مع متجهات: T27 وT29 وT30. ولا شيء منها برهان عن المقيِّم المرجعي المكتوب بـ Rust
T32	إعادة التشغيل الأجنبية: لكل عرّاف (oracle)، تساوي إعادة تشغيل السجل التشغيلَ الحي، ويصح عقد الإجابة على كل إجابة مسجَّلة	مُبرهَنة
T33	استعادة &mut عند الفشل (F.4.4): الاستدعاء الفاشل يترك حالة &mut لدى المستدعي كما كانت عند الاستدعاء؛ والاستدعاء الذي يعود يُجري الكتابة الراجعة (وقد أُلغيت القاعدة السابقة للنسخ إلى الخارج عند كل نتيجة)	مُبرهَنة
T34	تمريرة ANF الحافظة للترتيب قبل كل مُصدِر تعطي القيمة نفسها والمخزن نفسه وأثر الاحتسابات وعمليات الإصدار (emits) نفسه	مُبرهَنة لجزء نواتي مع ANF كاملة؛ والتطبيق مختبَر تفاضليًا على كل هدف، بما في ذلك مسح للميزانيات عبر نقطة الفخ

لـ T9 مجموعتا أهداف لأن لمحرك الورقة وللغة مترجمين اثنين. فـ T9-F هو الادعاء عن rce form --emit، الذي يقيسه §5.1. وT9-L هو الادعاء عن مُصدِرات برامج اللغة. والهدف الذي يقع خارج هاتين المجموعتين لا ادعاء T9 له.

الفحوص المُجراة لهذا الإصدار. عند التزام المحرك 1eb5f02، يكتمل lake build على الملفات الـ 31 في spec/lean/RCE/ من دون أي sorry (46 ملفًا عند 4304048 العام، و58 عند e416fd0)، ويُبلغ التدقيق الدائم أن مسلّمات 2,192 ثابت مبرهنة (يعدّ التدقيق كل ثابت مبرهنة في النواة؛ انظر ملاحظة التصحيحات أعلاه) هي propext وQuot.sound وClassical.choice فقط. ويتحقق Kani من 10 من 10 حزم اختبار للنواة (§5.3). وتجتاز اختبارات المحرك (cargo test --release) عدد 589 اختبارًا متمايزًا مع 0 إخفاقات (و2 متجاهَلان)؛ ويُبلغ make check عن 596 لأن خطوة البرهان فيه تشغّل 7 من تلك الاختبارات مرة ثانية. ويجتاز المدقق المرجعي، مبنيًا من المستودع العام كما يبنيه تكامله المستمر، 56 اختبارًا في البناء الافتراضي و112 مع تفعيل مجموعتي الإصدارين 0.6 و0.7، مع 0 إخفاقات، و57 مع اختبار الاتفاق مع tree-sitter. ويبني فحص المواصفة جداول LALR(1) للإصدار 0.5 وللإصدارين 0.6 و0.7، اللذين يتشاركان قواعد نحوية واحدة، مع 0 تعارضات، ويحلّل كل مثال بثلاثة محللات نحوية، ويجتاز بناء WebAssembly للمدقق 401 من 401 فحص مقابل مدوّنات الأمثلة.

ملاحظة تقارب. يضم الفهرس في agentlanguages.dev، المقروء في 13 أكتوبر 2026، قائمة من 42 لغة صُمّمت لكي يكتب وكلاء الذكاء الاصطناعي الشيفرة بها، وقد جمعها محرروه في معسكر نحوي ومعسكر تحقق ومعسكر تنسيق. وتظهر في أوصافه لمشاريع أخرى طُوّرت باستقلال عدة خيارات تصميمية في هذه الورقة، مثل العقود المفحوصة آليًا، والسجلات المسلسلة بالتجزئة، وإعادة التشغيل الحتمية، وشكل قانوني واحد لكل برنامج. هذه ملاحظة بأن الخيارات تتكرر. وليست دليلًا على أنها صحيحة، ولا تجري هذه الورقة أي مقارنة مع تلك المشاريع.

4. المحرك: التروس والبوابة والإيصالات

4.1 المحرك شكل

يشغّل RCE البرمجيات بوصفها رسمًا من معالجات صغيرة حتمية. والمعالج الذي لا يستطيع أن يقرر يرفع تصعيدًا. ويجيب محلِّل عن التصعيد مرة واحدة، ويُثبَّت الجواب معالجًا دائمًا، فتعمل الحالة التالية من الشكل نفسه من دون محلِّل. ويستوفي المحرك كل ثوابت الشكل، ويُفحص كل منها باختبار مسمّى في tests/form_laws.rs:

الثابت	ما يفعله المحرك
إعادة التحميل طيّ متحقَّق منه	تقرأ إعادة التحميل السجل حرفيًا، وتعيد حساب كل تجزئة وكل رابط، وتطوي الباقي بـ $\delta$. لا يُعاد ختم أي شيء. والسلسلة المكسورة ترفض التحميل.
ترتيب نبضات خالٍ من الأسماء	تعمل المعالجات بترتيب الرتبة الطوبولوجية، ثم بمفتاح عقدة خالٍ من الأسماء. تُجهَّز المخرجات وتُسلَّم بعد عمل كل المعالجات، كما في دلاليات ASM. وإعادة تسمية كل عقدة تعطي تجزئة الحالة المجهولة نفسها عند كل إدخال.
لا إسقاط صامت	صندوق البريد الممتلئ يحتفظ بالرسالة في طابور مرتّب ويسجّل Backpressure. ومع سعة 1 و10 مهام، تُسجَّل 9 إدخالات Backpressure وتُغلق المهام الـ 10 كلها.
الحمولات في السجل	المدخلات والنبضات ونتائج المعالجات الخارجية والتثبيتات والأعطال كلها إدخالات في السجل. وتجزئة الحالة بعد كل إدخال تطابق طيًّا من محرك فارغ، على 1,000 سجل عشوائي.
ساعة منطقية	تعدّ الحيوية النبضات، لا الزمن الجداري.
تجزئات مستقرة	SHA-256 (خوارزمية التجزئة الآمنة، 256 بت) على JSON قانوني، مع ترتيب المفاتيح عند كل عمق، للإدخالات والحالات والهيئات ومعرّفات القواعد.

4.2 التروس

لا يُجرَّب كل ترس إلا حين لا يجتاز الترس الذي دونه البوابة. وذلك الترتيب تسلسل واحد ثابت.

الترس	الطريقة	النسب
G0 البحث	مكتبة معالجات مشتركة مفهرسة بتجزئة الهيئة SHA-256؛ ولإصلاح الشيفرة، تحديد الموضع في دوال مرتبة	البحث في الشيفرة واسترجاعها [21]
G1 القواعد	قوالب إصلاح حتمية محروسة ومدقِّقات مشتقة من المخطط، يُفحص كل منها لحساسيته للطفرات	PAR وTBar وAVATAR وFixMiner [22, 23, 24, 25]؛ وأدوات تعديل الشيفرة مثل Coccinelle [26]
G2 التركيب	التعداد على قواعد المعالجات النحوية، والمحلّلات، والرسوم الإلكترونية	Sketching وSyGuS وegg [27, 9, 12]
G3 إلى G5 النماذج	نموذج قرار ذو أنواع، ثم نموذج صغير محلي، ثم نموذج بعيد، في الأخير	تسلسلات النماذج [28]

4.3 البوابة

لا يُرقّى مرشح إلا حين يجتاز البوابة. تعيد البوابة تشغيل المدخلات المسجلة للعقدة، وتشغّل المرشح في الظل على عينات جديدة مع حدّ تغطية (قاعدة الثلاثة عند ميزانية خطأ مصرّح بها)، وتفحص مخطط المخرجات، وتشترط شهادة البرهان من القسم 5. ويُسجَّل المرشح المرفوض مع مثاله المضاد.

4.4 الإيصالات

كل ترقية ورفض وتأجيل وتثبيت هو تعديل في سجل لا يُضاف إليه إلا من آخره ومسلسل بـ SHA-256، فالعبث بأي إدخال سابق يكسر السلسلة [29, 30]. وتُسعَّر تكلفة كل معالج من أعداد عمليات المفسِّر بجدول تكاليف المضيف في FGIR، الواجهة الخلفية للشيفرة الأصلية في flowG، وتُوسم est_j. وكل استدعاء للمشرف (foreman) يحمل إيصاله. ويسمّي الإيصال الترس، وطريقة التقدير (basis)، والمرشحين المجرَّبين، وما إذا كان الترس قد حلّ التصعيد. وحقله est_j مطلوب: فهو عدد منتهٍ غير سالب، أو null، ولا يُسمح بـ null إلا حين يقول basis إنه unpriced، كما في استدعاء نموذج بلا رقم للطاقة. والإيصال الذي يغيب عنه الحقل لا يُحلَّل. ولا تُقرأ التكلفة غير المسعَّرة صفرًا أبدًا، فالمجموع على الإيصالات يذكر استدعاءاته المسعَّرة وغير المسعَّرة منفصلة، والتوفير الذي يعتمد على حلّ غير مسعَّر يُذكر بوصفه مجهولًا. وتضيف تشغيلات السلّم عدّاد طاقة للحزمة على عينة فرعية، موسومًا reported_j.

4.5 مترجم الشكل

يأخذ rce form مواصفة وملاءمتها ويُصدر خمسة أهداف من تمثيل وسيط واحد للشكل:

.rce spec + fit
  lower ─► normalize ─► egg e-graph, equality saturation (+ admitted proposals)
  ─► extract (cost = est_j) ─► Form IR (typed relations, regions, rules with SHA-256 ids)
     ├─ Rust crate (pure step, typed state, SHA-256 log and fold, tests)
     │  └─ WASM (the same crate on wasm32-wasip1)
     ├─ Python (standard library only)
     ├─ XState v5 machine
     └─ SCXML document, executed by SCION

يثبّت التمثيل الوسيط سلوكًا واحدًا عند كل طرف عددي: فيضان الأعداد الصحيحة ذات 64 بت مفحوص وهو خطأ ولا يلتف أبدًا؛ والقسمة الصحيحة / تقتطع نحو الصفر ($-7/2=-3$)؛ و% تأخذ إشارة المقسوم ($-3\mathrm{mod}2=-1$)؛ والقسمة على صفر خطأ؛ والأعداد العشرية من نوع IEEE 754 binary64 والنتيجة غير المنتهية خطأ؛ وnull والغياب متمايزان؛ والزمن هو الساعة المنطقية فقط. كل هدف مولَّد. ولا يُكتب أي منها باليد.

معالج العملية أو HTTP أو الإغلاق (closure) ليس له حدّ، فتُترجم نتائجه المسجلة إلى عرّاف (oracle) مسجَّل مفهرس بتجزئة SHA-256 للمُدخل القانوني. ويرفع rce scan DIR --form شيفرة Rust وPython وTypeScript وGo القائمة إلى مخطط الشكل، ويُوسم كل عنصر مرفوع بأنه رفع نحوي.

4.6 المنهج: تقييم المكدس كله، وكل افتراض في الواجهات صريح

البرنامج مكدس من المستويات: الرموز والعبارات؛ والمعالجات؛ والشكل، وهو دالة خطوة واحدة $\delta :S\times E\to S\times O^{\ast }$ على $S={\Sigma }_c\times {\Sigma }_d$ (مناطق التحكم؛ والبيانات: الساعة وعدد المدخلات والعلاقات ذات الأنواع)؛ والسجل، وهو سلسلة تجزئة SHA-256 تسجّل إدخالاتها كل حدث وتجزئة الحالة التي أنتجها وتجزئة الإدخال السابق؛ وإعادات الكتابة التي تحوّل الشكل؛ والركيزة التي تنفّذه. ويقوم كل مستوى على افتراضات عن المستوى الذي تحته. لا يعامل RCE أي مستوى بوصفه ثابتًا. بل يقيّم المكدس كله، ويكتب كل افتراض في الواجهات عبارةً قابلة للفحص، ويفحصه في كل تشغيل.

الحد	الافتراض	الفحص
من المصدر إلى المعالج	المُدخل يستوفي عقد مصدره	فحص العقد عند حدث الإدخال في δ
من المعالج إلى المصبّ	كل مُخرَج Ok يستوفي مخطط المخرجات	برهان المعالج (verify::handler_proof)، كلّي وحتمي بواسطة مقيِّم النواة المفحوص بـ Kani
من السجل إلى الحالة	كل إدخال يحمل تجزئة الحالة التي أنتجها	طيّ النواة، الذي يرفض أول إدخال لا تطابق تجزئته (حزمة Kani fold_rejects_wrong_state)
من إعادة الكتابة إلى الشكل	إعادة الكتابة تحفظ المُخرَج لكل مُدخل	فحص عشوائي، ثم برهان SMT بـ Z3
من البذرة إلى المشرف	المعالج الذي لا يستطيع أن يقرر يصعّد بدل أن يخمّن	المعالجات البذرية تُصدر تصعيدات؛ ولا تُرقّى الحلول إلا عبر مسار الترقية
من الشكل إلى الهدف	كل هدف مُصدَر يحسب δ نفسها	كل هدف يحمل الأثر المرجعي نفسه

الفحص الفاشل يحدد موضع الكسر عند الحد الذي يقع فيه. ويُجرى التصحيح عند ذلك المستوى، ويُمرَّر عبر فحص ذلك الحد، ويُرقّى. وكل مستوى فوق المستوى المصحَّح يرث التصحيح من دون تغيير إضافي، لأن كل مستوى أعلى لا يستهلك المستوى المصحَّح إلا عبر الواجهة التي صار افتراضها مفحوصًا الآن. وهذا هو المعنى الذي تنتقل فيه التصحيحات صعودًا وتتراكم. ويشغّل RCE engine demo هذا في المتصفح على نواة RCE مترجمة إلى WebAssembly: تكسر طبقة Interfaces فيه كل افتراض وتعرض الفحص الذي يكتشفه، وتعرض طبقة Compounding التصحيح وهو ينتقل إلى كل دورة لاحقة.

5. التحقق

5.1 الاختبار التفاضلي عبر خمسة أهداف

يقود tests/form_targets.rs مواصفة حسابية من أحد عشر مؤثرًا بـ 29 حدثًا طرفيًا إضافة إلى 500 قيمة طرفية عشوائية ذات بذرة. وتطبع الأهداف المولَّدة Rust وPython وWASM وXState وSCXML الأثر المرجعي بايتًا ببايت، بما في ذلك الأطراف الحسابية. هذا اختبار تفاضلي على خط McKeeman وCsmith [86]: توافق بين تطبيقات مستقلة على مجموعة مدخلات مذكورة. وليس هذا تحققًا من صحة الترجمة [85] ولا مترجمًا متحقَّقًا منه. فهو يغطي المؤثرات الأحد عشر والأحداث الـ 529 في الاختبار، ولا يقول شيئًا عن المدخلات خارجها. ونتائج Z3 وKani أدناه هي التحقق.

يعرض الشكل التوضيحي 11 الإسقاطات الخمسة لشكل واحد والذهاب والإياب لهدفي مخطط الحالات.

5.2 إعادات كتابة مبرهنة في Z3

لقواعد إعادة الكتابة المتحقَّق منها نسب. يستنتج Ruler قواعد إعادة الكتابة ويفحصها بالإشباع بالمساواة من دون نموذج في الحلقة [87]. ولذلك فإن القواعد الـ 3 المقبولة من أصل 16 قاعدة اقترحها نموذج في القسم 5.5 عبارة عن البوابة، التي رفضت 13، وليست ادعاءً بأن النموذج هو أفضل مصدر للقواعد.

كل إعادة كتابة مدمجة في الرسم الإلكتروني مبرهنة في محلّل Z3 من نوع SMT (قابلية الإرضاء مقابل النظريات) [31] مقابل ترميز خالٍ من المكمّمات لتقييم حدود الشكل وحسابه: القيم كنوع بيانات، ومتجهات بتات من 64 بت مع فيضان مفحوص، وقسمة وباقٍ بإشارة المقسوم، وأعداد عشرية binary64. وإعادة الكتابة التي تغيّر الفيضان أو ترتيب التصعيد أو رسالة لا تحصل على برهان. ولا يدخل تكافؤ مقترح الرسم الإلكتروني إلا مع برهان.

5.3 براهين Kani للنواة

تُفحص نواة المحرك (سلسلة التجزئة، والطيّ، والمواضع الخالية من الأسماء، وتقييم المعالجات) بمدقِّق النماذج Kani للغة Rust [32]. وتقييم المعالجات هو النقطة الثابتة لخطوة غير تكرارية، ويبرهن Kani أن تلك الخطوة كلّية وحتمية لكل باني، بالاستقراء البنيوي. تم التحقق من عشر حزم اختبار بـ Kani 0.67.0، مع 0 فحوص فاشلة من 7,425:

الحزمة	الخاصية
chain_appended_verifies	سلسلة تجزئة مُلحَق بها تجتاز التحقق
chain_detects_tampering	الإدخال المعدَّل يكسر السلسلة
fold_equals_replay	الطيّ يساوي إعادة التشغيل
fold_rejects_wrong_state	الطيّ الذي يخالف الحالة المخزنة يُرفض
position_is_name_independent	مواضع القواعد لا تعتمد على أسماء العقد
reason_tokens_are_name_independent	الأسباب خالية من الأسماء على مستوى الرموز الكاملة
handler_core_leaves	المعالجات الورقية كلّية وحتمية
handler_core_validate	التدقيق كلّي وحتمي
handler_core_pipeline	خطوط المعالجة كلّية وحتمية
handler_core_ifhas	الحرّاس كلّيون وحتميون

5.4 بوابة الترقية على شهادة البرهان

يكتب تشغيل Kani شهادة تُخزَّن تجزئتها في proofs/kani.cert. ويمر المحرك والسجل ومعرّفات القواعد وتقييم المعالجات عبر النواة المبرهنة، والترقية تشترط الشهادة.

5.5 النموذج مقترِحًا خلف الفحص

يجوز للنموذج أن يقترح تكافؤات. ولا يجوز له أن يقبلها. مع نموذج برمجة محلي من 1.5 مليار معامل (Qwen2.5-Coder-1.5B تحت llama.cpp) على مواصفة العرض التوضيحي، قدّم المقترِح 16 تكافؤًا. وقبل الفحص 3 منها، بتجارب عشوائية وبرهان Z3، ورفض 13. وكان لمقترِح حتمي من 87 متطابقة مألوفة، 77 حسابية و10 بنيوية، 9 متطابقات مقبولة، كلها بنيوية، و78 مرفوضة: كل متطابقة حسابية، بسبب ترتيب الأعطال أو قيم غير عددية أو الفيضان، وإعادة كتابة بنيوية واحدة، const-absorbs-pipe، كانت ستُسقط بادئة مصعِّدة (اختبار المحرك tests/form_proposers.rs).

5.6 التوافق مع الشيفرة القائمة

يقرأ الرفع آلة الطلبات نفسها من تجهيزات اختبار بـ Rust وPython وTypeScript وGo، ويشغّل الشيفرة الأصلية على 40 متتالية ذات بذرة من 30 استدعاءً، ويتوافق في كل الاستدعاءات الـ 1,200 لكل لغة. وأعاد مقياس مرجعي مجمّد، سُجّل مسبقًا قبل أي نتيجة، التعبير عن ثلاثة برامج قائمة للتواصل البيعي في صورة أشكال. وتتوافق الأشكال مع الشيفرة الأصلية في 4,500 من 4,500 مُدخل مسجل، ويخفض الاستخلاص est_j في كل منها (مثلًا من $1.69\times 10^{-8}$ J إلى $1.49\times 10^{-8}$ J).

6. الرفع: الدخول إلى المنظومة من لغات أخرى

الرفع هو باب المنظومة للشيفرة المكتوبة في مكان آخر. وهو بناء، يُصنع لكل لغة من أدوات تملكها كل لغة أصلًا: قواعد نحوية صورية، ومحلّل نحوي مثل tree-sitter ينتج الشجرة النحوية، والشجرة النحوية المجردة، والرموز التي تحلّها أدوات خوادم اللغة (Language Server Protocol). ويبني rce scan DIR --form الشكل من تلك الشجرة للغات Rust وPython وTypeScript وGo (§4.5، §5.6). والبرنامج المرفوع يحمل أعطال مصدره، ولذلك يشمل الرفع الإصلاح، الذي يُقاس أدناه على مدوّنات علنية للأخطاء البرمجية مع إعطاء الموضع. وداخل المنظومة لا يمكن كتابة هذه الأعطال.

6.0 سلّم الإصلاح على الشيفرة المرفوعة

تُقاس مهمة البرمجة هنا بـ بتات النية التي تحتاجها: البتات التي يجب تقديمها من خارج ما يملكه المحرك أصلًا (البرنامج المحيط بالتعديل، والمكتبات، والاختبارات، وفهرس الإصلاحات المعروفة). وإذا كتبنا $H_{task}$ للبتات التي تثبّت المصنوع المستهدف و$H_{corpus}$ للبتات التي تثبّتها المدوّنة أصلًا، فإن البتات المقدَّمة هي $I=H_{task}-H_{corpus}$. والترس الذي يرتّب التعديل الصحيح في الرتبة $r$ بين مرشحيه قد قدّم ${\log }_{2}r$ بت من البحث، والبوابة تقدّم الباقي. ويرتّب السلّم المهام بحجم التعديل، وهو بديل موضوعي عن $I$: رمز واحد (L0)، وعبارة واحدة (L1)، وكتلة تغيير واحدة (L2)، وعدة كتل في ملف واحد (L3)، وعدة ملفات (L4)، ودالة من مواصفة أو اختبارات (L5)، وتغيير على مستوى البلاغ (L6)، وبرنامج من مواصفة (L7). وسُجّلت الدرجات والمدوّنات والتقسيمات والفرضيات مسبقًا قبل التشغيلات الكاملة؛ والملفات في المستودع العلني.

الدرجة	مدوّنة الاختبار المحجوزة	N	المحلولة	المعدل	فترة Wilson بنسبة 95%	الوسيط لبتات البحث	استدعاءات النموذج
L0 رمز واحد	طفرات على نمط PIT [109] لـ 9 مستودعات حقيقية عند التزامات مثبّتة (Java: commons-math وcommons-collections وjsoup وjoda-time وgson؛ Python: click وattrs وpydantic وsympy)	520,821	520,541	0.9995	من 0.9994 إلى 0.9995	2.3	0
L0 رمز واحد، مستودعات لم يُضبط عليها أبدًا	commons-text وcommons-io وmore-itertools وhttpx	23,015	23,015	1.0000	من 0.9998 إلى 1.0000	2.0	0
L1 عبارة واحدة، Java	إصلاحات الكتلة الواحدة في ManySStuBs4J 2.0 [107]	24,072	9,288	0.386	من 0.380 إلى 0.392	3.5	0
L1 عبارة واحدة، Java، الملف كاملًا	ManySStuBs4J 2.0 [107]، ملف الالتزام الأب مع فهارس دوال المشروع وحرّاسه	21,320	13,586	0.637	من 0.631 إلى 0.644	4.8	0
L1 عبارة واحدة، Python	TSSB-3M v1.0.0، الشريحتان 14 و15 [108]	157,089	27,266	0.174	من 0.172 إلى 0.175	4.8	0

يرسم الشكل التوضيحي 14 صفوف الجدول مع فتراتها.

تُقاس الدرجات من L2 إلى L4 على مجموعة Defects4J المحجوزة من 288 خطأ (القسم 8.1). وتتبع الدرجات من L5 إلى L7 بروتوكولات القسم 8.2. ويلي ذلك المنهج والبوابة والطاقة لكل صف.

قضية مفتوحة: خط الأساس لمعدل الرمز الواحد. تقيس صفوف L0 عدد المرات التي يعيد فيها جوار الرمز الواحد المرتب بالأسبقية طفرةً من رمز واحد إلى أصلها. فإذا بُني الجوار من جداول مؤثرات الطفرة نفسها التي أنتجت الطفرات، فإن المعدل المرتفع يعكس جزئيًا هذا التداخل لا القدرة على إصلاح أعطال تنشأ في الممارسة. وتستشهد الورقة بخطر الاقتران هذا ولا تعطي له رقمًا. وخط الأساس الذي يبيّن مقدار ما يفسّره هذا التداخل من المعدل هو بحث بسيط يعكس المؤثرات، يُشغَّل على الطفرات نفسها. ولم يُشغَّل خط الأساس هذا، فلا يُعطى هنا أي رقم، ويبقى معدل الرمز الواحد عرضة لهذا الاعتراض.

تُقرأ المعدلات بوصفها بتات نية. عند L0 تكون البتات الناقصة كلها تقريبًا على السطر، ويقدّمها جوار الرمز الواحد المرتب بالأسبقية بوسيط قدره 2.3 بت. وفي صف L1 الخاص بالكتلة فقط لا يرى المحرك إلا الكتلة ذات الأسطر الـ 7. فيغلق الفئات التي تقع بتاتها داخل الكتلة (Java: تغيير المؤثر 91%، وتبديل القيمة المنطقية الحرفية 84%، وتبديل الوسائط 82%؛ Python: تغيير القيمة المنطقية الحرفية 98.8%، وتبديل الوسائط 99.4%) ويترك مفتوحةً تلك التي تقع بتاتها خارجها: أسماء الدوال (22%) والمعرّفات (37%) تحتاج إلى الملف وأنواعه، والشروط المضافة الجديدة (من 3% إلى 7%) وإعادات كتابة العبارة كاملة (Python، 1.2% من فئة تمثل 34% من المدوّنة) نية جديدة. والنية الجديدة هي ما يقدّمه مزوِّد (مواصفة، أو اختبار، أو إنسان، أو نموذج محلي) مرة واحدة، وبعدها تكون الملاءمة في الفهرس.

المنهج. تُخلط كل مدوّنة ببذرة ثابتة. وتشكّل أول 2,000 موضع من كل خلط، ولـ L0 ثلاثة مستودعات كاملة (commons-lang وrequests وflask)، تقسيم التطوير، الذي يجوز ضبط التروس عليه؛ ولا تُذكر نتائج التطوير. وكل مهمة متبقية في تقسيم الاختبار. وقبل تشغيل الاختبار يُلتزم بالمحرك وتُسجَّل تجزئة ملفه التنفيذي، ولا يتغير أي ترس أثناء التشغيل. وكل صف في هذا القسم نتيجة محرك مجمّد على مهام الاختبار فقط، مع 0 استدعاءات للنموذج. والتسجيل المسبق (PREREG.json) وصفوف كل مهمة وبرنامج التقرير موجودة في المستودع العلني.

البوابة. عند L0 وL1 يكون الموضع معطى والبوابة هي تطابق الرموز: يجب أن يساوي السطر أو العبارة المصلَحة ما كتبه المطوّر، رمزًا برمز. وهذا أشد من اجتياز الاختبارات، لأن الرقعة قد تجتاز مجموعة اختبارات ضعيفة وتبقى خاطئة. فقد وجد Qi وزملاؤه أن معظم الرقع التي أبلغ GenProg أنها إصلاحات كانت معقولة لكنها غير صحيحة [92]؛ والإفراط في الملاءمة للاختبارات موثق في الإصلاح القائم على البحث والقائم على الدلاليات [93, 94] وعولج باختبارات مولَّدة [95]؛ والأدوات تحصل على درجات أعلى على المقياس المرجعي الذي ضُبطت عليه [96]؛ وتحديد موضع العطل يحيّز المقارنات [97]. ويزيل تطابق الرموز فجوة المعقولية على هذه الدرجات، وإعطاء الموضع يزيل حدّ تحديد الموضع، فيقيس المعدل تروس الإصلاح وحدها. وتستخدم L2 وما فوقها الاختبارات بوابةً وتذكر أعداد الرقع المعقولة والصحيحة كلًّا على حدة (القسم 8.1).

6.1 L0: أعطال الرمز الواحد

مدوّنة L0 هي كل طفرة على نمط PIT [109] لها رمز بديل صالح في تسعة مستودعات حقيقية عند التزامات مثبّتة، خمسة بـ Java وأربعة بـ Python: 520,821 مهمة اختبار من أصل 547,448. ويستعيد المحرك (الالتزام 65571d0، الترسان G0-T وG1-J) 520,541 منها، بمعدل 0.9995 (فترة Wilson بنسبة 95% من 0.9994 إلى 0.9995) بوسيط قدره 2.3 بت بحث. ومن الـ 280 غير المحلولة، 108 أرقام مطفَّرة داخل قيم حرفية عشرية و2 داخل قيم حرفية لمجموعات Python. ويُختبر ترس للقيم الحرفية العشرية (G0-F، الالتزام ecfe5a1) على أربعة مستودعات لم تُستخدم للضبط أبدًا (commons-text وcommons-io وmore-itertools وhttpx): 23,015 من 23,015 مهمة، 1.0000 (من 0.9998 إلى 1.0000)، بوسيط قدره 2.0 بت بحث. والطفرات بديل عن أعطال الرمز الواحد الحقيقية التي وجد Just وزملاؤه أنها مقترنة بالأعطال الحقيقية [110].

6.2 L1: أخطاء العبارة الواحدة من تواريخ حقيقية

تستخدم L1 مجموعتي بيانات علنيتين لإصلاحات حقيقية لأخطاء في عبارة واحدة، مستخرجة من تواريخ المشاريع مفتوحة المصدر. تعطي ManySStuBs4J 2.0 [107] ‏24,072 مهمة اختبار بـ Java؛ ويحلّ المحرك (الالتزام f2701b7) 9,288 منها، بمعدل 0.386 (من 0.380 إلى 0.392). وتعطي TSSB-3M v1.0.0 [108] ‏157,089 مهمة اختبار بـ Python من الشريحتين 14 و15؛ ويحلّ المحرك نفسه 27,266 منها، بمعدل 0.174 (من 0.172 إلى 0.175). ولا يتلقى المحرك إلا الكتلة ذات الأسطر الـ 7، فمعدل Java ذلك نتيجة للكتلة فقط. وحين يُعطى الملف كاملًا عند الالتزام الأب، مع فهارس دوال المشروع وشروط حراسته والتروس الخاصة بتغيير أسماء الدوال وإضافة الوسائط وشروط الحراسة والاستثناءات المرمية والمعدِّلات (الالتزام 62fb7a0، وبادئة sha256 للملف التنفيذي 3682c6515acdf722، مسجل مسبقًا قبل التشغيل)، يحلّ المحرك 13,586 من 21,320 مهمة اختبار بـ Java أمكن تحديد ملفها وعبارة الخطأ فيها، بمعدل 0.637 (من 0.631 إلى 0.644). وبحسب الفئة يغلق تغيير المؤثرات (95.9%)، وتغيير المعاملات (92.1%)، والمستدعين الخاطئين (87.9%)، وتبديل القيم المنطقية الحرفية (88.4%)، والوسائط المحذوفة (85.1%)، وتبديل الوسائط (83.3%)؛ ويبلغ تغيير أسماء الدوال 61.4% وإضافة الوسائط 51.4%، وتبقى الشروط الجديدة أو المضيَّقة (43.5% و51.7%) النيةَ المفتوحة الرئيسية. والجداول الكاملة لكل طبقة موجودة في المستودع. وليس لمجموعتي البيانات هاتين لوحة صدارة إصلاح منشورة تحت هذه البوابة (الكتلة فقط، وتطابق الرموز، والموضع معطى)، فلا يوضع بجانبهما رقم لإصلاح متعلَّم؛ أما Defects4J، التي لها لوحة كهذه، فتُقارن بـ TBar في القسم 8.1.

6.3 الطاقة

يحمل كل صف est_j، وهو تقدير يساوي ثواني المعالج مضروبة في 10 W: ‏0.40 J لكل مهمة محلولة عند L0، و0.13 على المستودعات الجديدة، و0.10 على ManySStuBs4J، و0.27 على TSSB-3M. وقُرئت عينة فرعية على RAPL [105]، وهو عدّاد الحزمة على شريحة المعالج، على حاسوب محمول بنظام Linux بمعالج Intel i9-13900H (اسم المضيف jetson-hub؛ وليس NVIDIA Jetson). وعملت حزمة الاختبار على 4 معالجات مثبّتة، وreported_j هو فرق الحزمة على التشغيل كله، بما في ذلك مشغّل Python، مطروحًا منه قدرة الخمول من عينة مدتها 10 ثوانٍ أُخذت قبله مباشرة، مضروبة في مدة التشغيل. وكانت مشغّلات التكامل المستمر تعمل، فكان الخمول من 40 W إلى 44 W، وعدم اليقين نحو ±1 W مضروبًا في المدة، أي ±10 J على هذه المجاميع.

العينة الفرعية (تقسيم الاختبار)	المهام	المحلولة	الجول الخام	reported_j	reported_j لكل مهمة محلولة	الثواني
L0، طفرات gson (ذات بذرة، أول 3,000)	3,000	3,000	648.3	167.5	0.056	11.8
L1، مواضع ManySStuBs4J من 2,000 إلى 3,999	2,000	690	377.2	17.9	0.026	8.2

تبني العينة الفرعية لـ L1 فهرس مشروعها من مهامها الـ 2,000 فقط، فيكون معدل حلها (34.5%) دون معدل التشغيل الكامل. وmeasured_j، أي عدّاد جداري على خط تغذية مسمّى، فارغ في كل صف؛ وبروتوكوله في القسم 8.3.

7. أدلة إعادة الاستخدام

يقوم موضع RCE على محور إعادة الاستخدام على حقيقة هندسية: الشيفرة يُعاد استخدامها على كل مقياس. وكل طريقة أدناه تقيس ذلك بطريقة مختلفة.

الطريقة	المصدر	النتيجة
تخطيط النسخ المستنسخة على مستوى الملفات	DéjàVu، Lopes et al. 2017 [33]	من بين 428 مليون ملف في 4.5 مليون مشروع غير متفرع على GitHub، 85 مليونًا فريدة: “70% of the code on GitHub consists of clones of previously created files”، أي أن 70% من الشيفرة على GitHub نسخ مستنسخة من ملفات أُنشئت سابقًا. وفي JavaScript تبلغ نسبة الملفات المتمايزة 6%.
التكرار على مستوى الأسطر	Gabel وSu 2010 [34]	مقابل 420 مليون سطر، “between 50% and 100% of each project is redundant”، أي أن ما بين 50% و100% من كل مشروع مكرر، عند نحو سطر واحد.
نماذج اللغة الإحصائية	Hindle et al. 2012 [35]	الشيفرة “very repetitive, and in fact even more so than natural languages”، أي شديدة التكرار بل أشد من اللغات الطبيعية.
إزالة التكرار التقريبي من المدوّنات	The Stack [36]	تزيل إزالة التكرار التقريبي 54.7% من The Stack v1 (من 6.4 TB إلى 2.9 TB) و52.4% من v2 (من 67.5 TB إلى 32.1 TB).
حفظ الأرشيف كاملًا	Software Heritage [129, 130]	30.3 مليار محتوى ملف فريد من 448 مليون أصل (عدّادات الأرشيف، مقروءة في 13 أكتوبر 2026)، يُخزَّن كل منها مرة واحدة بتجزئة بايتاته.
أنماط الإصلاح المستخرجة	PAR وTBar [22, 23]	وجد PAR “several common fix patterns”، أي عدة أنماط إصلاح شائعة، في أكثر من 60,000 رقعة بشرية. وتصلح فئات الأنماط الـ 15 في TBar ‏43 خطأ من Defects4J إصلاحًا صحيحًا في خط المعالجة القياسي، و74 من 101 مع تحديد مثالي لموضع العطل، من دون تعلّم. وهذه أرقام كما قُرئت من [23]؛ ولم يُعَد هنا التحقق من معنى الـ 101 (رقع معقولة أم أخطاء جرت محاولتها) مقابل تلك الورقة، فلتُعامل النسبة على أنها غير مؤكدة.
مهام عابرة للغات	Rosetta Code [131]	1,360 مهمة (و421 مهمة مسودة)، كل منها مفهوم واحد مطبَّق عبر كثير من 1,009 لغة معروفة.

كل صف مُدخل إلى المحرك. فالنسخ المستنسخة وإزالة التكرار تقول إن الملاءمة موجودة عادة، وذلك هو G0. والإصلاحات المتكررة تقول إن التكييف في معظمه فهرس صغير من إعادات الكتابة المحروسة، وذلك هو G1. والتكرار على مستوى الأسطر يقلّص فضاء البحث لـ G2. وتقيسه المنظومة على كل ملاءمة مرقّاة (القسم 2.3)، ويقيسه سلّم الإصلاح على الشيفرة المرفوعة على نطاق واسع على تقسيمات محجوزة (القسم 6). وهناك تحذيران يشحذان القراءة. فالنسخ المكررة تضخّم درجات الاسترجاع والنماذج ما لم تُزل [104]. والأسطر المعيبة أقل طبيعية من الأسطر المصلَحة [45]، فالخطأ نفسه هو الحالة التي يكون البحث أقل قدرة على التنبؤ بها؛ وهيئة الإصلاح، لا السطر المعيب، هي ما يجب أن يعتمد عليه G0 وG1. وخط استخراج القواعد الذي يفعل ذلك على نطاق واسع، من بحث التوليد والتحقق في GenProg [88] ونموذج الصحة المتعلَّم في Prophet [89] إلى Getafix في Facebook [90] والإصلاح الخالي من النماذج لمخالفات التحليل الساكن في Sorald [91]، يشتق القوالب من تاريخ منفصل ويذكر الدقة على الحالات غير المرئية [98]. وذلك هو المعيار الذي يتبنّاه القسم 8.4.

8. بروتوكولات القياس لما يأتي بعد ذلك

يُثبَّت كل بروتوكول قبل تشغيله: يُلتزم بالتسجيل المسبق، وتُسجَّل البذور والتزام المحلِّل، ويُحتفظ بكل مصنوع. البوابة أولًا، والجول ثانيًا، والوسوم دائمًا.

8.1 Defects4J

تضم Defects4J ‏854 خطأ حقيقيًا نشطًا بـ Java، لكل منها اختبارات تعيد إنتاجه [37].

1. التطوير على مجموعة جزئية من 100 خطأ، دون اتصال، عبر defects4j checkout؛ وذكر النتائج المحجوزة فقط، على مجموعة منفصلة من 288 خطأ مجمّدة قبل التشغيل (FROZEN-heldout-v1).
2. تشغيل G0، ثم G1، ثم G2، ثم نموذج محلي في الأخير. وتسجيل الترس الذي أغلق كل خطأ.
3. البوابة: تجتاز الاختبارات المحفِّزة والمجموعة الكاملة. وتُذكر أعداد الرقع المعقولة والصحيحة كلًّا على حدة؛ والصحيحة تعني المكافئة لرقعة المطوّر عند المراجعة.
4. ذكر استدعاءات النموذج لكل إصلاح صحيح والجول لكل إصلاح صحيح، موسومة.
5. نقاط مرجعية: إصلاحات TBar الصحيحة البالغة 43، و74 من 101 تحت تحديد مثالي للموضع (أرقام كما قُرئت من [23]، ولم يُعَد هنا التحقق من المقام). هذا القسم بروتوكول. ولا تعرض هذه الورقة أي نتيجة لهذا المحرك على Defects4J.
6. فحص التلوث: وسم كل خطأ يظهر إصلاحه حرفيًا في فهرس G0، والذكر مع الأخطاء الموسومة ومن دونها.

8.2 SWE-bench Lite، دون اتصال

SWE-bench Lite مجموعة جزئية من 300 مهمة من بلاغات GitHub حقيقية تُحسم باختبارات مخفية [38].

1. استخدام حزمة Docker الرسمية من دون شبكة.
2. التشغيل الأول: G0 وG1 فقط، وصفر استدعاءات للنموذج. هذه أرضية الحل من دون نموذج.
3. التشغيل الثاني: إضافة نموذج محلي بوصفه الترس الأخير.
4. ذكر معدل الحسم، واستدعاءات النموذج لكل مهمة محسومة، والجول لكل مهمة محسومة، موسومة.
5. فحص التلوث كما في 8.1. وجد SWE-Bench+ أن 32.67% من الرقع الناجحة كان حلها موجودًا في نص البلاغ [39].

8.3 عدّاد جداري

1. تركيب عدّاد جداري أو عدّاد تحويلي على مصدر تغذية المضيف، يسجّل بمعدل مذكور مع مزامنة ساعته مع سجل التشغيل.
2. آلة خاملة: إيقاف مشغّلات التكامل المستمر وعمليات البناء الأخرى، وفحص بوابة نافذة الهدوء قبل كل كتلة وتسجيلها.
3. طرح خط أساس مقيس للخمول، وذكر الطريقة.
4. ملء measured_j من العدّاد وحده. وذكر reported_j (RAPL) وest_j بجانبه في أعمدة منفصلة. وعدم الجمع عبر الوسوم أبدًا.
5. تكرار العينات الفرعية لـ RAPL من القسم 6.3 تحت العدّاد، ثم مجموعة Defects4J المحجوزة.

8.4 تشغيل محجوز مع تجميد التروس

هذا منهج القسم 6، ممدودًا إلى مدوّنات جديدة.

1. تجميد G0 وG1 وG2 عند التزام موسوم، وتسجيل تجزئة الملف التنفيذي، ونشر مجموعة القواعد مع طوابع زمن تأليفها.
2. سحب شريحة محجوزة منفصلة: نسخ Rust وPython من Multi-SWE-bench [102] وBugsInPy [103]، بعد إزالة تكرارها مقابل فهرس G0 [104].
3. التسجيل المسبق للشريحة والبذور والفرضيات قبل التشغيل الأول.
4. ذكر أعداد المحسومة والمعقولة والمتطابقة بايتًا ببايت كلًّا على حدة، مع فترة 95% لكل منها.

8.5 خطوط الأساس في الجدول نفسه

1. خالٍ من النماذج: cargo fix وclippy [106]، وSorald أو منفذ لـ TBar [91].
2. نموذج رخيص: Agentless مع نموذج محلي [99].
3. نموذج بعيد: وكيل مع نموذج رائد، تُقدَّر طاقته من إفصاحات المزوِّد وتُوسم est_j.
4. ذكر تكلفة النجاح (cost-of-pass) [101] بالجول وبالدولار لكل صف، مع ضبط التكلفة كما يشترط Kapoor وزملاؤه [100].

8.6 تقارب استدعاءات النموذج عند N كبير

الترقية هي الآلية التي يغادر بها النموذج الحلقة: يُدفع للمحلِّل مرة واحدة مقابل حالة جديدة، وتقبل البوابة الملاءمة معالجًا، وكل حالة لاحقة من الشكل نفسه تُغلق في G0 أو G1 (القسم 4.2). والتقارب هو الادعاء بأن استدعاءات النموذج لكل دورة تنخفض إلى الصفر على مواصفة ثابتة تحت حركة مرور حية. ويُقاس على النحو الآتي.

1. سحب 1,000 مواصفة على الأقل من مستودعات علنية، مقسّمة إلى طبقات بحسب اللغة والحجم، وتجميد المحرك والمحلِّل قبل الدورة الأولى.
2. إعادة تشغيل حركة مرور إنتاجية مسجلة، 10,000 حدث على الأقل لكل مواصفة، في دورات ذات حجم ثابت.
3. التسجيل لكل دورة: التصعيدات الجديدة، واستدعاءات النموذج، والترقيات، والتأجيلات، والجول لكل مهمة مغلقة، كل منها موسوم (est_j، reported_j، measured_j).
4. نقطة النهاية الأولية: حصة المواصفات التي تبلغ دورة بصفر استدعاءات للنموذج خلال 20 دورة، مع فترة Wilson بنسبة 95%. والثانوية: استدعاءات النموذج لكل مهمة مغلقة بحسب الدورة، ودورة آخر استدعاء للنموذج.
5. ذكر المواصفات التي لا تتقارب أبدًا مع سببها (مُدخل عالق، أو تبعية مفقودة، أو نية جديدة)، وتشغيل تأجيل المُدخل العالق بوصفه ذراعًا مسجلة مسبقًا.

القضية 8 (الاقتراب من الأرضية). كلما نمت تغطية G0 وG1، اقتربت الطاقة بالجول لكل مهمة محلولة من الأرضية الذهبية لتطبيق إصلاح معروف وتشغيل الاختبارات. وتختبر ذلك درجات السلّم ومجموعة Defects4J المحجوزة تحت العدّاد الجداري.

8.7 تغطية الرفع عبر اللغات

يُقاس الرفع أثناء بنائه. للغة $L$، يُعدّ البرنامج مرفوعًا حين يجتاز ${\pi }_L({\lambda }_L(p))$ اختبارات البرنامج نفسه ويعيد تشغيل آثاره المسجلة بايتًا ببايت، وحين يكون لـ ${\lambda }_L({\pi }_L({\lambda }_L(p)))$ تجزئة الهيئة نفسها التي لـ ${\lambda }_L(p)$. والعينة 10,000 برنامج على الأقل لكل لغة لعشر لغات على الأقل، مسحوبة ببذرة ثابتة من مدوّنات علنية مثبّتة، مع تجميد الرافع وتسجيل تجزئة ملفه التنفيذي قبل كل تشغيل، و0 استدعاءات للنموذج. ويذكر كل تشغيل الحصة المرفوعة مع فترة Wilson بنسبة 95%، وكل بنية لم تُرفع بعد بند عمل لرافع تلك اللغة، يُبنى ويُجمَّد قبل التشغيل التالي. والهدف كل برنامج بكل لغة.

9. معايير الدحض

مثبّتة قبل التشغيلات التي تختبرها.

المعرّف	الملاحظة	ما تدحضه
RCE-F0	في تشغيل مسجل مسبقًا من 10,000 شكل على الأقل، يطبع أي إسقاط أثرًا يختلف عن الأثر المرجعي للشكل، أو يُقبل أي مُدخل معيب	الادعاء بأن الإسقاطات أمينة وأن البوابة ترفض عند الدخول
RCE-F1	على الشريحة المحجوزة، تحسم G0 إلى G2 مع قواعد مجمّدة أقل من 10% من المهام مع 0 استدعاءات للنموذج	الادعاء بأن معظم الملاءمات موجودة أصلًا للإصلاح على هذا المقياس
RCE-F2	الرقع المتطابقة بايتًا ببايت أو المكافئة أقل من نصف المهام المحجوزة المحسومة	قراءة البوابة على أنها أكثر من معقولية في المهام المغطاة
RCE-F3	تحت العدّاد الجداري، يتجاوز إجمالي الجول لكل مهمة محلولة لمحلِّل RCE نظيره لدى أرخص خط أساس من النماذج على المهام التي يحلّها كلاهما	الادعاء بطاقة أقل لكل مهمة محلولة في المهام المغطاة
RCE-F4	في بروتوكول التقارب في القسم 8.6، يبلغ أقل من نصف المواصفات التي ليس فيها مُدخل عالق دورةً بصفر استدعاءات للنموذج خلال 20 دورة	إخراج النموذج من الحلقة بالترجمة

10. العمل المتبقي لإنجازه

لكل بند بروتوكول مسمّى.

1. بناء الرفع وقياسه عبر عشر لغات على الأقل تحت بروتوكول القسم 8.7.
2. ذراع المواصفات: مواصفات على نمط MBPP وHumanEval مؤلَّفة بوصفها أشكالًا ومُصدَرة إلى كل هدف.
3. نتائج محجوزة على L2 إلى L4، أي مجموعة Defects4J من 288 خطأ (القسم 8.1)، وعلى L5 إلى L7 (القسم 8.2).
4. خطوط الأساس في جدول واحد، وتكلفة النجاح بالجول وبالدولار (القسم 8.5).
5. سلسلة measured_j: عدّاد جداري على مضيف خامل، بـ 10 تكرارات على الأقل، والإجمالي والصافي جنبًا إلى جنب (القسم 8.3).
6. نشر مسح اللغات الـ 626 مع منهجه (الشكل التوضيحي 1).
7. مدوّنات محجوزة جديدة مع تجميد التروس: Multi-SWE-bench وBugsInPy (القسم 8.4).
8. تقارب استدعاءات النموذج عبر 1,000 مواصفة على الأقل (القسم 8.6).

11. الخاتمة

RCE منظومة شيفرة أصلية. يُؤلَّف البرنامج مرة واحدة، انطلاقًا من النية، بوصفه شكلًا: ترميز بلا فقد للحالة والأحداث والانتقالات النقية، وكل لغة هدف إسقاط أمين له. لا يمكن كتابة الحالات غير الصالحة، وتُرفض المدخلات المعيبة عند الدخول، فلا يمكن لبرنامج داخل المنظومة أن ينحرف عن نيته، ولا يحتاج إلى مقارنة فروق أو تتبع أخطاء بعد وقوعها. وكل ملاءمة تجتاز البوابة تُخزَّن ويُعاد استخدامها، وتتراكم المنظومة تحت بوابة صحتها رتيبة. وعلى 10,000 شكل مسجل مسبقًا مع محرك مجمّد و0 استدعاءات للنموذج، يعود كل شكل بالذهاب والإياب إلى بايتات متطابقة، وكل إسقاط حتمي، وكل مُدخل معيب وكل مواصفة معيبة تُرفض عند الدخول، ويعيد إسقاط Python تشغيل الأثر المرجعي في 9,999 منها. وتدخل الشيفرة من لغات أخرى بالرفع، وهو بناء من القواعد النحوية لكل لغة إلى شجرتها النحوية إلى الشكل؛ وعلى الشيفرة المرفوعة تستعيد تروس الإصلاح 99.95% من 520,821 عطلًا في رمز واحد و63.7% من 21,320 خطأ في عبارة واحدة بـ Java. ويذكر القسمان 3.6 و8.7 قضايا الشمولية وكيف يُقاس بناؤها.

المراجع

[1] C. E. Shannon, “Prediction and Entropy of Printed English,” Bell System Technical Journal 30(1), 1951. doi:10.1002/j.1538-7305.1951.tb01366.x

[2] Y. Gurevich, “Sequential Abstract State Machines Capture Sequential Algorithms,” ACM Transactions on Computational Logic 1(1), 2000. doi:10.1145/343369.343384

[3] A. Blass and Y. Gurevich, “Abstract State Machines Capture Parallel Algorithms,” ACM Transactions on Computational Logic, 2003. doi:10.1145/937555.937561

[4] N. Dershowitz and Y. Gurevich, “A Natural Axiomatization of Computability and Proof of Church’s Thesis,” Bulletin of Symbolic Logic, 2008. doi:10.2178/bsl/1231081370

[5] E. F. Codd, “A Relational Model of Data for Large Shared Data Banks,” Communications of the ACM, 1970. doi:10.1145/362384.362685

[6] G. H. Mealy, “A Method for Synthesizing Sequential Circuits,” Bell System Technical Journal, 1955. doi:10.1002/j.1538-7305.1955.tb03788.x

[7] E. F. Moore, “Gedanken-Experiments on Sequential Machines,” Automata Studies, 1956. doi:10.1515/9781400882618-006

[8] K. Kang et al., “Feature-Oriented Domain Analysis (FODA) Feasibility Study,” CMU/SEI-90-TR-021, 1990.

[9] R. Alur et al., “Syntax-Guided Synthesis,” FMCAD 2013. doi:10.1109/FMCAD.2013.6679385

[10] D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, 1987. doi:10.1016/0167-6423(87)90035-9

[11] R. Tate, M. Stepp, Z. Tatlock and S. Lerner, “Equality Saturation,” POPL 2009. doi:10.1145/1480881.1480915

[12] M. Willsey et al., “egg: Fast and Extensible Equality Saturation,” POPL 2021. doi:10.1145/3434304

[13] B. Moseley and P. Marks, “Out of the Tar Pit,” 2006.

[14] M. Fowler, “Event Sourcing,” 2005. https://martinfowler.com/eaaDev/EventSourcing.html

[15] P. Alvaro et al., “Dedalus: Datalog in Time and Space,” LNCS 2011. doi:10.1007/978-3-642-24206-9_16

[16] A. M. Turing, “On Computable Numbers,” Proceedings of the London Mathematical Society, 1937. doi:10.1112/plms/s2-42.1.230

[17] A. Church, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics, 1936. doi:10.2307/2371045

[18] P. Wadler, “Propositions as Types,” Communications of the ACM, 2015. doi:10.1145/2699407

[19] J. M. Hellerstein and P. Alvaro, “Keeping CALM,” Communications of the ACM, 2020. doi:10.1145/3369736

[20] G. Kahn, “The Semantics of a Simple Language for Parallel Programming,” IFIP 1974, pp. 471 to 475.

[21] H. Husain et al., “CodeSearchNet Challenge,” 2019. arXiv:1909.09436

[22] D. Kim, J. Nam, J. Song and S. Kim, “Automatic Patch Generation Learned from Human-Written Patches” (PAR), ICSE 2013. doi:10.1109/ICSE.2013.6606626

[23] K. Liu et al., “TBar: Revisiting Template-based Automated Program Repair,” ISSTA 2019. arXiv:1903.08409

[24] K. Liu et al., “AVATAR: Fixing Semantic Bugs with Fix Patterns of Static Analysis Violations,” SANER 2019. arXiv:1812.07270

[25] A. Koyuncu et al., “FixMiner: Mining Relevant Fix Patterns for Automated Program Repair,” 2018. arXiv:1810.01791

[26] Y. Padioleau et al., “Documenting and Automating Collateral Evolutions in Linux Device Drivers” (Coccinelle), EuroSys 2008. doi:10.1145/1352592.1352618

[27] A. Solar-Lezama et al., “Combinatorial Sketching for Finite Programs,” ASPLOS 2006. doi:10.1145/1168857.1168907

[28] L. Chen, M. Zaharia and J. Zou, “FrugalGPT,” 2023. arXiv:2305.05176

[29] S. Haber and W. S. Stornetta, “How to Time-Stamp a Digital Document,” Journal of Cryptology, 1991. doi:10.1007/BF00196791

[30] S. A. Crosby and D. S. Wallach, “Efficient Data Structures for Tamper-Evident Logging,” USENIX Security 2009.

[31] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” TACAS 2008. doi:10.1007/978-3-540-78800-3_24

[32] Kani Rust Verifier. https://github.com/model-checking/kani

[33] C. V. Lopes et al., “DéjàVu: A Map of Code Duplicates on GitHub,” OOPSLA 2017. doi:10.1145/3133908

[34] M. Gabel and Z. Su, “A Study of the Uniqueness of Source Code,” FSE 2010. doi:10.1145/1882291.1882315

[35] A. Hindle et al., “On the Naturalness of Software,” ICSE 2012. doi:10.1109/ICSE.2012.6227135

[36] D. Kocetkov et al., “The Stack: 3 TB of Permissively Licensed Source Code,” 2022. arXiv:2211.15533; The Stack v2 dataset card, https://huggingface.co/datasets/bigcode/the-stack-v2

[37] R. Just, D. Jalali and M. D. Ernst, “Defects4J: A Database of Existing Faults to Enable Controlled Testing Studies for Java Programs,” ISSTA 2014. doi:10.1145/2610384.2628055

[38] C. E. Jimenez et al., “SWE-bench: Can Language Models Resolve Real-World GitHub Issues?” 2023. arXiv:2310.06770

[39] R. Aleithan et al., “SWE-Bench+: Enhanced Coding Benchmark for LLMs,” 2024. arXiv:2410.06992

[40] C. E. Shannon, “A Mathematical Theory of Communication,” Bell System Technical Journal 27, 1948. doi:10.1002/j.1538-7305.1948.tb01338.x

[41] A. N. Kolmogorov, “Three approaches to the quantitative definition of information,” Problemy Peredachi Informatsii 1(1), 1965 (in Russian); English translation, International Journal of Computer Mathematics 2, 1968. doi:10.1080/00207166808803030

[42] R. J. Solomonoff, “A formal theory of inductive inference. Part I,” Information and Control 7(1), 1964. doi:10.1016/S0019-9958(64)90223-2

[43] G. J. Chaitin, “A Theory of Program Size Formally Identical to Information Theory,” Journal of the ACM 22(3), 1975. doi:10.1145/321892.321894

[44] J. Rissanen, “Modeling by shortest data description,” Automatica 14(5), 1978. doi:10.1016/0005-1098(78)90005-5

[45] B. Ray, V. Hellendoorn, S. Godhane, Z. Tu, A. Bacchelli and P. Devanbu, “On the ‘naturalness’ of buggy code,” ICSE 2016. doi:10.1145/2884781.2884848

[46] Z. Tu, Z. Su and P. Devanbu, “On the localness of software,” FSE 2014. doi:10.1145/2635868.2635875

[47] M. Allamanis, E. T. Barr, P. Devanbu and C. Sutton, “A Survey of Machine Learning for Big Code and Naturalness,” ACM Computing Surveys 51(4), 2018. doi:10.1145/3212695

[48] 陈浙哲, 刘忠鑫, 鄢萌, 徐洲, 夏鑫, 雷晏 (Z. Chen, Z. Liu, M. Yan, Z. Xu, X. Xia and Y. Lei), “代码自然性及其应用研究进展” (Research progress of code naturalness and its application), 软件学报 (Journal of Software) 33(8), 3015 to 3034, 2022. doi:10.13328/j.cnki.jos.006355

[49] G. Sridhara, V. S. Sinha and S. Mani, “Naturalness of Natural Language Artifacts in Software,” ISEC 2015 (India Software Engineering Conference). doi:10.1145/2723742.2723758

[50] P. Devanbu, “On the naturalness of software,” keynote, ISEC 2013 (India Software Engineering Conference). doi:10.1145/2442754.2442763

[51] A. Z. H. Yang, S. Kolak, V. J. Hellendoorn, R. Martins et al., “Revisiting Unnaturalness for Automated Program Repair in the Era of Large Language Models,” ICSE 2025. doi:10.1109/ICSE55347.2025.00089

[52] E. W. Dijkstra, “Guarded commands, nondeterminacy and formal derivation of programs,” Communications of the ACM 18(8), 1975. doi:10.1145/360933.360975

[53] N. Wirth, “Program development by stepwise refinement,” Communications of the ACM 14(4), 1971. doi:10.1145/362575.362577

[54] C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM 12(10), 1969. doi:10.1145/363235.363259

[55] J.-R. Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996. doi:10.1017/CBO9780511624162

[56] J.-R. Abrial, Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010. doi:10.1017/CBO9781139195881

[57] R.-J. Back and J. von Wright, Refinement Calculus: A Systematic Introduction, Springer, 1998. doi:10.1007/978-1-4612-1674-2

[58] F. L. Bauer and H. Wössner, Algorithmic Language and Program Development, Springer, 1982. doi:10.1007/978-3-642-61807-9

[59] S. Gulwani, “Automating string processing in spreadsheets using input-output examples,” POPL 2011. doi:10.1145/1926385.1926423

[60] S. Gulwani, O. Polozov and R. Singh, “Program Synthesis,” Foundations and Trends in Programming Languages 4(1-2), 2017. doi:10.1561/2500000010

[61] F. P. Brooks, “No Silver Bullet: Essence and Accidents of Software Engineering,” Computer 20(4), 1987. doi:10.1109/MC.1987.1663532

[62] P. Naur, “Programming as theory building,” Microprocessing and Microprogramming 15(5), 1985. doi:10.1016/0165-6074(85)90032-8

[63] M. M. Lehman, “Programs, life cycles, and laws of software evolution,” Proceedings of the IEEE 68(9), 1980. doi:10.1109/PROC.1980.11805

[64] P. Zave and M. Jackson, “Four dark corners of requirements engineering,” ACM Transactions on Software Engineering and Methodology 6(1), 1997. doi:10.1145/237432.237434

[65] R. Landauer, “Irreversibility and Heat Generation in the Computing Process,” IBM Journal of Research and Development 5(3), 1961. doi:10.1147/rd.53.0183

[66] C. H. Bennett, “Logical Reversibility of Computation,” IBM Journal of Research and Development 17(6), 1973. doi:10.1147/rd.176.0525

[67] M. Franz and T. Kistler, “Slim binaries,” Communications of the ACM 40(12), 1997. doi:10.1145/265563.265576

[68] C. W. Fraser, “Automatic inference of models for statistical code compression,” PLDI 1999. doi:10.1145/301618.301672

[69] P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,” POPL 1977. doi:10.1145/512950.512973

[70] Y. Futamura, “Partial evaluation of computation process: an approach to a compiler-compiler,” Systems, Computers, Controls 2(5), 1971; reprinted in Higher-Order and Symbolic Computation 12(4), 1999. doi:10.1023/A:1010095604496

[71] A. P. Ershov, “Mixed computation: potential applications and problems for study,” Theoretical Computer Science 18(1), 1982. doi:10.1016/0304-3975(82)90111-6

[72] W. A. Howard, “The formulae-as-types notion of construction,” in J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980.

[73] 土居真之, 肥後芳樹, 有馬諒, 下仲健斗, 楠本真二 (M. Doi, Y. Higo, R. Arima, K. Shimonaka and S. Kusumoto), “ソースコードの「自然さ」を利用した自動生成ファイルの特定” (Identifying auto-generated files using the naturalness of source code), 電子情報通信学会技術研究報告 (IEICE Technical Report) 117(380), 19 to 24, January 2018. https://sdl.ist.osaka-u.ac.jp/pman/pman3.cgi?D=517

[74] M. Doi, Y. Higo, R. Arima, K. Shimonaka and S. Kusumoto, “On the naturalness of auto-generated code: can we identify auto-generated code automatically?” ICPC 2018. doi:10.1145/3196321.3196356

[75] F. V. Arrebola, “Modelo de sugestão de código-fonte baseado em modelos de linguagem organizados em um contexto hierárquico” (A source code suggestion model based on language models organized in a hierarchical context), doctoral thesis in electrical engineering, Fundação Educacional Inaciana Padre Sabóia de Medeiros (FEI), Brazil, 2018. Advisor R. A. C. Bianchi.

[76] G. Febres, K. Jaffé and C. Gershenson, “Complexity measurement of natural and artificial languages,” Complexity 20(6), 2015. doi:10.1002/cplx.21529

[77] M. Rahman, D. Palani and P. C. Rigby, “Natural Software Revisited,” ICSE 2019. doi:10.1109/ICSE.2019.00022

[78] A. Torres, S. Baltes, C. Treude and M. Wagner, “Applying Information Theory to Software Evolution,” NLBSE 2023. doi:10.1109/NLBSE59153.2023.00017

[79] A. Blass, N. Dershowitz and Y. Gurevich, “When are two algorithms the same?,” Bulletin of Symbolic Logic 15(2), 2009. arXiv:0811.0811. https://arxiv.org/abs/0811.0811

[80] Y. N. Moschovakis, “What is an algorithm?,” in Mathematics Unlimited: 2001 and Beyond, Springer, 2001. https://www.math.ucla.edu/~ynm/papers/eng.pdf

[81] M. Y. Vardi, “What is an algorithm?,” Communications of the ACM 55(3), 2012. doi:10.1145/2093548.2093549

[82] S. Laddad, A. Cheung, J. M. Hellerstein and M. Milano, “Flo: a Semantic Foundation for Progressive Stream Processing,” POPL 2025. arXiv:2411.08274. https://arxiv.org/abs/2411.08274

[83] The Elm Architecture, Elm guide. https://guide.elm-lang.org/architecture/

[84] Temporal, “Workflows” (event history), documentation. https://docs.temporal.io/workflows

[85] A. Pnueli, M. Siegel and E. Singerman, “Translation validation,” TACAS 1998. doi:10.1007/BFb0054170

[86] X. Yang, Y. Chen, E. Eide and J. Regehr, “Finding and understanding bugs in C compilers,” PLDI 2011. doi:10.1145/1993498.1993532

[87] C. Nandi, M. Willsey, A. Zhu et al., “Rewrite Rule Inference Using Equality Saturation,” OOPSLA 2021. arXiv:2108.10436. https://arxiv.org/abs/2108.10436

[88] C. Le Goues, T. Nguyen, S. Forrest and W. Weimer, “GenProg: A Generic Method for Automatic Software Repair,” IEEE TSE 38(1), 2012. doi:10.1109/TSE.2011.104

[89] F. Long and M. Rinard, “Automatic patch generation by learning correct code,” POPL 2016. doi:10.1145/2837614.2837617

[90] J. Bader, A. Scott, M. Pradel and S. Chandra, “Getafix: Learning to Fix Bugs Automatically,” OOPSLA 2019. arXiv:1902.06111. https://arxiv.org/abs/1902.06111

[91] K. Etemadi, N. Harrand, S. Larsen et al., “Sorald: Automatic Patch Suggestions for SonarQube Static Analysis Violations,” IEEE TDSC, 2022. arXiv:2103.12033. https://arxiv.org/abs/2103.12033

[92] Z. Qi, F. Long, S. Achour and M. Rinard, “An analysis of patch plausibility and correctness for generate-and-validate patch generation systems,” ISSTA 2015. doi:10.1145/2771783.2771791

[93] E. K. Smith, E. T. Barr, C. Le Goues and Y. Brun, “Is the cure worse than the disease? Overfitting in automated program repair,” ESEC/FSE 2015. doi:10.1145/2786805.2786825

[94] X.-B. D. Le, F. Thung, D. Lo and C. Le Goues, “Overfitting in semantics-based automated program repair,” Empirical Software Engineering 23, 2018. doi:10.1007/s10664-017-9577-2

[95] Y. Xiong, X. Liu, M. Zeng, L. Zhang and G. Huang, “Identifying patch correctness in test-based program repair,” ICSE 2018. doi:10.1145/3180155.3180182

[96] T. Durieux, F. Madeiral, M. Martinez and R. Abreu, “Empirical Review of Java Program Repair Tools: A Large-Scale Experiment on 2,141 Bugs and 23,551 Repair Attempts,” ESEC/FSE 2019. arXiv:1905.11973. https://arxiv.org/abs/1905.11973

[97] K. Liu, A. Koyuncu, T. F. Bissyandé et al., “You Cannot Fix What You Cannot Find! An Investigation of Fault Localization Bias in Benchmarking Automated Program Repair Systems,” ICST 2019. arXiv:1812.07283. https://arxiv.org/abs/1812.07283

[98] M. Monperrus, “Automatic Software Repair: A Bibliography,” ACM Computing Surveys 51(1), 2018. doi:10.1145/3105906

[99] C. S. Xia, Y. Deng, S. Dunn and L. Zhang, “Agentless: Demystifying LLM-based Software Engineering Agents,” 2024. arXiv:2407.01489. https://arxiv.org/abs/2407.01489

[100] S. Kapoor, B. Stroebl, Z. S. Siegel, N. Nadgir and A. Narayanan, “AI Agents That Matter,” 2024. arXiv:2407.01502. https://arxiv.org/abs/2407.01502

[101] M. H. Erol, B. El, M. Suzgun, M. Yuksekgonul and J. Zou, “Cost-of-Pass: An Economic Framework for Evaluating Language Models,” 2025. arXiv:2504.13359. https://arxiv.org/abs/2504.13359

[102] D. Zan, Z. Huang, W. Liu et al., “Multi-SWE-bench: A Multilingual Benchmark for Issue Resolving,” 2025. arXiv:2504.02605. https://arxiv.org/abs/2504.02605

[103] R. Widyasari, S. Q. Sim, C. Lok et al., “BugsInPy: a database of existing bugs in Python programs to enable controlled testing and debugging studies,” ESEC/FSE 2020. doi:10.1145/3368089.3417943

[104] M. Allamanis, “The Adverse Effects of Code Duplication in Machine Learning Models of Code,” Onward! 2019. arXiv:1812.06469. https://arxiv.org/abs/1812.06469

[105] K. N. Khan, M. Hirki, T. Niemi, J. K. Nurminen and Z. Ou, “RAPL in Action: Experiences in Using RAPL for Power Measurements,” ACM TOMPECS 3(2), 2018. doi:10.1145/3177754

[106] The Rust project, rustfix and cargo fix. https://github.com/rust-lang/rustfix

[107] R.-M. Karampatsis and C. Sutton, “How Often Do Single-Statement Bugs Occur? The ManySStuBs4J Dataset,” MSR 2020. doi:10.1145/3379597.3387491

[108] C. Richter and H. Wehrheim, “TSSB-3M: Mining single statement bugs at massive scale,” MSR 2022. doi:10.1145/3524842.3528505

[109] H. Coles, T. Laurent, C. Henard, M. Papadakis and A. Ventresque, “PIT: a practical mutation testing tool for Java,” ISSTA 2016. doi:10.1145/2931037.2948707

[110] R. Just, D. Jalali, L. Inozemtseva, M. D. Ernst, R. Holmes and G. Fraser, “Are mutants a valid substitute for real faults in software testing?” FSE 2014. doi:10.1145/2635868.2635929

[111] I. J. Good, “Speculations Concerning the First Ultraintelligent Machine,” Advances in Computers 6, 1965. doi:10.1016/S0065-2458(08)60418-0

[112] J. Schmidhuber, “Gödel Machines: Fully Self-referential Optimal Universal Self-improvers,” in Artificial General Intelligence, Springer, 2007. doi:10.1007/978-3-540-68677-4_7

[113] E. Yudkowsky, “Intelligence Explosion Microeconomics,” Technical report 2013-1, Machine Intelligence Research Institute, 2013. https://intelligence.org/files/IEM.pdf

[114] M. H. Löb, “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic 20(2), 1955. doi:10.2307/2266895

[115] E. Yudkowsky and M. Herreshoff, “Tiling Agents for Self-Modifying AI, and the Löbian Obstacle,” Machine Intelligence Research Institute, 2013. https://intelligence.org/files/TilingAgentsDraft.pdf

[116] E. Zelikman, E. Lorch, L. Mackey and A. T. Kalai, “Self-Taught Optimizer (STOP): Recursively Self-Improving Code Generation,” 2023. doi:10.48550/arXiv.2310.02304

[117] J. Zhang, S. Hu, C. Lu, R. Lange and J. Clune, “Darwin Gödel Machine: Open-Ended Evolution of Self-Improving Agents,” 2025. doi:10.48550/arXiv.2505.22954

[118] A. Novikov et al., “AlphaEvolve: A coding agent for scientific and algorithmic discovery,” 2025. doi:10.48550/arXiv.2506.13131

[119] G. Wang, Y. Xie, Y. Jiang, A. Mandlekar, C. Xiao, Y. Zhu, L. Fan and A. Anandkumar, “Voyager: An Open-Ended Embodied Agent with Large Language Models,” 2023. doi:10.48550/arXiv.2305.16291

[120] Y. Futamura, “Partial Evaluation of Computation Process: An Approach to a Compiler-Compiler,” Higher-Order and Symbolic Computation 12(4), 1999 (first published 1971). doi:10.1023/A:1010095604496

[121] V. F. Turchin, “The Concept of a Supercompiler,” ACM Transactions on Programming Languages and Systems 8(3), 1986. doi:10.1145/5956.5957

[122] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce and A. Schmitt, “Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem,” ACM Transactions on Programming Languages and Systems 29(3), 2007. doi:10.1145/1232420.1232424

[123] M. Hofmann, B. Pierce and D. Wagner, “Symmetric Lenses,” POPL, 2011. doi:10.1145/1926385.1926428

[124] K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr and J. F. Terwilliger, “Bidirectional Transformations: A Cross-Discipline Perspective,” ICMT, LNCS 5563, 2009. doi:10.1007/978-3-642-02408-5_19

[125] E. W. Dijkstra, “A Constructive Approach to the Problem of Program Correctness,” BIT 8(3), 1968. doi:10.1007/BF01933419

[126] A. Hall and R. Chapman, “Correctness by Construction: Developing a Commercial Secure System,” IEEE Software 19(1), 2002. doi:10.1109/52.976937

[127] Y. Minsky, “OCaml for the Masses,” Communications of the ACM 54(11), 2011. doi:10.1145/2018396.2018413

[128] D. A. Turner, “Total Functional Programming,” Journal of Universal Computer Science 10(7), 2004. doi:10.3217/jucs-010-07-0751

[129] R. Di Cosmo and S. Zacchiroli, “Software Heritage: Why and How to Preserve Software Source Code,” iPRES 2017, Kyoto. https://hal.science/hal-01590958

[130] Software Heritage, archive counters, read 13 October 2026: 30,253,266,524 file contents and 448,311,919 origins. https://archive.softwareheritage.org/api/1/stat/counters/

[131] Rosetta Code, main page, read 13 October 2026: 1,360 tasks, 421 draft tasks, 1,009 known languages. https://rosettacode.org/wiki/Rosetta_Code