From 0dafd82e6106b63c7a6b14767b15fb8f50c01c71 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 2 Aug 2023 14:29:59 +0200
Subject: [PATCH] Revert "Allow configuring whether Caesium checks for
 alignment"

This reverts commit 4bd010b77812fc67d02a6e595440b24e54ea2ae2.
---
 Makefile                                  | 10 ---------
 theories/caesium/base.v                   |  1 -
 theories/caesium/config/config.v          | 26 -----------------------
 theories/caesium/config/default_config.v  |  9 --------
 theories/caesium/config/dune              |  6 ------
 theories/caesium/config/no_align_config.v |  9 --------
 theories/caesium/config/selected_config.v |  8 -------
 theories/caesium/loc.v                    | 25 +++++++++++-----------
 8 files changed, 12 insertions(+), 82 deletions(-)
 delete mode 100644 theories/caesium/config/config.v
 delete mode 100644 theories/caesium/config/default_config.v
 delete mode 100644 theories/caesium/config/dune
 delete mode 100644 theories/caesium/config/no_align_config.v
 delete mode 100644 theories/caesium/config/selected_config.v

diff --git a/Makefile b/Makefile
index 6e9ce42b..8578ceb3 100644
--- a/Makefile
+++ b/Makefile
@@ -56,16 +56,6 @@ builddep: builddep/refinedrust-builddep.opam
 
 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
diff --git a/theories/caesium/base.v b/theories/caesium/base.v
index 230a549c..47c4bbd6 100644
--- a/theories/caesium/base.v
+++ b/theories/caesium/base.v
@@ -1,5 +1,4 @@
 From lithium Require Export base.
-From caesium.config Require Export config.
 Set Default Proof Using "Type".
 
 Global Unset Program Cases.
diff --git a/theories/caesium/config/config.v b/theories/caesium/config/config.v
deleted file mode 100644
index 899dece0..00000000
--- a/theories/caesium/config/config.v
+++ /dev/null
@@ -1,26 +0,0 @@
-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.
diff --git a/theories/caesium/config/default_config.v b/theories/caesium/config/default_config.v
deleted file mode 100644
index acee1028..00000000
--- a/theories/caesium/config/default_config.v
+++ /dev/null
@@ -1,9 +0,0 @@
-
-(** 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.
diff --git a/theories/caesium/config/dune b/theories/caesium/config/dune
deleted file mode 100644
index cc61ed58..00000000
--- a/theories/caesium/config/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(coq.theory
- (name caesium.config)
- (package refinedrust)
- (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
- (synopsis "Configuration of the Caesium language")
- (theories ))
diff --git a/theories/caesium/config/no_align_config.v b/theories/caesium/config/no_align_config.v
deleted file mode 100644
index 4d1dcbcd..00000000
--- a/theories/caesium/config/no_align_config.v
+++ /dev/null
@@ -1,9 +0,0 @@
-
-(** 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.
diff --git a/theories/caesium/config/selected_config.v b/theories/caesium/config/selected_config.v
deleted file mode 100644
index 991ee801..00000000
--- a/theories/caesium/config/selected_config.v
+++ /dev/null
@@ -1,8 +0,0 @@
-
-(** 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.
diff --git a/theories/caesium/loc.v b/theories/caesium/loc.v
index 6072f269..8e9beb41 100644
--- a/theories/caesium/loc.v
+++ b/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 := if config.enforce_alignment then (n | l.2) else True.
+Definition aligned_to (l : loc) (n : nat) : Prop := (n | l.2).
 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.
-  rewrite /has_layout_loc/aligned_to. move => ??. case_match => //.
+  move => ??. rewrite /has_layout_loc.
   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 ?. case_match => //.
+  rewrite /has_layout_loc/aligned_to => Hl ?.
   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/aligned_to => ->. case_match => //. by apply Z.divide_1_l.
+  rewrite /has_layout_loc => ->. 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.
-  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.
+  move => Hl. apply Z.divide_add_r.
+  - apply: has_layout_loc_trans => //. 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,36 +170,35 @@ 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. rewrite /ly_mult/has_layout_loc/aligned_to. case_match => //. move => ??. by apply Z.divide_add_r. Qed.
+Proof. move => ??. rewrite /ly_mult. 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. rewrite /aligned_to. case_match => //. apply Z.divide_add_r. Qed.
+Proof. 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. case_match => //. destruct l => /=. rewrite Z.add_comm. split.
+  unfold aligned_to. 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:
-  config.enforce_alignment = true → l `aligned_to` n2 → (l +ₗ off) `aligned_to` (n1 * n2) → (n2 | off).
+  l `aligned_to` n2 → (l +ₗ off) `aligned_to` (n1 * n2) → (n2 | off).
 Proof.
-  unfold aligned_to. move => ->. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
+  unfold aligned_to. 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. rewrite /aligned_to. case_match; [|apply _]. apply Znumtheory.Zdivide_dec. Qed.
+Proof. apply Znumtheory.Zdivide_dec. Qed.
-- 
GitLab