feat: --refine=<id> + issue_propose — the agent proposes, a human approves (#173)

.github/workflows/ci.yml

@@ -45,7 +45,7 @@ jobs:
       - name: Install Lex toolchain
         run: |
           set -euxo pipefail
-          LEX_VERSION="0.11.66"
+          LEX_VERSION="0.11.68"
           # Backed off and limited: the release CDN returns a 504 often
           # enough to redden a build on its own, and re-running the job
           # by hand is not a fix. Retries are safe here — the request is

README.md

@@ -88,6 +88,7 @@ lex-code --plan --ollama "how should we structure the session module?"
 | `--bar` | Bar | Walk a project against the minimum bar, read-only ([below](#minimum-bar-mode)) |
 | `--multi` | Multi | Run Build + Test in parallel via `std.conc` |
 | `--issue=<id>` | Build | Implement a typed issue from its declared acceptance, then verify it ([below](#implementing-a-typed-issue)) |
+| `--refine=<id>` | Build | Propose a typed acceptance for a free-form issue; a human approves it ([below](#refining-a-free-form-issue)) |
 
 ### Implementing a typed issue
 
@@ -113,8 +114,29 @@ lex-code --issue=<id> ["optional extra guidance"]
    `[ISSUE_VERDICT]\t<verified|failed|inconclusive|unavailable>\t<id>`.
 
 `typed_delta` and `failing_example` issues close by proof. `free_form`,
-`metric_invariant` and `evidence` verify as `inconclusive` for now. For
-a `free_form` issue the agent ends by proposing a typed acceptance.
+`metric_invariant` and `evidence` verify as `inconclusive` for now.
+
+### Refining a free-form issue
+
+Not every issue starts with a contract. `--refine=<id>` has the agent read
+the code and **propose** one — exact signatures plus the examples that pin
+them, or the one failing example for a bug — with the `issue_propose`
+tool ([lex-lang #956](https://github.com/alpibrusl/lex-lang/issues/956)).
+It stops there: lex-code has no tool that approves, and the run ends by
+listing the proposals and the command that decides them.
+
+```sh
+lex-code --refine=<id>                         # agent proposes
+lex issue proposals <id>                       # review
+lex issue approve <proposal> --by <you>        # or: reject --notes "..."
+lex-code --issue=<id>                          # implement against the approved contract
+```
+
+Approving never rewrites the issue — its id, intents and verdicts stay
+put; the gate judges it against the latest approved proposal
+(`effective_acceptance` in `lex issue show`). `--refine` runs in Build
+mode with a prompt that forbids implementing; there is no dedicated
+read-only toolset yet (#88).
 
 ## Providers
 
@@ -585,6 +607,7 @@ for production interop.
 | `lex_test` | Run tests |
 | `issue_show` | Render a typed issue's acceptance as the contract to implement |
 | `issue_verify` | Evaluate a typed issue at head, record an `IssueVerified` attestation |
+| `issue_propose` | Propose a typed acceptance for a free-form issue (a human approves it) |
 
 ### Spec tools
 

lex.toml

@@ -1,7 +1,7 @@
 [package]
 name        = "lex-code"
 version     = "0.1.2"
-lex         = "0.11.66"
+lex         = "0.11.68"
 license     = "EUPL-1.2"
 description = "A Lex-native coding assistant — build/plan/explore/refactor/spec/test/review agents, TUI + A2A + ACP servers, lex-vcs tools."
 

src/issue_contract.lex

@@ -103,7 +103,7 @@ fn evidence_section(acc :: jv.Json) -> Str {
 }
 
 fn free_form_section() -> Str {
-  "Shape: free_form. There is no machine oracle — a human closes this issue. Work from the title and body, and end by proposing a typed acceptance (signatures + examples, or a failing example) that would have made it checkable.\n"
+  "Shape: free_form. There is no machine oracle yet — a human closes this issue. Work from the title and body. If you can state what \"done\" means as signatures + examples (or one failing example), call `issue_propose` with it: once a human approves the proposal, the gate judges this issue against it.\n"
 }
 
 fn acceptance_section(acc :: jv.Json) -> Str {
@@ -142,22 +142,41 @@ fn machine_closable(shape :: Str) -> Bool
   shape == "typed_delta" or shape == "failing_example"
 }
 
-fn shape_of(issue :: jv.Json) -> Str {
-  match jv.get_field(issue, "acceptance") {
-    None => "free_form",
-    Some(acc) => field_text(acc, "shape"),
+# The acceptance the gate evaluates: an approved proposal's
+# (`effective_acceptance`, #956) when the issue was refined, else its own.
+fn acceptance_of(issue :: jv.Json) -> jv.Json {
+  match jv.get_field(issue, "effective_acceptance") {
+    Some(a) => a,
+    None => match jv.get_field(issue, "acceptance") {
+      Some(a) => a,
+      None => JObj([]),
+    },
   }
 }
 
+fn shape_of(issue :: jv.Json) -> Str
+  examples {
+    shape_of(JObj([("acceptance", JObj([("shape", JStr("free_form"))]))])) => "free_form",
+    shape_of(JObj([("acceptance", JObj([("shape", JStr("free_form"))])), ("effective_acceptance", JObj([("shape", JStr("typed_delta"))]))])) => "typed_delta",
+    shape_of(JObj([])) => ""
+  }
+{
+  field_text(acceptance_of(issue), "shape")
+}
+
 # The build task for an issue: `lex issue show --output json` in, the
 # prompt the agent runs out.
 fn contract_prompt(issue :: jv.Json) -> Str {
   let id := field_text(issue, "issue_id")
   let body := field_text(issue, "body")
   let shape := shape_of(issue)
-  let acc := match jv.get_field(issue, "acceptance") {
-    None => JObj([]),
-    Some(a) => a,
+  let acc := acceptance_of(issue)
+  let refined := match jv.get_field(issue, "approved_proposal") {
+    None => "",
+    Some(p) => match jv.as_str(p) {
+      None => "",
+      Some(pid) => str.join(["(Filed free-form; refined by approved proposal ", pid, " — that acceptance is the contract.)\n"], ""),
+    },
   }
   let closing := if machine_closable(shape) {
     str.join(["\nDone is a proof, not a claim: call `issue_verify` with issue_id `", id, "` and iterate until its verdict is `verified`. A `failed` verdict's detail says exactly which signature or example is wrong. Every .lex file you write is published with this issue as its intent, so the ops link back to it.\n"], "")
@@ -168,7 +187,20 @@ fn contract_prompt(issue :: jv.Json) -> Str {
     ""
   } else {
     str.join(["\n", body, "\n"], "")
-  }, "\n", acceptance_section(acc), closing], "")
+  }, "\n", refined, acceptance_section(acc), closing], "")
+}
+
+# `--refine=<id>`: the agent's half of #956. It does the spec labor —
+# reads the code the issue is about and proposes what "done" means as a
+# typed acceptance — and stops there; approving is the human's.
+fn refine_prompt(issue :: jv.Json) -> Str {
+  let id := field_text(issue, "issue_id")
+  let body := field_text(issue, "body")
+  str.join(["Refine free-form issue ", id, ": ", field_text(issue, "title"), "\n", if str.is_empty(str.trim(body)) {
+    ""
+  } else {
+    str.join(["\n", body, "\n"], "")
+  }, "\nDo NOT implement it. Your job is to state what \"done\" means so a machine can check it:\n", bullets(["read the relevant code first (the package, existing signatures and naming) so the proposal fits it", "prefer typed_delta: the exact signatures to add/change/remove (`name:(a :: T, ...) -> R[:kind]`, one per line) plus examples `name(args) => expected` that pin the behavior, edge cases included", "use failing_example for a bug: the one example that fails today and must pass when fixed", str.join(["call `issue_propose` with issue_id `", id, "` and a rationale explaining why this captures the issue — more than one proposal is fine when the issue is genuinely ambiguous"], ""), "you cannot approve a proposal; end by summarising what you proposed and any judgment calls a human should check"])], "")
 }
 
 # `lex --output json issue verify` → the verdict word, or None when the

src/tools/index.lex

@@ -136,7 +136,7 @@ fn vcs_tools() -> List[t.Tool] {
 # calling it — it compares a file's effects against that mode's grant —
 # so the toolset has to be built per mode rather than shared.
 fn all_tools_for_mode(mode :: Str) -> List[t.Tool] {
-  list.concat([read_tool.tool(), write_tool.tool(), edit_tool.tool(), grep_tool.tool(), glob_tool.tool(), bash_tool.tool(), todo_tool.tool(), remember_tool.tool(), check_tool.tool(), os_check_tool.tool_for_mode(mode), audit_tool.tool(), semantic_search_tool.tool(), find_packages_tool.tool(), edit_files_tool.tool(), run_tool.tool(), test_tool.tool(), spec_check_tool.tool(), spec_smt_tool.tool(), sigid_tool.tool(), attest_tool.tool(), effects_tool.tool(), store_merge_tool.tool(), propagate_tool.tool(), guidelines_tool.tool(), bar_check_tool.tool(), github_pr_tool.tool(), github_pr_merge_tool.tool(), issue_tool.show_tool(), issue_tool.verify_tool()], vcs_tools())
+  list.concat([read_tool.tool(), write_tool.tool(), edit_tool.tool(), grep_tool.tool(), glob_tool.tool(), bash_tool.tool(), todo_tool.tool(), remember_tool.tool(), check_tool.tool(), os_check_tool.tool_for_mode(mode), audit_tool.tool(), semantic_search_tool.tool(), find_packages_tool.tool(), edit_files_tool.tool(), run_tool.tool(), test_tool.tool(), spec_check_tool.tool(), spec_smt_tool.tool(), sigid_tool.tool(), attest_tool.tool(), effects_tool.tool(), store_merge_tool.tool(), propagate_tool.tool(), guidelines_tool.tool(), bar_check_tool.tool(), github_pr_tool.tool(), github_pr_merge_tool.tool(), issue_tool.show_tool(), issue_tool.verify_tool(), issue_tool.propose_tool()], vcs_tools())
 }
 
 # The build agent's own toolset: build's grant forbids nothing, so this
@@ -169,7 +169,7 @@ fn all_tools() -> List[t.Tool] {
 # enough for the curated core; it doesn't need load_toolset gating the
 # way the heavier vcs/spec/store groups do.
 fn minimal_tools() -> List[t.Tool] {
-  [read_tool.tool(), write_tool.tool(), edit_tool.tool(), grep_tool.tool(), glob_tool.tool(), bash_tool.tool(), todo_tool.tool(), remember_tool.tool(), check_tool.tool(), run_tool.tool(), test_tool.tool(), stdlib_tool.tool(), guide_tool.tool(), cli_help_tool.tool(), find_packages_tool.tool(), edit_files_tool.tool(), issue_tool.show_tool(), issue_tool.verify_tool()]
+  [read_tool.tool(), write_tool.tool(), edit_tool.tool(), grep_tool.tool(), glob_tool.tool(), bash_tool.tool(), todo_tool.tool(), remember_tool.tool(), check_tool.tool(), run_tool.tool(), test_tool.tool(), stdlib_tool.tool(), guide_tool.tool(), cli_help_tool.tool(), find_packages_tool.tool(), edit_files_tool.tool(), issue_tool.show_tool(), issue_tool.verify_tool(), issue_tool.propose_tool()]
 }
 
 # Model name advertised to the LiteLLM proxy (must match a model_name in

src/tools/issue.lex

@@ -10,11 +10,20 @@
 # `detail` naming the wrong signature or example), so it reaches the
 # model as a successful tool result it can act on. Only a command that
 # could not answer — unknown issue, no store — is an Err.
+#
+# `issue_propose` (#956) is the agent's half of refining a free-form issue:
+# it proposes a typed acceptance, signed with the model that wrote it.
+# There is deliberately no approve tool — the human is the arbiter, and
+# `lex issue approve <proposal> --by WHO` is theirs to run.
 
 import "std.process" as proc
 
 import "std.str" as str
 
+import "std.list" as list
+
+import "std.io" as io
+
 import "lex-llm/tool" as t
 
 import "lex-schema/json_value" as jv
@@ -60,6 +69,83 @@ fn verify(args :: jv.Json) -> [net, io, proc] Result[jv.Json, e.Errors] {
   }
 }
 
+# One entry per non-blank line — how a model passes a list through a
+# string field without inventing a JSON-in-JSON encoding.
+fn lines(s :: Str) -> List[Str]
+  examples {
+    lines("a\n\n  b  \n") => ["a", "b"],
+    lines("") => []
+  }
+{
+  list.filter(list.map(str.split(s, "\n"), fn (l :: Str) -> Str {
+    str.trim(l)
+  }), fn (l :: Str) -> Bool {
+    not str.is_empty(l)
+  })
+}
+
+fn repeat_flag(flag :: Str, values :: List[Str]) -> List[Str]
+  examples {
+    repeat_flag("--api", ["a", "b"]) => ["--api", "a", "--api", "b"],
+    repeat_flag("--api", []) => []
+  }
+{
+  list.fold(values, [], fn (acc :: List[Str], v :: Str) -> List[Str] {
+    list.concat(acc, [flag, v])
+  })
+}
+
+fn opt_flag(flag :: Str, value :: Option[Str]) -> List[Str] {
+  match value {
+    None => [],
+    Some(v) => [flag, v],
+  }
+}
+
+type ProposeInput = { issue_id :: Str, shape :: Str, api :: Str, examples :: Str, predicate :: Option[Str], window :: Option[Str], subject :: Option[Str], invariants :: Str, rationale :: Str, by :: Str }
+
+# The `lex issue propose` argv for a proposal.
+fn propose_argv(p :: ProposeInput) -> List[Str]
+  examples {
+    propose_argv({ issue_id: "i1", shape: "typed_delta", api: "clamp:(x :: Int) -> Int", examples: "clamp(5) => 3\nclamp(0) => 0", predicate: None, window: None, subject: None, invariants: "", rationale: "r", by: "ollama/qwen" }) => ["--output", "json", "issue", "propose", "i1", "--shape", "typed_delta", "--api", "clamp:(x :: Int) -> Int", "--example", "clamp(5) => 3", "--example", "clamp(0) => 0", "--rationale", "r", "--by", "ollama/qwen"],
+    propose_argv({ issue_id: "i1", shape: "metric_invariant", api: "", examples: "", predicate: Some("p99 < 200"), window: Some("7d"), subject: None, invariants: "", rationale: "", by: "" }) => ["--output", "json", "issue", "propose", "i1", "--shape", "metric_invariant", "--predicate", "p99 < 200", "--window", "7d", "--rationale", "", "--by", ""]
+  }
+{
+  list.concat(util.json_cmd(["issue", "propose", p.issue_id, "--shape", p.shape]), list.concat(repeat_flag("--api", lines(p.api)), list.concat(repeat_flag("--example", lines(p.examples)), list.concat(opt_flag("--predicate", p.predicate), list.concat(opt_flag("--window", p.window), list.concat(opt_flag("--subject", p.subject), list.concat(repeat_flag("--invariant", lines(p.invariants)), ["--rationale", p.rationale, "--by", p.by])))))))
+}
+
+# Who is proposing: the turn's provider/model, as session.lex recorded it.
+fn proposer() -> [io] Str {
+  match io.read(".lex/intent/model") {
+    Err(_) => "lex-code",
+    Ok(m) => str.concat("lex-code/", str.trim(m)),
+  }
+}
+
+fn propose_params() -> s.ModelSchema {
+  { title: "IssueProposeArgs", description: "Propose a typed acceptance for a free_form issue; a human approves or rejects it.", fields: [s.required_str("issue_id", []), s.required_str("shape", []), s.optional(s.required_str("api", [])), s.optional(s.required_str("examples", [])), s.optional(s.required_str("predicate", [])), s.optional(s.required_str("window", [])), s.optional(s.required_str("subject", [])), s.optional(s.required_str("invariants", [])), s.required_str("rationale", [])] }
+}
+
+fn propose(args :: jv.Json) -> [net, io, proc] Result[jv.Json, e.Errors] {
+  match (util.field_str(args, "issue_id"), util.field_str(args, "shape")) {
+    (Some(id), Some(shape)) => {
+      let argv := propose_argv({ issue_id: id, shape: shape, api: util.field_str_or(args, "api", ""), examples: util.field_str_or(args, "examples", ""), predicate: util.field_str(args, "predicate"), window: util.field_str(args, "window"), subject: util.field_str(args, "subject"), invariants: util.field_str_or(args, "invariants", ""), rationale: util.field_str_or(args, "rationale", ""), by: proposer() })
+      match proc.run("lex", argv) {
+        Err(msg) => Err(e.single("", "proc_error", msg)),
+        Ok(out) => match util.cli_result(out) {
+          Err(detail) => Err(e.single("", "cli_failed", detail)),
+          Ok(body) => Ok(JStr(str.trim(body))),
+        },
+      }
+    },
+    _ => Err(e.single("", "missing", "issue_id and shape are required")),
+  }
+}
+
+fn propose_tool() -> t.Tool {
+  t.define("issue_propose", "Propose a typed acceptance for a free_form issue (lex issue propose). shape: typed_delta (api: one `name:signature[:added|changed|removed]` per line, e.g. `clamp:(x :: Int, lo :: Int, hi :: Int) -> Int`; examples: one `name(args) => expected` per line) | failing_example (examples: exactly one line) | metric_invariant (predicate, window) | evidence (subject, invariants one per line). rationale: why this captures the issue. Nothing changes until a HUMAN approves it; you cannot approve it yourself.", propose_params(), propose)
+}
+
 fn show_tool() -> t.Tool {
   t.define("issue_show", "Read a typed issue's declared acceptance (lex issue show) and render it as the contract to implement: exact signatures to add/change/remove, the examples that are its oracle, or the failing example to fix.", id_params("IssueShowArgs", "Show a typed issue's acceptance."), show)
 }

src/tools/smoke.lex

@@ -84,6 +84,7 @@ fn args_for(name :: Str) -> Option[jv.Json] {
     "find_packages" => Some(JObj([("query", JStr("gcd"))])),
     "issue_show" => Some(JObj([("issue_id", JStr("0000000000000000000000000000000000000000000000000000000000000000"))])),
     "issue_verify" => Some(JObj([("issue_id", JStr("0000000000000000000000000000000000000000000000000000000000000000"))])),
+    "issue_propose" => Some(JObj([("issue_id", JStr("0000000000000000000000000000000000000000000000000000000000000000")), ("shape", JStr("failing_example")), ("examples", JStr("f(1) => 1")), ("rationale", JStr("smoke"))])),
     _ => None,
   }
 }