Changeset 3410


Ignore:
Timestamp:
Dec 23, 2013, 5:21:38 PM (6 years ago)
Author:
piccolo
Message:

we just realized that correctness theorem is wrong in the way it is now
stated. It only holds for premeasurable traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3409 r3410  
    558558  ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs;
    559559  match r_lb with
    560   [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉
     560  [ None ⇒ None ?
    561561  | Some lbl ⇒ if ((a_return_post lbl ∈ keep))
    562562               then if ((get_element … m lbl) == lbl :: l1)
     
    10661066  |
    10671067  ]
     1068| #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
     1069  #EQ destruct(EQ) cases daemon
    10681070|*: cases daemon (*TODO*)
    10691071]
     
    13601362
    13611363lemma correctness : ∀p,p',prog.
     1364no_duplicates_labels … prog →
    13621365let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
    13631366∀s1,s2,s1' : state p.∀abs_top,abs_tail.
     
    13691372                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
    13701373 len … t = len … t'.
    1371 #p #p' #prog @pair_elim * #t_prog #m #keep #EQtrans
     1374#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    13721375#s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail
    13731376-abs_tail lapply s1' -s1' elim t
     
    14591462    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
    14601463    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    1461     xxxxx
    1462     cut(∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
    1463           t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it' ∧
    1464           get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … (call_post_trans … (f_body … env_it) n (nil ?)) ∧
    1465           f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it')
    1466     [ cases daemon (*TODO*) ] * #env_it' * #fresh' **** #EQenv_it' #EQtrans #EQgen_labels #EQsignature #EQlab_env_it
     1464    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     1465    cases(H … EQenv_it) -H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans
     1466    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
    14671467    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
    14681468    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
     
    14821482            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
    14831483            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
    1484             @(inverse_call_post_trans … fresh') [2: % |*: cases daemon (*TODO*) ]
     1484            @(inverse_call_post_trans … fresh')
     1485            [2: % |*: [2,3: /2 by / ]
     1486                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
     1487                whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
     1488                #no_dup lapply(no_duplicates_append_r … no_dup) #H1
     1489                lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
     1490                change with ([?]@?) in match (?::?); #H1
     1491                lapply(no_duplicates_append_r … H1) >append_nil //
     1492            ]
    14851493          ]
    14861494          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
     
    14921500          whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
    14931501          >append_nil whd in match (append ???) in ⊢ (???%); //
    1494         | 
    1495           xxxxxxxxxx
    1496            
    1497            
    1498            
    1499                    
    1500             inversion(memb ???) normalize nodelta #Hlbl_keep
    1501             [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    1502           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
    1503           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
    1504           lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
    1505           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
    1506           #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    1507           #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
    1508           normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //]
    1509    
    1510    
    1511    
    1512    
    1513     cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top'' @ abs_tail_cont) (get_element … m (a_call (f_lab … env_it'))))
    1514     [2: whd >EQcont12
    1515      change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
    1516      >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
    1517      cases opt_l' in EQcode_st1' EQclean; [| #lbl'] #EQcode_st1' normalize nodelta
    1518     [2: inversion(memb ???) normalize nodelta #Hlbl_keep
    1519         [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    1520           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
    1521           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
    1522           lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
    1523           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
    1524           #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    1525           #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
    1526           normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
    1527           cases daemon (*TODO*)
    15281502        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    1529           whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
    1530           % // % // % [ % // % //]  >EQcode12 <EQtrans
    1531            * [ #_ #l3'
    1532     cases(bind_inversion ????? H) in ⊢ ?;
    1533 
    1534    
    1535     >EQcost normalize
    1536    
    1537     %{l1}
    1538   xxxxxxxx
    1539    whd in match is_silent_cost_act_b; normalize nodelta
    1540     cases lab1 in H Hio11; normalize nodelta
    1541     [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
    1542     * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_
    1543     inversion(call_post_clean ?????)
    1544     [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta *****
    1545     #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11
    1546     whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?);
    1547     inversion(code … s1')
    1548     [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    1549        destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
    1550     normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
    1551     cases(IH (mk_state ? new_code' new_cont' (store … s1') false)  l1 ?)
    1552     [2: whd whd in match check_continuations; normalize nodelta >EQHl2
    1553         normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' **
    1554     #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')}
    1555     [ whd @(empty ????? 〈(cost_act (None ?)),?〉)
    1556       [3: @hide_prf assumption |4: @hide_prf @EQconts1' |*: ] @hide_prf //
    1557       [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct | % *]  ] %
    1558     [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); 
    1559       whd in match (get_costlabels_of_trace ????) in ⊢ (???%); //
    1560     | whd in match (len ????); whd in match (len ????) in ⊢ (???%);
    1561       >EQlen %
    1562     ]
    1563   | #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****]
    1564     * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??)
    1565     [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize
    1566         [ #f #c #_
    1567         | #x * #ABS @⊥ @ABS %
    1568         | #x #_
    1569         | #_
    1570         ]
    1571         #EQ destruct(EQ) ]
    1572     #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ)
    1573     >EQcode11  inversion(code … s1')
    1574     [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    1575        destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1'
    1576     normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio
    1577     cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?)
    1578     [2: whd whd in match check_continuations; normalize nodelta >EQHl2
    1579         normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' **
    1580         #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')}
    1581         [ whd @(empty ????? 〈lab1,?〉)
    1582         [3: @hide_prf assumption |4: assumption |*:] @hide_prf // #H3 @Hio11 >EQio @H3]
    1583         % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%);
    1584               >EQlen % ]
    1585         %{Hst3st3'} >associative_append <EQcost <associative_append
    1586         >map_labels_on_trace_append <associative_append @eq_f2 //
    1587         cases new_code' in EQcall';
    1588         [| #y | #seq #opt_l #i1 | #cond #ltrue #i_true #lfalse #i_false #i1
    1589          | #cond #ltrue #i_true #lfalse #ifalse | #f #act_p #ret_opt #i | #l_in #io #l_out #i ]
    1590         whd in match (call_post_clean ?????);
    1591         [1,2: #EQ destruct(EQ) //
     1503          cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
     1504          [2: whd >EQcont12
     1505              change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
     1506              >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
     1507            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
     1508            % // % // % // % [/5 by conj/] >EQcode12 <EQtrans
     1509            @(inverse_call_post_trans … fresh')
     1510            [2: % |*: [2,3: /2 by / ]
     1511                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
     1512                whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
     1513                #no_dup lapply(no_duplicates_append_r … no_dup) #H1
     1514                lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
     1515                change with ([?]@?) in match (?::?); #H1
     1516                lapply(no_duplicates_append_r … H1) >append_nil //
     1517            ]
     1518          ]
     1519          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
     1520          %{([a_return_post lbl'] @ abs_top''')}
     1521          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
     1522          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
     1523          %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     1524          >EQlab_env_it >associative_append >associative_append
     1525          >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
     1526          whd in match (map_labels_on_trace ??); >EQgen_labels
     1527          whd in match (foldr ?????); >append_nil
     1528           @is_permutation_cons
     1529          >append_nil whd in match (append ???) in ⊢ (???%); //
    15921530       
    1593        
    1594          whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%);
    1595        
    1596          @eq_f2  whd in ⊢ (??%?);
     1531
     1532        ]
     1533    | whd in ⊢ (???% → ?); #EQ destruct
     1534    ]
     1535|       
     1536   
     1537
    15971538         
    15981539 
Note: See TracChangeset for help on using the changeset viewer.