From 38cddd5dc02f886e5cb3a0e386f0f7a1e6c8da86 Mon Sep 17 00:00:00 2001
From: Amlal El Mahrouss <amlal@nekernel.org>
Date: Sun, 1 Mar 2026 05:48:35 +0100
Subject: feat: ddk!: Breaking changes, the DDK has been reworked in C++
 instead. chore: public, kernel: fixes and important patches.

Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>
---
 proofs/Makefile           | 13 +++++++++++++
 proofs/NeKernel/HeapMgr.v | 10 ++++++++++
 proofs/_CoqProject        |  4 ++++
 3 files changed, 27 insertions(+)
 create mode 100644 proofs/Makefile
 create mode 100644 proofs/NeKernel/HeapMgr.v
 create mode 100644 proofs/_CoqProject

(limited to 'proofs')

diff --git a/proofs/Makefile b/proofs/Makefile
new file mode 100644
index 00000000..1efedbc7
--- /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/NeKernel/HeapMgr.v b/proofs/NeKernel/HeapMgr.v
new file mode 100644
index 00000000..2c5bb9ca
--- /dev/null
+++ b/proofs/NeKernel/HeapMgr.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 00000000..62ede86f
--- /dev/null
+++ b/proofs/_CoqProject
@@ -0,0 +1,4 @@
+-R NectarDriver NectarDriver
+
+NectarDriver/Impl.v
+NectarDriver/Trait.v
\ No newline at end of file
-- 
cgit v1.2.3