make subsumption on uninit more complete

examples/malloc1.c

@@ -52,6 +52,7 @@ void slab_init(struct slab *s, unsigned char *p, size_t chunksize, size_t entry_
 [[rc::args("p @ &own<n @ slab<entry_size>>")]]
 [[rc::returns("{(0 < n)%nat} @ optional<&own<uninit<{ly_with_align entry_size entry_size}>>>")]]
 [[rc::ensures("own p : {(n - 1)%nat} @ slab<entry_size>")]]
+ [[rc::tactics("all: try by apply: has_layout_loc_trans'; solve_goal.")]]
 void* slab_alloc(struct slab *s)
 {
     struct freelist *f;

examples/mpool.c

@@ -354,7 +354,7 @@ void mpool_free(struct mpool *p, void *ptr) {
 [[rc::exists("n2 : nat")]]
 [[rc::returns("optional<&own<uninit<{ly_with_align (count * entry_size) (align * entry_size)}>>>")]]
 [[rc::ensures("frac q p : n2 @ mpool<entry_size>", "{q = Own → n2 <= n}")]]
-  [[rc::tactics("all: try (etrans; [eassumption|]); repeat progress rewrite /ly_size/=.")]]
+  [[rc::tactics("all: try (etrans; [eassumption|]); repeat progress rewrite /has_layout_loc/ly_size/=.")]]
   [[rc::tactics("all: rewrite -?Nat.mul_sub_distr_r; try apply: mult_le_compat_r; try apply mult_le_compat_r_1.")]]
   [[rc::tactics("all: try by destruct o'; solve_goal.")]]
 void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t align)
@@ -421,7 +421,6 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
         chunk->size = before_start;
       }
 
-      rc_uninit_strengthen_align(*start);
       ret = (void *)start;
       break;
     }

examples/proofs/malloc1/generated_code.v

@@ -29,102 +29,102 @@ Section code.
   Definition loc_22 : location_info := LocationInfo file_0 45 4 45 5.
   Definition loc_23 : location_info := LocationInfo file_0 45 15 45 16.
   Definition loc_24 : location_info := LocationInfo file_0 45 15 45 16.
-  Definition loc_27 : location_info := LocationInfo file_0 59 4 73 5.
-  Definition loc_28 : location_info := LocationInfo file_0 59 35 64 5.
-  Definition loc_29 : location_info := LocationInfo file_0 60 8 60 20.
-  Definition loc_30 : location_info := LocationInfo file_0 61 8 61 26.
-  Definition loc_31 : location_info := LocationInfo file_0 62 8 62 14.
-  Definition loc_32 : location_info := LocationInfo file_0 63 8 63 17.
-  Definition loc_33 : location_info := LocationInfo file_0 63 15 63 16.
-  Definition loc_34 : location_info := LocationInfo file_0 63 15 63 16.
-  Definition loc_35 : location_info := LocationInfo file_0 62 8 62 9.
-  Definition loc_36 : location_info := LocationInfo file_0 62 12 62 13.
-  Definition loc_37 : location_info := LocationInfo file_0 62 12 62 13.
-  Definition loc_38 : location_info := LocationInfo file_0 61 8 61 15.
-  Definition loc_39 : location_info := LocationInfo file_0 61 8 61 9.
-  Definition loc_40 : location_info := LocationInfo file_0 61 8 61 9.
-  Definition loc_41 : location_info := LocationInfo file_0 61 18 61 25.
-  Definition loc_42 : location_info := LocationInfo file_0 61 18 61 25.
-  Definition loc_43 : location_info := LocationInfo file_0 61 18 61 19.
-  Definition loc_44 : location_info := LocationInfo file_0 61 18 61 19.
-  Definition loc_45 : location_info := LocationInfo file_0 60 8 60 9.
-  Definition loc_46 : location_info := LocationInfo file_0 60 12 60 19.
-  Definition loc_47 : location_info := LocationInfo file_0 60 12 60 19.
-  Definition loc_48 : location_info := LocationInfo file_0 60 12 60 13.
-  Definition loc_49 : location_info := LocationInfo file_0 60 12 60 13.
-  Definition loc_50 : location_info := LocationInfo file_0 64 11 73 5.
-  Definition loc_51 : location_info := LocationInfo file_0 65 8 72 9.
-  Definition loc_52 : location_info := LocationInfo file_0 65 42 67 9.
-  Definition loc_53 : location_info := LocationInfo file_0 66 12 66 34.
-  Definition loc_54 : location_info := LocationInfo file_0 66 19 66 33.
-  Definition loc_55 : location_info := LocationInfo file_0 67 15 72 9.
-  Definition loc_56 : location_info := LocationInfo file_0 68 12 68 25.
-  Definition loc_57 : location_info := LocationInfo file_0 69 12 69 48.
-  Definition loc_58 : location_info := LocationInfo file_0 70 12 70 56.
-  Definition loc_59 : location_info := LocationInfo file_0 71 12 71 21.
-  Definition loc_60 : location_info := LocationInfo file_0 71 19 71 20.
-  Definition loc_61 : location_info := LocationInfo file_0 71 19 71 20.
-  Definition loc_62 : location_info := LocationInfo file_0 70 12 70 24.
-  Definition loc_63 : location_info := LocationInfo file_0 70 12 70 13.
-  Definition loc_64 : location_info := LocationInfo file_0 70 12 70 13.
-  Definition loc_65 : location_info := LocationInfo file_0 70 27 70 55.
-  Definition loc_66 : location_info := LocationInfo file_0 70 27 70 39.
-  Definition loc_67 : location_info := LocationInfo file_0 70 27 70 39.
-  Definition loc_68 : location_info := LocationInfo file_0 70 27 70 28.
-  Definition loc_69 : location_info := LocationInfo file_0 70 27 70 28.
-  Definition loc_70 : location_info := LocationInfo file_0 70 42 70 55.
-  Definition loc_71 : location_info := LocationInfo file_0 70 42 70 55.
-  Definition loc_72 : location_info := LocationInfo file_0 70 42 70 43.
-  Definition loc_73 : location_info := LocationInfo file_0 70 42 70 43.
-  Definition loc_74 : location_info := LocationInfo file_0 69 12 69 20.
-  Definition loc_75 : location_info := LocationInfo file_0 69 12 69 13.
-  Definition loc_76 : location_info := LocationInfo file_0 69 12 69 13.
-  Definition loc_77 : location_info := LocationInfo file_0 69 23 69 47.
-  Definition loc_78 : location_info := LocationInfo file_0 69 23 69 31.
-  Definition loc_79 : location_info := LocationInfo file_0 69 23 69 31.
-  Definition loc_80 : location_info := LocationInfo file_0 69 23 69 24.
-  Definition loc_81 : location_info := LocationInfo file_0 69 23 69 24.
-  Definition loc_82 : location_info := LocationInfo file_0 69 34 69 47.
-  Definition loc_83 : location_info := LocationInfo file_0 69 34 69 47.
-  Definition loc_84 : location_info := LocationInfo file_0 69 34 69 35.
-  Definition loc_85 : location_info := LocationInfo file_0 69 34 69 35.
-  Definition loc_86 : location_info := LocationInfo file_0 68 12 68 13.
-  Definition loc_87 : location_info := LocationInfo file_0 68 16 68 24.
-  Definition loc_88 : location_info := LocationInfo file_0 68 16 68 24.
-  Definition loc_89 : location_info := LocationInfo file_0 68 16 68 17.
-  Definition loc_90 : location_info := LocationInfo file_0 68 16 68 17.
-  Definition loc_91 : location_info := LocationInfo file_0 65 12 65 40.
-  Definition loc_92 : location_info := LocationInfo file_0 65 12 65 25.
-  Definition loc_93 : location_info := LocationInfo file_0 65 12 65 25.
-  Definition loc_94 : location_info := LocationInfo file_0 65 12 65 13.
-  Definition loc_95 : location_info := LocationInfo file_0 65 12 65 13.
-  Definition loc_96 : location_info := LocationInfo file_0 65 28 65 40.
-  Definition loc_97 : location_info := LocationInfo file_0 65 28 65 40.
-  Definition loc_98 : location_info := LocationInfo file_0 65 28 65 29.
-  Definition loc_99 : location_info := LocationInfo file_0 65 28 65 29.
-  Definition loc_100 : location_info := LocationInfo file_0 59 8 59 33.
-  Definition loc_101 : location_info := LocationInfo file_0 59 8 59 15.
-  Definition loc_102 : location_info := LocationInfo file_0 59 8 59 15.
-  Definition loc_103 : location_info := LocationInfo file_0 59 8 59 9.
-  Definition loc_104 : location_info := LocationInfo file_0 59 8 59 9.
-  Definition loc_105 : location_info := LocationInfo file_0 59 19 59 33.
-  Definition loc_108 : location_info := LocationInfo file_0 81 4 81 27.
-  Definition loc_109 : location_info := LocationInfo file_0 83 4 83 22.
-  Definition loc_110 : location_info := LocationInfo file_0 84 4 84 16.
-  Definition loc_111 : location_info := LocationInfo file_0 84 4 84 11.
-  Definition loc_112 : location_info := LocationInfo file_0 84 4 84 5.
-  Definition loc_113 : location_info := LocationInfo file_0 84 4 84 5.
-  Definition loc_114 : location_info := LocationInfo file_0 84 14 84 15.
-  Definition loc_115 : location_info := LocationInfo file_0 84 14 84 15.
-  Definition loc_116 : location_info := LocationInfo file_0 83 4 83 11.
-  Definition loc_117 : location_info := LocationInfo file_0 83 4 83 5.
-  Definition loc_118 : location_info := LocationInfo file_0 83 4 83 5.
-  Definition loc_119 : location_info := LocationInfo file_0 83 14 83 21.
-  Definition loc_120 : location_info := LocationInfo file_0 83 14 83 21.
-  Definition loc_121 : location_info := LocationInfo file_0 83 14 83 15.
-  Definition loc_122 : location_info := LocationInfo file_0 83 14 83 15.
-  Definition loc_123 : location_info := LocationInfo file_0 81 25 81 26.
-  Definition loc_124 : location_info := LocationInfo file_0 81 25 81 26.
+  Definition loc_27 : location_info := LocationInfo file_0 60 4 74 5.
+  Definition loc_28 : location_info := LocationInfo file_0 60 35 65 5.
+  Definition loc_29 : location_info := LocationInfo file_0 61 8 61 20.
+  Definition loc_30 : location_info := LocationInfo file_0 62 8 62 26.
+  Definition loc_31 : location_info := LocationInfo file_0 63 8 63 14.
+  Definition loc_32 : location_info := LocationInfo file_0 64 8 64 17.
+  Definition loc_33 : location_info := LocationInfo file_0 64 15 64 16.
+  Definition loc_34 : location_info := LocationInfo file_0 64 15 64 16.
+  Definition loc_35 : location_info := LocationInfo file_0 63 8 63 9.
+  Definition loc_36 : location_info := LocationInfo file_0 63 12 63 13.
+  Definition loc_37 : location_info := LocationInfo file_0 63 12 63 13.
+  Definition loc_38 : location_info := LocationInfo file_0 62 8 62 15.
+  Definition loc_39 : location_info := LocationInfo file_0 62 8 62 9.
+  Definition loc_40 : location_info := LocationInfo file_0 62 8 62 9.
+  Definition loc_41 : location_info := LocationInfo file_0 62 18 62 25.
+  Definition loc_42 : location_info := LocationInfo file_0 62 18 62 25.
+  Definition loc_43 : location_info := LocationInfo file_0 62 18 62 19.
+  Definition loc_44 : location_info := LocationInfo file_0 62 18 62 19.
+  Definition loc_45 : location_info := LocationInfo file_0 61 8 61 9.
+  Definition loc_46 : location_info := LocationInfo file_0 61 12 61 19.
+  Definition loc_47 : location_info := LocationInfo file_0 61 12 61 19.
+  Definition loc_48 : location_info := LocationInfo file_0 61 12 61 13.
+  Definition loc_49 : location_info := LocationInfo file_0 61 12 61 13.
+  Definition loc_50 : location_info := LocationInfo file_0 65 11 74 5.
+  Definition loc_51 : location_info := LocationInfo file_0 66 8 73 9.
+  Definition loc_52 : location_info := LocationInfo file_0 66 42 68 9.
+  Definition loc_53 : location_info := LocationInfo file_0 67 12 67 34.
+  Definition loc_54 : location_info := LocationInfo file_0 67 19 67 33.
+  Definition loc_55 : location_info := LocationInfo file_0 68 15 73 9.
+  Definition loc_56 : location_info := LocationInfo file_0 69 12 69 25.
+  Definition loc_57 : location_info := LocationInfo file_0 70 12 70 48.
+  Definition loc_58 : location_info := LocationInfo file_0 71 12 71 56.
+  Definition loc_59 : location_info := LocationInfo file_0 72 12 72 21.
+  Definition loc_60 : location_info := LocationInfo file_0 72 19 72 20.
+  Definition loc_61 : location_info := LocationInfo file_0 72 19 72 20.
+  Definition loc_62 : location_info := LocationInfo file_0 71 12 71 24.
+  Definition loc_63 : location_info := LocationInfo file_0 71 12 71 13.
+  Definition loc_64 : location_info := LocationInfo file_0 71 12 71 13.
+  Definition loc_65 : location_info := LocationInfo file_0 71 27 71 55.
+  Definition loc_66 : location_info := LocationInfo file_0 71 27 71 39.
+  Definition loc_67 : location_info := LocationInfo file_0 71 27 71 39.
+  Definition loc_68 : location_info := LocationInfo file_0 71 27 71 28.
+  Definition loc_69 : location_info := LocationInfo file_0 71 27 71 28.
+  Definition loc_70 : location_info := LocationInfo file_0 71 42 71 55.
+  Definition loc_71 : location_info := LocationInfo file_0 71 42 71 55.
+  Definition loc_72 : location_info := LocationInfo file_0 71 42 71 43.
+  Definition loc_73 : location_info := LocationInfo file_0 71 42 71 43.
+  Definition loc_74 : location_info := LocationInfo file_0 70 12 70 20.
+  Definition loc_75 : location_info := LocationInfo file_0 70 12 70 13.
+  Definition loc_76 : location_info := LocationInfo file_0 70 12 70 13.
+  Definition loc_77 : location_info := LocationInfo file_0 70 23 70 47.
+  Definition loc_78 : location_info := LocationInfo file_0 70 23 70 31.
+  Definition loc_79 : location_info := LocationInfo file_0 70 23 70 31.
+  Definition loc_80 : location_info := LocationInfo file_0 70 23 70 24.
+  Definition loc_81 : location_info := LocationInfo file_0 70 23 70 24.
+  Definition loc_82 : location_info := LocationInfo file_0 70 34 70 47.
+  Definition loc_83 : location_info := LocationInfo file_0 70 34 70 47.
+  Definition loc_84 : location_info := LocationInfo file_0 70 34 70 35.
+  Definition loc_85 : location_info := LocationInfo file_0 70 34 70 35.
+  Definition loc_86 : location_info := LocationInfo file_0 69 12 69 13.
+  Definition loc_87 : location_info := LocationInfo file_0 69 16 69 24.
+  Definition loc_88 : location_info := LocationInfo file_0 69 16 69 24.
+  Definition loc_89 : location_info := LocationInfo file_0 69 16 69 17.
+  Definition loc_90 : location_info := LocationInfo file_0 69 16 69 17.
+  Definition loc_91 : location_info := LocationInfo file_0 66 12 66 40.
+  Definition loc_92 : location_info := LocationInfo file_0 66 12 66 25.
+  Definition loc_93 : location_info := LocationInfo file_0 66 12 66 25.
+  Definition loc_94 : location_info := LocationInfo file_0 66 12 66 13.
+  Definition loc_95 : location_info := LocationInfo file_0 66 12 66 13.
+  Definition loc_96 : location_info := LocationInfo file_0 66 28 66 40.
+  Definition loc_97 : location_info := LocationInfo file_0 66 28 66 40.
+  Definition loc_98 : location_info := LocationInfo file_0 66 28 66 29.
+  Definition loc_99 : location_info := LocationInfo file_0 66 28 66 29.
+  Definition loc_100 : location_info := LocationInfo file_0 60 8 60 33.
+  Definition loc_101 : location_info := LocationInfo file_0 60 8 60 15.
+  Definition loc_102 : location_info := LocationInfo file_0 60 8 60 15.
+  Definition loc_103 : location_info := LocationInfo file_0 60 8 60 9.
+  Definition loc_104 : location_info := LocationInfo file_0 60 8 60 9.
+  Definition loc_105 : location_info := LocationInfo file_0 60 19 60 33.
+  Definition loc_108 : location_info := LocationInfo file_0 82 4 82 27.
+  Definition loc_109 : location_info := LocationInfo file_0 84 4 84 22.
+  Definition loc_110 : location_info := LocationInfo file_0 85 4 85 16.
+  Definition loc_111 : location_info := LocationInfo file_0 85 4 85 11.
+  Definition loc_112 : location_info := LocationInfo file_0 85 4 85 5.
+  Definition loc_113 : location_info := LocationInfo file_0 85 4 85 5.
+  Definition loc_114 : location_info := LocationInfo file_0 85 14 85 15.
+  Definition loc_115 : location_info := LocationInfo file_0 85 14 85 15.
+  Definition loc_116 : location_info := LocationInfo file_0 84 4 84 11.
+  Definition loc_117 : location_info := LocationInfo file_0 84 4 84 5.
+  Definition loc_118 : location_info := LocationInfo file_0 84 4 84 5.
+  Definition loc_119 : location_info := LocationInfo file_0 84 14 84 21.
+  Definition loc_120 : location_info := LocationInfo file_0 84 14 84 21.
+  Definition loc_121 : location_info := LocationInfo file_0 84 14 84 15.
+  Definition loc_122 : location_info := LocationInfo file_0 84 14 84 15.
+  Definition loc_123 : location_info := LocationInfo file_0 82 25 82 26.
+  Definition loc_124 : location_info := LocationInfo file_0 82 25 82 26.
 
   (* Definition of struct [freelist]. *)
   Program Definition struct_freelist := {|

examples/proofs/malloc1/generated_proof_slab_alloc.v

@@ -21,6 +21,7 @@ Section proof_slab_alloc.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "slab_alloc" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: try by apply: has_layout_loc_trans'; solve_goal.
     all: print_sidecondition_goal "slab_alloc".
   Qed.
 End proof_slab_alloc.

examples/proofs/mpool/generated_proof_mpool_alloc_contiguous_no_fallback.v

@@ -45,7 +45,7 @@ Section proof_mpool_alloc_contiguous_no_fallback.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "mpool_alloc_contiguous_no_fallback" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: try (etrans; [eassumption|]); repeat progress rewrite /ly_size/=.
+    all: try (etrans; [eassumption|]); repeat progress rewrite /has_layout_loc/ly_size/=.
     all: rewrite -?Nat.mul_sub_distr_r; try apply: mult_le_compat_r; try apply mult_le_compat_r_1.
     all: try by destruct o'; solve_goal.
     all: print_sidecondition_goal "mpool_alloc_contiguous_no_fallback".

include/refinedc.h

@@ -21,7 +21,6 @@
 
 #define rc_unlock(e) rc_annot(e, "UnlockA")
 #define rc_to_uninit(e) rc_annot(e, "ToUninit")
-#define rc_uninit_strengthen_align(e) rc_annot(e, "UninitStrengthenAlign")
 #define rc_stop(e) rc_annot(e, "StopAnnot")
 #define rc_share(e) rc_annot(e, "ShareAnnot")
 #define rc_unfold_once(e) rc_annot(e, "UnfoldOnceAnnot")

theories/lang/base.v

@@ -547,9 +547,9 @@ Lemma keep_factor2_is_power_of_two n x:
   keep_factor2 n x = n.
 Proof. move => [? ->]. by rewrite /keep_factor2 factor2'_pow. Qed.
 
-Lemma keep_factor2_min_eq (n m : nat):
+Lemma keep_factor2_leq (n m : nat):
   is_power_of_two n → (n | m) →
-  (n `min` keep_factor2 m n) = n.
+  n ≤ keep_factor2 m n.
 Proof.
   move => ? [o ->]. destruct (decide (o = 0)); first by subst; rewrite keep_factor2_0; lia.
   destruct (decide (n = 0)); first lia.
@@ -558,12 +558,17 @@ Proof.
   destruct (keep_factor2 o n); lia.
 Qed.
 
+Lemma keep_factor2_min_eq (n m : nat):
+  is_power_of_two n → (n | m) →
+  (n `min` keep_factor2 m n) = n.
+Proof. move => ??. apply: Nat.min_l. by apply: keep_factor2_leq. Qed.
+
 Lemma keep_factor2_min_1 n:
-  (1 `min` keep_factor2 n 1)%nat = 1%nat.
+  1 `min` keep_factor2 n 1 = 1.
 Proof.
   rewrite /keep_factor2 /factor2'. destruct (N.of_nat n) => // /=.
-  apply Nat.min_l. generalize (Pos_factor2 p) => k. induction k as [|k IH].
-  done. rewrite Nat.pow_succ_r'. move: IH. generalize (2 ^ k) => j. lia.
+  apply Nat.min_l. generalize (Pos_factor2 p) => k. induction k as [|k IH] => //.
+  rewrite Nat.pow_succ_r'. lia.
 Qed.
 
 Lemma keep_factor2_twice n m:

theories/lang/lang.v

@@ -616,6 +616,10 @@ Lemma ly_align_log_ly_align_eq_iff ly1 ly2:
   ly_align_log ly1 = ly_align_log ly2 ↔ ly_align ly1 = ly_align ly2.
 Proof. rewrite /ly_align. split; first naive_solver. move => /Nat.pow_inj_r. lia. Qed.
 
+Lemma ly_align_log_ly_align_le_iff ly1 ly2:
+  (ly_align_log ly1 ≤ ly_align_log ly2 ↔ ly_align ly1 ≤ ly_align ly2)%nat.
+Proof. rewrite /ly_align. apply: Nat.pow_le_mono_r_iff. lia. Qed.
+
 Lemma ly_align_ly_with_align m n :
   ly_align (ly_with_align m n) = keep_factor2 n 1.
 Proof. rewrite /ly_with_align/keep_factor2/factor2. by destruct (factor2' n). Qed.
@@ -646,6 +650,10 @@ Lemma has_layout_loc_trans l ly1 ly2 :
   l `has_layout_loc` ly2 → (ly1.(ly_align_log) ≤ ly2.(ly_align_log))%nat → l `has_layout_loc` ly1.
 Proof. rewrite /has_layout_loc/aligned_to => Hl ?. etrans;[|by apply Hl]. by apply Zdivide_nat_pow. Qed.
 
+Lemma has_layout_loc_trans' l ly1 ly2 :
+  l `has_layout_loc` ly2 → (ly_align ly1 ≤ ly_align ly2)%nat → l `has_layout_loc` ly1.
+Proof. rewrite -ly_align_log_ly_align_le_iff. by apply: has_layout_loc_trans. Qed.
+
 Lemma has_layout_loc_1 l ly:
   ly_align ly = 1%nat →
   l `has_layout_loc` ly.

theories/lithium/simpl_instances.v

@@ -69,6 +69,15 @@ Proof. split; destruct b; naive_solver. Qed.
 Global Instance simpl_Is_true_false b : SimplBoth (¬ Is_true b) (b = false).
 Proof. split; destruct b; naive_solver. Qed.
 
+Global Instance simpl_min_glb_nat n1 n2 m : SimplBoth (m ≤ n1 `min` n2)%nat (m ≤ n1 ∧ m ≤ n2)%nat.
+Proof. rewrite /SimplBoth. lia. Qed.
+Global Instance simpl_min_glb n1 n2 m : SimplBoth (m ≤ n1 `min` n2) (m ≤ n1 ∧ m ≤ n2).
+Proof. rewrite /SimplBoth. lia. Qed.
+Global Instance simpl_max_glb_nat n1 n2 m : SimplBoth (n1 `max` n2 ≤ m)%nat (n1 ≤ m ∧ n2 ≤ m)%nat.
+Proof. rewrite /SimplBoth. lia. Qed.
+Global Instance simpl_max_glb n1 n2 m : SimplBoth (n1 `max` n2 ≤ m) (n1 ≤ m ∧ n2 ≤ m).
+Proof. rewrite /SimplBoth. lia. Qed.
+
 Global Instance simpl_gt_both (n1 n2 : nat) `{!CanSolve (n1 ≠ 0)%nat} : SimplBoth (n1 > n2 * n1) (n2 = 0%nat).
 Proof. unfold CanSolve in *; split; destruct n2; naive_solver lia. Qed.
 Global Instance simpl_ge_both (n1 n2 : nat) `{!CanSolve (n1 ≠ 0)%nat} : SimplBoth (n1 >= n2 * n1) (n2 = 0 ∨ n2 = 1)%nat.
@@ -126,6 +135,9 @@ Qed.
 Global Instance simpl_cancel_mult_nat n1 n2 m `{!CanSolve (m ≠ 0)%nat}:
   SimplBothRel (=) (n1 * m)%nat (n2 * m)%nat (n1 = n2)%nat.
 Proof. unfold SimplBothRel. unfold CanSolve in *. by rewrite Nat.mul_cancel_r. Qed.
+Global Instance simpl_cancel_mult_nat_1 n m `{!CanSolve (m ≠ 0)%nat}:
+  SimplBothRel (=) (n * m)%nat m (n = 1)%nat.
+Proof. unfold SimplBothRel. unfold CanSolve in *. nia. Qed.
 Global Instance simpl_cancel_mult_le n1 n2 m `{!CanSolve (0 < m)}:
   SimplBothRel (≤) (n1 * m) (n2 * m) (n1 ≤ n2).
 Proof. unfold SimplBothRel. unfold CanSolve in *. by rewrite -Z.mul_le_mono_pos_r. Qed.

theories/typing/annotations.v

@@ -3,9 +3,6 @@ From refinedc.typing Require Import base.
 Inductive to_uninit_annot : Type :=
   ToUninit.
 
-Inductive uninit_strengthen_align_annot : Type :=
-  UninitStrengthenAlign.
-
 Inductive stop_annot : Type :=
   StopAnnot.
 

theories/typing/padded.v

@@ -104,24 +104,24 @@ Section padded.
 
   (* Only works for Own since ty might have interior mutability, but
   uninit ty assumes that the values are frozen *)
-  Lemma subsume_padded_uninit l ly lyty ty `{!Movable ty} T:
-    (∀ v, v◁ᵥty -∗ ⌜ty.(ty_layout) = lyty⌝ ∗ T) -∗
-    subsume (l ◁ₗ padded ty lyty ly) (l ◁ₗ uninit ly) T.
+  Lemma subsume_padded_uninit l ly1 ly2 lyty ty `{!Movable ty} T:
+    (∀ v, v◁ᵥty -∗ ⌜ty.(ty_layout) = lyty⌝ ∗ subsume (l ◁ₗ uninit ly1) (l ◁ₗ uninit ly2) T) -∗
+    subsume (l ◁ₗ padded ty lyty ly1) (l ◁ₗ uninit ly2) T.
   Proof.
     iIntros "HT". iDestruct 1 as ([? ?] ?) "(Hb & Hl & Hr)".
     iDestruct (ty_deref with "Hl") as (v1) "[Hl Hv1]".
     iDestruct (ty_size_eq with "Hv1") as %Hlen1.
     iDestruct (ty_deref with "Hr") as (v2) "[Hr Hv2]".
     iDestruct (ty_size_eq with "Hv2") as %Hlen2.
-    iDestruct ("HT" with "Hv1") as (<-) "$".
+    iDestruct ("HT" with "Hv1") as (<-) "HT". iApply "HT".
     iExists (v1 ++ v2).
     rewrite /= heap_mapsto_app /has_layout_val app_length Hlen1 Hlen2.
     iFrame. iPureIntro.
     split => //. rewrite /= /ly_offset {2}/ly_size. lia.
   Qed.
-  Global Instance subsume_padded_uninit_inst l ly lyty ty `{!Movable ty}:
-    SubsumePlace l Own (padded ty lyty ly) (uninit ly) :=
-    λ T, i2p (subsume_padded_uninit l ly lyty ty T).
+  Global Instance subsume_padded_uninit_inst l ly1 ly2 lyty ty `{!Movable ty}:
+    SubsumePlace l Own (padded ty lyty ly1) (uninit ly2) | 4 :=
+    λ T, i2p (subsume_padded_uninit l ly1 ly2 lyty ty T).
 
   Lemma subsume_uninit_padded l β ly lyty T:
     ⌜lyty ⊑ ly⌝ ∗ T -∗

theories/typing/uninit.v

@@ -38,10 +38,11 @@ Section uninit.
   Qed.
 
   (* This only works for own because of ty might have interior mutability. *)
-  Lemma uninit_mono l ty `{!Movable ty} ly T:
-    ⌜ty.(ty_layout) = ly⌝ ∗ (∀ v, v ◁ᵥ ty -∗ T) -∗ subsume (l ◁ₗ ty) (l ◁ₗ uninit ly) T.
+  Lemma uninit_mono l ty `{!Movable ty} ly T `{!FastDone (ty.(ty_layout) = ly)}:
+    (∀ v, v ◁ᵥ ty -∗ T) -∗
+    subsume (l ◁ₗ ty) (l ◁ₗ uninit ly) T.
   Proof.
-    iIntros "[<- HT] Hl".
+    unfold FastDone in *; subst. iIntros "HT Hl".
     iDestruct (ty_aligned with "Hl") as %?.
     iDestruct (ty_deref with "Hl") as (v) "[Hmt Hv]".
     iDestruct (ty_size_eq with "Hv") as %?.
@@ -49,10 +50,25 @@ Section uninit.
     - iExists _. by iFrame.
     - by iApply "HT".
   Qed.
-  Global Instance uninit_mono_inst l ty `{!Movable ty} ly:
+  (* This cannot be a definition but must be an Hint Extern since
+  Movable is a dependent subgoal and thus gets shelved. *)
+  Definition uninit_mono_inst l ty `{!Movable ty} ly `{!FastDone (ty.(ty_layout) = ly)}:
     SubsumePlace l Own ty (uninit ly) :=
     λ T, i2p (uninit_mono l ty ly T).
 
+  Lemma subsume_uninit_eq l β ly1 ly2 T `{!CanSolve (ly1.(ly_size) = ly2.(ly_size))}:
+    (⌜l `has_layout_loc` ly1⌝ -∗ ⌜l `has_layout_loc` ly2⌝ ∗ T) -∗
+    subsume (l ◁ₗ{β} uninit ly1) (l ◁ₗ{β} uninit ly2) T.
+  Proof.
+    revert select (CanSolve _) => Hsz. unfold CanSolve in *.
+    iIntros "HT Hl".
+    iDestruct "Hl" as (v Hv Hl) "Hl".
+    iDestruct ("HT" with "[//]") as (?) "$".
+    iExists _. iFrame. by rewrite /has_layout_val -Hsz.
+  Qed.
+  Global Instance subsume_uninit_eq_inst l β ly1 ly2 `{!CanSolve (ly1.(ly_size) = ly2.(ly_size))} :
+    SubsumePlace l β (uninit ly1) (uninit ly2) | 10 :=
+    λ T, i2p (subsume_uninit_eq l β ly1 ly2 T).
 
   Lemma split_uninit n l β ly1:
     (n ≤ ly1.(ly_size))%nat →
@@ -108,32 +124,27 @@ Section uninit.
     TypedBinOp v2 (v2 ◁ᵥ n @ int it)%I p (p ◁ₗ{β} uninit ly) (PtrOffsetOp u8) (IntOp it) PtrOp :=
     λ T, i2p (type_add_uninit v2 β ly p n it T).
 
-  Lemma annot_to_uninit l β ty T:
-    (∃ ly, (subsume (l ◁ₗ{β} ty) (l ◁ₗ{β} uninit ly) (l ◁ₗ{β} uninit ly -∗ T))) -∗
-    typed_annot_stmt ToUninit l (l ◁ₗ{β} ty) T.
-  Proof.
-    iDestruct 1 as (ly) "Hsub". iIntros "Hl". iApply step_fupd_intro => //. iModIntro.
-    iDestruct ("Hsub" with "Hl") as "[Hl HT]". by iApply "HT".
-  Qed.
-  Global Instance annot_to_uninit_inst l β ty:
-    TypedAnnotStmt (ToUninit) l (l ◁ₗ{β} ty) :=
-    λ T, i2p (annot_to_uninit l β ty T).
-
-  Lemma annot_uninit_strengthen_align l β ly T `{!FastDone (l `aligned_to` n)}:
-    (⌜is_power_of_two n⌝ ∗ (l ◁ₗ{β} uninit (ly_with_align ly.(ly_size) n) -∗ T)) -∗
-    typed_annot_stmt UninitStrengthenAlign l (l ◁ₗ{β} (uninit ly)) T.
+  Lemma annot_to_uninit l ty T `{!Movable ty}:
+    (∀ v, v ◁ᵥ ty -∗ l ◁ₗ uninit ty.(ty_layout) -∗ T) -∗
+    typed_annot_stmt ToUninit l (l ◁ₗ ty) T.
   Proof.
-    iIntros "[% HT] Hl". iApply step_fupd_intro => //. iModIntro. iApply "HT".
-    iDestruct "Hl" as (v Hv Hl) "Hl". iExists _. iFrame. iSplit => //. iPureIntro.
-    by apply ly_with_align_aligned_to.
+    iIntros "HT Hl". iApply step_fupd_intro => //. iModIntro.
+    iDestruct (ty_aligned with "Hl") as %?.
+    iDestruct (ty_deref with "Hl") as (v) "[Hmt Hv]".
+    iDestruct (ty_size_eq with "Hv") as %?.
+    iApply ("HT" with "Hv").
+    iExists _. by iFrame.
   Qed.
-  Global Instance annot_uninit_strengthen_align_inst l β ly `{!FastDone (l `aligned_to` n)}:
-    TypedAnnotStmt (UninitStrengthenAlign) l (l ◁ₗ{β} (uninit ly)) :=
-    λ T, i2p (annot_uninit_strengthen_align l β ly T).
+  Global Instance annot_to_uninit_inst l ty `{!Movable ty}:
+    TypedAnnotStmt (ToUninit) l (l ◁ₗ ty) :=
+    λ T, i2p (annot_to_uninit l ty T).
 
 End uninit.
 Notation "uninit< ly >" := (uninit ly) (only printing, format "'uninit<' ly '>'") : printing_sugar.
 
+Hint Extern 5 (SubsumePlace _ Own _ (uninit _)) =>
+  unshelve notypeclasses refine (uninit_mono_inst _ _ _ ) : typeclass_instances.
+
 Section void.
   Context `{!typeG Σ}.
 

theories/typing/union.v

@@ -211,7 +211,7 @@ Section function.
   Proof.
     iIntros "[-> [% HP]]". rewrite /variant/=. iApply typed_place_subsume.
     iApply subsume_padded_uninit. iIntros (v) "Hv".
-    iSplit => //. by iApply "HP".
+    iSplit => //. iIntros "$". by iApply "HP".
   Qed.
   Global Instance type_place_variant_neq_inst K ul n l ty `{!Movable ty} ti x:
     TypedPlace (GetMemberUnionPCtx ul n :: K) l Own (variant ti x ty) | 50:=

tutorial/proofs/t04_alloc/generated_proof_alloc.v

@@ -44,7 +44,7 @@ Section proof_alloc.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "alloc" "#1".