Changeset 2143


Ignore:
Timestamp:
Jul 2, 2012, 11:37:34 AM (5 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.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2139 r2143  
    403403qed.
    404404
     405(* XXX: move back into ASM.ma *)
     406lemma subvector_with_to_subvector_with_tl:
     407  ∀n: nat.
     408  ∀m: nat.
     409  ∀v.
     410  ∀fixed_v.
     411  ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v).
     412  ∀n': nat.
     413  ∀hd: addressing_mode_tag.
     414  ∀tl: Vector addressing_mode_tag n'.
     415  ∀m_refl: S n'=n.
     416  ∀v_refl: v≃hd:::tl.
     417   subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v.
     418  #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl
     419  generalize in match proof; destruct
     420  whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     421  cases (mem … eq_a ? fixed_v hd) normalize nodelta
     422  [1:
     423    whd in match (subvector_with … eq_a tl fixed_v);
     424    #assm assumption
     425  |2:
     426    normalize in ⊢ (% → ?);
     427    #absurd cases absurd
     428  ]
     429qed.
    405430
    406431let rec subaddressing_mode_elim_type
     
    437462  ] (refl … n) (refl_jmeq … v).
    438463  [20:
    439     generalize in match proof; destruct
    440     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    441     cases (mem … eq_a ? fixed_v hd) normalize nodelta
    442     [1:
    443       whd in match (subvector_with … eq_a tl fixed_v);
    444       #assm assumption
    445     |2:
    446       normalize in ⊢ (% → ?);
    447       #absurd cases absurd
    448     ]
     464    @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl)
    449465  ]
    450466  @(is_in_subvector_is_in_supervector … proof)
     
    460476  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
    461477   subaddressing_mode_elim_type n v addr Q m w H.
    462  #n #v #addr #Q #m #w elim w
    463  [ /2/
    464  | #n' #hd #tl #IH cases hd #H
    465    #INV whd #PO @IH #xaddr cases xaddr *
    466    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
    467    @ALREADYSEEN ]
     478  #n #v #addr #Q #m #w elim w
     479  [1:
     480    /2/
     481  |2:
     482    #n' #hd #tl #IH cases hd #H
     483    #INV whd #PO @IH #xaddr cases xaddr *
     484    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
     485    @ALREADYSEEN
     486  ]
    468487qed.
    469488
     
    474493  ∀Q: v → Prop.
    475494   subaddressing_mode_elim_type n v addr Q (S n) v ?.
    476 [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
    477 | @subvector_with_refl @eq_a_reflexive
    478 ]
     495  [1:
     496    #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
     497  |2:
     498    @subvector_with_refl @eq_a_reflexive
     499  ]
    479500qed.
    480501 
  • src/ASM/AssemblyProof.ma

    r2142 r2143  
    340340qed.
    341341
     342lemma m_lt_1_to_m_refl_0:
     343  ∀m: nat.
     344    m < 1 → m = 0.
     345  #m cases m try (#irrelevant %)
     346  #m' whd in ⊢ (% → ?); #relevant
     347  lapply (le_S_S_to_le … relevant)
     348  change with (? < ? → ?) -relevant #relevant
     349  cases (lt_to_not_zero … relevant)
     350qed.
     351
    342352(*CSC: move elsewhere*)         
    343353axiom lt_to_lt_nat_of_bitvector_add:
    344  ∀n,v,m1,m2.
    345   m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
    346    nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
    347    nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     354  ∀n,v,m1,m2.
     355    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
     356      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
     357      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
    348358
    349359(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
     
    645655      (external_ram … ps)
    646656      pc
    647       (special_function_registers_8051 … ps)
     657      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
    648658      (special_function_registers_8052 … ps)
    649659      (p1_latch … ps)
     
    764774*)
    765775
     776(* XXX: check values returned for conditional jumps below! *)
    766777definition ticks_of0:
    767778    ∀p:pseudo_assembly_program.
     
    775786    [ Instruction instr ⇒
    776787      match instr with
    777       [ JC lbl ⇒ ? (*
    778         match pol lookup_labels ppc with
    779         [ short_jump ⇒ 〈2, 2〉
    780         | absolute_jump ⇒ ?
    781         | long_jump ⇒ 〈4, 4〉
    782         ] *)
    783       | JNC lbl ⇒ ? (*
    784         match pol lookup_labels ppc with
    785         [ short_jump ⇒ 〈2, 2〉
    786         | absolute_jump ⇒ ?
    787         | long_jump ⇒ 〈4, 4〉
    788         ] *)
    789       | JB bit lbl ⇒ ? (*
    790         match pol lookup_labels ppc with
    791         [ short_jump ⇒ 〈2, 2〉
    792         | absolute_jump ⇒ ?
    793         | long_jump ⇒ 〈4, 4〉
    794         ] *)
    795       | JNB bit lbl ⇒ ? (*
    796         match pol lookup_labels ppc with
    797         [ short_jump ⇒ 〈2, 2〉
    798         | absolute_jump ⇒ ?
    799         | long_jump ⇒ 〈4, 4〉
    800         ] *)
    801       | JBC bit lbl ⇒ ? (*
    802         match pol lookup_labels ppc with
    803         [ short_jump ⇒ 〈2, 2〉
    804         | absolute_jump ⇒ ?
    805         | long_jump ⇒ 〈4, 4〉
    806         ] *)
    807       | JZ lbl ⇒ ? (*
    808         match pol lookup_labels ppc with
    809         [ short_jump ⇒ 〈2, 2〉
    810         | absolute_jump ⇒ ?
    811         | long_jump ⇒ 〈4, 4〉
    812         ] *)
    813       | JNZ lbl ⇒ ? (*
    814         match pol lookup_labels  ppc with
    815         [ short_jump ⇒ 〈2, 2〉
    816         | absolute_jump ⇒ ?
    817         | long_jump ⇒ 〈4, 4〉
    818         ] *)
    819       | CJNE arg lbl ⇒ ? (*
    820         match pol lookup_labels ppc with
    821         [ short_jump ⇒ 〈2, 2〉
    822         | absolute_jump ⇒ ?
    823         | long_jump ⇒ 〈4, 4〉
    824         ] *)
    825       | DJNZ arg lbl ⇒ ? (*
    826         match pol lookup_labels ppc with
    827         [ short_jump ⇒ 〈2, 2〉
    828         | absolute_jump ⇒ ?
    829         | long_jump ⇒ 〈4, 4〉
    830         ] *)
     788      [ JC lbl ⇒
     789        if policy ppc then
     790          〈4, 4〉
     791        else
     792          〈2, 2〉
     793      | JNC lbl ⇒
     794        if policy ppc then
     795          〈4, 4〉
     796        else
     797          〈2, 2〉
     798      | JB bit lbl ⇒
     799        if policy ppc then
     800          〈4, 4〉
     801        else
     802          〈2, 2〉
     803      | JNB bit lbl ⇒
     804        if policy ppc then
     805          〈4, 4〉
     806        else
     807          〈2, 2〉
     808      | JBC bit lbl ⇒
     809        if policy ppc then
     810          〈4, 4〉
     811        else
     812          〈2, 2〉
     813      | JZ lbl ⇒
     814        if policy ppc then
     815          〈4, 4〉
     816        else
     817          〈2, 2〉
     818      | JNZ lbl ⇒
     819        if policy ppc then
     820          〈4, 4〉
     821        else
     822          〈2, 2〉
     823      | CJNE arg lbl ⇒
     824        if policy ppc then
     825          〈4, 4〉
     826        else
     827          〈2, 2〉
     828      | DJNZ arg lbl ⇒
     829        if policy ppc then
     830          〈4, 4〉
     831        else
     832          〈2, 2〉
    831833      | ADD arg1 arg2 ⇒
    832834        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     
    916918    | Comment comment ⇒ 〈0, 0〉
    917919    | Cost cost ⇒ 〈0, 0〉
    918     | Jmp jmp ⇒ 〈2, 2〉
    919     | Call call ⇒ 〈2, 2〉
     920    | Jmp jmp ⇒
     921      if policy ppc then
     922        〈4, 4〉
     923      else
     924        〈2, 2〉
     925    | Call call ⇒
     926      if policy ppc then
     927        〈4, 4〉
     928      else
     929        〈2, 2〉
    920930    | Mov dptr tgt ⇒ 〈2, 2〉
    921931    ].
    922     cases daemon
    923 qed.
    924932
    925933definition ticks_of:
  • 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.