From 583b55feacdb641bb467c6ad8c3a790185dc8222 Mon Sep 17 00:00:00 2001
From: Amlal El Mahrouss <amlal@nekernel.org>
Date: Mon, 26 Jan 2026 02:56:49 +0100
Subject: chore: Fix scope leakage problem, adding proofs to NectarDriver.

Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>
---
 proofs/Makefile                                      | 13 +++++++++++++
 proofs/NectarDriver/Impl.v                           | 11 +++++++++++
 proofs/NectarDriver/Traits.v                         | 10 ++++++++++
 proofs/_CoqProject                                   |  4 ++++
 .../src/Compilers/NectarCompiler+AMD64.cc            | 20 +++++++++-----------
 5 files changed, 47 insertions(+), 11 deletions(-)
 create mode 100644 proofs/Makefile
 create mode 100644 proofs/NectarDriver/Impl.v
 create mode 100644 proofs/NectarDriver/Traits.v
 create mode 100644 proofs/_CoqProject

diff --git a/proofs/Makefile b/proofs/Makefile
new file mode 100644
index 0000000..1efedbc
--- /dev/null
+++ b/proofs/Makefile
@@ -0,0 +1,13 @@
+COQMAKEFILE ?= Makefile.coq
+
+all: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE)
+
+$(COQMAKEFILE): _CoqProject
+	coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+clean: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE) clean
+	rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
+
+.PHONY: all clean
\ No newline at end of file
diff --git a/proofs/NectarDriver/Impl.v b/proofs/NectarDriver/Impl.v
new file mode 100644
index 0000000..37b8878
--- /dev/null
+++ b/proofs/NectarDriver/Impl.v
@@ -0,0 +1,11 @@
+(*
+    NectarDriver: Impl keyword.
+
+    The Impl keyword defines methods and/or traits associated with a specific identifier N.
+
+    Author: Amlal El Mahrouss
+    Formalization: January 2026
+*)
+
+Require Import Logic.Classical_Prop.
+Require Import NectarDriver.Traits.
\ No newline at end of file
diff --git a/proofs/NectarDriver/Traits.v b/proofs/NectarDriver/Traits.v
new file mode 100644
index 0000000..2c5bb9c
--- /dev/null
+++ b/proofs/NectarDriver/Traits.v
@@ -0,0 +1,10 @@
+(*
+    NectarDriver: Traits keyword.
+
+    The Traits keyword defines formal semantic rules associated with a specific identifier N.
+
+    Author: Amlal El Mahrouss
+    Formalization: January 2026
+*)
+
+Require Import Logic.Classical_Prop.
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
new file mode 100644
index 0000000..62ede86
--- /dev/null
+++ b/proofs/_CoqProject
@@ -0,0 +1,4 @@
+-R NectarDriver NectarDriver
+
+NectarDriver/Impl.v
+NectarDriver/Trait.v
\ No newline at end of file
diff --git a/src/CompilerKit/src/Compilers/NectarCompiler+AMD64.cc b/src/CompilerKit/src/Compilers/NectarCompiler+AMD64.cc
index 63deddc..f395f6c 100644
--- a/src/CompilerKit/src/Compilers/NectarCompiler+AMD64.cc
+++ b/src/CompilerKit/src/Compilers/NectarCompiler+AMD64.cc
@@ -22,6 +22,7 @@
 #include <CompilerKit/PEF.h>
 #include <CompilerKit/UUID.h>
 #include <CompilerKit/Utilities/Compiler.h>
+#include "CompilerKit/Detail/Config.h"
 
 /* NeKernel NECTAR Compiler Driver. */
 /* This is part of the CompilerKit. */
@@ -363,10 +364,14 @@ CompilerKit::SyntaxLeafList::SyntaxLeaf CompilerFrontendNectarAMD64::Compile(
 
           auto tmp = left.substr(0, left.find(op.first));
 
-          kStdOut << tmp << "\n";
+          while (right.find(" ") != CompilerKit::STLString::npos)
+            tmp.erase(tmp.find(" "), 1);
+
+          while (right.find(" ") != CompilerKit::STLString::npos)
+            right.erase(right.find(" "), 1);
 
           if (auto var = nectar_find_variable(tmp); var) {
-            syntax_tree.fUserValue += "mov rdi, qword " + var->fRegister + "\n";
+            syntax_tree.fUserValue += "mov rdi, qword [rbp+" + std::to_string(-var->fStackOffset) + "]\n";
             delete var;
           } else {
             if (!isnumber(tmp[0])) {
@@ -376,10 +381,8 @@ CompilerKit::SyntaxLeafList::SyntaxLeaf CompilerFrontendNectarAMD64::Compile(
             syntax_tree.fUserValue += "mov rdi, " + tmp + "\n";
           }
 
-          kStdOut << right << "\n";
-
           if (auto var = nectar_find_variable(right); var) {
-            syntax_tree.fUserValue += "mov rsi, qword " + var->fRegister + "\n";
+            syntax_tree.fUserValue += "mov rsi, qword [rbp+" + std::to_string(-var->fStackOffset) + "]\n";
             delete var;
           }
 
@@ -544,11 +547,6 @@ CompilerKit::SyntaxLeafList::SyntaxLeaf CompilerFrontendNectarAMD64::Compile(
         // Pop function scope
         nectar_pop_scope();
 
-        // Clear function-local state
-        if (kFunctionEmbedLevel < 1) {
-          kContext.fVariables.clear();
-        }
-
         break;
       }
       case CompilerKit::KeywordKind::kKeywordKindDelete: {
@@ -1677,7 +1675,7 @@ NECTAR_MODULE(CompilerNectarAMD64) {
       CompilerKit::STLString err = "Unknown option: ";
       err += argv[index];
 
-      CompilerKit::Detail::print_error(err, "necdrv");
+      CompilerKit::Detail::print_error(err, "NectarDriver");
 
       continue;
     }
-- 
cgit v1.2.3