feat: add role

.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
@@ -78,7 +78,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
+          git fetch --depth=1 origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
@@ -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
@@ -125,7 +125,7 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Configure Build
+      - name: Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,21 +162,7 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-      - name: Build Stage 0 & Configure Stage 1
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build stage1-configure -j$NPROC
-      - name: Download Lake Cache
-        if: matrix.name == 'Linux Lake (Cached)'
-        run: |
-          cd src
-          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
-      - name: Build Target Stage
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build $TARGET_STAGE -j$NPROC
+          time make $TARGET_STAGE -j$NPROC
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
@@ -195,21 +181,6 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Lake Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
-        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
-        run: |
-          curl --version
-          cd src
-          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
-          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
-        env:
-          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
-          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
-          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install

.github/workflows/ci.yml

@@ -244,7 +244,7 @@ jobs:
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
                 // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -265,7 +265,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -273,19 +273,7 @@ jobs:
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
-              },
-              {
-                "name": "Linux Lake (Cached)",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
-                "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
-                "test": true,
-                "secondary": true,
-                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
-                "test-bench": large && level >= 2,
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
@@ -299,7 +287,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

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)
@@ -730,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)

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -243,19 +243,13 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   -- All of these reasons propagate through ABI decisions and can thus safely be ignored as they
   -- will be accounted for by the reference counting pass.
   | .constructorArg .. | .functionCallArg .. | .fvarCall .. | .partialApplication ..
-  | .jpArgPropagation ..
-  -- forward propagation can never affect a user-annotated parameter
-  | .forwardProjectionProp ..
-  -- backward propagation on a user-annotated parameter is only necessary if the projected value
-  -- directly flows into a reset-reuse. However, the borrow annotation propagator ensures this
-  -- situation never arises
-  | .backwardProjectionProp .. => false
+  | .jpArgPropagation .. => false
   -- Results of functions and constructors are naturally owned.
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
-  | .ownedAnnotation => true
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
+  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.

src/Lean/Elab/BuiltinTerm.lean

@@ -315,16 +315,9 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => panic! "resolveId? returned an unexpected expression"
 
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
+  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
-  if !backward.inferInstanceAs.wrap.get (← getOptions) then
-    return (← elabTerm (← `(_root_.inferInstanceAs $(⟨typeStx⟩))) expectedType?)
-
-  let some expectedType ← tryPostponeIfHasMVars? expectedType? |
-    throwError (m!"`inferInstanceAs` failed, expected type contains metavariables{indentD expectedType?}" ++
-      .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
-        instance translation. If you do not intend to transport instances between two types, \
-        consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
   let type ← withSynthesize (postpone := .yes) <| elabType typeStx
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType
@@ -336,7 +329,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+    let isMeta := (← read).isMetaSection
     withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst

src/Lean/Elab/Deriving/Basic.lean

@@ -220,7 +220,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType

src/Lean/Meta/Sym/SymM.lean

@@ -15,48 +15,6 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
-/-!
-## Sym Extensions
-
-Extensible state mechanism for `SymM`, allowing modules to register persistent state
-that lives across `simp` invocations within a `sym =>` block. Follows the same pattern
-as `Grind.SolverExtension` in `Lean/Meta/Tactic/Grind/Types.lean`.
--/
-
-/-- Opaque extension state type used to store type-erased extension values. -/
-opaque SymExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
-@[expose] def SymExtensionState : Type := SymExtensionStateSpec.fst
-instance : Inhabited SymExtensionState := SymExtensionStateSpec.snd
-
-/--
-A registered extension for `SymM`. Each extension gets a unique index into the
-extensions array in `Sym.State`. Can only be created via `registerSymExtension`.
--/
-structure SymExtension (σ : Type) where private mk ::
-  id        : Nat
-  mkInitial : IO σ
-  deriving Inhabited
-
-private builtin_initialize symExtensionsRef : IO.Ref (Array (SymExtension SymExtensionState)) ← IO.mkRef #[]
-
-/--
-Registers a new `SymM` state extension. Extensions can only be registered during initialization.
-Returns a handle for typed access to the extension's state.
--/
-def registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ) := do
-  unless (← initializing) do
-    throw (IO.userError "failed to register `Sym` extension, extensions can only be registered during initialization")
-  let exts ← symExtensionsRef.get
-  let id := exts.size
-  let ext : SymExtension σ := { id, mkInitial }
-  symExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
-  return ext
-
-/-- Returns initial state for all registered extensions. -/
-def SymExtensions.mkInitialStates : IO (Array SymExtensionState) := do
-  let exts ← symExtensionsRef.get
-  exts.mapM fun ext => ext.mkInitial
-
 /--
 Information about a single argument position in a function's type signature.
 
@@ -175,8 +133,6 @@ structure State where
   congrInfo : PHashMap ExprPtr CongrInfo := {}
   /-- Cache for `isDefEqI` results -/
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
-  /-- State for registered `SymExtension`s, indexed by extension id. -/
-  extensions : Array SymExtensionState := #[]
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -194,8 +150,7 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  let extensions ← SymExtensions.mkInitialStates
-  x { sharedExprs } |>.run' { debug, share, extensions }
+  x { sharedExprs } |>.run' { debug, share }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=
@@ -275,26 +230,4 @@ def isDefEqI (s t : Expr) : SymM Bool := do
   modify fun s => { s with defEqI := s.defEqI.insert key result }
   return result
 
-instance : Inhabited (SymM α) where
-  default := throwError "<SymM default value>"
-
-/-! ### SymExtension accessors -/
-
-private unsafe def SymExtension.getStateCoreImpl (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ :=
-  return unsafeCast extensions[ext.id]!
-
-@[implemented_by SymExtension.getStateCoreImpl]
-opaque SymExtension.getStateCore (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ
-
-def SymExtension.getState (ext : SymExtension σ) : SymM σ := do
-  ext.getStateCore (← get).extensions
-
-private unsafe def SymExtension.modifyStateImpl (ext : SymExtension σ) (f : σ → σ) : SymM Unit := do
-  modify fun s => { s with
-    extensions := s.extensions.modify ext.id fun state => unsafeCast (f (unsafeCast state))
-  }
-
-@[implemented_by SymExtension.modifyStateImpl]
-opaque SymExtension.modifyState (ext : SymExtension σ) (f : σ → σ) : SymM Unit
-
 end Lean.Meta.Sym

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/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/TCP/SSL.lean

@@ -0,0 +1,445 @@
+/-
+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
+  dbg_trace "start handshake"
+
+  dbg_trace "checking :D"
+  if ← ssl.handshake then
+    flushEncrypted native ssl
+    dbg_trace "handshaked :D"
+    return ()
+
+  dbg_trace "flush :D"
+  flushEncrypted native ssl
+
+  dbg_trace "receiving more data"
+  let encrypted? ← Async.ofPromise <| native.recv? chunkSize
+  match encrypted? with
+  | none =>
+    throw <| IO.userError "connection closed during TLS handshake"
+  | some encrypted =>
+    dbg_trace "feeding more data"
+    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
+
+/--
+Tries to accept an incoming TLS connection without blocking.
+-/
+@[inline]
+def tryAccept (s : Server) : IO (Option ServerConn) := do
+  let res ← s.native.tryAccept
+  let socket ← IO.ofExcept res
+  match socket with
+  | none => return none
+  | some native => return some (← mkServerConn native s.serverCtx)
+
+/--
+Creates a `Selector` that resolves once `s` has a connection available.
+-/
+def acceptSelector (s : Server) : Selector ServerConn :=
+  {
+    tryFn :=
+      s.tryAccept
+
+    registerFn waiter := do
+      let task ← s.native.accept
+
+      -- If we get cancelled the promise will be dropped so prepare for that
+      IO.chainTask (t := task.result?) fun res => do
+        match res with
+        | none => return ()
+        | some res =>
+          let lose := return ()
+          let win promise := do
+            try
+              let native ← IO.ofExcept res
+              let ssl ← Session.Server.mk s.serverCtx
+              let conn : ServerConn := ⟨native, ssl⟩
+              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
+
+/--
+Enables 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
+
+-- ## Connection (shared read/write operations for both roles)
+
+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
+  let accepted ← s.ssl.write data
+  flushEncrypted s.native s.ssl
+  return accepted
+
+/--
+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 pulls encrypted data from TCP first.
+-/
+partial def recv? {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option ByteArray) := do
+  match ← s.ssl.read? size with
+  | some plain =>
+    flushEncrypted s.native s.ssl
+    return some plain
+  | none =>
+    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) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
+  if (← s.ssl.pendingPlaintext) > 0 then
+    return ()
+
+  let rec go : Async Unit := do
+    let readable ← Async.ofPromise <| s.native.waitReadable
+
+    if !readable then
+      return ()
+
+    let encrypted? ← Async.ofPromise <| s.native.recv? chunkSize
+
+    match encrypted? with
+    | none =>
+      return ()
+    | some encrypted =>
+      feedEncryptedChunk s.ssl encrypted
+      flushEncrypted s.native s.ssl
+
+      if (← s.ssl.pendingPlaintext) > 0 then
+        return ()
+      else
+        go
+
+  go
+
+/--
+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
+
+/--
+Enables 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/SSL.lean

@@ -0,0 +1,178 @@
+/-
+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 ContextImpl : Role → NonemptyType.{0}
+
+/--
+Represents an OpenSSL context (`SSL_CTX`) parameterized by role.
+Use `Context.Server` or `Context.Client` for the concrete aliases.
+-/
+def Context (r : Role) : Type := (ContextImpl r).type
+
+/--
+Server-side TLS context (`SSL_CTX` configured with `TLS_server_method`).
+-/
+abbrev Context.Server := Context .server
+
+/--
+Client-side TLS context (`SSL_CTX` configured with `TLS_client_method`).
+-/
+abbrev Context.Client := Context .client
+
+instance (r : Role) : Nonempty (Context r) := (ContextImpl r).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
+
+/--
+reates 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
+
+private opaque SessionImpl : Role → NonemptyType.{0}
+
+/--
+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 `true` when the handshake is complete.
+-/
+@[extern "lean_uv_ssl_handshake"]
+opaque handshake {r : Role} (ssl : @& Session r) : IO Bool
+
+/--
+Attempts to write plaintext application data into SSL.
+Returns `true` when accepted, `false` when OpenSSL needs more I/O first.
+-/
+@[extern "lean_uv_ssl_write"]
+opaque write {r : Role} (ssl : @& Session r) (data : @& ByteArray) : IO Bool
+
+/--
+Attempts to read decrypted plaintext data. Returns `none` when OpenSSL needs more I/O.
+-/
+@[extern "lean_uv_ssl_read"]
+opaque read? {r : Role} (ssl : @& Session r) (maxBytes : UInt64) : IO (Option ByteArray)
+
+/--
+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/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,155 @@
+/*
+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_set_mode(ctx, SSL_MODE_AUTO_RETRY);
+
+    #ifdef SSL_OP_NO_RENEGOTIATION
+    SSL_CTX_clear_options(ctx, SSL_OP_NO_RENEGOTIATION);
+    #endif
+    #ifdef SSL_OP_ALLOW_CLIENT_RENEGOTIATION
+    SSL_CTX_set_options(ctx, SSL_OP_ALLOW_CLIENT_RENEGOTIATION);
+    #endif
+}
+
+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,490 @@
+/*
+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 <cstdlib>
+#include <cstring>
+#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));
+}
+
+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;
+}
+
+static void free_pending_writes(lean_ssl_session_object * obj) {
+    if (obj->pending_writes != nullptr) {
+        for (size_t i = 0; i < obj->pending_writes_count; i++) {
+            free(obj->pending_writes[i].data);
+        }
+        free(obj->pending_writes);
+        obj->pending_writes = nullptr;
+    }
+    obj->pending_writes_count = 0;
+}
+
+static bool append_pending_write(lean_ssl_session_object * obj, char const * data, size_t size) {
+    char * copy = (char*)malloc(size);
+    if (copy == nullptr) return false;
+
+    std::memcpy(copy, data, size);
+
+    size_t new_count = obj->pending_writes_count + 1;
+    lean_ssl_pending_write * new_arr = (lean_ssl_pending_write*)realloc(
+        obj->pending_writes, sizeof(lean_ssl_pending_write) * new_count
+    );
+
+    if (new_arr == nullptr) {
+        free(copy);
+        return false;
+    }
+
+    obj->pending_writes = new_arr;
+    obj->pending_writes[obj->pending_writes_count].data = copy;
+    obj->pending_writes[obj->pending_writes_count].size = size;
+    obj->pending_writes_count = new_count;
+    return true;
+}
+
+/*
+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 by renegotiation
+ -1 -> fatal error, *out_err filled
+*/
+static int try_flush_pending_writes(lean_ssl_session_object * obj, int * out_err) {
+    if (obj->pending_writes_count == 0) return 1;
+
+    size_t completed = 0;
+
+    for (size_t i = 0; i < obj->pending_writes_count; i++) {
+        lean_ssl_pending_write * pw = &obj->pending_writes[i];
+
+        while (pw->size > 0) {
+            int err = 0;
+            int step = ssl_write_step(obj, pw->data, pw->size, &err);
+
+            if (step == 1) {
+                // We do not enable partial writes, so a successful SSL_write consumes the full buffer.
+                pw->size = 0;
+                continue;
+            }
+
+            if (step == 0) {
+                goto done;
+            }
+
+            *out_err = err;
+            return -1;
+        }
+
+        free(pw->data);
+        pw->data = nullptr;
+        completed++;
+    }
+
+done:
+    if (completed > 0) {
+        obj->pending_writes_count -= completed;
+        if (obj->pending_writes_count == 0) {
+            free(obj->pending_writes);
+            obj->pending_writes = nullptr;
+        } else {
+            std::memmove(
+                obj->pending_writes,
+                obj->pending_writes + completed,
+                sizeof(lean_ssl_pending_write) * obj->pending_writes_count
+            );
+            // Keep memory usage proportional to currently queued writes.
+            lean_ssl_pending_write * shrunk = (lean_ssl_pending_write*)realloc(
+                obj->pending_writes,
+                sizeof(lean_ssl_pending_write) * obj->pending_writes_count
+            );
+            if (shrunk != nullptr) {
+                obj->pending_writes = shrunk;
+            }
+        }
+    }
+
+    return obj->pending_writes_count == 0 ? 1 : 0;
+}
+
+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);
+    }
+
+    free_pending_writes(obj);
+    free(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);
+    SSL_set_mode(ssl, SSL_MODE_AUTO_RETRY);
+
+    if (is_server) {
+        SSL_set_accept_state(ssl);
+    } else {
+        SSL_set_connect_state(ssl);
+    }
+
+    lean_ssl_session_object * ssl_obj = (lean_ssl_session_object*)malloc(sizeof(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;
+    ssl_obj->pending_writes_count = 0;
+    ssl_obj->pending_writes = nullptr;
+
+    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.setServerName (ssl : @& Session) (host : @& String) : IO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg _role, 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 Bool */
+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 lean_io_result_mk_ok(lean_box(1));
+    }
+
+    int err = SSL_get_error(ssl_obj->ssl, rc);
+    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    return mk_ssl_io_error("SSL_do_handshake failed", err);
+}
+
+/* Std.Internal.SSL.Session.write (ssl : @& Session) (data : @& ByteArray) : IO Bool */
+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 lean_io_result_mk_ok(lean_box(1));
+    }
+
+    int err = 0;
+    int step = ssl_write_step(ssl_obj, payload, data_len, &err);
+    if (step == 1) {
+        return lean_io_result_mk_ok(lean_box(1));
+    }
+
+    // If renegotiation blocks writes, queue plaintext and retry after subsequent reads.
+    if (step == 0 && err == SSL_ERROR_WANT_READ) {
+        if (!append_pending_write(ssl_obj, payload, data_len)) {
+            return mk_ssl_io_error("failed to append pending SSL write");
+        }
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    if (step == 0 && (err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN)) {
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    return mk_ssl_io_error("SSL_write failed", err);
+}
+
+/* Std.Internal.SSL.Session.read? (ssl : @& Session) (maxBytes : UInt64) : IO (Option ByteArray) */
+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 lean_io_result_mk_ok(mk_option_some(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 lean_io_result_mk_ok(mk_option_some(out));
+    }
+
+    lean_dec(out);
+
+    int err = SSL_get_error(ssl_obj->ssl, rc);
+    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || 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 lean_io_result_mk_ok(mk_option_none());
+    }
+
+    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 _role, 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,53 @@
+/*
+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
+
+namespace lean {
+
+static lean_external_class * g_ssl_session_external_class = nullptr;
+void initialize_openssl_session();
+
+#ifndef LEAN_EMSCRIPTEN
+typedef struct {
+    char * data;
+    size_t size;
+} lean_ssl_pending_write;
+
+typedef struct {
+    SSL * ssl;
+    BIO * read_bio;
+    BIO * write_bio;
+    size_t pending_writes_count;
+    lean_ssl_pending_write * pending_writes;
+} lean_ssl_session_object;
+
+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 _role, 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/elab/12897.lean

@@ -1,25 +1,12 @@
--- Tests that `normalizeInstance` auxiliary definitions work correctly
--- when used inside a `meta` section, for both `inferInstanceAs` and `deriving`.
+-- Tests that `inferInstanceAs` auxiliary definitions are properly marked `meta`
+-- when used inside a `meta` section.
 
 module
 
-public meta import Lean.Elab.Command
+meta section
 
-public meta section
+def Foo := List Nat
 
-namespace Test
+instance : EmptyCollection Foo := inferInstanceAs (EmptyCollection (List Nat))
 
-open Lean
-
--- `@[expose]` forces `normalizeInstance` to create aux wrapper definitions,
--- which is where the meta marking matters.
-@[expose] def Foo := Unit
-deriving Inhabited
-
-@[expose] def Bar := Name
-deriving Inhabited
-
-@[expose] def Baz := List Nat
-instance : EmptyCollection Baz := inferInstanceAs (EmptyCollection (List Nat))
-
-end Test
+end

tests/elab/13043.lean

@@ -1,20 +0,0 @@
--- Tests that `deriving` instances inside a `meta section` are properly marked `meta`.
--- Regression test for https://github.com/leanprover/lean4/pull/13043
-
-module
-
-public meta import Lean.Elab.Command
-
-public meta section
-
-namespace Test
-
-open Lean
-
-@[expose] def Foo := Unit
-deriving Inhabited
-
-@[expose] def Bar := Name
-deriving Inhabited
-
-end Test

tests/elab/async_ssl.lean

@@ -0,0 +1,238 @@
+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, sd)
+
+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
+  assertEqStr (String.fromUTF8! (received.getD ByteArray.empty)) "hello, tls!"
+
+  -- After draining, pendingEncrypted drops to 0.
+  let pendingAfter ← clientSess.pendingEncrypted
+  assertEqN pendingAfter 0 "pendingEncrypted after drain"
+
+  -- read? returns none when no data is available.
+  let empty ← clientSess.read? 1024
+  unless empty == none do
+    throw <| IO.userError "expected none 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
+
+-- ---------------------------------------------------------------------------
+-- 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

tests/elab/inferInstanceAs.lean

@@ -13,12 +13,6 @@ def D := I
 
 instance : C D := inferInstanceAs (C I)
 
--- We can still use it as an `inferInstance` synonym in the old mode
-set_option backward.inferInstanceAs.wrap false in
-/-- info: «inferInstanceAs» (C D) : C D -/
-#guard_msgs in
-#check inferInstanceAs (C D)
-
 /--
 info: @[implicit_reducible] private def instCD : C D :=
 { c := instCD._aux_1 }

tests/elab/lcnf_borrow_expected_type.lean

@@ -139,6 +139,8 @@ structure Quad where
 /-- Only traverses → parameter stays borrowed. -/
 @[noinline] def measuree (xs : List Nat) : Nat := xs.length
 
+/-
+
 /--
 trace: [Compiler.explicitRc] size: 22
     def cascadeDemo @&t : tobj :=
@@ -255,3 +257,5 @@ def preserveTailCall (x : @&Prod Nat Nat) (a : Nat) : Nat :=
   match a with
   | 0 => x.fst
   | a + 1 => preserveTailCall (mkNewProd x a) a
+
+-/

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/pkg/sym_ext/SymExt.lean

@@ -1,28 +0,0 @@
-/-
-Tests for `SymExtension` mechanism.
--/
-module
-public meta import SymExt.Decl
-meta import Lean.Meta.Sym
-
-open Lean Elab Tactic Meta Sym
-
-run_meta SymM.run do
-  let c0 ← getMyCounter
-  assert! c0 == 0
-  incrementMyCounter
-  let c1 ← getMyCounter
-  assert! c1 == 1
-  incrementMyCounter
-  let c2 ← getMyCounter
-  assert! c2 == 2
-
-run_meta do
-  SymM.run do
-    incrementMyCounter
-    let c ← getMyCounter
-    assert! c == 1
-  -- Should reset the counter
-  SymM.run do
-    let c ← getMyCounter
-    assert! c == 0

tests/pkg/sym_ext/SymExt/Decl.lean

@@ -1,20 +0,0 @@
-/-
-Declare a SymExtension and register it.
--/
-module
-public import Lean.Meta.Sym.SymM
-open Lean Meta Sym
-
-/-- Simple counter state for testing. -/
-public structure MyExtState where
-  counter : Nat := 0
-  deriving Inhabited
-
-initialize myExt : SymExtension MyExtState ←
-  registerSymExtension (return {})
-
-public def getMyCounter : SymM Nat := do
-  return (← myExt.getState).counter
-
-public def incrementMyCounter : SymM Unit := do
-  myExt.modifyState fun s => { s with counter := s.counter + 1 }

tests/pkg/sym_ext/lakefile.lean

@@ -1,5 +0,0 @@
-import Lake
-open System Lake DSL
-
-package sym_ext
-@[default_target] lean_lib SymExt

tests/pkg/sym_ext/lean-toolchain

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

tests/pkg/sym_ext/run_test.sh

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