Allow configuring whether Caesium checks for alignment

Makefile

@@ -55,3 +55,18 @@ builddep: builddep/refinedrust-builddep.opam
 .PHONY: builddep
 
 DUNE_FILES = $(shell find theories/ -type f -name 'dune')
+
+config:
+	@echo "# Setting default configuration"
+	@cp theories/caesium/config/default_config.v theories/caesium/config/selected_config.v
+.PHONY: config
+
+config-no-align:
+	@echo "# Setting no-align configuration"
+	@cp theories/caesium/config/no_align_config.v theories/caesium/config/selected_config.v
+.PHONY: config-no-align
+
+# Currently, we don't need to do anything special before building RefinedC in opam.
+prepare-install-refinedrust:
+	@true
+.PHONY: prepare-install-refinedrust

refinedrust.opam

@@ -17,7 +17,8 @@ depends: [
 ]
 
 build: [
-  [make "prepare-install-refinedc"]
+  [make "prepare-install-refinedrust"]
+  [make "config%{caesium-config}%"]
   ["dune" "subst"] {pinned}
   ["dune" "build" "-p" name "-j" jobs]
 ]

theories/caesium/base.v

 From lithium Require Export base.
+From caesium.config Require Export config.
 Set Default Proof Using "Type".
 
 Global Unset Program Cases.

theories/caesium/config/config.v

+From caesium.config Require Import selected_config.
+
+(** Compile time configuration for Caesium.
+
+NOTE: Do not modify selected_config.v! Instead modify the original
+configuration file and then use the Makefile to set the desired
+configuration. *)
+
+Module Type config_sig.
+  (** Should Caesium check that all pointers are well-aligned? *)
+  Parameter enforce_alignment : bool.
+
+  Axiom enforce_alignment_value : enforce_alignment = selected_config.enforce_alignment.
+End config_sig.
+
+Module config : config_sig.
+  Definition enforce_alignment : bool := selected_config.enforce_alignment.
+  Lemma enforce_alignment_value : enforce_alignment = selected_config.enforce_alignment.
+  Proof. reflexivity. Qed.
+End config.
+
+Class ConfigEnforceAlignment : Prop :=
+  config_enforce_alignment : config.enforce_alignment = true.
+
+Global Hint Extern 0 (ConfigEnforceAlignment) =>
+   (exact config.enforce_alignment_value) : typeclass_instances.

theories/caesium/config/default_config.v

+
+(** Default configuration for Caesium.
+
+NOTE: Do not modify selected_config.v! Instead modify the original
+configuration file and then use the Makefile to set the desired
+configuration. *)
+
+(** See config.v for explanation of the different configurations. *)
+Definition enforce_alignment : bool := true.

theories/caesium/config/dune

+(coq.theory
+ (name caesium.config)
+ (package refinedrust)
+ (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
+ (synopsis "Configuration of the Caesium language")
+ (theories ))

theories/caesium/config/no_align_config.v

+
+(** Configuration for Caesium that disables alignment checking.
+
+NOTE: Do not modify selected_config.v! Instead modify the original
+configuration file and then use the Makefile to set the desired
+configuration. *)
+
+(** See config.v for explanation of the different configurations. *)
+Definition enforce_alignment : bool := false.

theories/caesium/config/selected_config.v

+
+(** Default configuration for Caesium.
+
+NOTE: Do not modify selected_config.v! Instead modify the original
+configuration file and then use the Makefile to set the desired
+configuration. *)
+
+Definition enforce_alignment : bool := true.

theories/caesium/loc.v

@@ -66,7 +66,7 @@ Notation "l 'offset{' ly '}ₗ' z" := (offset_loc l%L ly z%Z)
 Global Typeclasses Opaque offset_loc.
 
 (** Proposition stating that location [l] is aligned to [n] *)
-Definition aligned_to (l : loc) (n : nat) : Prop := (n | l.2).
+Definition aligned_to (l : loc) (n : nat) : Prop := if config.enforce_alignment then (n | l.2) else True.
 Notation "l `aligned_to` n" := (aligned_to l n) (at level 50) : stdpp_scope.
 Arguments aligned_to : simpl never.
 Global Typeclasses Opaque aligned_to.
@@ -127,7 +127,7 @@ Lemma ly_with_align_aligned_to l m n:
   is_power_of_two n →
   l `has_layout_loc` ly_with_align m n.
 Proof.
-  move => ??. rewrite /has_layout_loc.
+  rewrite /has_layout_loc/aligned_to. move => ??. case_match => //.
   by rewrite ly_align_ly_with_align keep_factor2_is_power_of_two.
 Qed.
 
@@ -136,7 +136,7 @@ Lemma has_layout_loc_trans l ly1 ly2 :
   (ly1.(ly_align_log) ≤ ly2.(ly_align_log))%nat →
   l `has_layout_loc` ly1.
 Proof.
-  rewrite /has_layout_loc/aligned_to => Hl ?.
+  rewrite /has_layout_loc/aligned_to => Hl ?. case_match => //.
   etrans;[|by apply Hl]. by apply Zdivide_nat_pow.
 Qed.
 
@@ -153,15 +153,15 @@ Lemma has_layout_loc_1 l ly:
   ly_align ly = 1%nat →
   l `has_layout_loc` ly.
 Proof.
-  rewrite /has_layout_loc => ->. by apply Z.divide_1_l.
+  rewrite /has_layout_loc/aligned_to => ->. case_match => //. by apply Z.divide_1_l.
 Qed.
 
 Lemma has_layout_ly_offset l (n : nat) ly:
   l `has_layout_loc` ly →
   (l +ₗ n) `has_layout_loc` ly_offset ly n.
 Proof.
-  move => Hl. apply Z.divide_add_r.
-  - apply: has_layout_loc_trans => //. rewrite {1}/ly_align_log/=. destruct n; lia.
+  rewrite/has_layout_loc/aligned_to. case_match => //. move => Hl. apply Z.divide_add_r.
+  - etrans;[|by apply Hl]. apply Zdivide_nat_pow. rewrite {1}/ly_align_log/=. destruct n; lia.
   - rewrite/ly_offset. destruct n;[by subst;apply Z.divide_0_r|].
     etrans;[apply Zdivide_nat_pow, Nat.le_min_r|]. by apply factor2_divide.
 Qed.
@@ -170,35 +170,36 @@ Lemma has_layout_loc_ly_mult_offset l ly n:
   layout_wf ly →
   l `has_layout_loc` ly_mult ly (S n) →
   (l +ₗ ly_size ly) `has_layout_loc` ly_mult ly n.
-Proof. move => ??. rewrite /ly_mult. by apply Z.divide_add_r. Qed.
+Proof. rewrite /ly_mult/has_layout_loc/aligned_to. case_match => //. move => ??. by apply Z.divide_add_r. Qed.
 
 Lemma has_layout_loc_offset_loc l i ly:
   layout_wf ly →
   l `has_layout_loc` ly →
   (l offset{ly}ₗ i) `has_layout_loc` ly.
 Proof.
+  rewrite/has_layout_loc/aligned_to. case_match => //.
   move => Hwf Hl. apply Z.divide_add_r; [done|]. etrans; [by apply: Hwf|].
   apply: Z.divide_factor_l.
 Qed.
 
 Lemma aligned_to_offset l n off :
   l `aligned_to` n → (n | off) → (l +ₗ off) `aligned_to` n.
-Proof. apply Z.divide_add_r. Qed.
+Proof. rewrite /aligned_to. case_match => //. apply Z.divide_add_r. Qed.
 
 Lemma aligned_to_add l (n : nat) x:
   (l +ₗ x * n) `aligned_to` n ↔ l `aligned_to` n.
 Proof.
-  unfold aligned_to. destruct l => /=. rewrite Z.add_comm. split.
+  unfold aligned_to. case_match => //. destruct l => /=. rewrite Z.add_comm. split.
   - apply: Z.divide_add_cancel_r. by apply Z.divide_mul_r.
   - apply Z.divide_add_r. by apply Z.divide_mul_r.
 Qed.
 
 Lemma aligned_to_mult_eq l n1 n2 off:
-  l `aligned_to` n2 → (l +ₗ off) `aligned_to` (n1 * n2) → (n2 | off).
+  config.enforce_alignment = true → l `aligned_to` n2 → (l +ₗ off) `aligned_to` (n1 * n2) → (n2 | off).
 Proof.
-  unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
+  unfold aligned_to. move => ->. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
   apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
 Qed.
 
 #[export] Instance aligned_to_dec l n : Decision (l `aligned_to` n).
-Proof. apply Znumtheory.Zdivide_dec. Qed.
+Proof. rewrite /aligned_to. case_match; [|apply _]. apply Znumtheory.Zdivide_dec. Qed.