Land leftover TUI polish (#549) and native Anthropic output_config (#550)

TUI/run.zig

@@ -298,13 +298,7 @@ pub fn run(
             continue;
         }
         esc_stall = 0;
-        if (pending_len == inbuf.len) {
-            // A stuck head has filled the whole buffer: that is a parser
-            // wedge, not a dead tty. Drop it rather than letting the
-            // zero-length read below masquerade as a hangup and kill the
-            // TUI mid-session (#517).
-            pending_len = 0;
-        }
+        pending_len = stall.clearFullWedge(pending_len, inbuf.len);
         var filled = pending_len;
         const got = tty.readStdin(inbuf[filled..]);
         pacing.reads += 1;
@@ -505,9 +499,6 @@ test "run loop enables click+hover tracking and bracketed paste" {
     try std.testing.expect(std.mem.indexOf(u8, src, &kitty_on) != null);
     try std.testing.expect(std.mem.indexOf(u8, src, &wrap_off) != null);
     try std.testing.expect(std.mem.indexOf(u8, src, "a=d,d=A") != null);
-    // #517: a buffer-filling parser wedge must be cleared before the read,
-    // or the zero-length read reads as a hangup and kills the TUI.
-    try std.testing.expect(std.mem.indexOf(u8, src, "pending_len == inbuf.len") != null);
     // The idle paste sweep must DISCARD whatever was stuck mid-sequence before
     // the stall path below can see it. Leaving it there let a lone pending ESC
     // become the Escape KEY the instant `in_paste` cleared, cancelling a live

TUI/run_stall.zig

@@ -86,6 +86,12 @@ pub fn armExpired(now_ms: u64, arm_ms: u64) bool {
     return now_ms -| arm_ms > arm_window_ms;
 }
 
+/// A stuck CSI/OSC head that filled the read buffer is a parser wedge, not a
+/// hangup. Drop it so the next `read` is not a zero-length "TTY gone" (#517).
+pub fn clearFullWedge(pending_len: usize, buf_len: usize) usize {
+    return if (pending_len == buf_len) 0 else pending_len;
+}
+
 /// Is this read nothing but complete SGR mouse reports?
 ///
 /// ?1003h is on by default for image-chip hover, and a pointer merely RESTING
@@ -202,3 +208,10 @@ test "a lone ESC inside a latched paste is the escape hatch, not a 2s wait" {
     // Outside a paste nothing moved: #94's 2-stall Escape still fires.
     try std.testing.expectEqual(StallVerdict.escape_key, stallVerdict("\x1b", 2, .{}));
 }
+
+test "a buffer-filling parser wedge is dropped, not treated as hangup (#517)" {
+    try std.testing.expectEqual(@as(usize, 0), clearFullWedge(4096, 4096));
+    try std.testing.expectEqual(@as(usize, 12), clearFullWedge(12, 4096));
+    try std.testing.expectEqual(@as(usize, 0), clearFullWedge(0, 4096));
+    try std.testing.expectEqual(@as(usize, 1), clearFullWedge(1, 2));
+}

TUI/tty.zig

@@ -46,6 +46,16 @@ pub const RawState = if (is_windows) struct {
     input_cp: u32 = 0,
 } else std.posix.termios;
 
+/// Clear the line-discipline bits that steal keys the TUI owns (#523).
+/// Extracted so tests can mutate a termios-shaped value without a real tty.
+pub fn surrenderLineDiscipline(raw: anytype) void {
+    raw.lflag.ICANON = false;
+    raw.lflag.ECHO = false;
+    raw.lflag.ISIG = false;
+    raw.lflag.IEXTEN = false; // ^V (0x16) reaches us, not the tty's lnext
+    raw.iflag.IXON = false; // ^S/^Q are keys, not XOFF/XON flow control
+}
+
 pub fn enterRaw() ?RawState {
     if (is_windows) {
         const h = w.GetStdHandle(w.STD_OUTPUT_HANDLE);
@@ -67,11 +77,7 @@ pub fn enterRaw() ?RawState {
     const fd = std.posix.STDIN_FILENO;
     const orig = std.posix.tcgetattr(fd) catch return null;
     var raw = orig;
-    raw.lflag.ICANON = false;
-    raw.lflag.ECHO = false;
-    raw.lflag.ISIG = false;
-    raw.lflag.IEXTEN = false; // ^V (0x16) reaches us, not the tty's lnext (#523)
-    raw.iflag.IXON = false; // ^S/^Q are keys, not XOFF/XON flow control (#523)
+    surrenderLineDiscipline(&raw);
     raw.cc[@intFromEnum(std.posix.V.MIN)] = 0;
     raw.cc[@intFromEnum(std.posix.V.TIME)] = 0;
     std.posix.tcsetattr(fd, .NOW, raw) catch return null;
@@ -100,9 +106,16 @@ pub fn readStdin(buf: []u8) usize {
 }
 
 test "raw mode surrenders ^V and ^S to the app, not the line discipline (#523)" {
-    const src = @embedFile("tty.zig");
-    try std.testing.expect(std.mem.indexOf(u8, src, "IEXTEN = false") != null);
-    try std.testing.expect(std.mem.indexOf(u8, src, "IXON = false") != null);
+    var raw = struct {
+        lflag: struct { ICANON: bool = true, ECHO: bool = true, ISIG: bool = true, IEXTEN: bool = true } = .{},
+        iflag: struct { IXON: bool = true } = .{},
+    }{};
+    surrenderLineDiscipline(&raw);
+    try std.testing.expect(!raw.lflag.IEXTEN);
+    try std.testing.expect(!raw.iflag.IXON);
+    try std.testing.expect(!raw.lflag.ICANON);
+    try std.testing.expect(!raw.lflag.ECHO);
+    try std.testing.expect(!raw.lflag.ISIG);
 }
 
 test "Windows enterRaw switches the console to UTF-8 and restore puts the CPs back (#607)" {

lean-proofs/Graff/StructuredOutput.lean

@@ -1,23 +1,30 @@
 /-
-  Structured-output carrier ladder (#543): which server-visible carrier a
-  set --output-schema rides, per wire format, learned degrade state (sox),
-  and whether real tools occupy the request.
+  Structured-output carrier ladder (#543 / #550): which server-visible
+  carrier a set --output-schema rides, per wire format, learned degrade
+  state (sox), and whether real tools occupy the request.
 
   openai chat: json_schema until the provider rejects it (sox learned via
   the request() quirk ladder); degraded, the tools-off formatting turn
   carries the schema as a structured_output TOOL (dsh's pattern, forced by
   instruction, never tool_choice — thinking modes reject forcing), while a
-  turn with real tools falls back to json_object. anthropic: no
-  response_format exists at all — the tool is the only server carrier and
-  the prompt always embeds the schema. responses: native text.format.
+  turn with real tools falls back to json_object.
 
-  The invariant of record is never_silent: before 9e2da0a the anthropic
-  wire dropped a set schema with no error — the exact bug class this
-  kernel now makes unrepresentable.
+  anthropic: provider id `anthropic` tries native output_config.format
+  json_schema on the tools-off formatting turn (#550, kimi-code prior art).
+  A learned sox flag (output_config rejected) falls back to the
+  structured_output tool. minimax / kimi-anthropic stay on the tool
+  (modelled here as sox). Real tools never carry a grammar (ADR 0001).
+
+  responses: native text.format.
+
+  The invariant of record is never_silent on the formatting turn: before
+  9e2da0a the anthropic wire dropped a set schema with no error. An
+  anthropic tools turn may be silent — the two-phase split holds the
+  schema for the formatting call.
 
   Executable port: spec/ref/structured_output.py. Impl:
   src/agent_request_body.zig + agent_request_body_responses.zig
-  (schemaAwarePrompt / writeStructuredOutputTool / writeAnthropicStructuredTool).
+  (schemaAwarePrompt / writeAnthropicSchema / writeAnthropicOutputConfig).
 -/
 
 namespace Graff.StructuredOutput
@@ -27,53 +34,74 @@ inductive Wire
 deriving DecidableEq, Repr
 
 inductive Carrier
-  | none | jsonSchema | jsonObject | toolOpenai | toolAnthropic | textFormat
+  | none | jsonSchema | jsonObject | toolOpenai | toolAnthropic | textFormat | outputConfig
 deriving DecidableEq, Repr
 
 /-- The server-visible carrier of the schema for one request.
-    Args: wire, schema present, sox (json_schema was rejected), real tools present. -/
+    Args: wire, schema present, sox (native schema was rejected), real tools present. -/
 def carrier : Wire → Bool → Bool → Bool → Carrier
   | _, false, _, _ => .none
   | .responses, true, _, _ => .textFormat
   | .openai, true, false, _ => .jsonSchema
   | .openai, true, true, true => .jsonObject
   | .openai, true, true, false => .toolOpenai
   | .anthropic, true, _, true => .none
-  | .anthropic, true, _, false => .toolAnthropic
+  | .anthropic, true, false, false => .outputConfig
+  | .anthropic, true, true, false => .toolAnthropic
 
-/-- Whether the system prompt embeds the schema text (schemaAwarePrompt's
-    embedded-schema branch). Tools presence never changes the prompt. -/
+/-- Whether the system prompt embeds the schema JSON (schemaAwarePrompt's
+    cannot-enforce / tool-mode branch). Native Anthropic uses the light
+    prompt; sox (fallback) embeds. Tools presence never changes the prompt. -/
 def promptSchema : Wire → Bool → Bool → Bool
   | _, false, _ => false
-  | .anthropic, true, _ => true
+  | .anthropic, true, sox => sox
   | .openai, true, sox => sox
   | .responses, true, _ => false
 
-/-- #543's invariant of record: a set schema is NEVER silent — some
-    server-visible carrier exists, or the prompt itself embeds the schema. -/
+/-- A set schema is never silent on the formatting turn. An anthropic
+    tools turn may be — ADR 0001 forbids a grammar there; the two-phase
+    split holds the schema for the next call. -/
 theorem never_silent (w : Wire) (sox tools : Bool) :
-    carrier w true sox tools ≠ .none ∨ promptSchema w true sox = true := by
+    carrier w true sox tools ≠ .none ∨ promptSchema w true sox = true ∨
+      (w = .anthropic ∧ tools = true) := by
   cases w <;> cases sox <;> cases tools <;> decide
 
-/-- The learned degrade is a chat-wire quirk: sox changes nothing elsewhere. -/
-theorem sox_only_on_chat (w : Wire) (tools : Bool) (h : w ≠ .openai) :
-    carrier w true true tools = carrier w true false tools := by
-  cases w <;> cases tools <;> first | decide | exact absurd rfl h
+/-- The learned degrade does not touch the Responses wire. -/
+theorem sox_leaves_responses_alone (tools : Bool) :
+    carrier .responses true true tools = carrier .responses true false tools := by
+  cases tools <;> decide
 
-/-- Once a provider rejected json_schema, it is never sent again. -/
+/-- #550: native Anthropic formatting uses output_config; sox falls back to the tool. -/
+theorem sox_degrades_anthropic_native :
+    carrier .anthropic true false false = .outputConfig ∧
+      carrier .anthropic true true false = .toolAnthropic := by
+  decide
+
+/-- ADR 0001: no schema grammar on an anthropic tools turn. -/
+theorem no_grammar_on_anthropic_tools (sox : Bool) :
+    carrier .anthropic true sox true = .none := by
+  cases sox <;> decide
+
+/-- Once a provider rejected json_schema / output_config, it is never sent again. -/
 theorem no_json_schema_after_rejection (w : Wire) (tools : Bool) :
-    carrier w true true tools ≠ .jsonSchema := by
+    carrier w true true tools ≠ .jsonSchema ∧
+      carrier w true true tools ≠ .outputConfig := by
   cases w <;> cases tools <;> decide
 
 /-- No schema, no artifacts: the axis is byte-silent when unused. -/
 theorem absent_schema_is_silent (w : Wire) (sox tools : Bool) :
     carrier w false sox tools = .none ∧ promptSchema w false sox = false := by
   cases w <;> cases sox <;> cases tools <;> decide
 
-/-- The anthropic wire embeds the schema in the prompt unconditionally —
-    even when real tools displace the structured_output tool, nothing is lost. -/
-theorem anthropic_always_teaches (sox : Bool) :
-    promptSchema .anthropic true sox = true := by
-  cases sox <;> decide
+/-- Tool-mode fallback still embeds the schema so a rejected output_config
+    cannot go silent. -/
+theorem anthropic_fallback_teaches :
+    promptSchema .anthropic true true = true := by
+  decide
+
+/-- Native Anthropic uses the light prompt (server enforces on the formatting turn). -/
+theorem anthropic_native_prompt_is_light :
+    promptSchema .anthropic true false = false := by
+  decide
 
 end Graff.StructuredOutput

spec/kernels/structured_output.json

@@ -38,16 +38,16 @@
       "schema": true,
       "sox": false,
       "tools": false,
-      "carrier": "toolAnthropic",
-      "prompt_schema": true
+      "carrier": "outputConfig",
+      "prompt_schema": false
     },
     {
       "wire": "anthropic",
       "schema": true,
       "sox": false,
       "tools": true,
       "carrier": "none",
-      "prompt_schema": true
+      "prompt_schema": false
     },
     {
       "wire": "anthropic",

spec/ref/structured_output.py

@@ -1,4 +1,4 @@
-"""Executable port of lean-proofs/Graff/StructuredOutput.lean (#543)."""
+"""Executable port of lean-proofs/Graff/StructuredOutput.lean (#543 / #550)."""
 
 from __future__ import annotations
 
@@ -15,16 +15,18 @@ def carrier(wire: str, schema: bool, sox: bool, tools: bool) -> str:
         if not sox:
             return "jsonSchema"
         return "jsonObject" if tools else "toolOpenai"
-    # anthropic: no response_format exists on this wire at all
-    return "none" if tools else "toolAnthropic"
+    # anthropic: native output_config.format on the formatting turn (#550);
+    # sox (rejected) falls back to the structured_output tool. Tools turns
+    # never carry a grammar (ADR 0001).
+    if tools:
+        return "none"
+    return "toolAnthropic" if sox else "outputConfig"
 
 
 def prompt_schema(wire: str, schema: bool, sox: bool) -> bool:
     if not schema:
         return False
-    if wire == "anthropic":
-        return True
-    if wire == "openai":
+    if wire in ("anthropic", "openai"):
         return sox
     return False
 
@@ -51,18 +53,28 @@ def check_properties() -> int:
     for row in cells():
         n += 1
         w, s, x, t = row["wire"], row["schema"], row["sox"], row["tools"]
-        # never_silent: a set schema always reaches the provider somewhere.
+        # never_silent: a set schema always reaches the provider, except an
+        # anthropic tools turn (ADR 0001; the two-phase split holds it).
         if s and row["carrier"] == "none" and not row["prompt_schema"]:
-            raise ValueError(f"never_silent violated: {row}")
-        # sox_only_on_chat: the learned degrade changes nothing off the chat wire.
-        if w != "openai" and carrier(w, s, True, t) != carrier(w, s, False, t):
-            raise ValueError(f"sox_only_on_chat violated: {row}")
-        # no_json_schema_after_rejection.
-        if x and row["carrier"] == "jsonSchema":
+            if not (w == "anthropic" and t):
+                raise ValueError(f"never_silent violated: {row}")
+        # sox_leaves_responses_alone
+        if w == "responses" and carrier(w, s, True, t) != carrier(w, s, False, t):
+            raise ValueError(f"sox_leaves_responses_alone violated: {row}")
+        # sox_degrades_anthropic_native
+        if w == "anthropic" and s and not t:
+            want = "toolAnthropic" if x else "outputConfig"
+            if row["carrier"] != want:
+                raise ValueError(f"sox_degrades_anthropic_native violated: {row}")
+        # no_json_schema_after_rejection / no leftover output_config
+        if x and row["carrier"] in ("jsonSchema", "outputConfig"):
             raise ValueError(f"no_json_schema_after_rejection violated: {row}")
-        # absent_schema_is_silent.
+        # absent_schema_is_silent
         if not s and (row["carrier"] != "none" or row["prompt_schema"]):
             raise ValueError(f"absent_schema_is_silent violated: {row}")
+        # no_grammar_on_anthropic_tools
+        if w == "anthropic" and s and t and row["carrier"] != "none":
+            raise ValueError(f"no_grammar_on_anthropic_tools violated: {row}")
     return n
 
 

src/agent.zig

@@ -225,7 +225,7 @@ pub const Agent = struct {
     streamed_args: ArgTool = .none, // which meta tool's prose streamed live this request
     streamed_args_len: usize = 0, // raw bytes emitted for it (gates re-print suppression)
     cap_new: bool = false, // provider rejected max_tokens → use max_completion_tokens
-    sox_json_object: bool = false, // #543: provider rejected response_format json_schema → json_object + schema-in-prompt
+    sox_json_object: bool = false, // #543/#550: rejected json_schema / output_config → tool or json_object + schema-in-prompt
     effort_rejected: bool = false, // model rejected reasoning_effort → drop it (e.g. gpt-5.5 on chat/completions wants /v1/responses)
     output_schema: ?[]const u8 = null, // --output-schema: JSON schema the final answer must satisfy (response_format / text.format, #502)
     next_ask_id: u64 = 1,

src/agent_request.zig

@@ -537,7 +537,10 @@ pub fn request(self: *Agent, tools_in: ?[]const u8) !std.json.ObjectMap {
             // "This response_format type is unavailable now") must not lose the
             // --output-schema contract — retry in json_object mode with the
             // schema moved into the prompt, on the same ladder as cap_new.
-            if (self.output_schema != null and !self.sox_json_object and std.mem.indexOf(u8, msg, "response_format") != null) {
+            if (self.output_schema != null and !self.sox_json_object and
+                (std.mem.indexOf(u8, msg, "response_format") != null or
+                    std.mem.indexOf(u8, msg, "output_config") != null))
+            {
                 self.sox_json_object = true;
                 continue;
             }

src/agent_request_body.zig

@@ -96,10 +96,8 @@ pub fn buildBody(self: *Agent, tools: ?[]const u8, force_tool: bool, stream: boo
                     try s.objectField("tool_choice");
                     try s.print("{s}", .{"{\"type\":\"any\"}"});
                 }
-            } else if (self.output_schema != null) {
-                // #543: this wire has no response_format at all — the schema is
-                // ALWAYS delivered as the structured_output tool (dsh pattern).
-                try @import("agent_request_body_responses.zig").writeAnthropicStructuredTool(&s, self.output_schema.?);
+            } else if (self.output_schema) |schema_json| {
+                try @import("agent_request_body_responses.zig").writeAnthropicSchema(&s, self, schema_json);
             }
             try s.objectField("messages");
             // Cache the conversation prefix too (not just system) on the real