Changeset 1591 for src/ASM


Ignore:
Timestamp:
Dec 6, 2011, 5:24:45 PM (8 years ago)
Author:
mulligan
Message:

work from today

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1587 r1591  
    7272  mk_abstract_status
    7373   Status
    74    (λs,s'. eject … (execute_1 s) = s')
     74   (λs,s'. (execute_1 s) = s')
    7575   (λs,class. ASM_classify s = class)
    7676   (current_instruction_is_labelled cost_labels)
     
    9191  //
    9292qed.
    93 
    94 axiom size:
    95   ∀a: Type[0].
    96   ∀n: nat.
    97     BitVectorTrie Byte 16 → nat.
    98 
    99 (* XXX: need some precondition about pc not being too "big" to avoid overflow *)
    100 axiom fetch_pc_lt_new_pc:
    101   ∀mem: BitVectorTrie Byte 16.
    102   ∀pc: Word.
    103   ∀proof: nat_of_bitvector … pc < size Byte 16 mem.
    104     nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))).
    10593 
    10694axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
     
    10896    m - n ≤ m - S o → S m - n ≤ m - o.
    10997
    110 axiom strengthened_invariant:
     98lemma strengthened_invariant:
    11199  ∀code_memory: BitVectorTrie Byte 16.
    112   ∀program_size: nat.
    113   ∀code_memory_size: nat.
     100  ∀total_program_size: nat.
    114101  ∀new_program_counter: Word.
    115102  ∀program_counter: Word.
    116     code_memory_size ≤ size Byte 16 code_memory →
    117     program_size < code_memory_size →
    118       let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in
     103    total_program_size ≤ code_memory_size →
     104      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    119105        Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
    120106          new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
    121             nat_of_bitvector … program_counter < program_size →
    122               nat_of_bitvector … new_program_counter < program_size.
     107            nat_of_bitvector … program_counter ≤ total_program_size →
     108              nat_of_bitvector … new_program_counter ≤ total_program_size.
     109  #code_memory #total_program_size #new_program_counter #program_counter
     110  #relation_total_program_code_memory_size #end_instruction_is_ok
     111  #new_program_counter_from_fetch #program_counter_within_program
     112  >new_program_counter_from_fetch
     113  lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
     114   
    123115       
    124116(* XXX: use memoisation here in the future *)
    125117let rec block_cost
    126118  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    127     (program_counter: Word) (program_size: nat) (code_memory_size: nat)
    128       (size_invariant: code_memory_size ≤ size Byte 16 code_memory)
    129         (pc_invariant: nat_of_bitvector … program_counter < code_memory_size)
     119    (program_counter: Word) (program_size: nat) (total_program_size: nat)
     120      (size_invariant: total_program_size ≤ code_memory_size)
     121        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
    130122          (final_instr_invariant:
    131             let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in
     123            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    132124              Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
    133                 on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
    134   match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with
     125                on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
     126  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with
    135127  [ O ⇒ λabsurd. ⊥
    136128  | S program_size ⇒ λrecursive_case.
    137     let ticks ≝ \snd (fetch … code_memory pc) in
    138     let instr ≝ \fst (\fst (fetch … mem pc)) in
    139     let newpc ≝ \snd (\fst (fetch … mem pc)) in
     129    let ticks ≝ \snd (fetch … code_memory program_counter) in
     130    let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in
     131    let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in
    140132    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
    141133    [ None ⇒
     
    143135        match classify return λx. ∀classify_refl: x = classify. nat with
    144136        [ cl_jump ⇒ λclassify_refl. ticks
    145         | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
     137        | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    146138        | cl_return ⇒ λclassify_refl. ticks
    147         | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
     139        | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    148140        ] (refl … classify)
    149141    | Some _ ⇒ ticks
     
    153145    cases(lt_to_not_zero … absurd)
    154146  |2,4:
    155     cut(nat_of_bitvector … pc < nat_of_bitvector … newpc)
     147    cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
    156148    [1,3:
    157       @fetch_pc_lt_new_pc
     149      @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *)
    158150      lapply(transitive_lt
    159151        (nat_of_bitvector 16 pc)
  • src/ASM/Fetch.ma

    r1555 r1591  
    33include "ASM/ASM.ma".
    44
    5 definition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝
    6  λpmem: BitVectorTrie Byte 16.
    7  λpc: Word.
    8   〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
     5definition bitvector_max_nat ≝
     6  λlength: nat.
     7    2^length.
     8
     9definition code_memory_size ≝ bitvector_max_nat 16.
     10
     11include "ASM/JMCoercions.ma".
     12
     13axiom bitvector_lt_bitvector_max_nat:
     14  ∀length: nat.
     15  ∀v: BitVector length.
     16    nat_of_bitvector length v < bitvector_max_nat length.
     17
     18lemma word_lt_bitvector_max_nat:
     19  ∀w: Word.
     20    nat_of_bitvector … w < code_memory_size.
     21  #w //
     22qed.
     23   
     24axiom w_lt_half_add_increment:
     25  ∀length: nat.
     26  ∀v: BitVector length.
     27  ∀proof: nat_of_bitvector … v < bitvector_max_nat length - 1.
     28    nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))).
     29
     30definition next: BitVectorTrie Byte 16 → ∀program_counter: Word.
     31    nat_of_bitvector … program_counter < (code_memory_size - 1) →
     32      Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝
     33  λpmem: BitVectorTrie Byte 16.
     34  λpc: Word.
     35  λproof.
     36    〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
     37  @w_lt_half_add_increment @proof
     38qed.
    939
    1040(* timings taken from SIEMENS *)
    1141
    12 definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝
    13  λpmem: BitVectorTrie Byte 16.
    14  λpc_v.
    15   let 〈pc,v〉 ≝ pc_v in
     42definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
     43  nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
     44  Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
     45  λpmem.
     46  λpc.
     47  λv.
     48  λproof.
    1649   let 〈b,v〉 ≝ head … v in if b then
    1750    let 〈b,v〉 ≝ head … v in if b then
     
    2659         else
    2760          let 〈b,v〉≝  head … v in if b then
    28            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
     61           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    2962          else
    3063           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
     
    3467         else
    3568          let 〈b,v〉≝  head … v in if b then
    36            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     69           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    3770          else
    3871           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
     
    4679         else
    4780          let 〈b,v〉≝  head … v in if b then
    48            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
     81           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
    4982          else
    5083           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
     
    5487         else
    5588          let 〈b,v〉≝  head … v in if b then
    56            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     89           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    5790          else
    5891           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
     
    6093      let 〈b,v〉≝  head … v in if b then
    6194       let 〈b,v〉≝  head … v in if b then
    62         let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     95        let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
    6396       else
    6497        let 〈b,v〉≝  head … v in if b then
     
    67100         else
    68101          let 〈b,v〉≝  head … v in if b then
    69            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     102           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    70103          else
    71104           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
     
    75108           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
    76109          else
    77            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
    78          else
    79           let 〈b,v〉≝  head … v in if b then
    80            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    81           else
    82            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
     110           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
     111         else
     112          let 〈b,v〉≝  head … v in if b then
     113           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     114          else
     115           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
    83116      else
    84117       let 〈b,v〉≝  head … v in if b then
     
    90123         else
    91124          let 〈b,v〉≝  head … v in if b then
    92            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
     125           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
    93126          else
    94127           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
     
    98131           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
    99132          else
    100            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
    101          else
    102           let 〈b,v〉≝  head … v in if b then
    103            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    104           else
    105            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
     133           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
     134         else
     135          let 〈b,v〉≝  head … v in if b then
     136           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     137          else
     138           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    106139    else
    107140     let 〈b,v〉≝  head … v in if b then
    108141      let 〈b,v〉≝  head … v in if b then
    109142       let 〈b,v〉≝  head … v in if b then
    110         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    111        else
    112         let 〈b,v〉≝  head … v in if b then
    113          let 〈b,v〉≝  head … v in if b then
    114           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    115          else
    116           let 〈b,v〉≝  head … v in if b then
    117            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    118           else
    119            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     143        let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     144       else
     145        let 〈b,v〉≝  head … v in if b then
     146         let 〈b,v〉≝  head … v in if b then
     147          let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     148         else
     149          let 〈b,v〉≝  head … v in if b then
     150           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     151          else
     152           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    120153        else
    121154         let 〈b,v〉≝  head … v in if b then
     
    123156           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
    124157          else
    125            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
    126          else
    127           let 〈b,v〉≝  head … v in if b then
    128            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    129           else
    130            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    131       else
    132        let 〈b,v〉≝  head … v in if b then
    133         let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
    134        else
    135         let 〈b,v〉≝  head … v in if b then
    136          let 〈b,v〉≝  head … v in if b then
    137           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
     158           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
     159         else
     160          let 〈b,v〉≝  head … v in if b then
     161           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     162          else
     163           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     164      else
     165       let 〈b,v〉≝  head … v in if b then
     166        let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
     167       else
     168        let 〈b,v〉≝  head … v in if b then
     169         let 〈b,v〉≝  head … v in if b then
     170          let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
    138171         else
    139172          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
     
    143176           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
    144177          else
    145            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
    146          else
    147           let 〈b,v〉≝  head … v in if b then
    148            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    149           else
    150            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     178           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
     179         else
     180          let 〈b,v〉≝  head … v in if b then
     181           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     182          else
     183           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    151184     else
    152185      let 〈b,v〉≝  head … v in if b then
     
    159192         else
    160193          let 〈b,v〉≝  head … v in if b then
    161            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
    162           else
    163            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
     194           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
     195          else
     196           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
    164197        else
    165198         let 〈b,v〉≝  head … v in if b then
     
    167200           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
    168201          else
    169            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
    170          else
    171           let 〈b,v〉≝  head … v in if b then
    172            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    173           else
    174            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
    175       else
    176        let 〈b,v〉≝  head … v in if b then
    177         let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
    178        else
    179         let 〈b,v〉≝  head … v in if b then
    180          let 〈b,v〉≝  head … v in if b then
    181           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
    182          else
    183           let 〈b,v〉≝  head … v in if b then
    184            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     202           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
     203         else
     204          let 〈b,v〉≝  head … v in if b then
     205           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     206          else
     207           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     208      else
     209       let 〈b,v〉≝  head … v in if b then
     210        let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
     211       else
     212        let 〈b,v〉≝  head … v in if b then
     213         let 〈b,v〉≝  head … v in if b then
     214          let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
     215         else
     216          let 〈b,v〉≝  head … v in if b then
     217           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
    185218          else
    186219           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
     
    190223           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
    191224          else
    192            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    193          else
    194           let 〈b,v〉≝  head … v in if b then
    195            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    196           else
    197            let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
     225           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     226         else
     227          let 〈b,v〉≝  head … v in if b then
     228           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     229          else
     230           let 〈pc,b1〉≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
    198231   else
    199232    let 〈b,v〉≝  head … v in if b then
     
    201234      let 〈b,v〉≝  head … v in if b then
    202235       let 〈b,v〉≝  head … v in if b then
    203         let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
    204        else
    205         let 〈b,v〉≝  head … v in if b then
    206          let 〈b,v〉≝  head … v in if b then
    207           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
    208          else
    209           let 〈b,v〉≝  head … v in if b then
    210            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
    211           else
    212            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
     236        let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
     237       else
     238        let 〈b,v〉≝  head … v in if b then
     239         let 〈b,v〉≝  head … v in if b then
     240          let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
     241         else
     242          let 〈b,v〉≝  head … v in if b then
     243           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     244          else
     245           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
    213246        else
    214247         let 〈b,v〉≝  head … v in if b then
     
    216249           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
    217250          else
    218            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    219          else
    220           let 〈b,v〉≝  head … v in if b then
    221            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    222           else
    223            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
     251           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     252         else
     253          let 〈b,v〉≝  head … v in if b then
     254           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     255          else
     256           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
    224257      else
    225258       let 〈b,v〉≝  head … v in if b then
     
    231264         else
    232265          let 〈b,v〉≝  head … v in if b then
    233            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    234           else
    235            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    236         else
    237          let 〈b,v〉≝  head … v in if b then
    238           let 〈b,v〉≝  head … v in if b then
    239            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    240           else
    241            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
    242          else
    243           let 〈b,v〉≝  head … v in if b then
    244            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    245           else
    246            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
     266           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     267          else
     268           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     269        else
     270         let 〈b,v〉≝  head … v in if b then
     271          let 〈b,v〉≝  head … v in if b then
     272           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     273          else
     274           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     275         else
     276          let 〈b,v〉≝  head … v in if b then
     277           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     278          else
     279           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
    247280     else
    248281      let 〈b,v〉≝  head … v in if b then
     
    255288         else
    256289          let 〈b,v〉≝  head … v in if b then
    257            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    258           else
    259            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    260         else
    261          let 〈b,v〉≝  head … v in if b then
    262           let 〈b,v〉≝  head … v in if b then
    263            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    264           else
    265            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    266          else
    267           let 〈b,v〉≝  head … v in if b then
    268            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    269           else
    270            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
     290           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     291          else
     292           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     293        else
     294         let 〈b,v〉≝  head … v in if b then
     295          let 〈b,v〉≝  head … v in if b then
     296           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     297          else
     298           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     299         else
     300          let 〈b,v〉≝  head … v in if b then
     301           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     302          else
     303           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
    271304      else
    272305       let 〈b,v〉≝  head … v in if b then
     
    278311         else
    279312          let 〈b,v〉≝  head … v in if b then
    280            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    281           else
    282            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    283         else
    284          let 〈b,v〉≝  head … v in if b then
    285           let 〈b,v〉≝  head … v in if b then
    286            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    287           else
    288            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    289          else
    290           let 〈b,v〉≝  head … v in if b then
    291            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    292           else
    293            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
     313           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     314          else
     315           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     316        else
     317         let 〈b,v〉≝  head … v in if b then
     318          let 〈b,v〉≝  head … v in if b then
     319           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     320          else
     321           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     322         else
     323          let 〈b,v〉≝  head … v in if b then
     324           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     325          else
     326           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    294327    else
    295328     let 〈b,v〉≝  head … v in if b then
     
    303336         else
    304337          let 〈b,v〉≝  head … v in if b then
    305            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
    306           else
    307            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
     338           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
     339          else
     340           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
    308341        else
    309342         let 〈b,v〉≝  head … v in if b then
     
    314347         else
    315348          let 〈b,v〉≝  head … v in if b then
    316            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    317           else
    318            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     349           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     350          else
     351           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    319352      else
    320353       let 〈b,v〉≝  head … v in if b then
     
    326359         else
    327360          let 〈b,v〉≝  head … v in if b then
    328            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
    329           else
    330            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
     361           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
     362          else
     363           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
    331364        else
    332365         let 〈b,v〉≝  head … v in if b then
     
    337370         else
    338371          let 〈b,v〉≝  head … v in if b then
    339            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    340           else
    341            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     372           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     373          else
     374           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    342375     else
    343376      let 〈b,v〉≝  head … v in if b then
     
    350383         else
    351384          let 〈b,v〉≝  head … v in if b then
    352            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
     385           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
    353386          else
    354387           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
     
    358391           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    359392          else
    360            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    361          else
    362           let 〈b,v〉≝  head … v in if b then
    363            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    364           else
    365            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     393           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     394         else
     395          let 〈b,v〉≝  head … v in if b then
     396           let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     397          else
     398           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    366399      else
    367400       let 〈b,v〉≝  head … v in if b then
     
    373406         else
    374407          let 〈b,v〉≝  head … v in if b then
    375            let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
     408           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
    376409          else
    377410           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
     
    381414           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    382415          else
    383            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    384          else
    385           let 〈b,v〉≝  head … v in if b then
    386            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     416           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     417         else
     418          let 〈b,v〉≝  head … v in if b then
     419           let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    387420          else
    388421           〈〈RealInstruction (NOP …), pc〉, 1〉.
    389   %.
     422  try %
     423  cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *)
    390424qed.
    391425
    392 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
    393  λpmem: BitVectorTrie Byte 16.
    394  λpc: Word.
    395   fetch0 pmem (next pmem pc).
     426definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.
     427    Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
     428  λpmem: BitVectorTrie Byte 16.
     429  λpc: Word.
     430  let 〈word, byte〉 ≝ next pmem pc ? in
     431    fetch0 pmem word byte ?.
     432  cases daemon (* XXX: todo, proofs about size of pc *)
     433qed.
Note: See TracChangeset for help on using the changeset viewer.