Skip to content

Commit

Permalink
WIP getOType and getWType instructions: mainly needs to fix iInstr
Browse files Browse the repository at this point in the history
  • Loading branch information
@JuneRousseau
JuneRousseau committed Jul 26, 2023
1 parent ff5fc84 commit ab022f6
Show file tree
Hide file tree
Showing 29 changed files with 462 additions and 1,575 deletions.
12 changes: 0 additions & 12 deletions _CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,6 @@ theories/rules/rules_AddSubLt.v
theories/rules/rules_Lea.v
theories/rules/rules_Mov.v
theories/rules/rules_Restrict.v
theories/rules/rules_GetTag.v
theories/rules/rules_GetSealed.v
theories/rules/rules_IsCap.v
theories/rules/rules_Jmp.v
theories/rules/rules_Jnz.v
theories/rules/rules_Subseg.v
Expand All @@ -54,9 +51,6 @@ theories/rules_binary/rules_binary_Restrict.v
theories/rules_binary/rules_binary_Jmp.v
theories/rules_binary/rules_binary_Jnz.v
theories/rules_binary/rules_binary_Subseg.v
theories/rules_binary/rules_binary_GetTag.v
theories/rules_binary/rules_binary_GetSealed.v
theories/rules_binary/rules_binary_IsCap.v
theories/rules_binary.v
theories/solve_pure.v
theories/NamedProp.v
Expand All @@ -75,9 +69,6 @@ theories/ftlr/AddSubLt.v
theories/ftlr/Lea.v
theories/ftlr/Mov.v
theories/ftlr/Restrict.v
theories/ftlr/GetTag.v
theories/ftlr/GetSealed.v
theories/ftlr/IsCap.v
theories/ftlr/Jmp.v
theories/ftlr/Jnz.v
theories/ftlr/Subseg.v
Expand All @@ -91,9 +82,6 @@ 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/GetTag_binary.v
theories/ftlr_binary/GetSealed_binary.v
theories/ftlr_binary/IsCap_binary.v
theories/ftlr_binary/Jmp_binary.v
theories/ftlr_binary/Jnz_binary.v
theories/ftlr_binary/Lea_binary.v
Expand Down
22 changes: 6 additions & 16 deletions theories/cap_lang.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -339,26 +339,16 @@ Section opsem.
| _ => None
end

| GetTag dst r =>
| GetOType dst r =>
wr ← (reg φ) !! r;
match wr with
| WInt _ => updatePC (update_reg φ dst (WInt 0%Z))
| _ => updatePC (update_reg φ dst (WInt 1%Z))
| WSealed o _ => updatePC (update_reg φ dst (WInt o))
(* TODO if not a sealed, return -1 in any other case ? What if not a sealable ? *)
| _ => updatePC (update_reg φ dst (WInt (-1)))
end

| GetSealed dst r =>
wr ← (reg φ) !! r;
match wr with
| WSealed _ _ => updatePC (update_reg φ dst (WInt 1%Z))
| _ => updatePC (update_reg φ dst (WInt 0%Z))
end

| IsCap dst r =>
wr ← (reg φ) !! r;
match wr with
| WCap _ _ _ _ => updatePC (update_reg φ dst (WInt 1%Z))
| _ => updatePC (update_reg φ dst (WInt 0%Z))
end
| GetWType dst r =>
wr ← (reg φ) !! r; updatePC (update_reg φ dst (WInt (encodeWordType wr)))

| Seal dst r1 r2 =>
wr1 ← (reg φ) !! r1;
Expand Down
12 changes: 9 additions & 3 deletions theories/examples/addr_reg_sample.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,16 +47,22 @@ Section instr_encodings.
Definition lt_z_r r1 z r2 := encodeInstrW (Lt r1 (inl z) (inr r2)).
Definition lt_r_z r1 r2 z := encodeInstrW (Lt r1 (inr r2) (inl z)).
Definition jmp r := encodeInstrW (Jmp r).
Definition get_tag r1 r2 := encodeInstrW (GetTag r1 r2).
Definition get_sealed r1 r2 := encodeInstrW (GetSealed r1 r2).
Definition iscap r1 r2 := encodeInstrW (IsCap r1 r2).
Definition get_otype r1 r2 := encodeInstrW (GetOType r1 r2).
Definition get_wtype r1 r2 := encodeInstrW (GetWType r1 r2).
Definition halt := encodeInstrW Halt.
Definition fail_end := encodeInstrW Fail.

(* encodings of return pointer permission pair *)
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 :=
Expand Down
40 changes: 20 additions & 20 deletions theories/examples/arch_sealing.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,26 +145,26 @@ Section sealing.
| _ => false end.


Lemma wp_Get_fail_same E get_i dst pc_p pc_b pc_e pc_a w zsrc :
decodeInstrW w = get_i →
is_Get get_i dst dst →
isCorrectPC (WCap pc_p pc_b pc_e pc_a) →

{{{ ▷ PC ↦ᵣ WCap pc_p pc_b pc_e pc_a
∗ ▷ pc_a ↦ₐ w
∗ ▷ dst ↦ᵣ WInt zsrc }}}
Instr Executable @ E
{{{ RET FailedV; True }}}.
Proof.
iIntros (Hdecode Hinstr Hvpc φ) "(>HPC & >Hpc_a & >Hsrc) Hφ".
iDestruct (map_of_regs_2 with "HPC Hsrc") as "[Hmap %]".
iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+.
iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.
destruct Hspec as [* Hsucc |].
{ (* Success (contradiction) *) simplify_map_eq. }
{ (* Failure, done *) by iApply "Hφ". }
Qed.
(* Lemma wp_Get_fail_same E get_i dst pc_p pc_b pc_e pc_a w zsrc : *)
(* decodeInstrW w = get_i → *)
(* is_Get get_i dst dst → *)
(* isCorrectPC (WCap pc_p pc_b pc_e pc_a) → *)

(* {{{ ▷ PC ↦ᵣ WCap pc_p pc_b pc_e pc_a *)
(* ∗ ▷ pc_a ↦ₐ w *)
(* ∗ ▷ dst ↦ᵣ WInt zsrc }}} *)
(* Instr Executable @ E *)
(* {{{ RET FailedV; True }}}. *)
(* Proof. *)
(* iIntros (Hdecode Hinstr Hvpc φ) "(>HPC & >Hpc_a & >Hsrc) Hφ". *)
(* iDestruct (map_of_regs_2 with "HPC Hsrc") as "[Hmap %]". *)
(* iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto. *)
(* by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+. *)
(* iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec. *)
(* destruct Hspec as [* Hsucc |]. *)
(* { (* Success (contradiction) *) simplify_map_eq. } *)
(* { (* Failure, done *) by iApply "Hφ". } *)
(* Qed. *)

(* TODO: move this to unseal rules file *)
Lemma wp_unseal_nomatch_r2 E pc_p pc_b pc_e pc_a w r1 r2 p b e a wsealed pc_a' :
Expand Down
95 changes: 48 additions & 47 deletions theories/examples/dynamic_sealing.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Section sealing.
Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
{nainv: logrel_na_invs Σ}
`{MP: MachineParameters}
{seals:sealStoreG Σ}
{mono : sealLLG Σ}.

(* Assume r_t1 contains a capability representing a sealed value.
Expand Down Expand Up @@ -100,28 +101,28 @@ Section sealing.
Definition make_seal_preamble f_m ai :=
([∗ list] a_i;w_i ∈ ai;(make_seal_preamble_instrs f_m), a_i ↦ₐ w_i)%I.

(* TODO: move this to the rules_Get.v file. small issue with the spec of failure: it does not actually
require/leave a trace on dst! It would be good if req_regs of a failing get does not include dst (if possible) *)
Lemma wp_Get_fail_same E get_i dst pc_p pc_b pc_e pc_a w zsrc :
decodeInstrW w = get_i →
is_Get get_i dst dst →
isCorrectPC (WCap pc_p pc_b pc_e pc_a) →

{{{ ▷ PC ↦ᵣ WCap pc_p pc_b pc_e pc_a
∗ ▷ pc_a ↦ₐ w
∗ ▷ dst ↦ᵣ WInt zsrc }}}
Instr Executable @ E
{{{ RET FailedV; True }}}.
Proof.
iIntros (Hdecode Hinstr Hvpc φ) "(>HPC & >Hpc_a & >Hsrc) Hφ".
iDestruct (map_of_regs_2 with "HPC Hsrc") as "[Hmap %]".
iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+.
iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.
destruct Hspec as [* Hsucc |].
{ (* Success (contradiction) *) simplify_map_eq. }
{ (* Failure, done *) by iApply "Hφ". }
Qed.
(* (* TODO: move this to the rules_Get.v file. small issue with the spec of failure: it does not actually *)
(* require/leave a trace on dst! It would be good if req_regs of a failing get does not include dst (if possible) *) *)
(* Lemma wp_Get_fail_same E get_i dst pc_p pc_b pc_e pc_a w zsrc : *)
(* decodeInstrW w = get_i → *)
(* is_Get get_i dst dst → *)
(* isCorrectPC (WCap pc_p pc_b pc_e pc_a) → *)

(* {{{ ▷ PC ↦ᵣ WCap pc_p pc_b pc_e pc_a *)
(* ∗ ▷ pc_a ↦ₐ w *)
(* ∗ ▷ dst ↦ᵣ WInt zsrc }}} *)
(* Instr Executable @ E *)
(* {{{ RET FailedV; True }}}. *)
(* Proof. *)
(* iIntros (Hdecode Hinstr Hvpc φ) "(>HPC & >Hpc_a & >Hsrc) Hφ". *)
(* iDestruct (map_of_regs_2 with "HPC Hsrc") as "[Hmap %]". *)
(* iApply (wp_Get with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto. *)
(* by erewrite regs_of_is_Get; eauto; rewrite !dom_insert; set_solver+. *)
(* iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec. *)
(* destruct Hspec as [* Hsucc |]. *)
(* { (* Success (contradiction) *) simplify_map_eq. } *)
(* { (* Failure, done *) by iApply "Hφ". } *)
(* Qed. *)

Lemma unseal_spec pc_p pc_b pc_e (* PC *)
wret (* return cap *)
Expand Down Expand Up @@ -196,7 +197,7 @@ Section sealing.
codefrag_facts "Hprog". simpl in H, H0.
focus_block 3 "Hprog" as mid1 Hmid1 "Hprog" "Hcont".
iGo "Hprog". simpl in *. instantiate (1 := (mid1 ^+ 18)%a). solve_addr.
unfocus_block "Hprog" "Hcont" as "Hprog".
unfocus_block "Hprog" "Hcont" as "Hprog".

focus_block 4 "Hprog" as a_middle Ha_middle "Hprog" "Hcont".
iApply findb_spec; iFrameAutoSolve; eauto.
Expand Down Expand Up @@ -295,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.
Qed.
(* 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.

Lemma sealLL_alloc ι ll Ep Φ {Hpers : ∀ w, Persistent (Φ w)} :
ll ↦ₐ WInt 0%Z -∗
Expand Down
Loading

0 comments on commit ab022f6

Please sign in to comment.