source: src/ASM/Policy.ma @ 2227

Last change on this file since 2227 was 2225, checked in by sacerdot, 8 years ago

Minor and major improvements everywhere, shortened proofs.

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