Changeset 3145 for src/ERTL


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r3072 r3145  
    33include "ASM/Arithmetic.ma".
    44include "joint/TranslateUtils.ma".
     5include "joint/joint_stacksizes.ma".
    56
    67(* Note: translation is complicated by having to preserve the carry bit and
     
    441442%
    442443qed.
     444
     445lemma ERTLToLTL_monotone_stacksizes :
     446∀fix,col.
     447∀p_in.
     448let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in
     449stack_cost_model_le (stack_cost ? p_in) cost_m.
     450#fix #col #p_in whd
     451@list_map_opt_All2
     452[ @(λid_def1,id_def2.
     453   match \snd id_def1 with
     454   [ Internal f1 ⇒
     455     match \snd id_def2 with
     456     [ Internal f2 ⇒
     457       \fst id_def1 = \fst id_def2 ∧
     458       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
     459     | _ ⇒ False
     460     ]
     461   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     462   ])
     463| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     464  ** #H %{H} % ]
     465@All2_of_map * #id * #f normalize nodelta [2: %]
     466% [%]
     467cases (b_graph_translate ?????) #f_out * #data **
     468[2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data
     469#props >(ss_def_out_eq … props) >EQ_data
     470generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??);
     471-p_in //
     472qed.
     473
  • src/ERTL/ERTLToLTLAxiom.ma

    r3096 r3145  
    66include "common/AssocList.ma".
    77
    8 (* Inefficient, replace with Trie lookup *)
    9 definition lookup_stack_cost ≝
    10  λp.λid : ident.
    11   assoc_list_lookup ? ℕ id (eq_identifier …) p.
    12 
    138axiom ERTLToLTL_ok :
    149∀fix_comp : fixpoint_computer.
     
    1712let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
    1813(* what should we do with n? *)
    19 let stacksizes ≝ lookup_stack_cost m in
     14let stacksizes ≝ stack_sizes m in
    2015∀init_in.make_initial_state
    2116  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
Note: See TracChangeset for help on using the changeset viewer.