diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 1d0498b06b3faafcd281e20b26c1cdd38b488836..56de7e0a24738cc352901c8e5f2cb63ebc1f61db 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-10-16.2.5e58df61") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-11-06.5.4cfd3db8") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl/base_logic/base_lifting.v b/gpfsl/base_logic/base_lifting.v
index 1d837685337ca06ede892c502ce0990a7829c211..e65025c976001e27a881853e60f3b413045224cf 100644
--- a/gpfsl/base_logic/base_lifting.v
+++ b/gpfsl/base_logic/base_lifting.v
@@ -7,7 +7,7 @@ From gpfsl.base_logic Require Export history vprop na meta_data.
 
 Require Import iris.prelude.options.
 
-Local Hint Constructors head_step bin_op_eval un_op_eval lit_eq lit_neq : core.
+Local Hint Constructors base_step bin_op_eval un_op_eval lit_eq lit_neq : core.
 
 Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
   as_rec : e = Rec f xl erec.
@@ -43,10 +43,10 @@ Local Ltac solve_exec_safe :=
   intros; destruct_and?; subst; eexists _, _, []; do 2 econstructor;
   simpl; eauto with lia.
 Local Ltac solve_exec_puredet :=
-  simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval;
+  simpl; intros; destruct_and?; inv_base_step; inv_bin_op_eval;
   inv_un_op_eval; inv_lit; done.
 Local Ltac solve_pure_exec :=
-  intros ?; apply nsteps_once, pure_head_step_pure_step;
+  intros ?; apply nsteps_once, pure_base_step_pure_step;
     constructor; [ solve_exec_safe | solve_exec_puredet ].
 
 Global Instance pure_rec e f xl erec erec' el 𝓥 :
@@ -123,13 +123,13 @@ Lemma iwp_alloc E n 𝓥:
       ∗ (l ↦∗ repeat #☠ (Z.to_nat n)
       ∗ [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l >> i) ⊤) 𝓥'.(cur) }}}.
 Proof.
-  iIntros (SUB ? Φ) ">Seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (SUB ? Φ) ">Seen HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs ?) "Hσ".
   iMod (hist_interp_seen_wf _ _ _ SUB with "Hσ Seen") as "[Hσ [%WF %HC]]".
   iModIntro. iSplit; [iPureIntro|iNext].
-  - destruct (alloc_fresh_head_step n _ _ HC) as [σ2 [𝓥2 STEP]]; first done.
+  - destruct (alloc_fresh_base_step n _ _ HC) as [σ2 [𝓥2 STEP]]; first done.
     econstructor. do 3 eexists. exact STEP.
-  - iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     rename select (drf_post _ _ _ _ _) into DRFPost.
@@ -197,7 +197,7 @@ Lemma iwp_free E (n : Z) (l: loc) 𝓥 :
   {{{ 𝓥', RET #☠ at 𝓥'; ⌜𝓥 ⊑ 𝓥'⌝ ∗ seen 𝓥' }}}.
 Proof.
   iIntros (SUB ? Φ) "(>Seen & >Hmt & >Hf) HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs ?) "Hσ".
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
@@ -213,11 +213,11 @@ Proof.
   (* done accessing hist_ctx *)
   iModIntro. iSplit.
   - iPureIntro.
-    destruct (dealloc_head_step (Z.to_nat n) l σ1 𝓥) as [σ2 [𝓥2 STEP]];
+    destruct (dealloc_base_step (Z.to_nat n) l σ1 𝓥) as [σ2 [𝓥2 STEP]];
       [| | |exact EQD| |apply WF|exact HC|done|..
        |econstructor; eexists; exists σ2, []; rewrite Z2Nat.id // in STEP;
           exact STEP]; move => ??; by apply PRE.
-  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     rename select (drf_post _ _ _ _ _) into DRFPost.
@@ -236,16 +236,16 @@ Proof.
     iModIntro; iSplit; [done|]. iApply "HΦ". iFrame.
 Qed.
 
-Lemma read_head_reducible σ l q C o 𝓥:
+Lemma read_base_reducible σ l q C o 𝓥:
   alloc_local l C 𝓥.(cur) →
   (o = NonAtomic → σ.(na) !!aw l ⊑ 𝓥.(cur) !!aw l ∧ ∃ t m, C = {[t := m]}) →
-  seen 𝓥 -∗ hist_ctx σ -∗ hist l q%Qp C -∗ ⌜head_reducible (Read o #l at 𝓥)%E σ⌝.
+  seen 𝓥 -∗ hist_ctx σ -∗ hist l q%Qp C -∗ ⌜base_reducible (Read o #l at 𝓥)%E σ⌝.
 Proof.
   iIntros (ALLOC NASGL) "seen Hσ hist".
   iDestruct (hist_ctx_hist_allocated with "Hσ hist") as %MALLOC.
   iDestruct (hist_ctx_hist_cut with "Hσ hist") as %(Vc&LE&ta&Eqta&EqC&?&?&?&?).
   iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC). subst C.
-  destruct (read_head_step l o _ _ HC) as [σ2 [𝓥2 [v' STEP]]];
+  destruct (read_base_step l o _ _ HC) as [σ2 [𝓥2 [v' STEP]]];
     [apply WF|apply WF|exact MALLOC|done|..].
   - specialize (LE l). apply view_sqsubseteq in LE as [LE1 LE2].
       rewrite LE1 Eqta. by eapply alloc_local_cut.
@@ -279,7 +279,7 @@ Lemma iwp_read l q C rs ws o E Va 𝓥 :
               else ∀ Vna, na_local l rs Vna → na_local l (rs ∪ {[tr]}) (join Vna 𝓥'.(cur)))⌝ }}}.
 Proof.
   iIntros (ALLOC DRF NASGL SUB Φ) "(>seen & >hist & ana & Haw) HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; first auto.
+  iApply wp_lift_atomic_base_step_no_fork; first auto.
   iIntros (σ1 ? κ κs ?) "Hσ".
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
@@ -288,13 +288,13 @@ Proof.
     with "[Hσ Haw]" as %NA.
   { iIntros (?). subst o. simpl. iDestruct "Haw" as "(Haw & %)".
     by iDestruct (hist_ctx_atwrite_eq with "Hσ Haw") as %?. }
-  iDestruct (read_head_reducible _ _ _ _ o with "seen Hσ hist") as %?; [done|..].
+  iDestruct (read_base_reducible _ _ _ _ o with "seen Hσ hist") as %?; [done|..].
   { move => ISNA. specialize (NASGL ISNA). destruct (NA ISNA) as [ATL Eqws].
     split; [|done]. by rewrite Eqws. }
   iMod ("HClose" with "Hσ") as "Hσ".
   (* done accessing hist_ctx *)
   iModIntro; iSplit; [done|].
-  iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
   iDestruct (hist_ctx_read with "Hσ hist") as "#VS".
@@ -370,7 +370,7 @@ Proof.
   by iApply ("Post" with "[$s' $hist $at $FACT]").
 Qed.
 
-Lemma write_head_reducible l (v : val) o C rs ws σ 𝓥:
+Lemma write_base_reducible l (v : val) o C rs ws σ 𝓥:
   alloc_local l C 𝓥.(cur) →
   na_local l rs 𝓥.(cur) →
   (o = NonAtomic → ∃ t m, C = {[t := m]}) →
@@ -378,7 +378,7 @@ Lemma write_head_reducible l (v : val) o C rs ws σ 𝓥:
   (if decide (Relaxed ⊑ o) then True
    else ∃ rsa, atread l 1 rsa ∗
         ⌜atr_local l rsa 𝓥.(cur) ∧ atw_local l ws 𝓥.(cur)⌝) -∗
-  ⌜head_reducible (Write o #l v at 𝓥)%E σ⌝.
+  ⌜base_reducible (Write o #l v at 𝓥)%E σ⌝.
 Proof.
   iIntros (ALLOC NA NASGL) "seen Hσ hist na ag at".
   iDestruct (hist_ctx_hist_allocated with "Hσ hist") as %MALLOC.
@@ -394,7 +394,7 @@ Proof.
     iPureIntro. by do 2 eexists. }
   iPureIntro. subst C. have ALLOC2 := ALLOC.
   destruct ALLOC as [t' [m' [[Eqm' Le']%cell_cut_lookup_Some [_ SEEN]]]].
-  destruct (write_head_step l v v o σ 𝓥) as [σ2 [𝓥2 STEP]];
+  destruct (write_base_step l v v o σ 𝓥) as [σ2 [𝓥2 STEP]];
     [done|apply WF|exact MALLOC| |by rewrite to_of_val|..].
   - do 2 eexists. by rewrite memory_lookup_cell.
   - by rewrite Eqna.
@@ -429,19 +429,19 @@ Lemma iwp_write l (v: val) C Va rs ws o E 𝓥:
             ∧ write_helper 𝓥 o l t ∅ m.(mrel) 𝓥'⌝ }}}.
 Proof.
   iIntros (ALLOC NA AT NASGL SUB Φ) "(>seen & >hist & na & aw & ar) HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; first auto.
+  iApply wp_lift_atomic_base_step_no_fork; first auto.
   iIntros (σ1 ? κ κs ?) "Hσ".
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
   iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
   iDestruct (hist_ctx_hist_good with "Hσ hist") as %WFC.
   iDestruct (hist_ctx_write with "Hσ hist") as "#VS".
-  iDestruct (write_head_reducible with "seen Hσ hist na aw [ar]") as %?; [done..| |].
+  iDestruct (write_base_reducible with "seen Hσ hist na aw [ar]") as %?; [done..| |].
   { case_decide; [done|]. iDestruct "ar" as (rsa) "[? %]". iExists rsa. by iFrame. }
   iMod ("HClose" with "Hσ") as "Hσ".
   (* done accessing hist_ctx *)
   iModIntro. iSplit; [done|].
-  iIntros (v2 σ2 efs Hstep) "!> _"; inv_head_step.
+  iIntros (v2 σ2 efs Hstep) "!> _"; inv_base_step.
 
   rename select (drf_post _ _ _ _ _) into DRFPost.
   rename select (option positive) into ot.
@@ -530,14 +530,14 @@ Proof.
   etrans; [exact SL|]. apply view_sqsubseteq, LE.
 Qed.
 
-Lemma cas_head_reducible σ l q C rs vr (vw: val) orf or ow 𝓥
+Lemma cas_base_reducible σ l q C rs vr (vw: val) orf or ow 𝓥
   (ORF: Relaxed ⊑ orf) (OR: Relaxed ⊑ or) (OW: Relaxed ⊑ ow)
   (ALLOC: alloc_local l C 𝓥.(cur))
   (NA: na_local l rs 𝓥.(cur))
   (COMP: ∀ t m v, C !! t = Some m → 𝓥.(cur) !!w l ⊑ Some t →
                 memval_val_rel m.(mval) v → ∃ vl, v = #vl ∧ lit_comparable vr vl) :
   seen 𝓥 -∗ hist_ctx σ -∗ hist l q C -∗ naread l 1 rs
-  -∗ ⌜head_reducible (CAS #l #vr vw orf or ow at 𝓥)%E σ⌝.
+  -∗ ⌜base_reducible (CAS #l #vr vw orf or ow at 𝓥)%E σ⌝.
 Proof.
   iIntros "seen Hσ hist na".
   iDestruct (hist_ctx_hist_allocated with "Hσ hist") as %MALLOC.
@@ -545,7 +545,7 @@ Proof.
   iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
   iDestruct (hist_ctx_hist_good with "Hσ hist") as %GOOD.
   iDestruct (hist_ctx_naread_eq with "Hσ na") as %Eqna.
-  destruct (update_head_step l #vr vw vr vw orf or ow _ _ (global_wf_mem _ WF) HC)
+  destruct (update_base_step l #vr vw vr vw orf or ow _ _ (global_wf_mem _ WF) HC)
     as [σ2 [𝓥2 [b STEP]]]; [apply WF|exact MALLOC| | |by apply to_of_val|..];
     [done..|by rewrite Eqna| | | |].
   - specialize (LE l). apply view_sqsubseteq in LE as [LE1 LE2].
@@ -624,18 +624,18 @@ Lemma iwp_cas l vr vw orf or ow C q
   -∗ WP CAS #l #vr vw orf or ow at 𝓥 @ E {{ Φ }}.
 Proof.
   iIntros ">seen >hist ar na aw HΦ".
-  iApply wp_lift_atomic_head_step_no_fork_fupd; first auto.
+  iApply wp_lift_atomic_base_step_no_fork_fupd; first auto.
   iIntros (σ1 ? κ κs ?) "Hσ".
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
   iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
-  iDestruct (cas_head_reducible _ _ _ _ _ _ vw orf or
+  iDestruct (cas_base_reducible _ _ _ _ _ _ vw orf or
                 with "seen Hσ hist na") as %?; [done..|].
   iDestruct (hist_ctx_read with "Hσ hist") as "#VSR".
   iDestruct (hist_ctx_cas with "Hσ hist") as "#VSC".
   iMod ("HClose" with "Hσ") as "Hσ".
   (* done accessing hist_ctx *)
-  iModIntro. iSplit; [done|]. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  iModIntro. iSplit; [done|]. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
   - iClear "VSC".
     rename select (drf_post _ _ _ _ _) into DRFPost.
     rename select (option positive) into ot.
@@ -735,11 +735,11 @@ Lemma iwp_acq_fence E 𝓥 (SUB: ↑histN ⊆ E) :
     FenceAcq at 𝓥 @ E
   {{{ 𝓥', RET #☠ at 𝓥'; seen 𝓥' ∗ ⌜𝓥 ⊑ 𝓥' ∧ 𝓥'.(cur) = 𝓥'.(acq)⌝ }}}.
 Proof.
-  iIntros (Φ) ">seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) ">seen HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs ?) "Hσ !>". iSplit.
-  - iPureIntro. destruct (acq_fence_head_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
+  - iPureIntro. destruct (acq_fence_base_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
     econstructor. do 3 eexists. exact STEP.
-  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
@@ -768,11 +768,11 @@ Lemma iwp_rel_fence E 𝓥 (SUB: ↑histN ⊆ E) :
     FenceRel at 𝓥 @ E
   {{{ 𝓥', RET #☠ at 𝓥'; seen 𝓥' ∗ ⌜𝓥 ⊑ 𝓥' ∧ 𝓥'.(frel) = 𝓥'.(cur)⌝}}}.
 Proof.
-  iIntros (Φ) "seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "seen HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs ?) "Hσ !>". iSplit.
-  - iPureIntro. destruct (rel_fence_head_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
+  - iPureIntro. destruct (rel_fence_base_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
     econstructor. do 3 eexists. exact STEP.
-  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
@@ -801,11 +801,11 @@ Lemma iwp_sc_fence E 𝓥 𝓢 (SUB: ↑histN ⊆ E) :
   {{{ 𝓢' 𝓥', RET #☠ at 𝓥';
     seen 𝓥' ∗ sc_view 𝓢' ∗ ⌜𝓥 ⊑ 𝓥' ∧ ∃ 𝓢0, 𝓢 ⊑ 𝓢0 ∧ sc_fence_helper 𝓥 𝓢0 𝓥' 𝓢'⌝}}}.
 Proof.
-  iIntros (Φ) "[>seen >SC] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "[>seen >SC] HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs ?) "Hσ !>". iSplit.
-  - iPureIntro. destruct (sc_fence_head_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
+  - iPureIntro. destruct (sc_fence_base_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
     econstructor. do 3 eexists. exact STEP.
-  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
@@ -839,11 +839,11 @@ Lemma iwp_sc_fence' E 𝓥 (SUB: ↑histN ⊆ E) :
   {{{ 𝓢' 𝓥', RET #☠ at 𝓥';
     seen 𝓥' ∗ sc_view 𝓢' ∗ ⌜𝓥 ⊑ 𝓥' ∧ ∃ 𝓢0, sc_fence_helper 𝓥 𝓢0 𝓥' 𝓢'⌝}}}.
 Proof.
-  iIntros (Φ) "seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "seen HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
   iIntros (σ1 ? κ κs n) "Hσ !>". iSplit.
-  - iPureIntro. destruct (sc_fence_head_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
+  - iPureIntro. destruct (sc_fence_base_step σ1 𝓥) as [σ2 [𝓥2 STEP]].
     econstructor. do 3 eexists. exact STEP.
-  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+  - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index fe0238729f919772e1b9a14c304ce40841fc9767..f30638103dd9214daa9f1951439852d62bf2578f 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -80,7 +80,7 @@ Section definitions.
 
   (* Ghost history ownership *)
   Definition hist_def (l : loc) (q : Qp) (C : cell) : iProp Σ
-    := mapsto l (DfracOwn q) (Some C).
+    := pointsto l (DfracOwn q) (Some C).
   Definition hist_aux : seal (@hist_def). Proof. by eexists. Qed.
   Definition hist := unseal hist_aux.
   Definition hist_eq : @hist = @hist_def := seal_eq hist_aux.
@@ -332,20 +332,20 @@ Section hist.
     hist l p1 C1 ∗ hist l p2 C2 ⊢ ⌜C1 = C2⌝.
   Proof.
     rewrite hist_eq. iIntros "[h1 h2]".
-    iDestruct (mapsto_agree with "h1 h2") as %?. iPureIntro. by simplify_eq.
+    iDestruct (pointsto_agree with "h1 h2") as %?. iPureIntro. by simplify_eq.
   Qed.
 
   Lemma hist_combine l p1 p2 C1 C2:
     hist l p1 C1 ∗ hist l p2 C2 ⊢ hist l (p1 + p2) C1 ∗ ⌜ C1 = C2 ⌝.
   Proof.
     rewrite hist_eq. iIntros "[h1 h2]".
-    iDestruct (mapsto_combine with "h1 h2") as "[$ %]".
+    iDestruct (pointsto_combine with "h1 h2") as "[$ %]".
     iPureIntro. by simplify_eq.
   Qed.
 
   Lemma hist_frac_1 l p C:
     hist l p C ⊢ ⌜ ✓ p ⌝.
-  Proof. rewrite hist_eq /hist_def. iApply mapsto_valid. Qed.
+  Proof. rewrite hist_eq /hist_def. iApply pointsto_valid. Qed.
 
   (** Properties of freeable blocks *)
   Global Instance hist_freeable_timeless q l n : Timeless (†{q}l…n).
@@ -982,7 +982,7 @@ Section hist.
     ∗ ([∗ list] i ∈ seq 0 (Pos.to_nat n), ∃ rs, naread (l >> i) 1 rs)
     ==∗ ∃ Vc', ⌜𝓝' ⊑ Vc'⌝
         ∗ (gen_heap_interp (to_hist (mem_cut M' Vc'))
-        ∗ ([∗ list] i ∈ seq 0 (Pos.to_nat n), mapsto (l >> i) DfracDiscarded None))
+        ∗ ([∗ list] i ∈ seq 0 (Pos.to_nat n), pointsto (l >> i) DfracDiscarded None))
         ∗ (own hist_atread_name (● to_atr 𝓝')
           ∗ ([∗ list] i ∈ seq 0 (Pos.to_nat n), atread (l >> i) 1 ∅))
         ∗ (own hist_atwrite_name (● to_atw 𝓝')
@@ -1034,7 +1034,7 @@ Section hist.
       [|exact NEXT|done|].
     { move => ???. rewrite shift_nat_assoc. by apply DMES. }
     clear IH. rewrite Eqseq -fmap_S_seq. setoid_rewrite big_sepL_cons.
-    iAssert ([∗ list] i ∈ (S <$> seq 0 (length 𝑚s)), mapsto (l >> i) _ None)%I
+    iAssert ([∗ list] i ∈ (S <$> seq 0 (length 𝑚s)), pointsto (l >> i) _ None)%I
       with "[ownl]" as "$".
     { rewrite big_sepL_fmap big_sepL_mono; [done|] => ???.
       by rewrite shift_nat_assoc. }
@@ -1069,7 +1069,7 @@ Section hist.
         last by (rewrite EMP; apply cell_deallocated_singleton).
       rewrite EqLoc shift_0.
       iMod (gen_heap_update with "own1 hist") as "[$ hist]".
-      iApply (mapsto_persist with "hist").
+      iApply (pointsto_persist with "hist").
     - iDestruct (hist_ctx_atread_full with "[$oar $atr]") as %Eqrs.
       rewrite atread_eq -own_op. iApply (own_update_2 with "oar atr").
       apply auth_update. rewrite /= to_atr_insert EqLoc shift_0.
diff --git a/gpfsl/base_logic/weakestpre.v b/gpfsl/base_logic/weakestpre.v
index 52f19dc32c84148234d6546907012c19133b1aa0..f1769aacb54288d0ca76c4da82cc73575b71c646 100644
--- a/gpfsl/base_logic/weakestpre.v
+++ b/gpfsl/base_logic/weakestpre.v
@@ -20,15 +20,15 @@ Section base_prop.
 Context `{!noprolG Σ}.
 Implicit Type (Φ : val → vProp Σ).
 
-Lemma hist_head_step_seen e e' efs 𝓥 𝓥' σ σ' κs
+Lemma hist_base_step_seen e e' efs 𝓥 𝓥' σ σ' κs
   (IN: 𝓥 ∈ σ.(mem)) (WF: Wf σ):
-  nopro_lang.head_step (e at 𝓥)%E σ κs (e' at 𝓥')%E σ' efs →
+  nopro_lang.base_step (e at 𝓥)%E σ κs (e' at 𝓥')%E σ' efs →
   hist_ctx σ' -∗ seen 𝓥 ==∗
   hist_ctx σ' ∗ seen 𝓥' ∗ ([∗ list] ef ∈ efs, seen ef.(nopro_lang.expr_view)).
 Proof.
-  iIntros (STEP) "ctx #s". inv_head_step.
+  iIntros (STEP) "ctx #s". inv_base_step.
   - iFrame "ctx #".
-    rename select (head_step _ _ _ _ _ _) into BaseStep.
+    rename select (base_step _ _ _ _ _ _) into BaseStep.
     destruct efs as [|?[]]; inversion BaseStep; subst=>//=.
     rename select (Forall _ _) into ForkViews.
     inversion ForkViews as [|? ? Eq1]. subst. rewrite -Eq1.
@@ -45,16 +45,16 @@ Proof.
     apply join_closed_view; [done|by apply INV'].
 Qed.
 
-Lemma hist_interp_head_step_seen
+Lemma hist_interp_base_step_seen
   e e' efs 𝓥 𝓥' σ σ' κs E
   (IN: 𝓥 ∈ σ.(mem)) (WF: Wf σ) (SUB: ↑histN ⊆ E) :
-  nopro_lang.head_step (e at 𝓥)%E σ κs (e' at 𝓥')%E σ' efs →
+  nopro_lang.base_step (e at 𝓥)%E σ κs (e' at 𝓥')%E σ' efs →
   hist_interp σ' -∗ seen 𝓥 ={E}=∗
   hist_interp σ' ∗ seen 𝓥' ∗ ([∗ list] ef ∈ efs, seen ef.(nopro_lang.expr_view)).
 Proof.
   iIntros (STEP) "Hσ' Hs".
   iMod (hist_interp_open _ _ SUB with "Hσ'") as "[Hσ' HClose]".
-  iMod (hist_head_step_seen _ _ _ _ _ _ _ _ IN WF STEP with "Hσ' Hs")
+  iMod (hist_base_step_seen _ _ _ _ _ _ _ _ IN WF STEP with "Hσ' Hs")
     as "(Hσ' & $ & $)".
   by iMod ("HClose" with "Hσ'") as "$".
 Qed.
@@ -74,7 +74,7 @@ Proof.
   iModIntro. iSpecialize ("IH" $! _ _ with "WP").
   iApply (wp_wand with "IH"); [done..|]. iIntros (?) "(% & $)". iPureIntro.
   etrans.
-  + apply (nopro_lang.head_step_tview_sqsubseteq _ _ _ _ _ _ _ _ STEP). + done.
+  + apply (nopro_lang.base_step_tview_sqsubseteq _ _ _ _ _ _ _ _ STEP). + done.
 Qed.
 
 Lemma wp_larger_view_post_inv E e (Φ: nopro_lang.val → iProp Σ) 𝓥 :
@@ -94,7 +94,7 @@ Proof.
   iApply "IH". iApply (wp_wand with "WP").
   iIntros (?) "HV". iIntros (Le). iApply "HV". iPureIntro.
   etrans; last exact Le.
-  by apply (nopro_lang.head_step_tview_sqsubseteq _ _ _ _ _ _ _ _ STEP).
+  by apply (nopro_lang.base_step_tview_sqsubseteq _ _ _ _ _ _ _ _ STEP).
 Qed.
 
 Lemma wp_seen_post E e (Φ: nopro_lang.val → iProp Σ) 𝓥 (SUB: ↑histN ⊆ E) :
@@ -112,7 +112,7 @@ Proof.
   iMod ("WP" $! e' σ' efs with "[%] [$]") as "WP". { by econstructor. }
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "(Hσ' & WP & $)".
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. subst.
-  iMod (hist_interp_head_step_seen _ _ _ _ _ _ _ _ _ INV WFm SUB STEP with "Hσ' Hs")
+  iMod (hist_interp_base_step_seen _ _ _ _ _ _ _ _ _ INV WFm SUB STEP with "Hσ' Hs")
     as "($ & #Hs' & _)".
   by iApply "IH".
 Qed.
@@ -133,7 +133,7 @@ Proof.
   iMod ("WP" $! e' σ' efs with "[%] [$]") as "WP". { by econstructor. }
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "(Hσ' & WP & $)".
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. subst.
-  iMod (hist_interp_head_step_seen _ _ _ _ _ _ _ _ _ INV WFm SUB STEP with "Hσ' Hs")
+  iMod (hist_interp_base_step_seen _ _ _ _ _ _ _ _ _ INV WFm SUB STEP with "Hσ' Hs")
     as "($ & #Hs' & _)".
   by iApply ("IH" with "Hs' WP").
 Qed.
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index e4117d0e3251c65389aadd05a1d08acde9e74831..ec4dfeaceef6c8899099e4b6239fc3035e1b04cd 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -291,60 +291,60 @@ Module base.
   | memval_val_VVal v : memval_val_rel (VVal v) v
   | memval_val_AVal : memval_val_rel AVal (LitV LitPoison).
 
-  Inductive head_step M 𝓥 : expr → option event → expr → list expr → Prop :=
+  Inductive base_step M 𝓥 : expr → option event → expr → list expr → Prop :=
   | BetaS f xl e e' el:
       Forall (λ ei, is_Some (to_val ei)) el →
       Closed (f :b: xl +b+ []) e →
       subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
-      head_step M 𝓥 (App (Rec f xl e) el)
+      base_step M 𝓥 (App (Rec f xl e) el)
                   None
                   e'
                   []
   | UnOpS op l l' :
       un_op_eval op l l' →
-      head_step M 𝓥 (UnOp op (Lit l))
+      base_step M 𝓥 (UnOp op (Lit l))
                   None
                   (Lit l')
                   []
   | BinOpS op l1 l2 l' :
       bin_op_eval M op l1 l2 l' →
-      head_step M 𝓥 (BinOp op (Lit l1) (Lit l2))
+      base_step M 𝓥 (BinOp op (Lit l1) (Lit l2))
                   None
                   (Lit l')
                   []
   | CaseS i el e :
       0 ≤ i →
       el !! (Z.to_nat i) = Some e →
-      head_step M 𝓥 (Case (Lit $ LitInt i) el)
+      base_step M 𝓥 (Case (Lit $ LitInt i) el)
                   None
                   e
                   []
   | ForkS e :
-      head_step M 𝓥 (Fork e)
+      base_step M 𝓥 (Fork e)
                   None
                   (Lit LitPoison)
                   [e]
   | AllocS n l:
       0 < n →
-      head_step M 𝓥 (Alloc $ Lit $ LitInt n)
+      base_step M 𝓥 (Alloc $ Lit $ LitInt n)
                   (Some $ event.Alloc l (Z.to_pos n))
                   (Lit $ LitLoc l)
                   []
   | FreeS n (l : loc) :
       0 < n →
-      head_step M 𝓥 (Free (Lit $ LitInt n) (Lit $ LitLoc l))
+      base_step M 𝓥 (Free (Lit $ LitInt n) (Lit $ LitLoc l))
                   (Some $ Dealloc l (Z.to_pos n))
                   (Lit LitPoison)
                   []
   | ReadS (l : loc) (v: value.val) vr o :
       memval_val_rel v vr →
-      head_step M 𝓥 (Read o (Lit $ LitLoc l))
+      base_step M 𝓥 (Read o (Lit $ LitLoc l))
                   (Some $ event.Read l v o)
                   (of_val vr)
                   []
   | WriteS (l : loc) e v o :
       to_val e = Some v →
-      head_step M 𝓥 (Write o (Lit $ LitLoc l) e)
+      base_step M 𝓥 (Write o (Lit $ LitLoc l) e)
                   (Some $ event.Write l v o)
                   (Lit LitPoison)
                   []
@@ -363,7 +363,7 @@ Module base.
       (* all readable values must be comparable *)
       (∀ t m, M !! (l,t) = Some m → 𝓥.(cur) !!w l ⊑ Some t
           → ∃ v, memval_val_rel m.(mval) (LitV v) ∧ lit_comparable lit1 v) →
-      head_step M 𝓥 (CAS (Lit $ LitLoc l) e1 e2 orf or ow)
+      base_step M 𝓥 (CAS (Lit $ LitLoc l) e1 e2 orf or ow)
                   (Some $ event.Read l (VVal $ LitV lito) orf)
                   (Lit $ lit_of_bool false)
                   []
@@ -374,22 +374,22 @@ Module base.
       (* all readable values must be comparable *)
       (∀ t m, M !! (l,t) = Some m → 𝓥.(cur) !!w l ⊑ Some t
           → ∃ v, memval_val_rel m.(mval) (LitV v) ∧ lit_comparable lit1 v) →
-      head_step M 𝓥 (CAS (Lit $ LitLoc l) e1 e2 orf or ow)
+      base_step M 𝓥 (CAS (Lit $ LitLoc l) e1 e2 orf or ow)
                   (Some $ event.Update l (LitV lito) v2 or ow)
                   (Lit $ lit_of_bool true)
                   []
   | FAcqS :
-      head_step M 𝓥 (FenceAcq)
+      base_step M 𝓥 (FenceAcq)
                   (Some $ Fence AcqRel Relaxed)
                   (Lit LitPoison)
                   []
   | FRelS :
-      head_step M 𝓥 (FenceRel)
+      base_step M 𝓥 (FenceRel)
                   (Some $ Fence Relaxed AcqRel)
                   (Lit LitPoison)
                   []
   | FSCS :
-      head_step M 𝓥 (FenceSC)
+      base_step M 𝓥 (FenceSC)
                   (Some $ Fence SeqCst SeqCst)
                   (Lit LitPoison)
                   []
@@ -418,11 +418,11 @@ Module base.
   Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
   Lemma val_stuck M 𝓥 e1 evt e2 efs :
-    head_step M 𝓥 e1 evt e2 efs → to_val e1 = None.
+    base_step M 𝓥 e1 evt e2 efs → to_val e1 = None.
   Proof. destruct 1; naive_solver. Qed.
 
-  Lemma head_ctx_step_val M 𝓥 Ki e evt e2 efs :
-    head_step M 𝓥 (fill_item Ki e) evt e2 efs → is_Some (to_val e).
+  Lemma base_ctx_step_val M 𝓥 Ki e evt e2 efs :
+    base_step M 𝓥 (fill_item Ki e) evt e2 efs → is_Some (to_val e).
   Proof.
     destruct Ki; inversion_clear 1; decompose_Forall_hyps;
     simplify_option_eq; by eauto.
@@ -744,26 +744,26 @@ Module nopro_lang.
   Lemma forkView_subseteq 𝓥: forkView 𝓥 ⊑ 𝓥.
   Proof. rewrite /forkView; split; simpl; [done..|apply cur_acq]. Qed.
 
-  Inductive head_step :
+  Inductive base_step :
     expr → state → list Empty_set → expr → state → list expr → Prop :=
   | pure_step σ 𝓥 e e' efs
-      (BaseStep : base.head_step σ.(mem) 𝓥 e None e' (expr_expr <$> efs))
+      (BaseStep : base.base_step σ.(mem) 𝓥 e None e' (expr_expr <$> efs))
       (ForkViews : Forall (eq (forkView 𝓥)) (expr_view <$> efs))
-    : head_step (mkExpr e 𝓥) σ [] (mkExpr e' 𝓥) σ efs
+    : base_step (mkExpr e 𝓥) σ [] (mkExpr e' 𝓥) σ efs
   | impure_step σ 𝓥  𝓝' 𝓥' M' 𝓢' ot 𝑚s e evt e' efs
       (NoFork : efs = [])
-      (ExprStep : base.head_step σ.(mem) 𝓥 e (Some evt) e' (expr_expr <$> efs))
+      (ExprStep : base.base_step σ.(mem) 𝓥 e (Some evt) e' (expr_expr <$> efs))
       (PStep : lbl_machine_step 𝓥 σ.(mem) σ.(sc) evt ot 𝑚s 𝓥' M' 𝓢')
       (DRFPost: drf_post σ.(na) evt ot 𝑚s 𝓝')
       (DRFPre: ∀ evt2 e2 efs2 ot2 𝑚s2 𝓥2 M2 𝓢2,
-          base.head_step σ.(mem) 𝓥 e (Some evt2) e2 (expr_expr <$> efs2) →
+          base.base_step σ.(mem) 𝓥 e (Some evt2) e2 (expr_expr <$> efs2) →
           lbl_machine_step 𝓥 σ.(mem) σ.(sc) evt2 ot2 𝑚s2 𝓥2 M2 𝓢2 →
           drf_pre σ.(na) 𝓥 σ.(mem) evt2)
-    : head_step (mkExpr e 𝓥) σ [] (mkExpr e' 𝓥') (mkGB 𝓢' 𝓝' M') efs.
-  Arguments head_step _%E _ _ _%E _ _%E.
+    : base_step (mkExpr e 𝓥) σ [] (mkExpr e' 𝓥') (mkGB 𝓢' 𝓝' M') efs.
+  Arguments base_step _%E _ _ _%E _ _%E.
 
-  Lemma head_step_tview_sqsubseteq e 𝓥 σ κs e' 𝓥' σ' ef
-    (STEP: head_step (mkExpr e 𝓥) σ κs (mkExpr e' 𝓥') σ' ef) :
+  Lemma base_step_tview_sqsubseteq e 𝓥 σ κs e' 𝓥' σ' ef
+    (STEP: base_step (mkExpr e 𝓥) σ κs (mkExpr e' 𝓥') σ' ef) :
     𝓥 ⊑ 𝓥'.
   Proof.
     inversion STEP ; first done. subst. by eapply machine_step_tview_sqsubseteq.
@@ -807,18 +807,18 @@ Module nopro_lang.
   Proof. move/fmap_is_Some/fill_item_val => H. exact/fmap_is_Some. Qed.
 
   Lemma val_stuck σ1 e1 κs σ2 e2 ef :
-    head_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
+    base_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
   Proof.
     inversion 1; subst;
-      last destruct select (base.head_step _ _ _ _ _ _);
+      last destruct select (base.base_step _ _ _ _ _ _);
       first (cbv -[base.to_val]; by erewrite val_stuck; last eassumption);
       reflexivity.
   Qed.
 
-  Lemma head_ctx_step_val Ki e σ κs e2 σ2 ef :
-    head_step (fill_item Ki e) σ κs e2 σ2 ef → is_Some (to_val e).
+  Lemma base_ctx_step_val Ki e σ κs e2 σ2 ef :
+    base_step (fill_item Ki e) σ κs e2 σ2 ef → is_Some (to_val e).
   Proof.
-    inversion 1; subst; apply fmap_is_Some; exact: head_ctx_step_val.
+    inversion 1; subst; apply fmap_is_Some; exact: base_ctx_step_val.
   Qed.
 
   Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -832,10 +832,10 @@ Module nopro_lang.
   (** Closed expressions *)
 
   Lemma nopro_ectxi_lang_mixin :
-    EctxiLanguageMixin of_val to_val fill_item head_step.
+    EctxiLanguageMixin of_val to_val fill_item base_step.
   Proof.
     split; eauto using to_of_val, of_to_val, val_stuck, fill_item_val,
-      fill_item_no_val_inj, head_ctx_step_val with typeclass_instances.
+      fill_item_no_val_inj, base_ctx_step_val with typeclass_instances.
   Qed.
 End nopro_lang.
 
@@ -856,7 +856,7 @@ Proof.
   - intros σ κs [e' 𝓥'] σ' ef. cbn. move => STEP. apply/fmap_is_Some.
     destruct e=>//=; repeat (case_match; try done);
     inversion STEP;
-      lazymatch goal with [ X : head_step _ _ _ _ _ _ |- _] => inversion X end;
+      lazymatch goal with [ X : base_step _ _ _ _ _ _ |- _] => inversion X end;
       rewrite ?to_of_val; eauto.
   - apply ectxi_language_sub_redexes_are_values=> /= Ki [e' ?] Hfill.
     apply/fmap_is_Some. revert He. inversion Hfill as [Hfill']; subst; clear Hfill.
@@ -871,11 +871,11 @@ Qed.
 
 Section Progress.
   (** Lemmas for progress *)
-  Lemma alloc_fresh_head_step n σ 𝓥
+  Lemma alloc_fresh_base_step n σ 𝓥
     (CLOSED: 𝓥 ∈ σ.(mem)):
     let l := (fresh_block σ.(mem), 0) in
     0 < n →
-    ∃ σ' 𝓥', nopro_lang.head_step (mkExpr (Alloc $ Lit n) 𝓥) σ []
+    ∃ σ' 𝓥', nopro_lang.base_step (mkExpr (Alloc $ Lit n) 𝓥) σ []
                                   (mkExpr (Lit $ LitLoc l) 𝓥') σ' [].
   Proof.
     intros l Hn.
@@ -887,7 +887,7 @@ Section Progress.
     inversion STEP'. constructor.
   Qed.
 
-  Lemma dealloc_head_step (n: nat) (l: loc) σ 𝓥
+  Lemma dealloc_base_step (n: nat) (l: loc) σ 𝓥
     (NEMP: ∀ n', (n' < n)%nat → σ.(mem) !!c (l >> n') ≠ ∅)
     (NAR: ∀ n', (n' < n)%nat
             → σ.(na) !! (l >> n') ⊑ 𝓥.(cur) !! (l >> n'))
@@ -899,7 +899,7 @@ Section Progress.
     (AINV: alloc_inv σ.(mem)) (CLOSED: 𝓥 ∈ σ.(mem)) :
     (0 < n)%nat →
     ∃ σ' 𝓥',
-    nopro_lang.head_step (mkExpr (Free (Lit n) (Lit l)) 𝓥) σ []
+    nopro_lang.base_step (mkExpr (Free (Lit n) (Lit l)) 𝓥) σ []
                          (mkExpr (Lit LitPoison) 𝓥') σ' [].
   Proof.
     move => /Nat.neq_0_lt_0 Lt0.
@@ -918,7 +918,7 @@ Section Progress.
   Qed.
 
   (* Reading doesn't need initialization, thus can return poison *)
-  Lemma read_head_step l o σ 𝓥
+  Lemma read_base_step l o σ 𝓥
     (CLOSED: 𝓥 ∈ σ.(mem)) (WFM: Wf σ.(mem))
     (AINV: alloc_inv σ.(mem)) (ALLOC: allocated l σ.(mem))
     (NE: σ.(mem) !!c l ≠ ∅) :
@@ -929,7 +929,7 @@ Section Progress.
       (∀ 𝑚', 𝑚' ∈ σ.(mem) → mloc 𝑚' = l → Some (mto 𝑚') ⊑ ot !!w l) ∧
       σ.(na) !!aw l ⊑ 𝓥.(cur) !!aw l) →
     ∃ σ' 𝓥' v,
-      nopro_lang.head_step (mkExpr (Read o (Lit $ LitLoc l)) 𝓥) σ []
+      nopro_lang.base_step (mkExpr (Read o (Lit $ LitLoc l)) 𝓥) σ []
                            (nopro_lang.of_val (mkVal v 𝓥')) σ' [].
   Proof.
     move => otl NA RNA.
@@ -948,7 +948,7 @@ Section Progress.
       inversion STEP'. by constructor.
   Qed.
 
-  Lemma write_head_step l e v o σ 𝓥
+  Lemma write_base_step l e v o σ 𝓥
     (CLOSED: 𝓥 ∈ σ.(mem))
     (AINV: alloc_inv σ.(mem))
     (ALLOC: allocated l σ.(mem))
@@ -963,7 +963,7 @@ Section Progress.
        σ.(na) !!aw l ⊑ ot !!aw l ∧
        σ.(na) !!ar l ⊑ ot !!ar l) →
     ∃ σ' 𝓥',
-      nopro_lang.head_step (mkExpr (Write o (base .Lit $ LitLoc l) e) 𝓥) σ []
+      nopro_lang.base_step (mkExpr (Write o (base .Lit $ LitLoc l) e) 𝓥) σ []
                            (mkExpr (Lit LitPoison) 𝓥') σ' [].
   Proof.
     move => otl NAR NA NAW.
@@ -977,7 +977,7 @@ Section Progress.
   Qed.
 
   (* Update requires allocated and non-UB for all possible comparisons *)
-  Lemma update_head_step l er ew vr (vw: val) orf or ow σ 𝓥
+  Lemma update_base_step l er ew vr (vw: val) orf or ow σ 𝓥
     (WFM: Wf σ.(mem)) (CLOSED: 𝓥 ∈ σ.(mem))
     (AINV: alloc_inv σ.(mem))
     (ALLOC: allocated l σ.(mem)) (NE: σ.(mem) !!c l ≠ ∅)
@@ -995,7 +995,7 @@ Section Progress.
     (∀ (t: time) (m: baseMessage), σ.(mem) !! (l,t) = Some m → ot !!w l ⊑ Some t
       → ∃ v, memval_val_rel m.(mval) (LitV v) ∧ lit_comparable vr v) →
     ∃ σ' 𝓥' b,
-      nopro_lang.head_step (mkExpr (CAS (Lit $ LitLoc l) er ew orf or ow) 𝓥) σ []
+      nopro_lang.base_step (mkExpr (CAS (Lit $ LitLoc l) er ew orf or ow) 𝓥) σ []
                            (mkExpr (Lit b) 𝓥') σ' [].
   Proof.
     move => NAR ot NA INIT NUB.
@@ -1045,8 +1045,8 @@ Section Progress.
           by constructor.
   Qed.
 
-  Lemma acq_fence_head_step σ 𝓥 :
-    ∃ σ' 𝓥', nopro_lang.head_step (mkExpr FenceAcq 𝓥) σ []
+  Lemma acq_fence_base_step σ 𝓥 :
+    ∃ σ' 𝓥', nopro_lang.base_step (mkExpr FenceAcq 𝓥) σ []
                                   (mkExpr (Lit LitPoison) 𝓥') σ' [].
   Proof.
     do 2 eexists. econstructor 2;
@@ -1054,8 +1054,8 @@ Section Progress.
     move => ???????? STEP _. inversion STEP. constructor.
   Qed.
 
-  Lemma rel_fence_head_step σ 𝓥 :
-    ∃ σ' 𝓥', nopro_lang.head_step (mkExpr FenceRel 𝓥) σ []
+  Lemma rel_fence_base_step σ 𝓥 :
+    ∃ σ' 𝓥', nopro_lang.base_step (mkExpr FenceRel 𝓥) σ []
                                   (mkExpr (Lit LitPoison) 𝓥') σ' [].
   Proof.
     do 2 eexists. econstructor 2;
@@ -1063,8 +1063,8 @@ Section Progress.
     move => ???????? STEP _. inversion STEP. constructor.
   Qed.
 
-  Lemma sc_fence_head_step σ 𝓥 :
-    ∃ σ' 𝓥', nopro_lang.head_step (mkExpr FenceSC 𝓥) σ []
+  Lemma sc_fence_base_step σ 𝓥 :
+    ∃ σ' 𝓥', nopro_lang.base_step (mkExpr FenceSC 𝓥) σ []
                                   (mkExpr (Lit LitPoison) 𝓥') σ' [].
   Proof.
     do 2 eexists. econstructor 2;
@@ -1072,8 +1072,8 @@ Section Progress.
     move => ???????? STEP _. inversion STEP. constructor.
   Qed.
 
-  Lemma fork_head_step e σ 𝓥:
-    ∃ σ' 𝓥', nopro_lang.head_step (mkExpr (Fork e) 𝓥) σ []
+  Lemma fork_base_step e σ 𝓥:
+    ∃ σ' 𝓥', nopro_lang.base_step (mkExpr (Fork e) 𝓥) σ []
                                   (mkExpr (Lit LitPoison) 𝓥) σ' [mkExpr e 𝓥'].
   Proof. by repeat econstructor. Qed.
 End Progress.
diff --git a/gpfsl/lang/tactics.v b/gpfsl/lang/tactics.v
index 5139a7ab5734ca40960452fc0a095e850ed85107..22d6a12cb1c570efeb6eaf5578a79fa9df312bd5 100644
--- a/gpfsl/lang/tactics.v
+++ b/gpfsl/lang/tactics.v
@@ -276,17 +276,17 @@ Ltac reshape_expr e tac :=
   end
   in go (@nil ectx_item) e.
 
-Ltac inv_head_step :=
+Ltac inv_base_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
   | H : _ = of_val ?v |- _ =>
      is_var v; destruct v; first[discriminate H|injection H as H]
-  | H : head_step _ _ ?e _ _ _ |- _ =>
+  | H : base_step _ _ ?e _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
      inversion H ; subst; clear H
-  | H : nopro_lang.head_step ?e _ _ _ _ _ |- _ =>
+  | H : nopro_lang.base_step ?e _ _ _ _ _ |- _ =>
      try (is_var e; fail 1);
      inversion H ; subst; clear H
   | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H; subst
diff --git a/gpfsl/logic/lifting.v b/gpfsl/logic/lifting.v
index c66927ae3e3b87011e58275d8d9c92c93c68d813..b62215c9e4e6783c5439c00470edef8abc727a63 100644
--- a/gpfsl/logic/lifting.v
+++ b/gpfsl/logic/lifting.v
@@ -53,13 +53,13 @@ Lemma wp_fork tid e E (SUB: ↑histN ⊆ E) :
 Proof.
   rewrite wp_eq /wp_def /=. iStartProof (iProp _). iIntros (Φ V).
   iIntros "WP" (??) "HΦ". iIntros (𝓥 ?) "H𝓥 #s".
-  iApply wp_lift_atomic_head_step; eauto.
+  iApply wp_lift_atomic_base_step; eauto.
   iIntros (σ1 ????) "Hσ !>". iSplit.
-  - iPureIntro. destruct (fork_head_step e σ1 𝓥) as [σ2 [𝓥2 STEP]].
+  - iPureIntro. destruct (fork_base_step e σ1 𝓥) as [σ2 [𝓥2 STEP]].
     econstructor. do 3 eexists. exact STEP.
   - iNext. iSpecialize ("HΦ" with "[]"); first done.
     iMod (hist_interp_seen_wf with "Hσ s") as "[Hσ [%WF %HC]]"; [done|].
-    iIntros (v2 σ2 efs Hstep) "_"; inv_head_step. iModIntro. iFrame. iSplit; [|done].
+    iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. iModIntro. iFrame. iSplit; [|done].
     iDestruct (seen_mono _ _ (nopro_lang.forkView_subseteq _) with "s") as "s'".
     iMod (own_alloc (● to_latT (nopro_lang.forkView 𝓥))) as (tid') "H𝓥'";
       [by apply auth_auth_valid|].
@@ -284,7 +284,7 @@ Proof.
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. clear He1'. subst.
   have Eq: e_ = FenceRel ∧ K = [] by apply fill_base_constructor; [left|].
   destruct Eq. subst e_ K; simpl.
-  have Ext': 𝓥 ⊑ 𝓥2 by eapply nopro_lang.head_step_tview_sqsubseteq.
+  have Ext': 𝓥 ⊑ 𝓥2 by eapply nopro_lang.base_step_tview_sqsubseteq.
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "($ & WP & $)".
   iDestruct (wp_larger_view_post with "WP") as "WP".
   iModIntro. iApply iwp_fupd. iApply (iwp_wand with "WP").
@@ -294,7 +294,7 @@ Proof.
   iExists _. iFrame. rewrite view_at_unfold_2.
   assert (𝓥.(cur) ⊑ 𝓥3.(frel)); [|by iFrame].
   simpl in Ext3. rewrite Ext' -Ext3.
-  inv_head_step.
+  inv_base_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
   by destruct select (rel_fence_step _ _).
@@ -354,14 +354,14 @@ Proof.
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. clear He1'. subst.
   have Eq: e_ = FenceAcq ∧ K = [] by apply fill_base_constructor; [right;left|].
   destruct Eq. subst e_ K; simpl.
-  have Ext': 𝓥' ⊑ 𝓥2. { by eapply nopro_lang.head_step_tview_sqsubseteq. }
+  have Ext': 𝓥' ⊑ 𝓥2. { by eapply nopro_lang.base_step_tview_sqsubseteq. }
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "($ & WP & $)".
   iDestruct (wp_larger_view_post with "WP") as "WP".
   iModIntro. iApply (iwp_wand with "WP").
   iIntros ([v 𝓥3]) "/= (% & _ & $ & H)". iApply "H". rewrite view_at_unfold_2.
   assert (𝓥Acq.(acq) ⊑ 𝓥3.(cur)); [|by iFrame].
   rewrite H𝓥Acq.
-  inv_head_step.
+  inv_base_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
   destruct select (acq_fence_step _ _). subst.
@@ -409,7 +409,7 @@ Proof.
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. clear He1'. subst.
   have Eq: e_ = FenceSC ∧ K = [] by apply fill_base_constructor; [right;right|].
   destruct Eq. subst e_ K; simpl.
-  have Ext': 𝓥 ⊑ 𝓥2 by eapply nopro_lang.head_step_tview_sqsubseteq.
+  have Ext': 𝓥 ⊑ 𝓥2 by eapply nopro_lang.base_step_tview_sqsubseteq.
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "($ & WP & $)".
   iDestruct (wp_larger_view_post with "WP") as "WP".
   iModIntro. iApply iwp_fupd. iApply (iwp_wand with "WP").
@@ -419,7 +419,7 @@ Proof.
   iExists _. iFrame. rewrite view_at_unfold_2.
   assert (𝓥.(cur) ⊑ 𝓥3.(frel)); [|by iFrame].
   simpl in Ext3. rewrite Ext' -Ext3.
-  inv_head_step.
+  inv_base_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
   destruct select (sc_fence_step _ _ _ _).
@@ -467,7 +467,7 @@ Proof.
   rewrite /= -!fill_base_nopro in He1', He2'. inversion He1'. clear He1'. subst.
   have Eq: e_ = FenceSC ∧ K = [] by apply fill_base_constructor; [right;right|].
   destruct Eq. subst e_ K; simpl.
-  have Ext': 𝓥' ⊑ 𝓥2. { by eapply nopro_lang.head_step_tview_sqsubseteq. }
+  have Ext': 𝓥' ⊑ 𝓥2. { by eapply nopro_lang.base_step_tview_sqsubseteq. }
   iIntros "!> !>". iMod "WP". iModIntro. iMod "WP" as "($ & WP & $)".
   iDestruct (wp_larger_view_post with "WP") as "WP".
   iModIntro. iApply (iwp_wand with "WP").
@@ -475,7 +475,7 @@ Proof.
   rewrite view_at_unfold_2.
   assert (𝓥Acq.(acq) ⊑ 𝓥3.(cur)); [|by iFrame].
   simpl in Ext3. rewrite H𝓥Acq -Ext3.
-  inv_head_step.
+  inv_base_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
   destruct select (sc_fence_step _ _ _ _).
@@ -516,13 +516,13 @@ Proof.
   iIntros (Hl1 Hl2 Hpost). iStartProof (iProp _).
   iIntros (?) "HP". rewrite wp_eq /wp_def. iIntros (𝓥 ->) "H𝓥 _".
   destruct (bool_decide_reflect (l1 = l2)) as [->|].
-  - iApply wp_lift_pure_det_head_step_no_fork'; [done| | |].
+  - iApply wp_lift_pure_det_base_step_no_fork'; [done| | |].
     + repeat intro. eexists _, _, _, []; repeat constructor.
-    + intros. by inv_head_step; inv_bin_op_eval; inv_lit.
+    + intros. by inv_base_step; inv_bin_op_eval; inv_lit.
     + iPoseProof (Hpost with "HP") as "?".
       iIntros "!> _". iApply iwp_value. iFrame.
-  - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
-    iIntros (σ1 ? κ κs ?) "Hσ1 !>". inv_head_step.
+  - iApply wp_lift_atomic_base_step_no_fork; subst=>//.
+    iIntros (σ1 ? κ κs ?) "Hσ1 !>". inv_base_step.
     iSplitR.
     { iPureIntro. eexists _, _, _, []. constructor; [|by simpl].
       apply BinOpS, BinOpEqFalse. by constructor. }
@@ -535,7 +535,7 @@ Proof.
       + iExists _. by iApply Hl2.
       + by iApply Hpost. }
     clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "_".
-    inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+    inv_base_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
     + iMod (hist_interp_open with "Hσ1") as "[Hσ1 _]"; [done|].
       iExFalso. iDestruct "HP" as "[Hl1 _]".
       setoid_rewrite own_loc_own_loc_prim. setoid_rewrite own_loc_prim_hist.