Add verify-gate: ATLAS verify+repair on forge primitives
ober
b66ac0436ba89a6537b35a3d019b01718725724a
--- a/build-binary.ss +++ b/build-binary.ss @@ -143,6 +143,7 @@ "lib/jcode/guardrails/guardrails" "lib/jcode/guardrails/step-enforcer" "lib/jcode/core/workflow-runner" + "lib/jcode/core/verified" "lib/jcode/provider/sampling" "lib/jcode/provider/provider" "lib/jcode/proxy/convert" new file mode 100644 --- /dev/null +++ b/src/jcode/core/verified.ss @@ -0,0 +1,68 @@ +;;; jcode verified-coding workflow — ATLAS verify-gate + self-test repair, +;;; expressed entirely on forge primitives. +;;; +;;; ATLAS's V3 ablation (docs/reports/V3_ABLATION_STUDY.md in that repo) showed +;;; the accuracy oracle is *executing* candidates (build/sandbox verify) and +;;; repairing on failure — +7.3pp from self-verified repair on a frozen model, +;;; with no learned scoring (their Geometric Lens scored +0.0pp). This module +;;; reproduces that win using only forge's existing workflow engine: +;;; +;;; * required-steps (edit verify) — the runner's premature-terminal +;;; enforcement (workflow-runner 3b) blocks the terminal tool until every +;;; required step has *succeeded* (the runner records a step only on an `ok` +;;; outcome — workflow-runner.ss:149 — never on a raised error). +;;; * a verify callable that RAISES on failure — so a failing verify is never +;;; recorded as complete, keeping the terminal gated until verification +;;; actually passes. +;;; * the error budget (max-tool-errors) — caps repair attempts; each failed +;;; verify surfaces as a [ToolError] the model reads and repairs against +;;; (the self-test-repair seam: the failure detail rides in the error text). +;;; +;;; No new engine code, no Geometric Lens, no candidate scoring: forge supplies +;;; every moving part except the execution oracle, which is the verify callable. + +(export make-verify-callable + make-verified-workflow + verified-system-prompt) + +(import :jcode/core/workflow) + +;; A verify callable. RUN is applied to the tool args and must return a pair +;; (pass? . detail-string). On pass the detail is returned (and the runner +;; records `verify` as a completed required step). On fail the callable RAISES a +;; tool error carrying the detail — the runner turns that into a [ToolError] the +;; model repairs against, and does NOT record verify, so the terminal stays +;; gated until a later verify passes. +(def (make-verify-callable run) + (lambda (args) + (let ((r (run args))) + (if (and (pair? r) (car r)) + (string-append "VERIFIED: " (cdr r)) + (error 'verify + (string-append + "verification failed — fix the code and call verify again:\n" + (if (pair? r) (cdr r) "no detail"))))))) + +;; Default system prompt: the explicit edit → verify → (repair) → done contract. +(def verified-system-prompt + (string-append + "You are a coding agent. Follow this workflow exactly:\n" + "1. Use the edit tool to write or change the code.\n" + "2. Call the verify tool to run the build/tests.\n" + "3. If verify fails, read the error, fix the code with edit, then verify again.\n" + "4. Only call done AFTER verify has passed. You cannot finish on unverified code.\n")) + +;; Build a verified-coding workflow on forge primitives. EDIT-DEF, VERIFY-DEF and +;; DONE-DEF are tool-defs; VERIFY-DEF's callable should come from +;; make-verify-callable. required-steps = (edit-name verify-name) gates the +;; terminal (DONE-DEF) behind a successful verify. OPT may carry +;; (system-prompt . string) to override the default contract. +(def (make-verified-workflow name description edit-def verify-def done-def . opt) + (let* ((o (if (pair? opt) (car opt) '())) + (p (assoc 'system-prompt o)) + (sys (if p (cdr p) verified-system-prompt))) + (make-workflow name description + (list edit-def verify-def done-def) + (list (tool-def-name edit-def) (tool-def-name verify-def)) + (tool-def-name done-def) + sys))) --- a/src/jcode/ui/cli.ss +++ b/src/jcode/ui/cli.ss @@ -30,6 +30,7 @@ :jcode/core/compaction-strategy :jcode/core/workflow :jcode/core/workflow-runner + :jcode/core/verified :jcode/core/slot-worker :jcode/proxy/server :jcode/eval/scenario @@ -430,6 +431,78 @@ EXAMPLES: (printf "Disabling step enforcement lets the model answer before searching:~n") (printf "it completes but the answer is ungrounded, so accuracy flips to #f.~n")) +;; /forge verify — ATLAS's verify-gate + self-test repair, built purely on forge +;; primitives (required-steps + a verify callable that raises on failure). The +;; scripted model tries to finish on unwritten code; the gate forces it to edit, +;; verify, repair the failing verify, re-verify, then finish. With step +;; enforcement OFF the premature finish ships unwritten code — accuracy flips. +(def (forge-verify-demo-scenario) + (make-eval-scenario + "verify-gate" + "Premature done is forced through verify + repair before finishing." + (lambda () + (let ((code (vector "UNWRITTEN"))) + (cons + (make-verified-workflow + "vcode" "Edit, verify, done." + (make-tool-def + (make-tool-spec "edit" "Write code." '(("type" . "object"))) + (lambda (args) + (vector-set! code 0 (let ((p (assoc "content" args))) (if p (cdr p) ""))) + "edited") + '()) + (make-tool-def + (make-tool-spec "verify" "Run the build/tests." '(("type" . "object"))) + (make-verify-callable + (lambda (args) + (if (equal? (vector-ref code 0) "correct") + (cons #t "all tests passed") + (cons #f "test_basic FAILED: wrong output")))) + '()) + (make-tool-def + (make-tool-spec "done" "Finish." '(("type" . "object"))) + (lambda (args) (let ((p (assoc "summary" args))) (if p (cdr p) "done"))) + '())) + (lambda () (equal? (vector-ref code 0) "correct"))))) + "implement the feature" + (lambda () + (let ((n 0) + (script (list (list (make-wtool-call "done" '(("summary" . "all set")) "finishing")) + (list (make-wtool-call "edit" '(("content" . "buggy")) "first attempt")) + (list (make-wtool-call "verify" '() "checking")) + (list (make-wtool-call "edit" '(("content" . "correct")) "repairing")) + (list (make-wtool-call "verify" '() "re-checking")) + (list (make-wtool-call "done" '(("summary" . "fixed+verified")) "done"))))) + (lambda (messages tool-specs step) + (let ((r (if (< n (length script)) (list-ref script n) + (make-text-response "stuck")))) + (set! n (+ n 1)) r)))) + (lambda (args) (and args #t)) + '((max-iterations . 12)))) + +(def (forge-print-verify) + (printf "Verify-gate: ATLAS verify + self-test repair on forge primitives.~n") + (printf " required-steps (edit verify) + a verify callable that raises on~n") + (printf " failure → the terminal stays gated until verify actually passes.~n") + (let* ((scn (forge-verify-demo-scenario)) + (rows (run-ablation scn (list (ablation-preset-ref "reforged") + (ablation-preset-ref "no_steps")))) + (on (cdr (assoc "reforged" rows))) + (off (cdr (assoc "no_steps" rows)))) + (printf " reforged complete=~a accuracy=~a iters=~a~n" + (run-result-completeness on) (run-result-accuracy on) + (run-result-iterations-used on)) + (printf " no_steps complete=~a accuracy=~a iters=~a~n" + (run-result-completeness off) (run-result-accuracy off) + (run-result-iterations-used off)) + (let ((st (analyze-messages (run-result-messages on)))) + (printf " reforged stats tool-calls=~a step-nudges=~a tool-errors=~a~n" + (history-stats-total-tool-calls st) + (history-stats-step-nudges st) + (history-stats-tool-errors st)))) + (printf "With the gate, the failing verify is repaired and correct code ships;~n") + (printf "without it, the premature done ships unwritten code (accuracy #f).~n")) + ;; `jcode proxy` — serve the configured provider behind the guardrail proxy. (def (proxy-main args) (let loop ((args args) (port 8080) (bind "127.0.0.1")) @@ -458,7 +531,7 @@ EXAMPLES: (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 /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 /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))) @@ -551,6 +624,8 @@ EXAMPLES: (forge-print-proxy)) ((or (equal? cmd "forge eval") (equal? cmd "forge ablation")) (forge-print-ablation)) + ((equal? cmd "forge verify") + (forge-print-verify)) ((or (equal? cmd "forge on") (equal? cmd "forge enforce") (equal? cmd "forge enforce on")) (forge-respond-enforced? #t) --- a/test/run.ss +++ b/test/run.ss @@ -23,6 +23,7 @@ (jcode core steps) (jcode guardrails step-enforcer) (jcode core workflow-runner) + (jcode core verified) (jcode proxy convert) (jcode proxy handler) (jcode core slot-worker) @@ -1321,6 +1322,67 @@ (check! "pass-rate reforged 1/1" (cdr (assoc "reforged" rates)) '(1 . 1)) (check! "pass-rate no_steps 0/1" (cdr (assoc "no_steps" rates)) '(0 . 1))) +(section "=== verify-gate: ATLAS verify+repair on forge primitives ===") +;; A small model that tries to finish on UNWRITTEN code. make-verified-workflow +;; sets required-steps (edit verify) and a verify callable that RAISES on +;; failure, so the terminal stays gated until verify actually passes. The script +;; below tries done first, then writes buggy code, verifies (fails), repairs, +;; verifies (passes), and finishes — shipping correct code. Strip step +;; enforcement (no_steps) and the premature done ships UNWRITTEN code: accuracy +;; flips #t → #f. This is ATLAS's self-verified-repair win on existing machinery. +(define (verify-gate-scenario) + (make-eval-scenario + "verify-gate" "premature done forced through verify+repair" + (lambda () + (let ([code (vector "UNWRITTEN")]) + (cons + (make-verified-workflow "vcode" "edit, verify, done" + (make-tool-def (make-tool-spec "edit" "write code" '(("type" . "object"))) + (lambda (a) + (vector-set! code 0 (let ([p (assoc "content" a)]) (if p (cdr p) ""))) + "edited") + '()) + (make-tool-def (make-tool-spec "verify" "run tests" '(("type" . "object"))) + (make-verify-callable + (lambda (a) + (if (equal? (vector-ref code 0) "correct") + (cons #t "all tests passed") + (cons #f "test_basic FAILED: wrong output")))) + '()) + (make-tool-def (make-tool-spec "done" "finish" '(("type" . "object"))) + (lambda (a) (let ([p (assoc "summary" a)]) (if p (cdr p) "done"))) + '())) + (lambda () (equal? (vector-ref code 0) "correct"))))) + "implement the feature" + (lambda () + (scripted-responder + (list (list (make-wtool-call "done" '(("summary" . "all set")) #f)) + (list (make-wtool-call "edit" '(("content" . "buggy")) #f)) + (list (make-wtool-call "verify" '() #f)) + (list (make-wtool-call "edit" '(("content" . "correct")) #f)) + (list (make-wtool-call "verify" '() #f)) + (list (make-wtool-call "done" '(("summary" . "fixed+verified")) #f))))) + (lambda (args) (and args #t)) + '((max-iterations . 12)))) +(let ([on (run-eval-scenario (verify-gate-scenario))]) + (check! "verify-gate reforged completeness" (run-result-completeness on) #t) + (check! "verify-gate reforged accuracy (correct code shipped)" (run-result-accuracy on) #t) + (check! "verify-gate reforged iters 6" (run-result-iterations-used on) 6) + (let ([st (analyze-messages (run-result-messages on))]) + (check! "verify-gate repair fired (1 tool error)" (history-stats-tool-errors st) 1) + (check! "verify-gate gate fired (1 step nudge)" (history-stats-step-nudges st) 1))) +(let ([off (run-eval-scenario (verify-gate-scenario) + (list (cons 'ablation (ablation-preset-ref "no_steps"))))]) + (check! "verify-gate no_steps completeness" (run-result-completeness off) #t) + (check! "verify-gate no_steps accuracy #f (unwritten shipped)" (run-result-accuracy off) #f) + (check! "verify-gate no_steps iters 1" (run-result-iterations-used off) 1)) +;; the headline: the gate converts a wrong outcome into a right one. +(let* ([rows (run-ablation (verify-gate-scenario) + (list (ablation-preset-ref "reforged") (ablation-preset-ref "no_steps")))] + [rates (ablation-pass-rates rows)]) + (check! "verify-gate flip reforged 1/1" (cdr (assoc "reforged" rates)) '(1 . 1)) + (check! "verify-gate flip no_steps 0/1" (cdr (assoc "no_steps" rates)) '(0 . 1))) + ;; ── Results ─────────────────────────────────────────────────────── (printf "~n~a passed, ~a failed~n" pass-count fail-count)