machine-code/graph/GraphLangScript.sml

191   (exec_next locs (IF guard n1 n2) s t w call =
192      if guard s then exec_next locs n1 s t w call
193                 else exec_next locs n2 s t w call) /\
194   (exec_next locs (ASM assert update jmp) s t w call =
198   (exec_next locs (CALL assert update name jmp) s t w call =
201      locs name <> NONE /\
202      check_jump (Jump (THE (locs name))) t w /\
352   IMPL_INST code locs (Inst n assert next) =
355       assert s /\ exec_next locs next s t w call ==>
363   ``IMPL_INST code locs (Inst pc1 assert1 next1) /\
364     IMPL_INST code locs (Inst pc1 assert2 next2) ==>
366     !guard. IMPL_INST code locs (Inst pc1 assert1 (IF guard next1 next2))``,
370   ``IMPL_INST code locs (Inst pc1 assert1 next1) /\
371     IMPL_INST code locs (Inst pc1 assert2 next2) ==>
372     !guard. IMPL_INST code locs
378   ``IMPL_INST code locs
381     IMPL_INST code locs
387   ``(IMPL_INST code locs
389      IMPL_INST code locs
391     (IMPL_INST code locs
393      IMPL_INST code locs
398   ``IMPL_INST c locs (Inst n b (IF g (ASM x u (Jump j)) next)) <=>
399     IMPL_INST c locs (Inst n (\s. b s /\ g s) (ASM x u (Jump j))) /\
400     IMPL_INST c locs (Inst n (\s. b s /\ ~(g s)) next)``,
405   ``IMPL_INST c locs (Inst n (K T) (IF g next1 next2)) ==>
406     !a. (!s. a s ==> g s) ==> IMPL_INST c locs (Inst n a next1)``,
411   ``IMPL_INST c locs (Inst n (K T) (IF g next1 next2)) ==>
412     !a. (!s. a s ==> ($~ o g) s) ==> IMPL_INST c locs (Inst n a next2)``,
417   ``IMPL_INST c locs (Inst n (K T) next) ==>
418     !a. IMPL_INST c locs (Inst n a next)``,
423   ``IMPL_INST c locs (Inst n b (IF g (ASM pre u1 (Jump w)) next)) /\
424     IMPL_INST c locs (Inst w g (ASM NONE [] (Jump j))) ==>
426     IMPL_INST c locs (Inst n b (IF g (ASM pre u1 (Jump j)) next))``,
446   ``IMPL_INST c locs (Inst n b (IF g next (ASM pre u1 (Jump w)))) /\
447     IMPL_INST c locs (Inst w ($~ o g) (ASM NONE [] (Jump j))) ==>
449     IMPL_INST c locs (Inst n b (IF g next (ASM pre u1 (Jump j))))``,
1031   ``func_ok code locs f ==>
1036         func_ok c locs f``,
1491   ``func_ok code locs f /\
1492     EVERY (func_ok code locs) fs ==>
1493     EVERY (func_ok code locs) (f::fs)``,
1998   ``IMPL_INST code locs
2004       (locs name = SOME entry) ==>
2005       IMPL_INST code locs