WIP proof callback trusted compute example

theories/examples/enclaves/trusted_compute.v

@@ -231,8 +231,6 @@ Section trusted_compute_example.
 
     (* TODO not needed for this part of the spec, but will be required for the full proof *)
     (link_table_inv
-       (* link_addr v_link *)
-       (* b_link e_link a_link *)
        v_link
        assert_entry b_assert e_assert v_assert
     ∗ assert_inv b_assert a_flag e_assert v_assert
@@ -286,14 +284,6 @@ Section trusted_compute_example.
     iInstr "Hcode". (* Mov *)
     iInstr "Hcode". (* Lea *)
 
-    iInstr "Hcode". (* Lea *)
-    replace (a_data ^+1)%a with (b_main ^+ 50)%a by solve_addr'.
-    iInstr "Hcode". (* Load *)
-    iInstr "Hcode". (* Load *)
-    { admit. (* TODO it's fine *) }
-    iInstr "Hcode". (* Lea *)
-
-
     destruct (is_sealedL w0) eqn:Hsealed_w0 ; cycle 1.
     { (* w0 is not a sealed  *)
       destruct_lword (w0) ; cbn in Hsealed_w0 ; try done.
@@ -318,23 +308,77 @@ Section trusted_compute_example.
     iInstr "Hcode". (* Lea *)
     iInstr "Hcode". (* Jnz *)
     iInstr "Hcode". (* GetOType *)
-    (* iInstr "Hcode". (* EStoreId r_t2 r_t2 r_t4 *) *)
-  Admitted.
-
-        (* (* check otype(w_res) against identity of the enclave *) *)
-        (* GetOType r_t2 r_t0; (* r2 := LInt σ *) *)
-        (* EStoreId r_t2 r_t2 r_t4; (* r2 := if etbl[σ] = Some I then 1 else 0 *) *)
-        (* Sub r_t2 r_t2 1; (* r2 := if etbl[σ] = Some I then 0 else -1 *) *)
-        (* Jnz r_t3 r_t2; (* Jumps to `fails` if (etbl[σ] = None)  *) *)
-        (* Load r_t4 r_t4; *)
-        (* Sub r_t4 r_t4 hash_enclave; *)
-        (* Jnz r_t3 r_t4; *)
-
-        (* (* get returned value and assert it to be 42 *) *)
-        (* UnSeal r_t0 r_t0 r_t1; *)
-        (* Mov r_t1 r_t5; *)
-        (* GetA r_t4 r_t0; *)
-        (* Mov r_t5 42%Z *)
 
+    iInstr_lookup "Hcode" as "Hi" "Hcode".
+    wp_instr.
+    iApply (wp_estoreid_success_unknown with "[HPC Hr2 Hr4 Hi]"); try iFrame; try solve_pure.
+    iNext.
+    iIntros (retv) "H".
+    iDestruct "H" as "(Hi & Hr2 & [(-> & HPC & H)|(-> & HPC & Hr4)])".
+    iDestruct "H" as (I tid) "(Hr4 & Htc_env & %Hseal)".
+    all: wp_pure; iInstr_close "Hcode".
+    2:{ wp_end; by iRight. }
+
+    iInstr "Hcode". (* Sub *)
+    destruct (decide (I = hash_trusted_compute_enclave)) as [-> | HnI]
+    ; cycle 1.
+    { (* Not the right enclave *)
+      iInstr "Hcode". (* Jnz *)
+      by (injection; intro Hcontra; lia).
+      iInstr "Hcode". (* Fail *)
+      wp_end; by iRight.
+    }
+    replace (hash_trusted_compute_enclave - hash_trusted_compute_enclave)
+      with 0 by lia.
+    iInstr "Hcode". (* Jnz *)
+
+    (* UnSeal *)
+    iInstr_lookup "Hcode" as "Hi" "Hcode".
+    wp_instr.
+    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).
+    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 [Hr0 Hr1] ]"; eauto; iFrame.
+    wp_pure; iInstr_close "Hcode".
+
+    (* From here, I know that the content sw0 is supposed to be (O,-,-,42) *)
+    (* TODO instantiate the seal_pred *)
+    (* TODO we need the sealed word and sealing words to be valid! *)
+    assert ( fz42 : (42 <? MemNum)%Z = true). admit.
+    assert ( fnz42 : (0 <=? 42)%Z = true) by lia.
+    iAssert
+      (seal_pred o (fun lw => ⌜ ∃ b e v, (lw = LCap O b e (finz.FinZ 42 fz42 fnz42) v)⌝)%I
+      ) as "Hsign_tc".
+    admit.
+    Definition valid_sealed w o (Φ : LWord -> iProp Σ) :=
+      (∃ sb, ⌜w = LWSealed o sb⌝ ∗  ⌜∀ w : leibnizO LWord, Persistent (Φ w)⌝
+                                                           ∗ seal_pred o Φ ∗ Φ (LWSealable sb))%I.
+    iAssert (∃ (Φ : LWord -> iProp Σ), valid_sealed (LWSealed o sw0) o Φ)%I as (Φ) "Hseal_valid".
+    admit.
+    Set Nested Proofs Allowed.
+    Lemma seal_pred_valid_sealed_eq τ w Φ Φ' {Hpers : ∀ w, Persistent (Φ w)} :
+      seal_pred τ Φ -∗ valid_sealed w τ Φ' -∗ (∀ w, ▷ (Φ w ≡ Φ' w)).
+    Proof.
+      iIntros "Hsp Hvs".
+      iDestruct "Hvs" as (sb) "(_ & _ & Hsp' & _)".
+      iApply (seal_pred_agree with "Hsp Hsp'").
+    Qed.
+
+    iDestruct (seal_pred_valid_sealed_eq with "[$Hsign_tc] Hseal_valid") as "Hsigned".
+    iSpecialize ("Hsigned" $! (LWSealed o sw0)).
+
+    iInstr "Hcode". (* Mov *)
+    (* iInstr "Hcode". (* GetA *) *)
+    (* iInstr "Hcode". (* Mov *) *)
+    (* 2: { admit. (* Fail *)} *)
+    (* { cbn. } *)
+    Admitted.
 
 End trusted_compute_example.