Ignore:
Timestamp:
Jun 7, 2011, 2:56:39 AM (9 years ago)
Author:
sacerdot
Message:

Better statement, begin of uniform proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r889 r890  
    698698qed.
    699699
     700let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     701                       (encoding: list Byte) on encoding: Prop ≝
     702  match encoding with
     703  [ nil ⇒ final_pc = pc
     704  | cons hd tl ⇒
     705    let 〈new_pc, byte〉 ≝ next code_memory pc in
     706      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
     707  ].
     708
     709axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
     710
     711(*
    700712lemma test:
    701713  ∀pc,i.
     
    705717      let 〈instr_pc, ticks〉 ≝ fetched in
    706718        eq_instruction (\fst instr_pc)) i = true.
    707  #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
     719*)
     720lemma test:
     721  ∀pc,i,code_memory.
     722      let assembled ≝ assembly1 i in
     723      let len ≝ length … assembled in
     724      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     725      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
     726      let 〈instr_pc, ticks〉 ≝ fetched in
     727      let 〈instr,pc'〉 ≝ instr_pc in
     728       (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
     729 #pc #i #code_memory cases i [8: *]
     730 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
     731 [47,48,49: |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
     732  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
     733   59,60,63,64,65,66,67: #ARG]
     734 [1: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
     735 
     736 [7: #arg2]
     737 
     738  whd
     739 [ @(list_addressing_mode_tags_elim_prop … arg) whd try %
     740   @(list_addressing_mode_tags_elim_prop … arg2) whd try %
     741   * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
     742   whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 >eq_instruction_refl @eq_bv_refl
     743 |6: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
     744   * #H1 * #H2 #H3 whd in H3; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
     745   whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 <H3 >eq_instruction_refl @eq_bv_refl
     746 |7: @(list_addressing_mode_tags_elim_prop … arg) whd try %
     747   * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
     748 |3,5: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
     749   
     750   @split_elim
     751
     752 
     753   whd in ⊢ (??%?)
    708754   [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    709755         whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
     
    12971343 |   
    12981344
    1299 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    1300                        (encoding: list Byte) on encoding: Prop ≝
    1301   match encoding with
    1302   [ nil ⇒ final_pc = pc
    1303   | cons hd tl ⇒
    1304     let 〈new_pc, byte〉 ≝ next code_memory pc in
    1305       hd = byte ∧ encoding_check code_memory new_pc final_pc tl
    1306   ].
    1307 
    13081345definition assembly_specification:
    13091346  ∀assembly_program: pseudo_assembly_program.
Note: See TracChangeset for help on using the changeset viewer.