# UNDF: UNDF-2026-000001264
# CWE-668: Leaked Context -- LEAN_THREAD_PTR(g_opts) not reset at task boundaries
#
# Defect: g_opts is set per elaboration invocation but never cleared on task
#   completion. Thread pool reuse causes new task to inherit prior task's trace
#   options. Incorrect trace output; potential info leak across elab contexts.
#
# Fix: reset g_opts to nullptr in thread finalizer / task boundary cleanup.
#   Consistent with reset_thread_local() pattern used elsewhere in runtime.
#
# Complexity gate: correctness -- trace output isolated per task under concurrent elaboration
--- a/src/kernel/trace.cpp
+++ b/src/kernel/trace.cpp
@@ -6,10 +6,11 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <string>
 #include "util/io.h"
 #include "util/option_declarations.h"
 #include "library/elab_environment.h"
 #include "kernel/local_ctx.h"
 #include "kernel/trace.h"
+#include "runtime/thread.h"

 namespace lean {
 LEAN_THREAD_PTR(const options,               g_opts);
@@ -52,7 +53,14 @@ std::ostream & operator<<(std::ostream & ios, tclass const & c) {
 }

 void initialize_trace() {
+    // Register a reset function so that reset_thread_local() (called before
+    // each task starts on a reused thread) clears g_opts to nullptr.
+    // Without this, a thread-pool thread retains the prior elaboration task's
+    // trace options and leaks them into the next task's trace output.
+    register_thread_local_reset_fn([]() {
+        g_opts = nullptr;
+    });
 }

 void finalize_trace() {