To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit a52438d8 authored by Adam Nelson's avatar Adam Nelson
Browse files

Partial work on optimizationsTheory

uvmOptimizationsTheory proves the validity of optimizations on Mu
bytecode. Incomplete proofs are stubbed out with "cheat" or commented
out.
parent 68dd6b4a
......@@ -7,5 +7,7 @@ sig
val multi_case_tac : tactic
val rw_assums : thm list -> tactic
val rw_assums_once : thm list -> tactic
end
......@@ -19,5 +19,8 @@ struct
fun rw_assums xs =
POP_ASSUM_LIST (map_every (assume_tac o REWRITE_RULE xs) o rev)
fun rw_assums_once xs =
POP_ASSUM_LIST (map_every (assume_tac o ONCE_REWRITE_RULE xs) o rev)
end
open HolKernel Parse boolLib bossLib;
open sumSyntax
open monadsLib
open listTheory
(* Monads for options, lists, and sum types.
......@@ -32,6 +33,9 @@ val bind_left_INR = store_thm("bind_left_INR",
``(y. x = INR y) f. bind_left x f = x``,
Cases_on `x` >> simp[])
val bind_left_case = store_thm("bind_left_case",
``a f. bind_left a f = case a of INL l => f l | INR r => INR r``,
Cases >> rw[])
val bind_right_def = Define`
bind_right (sum : α + β) (fn : β -> α + γ) : α + γ =
......@@ -117,6 +121,16 @@ val right_list_def = Define`
right_list (sum : α + β) = case sum of INL _ => [] | INR b => [b]
`
val sequence_left_length = store_thm("sequence_left_length",
``xs xs'. (sequence_left xs = INL xs') (LENGTH xs = LENGTH xs')``,
Induct >> rw[] >> fs[definition "sequence_left_def"] >>
prove_tac[LENGTH_CONS])
val el_sequence_left = store_thm("el_sequence_left",
``xs xs' n. (sequence_left xs = INL xs') n < LENGTH xs
(EL n xs = INL (EL n xs'))``,
Induct >> rw[] >> fs[definition "sequence_left_def"] >> Cases_on `n` >> rw[])
(* Monad laws for bind_left: left identity, right identity, and associativity *)
val bind_left_monad_left_id = store_thm("bind_left_monad_left_id[simp]",
``bind_left (INL a) f = f a``, simp[])
......
......@@ -64,13 +64,30 @@ val lift_err_msg_def = Define`
functionality are included in the default simpset.
*)
val or_fail_OK_proves = Q.store_thm("or_fail_OK_proves[simp]",
`opt e. (opt or_fail e = OK x) = (opt = SOME x)`,
val or_fail_OK_proves = store_thm("or_fail_OK_proves[simp]",
``opt e. (opt or_fail e = OK x) = (opt = SOME x)``,
Cases >> rw[])
val assert_OK_proves = store_thm("assert_OK_proves[simp]",
``P e. (assert P or_fail e = OK ()) = P``,
Cases >> rw[])
val assert_Fail_proves = store_thm("assert_Fail_proves[simp]",
``P e e'. (assert P or_fail e = Fail e') (e' = e ¬P)``,
Cases >> rw[] >> prove_tac[])
val lift_err_msg_OK = store_thm("lift_err_msg_OK[simp]",
``x f y. (lift_err_msg f x = OK y) (x = OK y)``,
Cases >| [rw[lift_err_msg_def], Cases_on `y` >> rw[lift_err_msg_def]])
val lift_err_msg_Fail = store_thm("lift_err_msg_Fail[simp]",
``x y f. (lift_err_msg f x = Fail y)
(case y of
| UndefBehavior m => (m'. m = f m' x = Fail (UndefBehavior m'))
| Impossible m => x = Fail (Impossible m)
| NotImplemented m => x = Fail (NotImplemented m))``,
Cases >> Cases >> rw[lift_err_msg_def] >> Cases_on `y` >>
simp[lift_err_msg_def] >> prove_tac[])
val _ = export_theory()
......@@ -7,6 +7,7 @@ open uvmErrorsTheory
open monadsTheory
open monadsLib
open syntaxSugarTheory
open extraTactics
open alistTheory
open combinTheory
......@@ -65,6 +66,26 @@ val run_reg_reader_def = Define`
r (λn. FST <$> (lookup n regs or_fail Impossible "undefined register"))
`
val reads_reg_def = Define`
reads_reg (r : num) (rdr : α reg_reader)
regs c. run_reg_reader rdr regs run_reg_reader rdr (insert r c regs)
`
val reads_reg_return = store_thm("reads_reg_return",
``r x. ¬reads_reg r (return x)``,
rw[reads_reg_def, run_reg_reader_def])
val reads_reg_get = store_thm("reads_reg_get",
``ssa v r n. n < LENGTH (ssa v)
(r = FST (EL n (ssa v)) reads_reg r (EL n (get ssa v)))``,
rw[reads_reg_def, get_def, run_reg_reader_def] >> EQ_TAC >| [
strip_tac >> map_every qexists_tac [`LN`, `UndefV Void, [Void], []`] >>
rw[EL_MAP, lookup_def, lookup_insert, lift_left_def],
rw[EL_MAP, lookup_insert, lift_left_def] >> spose_not_then assume_tac >>
fs[]
])
val _ = Datatype`
jumps = <|
nor_jump : num # (num + value) list;
......@@ -135,6 +156,14 @@ val _ = Datatype`
val _ = type_abbrev("program", ``:func_name |-> opn_block spt``)
val opn_reads_reg_def = Define`
opn_reads_reg r (Nm rdr) = reads_reg r rdr
opn_reads_reg r (Ld rdr _) = reads_reg r rdr
opn_reads_reg r (St rdr) = reads_reg r rdr
opn_reads_reg r (Cmd rdr) = reads_reg r rdr
opn_reads_reg _ _ = F
`
val eval_expr_def = Define`
eval_expr (ssa : ssa_map) (Id _ v : expression) : value list reg_reader =
sequence (getc ssa v)
......@@ -438,5 +467,25 @@ val compile_program_def = Define`
od)
`
val is_jump_cmd_def = Define`
is_jump_cmd (DoPushStack _ _ _ _) = T
is_jump_cmd (DoPopStack _) = T
is_jump_cmd (DoJump _ _) = T
is_jump_cmd DoThreadExit = T
is_jump_cmd _ = F
`
val is_jump_opn_def = Define`
is_jump_opn (Cmd rdr) =
(cmd regs. run_reg_reader rdr regs = OK cmd is_jump_cmd cmd)
is_jump_opn _ = F
`
val opns_ok_def = Define`
opns_ok = COMPL NULL
COMPL (EXISTS is_jump_opn o FRONT)
is_jump_opn o LAST
`
val _ = export_theory()
......@@ -80,6 +80,10 @@ val _ = type_abbrev("mem_error", ``:('addr # mem_error_message) error``)
val _ = type_abbrev("mem_cell", ``:value # uvm_type list # num list``)
val _ = type_abbrev("mem_region", ``:mem_cell spt``)
val max_key_def = Define`max_key = foldi (λn _ m. MAX n m) 0 0`
val next_key_def = Define`next_key t = if isEmpty t then 0 else SUC (max_key t)`
val mem_cell_types_def = Define`
mem_cell_types (sz : num option)
(ty : uvm_type)
......@@ -139,8 +143,8 @@ val _ = Datatype`
val _ = Datatype`
address_space = <|
globals : α spt;
heap : num # α spt;
stack : (num # α spt) spt
heap : α spt;
stack : α spt spt
|>
`
......@@ -150,9 +154,9 @@ val _ = type_abbrev("buffer", ``:value list address_space``)
val address_space_ok_def = Define`
address_space_ok (as : α address_space)
wf as.globals
wf (SND as.heap)
wf as.heap
wf as.stack
EVERY (wf o SND) (toList as.stack)
EVERY wf (toList as.stack)
`
val mem_cell_ok_def = Define`
......@@ -181,19 +185,14 @@ val mem_region_ok_def = Define`
val memory_ok_def = Define`
memory_ok mem
let region_ok (n, r) = (mem_region_ok r k. k domain r k < n)
in mem_region_ok mem.globals
wf mem.stack
region_ok mem.heap
EVERY region_ok (toList mem.stack)
mem_region_ok mem.globals
wf mem.stack
mem_region_ok mem.heap
EVERY mem_region_ok (toList mem.stack)
`
val new_address_space_def = Define`
new_address_space = <|
globals := LN;
heap := (0, LN);
stack := LN
|>
new_address_space = <| globals := LN; heap := LN; stack := LN |>
`
val new_memory_def = Define`
......@@ -214,8 +213,8 @@ val new_memory_def = Define`
val addrs_of_def = Define`
addrs_of (as : α address_space) : addr list =
MAP ($, Global o FST) (toAList as.globals) ++
MAP ($, Heap o FST) (toAList (SND as.heap)) ++ do
(sn, _, region) <- toAList as.stack;
MAP ($, Heap o FST) (toAList as.heap) ++ do
(sn, region) <- toAList as.stack;
(n, _) <- toAList region;
return (Stack (StackID (nfst sn)) (FrameID (nsnd sn)), n)
od
......@@ -223,19 +222,19 @@ val addrs_of_def = Define`
val get_region_def = Define`
get_region as Global = as.globals
get_region as Heap = SND as.heap
get_region as Heap = as.heap
get_region as (Stack sid fid) =
option_CASE (lookup (stack_id_dest sid frame_id_dest fid) as.stack) LN SND
THE (OPTION_CHOICE
(lookup (stack_id_dest sid frame_id_dest fid) as.stack)
(SOME LN))
`
val put_region_def = Define`
put_region as Global r = as with globals := r
put_region as Heap r = as with heap :=
(SUC (foldi (K o MAX) 0 0 r), r)
put_region as Heap r = as with heap := r
put_region as (Stack sid fid) r =
as with stack updated_by
insert (stack_id_dest sid frame_id_dest fid)
(SUC (foldi (K o MAX) 0 0 r), r)
insert (stack_id_dest sid frame_id_dest fid) r
`
val get_addr_def = Define `get_addr as (a, n) = lookup n (get_region as a)`
......@@ -244,13 +243,34 @@ val put_addr_def = Define`
put_addr as (a, n) v = put_region as a (insert n v (get_region as a))
`
val map_with_keys_def = Define`
map_with_keys (f : num -> α -> β) (t : α spt) : β spt =
fromAList (MAP (λ(k, v). k, f k v) (toAList t))
`
val merge_def = Define`
merge f t1 t2 =
union (map_with_keys (λk v1. case lookup k t2 of
| SOME v2 => f v1 v2
| NONE => v1) t1)
t2
`
val address_space_union_def = Define`
address_space_union a1 a2 = a2 with <|
globals updated_by union a1.globals;
heap updated_by union a1.heap;
stack updated_by merge union a1.stack
|>
`
val memory_heap_alloc_def = Define`
memory_heap_alloc (mem : memory)
(sz : num option)
(ty : uvm_type)
: (memory # addr) + ε error = do
(allocated, heap) <-
region_alloc (SND mem.heap) sz ty (λn. n, SUC n) (FST mem.heap);
(allocated, _, heap) <-
region_alloc mem.heap sz ty (λn. n, SUC n) (next_key mem.heap);
return (mem with heap := heap, (Heap, allocated))
od
`
......@@ -263,9 +283,9 @@ val memory_stack_alloc_def = Define`
(ty : uvm_type)
: (memory # addr) + ε error =
let key = stack_id_dest sid frame_id_dest fid;
(n, s) = option_CASE (lookup key mem.stack) (0, LN) I
s = THE (OPTION_CHOICE (lookup key mem.stack) (SOME LN));
in do
(allocated, s') <- region_alloc s sz ty (λn. n, SUC n) n;
(allocated, _, s') <- region_alloc s sz ty (λn. n, SUC n) (next_key s);
return ((mem with stack updated_by insert key s'),
(Stack sid fid, allocated))
od
......@@ -281,11 +301,11 @@ val buffer_enqueue_def = Define`
let ins t = insert n (v::option_CASE (lookup n t) [] I) t in
case a of
| Global => buf with globals updated_by ins
| Heap => buf with heap updated_by I ## ins
| Heap => buf with heap updated_by ins
| Stack sid fid =>
let key = stack_id_dest sid frame_id_dest fid in
buf with stack updated_by λs.
insert key ((I ## ins) (option_CASE (lookup key s) (0, LN) I)) s
insert key (ins (THE (OPTION_CHOICE (lookup key s) (SOME LN)))) s
`
val buffer_dequeue_def = Define`
......@@ -298,12 +318,12 @@ val buffer_dequeue_def = Define`
| Global =>
((λt. buf with globals := t) ## I) <$> deq buf.globals
| Heap =>
((λt. buf with heap := (0, t)) ## I) <$> deq (SND buf.heap)
((λt. buf with heap := t) ## I) <$> deq buf.heap
| Stack sid fid =>
let key = stack_id_dest sid frame_id_dest fid in do
(_, fr) <- lookup key buf.stack;
fr <- lookup key buf.stack;
(t, old) <- deq fr;
return (buf with stack updated_by insert key (0, t), old)
return (buf with stack updated_by insert key t, old)
od
`
......@@ -311,6 +331,7 @@ val get_iaddr_cell_addrs_def = Define`
get_iaddr_cell_addrs (mem : memory) (ia : iaddr) : addr list + addr mem_error =
let region = get_region mem (FST ia.base); base = SND ia.base
in do
(* Look up type + offsets for the base location *)
(_, base_tys, base_offs_tl) <- lookup base region
or_fail UndefBehavior (ia.base, Unallocated);
base_offs <- return (base::base_offs_tl);
......@@ -319,6 +340,8 @@ val get_iaddr_cell_addrs_def = Define`
assert (ia.offset < LENGTH base_offs)
or_fail UndefBehavior (ia.base, BadOffset base_tys ia.offset);
off <- return (EL ia.offset base_offs);
(* Get a slice of the component's offsets *)
(_, tys, offs_tl) <- lookup off region
or_fail UndefBehavior ((FST ia.base, ia.offset), Unallocated);
offs <- return (off::offs_tl);
......@@ -355,6 +378,58 @@ val memory_load_def = Define`
(******************************************************************************)
val lookup_map_with_keys = store_thm("lookup_map_with_keys",
``t f k. lookup k (map_with_keys f t) = OPTION_MAP (f k) (lookup k t)``,
rw[map_with_keys_def, lookup_fromAList] >>
Cases_on `OPTION_MAP (f k) (lookup k t)` >> fs[OPTION_MAP_DEF] >| [
rw[ALOOKUP_FAILS, MEM_MAP] >> Cases_on `y` >> simp[MEM_toAList] >>
Cases_on `k = q` >> rw[],
`al. ALOOKUP (MAP (λ(k,v). (k,f k v)) al) k
= OPTION_MAP (f k) (ALOOKUP al k)` suffices_by rw[ALOOKUP_toAList] >>
Induct >- rw[FUN_EQ_THM] >> Cases >> rw[FUN_EQ_THM]
])
val wf_map_with_keys = store_thm("wf_map_with_keys",
``f t. wf (map_with_keys f t)``,
rw[map_with_keys_def] >> qmatch_rename_tac `wf (fromAList xs)` >>
Induct_on `xs` >- rw[fromAList_def, wf_def] >> Cases >>
rw[fromAList_def, wf_insert])
val lookup_merge = store_thm("lookup_merge",
``t1 t2 f k. lookup k (merge f t1 t2) =
let v1 = lookup k t1; v2 = lookup k t2
in OPTION_CHOICE (OPTION_MAP2 f v1 v2) (OPTION_CHOICE v1 v2)``,
rw[merge_def, lookup_union, lookup_map_with_keys] >>
ntac 2 CASE_TAC >> fs[OPTION_MAP_DEF, OPTION_MAP2_DEF])
val wf_merge = store_thm("wf_merge",
``t1 t2 f. wf t2 wf (merge f t1 t2)``,
rw[merge_def, wf_union, wf_map_with_keys])
val insert_union_commute = store_thm("insert_union_commute",
``t t' n v. wf t wf t' n domain t'
insert n v (union t' t) = union t' (insert n v t)``,
rw[FUN_EQ_THM, wf_insert, wf_union, spt_eq_thm, lookup_union, lookup_insert] >>
ntac 2 CASE_TAC >> fs[domain_lookup])
val merge_empty = store_thm("merge_empty",
``f x. merge f LN x = x``,
rw[merge_def, map_with_keys_def, toAList_def, fromAList_def, foldi_def])
(*
val address_space_union_assoc = store_thm("address_space_union_assoc",
``∀a1 a2 a3. address_space_union a1 (address_space_union a2 a3)
= address_space_union (address_space_union a1 a2) a3``,
rw[address_space_union_def, address_space_component_equality, union_assoc] >>
match_mp_tac spt_eq_thm
*)
val address_space_union_empty = store_thm("address_space_union_empty",
``address_space_union new_address_space = I``,
rw[FUN_EQ_THM, new_address_space_def, address_space_union_def,
theorem "address_space_component_equality", merge_empty])
val mem_region_set_value_ok = store_thm("mem_region_set_value_ok",
``k v r r'. mem_region_ok r mem_region_set_value k v r = OK r'
mem_region_ok r'``,
......
This diff is collapsed.
......@@ -35,9 +35,7 @@ val _ = Datatype`
val _ = Datatype`
sched_state = <|
program: program;
next_tid: thread_id;
threads: thread spt;
next_sid: stack_id;
stacks: stack spt;
memory: memory;
sched_tid: thread_id;
......@@ -47,17 +45,18 @@ val _ = Datatype`
val state_ok_def = Define`
state_ok (s : sched_state) : bool
let tn = thread_id_dest s.next_tid;
sn = stack_id_dest s.next_sid
let thread_ok' th = (
thread_ok th
stack_id_dest th.sid domain s.stacks
n th'. lookup n s.threads = SOME th' th th'
th.sid th'.sid)
in wf s.threads
wf s.stacks
wf s.sched_addrs
s.threads LN
s.stacks LN
EVERY (PROD_ALL ($> tn domain s.sched_addrs) thread_ok)
(toAList s.threads)
EVERY (PROD_ALL ($> sn) stack_ok)
(toAList s.stacks)
EVERY (PROD_ALL (domain s.sched_addrs) thread_ok') (toAList s.threads)
EVERY (stack_ok o SND) (toAList s.stacks)
memory_ok s.memory
`
......@@ -105,9 +104,7 @@ val new_sched_state_def = Define`
or_fail Impossible "no such main function version";
return <|
program := compile_program env;
next_tid := ThreadID 1;
threads := insert 0 (new_thread (StackID 0)) LN;
next_sid := StackID 1;
stacks := insert 0 <|
frames := [<|
id := FrameID 0;
......@@ -332,9 +329,22 @@ val take_step_def = Define`
od
`
val has_terminated_def = Define`
has_terminated (state : sched_state) : bool
EVERY (λ(tid, _).
case thread_current_frame_state (ThreadID tid) state of
| SOME (DEAD _) => T
| _ => F
) (toAList state.threads)
`
val try_step_def = Define`
try_step (step : sched_step) (state : sched_state) : sched_state or_error =
option_CASE (take_step step state) (OK state) I
if has_terminated state
then return state
else case take_step step state of
| NONE => return state
| SOME next => next
`
(*
......@@ -360,15 +370,6 @@ val take_steps_ok = store_thm("take_steps_ok",
match_mp_tac foldl_propagates >> simp[try_step_ok])
*)
val has_terminated_def = Define`
has_terminated (state : sched_state) : bool
EVERY (λ(tid, _).
case thread_current_frame_state (ThreadID tid) state of
| SOME (DEAD _) => T
| _ => F
) (toAList state.threads)
`
val get_return_values_def = Define`
get_return_values state =
case thread_current_frame_state (ThreadID 0) state of
......@@ -388,32 +389,31 @@ val run_finite_schedule_def = Define`
run_finite_schedule (schedule : sched_step list)
(state : sched_state)
: sched_state or_error =
FOLDL (λs step. s >>= λs. if has_terminated s then return s else try_step step s)
(OK state)
schedule
FOLDL (λs step. s >>= try_step step) (OK state) schedule
`
(*
val foldl_resolve_all_lemma = prove(
``(∀r. propagates state_ok (f r)) ⇒
propagates state_ok (λa. FOLDL (λs r. s >>= f r) (OK (resolve_all a)) rs)``,
rw[] >> imp_res_tac foldl_propagates >> fs[propagates_def] >>
metis_tac[resolve_all_ok])
val run_finite_schedule_ok = store_thm("run_finite_schedule_ok",
``∀sc. propagates state_ok (run_finite_schedule sc)``,
strip_tac >> match_mp_tac pointful >> rw[run_finite_schedule_def] >>
ho_match_mp_tac foldl_resolve_all_lemma >> rw[propagates_def] >>
FULL_CASE_TAC >> rw[] >> assume_tac try_step_ok >> fs[propagates_def] >>
metis_tac[])
*)
val run_finite_schedule_last_step = store_thm("run_finite_schedule_last_step",
``step steps s s'. run_finite_schedule (SNOC step steps) s = OK s'
last. run_finite_schedule steps s = OK last
(last = s' ∨ try_step step last = OK s')``,
try_step step last = OK s'``,
rw[run_finite_schedule_def, FOLDL_SNOC] >> qexists_tac `s''` >>
FULL_CASE_TAC >> rw[])
*)
BasicProvers.FULL_CASE_TAC >> rw[])
val run_finite_schedule_snoc = store_thm("run_finite_schedule_snoc",
``s step steps. s >>= run_finite_schedule (SNOC step steps)
= s >>= run_finite_schedule steps >>= try_step step``,
Cases >> rw[FUN_EQ_THM] >>
Cases_on `run_finite_schedule (SNOC step steps) x` >>
fs[run_finite_schedule_def, FOLDL_SNOC])
val run_schedule_def = Define`
run_schedule (schedule : sched_step llist)
......@@ -431,6 +431,7 @@ val run_schedule_terminated = store_thm("run_schedule_terminated",
``st. has_terminated st sc. run_schedule sc st = OK st``,
rw[run_schedule_def, Once whileTheory.WHILE])
(*
val run_finite_schedule_eq_run_schedule = store_thm("run_finite_schedule_eq_run_schedule",
``∀sc st. run_finite_schedule sc st = run_schedule (fromList sc) st``,
Induct >> rw[run_finite_schedule_def, run_schedule_def]
......@@ -447,6 +448,19 @@ val run_finite_schedule_eq_run_schedule = store_thm("run_finite_schedule_eq_run_
fs[uvmThreadsStacksTheory.foldl_fail]) >>
fs[try_step_def] >> Cases_on `take_step h st` >> fs[] >>
Cases_on `x` >> fs[])))
*)
val run_finite_schedule_append = store_thm("run_finite_schedule_append",
``sc1 sc2 st. run_finite_schedule sc1 st >>= run_finite_schedule sc2
= run_finite_schedule (sc1 ++ sc2) st``,
strip_tac >> listLib.SNOC_INDUCT_TAC >> strip_tac >>
fs[run_finite_schedule_def] >| [
`run_finite_schedule [] = OK` suffices_by simp[] >>
simp[FUN_EQ_THM, run_finite_schedule_def],
`sc1 ++ SNOC x sc2 = SNOC x (sc1 ++ sc2)` by simp[] >>
simp[run_finite_schedule_snoc, FOLDL_SNOC]
])
(*
val run_schedule_finite_ok = store_thm("run_schedule_finite_ok",
......@@ -487,14 +501,14 @@ val schedule_valid_def = Define`
val finite_schedule_terminates_snoc = store_thm("finite_schedule_terminates_snoc",
``p s. finite_schedule_terminates p s x. finite_schedule_terminates p (SNOC x s)``,
rw[finite_schedule_terminates_def, monadsTheory.merge_left_def] >>
multi_case_tac >> fs[run_finite_schedule_def, FOLDL_SNOC] >> rw[])
multi_case_tac >> fs[run_finite_schedule_def, FOLDL_SNOC, try_step_def] >> rw[])
val finite_schedule_terminates_snoc_eq = store_thm("finite_schedule_terminates_snoc_eq",
``st sc. finite_schedule_terminates st sc
x. run_finite_schedule sc st
= run_finite_schedule (SNOC x sc) st``,
rw[finite_schedule_terminates_def, monadsTheory.merge_left_def] >>
multi_case_tac >> fs[run_finite_schedule_def, FOLDL_SNOC])
multi_case_tac >> fs[run_finite_schedule_def, FOLDL_SNOC, try_step_def])
val finite_schedule_valid_snoc = store_thm("finite_schedule_valid_snoc",
``st sc. finite_schedule_terminates st sc
......@@ -531,6 +545,25 @@ val schedule_valid_inter = store_thm("schedule_valid_inter",
rw[schedule_valid_def, monadsTheory.merge_left_def] >> RES_TAC >>
multi_case_tac >> rw[IN_APP] >> rfs[] >> rw[])
val (advances_pc_by_rules, advances_pc_by_ind, advances_pc_by_cases) = Hol_reln`
(st tid. advances_pc_by 0 [] st tid)
(st st' n x xs tid.
try_step x st = OK st'
advances_pc_by n xs st' tid
advances_pc_by (
if (th sk sk' opns.
step = ExecInst
st.sched_tid = tid
get_thread tid st = SOME th
get_stack th.sid st = SOME sk
get_stack th.sid st' = SOME sk'
(HD sk.frames).state = ACTIVE opns
(HD sk'.frames).state = ACTIVE (TL opns)
(MAP frame_id sk.frames = MAP frame_id sk'.frames))
then SUC n else n
) (x::xs) st' tid)
`