Verifizierungsprüfungen

Nach der Kompression führt lean-ctx deterministische Prüfungen durch, um sicherzustellen, dass keine kritischen Informationen verloren gingen.

Pfad-Verankerung

Extrahiert Dateipfade aus der originalen Ausgabe und prüft deren Erhalt in der komprimierten Version.

Bezeichner-Prüfung

Erkennt Funktionsnamen, Struct-Namen und andere Code-Bezeichner und prüft deren Erhalt. Bezeichner >= 8 Zeichen werden als hoch-schwerwiegend eingestuft.

Zeilennummer-Konsistenz

Wenn Zeilennummern referenziert werden, wird geprüft, ob sie die tatsächliche Zeilenanzahl der Quelldatei nicht überschreiten.

Strukturelle Integrität

Prüft, ob Code-Blöcke balancierte Klammern haben. Eine Differenz > 2 deutet auf abgeschnittene Ausgabe hin.

Konfiguration

Die Verifizierung ist pro Profil konfigurierbar. Einzelne Prüftypen können je nach Anwendungsfall aktiviert werden.

# 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

Ergebnis-Format

Bei Warnungen wird eine [VERIFY]-Zeile an die Tool-Ausgabe angehängt.

[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

Intent-basiertes Model-Routing

lean-ctx klassifiziert jede Aufgabe in drei Dimensionen (What, How, Do) und empfiehlt eine Modellstufe.

Routing-Dimensionen

ctx_intent-Ausgabe

Das ctx_intent-Tool gibt nun die empfohlene Modellstufe zusammen mit der Intent-Klassifikation zurück.

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

Adaptive ML-Kompression

lean-ctx nutzt Thompson Sampling, um optimale Kompressionsschwellen pro Sprache und Dateityp zu lernen.

Thompson-Sampling-Bandits

Drei Bandit-Arme (konservativ, ausgewogen, aggressiv) konkurrieren mit unterschiedlichen Schwellenwerten.

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

Feedback-Schleife

Jedes Kompressionsergebnis fließt in das Bandit-System zurück. Periodischer Decay verhindert, dass veraltete Daten dominieren.

Dashboard-API

Zugriff auf Verifizierungsstatistiken und Prometheus-Metriken über die Dashboard-API.

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

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