Https support via openssl (#2)

.github/workflows/build.yml

@@ -1,6 +1,6 @@
 on:
   push:
-    branches: master
+    branches: main
   pull_request:
 
 name: Build

HttpClient/Basic.lean

@@ -33,6 +33,23 @@ structure Request where
 
 namespace Internal
 
+opaque SSLConnection : Type
+
+@[extern "ssl_connection_create"]
+opaque SSLConnection.create : UInt32 → IO SSLConnection
+
+@[extern "ssl_connection_connect"]
+opaque SSLConnection.connect : SSLConnection → IO Unit
+
+@[extern "ssl_connection_shutdown"]
+opaque SSLConnection.shutdown : SSLConnection → IO Unit
+
+@[extern "ssl_connection_write"]
+opaque SSLConnection.write : SSLConnection → ByteArray → IO Unit
+
+@[extern "ssl_connection_read"]
+opaque SSLConnection.read : SSLConnection → UInt32 → IO ByteArray
+
 def renderPath (uri : Http.URI) : String :=
   path ++ query
   where
@@ -55,8 +72,9 @@ def toRequestString [ToString T] (r : Http.Request T) : String :=
 def connect (uri : URI) : IO Connection := do
   let auth := uri.uri.auth.get uri.hasAuth
   let host := auth.host
+  let secure := uri.uri.scheme == Http.URI.Scheme.HTTPS
   let service := match auth.port with
-    | .none => "http"
+    | .none => if secure then "https" else "http"
     | .some p => toString p
 
   -- call getaddrinfo(3) to resolve the host
@@ -73,10 +91,20 @@ def connect (uri : URI) : IO Connection := do
     let sock ← Socket.mk .inet .stream
     try
       sock.connect addr
-      Connection.make
-        (λ c => sock.send c >>= λ _ => pure ())
-        (.some <$> sock.recv 4096)
-        sock.close
+      if secure
+        then do
+          let fd ← sock.getFd
+          let sslConnection ← SSLConnection.create fd
+          sslConnection.connect
+          Connection.make
+            sslConnection.write
+            (.some <$> sslConnection.read 4096)
+            (sslConnection.shutdown *> sock.close)
+        else do
+          Connection.make
+            (λ c => sock.send c >>= λ _ => pure ())
+            (.some <$> sock.recv 4096)
+            sock.close
     catch e =>
       sock.close
       throw e
@@ -126,5 +154,3 @@ def runRequest (connection : Connection) (request : Request)
   | .error e => throw (IO.userError s!"can't parse response {e}")
 
 end Internal
-
-end HttpClient

Main.lean

@@ -1,5 +1,7 @@
 import HttpClient
 
+
 def main : IO Unit := do
   let resp ← HttpClient.http .GET "http://localhost:8080" .none
+  -- let resp ← HttpClient.http .GET "http://www.google.com" .none
   IO.println s!"{resp.toString}"

lake-manifest.json

@@ -55,13 +55,13 @@
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargoniX/socket.lean",
+  {"url": "https://github.com/Yuras/socket.lean.git",
    "type": "git",
    "subDir": null,
-   "rev": "8e036b3c9460b433eaff28beefccbc6d8e3245b8",
+   "rev": "43732133cd97bf6e11084bee5d0d0b4addb5a7fa",
    "name": "socket",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "http-client",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/algebraic-sofia/soda",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 require Http from git "https://github.com/Yuras/lean4-http" @ "http-client"
-require socket from git "https://github.com/hargoniX/socket.lean" @ "main"
+require socket from git "https://github.com/Yuras/socket.lean.git" @ "http-client"
 require soda from git "https://github.com/algebraic-sofia/soda" @ "main"
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "stable"
 
@@ -15,9 +15,11 @@ lean_lib «HttpClient» where
 @[default_target]
 lean_exe «http-client-main» where
   root := `Main
+  moreLinkArgs := #["-lssl"]
 
 lean_exe «http-client-spec» where
   root := `Spec
+  moreLinkArgs := #["-lssl"]
 
 target http.o pkg : FilePath := do
   let oFile := pkg.buildDir / "native" / "http.o"

native/http.c

@@ -4,6 +4,7 @@
 #include <errno.h>
 #include <string.h>
 #include <sys/socket.h>
+#include <openssl/ssl.h>
 
 /*********************/
 
@@ -93,3 +94,88 @@ uint16_t addr_info_list_inet_get_port(lean_obj_arg lean_list) {
 	struct sockaddr_in* in = (struct sockaddr_in*)(list->current->ai_addr);
 	return htons(in->sin_port);
 }
+
+/*********************/
+
+struct ssl_connection {
+	SSL_CTX* ctx;
+	SSL* ssl;
+};
+
+static lean_external_class* ssl_connection_class = NULL;
+
+static void ssl_connection_finalize(void * obj) {
+	struct ssl_connection* connection = (struct ssl_connection*)obj;
+	SSL_shutdown(connection->ssl);
+	SSL_free(connection->ssl);
+	SSL_CTX_free(connection->ctx);
+	free(connection);
+}
+
+static void ssl_connection_foreach(void *, b_lean_obj_arg) {
+	// no nested lean objects
+}
+
+static lean_object* ssl_connection_to_lean(struct ssl_connection* connection) {
+	if (ssl_connection_class == NULL) {
+		ssl_connection_class = lean_register_external_class(
+			ssl_connection_finalize,
+			ssl_connection_foreach
+		);
+	}
+	return lean_alloc_external(ssl_connection_class, connection);
+}
+
+lean_obj_res ssl_connection_create(uint32_t fd) {
+	struct ssl_connection* connection = malloc(sizeof(struct ssl_connection));
+	const SSL_METHOD* method = TLS_client_method();
+	connection->ctx = SSL_CTX_new(method);
+	connection->ssl = SSL_new(connection->ctx);
+	SSL_set_fd(connection->ssl, fd);
+	return lean_io_result_mk_ok(ssl_connection_to_lean(connection));
+}
+
+lean_obj_res ssl_connection_connect(lean_obj_arg lean_connection) {
+	struct ssl_connection* connection = lean_get_external_data(lean_connection);
+	int err = SSL_connect(connection->ssl);
+	if (err < 0) {
+		return lean_io_result_mk_error(
+			lean_mk_io_error_other_error(-err, lean_mk_string("SSL_connect failed"))
+		);
+	}
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res ssl_connection_shutdown(lean_obj_arg lean_connection) {
+	struct ssl_connection* connection = lean_get_external_data(lean_connection);
+	int err = SSL_shutdown(connection->ssl);
+	if (err < 0) {
+		printf("shutdown: %i\n (ignoring)", err);
+	}
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res ssl_connection_write(lean_obj_arg lean_connection, lean_obj_arg lean_buf) {
+	struct ssl_connection* connection = lean_get_external_data(lean_connection);
+	int err = SSL_write(connection->ssl, lean_sarray_cptr(lean_buf), lean_sarray_size(lean_buf));
+	if (err < 0) {
+		return lean_io_result_mk_error(
+			lean_mk_io_error_other_error(-err, lean_mk_string("SSL_write failed"))
+		);
+	}
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res ssl_connection_read(lean_obj_arg lean_connection, uint32_t max) {
+	struct ssl_connection* connection = lean_get_external_data(lean_connection);
+	lean_object* lean_buf = lean_alloc_sarray(1, 0, max);
+	int len = SSL_read(connection->ssl, lean_sarray_cptr(lean_buf), max);
+	if (len < 0) {
+		return lean_io_result_mk_error(
+			lean_mk_io_error_other_error(-len, lean_mk_string("SSL_read failed"))
+		);
+	}
+	lean_sarray_object* array = lean_to_sarray(lean_buf);
+	array->m_size = len;
+	return lean_io_result_mk_ok(lean_buf);
+}