Skip to main content

lean_ctx/
instructions.rs

1use crate::core::config::CompressionLevel;
2use crate::core::rules_canonical::{self as rc, Wrapper};
3use crate::tools::CrpMode;
4
5/// Universal instruction cap for all MCP clients (in tokens, not bytes).
6const INSTRUCTION_CAP_TOKENS: usize = 800;
7
8/// Token budget for the static instruction skeleton (no session/knowledge
9/// state).  Asserted in CI so instruction creep cannot silently tax every
10/// session. Measured at compression `Off` (the test pins `LEAN_CTX_COMPRESSION=off`)
11/// so the budget is deterministic across dev machines, not just clean CI (#498).
12/// Raised in reviewed steps: 520→540 / 600→640 for the sharpened ctx_* redirects
13/// (#1030), then 540→590 / 640→680 (#609 loop one-liner), then 590→615 / 680→712
14/// (proactive `RECOVER` line). Lowered 615→545 / 712→675 by the v5 rules diet
15/// (#578): the COMPACT skeleton folded loop/paradox into INTENT (measured ~505 /
16/// ~639 + headroom). Clients whose rule file already carries the canonical block
17/// get a one-line anchor instead of the skeleton (`client_loads_rules_from_file`)
18/// and land far below even this.
19#[cfg(test)]
20const STATIC_INSTRUCTION_BUDGET_TOKENS: usize = 545;
21#[cfg(test)]
22const STATIC_INSTRUCTION_BUDGET_TDD_TOKENS: usize = 675;
23/// Windows carries a one-line SHELL hint inside the skeleton.
24#[cfg(all(test, windows))]
25const STATIC_INSTRUCTION_SHELL_HINT_TOKENS: usize = 25;
26#[cfg(all(test, not(windows)))]
27const STATIC_INSTRUCTION_SHELL_HINT_TOKENS: usize = 0;
28
29#[must_use]
30pub fn build_instructions(crp_mode: CrpMode) -> String {
31    build_instructions_with_client(crp_mode, "")
32}
33
34#[must_use]
35pub fn build_instructions_with_client(crp_mode: CrpMode, client_name: &str) -> String {
36    let cfg = crate::core::config::Config::load();
37    let minimal = cfg.minimal_overhead_effective_for_client(client_name);
38    let shadow = cfg.shadow_mode;
39    // Cross-channel dedup: if the client auto-loads compression from its own rule
40    // file, skip it here to avoid duplicate billing.
41    let level = if client_loads_compression_from_file(client_name) {
42        CompressionLevel::Off
43    } else {
44        CompressionLevel::effective(&cfg)
45    };
46    build_full_instructions(crp_mode, client_name, minimal, level, shadow)
47}
48
49/// Deterministic STATIC Claude Code instructions for the char-budget test: the
50/// cold first-contact handshake surface (skeleton + shell hint + decoder +
51/// CLAUDE.md pointer + guidance). It pins `minimal=true` (the dynamic
52/// session/knowledge/gotcha payload is governed by `INSTRUCTION_CAP_TOKENS`, not
53/// the char budget) plus `level=Off`, `shadow=false` (the default template), so
54/// the result is independent of the developer's local lean-ctx config and the
55/// assertion stays deterministic (#498) for every contributor, not just clean CI.
56#[must_use]
57pub fn claude_code_static_instructions_for_test() -> String {
58    build_full_instructions(CrpMode::Off, "", true, CompressionLevel::Off, false)
59}
60
61/// Deterministic variant for tests (no session/knowledge state).
62#[must_use]
63pub fn build_instructions_for_test(crp_mode: CrpMode) -> String {
64    let shadow = false;
65    // Resolve the effective compression level from config/env (matches the live
66    // build_full_instructions path) so terse/compression env vars are honoured.
67    let level = CompressionLevel::effective(&crate::core::config::Config::load());
68    let skeleton = rc::render(shadow, Wrapper::Bare, level);
69    let shell_hint = build_shell_hint();
70
71    let base = format!(
72        "{skeleton}\n\
73        {shell_hint}\n\
74        {decoder_block}\n\
75        {origin}",
76        decoder_block =
77            crate::core::protocol::instruction_decoder_block(matches!(crp_mode, CrpMode::Tdd)),
78        origin = crate::core::integrity::origin_line(),
79    );
80
81    match crp_mode_suffix(crp_mode) {
82        "" => format!("{base}\n\n{}", rc::INTELLIGENCE),
83        crp => format!("{base}\n\n{crp}\n\n{}", rc::INTELLIGENCE),
84    }
85}
86
87/// Deterministic instruction builder for the Instruction Compiler.
88/// Uses shadow mode (COMPACT_SHADOW profile) to avoid duplicating
89/// BULLETS/NEVER/CRITICAL that the CLAUDE.md / dedicated rule file carries.
90#[must_use]
91pub fn build_instructions_with_client_for_compiler(
92    crp_mode: CrpMode,
93    client_name: &str,
94    _unified_tool_mode: bool,
95) -> String {
96    let skeleton = rc::render(true, Wrapper::Bare, CompressionLevel::Off);
97    let shell_hint = build_shell_hint();
98
99    let base = format!(
100        "{skeleton}\n\
101        {shell_hint}\n\
102        {decoder_block}\n\
103        {origin}",
104        decoder_block =
105            crate::core::protocol::instruction_decoder_block(matches!(crp_mode, CrpMode::Tdd)),
106        origin = crate::core::integrity::origin_line(),
107    );
108
109    let _ = client_name;
110
111    match crp_mode_suffix(crp_mode) {
112        "" => format!("{base}\n\n{}", rc::INTELLIGENCE),
113        crp => format!("{base}\n\n{crp}\n\n{}", rc::INTELLIGENCE),
114    }
115}
116
117/// LITM calibration manifest rotation (#539).
118fn rotate_wakeup_manifest(session: &crate::core::session::SessionState, profile_name: &str) {
119    use crate::core::litm_calibration::{Position, record_outcome};
120    use crate::core::session::ManifestEntry;
121
122    let mut updated = session.clone();
123
124    for entry in &updated.wakeup_manifest {
125        if !entry.missed
126            && let Some(pos) = Position::parse(&entry.position)
127        {
128            record_outcome(&entry.profile, pos, true);
129        }
130    }
131
132    let mut manifest: Vec<ManifestEntry> = Vec::new();
133    let mut push = |key: &str, position: &str| {
134        let key = key.trim();
135        if !key.is_empty() {
136            manifest.push(ManifestEntry {
137                key: key.chars().take(80).collect(),
138                position: position.to_string(),
139                profile: profile_name.to_string(),
140                missed: false,
141            });
142        }
143    };
144
145    if let Some(ref task) = updated.task {
146        push(&task.description, "begin");
147    }
148    for d in updated.decisions.iter().rev().take(5) {
149        push(&d.summary, "begin");
150    }
151    for f in updated.findings.iter().rev().take(8) {
152        push(&f.summary, "end");
153    }
154    for n in updated.next_steps.iter().take(3) {
155        push(n, "end");
156    }
157
158    updated.wakeup_manifest = manifest;
159    let _ = updated.save();
160}
161
162/// Display path for the Claude config directory (respected by CLAUDE_CONFIG_DIR).
163#[must_use]
164pub fn claude_config_dir_display() -> String {
165    match std::env::var("CLAUDE_CONFIG_DIR") {
166        Ok(dir) if !dir.trim().is_empty() => {
167            let dir = dir.trim().to_string();
168            if dir.starts_with('~') {
169                dir
170            } else if let Some(home) = dirs::home_dir() {
171                let home_str = home.to_string_lossy();
172                if let Some(rest) = dir.strip_prefix(home_str.as_ref()) {
173                    format!("~{rest}")
174                } else {
175                    dir
176                }
177            } else {
178                dir
179            }
180        }
181        _ => "~/.claude".to_string(),
182    }
183}
184
185// ── MCP per-session instructions builder ──────────────────────
186
187fn build_full_instructions(
188    crp_mode: CrpMode,
189    client_name: &str,
190    minimal: bool,
191    level: CompressionLevel,
192    shadow: bool,
193) -> String {
194    let profile = crate::core::litm::LitmProfile::from_client_name(client_name);
195    let loaded_session = if minimal {
196        None
197    } else {
198        crate::core::session::SessionState::load_latest()
199    };
200
201    let (session_block, litm_end_block) = match loaded_session {
202        Some(ref session) => {
203            rotate_wakeup_manifest(session, profile.name);
204            let share = crate::core::litm_calibration::begin_share(profile.name);
205            let mut positioned = crate::core::litm::position_optimize_with_share(session, share);
206            // #962: hard token ceiling so the re-injected ACTIVE SESSION block can
207            // never crowd out the user's task (deterministic, generous default).
208            positioned.enforce_token_budget(crate::core::litm::active_session_budget());
209            let begin = format!(
210                "\n\n--- ACTIVE SESSION (LITM P1: begin position, profile: {}) ---\n{}\n---\n",
211                profile.name, positioned.begin_block
212            );
213            let end = if positioned.end_block.is_empty() {
214                String::new()
215            } else {
216                format!(
217                    "\n--- SESSION RESUME (post-compaction) ---\n{}\n---\n",
218                    positioned.end_block
219                )
220            };
221            (begin, end)
222        }
223        None => (String::new(), String::new()),
224    };
225
226    let project_root_for_blocks = if minimal {
227        None
228    } else {
229        loaded_session
230            .as_ref()
231            .and_then(|s| s.project_root.clone())
232            .or_else(|| {
233                std::env::current_dir()
234                    .ok()
235                    .map(|p| p.to_string_lossy().to_string())
236            })
237    };
238
239    let knowledge_block = match &project_root_for_blocks {
240        Some(root) => {
241            let knowledge = crate::core::knowledge::ProjectKnowledge::load(root);
242            match knowledge {
243                Some(k) if !k.facts.is_empty() || !k.patterns.is_empty() => {
244                    let aaak = k.format_aaak();
245                    if aaak.is_empty() {
246                        String::new()
247                    } else {
248                        format!("\n--- PROJECT MEMORY (AAAK) ---\n{}\n---\n", aaak.trim())
249                    }
250                }
251                _ => String::new(),
252            }
253        }
254        None => String::new(),
255    };
256
257    let gotcha_block = match &project_root_for_blocks {
258        Some(root) => {
259            let store = crate::core::gotcha_tracker::GotchaStore::load(root);
260            let files: Vec<String> = loaded_session
261                .as_ref()
262                .map(|s| s.files_touched.iter().map(|ft| ft.path.clone()).collect())
263                .unwrap_or_default();
264            let block = store.format_injection_block(&files);
265            if block.is_empty() {
266                String::new()
267            } else {
268                format!("\n{block}\n")
269            }
270        }
271        None => String::new(),
272    };
273
274    let health_block = match &project_root_for_blocks {
275        Some(root) => {
276            let block = crate::core::code_health::persist::format_session_block(root);
277            if block.is_empty() {
278                String::new()
279            } else {
280                format!("\n{block}\n")
281            }
282        }
283        None => String::new(),
284    };
285
286    let shell_hint = build_shell_hint();
287
288    // Skeleton includes tool-mapping rules + compression prompt (if level active).
289    // Shadow mode omits BULLETS/NEVER/CRITICAL automatically.
290    //
291    // Cross-channel dedup (#578): when the client's own auto-loaded rule file
292    // already carries the canonical rules block (Cursor mdc, Codex
293    // instructions.md), repeating the skeleton here would bill the same
294    // guidance twice on every session. A one-line anchor keeps the binding;
295    // the compression payload is deduped separately via `level` above.
296    //
297    // Hook-covered hosts (GL #1153) get the hook-aware anchor: repeating
298    // "ctx_* replaces native tools" to a Cursor whose hooks already compress
299    // the native calls re-creates exactly the instruction dissonance the
300    // HookCovered rule profile removes.
301    let skeleton = if client_loads_rules_from_file(client_name) {
302        let anchor = if client_is_hook_covered(client_name) {
303            HOOK_COVERED_ANCHOR
304        } else {
305            SKELETON_ANCHOR
306        };
307        let compression = rc::compression_text(level);
308        if compression.is_empty() {
309            anchor.to_string()
310        } else {
311            format!("{anchor}\n{compression}")
312        }
313    } else {
314        rc::render(shadow, Wrapper::Bare, level)
315    };
316
317    // Pointer to the full rule file (honours CLAUDE_CONFIG_DIR): agents load the
318    // detailed instructions on demand from there instead of inlining them.
319    let config_dir = claude_config_dir_display();
320
321    let base = format!(
322        "{skeleton}\n\
323        {shell_hint}\n\
324        {decoder_block}\n\
325        Full instructions at {config_dir}/CLAUDE.md\n\
326        {session_block}\n\
327        {knowledge_block}\n\
328        {gotcha_block}\n\
329        {health_block}\n\
330        {origin}\n\
331        {litm_end_block}",
332        decoder_block =
333            crate::core::protocol::instruction_decoder_block(matches!(crp_mode, CrpMode::Tdd)),
334        origin = crate::core::integrity::origin_line(),
335        litm_end_block = litm_end_block
336    );
337
338    // Guidance suffix: CRP mode + general output rule.
339    // This is the operational contract — protected from truncation.
340    let guidance_suffix = match crp_mode_suffix(crp_mode) {
341        "" => rc::INTELLIGENCE.to_string(),
342        crp => format!("{crp}\n\n{}", rc::INTELLIGENCE),
343    };
344
345    assemble_within_cap(&base, &guidance_suffix, INSTRUCTION_CAP_TOKENS)
346}
347
348fn crp_mode_suffix(crp_mode: CrpMode) -> &'static str {
349    match crp_mode {
350        CrpMode::Off => "",
351        CrpMode::Compact => {
352            "CRP MODE: compact — omit filler; abbreviate fn,cfg,impl,deps,req,res; \
353             diff lines (+/-) only; <=200 tok; trust tool outputs."
354        }
355        CrpMode::Tdd => {
356            "CRP MODE: tdd — max density; Fn refs + diff lines only \
357             (+F1:42 | -F1:10-15 | ~F1:42 old->new); <=150 tok; zero narration."
358        }
359    }
360}
361
362fn assemble_within_cap(base: &str, suffix: &str, cap_tokens: usize) -> String {
363    use crate::core::tokens::count_tokens;
364    let suffix = suffix.trim_end_matches('\n');
365    if suffix.is_empty() {
366        let full = base.to_string();
367        return if count_tokens(&full) > cap_tokens {
368            truncate_to_token_cap(&full, cap_tokens)
369        } else {
370            full
371        };
372    }
373
374    let full = format!("{base}\n\n{suffix}");
375    if count_tokens(&full) <= cap_tokens {
376        return full;
377    }
378
379    let suffix_tokens = count_tokens(suffix);
380    let Some(base_budget) = cap_tokens.checked_sub(suffix_tokens + 1) else {
381        return truncate_to_token_cap(&full, cap_tokens);
382    };
383    let trimmed_base = truncate_to_token_cap(base, base_budget);
384    format!("{trimmed_base}\n\n{suffix}")
385}
386
387fn truncate_to_token_cap(s: &str, cap_tokens: usize) -> String {
388    use crate::core::tokens::count_tokens;
389    if count_tokens(s) <= cap_tokens {
390        return s.to_string();
391    }
392    let cuts: Vec<usize> = s.match_indices('\n').map(|(i, _)| i).collect();
393    let (mut lo, mut hi) = (0usize, cuts.len());
394    let mut best: Option<usize> = None;
395    while lo < hi {
396        let mid = lo + (hi - lo) / 2;
397        let end = cuts[mid];
398        if end > 0 && count_tokens(&s[..end]) <= cap_tokens {
399            best = Some(end);
400            lo = mid + 1;
401        } else {
402            hi = mid;
403        }
404    }
405    if let Some(end) = best {
406        return s[..end].to_string();
407    }
408    let byte_approx = cap_tokens * 4;
409    let safe = s.floor_char_boundary(byte_approx.min(s.len()));
410    s[..safe].to_string()
411}
412
413/// Backward-compat alias kept for external callers.
414#[must_use]
415pub fn claude_code_instructions() -> String {
416    build_instructions(CrpMode::Off)
417}
418
419/// One-line replacement for the full rules skeleton when the client already
420/// auto-loads the canonical block from its own rule file (#578). Anchors the
421/// binding ("the rules you loaded apply to THIS server") without re-billing
422/// the guidance.
423const SKELETON_ANCHOR: &str = "lean-ctx active — your auto-loaded lean-ctx rules apply: \
424    ctx_* tools replace native Read/Grep/Shell/Glob (ctx_compose first).";
425
426/// The anchor for hook-covered hosts (GL #1153): consistent with the
427/// HookCovered rule profile — native tools are fine (the hooks compress
428/// them), the MCP call is for the exclusive capabilities.
429const HOOK_COVERED_ANCHOR: &str = "lean-ctx active — hooks compress native Shell/Read/Grep \
430    transparently; call ctx_compose to orient, ctx_semantic_search / ctx_knowledge for \
431    meaning & memory.";
432
433fn client_loads_compression_from_file(client_name: &str) -> bool {
434    crate::core::home::resolve_home_dir().is_some_and(|home| {
435        crate::core::rules_channel::client_autoloads_compression(client_name, &home)
436    })
437}
438
439fn client_loads_rules_from_file(client_name: &str) -> bool {
440    crate::core::home::resolve_home_dir()
441        .is_some_and(|home| crate::core::rules_channel::client_autoloads_rules(client_name, &home))
442}
443
444fn client_is_hook_covered(client_name: &str) -> bool {
445    crate::core::home::resolve_home_dir()
446        .is_some_and(|home| crate::core::rules_channel::client_hook_covered(client_name, &home))
447}
448
449fn build_shell_hint() -> String {
450    if !cfg!(windows) {
451        return String::new();
452    }
453    let name = crate::shell::shell_name();
454    let is_posix = matches!(name.as_str(), "bash" | "sh" | "zsh" | "fish");
455    if is_posix {
456        format!("\nSHELL: {name} (POSIX) — no PowerShell cmdlets.\n")
457    } else if name.contains("powershell") || name.contains("pwsh") {
458        format!("\nSHELL: {name}. Use PowerShell cmdlets.\n")
459    } else {
460        format!("\nSHELL: {name}.\n")
461    }
462}
463
464#[cfg(test)]
465mod tests {
466    use super::*;
467    use crate::core::tokens::count_tokens;
468
469    #[test]
470    fn guidance_suffix_survives_oversized_base() {
471        let base = "SESSION LINE\n".repeat(4000);
472        let suffix = "OUTPUT STYLE: expert-terse\nFn refs only, diff lines only.";
473        let out = assemble_within_cap(&base, suffix, INSTRUCTION_CAP_TOKENS);
474        assert!(out.contains("OUTPUT STYLE: expert-terse"));
475        assert!(count_tokens(&out) <= INSTRUCTION_CAP_TOKENS);
476        assert!(out.len() < base.len());
477    }
478
479    #[test]
480    fn empty_client_never_dedups_compression() {
481        assert!(!client_loads_compression_from_file(""));
482        assert!(!client_loads_compression_from_file("totally-unknown-agent"));
483    }
484
485    #[test]
486    fn covered_client_gets_anchor_instead_of_skeleton() {
487        // #578: a client whose rule file carries the canonical block must not
488        // pay for the full skeleton again in every MCP session.
489        let _guard = crate::core::data_dir::test_env_lock();
490        let tmp = tempfile::tempdir().unwrap();
491        let home = tmp.path();
492        std::fs::create_dir_all(home.join(".cursor/rules")).unwrap();
493        std::fs::write(
494            home.join(".cursor/rules/lean-ctx.mdc"),
495            rc::render(
496                false,
497                Wrapper::Dedicated,
498                crate::core::config::CompressionLevel::Standard,
499            ),
500        )
501        .unwrap();
502        let old_home = std::env::var("HOME").ok();
503        crate::test_env::set_var("HOME", home);
504        crate::test_env::set_var("LEAN_CTX_MINIMAL", "1");
505
506        let covered = build_instructions_with_client(CrpMode::Off, "cursor");
507        let uncovered = build_instructions_with_client(CrpMode::Off, "some-other-agent");
508
509        if let Some(h) = old_home {
510            crate::test_env::set_var("HOME", h);
511        } else {
512            crate::test_env::remove_var("HOME");
513        }
514        crate::test_env::remove_var("LEAN_CTX_MINIMAL");
515
516        assert!(
517            covered.contains(SKELETON_ANCHOR),
518            "covered client must get the anchor:\n{covered}"
519        );
520        assert!(
521            !covered.contains("MANDATORY MAPPING"),
522            "covered client must not re-pay the skeleton:\n{covered}"
523        );
524        // The mdc also carries the compression block → level dedups to Off.
525        assert!(
526            !covered.contains("OUTPUT STYLE:"),
527            "covered client must not re-pay the compression prompt:\n{covered}"
528        );
529        assert!(
530            uncovered.contains("MANDATORY MAPPING"),
531            "uncovered client keeps the full skeleton:\n{uncovered}"
532        );
533        eprintln!(
534            "instructions footprint: covered={} tok, uncovered={} tok",
535            count_tokens(&covered),
536            count_tokens(&uncovered)
537        );
538        assert!(
539            count_tokens(&covered) < count_tokens(&uncovered),
540            "anchor path must be strictly cheaper"
541        );
542    }
543
544    #[test]
545    fn hook_covered_client_gets_hook_aware_anchor() {
546        // GL #1153: with lean-ctx hooks covering the native tools, the anchor
547        // must not repeat "ctx_* replaces native tools" — that is exactly the
548        // instruction dissonance the HookCovered profile removes.
549        let _guard = crate::core::data_dir::test_env_lock();
550        let tmp = tempfile::tempdir().unwrap();
551        let home = tmp.path();
552        std::fs::create_dir_all(home.join(".cursor/rules")).unwrap();
553        std::fs::write(
554            home.join(".cursor/rules/lean-ctx.mdc"),
555            rc::render(
556                false,
557                Wrapper::HookCovered,
558                crate::core::config::CompressionLevel::Off,
559            ),
560        )
561        .unwrap();
562        std::fs::write(
563            home.join(".cursor/hooks.json"),
564            r#"{"version":1,"hooks":{"preToolUse":[
565                {"matcher":"Shell","command":"/usr/local/bin/lean-ctx hook rewrite"},
566                {"matcher":"Read|Grep","command":"/usr/local/bin/lean-ctx hook redirect"}
567            ]}}"#,
568        )
569        .unwrap();
570        let old_home = std::env::var("HOME").ok();
571        crate::test_env::set_var("HOME", home);
572        crate::test_env::set_var("LEAN_CTX_MINIMAL", "1");
573
574        let covered = build_instructions_with_client(CrpMode::Off, "cursor");
575
576        if let Some(h) = old_home {
577            crate::test_env::set_var("HOME", h);
578        } else {
579            crate::test_env::remove_var("HOME");
580        }
581        crate::test_env::remove_var("LEAN_CTX_MINIMAL");
582
583        assert!(
584            covered.contains(HOOK_COVERED_ANCHOR),
585            "hook-covered client must get the hook-aware anchor:\n{covered}"
586        );
587        assert!(
588            !covered.contains(SKELETON_ANCHOR) && !covered.contains("MANDATORY MAPPING"),
589            "hook-covered client must not carry the replace-native wording:\n{covered}"
590        );
591    }
592
593    #[test]
594    fn under_cap_keeps_everything() {
595        let base = "tool mapping block";
596        let suffix = "OUTPUT STYLE: dense";
597        let out = assemble_within_cap(base, suffix, INSTRUCTION_CAP_TOKENS);
598        assert!(out.contains(base));
599        assert!(out.contains(suffix));
600    }
601
602    #[test]
603    fn empty_suffix_caps_base_only() {
604        let base = "x\n".repeat(4000);
605        let out = assemble_within_cap(&base, "", INSTRUCTION_CAP_TOKENS);
606        assert!(count_tokens(&out) <= INSTRUCTION_CAP_TOKENS);
607    }
608
609    #[cfg(windows)]
610    #[test]
611    fn shell_hint_stays_within_its_budget() {
612        let hint = build_shell_hint();
613        let tokens = count_tokens(&hint);
614        assert!(
615            tokens <= STATIC_INSTRUCTION_SHELL_HINT_TOKENS,
616            "shell hint = {tokens} tok, budget {STATIC_INSTRUCTION_SHELL_HINT_TOKENS}: {hint}"
617        );
618    }
619
620    #[test]
621    fn minimal_overhead_instructions_stay_within_budget() {
622        const MINIMAL_INSTRUCTION_BUDGET_TOKENS: usize =
623            STATIC_INSTRUCTION_BUDGET_TDD_TOKENS + STATIC_INSTRUCTION_SHELL_HINT_TOKENS;
624        let _iso = crate::core::data_dir::isolated_data_dir();
625        crate::test_env::set_var("LEAN_CTX_MINIMAL", "1");
626        let out = build_instructions(CrpMode::Compact);
627        crate::test_env::remove_var("LEAN_CTX_MINIMAL");
628        let tokens = count_tokens(&out);
629        assert!(
630            tokens <= MINIMAL_INSTRUCTION_BUDGET_TOKENS,
631            "minimal-overhead instructions = {tokens} tok, budget {MINIMAL_INSTRUCTION_BUDGET_TOKENS}\n---\n{out}\n---"
632        );
633    }
634
635    #[test]
636    fn static_skeleton_stays_within_budget() {
637        let _iso = crate::core::data_dir::isolated_data_dir();
638        // Pin compression Off so the measured skeleton — and thus this budget —
639        // is deterministic regardless of the dev's local compression_level (#498).
640        crate::test_env::set_var("LEAN_CTX_COMPRESSION", "off");
641        for (mode, base_budget) in [
642            (CrpMode::Off, STATIC_INSTRUCTION_BUDGET_TOKENS),
643            (CrpMode::Compact, STATIC_INSTRUCTION_BUDGET_TOKENS),
644            (CrpMode::Tdd, STATIC_INSTRUCTION_BUDGET_TDD_TOKENS),
645        ] {
646            let budget = base_budget + STATIC_INSTRUCTION_SHELL_HINT_TOKENS;
647            let out = build_instructions_for_test(mode);
648            let tokens = count_tokens(&out);
649            assert!(
650                tokens <= budget,
651                "static instructions for {mode:?} = {tokens} tok, budget {budget}\n---\n{out}\n---"
652            );
653        }
654        crate::test_env::remove_var("LEAN_CTX_COMPRESSION");
655    }
656}