Changeset 2725 for src/common


Ignore:
Timestamp:
Feb 25, 2013, 11:45:57 AM (7 years ago)
Author:
campbell
Message:

Add observables to FEMeasurable proof; fix silly typo.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2690 r2725  
    586586  ms_compiled MS p1 p2 →
    587587  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'.
    589591#MS #p1 #p2 #m #n #stack_cost #max #compiled
    590592* #s0 * #prefix * #s1 * #interesting * #s2
    591 whd in ⊢ (? → ??(λ_.??(λ_.%)));
     593whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%)))));
    592594letin g ≝ (make_global … (pcs_exec … ) p1)
    593595letin g' ≝ (make_global … (pcs_exec … ) p2)
     
    606608#n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS'
    607609
    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' %
    619628] qed.
  • src/common/Measurable.ma

    r2722 r2725  
    400400  ! s0 ← make_initial_state … p;
    401401  ! 〈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;
    403403  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
    404404  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
Note: See TracChangeset for help on using the changeset viewer.