Changeset 2269


Ignore:
Timestamp:
Jul 26, 2012, 3:29:15 PM (7 years ago)
Author:
sacerdot
Message:

Proof completely repaired up to write_at_stack_pointer_status_of_pseudo_status,
which is missing from the library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2267 r2269  
    5151qed.
    5252
     53(*CSC: move elsewhere*)
     54lemma bv_append_eq_to_eq:
     55 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
     56  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
     57 #A #n #v1 elim v1
     58 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
     59 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
     60   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
     61qed.
     62   
    5363theorem main_thm:
    5464  ∀M, M': internal_pseudo_address_map.
     
    102112      %{0}
    103113      whd in match execute_1_pseudo_instruction0; normalize nodelta
    104       change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
    105       whd in match (execute_1_pseudo_instruction0 ?????);
    106       (* XXX: work on the left hand side of the equality *)
    107       whd in ⊢ (??%?);
    108       @split_eq_status try %
    109       /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
     114      change with (status_of_pseudo_status ????? = ?)
     115      whd in ⊢ (??%%); @split_eq_status try %
     116      [ >set_clock_set_program_counter ]
     117      >program_counter_set_program_counter >sigma_increment_commutation @add_zero
    110118    |6: (* Mov *)
    111119      #arg1 #arg2 #_
     
    206214      whd in match (expand_pseudo_instruction ??????);
    207215      whd in match (execute_1_pseudo_instruction0 ?????);
     216      whd in match (ticks_of0 ??????);
    208217      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
    209218      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
     
    231240      [1:
    232241        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
    233         [ @eq_f2 try %
    234           cases daemon (*CSC*)
     242        [ @eq_f2 try % @sym_eq
     243          @(pose … (set_clock ????)) #status #status_refl @sym_eq >status_refl
     244          /demod nohyps/
     245          (*CSC: mess with get_8051_sfr_set_program_counter + missing high level lemmas*)
     246          cut (∀A,B:Type[0]. ∀f,g:A → B. ∀a:A. f=g → f a = g a) [#A #B #f #f #a * %] #eq_fun
     247          >(eq_fun ???? ? (get_8051_sfr_set_program_counter (BitVectorTrie Byte 16) … SFR_SP …))
     248          >(eq_fun ???? ? (get_8051_sfr_set_program_counter pseudo_assembly_program … SFR_SP …))
     249          whd in match get_8051_sfr; normalize nodelta whd in match status_of_pseudo_status;
     250          normalize nodelta whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     251          cases accM try % normalize nodelta #ul #addr cases (vsplit bool ???)
     252          normalize nodelta #v1 #v2 cases (eq_upper_lower ul upper) normalize nodelta
     253          >get_index_v_set_index_miss try % #abs normalize in abs; destruct(abs)
    235254        ] whd in ⊢ (??%?);
    236255        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
    237256        @(pair_replace ????? ?? ??? carry_new_sp_refl')
    238         [ @eq_f2 try %
    239           cases daemon (*CSC*)
     257        [ @eq_f2 try % @sym_eq
     258          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
     259          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
     260          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
    240261        ]
    241262        whd in ⊢ (??%?);
     
    243264        change with (set_program_counter ???? = ?)
    244265        @set_program_counter_status_of_pseudo_status
    245         [2: @sym_eq cases daemon (*@write_at_stack_pointer_status_of_pseudo_status try %
     266        [2: @sym_eq cases daemon (*CSC: missing @write_at_stack_pointer_status_of_pseudo_status try %
    246267          [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
    247268                  @sigma_increment_commutation
     
    263284        [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta
    264285            >create_label_cost_refl %
    265         |2:  
    266           cases daemon (*CSC: make a lemma here!*)
    267         ]
     286        |2: cases (bv_append_eq_to_eq … relevant3) #H #_ >H
     287            cases (conjunction_true … aj_possible_refl) #K #_ @sym_eq
     288            @eq_bv_eq assumption ]
    268289      | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
    269         [ @eq_f2 try % cases daemon ]
     290        [ @eq_f2 try %
     291          @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     292          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status)
     293          >status_refl -status_refl try %
     294          @sym_eq @set_clock_status_of_pseudo_status try %
     295          @sym_eq @set_program_counter_status_of_pseudo_status try % assumption ]
    270296        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
    271297        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
    272         [ @eq_f2 try % cases daemon ]
     298        [ @eq_f2 try % @sym_eq
     299          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
     300          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
     301          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) ]
    273302        change with (set_program_counter ???? = ?)
    274303        @set_program_counter_status_of_pseudo_status
     
    284313          >program_counter_set_8051_sfr >set_clock_set_program_counter
    285314          >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl
    286         @sym_eq
     315        @sym_eq (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
    287316        cases daemon
    288317      ]
Note: See TracChangeset for help on using the changeset viewer.