Changeset 2528 for src/joint


Ignore:
Timestamp:
Dec 4, 2012, 9:05:52 AM (7 years ago)
Author:
piccolo
Message:

added cases PUSH, C_ADDRESS and COPACCS

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2507 r2528  
    360360λp,p',graph_prog,sigma,gsss,st,prf.
    361361mk_state …
    362   (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))
    363   (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))
     362  (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?)
     363  (sigma_is p p' graph_prog sigma (istack … st) ?)
    364364  (carry … st)
    365   (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf)))
    366   (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)).
     365  (sigma_regs … gsss (regs … st) ?)
     366  (sigma_mem p p' graph_prog sigma (m … st) ?).
     367@hide_prf
     368[ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))
     369| @(proj2 … (proj1 … prf)) | @(proj2 … prf)]
     370qed.
    367371
    368372
     
    11401144cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
    11411145#EQ >EQ //
     1146qed.
     1147
     1148lemma is_push_sigma_commute :
     1149∀ p, p', graph_prog,sigma,gss,st,val,is,prf1,prf2.
     1150(is_push (istack … st) val=return is) →
     1151∃prf3.
     1152is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1))
     1153        (sigma_beval p p' graph_prog sigma val prf2) =
     1154return sigma_is p p' graph_prog sigma is prf3.
     1155#p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H
     1156%
     1157[ @hide_prf
     1158whd in match sigma_is_opt; normalize nodelta
     1159inversion (istack ? ?) in H;
     1160whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1161[2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta
     1162inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %]
     1163[2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
     1164#val' #_
     1165inversion(sigma_beval_opt ???? a)
     1166  [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)]
     1167#ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec
     1168whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); *
     1169#EQ @EQ %
     1170]
     1171whd in match sigma_state; normalize nodelta
     1172cut(is_push (istack (make_sem_graph_params p p') st) val=return is)
     1173[ assumption] 
     1174#H1 whd in match sigma_is; normalize nodelta
     1175@opt_safe_elim #is1 #is1_spec
     1176whd in match sigma_beval; normalize nodelta
     1177@opt_safe_elim #sigma_val #sigma_val_sepc
     1178@opt_safe_elim #sigma_is #sigma_is_spec
     1179inversion(istack ? st)
     1180[2: #val1|3:#val1 #val2]
     1181#H2 >H2 in H1;
     1182whd in match is_push; normalize nodelta
     1183#EQ whd in EQ : (??%%); destruct(EQ)
     1184>H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta
     1185#EQ whd in EQ : (??%?); destruct(EQ)
     1186normalize nodelta
     1187whd in match sigma_is_opt in sigma_is_spec;
     1188normalize nodelta in sigma_is_spec;
     1189>sigma_val_sepc in sigma_is_spec;
     1190[ inversion(sigma_beval_opt ???? val1)
     1191[ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1) | #sigma_val1 #H3 >m_return_bind]]
     1192>m_return_bind
     1193#EQ whd in EQ : (??%?); destruct(EQ) [2: %]
     1194>H3 in EQ;
     1195normalize nodelta
     1196#EQ1 whd in EQ1 : (??%%); destruct(EQ1)
     1197normalize nodelta //
     1198qed.
     1199
     1200lemma beopaccs_sigma_commute :
     1201∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2.
     1202∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?.
     1203∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?.
     1204be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 →
     1205∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?.
     1206∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?.
     1207be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) =
     1208return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉.
     1209#p #p' #graph_prog #sigma #op #val1 #val2
     1210#opaccs1 #opaccs2 #prf1 #prf2
     1211whd in match be_opaccs; normalize nodelta
     1212#H elim(bind_inversion ????? H) -H
     1213#x * #x_spec
     1214#H elim(bind_inversion ????? H) -H
     1215#y * #y_spec
     1216#H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H;
     1217#b1 #b2 #EQ normalize in EQ; destruct(EQ)
     1218%
     1219[whd in match sigma_beval_opt; normalize nodelta % #ABS
     1220whd in ABS : (??%?); destruct(ABS)]
     1221%
     1222[whd in match sigma_beval_opt; normalize nodelta % #ABS
     1223whd in ABS : (??%?); destruct(ABS)]
     1224whd in match sigma_beval; normalize nodelta
     1225@opt_safe_elim #sigma_val1 #sigma_val1_spec
     1226@opt_safe_elim #sigma_val2 #sigma_val2_spec
     1227@opt_safe_elim #sigma_op1 #sigma_op1_spec
     1228@opt_safe_elim #sigma_op2 #sigma_op2_spec
     1229lapply x_spec -x_spec lapply sigma_val1_spec -sigma_val1_spec
     1230inversion val1 whd in match Byte_of_val; normalize nodelta
     1231[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
     1232[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1233#bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta
     1234whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ)
     1235#EQ whd in EQ : (???%); destruct(EQ)
     1236lapply y_spec -y_spec lapply sigma_val2_spec -sigma_val2_spec
     1237inversion val2 whd in match Byte_of_val; normalize nodelta
     1238[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
     1239[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1240#bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta
     1241whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta
     1242#EQ whd in EQ : (???%); destruct(EQ)
     1243>m_return_bind >m_return_bind
     1244whd in match sigma_beval_opt in sigma_op1_spec;
     1245normalize nodelta in sigma_op1_spec;
     1246whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec)
     1247whd in match sigma_beval_opt in sigma_op2_spec;
     1248normalize nodelta in sigma_op2_spec;
     1249whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec)
     1250>H1 %
    11421251qed.
    11431252
     
    12841393          inversion(sigma_beval_opt ???? y)
    12851394          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
    1286           xxxxxxxxxxxxxxxxxx
    1287        
    1288  qed.       
    1289        
     1395           whd in match sigma_is_opt; >H normalize nodelta >ABS
     1396           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
     1397          | #sigma_y #H >m_return_bind
     1398            cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %]
     1399            #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H)
     1400          ]
     1401        | #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ)
     1402          ]
     1403        ]
     1404     |
     1405        whd in match helper_def_retrieve in acca_arg_retrieve_commute;
     1406        normalize nodelta in acca_arg_retrieve_commute;
     1407        whd in match acca_arg_retrieve; normalize nodelta
     1408        @err_eq_to_io
     1409        change with
     1410        ((! v ← (acca_arg_retrieve_ p
     1411                                      (joint_closed_internal_function (make_sem_lin_params p p'))
     1412                                      (make_sem_lin_params p p')
     1413                                      (regs (make_sem_lin_params p p')
     1414                                         (sigma_state p p' graph_prog sigma gss st prf))
     1415                                      a);
     1416          ?)=?)
     1417          change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?)
     1418          cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf)
     1419          [4: assumption | | | | ] #H >H >m_return_bind
     1420          whd in match push; normalize nodelta
     1421          -H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec)
     1422          #wf_is #EQ >EQ >m_return_bind //
     1423     ]
     1424  | (*C_ADDRESS*)
     1425    #sy
     1426    change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
     1427    #sy_prf
     1428    change with ((dpl_reg p) → ?) #dpl 
     1429    change with ((dph_reg p) → ?) #dph
     1430    #H lapply(err_eq_from_io ????? H) -H
     1431    change with ((( ! st1 ← dpl_store p
     1432                                     (joint_closed_internal_function (make_sem_graph_params p p'))
     1433                                     (make_sem_graph_params p p')
     1434                                     ?
     1435                                     ?
     1436                                     ? ; ? ) = ?) → ?)
     1437    change with ((( ! st1 ← dpl_store ????
     1438    (BVptr
     1439      (mk_pointer
     1440         (opt_safe block
     1441           (find_symbol
     1442              (fundef
     1443                 (joint_closed_internal_function
     1444                    (make_sem_graph_params p p')
     1445                    ?
     1446                  )
     1447               )
     1448               (globalenv_noinit ? graph_prog)
     1449               ?
     1450           )
     1451           ?
     1452         )
     1453         ?
     1454      )
     1455      ?
     1456    ) ? ; ?) = ?) → ?)
     1457    change with ((( ! st1 ← ? ;
     1458        dph_store p (joint_closed_internal_function (make_sem_graph_params p p'))
     1459                  (make_sem_graph_params p p') ?
     1460                  (BVptr
     1461      (mk_pointer
     1462         (opt_safe block
     1463           (find_symbol
     1464              (fundef
     1465                 (joint_closed_internal_function
     1466                    (make_sem_graph_params p p')
     1467                    ?
     1468                  )
     1469               )
     1470               (globalenv_noinit ? graph_prog)
     1471               ?
     1472           )
     1473           ?
     1474         )
     1475         ?
     1476      )
     1477      ?
     1478    ) ?) = ?) → ?)
     1479    #H elim(bind_inversion ????? H) -H
     1480    #st1 * #dpl_st1
     1481    elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1)
     1482    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); %
     1483        #ABS destruct(ABS)]
     1484    #wf_st1 whd in match helper_def_store; normalize nodelta
     1485    #H elim(bind_inversion ????? H) -H #reg1 * #reg1_spec #EQ whd in EQ : (??%%);
     1486    destruct(EQ) -EQ
     1487    #dph_st'
     1488    elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st')
     1489    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?));
     1490        % #ABS destruct(ABS)]
     1491    #wf_st' whd in match helper_def_store; normalize nodelta
     1492    #H elim(bind_inversion ????? H) -H #reg2 * #reg2_spec #EQ whd in EQ : (??%%);
     1493    destruct(EQ) -EQ %{wf_st'} <e1
     1494    whd in match dpl_store; normalize nodelta
     1495    whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec;
     1496    whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec;
     1497    lapply reg1_spec -reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?);
     1498    destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec
     1499    #reg1_spec @opt_safe_elim #block_lin #block_lin_spec
     1500    cut(find_symbol
     1501         (fundef
     1502            (joint_closed_internal_function
     1503                (make_sem_lin_params p p')
     1504                (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog))
     1505            )
     1506          )
     1507          (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog))
     1508          sy
     1509          =
     1510          find_symbol
     1511            (fundef
     1512               (joint_closed_internal_function
     1513                   (make_sem_graph_params p p')
     1514                   (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)
     1515               )
     1516            )
     1517            (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog)
     1518            sy)   
     1519    [ @find_symbol_transf]
     1520    #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec
     1521    #EQ destruct(EQ) >reg1_spec >m_return_bind
     1522    whd in match dph_store; normalize nodelta
     1523    lapply reg2_spec -reg2_spec
     1524    whd in match sigma_beval; normalize nodelta
     1525    @opt_safe_elim #y
     1526    whd in match sigma_beval_opt; normalize nodelta
     1527    whd in ⊢((??%?)→?); #EQ destruct(EQ)
     1528    @opt_safe_elim #graph_block >block_graph_spec
     1529    #EQ destruct(EQ) #reg2_spec
     1530    cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 =
     1531    (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
     1532          reg1 (sigma_state p p' graph_prog sigma gss st prf)))
     1533    [whd in match set_regs; normalize nodelta >e0 %]
     1534    #sigma_st1_spec <sigma_st1_spec >reg2_spec
     1535    >m_return_bind %
     1536  | (*C_OPACCS*)
     1537    #op #a #b #arg1 #arg2
     1538    #H lapply(err_eq_from_io ????? H) -H
     1539    #H elim(bind_inversion ????? H) -H
     1540    #val1 * #val1_spec
     1541    elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec)
     1542    #wf_val1 #sigma_val1_commute
     1543    #H elim(bind_inversion ????? H) -H
     1544    #val2 * #val2_spec
     1545    elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec)
     1546    #wf_val2 #sigma_val2_commute
     1547    #H elim(bind_inversion ????? H) -H *
     1548    #opaccs1 #opaccs2 * #opaccs_spec
     1549    elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec)
     1550    #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute
     1551    #H elim(bind_inversion ????? H) -H
     1552    #st1 * #st1_spec
     1553    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec)
     1554    #wf_st1 #sigma_st1_commute #final_spec
     1555    elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec)
     1556    #wf_st' #sigma_final_commute
     1557    %{wf_st'}
     1558    whd in match helper_def_retrieve in sigma_val1_commute;
     1559    normalize nodelta in sigma_val1_commute;
     1560    whd in match acca_arg_retrieve; normalize nodelta
     1561    >sigma_val1_commute >m_return_bind
     1562    whd in match helper_def_retrieve in sigma_val2_commute;
     1563    normalize nodelta in sigma_val2_commute;
     1564    whd in match accb_arg_retrieve; normalize nodelta
     1565    >sigma_val2_commute >m_return_bind
     1566    >be_opaccs_commute >m_return_bind
     1567    whd in match helper_def_store in sigma_st1_commute;
     1568    normalize nodelta in sigma_st1_commute;
     1569    elim(bind_inversion ????? sigma_st1_commute)
     1570    #reg1 * #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1571    whd in match acca_store; normalize nodelta
     1572    >reg1_spec >m_return_bind
     1573    whd in match set_regs; normalize nodelta >e0
     1574    whd in match helper_def_store in sigma_final_commute;
     1575    normalize nodelta in sigma_final_commute;
     1576    elim(bind_inversion ????? sigma_final_commute)
     1577    #reg2 * #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1578    whd in match accb_store; normalize nodelta
     1579    >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta
     1580    >e1 %
     1581  | (*C_OP1*)
     1582   
    12901583inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    12911584    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
Note: See TracChangeset for help on using the changeset viewer.