include "ERTLptr/liveness.ma".
inductive decision: Type[0] ≝
| decision_spill: nat → decision
| decision_colour: Register → decision.
(* prop_colouring is the non interferece
prop_colouring 2 and 3 together say that spilled_no is the number of spilled
registers *)
(* Wilmer: the generation of the destruct principle diverges;
Ctr-C make the file pass *)
record coloured_graph (after: valuation register_lattice): Type[1] ≝
{ colouring: vertex → decision
; spilled_no: nat
; prop_colouring: ∀l. ∀v1, v2: vertex.
lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
}.
definition coloured_graph_computer ≝
∀globals.
joint_internal_function ERTLptr globals →
∀valuation.
coloured_graph valuation.