Changeset 3252


Ignore:
Timestamp:
May 3, 2013, 5:29:36 PM (4 years ago)
Author:
piccolo
Message:

proof obbligation added on ERTL to LTL proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLProof.ma

    r3217 r3252  
    14461446let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
    14471447let stacksizes ≝ lookup_stack_cost … m in
    1448 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
    1449 b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
    1450   init prog init_regs f_lbls f_regs →
     1448let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
    14511449cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
    14521450 init init_regs
     
    14541452 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
    14551453[2: @hide_prf %]
    1456 #fix_comp #colour #prog #init_regs #f_lbls #f_regs #good
     1454#fix_comp #colour #prog #init_regs #f_lbls #f_regs
    14571455whd in match cond_commutation_statement; normalize nodelta
    14581456#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
     
    15531551qed.
    15541552           
    1555            
    1556 axiom ERTLToLTL_ok :
     1553lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1554let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1555let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1556let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1557let stacksizes ≝ lookup_stack_cost … m in
     1558let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1559seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
     1560 init init_regs
     1561 f_lbls f_regs (state_rel fix_comp colour prog)
     1562 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1563[2: @hide_prf %]
     1564cases daemon (*TODO*)
     1565qed.
     1566
     1567lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1568let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1569let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1570let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1571let stacksizes ≝ lookup_stack_cost … m in
     1572let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1573return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
     1574 init init_regs
     1575 f_lbls f_regs (state_rel fix_comp colour prog)
     1576 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1577[2: @hide_prf %]
     1578cases daemon (*TODO*)
     1579qed.
     1580
     1581lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1582let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1583let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1584let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1585let stacksizes ≝ lookup_stack_cost … m in
     1586let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1587b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
     1588  init prog init_regs f_lbls f_regs →
     1589pre_main_commutation_statement  ERTL_semantics LTL_semantics prog stacksizes
     1590 init init_regs
     1591 f_lbls f_regs (state_rel fix_comp colour prog)
     1592 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1593[2: @hide_prf %]
     1594cases daemon qed.
     1595
     1596(*
     1597#fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd
     1598#st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta
     1599whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta
     1600whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
     1601#_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H ** #f #fn #stmt
     1602#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #stmt1
     1603#H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?); cases st1 in EQbl; -st1
     1604#st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 -pos1 normalize nodelta
     1605[ #EQ destruct(EQ)
     1606|*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
     1607]
     1608whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1))
     1609*)
     1610
     1611lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1612let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1613let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1614let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1615let stacksizes ≝ lookup_stack_cost … m in
     1616let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1617call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
     1618 init init_regs
     1619 f_lbls f_regs (state_rel fix_comp colour prog)
     1620 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1621[2: @hide_prf %]
     1622cases daemon qed.
     1623
     1624lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1625let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1626let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1627let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1628let stacksizes ≝ lookup_stack_cost … m in
     1629let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1630goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
     1631 init init_regs
     1632 f_lbls f_regs (state_rel fix_comp colour prog)
     1633 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1634[2: @hide_prf %]
     1635cases daemon qed.
     1636
     1637lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     1638let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1639let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1640let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
     1641let stacksizes ≝ lookup_stack_cost … m in
     1642let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1643tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
     1644 init init_regs
     1645 f_lbls f_regs (state_rel fix_comp colour prog)
     1646 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
     1647[2: @hide_prf %]
     1648#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2
     1649#f #fn *
     1650qed.
     1651
     1652             
     1653theorem ERTLToLTL_ok :
    15571654∀fix_comp : fixpoint_computer.
    15581655∀colour : coloured_graph_computer.
     
    15601657let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
    15611658(* what should we do with n? *)
    1562 let stacksizes ≝ stack_sizes m in
     1659let stacksizes ≝ lookup_stack_cost m in
    15631660∀init_in.make_initial_state
    15641661  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
     
    15721669    (joint_status LTL_semantics p_out stacksizes)
    15731670    R init_in init_out.
     1671#fix_comp #colour #p_in #init_in #EQinit_in
     1672letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in)))
     1673letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in)))
     1674letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in))
     1675letin stacksizes ≝ (lookup_stack_cost m)
     1676cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
     1677     (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
     1678#init_regs * #f_lbls * #f_regs #good
     1679@(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes
     1680(λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)»)
     1681init_regs f_lbls f_regs (state_rel fix_comp colour p_in)
     1682(state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in)
     1683%
     1684[ @good
     1685| #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn}
     1686  @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn)
     1687| #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn)
     1688| #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel;
     1689  normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta
     1690  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
     1691  >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta
     1692  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) assumption
     1693| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd
     1694  lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn *
     1695  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames
     1696  normalize nodelta #EQst whd in match sigma_fb_state_pc;
     1697  whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     1698  normalize nodelta @eq_f3 [2,3: % | assumption]
     1699| @pre_main_commute assumption
     1700| #f #fn * #bl #pos #EQbl whd in match fetch_statement;
     1701  whd in match fetch_internal_function; whd in match fetch_function;
     1702  normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
     1703  #_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H #stmt 
     1704  #H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?);
     1705  whd in match point_of_pc; normalize nodelta cases pos normalize nodelta
     1706  [ #EQ destruct(EQ)
     1707  |*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
     1708  ]
     1709  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1710| @cond_commute
     1711| @seq_commute
     1712| #f #fn #bl #EQfn #id #args #dest #lbl whd #bl'
     1713  %{(match id with [inl f1 ⇒ inl ?? f1 | inr x ⇒ inr ?? 〈it,it〉])}
     1714  %{args} %{it} normalize nodelta cases id [ #f1 % | * #dpl #dph %]
     1715| cases daemon (*TODO*)
     1716| @return_commute
     1717| @call_commute
     1718| @goto_commute
     1719| @tailcall_commute
     1720| cases daemon (*TODO*)
     1721| cases daemon (*TODO*)
     1722| cases daemon (*TODO*)
     1723| cases daemon (*TODO*)
     1724]
     1725qed.
Note: See TracChangeset for help on using the changeset viewer.