Ignore:
Timestamp:
Jul 2, 2012, 11:37:34 AM (8 years ago)
Author:
mulligan
Message:

Changes to the subaddressing mode elim functions moved into their correct place in ASM.ma. ticks_of0 completed, with all daemons removed. Another commutation lemma added in AssemblyProofSplit?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2142 r2143  
    340340qed.
    341341
     342lemma m_lt_1_to_m_refl_0:
     343  ∀m: nat.
     344    m < 1 → m = 0.
     345  #m cases m try (#irrelevant %)
     346  #m' whd in ⊢ (% → ?); #relevant
     347  lapply (le_S_S_to_le … relevant)
     348  change with (? < ? → ?) -relevant #relevant
     349  cases (lt_to_not_zero … relevant)
     350qed.
     351
    342352(*CSC: move elsewhere*)         
    343353axiom lt_to_lt_nat_of_bitvector_add:
    344  ∀n,v,m1,m2.
    345   m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
    346    nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
    347    nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     354  ∀n,v,m1,m2.
     355    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
     356      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
     357      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
    348358
    349359(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
     
    645655      (external_ram … ps)
    646656      pc
    647       (special_function_registers_8051 … ps)
     657      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
    648658      (special_function_registers_8052 … ps)
    649659      (p1_latch … ps)
     
    764774*)
    765775
     776(* XXX: check values returned for conditional jumps below! *)
    766777definition ticks_of0:
    767778    ∀p:pseudo_assembly_program.
     
    775786    [ Instruction instr ⇒
    776787      match instr with
    777       [ JC lbl ⇒ ? (*
    778         match pol lookup_labels ppc with
    779         [ short_jump ⇒ 〈2, 2〉
    780         | absolute_jump ⇒ ?
    781         | long_jump ⇒ 〈4, 4〉
    782         ] *)
    783       | JNC lbl ⇒ ? (*
    784         match pol lookup_labels ppc with
    785         [ short_jump ⇒ 〈2, 2〉
    786         | absolute_jump ⇒ ?
    787         | long_jump ⇒ 〈4, 4〉
    788         ] *)
    789       | JB bit lbl ⇒ ? (*
    790         match pol lookup_labels ppc with
    791         [ short_jump ⇒ 〈2, 2〉
    792         | absolute_jump ⇒ ?
    793         | long_jump ⇒ 〈4, 4〉
    794         ] *)
    795       | JNB bit lbl ⇒ ? (*
    796         match pol lookup_labels ppc with
    797         [ short_jump ⇒ 〈2, 2〉
    798         | absolute_jump ⇒ ?
    799         | long_jump ⇒ 〈4, 4〉
    800         ] *)
    801       | JBC bit lbl ⇒ ? (*
    802         match pol lookup_labels ppc with
    803         [ short_jump ⇒ 〈2, 2〉
    804         | absolute_jump ⇒ ?
    805         | long_jump ⇒ 〈4, 4〉
    806         ] *)
    807       | JZ lbl ⇒ ? (*
    808         match pol lookup_labels ppc with
    809         [ short_jump ⇒ 〈2, 2〉
    810         | absolute_jump ⇒ ?
    811         | long_jump ⇒ 〈4, 4〉
    812         ] *)
    813       | JNZ lbl ⇒ ? (*
    814         match pol lookup_labels  ppc with
    815         [ short_jump ⇒ 〈2, 2〉
    816         | absolute_jump ⇒ ?
    817         | long_jump ⇒ 〈4, 4〉
    818         ] *)
    819       | CJNE arg lbl ⇒ ? (*
    820         match pol lookup_labels ppc with
    821         [ short_jump ⇒ 〈2, 2〉
    822         | absolute_jump ⇒ ?
    823         | long_jump ⇒ 〈4, 4〉
    824         ] *)
    825       | DJNZ arg lbl ⇒ ? (*
    826         match pol lookup_labels ppc with
    827         [ short_jump ⇒ 〈2, 2〉
    828         | absolute_jump ⇒ ?
    829         | long_jump ⇒ 〈4, 4〉
    830         ] *)
     788      [ JC lbl ⇒
     789        if policy ppc then
     790          〈4, 4〉
     791        else
     792          〈2, 2〉
     793      | JNC lbl ⇒
     794        if policy ppc then
     795          〈4, 4〉
     796        else
     797          〈2, 2〉
     798      | JB bit lbl ⇒
     799        if policy ppc then
     800          〈4, 4〉
     801        else
     802          〈2, 2〉
     803      | JNB bit lbl ⇒
     804        if policy ppc then
     805          〈4, 4〉
     806        else
     807          〈2, 2〉
     808      | JBC bit lbl ⇒
     809        if policy ppc then
     810          〈4, 4〉
     811        else
     812          〈2, 2〉
     813      | JZ lbl ⇒
     814        if policy ppc then
     815          〈4, 4〉
     816        else
     817          〈2, 2〉
     818      | JNZ lbl ⇒
     819        if policy ppc then
     820          〈4, 4〉
     821        else
     822          〈2, 2〉
     823      | CJNE arg lbl ⇒
     824        if policy ppc then
     825          〈4, 4〉
     826        else
     827          〈2, 2〉
     828      | DJNZ arg lbl ⇒
     829        if policy ppc then
     830          〈4, 4〉
     831        else
     832          〈2, 2〉
    831833      | ADD arg1 arg2 ⇒
    832834        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     
    916918    | Comment comment ⇒ 〈0, 0〉
    917919    | Cost cost ⇒ 〈0, 0〉
    918     | Jmp jmp ⇒ 〈2, 2〉
    919     | Call call ⇒ 〈2, 2〉
     920    | Jmp jmp ⇒
     921      if policy ppc then
     922        〈4, 4〉
     923      else
     924        〈2, 2〉
     925    | Call call ⇒
     926      if policy ppc then
     927        〈4, 4〉
     928      else
     929        〈2, 2〉
    920930    | Mov dptr tgt ⇒ 〈2, 2〉
    921931    ].
    922     cases daemon
    923 qed.
    924932
    925933definition ticks_of:
Note: See TracChangeset for help on using the changeset viewer.