Changeset 1975


Ignore:
Timestamp:
May 21, 2012, 5:48:43 PM (5 years ago)
Author:
mulligan
Message:

Work from today on closing main_thm.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1972 r1975  
    13801380  -assm #c #assm cases assm
    13811381  -assm #r #assm cases assm destruct
    1382   cases l cases c cases r //
     1382  cases l cases c cases r assumption
    13831383qed.
    13841384
     
    14511451qed.
    14521452
    1453 axiom eq_instruction_to_eq:
     1453lemma eq_instruction_to_eq:
    14541454  ∀i1, i2: instruction.
    14551455    eq_instruction i1 i2 = true → i1 ≃ i2.
     1456  #i1 #i2
     1457  cases i1 cases i2 cases daemon (*
     1458  [1,10,19,28,37,46:
     1459    #arg1 #arg2
     1460    whd in match (eq_instruction ??);
     1461    cases arg1 #subaddressing_mode
     1462    cases subaddressing_mode
     1463    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1464    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1465    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1466    #word11 #irrelevant
     1467    cases arg2 #subaddressing_mode
     1468    cases subaddressing_mode
     1469    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1470    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1471    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     1472    #word11' #irrelevant normalize nodelta
     1473    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
     1474qed.
    14561475         
    14571476lemma fetch_assembly_pseudo':
  • src/ASM/AssemblyProofSplit.ma

    r1971 r1975  
    6666qed.
    6767
     68lemma get_8051_sfr_set_clock:
     69  ∀M: Type[0].
     70  ∀cm: M.
     71  ∀s: PreStatus M cm.
     72  ∀sfr: SFR8051.
     73  ∀t: Time.
     74    get_8051_sfr M cm (set_clock M cm s t) sfr =
     75      get_8051_sfr M cm s sfr.
     76  #M #cm #s #sfr #t %
     77qed.
    6878
    6979lemma special_function_registers_8051_set_arg_16:
     
    102112 #A #B #C #P * #a #b * //
    103113qed.
    104 *)
    105114
    106115lemma tech_pi1_let_as_commute:
     
    113122 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
    114123qed.
     124*)
    115125
    116126include alias "arithmetics/nat.ma".
     
    119129
    120130lemma pair_replace:
    121  ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c=c' → c ≃ 〈a,b〉 →
     131 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
    122132  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
    123133 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
     134qed.
     135
     136lemma pair_as_replace:
     137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c' → T. ∀EQc: c'= c.
     138  c ≃ 〈a,b〉 →
     139  P (let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H).
     140  [2:
     141    >EQc assumption
     142  |1:
     143    #A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct //
     144  ]
     145qed.
     146
     147lemma if_then_else_replace:
     148  ∀T: Type[0].
     149  ∀P: T → Prop.
     150  ∀t1, t2: T.
     151  ∀c, c', c'': bool.
     152    c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
     153  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
     154  assumption
    124155qed.
    125156
     
    159190 ∀P.
    160191 ∀EQP:
    161   P = (λs. ∃n:ℕ
    162       .execute n
     192  P = (λs.
     193        execute (|expand_relative_jump lookup_labels sigma ppc instr|)
    163194       (code_memory_of_pseudo_assembly_program cm sigma
    164195        policy)
     
    271302            ]
    272303        | INC addr ⇒ λinstr_refl.
    273             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
    274               [ ACC_A ⇒ λacc_a: True.
     304            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     305              [ ACC_A ⇒ λacc_a: True. λEQaddr.
    275306                let s' ≝ add_ticks1 s in
    276307                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
    277308                 set_arg_8 … s' ACC_A result
    278               | REGISTER r ⇒ λregister: True.
     309              | REGISTER r ⇒ λregister: True. λEQaddr.
    279310                let s' ≝ add_ticks1 s in
    280311                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    281312                 set_arg_8 … s' (REGISTER r) result
    282               | DIRECT d ⇒ λdirect: True.
     313              | DIRECT d ⇒ λdirect: True. λEQaddr.
    283314                let s' ≝ add_ticks1 s in
    284315                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    285316                 set_arg_8 … s' (DIRECT d) result
    286               | INDIRECT i ⇒ λindirect: True.
     317              | INDIRECT i ⇒ λindirect: True. λEQaddr.
    287318                let s' ≝ add_ticks1 s in
    288319                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    289320                 set_arg_8 … s' (INDIRECT i) result
    290               | DPTR ⇒ λdptr: True.
     321              | DPTR ⇒ λdptr: True. λEQaddr.
    291322                let s' ≝ add_ticks1 s in
    292323                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     
    295326                 set_8051_sfr … s' SFR_DPH bu
    296327              | _ ⇒ λother: False. ⊥
    297               ] (subaddressing_modein … addr)
     328              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
    298329        | NOP ⇒ λinstr_refl.
    299330           let s ≝ add_ticks2 s in
     
    343374                s
    344375        | CLR addr ⇒ λinstr_refl.
    345           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    346             [ ACC_A ⇒ λacc_a: True.
     376          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     377            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
    347378              let s ≝ add_ticks1 s in
    348379               set_arg_8 … s ACC_A (zero 8)
    349             | CARRY ⇒ λcarry: True.
     380            | CARRY ⇒ λcarry: True.  λEQaddr.
    350381              let s ≝ add_ticks1 s in
    351382               set_arg_1 … s CARRY false
    352             | BIT_ADDR b ⇒ λbit_addr: True.
     383            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
    353384              let s ≝ add_ticks1 s in
    354385               set_arg_1 … s (BIT_ADDR b) false
    355386            | _ ⇒ λother: False. ⊥
    356             ] (subaddressing_modein … addr)
     387            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
    357388        | CPL addr ⇒ λinstr_refl.
    358           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
    359             [ ACC_A ⇒ λacc_a: True.
     389          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     390            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
    360391                let s ≝ add_ticks1 s in
    361392                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    362393                let new_acc ≝ negation_bv ? old_acc in
    363394                 set_8051_sfr … s SFR_ACC_A new_acc
    364             | CARRY ⇒ λcarry: True.
     395            | CARRY ⇒ λcarry: True. λEQaddr.
    365396                let s ≝ add_ticks1 s in
    366397                let old_cy_flag ≝ get_arg_1 … s CARRY true in
    367398                let new_cy_flag ≝ ¬old_cy_flag in
    368399                 set_arg_1 … s CARRY new_cy_flag
    369             | BIT_ADDR b ⇒ λbit_addr: True.
     400            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
    370401                let s ≝ add_ticks1 s in
    371402                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
     
    373404                 set_arg_1 … s (BIT_ADDR b) new_bit
    374405            | _ ⇒ λother: False. ?
    375             ] (subaddressing_modein … addr)
     406            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
    376407        | SETB b ⇒ λinstr_refl.
    377408            let s ≝ add_ticks1 s in
     
    410441              set_8051_sfr … s SFR_ACC_A new_acc
    411442        | PUSH addr ⇒ λinstr_refl.
    412             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
    413               [ DIRECT d ⇒ λdirect: True.
     443            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
     444              [ DIRECT d ⇒ λdirect: True. λEQaddr.
    414445                let s ≝ add_ticks1 s in
    415446                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     
    417448                  write_at_stack_pointer … s d
    418449              | _ ⇒ λother: False. ⊥
    419               ] (subaddressing_modein … addr)
     450              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
    420451        | POP addr ⇒ λinstr_refl.
    421452            let s ≝ add_ticks1 s in
     
    596627 ) (*66s*)
    597628whd in match execute_1_preinstruction; normalize nodelta
    598 [1: (* ADD *)
    599   >p normalize nodelta
    600   >EQP %{1}
    601   whd in ⊢ (??%?);
    602   (* work on fetch_many *)
     629[4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
     630  lapply (subaddressing_modein ???)
     631  <EQaddr normalize nodelta #irrelevant
     632  try (>p normalize nodelta)
     633  try (>p1 normalize nodelta)
     634  (* XXX: start work on the left hand side *)
     635  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     636  (* XXX: work on fetch_many *)
    603637  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    604638  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    605639  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    606   <EQppc
    607   cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     640  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    608641  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    609   lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     642  >(eq_bv_eq … fetch_many_assm) -newpc
    610643  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     644  (* XXX: work on sigma commutation *)
     645  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     646  (* XXX: work on ticks (of all kinds) *)
     647  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     648  (* XXX: work on both sides *)
     649  [1,2,3,4,5:
     650    generalize in ⊢ (??(???(?%))?);
     651  |6,7,8,9,10,11:
     652    generalize in ⊢ (??(???(?%))?);
     653  |12:
     654    generalize in ⊢ (??(???(?%))?);
     655  ]
     656  <EQaddr normalize nodelta #irrelevant
     657  [1:
     658    @(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p)
     659 
     660  (* XXX: removes status 's' *)
     661  normalize nodelta >EQs -s -ticks
     662  whd in ⊢ (??%%);
     663  (* XXX: simplify the left hand side *)
     664
     665  (* XXX: work on both sides *)
     666|1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI  *)
     667  (* XXX: simplify the right hand side *)
     668  >p normalize nodelta
     669  try (>p1 normalize nodelta)
     670  (* XXX: start work on the left hand side *)
     671  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     672  (* XXX: work on fetch_many *)
     673  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     674  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     675  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     676  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     677  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     678  >(eq_bv_eq … fetch_many_assm) -newpc
     679  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     680  (* XXX: work on sigma commutation *)
     681  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     682  (* XXX: work on ticks (of all kinds) *)
     683  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     684  (* XXX: simplify the left hand side *)
    611685  @(pair_replace ?????????? p)
    612    [2: normalize nodelta >EQs -s >EQticks' -ticks'
    613        <instr_refl in EQticks; #EQticks >EQticks -ticks
    614        <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    615        whd in ⊢ (??%%);
    616        @split_eq_status
    617        try %
    618        [3: whd in ⊢ (??%%); >EQnewpc >sigma_increment_commutation %
    619        |2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
     686  [1,3,5,7,9,11,13,15:
     687    cases daemon
     688  |12,14,16:
     689    normalize nodelta
     690    @(pair_replace ?????????? p1)
     691       [1,3,5:
     692         cases daemon
     693       ]
     694  ]
     695  (* XXX: removes status 's' *)
     696  normalize nodelta >EQs -s -ticks
     697  whd in ⊢ (??%%);
     698  (* XXX: work on both sides *)
     699  cases daemon (*
     700       @split_eq_status try %
     701       [*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
    620702           whd in match (set_flags ??????);
    621703           (* CSC: TO BE COMPLETED *)
    622        ]
    623    | (*>get_arg_8_ok_set_clock*) (*CSC: to be done *)
    624    ]
    625 
    626 ] cases daemon
     704       ] *)
     705|10,42,43,44,45,49,52,56: (* MUL *)
     706  (* XXX: simplify the right hand side *)
     707  (* XXX: start work on the left hand side *)
     708  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     709  (* XXX: work on fetch_many *)
     710  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     711  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     712  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     713  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     714  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     715  >(eq_bv_eq … fetch_many_assm) -newpc
     716  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     717  (* XXX: work on sigma commutation *)
     718  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     719  (* XXX: work on ticks (of all kinds) *)
     720  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     721  (* XXX: removes status 's' *)
     722  normalize nodelta >EQs -s -ticks
     723  whd in ⊢ (??%%);
     724  (* XXX: work on both sides *)
     725  (* @split_eq_status try % *)
     726  cases daemon
     727|11,12: (* DIV *)
     728  normalize nodelta in p;
     729  >p normalize nodelta
     730  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     731  (* XXX: work on fetch_many *)
     732  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     733  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     734  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     735  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     736  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     737  >(eq_bv_eq … fetch_many_assm) -newpc
     738  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     739  (* XXX: work on sigma commutation *)
     740  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     741  (* XXX: work on ticks (of all kinds) *)
     742  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     743  (* XXX: work on both sides *)
     744  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
     745  >(?: pose_assm = 0)
     746  [2,4:
     747    <p >pose_refl
     748    cases daemon
     749  |1,3:
     750    (* XXX: removes status 's' *)
     751    normalize nodelta >EQs -s -ticks
     752    whd in ⊢ (??%%);
     753    (* XXX: work on both sides *)
     754    @split_eq_status try %
     755    cases daemon
     756  ]
     757|13,14,15: (* DA *)
     758  >p normalize nodelta
     759  >p1 normalize nodelta
     760  try (>p2 normalize nodelta
     761  try (>p3 normalize nodelta
     762  try (>p4 normalize nodelta
     763  try (>p5 normalize nodelta))))
     764  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     765  (* XXX: work on fetch_many *)
     766  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     767  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     768  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     769  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     770  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     771  >(eq_bv_eq … fetch_many_assm) -newpc
     772  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     773  (* XXX: work on sigma commutation *)
     774  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     775  (* XXX: work on ticks (of all kinds) *)
     776  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     777  (* XXX: work on both sides *)
     778  @(pair_replace ?????????? p)
     779  [1,3,5:
     780    cases daemon
     781  |2,4,6:
     782    @(if_then_else_replace ???????? p1)
     783    [1,3,5:
     784      cases daemon
     785    |2,4:
     786      normalize nodelta
     787      @(pair_replace ?????????? p2)
     788      [1,3:
     789        cases daemon
     790      |2,4:
     791        normalize nodelta >p3 normalize nodelta
     792        >p4 normalize nodelta try >p5
     793      ]
     794    ]
     795    (* XXX: removes status 's' *)
     796    normalize nodelta >EQs -s -ticks
     797    whd in ⊢ (??%%);
     798    (* XXX: work on both sides *)
     799    @split_eq_status try %
     800    cases daemon
     801  ]
     802|33,34,35: (* ANL, ORL, XRL *)
     803  (* XXX: simplify the right hand side *)
     804  [1,2,3:
     805    inversion addr #addr' #EQaddr normalize nodelta
     806    [1,3:
     807      inversion addr' #addr'' #EQaddr' normalize nodelta
     808    ]
     809  ]
     810  @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta
     811  (* XXX: start work on the left hand side *)
     812  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
     813  (* XXX: work on fetch_many *)
     814  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
     815  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     816  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
     817  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
     818  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
     819  >(eq_bv_eq … fetch_many_assm) -newpc
     820  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     821  (* XXX: work on sigma commutation *)
     822  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
     823  (* XXX: work on ticks (of all kinds) *)
     824  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     825  (* XXX: simplify the left hand side *)
     826  >EQaddr normalize nodelta try (>EQaddr' normalize nodelta)
     827  >lft_rgt_refl normalize nodelta
     828  (* XXX: removes status 's' *)
     829  normalize nodelta >EQs -s -ticks
     830  whd in ⊢ (??%%);
     831  (* XXX: work on both sides *)
     832  cases daemon
     833|
    627834qed.
    628835(*   
Note: See TracChangeset for help on using the changeset viewer.