Last change
on this file since 2898 was
2845,
checked in by piccolo, 8 years ago

ERTLptr to LTL correctness proof started

File size:
995 bytes

Line  

1  include "ERTLptr/liveness.ma". 

2  

3  inductive decision: Type[0] ≝ 

4   decision_spill: nat → decision 

5   decision_colour: Register → decision. 

6  

7  (* prop_colouring is the non interferece 

8  prop_colouring 2 and 3 together say that spilled_no is the number of spilled 

9  registers *) 

10  (* Wilmer: the generation of the destruct principle diverges; 

11  CtrC make the file pass *) 

12  record coloured_graph (after: valuation register_lattice): Type[1] ≝ 

13  { colouring: vertex → decision 

14  ; spilled_no: nat 

15  ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 

16  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2 

17  ; prop_spilled_no: (*CSC: the existguarded premise is just to make the proof more general *) 

18  ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no 

19  }. 

20  

21  definition coloured_graph_computer ≝ 

22  ∀globals. 

23  joint_internal_function ERTLptr globals → 

24  ∀valuation. 

25  coloured_graph valuation. 

Note: See
TracBrowser
for help on using the repository browser.