diff --git a/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html b/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html
index d310d213..1ac00779 100644
--- a/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html
+++ b/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html
@@ -355,7 +355,6 @@
cap_machine.ftlr.IsUnique
decide (reg_allows_sweep lregs r p b e a v /\ (r = PC \/ pc_a ∉ (finz.seq_between b e)))
in
-
length la = length Ps ->
allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps false
-∗ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw)
@@ -385,234 +384,173 @@ cap_machine.ftlr.IsUnique
Unshelve. Fail idtac. Admitted.
-
- Lemma isunique_case (lregs : leibnizO LReg)
- (ppc : Perm) (bpc epc apc : Addr) (vpc : Version)
- (lwpc : LWord) (dst src : RegName) (P : D):
- ftlr_instr lregs ppc bpc epc apc vpc lwpc (IsUnique dst src) P.
+ Lemma cond_open_contra
+ ppc bpc epc apc vpc lregs src psrc bsrc esrc asrc vsrc :
+ psrc ≠ machine_base.E ->
+ <[PC:=LCap ppc bpc epc apc vpc]> lregs !! src = Some (LCap psrc bsrc esrc asrc vsrc) ->
+ unique_in_registersL (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src
+ (LCap psrc bsrc esrc asrc vsrc) ->
+ (bpc <= apc < epc)%a ->
+ ¬ (reg_allows_sweep
+ (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc
+ esrc asrc vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+ -> psrc = O.
Proof.
- intros Hp Hsome i Hbae Hi.
- iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha HP Hcls HPC Hmap".
- specialize (HpersP lwpc).
- rewrite delete_insert_delete.
- iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /=";
- [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl.
-
-
-
- assert(∀ x : RegName, is_Some (<[PC:=LCap ppc bpc epc apc vpc]> lregs !! x)) as Hsome'.
+ intros Hp_neq_E Hlwsrc' Hunique_regs Hbae Hdecide.
+ rewrite /reg_allows_sweep in Hdecide.
+ apply not_and_r in Hdecide.
+ destruct Hdecide as [Hdecide|Hdecide]; cycle 1.
{
- intros. destruct (decide (x = PC)) as [Hx|Hx].
- rewrite Hx lookup_insert; unfold is_Some. by eexists.
- by rewrite lookup_insert_ne.
+ exfalso.
+ apply Decidable.not_or in Hdecide.
+ destruct Hdecide as [Hsrc_neq_PC Hapc_overlap].
+ apply Decidable.not_not in Hapc_overlap.
+ 2: {
+ clear.
+ assert (forall (a : Addr) (la : list Addr), Decision (apc ∈ finz.seq_between bsrc esrc))
+ by (intros; solve_decision).
+ specialize (H apc (finz.seq_between bsrc esrc)).
+ destruct H as [H'|H'] ; [left|right]; done.
+ }
+ clear -Hunique_regs Hapc_overlap Hsrc_neq_PC Hbae.
+ rewrite /unique_in_registersL in Hunique_regs.
+ eapply map_Forall_insert_1_1 in Hunique_regs.
+ rewrite decide_False in Hunique_regs; auto.
+ apply Hunique_regs.
+ rewrite /overlap_wordL /overlap_word //=.
+ apply elem_of_finz_seq_between in Hapc_overlap.
+ destruct (bsrc <? bpc)%a eqn:Hneq; solve_addr.
}
-
-
- assert (∃ psrc bsrc esrc asrc vsrc, read_reg_inr (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc vsrc)
- as (psrc & bsrc & esrc & asrc & vsrc & HVsrc).
- {
- specialize Hsome' with src as Hsrc.
- destruct Hsrc as [wsrc Hsomesrc].
- unfold read_reg_inr. rewrite Hsomesrc.
- destruct wsrc as [|[ psrc bsrc esrc asrc vsrc|] | ]; try done.
- by repeat eexists.
+ { rewrite /reg_allows_sweep in Hdecide.
+ apply Decidable.not_and in Hdecide; last apply lookup_dec.
+ destruct Hdecide as [Hdecide|Hdecide].
+ + by rewrite Hlwsrc' in Hdecide.
+ + destruct psrc ; try done.
}
-
-
- iDestruct (create_sweep_res with "[$Hreg] [$Hinv] [%]") as (Ps) "[%Hlen_Ps HSweepRes]"
- ; [ eassumption
- | by apply elem_of_finz_seq_between
- |].
-
-
-
- iMod (sweep_res_implies_mem_map with "HSweepRes Ha") as (mem) "[HSweepMem >HMemRes]".
- set (E := ⊤ ∖ ↑logN.@(apc, vpc)).
- set (E' := allow_sweep_mask (list_remove_elem apc (finz.seq_between bsrc esrc)) vsrc apc vpc).
- set (cond_open :=
- decide
- (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc
- vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
- ).
-
-
-
- iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC.
-
-
-
- iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto.
-
-
- iApply (wp_isunique with "[$Hmap $HMemRes]")
- ; eauto
- ; [ by simplify_map_eq
- | rewrite /subseteq /map_subseteq /set_subseteq_instance
- ; intros rr _; apply elem_of_dom
- ; rewrite lookup_insert_is_Some';
- eauto
- |].
-
-
- iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)".
-
-
- destruct Hspec as
- [ psrc' bsrc' esrc' asrc' vsrc' Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC
- | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC
- | lwsrc' psrc' bsrc' esrc' asrc' vsrc' Hlwsrc Hlwsrc' Hmem' Hincr_PC
- | ? ? Hfail]
- ; simplify_map_eq
- ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq)
- ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq)
- ; try (cbn in Hlwsrc' ; simplify_eq).
+ Unshelve. Fail idtac. Admitted.
- {
+ Lemma mem_map_recover_res_upd
+ (lregs : leibnizO LReg) (lmem lmem': LMem)
+ (pc_p : Perm) (pc_b pc_e pc_a : Addr) (pc_v : Version) (pc_lw : LWord)
+ (r : RegName)
+ (p : Perm) (b e a : Addr) (v : Version)
+ (Ps : list D) (P : D) :
- rewrite /allow_sweep_mem.
- subst cond_open; set (cond_open := decide (_ /\ _)).
- iDestruct "HSweepMem" as "(_ & HSweepMem)".
- destruct cond_open as [Hdecide|Hdecide]; cycle 1.
- + iDestruct "HSweepMem" as "->".
- iModIntro.
- rewrite /read_reg_inr Hlwsrc' in HVsrc; simplify_eq.
- apply not_and_r in Hdecide.
- destruct Hdecide as [Hdecide|Hdecide]; cycle 1.
- {
- exfalso.
- apply Decidable.not_or in Hdecide.
- destruct Hdecide as [Hsrc_neq_PC Hapc_overlap].
- apply Decidable.not_not in Hapc_overlap.
- 2: {
- clear.
- assert (forall (a : Addr) (la : list Addr), Decision (apc ∈ la))
- by (intros; solve_decision).
- specialize (H apc (finz.seq_between bsrc esrc)).
- destruct H as [H'|H'] ; [left|right]; done.
- }
- clear -Hunique_regs Hapc_overlap Hsrc_neq_PC Hbae.
- rewrite /unique_in_registersL in Hunique_regs.
- eapply map_Forall_insert_1_1 in Hunique_regs.
- rewrite decide_False in Hunique_regs; auto.
- apply Hunique_regs.
- rewrite /overlap_wordL /overlap_word //=.
- apply elem_of_finz_seq_between in Hapc_overlap.
- destruct (bsrc <? bpc)%a eqn:Hneq; solve_addr.
- }
- { rewrite /reg_allows_sweep in Hdecide.
- apply Decidable.not_and in Hdecide; last apply lookup_dec.
- destruct Hdecide as [Hdecide|Hdecide].
- + by rewrite Hlwsrc' in Hdecide.
- + destruct (decide (psrc = O)) as [->|Hpsrc_O]; last (destruct psrc ; try done).
- assert (src ≠ PC) as Hsrc_ne_pc.
- { intro ; subst ; inversion i ; inversion H1 ; cbn in * ; simplify_map_eq.
- destruct H8 ; done.
- }
- assert ( lmem' !! (apc, vpc) = Some lwpc ) as Hmem'_pca.
- { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto. }
- rewrite -(insert_id lmem' (apc,vpc) lwpc);auto.
- iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]".
- iMod ("Hcls" with "[Hmem HP]");[iExists lwpc;iFrame|iModIntro].
- iApply wp_pure_step_later; auto.
- iNext; iIntros "_".
- incrementLPC_inv; simplify_map_eq.
- assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq).
- simplify_map_eq.
- do 2 (rewrite (insert_commute _ _ PC) //) ; rewrite insert_insert.
- iApply ("IH" $! (<[dst := (LInt 1)]> (<[src:=LCap O bsrc esrc asrc (vsrc + 1)]> lregs))
- with "[%] [] [Hmap] [$Hown]"); eauto.
- { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
- {
- iIntros (ri ? Hri Hvs).
- destruct (decide (ri = dst)) ; simplify_map_eq
- ; first by rewrite !fixpoint_interp1_eq.
- destruct (decide (ri = src)); simplify_map_eq;
- first by rewrite !fixpoint_interp1_eq.
- iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto.
- }
- rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto.
- }
- + destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep].
- destruct (decide (src = PC)) as [->|Hsrc_ne_pc]; [clear Hvalid_sweep |].
-
-
- -
- incrementLPC_inv
- as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
- ; simplify_map_eq.
-
+ let la := (list_remove_elem pc_a (finz.seq_between b e)) in
+ let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in
+ let E' := allow_sweep_mask la v pc_a pc_v in
+ let cond_open :=
+ decide (reg_allows_sweep (<[PC:=LCap pc_p pc_b pc_e pc_a pc_v]> lregs) r p b e a v /\ (r = PC \/ pc_a ∉ (finz.seq_between b e)))
+ in
+ let lregs' := (<[PC:=LCap pc_p pc_b pc_e pc_a pc_v]> lregs) in
+
+ length la = length Ps ->
+ p ≠ machine_base.E ->
+ is_valid_updated_lmemory lmem (finz.seq_between b e) v lmem' ->
+ unique_in_registersL lregs' r (LCap p b e a v) ->
+ lregs' !! r = Some (LCap p b e a v) ->
+ isCorrectLPC (LCap pc_p pc_b pc_e pc_a pc_v) ->
+ Persistent (P pc_lw) ->
+
+ □ (∀ lw : LWord, P lw -∗ fixpoint interp1 lw)
+ -∗ P pc_lw
+ -∗ allow_sweep_mem lregs' r pc_a pc_v pc_lw p b e a v lmem Ps false
+ -∗ ([∗ map] la↦lw ∈ lmem', la ↦ₐ lw)
+ ={(if cond_open then E' else E), E}=∗
+ (pc_a,pc_v) ↦ₐ pc_lw ∗
+ if cond_open
+ then interp (LCap p b e a (v+1))
+ else emp
+ .
+ Proof.
+ intros * Hlen_Ps Hp_ne_E Hvalid_lmem' Hunique_regs Hlwsrc' Hcorrect_pc HpersP
+ ; iIntros "#Hread #HP HSweepMem Hmem".
+ subst lregs'.
+ assert ( (pc_b <= pc_a < pc_e)%a) as Hbae.
+ { inversion Hcorrect_pc ; inversion H1 ; cbn in * ; simplify_map_eq; done. }
+ iDestruct "HSweepMem" as "(%Hread & HSweepMem)".
+ subst cond_open; set (cond_open := decide _).
+ destruct cond_open as [Hdecide|Hdecide]; cycle 1.
+ - iDestruct "HSweepMem" as "->".
+ apply cond_open_contra in Hdecide; auto ; simplify_eq.
+ all: assert (r ≠ PC)
+ as Hr_ne_pc
+ by (intro ; subst ; inversion Hcorrect_pc
+ ; inversion H1 ; cbn in * ; simplify_map_eq
+ ; by destruct H8).
+ all: assert ( lmem' !! (pc_a, pc_v) = Some pc_lw )
+ as Hmem'_pca
+ by (eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto; by simplify_map_eq).
+ all: rewrite -(insert_id lmem' (pc_a,pc_v) pc_lw);auto.
+ all: iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]"; iFrame.
+ done.
+ - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep].
+
+ destruct (decide (r = PC)) as [->|r_ne_pc]
+ ; [clear Hvalid_sweep |]
+ ; simplify_map_eq.
+ +
iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
+ iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
subst E'.
- rewrite /read_reg_inr in HVsrc; simplify_map_eq.
- set (la' := (list_remove_elem asrc (finz.seq_between bsrc esrc)) ).
-
-
- assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
- do 2 (rewrite (insert_commute _ _ PC) //);
- rewrite !insert_insert.
- assert (a_pc' ∈ finz.seq_between b_pc' e_pc') as Hapc_in_range.
- { clear -i.
- inversion i ; cbn in * ; simplify_eq.
- inversion H0 ; cbn in * ; simplify_eq.
- by apply elem_of_finz_seq_between.
+ assert (a ∈ finz.seq_between b e) as Hapc_in_range.
+ { by apply isCorrectLPC_isCorrectPC_iff, isCorrectPC_withinBounds, withinBounds_in_seq
+ in Hcorrect_pc.
}
- assert ( a_pc' ∉ la') as Hapc_notin_la'
- by (by subst la' ; apply not_elemof_list_remove_elem).
+ assert ( a ∉ (list_remove_elem a (finz.seq_between b e)))
+ as Hapc_notin_la' by (by apply not_elemof_list_remove_elem).
- assert ( lmem' !! (a_pc', vsrc) = Some lwpc ) as Hmem'_pca.
- { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto.
+ assert ( lmem' !! (a, v) = Some pc_lw ) as Hmem'_pca.
+ { eapply is_valid_updated_lmemory_preserves_lmem ; cycle 1 ; eauto.
by simplify_map_eq.
}
-
- assert ( lmem' !! (a_pc', vsrc+1) = Some lwpc ) as Hmem'_pca_next.
+ assert ( lmem' !! (a, v+1) = Some pc_lw ) as Hmem'_pca_next.
{ eapply is_valid_updated_lmemory_preserves_lmem_next; cycle 1
- ; eauto
- ; last by simplify_map_eq.
- eapply Forall_forall; intros a Ha.
+ ; eauto
+ ; last by simplify_map_eq.
+ eapply Forall_forall; intros a' Ha'.
rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia).
eapply logical_region_version_neq; eauto ; last lia.
}
- assert (logical_region_map la' lws vsrc !! (a_pc', vsrc) = None)
- as Hasrc_notin_reg_la'.
- { subst la'. eapply logical_region_notin; eauto. }
+ assert (logical_region_map (list_remove_elem a (finz.seq_between b e)) lws v !! (a, v) = None)
+ as Hasrc_notin_reg_la'.
+ { eapply logical_region_notin; eauto. }
- assert ( ((logical_region_map la' lws) ) vsrc ⊆ lmem' )
- as Hmem'_be.
+ assert ( ((logical_region_map (list_remove_elem a (finz.seq_between b e)) lws) ) v ⊆ lmem' )
+ as Hmem'_be.
{
- eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b_pc' e_pc'))
+ eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b e))
; eauto.
eapply is_valid_updated_lmemory_insert'; eauto.
- subst la'.
- eapply Forall_forall; intros a Ha.
+ eapply Forall_forall; intros a' Ha'.
eapply logical_region_version_neq; eauto ; last lia.
}
- assert ( ((logical_region_map la' lws) ) (vsrc+1) ⊆ lmem' )
- as Hmem'_be_next.
+ assert ( ((logical_region_map (list_remove_elem a (finz.seq_between b e)) lws) ) (v+1) ⊆ lmem' )
+ as Hmem'_be_next.
{
- eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
- assert (v' = vsrc+1 /\ (a' ∈ la'))
- as [? Ha'_in_be] by (subst la' ; eapply logical_region_map_some_inv; eauto)
+ eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
+ assert (v' = v+1 /\ (a' ∈ (list_remove_elem a (finz.seq_between b e))))
+ as [? Ha'_in_be] by (eapply logical_region_map_some_inv; eauto)
; simplify_eq.
- destruct Hupd.
+ destruct Hvalid_lmem'.
eapply lookup_weaken; last eapply H0.
rewrite update_version_region_preserves_lmem_next; eauto.
{ rewrite lookup_insert_ne.
erewrite logical_region_map_lookup_versions; eauto.
clear -Ha'_in_be.
- intro ; simplify_eq ; subst la'.
- apply not_elemof_list_remove_elem in Ha'_in_be ; auto.
+ intro ; simplify_eq.
+ apply not_elemof_list_remove_elem in Ha'_in_be ; auto.
}
- { subst la'.
- eapply elem_of_submseteq; eauto.
+ { eapply elem_of_submseteq; eauto.
eapply list_remove_elem_submsteq.
}
{ rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia).
@@ -620,239 +558,334 @@ cap_machine.ftlr.IsUnique
}
}
- rewrite -(insert_id lmem' (a_pc', vsrc) lwpc); auto.
+ rewrite -(insert_id lmem' (a, v) pc_lw); auto.
iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha Hmem]".
-
-
- rewrite -(insert_id (_ lmem') (a_pc', vsrc+1) lwpc); auto.
+ rewrite -(insert_id (_ lmem') (a, v+1) pc_lw); auto.
2: { rewrite lookup_delete_ne ; first by simplify_map_eq. intro ; simplify_eq ; lia. }
iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_next Hmem]".
-
-
- eapply delete_subseteq_r with (k := ((a_pc', vsrc) : LAddr)) in Hmem'_be
+ eapply delete_subseteq_r with (k := ((a, v) : LAddr)) in Hmem'_be
; last (eapply logical_region_notin; eauto).
- eapply delete_subseteq_r with (k := ((a_pc', vsrc+1) : LAddr)) in Hmem'_be
+ eapply delete_subseteq_r with (k := ((a, v+1) : LAddr)) in Hmem'_be
; last (eapply logical_region_notin; eauto).
iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
; first (eapply Hmem'_be).
-
-
- eapply delete_subseteq_r with (k := ((a_pc', vsrc) : LAddr)) in Hmem'_be_next
+ eapply delete_subseteq_r with (k := ((a, v) : LAddr)) in Hmem'_be_next
; last (eapply logical_region_notin ; eauto).
- eapply delete_subseteq_r with (k := ((a_pc', vsrc+1) : LAddr)) in Hmem'_be_next
+ eapply delete_subseteq_r with (k := ((a, v+1) : LAddr)) in Hmem'_be_next
; last (eapply logical_region_notin ; eauto).
eapply delete_subseteq_list_r
- with (m3 := list_to_map (zip (map (λ a : Addr, (a, vsrc)) la') lws))
- in Hmem'_be_next
+ with (m3 := list_to_map (zip (map (λ a : Addr, (a, v)) (list_remove_elem a (finz.seq_between b e))) lws))
+ in Hmem'_be_next
; eauto
; last (by eapply update_logical_memory_region_disjoint).
iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
; first (eapply Hmem'_be_next); iClear "Hmem".
- iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
iDestruct "HPrange" as "#HPrange".
- iDestruct "HP" as "#HP".
iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
{
- iNext.
- iApply region_inv_construct; try done.
- subst la' ; auto.
- iExists lws; iSplit ; first done; iFrame "#∗".
+ iNext.
+ iApply region_inv_construct; try done; auto.
}
-
-
-
-
-
-
-
-
- iModIntro.
- iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗").
- iModIntro.
+ iSplitL "Ha"; first by iFrame.
- iMod (region_valid_alloc' _ b_pc' e_pc' a_pc' (a_pc'::la') (vsrc +1) (lwpc::lws) p_pc'
- with "[HPrange HP] [Hrange' Ha_next]")
- as "#Hinterp_src_next".
- { destruct p_pc' ; cbn in * ; try congruence; done. }
- { subst la' ; eapply list_remove_list_region ; auto.
+ iMod (region_valid_alloc' _ b e a (a::(list_remove_elem a (finz.seq_between b e))) (v +1) (pc_lw::lws) p
+ with "[HPrange HP] [Hrange' Ha_next]")
+ as "#Hinterp__next"; last done.
+ { destruct p ; cbn in * ; try congruence; done. }
+ { eapply list_remove_list_region ; auto.
apply list_remove_elem_in in Hapc_in_range.
by destruct Hapc_in_range as (la' & -> & ->).
}
- { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC".
+ { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P".
iSplit ; last iFrame "Hread_cond".
by rewrite Hlen_lws.
cbn.
iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
iAssert (
- (∀ (k : nat) (x0 : leibnizO LWord * D),
- ⌜zip lws Ps !! k = Some x0⌝
- → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
- )%I as "bla".
+ (∀ (k : nat) (x0 : leibnizO LWord * D),
+ ⌜zip lws Ps !! k = Some x0⌝
+ → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
+ )%I as "bla".
{ iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
- iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
+ iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
) as "blaa".
- iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
+ iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
by rewrite Hlen_lws.
iSplit.
by iApply "Hread".
- by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
+ by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
}
- { iClear "#". subst la'. clear -Hlen_Ps Hlen_lws.
+ { iClear "#". clear -Hlen_Ps Hlen_lws.
iApply big_sepL2_alt.
iSplit; first (iPureIntro; rewrite /= map_length; lia).
iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
rewrite fst_zip.
apply NoDup_fmap; auto.
{ by intros x y Heq ; simplify_eq. }
- rewrite /logical_region map_length ; lia.
+ rewrite /logical_region map_length Hlen_lws ; lia.
}
- iApply wp_pure_step_later; auto.
- iNext; iIntros "_".
+ +
+ iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
+ subst E'.
+ destruct Hvalid_sweep as [Hcontra|Hapc_notin_src] ; first done.
+ subst la.
+ rewrite !list_remove_elem_notin in Hvalid_lmem', Hlen_Ps, Hlen_lws |- * ; auto.
+
+
+ assert ( lmem' !! (pc_a, pc_v) = Some pc_lw ) as Hmem'_pca.
+ { eapply is_valid_updated_lmemory_preserves_lmem; eauto; by simplify_map_eq. }
+ assert ( logical_range_map b e lws v ⊆ lmem' )
+ as Hmem'_be.
+ {
+ eapply is_valid_updated_lmemory_lmem_incl with
+ (la := (finz.seq_between b e)) (v := v)
+ ; eauto.
+ eapply is_valid_updated_lmemory_insert; eauto.
+ eapply logical_range_notin; eauto.
+ eapply Forall_forall; intros a' Ha'.
+ eapply logical_range_version_neq; eauto ; last lia.
+ }
+ assert
+ (logical_range_map b e lws (v + 1) ⊆ lmem')
+ as Hmem'_be_next.
+ { clear -Hvalid_lmem' Hlen_lws Hapc_notin_src.
+ eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
+ assert (v' = v+1 /\ (a' ∈ (finz.seq_between b e)))
+ as [? Ha'_in_be] by (eapply logical_range_map_some_inv; eauto); simplify_eq.
+ destruct Hvalid_lmem'.
+ eapply lookup_weaken; last eauto.
+ rewrite update_version_region_preserves_lmem_next; eauto.
+ all: rewrite lookup_insert_ne //=; last (intro ; set_solver).
+ erewrite logical_region_map_lookup_versions; eauto.
+ eapply logical_region_version_neq; eauto; lia.
+ }
+
+ rewrite -(insert_id lmem' (pc_a, pc_v) pc_lw); auto.
+ iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]".
+ eapply delete_subseteq_r with (k := ((pc_a, pc_v) : LAddr)) in Hmem'_be
+ ; last (eapply logical_region_notin; eauto).
+ iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
+ ; first (eapply Hmem'_be).
+ eapply delete_subseteq_r with (k := ((pc_a, pc_v) : LAddr)) in Hmem'_be_next
+ ; last (eapply logical_region_notin ; eauto).
+ eapply delete_subseteq_list_r
+ with (m3 := list_to_map (zip (map (λ a : Addr, (a, v)) (finz.seq_between b e)) lws))
+ in Hmem'_be_next
+ ; eauto
+ ; last (by eapply update_logical_memory_region_disjoint).
+ iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
+ ; first (eapply Hmem'_be_next); iClear "Hmem".
+ iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
+ iDestruct "HPrange" as "#HPrange".
+ iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
+ {
+ iNext.
+ iApply region_inv_construct; try done; auto.
+ }
+ iSplitL "Ha_pc"; first by iFrame.
+
+
+ iMod (region_valid_alloc _ b e a (v +1) lws p
+ with "[HPrange] [Hrange']")
+ as "#Hinterp__next"; last done.
+ { destruct p ; cbn in * ; try congruence; done. }
+ { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P".
+ iSplit ; last iFrame "Hread_cond".
+ by rewrite <- Hlen_Ps, Hlen_lws.
+ cbn.
+ iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
+ iClear "Hread Hread_P HPrange".
+ iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
+ iAssert (
+ (∀ (k : nat) (x0 : leibnizO LWord * D),
+ ⌜zip lws Ps !! k = Some x0⌝
+ → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
+ )%I as "bla".
+ { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
+ iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
+ ) as "blaa".
+ iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
+ by rewrite Hlen_lws.
+ by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
+ }
+ { iClear "#". clear -Hlen_Ps Hlen_lws.
+ iApply big_sepL2_alt.
+ iSplit; first (iPureIntro; rewrite map_length; lia).
+ iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
+ rewrite fst_zip; first (apply NoDup_logical_region).
+ rewrite /logical_region map_length Hlen_lws ; lia.
+ }
+ Unshelve. Fail idtac. Admitted.
+
+
+ Local Instance if_Persistent
+ ppc bpc epc apc vpc lregs src psrc bsrc esrc asrc vsrc:
+ Persistent (if decide (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs)
+ src psrc bsrc esrc asrc vsrc
+ ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+ then interp (LCap psrc bsrc esrc asrc (vsrc + 1))
+ else emp)%I.
+ Proof. intros; case_decide; apply _. Qed.
+
+
+
+ Lemma isunique_case (lregs : leibnizO LReg)
+ (ppc : Perm) (bpc epc apc : Addr) (vpc : Version)
+ (lwpc : LWord) (dst src : RegName) (P : D):
+ ftlr_instr lregs ppc bpc epc apc vpc lwpc (IsUnique dst src) P.
+ Proof.
+ intros Hp Hsome i Hbae Hi.
+ iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha #HP Hcls HPC Hmap".
+ specialize (HpersP lwpc).
+ rewrite delete_insert_delete.
+ iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /=";
+ [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl.
+
+
+
+ assert(∀ x : RegName, is_Some (<[PC:=LCap ppc bpc epc apc vpc]> lregs !! x)) as Hsome'.
+ {
+ intros. destruct (decide (x = PC)) as [Hx|Hx].
+ rewrite Hx lookup_insert; unfold is_Some. by eexists.
+ by rewrite lookup_insert_ne.
+ }
+
+
+ assert (∃ psrc bsrc esrc asrc vsrc, read_reg_inr (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc vsrc)
+ as (psrc & bsrc & esrc & asrc & vsrc & HVsrc).
+ {
+ specialize Hsome' with src as Hsrc.
+ destruct Hsrc as [wsrc Hsomesrc].
+ unfold read_reg_inr. rewrite Hsomesrc.
+ destruct wsrc as [|[ psrc bsrc esrc asrc vsrc|] | ]; try done.
+ by repeat eexists.
+ }
+
+
+ iDestruct (create_sweep_res with "[$Hreg] [$Hinv] [%]") as (Ps) "[%Hlen_Ps HSweepRes]"
+ ; [ eassumption
+ | by apply elem_of_finz_seq_between
+ |].
+
+
+
+ iMod (sweep_res_implies_mem_map with "HSweepRes Ha") as (mem) "[HSweepMem >HMemRes]".
+ set (E := ⊤ ∖ ↑logN.@(apc, vpc)).
+ set (E' := allow_sweep_mask (list_remove_elem apc (finz.seq_between bsrc esrc)) vsrc apc vpc).
+ set (cond_open :=
+ decide
+ (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc
+ vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+ ).
+
+
+
+ iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC.
+
+
+
+ iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto.
+
+
+ iApply (wp_isunique with "[$Hmap $HMemRes]")
+ ; eauto
+ ; [ by simplify_map_eq
+ | rewrite /subseteq /map_subseteq /set_subseteq_instance
+ ; intros rr _; apply elem_of_dom
+ ; rewrite lookup_insert_is_Some';
+ eauto
+ |].
+ iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)".
+ destruct Hspec as
+ [ psrc' bsrc' esrc' asrc' vsrc' Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC
+ | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC
+ | lwsrc' psrc' bsrc' esrc' asrc' vsrc' Hlwsrc Hlwsrc' Hmem' Hincr_PC
+ | ? ? Hfail]
+ ; simplify_map_eq
+ ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq)
+ ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq)
+ ; try (cbn in Hlwsrc' ; simplify_eq).
+
+
+ {
+ rewrite /read_reg_inr Hlwsrc' in HVsrc ; simplify_eq.
+ iMod (mem_map_recover_res_upd with "Hread HP HSweepMem Hmem") as "[Ha #Hinterp]"; auto.
+
+
+ iModIntro.
+ iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗").
+ iModIntro.
+ iApply wp_pure_step_later; auto.
+ iNext; iIntros "_".
+ simplify_map_eq.
+
+
+ incrementLPC_inv
+ as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
+ ; simplify_map_eq.
+ assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
+ clear cond_open; set (cond_open := decide ( _ /\ _ )).
+ destruct cond_open as [Hdecide|Hdecide]; cycle 1.
+ -
+ apply cond_open_contra in Hdecide; auto ; simplify_eq.
+ assert (src ≠ PC)
+ as Hr_ne_pc
+ by (intro ; subst ; inversion i
+ ; inversion H1 ; cbn in * ; simplify_map_eq
+ ; by destruct H8).
+ do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert.
simplify_map_eq.
- iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]")
+ iApply ("IH" $! (<[dst := LInt 1]> (<[src := _]> lregs)) with "[%] [] [Hmap] [$Hown]")
; eauto.
{ intro; by repeat (rewrite lookup_insert_is_Some'; right). }
{ iIntros (r1 lw1 Hr1 Hlw1).
destruct (decide (r1 = dst)) as [ |Hr1_dst]
; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
- iApply "Hreg"; eauto. }
- { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. }
-
-
- -
- destruct Hvalid_sweep as [Hcontra|Hapc_notin_src] ; first done.
- incrementLPC_inv
- as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
- ; simplify_map_eq.
- assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
- do 2 (rewrite (insert_commute _ _ PC) //); rewrite insert_insert.
-
-
- assert ( lmem' !! (a_pc', v_pc') = Some lwpc ) as Hmem'_pca.
- { eapply is_valid_updated_lmemory_preserves_lmem; eauto. }
-
- iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
- subst E'.
- rewrite /read_reg_inr in HVsrc; simplify_map_eq.
- rewrite !list_remove_elem_notin in Hupd, Hlen_Ps, Hlen_lws |- * ; auto.
-
-
- assert ( logical_range_map bsrc esrc lws vsrc ⊆ lmem' )
- as Hmem'_be.
- {
- eapply is_valid_updated_lmemory_lmem_incl with
- (la := (finz.seq_between bsrc esrc)) (v := vsrc)
- ; eauto.
- eapply is_valid_updated_lmemory_insert; eauto.
- eapply logical_range_notin; eauto.
- eapply Forall_forall; intros a Ha.
- eapply logical_range_version_neq; eauto ; last lia.
- }
-
- assert
- (logical_range_map bsrc esrc lws (vsrc + 1) ⊆ lmem')
- as Hmem'_be_next.
- { clear -Hupd Hlen_lws Hapc_notin_src.
- eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
- assert (v' = vsrc+1 /\ (a' ∈ (finz.seq_between bsrc esrc)))
- as [? Ha'_in_be] by (eapply logical_range_map_some_inv; eauto); simplify_eq.
- destruct Hupd.
- eapply lookup_weaken; last eauto.
- rewrite update_version_region_preserves_lmem_next; eauto.
- all: rewrite lookup_insert_ne //=; last (intro ; set_solver).
- erewrite logical_region_map_lookup_versions; eauto.
- eapply logical_region_version_neq; eauto; lia.
- }
-
- rewrite -(insert_id lmem' (a_pc', v_pc') lwpc); auto.
- iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]".
- eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be
- ; last (eapply logical_region_notin; eauto).
- iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
- ; first (eapply Hmem'_be).
- eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be_next
- ; last (eapply logical_region_notin ; eauto).
- eapply delete_subseteq_list_r
- with (m3 := list_to_map (zip (map (λ a : Addr, (a, vsrc)) (finz.seq_between bsrc esrc)) lws))
- in Hmem'_be_next
- ; eauto
- ; last (by eapply update_logical_memory_region_disjoint).
- iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
- ; first (eapply Hmem'_be_next); iClear "Hmem".
- iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
- iDestruct "HPrange" as "#HPrange".
-
-
- iMod (region_valid_alloc _ bsrc esrc asrc (vsrc +1) lws psrc
- with "[HPrange] [Hrange']")
- as "#Hinterp_src_next".
- { destruct psrc ; cbn in * ; try congruence; done. }
- { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC".
- iSplit ; last iFrame "Hread_cond".
- by rewrite Hlen_lws.
- cbn.
- iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
- iClear "IH Hinv Hinva Hreg Hread Hwrite Hread_PSRC HPrange".
- iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
- iAssert (
- (∀ (k : nat) (x0 : leibnizO LWord * D),
- ⌜zip lws Ps !! k = Some x0⌝
- → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
- )%I as "bla".
- { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
- iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
- ) as "blaa".
- iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
- by rewrite Hlen_lws.
- by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
- }
- { iClear "#". clear -Hlen_Ps Hlen_lws.
- iApply big_sepL2_alt.
- iSplit; first (iPureIntro; rewrite map_length; lia).
- iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
- rewrite fst_zip; first (apply NoDup_logical_region).
- rewrite /logical_region map_length ; lia.
- }
-
- iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
- {
- iNext.
- iApply region_inv_construct; auto.
+ destruct (decide (r1 = src)) as [ |Hr1_src]
+ ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+ iApply "Hreg"; eauto.
+ }
+ { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
+ - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hwf].
+ destruct (decide (src = PC)) as [->|Hsrc_neq_pc]
+ ; [clear Hwf | destruct Hwf ; simplify_eq]
+ ; simplify_map_eq
+ ; do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert.
+ +
+ iApply ("IH" $! (<[dst := LInt 1]> lregs) with "[%] [] [Hmap] [$Hown]")
+ ; eauto.
+ { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
+ { iIntros (r1 lw1 Hr1 Hlw1).
+ destruct (decide (r1 = dst)) as [ |Hr1_dst]
+ ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+ iApply "Hreg"; eauto.
}
- iModIntro.
- iMod ("Hcls" with "[Ha_pc HP]") as "_"; first (iNext ; iExists _ ; iFrame).
- iModIntro.
-
-
- iApply wp_pure_step_later; auto.
- iNext; iIntros "_".
- simplify_map_eq.
- iApply ("IH" $! (<[dst := _]> (<[ src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]")
+ { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
+ +
+ iApply ("IH" $! (<[dst := LInt 1]> ( <[src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]")
; eauto.
{ intro; by repeat (rewrite lookup_insert_is_Some'; right). }
{ iIntros (r1 lw1 Hr1 Hlw1).
destruct (decide (r1 = dst)) as [ |Hr1_dst]
; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
destruct (decide (r1 = src)) as [ |Hr1_src]
- ; simplify_map_eq; first done.
- iApply "Hreg"; eauto. }
- { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. }
+ ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+ iApply "Hreg"; eauto.
+ }
+ { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
}
-
-
-
-
{
iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
subst E.
iModIntro.
- iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro].
+ iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro]; auto.
iApply wp_pure_step_later; auto.
iNext; iIntros "_".
incrementLPC_inv; simplify_map_eq.
@@ -875,7 +908,7 @@ cap_machine.ftlr.IsUnique
iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
subst E.
iModIntro.
- iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro].
+ iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro]; auto.
iApply wp_pure_step_later; auto.
iNext; iIntros "_".
incrementLPC_inv; simplify_map_eq.
@@ -898,8 +931,7 @@ cap_machine.ftlr.IsUnique
iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
subst E.
iModIntro.
- iMod ("Hcls" with "[Ha HP]") as "_".
- iNext; iExists lwpc ; iFrame.
+ iMod ("Hcls" with "[Ha HP]") as "_"; auto.
iModIntro.
iApply wp_pure_step_later; auto.
iNext; iIntros "_"; iApply wp_value; auto.
diff --git a/branch/june/attestation_refactor_ftlr/indexpage.html b/branch/june/attestation_refactor_ftlr/indexpage.html
index 83ad0608..180a7d1b 100644
--- a/branch/june/attestation_refactor_ftlr/indexpage.html
+++ b/branch/june/attestation_refactor_ftlr/indexpage.html
@@ -56,7 +56,7 @@
Z |
_ |
other |
-(2298 entries) |
+(2301 entries) |
Notation Index |
@@ -216,7 +216,7 @@
Z |
_ |
other |
-(943 entries) |
+(945 entries) |
Constructor Index |
@@ -315,6 +315,38 @@
(47 entries) |
+Instance Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(142 entries) |
+
+
Section Index |
A |
B |
@@ -347,38 +379,6 @@
(62 entries) |
-Instance Index |
-A |
-B |
-C |
-D |
-E |
-F |
-G |
-H |
-I |
-J |
-K |
-L |
-M |
-N |
-O |
-P |
-Q |
-R |
-S |
-T |
-U |
-V |
-W |
-X |
-Y |
-Z |
-_ |
-other |
-(141 entries) |
-
-
Abbreviation Index |
A |
B |
@@ -667,6 +667,7 @@ Global Index
compute_mask_union [lemma, in cap_machine.logrel]
compute_mask_difference [lemma, in cap_machine.logrel]
compute_mask [definition, in cap_machine.logrel]
+cond_open_contra [lemma, in cap_machine.ftlr.IsUnique]
Conf [definition, in cap_machine.cap_lang]
ConfFlag [inductive, in cap_machine.cap_lang]
ConfFlag_sind [definition, in cap_machine.cap_lang]
@@ -1163,6 +1164,7 @@ Global Index
head_ctx_step_val [lemma, in cap_machine.cap_lang]
helpers [section, in cap_machine.proofmode.tactics_helpers]
I
+if_Persistent [instance, in cap_machine.ftlr.IsUnique]
if_Persistent [instance, in cap_machine.ftlr.Load]
if_persistent [instance, in cap_machine.ftlr.interp_weakening]
IH [definition, in cap_machine.ftlr.interp_weakening]
@@ -1674,6 +1676,7 @@ Global Index
memMap_resource_1 [lemma, in cap_machine.rules.rules_base]
memMap_resource_0 [lemma, in cap_machine.rules.rules_base]
MemNum [definition, in cap_machine.addr_reg]
+mem_map_recover_res_upd [lemma, in cap_machine.ftlr.IsUnique]
mem_map_recover_res_noup [lemma, in cap_machine.ftlr.IsUnique]
mem_map_implies_pure_conds [lemma, in cap_machine.ftlr.IsUnique]
mem_map_recover_res [lemma, in cap_machine.ftlr.Load]
@@ -3052,6 +3055,7 @@ Lemma Index
compute_mask_mono [in cap_machine.logrel]
compute_mask_union [in cap_machine.logrel]
compute_mask_difference [in cap_machine.logrel]
+cond_open_contra [in cap_machine.ftlr.IsUnique]
ContiguousRegion_InCtx [in machine_utils.solve_pure]
contiguous_betweenL_program_split [in cap_machine.proofmode.contiguous]
contiguous_betweenL_contiguous_between [in cap_machine.proofmode.contiguous]
@@ -3477,6 +3481,7 @@ Lemma Index
memMap_resource_1_dq [in cap_machine.rules.rules_base]
memMap_resource_1 [in cap_machine.rules.rules_base]
memMap_resource_0 [in cap_machine.rules.rules_base]
+mem_map_recover_res_upd [in cap_machine.ftlr.IsUnique]
mem_map_recover_res_noup [in cap_machine.ftlr.IsUnique]
mem_map_implies_pure_conds [in cap_machine.ftlr.IsUnique]
mem_map_recover_res [in cap_machine.ftlr.Load]
@@ -4260,84 +4265,6 @@ Projection Index
SG_storedPreds [in cap_machine.seal_store]
SG_sealStore [in cap_machine.seal_store]
-Section Index
-A
-Assert [in cap_machine.examples.assert]
-
C
-cap_lang_rules [in cap_machine.rules.rules_IsUnique]
-cap_lang_rules [in cap_machine.rules.rules_Jnz]
-cap_lang_rules [in cap_machine.rules.rules_Subseg]
-cap_lang_rules [in cap_machine.rules.rules_Store]
-cap_lang_rules [in cap_machine.rules.rules_Lea]
-cap_lang_rules [in cap_machine.rules.rules_EStoreId]
-cap_lang_rules [in cap_machine.rules.rules_Seal]
-cap_lang_rules [in cap_machine.rules.rules_EInit]
-cap_lang_rules [in cap_machine.rules.rules_UnSeal]
-cap_lang_rules_opt [in cap_machine.rules.rules_base]
-cap_lang_rules [in cap_machine.rules.rules_base]
-cap_lang_rules [in cap_machine.rules.rules_Jmp]
-cap_lang_rules [in cap_machine.rules.rules_EDeInit]
-cap_lang_rules [in cap_machine.rules.rules_Mov]
-cap_lang_rules [in cap_machine.rules.rules_Load]
-cap_lang_rules [in cap_machine.rules.rules_AddSubLt]
-cap_lang_rules [in cap_machine.rules.rules_Restrict]
-cap_lang_rules [in cap_machine.rules.rules_Get]
-codefrag [in cap_machine.proofmode.region]
-codefrag [in cap_machine.proofmode.proofmode]
-codefrag_subblock [in cap_machine.proofmode.proofmode]
-Contiguous [in cap_machine.proofmode.contiguous]
-ContiguousL [in cap_machine.proofmode.contiguous]
-
D
-denote_domain [in cap_machine.proofmode.register_tactics]
-disjoint_list [in cap_machine.proofmode.disjoint_regions_tactics]
-
F
-finz_lemmas [in machine_utils.finz_base]
-finz.finz [in machine_utils.finz_base]
-fundamental [in cap_machine.ftlr.IsUnique]
-fundamental [in cap_machine.ftlr.Lea]
-fundamental [in cap_machine.ftlr.AddSubLt]
-fundamental [in cap_machine.ftlr.Load]
-fundamental [in cap_machine.ftlr.UnSeal]
-fundamental [in cap_machine.ftlr.Store]
-fundamental [in cap_machine.ftlr.Restrict]
-fundamental [in cap_machine.ftlr.Subseg]
-fundamental [in cap_machine.ftlr.interp_weakening]
-fundamental [in cap_machine.ftlr.ftlr_base]
-fundamental [in cap_machine.ftlr.Seal]
-fundamental [in cap_machine.ftlr.Mov]
-fundamental [in cap_machine.fundamental]
-fundamental [in cap_machine.ftlr.Jmp]
-fundamental [in cap_machine.ftlr.Get]
-fundamental [in cap_machine.ftlr.Jnz]
-
H
-helpers [in cap_machine.proofmode.tactics_helpers]
-
I
-instr_encodings [in cap_machine.examples.addr_reg_sample]
-
L
-lemmas [in machine_utils.finz_interval]
-Linking [in cap_machine.linking]
-logrel [in cap_machine.logrel]
-
M
-machine_param [in cap_machine.logical_mapsto]
-macros [in cap_machine.examples.macros]
-macros [in cap_machine.examples.macros_new]
-monotone [in cap_machine.monotone]
-
N
-named [in cap_machine.proofmode.NamedProp]
-
O
-opsem [in cap_machine.cap_lang]
-
R
-region [in cap_machine.proofmode.region]
-
S
-SimpleMalloc [in cap_machine.examples.malloc]
-SimpleSalloc [in cap_machine.examples.salloc]
-simpl_gmap [in cap_machine.proofmode.map_simpl]
-Store [in cap_machine.seal_store]
-
T
-tests.tests [in cap_machine.proofmode.NamedProp]
-
W
-word_type_encoding [in cap_machine.machine_parameters]
-
Instance Index
A
addr_inhabited [in cap_machine.machine_base]
@@ -4384,6 +4311,7 @@ Instance Index
H
hasValidAddress_dec [in cap_machine.logrel]
I
+if_Persistent [in cap_machine.ftlr.IsUnique]
if_Persistent [in cap_machine.ftlr.Load]
if_persistent [in cap_machine.ftlr.interp_weakening]
IncrFinZ_InCtx [in machine_utils.solve_pure]
@@ -4498,6 +4426,84 @@ Instance Index
Z
ZToFinZ_z_of [in machine_utils.class_instances]
+Section Index
+A
+Assert [in cap_machine.examples.assert]
+
C
+cap_lang_rules [in cap_machine.rules.rules_IsUnique]
+cap_lang_rules [in cap_machine.rules.rules_Jnz]
+cap_lang_rules [in cap_machine.rules.rules_Subseg]
+cap_lang_rules [in cap_machine.rules.rules_Store]
+cap_lang_rules [in cap_machine.rules.rules_Lea]
+cap_lang_rules [in cap_machine.rules.rules_EStoreId]
+cap_lang_rules [in cap_machine.rules.rules_Seal]
+cap_lang_rules [in cap_machine.rules.rules_EInit]
+cap_lang_rules [in cap_machine.rules.rules_UnSeal]
+cap_lang_rules_opt [in cap_machine.rules.rules_base]
+cap_lang_rules [in cap_machine.rules.rules_base]
+cap_lang_rules [in cap_machine.rules.rules_Jmp]
+cap_lang_rules [in cap_machine.rules.rules_EDeInit]
+cap_lang_rules [in cap_machine.rules.rules_Mov]
+cap_lang_rules [in cap_machine.rules.rules_Load]
+cap_lang_rules [in cap_machine.rules.rules_AddSubLt]
+cap_lang_rules [in cap_machine.rules.rules_Restrict]
+cap_lang_rules [in cap_machine.rules.rules_Get]
+codefrag [in cap_machine.proofmode.region]
+codefrag [in cap_machine.proofmode.proofmode]
+codefrag_subblock [in cap_machine.proofmode.proofmode]
+Contiguous [in cap_machine.proofmode.contiguous]
+ContiguousL [in cap_machine.proofmode.contiguous]
+
D
+denote_domain [in cap_machine.proofmode.register_tactics]
+disjoint_list [in cap_machine.proofmode.disjoint_regions_tactics]
+
F
+finz_lemmas [in machine_utils.finz_base]
+finz.finz [in machine_utils.finz_base]
+fundamental [in cap_machine.ftlr.IsUnique]
+fundamental [in cap_machine.ftlr.Lea]
+fundamental [in cap_machine.ftlr.AddSubLt]
+fundamental [in cap_machine.ftlr.Load]
+fundamental [in cap_machine.ftlr.UnSeal]
+fundamental [in cap_machine.ftlr.Store]
+fundamental [in cap_machine.ftlr.Restrict]
+fundamental [in cap_machine.ftlr.Subseg]
+fundamental [in cap_machine.ftlr.interp_weakening]
+fundamental [in cap_machine.ftlr.ftlr_base]
+fundamental [in cap_machine.ftlr.Seal]
+fundamental [in cap_machine.ftlr.Mov]
+fundamental [in cap_machine.fundamental]
+fundamental [in cap_machine.ftlr.Jmp]
+fundamental [in cap_machine.ftlr.Get]
+fundamental [in cap_machine.ftlr.Jnz]
+
H
+helpers [in cap_machine.proofmode.tactics_helpers]
+
I
+instr_encodings [in cap_machine.examples.addr_reg_sample]
+
L
+lemmas [in machine_utils.finz_interval]
+Linking [in cap_machine.linking]
+logrel [in cap_machine.logrel]
+
M
+machine_param [in cap_machine.logical_mapsto]
+macros [in cap_machine.examples.macros]
+macros [in cap_machine.examples.macros_new]
+monotone [in cap_machine.monotone]
+
N
+named [in cap_machine.proofmode.NamedProp]
+
O
+opsem [in cap_machine.cap_lang]
+
R
+region [in cap_machine.proofmode.region]
+
S
+SimpleMalloc [in cap_machine.examples.malloc]
+SimpleSalloc [in cap_machine.examples.salloc]
+simpl_gmap [in cap_machine.proofmode.map_simpl]
+Store [in cap_machine.seal_store]
+
T
+tests.tests [in cap_machine.proofmode.NamedProp]
+
W
+word_type_encoding [in cap_machine.machine_parameters]
+
Abbreviation Index
A
Addr [in cap_machine.addr_reg]
@@ -5316,7 +5322,7 @@ Record Index
Z |
_ |
other |
-(2298 entries) |
+(2301 entries) |
Notation Index |
@@ -5476,7 +5482,7 @@ Record Index
Z |
_ |
other |
-(943 entries) |
+(945 entries) |
Constructor Index |
@@ -5575,6 +5581,38 @@ Record Index
(47 entries) |
+Instance Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(142 entries) |
+
+
Section Index |
A |
B |
@@ -5607,38 +5645,6 @@ Record Index
(62 entries) |
-Instance Index |
-A |
-B |
-C |
-D |
-E |
-F |
-G |
-H |
-I |
-J |
-K |
-L |
-M |
-N |
-O |
-P |
-Q |
-R |
-S |
-T |
-U |
-V |
-W |
-X |
-Y |
-Z |
-_ |
-other |
-(141 entries) |
-
-
Abbreviation Index |
A |
B |