CVE-2026-72714

ملخص

مُثبِت Rocq لا يستعيد نسخة رسم الكون (universe graph) من علامة فحص الكون عند إغلاق وحدة عطّلت الفحص محليًا. من المتوقع أن يستمر `Unset Universe Checking` المحلي داخل وحدة ما حتى تنتهي الوحدة فقط، وتُستعاد العلامة العامة، لكن رسم الكون يحتفظ بنسخته الخاصة التي تبقى معطّلة. عندئذ تتناقض الرؤيتان: يُبلّغ `Test Universe Checking` عن الفحص بأنه مُفعّل بينما تستمر النواة في قبول مصطلحات غير متسقة مع الكون. وبما أن القيد بين كونين لم يعد مفروضًا، ينطبق مفارقة Hurkens وينتج برهانًا على `False`، ومنه يلزم أي قضية. لا يستخدم البرهان أي مسلّمات أو إضافات أو ميزات غير آمنة بعد إغلاق الوحدة، ويُبلّغ `Print Assumptions` عنه بأنه مغلق في السياق العام، لذا لا يعكس تدقيق المسلّمات ولا استعلام العلامة حالة النواة الفعلية. لا يتوفر أي إصلاح.

المصادر

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — تعطّل تزامن حالة فحص الكون في Rocq بعد إغلاق الوحدة النمطية