From 655342db3602601284fa81db621e6bdd455ca3be Mon Sep 17 00:00:00 2001 From: Alfonso Sastre Date: Tue, 8 Sep 2026 21:54:08 +0200 Subject: [PATCH] verification: fix sig_for so a directory target can ever be Fresh MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit verified.test/verified.spec_check records always name a directory (lex_test/lex_spec_check's own tool arg, e.g. "tests" — never a single file). sig_for used io.read unconditionally, which always errors on a directory, so harvest always stamped these records with sig: "". Since is_fresh treats a non-empty target with an empty sig as always Stale, VerifiedKindSeen("verified.test") and VerifiedTargetSeen(_, "verified.test") were permanently unsatisfiable for every project that ever asks for them -- not flaky, 100% reproducible, for as long as the tool's target stayed a directory. Found live in lex-economy: the `treasury` task was the first task in that project to ask for verified.test at all (identity/contract/ reputation only ever asked for verified.type_check), so this had never been exercised before. Fix: sig_for now falls back to hashing the sorted concatenation of every file's path+content under a directory when a plain io.read fails. Deliberately shells through `find` (`[proc]`) rather than std.fs.walk (`[fs_walk]`): sig_for is called from linter.lex's record_verified, which runs from inside edit/write's Tool.execute -- a row FIXED by the Tool record type at [net, io, proc] (effect rows unify by equality, not subtyping), so fs_walk is not an option there. This reuses the same proc-instead-of-the-typed-effect trade record_verified's own comment already documents for mkdir, rather than inventing a second one -- and needed only 3 downstream signatures widened (harvest, finish_turn, attest_verify_pass_if_clean; task_spec's is_fresh/presence/presence_on/target_outcome/verified_outcome), not the 20+ files a naive fs_walk widening cascades into. Single-file targets are unaffected: io.read is tried first, so an existing sig's meaning does not shift for the common case. lex check (104 files), lex fmt --check, lex doc-sync --check, and lex test tests all pass. Co-Authored-By: Claude Sonnet 5 --- src/server/graph.lex | 2 +- src/server/session.lex | 2 +- src/task_spec.lex | 14 +++--- src/verification.lex | 101 +++++++++++++++++++++++++++++++++++++++-- 4 files changed, 106 insertions(+), 13 deletions(-) diff --git a/src/server/graph.lex b/src/server/graph.lex index 58f66ae..de80ffc 100644 --- a/src/server/graph.lex +++ b/src/server/graph.lex @@ -650,7 +650,7 @@ fn run_agent_with_events(def :: AgentDef, task :: Str, provider_tag :: Str) -> [ # vacuous, wrong answer to "did verify find a failure" for that case. Same # trap `lex test`'s own empty-directory bug taught this session to guard # against (lex-lang v0.10.17); the fix here is the same shape. -fn attest_verify_pass_if_clean(log :: trail_log.Log, events :: List[trail_ev.Event]) -> [io, sql, time] Unit { +fn attest_verify_pass_if_clean(log :: trail_log.Log, events :: List[trail_ev.Event]) -> [io, sql, time, proc] Unit { if list.is_empty(tool_result_texts(events)) { () } else { diff --git a/src/server/session.lex b/src/server/session.lex index 9eda7ea..e953d42 100644 --- a/src/server/session.lex +++ b/src/server/session.lex @@ -453,7 +453,7 @@ fn refused_turn_streamed(session :: Session, reason :: Str, on_step :: (d.Step) # cache. A FAILED assistant append is deliberately not patched over — the # cache keeps the message anyway, so the next turn's derivation check finds # the divergence and refuses loudly. Noisy failure over silent context loss. -fn finish_turn(session :: Session, derived :: List[msg.Message], steps :: List[d.Step], started_ms :: Int) -> [env, net, io, sql, time] TurnResult { +fn finish_turn(session :: Session, derived :: List[msg.Message], steps :: List[d.Step], started_ms :: Int) -> [env, net, io, sql, time, proc] TurnResult { let ended := time.now_ms() let __harvested := verification.append_all(verification.harvest(session.log, started_ms, ended)) let __exported := obs.export_turn(session.id, session.log, started_ms, ended) diff --git a/src/task_spec.lex b/src/task_spec.lex index d467fa7..0e777d0 100644 --- a/src/task_spec.lex +++ b/src/task_spec.lex @@ -270,7 +270,7 @@ fn malformed_outcome(entry :: Str) -> Outcome # records (`target == ""`) have no single file to hash against, so they are # never stale by this check; that is the same limitation `sig_for` already # documents, not a new one. -fn is_fresh(r :: verification.Record) -> [io] Bool { +fn is_fresh(r :: verification.Record) -> [io, proc] Bool { if str.is_empty(r.target) { true } else { @@ -305,8 +305,8 @@ fn upgrade(acc :: Presence, hit :: Bool, fresh :: Bool) -> [io] Presence { } } -fn presence_on(records :: List[verification.Record], target :: Str, kind :: Str) -> [io] Presence { - list.fold(records, Absent, fn (acc :: Presence, r :: verification.Record) -> [io] Presence { +fn presence_on(records :: List[verification.Record], target :: Str, kind :: Str) -> [io, proc] Presence { + list.fold(records, Absent, fn (acc :: Presence, r :: verification.Record) -> [io, proc] Presence { let hit := r.kind == kind and r.target == target upgrade(acc, hit, if hit { is_fresh(r) @@ -316,8 +316,8 @@ fn presence_on(records :: List[verification.Record], target :: Str, kind :: Str) }) } -fn presence(records :: List[verification.Record], kind :: Str) -> [io] Presence { - list.fold(records, Absent, fn (acc :: Presence, r :: verification.Record) -> [io] Presence { +fn presence(records :: List[verification.Record], kind :: Str) -> [io, proc] Presence { + list.fold(records, Absent, fn (acc :: Presence, r :: verification.Record) -> [io, proc] Presence { let hit := r.kind == kind upgrade(acc, hit, if hit { is_fresh(r) @@ -327,7 +327,7 @@ fn presence(records :: List[verification.Record], kind :: Str) -> [io] Presence }) } -fn target_outcome(label :: Str, target :: Str, kind :: Str) -> [io] Outcome { +fn target_outcome(label :: Str, target :: Str, kind :: Str) -> [io, proc] Outcome { match presence_on(verification.all(), target, kind) { Fresh => { label: label, met: true, detail: "" }, Stale => { label: label, met: false, detail: str.join(["a ", kind, " record exists for ", target, " but it no longer matches the file's current content — re-run the check"], "") }, @@ -335,7 +335,7 @@ fn target_outcome(label :: Str, target :: Str, kind :: Str) -> [io] Outcome { } } -fn verified_outcome(label :: Str, kind :: Str) -> [io] Outcome { +fn verified_outcome(label :: Str, kind :: Str) -> [io, proc] Outcome { match presence(verification.all(), kind) { Fresh => { label: label, met: true, detail: "" }, Stale => { label: label, met: false, detail: str.join(["a ", kind, " record exists in this project but no longer matches its target's current content — re-run the check"], "") }, diff --git a/src/verification.lex b/src/verification.lex index 9694e1a..a06da0d 100644 --- a/src/verification.lex +++ b/src/verification.lex @@ -32,6 +32,8 @@ import "lex-schema/json_value" as jv import "std.io" as io +import "std.process" as proc + import "std.str" as str import "std.list" as list @@ -170,18 +172,109 @@ fn record_of(e :: ev.Event) -> Option[Record] } } +# Plain insertion sort over Str — std.list has no `sort` (the same family +# of gap as the missing `map.fold`), and `sig_for_dir` below needs a +# stable, content-derived file order rather than whatever `find` happens +# to print (readdir order is not guaranteed stable across calls). Str +# supports `<=` natively. +fn insert_sorted(sorted :: List[Str], x :: Str) -> List[Str] + examples { + insert_sorted([], "b") => ["b"], + insert_sorted(["b"], "a") => ["a", "b"], + insert_sorted(["a", "c"], "b") => ["a", "b", "c"] + } +{ + if list.is_empty(sorted) { + [x] + } else { + match list.head(sorted) { + None => [x], + Some(h) => if x <= h { + list.concat([x], sorted) + } else { + list.concat([h], insert_sorted(list.tail(sorted), x)) + }, + } + } +} + +fn sort_strs(xs :: List[Str]) -> List[Str] + examples { + sort_strs([]) => [], + sort_strs(["c", "a", "b", "a"]) => ["a", "a", "b", "c"] + } +{ + list.fold(xs, [], insert_sorted) +} + +# `target` is a DIRECTORY for every `lex_test`/`lex_spec_check` record +# (their tool arg is a path like "tests", never a single file) — `io.read` +# on a directory always errors, which used to fall straight through to +# `sig_for`'s "can't read" branch and return "" unconditionally. Combined +# with `is_fresh` (a non-empty target with an empty sig is always Stale), +# that made `verified.test`/`verified.spec_check` permanently +# unsatisfiable via `VerifiedKindSeen`/`VerifiedTargetSeen` — not flaky, +# every single time, for as long as the tool's target stayed a directory. +# Found live: lex-economy's `treasury` task was the first task in that +# project to ask for `verified.test` at all (its `identity`/`contract`/ +# `reputation` modules only ever asked for `verified.type_check`), so this +# had never been exercised before. +# +# Fixed by hashing the sorted concatenation of every file's path and +# content under the directory — deterministic, and it changes exactly +# when the directory's content does. Shelled through `find` (`[proc]`) +# rather than `std.fs.walk` (`[fs_walk]`) deliberately: `sig_for` is +# called from `linter.lex`'s `record_verified`, which runs from inside +# `edit`/`write`'s `Tool.execute` — a row FIXED by the `Tool` record type +# at `[net, io, proc]` (AGENTS.md; effect rows unify by equality, not +# subtyping), so adding `fs_walk` there is not an option without breaking +# that interface. `record_verified`'s own comment documents the same +# `proc`-instead-of-the-typed-effect trade for exactly this reason +# (`mkdir` instead of `std.fs.mkdir_p`) — this reuses the established +# pattern rather than inventing a second one. +fn sig_for_dir(target :: Str) -> [io, proc] Str { + match proc.run("find", [target, "-type", "f"]) { + Err(_) => "", + Ok(out) => if out.exit_code != 0 { + "" + } else { + let paths := list.filter(str.split(out.stdout, "\n"), fn (p :: Str) -> Bool { + not str.is_empty(p) + }) + if list.is_empty(paths) { + "" + } else { + let combined := list.fold(sort_strs(paths), "", fn (acc :: Str, p :: Str) -> [io] Str { + match io.read(p) { + Err(_) => acc, + Ok(content) => str.concat(acc, str.concat(p, content)), + } + }) + crypto.sha256_str(combined) + } + }, + } +} + # `target`'s content hash right now, or "" when there is nothing to hash — # an empty target (a whole-project-scope pass) or a target this process # can't read. "" is also what an unhashable record decodes to, so the two # cases are indistinguishable on purpose: both mean "cannot vouch for this # as fresh," which is the conservative side to fail on. -fn sig_for(target :: Str) -> [io] Str { +# +# Tries a plain file read first — the common case, and unchanged from +# before this function knew about directories, so no existing single-file +# sig's meaning shifts. Only falls through to `sig_for_dir` when that +# read fails, which is also what happens for a target that does not exist +# at all; `sig_for_dir` returns "" for that case too (find's own +# not-found error), so the fallback is safe either way. +fn sig_for(target :: Str) -> [io, proc] Str { if str.is_empty(target) { "" } else { match io.read(target) { - Err(_) => "", Ok(content) => crypto.sha256_str(content), + Err(_) => sig_for_dir(target), } } } @@ -198,10 +291,10 @@ fn sig_for(target :: Str) -> [io] Str { # `target` now, right after the turn that produced this record, is as close # to "the content this pass actually covered" as the session log leaves # reachable. -fn harvest(log :: trail_log.Log, since_ms :: Int, now_ms :: Int) -> [io, sql] List[Record] { +fn harvest(log :: trail_log.Log, since_ms :: Int, now_ms :: Int) -> [io, sql, proc] List[Record] { match trail_log.range(log, since_ms, now_ms) { Err(_) => [], - Ok(events) => list.fold(events, [], fn (acc :: List[Record], e :: ev.Event) -> [io] List[Record] { + Ok(events) => list.fold(events, [], fn (acc :: List[Record], e :: ev.Event) -> [io, proc] List[Record] { match record_of(e) { None => acc, Some(r) => list.concat(acc, [{ kind: r.kind, tool: r.tool, target: r.target, sig: sig_for(r.target), ts_ms: r.ts_ms }]),