Vakyartha documentation

1//! `WorkingSetPlanner` verification harness (docs/design/68-context-engine.md
2//! "Verification", "Probe harness" and "No-cut invariant"): a fixture ledger
3//! of 30 closed turns with mixed prose/tool/card answers, plus one open
4//! turn, planned against a synthetic 13k-token horizon. Zero model calls —
5//! this is deterministic, structural verification of the planner and the
6//! projection it drives, not of what a summarizer would choose to keep.
7
8use std::path::Path;
9
10use vak_context::capacity::{CacheBehaviour, CapacityProfile, Horizon, ProbeProvenance};
11use vak_context::planner::{self, Fidelity};
12use vak_llm::{ContentBlock, Message};
13use vak_session::types::{
14 FrozenContract, MessageRecord, PresentationRecord, PresentationSource, SessionHeader,
15 TurnCardRecord,
16};
17use vak_session::{SessionLog, SessionPath, TurnIndex, WorkingSetPlan};
18
19use crate::scorecard::{ContextScorecard, MetricDirection, QualityMetric};
20
21/// The synthetic horizon this harness plans against (docs/design/68 §"Probe
22/// harness"): small enough that a 30-turn fixture cannot all fit at `Full`,
23/// so the planner's Card/Packet tiers are actually exercised.
24const HORIZON_TOKENS: u64 = 13_000;
25
26/// The "small model" horizon for the two-model replay: tight enough that
27/// the 30-turn fixture cannot even fit every card, so the plan packets the
28/// oldest turns and writes a `Compaction` entry — the state the replay
29/// then re-projects under a large model.
30const REPLAY_SMALL_HORIZON_TOKENS: u64 = 1_500;
31
32fn header(cwd: &Path, session_id: &str) -> SessionHeader {
33 SessionHeader {
34 agent: None,
35 session_id: session_id.into(),
36 created_at: chrono::Utc::now(),
37 cwd: cwd.to_path_buf(),
38 parent_session_id: None,
39 contract_id: None,
40 work_item_id: None,
41 conversation: None,
42 contract: FrozenContract {
43 app_version: "0".into(),
44 provider: "fixture".into(),
45 model: "fixture-model".into(),
46 route_ladder: Vec::new(),
47 route_objective: String::new(),
48 route_annotations: Vec::new(),
49 system_prompt: "sys".into(),
50 permission_mode: "workspace-write".into(),
51 capabilities: Vec::new(),
52 prompt_layers: Vec::new(),
53 },
54 }
55}
56
57fn user_text(text: impl Into<String>) -> MessageRecord {
58 MessageRecord {
59 message: Message::user_text(text),
60 meta: None,
61 }
62}
63
64fn assistant_text(text: impl Into<String>) -> MessageRecord {
65 MessageRecord {
66 message: Message::assistant(vec![ContentBlock::text(text.into())]),
67 meta: None,
68 }
69}
70
71fn assistant_tool_call(id: &str, name: &str, input: serde_json::Value) -> MessageRecord {
72 MessageRecord {
73 message: Message::assistant(vec![ContentBlock::ToolUse {
74 id: id.into(),
75 name: name.into(),
76 input,
77 }]),
78 meta: None,
79 }
80}
81
82fn tool_result(id: &str, content: impl Into<String>) -> MessageRecord {
83 MessageRecord {
84 message: Message {
85 role: vak_llm::Role::User,
86 content: vec![ContentBlock::tool_result(id, content.into())],
87 },
88 meta: None,
89 }
90}
91
92/// The three answer shapes mixed across the fixture's 30 closed turns.
93enum TurnKind {
94 /// Plain Q&A, no tool calls at all.
95 Prose,
96 /// One evidence-producing tool call, then a prose answer that cites it.
97 Tool,
98 /// One evidence-producing tool call, then an emitted card.
99 Card,
100}
101
102/// Builds one closed turn of the given kind and returns its directive
103/// entry id, closing it with a real `TurnCard` (as the turn-close hook
104/// would) so the planner has real `tokens_full`/`tokens_card` to plan
105/// against.
106fn build_closed_turn(log: &mut SessionLog, i: usize, kind: TurnKind) -> Result<String, String> {
107 let turn_id = log
108 .append_message(user_text(format!(
109 "turn {i} directive: please help with task number {i}"
110 )))
111 .map_err(|e| e.to_string())?
112 .id;
113 let narration = match kind {
114 TurnKind::Prose => {
115 let text = format!("turn {i} prose answer with a bit of explanation");
116 log.append_message(assistant_text(text.clone()))
117 .map_err(|e| e.to_string())?;
118 text
119 }
120 TurnKind::Tool => {
121 let call_id = format!("call-{i}");
122 log.append_message(assistant_tool_call(
123 &call_id,
124 "search",
125 serde_json::json!({"query": format!("topic {i}")}),
126 ))
127 .map_err(|e| e.to_string())?;
128 log.append_message(tool_result(
129 &call_id,
130 format!(r#"[{{"title":"Result {i}","url":"https://example.com/{i}"}}]"#),
131 ))
132 .map_err(|e| e.to_string())?;
133 let text = format!("turn {i} answer citing the search result");
134 log.append_message(assistant_text(text.clone()))
135 .map_err(|e| e.to_string())?;
136 text
137 }
138 TurnKind::Card => {
139 let call_id = format!("call-{i}");
140 log.append_message(assistant_tool_call(
141 &call_id,
142 "search",
143 serde_json::json!({"query": format!("topic {i}")}),
144 ))
145 .map_err(|e| e.to_string())?;
146 log.append_message(tool_result(
147 &call_id,
148 format!(r#"[{{"title":"Result {i}","url":"https://example.com/{i}"}}]"#),
149 ))
150 .map_err(|e| e.to_string())?;
151 let card_id = format!("card-{i}");
152 log.append_message(assistant_tool_call(
153 &card_id,
154 "emit_research_card",
155 serde_json::json!({"semantic_type": "research.synthesis"}),
156 ))
157 .map_err(|e| e.to_string())?;
158 log.append_message(tool_result(
159 &card_id,
160 format!(r#"{{"presentation":"pres-{i}","ok":true}}"#),
161 ))
162 .map_err(|e| e.to_string())?;
163 let text = format!("turn {i} narration around the card");
164 log.append_message(assistant_text(text.clone()))
165 .map_err(|e| e.to_string())?;
166 log.append_presentation(PresentationRecord {
167 turn_id: turn_id.clone(),
168 source: PresentationSource::ToolCall {
169 tool_use_id: card_id,
170 },
171 semantic_type: "research.synthesis".into(),
172 skill_id: "skill".into(),
173 skill_version: "1".into(),
174 schema_version: 1,
175 payload: serde_json::json!({"takeaways": [format!("finding {i}")]}),
176 payload_digest: format!("digest-{i}"),
177 derived_from: vec![call_id],
178 title: format!("Card {i}"),
179 identity_digest: format!("Card {i}: finding {i}"),
180 })
181 .map_err(|e| e.to_string())?;
182 text
183 }
184 };
185 let card = TurnIndex::from_log(log)
186 .turn_by_id(&turn_id)
187 .ok_or("turn missing from index right after being written")?
188 .build_card("completed", narration, &|s| s.len() as u64 / 4);
189 log.append_turn_card(TurnCardRecord {
190 turn_id: turn_id.clone(),
191 card,
192 })
193 .map_err(|e| e.to_string())?;
194 Ok(turn_id)
195}
196
197/// Builds the 30-closed-turn-plus-one-open fixture and returns the log plus
198/// the open turn's tool-result content (for the no-cut assertion).
199fn build_fixture(dir: &Path, session_id: &str) -> Result<(SessionLog, String), String> {
200 let cwd = dir.to_path_buf();
201 let home = cwd.join(".vak-home");
202 std::fs::create_dir_all(&home).map_err(|e| e.to_string())?;
203 let mut log = SessionLog::create(
204 SessionPath::new_session_file(&home, &cwd, session_id),
205 header(&cwd, session_id),
206 )
207 .map_err(|e| e.to_string())?;
208
209 for i in 0..30 {
210 let kind = match i % 3 {
211 0 => TurnKind::Prose,
212 1 => TurnKind::Tool,
213 _ => TurnKind::Card,
214 };
215 build_closed_turn(&mut log, i, kind)?;
216 }
217
218 // The still-open 31st turn: a directive plus one dispatched tool call
219 // and its result, no final answer yet — always verbatim, never planned.
220 log.append_message(user_text("open turn: please check the current status"))
221 .map_err(|e| e.to_string())?;
222 log.append_message(assistant_tool_call(
223 "open-call",
224 "bash",
225 serde_json::json!({"command": "echo status"}),
226 ))
227 .map_err(|e| e.to_string())?;
228 let open_tool_result_content = "status: all clear, exit code: 0".to_string();
229 log.append_message(tool_result("open-call", open_tool_result_content.clone()))
230 .map_err(|e| e.to_string())?;
231
232 Ok((log, open_tool_result_content))
233}
234
235fn synthetic_profile() -> CapacityProfile {
236 CapacityProfile::from_probe(
237 HORIZON_TOKENS,
238 None,
239 Horizon {
240 tokens: HORIZON_TOKENS,
241 confidence: 0.9,
242 last_confirmed: std::time::SystemTime::now(),
243 },
244 CacheBehaviour::Unknown,
245 512,
246 ProbeProvenance {
247 probed_at: std::time::SystemTime::now(),
248 rungs: Vec::new(),
249 signals: Vec::new(),
250 metadata_digest: "context-engine-gate".into(),
251 quantisation: None,
252 },
253 )
254}
255
256/// Plans once against the fixture's current chain state, through the same
257/// entry point the agent loop and `/compact` use.
258fn plan_now(log: &SessionLog, profile: &CapacityProfile) -> WorkingSetPlan {
259 planner::plan_for_session(log, profile, 400, 100)
260}
261
262/// Every non-open turn with a card must appear in EXACTLY one place: either
263/// `per_turn` (Full or Card) or inside `packet_range` — never both, never
264/// neither ("never splits a turn").
265fn every_turn_accounted_exactly_once(index: &TurnIndex, plan: &WorkingSetPlan) -> bool {
266 let closed_carded: Vec<&str> = index
267 .turns
268 .iter()
269 .filter(|t| t.closed && t.card.is_some())
270 .map(|t| t.id.as_str())
271 .collect();
272 let position: std::collections::HashMap<&str, usize> = index
273 .turns
274 .iter()
275 .enumerate()
276 .map(|(i, t)| (t.id.as_str(), i))
277 .collect();
278 let packet_bounds = plan.packet_range.as_ref().map(|(first, last)| {
279 (
280 position.get(first.as_str()).copied().unwrap_or(usize::MAX),
281 position.get(last.as_str()).copied().unwrap_or(0),
282 )
283 });
284 let mut seen: std::collections::HashSet<&str> = std::collections::HashSet::new();
285 for (id, _) in &plan.per_turn {
286 if !seen.insert(id.as_str()) {
287 return false; // duplicate: split/double-counted turn
288 }
289 }
290 closed_carded.iter().all(|id| {
291 let in_per_turn = seen.contains(id);
292 let in_packet = packet_bounds.is_some_and(|(lo, hi)| {
293 let pos = position[id];
294 pos >= lo && pos <= hi
295 });
296 in_per_turn ^ in_packet
297 })
298}
299
300/// The no-cut invariant (docs/design/68 "No-cut invariant"): every tool
301/// result in the ledger is either verbatim (the open turn), a digest
302/// carrying its evidence id in its paired `tool_result` (a `Full` turn), or
303/// named in a card/packet — never silently absent and never a raw replay.
304fn no_cut_invariant_holds(log: &SessionLog, index: &TurnIndex, plan: &WorkingSetPlan) -> bool {
305 let messages = log.derive_with_plan(plan);
306 let joined: String = messages
307 .iter()
308 .map(Message::text_content)
309 .collect::<Vec<_>>()
310 .join("\n");
311
312 // `text_content()` strips non-Text blocks, so the verbatim check for a
313 // tool result (a ToolResult block, never Text) has to scan the derived
314 // messages' raw content directly rather than through `joined`.
315 let derived_tool_results: Vec<&str> = messages
316 .iter()
317 .flat_map(|m| m.content.iter())
318 .filter_map(|b| match b {
319 ContentBlock::ToolResult { content, .. } => Some(content.as_str()),
320 _ => None,
321 })
322 .collect();
323 let open_result_verbatim = log
324 .open_turn_verbatim()
325 .iter()
326 .flat_map(|m| m.content.iter())
327 .filter_map(|b| match b {
328 ContentBlock::ToolResult { content, .. } => Some(content.as_str()),
329 _ => None,
330 })
331 .all(|content| derived_tool_results.contains(&content));
332 if !open_result_verbatim {
333 return false;
334 }
335
336 let fidelity_of: std::collections::HashMap<&str, Fidelity> = plan
337 .per_turn
338 .iter()
339 .map(|(id, f)| (id.as_str(), *f))
340 .collect();
341
342 for turn in index.turns.iter().filter(|t| t.closed && t.card.is_some()) {
343 let card = turn.card.as_ref().unwrap_or_else(|| unreachable!());
344 match fidelity_of.get(turn.id.as_str()) {
345 Some(Fidelity::Full) => {
346 // The pair stays; the result is the digest tagged with the
347 // evidence id, never the raw content of a closed turn.
348 for trace in &card.did {
349 let tag = format!("[evidence:{}", trace.evidence_id);
350 let digested = derived_tool_results
351 .iter()
352 .any(|content| content.contains(&tag));
353 let raw = turn
354 .evidence_for(&trace.evidence_id)
355 .map(|evidence| evidence.content);
356 let leaked_raw = raw
357 .as_deref()
358 .map(|raw| derived_tool_results.contains(&raw))
359 .unwrap_or(false);
360 if !digested || leaked_raw {
361 return false;
362 }
363 }
364 }
365 Some(Fidelity::Card) => {
366 let line = card.line(0);
367 for trace in &card.did {
368 if !line.contains(&trace.evidence_id) {
369 return false;
370 }
371 }
372 }
373 Some(Fidelity::Packet) | None => {
374 if joined.contains(&turn.directive.text_content()) {
375 return false; // leaked raw despite being packeted
376 }
377 }
378 }
379 }
380 true
381}
382
383/// Two consecutive steps within the same (still open) turn must share a
384/// prefix digest and step k+1's messages must start with step k's, verbatim
385/// (append-only, docs/design/68 §6/§10).
386fn steps_are_append_only_with_a_stable_prefix(dir: &Path) -> Result<bool, String> {
387 let (mut log, _open_result) = build_fixture(dir, "gate-append-only")?;
388 let profile = synthetic_profile();
389 let system_prefix = "You are vak. Fixed system prompt.";
390 let tools: Vec<vak_llm::ToolDefinition> = vec![vak_llm::ToolDefinition::new(
391 "bash",
392 "Run a shell command.",
393 serde_json::json!({"type": "object"}),
394 )];
395
396 let plan_k = plan_now(&log, &profile);
397 let messages_k = log.derive_with_plan(&plan_k);
398 let digest_k = vak_context::assemble::prefix_digest(system_prefix, &tools);
399
400 log.append_message(assistant_tool_call(
401 "open-call-2",
402 "bash",
403 serde_json::json!({"command": "echo more"}),
404 ))
405 .map_err(|e| e.to_string())?;
406 log.append_message(tool_result("open-call-2", "more: ok"))
407 .map_err(|e| e.to_string())?;
408
409 let plan_k1 = plan_now(&log, &profile);
410 let messages_k1 = log.derive_with_plan(&plan_k1);
411 let digest_k1 = vak_context::assemble::prefix_digest(system_prefix, &tools);
412
413 if digest_k != digest_k1 {
414 return Ok(false);
415 }
416 if messages_k1.len() < messages_k.len() {
417 return Ok(false);
418 }
419 Ok(messages_k
420 .iter()
421 .zip(messages_k1.iter())
422 .all(|(a, b)| a.text_content() == b.text_content()))
423}
424
425/// A profile with the given usable horizon, for the two-model replay.
426fn profile_with_horizon(horizon: u64) -> CapacityProfile {
427 CapacityProfile::from_probe(
428 horizon,
429 None,
430 Horizon {
431 tokens: horizon,
432 confidence: 0.9,
433 last_confirmed: std::time::SystemTime::now(),
434 },
435 CacheBehaviour::Unknown,
436 512,
437 ProbeProvenance {
438 probed_at: std::time::SystemTime::now(),
439 rungs: Vec::new(),
440 signals: Vec::new(),
441 metadata_digest: format!("context-engine-gate-{horizon}"),
442 quantisation: None,
443 },
444 )
445}
446
447/// The two-model replay (docs/design/68-context-engine.md, principle 1 and
448/// §4): the projection is a function of `(ledger, the bound model's
449/// profile)` and nothing else. A session that ran on a small model —
450/// whose plan packeted the oldest turns and wrote a `Compaction` entry for
451/// them — is then bound to a model with a horizon large enough to hold
452/// every turn at `Full`. The large model's plan says `Full` for the turns
453/// the small model packeted, so its projection must carry those turns'
454/// real records, not the small model's packet summary. Then bound back to
455/// the small model, the stored packet is reused (no second summariser
456/// call) and the projection is the same as before the switch. Nothing in
457/// the ledger is ever cut; only the projection changes with the model.
458///
459/// Returns one flag per property so the scorecard can name which one
460/// broke.
461struct ReplayVerdict {
462 /// The large model's plan puts the small model's packeted turns at
463 /// `Full` (the planner is model-driven, not boundary-driven).
464 large_plan_promotes_packeted_turns: bool,
465 /// The large model's projection carries those turns' directives
466 /// verbatim and no `<context_summary>` at all.
467 large_projection_follows_its_plan: bool,
468 /// Bound back to the small model, the packet already stored is reused:
469 /// no compaction is needed and the projection matches the pre-switch
470 /// one byte for byte.
471 small_model_reuses_its_packet: bool,
472}
473
474fn two_model_replay(dir: &Path) -> Result<ReplayVerdict, String> {
475 let (mut log, _open_result) = build_fixture(dir, "gate-two-model-replay")?;
476 let small = profile_with_horizon(REPLAY_SMALL_HORIZON_TOKENS);
477 // Large enough that every closed turn fits at Full with room to spare.
478 let large = profile_with_horizon(2_000_000);
479
480 // 1) The small model runs: its plan packets the oldest turns, and the
481 // agent loop writes the packet (a stand-in summary here; the
482 // summariser's wording is irrelevant to the property).
483 let small_plan = plan_now(&log, &small);
484 let Some((first_packeted, last_packeted)) = small_plan.packet_range.clone() else {
485 return Err(
486 "the small profile must packet at least one turn for the replay to mean anything"
487 .into(),
488 );
489 };
490 if !log.packet_needs_compaction(&first_packeted, &last_packeted) {
491 return Err("a fresh ledger cannot already carry a packet".into());
492 }
493 log.append_incremental_compaction(
494 &first_packeted,
495 &last_packeted,
496 "small-model",
497 "SMALL-MODEL-PACKET".into(),
498 1_000,
499 )
500 .map_err(|e| e.to_string())?;
501 let small_messages_before = log.derive_with_plan(&plan_now(&log, &small));
502 let small_joined_before = small_messages_before
503 .iter()
504 .map(Message::text_content)
505 .collect::<Vec<_>>()
506 .join("\n");
507 if !small_joined_before.contains("SMALL-MODEL-PACKET") {
508 return Err("the small model's own projection must carry its packet".into());
509 }
510
511 let index = TurnIndex::from_log(&log);
512 let position: std::collections::HashMap<&str, usize> = index
513 .turns
514 .iter()
515 .enumerate()
516 .map(|(i, t)| (t.id.as_str(), i))
517 .collect();
518 let lo = position[first_packeted.as_str()];
519 let hi = position[last_packeted.as_str()];
520 let packeted: Vec<&vak_session::Turn> = index.turns[lo..=hi].iter().collect();
521
522 // 2) The same session, now bound to the large model.
523 let large_plan = plan_now(&log, &large);
524 let large_fidelity: std::collections::HashMap<&str, Fidelity> = large_plan
525 .per_turn
526 .iter()
527 .map(|(id, f)| (id.as_str(), *f))
528 .collect();
529 let large_plan_promotes_packeted_turns = large_plan.packet_range.is_none()
530 && packeted
531 .iter()
532 .all(|t| large_fidelity.get(t.id.as_str()) == Some(&Fidelity::Full));
533
534 let large_messages = log.derive_with_plan(&large_plan);
535 let large_joined = large_messages
536 .iter()
537 .map(Message::text_content)
538 .collect::<Vec<_>>()
539 .join("\n");
540 let large_projection_follows_its_plan = !large_joined.contains("<context_summary>")
541 && !large_joined.contains("SMALL-MODEL-PACKET")
542 && packeted
543 .iter()
544 .all(|t| large_joined.contains(&t.directive.text_content()));
545
546 // 3) Back to the small model: the stored packet covers exactly the
547 // range its plan needs again, so nothing is re-summarised and the
548 // projection is unchanged.
549 let small_plan_after = plan_now(&log, &small);
550 let reuses = small_plan_after
551 .packet_range
552 .as_ref()
553 .is_some_and(|(first, last)| !log.packet_needs_compaction(first, last));
554 let small_messages_after = log.derive_with_plan(&small_plan_after);
555 let same_projection = small_messages_before.len() == small_messages_after.len()
556 && small_messages_before
557 .iter()
558 .zip(small_messages_after.iter())
559 .all(|(a, b)| a.text_content() == b.text_content());
560 let small_model_reuses_its_packet = reuses && same_projection;
561
562 Ok(ReplayVerdict {
563 large_plan_promotes_packeted_turns,
564 large_projection_follows_its_plan,
565 small_model_reuses_its_packet,
566 })
567}
568
569/// Runs the planner-verification gate. Zero model calls: every property is
570/// structural, over a fixed 30-turn-plus-open fixture and a synthetic
571/// 13k-token profile (docs/design/68-context-engine.md "Verification").
572pub fn run_context_engine_scorecard() -> Result<ContextScorecard, String> {
573 let dir = tempfile::tempdir().map_err(|e| e.to_string())?;
574 let (log, _open_result) = build_fixture(dir.path(), "gate-budget")?;
575 let profile = synthetic_profile();
576 let plan = plan_now(&log, &profile);
577 let index = TurnIndex::from_log(&log);
578
579 let budget_ok = plan.spent <= plan.budget;
580 let accounted_ok = every_turn_accounted_exactly_once(&index, &plan);
581 let no_cut_ok = no_cut_invariant_holds(&log, &index, &plan);
582 let append_only_ok = steps_are_append_only_with_a_stable_prefix(dir.path())?;
583 let replay = two_model_replay(dir.path())?;
584
585 let metric = |name: &'static str, ok: bool| QualityMetric {
586 name,
587 value: if ok { 1.0 } else { 0.0 },
588 threshold: 1.0,
589 direction: MetricDirection::Min,
590 };
591
592 Ok(ContextScorecard {
593 metrics: vec![
594 metric("plan_never_exceeds_budget", budget_ok),
595 metric("every_turn_accounted_exactly_once", accounted_ok),
596 metric("no_cut_invariant_holds", no_cut_ok),
597 metric("steps_append_only_with_stable_prefix", append_only_ok),
598 metric(
599 "replay_large_plan_promotes_packeted_turns",
600 replay.large_plan_promotes_packeted_turns,
601 ),
602 metric(
603 "replay_large_projection_follows_its_plan",
604 replay.large_projection_follows_its_plan,
605 ),
606 metric(
607 "replay_small_model_reuses_its_packet",
608 replay.small_model_reuses_its_packet,
609 ),
610 ],
611 })
612}
613
614#[cfg(test)]
615#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
616mod tests {
617 use super::*;
618
619 #[test]
620 fn context_engine_scorecard_passes_on_healthy_machinery() {
621 let card = run_context_engine_scorecard().expect("harness");
622 println!("{card}");
623 assert!(card.passed(), "scorecard failed: {card}");
624 }
625
626 /// The two-model replay on its own, so a regression names the exact
627 /// property instead of failing the whole scorecard.
628 #[test]
629 fn projection_is_a_function_of_the_bound_model_not_of_earlier_models() {
630 let dir = tempfile::tempdir().unwrap();
631 let verdict = two_model_replay(dir.path()).expect("replay harness");
632 assert!(
633 verdict.large_plan_promotes_packeted_turns,
634 "the large model's plan must put the small model's packeted turns at Full"
635 );
636 assert!(
637 verdict.large_projection_follows_its_plan,
638 "the large model's projection must carry the packeted turns' records, not the small model's packet"
639 );
640 assert!(
641 verdict.small_model_reuses_its_packet,
642 "bound back to the small model, the stored packet must be reused and the projection unchanged"
643 );
644 }
645}
646

1//! `WorkingSetPlanner` verification harness (docs/design/68-context-engine.md
2//! "Verification", "Probe harness" and "No-cut invariant"): a fixture ledger
3//! of 30 closed turns with mixed prose/tool/card answers, plus one open
4//! turn, planned against a synthetic 13k-token horizon. Zero model calls —
5//! this is deterministic, structural verification of the planner and the
6//! projection it drives, not of what a summarizer would choose to keep.
7
8use std::path::Path;
9
10use vak_context::capacity::{CacheBehaviour, CapacityProfile, Horizon, ProbeProvenance};
11use vak_context::planner::{self, Fidelity};
12use vak_llm::{ContentBlock, Message};
13use vak_session::types::{
14 FrozenContract, MessageRecord, PresentationRecord, PresentationSource, SessionHeader,
15 TurnCardRecord,
16};
17use vak_session::{SessionLog, SessionPath, TurnIndex, WorkingSetPlan};
18
19use crate::scorecard::{ContextScorecard, MetricDirection, QualityMetric};
20
21/// The synthetic horizon this harness plans against (docs/design/68 §"Probe
22/// harness"): small enough that a 30-turn fixture cannot all fit at `Full`,
23/// so the planner's Card/Packet tiers are actually exercised.
24const HORIZON_TOKENS: u64 = 13_000;
25
26/// The "small model" horizon for the two-model replay: tight enough that
27/// the 30-turn fixture cannot even fit every card, so the plan packets the
28/// oldest turns and writes a `Compaction` entry — the state the replay
29/// then re-projects under a large model.
30const REPLAY_SMALL_HORIZON_TOKENS: u64 = 1_500;
31
32fn header(cwd: &Path, session_id: &str) -> SessionHeader {
33 SessionHeader {
34 agent: None,
35 session_id: session_id.into(),
36 created_at: chrono::Utc::now(),
37 cwd: cwd.to_path_buf(),
38 parent_session_id: None,
39 contract_id: None,
40 work_item_id: None,
41 conversation: None,
42 contract: FrozenContract {
43 app_version: "0".into(),
44 provider: "fixture".into(),
45 model: "fixture-model".into(),
46 route_ladder: Vec::new(),
47 route_objective: String::new(),
48 route_annotations: Vec::new(),
49 system_prompt: "sys".into(),
50 permission_mode: "workspace-write".into(),
51 capabilities: Vec::new(),
52 prompt_layers: Vec::new(),
53 },
54 }
55}
56
57fn user_text(text: impl Into<String>) -> MessageRecord {
58 MessageRecord {
59 message: Message::user_text(text),
60 meta: None,
61 }
62}
63
64fn assistant_text(text: impl Into<String>) -> MessageRecord {
65 MessageRecord {
66 message: Message::assistant(vec![ContentBlock::text(text.into())]),
67 meta: None,
68 }
69}
70
71fn assistant_tool_call(id: &str, name: &str, input: serde_json::Value) -> MessageRecord {
72 MessageRecord {
73 message: Message::assistant(vec![ContentBlock::ToolUse {
74 id: id.into(),
75 name: name.into(),
76 input,
77 }]),
78 meta: None,
79 }
80}
81
82fn tool_result(id: &str, content: impl Into<String>) -> MessageRecord {
83 MessageRecord {
84 message: Message {
85 role: vak_llm::Role::User,
86 content: vec![ContentBlock::tool_result(id, content.into())],
87 },
88 meta: None,
89 }
90}
91
92/// The three answer shapes mixed across the fixture's 30 closed turns.
93enum TurnKind {
94 /// Plain Q&A, no tool calls at all.
95 Prose,
96 /// One evidence-producing tool call, then a prose answer that cites it.
97 Tool,
98 /// One evidence-producing tool call, then an emitted card.
99 Card,
100}
101
102/// Builds one closed turn of the given kind and returns its directive
103/// entry id, closing it with a real `TurnCard` (as the turn-close hook
104/// would) so the planner has real `tokens_full`/`tokens_card` to plan
105/// against.
106fn build_closed_turn(log: &mut SessionLog, i: usize, kind: TurnKind) -> Result<String, String> {
107 let turn_id = log
108 .append_message(user_text(format!(
109 "turn {i} directive: please help with task number {i}"
110 )))
111 .map_err(|e| e.to_string())?
112 .id;
113 let narration = match kind {
114 TurnKind::Prose => {
115 let text = format!("turn {i} prose answer with a bit of explanation");
116 log.append_message(assistant_text(text.clone()))
117 .map_err(|e| e.to_string())?;
118 text
119 }
120 TurnKind::Tool => {
121 let call_id = format!("call-{i}");
122 log.append_message(assistant_tool_call(
123 &call_id,
124 "search",
125 serde_json::json!({"query": format!("topic {i}")}),
126 ))
127 .map_err(|e| e.to_string())?;
128 log.append_message(tool_result(
129 &call_id,
130 format!(r#"[{{"title":"Result {i}","url":"https://example.com/{i}"}}]"#),
131 ))
132 .map_err(|e| e.to_string())?;
133 let text = format!("turn {i} answer citing the search result");
134 log.append_message(assistant_text(text.clone()))
135 .map_err(|e| e.to_string())?;
136 text
137 }
138 TurnKind::Card => {
139 let call_id = format!("call-{i}");
140 log.append_message(assistant_tool_call(
141 &call_id,
142 "search",
143 serde_json::json!({"query": format!("topic {i}")}),
144 ))
145 .map_err(|e| e.to_string())?;
146 log.append_message(tool_result(
147 &call_id,
148 format!(r#"[{{"title":"Result {i}","url":"https://example.com/{i}"}}]"#),
149 ))
150 .map_err(|e| e.to_string())?;
151 let card_id = format!("card-{i}");
152 log.append_message(assistant_tool_call(
153 &card_id,
154 "emit_research_card",
155 serde_json::json!({"semantic_type": "research.synthesis"}),
156 ))
157 .map_err(|e| e.to_string())?;
158 log.append_message(tool_result(
159 &card_id,
160 format!(r#"{{"presentation":"pres-{i}","ok":true}}"#),
161 ))
162 .map_err(|e| e.to_string())?;
163 let text = format!("turn {i} narration around the card");
164 log.append_message(assistant_text(text.clone()))
165 .map_err(|e| e.to_string())?;
166 log.append_presentation(PresentationRecord {
167 turn_id: turn_id.clone(),
168 source: PresentationSource::ToolCall {
169 tool_use_id: card_id,
170 },
171 semantic_type: "research.synthesis".into(),
172 skill_id: "skill".into(),
173 skill_version: "1".into(),
174 schema_version: 1,
175 payload: serde_json::json!({"takeaways": [format!("finding {i}")]}),
176 payload_digest: format!("digest-{i}"),
177 derived_from: vec![call_id],
178 title: format!("Card {i}"),
179 identity_digest: format!("Card {i}: finding {i}"),
180 })
181 .map_err(|e| e.to_string())?;
182 text
183 }
184 };
185 let card = TurnIndex::from_log(log)
186 .turn_by_id(&turn_id)
187 .ok_or("turn missing from index right after being written")?
188 .build_card("completed", narration, &|s| s.len() as u64 / 4);
189 log.append_turn_card(TurnCardRecord {
190 turn_id: turn_id.clone(),
191 card,
192 })
193 .map_err(|e| e.to_string())?;
194 Ok(turn_id)
195}
196
197/// Builds the 30-closed-turn-plus-one-open fixture and returns the log plus
198/// the open turn's tool-result content (for the no-cut assertion).
199fn build_fixture(dir: &Path, session_id: &str) -> Result<(SessionLog, String), String> {
200 let cwd = dir.to_path_buf();
201 let home = cwd.join(".vak-home");
202 std::fs::create_dir_all(&home).map_err(|e| e.to_string())?;
203 let mut log = SessionLog::create(
204 SessionPath::new_session_file(&home, &cwd, session_id),
205 header(&cwd, session_id),
206 )
207 .map_err(|e| e.to_string())?;
208
209 for i in 0..30 {
210 let kind = match i % 3 {
211 0 => TurnKind::Prose,
212 1 => TurnKind::Tool,
213 _ => TurnKind::Card,
214 };
215 build_closed_turn(&mut log, i, kind)?;
216 }
217
218 // The still-open 31st turn: a directive plus one dispatched tool call
219 // and its result, no final answer yet — always verbatim, never planned.
220 log.append_message(user_text("open turn: please check the current status"))
221 .map_err(|e| e.to_string())?;
222 log.append_message(assistant_tool_call(
223 "open-call",
224 "bash",
225 serde_json::json!({"command": "echo status"}),
226 ))
227 .map_err(|e| e.to_string())?;
228 let open_tool_result_content = "status: all clear, exit code: 0".to_string();
229 log.append_message(tool_result("open-call", open_tool_result_content.clone()))
230 .map_err(|e| e.to_string())?;
231
232 Ok((log, open_tool_result_content))
233}
234
235fn synthetic_profile() -> CapacityProfile {
236 CapacityProfile::from_probe(
237 HORIZON_TOKENS,
238 None,
239 Horizon {
240 tokens: HORIZON_TOKENS,
241 confidence: 0.9,
242 last_confirmed: std::time::SystemTime::now(),
243 },
244 CacheBehaviour::Unknown,
245 512,
246 ProbeProvenance {
247 probed_at: std::time::SystemTime::now(),
248 rungs: Vec::new(),
249 signals: Vec::new(),
250 metadata_digest: "context-engine-gate".into(),
251 quantisation: None,
252 },
253 )
254}
255
256/// Plans once against the fixture's current chain state, through the same
257/// entry point the agent loop and `/compact` use.
258fn plan_now(log: &SessionLog, profile: &CapacityProfile) -> WorkingSetPlan {
259 planner::plan_for_session(log, profile, 400, 100)
260}
261
262/// Every non-open turn with a card must appear in EXACTLY one place: either
263/// `per_turn` (Full or Card) or inside `packet_range` — never both, never
264/// neither ("never splits a turn").
265fn every_turn_accounted_exactly_once(index: &TurnIndex, plan: &WorkingSetPlan) -> bool {
266 let closed_carded: Vec<&str> = index
267 .turns
268 .iter()
269 .filter(|t| t.closed && t.card.is_some())
270 .map(|t| t.id.as_str())
271 .collect();
272 let position: std::collections::HashMap<&str, usize> = index
273 .turns
274 .iter()
275 .enumerate()
276 .map(|(i, t)| (t.id.as_str(), i))
277 .collect();
278 let packet_bounds = plan.packet_range.as_ref().map(|(first, last)| {
279 (
280 position.get(first.as_str()).copied().unwrap_or(usize::MAX),
281 position.get(last.as_str()).copied().unwrap_or(0),
282 )
283 });
284 let mut seen: std::collections::HashSet<&str> = std::collections::HashSet::new();
285 for (id, _) in &plan.per_turn {
286 if !seen.insert(id.as_str()) {
287 return false; // duplicate: split/double-counted turn
288 }
289 }
290 closed_carded.iter().all(|id| {
291 let in_per_turn = seen.contains(id);
292 let in_packet = packet_bounds.is_some_and(|(lo, hi)| {
293 let pos = position[id];
294 pos >= lo && pos <= hi
295 });
296 in_per_turn ^ in_packet
297 })
298}
299
300/// The no-cut invariant (docs/design/68 "No-cut invariant"): every tool
301/// result in the ledger is either verbatim (the open turn), a digest
302/// carrying its evidence id in its paired `tool_result` (a `Full` turn), or
303/// named in a card/packet — never silently absent and never a raw replay.
304fn no_cut_invariant_holds(log: &SessionLog, index: &TurnIndex, plan: &WorkingSetPlan) -> bool {
305 let messages = log.derive_with_plan(plan);
306 let joined: String = messages
307 .iter()
308 .map(Message::text_content)
309 .collect::<Vec<_>>()
310 .join("\n");
311
312 // `text_content()` strips non-Text blocks, so the verbatim check for a
313 // tool result (a ToolResult block, never Text) has to scan the derived
314 // messages' raw content directly rather than through `joined`.
315 let derived_tool_results: Vec<&str> = messages
316 .iter()
317 .flat_map(|m| m.content.iter())
318 .filter_map(|b| match b {
319 ContentBlock::ToolResult { content, .. } => Some(content.as_str()),
320 _ => None,
321 })
322 .collect();
323 let open_result_verbatim = log
324 .open_turn_verbatim()
325 .iter()
326 .flat_map(|m| m.content.iter())
327 .filter_map(|b| match b {
328 ContentBlock::ToolResult { content, .. } => Some(content.as_str()),
329 _ => None,
330 })
331 .all(|content| derived_tool_results.contains(&content));
332 if !open_result_verbatim {
333 return false;
334 }
335
336 let fidelity_of: std::collections::HashMap<&str, Fidelity> = plan
337 .per_turn
338 .iter()
339 .map(|(id, f)| (id.as_str(), *f))
340 .collect();
341
342 for turn in index.turns.iter().filter(|t| t.closed && t.card.is_some()) {
343 let card = turn.card.as_ref().unwrap_or_else(|| unreachable!());
344 match fidelity_of.get(turn.id.as_str()) {
345 Some(Fidelity::Full) => {
346 // The pair stays; the result is the digest tagged with the
347 // evidence id, never the raw content of a closed turn.
348 for trace in &card.did {
349 let tag = format!("[evidence:{}", trace.evidence_id);
350 let digested = derived_tool_results
351 .iter()
352 .any(|content| content.contains(&tag));
353 let raw = turn
354 .evidence_for(&trace.evidence_id)
355 .map(|evidence| evidence.content);
356 let leaked_raw = raw
357 .as_deref()
358 .map(|raw| derived_tool_results.contains(&raw))
359 .unwrap_or(false);
360 if !digested || leaked_raw {
361 return false;
362 }
363 }
364 }
365 Some(Fidelity::Card) => {
366 let line = card.line(0);
367 for trace in &card.did {
368 if !line.contains(&trace.evidence_id) {
369 return false;
370 }
371 }
372 }
373 Some(Fidelity::Packet) | None => {
374 if joined.contains(&turn.directive.text_content()) {
375 return false; // leaked raw despite being packeted
376 }
377 }
378 }
379 }
380 true
381}
382
383/// Two consecutive steps within the same (still open) turn must share a
384/// prefix digest and step k+1's messages must start with step k's, verbatim
385/// (append-only, docs/design/68 §6/§10).
386fn steps_are_append_only_with_a_stable_prefix(dir: &Path) -> Result<bool, String> {
387 let (mut log, _open_result) = build_fixture(dir, "gate-append-only")?;
388 let profile = synthetic_profile();
389 let system_prefix = "You are vak. Fixed system prompt.";
390 let tools: Vec<vak_llm::ToolDefinition> = vec![vak_llm::ToolDefinition::new(
391 "bash",
392 "Run a shell command.",
393 serde_json::json!({"type": "object"}),
394 )];
395
396 let plan_k = plan_now(&log, &profile);
397 let messages_k = log.derive_with_plan(&plan_k);
398 let digest_k = vak_context::assemble::prefix_digest(system_prefix, &tools);
399
400 log.append_message(assistant_tool_call(
401 "open-call-2",
402 "bash",
403 serde_json::json!({"command": "echo more"}),
404 ))
405 .map_err(|e| e.to_string())?;
406 log.append_message(tool_result("open-call-2", "more: ok"))
407 .map_err(|e| e.to_string())?;
408
409 let plan_k1 = plan_now(&log, &profile);
410 let messages_k1 = log.derive_with_plan(&plan_k1);
411 let digest_k1 = vak_context::assemble::prefix_digest(system_prefix, &tools);
412
413 if digest_k != digest_k1 {
414 return Ok(false);
415 }
416 if messages_k1.len() < messages_k.len() {
417 return Ok(false);
418 }
419 Ok(messages_k
420 .iter()
421 .zip(messages_k1.iter())
422 .all(|(a, b)| a.text_content() == b.text_content()))
423}
424
425/// A profile with the given usable horizon, for the two-model replay.
426fn profile_with_horizon(horizon: u64) -> CapacityProfile {
427 CapacityProfile::from_probe(
428 horizon,
429 None,
430 Horizon {
431 tokens: horizon,
432 confidence: 0.9,
433 last_confirmed: std::time::SystemTime::now(),
434 },
435 CacheBehaviour::Unknown,
436 512,
437 ProbeProvenance {
438 probed_at: std::time::SystemTime::now(),
439 rungs: Vec::new(),
440 signals: Vec::new(),
441 metadata_digest: format!("context-engine-gate-{horizon}"),
442 quantisation: None,
443 },
444 )
445}
446
447/// The two-model replay (docs/design/68-context-engine.md, principle 1 and
448/// §4): the projection is a function of `(ledger, the bound model's
449/// profile)` and nothing else. A session that ran on a small model —
450/// whose plan packeted the oldest turns and wrote a `Compaction` entry for
451/// them — is then bound to a model with a horizon large enough to hold
452/// every turn at `Full`. The large model's plan says `Full` for the turns
453/// the small model packeted, so its projection must carry those turns'
454/// real records, not the small model's packet summary. Then bound back to
455/// the small model, the stored packet is reused (no second summariser
456/// call) and the projection is the same as before the switch. Nothing in
457/// the ledger is ever cut; only the projection changes with the model.
458///
459/// Returns one flag per property so the scorecard can name which one
460/// broke.
461struct ReplayVerdict {
462 /// The large model's plan puts the small model's packeted turns at
463 /// `Full` (the planner is model-driven, not boundary-driven).
464 large_plan_promotes_packeted_turns: bool,
465 /// The large model's projection carries those turns' directives
466 /// verbatim and no `<context_summary>` at all.
467 large_projection_follows_its_plan: bool,
468 /// Bound back to the small model, the packet already stored is reused:
469 /// no compaction is needed and the projection matches the pre-switch
470 /// one byte for byte.
471 small_model_reuses_its_packet: bool,
472}
473
474fn two_model_replay(dir: &Path) -> Result<ReplayVerdict, String> {
475 let (mut log, _open_result) = build_fixture(dir, "gate-two-model-replay")?;
476 let small = profile_with_horizon(REPLAY_SMALL_HORIZON_TOKENS);
477 // Large enough that every closed turn fits at Full with room to spare.
478 let large = profile_with_horizon(2_000_000);
479
480 // 1) The small model runs: its plan packets the oldest turns, and the
481 // agent loop writes the packet (a stand-in summary here; the
482 // summariser's wording is irrelevant to the property).
483 let small_plan = plan_now(&log, &small);
484 let Some((first_packeted, last_packeted)) = small_plan.packet_range.clone() else {
485 return Err(
486 "the small profile must packet at least one turn for the replay to mean anything"
487 .into(),
488 );
489 };
490 if !log.packet_needs_compaction(&first_packeted, &last_packeted) {
491 return Err("a fresh ledger cannot already carry a packet".into());
492 }
493 log.append_incremental_compaction(
494 &first_packeted,
495 &last_packeted,
496 "small-model",
497 "SMALL-MODEL-PACKET".into(),
498 1_000,
499 )
500 .map_err(|e| e.to_string())?;
501 let small_messages_before = log.derive_with_plan(&plan_now(&log, &small));
502 let small_joined_before = small_messages_before
503 .iter()
504 .map(Message::text_content)
505 .collect::<Vec<_>>()
506 .join("\n");
507 if !small_joined_before.contains("SMALL-MODEL-PACKET") {
508 return Err("the small model's own projection must carry its packet".into());
509 }
510
511 let index = TurnIndex::from_log(&log);
512 let position: std::collections::HashMap<&str, usize> = index
513 .turns
514 .iter()
515 .enumerate()
516 .map(|(i, t)| (t.id.as_str(), i))
517 .collect();
518 let lo = position[first_packeted.as_str()];
519 let hi = position[last_packeted.as_str()];
520 let packeted: Vec<&vak_session::Turn> = index.turns[lo..=hi].iter().collect();
521
522 // 2) The same session, now bound to the large model.
523 let large_plan = plan_now(&log, &large);
524 let large_fidelity: std::collections::HashMap<&str, Fidelity> = large_plan
525 .per_turn
526 .iter()
527 .map(|(id, f)| (id.as_str(), *f))
528 .collect();
529 let large_plan_promotes_packeted_turns = large_plan.packet_range.is_none()
530 && packeted
531 .iter()
532 .all(|t| large_fidelity.get(t.id.as_str()) == Some(&Fidelity::Full));
533
534 let large_messages = log.derive_with_plan(&large_plan);
535 let large_joined = large_messages
536 .iter()
537 .map(Message::text_content)
538 .collect::<Vec<_>>()
539 .join("\n");
540 let large_projection_follows_its_plan = !large_joined.contains("<context_summary>")
541 && !large_joined.contains("SMALL-MODEL-PACKET")
542 && packeted
543 .iter()
544 .all(|t| large_joined.contains(&t.directive.text_content()));
545
546 // 3) Back to the small model: the stored packet covers exactly the
547 // range its plan needs again, so nothing is re-summarised and the
548 // projection is unchanged.
549 let small_plan_after = plan_now(&log, &small);
550 let reuses = small_plan_after
551 .packet_range
552 .as_ref()
553 .is_some_and(|(first, last)| !log.packet_needs_compaction(first, last));
554 let small_messages_after = log.derive_with_plan(&small_plan_after);
555 let same_projection = small_messages_before.len() == small_messages_after.len()
556 && small_messages_before
557 .iter()
558 .zip(small_messages_after.iter())
559 .all(|(a, b)| a.text_content() == b.text_content());
560 let small_model_reuses_its_packet = reuses && same_projection;
561
562 Ok(ReplayVerdict {
563 large_plan_promotes_packeted_turns,
564 large_projection_follows_its_plan,
565 small_model_reuses_its_packet,
566 })
567}
568
569/// Runs the planner-verification gate. Zero model calls: every property is
570/// structural, over a fixed 30-turn-plus-open fixture and a synthetic
571/// 13k-token profile (docs/design/68-context-engine.md "Verification").
572pub fn run_context_engine_scorecard() -> Result<ContextScorecard, String> {
573 let dir = tempfile::tempdir().map_err(|e| e.to_string())?;
574 let (log, _open_result) = build_fixture(dir.path(), "gate-budget")?;
575 let profile = synthetic_profile();
576 let plan = plan_now(&log, &profile);
577 let index = TurnIndex::from_log(&log);
578
579 let budget_ok = plan.spent <= plan.budget;
580 let accounted_ok = every_turn_accounted_exactly_once(&index, &plan);
581 let no_cut_ok = no_cut_invariant_holds(&log, &index, &plan);
582 let append_only_ok = steps_are_append_only_with_a_stable_prefix(dir.path())?;
583 let replay = two_model_replay(dir.path())?;
584
585 let metric = |name: &'static str, ok: bool| QualityMetric {
586 name,
587 value: if ok { 1.0 } else { 0.0 },
588 threshold: 1.0,
589 direction: MetricDirection::Min,
590 };
591
592 Ok(ContextScorecard {
593 metrics: vec![
594 metric("plan_never_exceeds_budget", budget_ok),
595 metric("every_turn_accounted_exactly_once", accounted_ok),
596 metric("no_cut_invariant_holds", no_cut_ok),
597 metric("steps_append_only_with_stable_prefix", append_only_ok),
598 metric(
599 "replay_large_plan_promotes_packeted_turns",
600 replay.large_plan_promotes_packeted_turns,
601 ),
602 metric(
603 "replay_large_projection_follows_its_plan",
604 replay.large_projection_follows_its_plan,
605 ),
606 metric(
607 "replay_small_model_reuses_its_packet",
608 replay.small_model_reuses_its_packet,
609 ),
610 ],
611 })
612}
613
614#[cfg(test)]
615#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
616mod tests {
617 use super::*;
618
619 #[test]
620 fn context_engine_scorecard_passes_on_healthy_machinery() {
621 let card = run_context_engine_scorecard().expect("harness");
622 println!("{card}");
623 assert!(card.passed(), "scorecard failed: {card}");
624 }
625
626 /// The two-model replay on its own, so a regression names the exact
627 /// property instead of failing the whole scorecard.
628 #[test]
629 fn projection_is_a_function_of_the_bound_model_not_of_earlier_models() {
630 let dir = tempfile::tempdir().unwrap();
631 let verdict = two_model_replay(dir.path()).expect("replay harness");
632 assert!(
633 verdict.large_plan_promotes_packeted_turns,
634 "the large model's plan must put the small model's packeted turns at Full"
635 );
636 assert!(
637 verdict.large_projection_follows_its_plan,
638 "the large model's projection must carry the packeted turns' records, not the small model's packet"
639 );
640 assert!(
641 verdict.small_model_reuses_its_packet,
642 "bound back to the small model, the stored packet must be reused and the projection unchanged"
643 );
644 }
645}
646

Context Engine Gate

Indexing the workspace…

Context Engine Gate