Changeset 2942 for src/ERTLptr/Interference.ma

Timestamp:

Mar 23, 2013, 1:37:22 AM (7 years ago)

Author:

sacerdot

Message:

Many changes:

1. Coloured graphs are now specified in terms of livebefore
2. Type of livebefore changed so that it is now a valuation transformer
3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File:

• src/ERTLptr/Interference.ma (modified) (1 diff)

src/ERTLptr/Interference.ma

@@ -8 +8 @@
    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] ≝
+record coloured_graph (before: valuation register_lattice): Type[1] ≝
 { colouring: vertex → decision
 ; spilled_no: nat
 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 
-  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
+  lives v1 (before l) → lives v2 (before 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
+   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
 }.
 
 definition coloured_graph_computer ≝
  ∀globals.
-  joint_internal_function ERTLptr globals →
-   ∀valuation.
-    coloured_graph valuation.
+  ∀fn:joint_internal_function ERTLptr globals.
+   ∀liveafter.
+    coloured_graph (livebefore globals fn liveafter).