fix: issue with session

.claude/CLAUDE.md

@@ -7,11 +7,6 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
 The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
 Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
 
-To rebuild individual modules without a full build, use Lake directly:
-```
-cd src && lake build Init.Prelude
-```
-
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -61,11 +56,6 @@ make -C build/release/stage2 clean-stdlib
 ```
 must be run manually before building.
 
-To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
-```
-cd build/release/stage2 && lake build Init.Prelude
-```
-
 ## New features
 
 When asked to implement new features:

.github/workflows/build-template.yml

@@ -59,11 +59,11 @@ jobs:
         with:
           msystem: clang64
           # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv
+          brew install ccache tree zstd coreutils gmp libuv openssl
         if: runner.os == 'macOS'
       - name: Checkout
         uses: actions/checkout@v6
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 libssl-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache

doc/make/index.md

@@ -9,6 +9,7 @@ Requirements
 - [CMake](http://www.cmake.org)
 - [GMP (GNU multiprecision library)](http://gmplib.org/)
 - [LibUV](https://libuv.org/)
+- [OpenSSL](https://www.openssl.org/)
 
 Platform-Specific Setup
 -----------------------

doc/make/msys2.md

@@ -32,7 +32,7 @@ MSYS2 has a package management system, [pacman][pacman].
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
+pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp mingw-w64-clang-x86_64-openssl git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:

doc/make/osx-10.9.md

@@ -32,12 +32,13 @@ following to use `g++`.
 cmake -DCMAKE_CXX_COMPILER=g++ ...
 ```
 
-## Required Packages: CMake, GMP, libuv, pkgconf
+## Required Packages: CMake, GMP, libuv, OpenSSL, pkgconf
 
 ```bash
 brew install cmake
 brew install gmp
 brew install libuv
+brew install openssl
 brew install pkgconf
 ```
 

doc/make/ubuntu.md

@@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
 ## Basic packages
 
 ```bash
-sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang pkgconf
+sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf
 ```

flake.nix

@@ -24,7 +24,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config
+            cmake gmp libuv ccache pkg-config openssl openssl.dev
             llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
@@ -34,7 +34,21 @@
           hardeningDisable = [ "all" ];
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
-        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux (let
+          # Build OpenSSL 3 statically using pkgsDist's old-glibc stdenv,
+          # so the resulting static libs don't require newer glibc symbols.
+          opensslForDist = pkgsDist.stdenv.mkDerivation {
+            name = "openssl-static-${pkgs.lib.getVersion pkgs.openssl.name}";
+            inherit (pkgs.openssl) src;
+            nativeBuildInputs = [ pkgsDist.perl ];
+            configurePhase = ''
+            patchShebangs .
+            ./config --prefix=$out no-shared no-tests
+          '';
+            buildPhase = "make -j$NIX_BUILD_CORES";
+            installPhase = "make install_sw";
+          };
+        in {
           GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
             pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
               # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
@@ -53,13 +67,15 @@
             };
             doCheck = false;
           });
+          OPENSSL = opensslForDist;
+          OPENSSL_DEV = opensslForDist;
           GLIBC = pkgsDist.glibc;
           GLIBC_DEV = pkgsDist.glibc.dev;
           GCC_LIB = pkgsDist.gcc.cc.lib;
           ZLIB = pkgsDist.zlib;
           # for CI coredumps
           GDB = pkgsDist.gdb;
-        });
+        }));
     in {
       devShells.${system} = {
         # The default development shell for working on lean itself

script/prepare-llvm-linux.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
-# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
+# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP/OPENSSL) as in
 # ```
 # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/lean-llvm-x86_64-linux-gnu.tar.zst)
 # ```
@@ -42,6 +42,8 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
+# bundle OpenSSL static libs
+cp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
 # LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
 # but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
@@ -57,6 +59,7 @@ for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f st
 OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
+echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL_DEV/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
 # these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
 echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
@@ -74,8 +77,8 @@ fi
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
 # ld.so is usually included by the libc.so linker script but we discard those. Make sure it is linked to only after `libc.so` like in the original
 # linker script so that no libc symbols are bound to it instead.
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lssl -lcrypto -Wl,-Bdynamic -Wl,--no-as-needed -Wl,--disable-new-dtags,-rpath,ROOT/lib -fuse-ld=lld'"
+# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,-Bstatic -lssl -lcrypto -Wl,-Bdynamic -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-macos.sh

@@ -10,6 +10,7 @@ set -uxo pipefail
 
 GMP=${GMP:-$(brew --prefix)}
 LIBUV=${LIBUV:-$(brew --prefix)}
+OPENSSL=${OPENSSL:-$(brew --prefix openssl@3)}
 
 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
 [[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@@ -41,6 +42,7 @@ gcp llvm/lib/libc++.dylib stage1/lib/libc
 # and apparently since Sonoma does not do so implicitly either
 install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLEAN_STANDALONE=ON"
+echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
@@ -48,7 +50,7 @@ if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
   gcp $LIBUV/lib/libuv.a stage1/lib/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
 fi

script/prepare-llvm-mingw.sh

@@ -40,14 +40,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
 # This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
 # be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu,crypt32,gdi32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a /clang64/lib/libssl.a /clang64/lib/libcrypto.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lssl -lcrypto -lunwind -Wl,-Bdynamic -lcrypt32 -lgdi32 -fuse-ld=lld'"
+# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual. Always link ICU dynamically.
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lssl -lcrypto -lcrypt32 -lgdi32 -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

src/CMakeLists.txt

@@ -356,6 +356,48 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
+# OpenSSL
+if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  # Only on WebAssembly we compile OpenSSL ourselves
+  set(OPENSSL_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
+
+  # OpenSSL needs to be configured for Emscripten using their configuration system
+  ExternalProject_add(openssl
+    PREFIX openssl
+    GIT_REPOSITORY https://github.com/openssl/openssl
+    # Sync version with flake.nix if applicable
+    GIT_TAG openssl-3.0.15
+    CONFIGURE_COMMAND <SOURCE_DIR>/Configure linux-generic32 no-shared no-dso no-engine no-tests --prefix=<INSTALL_DIR> CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} AR=${CMAKE_AR} CFLAGS=${OPENSSL_EMSCRIPTEN_FLAGS}
+    BUILD_COMMAND emmake make -j
+    INSTALL_COMMAND emmake make install_sw
+    BUILD_IN_SOURCE ON)
+  set(OPENSSL_INCLUDE_DIR "${CMAKE_BINARY_DIR}/openssl/include")
+  set(OPENSSL_CRYPTO_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libcrypto.a")
+  set(OPENSSL_SSL_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libssl.a")
+  set(OPENSSL_LIBRARIES "${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY}")
+else()
+  find_package(OpenSSL 3 REQUIRED)
+  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
+endif()
+include_directories(${OPENSSL_INCLUDE_DIR})
+string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
+string(APPEND LEANSHARED_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
+
+if(NOT LEAN_STANDALONE)
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
+endif()
+
+if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--disable-new-dtags,-rpath,$$ORIGIN")
+endif()
+
+if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  if(NOT LEAN_STANDALONE)
+    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  endif()
+endif()
+
 # Windows SDK (for ICU)
 if(CMAKE_SYSTEM_NAME MATCHES "Windows")
   # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -614,38 +656,6 @@ else()
       OUTPUT_VARIABLE GIT_SHA1
       OUTPUT_STRIP_TRAILING_WHITESPACE
     )
-    # Fallback for jj workspaces where git cannot find .git directly.
-    # Use `jj git root` to find the backing git repo, then `jj log` to
-    # resolve the current workspace's commit (git HEAD points to the root
-    # workspace, not the current one).
-    if("${GIT_SHA1}" STREQUAL "")
-      find_program(JJ_EXECUTABLE jj)
-      if(JJ_EXECUTABLE)
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" git root
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_git_dir
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_git_root_result
-        )
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_commit
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_rev_result
-        )
-        if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
-          execute_process(
-            COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
-            OUTPUT_VARIABLE GIT_SHA1
-            OUTPUT_STRIP_TRAILING_WHITESPACE
-          )
-        endif()
-      endif()
-    endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
     # Now that we've prepared the information for the next stage, we can forget that we will use
     # Lake in the future as we won't use it in this stage
@@ -762,9 +772,9 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-    add_dependencies(leanrt libuv)
-    add_dependencies(leanrt_initial-exec libuv)
+  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+    add_dependencies(leanrt libuv openssl)
+    add_dependencies(leanrt_initial-exec libuv openssl)
   endif()
 
   add_subdirectory(util)
@@ -829,14 +839,7 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(
-  STDLIBS
-  Init
-  Std
-  Lean
-  Leanc
-  LeanIR
-)
+set(STDLIBS Init Std Lean Leanc LeanIR)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -944,7 +947,10 @@ if(PREV_STAGE)
 endif()
 
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-  add_custom_target(leanir ALL DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir VERBATIM)
+  add_custom_target(leanir ALL
+    DEPENDS leanshared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
+    VERBATIM)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

src/Init.lean

@@ -40,7 +40,6 @@ public import Init.Grind
 public import Init.GrindInstances
 public import Init.Sym
 public import Init.While
-public import Init.Repeat
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try

src/Init/Grind/Util.lean

@@ -30,13 +30,13 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
 ```
 using `eq_self`.
 -/
-@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
 /--
 Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
 from beta reduction during preprocessing. See `ProveEq.lean` for details.
 -/
-@[expose] def abstractFn {α : Sort u} (a : α) : α := a
+def abstractFn {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

src/Init/Notation.lean

@@ -624,23 +624,6 @@ existing code. It may be removed in a future version of the library.
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr
 
-/--
-The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.
-
-When a caller uses the old name with a replacement available, a deprecation warning is emitted
-and the argument is silently forwarded to the new parameter. When no replacement is provided,
-the parameter is treated as removed and using it produces an error.
-
-* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
-* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
-* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
-* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.
-
-A warning is emitted if `(since := "...")` is omitted.
--/
-syntax (name := deprecated_arg) "deprecated_arg" ppSpace ident (ppSpace ident)? (ppSpace str)?
-    (" (" &"since" " := " str ")")? : attr
-
 /--
 The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
 someone might **incorrectly** refer to a definition.

src/Init/Repeat.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.Core
-public import Init.Control.MonadAttach
-public import Init.WFExtrinsicFix
-import Init.While
-
-set_option linter.missingDocs true
-
-@[expose] public section
-
-namespace Lean
-
-/-!
-# Well-founded `Repeat` type for verified `repeat`/`while` loops
-
-This module provides a `Repeat` type that serves as an alternative to `Loop` for `repeat`/`while`
-loops. Unlike `Loop`, which uses `partial` recursion, `Repeat` is implemented using
-`WellFounded.extrinsicFix` and `MonadAttach`, enabling verified reasoning about loop programs.
--/
-
-/-- A type for `repeat`/`while` loops that supports well-founded reasoning via `extrinsicFix`. -/
-inductive Repeat where
-  /-- Creates a `Repeat` value. -/
-  | mk
-
-/--
-The step relation for well-founded recursion in `Repeat.forIn`.
-Relates `b'` to `b` when `f () b` can plausibly return `ForInStep.yield b'`,
-as witnessed by `MonadAttach.CanReturn`.
--/
-def Repeat.IsPlausibleStep {β : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m]
-    (f : Unit → β → m (ForInStep β)) : β → β → Prop :=
-  fun b' b => MonadAttach.CanReturn (f () b) (ForInStep.yield b')
-
-/-- Iterates the body `f` using well-founded recursion via `extrinsicFix`. -/
-@[inline]
-def Repeat.forIn {β : Type u} {m : Type u → Type v} [Monad m] [MonadAttach m]
-    (_ : Repeat) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  haveI : Nonempty β := ⟨init⟩
-  WellFounded.extrinsicFix (Repeat.IsPlausibleStep f) (a := init) fun b recur => do
-    match ← MonadAttach.attach (f () b) with
-      | ⟨ForInStep.done b, _⟩ => pure b
-      | ⟨ForInStep.yield b, h⟩ => recur b h
-
-instance [Monad m] [MonadAttach m] : ForIn m Repeat Unit where
-  forIn := Repeat.forIn
-
-/-- Override the bootstrapping `repeat` macro from `Init.While` to use `Repeat.mk` instead of
-`Loop.mk`. When the builtin do-element elaborator for `repeat` is available (`backward.do.while`
-option dispatch), this macro defers to it by throwing `unsupportedSyntax`. -/
-macro_rules
-  | `(doElem| repeat $seq) => do
-    if ← Macro.hasDecl `Lean.Elab.Do.elabDoRepeat then
-      Lean.Macro.throwUnsupported
-    `(doElem| for _ in Repeat.mk do $seq)
-
-end Lean

src/Init/While.lean

@@ -32,11 +32,8 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax (name := doRepeat) "repeat " doSeq : doElem
+syntax "repeat " doSeq : doElem
 
-/-- Bootstrapping fallback macro for `repeat`.
-Expands to `for _ in Loop.mk do ...`. Overridden by the macro in `Init.Repeat` after
-bootstrapping. -/
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
 

src/Lean/Compiler/LCNF/CoalesceRC.lean

@@ -21,7 +21,7 @@ Within a basic block, it is always safe to:
   until the later inc) and thus doing all relevant `inc` in the beginning doesn't change
   semantics.
 - Move all decrements on a variable to the last `dec` location (summing the counts). Because the
-  value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to
+  value is guaranteed to stay alive until at least the last `dec` anyway so a similiar argument to
   `inc` holds.
 
 Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -69,8 +69,8 @@ open ImpureType
 abbrev Mask := Array (Option FVarId)
 
 /--
-Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`.
-Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed.
+Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
+Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
 -/
 partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
     CompilerM (Array (CodeDecl .impure) × Mask) := do

src/Lean/Elab.lean

@@ -39,7 +39,6 @@ public import Lean.Elab.Extra
 public import Lean.Elab.GenInjective
 public import Lean.Elab.BuiltinTerm
 public import Lean.Elab.Arg
-public import Lean.Elab.DeprecatedArg
 public import Lean.Elab.PatternVar
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Macro

src/Lean/Elab/App.lean

@@ -11,7 +11,6 @@ public import Lean.Elab.Binders
 public import Lean.Elab.RecAppSyntax
 public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
-import Lean.Elab.DeprecatedArg
 import Init.Omega
 
 public section
@@ -89,38 +88,6 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U
 private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg :=
   namedArgs.find? fun namedArg => namedArg.name == binderName
 
-/--
-If the function being applied is a constant, search `namedArgs` for an argument whose name is
-a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
-returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
-option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
-error). The returned `namedArg` retains its original (old) name.
--/
-private def findDeprecatedBinderName? (namedArgs : List NamedArg) (f : Expr) (binderName : Name) :
-    TermElabM (Option NamedArg) := do
-  unless linter.deprecated.arg.get <| ← getOptions do return .none
-  unless f.getAppFn.isConst do return none
-  let declName := f.getAppFn.constName!
-  let env ← getEnv
-  for namedArg in namedArgs do
-    if let some entry := findDeprecatedArg? env declName namedArg.name then
-      if entry.newArg? == some binderName then
-        let msg := formatDeprecatedArgMsg entry
-        let span? := namedArg.ref[1]
-        let hint ←
-          if span?.getHeadInfo matches .original .. then
-            MessageData.hint "Rename this argument:" #[{
-              suggestion := .string entry.newArg?.get!.toString
-              span?
-              toCodeActionTitle? := some fun s =>
-                s!"Rename argument `{entry.oldArg}` to `{s}`"
-            }]
-          else
-            pure .nil
-        logWarningAt namedArg.ref <| .tagged ``deprecatedArgExt msg ++ hint
-        return some namedArg
-  return none
-
 /-- Erase entry for `binderName` from `namedArgs`. -/
 def eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
   namedArgs.filter (·.name != binderName)
@@ -271,23 +238,6 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
     else
       for namedArg in s.namedArgs do
         let f := s.f.getAppFn
-        if f.isConst then
-          let env ← getEnv
-          if linter.deprecated.arg.get (← getOptions) then
-            if let some entry := findDeprecatedArg? env f.constName! namedArg.name then
-              if entry.newArg?.isNone then
-                let msg := formatDeprecatedArgMsg entry
-                let hint ←
-                  if namedArg.ref.getHeadInfo matches .original .. then
-                    MessageData.hint "Delete this argument:" #[{
-                      suggestion := .string ""
-                      span? := namedArg.ref
-                      toCodeActionTitle? := some fun _ =>
-                        s!"Delete deprecated argument `{entry.oldArg}`"
-                    }]
-                  else
-                    pure .nil
-                throwErrorAt namedArg.ref (msg ++ hint)
         let validNames ← getFoundNamedArgs
         let fnName? := if f.isConst then some f.constName! else none
         throwInvalidNamedArg namedArg fnName? validNames
@@ -806,16 +756,13 @@ mutual
       let binderName := fType.bindingName!
       let binfo := fType.bindingInfo!
       let s ← get
-      let namedArg? ← match findBinderName? s.namedArgs binderName with
-        | some namedArg => pure (some namedArg)
-        | none => findDeprecatedBinderName? s.namedArgs s.f binderName
-      match namedArg? with
+      match findBinderName? s.namedArgs binderName with
       | some namedArg =>
         propagateExpectedType namedArg.val
-        eraseNamedArg namedArg.name
+        eraseNamedArg binderName
         elabAndAddNewArg binderName namedArg.val
         main
-      | none =>
+      | none          =>
         unless binderName.hasMacroScopes do
           pushFoundNamedArg binderName
         match binfo with

src/Lean/Elab/BuiltinDo.lean

@@ -15,4 +15,3 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
-public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/If.lean

@@ -63,6 +63,6 @@ where
     doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
     let mγ ← mkMonadicType (← read).doBlockResultType
     match h with
-    | `(_%$tk) => Term.elabTermEnsuringType (← `(if _%$tk : $cond then $then_ else $else_)) mγ
+    | `(_%$tk) => Term.elabTermEnsuringType (← `(if $(⟨tk⟩):hole : $cond then $then_ else $else_)) mγ
     | `($h:ident) => Term.elabTermEnsuringType (← `(if $h:ident : $cond then $then_ else $else_)) mγ
     | _ => throwUnsupportedSyntax

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -1,37 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Lean.Elab.BuiltinDo.Basic
-meta import Lean.Parser.Do
-import Lean.Elab.BuiltinDo.For
-import Lean.Elab.Do.Switch
-
-public section
-
-namespace Lean.Elab.Do
-
-open Lean.Parser.Term
-
-/--
-Builtin do-element elaborator for `repeat` (syntax kind `Lean.doRepeat`).
-
-When `backward.do.while` is `true`, expands to `for _ in Loop.mk do ...` (legacy behavior).
-When `backward.do.while` is `false` (default), expands to `for _ in Repeat.mk do ...`
-(well-founded behavior).
--/
-@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
-  let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax
-  let expanded ←
-    if Term.backward.do.while.get (← getOptions) then
-      `(doElem| for _ in Loop.mk do $seq)
-    else
-      `(doElem| for _ in Repeat.mk do $seq)
-  Term.withMacroExpansion stx expanded <|
-    withRef expanded <| elabDoElem ⟨expanded⟩ dec
-
-end Lean.Elab.Do

src/Lean/Elab/Coinductive.lean

@@ -43,7 +43,7 @@ builtin_initialize
 
   Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
   way its done for inductive declarations, but we omit applying attributes/modifiers and
-  we do not set the syntax references to track those declarations (as this is auxiliary piece of
+  we do not set the syntax references to track those declarations (as this is auxillary piece of
   data hidden from the user).
 
   Then, upon adding such flat inductives for each definition in the mutual block to the environment,
@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         | throwError "expected to be quantifier"
       let motiveMVar ← mkFreshExprMVar type
       /-
-        We intro all the indices and the occurrence of the coinductive predicate
+        We intro all the indices and the occurence of the coinductive predicate
       -/
       let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
       subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
           -/
           let originalCasesOn := mkAppN originalCasesOn indices
           /-
-            The next argument is the occurrence of the coinductive predicate.
+            The next argument is the occurence of the coinductive predicate.
             The original `casesOn` of the flat inductive mentions it in
             unrolled form, so we need to rewrite it.
           -/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
   let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
   /-
     We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
-    form of the associated flat inductives and applying parameters, as well as recursive calls
+    form of the associated flat inductives and applying paramaters, as well as recursive calls
     (with their parameters passed).
   -/
   let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

src/Lean/Elab/DeprecatedArg.lean

@@ -1,97 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.EnvExtension
-public import Lean.Message
-import Lean.Elab.Term
-
-public section
-
-namespace Lean.Elab
-open Meta
-
-register_builtin_option linter.deprecated.arg : Bool := {
-  defValue := true
-  descr := "if true, generate deprecation warnings and errors for deprecated parameters"
-}
-
-/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration. -/
-structure DeprecatedArgEntry where
-  declName : Name
-  oldArg : Name
-  newArg? : Option Name := none
-  text? : Option String := none
-  since? : Option String := none
-  deriving Inhabited
-
-/-- State: `declName → (oldArg → entry)` -/
-abbrev DeprecatedArgState := NameMap (NameMap DeprecatedArgEntry)
-
-private def addDeprecatedArgEntry (s : DeprecatedArgState) (e : DeprecatedArgEntry) : DeprecatedArgState :=
-  let inner := (s.find? e.declName).getD {} |>.insert e.oldArg e
-  s.insert e.declName inner
-
-builtin_initialize deprecatedArgExt :
-    SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState ←
-  registerSimplePersistentEnvExtension {
-    addEntryFn := addDeprecatedArgEntry
-    addImportedFn := mkStateFromImportedEntries addDeprecatedArgEntry {}
-  }
-
-/-- Look up a deprecated argument mapping for `(declName, argName)`. -/
-def findDeprecatedArg? (env : Environment) (declName : Name) (argName : Name) :
-    Option DeprecatedArgEntry :=
-  (deprecatedArgExt.getState env |>.find? declName) >>= (·.find? argName)
-
-/-- Format the deprecation warning message for a deprecated argument. -/
-def formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData :=
-  let base := match entry.newArg? with
-  | some newArg =>
-    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated, \
-      use `{newArg}` instead"
-  | none =>
-    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated"
-  match entry.text? with
-  | some text => base ++ m!": {text}"
-  | none => base
-
-builtin_initialize registerBuiltinAttribute {
-  name := `deprecated_arg
-  descr := "mark a parameter as deprecated"
-  add := fun declName stx _kind => do
-    let `(attr| deprecated_arg $oldId $[$newId?]? $[$text?]? $[(since := $since?)]?) := stx
-      | throwError "Invalid `[deprecated_arg]` attribute syntax"
-    let oldArg := oldId.getId
-    let newArg? := newId?.map TSyntax.getId
-    let text? := text?.map TSyntax.getString |>.filter (!·.isEmpty)
-    let since? := since?.map TSyntax.getString
-    let info ← getConstInfo declName
-    let paramNames ← MetaM.run' do
-      forallTelescopeReducing info.type fun xs _ =>
-        xs.mapM fun x => return (← x.fvarId!.getDecl).userName
-    if let some newArg := newArg? then
-      -- We have a replacement provided
-      unless Array.any paramNames (· == newArg) do
-        throwError "`{newArg}` is not a parameter of `{declName}`"
-      if Array.any paramNames (· == oldArg) then
-        throwError "`{oldArg}` is still a parameter of `{declName}`; \
-          rename it to `{newArg}` before adding `@[deprecated_arg]`"
-    else
-      -- We do not have a replacement provided
-      if Array.any paramNames (· == oldArg) then
-        throwError "`{oldArg}` is still a parameter of `{declName}`; \
-          remove it before adding `@[deprecated_arg]`"
-    if since?.isNone then
-      logWarning "`[deprecated_arg]` attribute should specify the date or library version \
-        at which the deprecation was introduced, using `(since := \"...\")`"
-    modifyEnv fun env => deprecatedArgExt.addEntry env {
-      declName, oldArg, newArg?, text?, since?
-    }
-}
-
-end Lean.Elab

src/Lean/Elab/Do/Legacy.lean

@@ -1780,10 +1780,6 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
-          else if k == `Lean.doRepeat then
-            let seq := doElem[1]
-            let expanded ← `(doElem| for _ in Loop.mk do $seq)
-            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/Do/Switch.lean

@@ -19,11 +19,6 @@ register_builtin_option backward.do.legacy : Bool := {
   descr    := "Use the legacy `do` elaborator instead of the new, extensible implementation."
 }
 
-register_builtin_option backward.do.while : Bool := {
-  defValue := false
-  descr    := "Use the legacy partial `Loop` type for `repeat`/`while` loops instead of the well-founded `Repeat` type. Useful as a workaround when the monad lacks a `MonadAttach` instance."
-}
-
 private def toDoElem (newKind : SyntaxNodeKind) : Macro := fun stx => do
   let stx := stx.setKind newKind
   withRef stx `(do $(⟨stx⟩):doElem)

src/Lean/LibrarySuggestions/Basic.lean

@@ -91,10 +91,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -99,7 +99,7 @@ where
       if (← withReducibleAndInstances <| isDefEq x val) then
         return true
       else
-        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsynthesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
+        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
         return false
     | _ =>
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"

src/Lean/Runtime.lean

@@ -21,6 +21,9 @@ opaque maxSmallNatFn : Unit → Nat
 @[extern "lean_libuv_version"]
 opaque libUVVersionFn : Unit → Nat
 
+@[extern "lean_openssl_version"]
+opaque openSSLVersionFn : Unit → Nat
+
 def closureMaxArgs : Nat :=
   closureMaxArgsFn ()
 
@@ -30,4 +33,7 @@ def maxSmallNat : Nat :=
 def libUVVersion : Nat :=
   libUVVersionFn ()
 
+def openSSLVersion : Nat :=
+  openSSLVersionFn ()
+
 end Lean

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -46,7 +46,7 @@ structure LeanSemanticToken where
   stx  : Syntax
   /-- Type of the semantic token. -/
   type : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precedence -/
+  /-- In case of overlap, higher-priority tokens will take precendence -/
   priority : Nat := 5
 
 /-- Semantic token information with absolute LSP positions. -/
@@ -57,7 +57,7 @@ structure AbsoluteLspSemanticToken where
   tailPos : Lsp.Position
   /-- Start position of the semantic token. -/
   type    : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precedence -/
+  /-- In case of overlap, higher-priority tokens will take precendence -/
   priority : Nat := 5
   deriving BEq, Hashable, FromJson, ToJson
 

src/Std/Do/SPred/Laws.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
-import Init.PropLemmas
 
 @[expose] public section
 
@@ -158,17 +157,3 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
-
-/-! # Prop-indexed quantifiers -/
-
-/-- Simplifies an existential over a true proposition. -/
-theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
-  induction σs with
-  | nil => ext; exact _root_.exists_prop_of_true h
-  | cons σ σs ih => ext; exact ih
-
-/-- Simplifies a universal over a true proposition. -/
-theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
-  induction σs with
-  | nil => ext; exact _root_.forall_prop_of_true h
-  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Std.Do.Triple.SpecLemmas
-import Std.Tactic.Do.Syntax
-
-set_option linter.missingDocs true
-
-@[expose] public section
-
-namespace Std.Do
-
-/-!
-# Specification theorem for `Repeat` loops
-
-This file contains the `@[spec]` theorem for `forIn` over `Lean.Repeat`, which enables
-verified reasoning about `repeat`/`while` loops using `mvcgen`.
--/
-
-set_option mvcgen.warning false
-
-section
-
-variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
-variable [Monad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps]
-
-/--
-Specification for `forIn` over a `Lean.Repeat` value.
-Takes a variant (termination measure), an invariant, a proof that the variant decreases,
-and a proof that each step preserves the invariant.
--/
-@[spec]
-theorem Spec.forIn_repeat
-    {l : _root_.Lean.Repeat} {init : β} {f : Unit → β → m (ForInStep β)}
-    (_variant : RepeatVariant β)
-    (inv : RepeatInvariant β ps)
-    (hwf : WellFounded (_root_.Lean.Repeat.IsPlausibleStep f))
-    (step : ∀ b,
-      Triple
-        (f () b)
-        (inv.1 (.repeat b))
-        (fun r => match r with
-          | .yield b' => inv.1 (.repeat b')
-          | .done b' => inv.1 (.done b'), inv.2)) :
-    Triple (forIn l init f) (inv.1 (.repeat init)) (fun b => inv.1 (.done b), inv.2) := by
-  change Triple (_root_.Lean.Repeat.forIn l init f) _ _
-  simp only [_root_.Lean.Repeat.forIn, WellFounded.extrinsicFix_eq_fix hwf]
-  induction hwf.apply init with
-  | intro b hacc ih =>
-  rw [WellFounded.fix_eq]
-  mvcgen [step, ih]
-  rename_i stp
-  apply SPred.forall_intro
-  intro _
-  cases stp <;> mvcgen [ih]
-
-end
-
-end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,8 +10,6 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
-public import Std.Do.WP.Adequacy
-public import Init.Repeat
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.
@@ -2190,90 +2188,3 @@ theorem Spec.forIn_stringSlice
       next => apply Triple.pure; simp
       next b => simp [ih _ _ hsp.next]
   | endPos => simpa using Triple.pure _ (by simp)
-
-/-!
-# Repeat loop specification infrastructure
--/
-
-/--
-Cursor type for `Repeat` loop invariants.
-Represents either a loop iteration in progress or a completed loop.
--/
-inductive RepeatCursor (β : Type u) where
-  /-- The loop is in progress with the current accumulator state `s`. -/
-  | «repeat» (s : β) : RepeatCursor β
-  /-- The loop has finished with the final accumulator state `s`. -/
-  | done (s : β) : RepeatCursor β
-
-/--
-An invariant for a `Repeat` loop. A postcondition over `RepeatCursor β` capturing both
-the in-progress and completed states.
--/
-@[spec_invariant_type]
-abbrev RepeatInvariant (β : Type u) (ps : PostShape.{u}) := PostCond (RepeatCursor β) ps
-
-/--
-A variant (termination measure) for a `Repeat` loop.
-Maps the accumulator state to a natural number that decreases with each iteration.
--/
-@[spec_invariant_type]
-abbrev RepeatVariant (β : Type u) := β → Nat
-
-section
-
-variable {α : Type u₁} {m : Type u₁ → Type v} {ps : PostShape.{u₁}}
-variable [Monad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps]
-
-/--
-Specification for `MonadAttach.attach`: the precondition is the weakest precondition of `x` with
-a postcondition that universally quantifies over the `CanReturn` proof.
--/
-@[spec]
-theorem Spec.attach
-    {x : m α} {Q : PostCond (Subtype (MonadAttach.CanReturn x)) ps} :
-    ⦃ wp⟦x⟧ ⟨fun a => spred(∀ (h : MonadAttach.CanReturn x a), Q.1 ⟨a, h⟩), Q.2⟩ ⦄ MonadAttach.attach x ⦃Q⦄ := by
-  apply Triple.iff.mpr
-  conv in wp x => rw [← WeaklyLawfulMonadAttach.map_attach (x := x)]
-  simp only [WPMonad.wp_map]
-  -- Goal: (Subtype.val <$> wp (attach x)).apply ⟨..., Q.2⟩ ⊢ₛ (wp (attach x)).apply Q
-  -- Rewrite LHS using apply_Functor_map
-  rw [PredTrans.apply_Functor_map]
-  -- Now both sides have (wp (attach x)).apply, use mono
-  apply (wp (MonadAttach.attach x)).mono
-  constructor
-  · intro ⟨a, h⟩
-    dsimp only []
-    rw [SPred.forall_prop_of_true h]
-  · dsimp only []
-    exact ExceptConds.entails.refl _
-
-end
-
-section
-
-variable {β : Type u₁} {m : Type u₁ → Type v} {ps : PostShape.{u₁}}
-variable [Monad m] [MonadAttach m] [WPAdequacy m ps]
-
-/--
-Derives well-foundedness of `_root_.Lean.Repeat.IsPlausibleStep f` from a WP proof that every
-step decreases a measure.
--/
-theorem _root_.Lean.Repeat.IsPlausibleStep.wf_of_wp_measure {f : Unit → β → m (ForInStep β)}
-    (measure : β → Nat)
-    (h : ∀ b, ⦃⌜True⌝⦄ f () b ⦃⇓ step => ⌜∀ b', step = .yield b' → measure b' < measure b⌝⦄)
-    : WellFounded (_root_.Lean.Repeat.IsPlausibleStep f) := by
-  apply Subrelation.wf ?_ (_root_.measure measure).wf
-  intro b' b hstep
-  simp_wf
-  simp [_root_.Lean.Repeat.IsPlausibleStep] at hstep
-  have h' : ⊢ₛ wp⟦f () b⟧ (⇓? step => ⌜∀ b', step = .yield b' → measure b' < measure b⌝) := by
-    apply SPred.entails.trans (Triple.iff.mp (h b))
-    apply (wp (f () b)).mono
-    simp [PostCond.entails]
-  exact WPAdequacy.adequate
-    (m := m) (ps := ps) (x := f () b)
-    (P := fun step => ∀ b', step = .yield b' → measure b' < measure b)
-    h' (.yield b') hstep b' rfl
-
-end
-

src/Std/Do/WP.lean

@@ -9,6 +9,5 @@ prelude
 public import Std.Do.WP.Basic
 public import Std.Do.WP.Monad
 public import Std.Do.WP.SimpLemmas
-public import Std.Do.WP.Adequacy
 
 set_option linter.missingDocs true

src/Std/Do/WP/Adequacy.lean

@@ -1,85 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Std.Do.WP.Monad
-import Init.Control.MonadAttach
-
-@[expose] public section
-
-set_option linter.missingDocs true
-
-/-!
-# WP Adequacy
-
-This module provides a small adequacy principle: a `mayThrow` postcondition is enough to recover
-facts about values that `MonadAttach` says can actually be returned.
--/
-
-namespace Std.Do
-
-/-- A small adequacy principle: a `mayThrow` postcondition is enough to recover facts about
-values that `MonadAttach` says can actually be returned. -/
-class WPAdequacy (m : Type u → Type v) (ps : outParam PostShape.{u}) [Monad m] [MonadAttach m]
-    extends WP m ps where
-  /-- If the weakest precondition says that `P` holds for all return values, then `P` holds for
-  any value that `MonadAttach.CanReturn` says can be returned. -/
-  adequate {α : Type u} {x : m α} {P : α → Prop} :
-    (⊢ₛ wp⟦x⟧ (⇓? a => ⌜P a⌝)) → ∀ a, MonadAttach.CanReturn x a → P a
-
-instance : WPAdequacy Id .pure where
-  adequate := by
-    intro α x P hwp a hret
-    have hx : P x.run := by
-      simpa [WP.wp] using hwp
-    simpa [MonadAttach.CanReturn] using (hret ▸ hx)
-
-instance [Monad m] [MonadAttach m] [WPAdequacy m ps] :
-    WPAdequacy (StateT σ m) (.arg σ ps) where
-  adequate := by
-    intro α x P hwp a hret
-    rcases hret with ⟨s, s', hret⟩
-    have hwp' : ⊢ₛ wp⟦x.run s⟧ (⇓? r => ⌜P r.1⌝) := hwp s
-    exact WPAdequacy.adequate (m := m) (ps := ps) (x := x.run s) (P := fun r => P r.1) hwp' (a, s') hret
-
-instance [Monad m] [MonadAttach m] [WPAdequacy m ps] :
-    WPAdequacy (ReaderT ρ m) (.arg ρ ps) where
-  adequate := by
-    intro α x P hwp a hret
-    rcases hret with ⟨r, hret⟩
-    have hwp' : ⊢ₛ wp⟦x.run r⟧ (⇓? a => ⌜P a⌝) := hwp r
-    exact WPAdequacy.adequate (m := m) (ps := ps) (x := x.run r) (P := P) hwp' a hret
-
-instance [Monad m] [MonadAttach m] [WPAdequacy m .pure] :
-    WPAdequacy (ExceptT ε m) (.except ε .pure) where
-  adequate := by
-    intro α x P hwp a hret
-    have hwp0 := hwp
-    simp only [WP.wp, PredTrans.apply_pushExcept, ExceptConds.fst_true, ExceptConds.snd_true] at hwp0
-    have hwp' : ⊢ₛ wp⟦x.run⟧ (⇓? r => ⌜match r with | .ok a => P a | .error _ => True⌝) := by
-      apply SPred.entails.trans hwp0
-      apply (wp x.run).mono
-      simp [PostCond.entails]
-      intro r <;> cases r <;> simp
-    exact WPAdequacy.adequate (m := m) (ps := .pure) (x := x.run)
-      (P := fun r => match r with | .ok a => P a | .error _ => True) hwp' (.ok a) hret
-
-instance [Monad m] [MonadAttach m] [WPAdequacy m .pure] :
-    WPAdequacy (OptionT m) (.except PUnit .pure) where
-  adequate := by
-    intro α x P hwp a hret
-    have hwp0 := hwp
-    simp only [WP.wp, PredTrans.apply_pushOption, ExceptConds.fst_true, ExceptConds.snd_true] at hwp0
-    have hwp' : ⊢ₛ wp⟦x.run⟧ (⇓? r => ⌜match r with | some a => P a | none => True⌝) := by
-      apply SPred.entails.trans hwp0
-      apply (wp x.run).mono
-      simp [PostCond.entails]
-      intro r <;> cases r <;> simp
-    exact WPAdequacy.adequate (m := m) (ps := .pure) (x := x.run)
-      (P := fun r => match r with | some a => P a | none => True) hwp' (some a) hret
-
-end Std.Do

src/Std/Internal.lean

@@ -10,6 +10,7 @@ public import Std.Internal.Async
 public import Std.Internal.Http
 public import Std.Internal.Parsec
 public import Std.Internal.UV
+public import Std.Internal.SSL
 
 @[expose] public section
 

src/Std/Internal/Async.lean

@@ -10,6 +10,7 @@ public import Std.Internal.Async.Basic
 public import Std.Internal.Async.ContextAsync
 public import Std.Internal.Async.Timer
 public import Std.Internal.Async.TCP
+public import Std.Internal.Async.TCP.SSL
 public import Std.Internal.Async.UDP
 public import Std.Internal.Async.DNS
 public import Std.Internal.Async.Select
@@ -17,3 +18,4 @@ public import Std.Internal.Async.Process
 public import Std.Internal.Async.System
 public import Std.Internal.Async.Signal
 public import Std.Internal.Async.IO
+public import Std.Internal.SSL

src/Std/Internal/Async/Basic.lean

@@ -487,8 +487,6 @@ instance : Monad BaseAsync where
   pure := BaseAsync.pure
   bind := BaseAsync.bind
 
-instance : MonadAttach BaseAsync := .trivial
-
 instance : MonadLift BaseIO BaseAsync where
   monadLift := BaseAsync.lift
 
@@ -709,8 +707,6 @@ instance : Monad (EAsync ε) where
   pure := EAsync.pure
   bind := EAsync.bind
 
-instance : MonadAttach (EAsync ε) := .trivial
-
 instance : MonadLift (EIO ε) (EAsync ε) where
   monadLift := EAsync.lift
 

src/Std/Internal/Async/TCP.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.TCP
+public import Std.Internal.Async.IO
 public import Std.Internal.Async.Select
 
 public section

src/Std/Internal/Async/TCP/SSL.lean

@@ -0,0 +1,442 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.UV.TCP
+public import Std.Internal.Async.Timer
+public import Std.Internal.Async.Select
+public import Std.Internal.SSL
+
+public section
+
+namespace Std.Internal.IO.Async.TCP.SSL
+
+open Std.Internal.SSL
+open Std.Internal.UV.TCP
+open Std.Net
+
+/--
+Default chunk size used by TLS I/O loops.
+-/
+def ioChunkSize : UInt64 := 16 * 1024
+
+-- ## Private helpers: SSL ↔ TCP I/O bridge
+
+/--
+Feeds an encrypted chunk into the SSL input BIO.
+Raises an error if OpenSSL consumed fewer bytes than supplied.
+-/
+@[inline]
+private def feedEncryptedChunk (ssl : Session r) (encrypted : ByteArray) : IO Unit := do
+  if encrypted.size == 0 then return ()
+  let consumed ← ssl.feedEncrypted encrypted
+  if consumed.toNat != encrypted.size then
+    throw <| IO.userError s!"TLS input short write: consumed {consumed} / {encrypted.size} bytes"
+
+/--
+Drains all pending encrypted bytes from the SSL output BIO and sends them over TCP.
+-/
+private partial def flushEncrypted (native : Socket) (ssl : Session r) : Async Unit := do
+  let out ← ssl.drainEncrypted
+  if out.size == 0 then return ()
+  Async.ofPromise <| native.send #[out]
+  flushEncrypted native ssl
+
+/--
+Runs the TLS handshake loop to completion, interleaving SSL state machine steps
+with TCP I/O.
+-/
+private partial def doHandshake (native : Socket) (ssl : Session r) (chunkSize : UInt64) : Async Unit := do
+  let want ← ssl.handshake
+  flushEncrypted native ssl
+  match want with
+  | none =>
+    return ()
+  | some .write =>
+    doHandshake native ssl chunkSize
+  | some .read =>
+    let encrypted? ← Async.ofPromise <| native.recv? chunkSize
+    match encrypted? with
+    | none =>
+      throw <| IO.userError "connection closed during TLS handshake"
+    | some encrypted =>
+      feedEncryptedChunk ssl encrypted
+      doHandshake native ssl chunkSize
+
+-- ## Types
+
+/--
+Represents a TLS-enabled TCP server socket. Carries its own server context so
+that each accepted connection gets a session configured from the same context.
+-/
+structure Server where
+  private ofNative ::
+    native : Socket
+    serverCtx : Context.Server
+
+/--
+Represents a TLS-enabled TCP connection, parameterized by TLS role.
+Use `Client` for outgoing connections and `ServerConn` for server-accepted connections.
+-/
+structure Connection (r : Role) where
+  private ofNative ::
+    native : Socket
+    ssl : Session r
+
+/--
+An outgoing TLS client connection.
+-/
+abbrev Client := Connection .client
+
+/--
+An incoming TLS connection accepted by a `Server`.
+-/
+abbrev ServerConn := Connection .server
+
+namespace Server
+
+/--
+Creates a new TLS-enabled TCP server socket using the given context.
+-/
+@[inline]
+def mk (serverCtx : Context.Server) : IO Server := do
+  let native ← Socket.new
+  return Server.ofNative native serverCtx
+
+/--
+Configures the server context with a PEM certificate and private key.
+-/
+@[inline]
+def configureServer (s : Server) (certFile keyFile : String) : IO Unit :=
+  s.serverCtx.configure certFile keyFile
+
+/--
+Binds the server socket to the specified address.
+-/
+@[inline]
+def bind (s : Server) (addr : SocketAddress) : IO Unit :=
+  s.native.bind addr
+
+/--
+Listens for incoming connections with the given backlog.
+-/
+@[inline]
+def listen (s : Server) (backlog : UInt32) : IO Unit :=
+  s.native.listen backlog
+
+@[inline] private def mkServerConn (native : Socket) (ctx : Context.Server) : IO ServerConn := do
+  let ssl ← Session.Server.mk ctx
+  return ⟨native, ssl⟩
+
+/--
+Accepts an incoming TLS connection and performs the TLS handshake.
+-/
+@[inline]
+def accept (s : Server) (chunkSize : UInt64 := ioChunkSize) : Async ServerConn := do
+  let native ← Async.ofPromise <| s.native.accept
+  let conn ← mkServerConn native s.serverCtx
+  doHandshake conn.native conn.ssl chunkSize
+  return conn
+
+/--
+Creates a `Selector` that resolves once `s` has a connection available and the TLS handshake
+has completed.
+-/
+def acceptSelector (s : Server) : Selector ServerConn :=
+  {
+    tryFn := do
+      let res ← s.native.tryAccept
+      match ← IO.ofExcept res with
+      | none => return none
+      | some native =>
+        let conn ← mkServerConn native s.serverCtx
+        doHandshake conn.native conn.ssl ioChunkSize
+        return some conn
+
+    registerFn waiter := do
+      let connTask ← (do
+        let native ← Async.ofPromise <| s.native.accept
+        let ssl ← Session.Server.mk s.serverCtx
+        let conn : ServerConn := ⟨native, ssl⟩
+        doHandshake conn.native conn.ssl ioChunkSize
+        return conn
+      ).asTask
+
+      -- If we get cancelled the promise will be dropped so prepare for that
+      discard <| IO.mapTask (t := connTask) fun res => do
+        let lose := return ()
+        let win promise := do
+          try
+            let conn ← IO.ofExcept res
+            promise.resolve (.ok conn)
+          catch e =>
+            promise.resolve (.error e)
+        waiter.race lose win
+
+    unregisterFn := s.native.cancelAccept
+  }
+
+/--
+Gets the local address of the server socket.
+-/
+@[inline]
+def getSockName (s : Server) : IO SocketAddress :=
+  s.native.getSockName
+
+/--
+Disables the Nagle algorithm for all client sockets accepted by this server socket.
+-/
+@[inline]
+def noDelay (s : Server) : IO Unit :=
+  s.native.noDelay
+
+/--
+Enables TCP keep-alive for all client sockets accepted by this server socket.
+-/
+@[inline]
+def keepAlive (s : Server) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val ≥ 1 := by decide) : IO Unit :=
+  s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
+
+end Server
+
+namespace Connection
+
+/--
+Attempts to write plaintext data into TLS. Returns true when accepted.
+Any encrypted TLS output generated is flushed to the socket.
+-/
+@[inline]
+def write {r : Role} (s : Connection r) (data : ByteArray) : Async Bool := do
+  match ← s.ssl.write data with
+  | none =>
+    flushEncrypted s.native s.ssl
+    return true
+  | some _ =>
+    -- Data was queued internally; flush whatever the SSL engine produced.
+    flushEncrypted s.native s.ssl
+    return false
+
+/--
+Sends data through a TLS-enabled socket.
+Fails if OpenSSL reports the write as pending additional I/O.
+-/
+@[inline]
+def send {r : Role} (s : Connection r) (data : ByteArray) : Async Unit := do
+  if ← s.write data then
+    return ()
+  else
+    throw <| IO.userError "TLS write is pending additional I/O; call `recv?` or retry later"
+
+/--
+Sends multiple data buffers through the TLS-enabled socket.
+-/
+@[inline]
+def sendAll {r : Role} (s : Connection r) (data : Array ByteArray) : Async Unit :=
+  data.forM (s.send ·)
+
+/--
+Receives decrypted plaintext data from TLS.
+If no plaintext is immediately available, this function performs the required socket I/O
+(flush or receive) and retries until data arrives or the connection is closed.
+-/
+partial def recv? {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option ByteArray) := do
+  match ← s.ssl.read? size with
+  | .data plain =>
+    flushEncrypted s.native s.ssl
+    return some plain
+  | .closed =>
+    return none
+  | .wantIO _ =>
+    flushEncrypted s.native s.ssl
+    let encrypted? ← Async.ofPromise <| s.native.recv? chunkSize
+    match encrypted? with
+    | none =>
+      return none
+    | some encrypted =>
+      feedEncryptedChunk s.ssl encrypted
+      recv? s size chunkSize
+
+/--
+Tries to receive decrypted plaintext data without blocking.
+Returns `some (some data)` if plaintext is available, `some none` if the peer closed,
+or `none` if no data is ready yet.
+-/
+partial def tryRecv {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option (Option ByteArray)) := do
+  let pending ← s.ssl.pendingPlaintext
+
+  if pending > 0 then
+    return some (← s.recv? size)
+  else
+    let readableWaiter ← s.native.waitReadable
+
+    flushEncrypted s.native s.ssl
+
+    if ← readableWaiter.isResolved then
+      let encrypted? ← Async.ofPromise <| s.native.recv? ioChunkSize
+      match encrypted? with
+      | none =>
+        return none
+      | some encrypted =>
+        feedEncryptedChunk s.ssl encrypted
+        tryRecv s size chunkSize
+    else
+      s.native.cancelRecv
+      return none
+
+/--
+Feeds encrypted socket data into SSL until plaintext is pending.
+Resolves the returned promise once plaintext is available.
+-/
+partial def waitReadable {r : Role} (s : Connection r) : Async Unit := do
+  flushEncrypted s.native s.ssl
+
+  let pending ← s.ssl.pendingPlaintext
+  if pending > 0 then
+    return ()
+
+  if (← s.ssl.pendingPlaintext) > 0 then
+    return ()
+
+  match ← s.ssl.read? 0 with
+  | .data _ =>
+    flushEncrypted s.native s.ssl
+    return ()
+  | .closed =>
+    return ()
+  | .wantIO _ =>
+    flushEncrypted s.native s.ssl
+    let encrypted? ← Async.ofPromise <| s.native.recv? ioChunkSize
+    match encrypted? with
+    | none => return ()
+    | some encrypted =>
+      feedEncryptedChunk s.ssl encrypted
+      waitReadable s
+
+/--
+Creates a `Selector` that resolves once `s` has plaintext data available.
+-/
+def recvSelector {r : Role} (s : Connection r) (size : UInt64) : Selector (Option ByteArray) :=
+  {
+    tryFn := s.tryRecv size
+
+    registerFn waiter := do
+      let readableWaiter ← s.waitReadable.asTask
+
+      -- If we get cancelled the promise will be dropped so prepare for that
+      discard <| IO.mapTask (t := readableWaiter) fun res => do
+        match res with
+        | .error _ => return ()
+        | .ok _ =>
+          let lose := return ()
+          let win promise := do
+            try
+              -- We know that this read should not block.
+              let result ← (s.recv? size).block
+              promise.resolve (.ok result)
+            catch e =>
+              promise.resolve (.error e)
+          waiter.race lose win
+
+    unregisterFn := s.native.cancelRecv
+  }
+
+/--
+Shuts down the write side of the socket.
+-/
+@[inline]
+def shutdown {r : Role} (s : Connection r) : Async Unit :=
+  Async.ofPromise <| s.native.shutdown
+
+/--
+Gets the remote address of the socket.
+-/
+@[inline]
+def getPeerName {r : Role} (s : Connection r) : IO SocketAddress :=
+  s.native.getPeerName
+
+/--
+Gets the local address of the socket.
+-/
+@[inline]
+def getSockName {r : Role} (s : Connection r) : IO SocketAddress :=
+  s.native.getSockName
+
+/--
+Returns the X.509 verification result code for this TLS session.
+-/
+@[inline]
+def verifyResult {r : Role} (s : Connection r) : IO UInt64 :=
+  s.ssl.verifyResult
+
+/--
+Disables the Nagle algorithm for the socket.
+-/
+@[inline]
+def noDelay {r : Role} (s : Connection r) : IO Unit :=
+  s.native.noDelay
+
+/--
+Enables TCP keep-alive with a specified delay for the socket.
+-/
+@[inline]
+def keepAlive {r : Role} (s : Connection r) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val ≥ 0 := by decide) : IO Unit :=
+  s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
+
+end Connection
+
+-- ## Client (outgoing connection setup)
+
+namespace Client
+
+/--
+Creates a new outgoing TLS client connection using the given client context.
+-/
+@[inline]
+def mk (ctx : Context.Client) : IO Client := do
+  let native ← Socket.new
+  let ssl ← Session.Client.mk ctx
+  return ⟨native, ssl⟩
+
+/--
+Configures the given client context.
+`caFile` may be empty to use default trust settings.
+-/
+@[inline]
+def configureContext (ctx : Context.Client) (caFile := "") (verifyPeer := true) : IO Unit :=
+  ctx.configure caFile verifyPeer
+
+/--
+Binds the client socket to the specified address.
+-/
+@[inline]
+def bind (s : Client) (addr : SocketAddress) : IO Unit :=
+  s.native.bind addr
+
+/--
+Sets SNI server name used during the TLS handshake.
+-/
+@[inline]
+def setServerName (s : Client) (host : String) : IO Unit :=
+  Session.Client.setServerName s.ssl host
+
+/--
+Performs the TLS handshake on an established TCP connection.
+-/
+@[inline]
+def handshake (s : Client) (chunkSize : UInt64 := ioChunkSize) : Async Unit :=
+  doHandshake (Connection.native s) (Connection.ssl s) chunkSize
+
+/--
+Connects the client socket to the given address and performs the TLS handshake.
+-/
+@[inline]
+def connect (s : Client) (addr : SocketAddress) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
+  Async.ofPromise <| (Connection.native s).connect addr
+  s.handshake chunkSize
+
+end Std.Internal.IO.Async.TCP.SSL.Client

src/Std/Internal/Http/Data.lean

@@ -14,7 +14,6 @@ public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Headers
 public import Std.Internal.Http.Data.URI
-public import Std.Internal.Http.Data.Body
 
 /-!
 # HTTP Data Types

src/Std/Internal/Http/Data/Body.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Length
-public import Std.Internal.Http.Data.Body.Any
-public import Std.Internal.Http.Data.Body.Stream
-public import Std.Internal.Http.Data.Body.Empty
-public import Std.Internal.Http.Data.Body.Full
-
-public section
-
-/-!
-# Body
-
-This module re-exports all HTTP body types: `Body.Empty`, `Body.Full`, `Body.Stream`,
-`Body.Any`, and `Body.Length`, along with the `Http.Body` typeclass and conversion
-utilities (`ToByteArray`, `FromByteArray`).
--/

src/Std/Internal/Http/Data/Body/Any.lean

@@ -1,83 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Http.Data.Body.Basic
-
-public section
-
-/-!
-# Body.Any
-
-A type-erased body backed by closures. Implements `Http.Body` and can be constructed from any
-type that also implements `Http.Body`. Used as the default handler response body type.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-A type-erased body handle. Operations are stored as closures, making it open to any body type
-that implements `Http.Body`.
--/
-structure Any where
-
-  /--
-  Receives the next body chunk. Returns `none` at end-of-stream.
-  -/
-  recv : Async (Option Chunk)
-
-  /--
-  Closes the body stream.
-  -/
-  close : Async Unit
-
-  /--
-  Returns `true` when the body stream is closed.
-  -/
-  isClosed : Async Bool
-
-  /--
-  Selector that resolves when a chunk is available or EOF is reached.
-  -/
-  recvSelector : Selector (Option Chunk)
-
-  /--
-  Returns the declared size.
-  -/
-  getKnownSize : Async (Option Body.Length)
-
-  /--
-  Sets the size of the body.
-  -/
-  setKnownSize : Option Body.Length → Async Unit
-namespace Any
-
-/--
-Erases a body of any `Http.Body` instance into a `Body.Any`.
--/
-def ofBody [Http.Body α] (body : α) : Any where
-  recv := Http.Body.recv body
-  close := Http.Body.close body
-  isClosed := Http.Body.isClosed body
-  recvSelector := Http.Body.recvSelector body
-  getKnownSize := Http.Body.getKnownSize body
-  setKnownSize := Http.Body.setKnownSize body
-
-end Any
-
-instance : Http.Body Any where
-  recv := Any.recv
-  close := Any.close
-  isClosed := Any.isClosed
-  recvSelector := Any.recvSelector
-  getKnownSize := Any.getKnownSize
-  setKnownSize := Any.setKnownSize
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Basic.lean

@@ -1,102 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Async
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Headers
-public import Std.Internal.Http.Data.Body.Length
-
-public section
-
-/-!
-# Body.Basic
-
-This module defines the `Body` typeclass for HTTP body streams, and shared conversion types
-`ToByteArray` and `FromByteArray` used for encoding and decoding body content.
--/
-
-namespace Std.Http
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-Typeclass for values that can be read as HTTP body streams.
--/
-class Body (α : Type) where
-  /--
-  Receives the next body chunk. Returns `none` at end-of-stream.
-  -/
-  recv : α → Async (Option Chunk)
-
-  /--
-  Closes the body stream.
-  -/
-  close : α → Async Unit
-
-  /--
-  Returns `true` when the body stream is closed.
-  -/
-  isClosed : α → Async Bool
-
-  /--
-  Selector that resolves when a chunk is available or EOF is reached.
-  -/
-  recvSelector : α → Selector (Option Chunk)
-
-  /--
-  Gets the declared size of the body.
-  -/
-  getKnownSize : α → Async (Option Body.Length)
-
-  /--
-  Sets the declared size of a body.
-  -/
-  setKnownSize : α → Option Body.Length → Async Unit
-end Std.Http
-
-namespace Std.Http.Body
-
-/--
-Typeclass for types that can be converted to a `ByteArray`.
--/
-class ToByteArray (α : Type) where
-
-  /--
-  Transforms into a `ByteArray`.
-  -/
-  toByteArray : α → ByteArray
-
-instance : ToByteArray ByteArray where
-  toByteArray := id
-
-instance : ToByteArray String where
-  toByteArray := String.toUTF8
-
-/--
-Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
-message if the bytes are not valid for the target type.
--/
-class FromByteArray (α : Type) where
-
-  /--
-  Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
-  -/
-  fromByteArray : ByteArray → Except String α
-
-instance : FromByteArray ByteArray where
-  fromByteArray := .ok
-
-instance : FromByteArray String where
-  fromByteArray bs :=
-    match String.fromUTF8? bs with
-    | some s => .ok s
-    | none => .error "invalid UTF-8 encoding"
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Empty.lean

@@ -1,116 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
-
-public section
-
-/-!
-# Body.Empty
-
-Represents an always-empty, already-closed body handle.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-An empty body handle.
--/
-structure Empty where
-deriving Inhabited, BEq
-
-namespace Empty
-
-/--
-Receives from an empty body, always returning end-of-stream.
--/
-@[inline]
-def recv (_ : Empty) : Async (Option Chunk) :=
-  pure none
-
-/--
-Closes an empty body (no-op).
--/
-@[inline]
-def close (_ : Empty) : Async Unit :=
-  pure ()
-
-/--
-Empty bodies are always closed for reading.
--/
-@[inline]
-def isClosed (_ : Empty) : Async Bool :=
-  pure true
-
-/--
-Selector that immediately resolves with end-of-stream for an empty body.
--/
-@[inline]
-def recvSelector (_ : Empty) : Selector (Option Chunk) where
-  tryFn := pure (some none)
-  registerFn waiter := do
-    let lose := pure ()
-    let win promise := do
-      promise.resolve (.ok none)
-    waiter.race lose win
-  unregisterFn := pure ()
-
-end Empty
-
-instance : Http.Body Empty where
-  recv := Empty.recv
-  close := Empty.close
-  isClosed := Empty.isClosed
-  recvSelector := Empty.recvSelector
-  getKnownSize _ := pure (some <| .fixed 0)
-  setKnownSize _ _ := pure ()
-
-
-instance : Coe Empty Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Empty) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Empty)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-open Internal.IO.Async
-
-/--
-Builds a request with no body.
--/
-def empty (builder : Builder) : Async (Request Body.Empty) :=
-  pure <| builder.body {}
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response with no body.
--/
-def empty (builder : Builder) : Async (Response Body.Empty) :=
-  pure <| builder.body {}
-
-end Response.Builder

src/Std/Internal/Http/Data/Body/Full.lean

@@ -1,232 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Sync
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
-public import Init.Data.ByteArray
-
-public section
-
-/-!
-# Body.Full
-
-A body backed by a fixed `ByteArray` held in a `Mutex`.
-
-The byte array is consumed at most once: the first call to `recv` atomically takes the data
-and returns it as a single chunk; subsequent calls return `none` (end-of-stream).
-Closing the body discards any unconsumed data.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-A body backed by a fixed, mutex-protected `ByteArray`.
-
-The data is consumed on the first read. Once consumed (or explicitly closed), the body
-behaves as a closed, empty channel.
--/
-structure Full where
-  private mk ::
-  private state : Mutex (Option ByteArray)
-deriving Nonempty
-
-namespace Full
-
-private def takeChunk : AtomicT (Option ByteArray) Async (Option Chunk) := do
-  match ← get with
-  | none =>
-    pure none
-  | some data =>
-    set (none : Option ByteArray)
-    if data.isEmpty then
-      pure none
-    else
-      pure (some (Chunk.ofByteArray data))
-
-/--
-Creates a `Full` body from a `ByteArray`.
--/
-def ofByteArray (data : ByteArray) : Async Full := do
-  let state ← Mutex.new (some data)
-  return { state }
-
-/--
-Creates a `Full` body from a `String`.
--/
-def ofString (data : String) : Async Full := do
-  let state ← Mutex.new (some data.toUTF8)
-  return { state }
-
-/--
-Receives the body data. Returns the full byte array on the first call as a single chunk,
-then `none` on all subsequent calls.
--/
-def recv (full : Full) : Async (Option Chunk) :=
-  full.state.atomically do
-    takeChunk
-
-/--
-Closes the body, discarding any unconsumed data.
--/
-def close (full : Full) : Async Unit :=
-  full.state.atomically do
-    set (none : Option ByteArray)
-
-/--
-Returns `true` when the data has been consumed or the body has been closed.
--/
-def isClosed (full : Full) : Async Bool :=
-  full.state.atomically do
-    return (← get).isNone
-
-/--
-Returns the known size of the remaining data.
-Returns `some (.fixed n)` with the current byte count, or `some (.fixed 0)` if the body has
-already been consumed or closed.
--/
-def getKnownSize (full : Full) : Async (Option Body.Length) :=
-  full.state.atomically do
-    match ← get with
-    | none => pure (some (.fixed 0))
-    | some data => pure (some (.fixed data.size))
-
-/--
-Selector that immediately resolves to the remaining chunk (or EOF).
--/
-def recvSelector (full : Full) : Selector (Option Chunk) where
-  tryFn := do
-    let chunk ← full.state.atomically do
-      takeChunk
-    pure (some chunk)
-
-  registerFn waiter := do
-    full.state.atomically do
-      let lose := pure ()
-
-      let win promise := do
-        let chunk ← takeChunk
-        promise.resolve (.ok chunk)
-
-      waiter.race lose win
-
-  unregisterFn := pure ()
-
-end Full
-
-instance : Http.Body Full where
-  recv := Full.recv
-  close := Full.close
-  isClosed := Full.isClosed
-  recvSelector := Full.recvSelector
-  getKnownSize := Full.getKnownSize
-  setKnownSize _ _ := pure ()
-
-instance : Coe Full Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Full) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Full)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-
-open Internal.IO.Async
-
-/--
-Builds a request body from raw bytes without setting any headers.
-Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
--/
-def fromBytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) := do
-  return builder.body (← Body.Full.ofByteArray content)
-
-/--
-Builds a request with a binary body.
-Sets `Content-Type: application/octet-stream`.
-Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
--/
-def bytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
-
-/--
-Builds a request with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
--/
-def text (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
-
-/--
-Builds a request with a JSON body.
-Sets `Content-Type: application/json`.
--/
-def json (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
-
-/--
-Builds a request with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
--/
-def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response body from raw bytes without setting any headers.
-Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
--/
-def fromBytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) := do
-  return builder.body (← Body.Full.ofByteArray content)
-
-/--
-Builds a response with a binary body.
-Sets `Content-Type: application/octet-stream`.
-Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
--/
-def bytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
-
-/--
-Builds a response with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
--/
-def text (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
-
-/--
-Builds a response with a JSON body.
-Sets `Content-Type: application/json`.
--/
-def json (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
-
-/--
-Builds a response with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
--/
-def html (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
-
-end Response.Builder

src/Std/Internal/Http/Data/Body/Length.lean

@@ -1,60 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Init.Data.Repr
-
-public section
-
-/-!
-# Body.Length
-
-This module defines the `Length` type, that represents the Content-Length or Transfer-Encoding
-of an HTTP request or response.
--/
-
-namespace Std.Http.Body
-
-set_option linter.all true
-
-/--
-Size of the body of a response or request.
--/
-inductive Length
-  /--
-  Indicates that the HTTP message body uses **chunked transfer encoding**.
-  -/
-  | chunked
-
-  /--
-  Indicates that the HTTP message body has a **fixed, known length**, as specified by the
-  `Content-Length` header.
-  -/
-  | fixed (n : Nat)
-deriving Repr, BEq
-
-namespace Length
-
-/--
-Checks if the `Length` is chunked.
--/
-@[inline]
-def isChunked : Length → Bool
-  | .chunked => true
-  | _ => false
-
-/--
-Checks if the `Length` is a fixed size.
--/
-@[inline]
-def isFixed : Length → Bool
-  | .fixed _ => true
-  | _ => false
-
-end Length
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Stream.lean

@@ -1,650 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Sync
-public import Std.Internal.Async
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Any
-public import Init.Data.ByteArray
-
-public section
-
-/-!
-# Body.Stream
-
-This module defines a zero-buffer rendezvous body channel (`Body.Stream`) that supports
-both sending and receiving chunks.
-
-There is no queue and no capacity. A send waits for a receiver and a receive waits for a sender.
-At most one blocked producer and one blocked consumer are supported.
--/
-
-namespace Std.Http
-
-namespace Body
-
-open Std Internal IO Async
-
-set_option linter.all true
-
-namespace Channel
-
-open Internal.IO.Async in
-private inductive Consumer where
-  | normal (promise : IO.Promise (Option Chunk))
-  | select (finished : Waiter (Option Chunk))
-
-private def Consumer.resolve (c : Consumer) (x : Option Chunk) : BaseIO Bool := do
-  match c with
-  | .normal promise =>
-    promise.resolve x
-    return true
-  | .select waiter =>
-    let lose := return false
-    let win promise := do
-      promise.resolve (.ok x)
-      return true
-    waiter.race lose win
-
-private structure Producer where
-  chunk : Chunk
-
-  /--
-  Resolved with `true` when consumed by a receiver, `false` when the channel closes.
-  -/
-  done : IO.Promise Bool
-
-open Internal.IO.Async in
-private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
-  let lose := return false
-  let win promise := do
-    promise.resolve (.ok x)
-    return true
-  waiter.race lose win
-
-private structure State where
-  /--
-  A single blocked producer waiting for a receiver.
-  -/
-  pendingProducer : Option Producer
-
-  /--
-  A single blocked consumer waiting for a producer.
-  -/
-  pendingConsumer : Option Consumer
-
-  /--
-  A waiter for `Stream.interestSelector`.
-  -/
-  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
-
-  /--
-  Whether the channel is closed.
-  -/
-  closed : Bool
-
-  /--
-  Known size of the stream if available.
-  -/
-  knownSize : Option Body.Length
-
-  /--
-  Buffered partial chunk data accumulated from `Stream.send ... (incomplete := true)`.
-  These partial pieces are collapsed and emitted as a single chunk on the next complete send.
-  -/
-  pendingIncompleteChunk : Option Chunk := none
-deriving Nonempty
-
-end Channel
-
-/--
-A zero-buffer rendezvous body channel that supports both sending and receiving chunks.
--/
-structure Stream where
-  private mk ::
-  private state : Mutex Channel.State
-deriving Nonempty, TypeName
-
-/--
-Creates a rendezvous body stream.
--/
-def mkStream : Async Stream := do
-  let state ← Mutex.new {
-    pendingProducer := none
-    pendingConsumer := none
-    interestWaiter := none
-    closed := false
-    knownSize := none
-  }
-  return { state }
-
-namespace Channel
-
-private def decreaseKnownSize (knownSize : Option Body.Length) (chunk : Chunk) : Option Body.Length :=
-  match knownSize with
-  | some (.fixed res) => some (Body.Length.fixed (res - chunk.data.size))
-  | _ => knownSize
-
-private def pruneFinishedWaiters [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Unit := do
-  let st ← get
-
-  let pendingConsumer ←
-    match st.pendingConsumer with
-    | some (.select waiter) =>
-      if ← waiter.checkFinished then
-        pure none
-      else
-        pure st.pendingConsumer
-    | _ =>
-      pure st.pendingConsumer
-
-  let interestWaiter ←
-    match st.interestWaiter with
-    | some waiter =>
-      if ← waiter.checkFinished then
-        pure none
-      else
-        pure st.interestWaiter
-    | none =>
-      pure none
-
-  set { st with pendingConsumer, interestWaiter }
-
-private def signalInterest [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m Unit := do
-  let st ← get
-  if let some waiter := st.interestWaiter then
-    discard <| resolveInterestWaiter waiter true
-    set { st with interestWaiter := none }
-
-private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Bool := do
-  let st ← get
-  return st.pendingProducer.isSome || st.closed
-
-private def hasInterest' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Bool := do
-  let st ← get
-  return st.pendingConsumer.isSome
-
-private def tryRecv' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m (Option Chunk) := do
-  let st ← get
-  if let some producer := st.pendingProducer then
-    set {
-      st with
-      pendingProducer := none
-      knownSize := decreaseKnownSize st.knownSize producer.chunk
-    }
-    discard <| producer.done.resolve true
-    return some producer.chunk
-  else
-    return none
-
-private def close' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m Unit := do
-  let st ← get
-  if st.closed then
-    return ()
-
-  if let some consumer := st.pendingConsumer then
-    discard <| consumer.resolve none
-
-  if let some waiter := st.interestWaiter then
-    discard <| resolveInterestWaiter waiter false
-
-  if let some producer := st.pendingProducer then
-    discard <| producer.done.resolve false
-
-  set {
-    st with
-    pendingProducer := none
-    pendingConsumer := none
-    interestWaiter := none
-    pendingIncompleteChunk := none
-    closed := true
-  }
-
-end Channel
-
-namespace Stream
-
-/--
-Attempts to receive a chunk from the channel without blocking.
-Returns `some chunk` only when a producer is already waiting.
--/
-def tryRecv (stream : Stream) : Async (Option Chunk) :=
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    Channel.tryRecv'
-
-private def recv' (stream : Stream) : BaseIO (AsyncTask (Option Chunk)) := do
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-
-    if let some chunk ← Channel.tryRecv' then
-      return AsyncTask.pure (some chunk)
-
-    let st ← get
-    if st.closed then
-      return AsyncTask.pure none
-
-    if st.pendingConsumer.isSome then
-      return Task.pure (.error (IO.Error.userError "only one blocked consumer is allowed"))
-
-    let promise ← IO.Promise.new
-    set { st with pendingConsumer := some (.normal promise) }
-    Channel.signalInterest
-    return promise.result?.map (sync := true) fun
-      | none => .error (IO.Error.userError "the promise linked to the consumer was dropped")
-      | some res => .ok res
-
-/--
-Receives a chunk from the channel. Blocks until a producer sends one.
-Returns `none` if the channel is closed and no producer is waiting.
--/
-def recv (stream : Stream) : Async (Option Chunk) := do
-  Async.ofAsyncTask (← recv' stream)
-
-/--
-Closes the channel.
--/
-def close (stream : Stream) : Async Unit :=
-  stream.state.atomically do
-    Channel.close'
-
-/--
-Checks whether the channel is closed.
--/
-@[always_inline, inline]
-def isClosed (stream : Stream) : Async Bool :=
-  stream.state.atomically do
-    return (← get).closed
-
-/--
-Gets the known size if available.
--/
-@[always_inline, inline]
-def getKnownSize (stream : Stream) : Async (Option Body.Length) :=
-  stream.state.atomically do
-    return (← get).knownSize
-
-/--
-Sets known size metadata.
--/
-@[always_inline, inline]
-def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
-  stream.state.atomically do
-    modify fun st => { st with knownSize := size }
-
-open Internal.IO.Async in
-
-/--
-Creates a selector that resolves when a producer is waiting (or the channel closes).
--/
-def recvSelector (stream : Stream) : Selector (Option Chunk) where
-  tryFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      if ← Channel.recvReady' then
-        return some (← Channel.tryRecv')
-      else
-        return none
-
-  registerFn waiter := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      if ← Channel.recvReady' then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok (← Channel.tryRecv'))
-        waiter.race lose win
-      else
-        let st ← get
-        if st.pendingConsumer.isSome then
-          throw (.userError "only one blocked consumer is allowed")
-
-        set { st with pendingConsumer := some (.select waiter) }
-        Channel.signalInterest
-
-  unregisterFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-
-/--
-Iterates over chunks until the channel closes.
--/
-@[inline]
-protected partial def forIn
-    {β : Type} (stream : Stream) (acc : β)
-    (step : Chunk → β → Async (ForInStep β)) : Async β := do
-
-  let rec @[specialize] loop (stream : Stream) (acc : β) : Async β := do
-    if let some chunk ← stream.recv then
-      match ← step chunk acc with
-      | .done res => return res
-      | .yield res => loop stream res
-    else
-      return acc
-
-  loop stream acc
-
-/--
-Context-aware iteration over chunks until the channel closes.
--/
-@[inline]
-protected partial def forIn'
-    {β : Type} (stream : Stream) (acc : β)
-    (step : Chunk → β → ContextAsync (ForInStep β)) : ContextAsync β := do
-
-  let rec @[specialize] loop (stream : Stream) (acc : β) : ContextAsync β := do
-    let data ← Selectable.one #[
-      .case stream.recvSelector pure,
-      .case (← ContextAsync.doneSelector) (fun _ => pure none),
-    ]
-
-    if let some chunk := data then
-      match ← step chunk acc with
-      | .done res => return res
-      | .yield res => loop stream res
-    else
-      return acc
-
-  loop stream acc
-
-/--
-Abstracts over how the next chunk is received, allowing `readAll` to work in both `Async`
-(no cancellation) and `ContextAsync` (races with cancellation via `doneSelector`).
--/
-class NextChunk (m : Type → Type) where
-  /--
-  Receives the next chunk, stopping at EOF or (in `ContextAsync`) when the context is cancelled.
-  -/
-  nextChunk : Stream → m (Option Chunk)
-
-instance : NextChunk Async where
-  nextChunk := Stream.recv
-
-instance : NextChunk ContextAsync where
-  nextChunk stream := do
-    Selectable.one #[
-      .case stream.recvSelector pure,
-      .case (← ContextAsync.doneSelector) (fun _ => pure none),
-    ]
-
-/--
-Reads all remaining chunks and decodes them into `α`.
-
-Works in both `Async` (reads until EOF, no cancellation) and `ContextAsync` (also stops if the
-context is cancelled).
--/
-partial def readAll
-    [FromByteArray α]
-    [Monad m] [MonadExceptOf IO.Error m] [NextChunk m]
-    (stream : Stream)
-    (maximumSize : Option UInt64 := none) :
-    m α := do
-
-  let rec loop (result : ByteArray) : m ByteArray := do
-    match ← NextChunk.nextChunk stream with
-    | none => return result
-    | some chunk =>
-      let result := result ++ chunk.data
-      if let some max := maximumSize then
-        if result.size.toUInt64 > max then
-          throw (.userError s!"body exceeded maximum size of {max} bytes")
-      loop result
-
-  let result ← loop ByteArray.empty
-
-  match FromByteArray.fromByteArray result with
-  | .ok a => return a
-  | .error msg => throw (.userError msg)
-
-private def collapseForSend
-    (stream : Stream)
-    (chunk : Chunk)
-    (incomplete : Bool) : BaseIO (Except IO.Error (Option Chunk)) := do
-
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    let st ← get
-
-    if st.closed then
-      return .error (.userError "channel closed")
-
-    let merged := match st.pendingIncompleteChunk with
-      | some pending =>
-        {
-          data := pending.data ++ chunk.data
-          extensions := if pending.extensions.isEmpty then chunk.extensions else pending.extensions
-        }
-      | none => chunk
-
-    if incomplete then
-      set { st with pendingIncompleteChunk := some merged }
-      return .ok none
-    else
-      set { st with pendingIncompleteChunk := none }
-      return .ok (some merged)
-
-/--
-Sends a chunk, retrying if a select-mode consumer races and loses. If no consumer is ready,
-installs the chunk as a pending producer and awaits acknowledgement from the receiver.
--/
-private partial def send' (stream : Stream) (chunk : Chunk) : Async Unit := do
-  let done ← IO.Promise.new
-  let result : Except IO.Error (Option Bool) ← stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    let st ← get
-
-    if st.closed then
-      return .error (IO.Error.userError "channel closed")
-
-    if let some consumer := st.pendingConsumer then
-      let success ← consumer.resolve (some chunk)
-
-      if success then
-        set {
-          st with
-          pendingConsumer := none
-          knownSize := Channel.decreaseKnownSize st.knownSize chunk
-        }
-        return .ok (some true)
-      else
-        set { st with pendingConsumer := none }
-        return .ok (some false)
-    else if st.pendingProducer.isSome then
-      return .error (IO.Error.userError "only one blocked producer is allowed")
-    else
-      set { st with pendingProducer := some { chunk, done } }
-      return .ok none
-
-  match result with
-  | .error err =>
-    throw err
-  | .ok (some true) =>
-    return ()
-  | .ok (some false) =>
-    -- The select-mode consumer raced and lost; recurse to allocate a fresh `done` promise.
-    send' stream chunk
-  | .ok none =>
-    match ← await done.result? with
-    | some true => return ()
-    | _ => throw (IO.Error.userError "channel closed")
-
-/--
-Sends a chunk.
-
-If `incomplete := true`, the chunk is buffered and collapsed with subsequent chunks, and is not
-delivered to the receiver yet.
-If `incomplete := false`, any buffered incomplete pieces are collapsed with this chunk and the
-single merged chunk is sent.
--/
-def send (stream : Stream) (chunk : Chunk) (incomplete : Bool := false) : Async Unit := do
-  match (← collapseForSend stream chunk incomplete) with
-  | .error err => throw err
-  | .ok none => pure ()
-  | .ok (some toSend) =>
-    if toSend.data.isEmpty ∧ toSend.extensions.isEmpty then
-      return ()
-
-    send' stream toSend
-
-/--
-Returns `true` when a consumer is currently blocked waiting for data.
--/
-def hasInterest (stream : Stream) : Async Bool :=
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    Channel.hasInterest'
-
-open Internal.IO.Async in
-/--
-Creates a selector that resolves when consumer interest is present.
-Returns `true` when a consumer is waiting, `false` when the channel closes first.
--/
-def interestSelector (stream : Stream) : Selector Bool where
-  tryFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      let st ← get
-      if st.pendingConsumer.isSome then
-        return some true
-      else if st.closed then
-        return some false
-      else
-        return none
-
-  registerFn waiter := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      let st ← get
-
-      if st.pendingConsumer.isSome then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok true)
-        waiter.race lose win
-      else if st.closed then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok false)
-        waiter.race lose win
-      else if st.interestWaiter.isSome then
-        throw (.userError "only one blocked interest selector is allowed")
-      else
-        set { st with interestWaiter := some waiter }
-
-  unregisterFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-
-end Stream
-
-/--
-Creates a body from a producer function.
-Returns the stream immediately and runs `gen` in a detached task.
-The channel is always closed when `gen` returns or throws.
-Errors from `gen` are not rethrown here; consumers observe end-of-stream via `recv = none`.
--/
-def stream (gen : Stream → Async Unit) : Async Stream := do
-  let s ← mkStream
-  background <| do
-    try
-      gen s
-    finally
-      s.close
-  return s
-
-/--
-Creates a body from a fixed byte array.
--/
-def fromBytes (content : ByteArray) : Async Stream := do
-  stream fun s => do
-    s.setKnownSize (some (.fixed content.size))
-    if content.size > 0 then
-      s.send (Chunk.ofByteArray content)
-
-/--
-Creates an empty `Stream` body channel (already closed, no data).
-
-Prefer `Body.Empty` when you need a concrete zero-cost type. Use this when the calling
-context requires a `Stream` specifically.
--/
-def empty : Async Stream := do
-  let s ← mkStream
-  s.setKnownSize (some (.fixed 0))
-  s.close
-  return s
-
-instance : ForIn Async Stream Chunk where
-  forIn := Stream.forIn
-
-instance : ForIn ContextAsync Stream Chunk where
-  forIn := Stream.forIn'
-
-instance : Http.Body Stream where
-  recv := Stream.recv
-  close := Stream.close
-  isClosed := Stream.isClosed
-  recvSelector := Stream.recvSelector
-  getKnownSize := Stream.getKnownSize
-  setKnownSize := Stream.setKnownSize
-
-instance : Coe Stream Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Stream) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Stream)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Stream)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-
-open Internal.IO.Async
-
-/--
-Builds a request with a streaming body generator.
--/
-def stream
-    (builder : Builder)
-    (gen : Body.Stream → Async Unit) :
-    Async (Request Body.Stream) := do
-  let s ← Body.stream gen
-  return Request.Builder.body builder s
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response with a streaming body generator.
--/
-def stream
-    (builder : Builder)
-    (gen : Body.Stream → Async Unit) :
-    Async (Response Body.Stream) := do
-  let s ← Body.stream gen
-  return Response.Builder.body builder s
-
-end Response.Builder

src/Std/Internal/Http/Data/Request.lean

@@ -124,6 +124,12 @@ def new : Builder := { }
 
 namespace Builder
 
+/--
+Creates a new HTTP request builder with the default head
+(method: GET, version: HTTP/1.1, target: `*`).
+-/
+def empty : Builder := { }
+
 /--
 Sets the HTTP method for the request being built.
 -/

src/Std/Internal/Http/Data/Response.lean

@@ -111,7 +111,7 @@ namespace Builder
 /--
 Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
-def new : Builder := { }
+def empty : Builder := { }
 
 /--
 Sets the HTTP status code for the response being built.
@@ -173,66 +173,66 @@ end Builder
 Creates a new HTTP Response builder with the 200 status code.
 -/
 def ok : Builder :=
-  .new |>.status .ok
+  .empty |>.status .ok
 
 /--
 Creates a new HTTP Response builder with the provided status.
 -/
 def withStatus (status : Status) : Builder :=
-  .new |>.status status
+  .empty |>.status status
 
 /--
 Creates a new HTTP Response builder with the 404 status code.
 -/
 def notFound : Builder :=
-  .new |>.status .notFound
+  .empty |>.status .notFound
 
 /--
 Creates a new HTTP Response builder with the 500 status code.
 -/
 def internalServerError : Builder :=
-  .new |>.status .internalServerError
+  .empty |>.status .internalServerError
 
 /--
 Creates a new HTTP Response builder with the 400 status code.
 -/
 def badRequest : Builder :=
-  .new |>.status .badRequest
+  .empty |>.status .badRequest
 
 /--
 Creates a new HTTP Response builder with the 201 status code.
 -/
 def created : Builder :=
-  .new |>.status .created
+  .empty |>.status .created
 
 /--
 Creates a new HTTP Response builder with the 202 status code.
 -/
 def accepted : Builder :=
-  .new |>.status .accepted
+  .empty |>.status .accepted
 
 /--
 Creates a new HTTP Response builder with the 401 status code.
 -/
 def unauthorized : Builder :=
-  .new |>.status .unauthorized
+  .empty |>.status .unauthorized
 
 /--
 Creates a new HTTP Response builder with the 403 status code.
 -/
 def forbidden : Builder :=
-  .new |>.status .forbidden
+  .empty |>.status .forbidden
 
 /--
 Creates a new HTTP Response builder with the 409 status code.
 -/
 def conflict : Builder :=
-  .new |>.status .conflict
+  .empty |>.status .conflict
 
 /--
 Creates a new HTTP Response builder with the 503 status code.
 -/
 def serviceUnavailable : Builder :=
-  .new |>.status .serviceUnavailable
+  .empty |>.status .serviceUnavailable
 
 end Response

src/Std/Internal/Http/Data/URI.lean

@@ -94,3 +94,4 @@ def parseOrRoot (s : String) : Std.Http.URI.Path :=
   parse? s |>.getD { segments := #[], absolute := true }
 
 end Std.Http.URI.Path
+

src/Std/Internal/SSL.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.SSL.Context
+public import Std.Internal.SSL.Session

src/Std/Internal/SSL/Context.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.System.Promise
+
+public section
+
+namespace Std.Internal.SSL
+
+/--
+Distinguishes server-side from client-side TLS contexts and sessions at the type level.
+-/
+inductive Role where
+  | server
+  | client
+
+private opaque ContextServerImpl : NonemptyType.{0}
+private opaque ContextClientImpl : NonemptyType.{0}
+
+/--
+Server-side TLS context (`SSL_CTX` configured with `TLS_server_method`).
+-/
+def Context.Server : Type := ContextServerImpl.type
+
+/--
+Client-side TLS context (`SSL_CTX` configured with `TLS_client_method`).
+-/
+def Context.Client : Type := ContextClientImpl.type
+
+instance : Nonempty Context.Server := ContextServerImpl.property
+instance : Nonempty Context.Client := ContextClientImpl.property
+
+namespace Context
+
+namespace Server
+
+/--
+Creates a new server-side TLS context using `TLS_server_method`.
+-/
+@[extern "lean_uv_ssl_ctx_mk_server"]
+opaque mk : IO Context.Server
+
+/--
+Loads a PEM certificate and private key into a server context.
+-/
+@[extern "lean_uv_ssl_ctx_configure_server"]
+opaque configure (ctx : @& Context.Server) (certFile : @& String) (keyFile : @& String) : IO Unit
+
+end Server
+
+namespace Client
+
+/--
+Creates a new client-side TLS context using `TLS_client_method`.
+-/
+@[extern "lean_uv_ssl_ctx_mk_client"]
+opaque mk : IO Context.Client
+
+/--
+Configures CA trust anchors and peer verification for a client context.
+`caFile` may be empty to use platform default trust anchors.
+-/
+@[extern "lean_uv_ssl_ctx_configure_client"]
+opaque configure (ctx : @& Context.Client) (caFile : @& String) (verifyPeer : Bool) : IO Unit
+
+end Client
+
+end Context
+
+end Std.Internal.SSL

src/Std/Internal/SSL/Session.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.SSL.Context
+
+public section
+
+namespace Std.Internal.SSL
+
+private opaque SessionImpl : Role → NonemptyType.{0}
+
+/--
+Indicates what kind of socket I/O OpenSSL needs before the current operation can proceed.
+-/
+inductive IOWant where
+
+  /--
+  OpenSSL needs more encrypted bytes from the socket (`SSL_ERROR_WANT_READ`).
+  -/
+  | read
+
+  /--
+  OpenSSL needs to flush encrypted bytes to the socket (`SSL_ERROR_WANT_WRITE`).
+  -/
+  | write
+
+/--
+Result of a `Session.read?` call.
+-/
+inductive ReadResult where
+
+  /--
+  Plaintext data was successfully decrypted.
+  -/
+  | data (bytes : ByteArray)
+
+  /--
+  OpenSSL needs socket I/O before it can produce plaintext.
+  -/
+  | wantIO (want : IOWant)
+
+  /--
+  The peer closed the TLS session cleanly (`SSL_ERROR_ZERO_RETURN`).
+  -/
+  | closed
+
+/--
+Represents an OpenSSL SSL session parameterized by role.
+Use `Session.Server` or `Session.Client` for the concrete aliases.
+-/
+def Session (r : Role) : Type := (SessionImpl r).type
+
+/--
+Server-side TLS session.
+-/
+abbrev Session.Server := Session .server
+
+/--
+Client-side TLS session.
+-/
+abbrev Session.Client := Session .client
+
+instance (r : Role) : Nonempty (Session r) := (SessionImpl r).property
+
+namespace Session
+
+namespace Server
+
+/--
+Creates a new server-side SSL session from the given context.
+-/
+@[extern "lean_uv_ssl_mk_server"]
+opaque mk (ctx : @& Context.Server) : IO Session.Server
+
+end Server
+
+namespace Client
+
+/--
+Creates a new client-side SSL session from the given context.
+-/
+@[extern "lean_uv_ssl_mk_client"]
+opaque mk (ctx : @& Context.Client) : IO Session.Client
+
+/--
+Sets the SNI host name for client-side handshakes.
+-/
+@[extern "lean_uv_ssl_set_server_name"]
+opaque setServerName (ssl : @& Session.Client) (host : @& String) : IO Unit
+
+end Client
+
+/--
+Gets the X.509 verify result code after handshake.
+-/
+@[extern "lean_uv_ssl_verify_result"]
+opaque verifyResult {r : Role} (ssl : @& Session r) : IO UInt64
+
+/--
+Runs one handshake step.
+Returns `none` when the handshake is complete, or `some w` when OpenSSL needs socket I/O of
+kind `w` before the handshake can proceed.
+-/
+@[extern "lean_uv_ssl_handshake"]
+opaque handshake {r : Role} (ssl : @& Session r) : IO (Option IOWant)
+
+/--
+Attempts to write plaintext application data into SSL.
+Returns `none` when the data was accepted, or `some w` when OpenSSL needs socket I/O of kind
+`w` before the write can complete (the data is queued internally and retried after the next read).
+-/
+@[extern "lean_uv_ssl_write"]
+opaque write {r : Role} (ssl : @& Session r) (data : @& ByteArray) : IO (Option IOWant)
+
+/--
+Attempts to read decrypted plaintext data.
+-/
+@[extern "lean_uv_ssl_read"]
+opaque read? {r : Role} (ssl : @& Session r) (maxBytes : UInt64) : IO ReadResult
+
+/--
+Feeds encrypted TLS bytes into the SSL input BIO.
+-/
+@[extern "lean_uv_ssl_feed_encrypted"]
+opaque feedEncrypted {r : Role} (ssl : @& Session r) (data : @& ByteArray) : IO UInt64
+
+/--
+Drains encrypted TLS bytes from the SSL output BIO.
+-/
+@[extern "lean_uv_ssl_drain_encrypted"]
+opaque drainEncrypted {r : Role} (ssl : @& Session r) : IO ByteArray
+
+/--
+Returns the amount of encrypted TLS bytes currently pending in the output BIO.
+-/
+@[extern "lean_uv_ssl_pending_encrypted"]
+opaque pendingEncrypted {r : Role} (ssl : @& Session r) : IO UInt64
+
+/--
+Returns the amount of decrypted plaintext bytes currently buffered inside the SSL object.
+-/
+@[extern "lean_uv_ssl_pending_plaintext"]
+opaque pendingPlaintext {r : Role} (ssl : @& Session r) : IO UInt64
+
+end Session
+
+end Std.Internal.SSL

src/Std/Tactic/Do.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Std.Tactic.Do.ProofMode
 public import Std.Tactic.Do.Syntax
-public import Std.Do.Triple.RepeatSpec
 
 @[expose] public section
 

src/lake/Lake/CLI/Help.lean

@@ -386,7 +386,7 @@ OPTIONS:
   --force-download                redownload existing files
 
 Downloads build outputs for packages in the workspace from a remote cache
-service. The cache service used can be specified via the `--service` option.
+service. The cache service used can be specifed via the `--service` option.
 Otherwise, Lake will the system default, or, if none is configured, Reservoir.
 See `lake cache services` for more information on how to configure services.
 
@@ -429,7 +429,7 @@ USAGE:
 
 Uploads the input-to-output mappings contained in the specified file along
 with the corresponding output artifacts to a remote cache. The cache service
-used can be specified via the `--service` option. If not specified, Lake will use
+used via be specified via `--service` option. If not specifed, Lake will used
 the system default, or error if none is configured. See the help page of
 `lake cache services` for more information on how to configure services.
 

src/lake/Lake/CLI/Main.lean

@@ -446,7 +446,7 @@ protected def get : CliM PUnit := do
           logWarning endpointDeprecation
           if opts.mappingsOnly then
             error "`--mappings-only` requires services to be configured
-              via the Lake system configuration (not environment variables)"
+              via the Lake system configuration (not enviroment variables)"
           return .downloadService artifactEndpoint revisionEndpoint ws.lakeEnv.cacheService?
         | none, none =>
             return ws.defaultCacheService

src/lake/Lake/Config/Cache.lean

@@ -765,13 +765,12 @@ where
       \n  remote URL: {info.url}"
     match cfg.kind with
     | .get =>
-      unless code? matches .ok 404 do -- ignore response bodies on 404s
-        if let .ok size := out.getAs Nat "size_download" then
-          if size > 0 then
-            if let .ok contentType := out.getAs String "content_type" then
-              if contentType != artifactContentType then
-                if let .ok resp ← IO.FS.readFile info.path |>.toBaseIO then
-                  msg := s!"{msg}\nunexpected response:\n{resp}"
+      if let .ok size := out.getAs Nat "size_download" then
+        if size > 0 then
+          if let .ok contentType := out.getAs String "content_type" then
+            if contentType != artifactContentType then
+              if let .ok resp ← IO.FS.readFile info.path |>.toBaseIO then
+                msg := s!"{msg}\nunexpected response:\n{resp}"
       removeFileIfExists info.path
     | .put =>
       if let .ok size := out.getAs Nat "size_download" then
@@ -788,7 +787,7 @@ private def transferArtifacts
     match cfg.kind with
     | .get =>
       cfg.infos.forM fun info => do
-        h.putStrLn s!"url = {info.url.quote}"
+        h.putStrLn s!"url = {info.url}"
         h.putStrLn s!"-o {info.path.toString.quote}"
       h.flush
       return #[
@@ -799,7 +798,7 @@ private def transferArtifacts
     | .put =>
       cfg.infos.forM fun info => do
         h.putStrLn s!"-T {info.path.toString.quote}"
-        h.putStrLn s!"url = {info.url.quote}"
+        h.putStrLn s!"url = {info.url}"
       h.flush
       return #[
         "-Z", "-X", "PUT", "-L",
@@ -828,13 +827,6 @@ private def transferArtifacts
   if s.didError then
     failure
 
-private def reservoirArtifactsUrl (service : CacheService) (scope : CacheServiceScope) : String :=
-  let endpoint :=
-    match scope.impl with
-    | .repo scope => appendScope s!"{service.impl.apiEndpoint}/repositories" scope
-    | .str scope => appendScope s!"{service.impl.apiEndpoint}/packages" scope
-  s!"{endpoint}/artifacts"
-
 public def downloadArtifacts
    (descrs : Array ArtifactDescr) (cache : Cache)
    (service : CacheService) (scope : CacheServiceScope) (force := false)
@@ -852,68 +844,8 @@ public def downloadArtifacts
     return s.push {url, path, descr}
   if infos.isEmpty then
     return
-  let infos ← id do
-    if service.isReservoir then
-      -- Artifact cloud storage URLs are fetched in a single request
-      -- to avoid hammering the Reservoir web host
-      fetchUrls (service.reservoirArtifactsUrl scope) infos
-    else return infos
   IO.FS.createDirAll cache.artifactDir
   transferArtifacts {scope, infos, kind := .get}
-where
-  fetchUrls url infos := IO.FS.withTempFile fun h path => do
-    let body := Json.arr <| infos.map (toJson ·.descr.hash)
-    h.putStr body.compress
-    h.flush
-    let args := #[
-        "-X", "POST", "-L", "-d", s!"@{path}",
-        "--retry", "3", -- intermittent network errors can occur
-        "-s", "-w", "%{stderr}%{json}\n",
-        "-H", "Content-Type: application/json",
-      ]
-    let args := Reservoir.lakeHeaders.foldl (· ++ #["-H", ·]) args
-    let spawnArgs := {
-      cmd := "curl", args := args.push url
-      stdout := .piped, stderr := .piped
-    }
-    logVerbose (mkCmdLog spawnArgs)
-    let {stdout, stderr, exitCode} ← IO.Process.output spawnArgs
-    match Json.parse stdout >>= fromJson? with
-    | .ok (resp :  ReservoirResp (Array String)) =>
-      match resp with
-      | .data urls =>
-        if h : infos.size = urls.size then
-          let s := infos.size.fold (init := infos.toVector) fun i hi s =>
-            s.set i {s[i] with url := urls[i]'(h ▸ hi)}
-          return s.toArray
-        else
-          error s!"failed to fetch artifact URLs\
-          \n  POST {url}\
-          \nIncorrect number of results: expected {infos.size}, got {urls.size}"
-      | .error status message =>
-        error s!"failed to fetch artifact URLs (status code: {status})\
-          \n  POST {url}\
-          \nReservoir error: {message}"
-    | .error _ =>
-      match Json.parse stderr >>= fromJson? with
-      | .ok (out : JsonObject) =>
-        let mut msg := "failed to fetch artifact URLs"
-        if let .ok code := out.getAs Nat "http_code" then
-          msg := s!"{msg} (status code: {code})"
-        msg := s!"{msg}\n  POST {url}"
-        if let .ok errMsg := out.getAs String "errormsg" then
-          msg := s!"{msg}\n  Transfer error: {errMsg}"
-        unless stdout.isEmpty do
-          msg := s!"{msg}\nstdout:\n{stdout.trimAsciiEnd}"
-        logError msg
-        logVerbose s!"curl JSON:\n{stderr.trimAsciiEnd}"
-      | .error e =>
-        logError s!"failed to fetch artifact URLs\
-          \n  POST {url}
-          \nInvalid curl JSON: {e}; received: {stderr.trimAscii}"
-        unless stdout.isEmpty do
-          logWarning s!"curl produced unexpected output:\n{stdout.trimAsciiEnd}"
-      error s!"curl exited with code {exitCode}"
 
 @[deprecated "Deprecated without replacement." (since := "2026-02-27")]
 public def downloadOutputArtifacts

src/lake/Lake/Reservoir.lean

@@ -103,6 +103,24 @@ public instance : FromJson RegistryPkg := ⟨RegistryPkg.fromJson?⟩
 
 end RegistryPkg
 
+/-- A Reservoir API response object. -/
+public inductive ReservoirResp (α : Type u)
+| data (a : α)
+| error (status : Nat) (message : String)
+
+public protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String (ReservoirResp α) := do
+  let obj ← JsonObject.fromJson? val
+  if let some (err : JsonObject) ← obj.get? "error" then
+    let status ← err.get "status"
+    let message ← err.get "message"
+    return .error status message
+  else if let some (val : Json) ← obj.get? "data" then
+    .data <$> fromJson? val
+  else
+    .data <$> fromJson? val
+
+public instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩
+
 public def Reservoir.pkgApiUrl (lakeEnv : Lake.Env) (owner pkg : String) :=
    s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
 

src/lake/Lake/Util/Reservoir.lean

@@ -6,9 +6,8 @@ Authors: Mac Malone
 module
 
 prelude
-public import Lake.Util.JsonObject
-
-open Lean
+public import Init.Prelude
+import Init.Data.Array.Basic
 
 namespace Lake
 
@@ -16,23 +15,3 @@ public def Reservoir.lakeHeaders : Array String := #[
   "X-Reservoir-Api-Version:1.0.0",
   "X-Lake-Registry-Api-Version:0.1.0"
 ]
-
-/-- A Reservoir API response object. -/
-public inductive ReservoirResp (α : Type u)
-| data (a : α)
-| error (status : Nat) (message : String)
-
-public protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String (ReservoirResp α) := do
-  if let .ok obj := JsonObject.fromJson? val then
-    if let some (err : JsonObject) ← obj.get? "error" then
-      let status ← err.get "status"
-      let message ← err.get "message"
-      return .error status message
-    else if let some (val : Json) ← obj.get? "data" then
-      .data <$> fromJson? val
-    else
-      .data <$> fromJson? val
-  else
-    .data <$> fromJson? val
-
-public instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩

src/runtime/CMakeLists.txt

@@ -33,6 +33,9 @@ set(
   uv/dns.cpp
   uv/system.cpp
   uv/signal.cpp
+  openssl.cpp
+  openssl/context.cpp
+  openssl/session.cpp
 )
 if(USE_MIMALLOC)
   list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c)

src/runtime/init_module.cpp

@@ -14,6 +14,9 @@ Author: Leonardo de Moura
 #include "runtime/mutex.h"
 #include "runtime/init_module.h"
 #include "runtime/libuv.h"
+#include "runtime/openssl.h"
+#include "runtime/openssl/context.h"
+#include "runtime/openssl/session.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -25,6 +28,9 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_mutex();
     initialize_process();
     initialize_stack_overflow();
+    initialize_openssl();
+    initialize_openssl_context();
+    initialize_openssl_session();
     initialize_libuv();
 }
 void initialize_runtime_module() {
@@ -32,6 +38,7 @@ void initialize_runtime_module() {
 }
 void finalize_runtime_module() {
     finalize_stack_overflow();
+    finalize_openssl();
     finalize_process();
     finalize_mutex();
     finalize_thread();

src/runtime/openssl.cpp

@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#include "runtime/openssl.h"
+#include "runtime/io.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/opensslv.h>
+#include <openssl/ssl.h>
+#include <openssl/err.h>
+
+namespace lean {
+
+void initialize_openssl() {
+    if (OPENSSL_init_ssl(0, nullptr) != 1) {
+        lean_internal_panic("failed to initialize OpenSSL");
+    }
+}
+
+void finalize_openssl() {}
+
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
+    return lean_unsigned_to_nat(OPENSSL_VERSION_NUMBER);
+}
+
+#else
+
+namespace lean {
+
+void initialize_openssl() {}
+void finalize_openssl() {}
+
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
+    return lean_box(0);
+}
+
+#endif

src/runtime/openssl.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#pragma once
+#include <lean/lean.h>
+
+namespace lean {
+
+void initialize_openssl();
+void finalize_openssl();
+
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);

src/runtime/openssl/context.cpp

@@ -0,0 +1,148 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+
+#include "runtime/openssl/context.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/err.h>
+#endif
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+static inline lean_obj_res mk_ssl_ctx_io_error(char const * where) {
+    unsigned long err = ERR_get_error();
+    char err_buf[256];
+    err_buf[0] = '\0';
+
+    if (err != 0) {
+        ERR_error_string_n(err, err_buf, sizeof(err_buf));
+    }
+
+    ERR_clear_error();
+
+    std::string msg(where);
+    if (err_buf[0] != '\0') {
+        msg += ": ";
+        msg += err_buf;
+    }
+
+    return lean_io_result_mk_error(lean_mk_io_user_error(mk_string(msg.c_str())));
+}
+
+static void configure_ctx_options(SSL_CTX * ctx) {
+    SSL_CTX_clear_options(ctx, SSL_OP_NO_RENEGOTIATION);
+}
+
+static void lean_ssl_context_finalizer(void * ptr) {
+    lean_ssl_context_object * obj = (lean_ssl_context_object*)ptr;
+    if (obj->ctx != nullptr) {
+        SSL_CTX_free(obj->ctx);
+    }
+    free(obj);
+}
+
+void initialize_openssl_context() {
+    g_ssl_context_external_class = lean_register_external_class(lean_ssl_context_finalizer, [](void * obj, lean_object * f) {
+        (void)obj;
+        (void)f;
+    });
+}
+
+static lean_obj_res mk_ssl_context(const SSL_METHOD * method) {
+    SSL_CTX * ctx = SSL_CTX_new(method);
+    if (ctx == nullptr) {
+        return mk_ssl_ctx_io_error("SSL_CTX_new failed");
+    }
+
+    configure_ctx_options(ctx);
+
+    lean_ssl_context_object * obj = (lean_ssl_context_object*)malloc(sizeof(lean_ssl_context_object));
+    if (obj == nullptr) {
+        SSL_CTX_free(ctx);
+        return mk_ssl_ctx_io_error("failed to allocate SSL context object");
+    }
+
+    obj->ctx = ctx;
+    lean_object * lean_obj = lean_ssl_context_object_new(obj);
+    lean_mark_mt(lean_obj);
+    return lean_io_result_mk_ok(lean_obj);
+}
+
+/* Std.Internal.SSL.Context.mkServer : IO Context */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server() {
+    return mk_ssl_context(TLS_server_method());
+}
+
+/* Std.Internal.SSL.Context.mkClient : IO Context */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client() {
+    return mk_ssl_context(TLS_client_method());
+}
+
+/* Std.Internal.SSL.Context.configureServer (ctx : @& Context) (certFile keyFile : @& String) : IO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx_obj, b_obj_arg cert_file, b_obj_arg key_file) {
+    lean_ssl_context_object * obj = lean_to_ssl_context_object(ctx_obj);
+    const char * cert = lean_string_cstr(cert_file);
+    const char * key = lean_string_cstr(key_file);
+
+    if (SSL_CTX_use_certificate_file(obj->ctx, cert, SSL_FILETYPE_PEM) <= 0) {
+        return mk_ssl_ctx_io_error("SSL_CTX_use_certificate_file failed");
+    }
+    if (SSL_CTX_use_PrivateKey_file(obj->ctx, key, SSL_FILETYPE_PEM) <= 0) {
+        return mk_ssl_ctx_io_error("SSL_CTX_use_PrivateKey_file failed");
+    }
+    if (SSL_CTX_check_private_key(obj->ctx) != 1) {
+        return mk_ssl_ctx_io_error("SSL_CTX_check_private_key failed");
+    }
+
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+/* Std.Internal.SSL.Context.configureClient (ctx : @& Context) (caFile : @& String) (verifyPeer : Bool) : IO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx_obj, b_obj_arg ca_file, uint8_t verify_peer) {
+    lean_ssl_context_object * obj = lean_to_ssl_context_object(ctx_obj);
+    const char * ca = lean_string_cstr(ca_file);
+
+    if (ca != nullptr && ca[0] != '\0') {
+        if (SSL_CTX_load_verify_locations(obj->ctx, ca, nullptr) != 1) {
+            return mk_ssl_ctx_io_error("SSL_CTX_load_verify_locations failed");
+        }
+    } else if (verify_peer) {
+        if (SSL_CTX_set_default_verify_paths(obj->ctx) != 1) {
+            return mk_ssl_ctx_io_error("SSL_CTX_set_default_verify_paths failed");
+        }
+    }
+
+    SSL_CTX_set_verify(obj->ctx, verify_peer ? SSL_VERIFY_PEER : SSL_VERIFY_NONE, nullptr);
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+#else
+
+void initialize_openssl_context() {}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server() {
+    return io_result_mk_error("lean_uv_ssl_ctx_mk_server is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client() {
+    return io_result_mk_error("lean_uv_ssl_ctx_mk_client is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx_obj, b_obj_arg cert_file, b_obj_arg key_file) {
+    (void)ctx_obj; (void)cert_file; (void)key_file;
+    return io_result_mk_error("lean_uv_ssl_ctx_configure_server is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx_obj, b_obj_arg ca_file, uint8_t verify_peer) {
+    (void)ctx_obj; (void)ca_file; (void)verify_peer;
+    return io_result_mk_error("lean_uv_ssl_ctx_configure_client is not supported");
+}
+
+#endif
+
+}

src/runtime/openssl/context.h

@@ -0,0 +1,40 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#pragma once
+
+#include <lean/lean.h>
+#include "runtime/io.h"
+#include "runtime/object.h"
+#include "runtime/openssl.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/ssl.h>
+#endif
+
+namespace lean {
+
+static lean_external_class * g_ssl_context_external_class = nullptr;
+void initialize_openssl_context();
+
+#ifndef LEAN_EMSCRIPTEN
+typedef struct {
+    SSL_CTX * ctx;
+} lean_ssl_context_object;
+
+static inline lean_object * lean_ssl_context_object_new(lean_ssl_context_object * c) {
+    return lean_alloc_external(g_ssl_context_external_class, c);
+}
+static inline lean_ssl_context_object * lean_to_ssl_context_object(lean_object * o) {
+    return (lean_ssl_context_object*)(lean_get_external_data(o));
+}
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx, b_obj_arg cert_file, b_obj_arg key_file);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx, b_obj_arg ca_file, uint8_t verify_peer);
+
+}

src/runtime/openssl/session.cpp

@@ -0,0 +1,501 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+
+#include "runtime/openssl/session.h"
+
+#include <climits>
+#include <new>
+#include <string>
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/err.h>
+#endif
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+static inline lean_object * mk_ssl_error(char const * where, int ssl_err = 0) {
+    unsigned long err = ERR_get_error();
+    char err_buf[256];
+    err_buf[0] = '\0';
+
+    if (err != 0) {
+        ERR_error_string_n(err, err_buf, sizeof(err_buf));
+    }
+
+    // Drain remaining errors so they don't pollute future calls.
+    ERR_clear_error();
+
+    std::string msg(where);
+
+    if (ssl_err != 0) {
+        msg += " (ssl_error=" + std::to_string(ssl_err) + ")";
+    }
+    if (err_buf[0] != '\0') {
+        msg += ": ";
+        msg += err_buf;
+    }
+
+    return lean_mk_io_user_error(mk_string(msg.c_str()));
+}
+
+static inline lean_obj_res mk_ssl_io_error(char const * where, int ssl_err = 0) {
+    return lean_io_result_mk_error(mk_ssl_error(where, ssl_err));
+}
+
+/*
+ * Lean encoding for `Option IOWant`:
+ *   none            = lean_box(0)               (handshake done / write accepted)
+ *   some IOWant.read  = ctor(1){ lean_box(0) }  (SSL_ERROR_WANT_READ)
+ *   some IOWant.write = ctor(1){ lean_box(1) }  (SSL_ERROR_WANT_WRITE)
+ *
+ * Lean encoding for `ReadResult`:
+ *   data bytes    = ctor(0){ bytes }             (non-nullary constructor 0)
+ *   wantIO .read  = ctor(1){ lean_box(0) }       (non-nullary constructor 1)
+ *   wantIO .write = ctor(1){ lean_box(1) }
+ *   closed        = lean_box(0)                  (first nullary constructor)
+ */
+static inline lean_obj_res mk_option_io_want_none() {
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+static inline lean_obj_res mk_option_io_want_read() {
+    lean_object * r = lean_alloc_ctor(1, 1, 0);
+    lean_ctor_set(r, 0, lean_box(0));
+    return lean_io_result_mk_ok(r);
+}
+
+static inline lean_obj_res mk_option_io_want_write() {
+    lean_object * r = lean_alloc_ctor(1, 1, 0);
+    lean_ctor_set(r, 0, lean_box(1));
+    return lean_io_result_mk_ok(r);
+}
+
+static inline lean_obj_res mk_read_result_data(lean_object * bytes) {
+    lean_object * r = lean_alloc_ctor(0, 1, 0);
+    lean_ctor_set(r, 0, bytes);
+    return lean_io_result_mk_ok(r);
+}
+
+static inline lean_obj_res mk_read_result_want_read() {
+    lean_object * r = lean_alloc_ctor(1, 1, 0);
+    lean_ctor_set(r, 0, lean_box(0));
+    return lean_io_result_mk_ok(r);
+}
+
+static inline lean_obj_res mk_read_result_want_write() {
+    lean_object * r = lean_alloc_ctor(1, 1, 0);
+    lean_ctor_set(r, 0, lean_box(1));
+    return lean_io_result_mk_ok(r);
+}
+
+static inline lean_obj_res mk_read_result_closed() {
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+static inline lean_object * mk_empty_byte_array() {
+    lean_object * arr = lean_alloc_sarray(1, 0, 0);
+    lean_sarray_set_size(arr, 0);
+    return arr;
+}
+
+/*
+Return values:
+  1 -> write completed
+  0 -> write blocked (WANT_READ / WANT_WRITE / ZERO_RETURN)
+ -1 -> fatal error
+*/
+static int ssl_write_step(lean_ssl_session_object * obj, char const * data, size_t size, int * out_err) {
+    if (size > INT_MAX) {
+        *out_err = SSL_ERROR_SSL;
+        return -1;
+    }
+
+    int rc = SSL_write(obj->ssl, data, (int)size);
+    if (rc > 0) {
+        return 1;
+    }
+
+    int err = SSL_get_error(obj->ssl, rc);
+    *out_err = err;
+    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
+        return 0;
+    }
+    return -1;
+}
+
+/*
+Return values:
+  1 -> all pending writes flushed
+  0 -> still blocked, *out_err filled with SSL_ERROR_WANT_READ or SSL_ERROR_WANT_WRITE
+ -1 -> fatal error, *out_err filled
+*/
+static int try_flush_pending_writes(lean_ssl_session_object * obj, int * out_err) {
+    while (!obj->pending_writes.empty()) {
+        auto & pw = obj->pending_writes.front();
+        int step = ssl_write_step(obj, pw.data(), pw.size(), out_err);
+        if (step < 0) return -1;
+        if (step == 0) return 0;
+        obj->pending_writes.erase(obj->pending_writes.begin());
+    }
+    return 1;
+}
+
+void lean_ssl_session_finalizer(void * ptr) {
+    lean_ssl_session_object * obj = (lean_ssl_session_object*)ptr;
+    if (obj->ssl != nullptr) SSL_free(obj->ssl);
+    delete obj;
+}
+
+void initialize_openssl_session() {
+    g_ssl_session_external_class = lean_register_external_class(lean_ssl_session_finalizer, [](void * obj, lean_object * f) {
+        (void)obj;
+        (void)f;
+    });
+}
+
+static lean_obj_res mk_ssl_session(SSL_CTX * ctx, uint8_t is_server) {
+    SSL * ssl = SSL_new(ctx);
+    if (ssl == nullptr) {
+        return mk_ssl_io_error("SSL_new failed");
+    }
+
+    BIO * read_bio = BIO_new(BIO_s_mem());
+    BIO * write_bio = BIO_new(BIO_s_mem());
+
+    if (read_bio == nullptr || write_bio == nullptr) {
+        if (read_bio != nullptr) BIO_free(read_bio);
+        if (write_bio != nullptr) BIO_free(write_bio);
+        SSL_free(ssl);
+        return mk_ssl_io_error("BIO_new failed");
+    }
+
+    BIO_set_nbio(read_bio, 1);
+    BIO_set_nbio(write_bio, 1);
+
+    SSL_set_bio(ssl, read_bio, write_bio);
+
+    if (is_server) {
+        SSL_set_accept_state(ssl);
+    } else {
+        SSL_set_connect_state(ssl);
+    }
+
+    lean_ssl_session_object * ssl_obj = new (std::nothrow) lean_ssl_session_object();
+    if (ssl_obj == nullptr) {
+        SSL_free(ssl);
+        return mk_ssl_io_error("failed to allocate SSL session object");
+    }
+
+    ssl_obj->ssl = ssl;
+    ssl_obj->read_bio = read_bio;
+    ssl_obj->write_bio = write_bio;
+
+    lean_object * obj = lean_ssl_session_object_new(ssl_obj);
+    lean_mark_mt(obj);
+    return lean_io_result_mk_ok(obj);
+}
+
+/* Std.Internal.SSL.Session.Server.mk (ctx : @& Context.Server) : IO Session.Server */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx_obj) {
+    lean_ssl_context_object * ctx = lean_to_ssl_context_object(ctx_obj);
+    return mk_ssl_session(ctx->ctx, 1);
+}
+
+/* Std.Internal.SSL.Session.Client.mk (ctx : @& Context.Client) : IO Session.Client */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx_obj) {
+    lean_ssl_context_object * ctx = lean_to_ssl_context_object(ctx_obj);
+    return mk_ssl_session(ctx->ctx, 0);
+}
+
+/* Std.Internal.SSL.Session.Client.setServerName (ssl : @& Session.Client) (host : @& String) : IO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    const char * server_name = lean_string_cstr(host);
+    if (SSL_set_tlsext_host_name(ssl_obj->ssl, server_name) != 1) {
+        return mk_ssl_io_error("SSL_set_tlsext_host_name failed");
+    }
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+/* Std.Internal.SSL.Session.verifyResult (ssl : @& Session) : IO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    long result = SSL_get_verify_result(ssl_obj->ssl);
+    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)result));
+}
+
+/* Std.Internal.SSL.Session.handshake (ssl : @& Session) : IO (Option IOWant) */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    int rc = SSL_do_handshake(ssl_obj->ssl);
+
+    if (rc == 1) {
+        return mk_option_io_want_none();
+    }
+
+    int err = SSL_get_error(ssl_obj->ssl, rc);
+    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_ZERO_RETURN) {
+        return mk_option_io_want_read();
+    }
+    if (err == SSL_ERROR_WANT_WRITE) {
+        return mk_option_io_want_write();
+    }
+
+    return mk_ssl_io_error("SSL_do_handshake failed", err);
+}
+
+/* Std.Internal.SSL.Session.write (ssl : @& Session) (data : @& ByteArray) : IO (Option IOWant) */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    size_t data_len = lean_sarray_size(data);
+    char const * payload = (char const*)lean_sarray_cptr(data);
+
+    if (data_len == 0) {
+        return mk_option_io_want_none();
+    }
+
+    // If there are pending writes, try to flush them first to preserve write order.
+    // Only attempt the new write directly if the queue fully drains.
+    if (!ssl_obj->pending_writes.empty()) {
+        int flush_err = 0;
+        int flushed = try_flush_pending_writes(ssl_obj, &flush_err);
+
+        if (flushed < 0) {
+            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
+        }
+
+        if (flushed == 0) {
+            ssl_obj->pending_writes.emplace_back(payload, payload + data_len);
+            if (flush_err == SSL_ERROR_WANT_READ) {
+                return mk_option_io_want_read();
+            }
+            return mk_option_io_want_write();
+        }
+        // flushed == 1: queue is clear, fall through to attempt the new write
+    }
+
+    int err = 0;
+    int step = ssl_write_step(ssl_obj, payload, data_len, &err);
+
+    if (step == 1) {
+        return mk_option_io_want_none();
+    }
+
+    if (step == 0 && err == SSL_ERROR_ZERO_RETURN) {
+        return mk_ssl_io_error("SSL_write failed: peer closed the TLS session", err);
+    }
+
+    // Queue plaintext so it is retried after the required socket I/O completes.
+    if (step == 0) {
+        ssl_obj->pending_writes.emplace_back(payload, payload + data_len);
+        if (err == SSL_ERROR_WANT_READ) {
+            return mk_option_io_want_read();
+        }
+        return mk_option_io_want_write();
+    }
+
+    return mk_ssl_io_error("SSL_write failed", err);
+}
+
+/* Std.Internal.SSL.Session.read? (ssl : @& Session) (maxBytes : UInt64) : IO ReadResult */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+
+    if (max_bytes == 0) {
+        return mk_read_result_data(mk_empty_byte_array());
+    }
+
+    if (max_bytes > INT_MAX) {
+        max_bytes = INT_MAX;
+    }
+
+    lean_object * out = lean_alloc_sarray(1, 0, max_bytes);
+    int rc = SSL_read(ssl_obj->ssl, (void*)lean_sarray_cptr(out), (int)max_bytes);
+
+    if (rc > 0) {
+        int flush_err = 0;
+        if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
+            lean_dec(out);
+            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
+        }
+        lean_sarray_set_size(out, (size_t)rc);
+        return mk_read_result_data(out);
+    }
+
+    lean_dec(out);
+
+    int err = SSL_get_error(ssl_obj->ssl, rc);
+
+    if (err == SSL_ERROR_ZERO_RETURN) {
+        int flush_err = 0;
+        if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
+            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
+        }
+        return mk_read_result_closed();
+    }
+
+    if (err == SSL_ERROR_WANT_READ) {
+        int flush_err = 0;
+        int flushed = try_flush_pending_writes(ssl_obj, &flush_err);
+        if (flushed < 0) {
+            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
+        }
+        if (flushed == 0 && flush_err == SSL_ERROR_WANT_WRITE) {
+            return mk_read_result_want_write();
+        }
+        return mk_read_result_want_read();
+    }
+
+    if (err == SSL_ERROR_WANT_WRITE) {
+        int flush_err = 0;
+        int flushed = try_flush_pending_writes(ssl_obj, &flush_err);
+        if (flushed < 0) {
+            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
+        }
+        if (flushed == 0 && flush_err == SSL_ERROR_WANT_READ) {
+            return mk_read_result_want_read();
+        }
+        return mk_read_result_want_write();
+    }
+
+    return mk_ssl_io_error("SSL_read failed", err);
+}
+
+/* Std.Internal.SSL.Session.feedEncrypted (ssl : @& Session) (data : @& ByteArray) : IO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    size_t data_len = lean_sarray_size(data);
+
+    if (data_len == 0) {
+        return lean_io_result_mk_ok(lean_box_uint64(0));
+    }
+
+    if (data_len > INT_MAX) {
+        return mk_ssl_io_error("BIO_write input too large");
+    }
+
+    int rc = BIO_write(ssl_obj->read_bio, lean_sarray_cptr(data), (int)data_len);
+    if (rc >= 0) {
+        return lean_io_result_mk_ok(lean_box_uint64((uint64_t)rc));
+    }
+
+    if (BIO_should_retry(ssl_obj->read_bio)) {
+        return lean_io_result_mk_ok(lean_box_uint64(0));
+    }
+
+    return mk_ssl_io_error("BIO_write failed");
+}
+
+/* Std.Internal.SSL.Session.drainEncrypted (ssl : @& Session) : IO ByteArray */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    size_t pending = BIO_ctrl_pending(ssl_obj->write_bio);
+
+    if (pending == 0) {
+        return lean_io_result_mk_ok(mk_empty_byte_array());
+    }
+
+    if (pending > INT_MAX) {
+        return mk_ssl_io_error("BIO_pending output too large");
+    }
+
+    lean_object * out = lean_alloc_sarray(1, 0, pending);
+    int rc = BIO_read(ssl_obj->write_bio, (void*)lean_sarray_cptr(out), (int)pending);
+
+    if (rc >= 0) {
+        lean_sarray_set_size(out, (size_t)rc);
+        return lean_io_result_mk_ok(out);
+    }
+
+    lean_dec(out);
+
+    if (BIO_should_retry(ssl_obj->write_bio)) {
+        return lean_io_result_mk_ok(mk_empty_byte_array());
+    }
+
+    return mk_ssl_io_error("BIO_read failed");
+}
+
+/* Std.Internal.SSL.Session.pendingEncrypted (ssl : @& Session) : IO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)BIO_ctrl_pending(ssl_obj->write_bio)));
+}
+
+/* Std.Internal.SSL.Session.pendingPlaintext (ssl : @& Session) : IO UInt64 */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl) {
+    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
+    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)SSL_pending(ssl_obj->ssl)));
+}
+
+#else
+
+void initialize_openssl_session() {}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx_obj) {
+    (void)ctx_obj;
+    return io_result_mk_error("lean_uv_ssl_mk_server is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx_obj) {
+    (void)ctx_obj;
+    return io_result_mk_error("lean_uv_ssl_mk_client is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host) {
+    (void)ssl;
+    (void)host;
+    return io_result_mk_error("lean_uv_ssl_set_server_name is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl) {
+    (void)ssl;
+    return io_result_mk_error("lean_uv_ssl_verify_result is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl) {
+    (void)ssl;
+    return io_result_mk_error("lean_uv_ssl_handshake is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
+    (void)ssl;
+    (void)data;
+    return io_result_mk_error("lean_uv_ssl_write is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes) {
+    (void)ssl;
+    (void)max_bytes;
+    return io_result_mk_error("lean_uv_ssl_read is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
+    (void)ssl;
+    (void)data;
+    return io_result_mk_error("lean_uv_ssl_feed_encrypted is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl) {
+    (void)ssl;
+    return io_result_mk_error("lean_uv_ssl_drain_encrypted is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl) {
+    (void)ssl;
+    return io_result_mk_error("lean_uv_ssl_pending_encrypted is not supported");
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl) {
+    (void)ssl;
+    return io_result_mk_error("lean_uv_ssl_pending_plaintext is not supported");
+}
+
+#endif
+
+}

src/runtime/openssl/session.h

@@ -0,0 +1,49 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#pragma once
+
+#include <lean/lean.h>
+#include "runtime/io.h"
+#include "runtime/object.h"
+#include "runtime/openssl/context.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/ssl.h>
+#include <openssl/bio.h>
+#endif
+
+#include <vector>
+
+namespace lean {
+
+static lean_external_class * g_ssl_session_external_class = nullptr;
+void initialize_openssl_session();
+
+#ifndef LEAN_EMSCRIPTEN
+struct lean_ssl_session_object {
+    SSL * ssl;
+    BIO * read_bio;
+    BIO * write_bio;
+    std::vector<std::vector<char>> pending_writes;
+};
+
+static inline lean_object * lean_ssl_session_object_new(lean_ssl_session_object * s) { return lean_alloc_external(g_ssl_session_external_class, s); }
+static inline lean_ssl_session_object * lean_to_ssl_session_object(lean_object * o) { return (lean_ssl_session_object*)(lean_get_external_data(o)); }
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg ssl, b_obj_arg host);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl);
+
+}

tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean

@@ -6,7 +6,6 @@ open Lean Meta Elab Tactic Sym Std Do SpecAttr
 namespace GetThrowSet
 
 set_option mvcgen.warning false
-set_option backward.do.legacy false -- exercises asymmetric bind depth from new do elaborator
 
 abbrev M := ExceptT String <| StateM Nat
 

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -876,10 +876,11 @@ meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
 meta def work (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
   let goal := { goal with mvarId }
-  let mut worklist := #[goal]
+  let mut worklist := Std.Queue.empty.enqueue goal
   repeat do
-    let mut some goal := worklist.back? | break
-    worklist := worklist.pop
+    let some (goal, worklist') := worklist.dequeue? | break
+    let mut goal := goal
+    worklist := worklist'
     let res ← solve goal.mvarId
     match res with
     | .noEntailment .. | .noProgramFoundInTarget .. =>
@@ -895,7 +896,7 @@ meta def work (goal : Grind.Goal) : VCGenM Unit := do
       -- to share E-graph context before forking.
       if subgoals.length > 1 then
         goal ← (← read).preTac.processHypotheses goal
-      worklist := worklist ++ (subgoals |>.map ({ goal with mvarId := · }) |>.reverse)
+      worklist := worklist.enqueueAll (subgoals.map ({ goal with mvarId := · }))
 
 public structure Result where
   invariants : Array MVarId

tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean

@@ -15,7 +15,5 @@ set_option maxHeartbeats 100000000
 
 -- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental
 -- context internalization. This avoids O(n) re-internalization per VC.
--- `simplifying_assumptions [Nat.add_assoc]` here speeds up grind and kernel checking by a factor
--- of 2 because long chains `s + 1 + ... + 1` are collapsed into `s + n`.
-#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' simplifying_assumptions [Nat.add_assoc] with grind) `(tactic| fail)
+#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail)
   [50, 100, 150]

tests/elab/async_http_body.lean

@@ -1,725 +0,0 @@
-import Std.Internal.Http.Data.Body
-
-open Std.Internal.IO Async
-open Std.Http
-open Std.Http.Body
-
-/-! ## Stream tests -/
-
--- Test send and recv on stream
-
-def channelSendRecv : Async Unit := do
-  let stream ← Body.mkStream
-  let chunk := Chunk.ofByteArray "hello".toUTF8
-
-  let sendTask ← async (t := AsyncTask) <| stream.send chunk
-  let result ← stream.recv
-
-  assert! result.isSome
-  assert! result.get!.data == "hello".toUTF8
-  await sendTask
-
-#eval channelSendRecv.block
-
-
--- Test tryRecv on empty stream returns none
-
-def channelTryRecvEmpty : Async Unit := do
-  let stream ← Body.mkStream
-  let result ← stream.tryRecv
-  assert! result.isNone
-
-#eval channelTryRecvEmpty.block
-
--- Test tryRecv consumes a waiting producer
-
-def channelTryRecvWithPendingSend : Async Unit := do
-  let stream ← Body.mkStream
-
-  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "data".toUTF8)
-  let mut result := none
-  let mut fuel := 100
-  while result.isNone && fuel > 0 do
-    result ← stream.tryRecv
-    if result.isNone then
-      let _ ← Selectable.one #[
-        .case (← Selector.sleep 1) pure
-      ]
-    fuel := fuel - 1
-
-  assert! result.isSome
-  assert! result.get!.data == "data".toUTF8
-  await sendTask
-
-#eval channelTryRecvWithPendingSend.block
-
--- Test close sets closed flag
-
-def channelClose : Async Unit := do
-  let stream ← Body.mkStream
-  assert! !(← stream.isClosed)
-  stream.close
-  assert! (← stream.isClosed)
-
-#eval channelClose.block
-
--- Test recv on closed stream returns none
-
-def channelRecvAfterClose : Async Unit := do
-  let stream ← Body.mkStream
-  stream.close
-  let result ← stream.recv
-  assert! result.isNone
-
-#eval channelRecvAfterClose.block
-
--- Test for-in iteration collects chunks until close
-
-def channelForIn : Async Unit := do
-  let stream ← Body.mkStream
-
-  let producer ← async (t := AsyncTask) <| do
-    stream.send (Chunk.ofByteArray "a".toUTF8)
-    stream.send (Chunk.ofByteArray "b".toUTF8)
-    stream.close
-
-  let mut acc : ByteArray := .empty
-  for chunk in stream do
-    acc := acc ++ chunk.data
-
-  assert! acc == "ab".toUTF8
-  await producer
-
-#eval channelForIn.block
-
--- Test chunk extensions are preserved
-
-def channelExtensions : Async Unit := do
-  let stream ← Body.mkStream
-  let chunk := { data := "hello".toUTF8, extensions := #[(.mk "key", some (Chunk.ExtensionValue.ofString! "value"))] : Chunk }
-
-  let sendTask ← async (t := AsyncTask) <| stream.send chunk
-  let result ← stream.recv
-
-  assert! result.isSome
-  assert! result.get!.extensions.size == 1
-  assert! result.get!.extensions[0]! == (Chunk.ExtensionName.mk "key", some <| .ofString! "value")
-  await sendTask
-
-#eval channelExtensions.block
-
--- Test known size metadata
-
-def channelKnownSize : Async Unit := do
-  let stream ← Body.mkStream
-  stream.setKnownSize (some (.fixed 100))
-  let size ← stream.getKnownSize
-  assert! size == some (.fixed 100)
-
-#eval channelKnownSize.block
-
--- Test known size decreases when a chunk is consumed
-
-def channelKnownSizeDecreases : Async Unit := do
-  let stream ← Body.mkStream
-  stream.setKnownSize (some (.fixed 5))
-
-  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "hello".toUTF8)
-  let _ ← stream.recv
-  await sendTask
-
-  let size ← stream.getKnownSize
-  assert! size == some (.fixed 0)
-
-#eval channelKnownSizeDecreases.block
-
--- Test only one blocked producer is allowed
-
-def channelSingleProducerRule : Async Unit := do
-  let stream ← Body.mkStream
-  let send1 ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "one".toUTF8)
-
-  -- Yield so `send1` can occupy the single pending-producer slot.
-  let _ ← Selectable.one #[
-    .case (← Selector.sleep 5) pure
-  ]
-
-  let send2Failed ←
-    try
-      stream.send (Chunk.ofByteArray "two".toUTF8)
-      pure false
-    catch _ =>
-      pure true
-  assert! send2Failed
-
-  let first ← stream.recv
-  assert! first.isSome
-  assert! first.get!.data == "one".toUTF8
-
-  await send1
-
-#eval channelSingleProducerRule.block
-
--- Test only one blocked consumer is allowed
-
-def channelSingleConsumerRule : Async Unit := do
-  let stream ← Body.mkStream
-
-  let recv1 ← async (t := AsyncTask) <| stream.recv
-
-  let hasInterest ← Selectable.one #[
-    .case stream.interestSelector pure
-  ]
-  assert! hasInterest
-
-  let recv2Failed ←
-    try
-      let _ ← stream.recv
-      pure false
-    catch _ =>
-      pure true
-
-  assert! recv2Failed
-
-  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "ok".toUTF8)
-  let r1 ← await recv1
-
-  assert! r1.isSome
-  assert! r1.get!.data == "ok".toUTF8
-  await sendTask
-
-#eval channelSingleConsumerRule.block
-
--- Test hasInterest reflects blocked receiver state
-
-def channelHasInterest : Async Unit := do
-  let stream ← Body.mkStream
-  assert! !(← stream.hasInterest)
-
-  let recvTask ← async (t := AsyncTask) <| stream.recv
-
-  let hasInterest ← Selectable.one #[
-    .case stream.interestSelector pure
-  ]
-  assert! hasInterest
-  assert! (← stream.hasInterest)
-
-  let sendTask ← async (t := AsyncTask) <| stream.send (Chunk.ofByteArray "x".toUTF8)
-  let _ ← await recvTask
-  await sendTask
-
-  assert! !(← stream.hasInterest)
-
-#eval channelHasInterest.block
-
--- Test interestSelector resolves false when stream closes first
-
-def channelInterestSelectorClose : Async Unit := do
-  let stream ← Body.mkStream
-
-  let waitInterest ← async (t := AsyncTask) <|
-    Selectable.one #[
-      .case stream.interestSelector pure
-    ]
-
-  stream.close
-  let interested ← await waitInterest
-  assert! interested == false
-
-#eval channelInterestSelectorClose.block
-
--- Test incomplete sends are buffered and merged into one chunk on the final send
-
-def channelIncompleteChunks : Async Unit := do
-  let stream ← Body.mkStream
-
-  let sendTask ← async (t := AsyncTask) <| do
-    stream.send (Chunk.ofByteArray "hel".toUTF8) (incomplete := true)
-    stream.send (Chunk.ofByteArray "lo".toUTF8)
-
-  let result ← stream.recv
-
-  assert! result.isSome
-  assert! result.get!.data == "hello".toUTF8
-  await sendTask
-
-#eval channelIncompleteChunks.block
-
--- Test sending to a closed stream raises an error
-
-def channelSendAfterClose : Async Unit := do
-  let stream ← Body.mkStream
-  stream.close
-
-  let failed ←
-    try
-      stream.send (Chunk.ofByteArray "test".toUTF8)
-      pure false
-    catch _ =>
-      pure true
-  assert! failed
-
-#eval channelSendAfterClose.block
-
--- Test Body.stream runs producer and returns the stream handle
-
-def channelStreamHelper : Async Unit := do
-  let stream ← Body.stream fun s => do
-    s.send (Chunk.ofByteArray "hello".toUTF8)
-
-  let result ← stream.recv
-  assert! result.isSome
-  assert! result.get!.data == "hello".toUTF8
-
-  let eof ← stream.recv
-  assert! eof.isNone
-
-#eval channelStreamHelper.block
-
--- Test Body.empty creates an already-closed Stream
-
-def channelEmptyHelper : Async Unit := do
-  let stream ← Body.empty
-  assert! (← stream.isClosed)
-
-  let result ← stream.recv
-  assert! result.isNone
-
-#eval channelEmptyHelper.block
-
--- Test Stream.readAll concatenates all chunks
-
-def channelReadAll : Async Unit := do
-  let stream ← Body.mkStream
-
-  let sendTask ← async (t := AsyncTask) <| do
-    stream.send (Chunk.ofByteArray "foo".toUTF8)
-    stream.send (Chunk.ofByteArray "bar".toUTF8)
-    stream.close
-
-  let result : ByteArray ← stream.readAll
-  assert! result == "foobar".toUTF8
-  await sendTask
-
-#eval channelReadAll.block
-
--- Test Stream.readAll enforces a maximum size limit
-
-def channelReadAllMaxSize : Async Unit := do
-  let stream ← Body.mkStream
-
-  let sendTask ← async (t := AsyncTask) <| do
-    stream.send (Chunk.ofByteArray "abcdefgh".toUTF8)
-    stream.close
-
-  let failed ←
-    try
-      let _ : ByteArray ← stream.readAll (maximumSize := some 4)
-      pure false
-    catch _ =>
-      pure true
-  assert! failed
-  await sendTask
-
-#eval channelReadAllMaxSize.block
-
--- Test Stream.getKnownSize reflects the value set via setKnownSize
-
-def channelKnownSizeRoundtrip : Async Unit := do
-  let stream ← Body.mkStream
-  stream.setKnownSize (some (.fixed 42))
-
-  let size ← stream.getKnownSize
-  assert! size == some (.fixed 42)
-
-#eval channelKnownSizeRoundtrip.block
-
-/-! ## Full tests -/
-
--- Test Full.recv returns content once then EOF
-
-def fullRecvConsumesOnce : Async Unit := do
-  let full ← Body.Full.ofString "hello"
-  let first ← full.recv
-  let second ← full.recv
-
-  assert! first.isSome
-  assert! first.get!.data == "hello".toUTF8
-  assert! second.isNone
-
-#eval fullRecvConsumesOnce.block
-
--- Test Full known-size metadata tracks consumption
-
-def fullKnownSizeLifecycle : Async Unit := do
-  let data := ByteArray.mk #[0x01, 0x02, 0x03, 0x04]
-  let full ← Body.Full.ofByteArray data
-
-  assert! (← full.getKnownSize) == some (.fixed 4)
-  let chunk ← full.recv
-  assert! chunk.isSome
-  assert! chunk.get!.data == data
-  assert! (← full.getKnownSize) == some (.fixed 0)
-
-#eval fullKnownSizeLifecycle.block
-
--- Test Full.close discards remaining content
-
-def fullClose : Async Unit := do
-  let full ← Body.Full.ofString "bye"
-  assert! !(← full.isClosed)
-  full.close
-  assert! (← full.isClosed)
-  assert! (← full.recv).isNone
-
-#eval fullClose.block
-
--- Test Full from an empty ByteArray returns none on the first recv
-
-def fullEmptyBytes : Async Unit := do
-  let full ← Body.Full.ofByteArray ByteArray.empty
-  let result ← full.recv
-  assert! result.isNone
-
-#eval fullEmptyBytes.block
-
--- Test Full.recvSelector resolves immediately with the stored chunk
-
-def fullRecvSelectorResolves : Async Unit := do
-  let full ← Body.Full.ofString "world"
-  let result ← Selectable.one #[
-    .case full.recvSelector pure
-  ]
-  assert! result.isSome
-  assert! result.get!.data == "world".toUTF8
-
-#eval fullRecvSelectorResolves.block
-
--- Test Full.getKnownSize returns 0 after close
-
-def fullKnownSizeAfterClose : Async Unit := do
-  let full ← Body.Full.ofString "data"
-  assert! (← full.getKnownSize) == some (.fixed 4)
-  full.close
-  assert! (← full.getKnownSize) == some (.fixed 0)
-
-#eval fullKnownSizeAfterClose.block
-
--- Test Full.tryRecv succeeds once and returns none thereafter
-
-def fullTryRecvIdempotent : Async Unit := do
-  let full ← Body.Full.ofString "once"
-  let first ← full.recv
-  let second ← full.recv
-  assert! first.isSome
-  assert! first.get!.data == "once".toUTF8
-  assert! second.isNone
-
-#eval fullTryRecvIdempotent.block
-
-/-! ## Empty tests -/
-
--- Test Empty.recv always returns none
-
-def emptyBodyRecv : Async Unit := do
-  let body : Body.Empty := {}
-  let result ← body.recv
-  assert! result.isNone
-
-#eval emptyBodyRecv.block
-
--- Test Empty.isClosed is always true
-
-def emptyBodyIsClosed : Async Unit := do
-  let body : Body.Empty := {}
-  assert! (← body.isClosed)
-
-#eval emptyBodyIsClosed.block
-
--- Test Empty.close is a no-op: still closed and recv still returns none
-
-def emptyBodyClose : Async Unit := do
-  let body : Body.Empty := {}
-  body.close
-  assert! (← body.isClosed)
-  let result ← body.recv
-  assert! result.isNone
-
-#eval emptyBodyClose.block
-
--- Test Empty.recvSelector resolves immediately with none
-
-def emptyBodyRecvSelector : Async Unit := do
-  let body : Body.Empty := {}
-  let result ← Selectable.one #[
-    .case body.recvSelector pure
-  ]
-  assert! result.isNone
-
-#eval emptyBodyRecvSelector.block
-
-/-! ## Any tests -/
-
--- Test Any wrapping a Full body forwards recv correctly
-
-def anyFromFull : Async Unit := do
-  let full ← Body.Full.ofString "hello"
-  let any : Body.Any := full
-  let result ← any.recv
-  assert! result.isSome
-  assert! result.get!.data == "hello".toUTF8
-
-#eval anyFromFull.block
-
--- Test Any wrapping an Empty body returns none and reports closed
-
-def anyFromEmpty : Async Unit := do
-  let empty : Body.Empty := {}
-  let any : Body.Any := empty
-  let result ← any.recv
-  assert! result.isNone
-  assert! (← any.isClosed)
-
-#eval anyFromEmpty.block
-
--- Test Any.close closes the underlying body
-
-def anyCloseForwards : Async Unit := do
-  let full ← Body.Full.ofString "test"
-  let any : Body.Any := full
-  any.close
-  assert! (← any.isClosed)
-  let result ← any.recv
-  assert! result.isNone
-
-#eval anyCloseForwards.block
-
--- Test Any.recvSelector resolves immediately for a Full body
-
-def anyRecvSelectorFromFull : Async Unit := do
-  let full ← Body.Full.ofString "sel"
-  let any : Body.Any := full
-  let result ← Selectable.one #[
-    .case any.recvSelector pure
-  ]
-  assert! result.isSome
-  assert! result.get!.data == "sel".toUTF8
-
-#eval anyRecvSelectorFromFull.block
-
-/-! ## Request.Builder body tests -/
-
-private def recvBuiltBody (body : Body.Full) : Async (Option Chunk) :=
-  body.recv
-
--- Test Request.Builder.text sets correct headers
-
-def requestBuilderText : Async Unit := do
-  let req ← Request.post (.originForm! "/api")
-    |>.text "Hello, World!"
-
-  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
-  assert! req.line.headers.get? Header.Name.contentLength == none
-
-  let body ← recvBuiltBody req.body
-  assert! body.isSome
-  assert! body.get!.data == "Hello, World!".toUTF8
-
-#eval requestBuilderText.block
-
--- Test Request.Builder.json sets correct headers
-
-def requestBuilderJson : Async Unit := do
-  let req ← Request.post (.originForm! "/api")
-    |>.json "{\"key\": \"value\"}"
-
-  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
-  assert! req.line.headers.get? Header.Name.contentLength == none
-  let body ← recvBuiltBody req.body
-  assert! body.isSome
-  assert! body.get!.data == "{\"key\": \"value\"}".toUTF8
-
-#eval requestBuilderJson.block
-
--- Test Request.Builder.fromBytes sets body
-
-def requestBuilderFromBytes : Async Unit := do
-  let data := ByteArray.mk #[0x01, 0x02, 0x03]
-  let req ← Request.post (.originForm! "/api")
-    |>.fromBytes data
-
-  assert! req.line.headers.get? Header.Name.contentLength == none
-  let body ← recvBuiltBody req.body
-  assert! body.isSome
-  assert! body.get!.data == data
-
-#eval requestBuilderFromBytes.block
-
--- Test Request.Builder.noBody creates empty body
-
-def requestBuilderNoBody : Async Unit := do
-  let req ← Request.get (.originForm! "/api")
-    |>.empty
-
-  assert! req.body == {}
-
-#eval requestBuilderNoBody.block
-
--- Test Request.Builder.bytes sets application/octet-stream content type
-
-def requestBuilderBytes : Async Unit := do
-  let data := ByteArray.mk #[0xde, 0xad, 0xbe, 0xef]
-  let req ← Request.post (.originForm! "/api")
-    |>.bytes data
-
-  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/octet-stream")
-  let body ← recvBuiltBody req.body
-  assert! body.isSome
-  assert! body.get!.data == data
-
-#eval requestBuilderBytes.block
-
--- Test Request.Builder.html sets text/html content type
-
-def requestBuilderHtml : Async Unit := do
-  let req ← Request.post (.originForm! "/api")
-    |>.html "<h1>Hello</h1>"
-
-  assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/html; charset=utf-8")
-  let body ← recvBuiltBody req.body
-  assert! body.isSome
-  assert! body.get!.data == "<h1>Hello</h1>".toUTF8
-
-#eval requestBuilderHtml.block
-
--- Test Request.Builder.stream creates a streaming body
-
-def requestBuilderStream : Async Unit := do
-  let req ← Request.post (.originForm! "/api")
-    |>.stream fun s => do
-      s.send (Chunk.ofByteArray "streamed".toUTF8)
-
-  let result ← req.body.recv
-  assert! result.isSome
-  assert! result.get!.data == "streamed".toUTF8
-
-#eval requestBuilderStream.block
-
--- Test Request.Builder.noBody body is always closed and returns none
-
-def requestBuilderNoBodyAlwaysClosed : Async Unit := do
-  let req ← Request.get (.originForm! "/api")
-    |>.empty
-
-  assert! (← req.body.isClosed)
-  let result ← req.body.recv
-  assert! result.isNone
-
-#eval requestBuilderNoBodyAlwaysClosed.block
-
-/-! ## Response.Builder body tests -/
-
--- Test Response.Builder.text sets correct headers
-
-def responseBuilderText : Async Unit := do
-  let res ← Response.ok
-    |>.text "Hello, World!"
-
-  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
-  assert! res.line.headers.get? Header.Name.contentLength == none
-
-  let body ← recvBuiltBody res.body
-  assert! body.isSome
-  assert! body.get!.data == "Hello, World!".toUTF8
-
-#eval responseBuilderText.block
-
--- Test Response.Builder.json sets correct headers
-
-def responseBuilderJson : Async Unit := do
-  let res ← Response.ok
-    |>.json "{\"status\": \"ok\"}"
-
-  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
-  assert! res.line.headers.get? Header.Name.contentLength == none
-  let body ← recvBuiltBody res.body
-  assert! body.isSome
-  assert! body.get!.data == "{\"status\": \"ok\"}".toUTF8
-
-#eval responseBuilderJson.block
-
--- Test Response.Builder.fromBytes sets body
-
-def responseBuilderFromBytes : Async Unit := do
-  let data := ByteArray.mk #[0xaa, 0xbb]
-  let res ← Response.ok
-    |>.fromBytes data
-
-  assert! res.line.headers.get? Header.Name.contentLength == none
-  let body ← recvBuiltBody res.body
-  assert! body.isSome
-  assert! body.get!.data == data
-
-#eval responseBuilderFromBytes.block
-
--- Test Response.Builder.noBody creates empty body
-
-def responseBuilderNoBody : Async Unit := do
-  let res ← Response.ok
-    |>.empty
-
-  assert! res.body == {}
-
-#eval responseBuilderNoBody.block
-
--- Test Response.Builder.bytes sets application/octet-stream content type
-
-def responseBuilderBytes : Async Unit := do
-  let data := ByteArray.mk #[0xca, 0xfe]
-  let res ← Response.ok
-    |>.bytes data
-
-  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/octet-stream")
-  let body ← recvBuiltBody res.body
-  assert! body.isSome
-  assert! body.get!.data == data
-
-#eval responseBuilderBytes.block
-
--- Test Response.Builder.html sets text/html content type
-
-def responseBuilderHtml : Async Unit := do
-  let res ← Response.ok
-    |>.html "<p>OK</p>"
-
-  assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/html; charset=utf-8")
-  let body ← recvBuiltBody res.body
-  assert! body.isSome
-  assert! body.get!.data == "<p>OK</p>".toUTF8
-
-#eval responseBuilderHtml.block
-
--- Test Response.Builder.stream creates a streaming body
-
-def responseBuilderStream : Async Unit := do
-  let res ← Response.ok
-    |>.stream fun s => do
-      s.send (Chunk.ofByteArray "streamed".toUTF8)
-
-  let result ← res.body.recv
-  assert! result.isSome
-  assert! result.get!.data == "streamed".toUTF8
-
-#eval responseBuilderStream.block
-
--- Test Response.Builder.noBody body is always closed and returns none
-
-def responseBuilderNoBodyAlwaysClosed : Async Unit := do
-  let res ← Response.ok
-    |>.empty
-
-  assert! (← res.body.isClosed)
-  let result ← res.body.recv
-  assert! result.isNone
-
-#eval responseBuilderNoBodyAlwaysClosed.block

tests/elab/async_ssl.lean

@@ -0,0 +1,601 @@
+import Std.Internal.Async.TCP.SSL
+import Std.Net.Addr
+
+open Std.Internal.IO Async TCP.SSL
+open Std.Net
+open Std.Internal.SSL
+
+-- ---------------------------------------------------------------------------
+-- Helpers
+-- ---------------------------------------------------------------------------
+
+def assertEqStr (actual expected : String) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError s!"expected '{expected}', got '{actual}'"
+
+def assertGt (actual : UInt64) (bound : UInt64) (label : String) : IO Unit := do
+  unless actual > bound do
+    throw <| IO.userError s!"{label}: expected > {bound}, got {actual}"
+
+def assertEqN (actual expected : UInt64) (label : String) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError s!"{label}: expected {expected}, got {actual}"
+
+-- Generate a self-signed certificate for testing.
+def setupTestCerts : IO (String × String) := do
+  IO.FS.createDirAll "/tmp/lean_ssl_test"
+  let keyFile  := "/tmp/lean_ssl_test/key.pem"
+  let certFile := "/tmp/lean_ssl_test/cert.pem"
+
+  discard <| IO.Process.output {
+    cmd  := "openssl"
+    args := #["genrsa", "-out", keyFile, "2048"]
+  }
+
+  discard <| IO.Process.output {
+    cmd  := "openssl"
+    args := #["req", "-new", "-x509", "-key", keyFile, "-out", certFile,
+              "-days", "1", "-subj", "/CN=localhost"]
+  }
+
+  return (certFile, keyFile)
+
+-- Drive one handshake step: advance both state machines and exchange encrypted
+-- bytes between their memory BIOs. Returns (clientDone, serverDone).
+def handshakeStep {rc rs : Role} (c : Session rc) (s : Session rs) : IO (Bool × Bool) := do
+  let cd ← c.handshake
+  let cOut ← c.drainEncrypted
+  if cOut.size > 0 then
+    discard <| s.feedEncrypted cOut
+  let sd ← s.handshake
+  let sOut ← s.drainEncrypted
+  if sOut.size > 0 then
+    discard <| c.feedEncrypted sOut
+  return (cd.isNone, sd.isNone)
+
+partial def runHandshake {rc rs : Role} (c : Session rc) (s : Session rs) : IO Unit := do
+  let (cd, sd) ← handshakeStep c s
+  unless cd && sd do runHandshake c s
+
+-- Pipe all pending encrypted output from src into dst's read BIO.
+def pipeEncrypted {r1 r2 : Role} (src : Session r1) (dst : Session r2) : IO Unit := do
+  let bytes ← src.drainEncrypted
+  if bytes.size > 0 then
+    discard <| dst.feedEncrypted bytes
+
+-- ---------------------------------------------------------------------------
+-- Test 1: Context creation and configuration (smoke test)
+-- ---------------------------------------------------------------------------
+
+def testContextCreation (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+
+  let clientCtx ← Context.Client.mk
+  clientCtx.configure "" false
+
+  -- Configuring with a CA file path (non-empty) exercises the other branch.
+  let clientCtx2 ← Context.Client.mk
+  clientCtx2.configure certFile false
+
+-- ---------------------------------------------------------------------------
+-- Test 2: In-process TLS handshake between two memory-BIO sessions
+-- ---------------------------------------------------------------------------
+
+def testInProcessHandshake (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+
+  let clientCtx ← Context.Client.mk
+  clientCtx.configure "" false  -- skip peer verification
+
+  let serverSess ← Session.Server.mk serverCtx
+  let clientSess ← Session.Client.mk clientCtx
+
+  -- setServerName exercises SSL_set_tlsext_host_name.
+  clientSess.setServerName "localhost"
+
+  runHandshake clientSess serverSess
+
+  -- verifyResult: just verify the call succeeds (self-signed cert returns
+  -- X509_V_ERR_DEPTH_ZERO_SELF_SIGNED_CERT even with VERIFY_NONE).
+  discard <| clientSess.verifyResult
+
+-- ---------------------------------------------------------------------------
+-- Test 3: write / pendingEncrypted / drainEncrypted / feedEncrypted / read?
+-- ---------------------------------------------------------------------------
+
+def testDataTransfer (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+
+  let clientCtx ← Context.Client.mk
+  clientCtx.configure "" false
+
+  let serverSess ← Session.Server.mk serverCtx
+  let clientSess ← Session.Client.mk clientCtx
+
+  runHandshake clientSess serverSess
+
+  -- write plaintext → encrypted bytes appear in the write BIO.
+  let msg := "hello, tls!".toUTF8
+  discard <| clientSess.write msg
+
+  -- pendingEncrypted > 0 before draining.
+  let pending ← clientSess.pendingEncrypted
+  assertGt pending 0 "pendingEncrypted"
+
+  -- Pipe to server and read back.
+  pipeEncrypted clientSess serverSess
+  let received ← serverSess.read? 1024
+  match received with
+  | .data bytes => assertEqStr (String.fromUTF8! bytes) "hello, tls!"
+  | _ => throw <| IO.userError "expected data from server session"
+
+  -- After draining, pendingEncrypted drops to 0.
+  let pendingAfter ← clientSess.pendingEncrypted
+  assertEqN pendingAfter 0 "pendingEncrypted after drain"
+
+  -- read? returns wantIO when no data is available.
+  let empty ← clientSess.read? 1024
+  match empty with
+  | .wantIO _ => return ()
+  | _ => throw <| IO.userError "expected wantIO when no data available"
+
+-- ---------------------------------------------------------------------------
+-- Test 4: pendingPlaintext — write 100 bytes, read 10, rest stays buffered
+-- ---------------------------------------------------------------------------
+
+def testPendingPlaintext (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+
+  let clientCtx ← Context.Client.mk
+  clientCtx.configure "" false
+
+  let serverSess ← Session.Server.mk serverCtx
+  let clientSess ← Session.Client.mk clientCtx
+
+  runHandshake clientSess serverSess
+
+  let bigMsg := (String.ofList (List.replicate 100 'x')).toUTF8
+  discard <| clientSess.write bigMsg
+  pipeEncrypted clientSess serverSess
+
+  -- Read only 10 bytes; the remaining 90 stay in SSL's plaintext buffer.
+  discard <| serverSess.read? 10
+  let remaining ← serverSess.pendingPlaintext
+  assertEqN remaining 90 "pendingPlaintext after partial read"
+
+-- ---------------------------------------------------------------------------
+-- Test 5: Full TCP/TLS round-trip
+-- ---------------------------------------------------------------------------
+
+def serverTask (server : TCP.SSL.Server) : Async Unit := do
+  let client ← server.accept
+  let msg ← client.recv? 1024
+  client.send (msg.getD ByteArray.empty)  -- echo
+  client.shutdown
+
+def clientTask (addr : SocketAddress) (clientCtx : Context.Client) : Async Unit := do
+  let client ← Client.mk clientCtx
+  client.setServerName "localhost"
+  client.connect addr
+  client.noDelay
+  client.send "hello over tls".toUTF8
+  let resp ← client.recv? 1024
+  let got := String.fromUTF8! (resp.getD ByteArray.empty)
+  unless got == "hello over tls" do
+    throw <| IO.userError s!"round-trip mismatch: '{got}'"
+  let _ ← client.getPeerName
+  let _ ← client.getSockName
+  let _ ← client.verifyResult
+  client.shutdown
+
+def testTCPSSL (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.configureServer certFile keyFile  -- idempotent re-configuration
+  server.bind addr
+  server.listen 128
+
+  let _ ← server.getSockName
+
+  let srvTask ← (serverTask server).toIO
+  let cliTask ← (clientTask addr clientCtx).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 6: Multiple sequential round-trips (no hang between messages)
+-- ---------------------------------------------------------------------------
+
+def testMultipleRoundTrips (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    for _ in List.range 5 do
+      let msg ← conn.recv? 1024
+      conn.send (msg.getD ByteArray.empty)
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    for i in List.range 5 do
+      let payload := s!"msg{i}".toUTF8
+      client.send payload
+      let resp ← client.recv? 1024
+      let got := String.fromUTF8! (resp.getD ByteArray.empty)
+      unless got == s!"msg{i}" do
+        throw <| IO.userError s!"round-trip {i} mismatch: '{got}'"
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 7: Large payload (> one TLS record = 16 KB), no hang on fragmentation
+-- ---------------------------------------------------------------------------
+
+def testLargePayload (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let payloadSize := 64 * 1024  -- 64 KB: spans multiple TLS records
+  let payload := ByteArray.mk (List.replicate payloadSize 0x42).toArray
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    -- Accumulate until we have all bytes, then echo back.
+    let mut buf := ByteArray.empty
+    while buf.size < payloadSize do
+      let chunk ← conn.recv? (payloadSize - buf.size).toUInt64
+      buf := buf ++ chunk.getD ByteArray.empty
+    conn.send buf
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    client.send payload
+    let mut buf := ByteArray.empty
+    while buf.size < payloadSize do
+      let chunk ← client.recv? (payloadSize - buf.size).toUInt64
+      buf := buf ++ chunk.getD ByteArray.empty
+    unless buf.size == payloadSize do
+      throw <| IO.userError s!"large payload size mismatch: {buf.size}"
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 8: recv? returns none after peer shutdown (no hang on closed conn)
+-- ---------------------------------------------------------------------------
+
+def testRecvAfterShutdown (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    let msg ← conn.recv? 1024
+    conn.send (msg.getD ByteArray.empty)
+    conn.shutdown  -- server closes write side first
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    client.send "ping".toUTF8
+    -- Receive the echo
+    let resp ← client.recv? 1024
+    let got := String.fromUTF8! (resp.getD ByteArray.empty)
+    unless got == "ping" do
+      throw <| IO.userError s!"echo mismatch: '{got}'"
+    -- After server shutdown, recv? must return none, not hang
+    let closed ← client.recv? 1024
+    unless closed.isNone do
+      throw <| IO.userError "expected none after server shutdown"
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 9: acceptSelector delivers a fully-handshaked connection
+-- ---------------------------------------------------------------------------
+
+def testAcceptSelector (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← Selectable.one #[
+      .case (selector := server.acceptSelector) (cont := fun c => return c)
+    ]
+    let msg ← conn.recv? 1024
+    conn.send (msg.getD ByteArray.empty)
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    client.send "via selector".toUTF8
+    let resp ← client.recv? 1024
+    let got := String.fromUTF8! (resp.getD ByteArray.empty)
+    unless got == "via selector" do
+      throw <| IO.userError s!"selector round-trip mismatch: '{got}'"
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 10: sendAll — multiple buffers are fully delivered and echoed
+-- ---------------------------------------------------------------------------
+
+def testSendAll (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  -- Three chunks whose concatenation we can verify.
+  let chunks  := #["alpha".toUTF8, "beta".toUTF8, "gamma".toUTF8]
+  let expected := "alphabetagamma"
+  let total    := expected.length
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    let mut buf := ByteArray.empty
+    while buf.size < total do
+      let chunk ← conn.recv? total.toUInt64
+      buf := buf ++ chunk.getD ByteArray.empty
+    conn.send buf
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    client.sendAll chunks
+    let mut buf := ByteArray.empty
+    while buf.size < total do
+      let chunk ← client.recv? total.toUInt64
+      buf := buf ++ chunk.getD ByteArray.empty
+    assertEqStr (String.fromUTF8! buf) expected
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 11: recvSelector — server pushes data, client receives via selector
+-- ---------------------------------------------------------------------------
+
+def testRecvSelector (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    conn.send "pushed".toUTF8
+    let ack ← conn.recv? 1024
+    let got := String.fromUTF8! (ack.getD ByteArray.empty)
+    unless got == "ack" do
+      throw <| IO.userError s!"server: expected 'ack', got '{got}'"
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    -- Block until the server's push arrives, using recvSelector.
+    let result ← Selectable.one #[
+      .case (selector := client.recvSelector 1024) (cont := fun r => return r)
+    ]
+    let got := String.fromUTF8! (result.getD ByteArray.empty)
+    unless got == "pushed" do
+      throw <| IO.userError s!"recvSelector mismatch: '{got}'"
+    client.send "ack".toUTF8
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 12: Sequential reuse — same server socket handles N clients in a row
+-- ---------------------------------------------------------------------------
+
+def testSequentialConnections (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  for i in List.range 3 do
+    let srvTask ← (do
+      let conn ← server.accept
+      let msg ← conn.recv? 1024
+      conn.send (msg.getD ByteArray.empty)
+      conn.shutdown
+    : Async Unit).toIO
+
+    let cliTask ← (do
+      let client ← Client.mk clientCtx
+      client.setServerName "localhost"
+      client.connect addr
+      let payload := s!"conn-{i}".toUTF8
+      client.send payload
+      let resp ← client.recv? 1024
+      let got := String.fromUTF8! (resp.getD ByteArray.empty)
+      unless got == s!"conn-{i}" do
+        throw <| IO.userError s!"connection {i} echo mismatch: '{got}'"
+      client.shutdown
+    : Async Unit).toIO
+
+    srvTask.block
+    cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Test 13: Simultaneous bidirectional — both sides send before either reads,
+--          verifying no deadlock occurs.
+-- ---------------------------------------------------------------------------
+
+def testBidirectional (addr : SocketAddress) (certFile keyFile : String) : IO Unit := do
+  let serverCtx ← Context.Server.mk
+  serverCtx.configure certFile keyFile
+  let clientCtx ← Context.Client.mk
+  Client.configureContext clientCtx "" false
+
+  let server ← Server.mk serverCtx
+  server.bind addr
+  server.listen 128
+
+  let srvTask ← (do
+    let conn ← server.accept
+    conn.send "from-server".toUTF8        -- send without waiting for client first
+    let msg ← conn.recv? 1024
+    let got := String.fromUTF8! (msg.getD ByteArray.empty)
+    unless got == "from-client" do
+      throw <| IO.userError s!"server recv mismatch: '{got}'"
+    conn.shutdown
+  : Async Unit).toIO
+
+  let cliTask ← (do
+    let client ← Client.mk clientCtx
+    client.setServerName "localhost"
+    client.connect addr
+    client.send "from-client".toUTF8      -- send without waiting for server first
+    let msg ← client.recv? 1024
+    let got := String.fromUTF8! (msg.getD ByteArray.empty)
+    unless got == "from-server" do
+      throw <| IO.userError s!"client recv mismatch: '{got}'"
+    client.shutdown
+  : Async Unit).toIO
+
+  srvTask.block
+  cliTask.block
+
+-- ---------------------------------------------------------------------------
+-- Run all tests
+-- ---------------------------------------------------------------------------
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testContextCreation certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testInProcessHandshake certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testDataTransfer certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testPendingPlaintext certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testTCPSSL (SocketAddressV4.mk (.ofParts 127 0 0 1) 18443) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testTCPSSL (SocketAddressV6.mk (.ofParts 0 0 0 0 0 0 0 1) 18444) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testMultipleRoundTrips (SocketAddressV4.mk (.ofParts 127 0 0 1) 18445) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testLargePayload (SocketAddressV4.mk (.ofParts 127 0 0 1) 18446) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testRecvAfterShutdown (SocketAddressV4.mk (.ofParts 127 0 0 1) 18447) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testAcceptSelector (SocketAddressV4.mk (.ofParts 127 0 0 1) 18448) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testSendAll (SocketAddressV4.mk (.ofParts 127 0 0 1) 18449) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testRecvSelector (SocketAddressV4.mk (.ofParts 127 0 0 1) 18450) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testSequentialConnections (SocketAddressV4.mk (.ofParts 127 0 0 1) 18451) certFile keyFile
+
+#eval do
+  let (certFile, keyFile) ← setupTestCerts
+  testBidirectional (SocketAddressV4.mk (.ofParts 127 0 0 1) 18452) certFile keyFile

tests/elab/deprecated_arg.lean

@@ -1,330 +0,0 @@
-/-
-Tests for the `deprecated_arg` attribute.
--/
-
--- `newArg` is not a parameter of the declaration
-/--
-error: `new` is not a parameter of `f1`
--/
-#guard_msgs in
-@[deprecated_arg old new]
-def f1 (x : Nat) : Nat := x
-
--- `oldArg` is still a parameter of the declaration (rename not applied)
-/--
-error: `old` is still a parameter of `f2`; rename it to `new` before adding `@[deprecated_arg]`
--/
-#guard_msgs in
-@[deprecated_arg old new]
-def f2 (old new : Nat) : Nat := old + new
-
--- Neither name is a parameter — reports that `newArg` is not a parameter
-/--
-error: `baz` is not a parameter of `f3`
--/
-#guard_msgs in
-@[deprecated_arg bar baz]
-def f3 (x : Nat) : Nat := x
-
--- Valid usage without `since`: warns about missing `since`
-/--
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
--/
-#guard_msgs in
-@[deprecated_arg old new]
-def f4 (new : Nat) : Nat := new
-
--- Valid usage with `since`: no warning
-#guard_msgs in
-@[deprecated_arg old new (since := "2026-03-18")]
-def f5 (new : Nat) : Nat := new
-
--- Multiple renames without `since`: warns twice
-/--
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
----
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
--/
-#guard_msgs in
-@[deprecated_arg old1 new1, deprecated_arg old2 new2]
-def f6 (new1 new2 : Nat) : Nat := new1 + new2
-
-/-! ## Functional tests: warning + correct elaboration -/
-
--- Old name produces warning with code action hint and elaborates correctly
-/--
-warning: parameter `old` of `f4` has been deprecated, use `new` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲
----
-info: f4 42 : Nat
--/
-#guard_msgs in
-#check f4 (old := 42)
-
--- New name produces no warning
-/--
-info: f4 42 : Nat
--/
-#guard_msgs in
-#check f4 (new := 42)
-
--- Positional arguments are unaffected
-/--
-info: f4 42 : Nat
--/
-#guard_msgs in
-#check f4 42
-
--- `since` field does not appear in warning message (consistent with `@[deprecated]`)
-/--
-warning: parameter `old` of `f5` has been deprecated, use `new` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲
----
-info: f5 42 : Nat
--/
-#guard_msgs in
-#check f5 (old := 42)
-
--- Multiple renames: both warnings emitted with code action hints
-/--
-warning: parameter `old1` of `f6` has been deprecated, use `new1` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲1
----
-warning: parameter `old2` of `f6` has been deprecated, use `new2` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲2
----
-info: f6 1 2 : Nat
--/
-#guard_msgs in
-#check f6 (old1 := 1) (old2 := 2)
-
--- Multiple renames: new names produce no warnings
-/--
-info: f6 1 2 : Nat
--/
-#guard_msgs in
-#check f6 (new1 := 1) (new2 := 2)
-
--- Mixed: one old name, one new name
-/--
-warning: parameter `old1` of `f6` has been deprecated, use `new1` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲1
----
-info: f6 1 2 : Nat
--/
-#guard_msgs in
-#check f6 (old1 := 1) (new2 := 2)
-
-/-! ## Disabling the linter rejects old names -/
-
--- When `linter.deprecated.arg` is false, old names produce a clean error
-/--
-error: Invalid argument name `old` for function `f4`
-
-Hint: Perhaps you meant one of the following parameter names:
-  • `new`: o̵l̵d̵n̲e̲w̲
--/
-#guard_msgs in
-set_option linter.deprecated.arg false in
-#check f4 (old := 42)
-
--- New name still works when linter is disabled
-/--
-info: f4 42 : Nat
--/
-#guard_msgs in
-set_option linter.deprecated.arg false in
-#check f4 (new := 42)
-
-/-! ## Removed (no replacement) deprecated arguments -/
-
--- `oldArg` is still a parameter of the declaration
-/--
-error: `removed` is still a parameter of `r1`; remove it before adding `@[deprecated_arg]`
--/
-#guard_msgs in
-@[deprecated_arg removed]
-def r1 (removed : Nat) : Nat := removed
-
--- Valid removed arg without `since`: warns about missing `since`
-/--
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
--/
-#guard_msgs in
-@[deprecated_arg removed]
-def r2 (x : Nat) : Nat := x
-
--- Valid removed arg with `since`: no warning
-#guard_msgs in
-@[deprecated_arg removed (since := "2026-03-23")]
-def r3 (x : Nat) : Nat := x
-
--- Using a removed arg produces an error with delete hint
-/--
-error: parameter `removed` of `r2` has been deprecated
-
-Hint: Delete this argument:
-  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check r2 (removed := 42)
-
--- Using a removed arg with `since` produces an error with delete hint
-/--
-error: parameter `removed` of `r3` has been deprecated
-
-Hint: Delete this argument:
-  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check r3 (removed := 42)
-
--- Normal args still work alongside removed deprecated args
-/--
-info: r2 42 : Nat
--/
-#guard_msgs in
-#check r2 (x := 42)
-
--- Positional args work fine
-/--
-info: r3 42 : Nat
--/
-#guard_msgs in
-#check r3 42
-
--- Removed arg: when linter is disabled, falls through to normal "invalid arg" error
-/--
-error: Invalid argument name `removed` for function `r2`
-
-Hint: Perhaps you meant one of the following parameter names:
-  • `x`: r̵e̵m̵o̵v̵e̵d̵x̲
--/
-#guard_msgs in
-set_option linter.deprecated.arg false in
-#check r2 (removed := 42)
-
--- Mix of renamed and removed on same declaration
-/--
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
----
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
--/
-#guard_msgs in
-@[deprecated_arg old new, deprecated_arg removed]
-def r4 (new : Nat) : Nat := new
-
--- Renamed arg still warns
-/--
-warning: parameter `old` of `r4` has been deprecated, use `new` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲
----
-info: r4 42 : Nat
--/
-#guard_msgs in
-#check r4 (old := 42)
-
--- Removed arg errors
-/--
-error: parameter `removed` of `r4` has been deprecated
-
-Hint: Delete this argument:
-  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check r4 (removed := 42)
-
-@[deprecated_arg arg (since := "26.03.26")]
-def r5 (x : Nat) : Nat := x
-
-/--
-error: parameter `arg` of `r5` has been deprecated
-
-Hint: Delete this argument:
-  (̵a̵r̵g̵ ̵:̵=̵ ̵6̵)̵
--/
-#guard_msgs in
-#check r5 3 (arg := 6)
-
-/--
-error: Invalid argument name `arg` for function `r5`
-
-Hint: Perhaps you meant one of the following parameter names:
-  • `x`: a̵r̵g̵x̲
--/
-#guard_msgs in
-set_option linter.deprecated.arg false in
-#check r5 3 (arg := 6)
-
-/-! ## Custom deprecation messages -/
-
--- Renamed arg with custom message
-#guard_msgs in
-@[deprecated_arg old new "this parameter was split into two" (since := "2026-03-26")]
-def m1 (new : Nat) : Nat := new
-
--- Using renamed arg with message shows the message in the warning
-/--
-warning: parameter `old` of `m1` has been deprecated, use `new` instead: this parameter was split into two
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲
----
-info: m1 42 : Nat
--/
-#guard_msgs in
-#check m1 (old := 42)
-
--- Removed arg with custom message
-#guard_msgs in
-@[deprecated_arg gone "no longer needed" (since := "2026-03-26")]
-def m2 (x : Nat) : Nat := x
-
--- Using removed arg with message shows the message in the error
-/--
-error: parameter `gone` of `m2` has been deprecated: no longer needed
-
-Hint: Delete this argument:
-  (̵g̵o̵n̵e̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check m2 (gone := 42)
-
--- Without custom message, behavior unchanged
-/--
-error: parameter `removed` of `r3` has been deprecated
-
-Hint: Delete this argument:
-  (̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check r3 (removed := 42)
-
--- Removed arg with text but no `since`: warns about missing `since`
-/--
-warning: `[deprecated_arg]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
--/
-#guard_msgs in
-@[deprecated_arg dropped "use positional args"]
-def m3 (x : Nat) : Nat := x
-
-/--
-error: parameter `dropped` of `m3` has been deprecated: use positional args
-
-Hint: Delete this argument:
-  (̵d̵r̵o̵p̵p̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
--/
-#guard_msgs in
-#check m3 (dropped := 42)

tests/elab/doDepIfAnon.lean

@@ -1,14 +0,0 @@
--- Test that anonymous `if _ : cond then ...` works in do blocks (new do elaborator)
-set_option backward.do.legacy false
-def testDepIfAnon (n : Nat) : IO Unit := do
-  if _ : n > 0 then
-    IO.println "positive"
-  else
-    IO.println "zero"
-
--- Test the named variant too
-def testDepIfNamed (n : Nat) : IO Unit := do
-  if h : n > 0 then
-    IO.println s!"positive: {n} > 0"
-  else
-    IO.println "zero"

tests/elab/grind_13167.lean

@@ -1,6 +0,0 @@
-module
-
--- https://github.com/leanprover/lean4/issues/13167
-theorem Option.bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
-    pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by
-  grind [cases Option, pmap]

tests/elab/openssl.lean

@@ -0,0 +1,6 @@
+import Lean.Runtime
+
+-- Non-emscripten build: expect the major version of OpenSSL (3)
+/-- info: 3 -/
+#guard_msgs in
+#eval if !System.Platform.isEmscripten then Lean.openSSLVersion >>> 28 else 3

tests/elab/repeat_extrinsic.lean

@@ -1,89 +0,0 @@
-module
-
-import Std
-
-set_option mvcgen.warning false
-
-open Std.Do
-
-/-!
-# Tests for extrinsic `repeat`/`while` loops
-
-These tests verify that the new `Repeat` type and its verification infrastructure work correctly.
--/
-
-/-- `sqrt n` computes the integer square root of `n` using a `while` loop. -/
-def sqrt (n : Nat) : Id Nat := do
-  if n = 0 then
-    return 0
-  let mut i := 0
-  while i * i ≤ n
-  do
-    i := i + 1
-  return i - 1
-
-/-- The `sqrt` function returns the correct integer square root. -/
-theorem sqrt_correct :
-    ⦃⌜True⌝⦄ sqrt n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
-  mvcgen [sqrt]
-  invariants
-  | inv1 => fun i => (n + 2) - i
-  | inv2 => ⇓ cursor => match cursor with
-    | .repeat i => ⌜∀ j, j < i → j * j ≤ n⌝
-    | .done i => ⌜(∀ j, j < i → j * j ≤ n) ∧ n < i * i⌝
-  with (try grind)
-  | vc2 =>
-    apply Lean.Repeat.IsPlausibleStep.wf_of_wp_measure (fun i => (n + 2) - i)
-    intro r
-    mvcgen with try grind
-    | vc1 hsqr =>
-      have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
-      grind
-  | vc3 =>
-    rename_i b hsqr _ hinv
-    intro j hj
-    rcases Nat.lt_or_eq_of_le (Nat.lt_succ_iff.mp hj) with hlt | rfl
-    · exact hinv j hlt
-    · exact hsqr
-  | vc6 res h =>
-    have : res - 1 < res := by grind
-    grind
-
-set_option backward.do.while true in
-/-- Test: `backward.do.while true` should expand to `Loop.mk`. -/
-def loopBackwardCompat (n : Nat) : Nat := Id.run do
-  let mut i := 0
-  repeat
-    if i < n then
-      i := i + 1
-    else
-      break
-  return i
-
--- Verify the backward-compat loop computes correctly
-#guard loopBackwardCompat 5 == 5
-#guard loopBackwardCompat 0 == 0
-
-/-- Test: default setting should expand to `Repeat.mk`. -/
-def loopDefault (n : Nat) : Nat := Id.run do
-  let mut i := 0
-  repeat
-    if i < n then
-      i := i + 1
-    else
-      break
-  return i
-
--- Verify the default loop computes correctly
-#guard loopDefault 5 == 5
-#guard loopDefault 0 == 0
-
--- Verify sqrt computes correctly
-#guard Id.run (sqrt 0) == 0
-#guard Id.run (sqrt 1) == 1
-#guard Id.run (sqrt 4) == 2
-#guard Id.run (sqrt 8) == 2
-#guard Id.run (sqrt 9) == 3
-#guard Id.run (sqrt 15) == 3
-#guard Id.run (sqrt 16) == 4
-#guard Id.run (sqrt 100) == 10

tests/pkg/deprecated_arg/DeprecatedArg.lean

@@ -1 +0,0 @@
-import DeprecatedArg.Use

tests/pkg/deprecated_arg/DeprecatedArg/Def.lean

@@ -1,5 +0,0 @@
-@[deprecated_arg arg foo (since := "2026-03-18")]
-def f (foo : Nat) : Nat := foo + 1
-
-@[deprecated_arg old1 new1 (since := "2026-03-18"), deprecated_arg old2 new2 (since := "2026-03-18")]
-def g (new1 new2 : Nat) : Nat := new1 + new2

tests/pkg/deprecated_arg/DeprecatedArg/Use.lean

@@ -1,55 +0,0 @@
-import DeprecatedArg.Def
-
--- Cross-file: old name produces warning
-/--
-warning: parameter `arg` of `f` has been deprecated, use `foo` instead
-
-Hint: Rename this argument:
-  a̵r̵g̵f̲o̲o̲
----
-info: f 42 : Nat
--/
-#guard_msgs in
-#check f (arg := 42)
-
--- Cross-file: new name produces no warning
-/--
-info: f 42 : Nat
--/
-#guard_msgs in
-#check f (foo := 42)
-
--- Cross-file: positional arg produces no warning
-/--
-info: f 42 : Nat
--/
-#guard_msgs in
-#check f 42
-
--- Cross-file: multiple renames
-/--
-warning: parameter `old1` of `g` has been deprecated, use `new1` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲1
----
-warning: parameter `old2` of `g` has been deprecated, use `new2` instead
-
-Hint: Rename this argument:
-  o̵l̵d̵n̲e̲w̲2
----
-info: g 1 2 : Nat
--/
-#guard_msgs in
-#check g (old1 := 1) (old2 := 2)
-
--- Cross-file: disabling the linter rejects old names with a clean error
-/--
-error: Invalid argument name `arg` for function `f`
-
-Hint: Perhaps you meant one of the following parameter names:
-  • `foo`: a̵r̵g̵f̲o̲o̲
--/
-#guard_msgs in
-set_option linter.deprecated.arg false in
-#check f (arg := 42)

tests/pkg/deprecated_arg/lakefile.lean

@@ -1,5 +0,0 @@
-import Lake
-open Lake DSL
-
-package deprecated_arg
-@[default_target] lean_lib DeprecatedArg

tests/pkg/deprecated_arg/lean-toolchain

@@ -1 +0,0 @@
-../../../build/release/stage1

tests/pkg/deprecated_arg/run_test.sh

@@ -1,2 +0,0 @@
-rm -rf .lake/build
-lake build

tests/pkg/ver_clash/clean.sh

@@ -1,6 +1 @@
 rm -rf work
-
-# previous clean.sh, without it we would be copying old .git dirs and get a test failure
-rm -rf DiamondExample-*/.git
-rm -rf DiamondExample-*/.lake DiamondExample-*/lake-manifest.json
-rm -f DiamondExample-D/produced.out