Changeset 2209


Ignore:
Timestamp:
Jul 18, 2012, 2:56:12 PM (5 years ago)
Author:
mulligan
Message:

Closed major daemons in the supporting lemmas of the main lemma.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2197 r2209  
    473473         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    474474    | INDIRECT i ⇒
    475        let d ≝ get_register … s [[false;false;i]] in
    476        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
     475        let d ≝ get_register … s [[false;false;i]] in
     476        let address ≝ bit_address_of_register … s [[false;false;i]] in
     477          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
     478            ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    477479    | EXT_INDIRECT _ ⇒ true
    478480    | REGISTER r ⇒
  • src/ASM/AssemblyProofSplit.ma

    r2207 r2209  
    9898qed.
    9999
    100 lemma lookup_low_internal_ram_false:
    101   ∀cm: pseudo_assembly_program.
    102   ∀status.
    103   ∀b, b': BitVector 7.
    104     b = b' →
    105     lookup … b (low_internal_ram … cm status) (zero 8) = false:::b'.
    106   #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter
    107   #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b #b' #b_refl
    108   cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *)
    109 qed.
    110 
    111100lemma sfr_psw_eq_to_bit_address_of_register_eq:
    112101  ∀A: Type[0].
     
    148137    #_
    149138    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    150     whd in match get_register; normalize nodelta
    151     cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false
    152     @sfr_psw_eq_to_bit_address_of_register_eq assumption (* XXX: dubious *)
     139    <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption
    153140  ]
    154141qed.
    155 (* XXX: indirect case false above *)
    156142
     143lemma not_b_c_to_b_not_c:
     144  ∀b, c: bool.
     145    (¬b) = c → b = (¬c).
     146  //
     147qed.
     148(* XXX: move above elsewhere *)
     149
     150lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
     151  ∀M.
     152  ∀sigma.
     153  ∀sfr8051.
     154  ∀b.
     155    sfr8051 ≠ SFR_ACC_A →
     156      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
     157  #M #sigma * #b
     158  [18:
     159    #relevant cases (absurd … (refl ??) relevant)
     160  ]
     161  #_ %
     162qed.
     163
     164lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
     165  ∀M.
     166  ∀sigma: Word → Word.
     167  ∀w: BitVector 8.
     168  ∀b.
     169    w ≠ bitvector_of_nat … 224 →
     170      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
     171  #M #sigma #w #b #w_neq_assm
     172  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
     173  [1:
     174    #sfr_of_Byte_refl %
     175  |2:
     176    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
     177    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
     178    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
     179    @(absurd ?? w_neq_assm)
     180    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
     181    whd in match sfr_of_Byte; normalize nodelta
     182    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     183    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     184    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     185    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     186    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     187    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     188    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     189    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     190    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     191    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     192    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     193    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     194    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     195    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     196    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     197    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     198    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     199    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     200    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     201    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     202    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     203    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     204    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     205    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     206    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
     207    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     208    #absurd destruct(absurd)
     209qed.
     210
     211lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
     212  ∀M, sigma, w, b.
     213    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
     214      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
     215  #M #sigma #w #b #assoc_list_exists_assm
     216  whd in ⊢ (??%?);
     217  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
     218qed.
     219   
    157220lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
    158221  ∀M', cm.
     
    184247      normalize nodelta %
    185248    |4:
    186       #_
     249      #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm)
     250      -assoc_list_exists_assm #assoc_list_exists_assm
    187251      <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
    188       >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     252      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)
    189253      normalize nodelta %
    190254    ]
    191255  |3:
    192256    #w whd in ⊢ (??%? → ??%?);
    193     cases daemon (* XXX: ??? *)
     257    @eq_bv_elim #eq_bv_refl normalize nodelta
     258    [1:
     259      #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)
     260      #assoc_list_exists_refl #eq_accumulator_refl
     261      >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b)
     262      whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl)
     263      %
     264    |2:
     265      #assoc_list_exists_assm
     266      @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     267      cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl
     268      <head_head' inversion bit #bit_refl normalize nodelta
     269      >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl;
     270      [1:
     271        @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption
     272      |2:
     273        @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map
     274        <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)
     275      ]
     276    ]
    194277  |5,6:
    195278    #w #_ %
     
    700783      change with (set_arg_8 ????? = ?)
    701784      @set_arg_8_status_of_pseudo_status try %
    702       [ @sym_eq @set_clock_status_of_pseudo_status
    703         [ @sym_eq >EQs @set_program_counter_status_of_pseudo_status %
    704         | >EQs >EQticks <instr_refl >addr_refl @eq_f2 %
    705         ]
    706       | @(subaddressing_mode_elim … acc_a) @I
    707       | >EQs >EQticks <instr_refl >addr_refl
     785      >EQs >EQticks <instr_refl >addr_refl
     786      [1:
     787        @sym_eq @set_clock_status_of_pseudo_status
     788        [1:
     789          @sym_eq @set_program_counter_status_of_pseudo_status %
     790        |2:
     791          @eq_f2 %
     792        ]
     793      |2:
     794        @(subaddressing_mode_elim … acc_a) @I
     795      |3:
    708796        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    709797        [1:
    710798          @(subaddressing_mode_elim … acc_a) %
    711         |2:
    712           %
    713         |3:
    714           %
    715799        |4:
    716800          @eq_f2
     
    719803          [1:
    720804            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    721             [1:
    722               @(subaddressing_mode_elim … acc_a) %
    723             |*:
    724               %
    725             ]
     805            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
    726806          |3:
    727807            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    728             [1:
    729               /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
    730             |*:
    731               %
    732             ]
     808            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    733809          |2:
    734810            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    735             [1:
    736               @(subaddressing_mode_elim … acc_a) %
    737             |2:
    738               %
    739             ]
     811            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
    740812          |4:
    741813            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    742             [1:
    743               /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
    744             |*:
    745               %
    746             ]
     814            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
    747815          ]
     816        |*:
     817          %
    748818        ]
    749819      ]
Note: See TracChangeset for help on using the changeset viewer.