Bend 2 and the Vibe-Coding Trap

package Game with SPARK_Mode is subtype Column is Integer range 0 .. 11; subtype Row is Integer range 0 .. 7; type State is record X : Column; Y : Row; Won : Boolean; end record; Start : constant State := (8, 5, False); function Wall (X : Column; Y : Row) return Boolean is (((X = 3 or X = 11) and Y <= 3) or ((Y = 3 or Y = 7) and X <= 3)); function Cell (X : Column; Y : Row) return Character is (if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.'); -- Inductive invariant: outside the sealed room, off walls, not won. function Safe (G : State) return Boolean is ((G.X > 2 or G.Y > 2) and not Wall (G.X, G.Y) and not G.Won) with Ghost; procedure Step (G : in out State; Key : Character) with Post => (if Safe (G'Old) then Safe (G)); -- Both Bend laws, including the actual cell drawn by the terminal. function Replay (Keys : String) return State with Post => not Replay'Result.Won and Cell (Replay'Result.X, Replay'Result.Y) /= 'F'; end Game; ------------------------------ package body Game with SPARK_Mode is procedure Step (G : in out State; Key : Character) is X : Column := G.X; Y : Row := G.Y; begin case Key is when 'w' => Y := (Y - 1) mod 8; when 's' => Y := (Y + 1) mod 8; when 'a' => X := (X - 1) mod 12; when 'd' => X := (X + 1) mod 12; when others => return; end case; if not Wall (X, Y) then G := (X, Y, G.Won or Cell (X, Y) = 'F'); end if; end Step; function Replay (Keys : String) return State is G : State := Start; begin for Key of Keys loop pragma Loop_Invariant (Safe (G)); Step (G, Key); end loop; return G; end Replay; end Game; ------------------------------ with Ada.Text_IO; use Ada.Text_IO; with Game; use Game; procedure Main is G : State := Start; begin Put_Line ("Winning is impossible. WASD + Enter to move; q + Enter to quit."); loop for Y in Row loop for X in Column loop Put (if X = G.X and Y = G.Y then 'P' else Cell (X, Y)); end loop; New_Line; end loop; Put_Line (if G.Won then "WON (this should be unreachable)" else "still not won"); exit when End_Of_File; declare Keys : constant String := Get_Line; begin exit when Keys = "q"; for Key of Keys loop Step (G, Key); end loop; end; end loop; end Main;