diff --git a/README.md b/README.md index acc8a61..a8de937 100644 --- a/README.md +++ b/README.md @@ -751,6 +751,20 @@ src/list.lex`), and a file is not a function, so neither criterion can say attestation graph, which is what `lex blame --with-evidence` reads and what `attestation_query` calls the stronger signal. +`verified.type_check`/`.spec_check`/`.test` are written by lex-llm's own +dispatcher whenever `lex_check`/`lex_spec_check`/`lex_test` reports a pass — +mechanical evidence the tool actually ran and actually passed, not the +model's word for it. `verified.independent_check` is the fourth kind, and +it is lex-code's own: a bare `lex_run` pass proves nothing on its own (an +ordinary build-mode run passing is not evidence of anything beyond "the +function didn't crash"), so it is written directly by +`impl_test_fix_loop_verified`'s fix-loop gate (`graph.lex`'s +`attest_verify_pass_if_clean`) only when a `verify`-mode agent's own +`lex_run` came back clean — the strongest evidence in the system, since +verify re-derives the expected output instead of trusting anything on +disk. A task spec can require it the same way as the others: +`verified = ["verified.independent_check"]`. + ### Pipeline specs A spec is two characters of grammar: `,` runs stages in order, `|` runs them diff --git a/src/server/graph.lex b/src/server/graph.lex index e5f0cbd..58f66ae 100644 --- a/src/server/graph.lex +++ b/src/server/graph.lex @@ -39,6 +39,8 @@ import "std.process" as proc import "./session" as sess +import "../verification" as verification + # `task_prefix` is what the old runner did inline — `"Write unit tests # for: " ++ task`. Making it a field is what lets a caller build a node # for work the presets never anticipated. @@ -622,12 +624,58 @@ fn run_agent_with_events(def :: AgentDef, task :: Str, provider_tag :: Str) -> [ let ended := time.now_ms() match trail_log.range(result.session.log, started, ended) { Err(_) => ({ name: def.name, steps: result.steps }, []), - Ok(events) => ({ name: def.name, steps: result.steps }, events), + Ok(events) => { + let __attested := attest_verify_pass_if_clean(result.session.log, events) + ({ name: def.name, steps: result.steps }, events) + }, } }, } } +# lex-code#32: verify mode's own pass is never one of lex-llm's `verified.*` +# kinds — `lex_run` (what verify's own convention runs its checks through) +# isn't a tool `verified_kind_for_tool` recognizes, and it shouldn't be +# recognized generically there either: an ordinary build-mode `lex_run` +# passing proves nothing, only a VERIFY-mode one that found no FAIL does. +# So a clean pass here — the strongest evidence in the whole system, an +# independent re-derivation that never trusted the implementation — left +# no durable trace for a later `review` agent or `task_spec.lex` criterion +# to find. Attest it directly, reusing `verification.lex`'s own +# Record/harvest/append_all rather than inventing a second mechanism. +# +# Guarded on "did this turn's tool output actually contain a `lex_run` +# result at all", not just "no FAIL found in it" — a session that errored +# out before running anything has an empty event list, and `false` is the +# 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 { + if list.is_empty(tool_result_texts(events)) { + () + } else { + if verify_found_failure(events) { + () + } else { + match trail_log.append(log, independent_check_kind(), None, "{\"tool\":\"lex_run\",\"target\":\"\",\"result\":\"pass\"}") { + Err(_) => (), + Ok(evt) => { + let __promoted := verification.append_all(verification.harvest(log, evt.ts_ms, evt.ts_ms + 1)) + () + }, + } + } + } +} + +fn independent_check_kind() -> Str + examples { + independent_check_kind() => "verified.independent_check" + } +{ + "verified.independent_check" +} + # ---- the fix loop ------------------------------------------------------- # # Runs `setup` once, then mechanically verifies with a real subprocess — @@ -881,7 +929,10 @@ fn run_agent_persistent_with_events(def :: AgentDef, task :: Str, provider_tag : let ended := time.now_ms() match trail_log.range(result.session.log, started, ended) { Err(_) => ({ name: def.name, steps: result.steps }, []), - Ok(events) => ({ name: def.name, steps: result.steps }, events), + Ok(events) => { + let __attested := attest_verify_pass_if_clean(result.session.log, events) + ({ name: def.name, steps: result.steps }, events) + }, } }, } diff --git a/src/verification.lex b/src/verification.lex index a51198d..9694e1a 100644 --- a/src/verification.lex +++ b/src/verification.lex @@ -57,13 +57,21 @@ fn path() -> Str ".lex/verified.jsonl" } -# The event kinds lex-llm writes when a verification tool reports a pass. +# The event kinds a verification tool reports a pass under. The first +# three are lex-llm's own (`verified_kind_for_tool` in lex-llm/agent.lex); +# `verified.independent_check` is lex-code's own, written directly by +# `graph.lex`'s fix-loop verify gate rather than by lex-llm's dispatcher — +# `lex_run` (what verify mode's own convention runs its checks through) +# isn't one of the tool names that dispatcher recognizes, and adding it +# there would need lex-llm to also know a call came from Verify mode +# specifically, since an ordinary build-mode `lex_run` passing proves +# nothing (lex-code#32). fn verified_kinds() -> List[Str] examples { - verified_kinds() => ["verified.type_check", "verified.spec_check", "verified.test"] + verified_kinds() => ["verified.type_check", "verified.spec_check", "verified.test", "verified.independent_check"] } { - ["verified.type_check", "verified.spec_check", "verified.test"] + ["verified.type_check", "verified.spec_check", "verified.test", "verified.independent_check"] } fn is_verified_kind(kind :: Str) -> Bool