From be72849d4896b2149e2d6c83789d7eb7a1d7cd85 Mon Sep 17 00:00:00 2001
From: Daly Brown <47283601+dalybrown@users.noreply.github.com>
Date: Thu, 4 Apr 2024 15:52:14 -0400
Subject: [PATCH 1/5] Expose DTLS in Ada wrapper and update examples

---
 wrapper/Ada/.gitignore        |   1 +
 wrapper/Ada/README.md         |   9 +--
 wrapper/Ada/default.gpr       |   4 --
 wrapper/Ada/spark_sockets.adb |  42 +++++++++++++-
 wrapper/Ada/spark_sockets.ads |   7 ++-
 wrapper/Ada/tls_client.adb    |  71 ++++++++++++++++++-----
 wrapper/Ada/tls_server.adb    | 103 +++++++++++++++++++++++++---------
 wrapper/Ada/user_settings.h   |  10 +---
 wrapper/Ada/wolfssl.adb       |  80 ++++++++++++++++++++++++++
 wrapper/Ada/wolfssl.ads       |  25 +++++++++
 10 files changed, 293 insertions(+), 59 deletions(-)
 create mode 100644 wrapper/Ada/.gitignore

diff --git a/wrapper/Ada/.gitignore b/wrapper/Ada/.gitignore
new file mode 100644
index 000000000..b672fdeaf
--- /dev/null
+++ b/wrapper/Ada/.gitignore
@@ -0,0 +1 @@
+obj
diff --git a/wrapper/Ada/README.md b/wrapper/Ada/README.md
index 0af9eafc0..76f4b8e8b 100644
--- a/wrapper/Ada/README.md
+++ b/wrapper/Ada/README.md
@@ -2,7 +2,7 @@
 The source code for the Ada/SPARK binding of the WolfSSL library
 is the WolfSSL Ada package in the wolfssl.ads and wolfssl.adb files.
 
-The source code here also demonstrates a TLS v1.3 server and client
+The source code here also demonstrates a (D)TLS v1.3 server and client
 using the WolfSSL Ada binding. The implementation is cross-platform
 and compiles on Linux, Mac OS X and Windows.
 
@@ -15,7 +15,8 @@ for the secondary stack. The GNAT User's Guide recommends
 avoiding the secondary stack using the restriction
 No_Secondary_Stack (see the GNAT configuration file gnat.adc
 which instructs compilation of the WolfSSL Ada binding under
-this restriction).
+this restriction). Note, however, that the examples do make use of the
+secondary stack.
 
 Portability: The WolfSSL Ada binding makes no usage of controlled types
 and has no dependency upon the Ada.Finalization package.
@@ -91,13 +92,13 @@ Make sure the executables for the compiler and GPRBuild are on the PATH
 and use gprbuild to build the source code.
 
 ## Files
-The TLS v1.3 client example in the Ada/SPARK programming language
+The (D)TLS v1.3 client example in the Ada/SPARK programming language
 using the WolfSSL library can be found in the files:
 tls_client_main.adb
 tls_client.ads
 tls_client.adb
 
-The TLS v1.3 server example in the Ada/SPARK programming language
+The (D)TLS v1.3 server example in the Ada/SPARK programming language
 using the WolfSSL library can be found in the files:
 tls_server_main.adb
 tls_server.ads
diff --git a/wrapper/Ada/default.gpr b/wrapper/Ada/default.gpr
index bbd3b34f1..42dcd745c 100644
--- a/wrapper/Ada/default.gpr
+++ b/wrapper/Ada/default.gpr
@@ -26,10 +26,6 @@ project Default is
       for Spec_Suffix ("C") use ".h";
    end Naming;
 
-   package Builder is
-      for Global_Configuration_Pragmas use "gnat.adc";
-   end Builder;
-
    package Compiler is
       for Switches ("C") use
          ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.
diff --git a/wrapper/Ada/spark_sockets.adb b/wrapper/Ada/spark_sockets.adb
index e315f230e..2edd8d08b 100644
--- a/wrapper/Ada/spark_sockets.adb
+++ b/wrapper/Ada/spark_sockets.adb
@@ -19,6 +19,7 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
+with Ada.Streams;
 with Interfaces.C;
 
 package body SPARK_Sockets is
@@ -33,16 +34,35 @@ package body SPARK_Sockets is
          return (Exists => False);
    end Inet_Addr;
 
-   procedure Create_Socket (Socket : in out Optional_Socket) is
+   procedure Create_Socket
+     (Socket : in out Optional_Socket;
+      Family : GNAT.Sockets.Family_Type;
+      Mode   : GNAT.Sockets.Mode_Type) is
       S : Socket_Type;
    begin
-      GNAT.Sockets.Create_Socket (S);
+      GNAT.Sockets.Create_Socket (S, Family, Mode);
       Socket := (Exists => True, Socket => S);
    exception
-      when others =>
+      when E : others =>
          Socket := (Exists => False);
    end Create_Socket;
 
+   procedure Create_Stream_Socket (Socket : in out Optional_Socket) is
+   begin
+      Create_Socket
+        (Socket => Socket,
+         Family => GNAT.Sockets.Family_Inet,
+         Mode   => GNAT.Sockets.Socket_Stream);
+   end Create_Stream_Socket;
+
+   procedure Create_Datagram_Socket (Socket : in out Optional_Socket) is
+   begin
+      Create_Socket
+        (Socket => Socket,
+         Family => GNAT.Sockets.Family_Inet,
+         Mode   => GNAT.Sockets.Socket_Datagram);
+   end Create_Datagram_Socket;
+
    function Connect_Socket (Socket : Socket_Type;
                             Server : Sock_Addr_Type)
                             return Subprogram_Result is
@@ -99,6 +119,22 @@ package body SPARK_Sockets is
          return Failure;
    end Listen_Socket;
 
+   function Receive_Socket
+     (Socket : Socket_Type)
+      return Subprogram_Result is
+
+      Item : Ada.Streams.Stream_Element_Array (1 .. 4096);
+      Last : Ada.Streams.Stream_Element_Offset;
+      From : GNAT.Sockets.Sock_Addr_Type;
+
+   begin
+      GNAT.Sockets.Receive_Socket (Socket, Item, Last, From);
+      return Success;
+   exception
+      when others =>
+         return Failure;
+   end Receive_Socket;
+
    procedure Accept_Socket (Server  : Socket_Type;
                             Socket  : out Optional_Socket;
                             Address : out Sock_Addr_Type;
diff --git a/wrapper/Ada/spark_sockets.ads b/wrapper/Ada/spark_sockets.ads
index ee9864c6f..5ac299863 100644
--- a/wrapper/Ada/spark_sockets.ads
+++ b/wrapper/Ada/spark_sockets.ads
@@ -83,7 +83,10 @@ package SPARK_Sockets with SPARK_Mode is
       end case;
    end record;
 
-   procedure Create_Socket (Socket : in out Optional_Socket) with
+   procedure Create_Stream_Socket (Socket : in out Optional_Socket) with
+      Pre => not Socket.Exists;
+
+   procedure Create_Datagram_Socket (Socket : in out Optional_Socket) with
       Pre => not Socket.Exists;
 
    function Connect_Socket (Socket : Socket_Type;
@@ -116,6 +119,8 @@ package SPARK_Sockets with SPARK_Mode is
    --  appropriate in usual cases. It can be adjusted according to each
    --  application's particular requirements.
 
+   function Receive_Socket (Socket : Socket_Type) return Subprogram_Result;
+
    procedure Accept_Socket (Server  : Socket_Type;
                             Socket  : out Optional_Socket;
                             Address : out Sock_Addr_Type;
diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb
index 88f5a60df..60b612d2a 100644
--- a/wrapper/Ada/tls_client.adb
+++ b/wrapper/Ada/tls_client.adb
@@ -137,6 +137,7 @@ package body Tls_Client with SPARK_Mode is
       Output : WolfSSL.Write_Result;
 
       Result : WolfSSL.Subprogram_Result;
+      DTLS   : Boolean := False;
    begin
       Result := WolfSSL.Initialize;
       if Result /= Success then
@@ -144,14 +145,29 @@ package body Tls_Client with SPARK_Mode is
          return;
       end if;
 
-      if Argument_Count < 1 then
-         Put_Line ("usage: tcl_client <IPv4 address>");
+      if Argument_Count < 1
+         or Argument_Count > 2
+         or (Argument_Count = 2 and then Argument (2) /= "--dtls")
+      then
+         Put_Line ("usage: tls_client_main <IPv4 address> [--dtls]");
          return;
       end if;
-      SPARK_Sockets.Create_Socket (C);
+
+      DTLS := (SPARK_Terminal.Argument_Count = 2);
+
+      if DTLS then
+         SPARK_Sockets.Create_Datagram_Socket (C);
+      else
+         SPARK_Sockets.Create_Stream_Socket (C);
+      end if;
+
       if not C.Exists then
-         Put_Line ("ERROR: Failed to create socket.");
-         return;
+         declare
+            Mode : constant String := (if DTLS then "datagram" else "stream");
+         begin
+            Put_Line ("ERROR: Failed to create " & Mode & " socket.");
+            return;
+         end;
       end if;
 
       Addr := SPARK_Sockets.Inet_Addr (Argument (1));
@@ -167,18 +183,26 @@ package body Tls_Client with SPARK_Mode is
             Addr   => Addr.Addr,
             Port   => P);
 
-      Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
-                                              Server => A);
-      if Result /= Success then
-         Put_Line ("ERROR: Failed to connect to server.");
-         SPARK_Sockets.Close_Socket (C);
-         Set (Exit_Status_Failure);
-         return;
+      if not DTLS then
+         Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket,
+                                                 Server => A);
+         if Result /= Success then
+            Put_Line ("ERROR: Failed to connect to server.");
+            SPARK_Sockets.Close_Socket (C);
+            Set (Exit_Status_Failure);
+            return;
+         end if;
       end if;
 
       --  Create and initialize WOLFSSL_CTX.
-      WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Client_Method,
-                              Context => Ctx);
+      WolfSSL.Create_Context
+        (Method  =>
+           (if DTLS then
+               WolfSSL.DTLSv1_3_Client_Method
+            else
+               WolfSSL.TLSv1_3_Client_Method),
+         Context => Ctx);
+
       if not WolfSSL.Is_Valid (Ctx) then
          Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
          SPARK_Sockets.Close_Socket (C);
@@ -186,6 +210,11 @@ package body Tls_Client with SPARK_Mode is
          return;
       end if;
 
+      --  Require mutual authentication.
+      WolfSSL.Set_Verify
+         (Context => Ctx,
+          Mode    => WolfSSL.Verify_Peer & WolfSSL.Verify_Fail_If_No_Peer_Cert);
+
       --  Load client certificate into WOLFSSL_CTX.
       Result := WolfSSL.Use_Certificate_File (Context => Ctx,
                                               File    => CERT_FILE,
@@ -241,6 +270,20 @@ package body Tls_Client with SPARK_Mode is
          return;
       end if;
 
+      if DTLS then
+      --  Set DTLS peer.
+         Result := WolfSSL.DTLS_Set_Peer(Ssl     => Ssl,
+                                         Address => A);
+         if Result /= Success then
+            Put_Line ("ERROR: Failed to set the DTLS peer.");
+            SPARK_Sockets.Close_Socket (C);
+            WolfSSL.Free (Ssl);
+            WolfSSL.Free (Context => Ctx);
+            Set (Exit_Status_Failure);
+            return;
+         end if;
+      end if;
+
       --  Attach wolfSSL to the socket.
       Result := WolfSSL.Attach (Ssl    => Ssl,
                                 Socket => SPARK_Sockets.To_C (C.Socket));
diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb
index 2858f26fd..7a08b1b4f 100644
--- a/wrapper/Ada/tls_server.adb
+++ b/wrapper/Ada/tls_server.adb
@@ -105,6 +105,7 @@ package body Tls_Server with SPARK_Mode is
       Ch : Character;
 
       Result : WolfSSL.Subprogram_Result;
+      DTLS   : Boolean := False;
       Shall_Continue : Boolean := True;
 
       Input  : WolfSSL.Read_Result;
@@ -117,12 +118,31 @@ package body Tls_Server with SPARK_Mode is
          return;
       end if;
 
-      SPARK_Sockets.Create_Socket (Socket => L);
-      if not L.Exists then
-         Put_Line ("ERROR: Failed to create socket.");
+      if SPARK_Terminal.Argument_Count > 1
+         or (SPARK_Terminal.Argument_Count = 1
+         and then SPARK_Terminal.Argument (1) /= "--dtls")
+      then
+         Put_Line ("usage: tls_server_main [--dtls]");
          return;
       end if;
 
+      DTLS := (SPARK_Terminal.Argument_Count = 1);
+
+      if DTLS then
+         SPARK_Sockets.Create_Datagram_Socket (Socket => L);
+      else
+         SPARK_Sockets.Create_Stream_Socket (Socket => L);
+      end if;
+
+      if not L.Exists then
+         declare
+            Mode : constant String := (if DTLS then "datagram" else "stream");
+         begin
+            Put_Line ("ERROR: Failed to create " & Mode & " socket.");
+            return;
+         end;
+      end if;
+
       Option := (Name => Reuse_Address, Enabled => True);
       Result := SPARK_Sockets.Set_Socket_Option (Socket => L.Socket,
                                                  Level  => Socket_Level,
@@ -144,17 +164,32 @@ package body Tls_Server with SPARK_Mode is
          return;
       end if;
 
-      Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket,
-                                             Length => 5);
+      if DTLS then
+         Result := SPARK_Sockets.Receive_Socket (Socket => L.Socket);
+      else
+         Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket,
+                                                Length => 5);
+      end if;
+
       if Result /= Success then
-         Put_Line ("ERROR: Failed to configure listener socket.");
-         SPARK_Sockets.Close_Socket (L);
-         return;
+         declare
+            Operation : constant String := (if DTLS then "receiver" else "listener");
+         begin
+            Put_Line ("ERROR: Failed to configure " & Operation & " socket.");
+            SPARK_Sockets.Close_Socket (L);
+            return;
+         end;
       end if;
 
       --  Create and initialize WOLFSSL_CTX.
-      WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Server_Method,
-                              Context => Ctx);
+      WolfSSL.Create_Context
+        (Method  =>
+           (if DTLS then
+               WolfSSL.DTLSv1_3_Server_Method
+            else
+               WolfSSL.TLSv1_3_Server_Method),
+         Context => Ctx);
+
       if not WolfSSL.Is_Valid (Ctx) then
          Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
          SPARK_Sockets.Close_Socket (L);
@@ -217,16 +252,18 @@ package body Tls_Server with SPARK_Mode is
          pragma Loop_Invariant (not WolfSSL.Is_Valid (Ssl));
          pragma Loop_Invariant (WolfSSL.Is_Valid (Ctx));
 
-         Put_Line ("Waiting for a connection...");
-         SPARK_Sockets.Accept_Socket (Server  => L.Socket,
-                                      Socket  => C,
-                                      Address => A,
-                                      Result  => Result);
-         if Result /= Success then
-            Put_Line ("ERROR: failed to accept the connection.");
-            SPARK_Sockets.Close_Socket (L);
-            WolfSSL.Free (Context => Ctx);
-            return;
+         if not DTLS then
+            Put_Line ("Waiting for a connection...");
+            SPARK_Sockets.Accept_Socket (Server  => L.Socket,
+                                         Socket  => C,
+                                         Address => A,
+                                         Result  => Result);
+            if Result /= Success then
+               Put_Line ("ERROR: failed to accept the connection.");
+               SPARK_Sockets.Close_Socket (L);
+               WolfSSL.Free (Context => Ctx);
+               return;
+            end if;
          end if;
 
          --  Create a WOLFSSL object.
@@ -241,8 +278,9 @@ package body Tls_Server with SPARK_Mode is
          end if;
 
          --  Attach wolfSSL to the socket.
-         Result := WolfSSL.Attach (Ssl    => Ssl,
-                                   Socket => SPARK_Sockets.To_C (C.Socket));
+         Result := WolfSSL.Attach
+           (Ssl    => Ssl,
+            Socket => SPARK_Sockets.To_C (if DTLS then L.Socket else C.Socket));
          if Result /= Success then
             Put_Line ("ERROR: Failed to set the file descriptor.");
             WolfSSL.Free (Ssl);
@@ -253,7 +291,7 @@ package body Tls_Server with SPARK_Mode is
             return;
          end if;
 
-         --  Establish TLS connection.
+         --  Establish (D)TLS connection.
          Result := WolfSSL.Accept_Connection (Ssl);
          if Result /= Success then
             Put_Line ("Accept error.");
@@ -268,7 +306,7 @@ package body Tls_Server with SPARK_Mode is
          Put_Line ("Client connected successfully.");
 
          Input := WolfSSL.Read (Ssl);
-         if not  Input.Success then
+         if not Input.Success then
             Put_Line ("Read error.");
             WolfSSL.Free (Ssl);
             SPARK_Sockets.Close_Socket (L);
@@ -306,15 +344,28 @@ package body Tls_Server with SPARK_Mode is
          end if;
 
          for I in 1 .. 3 loop
+
             Result := WolfSSL.Shutdown (Ssl);
+
+            if DTLS then
+               exit;
+            end if;
+
             exit when Result = Success;
             delay 0.001;  --  Delay is expressed in seconds.
+
          end loop;
-         if Result /= Success then
+         if not DTLS and then Result /= Success then
             Put_Line ("ERROR: Failed to shutdown WolfSSL context.");
          end if;
+
          WolfSSL.Free (Ssl);
-         SPARK_Sockets.Close_Socket (C);
+
+         if DTLS then
+            Shall_Continue := False;
+         else
+            SPARK_Sockets.Close_Socket (C);
+         end if;
 
          Put_Line ("Shutdown complete.");
       end loop;
diff --git a/wrapper/Ada/user_settings.h b/wrapper/Ada/user_settings.h
index df4ada44e..b66bb3224 100644
--- a/wrapper/Ada/user_settings.h
+++ b/wrapper/Ada/user_settings.h
@@ -75,13 +75,9 @@ extern "C" {
 #define WOLFSSL_TLS13_NO_PEEK_HANDSHAKE_DONE
 
 /* DTLS */
-#if 0
-    #define WOLFSSL_DTLS
-    #define WOLFSSL_MULTICAST
-
-    /* DTLS v1.3 is not yet included with enable-all */
-    //#define WOLFSSL_DTLS13
-#endif
+#define WOLFSSL_DTLS
+// #define WOLFSSL_MULTICAST
+#define WOLFSSL_DTLS13
 
 /* DG Disabled SSLv3 and TLSv1.0 - should avoid using */
 //#define WOLFSSL_ALLOW_SSLV3
diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb
index f1eac8f8a..811d4775a 100644
--- a/wrapper/Ada/wolfssl.adb
+++ b/wrapper/Ada/wolfssl.adb
@@ -19,7 +19,12 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
+pragma Warnings (Off, "* is an internal GNAT unit");
+with GNAT.Sockets.Thin_Common;
+pragma Warnings (On, "* is an internal GNAT unit");
+with Interfaces.C.Extensions;
 with Interfaces.C.Strings;
+with System;
 
 package body WolfSSL is
 
@@ -97,6 +102,46 @@ package body WolfSSL is
       return WolfTLSv1_3_Client_Method;
    end TLSv1_3_Client_Method;
 
+   function WolfDTLSv1_2_Server_Method return Method_Type with
+     Convention    => C,
+     External_Name => "wolfDTLSv1_2_server_method",
+     Import        => True;
+
+   function DTLSv1_2_Server_Method return Method_Type is
+   begin
+      return WolfDTLSv1_2_Server_Method;
+   end DTLSv1_2_Server_Method;
+
+   function WolfDTLSv1_2_Client_Method return Method_Type with
+     Convention    => C,
+     External_Name => "wolfDTLSv1_2_client_method",
+     Import        => True;
+
+   function DTLSv1_2_Client_Method return Method_Type is
+   begin
+      return WolfDTLSv1_2_Client_Method;
+   end DTLSv1_2_Client_Method;
+
+   function WolfDTLSv1_3_Server_Method return Method_Type with
+     Convention    => C,
+     External_Name => "wolfDTLSv1_3_server_method",
+     Import        => True;
+
+   function DTLSv1_3_Server_Method return Method_Type is
+   begin
+      return WolfDTLSv1_3_Server_Method;
+   end DTLSv1_3_Server_Method;
+
+   function WolfDTLSv1_3_Client_Method return Method_Type with
+     Convention    => C,
+     External_Name => "wolfDTLSv1_3_client_method",
+     Import        => True;
+
+   function DTLSv1_3_Client_Method return Method_Type is
+   begin
+      return WolfDTLSv1_3_Client_Method;
+   end DTLSv1_3_Client_Method;
+
    function WolfSSL_CTX_new (Method : Method_Type)
                              return Context_Type with
      Convention => C, External_Name => "wolfSSL_CTX_new", Import => True;
@@ -487,6 +532,41 @@ package body WolfSSL is
       return Subprogram_Result (Result);
    end Use_Private_Key_Buffer;
 
+   function WolfSSL_DTLS_Set_Peer
+     (ssl    : WolfSSL_Type;
+      peer   : GNAT.Sockets.Thin_Common.Sockaddr_Access;
+      peerSz : Interfaces.C.unsigned)
+      return int with
+     Convention    => C,
+     External_Name => "wolfSSL_dtls_set_peer",
+     Import        => True;
+
+   function DTLS_Set_Peer
+     (Ssl     : WolfSSL_Type;
+      Address : GNAT.Sockets.Sock_Addr_Type)
+      return Subprogram_Result is
+
+      Sin    : aliased GNAT.Sockets.Thin_Common.Sockaddr;
+      Length : Interfaces.C.int;
+
+   begin
+
+      GNAT.Sockets.Thin_Common.Set_Address
+        (Sin     => Sin'Unchecked_Access,
+         Address => Address,
+         Length  => Length);
+
+      pragma Assert (Length > 0);
+
+      return
+        Subprogram_Result
+          (WolfSSL_DTLS_Set_Peer
+             (ssl    => Ssl,
+              peer   => Sin'Unchecked_Access,
+              peerSz => Interfaces.C.unsigned (Length)));
+
+   end DTLS_Set_Peer;
+
    function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with
      Convention    => C,
      External_Name => "wolfSSL_set_fd",
diff --git a/wrapper/Ada/wolfssl.ads b/wrapper/Ada/wolfssl.ads
index a3f536e5d..361544630 100644
--- a/wrapper/Ada/wolfssl.ads
+++ b/wrapper/Ada/wolfssl.ads
@@ -19,6 +19,7 @@
 -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 --
 
+with GNAT.Sockets;
 with Interfaces.C;
 
 --  This package is annotated "with SPARK_Mode" that SPARK can verify
@@ -70,6 +71,22 @@ package WolfSSL with SPARK_Mode is
    --  This function is used to indicate that the application is a client
    --  and will only support the TLS 1.3 protocol.
 
+   function DTLSv1_2_Server_Method return Method_Type;
+   --  This function is used to indicate that the application is a server
+   --  and will only support the DTLS 1.2 protocol.
+
+   function DTLSv1_2_Client_Method return Method_Type;
+   --  This function is used to indicate that the application is a client
+   --  and will only support the DTLS 1.2 protocol.
+
+   function DTLSv1_3_Server_Method return Method_Type;
+   --  This function is used to indicate that the application is a server
+   --  and will only support the DTLS 1.3 protocol.
+
+   function DTLSv1_3_Client_Method return Method_Type;
+   --  This function is used to indicate that the application is a client
+   --  and will only support the DTLS 1.3 protocol.
+
    procedure Create_Context (Method  : Method_Type;
                              Context : out Context_Type);
    --  This function creates a new SSL context, taking a desired SSL/TLS
@@ -270,6 +287,14 @@ package WolfSSL with SPARK_Mode is
    --  Format specifies the format type of the buffer; ASN1 or PEM.
    --  Please see the examples for proper usage.
 
+   function DTLS_Set_Peer
+     (Ssl     : WolfSSL_Type;
+      Address : GNAT.Sockets.Sock_Addr_Type)
+      return Subprogram_Result with
+     Pre => Is_Valid (Ssl);
+   --  This function wraps the corresponding WolfSSL C function to allow
+   --  clients to use Ada socket types when implementing a DTLS client.
+
    function Attach (Ssl    : WolfSSL_Type;
                     Socket : Integer)
                     return Subprogram_Result with

From 63547d954a0c5d65fcb87a6f9d981865423fd6b8 Mon Sep 17 00:00:00 2001
From: Daly Brown <47283601+dalybrown@users.noreply.github.com>
Date: Thu, 4 Apr 2024 16:06:19 -0400
Subject: [PATCH 2/5] Fix formatting issues and remove unused variable

---
 wrapper/Ada/spark_sockets.adb | 2 +-
 wrapper/Ada/tls_client.adb    | 1 -
 wrapper/Ada/tls_server.adb    | 6 +-----
 3 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/wrapper/Ada/spark_sockets.adb b/wrapper/Ada/spark_sockets.adb
index 2edd8d08b..a662a010d 100644
--- a/wrapper/Ada/spark_sockets.adb
+++ b/wrapper/Ada/spark_sockets.adb
@@ -43,7 +43,7 @@ package body SPARK_Sockets is
       GNAT.Sockets.Create_Socket (S, Family, Mode);
       Socket := (Exists => True, Socket => S);
    exception
-      when E : others =>
+      when others =>
          Socket := (Exists => False);
    end Create_Socket;
 
diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb
index 60b612d2a..807b355ad 100644
--- a/wrapper/Ada/tls_client.adb
+++ b/wrapper/Ada/tls_client.adb
@@ -271,7 +271,6 @@ package body Tls_Client with SPARK_Mode is
       end if;
 
       if DTLS then
-      --  Set DTLS peer.
          Result := WolfSSL.DTLS_Set_Peer(Ssl     => Ssl,
                                          Address => A);
          if Result /= Success then
diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb
index 7a08b1b4f..09778c5d8 100644
--- a/wrapper/Ada/tls_server.adb
+++ b/wrapper/Ada/tls_server.adb
@@ -347,11 +347,7 @@ package body Tls_Server with SPARK_Mode is
 
             Result := WolfSSL.Shutdown (Ssl);
 
-            if DTLS then
-               exit;
-            end if;
-
-            exit when Result = Success;
+            exit when DTLS or Result = Success;
             delay 0.001;  --  Delay is expressed in seconds.
 
          end loop;

From 42f7be20c8045be3032a88ae69028a70bbcb75e7 Mon Sep 17 00:00:00 2001
From: Daly Brown <47283601+dalybrown@users.noreply.github.com>
Date: Thu, 4 Apr 2024 16:19:44 -0400
Subject: [PATCH 3/5] Fix assertion that address length must be greater than
 zero

---
 wrapper/Ada/wolfssl.adb | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/wrapper/Ada/wolfssl.adb b/wrapper/Ada/wolfssl.adb
index 811d4775a..068466ae3 100644
--- a/wrapper/Ada/wolfssl.adb
+++ b/wrapper/Ada/wolfssl.adb
@@ -556,7 +556,7 @@ package body WolfSSL is
          Address => Address,
          Length  => Length);
 
-      pragma Assert (Length > 0);
+      pragma Assert (Length >= 0);
 
       return
         Subprogram_Result

From 97e731f27b5656228ce30952d55028b59b6cac25 Mon Sep 17 00:00:00 2001
From: Daly Brown <47283601+dalybrown@users.noreply.github.com>
Date: Fri, 5 Apr 2024 12:09:11 -0400
Subject: [PATCH 4/5] Address gnatprove warnings and errors

---
 wrapper/Ada/tls_server.adb | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb
index 09778c5d8..28a032fdc 100644
--- a/wrapper/Ada/tls_server.adb
+++ b/wrapper/Ada/tls_server.adb
@@ -105,7 +105,7 @@ package body Tls_Server with SPARK_Mode is
       Ch : Character;
 
       Result : WolfSSL.Subprogram_Result;
-      DTLS   : Boolean := False;
+      DTLS : Boolean;
       Shall_Continue : Boolean := True;
 
       Input  : WolfSSL.Read_Result;
@@ -271,7 +271,11 @@ package body Tls_Server with SPARK_Mode is
          if not WolfSSL.Is_Valid (Ssl) then
             Put_Line ("ERROR: failed to create WOLFSSL object.");
             SPARK_Sockets.Close_Socket (L);
-            SPARK_Sockets.Close_Socket (C);
+
+            if not DTLS then
+               SPARK_Sockets.Close_Socket (C);
+            end if;
+
             WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
@@ -285,7 +289,11 @@ package body Tls_Server with SPARK_Mode is
             Put_Line ("ERROR: Failed to set the file descriptor.");
             WolfSSL.Free (Ssl);
             SPARK_Sockets.Close_Socket (L);
-            SPARK_Sockets.Close_Socket (C);
+
+            if not DTLS then
+               SPARK_Sockets.Close_Socket (C);
+            end if;
+
             WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
@@ -297,7 +305,11 @@ package body Tls_Server with SPARK_Mode is
             Put_Line ("Accept error.");
             WolfSSL.Free (Ssl);
             SPARK_Sockets.Close_Socket (L);
-            SPARK_Sockets.Close_Socket (C);
+
+            if not DTLS then
+               SPARK_Sockets.Close_Socket (C);
+            end if;
+
             WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;
@@ -310,7 +322,11 @@ package body Tls_Server with SPARK_Mode is
             Put_Line ("Read error.");
             WolfSSL.Free (Ssl);
             SPARK_Sockets.Close_Socket (L);
-            SPARK_Sockets.Close_Socket (C);
+
+            if not DTLS then
+               SPARK_Sockets.Close_Socket (C);
+            end if;
+
             WolfSSL.Free (Context => Ctx);
             Set (Exit_Status_Failure);
             return;

From 707e60aa79dca9cbe2370e60e2753eb14a0cd0c9 Mon Sep 17 00:00:00 2001
From: Daly Brown <47283601+dalybrown@users.noreply.github.com>
Date: Mon, 8 Apr 2024 19:40:06 -0400
Subject: [PATCH 5/5] Address gnatprove issues in tls client

---
 wrapper/Ada/tls_client.adb | 12 +++++++++---
 wrapper/Ada/tls_client.ads |  3 ++-
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb
index 807b355ad..3ec39320a 100644
--- a/wrapper/Ada/tls_client.adb
+++ b/wrapper/Ada/tls_client.adb
@@ -47,12 +47,18 @@ package body Tls_Client with SPARK_Mode is
       Ada.Text_IO.Put (Text);
    end Put;
 
-   procedure Put (Number : Natural) is
+   procedure Put (Number : Natural)
+   with
+     Annotate => (GNATprove, Might_Not_Return)
+   is
    begin
       Natural_IO.Put (Item => Number, Width => 0, Base => 10);
    end Put;
 
-   procedure Put (Number : Byte_Index) is
+   procedure Put (Number : Byte_Index)
+   with
+     Annotate => (GNATprove, Might_Not_Return)
+   is
    begin
       Natural_IO.Put (Item => Natural (Number), Width => 0, Base => 10);
    end Put;
@@ -137,7 +143,7 @@ package body Tls_Client with SPARK_Mode is
       Output : WolfSSL.Write_Result;
 
       Result : WolfSSL.Subprogram_Result;
-      DTLS   : Boolean := False;
+      DTLS   : Boolean;
    begin
       Result := WolfSSL.Initialize;
       if Result /= Success then
diff --git a/wrapper/Ada/tls_client.ads b/wrapper/Ada/tls_client.ads
index 50a52b3cc..aa1ad36e0 100644
--- a/wrapper/Ada/tls_client.ads
+++ b/wrapper/Ada/tls_client.ads
@@ -32,6 +32,7 @@ package Tls_Client with SPARK_Mode is
       Pre  => (not Client.Exists and not
                   WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)),
       Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and
-                  not WolfSSL.Is_Valid (Ctx));
+                  not WolfSSL.Is_Valid (Ctx)),
+     Annotate => (GNATprove, Might_Not_Return);
 
 end Tls_Client;