source: src/ASM/Policy.ma

Last change on this file was 3078, checked in by tranquil, 7 years ago

fixed change of Mov

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