Buffer overflow in `lean_io_prim_handle_read`

-- file: Main.lean
def main : IO Unit := do
  IO.FS.writeFile "test_overflow.bin" "hello"
  let h ← IO.FS.Handle.mk "test_overflow.bin" .read
  -- SIZE_MAX = 2^64 - 1 on 64-bit. Construct it as USize.
  -- (0 : USize) - 1 wraps to SIZE_MAX
  let n : USize := (0 : USize) - (1 : USize)
  IO.eprintln s!"Attempting to read {n.toNat} bytes..."
  let result ← h.read n
  IO.println s!"Read {result.size} bytes"

-- file: lakefile.lean
import Lake
open Lake DSL
package overflow
@[default_target]
lean_exe overflow where
  root := `Main

# lake exe overflow
Attempting to read 18446744073709551615 bytes...
uncaught exception: bad address (error code: 14)

Lean version: 4.31.0-nightly-2026-04-13

valgrind --tool=memcheck --error-exitcode=99 ./.lake/build/bin/overflow 

~/lean-overflow-repro# lake clean && lake build overflow 
info: downloading https://github.com/leanprover/lean4-nightly/releases/download/nightly-2026-04-13/lean-4.31.0-nightly-2026-04-13-linux.tar.zst
508.0 MiB / 508.0 MiB (100 %) 134.3 MiB/s ETA:   0 s
info: installing /root/.elan/toolchains/leanprover--lean4-nightly---nightly-2026-04-13
Build completed successfully (4 jobs).
root@lean-prover-test-ash-1:~/lean-overflow-repro# ls -la ./.lake/build/bin/overflow
-rwxr-xr-x 1 root root 4165984 Apr 13 13:23 ./.lake/build/bin/overflow
root@lean-prover-test-ash-1:~/lean-overflow-repro# valgrind --tool=memcheck --error-exitcode=99 ./.lake/build/bin/overflow 
==398161== Memcheck, a memory error detector
==398161== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==398161== Using Valgrind-3.18.1 and LibVEX; rerun with -h for copyright info
==398161== Command: ./.lake/build/bin/overflow
==398161== 
==398161== Warning: set address range perms: large range [0x50354000000, 0x50394000000) (defined)
==398161== Warning: set address range perms: large range [0x4f89000, 0x44f8a000) (noaccess)
==398161== Warning: set address range perms: large range [0x59c87000, 0x99c88000) (noaccess)
Attempting to read 18446744073709551615 bytes...
==398161== Thread 3:
==398161== Syscall param read(buf) points to unaddressable byte(s)
==398161==    at 0x497589C: __libc_read (read.c:26)
==398161==    by 0x497589C: read (read.c:24)
==398161==    by 0x48EC394: _IO_file_xsgetn (fileops.c:1341)
==398161==    by 0x48E0BA8: fread (iofread.c:38)
==398161==    by 0x2E990B: lean_io_prim_handle_read (in /root/lean-overflow-repro/.lake/build/bin/overflow)
==398161==    by 0x1A50D4: _lean_main (in /root/lean-overflow-repro/.lake/build/bin/overflow)
==398161==    by 0x283826: std::__1::__function::__func<lean_run_main::$_0, std::__1::allocator<lean_run_main::$_0>, void ()>::operator()() (in /root/lean-overflow-repro/.lake/build/bin/overflow)
==398161==    by 0x283DF4: lean::lthread::imp::_main(void*) (in /root/lean-overflow-repro/.lake/build/bin/overflow)
==398161==    by 0x48F5AC2: start_thread (pthread_create.c:442)
==398161==    by 0x4986A83: clone (clone.S:100)
==398161==  Address 0x50394000000 is not stack'd, malloc'd or (recently) free'd
==398161== 
==398161== Warning: set address range perms: large range [0x59c87000, 0x99c88000) (noaccess)
uncaught exception: bad address (error code: 14)
==398161== 
==398161== HEAP SUMMARY:
==398161==     in use at exit: 17,944 bytes in 35 blocks
==398161==   total heap usage: 168 allocs, 133 frees, 47,547 bytes allocated
==398161== 
==398161== LEAK SUMMARY:
==398161==    definitely lost: 0 bytes in 0 blocks
==398161==    indirectly lost: 0 bytes in 0 blocks
==398161==      possibly lost: 288 bytes in 1 blocks
==398161==    still reachable: 17,656 bytes in 34 blocks
==398161==         suppressed: 0 bytes in 0 blocks
==398161== Rerun with --leak-check=full to see details of leaked memory
==398161== 
==398161== For lists of detected and suppressed errors, rerun with: -s
==398161== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)