source: src/ERTL/Interference.ma @ 2183

Last change on this file since 2183 was 1730, checked in by sacerdot, 9 years ago

Minor changes while studying the proof.

File size: 1.3 KB
RevLine 
[1229]1include "ERTL/ERTL.ma".
2include "ERTL/liveness.ma".
[1127]3
[1229]4definition vertex ≝ register ⊎ Register.
5
6inductive decision: Type[0] ≝
[1232]7  | decision_spill: nat → decision
[1229]8  | decision_colour: Register → decision.
9
[1232]10definition is_member ≝
11  λvertex.
12  λregister_lattice.
13  let 〈l, r〉 ≝ register_lattice in
14  match vertex with
15  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
16  | inr v ⇒ set_member ? eq_Register v r
17  ].
18
[1423]19(* prop_colouring is the non interferece
20   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
21   registers *)
22(* Wilmer: the generation of the destruct principle diverges;
23   Ctr-C make the file pass *)
[1232]24record coloured_graph (v: valuation): Type[1] ≝
[1423]25{ colouring: vertex → decision
26; spilled_no: nat
27; prop_colouring: ∀l. ∀v1, v2: vertex.
28   is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
[1730]29; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *)
[1423]30   ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
[1730]31(* CSC: useless for the proof and very weak
[1423]32; prop_colouring3:
33   spilled_no = 0 ∨
34    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
[1730]35*)
[1229]36}.
37
[1232]38axiom build: ∀valuation. coloured_graph valuation.
Note: See TracBrowser for help on using the repository browser.