Remove opaque Pixels type; add safe updateTexture and zero-copy updateTextureFromSurface

The opaque Pixels type wrapped a void* pointing into an SDL_Surface's
pixel buffer, but nothing tied the Pixels lifetime to the surface. If
the GC collected the surface first, the Pixels pointer would dangle,
causing use-after-free.

Replace with two safe alternatives:

- updateTexture now takes a ByteArray (Lean-owned, GC-managed buffer)
  plus pitch, matching how Haskell's sdl2 uses ByteString and Rust's
  rust-sdl2 uses &[u8]. This is faithful to SDL_UpdateTexture's general
  void* interface but requires copying pixels into a ByteArray first.

- updateTextureFromSurface is a new zero-copy convenience that takes an
  SDLSurface directly. The C side extracts both pixels and pitch from
  the surface internally. Because the surface is borrowed (@&) for the
  call's duration, the GC cannot collect it mid-use. This is not
  strictly faithful to SDL_UpdateTexture's C API, but is the common
  case and avoids an unnecessary memcpy.

Also removes: Pixels type, Pixels.nonemptyType, sdl_pixels_external_class,
sdl_Surface_get_pixels, and the pixels_external_class registration in
sdl_init.

WebcamApp.lean is updated to use updateTextureFromSurface.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

SDL.lean

@@ -132,10 +132,6 @@ instance SDLSurface.instNonempty : Nonempty SDLSurface := SDLSurface.nonemptyTyp
 
 namespace SDLSurface
 
-private opaque Pixels.nonemptyType : NonemptyType
-def Pixels: Type := Pixels.nonemptyType.type
-instance PIxels.instNonempty : Nonempty Pixels := Pixels.nonemptyType.property
-
 @[extern "sdl_Surface_get_format"]
 opaque format : @& SDLSurface -> UInt32
 
@@ -145,9 +141,6 @@ opaque w : @& SDLSurface -> Int32
 @[extern "sdl_Surface_get_h"]
 opaque h : @& SDLSurface -> Int32
 
-@[extern "sdl_Surface_get_pixels"]
-opaque pixels : @& SDLSurface -> Pixels
-
 @[extern "sdl_Surface_get_pitch"]
 opaque pitch : @& SDLSurface -> Int32
 
@@ -167,7 +160,16 @@ opaque createTextureFromSurface
 
 -- TODO handle SDLRect argument
 @[extern "sdl_update_texture"]
-opaque updateTexture (texture: @& SDLTexture) (pixels: @& SDLSurface.Pixels) (pitch: Int32): SDLIO Bool
+opaque updateTexture (texture: @& SDLTexture) (pixels: @& ByteArray) (pitch: Int32): SDLIO Bool
+
+-- Zero-copy optimization: updates a texture directly from an SDL_Surface's
+-- pixel buffer, avoiding the intermediate ByteArray copy required by
+-- updateTexture. This is not strictly faithful to the SDL_UpdateTexture C API
+-- (which takes a generic void* for pixels), but is safe because the surface
+-- is borrowed (@&) for the duration of the call, preventing the GC from
+-- collecting the surface (and its pixel data) while the update is in progress.
+@[extern "sdl_update_texture_from_surface"]
+opaque updateTextureFromSurface (texture: @& SDLTexture) (surface: @& SDLSurface): SDLIO Bool
 
 
 def loadImageTexture

WebcamApp.lean

@@ -106,10 +106,8 @@ partial def webcamLoop (stateRef: IO.Ref WebcamState): IO Unit := do
         let cameraTexture ← SDL.createTexture state.renderer cameraFrame.format SDL.SDL_TEXTUREACCESS_STREAMING w h
         stateRef.modify fun s => { s with texture := some cameraTexture }
       | some tx =>
-        -- Subsequent frames: update the texture
-        let pixels := cameraFrame.pixels
-        let pitch := cameraFrame.pitch
-        let _ ← SDL.updateTexture tx pixels pitch
+        -- Subsequent frames: update the texture directly from the camera frame
+        let _ ← SDL.updateTextureFromSurface tx cameraFrame
 
       SDL.releaseCameraFrame state.camera cameraFrame
 

c/sdl.c

@@ -99,13 +99,6 @@ static void sdl_mixer_audio_foreach(void * val, lean_obj_arg fn) {
 
 }
 
-static lean_external_class* sdl_pixels_external_class = NULL;
-static void sdl_pixels_foreach(void* vald, lean_obj_arg fn) {
-}
-static void sdl_pixels_finalizer(void*h) {
-}
-
-
 static lean_external_class * sdl_camera_external_class = NULL;
 static void sdl_camera_foreach(void * val, lean_obj_arg fn) {
 
@@ -141,7 +134,6 @@ lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
     sdl_camera_external_class = lean_register_external_class(sdl_camera_finalizer, sdl_camera_foreach);
     sdl_camera_spec_external_class = lean_register_external_class(sdl_camera_spec_finalizer, sdl_camera_spec_foreach);
     sdl_camera_frame_external_class = lean_register_external_class(sdl_camera_frame_finalizer, sdl_camera_frame_foreach);
-    sdl_pixels_external_class = lean_register_external_class(sdl_pixels_finalizer, sdl_pixels_foreach);
 
     return lean_io_result_mk_ok(lean_box_uint32(result));
 }
@@ -312,13 +304,6 @@ int32_t sdl_Surface_get_h(b_lean_obj_arg surface_obj) {
     return (int32_t)surface->h;
 }
 
-lean_object* sdl_Surface_get_pixels(b_lean_obj_arg surface_obj) {
-    SDL_Surface* surface = (SDL_Surface*)lean_get_external_data(surface_obj);
-    void* pixels = surface->pixels;
-    lean_object* external_pixels = lean_alloc_external(sdl_pixels_external_class, pixels);
-    return external_pixels;  // Not wrapped in IO - Lean expects Pixels directly
-}
-
 int32_t sdl_Surface_get_pitch(b_lean_obj_arg surface_obj) {
     SDL_Surface* surface = (SDL_Surface*)lean_get_external_data(surface_obj);
     return (int32_t)surface->pitch;
@@ -353,14 +338,27 @@ lean_obj_res sdl_create_texture_from_surface(b_lean_obj_arg g_renderer, b_lean_o
     return lean_io_result_mk_ok(external_texture);
 }
 
-lean_obj_res sdl_update_texture(b_lean_obj_arg texture_obj, b_lean_obj_arg pixels_obj, int32_t pitch) {
+lean_obj_res sdl_update_texture(b_lean_obj_arg texture_obj, b_lean_obj_arg byte_array, int32_t pitch) {
     SDL_Texture * texture = (SDL_Texture *)lean_get_external_data(texture_obj);
-    void* pixels = lean_get_external_data(pixels_obj);  // Pixels is void*, not SDL_Surface*
+    void* pixels = (void*)lean_sarray_cptr(byte_array);
 
     bool result = SDL_UpdateTexture(texture, NULL, pixels, pitch);
     return lean_io_result_mk_ok(lean_box(result));
 }
 
+// Zero-copy optimization: updates a texture directly from an SDL_Surface's
+// pixel buffer, avoiding the intermediate ByteArray copy. This is not
+// strictly faithful to the SDL_UpdateTexture C API (which takes a void*),
+// but is safe because the surface is borrowed for the duration of the call,
+// preventing the GC from freeing the pixel data mid-use.
+lean_obj_res sdl_update_texture_from_surface(b_lean_obj_arg texture_obj, b_lean_obj_arg surface_obj) {
+    SDL_Texture * texture = (SDL_Texture *)lean_get_external_data(texture_obj);
+    SDL_Surface * surface = (SDL_Surface *)lean_get_external_data(surface_obj);
+
+    bool result = SDL_UpdateTexture(texture, NULL, surface->pixels, surface->pitch);
+    return lean_io_result_mk_ok(lean_box(result));
+}
+
 lean_obj_res sdl_load_font(b_lean_obj_arg fontname, uint32_t font_size, lean_obj_arg w) {
     const char* fontname_str = lean_string_cstr(fontname);
     TTF_Font* font = TTF_OpenFont(fontname_str, font_size);