From 86d090ae3313e14b935deffbd8de328850bf822a Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Fri, 5 Dec 2025 21:10:17 +0100 Subject: [PATCH 1/3] Use 3rd person for switcher code documentation. See (https://developers.google.com/style/reference-verbs) and (https://www.oracle.com/technical-resources/articles/java/javadoc-tool.html#styleguide) --- theories/switcher/switcher.v | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/theories/switcher/switcher.v b/theories/switcher/switcher.v index 3464d465..5295dc01 100644 --- a/theories/switcher/switcher.v +++ b/theories/switcher/switcher.v @@ -8,7 +8,7 @@ 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; @@ -16,7 +16,7 @@ Section Switcher. 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; @@ -24,7 +24,7 @@ Section Switcher. 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 and *) 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,12 +81,12 @@ 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 ]. @@ -94,7 +94,7 @@ Section Switcher. encodeInstrsW [ (* --- Callback --- *) - (* Restores caller's stack frame *) + (* Restores the caller's stack frame *) ReadSR ctp mtdc; Load csp ctp; Lea ctp (-1)%Z; @@ -110,7 +110,7 @@ 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 @@ -118,10 +118,10 @@ Section Switcher. (* 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 ]. From fd55c55598491a73dd76ff81ef7bbf4a8eedf4c4 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Tue, 16 Dec 2025 11:58:19 +0100 Subject: [PATCH 2/3] Fix dune --- dune | 26 ++++++++++++++++++++++++++ dune-project | 4 ++-- 2 files changed, 28 insertions(+), 2 deletions(-) create mode 100644 dune diff --git a/dune b/dune new file mode 100644 index 00000000..1c3df710 --- /dev/null +++ b/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) +)) diff --git a/dune-project b/dune-project index 80137734..726ebee8 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ -(lang dune 3.18) -(using coq 0.8) +(lang dune 3.20) +(using coq 0.10) (name griotte) From d3afd1e0e451b88051c85fc9da1d1390eb04b592 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Tue, 16 Dec 2025 12:00:04 +0100 Subject: [PATCH 3/3] Fix documentations warnings --- theories/logrel/logrel.v | 6 +++--- theories/switcher/switcher_preamble.v | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/logrel/logrel.v b/theories/logrel/logrel.v index f4ead2f7..02d358d3 100644 --- a/theories/logrel/logrel.v +++ b/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. diff --git a/theories/switcher/switcher_preamble.v b/theories/switcher/switcher_preamble.v index 6b616bd8..f1b8a4d1 100644 --- a/theories/switcher/switcher_preamble.v +++ b/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 Σ :=