 Timestamp:
 Mar 28, 2013, 7:49:22 PM (7 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2728 r3022 626 626 ] qed. 627 627 628 629 definition 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 1 1 include "RTLabs/CostSpec.ma". 2 3 (* This isn't quite right  it should be injective over all PCs, not just 4 perfunction. *) 2 5 3 6 (* Check that the RTLabs pc → cost label map is injective for a given RTLabs … … 128 131 λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f  _ ⇒ true ]) (prog_funct … p). 129 132 130 theorem check_pro ject_cost_injectivity_ok : ∀p.133 theorem check_program_cost_injectivity_ok : ∀p. 131 134 bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p. 132 135 #p % … … 143 146 144 147 148 definition 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. 145 156 
src/compiler.ma
r3021 r3022 69 69 let p ≝ cminor_to_rtlabs p in 70 70 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〉. 78 74 79 75 (* The compiler backend *) 
src/correctness.ma
r3021 r3022 126 126 #p_loc #EQ_assembler 127 127 whd 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 128 134 #NOT_WRONG % 129 [ cases daemon (* TODO *)135 [ destruct cases daemon (* TODO *) 130 136  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 131 137
Note: See TracChangeset
for help on using the changeset viewer.