open HolKernel Parse boolLib bossLib

open uvmMemoryTheory
open uvmThreadsStacksTheory
open uvmInstructionSemanticsTheory

open arithmeticTheory
open combinTheory
open numpairTheory
open pred_setTheory
open listTheory
open llistTheory
open sortingTheory
open sptreeTheory

open monadsyntax
open BasicProvers
open DefineUtils

val _ = new_theory "uvmScheduler"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)

val _ = Datatype`
  sched_step =
  | ExecInst
  | NextThread
  | NextAddr
  | DequeueStore
  | DequeueInvalidation
`

val _ = Datatype`
  sched_state = <|
    program: program;
    next_tid: thread_id;
    threads: thread spt;
    next_sid: stack_id;
    stacks: stack spt;
    memory: memory;
    cur_tid: thread_id;
    cur_addr: addr
  |>
`

val state_ok_def = Define`
  state_ok (s : sched_state) : bool ⇔
    let tn = thread_id_dest s.next_tid in
    let sn = stack_id_dest s.next_sid in
      wf s.threads
    ∧ wf s.stacks
    ∧ s.threads ≠ LN
    ∧ s.stacks ≠ LN
    ∧ EVERY (PROD_ALL ($> tn) thread_ok) (toAList s.threads)
    ∧ EVERY (PROD_ALL ($> sn) stack_ok) (toAList s.stacks)
    ∧ memory_ok s.memory
`

val get_thread_def = Define`
  get_thread tid state : thread option =
    lookup (thread_id_dest tid) state.threads
`

val get_stack_def = Define`
  get_stack sid state : stack option =
    lookup (stack_id_dest sid) state.stacks
`

val next_thread_def = Define`
  next_thread state : thread_id =
    let tids = QSORT $< (MAP FST (toAList state.threads)) in
    ThreadID (
      case FIND ($> (thread_id_dest state.cur_tid)) tids of
      | SOME a => a
      | NONE => HD tids)
`

val next_addr_def = Define`
  next_addr state : addr =
    let all_addrs = (
      LIST_BIND (toList state.threads) (λth. addrs_of th.sb ++ addrs_of th.ib)
      :> nub :> QSORT addr_lt) in
    case FIND (C addr_lt state.cur_addr) all_addrs of
    | SOME a => a
    | NONE => if NULL all_addrs then (Global, 0) else HD all_addrs
`

val new_sched_state_def = Define`
  new_sched_state (env : environment) (main : func_name)
                  : sched_state or_error = do
    mem <- new_memory env.globals;
    vopt <- expect (FLOOKUP env.func_versions main)
      (InvalidState "no such main function");
    version <- expect vopt (UndefinedBehavior "main function undefined");
    func <- expect (FLOOKUP env.functions version)
      (InvalidState "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;
              fn := main;
              regs := LN;
              state := READY func.signature.arg_types <|
                  nor_jump := (0, GENLIST INL (LENGTH func.signature.arg_types));
                  exc_jump := NONE
                |>
            |>];
          next_frame := FrameID 1
        |> LN;
      memory := mem;
      cur_tid := ThreadID 0;
      cur_addr := (Global, 0)
    |>
  od
`

(*
val new_sched_state_ok = store_thm("new_sched_state_ok",
  ``∀env main s. new_sched_state env main = OK s ⇒ state_ok s``,

  rw[new_sched_state_def, state_ok_def] >>
  fs[wf_insert, wf_def, new_memory_def, new_address_space_def] >>
  ONCE_REWRITE_TAC[insert_def] >>
  simp[toList_def, toListA_def, toAList_def, foldi_def, new_thread_ok,
       thread_id_dest_def, stack_id_dest_def, frame_id_lt_def,
       stack_ok_def, memory_ok_def, mem_region_ok_def, frame_ok_def, wf_def] >>
  multi_case_tac >> simp[wf_def, toListA_def] >| [
    ntac 2 (pop_assum (K all_tac)) >> pop_assum mp_tac >>
    qmatch_rename_tac `FOLDL _ (OK (ll, _)) (ZIP (_, MAP SND globals)) = _ ⇒ _` >>
    map_every qid_spec_tac [`q`, `r`, `globals`] >>
    listLib.SNOC_INDUCT_TAC >> fs[wf_def] >> rw[] >>
    fs[MAP_SNOC, GENLIST, rich_listTheory.ZIP_SNOC, FOLDL_SNOC, region_alloc_def] >>
    multi_case_tac >> fs[] >> POP_ASSUM_LIST (K all_tac) >>
    Induct_on `q''`
    Induct_on `globals` >> 
    Induct_on `env.globals` >> rw[] >| [
      `env.globals = []` by simp[] >> fs[] >> prove_tac[wf_def],
      `env.globals = h::v`
    ]
  ]
  Induct_on `env.globals` >> rw[]

  fs[MEM_EL, EL_GENLIST, optionTheory.IS_SOME_DEF, PEEK_ADD] >| [

    `stack_ok <|frames := []; next_frame := Frame 0|>`
      suffices_by metis_tac[push_frame_ok, propagates_def] >>
    simp[stack_ok_def],

    match_mp_tac EVERY_LEAF_ADD >> simp[EVERY_LEAF_def, new_thread_ok]
  ])
*)

val thread_current_frame_state_def = Define`
  thread_current_frame_state tid state =
    OPTION_BIND (get_thread tid state) (λth.
    OPTION_BIND (get_stack th.sid state) (λst.
      case st.frames of
      | fr::_ => SOME fr.state
      | _ => SOME (DEAD NONE)))
`
(*
val extract_def = Define`
  extract (n : num) (xs : α list) : (α # α list) option =
    if n < LENGTH xs
    then SOME (EL n xs, TAKE n xs ++ DROP (SUC n) xs)
    else NONE
`

val extract_cons = store_thm("extract_cons",
  ``extract n xs = SOME (x, xs') ⇔
    extract (SUC n) (h::xs) = SOME (x, h::xs')``,
  rw[extract_def])

val imp_extract_map = store_thm("imp_extract_map",
  ``∀n f xs x xs'.
      extract n xs = SOME (x, xs')
    ⇒ extract n (MAP f xs) = SOME (f x, MAP f xs')``,
  rw[extract_def, EL_MAP] >> rw[MAP_APPEND, MAP_TAKE] >>
  match_mp_tac LIST_EQ >> rw[EL_MAP, rich_listTheory.EL_DROP])

val extract_all_distinct_filter = store_thm("extract_all_distinct_filter",
  ``∀n xs x xs'. ALL_DISTINCT xs
    ⇒ extract n xs = SOME (x, xs') ⇒ xs' = FILTER ($≠ x) xs``,
  rw[extract_def] >> simp[FILTER_EQ_APPEND] >>
  qexists_tac `TAKE n xs` >> qexists_tac `DROP n xs` >> fs[] >>
  `DROP n xs = EL n xs::DROP (SUC n) xs` by
    metis_tac[rich_listTheory.DROP_EL_CONS, ADD1] >>
  rw[FILTER_EQ_ID, EVERY_MEM, MEM_EL]
  >- (Cases_on `n' < n` >>
      fs[rich_listTheory.EL_TAKE, ALL_DISTINCT_EL_IMP])
  >- (Cases_on `n' < LENGTH xs - SUC n` >>
      fs[rich_listTheory.EL_DROP, ALL_DISTINCT_EL_IMP]))

val extract_every = store_thm("extract_every",
  ``∀P n xs x xs'. EVERY P xs ⇒ extract n xs = SOME (x, xs') ⇒ EVERY P xs'``,
  let open rich_listTheory in simp[extract_def, EVERY_TAKE, EVERY_DROP] end)

val extract_sorted = store_thm("extract_sorted",
  ``∀R xs n x xs'. transitive R ∧ irreflexive R ∧ SORTED R xs
                 ⇒ extract n xs = SOME (x, xs')
                 ⇒ SORTED R xs'``,
    metis_tac[SORTED_ALL_DISTINCT, extract_all_distinct_filter, sorted_filter])

val extract_mem = store_thm("extract_mem",
  ``∀n xs x xs'. ALL_DISTINCT xs ∧ extract n xs = SOME (x, xs') ⇒ ¬MEM x xs'``,
  let open rich_listTheory in
  rw[extract_def, MEM_EL] >> simp[] >>
  Cases_on `n' < n + LENGTH xs - SUC n` >> simp[] >> Cases_on `n' < n` >| [
  
    fs[EL_APPEND1, EL_TAKE] >>
    `n ≠ n' ∧ n' < LENGTH xs` by simp[] >> prove_tac[ALL_DISTINCT_EL_IMP],
  
    fs[EL_APPEND2, EL_DROP] >>
    `n' + SUC n - n ≠ n ∧ n' + SUC n - n < LENGTH xs ∧ n < LENGTH xs` by simp[] >>
    prove_tac[ALL_DISTINCT_EL_IMP]]

  end)

val extract_not_mem = store_thm("extract_not_mem",
  ``∀n xs x xs' y. ¬MEM y xs ∧ extract n xs = SOME (x, xs') ⇒ ¬MEM y xs'``,
  rw[extract_def] >> rw[MEM_APPEND] >> fs[MEM_EL] >> rw[]
  >- (Cases_on `n' < n` >> rw[] >> `n' < LENGTH xs` by simp[] >>
      metis_tac[rich_listTheory.EL_TAKE])
  >- (Cases_on `n' < LENGTH xs - SUC n` >> rw[] >>
      `n' + SUC n < LENGTH xs` by simp[] >>
      metis_tac[rich_listTheory.EL_DROP]))
*)

val exec_non_memory_action_def = Define`
  exec_non_memory_action (rdr : (num, value) alist reg_reader)
                         (st : sched_state)
                         : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    sk <- expect (get_stack th.sid st) (InvalidState "missing stack");
    rs <- run_reg_reader rdr (HD sk.frames).regs;
    sk' <- FOLDL (λs r. s >>= set_register r) (OK sk) rs;
    return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
  od
`

val exec_load_def = Define`
  exec_load (rdr : iaddr reg_reader)
            (dst : num)
            (st : sched_state)
            : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    sk <- expect (get_stack th.sid st) (InvalidState "missing stack");
    ia <- run_reg_reader rdr (HD sk.frames).regs;
    ad <- HD <$> get_iaddr_cell_addrs st.memory ia;
    ld <- memory_load st.memory th.sb th.ib ad;
    sk' <- set_register (dst, ld) sk;
    return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
  od
`

val exec_store_def = Define`
  exec_store (rdr : (iaddr # value) reg_reader)
             (st : sched_state)
             : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    sk <- expect (get_stack th.sid st) (InvalidState "missing stack");
    (ia, v) <- run_reg_reader rdr (HD sk.frames).regs;
    ad <- HD <$> get_iaddr_cell_addrs st.memory ia;
    return (st with threads updated_by
      insert (thread_id_dest st.cur_tid) (enqueue_store (ad, v) th) o
      map (enqueue_invalidation (ad, v)))
  od
`

val exec_commit_def = Define`
  exec_commit (st : sched_state) : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    assert (NULL (addrs_of th.sb)) InvalidStep;
    return st
  od
`

val exec_reconcile_def = Define`
  exec_reconcile (st : sched_state) : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    return (st with threads updated_by insert (thread_id_dest st.cur_tid)
      (th with ib := new_address_space))
  od
`

val exec_command_def = Define`
  exec_command (rdr : command reg_reader)
               (st : sched_state)
               : sched_state or_error = do
    th <- expect (get_thread st.cur_tid st) InvalidStep;
    sk <- expect (get_stack th.sid st) (InvalidState "missing stack");
    cmd <- run_reg_reader rdr (HD sk.frames).regs;
    case cmd of
    | DoPushStack fn sig args next => do
        sk' <- push_stack st.program fn sig args next sk;
        return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
      od
    | DoPopStack rvs => do
        sk' <- pop_stack st.program rvs sk;
        (* TODO: Free stack memory *)
        return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
      od
    | DoJump label args => do
        sk' <- jump st.program label args sk;
        return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
      od
    | DoHeapAlloc ty sz dst => do
        (mem, ad) <- memory_heap_alloc st.memory sz ty;
        sk' <- set_register (dst, RefV ty (SOME ad)) sk;
        return (st with <|
          stacks updated_by insert (stack_id_dest th.sid) sk';
          memory := mem
        |>)
      od
    | DoStackAlloc ty sz dst => do
        (mem, ad) <- memory_stack_alloc st.memory th.sid (HD sk.frames).id sz ty;
        sk' <- set_register (dst, RefV ty (SOME ad)) sk;
        return (st with <|
          stacks updated_by insert (stack_id_dest th.sid) sk';
          memory := mem
        |>)
      od
    | DoGetStack dst => Fail (NotImplemented "DoGetStack")
    | DoNewThread sid rvs dst => Fail (NotImplemented "DoNewThread")
    | DoThreadExit => Fail (NotImplemented "DoThreadExit")
  od
`

val take_step_def = Define`
    take_step ExecInst st = do
      th <- expect (get_thread st.cur_tid st) InvalidStep;
      sk <- expect (get_stack th.sid st) (InvalidState "missing stack");
      case (HD sk.frames).state of
      | ACTIVE (opn::rest) =>
          (st with stacks updated_by
             insert (stack_id_dest th.sid) (sk with frames updated_by
               λf. (HD f with state := ACTIVE rest)::TL f)) :>
          (case opn of
           | Nm rdr => exec_non_memory_action rdr
           | Ld rdr dst => exec_load rdr dst
           | St rdr => exec_store rdr
           | Com => exec_commit
           | Rec => exec_reconcile
           | Cmd rdr => exec_command rdr)
      | _ => Fail (InvalidState "live thread's top stack frame is not ACTIVE")
    od
  ∧ take_step NextThread st =
      return (st with cur_tid := next_thread st)
  ∧ take_step NextAddr st =
      return (st with cur_addr := next_addr st)
  ∧ take_step DequeueStore st = do
      th <- expect (get_thread st.cur_tid st) InvalidStep;
      (sb, v) <- expect (buffer_dequeue th.sb st.cur_addr) InvalidStep;
      mem <- memory_put st.memory st.cur_addr v;
      return (st with <|
        threads updated_by insert (thread_id_dest st.cur_tid) (th with sb := sb);
        memory := mem
      |>)
    od
  ∧ take_step DequeueInvalidation st = do
      th <- expect (get_thread st.cur_tid st) InvalidStep;
      (ib, _) <- expect (buffer_dequeue th.ib st.cur_addr) InvalidStep;
      return (st with threads updated_by
        insert (thread_id_dest st.cur_tid) (th with ib := ib))
    od
`

val step_or_def = Define`
    step_or last (Fail InvalidStep) = return last
  ∧ step_or _ next = next
`

val try_step_def = Define`
  try_step (step : sched_step) (state : sched_state) : sched_state or_error =
    step_or state (take_step step state)
`

(*
val try_step_ok = store_thm("try_step_ok",
  ``∀step. propagates state_ok (try_step step)``,
  assume_tac take_step_ok >> assume_tac resolve_all_ok >>
  fs[propagates_def] >> rw[try_step_def] >> every_case_tac >> fs[] >>
  metis_tac[])
  *)

(* Expand eta reductions ("pointfree" style) into lambdas *)
val pointful = prove(``∀P f. P (λx. f x) ⇒ P f``, metis_tac[])

val take_steps_def = Define`
  take_steps (steps : sched_step list) (state : sched_state) : sched_state or_error =
    FOLDL (λs step. s >>= try_step step) (OK state) steps
`

(*
val take_steps_ok = store_thm("take_steps_ok",
  ``∀steps. propagates state_ok (take_steps steps)``,
  strip_tac >> match_mp_tac pointful >> rw[take_steps_def] >>
  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
    | SOME (DEAD (SOME rv)) => return rv
    | SOME (DEAD NONE) => Fail (UndefinedBehavior "no return value")
    | _ => Fail (InvalidState "schedule exhausted")
`

val get_global_value_def = Define`
  get_global_value env name state = 
    expect (OPTION_BIND
        (OPTION_MAP FST (INDEX_FIND 0 ($= name o FST) env.globals))
        (OPTION_MAP FST o get_addr state.memory o $, Global))
    (InvalidState (name ++ " is undefined"))
`

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
`

(*
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')``,
  rw[run_finite_schedule_def, FOLDL_SNOC] >> qexists_tac `s''` >>
  FULL_CASE_TAC >> rw[])
  *)

val run_schedule_def = Define`
  run_schedule (schedule : sched_step llist)
               (state : sched_state)
               : sched_state or_error =
    SND (WHILE
      (λ(steps, state).
        IS_SOME (LHD steps) ∧
        (case state of OK state => ¬has_terminated state | Fail _ => F))
      (λ(steps, state). THE (LTL steps), state >>= try_step (THE (LHD steps)))
      (schedule, OK state))
`

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]
  >- simp[Once whileTheory.WHILE]
  >- (`run_schedule (fromList sc) st = run_schedule (h:::fromList sc) st`
        suffices_by fs[run_schedule_def, run_finite_schedule_def] >>
      rw[run_schedule_def] >> Cases_on `sc` >>
      simp[Once whileTheory.WHILE] >> simp[Once whileTheory.WHILE])
  >- (simp[Once whileTheory.WHILE] >>
      Cases_on `∃st'. try_step h (resolve_all st) = OK (resolve_all st')`
      >- (fs[run_schedule_def, run_finite_schedule_def] >> metis_tac[])
      >- (`∃x. try_step h (resolve_all st) = Fail x` suffices_by (
            rw[Once whileTheory.WHILE] >> Cases_on `try_step h (resolve_all st)` >>
            fs[uvmThreadsStacksTheory.foldl_fail]) >>
          fs[try_step_def] >> CASE_TAC >> fs[] >> TRY CASE_TAC >> fs[] >>
          metis_tac[])))

val run_schedule_finite_ok = store_thm("run_schedule_finite_ok",
  ``∀sc. LFINITE sc ⇒ propagates state_ok (run_schedule sc)``,
  rw[] >> match_mp_tac pointful >>
  `propagates state_ok (λx. run_finite_schedule (THE (toList sc)) x)`
    suffices_by rw[run_finite_schedule_eq_run_schedule, to_fromList] >>
  metis_tac[run_finite_schedule_ok])
*)

(*
val finite_schedule_terminates_def = Define`
  finite_schedule_terminates (prg : program) (schedule : sched_step list) ⇔
    merge_left (K T) (has_terminated <$>
      (new_sched_state prg >>= run_finite_schedule schedule))
`

val schedule_terminates_def = Define`
  schedule_terminates (prg : program) (schedule : sched_step llist) ⇔
    ∃n fs. LTAKE n schedule = SOME fs ∧ finite_schedule_terminates prg fs
`

val finite_schedule_valid_def = Define`
  finite_schedule_valid (validator : sched_state -> bool)
                        (prg : program)
                        (schedule : sched_step list) ⇔
    ∀len. len ≤ LENGTH schedule
        ⇒ merge_left (K T) (validator <$>
            (new_sched_state prg >>= run_finite_schedule (TAKE len schedule)))
`

val schedule_valid_def = Define`
  schedule_valid (validator : sched_state -> bool)
                 (prg : program)
                 (schedule : sched_step llist) ⇔
    ∀len fs. LTAKE len schedule = SOME fs
        ⇒ merge_left (K T) (validator <$>
            (new_sched_state prg >>= run_finite_schedule fs))
`

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, sumMonadTheory.merge_left_def] >>
  pop_assum mp_tac >> REPEAT CASE_TAC >>
  fs[run_finite_schedule_def, FOLDL_SNOC] >> rw[] >> fs[]
  >- (rw[] >> fs[] >> rw[] >> fs[] >> rw[])
  >- fs[run_finite_schedule_def])

val finite_schedule_terminates_snoc_eq = store_thm("finite_schedule_terminates_snoc_eq",
  ``∀p s. finite_schedule_terminates p s
        ⇒ ∀x. new_sched_state p >>= run_finite_schedule s
            = new_sched_state p >>= run_finite_schedule (SNOC x s)``,
  rw[finite_schedule_terminates_def, sumMonadTheory.merge_left_def] >>
  pop_assum mp_tac >> CASE_TAC
  >- fs[run_finite_schedule_def, FOLDL_SNOC]
  >- (Cases_on `new_sched_state p` >>
      fs[run_finite_schedule_def, FOLDL_SNOC]))

val finite_schedule_valid_snoc = store_thm("finite_schedule_valid_snoc",
  ``∀p s. finite_schedule_terminates p s
    ⇒ ∀v. finite_schedule_valid v p s
    ⇒ ∀x. finite_schedule_valid v p (SNOC x s)``,
  rw[finite_schedule_valid_def] >> Cases_on `len = SUC (LENGTH s)` >>
  fs[] >> rw[]
  >- (`TAKE (SUC (LENGTH s)) (SNOC x s) = SNOC x s` by (
        `LENGTH (SNOC x s) = SUC (LENGTH s)` by simp[] >>
        metis_tac[TAKE_LENGTH_ID]) >>
      `new_sched_state p >>= run_finite_schedule (SNOC x s) =
       new_sched_state p >>= run_finite_schedule s`
        by simp[finite_schedule_terminates_snoc_eq] >>
      rw[] >> `LENGTH s ≤ LENGTH s` by simp[] >>
      metis_tac[TAKE_LENGTH_ID])
  >- (`len ≤ LENGTH s` by simp[] >>
      `TAKE len (SNOC x s) = TAKE len s` suffices_by metis_tac[] >>
      fs[TAKE_APPEND1]))

val finite_schedule_valid_monotonic = store_thm("finite_schedule_valid_monotonic",
  ``∀v v' p s'. (∀x. v x ⇒ v' x)
              ∧ finite_schedule_valid v p s
              ⇒ finite_schedule_valid v' p s``,
  rw[finite_schedule_valid_def, sumMonadTheory.merge_left_def] >> RES_TAC >>
  multi_case_tac >> first_x_assum match_mp_tac
  >- (imp_res_tac (Q.prove(`∀x y. x = OK y ⇒ y = OUTL x`, simp[])) >> rw[])
  >- rfs[sumMonadTheory.bind_left_def])

val schedule_valid_monotonic = store_thm("schedule_valid_monotonic",
  ``∀v v' p s. (∀x. v x ⇒ v' x) ∧ schedule_valid v p s ⇒ schedule_valid v' p s``,
  rw[schedule_valid_def, sumMonadTheory.merge_left_def] >> RES_TAC >>
  multi_case_tac >> first_x_assum match_mp_tac
  >- (imp_res_tac (Q.prove(`∀x y. x = OK y ⇒ y = OUTL x`, simp[])) >> rw[])
  >- rfs[sumMonadTheory.bind_left_def])

val schedule_valid_inter = store_thm("schedule_valid_inter",
  ``∀v v' p s. schedule_valid v p s ∧ schedule_valid v' p s
             ⇒ schedule_valid (v ∩ v') p s``,
  rw[schedule_valid_def, sumMonadTheory.merge_left_def] >> RES_TAC >>
  multi_case_tac >> rw[IN_APP] >> rfs[] >> rw[])

val finite_schedule_valid_state_ok = store_thm("finite_schedule_valid_state_ok",
  ``∀p s. finite_schedule_valid state_ok p s``,
  rw[finite_schedule_valid_def, sumMonadTheory.merge_left_def] >>
  multi_case_tac >>
  prove_tac[new_sched_state_ok, run_finite_schedule_ok, propagates_def])

val schedule_valid_state_ok = store_thm("schedule_valid_state_ok",
  ``∀p s. schedule_valid state_ok p s``,
  rw[schedule_valid_def, sumMonadTheory.merge_left_def] >>
  multi_case_tac >>
  prove_tac[init_sched_state_ok, run_finite_schedule_ok, propagates_def])

val generate_valid_schedule_def = Define`
  generate_valid_schedule (valid : sched_state -> bool)
                          (prg : program)
                          (steps : sched_step llist)
                          : sched_step list option =
    let init = new_sched_state prg in
    if ¬IMAGE OK valid init then NONE else
    FST (WHILE
      (λ(sched, state).
        IS_SOME sched ∧
        (case state of Fail _ => F | OK s => ¬has_terminated s))
      (λ(sched, state).
        case LHD (WHILE (λsteps.
          merge_left ($= InvalidStep) (do
            step <- expect (LHD steps) (InvalidState ARB);
            state <- state;
            next <- take_step step state;
            return (valid next)
          od)) (THE o LTL) steps) of
        | SOME next =>
            (SOME (SNOC next (THE sched)), state >>= try_step next)
        | NONE => (NONE, state))
      (SOME [], init))
`

val generate_valid_schedule_terminates = store_thm("generate_valid_schedule_terminates",
  ``∀v vs p s. generate_valid_schedule v p s = SOME vs
             ⇒ finite_schedule_terminates p vs``,
  strip_tac >> `∀x. x ∈ v ⇒ v x` by metis_tac[pred_setTheory.IN_APP] >> Induct >>
  rw[generate_valid_schedule_def, finite_schedule_terminates_def,
     sumMonadTheory.merge_left_def] >> CASE_TAC >> fs[run_finite_schedule_def] >>
  rw[] >> fs[sumMonadTheory.lift_left_def] >> rw[]
  >- (fs[Once whileTheory.WHILE] >> SPOSE_NOT_THEN MP_TAC >> strip_tac >> fs[] >>
      POP_ASSUM (K ALL_TAC) >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM MP_TAC >>
      CASE_TAC >> fs[Once whileTheory.WHILE]
      Q.MATCH_ABBREV_TAC `
        FST (WHILE wcond wbody
          case winit of
          | NONE => (NONE, OK (resolve_all y0)) 
          | SOME next => (SOME [next], try_step next (resolve_all y0))
        ) = SOME [] ⇒ F` >>
      Cases_on 
     [Once whileTheory.WHILE]
  listLib.SNOC_INDUCT_TAC

val generate_valid_schedule_valid = store_thm("generate_valid_schedule_valid",
  ``∀v vs p s. generate_valid_schedule v p s = SOME vs
             ⇒ finite_schedule_valid v p vs``,
  strip_tac >> `∀x. x ∈ v ⇒ v x` by metis_tac[pred_setTheory.IN_APP] >>
  rw[sumMonadTheory.merge_left_def, finite_schedule_valid_def,
     generate_valid_schedule_def] >>
  CASE_TAC >> fs[] >> rw[] >> fs[] >> rw[] >>
  REPEAT (POP_ASSUM MP_TAC) >>
  SPEC_TAC (``y0': sched_state``, ``y0': sched_state``) >>
  Induct_on `len`
  >- (rw[run_finite_schedule_def] >> fs[])
  >- (rw[] >> fs[])
  >> rw[] >> fs[] >>
  `TAKE (SUC len) vs = `
  
  SPEC_TAC (``len``, ``len``)
  
  listLib.SNOC_INDUCT_TAC
  >- (rw[sumMonadTheory.merge_left_def, finite_schedule_valid_def,
         generate_valid_schedule_def] >>
      CASE_TAC >> fs[run_finite_schedule_def] >> rw[] >> fs[])
  >- (rw[sumMonadTheory.merge_left_def, finite_schedule_valid_def,
         generate_valid_schedule_def] >>
      CASE_TAC >> fs[run_finite_schedule_def])
)
*)

(* A schedule is fair iff, at any point in the schedule, all possible steps
   occur at some future point in the schedule.
*)
val fair_def = Define`
  fair (s : sched_step llist) : bool ⇔
    ∀step n. ∃j. LNTH (n + j) s = SOME step
`

(* A schedule is fair within the bounding set `m` iff, for some length `l`, at
   any point in the schedule, every step in `m` is at most `l` steps away.
*)
val fair_bounded_def = Define`
  fair_bounded (m : sched_step set) (l : num) (s : sched_step llist) : bool ⇔
    ∀step. step ∈ m ⇒ ∀n. ∃j. j ≤ l ∧ (LNTH (n + j) s = SOME step) 
`

(* A finite schedule is fair within the bounding set `m` iff, for some length
   `l`, at any point in the schedule, if there are at least `l` steps remaining,
   every step in `m` is at most `l` steps away.

   A finite schedule cannot be fair for an infinite set `m`, or for a length `l`
   that is less than the cardinality of `m`, as no possible schedule could
   satisfy these requirements.
*)
val fair_finite_def = Define`
  fair_finite (m : sched_step set) (l : num) (s : sched_step list) : bool ⇔
    FINITE m ∧ CARD m ≤ SUC l ∧
    ∀step. step ∈ m ⇒ ∀n. (n ≤ LENGTH s - l) ⇒ ∃j. j ≤ l ∧ (EL (n + j) s = step) 
`

local
  open optionTheory
  open pred_setTheory

  val fair_bounded_lemma = Q.prove(
    `fair_bounded m l s ⇒ m ⊆ IMAGE (λn. THE (LNTH n s)) (count (SUC l))`,
    rw[fair_bounded_def, SUBSET_DEF] >>
    metis_tac[THE_DEF, LESS_EQ_IMP_LESS_SUC, ADD_0])
in
  val fair_weak_corollary = Q.store_thm("fair_weak_corollary",
    `∀s. fair s ⇒ ∀step. exists ($= step) s`,
    rw[fair_def, exists_LNTH] >> metis_tac[])

  val fair_infinite = Q.store_thm("fair_infinite",
    `∀s. fair s ⇒ ¬LFINITE s`,

    SPOSE_NOT_THEN STRIP_ASSUME_TAC >> fs[fair_def, LFINITE_LNTH_NONE] >>
    `∀j. n ≤ j + n` by simp[] >> metis_tac[LNTH_NONE_MONO, NOT_SOME_NONE])

  val fair_lcons = Q.store_thm("fair_lcons",
    `∀s. fair s ⇔ ∀s'. fair (s':::s)`,

    strip_tac >>

    `(∀s'. fair (s':::s)) ⇒ fair s` by (
      rw[fair_def] >> Induct_on `n` >> rw[] >>
      metis_tac[LNTH, LTL_LCONS, OPTION_JOIN_DEF, OPTION_MAP_DEF, ADD_SUC]) >>

    `fair s ⇒ ∀s'. fair (s':::s)` by (
      rw[fair_def] >> `∀step. ∃j. LNTH j s = SOME step` by metis_tac[] >>
      Induct_on `n` >> rw[] >>
      metis_tac[LNTH, LTL_LCONS, OPTION_JOIN_DEF, OPTION_MAP_DEF, ADD_SUC]) >>

    metis_tac[])

  val fair_bounded_weak_corollary = Q.store_thm("fair_bounded_weak_corollary",
    `∀m s. (∃l. fair_bounded m l s) ⇒ ∀step. step ∈ m ⇒ exists ($= step) s`,
    rw[fair_bounded_def, exists_LNTH] >> metis_tac[])

  val fair_bounded_infinite = Q.store_thm("fair_bounded_infinite",
    `∀m l s. fair_bounded m l s ∧ m ≠ {} ⇒ ¬LFINITE s`,

    SPOSE_NOT_THEN STRIP_ASSUME_TAC >> fs[fair_bounded_def, LFINITE_LNTH_NONE] >>
    `∀j. n ≤ j + n` by simp[] >>
    metis_tac[LNTH_NONE_MONO, NOT_SOME_NONE, MEMBER_NOT_EMPTY])

  val fair_bounded_finite_set = Q.store_thm("fair_bounded_finite_set",
    `∀m l s. fair_bounded m l s ⇒ FINITE m`,
    REPEAT strip_tac >>
    metis_tac[fair_bounded_lemma, SUBSET_FINITE, FINITE_COUNT, IMAGE_FINITE])

  val fair_bounded_card = Q.store_thm("fair_bounded_card",
    `∀m l s. fair_bounded m l s ⇒ CARD m ≤ SUC l`,
    REPEAT strip_tac >>
    metis_tac[fair_bounded_lemma, CARD_COUNT, CARD_IMAGE, CARD_SUBSET,
      SUBSET_FINITE, FINITE_COUNT, IMAGE_FINITE, LESS_EQ_TRANS])

  val fair_finite_weak_corollary = Q.store_thm("fair_finite_weak_corollary",
    `∀m l s. fair_finite m l s ∧ l < LENGTH s ⇒ m ⊆ set s`,
    rw[fair_finite_def] >>
    `∀step. step ∈ m ⇒ ∃j. j ≤ l ∧ EL j s = step` by
      (fs[SUB_LEFT_LESS_EQ] >> metis_tac[ADD_0, LESS_0_CASES]) >>
    metis_tac[MEM, MEM_EL, LIST_TO_SET, LESS_EQ_LESS_TRANS, INSERT_DEF, SUBSET_DEF])

  (*
  val fair_bounded_ltake_fair_finite = Q.store_thm("fair_bounded_ltake_fair_finite",
    `∀m l s n. fair_bounded m l s ∧ l < n ⇒ fair_finite m l (THE (LTAKE n s))`,
    rw[fair_finite_def]
    >- metis_tac[fair_bounded_finite_set]
    >- metis_tac[fair_bounded_card]
    >- (
    fs[fair_bounded_def] >>
    metis_tac[LTAKE_LNTH_EL, THE_DEF, LESS_EQ_IMP_LESS_SUC, LTAKE_LENGTH]
    )
  ) *)

end

val cycle_def = Define`
  cycle (xs : α list) : α llist =
    LUNFOLD (λn. SOME (SUC n MOD LENGTH xs, EL n xs)) 0
`

val cycle_lnth =
  let
    val lemma = Q.prove(
      `∀m n f g. LNTH n (LUNFOLD (λn. SOME (f n, g n)) m)
               = LNTH 0 (LUNFOLD (λn. SOME (f n, g n)) (FUNPOW f n m))`,
      Induct_on `n` >>
      fs[FUNPOW_SUC, LNTH_LUNFOLD] >> metis_tac[FUNPOW_SUC, FUNPOW])
    val lemma' = SIMP_RULE (srw_ss()) [LNTH_LUNFOLD] lemma
  in
    Q.store_thm("cycle_nth",
      `∀n xs. xs ≠ [] ⇒ (LNTH n (cycle xs) = SOME (EL (n MOD (LENGTH xs)) xs))`,

      rw[cycle_def, lemma'] >>
      `FUNPOW (λn. SUC n MOD LENGTH xs) n 0 = n MOD LENGTH xs` suffices_by simp[] >>
      Induct_on `n` >>
      `0 ≠ LENGTH xs` by metis_tac[LENGTH_NIL] >>
      simp[FUNPOW_SUC, MOD_MOD] >>
      asm_simp_tac(srw_ss() ++ numSimps.MOD_ss ++ numSimps.ARITH_ss)[ADD1])
  end

val cycle_lnth_mem = store_thm("cycle_lnth_mem",
  ``∀n xs x. xs ≠ [] ∧ LNTH n (cycle xs) = SOME x ⇒ MEM x xs``,
  rw[MEM_EL] >> imp_res_tac cycle_lnth >> fs[] >>
  qexists_tac `n MOD LENGTH xs` >> rw[] >>
  match_mp_tac MOD_LESS >> prove_tac[LENGTH_NIL, LESS_0_CASES])

(*
val cycle_ltake_mem = store_thm("cycle_ltake_mem",
  ``∀n x xs xs'. xs ≠ [] ∧ LTAKE n (cycle xs) = SOME xs' ⇒ MEM x xs' ⇒ MEM x xs``,
  Induct >> rw[] >> fs[] >>
  Cases_on `LTAKE n (cycle xs)` >> fs[LTAKE_SNOC_LNTH] >>
  `LNTH n (cycle xs) = SOME (EL (n MOD (LENGTH xs)) xs)`
    by metis_tac[cycle_lnth] >>
  fs[] >> rw[] >> fs[] >> simp[MEM_EL] >>
  qexists_tac `n MOD LENGTH xs` >>
  `0 ≠ LENGTH xs` by metis_tac[LENGTH_NIL] >> fs[])

(* Generates a simple bounding set for `fair_bounded`, containing all possible
   steps for a given number of threads, a given max message queue depth, and a
   set of legal branch prediction guesses.
*)
val step_bound_def = Define`
  step_bound max_thread max_commit_depth legal_guesses : sched_step set =
    {step | (
      case step of
      | Commit tid n => tid ≼ max_thread ∧ n ≤ max_commit_depth
      | Proceed tid NONE => tid ≼ max_thread
      | Proceed tid (SOME guess) => tid ≼ max_thread ∧ guess ∈ legal_guesses)}
`

val seq_cst_bound_def = Define `seq_cst_bound max_thread = step_bound max_thread 0 ∅`
*)

(* FIXME: This schedule could get stuck in a cycle.
          Change the schedule steps to something easier to reason about. *)
val naive_schedule_def = Define`
  naive_schedule : sched_step llist =
    cycle [ExecInst; DequeueStore; NextAddr; NextThread; DequeueInvalidation]
`

(*
val imp_sorted_action_id = prove(
  ``SORTED action_id_lt ls ∧ m < n ∧ n < LENGTH ls
    ⇒ action_id_lt (EL m ls) (EL n ls)``,
  prove_tac[sortingTheory.SORTED_EL_LESS, relationTheory.transitive_def,
    action_id_lt_trans])

val seq_cst_schedule_commit_0 = store_thm("seq_cst_schedule_commit_0",
  ``∀n tid e x. 0 < n ∧ LNTH e (seq_cst_schedule n) = SOME (Commit tid x) ⇒ x = 0``,
  rw[seq_cst_schedule_def] >>
  qmatch_assum_abbrev_tac `LNTH e (cycle steps) = SOME (Commit tid x)` >>
  `steps ≠ []` by (qunabbrev_tac `steps` >> Induct_on `n` >> rw[GENLIST]) >>
  `MEM (Commit tid x) steps` by (qunabbrev_tac `steps` >> prove_tac[cycle_lnth_mem]) >>
  qunabbrev_tac `steps` >> fs[MEM_FLAT, MEM_GENLIST] >> rw[] >> fs[MEM_EL])

val seq_cst_schedule_proceed_none = store_thm("seq_cst_schedule_proceed_none",
  ``∀n tid e x. 0 < n ∧ LNTH e (seq_cst_schedule n) = SOME (Proceed tid x) ⇒ x = NONE``,
  rw[seq_cst_schedule_def] >>
  qmatch_assum_abbrev_tac `LNTH e (cycle steps) = SOME (Proceed tid x)` >>
  `steps ≠ []` by (qunabbrev_tac `steps` >> Induct_on `n` >> rw[GENLIST]) >>
  `MEM (Proceed tid x) steps` by (qunabbrev_tac `steps` >> prove_tac[cycle_lnth_mem]) >>
  qunabbrev_tac `steps` >> fs[MEM_FLAT, MEM_GENLIST] >> rw[] >> fs[MEM_EL])

val outbox_program_order_def = Define`
  outbox_program_order st ⇔
    ∀tid th cmsg oid oact.
      get_thread tid st = SOME th
    ∧ MEM cmsg st.memory.committed
    ∧ MEM (oid, oact) th.outbox
    ⇒ program_order cmsg (Message (SOME (Thread tid)) oid oact)
`

val commit_0_outbox_program_order = prove(
  ``∀tid. propagates (state_ok ∩ outbox_program_order) (try_step (Commit tid 0))``,

  Cases >> rw[propagates_def, IN_APP]
  >- prove_tac[propagates_def, try_step_ok] >>
  fs[outbox_program_order_def, try_step_def, take_step_def, get_thread_def] >>
  multi_case_tac >> fs[resolve_all_preserves, EL_LUPDATE] >| [
  
    fs[program_order_def, extract_def, state_ok_def, EVERY_EL] >>
    multi_case_tac >> fs[] >>
    `thread_ok th'` by prove_tac[optionTheory.OPTION_ALL_def] >>
    fs[thread_ok_def, MEM_EL] >>
    `action_id_lt (FST (HD th'.outbox)) oid
      = action_id_lt (EL 0 (MAP FST th'.outbox))
                     (EL (n' + 1) (MAP FST th'.outbox))`
      by (simp[EL_MAP] >> `n' + 1 < LENGTH th'.outbox` by simp[] >>
          metis_tac[rich_listTheory.EL_DROP, pairTheory.FST]) >>
    pop_assum (fn x => SUBST_TAC [x]) >>
    match_mp_tac imp_sorted_action_id >>
    rw[sorted_map |> ISPEC ``action_id_lt`` |> REWRITE_RULE[
      relationTheory.transitive_def, relationTheory.inv_image_def,
      action_id_lt_trans]],

    multi_case_tac >> fs[extract_def] >> rw[] >>
    first_x_assum match_mp_tac >> qexists_tac `th'` >> rw[] >>
    prove_tac[rich_listTheory.MEM_DROP_IMP]])

val proceed_outbox_program_order = prove(
  ``∀tid guess.
      propagates (state_ok ∩ outbox_program_order) (try_step (Proceed tid guess))``,

  Cases >> rw[propagates_def, IN_APP]
  >- prove_tac[propagates_def, try_step_ok] >>
  fs[outbox_program_order_def, try_step_def, take_step_def, get_thread_def] >>
  multi_case_tac >> fs[resolve_all_preserves, EL_LUPDATE, state_ok_def] >>
  multi_case_tac >>

  TRY (
    Cases_on `MEM (oid, oact) x.outbox`
    >- (first_x_assum match_mp_tac >> qexists_tac `x` >> rw[])) >>

  Cases_on `cmsg` >> rw[program_order_def] >>
  qmatch_rename_tac `_ ≠ SOME (Thread tid') ∨ _` >>
  qmatch_abbrev_tac `thr ≠ SOME (Thread tid') ∨ _` >>
  Cases_on `thr = SOME (Thread tid')` >> simp[] >>
  Cases_on `tid' < LENGTH a.threads` >>
  fs[rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2] >>

  imp_res_tac exec_terminst_follows >> fs[thread_follows_def] >>
  RES_TAC >> fs[EVERY_EL, MEM_EL] >>

  `message_ok a.threads (Message (SOME (Thread tid')) a' a0)`
    suffices_by (rw[message_ok_def] >>
      prove_tac[action_id_lt_trans, program_order_def]) >>
  prove_tac[])

val seq_cst_schedule_outbox_program_order = store_thm(
  "seq_cst_schedule_outbox_program_order",
  ``∀len n fs.
      0 < n
    ∧ LTAKE len (seq_cst_schedule n) = SOME fs
    ⇒ propagates (state_ok ∩ outbox_program_order) (run_finite_schedule fs)``,
    
  Induct >> rw[propagates_def, IN_APP] >| [
  
    prove_tac[propagates_def, run_finite_schedule_ok],
  
    fs[run_finite_schedule_def, init_sched_state_def, get_thread_def,
        outbox_program_order_def] >>
    rw[] >> fs[resolve_all_preserves],
  
    prove_tac[propagates_def, run_finite_schedule_ok],
  
    fs[LTAKE_SNOC_LNTH] >> every_case_tac >> rw[] >>
    fs[ONCE_REWRITE_RULE [EQ_SYM_EQ] SNOC_APPEND] >>
    imp_res_tac run_finite_schedule_last_step >| [
    
      fs[propagates_def, IN_APP] >> metis_tac[],
    
      Cases_on `x` >| [
      
        imp_res_tac seq_cst_schedule_commit_0 >>
        assume_tac commit_0_outbox_program_order >> fs[propagates_def, IN_APP] >>
        metis_tac[],
      
        assume_tac proceed_outbox_program_order >> fs[propagates_def, IN_APP] >>
        metis_tac[]]]])

(*
val seq_cst_schedule_sorted = store_thm("seq_cst_schedule_sorted",
  ``∀p n. 0 < n
    ⇒ schedule_valid (λs. SORTED (inv program_order) s.memory.committed) p
                     (seq_cst_schedule n)``,
  rw[schedule_valid_def, single_thread_seq_cst_schedule_def,
      sumMonadTheory.merge_left_def] >>
  CASE_TAC >> fs[] >> rw[] >>
  POP_ASSUM_LIST (map_every mp_tac) >>
  map_every qid_spec_tac [`s`, `fs`, `len`] >>
  Induct >> rw[] >| [

    (* Base case: nil schedule *)
    fs[run_finite_schedule_def, init_sched_state_def, APP_DEF, REVERSE_GENLIST] >>
    rw[resolve_all_preserves, SORTED_EL_SUC, relationTheory.inv_DEF] >>
    Cases_on `SUC n' = LENGTH p.env.globals`
    >- rw[SNOC_APPEND, rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2,
         LENGTH_GENLIST, program_order_def, action_id_lt_def]
    >- (`SUC n' < LENGTH p.env.globals` by simp[] >>
        rw[SNOC_APPEND,  rich_listTheory.EL_APPEND1, program_order_def,
            action_id_lt_def]),

    (* Inductive case *)
    fs[LTAKE_SNOC_LNTH] >>
    every_case_tac >> fs[] >> rw[] >>
    fs[ONCE_REWRITE_RULE [EQ_SYM_EQ] SNOC_APPEND] >>
    imp_res_tac run_finite_schedule_last_step >>
    imp_res_tac init_sched_state_ok >> rw[] >>
    `outbox_program_order y0`
      by (rw[outbox_program_order_def, get_thread_def] >>
          fs[init_sched_state_def] >> rw[] >> fs[]) >>
    `outbox_program_order last`
      by (assume_tac seq_cst_schedule_outbox_program_order >>
          fs[propagates_def, IN_APP] >> RES_TAC) >>
    map_every (fn x => Cases_on x >> simp[]) [`s.memory.committed`, `t`] >>
    (SORTED_DEF |> CONJUNCTS |> last |> IMP_CANON |> hd |> EQ_IMP_RULE |> #2
      |> match_mp_tac) >> rw[] >>
    
    fs[try_step_def] >> multi_case_tac >>
    Cases_on `x` >> Cases_on `t` >> fs[take_step_def] >> multi_case_tac >>
    fs[resolve_all_preserves, extract_def, SORTED_DEF] >>

    rw[relationTheory.inv_DEF] >>
    qpat_assum `outbox_program_order last`
      (match_mp_tac o REWRITE_RULE [outbox_program_order_def]) >>
    rw[] >> prove_tac[MEM_EL]])
*)

val seq_cst_schedule_program_order = store_thm("seq_cst_schedule_program_order",
  ``∀p n. 0 < n
    ⇒ schedule_valid (λs. ∀i j. i < LENGTH s.memory.committed ∧ j < i
                      ⇒ program_order (EL i s.memory.committed) (EL j s.memory.committed))
                     p
                     (seq_cst_schedule n)``,
  rw[schedule_valid_def, single_thread_seq_cst_schedule_def,
      sumMonadTheory.merge_left_def] >>
  CASE_TAC >> fs[] >> rw[] >>
  POP_ASSUM_LIST (map_every mp_tac) >>
  map_every qid_spec_tac [`i`, `j`, `s`, `fs`, `len`] >>
  Induct >> rw[] >| [

    fs[run_finite_schedule_def, init_sched_state_def, APP_DEF, REVERSE_GENLIST] >>
    rw[resolve_all_preserves] >> fs[resolve_all_preserves] >>
    Cases_on `i = LENGTH p.env.globals`
    >- rw[SNOC_APPEND, rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2,
         LENGTH_GENLIST, program_order_def, action_id_lt_def]
    >- (`j < LENGTH p.env.globals` by simp[] >>
        rw[SNOC_APPEND,  rich_listTheory.EL_APPEND1, program_order_def,
            action_id_lt_def]),

    fs[LTAKE_SNOC_LNTH] >>
    every_case_tac >> fs[] >> rw[] >>
    fs[ONCE_REWRITE_RULE [EQ_SYM_EQ] SNOC_APPEND] >>
    imp_res_tac run_finite_schedule_last_step >>
    imp_res_tac init_sched_state_ok >> rw[] >>
    `outbox_program_order y0`
      by (rw[outbox_program_order_def, get_thread_def] >>
          fs[init_sched_state_def] >> rw[] >> fs[]) >>
    `outbox_program_order last`
      by (assume_tac seq_cst_schedule_outbox_program_order >>
          fs[propagates_def, IN_APP] >> RES_TAC) >>
    fs[try_step_def] >> multi_case_tac >>
    Cases_on `x` >> Cases_on `t` >> fs[take_step_def] >> multi_case_tac >>
    fs[resolve_all_preserves, extract_def] >>
    Cases_on `j` >> fs[]
    >- (qpat_assum `outbox_program_order last`
          (match_mp_tac o REWRITE_RULE [outbox_program_order_def]) >>
        rw[] >> `∃i'. i = SUC i'` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >>
        `i' < LENGTH last.memory.committed` by simp[] >>
        simp[] >> prove_tac[MEM_EL])
    >- (`0 < i` by simp[] >>
        `∃i'. i = SUC i'` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >>
        `i' < LENGTH last.memory.committed` by simp[] >>
        simp[])])

(* Using seq_cst_schedule guarantees local sequential consistency. *)
val seq_cst_schedule_local_seq_cst = store_thm(
  "seq_cst_schedule_local_seq_cst",
  ``∀p n. 0 < n ⇒ schedule_valid (λs. local_seq_cst s.memory) p (seq_cst_schedule n)``,
  rw[] >> match_mp_tac (
    ISPEC ``state_ok ∩ (λs. ∀i j. i < LENGTH s.memory.committed ∧ j < i
                        ⇒ program_order (EL i s.memory.committed) (EL j s.memory.committed))``
          schedule_valid_monotonic) >>
  rw[seq_cst_schedule_program_order, schedule_valid_state_ok, schedule_valid_inter,
      local_seq_cst_def, EVERY_GENLIST, IN_APP] >>
  rw[EVERY_EL, rich_listTheory.EL_TAKE])

*)

(* For some reason HOL doesn't define this symbol by default... *)
val _ = TeX_notation{hol="⊌", TeX=("\\ensuremath{\\uplus}", 1)}

val _ = export_theory()