Changeset 2264 for src/ASM/Policy.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2230 r2264  
    3030          ] (refl … z)
    3131  ] (refl … n).
    32 [5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) //
     32[5: #l #_ %
    3333| normalize nodelta cases (jump_expansion_start program (create_label_map program))
    3434  #x cases x -x
     
    262262  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
    263263  ].
    264 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ]
     264[2: #l #_ %]
    265265#program #policy #l elim l -l;
    266266[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
     
    332332  [ None ⇒ True
    333333  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
    334 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]
     334[2: #l #_ %]
    335335#program #policy inversion (jump_expansion_step ???)
    336336#p cases p -p #ch #pol normalize nodelta cases pol
Note: See TracChangeset for help on using the changeset viewer.