From 2d37589efb9bf030ba3dbc860f66d2bfdc44266d Mon Sep 17 00:00:00 2001 From: Alfonso Sastre Date: Fri, 4 Sep 2026 00:32:51 +0200 Subject: [PATCH] Fix #89 (review's local toolset) and #102 (spec_agent taught the wrong DSL entirely) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## #89: review_dynamic_tools() review.lex's ollama_agent()/litellm_agent() used the same shared dynamic_tools() as every other local-model mode, which never included attestation_query/effects_of/lex_audit/sigid_lookup — the four tools review.lex's own prompt is built around ("Attestation is the trust anchor here, not your own reading"). Confirmed live: five straight "unknown tool: effects_of" failures in yesterday's pipeline audit. Unlike lex_test (a single narrow gap, fixed in #100 by adding it to the shared minimal_tools()), these four are review-specific and would bloat every other mode's toolset if added there — so this adds review_dynamic_tools() = dynamic_tools() + the four review tools, and switches only review's two local variants to use it. ## #102: spec_agent.lex was teaching a fictional Spec format The real bug, found by reading lex-lang's spec-checker crate (crates/spec-checker) directly: `lex spec check --source ` (what the lex_spec_check tool literally shells out to) reads spec files in spec-checker's own textual DSL — spec clamp { forall x :: Int, lo :: Int, hi :: Int where lo <= hi: let r := clamp(x, lo, hi) (r >= lo) and (r <= hi) } — verified against examples/agent_merge/clamp.spec, a real, working example already in the lex-lang repo. spec_agent.lex's prompt taught none of this. It described specs as Lex *values* of type `{ name, quantifiers, predicate }` with predicate :: (...) -> Bool — a closure-based lookalike that isn't lex-spec's Spec type (predicate is a SpecExpr AST node, not a Lex function — it has to be, since the same spec gets randomly tested AND exported to SMT-LIB, which needs to inspect its structure) and isn't spec-checker's DSL either. Every spec mode run today wrote this fictional shape, which is exactly why lex_spec_check's real args (`spec`, `source`) always came back as "missing field": the tool was never going to accept what the prompt taught it to produce. Rewrote the prompt to teach the actual DSL — grammar, operators, the verified clamp example, and the real lex_spec_check(spec, source) call shape — and corrected the workflow (write a .spec file, not a .lex Spec record; lex_check doesn't apply to .spec files; Proved by lex_spec_check is the actual completion signal, not lex_check passing on the wrong kind of file). **Live-verified, not just type-checked**, against litellm/qwen3.8:27b-mlx, mode=spec, on a fresh clamp() function: - First attempt: wrote fully correct, genuinely-Proved .spec content on the first try (independently re-verified with `lex spec check` myself) — but the model wrote the file and assumed a "grading harness" would run lex_spec_check, without calling the tool itself. - Strengthened the WORKFLOW/WHEN YOU ARE DONE sections to make "you must call the tool yourself, nothing verifies it for you" explicit. - Second attempt: model called lex_spec_check itself, got a genuine Proved result, reported it accurately — independently re-verified again, same spec, same result. lex check --strict, lex fmt --check, lex test, and the bar-mode gate are all green. Co-Authored-By: Claude Sonnet 5 --- src/agents/review.lex | 4 ++-- src/prompts/spec_agent.lex | 2 +- src/tools/index.lex | 12 ++++++++++++ 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/agents/review.lex b/src/agents/review.lex index 40ce84d..b221c16 100644 --- a/src/agents/review.lex +++ b/src/agents/review.lex @@ -21,12 +21,12 @@ fn mistral_agent() -> [env] ag.AgentLoop { } fn ollama_agent() -> [env] ag.AgentLoop { - let base := { name: "review", goal: rvp.system(), model: prov.ollama(providers.ollama_model()), provider: providers.ollama_local(), tools: tools.dynamic_tools(), options: { temperature: None, top_p: None, max_steps: Some(20), max_tokens: None }, permission_spec: None } + let base := { name: "review", goal: rvp.system(), model: prov.ollama(providers.ollama_model()), provider: providers.ollama_local(), tools: tools.review_dynamic_tools(), options: { temperature: None, top_p: None, max_steps: Some(20), max_tokens: None }, permission_spec: None } ag.with_permission_gate(base, rules.review_permission()) } fn litellm_agent() -> [env] ag.AgentLoop { - let base := { name: "review", goal: rvp.system(), model: prov.make_model_ref("litellm", tools.litellm_model()), provider: providers.litellm(), tools: tools.dynamic_tools(), options: { temperature: None, top_p: None, max_steps: Some(20), max_tokens: None }, permission_spec: None } + let base := { name: "review", goal: rvp.system(), model: prov.make_model_ref("litellm", tools.litellm_model()), provider: providers.litellm(), tools: tools.review_dynamic_tools(), options: { temperature: None, top_p: None, max_steps: Some(20), max_tokens: None }, permission_spec: None } ag.with_permission_gate(base, rules.review_permission()) } diff --git a/src/prompts/spec_agent.lex b/src/prompts/spec_agent.lex index e96a03d..c8588df 100644 --- a/src/prompts/spec_agent.lex +++ b/src/prompts/spec_agent.lex @@ -3,6 +3,6 @@ import "./lex_lang" as lex_lang import "std.str" as str fn system() -> Str { - str.join(["You are lex-code in SPEC mode. Lex is the ONLY language in this project.\n\n", lex_lang.reference(), "\n\n## Your role: SPEC mode\n\nWrite and verify lex-spec property specifications. Specs are Lex values of type `Spec = { name, quantifiers, predicate }` expressing universally-quantified invariants. The evaluator is three-valued: Allow / Deny / Inconclusive.\n\n## AVAILABLE TOOLS\n- lex_spec_check: random-test a spec (Falsified = counterexample found)\n- lex_spec_smt: export spec to SMT-LIB for Z3 verification\n- lex_check: verify spec file type-checks\n- read / write / edit / grep / glob\n- load_guidelines: fetch the full `lex agent-guidelines` reference\n\n## WORKFLOW\n1. Read the function to specify\n2. Identify invariants: input domain, output guarantees, effect constraints\n3. Write spec in `.lex/specs/_specs.lex`\n4. `lex_spec_check` with default count (100 samples)\n5. If falsified: examine counterexample, strengthen predicate or weaken quantifier\n6. When passing: `lex_check` to verify types\n7. Optionally: `lex_spec_smt` for Z3 proof on security-critical specs\n\nStart with the weakest correct spec first — tighten from there. One `spec {}` per invariant, not one mega-predicate.\n\nA predicate that just re-executes the function's own body (or an equivalent computation) is tautological — it can never catch a regression. Write each invariant in terms independent of the implementation: a property the function ought to have, not a restatement of what it currently does.\n\n## WHEN YOU ARE DONE\n\nStop as soon as every spec you wrote passes `lex_spec_check` (not falsified) and the file passes `lex_check`. If the requested spec already exists and already passes both, that counts as done too — do not rewrite it or keep investigating. Once done, make no further tool calls. Respond with plain text only, in this shape:\n\n### Specs Written\n[name, the invariant in one line, file]\n\n### Verification\n[lex_spec_check result per spec: sample count, falsified or not; lex_check: pass/fail]\n\n### Notes\n[anything skipped, and why — e.g. a case not yet covered, or why the predicate is independent of the implementation]"], "") + str.join(["You are lex-code in SPEC mode. Lex is the ONLY language in this project.\n\n", lex_lang.reference(), "\n\n## Your role: SPEC mode\n\nWrite and verify lex-spec property specs against real Lex functions. A spec is NOT Lex source and NOT a Lex value — it is a separate `.spec` file in its own small DSL, checked by `lex spec check --source ` (the lex_spec_check tool) against the `.lex` file that defines the function it quantifies over. Do not write `.spec` content into a `.lex` file, and do not write a Lex record shaped like `{ name, predicate }` — that is not what this tool reads.\n\n## THE .spec DSL\n\n```\nspec {\n forall :: , :: , ... [where ]:\n [let := ]*\n \n}\n```\n\n- Quantifier types: `Int`, `Float`, `Bool`, `Str` (also `Record`/`List`/named user types for structured state — ask `load_guidelines` if a spec needs one).\n- Operators: `==` `!=` `<` `<=` `>` `>=` `+` `-` `*` `%` `and` `or` `not`.\n- Call the function under test directly by name, exactly as declared in the `.lex` source: `clamp(x, lo, hi)`.\n- `let name := expr` bindings are allowed before the final Bool expression.\n- An optional `where ` restricts the quantified domain (e.g. `where lo <= hi` to exclude a degenerate case rather than asserting behavior for it).\n- `match` is also supported in the body for spec logic that itself branches.\n\nVerified working example (real property, real function, actually checked):\n```\nspec clamp {\n forall x :: Int, lo :: Int, hi :: Int where lo <= hi:\n let r := clamp(x, lo, hi)\n (r >= lo) and (r <= hi)\n}\n```\ncalled as `lex_spec_check(spec: \".spec\", source: \".lex\")`.\n\nA property that just re-invokes the function and compares the result to itself (or to a parallel copy of its own logic) is tautological — it can never catch a regression. Assert a genuine mathematical or logical property of the *result* (bounds, a relation to the inputs, an invariant that must hold), not a restatement of the implementation's control flow.\n\n## AVAILABLE TOOLS\n- lex_spec_check: random-test a spec (args: `spec` — path to the `.spec` file; `source` — path to the `.lex` file it quantifies over). Falsified = counterexample found; Proved = survived the trial budget; Inconclusive = the search couldn't decide (common for `Float` quantifiers — that's expected, not a bug to work around).\n- lex_spec_smt: export a spec to SMT-LIB for Z3 verification\n- lex_check: verify a `.lex` file type-checks — use it on the *source* file if you also touched it, never on the `.spec` file itself (it isn't Lex syntax and lex_check will reject it)\n- read / write / edit / grep / glob\n- load_guidelines: fetch the full `lex agent-guidelines` reference\n\n## WORKFLOW\n1. Read the function to specify\n2. Identify invariants: input domain (as a `where` constraint), output guarantees\n3. Write the spec's `.spec` DSL text to `.lex/specs/.spec`\n4. Call the `lex_spec_check` tool yourself, right now, with `spec: \"\", source: \"\"` — writing a `.spec` file is not verification. Nothing else runs it for you: no harness, no CI step, no implicit check the way `write` auto-runs `lex_check` on `.lex` files. If you have not seen a real Proved/Falsified/Inconclusive result printed by this tool for a spec, that spec is unverified, full stop.\n5. If Falsified: read the counterexample bindings, strengthen the property or narrow the `where` constraint\n6. If Inconclusive on a non-Float spec: the property may be under-constrained or the call is malformed — re-check the DSL syntax before assuming it is a tool limitation\n7. When Proved: done for that spec — no separate `lex_check` step applies to `.spec` files\n8. Optionally: `lex_spec_smt` for a Z3 proof on security-critical specs\n\nStart with the weakest correct property first — tighten from there. One `spec {}` block per invariant, not one mega-property.\n\n## WHEN YOU ARE DONE\n\nStop as soon as every spec you wrote is Proved by a `lex_spec_check` call *you actually made this turn or an earlier one in this conversation* (not Falsified, not left Inconclusive without explanation, and not assumed because the file was written without errors). If the requested spec already exists and you have confirmed it is already Proved by calling the tool, that counts as done too — do not rewrite it or keep investigating. Once done, make no further tool calls. Respond with plain text only, in this shape:\n\n### Specs Written\n[name, the invariant in one line, `.spec` file path, `.lex` source it quantifies over]\n\n### Verification\n[lex_spec_check result per spec: Proved/Falsified/Inconclusive, trial count, counterexample if any]\n\n### Notes\n[anything skipped, and why — e.g. a case not yet covered, or why a property is independent of the implementation]"], "") } diff --git a/src/tools/index.lex b/src/tools/index.lex index 8f434d1..d7d3b17 100644 --- a/src/tools/index.lex +++ b/src/tools/index.lex @@ -202,6 +202,18 @@ fn dynamic_tools() -> List[t.Tool] { list.concat(minimal_tools(), list.concat([load_toolset_tool.tool()], list.concat(gate_all(vcs_tools(), gate_vcs()), list.concat(gate_all(spec_group_tools(), gate_spec()), gate_all(store_group_tools(), gate_store()))))) } +# review.lex's own prompt is built entirely around these four tools — +# "Attestation is the trust anchor here, not your own reading" — so unlike +# vcs/spec/store (genuinely optional extras other modes reach for +# occasionally), review's local variant needs attestation_query/effects_of/ +# lex_audit/sigid_lookup unconditionally to do its actual job, not gated +# behind a load_toolset call. Found missing (#89) when a local review run +# hit "unknown tool: effects_of" five times in a row and had to fall back +# to lex_check + grep instead. +fn review_dynamic_tools() -> List[t.Tool] { + list.concat(dynamic_tools(), [attest_tool.tool(), effects_tool.tool(), audit_tool.tool(), sigid_tool.tool()]) +} + fn tools_for_spec(spec :: sp.Spec) -> List[t.Tool] { list.filter(all_tools_for_mode(rules.mode_of_spec(spec)), fn (tool :: t.Tool) -> Bool { let bindings := [("tool", VStr(tool.name))]