Changeset 846


Ignore:
Timestamp:
May 25, 2011, 6:10:04 PM (8 years ago)
Author:
mulligan
Message:

changes

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r844 r846  
    675675definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    676676 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
    677 
  • src/ASM/AssemblyProof.ma

    r845 r846  
    131131  ].
    132132
    133 axiom sigma: pseudo_assembly_program → Word → Word.
     133axiom sigma': pseudo_assembly_program → Word → Word.
    134134
    135135definition assembly_specification:
     
    141141      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
    142142      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
    143       let labels ≝ λx. sigma pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
    144       let datalabels ≝ λx. sigma pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
     143      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
     144      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
    145145      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
    146        (sigma pseudo_assembly_program pc) labels datalabels pre_instr in
     146       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
    147147      match pre_assembled with
    148148       [ None ⇒ True
    149149       | Some pc_code ⇒
    150150          let 〈new_pc,code〉 ≝ pc_code in
    151            encoding_check code_mem pc (sigma pseudo_assembly_program pre_new_pc) code ].
     151           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
    152152
    153153axiom assembly_meets_specification:
     
    185185    | Some p ⇒
    186186       let cm ≝ load_code_memory (\fst p) in
    187        let pc ≝ sigma pap (program_counter ? ps) in
     187       let pc ≝ sigma' pap (program_counter ? ps) in
    188188        Some …
    189189         (mk_PreStatus (BitVectorTrie Byte 16)
     
    198198           (p3_latch … ps)
    199199           (clock … ps)) ].
    200            
     200(*
    201201definition write_at_stack_pointer':
    202202 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
     
    300300    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
    301301    ].
    302  #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     302 #ps #ps' #H whd in ⊢ (mat
     303 ch % with [ _ ⇒ ? | _ ⇒ ? ])
    303304 generalize in match (refl … (assembly (code_memory … ps)))
    304305 cases (assembly ?) in ⊢ (???% → %)
    305306  [ #K whd whd in ⊢ (??%?) <H >K %
    306307  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    307 qed.
     308qed.*)
     309
     310let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
     311  match encoding with
     312  [ nil ⇒ True
     313  | cons hd tl ⇒
     314    let 〈new_pc, byte〉 ≝ next code_memory pc in
     315      hd = byte ∧ encoding_check' code_memory new_pc tl
     316  ].
     317
     318lemma test:
     319  ∀i: instruction.
     320  ∃pc.
     321  let assembled ≝ assembly1 i in
     322  let code_memory ≝ load_code_memory assembled in
     323  let fetched ≝ fetch code_memory pc in
     324  let 〈instr_pc, ticks〉 ≝ fetched in
     325    \fst instr_pc = i.
     326  # INSTR
     327  %
     328  [ @ (zero 16)
     329  | cases INSTR
     330  ].
     331
     332lemma test:
     333  ∀pc: Word.
     334  ∀code_memory: BitVectorTrie Byte 16.
     335  ∀i: instruction.
     336    let assembled ≝ assembly1 i in
     337      encoding_check' code_memory pc assembled →
     338        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
     339        let 〈instr, pc〉 ≝ instr_pc in
     340          instr = i.
     341  # PC # CODE_MEMORY # INSTRUCTION
     342  whd
     343  whd in ⊢ (? → match % with [ _ ⇒ ? ])
     344  cases (next CODE_MEMORY PC)
     345  whd
     346  # PC1 # V1
     347
     348
     349  cases (fetch CODE_MEMORY PC)
     350  # INSTR_PC
     351  # TICKS
     352  cases (INSTRUCTION)
     353  [ # ADDR11
     354    # ENCODING_CHECK
     355    whd in ENCODING_CHECK;
     356    normalize
     357    cases (INSTR_PC)
     358    # INSTR
     359    # PC
     360    normalize
     361   
     362   
     363  # ENCODING
     364  normalize
     365  [ cases INSTR_PC
     366    # NEW_INSTRUCTION
     367    # PC
     368    normalize
     369    normalize in ENCODING;
     370  | # ASSEMBLED
     371    whd
    308372 
    309373lemma main_thm:
Note: See TracChangeset for help on using the changeset viewer.