सत्यापन जाँच

संपीड़न के बाद, 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

अनुकूली ML संपीड़न

Thompson Sampling का उपयोग करके इष्टतम संपीड़न सीमाएँ सीखता है।

Thompson Sampling बैंडिट्स

तीन बाँहें (रूढ़िवादी, संतुलित, आक्रामक) विभिन्न सीमाओं के साथ।

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

फ़ीडबैक लूप

प्रत्येक संपीड़न परिणाम बैंडिट सिस्टम में फ़ीड होता है।

डैशबोर्ड API

डैशबोर्ड API के माध्यम से सत्यापन आँकड़ों तक पहुँचें।

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

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