Changeset 2536


Ignore:
Timestamp:
Dec 6, 2012, 1:18:35 PM (7 years ago)
Author:
piccolo
Message:

finished eval_seq_no_pc_sigma_commute lemma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2529 r2536  
    511511  retrieve … (sigma_regs … gsss r prf1) a
    512512     = return sigma_beval p p' graph_prog sigma bv prf2.
    513  
     513
     514
    514515record good_state_sigma
    515516  (p : unserialized_params)
     
    537538  pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv =
    538539    return sigma_regs p p' graph_prog sigma gsss r2 prf2
    539 ; allocate_locals_commute :
    540   ∀ loc, r1, prf1. ∃ prf2.
    541   allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
    542   sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
    543540; save_frame_commute :
    544541  ∀dest,st1,st2,prf1.
     
    548545  ∃prf2.
    549546  save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
     547; allocate_locals_commute :
     548  ∀ loc, r1, prf1. ∃ prf2.
     549  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
     550  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
    550551; eval_ext_seq_commute :
    551552  let lin_prog ≝ linearise p graph_prog in
    552   ∀stack_sizes.
     553  ∀ stack_sizes.
    553554  ∀ext,i,fn,st1,st2,prf1.
    554555  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     
    596597            return mk_state_pc ? st2' pc'
    597598}.
     599
     600
     601
     602
    598603
    599604lemma store_commute :
     
    12601265
    12611266lemma is_push_sigma_commute :
    1262 ∀ p, p', graph_prog,sigma,gss,st,val,is,prf1,prf2.
    1263 (is_push (istack … st) val=return is) →
     1267∀ p, p', graph_prog,sigma,is,val,is',prf1,prf2.
     1268(is_push is val=return is') →
    12641269∃prf3.
    1265 is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1))
    1266         (sigma_beval p p' graph_prog sigma val prf2) =
    1267 return sigma_is p p' graph_prog sigma is prf3.
    1268 #p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H
     1270is_push (sigma_is p p' graph_prog sigma is prf1)
     1271  (sigma_beval p p' graph_prog sigma val prf2) =
     1272return sigma_is p p' graph_prog sigma is' prf3.
     1273#p #p' #graph_prog #sigma *
     1274[ | #bv1 | #bv1 #bv2 ] #val #is' #prf1 #prf2
     1275whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1276whd in match sigma_beval; normalize nodelta
     1277@opt_safe_elim #val' #EQsigma_val
    12691278%
    1270 [ @hide_prf
     1279[1,3: @hide_prf %
     1280|*: whd in match sigma_is in ⊢ (???%); normalize nodelta
     1281  @opt_safe_elim #is''
     1282] whd in match sigma_is_opt; normalize nodelta
     1283[2,4:
     1284  inversion (sigma_beval_opt ?????)
     1285  [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1;
     1286    normalize nodelta * #H @H % ]
     1287  #bv1' #EQ_bv1' >m_return_bind ]
     1288>EQsigma_val
     1289whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1290whd in match sigma_is; normalize nodelta
     1291@opt_safe_elim #is1
    12711292whd in match sigma_is_opt; normalize nodelta
    1272 inversion (istack ? ?) in H;
    1273 whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1274 [2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta
    1275 inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %]
    1276 [2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
    1277 #val' #_
    1278 inversion(sigma_beval_opt ???? a)
    1279   [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)]
    1280 #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec
    1281 whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); *
    1282 #EQ @EQ %
    1283 ]
    1284 whd in match sigma_state; normalize nodelta
    1285 cut(is_push (istack (make_sem_graph_params p p') st) val=return is)
    1286 [ assumption] 
    1287 #H1 whd in match sigma_is; normalize nodelta
    1288 @opt_safe_elim #is1 #is1_spec
    1289 whd in match sigma_beval; normalize nodelta
    1290 @opt_safe_elim #sigma_val #sigma_val_sepc
    1291 @opt_safe_elim #sigma_is #sigma_is_spec
    1292 inversion(istack ? st)
    1293 [2: #val1|3:#val1 #val2]
    1294 #H2 >H2 in H1;
    1295 whd in match is_push; normalize nodelta
    1296 #EQ whd in EQ : (??%%); destruct(EQ)
    1297 >H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta
    1298 #EQ whd in EQ : (??%?); destruct(EQ)
    1299 normalize nodelta
    1300 whd in match sigma_is_opt in sigma_is_spec;
    1301 normalize nodelta in sigma_is_spec;
    1302 >sigma_val_sepc in sigma_is_spec;
    1303 [ inversion(sigma_beval_opt ???? val1)
    1304 [ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1) | #sigma_val1 #H3 >m_return_bind]]
    1305 >m_return_bind
    1306 #EQ whd in EQ : (??%?); destruct(EQ) [2: %]
    1307 >H3 in EQ;
    1308 normalize nodelta
    1309 #EQ1 whd in EQ1 : (??%%); destruct(EQ1)
    1310 normalize nodelta //
     1293[ #H @('bind_inversion H) #bv1''
     1294  >EQ_bv1' #EQ destruct(EQ) ]
     1295whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    13111296qed.
    13121297
     
    13201305be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) =
    13211306return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉.
    1322 #p #p' #graph_prog #sigma #op #val1 #val2
    1323 #opaccs1 #opaccs2 #prf1 #prf2
    1324 whd in match be_opaccs; normalize nodelta
    1325 #H elim(bind_inversion ????? H) -H
    1326 #x * #x_spec
    1327 #H elim(bind_inversion ????? H) -H
    1328 #y * #y_spec
    1329 #H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H;
    1330 #b1 #b2 #EQ normalize in EQ; destruct(EQ)
    1331 %
    1332 [whd in match sigma_beval_opt; normalize nodelta % #ABS
    1333 whd in ABS : (??%?); destruct(ABS)]
    1334 %
    1335 [whd in match sigma_beval_opt; normalize nodelta % #ABS
    1336 whd in ABS : (??%?); destruct(ABS)]
     1307#p #p' #graph_prog #sigma #op
     1308@bv_pc_other
     1309[ #pc1 #p1 #val2
     1310| #val1 #val1_no_pc @bv_pc_other
     1311  [ #pc #p | #val2 #val2_no_pc ]
     1312
     1313#opaccs1 #opaccs2
     1314#prf1 #prf2
     1315[1,2: [2: #H @('bind_inversion H) #by1 #_ ]
     1316  whd in ⊢ (??%%→?); #EQ destruct]
     1317#EQ
     1318>(sigma_bv_no_pc … val1_no_pc)
     1319>(sigma_bv_no_pc … val2_no_pc)
     1320cut (bv_no_pc opaccs1 ∧ bv_no_pc opaccs2)
     1321[ cases val1 in EQ; cases daemon ] *
     1322#H1 #H2 @('bind_inversion EQ) #bt #bt_spec
     1323#H3 @('bind_inversion H3) #bt'
     1324#bt_spec' cases (opaccs eval op bt bt')
     1325#ev_bt #ev_bt' normalize nodelta
     1326#EQ1 whd in EQ1 : (??%%); destruct(EQ1)
     1327% [ whd in match sigma_beval_opt ; normalize nodelta %
     1328#ABS whd in ABS : (??%?); destruct(ABS) ]
     1329% [ whd in match sigma_beval_opt ; normalize nodelta %
     1330#ABS whd in ABS : (??%?); destruct(ABS) ]
     1331>(sigma_bv_no_pc … H1)
     1332>(sigma_bv_no_pc … H2) assumption
     1333qed.
     1334
     1335lemma sigma_ptr_commute :
     1336∀ p, p', graph_prog , sigma , val1, val2, ptr, prf1, prf2.
     1337pointer_of_address 〈val1,val2〉= return ptr →
     1338pointer_of_address 〈sigma_beval p p' graph_prog sigma val1 prf1,
     1339                    sigma_beval p p' graph_prog sigma val2 prf2〉 = return ptr.
     1340#p #p' #graph_prog #sigma #val1 #val2 #ptr #prf1 #prf2
    13371341whd in match sigma_beval; normalize nodelta
    13381342@opt_safe_elim #sigma_val1 #sigma_val1_spec
    1339 @opt_safe_elim #sigma_val2 #sigma_val2_spec
    1340 @opt_safe_elim #sigma_op1 #sigma_op1_spec
    1341 @opt_safe_elim #sigma_op2 #sigma_op2_spec
    1342 lapply x_spec -x_spec lapply sigma_val1_spec -sigma_val1_spec
    1343 inversion val1 whd in match Byte_of_val; normalize nodelta
    1344 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
    1345 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1346 #bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta
    1347 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ)
    1348 #EQ whd in EQ : (???%); destruct(EQ)
    1349 lapply y_spec -y_spec lapply sigma_val2_spec -sigma_val2_spec
    1350 inversion val2 whd in match Byte_of_val; normalize nodelta
    1351 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
    1352 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1353 #bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta
    1354 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta
    1355 #EQ whd in EQ : (???%); destruct(EQ)
    1356 >m_return_bind >m_return_bind
    1357 whd in match sigma_beval_opt in sigma_op1_spec;
    1358 normalize nodelta in sigma_op1_spec;
    1359 whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec)
    1360 whd in match sigma_beval_opt in sigma_op2_spec;
    1361 normalize nodelta in sigma_op2_spec;
    1362 whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec)
    1363 >H1 %
    1364 qed.
     1343@opt_safe_elim #sigma_Val2 #sigma_val2_spec
     1344whd in match pointer_of_address; whd in match pointer_of_bevals;
     1345normalize nodelta cases val1 in sigma_val1_spec; normalize nodelta
     1346  [1,2,3,4,5: [|| #ptr1 #ptr2 #p | #by | #p] #_ #ABS whd in ABS : (??%%); destruct(ABS)
     1347  |   #ptr2 #p2 whd in match sigma_beval_opt; normalize nodelta
     1348      #EQ whd in EQ : (??%%); destruct(EQ) cases val2 in sigma_val2_spec; normalize nodelta
     1349      [1,2,3,4,5: [|| #ptr1 #ptr2 #p | #by | #p] #_ #ABS whd in ABS : (??%%); destruct(ABS)
     1350      |  #ptr1 #p1 whd in match sigma_beval_opt; normalize nodelta
     1351         #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta //
     1352      | #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)
     1353      ]
     1354  |   #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)
     1355  ]
     1356skip
     1357qed.
     1358 
    13651359
    13661360lemma eval_seq_no_pc_sigma_commute :
     
    13771371    f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
    13781372  return sigma_state … gss st' prf'.
    1379   #p #p' #graph_prog #stack_sizes #sigma #gss
     1373  #p #p' #graph_prog #stack_sizes #sigma #gss #f
    13801374  #fn #st #stmt
    13811375  #st' #prf
    1382   whd in match eval_seq_no_pc;
     1376  whd in match eval_seq_no_pc; 
    13831377  cases stmt normalize nodelta
    13841378  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
    1385   | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
    1386     change with
    1387      (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p'))
    1388                       (make_sem_graph_params p p') ??) in H : (??%?);
    1389     lapply H -H
    1390     whd in match pair_reg_move; normalize nodelta #H
    1391     elim(bind_inversion ????? H) -H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1379  | (* MOVE *) #mv_sig #H
     1380    whd in match pair_reg_move; normalize nodelta
     1381    @('bind_inversion H) -H #reg #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
    13921382    elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec)
    13931383    #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %]
     
    13991389      ]
    14001390  | (* POP *)
    1401     #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
    1402     * #val #st1 * #vals_spec #H
    1403     change with (acca_store p
    1404                           (joint_closed_internal_function (make_sem_graph_params p p'))
    1405                           (make_sem_graph_params p p') a val st1 = ?) in H;
    1406     change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec;
     1391    #a #H @('bind_inversion H) -H
     1392    * #val #st1 #vals_spec #H
    14071393    lapply vals_spec -vals_spec
    14081394    whd in match pop; normalize nodelta
     
    14381424     ] 
    14391425     #prf' #acca_store_commute %{prf'}     
    1440     whd in match sigma_state in ⊢ (??(????(?????(?????%?)?))?);
     1426    whd in match sigma_state in ⊢ (??(?????(?????%?)?)?);
    14411427    whd in match sigma_is; normalize nodelta
    14421428    @opt_safe_elim #int_stack #int_stack_sigma_spec
    14431429    >is_stack_st_spec in int_stack_sigma_spec;
    14441430    whd in match sigma_is_opt; normalize nodelta
    1445     #IS_SPEC elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
    1446     [ #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1447     | #sigma_bv_not_used * #sigma_bv_not_used_spec #IS_SPEC
    1448       elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
    1449       #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
     1431    #IS_SPEC @('bind_inversion IS_SPEC) -IS_SPEC
     1432    [ #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1433    | #sigma_bv_not_used #sigma_bv_not_used_spec #IS_SPEC
     1434      @('bind_inversion IS_SPEC) -IS_SPEC
     1435      #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
    14501436      normalize nodelta >m_return_bind
    1451       @err_eq_to_io <acca_store_commute
    1452       whd in match helper_def_store; normalize nodelta
    1453       whd in match acca_store; normalize nodelta
     1437      <acca_store_commute
     1438      whd in match helper_def_store;  whd in match acca_store;
    14541439      whd in match sigma_beval; normalize nodelta
    14551440     @opt_safe_elim #xx #xx_spec
     
    14591444       change with (return set_regs (make_sem_lin_params p p') ?
    14601445                                   (set_istack (make_sem_lin_params p p') ? ?) = ?);
    1461        change with (? = return set_regs ? ?
    1462                    (sigma_state p p' graph_prog sigma gss
    1463                    (set_istack ? (one_is Bv_not_used) st) ?))
    14641446       >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)
    14651447       [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec
     
    14671449     ]
    14681450  | (* PUSH *)
    1469      #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
    1470      #val *
    1471      change with (((acca_arg_retrieve p
    1472                 (joint_closed_internal_function (make_sem_graph_params p p'))
    1473                  (make_sem_graph_params p p') st a) = ?) → ?)
    1474      #graph_ret_spec
     1451     #a #H @('bind_inversion H) -H
     1452     #val  #graph_ret_spec
    14751453     change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?)
    14761454     #graph_push_spec
     
    14781456     #val_wf #acca_arg_retrieve_commute
    14791457     whd in match push in graph_push_spec; normalize nodelta  in graph_push_spec;
    1480      elim(bind_inversion ????? graph_push_spec) -graph_push_spec
    1481      #int_stack * #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1458     @('bind_inversion graph_push_spec) -graph_push_spec
     1459     #int_stack #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
    14821460     %
    14831461     [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]]
     
    15021480          whd in match sigma_is_opt; normalize nodelta
    15031481          inversion(sigma_beval_opt ???? y)
    1504           [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
    1505          xxxxxxxxxxxxxxxxxx
    1506        
    1507  qed.       
    1508 
    1509 lemma eval_statement_no_pc_sigma_commute :
    1510  ∀p,p',graph_prog.
    1511  let lin_prog ≝ linearise p graph_prog in
    1512  ∀stack_sizes.
    1513  ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
    1514  ∀f,fn,st,stmt,st'.
    1515  ∀prf : well_formed_state … gss st.
    1516   eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    1517    f fn stmt st = return st' →
    1518   ∃prf'.
    1519   eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    1520     f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
    1521        (sigma_state … gss st prf) =
    1522   return sigma_state … gss st' prf'.
    1523   #p #p' #graph_prog #stack_sizes #sigma #gss
    1524   #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
    1525   #st' #prf
    1526   whd in match eval_statement_no_pc; normalize nodelta
    1527   [ @eval_seq_no_pc_sigma_commute
    1528   |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    1529   | (* tailcall, follow proof of CALL in previous lemma *)
    1530     cases daemon
    1531   ]
    1532 qed.
    1533 
    1534 =======
     1482          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))     
    15351483           whd in match sigma_is_opt; >H normalize nodelta >ABS
    15361484           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
     
    15421490          ]
    15431491        ]
    1544      |
    1545         whd in match helper_def_retrieve in acca_arg_retrieve_commute;
    1546         normalize nodelta in acca_arg_retrieve_commute;
    1547         whd in match acca_arg_retrieve; normalize nodelta
    1548         @err_eq_to_io
    1549         change with
    1550         ((! v ← (acca_arg_retrieve_ p
    1551                                       (joint_closed_internal_function (make_sem_lin_params p p'))
    1552                                       (make_sem_lin_params p p')
    1553                                       (regs (make_sem_lin_params p p')
    1554                                          (sigma_state p p' graph_prog sigma gss st prf))
    1555                                       a);
    1556           ?)=?)
    1557           change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?)
    1558           cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf)
    1559           [4: assumption | | | | ] #H >H >m_return_bind
    1560           whd in match push; normalize nodelta
    1561           -H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec)
    1562           #wf_is #EQ >EQ >m_return_bind //
     1492     | change with (acca_arg_retrieve ????? = ?) in acca_arg_retrieve_commute;
     1493       >acca_arg_retrieve_commute in ⊢ (??%?); >m_return_bind
     1494       elim(is_push_sigma_commute … (proj2 … (proj1 …(proj1 … prf))) val_wf int_stack_spec)
     1495          #wf_is #EQ whd in match push; normalize nodelta >EQ %
    15631496     ]
    15641497  | (*C_ADDRESS*)
    1565     #sy 
    1566     change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
     1498    #sy
     1499    change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
    15671500    #sy_prf
    15681501    change with ((dpl_reg p) → ?) #dpl 
    15691502    change with ((dph_reg p) → ?) #dph
    1570     #H lapply(err_eq_from_io ????? H) -H
    15711503    change with ((( ! st1 ← dpl_store p
    15721504                                     (joint_closed_internal_function (make_sem_graph_params p p'))
    1573                                      (make_sem_graph_params p p')
     1505                                     ?
    15741506                                     ?
    15751507                                     ?
     
    15971529    change with ((( ! st1 ← ? ;
    15981530        dph_store p (joint_closed_internal_function (make_sem_graph_params p p'))
    1599                   (make_sem_graph_params p p') ?
     1531                  ? ?
    16001532                  (BVptr
    16011533      (mk_pointer
     
    16171549      ?
    16181550    ) ?) = ?) → ?)
    1619     #H elim(bind_inversion ????? H) -H
    1620     #st1 * #dpl_st1
     1551    #H @('bind_inversion H) -H
     1552    #st1 #dpl_st1
    16211553    elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1)
    16221554    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); %
    16231555        #ABS destruct(ABS)]
    16241556    #wf_st1 whd in match helper_def_store; normalize nodelta
    1625     #H elim(bind_inversion ????? H) -H #reg1 * #reg1_spec #EQ whd in EQ : (??%%);
     1557    #H @('bind_inversion H) -H #reg1 #reg1_spec #EQ whd in EQ : (??%%);
    16261558    destruct(EQ) -EQ
    16271559    #dph_st'
     
    16301562        % #ABS destruct(ABS)]
    16311563    #wf_st' whd in match helper_def_store; normalize nodelta
    1632     #H elim(bind_inversion ????? H) -H #reg2 * #reg2_spec #EQ whd in EQ : (??%%);
     1564    #H @('bind_inversion H) -H #reg2 #reg2_spec #EQ whd in EQ : (??%%);
    16331565    destruct(EQ) -EQ %{wf_st'} <e1
    16341566    whd in match dpl_store; normalize nodelta
     
    16761608  | (*C_OPACCS*)
    16771609    #op #a #b #arg1 #arg2
    1678     #H lapply(err_eq_from_io ????? H) -H
    1679     #H elim(bind_inversion ????? H) -H
    1680     #val1 * #val1_spec
     1610    #H @('bind_inversion H) -H
     1611    #val1 #val1_spec
    16811612    elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec)
    16821613    #wf_val1 #sigma_val1_commute
    1683     #H elim(bind_inversion ????? H) -H
    1684     #val2 * #val2_spec
     1614    #H @('bind_inversion H) -H #val2 #val2_spec
    16851615    elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec)
    16861616    #wf_val2 #sigma_val2_commute
    1687     #H elim(bind_inversion ????? H) -H *
    1688     #opaccs1 #opaccs2 * #opaccs_spec
     1617    #H @('bind_inversion H) -H *
     1618    #opaccs1 #opaccs2 #opaccs_spec
    16891619    elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec)
    16901620    #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute
    1691     #H elim(bind_inversion ????? H) -H
    1692     #st1 * #st1_spec
     1621    #H @('bind_inversion H) -H #st1 #st1_spec
    16931622    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec)
    16941623    #wf_st1 #sigma_st1_commute #final_spec
     
    17071636    whd in match helper_def_store in sigma_st1_commute;
    17081637    normalize nodelta in sigma_st1_commute;
    1709     elim(bind_inversion ????? sigma_st1_commute)
    1710     #reg1 * #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1638    @('bind_inversion sigma_st1_commute)
     1639    #reg1 #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
    17111640    whd in match acca_store; normalize nodelta
    17121641    >reg1_spec >m_return_bind
     
    17141643    whd in match helper_def_store in sigma_final_commute;
    17151644    normalize nodelta in sigma_final_commute;
    1716     elim(bind_inversion ????? sigma_final_commute)
    1717     #reg2 * #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1645    @('bind_inversion sigma_final_commute)
     1646    #reg2 #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
    17181647    whd in match accb_store; normalize nodelta
    17191648    >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta
    17201649    >e1 %
    17211650  | (*C_OP1*)
     1651    #op #a #arg #H @('bind_inversion H) -H #val1 #val1_spec
     1652    elim (retrieve_commute p p' graph_prog sigma ?? ? (acca_retrieve_commute … gss) ??? prf val1_spec)
     1653    #wf_val1 #sigma_val1_commute #H @('bind_inversion H) #op_val1 #op_val1_spec
     1654    cut(∃ wf_opval1. be_op1 op (sigma_beval … wf_val1) = return sigma_beval p p' graph_prog sigma op_val1 wf_opval1)
     1655    [ whd in match be_op1 in op_val1_spec; normalize nodelta in op_val1_spec;
     1656      @('bind_inversion op_val1_spec) #bt1 #b1_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1657      % [ @hide_prf whd in match sigma_beval_opt; normalize nodelta % #ABS whd in ABS : (??%?);
     1658          destruct(ABS)]
     1659      whd in match Byte_of_val in b1_spec; normalize nodelta in b1_spec;
     1660      whd in match sigma_beval; normalize nodelta
     1661      @opt_safe_elim #sigma_val1 #sigma_val1_spec
     1662      @opt_safe_elim #sigma_op_val1 #sigma_op_val1_spec
     1663      cases(val1) in b1_spec op_val1_spec sigma_val1_spec; normalize nodelta
     1664      [4: #bt2  #EQ whd in EQ : (???%); destruct(EQ)
     1665          whd in match Byte_of_val; normalize nodelta >m_return_bind
     1666          #EQ whd in EQ : (??%%); destruct(EQ)
     1667          whd in match sigma_beval_opt; normalize nodelta
     1668          #EQ whd in EQ : (??%%); destruct(EQ)
     1669          whd in match sigma_beval_opt in sigma_op_val1_spec;
     1670          normalize nodelta in sigma_op_val1_spec; whd in sigma_op_val1_spec : (??%?);
     1671          destruct(sigma_op_val1_spec) //
     1672      |*: [3: #pt1 #pt2 #p] [4:#p] [5:#pt #p] [6:#pc #p] #ABS whd in ABS : (???%);
     1673          destruct(ABS)
     1674      ]
     1675    ] * #wf_op_val1 #sigma_op_val1_commute #H1
     1676    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_op_val1 H1)
     1677    #wf_st' #final_commute %{wf_st'}
     1678    change with (acca_retrieve ????? = ?) in sigma_val1_commute;
     1679    >sigma_val1_commute >m_return_bind >sigma_op_val1_commute >m_return_bind
     1680    assumption
     1681  | (*C_OP2*)
     1682     #op #a #arg1 #arg2 #H @('bind_inversion H) -H
     1683     @bv_pc_other (*val1*)
     1684     [ #pc_val1 #part_val1
     1685     | #val1 #val1_no_pc
     1686     ] #val1_spec
     1687     #H @('bind_inversion H) -H
     1688     [ #val2
     1689     | @bv_pc_other (*val2*)
     1690       [ #pc_val2 #part_val2
     1691       | #val2 #val2_no_pc
     1692       ]
     1693     ] #val2_spec
     1694     #H @('bind_inversion H) -H * #val3 #bit1
     1695     [1,2: [2: cases val1 [||#pt1 #pt2 #p|#by|#p|#pt #p|#pc #p] cases op ]
     1696       whd in ⊢(??%%→?); #EQ destruct(EQ) ]
     1697     #H cut (bv_no_pc val3)
     1698      [ lapply H -H
     1699        whd in match be_op2; normalize nodelta
     1700        cases val1 normalize nodelta
     1701        [1,7: [2: #pc #p] #ABS whd in ABS : (???%); destruct(ABS)
     1702        |2,3,5: [ |#pt1 #pt2 #p | #p ] cases op normalize nodelta
     1703          [1,2,3,4,6,7,8,9,10,12,13,14,15,16,17 : #ABS whd in ABS : (???%); destruct(ABS)]
     1704          cases val2 normalize nodelta
     1705          [1,2,3,4,5,6,7,8,9,12,13,14,15,16,17,18,21 :
     1706            [||#ptr1 #ptr2 #p| #byte2 | #p | #ptr #p | #pc #p | | | #p| #ptr #p | #pc #p | | | #pt1 #pt2 #p | #bt | #pc #p] 
     1707            #EQ whd in EQ : (??%%); destruct(EQ) //
     1708          | #pt3 #pt4 #p1 @if_elim [2: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
     1709            #_ @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1710          | #bt @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1711            #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1712          | #p3 @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1713            #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1714          | #ptt #part @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1715            #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1716          ]
     1717        |4,6: [ #bt1 | #ptr #p] cases val2 normalize nodelta
     1718          [1,3,4,5,7,8,9,10,14: [|#pt1 #pt2 #p
     1719                              | #bt2 #H @('bind_inversion H) #bit #bit_spec cases(op2 ? ? ? ? ?)
     1720                                #x #y normalize nodelta
     1721                              | #p | #pc #part | | | #ptr #ptr' #p| #pc #p]
     1722                 #EQ whd in EQ : (??%%); destruct(EQ) //
     1723          |*: [|#ptr #p| #bt | #p | #ptr #p ] cases op normalize nodelta
     1724              [1,2,3,4,5,6,9,10,11,12,16,17,18,19,20,21,22,23,25,26,28,29:
     1725                 #EQ whd in EQ : (??%%); destruct(EQ) //
     1726              |7,8,13,14,15: whd in match be_add_sub_byte; normalize nodelta
     1727                cases(ptype ?) normalize nodelta [2,4,6,8,10: #ABS whd in ABS : (??%%); destruct(ABS)]
     1728                cases p * normalize nodelta #n_part_spec [2,6: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
     1729                [1,2,4,5,7 : #H @('bind_inversion H) #bit #bit_spec
     1730                       @if_elim [1,3,5,7,9: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
     1731                       #_ elim(op2 ? ? ? ? ?) #a1 #a2 normalize nodelta
     1732                       #EQ whd in EQ : (??%%); destruct(EQ) //
     1733                |*: #_ cases(carry ? st) normalize nodelta
     1734                  [1,2,4,5,7,8 : [1,3,5: #bool ] #ABS whd in ABS : (???%); destruct(ABS)]
     1735                  #bool #pt #p1 #bitvect @if_elim #_ [2,4,6: #ABS whd in ABS : (???%); destruct(ABS)]
     1736                  @If_elim [2,4,6: #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1737                  #proof elim(op2_bytes ?????) #a #b
     1738                  normalize nodelta #EQ whd in EQ : (???%); destruct(EQ) //
     1739                ]
     1740              |24,30: @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1741              | cases(ptype ?) normalize nodelta [2: #ABS whd in ABS : (???%); destruct(ABS)]
     1742                @if_elim #_ [2: #ABS whd in ABS : (??%%); destruct(ABS)]
     1743                #H @('bind_inversion H) #b #_ elim(op2 ?????) #x #y normalize nodelta
     1744                #EQ whd in EQ : (??%%); destruct(EQ) //
     1745              ]
     1746          ]
     1747        ]
     1748      ] #val3_spec lapply H -H #val3_op_spec #H @('bind_inversion H) #st1
     1749        #st1_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1750        elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val1_spec)
     1751        #wf_val1 #sigma_val1_commute
     1752        elim(retrieve_commute p p' graph_prog sigma ?? ? (snd_arg_retrieve_commute … gss) ??? prf val2_spec)
     1753        #wf_val2 #sigma_val2_commute
     1754       
     1755        elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf ? st1_spec)
     1756        [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta inversion val3 normalize nodelta
     1757          [7: #pc #p #H >H in val3_spec; #ABS @⊥ //
     1758          |*: [||#pt1 #pt2 #p|#bt|#p|#pt #p] #_ % #ABS whd in ABS : (??%%); destruct(ABS)
     1759          ]
     1760        ]
     1761        #wf_st1 #sigma_st1_commute   
     1762        %
     1763        [ @hide_prf % [2: @(proj2 … wf_st1)] % [2: @(proj2 … (proj1 … wf_st1))]
     1764          % [2:@(proj2 … (proj1 … (proj1 … wf_st1)))] 
     1765          @(proj1 … (proj1 … (proj1 … wf_st1)))
     1766        ]
     1767         change with ((acca_arg_retrieve ?????)=?) in sigma_val1_commute;
     1768         >sigma_val1_commute >m_return_bind
     1769         change with ((snd_arg_retrieve ?????)=?) in sigma_val2_commute;
     1770         >sigma_val2_commute >m_return_bind
     1771         >(sigma_bv_no_pc … val1_no_pc) >(sigma_bv_no_pc … val2_no_pc)
     1772         whd in match sigma_state in ⊢ (??(?????%?)?); normalize nodelta
     1773        >val3_op_spec >m_return_bind
     1774        change with ((acca_store ??????) = ?) in sigma_st1_commute;
     1775        >(sigma_bv_no_pc … val3_spec) in sigma_st1_commute;
     1776        #H >H >m_return_bind //
     1777  | (*C_CLEAR_CARRY*)
     1778     #EQ whd in EQ : (??%%); destruct(EQ)
     1779     %{prf} //
     1780  | (*C_SET_CARRY*)
     1781    #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
     1782  | (*C_LOAD*)
     1783    #a #dpl #dph #H @('bind_inversion H) -H #val1 #val1_spec
     1784    #H @('bind_inversion H) -H #val2 #val2_spec
     1785    #H @('bind_inversion H) -H #ptr #ptr_spec
     1786    #H @('bind_inversion H) -H #val3 #val3_spec #final_spec
     1787    elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec)
     1788    #wf_val1 #sigma_val1_commute
     1789    elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec)
     1790    #wf_val2 #sigma_val2_commute
     1791    lapply(opt_eq_from_res ???? val3_spec) -val3_spec #val3_spec
     1792    elim(beloadv_sigma_commute p p' graph_prog sigma ???? val3_spec)
     1793    [2: @hide_prf @(proj2 … prf)] #wf_val3 #sigma_val3_commute
     1794    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_val3 final_spec)
     1795    #wf_st' #sigma_st_commute %{wf_st'}
     1796    change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute;
     1797    >sigma_val1_commute >m_return_bind
     1798    change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute;
     1799    >sigma_val2_commute >m_return_bind
     1800    >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec)
     1801    >m_return_bind >sigma_val3_commute >m_return_bind
     1802    change with (acca_store ?????? = ?) in sigma_st_commute; assumption
     1803  | (*C_STORE*)
     1804     #dpl #dph #a #H @('bind_inversion H) -H #val1 #val1_spec
     1805     #H @('bind_inversion H) -H #val2 #val2_spec
     1806     #H @('bind_inversion H) -H #ptr #ptr_spec
     1807     #H @('bind_inversion H) -H #val3 #val3_spec
     1808     #H @('bind_inversion H) -H #mem #mem_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1809     elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec)
     1810     #wf_val1 #sigma_val1_commute   
     1811     elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec)
     1812     #wf_val2 #sigma_val2_commute
     1813     elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val3_spec)
     1814     #wf_val3 #sigma_val3_commute     
     1815     lapply(opt_eq_from_res ???? mem_spec) -mem_spec #mem_spec
     1816     elim(bestorev_sigma_commute p p' graph_prog sigma ????? wf_val3 mem_spec)
     1817     [2: @hide_prf @(proj2 … prf)]
     1818     #wf_mem #sigma_mem_commute
     1819     % [@hide_prf % [2: @wf_mem] % [2: @(proj2 … (proj1 … prf))] %
     1820        [ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))]
     1821       ]
     1822    change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute;
     1823    >sigma_val1_commute >m_return_bind
     1824    change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute;
     1825    >sigma_val2_commute >m_return_bind
     1826    >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec)
     1827    >m_return_bind
     1828    change with (acca_arg_retrieve ????? = ?) in sigma_val3_commute;
     1829    >sigma_val3_commute >m_return_bind >sigma_mem_commute
     1830    >m_return_bind //
     1831  | (*CALL*)
     1832     #f #args #dest
     1833     #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
     1834 |  (*C_EXT*)
     1835    #s_ext #H
     1836    elim(eval_ext_seq_commute … sigma gss … prf H)
     1837    #wf_st' #H1 %{wf_st'} >H1 //
     1838 ]
     1839 skip
     1840 qed.
     1841   (* check(save_frame_commute)*)
    17221842   
    1723 >>>>>>> .r2528
     1843lemma eval_statement_no_pc_sigma_commute :
     1844 ∀p,p',graph_prog.
     1845 let lin_prog ≝ linearise p graph_prog in
     1846 ∀stack_sizes.
     1847 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1848 ∀f,fn,st,stmt,st'.
     1849 ∀prf : well_formed_state … gss st.
     1850  eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1851   f fn stmt st = return st' →
     1852  ∃prf'.
     1853  eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1854    f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
     1855       (sigma_state … gss st prf) =
     1856  return sigma_state … gss st' prf'.
     1857  #p #p' #graph_prog #stack_sizes #sigma #gss
     1858  #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
     1859  #st' #prf
     1860  whd in match eval_statement_no_pc; normalize nodelta
     1861  [ @eval_seq_no_pc_sigma_commute
     1862  |*: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     1863  ]
     1864qed.
     1865
     1866
    17241867inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    17251868    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
Note: See TracChangeset for help on using the changeset viewer.