Changeset 2109


Ignore:
Timestamp:
Jun 26, 2012, 2:47:56 PM (5 years ago)
Author:
mulligan
Message:

Finished porting the large, main lemma to the new notion of jump expansion that we share with Jaap.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2108 r2109  
    904904    cases daemon
    905905  |2,4:
    906     XXX: here
    907     >EQppc
     906    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     907    [2, 4:
     908      cases daemon (* XXX: !!! *)
     909    ]
     910    normalize nodelta >EQppc
    908911    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    909912    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     
    917920      >EQstatus_after_1 in ⊢ (???%);
    918921      whd in ⊢ (???%);
    919       [1:exists_labelled_instruction id instr_list →
     922      [1:
    920923        <fetch_refl in ⊢ (???%);
    921924      |2:
     
    971974      (* XXX: switch to the right hand side *)
    972975      normalize nodelta >EQs -s >EQticks -ticks
    973       cases (¬ eq_bv ???) normalize nodelta
    974       whd in ⊢ (??%%);
     976      normalize nodelta whd in ⊢ (??%%);
    975977    ]
    976978    (* XXX: finally, prove the equality using sigma commutation *)
     
    988990
    989991  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    990   whd in match (expand_relative_jump ????);
    991992  <EQppc in fetch_many_assm;
     993  whd in match (short_jump_cond ??);
     994  @pair_elim #sj_possible #disp
    992995  @pair_elim #result #flags #sub16_refl
    993996  @pair_elim #upper #lower #vsplit_refl
    994   inversion (eq_bv ???) #upper_vsplit_refl normalize nodelta
     997  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     998  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    995999  [1,3:
    9961000    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1001    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     1002    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    9971003    whd in ⊢ (??%?);
    9981004    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     
    10191025    ]
    10201026  |2,4:
    1021     >EQppc
     1027    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     1028    [2, 4:
     1029      cases daemon (* XXX: !!! *)
     1030    ]
     1031    normalize nodelta >EQppc
    10221032    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    10231033    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     
    10901100 
    10911101  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    1092   whd in match (expand_relative_jump ????);
    10931102  <EQppc in fetch_many_assm;
     1103  whd in match (short_jump_cond ??);
     1104  @pair_elim #sj_possible #disp
    10941105  @pair_elim #result #flags #sub16_refl
    10951106  @pair_elim #upper #lower #vsplit_refl
    1096   cases (eq_bv ???) normalize nodelta
     1107  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     1108  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    10971109  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    10981110    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1111    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     1112    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    10991113    whd in ⊢ (??%?);
    11001114    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     
    11111125    cases daemon
    11121126  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1113     >EQppc
     1127    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
     1128    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1129      cases daemon (* XXX: !!! *)
     1130    ]
     1131    normalize nodelta >EQppc
    11141132    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    11151133    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     
    12411259  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    12421260  whd in ⊢ (??%?);
     1261  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    12431262  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    12441263  (* XXX: work on the left hand side *)
     
    14091428  ]
    14101429qed.
    1411 *)
Note: See TracChangeset for help on using the changeset viewer.