Changeset 872


Ignore:
Timestamp:
Jun 1, 2011, 5:32:49 PM (8 years ago)
Author:
mulligan
Message:

changes from today, need investigation of reduction machine

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r871 r872  
    345345  λv: Vector addressing_mode_tag (S m).
    346346  λq: Vector addressing_mode_tag (S n).
    347   λP: (Vector addressing_mode_tag (S m) × (Vector addressing_mode_tag (S n))) → bool.
    348     P 〈v, q〉.
    349 
    350 axiom union_elim:
    351   ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool.
    352 
    353 (*
     347  λP: (v × q) → bool.
     348    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
     349
     350definition union_elim ≝
     351  λA, B: Type[0].
     352  λelimA: (A → bool) → bool.
     353  λelimB: (B → bool) → bool.
     354  λelimU: A ⊎ B → bool.
     355    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
     356                           
    354357definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    355358  λP.
     
    361364    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
    362365    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
    363     list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. P (DJNZ ? ? addr)) ∧
     366    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    364367    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
    365368    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
     
    381384    P (RETI ?) ∧
    382385    P (NOP ?) ∧
     386    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
    383387    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
    384388    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
    385     bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))).
    386    
    387    
    388    
    389    
    390    
    391     list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)).
    392 
    393     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧
    394     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧
    395     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧
    396     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧
    397     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧
    398     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧
    399     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧
    400     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧
    401     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧
    402     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧
    403     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧
    404     P (RET ?) ∧
    405     P (RETI ?) ∧
    406     P (NOP ?).
     389    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
     390    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
     391                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
     392                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
     393    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
     394    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
     395                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
     396                   (λd. P (XRL ? d)) ∧
     397    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
     398                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
     399                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
     400                   (λd. P (ANL ? d)) ∧
     401    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
     402                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
     403                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
     404                   (λd. P (ORL ? d)) ∧
     405    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
     406                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
     407                   (λd. P (MOVX ? d)) ∧
     408    union_elim ? ? (
     409      union_elim ? ? (
     410        union_elim ? ? (
     411          union_elim ? ? (
     412            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
     413                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
     414                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
     415                            (product_elim ? ? [[dptr]] [[data16]]))
     416                            (product_elim ? ? [[carry]] [[bit_addr]]))
     417                            (product_elim ? ? [[bit_addr]] [[carry]])
     418                            (λd. P (MOV ? d)).
     419  %
     420qed.
    407421 
    408 
    409 axiom instruction_elim: ∀P: instruction → bool. bool.
    410  
    411  
    412 lemma instruction_elim_correct:
    413   ∀i: instruction.
    414   ∀P: instruction → bool.
    415     instruction_elim P = true → ∀j. P j = true.
    416  
     422definition instruction_elim: ∀P: instruction → bool. bool ≝
     423  λP. (*
     424    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
     425    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
     426    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
     427    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
     428    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
     429    P (JMP INDIRECT_DPTR) ∧
     430    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
     431    preinstruction_elim (λp. P (RealInstruction p)). *)
     432  %
     433qed.
     434
     435
     436axiom instruction_elim_complete:
     437 ∀P. instruction_elim P = true → ∀i. P i = true.
     438
     439definition eq_instruction ≝
     440  λi, j: instruction.
     441    true.
     442(*
    417443lemma test:
    418   ∀i: instruction.
    419   ∃pc.
    420   let assembled ≝ assembly1 i in
    421   let code_memory ≝ load_code_memory assembled in
    422   let fetched ≝ fetch code_memory pc in
    423   let 〈instr_pc, ticks〉 ≝ fetched in
    424     \fst instr_pc = i.
    425   # INSTR
    426   @ (ex_intro ?)
    427   [ @ (zero 16)
    428   | @ (instruction_elim INSTR)
    429   ].
    430 *)
     444  let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
     445      (let assembled ≝ assembly1 i in
     446      let code_memory ≝ load_code_memory assembled in
     447      let fetched ≝ fetch code_memory ? in
     448      let 〈instr_pc, ticks〉 ≝ fetched in
     449        eq_instruction (\fst instr_pc)) i = true.
     450 [2: @ zero
     451 | normalize
     452 ]*)
     453
     454lemma test:
     455  ∀i.
     456      (let assembled ≝ assembly1 i in
     457      let code_memory ≝ load_code_memory assembled in
     458      let fetched ≝ fetch code_memory ? in
     459      let 〈instr_pc, ticks〉 ≝ fetched in
     460        eq_instruction (\fst instr_pc)) i = true.
     461 [ @ (instruction_elim_complete )
     462 | @ zero
     463 ]
     464 normalize
     465   
    431466 
    432467(* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset for help on using the changeset viewer.