Commit 3c3cfb91 authored by Michael Sammler's avatar Michael Sammler
Browse files

improve early alloc

parent 7db018ac
Pipeline #42483 passed with stage
in 29 minutes and 52 seconds
......@@ -15,7 +15,8 @@ struct
[[rc::refined_by("base : loc", "given : Z", "remaining : Z")]]
[[rc::let("z_cur : Z = {(base.2 + given * PAGE_SIZE)%Z}")]]
[[rc::let("z_end : Z = {(base.2 + (given + remaining) * PAGE_SIZE)%Z}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}",
"{base.2 + (given + remaining) * PAGE_SIZE <= max_int u64}")]]
region {
[[rc::field("z_end @ int<uintptr_t>")]] uintptr_t end;
[[rc::field("z_cur @ int<uintptr_t>")]] uintptr_t cur;
......@@ -52,12 +53,8 @@ extern void clear_page(void *to);
[[rc::requires("{0 < n ≤ remaining}", "{n ≪ PAGE_SHIFT ≤ max_int u32}")]]
[[rc::returns("&own<zeroed<PAGES<{Z.to_nat n}>>>")]]
[[rc::ensures("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::tactics("all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.")]]
[[rc::tactics("all: try apply: has_layout_loc_trans' => //.")]]
[[rc::tactics("all: try rewrite -> Z.shiftl_mul_pow2 in *; try lia.")]]
[[rc::tactics("all: rewrite ?ly_offset_PAGES; try solve_goal.")]]
[[rc::tactics("all: transitivity max_alloc_end; last done.")]]
[[rc::tactics("all: etransitivity; last eassumption.")]]
[[rc::tactics("all: rewrite -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.")]]
void *hyp_early_alloc_contig(unsigned int nr_pages){
uintptr_t ret = cur, p;
unsigned int i;
......
......@@ -6,136 +6,136 @@ Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section code.
Definition file_0 : string := "linux/pkvm/early_alloc.c".
Definition loc_2 : location_info := LocationInfo file_0 41 2 41 52.
Definition loc_3 : location_info := LocationInfo file_0 41 9 41 51.
Definition loc_4 : location_info := LocationInfo file_0 41 9 41 45.
Definition loc_5 : location_info := LocationInfo file_0 41 10 41 19.
Definition loc_6 : location_info := LocationInfo file_0 41 10 41 19.
Definition loc_7 : location_info := LocationInfo file_0 41 11 41 14.
Definition loc_8 : location_info := LocationInfo file_0 41 22 41 44.
Definition loc_9 : location_info := LocationInfo file_0 41 34 41 44.
Definition loc_10 : location_info := LocationInfo file_0 41 34 41 44.
Definition loc_11 : location_info := LocationInfo file_0 41 35 41 38.
Definition loc_12 : location_info := LocationInfo file_0 41 49 41 51.
Definition loc_15 : location_info := LocationInfo file_0 62 2 62 31.
Definition loc_16 : location_info := LocationInfo file_0 65 2 66 26.
Definition loc_17 : location_info := LocationInfo file_0 68 2 68 16.
Definition loc_18 : location_info := LocationInfo file_0 68 16 68 3.
Definition loc_19 : location_info := LocationInfo file_0 69 2 69 30.
Definition loc_20 : location_info := LocationInfo file_0 70 2 73 3.
Definition loc_21 : location_info := LocationInfo file_0 83 2 87 3.
Definition loc_22 : location_info := LocationInfo file_0 83 7 83 12.
Definition loc_23 : location_info := LocationInfo file_0 83 2 87 3.
Definition loc_24 : location_info := LocationInfo file_0 89 2 89 67.
Definition loc_25 : location_info := LocationInfo file_0 89 9 89 66.
Definition loc_26 : location_info := LocationInfo file_0 89 35 89 47.
Definition loc_27 : location_info := LocationInfo file_0 89 35 89 47.
Definition loc_28 : location_info := LocationInfo file_0 89 37 89 40.
Definition loc_29 : location_info := LocationInfo file_0 89 51 89 65.
Definition loc_30 : location_info := LocationInfo file_0 89 61 89 64.
Definition loc_31 : location_info := LocationInfo file_0 89 61 89 64.
Definition loc_32 : location_info := LocationInfo file_0 83 33 87 3.
Definition loc_33 : location_info := LocationInfo file_0 84 4 84 18.
Definition loc_34 : location_info := LocationInfo file_0 84 18 84 5.
Definition loc_35 : location_info := LocationInfo file_0 85 4 85 24.
Definition loc_36 : location_info := LocationInfo file_0 86 4 86 73.
Definition loc_37 : location_info := LocationInfo file_0 83 2 87 3.
Definition loc_38 : location_info := LocationInfo file_0 83 28 83 31.
Definition loc_39 : location_info := LocationInfo file_0 83 28 83 29.
Definition loc_40 : location_info := LocationInfo file_0 86 4 86 14.
Definition loc_41 : location_info := LocationInfo file_0 86 4 86 14.
Definition loc_42 : location_info := LocationInfo file_0 86 15 86 71.
Definition loc_43 : location_info := LocationInfo file_0 86 41 86 53.
Definition loc_44 : location_info := LocationInfo file_0 86 41 86 53.
Definition loc_45 : location_info := LocationInfo file_0 86 43 86 46.
Definition loc_46 : location_info := LocationInfo file_0 86 57 86 70.
Definition loc_47 : location_info := LocationInfo file_0 86 66 86 69.
Definition loc_48 : location_info := LocationInfo file_0 86 66 86 69.
Definition loc_49 : location_info := LocationInfo file_0 85 4 85 5.
Definition loc_50 : location_info := LocationInfo file_0 85 8 85 23.
Definition loc_51 : location_info := LocationInfo file_0 85 8 85 11.
Definition loc_52 : location_info := LocationInfo file_0 85 8 85 11.
Definition loc_53 : location_info := LocationInfo file_0 85 14 85 23.
Definition loc_54 : location_info := LocationInfo file_0 85 15 85 16.
Definition loc_55 : location_info := LocationInfo file_0 85 15 85 16.
Definition loc_56 : location_info := LocationInfo file_0 85 20 85 22.
Definition loc_57 : location_info := LocationInfo file_0 84 4 84 17.
Definition loc_58 : location_info := LocationInfo file_0 84 5 84 17.
Definition loc_59 : location_info := LocationInfo file_0 84 7 84 10.
Definition loc_60 : location_info := LocationInfo file_0 83 14 83 26.
Definition loc_61 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_62 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_63 : location_info := LocationInfo file_0 83 18 83 26.
Definition loc_64 : location_info := LocationInfo file_0 83 18 83 26.
Definition loc_65 : location_info := LocationInfo file_0 83 7 83 8.
Definition loc_66 : location_info := LocationInfo file_0 83 11 83 12.
Definition loc_67 : location_info := LocationInfo file_0 70 29 73 3.
Definition loc_68 : location_info := LocationInfo file_0 71 4 71 20.
Definition loc_69 : location_info := LocationInfo file_0 72 4 72 26.
Definition loc_70 : location_info := LocationInfo file_0 72 11 72 25.
Definition loc_71 : location_info := LocationInfo file_0 71 4 71 13.
Definition loc_72 : location_info := LocationInfo file_0 71 5 71 8.
Definition loc_73 : location_info := LocationInfo file_0 71 16 71 19.
Definition loc_74 : location_info := LocationInfo file_0 71 16 71 19.
Definition loc_76 : location_info := LocationInfo file_0 70 6 70 27.
Definition loc_77 : location_info := LocationInfo file_0 70 6 70 15.
Definition loc_78 : location_info := LocationInfo file_0 70 6 70 15.
Definition loc_79 : location_info := LocationInfo file_0 70 7 70 10.
Definition loc_80 : location_info := LocationInfo file_0 70 18 70 27.
Definition loc_81 : location_info := LocationInfo file_0 70 18 70 27.
Definition loc_82 : location_info := LocationInfo file_0 70 19 70 22.
Definition loc_83 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_84 : location_info := LocationInfo file_0 69 3 69 6.
Definition loc_85 : location_info := LocationInfo file_0 69 2 69 29.
Definition loc_86 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_87 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_88 : location_info := LocationInfo file_0 69 3 69 6.
Definition loc_89 : location_info := LocationInfo file_0 69 15 69 29.
Definition loc_90 : location_info := LocationInfo file_0 69 15 69 23.
Definition loc_91 : location_info := LocationInfo file_0 69 15 69 23.
Definition loc_92 : location_info := LocationInfo file_0 69 27 69 29.
Definition loc_93 : location_info := LocationInfo file_0 68 2 68 15.
Definition loc_94 : location_info := LocationInfo file_0 68 3 68 15.
Definition loc_95 : location_info := LocationInfo file_0 68 5 68 8.
Definition loc_96 : location_info := LocationInfo file_0 66 4 66 26.
Definition loc_97 : location_info := LocationInfo file_0 66 11 66 25.
Definition loc_99 : location_info := LocationInfo file_0 65 6 65 15.
Definition loc_101 : location_info := LocationInfo file_0 65 7 65 15.
Definition loc_102 : location_info := LocationInfo file_0 65 7 65 15.
Definition loc_103 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_104 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_105 : location_info := LocationInfo file_0 62 19 62 22.
Definition loc_110 : location_info := LocationInfo file_0 99 2 99 16.
Definition loc_111 : location_info := LocationInfo file_0 99 16 99 3.
Definition loc_112 : location_info := LocationInfo file_0 100 2 100 35.
Definition loc_113 : location_info := LocationInfo file_0 100 9 100 34.
Definition loc_114 : location_info := LocationInfo file_0 100 9 100 31.
Definition loc_115 : location_info := LocationInfo file_0 100 9 100 31.
Definition loc_116 : location_info := LocationInfo file_0 100 32 100 33.
Definition loc_117 : location_info := LocationInfo file_0 99 2 99 15.
Definition loc_118 : location_info := LocationInfo file_0 99 3 99 15.
Definition loc_119 : location_info := LocationInfo file_0 99 5 99 8.
Definition loc_122 : location_info := LocationInfo file_0 110 2 110 20.
Definition loc_123 : location_info := LocationInfo file_0 111 2 111 52.
Definition loc_124 : location_info := LocationInfo file_0 112 2 112 31.
Definition loc_125 : location_info := LocationInfo file_0 112 2 112 11.
Definition loc_126 : location_info := LocationInfo file_0 112 3 112 6.
Definition loc_127 : location_info := LocationInfo file_0 112 14 112 30.
Definition loc_128 : location_info := LocationInfo file_0 112 26 112 30.
Definition loc_129 : location_info := LocationInfo file_0 112 26 112 30.
Definition loc_130 : location_info := LocationInfo file_0 111 2 111 11.
Definition loc_131 : location_info := LocationInfo file_0 111 3 111 6.
Definition loc_132 : location_info := LocationInfo file_0 111 14 111 51.
Definition loc_133 : location_info := LocationInfo file_0 111 26 111 51.
Definition loc_134 : location_info := LocationInfo file_0 111 27 111 43.
Definition loc_135 : location_info := LocationInfo file_0 111 39 111 43.
Definition loc_136 : location_info := LocationInfo file_0 111 39 111 43.
Definition loc_137 : location_info := LocationInfo file_0 111 46 111 50.
Definition loc_138 : location_info := LocationInfo file_0 111 46 111 50.
Definition loc_139 : location_info := LocationInfo file_0 110 2 110 12.
Definition loc_140 : location_info := LocationInfo file_0 110 3 110 6.
Definition loc_141 : location_info := LocationInfo file_0 110 15 110 19.
Definition loc_142 : location_info := LocationInfo file_0 110 15 110 19.
Definition loc_2 : location_info := LocationInfo file_0 42 2 42 52.
Definition loc_3 : location_info := LocationInfo file_0 42 9 42 51.
Definition loc_4 : location_info := LocationInfo file_0 42 9 42 45.
Definition loc_5 : location_info := LocationInfo file_0 42 10 42 19.
Definition loc_6 : location_info := LocationInfo file_0 42 10 42 19.
Definition loc_7 : location_info := LocationInfo file_0 42 11 42 14.
Definition loc_8 : location_info := LocationInfo file_0 42 22 42 44.
Definition loc_9 : location_info := LocationInfo file_0 42 34 42 44.
Definition loc_10 : location_info := LocationInfo file_0 42 34 42 44.
Definition loc_11 : location_info := LocationInfo file_0 42 35 42 38.
Definition loc_12 : location_info := LocationInfo file_0 42 49 42 51.
Definition loc_15 : location_info := LocationInfo file_0 59 2 59 31.
Definition loc_16 : location_info := LocationInfo file_0 62 2 63 26.
Definition loc_17 : location_info := LocationInfo file_0 65 2 65 16.
Definition loc_18 : location_info := LocationInfo file_0 65 16 65 3.
Definition loc_19 : location_info := LocationInfo file_0 66 2 66 30.
Definition loc_20 : location_info := LocationInfo file_0 67 2 70 3.
Definition loc_21 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_22 : location_info := LocationInfo file_0 80 7 80 12.
Definition loc_23 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_24 : location_info := LocationInfo file_0 86 2 86 67.
Definition loc_25 : location_info := LocationInfo file_0 86 9 86 66.
Definition loc_26 : location_info := LocationInfo file_0 86 35 86 47.
Definition loc_27 : location_info := LocationInfo file_0 86 35 86 47.
Definition loc_28 : location_info := LocationInfo file_0 86 37 86 40.
Definition loc_29 : location_info := LocationInfo file_0 86 51 86 65.
Definition loc_30 : location_info := LocationInfo file_0 86 61 86 64.
Definition loc_31 : location_info := LocationInfo file_0 86 61 86 64.
Definition loc_32 : location_info := LocationInfo file_0 80 33 84 3.
Definition loc_33 : location_info := LocationInfo file_0 81 4 81 18.
Definition loc_34 : location_info := LocationInfo file_0 81 18 81 5.
Definition loc_35 : location_info := LocationInfo file_0 82 4 82 24.
Definition loc_36 : location_info := LocationInfo file_0 83 4 83 73.
Definition loc_37 : location_info := LocationInfo file_0 80 2 84 3.
Definition loc_38 : location_info := LocationInfo file_0 80 28 80 31.
Definition loc_39 : location_info := LocationInfo file_0 80 28 80 29.
Definition loc_40 : location_info := LocationInfo file_0 83 4 83 14.
Definition loc_41 : location_info := LocationInfo file_0 83 4 83 14.
Definition loc_42 : location_info := LocationInfo file_0 83 15 83 71.
Definition loc_43 : location_info := LocationInfo file_0 83 41 83 53.
Definition loc_44 : location_info := LocationInfo file_0 83 41 83 53.
Definition loc_45 : location_info := LocationInfo file_0 83 43 83 46.
Definition loc_46 : location_info := LocationInfo file_0 83 57 83 70.
Definition loc_47 : location_info := LocationInfo file_0 83 66 83 69.
Definition loc_48 : location_info := LocationInfo file_0 83 66 83 69.
Definition loc_49 : location_info := LocationInfo file_0 82 4 82 5.
Definition loc_50 : location_info := LocationInfo file_0 82 8 82 23.
Definition loc_51 : location_info := LocationInfo file_0 82 8 82 11.
Definition loc_52 : location_info := LocationInfo file_0 82 8 82 11.
Definition loc_53 : location_info := LocationInfo file_0 82 14 82 23.
Definition loc_54 : location_info := LocationInfo file_0 82 15 82 16.
Definition loc_55 : location_info := LocationInfo file_0 82 15 82 16.
Definition loc_56 : location_info := LocationInfo file_0 82 20 82 22.
Definition loc_57 : location_info := LocationInfo file_0 81 4 81 17.
Definition loc_58 : location_info := LocationInfo file_0 81 5 81 17.
Definition loc_59 : location_info := LocationInfo file_0 81 7 81 10.
Definition loc_60 : location_info := LocationInfo file_0 80 14 80 26.
Definition loc_61 : location_info := LocationInfo file_0 80 14 80 15.
Definition loc_62 : location_info := LocationInfo file_0 80 14 80 15.
Definition loc_63 : location_info := LocationInfo file_0 80 18 80 26.
Definition loc_64 : location_info := LocationInfo file_0 80 18 80 26.
Definition loc_65 : location_info := LocationInfo file_0 80 7 80 8.
Definition loc_66 : location_info := LocationInfo file_0 80 11 80 12.
Definition loc_67 : location_info := LocationInfo file_0 67 29 70 3.
Definition loc_68 : location_info := LocationInfo file_0 68 4 68 20.
Definition loc_69 : location_info := LocationInfo file_0 69 4 69 26.
Definition loc_70 : location_info := LocationInfo file_0 69 11 69 25.
Definition loc_71 : location_info := LocationInfo file_0 68 4 68 13.
Definition loc_72 : location_info := LocationInfo file_0 68 5 68 8.
Definition loc_73 : location_info := LocationInfo file_0 68 16 68 19.
Definition loc_74 : location_info := LocationInfo file_0 68 16 68 19.
Definition loc_76 : location_info := LocationInfo file_0 67 6 67 27.
Definition loc_77 : location_info := LocationInfo file_0 67 6 67 15.
Definition loc_78 : location_info := LocationInfo file_0 67 6 67 15.
Definition loc_79 : location_info := LocationInfo file_0 67 7 67 10.
Definition loc_80 : location_info := LocationInfo file_0 67 18 67 27.
Definition loc_81 : location_info := LocationInfo file_0 67 18 67 27.
Definition loc_82 : location_info := LocationInfo file_0 67 19 67 22.
Definition loc_83 : location_info := LocationInfo file_0 66 2 66 11.
Definition loc_84 : location_info := LocationInfo file_0 66 3 66 6.
Definition loc_85 : location_info := LocationInfo file_0 66 2 66 29.
Definition loc_86 : location_info := LocationInfo file_0 66 2 66 11.
Definition loc_87 : location_info := LocationInfo file_0 66 2 66 11.
Definition loc_88 : location_info := LocationInfo file_0 66 3 66 6.
Definition loc_89 : location_info := LocationInfo file_0 66 15 66 29.
Definition loc_90 : location_info := LocationInfo file_0 66 15 66 23.
Definition loc_91 : location_info := LocationInfo file_0 66 15 66 23.
Definition loc_92 : location_info := LocationInfo file_0 66 27 66 29.
Definition loc_93 : location_info := LocationInfo file_0 65 2 65 15.
Definition loc_94 : location_info := LocationInfo file_0 65 3 65 15.
Definition loc_95 : location_info := LocationInfo file_0 65 5 65 8.
Definition loc_96 : location_info := LocationInfo file_0 63 4 63 26.
Definition loc_97 : location_info := LocationInfo file_0 63 11 63 25.
Definition loc_99 : location_info := LocationInfo file_0 62 6 62 15.
Definition loc_101 : location_info := LocationInfo file_0 62 7 62 15.
Definition loc_102 : location_info := LocationInfo file_0 62 7 62 15.
Definition loc_103 : location_info := LocationInfo file_0 59 18 59 27.
Definition loc_104 : location_info := LocationInfo file_0 59 18 59 27.
Definition loc_105 : location_info := LocationInfo file_0 59 19 59 22.
Definition loc_110 : location_info := LocationInfo file_0 96 2 96 16.
Definition loc_111 : location_info := LocationInfo file_0 96 16 96 3.
Definition loc_112 : location_info := LocationInfo file_0 97 2 97 35.
Definition loc_113 : location_info := LocationInfo file_0 97 9 97 34.
Definition loc_114 : location_info := LocationInfo file_0 97 9 97 31.
Definition loc_115 : location_info := LocationInfo file_0 97 9 97 31.
Definition loc_116 : location_info := LocationInfo file_0 97 32 97 33.
Definition loc_117 : location_info := LocationInfo file_0 96 2 96 15.
Definition loc_118 : location_info := LocationInfo file_0 96 3 96 15.
Definition loc_119 : location_info := LocationInfo file_0 96 5 96 8.
Definition loc_122 : location_info := LocationInfo file_0 107 2 107 20.
Definition loc_123 : location_info := LocationInfo file_0 108 2 108 52.
Definition loc_124 : location_info := LocationInfo file_0 109 2 109 31.
Definition loc_125 : location_info := LocationInfo file_0 109 2 109 11.
Definition loc_126 : location_info := LocationInfo file_0 109 3 109 6.
Definition loc_127 : location_info := LocationInfo file_0 109 14 109 30.
Definition loc_128 : location_info := LocationInfo file_0 109 26 109 30.
Definition loc_129 : location_info := LocationInfo file_0 109 26 109 30.
Definition loc_130 : location_info := LocationInfo file_0 108 2 108 11.
Definition loc_131 : location_info := LocationInfo file_0 108 3 108 6.
Definition loc_132 : location_info := LocationInfo file_0 108 14 108 51.
Definition loc_133 : location_info := LocationInfo file_0 108 26 108 51.
Definition loc_134 : location_info := LocationInfo file_0 108 27 108 43.
Definition loc_135 : location_info := LocationInfo file_0 108 39 108 43.
Definition loc_136 : location_info := LocationInfo file_0 108 39 108 43.
Definition loc_137 : location_info := LocationInfo file_0 108 46 108 50.
Definition loc_138 : location_info := LocationInfo file_0 108 46 108 50.
Definition loc_139 : location_info := LocationInfo file_0 107 2 107 12.
Definition loc_140 : location_info := LocationInfo file_0 107 3 107 6.
Definition loc_141 : location_info := LocationInfo file_0 107 15 107 19.
Definition loc_142 : location_info := LocationInfo file_0 107 15 107 19.
(* Definition of struct [region]. *)
Program Definition struct_region := {|
......
......@@ -37,12 +37,8 @@ Section proof_hyp_early_alloc_contig.
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_contig" "#3".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.
all: try apply: has_layout_loc_trans' => //.
all: try rewrite -> Z.shiftl_mul_pow2 in *; try lia.
all: rewrite ?ly_offset_PAGES; try solve_goal.
all: transitivity max_alloc_end; last done.
all: etransitivity; last eassumption.
all: rewrite -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.
all: print_sidecondition_goal "hyp_early_alloc_contig".
Qed.
End proof_hyp_early_alloc_contig.
......@@ -30,7 +30,8 @@ Section spec.
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (ptr (Z.to_nat ((given + remaining) * PAGE_SIZE)))))
]) (
0 given
0 remaining
0 remaining
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
)
)%I.
Typeclasses Opaque region_rec.
......@@ -56,7 +57,8 @@ Section spec.
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (ptr (Z.to_nat ((given + remaining) * PAGE_SIZE)))))
]) (
0 given
0 remaining
0 remaining
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
)
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
......
......@@ -42,20 +42,3 @@ Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.
Section instances.
Context `{!typeG Σ}.
Lemma simplify_hyp_loc_in_bounds_ptr_in_range l (n : nat) T:
(min_alloc_start l.2 l.2 + n max_alloc_end - loc_in_bounds l n - T) -
simplify_hyp (loc_in_bounds l n) T.
Proof.
iIntros "HT Hlib".
iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
by iApply "HT".
Qed.
(* FIXME limit the application in a cleaner way. *)
Global Instance simplify_hyp_loc_in_bounds_ptr_in_range_inst l n `{!TCUnless (FastDone (min_alloc_start l.2))}:
SimplifyHyp (loc_in_bounds l n) (Some 0%N) :=
λ T, i2p (simplify_hyp_loc_in_bounds_ptr_in_range l n T).
End instances.
......@@ -12,7 +12,7 @@ Set Default Proof Using "Type".
Global Unset Program Cases.
Global Set Keyed Unification.
Typeclasses Opaque Z.divide Z.modulo Z.div.
Typeclasses Opaque Z.divide Z.modulo Z.div Z.shiftl Z.shiftr.
Arguments min : simpl nomatch.
Arguments Z.testbit : simpl never.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment