Make ATLAS verify-gate + best-of-k usable on a live local model

ober

be992ce40d5f9ecad08cd852a6a4624bfd50820b

diff --git a/build-binary.ss b/build-binary.ss
index 42aa7cc..c9fc60a 100644
--- a/build-binary.ss
+++ b/build-binary.ss
@@ -151,6 +151,7 @@
     "lib/jcode/proxy/handler"
     "lib/jcode/core/slot-worker"
     "lib/jcode/proxy/server"
+    "lib/jcode/core/verified-run"
     "lib/jcode/eval/scenario"
     "lib/jcode/eval/ablation"
     "lib/jcode/eval/runner"
diff --git a/src/jcode/core/agent.ss b/src/jcode/core/agent.ss
index 6467ac4..aee9497 100644
--- a/src/jcode/core/agent.ss
+++ b/src/jcode/core/agent.ss
@@ -10,6 +10,7 @@
         current-model-override
         get-current-provider
         forge-respond-enforced?
+        forge-max-repeated-calls
         try-parse-text-tool-calls
         try-parse-xml-tool-calls)
 
@@ -48,6 +49,35 @@
 ;; turn on for small local models that can't be trusted to pick tool-vs-text.
 (def forge-respond-enforced? (make-parameter #f))
 
+;; No-progress loop breaker (ATLAS) for the chat loop. When the model emits the
+;; same tool-call batch this many times in a row — a degenerate loop the
+;; retry/error budgets miss, since the calls neither error nor finish — the turn
+;; is stopped instead of silently burning rounds. #f disables. Per-turn state
+;; lives in forge-breaker-state, reset by agent-run at the start of each turn.
+(def forge-max-repeated-calls (make-parameter 3))
+(def forge-breaker-state (make-parameter #f))
+
+(def (chat-calls-signature calls)
+  (string-join
+    (map (lambda (tc)
+           (let ((a (tool-call-arguments tc)))
+             (string-append (tool-call-name tc) "|"
+                            (if (string? a) a (format "~a" a)))))
+         calls)
+    ";"))
+
+;; Update the per-turn breaker state with CALLS; report whether executing them
+;; now is the Nth identical repeat in a row (>= the configured limit).
+(def (forge-no-progress? calls)
+  (let ((limit (forge-max-repeated-calls))
+        (st    (forge-breaker-state)))
+    (and limit st (pair? calls)
+         (let ((sig (chat-calls-signature calls)))
+           (if (equal? sig (vector-ref st 0))
+             (vector-set! st 1 (+ (vector-ref st 1) 1))
+             (begin (vector-set! st 0 sig) (vector-set! st 1 1)))
+           (>= (vector-ref st 1) limit)))))
+
 (def (system-prompt)
   (format "You are an expert AI coding assistant. You help users with software development tasks.
 Working directory: ~a
@@ -1082,9 +1112,10 @@ Be concise. Prefer edit over write for modifying existing files.
   ;; One guardrails instance per user turn — its retry/error budget persists
   ;; across the tool-call rounds of this turn, then resets for the next.
   (let ((gr (make-guardrails (list-tools))))
-    (if (current-stream-cb)
-      (agent-loop-stream session-id (session-get-messages session-id) 0 gr)
-      (agent-loop        session-id (session-get-messages session-id) 0 gr))))
+    (parameterize ((forge-breaker-state (vector #f 0)))
+      (if (current-stream-cb)
+        (agent-loop-stream session-id (session-get-messages session-id) 0 gr)
+        (agent-loop        session-id (session-get-messages session-id) 0 gr)))))
 
 (def (agent-loop session-id messages round gr)
   (let* ((provider (get-current-provider))
@@ -1176,6 +1207,13 @@ Be concise. Prefer edit over write for modifying existing files.
             (let ((final (make-assistant-message (respond-call->text rc) #f)))
               (session-add-message session-id final)
               final))
+           ;; No-progress breaker: same tool batch repeated — stop the turn.
+           ((forge-no-progress? calls)
+            (log-warn logger "no-progress-break" `((round . ,round)))
+            (let ((final (make-assistant-message
+                           "[stopped: repeated the same tool call(s) with no progress]" #f)))
+              (session-add-message session-id final)
+              final))
            (else
             ;; If calls were rescued from bare text, effective is only the
             ;; text — rebuild it carrying the tool_calls so results stay paired.
@@ -1290,6 +1328,14 @@ Be concise. Prefer edit over write for modifying existing files.
               (let ((final (make-assistant-message msg #f)))
                 (session-add-message session-id final)
                 final)))
+           ;; No-progress breaker: same tool batch repeated — stop the turn.
+           ((forge-no-progress? calls)
+            (log-warn logger "no-progress-break" `((round . ,round)))
+            (let ((msg "[stopped: repeated the same tool call(s) with no progress]"))
+              (when raw-cb (raw-cb msg))
+              (let ((final (make-assistant-message msg #f)))
+                (session-add-message session-id final)
+                final)))
            (else
             (let ((asst (if (null? tcs) (make-assistant-message #f calls) response)))
               (session-add-message session-id asst)
diff --git a/src/jcode/core/verified-run.ss b/src/jcode/core/verified-run.ss
new file mode 100644
index 0000000..5672c91
--- /dev/null
+++ b/src/jcode/core/verified-run.ss
@@ -0,0 +1,158 @@
+;;; jcode verified-run — ATLAS verify-gate + best-of-k against a LIVE model
+;;;
+;;; Makes the forge workflow engine usable from jcode chat on a real provider.
+;;; Three pieces the engine needs that free-form chat lacks, supplied here:
+;;;   * a provider-backed responder — bridges the live jcode provider into the
+;;;     runner's (messages tool-specs step) seam, reusing proxy's
+;;;     make-provider-backend (tool-spec->schema, provider-chat, args->assoc).
+;;;   * a coding workflow — read / edit / verify / done tool-defs, with
+;;;     required-steps (edit verify) gating the terminal (done).
+;;;   * a verify oracle — a callable that shells out to a build/test command and
+;;;     RAISES on failure (verified.ss make-verify-callable), so the runner never
+;;;     records verify as complete until the build passes: the gate.
+;;; Driven by run-workflow (no-progress breaker via max-repeated-calls) or, when
+;;; best-of>1, run-best-of-k (diverse resampling with the verify gate as selector).
+
+(export verified-run
+        provider-responder
+        coding-workflow
+        run-verify-command
+        default-verify-command)
+
+(import :std/os/aproc
+        :std/misc/string
+        :std/misc/ports
+        :jcode/core/workflow
+        :jcode/core/verified
+        :jcode/core/best-of-k
+        :jcode/core/workflow-runner
+        :jcode/proxy/server)
+
+(def default-verify-command "make build")
+
+(def (opt-get o key) (let ((p (assoc key o))) (and p (cdr p))))
+
+;; ── provider-backed responder ─────────────────────────────────────────
+;; make-provider-backend gives the (messages tool-specs sampling) seam; the
+;; runner wants (messages tool-specs step-index). Ignore the step index and pass
+;; no request-level sampling — the provider applies its own per-model policy.
+(def (provider-responder provider)
+  (let ((backend (make-provider-backend provider)))
+    (lambda (messages tool-specs _step)
+      (backend messages tool-specs #f))))
+
+;; ── verify oracle ──────────────────────────────────────────────────────
+(def (tail-lines s n)
+  (let* ((lines (string-split s #\newline))
+         (len   (length lines)))
+    (if (<= len n) s
+      (string-join (list-tail lines (- len n)) "\n"))))
+
+;; Run CMD via the shell in CWD; return (pass? . detail). detail is the tail of
+;; combined stdout+stderr so a failing build rides back to the model as the
+;; [ToolError] text it repairs against.
+(def (run-verify-command cmd cwd)
+  (let-values (((stdout stderr exit-code)
+                (aproc-run/status cmd dir: cwd)))
+    (let* ((out (string-append (or stdout "")
+                  (if (and stderr (not (string=? stderr "")))
+                    (string-append "\n" stderr) "")))
+           (detail (string-append "exit " (number->string exit-code) "\n"
+                                   (tail-lines out 40))))
+      (cons (= exit-code 0) detail))))
+
+;; ── coding workflow tools ──────────────────────────────────────────────
+(def (arg-ref args key default)
+  (let ((p (assoc key args))) (if p (cdr p) default)))
+
+(def (abs-path cwd path)
+  (if (and (> (string-length path) 0) (char=? (string-ref path 0) #\/))
+    path
+    (string-append cwd "/" path)))
+
+(def (do-read args cwd)
+  (let ((path (arg-ref args "path" #f)))
+    (if (not path) (error 'read "missing path arg")
+      (let ((p (abs-path cwd path)))
+        (if (file-exists? p) (read-file-string p)
+          (string-append "(file does not exist: " path ")"))))))
+
+(def (do-edit args cwd)
+  (let ((path    (arg-ref args "path" #f))
+        (content (arg-ref args "content" #f)))
+    (cond
+      ((not path)    (error 'edit "missing path arg"))
+      ((not content) (error 'edit "missing content arg"))
+      (else
+       (let ((p (abs-path cwd path)))
+         (write-file-string p content)
+         (string-append "wrote " path " ("
+                        (number->string (string-length content)) " bytes)"))))))
+
+;; Minimal JSON-Schema object; the per-arg contract rides in each tool's
+;; description (nested schema alists don't serialize cleanly, descriptions do).
+(def *obj-schema* '(("type" . "object")))
+
+(def (coding-workflow verify-cmd cwd)
+  (let ((read-def
+          (make-tool-def
+            (make-tool-spec "read"
+              "Read a file's current contents. args: {\"path\": string}."
+              *obj-schema*)
+            (lambda (args) (do-read args cwd)) '()))
+        (edit-def
+          (make-tool-def
+            (make-tool-spec "edit"
+              "Write the FULL new contents of a file (overwrites). args: {\"path\": string, \"content\": string}."
+              *obj-schema*)
+            (lambda (args) (do-edit args cwd)) '()))
+        (verify-def
+          (make-tool-def
+            (make-tool-spec "verify"
+              (string-append "Run the build/tests (" verify-cmd "). No args. On failure it "
+                             "raises with the error output — read it, fix the code with edit, "
+                             "then call verify again.")
+              *obj-schema*)
+            (make-verify-callable (lambda (args) (run-verify-command verify-cmd cwd)))
+            '()))
+        (done-def
+          (make-tool-def
+            (make-tool-spec "done"
+              "Finish the task. Only call AFTER verify has passed. args: {\"summary\": string}."
+              *obj-schema*)
+            (lambda (args) (arg-ref args "summary" "done"))
+            '())))
+    (make-workflow
+      "verified-coding"
+      "Edit code, verify it builds, repair on failure, then finish."
+      (list read-def edit-def verify-def done-def)
+      (list "edit" "verify")          ; required steps gate the terminal
+      "done"                          ; terminal tool
+      (string-append
+        "You are a coding agent working in " cwd ".\n"
+        "Tools: read(path), edit(path,content=FULL new file), verify(), done(summary).\n"
+        "Workflow:\n"
+        "1. read any files you need to understand first.\n"
+        "2. edit to write or change code (always send the COMPLETE file content).\n"
+        "3. verify to run the build/tests.\n"
+        "4. If verify fails, read the error, fix with edit, verify again.\n"
+        "5. Only call done AFTER verify has passed. You cannot finish on unverified code."))))
+
+;; ── entry point ─────────────────────────────────────────────────────────
+;; Run TASK against PROVIDER through the verified-coding workflow. OPT assoc:
+;;   verify-command (default "make build")  cwd (default ".")
+;;   best-of (1)  max-iterations (24)  max-repeated-calls (3)  on-message (#f)
+;; Returns the done tool's summary string, or raises the runner's condition
+;; (MaxIterations / StepEnforcement / ToolExecution / NoProgress) on failure.
+(def (verified-run provider task . opt)
+  (let* ((o    (if (pair? opt) (car opt) '()))
+         (vcmd (or (opt-get o 'verify-command) default-verify-command))
+         (cwd  (or (opt-get o 'cwd) "."))
+         (k    (or (opt-get o 'best-of) 1))
+         (wf   (coding-workflow vcmd cwd))
+         (ropt (list (cons 'max-iterations     (or (opt-get o 'max-iterations) 24))
+                     (cons 'max-repeated-calls (or (opt-get o 'max-repeated-calls) 3))
+                     (cons 'on-message         (opt-get o 'on-message)))))
+    (if (> k 1)
+      (run-best-of-k wf task (lambda () (provider-responder provider)) k ropt)
+      (run-workflow  wf task (provider-responder provider) ropt))))
diff --git a/src/jcode/ui/cli.ss b/src/jcode/ui/cli.ss
index 8e990a5..36816fe 100644
--- a/src/jcode/ui/cli.ss
+++ b/src/jcode/ui/cli.ss
@@ -32,6 +32,7 @@
         :jcode/core/workflow-runner
         :jcode/core/verified
         :jcode/core/best-of-k
+        :jcode/core/verified-run
         :jcode/core/slot-worker
         :jcode/proxy/server
         :jcode/eval/scenario
@@ -105,6 +106,7 @@
         ((equal? (car rest) "keys")     (keys-command (cdr rest)))
         ((equal? (car rest) "serve")    (serve-main (cdr rest)))
         ((equal? (car rest) "proxy")    (proxy-main (cdr rest)))
+        ((equal? (car rest) "verified") (verified-main (cdr rest)))
         ((equal? (car rest) "relay")    (relay-main (cdr rest)))
         ((equal? (car rest) "connect")  (connect-main (cdr rest)))
         (else (one-shot-mode (string-join rest " ") opts)))
@@ -218,6 +220,12 @@ COMMANDS:
     connect HOST:PORT --host NAME
                      Controller mode: dial relay, attach to host NAME,
                      proxy stdin/stdout (speaks the serve protocol).
+    verified TASK    Verify-gated coding on your live model: the agent must
+                     edit -> verify (build/tests) -> repair until it passes,
+                     then finish. Cannot ship unverified code.
+                     [--bestof K] resample K trajectories, verify selects.
+                     [--verify CMD] build/test cmd (default: make build).
+                     [--cwd DIR] working directory (default: .).
 
 EXAMPLES:
     jcode                           Start interactive session
@@ -228,6 +236,8 @@ EXAMPLES:
     jcode relay --port 9001          Run relay on VPS
     jcode serve --connect vps:9001 --register laptop    Mac dials in
     jcode connect vps:9001 --host laptop          Phone/CLI talks to laptop
+    jcode verified \"add a --version flag\" --verify \"make test\"   Verify-gated edit
+    jcode verified \"fix the parser bug\" --bestof 3              Best-of-3, verify picks
 "))
 
 (def (interactive-mode opts)
@@ -639,11 +649,80 @@ EXAMPLES:
        (fprintf (current-error-port) "[ERROR] unknown proxy option: ~a~n" (car args))
        (exit 1)))))
 
+;; ── verified-run UI (ATLAS verify-gate + best-of-k on the live model) ──
+(def (vr-truncate s n)
+  (if (> (string-length s) n) (string-append (substring s 0 n) "…") s))
+
+(def (vr-first-line s)
+  (let ((i (string-index s #\newline)))
+    (if i (substring s 0 i) s)))
+
+(def (vr-args->display a)
+  (cond
+    ((string? a) a)
+    ((null? a) "")
+    ((and (pair? a) (pair? (car a)))
+     (string-join
+       (map (lambda (kv)
+              (let ((v (cdr kv)))
+                (string-append (car kv) "="
+                  (vr-truncate (if (string? v) v (format "~a" v)) 60))))
+            a)
+       " "))
+    (else (format "~a" a))))
+
+;; on-message hook: render the workflow trajectory compactly as it runs.
+(def (vr-print-message msg)
+  (let ((role (message-role msg))
+        (content (message-content msg))
+        (tcs (message-tool-calls msg)))
+    (cond
+      ((and tcs (pair? tcs))
+       (for-each
+         (lambda (tc)
+           (printf "  [~a] ~a~n" (tool-call-name tc)
+                   (vr-truncate (vr-args->display (tool-call-arguments tc)) 90)))
+         tcs))
+      ((equal? role "tool")
+       (printf "    -> ~a~n" (vr-truncate (vr-first-line (or content "")) 110)))
+      (else (void)))))
+
+(def (run-verified-task provider task bestof vcmd cwd)
+  (printf "Verified run (best-of-~a, verify=~a)~n  task: ~a~n"
+          bestof (or vcmd default-verify-command) task)
+  (let ((opt (list (cons 'best-of bestof)
+                   (cons 'on-message vr-print-message)
+                   (cons 'verify-command (or vcmd default-verify-command))
+                   (cons 'cwd (or cwd ".")))))
+    (guard (e [#t (printf "~n✗ verified-run stopped: ~a~n" (err->string e))])
+      (let ((summary (verified-run provider task opt)))
+        (printf "~n✓ done: ~a~n" summary)))))
+
+;; `jcode verified <task> [--bestof K] [--verify CMD] [--cwd DIR]`
+(def (verified-main args)
+  (let loop ((args args) (words '()) (bestof 1) (vcmd #f) (cwd #f))
+    (cond
+      ((null? args)
+       (let ((task (string-join (reverse words) " ")))
+         (if (string=? task "")
+           (begin
+             (fprintf (current-error-port)
+               "[ERROR] usage: jcode verified <task> [--bestof K] [--verify CMD] [--cwd DIR]~n")
+             (exit 1))
+           (run-verified-task (get-current-provider) task bestof vcmd cwd))))
+      ((and (equal? (car args) "--bestof") (pair? (cdr args)))
+       (loop (cddr args) words (or (string->number (cadr args)) 1) vcmd cwd))
+      ((and (equal? (car args) "--verify") (pair? (cdr args)))
+       (loop (cddr args) words bestof (cadr args) cwd))
+      ((and (equal? (car args) "--cwd") (pair? (cdr args)))
+       (loop (cddr args) words bestof vcmd (cadr args)))
+      (else (loop (cdr args) (cons (car args) words) bestof vcmd cwd)))))
+
 (def (handle-command input session-id)
   (let ((cmd (string-trim (substring input 1 (string-length input)))))
     (cond
       ((equal? cmd "help")
-       (display "\nCommands:\n  /help              Show this help\n  /model [name]      Show or set model\n  /provider [name]   Show or set provider\n  /plan              Switch to PLAN mode (read-only)\n  /build             Switch to BUILD mode (read+write)\n  /mode              Show current mode\n  /mcp               Toggle MCP tools on/off\n  /tools             List available tools\n  /clear             Start a new session\n  /sessions          List saved sessions\n  /compact           Show message count\n  /undo [N]          Revert last N checkpoint(s) (default 1)\n  /checkpoints       List recent shadow-git checkpoints\n  /forge [on|off]    Show or toggle forge guardrails\n  /forge sampling <off|on|strict>  Per-model sampling policy\n  /forge workflow    Describe + self-test the workflow engine\n  /forge proxy       Describe + self-test the OpenAI-compatible proxy\n  /forge ablation    Describe + self-test the eval/ablation harness\n  /forge verify      Describe + self-test the verify-gate (ATLAS verify+repair)\n  /forge bestofk     Describe + self-test best-of-k diverse-gen (ATLAS Phase-1)\n  /forge breaker     Describe + self-test the no-progress loop breaker\n  /quit              Exit\n\nMulti-line: end a line with \\ to continue on the next line.\n\n"))
+       (display "\nCommands:\n  /help              Show this help\n  /model [name]      Show or set model\n  /provider [name]   Show or set provider\n  /plan              Switch to PLAN mode (read-only)\n  /build             Switch to BUILD mode (read+write)\n  /mode              Show current mode\n  /mcp               Toggle MCP tools on/off\n  /tools             List available tools\n  /clear             Start a new session\n  /sessions          List saved sessions\n  /compact           Show message count\n  /undo [N]          Revert last N checkpoint(s) (default 1)\n  /checkpoints       List recent shadow-git checkpoints\n  /forge [on|off]    Show or toggle forge guardrails\n  /forge sampling <off|on|strict>  Per-model sampling policy\n  /forge workflow    Describe + self-test the workflow engine\n  /forge proxy       Describe + self-test the OpenAI-compatible proxy\n  /forge ablation    Describe + self-test the eval/ablation harness\n  /forge verify      Describe + self-test the verify-gate (ATLAS verify+repair)\n  /forge bestofk     Describe + self-test best-of-k diverse-gen (ATLAS Phase-1)\n  /forge breaker     Describe + self-test the no-progress loop breaker\n  /forge run <task>  Verify-gated coding on your live model (edit→verify→done)\n  /quit              Exit\n\nMulti-line: end a line with \\ to continue on the next line.\n\n"))
       ((equal? cmd "model")
        (printf "Provider: ~a~n" (or (current-provider-override) (config-provider)))
        (printf "Model:    ~a~n" (or (current-model-override) (config-model)))
@@ -742,6 +821,14 @@ EXAMPLES:
        (forge-print-bestofk))
       ((or (equal? cmd "forge breaker") (equal? cmd "forge no-progress"))
        (forge-print-breaker))
+      ((string-prefix? "forge run " cmd)
+       (let ((task (string-trim (substring cmd (string-length "forge run ")
+                                           (string-length cmd)))))
+         (if (string=? task "")
+           (printf "Usage: /forge run <task>   (verify-gated coding on your live model)~n")
+           (run-verified-task (get-current-provider) task 1 #f #f))))
+      ((equal? cmd "forge run")
+       (printf "Usage: /forge run <task>   (verify-gated coding on your live model)~n"))
       ((or (equal? cmd "forge on") (equal? cmd "forge enforce")
            (equal? cmd "forge enforce on"))
        (forge-respond-enforced? #t)
diff --git a/test/run.ss b/test/run.ss
index 28ff4a8..daecbe8 100644
--- a/test/run.ss
+++ b/test/run.ss
@@ -25,6 +25,7 @@
         (jcode core workflow-runner)
         (jcode core verified)
         (jcode core best-of-k)
+        (jcode core verified-run)
         (jcode proxy convert)
         (jcode proxy handler)
         (jcode core slot-worker)
@@ -1485,6 +1486,40 @@
                                                (cons 'max-repeated-calls 2)))])
   (check! "breaker leaves real edit/verify repair alone" result "SHIPPED"))
 
+(section "=== verified-run: coding workflow on a REAL file + REAL shell verify ===")
+;; The verify-gate/best-of-k tests above use mock callables. This one drives the
+;; live-model bridge's genuinely new code — do-edit (real write-file-string),
+;; run-verify-command (real /bin/sh shell-out → exit-code → pass?), and
+;; coding-workflow's gate wiring — with a scripted responder standing in for the
+;; model. verify is `grep -q correct <file>`: it FAILS on "buggy" (exit 1) and
+;; PASSES on "correct" (exit 0). The script edits buggy, verifies (fails), then
+;; tries to done — that premature done must be GATED because the failed verify
+;; RAISED (make-verify-callable) and was never recorded. Only after a repair edit
+;; and a passing verify does done go through. result == "verified-and-done"
+;; (never "shipped-buggy") proves the real shell verify actually gates the
+;; terminal; the file ending in "correct" proves do-edit wrote real bytes.
+(let* ([vr-dir  "/tmp"]
+       [vr-name "jcode-verified-run-test.txt"]
+       [vr-path (string-append vr-dir "/" vr-name)]
+       [slurp   (lambda (p) (call-with-input-file p (lambda (i) (get-string-all i))))])
+  (guard (e [#t (void)]) (delete-file vr-path))   ; clean any stale file
+  (let* ([wf   (coding-workflow (string-append "grep -q correct " vr-name) vr-dir)]
+         [resp (scripted-responder
+                 (list
+                   (list (make-wtool-call "edit" (list (cons "path" vr-name) (cons "content" "buggy")) #f))
+                   (list (make-wtool-call "verify" '() #f))
+                   (list (make-wtool-call "done" '(("summary" . "shipped-buggy")) #f))
+                   (list (make-wtool-call "edit" (list (cons "path" vr-name) (cons "content" "correct")) #f))
+                   (list (make-wtool-call "verify" '() #f))
+                   (list (make-wtool-call "done" '(("summary" . "verified-and-done")) #f))))]
+         [result (run-workflow wf "implement the feature" resp
+                               (list (cons 'max-iterations 12)))])
+    (check! "verified-run: gate held — done after passing verify, not the buggy one"
+            result "verified-and-done")
+    (check! "verified-run: do-edit wrote the repaired bytes to the real file"
+            (slurp vr-path) "correct"))
+  (guard (e [#t (void)]) (delete-file vr-path)))
+
 ;; ── Results ───────────────────────────────────────────────────────
 
 (printf "~n~a passed, ~a failed~n" pass-count fail-count)