Changeset 1604 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Dec 14, 2011, 11:52:28 AM (8 years ago)
Author:
mulligan
Message:

for jaap

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Fetch.ma

    r1602 r1604  
    1010definition code_memory_size ≝ bitvector_max_nat 16.
    1111
    12 axiom bitvector_lt_bitvector_max_nat:
    13   ∀length: nat.
    14   ∀v: BitVector length.
    15     nat_of_bitvector length v < bitvector_max_nat length.
    16 
    17 lemma word_lt_bitvector_max_nat:
    18   ∀w: Word.
    19     nat_of_bitvector … w < code_memory_size.
    20   #w //
    21 qed.
    22    
    23 axiom w_lt_half_add_increment:
    24   ∀length: nat.
    25   ∀v: BitVector length.
    26   ∀proof: nat_of_bitvector … v < bitvector_max_nat length - 1.
    27     nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))).
    28 
    29 lemma minus_leq_minus:
    30   ∀m, n, o: nat.
    31     n ≤ m → o ≤ m → o ≤ n → m - n ≤ m - o.
    32   #m #n #o #m_le_n #m_le_o #o_le_n
    33   cases daemon (* XXX: todo *)
    34 qed.
    35 
    36 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word.
    37     nat_of_bitvector … program_counter < (code_memory_size - 24) →
    38       Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ∧
    39         (nat_of_bitvector … (\fst ret)) ≤ code_memory_size ≝
     12definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    4013  λpmem: BitVectorTrie Byte 16.
    4114  λpc: Word.
    42   λproof.
    4315    〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
    44   @conj
    45   [1:
    46     @w_lt_half_add_increment
    47     @(transitive_le
    48       (S (nat_of_bitvector … pc))
    49       (code_memory_size - 24)
    50       (code_memory_size - 1) ? ?)
    51     [1:
    52       @proof
    53     |2:
    54       @(minus_leq_minus code_memory_size 24 1) //
    55     ]
    56   |2:
    57     cases daemon (* XXX: todo *)
    58   ]
    59 qed.
    60 
    61 axiom o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p:
    62   ∀m, n, o, p: nat.
    63     p < o → m < n - o → m < n - p.
    64 
    65 lemma pair_eq_1_jmeq:
    66   ∀a, b: Type[0].
    67   ∀a1, a2: a.
    68   ∀b1, b2: b.
    69     〈a1, b1〉 ≃ 〈a2, b2〉 → a1 = a2.
    70   #a #b #a1 #a2 #b1 #b2 #assm
    71   cases daemon (* XXX: no jm discrimination for pairs *)
    72 qed.
    73    
    74 lemma prod_fst_jmeq:
    75   ∀a, b: Type[0].
    76   ∀p: a × b.
    77   ∀l: a.
    78   ∀r: b.
    79     p ≃ 〈l, r〉 → l = fst … p.
    80   #a #b #p #l #r
    81   cases p #aa #bb #assm @sym_eq
    82   lapply (pair_eq_1_jmeq a b aa l bb r assm)
    83   #assm assumption
    84 qed.
    85 
    86 lemma lt_to_le:
    87   ∀m, n: nat.
    88     m < n → m ≤ n.
    89   #m #n #assm /2 by le_S_to_le/
    90 qed.
    9116
    9217lemma Prod_inv_rect_Type0:
    … …  
    11237(* timings taken from SIEMENS *)
    11338
    114 definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
    115   nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
    116   Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
     39definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
     40    ∀program_counter: Word. Byte → instruction × Word × nat ≝
    11741  λpmem.
    11842  λpc.
    11943  λv.
    120   λproof.
    12144   let 〈b,v〉 ≝ head … v in if b then
    12245    let 〈b,v〉 ≝ head … v in if b then
    … …  
    13154         else
    13255          let 〈b,v〉≝  head … v in if b then
    133            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
     56           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    13457          else
    13558           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
    … …  
    13962         else
    14063          let 〈b,v〉≝  head … v in if b then
    141            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     64           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    14265          else
    14366           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
    … …  
    15174         else
    15275          let 〈b,v〉≝  head … v in if b then
    153            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
     76           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
    15477          else
    15578           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
    … …  
    15982         else
    16083          let 〈b,v〉≝  head … v in if b then
    161            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     84           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    16285          else
    16386           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
    … …  
    16588      let 〈b,v〉≝  head … v in if b then
    16689       let 〈b,v〉≝  head … v in if b then
    167         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     90        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
    16891       else
    16992        let 〈b,v〉≝  head … v in if b then
    … …  
    17295         else
    17396          let 〈b,v〉≝  head … v in if b then
    174            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     97           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    17598          else
    17699           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
    … …  
    180103           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
    181104          else
    182            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
    183          else
    184           let 〈b,v〉≝  head … v in if b then
    185            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    186           else
    187            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
     105           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
     106         else
     107          let 〈b,v〉≝  head … v in if b then
     108           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     109          else
     110           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
    188111      else
    189112       let 〈b,v〉≝  head … v in if b then
    … …  
    195118         else
    196119          let 〈b,v〉≝  head … v in if b then
    197            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
     120           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
    198121          else
    199122           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
    … …  
    203126           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
    204127          else
    205            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
    206          else
    207           let 〈b,v〉≝  head … v in if b then
    208            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    209           else
    210            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
     128           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
     129         else
     130          let 〈b,v〉≝  head … v in if b then
     131           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     132          else
     133           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    211134    else
    212135     let 〈b,v〉≝  head … v in if b then
    213136      let 〈b,v〉≝  head … v in if b then
    214137       let 〈b,v〉≝  head … v in if b then
    215         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    216        else
    217         let 〈b,v〉≝  head … v in if b then
    218          let 〈b,v〉≝  head … v in if b then
    219           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    220          else
    221           let 〈b,v〉≝  head … v in if b then
    222            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    223           else
    224            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     138        let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     139       else
     140        let 〈b,v〉≝  head … v in if b then
     141         let 〈b,v〉≝  head … v in if b then
     142          let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     143         else
     144          let 〈b,v〉≝  head … v in if b then
     145           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     146          else
     147           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    225148        else
    226149         let 〈b,v〉≝  head … v in if b then
    … …  
    228151           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
    229152          else
    230            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
    231          else
    232           let 〈b,v〉≝  head … v in if b then
    233            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    234           else
    235            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    236       else
    237        let 〈b,v〉≝  head … v in if b then
    238         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
    239        else
    240         let 〈b,v〉≝  head … v in if b then
    241          let 〈b,v〉≝  head … v in if b then
    242           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
     153           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
     154         else
     155          let 〈b,v〉≝  head … v in if b then
     156           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     157          else
     158           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     159      else
     160       let 〈b,v〉≝  head … v in if b then
     161        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
     162       else
     163        let 〈b,v〉≝  head … v in if b then
     164         let 〈b,v〉≝  head … v in if b then
     165          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
    243166         else
    244167          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
    … …  
    248171           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
    249172          else
    250            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
    251          else
    252           let 〈b,v〉≝  head … v in if b then
    253            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    254           else
    255            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     173           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
     174         else
     175          let 〈b,v〉≝  head … v in if b then
     176           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     177          else
     178           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    256179     else
    257180      let 〈b,v〉≝  head … v in if b then
    … …  
    264187         else
    265188          let 〈b,v〉≝  head … v in if b then
    266            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
    267           else
    268            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
     189           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
     190          else
     191           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
    269192        else
    270193         let 〈b,v〉≝  head … v in if b then
    … …  
    272195           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
    273196          else
    274            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
    275          else
    276           let 〈b,v〉≝  head … v in if b then
    277            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    278           else
    279            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
    280       else
    281        let 〈b,v〉≝  head … v in if b then
    282         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
    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〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
    287          else
    288           let 〈b,v〉≝  head … v in if b then
    289            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     197           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
     198         else
     199          let 〈b,v〉≝  head … v in if b then
     200           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     201          else
     202           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     203      else
     204       let 〈b,v〉≝  head … v in if b then
     205        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
     206       else
     207        let 〈b,v〉≝  head … v in if b then
     208         let 〈b,v〉≝  head … v in if b then
     209          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
     210         else
     211          let 〈b,v〉≝  head … v in if b then
     212           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
    290213          else
    291214           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
    … …  
    295218           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
    296219          else
    297            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    298          else
    299           let 〈b,v〉≝  head … v in if b then
    300            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    301           else
    302            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
     220           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     221         else
     222          let 〈b,v〉≝  head … v in if b then
     223           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     224          else
     225           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
    303226   else
    304227    let 〈b,v〉≝  head … v in if b then
    … …  
    306229      let 〈b,v〉≝  head … v in if b then
    307230       let 〈b,v〉≝  head … v in if b then
    308         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
    309        else
    310         let 〈b,v〉≝  head … v in if b then
    311          let 〈b,v〉≝  head … v in if b then
    312           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
    313          else
    314           let 〈b,v〉≝  head … v in if b then
    315            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
    316           else
    317            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
     231        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
     232       else
     233        let 〈b,v〉≝  head … v in if b then
     234         let 〈b,v〉≝  head … v in if b then
     235          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
     236         else
     237          let 〈b,v〉≝  head … v in if b then
     238           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     239          else
     240           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
    318241        else
    319242         let 〈b,v〉≝  head … v in if b then
    … …  
    321244           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
    322245          else
    323            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    324          else
    325           let 〈b,v〉≝  head … v in if b then
    326            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    327           else
    328            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
     246           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     247         else
     248          let 〈b,v〉≝  head … v in if b then
     249           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     250          else
     251           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
    329252      else
    330253       let 〈b,v〉≝  head … v in if b then
    … …  
    336259         else
    337260          let 〈b,v〉≝  head … v in if b then
    338            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    339           else
    340            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    341         else
    342          let 〈b,v〉≝  head … v in if b then
    343           let 〈b,v〉≝  head … v in if b then
    344            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    345           else
    346            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
    347          else
    348           let 〈b,v〉≝  head … v in if b then
    349            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    350           else
    351            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
     261           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     262          else
     263           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     264        else
     265         let 〈b,v〉≝  head … v in if b then
     266          let 〈b,v〉≝  head … v in if b then
     267           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     268          else
     269           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     270         else
     271          let 〈b,v〉≝  head … v in if b then
     272           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     273          else
     274           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
    352275     else
    353276      let 〈b,v〉≝  head … v in if b then
    … …  
    360283         else
    361284          let 〈b,v〉≝  head … v in if b then
    362            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    363           else
    364            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    365         else
    366          let 〈b,v〉≝  head … v in if b then
    367           let 〈b,v〉≝  head … v in if b then
    368            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    369           else
    370            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    371          else
    372           let 〈b,v〉≝  head … v in if b then
    373            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    374           else
    375            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
     285           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     286          else
     287           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     288        else
     289         let 〈b,v〉≝  head … v in if b then
     290          let 〈b,v〉≝  head … v in if b then
     291           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     292          else
     293           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     294         else
     295          let 〈b,v〉≝  head … v in if b then
     296           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     297          else
     298           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
    376299      else
    377300       let 〈b,v〉≝  head … v in if b then
    … …  
    383306         else
    384307          let 〈b,v〉≝  head … v in if b then
    385            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    386           else
    387            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    388         else
    389          let 〈b,v〉≝  head … v in if b then
    390           let 〈b,v〉≝  head … v in if b then
    391            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    392           else
    393            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    394          else
    395           let 〈b,v〉≝  head … v in if b then
    396            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    397           else
    398            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
     308           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     309          else
     310           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     311        else
     312         let 〈b,v〉≝  head … v in if b then
     313          let 〈b,v〉≝  head … v in if b then
     314           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     315          else
     316           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     317         else
     318          let 〈b,v〉≝  head … v in if b then
     319           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     320          else
     321           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    399322    else
    400323     let 〈b,v〉≝  head … v in if b then
    … …  
    408331         else
    409332          let 〈b,v〉≝  head … v in if b then
    410            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
    411           else
    412            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
     333           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
     334          else
     335           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
    413336        else
    414337         let 〈b,v〉≝  head … v in if b then
    … …  
    419342         else
    420343          let 〈b,v〉≝  head … v in if b then
    421            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    422           else
    423            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     344           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     345          else
     346           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    424347      else
    425348       let 〈b,v〉≝  head … v in if b then
    … …  
    431354         else
    432355          let 〈b,v〉≝  head … v in if b then
    433            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
    434           else
    435            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
     356           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
     357          else
     358           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
    436359        else
    437360         let 〈b,v〉≝  head … v in if b then
    … …  
    442365         else
    443366          let 〈b,v〉≝  head … v in if b then
    444            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    445           else
    446            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     367           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     368          else
     369           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    447370     else
    448371      let 〈b,v〉≝  head … v in if b then
    … …  
    455378         else
    456379          let 〈b,v〉≝  head … v in if b then
    457            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
     380           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
    458381          else
    459382           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
    … …  
    463386           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    464387          else
    465            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    466          else
    467           let 〈b,v〉≝  head … v in if b then
    468            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    469           else
    470            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     388           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     389         else
     390          let 〈b,v〉≝  head … v in if b then
     391           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     392          else
     393           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    471394      else
    472395       let 〈b,v〉≝  head … v in if b then
    … …  
    478401         else
    479402          let 〈b,v〉≝  head … v in if b then
    480            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
     403           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
    481404          else
    482405           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
    … …  
    486409           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    487410          else
    488            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    489          else
    490           let 〈b,v〉≝  head … v in if b then
    491            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     411           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     412         else
     413          let 〈b,v〉≝  head … v in if b then
     414           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    492415          else
    493416           〈〈RealInstruction (NOP …), pc〉, 1〉.
    494   try %
    495   cases daemon (*
    496   try (
    497     @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
    498       (nat_of_bitvector 16 pc) code_memory_size 24 1
    499       (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)
    500   )
    501   [6,8,14,15,16,17,20,21,22,23,25,28,30,31,32,33,34,37,38,39,40,41,44,45,46,47,
    502    50,51,52,53,56,57,58,59,65,69,71,73,75:
    503     cases daemon (* XXX: segmentation fault *)
    504   |1,2,3,4,5,7,8,9,10,11,12,13,18,19,24,26,27,29,35,36,42,43,48,49,54,55,60,61,
    505    62,63,64,66,67,68,70,72,74,76:
    506     @breakup_pair' cases (next pmem pc ?)
    507     normalize * normalize #pc' #byte @lt_to_le
    508   [30:
    509     generalize in match pc in EQ; #pc' #EQ' -pc
    510     cut(nat_of_bitvector … pc < nat_of_bitvector … pc')
    511     [1:
    512       cut(pc' = \fst (next pmem pc (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
    513          code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)))
    514       [1:
    515         //
    516       |2:
    517         #assm >assm @sig2
    518       ]
    519     | #lt_assm
    520       lapply(transitive_le
    521         (S (nat_of_bitvector … pc))
    522         (nat_of_bitvector … pc')
    523         (S (nat_of_bitvector … pc')) lt_assm ?)
    524       [1:
    525         //
    526       |2:
    527         #le_assm
    528         lapply(transitive_le
    529           (S (nat_of_bitvector … pc))
    530           (S (nat_of_bitvector … pc'))
    531           (code_memory_size - 1) le_assm ?)
    532         [2:
    533           //
    534         |1:
    535           @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
    536             (nat_of_bitvector … pc) code_memory_size 24 1 ? ?)
    537           [1:
    538             @le_S_S @le_S_S @le_O_n
    539           |2:
    540             assumption
    541           ]
    542         ]
    543       ]
    544     ] XXX: blah! *)
     417  %
    545418qed.
    546419
    547 definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.
    548     Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
     420definition fetch: ∀code_memory: BitVectorTrie Byte 16.
     421    ∀program_counter: Word. instruction × Word × nat ≝
    549422  λpmem: BitVectorTrie Byte 16.
    550423  λpc: Word.
    551   let 〈word, byte〉 ≝ next pmem pc ? in
    552     fetch0 pmem word byte ?.
    553   cases daemon (* XXX: todo, proofs about size of pc *)
    554 qed.
     424  let 〈word, byte〉 ≝ next pmem pc in
     425    fetch0 pmem word byte.
     426
     427let rec fetch_program_counter_n
     428  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
     429    on n: Word ≝
     430  match n with
     431  [ O ⇒ program_counter
     432  | S n ⇒
     433    let tail_pc ≝ fetch_program_counter_n n code_memory program_counter in
     434    let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
     435      program_counter
     436  ].
Note: See TracChangeset for help on using the changeset viewer.