Ignore:
Timestamp:
Dec 7, 2012, 11:35:19 AM (7 years ago)
Author:
piccolo
Message:

finished stmt_at_sigma_commute

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2536 r2543  
    539539    return sigma_regs p p' graph_prog sigma gsss r2 prf2
    540540; save_frame_commute :
    541   ∀dest,st1,st2,prf1.
    542   save_frame ?? (p' ?) dest st1 = return st2 →
     541  ∀b,dest,st1,st2,prf1.
     542  save_frame ?? (p' ?) b dest st1 = return st2 →
    543543  let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1))
    544544    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
    545545  ∃prf2.
    546   save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
     546  save_frame ?? (p' ?) b dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
    547547; allocate_locals_commute :
    548548  ∀ loc, r1, prf1. ∃ prf2.
     
    981981   stmt_at … graph_code
    982982    lbl = return stmt →
    983  stmt_at ?? lin_code
    984   pt = return graph_to_lin_statement … stmt ∧
    985983  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
    986984 match stmt with
    987  [ final stmt ⇒ True
    988  | sequential stmt nxt ⇒
    989    (sigma nxt = Some ? (S pt) ∨
    990     (stmt_at ?? lin_code
    991      (S pt) = return final (mk_lin_params p) … (GOTO … nxt)))
     985 [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s')
     986 | sequential s' nxt ⇒
     987             match s' with
     988             [ step_seq _ ⇒
     989               (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧
     990                  ((sigma nxt = Some ? (S pt)) ∨
     991                   (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt)))
     992             | COND a ltrue ⇒
     993               (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧
     994               sigma nxt = Some ? (S pt)) ∨
     995               (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt))
     996             ]
     997 | FCOND abs _ _ _ ⇒ Ⓧabs   
    992998 ]. 
    993999 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
    9941000 * #_ #lin_stmt_spec #prf
    995 elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at
     1001elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec
    9961002#All_succs_in #next_spec
    997 #EQstmt_at_graph_stmt
    998 #stmt >EQstmt_at
    999 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    1000 % [ % assumption ]
    1001 cases stmt in next_spec; -stmt normalize nodelta [2: // ]
    1002 #stmt #nxt
    1003 whd in match opt_All;
    1004 whd in match stmt_implicit_label;
    1005 normalize nodelta //
     1003#stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ)
     1004% [assumption]
     1005//
    10061006qed.
    10071007 
     
    10971097  fetch_statement (make_sem_graph_params p p') …
    10981098    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    1099   fetch_statement (make_sem_lin_params p p') …
    1100     (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    1101   return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧
    11021099  All ? (λlbl.well_formed_pc p p' graph_prog sigma
    11031100      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
    1104     (stmt_explicit_labels … stmt) ∧
     1101    (stmt_explicit_labels … stmt) ∧ 
    11051102  match stmt with
    1106   [ sequential stmt nxt ⇒
    1107     ∃prf'.
    1108     let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
    1109     let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
    1110     (nxt_pc = sigma_nxt ∨
    1111      fetch_statement (make_sem_lin_params p p') …
    1112       (globalenv_noinit … lin_prog) nxt_pc =
    1113       return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
    1114   | final stmt ⇒ True
     1103  [  sequential s nxt ⇒
     1104        match s with
     1105        [ step_seq x ⇒
     1106          fetch_statement (make_sem_lin_params p p') …
     1107          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
     1108              return 〈f, \fst (linearise_int_fun … fn),
     1109                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
     1110          ∃prf'.
     1111            let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1112            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1113            (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
     1114             (globalenv_noinit … lin_prog) nxt_pc =
     1115             return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     1116        | COND a ltrue ⇒
     1117            (∃ prf'.
     1118            let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1119            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1120            (fetch_statement (make_sem_lin_params p p') …
     1121            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
     1122              return 〈f, \fst (linearise_int_fun … fn),
     1123                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
     1124             nxt_pc = sigma_nxt)) ∨
     1125             fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
     1126             =
     1127             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉
     1128         ]
     1129    | final z ⇒   fetch_statement (make_sem_lin_params p p') …
     1130                   (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
     1131                   return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉
     1132    | FCOND abs _ _ _ ⇒ Ⓧabs
    11151133  ].
    1116 #p #p' #graph_prog #pc #f #fn #stmt #sigma #good
    1117 elim (good fn) * #_ #all_labels_in #good_local #wfprf
    1118 #H
    1119 elim (fetch_statement_inv … H)
    1120 #fetchfn #graph_stmt
    1121 whd in match fetch_statement; normalize nodelta
    1122 >sigma_pblock_eq_lemma
     1134#p #p' #graph_prog #pc #f #fn #stmt #sigma
     1135#good elim (good fn) * #_ #all_labels_in #good_local #wfprf
     1136#H elim (fetch_statement_inv … H) #fetchfn #graph_stmt
     1137whd in match well_formed_pc in wfprf; normalize nodelta in wfprf;
     1138inversion(sigma_pc_opt p p' graph_prog sigma pc)
     1139[#ABS @⊥ >ABS in wfprf; * #H @H %]
     1140#lin_pc #lin_pc_spec
     1141whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec;
     1142@('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn
     1143#EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) -H
     1144#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
     1145lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt)
     1146[@lin_pt_spec|] * #H1 #H2 %
     1147[ -H2 @(All_mp … (All_append_r … H1)) #lab #lab_spec
     1148  whd in match well_formed_pc; normalize nodelta
     1149  whd in match sigma_pc_opt; normalize nodelta >fetchfn
     1150  >m_return_bind whd in match point_of_pc; whd in match pc_of_point;
     1151  normalize nodelta >point_of_offset_of_point
     1152  cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %]
     1153  #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?));
     1154  % #ABS destruct(ABS)
     1155] lapply H2
     1156cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     1157#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
     1158>sigma_pblock_eq_lemma
    11231159>(fetch_internal_function_transf … fetchfn) >m_return_bind
    1124 whd in match sigma_pc; normalize nodelta @opt_safe_elim
    1125 #lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta
    1126 >fetchfn in ⊢ (%→?); >m_return_bind
    1127 inversion (sigma ??)
    1128 [ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    1129 #lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
    1130 cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) *
    1131 #H1 #H2 #H3 % [ % ]
    1132 [ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
    1133   >H1 %
    1134 | @(All_mp … (All_append_r … H2)) #lbl #prf'
    1135  whd whd in match sigma_pc_opt; normalize nodelta
    1136  >fetchfn >m_return_bind >point_of_pc_of_point
    1137  >(opt_to_opt_safe … prf') % normalize
    1138  #ABS destruct(ABS)
    1139 | cases stmt in H2 H3; normalize nodelta [2: // ]
    1140   -stmt #stmt #nxt * #next_in #_ #nxt_spec
    1141   % 
    1142   [ @hide_prf whd %
    1143   | @opt_safe_elim #pc'
    1144   ]
    1145   >graph_succ_pc whd in ⊢ (??%?→?);
    1146   >fetchfn normalize nodelta >point_of_pc_of_point
    1147   >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1148   cases nxt_spec
    1149   [ #EQsigma_nxt %1
    1150     whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta
    1151     >point_of_offset_of_point lapply next_in >EQsigma_nxt #N %
    1152   | #EQstmt_at_nxt %2
    1153     whd in match (succ_pc ???);
    1154     >(fetch_internal_function_transf … fetchfn) >m_return_bind
    1155     whd in match point_of_pc;
    1156     normalize nodelta >point_of_offset_of_point >point_of_offset_of_point
    1157     whd in match (point_of_succ ???);
    1158     >EQstmt_at_nxt %
    1159   ]
    1160 ]
    1161 qed. 
     1160[ %
     1161   [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta
     1162     @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta
     1163    >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point
     1164    >(proj1 … H3) >m_return_bind //
     1165   |
     1166   %
     1167      [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt;
     1168        normalize nodelta lapply fetchfn
     1169        whd in match fetch_internal_function; normalize nodelta
     1170        #H4 @('bind_inversion H4) #x #x_spec
     1171        >x_spec >m_return_bind #EQ >EQ >m_return_bind
     1172        whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc;
     1173        whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
     1174        cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
     1175        lapply all_labels_spec #Z
     1176        lapply(All_nth ? ? 0 ? Z nxt) whd in match stmt_labels; normalize nodelta
     1177        #Z1 normalize in Z1; lapply(Z1 ?) [%] inversion(sigma ??)
     1178        [#_ #ABS @⊥ elim ABS #ABS @ABS %] #sn #sigma_graph_f_spec >sigma_graph_f_spec
     1179        #_ #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
     1180      | cases(proj2 … H3)
     1181        [ #Z %1 whd in match sigma_pc; normalize nodelta
     1182          @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta
     1183          >lin_pc_spec #EQ destruct(EQ)
     1184          @opt_safe_elim #pc2 >fetchfn >m_return_bind
     1185          whd in match point_of_pc; whd in match succ_pc; normalize nodelta
     1186          whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
     1187          >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ)
     1188          whd in match point_of_pc; whd in match point_of_succ; normalize nodelta
     1189          >point_of_offset_of_point %
     1190        | #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta
     1191          #H @('bind_inversion H) -H * #x1 #x2 #x_spec
     1192          lapply(fetch_function_transf ???? graph_prog
     1193            (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec)
     1194          #HH
     1195          <sigma_pblock_eq_lemma in HH; [2:@wfprf|||||] #HH >HH >m_return_bind
     1196          cases x2 normalize nodelta [#g_fun | #xxx] #EQ whd in EQ : (??%%); destruct(EQ)
     1197          >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta
     1198          whd in match pc_of_point; normalize nodelta  >point_of_offset_of_point
     1199          whd in match sigma_pc; normalize nodelta
     1200          @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
     1201          >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?);
     1202          destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1203           >Z >m_return_bind %
     1204         ]
     1205      ]
     1206   ]
     1207   | cases H3
     1208      [ * #Z1 #Z2 %1 % [ @hide_prf  whd in match well_formed_pc; normalize nodelta
     1209        whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
     1210        whd in match point_of_pc; whd in match succ_pc; normalize nodelta
     1211        whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
     1212        >Z2 >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
     1213      ] %
     1214      [ whd in match sigma_pc; normalize nodelta
     1215        @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
     1216        >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?);
     1217        destruct(EQ) whd in match point_of_pc; normalize nodelta
     1218        >point_of_offset_of_point >Z1 >m_return_bind %
     1219      | whd in match sigma_pc; normalize nodelta
     1220       @opt_safe_elim #line_pc
     1221       @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta
     1222       >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc;
     1223       normalize nodelta  >point_of_offset_of_point >Z2 >m_return_bind
     1224       #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind
     1225       #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc;
     1226       normalize nodelta >point_of_offset_of_point %
     1227       ]
     1228       | #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind
     1229         @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta
     1230         >fetchfn >m_return_bind >lin_pt_spec >m_return_bind
     1231         #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta
     1232         >point_of_offset_of_point >Z >m_return_bind %
     1233        ]
     1234   | whd in match sigma_pc; normalize nodelta @opt_safe_elim
     1235     #line_pc whd in match sigma_pc_opt; normalize nodelta  >fetchfn >m_return_bind
     1236      >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ)
     1237      whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1238      >H3 >m_return_bind %
     1239   ]
     1240   qed.
    11621241
    11631242lemma point_of_pc_sigma_commute :
     
    12021281#res #_
    12031282#H lapply (res_eq_from_opt ??? H) -H
    1204 cases daemon
    1205 (*#H elim (bind_inversion ????? H) in ⊢ ?;
    1206 * #f #stmt *
    1207 whd in ⊢ (??%?→?);*)
     1283#H  @('bind_inversion H) -H
     1284* #f #stmt
     1285whd in match fetch_statement; normalize nodelta
     1286#H @('bind_inversion H) -H *
     1287#id #int_f
     1288whd in match fetch_internal_function; normalize nodelta
     1289#H @('bind_inversion H) -H * #id1 #int_f1
     1290whd in match fetch_function; normalize nodelta
     1291#H lapply(opt_eq_from_res ???? H) -H
     1292#H @('bind_inversion H) -H #id2
     1293whd in match symbol_for_block; normalize nodelta
     1294whd in match option_map; normalize nodelta
     1295cases (find ?? (symbols ? ?) ?) normalize nodelta
     1296[1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ)
     1297#H @('bind_inversion H) -H #int_f2 whd in match find_funct_ptr;
     1298normalize nodelta cases(block_region (pc_block (pc ? ?)))
     1299normalize nodelta [1,3: #ABS destruct(ABS)]
     1300cases(block_id (pc_block (pc ??))) normalize nodelta
     1301[1,2,4,5: [2,4: #pos] #ABS destruct(ABS)]
     1302#pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ)
     1303cases int_f1 in int_f2_spec; normalize nodelta
     1304[2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1305#int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1306#H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H
     1307#stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1308cases (stmt) in stmt1_spec; normalize nodelta
     1309[1,3,4,6: [1,3: #js #jsucc #_ | 2,4: #a #b #c #d #_] #ABS whd in ABS : (???%);
     1310 destruct(ABS)]
     1311#fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta
     1312[1,3,4,6: [1,3: #l #_|2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)]
     1313#STMT_SPEC #H @('bind_inversion H) -H #state_pc #state_pc_sepc
     1314#H @('bind_inversion H) -H #succ_pc whd in match next_of_pc; normalize nodelta
     1315#H @('bind_inversion H) -H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta
     1316#H @('bind_inversion H) -H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta
     1317#H @('bind_inversion H) -H * #id6 #int_f6 whd in match fetch_function; normalize nodelta
     1318#H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id7
     1319whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta
     1320cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)]
     1321#sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) -H #int_f7
     1322whd in match find_funct_ptr; normalize nodelta
     1323cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)]
     1324cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)]
     1325#pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec;
     1326normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1327#int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1328#H @('bind_inversion H) -H #stmt2 #H lapply(opt_eq_from_res ???? H) -H
     1329#stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1330cases int_f4 in stmt2_spec; normalize nodelta
     1331[2,3,5,6:
     1332
     1333xxxxxxxxxxxxxx
     1334
    12081335qed.
    12091336
Note: See TracChangeset for help on using the changeset viewer.