source: src/ASM/ASMCosts.ma @ 1691

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

Some progress in the proof: less daemons, less hypotheses in lemmas.

File size: 75.9 KB
RevLine 
[1486]1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
[1560]5include "common/StructuredTraces.ma".
[1486]6
[1642]7let rec fetch_program_counter_n
8  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
9    on n: option Word ≝
10  match n with
11  [ O ⇒ Some … program_counter
12  | S n ⇒
13    match fetch_program_counter_n n code_memory program_counter with
14    [ None ⇒ None …
15    | Some tail_pc ⇒
16      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
17        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
18          Some … program_counter
19        else
20          None Word (* XXX: overflow! *)
21    ]
22  ].
[1621]23   
[1642]24definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
[1621]25  λcode_memory: BitVectorTrie Byte 16.
[1639]26  λprogram_size: nat.
[1621]27  λprogram_counter: Word.
[1642]28    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
29        nat_of_bitvector 16 program_counter < program_size.
[1639]30   
[1642]31definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
[1621]32  λcode_memory: BitVectorTrie Byte 16.
33  λtotal_program_size: nat.
[1642]34  ∀program_counter: Word.
35  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
36  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
[1621]37    match instruction with
38    [ RealInstruction instr ⇒
39      match instr with
40      [ RET                    ⇒ True
41      | JC   relative          ⇒ True (* XXX: see below *)
42      | JNC  relative          ⇒ True (* XXX: see below *)
43      | JB   bit_addr relative ⇒ True
44      | JNB  bit_addr relative ⇒ True
45      | JBC  bit_addr relative ⇒ True
46      | JZ   relative          ⇒ True
47      | JNZ  relative          ⇒ True
48      | CJNE src_trgt relative ⇒ True
49      | DJNZ src_trgt relative ⇒ True
50      | _                      ⇒
[1642]51        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
52          nat_of_bitvector … program_counter' < total_program_size
[1621]53      ]
54    | LCALL addr         ⇒
55      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
56      [ ADDR16 addr ⇒ λaddr16: True.
[1642]57          reachable_program_counter code_memory total_program_size addr ∧
58            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
59              nat_of_bitvector … program_counter' < total_program_size
[1621]60      | _ ⇒ λother: False. ⊥
61      ] (subaddressing_modein … addr)
62    | ACALL addr         ⇒
63      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
64      [ ADDR11 addr ⇒ λaddr11: True.
[1642]65        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
[1621]66        let 〈thr, eig〉 ≝ split … 3 8 addr in
67        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
68        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
[1642]69          reachable_program_counter code_memory total_program_size new_program_counter ∧
70            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
71              nat_of_bitvector … program_counter' < total_program_size
[1621]72      | _ ⇒ λother: False. ⊥
73      ] (subaddressing_modein … addr)
74    | AJMP  addr         ⇒
75      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
76      [ ADDR11 addr ⇒ λaddr11: True.
[1642]77        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
[1621]78        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
79        let bit ≝ get_index' … O ? nl in
80        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
81        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
82        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
[1642]83          reachable_program_counter code_memory total_program_size new_program_counter
[1621]84      | _ ⇒ λother: False. ⊥
85      ] (subaddressing_modein … addr)
86    | LJMP  addr         ⇒
87      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
88      [ ADDR16 addr ⇒ λaddr16: True.
[1642]89          reachable_program_counter code_memory total_program_size addr
[1621]90      | _ ⇒ λother: False. ⊥
91      ] (subaddressing_modein … addr)
92    | SJMP  addr     ⇒
93      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
94      [ RELATIVE addr ⇒ λrelative: True.
[1642]95        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
96          reachable_program_counter code_memory total_program_size new_program_counter
[1621]97      | _ ⇒ λother: False. ⊥
98      ] (subaddressing_modein … addr)
[1645]99    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
100      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
101        nat_of_bitvector … program_counter' < total_program_size
[1621]102    | MOVC  src trgt ⇒
[1642]103        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
104          nat_of_bitvector … program_counter' < total_program_size
[1621]105    ].
106  cases other
107qed.
[1648]108       
109lemma is_a_decidable:
110  ∀hd.
111  ∀element.
112    is_a hd element = true ∨ is_a hd element = false.
113  #hd #element //
114qed.
115
116lemma mem_decidable:
117  ∀n: nat.
118  ∀v: Vector addressing_mode_tag n.
119  ∀element: addressing_mode_tag.
120    mem … eq_a n v element = true ∨
121      mem … eq_a … v element = false.
122  #n #v #element //
123qed.
124
[1650]125lemma eq_a_elim:
126  ∀tag.
127  ∀hd.
128  ∀P: bool → Prop.
129    (tag = hd → P (true)) →
130      (tag ≠ hd → P (false)) →
131        P (eq_a tag hd).
132  #tag #hd #P
133  cases tag
134  cases hd
135  #true_hyp #false_hyp
136  try @false_hyp
137  try @true_hyp
138  try %
139  #absurd destruct(absurd)
140qed.
141 
142lemma is_a_true_to_is_in:
[1648]143  ∀n: nat.
[1650]144  ∀x: addressing_mode.
145  ∀tag: addressing_mode_tag.
146  ∀supervector: Vector addressing_mode_tag n.
147  mem addressing_mode_tag eq_a n supervector tag →
148    is_a tag x = true →
149      is_in … supervector x.
150  #n #x #tag #supervector
151  elim supervector
152  [1:
153    #absurd cases absurd
154  |2:
155    #n' #hd #tl #inductive_hypothesis
156    whd in match (mem … eq_a (S n') (hd:::tl) tag);
157    @eq_a_elim normalize nodelta
158    [1:
159      #tag_hd_eq #irrelevant
160      whd in match (is_in (S n') (hd:::tl) x);
161      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
162      @I
163    |2:
164      #tag_hd_neq
165      whd in match (is_in (S n') (hd:::tl) x);
166      change with (
167        mem … eq_a n' tl tag)
168          in match (fold_right … n' ? false tl);
169      #mem_hyp #is_a_hyp
170      cases(is_a hd x)
171      [1:
172        normalize nodelta //
173      |2:
174        normalize nodelta
175        @inductive_hypothesis assumption
176      ]
177    ]
178  ]
179qed.
[1648]180
181lemma is_in_subvector_is_in_supervector:
[1625]182  ∀m, n: nat.
183  ∀subvector: Vector addressing_mode_tag m.
[1648]184  ∀supervector: Vector addressing_mode_tag n.
[1646]185  ∀element: addressing_mode.
[1625]186    subvector_with … eq_a subvector supervector →
187      is_in m subvector element → is_in n supervector element.
[1648]188  #m #n #subvector #supervector #element
189  elim subvector
190  [1:
191    #subvector_with_proof #is_in_proof
192    cases is_in_proof
193  |2:
[1650]194    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
195    whd in match (is_in … (hd':::tl') element);
196    cases (is_a_decidable hd' element)
[1648]197    [1:
[1650]198      #is_a_true >is_a_true
[1648]199      #irrelevant
[1650]200      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
201      @(is_a_true_to_is_in … is_a_true)
202      lapply(subvector_with_proof)
203      cases(mem … eq_a n supervector hd') //
[1648]204    |2:
205      #is_a_false >is_a_false normalize nodelta
206      #assm
207      @inductive_hypothesis
208      [1:
[1650]209        generalize in match subvector_with_proof;
210        whd in match (subvector_with … eq_a (hd':::tl') supervector);
211        cases(mem_decidable n supervector hd')
[1648]212        [1:
213          #mem_true >mem_true normalize nodelta
214          #assm assumption
215        |2:
216          #mem_false >mem_false #absurd
217          cases absurd
218        ]
219      |2:
220        assumption
221      ]
222    ]
[1650]223  ]
[1648]224qed.
[1625]225
[1622]226let rec member_addressing_mode_tag
227  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
228    on v: Prop ≝
229  match v with
230  [ VEmpty ⇒ False
231  | VCons n' hd tl ⇒
[1623]232      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
[1622]233  ].
234 
235let rec subaddressing_mode_elim_type
[1625]236  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
[1622]237    (Q: addressing_mode → T → Prop)
[1625]238      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
239      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
240      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
241      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
242      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
243      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
244      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
245      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
246      (p_dptr:                               is_in m fixed_v DPTR              → T)
247      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
248      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
249      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
250      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
251      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
252      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
253      (p_carry:                              is_in m fixed_v CARRY             → T)
254      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
255      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
256      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
257        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
258      on v: Prop ≝
259  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
[1623]260  [ VEmpty         ⇒ λm_refl. λv_refl.
[1625]261      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
[1623]262        Q addr (
[1625]263        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
[1624]264        [ ADDR11 x          ⇒ p_addr11 x
265        | ADDR16 x          ⇒ p_addr16 x
266        | DIRECT x          ⇒ p_direct x
267        | INDIRECT x        ⇒ p_indirect x
268        | EXT_INDIRECT x    ⇒ p_ext_indirect x
269        | ACC_A             ⇒ p_acc_a
270        | REGISTER x        ⇒ p_register x
271        | ACC_B             ⇒ p_acc_b
272        | DPTR              ⇒ p_dptr
273        | DATA x            ⇒ p_data x
274        | DATA16 x          ⇒ p_data16 x
275        | ACC_DPTR          ⇒ p_acc_dptr
276        | ACC_PC            ⇒ p_acc_pc
[1623]277        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
[1624]278        | INDIRECT_DPTR     ⇒ p_indirect_dptr
279        | CARRY             ⇒ p_carry
280        | BIT_ADDR x        ⇒ p_bit_addr x
281        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
282        | RELATIVE x        ⇒ p_relative x
[1623]283        ] p)
284  | VCons n' hd tl ⇒ λm_refl. λv_refl.
[1625]285    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
286      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
287        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
288          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
289            p_bit_addr p_n_bit_addr p_relative n' tl ?
[1623]290    in
291    match hd return λa: addressing_mode_tag. a = hd → ? with
[1624]292    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
293    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
294    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
295    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
296    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
297    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
298    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
299    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
300    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
301    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
302    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
303    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
304    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
[1623]305    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
[1624]306    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
307    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
308    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
309    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
310    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
[1622]311    ] (refl … hd)
[1624]312  ] (refl … n) (refl_jmeq … v).
313  [20:
[1625]314    generalize in match proof; destruct
315    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
316    cases (mem … eq_a m fixed_v hd) normalize nodelta
317    [1:
318      whd in match (subvector_with … eq_a tl fixed_v);
319      #assm assumption
320    |2:
321      normalize in ⊢ (% → ?);
322      #absurd cases absurd
323    ]
324  ]
[1646]325  @(is_in_subvector_is_in_supervector … proof)
[1625]326  destruct @I
[1623]327qed.
[1621]328
[1645]329lemma subaddressing_mode_elim':
[1624]330  ∀T: Type[2].
[1645]331  ∀n: nat.
332  ∀o: nat.
333  ∀Q: addressing_mode → T → Prop.
334  ∀fixed_v: Vector addressing_mode_tag (n + o).
335  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
336  ∀v1: Vector addressing_mode_tag n.
337  ∀v2: Vector addressing_mode_tag o.
338  ∀fixed_v_proof: fixed_v = v1 @@ v2.
339  ∀subaddressing_mode_proof.
340    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
341      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
342  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
343  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
344  cases daemon
345qed.
346
347axiom subaddressing_mode_elim:
348  ∀T: Type[2].
[1625]349  ∀m: nat.
[1645]350  ∀n: nat.
351  ∀Q: addressing_mode → T → Prop.
[1625]352  ∀fixed_v: Vector addressing_mode_tag m.
353  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
[1624]354  ∀v: Vector addressing_mode_tag n.
[1625]355  ∀proof.
356    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
[1624]358
[1658]359definition current_instruction0 ≝
360  λcode_memory: BitVectorTrie Byte 16.
361  λprogram_counter: Word.
362    \fst (\fst (fetch … code_memory program_counter)).
363
364definition current_instruction ≝
[1669]365  λcode_memory.
366  λs: Status code_memory.
367    current_instruction0 code_memory (program_counter … s).
[1658]368
369definition ASM_classify0: instruction → status_class ≝
370  λi: instruction.
371  match i with
372   [ RealInstruction pre ⇒
373     match pre with
374      [ RET ⇒ cl_return
375      | JZ _ ⇒ cl_jump
376      | JNZ _ ⇒ cl_jump
377      | JC _ ⇒ cl_jump
378      | JNC _ ⇒ cl_jump
379      | JB _ _ ⇒ cl_jump
380      | JNB _ _ ⇒ cl_jump
381      | JBC _ _ ⇒ cl_jump
382      | CJNE _ _ ⇒ cl_jump
383      | DJNZ _ _ ⇒ cl_jump
384      | _ ⇒ cl_other
385      ]
386   | ACALL _ ⇒ cl_call
387   | LCALL _ ⇒ cl_call
388   | JMP _ ⇒ cl_call
389   | AJMP _ ⇒ cl_jump
390   | LJMP _ ⇒ cl_jump
391   | SJMP _ ⇒ cl_jump
392   | _ ⇒ cl_other
393   ].
394
[1669]395definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
396  λcode_memory.
397  λs: Status code_memory.
398    ASM_classify0 (current_instruction … s).
[1658]399
400definition current_instruction_is_labelled ≝
[1669]401  λcode_memory.
[1658]402  λcost_labels: BitVectorTrie costlabel 16.
[1669]403  λs: Status code_memory.
404  let pc ≝ program_counter … code_memory s in
[1658]405    match lookup_opt … pc cost_labels with
406    [ None ⇒ False
407    | _    ⇒ True
408    ].
409
410definition next_instruction_properly_relates_program_counters ≝
[1669]411  λcode_memory.
412  λbefore: Status code_memory.
413  λafter : Status code_memory.
414  let size ≝ current_instruction_cost code_memory before in
415  let pc_before ≝ program_counter … code_memory before in
416  let pc_after ≝ program_counter … code_memory after in
[1658]417  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
418    sum = pc_after.
419
[1669]420definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
421  λcode_memory.
422  λcost_labels.
423    mk_abstract_status
424      (Status code_memory)
425      (λs,s'. (execute_1 … s) = s')
426      (λs,class. ASM_classify … s = class)
427      (current_instruction_is_labelled … cost_labels)
428      (next_instruction_properly_relates_program_counters code_memory).
[1658]429
430let rec trace_any_label_length
[1669]431  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
432    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
433      (final_status: Status code_memory)
434      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
[1658]435        on the_trace: nat ≝
436  match the_trace with
437  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
438  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
439  | tal_base_return the_status _ _ _ ⇒ 0
440  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
441      let tail_length ≝ trace_any_label_length … final_trace in
442      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
443        pc_difference + tail_length
444  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
445      let tail_length ≝ trace_any_label_length … tail_trace in
446      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
447        pc_difference + tail_length       
448  ].
449
450let rec compute_paid_trace_any_label
[1669]451  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
452    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
453      (final_status: Status code_memory)
454        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
[1658]455       on the_trace: nat ≝
456  match the_trace with
[1669]457  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
458  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
459  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
[1658]460  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
461     _ _ _ call_trace _ final_trace ⇒
[1669]462      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
463      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
[1658]464        current_instruction_cost + final_trace_cost
465  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
[1669]466      let current_instruction_cost ≝ current_instruction_cost … status_pre in
[1658]467      let tail_trace_cost ≝
[1669]468       compute_paid_trace_any_label … cost_labels end_flag
[1658]469        status_init status_end tail_trace
470      in
471        current_instruction_cost + tail_trace_cost
472  ].
473
474definition compute_paid_trace_label_label ≝
[1669]475  λcode_memory: BitVectorTrie Byte 16.
476  λcost_labels: BitVectorTrie costlabel 16.
[1658]477  λtrace_ends_flag: trace_ends_with_ret.
[1669]478  λstart_status: Status code_memory.
479  λfinal_status: Status code_memory.
480  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
[1658]481  match the_trace with
482  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
483      compute_paid_trace_any_label … given_trace
484  ].
485
[1622]486include alias "arithmetics/nat.ma".
[1658]487include alias "basics/logic.ma".
[1622]488
[1663]489lemma plus_right_monotone:
490  ∀m, n, o: nat.
491    m = n → m + o = n + o.
492  #m #n #o #refl >refl %
493qed.
[1658]494
[1665]495(* XXX: indexing bug re-emerges! *)
496example fetch_half_add:
[1669]497  ∀code_memory: BitVectorTrie Byte 16.
[1665]498  ∀cost_labels: BitVectorTrie costlabel 16.
[1669]499  ∀the_status : ASM_abstract_status code_memory cost_labels.
500    \snd (\fst (fetch code_memory (program_counter … the_status))) =
501      \snd (half_add 16 (program_counter … the_status)
502        (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))).
[1665]503  cases daemon
504qed.
505
506axiom half_add_minus_right:
507  ∀size : nat.
508  ∀left : BitVector size.
509  ∀right: nat.
510  nat_of_bitvector … (\snd (half_add … left (bitvector_of_nat … right))) -
511    nat_of_bitvector … left = right.
512
513lemma minus_plus_cancel:
514  ∀m, n : nat.
515  ∀proof: n ≤ m.
516    (m - n) + n = m.
517  #m #n #proof /2 by plus_minus/
518qed.
519
[1669]520(* XXX: indexing bug *)
521example fetch_twice_fetch_execute_1:
522  ∀code_memory: BitVectorTrie Byte 16.
523  ∀start_status: Status code_memory.
524    \snd (\fst (fetch code_memory (program_counter … start_status))) =
525      program_counter … (execute_1 … start_status).
526  cases daemon
527qed. (*
528  #code_memory #start_status
529  whd in match (execute_1 code_memory start_status);
530  whd in match (execute_1' code_memory start_status); normalize nodelta
531  cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks
532  cases instruction_pc #instruction #pc normalize nodelta *)
533
[1684]534lemma reachable_program_counter_to_0_lt_total_program_size:
535  ∀code_memory: BitVectorTrie Byte 16.
536  ∀program_counter: Word.
537  ∀total_program_size: nat.
538    reachable_program_counter code_memory total_program_size program_counter →
539      0 < total_program_size.
540  #code_memory #program_counter #total_program_size
541  whd in match reachable_program_counter; normalize nodelta * * #some_n
542  #_ cases (nat_of_bitvector 16 program_counter)
543  [1:
544    #assm assumption
545  |2:
546    #new_pc @ltn_to_ltO
547  ]
548qed.
549
550lemma trace_compute_paid_trace_cl_other:
[1669]551  ∀code_memory' : (BitVectorTrie Byte 16).
552  ∀program_counter' : Word.
553  ∀total_program_size : ℕ.
554  ∀cost_labels : (BitVectorTrie costlabel 16).
555  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
556  ∀good_program_witness : (good_program code_memory' total_program_size).
557  ∀program_size' : ℕ.
558  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
559  ∀ticks : ℕ.
560  ∀instruction : instruction.
561  ∀program_counter'' : Word.
562  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
563  ∀start_status : (Status code_memory').
564  ∀final_status : (Status code_memory').
565  ∀trace_ends_flag : trace_ends_with_ret.
566  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
567  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
568  ∀classify_assm: ASM_classify0 instruction = cl_other.
569  ∀pi1 : ℕ.
570   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
571         [None ⇒ true
572         |Some _ ⇒ false
573         ] 
574    then
575      ∀start_status0:Status code_memory'.
576      ∀final_status0:Status code_memory'.
577      ∀trace_ends_flag0:trace_ends_with_ret.
578      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
579        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
580        (∃n:ℕ
581                    .trace_any_label_length code_memory' cost_labels
582                     trace_ends_flag0 start_status0 final_status0 the_trace0
583                     +S n
584                     =total_program_size)
585                   ∧pi1
586                    =compute_paid_trace_any_label code_memory' cost_labels
587                     trace_ends_flag0 start_status0 final_status0 the_trace0
588    else (pi1=O) )
589   →(∃n:ℕ
590     .trace_any_label_length code_memory' cost_labels trace_ends_flag
591      start_status final_status the_trace
592      +S n
593      =total_program_size)
594    ∧ticks+pi1
595     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
596      start_status final_status the_trace.
597  #code_memory' #program_counter' #total_program_size #cost_labels
598  #reachable_program_counter_witness #good_program_witness
599  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
[1691]600  #start_status #final_status
[1669]601  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
602  #recursive_assm @(trace_any_label_inv_ind … the_trace)
603    [5:
604      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
605      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
606      #the_trace_refl
607      destruct
608      whd in match (trace_any_label_length … (tal_step_default …));
609      whd in match (compute_paid_trace_any_label … (tal_step_default …));
610      whd in costed_assm:(?%);
611      generalize in match costed_assm;
612      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
613      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
614        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
615      #lookup_assm cases lookup_assm
616      [1:
617        #None_lookup_opt_assm normalize nodelta #ignore
618        generalize in match recursive_assm;
619        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
620        [1:
621          <fetch_twice_fetch_execute_1 <FETCH %
622        |2:
623          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
624          normalize nodelta #new_recursive_assm
625          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
626            end_flag trace_any_label ?) [2: % ]
627          #exists_assm #recursive_block_cost_assm %
628          [1:
629            cases exists_assm #exists_n #total_program_size_refl
630            <total_program_size_refl
631            %{(exists_n - current_instruction_cost … status_pre)}
[1684]632            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
633            cases daemon
[1669]634          |2:
635            >recursive_block_cost_assm
636            whd in match (current_instruction_cost … status_pre);
637            cut(ticks = \snd (fetch code_memory'
638               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
639            [1:
640              <FETCH %
641            |2:
642              #ticks_refl_assm >ticks_refl_assm %
643            ]
644          ]
645        ]
646      |2:
647        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
648        #absurd cases absurd #absurd cases(absurd I)
649      ]
650    |1:
651      #status_start #status_final #execute_assm #classifier_assm #costed_assm
652      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
653      destruct
654      whd in match (trace_any_label_length … (tal_base_not_return …));
655      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
656      whd in costed_assm;
657      generalize in match costed_assm;
658      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
659      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
660        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
661      #lookup_assm cases lookup_assm
662      [1:
663        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
664        #absurd cases absurd
665      |2:
666        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
667        generalize in match recursive_assm;
668        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
669        [1:
670          <fetch_twice_fetch_execute_1 <FETCH %
671        |2:
672          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
673          normalize nodelta #new_recursive_assm >new_recursive_assm %
674          [1:
675            %{(pred total_program_size)} whd in ⊢ (??%?);
676            @S_pred
[1684]677            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
[1669]678          |2:
679            cut(ticks = \snd (fetch code_memory'
680               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
681            [1:
682              <FETCH %
683            |2:
684              #ticks_refl_assm >ticks_refl_assm
685              <plus_n_O %
686            ]
687          ]
688        ]
689      ]
690    |2:
691      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
692      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
693    |3:
694      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
695      #classifier_assm #after_return_assm #trace_label_return #costed_assm
696      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
697      destruct @⊥
[1684]698    |4:
699      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
700      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
701      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
702      #final_status_refl #the_trace_refl destruct @⊥
[1669]703    ]
[1684]704  change with (ASM_classify0 ? = ?) in classifier_assm;
705  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
706  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
707  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
[1669]708qed.
709
[1684]710lemma trace_compute_paid_trace_cl_jump:
711  ∀code_memory': BitVectorTrie Byte 16.
712  ∀program_counter': Word.
713  ∀total_program_size: ℕ.
714  ∀cost_labels: BitVectorTrie costlabel 16.
715  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
716  ∀good_program_witness: good_program code_memory' total_program_size.
717  ∀first_time_around: bool.
718  ∀program_size': ℕ.
719  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
720  ∀ticks: ℕ.
721  ∀instruction: instruction.
722  ∀program_counter'': Word.
723  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
724  ∀start_status: (Status code_memory').
725  ∀final_status: (Status code_memory').
726  ∀trace_ends_flag: trace_ends_with_ret.
727  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
728  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
729  ∀classify_assm: ASM_classify0 instruction = cl_jump.
[1691]730   (∃n:ℕ
[1684]731     .trace_any_label_length code_memory' cost_labels trace_ends_flag
732      start_status final_status the_trace
733      +S n
734      =total_program_size)
735    ∧ticks
736     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
[1691]737      start_status final_status the_trace.
[1684]738  #code_memory' #program_counter' #total_program_size #cost_labels
739  #reachable_program_counter_witness #good_program_witness #first_time_around
740  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
[1691]741  #start_status #final_status
[1684]742  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
743  @(trace_any_label_inv_ind … the_trace)
744  [1:
745    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
746    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
747    destruct
748    whd in match (trace_any_label_length … (tal_base_not_return …));
749    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
750    whd in costed_assm;
751    generalize in match costed_assm;
752    generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … start_status')) cost_labels));
753    generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' start_status')) cost_labels)
754      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
755    #lookup_assm cases lookup_assm
756    [1:
757      #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
758      #absurd cases absurd
759    |2:
[1691]760      #costlabel #Some_lookup_opt_assm normalize nodelta #ignore %
761      [2: <FETCH %
762      | cases daemon ]
[1684]763    ]
764  |2:
765    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
766    #start_status_refl #final_status_refl #the_trace_refl destruct @⊥
767  |3:
768    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
769    #classifier_assm #after_return_assm #trace_label_return #costed_assm
770    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
771    destruct @⊥
772  |4:
773    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
774    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
775    #costed_assm #trace_any_label_return #trace_ends_flag_refl #start_status_refl
776    #final_status_refl #the_trace_refl destruct @⊥
777  |5:
778    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
779    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
780    #final_status_refl #the_trace_refl destruct @⊥
781  ]
782  change with (ASM_classify0 ? = ?) in classifier_assm;
783  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
784  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
785  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
786qed.
787
788lemma trace_compute_paid_trace_cl_call:
789  ∀code_memory' : (BitVectorTrie Byte 16).
790  ∀program_counter' : Word.
791  ∀total_program_size : ℕ.
792  ∀cost_labels : (BitVectorTrie costlabel 16).
793  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
794  ∀good_program_witness : (good_program code_memory' total_program_size).
795  ∀program_size' : ℕ.
796  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
797  ∀ticks : ℕ.
798  ∀instruction : instruction.
799  ∀program_counter'' : Word.
800  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
801  ∀start_status : (Status code_memory').
802  ∀final_status : (Status code_memory').
803  ∀trace_ends_flag : trace_ends_with_ret.
804  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
805  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
806  ∀classify_assm: ASM_classify0 instruction = cl_call.
807  ∀pi1 : ℕ.
808  if match lookup_opt costlabel 16 program_counter'' cost_labels with 
809        [None ⇒ true|Some _ ⇒ false] 
810   then (∀start_status0:Status code_memory'
811             .∀final_status0:Status code_memory'
812              .∀trace_ends_flag0:trace_ends_with_ret
813               .∀the_trace0:trace_any_label
814                                        (ASM_abstract_status code_memory' cost_labels)
815                                        trace_ends_flag0 start_status0 final_status0
816                .program_counter''
817                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
818                 →(∃n:ℕ
819                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
820                    start_status0 final_status0 the_trace0
821                    +S n
822                    =total_program_size)
823                  ∧pi1
824                   =compute_paid_trace_any_label code_memory' cost_labels
825                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
826   else (pi1=O) 
827   →(∃n:ℕ
828     .trace_any_label_length code_memory' cost_labels trace_ends_flag
829      start_status final_status the_trace
830      +S n
831      =total_program_size)
832    ∧ticks+pi1
833     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
834      start_status final_status the_trace.
835  #code_memory' #program_counter' #total_program_size #cost_labels
836  #reachable_program_counter_witness #good_program_witness #program_size'
[1691]837  #recursive_case #ticks #instruction #program_counter'' #FETCH
838  #start_status #final_status #trace_ends_flag
[1684]839  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
840  @(trace_any_label_inv_ind … the_trace)
841  cases daemon
842qed.
843
[1650]844let rec block_cost'
[1658]845  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
[1621]846    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
[1658]847      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
848        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
849          on program_size:
850          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
851          Σcost_of_block: nat.
[1669]852          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
853            ∀start_status: Status code_memory'.
854            ∀final_status: Status code_memory'.
[1658]855            ∀trace_ends_flag.
[1669]856            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
857              program_counter' = program_counter … start_status →
858                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
859                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
860          else
861            (cost_of_block = 0) ≝
[1658]862  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
[1642]863  [ O ⇒ λbase_case. ⊥
[1621]864  | S program_size' ⇒ λrecursive_case.
[1663]865    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
[1650]866    let to_continue ≝
[1669]867      match lookup_opt … program_counter' cost_labels with
[1650]868      [ None ⇒ true
869      | Some _ ⇒ first_time_around
870      ]
871    in
[1669]872      ((if to_continue then
873       pi1 … (match instruction return λx. x = instruction → ? with
[1663]874        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
875          match real_instruction return λx. x = real_instruction →
876          Σcost_of_block: nat.
[1669]877            ∀start_status: Status code_memory'.
878            ∀final_status: Status code_memory'.
[1663]879            ∀trace_ends_flag.
[1669]880            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
881              program_counter' = program_counter … start_status →
882                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
883                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
[1663]884          [ RET                    ⇒ λinstr. ticks
885          | JC   relative          ⇒ λinstr. ticks
886          | JNC  relative          ⇒ λinstr. ticks
887          | JB   bit_addr relative ⇒ λinstr. ticks
888          | JNB  bit_addr relative ⇒ λinstr. ticks
889          | JBC  bit_addr relative ⇒ λinstr. ticks
890          | JZ   relative          ⇒ λinstr. ticks
891          | JNZ  relative          ⇒ λinstr. ticks
892          | CJNE src_trgt relative ⇒ λinstr. ticks
893          | DJNZ src_trgt relative ⇒ λinstr. ticks
894          | _                      ⇒ λinstr.
[1669]895         
[1658]896              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]897          ] (refl …)
898        | ACALL addr     ⇒ λinstr.
[1658]899            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]900        | AJMP  addr     ⇒ λinstr. ticks
901        | LCALL addr     ⇒ λinstr.
[1658]902            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]903        | LJMP  addr     ⇒ λinstr. ticks
904        | SJMP  addr     ⇒ λinstr. ticks
905        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
[1658]906            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]907        | MOVC  src trgt ⇒ λinstr.
[1658]908            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1669]909        ] (refl …))
[1650]910      else
[1669]911        0)
912      : Σcost_of_block: nat.
913          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
914          [ true ⇒
915            ∀start_status: Status code_memory'.
916            ∀final_status: Status code_memory'.
917            ∀trace_ends_flag.
918            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
919              program_counter' = program_counter … start_status →
920                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
921                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
922          | false ⇒
923            (cost_of_block = 0)
924          ])
[1621]925  ].
[1642]926  [1:
927    cases reachable_program_counter_witness #_ #hyp
928    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
929    @(le_to_lt_to_lt … base_case hyp)
[1669]930  |2:
[1684]931    change with (if to_continue then ? else (? = 0))
932    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
933    @pi2
[1669]934  |3:
[1684]935    change with (if to_continue then ? else (0 = 0))
936    >p normalize nodelta %
937  |98,104,107:
[1669]938    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
[1663]939    cases(block_cost' ?????????) -block_cost'
[1691]940    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
941    destruct %
[1684]942  |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
[1691]943   92,95:
[1684]944    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
945    cases(block_cost' ?????????) -block_cost'
[1691]946    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
[1669]947    destruct %
[1684]948  |62,63,64,65,66,67,68,69,101,102,103:
[1691]949    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
950    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
951    destruct %
[1684]952  |96,99:
953    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
954    lapply(good_program_witness program_counter' reachable_program_counter_witness)
955    <FETCH normalize nodelta <instr normalize nodelta *
956    #program_counter_lt' #program_counter_lt_tps' %
957    [1,3:
958      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
959      <FETCH normalize nodelta whd in match ltb; normalize nodelta
960      >(le_to_leb_true … program_counter_lt') %
961    |2,4:
962      assumption
963    ]
964  |105:
965    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
966    lapply(good_program_witness program_counter' reachable_program_counter_witness)
967    <FETCH normalize nodelta <instr normalize nodelta
968    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
969    * * * * #n'
970    #_ #_ #program_counter_lt' #program_counter_lt_tps'
971    %
[1663]972    [1:
[1684]973      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
974      <FETCH normalize nodelta whd in match ltb; normalize nodelta
975      >(le_to_leb_true … program_counter_lt') %
976    |2:
977      assumption
978    ]
979  |106:
980    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
981    lapply(good_program_witness program_counter' reachable_program_counter_witness)
982    <FETCH normalize nodelta <instr normalize nodelta
983    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
984    * * * * #n'
985    #_ #_ #program_counter_lt' #program_counter_lt_tps'
986    @(transitive_le
987      total_program_size
988      ((S program_size') + nat_of_bitvector … program_counter')
989      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
990    normalize in match (S program_size' + nat_of_bitvector … program_counter');
991    >plus_n_Sm
992    @monotonic_le_plus_r
993    change with (
994      nat_of_bitvector … program_counter' <
995        nat_of_bitvector … program_counter'')
996    assumption
997  |108:
998    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
999    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1000    <FETCH normalize nodelta <instr normalize nodelta
1001    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1002    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1003    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1004    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1005    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1006    %
1007    [1:
1008      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1009      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1010      >(le_to_leb_true … program_counter_lt') %
1011    |2:
1012      assumption
1013    ]
1014  |109:
1015    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1016    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1017    <FETCH normalize nodelta <instr normalize nodelta
1018    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1019    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1020    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1021    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1022    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1023    @(transitive_le
1024      total_program_size
1025      ((S program_size') + nat_of_bitvector … program_counter')
1026      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1027    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1028    >plus_n_Sm
1029    @monotonic_le_plus_r
1030    change with (
1031      nat_of_bitvector … program_counter' <
1032        nat_of_bitvector … program_counter'')
1033    assumption
1034  |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
1035   78,81,84,87,90,93:
1036    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1037    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1038    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1039    #program_counter_lt' #program_counter_lt_tps' %
1040    try assumption
1041    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1042    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1043    >(le_to_leb_true … program_counter_lt') %
1044  |97,100:
1045    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1046    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1047    <FETCH normalize nodelta <instr normalize nodelta
1048    try(<real_instruction_refl <instr normalize nodelta) *
1049    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1050    @(transitive_le
1051      total_program_size
1052      ((S program_size') + nat_of_bitvector … program_counter')
1053      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1054    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1055    >plus_n_Sm
1056    @monotonic_le_plus_r
1057    change with (
1058      nat_of_bitvector … program_counter' <
1059        nat_of_bitvector … program_counter'')
1060    assumption
1061  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
1062   94:
1063    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1064    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1065    <FETCH normalize nodelta
1066    <real_instruction_refl <instr normalize nodelta *
1067    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1068    @(transitive_le
1069      total_program_size
1070      ((S program_size') + nat_of_bitvector … program_counter')
1071      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1072    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1073    >plus_n_Sm
1074    @monotonic_le_plus_r
1075    change with (
1076      nat_of_bitvector … program_counter' <
1077        nat_of_bitvector … program_counter'')
1078    assumption
1079  |10:
1080    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1081    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1082      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1083    [1:
1084      @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness …
1085        recursive_case … instruction program_counter' … FETCH)
1086    |2:
1087    ]
1088  ]
1089qed.
1090 
1091 
1092 
1093 
1094    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1095    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1096    <FETCH normalize nodelta
1097    <real_instruction_refl <instr normalize nodelta *
1098    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1099    @(transitive_le
1100      total_program_size
1101      ((S program_size') + nat_of_bitvector … program_counter')
1102      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1103    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1104    >plus_n_Sm
1105    @monotonic_le_plus_r
1106    change with (
1107      nat_of_bitvector … program_counter' <
1108        nat_of_bitvector … program_counter'')
1109    assumption
1110  |4:
1111    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1112    cases(block_cost' ??? ? ?????) -block_cost'
1113    #recursive_block_cost #recursive_assm
1114    @(trace_any_label_inv_ind … the_trace)
1115    [1:
[1669]1116      #status_start #status_final #execute_assm #classifier_assm #costed_assm
1117      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1118      destruct
1119      whd in match (trace_any_label_length … (tal_base_not_return …));
1120      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
1121      whd in costed_assm;
[1663]1122    |2:
1123      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
1124      #start_status_refl #final_status_refl #the_trace_assm destruct
1125      whd in classifier_assm;
1126      whd in classifier_assm:(??%?);
1127      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1128      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1129      @⊥ <FETCH in classifier_assm; normalize nodelta
1130      #absurd destruct(absurd)
1131    |3:
1132      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1133      #classifier_assm #after_return_assm #trace_label_return #costed_assm
[1669]1134      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1135      destruct
1136      whd in classifier_assm;
1137      whd in classifier_assm:(??%?);
1138      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1139      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1140      @⊥ <FETCH in classifier_assm; normalize nodelta
1141      #absurd destruct(absurd)
1142    |4:
1143      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1144      #status_final #execute_assm #classifier_assm #after_return_assm
1145      #trace_label_return #costed_assm #trace_any_label #ends_flag_refl
1146      #start_status_refl #final_status_refl #the_trace_refl
1147      destruct
1148      whd in classifier_assm;
1149      whd in classifier_assm:(??%?);
1150      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1151      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1152      @⊥ <FETCH in classifier_assm; normalize nodelta
1153      #absurd destruct(absurd)
1154    ]
1155   
1156   
1157   
1158   
1159   
1160   
1161   
1162   
1163   
1164   
1165   
1166   
1167   
1168   
1169   
1170   
1171   
1172   
1173   
1174   
1175   
1176   
1177   
1178   
1179   
1180   
1181   
1182   
1183   
1184    |3:
1185      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1186      #classifier_assm #after_return_assm #trace_label_return #costed_assm
[1663]1187      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1188      destruct
[1665]1189      whd in match (compute_paid_trace_any_label … (tal_base_call …));
1190      whd in match (trace_any_label_length … (tal_base_call …));
[1669]1191      cases(recursive_assm …
1192        (tal_base_call (ASM_abstract_status code_memory' cost_labels)
1193         status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …)
1194         classifier_assm after_return_assm trace_label_return costed_assm) ?)
[1665]1195      [1:
[1669]1196        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
[1665]1197        [1:
1198          %{(pred total_program_size)}
1199          whd in ⊢ (??%?);
1200          >S_pred [1: % ]
1201          <recursive_trace_total
1202          @lt_O_S
1203        |2:
1204          >recursive_block_cost_assm
1205          whd in ⊢ (??(??%)?); <FETCH
1206          (* XXX: ??? *)
1207        ]
1208      |2:
[1669]1209        cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call))))
[1665]1210        [1:
1211          cases FETCH %
1212        |2:
1213          #program_counter_hyp'' >program_counter_hyp''
1214          whd in after_return_assm; <after_return_assm
1215          whd in match (current_instruction_cost status_pre_fun_call);
1216          @fetch_half_add
1217        ]
[1663]1218      ]
1219    |4:
1220      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1221      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1222      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
[1665]1223      #final_status_refl #the_trace_refl
1224      generalize in match execute_assm; destruct #execute_assm
[1663]1225      whd in match (compute_paid_trace_any_label … (tal_step_call …));
1226      whd in match (trace_any_label_length … (tal_step_call …));
1227      cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
1228      [1:
[1665]1229        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
[1663]1230        [1:
[1665]1231          <recursive_trace_total %
[1663]1232          [1:
[1665]1233            @(recursive_n - (current_instruction_cost status_pre_fun_call))
[1663]1234          |2:
[1665]1235            whd in after_return_assm; cases after_return_assm
1236            >half_add_minus_right in ⊢ (??%?);
1237            >commutative_plus in ⊢ (???%);
[1663]1238            >commutative_plus in ⊢ (??%?);
[1665]1239            <associative_plus in ⊢ (??%?);
1240            @plus_right_monotone
1241            cut(current_instruction_cost status_pre_fun_call ≤ recursive_n)
1242            [1:
1243              (* XXX: ??? *)
1244            |2:
1245              #current_instruction_cost_assm
1246              <minus_Sn_m in ⊢ (??%?); [2: assumption ]
1247              >minus_plus_cancel [1: % ]
1248              @le_S assumption
1249            ]
[1663]1250          ]
1251        |2:
[1665]1252          >recursive_block_cost_assm
[1663]1253          @plus_right_monotone
1254          whd in match (current_instruction_cost status_pre_fun_call);
1255          <FETCH %
1256        ]
[1669]1257     
[1663]1258      |2:
[1665]1259        lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
1260        #hyp cases (hyp trace_label_return)
1261        @as_execute_preserves_code_memory whd %
[1663]1262      |3:
[1665]1263        cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
1264        [1:
1265          cases FETCH %
1266        |2:
1267          #program_counter_hyp'' >program_counter_hyp''
1268          whd in after_return_assm; <after_return_assm
1269          whd in match (current_instruction_cost status_pre_fun_call);
1270          @fetch_half_add
1271        ]
[1663]1272      ]
1273    |5:
1274      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace'
1275      #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1276      #final_status_refl #trace_refl
1277      generalize in match the_trace; destruct #the_trace
1278      whd in classifier_assm;
1279      whd in classifier_assm:(??%?);
1280      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1281      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1282      @⊥ <FETCH in classifier_assm; normalize nodelta
1283      #absurd destruct(absurd)
1284    ]
1285  |7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61,
1286    64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107:
1287    cases daemon (* XXX: massive terms *)
[1642]1288  |2:
1289    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
[1658]1290    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1663]1291    <FETCH normalize nodelta <instr normalize nodelta
[1658]1292    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1293    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1294    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1295    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1296    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1297    @(transitive_le
1298      total_program_size
1299      ((S program_size') + nat_of_bitvector … program_counter')
1300      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1301    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1302    >plus_n_Sm
1303    @monotonic_le_plus_r
1304    change with (
1305      nat_of_bitvector … program_counter' <
1306        nat_of_bitvector … program_counter'')
1307    assumption
1308  |3:
1309    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1310    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1663]1311    <FETCH normalize nodelta <instr normalize nodelta
[1658]1312    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1313    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1314    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1315    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1316    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1317    %
1318    [1:
1319      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1320      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1321      >(le_to_leb_true … program_counter_lt') %
1322    |2:
1323      assumption
1324    ]
1325  |5:
1326    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1327    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1663]1328      <FETCH normalize nodelta <instr normalize nodelta
[1658]1329    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1330    * * * * #n'
1331    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1332    @(transitive_le
1333      total_program_size
1334      ((S program_size') + nat_of_bitvector … program_counter')
1335      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1336    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1337    >plus_n_Sm
1338    @monotonic_le_plus_r
1339    change with (
1340      nat_of_bitvector … program_counter' <
1341        nat_of_bitvector … program_counter'')
1342    assumption
[1663]1343  |6:
1344    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1345    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1346      <FETCH normalize nodelta <instr normalize nodelta
1347    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1348    * * * * #n'
1349    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1350    %
1351    [1:
1352      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1353      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1354      >(le_to_leb_true … program_counter_lt') %
1355    |2:
1356      assumption
1357    ]
1358  |11,14: (* JMP and MOVC *)
1359    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1360    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1361    <FETCH normalize nodelta <instr normalize nodelta
1362    try(<real_instruction_refl <instr normalize nodelta) *
1363    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1364    @(transitive_le
1365      total_program_size
1366      ((S program_size') + nat_of_bitvector … program_counter')
1367      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1368    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1369    >plus_n_Sm
1370    @monotonic_le_plus_r
1371    change with (
1372      nat_of_bitvector … program_counter' <
1373        nat_of_bitvector … program_counter'')
1374    assumption
1375  |12,15:
1376    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1377    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1378    <FETCH normalize nodelta <instr normalize nodelta *
1379    #program_counter_lt' #program_counter_lt_tps' %
1380    [1,3:
1381      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1382      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1383      >(le_to_leb_true … program_counter_lt') %
1384    |2,4:
1385      assumption
1386    ]
1387  |17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98,
1388   102,105:
1389    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1390    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1391    <FETCH normalize nodelta
1392    <real_instruction_refl <instr normalize nodelta *
1393    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1394    @(transitive_le
1395      total_program_size
1396      ((S program_size') + nat_of_bitvector … program_counter')
1397      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1398    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1399    >plus_n_Sm
1400    @monotonic_le_plus_r
1401    change with (
1402      nat_of_bitvector … program_counter' <
1403        nat_of_bitvector … program_counter'')
1404    assumption
1405  |18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78,
1406    81,84,87,90,93,96,99,103,106:
1407    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1408    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1409    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1410    #program_counter_lt' #program_counter_lt_tps' %
1411    try assumption
1412    [*:
1413      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1414      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1415      >(le_to_leb_true … program_counter_lt') %
1416    ]
[1658]1417  [1:
1418    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
1419    cases(block_cost' ?????? ?? ?) -block_cost'
1420    #recursive_block_cost #recursive_assm
1421    @(trace_any_label_inv_ind … the_trace)
1422    [1:
1423      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
1424      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
1425      cases classifier_assm
1426      whd in match (as_classifier ? ? ?);
1427      whd in ⊢ (??%? → ?);
1428      whd in match current_instruction; normalize nodelta
1429      whd in match current_instruction0; normalize nodelta
1430      #absurd @⊥ >p1 in absurd; normalize nodelta
1431      #absurd destruct(absurd)
1432    |2:
1433      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
1434      #start_status_refl #final_status_refl #the_trace_assm destruct
1435      whd in classifier_assm;
1436      whd in classifier_assm:(??%?);
1437      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1438      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1439      @⊥
1440      >p1 in classifier_assm; normalize nodelta
1441      #absurd destruct(absurd)
1442    |3:
1443      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1444      #classifier_assm #after_return_assm #trace_label_return #costed_assm
1445      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1446      destruct
1447      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
1448        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
1449          (execute_1 status_pre_fun_call) status_final
1450          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
1451          after_return_assm trace_label_return costed_assm) ? ?)
1452      [2: %
1453      |3:
1454      |1:
1455      ]
1456    |4:
1457      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1458      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1459      #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
1460      #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
1461    |5:
1462      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
1463      #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
1464      #the_trace_refl -the_trace_refl destruct
1465      whd in classifier_assm;
1466      whd in classifier_assm:(??%?);
1467      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1468      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1469      @⊥ >p1 in classifier_assm; normalize nodelta
1470      #absurd destruct(absurd)
1471    ]
1472  [1:
1473    #start_status #final_status #trace_ends_flag #the_trace
1474    #code_memory_refl #program_counter_refl
1475    cases(block_cost' ?????? ?? ?) -block_cost'
1476    #recursive_block_cost #recursive_assm
1477    @(trace_any_label_inv_ind … the_trace)
1478    [1:
1479      #start_status' #final_status' #execute_assm #not_return_assm
1480      #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
1481      #the_trace_assm
1482      cases daemon (* XXX: bug in notion of traces here *)
1483    |2:
1484
1485    |3:
1486      cases daemon (* XXX *)
1487    |4:
1488    ]
1489  |108:
1490    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1491    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1492    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1493    #program_counter_lt' #program_counter_lt_tps' %
1494    try assumption
1495    [*:
1496      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1497      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1498      >(le_to_leb_true … program_counter_lt') %
1499    ]
1500  [1:
1501    cases reachable_program_counter_witness #_ #hyp
1502    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
1503    @(le_to_lt_to_lt … base_case hyp)
1504  |2:
1505    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
[1642]1506    lapply(good_program_witness program_counter reachable_program_counter_witness)
1507      <FETCH normalize nodelta <instr normalize nodelta
[1645]1508    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
[1642]1509    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
1510    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1511    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1512    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1513    @(transitive_le
1514      total_program_size
1515      ((S program_size') + nat_of_bitvector … program_counter)
1516      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1517    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1518    >plus_n_Sm
1519    @monotonic_le_plus_r
1520    change with (
1521      nat_of_bitvector … program_counter <
1522        nat_of_bitvector … program_counter')
1523    assumption
1524  |3:
1525    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1526    lapply(good_program_witness program_counter reachable_program_counter_witness)
1527      <FETCH normalize nodelta <instr normalize nodelta
[1645]1528    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
[1642]1529    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
1530    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1531    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1532    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1533    %
1534    [1:
1535      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1536      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1537      >(le_to_leb_true … program_counter_lt') %
1538    |2:
1539      assumption
1540    ]
1541  |4:
1542    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1543    lapply(good_program_witness program_counter reachable_program_counter_witness)
1544      <FETCH normalize nodelta <instr normalize nodelta
[1645]1545    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
[1642]1546    * * * * #n'
1547    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1548    @(transitive_le
1549      total_program_size
1550      ((S program_size') + nat_of_bitvector … program_counter)
1551      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1552    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1553    >plus_n_Sm
1554    @monotonic_le_plus_r
1555    change with (
1556      nat_of_bitvector … program_counter <
1557        nat_of_bitvector … program_counter')
1558    assumption
1559  |5:
1560    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1561    lapply(good_program_witness program_counter reachable_program_counter_witness)
1562      <FETCH normalize nodelta <instr normalize nodelta
[1645]1563    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
[1642]1564    * * * * #n'
1565    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1566    %
1567    [1:
1568      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1569      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1570      >(le_to_leb_true … program_counter_lt') %
1571    |2:
1572      assumption
1573    ]
[1645]1574  |6,8: (* JMP and MOVC *)
[1642]1575    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1576    lapply(good_program_witness program_counter reachable_program_counter_witness)
1577    <FETCH normalize nodelta <instr normalize nodelta
1578    try(<real_instruction_refl <instr normalize nodelta) *
1579    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1580    @(transitive_le
1581      total_program_size
1582      ((S program_size') + nat_of_bitvector … program_counter)
1583      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1584    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1585    >plus_n_Sm
1586    @monotonic_le_plus_r
1587    change with (
1588      nat_of_bitvector … program_counter <
1589        nat_of_bitvector … program_counter')
1590    assumption
[1645]1591  |7,9:
[1642]1592    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1593    lapply(good_program_witness program_counter reachable_program_counter_witness)
[1645]1594    <FETCH normalize nodelta <instr normalize nodelta *
[1642]1595    #program_counter_lt' #program_counter_lt_tps' %
[1645]1596    [1,3:
[1642]1597      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1598      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1599      >(le_to_leb_true … program_counter_lt') %
[1645]1600    |2,4:
[1642]1601      assumption
1602    ]
1603  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
1604    55,57,59,61,63:
1605    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1606    lapply(good_program_witness program_counter reachable_program_counter_witness)
[1645]1607    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
[1642]1608    #program_counter_lt' #program_counter_lt_tps' %
[1645]1609    try assumption
1610    [*:
[1642]1611      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1612      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1613      >(le_to_leb_true … program_counter_lt') %
1614    ]
1615  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
1616    54,56,58,60,62:
1617    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1618    lapply(good_program_witness program_counter reachable_program_counter_witness)
1619    <FETCH normalize nodelta
1620    <real_instruction_refl <instr normalize nodelta *
1621    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1622    @(transitive_le
1623      total_program_size
1624      ((S program_size') + nat_of_bitvector … program_counter)
1625      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1626    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1627    >plus_n_Sm
1628    @monotonic_le_plus_r
1629    change with (
1630      nat_of_bitvector … program_counter <
1631        nat_of_bitvector … program_counter')
1632    assumption
1633  ]
1634qed.
1635
[1650]1636definition block_cost ≝
1637  λcode_memory: BitVectorTrie Byte 16.
1638  λprogram_counter: Word.
1639  λtotal_program_size: nat.
1640  λcost_labels: BitVectorTrie costlabel 16.
1641  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1642  λgood_program_witness: good_program code_memory total_program_size.
1643    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1644      reachable_program_counter_witness good_program_witness true ?.
1645  @le_plus_n_r
1646qed.
1647
[1646]1648lemma fetch_program_counter_n_Sn:
[1645]1649  ∀instruction: instruction.
1650  ∀program_counter, program_counter': Word.
1651  ∀ticks, n: nat.
1652  ∀code_memory: BitVectorTrie Byte 16.
1653    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1654      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
[1646]1655        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1656          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1657  #instruction #program_counter #program_counter' #ticks #n #code_memory
1658  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1659  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1660  <fetch_program_counter_n_hyp normalize nodelta
1661  <fetch_hyp normalize nodelta
1662  change with (
1663    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1664  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1665  >(le_to_leb_true … lt_hyp) %
1666qed.
1667
[1645]1668let rec traverse_code_internal
[1646]1669  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
1670    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
1671      (reachable_program_counter_witness:
1672          ∀lbl: costlabel.
1673          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1674            reachable_program_counter code_memory fixed_program_size program_counter)
1675        (good_program_witness: good_program code_memory fixed_program_size)
1676        on program_size: identifier_map CostTag nat ≝
1677  match program_size with
1678  [ O ⇒ empty_map …
1679  | S program_size ⇒
1680    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
1681    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
1682    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
1683    [ None ⇒ λlookup_refl. cost_mapping
1684    | Some lbl ⇒ λlookup_refl.
[1650]1685      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
[1645]1686        add … cost_mapping lbl cost
[1646]1687    ] (refl … (lookup_opt … program_counter cost_labels))
[1645]1688  ].
[1646]1689  [1:
1690    @(reachable_program_counter_witness lbl)
1691    assumption
1692  |2:
[1645]1693    assumption
[1642]1694  ]
[1639]1695qed.
[1486]1696
1697definition traverse_code ≝
[1645]1698  λcode_memory: BitVectorTrie Byte 16.
[1646]1699  λcost_labels: BitVectorTrie costlabel 16.
[1486]1700  λprogram_size: nat.
[1646]1701  λreachable_program_counter_witness:
1702          ∀lbl: costlabel.
1703          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1704            reachable_program_counter code_memory program_size program_counter.
[1645]1705  λgood_program_witness: good_program code_memory program_size.
[1646]1706    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
[1648]1707 
[1486]1708definition compute_costs ≝
1709  λprogram: list Byte.
[1557]1710  λcost_labels: BitVectorTrie costlabel 16.
[1648]1711  λreachable_program_witness.
[1645]1712  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
1713    let program_size ≝ |program| + 1 in
1714    let code_memory ≝ load_code_memory program in
[1648]1715      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
[1646]1716  @good_program_witness
[1645]1717qed.
Note: See TracBrowser for help on using the repository browser.