Ignore:
Timestamp:
Dec 12, 2012, 2:43:03 PM (7 years ago)
Author:
tranquil
Message:

as_classify changed to a partial function
added a status for tailcalls

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2551 r2553  
    10241024*)
    10251025
    1026 axiom symbol_for_block_transf :
     1026lemma symbol_for_block_match:
     1027    ∀M:matching.∀initV,initW.
     1028     (∀v,w. match_var_entry M v w →
     1029      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     1030    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     1031    ∀MATCH:match_program … M p p'.
     1032    ∀b: block.
     1033    symbol_for_block … (globalenv … initW p') b =
     1034    symbol_for_block … (globalenv … initV p) b.
     1035* #A #B #V #W #match_fn #match_var #initV #initW #H
     1036#p #p' * #Mvars #Mfn #Mmain
     1037#b
     1038whd in match symbol_for_block; normalize nodelta
     1039whd in match globalenv in ⊢ (???%); normalize nodelta
     1040whd in match (globalenv_allocmem ????);
     1041change with (add_globals ?????) in match (foldl ?????);
     1042>(proj1 … (add_globals_match … initW … Mvars))
     1043[ % |*:]
     1044[ * #idr #v * #idr' #w #MVE %
     1045  [ inversion MVE
     1046    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
     1047  | @(H … MVE)
     1048  ]
     1049| @(matching_fns_get_same_blocks … Mfn)
     1050  #f #g @match_funct_entry_id
     1051]
     1052qed.
     1053
     1054lemma symbol_for_block_transf :
    10271055 ∀A,B,V,init.∀prog_in : program A V.
    10281056 ∀trans : ∀vars.A vars → B vars.
    10291057 let prog_out ≝ transform_program … prog_in trans in
    1030  ∀bl, i.
    1031  symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
    1032  symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
     1058 ∀bl.
     1059 symbol_for_block … (globalenv … init prog_out) bl =
     1060 symbol_for_block … (globalenv … init prog_in) bl.
     1061#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
     1062#v0 #w0 * //
     1063qed.
    10331064
    10341065lemma fetch_function_transf :
     
    10471078 #H @('bind_inversion H) -H #fd #eq_find_funct
    10481079 whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1049  >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
     1080 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
    10501081 >(find_funct_ptr_transf A B …  eq_find_funct) %
    10511082qed.
     
    12801311normalize //
    12811312qed.
    1282 check pc_of_label
     1313
    12831314lemma fetch_statement_sigma_commute:
    12841315  ∀p,p',graph_prog,pc,f,fn,stmt.
     
    12881319  fetch_statement (make_sem_graph_params p p') …
    12891320    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    1290 (*  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
     1321  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
    12911322      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
    12921323      pc_of_label (make_sem_lin_params p p') …
     
    12941325          (pc_block pc)
    12951326          lbl = return sigma_pc … prf)
    1296     (stmt_explicit_labels … stmt) ∧ *)
     1327    (stmt_explicit_labels … stmt) ∧
    12971328  match stmt with
    12981329  [  sequential s nxt ⇒
     
    13511382#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
    13521383lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt)
    1353 [@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 (* #H2 %
    1354 [ @In_All
    1355   #lab #lab_in
    1356   lapply (All_In ??? lab H1 ?)
    1357   [ @Exists_append_r assumption ]
    1358   inversion (sigma graph_fun lab) [#_ * #ABS @⊥ @ABS %]
    1359   #lin_pt #EQsigma #_
    1360   %
    1361   [ @hide_prf whd %
    1362   | whd in match sigma_pc; normalize nodelta
    1363     @opt_safe_elim #pc_lin
    1364   ] whd in match sigma_pc_opt;
    1365   normalize nodelta >(eqZb_false … Hbl) >fetchfn normalize nodelta
    1366   >m_return_bind >point_of_pc_of_point >EQsigma
    1367   #EQ whd in EQ : (??%?); destruct(EQ)
    1368   whd in match pc_of_label; normalize nodelta
    1369   >(fetch_internal_function_transf … fetchfn) >m_return_bind
    1370   inversion (point_of_label ????)
    1371   [2: #lin_pt' #EQ lapply (all_labels_in … EQ) >EQsigma
    1372     #EQ' destruct % ]
    1373   change with (If ? then with prf do ? else ? = ? → ?)   
    1374   @If_elim <(lin_code_has_label … (mk_lin_params p))
    1375   [ #_ whd in ⊢ (??%?→?); #EQ destruct ]
    1376   #ABS cases (absurd ?? ABS)
    1377   lapply (pi2 … (\fst (linearise_int_fun … graph_fun)) … )
    1378   [2:
    1379   normalize nodelta
    1380  
    1381   >m_return_bind whd in ⊢ (?(??%?));
    1382     % #ABS destruct(ABS)
    1383    
    1384       >(eqZb_false … Hbl) normalize nodelta >fetchfn
    1385     >m_return_bind >point_of_pc_of_point inversion(sigma graph_fun lab) in lab_spec;
    1386     [ #_ * #ABS @⊥ @ABS %] #linear_pt #linear_pt_spec #_ >m_return_bind
    1387     whd in match pc_of_label; normalize nodelta
    1388     >(fetch_internal_function_transf … fetchfn) >m_return_bind
    1389 
    1390 ] lapply H2 *)
    1391 cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
     1384[@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 %
     1385[ cases stmt in H2;
     1386  [ * [#s|#a#lbl]#nxt | #s | *]
     1387  normalize nodelta
     1388  [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ]
     1389  cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ)
     1390  #H #_
     1391  [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn)
     1392  |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H
     1393  ]
     1394]
     1395cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    13921396#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
    13931397>pc_block_sigma_commute
     
    14601464  | >H3 >m_return_bind %
    14611465]
    1462 qed. 
     1466qed.
    14631467
    14641468
     
    14681472qed.
    14691473
     1474lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
     1475  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
     1476#X #Y #P #F #m #n #H #x #EQ
     1477cases (H x ?)
     1478[ #prf #EQ' %{prf} >EQ' %
     1479| cases m in EQ; normalize #x #EQ destruct %
     1480]
     1481qed.
     1482
     1483lemma sigma_pc_exit :
     1484  ∀p,p',graph_prog,sigma,pc,prf.
     1485  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
     1486  pc = exit →
     1487  sigma_pc p p' graph_prog sigma pc prf = exit.
     1488#p #p' #graph_prog #sigma #pc #prf
     1489whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
     1490#EQ1 #EQ2 destruct
     1491whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?);
     1492destruct %
     1493qed.
     1494
     1495(* this should make things easier for ops using memory (where pc cant happen) *)
     1496definition bv_no_pc : beval → Prop ≝
     1497λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
     1498
     1499lemma bv_pc_other :
     1500  ∀P : beval → Prop.
     1501  (∀pc,p.P (BVpc pc p)) →
     1502  (∀bv.bv_no_pc bv → P bv) →
     1503  ∀bv.P bv.
     1504#P #H1 #H2 * /2/ qed.
     1505
     1506lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
     1507  bv_no_pc bv →
     1508  sigma_beval p p' graph_prog sigma bv prf = bv.
     1509#p #p' #graph_prog #sigma *
     1510[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     1511#prf * whd in match sigma_beval; normalize nodelta
     1512@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
     1513qed.
     1514
     1515lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
     1516bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
     1517#p #p' #graph_prog #sigma *
     1518[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
     1519% whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
     1520
     1521lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by.
     1522* [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by
     1523  whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
     1524
     1525lemma sigma_pc_no_exit :
     1526  ∀p,p',graph_prog,sigma,pc,prf.
     1527  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
     1528  pc ≠ exit →
     1529  sigma_pc p p' graph_prog sigma pc prf ≠ exit.
     1530#p #p' #graph_prog #sigma #pc #prf
     1531@(eqZb_elim (block_id (pc_block pc)) (-1))
     1532[ #Hbl
     1533  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
     1534  whd in match sigma_pc_opt; normalize nodelta
     1535  >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ]
     1536#NEQ #_ inversion (sigma_pc ??????)
     1537** #r #id #EQr #off #EQ
     1538lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ'
     1539% #ABS destruct(ABS) cases NEQ #H @H -H
     1540cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') %
     1541qed.
    14701542
    14711543definition linearise_status_rel:
     
    14911563>EQ2
    14921564whd in ⊢ (%→%);
     1565whd in match (exit ?);
     1566letin exit_pc ≝ (mk_program_counter «mk_block Code (-1), refl …» one)
    14931567#H lapply (opt_to_opt_safe … H)
    14941568@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
     
    14961570#H  @('bind_inversion H) -H
    14971571** #id #int_f #stmt
    1498 #stmt_spec lapply(fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
     1572#stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec)
    14991573cases stmt in stmt_spec; -stmt normalize nodelta
    1500 [1,3: [ #a #b #_| #a #b #c #d #e] #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1501 #fin_step cases(fin_step) -fin_step normalize nodelta
    1502 [1,3: [#l| #a #b #c] #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
    1503 #fetch_graph_spec #fetch_lin_spec
     1574[1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
     1575* normalize nodelta
     1576[1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
     1577#fetch_graph_spec #_ #fetch_lin_spec
    15041578#H >fetch_lin_spec >m_return_bind normalize nodelta
    1505 @('bind_inversion H) -H #state_pc #state_pc_spec
    1506 elim(pop_frame_commute
    1507   p p' graph_prog sigma gss ? id int_f ? (hide_prf … (proj2 … prf)) … state_pc_spec)
    1508 #wf_state_pc normalize nodelta #sigma_state_pc_commute >sigma_state_pc_commute
    1509 >m_return_bind @eq_program_counter_elim normalize nodelta
    1510 [2: #_ #EQ whd in EQ : (???%); destruct(EQ)] #state_pc_spec #H
    1511 @eq_program_counter_elim normalize nodelta
    1512 [2: * #ABS @⊥ @ABS whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
    1513     @opt_safe_elim #next_pc @eqZb_elim normalize nodelta >state_pc_spec
    1514     [2: * #ABS1 @⊥ @ABS1 normalize %] #_ #EQ whd in EQ : (??%?); destruct(EQ) %
    1515 |   #_ @('bind_inversion H) -H #list_val #list_val_spec 
    1516 elim(read_result_commute p p' graph_prog sigma gss ? ? ? ? ? list_val_spec)
    1517 [2: @hide_prf @(proj2 … prf)] #wf_lm #EQ >EQ -EQ >m_return_bind
    1518 whd in match Word_of_list_beval in ⊢ (% → ?); normalize nodelta
    1519 #H @('bind_inversion H) -H * #b1 #l1 #b1_l1_spec #H
    1520 cases list_val in list_val_spec wf_lm b1_l1_spec; -list_val normalize nodelta
    1521 [ #_ #l #ABS whd in ABS : (???%); destruct(ABS)]
    1522 #b2 #l2 #b2_l2_spec #wf_b2_l2 #H1 @('bind_inversion H1) -H1
    1523 #bt whd in match Byte_of_val; normalize nodelta
    1524 cases (b2) in b2_l2_spec wf_b2_l2; -b2 normalize nodelta
    1525 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (???%); destruct(ABS)]
    1526 #by #by_l2_spec #wf_by_l2 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%);
    1527 destruct(EQ) @('bind_inversion H) -H * #by1 #l3
    1528 cases l1 in by_l2_spec wf_by_l2; -l1 normalize nodelta [ #_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1529 #val #l1 #b1_val_l1_spec #wf_b1_val_l1 #H @('bind_inversion H) -H #by1
    1530 cases val in b1_val_l1_spec wf_b1_val_l1; -val
    1531 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] whd in match Byte_of_val; normalize nodelta
    1532 #ABS whd in ABS : (???%); destruct(ABS)]
    1533 #by2 #b1_by2_l1_spec #wf_b1_by2_l1 whd in match Byte_of_val; normalize nodelta
    1534 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)
    1535 #H @('bind_inversion H) -H * #by2 #l2
    1536 cases(l3) in b1_by2_l1_spec wf_b1_by2_l1; -l3 normalize nodelta
    1537 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1538 #val #l1 #b1_by1_val_l1_spec #wf_b1_by1_val_l1 #H @('bind_inversion H) -H
    1539 #by3 cases val in b1_by1_val_l1_spec wf_b1_by1_val_l1; -val normalize nodelta
    1540 [1,2,3,5,6,7: [||#a #b #c | #p | #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (??%%); destruct(ABS)] 
    1541 #by3 #b1_by1_by3_l1_spec #wf_b1_by1_by3_l1 #EQ whd in EQ : (???%); destruct(EQ)
    1542 #EQ whd in EQ : (???%); destruct(EQ) #H @('bind_inversion H) -H *
    1543 #by3 #l1 cases l2 in  b1_by1_by3_l1_spec  wf_b1_by1_by3_l1; -l2 normalize nodelta
    1544 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)]
    1545 #val #l2 #_ #wf_b1_by1_by2_val #H @('bind_inversion H) -H #by4
    1546 cases val in wf_b1_by1_by2_val; -val normalize nodelta
    1547 [1,2,3,5,6,7: [|| #a #b #c |#p | #p #p'|#p #pa] #a #ABS whd in ABS : (???%); destruct(ABS)]
    1548 #by5 #wf_list #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ)  cases l1 in wf_list; -l1 normalize nodelta [2: #val #l #a #ABS whd in ABS : (???%); destruct(ABS)]
    1549 #wf_list #EQ whd in EQ : (???%); destruct(EQ)
    1550 @opt_safe_elim #l #H normalize in H; destruct(H) normalize % #ABS destruct(ABS)
     1579letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes))
     1580letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
     1581cut (preserving … res_preserve …
     1582       (sigma_state … gss)
     1583       (λl.λ_ : True.l)
     1584       (λst.
     1585          do st' ← pop_frame … graph_ge id int_f st;
     1586          if eq_program_counter (pc … st') exit_pc then
     1587          do vals ← read_result … graph_ge (joint_if_result … int_f) st ;
     1588            Word_of_list_beval vals
     1589          else
     1590            Error ? [ ])
     1591       (λst.
     1592          do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st;
     1593          if eq_program_counter (pc … st') exit_pc then
     1594          do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ;
     1595            Word_of_list_beval vals
     1596          else
     1597            Error ? [ ]))
     1598[ #st #prf @mfr_bind [3: @pop_frame_commute |*:]
     1599  #st' #prf' @eq_program_counter_elim 
     1600  [ #EQ_pc >(sigma_pc_exit … EQ_pc) normalize nodelta
     1601    @mfr_bind [3: @read_result_commute |*:]
     1602    #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv'
     1603    @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1604        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1605    [
     1606    | * -lbv -lbv' #by1 #lbv #lbv_prf
     1607      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1608        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1609    [ @opt_safe_elim #lbv' #EQ_lbv'
     1610    |* -lbv #by2 #lbv #lbv_prf
     1611      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1612        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1613    [ @opt_safe_elim #lbv' #EQ_lbv'
     1614    |* -lbv #by3 #lbv #lbv_prf
     1615      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
     1616        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
     1617    [ @opt_safe_elim #lbv' #EQ_lbv'
     1618    |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ]
     1619      #lbv_prf @mfr_return %
     1620    ]]]]
     1621    cases lbv in EQ_lbv';
     1622    try (#H @res_preserve_error)
     1623    -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1'
     1624    #H @('bind_inversion H) -H #tl' #EQtl'
     1625    whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1626    @(mfr_bind … (λby.λ_:True.by))
     1627    [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1';
     1628      whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1629    |*: #by1 * @mfr_return_eq
     1630      change with (m_list_map ????? = ?) in EQtl';
     1631      [1,3,5,7: %
     1632      |*: @opt_safe_elim #lbv''
     1633      ] >EQtl' #EQ destruct %
     1634    ]
     1635  | #_ @res_preserve_error
     1636  ]
     1637]
     1638#PRESERVE
     1639cases (PRESERVE … (proj2 … prf) … H) *
     1640#EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS)
    15511641qed.
    15521642
     
    15651655#EQ >EQ //
    15661656qed.*)
    1567 
    1568 (* this should make things easier for ops using memory (where pc cant happen) *)
    1569 definition bv_no_pc : beval → Prop ≝
    1570 λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
    1571 
    1572 lemma bv_pc_other :
    1573   ∀P : beval → Prop.
    1574   (∀pc,p.P (BVpc pc p)) →
    1575   (∀bv.bv_no_pc bv → P bv) →
    1576   ∀bv.P bv.
    1577 #P #H1 #H2 * /2/ qed.
    1578 
    1579 lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
    1580   bv_no_pc bv →
    1581   sigma_beval p p' graph_prog sigma bv prf = bv.
    1582 #p #p' #graph_prog #sigma *
    1583 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
    1584 #prf * whd in match sigma_beval; normalize nodelta
    1585 @opt_safe_elim #bv' normalize #EQ destruct(EQ) %
    1586 qed.
    1587 
    1588 lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
    1589 bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
    1590 #p #p' #graph_prog #sigma *
    1591 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
    1592 % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
    15931657
    15941658lemma is_push_sigma_commute :
     
    16241688qed.
    16251689
    1626 lemma byte_of_val_inv :
    1627   ∀e,bv,v.Byte_of_val e bv = return v → bv = BVByte v.
    1628 #e *
    1629 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] #v
    1630 whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
    1631 
    1632 lemma bit_of_val_inv :
     1690lemma Bit_of_val_inv :
    16331691  ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v.
    16341692#e *
     
    16541712#v #EQ %{I}
    16551713>sigma_bv_no_pc try assumption
    1656 >(byte_of_val_inv … EQ) %
     1714>(Byte_of_val_inv … EQ) %
    16571715qed.
    16581716
     
    16681726[2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
    16691727#v #EQ %{I} >sigma_bv_no_pc try assumption
    1670 >(byte_of_val_inv … EQ) %
     1728>(Byte_of_val_inv … EQ) %
    16711729qed.
    16721730
     
    19862044 qed.
    19872045
    1988 lemma eval_seq_no_call_no_goto :
     2046lemma eval_seq_no_call_no_goto_ok :
    19892047 ∀p,p',graph_prog.
    19902048 let lin_prog ≝ linearise p graph_prog in
     
    20192077[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    20202078  whd in match joint_classify_step; normalize nodelta
    2021   @no_call_other assumption
     2079  >no_call_other try % assumption
    20222080| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
    20232081  whd in match eval_statement_no_pc; normalize nodelta
     
    20302088qed.
    20312089
    2032 lemma eval_seq_no_call_goto :
     2090lemma eval_seq_no_call_goto_ok :
    20332091 ∀p,p',graph_prog.
    20342092 let lin_prog ≝ linearise p graph_prog in
     
    20462104  (succ_pc (make_sem_graph_params p p') …
    20472105    (pc … st) nxt) in
    2048  (? : Prop) →
     2106 ∀prf'.
    20492107 fetch_statement (make_sem_lin_params p p') …
    20502108   (globalenv_noinit … lin_prog)
    20512109     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
    20522110   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
     2111 pc_of_label (make_sem_lin_params p p') ?
     2112                (globalenv_noinit ? (linearise p … graph_prog))
     2113                (pc_block (pc … st))
     2114                nxt = return sigma_pc p p' graph_prog sigma
     2115    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
    20532116 ∃prf''.
    20542117 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     
    20572120 bool_to_Prop (taaf_non_empty … taf).
    20582121#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
    2059 #prf #EQfetch' #EQeval #prf' #EQsucc_pc
     2122#prf #EQfetch' #EQeval #prf' #EQsucc_pc #EQ_pc_of_label
    20602123cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
    20612124#prf'' #EQeval'
    20622125% [ @hide_prf % assumption ]
    2063 %{(taaf_step … (taa_base …) …)} [3: % ]
    2064 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
     2126%{(taaf_step … (taa_step … (taa_base …)) …)} [7: % ]
     2127[4: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
    20652128  whd in match joint_classify_step; normalize nodelta
    2066   @no_call_other assumption
    2067 | whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
     2129  >no_call_other try % assumption
     2130|3: whd whd in match eval_state; normalize nodelta >EQfetch' in ⊢ (??%?);
     2131  >m_return_bind in ⊢ (??%?);
    20682132  whd in match eval_statement_no_pc; normalize nodelta
    2069   >EQeval' >m_return_bind
     2133  >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
    20702134  whd in match eval_statement_advance; normalize nodelta
    2071   >no_call_advance [2: assumption ]
    2072   whd in match (next ???);
    2073   >EQsucc_pc %
     2135  >no_call_advance in ⊢ (??%?); [2: assumption ]
     2136  whd in match (next ???) in ⊢ (??%?);
     2137  >EQsucc_pc in ⊢ (??%?); %
     2138|1: whd whd in ⊢ (??%?); >EQsucc_pc %
     2139|5: %* #H @H -H whd in ⊢ (??%?);  >EQsucc_pc %
     2140|2: whd whd in match eval_state; normalize nodelta
     2141  >EQsucc_pc >m_return_bind >m_return_bind whd in match eval_statement_advance;
     2142  normalize nodelta whd in match goto; normalize nodelta
     2143  whd in match (pc_block ?); >pc_block_sigma_commute
     2144  >EQ_pc_of_label %
     2145|*:
    20742146]
    20752147qed.
    20762148
    2077 
    2078  
    2079 
    2080   [ assumption
    2081   | assu
    2082  
     2149lemma eval_call_ok :
     2150 ∀p,p',graph_prog.
     2151 let lin_prog ≝ linearise p graph_prog in
     2152 ∀stack_sizes.
     2153 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     2154 ∀st,st',f,fn,called,args,dest,nxt.
     2155 ∀prf : well_formed_state_pc … gss st.
    20832156  fetch_statement (make_sem_lin_params p p') …
    2084           (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    2085               return 〈f, \fst (linearise_int_fun … fn),
    2086                       sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
    2087           ∃prf'.
    2088             let nxt_pc ≝  in
    2089             let sigma_nxt ≝  in
    2090             (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
    2091              (globalenv_noinit … lin_prog) nxt_pc =
    2092              return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     2157    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
     2158      return 〈f, \fst (linearise_int_fun … fn),
     2159        sequential … (CALL (mk_lin_params p) … called args dest ) it〉 →
     2160   eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     2161      (CALL … called args dest) nxt st = return st' →
     2162(* let st_pc' ≝ mk_state_pc ? st'
     2163  (succ_pc (make_sem_graph_params p p') …
     2164    (pc … st) nxt) in
     2165 ∀prf'.
     2166 fetch_statement (make_sem_lin_params p p') …
     2167   (globalenv_noinit … lin_prog)
     2168     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
     2169   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
     2170 pc_of_label (make_sem_lin_params p p') ?
     2171                (globalenv_noinit ? (linearise p … graph_prog))
     2172                (pc_block (pc … st))
     2173                nxt = return sigma_pc p p' graph_prog sigma
     2174    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →*)
     2175  let st2_pre_call ≝ sigma_state_pc … gss st prf in
     2176  ∃is_call, is_call'.
     2177  ∃prf'.
     2178  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
     2179  joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» =
     2180  joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧
     2181  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
     2182    st2_pre_call = return st2_after_call.
     2183cases daemon
     2184qed.
     2185
     2186lemma eval_goto_ok :
     2187lemma eval_tailcall_ok :
     2188lemma eval_cond_cond_ok :
     2189lemma eval_cond_fcond_ok :
     2190lemma eval_return_ok :
     2191
    20932192
    20942193inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.