From f792a1fcd272bb6788fa8db01515806a15f9e9ab Mon Sep 17 00:00:00 2001 From: Marco Doehler Date: Sat, 14 Mar 2026 19:03:07 +0000 Subject: [PATCH 1/4] =?UTF-8?q?Phase=2020:=20LLM-Dokumentation=20=E2=80=94?= =?UTF-8?q?=20FTL-Spec,=20MCP-Integration,=20Beispiele?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Haiku 4.5 --- ftl-examples.md | 612 +++++++++++++++++++++++++++++++++++++++++++++ ftl-spec.md | 402 +++++++++++++++++++++++++++++ mcp-integration.md | 327 ++++++++++++++++++++++++ 3 files changed, 1341 insertions(+) create mode 100644 ftl-examples.md create mode 100644 ftl-spec.md create mode 100644 mcp-integration.md diff --git a/ftl-examples.md b/ftl-examples.md new file mode 100644 index 0000000..bfaef4d --- /dev/null +++ b/ftl-examples.md @@ -0,0 +1,612 @@ +# FTL Examples + +## hello_world + +Minimal program: writes "Hello World\n" to stdout, exits 0 on success, 1 on failure. + +Nodes: 5C + 2E(syscall_write, syscall_exit) + 1E(syscall_exit) + 3K + 2V + 3T + 1R +Effects: IO, PROC +Contracts: 2 pre-conditions on syscall_write arguments (fd==1, len==12) + +```ftl +// Hello World — FLUX v3 FTL +// Spec Section 11: Minimal-Beispiel + +// Typen +T:a1 = array { element: u8, max_length: 12 } +T:a2 = integer { bits: 64, signed: false } +T:a3 = unit + +// Regionen +R:b1 = region { lifetime: static } + +// Compute-Nodes +C:c1 = const_bytes { value: [72,101,108,108,111,32,87,111,114,108,100,10], type: T:a1, region: R:b1 } +C:c2 = const { value: 1, type: T:a2 } +C:c3 = const { value: 12, type: T:a2 } +C:c4 = const { value: 0, type: T:a2 } +C:c5 = const { value: 1, type: T:a2 } + +// Effect-Nodes +E:d1 = syscall_write { inputs: [C:c2, C:c1, C:c3], type: T:a2, effects: [IO], success: K:f2, failure: K:f3 } + +// Success path: exit(0) +K:f2 = seq { steps: [E:d2] } +E:d2 = syscall_exit { inputs: [C:c4], type: T:a3, effects: [PROC] } + +// Failure path: exit(1) +K:f3 = seq { steps: [E:d3] } +E:d3 = syscall_exit { inputs: [C:c5], type: T:a3, effects: [PROC] } + +// Contracts +V:e1 = contract { target: E:d1, pre: C:c2.val == 1 } +V:e2 = contract { target: E:d1, pre: C:c3.val == 12 } + +// Entry +K:f1 = seq { steps: [E:d1] } +entry: K:f1 +``` + +## ffi + +FFI calls to C library functions (malloc, free, memcpy, fopen, fwrite, fclose). +Demonstrates: X-Node declarations, call_extern E-Nodes, opaque types, trust: EXTERN contracts, cleanup paths. + +Nodes: 8C + 12E(call_extern, syscall_exit) + 10K + 7V + 8T + 2R + 6X +Effects: IO, MEM, PROC +Contracts: 5 trust:EXTERN assumptions, 2 verified pre-conditions + +```ftl +// FFI — External C library calls (malloc/free/memcpy) +// Demonstrates X-Node declarations, call_extern E-Nodes, +// opaque types, and trust: EXTERN contracts + +// === Typen === +T:a1 = integer { bits: 64, signed: false } +T:a2 = integer { bits: 32, signed: true } +T:a3 = unit +T:a4 = boolean +T:ptr = integer { bits: 64, signed: false } +T:size_t = integer { bits: 64, signed: false } + +// Opaque type for external struct (e.g. FILE) +T:ext_file = opaque { size: 216, align: 8 } + +// Buffer type +T:buf = array { element: u8, max_length: 4096 } + +// === Regionen === +R:b1 = region { lifetime: static } +R:b2 = region { lifetime: scoped, parent: R:b1 } + +// === Extern declarations (X-Nodes) === +X:ext1 = extern { name: "malloc", abi: C, params: [T:size_t], result: T:ptr, effects: [MEM] } +X:ext2 = extern { name: "free", abi: C, params: [T:ptr], result: T:a3, effects: [MEM] } +X:ext3 = extern { name: "memcpy", abi: C, params: [T:ptr, T:ptr, T:size_t], result: T:ptr, effects: [MEM] } +X:ext4 = extern { name: "fopen", abi: C, params: [T:ptr, T:ptr], result: T:ptr, effects: [IO] } +X:ext5 = extern { name: "fwrite", abi: C, params: [T:ptr, T:size_t, T:size_t, T:ptr], result: T:size_t, effects: [IO] } +X:ext6 = extern { name: "fclose", abi: C, params: [T:ptr], result: T:a2, effects: [IO] } + +// === Constants === +C:c_alloc_size = const { value: 4096, type: T:size_t } +C:c_zero = const { value: 0, type: T:a1 } +C:c_one = const { value: 1, type: T:size_t } +C:c_null = const { value: 0, type: T:ptr } +C:c_exit0 = const { value: 0, type: T:a2 } +C:c_exit1 = const { value: 1, type: T:a2 } + +// File path and mode as byte arrays +T:a_path = array { element: u8, max_length: 16 } +T:a_mode = array { element: u8, max_length: 4 } +C:c_path = const_bytes { value: [47,116,109,112,47,111,117,116,46,98,105,110,0], type: T:a_path, region: R:b1 } +C:c_mode = const_bytes { value: [119,98,0], type: T:a_mode, region: R:b1 } + +// Data to write +C:c_data = const_bytes { value: [72,101,108,108,111,32,70,70,73,10], type: T:buf, region: R:b1 } +C:c_data_len = const { value: 10, type: T:size_t } + +// === Step 1: malloc — allocate buffer === +E:d1 = call_extern { target: X:ext1, inputs: [C:c_alloc_size], type: T:ptr, effects: [MEM], success: K:f_alloc_ok, failure: K:f_cleanup } + +// === Step 2: memcpy — copy data into allocated buffer === +K:f_alloc_ok = seq { steps: [E:d2] } +E:d2 = call_extern { target: X:ext3, inputs: [E:d1, C:c_data, C:c_data_len], type: T:ptr, effects: [MEM], success: K:f_copy_ok, failure: K:f_free_and_exit } + +// === Step 3: fopen — open output file === +K:f_copy_ok = seq { steps: [E:d3] } +E:d3 = call_extern { target: X:ext4, inputs: [C:c_path, C:c_mode], type: T:ptr, effects: [IO], success: K:f_file_ok, failure: K:f_free_and_exit } + +// === Step 4: fwrite — write buffer to file === +K:f_file_ok = seq { steps: [E:d4] } +E:d4 = call_extern { target: X:ext5, inputs: [E:d1, C:c_one, C:c_data_len, E:d3], type: T:size_t, effects: [IO], success: K:f_write_ok, failure: K:f_close_free_exit } + +// === Step 5: fclose — close file === +K:f_write_ok = seq { steps: [E:d5] } +E:d5 = call_extern { target: X:ext6, inputs: [E:d3], type: T:a2, effects: [IO], success: K:f_close_ok, failure: K:f_free_and_exit } + +// === Step 6: free — release buffer === +K:f_close_ok = seq { steps: [E:d6] } +E:d6 = call_extern { target: X:ext2, inputs: [E:d1], type: T:a3, effects: [MEM], success: K:f_success, failure: K:f_exit_fail } + +// === Success exit === +K:f_success = seq { steps: [E:d_exit0] } +E:d_exit0 = syscall_exit { inputs: [C:c_exit0], type: T:a3, effects: [PROC] } + +// === Failure / Cleanup paths === + +// Cleanup: close file, free buffer, exit(1) +K:f_close_free_exit = seq { steps: [E:d_close_cleanup, E:d_free_cleanup, E:d_exit1] } +E:d_close_cleanup = call_extern { target: X:ext6, inputs: [E:d3], type: T:a2, effects: [IO], success: K:f_free_and_exit, failure: K:f_free_and_exit } + +// Cleanup: free buffer, exit(1) +K:f_free_and_exit = seq { steps: [E:d_free_cleanup, E:d_exit1] } +E:d_free_cleanup = call_extern { target: X:ext2, inputs: [E:d1], type: T:a3, effects: [MEM], success: K:f_exit_fail, failure: K:f_exit_fail } + +// Cleanup: just exit(1) +K:f_exit_fail = seq { steps: [E:d_exit1] } +K:f_cleanup = seq { steps: [E:d_exit1] } +E:d_exit1 = syscall_exit { inputs: [C:c_exit1], type: T:a3, effects: [PROC] } + +// === Contracts (trust: EXTERN for FFI assumptions) === + +// malloc returns non-null for valid size +V:e1 = contract { target: E:d1, trust: EXTERN, assume: result != 0, post: region_valid(R:b2) } + +// memcpy returns dest pointer +V:e2 = contract { target: E:d2, trust: EXTERN, assume: result == E:d1, post: result != 0 } + +// fopen returns non-null on success +V:e3 = contract { target: E:d3, trust: EXTERN, assume: result != 0, post: result != 0 } + +// fwrite writes exactly the requested bytes +V:e4 = contract { target: E:d4, trust: EXTERN, assume: result == C:c_data_len.val, post: result > 0 } + +// free does not fail (void return) +V:e5 = contract { target: E:d6, trust: EXTERN, assume: true, post: true } + +// Verified contracts: parameter types match declarations +V:e6 = contract { target: E:d1, pre: C:c_alloc_size.val > 0 } +V:e7 = contract { target: E:d4, pre: C:c_data_len.val <= 4096 } + +// === Main sequence === +K:f_main = seq { steps: [E:d1] } +entry: K:f_main +``` + +## snake_game + +Full game: terminal raw mode, ANSI rendering, ALSA sound, game loop with collision detection. +Demonstrates: struct/variant types, M-nodes (alloc/load/store), K:loop, K:branch, syscall_ioctl, syscall_open, syscall_close, syscall_nanosleep, call_pure, generic ops (bhaskara_approx, or), forall contracts with index access. + +Nodes: ~30C + ~15E + ~20K + 10V + 10T + 4R + 9M +Effects: IO, PROC +Contracts: terminal fd, snake bounds (forall invariant), framebuffer size, sine range, snake length invariant + +```ftl +// Snake Game — Full FTL v3 graph +// Based on SIMULATION-snake-game.md +// ~100 Nodes: Terminal, Sound, Game Logic, Renderer, Cleanup + +// ============================================================ +// TYPES +// ============================================================ + +// Primitives +T:a10 = integer { bits: 32, signed: true } +T:a13 = integer { bits: 64, signed: false } +T:a14 = integer { bits: 16, signed: true } +T:a12 = boolean +T:a15 = unit +T:a16 = integer { bits: 8, signed: false } + +// Struct: Position {x, y} +T:a1 = struct { fields: [x: T:a10, y: T:a10] } + +// Array: snake body (max 800 segments) +T:a2 = array { element: T:a1, max_length: 800 } + +// Variant: Direction +T:a11 = variant { cases: [UP: T:a15, DOWN: T:a15, LEFT: T:a15, RIGHT: T:a15] } + +// Struct: GameState {snake, length, dir, food, score, alive} +T:a3 = struct { fields: [snake: T:a2, length: T:a10, dir: T:a11, food: T:a1, score: T:a10, alive: T:a12] } + +// Framebuffer (16384 bytes, corrected from simulation iteration 3) +T:a4 = array { element: T:a16, max_length: 16384 } + +// PCM sound buffer (2048 samples, S16_LE) +T:a5 = array { element: T:a14, max_length: 2048 } + +// ANSI escape sequences +T:a6 = array { element: T:a16, max_length: 32 } + +// Float for sin approximation +T:a17 = integer { bits: 32, signed: true } + +// ============================================================ +// REGIONS +// ============================================================ + +R:b1 = region { lifetime: static } +R:b2 = region { lifetime: scoped, parent: R:b1 } +R:b3 = region { lifetime: scoped, parent: R:b2 } +R:b4 = region { lifetime: scoped, parent: R:b1 } + +// ============================================================ +// CONSTANTS +// ============================================================ + +// File descriptors and syscall params +C:c_stdin = const { value: 0, type: T:a10 } +C:c_stdout = const { value: 1, type: T:a10 } +C:c_zero = const { value: 0, type: T:a10 } +C:c_one = const { value: 1, type: T:a10 } +C:c_neg1 = const { value: -1, type: T:a10 } +C:c_exit0 = const { value: 0, type: T:a10 } +C:c_exit1 = const { value: 1, type: T:a10 } +C:c_true = const { value: 1, type: T:a12 } +C:c_false = const { value: 0, type: T:a12 } + +// Grid dimensions +C:c_width = const { value: 40, type: T:a10 } +C:c_height = const { value: 20, type: T:a10 } +C:c_max_snake = const { value: 800, type: T:a10 } + +// Initial position +C:c_init_x = const { value: 20, type: T:a10 } +C:c_init_y = const { value: 10, type: T:a10 } +C:c_init_pos = const { value: 0, type: T:a1 } + +// Food initial position +C:c_food_x = const { value: 7, type: T:a10 } +C:c_food_y = const { value: 14, type: T:a10 } + +// Sound parameters +C:c_freq_eat = const { value: 880, type: T:a10 } +C:c_freq_die = const { value: 220, type: T:a10 } +C:c_sample_rate = const { value: 44100, type: T:a10 } +C:c_samples_eat = const { value: 276, type: T:a10 } +C:c_samples_die = const { value: 2048, type: T:a10 } + +// Score increment +C:c_score_inc = const { value: 10, type: T:a10 } + +// Typed zero constants for specific element types +C:c_zero_u8 = const { value: 0, type: T:a16 } +C:c_zero_i16 = const { value: 0, type: T:a14 } + +// ioctl constants for terminal raw mode +C:c_tcgets = const { value: 21505, type: T:a13 } +C:c_tcsets = const { value: 21506, type: T:a13 } + +// ALSA device path: /dev/snd/pcmC0D0p +C:c_alsa_path = const_bytes { value: [47,100,101,118,47,115,110,100,47,112,99,109,67,48,68,48,112,0], type: T:a6, region: R:b1 } + +// ANSI: hide cursor, clear screen +C:c_ansi_hide = const_bytes { value: [27,91,63,50,53,108], type: T:a6, region: R:b1 } +C:c_ansi_show = const_bytes { value: [27,91,63,50,53,104], type: T:a6, region: R:b1 } +C:c_ansi_clear = const_bytes { value: [27,91,50,74,27,91,72], type: T:a6, region: R:b1 } + +// Sleep duration (150ms in nanoseconds) +C:c_sleep_ns = const { value: 150000000, type: T:a13 } + +// Framebuffer size +C:c_fb_size = const { value: 16384, type: T:a13 } + +// ============================================================ +// MEMORY NODES — Framebuffer and PCM buffer +// ============================================================ + +M:g1 = alloc { type: T:a4, region: R:b3 } +M:g2 = alloc { type: T:a5, region: R:b4 } +M:g3 = alloc { type: T:a3, region: R:b2 } + +// Game state store/load +M:g4 = store { target: M:g3, index: C:c_zero, value: C:c_init_pos } +M:g5 = load { source: M:g3, index: C:c_zero, type: T:a3 } + +// Framebuffer write (render output) +M:g6 = store { target: M:g1, index: C:c_zero, value: C:c_zero_u8 } + +// Framebuffer read (for syscall_write) +M:g7 = load { source: M:g1, index: C:c_zero, type: T:a16 } + +// PCM buffer write (sound samples) +M:g8 = store { target: M:g2, index: C:c_zero, value: C:c_zero_i16 } + +// PCM buffer read (for pcm_write) +M:g9 = load { source: M:g2, index: C:c_zero, type: T:a14 } + +// ============================================================ +// TERMINAL INIT (E-Nodes with success/failure) +// ============================================================ + +// Save terminal state and set raw mode +E:d_term_save = syscall_ioctl { inputs: [C:c_stdin, C:c_tcgets, M:g3], type: T:a10, effects: [IO], success: K:f_term_raw, failure: K:f_cleanup } +K:f_term_raw = seq { steps: [E:d_term_set] } +E:d_term_set = syscall_ioctl { inputs: [C:c_stdin, C:c_tcsets, M:g3], type: T:a10, effects: [IO], success: K:f_term_ok, failure: K:f_cleanup } + +// Write hide-cursor ANSI sequence +K:f_term_ok = seq { steps: [E:d_hide_cursor] } +E:d_hide_cursor = syscall_write { inputs: [C:c_stdout, C:c_ansi_hide, C:c_one], type: T:a10, effects: [IO], success: K:f_term_done, failure: K:f_cleanup } +K:f_term_done = seq { steps: [E:d_snd_init] } + +// ============================================================ +// SOUND INIT +// ============================================================ + +E:d_snd_init = syscall_open { inputs: [C:c_alsa_path], type: T:a10, effects: [IO], success: K:f_snd_ok, failure: K:f_cleanup } +K:f_snd_ok = seq { steps: [K:f_game_init] } + +// ============================================================ +// GAME INIT — Pure computation +// ============================================================ + +// Initialize game state +C:c_game_init = const { value: 0, type: T:a3 } +K:f_game_init = seq { steps: [M:g4, K:f_game_loop] } + +// ============================================================ +// GAME LOOP — K:loop with game state +// ============================================================ + +// Alive check (loaded from game state) +C:c_alive = load { source: M:g3, index: C:c_zero, type: T:a12 } + +K:f_game_loop = loop { condition: C:c_alive, body: K:f_tick, state: M:g5, state_type: T:a3 } + +// ============================================================ +// TICK — One game loop iteration +// ============================================================ + +K:f_tick = seq { steps: [E:d_read_key, C:c_update, K:f_render_phase, K:f_food_check, E:d_sleep] } + +// --- Input: non-blocking read --- +E:d_read_key = syscall_read { inputs: [C:c_stdin, M:g3, C:c_one], type: T:a10, effects: [IO], success: K:f_key_ok, failure: K:f_key_ok } +K:f_key_ok = seq { steps: [C:c_update] } + +// --- Update: pure game state computation --- +C:c_update = call_pure { target: "update_game", inputs: [M:g5, E:d_read_key], type: T:a3 } + +// --- Collision check --- +C:c_self_collide = call_pure { target: "check_self_collision", inputs: [C:c_update], type: T:a12 } +C:c_wall_collide = call_pure { target: "check_wall_collision", inputs: [C:c_update, C:c_width, C:c_height], type: T:a12 } +C:c_any_collide = or { inputs: [C:c_self_collide, C:c_wall_collide], type: T:a12 } + +// --- Alive check: branch on collision --- +K:f_alive_check = branch { condition: C:c_any_collide, true: K:f_die, false: K:f_continue } + +// --- Food check --- +C:c_head_eq_food = call_pure { target: "head_equals_food", inputs: [C:c_update], type: T:a12 } +K:f_food_check = branch { condition: C:c_head_eq_food, true: K:f_eat, false: K:f_no_eat } + +// ============================================================ +// RENDER PHASE +// ============================================================ + +K:f_render_phase = seq { steps: [C:c_render, M:g6, E:d_write_frame] } + +// Render game state to framebuffer (pure) +C:c_render = call_pure { target: "render_game", inputs: [C:c_update, C:c_width, C:c_height], type: T:a4 } + +// Write framebuffer to stdout +E:d_write_frame = syscall_write { inputs: [C:c_stdout, M:g1, C:c_fb_size], type: T:a10, effects: [IO], success: K:f_frame_done, failure: K:f_cleanup } +K:f_frame_done = seq { steps: [K:f_food_check] } + +// ============================================================ +// EAT — Food consumed: score++, grow snake, play sound +// ============================================================ + +K:f_eat = seq { steps: [C:c_new_score, C:c_grow, K:f_eat_sound] } + +C:c_new_score = add { inputs: [M:g5, C:c_score_inc], type: T:a10 } +C:c_grow = add { inputs: [M:g5, C:c_one], type: T:a10 } + +// Generate eat sound via Bhaskara sine approximation +C:c_angle_eat = mul { inputs: [C:c_freq_eat, C:c_samples_eat], type: T:a10 } +C:c_sin_eat = bhaskara_approx { inputs: [C:c_angle_eat], type: T:a14 } + +// Fill PCM buffer with sine samples +M:g8_eat = store { target: M:g2, index: C:c_zero, value: C:c_sin_eat } + +// Write PCM to ALSA device +K:f_eat_sound = seq { steps: [M:g8_eat, E:d_pcm_eat] } +E:d_pcm_eat = syscall_write { inputs: [E:d_snd_init, M:g2, C:c_samples_eat], type: T:a10, effects: [IO], success: K:f_no_eat, failure: K:f_no_eat } + +// No eat: continue +K:f_no_eat = seq { steps: [E:d_sleep] } + +// ============================================================ +// DIE — Game over: play death sound, set alive=false +// ============================================================ + +K:f_die = seq { steps: [C:c_set_dead, K:f_die_sound] } + +C:c_set_dead = const { value: 0, type: T:a12 } + +// Generate death sound +C:c_angle_die = mul { inputs: [C:c_freq_die, C:c_samples_die], type: T:a10 } +C:c_sin_die = bhaskara_approx { inputs: [C:c_angle_die], type: T:a14 } +M:g8_die = store { target: M:g2, index: C:c_zero, value: C:c_sin_die } + +K:f_die_sound = seq { steps: [M:g8_die, E:d_pcm_die] } +E:d_pcm_die = syscall_write { inputs: [E:d_snd_init, M:g2, C:c_samples_die], type: T:a10, effects: [IO], success: K:f_after_die, failure: K:f_after_die } +K:f_after_die = seq { steps: [K:f_cleanup] } + +// ============================================================ +// CONTINUE — Normal tick end +// ============================================================ + +K:f_continue = seq { steps: [K:f_render_phase] } + +// Sleep (nanosleep syscall) +E:d_sleep = syscall_nanosleep { inputs: [C:c_sleep_ns], type: T:a10, effects: [IO], success: K:f_tick_end, failure: K:f_tick_end } +K:f_tick_end = seq { steps: [K:f_alive_check] } + +// ============================================================ +// CLEANUP — Converging failure/exit path +// All failure paths lead here: term_restore + sound_close + exit +// ============================================================ + +K:f_cleanup = seq { steps: [E:d_snd_close, E:d_restore, E:d_show_cursor, E:d_exit_clean] } + +// Close ALSA device +E:d_snd_close = syscall_close { inputs: [E:d_snd_init], type: T:a10, effects: [IO], success: K:f_restore, failure: K:f_restore } +K:f_restore = seq { steps: [E:d_restore] } + +// Restore terminal settings +E:d_restore = syscall_ioctl { inputs: [C:c_stdin, C:c_tcsets, M:g3], type: T:a10, effects: [IO], success: K:f_show, failure: K:f_show } +K:f_show = seq { steps: [E:d_show_cursor] } + +// Show cursor again +E:d_show_cursor = syscall_write { inputs: [C:c_stdout, C:c_ansi_show, C:c_one], type: T:a10, effects: [IO], success: K:f_exit_seq, failure: K:f_exit_seq } +K:f_exit_seq = seq { steps: [E:d_exit_clean] } + +// Exit +E:d_exit_clean = syscall_exit { inputs: [C:c_exit0], type: T:a15, effects: [PROC] } +E:d_exit_fail = syscall_exit { inputs: [C:c_exit1], type: T:a15, effects: [PROC] } + +// ============================================================ +// CONTRACTS +// ============================================================ + +// Terminal fd is stdin +V:e1 = contract { target: E:d_term_save, pre: C:c_stdin.val == 0 } + +// Snake bounds: all positions within grid +V:e2 = contract { target: K:f_game_loop, invariant: forall i in 0..state.length: state.snake[i].x >= 0 } +V:e3 = contract { target: K:f_game_loop, invariant: forall i in 0..state.length: state.snake[i].x < 40 } +V:e4 = contract { target: K:f_game_loop, invariant: forall i in 0..state.length: state.snake[i].y >= 0 } +V:e5 = contract { target: K:f_game_loop, invariant: forall i in 0..state.length: state.snake[i].y < 20 } + +// Framebuffer size: render output fits buffer +V:e6 = contract { target: C:c_render, post: result.size <= 16384 } + +// Bhaskara sine approximation range +V:e7 = contract { target: C:c_sin_eat, post: result >= -1 AND result <= 1 } +V:e8 = contract { target: C:c_sin_die, post: result >= -1 AND result <= 1 } + +// Snake length invariant +V:e9 = contract { target: K:f_game_loop, invariant: state.length <= 800 } + +// ALSA path is non-null +V:e10 = contract { target: E:d_snd_init, pre: C:c_alsa_path != null } + +// ============================================================ +// MAIN — Entry point +// ============================================================ + +K:f_main = seq { steps: [E:d_term_save] } +entry: K:f_main +``` + +## concurrency + +Producer-consumer pattern with atomic operations and parallel execution. +Demonstrates: K:par with BARRIER sync, atomic_load/atomic_store/atomic_cas, K:loop (spin-wait), memory ordering (ACQUIRE, RELEASE, SEQ_CST), forall contracts with tuple binding. + +Nodes: 10C + 2E + 8K + 3V + 6T + 2R + 4M +Effects: PROC +Contracts: data-race freedom (forall tuple binding), counter bounds, CAS consistency + +```ftl +// Concurrency — K:Par with atomic operations and BARRIER sync +// Two parallel branches accessing shared state via atomic ops + +// === Typen === +T:a1 = integer { bits: 64, signed: false } +T:a2 = integer { bits: 64, signed: true } +T:a3 = integer { bits: 32, signed: true } +T:a4 = unit +T:a5 = boolean +T:a6 = array { element: T:a2, max_length: 1024 } + +// === Regionen === +R:b1 = region { lifetime: static } +R:b2 = region { lifetime: scoped, parent: R:b1 } + +// === Shared Memory === +M:g1 = alloc { type: T:a1, region: R:b2 } +M:g2 = alloc { type: T:a6, region: R:b2 } + +// === Constants === +C:c0 = const { value: 0, type: T:a1 } +C:c1 = const { value: 1, type: T:a1 } +C:c2 = const { value: 2, type: T:a1 } +C:c10 = const { value: 10, type: T:a1 } +C:c42 = const { value: 42, type: T:a2 } +C:c99 = const { value: 99, type: T:a2 } +C:c_true = const { value: 1, type: T:a5 } +C:c_exit0 = const { value: 0, type: T:a3 } +C:c_exit1 = const { value: 1, type: T:a3 } + +// === Initial store: shared counter = 0 === +C:s_init = atomic_store { target: M:g1, value: C:c0, order: SEQ_CST } + +// === Branch 1: Producer — increment counter, write to array === + +// Load current counter +C:s1_load = atomic_load { source: M:g1, order: ACQUIRE, type: T:a1 } + +// Compute new value +C:c_inc1 = add { inputs: [C:s1_load, C:c1], type: T:a1 } + +// Store incremented counter +C:s1_store = atomic_store { target: M:g1, value: C:c_inc1, order: RELEASE } + +// Write data to array at index 0 +M:g3 = store { target: M:g2, index: C:c0, value: C:c42 } + +// Producer sequence +K:f_prod = seq { steps: [C:s1_store, M:g3] } + +// === Branch 2: Consumer — spin until counter > 0, then read === + +// Load counter atomically +C:s2_load = atomic_load { source: M:g1, order: ACQUIRE, type: T:a1 } + +// Check if counter > 0 +C:c_ready = gt { inputs: [C:s2_load, C:c0], type: T:a5 } + +// Read from array at index 0 +M:g4 = load { source: M:g2, index: C:c0, type: T:a2 } + +// CAS: try to set counter from current to 0 (consume token) +C:s2_cas = atomic_cas { target: M:g1, expected: C:s2_load, desired: C:c0, order: SEQ_CST, success: K:f_cas_ok, failure: K:f_cas_retry } + +// CAS success: read the data +K:f_cas_ok = seq { steps: [M:g4] } + +// CAS failure: retry the load +K:f_cas_retry = seq { steps: [C:s2_load] } + +// Consumer: branch on readiness, then CAS +K:f_cons_body = branch { condition: C:c_ready, true: K:f_cas_attempt, false: K:f_cons_spin } +K:f_cas_attempt = seq { steps: [C:s2_cas] } +K:f_cons_spin = seq { steps: [C:s2_load] } + +// Consumer loop: spin until ready +K:f_cons = loop { condition: C:c_ready, body: K:f_cons_body, state: C:s2_load, state_type: T:a1 } + +// === Parallel execution with BARRIER sync === +K:f_par = par { branches: [K:f_prod, K:f_cons], sync: BARRIER, memory_order: ACQUIRE_RELEASE } + +// === Contracts === + +// Data-race freedom: all shared accesses are atomic +V:e1 = contract { target: K:f_par, invariant: forall (b1, b2) in branches: shared_mnodes(b1, b2) == {} OR all_accesses_atomic(b1, b2) } + +// Counter never exceeds 10 +V:e2 = contract { target: K:f_par, invariant: C:s1_load.val <= 10 } + +// CAS expected value is consistent with loaded value +V:e3 = contract { target: C:s2_cas, pre: C:s2_load.val >= 0 } + +// === Cleanup and exit === +E:d_exit0 = syscall_exit { inputs: [C:c_exit0], type: T:a4, effects: [PROC] } +E:d_exit1 = syscall_exit { inputs: [C:c_exit1], type: T:a4, effects: [PROC] } + +// === Main sequence === +K:f_main = seq { steps: [C:s_init, K:f_par, E:d_exit0] } +entry: K:f_main +``` diff --git a/ftl-spec.md b/ftl-spec.md new file mode 100644 index 0000000..8fc54b8 --- /dev/null +++ b/ftl-spec.md @@ -0,0 +1,402 @@ +# FTL (FLUX Text Language) Specification + +Version: v3 +Parser: PEG grammar (pest) +File extension: `.ftl` + +## Program Structure + +An FTL program is a sequence of node definitions and one `entry` declaration. +Nodes are defined in any order. Forward references are allowed. + +``` +* +entry: +``` + +## Node ID Format + +Every node has a typed ID: `:` + +| Prefix | Node Type | Purpose | +|--------|-----------|---------| +| T | Type | Type definitions | +| R | Region | Memory lifetime regions | +| C | Compute | Pure computations | +| E | Effect | Side effects (IO, syscalls, FFI) | +| K | Control | Control flow (seq, branch, loop, par) | +| V | Contract | Verification obligations | +| M | Memory | Memory operations (alloc, load, store) | +| X | Extern | FFI declarations | + +Identifier: `[a-zA-Z0-9_]+` +Examples: `T:a1`, `C:c_hello`, `K:f_main`, `X:ext1` + +## Comments + +``` +// single line comment +``` + +## T-Node (Type Definitions) + +``` +T: = integer { bits: <8|16|32|64|128>, signed: } +T: = float { bits: <32|64> } +T: = boolean +T: = unit +T: = array { element: , max_length: } +T: = array { element: , max_length: , constraint: } +T: = struct { fields: [: , ...] } +T: = struct { fields: [: , ...], layout: } +T: = variant { cases: [: , ...] } +T: = fn { params: [, ...], result: } +T: = fn { params: [, ...], result: , effects: [, ...] } +T: = opaque { size: , align: } +``` + +### Type References + +A `` is either a T-node ID or a builtin type name. + +Builtin types: `u8`, `u16`, `u32`, `u64`, `i8`, `i16`, `i32`, `i64`, `f32`, `f64`, `bool`, `unit` + +### Tag Names (for variants) + +Tag names start with an uppercase letter: `[A-Z][A-Za-z0-9_]*` +Examples: `UP`, `DOWN`, `LEFT`, `RIGHT` + +### Layout (optional, for structs) + +- `OPTIMAL` (default) -- compiler chooses layout +- `PACKED` -- no padding +- `C_ABI` -- C-compatible layout + +## R-Node (Region Definitions) + +``` +R: = region { lifetime: static } +R: = region { lifetime: scoped, parent: R: } +``` + +Regions define memory lifetimes. Scoped regions have a parent region. + +## C-Node (Compute Definitions) + +All C-nodes are pure (no side effects). + +### const +``` +C: = const { value: , type: } +C: = const { value: , type: , region: R: } +``` + +Literal values: integer (`-?[0-9]+`), float (`-?[0-9]+.[0-9]+`), boolean (`true`/`false`), string (`"..."`). + +### const_bytes +``` +C: = const_bytes { value: [, ...], type: , region: R: } +``` + +Byte array literal. Each byte is an integer 0-255. + +### Arithmetic / Logic Operations +``` +C: = { inputs: [, ...], type: } +``` + +Operators: `add`, `sub`, `mul`, `div`, `mod`, `and`, `or`, `xor`, `shl`, `shr`, `neg`, `not`, `eq`, `neq`, `lt`, `lte`, `gt`, `gte` + +### call_pure +``` +C: = call_pure { target: "", inputs: [, ...], type: } +``` + +Calls a pure named function. Target is a string literal. + +### Atomic Operations (Concurrency) + +``` +C: = atomic_load { source: M:, order: , type: } +C: = atomic_store { target: M:, value: , order: } +C: = atomic_cas { target: M:, expected: , desired: , order: , success: , failure: } +``` + +Memory orders: `SEQ_CST`, `ACQUIRE_RELEASE`, `ACQUIRE`, `RELEASE`, `RELAXED` + +### Generic Compute Operation (catch-all) +``` +C: = { : , ... } +``` + +For operations not covered above (e.g., `bhaskara_approx`, `load`). Field values can be: node_ref, node_ref_list, type_ref, literal, effect_list, byte_array, memory_order, tag_name, ident. + +## E-Node (Effect Definitions) + +E-nodes represent side effects. + +### Syscalls + +``` +E: = syscall_exit { inputs: [, ...], type: , effects: [, ...] } +``` + +`syscall_exit` has no success/failure continuations. + +``` +E: = syscall_write { inputs: [, , ], type: , effects: [, ...], success: , failure: } +E: = syscall_read { inputs: [, , ], type: , effects: [, ...], success: , failure: } +E: = syscall_open { inputs: [], type: , effects: [, ...], success: , failure: } +E: = syscall_close { inputs: [], type: , effects: [, ...], success: , failure: } +E: = syscall_ioctl { inputs: [, , ], type: , effects: [, ...], success: , failure: } +``` + +### call_extern (FFI) +``` +E: = call_extern { target: X:, inputs: [, ...], type: , effects: [, ...], success: , failure: } +``` + +### Generic Effect (catch-all) +``` +E: = { : , ... } +``` + +### Effect Names + +Effect names are uppercase identifiers: `[A-Z][A-Za-z0-9_]*` +Common effects: `IO`, `MEM`, `PROC` + +## K-Node (Control Flow) + +### seq +``` +K: = seq { steps: [, ...] } +``` + +Sequential execution of steps. + +### branch +``` +K: = branch { condition: , true: , false: } +``` + +Conditional branch. `condition` must evaluate to boolean. + +### loop +``` +K: = loop { condition: , body: , state: , state_type: } +``` + +Loop with mutable state. Runs `body` while `condition` is true. + +### par (Parallel) +``` +K: = par { branches: [, ...], sync: } +K: = par { branches: [, ...], sync: , memory_order: } +``` + +Parallel execution of branches with synchronization mode. + +## V-Node (Contract Definitions) + +``` +V: = contract { target: , , ... } +``` + +A contract binds to a target node and contains one or more clauses. + +### Clause Types + +``` +pre: +post: +invariant: +assume: +trust: +``` + +Multiple clauses can appear in a single contract, comma-separated: +``` +V: = contract { target: E:d1, trust: EXTERN, assume: result != 0, post: result != 0 } +``` + +## X-Node (Extern / FFI Declarations) + +``` +X: = extern { name: "", abi: , params: [, ...], result: } +X: = extern { name: "", abi: , params: [, ...], result: , effects: [, ...] } +``` + +## M-Node (Memory Operations) + +### alloc +``` +M: = alloc { type: , region: R: } +``` + +### load +``` +M: = load { source: M:, index: , type: } +``` + +### store +``` +M: = store { target: M:, index: , value: } +``` + +## Entry Point + +``` +entry: +``` + +Exactly one entry point per program. Typically references a K-node. + +## Formula Syntax (for V-Node contracts) + +Operator precedence (low to high): `OR` < `AND` < `NOT` < comparison < `+`/`-` < `*`/`/`/`%` < unary + +### Logical Operators +``` + AND + OR +NOT +``` + +Note: use `AND`/`OR`/`NOT` (uppercase), not `&&`/`||`/`!`. + +### Comparison Operators +``` + == + != + < + > + <= + >= +``` + +### Arithmetic Operators (within formulas) +``` + + + - + * + / + % +- +``` + +### Quantifiers +``` +forall in ..: +forall (, ) in : +``` + +### Special Tokens +``` +result // return value of target node +state // loop state variable +null // null pointer +``` + +### Field Access +``` +. +.. +state. +state.[]. +``` + +### Index Access +``` +[] +[]. +``` + +### Function Calls in Formulas +``` +region_valid(R:) +shared_mnodes(, ) +all_accesses_atomic(, ) +``` + +### Empty Set +``` +{} +``` + +### Boolean Literals +``` +true +false +``` + +### Parentheses +``` +() +``` + +## Struct/Array/Variant Operations (C-Node) + +These are parsed as generic compute ops or specific named ops: + +``` +C: = array_length { ... } +C: = struct_get { ... } +C: = struct_set { ... } +C: = variant_tag { ... } +C: = variant_get { ... } +C: = variant_wrap { ... } +``` + +## Complete Example: Hello World + +```ftl +// Types +T:a1 = array { element: u8, max_length: 12 } +T:a2 = integer { bits: 64, signed: false } +T:a3 = unit + +// Regions +R:b1 = region { lifetime: static } + +// Compute-Nodes +C:c1 = const_bytes { value: [72,101,108,108,111,32,87,111,114,108,100,10], type: T:a1, region: R:b1 } +C:c2 = const { value: 1, type: T:a2 } +C:c3 = const { value: 12, type: T:a2 } +C:c4 = const { value: 0, type: T:a2 } +C:c5 = const { value: 1, type: T:a2 } + +// Effect-Nodes +E:d1 = syscall_write { inputs: [C:c2, C:c1, C:c3], type: T:a2, effects: [IO], success: K:f2, failure: K:f3 } + +// Success path: exit(0) +K:f2 = seq { steps: [E:d2] } +E:d2 = syscall_exit { inputs: [C:c4], type: T:a3, effects: [PROC] } + +// Failure path: exit(1) +K:f3 = seq { steps: [E:d3] } +E:d3 = syscall_exit { inputs: [C:c5], type: T:a3, effects: [PROC] } + +// Contracts +V:e1 = contract { target: E:d1, pre: C:c2.val == 1 } +V:e2 = contract { target: E:d1, pre: C:c3.val == 12 } + +// Entry +K:f1 = seq { steps: [E:d1] } +entry: K:f1 +``` + +## Validation Pipeline + +1. Parse (PEG grammar) +2. Structural validation (dangling refs, duplicate IDs) +3. Type and effect checking +4. Region checking (lifetime safety) +5. Contract proving (Z3/BMC) +6. Compilation to content-addressed binary graph + +## Error Codes + +- 1000-1999: Structural validation errors (fatal) +- 2000-2999: Warnings (non-fatal) +- 3000+: Type/effect/region errors (fatal) diff --git a/mcp-integration.md b/mcp-integration.md new file mode 100644 index 0000000..3351a7b --- /dev/null +++ b/mcp-integration.md @@ -0,0 +1,327 @@ +# FLUX MCP Server Integration + +## Configuration + +### Claude Desktop +Add to `claude_desktop_config.json`: +```json +{ + "mcpServers": { + "flux-ftl": { + "command": "/path/to/flux-mcp", + "args": [] + } + } +} +``` + +### Claude Code +Add to `.mcp.json` in project root or `~/.claude/mcp.json`: +```json +{ + "mcpServers": { + "flux-ftl": { + "command": "/path/to/flux-mcp", + "args": [] + } + } +} +``` + +### Generic MCP Client +The server communicates via JSON-RPC 2.0 over stdio (one JSON object per line). + +## Available Tools + +### flux_check + +Validates FTL source code through the full pipeline: parse, structural validation, type/effect checking, region checking, contract proving, compilation. + +**Input:** +```json +{ + "ftl_source": "string (required) -- FTL source code", + "bmc": "boolean (optional) -- enable Bounded Model Checking", + "bmc_depth": "integer (optional, default: 10) -- BMC unrolling depth" +} +``` + +**Output:** +```json +{ + "status": "OK | PARSE_ERROR | VALIDATION_FAIL | PROOF_FAIL", + "parse_errors": [ + { + "line": "integer", + "column": "integer", + "message": "string" + } + ], + "validation_errors": [ + { + "error_code": "integer", + "node_id": "string -- e.g. T:a1", + "violation": "string", + "message": "string", + "suggestion": "string | null" + } + ], + "proof_results": [ + { + "contract_id": "string -- V-node ID", + "target_id": "string -- target node ID", + "clause_index": "integer", + "clause_kind": "pre | post | invariant | assume", + "status": "PROVEN | DISPROVEN | UNKNOWN | ASSUMED | TIMEOUT | BMC_PROVEN | BMC_REFUTED", + "counterexample": "string | null" + } + ], + "feedback": { + "status": "PASS | FIXABLE | FATAL", + "summary": "string", + "issues": [ + { + "severity": "error | warning | info", + "category": "parse_error | structural_validation | type_mismatch | effect_violation | region_error | contract_violation | proof_failure", + "node_id": "string", + "message": "string", + "suggestion": { + "action": "replace | add | remove | modify | restructure", + "target_node": "string | null", + "description": "string", + "example": "string | null" + }, + "context": { + "related_nodes": ["string"], + "expected": "string | null", + "actual": "string | null" + } + } + ], + "iteration_hint": { + "estimated_fixes": "integer", + "priority_order": ["string -- node IDs to fix first"], + "strategy": "string -- suggested repair strategy" + } + } +} +``` + +### flux_compile + +Compiles FTL to content-addressed binary graph (BLAKE3 hashed). + +**Input:** +```json +{ + "ftl_source": "string (required)" +} +``` + +**Output:** +```json +{ + "entry_hash": "string -- BLAKE3 hash of entry node", + "total_nodes": "integer", + "nodes": ["node metadata array"] +} +``` + +### flux_build + +Full pipeline: parse, validate, prove, optimize, codegen (LLVM), link to executable. + +**Input:** +```json +{ + "ftl_source": "string (required)", + "output_path": "string (required) -- path for output binary", + "target": "string (optional, default: host) -- host | x86_64 | aarch64 | riscv64 | wasm32", + "opt_level": "integer (optional, default: 2) -- 0 (none), 1 (less), 2 (default), 3 (aggressive)", + "bmc": "boolean (optional)", + "bmc_depth": "integer (optional, default: 10)" +} +``` + +**Output:** +```json +{ + "executable_path": "string", + "optimization_stats": { + "nodes_before": "integer", + "nodes_after": "integer", + "constants_folded": "integer", + "dead_nodes_removed": "integer", + "identities_removed": "integer" + } +} +``` + +### flux_ir + +Generate LLVM IR from FTL source. + +**Input:** +```json +{ + "ftl_source": "string (required)", + "target": "string (optional, default: host)" +} +``` + +**Output:** +```json +{ + "llvm_ir": "string -- LLVM IR text" +} +``` + +### flux_evolve + +Evolve graph variants using genetic algorithm (mutation, crossover, selection). + +**Input:** +```json +{ + "ftl_source": "string (required)", + "generations": "integer (optional, default: 50)", + "population": "integer (optional, default: 30)", + "mutation_rate": "number (optional, default: 0.3)", + "crossover_rate": "number (optional, default: 0.5)", + "seed": "integer (optional) -- for reproducibility" +} +``` + +**Output:** +```json +{ + "best_program": "object -- best evolved FTL program as JSON AST", + "fitness": "number", + "generations_run": "integer", + "stats": { + "best_fitness": "number", + "avg_fitness": "number", + "proven_count": "integer", + "incubated_count": "integer" + } +} +``` + +### flux_prove + +Formal contract verification only (no compilation). + +**Input:** +```json +{ + "ftl_source": "string (required)", + "bmc": "boolean (optional)", + "bmc_depth": "integer (optional, default: 10)" +} +``` + +**Output:** +```json +{ + "results": [ + { + "contract_id": "string -- V-node ID", + "target_id": "string -- target node ID", + "clause_kind": "pre | post | invariant | assume", + "status": "PROVEN | DISPROVEN | UNKNOWN | ASSUMED | TIMEOUT | BMC_PROVEN | BMC_REFUTED", + "counterexample": "string | null" + } + ] +} +``` + +### flux_generate + +Generate FTL from natural language or structured requirements using an LLM backend. + +**Input:** +```json +{ + "requirement": "string (required) -- natural language or structured requirement", + "requirement_type": "string (optional, default: translate) -- translate | optimize | extend", + "provider": "string (optional, default: anthropic) -- LLM provider", + "model": "string (optional) -- specific model name", + "max_iterations": "integer (optional, default: 5)" +} +``` + +**Output:** +```json +{ + "ftl_source": "string -- generated FTL", + "final_status": "Success | PartialSuccess | Failed", + "iterations": "integer" +} +``` + +## Workflow: Generate, Check, Repair + +``` +1. Generate FTL for a requirement +2. Call flux_check with the FTL source +3. IF status != "OK": + a. Read feedback.issues for error details + b. Read feedback.iteration_hint for repair strategy + c. Fix the FTL based on suggestions + d. GOTO 2 +4. IF status == "OK": + a. Call flux_build to create executable + b. OR call flux_evolve to optimize variants + c. OR call flux_prove for deeper verification with BMC +``` + +## Interpreting Feedback + +### Status Mapping + +| feedback.status | Meaning | Action | +|-----------------|---------|--------| +| PASS | All checks passed | Proceed to build/evolve | +| FIXABLE | Errors found, repair suggestions available | Apply suggestions, re-check | +| FATAL | Structural errors, program cannot be analyzed | Rewrite affected sections | + +### Issue Priority + +Process issues in the order given by `feedback.iteration_hint.priority_order`. +Each entry is a node ID. Fix errors on that node first before moving to the next. + +### Error Code Ranges + +| Range | Category | Severity | +|-------|----------|----------| +| 1000-1999 | Structural validation | Fatal | +| 2000-2999 | Warnings | Non-fatal | +| 3000+ | Type/effect/region | Fatal | + +### Proof Status Interpretation + +| Status | Meaning | +|--------|---------| +| PROVEN | Contract verified correct by Z3 | +| DISPROVEN | Counterexample found -- contract violated | +| UNKNOWN | Solver timeout or undecidable | +| ASSUMED | Marked with `assume:` clause, not verified | +| BMC_PROVEN | Verified up to BMC depth | +| BMC_REFUTED | Counterexample found via BMC | +| TIMEOUT | Solver exceeded time limit | + +## CLI Equivalent Commands + +The MCP tools map to CLI subcommands: + +| MCP Tool | CLI Command | +|----------|-------------| +| flux_check | `flux-ftl check [--bmc] [--bmc-depth N]` | +| flux_compile | `flux-ftl compile [-o output]` | +| flux_build | `flux-ftl build [-o output] [--opt-level N] [--target T]` | +| flux_ir | `flux-ftl ir [--target T]` | +| flux_evolve | `flux-ftl evolve [--generations N] [--population N]` | +| flux_generate | `flux-ftl generate "" [--provider P]` | + +All CLI commands accept `-` for stdin. `flux-ftl check` defaults to stdin when no file is given. +Output is JSON to stdout. From c9165d91dff55b0790b5c3f4e9bfe76b92576a3f Mon Sep 17 00:00:00 2001 From: Marco Doehler Date: Sat, 14 Mar 2026 19:05:01 +0000 Subject: [PATCH 2/4] =?UTF-8?q?Phase=2020:=20MCP=20Server=20=E2=80=94=20FL?= =?UTF-8?q?UX=20als=20Tool=20f=C3=BCr=20LLMs=20via=20JSON-RPC=202.0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implementiert einen MCP-Server (flux-mcp binary) der die FLUX-Pipeline über stdio als JSON-RPC 2.0 Tools exponiert. Extrahiert pipeline.rs als shared module für CLI und MCP. 6 Tools: flux_check, flux_compile, flux_build, flux_ir, flux_evolve, flux_prove 11 MCP-Tests, alle bestehenden 271 Tests bestehen weiterhin. Co-Authored-By: Claude Haiku 4.5 --- flux-ftl/Cargo.toml | 8 + flux-ftl/src/bin/flux-mcp.rs | 663 +++++++++++++++++++++++++++++++++++ flux-ftl/src/lib.rs | 1 + flux-ftl/src/main.rs | 217 +----------- flux-ftl/src/pipeline.rs | 213 +++++++++++ flux-ftl/tests/mcp_tests.rs | 212 +++++++++++ 6 files changed, 1106 insertions(+), 208 deletions(-) create mode 100644 flux-ftl/src/bin/flux-mcp.rs create mode 100644 flux-ftl/src/pipeline.rs create mode 100644 flux-ftl/tests/mcp_tests.rs diff --git a/flux-ftl/Cargo.toml b/flux-ftl/Cargo.toml index 29b7e6d..f99080f 100644 --- a/flux-ftl/Cargo.toml +++ b/flux-ftl/Cargo.toml @@ -17,6 +17,14 @@ rand = "0.8" reqwest = { version = "0.12", features = ["json"] } tokio = { version = "1", features = ["full"] } +[[bin]] +name = "flux-ftl" +path = "src/main.rs" + +[[bin]] +name = "flux-mcp" +path = "src/bin/flux-mcp.rs" + [dev-dependencies] criterion = { version = "0.5", features = ["html_reports"] } assert_cmd = "2" diff --git a/flux-ftl/src/bin/flux-mcp.rs b/flux-ftl/src/bin/flux-mcp.rs new file mode 100644 index 0000000..64e8f96 --- /dev/null +++ b/flux-ftl/src/bin/flux-mcp.rs @@ -0,0 +1,663 @@ +// --------------------------------------------------------------------------- +// flux-mcp — MCP (Model Context Protocol) server for FLUX FTL +// --------------------------------------------------------------------------- +// +// Exposes the FLUX FTL compiler pipeline as tools for LLMs via JSON-RPC 2.0 +// over stdio (stdin/stdout). Implements the MCP protocol without external +// MCP crates — only serde_json and standard I/O. +// +// Tools: +// flux_check — Parse, validate, type-check, region-check, prove contracts +// flux_compile — Compile to content-addressed binary graph +// flux_build — Full pipeline: check + compile + LLVM codegen + link +// flux_ir — Generate LLVM IR from FTL source +// flux_evolve — Evolve graph variants using a genetic algorithm +// flux_prove — Formally prove V-Node contracts using Z3 +// --------------------------------------------------------------------------- + +use std::io::{BufRead, BufReader, Write}; + +use serde::{Deserialize, Serialize}; +use serde_json::Value; + +use flux_ftl::codegen::{self, CodegenConfig, FluxTarget, OptLevel, OutputFormat}; +use flux_ftl::compiler::{self, CompileMetadata}; +use flux_ftl::evolution::{self, EvolutionConfig, GraphPool}; +use flux_ftl::optimizer::{self, OptimizationConfig}; +use flux_ftl::pipeline::{self, FullStatus}; +use flux_ftl::prover::{prove_contracts, BmcConfig, ProverConfig}; + +// --------------------------------------------------------------------------- +// JSON-RPC types +// --------------------------------------------------------------------------- + +#[derive(Deserialize)] +struct JsonRpcRequest { + #[allow(dead_code)] + jsonrpc: String, + id: Option, + method: String, + params: Option, +} + +#[derive(Serialize)] +struct JsonRpcResponse { + jsonrpc: String, + id: Value, + #[serde(skip_serializing_if = "Option::is_none")] + result: Option, + #[serde(skip_serializing_if = "Option::is_none")] + error: Option, +} + +#[derive(Serialize)] +struct JsonRpcError { + code: i64, + message: String, +} + +// --------------------------------------------------------------------------- +// MCP Tool definition +// --------------------------------------------------------------------------- + +#[derive(Serialize)] +struct Tool { + name: String, + description: String, + #[serde(rename = "inputSchema")] + input_schema: Value, +} + +// --------------------------------------------------------------------------- +// Response helpers +// --------------------------------------------------------------------------- + +fn send_response(stdout: &std::io::Stdout, response: &JsonRpcResponse) { + let json = serde_json::to_string(response).expect("failed to serialize response"); + let mut out = stdout.lock(); + let _ = writeln!(out, "{}", json); + let _ = out.flush(); +} + +fn send_result(stdout: &std::io::Stdout, id: Value, result: Value) { + send_response(stdout, &JsonRpcResponse { + jsonrpc: "2.0".to_string(), + id, + result: Some(result), + error: None, + }); +} + +fn send_error(stdout: &std::io::Stdout, id: Value, code: i64, message: &str) { + send_response(stdout, &JsonRpcResponse { + jsonrpc: "2.0".to_string(), + id, + result: None, + error: Some(JsonRpcError { + code, + message: message.to_string(), + }), + }); +} + +fn send_tool_result(stdout: &std::io::Stdout, id: Value, text: &str) { + let content = serde_json::json!({ + "content": [{"type": "text", "text": text}] + }); + send_result(stdout, id, content); +} + +fn send_tool_error(stdout: &std::io::Stdout, id: Value, text: &str) { + let content = serde_json::json!({ + "content": [{"type": "text", "text": text}], + "isError": true + }); + send_result(stdout, id, content); +} + +// --------------------------------------------------------------------------- +// Handler: initialize +// --------------------------------------------------------------------------- + +fn handle_initialize(stdout: &std::io::Stdout, id: Value) { + let result = serde_json::json!({ + "protocolVersion": "2024-11-05", + "capabilities": { + "tools": {} + }, + "serverInfo": { + "name": "flux-ftl", + "version": "1.0.0" + } + }); + send_result(stdout, id, result); +} + +// --------------------------------------------------------------------------- +// Handler: tools/list +// --------------------------------------------------------------------------- + +fn build_tools() -> Vec { + vec![ + Tool { + name: "flux_check".to_string(), + description: "Parse, validate, type-check, region-check, and prove contracts for FTL source code. Returns structured JSON with parse_errors, validation_errors, proof_results, and LLM feedback with repair suggestions.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string", "description": "FTL source code to check" }, + "bmc": { "type": "boolean", "description": "Enable Bounded Model Checking as Z3 fallback", "default": false }, + "bmc_depth": { "type": "integer", "description": "BMC unrolling depth", "default": 10 } + }, + "required": ["ftl_source"] + }), + }, + Tool { + name: "flux_compile".to_string(), + description: "Compile validated FTL to a content-addressed binary graph with BLAKE3 hashes. Returns compilation metadata including entry_hash, total_nodes, and node details.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string", "description": "FTL source code to compile" } + }, + "required": ["ftl_source"] + }), + }, + Tool { + name: "flux_build".to_string(), + description: "Full pipeline: check + compile + LLVM codegen + link to executable binary. Returns the path to the generated executable.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string" }, + "output_path": { "type": "string", "description": "Path for output executable" }, + "target": { "type": "string", "enum": ["host", "x86_64", "aarch64", "riscv64", "wasm32"], "default": "host" }, + "opt_level": { "type": "integer", "enum": [0, 1, 2, 3], "default": 2 } + }, + "required": ["ftl_source", "output_path"] + }), + }, + Tool { + name: "flux_ir".to_string(), + description: "Generate LLVM IR from FTL source. Useful for debugging and inspecting generated code.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string" }, + "target": { "type": "string", "enum": ["host", "x86_64", "aarch64", "riscv64", "wasm32"], "default": "host" } + }, + "required": ["ftl_source"] + }), + }, + Tool { + name: "flux_evolve".to_string(), + description: "Evolve graph variants using a genetic algorithm. Takes a base FTL program and produces optimized variants through mutation, crossover, and selection.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string" }, + "generations": { "type": "integer", "default": 50 }, + "population": { "type": "integer", "default": 30 }, + "mutation_rate": { "type": "number", "default": 0.3 }, + "seed": { "type": "integer", "description": "Random seed for reproducibility" } + }, + "required": ["ftl_source"] + }), + }, + Tool { + name: "flux_prove".to_string(), + description: "Formally prove V-Node contracts using Z3 SMT solver with optional BMC fallback. Returns per-contract proof status (Proven/Disproven/Unknown/BmcProven/Assumed) with counterexamples for disproven contracts.".to_string(), + input_schema: serde_json::json!({ + "type": "object", + "properties": { + "ftl_source": { "type": "string" }, + "bmc": { "type": "boolean", "default": false }, + "bmc_depth": { "type": "integer", "default": 10 } + }, + "required": ["ftl_source"] + }), + }, + ] +} + +fn handle_tools_list(stdout: &std::io::Stdout, id: Value) { + let tools = build_tools(); + let result = serde_json::json!({ "tools": tools }); + send_result(stdout, id, result); +} + +// --------------------------------------------------------------------------- +// Handler: tools/call +// --------------------------------------------------------------------------- + +fn handle_tools_call(stdout: &std::io::Stdout, id: Value, params: Option) { + let params = match params { + Some(p) => p, + None => { + send_error(stdout, id, -32602, "Missing params for tools/call"); + return; + } + }; + + let tool_name = match params.get("name").and_then(|v| v.as_str()) { + Some(n) => n.to_string(), + None => { + send_error(stdout, id, -32602, "Missing 'name' in tools/call params"); + return; + } + }; + + let args = params.get("arguments").cloned().unwrap_or(Value::Object(serde_json::Map::new())); + + match tool_name.as_str() { + "flux_check" => handle_flux_check(stdout, id, &args), + "flux_compile" => handle_flux_compile(stdout, id, &args), + "flux_build" => handle_flux_build(stdout, id, &args), + "flux_ir" => handle_flux_ir(stdout, id, &args), + "flux_evolve" => handle_flux_evolve(stdout, id, &args), + "flux_prove" => handle_flux_prove(stdout, id, &args), + _ => send_tool_error(stdout, id, &format!("Unknown tool: {}", tool_name)), + } +} + +// --------------------------------------------------------------------------- +// Tool: flux_check +// --------------------------------------------------------------------------- + +fn handle_flux_check(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let bmc = args.get("bmc").and_then(|v| v.as_bool()).unwrap_or(false); + let bmc_depth = args.get("bmc_depth").and_then(|v| v.as_u64()).unwrap_or(10) as u32; + + let bmc_config = if bmc { + Some(BmcConfig { + max_depth: bmc_depth, + ..BmcConfig::default() + }) + } else { + None + }; + + let result = pipeline::run_check_with_bmc(ftl_source, bmc_config); + let json = match pipeline::result_to_json(&result) { + Ok(j) => j, + Err(e) => { + send_tool_error(stdout, id, &format!("Serialization error: {}", e)); + return; + } + }; + + send_tool_result(stdout, id, &json); +} + +// --------------------------------------------------------------------------- +// Tool: flux_compile +// --------------------------------------------------------------------------- + +fn handle_flux_compile(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let result = pipeline::run_check(ftl_source); + if result.status != FullStatus::Ok { + let json = pipeline::result_to_json(&result).unwrap_or_else(|e| e); + send_tool_error(stdout, id, &format!("Check failed:\n{}", json)); + return; + } + + let ast = match &result.ast { + Some(a) => a, + None => { + send_tool_error(stdout, id, "No AST available after check"); + return; + } + }; + + match compiler::compile(ast) { + Ok(graph) => { + let metadata = CompileMetadata::from(&graph); + let json = serde_json::to_string(&metadata) + .unwrap_or_else(|e| format!("{{\"error\": \"{}\"}}", e)); + send_tool_result(stdout, id, &json); + } + Err(e) => { + send_tool_error(stdout, id, &format!("Compilation error: {}", e)); + } + } +} + +// --------------------------------------------------------------------------- +// Tool: flux_build +// --------------------------------------------------------------------------- + +fn handle_flux_build(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let output_path = match args.get("output_path").and_then(|v| v.as_str()) { + Some(s) => s.to_string(), + None => { + send_tool_error(stdout, id, "Missing required argument: output_path"); + return; + } + }; + + let target_str = args.get("target").and_then(|v| v.as_str()).unwrap_or("host"); + let opt_level_num = args.get("opt_level").and_then(|v| v.as_u64()).unwrap_or(2) as u8; + + let flux_target = match FluxTarget::parse(target_str) { + Ok(t) => t, + Err(e) => { + send_tool_error(stdout, id, &format!("Invalid target: {}", e)); + return; + } + }; + + let result = pipeline::run_check(ftl_source); + if result.status != FullStatus::Ok { + let json = pipeline::result_to_json(&result).unwrap_or_else(|e| e); + send_tool_error(stdout, id, &format!("Check failed:\n{}", json)); + return; + } + + let ast = match &result.ast { + Some(a) => a, + None => { + send_tool_error(stdout, id, "No AST available after check"); + return; + } + }; + + // Apply graph-level optimizations before codegen + let opt_config = OptimizationConfig { + llvm_opt_level: opt_level_num, + enable_graph_opts: opt_level_num > 0, + strip_dead_nodes: opt_level_num > 0, + fold_constants: opt_level_num > 0, + }; + let opt_result = optimizer::optimize_graph(ast, &opt_config); + let optimized_ast = &opt_result.optimized_program; + + let opt = match opt_level_num { + 0 => OptLevel::None, + 1 => OptLevel::Less, + 3 => OptLevel::Aggressive, + _ => OptLevel::Default, + }; + + let config = CodegenConfig { + opt_level: opt, + output_format: OutputFormat::ObjectFile, + target_triple: flux_target.resolved_triple(), + target: flux_target, + }; + + let cg_result = match codegen::codegen(optimized_ast, &config) { + Ok(r) => r, + Err(e) => { + send_tool_error(stdout, id, &format!("Codegen error: {}", e)); + return; + } + }; + + // Write object file to a temp path + let tmp_dir = std::env::temp_dir(); + let obj_path = tmp_dir.join("flux_mcp_build.o"); + if let Err(e) = std::fs::write(&obj_path, &cg_result.output_bytes) { + send_tool_error(stdout, id, &format!("Failed to write object file: {}", e)); + return; + } + + // Link with cc + let link_status = std::process::Command::new("cc") + .arg(&obj_path) + .arg("-o") + .arg(&output_path) + .arg("-lc") + .status(); + + // Clean up temp file + let _ = std::fs::remove_file(&obj_path); + + match link_status { + Ok(s) if s.success() => { + let result_json = serde_json::json!({ + "status": "OK", + "output_path": output_path, + "opt_level": opt_level_num, + "target": target_str, + }); + send_tool_result(stdout, id, &result_json.to_string()); + } + Ok(s) => { + send_tool_error(stdout, id, &format!( + "Linker failed with exit code {}", + s.code().unwrap_or(-1) + )); + } + Err(e) => { + send_tool_error(stdout, id, &format!("Failed to run linker (cc): {}", e)); + } + } +} + +// --------------------------------------------------------------------------- +// Tool: flux_ir +// --------------------------------------------------------------------------- + +fn handle_flux_ir(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let target_str = args.get("target").and_then(|v| v.as_str()).unwrap_or("host"); + + let flux_target = match FluxTarget::parse(target_str) { + Ok(t) => t, + Err(e) => { + send_tool_error(stdout, id, &format!("Invalid target: {}", e)); + return; + } + }; + + let result = pipeline::run_check(ftl_source); + if result.status != FullStatus::Ok { + let json = pipeline::result_to_json(&result).unwrap_or_else(|e| e); + send_tool_error(stdout, id, &format!("Check failed:\n{}", json)); + return; + } + + let ast = match &result.ast { + Some(a) => a, + None => { + send_tool_error(stdout, id, "No AST available after check"); + return; + } + }; + + let config = CodegenConfig { + output_format: OutputFormat::LlvmIr, + target_triple: flux_target.resolved_triple(), + target: flux_target, + ..CodegenConfig::default() + }; + + match codegen::codegen(ast, &config) { + Ok(cg_result) => { + send_tool_result(stdout, id, &cg_result.llvm_ir); + } + Err(e) => { + send_tool_error(stdout, id, &format!("Codegen error: {}", e)); + } + } +} + +// --------------------------------------------------------------------------- +// Tool: flux_evolve +// --------------------------------------------------------------------------- + +fn handle_flux_evolve(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let generations = args.get("generations").and_then(|v| v.as_u64()).unwrap_or(50) as u32; + let population = args.get("population").and_then(|v| v.as_u64()).unwrap_or(30) as usize; + let mutation_rate = args.get("mutation_rate").and_then(|v| v.as_f64()).unwrap_or(0.3); + let seed = args.get("seed").and_then(|v| v.as_u64()); + + let result = pipeline::run_check(ftl_source); + let ast = match &result.ast { + Some(a) => a, + None => { + let json = pipeline::result_to_json(&result).unwrap_or_else(|e| e); + send_tool_error(stdout, id, &format!("Check failed:\n{}", json)); + return; + } + }; + + let config = EvolutionConfig { + population_size: population, + mutation_rate, + max_generations: generations, + seed, + ..Default::default() + }; + + let mut pool = GraphPool::new(config); + pool.seed_population(ast, population); + let evo_result = pool.run(generations); + + let result_json = serde_json::json!({ + "generations_run": evo_result.generations_run, + "best_fitness": evo_result.population_stats.best_fitness, + "avg_fitness": evo_result.population_stats.avg_fitness, + "proven_count": evo_result.population_stats.proven_count, + "incubated_count": evo_result.population_stats.incubated_count, + "best_node_count": evolution::count_nodes(&evo_result.best.program), + "best_depth": evolution::calculate_depth(&evo_result.best.program), + "best_program": evo_result.best.program, + }); + + send_tool_result(stdout, id, &result_json.to_string()); +} + +// --------------------------------------------------------------------------- +// Tool: flux_prove +// --------------------------------------------------------------------------- + +fn handle_flux_prove(stdout: &std::io::Stdout, id: Value, args: &Value) { + let ftl_source = match args.get("ftl_source").and_then(|v| v.as_str()) { + Some(s) => s, + None => { + send_tool_error(stdout, id, "Missing required argument: ftl_source"); + return; + } + }; + + let bmc = args.get("bmc").and_then(|v| v.as_bool()).unwrap_or(false); + let bmc_depth = args.get("bmc_depth").and_then(|v| v.as_u64()).unwrap_or(10) as u32; + + // Parse and validate first + let check_result = pipeline::run_check(ftl_source); + let ast = match &check_result.ast { + Some(a) => a, + None => { + let json = pipeline::result_to_json(&check_result).unwrap_or_else(|e| e); + send_tool_error(stdout, id, &format!("Check failed:\n{}", json)); + return; + } + }; + + let bmc_config = if bmc { + Some(BmcConfig { + max_depth: bmc_depth, + ..BmcConfig::default() + }) + } else { + None + }; + + let prover_config = ProverConfig { + bmc_config, + ..ProverConfig::default() + }; + + let proof_results = prove_contracts(ast, &prover_config); + let json = serde_json::to_string(&proof_results) + .unwrap_or_else(|e| format!("{{\"error\": \"{}\"}}", e)); + + send_tool_result(stdout, id, &json); +} + +// --------------------------------------------------------------------------- +// Main loop +// --------------------------------------------------------------------------- + +fn main() { + let stdin = BufReader::new(std::io::stdin()); + let stdout = std::io::stdout(); + + for line in stdin.lines() { + let line = match line { + Ok(l) => l, + Err(_) => break, + }; + + if line.trim().is_empty() { + continue; + } + + let request: JsonRpcRequest = match serde_json::from_str(&line) { + Ok(r) => r, + Err(e) => { + send_error(&stdout, Value::Null, -32700, &format!("Parse error: {}", e)); + continue; + } + }; + + // Notifications (no id) don't get responses + if request.id.is_none() { + continue; + } + + let id = request.id.unwrap(); + + match request.method.as_str() { + "initialize" => handle_initialize(&stdout, id), + "tools/list" => handle_tools_list(&stdout, id), + "tools/call" => handle_tools_call(&stdout, id, request.params), + _ => send_error( + &stdout, + id, + -32601, + &format!("Method not found: {}", request.method), + ), + } + } +} diff --git a/flux-ftl/src/lib.rs b/flux-ftl/src/lib.rs index 3b768ac..e51bf30 100644 --- a/flux-ftl/src/lib.rs +++ b/flux-ftl/src/lib.rs @@ -7,6 +7,7 @@ pub mod feedback; pub mod llm; pub mod optimizer; pub mod parser; +pub mod pipeline; pub mod prover; pub mod region_checker; pub mod type_checker; diff --git a/flux-ftl/src/main.rs b/flux-ftl/src/main.rs index b0445c8..0eeb00a 100644 --- a/flux-ftl/src/main.rs +++ b/flux-ftl/src/main.rs @@ -1,20 +1,13 @@ use std::io::Read; use std::process::ExitCode; -use serde::Serialize; - use flux_ftl::codegen::{self, CodegenConfig, FluxTarget, OptLevel, OutputFormat}; -use flux_ftl::compiler::{self, CompileMetadata}; -use flux_ftl::error::Status; +use flux_ftl::compiler; use flux_ftl::evolution::{self, EvolutionConfig, GraphPool}; -use flux_ftl::feedback::{self, LlmFeedback, ValidationError as FeedbackValidationError}; use flux_ftl::llm::{GenerateRequest, GenerationLoop, LlmConfig, LlmProvider, RequirementType}; use flux_ftl::optimizer::{self, OptimizationConfig}; -use flux_ftl::parser::parse_ftl; -use flux_ftl::prover::{prove_contracts, BmcConfig, ProofResult, ProofStatus, ProverConfig}; -use flux_ftl::region_checker::check_regions; -use flux_ftl::type_checker::check_types_and_effects; -use flux_ftl::validator::validate; +use flux_ftl::pipeline::{self, FullResult, FullStatus}; +use flux_ftl::prover::BmcConfig; // --------------------------------------------------------------------------- // CLI definition @@ -88,48 +81,6 @@ enum Commands { }, } -// --------------------------------------------------------------------------- -// Shared result types -// --------------------------------------------------------------------------- - -#[derive(Debug, Serialize)] -struct FullResult { - status: FullStatus, - #[serde(skip_serializing_if = "Option::is_none")] - ast: Option, - #[serde(skip_serializing_if = "Vec::is_empty")] - parse_errors: Vec, - #[serde(skip_serializing_if = "Vec::is_empty")] - validation_errors: Vec, - #[serde(skip_serializing_if = "Vec::is_empty")] - proof_results: Vec, - #[serde(skip_serializing_if = "Option::is_none")] - compiled: Option, - #[serde(skip_serializing_if = "Option::is_none")] - compile_error: Option, - #[serde(skip_serializing_if = "Option::is_none")] - feedback: Option, -} - -#[derive(Debug, Serialize, PartialEq, Eq)] -#[serde(rename_all = "SCREAMING_SNAKE_CASE")] -enum FullStatus { - Ok, - ParseError, - ValidationFail, - ProofFail, -} - -#[derive(Debug, Serialize)] -struct GenericError { - error_code: u32, - node_id: String, - violation: String, - message: String, - #[serde(skip_serializing_if = "Option::is_none")] - suggestion: Option, -} - // --------------------------------------------------------------------------- // Input helper // --------------------------------------------------------------------------- @@ -146,162 +97,12 @@ fn read_input(file: &str) -> Result { } } -// --------------------------------------------------------------------------- -// Check pipeline — shared across all subcommands -// --------------------------------------------------------------------------- - -fn run_check(input: &str) -> FullResult { - run_check_with_bmc(input, None) -} - -fn run_check_with_bmc(input: &str, bmc_config: Option) -> FullResult { - let parse_result = parse_ftl(input); - - let ast = match parse_result.status { - Status::Ok => match parse_result.ast { - Some(ast) => ast, - None => { - return FullResult { - status: FullStatus::ParseError, - ast: None, - parse_errors: parse_result.errors, - validation_errors: Vec::new(), - proof_results: Vec::new(), - compiled: None, - compile_error: None, - feedback: None, - }; - } - }, - Status::Error => { - let fb = feedback::generate_feedback(&parse_result.errors, &[], &[]); - return FullResult { - status: FullStatus::ParseError, - ast: None, - parse_errors: parse_result.errors, - validation_errors: Vec::new(), - proof_results: Vec::new(), - compiled: None, - compile_error: None, - feedback: Some(fb), - }; - } - }; - - let mut validation_errors = Vec::new(); - - // Phase 1: Structural validation - let vr = validate(&ast); - for e in &vr.errors { - validation_errors.push(GenericError { - error_code: e.error_code, - node_id: e.node_id.clone(), - violation: e.violation.clone(), - message: e.message.clone(), - suggestion: e.suggestion.clone(), - }); - } - for w in &vr.warnings { - validation_errors.push(GenericError { - error_code: w.error_code, - node_id: w.node_id.clone(), - violation: w.violation.clone(), - message: w.message.clone(), - suggestion: w.suggestion.clone(), - }); - } - - // Phase 2: Type and effect checks - for e in check_types_and_effects(&ast) { - validation_errors.push(GenericError { - error_code: e.error_code, - node_id: e.node_id, - violation: e.violation, - message: e.message, - suggestion: e.suggestion, - }); - } - - // Phase 3: Region checks - for e in check_regions(&ast) { - validation_errors.push(GenericError { - error_code: e.error_code, - node_id: e.node_id, - violation: e.violation, - message: e.message, - suggestion: e.suggestion, - }); - } - - let has_fatal = validation_errors - .iter() - .any(|e| e.error_code < 2000 || e.error_code >= 3000); - - // Phase 4: Contract proving (only if no fatal validation errors) - let proof_results = if !has_fatal { - let config = ProverConfig { - bmc_config, - ..ProverConfig::default() - }; - prove_contracts(&ast, &config) - } else { - Vec::new() - }; - - let has_disproven = proof_results - .iter() - .any(|r| r.status == ProofStatus::Disproven); - - let status = if has_fatal { - FullStatus::ValidationFail - } else if has_disproven { - FullStatus::ProofFail - } else { - FullStatus::Ok - }; - - // Phase 5: Compilation (run unless fatal validation errors) - let (compiled, compile_error) = if !has_fatal { - match compiler::compile(&ast) { - Ok(graph) => (Some(CompileMetadata::from(&graph)), None), - Err(e) => (None, Some(format!("{}", e))), - } - } else { - (None, None) - }; - - // Phase 7: Generate LLM feedback - let feedback_validation_errors: Vec = validation_errors - .iter() - .map(|ge| FeedbackValidationError { - error_code: ge.error_code, - node_id: ge.node_id.clone(), - violation: ge.violation.clone(), - message: ge.message.clone(), - suggestion: ge.suggestion.clone(), - }) - .collect(); - - let fb = feedback::generate_feedback(&[], &feedback_validation_errors, &proof_results); - - FullResult { - status, - ast: Some(ast), - parse_errors: Vec::new(), - validation_errors, - proof_results, - compiled, - compile_error, - feedback: Some(fb), - } -} - // --------------------------------------------------------------------------- // Output formatting // --------------------------------------------------------------------------- fn print_json(result: &FullResult) -> Result<(), String> { - let json = serde_json::to_string(result).map_err(|e| format!("JSON serialization: {}", e))?; + let json = pipeline::result_to_json(result)?; println!("{}", json); Ok(()) } @@ -328,7 +129,7 @@ fn cmd_check(file: &str, bmc: bool, bmc_depth: u32) -> ExitCode { None }; - let result = run_check_with_bmc(&input, bmc_config); + let result = pipeline::run_check_with_bmc(&input, bmc_config); let exit = match result.status { FullStatus::Ok => ExitCode::SUCCESS, FullStatus::ValidationFail | FullStatus::ProofFail => ExitCode::from(1), @@ -352,7 +153,7 @@ fn cmd_compile(file: &str, output: Option<&str>) -> ExitCode { } }; - let result = run_check(&input); + let result = pipeline::run_check(&input); if result.status != FullStatus::Ok { if let Err(e) = print_json(&result) { eprintln!("error: {}", e); @@ -422,7 +223,7 @@ fn cmd_build(file: &str, output: Option<&str>, opt_level: u8, target_str: &str, None }; - let result = run_check_with_bmc(&input, bmc_config); + let result = pipeline::run_check_with_bmc(&input, bmc_config); if result.status != FullStatus::Ok { if let Err(e) = print_json(&result) { eprintln!("error: {}", e); @@ -546,7 +347,7 @@ fn cmd_ir(file: &str, target_str: &str) -> ExitCode { } }; - let result = run_check(&input); + let result = pipeline::run_check(&input); if result.status != FullStatus::Ok { if let Err(e) = print_json(&result) { eprintln!("error: {}", e); @@ -703,7 +504,7 @@ fn cmd_evolve( } }; - let result = run_check(&input); + let result = pipeline::run_check(&input); let ast = match &result.ast { Some(a) => a, None => { diff --git a/flux-ftl/src/pipeline.rs b/flux-ftl/src/pipeline.rs new file mode 100644 index 0000000..ee36027 --- /dev/null +++ b/flux-ftl/src/pipeline.rs @@ -0,0 +1,213 @@ +// --------------------------------------------------------------------------- +// pipeline.rs — Shared check/compile pipeline used by CLI and MCP server +// --------------------------------------------------------------------------- + +use serde::Serialize; + +use crate::compiler::{self, CompileMetadata}; +use crate::error::Status; +use crate::feedback::{self, LlmFeedback, ValidationError as FeedbackValidationError}; +use crate::parser::parse_ftl; +use crate::prover::{prove_contracts, BmcConfig, ProofResult, ProofStatus, ProverConfig}; +use crate::region_checker::check_regions; +use crate::type_checker::check_types_and_effects; +use crate::validator::validate; + +// --------------------------------------------------------------------------- +// Public result types +// --------------------------------------------------------------------------- + +#[derive(Debug, Serialize)] +pub struct FullResult { + pub status: FullStatus, + #[serde(skip_serializing_if = "Option::is_none")] + pub ast: Option, + #[serde(skip_serializing_if = "Vec::is_empty")] + pub parse_errors: Vec, + #[serde(skip_serializing_if = "Vec::is_empty")] + pub validation_errors: Vec, + #[serde(skip_serializing_if = "Vec::is_empty")] + pub proof_results: Vec, + #[serde(skip_serializing_if = "Option::is_none")] + pub compiled: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub compile_error: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub feedback: Option, +} + +#[derive(Debug, Serialize, PartialEq, Eq)] +#[serde(rename_all = "SCREAMING_SNAKE_CASE")] +pub enum FullStatus { + Ok, + ParseError, + ValidationFail, + ProofFail, +} + +#[derive(Debug, Serialize)] +pub struct GenericError { + pub error_code: u32, + pub node_id: String, + pub violation: String, + pub message: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub suggestion: Option, +} + +// --------------------------------------------------------------------------- +// Pipeline functions +// --------------------------------------------------------------------------- + +/// Run the full check pipeline without BMC. +pub fn run_check(input: &str) -> FullResult { + run_check_with_bmc(input, None) +} + +/// Run the full check pipeline with optional BMC configuration. +pub fn run_check_with_bmc(input: &str, bmc_config: Option) -> FullResult { + let parse_result = parse_ftl(input); + + let ast = match parse_result.status { + Status::Ok => match parse_result.ast { + Some(ast) => ast, + None => { + return FullResult { + status: FullStatus::ParseError, + ast: None, + parse_errors: parse_result.errors, + validation_errors: Vec::new(), + proof_results: Vec::new(), + compiled: None, + compile_error: None, + feedback: None, + }; + } + }, + Status::Error => { + let fb = feedback::generate_feedback(&parse_result.errors, &[], &[]); + return FullResult { + status: FullStatus::ParseError, + ast: None, + parse_errors: parse_result.errors, + validation_errors: Vec::new(), + proof_results: Vec::new(), + compiled: None, + compile_error: None, + feedback: Some(fb), + }; + } + }; + + let mut validation_errors = Vec::new(); + + // Phase 1: Structural validation + let vr = validate(&ast); + for e in &vr.errors { + validation_errors.push(GenericError { + error_code: e.error_code, + node_id: e.node_id.clone(), + violation: e.violation.clone(), + message: e.message.clone(), + suggestion: e.suggestion.clone(), + }); + } + for w in &vr.warnings { + validation_errors.push(GenericError { + error_code: w.error_code, + node_id: w.node_id.clone(), + violation: w.violation.clone(), + message: w.message.clone(), + suggestion: w.suggestion.clone(), + }); + } + + // Phase 2: Type and effect checks + for e in check_types_and_effects(&ast) { + validation_errors.push(GenericError { + error_code: e.error_code, + node_id: e.node_id, + violation: e.violation, + message: e.message, + suggestion: e.suggestion, + }); + } + + // Phase 3: Region checks + for e in check_regions(&ast) { + validation_errors.push(GenericError { + error_code: e.error_code, + node_id: e.node_id, + violation: e.violation, + message: e.message, + suggestion: e.suggestion, + }); + } + + let has_fatal = validation_errors + .iter() + .any(|e| e.error_code < 2000 || e.error_code >= 3000); + + // Phase 4: Contract proving (only if no fatal validation errors) + let proof_results = if !has_fatal { + let config = ProverConfig { + bmc_config, + ..ProverConfig::default() + }; + prove_contracts(&ast, &config) + } else { + Vec::new() + }; + + let has_disproven = proof_results + .iter() + .any(|r| r.status == ProofStatus::Disproven); + + let status = if has_fatal { + FullStatus::ValidationFail + } else if has_disproven { + FullStatus::ProofFail + } else { + FullStatus::Ok + }; + + // Phase 5: Compilation (run unless fatal validation errors) + let (compiled, compile_error) = if !has_fatal { + match compiler::compile(&ast) { + Ok(graph) => (Some(CompileMetadata::from(&graph)), None), + Err(e) => (None, Some(format!("{}", e))), + } + } else { + (None, None) + }; + + // Phase 7: Generate LLM feedback + let feedback_validation_errors: Vec = validation_errors + .iter() + .map(|ge| FeedbackValidationError { + error_code: ge.error_code, + node_id: ge.node_id.clone(), + violation: ge.violation.clone(), + message: ge.message.clone(), + suggestion: ge.suggestion.clone(), + }) + .collect(); + + let fb = feedback::generate_feedback(&[], &feedback_validation_errors, &proof_results); + + FullResult { + status, + ast: Some(ast), + parse_errors: Vec::new(), + validation_errors, + proof_results, + compiled, + compile_error, + feedback: Some(fb), + } +} + +/// Serialize a FullResult to JSON string. +pub fn result_to_json(result: &FullResult) -> Result { + serde_json::to_string(result).map_err(|e| format!("JSON serialization: {}", e)) +} diff --git a/flux-ftl/tests/mcp_tests.rs b/flux-ftl/tests/mcp_tests.rs new file mode 100644 index 0000000..7bbe671 --- /dev/null +++ b/flux-ftl/tests/mcp_tests.rs @@ -0,0 +1,212 @@ +use std::io::Write; +use std::process::{Command, Stdio}; + +fn mcp_cmd() -> Command { + Command::new(env!("CARGO_BIN_EXE_flux-mcp")) +} + +fn send_request(input: &str) -> (String, String) { + let mut child = mcp_cmd() + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .expect("failed to spawn flux-mcp"); + + { + let stdin = child.stdin.as_mut().expect("failed to open stdin"); + stdin.write_all(input.as_bytes()).expect("failed to write"); + } + + let output = child.wait_with_output().expect("failed to wait"); + let stdout = String::from_utf8_lossy(&output.stdout).to_string(); + let stderr = String::from_utf8_lossy(&output.stderr).to_string(); + (stdout, stderr) +} + +fn send_jsonrpc(method: &str, params: Option) -> serde_json::Value { + let request = if let Some(p) = params { + serde_json::json!({"jsonrpc": "2.0", "id": 1, "method": method, "params": p}) + } else { + serde_json::json!({"jsonrpc": "2.0", "id": 1, "method": method}) + }; + + let input = format!("{}\n", request); + let (stdout, _) = send_request(&input); + + let first_line = stdout.lines().next().expect("no output from MCP server"); + serde_json::from_str(first_line).expect("invalid JSON response") +} + +#[test] +fn mcp_initialize() { + let resp = send_jsonrpc("initialize", None); + + assert_eq!(resp["jsonrpc"], "2.0"); + assert_eq!(resp["id"], 1); + assert!(resp["error"].is_null()); + + let result = &resp["result"]; + assert_eq!(result["protocolVersion"], "2024-11-05"); + assert_eq!(result["serverInfo"]["name"], "flux-ftl"); + assert_eq!(result["serverInfo"]["version"], "1.0.0"); + assert!(result["capabilities"]["tools"].is_object()); +} + +#[test] +fn mcp_tools_list() { + let resp = send_jsonrpc("tools/list", None); + + let tools = resp["result"]["tools"].as_array().expect("tools should be array"); + assert_eq!(tools.len(), 6); + + let names: Vec<&str> = tools.iter().map(|t| t["name"].as_str().unwrap()).collect(); + assert!(names.contains(&"flux_check")); + assert!(names.contains(&"flux_compile")); + assert!(names.contains(&"flux_build")); + assert!(names.contains(&"flux_ir")); + assert!(names.contains(&"flux_evolve")); + assert!(names.contains(&"flux_prove")); + + for tool in tools { + assert!(tool["description"].is_string()); + assert!(tool["inputSchema"].is_object()); + assert_eq!(tool["inputSchema"]["type"], "object"); + let required = tool["inputSchema"]["required"].as_array().unwrap(); + assert!(required.iter().any(|r| r == "ftl_source")); + } +} + +#[test] +fn mcp_flux_check_valid() { + let ftl = std::fs::read_to_string("testdata/hello_world.ftl").expect("read testdata"); + + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_check", + "arguments": { "ftl_source": ftl } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + assert!(content.is_array()); + let text = content[0]["text"].as_str().expect("text content"); + let check_result: serde_json::Value = serde_json::from_str(text).expect("valid JSON in text"); + assert_eq!(check_result["status"], "OK"); +} + +#[test] +fn mcp_flux_check_invalid() { + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_check", + "arguments": { "ftl_source": "this is not valid FTL" } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + let text = content[0]["text"].as_str().expect("text content"); + let check_result: serde_json::Value = serde_json::from_str(text).expect("valid JSON in text"); + assert_eq!(check_result["status"], "PARSE_ERROR"); +} + +#[test] +fn mcp_flux_compile_valid() { + let ftl = std::fs::read_to_string("testdata/hello_world.ftl").expect("read testdata"); + + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_compile", + "arguments": { "ftl_source": ftl } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + let text = content[0]["text"].as_str().expect("text content"); + let compile_result: serde_json::Value = serde_json::from_str(text).expect("valid JSON"); + assert!(compile_result["entry_hash"].is_string()); + assert!(compile_result["total_nodes"].is_number()); +} + +#[test] +fn mcp_flux_prove_valid() { + let ftl = std::fs::read_to_string("testdata/hello_world.ftl").expect("read testdata"); + + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_prove", + "arguments": { "ftl_source": ftl } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + let text = content[0]["text"].as_str().expect("text content"); + let proof_results: serde_json::Value = serde_json::from_str(text).expect("valid JSON"); + assert!(proof_results.is_array()); + + let results = proof_results.as_array().unwrap(); + assert!(!results.is_empty()); + for r in results { + assert!(r["contract_id"].is_string()); + assert!(r["status"].is_string()); + } +} + +#[test] +fn mcp_flux_ir_valid() { + let ftl = std::fs::read_to_string("testdata/hello_world.ftl").expect("read testdata"); + + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_ir", + "arguments": { "ftl_source": ftl } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + let text = content[0]["text"].as_str().expect("text content"); + assert!(text.contains("define"), "IR should contain 'define'"); +} + +#[test] +fn mcp_unknown_tool() { + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "nonexistent_tool", + "arguments": {} + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + assert_eq!(content[0]["type"], "text"); + assert!(resp["result"]["isError"].as_bool().unwrap_or(false)); +} + +#[test] +fn mcp_unknown_method() { + let resp = send_jsonrpc("bogus/method", None); + + assert!(resp["error"].is_object()); + assert_eq!(resp["error"]["code"], -32601); +} + +#[test] +fn mcp_missing_ftl_source() { + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_check", + "arguments": {} + }))); + + assert!(resp["error"].is_null()); + assert!(resp["result"]["isError"].as_bool().unwrap_or(false)); +} + +#[test] +fn mcp_multiple_requests() { + let req1 = serde_json::json!({"jsonrpc": "2.0", "id": 1, "method": "initialize"}); + let req2 = serde_json::json!({"jsonrpc": "2.0", "id": 2, "method": "tools/list"}); + let input = format!("{}\n{}\n", req1, req2); + + let (stdout, _) = send_request(&input); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines.len(), 2, "should get 2 responses for 2 requests"); + + let resp1: serde_json::Value = serde_json::from_str(lines[0]).unwrap(); + let resp2: serde_json::Value = serde_json::from_str(lines[1]).unwrap(); + assert_eq!(resp1["id"], 1); + assert_eq!(resp2["id"], 2); +} From eb6c61a25e603e5fbd76f7172545c765037a7fac Mon Sep 17 00:00:00 2001 From: Marco Doehler Date: Sat, 14 Mar 2026 19:05:24 +0000 Subject: [PATCH 3/4] Add MCP tests for invalid JSON, notifications, and flux_evolve Extends the MCP test suite with 3 additional integration tests: - mcp_invalid_json: verifies -32700 parse error response - mcp_notification_no_response: verifies notifications are silent - mcp_flux_evolve_valid: validates evolution tool with seed Co-Authored-By: Claude Haiku 4.5 --- flux-ftl/tests/mcp_tests.rs | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/flux-ftl/tests/mcp_tests.rs b/flux-ftl/tests/mcp_tests.rs index 7bbe671..3715424 100644 --- a/flux-ftl/tests/mcp_tests.rs +++ b/flux-ftl/tests/mcp_tests.rs @@ -210,3 +210,40 @@ fn mcp_multiple_requests() { assert_eq!(resp1["id"], 1); assert_eq!(resp2["id"], 2); } + +#[test] +fn mcp_invalid_json() { + let (stdout, _) = send_request("this is not json\n"); + let first_line = stdout.lines().next().expect("should get error response"); + let resp: serde_json::Value = serde_json::from_str(first_line).expect("valid JSON error"); + assert_eq!(resp["error"]["code"], -32700); +} + +#[test] +fn mcp_notification_no_response() { + // Notifications (no id field) should produce no response + let notif = r#"{"jsonrpc":"2.0","method":"notifications/initialized"}"#; + let init = r#"{"jsonrpc":"2.0","id":1,"method":"initialize"}"#; + let input = format!("{}\n{}\n", init, notif); + let (stdout, _) = send_request(&input); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines.len(), 1, "notification should not produce a response"); +} + +#[test] +fn mcp_flux_evolve_valid() { + let ftl = std::fs::read_to_string("testdata/hello_world.ftl").expect("read testdata"); + + let resp = send_jsonrpc("tools/call", Some(serde_json::json!({ + "name": "flux_evolve", + "arguments": { "ftl_source": ftl, "generations": 2, "population": 3, "seed": 42 } + }))); + + assert!(resp["error"].is_null()); + let content = &resp["result"]["content"]; + let text = content[0]["text"].as_str().expect("text content"); + let evolve_result: serde_json::Value = serde_json::from_str(text).expect("valid JSON"); + assert!(evolve_result["generations_run"].is_number()); + assert!(evolve_result["best_fitness"].is_number()); + assert!(evolve_result["best_program"].is_object()); +} From 7613b7553c22705f8ddb10e78241efb7f7963963 Mon Sep 17 00:00:00 2001 From: Marco Doehler Date: Sat, 14 Mar 2026 19:07:06 +0000 Subject: [PATCH 4/4] Fix CI: add libpolly-14-dev for LLVM static linking Co-Authored-By: Claude Haiku 4.5 --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7cc9ce5..4db11ee 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: - name: Install system dependencies run: | sudo apt-get update - sudo apt-get install -y libz3-dev llvm-14-dev libllvm14 libclang-14-dev + sudo apt-get install -y libz3-dev llvm-14-dev libllvm14 libclang-14-dev libpolly-14-dev - name: Setup Rust uses: dtolnay/rust-toolchain@stable