Changeset 3448


Ignore:
Timestamp:
Feb 19, 2014, 6:45:55 PM (5 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3447 r3448  
    15491549        >memb_append_l1 // <(\P EQx_hdlab) >Hx // ]
    15501550    normalize nodelta >get_element_append_l1
    1551     [2: cases daemon (*noduplicates*)] @get_element_append_l1
     1551    [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail
     1552        [ whd in match (foldr ?????); @lab_map_in_domain // ]
     1553        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
     1554        >memb_append_l2 // >IH %
     1555    ] @get_element_append_l1
    15521556    % #H1 
    15531557    (* subproof with no nice statement *)
     
    15801584    ]
    15811585    ]
    1582   | whd #x #Hx >memb_append_l12 [2: cases daemon (*TODO*) ]
     1586  | whd #x #Hx >memb_append_l12
     1587    [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail
     1588        [ whd in match (foldr ?????); @lab_to_keep_in_domain // ]
     1589        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
     1590        >memb_append_l2 // >IH %
     1591    ]
    15831592    >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H)
    15841593    // @⊥
     
    16861695   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
    16871696   (((x ::l4 @y ::l3) @l8) @l9)).
     1697   
     1698lemma append_premeasurable : ∀S : abstract_status.
     1699∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
     1700pre_measurable_trace … t1 → pre_measurable_trace … t2 →
     1701pre_measurable_trace … (t1 @ t2).
     1702#S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
     1703[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
     1704  %2 // @IH //
     1705| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
     1706| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
     1707| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
     1708  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
     1709  normalize >append_associative in ⊢ (????(???????%)); %5 // @IH2 //
     1710]
     1711qed.
    16881712   
    16891713
    1690 lemma correctness : ∀p,p',prog.
     1714lemma correctness_lemma : ∀p,p',prog.
    16911715no_duplicates_labels … prog →
    16921716let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     
    17001724                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
    17011725 len … t = len … t' ∧
    1702  ∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
     1726 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
    17031727 cont … s1 = k @ cont … s2 →
    1704 All … (λx.let 〈lab,i〉 ≝ x in ¬ is_unlabelled_ret_act lab) k →
    1705 ∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|.
     1728∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
     1729∧ pre_measurable_trace … t'.
    17061730#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    17071731#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
    17081732-abs_tail lapply s1' -s1' elim Hpre
    1709 [ #st #_ #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
     1733[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
    17101734  %
    1711   [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    1712     @is_permutation_eq
    1713   | #k #i #_ #EQcont_st #wf %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
    1714   ]
     1735  [ %
     1736    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
     1737      @is_permutation_eq
     1738    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
     1739    ]
     1740  | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
     1741    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
     1742    inversion(code ??) normalize nodelta
     1743    [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
     1744     | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_
     1745     | #lin #io #lout #i #_ ]
     1746    #EQcode_s1' normalize nodelta [|*: % #EQ destruct] <H2
     1747    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1748    normalize in Hst; <e1 in Hst; normalize nodelta //
     1749  ]   
    17151750| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    17161751  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
    1717     #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #_ * #opt_l #EQ destruct(EQ)
     1752    #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #class_st11 * #opt_l #EQ destruct(EQ)
    17181753    #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
    17191754    whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
     
    17391774      [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
    17401775           cases(call_post_clean ?????) normalize nodelta
    1741            [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
     1776           [1,3,5,7,9: #EQ destruct(EQ)]
     1777        [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta]
     1778          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1779        | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?);
     1780          [2: cases(call_post_clean ?????) normalize nodelta
     1781          [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?);
     1782          #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1783        | * #z1 #z2 cases(call_post_clean ?????)
     1784          [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta]
     1785          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1786        | * #z1 #z2 cases ret_post normalize nodelta
     1787          [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ]
     1788          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1789        | * #z1 #z2 cases(?∧?) normalize nodelta
     1790          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1791        ]
     1792      ]
    17421793      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
    17431794      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
     
    17451796         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
    17461797         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1747       #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
     1798      #abs_top' * #abs_tail' * #st3' * #t' ****
     1799      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t'
    17481800      %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    17491801      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    17501802        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1751       % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
     1803      %
     1804      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
    17521805      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    17531806      [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    1754       destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1807      destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    17551808      #EQk1 #EQlength %{(〈cost_act (None ?),new_code'〉::k1)}
    1756       % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
     1809      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
     1810      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
     1811      normalize in class_st11; >EQcode11 in class_st11; //
    17571812    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
    17581813      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     
    17661821      | #l_in #io #l_out #i #_
    17671822      ]
    1768       [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
     1823      [|*: #_ whd in ⊢ (??%% → ?);
     1824           [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1825           | cases(call_post_clean ?????) normalize nodelta
     1826             [| * #z2 #z3 cases lbl normalize nodelta
     1827                [| #z4 cases(?==?) normalize nodelta] ]
     1828             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1829           | cases(call_post_clean ?????) normalize nodelta
     1830             [| * #z2 #z3 cases(call_post_clean ?????)
     1831               [| * #z4 #z5 >m_return_bind cases(call_post_clean ?????)
     1832                  [| * #z6 #z7 >m_return_bind cases(?∧?) normalize nodelta ]]]
     1833             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1834           |  cases(call_post_clean ?????) normalize nodelta
     1835             [| * #z2 #z3 cases(call_post_clean ?????)
     1836                [| * #z4 #z5 >m_return_bind cases(?∧?) normalize nodelta ]]
     1837             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1838           | cases(call_post_clean ?????) normalize nodelta
     1839             [| * #z1 #z2 cases ret_post normalize nodelta
     1840                [| #z3 cases(memb ???) normalize nodelta
     1841                   [ cases (?==?) normalize nodelta]]]
     1842             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1843           | cases(call_post_clean ?????) normalize nodelta
     1844             [| * #z1 #z2 cases(?∧?) normalize nodelta ]
     1845             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1846           ]
     1847      ]
    17691848      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
    17701849      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
     
    17731852         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
    17741853         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1775       #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcost #EQlen #stack_safety
     1854      #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety
     1855      #pre_t'
    17761856      %{abs_top'} %{abs_tail'} %{st3'}
    17771857      %{(t_ind … (cost_act (Some ? lbl)) … t')}
    17781858      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    17791859        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1780       % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
     1860      %
     1861      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
    17811862          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    17821863          @is_permutation_cons assumption
    17831864        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    17841865          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    1785           destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1866          destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    17861867          #EQk1 #EQlength %{(〈cost_act (Some ? lbl),new_code'〉::k1)}
    17871868          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    1788         ]
     1869        ]]
     1870      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
     1871      normalize in class_st11; >EQcode11 in class_st11; //
    17891872    ]
    17901873  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
     
    17941877    ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
    17951878    #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ]
    1796     inversion(code ??) [1,2,4,5,6,7,8,9,11,12,13,14: cases daemon (*assurdi*)]
     1879    inversion(code ??)
     1880    [1,2,4,5,6,7,8,9,11,12,13,14:
     1881      [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1882      |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1883      |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     1884            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1885            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1886                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     1887                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     1888            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1889      |4,10:  #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     1890            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1891            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1892                [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     1893            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1894      |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1895             normalize nodelta
     1896             [2,4: * #z1 #z2 cases lbl normalize nodelta
     1897               [2,4: #l1 cases(memb ???) normalize nodelta
     1898                 [1,3: cases(?==?) normalize nodelta ]]]
     1899            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1900      |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1901             normalize nodelta
     1902             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     1903             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1904      ]
     1905    ]
    17971906    #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?);
    17981907    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
     
    18101919    |2,5:
    18111920    ]
    1812     #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1813     %{abs_top1}
     1921    #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1922    #pre_t' %{abs_top1}
    18141923    %{abs_tail1} %{s2'} %{(t_ind … t')}
    18151924    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
    18161925    |2,5:
    18171926    ]
    1818     % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
     1927    % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
    18191928        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
    18201929        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
    18211930        assumption
    1822       |*: #k #i #EQcont_st3 >EQcont #EQ #H
    1823           cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
    1824       ]
     1931      |*: #k #i #EQcont_st3 >EQcont #EQ
     1932          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     1933      ]]
     1934    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    18251935  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18261936    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18281938    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
    18291939    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1830     [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     1940    [1,2,3,5,6,7:
     1941     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1942     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1943     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1944       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     1945       [2: #l1 cases(?==?) normalize nodelta]]
     1946       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1947     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     1948       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1949       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1950       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     1951       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1952     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1953             normalize nodelta
     1954             [2,4: * #z1 #z2 cases lbl normalize nodelta
     1955               [2,4: #l1 cases(memb ???) normalize nodelta
     1956                 [1,3: cases(?==?) normalize nodelta ]]]
     1957            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1958     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1959             normalize nodelta
     1960             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     1961             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1962      ]
     1963    ]
     1964    #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
    18311965    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    18321966    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     
    18451979        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18461980        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1847     ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen
    1848       #stack_safety %{abs_top1} %{abs_tail1}
     1981    ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
     1982      #stack_safety #pre_t' %{abs_top1} %{abs_tail1}
    18491983    %{s2'} %{(t_ind … t')}
    18501984    [ @hide_prf @(cond_true … EQcode_s1') //
    18511985    |
    18521986    ]
    1853     %
     1987    % [ %
    18541988    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    18551989      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    18561990      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    18571991      assumption
    1858     |  #k #i1 #EQcont_st3 #EQcont_st11 #H
     1992    |  #k #i1 #EQcont_st3 #EQcont_st11
    18591993       cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
    1860        [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     1994       [2: >EQcont_st12 >EQcont_st11 % ]
    18611995       * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    18621996       %{tl1} % // whd in EQk1 : (??%%); destruct //
    1863     ]
     1997    ]]
     1998    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    18641999  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18652000    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18672002    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
    18682003    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1869     [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     2004    [1,2,3,5,6,7:
     2005     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2006     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2007     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2008       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2009       [2: #l1 cases(?==?) normalize nodelta]]
     2010       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2011     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2012       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2013       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2014       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2015       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2016     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2017             normalize nodelta
     2018             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2019               [2,4: #l1 cases(memb ???) normalize nodelta
     2020                 [1,3: cases(?==?) normalize nodelta ]]]
     2021            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2022     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2023             normalize nodelta
     2024             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2025             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2026      ]
     2027    ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
    18702028    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    18712029    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     
    18842042        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18852043        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1886     ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen #stack_safety
     2044    ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
     2045    #pre_t'
    18872046    %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    18882047    [ @hide_prf @(cond_false … EQcode_s1') //
    18892048    |
    18902049    ]
    1891     %
     2050    % [ %
    18922051    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    18932052      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    18942053      >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    18952054      assumption
    1896     | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2055    | #k #i1 #EQcont_st3 #EQcont_st11
    18972056      cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
    1898       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2057      [2: >EQcont_st12 >EQcont_st11 % ]
    18992058      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    19002059      %{tl1} % // whd in EQk1 : (??%%); destruct //
    1901     ]
     2060    ] ]
     2061    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19022062 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    19032063   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
    19042064   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
    19052065   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1906    [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     2066   [1,2,3,4,6,7:
     2067     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2068     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2069     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2070       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2071       [2: #l1 cases(?==?) normalize nodelta]]
     2072       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2073     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2074            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2075            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2076                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2077                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2078            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2079     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2080             normalize nodelta
     2081             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2082               [2,4: #l1 cases(memb ???) normalize nodelta
     2083                 [1,3: cases(?==?) normalize nodelta ]]]
     2084            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2085     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2086             normalize nodelta
     2087             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2088             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2089      ]
     2090   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
    19072091   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19082092   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     
    19232107       % //
    19242108   ]
    1925    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1926    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2109   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2110   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19272111   [ @hide_prf @(loop_true … EQcode_s1') // |]
    1928    %
     2112   % [ %
    19292113   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19302114     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19312115      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19322116     @is_permutation_cons assumption
    1933    | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2117   | #k #i1 #EQcont_st3 #EQcont_st11
    19342118      cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …)
    1935       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2119      [2: >EQcont_st12 >EQcont_st11 % ]
    19362120      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    19372121      %{tl1} % // whd in EQk1 : (??%%); destruct //
    1938    ]
     2122   ] ]
     2123   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19392124 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    19402125   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
    19412126   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
    19422127   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1943    [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     2128   [1,2,3,4,6,7:
     2129     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2130     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2131     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2132       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2133       [2: #l1 cases(?==?) normalize nodelta]]
     2134       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2135     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2136            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2137            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2138                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2139                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2140            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2141     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2142             normalize nodelta
     2143             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2144               [2,4: #l1 cases(memb ???) normalize nodelta
     2145                 [1,3: cases(?==?) normalize nodelta ]]]
     2146            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2147     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2148             normalize nodelta
     2149             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2150             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2151      ]
     2152   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
    19442153   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19452154   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     
    19582167        % // % // % // % [2: %] //
    19592168   ]
    1960    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1961    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2169   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2170   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19622171   [ @hide_prf @(loop_false … EQcode_s1') // |]
    1963    %
     2172   % [ %
    19642173   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19652174     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19662175     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19672176     @is_permutation_cons assumption
    1968    | #k #i #EQcont_st3 <EQcont_st12 #EQ #H
    1969      cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
    1970    ]
     2177   | #k #i #EQcont_st3 <EQcont_st12 #EQ
     2178     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     2179   ]]
     2180   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19712181 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    19722182   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     
    19742184   [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
    19752185   #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1976    [1,2,3,4,5,6: cases daemon (*ASSURDI*)] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
     2186   [1,2,3,4,5,6:
     2187     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2188     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2189     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2190       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2191       [2: #l1 cases(?==?) normalize nodelta]]
     2192       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2193     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2194            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2195            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2196                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2197                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2198            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2199     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2200       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2201       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2202       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2203       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2204     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2205             normalize nodelta
     2206             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2207               [2,4: #l1 cases(memb ???) normalize nodelta
     2208                 [1,3: cases(?==?) normalize nodelta ]]]
     2209            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2210      ]
     2211   ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
    19772212   whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19782213   [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta
     
    19892224       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    19902225   ]
    1991    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1992    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2226   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2227   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19932228   [ @hide_prf @(io_in … EQcode_s1') // |]
    1994    %
     2229   % [ %
    19952230   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19962231     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19972232     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19982233     @is_permutation_cons assumption
    1999    | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2234   | #k #i1 #EQcont_st3 #EQcont_st11
    20002235      cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …)
    2001       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2236      [2: >EQcont_st12 >EQcont_st11 %]
    20022237      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    20032238      %{tl1} % // whd in EQk1 : (??%%); destruct //
    2004    ]
     2239   ]]
     2240   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    20052241  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    20062242    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
     
    20082244    destruct #t #_ * #nf #EQ destruct
    20092245  ]
    2010 | #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,8: cases daemon (*assurdi*)]
     2246| #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?;
     2247  [1,2,3,4,5,6,7,8:
     2248    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
     2249    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
     2250    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
     2251    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
     2252    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2253    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2254    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
     2255    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
     2256    ]
     2257    destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS %
     2258  ]
    20112259  #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ)
    20122260  #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6)
     
    20282276  inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    20292277  ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?);
    2030   inversion(code … s1') [1,3,4,5,6,7: cases daemon (*TODO*) ] #r_t' #EQcode_s1'
     2278  inversion(code … s1')
     2279  [1,3,4,5,6,7:
     2280     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2281     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2282       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2283       [2: #l1 cases(?==?) normalize nodelta]]
     2284       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2285     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2286            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2287            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2288                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2289                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2290            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2291     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2292       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2293       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2294       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2295       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2296     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2297             normalize nodelta
     2298             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2299               [2,4: #l1 cases(memb ???) normalize nodelta
     2300                 [1,3: cases(?==?) normalize nodelta ]]]
     2301            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2302     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2303             normalize nodelta
     2304             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2305             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2306      ]
     2307  ]
     2308   #r_t' #EQcode_s1'
    20312309  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    20322310  #EQstore11 #EQio_11 #EQ destruct
    20332311  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    20342312  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2035   #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2036   %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2313  #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2314  #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    20372315  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    20382316  | ]
    2039   %
     2317  % [ %
    20402318  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    20412319    whd in match (get_costlabels_of_trace ????);
     
    20452323  | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%);
    20462324    [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    2047     destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     2325    destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    20482326    #EQk1 #EQlength %{(〈ret_act (Some ? lbl1),i〉::k1)}
    20492327    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    2050   ]
     2328  ]]
     2329  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    20512330| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    2052   [1,2,3,4,5,6,7,9: cases daemon (*absurd!*)
     2331  [1,2,3,4,5,6,7,9:
     2332    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
     2333    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
     2334    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
     2335    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
     2336    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2337    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2338    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
     2339    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
     2340    ]
     2341    destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); *
    20532342  | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
    20542343    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
     
    20592348    #abs_top_cont #abs_tail_cont #EQcheck
    20602349    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
    2061     [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
     2350    [1,2,3,4,5,7:
     2351     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2352     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2353     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2354       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2355       [2: #l1 cases(?==?) normalize nodelta]]
     2356       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2357     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2358            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2359            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2360                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2361                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2362            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2363     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2364       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2365       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2366       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2367       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2368     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2369             normalize nodelta
     2370             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2371             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2372     ]
     2373    ] #f' #act_p' #opt_l' #i' #_
    20622374    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    20632375    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     
    20922404            ]
    20932405          ]
    2094           #abs_top''' * #abs_tail''' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
    2095           %{abs_top'''}
     2406          #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
     2407          #pre_t' %{abs_top'''}
    20962408          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    20972409          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
    2098           %
     2410          % [ %
    20992411          [ % [2: whd in ⊢ (??%%); >EQlen %]
    21002412            %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     
    21032415            whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
    21042416            >append_nil whd in match (append ???) in ⊢ (???%); //
    2105           | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2417          | #k #i1 #EQcont_st3 #EQcont_st11
    21062418            cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …)
    2107             [2: >EQcont12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2419            [2: >EQcont12 >EQcont_st11 % ]
    21082420            * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    21092421            %{tl1} % // whd in EQk1 : (??%%); destruct //
    2110           ]
     2422          ]]
     2423          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
    21112424        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    21122425        ]
     
    21642477          ]
    21652478     ]
    2166      #abs_top''' * #abs_tail''' * #st41' * #t1' *** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2479     #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2480     #pre_t1'
    21672481     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
    21682482     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     
    21932507             abs_tail_cont abs_top'''')
    21942508     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2195      #abs_top_1 * #abs_tail_1 * #st5' * #t2' *** #Hst5_st5' #EQcosts'
    2196      #EQlen'  #stack_safety2 %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2509     #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
     2510     #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    21972511     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    21982512     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
    21992513     |2,4: skip
    22002514     ]
    2201      %
     2515     % [ %
    22022516     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
    22032517           whd in ⊢ (??%%); @eq_f // ]
     
    22142528       cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
    22152529       >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
    2216      | #k #i #EQcont_st3 #EQ #H
    2217        cases(stack_safety2 … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
     2530     | #k #i #EQcont_st3 #EQ
     2531       cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     2532     ]]
     2533     %4
     2534     [ normalize >EQcode_st1' normalize nodelta % #EQ destruct
     2535     | %{f} % //
     2536     | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I
     2537     | @append_premeasurable // %3 //
     2538       [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct
     2539       | whd %{lbl'} %
     2540       ]
    22182541     ]
    22192542]
  • LTS/Vm.ma

    r3379 r3448  
    1 include "Common.ma".
    2 
    3 inductive instr: Type[0] :=
    4 | Iconst: nat → instr
    5 | Ivar: option ident → instr
    6 | Isetvar: option ident → instr
    7 | Iadd: instr
    8 | Isub: instr
    9 | Ijmp: nat → instr
    10 | Ibne: nat → instr
    11 | Ibge: nat → instr
    12 | Ihalt: instr
    13 | Iio: instr
    14 | Icall: fname → instr
    15 | Iret: fname → instr.
    16 
    17 definition programT ≝ fname → list instr.
    18 
    19 definition fetch: list instr → nat → option instr ≝ λl,n. nth_opt ? n l.
    20 
    21 definition stackT: Type[0] ≝ list nat.
    22 
    23 definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).
    24 
    25 definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).
    26 
    27 inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
    28 | vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
    29    vmstep …
    30     〈c, pc,     stk,      s〉
    31     〈c, 1 + pc, n :: stk, s〉
    32 | vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
    33    vmstep …
    34     〈c, pc,     stk,              s〉
    35     〈c, 1 + pc, get … s x :: stk, s〉
    36 | vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
    37    vmstep …
    38     〈c, pc,     n :: stk, s〉
    39     〈c, 1 + pc, stk,      set … s x n〉
    40 | vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
    41    vmstep …
    42     〈c, pc,     n2 :: n1 :: stk,  s〉
    43     〈c, 1 + pc, (n1 + n2) :: stk, s〉
    44 | vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
    45    vmstep …
    46     〈c, pc,     n2 :: n1 :: stk,  s〉
    47     〈c, 1 + pc, (n1 - n2) :: stk, s〉
    48 | vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) →
    49    let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
    50    vmstep …
    51     〈c, pc,  n2 :: n1 :: stk, s〉
    52     〈c, pc', stk,             s〉
    53 | vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) →
    54    let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
    55    vmstep …
    56     〈c, pc,  n2 :: n1 :: stk, s〉
    57     〈c, pc', stk,             s〉
    58 | vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) →
    59    let pc' ≝ 1 + pc + ofs in
    60    vmstep …
    61     〈c,           pc, stk, s〉
    62     〈c, 1 + pc + ofs, stk, s〉
    63 | vmstep_io: ∀c,pc,stk,s. fetch c pc = Some … Iio →
    64    vmstep …
    65     〈c,     pc, stk, s〉
    66     〈c, 1 + pc, stk, s〉.
    67 
    68 definition emitterT ≝ nat → nat → option label.
    69 
    70 definition vmlstep: ∀p: programT. ∀S: storeT. ∀emit: emitterT.
    71  vmstate S → vmstate S → list label → Prop ≝
    72 λp,S,emitter,s1,s2,ll. ∀l.
    73  vmstep p S s1 s2 ∧ ll = [l] ∧ emitter (pc … s1) (pc … s2) = Some … l.
    74 
    75 (*
    76 Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).
    77 
    78 Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
    79         exists pc,
    80         code_at c pc = Some (Ihalt lbl) /\
    81         star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.
    82 
    83 Definition term_vm (c: code_vm) (s_init s_fin: store):=
    84         exists pc,
    85         code_at c pc = Some (Ihalt False) /\
    86         star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.
    87 
    88 Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
    89         exists pc,
    90         code_at c pc = Some (Ihalt label) /\
    91         star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
    92 *)
     1include "Traces.ma".
     2include "basics/lists/list.ma".
     3include "../src/utilities/option.ma".
     4include "basics/jmeq.ma".
     5
     6record monoid: Type[1] ≝
     7 { carrier :> Type[0]
     8 ; op: carrier → carrier → carrier
     9 ; e: carrier
     10 ; neutral: ∀x. op … x e = x
     11 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
     12 }.
     13
     14record assembler_params : Type[1] ≝
     15{ seq_instr : Type[0]
     16; jump_condition : Type[0]
     17; io_instr : Type[0]
     18; entry_of_function : FunctionName → ℕ
     19; call_label_fun : list (ℕ × CallCostLabel)
     20; return_label_fun : list (ℕ × ReturnPostCostLabel)
     21}.
     22
     23inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
     24| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
     25| Ijmp: ℕ → AssemblerInstr p
     26| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
     27| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
     28| Icall: FunctionName → AssemblerInstr p
     29| Iret: AssemblerInstr p.
     30
     31definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
     32
     33definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
     34 λp,l,n. nth_opt ? n (\fst l).
     35
     36definition stackT: Type[0] ≝ list (nat).
     37
     38record sem_params (p : assembler_params) : Type[1] ≝
     39{ m : monoid
     40; asm_store_type : Type[0]
     41; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
     42; eval_asm_cond : jump_condition p → asm_store_type → option bool
     43; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
     44; cost_of_io : io_instr p → asm_store_type → m
     45; cost_of : AssemblerInstr p → m
     46}.
     47
     48record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
     49{ pc : ℕ
     50; asm_stack : stackT
     51; asm_store : asm_store_type … p'
     52; asm_is_io : bool
     53; cost : m … p'
     54}.
     55
     56definition label_of_pc ≝ λL.λl.λpc.find …
     57   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
     58
     59
     60inductive vmstep (p : assembler_params) (p' : sem_params p)
     61   (prog : AssemblerProgram p)  :
     62      ActionLabel → relation (vm_state p p') ≝
     63| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
     64           fetch … prog (pc … st1) = return (Seq p i l) →
     65           asm_is_io … st1 = false →
     66           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
     67           asm_stack … st1 = asm_stack … st2 →
     68           asm_is_io … st1 = asm_is_io … st2 →
     69           S (pc … st1) = pc … st2 →
     70           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
     71           vmstep … (cost_act l) st1 st2
     72| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
     73           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
     74           asm_is_io … st1 = false →
     75           asm_store … st1 = asm_store … st2 →
     76           asm_stack … st1 = asm_stack … st2 →
     77           asm_is_io … st1 = asm_is_io … st2 →
     78           new_pc = pc … st2 →
     79           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
     80           vmstep … (cost_act (None ?)) st1 st2
     81| vm_cjump_true :
     82           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
     83           eval_asm_cond p p' cond (asm_store … st1) = return true→
     84           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     85           asm_is_io … st1 = false →
     86           asm_store … st1 = asm_store … st2 →
     87           asm_stack … st1 = asm_stack … st2 →
     88           asm_is_io … st1 = asm_is_io … st2 →
     89           pc … st2 = new_pc →
     90           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
     91           vmstep … (cost_act (Some ? ltrue)) st1 st2
     92| vm_cjump_false :
     93           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
     94           eval_asm_cond p p' cond (asm_store … st1) = return false→
     95           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     96           asm_is_io … st1 = false →
     97           asm_store … st1 = asm_store … st2 →
     98           asm_stack … st1 = asm_stack … st2 →
     99           asm_is_io … st1 = asm_is_io … st2 →
     100           S (pc … st1) = pc … st2 →
     101           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
     102           vmstep … (cost_act (Some ? lfalse)) st1 st2
     103| vm_io_in : 
     104           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
     105           fetch … prog (pc … st1) = return (Iio p lin io lout) →
     106           asm_is_io … st1 = false →
     107           asm_store … st1 = asm_store … st2 →
     108           asm_stack … st1 = asm_stack … st2 →
     109           true = asm_is_io … st2 →
     110           pc … st1 = pc … st2 →
     111           cost … st1 = cost … st2 →
     112           vmstep … (cost_act (Some ? lin)) st1 st2
     113| vm_io_out :
     114           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
     115           fetch … prog (pc … st1) = return (Iio p lin io lout) →
     116           asm_is_io … st1 = true →
     117           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
     118           asm_stack … st1 = asm_stack … st2 →
     119           false = asm_is_io … st2 →
     120           S (pc … st1) = pc … st2 →
     121           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
     122           vmstep … (cost_act (Some ? lout)) st1 st2
     123| vm_call :
     124           ∀st1,st2 : vm_state p p'.∀f,lbl.
     125           fetch … prog (pc … st1) = return (Icall p f) →
     126           asm_is_io … st1 = false →
     127           asm_store … st1 = asm_store … st2 →
     128           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
     129           asm_is_io … st1 = asm_is_io … st2 →
     130           entry_of_function p  f = pc … st2 →
     131           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
     132           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
     133           vmstep … (call_act f lbl) st1 st2
     134| vm_ret :
     135          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
     136           fetch … prog (pc … st1) = return (Iret p) →
     137           asm_is_io … st1 = false →
     138           asm_store … st1 = asm_store … st2 →
     139           asm_stack … st1 = newpc ::  asm_stack … st2  →
     140           asm_is_io … st1 = asm_is_io … st2 →
     141           newpc = pc … st2 →
     142           label_of_pc ? (return_label_fun p) newpc = return lbl →
     143           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
     144           vmstep … (ret_act (Some ? lbl)) st1 st2.
     145           
     146include "../src/utilities/hide.ma".
     147
     148discriminator option.
     149
     150definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
     151λp,p',prog.mk_abstract_status
     152                (vm_state p p')
     153                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
     154                               vmstep p p' prog l st1 st2)
     155                (λ_.λ_.True)
     156                (λs.match fetch … prog (pc … s) with
     157                    [ Some i ⇒ match i with
     158                               [ Seq _ _ ⇒ cl_other
     159                               | Ijmp _ ⇒ cl_other
     160                               | CJump _ _ _ _ ⇒ cl_jump
     161                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
     162                               | Icall _ ⇒ cl_other
     163                               | Iret ⇒ cl_other
     164                               ]
     165                    | None ⇒ cl_other
     166                    ]
     167                )
     168                (λ_.true)
     169                (λs.eqb (pc ?? s) O)
     170                (λs.eqb (pc … s) (\snd prog))
     171                ???.
     172@hide_prf cases daemon (*
     173[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
     174  [ #_ #EQ destruct] * normalize nodelta
     175  [ #seq #lbl #_
     176  | #n #_
     177  | #cond #newpc #ltrue #lfalse #EQfetch
     178  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
     179  | #f #_
     180  | #_
     181  ]
     182  #EQ destruct * #_ #H inversion H in ⊢ ?;
     183  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
     184  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
     185  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
     186  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
     187  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
     188  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
     189  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
     190  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
     191  ]   
     192  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
     193  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
     194| #s1 #s2 #l inversion(fetch ???) normalize nodelta
     195  [ #_ #EQ destruct] * normalize nodelta
     196  [ #seq #lbl #_
     197  | #n #_
     198  | #cond #newpc #ltrue #lfalse #_
     199  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
     200  | #f #_
     201  | #_
     202  ]
     203  #EQ destruct * #_ #H inversion H in ⊢ ?;
     204  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
     205  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
     206  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
     207  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
     208  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
     209  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
     210  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
     211  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
     212  ]   
     213  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
     214|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
     215  [ #_ #EQ destruct] * normalize nodelta
     216  [ #seq #lbl #_
     217  | #n #_
     218  | #cond #newpc #ltrue #lfalse #EQfetch
     219  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
     220  | #f #_
     221  | #_
     222  ]
     223  #EQ destruct * #_ #H inversion H in ⊢ ?;
     224  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
     225  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
     226  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
     227  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
     228  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
     229  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
     230  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
     231  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
     232  ]   
     233  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
     234  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
     235]*)
     236qed.
     237
     238definition emits_labels ≝
     239λp.λinstr : AssemblerInstr p.match instr with
     240        [ Seq _ opt_l ⇒ match opt_l with
     241                        [ None ⇒ Some ? (λpc.S pc)
     242                        | Some _ ⇒ None ?
     243                        ]
     244        | Ijmp newpc ⇒ Some ? (λ_.newpc)
     245        | _ ⇒ None ?
     246        ].
     247
     248
     249let rec block_cost (p : assembler_params) (p' : sem_params p)
     250 (prog: AssemblerProgram p) (program_counter: ℕ)
     251    (program_size: ℕ)
     252        on program_size: option (m … p') ≝
     253match program_size with
     254  [ O ⇒ None ?
     255  | S program_size' ⇒
     256    if eqb program_counter (\snd prog) then
     257       return e … (m … p')
     258    else
     259    ! instr ← fetch … prog program_counter;
     260    ! n ← (match emits_labels … instr with
     261          [ Some f ⇒ block_cost … prog (f program_counter) program_size'
     262          | None ⇒ return e …
     263          ]);
     264    return (op … (m … p') (cost_of p p' instr) n)
     265  ].
     266 
     267axiom initial_act : CostLabel.
     268 
     269record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
     270{ map_type :> Type[0]
     271; empty_map : map_type
     272; get_map : map_type → dom → option codom
     273; set_map : map_type → dom → codom → map_type
     274; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
     275; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
     276}.
     277
     278let rec labels_pc (p : assembler_params)
     279(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
     280match prog with
     281[ nil ⇒ [〈initial_act,O〉] @
     282        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
     283        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
     284| cons i is ⇒
     285  match i with
     286  [ Seq _ opt_l ⇒ match opt_l with
     287                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
     288                  | None ⇒ [ ]
     289                  ]
     290  | Ijmp _ ⇒ [ ]
     291  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
     292  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
     293  | Icall f ⇒ [ ]
     294  | Iret ⇒ [ ]
     295  ] @ labels_pc p is (S program_counter)             
     296].
     297
     298definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.
     299∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝
     300λp,p',mT,prog.
     301let 〈instrs,final〉 ≝ prog in
     302let prog_size ≝ S (|instrs|) in
     303m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … prog w prog_size; 
     304                               return set_map … m z k) (labels_pc … instrs O)
     305      (empty_map ?? mT).
     306
     307(*falso: necessita di no_duplicates*)
     308axiom static_analisys_ok : ∀p,p',mT,prog,lbl,pc,map.
     309static_analisys p p' mT prog = return map →
     310mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
     311get_map … map lbl = block_cost … prog pc (S (|(\fst prog)|)). 
     312
     313include "Simulation.ma".
     314
     315record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2)
     316 : Prop ≝
     317 { R_label : option ActionLabel
     318 ; R_post_state : option S
     319 ; R_fin_ok : match R_label with
     320               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
     321               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
     322                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
     323                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
     324               ]
     325 }.
     326 
     327lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     328∀f : A → option B.∀y : B.
     329! x ← m; f x = return y →
     330∃ x.(m = return x) ∧ (f x = return y).
     331#A #B * [| #a] #f #y normalize #EQ [destruct]
     332%{a} %{(refl …)} //
     333qed.
     334
     335lemma static_dynamic : ∀p,p',prog,k,mT,map.
     336static_analisys p p' mT prog = return map →
     337∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     338pre_measurable_trace … t → terminated_trace … t →
     339block_cost … prog (pc … st1) (S (|(\fst prog)|)) = return k →
     340op … (m … p') (cost … st1)
     341 (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1)
     342     k (get_costlabels_of_trace … t)) = cost … st2.
     343[2: cases daemon]
     344#p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t
     345[ #st #_ ** [|#r_lab] normalize nodelta #opt_r_state
     346  [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st
     347    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     348    >neutral %
     349  | ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?);
     350    >H3 normalize nodelta #H cases(bind_inversion ????? H) -H
     351    #i * #EQi #H cases(bind_inversion ????? H) -H #el
     352    inversion H4
     353    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
     354      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
     355      #EQ destruct whd in match emits_labels; normalize nodelta
     356      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
     357      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
     358      #EQ destruct whd in match (foldr ?????);
     359
     360
     361
     362
Note: See TracChangeset for help on using the changeset viewer.