أشجار تقييم المتطلبات (RET)

نظرة سريعة

ما: جبر متطلبات ثنائي وثلاثي القيم مع حد صريح أساسي لماذا: جعل منطق البوابة صريحًا، وقابلًا للتدقيق، وحتميًا - لا قواعد مخفية من: المطورون والمشغلون الذين يؤلفون متطلبات بوابة معقدة المتطلبات السابقة: فهم أساسي للشروط (انظر condition_authoring.md)

خلفية منخفضة/AOT (RET)

RET الآن توفر واجهة خلفية منخفضة/ AOT مضافة في ret-logic:

تجميع مرة واحدة: Requirement<P> -> CompiledRequirement<K>
قيّم المسارات السريعة وقت التشغيل:
- CompiledRequirement::eval
- CompiledRequirement::eval_block
- CompiledRequirement::eval_tristate (+ variant trace)
صدّر تبعيات مفاتيح المحمول الحتمية:
- CompiledRequirement::predicate_keys()
احسب عروض البواقي والتقدم الموجّهة للتفسير:
- Requirement::residual
- CompiledRequirement::residual
حافظ على التوافق:
- تظل Requirement::eval* مدعومة ودون تغيير.

هذا مستقل عن النطاقات: توفر النطاقات خريطة مفاتيح حتمية (PredicateRegistry) وتنفيذ مفاتيح في وقت التشغيل (PredicateRuntime). يتطلب شرح المتبقي/التقدم أيضًا تنفيذات تقدم على مستوى الشرط أو المقياس من خلال ConditionProgressEval و PredicateProgressRuntime.

الإدخال في وقت الترجمة مقابل وقت التشغيل

لا تؤثر عملية استيعاب المصدر (RON، JSON، DSL، حمولة MCP، إلخ) على دلالات RET. الفرق هو دورة الحياة:

الاستيعاب في وقت التجميع/وقت التحميل: تحليل + تحقق + تجميع مرة واحدة، تخزين الأثر المجمع.
الاستيعاب في وقت التشغيل: تحليل + تحقق + تجميع عند وصول البوابة، ثم تنفيذ الأثر المجمع.

تتقارب كلا المسارين إلى نفس الجبر وسلوك المحلل المترجم عندما تكون متطلبات الإدخال متكافئة.

لماذا RET؟

المشكلة: كيف يمكنك دمج عدة فحوصات للأدلة في قرار بوابة واحد؟

سيناريو المثال: “أريد نشره في الإنتاج إذا:

البيئة هي ‘إنتاج’ و
تم اجتياز الاختبارات وَ
التغطية تزيد عن 85% و
تمت الموافقة على الأقل من 2 من 3 مراجعين

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

مع RET: تعبر عن المنطق كهيكل شجري:

{
  "requirement": {
    "And": [
      { "Condition": "env_is_prod" },
      { "Condition": "tests_ok" },
      { "Condition": "coverage_ok" },
      {
        "RequireGroup": {
          "min": 2,
          "reqs": [
            { "Condition": "alice_approved" },
            { "Condition": "bob_approved" },
            { "Condition": "carol_approved" }
          ]
        }
      }
    ]
  }
}

الفوائد:

صريح: المنطق مرئي في مواصفات السيناريو
قابل للفحص: قانون المتطلبات هو بيانات صريحة بدلاً من تدفق تحكم مخفي.
حتمي: نفس المتطلبات التي تم التحقق منها وتعيين الحقيقة الورقية الدقيقة تنتج نفس نتيجة RET.
قابل لإعادة التقييم: يمكن تقييم القانون الكنسي للمتطلبات والمدخلات الورقية دون إعادة استعلام المزودين. هذه الخاصية RET لا تؤسس بمفردها إعادة تشغيل دلالات Decision Gate الكاملة، أو تاريخ الالتزام المقبول، أو مصداقية الأدلة، أو عدم الإنكار.

[Security]: Explicit gate logic narrows the hidden-control-flow surface; it does not prove that provider, comparator, admission, policy, transition, or dispatch behavior is benign. Current runpacks provide bounded integrity and تدقيق/تصدير الدليل فقط.

نموذج ذهني: شجرة تقييم RET

إليك كيفية تقييم شجرة المتطلبات:

RET EVALUATION TREE (simplified)

Gate Requirement (tree structure)
  And
  |-- Pred(A) -> true
  |-- Pred(B) -> unknown
  |-- Not(C) -> false
  `-- RequireGroup (min: 2)
      |-- Pred(D) -> true
      |-- Pred(E) -> true
      `-- Pred(F) -> false

Strong Kleene Logic: And(true, unknown, true, true) -> unknown
(gate holds)

ترتيب التقييم:

تقييم شروط الورقة يكون ثلاثي الحالة (صحيح/خطأ/غير معروف)
تجمع عقد المشغل نتائج الأطفال عبر منطق ثلاثي الحالة
نتيجة العقدة الجذرية تحدد نتيجة البوابة

نتائج الولايات الثلاث

RET يستخدم منطق ثلاثي الحالة (ليس فقط صحيح/خطأ):

true: تصاريح الدخول (تم استيفاء جميع المتطلبات)
false: فشل البوابة (تعارض المتطلبات)
unknown: البوابة تحتفظ (المتطلبات غير حاسمة)

لماذا ثلاثي الحالة؟ تغلق البوابات بشكل آمن: تمر البوابة فقط عندما يتم تقييم الشرط إلى true. تمنع النتائج unknown البوابات من المرور حتى اكتمل الدليل.

مثال:

Gate: And(tests_ok, coverage_ok)
Conditions:
- tests_ok: true (tests passed)
- coverage_ok: unknown (coverage report missing)

Outcome: unknown (gate holds until coverage is available)

مشغلات أساسية

و

الدلالات: يجب أن تكون جميع الأطفال true

جدول الحقيقة (2 عاملين):

اليسار	اليمين	النتيجة
true	true	true
true	false	false
true	unknown	unknown
false	(أي)	false
unknown	true	unknown
unknown	unknown	unknown

مثال:

{
  "requirement": {
    "And": [
      { "Condition": "tests_ok" },
      { "Condition": "coverage_ok" }
    ]
  }
}

حالة الاستخدام: يجب أن تمر كل من الاختبارات والتغطية

السلوك:

جميع true -> true (تصاريح البوابة)
أي false -> false (البوابة تفشل)
بخلاف ذلك -> unknown (البوابة مغلقة)

أو

الدلالات: يمكن أن يكون أي طفل true

جدول الحقيقة (2 عاملين):

اليسار	اليمين	النتيجة
صحيح	(أي)	صحيح
خطأ	خطأ	خطأ
خطأ	غير معروف	غير معروف
غير معروف	خطأ	غير معروف
غير معروف	غير معروف	غير معروف

مثال:

{
  "requirement": {
    "Or": [
      { "Condition": "manual_override" },
      { "Condition": "tests_ok" }
    ]
  }
}

حالة الاستخدام: يجب أن ينجح إما التعديل اليدوي أو الاختبارات الآلية

السلوك:

أي true -> true (تصاريح البوابة)
جميع false -> false (فشل البوابة)
بخلاف ذلك -> unknown (البوابة مغلقة)

لا

الدلالات: عكس نتيجة الطفل

جدول الحقيقة:

المدخلات	النتيجة
true	false
false	true
unknown	unknown

مثال:

{
  "requirement": {
    "And": [
      { "Condition": "tests_ok" },
      { "Not": { "Condition": "blocklist_hit" } }
    ]
  }
}

حالة الاستخدام: يجب أن تنجح الاختبارات ويجب ألا يتم الوصول إلى القائمة السوداء

السلوك:

true -> false
false -> true
unknown -> unknown (فشل مغلق: لا يمكن تأكيد الغياب)

RequireGroup (نصاب)

الدلالات: يجب أن يكون على الأقل N من M الأطفال true

المعلمات:

min: الحد الأدنى لعدد النتائج true المطلوبة
reqs: مصفوفة من المتطلبات الفرعية

مثال:

{
  "requirement": {
    "RequireGroup": {
      "min": 2,
      "reqs": [
        { "Condition": "alice_approved" },
        { "Condition": "bob_approved" },
        { "Condition": "carol_approved" }
      ]
    }
  }
}

حالة الاستخدام: يجب أن يوافق على الأقل 2 من 3 مراجعين

السلوك:

عد النتائج true
إذا كان العدد >= min -> true (تم الوصول إلى النصاب)
إذا كان العدد + غير معروف < min -> false (الحد الأدنى غير ممكن)
بخلاف ذلك -> unknown (في انتظار النصاب)

أمثلة جدول الحقيقة:

النتائج	الحد الأدنى	النتيجة	السبب
[صحيح، صحيح، خطأ]	2	صحيح	2 صحيح >= الحد الأدنى (تم الوصول إلى النصاب)
[صحيح، غير معروف، غير معروف]	2	غير معروف	1 صحيح، لا يمكن الوصول إلى الحد الأدنى بعد
[صحيح، خطأ، خطأ]	2	خطأ	1 صحيح، الحد الأقصى الممكن هو 1 < الحد الأدنى
[صحيح، صحيح، غير معروف]	2	صحيح	2 صحيح >= الحد الأدنى (تم الوفاء به بالفعل)
[خطأ، خطأ، خطأ]	2	خطأ	0 صحيح، مستحيل

[المطور]: راجع ret-logic crate للتنفيذ. يقوم RequireGroup بحساب true/false بشكل مستقل (unknown ليس أي منهما).

شرط (عقدة ورقية)

الدلالات: الإشارة إلى حالة بواسطة المفتاح

مثال:

{
  "requirement": { "Condition": "tests_ok" }
}

حالة الاستخدام: بوابة بسيطة بشرط واحد

السلوك:

يقيم نتيجة الحالة الثلاثية للشرط
يجب أن توجد الشرط في RawScenarioSpec.conditions

قواعد انتشار ثلاثي الولايات

كيف تنتشر نتائج unknown عبر المشغلين:

و الانتشار

المعاملات	النتيجة	السبب
`And(true, true, true)`	true	جميع المتطلبات مُرضية
`And(true, false, true)`	false	واحدة تفشل -> And تفشل
`And(true, unknown, true)`	unknown	لا يمكن تأكيد جميع القيم كـ true بعد
`And(false, unknown)`	false	واحدة تفشل (دائرة قصيرة)
`And(unknown, unknown)`	unknown	الأدلة قيد الانتظار

القاعدة: false تهيمن؛ جميع true تعطي true؛ خلاف ذلك unknown

أو انتشار

المعاملات	النتيجة	السبب
`Or(false, false, false)`	false	جميع المتطلبات فشلت
`Or(true, false, false)`	true	واحدة تنجح -> Or تنجح
`Or(false, unknown, false)`	unknown	لا يمكن تأكيد جميع القيم كـ false بعد
`Or(true, unknown)`	true	واحدة تنجح (دائرة قصيرة)
`Or(unknown, unknown)`	unknown	الأدلة قيد الانتظار

القاعدة: true تهيمن؛ جميع false تعطي false؛ خلاف ذلك unknown

توزيع RequireGroup

النتائج	الحد الأدنى	عدد true	عدد unknown	النتيجة
[T, T, F]	2	2	0	true (تم الوصول إلى الحد الأدنى)
[T, U, U]	2	1	2	unknown (الحد الأقصى 3، نحتاج 2)
[T, F, F]	2	1	0	false (الحد الأقصى 1 < الحد الأدنى)
[U, U, U]	2	0	3	unknown (الحد الأقصى 3، نحتاج 2)
[F, F, F]	2	0	0	false (مستحيل)

قاعدة:

إذا كان true_count >= min -> true (تم الوصول إلى النصاب)
إذا كان true_count + unknown_count < min -> false (الحد الأدنى غير ممكن)
بخلاف ذلك -> unknown (في انتظار النصاب)

[LLM Agent]: عندما تعيد RequireGroup unknown، تحتاج إلى مزيد من الأدلة. تحقق من أي الشروط غير معروفة واعمل على تلبيتها.

حالات الاستخدام العملية

متطلب بسيط: كلا الشرطين

السيناريو: نشر إذا تم اجتياز الاختبارات و كانت التغطية فوق 85%

{
  "And": [
    { "Condition": "tests_ok" },
    { "Condition": "coverage_ok" }
  ]
}

متطلب النصاب: 2 من 3 مراجعين

السيناريو: دمج PR إذا تمت الموافقة من قبل 2 على الأقل من 3 مراجعين

{
  "RequireGroup": {
    "min": 2,
    "reqs": [
      { "Condition": "alice_approved" },
      { "Condition": "bob_approved" },
      { "Condition": "carol_approved" }
    ]
  }
}

متطلب الاستبعاد: غير مدرج في القائمة السوداء

السيناريو: نشر إذا لم يكن مدرجًا في القائمة السوداء

{
  "Not": { "Condition": "blocklist_hit" }
}

متطلب معقد: (A AND B) OR C

السيناريو: نشر إذا (تم اجتياز الاختبارات و كانت التغطية جيدة) أو تجاوز يدوي

{
  "Or": [
    {
      "And": [
        { "Condition": "tests_ok" },
        { "Condition": "coverage_ok" }
      ]
    },
    { "Condition": "manual_override" }
  ]
}

RET في طوبولوجيا Monotone-DAG

توبولوجيا السيناريو ليست جهاز توجيه النتائج. كل مرحلة غير جذرية تحمل قانون RET أحادي الاتجاه واحد على معرفات المراحل المكتملة. تلك الذرات هي المصدر الوحيد لحواف الاعتماد الواردة. على سبيل المثال، يصبح ship جاهزًا بعد أن تكتمل build و security_review أو operator_override:

{
  "kind": "requires",
  "requirement": {
    "And": [
      { "Condition": "build" },
      {
        "Or": [
          { "Condition": "security_review" },
          { "Condition": "operator_override" }
        ]
      }
    ]
  }
}

تقبل متطلبات التوبولوجيا وقوانين إكمال السيناريو فقط تحسين RET أحادي الاتجاه: لا نفي ولا تعبير يمكن أن يصبح false مع زيادة مجموعة المراحل المكتملة. تحتفظ متطلبات إكمال المرحلة بكامل RET، بما في ذلك النفي القانوني، لأنها تقيم ملاحظة الأدلة بدلاً من تقدم الرسم البياني الأحادي الاتجاه.

عندما تجعل إكمال واحد العديد من الأشقاء جاهزين، يبقى الجميع مستقلين ready_unopened. يمكن للمشغل فتح أي منهم أو جميعهم. فتح واحد لا يختار فرعًا حصريًا ولا يلغي أو يعين أو يحتفظ بآخر.

أوضاع المنطق

تستخدم بنية MCP الحالية القيمة الافتراضية لـ ControlPlaneConfig Strong Kleene. تدعم مكتبة RET الأساسية وتكوين التحكم البرمجي أيضًا Bochvar. لذلك، فإن هوية المُقيِّم/وضع المنطق هي جزء من المدخلات الدلالية ويجب الاحتفاظ بها لأي مطالبة بإعادة التشغيل.

الخصائص الرئيسية لـ Strong Kleene:

الخصائص الرئيسية:

And(true, unknown) -> unknown (لا يمكن تأكيد أن جميعها صحيحة)
Or(false, unknown) -> unknown (لا يمكن تأكيد أن جميعها خاطئة)
Not(unknown) -> unknown (لا يمكن عكس عدم اليقين)

يُعد Bochvar unknown معديًا لـ And و Or، بما في ذلك الحالات التي يمكن لـ Strong Kleene حلها من خلال قيمة ماصة. يستخدم RequireGroup نفس قاعدة العد/الحدود في كلا الوضعين الحاليين.

لماذا يعتبر Strong Kleene هو الافتراضي الحالي:

أكثر بديهية للأدلة الجزئية
دوائر قصيرة عند الإمكان (And(false, unknown) -> false)
الفشل في التوازن مع قابلية الاستخدام

[المطور]: راجع crates/ret-logic/src/lib.rs لخوارزمية التقييم.

حالات الاستخدام

أساسي: بوابات معقدة تتطلب تركيبات بوليانية (و، أو، نصاب) ثانوي: بوابات بسيطة مع شروط فردية (عقدة الشرط فقط) نموذج مضاد: لا تقم بتعشيش RETs بعمق شديد - يفضل الشروط المركزة والأشجار المسطحة

استكشاف الأخطاء وإصلاحها

المشكلة: البوابة عالقة في `unknown`

الأعراض: البوابة لا تمر أبداً، دائماً تعود unknown

السبب: واحدة أو أكثر من الشروط تقيم إلى unknown

الحل:

تحقق من تتبع البوابة لمعرفة أي الشروط هي unknown
إصلاح مشكلات الحالة الأساسية (انظر condition_authoring.md)
الأسباب الشائعة:
- لم يتم قبول أي مرشح دليل لشرط مطلوب؛
- كانت هناك مرشحين لكنهم فشلوا في ضمان، أو حداثة، أو اتفاق، أو سياسة النصاب;
- فشلت الاكتساب المحلي من الناحية التشغيلية وبالتالي لم يتم سك أي دليل.

عدم تطابق نوع/شرط ما بعد التحقق هو فشل في النزاهة، وليس unknown دلاليًا.

المشكلة: RequireGroup لا تنجح أبداً

الأعراض: RequireGroup دائمًا ما تعيد false أو unknown

السبب: min مرتفع جدًا، أو عدد كبير من الشروط فشل.

الحل:

تحقق من قيمة min مقابل عدد الشروط
تحقق من نتائج الحالة في تتبع البوابة
تأكد من أن هناك على الأقل min شرط يمكن أن يكون true في نفس الوقت

مثال:

// BAD: min is 3, but only 2 conditions
{
  "RequireGroup": {
    "min": 3,
    "reqs": [
      { "Condition": "a" },
      { "Condition": "b" }
    ]
  }
}

// GOOD: min <= number of conditions
{
  "RequireGroup": {
    "min": 2,
    "reqs": [
      { "Condition": "a" },
      { "Condition": "b" },
      { "Condition": "c" }
    ]
  }
}

المشكلة: لم يتم فتح شقيق جاهز تلقائيًا

الأعراض: إكمال أحد الوالدين يجعل العديد من الأطفال جاهزين، لكن لا يبدأ أي منهم العمل.

السبب: الجاهزية والفتح مفصولتان عمدًا. تستمد DG الحدود الجاهزة الكنسية؛ لا تختار سياسة المشغل أو تلمح إلى التفرع.

الحل: اختر مرحلة ready_unopened صريحة واستدعِ scenario_open_stage مع الرأس المقبول بالضبط. قد تختار أداة التنسيق عدة أشقاء، لكن التعيين، والإيجارات، والتفرد، والتوافق مع الوكلاء هي سلطات منفصلة.

نصائح التأليف

1. حافظ على استقرار مفاتيح الحالة ووصفها بدقة

استخدم tests_ok وليس pred1
يتم الإشارة إلى المفاتيح في حزم التشغيل للتدقيق

2. استخدم RequireGroup لفحوصات نمط النصاب

مثال: “2 من 3 مراجعين”، “3 من 5 فحوصات مركز البيانات”
بديل: شروط متعددة و (لكن أقل مرونة)

3. تفضيل الأشجار الصغيرة ذات الظروف المركزة

أسهل في التدقيق والفهم
أسهل في تصحيح الأخطاء عند فشل البوابات

4. تحقق من هيكل RET أثناء تعريف السيناريو

Decision Gate تتحقق من RETs في وقت scenario_define
يفشل بسرعة إذا كانت البنية غير صالحة (على سبيل المثال، الإشارة إلى شروط غير موجودة)

5. الحفاظ على تمييز القوانين الطوبولوجية والدليل

استخدم RET أحادي الاتجاه لمعرفات المرحلة للمتطلبات السابقة وإكمال السيناريو.
استخدم قانون إكمال الأدلة لمرحلة واحدة باستخدام معرف الشرط الكامل.
لا تدعي توجيه نتيجة false أو unknown العادية.
إعادة النظر في هذه الإرشادات فقط بعد إغلاق قرار الانتقال المعيق ووجود أدلة التنفيذ.

مسارات التعلم المتقاطعة

مسار المستخدم الجديد: getting_started.md -> condition_authoring.md -> هذا الدليل -> integration_patterns.md

مسار المنطق المتقدم: هذا الدليل -> evidence_flow_and_execution_model.md -> فهم كيف تتناسب RETs مع خط تقييم الأداء

مسار الأمان: هذا الدليل -> security_guide.md -> تعلم كيف تمنع المنطق الصريح الأبواب الخلفية

معجم

و: مشغل يتطلب أن تكون جميع الأطفال true.

البوابة: نقطة قرار في سيناريو، يتم تقييمها عبر RET مقابل الأدلة.

أو: عامل يتطلب أن يكون أي طفل true.

ملاحظة: المشغل يعكس نتيجة الطفل (true <-> false).

الحالة: تعريف فحص الأدلة: استعلام + مقارن + قيمة متوقعة.

RequireGroup: مشغل النصاب يتطلب أن يكون على الأقل N من M الأطفال true.

RET: شجرة تقييم المتطلبات: دلالات ثلاثية القيم مختارة من And/Or/Not بالإضافة إلى حد أولي متميز لمجموعة المتطلبات للأبواب.

TriState: نتيجة التقييم: true (نجاح)، false (فشل)، أو unknown (معلق).

منطق كلين القوي: وضع منطق ثلاثي الحالات حيث And(true, unknown) -> unknown.

أشجار تقييم المتطلبات (RET)

نظرة سريعة

خلفية منخفضة/AOT (RET)

الإدخال في وقت الترجمة مقابل وقت التشغيل

لماذا RET؟

نموذج ذهني: شجرة تقييم RET

نتائج الولايات الثلاث

مشغلات أساسية

و

أو

لا

RequireGroup (نصاب)

شرط (عقدة ورقية)

قواعد انتشار ثلاثي الولايات

و الانتشار

أو انتشار

توزيع RequireGroup

حالات الاستخدام العملية

متطلب بسيط: كلا الشرطين

متطلب النصاب: 2 من 3 مراجعين

متطلب الاستبعاد: غير مدرج في القائمة السوداء

متطلب معقد: (A AND B) OR C

RET في طوبولوجيا Monotone-DAG

أوضاع المنطق

حالات الاستخدام

استكشاف الأخطاء وإصلاحها

المشكلة: البوابة عالقة في unknown

المشكلة: RequireGroup لا تنجح أبداً

المشكلة: لم يتم فتح شقيق جاهز تلقائيًا

نصائح التأليف

مسارات التعلم المتقاطعة

معجم

المشكلة: البوابة عالقة في `unknown`