Ignore:
Timestamp:
May 17, 2012, 5:45:21 PM (8 years ago)
Author:
mulligan
Message:

Progress made on main_thm proof: trying to find a pattern to use across all ~150 goals

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1963 r1966  
    33include alias "basics/logic.ma".
    44
    5 axiom add_commutative:
    6   ∀n: nat.
    7   ∀l, r: BitVector n.
    8     add … l r = add … r l.
     5lemma set_arg_16_mk_Status_commutation:
     6  ∀M: Type[0].
     7  ∀cm: M.
     8  ∀s: PreStatus M cm.
     9  ∀w: Word.
     10  ∀d: [[dptr]].
     11    set_arg_16 M cm s w d =
     12      mk_PreStatus M cm
     13        (low_internal_ram … s)
     14        (high_internal_ram … s)
     15        (external_ram … s)
     16        (program_counter … s)
     17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
     18        (special_function_registers_8052 … s)
     19        (p1_latch … s)
     20        (p3_latch … s)
     21        (clock … s).
     22  #M #cm #s #w #d
     23  whd in match set_arg_16; normalize nodelta
     24  whd in match set_arg_16'; normalize nodelta
     25  @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
     26  cases (split bool 8 8 w) #bu #bl normalize nodelta
     27  whd in match set_8051_sfr; normalize nodelta %
     28qed.
     29
     30lemma set_program_counter_mk_Status_commutation:
     31  ∀M: Type[0].
     32  ∀cm: M.
     33  ∀s: PreStatus M cm.
     34  ∀w: Word.
     35    set_program_counter M cm s w =
     36      mk_PreStatus M cm
     37        (low_internal_ram … s)
     38        (high_internal_ram … s)
     39        (external_ram … s)
     40        w
     41        (special_function_registers_8051 … s)
     42        (special_function_registers_8052 … s)
     43        (p1_latch … s)
     44        (p3_latch … s)
     45        (clock … s).
     46  //
     47qed.       
     48
     49lemma set_clock_mk_Status_commutation:
     50  ∀M: Type[0].
     51  ∀cm: M.
     52  ∀s: PreStatus M cm.
     53  ∀c: nat.
     54    set_clock M cm s c =
     55      mk_PreStatus M cm
     56        (low_internal_ram … s)
     57        (high_internal_ram … s)
     58        (external_ram … s)
     59        (program_counter … s)
     60        (special_function_registers_8051 … s)
     61        (special_function_registers_8052 … s)
     62        (p1_latch … s)
     63        (p3_latch … s)
     64        c.
     65  //
     66qed.
     67
     68
     69lemma special_function_registers_8051_set_arg_16:
     70  ∀M, M': Type[0].
     71  ∀cm: M.
     72  ∀cm': M'.
     73  ∀s: PreStatus M cm.
     74  ∀s': PreStatus M' cm'.
     75  ∀w, w': Word.
     76  ∀d, d': [[dptr]].
     77  (∀sfr: SFR8051.
     78    sfr ≠ SFR_DPH → sfr ≠ SFR_DPL →
     79      get_8051_sfr M cm s sfr = get_8051_sfr M' cm' s' sfr) →
     80        w = w' →
     81          special_function_registers_8051 ?? (set_arg_16 … s w d) =
     82            special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
     83  #M #M' #cm #cm' #s #s' #w #w' #d
     84  cases daemon
     85qed.
     86
    987
    1088theorem main_thm:
    1189  ∀M.
    1290  ∀M'.
    13   ∀cm.
    14   ∀ps.
    15   ∀sigma.
    16   ∀policy.
    17     next_internal_pseudo_address_map M cm ps = Some … M' →
     91  ∀program: pseudo_assembly_program.
     92  ∀sigma: Word → Word.
     93  ∀policy: Word → bool.
     94  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
     95  ∀ps: PseudoStatus program.
     96    next_internal_pseudo_address_map M program ps = Some … M' →
    1897      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    1998        status_of_pseudo_status M' …
    20           (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
    21   #M #M' * #preamble #instr_list #ps #sigma #policy
     99          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
     100  #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
    22101  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    23102  @(pose … (program_counter ?? ps)) #ppc #EQppc
    24   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
    25   @pair_elim #labels #costs #H0 normalize nodelta
    26   @pair_elim #assembled #costs' #EQ1 normalize nodelta
    27   @pair_elim #pi #newppc #EQ2 normalize nodelta
     103  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
     104  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
     105  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
     106  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
     107  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
    28108  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
    29109  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    30110  whd in match execute_1_pseudo_instruction; normalize nodelta
    31   whd in match ticks_of; normalize nodelta <EQppc >EQ2 normalize nodelta
    32   lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
    33   lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    34   [1: >EQ2 %
    35   |2:
    36   |3: normalize nodelta
     111  whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
     112  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
     113  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     114  [1: >fetch_pseudo_refl % ]
     115  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
     116  generalize in match assm1; -assm1 -assm2 -assm3
     117  normalize nodelta
    37118  cases pi
    38119  [2,3:
    39     #ARG
    40     #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
    41     #H2
    42     whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
     120    #arg
     121    (* XXX: we first work on sigma_increment_commutation *)
     122    #sigma_increment_commutation
     123    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     124    (* XXX: we work on the maps *)
     125    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     126    (* XXX: we assume the fetch_many hypothesis *)
     127    #fetch_many_assm
     128    (* XXX: we give the existential *)
     129    %{0}
    43130    whd in match (execute_1_pseudo_instruction0 ?????);
    44     %{0} @split_eq_status //
    45     [1,2: /demod/ >EQnewppc >H3 <add_zero % (*CSC: auto not working, why? *) ]
    46   |6: (* Mov *) #arg1 #arg2
     131    (* XXX: work on the left hand side of the equality *)
     132    whd in ⊢ (??%?);
     133    @split_eq_status //
     134    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
     135  |6: (* Mov *)
     136    #arg1 #arg2
     137    (* XXX: we first work on sigma_increment_commutation *)
     138    #sigma_increment_commutation
     139    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     140    (* XXX: we work on the maps *)
     141    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     142    (* XXX: we assume the fetch_many hypothesis *)
     143    #fetch_many_assm
     144    (* XXX: we give the existential *)
     145    %{1}
     146    whd in match (execute_1_pseudo_instruction0 ?????);
     147    (* XXX: work on the left hand side of the equality *)
     148    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     149    (* XXX: execute fetches some more *)
     150    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     151    whd in fetch_many_assm;
     152    >EQassembled in fetch_many_assm;
     153    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
     154    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
     155    #fetch_many_assm whd in fetch_many_assm;
     156    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     157    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
     158    (* XXX: now we start to work on the mk_PreStatus equality *)
     159    change with (set_arg_16 ????? = ?)
     160    >set_program_counter_mk_Status_commutation
     161    >set_clock_mk_Status_commutation
     162    >set_arg_16_mk_Status_commutation
     163   
     164    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
     165    >set_program_counter_mk_Status_commutation
     166    >set_clock_mk_Status_commutation
     167    >set_arg_16_mk_Status_commutation in ⊢ (???%);
     168   
     169   
     170    @split_eq_status //
     171    [1:
     172      assumption
     173    |2:
     174      @special_function_registers_8051_set_arg_16
     175      [2:
     176         >EQlookup_datalabels %
     177      |1:
     178        *
     179        #absurd1 #absurd2
     180        try (@⊥ cases absurd1 -absurd #absurd1 @absurd1 %)
     181        try (@⊥ cases absurd2 -absurd #absurd2 @absurd2 %)
     182        whd in ⊢ (??%%); cases daemon (* XXX: not nice! manipulation of vectors; true though *)
     183      ]
     184    ]
     185
     186(* 
     187    @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1 whd in ⊢ (??%?);
     188    whd in match (get_arg_16 ????); whd in match (set_arg_16' ?????);
     189 
     190    @split_eq_status 
     191   
     192   
     193    #fetch_many_assm
     194    >assembly_refl in fetch_many_assm;
     195   
     196    cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
     197    whd in ⊢ (??%?);   
     198   
     199   
    47200      #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
    48201      #H2
     
    70223       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    71224
    72 
     225*)
    73226
    74227  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
     
    130283              @low_internal_ram_write_at_stack_pointer
    131284               [ >EQ0 @pol | % | %
    132                | @(pair_destruct_2 … EQ1)
     285               | @(  … EQ1)
    133286               | @(pair_destruct_2 … EQ2)
    134287               | >(pair_destruct_1 ????? EQpc)
Note: See TracChangeset for help on using the changeset viewer.