Separate GetWType from the other Get -- WIP fixing keylist

_CoqProject

@@ -28,6 +28,7 @@ theories/cap_lang.v
 theories/region.v
 theories/rules/rules_base.v
 theories/rules/rules_Get.v
+theories/rules/rules_GetWType.v
 theories/rules/rules_Load.v
 theories/rules/rules_Store.v
 theories/rules/rules_AddSubLt.v
@@ -42,6 +43,7 @@ theories/rules/rules_UnSeal.v
 theories/rules.v
 theories/rules_binary/rules_binary_base.v
 theories/rules_binary/rules_binary_Get.v
+theories/rules_binary/rules_binary_GetWType.v
 theories/rules_binary/rules_binary_Load.v
 theories/rules_binary/rules_binary_Store.v
 theories/rules_binary/rules_binary_AddSubLt.v
@@ -63,6 +65,7 @@ theories/monotone.v
 theories/ftlr/ftlr_base.v
 theories/ftlr/interp_weakening.v
 theories/ftlr/Get.v
+theories/ftlr/GetWType.v
 theories/ftlr/Load.v
 theories/ftlr/Store.v
 theories/ftlr/AddSubLt.v
@@ -82,6 +85,7 @@ theories/ftlr_binary/Load_binary.v
 theories/ftlr_binary/Mov_binary.v
 theories/ftlr_binary/AddSubLt_binary.v
 theories/ftlr_binary/Get_binary.v
+theories/ftlr_binary/GetWType_binary.v
 theories/ftlr_binary/Jmp_binary.v
 theories/ftlr_binary/Jnz_binary.v
 theories/ftlr_binary/Lea_binary.v

theories/examples/addr_reg_sample.v

@@ -56,13 +56,6 @@ Section instr_encodings.
   Definition e := encodePerm E.
 End instr_encodings.
 
-Section word_type_encoding.
-  Definition wt_cap := WCap O 0%a 0%a 0%a.
-  Definition wt_sealrange := WSealRange (false, false) 0%ot 0%ot 0%ot.
-  Definition wt_sealed := WSealed 0%ot (SCap O 0%a 0%a 0%a).
-  Definition wt_int := WInt 0.
-End word_type_encoding.
-
 (* Some additional helper lemmas about region_addrs *)
 
 Definition region_addrs_zeroes (b e : Addr) : list Word :=

theories/examples/dynamic_sealing.v

@@ -296,30 +296,30 @@ Section sealing.
     iFrame. iNext. iIntros "(HPC & Hr_env & Hr_t0 & Hpc_b & Ha_r' & Hregs & HisList & Hprog & Hown)".
     unfocus_block "Hprog" "Hcont" as "Hprog".
 
-    (* rewrite (updatePcPerm_cap_non_E pc_p pc_b pc_e (a_first ^+ 54)%a ltac:(destruct Hvpc; congruence)). *)
-    (* focus_block 2 "Hprog" as a_middle' Ha_middle' "Hprog" "Hcont". *)
-    (* iDestruct (big_sepM_delete _ _ r_t7 with "Hregs") as "[Hr_t7 Hregs]";[simplify_map_eq; auto|]. *)
-    (* iDestruct (big_sepM_delete _ _ r_t2 with "Hregs") as "[Hr_t2 Hregs]";[simplify_map_eq; auto|]. *)
-    (* iDestruct (big_sepM_delete _ _ r_t3 with "Hregs") as "[Hr_t3 Hregs]";[simplify_map_eq; auto|]. *)
-    (* map_simpl "Hregs". *)
-    (* iDestruct "HisList" as (a a' a'' pbvals') "(%HA & #Hpref' & Hr_t1 & Ha)". *)
-    (* destruct HA as (HA & HB). *)
-    (* iGo "Hprog". instantiate (1:=a'). solve_addr. solve_addr. *)
-    (* iGo "Hprog". (* rewrite decode_encode_perm_inv. reflexivity. *) *)
-    (* (* iGo "Hprog". rewrite decode_encode_perm_inv. auto. solve_addr. *) *)
-    (* (* iGo "Hprog". *) *)
-    (* unfocus_block "Hprog" "Hcont" as "Hprog". *)
-    (* iApply "Hφ"; iFrame "∗ #". *)
-    (* iSplitR "Hr_t1 Ha ". *)
-    (* - iDestruct (big_sepM_insert _ _ r_t3 with "[$Hregs $Hr_t3]") as "Hregs"; [apply lookup_delete|]. *)
-    (*   map_simpl "Hregs". *)
-    (*   iDestruct (big_sepM_insert _ _ r_t2 with "[$Hregs $Hr_t2]") as "Hregs"; [simplify_map_eq;auto|]. *)
-    (*   map_simpl "Hregs". *)
-    (*   iDestruct (big_sepM_insert _ _ r_t7 with "[$Hregs $Hr_t7]") as "Hregs"; [simplify_map_eq;auto|]. *)
-    (*   map_simpl "Hregs". *)
-    (*   repeat rewrite -(insert_commute _ _ r_t7)//. *)
-    (* - iExists _, _, _. iFrame. iSplit;eauto. *)
-  Admitted.
+    rewrite (updatePcPerm_cap_non_E pc_p pc_b pc_e (a_first ^+ 57)%a ltac:(destruct Hvpc; congruence)).
+    focus_block 2 "Hprog" as a_middle' Ha_middle' "Hprog" "Hcont".
+    iDestruct (big_sepM_delete _ _ r_t7 with "Hregs") as "[Hr_t7 Hregs]";[simplify_map_eq; auto|].
+    iDestruct (big_sepM_delete _ _ r_t2 with "Hregs") as "[Hr_t2 Hregs]";[simplify_map_eq; auto|].
+    iDestruct (big_sepM_delete _ _ r_t3 with "Hregs") as "[Hr_t3 Hregs]";[simplify_map_eq; auto|].
+    map_simpl "Hregs".
+    iDestruct "HisList" as (a a' a'' pbvals') "(%HA & #Hpref' & Hr_t1 & Ha)".
+    destruct HA as (HA & HB).
+    iGo "Hprog". instantiate (1:=a'). solve_addr. solve_addr.
+    iGo "Hprog". (* rewrite decode_encode_perm_inv. reflexivity. *)
+    (* iGo "Hprog". rewrite decode_encode_perm_inv. auto. solve_addr. *)
+    (* iGo "Hprog". *)
+    unfocus_block "Hprog" "Hcont" as "Hprog".
+    iApply "Hφ"; iFrame "∗ #".
+    iSplitR "Hr_t1 Ha ".
+    - iDestruct (big_sepM_insert _ _ r_t3 with "[$Hregs $Hr_t3]") as "Hregs"; [apply lookup_delete|].
+      map_simpl "Hregs".
+      iDestruct (big_sepM_insert _ _ r_t2 with "[$Hregs $Hr_t2]") as "Hregs"; [simplify_map_eq;auto|].
+      map_simpl "Hregs".
+      iDestruct (big_sepM_insert _ _ r_t7 with "[$Hregs $Hr_t7]") as "Hregs"; [simplify_map_eq;auto|].
+      map_simpl "Hregs".
+      repeat rewrite -(insert_commute _ _ r_t7)//.
+    - iExists _, _, _. iFrame. iSplit;eauto.
+  Qed.
 
   Lemma sealLL_alloc ι ll Ep Φ {Hpers : ∀ w, Persistent (Φ w)} :
     ll ↦ₐ WInt 0%Z -∗