harn-stdlib 0.10.133

Embedded Harn standard library source catalog
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
import {
  CompletionRequirementEvidencePacket,
  CompletionRequirementReport,
  completion_requirement_assessments_schema,
  completion_requirement_contract,
  completion_requirement_ids,
  completion_requirement_report,
} from "std/agent/completion_requirements"
import {
  COMPLETION_JUDGE_GAP_CLASSES,
  CompletionJudgeGapClass,
  __completion_judge_gap_class,
} from "std/agent/judge_internals"

/**
 * Decoded completion decision. The schema admits `done` and `continue` only;
 * an out-of-contract value is preserved verbatim so telemetry can show what
 * the judge actually said, and is treated as a non-veto by the caller.
 */
/**
 * One itemized gap from a refusal.
 *
 * `criterion` is what the gap is against, so the actor can see the whole set it
 * has to satisfy instead of discovering it one refusal at a time.
 * `evidence_quote` is what the judge read to conclude it, checked against the
 * evidence the judge was actually handed.
 */
pub type CompletionJudgeGapItem = {
  criterion: string,
  gap_class: CompletionJudgeGapClass,
  detail: string,
  evidence_quote: string,
  // The requirement-ledger row this gap is against, or "" for unattributed.
  // Constrained at the schema to the ids the ledger handed the judge, and
  // normalized to "" here for anything else, so this is never the product of
  // matching the gap's prose against a row's prose. A judge that cannot name a
  // row says nothing and the run counts it (#8104).
  requirement_id: string,
}

pub type CompletionJudgeVerdict = {
  verdict: string,
  detail: string,
  gap_class: CompletionJudgeGapClass,
  // Every gap the refusal itemized. Empty on an approval and on replies that
  // predate the field, which is why no clause may read "no gaps" as "no
  // objection" without also checking the verdict.
  gaps: list<CompletionJudgeGapItem>,
  // Whether the RAW reply carried a non-blank `gap_class` field at all, before
  // `__completion_judge_gap_class` folds absent, blank, unrecognized, and an
  // explicit `other` into the same normalized value. The normalized value
  // cannot tell those apart; this can, and it is what the contradiction check
  // below keys on.
  gap_declared: bool,
  requirement_report?: CompletionRequirementReport?,
}

/**
 * How much of the judge's `detail` survives the decode boundary.
 *
 * The bound exists so a replayed or older-transport reply cannot carry an
 * unbounded string into feedback and telemetry. It is NOT a prompt-budget
 * control: the evidence projection sitting beside this field in the same
 * receipt runs to several kilobytes.
 *
 * It was 240, which is below the cost of one actionable instruction. A judge
 * detail is written complaint-first and remedy-last ("X is not discriminating,
 * ADJUST the fixture, then rerun the verifier"), so a cut at 240 removed the
 * half the actor needed and kept the half it could not act on. Measured on a
 * live run, four of five refusals were amputated mid-word and the loop spent
 * its whole invocation budget re-raising an objection the actor had never been
 * told how to answer (#8074).
 */
const __COMPLETION_JUDGE_DETAIL_CHAR_LIMIT: int = 1000

/**
 * Appended when `__judge_clamp_completion_detail` actually cuts something.
 *
 * Without it a truncated instruction is indistinguishable from an instruction
 * the judge chose to end there, which is precisely what made #8074 invisible
 * for as long as it was.
 */
const __JUDGE_DETAIL_TRUNCATION_MARKER: string = " [truncated]"

/**
 * Bound the judge's detail without destroying its meaning.
 *
 * Cuts on a word boundary and marks the cut. A single word longer than the
 * whole budget still falls back to a hard character cut, because the bound is
 * the guarantee and the word boundary is only a courtesy.
 *
 * @effects: []
 * @errors: []
 * @api_stability: internal
 * @example: __judge_clamp_completion_detail("short detail")
 */
pub fn __judge_clamp_completion_detail(detail: string) -> string {
  if len(detail) <= __COMPLETION_JUDGE_DETAIL_CHAR_LIMIT {
    return detail
  }
  const marker_cost = len(__JUDGE_DETAIL_TRUNCATION_MARKER)
  const budget = __COMPLETION_JUDGE_DETAIL_CHAR_LIMIT - marker_cost
  let kept = ""
  let stopped = false
  for word in detail.split(" ") {
    if !stopped {
      const candidate = if kept == "" {
        word
      } else {
        kept + " " + word
      }
      if len(candidate) <= budget {
        kept = candidate
      } else {
        stopped = true
      }
    }
  }
  const head = if kept == "" {
    substring(detail, 0, budget)
  } else {
    kept
  }
  return head.trim_end() + __JUDGE_DETAIL_TRUNCATION_MARKER
}

/**
 * Gap classes that name a specific unmet obligation.
 *
 * `other` is deliberately absent. It is the value the schema documents for a
 * `done` verdict, and the value an absent, blank, or unrecognized field decodes
 * to, so a cached or older-pin reply carrying no gap class at all arrives here
 * as `other`. Reading `other` as a named gap would refuse every one of those
 * replies, which is the opposite of the safe direction.
 */
pub const COMPLETION_JUDGE_NAMED_GAP_CLASSES = [
  "missing_artifact",
  "unmet_manner_clause",
  "failed_verification",
  "unresolved_authorization",
]

/**
 * __judge_completion_verdict_contradicts_itself.
 *
 * Whether a decoded verdict accepts and refuses in the same object: `done`
 * beside ANY declared gap. The pair is checkable without a model, and a judge
 * that produces it has not decided the run is finished, it has decided the
 * run is blocked.
 *
 * This keys on `gap_declared`, not on membership in the four named gap
 * classes. A judge free to launder an unmet obligation into `gap_class:
 * "other"` — the catch-all for a gap whose class is unclear — used exactly
 * that escape: the same blocked-write fact that got `unresolved_authorization`
 * (refused) on one call got `other` (accepted) on the next, no schema
 * violation either time. Keying on the four names cannot close that, because
 * `other` is never one of the four names. See harn#7910.
 *
 * It also keys on the `gaps` array, which is the half that carries the claim.
 * Either alone is insufficient. A reply can name a gap in the array while
 * leaving the class unsent, and a reply can name a class while sending no
 * array, and both are the same self-contradiction.
 *
 * What is NOT a contradiction, since `none` joined the enum, is an approval
 * saying so. `gap_declared` is raw presence minus `none`, so a `done` that
 * omits the field and a `done` that explicitly sends `none` both pass, while
 * an explicit `other` on a `done` is refused exactly as harn#7910 requires —
 * `other` is no longer the value a compliant approval is left with, so a `done`
 * still sending it is naming a gap it declined to classify.
 *
 * @effects: []
 * @errors: []
 * @api_stability: internal
 * @example: __judge_completion_verdict_contradicts_itself({verdict: "done", detail: "", gap_class: "other", gap_declared: true})
 */
pub fn __judge_completion_verdict_contradicts_itself(decoded: CompletionJudgeVerdict) -> bool {
  return decoded.verdict == "done" && (len(decoded.gaps) > 0 || decoded.gap_declared)
}

/**
 * __judge_completion_verdict_refuses_without_a_gap.
 *
 * The converse shape: a `continue` that names nothing. A refusal with no gap
 * hands the actor a verdict it cannot act on, which is the same dead end a
 * contradiction produces from the other side.
 *
 * This rule used to live in the reply schema as `minItems: 1` on `gaps`, where
 * it could not see the verdict, so it refused every approval to enforce a rule
 * about refusals. Here it can see the verdict, so it costs approvals nothing.
 *
 * A `continue` reaching this state keeps its verdict. Converting a refusal into
 * an approval over a shape defect is the one direction that can end a run that
 * should not end, and the reply still carries `detail`, which is required and
 * non-empty. The caller names the shape on the record instead.
 *
 * @effects: []
 * @errors: []
 * @api_stability: internal
 * @example: __judge_completion_verdict_refuses_without_a_gap({verdict: "continue", detail: "x", gap_class: "other", gaps: [], gap_declared: false})
 */
pub fn __judge_completion_verdict_refuses_without_a_gap(decoded: CompletionJudgeVerdict) -> bool {
  return decoded.verdict == "continue" && len(decoded.gaps) == 0 && !decoded.gap_declared
}

/**
 * What the actor is told when a `done` was overridden for contradicting itself.
 *
 * The branch this serves used to fall through to the judge's own `detail`,
 * which on a `done` reply is its rationale for finishing. Injecting that as the
 * reason a run may not stop hands the actor a paragraph saying the work is
 * complete, so the veto is indistinguishable from an approval, the actor has
 * nothing to act on, and the loop cannot advance. Measured on three read-only
 * review cells: the same sentence re-injected on five consecutive iterations,
 * one tool call across seven turns, and a run that ended at the judge cap.
 *
 * So this names the condition instead: that a gap was declared alongside the
 * `done`, which gap, and the two ways out. The gap's own detail is included
 * when it has one, because the class alone is a label and the actor needs the
 * claim. The quote is deliberately NOT echoed: on the measured cells it was the
 * judge's own summary prose rather than a line from the evidence, so repeating
 * it would reintroduce exactly the sentence this function exists to stop
 * sending.
 *
 * @effects: []
 * @errors: []
 * @api_stability: internal
 * @example: __judge_contradiction_feedback({verdict: "done", detail: "", gap_class: "other", gaps: [], gap_declared: true})
 */
pub fn __judge_contradiction_feedback(decoded: CompletionJudgeVerdict) -> string {
  const first = if len(decoded.gaps) > 0 {
    trim(to_string(decoded.gaps[0]?.detail ?? ""))
  } else {
    ""
  }
  const named = if first != "" {
    " The outstanding item is: " + first
  } else {
    ""
  }
  return "The completion check reported the work finished while also recording an "
    + "outstanding gap of class `"
    + to_string(decoded.gap_class)
    + "`, so it cannot be read as a confirmation."
    + named
    + " Either resolve that gap and say what you changed, or, if it does not "
    + "apply to this task, say why it does not before finishing."
}

/**
 * __judge_completion_verdict_schema.
 *
 * One discriminant and one dual-purpose detail keep completion decisions
 * inside small-model output budgets. `detail` is the evidence basis for
 * `done`, or the single concrete gap and next action for `continue`.
 *
 * `gap_class` names WHAT a `continue` is refusing on. It is deliberately NOT
 * required: the checkpoint validates this schema strictly, and cached, replayed,
 * and older-pin judge responses carry no such field. An absent value decodes to
 * `other`, which is the reading that grants no authority — so the compatible
 * direction and the safe direction are the same direction. An approval says so
 * with `none`, or by omitting the field; see
 * `__judge_completion_verdict_contradicts_itself` for what still counts as a
 * `done` that names a gap.
 *
 * This schema states shape that holds for BOTH verdicts and nothing else. A
 * JSON validator is handed the reply without the question, so it cannot tell an
 * approval from a refusal, and any rule that depends on which one this is can
 * only be half enforced here. Those rules live in
 * `__judge_completion_verdict_read` and its two predicates.
 *
 * @effects: []
 * @errors: []
 * @api_stability: experimental
 * @example: __judge_completion_verdict_schema()
 */
pub fn __judge_completion_verdict_schema(raw_requirement_contract: unknown = nil) -> dict {
  const contract = completion_requirement_contract(raw_requirement_contract)
  let properties = {
    verdict: {type: "string", enum: ["done", "continue"]},
    detail: {
      type: "string",
      minLength: 1,
      description:
        "Brief evidence basis or gap. State the remedy, not only the problem. Harn keeps the first 1000 characters.",
    },
    gap_class: {
      type: "string",
      enum: COMPLETION_JUDGE_GAP_CLASSES,
      description:
        "On `continue`, the kind of gap being named. On `done`, send `none` or omit the field.",
    },
    // The judge used to have one `detail` and one `gap_class` to answer with,
    // and was told to use them for "the single most important gap". A judge
    // holding three objections could not state them, so it named one, the
    // actor fixed it, and the next invocation named the next. With a default
    // cap of three that is a task with three real gaps failing inside its own
    // budget while every refusal it received was correct. `gaps` is the room
    // to say all of it at once.
    // NO `minItems`. It used to be 1, unconditionally, while this field's own
    // description told the model to omit the array on `done`. `gaps` is not in
    // `required`, so omitting it is legal and sending `[]` was not — and those
    // two encode the same fact. Measured over an eval archive of 62 judge
    // calls: not one `done` reply reached the pipeline carrying no gap. All 22
    // were schema-rejected for `gaps: []`, and the repair turn, which hands the
    // model its own text back and asks it to correct the JSON, can only satisfy
    // a one-item minimum by inventing a gap. The model did what it was asked
    // and lifted a sentence out of its own `detail` into `evidence_quote`.
    // Everything downstream then reacted to that artifact: the self-
    // contradiction check fired, the re-ask flipped the verdict, the invented
    // sentence could not be grounded, a second re-ask fired, and the gate
    // converted the whole thing back to `done`. Three judge calls and two
    // re-asks to arrive where the first answer already was, on 22 of 62 calls.
    //
    // A validator cannot see the verdict, so verdict-dependent shape put here
    // can only ever be enforced in one direction. It lives in the typed read
    // now, which can see it, and which already owned the converse rule.
    gaps: {
      type: "array",
      description: "On `continue`, EVERY gap you currently hold, not the most important one. "
        + "The actor can only converge on a set it is shown in full. On `done`, send `[]` or "
        + "omit the field.",
      items: {
        type: "object",
        required: ["criterion", "gap_class", "detail"],
        additionalProperties: false,
        properties: {
          criterion: {
            type: "string",
            minLength: 1,
            description:
              "The requirement from the task statement this gap is against, quoted or closely paraphrased. One gap, one criterion.",
          },
          gap_class: {type: "string", enum: COMPLETION_JUDGE_GAP_CLASSES},
          detail: {
            type: "string",
            minLength: 1,
            description: "What is missing and the substantive next action that closes it.",
          },
          evidence_quote: {
            type: "string",
            description: "A line copied VERBATIM from the evidence above that shows this gap. "
              + "Required when the gap is about the content of a file the evidence displays. "
              + "A quote that does not appear in the evidence is refused.",
          },
        },
      },
    },
  }
  // Attribution is offered ONLY when there is a ledger to attribute to, and it
  // is an enum of that ledger's own ids rather than a free string, so the model
  // cannot invent a row and nothing downstream has to match prose to prose.
  const requirement_ids = completion_requirement_ids(contract)
  if len(requirement_ids) > 0 {
    properties = properties
      + {
        gaps: properties.gaps
          + {
            items: properties.gaps.items
              + {
                properties: properties.gaps.items.properties
                  + {
                    requirement_id: {
                      type: "string",
                      enum: requirement_ids,
                      description: "The acceptance row this gap is against. Omit it if no single row covers "
                        + "the gap; do not guess, an omitted row is recorded as unattributed.",
                    },
                  },
              },
          },
      }
  }
  const assessments = completion_requirement_assessments_schema(contract)
  if assessments != nil {
    properties = properties + {requirement_report: assessments}
  }
  return {
    type: "object",
    properties: properties,
    required: ["verdict", "detail"],
    additionalProperties: false,
  }
}

/**
 * __judge_completion_verdict_read.
 *
 * Decode a judge response into the compact verdict. The superseded shape
 * `{action, reason, repair, ...}` still decodes, because cached and replayed
 * judge responses outlive the schema that produced them and a decision read
 * as absent would silently become an approval.
 *
 * @effects: []
 * @errors: []
 * @api_stability: experimental
 * @example: __judge_completion_verdict_read({verdict: "done", detail: "tests pass"})
 */
pub fn __judge_completion_verdict_read(
  result: dict,
  raw_requirement_contract: unknown = nil,
  evidence_packet: CompletionRequirementEvidencePacket = {},
) -> CompletionJudgeVerdict {
  const raw = trim(to_string(result?.verdict ?? result?.action ?? ""))
  const verdict = if raw == "accept" {
    "done"
  } else {
    raw
  }
  // First non-blank wins rather than first non-nil: the superseded shape
  // carried an empty `repair` on approval, which would otherwise shadow the
  // `reason` that holds the audit basis.
  let detail = ""
  for candidate in [result?.detail, result?.repair, result?.reason] {
    if detail == "" {
      detail = trim(to_string(candidate ?? ""))
    }
  }
  const clamped = __judge_clamp_completion_detail(detail)
  // Raw presence, read before normalization. `__completion_judge_gap_class`
  // folds a missing field, a blank string, an unrecognized string, and an
  // explicit `"other"` into the same `"other"` value, which is right for
  // display and for the arbitration ladder but wrong for this one question:
  // did the reply CLAIM a gap here?
  //
  // `none` is excluded because it is the one value that answers that question
  // with no. Without it in the enum, an approval had nothing legal to send and
  // models sent `other`, which read as a claimed gap and made every such
  // approval a self-contradiction. Blank and absent stay outside the claim too;
  // they always did.
  const raw_gap_class = lowercase(trim(to_string(result?.gap_class ?? "")))
  const gap_declared = raw_gap_class != "" && raw_gap_class != "none"
  const contract = completion_requirement_contract(raw_requirement_contract)
  return {
    verdict: verdict,
    detail: clamped,
    gap_class: __completion_judge_gap_class(result?.gap_class),
    gaps: __judge_completion_gaps_read(result, completion_requirement_ids(contract)),
    gap_declared: gap_declared,
    requirement_report: completion_requirement_report(
      contract,
      result?.requirement_report,
      evidence_packet,
    ),
  }
}

/**
 * The gaps a refusal itemized, normalized.
 *
 * Empty for an approval, for a reply that predates the `gaps` field, and for a
 * reply that sent something other than a list. Callers distinguish "itemized
 * nothing" from "itemized badly" by asking for the raw field themselves; this
 * reader only ever returns well-formed rows.
 *
 * @effects: []
 * @errors: []
 * @api_stability: experimental
 * @example: __judge_completion_gaps_read({gaps: []})
 */
pub fn __judge_completion_gaps_read(
  result: dict,
  known_requirement_ids: list<string> = [],
) -> list<CompletionJudgeGapItem> {
  const raw = result?.gaps
  guard type_of(raw) == "list" else {
    return []
  }
  let out: list<CompletionJudgeGapItem> = []
  for entry in raw {
    guard type_of(entry) == "dict" else {
      continue
    }
    const criterion = trim(to_string(entry?.criterion ?? ""))
    const detail = trim(to_string(entry?.detail ?? ""))
    if criterion == "" || detail == "" {
      continue
    }
    // An id the ledger did not hand out is not a near miss to be repaired, it
    // is an attribution the run cannot stand behind. Drop it to unattributed
    // and let the count say so.
    const claimed_id = trim(to_string(entry?.requirement_id ?? ""))
    const requirement_id = if (known_requirement_ids ?? []).contains(claimed_id) {
      claimed_id
    } else {
      ""
    }
    out = out
      + [
        {
          criterion: criterion,
          gap_class: __completion_judge_gap_class(entry?.gap_class),
          detail: detail,
          evidence_quote: trim(to_string(entry?.evidence_quote ?? "")),
          requirement_id: requirement_id,
        },
      ]
  }
  return out
}

/**
 * How many itemized gaps name no acceptance row.
 *
 * Reported on the receipt rather than left implicit, because a refusal set that
 * attributes nothing is the finding: either the ledger does not cover what the
 * judge is objecting to, or the judge is objecting outside the contract. Both
 * are worth seeing, and neither is visible if absence is silent.
 *
 * @effects: []
 * @errors: []
 * @api_stability: experimental
 * @example: __judge_gaps_unattributed_count([])
 */
pub fn __judge_gaps_unattributed_count(gaps: list<CompletionJudgeGapItem>) -> int {
  let unattributed = 0
  for gap in gaps {
    if trim(gap.requirement_id) == "" {
      unattributed = unattributed + 1
    }
  }
  return unattributed
}

/**
 * Quotes a refusal attributed to the evidence that are not in the evidence.
 *
 * Measured 2026-09-05 on two scheduler trials: the judge refused ten times
 * saying the ready queue was still unsorted, phrased against the file view it
 * had been shown ("the current scheduler.go shown in the live edited window").
 * Seven of those were harn#8090 and the judge was right about what it could
 * see. The rest had the view in front of them.
 *
 * A quote is checked by presence in the rendered evidence the judge was
 * actually handed, whitespace-normalized so a reflowed copy still matches. This
 * cannot catch a wrong INFERENCE from a real line, and is not meant to: it
 * catches a claim attributed to a view that does not support it, which is the
 * observed failure. An empty quote is not a violation — the field is required
 * only for file-content gaps, and a judge that cites nothing is judged by the
 * other clauses.
 *
 * @effects: []
 * @errors: []
 * @api_stability: experimental
 * @example: __judge_ungrounded_gap_quotes([], "")
 */
pub fn __judge_ungrounded_gap_quotes(
  gaps: list<CompletionJudgeGapItem>,
  evidence: string,
) -> list<string> {
  const haystack = __judge_collapse_spaces(evidence)
  guard haystack != "" else {
    // No evidence rendered means nothing to contradict. Refusing here would
    // fail a judge for the harness having shown it nothing.
    return []
  }
  let bad: list<string> = []
  for gap in gaps {
    const quote = __judge_collapse_spaces(gap.evidence_quote)
    if quote == "" {
      continue
    }
    if !haystack.contains(quote) {
      bad = bad + [gap.evidence_quote]
    }
  }
  return bad
}

/** Whitespace-normalize so a reflowed or re-indented copy of a real line still matches. */
fn __judge_collapse_spaces(value: string) -> string {
  let out = ""
  let last_space = true
  for ch in split(trim(value), "") {
    const is_space = ch == " " || ch == "\t" || ch == "\n" || ch == "\r"
    if is_space {
      if !last_space {
        out = out + " "
      }
      last_space = true
    } else {
      out = out + ch
      last_space = false
    }
  }
  return trim(out)
}