Skills › math-proof › siege › ledger.py
ledger.py
662 lines · plugins/math-proof/skills/siege/scripts/ledger.py at a7ba5b9
1#!/usr/bin/env python3
2"""Bookkeeping helper for the math-proof plugin's siege skill: the four mechanical
3decisions of the round loop and its waves that should not depend on a
4model's judgment.
6 ledger.py check DIR R WAVE MIN_ROUNDS ATTEMPT
7 After the round-R plan step: validates the shape of what the judge
8 wrote, applies the early-conclusion gate, commits the round's ledger
9 lines (numbered on) to DIR/ledger.md once the round's plan is final,
10 and prints ONE verdict line for the orchestrator:
11 WAVE <n> FLOOR <f> run round R's wave (files roundR_q1.md .. roundR_q<n>.md);
12 stop the run if fewer than <f> of its queries come
13 back answered or partial
14 CONCLUDE <why> leave the round loop
15 RETRY: <text> relaunch the plan step with <text> as an added
16 first paragraph (ATTEMPT < 3 only)
17 TAIL: <why> give up on this round and go to the proof tail
18 ledger.py append DIR R
19 Number the lines of DIR/roundR_ledger_block.md on from the ledger of
20 rounds before R, write DIR/roundR_ledger.md, rebuild DIR/ledger.md.
21 Idempotent (safe to re-run for the same round).
22 ledger.py gate DIR [R]
23 Print CONCLUDE or "REJECT: <reason>" for the early-conclusion gate on
24 the assembled ledger as it stands (plus round R's not-yet-appended
25 block, numbered on, when R is given).
26 ledger.py answers DIR Q1 [Q2 ...]
27 After a wave's workers have all returned: decide which answer files
28 are finished. A worker that finishes writes the end line
29 "=== END OF ANSWER <Q> ===" last; a file without it was cut off. For
30 each query stem Q (e.g. round2_q3) prints "Q: answered" (DIR/Q.answer.md
31 ends with Q's end line), "Q: partial" (only an unfinished file exists)
32 or "Q: no answer", then one TOTAL line with the number of queries and
33 the three counts. Side effects, so that a .answer.md file always means
34 a finished answer: an unfinished DIR/Q.answer.md is moved to
35 DIR/Q.partial.md (if an older, longer Q.partial.md is already there,
36 that one stays and the new file goes to Q.partial.prev.md instead; a
37 shorter older one moves to Q.partial.prev.md), and an empty
38 DIR/Q.answer.md is deleted. Nothing a worker wrote is ever deleted or
39 overwritten except an older Q.partial.prev.md. Idempotent; an ERROR
40 line (and nothing touched) if a stem is wrong.
42A malformed command (DIR not an existing directory, a missing or non-numeric
43argument) prints an ERROR line and touches nothing. Standard library only
44(Python 3.7 or later); files are read and written as UTF-8 regardless of the
45platform's default encoding. Always exits 0 and says what it decided on
46stdout; any internal error prints a fail-closed verdict (RETRY/REJECT, or an
47ERROR line from `answers`) rather than a traceback the orchestrator might
48misread.
49"""
51from __future__ import annotations
53import re
54import sys
55from pathlib import Path
57MAX_ATTEMPTS = 3 # plan attempts per round before a shortfall is accepted
58ENC = dict(encoding="utf-8", errors="replace")
60# ---- ledger parsing and the early-conclusion gate --------------------------
61_LEDGER_STATUS_WORDS = ("OPEN", "PROVED", "REFUTED", "RETRACT", "RETRACTED", "SKETCHED")
62_SETTLED = ("PROVED", "REFUTED")
65def _take_tags(text: str, tags: set) -> str:
66 """Strip a leading cluster of short bracketed tags ("[GOAL] ",
67 "[AUDIT]: ") off text, adding each (upper-cased) to tags; a
68 bracketed STATUS word is not a tag and stops the scan. Tags count
69 only in this leading position — a prose mention later in the line
70 ("the key step toward [GOAL]") is not a tag."""
71 while True:
72 m = re.match(r"^[*_\s]*\[([A-Za-z]{1,6})\]\s*[:\-–—]?\s*", text)
73 if not m or m.group(1).upper() in _LEDGER_STATUS_WORDS:
74 return text
75 tags.add(m.group(1).upper())
76 text = text[m.end() :]
79def _cited_ids(text: str) -> set:
80 """Ledger-id citations in an entry's free text. Two forms count:
81 the word forms ("entry 12", "line 12", "claim 12", "item 12",
82 "no. 12", and hybrids like "entry L5" — case-insensitive, the
83 same family the RETRACT target parser tolerates) and the "#12"
84 form. A prose "L12" deliberately does NOT count: every
85 prose-position L-number matcher tried was fail-open on analysis
86 prose — "in L2", "the L2 norm", "L2(R)", and coordinated lists
87 like "verified the L1 and L2 bounds" collide exactly with the
88 small ids early-round goals get. The plan brief and the RETRY
89 correction teach the counted forms, so a judge writing
90 "cites L12" is re-asked and can correct — a missed citation only
91 costs a retry (fail-closed), where a spurious one ends a paid run
92 early. Decimal and slash-fraction references never count ("Claim
93 2.4 of the draft", "line 1/2" — ledger ids are integers), and the
94 L hybrid ("entry L5") is not accepted after "line"/"lines", where
95 it collides with geometry prose ("lines L2 and L4 are tangent").
96 Bare integers are never citations (math prose is full of them)."""
97 ids = set()
98 for m in re.finditer(r"#(\d{1,4})\b(?![./]\d)", text):
99 ids.add(int(m.group(1)))
100 for m in re.finditer(
101 r"\b(?:entry|entries|claim|claims|item|items|id|ids|no\.|number)"
102 r"\s+#?L?(\d{1,4})\b(?![./]\d)"
103 r"|\b(?:line|lines)\s+#?(\d{1,4})\b(?![./]\d)",
104 text,
105 re.IGNORECASE,
106 ):
107 ids.add(int(m.group(1) or m.group(2)))
108 return ids
111def ledger_entries(ledger_text: str) -> dict[int, dict]:
112 """Parse the assembled numbered ledger ("12. OPEN: claim — locator",
113 "13. RETRACT 4: reason") into {n: {status, text, retracted_by,
114 goal, audit}}. Tolerant of what judges actually write after the
115 number this script assigns: a self-assigned id ("L3.", "(L5)", "#7:"),
116 markdown emphasis around the status word ("**OPEN**:"), any case,
117 and RETRACT spelled "RETRACTED" / aimed at "L4", "#4", "entry 4" or
118 "claim 4". status is upper-cased (PROVED / REFUTED / OPEN / RETRACT
119 / whatever other word the judge used); retracted_by is the number
120 of the RETRACT line that removed the entry from force, if any.
121 goal/audit are set only by a [GOAL]/[AUDIT] tag in tag position —
122 immediately before or after the status word — never by a prose
123 mention elsewhere in the line."""
124 out: dict[int, dict] = {}
125 for ln in ledger_text.splitlines():
126 m = re.match(r"\s*(\d+)\.\s+(.*)", ln)
127 if not m:
128 continue
129 n, rest = int(m.group(1)), m.group(2)
130 # a self-assigned id is dropped only when punctuated or bracketed
131 # ("L3." / "L3:" / "(L3)" / "#3:"), so prose like "L2 norm" survives
132 rest = re.sub(
133 r"^[*_\s]*(?:\(\s*(?:L|#)?\s*\d+\s*\)\s*[.:\-–—]?|(?:L|#)\s*\d+\s*[.:)\-–—])\s*",
134 "",
135 rest,
136 )
137 tags: set = set()
138 rest = _take_tags(rest, tags)
139 sm = re.match(
140 r"[*_\s\[]*([A-Za-z]+)[*_\]]*\s*[:.\-–—]?\s*(.*)", rest, re.DOTALL
141 )
142 if not sm:
143 continue
144 status, text = sm.group(1).upper(), sm.group(2)
145 if status.startswith("RETRACT"):
146 status = "RETRACT"
147 text = _take_tags(text, tags)
148 out[n] = {
149 "status": status,
150 "text": text,
151 "retracted_by": None,
152 "goal": "GOAL" in tags,
153 "audit": "AUDIT" in tags,
154 }
155 for n, e in out.items():
156 if e["status"] == "RETRACT":
157 tm = re.match(
158 r"[*_\s]*(?:entry|claim|item|line|no\.?|number)?\s*[#(]?\s*L?\s*(\d+)",
159 e["text"],
160 re.IGNORECASE,
161 )
162 if tm and int(tm.group(1)) in out and int(tm.group(1)) != n:
163 out[int(tm.group(1))]["retracted_by"] = n
164 return out
167def early_conclude_ok(entries: dict[int, dict], known_locators=None) -> bool:
168 """Early-conclusion gate. True when the ledger's goal is settled and
169 twice audited:
171 - the NEWEST in-force [GOAL]-tagged line is PROVED or REFUTED (the
172 ledger's own supersession rule: a later unsettled [GOAL] update
173 takes the goal back out of play without needing a RETRACT);
174 - at least two in-force PROVED [AUDIT] lines — the goal line itself
175 never counts as its own audit, byte-duplicate lines count once —
176 each cite the goal line, or a line its text cites, by ledger id
177 ("entry 12" / "#12"; a prose "L12" does not count — see
178 _cited_ids; ids must resolve to existing entries), and at least
179 one cites the goal line itself;
180 - when known_locators is given (check and gate pass the stems of the
181 result files that actually exist), each counted audit line must
182 name one — matched case-insensitively, since the files are all
183 lowercase while a judge may title-case at sentence start — and
184 the counted audits must span at least two distinct locators,
185 tying the certifications to queries that really ran, from at
186 least two separate queries.
188 REFUTED settles a prove-or-disprove goal as surely as PROVED (an
189 audited disproof concludes the run). One consequence of the
190 cite-the-goal requirement, by design: audits recorded before the
191 [GOAL] line existed (or before a [GOAL] re-statement) cite older
192 ids and so cannot satisfy it — append-only history is never
193 implicitly re-tagged — and the concluding plan's own ledger block
194 must re-state at least one certification citing the goal line's
195 id (the RETRY correction names this fix). The gate is a structured
196 attestation check on judge-written ledger text, not an independent
197 proof check: the run's correctness still rests on the audits being
198 real, which the locator requirement grounds but cannot prove."""
199 live = {n: e for n, e in entries.items() if e["retracted_by"] is None}
200 goals = sorted(n for n, e in live.items() if e.get("goal"))
201 if not goals:
202 return False
203 g = goals[-1]
204 if live[g]["status"] not in _SETTLED:
205 return False
206 chain = {g} | {m for m in _cited_ids(live[g]["text"]) if m in live}
207 audits = []
208 seen = set()
209 for n in sorted(live):
210 e = live[n]
211 if e["status"] != "PROVED" or not e.get("audit") or e.get("goal") or n == g:
212 continue
213 cites = _cited_ids(e["text"]) & chain
214 if not cites:
215 continue
216 norm = " ".join(e["text"].split()).lower()
217 if norm in seen:
218 continue
219 locs = None
220 if known_locators is not None:
221 locs = {
222 loc
223 for loc in known_locators
224 if re.search(
225 rf"(?<![A-Za-z0-9_]){re.escape(loc)}(?![A-Za-z0-9_])",
226 e["text"],
227 re.IGNORECASE,
228 )
229 }
230 if not locs:
231 continue
232 seen.add(norm)
233 audits.append((n, cites, locs))
234 if len(audits) < 2:
235 return False
236 if not any(g in cites for _, cites, _ in audits):
237 return False
238 if known_locators is not None:
239 spanned = set().union(*(locs for _, _, locs in audits))
240 if len(spanned) < 2:
241 return False
242 return True
245# ---- end of ledger parsing and the gate -----------------------------------
248def _round_of(p: Path) -> int:
249 m = re.fullmatch(r"round(\d+)_ledger", p.stem)
250 return int(m.group(1)) if m else -1
253def _parts(d: Path) -> list:
254 return sorted(
255 (p for p in d.glob("round*_ledger.md") if _round_of(p) >= 0), key=_round_of
256 )
259def ledger_text(d: Path, before=None) -> str:
260 """The assembled ledger: the per-round numbered parts, in round order."""
261 out = []
262 for p in _parts(d):
263 if before is not None and _round_of(p) >= before:
264 continue
265 out.append(p.read_text(**ENC))
266 return "".join(out)
269def numbered_lines(d: Path, r: int, block: str) -> list:
270 """Round r's new lines, numbered on from the ledger of rounds < r, with
271 the judge's bullets / numbering / self-assigned ids stripped."""
272 prior = ledger_text(d, before=r)
273 n = sum(1 for ln in prior.splitlines() if ln.strip())
274 lines = []
275 for raw in (block or "").splitlines():
276 ln = re.sub(r"^(?:[-*]|\d{1,4}\.)\s+", "", raw.strip())
277 ln = re.sub(
278 r"^(?:\((?:L|#)?\d{1,4}\)(?:[.:]\s*|\s+)|(?:L|#)\d{1,4}[.:]\s+)(?=\S)",
279 "",
280 ln,
281 )
282 if ln:
283 n += 1
284 lines.append(f"{n}. {ln}")
285 return lines
288def append(d: Path, r: int) -> int:
289 bp = d / f"round{r}_ledger_block.md"
290 block = bp.read_text(**ENC) if bp.exists() else ""
291 lines = numbered_lines(d, r, block)
292 (d / f"round{r}_ledger.md").write_text(
293 "".join(f"{ln}\n" for ln in lines), encoding="utf-8"
294 )
295 (d / "ledger.md").write_text(ledger_text(d), encoding="utf-8")
296 return len(lines)
299def known_locators(d: Path) -> set:
300 return {p.name[: -len(".answer.md")] for p in d.glob("*.answer.md")}
303def gate_reason(text: str, locs: set) -> str:
304 """'' when the early-conclusion gate passes on this ledger text, else
305 the first failing condition in plain words (the pass/fail decision
306 itself is early_conclude_ok's)."""
307 entries = ledger_entries(text)
308 if early_conclude_ok(entries, locs):
309 return ""
310 live = {n: e for n, e in entries.items() if e["retracted_by"] is None}
311 goals = sorted(n for n, e in live.items() if e.get("goal"))
312 if not goals:
313 return "the ledger has no [GOAL]-tagged line in force"
314 g = goals[-1]
315 if live[g]["status"] not in _SETTLED:
316 return f"the newest [GOAL] line (entry {g}) is {live[g]['status']}, not PROVED or REFUTED"
317 audits = [
318 n
319 for n, e in live.items()
320 if e["status"] == "PROVED" and e.get("audit") and not e.get("goal") and n != g
321 ]
322 if len(audits) < 2:
323 return f"only {len(audits)} PROVED [AUDIT] line(s) in force besides the goal line (entry {g}); two are needed"
324 return (
325 f"the [AUDIT] lines do not yet form a qualifying pair: each must cite the [GOAL] line "
326 f"(entry {g}) or a line it cites as 'entry N' or '#N' (at least one citing entry {g} itself), "
327 f"each must name the locator of an answer file that exists (e.g. round3_q2), and together "
328 f"they must come from two different queries"
329 )
332def round_queries(d: Path, r: int) -> list:
333 qs = [
334 p for p in d.glob(f"round{r}_q*.md") if re.fullmatch(rf"round{r}_q\d+", p.stem)
335 ]
336 return sorted(qs, key=lambda p: int(p.stem.rsplit("_q", 1)[1]))
339def is_attack(p: Path) -> bool:
340 """kind: attempt declared near the top (first three non-empty lines that
341 contain letters — tolerates a front-matter fence or a heading first)."""
342 seen = 0
343 for ln in p.read_text(**ENC).splitlines():
344 if not re.search(r"[A-Za-z]", ln):
345 continue
346 if re.match(
347 r"[*_\s`#>-]*kind[*_`\s]*[:=][\s\"'*_`]*(attempt|attack)", ln, re.IGNORECASE
348 ):
349 return True
350 seen += 1
351 if seen >= 3:
352 return False
353 return False
356def is_withdrawn(p: Path) -> bool:
357 """An emptied or '(withdrawn)' query file left over from a re-plan."""
358 t = p.read_text(**ENC).strip()
359 return not t or bool(
360 re.fullmatch(r"[(\[]?\s*withdrawn\s*[)\]]?\.?", t, re.IGNORECASE)
361 )
364def wave_floor(n: int) -> int:
365 """Fewest queries of a round's wave that may come back answered or
366 partial before the run stops (3 in 10 of the wave, rounded down, and at
367 least 1)."""
368 return max(1, (3 * n) // 10)
371_STEM = re.compile(r"[A-Za-z0-9_]+")
374def is_end_line(line: str, stem: str) -> bool:
375 """True when line is the end line of query `stem`, "=== END OF ANSWER
376 <stem> ===", compared tolerantly: any case; the '=' rails in any
377 length or absent, or drawn with other symbols; markdown dressing (a
378 heading '#', a quote '>', a list marker, a wrapper or inner emphasis of
379 backticks, asterisks, underscores or quotes, an escaped underscore
380 'round2\\_q3'); a colon after ANSWER; a final period; and the stem given
381 bare, as "<stem>.md", as "<stem>.answer.md" or as a plain path ending in
382 one of those; a checklist item ("- [ ] ...") never counts. What must
383 survive is exactly the words END OF ANSWER followed by this query's own
384 name and nothing else: an end line copied in from another query's text
385 (spliced into a task file by the judge, say) names that other query, and
386 a sentence that merely mentions the end line has other words around it;
387 neither counts."""
388 if re.search(r"\[[ xX]\]", line): # a checklist item is a plan, not an end line
389 return False
390 t = line.replace("\\_", "_")
391 t = re.sub(r"[^A-Za-z0-9_./ -]+", " ", t) # drop rails, emphasis, quotes
392 t = " ".join(t.split()).strip("_- ")
393 t = re.sub(r"^\d{1,2}\. ", "", t) # a numbered-list marker
394 name = rf"(?:[A-Za-z0-9_./-]*/)?{re.escape(stem)}(?:\.answer\.md|\.md)?"
395 return bool(re.fullmatch(rf"END OF ANSWER {name} ?\.?", t, re.IGNORECASE))
398_TAG_ONLY = re.compile(r"(?:\s*</?[A-Za-z_][\w:.-]*\s*/?>)+\s*")
401def _last_line(text: str) -> str:
402 """The last line of text that contains a letter or digit ('' if none),
403 so that a closing code fence or a rule drawn under the end line does
404 not hide it. A line made of nothing but bare markup tags without
405 attributes (a stray '</details>' or similar closing tag a model sometimes
406 emits after its last real line) is skipped the same way: a worker does not
407 write its end line in that form, and skipping such a line can only
408 reveal an end line the worker did write above it."""
409 for ln in reversed(text.splitlines()):
410 if not re.search(r"[A-Za-z0-9]", ln) or _TAG_ONLY.fullmatch(ln):
411 continue
412 return ln
413 return ""
416def answers(d: Path, args: list) -> str:
417 """Classify each query's answer file and set unfinished ones aside (see
418 the module docstring). Only one line of DIR/Q.answer.md is looked at, the
419 last that contains a letter or digit and is not a bare markup tag;
420 nothing else in any file is read for meaning."""
421 stems, seen = [], set()
422 for arg in args:
423 stem = Path(arg).name # tolerate a path or a file name for a stem
424 for suffix in (".answer.md", ".partial.md", ".md"):
425 if stem.endswith(suffix):
426 stem = stem[: -len(suffix)]
427 break
428 if not _STEM.fullmatch(stem):
429 return f"ERROR: {arg!r} is not a query stem (letters, digits and underscores only, e.g. round2_q3, extra_q1, r3_q2, r3_verify); nothing was touched"
430 if not any((d / f"{stem}{x}").exists() for x in (".md", ".answer.md", ".partial.md")):
431 return f"ERROR: there is no query file {stem}.md in {d} (wrong DIR, or a mistyped stem); nothing was touched"
432 if stem not in seen:
433 seen.add(stem)
434 stems.append(stem)
435 out, counts = [], {"answered": 0, "partial": 0, "no answer": 0}
436 for stem in stems:
437 a, p = d / f"{stem}.answer.md", d / f"{stem}.partial.md"
438 status = None
439 if a.exists():
440 text = a.read_text(**ENC)
441 if is_end_line(_last_line(text), stem):
442 status = "answered"
443 elif not text.strip():
444 a.unlink() # an empty file is no answer; any older partial stays
445 elif p.exists() and p.stat().st_size > len(text.encode("utf-8", "replace")):
446 # an older, longer unfinished file stays the partial; keep this one beside it
447 a.replace(d / f"{stem}.partial.prev.md")
448 else:
449 if p.exists() and p.read_text(**ENC).strip():
450 p.replace(d / f"{stem}.partial.prev.md")
451 a.replace(p)
452 if status is None:
453 partial = p.exists() and p.read_text(**ENC).strip()
454 status = "partial" if partial else "no answer"
455 counts[status] += 1
456 out.append(f"{stem}: {status}")
457 out.append(
458 f"TOTAL ({len(stems)} {'query' if len(stems) == 1 else 'queries'}): answered {counts['answered']}, partial {counts['partial']}, no answer {counts['no answer']}"
459 )
460 return "\n".join(out)
463GATE_RULE = (
464 "Concluding before round {m} requires the claims ledger to hold the headline goal settled "
465 "as a PROVED or REFUTED line tagged [GOAL], plus at least two PROVED lines tagged [AUDIT] "
466 "from two separate verify queries, each naming its query's locator (e.g. round3_q2) and "
467 "citing the [GOAL] line or its chain by ledger id written 'entry 12' or '#12', at least one "
468 "citing the [GOAL] line itself. Only the newest [GOAL] line counts, it never counts as one of "
469 "its own audits, and audits recorded before that line cite older ids — re-state the "
470 "certifications citing its id (one suffices when the [GOAL] line itself cites the line they "
471 "certify; otherwise two, from separate queries). Either compose a wave — for example verify "
472 "queries whose certifications complete the chain — or conclude once the ledger qualifies."
473)
474STILL_THERE = (
475 " The files from your previous attempt at this round (summary, ledger block, notes, any query "
476 "files) are still in place and this round's ledger block has NOT been appended to DIR/ledger.md "
477 "yet: rewrite DIR/round{r}_ledger_block.md so that it holds ALL of this round's new ledger lines, "
478 "and if you now conclude instead of composing a wave, delete this round's query files "
479 "(DIR/round{r}_q*.md) first — existing query files take precedence over a conclusion."
480)
483def check(d: Path, r: int, wave: int, min_rounds: int, attempt: int) -> str:
484 """The round-r plan verdict. The round's ledger block is committed to
485 ledger.md only together with a terminal verdict (WAVE / CONCLUDE /
486 TAIL), never on RETRY — so a re-planned round simply rewrites its block,
487 and the early-conclusion gate is evaluated on the ledger of earlier
488 rounds plus this attempt's not-yet-appended lines."""
489 final = attempt >= MAX_ATTEMPTS
490 wave = max(1, wave)
491 sp = d / f"round{r}_summary.md"
492 if not sp.exists() or not sp.read_text(**ENC).strip():
493 what = f"no running summary (DIR/round{r}_summary.md is missing or empty)"
494 return (
495 f"TAIL: {what} after {attempt} attempts"
496 if final
497 else f"RETRY: Correction — the previous attempt at this step wrote {what}. "
498 f"Write DIR/round{r}_summary.md, then EITHER DIR/round{r}_DONE.md OR between 1 and {wave} query files."
499 + STILL_THERE.format(r=r)
500 )
501 qs = round_queries(d, r)
502 for p in [q for q in qs if is_withdrawn(q)]:
503 p.replace(p.with_name(p.stem + ".withdrawn.md"))
504 qs.remove(p)
505 for k, p in enumerate(qs, 1): # close gaps so the wave is q1..qn
506 want = d / f"round{r}_q{k}.md"
507 if p != want:
508 p.replace(want)
509 qs[k - 1] = want
510 done = d / f"round{r}_DONE.md"
511 if qs: # composed queries take precedence over a verdict
512 if done.exists():
513 done.replace(d / f"round{r}_DONE.superseded.md")
514 extra = ""
515 if len(qs) > wave:
516 for p in qs[wave:]:
517 p.replace(p.with_name(p.stem + ".overcount.md"))
518 qs = qs[:wave]
519 extra = f"; over-count: files beyond q{wave} set aside"
520 need = (len(qs) + 1) // 2
521 got = sum(1 for p in qs if is_attack(p))
522 if got < need and not final:
523 return (
524 f"RETRY: Correction — the previous plan step composed {len(qs)} queries but marked only {got} "
525 f"with a first line 'kind: attempt'; at least {need} (half, rounded up) must be attempt queries "
526 f"aimed at this run's own flagged open questions, each beginning with the line 'kind: attempt' "
527 f"and naming the open question it attempts. Rewrite the query files DIR/round{r}_q1.md … "
528 f"(overwrite them; if you now compose fewer, delete the surplus files with rm) so that the wave "
529 f"satisfies this." + STILL_THERE.format(r=r)
530 )
531 n_new = append(d, r)
532 note = f", kind=attempt {got}/{len(qs)}" + (
533 " accepted below quota after retries" if got < need else ""
534 )
535 return (
536 f"WAVE {len(qs)} FLOOR {wave_floor(len(qs))} (ledger +{n_new}{note}{extra})"
537 )
538 if done.exists() and done.read_text(**ENC).strip():
539 if r >= min_rounds:
540 n_new = append(d, r)
541 return f"CONCLUDE (round {r} >= floor {min_rounds}; ledger +{n_new})"
542 bp = d / f"round{r}_ledger_block.md"
543 pending = numbered_lines(d, r, bp.read_text(**ENC) if bp.exists() else "")
544 text = ledger_text(d, before=r) + "".join(f"{ln}\n" for ln in pending)
545 why = gate_reason(text, known_locators(d))
546 if not why:
547 n_new = append(d, r)
548 return f"CONCLUDE (audited chain accepted before round {min_rounds}; ledger +{n_new})"
549 if final:
550 n_new = append(d, r)
551 return f"CONCLUDE (accepted before round {min_rounds} after {attempt} plan attempts without a qualifying chain — {why}; ledger +{n_new})"
552 done.replace(d / f"round{r}_DONE.rejected{attempt}.md")
553 return (
554 f"RETRY: Correction — your conclusion at round {r} was not accepted: {why}. "
555 + GATE_RULE.format(m=min_rounds)
556 + STILL_THERE.format(r=r)
557 )
558 what = f"neither DIR/round{r}_DONE.md nor any query file DIR/round{r}_q1.md …"
559 if final:
560 n_new = append(d, r)
561 return f"TAIL: {what} after {attempt} attempts (ledger +{n_new})"
562 return (
563 f"RETRY: Correction — the previous attempt at this step wrote {what}. The required shape is: "
564 f"DIR/round{r}_summary.md, then EITHER DIR/round{r}_DONE.md (only if the goal is fully established) "
565 f"OR between 1 and {wave} query files. Write exactly that."
566 + STILL_THERE.format(r=r)
567 )
570USAGE = (
571 "usage: ledger.py check DIR R WAVE MIN_ROUNDS ATTEMPT | append DIR R | gate DIR [R] | "
572 "answers DIR Q1 [Q2 ...] (bookkeeping for the math-proof siege skill; DIR is the run directory)"
573)
574# per command: its usage form, then how many arguments follow DIR (at least,
575# at most) and how many of those must be whole numbers
576_FORMS = {
577 "check": ("check DIR R WAVE MIN_ROUNDS ATTEMPT", 4, 4, 4),
578 "append": ("append DIR R", 1, 1, 1),
579 "gate": ("gate DIR [R]", 0, 1, 1),
580 "answers": ("answers DIR Q1 [Q2 ...]", 1, None, 0),
581}
584def _malformed(argv: list) -> str:
585 """'' when the command line has the right shape, else an ERROR line."""
586 cmd, rest = argv[1], argv[3:]
587 if cmd not in _FORMS:
588 return f"ERROR: unknown command {cmd!r}. {USAGE}; nothing was touched"
589 form, lo, hi, nints = _FORMS[cmd]
590 if len(argv) < 3 or len(rest) < lo or (hi is not None and len(rest) > hi):
591 return f"ERROR: usage: ledger.py {form} (DIR first, as an absolute path); nothing was touched"
592 d = Path(argv[2])
593 if not d.is_dir():
594 return f"ERROR: '{d}' is not an existing run directory; give the run directory's absolute path first (ledger.py {form}); nothing was touched"
595 if not all(a.isascii() and a.isdigit() for a in rest[:nints]):
596 return f"ERROR: usage: ledger.py {form}; the arguments after DIR must be whole numbers (got {' '.join(rest[:nints])}); nothing was touched"
597 return ""
600def main(argv: list) -> str:
601 if len(argv) < 2 or argv[1] in ("-h", "--help"):
602 return USAGE
603 try:
604 bad = _malformed(argv)
605 if bad:
606 return bad
607 cmd = argv[1]
608 d = Path(argv[2])
609 if cmd == "append":
610 return f"APPENDED {append(d, int(argv[3]))}"
611 if cmd == "gate": # on ledger.md as it stands, plus round R's pending block if R given
612 text = ledger_text(d)
613 if len(argv) > 3:
614 r = int(argv[3])
615 bp = d / f"round{r}_ledger_block.md"
616 text = ledger_text(d, before=r) + "".join(
617 f"{ln}\n"
618 for ln in numbered_lines(
619 d, r, bp.read_text(**ENC) if bp.exists() else ""
620 )
621 )
622 why = gate_reason(text, known_locators(d))
623 return "CONCLUDE" if not why else f"REJECT: {why}"
624 if cmd == "answers":
625 return answers(d, argv[3:])
626 if cmd == "check":
627 r, wave, min_rounds, attempt = (int(x) for x in argv[3:7])
628 # the orchestrator's attempt count is advisory: every RETRY this
629 # script has already issued for round r is logged, so a confused
630 # caller passing attempt=1 forever still reaches the terminal
631 # verdicts after MAX_ATTEMPTS plan steps
632 logp = d / "judge" / f"plan_r{r}_retries.log"
633 issued = len(logp.read_text(**ENC).splitlines()) if logp.exists() else 0
634 attempt = max(attempt, issued + 1)
635 verdict = check(d, r, wave, min_rounds, attempt)
636 if verdict.startswith("RETRY"):
637 logp.parent.mkdir(parents=True, exist_ok=True)
638 with logp.open("a", encoding="utf-8") as f:
639 f.write(f"attempt {attempt}: {verdict[:120]}\n")
640 # corrections are pasted into a brief whose paths are absolute
641 return verdict.replace("DIR/", str(d).rstrip("/") + "/")
642 return USAGE
643 except Exception as e: # fail closed, in words the orchestrator can relay
644 if len(argv) > 1 and argv[1] == "answers":
645 return f"ERROR: the bookkeeping script could not classify the answer files ({type(e).__name__}: {str(e)[:200]}); check DIR and the query stems and run the command again"
646 attempt = 0
647 try:
648 attempt = int(argv[6]) if len(argv) > 6 and argv[1] == "check" else 0
649 except ValueError:
650 pass
651 err = f"the bookkeeping script could not process this round's files ({type(e).__name__}: {str(e)[:200]})"
652 if attempt >= MAX_ATTEMPTS:
653 return f"TAIL: {err}, still failing after {attempt} attempts"
654 return f"RETRY: Correction — {err}; re-check the file names and formats the brief asks for and write them again."
657if __name__ == "__main__":
658 try: # the verdict goes out as UTF-8 whatever the console's code page (Windows)
659 sys.stdout.reconfigure(encoding="utf-8", errors="replace")
660 except (AttributeError, ValueError):
661 pass
662 print(main(sys.argv))