Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (8 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofsSplit.ma

    r2172 r2272  
    8181  ∀cm: M.
    8282  ∀s: PreStatus M cm.
    83   ∀sfr: SFR8051.
    8483  ∀pc: Word.
    8584    get_8051_sfr M cm (set_program_counter M cm s pc) =
    8685      get_8051_sfr M cm s.
    87   #M #cm #s #sfr #pc %
     86  #M #cm #s #pc %
    8887qed.
    8988
     
    360359  ∀sigma: Word → Word.
    361360  ∀policy: Word → bool.
    362     \snd M = data
     361    \snd M = None …
    363362      special_function_registers_8051 pseudo_assembly_program cm s =
    364363        special_function_registers_8051 (BitVectorTrie Byte 16)
     
    457456  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    458457  cases M #left #right cases right normalize nodelta try %
    459   -right * #address
     458  -right * * #address normalize nodelta
    460459  @pair_elim #high #low #high_low_refl normalize nodelta
    461460  whd in match sfr_8051_index; normalize nodelta
     
    469468include alias "ASM/BitVectorTrie.ma".
    470469*)
    471 
    472 lemma get_8051_sfr_status_of_pseudo_status:
    473   ∀M.
    474   ∀cm, ps, sigma, policy.
    475   ∀sfr.
    476     (sfr = SFR_ACC_A → \snd M = data) →
    477     get_8051_sfr (BitVectorTrie Byte 16)
    478       (code_memory_of_pseudo_assembly_program cm sigma policy)
    479       (status_of_pseudo_status M cm ps sigma policy) sfr =
    480     get_8051_sfr pseudo_assembly_program cm ps sfr.
    481   #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
    482   [18:
    483      >relevant %
    484   ]
    485   cases sndM try % * #address
    486   whd in match get_8051_sfr;
    487   whd in match status_of_pseudo_status; normalize nodelta
    488   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    489   @pair_elim #upper #lower #upper_lower_refl
    490   @get_index_v_set_index_miss @nmk #relevant
    491   normalize in relevant; destruct(relevant)
    492 qed.
    493470
    494471lemma bitvector_cases_hd_tl:
     
    572549      special_function_registers_8051 M cm ps.
    573550  //
    574 qed.
    575 
    576 lemma get_arg_8_pseudo_addressing_mode_ok:
    577   ∀M: internal_pseudo_address_map.
    578   ∀cm: pseudo_assembly_program.
    579   ∀ps: PreStatus pseudo_assembly_program cm.
    580   ∀sigma: Word → Word.
    581   ∀policy: Word → bool.
    582   ∀addr1: [[registr; direct]].
    583     addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
    584       get_arg_8 (BitVectorTrie Byte 16)
    585         (code_memory_of_pseudo_assembly_program cm sigma policy)
    586         (status_of_pseudo_status M cm ps sigma policy) true addr1 =
    587       get_arg_8 pseudo_assembly_program cm ps true addr1.
    588   [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    589   #M #cm #ps #sigma #policy #addr1
    590   @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
    591   [1:
    592     whd in ⊢ (??%? → ??%?);
    593     whd in match bit_address_of_register; normalize nodelta
    594     @pair_elim #un #ln #un_ln_refl
    595     lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
    596     @(pair_replace ?????????? un_ln_refl)
    597     [1:
    598       whd in match get_8051_sfr; normalize nodelta
    599       whd in match sfr_8051_index; normalize nodelta
    600       @eq_f <get_index_v_special_function_registers_8051_not_acc_a
    601       try % #absurd destruct(absurd)
    602     |2:
    603       #assembly_mode_ok_refl
    604       >low_internal_ram_of_pseudo_internal_ram_miss
    605       [1:
    606         %
    607       |2:
    608         cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
    609         #absurd try % @sym_eq assumption
    610       ]
    611     ]
    612   |2:
    613     #addressing_mode_ok_refl whd in ⊢ (??%?);
    614     @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
    615     @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    616     inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    617     [1:
    618       whd in ⊢ (??%%); normalize nodelta
    619       cases (eqb ??) normalize nodelta [1: % ]
    620       cases (eqb ??) normalize nodelta [1: % ]
    621       cases (eqb ??) normalize nodelta [1: % ]
    622       cases (eqb ??) normalize nodelta [1: % ]
    623       cases (eqb ??) normalize nodelta [1:
    624         @get_8051_sfr_status_of_pseudo_status
    625         #absurd destruct(absurd)
    626       ]
    627       cases (eqb ??) normalize nodelta [1:
    628         @get_8051_sfr_status_of_pseudo_status
    629         #absurd destruct(absurd)
    630       ]
    631       cases (eqb ??) normalize nodelta [1:
    632         @get_8051_sfr_status_of_pseudo_status
    633         #absurd destruct(absurd)
    634       ]
    635       cases (eqb ??) normalize nodelta [1:
    636         @get_8051_sfr_status_of_pseudo_status
    637         #absurd destruct(absurd)
    638       ]
    639       cases (eqb ??) normalize nodelta [1:
    640         @get_8051_sfr_status_of_pseudo_status
    641         #absurd destruct(absurd)
    642       ]
    643       cases (eqb ??) normalize nodelta [1: % ]
    644       cases (eqb ??) normalize nodelta [1: % ]
    645       cases (eqb ??) normalize nodelta [1: % ]
    646       cases (eqb ??) normalize nodelta [1: % ]
    647       cases (eqb ??) normalize nodelta [1: % ]
    648       cases (eqb ??) normalize nodelta [1:
    649         @get_8051_sfr_status_of_pseudo_status
    650         #absurd destruct(absurd)
    651       ]
    652       cases (eqb ??) normalize nodelta [1:
    653         @get_8051_sfr_status_of_pseudo_status
    654         #absurd destruct(absurd)
    655       ]
    656       cases (eqb ??) normalize nodelta [1:
    657         @get_8051_sfr_status_of_pseudo_status
    658         #absurd destruct(absurd)
    659       ]
    660       cases (eqb ??) normalize nodelta [1:
    661         @get_8051_sfr_status_of_pseudo_status
    662         #absurd destruct(absurd)
    663       ]
    664       cases (eqb ??) normalize nodelta [1:
    665         @get_8051_sfr_status_of_pseudo_status
    666         #absurd destruct(absurd)
    667       ]
    668       cases (eqb ??) normalize nodelta [1:
    669         @get_8051_sfr_status_of_pseudo_status
    670         #absurd destruct(absurd)
    671       ]
    672       cases (eqb ??) normalize nodelta [1:
    673         @get_8051_sfr_status_of_pseudo_status
    674         #absurd destruct(absurd)
    675       ]
    676       cases (eqb ??) normalize nodelta [1:
    677         @get_8051_sfr_status_of_pseudo_status
    678         #absurd destruct(absurd)
    679       ]
    680       cases (eqb ??) normalize nodelta [1:
    681         @get_8051_sfr_status_of_pseudo_status
    682         #absurd destruct(absurd)
    683       ]
    684       cases (eqb ??) normalize nodelta [1:
    685         @get_8051_sfr_status_of_pseudo_status
    686         #absurd destruct(absurd)
    687       ]
    688       inversion (eqb ??) #eqb_refl normalize nodelta [1:
    689         @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
    690         whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
    691         >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
    692         #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
    693         #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
    694       ]
    695       cases (eqb ??) normalize nodelta [1:
    696         @get_8051_sfr_status_of_pseudo_status
    697         #absurd destruct(absurd)
    698       ] %
    699     |2:
    700       lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
    701       whd in match status_of_pseudo_status; normalize nodelta
    702       >low_internal_ram_of_pseudo_internal_ram_miss try %
    703       cut(arg = false:::(three_bits@@nl))
    704       [1:
    705         <get_index_v_refl
    706         cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
    707         [1:
    708           cut(ignore = [[get_index_v bool 4 nu 0 ?]])
    709           [1:
    710             @le_S_S @le_O_n
    711           |2:
    712             cut(ignore = \fst (vsplit bool 1 3 nu))
    713             [1:
    714               >ignore_three_bits_refl %
    715             |2:
    716               #ignore_refl >ignore_refl
    717               cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
    718               >nu_refl %
    719             ]
    720           |3:
    721             #ignore_refl >ignore_refl in ignore_three_bits_refl;
    722             #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
    723             #nu_refl <nu_refl %
    724           ]
    725         |2:
    726           #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
    727           @sym_eq @vsplit_ok >nu_nl_refl %
    728         ]
    729       |2:
    730         #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
    731         normalize nodelta
    732         [1:
    733           cases (eq_bv ???) normalize #absurd destruct(absurd)
    734         |2:
    735           #_ %
    736         ]
    737       ]
    738     ]
    739   ] *)
    740551qed.
    741552
     
    811622  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
    812623  whd in match (set_8051_sfr ?????);
    813   cases M #callM * try % #upper_lower #address
     624  cases M * #low #high * try % * *
    814625  whd in match (special_function_registers_8051 ???);
    815   whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
     626  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta
    816627  @pair_elim #high #low #high_low_refl normalize nodelta
    817628  cases (eq_upper_lower ??) normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.