source: src/ASM/Assembly.ma @ 1614

Last change on this file since 1614 was 1614, checked in by boender, 8 years ago
  • split policy from assembly
File size: 21.2 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Status.ma".
5include alias "basics/logic.ma".
6include alias "arithmetics/nat.ma".
7include "utilities/extralib.ma".
8include "ASM/Policy.ma".
9
10(**************************************** START OF POLICY ABSTRACTION ********************)
11
12definition policy_type ≝ Word → jump_length.
13
14definition jump_expansion':
15 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
16 policy_type ≝
17 λprogram.λpc.
18  let policy ≝
19    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
20  lookup ? ? pc policy long_jump.
21/2 by Stub, mk_Sig/
22qed.
23
24definition assembly_1_pseudoinstruction_safe ≝
25  λprogram: pseudo_assembly_program.
26  λjump_expansion: policy_type.
27  λppc: Word.
28  λpc: Word.
29  λlookup_labels.
30  λlookup_datalabels.
31  λi.
32  let expansion ≝ jump_expansion ppc in
33    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
34    [ None ⇒ None ?
35    | Some pseudos ⇒
36      let mapped ≝ map ? ? assembly1 pseudos in
37      let flattened ≝ flatten ? mapped in
38      let pc_len ≝ length ? flattened in
39        Some ? (〈pc_len, flattened〉)
40    ].
41 
42definition construct_costs_safe ≝
43  λprogram.
44  λjump_expansion: policy_type.
45  λpseudo_program_counter: nat.
46  λprogram_counter: nat.
47  λcosts: BitVectorTrie costlabel 16.
48  λi.
49  match i with
50  [ Cost cost ⇒
51    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
52      Some ? 〈program_counter, (insert … program_counter_bv cost costs)〉
53  | _ ⇒
54    let pc_bv ≝ bitvector_of_nat ? program_counter in
55    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
56    let lookup_labels ≝ λx.pc_bv in
57    let lookup_datalabels ≝ λx.zero ? in
58    let pc_delta_assembled ≝
59      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
60        lookup_labels lookup_datalabels i
61    in
62    match pc_delta_assembled with
63    [ None ⇒ None ?
64    | Some pc_delta_assembled ⇒
65      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
66        Some ? 〈pc_delta + program_counter, costs〉       
67    ]
68  ].
69
70(* This establishes the correspondence between pseudo program counters and
71   program counters. It is at the heart of the proof. *)
72(*CSC: code taken from build_maps *)
73definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
74 λinstr_list.
75 λjump_expansion: policy_type.
76 λl:list labelled_instruction.
77 λacc.
78  foldl …
79   (λt,i.
80       match t with
81       [ None ⇒ None …
82       | Some ppc_pc_map ⇒
83         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
84         let 〈program_counter, sigma_map〉 ≝ pc_map in
85         let 〈label, i〉 ≝ i in
86          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
87           [ None ⇒ None ?
88           | Some pc_ignore ⇒
89              let 〈pc,ignore〉 ≝ pc_ignore in
90                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
91       ]) acc l.
92
93definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
94  λprog.
95  λjump_expansion.
96    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
97
98definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
99 λprogram,jump_expansion,instr_list.
100  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
101   [ None ⇒ None …
102   | Some result ⇒
103      let 〈ppc,pc_sigma_map〉 ≝ result in
104      let 〈pc,map〉 ≝ pc_sigma_map in
105       Some … 〈ppc,pc〉 ].
106
107definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
108 λinstr_list,jump_expansion.
109  match sigma0 instr_list jump_expansion with
110  [ None ⇒ None ?
111  | Some result ⇒
112    let 〈ppc,pc_sigma_map〉 ≝ result in
113    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
114      if gtb pc (2^16) then
115        None ?
116      else
117        Some ? (λx. lookup … x sigma_map (zero …)) ].
118
119(* stuff about policy *)
120
121definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
122
123definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
124
125lemma eject_policy: ∀p. policy p → policy_type.
126 #p #pol @(pi1 … pol)
127qed.
128
129coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
130
131definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
132 λp,policy.
133  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
134   [ None ⇒ λabs. ⊥
135   | Some r ⇒ λ_.r] (pi2 … policy).
136 cases abs /2/
137qed.
138
139example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
140 cases daemon.
141qed.
142
143axiom fetch_pseudo_instruction_split:
144 ∀instr_list,ppc.
145  ∃pre,suff,lbl.
146   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
147
148lemma sigma00_append:
149 ∀instr_list,jump_expansion,l1,l2,acc.
150  sigma00 instr_list jump_expansion (l1@l2) acc =
151   sigma00 instr_list jump_expansion
152    l2 (sigma00 instr_list jump_expansion l1 acc).
153 whd in match sigma00; normalize nodelta;
154 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
155qed.
156
157lemma sigma00_strict:
158 ∀instr_list,jump_expansion,l,acc. acc = None ? →
159  sigma00 instr_list jump_expansion l acc = None ….
160 #instr_list #jump_expansion #l elim l
161  [ #acc #H >H %
162  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
163qed.
164
165lemma policy_ok_prefix_ok:
166 ∀program.∀pol:policy program.∀suffix,prefix.
167  prefix@suffix = \snd program →
168   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
169 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
170 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
171 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
172 normalize nodelta >sigma00_append
173 cases (sigma00 ?? prefix ?)
174  [2: #x #_ % #abs destruct(abs)
175  | * #abs @⊥ @abs >sigma00_strict % ]
176qed.
177
178lemma policy_ok_prefix_hd_ok:
179 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
180  (prefix@[hd])@suffix = \snd program →
181   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
182    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
183    let 〈program_counter, sigma_map〉 ≝ pc_map in
184    let 〈label, i〉 ≝ hd in
185     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
186 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
187 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
188  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
189 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
190 @pair_elim #pc #map #EQ4 normalize nodelta
191 @pair_elim #l' #i' #EQ5 normalize nodelta
192 cases (construct_costs_safe ??????) normalize
193  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
194qed.
195
196definition expand_pseudo_instruction:
197 ∀program:pseudo_assembly_program.∀pol: policy program.
198  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
199  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
200  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
201  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
202  pc = sigma program pol ppc →
203  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
204≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
205   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
206    [ None ⇒ let dummy ≝ [ ] in dummy
207    | Some res ⇒ res ].
208 [ @⊥ whd in p:(??%??);
209   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
210   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
211   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
212   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
213   #res #K
214   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
215   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
216   cases daemon (* CSC: XXXXXXXX Ero qui
217   
218    [3: @policy_ok_prefix_ok ]
219    | sigma00 program pol pre
220
221
222
223   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
224   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
225   per concludere construct_costs_safe ≠ None *)
226 | >p %]
227qed.
228
229(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
230definition assembly_1_pseudoinstruction':
231 ∀program:pseudo_assembly_program.∀pol: policy program.
232  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
233  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
234  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
235  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
236  Σres:(nat × (list Byte)).
237   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
238   let 〈len,code〉 ≝ res in
239    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
240     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
241≝ λprogram: pseudo_assembly_program.
242  λpol: policy program.
243  λppc: Word.
244  λlookup_labels.
245  λlookup_datalabels.
246  λpi.
247  λprf1,prf2,prf3.
248   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
249    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
250    | Some res ⇒ res ].
251 [ @⊥ elim pi in p; [*]
252   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
253   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
254   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
255   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
256   cases daemon
257 | % [ >p %]
258   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
259   (* THIS SHOULD BE TRUE INSTEAD *)
260   cases daemon]
261qed.
262
263definition assembly_1_pseudoinstruction:
264 ∀program:pseudo_assembly_program.∀pol: policy program.
265  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
266  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
267  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
268  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
269   nat × (list Byte)
270≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
271   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
272    prf2 prf3.
273
274lemma assembly_1_pseudoinstruction_ok1:
275 ∀program:pseudo_assembly_program.∀pol: policy program.
276  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
277  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
278  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
279  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
280     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
281   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
282 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
283 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
284 #H1 #_ @H1
285qed.
286
287(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
288definition construct_costs':
289 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
290  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
291
292  λprogram.λpol: policy program.λppc,pc,costs,i.
293   match construct_costs_safe program pol ppc pc costs i with
294    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
295    | Some res ⇒ res ].
296 [ cases daemon
297 | >p %]
298qed.
299
300definition construct_costs ≝
301 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i).
302
303(*
304axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
305axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
306
307axiom foldl_strong_step:
308 ∀A:Type[0].
309  ∀P: list A → Type[0].
310   ∀l: list A.
311    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
312     ∀acc: P [ ].
313      ∀Q: ∀prefix. P prefix → Prop.
314       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
315        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
316       Q [ ] acc →
317        Q l (foldl_strong A P l H acc).
318(*
319 #A #P #l #H #acc #Q #HQ #Hacc normalize;
320 generalize in match
321  (foldl_strong ?
322   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
323   l ? Hacc)
324 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
325 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
326 #K
327
328 generalize in match
329  (foldl_strong ?
330   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
331 [2: @H
332*)
333
334axiom foldl_elim:
335 ∀A:Type[0].
336  ∀B: Type[0].
337   ∀H: A → B → A.
338    ∀acc: A.
339     ∀l: list B.
340      ∀Q: A → Prop.
341       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
342         Q acc →
343          Q (foldl A B H acc l).
344*)
345
346lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
347 #A #a #b #EQ destruct //
348qed.
349
350(*
351lemma tech_pc_sigma00_append_Some:
352 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
353  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
354   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
355 #program #pol #prefix #costs #label #i #ppc #pc #H
356  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
357  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
358  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
359  whd in match sigma0; normalize nodelta;
360  >foldl_step
361  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
362  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
363  cases (sigma00 program pol prefix) in H ⊢ %
364   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
365   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
366     
367     normalize nodelta; -H;
368     
369 
370   generalize in match H; -H;
371  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
372   [2: whd in ⊢ (??%%)
373XXX
374*)
375
376axiom construct_costs_sigma:
377 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
378  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
379   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
380
381axiom tech_pc_sigma00_append_Some:
382 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
383  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
384   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
385
386axiom eq_identifier_eq:
387  ∀tag: String.
388  ∀l.
389  ∀r.
390    eq_identifier tag l r = true → l = r.
391
392axiom neq_identifier_neq:
393  ∀tag: String.
394  ∀l, r: identifier tag.
395    eq_identifier tag l r = false → (l = r → False).
396
397definition build_maps:
398 ∀pseudo_program.∀pol:policy pseudo_program.
399  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
400   let 〈labels, costs〉 ≝ res in
401    ∀id. occurs_exactly_once id (\snd pseudo_program) →
402     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
403  λpseudo_program.
404  λpol:policy pseudo_program.
405    let result ≝
406      foldl_strong
407        (option Identifier × pseudo_instruction)
408          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
409            let 〈labels,ppc_pc_costs〉 ≝ res in
410            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
411            let 〈pc',costs〉 ≝ pc_costs in
412              And ( And (
413              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
414                (ppc' = length … pre)) (*∧ *)
415                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
416                (∀id. occurs_exactly_once id pre →
417                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
418                (\snd pseudo_program)
419        (λprefix,i,tl,prf,t.
420          let 〈labels, ppc_pc_costs〉 ≝ t in
421          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
422          let 〈pc,costs〉 ≝ pc_costs in
423          let 〈label, i'〉 ≝ i in
424          let labels ≝
425            match label with
426            [ None ⇒ labels
427            | Some label ⇒
428                let program_counter_bv ≝ bitvector_of_nat ? pc in
429                  add ? ? labels label program_counter_bv
430            ]
431          in
432            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
433              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
434    in
435      let 〈labels, ppc_pc_costs〉 ≝ result in
436      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
437      let 〈pc, costs〉 ≝ pc_costs in
438        〈labels, costs〉.
439 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
440   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
441   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
442   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
443   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
444   | #id normalize nodelta; -labels1; cases label; normalize nodelta
445     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
446     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
447       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
448        [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
449          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
450        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
451          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
452          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
453          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
454 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
455 | generalize in match (pi2 … result) in ⊢ ?;
456   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
457   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
458qed.
459
460definition assembly:
461 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
462  λp.let 〈preamble, instr_list〉 ≝ p in
463   λpol.
464    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
465    let datalabels ≝ construct_datalabels preamble in
466    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
467    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
468    let result ≝
469     foldl_strong
470      (option Identifier × pseudo_instruction)
471      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
472        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
473        let 〈ppc,code〉 ≝ ppc_code in
474         ∀ppc'.
475          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
476          let 〈len,assembledi〉 ≝
477           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
478           True)
479      instr_list
480      (λprefix,hd,tl,prf,pc_ppc_code.
481        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
482        let 〈ppc, code〉 ≝ ppc_code in
483        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
484        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
485        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
486         〈new_pc, 〈new_ppc, (code @ program)〉〉)
487      〈(zero ?), 〈(zero ?), [ ]〉〉
488    in
489     〈\snd (\snd result), costs〉.
490 [2,5: %
491 |*: cases daemon ]
492qed.
493
494definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
495 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.