Changeset 854


Ignore:
Timestamp:
May 27, 2011, 5:13:29 PM (8 years ago)
Author:
mulligan
Message:

commit to avoid conflicts

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r853 r854  
    4444(* RUSSEL **)
    4545
     46let rec bitvector_elim_internal
     47  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
     48  match m return λm. m ≤ n → BitVector (n - m) → bool with
     49  [ O    ⇒ λprf1. λprefix. P ?
     50  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
     51  ].
     52  [ applyS prefix
     53  | letin res ≝ (bit ::: prefix)
     54    < (minus_S_S ? ?)
     55    > (minus_Sn_m ? ?)
     56    [ @ res
     57    | @ prf2
     58    ]
     59  | /2/
     60  ].
     61qed.
     62
     63definition bitvector_elim ≝
     64  λn: nat.
     65  λP: BitVector n → bool.
     66    bitvector_elim_internal n P n ? ?.
     67  [ @ (le_n ?)
     68  | < (minus_n_n ?)
     69    @ [[ ]]
     70  ]
     71qed.
     72
     73lemma subvector_hd_tl:
     74  ∀A: Type[0].
     75  ∀
     76  ∀hd: A.
     77  ∀
     78
     79let rec list_addressing_mode_tags_elim
     80  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
     81  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
     82   (l → bool) → bool ] with
     83  [ VEmpty      ⇒  true 
     84  | VCons len hd tl ⇒ λP.
     85    let process_hd ≝
     86      match hd return λhd. ∀P: hd:::tl → bool. bool with
     87      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
     88      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
     89      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
     90      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
     91      | acc_a ⇒ λP.P ACC_A
     92      | acc_b ⇒ λP.P ACC_B
     93      | dptr ⇒ λP.P DPTR
     94      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
     95      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
     96      | acc_dptr ⇒ λP.P ACC_DPTR
     97      | acc_pc ⇒ λP.P ACC_PC
     98      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
     99      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
     100      | carry ⇒ λP.P CARRY
     101      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
     102      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
     103      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
     104      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
     105      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
     106      ]
     107    in
     108      andb (process_hd P)
     109       (match len return λlen. Vector addressing_mode_tag len → bool with
     110         [ O ⇒ λ_.true
     111         | S y ⇒ λtl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl)
     112  ].
     113  [1: @ (execute_1_technical ? ? tl)
     114      [ //
     115      |
     116      ]
     117  ].
     118
     119definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
     120 λP.
     121   P (ADD … ACC_A
     122   P (DA … ACC_A).
     123 %
     124qed.
     125 
     126
     127definition instruction_elim: ∀P: instruction → bool. bool.
     128 
     129 
     130lemma instruction_elim_correct:
     131  ∀i: instruction.
     132  ∀P: instruction → bool.
     133    instruction_elim P = true → ∀j. P j = true.
     134 
     135lemma test:
     136  ∀i: instruction.
     137  ∃pc.
     138  let assembled ≝ assembly1 i in
     139  let code_memory ≝ load_code_memory assembled in
     140  let fetched ≝ fetch code_memory pc in
     141  let 〈instr_pc, ticks〉 ≝ fetched in
     142    \fst instr_pc = i.
     143  # INSTR
     144  @ (ex_intro ?)
     145  [ @ (zero 16)
     146  | @ (instruction_elim INSTR)
     147  ].
     148 
     149    (* > append_cons_commute
     150    @
    46151
    47152include "basics/jmeq.ma".
  • src/ASM/Vector.ma

    r749 r854  
    494494  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    495495
     496
    496497definition subvector_with ≝
    497498  λA: Type[0].
Note: See TracChangeset for help on using the changeset viewer.