Changeset 1534 for src/ASM


Ignore:
Timestamp:
Nov 23, 2011, 10:36:34 AM (9 years ago)
Author:
mulligan
Message:

committing my changes to interpret to prevent any further conflicts

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/CostsProof.ma

    r1522 r1534  
    99  | LJMP _ ⇒ True
    1010  | SJMP _ ⇒ True
    11   | JMP _ ⇒ True
     11  | JMP _ ⇒ False
    1212  | RealInstruction ri ⇒
    1313    match ri with
    … …  
    3131  [ ACALL _ ⇒ True
    3232  | LCALL _ ⇒ True
     33  | JMP ⇒ True (* XXX: is function pointer call *)
    3334  | _ ⇒ False
    3435  ].

  • src/ASM/Interpret.ma

    r1533 r1534  
    122122
    123123lemma set_flags_ignores_clock:
    124  ∀M,s,f1,f2,f3. clock M s ≤ clock … (set_flags … s f1 f2 f3).
     124 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
    125125//
    126126qed.
    … …  
    132132qed.
    133133
     134example set_program_counter_ignores_clock:
     135  ∀M: Type[0].
     136  ∀s: PreStatus M.
     137  ∀pc: Word.
     138    clock M (set_program_counter … s pc) = clock … s.
     139  #M #s #pc %
     140qed.
     141
     142example set_low_internal_ram_ignores_clock:
     143  ∀M: Type[0].
     144  ∀s: PreStatus M.
     145  ∀ram: BitVectorTrie Byte 7.
     146    clock … (set_low_internal_ram … s ram) = clock … s.
     147  #M #s #ram %
     148qed.
     149
     150example set_8051_sfr_ignores_clock:
     151  ∀M: Type[0].
     152  ∀s: PreStatus M.
     153  ∀sfr: SFR8051.
     154  ∀v: Byte.
     155    clock … (set_8051_sfr ? s sfr v) = clock … s.
     156  #M #s #sfr #v %
     157qed.
     158
     159axiom set_arg_8_ignores_clock:
     160  ∀M: Type[0].
     161  ∀s: PreStatus M.
     162  ∀arg.
     163  ∀val.
     164    clock M (set_arg_8 … s arg val) = clock … s.
     165 
     166example clock_set_clock:
     167  ∀M: Type[0].
     168  ∀s: PreStatus M.
     169  ∀v.
     170    clock … (set_clock … s v) = v.
     171  #M #s #v %
     172qed.
     173
    134174lemma tech_clocks_le:
    135175 ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t.
    … …  
    140180 ∀ticks: nat × nat.
    141181 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
    142   ∀s:PreStatus M. Σs':PreStatus M. clock … s ≤ clock … s' ≝
     182 ∀s:PreStatus M. Σs': PreStatus M. clock M s ≤ clock … s' ≝
    143183  λticks.
    144184  λA, M: Type[0].
    … …  
    148188  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
    149189  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    150   match instr with
     190  match instr return λx. Σs': PreStatus M. clock … s ≤ clock … s' with
    151191        [ ADD addr1 addr2 ⇒
    152192            let s ≝ add_ticks1 s in
    … …  
    222262              let 〈addr1, addr2〉 ≝ l' in
    223263              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    224                 set_arg_8 ? s addr1 xor_val
     264                eject … (set_arg_8 ? s addr1 xor_val)
    225265            | inr r ⇒
    226266              let 〈addr1, addr2〉 ≝ r in
    227267              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
    228                 set_arg_8 ? s addr1 xor_val
     268                eject … (set_arg_8 ? s addr1 xor_val)
    229269            ]
    230270        | INC addr ⇒
    231             let s' ≝ add_ticks1 s in
    232271            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    233272                                                           registr;
    234273                                                           direct;
    235274                                                           indirect;
    236                                                            dptr ]] x) → Σs'.clock … s ≤ clock … s' with
     275                                                           dptr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
    237276              [ ACC_A ⇒ λacc_a: True.
     277                let s' ≝ add_ticks1 s in
    238278                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
    239279                 eject … (set_arg_8 ? s' ACC_A result)
    240280              | REGISTER r ⇒ λregister: True.
     281                let s' ≝ add_ticks1 s in
    241282                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    242283                 eject … (set_arg_8 ? s' (REGISTER r) result)
    243284              | DIRECT d ⇒ λdirect: True.
     285                let s' ≝ add_ticks1 s in
    244286                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    245287                 eject … (set_arg_8 ? s' (DIRECT d) result)
    246288              | INDIRECT i ⇒ λindirect: True.
     289                let s' ≝ add_ticks1 s in
    247290                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    248291                 eject … (set_arg_8 ? s' (INDIRECT i) result)
    249292              | DPTR ⇒ λdptr: True.
     293                let s' ≝ add_ticks1 s in
    250294                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
    251295                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
    252296                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
    253                   set_8051_sfr ? s' SFR_DPH bu
     297                  eject … (set_8051_sfr ? s' SFR_DPH bu)
    254298              | _ ⇒ λother: False. ⊥
    255299              ] (subaddressing_modein … addr)
     300        | NOP ⇒
     301           let s ≝ add_ticks2 s in
     302            s
    256303        | DEC addr ⇒
    257304           let s ≝ add_ticks1 s in
    258305           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    259              set_arg_8 ? s addr result
     306             eject … (set_arg_8 ? s addr result)
    260307        | MUL addr1 addr2 ⇒
    261308           let s ≝ add_ticks1 s in
    … …  
    267314           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    268315           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
    269              set_8051_sfr ? s SFR_ACC_B high
     316             eject … (set_8051_sfr ? s SFR_ACC_B high)
    270317        | DIV addr1 addr2 ⇒
    271318           let s ≝ add_ticks1 s in
    … …  
    279326                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
    280327                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
    281                    set_flags ? s false (None Bit) false
     328                   eject … (set_flags ? s false (None Bit) false)
    282329               ]
    283330        | DA addr ⇒
    284331            let s ≝ add_ticks1 s in
    285             let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
     332            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    286333              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
    287334                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    … …  
    298345                s
    299346        | CLR addr ⇒
    300           let s ≝ add_ticks1 s in
    301           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    302             [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
    303             | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
    304             | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
     347          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
     348            [ ACC_A ⇒ λacc_a: True.
     349              let s ≝ add_ticks1 s in
     350                eject … (set_arg_8 ? s ACC_A (zero 8))
     351            | CARRY ⇒ λcarry: True.
     352              let s ≝ add_ticks1 s in
     353                eject … (set_arg_1 ? s CARRY false)
     354            | BIT_ADDR b ⇒ λbit_addr: True.
     355              let s ≝ add_ticks1 s in
     356                eject … (set_arg_1 ? s (BIT_ADDR b) false)
    305357            | _ ⇒ λother: False. ⊥
    306358            ] (subaddressing_modein … addr)
    307359        | CPL addr ⇒
    308           let s ≝ add_ticks1 s in
    309           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
     360          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
    310361            [ ACC_A ⇒ λacc_a: True.
     362                let s ≝ add_ticks1 s in
    311363                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    312364                let new_acc ≝ negation_bv ? old_acc in
    313                   set_8051_sfr ? s SFR_ACC_A new_acc
     365                  eject … (set_8051_sfr ? s SFR_ACC_A new_acc)
    314366            | CARRY ⇒ λcarry: True.
     367                let s ≝ add_ticks1 s in
    315368                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
    316369                let new_cy_flag ≝ ¬old_cy_flag in
    317                   set_arg_1 ? s CARRY new_cy_flag
     370                  eject … (set_arg_1 ? s CARRY new_cy_flag)
    318371            | BIT_ADDR b ⇒ λbit_addr: True.
     372                let s ≝ add_ticks1 s in
    319373                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
    320374                let new_bit ≝ ¬old_bit in
    321                   set_arg_1 ? s (BIT_ADDR b) new_bit
     375                  eject … (set_arg_1 ? s (BIT_ADDR b) new_bit)
    322376            | _ ⇒ λother: False. ?
    323377            ] (subaddressing_modein … addr)
    … …  
    358412              set_8051_sfr ? s SFR_ACC_A new_acc
    359413        | PUSH addr ⇒
    360             let s ≝ add_ticks1 s in
    361             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
     414            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with
    362415              [ DIRECT d ⇒ λdirect: True.
     416                let s ≝ add_ticks1 s in
    363417                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    364418                let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    … …  
    386440            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    387441              set_arg_8 ? s addr2 new_arg
     442        | _ ⇒ ?
     443        ].
    388444        | RET ⇒
    389445            let s ≝ add_ticks1 s in
    … …  
    412468            [ inl l ⇒
    413469              let 〈addr1, addr2〉 ≝ l in
    414                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     470                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    415471            | inr r ⇒
    416472              let 〈addr1, addr2〉 ≝ r in
    417                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     473                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    418474            ]
    419475        | MOV addr ⇒
    … …  
    430486                            [ inl l'''' ⇒
    431487                              let 〈addr1, addr2〉 ≝ l'''' in
    432                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     488                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    433489                            | inr r'''' ⇒
    434490                              let 〈addr1, addr2〉 ≝ r'''' in
    435                                 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     491                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    436492                            ]
    437493                        | inr r''' ⇒
    438494                          let 〈addr1, addr2〉 ≝ r''' in
    439                             set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
     495                            eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
    440496                        ]
    441497                    | inr r'' ⇒
    442498                      let 〈addr1, addr2〉 ≝ r'' in
    443                         set_arg_16 ? s (get_arg_16 ? s addr2) addr1
     499                        eject … (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
    444500                    ]
    445501                | inr r ⇒
    446502                  let 〈addr1, addr2〉 ≝ r in
    447                     set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     503                    eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
    448504                ]
    449505            | inr r ⇒
    450506              let 〈addr1, addr2〉 ≝ r in
    451                 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
     507                eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
    452508            ]
    453509          | JC addr ⇒
    454510                  if get_cy_flag ? s then
    455                    let s ≝ add_ticks1 s in
    456                     set_program_counter ? s (addr_of addr s)
     511                    let s ≝ add_ticks1 s in
     512                      set_program_counter ? s (addr_of addr s)
    457513                  else
    458                    let s ≝ add_ticks2 s in
    459                     s
     514                    let s ≝ add_ticks2 s in
     515                      s
    460516            | JNC addr ⇒
    461517                  if ¬(get_cy_flag ? s) then
    462518                   let s ≝ add_ticks1 s in
    463                     set_program_counter ? s (addr_of addr s)
     519                     eject … (set_program_counter ? s (addr_of addr s))
    464520                  else
    465521                   let s ≝ add_ticks2 s in
    … …  
    510566                            let s ≝ add_ticks1 s in
    511567                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    512                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     568                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    513569                          else
    514570                            let s ≝ add_ticks2 s in
    515                             (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     571                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    516572                    | inr r' ⇒
    517573                        let 〈addr1, addr2'〉 ≝ r' in
    … …  
    521577                            let s ≝ add_ticks1 s in
    522578                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    523                               set_flags ? s new_cy (None ?) (get_ov_flag ? s)
     579                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    524580                          else
    525581                            let s ≝ add_ticks2 s in
    526                             (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
     582                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    527583                    ]
    528584            | DJNZ addr1 addr2 ⇒
    … …  
    535591                 let s ≝ add_ticks2 s in
    536592                  s
    537         | NOP ⇒
    538            let s ≝ add_ticks2 s in
    539             s
    540593        ]. (*14s*)
    541     try assumption (*20s*)
     594(*    try assumption (*20s*)
    542595    try % (*6s*)
    543596    try (
    544597      @ (execute_1_technical … (subaddressing_modein …))
    545598      @ I
    546     ) (*34s*)
    547  [1,2,3: /by/ (*41s*)
     599    ) (*34s*) *)
     600 [9: normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
     601     >clock_set_clock //
     602 |32,34: cases l #either normalize nodelta cases either
     603      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
     604      >clock_set_clock //
     605 |36,48: cases addr #either normalize nodelta cases either
     606      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
     607      >clock_set_clock // (* XXX: change addr to l *)
     608 |44: cases l2 #either normalize nodelta
     609      [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
     610          >clock_set_clock //
     611      |1: cases either #addr cases addr #addr1 #addr2 normalize nodelta
     612          >set_arg_8_ignores_clock >clock_set_clock //
     613      ] (* XXX: change l2 to l *)
     614 |5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false)
     615     #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
     616 |37: cases addr
     617 |20,21,30,31: (* XXX: segfault here *)
     618 |1,2,3: /by/ (*41s*)
    548619 |4,6,7,8,10,11,12,13,14,15: /by/ (*6s*)
    549620 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*)
    550621 |33,35,39,41,43,54,55,56: /by/ (*6s*)
    551  |57: <set_args_8_ignores_clock /by/ (*0.5s ??*)
    552  (* 31,32,34,36,44,48 facili *)
     622 |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
    553623 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
    554624 |*:cases daemon]
    … …  
    603673          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    604674            [ ADDR11 a ⇒ λaddr11: True.
    605               let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
     675              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    606676              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    607               let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     677              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    608678              let s ≝ write_at_stack_pointer ? s pc_bl in
    609               let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
     679              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    610680              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    611681              let s ≝ write_at_stack_pointer ? s pc_bu in
    612               let 〈thr,eig〉 ≝ split ? 3 8 a in
    613               let 〈fiv,thr'〉 ≝ split ? 5 3 pc_bu in
     682              let 〈thr, eig〉 ≝ split ? 3 8 a in
     683              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    614684              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    615685                set_program_counter ? s new_addr
    … …  
    620690          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    621691            [ ADDR16 a ⇒ λaddr16: True.
    622               let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
     692              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    623693              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    624               let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     694              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    625695              let s ≝ write_at_stack_pointer ? s pc_bl in
    626               let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
     696              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    627697              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    628698              let s ≝ write_at_stack_pointer ? s pc_bu in
    … …  
    636706              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    637707              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    638               let new_addr ≝ \snd (half_add ? dptr big_acc) in
     708              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    639709              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    640710                set_8051_sfr ? s SFR_ACC_A result
    641711            | ACC_PC ⇒ λacc_pc: True.
    642712              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    643               let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
     713              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
    644714              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    645715              (*      addition of the PC with the DPTR? At the moment, no.              *)
    646716              let s ≝ set_program_counter ? s inc_pc in
    647               let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
     717              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    648718              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
    649719                set_8051_sfr ? s SFR_ACC_A result
    … …  
    654724          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    655725          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    656           let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
    657           let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
     726          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
     727          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
    658728            set_program_counter ? s new_pc
    659729        | LJMP addr ⇒
    … …  
    668738          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    669739            [ RELATIVE r ⇒ λrelative: True.
    670                 let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
     740                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    671741                  set_program_counter ? s new_pc
    672742            | _ ⇒ λother: False. ⊥
    … …  
    676746          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    677747            [ ADDR11 a ⇒ λaddr11: True.
    678               let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    679               let 〈nu,nl〉 ≝ split ? 4 4 pc_bu in
     748              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     749              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    680750              let bit ≝ get_index' ? O ? nl in
    681               let 〈relevant1,relevant2〉 ≝ split ? 3 8 a in
     751              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    682752              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    683               let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
     753              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
    684754                set_program_counter ? s new_pc
    685755            | _ ⇒ λother: False. ⊥
    686756            ] (subaddressing_modein … addr)
     757      ].
     758    try assumption
     759    try (
     760      normalize
     761      repeat (@ (le_S_S))
     762      @ (le_O_n)
     763    )
     764    try (
     765      @ (execute_1_technical … (subaddressing_modein …))
     766      @ I
     767    )
     768    try (
     769      normalize
     770      @ I
     771    )
    687772      ]. (*5s*)
    688773    try assumption (*12s*)
Note: See TracChangeset for help on using the changeset viewer.