Changeset 1646


Ignore:
Timestamp:
Jan 16, 2012, 3:04:14 PM (8 years ago)
Author:
mulligan
Message:

finished the block_costs computation, and propagated the changes forward, subject to closing two axioms (an elimination principle, and a lemma on subvectors). moved some code around to its rightful place.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1645 r1646  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
    6 
    7 definition current_instruction0 ≝
    8   λmem,pc. \fst (\fst (fetch … mem pc)).
    9 
    10 definition current_instruction ≝
    11  λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
    12 
    13 definition ASM_classify0: instruction → status_class ≝
    14  λi.
    15   match i with
    16    [ RealInstruction pre ⇒
    17      match pre with
    18       [ RET ⇒ cl_return
    19       | JZ _ ⇒ cl_jump
    20       | JNZ _ ⇒ cl_jump
    21       | JC _ ⇒ cl_jump
    22       | JNC _ ⇒ cl_jump
    23       | JB _ _ ⇒ cl_jump
    24       | JNB _ _ ⇒ cl_jump
    25       | JBC _ _ ⇒ cl_jump
    26       | CJNE _ _ ⇒ cl_jump
    27       | DJNZ _ _ ⇒ cl_jump
    28       | _ ⇒ cl_other
    29       ]
    30    | ACALL _ ⇒ cl_call
    31    | LCALL _ ⇒ cl_call
    32    | JMP _ ⇒ cl_call
    33    | AJMP _ ⇒ cl_jump
    34    | LJMP _ ⇒ cl_jump
    35    | SJMP _ ⇒ cl_jump
    36    | _ ⇒ cl_other
    37    ].
    38 
    39 definition ASM_classify: Status → status_class ≝
    40  λs.ASM_classify0 (current_instruction s).
    41 
    42 definition current_instruction_is_labelled ≝
    43   λcost_labels: BitVectorTrie costlabel 16.
    44   λs: Status.
    45   let pc ≝ program_counter … s in
    46     match lookup_opt … pc cost_labels with
    47     [ None ⇒ False
    48     | _    ⇒ True
    49     ].
    50 
    51 definition label_of_current_instruction:
    52  BitVectorTrie costlabel 16 → Status → list costlabel
    53  ≝
    54   λcost_labels,s.
    55   let pc ≝ program_counter … s in
    56     match lookup_opt … pc cost_labels with
    57     [ None ⇒ []
    58     | Some l ⇒ [l]
    59     ].
    60 
    61 definition next_instruction_properly_relates_program_counters ≝
    62   λbefore: Status.
    63   λafter : Status.
    64   let size ≝ current_instruction_cost before in
    65   let pc_before ≝ program_counter … before in
    66   let pc_after ≝ program_counter … after in
    67   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    68     sum = pc_after.
    69 
    70 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    71  λcost_labels.
    72   mk_abstract_status
    73    Status
    74    (λs,s'. (execute_1 s) = s')
    75    (λs,class. ASM_classify s = class)
    76    (current_instruction_is_labelled cost_labels)
    77    next_instruction_properly_relates_program_counters.
    78 
    79 (* To be moved in ASM/arithmetic.ma *)
    80 definition addr16_of_addr11: Word → Word11 → Word ≝
    81   λpc: Word.
    82   λa: Word11.
    83   let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
    84   let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
    85   let 〈b123, b〉 ≝ split … 3 8 a in
    86   let b1 ≝ get_index_v … b123 0 ? in
    87   let b2 ≝ get_index_v … b123 1 ? in
    88   let b3 ≝ get_index_v … b123 2 ? in
    89   let p5 ≝ get_index_v … n2 0 ? in
    90     (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
    91   //
    92 qed.
    936
    947let rec fetch_program_counter_n
     
    11528    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
    11629        nat_of_bitvector 16 program_counter < program_size.
    117 
    118 axiom full_add_zero:
    119   ∀n: nat.
    120   ∀b: BitVector n.
    121     \snd (full_add n (zero …) b false) = b.
    122 
    123 lemma half_add_zero:
    124   ∀n: nat.
    125   ∀b: BitVector n.
    126     \snd (half_add n (zero …) b) = b.
    127   #n #b
    128   cases b
    129   [1:
    130     %
    131   |2:
    132     #n' #hd #tl
    133     cases hd
    134     whd in match half_add; normalize nodelta
    135     >full_add_zero %
    136   ]
    137 qed.
    13830   
    13931definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
     
    215107qed.
    216108
    217 lemma is_in_tail_to_is_in_cons_hd_tl:
     109lemma is_in_tl_to_is_in_cons_hd_tl:
    218110  ∀n: nat.
    219111  ∀the_vect: Vector addressing_mode_tag n.
     
    226118qed.
    227119
    228 lemma is_in_subvector_is_in_supervector:
     120axiom is_in_subvector_is_in_supervector:
    229121  ∀m, n: nat.
    230122  ∀subvector: Vector addressing_mode_tag m.
     123  ∀element: addressing_mode.
    231124  ∀supervector: Vector addressing_mode_tag n.
    232   ∀element: addressing_mode.
    233125    subvector_with … eq_a subvector supervector →
    234126      is_in m subvector element → is_in n supervector element.
    235   #m #n #subvector #supervector #element
    236   elim subvector
    237   [1:
    238     #subvector_proof #is_in_proof
    239     normalize in is_in_proof; cases is_in_proof
    240   |2:
    241     #n' #addressing_mode_tag #tail #ind_hyp #subvector_proof #is_in_proof
    242     @ind_hyp
    243     cases daemon (* XXX *)
    244   ]
    245 qed.
    246127
    247128let rec member_addressing_mode_tag
     
    344225    ]
    345226  ]
    346   @(is_in_subvector_is_in_supervector n m v fixed_v … proof)
     227  @(is_in_subvector_is_in_supervector … proof)
    347228  destruct @I
    348229qed.
     
    416297
    417298include alias "arithmetics/nat.ma".
    418 
    419 lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
    420   ∀m, n, o: nat.
    421     n < o → m + n < m + o.
    422   #m #n #o #assm /2 by monotonic_le_plus_r/
    423 qed.   
    424299
    425300let rec block_cost
     
    602477qed.
    603478
    604 axiom fetch_program_counter_n_Sn:
     479lemma fetch_program_counter_n_Sn:
    605480  ∀instruction: instruction.
    606481  ∀program_counter, program_counter': Word.
     
    609484    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
    610485      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
    611         Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
    612        
     486        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
     487          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
     488  #instruction #program_counter #program_counter' #ticks #n #code_memory
     489  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
     490  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
     491  <fetch_program_counter_n_hyp normalize nodelta
     492  <fetch_hyp normalize nodelta
     493  change with (
     494    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
     495  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
     496  >(le_to_leb_true … lt_hyp) %
     497qed.
     498
    613499let rec traverse_code_internal
    614   (program: list Byte) (code_memory: BitVectorTrie Byte 16)
    615     (cost_labels: BitVectorTrie costlabel 16) (program_counter: Word)
    616       (program_size: nat) (reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter)
    617         (good_program_witness: good_program code_memory program_size)
    618           (n: nat) (fetch_program_counter_proof: Some … program_counter = fetch_program_counter_n n code_memory (zero …))
    619         on program: identifier_map CostTag nat ≝
    620   let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
    621   match program with
    622   [ nil ⇒ empty_map …
    623   | cons hd tl ⇒
    624     match lookup_opt … program_counter cost_labels with
    625     [ None ⇒ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ?
    626     | Some lbl ⇒
    627       let cost ≝ block_cost code_memory program_counter program_size program_size cost_labels ? good_program_witness ? in
    628       let cost_mapping ≝ traverse_code_internal tl code_memory cost_labels new_program_counter program_size ? good_program_witness (S n) ? in
     500  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     501    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
     502      (reachable_program_counter_witness:
     503          ∀lbl: costlabel.
     504          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
     505            reachable_program_counter code_memory fixed_program_size program_counter)
     506        (good_program_witness: good_program code_memory fixed_program_size)
     507        on program_size: identifier_map CostTag nat ≝
     508  match program_size with
     509  [ O ⇒ empty_map …
     510  | S program_size ⇒
     511    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
     512    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
     513    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
     514    [ None ⇒ λlookup_refl. cost_mapping
     515    | Some lbl ⇒ λlookup_refl.
     516      let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size cost_labels ? good_program_witness ? in
    629517        add … cost_mapping lbl cost
    630     ]
     518    ] (refl … (lookup_opt … program_counter cost_labels))
    631519  ].
    632   [6:
     520  [1:
     521    @(reachable_program_counter_witness lbl)
     522    assumption
     523  |2:
    633524    //
    634   |2,4:
    635     @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n)
     525  |3:
    636526    assumption
    637   |5:
    638     assumption
    639   |1,3:
    640     whd in match reachable_program_counter; normalize nodelta
    641     @conj
    642     [1,3:
    643       %{(S n)}
    644       @(fetch_program_counter_n_Sn instruction program_counter new_program_counter ticks n)
    645       assumption
    646     |2,4:
    647       cases daemon (* XXX ??? *)
    648     ]
    649527  ]
    650528qed.
    651529
    652530definition traverse_code ≝
    653   λprogram: list Byte.
    654531  λcode_memory: BitVectorTrie Byte 16.
    655   λcost_labels.
     532  λcost_labels: BitVectorTrie costlabel 16.
    656533  λprogram_size: nat.
    657   λprogram_not_empty_proof: 0 < program_size.
     534  λreachable_program_counter_witness:
     535          ∀lbl: costlabel.
     536          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
     537            reachable_program_counter code_memory program_size program_counter.
    658538  λgood_program_witness: good_program code_memory program_size.
    659     traverse_code_internal program code_memory cost_labels (zero …) program_size ? good_program_witness.
    660   normalize @conj
    661   [2:
    662     assumption
    663   |1:
    664     %{0} %
    665   ]
    666 qed.
     539    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
    667540
    668541definition compute_costs ≝
     
    670543  λcost_labels: BitVectorTrie costlabel 16.
    671544  λhas_main: bool.
     545  λreachable_program_counter_witness:
     546   ∀lbl: costlabel.
     547   ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
     548     reachable_program_counter (load_code_memory program) (|program| + 1) program_counter. 
    672549  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
    673   λprogram_not_empty_proof: 0 < |program|.
    674550    let program_size ≝ |program| + 1 in
    675551    let code_memory ≝ load_code_memory program in
    676       traverse_code program code_memory cost_labels program_size ?.
    677   //
    678 qed.
     552      traverse_code code_memory cost_labels program_size reachable_program_counter_witness ?.
     553  @good_program_witness
     554qed.
  • src/ASM/Arithmetic.ma

    r1599 r1646  
    11include "ASM/BitVector.ma".
    22include "ASM/Util.ma".
     3
     4definition addr16_of_addr11: Word → Word11 → Word ≝
     5  λpc: Word.
     6  λa: Word11.
     7  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
     8  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
     9  let 〈b123, b〉 ≝ split … 3 8 a in
     10  let b1 ≝ get_index_v … b123 0 ? in
     11  let b2 ≝ get_index_v … b123 1 ? in
     12  let b3 ≝ get_index_v … b123 2 ? in
     13  let p5 ≝ get_index_v … n2 0 ? in
     14    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
     15  //
     16qed.
    317
    418definition nat_of_bool ≝
  • src/ASM/Vector.ma

    r1599 r1646  
    522522  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    523523
    524 
    525 definition subvector_with ≝
    526   λA: Type[0].
    527   λn: nat.
    528   λm: nat.
    529   λf: A → A → bool.
    530   λv: Vector A n.
    531   λq: Vector A m.
    532     fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
     524let rec subvector_with
     525  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     526    on sub: bool ≝
     527  match sub with
     528  [ VEmpty         ⇒ true
     529  | VCons n' hd tl ⇒
     530    if mem … eq … sup hd then
     531      subvector_with … eq tl sup
     532    else
     533      false
     534  ].
    533535   
    534536(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.