Move side lemmas in the files they belong

Author: JuneRousseau

_CoqProject

@@ -43,7 +43,7 @@ theories/proofmode/register_tactics.v
 # Program logic: Unary WP rules
 theories/program_logic/transiently.v
 theories/program_logic/wp_opt.v
-theories/program_logic/cerisier_state_interp.v
+theories/program_logic/base_logic.v
 theories/program_logic/rules_base.v
 theories/program_logic/rules_fail.v
 theories/program_logic/rules/rules_Get.v

theories/logrel/ftlr/EInit.v

@@ -6,56 +6,6 @@ From cap_machine.logrel Require Import ftlr_base interp_weakening.
 From cap_machine.program_logic Require Import rules_EInit.
 From cap_machine Require Import proofmode.
 
-(* TODO generalise *)
-Lemma map_Forall_all_P (w : LWord) (la : list Addr) (lws : list LWord) (v : Version)
-  (P : LWord -> Prop) :
-  NoDup la ->
-  length lws = length la ->
-  w ∈ lws ->
-  map_Forall
-    (λ (a : LAddr) (lw : LWord), laddr_get_addr a ∈ la ∧ (laddr_get_version a) = v  → P lw)
-    (logical_region_map la lws v)
-  -> P w.
-Proof.
-  generalize dependent lws.
-  generalize dependent w.
-  induction la as [|a la]; intros w lws Hnodup Hlen Hw Hall_z.
-  - destruct lws ; set_solver.
-  - destruct lws as [|w1 lws] ; first set_solver.
-    cbn in Hlen ; simplify_eq.
-    apply NoDup_cons in Hnodup as [Ha_notin_l Hnodup].
-    cbn in Hall_z.
-    apply map_Forall_insert in Hall_z as [Hladdr Hall_z].
-    2: { rewrite -not_elem_of_list_to_map.
-         intro Hcontra.
-         rewrite elem_of_list_fmap in Hcontra.
-         destruct Hcontra as ([x vx] & Hx & Hcontra)
-         ; cbn in Hx ; simplify_eq.
-         apply elem_of_zip_l in Hcontra.
-         rewrite elem_of_list_fmap in Hcontra.
-         destruct Hcontra as (y & Hy & Hcontra)
-         ; cbn in Hy ; simplify_eq.
-         set_solver.
-    }
-    apply elem_of_cons in Hw as [-> | Hw].
-    * apply Hladdr; set_solver.
-    * eapply IHla; eauto.
-      eapply map_Forall_impl; eauto.
-      intros [y vy] wy IH Hy; cbn in *.
-      apply IH.
-      set_solver.
-Qed.
-
-Lemma elem_of_logical_region (a : Addr) (la : list Addr) (v : Version) :
-  a ∈ la <->
-    (a, v) ∈ logical_region la v.
-Proof.
-  split; rewrite /logical_region; intros Ha.
-  - by apply elem_of_list_fmap; exists a.
-  - apply elem_of_list_fmap in Ha.
-    by destruct Ha as (? & ? & ?); simplify_eq.
-Qed.
-
 Section fundamental.
   Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}

theories/opsem/cap_lang.v

@@ -415,6 +415,29 @@ Proof.
   ; [eapply sweep_registers_addr_spec | eapply sweep_memory_addr_spec].
 Qed.
 
+Lemma sweep_implies_no_pc {phr phm p pc_b pc_e pc_a r a} b e :
+  phr !! PC = Some (WCap p pc_b pc_e pc_a)
+  → phr !! r = Some (WCap RX b e a)
+  → sweep_reg phm phr r = true
+  → r ≠ PC
+  -> pc_a ∈ finz.seq_between pc_b pc_e
+  → pc_a ∉ finz.seq_between b e.
+Proof.
+  intros Hpc Hr Hsweep Hinbouds pcHrpc.
+  unfold sweep_reg, sweep_memory_reg, sweep_registers_reg in Hsweep.
+  rewrite Hr in Hsweep.
+  rewrite andb_true_iff in Hsweep.
+  destruct Hsweep as [_ Hsweep].
+  unfold unique_in_registers in *.
+  rewrite bool_decide_eq_true in Hsweep.
+  rewrite map_Forall_lookup in Hsweep.
+  eapply Hsweep in Hpc.
+  destruct (decide (PC = r)); eauto.
+  apply overlap_word_disjoint in Hpc.
+  intro Hpca.
+  eapply elem_of_disjoint; eauto.
+Qed.
+
 Section opsem.
   Context `{MachineParameters}.
 

…es/program_logic/cerisier_state_interp.v theories/program_logic/base_logic.vtheories/program_logic/cerisier_state_interp.v renamed to theories/program_logic/base_logic.v theories/program_logic/cerisier_state_interp.v renamed to theories/program_logic/base_logic.v

@@ -1197,7 +1197,25 @@ Proof.
   now eapply lookup_insert.
 Qed.
 
-Lemma update_version_region_insert
+Lemma update_version_region_insert (glmem llmem : LMem) (a : Addr) (la : list Addr) (v v' : Version) (lw : LWord) :
+  a ∉ la ->
+  (<[(a, v):= lw]> (update_version_region glmem la v' llmem)) =
+  (update_version_region (<[(a, v):= lw]> glmem) la v' (<[(a, v):= lw]> llmem)).
+Proof.
+  revert a v v' lw glmem llmem.
+  induction la; intros a' v v' lw glmem llmem Ha'; first set_solver.
+  cbn.
+  rewrite -/(update_version_region glmem la v' llmem).
+  rewrite -/(update_version_region (<[(a', v):=lw]> glmem) la v' (<[(a', v):=lw]> llmem)).
+  rewrite /update_version_addr.
+  rewrite lookup_insert_ne; last (intro; simplify_eq; set_solver).
+  destruct ( glmem !! (a, v') ) eqn:Ha_glmem; rewrite Ha_glmem.
+  - rewrite insert_commute; last (intro; simplify_eq; set_solver).
+    rewrite IHla; set_solver.
+  - rewrite IHla; set_solver.
+Qed.
+
+Lemma update_version_region_insert_subseteq
   (glmem lmem lmem' : LMem) (la : list Addr) (a' : Addr) (v v' : Version) (lw : LWord):
   NoDup la ->
   a' ∉ la ->
@@ -1775,7 +1793,7 @@ Proof.
     + split; cbn in *; try done.
       eapply insert_subseteq_r_inv; eauto.
   - destruct Hvalid as (Hupd & Hgl_llmem & HmaxMap' & HnextMap).
-    split; first (eapply update_version_region_insert; eauto).
+    split; first (eapply update_version_region_insert_subseteq; eauto).
     split; auto.
     eapply insert_subseteq_r_inv; eauto.
 Qed.
@@ -2197,6 +2215,76 @@ Proof.
   eapply lmeasure_measure_aux; eauto.
 Qed.
 
+Definition lmeasure `{MP : MachineParameters} (m : LMem) (b e: Addr) v : option Z :=
+  hash_instr ← hash_lmemory_range m (b^+1)%a e v;
+  Some (hash_concat (hash b) hash_instr).
+
+Lemma lmeasure_weaken_aux (lmem lmt: LMem) (la : list Addr) (v : Version) :
+  lmem ⊆ lmt →
+  Forall (fun a => is_Some (lmem !! (a, v))) la →
+  lmemory_get_instrs lmem la v = lmemory_get_instrs lmt la v.
+Proof.
+  intros Hincl Hall.
+  induction la ; first done.
+  rewrite Forall_cons in Hall. destruct Hall as [ [w Ha] Hall].
+  apply IHla in Hall.
+  assert (lmt !! (a, v) = Some w) as Ha' by (eapply lookup_weaken in Ha ; eauto).
+  cbn.
+  rewrite -/(lmemory_get_instrs lmem la v) -/(lmemory_get_instrs lmt la v).
+  by rewrite Ha Ha' Hall.
+Qed.
+
+Lemma lmeasure_weaken `{MP : MachineParameters} {lmem lmt} {b e v} :
+  lmem ⊆ lmt →
+  Forall (fun a => is_Some (lmem !! (a, v))) (finz.seq_between b e) →
+  hash_lmemory_range lmem b e v = hash_lmemory_range lmt b e v.
+Proof.
+  intros Hincl Hall.
+  rewrite /hash_lmemory_range.
+  erewrite lmeasure_weaken_aux; eauto.
+Qed.
+
+Definition ensures_is_zL (lmem : LMem) (b e : Addr) (v : Version) : Prop :=
+  map_Forall (fun la lw => (laddr_get_addr la) ∈ (finz.seq_between b e) ∧ (laddr_get_version la) = v
+                        -> is_zL lw) lmem.
+
+Lemma ensures_is_z_corresponds {phr phm lr lm vmap} {p} {b e a} {v} :
+  state_phys_log_corresponds phr phm lr lm vmap →
+  is_cur_word (LCap p b e a v) vmap ->
+  ensures_is_z phm b e →
+  ensures_is_zL lm b e v.
+Proof.
+  intros Hcorr Hr Hensure_z.
+  rewrite /ensures_is_zL.
+  rewrite /ensures_is_z in Hensure_z.
+  apply bool_decide_unpack in Hensure_z.
+  destruct Hcorr as [ Hreg (? & ? & ?) ].
+  rewrite /is_cur_word in Hr.
+  rewrite /mem_vmap_root in H0.
+  rewrite /mem_current_version in H.
+  rewrite map_Forall_lookup in H.
+  rewrite map_Forall_lookup.
+  intros [a' v'] lw Hla [Hla_in ?]; cbn in *; simplify_eq.
+  specialize (Hr a' Hla_in).
+  rewrite map_Forall_lookup in H0; eauto.
+  eapply H0 in Hr.
+  destruct Hr as (?&?&?&?); cbn in *.
+  rewrite map_Forall_lookup in Hensure_z; eauto.
+  rewrite H2 in Hla; simplify_eq.
+  apply Hensure_z in H3; eauto.
+  destruct lw ; eauto.
+Qed.
+
+Lemma ensures_is_z_mono {lm lm'} {b e} {v}  :
+  lm ⊆ lm' → ensures_is_zL lm' b e v -> ensures_is_zL lm b e v.
+Proof.
+  intros Hsub Hensure_is_zL.
+  rewrite /ensures_is_zL in Hensure_is_zL |- *.
+  rewrite map_Forall_lookup.
+  intros [a v'] lw Hla [Hin ?] ; cbn in *; simplify_eq.
+  eapply lookup_weaken in Hla; eauto.
+Qed.
+
 End Logical_mapsto.
 
 Section lmachine_param.
@@ -2287,10 +2375,8 @@ Qed.
 
 (** Miscellaneous about logical regions *)
 (* TODO move definition to regions.v ? *)
-
 Lemma elem_of_logical_region (a : Addr) (la : list Addr) (v : Version) :
-  a ∈ la <->
-    (a, v) ∈ logical_region la v.
+  a ∈ la <-> (a, v) ∈ logical_region la v.
 Proof.
   split; rewrite /logical_region; intros Ha.
   - by apply elem_of_list_fmap; exists a.
@@ -2860,3 +2946,43 @@ Proof.
   cbn. intros Hreg Hcurregs.
   apply (map_Forall_lookup_1 _ _ _ _ Hcurregs Hreg).
 Qed.
+
+(* TODO generalise *)
+Lemma map_Forall_all_P (w : LWord) (la : list Addr) (lws : list LWord) (v : Version)
+  (P : LWord -> Prop) :
+  NoDup la ->
+  length lws = length la ->
+  w ∈ lws ->
+  map_Forall
+    (λ (a : LAddr) (lw : LWord), laddr_get_addr a ∈ la ∧ (laddr_get_version a) = v  → P lw)
+    (logical_region_map la lws v)
+  -> P w.
+Proof.
+  generalize dependent lws.
+  generalize dependent w.
+  induction la as [|a la]; intros w lws Hnodup Hlen Hw Hall_z.
+  - destruct lws ; set_solver.
+  - destruct lws as [|w1 lws] ; first set_solver.
+    cbn in Hlen ; simplify_eq.
+    apply NoDup_cons in Hnodup as [Ha_notin_l Hnodup].
+    cbn in Hall_z.
+    apply map_Forall_insert in Hall_z as [Hladdr Hall_z].
+    2: { rewrite -not_elem_of_list_to_map.
+         intro Hcontra.
+         rewrite elem_of_list_fmap in Hcontra.
+         destruct Hcontra as ([x vx] & Hx & Hcontra)
+         ; cbn in Hx ; simplify_eq.
+         apply elem_of_zip_l in Hcontra.
+         rewrite elem_of_list_fmap in Hcontra.
+         destruct Hcontra as (y & Hy & Hcontra)
+         ; cbn in Hy ; simplify_eq.
+         set_solver.
+    }
+    apply elem_of_cons in Hw as [-> | Hw].
+    * apply Hladdr; set_solver.
+    * eapply IHla; eauto.
+      eapply map_Forall_impl; eauto.
+      intros [y vy] wy IH Hy; cbn in *.
+      apply IH.
+      set_solver.
+Qed.

theories/program_logic/logical_mapsto.v

@@ -91,48 +91,6 @@ Section cap_lang_rules.
 
     EInit_fail lregs lmem  r_code r_data tidx ot.
 
-  Definition ensures_is_zL lmem b e v : Prop :=
-    map_Forall (fun la lw => (laddr_get_addr la) ∈ (finz.seq_between b e) ∧ (laddr_get_version la) = v
-                          -> is_zL lw) lmem.
-
-  Lemma ensures_is_z_corresponds {phr phm lr lm vmap} {r} {p} {b e a} {v} :
-    state_phys_log_corresponds phr phm lr lm vmap →
-    is_cur_word (LCap p b e a v) vmap ->
-    ensures_is_z phm b e →
-    ensures_is_zL lm b e v.
-  Proof.
-    intros Hcorr Hr Hensure_z.
-    rewrite /ensures_is_zL.
-    rewrite /ensures_is_z in Hensure_z.
-    apply bool_decide_unpack in Hensure_z.
-    destruct Hcorr as [ Hreg (? & ? & ?) ].
-    rewrite /is_cur_word in Hr.
-    rewrite /mem_vmap_root in H0.
-    rewrite /mem_current_version in H.
-    rewrite map_Forall_lookup in H.
-    rewrite map_Forall_lookup.
-    intros [a' v'] lw Hla [Hla_in ?]; cbn in *; simplify_eq.
-    specialize (Hr a' Hla_in).
-    rewrite map_Forall_lookup in H0; eauto.
-    eapply H0 in Hr.
-    destruct Hr as (?&?&?&?); cbn in *.
-    rewrite map_Forall_lookup in Hensure_z; eauto.
-    rewrite H2 in Hla; simplify_eq.
-    apply Hensure_z in H3; eauto.
-    destruct lw ; eauto.
-  Qed.
-
-  Lemma ensures_is_z_mono {lm lm'} {b e} {v}  :
-    lm ⊆ lm' →
-    ensures_is_zL lm' b e v -> ensures_is_zL lm b e v.
-  Proof.
-    intros Hsub Hensure_is_zL.
-    rewrite /ensures_is_zL in Hensure_is_zL |- *.
-    rewrite map_Forall_lookup.
-    intros [a v'] lw Hla [Hin ?] ; cbn in *; simplify_eq.
-    eapply lookup_weaken in Hla; eauto.
-  Qed.
-
   Definition EInit_spec_success (lregs lregs' : LReg) (lmem1 lmem4 : LMem) (tidx tidx_incr : TIndex)
     (ot : OType) (r_code r_data : RegName) (retv : val) : iProp Σ :=
     ∃ glmem lmem2 lmem3 (code_b code_e code_a : Addr) (code_v : Version) (data_b data_e data_a : Addr)
@@ -185,77 +143,6 @@ Section cap_lang_rules.
     -> readAllowed p = true
     -> (finz.seq_between b e) ## reserved_addresses.
 
-  Definition lmeasure (m : LMem) (b e: Addr) v : option Z :=
-    hash_instr ← hash_lmemory_range m (b^+1)%a e v;
-    Some (hash_concat (hash b) hash_instr).
-
-
-  Lemma lmeasure_weaken_aux (lmem lmt: LMem) (la : list Addr) (v : Version) :
-    lmem ⊆ lmt →
-    Forall (fun a => is_Some (lmem !! (a, v))) la →
-    lmemory_get_instrs lmem la v = lmemory_get_instrs lmt la v.
-  Proof.
-    intros Hincl Hall.
-    induction la ; first done.
-    rewrite Forall_cons in Hall. destruct Hall as [ [w Ha] Hall].
-    apply IHla in Hall.
-    assert (lmt !! (a, v) = Some w) as Ha' by (eapply lookup_weaken in Ha ; eauto).
-    cbn.
-    rewrite -/(lmemory_get_instrs lmem la v) -/(lmemory_get_instrs lmt la v).
-    by rewrite Ha Ha' Hall.
-  Qed.
-
-  Lemma lmeasure_weaken {lmem lmt} {b e v} :
-    lmem ⊆ lmt →
-    Forall (fun a => is_Some (lmem !! (a, v))) (finz.seq_between b e) →
-    hash_lmemory_range lmem b e v = hash_lmemory_range lmt b e v.
-  Proof.
-    intros Hincl Hall.
-    rewrite /hash_lmemory_range.
-    erewrite lmeasure_weaken_aux; eauto.
-  Qed.
-
-  Lemma sweep_implies_no_pc {σ p pc_b pc_e pc_a r a v} b e :
-    reg σ !! PC = Some (WCap p pc_b pc_e pc_a)
-    → reg σ !! r = Some (WCap RX b e a)
-    → sweep_reg (mem σ) (reg σ) r = true
-    → r ≠ PC
-    -> pc_a ∈ finz.seq_between pc_b pc_e
-    → pc_a ∉ finz.seq_between b e.
-  Proof.
-    intros Hpc Hr Hsweep Hinbouds pcHrpc.
-    unfold sweep_reg, sweep_memory_reg, sweep_registers_reg in Hsweep.
-    rewrite Hr in Hsweep.
-    rewrite andb_true_iff in Hsweep.
-    destruct Hsweep as [_ Hsweep].
-    unfold unique_in_registers in *.
-    rewrite bool_decide_eq_true in Hsweep.
-    rewrite map_Forall_lookup in Hsweep.
-    eapply Hsweep in Hpc.
-    destruct (decide (PC = r)); eauto.
-    apply overlap_word_disjoint in Hpc.
-    intro Hpca.
-    eapply elem_of_disjoint; eauto.
-  Qed.
-
-  Lemma update_version_region_insert (a : Addr) (la : list Addr) (v v' : Version) (lw : LWord) (glmem llmem : LMem ) :
-    a ∉ la ->
-    (<[(a, v):= lw]> (update_version_region glmem la v' llmem)) =
-    (update_version_region (<[(a, v):= lw]> glmem) la v' (<[(a, v):= lw]> llmem)).
-  Proof.
-    revert a v v' lw glmem llmem.
-    induction la; intros a' v v' lw glmem llmem Ha'; first set_solver.
-    cbn.
-    rewrite -/(update_version_region glmem la v' llmem).
-    rewrite -/(update_version_region (<[(a', v):=lw]> glmem) la v' (<[(a', v):=lw]> llmem)).
-    rewrite /update_version_addr.
-    rewrite lookup_insert_ne; last (intro; simplify_eq; set_solver).
-    destruct ( glmem !! (a, v') ) eqn:Ha_glmem; rewrite Ha_glmem.
-    - rewrite insert_commute; last (intro; simplify_eq; set_solver).
-      rewrite IHla; set_solver.
-    - rewrite IHla; set_solver.
-  Qed.
-
   Definition exec_optL_EInit {A}
     (lregs : LReg) (lmem : LMem)
     (r1 r2 :  RegName) (code_sweep data_sweep : bool)