فحوصات التحقق

بعد الضغط، يقوم lean-ctx بإجراء فحوصات حتمية لضمان عدم فقدان معلومات مهمة.

تثبيت المسارات

يستخرج مسارات الملفات ويتحقق من حفظها.

فحص المعرفات

يكتشف أسماء الدوال والهياكل ويتحقق من حفظها.

تناسق أرقام السطور

يتحقق من أن أرقام السطور المشار إليها لا تتجاوز العدد الفعلي.

السلامة الهيكلية

يتحقق من توازن الأقواس في كتل الكود.

التكوين

التحقق قابل للتكوين حسب الملف الشخصي.

# Profile-specific verification settings
[verification]
enabled = true
# Optional explicit mode (recommended for clarity):
#   "warn" (default) -> FAIL only on High severity warnings
#   "fail"           -> FAIL on Medium+High warnings (strict)
mode = "warn"
check_paths = true
check_identifiers = true
check_line_numbers = false  # opt-in
check_structure = true

# Legacy alias (still supported):
# strict_mode = true

تنسيق النتيجة

عند اكتشاف تحذيرات، يتم إضافة سطر [VERIFY].

[VERIFY] WARN(mangled_identifier=2, missing_path=1) loss=15.0%
[VERIFY] FAIL(brace_mismatch=1, missing_path=1) loss=40.0%

Proof artifacts (ContextProofV2)

82 Lean4 theorems back the proof system, covering policy invariants (PathJail, Budget, Scope), compression safety, and the terse engine (TerseQuality, TerseEngine).

# MCP
ctx_proof action="export" format="summary"

# CLI
lean-ctx proof --summary

Verification observability (versioned stats)

# MCP
ctx_verify action="stats" format="json"

# CLI
lean-ctx verify --json

توجيه النماذج القائم على النية

يصنف lean-ctx كل مهمة إلى ثلاثة أبعاد ويوصي بمستوى النموذج.

أبعاد التوجيه

مخرجات ctx_intent

يعيد ctx_intent الآن مستوى النموذج الموصى به.

INTENT_OK id=42 type=fix_bug source=heuristic conf=90% subj=file(auth.rs)
| route: dimension=how model_tier=standard reason=fix_bug(how) + complexity -> standard

الضغط التكيفي بالتعلم الآلي

يستخدم عينة طومسون لتعلم عتبات الضغط المثلى.

قطاع طريق طومسون

ثلاثة أذرع (محافظ، متوازن، عدواني) بعتبات مختلفة.

Threshold Bandits (Thompson Sampling):
  rs_feedback (pulls: 120):
    conservative: α=15.2 β=8.1 mean=65% entropy=1.20 jaccard=0.80
    balanced:     α=22.3 β=5.2 mean=81% entropy=0.90 jaccard=0.70
    aggressive:   α=8.4 β=12.0 mean=41% entropy=0.60 jaccard=0.55

حلقة التغذية الراجعة

كل نتيجة ضغط تغذي نظام القطاع.

واجهة برمجة لوحة المعلومات

الوصول إلى إحصائيات التحقق عبر واجهة برمجة لوحة المعلومات.

# Verification stats
curl http://localhost:3179/api/verification

# Prometheus metrics (includes verification counters)
curl http://localhost:3179/metrics | grep verification