Logical call-stack frame stores capability metadata

theories/logrel/call_stack.v

@@ -8,10 +8,11 @@ From cap_machine Require Import cap_lang.
     kept track by the switcher.
 
     - [wret] records the value of [cra], the return pointer of the caller
-    - [wstk] records the value of [csp], the (compartment) stack frame of the caller
     - [wcgp] records the value of [cgp], the global data (compartment's memory) of the caller
     - [wcs0] records the value of [cs0], general purpose register
     - [wcs1] records the value of [cs1], general purpose register
+    - [b_stk], [a_stk] and  [e_stk] records the bounds of the stack capability [csp],
+    the (compartment) stack frame of the caller
 
     TODO: reformulate the following.
     In addition, it records whether the caller of the topmost frame
@@ -23,10 +24,12 @@ From cap_machine Require Import cap_lang.
  **)
 Record cframe := MkCFrame {
       wret : Word;
-      wstk : Word;
       wcgp : Word;
       wcs0 : Word;
       wcs1 : Word;
+      b_stk : Addr;
+      a_stk : Addr;
+      e_stk : Addr;
       is_untrusted_caller : bool;
   }.
 

theories/logrel/logrel.v

@@ -302,13 +302,16 @@ Section logrel.
     :=
     (λne (cstk : CSTK) (W : WORLD) (C : CmptName) (frm : cframe)
      ,
-       ∀ wca0 wca1 regs a_stk e_stk stk_mem_l stk_mem_h,
+       ∀ wca0 wca1 regs stk_mem_l stk_mem_h,
+       let b_stk := frm.(b_stk) in
+       let a_stk := frm.(a_stk) in
+       let e_stk := frm.(e_stk) in
        let astk4 := (a_stk ^+4)%a in
        let callee_stk_region := finz.seq_between (if frm.(is_untrusted_caller) then a_stk else astk4) e_stk in
        let callee_stk_mem := if frm.(is_untrusted_caller) then stk_mem_l++stk_mem_h else stk_mem_h in
        ( PC ↦ᵣ updatePcPerm frm.(wret)
          ∗ cra ↦ᵣ frm.(wret)
-         ∗ csp ↦ᵣ frm.(wstk)
+         ∗ csp ↦ᵣ (WCap RWL Local b_stk e_stk a_stk)
          (* cgp, cs0 and cs1 are callee-saved registers *)
          ∗ cgp ↦ᵣ frm.(wcgp)
          ∗ cs0 ↦ᵣ frm.(wcs0)
@@ -320,8 +323,6 @@ Section logrel.
          ∗ ⌜dom regs = all_registers_s ∖ {[PC; cra ; cgp; csp; cs0; cs1 ; ca0; ca1]}⌝
          ∗ ( [∗ map] r↦w ∈ regs, r ↦ᵣ w ∗ ⌜ w = WInt 0 ⌝ )
          (* points-to predicate of the stack region *)
-         ∗ ⌜ get_a frm.(wstk) = Some a_stk ⌝
-         ∗ ⌜ get_e frm.(wstk) = Some e_stk ⌝
          ∗ [[ a_stk , astk4 ]] ↦ₐ [[ stk_mem_l ]]
          ∗ [[ astk4 , e_stk ]] ↦ₐ [[ stk_mem_h ]]
          (* World interpretation *)
@@ -388,7 +389,7 @@ Section logrel.
              (* Continuation for the rest of the call-stack *)
              interp_cont_aux interp cstk' Ws' Cs'
              (* The callee stack frame must be safe, because we use the old copy of the stack to clear the stack *)
-             ∗ interp_callee_part_of_the_stack interp Wt Ct frm.(wstk) frm.(is_untrusted_caller)
+             ∗ interp_callee_part_of_the_stack interp Wt Ct (WCap RWL Local frm.(b_stk) frm.(e_stk) frm.(a_stk)) frm.(is_untrusted_caller)
              (* The continuation when matching the switcher's state at return-to-caller *)
              ∗ (∀ W', ⌜related_sts_pub_world Wt W'⌝
                       -∗  interp_cont_exec interp (interp_cont_aux interp cstk' Ws' Cs') cstk' W' Ct frm)))%I
@@ -408,9 +409,6 @@ Section logrel.
     f_equiv.
     f_equiv;[apply IHy|].
     f_equiv;[| repeat (f_equiv; auto)].
-    rewrite /interp_callee_part_of_the_stack.
-    destruct wstk; auto.
-    destruct sb ; auto.
     apply Heq.
   Qed.
 

theories/logrel/monotone.v

@@ -601,10 +601,7 @@ Proof.
   iNext.
   iSplitL "Hic";[|iSplitL "Hcallee"].
   - iFrame.
-  - rewrite /interp_callee_part_of_the_stack /=.
-    case_match=>//.
-    case_match=>//.
-    iApply (interp_monotone with "[//] [$]").
+  - iApply (interp_monotone with "[//] [$]").
   - iIntros (W'' Hrel').
     iApply "Hcont". iPureIntro.
     eapply related_sts_pub_trans_world;eauto.

theories/switcher/interp_switcher_call.v

@@ -964,10 +964,12 @@ Section fundamental.
 
     eset (frame :=
            {| wret := WInt 0;
-              wstk := (WCap RWL Local b e a);
               wcgp := WInt 0;
               wcs0 := WInt 0;
               wcs1 := WInt 0;
+              b_stk := b ;
+              a_stk := a ;
+              e_stk := e ;
               is_untrusted_caller := true
            |}).
 
@@ -993,7 +995,7 @@ Section fundamental.
     { iFrame. iNext. simpl.
       iSplit.
       - iApply (interp_weakening with "IH Hspv");auto;solve_addr.
-      - iIntros (W' HW' ???????) "(HPC & _)".
+      - iIntros (W' HW' ?????) "(HPC & _)".
         rewrite /interp_conf.
         wp_instr.
         iApply (wp_notCorrectPC with "[$]").

theories/switcher/interp_switcher_return.v

@@ -223,15 +223,6 @@ Section fundamental.
     rewrite /cframe_interp.
     iEval (cbn) in "Hcframe_interp".
     iDestruct "Hcframe_interp" as (wtstk4) "[Ha_tstk Hcframe_interp]".
-    destruct wstk; try done.
-    destruct sb; try done.
-    destruct p; try done.
-    destruct rx; try done.
-    destruct w; try done.
-    destruct dl; try done.
-    destruct dro; try done.
-    destruct g; try done.
-    rename a into a_stk; rename b into b_stk; rename e into e_stk.
     iDestruct "Hcframe_interp" as "(%HWF & -> & Hcframe_interp)".
     destruct HWF as (Hb_a4 & He_a1 & [a_stk4 Ha_stk4]).
     simpl in Hfreq. destruct Hfreq as (Hfrelated & <- & Hfreq).

theories/switcher/switcher_preamble.v

@@ -101,11 +101,11 @@ Section Switcher_preamble.
       with the stack pointer of the callee.
       See [execute_entry_point] to understand how they are related.
    *)
-  Definition csp_sync (cstk : CSTK) (a_stk e_stk : Addr) :=
+  Definition csp_sync (cstk : CSTK) (a_stk' e_stk' : Addr) :=
     match cstk with
     | frm::_ =>
-        get_a frm.(wstk) = Some a_stk
-        ∧ get_e frm.(wstk) = Some e_stk
+        frm.(a_stk) = a_stk'
+        ∧ frm.(e_stk) = e_stk'
     | _ => True
     end
   .
@@ -244,22 +244,20 @@ Section Switcher_preamble.
         and the content should match the words of the call-frame.
    *)
   Definition cframe_interp (frm : cframe) (a_tstk : Addr) : iProp Σ :=
+    let b_stk := frm.(b_stk) in
+    let a_stk := frm.(a_stk) in
+    let e_stk := frm.(e_stk) in
     ∃ (wtstk4 : Word),
       a_tstk ↦ₐ wtstk4 ∗
-      match frm.(wstk) with
-      | WCap RWL Local b_stk e_stk a_stk =>
-          (⌜ (b_stk <= a_stk)%a ∧ (a_stk ^+ 3 < e_stk)%a ∧ is_Some (a_stk + 4)%a ⌝
-           ∗ ⌜ wtstk4 = WCap RWL Local b_stk e_stk (a_stk ^+ 4)%a ⌝
-           ∗ if frm.(is_untrusted_caller)
-             then True
-             else
-               a_stk ↦ₐ frm.(wcs0)
-               ∗ (a_stk ^+ 1)%a ↦ₐ frm.(wcs1)
-               ∗ (a_stk ^+ 2)%a ↦ₐ frm.(wret)
-               ∗ (a_stk ^+ 3)%a ↦ₐ frm.(wcgp))%I
-      (* Constraints WFness of the register save area *)
-      | _ => False
-      end.
+      (⌜ (b_stk <= a_stk)%a ∧ (a_stk ^+ 3 < e_stk)%a ∧ is_Some (a_stk + 4)%a ⌝
+       ∗ ⌜ wtstk4 = WCap RWL Local b_stk e_stk (a_stk ^+ 4)%a ⌝
+       ∗ if frm.(is_untrusted_caller)
+         then True
+         else
+           a_stk ↦ₐ frm.(wcs0)
+           ∗ (a_stk ^+ 1)%a ↦ₐ frm.(wcs1)
+           ∗ (a_stk ^+ 2)%a ↦ₐ frm.(wret)
+           ∗ (a_stk ^+ 3)%a ↦ₐ frm.(wcgp))%I.
 
   (** [cstack_interp] interprets a call-stack.
       It simply interpret the topmost stack frame,

theories/switcher/switcher_spec_call.v

@@ -802,10 +802,12 @@ Section Switcher.
 
     set (frame :=
            {| wret := wcra_caller;
-              wstk := (WCap RWL Local b_stk e_stk a_stk);
               wcgp := wcgp_caller;
               wcs0 := wcs0_caller;
               wcs1 := wcs1_caller;
+              b_stk := b_stk;
+              a_stk := a_stk;
+              e_stk := e_stk;
               is_untrusted_caller := false
            |}).
 
@@ -881,7 +883,7 @@ Section Switcher.
       iSplit;[auto|]. iFrame "Htstk Hstk_interp".
       iSplit;[iPureIntro;solve_addr|].
       iSplit;[iPureIntro;solve_addr|].
-      iFrame.
+      iFrame; cbn.
       replace (a_stk ^+ 1)%a with a_stk1 by solve_addr+Hastk1.
       replace (a_stk ^+ 2)%a with a_stk2 by solve_addr+Hastk1 Hastk2.
       replace (a_stk ^+ 3)%a with a_stk3 by solve_addr+Hastk1 Hastk2 Hastk3.
@@ -917,10 +919,10 @@ Section Switcher.
       iEval (cbn).
       replace (a_stk ^+ 4)%a with a_stk4 by solve_addr. iSplitR.
       { iNext. iFrame "Hstk4v". }
-      iIntros "!>" (W' HW' ???????) "(HPC & Hcra & Hcsp & Hgp & Hcs0 & Hcs1 & Ha0 & #Hv
-      & Hca1 & #Hv' & % & Hregs & % & % & Hstk & Hstk' & Hr & Hcls & Hsts & Hcont & Hcstk & Own)".
+      iIntros "!>" (W' HW' ?????) "(HPC & Hcra & Hcsp & Hgp & Hcs0 & Hcs1 & Ha0 & #Hv
+      & Hca1 & #Hv' & % & Hregs & Hstk & Hstk' & Hr & Hcls & Hsts & Hcont & Hcstk & Own)".
       iApply "Hpost";iLeft. simplify_eq.
-      replace (a_stk0 ^+ 4)%a with a_stk4 by solve_addr.
+      replace (a_stk ^+ 4)%a with a_stk4 by solve_addr.
       iFrame "∗#%".
       iSplit.
       {

theories/switcher/switcher_spec_return.v

@@ -171,15 +171,6 @@ Section Switcher.
     rewrite /cframe_interp.
     iEval (cbn) in "Hcframe_interp".
     iDestruct "Hcframe_interp" as (wtstk4) "[Ha_tstk Hcframe_interp]".
-    destruct wstk; try done.
-    destruct sb; try done.
-    destruct p; try done.
-    destruct rx; try done.
-    destruct w; try done.
-    destruct dl; try done.
-    destruct dro; try done.
-    destruct g; try done.
-    rename a into a_stk; rename b into b_stk; rename e into e_stk.
     iDestruct "Hcframe_interp" as "(%HWF & -> & Hcframe_interp)".
     destruct HWF as (Hb_a4 & He_a1 & [a_stk4 Ha_stk4]).
     cbn in Hcsp_sync; destruct Hcsp_sync as [ Ha He ]; simplify_eq.
@@ -802,10 +793,7 @@ Section Switcher.
       iApply ("Hexec_topmost_frm" with
                "[] [$HPC $Hcra $Hcsp $Hcgp $Hcs0 $Hcs1 $Hca0 $Hca1 $Hinterp_Wfixed_wca0 $Hinterp_Wfixed_wca1
       $Hrmap $Hr $Hstk $Hstk' $Hsts $Hres $Hcont_K $Hcstk_frag $Hna]"); first done.
-
-      iSplitR.
-      { iPureIntro;rewrite Harg_rmap'; set_solver. }
-      iSplit; done.
+      iPureIntro;rewrite Harg_rmap'; set_solver.
 
     - (* Case where caller is untrusted, we use the IH *)