Documentation

dune

@@ -0,0 +1,26 @@
+;; The following trick is borrowed from a dune file of Coq-HoTT.
+(rule
+ (alias runtest)
+ (deps
+  (glob_files_rec ./*.vo))
+ (action
+  (run
+    rocqchk
+    -Q theories cap_machine
+    -Q machine_utils/theories machine_utils
+    %{deps}
+    -o)))
+
+;; Only compiles Rocq files.
+(alias
+ (name rocq-part)
+ (deps
+  (alias_rec theories/all)))
+
+;; Compile everything (including documentation).
+(alias
+ (name default)
+ (deps
+  (alias_rec doc)
+  (alias rocq-part)
+))

dune-project

@@ -1,5 +1,5 @@
-(lang dune 3.18)
-(using coq 0.8)
+(lang dune 3.20)
+(using coq 0.10)
 
 (name griotte)
 

theories/logrel/logrel.v

@@ -342,11 +342,11 @@ Section logrel.
 
   (** [interp_callee_part_of_the_stack] interprets the stack pointer of the caller [wstk].
       When a caller calls the switcher-call routine with a capability [WCap p g b e a] in the [csp]
-      register, the switcher is using the region `[a,a+4)` for as callee-saved registers area,
-      and giving the region `[a+4,e)` as callee-stack frame.
+      register, the switcher is using the region "[a,a+4)" for as callee-saved registers area,
+      and giving the region "[a+4,e)" as callee-stack frame.
 
       If the caller is trusted, the callee-saved registers area is expected to be solely accessed by the switcher,
-      sharing in fact only the region `[a+4,e)` with the caller.
+      sharing in fact only the region "[a+4,e)" with the caller.
 
       If the caller is untrusted, there are no guarantees that the caller won't share its entire stack frame
       with the callee, through one of the arguments.

theories/switcher/switcher.v

@@ -8,23 +8,23 @@ Section Switcher.
 
   Definition switcher_call_instrs : list Word :=
     encodeInstrsW [
-        (* Check permissions of the stack *)
+        (* Checks the permissions of the stack (RWL) *)
         GetP ct2 csp;
         Mov ctp (encodePerm RWL);
         Sub ct2 ct2 ctp;
         Jnz 2%Z ct2;
         Jmp 2%Z;
         Fail;
 
-        (* Check locality of the stack *)
+        (* Checks the locality of the stack (Local) *)
         GetL ct2 csp;
         Mov ctp (encodeLoc Local);
         Sub ct2 ct2 ctp;
         Jnz 2%Z ct2;
         Jmp 2%Z;
         Fail;
 
-        (* Save the callee registers *)
+        (* Saves the callee registers *)
         Store csp cs0;
         Lea csp 1%Z;
         Store csp cs1;
@@ -34,7 +34,7 @@ Section Switcher.
         Store csp cgp;
         Lea csp 1%Z;
 
-        (* Check that the trusted stack has enough space *)
+        (* Checks that the trusted stack has enough space *)
         ReadSR ct2 mtdc;
         GetA cs0 ct2;
         machine_base.Add cs0 cs0 1%Z;
@@ -43,20 +43,20 @@ Section Switcher.
         Jnz 2%Z ctp;
         Fail;
 
-        (* Save the caller's stack pointer in the trusted stack *)
+        (* Saves the caller's stack pointer in the trusted stack *)
         Lea ct2 1%Z;
         Store ct2 csp;
         WriteSR mtdc ct2;
 
-      (* Chop off the stack *)
+        (* Restricts the boundaries of the stack *)
         GetE cs0 csp;
         GetA cs1 csp;
         Subseg csp cs1 cs0
       ]
-      (* Zero out the callee's stack frame *)
+      (* Zeroes the callee's stack frame out *)
       ++ clear_stack_instrs cs0 cs1
       ++ encodeInstrsW [
-        (* Fetch (unsealing capability and unseal entry point *)
+        (* Fetches (un-)sealing capability and unseals the entry point *)
         GetB cs1 PC;
         GetA cs0 PC;
         Sub cs1 cs1 cs0;
@@ -66,12 +66,12 @@ Section Switcher.
         Load cs0 cs0;
         UnSeal ct1 cs0 ct1;
 
-        (* Load and decode entry point nargs and offset *)
+        (* Loads and decodes the entry point <nargs> and <offset> *)
         Load cs0 ct1;
         LAnd ct2 cs0 7%Z;
         LShiftR cs0 cs0 3%Z;
 
-        (* Prepare callee's PCC in cra, and callee's CGP in cgp *)
+        (* Prepares the callee's PCC in cra, and callee's CGP in cgp *)
         GetB cgp ct1;
         GetA cs1 ct1;
         Sub cs1 cgp cs1;
@@ -81,20 +81,20 @@ Section Switcher.
         Load cgp ct1;
         Lea cra cs0;
         machine_base.Add ct2 ct2 1%Z]
-      (* clear registers, skipping arguments *)
+      (* Clears the registers, skipping arguments *)
       ++ clear_registers_pre_call_skip_instrs
       ++ clear_registers_pre_call_instrs
       ++ encodeInstrsW [
 
-        (* Jump to callee *)
+        (* Jumps to the callee *)
         Jalr cra cra
       ].
 
   Definition switcher_return_instrs : list Word :=
     encodeInstrsW [
 
         (* --- Callback --- *)
-        (* Restores caller's stack frame *)
+        (* Restores the caller's stack frame *)
         ReadSR ctp mtdc;
         Load csp ctp;
         Lea ctp (-1)%Z;
@@ -110,18 +110,18 @@ Section Switcher.
         Lea csp (-1)%Z;
         Load cs0 csp;
 
-        (* Zero out the callee stack frame *)
+        (* Zeroes the callee stack frame out *)
         GetE ct0 csp;
         GetA ct1 csp]
       ++ clear_stack_instrs ct0 ct1
       ++ encodeInstrsW[
         (* Restores the return pointer to caller  *)
         Mov cra ca2
       ]
-      (* Clear registers *)
+      (* Clears the registers *)
       ++ clear_registers_post_call_instrs
       ++ encodeInstrsW [
-        (* Jump back to caller *)
+        (* Jumps back to the caller *)
         JmpCap cra
       ].
 

theories/switcher/switcher_preamble.v

@@ -82,8 +82,8 @@ Section Switcher_preamble.
       An important point is the use of [csp_sync] and the stack capability [WCap RWL Local a_stk4 e_stk a_stk4].
       If the call stack is not empty, we know that the caller's stack looks like
       [WCap RWL Local b_stk e_stk a_stk] (it is tested by the switcher's call routine).
-      The switcher reserves the area `[a_stk, a_stk+4)` for the callee-saved area,
-      and passes the rest, i.e. `[a_stk+4, e_stk)`  to the callee.
+      The switcher reserves the area "[a_stk, a_stk+4)" for the callee-saved area,
+      and passes the rest, i.e. "[a_stk+4, e_stk)"  to the callee.
 
       [csp_sync] synchronises the caller's stack pointer with the callee stack pointer.
       It's important when proving the functional specification of the return-to-switcher routine,
@@ -246,7 +246,7 @@ Section Switcher_preamble.
       as well as the unsealing capability of the switcher's otype.
 
       Finally, it holds the points-to predicates of the trusted stack.
-      The unused part `[a_tstk+1, e_trusted_stack)` contains some unknown values.
+      The unused part "[a_tstk+1, e_trusted_stack)" contains some unknown values.
       The used part is contained in the definition of [stack_interp].
    *)
   Definition switcher_inv : iProp Σ :=