Changeset 1953


Ignore:
Timestamp:
May 16, 2012, 10:29:22 AM (7 years ago)
Author:
mulligan
Message:

Commit to avoid conflicts.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1952 r1953  
    18501850  λpolicy.
    18511851  λppc: Word.
    1852   λfetched. ?.
    1853 cases daemon(*
     1852  λfetched.
    18541853    match fetched with
    18551854    [ Instruction instr ⇒
    18561855      match instr with
    1857       [ JC lbl ⇒
     1856      [ JC lbl ⇒ ? (*
    18581857        match pol lookup_labels ppc with
    18591858        [ short_jump ⇒ 〈2, 2〉
    18601859        | medium_jump ⇒ ?
    18611860        | long_jump ⇒ 〈4, 4〉
    1862         ]
    1863       | JNC lbl ⇒
     1861        ] *)
     1862      | JNC lbl ⇒ ? (*
    18641863        match pol lookup_labels ppc with
    18651864        [ short_jump ⇒ 〈2, 2〉
    18661865        | medium_jump ⇒ ?
    18671866        | long_jump ⇒ 〈4, 4〉
    1868         ]
    1869       | JB bit lbl ⇒
     1867        ] *)
     1868      | JB bit lbl ⇒ ? (*
    18701869        match pol lookup_labels ppc with
    18711870        [ short_jump ⇒ 〈2, 2〉
    18721871        | medium_jump ⇒ ?
    18731872        | long_jump ⇒ 〈4, 4〉
    1874         ]
    1875       | JNB bit lbl ⇒
     1873        ] *)
     1874      | JNB bit lbl ⇒ ? (*
    18761875        match pol lookup_labels ppc with
    18771876        [ short_jump ⇒ 〈2, 2〉
    18781877        | medium_jump ⇒ ?
    18791878        | long_jump ⇒ 〈4, 4〉
    1880         ]
    1881       | JBC bit lbl ⇒
     1879        ] *)
     1880      | JBC bit lbl ⇒ ? (*
    18821881        match pol lookup_labels ppc with
    18831882        [ short_jump ⇒ 〈2, 2〉
    18841883        | medium_jump ⇒ ?
    18851884        | long_jump ⇒ 〈4, 4〉
    1886         ]
    1887       | JZ lbl ⇒
     1885        ] *)
     1886      | JZ lbl ⇒ ? (*
    18881887        match pol lookup_labels ppc with
    18891888        [ short_jump ⇒ 〈2, 2〉
    18901889        | medium_jump ⇒ ?
    18911890        | long_jump ⇒ 〈4, 4〉
    1892         ]
    1893       | JNZ lbl ⇒
     1891        ] *)
     1892      | JNZ lbl ⇒ ? (*
    18941893        match pol lookup_labels  ppc with
    18951894        [ short_jump ⇒ 〈2, 2〉
    18961895        | medium_jump ⇒ ?
    18971896        | long_jump ⇒ 〈4, 4〉
    1898         ]
    1899       | CJNE arg lbl ⇒
     1897        ] *)
     1898      | CJNE arg lbl ⇒ ? (*
    19001899        match pol lookup_labels ppc with
    19011900        [ short_jump ⇒ 〈2, 2〉
    19021901        | medium_jump ⇒ ?
    19031902        | long_jump ⇒ 〈4, 4〉
    1904         ]
    1905       | DJNZ arg lbl ⇒
     1903        ] *)
     1904      | DJNZ arg lbl ⇒ ? (*
    19061905        match pol lookup_labels ppc with
    19071906        [ short_jump ⇒ 〈2, 2〉
    19081907        | medium_jump ⇒ ?
    19091908        | long_jump ⇒ 〈4, 4〉
    1910         ]
     1909        ] *)
    19111910      | ADD arg1 arg2 ⇒
    19121911        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     
    20001999    | Mov dptr tgt ⇒ 〈2, 2〉
    20012000    ].
    2002   cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
    2003 *)qed.
     2001    cases daemon
     2002qed.
    20042003
    20052004definition ticks_of:
     
    20322031      v = v' ∧ q = q'.
    20332032
    2034 axiom split_vector_singleton:
     2033lemma split_vector_singleton:
    20352034  ∀A: Type[0].
    20362035  ∀n: nat.
     
    20382037  ∀rest: Vector A n.
    20392038  ∀s: Vector A 1.
    2040   ∀prf.
    20412039    v = s @@ rest →
    2042     ((get_index_v A ? v 0 prf) ::: rest) = v.
     2040    ((get_index_v A ? v 0 ?) ::: rest) = v.
     2041  [1:
     2042    #A #n #v cases daemon (* XXX: !!! *)
     2043  |2:
     2044    @le_S_S @le_O_n
     2045  ]
     2046qed.
    20432047
    20442048example sub_minus_one_seven_eight:
     
    21212125
    21222126axiom low_internal_ram_write_at_stack_pointer:
    2123  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2127 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
     2128 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    21242129  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21252130  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
    21262131  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
    21272132  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    2128   bu@@bl = \fst (sigma (pbu@@pbl)) →
     2133  bu@@bl = sigma (pbu@@pbl) →
    21292134   low_internal_ram T1 cm1
    21302135     (write_at_stack_pointer …
     
    21462151        pbu)).
    21472152
    2148 axiom high_internal_ram_write_at_stack_pointer:
    2149  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2153lemma high_internal_ram_write_at_stack_pointer:
     2154 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
     2155 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    21502156  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21512157  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
    21522158  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
    21532159  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    2154   bu@@bl = \fst (sigma (pbu@@pbl)) →
     2160  bu@@bl = sigma (pbu@@pbl) →
    21552161   high_internal_ram T1 cm1
    21562162     (write_at_stack_pointer …
     
    21712177          SFR_SP sp2)
    21722178        pbu)).
     2179  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
     2180  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
     2181  cases daemon (* XXX: !!! *)
     2182qed.
    21732183
    21742184lemma Some_Some_elim:
     
    21782188
    21792189(*CSC: ???*)
    2180 axiom snd_assembly_1_pseudoinstruction_ok:
     2190lemma snd_assembly_1_pseudoinstruction_ok:
    21812191  ∀program: pseudo_assembly_program.
    21822192  ∀sigma: Word → Word.
     
    21912201    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
    21922202      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
     2203  #program #sigma #policy #ppc #pi #lookup_labels #lookup_datalabels
     2204  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
     2205  normalize nodelta cases daemon (* XXX: !!! *)
     2206qed.
    21932207
    21942208lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
Note: See TracChangeset for help on using the changeset viewer.