diff --git a/src/core/agent/runtime/orchestrator.zig b/src/core/agent/runtime/orchestrator.zig index ff6e8cc05..66e2b13cd 100644 --- a/src/core/agent/runtime/orchestrator.zig +++ b/src/core/agent/runtime/orchestrator.zig @@ -6050,6 +6050,50 @@ fn visionToolMode(mode: image_route.VisionMode) runtime_gateway_step.VisionToolM }; } +/// The user images a request carries that the session still keeps, split at +/// the turn's own user message: those before it came from earlier turns, and +/// the rest arrived this turn. `image_attachments.withholdDroppedImages` turns +/// the others into notes. +const RequestUserImages = struct { this_turn: bool, earlier: bool }; + +fn requestUserImages(messages: []const ChatMessage, current_user_message_index: usize) RequestUserImages { + var found: RequestUserImages = .{ .this_turn = false, .earlier = false }; + for (messages, 0..) |message, index| { + for (message.images) |image| { + if (image.droppedFromSession()) continue; + if (index < current_user_message_index) found.earlier = true else found.this_turn = true; + break; + } + } + return found; +} + +test "requestUserImages splits kept images at the turn's own message" { + const kept = [_]types.ImageAttachment{.{ .id = 1, .path = @constCast("inline://1"), .media_type = @constCast("image/png"), .inline_data = @constCast("png") }}; + const dropped = [_]types.ImageAttachment{.{ .id = 2, .path = @constCast("inline://2"), .media_type = @constCast("image/png"), .snapshot_sha256 = @constCast("digest") }}; + const earlier_only = [_]ChatMessage{ + .{ .role = .user, .content = "first", .images = &kept }, + .{ .role = .assistant, .content = "ok" }, + .{ .role = .user, .content = "Testing" }, + }; + try std.testing.expectEqual(RequestUserImages{ .this_turn = false, .earlier = true }, requestUserImages(&earlier_only, 2)); + const now = [_]ChatMessage{ + .{ .role = .user, .content = "first", .images = &dropped }, + .{ .role = .assistant, .content = "ok" }, + .{ .role = .user, .content = "Look", .images = &kept }, + }; + try std.testing.expectEqual(RequestUserImages{ .this_turn = true, .earlier = false }, requestUserImages(&now, 2)); +} + +/// What the user hears, once per turn, when a down catalog withholds images. +fn catalogDownNotice(chosen: image_route.Decision) []const u8 { + const tools = chosen.tool_images == .withheld_unknown; + const earlier = chosen.earlier_images == .withheld_unknown; + if (earlier and tools) return "Earlier images and images from tools aren't reaching the model right now because image support couldn't be confirmed (model catalog unavailable). fx will retry automatically as the catalog recovers."; + if (earlier) return "Earlier images aren't reaching the model right now because image support couldn't be confirmed (model catalog unavailable). fx will retry automatically as the catalog recovers."; + return "Images from tools aren't reaching the model right now because image support couldn't be confirmed (model catalog unavailable). fx will retry automatically as the catalog recovers."; +} + /// Whether a tool image in `messages` still reaches the request: one the /// session keeps, or a handle to materialize. `image_attachments.withholdDroppedImages` /// turns the others into notes. @@ -7181,8 +7225,10 @@ fn processQueuedPromptLoop( // and every route, mode, and tool image choice below follows the // decision it returns (`tests/tla/image_route/spec/ImageRoute.tla` // OneSnapshot). + const user_images = requestUserImages(recovery_source_messages, current_user_message_index); var image_event: image_route.Event = .{ .request_ready = .{ - .user_images = job.authorized_image_catalog.len > 0 or job.images.len > 0, + .user_images = job.images.len > 0 or user_images.this_turn, + .earlier_images = user_images.earlier, .pending_images = pending_image_ids.len > 0, .tool_images = requestHasToolImages(recovery_source_messages), .fallback = config.provider_capabilities.vision_fallback and deps.tool_registry.lookup("vision") != null, @@ -7230,7 +7276,7 @@ fn processQueuedPromptLoop( "agent", "vision_policy", step_ctx, - "model={s} image_support={s} route={s} mode={s} pending_images={d} tool_images={s}", + "model={s} image_support={s} route={s} mode={s} pending_images={d} tool_images={s} earlier_images={s}", .{ gateway_model, @tagName(image_route_state.support), @@ -7238,9 +7284,17 @@ fn processQueuedPromptLoop( @tagName(image_choice.mode), pending_image_ids.len, @tagName(image_choice.tool_images), + @tagName(image_choice.earlier_images), }, ); const projected_request_messages = blk: { + // The core fails a request whose images attached this turn + // have no route, so the user images left on that route came + // from earlier turns. They stay in the history and leave this + // request as notes (ImageRoute.tla NoSilentWithhold). + if (image_choice.route == .unavailable) { + break :blk try image_attachments.withholdEarlierImages(overlay_arena, recovery_source_messages, image_choice.earlier_images); + } if (job.authorized_image_catalog.len == 0 and job.images.len == 0) { break :blk recovery_source_messages; } @@ -7263,7 +7317,7 @@ fn processQueuedPromptLoop( job.authorized_image_catalog, ); }, - // The core fails a request whose user images have no route. + // Handled above. .unavailable => unreachable, }; }; @@ -7327,13 +7381,13 @@ fn processQueuedPromptLoop( if (request_messages.ptr != located_messages.ptr) { debug_trace.eventf("history", "assistant_tail_continued", step_ctx, "messages={d}", .{located_messages.len}); } - // Tool images withheld because the catalog could not confirm image + // Images withheld because the catalog could not confirm image // input are invisible in the transcript otherwise. The core asks // to tell the user once per turn, and only when the catalog itself // is known to be down; a confirmed model without image input // relies on the model-facing notice instead. if (notify_catalog_down) { - try deps.push_text(deps.ctx, .{ .operational = "Images from tools aren't reaching the model right now because image support couldn't be confirmed (model catalog unavailable). fx will retry automatically as the catalog recovers." }); + try deps.push_text(deps.ctx, .{ .operational = catalogDownNotice(image_choice) }); try deps.push_text(deps.ctx, .{ .operational = "\n" }); } last_gateway_message_count = gateway_instructions.items.len + request_messages.len; diff --git a/src/core/agent/runtime/tests/gateway_flow.zig b/src/core/agent/runtime/tests/gateway_flow.zig index b776f5ef2..d0993c7b9 100644 --- a/src/core/agent/runtime/tests/gateway_flow.zig +++ b/src/core/agent/runtime/tests/gateway_flow.zig @@ -1809,6 +1809,52 @@ test "processQueuedPrompt rereads historical authorized image through optional V try std.testing.expectEqualStrings("Final selected-model answer", hooks.finish_assistant_text.?); } +test "processQueuedPrompt sends a text-only turn while a down catalog withholds an earlier image" { + // The reported session: a screenshot from an earlier turn, then a + // text-only turn after a restart, while the model catalog is unreachable. + const alloc = std.testing.allocator; + var tmp = std.testing.tmpDir(.{}); + defer tmp.cleanup(); + const image_path = try writeTestImagePath(alloc, &tmp); + defer alloc.free(image_path); + const history_image = try testCapturedImage(alloc, &tmp, image_path, 1); + defer types.freeImageAttachment(alloc, history_image); + var history_images = [_]types.ImageAttachment{history_image}; + var history = [_]HistoryTurn{.{ .assistant = .{ + .user = .{ + .text = @constCast("Is this redirect right? [Image #1]"), + .images = &history_images, + }, + .assistant = @constCast("It is the local callback."), + } }}; + const completions = [_]FakeCompletion{.{ .content = "Here is the preview." }}; + var gateway = FakeGateway.init(alloc, &completions); + defer gateway.deinit(); + var hooks = FakeAgentRuntimeDeps.init(alloc); + hooks.catalog_unavailable = true; + hooks.default_model_capabilities = .{ .image_input_support = .unknown, .context_window = 1_000_000 }; + hooks.tool_registry = .{ .tools = test_support.vision_agent_test_tools[0..] }; + defer hooks.deinit(); + var fixture = PromptFixture{}; + var job = fixture.job(); + job.prompt = @constCast("Testing"); + job.history = history[0..]; + job.authorized_image_catalog = &history_images; + + try runFakePrompt(&gateway, &hooks, fixture.config(), job); + + try std.testing.expectEqual(@as(usize, 1), gateway.request_bodies.items.len); + try expectBodyNotContains(&gateway, 0, "\"type\":\"file\""); + try expectBodyNotContains(&gateway, 0, "\"name\":\"vision\""); + try expectBodyContains(&gateway, 0, "[Image #1 was not sent with this request: fx could not confirm image input support"); + try std.testing.expectEqualStrings("Here is the preview.", hooks.finish_assistant_text.?); + var notices: usize = 0; + for (hooks.texts.items) |text| { + if (std.mem.find(u8, text, "Earlier images aren't reaching the model right now") != null) notices += 1; + } + try std.testing.expectEqual(@as(usize, 1), notices); +} + test "processQueuedPrompt keeps required Vision gate cancellation neutral" { const alloc = std.testing.allocator; var tmp = std.testing.tmpDir(.{}); diff --git a/src/core/images/image_attachments.zig b/src/core/images/image_attachments.zig index 8fc5e8427..a57ec1da2 100644 --- a/src/core/images/image_attachments.zig +++ b/src/core/images/image_attachments.zig @@ -7,6 +7,7 @@ const display_width = @import("../shared/display_width.zig"); const entity_spans = @import("../shared/entity_spans.zig"); const file_mutation_contract = @import("../tooling/file_mutation_contract.zig"); const image_data = @import("image_data.zig"); +const image_route = @import("image_route.zig"); const io_mod = @import("../shared/io.zig"); const png_downscale = @import("png_downscale.zig"); const types = @import("../shared/types.zig"); @@ -911,6 +912,51 @@ pub fn withholdDroppedImages(arena: std.mem.Allocator, messages: []const types.C return result orelse messages; } +/// Leaves the user images in `messages` out of a request when the image +/// route core withholds earlier images (`held`), each with a note in its +/// place that says why, so the model knows an image exists that it cannot +/// see. The core fails a request whose images attached this turn have no +/// route, so on that route every user image left is an earlier one. Images +/// that go inline or through the vision tool are not withheld here, and +/// images the session dropped stay for `withholdDroppedImages` to note. +/// Returns `messages` itself when nothing is withheld, otherwise a copy +/// allocated in `arena`. History is not modified. +pub fn withholdEarlierImages( + arena: std.mem.Allocator, + messages: []const types.ChatMessage, + held: image_route.ToolImages, +) ![]const types.ChatMessage { + const reason: []const u8 = switch (held) { + .none, .attached, .withheld_fallback => return messages, + .withheld_unknown => "fx could not confirm image input support for this model (the model is not listed in the model catalog, or the catalog is unavailable). It stays in this session and can be sent again once support is confirmed; until then, ask the user to describe it if you need it.", + .withheld_dead_end => "this model does not accept inline images and no vision fallback is available. Ask the user to describe it or switch to a vision-capable model if you need it.", + }; + var result: ?[]types.ChatMessage = null; + for (messages, 0..) |message, index| { + var withheld: usize = 0; + for (message.images) |image| { + if (!image.droppedFromSession()) withheld += 1; + } + if (withheld == 0) continue; + const projected = result orelse try arena.dupe(types.ChatMessage, messages); + result = projected; + const dropped = try arena.alloc(types.ImageAttachment, message.images.len - withheld); + var notice: std.Io.Writer.Allocating = .init(arena); + var next: usize = 0; + for (message.images) |image| { + if (image.droppedFromSession()) { + dropped[next] = image; + next += 1; + continue; + } + notice.writer.print("[Image #{d} was not sent with this request: {s}]\n", .{ image.id, reason }) catch return error.OutOfMemory; + } + projected[index].images = dropped; + projected[index].content = try std.mem.concat(arena, u8, &.{ notice.written(), message.content orelse "" }); + } + return result orelse messages; +} + fn writeWithheldAttachmentNotice( writer: *std.Io.Writer, attachment: types.ImageAttachment, @@ -3235,6 +3281,152 @@ test "requests leave out images the session dropped, each with a note" { try std.testing.expect((try withholdDroppedImages(arena, &kept)).ptr == (&kept).ptr); } +test "requests leave out earlier images the route cannot carry, each with a note" { + var arena_state = std.heap.ArenaAllocator.init(std.testing.allocator); + defer arena_state.deinit(); + const arena = arena_state.allocator(); + const digest = text_utils.repeat("a", 64); + const images = [_]types.ImageAttachment{ + .{ .id = 1, .path = @constCast("inline://image-1"), .media_type = @constCast("image/png"), .snapshot_sha256 = @constCast(digest), .inline_data = @constCast("png") }, + .{ .id = 2, .path = @constCast("inline://image-2"), .media_type = @constCast("image/png"), .snapshot_sha256 = @constCast(digest) }, + }; + const messages = [_]types.ChatMessage{ + .{ .role = .user, .content = "Look at [Image #1] [Image #2]", .images = &images }, + .{ .role = .assistant, .content = "It shows a logo." }, + .{ .role = .user, .content = "Testing" }, + }; + const unknown = try withholdEarlierImages(arena, &messages, .withheld_unknown); + // Image 1 leaves as a note; image 2, which the session dropped, stays for + // withholdDroppedImages. + try std.testing.expectEqual(@as(usize, 1), unknown[0].images.len); + try std.testing.expectEqual(@as(usize, 2), unknown[0].images[0].id); + try std.testing.expect(std.mem.startsWith(u8, unknown[0].content.?, "[Image #1 was not sent with this request: fx could not confirm image input support for this model")); + try std.testing.expect(std.mem.endsWith(u8, unknown[0].content.?, "]\nLook at [Image #1] [Image #2]")); + try std.testing.expect(unknown[2].content.?.ptr == messages[2].content.?.ptr); + try std.testing.expectEqual(@as(usize, 2), messages[0].images.len); + + const dead_end = try withholdEarlierImages(arena, &messages, .withheld_dead_end); + try std.testing.expect(std.mem.find(u8, dead_end[0].content.?, "no vision fallback is available") != null); + + for ([_]image_route.ToolImages{ .none, .attached, .withheld_fallback }) |held| { + try std.testing.expect((try withholdEarlierImages(arena, &messages, held)).ptr == (&messages).ptr); + } +} + +/// Draws for `driveWithholdEarlierImages` from a fuzzer, with one hash per +/// draw site so the fuzzer tells the draws apart. +const EarlierImageFuzzDraws = struct { + smith: *std.testing.Smith, + + fn below(self: EarlierImageFuzzDraws, n: usize, site: u32) usize { + return self.smith.indexWithHash(n, site); + } + + fn flag(self: EarlierImageFuzzDraws, site: u32) bool { + return self.smith.valueWithHash(bool, site); + } +}; + +/// Draws for `driveWithholdEarlierImages` from a seeded generator. +const EarlierImageSeededDraws = struct { + random: std.Random, + + fn below(self: EarlierImageSeededDraws, n: usize, _: u32) usize { + return self.random.uintLessThan(usize, n); + } + + fn flag(self: EarlierImageSeededDraws, _: u32) bool { + return self.random.boolean(); + } +}; + +/// Builds a history that `draws` chooses, with images the session holds and +/// images it dropped, projects it under one held-images value, and checks +/// what every projection must keep. +fn driveWithholdEarlierImages(draws: anytype) !void { + const max_messages = 6; + const max_images = 3; + var arena_state = std.heap.ArenaAllocator.init(std.testing.allocator); + defer arena_state.deinit(); + const arena = arena_state.allocator(); + const digest = text_utils.repeat("a", 64); + const roles = [_]types.ChatRole{ .user, .assistant, .tool }; + var images: [max_messages][max_images]types.ImageAttachment = undefined; + var image_counts: [max_messages]usize = undefined; + var messages: [max_messages]types.ChatMessage = undefined; + const count = draws.below(max_messages + 1, 1); + for (messages[0..count], 0..) |*message, index| { + image_counts[index] = draws.below(max_images + 1, 2); + for (images[index][0..image_counts[index]]) |*image| { + image.* = .{ + .id = 1 + draws.below(9, 3), + .path = @constCast("inline://image"), + .media_type = @constCast("image/png"), + .snapshot_sha256 = @constCast(digest), + // Without bytes and with a digest, the session dropped it. + .inline_data = if (draws.flag(4)) null else @constCast("png"), + }; + } + message.* = .{ + .role = roles[draws.below(roles.len, 5)], + .content = if (draws.flag(6)) null else "text", + .images = images[index][0..image_counts[index]], + }; + } + const kinds = [_]image_route.ToolImages{ .none, .attached, .withheld_fallback, .withheld_dead_end, .withheld_unknown }; + const held = kinds[draws.below(kinds.len, 7)]; + const source = messages[0..count]; + const projected = try withholdEarlierImages(arena, source, held); + + try std.testing.expectEqual(count, projected.len); + const withholds = held == .withheld_unknown or held == .withheld_dead_end; + var withheld_any = false; + for (source, projected, 0..) |before, after, index| { + // History is not modified. + try std.testing.expectEqual(image_counts[index], before.images.len); + var held_here: usize = 0; + for (before.images) |image| { + if (!image.droppedFromSession()) held_here += 1; + } + if (!withholds or held_here == 0) { + try std.testing.expect(after.images.ptr == before.images.ptr and after.images.len == before.images.len); + try std.testing.expectEqual(before.content, after.content); + continue; + } + withheld_any = true; + // No image the session holds reaches the request; dropped ones stay. + try std.testing.expectEqual(before.images.len - held_here, after.images.len); + for (after.images) |image| try std.testing.expect(image.droppedFromSession()); + // One note per withheld image, ahead of the unchanged text. + const content = after.content orelse return error.TestUnexpectedResult; + try std.testing.expect(std.mem.endsWith(u8, content, before.content orelse "")); + try std.testing.expectEqual(held_here, std.mem.count(u8, content, " was not sent with this request: ")); + for (before.images) |image| { + if (image.droppedFromSession()) continue; + var buffer: [64]u8 = undefined; + const note = try std.mem.print(&buffer, "[Image #{d} was not sent with this request: ", .{image.id}); + try std.testing.expect(std.mem.find(u8, content, note) != null); + } + } + if (!withheld_any) try std.testing.expect(projected.ptr == source.ptr); +} + +fn fuzzWithholdEarlierImages(_: void, smith: *std.testing.Smith) !void { + try driveWithholdEarlierImages(EarlierImageFuzzDraws{ .smith = smith }); +} + +test "earlier images withheld from a request always leave a note" { + try std.testing.fuzz({}, fuzzWithholdEarlierImages, .{ + // Empty input draws the smallest values: a request with no messages. + .corpus = &(.{""} ++ @import("fuzz_corpus").earlier_image_notes.*), + }); +} + +test "earlier images withheld from seeded random histories always leave a note" { + var prng: std.Random.DefaultPrng = .init(20261022); + for (0..2000) |_| try driveWithholdEarlierImages(EarlierImageSeededDraws{ .random = prng.random() }); +} + test "requests name the saved file of each attached image, never its source" { const alloc = std.testing.allocator; var arena_state = std.heap.ArenaAllocator.init(alloc); diff --git a/src/core/images/image_route.zig b/src/core/images/image_route.zig index 5e9f56b3c..bd3c814c4 100644 --- a/src/core/images/image_route.zig +++ b/src/core/images/image_route.zig @@ -10,8 +10,8 @@ //! below are the model's properties; `tests/tla/image_route/design/DESIGN.md` //! lists where each one is enforced. //! -//! This file imports only `std`, so the JSON-lines harness in -//! `tests/tla/drivers/image_route/` can build it on its own. +//! Outside its tests, this file imports only `std`, so the JSON-lines +//! harness in `tests/tla/drivers/image_route/` can build it on its own. const std = @import("std"); /// Whether the selected model takes images inline. @@ -68,7 +68,8 @@ pub const VisionMode = enum { required, }; -/// What happens to the tool images in the request's history. +/// What happens to the images already in the request's history: tool +/// images, and user images from earlier turns, which follow the same rule. pub const ToolImages = enum { /// The history has none. none, @@ -83,18 +84,22 @@ pub const ToolImages = enum { }; pub const FailReason = enum { - /// User images, and the catalog could not confirm image input. + /// Images attached this turn, and the catalog could not confirm image input. capability_unknown, - /// User images, a model without vision, and no vision tool. + /// Images attached this turn, a model without vision, and no vision tool. no_native_image, }; /// What the shell knows about the request it is about to send. Only flags: /// image bytes never enter the core. pub const Request = struct { - /// The turn carries user images, attached now or authorized earlier. + /// The user attached images this turn. Only these can fail a request. user_images: bool, - /// Some of those images still wait for the model's first look. + /// The history holds user images from earlier turns that the session + /// still has. They are attached or withheld like tool images, so an old + /// image never blocks a new turn. + earlier_images: bool, + /// Some images attached this turn still wait for the model's first look. pending_images: bool, /// The request history holds tool images the session still has. tool_images: bool, @@ -130,6 +135,7 @@ pub const Decision = struct { route: Route, mode: VisionMode, tool_images: ToolImages, + earlier_images: ToolImages, }; pub const Effect = union(enum) { @@ -171,7 +177,7 @@ fn onRequest(state: State, request: Request) Output { next.pending = request; return .{ .state = next }; } - if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) { + if (state.support == .unknown and !state.resolved and hasImages(request)) { var next = state; next.resolved = true; next.pending = request; @@ -195,7 +201,7 @@ fn decide(state: State, request: Request) Output { const reason: FailReason = if (state.support == .unknown) .capability_unknown else .no_native_image; return withEffects(state, &.{.{ .fail = reason }}); } - if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) { + if (withholdsUnknown(chosen) and request.catalog_down and !state.notified) { var next = state; next.notified = true; return withEffects(next, &.{ .notify_catalog_down, .{ .send = chosen } }); @@ -203,6 +209,14 @@ fn decide(state: State, request: Request) Output { return withEffects(state, &.{.{ .send = chosen }}); } +fn hasImages(request: Request) bool { + return request.user_images or request.earlier_images or request.tool_images; +} + +fn withholdsUnknown(chosen: Decision) bool { + return chosen.tool_images == .withheld_unknown or chosen.earlier_images == .withheld_unknown; +} + /// The image handling `support` implies for `request`. pub fn decision(support: Support, request: Request) Decision { const route: Route = switch (support) { @@ -216,12 +230,24 @@ pub fn decision(support: Support, request: Request) Decision { .required else .optional; - const tool_images: ToolImages = if (!request.tool_images) .none else switch (support) { + return .{ + .route = route, + .mode = mode, + .tool_images = held(request.tool_images, support, route), + .earlier_images = held(request.earlier_images, support, route), + }; +} + +/// How images already in the history travel when `present`: inline only to +/// a model the catalog lists with vision, and otherwise withheld with the +/// reason the model needs to act on. +fn held(present: bool, support: Support, route: Route) ToolImages { + if (!present) return .none; + return switch (support) { .native => .attached, .unknown => .withheld_unknown, .non_native => if (route == .fallback) .withheld_fallback else .withheld_dead_end, }; - return .{ .route = route, .mode = mode, .tool_images = tool_images }; } fn withEffects(state: State, list: []const Effect) Output { @@ -251,13 +277,14 @@ pub fn abstract(state: *const State) Abstract { } fn eachRequest(comptime body: anytype) !void { - for (0..32) |bits| { + for (0..64) |bits| { const request: Request = .{ .user_images = bits & 1 != 0, .pending_images = bits & 2 != 0, .tool_images = bits & 4 != 0, .fallback = bits & 8 != 0, .catalog_down = bits & 16 != 0, + .earlier_images = bits & 32 != 0, }; if (request.pending_images and !request.user_images) continue; try body(request); @@ -283,10 +310,13 @@ test "every decision reads one support value" { try std.testing.expectEqual(chosen.route == .native, support == .native); try std.testing.expectEqual(chosen.route == .fallback, chosen.mode != .unavailable); try std.testing.expectEqual(chosen.tool_images == .none, !request.tool_images); - if (chosen.tool_images == .attached) try std.testing.expectEqual(Support.native, support); - if (chosen.tool_images == .withheld_unknown) try std.testing.expectEqual(Support.unknown, support); - if (chosen.tool_images == .withheld_fallback) try std.testing.expectEqual(Route.fallback, chosen.route); - if (chosen.tool_images == .withheld_dead_end) try std.testing.expect(support == .non_native and chosen.route == .unavailable); + try std.testing.expectEqual(chosen.earlier_images == .none, !request.earlier_images); + for ([_]ToolImages{ chosen.tool_images, chosen.earlier_images }) |images| { + if (images == .attached) try std.testing.expectEqual(Support.native, support); + if (images == .withheld_unknown) try std.testing.expectEqual(Support.unknown, support); + if (images == .withheld_fallback) try std.testing.expectEqual(Route.fallback, chosen.route); + if (images == .withheld_dead_end) try std.testing.expect(support == .non_native and chosen.route == .unavailable); + } if (chosen.route == .fallback) try std.testing.expectEqual(request.pending_images, chosen.mode == .required); } } @@ -298,7 +328,7 @@ test "a turn asks for capabilities at most once and answers the request it held" fn check(request: Request) !void { const started = step(.{}, .{ .turn_started = .unknown }); const first = step(started.state, .{ .request_ready = request }); - if (!request.user_images and !request.tool_images) { + if (!hasImages(request)) { try std.testing.expectEqual(@as(usize, 1), first.len); try std.testing.expect(first.effects()[0] == .send); return; @@ -323,7 +353,7 @@ test "a turn asks for capabilities at most once and answers the request it held" } test "the catalog-down notice reaches the user once per turn" { - const request: Request = .{ .user_images = false, .pending_images = false, .tool_images = true, .fallback = true, .catalog_down = true }; + const request: Request = .{ .user_images = false, .earlier_images = false, .pending_images = false, .tool_images = true, .fallback = true, .catalog_down = true }; var state = step(.{}, .{ .turn_started = .unknown }).state; var notices: usize = 0; for (0..3) |_| { @@ -341,7 +371,7 @@ test "the catalog-down notice reaches the user once per turn" { test "user images without a route fail the request and never send" { for (all_support) |support| { - const request: Request = .{ .user_images = true, .pending_images = true, .tool_images = true, .fallback = false, .catalog_down = false }; + const request: Request = .{ .user_images = true, .earlier_images = true, .pending_images = true, .tool_images = true, .fallback = false, .catalog_down = false }; const out = step(.{ .support = support, .resolved = true }, .{ .request_ready = request }); try std.testing.expectEqual(@as(usize, 1), out.len); switch (support) { @@ -353,7 +383,7 @@ test "user images without a route fail the request and never send" { } test "abstract maps the pending request onto a sequence of at most one" { - const request: Request = .{ .user_images = true, .pending_images = false, .tool_images = false, .fallback = true, .catalog_down = false }; + const request: Request = .{ .user_images = true, .earlier_images = false, .pending_images = false, .tool_images = false, .fallback = true, .catalog_down = false }; const idle: State = .{}; try std.testing.expectEqual(@as(usize, 0), abstract(&idle).pending.len); const waiting: State = .{ .resolved = true, .pending = request }; @@ -367,3 +397,214 @@ test "requests carry flags, not image bytes" { try std.testing.expect(field_type == bool); } } + +test "an earlier image never blocks a turn" { + // The reported session: a screenshot from an earlier turn, then a + // text-only turn after a restart, while the catalog cannot be reached. + for (all_support) |support| { + for ([_]bool{ false, true }) |fallback| { + for ([_]bool{ false, true }) |catalog_down| { + const request: Request = .{ .user_images = false, .earlier_images = true, .pending_images = false, .tool_images = false, .fallback = fallback, .catalog_down = catalog_down }; + const asked = step(step(.{}, .{ .turn_started = .unknown }).state, .{ .request_ready = request }); + try std.testing.expectEqual(Effect.resolve_capabilities, asked.effects()[0]); + const out = step(asked.state, .{ .capabilities_resolved = support }); + const answer = out.effects()[out.len - 1]; + try std.testing.expect(answer == .send); + const expected: ToolImages = switch (support) { + .native => .attached, + .non_native => if (fallback) .withheld_fallback else .withheld_dead_end, + .unknown => ToolImages.withheld_unknown, + }; + try std.testing.expectEqual(expected, answer.send.earlier_images); + // The user hears once that the catalog is down. + try std.testing.expectEqual(support == .unknown and catalog_down, out.len == 2); + } + } + } +} + +/// The request a step decided: the event's own request, or the one a reply +/// answered. +fn decidedRequest(before: State, event: Event) ?Request { + return switch (event) { + .turn_started => null, + .request_ready => |request| if (before.pending == null) request else null, + .capabilities_resolved => before.pending, + }; +} + +/// The laws of `tests/tla/image_route/spec/ImageRoute.tla` that one step +/// shows, checked on what `step` returned for `event` from `before`. The +/// fuzz target and the seeded test run every step through it, so +/// `zig build test` holds the core to the model where TLC does not run. +fn expectLaws(before: State, event: Event, out: Output) !void { + const after = out.state; + const effects = out.effects(); + const decided = decidedRequest(before, event); + // Bounded: at most a notice, then one answer. + try std.testing.expect(effects.len <= max_effects); + if (effects.len == 2) try std.testing.expect(effects[0] == .notify_catalog_down and effects[1] == .send); + for (effects) |effect| switch (effect) { + // ResolveOnlyWhenNeeded, ResolveOncePerTurn, and PendingWaitsForReply. + .resolve_capabilities => { + try std.testing.expect(event == .request_ready and before.pending == null); + try std.testing.expect(before.support == .unknown and !before.resolved and hasImages(event.request_ready)); + try std.testing.expect(after.resolved and after.pending != null); + }, + // NotifyOnlyWhenDown and NotifyOncePerTurn. + .notify_catalog_down => { + const request = decided orelse return error.TestUnexpectedResult; + try std.testing.expect(effects.len == 2 and withholdsUnknown(effects[1].send)); + try std.testing.expect(request.catalog_down and !before.notified and after.notified); + }, + .send => |chosen| { + const request = decided orelse return error.TestUnexpectedResult; + // DecideOnlyWhenReady. + try std.testing.expect(after.pending == null); + // OneSnapshot and NativeExcludesFallback. + try std.testing.expectEqual(after.support == .native, chosen.route == .native); + const kinds = [_]struct { bool, ToolImages }{ + .{ request.tool_images, chosen.tool_images }, + .{ request.earlier_images, chosen.earlier_images }, + }; + for (kinds) |kind| { + const present, const images = kind; + // NoSilentWithhold: attached or withheld with a notice, never neither. + try std.testing.expectEqual(present, images != .none); + // UnknownNeverInline, OneSnapshot, and AskedBeforeUnknown. + switch (images) { + .none => {}, + .attached => try std.testing.expectEqual(Support.native, after.support), + .withheld_unknown => try std.testing.expect(after.support == .unknown and after.resolved), + .withheld_fallback => try std.testing.expect(after.support == .non_native and chosen.route == .fallback), + .withheld_dead_end => try std.testing.expect(after.support == .non_native and chosen.route == .unavailable), + } + } + // RouteModeCoherent and RequiredWhenPending. + try std.testing.expectEqual(chosen.route == .fallback, chosen.mode != .unavailable); + if (chosen.route == .fallback) try std.testing.expectEqual(request.pending_images, chosen.mode == .required); + // FailExactlyWhenUnroutable: images attached this turn always have a route. + if (request.user_images) try std.testing.expect(chosen.route != .unavailable); + }, + .fail => |reason| { + const request = decided orelse return error.TestUnexpectedResult; + try std.testing.expect(after.pending == null); + // FailExactlyWhenUnroutable: only images attached this turn fail + // a request, so an earlier image never blocks one. + try std.testing.expect(request.user_images); + switch (reason) { + // AskedBeforeUnknown. + .capability_unknown => try std.testing.expect(after.support == .unknown and after.resolved), + .no_native_image => try std.testing.expect(after.support == .non_native and !request.fallback), + } + }, + }; + switch (event) { + // TurnResets. + .turn_started => try std.testing.expect(effects.len == 0 and !after.resolved and !after.notified and after.pending == null), + // DuplicateRequestIsQuiet, and every other request is asked about or answered. + .request_ready => try std.testing.expectEqual(before.pending != null, effects.len == 0), + // StaleReplyIsQuiet. + .capabilities_resolved => if (before.pending == null) { + try std.testing.expectEqual(@as(usize, 0), effects.len); + try std.testing.expectEqualDeep(before, after); + }, + } +} + +/// Draws for `driveCore` from a fuzzer. Each draw site passes its own hash, +/// so the fuzzer tells the draws apart. +const FuzzDraws = struct { + smith: *std.testing.Smith, + + fn below(self: FuzzDraws, n: usize, site: u32) usize { + return self.smith.indexWithHash(n, site); + } + + fn flag(self: FuzzDraws, site: u32) bool { + return self.smith.valueWithHash(bool, site); + } +}; + +/// Draws for `driveCore` from a seeded generator. +const SeededDraws = struct { + random: std.Random, + + fn below(self: SeededDraws, n: usize, _: u32) usize { + return self.random.uintLessThan(usize, n); + } + + fn flag(self: SeededDraws, _: u32) bool { + return self.random.boolean(); + } +}; + +/// Drives the core through up to 64 events that `draws` chooses, crashes +/// included, and checks every step against the model's laws. +fn driveCore(draws: anytype) !void { + var state: State = .{}; + const steps = 1 + draws.below(64, 1); + for (0..steps) |_| { + const event: Event = switch (draws.below(4, 2)) { + 0 => .{ .turn_started = all_support[draws.below(all_support.len, 3)] }, + 1 => ready: { + const user_images = draws.flag(4); + const earlier_images = draws.flag(5); + // Pending images are some of the images attached this turn. + const pending_images = user_images and draws.flag(6); + break :ready .{ .request_ready = .{ + .user_images = user_images, + .earlier_images = earlier_images, + .pending_images = pending_images, + .tool_images = draws.flag(7), + .fallback = draws.flag(8), + .catalog_down = draws.flag(9), + } }; + }, + 2 => .{ .capabilities_resolved = all_support[draws.below(all_support.len, 10)] }, + else => { + // A crash: the next process starts from the core's zero state. + state = .{}; + continue; + }, + }; + const out = step(state, event); + try expectLaws(state, event, out); + state = out.state; + } +} + +fn fuzzCore(_: void, smith: *std.testing.Smith) !void { + try driveCore(FuzzDraws{ .smith = smith }); +} + +/// A fuzz corpus entry: the draws `driveCore` reads, one little-endian u64 +/// each, as the fuzzer's input format holds them. +fn corpusOf(comptime values: []const u64) []const u8 { + comptime { + var bytes: [values.len * 8]u8 = undefined; + for (values, 0..) |value, index| std.mem.writeInt(u64, bytes[index * 8 ..][0..8], value, .little); + const final = bytes; + return &final; + } +} + +test "the core keeps the model's laws on arbitrary event sequences" { + try std.testing.fuzz({}, fuzzCore, .{ + .corpus = &(.{ + // The reported session: a turn starts with support unknown, its + // request holds only an earlier image while the catalog is down, and + // the catalog check answers unknown. + comptime corpusOf(&.{ 2, 0, 0, 1, 0, 1, 0, 1, 1, 2, 0 }), + // An image attached now while the catalog is down still fails. + comptime corpusOf(&.{ 2, 0, 0, 1, 1, 1, 1, 0, 1, 1, 2, 0 }), + } ++ @import("fuzz_corpus").image_route.*), + }); +} + +test "the core keeps the model's laws on seeded random event sequences" { + // The fuzz target's driver with a seeded generator in place of a fuzzer, + // so every test run walks thousands of sequences, not only the corpus. + var prng: std.Random.DefaultPrng = .init(20261022); + for (0..4000) |_| try driveCore(SeededDraws{ .random = prng.random() }); +} diff --git a/src/fuzz_targets.zig b/src/fuzz_targets.zig index 08471cd0e..7b2d5ed8b 100644 --- a/src/fuzz_targets.zig +++ b/src/fuzz_targets.zig @@ -8,7 +8,9 @@ test { _ = @import("acp/jsonrpc.zig"); _ = @import("acp/mcp_servers.zig"); _ = @import("core/agent/runtime/vision_contracts.zig"); + _ = @import("core/images/image_attachments.zig"); _ = @import("core/images/image_data.zig"); + _ = @import("core/images/image_route.zig"); _ = @import("core/mcp/elicitation.zig"); _ = @import("core/mcp_host/wire_tests.zig"); _ = @import("core/session/session_codec.zig"); diff --git a/tests/e2e/vision-route-fake-gateway.test.ts b/tests/e2e/vision-route-fake-gateway.test.ts index c356ee488..ebd9831c5 100644 --- a/tests/e2e/vision-route-fake-gateway.test.ts +++ b/tests/e2e/vision-route-fake-gateway.test.ts @@ -1841,6 +1841,52 @@ describe("Vision route fake Gateway", () => { TIMEOUT, ); + test( + "a resumed text-only turn is sent while the catalog is down, with the earlier image withheld", + async () => { + const root = createIsolatedRoot(); + const fixture = createScopedImageFixture(root); + const imageData = readFileSync(fixture.imagePath).toString("base64"); + const up = startImageGateway([sseText("It shows a logo.")]); + const down = startImageGateway( + [sseText("Text turn answered")], + undefined, + new Response("catalog unavailable", { status: 503 }), + ); + try { + const first = await runFx( + ["ask", "--json", "--auto", "--no-color", "--image", fixture.imagePath, "Describe the attached image."], + { cwd: root.workspace, env: fakeGatewayEnv(root, up, KIMI_MODEL), timeoutMs: TIMEOUT }, + ); + const firstJson = parseFxJson(first); + expect(firstJson.exit_code).toBe(0); + expect(up.chatRequests[0]!.body).toContain(imageData); + + // The next turn, in a new process, cannot reach the catalog. + const resumed = await runFx( + ["ask", "--json", "--auto", "--no-color", "--resume-id", firstJson.session_id, "Testing"], + { cwd: root.workspace, env: fakeGatewayEnv(root, down, KIMI_MODEL), timeoutMs: TIMEOUT }, + ); + const resumedJson = parseFxJson(resumed); + expect(resumedJson.exit_code).toBe(0); + expect(resumedJson.output).toContain("Text turn answered"); + expect(down.chatRequests).toHaveLength(1); + const body = down.chatRequests[0]!.body; + expect(filePartCount(body)).toBe(0); + expect(body).not.toContain(imageData); + expect(body).not.toContain('"name":"vision"'); + expect(body).toContain("[Image #1 was not sent with this request: fx could not confirm image input support"); + expect(resumed.stderr.split("Earlier images aren't reaching the model right now")).toHaveLength(2); + expect(resumed.stderr).not.toContain("Unable to verify image support"); + } finally { + up.stop(); + down.stop(); + rmSync(root.root, { recursive: true, force: true }); + } + }, + TIMEOUT, + ); + test( "Vision outage is an ordinary failed tool result with the exact notice", async () => { diff --git a/tests/fuzz/targets.json b/tests/fuzz/targets.json index 389ad11cc..5fd6997f7 100644 --- a/tests/fuzz/targets.json +++ b/tests/fuzz/targets.json @@ -3,6 +3,8 @@ {"name": "acp_mcp_servers", "module": "fx", "test": "ACP MCP parser handles fuzzed request bytes", "iterations": 1500000}, {"name": "vision_json", "module": "fx", "test": "Vision JSON parsers tolerate arbitrary bounded bytes", "iterations": 1200000}, {"name": "image_dimensions", "module": "fx", "test": "image dimension parsing stays bounded on arbitrary bytes", "iterations": 5000000}, + {"name": "image_route", "module": "fx", "test": "the core keeps the model's laws on arbitrary event sequences", "iterations": 5000000}, + {"name": "earlier_image_notes", "module": "fx", "test": "earlier images withheld from a request always leave a note", "iterations": 100000}, {"name": "mcp_elicitation", "module": "fx", "test": "elicitation request and response parsers stay bounded under fuzzed bytes", "iterations": 1500000}, {"name": "session_optional_fields", "module": "fx", "test": "durable session optional fields handle fuzzed ownership paths", "iterations": 3000000}, {"name": "session_work_provenance", "module": "fx", "test": "per-turn work provenance parser handles fuzzed ownership paths", "iterations": 2100000}, diff --git a/tests/tla/README.md b/tests/tla/README.md index a58c8b28c..e26f52506 100644 --- a/tests/tla/README.md +++ b/tests/tla/README.md @@ -7,7 +7,7 @@ TLA+ specifications for fx, checked with TLC, together with the scripts and Bun | `acp/` | The ACP permission modes, which match the CLI's `/permissions`, and the per-session Standard, Fast, and Ultrafast speed (`src/acp/`). | `acp/check.sh`, then the drivers in `drivers/acp/` | | `cli/` | How `fx` and `fx ask` handle `--model`, `--fast`, `--ultrafast`, and `--effort` at launch, for the current design and a proposed one that validates them. | `cli/check.sh`, `bun test drivers/cli/` | | `durable/` | Durable libfx sessions (`sdk/fx-sdk.js`): the journal, tool replay, parallel batches, fencing, the inbox, resumption, and snapshots. | `durable/check.sh`, `durable/mutants.py` | -| `image_route/` | How images reach the model on each request (`src/core/images/image_route.zig`): whether the catalog's `vision` tag makes image input native, the user-image route and vision tool mode, tool images attached or withheld with a notice, one capability request and one catalog-down notice per turn, and crashes, duplicate requests, and lost or stale replies. `design/` holds the goal, vision, context, and design the checks trace to, and `mutations.json` the planted bugs. | `image_route/check.sh`, which runs `bun run verify`: TLC, every graph edge replayed against the real core, code traces checked by TLC, every planted bug, and `design/DESIGN.md` traceability | +| `image_route/` | How images reach the model on each request (`src/core/images/image_route.zig`): whether the catalog's `vision` tag makes image input native, the user-image route and vision tool mode, tool images and images from earlier turns attached or withheld with a notice, only images attached this turn failing a request, one capability request and one catalog-down notice per turn, and crashes, duplicate requests, and lost or stale replies. `design/` holds the goal, vision, context, and design the checks trace to, and `mutations.json` the planted bugs. | `image_route/check.sh`, which runs `bun run verify`: TLC, every graph edge replayed against the real core, code traces checked by TLC, `fx ask` turns of the built `zig-out/bin/fx` checked by TLC (`spec/BinaryImageRoute.tla`), every planted bug, and `design/DESIGN.md` traceability | | `indexer/` | When a scanned root's listing may be reused, merging parallel grep results, the file picker's loading row, and listing snapshots (`src/core/indexer/`). | `indexer/check.sh` | | `mcp/` | The MCP engine (`src/mcp/`): wire format, requests, stdio, version detection, the tool catalog, both HTTP transports, input-required rounds, authorization, subscriptions, elicitation, and the engine. `rules.md` lists the MCP specification rules the models cite by ID. | `mcp/check.sh`, then the drivers in `drivers/mcp/` | | `mcp_host/` | fx's MCP host (`src/core/mcp_host/`): host lifecycle, saved credentials, logins shared between processes, logins beside processes that run an older build (`MixedBuilds.tla`), sign-in, elicitation routing, and calls held for the URLs a server asks the user to open. | `mcp_host/check.sh`, `bun test drivers/mcp_host/` | diff --git a/tests/tla/drivers/image_route/binary-to-spec.ts b/tests/tla/drivers/image_route/binary-to-spec.ts new file mode 100644 index 000000000..89dee8ba2 --- /dev/null +++ b/tests/tla/drivers/image_route/binary-to-spec.ts @@ -0,0 +1,375 @@ +// Binary to spec: drives the built fx binary through `fx ask` turns against a +// fake gateway, records what each turn did, and has TLC check every turn +// against ImageRoute (BinaryImageRoute.tla). +// +// The harness checks src/core/images/image_route.zig alone. This stage +// checks the shell around it through the real binary: the request flags the +// orchestrator computes from the session, the projections that attach or +// withhold images, the vision tool, and the notices. A flag computed from +// the wrong source, such as counting an earlier turn's image as one attached +// now, passes every core check and fails here. +// +// Each session is one saved fx session with its own HOME, and each turn is +// one `fx ask` process that sees one catalog view: listed with vision, +// listed without it, missing the model, or down (its host refuses +// connections, as an unreachable gateway does). The matrix runs every view +// with and without an image attached now, after a turn that left an image +// in the history and after none. The random sessions, seeded so a failure +// replays, mix views and attachments over several turns. +// +// Run alone: bun binary-to-spec.ts [--bin PATH] [--seed N] [--sessions N] +import { copyFileSync, existsSync, mkdirSync, mkdtempSync, readFileSync, writeFileSync } from "node:fs"; +import { createServer } from "node:net"; +import { join } from "node:path"; +import { binary, testEnvironment } from "../lib/context.ts"; +import { REPO_ROOT, outDir } from "../lib/tlc.ts"; +import { checkTlc, seededRandom, specFiles, toTla, type CheckedTlc, type Request as RouteRequest, type View } from "./lib.ts"; + +const MODEL = "moonshotai/kimi-k3"; +// The vision tool's model, listed so the fallback route can finish a turn. +const VISION_MODEL = "google/gemini-2.5-flash"; +const IMAGE = join(REPO_ROOT, "tests", "e2e", "fixtures", "placeholder-logo.png"); + +// What the binary prints, matched by stable prefixes of its own text. +const UNKNOWN_NOTE = "was not sent with this request: fx could not confirm image input support"; +const DEAD_END_NOTE = "was not sent with this request: this model does not accept inline images"; +const CATALOG_DOWN_NOTICE = "aren't reaching the model right now"; + +export type ViewName = "vision" | "no_vision" | "missing" | "down"; +export const VIEW_NAMES: ViewName[] = ["vision", "no_vision", "missing", "down"]; +const VIEWS: Record = { + vision: { kind: "listed", vision: true, file_input: false }, + no_vision: { kind: "listed", vision: false, file_input: false }, + missing: { kind: "missing", vision: false, file_input: false }, + down: { kind: "down", vision: false, file_input: false }, +}; + +export type Turn = { view: ViewName; attach: boolean }; +export type Seen = { + kind: string; + reason: string; + notified: boolean; + inline_now: boolean; + inline_earlier: boolean; + vision_tool: boolean; + vision_required: boolean; + references: boolean; + earlier_note: string; +}; +export type Observation = { session: string; turn: number; view: View; req: RouteRequest; seen: Seen; exit: number; error: string | null }; + +function sseText(text: string) { + return sse([{ type: "text-delta", id: "answer", delta: text }], "stop"); +} + +function sse(parts: object[], finish: string) { + return new Response( + [ + ...parts.map((part) => `data: ${JSON.stringify(part)}\n\n`), + `data: ${JSON.stringify({ type: "finish", finishReason: { unified: finish, raw: finish }, usage: { inputTokens: { total: 1 }, outputTokens: { total: 1 } } })}\n\n`, + "data: [DONE]\n\n", + ].join(""), + { headers: { "content-type": "text/event-stream" } }, + ); +} + +/// One fake gateway per session. The catalog answers with the current +/// turn's view; model requests are recorded per turn and answered so every +/// route can finish: a required vision call is made with the ids the request +/// offers, its evidence request gets evidence for them, and anything else +/// gets plain text. +class FakeGateway { + view: ViewName = "vision"; + requests: string[] = []; + private visionIds: number[] = []; + private server: ReturnType; + + constructor() { + this.server = Bun.serve({ port: 0, fetch: (req) => this.answer(req) }); + } + + get base() { return `http://127.0.0.1:${this.server.port}`; } + get chatUrl() { return `${this.base}/v4/ai/language-model`; } + stop() { this.server.stop(true); } + + private catalog(): Response { + const listed = (id: string, tags: string[]) => ({ id, type: "language", tags }); + const vision = listed(VISION_MODEL, ["vision", "tool-use"]); + switch (this.view) { + case "vision": return Response.json({ data: [listed(MODEL, ["vision", "tool-use"]), vision] }); + case "no_vision": return Response.json({ data: [listed(MODEL, ["tool-use"]), vision] }); + case "missing": return Response.json({ data: [vision] }); + case "down": return new Response("down", { status: 503 }); + } + } + + private async answer(req: Request): Promise { + if (new URL(req.url).pathname.endsWith("/v1/models")) return this.catalog(); + if (req.method !== "POST") return new Response("not found", { status: 404 }); + const body = await req.text(); + if (body.includes("Generate a short title")) return sseText("Image route session"); + if (body.includes("fx_vision_evidence")) { + const images = this.visionIds.map((image_id) => ({ image_id, status: "ok", summary: `image ${image_id}`, visible_text: [], details: [] })); + return sseText(JSON.stringify({ images })); + } + this.requests.push(body); + if (body.includes('"toolChoice":{"type":"required"}') && body.includes('"name":"vision"')) { + const offered = /([\s\S]*?)<\/available_images>/.exec(body)?.[1] ?? ""; + this.visionIds = [...offered.matchAll(/\[Image #(\d+)\]/g)].map((match) => Number(match[1])); + const input = { image_ids: this.visionIds, focus: "describe the image" }; + return sse([{ type: "tool-call", toolCallId: `vision_${this.requests.length}`, toolName: "vision", input }], "tool-calls"); + } + return sseText("OK"); + } +} + +/// An address nothing listens on, so connecting is refused at once. +async function refusedBase(): Promise { + return await new Promise((resolve) => { + const socket = createServer(); + socket.listen(0, "127.0.0.1", () => { + const port = (socket.address() as { port: number }).port; + socket.close(() => resolve(`http://127.0.0.1:${port}`)); + }); + }); +} + +async function runSession(bin: string, dir: string, name: string, turns: Turn[], refused: string): Promise { + const root = mkdtempSync(join(dir, "session-")); + const home = join(root, "home"); + const workspace = join(root, "workspace"); + mkdirSync(join(home, ".fx"), { recursive: true }); + mkdirSync(workspace, { recursive: true }); + writeFileSync(join(home, ".fx", "settings.json"), "{}"); + const gateway = new FakeGateway(); + const observations: Observation[] = []; + let sessionId = ""; + // Images earlier turns left in the session's history, by their base64. + const earlier: string[] = []; + try { + for (const [index, turn] of turns.entries()) { + gateway.view = turn.view; + gateway.requests = []; + let imageData = ""; + const args = ["ask", "--json", "--auto", "--no-color"]; + if (sessionId) args.push("--resume-id", sessionId); + if (turn.attach) { + // A distinct image per turn, so a request body shows which ones it carries. + const path = join(workspace, `turn-${index + 1}.png`); + copyFileSync(IMAGE, path); + writeFileSync(path, Buffer.concat([readFileSync(path), Buffer.from(`${name} turn ${index + 1}`)])); + imageData = readFileSync(path).toString("base64"); + args.push("--image", path); + } + args.push(`Turn ${index + 1}: reply OK.`); + const proc = Bun.spawn([bin, ...args], { + cwd: workspace, + stdout: "pipe", + stderr: "pipe", + env: testEnvironment({ + HOME: home, + TMPDIR: root, + AI_GATEWAY_API_KEY: "fake-image-route-key", + FX_MODEL: MODEL, + FX_GATEWAY_BASE_URL: turn.view === "down" ? refused : gateway.base, + FX_GATEWAY_CHAT_URL: gateway.chatUrl, + }), + }); + const timer = setTimeout(() => proc.kill("SIGKILL"), 30_000); + const [stdout, stderr, exit] = await Promise.all([new Response(proc.stdout).text(), new Response(proc.stderr).text(), proc.exited]); + clearTimeout(timer); + let json: { session_id?: string; error?: string } = {}; + try { json = JSON.parse(stdout.trim().split("\n").at(-1) ?? "{}"); } catch { json = {}; } + + // The flags the spec says the shell computes from this turn. + const req: RouteRequest = { + user_images: turn.attach, + earlier_images: earlier.length > 0, + pending_images: turn.attach, + tool_images: false, + fallback: true, + catalog_down: turn.view === "down", + }; + const body = gateway.requests[0]; + const error = json.error ?? null; + const seen: Seen = { kind: "send", reason: "none", notified: false, inline_now: false, inline_earlier: false, vision_tool: false, vision_required: false, references: false, earlier_note: "none" }; + if (body === undefined) { + seen.kind = exit !== 0 && error ? "fail" : "error"; + seen.reason = error === "ModelImageCapabilityUnavailable" ? "capability_unknown" + : error === "SubscriptionNativeImageUnavailable" ? "no_native_image" + : `exit ${exit}: ${error ?? stderr.trim().slice(0, 200)}`; + } else { + seen.notified = stderr.includes(CATALOG_DOWN_NOTICE); + seen.inline_now = turn.attach && body.includes(imageData); + seen.inline_earlier = earlier.some((data) => body.includes(data)); + seen.vision_tool = body.includes('"name":"vision"'); + seen.vision_required = body.includes('"toolChoice":{"type":"required"}'); + seen.references = body.includes(""); + seen.earlier_note = body.includes(UNKNOWN_NOTE) ? "unknown" : body.includes(DEAD_END_NOTE) ? "dead_end" : "none"; + } + observations.push({ session: name, turn: index + 1, view: VIEWS[turn.view], req, seen, exit, error }); + // A turn that finished is saved, and its image stays in the history. + if (exit === 0) { + sessionId ||= json.session_id ?? ""; + if (turn.attach) earlier.push(imageData); + } + } + } finally { + gateway.stop(); + } + return observations; +} + +export function matrixSessions(): { name: string; turns: Turn[] }[] { + const sessions: { name: string; turns: Turn[] }[] = []; + for (const before of [false, true]) { + for (const view of VIEW_NAMES) { + for (const attach of [false, true]) { + const last: Turn = { view, attach }; + sessions.push({ + name: `${before ? "after an image" : "first turn"}, ${view}, ${attach ? "image now" : "text only"}`, + turns: before ? [{ view: "vision", attach: true }, last] : [last], + }); + } + } + } + return sessions; +} + +export function randomSessions(seed: number, count: number, maxTurns: number): { name: string; turns: Turn[] }[] { + const random = seededRandom(seed); + const sessions: { name: string; turns: Turn[] }[] = []; + for (let i = 0; i < count; i += 1) { + const length = 2 + Math.floor(random() * (maxTurns - 1)); + const turns: Turn[] = []; + for (let t = 0; t < length; t += 1) { + // The down catalog is the reported case, so it comes up often. + const roll = random(); + const view: ViewName = roll < 0.35 ? "down" : VIEW_NAMES[Math.floor(random() * 3)]!; + turns.push({ view, attach: random() < 0.4 }); + } + sessions.push({ name: `random ${i + 1} (seed ${seed})`, turns }); + } + return sessions; +} + +export type Mismatch = { observation: Observation; expected: string }; +export type BinaryToSpecResult = { + /// Every turn conforms. With `-continue`, TLC 2.19 still ends by saying + /// no error was found, so this reads the violations it reported instead. + ok: boolean; + sessions: number; + turns: number; + observationsPath: string; + tlc: CheckedTlc; + /// The turns TLC found violating, the first only unless `all` was set. + mismatches: Mismatch[]; +}; + +/// The turns TLC reports violating BinaryConforms: for each error trace, its +/// last state names the turn (`at`) and what the model expected. +function mismatchesFrom(output: string, observations: Observation[]): Mismatch[] { + const found: Mismatch[] = []; + for (const chunk of output.split("Error: Invariant BinaryConforms is violated.").slice(1)) { + const last = chunk.split(/\nState \d+:/).at(-1) ?? ""; + const at = Number(/\/\\ at = (\d+)/.exec(last)?.[1] ?? NaN); + const expected = /\/\\ expected = (\[[\s\S]*?\])\s*(?:\n\s*\n|\n\/\\|$)/.exec(last)?.[1]?.replace(/\s+/g, " ") ?? "(not in TLC's output)"; + const observation = observations[at - 1]; + if (observation && !found.some((m) => m.observation === observation)) found.push({ observation, expected }); + } + return found; +} + +export async function binaryToSpec(options: { bin: string; dir: string; seed: number; randomSessions: number; maxTurns: number; all?: boolean }): Promise { + if (!existsSync(options.bin)) throw new Error(`no fx binary at ${options.bin}; run zig build, or point FX_BIN at one`); + const sessions = [...matrixSessions(), ...randomSessions(options.seed, options.randomSessions, options.maxTurns)]; + mkdirSync(options.dir, { recursive: true }); + const refused = await refusedBase(); + const observations: Observation[] = []; + for (const session of sessions) observations.push(...await runSession(options.bin, options.dir, session.name, session.turns, refused)); + + const observationsPath = join(options.dir, "observations.json"); + writeFileSync(observationsPath, `${JSON.stringify(observations, null, 1)}\n`); + const checked = await checkObservations(join(options.dir, "tlc"), observations, options.all ?? false); + return { ...checked, sessions: sessions.length, turns: observations.length, observationsPath }; +} + +/// Has TLC check `observations` against the model in `dir`. The binary +/// stage runs it on what the binary did, and its self-check on doctored +/// copies, which it must reject. +export async function checkObservations(dir: string, observations: Observation[], all: boolean): Promise<{ ok: boolean; tlc: CheckedTlc; mismatches: Mismatch[] }> { + const data = [ + "---- MODULE BinaryData ----", + "EXTENDS Sequences", + "Observations == <<", + observations.map((o) => ` \\* ${o.session}, turn ${o.turn}\n ${toTla({ view: o.view, req: o.req, seen: o.seen })}`).join(",\n"), + ">>", + "====", + "", + ].join("\n"); + const files = { + ...specFiles(), + "BinaryImageRoute.tla": readFileSync(join(REPO_ROOT, "tests", "tla", "image_route", "spec", "BinaryImageRoute.tla"), "utf8"), + "BinaryImageRoute.cfg": readFileSync(join(REPO_ROOT, "tests", "tla", "image_route", "spec", "BinaryImageRoute.cfg"), "utf8"), + "BinaryData.tla": data, + }; + const tlc = await checkTlc(dir, "BinaryImageRoute", "BinaryImageRoute.cfg", files, all ? ["-continue"] : []); + const ok = tlc.verdict === "pass" && !tlc.output.includes("Error: Invariant BinaryConforms is violated."); + return { ok, tlc, mismatches: mismatchesFrom(tlc.output, observations) }; +} + +/// Copies of `observations` with one turn misreported, each as a binary +/// with a known bug would show it. The model must reject every one, or the +/// binary stage could pass whatever the binary did. +export function doctoredObservations(observations: Observation[]): { name: string; observations: Observation[] }[] { + const doctor = (name: string, pick: (o: Observation) => boolean, change: (seen: Seen) => Seen) => { + const index = observations.findIndex(pick); + if (index < 0) return null; + const copy = observations.map((o) => ({ ...o, seen: { ...o.seen } })); + copy[index]!.seen = change(copy[index]!.seen); + return { name, observations: copy }; + }; + const none: Seen = { kind: "send", reason: "none", notified: false, inline_now: false, inline_earlier: false, vision_tool: false, vision_required: false, references: false, earlier_note: "none" }; + return [ + doctor("an earlier image fails a text-only turn (the reported bug)", + (o) => o.seen.earlier_note === "unknown", + () => ({ ...none, kind: "fail", reason: "capability_unknown" })), + doctor("an unconfirmed earlier image is sent inline", + (o) => o.seen.earlier_note === "unknown", + (seen) => ({ ...seen, earlier_note: "none", inline_earlier: true })), + doctor("a down catalog withholds an earlier image without telling the user", + (o) => o.seen.earlier_note === "unknown" && o.seen.notified, + (seen) => ({ ...seen, notified: false })), + doctor("an image attached now is sent while support is unknown", + (o) => o.seen.kind === "fail" && o.seen.reason === "capability_unknown", + () => ({ ...none })), + ].filter((entry): entry is { name: string; observations: Observation[] } => entry !== null); +} + +if (import.meta.main) { + const flag = (name: string) => { + const index = process.argv.indexOf(name); + return index >= 0 ? process.argv[index + 1] : undefined; + }; + const started = performance.now(); + const result = await binaryToSpec({ + bin: flag("--bin") ?? binary, + dir: outDir("image-route-binary"), + seed: Number(flag("--seed") ?? process.env.FX_IMAGE_ROUTE_SEED ?? "20261022"), + randomSessions: Number(flag("--sessions") ?? process.env.FX_IMAGE_ROUTE_BINARY_SESSIONS ?? "8"), + maxTurns: 5, + // Standalone runs list every turn that disagrees, not just the first. + all: true, + }); + const { ok } = result; + console.log(`${ok ? "PASS" : "FAIL"} binary to spec: ${result.sessions} sessions, ${result.turns} turns, ${result.mismatches.length} disagree with the model, ${((performance.now() - started) / 1000).toFixed(1)} s; observations ${result.observationsPath}`); + for (const { observation, expected } of result.mismatches) { + const view = observation.view.kind === "listed" ? `listed(vision=${observation.view.vision})` : observation.view.kind; + console.log(` mismatch: ${observation.session}, turn ${observation.turn}, catalog ${view}`); + console.log(` flags: ${toTla(observation.req)}`); + console.log(` expected: ${expected}`); + console.log(` binary: ${toTla(observation.seen)}`); + } + if (!ok && result.mismatches.length === 0) console.log(result.tlc.output.slice(-3000)); + process.exitCode = ok ? 0 : 1; +} diff --git a/tests/tla/drivers/image_route/code-to-spec.ts b/tests/tla/drivers/image_route/code-to-spec.ts index ed009349d..acf42d58b 100644 --- a/tests/tla/drivers/image_route/code-to-spec.ts +++ b/tests/tla/drivers/image_route/code-to-spec.ts @@ -20,17 +20,18 @@ const visionOnly = listed(true, false); const views: View[] = [listed(true, true), visionOnly, listed(false, true), listed(false, false), missing, down]; function req(flags: Partial): Request { - return { user_images: false, pending_images: false, tool_images: false, fallback: false, catalog_down: false, ...flags }; + return { user_images: false, earlier_images: false, pending_images: false, tool_images: false, fallback: false, catalog_down: false, ...flags }; } const requests: Request[] = []; -for (let bits = 0; bits < 32; bits += 1) { +for (let bits = 0; bits < 64; bits += 1) { const r = req({ user_images: (bits & 1) !== 0, pending_images: (bits & 2) !== 0, tool_images: (bits & 4) !== 0, fallback: (bits & 8) !== 0, catalog_down: (bits & 16) !== 0, + earlier_images: (bits & 32) !== 0, }); if (r.pending_images && !r.user_images) continue; requests.push(r); @@ -65,6 +66,20 @@ export const scripted: Record = { "user images with no route": [turn(listed(false, true)), ready({ user_images: true, pending_images: true }), ready({ user_images: true, fallback: true, pending_images: true })], // The catalog recovers within the turn: the one resolve picks it up. "catalog recovers within the turn": [turn(down), ready({ tool_images: true, user_images: true, fallback: true }), reply(listed(true, false)), ready({ tool_images: true })], + // The reported session: an earlier screenshot, then text-only turns after + // a restart with the catalog unreachable. Each is sent, the image + // withheld with a note, and the user hears once per turn. + "earlier image while the catalog is down": [ + turn(down), ready({ earlier_images: true, fallback: true, catalog_down: true }), reply(down), + ready({ earlier_images: true, fallback: true, catalog_down: true }), + turn(down), ready({ earlier_images: true, fallback: true, catalog_down: true }), reply(down), + ], + // An image attached now still fails while support is unknown. + "image attached now while the catalog is down": [turn(down), ready({ user_images: true, pending_images: true, earlier_images: true, catalog_down: true }), reply(down)], + // A model without vision and no vision tool: the earlier image is a dead end, not a failure. + "earlier image with no route": [turn(listed(false, false)), ready({ earlier_images: true })], + // Earlier images go inline again once the catalog lists vision. + "earlier image after the catalog recovers": [turn(missing), ready({ earlier_images: true }), reply(missing), turn(visionOnly), ready({ earlier_images: true })], }; function randomEvents(random: () => number, length: number): Event[] { diff --git a/tests/tla/drivers/image_route/harness.zig b/tests/tla/drivers/image_route/harness.zig index 377362769..02111995e 100644 --- a/tests/tla/drivers/image_route/harness.zig +++ b/tests/tla/drivers/image_route/harness.zig @@ -5,7 +5,7 @@ //! it reads one event per line and prints one line per event: //! //! in: {"event":"turn_started","view":{"kind":"listed","vision":true,"file_input":false}} -//! {"event":"request_ready","req":{"user_images":false,...}} +//! {"event":"request_ready","req":{"user_images":false,"earlier_images":true,...}} //! {"event":"capabilities_resolved","view":{"kind":"down","vision":false,"file_input":false}} //! out: {"state":{"support":"unknown","resolved":false,"notified":false,"pending":[]},"out":[...]} //! @@ -35,6 +35,7 @@ const EffectJson = struct { route: ?image_route.Route = null, mode: ?image_route.VisionMode = null, tool_images: ?image_route.ToolImages = null, + earlier_images: ?image_route.ToolImages = null, reason: ?image_route.FailReason = null, }; @@ -67,7 +68,7 @@ fn effectJson(effect: image_route.Effect) EffectJson { return switch (effect) { .resolve_capabilities => .{ .kind = "resolve" }, .notify_catalog_down => .{ .kind = "notify" }, - .send => |chosen| .{ .kind = "send", .route = chosen.route, .mode = chosen.mode, .tool_images = chosen.tool_images }, + .send => |chosen| .{ .kind = "send", .route = chosen.route, .mode = chosen.mode, .tool_images = chosen.tool_images, .earlier_images = chosen.earlier_images }, .fail => |reason| .{ .kind = "fail", .reason = reason }, }; } diff --git a/tests/tla/drivers/image_route/lib.ts b/tests/tla/drivers/image_route/lib.ts index 0526bad44..2c1aeb62b 100644 --- a/tests/tla/drivers/image_route/lib.ts +++ b/tests/tla/drivers/image_route/lib.ts @@ -18,12 +18,13 @@ export const PINNED_TLC_VERSION = "TLC2 Version 2.19 of 08 August 2024 (rev: 5a4 export type View = { kind: "listed" | "missing" | "down"; vision: boolean; file_input: boolean }; export type Request = { user_images: boolean; + earlier_images: boolean; pending_images: boolean; tool_images: boolean; fallback: boolean; catalog_down: boolean; }; -export type Effect = { kind: string; route?: string; mode?: string; tool_images?: string; reason?: string }; +export type Effect = { kind: string; route?: string; mode?: string; tool_images?: string; earlier_images?: string; reason?: string }; export type CoreState = { support: string; resolved: boolean; notified: boolean; pending: Request[] }; export type Shown = CoreState & { out: Effect[] }; export type Act = diff --git a/tests/tla/drivers/image_route/traceability.ts b/tests/tla/drivers/image_route/traceability.ts index 686cd3566..635f0fa40 100644 --- a/tests/tla/drivers/image_route/traceability.ts +++ b/tests/tla/drivers/image_route/traceability.ts @@ -10,7 +10,7 @@ // mutation:ID a planted bug in mutations.json // zig:path#name a `test "name"` block in that Zig file // e2e:path#name, sdk:path#name a test whose source contains that name -// driver:name a driver stage: spec-to-code or code-to-spec +// driver:name a driver stage: spec-to-code, code-to-spec, or binary-to-spec // review:text how a check that cannot be automated is enforced instead import { existsSync, readFileSync } from "node:fs"; import { join } from "node:path"; @@ -83,7 +83,7 @@ export function checkTraceability(designPath = join(MODEL_DIR, "design", "DESIGN fileTest(); break; case "driver": - if (!["spec-to-code", "code-to-spec"].includes(value)) problems.push(`${owner}: ${token} is not a driver stage`); + if (!["spec-to-code", "code-to-spec", "binary-to-spec"].includes(value)) problems.push(`${owner}: ${token} is not a driver stage`); break; case "review": if (value.length < 20) problems.push(`${owner}: ${token} must say how it is enforced`); diff --git a/tests/tla/drivers/image_route/verify.ts b/tests/tla/drivers/image_route/verify.ts index fbc1082b4..61046a0c7 100644 --- a/tests/tla/drivers/image_route/verify.ts +++ b/tests/tla/drivers/image_route/verify.ts @@ -7,15 +7,23 @@ // 3. the harness, built from the real src/core/images/image_route.zig; // 4. spec to code: every graph edge replayed against the real core; // 5. code to spec: scripted and random traces with faults, checked by TLC; -// 6. every planted bug in the spec caught by its property; -// 7. every planted bug in the code caught in both directions; -// 8. traceability: DESIGN.md accounts for every question, rule, and law. +// 6. binary to spec: `fx ask` turns of the built binary, a matrix and +// random sessions, each checked by TLC against the model, and doctored +// observations the check must reject; +// 7. every planted bug in the spec caught by its property; +// 8. every planted bug in the code caught in both directions; +// 9. traceability: DESIGN.md accounts for every question, rule, and law. // // Settings: FX_IMAGE_ROUTE_SEED (default 20261019), FX_IMAGE_ROUTE_TRACES -// (random traces, default 300), FX_TLA_OUT (where the report goes). +// (random traces, default 300), FX_IMAGE_ROUTE_BINARY_SESSIONS (random +// binary sessions, default 8), FX_BIN (the binary, default zig-out/bin/fx, +// which `zig build` must have built from this checkout), FX_TLA_OUT (where +// the report goes). import { mkdirSync, readFileSync, writeFileSync } from "node:fs"; import { dirname, join } from "node:path"; +import { binary } from "../lib/context.ts"; import { outDir, writeJson } from "../lib/tlc.ts"; +import { binaryToSpec, checkObservations, doctoredObservations } from "./binary-to-spec.ts"; import { codeToSpec } from "./code-to-spec.ts"; import { MODEL_DIR, PINNED_TLC_VERSION, buildHarness, checkTlc, pinnedToolchain, specFiles } from "./lib.ts"; import { codeMutations, specMutations } from "./mutations.ts"; @@ -24,8 +32,9 @@ import { checkTraceability } from "./traceability.ts"; const seed = Number(process.env.FX_IMAGE_ROUTE_SEED ?? "20261019"); const randomTraces = Number(process.env.FX_IMAGE_ROUTE_TRACES ?? "300"); +const binarySessions = Number(process.env.FX_IMAGE_ROUTE_BINARY_SESSIONS ?? "8"); const out = outDir("image-route"); -const report: Record = { started: new Date().toISOString(), seed, randomTraces, out }; +const report: Record = { started: new Date().toISOString(), seed, randomTraces, binarySessions, binary, out }; const failures: string[] = []; const started = performance.now(); const elapsed = (from: number) => `${((performance.now() - from) / 1000).toFixed(1)} s`; @@ -66,6 +75,23 @@ try { stage("code to spec", traces.tlc.verdict === "pass", `${traces.traces} traces, ${traces.steps} steps, TLC ${traces.tlc.verdict}${traces.tlc.property ? ` (${traces.tlc.property})` : ""}, ${traces.tlc.distinctStates} distinct states, ${elapsed(at)}`); + at = performance.now(); + const turns = await binaryToSpec({ bin: binary, dir: join(out, "binary-to-spec"), seed, randomSessions: binarySessions, maxTurns: 5 }); + const doctored = doctoredObservations(JSON.parse(readFileSync(turns.observationsPath, "utf8"))); + const doctoredRejected: string[] = []; + for (const [index, entry] of doctored.entries()) { + if (!(await checkObservations(join(out, "binary-to-spec", `doctored-${index + 1}`), entry.observations, false)).ok) doctoredRejected.push(entry.name); + } + report.binaryToSpec = { ok: turns.ok, sessions: turns.sessions, turns: turns.turns, observationsPath: turns.observationsPath, mismatches: turns.mismatches, doctored: doctored.map((entry) => entry.name), rejected: doctoredRejected }; + const first = turns.mismatches[0]; + // Each doctored copy needs a turn of its kind, so all four must exist. + stage("binary to spec", turns.ok && doctored.length === 4 && doctoredRejected.length === doctored.length, + turns.ok + ? `${turns.turns} turns over ${turns.sessions} sessions of ${binary} as the model decides; rejects ${doctoredRejected.length} of ${doctored.length} doctored observations; ${elapsed(at)}` + : first + ? `${first.observation.session}, turn ${first.observation.turn}: the model expects ${first.expected}, the binary showed ${JSON.stringify(first.observation.seen)}` + : `TLC ${turns.tlc.verdict}${turns.tlc.property ? ` (${turns.tlc.property})` : ""}`); + at = performance.now(); const specBugs = await specMutations(join(out, "spec-mutations")); report.specMutations = specBugs; diff --git a/tests/tla/image_route/design/DESIGN.md b/tests/tla/image_route/design/DESIGN.md index 30dc3c5b3..c210f9676 100644 --- a/tests/tla/image_route/design/DESIGN.md +++ b/tests/tla/image_route/design/DESIGN.md @@ -22,8 +22,8 @@ How fx decides, for each model request, where images go: inline, through the vis - Q14: The catalog fetch keeps the transport's deadline. A timeout leaves the resolver failed and support unknown, so the request goes out without images and with the "could not confirm" notice. The caller assumes nothing about vision. - Q15: A slow, down, rate-limited, or malformed catalog leaves the resolver failed (`gateway.zig:2713-2715` rejects malformed JSON), which the core sees as unknown support. The request still goes out, without images. - Q16: The core's state lives in memory and dies with the process. Tool images stay in the session store, and the next process decides again from its first turn. -- Q18: Unknown support with a down catalog: one notice per turn in the transcript (`orchestrator.zig:7493-7496`, this change), and a model-facing note that it may recover. No vision: the model is told to call the vision tool, or to ask for a vision model. User images with no route: `ModelImageCapabilityUnavailable` or `SubscriptionNativeImageUnavailable`, as before. Each recovers on a later turn once the catalog answers. -- Q19: Nothing. A withheld image stays in the store with a notice (`NoSilentWithhold`), session-dropped images become notes (`image_attachments.zig:883-887`), and the `vision_policy` trace line now records the tool image decision (`orchestrator.zig:7375-7388`, this change). +- Q18: Unknown support with a down catalog: one notice per turn in the transcript (`orchestrator.zig:7493-7496`, this change), and a model-facing note that it may recover. No vision: the model is told to call the vision tool, or to ask for a vision model. Images attached this turn with no route: `ModelImageCapabilityUnavailable` or `SubscriptionNativeImageUnavailable`, and the failed turn is not saved, so its image never enters the history. Images from earlier turns never fail a turn: on a route that cannot carry them they leave the request as one note each (`image_attachments.withholdEarlierImages`), as tool images do, and a down catalog tells the user once per turn. Counting them as attached now once left a session that attached a screenshot, restarted, and could not reach the catalog unable to send even plain text. Each recovers on a later turn once the catalog answers. +- Q19: Nothing. A withheld image stays in the store with a notice (`NoSilentWithhold`), session-dropped images become notes (`image_attachments.zig:883-887`), withheld earlier images become one note each (`image_attachments.withholdEarlierImages`), and the `vision_policy` trace line records the tool image and earlier image decisions. - Q21: None in the core. The resolver's refresh interval uses `io_mod.milliTimestamp` (`gateway_provider.zig:173`), unchanged. - Q22: The core has one waiting request and at most two effects per step (`Bounded`). Images in history are bounded by the existing caps in Q2. - Q24: One `step` call and one scan of the request's messages per model request (`requestHasToolImages`, `orchestrator.zig:6199-6208`, this change). Nothing runs at startup, per keystroke, or per token. @@ -34,12 +34,12 @@ How fx decides, for each model request, where images go: inline, through the vis - Q30: The gateway controls the tags over TLS. A repository cannot set capabilities, because project `.fx.json` accepts no profile-owned keys (`config_runtime.zig` `parseProjectSafeFields`). Tool output reaches the core only as a flag that images exist. - Q31: Nowhere. Core events and the trace line hold only model ids and tag names. - Q32: No. Images from permission-denied results still never leave the process (`vercel_protocol.zig:691-704`). -- Q33: Dropping `file_input` from one condition (`model_capabilities.zig:100` on `b0a90fd3a`) fixes the reported bug. +- Q33: Dropping `file_input` from one condition (`model_capabilities.zig:100` on `b0a90fd3a`) fixes the first reported bug. The second, an earlier image blocking every turn, needs the shell to split a request's user images at the turn's own message (`orchestrator.zig` `requestUserImages`) and the core to treat earlier ones as it treats tool images. - Q34: The core extraction. Without it the reported bug is still fixed, but Q9's ordering fix has no function to check against a model. The design keeps it for that reason and for G6; see R10. -- Q35: It reuses the resolver, `projectToolImageMessages`, and the wire encoder. It replaces `visionPolicy` and the inline re-resolve, so no parallel path remains, and it drops both inherited flaws: the `file-input` rule and the late re-resolve. +- Q35: It reuses the resolver, `projectToolImageMessages`, and the wire encoder. It replaces `visionPolicy` and the inline re-resolve, so no parallel path remains, and it drops both inherited flaws: the `file-input` rule and the late re-resolve. Earlier images reuse the tool image rule (`held`) and the dropped-image note pattern rather than a rule of their own. - Q36: Nothing. No setting, override, or provider table. -- Q37: `tests/e2e/file-tool-paths.test.ts` through the built binary, `sdk/tests/test-agent-images.mjs` through libfx on both backends, the drivers on the real core, and a live run of the built binary against the gateway (`GOAL.md`, item 6). -- Q38: The `vision_policy` trace line logs `image_support`, `route`, `mode`, `pending_images`, and `tool_images` for every request, and `image_gate` diagnostics record each failure (`orchestrator.zig:7357-7366`, this change). +- Q37: `tests/e2e/file-tool-paths.test.ts` through the built binary, `sdk/tests/test-agent-images.mjs` through libfx on both backends, the drivers on the real core, the binary stage on `fx ask` turns of the built binary (`binary-to-spec.ts`), `tests/e2e/vision-route-fake-gateway.test.ts` for a resumed turn while the catalog is down, and a live run of the built binary against the gateway (`GOAL.md`, item 6). +- Q38: The `vision_policy` trace line logs `image_support`, `route`, `mode`, `pending_images`, `tool_images`, and `earlier_images` for every request, and `image_gate` diagnostics record each failure (`orchestrator.zig:7357-7366`, this change). - Q39: Revert the change. No data needs migrating. Reverting `supportFromCatalog` alone (`image_route.zig:47-52`, this change) restores the old rule. Not applicable: Q17, Q20, Q23, Q28 (the core writes nothing that can be partial, holds no process, file, lock, or connection, consumes one synchronous event at a time, and changes no saved format, so nothing needs migrating). @@ -53,15 +53,16 @@ The laws `step` obeys. Each one is a named invariant or property in `spec/ImageR - **L3 NativeExcludesFallback**: native delivery and the vision tool never meet in one request. - **L4 OneSnapshot**: a request's route, vision tool mode, and tool image handling all follow the one support value the state holds after the step (ordering). - **L5 UnknownNeverInline**: no image goes to a model the catalog has not confirmed (ownership: the catalog decides). -- **L6 NoSilentWithhold**: tool images are attached, or withheld with a notice the model can act on, never neither. The vision tool is required exactly while user images wait for it (`RequiredWhenPending`). -- **L7 FailExactlyWhenUnroutable**: a request with user images and no route fails, with the reason that matches support. Nothing else fails. +- **L6 NoSilentWithhold**: tool images and images from earlier turns are attached, or withheld with a notice the model can act on, never neither. The vision tool is required exactly while images attached this turn wait for it (`RequiredWhenPending`). +- **L7 FailExactlyWhenUnroutable**: a request whose images were attached this turn and have no route fails, with the reason that matches support. Nothing else fails, so an image from an earlier turn never blocks a turn. - **L8 ResolveOncePerTurn**: the core asks for capabilities only when images wait on unknown support (`ResolveOnlyWhenNeeded`), and at most once per turn (idempotence). This also makes the shell's effect loop end. -- **L9 NotifyOncePerTurn**: the user hears about a down catalog only for tool images it withholds (`NotifyOnlyWhenDown`), and at most once per turn (idempotence). +- **L9 NotifyOncePerTurn**: the user hears about a down catalog only for images it withholds (`NotifyOnlyWhenDown`), and at most once per turn (idempotence). - **L10 DuplicateRequestIsQuiet**: a request delivered while a reply is owed runs nothing, and a reply nothing waits for changes nothing (`StaleReplyIsQuiet`) (idempotence and ordering). - **L11 Bounded**: at most one waiting request, and at most two effects per step, a notice and then one answer (bounds). - **L12 Answered**: every request that waits for a reply is answered, unless its turn ends first (liveness). - **L13 DecideOnlyWhenReady**: a decision comes only once no reply is owed. While one is owed, the turn has asked once and decided nothing (`PendingWaitsForReply`) (ordering). - **L14 TurnResets**: a new turn, and a new process after a crash, start with no request waiting and no capability request or notice spent. +- **L15 AskedBeforeUnknown**: a turn judges support unknown, by withholding images as unconfirmed or by failing for it, only after it asked the catalog in that turn (ordering). ## Enforcement @@ -75,7 +76,7 @@ The laws `step` obeys. Each one is a named invariant or property in `spec/ImageR | R4 | pass | The gateway catalog is the source, the resolver caches it, and the core keeps one snapshot per turn that only a reply to its own request replaces. | `inv:VisionImpliesNative`, `inv:OneSnapshot`, `prop:StaleReplyIsQuiet` | | R5 | pass | One event per request, at most one capability request per turn, at most two effects per step. Image bytes per request are capped as in Q2. | `inv:Bounded`, `prop:ResolveOncePerTurn`, `inv:ResolveOnlyWhenNeeded` | | R6 | pass | Only the capability request repeats safely, and the core still sends it once per turn. Sends, failures, and notices are never re-emitted. | `prop:DuplicateRequestIsQuiet`, `prop:NotifyOncePerTurn`, `prop:ResolveOncePerTurn` | -| R7 | pass | Crashes, a down or missing catalog, and lost, stale, and duplicated replies are actions in the model, and the code is checked on traces that inject them. | `inv:UnknownNeverInline`, `inv:TurnResets`, `prop:Answered`, `inv:FailExactlyWhenUnroutable`, `driver:code-to-spec` | +| R7 | pass | Crashes, a down or missing catalog, and lost, stale, and duplicated replies are actions in the model, and the code is checked on traces that inject them. | `inv:UnknownNeverInline`, `inv:TurnResets`, `prop:Answered`, `inv:FailExactlyWhenUnroutable`, `driver:code-to-spec`, `driver:binary-to-spec` | | R8 | n/a | No saved format or protocol changes (Q27). The routing decision is never saved. | | | R9 | pass | It drops two inherited flaws: the `file-input` rule and the re-resolve after the route is chosen. | `mutation:S1`, `mutation:C1`, `mutation:S2`, `mutation:C7`, `inv:OneSnapshot` | | R10 | fail | Accepted. The reported bug needs one line. The pure core, its harness, and the drivers exist so the ordering fix (Q9) is checkable against a model, as G6 requires. | `review:the core adds no setting, cache, or provider table; Q34 and Final design name what could be removed`, `driver:spec-to-code` | @@ -89,16 +90,17 @@ The laws `step` obeys. Each one is a named invariant or property in `spec/ImageR | L2 | Vision tool only on the fallback route | `inv:RouteModeCoherent`, `trace:RouteModeCoherent`, `mutation:S18`, `mutation:C17`, `zig:src/core/images/image_route.zig#every decision reads one support value` | | L3 | Native excludes the vision tool | `inv:NativeExcludesFallback`, `trace:NativeExcludesFallback`, `mutation:S19`, `mutation:C18`, `sdk:sdk/tests/test-agent-images.mjs#a native image model is not offered the vision tool` | | L4 | One snapshot per request | `inv:OneSnapshot`, `trace:OneSnapshot`, `mutation:S2`, `mutation:C7` | -| L5 | Unknown never inline | `inv:UnknownNeverInline`, `trace:UnknownNeverInline`, `mutation:S5`, `mutation:C4`, `zig:src/core/agent/runtime/gateway_step.zig#projectToolImageMessages tells the truth when the catalog is unavailable` | -| L6 | No silent withhold | `inv:NoSilentWithhold`, `inv:RequiredWhenPending`, `trace:NoSilentWithhold`, `trace:RequiredWhenPending`, `mutation:S17`, `mutation:C16`, `mutation:S10`, `mutation:C10`, `zig:src/core/agent/runtime/orchestrator.zig#requestHasToolImages ignores images the session dropped`, `e2e:tests/e2e/file-tool-paths.test.ts#read_file image is withheld with guidance for a text-only model` | -| L7 | Fail exactly when unroutable | `inv:FailExactlyWhenUnroutable`, `trace:FailExactlyWhenUnroutable`, `mutation:S8`, `mutation:C9`, `zig:src/core/images/image_route.zig#user images without a route fail the request and never send` | +| L5 | Unknown never inline | `inv:UnknownNeverInline`, `trace:UnknownNeverInline`, `mutation:S5`, `mutation:C4`, `zig:src/core/agent/runtime/gateway_step.zig#projectToolImageMessages tells the truth when the catalog is unavailable`, `mutation:S21`, `mutation:C20`, `driver:binary-to-spec` | +| L6 | No silent withhold | `inv:NoSilentWithhold`, `inv:RequiredWhenPending`, `trace:NoSilentWithhold`, `trace:RequiredWhenPending`, `mutation:S17`, `mutation:C16`, `mutation:S10`, `mutation:C10`, `zig:src/core/agent/runtime/orchestrator.zig#requestHasToolImages ignores images the session dropped`, `e2e:tests/e2e/file-tool-paths.test.ts#read_file image is withheld with guidance for a text-only model`, `mutation:S22`, `mutation:C21`, `zig:src/core/images/image_attachments.zig#requests leave out earlier images the route cannot carry, each with a note`, `zig:src/core/images/image_attachments.zig#earlier images withheld from seeded random histories always leave a note` | +| L7 | Fail exactly when unroutable | `inv:FailExactlyWhenUnroutable`, `trace:FailExactlyWhenUnroutable`, `mutation:S8`, `mutation:C9`, `zig:src/core/images/image_route.zig#user images without a route fail the request and never send`, `mutation:S20`, `mutation:C19`, `zig:src/core/images/image_route.zig#an earlier image never blocks a turn`, `zig:src/core/agent/runtime/orchestrator.zig#requestUserImages splits kept images at the turn's own message`, `zig:src/core/agent/runtime/tests/gateway_flow.zig#processQueuedPrompt sends a text-only turn while a down catalog withholds an earlier image`, `e2e:tests/e2e/vision-route-fake-gateway.test.ts#a resumed text-only turn is sent while the catalog is down, with the earlier image withheld`, `driver:binary-to-spec` | | L8 | One capability request per turn, only for images | `inv:ResolveOnlyWhenNeeded`, `prop:ResolveOncePerTurn`, `trace:ResolveOnlyWhenNeeded`, `trace:ResolveOncePerTurn`, `mutation:S3`, `mutation:C2`, `mutation:S15`, `mutation:C14`, `zig:src/core/images/image_route.zig#a turn asks for capabilities at most once and answers the request it held` | -| L9 | One catalog-down notice per turn, only when down | `inv:NotifyOnlyWhenDown`, `prop:NotifyOncePerTurn`, `trace:NotifyOnlyWhenDown`, `trace:NotifyOncePerTurn`, `mutation:S4`, `mutation:C3`, `mutation:S16`, `mutation:C15`, `zig:src/core/images/image_route.zig#the catalog-down notice reaches the user once per turn` | +| L9 | One catalog-down notice per turn, only when down | `inv:NotifyOnlyWhenDown`, `prop:NotifyOncePerTurn`, `trace:NotifyOnlyWhenDown`, `trace:NotifyOncePerTurn`, `mutation:S4`, `mutation:C3`, `mutation:S16`, `mutation:C15`, `zig:src/core/images/image_route.zig#the catalog-down notice reaches the user once per turn`, `driver:binary-to-spec` | | L10 | Duplicates and stale replies are quiet | `prop:DuplicateRequestIsQuiet`, `prop:StaleReplyIsQuiet`, `trace:DuplicateRequestIsQuiet`, `trace:StaleReplyIsQuiet`, `mutation:S6`, `mutation:C5`, `mutation:S7`, `mutation:C6` | | L11 | Bounded | `inv:Bounded`, `trace:Bounded`, `mutation:S12`, `mutation:C11`, `zig:src/core/images/image_route.zig#abstract maps the pending request onto a sequence of at most one` | | L12 | Every waiting request is answered | `prop:Answered`, `mutation:S11`, `review:a finite trace cannot show liveness; TLC proves Answered over the whole model under fairness of replies, and ConformsToSpec makes each recorded reply clear its request` | | L13 | Decide only when no reply is owed | `inv:DecideOnlyWhenReady`, `inv:PendingWaitsForReply`, `trace:DecideOnlyWhenReady`, `trace:PendingWaitsForReply`, `mutation:S13`, `mutation:C12`, `mutation:S14`, `mutation:C13` | | L14 | Turns and processes start clean | `inv:TurnResets`, `trace:TurnResets`, `mutation:S9`, `mutation:C8` | +| L15 | Unknown only after asking | `inv:AskedBeforeUnknown`, `trace:AskedBeforeUnknown`, `mutation:S23`, `mutation:C22`, `zig:src/core/images/image_route.zig#the core keeps the model's laws on arbitrary event sequences`, `zig:src/core/images/image_route.zig#the core keeps the model's laws on seeded random event sequences` | ## Final design @@ -108,7 +110,7 @@ The laws `step` obeys. Each one is a named invariant or property in `spec/ImageR ### The core -`src/core/images/image_route.zig` (this change) imports only `std`. +`src/core/images/image_route.zig` (this change) imports only `std` outside its tests. - **State** (`:107-116`): `support`, the turn's one capability snapshot; `resolved` and `notified`, the turn's spent capability request and notice; `pending`, the request waiting for a reply, if any. - **Events** (`:118-127`): `turn_started(Support)`, `request_ready(Request)`, and `capabilities_resolved(Support)`. Time does not enter. I/O results arrive as `capabilities_resolved`, and failures arrive as the support value they produce. @@ -128,6 +130,12 @@ The turn loop in `processQueuedPromptLoop` is the only code that runs effects. `visionPolicy`, `ImageRoute`, `VisionPolicy`, and the per-turn flags `tool_image_capabilities_resolved` and `tool_image_strip_notified` are gone, along with their tests. The core's tests and the model cover the same laws. +### Earlier images + +A request's user images are split at the turn's own user message (`orchestrator.zig` `requestUserImages`): `user_images` are the ones attached this turn and `earlier_images` the ones earlier turns left in the history, counting only images the session still holds. Only `user_images` can fail a request (L7). `decision` gives earlier images the tool image rule (`held` in `image_route.zig`), so they go inline to a model listed with vision, through the vision tool's image references on the fallback route, and otherwise leave the request as one note each (`image_attachments.withholdEarlierImages`). A down catalog that withholds them tells the user once per turn (`catalogDownNotice`), and the turn asks the catalog before judging support unknown (L15). + +`binary-to-spec.ts` checks this through the built binary: each `fx ask` turn is recorded with the catalog view it saw, the flags the spec says the shell computes from the turn, and what its first request carried, and `BinaryImageRoute.tla` holds every turn to `DecideOut`. On the binary before this change it fails on exactly the text-only turns after an earlier image while the catalog is missing or down. + ### Mechanisms added, and the answers that required them | Mechanism | Required by | @@ -135,6 +143,8 @@ The turn loop in `processQueuedPromptLoop` is the only code that runs effects. | Support from `vision` alone | Q1 and R9: the inherited rule reads a document tag as an image tag | | Asking before deciding, with the request held in `pending` | Q9: deciding first splits one request across two snapshots | | `pending` replaced by a newer request, and stale replies ignored | Q8 and Q11 | +| `earlier_images`, split from `user_images` | Q18: an earlier image failed every later turn while support was unknown | +| The binary stage and `BinaryImageRoute.tla` | Q37: the shell's flags, which caused the second bug, are outside what the core harness can see | | A pure core with `abstract` and a harness | Q37 and G6: the orchestrator cannot be checked against a model, and a pure step can | ### Rules this design breaks diff --git a/tests/tla/image_route/design/GOAL.md b/tests/tla/image_route/design/GOAL.md index 3226b0db4..8833e2347 100644 --- a/tests/tla/image_route/design/GOAL.md +++ b/tests/tla/image_route/design/GOAL.md @@ -21,6 +21,7 @@ Each criterion is a check that passes on this change and failed, or could fail, | G5 | No extra catalog traffic: at most one capability request per turn from the image decision, and none for a request without images. | `ResolveOncePerTurn` and `ResolveOnlyWhenNeeded` | | G6 | The decision is one pure function, checked against its model in both directions. | `bun run verify` in `tests/tla/image_route` | | G7 | Nothing slows startup or adds network I/O on a path without images. | The `Startup Latency` CI job, and `ResolveOnlyWhenNeeded` | +| G8 | An image from an earlier turn never fails a later turn: while support is unknown, the turn is sent with the image withheld and a note in its place, and only an image attached now can fail. | `FailExactlyWhenUnroutable` and planted bugs S20 and C19, the binary stage of `bun run verify`, and `tests/e2e/vision-route-fake-gateway.test.ts`, "a resumed text-only turn is sent while the catalog is down, with the earlier image withheld". Both fail on the binary before this change | ## Non-goals diff --git a/tests/tla/image_route/mutations.json b/tests/tla/image_route/mutations.json index 8d3caa749..448a01dde 100644 --- a/tests/tla/image_route/mutations.json +++ b/tests/tla/image_route/mutations.json @@ -18,8 +18,8 @@ { "id": "S3", "breaks": "A turn asks for capabilities again after it already asked.", - "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ (r.user_images \\/ r.tool_images)", - "replace": "NeedsResolve(r) == support = \"unknown\" /\\ (r.user_images \\/ r.tool_images)", + "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ HasImages(r)", + "replace": "NeedsResolve(r) == support = \"unknown\" /\\ HasImages(r)", "expect": "ResolveOncePerTurn" }, { @@ -102,7 +102,7 @@ { "id": "S15", "breaks": "The core asks for capabilities for a request without images.", - "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ (r.user_images \\/ r.tool_images)", + "find": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved /\\ HasImages(r)", "replace": "NeedsResolve(r) == support = \"unknown\" /\\ ~resolved", "expect": "ResolveOnlyWhenNeeded" }, @@ -133,6 +133,34 @@ "find": "LET route == CASE s = \"native\" -> \"native\"", "replace": "LET route == CASE s = \"native\" -> (IF r.fallback THEN \"fallback\" ELSE \"native\")", "expect": "NativeExcludesFallback" + }, + { + "id": "S20", + "breaks": "An earlier image fails the request like one attached now: the reported bug.", + "find": "Unroutable(s, r) == r.user_images /\\ Decide(s, r).route = \"unavailable\"", + "replace": "Unroutable(s, r) == (r.user_images \\/ r.earlier_images) /\\ Decide(s, r).route = \"unavailable\"", + "expect": "FailExactlyWhenUnroutable" + }, + { + "id": "S21", + "breaks": "Earlier images go inline whatever the support.", + "find": "earlier == IF ~r.earlier_images THEN \"none\" ELSE Held(s, route)", + "replace": "earlier == IF ~r.earlier_images THEN \"none\" ELSE \"attached\"", + "expect": "UnknownNeverInline" + }, + { + "id": "S22", + "breaks": "Earlier images vanish from the request without a notice.", + "find": "earlier == IF ~r.earlier_images THEN \"none\" ELSE Held(s, route)", + "replace": "earlier == \"none\"", + "expect": "NoSilentWithhold" + }, + { + "id": "S23", + "breaks": "Earlier images are withheld as unconfirmed without the turn asking the catalog.", + "find": "HasImages(r) == r.user_images \\/ r.earlier_images \\/ r.tool_images", + "replace": "HasImages(r) == r.user_images \\/ r.tool_images", + "expect": "AskedBeforeUnknown" } ], "code": [ @@ -146,15 +174,15 @@ { "id": "C2", "breaks": "A turn asks for capabilities again after it already asked.", - "find": "if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) {", - "replace": "if (state.support == .unknown and (request.user_images or request.tool_images)) {", + "find": "if (state.support == .unknown and !state.resolved and hasImages(request)) {", + "replace": "if (state.support == .unknown and hasImages(request)) {", "expect": "ResolveOncePerTurn" }, { "id": "C3", "breaks": "The catalog-down notice repeats within a turn.", - "find": "if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) {", - "replace": "if (chosen.tool_images == .withheld_unknown and request.catalog_down) {", + "find": "if (withholdsUnknown(chosen) and request.catalog_down and !state.notified) {", + "replace": "if (withholdsUnknown(chosen) and request.catalog_down) {", "expect": "NotifyOncePerTurn" }, { @@ -230,15 +258,15 @@ { "id": "C14", "breaks": "The core asks for capabilities for a request without images.", - "find": "if (state.support == .unknown and !state.resolved and (request.user_images or request.tool_images)) {", + "find": "if (state.support == .unknown and !state.resolved and hasImages(request)) {", "replace": "if (state.support == .unknown and !state.resolved) {", "expect": "ResolveOnlyWhenNeeded" }, { "id": "C15", "breaks": "The catalog-down notice appears when the catalog is up.", - "find": "if (chosen.tool_images == .withheld_unknown and request.catalog_down and !state.notified) {", - "replace": "if (chosen.tool_images == .withheld_unknown and !state.notified) {", + "find": "if (withholdsUnknown(chosen) and request.catalog_down and !state.notified) {", + "replace": "if (withholdsUnknown(chosen) and !state.notified) {", "expect": "NotifyOnlyWhenDown" }, { @@ -261,6 +289,34 @@ "find": ".native => .native,", "replace": ".native => if (request.fallback) .fallback else .native,", "expect": "NativeExcludesFallback" + }, + { + "id": "C19", + "breaks": "An earlier image fails the request like one attached now: the reported bug.", + "find": "if (request.user_images and chosen.route == .unavailable) {", + "replace": "if ((request.user_images or request.earlier_images) and chosen.route == .unavailable) {", + "expect": "FailExactlyWhenUnroutable" + }, + { + "id": "C20", + "breaks": "Earlier images go inline whatever the support.", + "find": ".earlier_images = held(request.earlier_images, support, route),", + "replace": ".earlier_images = if (request.earlier_images) .attached else .none,", + "expect": "UnknownNeverInline" + }, + { + "id": "C21", + "breaks": "Earlier images vanish from the request without a notice.", + "find": ".earlier_images = held(request.earlier_images, support, route),", + "replace": ".earlier_images = .none,", + "expect": "NoSilentWithhold" + }, + { + "id": "C22", + "breaks": "Earlier images are withheld as unconfirmed without the turn asking the catalog.", + "find": "return request.user_images or request.earlier_images or request.tool_images;", + "replace": "return request.user_images or request.tool_images;", + "expect": "AskedBeforeUnknown" } ] } diff --git a/tests/tla/image_route/spec/BinaryImageRoute.cfg b/tests/tla/image_route/spec/BinaryImageRoute.cfg new file mode 100644 index 000000000..e10674dbf --- /dev/null +++ b/tests/tla/image_route/spec/BinaryImageRoute.cfg @@ -0,0 +1,6 @@ +\* Every turn the built fx binary ran shows what ImageRoute decides for it. +\* BinaryData.tla is generated next to this file for each run. +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +INVARIANT + BinaryConforms diff --git a/tests/tla/image_route/spec/BinaryImageRoute.tla b/tests/tla/image_route/spec/BinaryImageRoute.tla new file mode 100644 index 000000000..c73fa1057 --- /dev/null +++ b/tests/tla/image_route/spec/BinaryImageRoute.tla @@ -0,0 +1,56 @@ +-------------------------- MODULE BinaryImageRoute -------------------------- +(***************************************************************************) +(* Checks what the built fx binary did against ImageRoute. *) +(* *) +(* tests/tla/drivers/image_route/binary-to-spec.ts runs `fx ask` turns *) +(* against a fake gateway and records each one in BinaryData.tla, which *) +(* is generated for each run: the catalog view the turn saw, the request *) +(* flags the shell must compute from the turn itself (an image attached *) +(* now, an image an earlier turn left in the history, the vision tool, a *) +(* down catalog), and what the binary did: the error it failed with, or *) +(* what its first model request carried and what it told the user. *) +(* *) +(* A turn starts with no notice spent, so the model's answer to the *) +(* turn's first request is DecideOut under the support the catalog's view *) +(* derives. Observe maps those effects onto what a request body and the *) +(* process show. BinaryConforms holds when the binary showed exactly that *) +(* for every turn, which checks the shell's flags as well as the core. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, BinaryData + +\* at is the turn under check, and expected is what the model says that +\* turn shows, kept as a variable so TLC's error trace prints it. +VARIABLES at, expected + +IR == INSTANCE ImageRoute WITH support <- "unknown", resolved <- FALSE, notified <- FALSE, + pending <- <<>>, out <- <<>>, act <- [name |-> "Init"] + +Kinds(effects) == {effects[i].kind : i \in 1..Len(effects)} +Answer(effects) == CHOOSE e \in {effects[i] : i \in 1..Len(effects)} : e.kind \in {"send", "fail"} + +\* What a turn shows for the effects its first request r got. Every field +\* is present for every outcome, so observations compare as plain records. +Observe(effects, r) == + LET e == Answer(effects) + sent == e.kind = "send" + IN [kind |-> e.kind, + reason |-> IF sent THEN "none" ELSE e.reason, + notified |-> "notify" \in Kinds(effects), + inline_now |-> IF sent THEN r.user_images /\ e.route = "native" ELSE FALSE, + inline_earlier |-> IF sent THEN e.earlier_images = "attached" ELSE FALSE, + vision_tool |-> IF sent THEN e.mode # "unavailable" ELSE FALSE, + vision_required |-> IF sent THEN e.mode = "required" ELSE FALSE, + references |-> IF sent THEN e.route = "fallback" /\ (r.user_images \/ r.earlier_images) ELSE FALSE, + earlier_note |-> IF ~sent THEN "none" + ELSE CASE e.earlier_images = "withheld_unknown" -> "unknown" + [] e.earlier_images = "withheld_dead_end" -> "dead_end" + [] OTHER -> "none"] + +Expected(o) == Observe(IR!DecideOut(IR!Derive(o.view), o.req, FALSE), o.req) + +Init == at = 1 /\ expected = Expected(Observations[1]) +Next == at < Len(Observations) /\ at' = at + 1 /\ expected' = Expected(Observations[at + 1]) +Spec == Init /\ [][Next]_<> + +BinaryConforms == expected = Observations[at].seen +============================================================================= diff --git a/tests/tla/image_route/spec/ImageRoute.tla b/tests/tla/image_route/spec/ImageRoute.tla index a37e749db..8f8d6ff9d 100644 --- a/tests/tla/image_route/spec/ImageRoute.tla +++ b/tests/tla/image_route/spec/ImageRoute.tla @@ -19,6 +19,12 @@ (* support, resolved, notified, and pending are `abstract(state)` in the *) (* code. out is the effects the step returned, and act is the event the *) (* step took, recorded so the laws can name it. *) +(* *) +(* A request's user images are split by when they arrived: user_images *) +(* are the ones attached this turn, and earlier_images are the ones from *) +(* earlier turns that the history still holds. Only images attached this *) +(* turn can fail a request. Earlier ones, like tool images, are attached *) +(* or withheld with a notice, so an old image never blocks a new turn. *) (***************************************************************************) EXTENDS Naturals, Sequences @@ -31,11 +37,11 @@ Reasons == {"capability_unknown", "no_native_image"} Views == [kind: {"listed"}, vision: BOOLEAN, file_input: BOOLEAN] \cup [kind: {"missing", "down"}, vision: {FALSE}, file_input: {FALSE}] -Requests == {r \in [user_images: BOOLEAN, pending_images: BOOLEAN, tool_images: BOOLEAN, - fallback: BOOLEAN, catalog_down: BOOLEAN] : +Requests == {r \in [user_images: BOOLEAN, earlier_images: BOOLEAN, pending_images: BOOLEAN, + tool_images: BOOLEAN, fallback: BOOLEAN, catalog_down: BOOLEAN] : r.pending_images => r.user_images} -Sends == [kind: {"send"}, route: Routes, mode: Modes, tool_images: ToolImages] +Sends == [kind: {"send"}, route: Routes, mode: Modes, tool_images: ToolImages, earlier_images: ToolImages] Effects == [kind: {"resolve", "notify"}] \cup Sends \cup [kind: {"fail"}, reason: Reasons] \* At most one request; the core's `?Request`. @@ -53,6 +59,12 @@ vars == <> \* `supportFromCatalog`. Derive(v) == IF v.kind = "listed" THEN (IF v.vision THEN "native" ELSE "non_native") ELSE "unknown" +\* `held`: how images already in the history travel under support s on +\* route. Tool images and earlier user images follow this one rule. +Held(s, route) == CASE s = "native" -> "attached" + [] s = "unknown" -> "withheld_unknown" + [] OTHER -> IF route = "fallback" THEN "withheld_fallback" ELSE "withheld_dead_end" + \* `decision`. Decide(s, r) == LET route == CASE s = "native" -> "native" @@ -60,14 +72,15 @@ Decide(s, r) == [] OTHER -> IF r.fallback THEN "fallback" ELSE "unavailable" mode == IF route # "fallback" THEN "unavailable" ELSE IF r.pending_images THEN "required" ELSE "optional" - tool == IF ~r.tool_images THEN "none" - ELSE CASE s = "native" -> "attached" - [] s = "unknown" -> "withheld_unknown" - [] OTHER -> IF route = "fallback" THEN "withheld_fallback" ELSE "withheld_dead_end" - IN [kind |-> "send", route |-> route, mode |-> mode, tool_images |-> tool] + tool == IF ~r.tool_images THEN "none" ELSE Held(s, route) + earlier == IF ~r.earlier_images THEN "none" ELSE Held(s, route) + IN [kind |-> "send", route |-> route, mode |-> mode, tool_images |-> tool, earlier_images |-> earlier] + +\* Whether send e withholds some image as unconfirmed. +WithholdsUnknown(e) == e.tool_images = "withheld_unknown" \/ e.earlier_images = "withheld_unknown" Unroutable(s, r) == r.user_images /\ Decide(s, r).route = "unavailable" -Notifies(s, r, n) == ~Unroutable(s, r) /\ Decide(s, r).tool_images = "withheld_unknown" /\ r.catalog_down /\ ~n +Notifies(s, r, n) == ~Unroutable(s, r) /\ WithholdsUnknown(Decide(s, r)) /\ r.catalog_down /\ ~n \* `decide`: the effects of deciding r under s, and the next notified flag. DecideOut(s, r, n) == @@ -78,7 +91,9 @@ DecideOut(s, r, n) == DecideNotified(s, r, n) == n \/ Notifies(s, r, n) -NeedsResolve(r) == support = "unknown" /\ ~resolved /\ (r.user_images \/ r.tool_images) +HasImages(r) == r.user_images \/ r.earlier_images \/ r.tool_images + +NeedsResolve(r) == support = "unknown" /\ ~resolved /\ HasImages(r) Init == /\ support = "unknown" @@ -175,16 +190,18 @@ VisionImpliesNative == /\ act.view.kind # "listed" => support = "unknown" \* L5: no image goes to a model the catalog has not confirmed. -UnknownNeverInline == \A e \in SendsOut : e.tool_images = "attached" => support = "native" +UnknownNeverInline == + \A e \in SendsOut : (e.tool_images = "attached" \/ e.earlier_images = "attached") => support = "native" -\* L4: route, mode, and tool images all follow the one support value the -\* state holds after the step. +\* L4: route, mode, tool images, and earlier images all follow the one +\* support value the state holds after the step. OneSnapshot == \A e \in SendsOut : /\ (e.route = "native") <=> (support = "native") - /\ e.tool_images = "withheld_unknown" => support = "unknown" - /\ e.tool_images = "withheld_fallback" => (support = "non_native" /\ e.route = "fallback") - /\ e.tool_images = "withheld_dead_end" => (support = "non_native" /\ e.route = "unavailable") + /\ \A h \in {e.tool_images, e.earlier_images} : + /\ h = "withheld_unknown" => support = "unknown" + /\ h = "withheld_fallback" => (support = "non_native" /\ e.route = "fallback") + /\ h = "withheld_dead_end" => (support = "non_native" /\ e.route = "unavailable") \* L2: the vision tool is offered exactly on the fallback route. RouteModeCoherent == \A e \in SendsOut : (e.route = "fallback") <=> (e.mode # "unavailable") @@ -192,15 +209,20 @@ RouteModeCoherent == \A e \in SendsOut : (e.route = "fallback") <=> (e.mode # "u \* L3: native delivery and the vision tool never meet. NativeExcludesFallback == \A e \in SendsOut : support = "native" => (e.route = "native" /\ e.mode = "unavailable") -\* L6: tool images are attached or withheld with a notice; never neither. +\* L6: tool images and earlier images are attached or withheld with a +\* notice; never neither. NoSilentWithhold == - \A e \in SendsOut : Decided # <<>> /\ (Head(Decided).tool_images <=> e.tool_images # "none") + \A e \in SendsOut : + /\ Decided # <<>> + /\ Head(Decided).tool_images <=> e.tool_images # "none" + /\ Head(Decided).earlier_images <=> e.earlier_images # "none" \* L6: the vision tool is required exactly while user images wait. RequiredWhenPending == \A e \in SendsOut : e.route = "fallback" => ((e.mode = "required") <=> Head(Decided).pending_images) -\* L7: user images without a route fail the request; nothing else does. +\* L7: images attached this turn without a route fail the request; nothing +\* else does, so earlier images never block a turn. FailExactlyWhenUnroutable == /\ \A e \in FailsOut : /\ Decided # <<>> @@ -214,13 +236,19 @@ ResolveOnlyWhenNeeded == HasKind("resolve") => /\ act.name = "RequestReady" /\ support = "unknown" - /\ (act.req.user_images \/ act.req.tool_images) + /\ HasImages(act.req) /\ pending = <> -\* L9: the user hears about a down catalog only for tool images it withholds. +\* L15: support is judged unknown, by withholding images as unconfirmed or +\* failing for it, only after the turn asked the catalog. +AskedBeforeUnknown == + /\ \A e \in SendsOut : WithholdsUnknown(e) => resolved + /\ \A e \in FailsOut : e.reason = "capability_unknown" => resolved + +\* L9: the user hears about a down catalog only for images it withholds. NotifyOnlyWhenDown == HasKind("notify") => - /\ \E e \in SendsOut : e.tool_images = "withheld_unknown" + /\ \E e \in SendsOut : WithholdsUnknown(e) /\ Head(Decided).catalog_down \* L13: a decision comes only once no reply is owed. diff --git a/tests/tla/image_route/spec/MCImageRoute.cfg b/tests/tla/image_route/spec/MCImageRoute.cfg index 94bb4f0cb..71dea2686 100644 --- a/tests/tla/image_route/spec/MCImageRoute.cfg +++ b/tests/tla/image_route/spec/MCImageRoute.cfg @@ -15,6 +15,7 @@ INVARIANT RequiredWhenPending FailExactlyWhenUnroutable ResolveOnlyWhenNeeded + AskedBeforeUnknown NotifyOnlyWhenDown DecideOnlyWhenReady TurnResets diff --git a/tests/tla/image_route/spec/TraceImageRoute.cfg b/tests/tla/image_route/spec/TraceImageRoute.cfg index 4712d15bd..75317db0c 100644 --- a/tests/tla/image_route/spec/TraceImageRoute.cfg +++ b/tests/tla/image_route/spec/TraceImageRoute.cfg @@ -18,6 +18,7 @@ INVARIANT RequiredWhenPending FailExactlyWhenUnroutable ResolveOnlyWhenNeeded + AskedBeforeUnknown NotifyOnlyWhenDown DecideOnlyWhenReady TurnResets diff --git a/tests/tla/image_route/spec/TraceImageRoute.tla b/tests/tla/image_route/spec/TraceImageRoute.tla index b4fd9891a..80b2eae50 100644 --- a/tests/tla/image_route/spec/TraceImageRoute.tla +++ b/tests/tla/image_route/spec/TraceImageRoute.tla @@ -65,6 +65,7 @@ NoSilentWithhold == IR!NoSilentWithhold RequiredWhenPending == IR!RequiredWhenPending FailExactlyWhenUnroutable == IR!FailExactlyWhenUnroutable ResolveOnlyWhenNeeded == IR!ResolveOnlyWhenNeeded +AskedBeforeUnknown == IR!AskedBeforeUnknown NotifyOnlyWhenDown == IR!NotifyOnlyWhenDown DecideOnlyWhenReady == IR!DecideOnlyWhenReady TurnResets == IR!TurnResets