Vérifications de sortie

Après la compression, lean-ctx effectue des vérifications déterministes pour garantir qu'aucune information critique n'a été perdue.

Ancrage des chemins

Extrait les chemins de fichiers de la sortie originale et vérifie leur préservation dans la version compressée.

Vérification des identifiants

Détecte les noms de fonctions et de structures et vérifie leur préservation.

Cohérence des numéros de ligne

Vérifie que les numéros de ligne référencés ne dépassent pas le nombre réel de lignes du fichier source.

Intégrité structurelle

Vérifie que les blocs de code ont des accolades équilibrées.

Configuration

La vérification est configurable par profil.

# 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

Format du résultat

Lorsque des avertissements sont détectés, une ligne [VERIFY] est ajoutée à la sortie.

[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

Routage de modèle basé sur l'intention

lean-ctx classe chaque tâche en trois dimensions (What, How, Do) et recommande un niveau de modèle.

Dimensions de routage

Sortie ctx_intent

L'outil ctx_intent retourne maintenant le niveau de modèle recommandé.

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

Compression ML adaptative

lean-ctx utilise le Thompson Sampling pour apprendre les seuils de compression optimaux.

Bandits Thompson Sampling

Trois bras (conservateur, équilibré, agressif) avec différents seuils.

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

Boucle de rétroaction

Chaque résultat de compression alimente le système de bandits.

API Dashboard

Accédez aux statistiques de vérification via l'API du dashboard.

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

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