البراهين الصورية

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

الاحتفاظ بنتيجة

تدخل نتيجة أي مُحلِّل تحت عقد واحد، هو ملف JSON:

{
  "property": {"id": "transfer-authorized", "notation": "LTL", "statement": "G(transfer -> authorized)"},
  "model": {"digest": "sha256:...", "description": "the agent's tool-permission model"},
  "solver": {"name": "nuXmv", "version": "2.0.0"},
  "assumptions": ["the tool router is the only path to transfer"],
  "outcome": "PROVED",
  "scope": "the permission model, not the deployment",
  "produced_at": "2026-10-19T09:00:00Z"
}

oloproof proofs import result.json

المآل واحد من PROVED أو DISPROVED أو UNKNOWN أو TIMEOUT أو ERROR أو NOT_APPLICABLE، وهو حقل قائم بذاته: ليس حالة قرار أبدًا. يحمل certificate وcounterexample ما أعطاه المُحلِّل، ويحمل timeout_seconds وenvironment كيف جرى. والنتيجة مختومة بمحتواها، فالنسخة المعدَّلة نتيجة أخرى. ويُرفض الملف الذي يخالف العقد برمز الخروج 2، وكذلك produced_at بلا منطقة زمنية أو في المستقبل، وPROVED يحمل مثالًا مضادًا؛ والمخطط هو schemas/v1/proof_result.schema.json.

تشغيل z3

في SMT-LIB، يشغّل Oloproof بنفسه مُحلِّلًا واحدًا، هو z3، حين يكون في PATH لديك (brew install z3 أو apt install z3 أو pip install z3-solver). ويقرّر الملف نفي الخاصية:

oloproof proofs run transfer.smt2 --property transfer-authorized --statement "every transfer is authorized"

تعني unsat أنه لا يوجد مثال مضاد في النموذج: PROVED. وتعني sat أن واحدًا موجود: DISPROVED، مع نموذج z3 مثالًا مضادًا حين يطلبه الملف بـ(get-model). وunknown هي UNKNOWN، والتشغيل الذي يتجاوز --timeout هو TIMEOUT، وكل ما عدا ذلك ERROR: عدة إجابات، أو خطأ بعد الإجابة، أو خروج برمز غير الصفر. والخطأ الوحيد المقبول هو قول z3 إنه لا نموذج متاح بعد unsat، إذ لا نموذج يُعطى. ويعرض oloproof proofs list كل نتيجة يحتفظ بها المشروع.

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

اشتراط برهان

proofs:
  - id: no-unauthorized-transfer
    property: transfer-authorized

يُحسم إدخال proofs: في release.yaml عند كل بوابة على آخر نتيجة وصلت لخاصيته، أو للنموذج الذي يسمّيه model: (بصمة) حين تحدّد واحدًا. التاريخ الذي تحمله النتيجة لا يرتّب شيئًا، فالنتيجة المؤرخة لاحقًا لا تستطيع إخفاء نتيجة وصلت بعدها. وحين تُحفظ DISPROVED للخاصية، تقرؤها القاعدة أيًّا كان ما وصل بعدها، فلا تخفي PROVED لاحقة مثالًا مضادًا أبدًا، ولو كان لنموذج آخر: فبصمة النموذج يكتبها من دفع النتيجة. وللانتقال إلى نموذج مصحَّح، سمِّ بصمته في model:، فتقرأ القاعدة نتائج ذلك النموذج وحدها. PROVED هي PASS وDISPROVED هي FAIL. وأي مآل آخر هو INSUFFICIENT_EVIDENCE بالسبب proof_undecided، وغياب أي نتيجة هو INSUFFICIENT_EVIDENCE بالسبب proof_missing، فالإصدار الذي يشترط برهانًا ينتظره. ويرسله requires_manual_review: true إلى المراجعة أيًّا كان المآل.

أين يظهر

يحمل oloproof push النتائج التي قرأتها البوابة. تحتفظ بها مساحة عملك لكنها لا تستطيع إعادة تشغيل مُحلِّل ولا رؤية نموذجك، لذلك تحجب PASS البرهان بوصفها MANUAL_REVIEW ليقرأها شخص؛ أما FAIL أو INSUFFICIENT_EVIDENCE فيبقى كما هو. ويحمل سجل القرار النتائج التي قرأتها بوابة تشغيله، لا النتائج المستوردة بعده: يعيد record verify قراءة قرار كل قاعدة منها، ويُفشل نتيجةً عُدّلت بعد ختمها، ويعرض النتيجة نفسها على أنها قول الفريق.

إلى أين بعد ذلك

• سجل المخاطر يشرح ما قد يسوء، مما يمكن للبرهان استبعاده في النموذج.
• Gating يشرح كيف توقف القاعدة إصدارًا.