Changeset 1588 for src/ASM/Status.ma


Ignore:
Timestamp:
Dec 6, 2011, 11:21:37 AM (8 years ago)
Author:
sacerdot
Message:

All goals generated by Russell for execute_1* are now closed, mostly by
automation. Since automation does not work on equational goals that contain
equations, I was forced to change every (?) Russel definition into triples:
fun' with Sigma type as a type; fun as @eject of fun'; fun_ok as @sig2 of fun'.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1581 r1588  
    762762qed.
    763763
    764 definition set_arg_16: ∀M: Type[0]. PreStatus M → Word → [[ dptr ]] → PreStatus M
     764definition set_arg_16': ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → Σs':PreStatus M. clock … s = clock … s'
    765765  λM.
    766766  λs.
    767767  λv.
    768768  λa.
    769    match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
     769   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M s = clock M s' with
    770770     [ DPTR ⇒ λ_:True.
    771771       let 〈 bu, bl 〉 ≝ split … 8 8 v in
     
    778778       ]
    779779     ] (subaddressing_modein … a).
     780 //
     781qed.
     782
     783definition set_arg_16: ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → PreStatus M ≝
     784 set_arg_16'.
     785
     786lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x).
     787 #M #s #x #v whd in match set_arg_16; normalize nodelta @sig2
     788qed.
     789
    780790   
    781791definition get_arg_16: ∀M: Type[0]. PreStatus M → [[ data16 ]] → Word ≝
     
    856866axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clock m s = clock … (set_bit_addressable_sfr … s d v).
    857867
    858 definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ;
     868definition set_arg_8': ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ;
    859869                                   acc_a ; acc_b ; ext_indirect ;
    860870                                   ext_indirect_dptr ]] → Byte → Σs':PreStatus M.
     
    911921      ] (subaddressing_modein … a).
    912922// qed.
     923
     924definition set_arg_8: ∀M: Type[0]. ∀s:PreStatus M. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M ≝
     925 set_arg_8'.
     926
     927lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v).
     928 #M #s #x #v whd in match set_arg_8; normalize nodelta @sig2
     929qed.
    913930
    914931theorem modulus_less_than:
     
    10201037qed.
    10211038     
    1022 (* XXX: Russell typing: Σs': PreStatus M. clock … s = clock M s', causes dangling de Bruijn
    1023         pointer assertion failure in nCicMetaSubst.ml, line 293.  *)
    1024 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝
     1039definition set_arg_1': ∀M: Type[0]. ∀s:PreStatus M. [[bit_addr; carry]] → Bit → Σs':PreStatus M. clock … s = clock … s' ≝
    10251040  λm: Type[0].
    10261041  λs: PreStatus m.
    10271042  λa: [[bit_addr; carry]].
    10281043  λv: Bit.
    1029     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
     1044    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m s = clock m s' with
    10301045      [ BIT_ADDR b ⇒ λbit_addr: True.
    10311046        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
     
    10621077            [ ]
    10631078      ] (subaddressing_modein … a).
    1064       [1,2,3,6:
    1065          normalize
    1066          repeat (@ le_S_S)
    1067          @ le_O_n
    1068       |4,5:
    1069          @ modulus_less_than
    1070       ]
     1079try (repeat @le_S_S @le_O_n)
     1080/by/
     1081qed.
     1082
     1083definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M ≝ set_arg_1'.
     1084
     1085lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v).
     1086 #M #s #x #v whd in match set_arg_1; normalize nodelta @sig2
    10711087qed.
    10721088
Note: See TracChangeset for help on using the changeset viewer.