Commit 63fa5416 authored by Michael Sammler's avatar Michael Sammler
Browse files

remove normalize_loc

parent d109772c
Pipeline #42392 passed with stage
in 14 minutes and 38 seconds
......@@ -35,6 +35,7 @@ int* roundtrip1(int* p){
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::returns("p @ &own<n @ int<i32>>")]]
[[rc::tactics("all: try f_equal; solve_loc_eq.")]]
int* roundtrip2(int* p){
size_t i = (size_t) p;
int *q = (void*) i;
......
......@@ -45,75 +45,75 @@ Section code.
Definition loc_51 : location_info := LocationInfo file_0 30 13 30 23.
Definition loc_52 : location_info := LocationInfo file_0 30 22 30 23.
Definition loc_53 : location_info := LocationInfo file_0 30 22 30 23.
Definition loc_58 : location_info := LocationInfo file_0 39 2 39 24.
Definition loc_59 : location_info := LocationInfo file_0 40 2 40 21.
Definition loc_60 : location_info := LocationInfo file_0 41 2 41 47.
Definition loc_61 : location_info := LocationInfo file_0 41 9 41 46.
Definition loc_62 : location_info := LocationInfo file_0 41 35 41 38.
Definition loc_63 : location_info := LocationInfo file_0 41 35 41 38.
Definition loc_64 : location_info := LocationInfo file_0 41 42 41 45.
Definition loc_65 : location_info := LocationInfo file_0 41 42 41 45.
Definition loc_66 : location_info := LocationInfo file_0 40 11 40 20.
Definition loc_67 : location_info := LocationInfo file_0 40 19 40 20.
Definition loc_68 : location_info := LocationInfo file_0 40 19 40 20.
Definition loc_71 : location_info := LocationInfo file_0 39 13 39 23.
Definition loc_72 : location_info := LocationInfo file_0 39 22 39 23.
Definition loc_73 : location_info := LocationInfo file_0 39 22 39 23.
Definition loc_78 : location_info := LocationInfo file_0 49 2 49 24.
Definition loc_79 : location_info := LocationInfo file_0 50 2 50 20.
Definition loc_80 : location_info := LocationInfo file_0 51 2 51 44.
Definition loc_81 : location_info := LocationInfo file_0 52 2 52 13.
Definition loc_82 : location_info := LocationInfo file_0 53 2 53 11.
Definition loc_83 : location_info := LocationInfo file_0 53 9 53 10.
Definition loc_84 : location_info := LocationInfo file_0 53 9 53 10.
Definition loc_85 : location_info := LocationInfo file_0 52 10 52 12.
Definition loc_86 : location_info := LocationInfo file_0 52 10 52 12.
Definition loc_87 : location_info := LocationInfo file_0 52 11 52 12.
Definition loc_88 : location_info := LocationInfo file_0 52 11 52 12.
Definition loc_91 : location_info := LocationInfo file_0 51 2 51 3.
Definition loc_92 : location_info := LocationInfo file_0 51 6 51 43.
Definition loc_93 : location_info := LocationInfo file_0 51 32 51 35.
Definition loc_94 : location_info := LocationInfo file_0 51 32 51 35.
Definition loc_95 : location_info := LocationInfo file_0 51 39 51 42.
Definition loc_96 : location_info := LocationInfo file_0 51 39 51 42.
Definition loc_97 : location_info := LocationInfo file_0 50 11 50 19.
Definition loc_98 : location_info := LocationInfo file_0 50 18 50 19.
Definition loc_99 : location_info := LocationInfo file_0 50 18 50 19.
Definition loc_102 : location_info := LocationInfo file_0 49 13 49 23.
Definition loc_103 : location_info := LocationInfo file_0 49 22 49 23.
Definition loc_104 : location_info := LocationInfo file_0 49 22 49 23.
Definition loc_109 : location_info := LocationInfo file_0 61 2 61 30.
Definition loc_110 : location_info := LocationInfo file_0 62 2 62 56.
Definition loc_111 : location_info := LocationInfo file_0 63 2 63 12.
Definition loc_112 : location_info := LocationInfo file_0 63 9 63 11.
Definition loc_113 : location_info := LocationInfo file_0 63 9 63 11.
Definition loc_114 : location_info := LocationInfo file_0 63 10 63 11.
Definition loc_115 : location_info := LocationInfo file_0 63 10 63 11.
Definition loc_116 : location_info := LocationInfo file_0 62 11 62 55.
Definition loc_117 : location_info := LocationInfo file_0 62 37 62 40.
Definition loc_118 : location_info := LocationInfo file_0 62 37 62 40.
Definition loc_119 : location_info := LocationInfo file_0 62 44 62 54.
Definition loc_120 : location_info := LocationInfo file_0 62 52 62 53.
Definition loc_121 : location_info := LocationInfo file_0 62 52 62 53.
Definition loc_124 : location_info := LocationInfo file_0 61 16 61 29.
Definition loc_125 : location_info := LocationInfo file_0 61 28 61 29.
Definition loc_126 : location_info := LocationInfo file_0 61 28 61 29.
Definition loc_131 : location_info := LocationInfo file_0 71 2 71 24.
Definition loc_132 : location_info := LocationInfo file_0 72 2 72 20.
Definition loc_133 : location_info := LocationInfo file_0 73 2 73 50.
Definition loc_134 : location_info := LocationInfo file_0 73 9 73 49.
Definition loc_135 : location_info := LocationInfo file_0 73 9 73 49.
Definition loc_136 : location_info := LocationInfo file_0 73 10 73 49.
Definition loc_137 : location_info := LocationInfo file_0 73 37 73 40.
Definition loc_138 : location_info := LocationInfo file_0 73 37 73 40.
Definition loc_139 : location_info := LocationInfo file_0 73 44 73 47.
Definition loc_140 : location_info := LocationInfo file_0 73 44 73 47.
Definition loc_141 : location_info := LocationInfo file_0 72 11 72 19.
Definition loc_142 : location_info := LocationInfo file_0 72 18 72 19.
Definition loc_143 : location_info := LocationInfo file_0 72 18 72 19.
Definition loc_146 : location_info := LocationInfo file_0 71 13 71 23.
Definition loc_147 : location_info := LocationInfo file_0 71 22 71 23.
Definition loc_148 : location_info := LocationInfo file_0 71 22 71 23.
Definition loc_58 : location_info := LocationInfo file_0 40 2 40 24.
Definition loc_59 : location_info := LocationInfo file_0 41 2 41 21.
Definition loc_60 : location_info := LocationInfo file_0 42 2 42 47.
Definition loc_61 : location_info := LocationInfo file_0 42 9 42 46.
Definition loc_62 : location_info := LocationInfo file_0 42 35 42 38.
Definition loc_63 : location_info := LocationInfo file_0 42 35 42 38.
Definition loc_64 : location_info := LocationInfo file_0 42 42 42 45.
Definition loc_65 : location_info := LocationInfo file_0 42 42 42 45.
Definition loc_66 : location_info := LocationInfo file_0 41 11 41 20.
Definition loc_67 : location_info := LocationInfo file_0 41 19 41 20.
Definition loc_68 : location_info := LocationInfo file_0 41 19 41 20.
Definition loc_71 : location_info := LocationInfo file_0 40 13 40 23.
Definition loc_72 : location_info := LocationInfo file_0 40 22 40 23.
Definition loc_73 : location_info := LocationInfo file_0 40 22 40 23.
Definition loc_78 : location_info := LocationInfo file_0 50 2 50 24.
Definition loc_79 : location_info := LocationInfo file_0 51 2 51 20.
Definition loc_80 : location_info := LocationInfo file_0 52 2 52 44.
Definition loc_81 : location_info := LocationInfo file_0 53 2 53 13.
Definition loc_82 : location_info := LocationInfo file_0 54 2 54 11.
Definition loc_83 : location_info := LocationInfo file_0 54 9 54 10.
Definition loc_84 : location_info := LocationInfo file_0 54 9 54 10.
Definition loc_85 : location_info := LocationInfo file_0 53 10 53 12.
Definition loc_86 : location_info := LocationInfo file_0 53 10 53 12.
Definition loc_87 : location_info := LocationInfo file_0 53 11 53 12.
Definition loc_88 : location_info := LocationInfo file_0 53 11 53 12.
Definition loc_91 : location_info := LocationInfo file_0 52 2 52 3.
Definition loc_92 : location_info := LocationInfo file_0 52 6 52 43.
Definition loc_93 : location_info := LocationInfo file_0 52 32 52 35.
Definition loc_94 : location_info := LocationInfo file_0 52 32 52 35.
Definition loc_95 : location_info := LocationInfo file_0 52 39 52 42.
Definition loc_96 : location_info := LocationInfo file_0 52 39 52 42.
Definition loc_97 : location_info := LocationInfo file_0 51 11 51 19.
Definition loc_98 : location_info := LocationInfo file_0 51 18 51 19.
Definition loc_99 : location_info := LocationInfo file_0 51 18 51 19.
Definition loc_102 : location_info := LocationInfo file_0 50 13 50 23.
Definition loc_103 : location_info := LocationInfo file_0 50 22 50 23.
Definition loc_104 : location_info := LocationInfo file_0 50 22 50 23.
Definition loc_109 : location_info := LocationInfo file_0 62 2 62 30.
Definition loc_110 : location_info := LocationInfo file_0 63 2 63 56.
Definition loc_111 : location_info := LocationInfo file_0 64 2 64 12.
Definition loc_112 : location_info := LocationInfo file_0 64 9 64 11.
Definition loc_113 : location_info := LocationInfo file_0 64 9 64 11.
Definition loc_114 : location_info := LocationInfo file_0 64 10 64 11.
Definition loc_115 : location_info := LocationInfo file_0 64 10 64 11.
Definition loc_116 : location_info := LocationInfo file_0 63 11 63 55.
Definition loc_117 : location_info := LocationInfo file_0 63 37 63 40.
Definition loc_118 : location_info := LocationInfo file_0 63 37 63 40.
Definition loc_119 : location_info := LocationInfo file_0 63 44 63 54.
Definition loc_120 : location_info := LocationInfo file_0 63 52 63 53.
Definition loc_121 : location_info := LocationInfo file_0 63 52 63 53.
Definition loc_124 : location_info := LocationInfo file_0 62 16 62 29.
Definition loc_125 : location_info := LocationInfo file_0 62 28 62 29.
Definition loc_126 : location_info := LocationInfo file_0 62 28 62 29.
Definition loc_131 : location_info := LocationInfo file_0 72 2 72 24.
Definition loc_132 : location_info := LocationInfo file_0 73 2 73 20.
Definition loc_133 : location_info := LocationInfo file_0 74 2 74 50.
Definition loc_134 : location_info := LocationInfo file_0 74 9 74 49.
Definition loc_135 : location_info := LocationInfo file_0 74 9 74 49.
Definition loc_136 : location_info := LocationInfo file_0 74 10 74 49.
Definition loc_137 : location_info := LocationInfo file_0 74 37 74 40.
Definition loc_138 : location_info := LocationInfo file_0 74 37 74 40.
Definition loc_139 : location_info := LocationInfo file_0 74 44 74 47.
Definition loc_140 : location_info := LocationInfo file_0 74 44 74 47.
Definition loc_141 : location_info := LocationInfo file_0 73 11 73 19.
Definition loc_142 : location_info := LocationInfo file_0 73 18 73 19.
Definition loc_143 : location_info := LocationInfo file_0 73 18 73 19.
Definition loc_146 : location_info := LocationInfo file_0 72 13 72 23.
Definition loc_147 : location_info := LocationInfo file_0 72 22 72 23.
Definition loc_148 : location_info := LocationInfo file_0 72 22 72 23.
(* Definition of function [int_ptr]. *)
Definition impl_int_ptr : function := {|
......
......@@ -21,6 +21,7 @@ Section proof_roundtrip2.
- repeat liRStep; liShow.
all: print_typesystem_goal "roundtrip2" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: try f_equal; solve_loc_eq.
all: print_sidecondition_goal "roundtrip2".
Qed.
End proof_roundtrip2.
......@@ -30,15 +30,3 @@ Qed.
(** * location offset *)
Global Instance simpl_offset_inj l1 l2 sl n : SimplBothRel (=) (l1 at{sl} n) (l2 at{sl} n) (l1 = l2).
Proof. unfold GetMemberLoc. split; [apply shift_loc_inj1| naive_solver]. Qed.
(** * Location normalzation. *)
Definition normalize_loc (p1 p2 : loc) : Prop := locked eq p1 p2.
Typeclasses Opaque normalize_loc.
Global Instance simpl_normalize_loc_pair (p q : loc):
SimplAnd (normalize_loc (p.1, p.2) q) (λ T, normalize_loc p q T).
Proof. rewrite /normalize_loc. unlock. by destruct p. Qed.
Global Instance simpl_normalize_loc_refl (p q : loc):
SimplAnd (normalize_loc p q) (λ T, p = q T) | 1000.
Proof. rewrite /normalize_loc. unlock. done. Qed.
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs optional int singleton.
From refinedc.typing.automation Require Import simplification.
Set Default Proof Using "Type".
Section own.
......@@ -229,15 +228,13 @@ Section own.
Lemma type_copy_aid v1 v2 P1 P2 T:
( p1 p2, subsume P1 (v1 ◁ᵥ p1 @ frac_ptr Own (place p1)) (
subsume P2 (v2 ◁ᵥ p2 @ frac_ptr Own (place p2)) (
p, normalize_loc (p2.1, p1.2) p
T (val_of_loc p) (t2mt (value void* (val_of_loc p)))))) -
T (val_of_loc (p2.1, p1.2)) (t2mt (value void* (val_of_loc (p2.1, p1.2))))))) -
typed_copy_alloc_id v1 P1 v2 P2 T.
Proof.
iIntros "HT Hp1 Hp2" (Φ) "HΦ". iDestruct "HT" as (p1 p2) "HT".
iDestruct ("HT" with "Hp1") as "[Hp1 HT]". iDestruct "Hp1" as (->) "Hp1".
iDestruct ("HT" with "Hp2") as "[Hp2 HT]". iDestruct "Hp2" as (->) "Hp2".
iDestruct "HT" as (p Hp) "HT". rewrite /normalize_loc in Hp. unlock in Hp.
iApply wp_copy_alloc_id; try by rewrite val_to_of_loc. rewrite Hp.
iApply wp_copy_alloc_id; try by rewrite val_to_of_loc.
by iApply ("HΦ" with "[] HT").
Qed.
Global Instance type_copy_aid_inst v1 v2 P1 P2:
......
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