Unfold more definitions in the side condition solver.

examples/proofs/spinlock/generated_code.v

@@ -12,35 +12,35 @@ Section code.
   Definition loc_4 : location_info := LocationInfo file_0 8 4 8 8.
   Definition loc_5 : location_info := LocationInfo file_0 8 4 8 8.
   Definition loc_6 : location_info := LocationInfo file_0 8 17 8 18.
-  Definition loc_9 : location_info := LocationInfo file_0 13 4 13 23.
-  Definition loc_10 : location_info := LocationInfo file_0 15 4 17 5.
-  Definition loc_11 : location_info := LocationInfo file_0 15 4 17 5.
-  Definition loc_12 : location_info := LocationInfo file_0 15 144 17 5.
-  Definition loc_13 : location_info := LocationInfo file_0 16 8 16 21.
-  Definition loc_14 : location_info := LocationInfo file_0 15 4 17 5.
-  Definition loc_15 : location_info := LocationInfo file_0 15 4 17 5.
-  Definition loc_16 : location_info := LocationInfo file_0 16 8 16 16.
-  Definition loc_17 : location_info := LocationInfo file_0 16 19 16 20.
-  Definition loc_18 : location_info := LocationInfo file_0 15 10 15 142.
-  Definition loc_19 : location_info := LocationInfo file_0 15 10 15 130.
-  Definition loc_20 : location_info := LocationInfo file_0 15 10 15 59.
-  Definition loc_21 : location_info := LocationInfo file_0 15 60 15 71.
-  Definition loc_22 : location_info := LocationInfo file_0 15 61 15 71.
-  Definition loc_23 : location_info := LocationInfo file_0 15 61 15 65.
-  Definition loc_24 : location_info := LocationInfo file_0 15 61 15 65.
-  Definition loc_25 : location_info := LocationInfo file_0 15 73 15 82.
-  Definition loc_26 : location_info := LocationInfo file_0 15 74 15 82.
-  Definition loc_27 : location_info := LocationInfo file_0 15 84 15 85.
-  Definition loc_28 : location_info := LocationInfo file_0 15 134 15 142.
-  Definition loc_29 : location_info := LocationInfo file_0 15 141 15 142.
-  Definition loc_30 : location_info := LocationInfo file_0 13 21 13 22.
-  Definition loc_35 : location_info := LocationInfo file_0 22 4 22 74.
-  Definition loc_36 : location_info := LocationInfo file_0 22 4 22 35.
-  Definition loc_37 : location_info := LocationInfo file_0 22 36 22 47.
-  Definition loc_38 : location_info := LocationInfo file_0 22 37 22 47.
-  Definition loc_39 : location_info := LocationInfo file_0 22 37 22 41.
-  Definition loc_40 : location_info := LocationInfo file_0 22 37 22 41.
-  Definition loc_41 : location_info := LocationInfo file_0 22 49 22 50.
+  Definition loc_9 : location_info := LocationInfo file_0 12 4 12 23.
+  Definition loc_10 : location_info := LocationInfo file_0 14 4 16 5.
+  Definition loc_11 : location_info := LocationInfo file_0 14 4 16 5.
+  Definition loc_12 : location_info := LocationInfo file_0 14 144 16 5.
+  Definition loc_13 : location_info := LocationInfo file_0 15 8 15 21.
+  Definition loc_14 : location_info := LocationInfo file_0 14 4 16 5.
+  Definition loc_15 : location_info := LocationInfo file_0 14 4 16 5.
+  Definition loc_16 : location_info := LocationInfo file_0 15 8 15 16.
+  Definition loc_17 : location_info := LocationInfo file_0 15 19 15 20.
+  Definition loc_18 : location_info := LocationInfo file_0 14 10 14 142.
+  Definition loc_19 : location_info := LocationInfo file_0 14 10 14 130.
+  Definition loc_20 : location_info := LocationInfo file_0 14 10 14 59.
+  Definition loc_21 : location_info := LocationInfo file_0 14 60 14 71.
+  Definition loc_22 : location_info := LocationInfo file_0 14 61 14 71.
+  Definition loc_23 : location_info := LocationInfo file_0 14 61 14 65.
+  Definition loc_24 : location_info := LocationInfo file_0 14 61 14 65.
+  Definition loc_25 : location_info := LocationInfo file_0 14 73 14 82.
+  Definition loc_26 : location_info := LocationInfo file_0 14 74 14 82.
+  Definition loc_27 : location_info := LocationInfo file_0 14 84 14 85.
+  Definition loc_28 : location_info := LocationInfo file_0 14 134 14 142.
+  Definition loc_29 : location_info := LocationInfo file_0 14 141 14 142.
+  Definition loc_30 : location_info := LocationInfo file_0 12 21 12 22.
+  Definition loc_35 : location_info := LocationInfo file_0 21 4 21 74.
+  Definition loc_36 : location_info := LocationInfo file_0 21 4 21 35.
+  Definition loc_37 : location_info := LocationInfo file_0 21 36 21 47.
+  Definition loc_38 : location_info := LocationInfo file_0 21 37 21 47.
+  Definition loc_39 : location_info := LocationInfo file_0 21 37 21 41.
+  Definition loc_40 : location_info := LocationInfo file_0 21 37 21 41.
+  Definition loc_41 : location_info := LocationInfo file_0 21 49 21 50.
 
   (* Definition of struct [atomic_flag]. *)
   Program Definition struct_atomic_flag := {|

examples/proofs/spinlock/generated_proof_sl_lock.v

@@ -30,7 +30,6 @@ Section proof_sl_lock.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "sl_lock" "#1".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: try by rewrite /bytes_per_int/=; have ->: bytes_per_addr = 8%nat; solve_goal.
     all: print_sidecondition_goal "sl_lock".
   Qed.
 End proof_sl_lock.

examples/spinlock.c

@@ -8,7 +8,6 @@ void sl_init(struct spinlock* lock) {
     lock->lock = 0;
 }
 
-[[rc::tactics("all: try by rewrite /bytes_per_int/=; have ->: bytes_per_addr = 8%nat; solve_goal.")]]
 void sl_lock(struct spinlock* lock) {
     bool expected = 0;
     [[rc::inv_vars("expected : false @ boolean<bool_it>")]]

theories/typing/automation/solvers.v

@@ -162,10 +162,22 @@ Lemma unfold_int_elem_of_it (z : Z) (it : int_type) :
   z ∈ it = (min_int it ≤ z ∧ z ≤ max_int it).
 Proof. done. Qed.
 
+Ltac unfold_common_defs :=
+  unfold
+  (* Layout *)
+    ly_size, ly_with_align, ly_align_log,
+  (* Integer bounds *)
+    max_int, min_int, int_half_modulus, int_modulus,
+    bits_per_int, bytes_per_int,
+  (* Address bounds *)
+    max_alloc_end, min_alloc_start, bytes_per_addr,
+  (* Other byte-level definitions *)
+    bits_per_byte in *.
+
 (** * [solve_goal] without cleaning of the context  *)
 Ltac unprepared_solve_goal :=
   try rewrite -> unfold_int_elem_of_it in *;
-  unfold ly_size, ly_align_log, max_int, min_int, int_half_modulus, int_modulus in *; simpl in *;
+  unfold_common_defs; simpl in *;
   normalize_and_simpl_goal;
   rewrite /ly_size/ly_align_log //=; enrich_context;
   repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //;