Changeset 3022


Ignore:
Timestamp:
Mar 28, 2013, 7:49:22 PM (4 years ago)
Author:
campbell
Message:

Make a couple of tests monadic for easier inversion.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2728 r3022  
    626626] qed.
    627627
     628
     629definition check_cost_program_prf : ∀p:RTLabs_program. res (well_cost_labelled_program p) ≝
     630λp. (match check_cost_program p return λb. bool_to_Prop b ↔ well_cost_labelled_program p → res ? with
     631     [ true ⇒ λH. OK ??
     632     | false ⇒ λ_. Error ? (msg BadCostLabelling)
     633     ])
     634    (check_cost_program_ok p).
     635@(proj1 … H)
     636% qed.
     637
  • src/RTLabs/CostInj.ma

    r2937 r3022  
    11include "RTLabs/CostSpec.ma".
     2
     3(* This isn't quite right - it should be injective over all PCs, not just
     4   per-function. *)
    25
    36(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
     
    128131λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).
    129132
    130 theorem check_project_cost_injectivity_ok : ∀p.
     133theorem check_program_cost_injectivity_ok : ∀p.
    131134  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
    132135#p %
     
    143146
    144147
     148definition check_program_cost_injectivity_prf : ∀p:RTLabs_program. res (program_cost_injectivity p) ≝
     149λp. (match check_program_cost_injectivity p return λb. bool_to_Prop b ↔ program_cost_injectivity p → res ? with
     150     [ true ⇒ λH. OK ??
     151     | false ⇒ λ_. Error ? (msg BadCostLabelling)
     152     ])
     153    (check_program_cost_injectivity_ok p).
     154@(proj1 … H)
     155% qed.
    145156
  • src/compiler.ma

    r3021 r3022  
    6969  let p ≝ cminor_to_rtlabs p in
    7070  let i ≝ observe rtlabs_pass p in
    71   if check_cost_program p then
    72     if check_program_cost_injectivity p then
    73       (return 〈init_cost,p',p〉)
    74     else
    75       (Error ? (msg RepeatedCostLabel))
    76   else
    77     (Error ? (msg BadCostLabelling)).
     71  ! WCL ← check_cost_program_prf p;
     72  ! INJ ← check_program_cost_injectivity_prf p;
     73  return 〈init_cost,p',p〉.
    7874
    7975(* The compiler back-end *)
  • src/correctness.ma

    r3021 r3022  
    126126#p_loc #EQ_assembler
    127127whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     128
     129@('bind_inversion EQ_front_end) #cminor #CMINOR
     130#H @('bind_inversion H) -H #WCL #_
     131#H @('bind_inversion H) -H #INJ #_
     132#EQ_front_end'
     133
    128134#NOT_WRONG %
    129 [ cases daemon (* TODO *)
     135[ destruct cases daemon (* TODO *)
    130136| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    131137
Note: See TracChangeset for help on using the changeset viewer.