Changeset 2725
 Timestamp:
 Feb 25, 2013, 11:45:57 AM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2690 r2725 586 586 ms_compiled MS p1 p2 → 587 587 measurable (ms_C1 MS) p1 m n stack_cost max → 588 ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max. 588 ∃m',n'. 589 measurable (ms_C2 MS) p2 m' n' stack_cost max ∧ 590 observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. 589 591 #MS #p1 #p2 #m #n #stack_cost #max #compiled 590 592 * #s0 * #prefix * #s1 * #interesting * #s2 591 whd in ⊢ (? → ??(λ_.??(λ_. %)));593 whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%))))); 592 594 letin g ≝ (make_global … (pcs_exec … ) p1) 593 595 letin g' ≝ (make_global … (pcs_exec … ) p2) … … 606 608 #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' 607 609 608 %{m'} %{n'} %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'} 609 % [ % [ % [ % [ % 610 [ assumption 611  assumption 612 ] assumption 613 ] @(build_label_to_ret … EXEC1' ? ENDS') 614 [ #s #CS @(ms_labelled_normal_2 … CS) 615  <(ms_rel_labelled … R1) @CS1 616 ] 617 ] @RETURNS' 618 ] cases daemon (* TODO! *) 610 %{m'} %{n'} % 611 [ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'} 612 % [ % [ % [ % [ % 613 [ assumption 614  assumption 615 ] assumption 616 ] @(build_label_to_ret … EXEC1' ? ENDS') 617 [ #s #CS @(ms_labelled_normal_2 … CS) 618  <(ms_rel_labelled … R1) @CS1 619 ] 620 ] @RETURNS' 621 ] cases daemon (* TODO! *) 622 ] 623  >INIT >INIT' 624 whd in ⊢ (??%%); >EXEC0 >EXEC0' 625 whd in ⊢ (??%%); >EXEC1 >EXEC1' 626 whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %; 627 #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % 619 628 ] qed. 
src/common/Measurable.ma
r2722 r2725 400 400 ! s0 ← make_initial_state … p; 401 401 ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; 402 ! 〈interesting,s2〉 ← exec_steps m?? (cs_exec … C') g s1;402 ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1; 403 403 let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in 404 404 return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
Note: See TracChangeset
for help on using the changeset viewer.