[2034] | 1 | include "ASM/PolicyStep.ma". |
---|
[1614] | 2 | |
---|
[1931] | 3 | include alias "basics/lists/list.ma". |
---|
| 4 | include alias "arithmetics/nat.ma". |
---|
| 5 | include alias "basics/logic.ma". |
---|
| 6 | |
---|
[2141] | 7 | let rec jump_expansion_internal (program: Σl:list labelled_instruction. |
---|
| 8 | lt (S (|l|)) 2^16 ∧ is_well_labelled_p l) (n: ℕ) |
---|
[1931] | 9 | on n:(Σx:bool × (option ppc_pc_map). |
---|
[2059] | 10 | let 〈no_ch,pol〉 ≝ x in |
---|
[2101] | 11 | match pol with |
---|
[1879] | 12 | [ None ⇒ True |
---|
[1931] | 13 | | Some x ⇒ |
---|
[2152] | 14 | And (And (And (And |
---|
| 15 | (not_jump_default program x) |
---|
[2034] | 16 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) |
---|
[2059] | 17 | (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉))) |
---|
[2152] | 18 | (sigma_compact_unsafe program (create_label_map program) x)) |
---|
[2211] | 19 | (\fst x ≤ 2^16) |
---|
[2101] | 20 | ]) ≝ |
---|
| 21 | let labels ≝ create_label_map program in |
---|
[2034] | 22 | match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with |
---|
[2059] | 23 | [ O ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉 |
---|
| 24 | | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in |
---|
[1931] | 25 | match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with |
---|
[1879] | 26 | [ None ⇒ λp2.〈false,None ?〉 |
---|
[2059] | 27 | | Some op ⇒ λp2.if no_ch |
---|
| 28 | then pi1 ?? (jump_expansion_internal program m) |
---|
[2225] | 29 | else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?») |
---|
[1810] | 30 | ] (refl … z) |
---|
[2034] | 31 | ] (refl … n). |
---|
[2264] | 32 | [5: #l #_ % |
---|
[2225] | 33 | | normalize nodelta cases (jump_expansion_start program (create_label_map program)) |
---|
[2034] | 34 | #x cases x -x |
---|
[2225] | 35 | [ #H % |
---|
[2152] | 36 | | #sigma normalize nodelta #H @conj [ @conj |
---|
| 37 | [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) |
---|
[2153] | 38 | | @(proj2 ?? (proj1 ?? (proj1 ?? H))) |
---|
[2008] | 39 | ] |
---|
[2034] | 40 | | @(proj2 ?? H) |
---|
| 41 | ] |
---|
[1879] | 42 | ] |
---|
[2225] | 43 | | % |
---|
[2059] | 44 | | cases no_ch in p1; #p1 |
---|
[2101] | 45 | [ @(pi2 ?? (jump_expansion_internal program m)) |
---|
[2225] | 46 | | cases (jump_expansion_step ???) |
---|
[2034] | 47 | #x cases x -x #ch2 #z2 cases z2 normalize nodelta |
---|
[2225] | 48 | [ #_ % |
---|
[2152] | 49 | | #j2 #H2 @conj [ @conj |
---|
| 50 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) |
---|
[2153] | 51 | | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) |
---|
[2059] | 52 | ] |
---|
[2034] | 53 | | @(proj2 ?? H2) |
---|
| 54 | ] |
---|
[1809] | 55 | ] |
---|
[1810] | 56 | ] |
---|
[2034] | 57 | | cases (jump_expansion_internal program m) in p1; |
---|
| 58 | #p cases p -p #p #r cases r normalize nodelta |
---|
| 59 | [ #_ >p2 #ABS destruct (ABS) |
---|
| 60 | | #map >p2 normalize nodelta |
---|
[2152] | 61 | #H #eq destruct (eq) @H |
---|
[2034] | 62 | ] |
---|
[1614] | 63 | ] |
---|
| 64 | qed. |
---|
[1810] | 65 | |
---|
[2153] | 66 | |
---|
[2101] | 67 | lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program). |
---|
[1809] | 68 | #program whd #x whd #n #Hn |
---|
[1937] | 69 | cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉) |
---|
[1931] | 70 | #y #z normalize nodelta @refl |
---|
[1809] | 71 | qed. |
---|
[1614] | 72 | |
---|
[2101] | 73 | lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program). |
---|
[1809] | 74 | #program whd #x #y #Hxy whd #n #Hn |
---|
[1937] | 75 | lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) |
---|
[1931] | 76 | #x1 #x2 |
---|
[1937] | 77 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) |
---|
[1931] | 78 | #y1 #y2 normalize nodelta // |
---|
[1809] | 79 | qed. |
---|
| 80 | |
---|
[2101] | 81 | lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program). |
---|
| 82 | #program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?); |
---|
| 83 | whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy |
---|
[1937] | 84 | lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) |
---|
[1931] | 85 | #x1 #x2 |
---|
[1937] | 86 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2 |
---|
| 87 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2 |
---|
[1931] | 88 | normalize nodelta // |
---|
[1809] | 89 | qed. |
---|
| 90 | |
---|
[1931] | 91 | definition policy_equal_opt ≝ |
---|
| 92 | λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map. |
---|
[1809] | 93 | match p1 with |
---|
| 94 | [ Some x1 ⇒ match p2 with |
---|
[2101] | 95 | [ Some x2 ⇒ sigma_jump_equal program x1 x2 |
---|
[1809] | 96 | | _ ⇒ False |
---|
| 97 | ] |
---|
| 98 | | None ⇒ p2 = None ? |
---|
| 99 | ]. |
---|
[1614] | 100 | |
---|
[1931] | 101 | lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program). |
---|
[2225] | 102 | #program whd #x whd cases x try % #y @pe_int_refl |
---|
[1614] | 103 | qed. |
---|
| 104 | |
---|
[1931] | 105 | lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program). |
---|
[1809] | 106 | #program whd #x #y #Hxy whd cases y in Hxy; |
---|
| 107 | [ cases x |
---|
[2225] | 108 | [ #_ % |
---|
[1809] | 109 | | #x' #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 110 | ] |
---|
| 111 | | #y' cases x |
---|
[1931] | 112 | [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H) |
---|
[1809] | 113 | | #x' #H @pe_int_sym @H |
---|
| 114 | ] |
---|
| 115 | ] |
---|
[1614] | 116 | qed. |
---|
| 117 | |
---|
[1931] | 118 | lemma pe_trans: ∀program.transitive ? (policy_equal_opt program). |
---|
[1809] | 119 | #program whd #x #y #z cases x |
---|
| 120 | [ #Hxy #Hyz >Hxy in Hyz; // |
---|
| 121 | | #x' cases y |
---|
| 122 | [ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 123 | | #y' cases z |
---|
| 124 | [ #_ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
| 125 | | #z' @pe_int_trans |
---|
| 126 | ] |
---|
| 127 | ] |
---|
| 128 | ] |
---|
[1614] | 129 | qed. |
---|
| 130 | |
---|
[1809] | 131 | definition step_none: ∀program.∀n. |
---|
| 132 | (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? → |
---|
| 133 | ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?. |
---|
| 134 | #program #n lapply (refl ? (jump_expansion_internal program n)) |
---|
| 135 | cases (jump_expansion_internal program n) in ⊢ (???% → %); |
---|
| 136 | #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k |
---|
| 137 | [ <plus_n_O >Heqj @Hj |
---|
[2101] | 138 | | #k' -k <plus_n_Sm |
---|
[1810] | 139 | lapply (refl ? (jump_expansion_internal program (n+k'))) |
---|
[2034] | 140 | cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %); |
---|
[1879] | 141 | #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2 |
---|
| 142 | cases p2 in H Heqj2; |
---|
[1809] | 143 | [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); |
---|
| 144 | >Heqj2 normalize nodelta @refl |
---|
| 145 | | #x #H #Heqj2 #abs destruct (abs) |
---|
| 146 | ] |
---|
| 147 | ] |
---|
| 148 | qed. |
---|
| 149 | |
---|
[2153] | 150 | lemma jump_pc_equal: ∀program.∀n. |
---|
| 151 | match \snd (jump_expansion_internal program n) with |
---|
| 152 | [ None ⇒ True |
---|
| 153 | | Some p1 ⇒ match \snd (jump_expansion_internal program (S n)) with |
---|
| 154 | [ None ⇒ True |
---|
| 155 | | Some p2 ⇒ sigma_jump_equal program p1 p2 → sigma_pc_equal program p1 p2 |
---|
| 156 | ] |
---|
| 157 | ]. |
---|
| 158 | #program #n lapply (refl ? (jump_expansion_internal program n)) |
---|
| 159 | cases (jump_expansion_internal program n) in ⊢ (???% → %); #x cases x -x |
---|
| 160 | #Nno_ch #No cases No |
---|
| 161 | [ normalize nodelta #HN #NEQ @I |
---|
| 162 | | #Npol normalize nodelta #HN #NEQ lapply (refl ? (jump_expansion_internal program (S n))) |
---|
| 163 | cases (jump_expansion_internal program (S n)) in ⊢ (???% → %); #x cases x -x |
---|
| 164 | #Sno_ch #So cases So |
---|
| 165 | [ normalize nodelta #HS #SEQ @I |
---|
| 166 | | #Spol normalize nodelta #HS #SEQ #Hj |
---|
| 167 | whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*) |
---|
| 168 | >NEQ in SEQ; normalize nodelta cases Nno_ch in HN; |
---|
| 169 | [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ)))) |
---|
| 170 | / by / |
---|
[2225] | 171 | | #HN normalize nodelta cases (jump_expansion_step ???) |
---|
[2153] | 172 | #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o |
---|
| 173 | [ normalize nodelta #_ #H destruct (H) |
---|
| 174 | | #Stno_p normalize nodelta #HSt #STeq |
---|
| 175 | <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? STeq)))) in Hj; #Hj |
---|
| 176 | @(proj2 ?? (proj1 ?? HSt)) @(proj2 ?? (proj1 ?? (proj1 ?? HSt))) @Hj |
---|
| 177 | ] |
---|
| 178 | ] |
---|
| 179 | ] |
---|
| 180 | ] |
---|
[2225] | 181 | qed. |
---|
[2153] | 182 | |
---|
[2141] | 183 | lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
[1931] | 184 | ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n))) |
---|
[1809] | 185 | (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → |
---|
[1931] | 186 | policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) |
---|
[1809] | 187 | (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). |
---|
[2316] | 188 | #program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x |
---|
| 189 | #no_ch #pol cases pol normalize nodelta |
---|
| 190 | [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O |
---|
| 191 | #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by / |
---|
| 192 | | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???); |
---|
| 193 | lapply (refl ? (jump_expansion_internal program (S n))) |
---|
| 194 | whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn |
---|
| 195 | normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq |
---|
| 196 | [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n)))) |
---|
| 197 | whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq |
---|
| 198 | normalize nodelta #Teq >Teq @pe_refl |
---|
| 199 | | #Heq lapply (refl ? (jump_expansion_internal program (S (S n)))) |
---|
| 200 | whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq |
---|
[2653] | 201 | normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*) |
---|
[2316] | 202 | #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol |
---|
| 203 | [ normalize nodelta #HSn #Heq #Seq cases Heq |
---|
| 204 | | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq |
---|
| 205 | [ @pe_refl |
---|
| 206 | | cases daemon |
---|
| 207 | ] |
---|
| 208 | ] |
---|
| 209 | ] |
---|
| 210 | ] |
---|
[1614] | 211 | qed. |
---|
| 212 | |
---|
[2141] | 213 | lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction. |
---|
| 214 | S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ. |
---|
[1931] | 215 | policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
[1809] | 216 | (\snd (pi1 … (jump_expansion_internal program (S n)))) → |
---|
[1931] | 217 | ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
[1809] | 218 | (\snd (pi1 … (jump_expansion_internal program k))). |
---|
| 219 | #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k; |
---|
| 220 | lapply Heq -Heq; lapply n -n; elim z -z; |
---|
| 221 | [ #n #Heq <plus_n_O @pe_refl |
---|
| 222 | | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); |
---|
| 223 | @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n))))) |
---|
| 224 | [ @Heq |
---|
| 225 | | @Hind @pe_step @Heq |
---|
| 226 | ] |
---|
| 227 | ] |
---|
[1614] | 228 | qed. |
---|
| 229 | |
---|
[1809] | 230 | (* this number monotonically increases over iterations, maximum 2*|program| *) |
---|
[1931] | 231 | let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ) |
---|
[1614] | 232 | on program: ℕ ≝ |
---|
| 233 | match program with |
---|
| 234 | [ nil ⇒ acc |
---|
[2034] | 235 | | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with |
---|
[1937] | 236 | [ long_jump ⇒ measure_int t policy (acc + 2) |
---|
[2101] | 237 | | absolute_jump ⇒ measure_int t policy (acc + 1) |
---|
[1937] | 238 | | _ ⇒ measure_int t policy acc |
---|
[1614] | 239 | ] |
---|
| 240 | ]. |
---|
| 241 | |
---|
| 242 | lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. |
---|
[1809] | 243 | measure_int program policy (x+d) = measure_int program policy x + d. |
---|
| 244 | #program #policy #x #d generalize in match x; -x elim d |
---|
| 245 | [ // |
---|
| 246 | | -d; #d #Hind elim program |
---|
| 247 | [ / by refl/ |
---|
| 248 | | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); |
---|
[2034] | 249 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) |
---|
[1809] | 250 | [ normalize nodelta @Hd |
---|
[1937] | 251 | |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus |
---|
| 252 | @Hd |
---|
[1809] | 253 | ] |
---|
| 254 | ] |
---|
| 255 | ] |
---|
[1614] | 256 | qed. |
---|
[1809] | 257 | |
---|
| 258 | lemma measure_le: ∀program.∀policy. |
---|
| 259 | measure_int program policy 0 ≤ 2*|program|. |
---|
| 260 | #program #policy elim program |
---|
| 261 | [ normalize @le_n |
---|
| 262 | | #h #t #Hind whd in match (measure_int ???); |
---|
[2034] | 263 | cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) |
---|
[1809] | 264 | [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ |
---|
[1937] | 265 | |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) |
---|
| 266 | @le_plus [1,3: @Hind |2,4: / by le_n/ ] |
---|
[1809] | 267 | ] |
---|
| 268 | ] |
---|
| 269 | qed. |
---|
| 270 | |
---|
[1940] | 271 | (* uses the second part of policy_increase *) |
---|
[2141] | 272 | lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction. |
---|
| 273 | S (|l|) <2^16 ∧ is_well_labelled_p l). |
---|
[1931] | 274 | ∀policy:Σp:ppc_pc_map. |
---|
[2141] | 275 | (*out_of_program_none program p ∧*) |
---|
[2101] | 276 | not_jump_default program p ∧ |
---|
[2034] | 277 | \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ |
---|
[2059] | 278 | \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ |
---|
[2225] | 279 | sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧ |
---|
[2211] | 280 | \fst p ≤ 2^16. |
---|
[1809] | 281 | ∀l.|l| ≤ |program| → ∀acc:ℕ. |
---|
[2225] | 282 | match \snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy)) with |
---|
[1809] | 283 | [ None ⇒ True |
---|
| 284 | | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc |
---|
| 285 | ]. |
---|
[2264] | 286 | [2: #l #_ %] |
---|
[1614] | 287 | #program #policy #l elim l -l; |
---|
[1809] | 288 | [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] |
---|
| 289 | | #h #t #Hind #Hp #acc |
---|
[2225] | 290 | inversion (jump_expansion_step ???) #pi1 cases pi1 -pi1 #c #r cases r |
---|
[1879] | 291 | [ / by I/ |
---|
[2008] | 292 | | #x normalize nodelta #Hx #Hjeq |
---|
[2141] | 293 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp)) |
---|
[1809] | 294 | whd in match (measure_int ???); whd in match (measure_int ? x ?); |
---|
[2034] | 295 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉) |
---|
| 296 | #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉) |
---|
[2008] | 297 | #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 |
---|
[1937] | 298 | [1,4,5,7,8,9: #H cases H |
---|
| 299 | |2,3,6: #_ normalize nodelta |
---|
| 300 | [1,2: @(transitive_le ? (measure_int t x acc)) |
---|
| 301 | |3: @(transitive_le ? (measure_int t x (acc+1))) |
---|
| 302 | ] |
---|
| 303 | [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] |
---|
| 304 | >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
| 305 | |11,12,13,15,16,17: #H destruct (H) |
---|
| 306 | |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
| 307 | ] |
---|
| 308 | ] |
---|
| 309 | ] |
---|
[1614] | 310 | qed. |
---|
| 311 | |
---|
| 312 | lemma measure_full: ∀program.∀policy. |
---|
| 313 | measure_int program policy 0 = 2*|program| → ∀i.i<|program| → |
---|
[2652] | 314 | is_jump (\snd (nth i ? program 〈None ?,Comment EmptyString〉)) → |
---|
[2034] | 315 | (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. |
---|
[1937] | 316 | #program #policy elim program in ⊢ (% → ∀i.% → ? → %); |
---|
[1809] | 317 | [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
[1937] | 318 | | #h #t #Hind #Hm #i #Hi #Hj |
---|
| 319 | cases (le_to_or_lt_eq … Hi) -Hi |
---|
| 320 | [ #Hi @Hind |
---|
| 321 | [ whd in match (measure_int ???) in Hm; |
---|
[2034] | 322 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm; |
---|
[1937] | 323 | normalize nodelta |
---|
[2700] | 324 | [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le |
---|
| 325 | @monotonic_lt_times_r [/2/] % |
---|
[1931] | 326 | | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) |
---|
[1937] | 327 | <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ |
---|
| 328 | | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ |
---|
[1931] | 329 | ] |
---|
[1937] | 330 | | @(le_S_S_to_le … Hi) |
---|
| 331 | | @Hj |
---|
[1809] | 332 | ] |
---|
| 333 | | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; |
---|
[2034] | 334 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm; |
---|
[1809] | 335 | normalize nodelta |
---|
[2700] | 336 | [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le |
---|
| 337 | @monotonic_lt_times_r try % /2/ |
---|
[1937] | 338 | | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) |
---|
| 339 | <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ |
---|
| 340 | | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ |
---|
[1809] | 341 | ] |
---|
[1937] | 342 | ] |
---|
[1809] | 343 | ] |
---|
[1614] | 344 | qed. |
---|
| 345 | |
---|
[1940] | 346 | (* uses second part of policy_increase *) |
---|
[2141] | 347 | lemma measure_special: ∀program:(Σl:list labelled_instruction. |
---|
| 348 | (S (|l|)) < 2^16 ∧ is_well_labelled_p l). |
---|
[1931] | 349 | ∀policy:Σp:ppc_pc_map. |
---|
[2141] | 350 | not_jump_default program p ∧ |
---|
[2034] | 351 | \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ |
---|
[2059] | 352 | \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ |
---|
[2225] | 353 | sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧ |
---|
[2211] | 354 | \fst p ≤ 2^16. |
---|
[2225] | 355 | match (\snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy))) with |
---|
[1809] | 356 | [ None ⇒ True |
---|
[2101] | 357 | | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ]. |
---|
[2264] | 358 | [2: #l #_ %] |
---|
[2225] | 359 | #program #policy inversion (jump_expansion_step ???) |
---|
[1879] | 360 | #p cases p -p #ch #pol normalize nodelta cases pol |
---|
| 361 | [ / by I/ |
---|
[1809] | 362 | | #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|)) |
---|
| 363 | @(list_ind ? (λx.|x| ≤ |pi1 ?? program| → |
---|
| 364 | measure_int x policy 0 = measure_int x p 0 → |
---|
[2101] | 365 | sigma_jump_equal x policy p) ?? (pi1 ?? program)) |
---|
[2034] | 366 | [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n |
---|
| 367 | | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 368 | [ @Hind |
---|
[1879] | 369 | [ @(transitive_le … Hp) / by / |
---|
[1809] | 370 | | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; |
---|
[2141] | 371 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp)) |
---|
[2059] | 372 | #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; |
---|
| 373 | #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); |
---|
| 374 | #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta |
---|
[1937] | 375 | cases x2 cases y2 normalize nodelta |
---|
| 376 | [1: / by / |
---|
| 377 | |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
| 378 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
| 379 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
[1965] | 380 | |4,7,8: #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ] |
---|
[1937] | 381 | |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) |
---|
| 382 | #_ #H @(injective_plus_r … H) |
---|
| 383 | |6: >measure_plus >measure_plus |
---|
| 384 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
| 385 | #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
| 386 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
| 387 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
| 388 | |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) |
---|
| 389 | #_ #H @(injective_plus_r … H) |
---|
| 390 | ] |
---|
[2034] | 391 | | @Hi |
---|
[1614] | 392 | ] |
---|
[2034] | 393 | | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; |
---|
[2141] | 394 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp)) |
---|
[2034] | 395 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm; |
---|
[1940] | 396 | #x1 #x2 |
---|
[2034] | 397 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2 |
---|
[1940] | 398 | normalize nodelta cases x2 cases y2 normalize nodelta |
---|
[1965] | 399 | [1,5,9: #_ #_ @refl |
---|
| 400 | |4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ] |
---|
[1809] | 401 | |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
| 402 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
| 403 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
| 404 | |6: >measure_plus >measure_plus |
---|
| 405 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
| 406 | #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
| 407 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
[1931] | 408 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
[1965] | 409 | ] |
---|
[1614] | 410 | ] |
---|
[1809] | 411 | ] |
---|
[1614] | 412 | qed. |
---|
| 413 | |
---|
[2141] | 414 | lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction. |
---|
| 415 | S (|l|) < 2^16 ∧ is_well_labelled_p l. |
---|
[1940] | 416 | match jump_expansion_start program (create_label_map program) with |
---|
| 417 | [ None ⇒ True |
---|
| 418 | | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0 |
---|
| 419 | ]. |
---|
| 420 | #l #program lapply (refl ? (jump_expansion_start program (create_label_map program))) |
---|
| 421 | cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ |
---|
| 422 | cases p in Hp EQ; |
---|
| 423 | [ / by I/ |
---|
| 424 | | #pl normalize nodelta #Hpl #EQ elim l |
---|
| 425 | [ / by refl/ |
---|
[1965] | 426 | | #h #t #Hind #Hp whd in match (measure_int ???); |
---|
[2141] | 427 | elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp)) |
---|
[2008] | 428 | #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind |
---|
| 429 | @(transitive_le … Hp) @le_n_Sn |
---|
[1965] | 430 | ] |
---|
[2034] | 431 | ] |
---|
[1614] | 432 | qed. |
---|
| 433 | |
---|
[1809] | 434 | (* the actual computation of the fixpoint *) |
---|
[2141] | 435 | definition je_fixpoint: ∀program:(Σl:list labelled_instruction. |
---|
| 436 | S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
[1932] | 437 | Σp:option ppc_pc_map. |
---|
[2101] | 438 | match p with |
---|
[1932] | 439 | [ None ⇒ True |
---|
[2211] | 440 | | Some pol ⇒ And (And (And |
---|
| 441 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) |
---|
| 442 | (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉))) |
---|
[2225] | 443 | (sigma_compact program (pi1 … (create_label_map program)) pol)) |
---|
[2211] | 444 | (\fst pol ≤ 2^16) |
---|
[2101] | 445 | ]. |
---|
| 446 | #program @(\snd (jump_expansion_internal program (S (2*|program|)))) |
---|
| 447 | cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) |
---|
[1809] | 448 | (\snd (pi1 ?? (jump_expansion_internal program k))) |
---|
| 449 | (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|)) |
---|
[2101] | 450 | [ #Hex cases Hex -Hex #k #Hk |
---|
[2225] | 451 | inversion (jump_expansion_internal ??) |
---|
[2101] | 452 | #x cases x -x #Gno_ch #Go cases Go normalize nodelta |
---|
| 453 | [ #H #Heq / by I/ |
---|
| 454 | | -Go #Gp #HGp #Geq |
---|
| 455 | cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*|program|))) |
---|
| 456 | (\snd (jump_expansion_internal program (S (2*|program|))))) |
---|
| 457 | [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*|program|)) (le_S … (le_S_to_le … (proj1 ?? Hk))))) |
---|
| 458 | @pe_sym @equal_remains_equal [ @(proj2 ?? Hk) | @(le_S_to_le … (proj1 ?? Hk)) ] |
---|
| 459 | | >Geq lapply (refl ? (jump_expansion_internal program (2*|program|))) |
---|
| 460 | cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %); |
---|
| 461 | #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta |
---|
| 462 | [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS) |
---|
| 463 | | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq |
---|
[2211] | 464 | @conj [ @conj [ @conj |
---|
| 465 | [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) |
---|
| 466 | | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) |
---|
| 467 | ] |
---|
[2225] | 468 | | @(equal_compact_unsafe_compact ? Fp) |
---|
[2153] | 469 | [ lapply (jump_pc_equal program (2*|program|)) |
---|
| 470 | >Feq >Geq normalize nodelta #H @H @Heq |
---|
[2316] | 471 | | @Heq |
---|
[2211] | 472 | | cases daemon (* true, but have to add this to properties *) |
---|
[2316] | 473 | | cases daemon |
---|
[2152] | 474 | | @(proj2 ?? (proj1 ?? HGp)) |
---|
| 475 | ] |
---|
[2101] | 476 | ] |
---|
[2211] | 477 | | @(proj2 ?? HGp) |
---|
| 478 | ] |
---|
[2101] | 479 | ] |
---|
[1809] | 480 | ] |
---|
| 481 | ] |
---|
[2101] | 482 | | #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa |
---|
| 483 | lapply (refl ? (jump_expansion_internal program (2*|program|))) |
---|
| 484 | cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %); |
---|
| 485 | #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta |
---|
| 486 | [ (* None *) |
---|
| 487 | #HF #Feq lapply (step_none program (2*|program|) ? 1) >Feq / by / |
---|
| 488 | <plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/ |
---|
| 489 | | -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?) |
---|
| 490 | [ @le_to_le_to_eq |
---|
| 491 | [ @measure_le |
---|
| 492 | | cut (∀x:ℕ.x ≤ 2*|program| → |
---|
| 493 | ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ |
---|
| 494 | x ≤ measure_int program p 0)) |
---|
| 495 | [ #x elim x |
---|
| 496 | [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program))) |
---|
| 497 | cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); |
---|
| 498 | #z cases z -z normalize nodelta |
---|
| 499 | [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn |
---|
| 500 | @(absurd … (step_none program 0 ? n)) |
---|
| 501 | [ whd in match (jump_expansion_internal ??); >Heqn @refl |
---|
| 502 | | <Hn >Feq @nmk #H destruct (H) |
---|
| 503 | ] |
---|
| 504 | | #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj |
---|
| 505 | [ whd in match (jump_expansion_internal ??); >Zeq @refl |
---|
| 506 | | @le_O_n |
---|
| 507 | ] |
---|
| 508 | ] |
---|
| 509 | | -x #x #Hind #Hx |
---|
| 510 | lapply (refl ? (jump_expansion_internal program (S x))) |
---|
| 511 | cases (jump_expansion_internal program (S x)) in ⊢ (???% → %); |
---|
| 512 | #z cases z -z #Sno_ch #So cases So -So |
---|
| 513 | [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk |
---|
| 514 | @(absurd … (step_none program (S x) ? k)) |
---|
| 515 | [ >Seq @refl |
---|
| 516 | | <Hk >Feq @nmk #H destruct (H) |
---|
| 517 | ] |
---|
| 518 | | #Sp #HSp #Seq @(ex_intro ?? Sp) @conj |
---|
| 519 | [ @refl |
---|
| 520 | | elim (Hind (transitive_le … (le_n_Sn x) Hx)) |
---|
| 521 | #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol)) |
---|
| 522 | lapply (proj1 ?? Hpol) -Hpol |
---|
| 523 | lapply (refl ? (jump_expansion_internal program x)) |
---|
| 524 | cases (jump_expansion_internal program x) in ⊢ (???% → %); |
---|
| 525 | #z cases z -z #Xno_ch #Xo cases Xo |
---|
| 526 | [ #HXp #Xeq #abs destruct (abs) |
---|
| 527 | | normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol |
---|
| 528 | lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt; |
---|
| 529 | normalize nodelta #Hpe |
---|
| 530 | lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0) |
---|
[2153] | 531 | [ @HXp |
---|
[2101] | 532 | | lapply (Hfa x Hx) >Xeq >Seq |
---|
| 533 | lapply (measure_special program «Xp,?») |
---|
[2153] | 534 | [ @HXp |
---|
[2101] | 535 | | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*) |
---|
| 536 | >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq |
---|
| 537 | [ normalize nodelta #EQ |
---|
| 538 | >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ))) |
---|
| 539 | #_ #abs @⊥ @(absurd ?? abs) / by / |
---|
| 540 | | normalize nodelta cases (jump_expansion_step ???); |
---|
| 541 | #z cases z -z #stch #sto cases sto |
---|
| 542 | [ normalize nodelta #_ #ABS destruct (ABS) |
---|
| 543 | | -sto #stp normalize nodelta #Hstp #steq |
---|
| 544 | >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq)))) |
---|
| 545 | #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp) |
---|
| 546 | [ / by / |
---|
| 547 | | #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp |
---|
[1879] | 548 | ] |
---|
| 549 | ] |
---|
[2101] | 550 | ] |
---|
[1879] | 551 | ] |
---|
| 552 | ] |
---|
[2101] | 553 | ] |
---|
[1879] | 554 | ] |
---|
[2101] | 555 | ] |
---|
[1810] | 556 | ] |
---|
[2101] | 557 | | #H elim (H (2*|program|) (le_n ?)) #plp >Feq #Hplp |
---|
| 558 | >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp) |
---|
| 559 | ] |
---|
| 560 | ] |
---|
[2153] | 561 | | #Hfull lapply (refl ? (jump_expansion_internal program (S (2*|program|)))) |
---|
| 562 | cases (jump_expansion_internal program (S (2*|program|))) in ⊢ (???% → %); |
---|
| 563 | #z cases z -z #Gch #Go cases Go normalize nodelta |
---|
| 564 | [ #HGp #Geq @I |
---|
[2211] | 565 | | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj |
---|
| 566 | [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) |
---|
| 567 | | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) |
---|
| 568 | ] |
---|
[2225] | 569 | | @(equal_compact_unsafe_compact ? Fp) |
---|
[2317] | 570 | [1,2: |
---|
| 571 | [1: lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta |
---|
| 572 | #H @H ] |
---|
| 573 | #i #Hi |
---|
[2652] | 574 | inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) |
---|
[2317] | 575 | [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*) |
---|
[2153] | 576 | >Feq in Geq; normalize nodelta cases Fno_ch |
---|
[2317] | 577 | [1,3: normalize nodelta #Heq |
---|
[2153] | 578 | >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) % |
---|
[2317] | 579 | |2,4: normalize nodelta cases (jump_expansion_step ???) |
---|
[2153] | 580 | #x cases x -x #stch #sto normalize nodelta cases sto |
---|
[2317] | 581 | [1,3: normalize nodelta #_ #X destruct (X) |
---|
| 582 | |2,4: -sto #stp normalize nodelta #Hst #Heq |
---|
[2153] | 583 | <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) |
---|
| 584 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi)) |
---|
[2317] | 585 | lapply (Hfull i Hi ?) [1,3: >Hj %] |
---|
[2153] | 586 | cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) |
---|
| 587 | #fp #fj #Hfj >Hfj normalize nodelta |
---|
| 588 | cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) |
---|
| 589 | #stp #stj cases stj normalize nodelta |
---|
[2317] | 590 | [1,2,4,5: #H cases H #H2 cases H2 destruct (H2) |
---|
| 591 | |3,6: #_ @refl |
---|
[2153] | 592 | ] |
---|
[2317] | 593 | ] |
---|
[1809] | 594 | ] |
---|
[2317] | 595 | |2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %] |
---|
| 596 | >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] % |
---|
[1809] | 597 | ] |
---|
[2317] | 598 | | cases daemon (* true, but have to add to properties in some way *) |
---|
| 599 | | cases daemon |
---|
| 600 | | @(proj2 ?? (proj1 ?? HGp)) |
---|
[1809] | 601 | ] |
---|
[1810] | 602 | ] |
---|
[2317] | 603 | | @(proj2 ?? HGp) |
---|
| 604 | ] |
---|
[1809] | 605 | ] |
---|
| 606 | ] |
---|
| 607 | ] |
---|
[2317] | 608 | | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) |
---|
| 609 | #x cases x -x #nch #npol normalize nodelta #Hnpol |
---|
| 610 | #x cases x -x #Sch #Spol normalize nodelta #HSpol |
---|
| 611 | cases npol in Hnpol; cases Spol in HSpol; |
---|
| 612 | [ #Hnpol #HSpol %1 // |
---|
| 613 | |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // |
---|
| 614 | #H destruct (H) |
---|
| 615 | |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m |
---|
| 616 | cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) |
---|
| 617 | #x1 #x2 |
---|
| 618 | cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) |
---|
| 619 | #y1 #y2 normalize nodelta |
---|
| 620 | @dec_eq_jump_length |
---|
| 621 | ] |
---|
| 622 | ] |
---|
[1810] | 623 | qed. |
---|
[1809] | 624 | |
---|
[1965] | 625 | include alias "arithmetics/nat.ma". |
---|
[1942] | 626 | include alias "basics/logic.ma". |
---|
| 627 | |
---|
[2211] | 628 | lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map. |
---|
| 629 | And (And (And |
---|
| 630 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0) |
---|
| 631 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
| 632 | (sigma_compact program (create_label_map program) p)) |
---|
| 633 | (\fst p ≤ 2^16).i ≤ j → j ≤ |program| → |
---|
| 634 | \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤ |
---|
| 635 | \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉). |
---|
| 636 | #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n |
---|
| 637 | [ <plus_n_O #_ @le_n |
---|
| 638 | | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H))) |
---|
[2318] | 639 | lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H) |
---|
[2211] | 640 | lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))) |
---|
| 641 | cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %); |
---|
| 642 | [ normalize nodelta #_ #abs cases abs |
---|
| 643 | | #x cases x -x #pc #jl #EQ normalize nodelta |
---|
| 644 | lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))) |
---|
| 645 | cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %); |
---|
| 646 | [ normalize nodelta #_ #abs cases abs |
---|
| 647 | | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp |
---|
| 648 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
| 649 | >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r |
---|
| 650 | ] |
---|
| 651 | ] |
---|
| 652 | ] |
---|
| 653 | qed. |
---|
| 654 | |
---|
[1809] | 655 | (* The glue between Policy and Assembly. *) |
---|
[1615] | 656 | definition jump_expansion': |
---|
[2152] | 657 | ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
[2078] | 658 | option (Σsigma_policy:(Word → Word) × (Word → bool). |
---|
| 659 | let 〈sigma,policy〉≝ sigma_policy in |
---|
[2101] | 660 | sigma_policy_specification 〈\fst program,\snd program〉 sigma policy) |
---|
| 661 | ≝ |
---|
[1965] | 662 | λprogram. |
---|
[2101] | 663 | let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in |
---|
| 664 | match f return λx.f = x → ? with |
---|
| 665 | [ None ⇒ λp.None ? |
---|
| 666 | | Some x ⇒ λp.Some ? |
---|
[2225] | 667 | «〈(λppc.let pc ≝ \fst (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in |
---|
[2078] | 668 | bitvector_of_nat 16 pc), |
---|
[2225] | 669 | (λppc.let jl ≝ \snd (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in |
---|
[2078] | 670 | jmpeqb jl long_jump)〉,?» |
---|
[2101] | 671 | ] (refl ? f). |
---|
| 672 | normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta |
---|
| 673 | lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x |
---|
[2229] | 674 | #fpc #fpol #Hfpol cases Hfpol ** #Hfpol1 #Hfpol2 #Hfpol3 #Hfpol4 |
---|
[2101] | 675 | @conj |
---|
[2229] | 676 | [ >Hfpol1 % |
---|
[2228] | 677 | | #ppc #ppc_ok normalize nodelta |
---|
| 678 | >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) = |
---|
[2652] | 679 | \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)) |
---|
[2228] | 680 | [2: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
[2652] | 681 | >(nth_safe_nth … 〈None ?, Comment EmptyString〉) |
---|
| 682 | cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉) |
---|
[2228] | 683 | #lbl #ins % ] |
---|
[2318] | 684 | lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok) |
---|
| 685 | [2: >bitvector_of_nat_inverse_nat_of_bitvector |
---|
[2230] | 686 | inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ] |
---|
| 687 | * #pc #jl #Hl normalize nodelta |
---|
| 688 | inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ] |
---|
| 689 | * #Spc #Sjl #SHL lapply SHL |
---|
| 690 | <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative |
---|
| 691 | #SHl normalize nodelta #Hcompact |
---|
[2228] | 692 | @conj |
---|
[2230] | 693 | [ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) |
---|
| 694 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) |
---|
| 695 | >add_bitvector_of_nat_plus >Hcompact % |
---|
[2211] | 696 | | (* Basic proof scheme: |
---|
| 697 | - ppc < |snd program|, hence our instruction is in the program |
---|
| 698 | - either we are the last non-zero-size instruction, in which case we are |
---|
| 699 | either smaller than 2^16 (because the entire program is), or we are exactly |
---|
| 700 | 2^16 and something weird happens |
---|
| 701 | - or we are not, in which case we are definitely smaller than 2^16 (by transitivity |
---|
| 702 | through the next non-zero instruction) |
---|
| 703 | *) |
---|
[2229] | 704 | elim (le_to_or_lt_eq … Hfpol4) #Hfpc |
---|
| 705 | [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2 |
---|
[2230] | 706 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) |
---|
| 707 | >nat_of_bitvector_bitvector_of_nat_inverse |
---|
| 708 | [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) |
---|
| 709 | >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) |
---|
| 710 | #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ] |
---|
| 711 | lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) |
---|
| 712 | >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X |
---|
[2211] | 713 | | (* the program is of length 2^16 and ppc is followed by only zero-size instructions |
---|
| 714 | * until the end of the program *) |
---|
| 715 | elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))) |
---|
[2230] | 716 | [ >bitvector_of_nat_inverse_nat_of_bitvector |
---|
| 717 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta |
---|
| 718 | >nat_of_bitvector_bitvector_of_nat_inverse |
---|
| 719 | [2: <Hfpc >Hfpol2 @Hpc ] |
---|
| 720 | elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))) |
---|
| 721 | <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc |
---|
| 722 | [ %1 >Hcompact in HSpc; #X @X |
---|
| 723 | | %2 @conj |
---|
| 724 | [2: >Hcompact in HSpc; #X @X |
---|
| 725 | | #ppc' #ppc_ok' #Hppc' |
---|
[2318] | 726 | (* S ppc < ppc' < |\snd program| *) |
---|
| 727 | (* lookup S ppc = 2^16 *) |
---|
| 728 | (* lookup |\snd program| = 2^16 *) |
---|
| 729 | (* lookup ppc' = 2^16 → instruction size = 0 *) |
---|
| 730 | lapply (Hfpol3 ? (nat_of_bitvector ? ppc') ppc_ok') |
---|
| 731 | [2: >bitvector_of_nat_inverse_nat_of_bitvector |
---|
| 732 | inversion (lookup_opt ????) normalize nodelta |
---|
| 733 | [ #_ #abs cases abs |
---|
| 734 | | * #xpc #xjl #XEQ normalize nodelta |
---|
| 735 | inversion (lookup_opt ????) normalize nodelta |
---|
| 736 | [ #_ #abs cases abs |
---|
| 737 | | * #Sxpc #Sxjl #SXEQ normalize nodelta |
---|
| 738 | #Hpcompact |
---|
| 739 | lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok')) |
---|
| 740 | >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1 |
---|
| 741 | lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?)) |
---|
| 742 | <Hfpol2 >Hfpc #Hle2 |
---|
| 743 | lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1 |
---|
[2211] | 744 | >bitvector_of_nat_inverse_nat_of_bitvector |
---|
[2318] | 745 | >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc |
---|
| 746 | lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok') |
---|
| 747 | >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1 |
---|
| 748 | lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?)) |
---|
| 749 | <Hfpol2 >Hfpc #Hle2 |
---|
| 750 | lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2 |
---|
| 751 | >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc |
---|
| 752 | >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H |
---|
| 753 | @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction; |
---|
[2652] | 754 | normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉) |
---|
| 755 | cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H; |
---|
[2318] | 756 | #lbl #ins normalize nodelta #X @sym_eq @X |
---|
| 757 | ] |
---|
| 758 | ] ] |
---|
[2211] | 759 | ] |
---|
| 760 | ] |
---|
| 761 | | >bitvector_of_nat_inverse_nat_of_bitvector |
---|
[2230] | 762 | <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc |
---|
| 763 | %1 >Hpc |
---|
[2211] | 764 | >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?)); |
---|
| 765 | <plus_O_n whd in match instruction_size; normalize nodelta |
---|
[2318] | 766 | inversion (assembly_1_pseudoinstruction ??? ppc ??) |
---|
[2230] | 767 | #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass) |
---|
| 768 | #Hli >Hli |
---|
[2318] | 769 | lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc ??) |
---|
| 770 | [6: >Hass / by / ] |
---|
[2211] | 771 | ] |
---|
| 772 | ] |
---|
[2318] | 773 | ] ] |
---|
[2101] | 774 | ] |
---|
[2652] | 775 | qed. |
---|