Ignore:
Timestamp:
Jul 2, 2012, 11:37:34 AM (8 years ago)
Author:
mulligan
Message:

Changes to the subaddressing mode elim functions moved into their correct place in ASM.ma. ticks_of0 completed, with all daemons removed. Another commutation lemma added in AssemblyProofSplit?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2140 r2143  
    175175  ∀s: PreStatus M cm.
    176176  ∀flag: bool.
    177   ∀addr.
     177  ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
    178178  ∀pc: Word.
    179179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
    180180      get_arg_8 M cm s flag addr.
     181  [2,3:
     182    cases addr #subaddressing_mode
     183    cases subaddressing_mode
     184    try (#addr1 whd in ⊢ (% → %);)
     185    whd in ⊢ (% → %); //
     186  ]
    181187  #M #cm #s #flag #addr #pc
    182188  whd in match get_arg_8; normalize nodelta
    183189  cases addr *
    184   try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I)
    185190  try (#addr1 #absurd normalize in absurd; cases absurd @I)
    186191  try (#absurd normalize in absurd; cases absurd @I)
    187192  try (#addr1 #addr2) try #addr1
    188   normalize nodelta try %
    189   cases daemon (* XXX: rewrite not working but provable *)
     193  normalize nodelta %
    190194qed.
    191195
     
    319323  #M #cm #s #pc #pc' %
    320324qed.
     325
     326(* XXX: move elsewhere *)
     327lemma bitvector_8_cases:
     328  ∀w: BitVector 8.
     329    ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
     330      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
     331 #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
     332 >(BitVector_O … w) %
     333qed.
     334
     335(* XXX: not true
     336lemma p3_latch_set_arg_8:
     337  ∀M: Type[0].
     338  ∀cm: M.
     339  ∀s: PreStatus M cm.
     340  ∀args.
     341  ∀v: Byte.
     342    p3_latch M cm (set_arg_8 M cm s args v) =
     343      p3_latch M cm s.
     344  #M #cm #s #args #v
     345  @(subaddressing_mode_elim … args)
     346  try #w try %
     347  whd in match set_arg_8; normalize nodelta
     348  whd in match set_arg_8'; normalize nodelta
     349  inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
     350  inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     351  inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
     352  whd in match set_bit_addressable_sfr; normalize nodelta
     353  @(bitvector_8_elim_prop … w)
     354*)
     355
     356lemma status_of_pseudo_status_does_not_change_8051_sfrs:
     357  ∀M: internal_pseudo_address_map.
     358  ∀cm: pseudo_assembly_program.
     359  ∀s: PreStatus pseudo_assembly_program cm.
     360  ∀sigma: Word → Word.
     361  ∀policy: Word → bool.
     362    \snd M = (None …) →
     363      special_function_registers_8051 pseudo_assembly_program cm s =
     364        special_function_registers_8051 (BitVectorTrie Byte 16)
     365          (code_memory_of_pseudo_assembly_program cm sigma policy)
     366          (status_of_pseudo_status M cm s sigma policy).
     367  #M #cm #s #sigma #policy #None_proof cases s
     368  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     369  whd in match status_of_pseudo_status; normalize nodelta
     370  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     371  >None_proof %
     372qed.
     373
     374lemma special_function_registers_8051_set_program_counter:
     375  ∀cm: pseudo_assembly_program.
     376  ∀ps: PreStatus pseudo_assembly_program cm.
     377  ∀v: Word.
     378  special_function_registers_8051 pseudo_assembly_program cm
     379   (set_program_counter pseudo_assembly_program cm ps v) =
     380     special_function_registers_8051 pseudo_assembly_program cm ps.
     381  #cm #ps #v %
     382qed.
     383
     384(*
     385lemma get_arg_8_status_of_pseudo_status:
     386  ∀M: internal_pseudo_address_map.
     387  ∀cm: pseudo_assembly_program.
     388  ∀ps.
     389  ∀sigma: Word → Word.
     390  ∀policy: Word → bool.
     391  ∀b: bool.
     392  ∀addr1: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect_dptr]].
     393    get_arg_8 (BitVectorTrie Byte 16)
     394     (code_memory_of_pseudo_assembly_program cm sigma policy)
     395     (status_of_pseudo_status M cm ps sigma policy) b addr1 =
     396    get_arg_8 pseudo_assembly_program cm ps b addr1.
     397  [2,3:
     398    @(subaddressing_mode_elim … addr1) try #w @I
     399  ]
     400  #M #cm #ps #sigma #policy #b #addr1
     401  @(subaddressing_mode_elim … addr1)
     402  try #w
     403  [1:
     404    whd in ⊢ (??%%);
     405    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     406    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     407    cases (get_index_v bool ????) normalize nodelta try %
     408    cases daemon (* XXX: require axioms from Assembly.ma *)
     409  |2:
     410    whd in ⊢ (??%%);
     411    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     412    lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
     413    @(pair_replace ?????????? nu_nl_refl) [1: cases daemon (* XXX: !! *) ]
     414    @pair_elim #bit_one_v #three_bits #bit_one_v_three_bits_refl normalize nodelta
     415    cases (get_index_v bool ????) normalize nodelta
     416    cases daemon (* XXX: same as above *)
     417  |3:
     418    whd in ⊢ (??%%); @(bitvector_3_elim_prop … w)
     419    whd in match bit_address_of_register; normalize nodelta
     420    @pair_elim #un #ln #un_ln_refl
     421    cases (¬get_index_v bool ???? ∧ ¬get_index_v bool ????) normalize nodelta
     422    [1,3,5,7,9,11,13,15:
     423      cases daemon (* XXX: same as above *)
     424    |*:
     425      cases (¬get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
     426      [1,3,5,7,9,11,13,15:
     427        cases daemon (* XXX: same as above *)
     428      |*:
     429        cases (get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
     430        cases daemon (* XXX: same as above *)
     431      ]
     432    ]
     433  |4,5:
     434    whd in ⊢ (??%%); <status_of_pseudo_status_does_not_change_8051_sfrs %
     435  |6,7,8:
     436    %
     437  ]
     438qed.
     439*)
    321440
    322441(*
     
    823942  >p normalize nodelta >p1 normalize nodelta
    824943  (* XXX: switch to the left hand side *)
    825   -instr_refl >EQP -P normalize nodelta
     944  >EQP -P normalize nodelta
    826945  #sigma_increment_commutation #maps_assm #fetch_many_assm
    827946  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     
    843962    @(pair_replace ?????????? p) normalize nodelta
    844963    [1,3:
    845       >get_arg_8_set_program_counter
    846       cases daemon
     964      >(get_arg_8_set_program_counter … true addr1) in ⊢ (??%?);
     965      [2,4: (* /2 by _/ *) cases daemon ] @eq_f3 [2,3,5,6: % ]
     966      whd in ⊢ (??%?); @(subaddressing_mode_elim … addr1)
     967      #arg normalize nodelta whd in ⊢ (???%);
     968      [1,3:
     969        whd in match get_register; normalize nodelta
     970        @(bitvector_3_elim_prop … arg)
     971        whd in match bit_address_of_register; normalize nodelta
     972        @pair_elim #un #ln #un_ln_refl
     973        lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
     974        @(pair_replace ?????????? un_ln_refl)
     975        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
     976          whd in match get_8051_sfr; normalize nodelta
     977          whd in match sfr_8051_index; normalize nodelta
     978          @eq_f <status_of_pseudo_status_does_not_change_8051_sfrs
     979          >EQs
     980          [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
     981            /demod nohyps/ %
     982          |*:
     983            cases daemon
     984          ]
     985        |*:
     986          >low_internal_ram_of_pseudo_internal_ram_miss
     987          cases daemon
     988          (* XXX: require axioms about low_internal_ram_of_pseudo_low_internal_ram *)         
     989        ]
     990      |2,4:
     991        @pair_elim #nu #nl #nu_nl_refl
     992        lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
     993        @pair_elim #ignore #three_bits #ignore_three_bits_refl
     994        lapply (refl_to_jmrefl ??? ignore_three_bits_refl) -ignore_three_bits_refl #ignore_three_bits_refl
     995        inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     996        [1,3:
     997          @(pair_replace ?????????? ignore_three_bits_refl) try %
     998          >get_index_v_refl normalize nodelta >EQs %
     999        |2,4:
     1000          @(pair_replace ?????????? ignore_three_bits_refl) try %
     1001          >get_index_v_refl normalize nodelta >EQs
     1002          cases daemon
     1003          (* XXX: require axioms about low_internal_ram as above *)
     1004        ]
     1005      ]
    8471006    ]
    8481007    (* XXX: switch to the right hand side *)
     
    8521011    (* XXX: finally, prove the equality using sigma commutation *)
    8531012    @split_eq_status try %
    854     cases daemon
     1013    [1,2,3,19,20,21,28,29,30:
     1014      cases daemon (* XXX: axioms as above *)
     1015    |4,13,22,31:
     1016    |5,14,23,32:
     1017    |6,15,24,33:
     1018    |7,16,25,34:
     1019    |8,17,26,35:
     1020      whd in ⊢ (??%%);
     1021     
     1022    |9,18,27,36:
     1023      whd in ⊢ (??%%);
     1024      whd in match (ticks_of_instruction ?); <instr_refl
     1025      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
     1026    ]
    8551027  |2,4:
    8561028    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
Note: See TracChangeset for help on using the changeset viewer.