Changeset 1919 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 7, 2012, 11:12:13 AM (8 years ago)
Author:
mulligan
Message:

Fixes to get everything compiling again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1916 r1919  
    7979      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    8080        reachable_program_counter code_memory total_program_size jump_target
    81       (*match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    82       [ ADDR11 addr ⇒ λaddr11: True.
    83         let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
    84         let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
    85         let bit ≝ get_index' … O ? nl in
    86         let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
    87         let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    88         let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
    89           reachable_program_counter code_memory total_program_size new_program_counter
    90       | _ ⇒ λother: False. ⊥
    91       ] (subaddressing_modein … addr) *)
    9281    | LJMP  addr         ⇒
    9382      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    9483        reachable_program_counter code_memory total_program_size jump_target
    95       (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    96       [ ADDR16 addr ⇒ λaddr16: True.
    97           reachable_program_counter code_memory total_program_size addr
    98       | _ ⇒ λother: False. ⊥
    99       ] (subaddressing_modein … addr)*)
    10084    | SJMP  addr     ⇒
    10185      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
    10286        reachable_program_counter code_memory total_program_size jump_target
    103       (*match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
    104       [ RELATIVE addr ⇒ λrelative: True.
    105         let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
    106           reachable_program_counter code_memory total_program_size new_program_counter
    107       | _ ⇒ λother: False. ⊥
    108       ] (subaddressing_modein … addr)*)
    10987    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
    11088      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     
    134112    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    135113      program_counter ? code_memory after = program_counter_after.
    136 (* XXX: why defined like this?
    137   let size ≝ current_instruction_cost code_memory before in
    138   let pc_before ≝ program_counter … code_memory before in
    139   let pc_after ≝ program_counter … code_memory after in
    140   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    141     sum = pc_after.
    142 *)
    143114
    144115definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     
    148119      (Status code_memory)
    149120      (λs,s'. (execute_1 … s) = s')
     121      ?
     122      ?
    150123      (λs,class. ASM_classify … s = class)
    151124      (current_instruction_is_labelled … cost_labels)
    152       (next_instruction_properly_relates_program_counters code_memory).
     125      (next_instruction_properly_relates_program_counters code_memory)
     126      ?.
     127  cases daemon (* XXX: new additions to abstract status record *)
     128qed.
    153129
    154130let rec trace_any_label_length
     
    172148  ].
    173149
    174 let rec trace_any_label_length'
    175   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    176     (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    177       (final_status: Status code_memory)
    178       (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
    179         on the_trace: nat ≝
    180   match the_trace with
    181   [ tal_base_not_return the_status _ _ _ _ ⇒ 1
    182   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 1
    183   | tal_base_return the_status _ _ _ ⇒ 1
    184   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
    185       let tail_length ≝ trace_any_label_length' … final_trace in
    186         S tail_length
    187   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    188       let tail_length ≝ trace_any_label_length' … tail_trace in
    189         S tail_length       
    190   ].
     150definition trace_any_label_length' ≝
     151  λcode_memory: BitVectorTrie Byte 16.
     152  λcost_labels: BitVectorTrie costlabel 16.
     153  λtrace_ends_flag: trace_ends_with_ret.
     154  λstart_status: Status code_memory.
     155  λfinal_status: Status code_memory.
     156  λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
     157    as_trace_any_label_length' … the_trace.
    191158
    192159let rec compute_paid_trace_any_label
     
    618585          @plus_right_monotone whd in ⊢ (???%); <FETCH %
    619586        |2:
    620           normalize in size_invariant;
    621           lapply (le_S_S_to_le … size_invariant)
    622           #assm assumption
     587          @le_S_S_to_le @size_invariant
    623588        |3:
    624589          %
     
    11941159inverter nat_jmdiscr for nat.
    11951160
    1196 (* XXX: this is false in the general case.  For instance, if n = 0 then the
    1197         base case requires us prove 1 = 0, as it is the carry bit that holds
    1198         the result of the addition. *)
    1199 axiom succ_nat_of_bitvector_half_add_1:
    1200   ∀n: nat.
    1201   ∀bv: BitVector n.
    1202   ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    1203     S (nat_of_bitvector … bv) = nat_of_bitvector …
    1204       (\snd (half_add n (bitvector_of_nat … 1) bv)).
    1205 
    12061161lemma plus_lt_to_lt:
    12071162  ∀m, n, o: nat.
     
    12451200    lapply (injective_S … absurd) -absurd #absurd
    12461201    /2/
    1247   ]
    1248 qed.
    1249 
    1250 lemma generalized_nat_cases:
    1251   ∀n: nat.
    1252     n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m).
    1253   #n
    1254   cases n
    1255   [1:
    1256     @or_introl @or_introl %
    1257   |2:
    1258     #n' cases n'
    1259     [1:
    1260       @or_introl @or_intror %
    1261     |2:
    1262       #n'' @or_intror %{n''} %
    1263     ]
    12641202  ]
    12651203qed.
Note: See TracChangeset for help on using the changeset viewer.