Changeset 2160 for src/ASM/Status.ma


Ignore:
Timestamp:
Jul 6, 2012, 5:26:21 PM (8 years ago)
Author:
mulligan
Message:

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2139 r2160  
    617617qed.
    618618
    619 definition set_bit_addressable_sfr ≝
     619definition set_bit_addressable_sfr':
     620    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
     621      Σs':PreStatus M code_memory.
     622        clock … code_memory s = clock … code_memory s' ∧
     623        program_counter … code_memory s = program_counter … code_memory s' ≝
    620624  λM: Type[0].
    621625  λcode_memory:M.
     
    625629    let address ≝ nat_of_bitvector … b in
    626630      if (eqb address 128) then
    627         ?
     631        match not_implemented in False with [ ]
    628632      else if (eqb address 144) then
    629633        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     
    631635          status_2
    632636      else if (eqb address 160) then
    633         ?
     637        match not_implemented in False with [ ]
    634638      else if (eqb address 176) then
    635639        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     
    681685        set_8051_sfr ?? s SFR_ACC_B v
    682686      else
    683         ?.
    684       cases not_implemented
     687        match not_implemented in False with [ ].
     688  /2 by refl, pair_destruct/
     689qed.
     690
     691definition set_bit_addressable_sfr:
     692    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
     693      PreStatus M code_memory ≝ set_bit_addressable_sfr'.
     694
     695lemma clock_set_bit_addressable_sfr:
     696    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
     697        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
     698  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
     699  cases (set_bit_addressable_sfr' ?????) #s' * //
     700qed.
     701
     702lemma program_counter_set_bit_addressable_sfr:
     703    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
     704        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
     705  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
     706  cases (set_bit_addressable_sfr' ?????) #s' * //
    685707qed.
    686708
     
    880902qed.
    881903
    882 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
    883 
    884 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
     904definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    885905                                   acc_a ; acc_b ; ext_indirect ;
    886                                    ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
    887                                    clock … code_memory s = clock … code_memory s' ≝
     906                                   ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory.
     907                                   clock … code_memory s = clock … code_memory s' ∧
     908                                   (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧
     909                                   (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧
     910                                   program_counter … code_memory s = program_counter … code_memory s' ∧
     911                                   (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝
    888912  λm, cm, s, a, v.
    889913    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    890914                                                acc_a ; acc_b ; ext_indirect ;
    891915                                                ext_indirect_dptr ]] x) →
    892                    Σs':PreStatus m cm. clock m cm s = clock m cm s'
     916                   Σs':PreStatus m cm. ?
    893917                   (*CSC: bug here if one specified the two clock above*)
    894918            with
     
    936960          match other in False with [ ]
    937961      ] (subaddressing_modein … a).
    938 // qed.
     962  /6 by conj, False_ind/
     963qed.
    939964
    940965definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝
    941966 set_arg_8'.
    942967
    943 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
    944  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
     968lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
     969 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     970 cases (set_arg_8' ?????) #s' * * * * //
     971qed.
     972
     973lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v).
     974 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     975 cases (set_arg_8' ?????) #s' * * * * //
     976qed.
     977
     978lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v).
     979  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     980  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     981  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     982  * * * * #_ #relevant #_ #_ #_ @relevant @I
     983qed.
     984
     985lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v).
     986  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     987  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     988  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     989  * * * * #_ #_ #relevant #_ #_ @relevant @I
     990qed.
     991
     992lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v).
     993  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     994  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     995  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     996  * * * * #_ #_ #_ #_ #relevant @relevant @I
    945997qed.
    946998
Note: See TracChangeset for help on using the changeset viewer.