Changeset 1526


Ignore:
Timestamp:
Nov 22, 2011, 10:43:47 AM (8 years ago)
Author:
sacerdot
Message:

Using Russell to prove some properties.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1522 r1526  
    11include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
     3include "ASM/JMCoercions.ma".
    34
    45definition sign_extension: Byte → Word ≝
     
    119120include alias "ASM/BitVectorTrie.ma".
    120121
     122
     123lemma set_flags_ignores_clock:
     124 ∀M,s,f1,f2,f3. clock M s ≤ clock … (set_flags … s f1 f2 f3).
     125//
     126qed.
     127
     128lemma set_args_8_ignores_clock:
     129 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
     130#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
     131#a #E >E //
     132qed.
     133
    121134definition execute_1_preinstruction:
    122135 ∀ticks: nat × nat.
    123  ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
     136 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
     137  ∀s:PreStatus M. Σs':PreStatus M. clock … s ≤ clock … s' ≝
    124138  λticks.
    125139  λA, M: Type[0].
     
    210224            ]
    211225        | INC addr ⇒
    212             let s ≝ add_ticks1 s in
     226            let s' ≝ add_ticks1 s in
    213227            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    214228                                                           registr;
    215229                                                           direct;
    216230                                                           indirect;
    217                                                            dptr ]] x) → ? with
     231                                                           dptr ]] x) → Σs'.clock … s ≤ clock … s' with
    218232              [ ACC_A ⇒ λacc_a: True.
    219                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
    220                   set_arg_8 ? s ACC_A result
     233                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
     234                 eject … (set_arg_8 ? s' ACC_A result)
    221235              | REGISTER r ⇒ λregister: True.
    222                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
    223                   set_arg_8 ? s (REGISTER r) result
     236                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     237                 eject … (set_arg_8 ? s' (REGISTER r) result)
    224238              | DIRECT d ⇒ λdirect: True.
    225                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
    226                   set_arg_8 ? s (DIRECT d) result
     239                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     240                 eject … (set_arg_8 ? s' (DIRECT d) result)
    227241              | INDIRECT i ⇒ λindirect: True.
    228                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
    229                   set_arg_8 ? s (INDIRECT i) result
     242                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     243                 eject … (set_arg_8 ? s' (INDIRECT i) result)
    230244              | DPTR ⇒ λdptr: True.
    231                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
    232                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
    233                 let s ≝ set_8051_sfr ? s SFR_DPL bl in
    234                   set_8051_sfr ? s SFR_DPH bu
     245                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in
     246                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in
     247                let s ≝ set_8051_sfr ? s' SFR_DPL bl in
     248                  set_8051_sfr ? s' SFR_DPH bu
    235249              | _ ⇒ λother: False. ⊥
    236250              ] (subaddressing_modein … addr)
     
    519533           let s ≝ add_ticks2 s in
    520534            s
    521         ].
    522     try assumption
    523     try @I
     535        ]. (*67s*)
     536    try assumption (*180s*)
     537    try % (*41s*)
    524538    try (
    525539      @ (execute_1_technical … (subaddressing_modein …))
    526540      @ I
    527     )
     541    ) (*132s*)
     542 [(*1:/by/,2,3: /by/*)
     543 |4:
     544 |6,7,8,10,11,12,13,14,15: /by/ (*56s*)
     545 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*73s*)
     546 |33,35,39,41,43,54,55,56: /by/ (*48s*)
     547 |
     548 (* 31,32,34,36,44,48 facili *)
     549 (* 4,5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
    528550qed.
    529551
  • src/ASM/Status.ma

    r1522 r1526  
    66include "ASM/Arithmetic.ma".
    77include "ASM/BitVectorTrie.ma".
     8include "ASM/JMCoercions.ma".
    89
    910definition Time ≝ nat.
     
    853854qed.
    854855
    855 definition set_arg_8: ∀M: Type[0]. PreStatus M → [[ direct ; indirect ; registr ;
     856axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v).
     857
     858definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ;
    856859                                   acc_a ; acc_b ; ext_indirect ;
    857                                    ext_indirect_dptr ]] → Byte → PreStatus M ≝
     860                                   ext_indirect_dptr ]] → Byte → Σs':PreStatus M.
     861                                   clock … s = clock … s' ≝
    858862  λm, s, a, v.
    859863    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    860864                                                acc_a ; acc_b ; ext_indirect ;
    861                                                 ext_indirect_dptr ]] x) → ? with
     865                                                ext_indirect_dptr ]] x) →
     866                   Σs':PreStatus m. ?(*clock … s*) = ?(*clock … s'*)
     867                   (*CSC: bug here if one specified the two clock above*)
     868            with
    862869      [ DIRECT d ⇒
    863870        λdirect: True.
     
    899906          let memory ≝ insert ? 16 address v (external_ram ? s) in
    900907            set_external_ram ? s memory
    901       | _ ⇒
     908      | _ ⇒ 
    902909        λother: False.
    903910          match other in False with [ ]
    904911      ] (subaddressing_modein … a).
    905   [1,2,3,4:
    906      normalize
    907      repeat (@ le_S_S)
    908      @ le_O_n
    909   ]
    910 qed.
     912// qed.
    911913
    912914theorem modulus_less_than:
     
    10241026      [ BIT_ADDR b ⇒ λbit_addr: True.
    10251027          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1026           let bit_1 ≝ get_index_v nu 0 ? in
     1028          let bit_1 ≝ get_index_v ?? nu 0 ? in
    10271029          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    10281030          match bit_1 with
Note: See TracChangeset for help on using the changeset viewer.