Changeset 1916


Ignore:
Timestamp:
May 4, 2012, 1:59:00 PM (7 years ago)
Author:
mulligan
Message:

Closed remaining daemons in block_cost'. Rest of file now typechecks to end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1913 r1916  
    7777      ] (subaddressing_modein … addr)
    7878    | AJMP  addr         ⇒
    79       match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
     79      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
     80        reachable_program_counter code_memory total_program_size jump_target
     81      (*match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    8082      [ ADDR11 addr ⇒ λaddr11: True.
    8183        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
     
    8789          reachable_program_counter code_memory total_program_size new_program_counter
    8890      | _ ⇒ λother: False. ⊥
    89       ] (subaddressing_modein … addr)
     91      ] (subaddressing_modein … addr) *)
    9092    | LJMP  addr         ⇒
    91       match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
     93      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
     94        reachable_program_counter code_memory total_program_size jump_target
     95      (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    9296      [ ADDR16 addr ⇒ λaddr16: True.
    9397          reachable_program_counter code_memory total_program_size addr
    9498      | _ ⇒ λother: False. ⊥
    95       ] (subaddressing_modein … addr)
     99      ] (subaddressing_modein … addr)*)
    96100    | SJMP  addr     ⇒
    97       match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
     101      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
     102        reachable_program_counter code_memory total_program_size jump_target
     103      (*match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
    98104      [ RELATIVE addr ⇒ λrelative: True.
    99105        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
    100106          reachable_program_counter code_memory total_program_size new_program_counter
    101107      | _ ⇒ λother: False. ⊥
    102       ] (subaddressing_modein … addr)
     108      ] (subaddressing_modein … addr)*)
    103109    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
    104110      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     
    837843    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    838844    cases (block_cost' ????????) -block_cost'
    839     cases daemon
     845    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
     846    whd in match (program_counter_after_other ??); normalize nodelta destruct
     847    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
    840848  ]
    841849  -block_cost'
     
    893901    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    894902    >(le_to_leb_true … program_counter_lt') %
    895   |*: (* XXX: unconditional jumps *)
    896     cases daemon
     903  |29,30,31: (* XXX: unconditional jumps *)
     904    normalize nodelta
     905    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     906    lapply (good_program_witness program_counter' reachable_program_counter_witness)
     907    <FETCH normalize nodelta <instr normalize nodelta #assm assumption
    897908  ]
    898909qed.
Note: See TracChangeset for help on using the changeset viewer.