Changeset 2264 for src/ASM/Policy.ma

Timestamp:

Jul 26, 2012, 12:38:42 AM (7 years ago)

Author:

sacerdot

Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:

• src/ASM/Policy.ma (modified) (3 diffs)

src/ASM/Policy.ma

@@ -30 +30 @@
           ] (refl … z)
   ] (refl … n).
-[5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) // 
+[5: #l #_ %
 | normalize nodelta cases (jump_expansion_start program (create_label_map program))
   #x cases x -x
@@ -262 +262 @@
   | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
   ].
-[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ]
+[2: #l #_ %]
 #program #policy #l elim l -l;
 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
@@ -332 +332 @@
   [ None ⇒ True
   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
-[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]
+[2: #l #_ %]
 #program #policy inversion (jump_expansion_step ???)
 #p cases p -p #ch #pol normalize nodelta cases pol