diff --git a/CHANGELOG.md b/CHANGELOG.md
index d921a392e..3109c7ddd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,19 @@
 
 ## New features
 
+- The stack allocation checker accepts more programs. This checker is run
+  during the stack allocation pass to verify that the transformation done
+  by the pass (mostly, turning arrays accesses into memory accesses)
+  is correct. It ensures that there is no aliasing problem when two arrays
+  are put in the same place in memory. Before, an assignment `a1 = a2`, where
+  `a1` and `a2` are two arrays, was accepted only if there was no aliasing
+  issue on `a2`, and `a1` was marked as having no aliasing issue.
+  Now, there is no such requirement on `a2`, and `a1` is marked as having
+  the same aliasing issues as `a2`.
+  This gives in particular more freedom for spilling and unspilling reg ptr,
+  see `compiler/tests/success/subarrays/x86_64/spill_partial.jazz`.
+  ([PR #841](https://github.com/jasmin-lang/jasmin/pull/841)).
+
 - ARM now compiles `x = imm;` smartly: for small immediates, a single `MOV`; for
   immediates whose negation is small, a single `MVN`; and for large immediates
   a pair of `MOV` and `MOVT`.
diff --git a/compiler/tests/success/subarrays/x86-64/copy_partial.jazz b/compiler/tests/success/subarrays/x86-64/copy_partial.jazz
new file mode 100644
index 000000000..68f40a762
--- /dev/null
+++ b/compiler/tests/success/subarrays/x86-64/copy_partial.jazz
@@ -0,0 +1,22 @@
+export fn test () -> reg u64 {
+  stack u64[2] s;
+  reg ptr u64[2] r1 r2;
+
+  s[0] = 0;
+  s[1] = 1;
+
+  r1 = s;
+  r1[0] = 2;
+
+  r2 = s; // we copy s while it is not fully valid
+  r2[1] = 3;
+
+  s[0:1] = r1[0:1];
+  s[1:1] = r2[1:1];
+
+  reg u64 res;
+  res = s[0];
+  res += s[1];
+
+  return res;
+}
diff --git a/compiler/tests/success/subarrays/x86-64/spill_partial.jazz b/compiler/tests/success/subarrays/x86-64/spill_partial.jazz
new file mode 100644
index 000000000..35e4b1ff5
--- /dev/null
+++ b/compiler/tests/success/subarrays/x86-64/spill_partial.jazz
@@ -0,0 +1,19 @@
+fn f (reg ptr u64[2] r) -> reg ptr u64[2] {
+  r[0] = 1;
+  return r;
+}
+
+export fn test (reg ptr u64[4] r) -> reg ptr u64[4], reg u64 {
+  reg ptr u64[2] r2;
+
+  r2 = r[1:2];
+  () = #spill(r);
+  r2 = f(r2);
+  () = #unspill(r); // we unspill r, while it is not fully valid
+  r[1:2] = r2;
+
+  reg u64 res;
+  res = r[1];
+
+  return r, res;
+}
diff --git a/compiler/tests/success/subarrays/x86-64/swap_partial.jazz b/compiler/tests/success/subarrays/x86-64/swap_partial.jazz
new file mode 100644
index 000000000..b72963ff3
--- /dev/null
+++ b/compiler/tests/success/subarrays/x86-64/swap_partial.jazz
@@ -0,0 +1,25 @@
+export fn test () -> reg u64 {
+  stack u64[2] s;
+  reg ptr u64[2] r1 r2;
+
+  s[0] = 0;
+  s[1] = 1;
+
+  r1 = s;
+  r1[0] = 2;
+
+  r2 = s; // we copy s while it is not fully valid
+  r2[1] = 3;
+
+  // we swap two arrays that are both not full valid
+  (r1, r2) = #swap(r1, r2);
+
+  s[0:1] = r2[0:1];
+  s[1:1] = r1[1:1];
+
+  reg u64 res;
+  res = 0;
+  res += s[1];
+
+  return res;
+}
diff --git a/proofs/compiler/stack_alloc.v b/proofs/compiler/stack_alloc.v
index 7de924655..6f89f73d6 100644
--- a/proofs/compiler/stack_alloc.v
+++ b/proofs/compiler/stack_alloc.v
@@ -236,16 +236,20 @@ Definition sub_region_at_ofs sr ofs len :=
      sr_zone   := sub_zone_at_ofs sr.(sr_zone) ofs len
   |}.
 
-Definition check_valid (rmap:region_map) (x:var_i) ofs len :=
+Definition get_sub_region_bytes (rmap:region_map) (x:var_i) ofs len :=
   (* we get the bytes associated to variable [x] *)
   Let sr := get_sub_region rmap x in
   let bytes := get_var_bytes rmap sr.(sr_region) x in
   let sr' := sub_region_at_ofs sr ofs len in
   let isub_ofs := interval_of_zone sr'.(sr_zone) in
-  (* we check if [isub_ofs] is a subset of one of the intervals of [bytes] *)
-  Let _   := assert (ByteSet.mem bytes isub_ofs)
-                    (stk_error x (pp_box [:: pp_s "the region associated to variable"; pp_var x; pp_s "is partial"])) in
-  ok (sr, sr').
+  ok (sr, sr', ByteSet.inter bytes (ByteSet.full isub_ofs)).
+
+Definition check_valid x sr bytes :=
+  Let _ :=
+    assert (ByteSet.mem bytes (interval_of_zone sr.(sr_zone)))
+           (stk_error x (pp_box [:: pp_s "the region associated to variable"; pp_var x; pp_s "is partial"]))
+  in
+  ok tt.
 
 Definition clear_bytes i bytes := ByteSet.remove bytes i.
 (* TODO: check optim
@@ -329,18 +333,20 @@ Definition set_arr_word (rmap:region_map) al (x:var_i) ofs ws :=
 
 Definition set_arr_call rmap x sr := set_sub_region rmap x sr (Some 0)%Z (size_slot x).
 
-Definition set_move_bytes rv x sr :=
+Definition set_move_bytes rv x sr bytesy :=
   let bm := get_bytes_map sr.(sr_region) rv in
   let bytes := get_bytes x bm in
-  let bm := Mvar.set bm x (ByteSet.add (interval_of_zone sr.(sr_zone)) bytes) in
+  let bytes := ByteSet.remove bytes (interval_of_zone sr.(sr_zone)) in
+  let bytes := ByteSet.union bytes bytesy in
+  let bm := Mvar.set bm x bytes in
   Mr.set rv sr.(sr_region) bm.
 
-Definition set_move_sub (rmap:region_map) x sr :=
-  let rv := set_move_bytes rmap x sr in
+Definition set_move_sub (rmap:region_map) x sr bytes :=
+  let rv := set_move_bytes rmap x sr bytes in
   {| var_region := rmap.(var_region);
      region_var := rv |}.
 
-Definition set_arr_sub (rmap:region_map) (x:var_i) ofs len sr_from :=
+Definition set_arr_sub (rmap:region_map) (x:var_i) ofs len sr_from bytesy :=
   Let sr := get_sub_region rmap x in
   let sr' := sub_region_at_ofs sr (Some ofs) len in
   Let _ := assert (sr' == sr_from)
@@ -349,13 +355,13 @@ Definition set_arr_sub (rmap:region_map) (x:var_i) ofs len sr_from :=
                       pp_s "the assignment to sub-array"; pp_var x;
                       pp_s "cannot be turned into a nop: source and destination regions are not equal"]))
   in
-  ok (set_move_sub rmap x sr').
+  ok (set_move_sub rmap x sr' bytesy).
 
 (* identical to [set_sub_region], except clearing
    TODO: fusion with set_arr_sub ? not sure its worth
 *)
-Definition set_move (rmap:region_map) (x:var) sr :=
-  let rv := set_move_bytes rmap x sr in
+Definition set_move (rmap:region_map) (x:var) sr bytesy :=
+  let rv := set_move_bytes rmap x sr bytesy in
   {| var_region := Mvar.set rmap.(var_region) x sr;
      region_var := rv |}.
 
@@ -565,26 +571,20 @@ Definition check_vpk rmap (x:var_i) vpk ofs len :=
   match vpk with
   | VKglob (_, ws) =>
     let sr := sub_region_glob x ws in
-    ok (sr, sub_region_at_ofs sr ofs len)
+    let sr' := sub_region_at_ofs sr ofs len in
+    (* useless inter, but allows to state a uniform lemma *)
+    let bytes := ByteSet.inter (ByteSet.full (interval_of_zone sr.(sr_zone)))
+                               (ByteSet.full (interval_of_zone sr'.(sr_zone)))
+    in
+    ok (sr, sr', bytes)
   | VKptr _pk =>
-    check_valid rmap x ofs len
+    get_sub_region_bytes rmap x ofs len
   end.
 
-(* We could write [check_vpk] as follows.
-  Definition check_vpk' rmap (x : gvar) ofs len :=
-    let (sr, bytes) := check_gvalid rmap x in
-    let sr' := sub_region_at_ofs sr.(sr_zone) ofs len in
-    let isub_ofs := interval_of_zone sr'.(sr_zone) in
-    (* we check if [isub_ofs] is a subset of one of the intervals of [bytes] *)
-    (* useless test when [x] is glob, but factorizes call to [sub_region_at_ofs] *)
-    Let _   := assert (ByteSet.mem bytes isub_ofs)
-                      (Cerr_stk_alloc "check_valid: the region is partial") in
-    ok sr'.
-*)
-
 Definition check_vpk_word rmap al x vpk ofs ws :=
-  Let srs := check_vpk rmap x vpk ofs (wsize_size ws) in
-  check_align al x srs.1 ws.
+  Let: (sr, sr', bytes) := check_vpk rmap x vpk ofs (wsize_size ws) in
+  Let _ := check_valid x sr' bytes in
+  check_align al x sr ws.
 
 Fixpoint alloc_e (e:pexpr) :=
   match e with
@@ -715,11 +715,11 @@ Definition is_nop is_spilling rmap (x:var) (sry:sub_region) : bool :=
   else false.
 
 (* TODO: better error message *)
-Definition get_addr is_spilling rmap x dx tag sry vpk y ofs :=
+Definition get_addr is_spilling rmap x dx tag sry bytesy vpk y ofs :=
   let ir := if is_nop is_spilling rmap x sry
             then Some nop
             else sap_mov_ofs saparams dx tag vpk y ofs in
-  let rmap := Region.set_move rmap x sry in
+  let rmap := Region.set_move rmap x sry bytesy in
   (rmap, ir).
 
 Definition get_ofs_sub aa ws x e1 :=
@@ -791,13 +791,12 @@ Definition alloc_array_move rmap r tag e :=
     match vk with
     | None => Error (stk_ierror_basic vy "register array remains")
     | Some vpk =>
-      Let srs := check_vpk rmap vy vpk (Some ofs) len in
-      let sry := srs.2 in
+      Let: (_, sry, bytesy) := check_vpk rmap vy vpk (Some ofs) len in
       Let eofs := mk_addr_pexpr rmap vy vpk in
-      ok (sry, vpk, eofs.1, (eofs.2 + ofs)%Z)
+      ok (sry, vpk, bytesy, eofs.1, (eofs.2 + ofs)%Z)
     end
   in
-  let '(sry, vpk, ey, ofs) := sryl in
+  let '(sry, vpk, bytesy, ey, ofs) := sryl in
   match subx with
   | None =>
     match get_local (v_var x) with
@@ -813,11 +812,11 @@ Definition alloc_array_move rmap r tag e :=
                       pp_s "the assignment to array"; pp_var x;
                       pp_s "cannot be turned into a nop: source and destination regions are not equal"]))
         in
-        let rmap := Region.set_move rmap x sry in
+        let rmap := Region.set_move rmap x sry bytesy in
         ok (rmap, nop)
       | Pregptr p =>
         let (rmap, oir) :=
-            get_addr None rmap x (Lvar (with_var x p)) tag sry vpk ey ofs in
+            get_addr None rmap x (Lvar (with_var x p)) tag sry bytesy vpk ey ofs in
         match oir with
         | None =>
           let err_pp := pp_box [:: pp_s "cannot compute address"; pp_var x] in
@@ -829,7 +828,7 @@ Definition alloc_array_move rmap r tag e :=
         let is_spilling := Some (slot, ws, z, x') in
         let dx_ofs := cast_const (ofsx + z.(z_ofs)) in
         let dx := Lmem Aligned Uptr (with_var x pmap.(vrsp)) dx_ofs in
-        let (rmap, oir) := get_addr is_spilling rmap x dx tag sry vpk ey ofs in
+        let (rmap, oir) := get_addr is_spilling rmap x dx tag sry bytesy vpk ey ofs in
         match oir with
         | None =>
           let err_pp := pp_box [:: pp_s "cannot compute address"; pp_var x] in
@@ -843,7 +842,7 @@ Definition alloc_array_move rmap r tag e :=
     match get_local (v_var x) with
     | None   => Error (stk_ierror_basic x "register array remains")
     | Some _ =>
-      Let rmap := Region.set_arr_sub rmap x ofs len sry in
+      Let rmap := Region.set_arr_sub rmap x ofs len sry bytesy in
       ok (rmap, nop)
     end
   end.
@@ -880,13 +879,12 @@ Definition alloc_protect_ptr rmap ii r t e msf :=
                       (stk_error_no_var "argument of protect_ptr should be a reg ptr") in
       Let _ := assert (if r is Lvar _ then true else false)
                       (stk_error_no_var "destination of protect_ptr should be a reg ptr") in
-      Let srs := check_vpk rmap vy vpk (Some ofs) len in
-      let sry := srs.2 in
+      Let: (_, sry, bytesy) := check_vpk rmap vy vpk (Some ofs) len in
       Let: (e, _ofs) := mk_addr_pexpr rmap vy vpk in (* ofs is ensured to be 0 *)
-      ok (sry, vpk, e)
+      ok (sry, bytesy, vpk, e)
     end
   in
-  let '(sry, vpk, ey) := sryl in
+  let '(sry, bytesy, vpk, ey) := sryl in
   match subx with
   | None =>
     match get_local (v_var x) with
@@ -897,7 +895,7 @@ Definition alloc_protect_ptr rmap ii r t e msf :=
         let dx := Lvar (with_var x px) in
         Let msf := add_iinfo ii (alloc_e rmap msf) in
         Let ir := lower_protect_ptr_fail ii [::dx] t [:: ey; msf] in
-        let rmap := Region.set_move rmap x sry in
+        let rmap := Region.set_move rmap x sry bytesy in
         ok (rmap, ir)
       | _ => Error (stk_error_no_var "only reg ptr can receive the result of protect_ptr")
       end
@@ -932,7 +930,8 @@ Definition alloc_array_move_init rmap r tag e :=
         end
       end in
     let sr := sub_region_at_ofs sr (Some ofs) len in
-    let rmap := Region.set_move_sub rmap x sr in
+    let bytesy := ByteSet.full (interval_of_zone sr.(sr_zone)) in
+    let rmap := Region.set_move_sub rmap x sr bytesy in
     ok (rmap, nop )
   else alloc_array_move rmap r tag e.
 
@@ -1043,10 +1042,14 @@ Definition alloc_call_arg_aux rmap0 rmap (sao_param: option param_info) (e:pexpr
     ok (rmap, (None, Pvar x))
   | None, Some _ => Error (stk_ierror_basic xv "argument not a reg")
   | Some pi, Some (Pregptr p) =>
-    Let srs := Region.check_valid rmap0 xv (Some 0%Z) (size_slot xv) in
-    let sr := srs.1 in
-    Let rmap := if pi.(pp_writable) then set_clear rmap xv sr (Some 0%Z) (size_slot xv) else ok rmap in
+    Let: (sr, sr', bytes) := Region.get_sub_region_bytes rmap0 xv (Some 0%Z) (size_slot xv) in
+    Let _ := Region.check_valid xv sr' bytes in
     Let _  := check_align Aligned xv sr pi.(pp_align) in
+    Let rmap :=
+      if pi.(pp_writable) then
+        set_clear rmap xv sr (Some 0%Z) (size_slot xv)
+      else ok rmap
+    in
     ok (rmap, (Some (pi.(pp_writable),sr), Pvar (mk_lvar (with_var xv p))))
   | Some _, _ => Error (stk_ierror_basic xv "the argument should be a reg ptr")
   end.
@@ -1186,12 +1189,12 @@ Definition alloc_array_swap rmap rs t es :=
   | [:: Lvar x; Lvar y], [::Pvar z'; Pvar w'] =>
     let z := z'.(gv) in
     Let pz  := get_regptr z in
-    Let: (_, srz) := check_valid rmap z (Some 0%Z) (size_of z.(vtype)) in
+    Let: (_, srz, bytesz) := get_sub_region_bytes rmap z (Some 0%Z) (size_of z.(vtype)) in
     let w := w'.(gv) in
     Let pw := get_regptr w in
-    Let: (_, srw) := check_valid rmap w (Some 0%Z) (size_of w.(vtype)) in
-    let rmap := Region.set_move rmap x srw in
-    let rmap := Region.set_move rmap y srz in
+    Let: (_, srw, bytesw) := get_sub_region_bytes rmap w (Some 0%Z) (size_of w.(vtype)) in
+    let rmap := Region.set_move rmap x srw bytesw in
+    let rmap := Region.set_move rmap y srz bytesz in
     Let px := get_regptr x in
     Let py := get_regptr y in
     Let _ := assert ((is_lvar z') && (is_lvar w'))
@@ -1301,7 +1304,8 @@ Definition add_alloc globals stack (xpk:var * ptr_kind_init) (lrx: Mvar.t ptr_ki
             let rmap :=
               if sc is Slocal then
                 let sr := sub_region_stack x' ws' z in
-                Region.set_arr_init rmap x sr
+                let bytes := ByteSet.full (interval_of_zone sr.(sr_zone)) in
+                Region.set_arr_init rmap x sr bytes
               else
                 rmap
             in
@@ -1371,12 +1375,12 @@ Definition check_result pmap rmap paramsi params oi (x:var_i) :=
   match oi with
   | Some i =>
     match nth None paramsi i with
-    | Some sr =>
+    | Some sr_param =>
       Let _ := assert (x.(vtype) == (nth x params i).(vtype))
                       (stk_ierror_no_var "reg ptr in result not corresponding to a parameter") in
-      Let srs := check_valid rmap x (Some 0%Z) (size_slot x) in
-      let sr' := srs.1 in
-      Let _  := assert (sr == sr') (stk_ierror_no_var "invalid reg ptr in result") in
+      Let: (sr, sr', bytes) := get_sub_region_bytes rmap x (Some 0%Z) (size_slot x) in
+      Let _ := check_valid x sr' bytes in
+      Let _  := assert (sr_param == sr) (stk_ierror_no_var "invalid reg ptr in result") in
       Let p  := get_regptr pmap x in
       ok p
     | None => Error (stk_ierror_no_var "invalid function info")
@@ -1422,9 +1426,10 @@ Definition init_param (mglob stack : Mvar.t (Z * wsize)) accu pi (x:var_i) :=
       {| r_slot := x;
          r_align := pi.(pp_align); r_writable := pi.(pp_writable) |} in
     let sr := sub_region_full x r in
+    let bytes := ByteSet.full (interval_of_zone sr.(sr_zone)) in
     ok (Sv.add pi.(pp_ptr) disj,
         Mvar.set lmap x (Pregptr pi.(pp_ptr)),
-        set_move rmap x sr,
+        set_move rmap x sr bytes,
         (Some sr, with_var x pi.(pp_ptr)))
   end.
 
diff --git a/proofs/compiler/stack_alloc_proof.v b/proofs/compiler/stack_alloc_proof.v
index 29b625f05..b3899fc56 100644
--- a/proofs/compiler/stack_alloc_proof.v
+++ b/proofs/compiler/stack_alloc_proof.v
@@ -859,19 +859,24 @@ Section EXPR.
     by move=> ?; split => -[->].
   Qed.
 
-  Lemma check_validP (x : var_i) ofs len sr sr' :
-    check_valid rmap x ofs len = ok (sr, sr') ->
-    exists bytes, [/\
-      check_gvalid rmap (mk_lvar x) = Some (sr, bytes),
+  Lemma get_sub_region_bytesP (x : var_i) ofs len sr sr' bytes :
+    get_sub_region_bytes rmap x ofs len = ok (sr, sr', bytes) ->
+    exists bytesx, [/\
+      check_gvalid rmap (mk_lvar x) = Some (sr, bytesx),
       sr' = sub_region_at_ofs sr ofs len &
       let isub_ofs := interval_of_zone sr'.(sr_zone) in
-      ByteSet.mem bytes isub_ofs].
+      bytes = ByteSet.inter bytesx (ByteSet.full isub_ofs)].
   Proof.
-    rewrite /check_valid /check_gvalid.
-    t_xrbindP=> sr'' /get_sub_regionP -> hmem ? <-; subst sr''.
+    rewrite /get_sub_region_bytes /check_gvalid.
+    t_xrbindP=> _ /get_sub_regionP -> -> <- <- /=.
     by eexists.
   Qed.
 
+  Lemma check_validP (x : var_i) sr bytes tt :
+    check_valid x sr bytes = ok tt ->
+    ByteSet.mem bytes (interval_of_zone sr.(sr_zone)).
+  Proof. by rewrite /check_valid; t_xrbindP. Qed.
+
   Lemma sub_region_addr_glob x ofs ws :
     wf_global x ofs ws ->
     sub_region_addr (sub_region_glob x ws) = (rip + wrepr _ ofs)%R.
@@ -898,25 +903,22 @@ Section EXPR.
     wf_sub_region (sub_region_stkptr sl ws z) spointer.
   Proof. by case. Qed.
 
-  Lemma check_vpkP x vpk ofs len sr sr' :
+  Lemma check_vpkP x vpk ofs len sr sr' bytes :
     (forall zofs, ofs = Some zofs -> 0 <= zofs /\ zofs + len <= size_slot x.(gv)) ->
     get_var_kind pmap x = ok (Some vpk) ->
-    check_vpk rmap x.(gv) vpk ofs len = ok (sr, sr') ->
-    exists bytes,
-      [/\ check_gvalid rmap x = Some (sr, bytes),
+    check_vpk rmap x.(gv) vpk ofs len = ok (sr, sr', bytes) ->
+    exists bytesx,
+      [/\ check_gvalid rmap x = Some (sr, bytesx),
       sr' = sub_region_at_ofs sr ofs len &
       let isub_ofs := interval_of_zone sr'.(sr_zone) in
-      ByteSet.mem bytes isub_ofs].
+      bytes = ByteSet.inter bytesx (ByteSet.full isub_ofs)].
   Proof.
     move=> hofs; rewrite /get_var_kind /check_gvalid.
     case : (@idP (is_glob x)) => hg.
-    + t_xrbindP=> -[_ ws'] /get_globalP /dup [] /wf_globals /sub_region_glob_wf hwf -> <- /= [<- <-].
-      set bytes := ByteSet.full _.
-      exists bytes; split=> //.
-      apply: mem_incl_r; last by apply mem_full.
-      rewrite subset_interval_of_zone.
-      by apply (zbetween_zone_sub_zone_at_ofs hwf).
-    by case hlocal: get_local => [pk|//] [<-] /(check_validP).
+    + t_xrbindP=> -[_ ws'] /get_globalP /dup [] /wf_globals /sub_region_glob_wf hwf -> <- /= [<- <- <-].
+      set bytesx := ByteSet.full _.
+      by exists bytesx.
+    by case hlocal: get_local => [pk|//] [<-] /get_sub_region_bytesP.
   Qed.
 
   Lemma check_vpk_wordP al x vpk ofs ws t :
@@ -931,10 +933,12 @@ Section EXPR.
   Proof.
     move=> hofs hget.
     rewrite /check_vpk_word.
-    t_xrbindP=> -[sr sr'] /(check_vpkP hofs hget) [bytes [hgvalid -> hmem]].
+    t_xrbindP=> -[[sr sr'] bytes] /(check_vpkP hofs hget) [bytesx [hgvalid -> ->]].
     assert (hwf := check_gvalid_wf wfr_wf hgvalid).
-    move=> /(check_alignP hwf) hal.
-    by exists sr, bytes.
+    t_xrbindP=> /check_validP hmem /(check_alignP hwf) hal.
+    exists sr, bytesx; split=> //.
+    apply: mem_incl_l hmem.
+    by apply subset_inter_l.
   Qed.
 
   Lemma addr_from_pkP wdb (x:var_i) pk sr xi ofs :
@@ -1866,15 +1870,16 @@ Proof.
   by rewrite heq; move=> /(_ ltac:(discriminate)) [->].
 Qed.
 
-Lemma get_var_bytes_set_move_bytes rmap x sr r y :
-  get_var_bytes (set_move_bytes rmap x sr) r y =
-    let bytes := get_var_bytes rmap r y in
+Lemma get_var_bytes_set_move_bytes rmap x sr bytes r y :
+  get_var_bytes (set_move_bytes rmap x sr bytes) r y =
+    let bytesy := get_var_bytes rmap r y in
     if sr_region sr != r then
-      bytes
+      bytesy
     else
       if x == y then
-        ByteSet.add (interval_of_zone sr.(sr_zone)) bytes
-      else bytes.
+        ByteSet.union
+          (ByteSet.remove bytesy (interval_of_zone sr.(sr_zone))) bytes
+      else bytesy.
 Proof.
   rewrite /set_move_bytes /get_var_bytes get_bytes_map_setP.
   case: eqP => //= <-.
@@ -1882,13 +1887,13 @@ Proof.
   by case: eqP => //= <-.
 Qed.
 
-Lemma check_gvalid_set_move rmap x sr y sry bytes :
-  check_gvalid (set_move rmap x sr) y = Some (sry, bytes) ->
+Lemma check_gvalid_set_move rmap x sr bytes y sry bytesy :
+  check_gvalid (set_move rmap x sr bytes) y = Some (sry, bytesy) ->
     [/\ ~ is_glob y, x = gv y, sr = sry &
-        bytes = get_var_bytes (set_move_bytes rmap x sr) sr.(sr_region) x]
+        bytesy = get_var_bytes (set_move_bytes rmap x sr bytes) sr.(sr_region) x]
   \/
     [/\ ~ is_glob y -> x <> gv y &
-        check_gvalid rmap y = Some (sry, bytes)].
+        check_gvalid rmap y = Some (sry, bytesy)].
 Proof.
   rewrite /check_gvalid.
   case: (@idP (is_glob y)) => hg.
@@ -1904,25 +1909,25 @@ Proof.
   by move: hneq=> /eqP /negPf ->.
 Qed.
 
-Lemma set_arr_subP rmap x ofs len sr_from rmap2 :
-  set_arr_sub rmap x ofs len sr_from = ok rmap2 ->
+Lemma set_arr_subP rmap x ofs len sr_from bytesy rmap2 :
+  set_arr_sub rmap x ofs len sr_from bytesy = ok rmap2 ->
   exists sr, [/\
     Mvar.get rmap.(var_region) x = Some sr,
     sub_region_at_ofs sr (Some ofs) len = sr_from &
-    set_move_sub rmap x (sub_region_at_ofs sr (Some ofs) len) = rmap2].
+    set_move_sub rmap x (sub_region_at_ofs sr (Some ofs) len) bytesy = rmap2].
 Proof.
   rewrite /set_arr_sub.
   t_xrbindP=> sr /get_sub_regionP -> /eqP heqsub hmove.
   by exists sr.
 Qed.
 
-Lemma check_gvalid_set_move_sub rmap x sr y sry bytes :
-  check_gvalid (set_move_sub rmap x sr) y = Some (sry, bytes) ->
+Lemma check_gvalid_set_move_sub rmap x sr bytes y sry bytesy :
+  check_gvalid (set_move_sub rmap x sr bytes) y = Some (sry, bytesy) ->
     ([/\ ~ is_glob y, x = gv y, Mvar.get rmap.(var_region) x = Some sry &
-         bytes = get_var_bytes (set_move_sub rmap x sr) sry.(sr_region) x]
+         bytesy = get_var_bytes (set_move_sub rmap x sr bytes) sry.(sr_region) x]
   \/
     [/\ ~ is_glob y -> x <> gv y &
-        check_gvalid rmap y = Some (sry, bytes)]).
+        check_gvalid rmap y = Some (sry, bytesy)]).
 Proof.
   rewrite /check_gvalid.
   case: (@idP (is_glob y)) => hg.
@@ -2052,11 +2057,11 @@ Proof.
   by case: hbound => _ /ZltP ->.
 Qed.
 
-Lemma valid_pk_set_move (rmap:region_map) s2 x sr y pk sry :
+Lemma valid_pk_set_move (rmap:region_map) s2 x sr bytes y pk sry :
   ~ Sv.In x pmap.(vnew) ->
   wf_local y pk ->
   valid_pk rmap s2 sry pk ->
-  valid_pk (set_move rmap x sr) s2 sry pk.
+  valid_pk (set_move rmap x sr bytes) s2 sry pk.
 Proof.
   move=> hnnew hlocal.
   case: pk hlocal => //=.
@@ -2067,45 +2072,45 @@ Proof.
   by have := hlocal.(wfs_new); congruence.
 Qed.
 
-Lemma wfr_VAL_set_move rmap s1 s2 x sr v :
+Lemma wfr_VAL_set_move rmap s1 s2 x sr bytes v :
   truncatable true (vtype x) v ->
-  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr) sr.(sr_region) x)
+  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr bytes) sr.(sr_region) x)
     (vm_truncate_val (vtype x) v) ->
   wfr_VAL rmap s1 s2 ->
-  wfr_VAL (set_move rmap x sr) (with_vm s1 (evm s1).[x <- v]) s2.
+  wfr_VAL (set_move rmap x sr bytes) (with_vm s1 (evm s1).[x <- v]) s2.
 Proof.
   move=> htr heqval hval y sry bytesy vy /check_gvalid_set_move [].
   + by move=> [? ? <- ->]; subst x; rewrite get_gvar_eq //; t_xrbindP => hd <-.
   by move=> [? hgvalid]; rewrite get_gvar_neq => //; apply hval.
 Qed.
 
-Lemma wfr_PTR_set_move (rmap : region_map) s2 x pk sr :
+Lemma wfr_PTR_set_move (rmap : region_map) s2 x pk sr bytes :
   get_local pmap x = Some pk ->
   valid_pk rmap s2 sr pk ->
   wfr_PTR rmap s2 ->
-  wfr_PTR (set_move rmap x sr) s2.
+  wfr_PTR (set_move rmap x sr bytes) s2.
 Proof.
   move=> hlx hpk hptr y sry.
   have /wf_vnew hnnew := hlx.
   rewrite Mvar.setP; case: eqP.
   + move=> <- [<-].
     exists pk; split=> //.
-    by apply (valid_pk_set_move _ hnnew (wf_locals hlx) hpk).
+    by apply (valid_pk_set_move _ _ hnnew (wf_locals hlx) hpk).
   move=> _ /hptr {pk hlx hpk} [pk [hly hpk]].
   exists pk; split=> //.
-  by apply (valid_pk_set_move _ hnnew (wf_locals hly) hpk).
+  by apply (valid_pk_set_move _ _ hnnew (wf_locals hly) hpk).
 Qed.
 
 (* There are several lemmas about [set_move] and [valid_state], and all are useful. *)
-Lemma valid_state_set_move rmap m0 s1 s2 x sr pk v :
+Lemma valid_state_set_move rmap m0 s1 s2 x sr bytes pk v :
   valid_state rmap m0 s1 s2 ->
   wf_sub_region sr x.(vtype) ->
   get_local pmap x = Some pk ->
   valid_pk rmap.(region_var) s2 sr pk ->
   truncatable true (vtype x) v ->
-  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr) sr.(sr_region) x)
+  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr bytes) sr.(sr_region) x)
        (vm_truncate_val (vtype x) v) ->
-  valid_state (set_move rmap x sr) m0 (with_vm s1 (evm s1).[x <- v]) s2.
+  valid_state (set_move rmap x sr bytes) m0 (with_vm s1 (evm s1).[x <- v]) s2.
 Proof.
   move=> hvs hwf hlx hpk htr heqval.
   case:(hvs) => hscs hvalid hdisj hincl hincl2 hunch hrip hrsp heqvm hwfr heqmem hglobv htop.
@@ -2123,15 +2128,15 @@ Lemma ptr_prop x p (w:word Uptr):
   type_of_val (Vword w) = vtype p.
 Proof. by move=> /wf_locals /= /wfr_rtype ->. Qed.
 
-Lemma valid_state_set_move_regptr rmap m0 s1 s2 x sr v p:
+Lemma valid_state_set_move_regptr rmap m0 s1 s2 x sr bytes v p:
   type_of_val (Vword (sub_region_addr sr)) = vtype p ->
   valid_state rmap m0 s1 s2 ->
   wf_sub_region sr x.(vtype) ->
   get_local pmap x = Some (Pregptr p) ->
   truncatable true (vtype x) v ->
-  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr) sr.(sr_region) x)
+  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr bytes) sr.(sr_region) x)
         (vm_truncate_val (vtype x) v) ->
-  valid_state (set_move rmap x sr) m0
+  valid_state (set_move rmap x sr bytes) m0
        (with_vm s1 (evm s1).[x <- v])
        (with_vm s2 (evm s2).[p <- Vword (sub_region_addr sr)]).
 Proof.
@@ -2183,17 +2188,17 @@ Proof. by move=> hvs /wfr_ptr [_ [/wf_vnew ? _]]. Qed.
 (* The lemma manipulates [set_stack_ptr (set_move ...)], rather than
    [set_stack_ptr] alone.
 *)
-Lemma check_gvalid_set_stack_ptr rmap m0 s1 s2 s ws z f y sry bytes x sr :
+Lemma check_gvalid_set_stack_ptr rmap m0 s1 s2 s ws z f y sry bytesy x sr bytes :
   valid_state rmap m0 s1 s2 ->
   ~ Sv.In x pmap.(vnew) ->
   Sv.In f pmap.(vnew) ->
-  check_gvalid (set_stack_ptr (set_move rmap x sr) s ws z f) y = Some (sry, bytes) ->
-  exists bytes',
-    [/\ check_gvalid (set_move rmap x sr) y = Some (sry, bytes'),
+  check_gvalid (set_stack_ptr (set_move rmap x sr bytes) s ws z f) y = Some (sry, bytesy) ->
+  exists bytesy',
+    [/\ check_gvalid (set_move rmap x sr bytes) y = Some (sry, bytesy'),
         ~ is_glob y -> f <> gv y &
-        bytes =
-          if (sub_region_stkptr s ws z).(sr_region) != sry.(sr_region) then bytes'
-          else ByteSet.remove bytes' (interval_of_zone (sub_zone_at_ofs (sub_region_stkptr s ws z).(sr_zone) (Some 0) (wsize_size Uptr)))].
+        bytesy =
+          if (sub_region_stkptr s ws z).(sr_region) != sry.(sr_region) then bytesy'
+          else ByteSet.remove bytesy' (interval_of_zone (sub_zone_at_ofs (sub_region_stkptr s ws z).(sr_zone) (Some 0) (wsize_size Uptr)))].
 Proof.
   move=> hvs hnnew hnew.
   rewrite /check_gvalid /=.
@@ -2238,7 +2243,7 @@ Proof.
   by apply (distinct_regions_disjoint_zrange hwf hwf1 heqr).
 Qed.
 
-Lemma valid_state_set_stack_ptr rmap m0 s1 s2 x s ofs ws z f mem2 sr v :
+Lemma valid_state_set_stack_ptr rmap m0 s1 s2 x s ofs ws z f mem2 sr bytes v :
   valid_state rmap m0 s1 s2 ->
   wf_sub_region sr x.(vtype) ->
   get_local pmap x = Some (Pstkptr s ofs ws z f) ->
@@ -2249,9 +2254,9 @@ Lemma valid_state_set_stack_ptr rmap m0 s1 s2 x s ofs ws z f mem2 sr v :
     read mem2 al p ws = read (emem s2) al p ws) ->
   read mem2 Aligned (sub_region_addr (sub_region_stkptr s ws z)) Uptr = ok (sub_region_addr sr) ->
   truncatable true (vtype x) v ->
-  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr) sr.(sr_region) x)
+  eq_sub_region_val x.(vtype) (emem s2) sr (get_var_bytes (set_move rmap x sr bytes) sr.(sr_region) x)
    (vm_truncate_val (vtype x) v) ->
-  valid_state (set_stack_ptr (set_move rmap x sr) s ws z f) m0 (with_vm s1 (evm s1).[x <- v]) (with_mem s2 mem2).
+  valid_state (set_stack_ptr (set_move rmap x sr bytes) s ws z f) m0 (with_vm s1 (evm s1).[x <- v]) (with_mem s2 mem2).
 Proof.
   move=> hvs hwf hlx hss hvalideq hreadeq hreadptr htr heqval.
   have hreadeq': forall al p ws,
@@ -2286,19 +2291,19 @@ Proof.
     move=> hneq /wfr_ptr [pky [hly hpky]].
     exists pky; split=> //.
     apply (valid_pk_set_stack_ptr hlocal hreadeq hneq hly).
-    by apply (valid_pk_set_move sr (wf_vnew hlx) (wf_locals hly) hpky).
+    by apply (valid_pk_set_move sr _ (wf_vnew hlx) (wf_locals hly) hpky).
   + by apply (eq_mem_source_write_slot hvs hwfs hreadeq).
   by rewrite -(ss_top_stack hss).
 Qed.
 
-Lemma valid_state_set_move_sub rmap m0 s1 s2 x pk v sr :
+Lemma valid_state_set_move_sub rmap m0 s1 s2 x pk v sr bytes :
   valid_state rmap m0 s1 s2 ->
   get_local pmap x = Some pk ->
   truncatable true (vtype x) v ->
   (forall srx, Mvar.get rmap.(var_region) x = Some srx ->
-    eq_sub_region_val x.(vtype) (emem s2) srx (get_var_bytes (set_move_sub rmap x sr) srx.(sr_region) x)
+    eq_sub_region_val x.(vtype) (emem s2) srx (get_var_bytes (set_move_sub rmap x sr bytes) srx.(sr_region) x)
         (vm_truncate_val (vtype x) v)) ->
-  valid_state (set_move_sub rmap x sr) m0 (with_vm s1 (evm s1).[x <- v]) s2.
+  valid_state (set_move_sub rmap x sr bytes) m0 (with_vm s1 (evm s1).[x <- v]) s2.
 Proof.
   move=> hvs hlx htr heqval.
   case:(hvs) => hscs hvalid hdisj hincl hincl2 hunch hrip hrsp heqvm hwfr heqmem hglobv htop.
@@ -2329,7 +2334,7 @@ Qed.
    sub-region [sr], since we can derive it for the rest of [sr] from
    the [valid_state] hypothesis.
 *)
-Lemma valid_state_set_move_sub_write_lval rmap m0 s1 s2 r x ofsx ofs len n (a : WArray.array n) s1' pk sr :
+Lemma valid_state_set_move_sub_write_lval rmap m0 s1 s2 r x ofsx ofs len n (a : WArray.array n) s1' pk sr bytes :
   valid_state rmap m0 s1 s2 ->
   get_Lvar_sub r = ok (x, ofsx) ->
   match ofsx with
@@ -2339,14 +2344,15 @@ Lemma valid_state_set_move_sub_write_lval rmap m0 s1 s2 r x ofsx ofs len n (a :
   write_lval true gd r (Varr a) s1 = ok s1' ->
   get_local pmap x = Some pk ->
   (forall srx, Mvar.get rmap.(var_region) x = Some srx -> srx = sr) ->
-  let: rmap2 := set_move_sub rmap x (sub_region_at_ofs sr (Some ofs) len) in
+  ByteSet.subset bytes (ByteSet.full (interval_of_zone (sub_region_at_ofs sr (Some ofs) len).(sr_zone))) ->
+  let: rmap2 := set_move_sub rmap x (sub_region_at_ofs sr (Some ofs) len) bytes in
   eq_sub_region_val_read (emem s2) (sub_region_at_ofs sr (Some ofs) len) (get_var_bytes rmap2 sr.(sr_region) x) (Varr a) ->
   valid_state rmap2 m0 s1' s2.
 Proof.
   move=> hvs.
   set valid_state := valid_state. (* hack due to typeclass interacting badly *)
   case: r => //=.
-  + move=> _ [-> <-] [<- <-] /write_varP [-> hdb h] hlx hget hread.
+  + move=> _ [-> <-] [<- <-] /write_varP [-> hdb h] hlx hget _ hread.
     have /vm_truncate_valE [hty heq]:= h.
     apply (valid_state_set_move_sub hvs hlx h).
     move=> _ /hget ->; rewrite heq.
@@ -2360,7 +2366,7 @@ Proof.
   have {he hv} he : sem_pexpr true gd s1 e >>= to_int = ok i.
   + by rewrite he.
   have {hofs} -> := get_ofs_subP he hofs.
-  move=> hlx hget hread.
+  move=> hlx hget hsub hread.
   apply (valid_state_set_move_sub hvs hlx h).
   move=> srx /dup[] /hget{hget} ? hget; subst srx; rewrite heq.
   split=> // off hmem w /=.
@@ -2378,8 +2384,10 @@ Proof.
   apply hread'.
   move: hmem.
   rewrite get_var_bytes_set_move_bytes !eq_refl /=.
-  rewrite ByteSet.addE => /orP [|//].
-  by rewrite /I.memi /= !zify; lia.
+  rewrite ByteSet.unionE => /orP[].
+  + by rewrite ByteSet.removeE => /andP [].
+  move: hsub => /ByteSet.subsetP /[apply].
+  by rewrite ByteSet.fullE /I.memi /= !zify; lia.
 Qed.
 
 (* ------------------------------------------------------------------ *)
@@ -2453,7 +2461,8 @@ Proof.
   have hofs': forall zofs, Some ofs = Some zofs -> 0 <= zofs /\ zofs + len <= size_slot y.(gv).
   + by move=> _ [<-].
   t_xrbindP=> -[[[sry' mk] ey] ofs2'] _ <-.
-  t_xrbindP=> -[sry _] /(check_vpkP hofs' hkindy) [bytesy [hgvalidy -> hmemy]].
+  t_xrbindP=> -[[sry sry''] bytesy] hvpk.
+  have {hvpk} [{}bytesy [hgvalidy -> ->]] := check_vpkP hofs' hkindy hvpk.
   assert (hwfy := check_gvalid_wf wfr_wf hgvalidy).
   have hwfy': wf_sub_region (sub_region_at_ofs sry (Some ofs) len) (sarr (Z.to_pos len)).
   + move: hofs'.
@@ -2463,22 +2472,32 @@ Proof.
   have hpky: valid_vpk rmap1 s2 y.(gv) sry vpky.
   + have /wfr_gptr := hgvalidy.
     by rewrite hkindy => -[_ [[]] <-].
-  move=> [e1 ofs2] /(mk_addr_pexprP true _ hwfpky hpky) [w [he1 haddr]] ? <- <- ?; subst sry' ofs2'.
+  t_xrbindP=> -[e1 ofs2] /(mk_addr_pexprP true _ hwfpky hpky) [w [he1 haddr]] /= ? <- <- ?; subst sry' ofs2'.
   have [? [ay [hgety hay]]] := get_Pvar_subP he hgete hofsy.
   subst n.
-  have hread: forall bytes,
-    eq_sub_region_val_read (emem s2) (sub_region_at_ofs sry (Some ofs) len) bytes (Varr a').
-  + move=> bytes off hmem w' /= /dup[].
-    rewrite -{1}get_read8 => /WArray.get_valid8 /WArray.in_boundP hoff.
-    move=> /hay.
+  have hread:
+    eq_sub_region_val_read
+      (emem s2) (sub_region_at_ofs sry (Some ofs) len)
+      (get_var_bytes
+        (set_move_bytes rmap1 x (sub_region_at_ofs sry (Some ofs) len)
+          (ByteSet.inter
+            bytesy
+            (ByteSet.full
+              (interval_of_zone
+                (sub_region_at_ofs sry (Some ofs) len).(sr_zone)))))
+        (sub_region_at_ofs sry (Some ofs) len).(sr_region) x)
+      (Varr a').
+  + rewrite /= get_var_bytes_set_move_bytes /= !eqxx /=.
+    move=> off hmem w' /dup[] /get_val_byte_bound /= hoff /hay.
     rewrite -sub_region_addr_offset -GRing.addrA -wrepr_add.
     assert (hval := wfr_val hgvalidy hgety).
     case: hval => hread _.
     apply hread.
-    rewrite memi_mem_U8; apply: mem_incl_r hmemy; rewrite subset_interval_of_zone.
-    rewrite -(sub_zone_at_ofs_compose _ _ _ len).
-    apply zbetween_zone_byte; last by rewrite /=; lia.
-    by apply zbetween_zone_refl.
+    move: hmem; rewrite ByteSet.unionE.
+    case/orP.
+    + by rewrite ByteSet.removeE /I.memi /= !zify; lia.
+    rewrite ByteSet.interE => /andP [+ _].
+    by rewrite Z.add_assoc.
 
   case: r hgetr hw => //.
   + move=> _ [-> <-] /write_varP [ -> hdb h].
@@ -2486,11 +2505,19 @@ Proof.
     case hlx: (get_local pmap x) => [pk|//].
     have /wf_locals hlocal := hlx.
 
-    have heqval: forall bytes,
-      eq_sub_region_val x.(vtype) (emem s2) (sub_region_at_ofs sry (Some ofs) len)
-                        bytes (Varr a').
-    + move=> bytes.
-      by split=> // off /hread{hread}hread w' /(cast_get8 hax) /hread.
+    have heqval:
+      eq_sub_region_val
+        x.(vtype) (emem s2) (sub_region_at_ofs sry (Some ofs) len)
+        (get_var_bytes
+          (set_move_bytes rmap1 x (sub_region_at_ofs sry (Some ofs) len)
+            (ByteSet.inter
+              bytesy
+              (ByteSet.full
+                (interval_of_zone
+                  (sub_region_at_ofs sry (Some ofs) len).(sr_zone)))))
+          (sub_region_at_ofs sry (Some ofs) len).(sr_region) x)
+        (Varr a').
+    + by split.
 
     have hwf: wf_sub_region (sub_region_at_ofs sry (Some ofs) len) x.(vtype).
     + by apply: (wf_sub_region_subtype _ hwfy'); rewrite hty.
@@ -2499,7 +2526,9 @@ Proof.
     + t_xrbindP=> s ofs' ws z sc hlx hlocal /eqP heqsub <- <-.
       exists s2; split; first by constructor.
       (* valid_state update *)
-      by have := (valid_state_set_move hvs hwf hlx _ h); apply => //; rewrite htreq.
+      apply: (valid_state_set_move hvs hwf hlx _ h) => //.
+      by rewrite htreq.
+
     + move=> p hlx hlocal /=.
       case Hmov_ofs: (sap_mov_ofs saparams) => [ins| //].
       move=> [<- <-].
@@ -2556,7 +2585,8 @@ Proof.
 
     exists (with_vm (with_mem s2 mem2) vm2); split=> //.
     apply valid_state_vm_eq => //.
-    by apply (valid_state_set_stack_ptr hvs hwf hlx hss hvalideq hreadeq hreadptr h); rewrite htreq.
+    apply (valid_state_set_stack_ptr hvs hwf hlx hss hvalideq hreadeq hreadptr h).
+    by rewrite htreq.
 
   (* interestingly, we can prove that n = Z.to_pos len = Z.to_pos (arr_size ws len2)
      but it does not seem useful
@@ -2568,7 +2598,8 @@ Proof.
   exists s2; split; first by constructor.
   apply (valid_state_set_move_sub_write_lval hvs hgetr refl_equal hw hlx).
   + by move=> ?; rewrite hgetx => -[].
-  by rewrite heqsub.
+  + by rewrite heqsub; apply subset_inter_r.
+  by move: hread; rewrite -{-3}heqsub.
 Qed.
 
 Lemma is_protect_ptr_failP rs o es r e msf :
@@ -2602,7 +2633,9 @@ Proof.
   set ofs := 0%Z; set len := size_slot (gv y).
   have hofs': forall zofs, Some ofs = Some zofs -> 0 <= zofs /\ zofs + len <= size_slot y.(gv).
   + by move=> _ [<-].
-  t_xrbindP => -[[sry' mk] ey] hvpky hr [sry _] /(check_vpkP hofs' hkindy) [bytesy [hgvalidy -> hmemy]].
+  t_xrbindP => -[[sry' mk] ey] hvpky hr.
+  t_xrbindP=> -[[sry sry''] bytesy] hvpk.
+  have {hvpk} [{}bytesy [hgvalidy -> ->]] := check_vpkP hofs' hkindy hvpk.
   assert (hwfy := check_gvalid_wf wfr_wf hgvalidy).
   have hwfy': wf_sub_region (sub_region_at_ofs sry (Some ofs) len) (sarr (Z.to_pos len)).
   + move: hofs'.
@@ -2612,33 +2645,51 @@ Proof.
   have hpky: valid_vpk rmap1 s2 y.(gv) sry vpky.
   + have /wfr_gptr := hgvalidy.
     by rewrite hkindy => -[_ [[]] <-].
-  move=> [e1 ofs2] /dup [] hmk_addr /(mk_addr_pexprP true _ hwfpky hpky) [w [he1 haddr]] [] <- _ <-.
+  t_xrbindP=> -[e1 ofs2] /dup [] hmk_addr /(mk_addr_pexprP true _ hwfpky hpky) [w [he1 haddr]] [] <- _ <-.
   have [? [ay [hgety hay]]] := get_Pvar_subP he hgete erefl; subst n.
 
-  have hread: forall bytes,
-    eq_sub_region_val_read (emem s2) (sub_region_at_ofs sry (Some ofs) len) bytes (Varr a').
-  + move=> bytes off hmem w' /(cast_get8 (WArray.castK a')) /dup[].
-    rewrite -{1}get_read8 => /WArray.get_valid8 /WArray.in_boundP; rewrite Z2Pos.id // => hoff.
-    move=> /hay.
+  have hread:
+    eq_sub_region_val_read
+      (emem s2) (sub_region_at_ofs sry (Some ofs) len)
+      (get_var_bytes
+        (set_move_bytes rmap1 x (sub_region_at_ofs sry (Some ofs) len)
+          (ByteSet.inter
+            bytesy
+            (ByteSet.full
+              (interval_of_zone
+                (sub_region_at_ofs sry (Some ofs) len).(sr_zone)))))
+        (sub_region_at_ofs sry (Some ofs) len).(sr_region) x)
+      (Varr a').
+  + rewrite /= get_var_bytes_set_move_bytes /= !eqxx /=.
+    move=> off hmem w' /dup[] /get_val_byte_bound /= hoff /hay.
     rewrite -sub_region_addr_offset -GRing.addrA -wrepr_add.
     assert (hval := wfr_val hgvalidy hgety).
     case: hval => hread _.
     apply hread.
-    rewrite memi_mem_U8; apply: mem_incl_r hmemy; rewrite subset_interval_of_zone.
-    rewrite -(sub_zone_at_ofs_compose _ _ _ len).
-    apply zbetween_zone_byte => //.
-    by apply zbetween_zone_refl.
+    move: hmem; rewrite ByteSet.unionE.
+    case/orP.
+    + by rewrite ByteSet.removeE /I.memi /= !zify; lia.
+    rewrite ByteSet.interE => /andP [+ _].
+    by rewrite Z.add_assoc.
 
   case: r hr hgetr hw => //=.
   move=> _ _ [-> <-] /write_varP [->] _ /vm_truncate_valE [hxty _].
   case hlx: (get_local pmap x) => [pk|//].
   have /wf_locals hlocal := hlx.
 
-  have heqval: forall bytes,
-    eq_sub_region_val x.(vtype) (emem s2) (sub_region_at_ofs sry (Some ofs) len)
-                      bytes (Varr a').
-  + move=> bytes.
-    by split=> // off /hread{hread}hread w' /(cast_get8 hax) /hread.
+  have heqval:
+      eq_sub_region_val
+        x.(vtype) (emem s2) (sub_region_at_ofs sry (Some ofs) len)
+        (get_var_bytes
+          (set_move_bytes rmap1 x (sub_region_at_ofs sry (Some ofs) len)
+            (ByteSet.inter
+              bytesy
+              (ByteSet.full
+                (interval_of_zone
+                  (sub_region_at_ofs sry (Some ofs) len).(sr_zone)))))
+          (sub_region_at_ofs sry (Some ofs) len).(sr_region) x)
+        (Varr a').
+  + by split.
 
   have hwf: wf_sub_region (sub_region_at_ofs sry (Some ofs) len) x.(vtype).
   + by apply: (wf_sub_region_subtype _ hwfy'); rewrite hxty.
@@ -2698,14 +2749,14 @@ Proof.
   move=> _ /write_varP [-> _ /vm_truncate_valE [hxty hxtr]].
   move=> _ /write_varP [-> _ /vm_truncate_valE [hyty hytr]].
   rewrite with_vm_idem /= => ?; subst s1'.
-  move=> pz /get_regptrP hpz [srz srz_] /check_validP [zbytes [gvalidz ? /= /ByteSet.memP hzbytes]]; subst srz_.
+  move=> pz /get_regptrP hpz [[srz srz_] _] /get_sub_region_bytesP [zbytes [gvalidz ? ->]]; subst srz_.
   t_xrbindP.
-  move=> pw /get_regptrP hpw [srw srw_] /check_validP [wbytes [gvalidw ? /= /ByteSet.memP hwbytes]]; subst srw_.
+  move=> pw /get_regptrP hpw [[srw srw_] _] /get_sub_region_bytesP [wbytes [gvalidw ? ->]]; subst srw_.
   t_xrbindP.
   move=> px /get_regptrP hpx py /get_regptrP hpy /andP [xloc yloc] <- <-.
   have hwty := type_of_get_gvar_array hw.
   rewrite hwty -hxty.
-  set rmap1' := set_move rmap1 _ _.
+  set rmap1' := set_move rmap1 _ _ _.
   have : valid_state rmap1' m0
          (with_vm s1 (evm s1).[x <- Varr tw])
          (with_vm s2 (evm s2).[px <- Vword (sub_region_addr (sub_region_at_ofs srw (Some 0) (size_slot x)))]).
@@ -2715,21 +2766,20 @@ Proof.
     apply (valid_state_set_move_regptr (ptr_prop _ hpx) hvs (sub_region_at_ofs_0_wf hwfw) hpx htrx).
     rewrite /set_move /= get_var_bytes_set_move_bytes eqxx /= eqxx /=.
     rewrite hxty eqxx; split => //.
-    move=> off hmem ww hget.
+    move=> off hmem ww /dup[] /get_val_byte_bound /= hoff hget.
     have /(_ _ _ _ _ hvs _ _ _ _ gvalidw) := vs_wf_region.(wfr_val).
     rewrite get_gvar_nglob in hw => //; last by rewrite -is_lvar_is_glob.
-    rewrite get_gvar_nglob // => /(_ _ hw) [+ _]. 
+    rewrite get_gvar_nglob // => /(_ _ hw) [+ _].
     rewrite -sub_region_addr_offset wrepr0 GRing.addr0; apply => //.
-    apply: hwbytes; move: hmem; rewrite ByteSet.addE.
-    rewrite /= Z.add_0_r hwty /=.
-    case: (boolP (I.memi _ _)) => //=.
-    have := get_val_byte_bound hget.
-    by rewrite /I.memi /= !zify; lia.
+    move: hmem; rewrite ByteSet.unionE.
+    case/orP.
+    + by rewrite ByteSet.removeE /I.memi /= !zify; lia.
+    by rewrite ByteSet.interE /= Z.add_0_r => /andP [+ _].
   set s1' := with_vm s1 _.
   set s2' := with_vm s2 _ => hvs'.
   have hzty := type_of_get_gvar_array hz.
   rewrite hzty -hyty.
-  set rmap1'' := set_move rmap1' _ _.
+  set rmap1'' := set_move rmap1' _ _ _.
   have hvs'' : valid_state rmap1'' m0
          (with_vm s1' (evm s1').[y <- Varr tz])
          (with_vm s2' (evm s2').[py <- Vword (sub_region_addr (sub_region_at_ofs srz (Some 0) (size_slot y)))]).
@@ -2739,16 +2789,15 @@ Proof.
     apply (valid_state_set_move_regptr (ptr_prop _ hpy) hvs' (sub_region_at_ofs_0_wf hwfz) hpy htry).
     rewrite /set_move /= get_var_bytes_set_move_bytes eqxx /= eqxx /=.
     rewrite hyty eqxx; split => //.
-    move=> off hmem ww hget.
+    move=> off hmem ww /dup[] /get_val_byte_bound /= hoff hget.
     have /(_ _ _ _ _ hvs _ _ _ _ gvalidz) := vs_wf_region.(wfr_val).
     rewrite get_gvar_nglob in hz => //; last by rewrite -is_lvar_is_glob.
     rewrite get_gvar_nglob // => /(_ _ hz) [+ _]. 
     rewrite -sub_region_addr_offset wrepr0 GRing.addr0; apply => //.
-    apply: hzbytes; move: hmem; rewrite ByteSet.addE.
-    rewrite /= Z.add_0_r hzty /=.
-    case: (boolP (I.memi _ _)) => //=.
-    have := get_val_byte_bound hget.
-    by rewrite /I.memi /= !zify; lia.
+    move: hmem; rewrite ByteSet.unionE.
+    case/orP.
+    + by rewrite ByteSet.removeE /I.memi /= !zify; lia.
+    by rewrite ByteSet.interE /= Z.add_0_r => /andP [+ _].
   eexists; split; last eauto.  
   rewrite /s2' with_vm_idem /=.
   rewrite -!sub_region_addr_offset !wrepr0 !GRing.addr0.
@@ -2797,6 +2846,7 @@ Proof.
       by rewrite hlx => -[_ [[<-] ->]].
     + by move=> _ _ /get_sub_regionP; congruence.
     by move=> _ _ _ _ _ _ /get_sub_regionP; congruence.
+  + by apply subset_refl.
   move=> off hmem w /=.
   by rewrite WArray.get_empty; case: ifP.
 Qed.
@@ -2886,7 +2936,7 @@ Proof.
   t_xrbindP=> x _ _.
   case: get_local => [pk|//].
   case: pk => // p.
-  t_xrbindP=> -[sr ?] _ _ _ _ _ /= <- _.
+  t_xrbindP=> -[[sr ?] ?] _; t_xrbindP=> _ _ _ _ _ /= <- _.
   by eexists.
 Qed.
 
@@ -2921,7 +2971,7 @@ Proof.
   case: opi => [pi|].
   + case: get_local => [pk|//].
     case: pk => // p.
-    t_xrbindP=> -[{sr}sr _] /= _ tt hclear _ _ hw <- _.
+    t_xrbindP=> -[[sr' ?] ?] /= _; t_xrbindP=> _ _ tt hclear _ hw <- _.
     by move: hclear; rewrite hw => /set_clearP [? _].
   case: get_local => //.
   by t_xrbindP.
@@ -3320,7 +3370,8 @@ Proof.
   case: opi => [pi|].
   + case: get_local => [pk|//].
     case: pk => // p.
-    t_xrbindP=> -[sr _] /check_validP [bytes [hgvalid -> hmem]] /= {rmap2}rmap2 hclear _ <- _ _.
+    t_xrbindP=> -[[sr _] _] /get_sub_region_bytesP [bytes [hgvalid -> ->]].
+    t_xrbindP=> /check_validP hmem _ /= {rmap2}rmap2 hclear <- _ _.
     case: pp_writable hclear; last first.
     + move=> [<-]; split=> //.
       by apply incl_refl.
@@ -3331,7 +3382,11 @@ Proof.
       move: hgvalid; rewrite /check_gvalid /=.
       case: Mvar.get => [_|//] [-> hget] hnone.
       move: hmem; rewrite -hget (get_var_bytes_None _ hnone) /=.
-      move=> /mem_is_empty_l -/(_ is_empty_empty).
+      have hempty: forall b, ByteSet.is_empty (ByteSet.inter ByteSet.empty b).
+      + move=> b.
+        apply: (is_empty_incl _ is_empty_empty).
+        by apply subset_inter_l.
+      move=> /mem_is_empty_l /(_ (hempty _)).
       apply /negP.
       apply interval_of_zone_wf.
       by apply size_of_gt0.
@@ -3385,8 +3440,8 @@ Proof.
     by eexists.
   case hlx: get_local => [pk|//].
   case: pk hlx => // p hlx.
-  t_xrbindP=> -[sr _] /check_validP [bytes [hgvalid -> hmem]] /=.
-  move=> _ _ _ _ _ <- /= hget.
+  t_xrbindP=> -[[sr ?] ?] /get_sub_region_bytesP [bytes [hgvalid -> ->]] /=.
+  t_xrbindP=> /check_validP hmem _ _ _ _ _ <- /= hget.
   have /wfr_gptr := hgvalid.
   rewrite /get_var_kind /= hlx => -[_ [[<-] /=]] hgetp.
   rewrite get_gvar_nglob // /get_var /= {}hgetp /= orbT /=.
@@ -3399,6 +3454,11 @@ Proof.
   have /(wfr_val hgvalid) [hread /= hty] := hget'.
   move=> off w /dup[] /get_val_byte_bound; rewrite hty => hoff.
   apply hread.
+  have :=
+    subset_inter_l bytes
+      (ByteSet.full
+        (interval_of_zone (sub_region_at_ofs sr (Some 0) (size_slot x)).(sr_zone))).
+  move=> /mem_incl_l -/(_ _ hmem) {}hmem.
   rewrite memi_mem_U8; apply: mem_incl_r hmem; rewrite subset_interval_of_zone.
   rewrite -(Z.add_0_l off).
   rewrite -(sub_zone_at_ofs_compose _ _ _ (size_slot x)).
@@ -3458,9 +3518,9 @@ Proof.
     by rewrite /wf_arg hnreg.
   case hlx: get_local => [pk|//].
   case: pk hlx => // p hlx.
-  t_xrbindP=> -[sr _] /check_validP [bytes [hgvalid _ _]] /=.
+  t_xrbindP=> -[[sr ?] ?] /get_sub_region_bytesP [bytes [hgvalid _ _]] /=.
   have /(check_gvalid_wf wfr_wf) /= hwf := hgvalid.
-  move=> {}rmap2 hclear /(check_alignP hwf) halign _ <- hget /=.
+  t_xrbindP=> _ /(check_alignP hwf) halign {}rmap2 hclear _ <- hget /=.
   have /wfr_gptr := hgvalid.
   rewrite /get_var_kind /= hlx => -[_ [[<-] /=]] hgetp.
   rewrite get_gvar_nglob // /get_var /= {}hgetp /= orbT /=.
@@ -3562,9 +3622,9 @@ Proof.
     by split.
   case hlx: get_local => [pk|//].
   case: pk hlx => // p hlx.
-  t_xrbindP=> -[sr _] /check_validP [bytes [hgvalid -> hmem]] /=.
+  t_xrbindP=> -[[sr _] _] /get_sub_region_bytesP [bytes [hgvalid -> ->]] /=.
   have /(check_gvalid_wf wfr_wf) /= hwf := hgvalid.
-  move=> {rmap2}rmap2 hclear _ <- <- <- hget /=.
+  t_xrbindP=> _ _ {rmap2}rmap2 hclear <- <- <- hget /=.
   have /wfr_gptr := hgvalid.
   rewrite /get_var_kind /= hlx => -[_ [[<-] /=]] hgetp.
   rewrite get_gvar_nglob // /get_var /= {}hgetp /= orbT /= => -[<-].
@@ -4133,8 +4193,8 @@ Proof.
   move: hresult; rewrite /check_result.
   case: sao_return => [i|].
   + case heq: nth => [sr|//].
-    t_xrbindP=> /eqP heqty -[sr' _] /check_validP [bytes [hgvalid -> hmem]].
-    move=> /= /eqP ? p /get_regptrP hlres1 <-; subst sr'.
+    t_xrbindP=> /eqP heqty -[[sr' _] _] /get_sub_region_bytesP [bytes [hgvalid -> ->]].
+    t_xrbindP=> /check_validP hmem /eqP ? p /get_regptrP hlres1 <-; subst sr'.
     have /wfr_gptr := hgvalid.
     rewrite /get_var_kind /= /get_var /get_local hlres1 => -[? [[<-] /= ->]] /=; rewrite orbT /=.
     eexists; split; first by reflexivity.
@@ -4154,6 +4214,11 @@ Proof.
     case: hval => hread hty.
     move=> off w /dup[] /get_val_byte_bound; rewrite hty => hoff.
     apply hread.
+    have :=
+    subset_inter_l bytes
+      (ByteSet.full
+        (interval_of_zone (sub_region_at_ofs sr (Some 0) (size_slot res1)).(sr_zone))).
+    move=> /mem_incl_l -/(_ _ hmem) {}hmem.
     rewrite memi_mem_U8; apply: mem_incl_r hmem; rewrite subset_interval_of_zone.
     rewrite -(Z.add_0_l off).
     rewrite -(sub_zone_at_ofs_compose _ _ _ (size_slot res1)).