@@ -13,7 +13,7 @@
 (** Translation from Csharpminor to Cminor. *)
 
 From Coq Require Import FSets FSetAVL Orders Mergesort.
-Require Import Coqlib Maps Ordered Errors Integers Floats.
+Require Import Coqlib Maps Ordered Errors Integers Floats Memory.
 Require Import AST Linking.
 Require Import Csharpminor Cminor.
 
@@ -216,16 +216,11 @@ with transl_lblstmt (cenv: compilenv) (xenv: exit_env) (ls: Csharpminor.lbl_stmt
   allocated a slot in the Cminor stack data.  Sufficient padding is
   inserted to ensure adequate alignment of addresses. *)
 
-Definition block_alignment (sz: Z) : Z :=
-  if zlt sz 2 then 1
-  else if zlt sz 4 then 2
-  else if zlt sz 8 then 4 else 8.
-
 Definition assign_variable
     (cenv_stacksize: compilenv * Z) (id_sz: ident * Z) : compilenv * Z :=
   let (id, sz) := id_sz in
   let (cenv, stacksize) := cenv_stacksize in
-  let ofs := align stacksize (block_alignment sz) in
+  let ofs := align stacksize (min_safe_alignment sz) in
   (PTree.set id ofs cenv, ofs + Z.max 0 sz).
 
 Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z :=
 
@@ -885,21 +885,12 @@ Qed.
 
 (** Properties of the compilation environment produced by [build_compilenv] *)
 
-Remark block_alignment_pos:
-  forall sz, block_alignment sz > 0.
-Proof.
-  unfold block_alignment; intros.
-  destruct (zlt sz 2). lia.
-  destruct (zlt sz 4). lia.
-  destruct (zlt sz 8); lia.
-Qed.
-
 Remark assign_variable_incr:
   forall id sz cenv stksz cenv' stksz',
   assign_variable (cenv, stksz) (id, sz) = (cenv', stksz') -> stksz <= stksz'.
 Proof.
   simpl; intros. inv H.
-  generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)).
+  generalize (align_le stksz (min_safe_alignment sz) (min_safe_alignment_pos sz)).
   assert (0 <= Z.max 0 sz). apply Zmax_bound_l. lia.
   lia.
 Qed.
@@ -919,35 +910,22 @@ Qed.
 
 Remark inj_offset_aligned_block:
   forall stacksize sz,
-  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz.
+  Mem.inj_offset_aligned (align stacksize (min_safe_alignment sz)) sz.
 Proof.
-  intros; red; intros.
-  apply Z.divide_trans with (block_alignment sz).
-  unfold align_chunk.  unfold block_alignment.
-  generalize Z.divide_1_l; intro.
-  generalize Z.divide_refl; intro.
-  assert (2 | 4). exists 2; auto.
-  assert (2 | 8). exists 4; auto.
-  assert (4 | 8). exists 2; auto.
-  destruct (zlt sz 2).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct (zlt sz 4).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct (zlt sz 8).
-  destruct chunk; simpl in *; auto; extlia.
-  destruct chunk; simpl; auto.
-  apply align_divides. apply block_alignment_pos.
+  intros; red; intros. apply Z.divide_trans with (min_safe_alignment sz).
+- apply min_safe_alignment_safe; auto.
+- apply align_divides. apply min_safe_alignment_pos.
 Qed.
 
 Remark inj_offset_aligned_block':
   forall stacksize sz,
-  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz).
+  Mem.inj_offset_aligned (align stacksize (min_safe_alignment sz)) (Z.max 0 sz).
 Proof.
   intros.
-  replace (block_alignment sz) with (block_alignment (Z.max 0 sz)).
+  replace (min_safe_alignment sz) with (min_safe_alignment (Z.max 0 sz)).
   apply inj_offset_aligned_block.
   rewrite Zmax_spec. destruct (zlt sz 0); auto.
-  transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. lia.
+  transitivity 1. reflexivity. unfold min_safe_alignment. rewrite zlt_true. auto. lia.
 Qed.
 
 Lemma assign_variable_sound:
@@ -962,21 +940,22 @@ Lemma assign_variable_sound:
 Proof.
   unfold assign_variable; intros until vars; intros ASV NOREPET POS COMPAT SEP.
   inv ASV.
-  assert (LE: sz1 <= align sz1 (block_alignment sz)). apply align_le. apply block_alignment_pos.
+  assert (LE: sz1 <= align sz1 (min_safe_alignment sz)).
+  { apply align_le. apply min_safe_alignment_pos. }
   assert (EITHER: forall id' sz',
              In (id', sz') (vars ++ (id, sz) :: nil) ->
              In (id', sz') vars /\ id' <> id \/ (id', sz') = (id, sz)).
-    intros. rewrite in_app in H. destruct H.
+  { intros. rewrite in_app in H. destruct H.
     left; split; auto. red; intros; subst id'. elim NOREPET.
     change id with (fst (id, sz')). apply in_map; auto.
-    simpl in H. destruct H. auto. contradiction.
+    simpl in H. destruct H. auto. contradiction. }
   split; red; intros.
   apply EITHER in H. destruct H as [[P Q] | P].
   exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
   exists ofs.
   split. rewrite PTree.gso; auto.
   split. auto. split. auto. zify; lia.
-  inv P. exists (align sz1 (block_alignment sz)).
+  inv P. exists (align sz1 (min_safe_alignment sz)).
   split. apply PTree.gss.
   split. apply inj_offset_aligned_block.
   split. lia.
 
@@ -126,6 +126,39 @@ Proof.
         | exists 8; reflexivity ].
 Qed.
 
+(** Given the size [sz] of a block, [min_safe_alignment sz] is the minimum
+    alignment that guarantees that all valid memory accesses in the block
+    have at least this alignment.  *)
+
+Definition min_safe_alignment (sz: Z) : Z :=
+  if zlt sz 2 then 1
+  else if zlt sz 4 then 2
+  else if zlt sz 8 then 4 else 8.
+
+Lemma min_safe_alignment_pos: forall sz,
+  min_safe_alignment sz > 0.
+Proof.
+  intros; unfold min_safe_alignment. repeat (destruct zlt); lia.
+Qed.
+
+Lemma min_safe_alignment_safe: forall sz chunk,
+  size_chunk chunk <= sz -> (align_chunk chunk | min_safe_alignment sz).
+Proof.
+  intros.
+  generalize Z.divide_1_l Z.divide_refl; intros.
+  assert (2 | 4) by (exists 2; auto).
+  assert (2 | 8) by (exists 4; auto).
+  assert (4 | 8) by (exists 2; auto).
+  unfold size_chunk, align_chunk, min_safe_alignment in *.
+  destruct (zlt sz 2). destruct chunk; auto; lia.
+  destruct (zlt sz 4). destruct chunk; auto; lia.
+  destruct (zlt sz 8). destruct chunk; auto; lia.
+  destruct chunk; auto.
+Qed.
+
+(** Memory quantities are a coarser variant of memory chunks, used to represent
+    the size of a pointer (32 or 64 bits). *)
+
 Inductive quantity : Type := Q32 | Q64.
 
 Definition quantity_eq (q1 q2: quantity) : {q1 = q2} + {q1 <> q2}.