From 39b5cdd109f5fc8d93487ad33980b91305026a92 Mon Sep 17 00:00:00 2001
From: Antonin Reitz <antonin.reitz@inria.fr>
Date: Sat, 6 Jul 2024 03:05:46 +0200
Subject: [PATCH] some comments

---
 lib_avl_mono/Impl.Trees.Cast.M.fst |  2 ++
 src/ArrayAlignment.fst             |  2 ++
 src/ExternUtils.fst                | 10 +++++++++-
 src/FatalError.fst                 |  5 +----
 src/Mman.fst                       |  7 ++++---
 src/Mman2.fst                      |  2 ++
 6 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/lib_avl_mono/Impl.Trees.Cast.M.fst b/lib_avl_mono/Impl.Trees.Cast.M.fst
index 00d68c7..6bcd235 100644
--- a/lib_avl_mono/Impl.Trees.Cast.M.fst
+++ b/lib_avl_mono/Impl.Trees.Cast.M.fst
@@ -15,6 +15,8 @@ module G = FStar.Ghost
 open Constants
 open Utils2
 
+/// lib_avl_mono/Impl.Trees.Cast.M.fst contains axiomatization that is required to reuse the slab allocator for the allocation of the large allocation metadata AVL tree's nodes. In particular, it consists mostly of corresponding casts.
+
 // this is a compilation-time assert, see c/utils.c static_assert usage
 assume val avl_data_size_aux : v:U32.t{U32.v v <= 64}
 
diff --git a/src/ArrayAlignment.fst b/src/ArrayAlignment.fst
index d9d6e9e..b47e28a 100644
--- a/src/ArrayAlignment.fst
+++ b/src/ArrayAlignment.fst
@@ -12,6 +12,8 @@ unfold let same_base_array (#a: Type) (arr1 arr2: array a)
   =
   A.base (A.ptr_of arr1) == A.base (A.ptr_of arr2)
 
+/// src/ArrayAlignment.fst contains axiomatization of array alignments.
+
 // abstract property that the underlying pointer v-bytes aligned
 assume val array_u8_alignment (arr: array U8.t) (v: U32.t{U32.v v > 0}): prop
 
diff --git a/src/ExternUtils.fst b/src/ExternUtils.fst
index 01f7491..0307612 100644
--- a/src/ExternUtils.fst
+++ b/src/ExternUtils.fst
@@ -13,12 +13,15 @@ module A = Steel.Array
 
 open Utils2
 
+/// src/ExternUtils.fst contains axiomatizations of various compiler builtins or basic C code.
+///
 let check (_:unit)
   =
   assert (not (nth_is_zero U64.one (U32.uint_to_t 0)));
   assert (nth_is_zero U64.one (U32.uint_to_t 1));
   ()
 
+// bitwise-operations compiler builtin
 assume val ffs64 (x: U64.t) (bound: G.erased U32.t)
   : Pure U32.t
   (requires
@@ -34,6 +37,7 @@ assume val ffs64 (x: U64.t) (bound: G.erased U32.t)
 
 // count leading zeroes,
 // returns r, the number of rightmost bits set to zero
+// bitwise-operations compiler builtin
 assume val clz (x: U64.t)
   : Pure U32.t
   (requires U64.v x > 0)
@@ -45,6 +49,7 @@ assume val clz (x: U64.t)
 
 open FStar.Mul
 
+// compiler builtin
 assume val builtin_mul_overflow(x y: US.t)
   : Pure US.t
   (requires True)
@@ -53,7 +58,7 @@ assume val builtin_mul_overflow(x y: US.t)
     US.v r == US.v x * US.v y
   )
 
-
+// explicit_bzero zeroing function wrapper
 assume val apply_zeroing_u8
   (ptr: array U8.t)
   (n: US.t)
@@ -65,9 +70,11 @@ assume val apply_zeroing_u8
   )
   (ensures fun h0 _ h1 ->
     A.length ptr >= US.v n /\
+    // n first bytes of ptr are zeroes after execution of the function
     zf_u8 (Seq.slice (A.asel ptr h1) 0 (US.v n))
   )
 
+// check whether an array is zeroed
 assume val check_zeroing_u8
   (ptr: array U8.t)
   (n: US.t)
@@ -82,6 +89,7 @@ assume val check_zeroing_u8
     (b ==> zf_u8 (Seq.slice (A.asel ptr h1) 0 (US.v n)))
   )
 
+// memcpy function wrapper
 assume val memcpy_u8
   (dest src: array U8.t) (n: US.t)
   : Steel (array U8.t)
diff --git a/src/FatalError.fst b/src/FatalError.fst
index 1822c18..5be6288 100644
--- a/src/FatalError.fst
+++ b/src/FatalError.fst
@@ -12,10 +12,7 @@ open Config
 open Utils2
 open NullOrVarray
 
-// fatal_error wrappers
-// these functions only perform a fatal_error call
-// thus, postcondition does not really matter as it is are tailored
-// to respect caller postcondition so that verification works
+/// src/FatalError.fst contains context-specific wrappers of the C fatal_error function.
 
 open Impl.Trees.Cast.M
 open Impl.Trees.Types
diff --git a/src/Mman.fst b/src/Mman.fst
index 19dc7b4..7c69e45 100644
--- a/src/Mman.fst
+++ b/src/Mman.fst
@@ -16,6 +16,8 @@ open Constants
 open Config
 open Utils2
 
+/// Memory management axiomatizations
+
 /// 1) Initialization of the allocator
 // all functions with a _init suffix
 // are only meant to be used at initialization
@@ -113,7 +115,7 @@ open PtrdiffWrapper
 // POSIX spec: mmap returns a page-aligned array of bytes;
 // thus, mmap_u8 returns a page-aligned array of bytes;
 // hence the postcondition array_u8_alignment page_size
-//noextract
+/// mmap syscall wrapper
 assume val mmap_u8
   (size: US.t)
   : Steel (array U8.t)
@@ -131,8 +133,7 @@ assume val mmap_u8
     )
   )
 
-// TODO: should the underlying munmap fail in a stricter manner?
-//noextract
+/// munmap syscall wrapper
 assume val munmap_u8 (ptr: array U8.t) (size: US.t)
   : Steel unit
     (A.varray ptr)
diff --git a/src/Mman2.fst b/src/Mman2.fst
index c66dfd4..56539b6 100644
--- a/src/Mman2.fst
+++ b/src/Mman2.fst
@@ -7,6 +7,8 @@ module R = Steel.Reference
 open Impl.Trees.Types
 module G = FStar.Ghost
 
+/// Memory management axiomatizations
+
 assume val mmap_ptr_metadata_init (_:unit)
   : SteelT (R.ref t)
   emp