Document mutex invariant for HMAC_DRBG

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>

include/mbedtls/hmac_drbg.h

@@ -101,6 +101,14 @@ typedef struct mbedtls_hmac_drbg_context
     void *p_entropy;            /*!< context for the entropy function        */
 
 #if defined(MBEDTLS_THREADING_C)
+    /* Invariant: the mutex is initialized if and only if
+     * md_ctx->md_info != NULL. This means that the mutex is initialized
+     * during the initial seeding in mbedtls_hmac_drbg_seed() or
+     * mbedtls_hmac_drbg_seed_buf() and freed in mbedtls_ctr_drbg_free().
+     *
+     * Note that this invariant may change without notice. Do not rely on it
+     * and do not access the mutex directly in application code.
+     */
     mbedtls_threading_mutex_t mutex;
 #endif
 } mbedtls_hmac_drbg_context;

library/hmac_drbg.c

@@ -254,6 +254,7 @@ int mbedtls_hmac_drbg_seed( mbedtls_hmac_drbg_context *ctx,
     if( ( ret = mbedtls_md_setup( &ctx->md_ctx, md_info, 1 ) ) != 0 )
         return( ret );
 
+    /* The mutex is initialized iff the md context is set up. */
 #if defined(MBEDTLS_THREADING_C)
     mbedtls_mutex_init( &ctx->mutex );
 #endif
@@ -425,6 +426,7 @@ void mbedtls_hmac_drbg_free( mbedtls_hmac_drbg_context *ctx )
         return;
 
 #if defined(MBEDTLS_THREADING_C)
+    /* The mutex is initialized iff the md context is set up. */
     if( ctx->md_ctx.md_info != NULL )
         mbedtls_mutex_free( &ctx->mutex );
 #endif