Changeset 1591 for src/ASM/Fetch.ma


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

work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.