Changeset 1533 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 22, 2011, 7:24:00 PM (9 years ago)
Author:
sacerdot
Message:

Proof of execute_1 with Russell completed (up to some daemon used before).

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1527 r1533  
    555555qed.
    556556
     557(*CSC: indexing diverges, why?*)
     558example set_program_counter_ignores_clock:
     559  ∀M.∀s: PreStatus M.
     560  ∀pc: Word.
     561    clock … (set_program_counter … s pc) = clock … s.
     562 //
     563qed.
     564
     565lemma set_8051_sfr_ignores_clock:
     566  ∀M.∀s: PreStatus M.
     567  ∀sfr: SFR8051.
     568  ∀v: Byte.
     569    clock … (set_8051_sfr ? s sfr v) = clock … s.
     570  //
     571qed.
     572
     573lemma write_at_stack_pointer_ignores_clock:
     574  ∀M.∀s: PreStatus M.
     575  ∀sp: Byte.
     576    clock … (write_at_stack_pointer … s sp) = clock … s.
     577  #M #s #sp
     578  change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
     579   in match (write_at_stack_pointer ???);
     580  normalize nodelta
     581  cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
     582  #nu #nl normalize nodelta;
     583  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
     584  [ normalize nodelta; %
     585  | normalize nodelta; %
     586  ]
     587qed.
     588
    557589definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
    558590  λs0,instr_pc_ticks.
    … …  
    567599        | _ ⇒ λabsd. ⊥
    568600        ] (subaddressing_modein … x)) instr s
    569      | ACALL addr ⇒ ?(*
     601     | ACALL addr ⇒
    570602          let s ≝ set_clock ? s (ticks + clock ? s) in
    571           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     603          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    572604            [ ADDR11 a ⇒ λaddr11: True.
    573605              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    574606              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    575               let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
    576               let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
     607              let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    577608              let s ≝ write_at_stack_pointer ? s pc_bl in
    578609              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    579610              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    580611              let s ≝ write_at_stack_pointer ? s pc_bu in
    581               let thr ≝ \fst (split ? 3 8 a) in
    582               let eig ≝ \snd (split ? 3 8 a) in
    583               let fiv ≝ \fst (split ? 5 3 pc_bu) in
    584               let thr' ≝ \snd (split ? 5 3 pc_bu) in
     612              let 〈thr,eig〉 ≝ split ? 3 8 a in
     613              let 〈fiv,thr'〉 ≝ split ? 5 3 pc_bu in
    585614              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    586615                set_program_counter ? s new_addr
    587616            | _ ⇒ λother: False. ⊥
    588             ] (subaddressing_modein … addr)*)
     617            ] (subaddressing_modein … addr)
    589618        | LCALL addr ⇒
    590619          let s ≝ set_clock ? s (ticks + clock ? s) in
    591           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     620          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    592621            [ ADDR16 a ⇒ λaddr16: True.
    593622              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    594623              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    595               let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
    596               let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
     624              let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    597625              let s ≝ write_at_stack_pointer ? s pc_bl in
    598626              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    … …  
    604632        | MOVC addr1 addr2 ⇒
    605633          let s ≝ set_clock ? s (ticks + clock ? s) in
    606           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     634          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    607635            [ ACC_DPTR ⇒ λacc_dptr: True.
    608636              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    … …  
    631659        | LJMP addr ⇒
    632660          let s ≝ set_clock ? s (ticks + clock ? s) in
    633           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     661          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    634662            [ ADDR16 a ⇒ λaddr16: True.
    635663                set_program_counter ? s a
    … …  
    638666        | SJMP addr ⇒
    639667          let s ≝ set_clock ? s (ticks + clock ? s) in
    640           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     668          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    641669            [ RELATIVE r ⇒ λrelative: True.
    642670                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
    … …  
    646674        | AJMP addr ⇒
    647675          let s ≝ set_clock ? s (ticks + clock ? s) in
    648           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     676          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with
    649677            [ ADDR11 a ⇒ λaddr11: True.
    650               let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
    651               let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
    652               let nu ≝ \fst (split ? 4 4 pc_bu) in
    653               let nl ≝ \snd (split ? 4 4 pc_bu) in
     678              let 〈pc_bu,pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     679              let 〈nu,nl〉 ≝ split ? 4 4 pc_bu in
    654680              let bit ≝ get_index' ? O ? nl in
    655               let relevant1 ≝ \fst (split ? 3 8 a) in
    656               let relevant2 ≝ \snd (split ? 3 8 a) in
     681              let 〈relevant1,relevant2〉 ≝ split ? 3 8 a in
    657682              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    658683              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
    … …  
    660685            | _ ⇒ λother: False. ⊥
    661686            ] (subaddressing_modein … addr)
    662       ].
    663     try assumption
    664     try (
    665       normalize
    666       repeat (@ (le_S_S))
    667       @ (le_O_n)
    668     )
    669     try (
    670       @ (execute_1_technical … (subaddressing_modein …))
    671       @ I
    672     )
    673     try (
    674       normalize
    675       @ I
    676     )     
    677 qed.
    678 
    679 definition execute_1: Status → Status ≝
     687      ]. (*5s*)
     688    try assumption (*12s*)
     689    [1,2: >set_program_counter_ignores_clock normalize nodelta
     690      >write_at_stack_pointer_ignores_clock
     691      >set_8051_sfr_ignores_clock
     692      >write_at_stack_pointer_ignores_clock
     693      >set_8051_sfr_ignores_clock
     694      change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
     695    |3,4,5,6: >set_program_counter_ignores_clock normalize nodelta
     696     change with (? ≤ ?+?) >set_program_counter_ignores_clock /by/
     697    |7,8: >set_8051_sfr_ignores_clock normalize nodelta change with (? ≤ ?+?)
     698      >set_program_counter_ignores_clock /by/]
     699qed.
     700
     701definition execute_1: ∀s:Status. Σs':Status. clock … s ≤ clock … s' ≝
    680702  λs: Status.
    681703    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
Note: See TracChangeset for help on using the changeset viewer.