feat: implement from a typed issue — --issue=<id>, issue_show/issue_verify (#173)

.github/workflows/ci.yml

@@ -45,7 +45,7 @@ jobs:
       - name: Install Lex toolchain
         run: |
           set -euxo pipefail
-          LEX_VERSION="0.11.32"
+          LEX_VERSION="0.11.66"
           # 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

@@ -87,6 +87,34 @@ lex-code --plan --ollama "how should we structure the session module?"
 | `--verify` | Verify | Independently re-derive expected output from the task's own spec and check the implementation against it — never trusts the implementation's existing test file ([below](#independent-verification-mode)) |
 | `--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)) |
+
+### Implementing a typed issue
+
+A [typed issue](https://github.com/alpibrusl/lex-lang/issues/949) is a
+contract, not a description: exact signatures to add, change, or remove,
+plus the examples that decide whether it holds (or, for a bug, the one
+example that fails at head). `--issue=<id>` works from that contract:
+
+```sh
+lex issue create --title "digit_sum" --shape typed_delta \
+  --api 'digit_sum:(n :: Int) -> Int:added' \
+  --example 'digit_sum(1234) => 10' --example 'digit_sum(-56) => 11'
+lex-code --issue=<id> ["optional extra guidance"]
+```
+
+1. `lex issue show` renders the acceptance as the task.
+2. The session is bound to the issue, so every clean `.lex` write is
+   published with `--intent-issue` and its ops link back to it
+   (issue → intent → ops → attestation).
+3. The agent iterates against the oracle with the `issue_verify` tool.
+4. Whatever the model claims, the run ends with `lex issue verify` and a
+   machine-readable last line:
+   `[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.
 
 ## Providers
 
@@ -555,6 +583,8 @@ for production interop.
 | `lex_audit` | Effect audit |
 | `lex_run` | Run a Lex expression |
 | `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 |
 
 ### Spec tools
 

lex.toml

@@ -1,7 +1,7 @@
 [package]
 name        = "lex-code"
 version     = "0.1.2"
-lex         = "0.11.32"
+lex         = "0.11.66"
 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

@@ -0,0 +1,196 @@
+# lex-code — implement from a typed issue (#173, lex-lang #949)
+#
+# A typed issue is the contract the manifesto asks an agent to work
+# from — "a type signature, a set of examples, a set of properties" —
+# rather than a codebase to imitate. `lex issue show <id>` hands back
+# its declared acceptance; this module turns that into the task the
+# build agent runs, and reads `lex issue verify`'s verdict back.
+#
+# Pure on purpose: everything that touches the CLI lives in the tools
+# (src/tools/issue.lex) and the `--issue` entry point (src/tui/main.lex),
+# so the rendering is covered by examples rather than by a live store.
+#
+# The acceptance, by shape (lex-store's `Acceptance`, serde tag "shape"):
+#   typed_delta      api: [{name, signature, kind}], examples: [Str]
+#   failing_example  example: Str   — fails at HEAD; fixed = passes
+#   metric_invariant predicate, window — a window over the event log
+#   evidence         subject, invariants — an attested chain
+#   free_form        nothing — human-closed, the explicit exception
+
+import "std.str" as str
+
+import "std.list" as list
+
+import "lex-schema/json_value" as jv
+
+fn field_text(j :: jv.Json, key :: Str) -> Str {
+  match jv.get_field(j, key) {
+    None => "",
+    Some(v) => match jv.as_str(v) {
+      None => "",
+      Some(s) => s,
+    },
+  }
+}
+
+fn field_list(j :: jv.Json, key :: Str) -> List[jv.Json] {
+  match jv.get_field(j, key) {
+    None => [],
+    Some(v) => match jv.as_list(v) {
+      None => [],
+      Some(xs) => xs,
+    },
+  }
+}
+
+fn texts(xs :: List[jv.Json]) -> List[Str] {
+  list.fold(xs, [], fn (acc :: List[Str], x :: jv.Json) -> List[Str] {
+    match jv.as_str(x) {
+      None => acc,
+      Some(s) => list.concat(acc, [s]),
+    }
+  })
+}
+
+fn bullets(lines :: List[Str]) -> Str
+  examples {
+    bullets([]) => "",
+    bullets(["a", "b"]) => "  - a\n  - b\n"
+  }
+{
+  str.join(list.map(lines, fn (l :: Str) -> Str {
+    str.join(["  - ", l, "\n"], "")
+  }), "")
+}
+
+# One API entry as the declaration the store will compare against:
+# `fn <name><signature>`. The gate compares whitespace-insensitively,
+# but the model should still copy it verbatim.
+fn api_line(entry :: jv.Json) -> Str {
+  let kind := field_text(entry, "kind")
+  let decl := str.join(["fn ", field_text(entry, "name"), field_text(entry, "signature")], "")
+  if kind == "removed" {
+    str.join(["REMOVE `", decl, "` — it must be absent at head"], "")
+  } else {
+    if kind == "changed" {
+      str.join(["CHANGE to `", decl, "` — this exact signature at head"], "")
+    } else {
+      str.join(["ADD `", decl, "` — this exact signature at head"], "")
+    }
+  }
+}
+
+fn typed_delta_section(acc :: jv.Json) -> Str {
+  let api := list.map(field_list(acc, "api"), api_line)
+  let examples := texts(field_list(acc, "examples"))
+  str.join(["Shape: typed_delta. The API delta is the contract:\n", bullets(api), if list.is_empty(examples) {
+    ""
+  } else {
+    str.join(["These examples are the oracle — each must hold at head. Put them in the function's own `examples { }` block so the store's write-time gate runs them on every publish:\n", bullets(examples)], "")
+  }], "")
+}
+
+fn failing_example_section(acc :: jv.Json) -> Str {
+  str.join(["Shape: failing_example (a bug report). This example FAILS at head today; the issue is fixed when it passes:\n", bullets([field_text(acc, "example")]), "Fix the implementation, not the example. Add the example to the function's `examples { }` block so it cannot regress.\n"], "")
+}
+
+fn metric_section(acc :: jv.Json) -> Str {
+  str.join(["Shape: metric_invariant. Predicate `", field_text(acc, "predicate"), "` must hold over the window `", field_text(acc, "window"), "`. The gate cannot evaluate this from code alone yet (it reports inconclusive); build what makes the predicate observable and true, and say what you could not verify.\n"], "")
+}
+
+fn evidence_section(acc :: jv.Json) -> Str {
+  str.join(["Shape: evidence. Subject `", field_text(acc, "subject"), "` needs an attested chain satisfying:\n", bullets(texts(field_list(acc, "invariants"))), "The gate reports inconclusive for this shape today; say what evidence you produced.\n"], "")
+}
+
+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"
+}
+
+fn acceptance_section(acc :: jv.Json) -> Str {
+  let shape := field_text(acc, "shape")
+  if shape == "typed_delta" {
+    typed_delta_section(acc)
+  } else {
+    if shape == "failing_example" {
+      failing_example_section(acc)
+    } else {
+      if shape == "metric_invariant" {
+        metric_section(acc)
+      } else {
+        if shape == "evidence" {
+          evidence_section(acc)
+        } else {
+          free_form_section()
+        }
+      }
+    }
+  }
+}
+
+# Whether the gate can close this issue by itself. Mirrors lex-store's
+# `Acceptance::is_machine_evaluable` for the shapes whose evaluator
+# exists at head (typed_delta, failing_example); the other three verify
+# as inconclusive today.
+fn machine_closable(shape :: Str) -> Bool
+  examples {
+    machine_closable("typed_delta") => true,
+    machine_closable("failing_example") => true,
+    machine_closable("free_form") => false,
+    machine_closable("metric_invariant") => false
+  }
+{
+  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 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 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"], "")
+  } else {
+    str.join(["\nWhen finished, call `issue_verify` with issue_id `", id, "` to record the verdict (expect `inconclusive` for this shape). Every .lex file you write is published with this issue as its intent.\n"], "")
+  }
+  str.join(["Implement typed issue ", id, ": ", field_text(issue, "title"), "\n", if str.is_empty(str.trim(body)) {
+    ""
+  } else {
+    str.join(["\n", body, "\n"], "")
+  }, "\n", acceptance_section(acc), closing], "")
+}
+
+# `lex --output json issue verify` → the verdict word, or None when the
+# command did not answer (unknown issue, no store). A `failed` verdict
+# exits 1 but is still `"ok": true` — an answer, not an error.
+fn verdict_of(stdout :: Str) -> Option[Str]
+  examples {
+    verdict_of("{\"ok\": true, \"data\": {\"verdict\": \"failed\", \"detail\": \"x\"}}") => Some("failed"),
+    verdict_of("{\"ok\": true, \"data\": {\"verdict\": \"verified\"}}") => Some("verified"),
+    verdict_of("{\"ok\": false, \"error\": {\"message\": \"unknown issue\"}}") => None,
+    verdict_of("error: unknown command `issue`") => None
+  }
+{
+  match jv.parse(str.trim(stdout)) {
+    Err(_) => None,
+    Ok(env) => match jv.get_field(env, "data") {
+      None => None,
+      Some(data) => match jv.get_field(data, "verdict") {
+        None => None,
+        Some(v) => jv.as_str(v),
+      },
+    },
+  }
+}
+

src/tools/index.lex

@@ -62,6 +62,8 @@ import "./vcs/op_replay" as vcs_op_replay_tool
 
 import "./vcs/recall" as vcs_recall_tool
 
+import "./issue" as issue_tool
+
 import "./vcs/op_push" as vcs_op_push_tool
 
 import "./vcs/op_pull" as vcs_op_pull_tool
@@ -134,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()], 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()], vcs_tools())
 }
 
 # The build agent's own toolset: build's grant forbids nothing, so this
@@ -167,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()]
+  [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()]
 }
 
 # Model name advertised to the LiteLLM proxy (must match a model_name in

src/tools/issue.lex

@@ -0,0 +1,70 @@
+# lex-code — typed issues as agent tools (#173, lex-lang #949)
+#
+# `issue_show` reads an issue's declared acceptance — the contract to
+# satisfy. `issue_verify` evaluates it at the store's head and records an
+# `IssueVerified` attestation: done is a proof the gate checks, never a
+# status the agent sets. Together they let the fix loop iterate against
+# the issue's own oracle rather than against the agent's reading of it.
+#
+# A `failed` verdict exits 1 but is still an answer (`"ok": true` with a
+# `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.
+
+import "std.process" as proc
+
+import "std.str" as str
+
+import "lex-llm/tool" as t
+
+import "lex-schema/json_value" as jv
+
+import "lex-schema/error" as e
+
+import "lex-schema/schema" as s
+
+import "../issue_contract" as ic
+
+import "./util" as util
+
+fn id_params(title :: Str, description :: Str) -> s.ModelSchema {
+  { title: title, description: description, fields: [s.required_str("issue_id", [])] }
+}
+
+fn show(args :: jv.Json) -> [net, io, proc] Result[jv.Json, e.Errors] {
+  match util.field_str(args, "issue_id") {
+    None => Err(e.single("issue_id", "missing", "issue_id is required")),
+    Some(id) => match proc.run("lex", util.json_cmd(["issue", "show", id])) {
+      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) => match jv.parse(str.trim(body)) {
+          Err(_) => Ok(JStr(body)),
+          Ok(issue) => Ok(JStr(ic.contract_prompt(issue))),
+        },
+      },
+    },
+  }
+}
+
+fn verify(args :: jv.Json) -> [net, io, proc] Result[jv.Json, e.Errors] {
+  match util.field_str(args, "issue_id") {
+    None => Err(e.single("issue_id", "missing", "issue_id is required")),
+    Some(id) => match proc.run("lex", util.json_cmd(["issue", "verify", id])) {
+      Err(msg) => Err(e.single("", "proc_error", msg)),
+      Ok(out) => match ic.verdict_of(out.stdout) {
+        Some(_) => Ok(JStr(str.trim(out.stdout))),
+        None => Err(e.single("", "cli_failed", util.combined(out))),
+      },
+    },
+  }
+}
+
+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)
+}
+
+fn verify_tool() -> t.Tool {
+  t.define("issue_verify", "Evaluate a typed issue's acceptance at the store head (lex issue verify) and record an IssueVerified attestation. Verdict: verified | failed (with detail naming the wrong signature or example) | inconclusive (shape not machine-evaluable). Call it to prove an issue done; iterate until verified.", id_params("IssueVerifyArgs", "Verify a typed issue at head."), verify)
+}
+