WIP proof TC example: setup for custom enclave predicates

theories/examples/enclaves/trusted_compute.v

@@ -148,7 +148,7 @@ Section trusted_compute_example.
         Load r_t1 r_t1
       ]
       ++ assert_reg_instrs assert_lt_offset r_t1
-      ++ encodeInstrsLW [Halt]
+      ++ encodeInstrsLW [Mov r_t0 0 ; Mov r_t3 0 ; Halt]
       ++ (* fails: *) encodeInstrsLW [Fail].
 
   Definition trusted_compute_main_init_len : Z :=
@@ -277,8 +277,48 @@ Section trusted_compute_example.
 
   Definition flag_assertN := (trusted_computeN.@"flag_assert").
   Definition flag_inv a_flag v_flag :=
-    inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z) .
-
+    inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z).
+
+  (* TODO: move somewhere else, this is not specific to trusted compute *)
+  Record CustomEnclave :=
+    MkCustomEnclave {
+        code : list LWord;
+        code_region : LAddr;
+        Penc : LWord -> iProp Σ;
+        Psign : LWord -> iProp Σ;
+      }.
+
+  Definition custom_enclaves_map : Type :=
+    gmap EIdentity CustomEnclave.
+
+  Definition custom_enclaves_map_wf (cenclaves : custom_enclaves_map) :=
+    map_Forall
+      (fun I ce => I = hash_concat (hash (code_region ce)) (hash (code ce)))
+      cenclaves.
+
+  Definition custom_enclaveN := (trusted_computeN.@"custom_enclave").
+  Definition custom_enclave_inv (cenclaves : custom_enclaves_map) :=
+    inv custom_enclaveN
+      (
+        ⌜ custom_enclaves_map_wf cenclaves ⌝ -∗
+        □ ∀ (I : EIdentity) (tid : TIndex) (ot : OType) (ce : CustomEnclave),
+          enclave_all tid I
+          ∗ ⌜ cenclaves !! I = Some ce ⌝
+          ∗ ⌜ has_seal ot tid ⌝ -∗
+          seal_pred ot (Penc ce)
+          ∗ seal_pred (ot ^+ 1)%ot (Psign ce)
+      ).
+
+  (* Trusted Compute Custom Predicates *)
+  Definition tc_enclave_pred tc_data_cap tc_addr : CustomEnclave :=
+   MkCustomEnclave
+     (trusted_compute_enclave_code tc_data_cap)
+     tc_addr
+     sealed_42 (* TODO: should be false ! *)
+     sealed_42.
+
+  Definition tcenclaves_map tc_data_cap tc_addr : custom_enclaves_map :=
+   {[hash_trusted_compute_enclave := tc_enclave_pred tc_data_cap tc_addr]}.
 
   Lemma trusted_compute_callback_code_spec
     (b_main adv adv_end: Addr)
@@ -288,6 +328,7 @@ Section trusted_compute_example.
     (assert_lt_offset : Z)
     (b_assert e_assert a_flag : Addr) (v_assert : Version) (* assert *)
     (w0 w1 w2 w3 w4 w5 : LWord)
+    tc_data_cap tc_addr
     φ :
 
     let v_link := pc_v in
@@ -304,11 +345,15 @@ Section trusted_compute_example.
     (a_link + assert_lt_offset)%a = Some assert_entry →
     withinBounds b_link e_link assert_entry = true ->
 
+    (* TODO: should be proved *)
+    custom_enclaves_map_wf (tcenclaves_map tc_data_cap tc_addr) ->
+
     (link_table_inv
        v_link
        assert_entry b_assert e_assert v_assert
     ∗ assert_inv b_assert a_flag e_assert v_assert
     ∗ flag_inv a_flag v_assert)
+    ∗ custom_enclave_inv (tcenclaves_map tc_data_cap tc_addr)
     ∗ interp w1
     ∗ interp w0
 
@@ -329,9 +374,9 @@ Section trusted_compute_example.
           (* NOTE this post-condition stops after jumping to the adversary *)
           ∗ ▷ ( codefrag b_main pc_v trusted_compute_main
                 ∗ ((a_data)%a, pc_v) ↦ₐ link_cap
-                ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LWInt 0%Z)
+                ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LCap RWX b_main e_main a_data pc_v)
 
-                ∗ PC ↦ᵣ LCap RWX b_main e_main a_data pc_v
+                ∗ PC ↦ᵣ LCap RX b_main e_main (a_data ^+ (-2))%a pc_v
                 ∗ r_t0 ↦ᵣ LInt 0
                 ∗ r_t1 ↦ᵣ LInt 0
                 ∗ r_t2 ↦ᵣ LInt 0
@@ -355,8 +400,8 @@ Section trusted_compute_example.
           /trusted_compute_main_init_len /trusted_compute_main_callback_len
       ; solve_addr.
 
-    intros ?????? Hregion Hassert Hlink.
-    iIntros "#[ [HlinkInv [HassertInv HflagInv] ] [ Hinterp_w1 Hinterp_w0] ]
+    intros ?????? Hregion Hassert Hlink Hwf_cemap.
+    iIntros "#[ [HlinkInv [HassertInv HflagInv] ] [ Hcemap_inv [ Hinterp_w1 Hinterp_w0]] ]
              (Hcode & Hlink_cap & Hdata1 & HPC & Hr0 & Hr1 & Hr2 & Hr3 & Hr4 & Hr5 & Hna & Hcont)".
     codefrag_facts "Hcode".
 
@@ -396,7 +441,7 @@ Section trusted_compute_example.
     iNext.
     iIntros (retv) "H".
     iDestruct "H" as "(Hi & Hr2 & [(-> & HPC & H)|(-> & HPC & Hr4)])".
-    iDestruct "H" as (I tid) "(Hr4 & Htc_env & %Hseal)".
+    iDestruct "H" as (I tid) "(Hr4 & #Htc_env & %Hseal)".
     all: wp_pure; iInstr_close "Hcode".
     2:{ wp_end; by iRight. }
 
@@ -413,27 +458,44 @@ Section trusted_compute_example.
       with 0 by lia.
     iInstr "Hcode". (* Jnz *)
     iDestruct (interp_valid_sealed with "Hinterp_w0") as (Φ) "Hseal_valid".
+    rewrite /custom_enclave_inv.
+
 
     (* UnSeal *)
-    iInstr_lookup "Hcode" as "Hi" "Hcode".
     wp_instr.
+    iMod (inv_acc with "Hcemap_inv") as "(#Hcemap & Hclose)"; first solve_ndisj.
+
+    iInstr_lookup "Hcode" as "Hi" "Hcode".
     iDestruct (map_of_regs_3 with "HPC Hr1 Hr0") as "[Hmap _]".
     iApply (wp_UnSeal with "[$Hmap Hi]"); eauto; simplify_map_eq; eauto;
     try solve_pure.
     by unfold regs_of; rewrite !dom_insert; set_solver+.
     iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.
-    destruct Hspec as [ ? ? ? ? ? ? ? Hps Hbounds Hregs'|]; last (by wp_pure; wp_end; iRight).
+    destruct Hspec as [ ? ? ? ? ? ? ? Hps Hbounds Hregs'|]; cycle 1.
+    { iMod ("Hclose" with "Hcemap") as "_". iModIntro.
+      by wp_pure; wp_end; iRight.
+    }
+    iMod ("Hclose" with "Hcemap") as "_"; iModIntro.
     incrementLPC_inv as (p''&b_main'&e_main'&a_main'&pc_v'& ? & HPC & Z & Hregs'); simplify_map_eq.
     repeat (rewrite insert_commute //= insert_insert).
     replace x with (b_main' ^+ 20)%a by solve_addr.
     clear Z.
     iDestruct (regs_of_map_3 with "[$Hmap]") as "[HPC [Hr1 Hr0] ]"; eauto; iFrame.
     wp_pure; iInstr_close "Hcode".
 
-    (* TODO: I should get that from the enclave custom predicate *)
-    iAssert (seal_pred_42 a) as "#Hseal_pred42". admit.
-    iDestruct (seal_pred_valid_sealed_eq with "[$Hseal_pred42] Hseal_valid") as "Heqv".
+    iAssert (
+        seal_pred a (Penc (tc_enclave_pred tc_data_cap tc_addr))
+        ∗ seal_pred (a ^+ 1)%f (Psign (tc_enclave_pred tc_data_cap tc_addr))
+      )%I as "[Htc_Penc _]".
+    {
+      iApply "Hcemap"; iFrame "%#".
+      iPureIntro.
+      rewrite /tcenclaves_map.
+      by simplify_map_eq.
+    }
+    iEval (cbn) in "Htc_Penc".
 
+    iDestruct (seal_pred_valid_sealed_eq with "[$Htc_Penc] Hseal_valid") as "Heqv".
     iAssert (▷ sealed_42 (LWSealable sb))%I as (fb fe fv) ">%Hseal42".
     { iDestruct "Hseal_valid" as (sb') "(%Heq & _ & _ & HΦ)".
       inversion Heq; subst.
@@ -456,6 +518,7 @@ Section trusted_compute_example.
     rewrite /trusted_compute_main_init_len.
 
     focus_block 2%nat "Hcode" as addr_block2 Haddr_block2 "Hblock" "Hcode'".
+    cbn in Haddr_block2.
     iMod (na_inv_acc with "HlinkInv Hna") as "(>Hassert_entry & Hna & Hclose)"; [ solve_ndisj.. |].
     iApply assert_reg_success; last iFrame "#∗"; try solve_pure ; try solve_addr'.
     solve_ndisj.
@@ -465,13 +528,18 @@ Section trusted_compute_example.
     unfocus_block "Hblock" "Hcode'" as "Hcode".
 
     focus_block 3%nat "Hcode" as addr_block3 Haddr_block3 "Hblock" "Hcode'".
+    cbn in Haddr_block3.
+    iInstr "Hblock". (* Mov *)
+    admit. (* TODO why automation doesn't work here? *)
+    iInstr "Hblock". (* Mov *)
+    admit. (* TODO why automation doesn't work here? *)
     iInstr "Hblock". (* Halt *)
-    admit. (* TODO why it doesn't work here? *)
+    admit. (* TODO why automation doesn't work here? *)
     unfocus_block "Hblock" "Hcode'" as "Hcode".
+    replace (addr_block3 ^+ 2)%a with (a_data ^+ -2)%a by solve_addr'.
+
     iApply (wp_wand with "[-]") ; [  | iIntros (?) "H"; iLeft ; iApply "H"].
     iApply "Hcont"; iFrame.
-    admit. (* TODO: fix the post condition  *)
-
     Admitted.
 
 End trusted_compute_example.