Changeset 1526 for src/ASM/Status.ma


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

Using Russell to prove some properties.

File:
1 edited

Legend:

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