open HolKernel Parse boolLib bossLib

open uvmMemoryTheory
open uvmIRTheory
open uvmValuesTheory
open uvmErrorsTheory
open uvmInstructionSemanticsTheory
open sumMonadTheory
open DefineUtils

open arithmeticTheory
open combinTheory
open finite_mapTheory
open patriciaTheory
open listTheory
open indexedListsTheory
open optionTheory
open pairTheory
open pred_setTheory
open relationTheory
open sortingTheory
open sptreeTheory
open lcsymtacs
open monadsyntax

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

val _ = Datatype`
  thread = <|
    sid: stack_id;
    sb: buffer;
    ib: buffer
  |>
`

val _ = Datatype`
  frame_state =
  | READY (uvm_type list) jumps
  | ACTIVE (opn list)
  | DEAD (value resume_values option) 
`

val _ = Datatype`
  frame = <|
    id: frame_id;
    fn: func_name;
    regs: mem_region;
    state: frame_state
  |>
`

val _ = Datatype`
  stack = <|
    frames: frame list;
    next_frame: frame_id
  |>
`

val frame_ok_def = Define`
  frame_ok (f : frame) ⇔
    mem_region_ok f.regs
`

val stack_ok_def = Define`
  stack_ok (s : stack) ⇔
    ¬NULL s.frames ∧
    EVERY (λf. frame_ok f ∧ f.id ≺ s.next_frame) s.frames ∧
    EVERY (λf. ¬∃ops. f.state = ACTIVE ops) (TL s.frames)
`

val thread_ok_def = Define`
  thread_ok (th : thread) ⇔ address_space_ok th.sb ∧ address_space_ok th.ib
`

(* A frame f₁ follows a previous frame f₀ iff f₁ is a valid future
   state of f₀. There are only two conditions on this: the frame's ID/function
   remains the same, and a dead frame cannot be modified or become alive again.

   This relation is a partial ordering on frames.
*)
val frame_follows_def = Define`
  frame_follows (f0 : frame) (f1 : frame) ⇔
    frame_ok f0
  ⇒ frame_ok f1
  ∧ (f0.id = f1.id)
  ∧ (f0.fn = f1.fn)
  ∧ (∀vs. f0.state = DEAD vs ⇒ f0 = f1)
`

val frame_follows_refl = store_thm("frame_follows_refl",
  ``∀s. frame_follows s s``,
  rw[frame_follows_def])

val frame_follows_trans = store_thm("frame_follows_trans",
  ``∀a b c. frame_follows a b ∧ frame_follows b c ⇒ frame_follows a c``,
  metis_tac[frame_follows_def])

(* A stack s₁ follows a previous stack s₀ iff s₁ is a valid future
   state of s₀.

   This relation is a partial ordering on stacks.
*)
val stack_follows_def = Define`
  stack_follows (s0 : stack) (s1 : stack) ⇔
    stack_ok s0
  ⇒ stack_ok s1
  ∧ s0.next_frame ≼ s1.next_frame
  ∧ EVERY (λn. n < LENGTH s0.frames
             ∧ frame_follows (EL n (REVERSE s0.frames)) (EL n (REVERSE s1.frames))
             ∨ s0.next_frame ≼ (EL n (REVERSE s1.frames)).id)
          (GENLIST I (LENGTH s1.frames))
`

val stack_follows_refl = store_thm("stack_follows_refl",
  ``∀s. stack_follows s s``,
  rw[stack_follows_def, EVERY_MEM, MEM_EL] >>
  rw[EL_GENLIST, frame_follows_refl])

val stack_follows_trans = store_thm("stack_follows_trans",
  ``∀a b c. stack_follows a b ∧ stack_follows b c ⇒ stack_follows a c``,
  rw[stack_follows_def, EVERY_EL] >| [
    prove_tac[frame_id_lt_trans],

    res_tac >> res_tac >>
    fs[EL_REVERSE] >> rfs[stack_ok_def, EVERY_EL, EL_REVERSE] >> 
    `∀m n. m < n ⇒ PRE (n - m) < n` by simp[] >>
    metis_tac[frame_follows_def, frame_id_lt_trans, EL_REVERSE]
  ])

val propagates_def = Define`
  propagates P f ⇔ ∀a b. P a ⇒ f a = OK b ⇒ P b
`

val frame_follows_ok = store_thm("frame_follows_ok",
  ``∀f. (∀t0 t1. f t0 = OK t1 ⇒ frame_follows t0 t1)
      ⇒ propagates frame_ok f``,
  rw[frame_follows_def, propagates_def] >> prove_tac[])

val imp_frame_follows_ok = store_thm("imp_frame_follows_ok",
  ``∀f t0 t1.  frame_ok t0 ∧ frame_follows t0 t1 ⇒ frame_ok t1``,
  rw[frame_follows_def])

val stack_follows_ok = store_thm("stack_follows_ok",
  ``∀f. (∀t0 t1. f t0 = OK t1 ⇒ stack_follows t0 t1)
      ⇒ propagates stack_ok f``,
  rw[stack_follows_def, propagates_def] >> prove_tac[])

val imp_stack_follows_ok = store_thm("imp_stack_follows_ok",
  ``∀f t0 t1.  stack_ok t0 ∧ stack_follows t0 t1 ⇒ stack_ok t1``,
  rw[stack_follows_def])

val imp_propagates = store_thm("imp_propagates",
  ``∀P f a b. propagates P f ∧ P a ⇒ f a = OK b ⇒ P b``,
  metis_tac[propagates_def])

val imp_propagates_fst = store_thm("imp_propagates_fst",
  ``∀P f a b b'. propagates P (liftM FST o f) ∧ P a ⇒ f a = OK (b, b') ⇒ P b``,
  rw[propagates_def] >> metis_tac[FST])

val imp_propagates_snd = store_thm("imp_propagates_snd",
  ``∀P f a b b'. propagates P (liftM SND o f) ∧ P a ⇒ f a = OK (b', b) ⇒ P b``,
  rw[propagates_def] >> metis_tac[SND])

val propagates_liftM = store_thm("propagates_liftM",
  ``∀P f g. propagates P (liftM g o f) ⇔ ∀a b. P a ∧ f a = OK b ⇒ P (g b)``,
  rw[propagates_def] >> metis_tac[])

val preserves_def = Define`
  preserves a f ⇔ ∀v. propagates ($= v o a) f
`

val imp_preserves = store_thm("imp_preserves",
  ``∀a f x y. preserves a f ⇒ f x = OK y ⇒ a x = a y``,
  rw[preserves_def, propagates_def])

val imp_preserves_snd = store_thm("imp_preserves_snd",
  ``∀a f x y y'. preserves a (liftM SND o f) ⇒ f x = OK (y', y) ⇒ a x = a y``,
  rw[propagates_def, preserves_def] >> metis_tac[SND])

val foldl_fail = store_thm("foldl_fail",
  ``∀f e. FOLDL (λs r. s >>= f r) (Fail e) rs = Fail e``,
  Induct_on `rs` >> fs[] >> Cases_on `h` >> fs[])

val foldl_follows = store_thm("foldl_follows",
  ``∀f t0 t1.
      (∀r t0 t1. (f r t0 = OK t1) ⇒ stack_follows t0 t1)
    ∧ (∃rs. FOLDL (λs r. s >>= f r) (OK t0) rs = OK t1)
    ⇒ stack_follows t0 t1``,
  rw[] >> pop_assum mp_tac >> map_every qid_spec_tac [`t0`, `t1`] >>
  Induct_on `rs` >> fs[FOLDL, stack_follows_refl] >> rw[] >>
  Cases_on `f h t0` >>
  metis_tac[stack_follows_trans, foldl_fail])

val foldl_propagates = store_thm("foldl_propagates",
  ``(∀r. propagates P (f r))
    ⇒ propagates P (λa. FOLDL (λs r. s >>= f r) (OK a) rs)``,
  strip_tac >> Induct_on `rs` >> rw[]
  >- (rw[propagates_def] >> simp[FOLDL])
  >- (rw[propagates_def] >> Cases_on `f h a` >> fs[propagates_def] >>
      metis_tac[foldl_fail]))

val imp_foldl_propagates = store_thm("imp_foldl_propagates",
  ``∀P. (∀r. propagates P (f r)) ∧ P a
      ∧ FOLDL (λs r. s >>= f r) (OK a) rs = OK b ⇒ P b``,
  rw[] >> pop_assum (mp_tac o CONV_RULE (UNBETA_CONV ``a`` |> LHS_CONV)) >>
  match_mp_tac imp_propagates >> simp[foldl_propagates])

val foldl_preserves = store_thm("foldl_preserves",
  ``(∀r. preserves a (f r))
    ⇒ preserves a (λx. FOLDL (λs r. s >>= f r) (OK x) rs)``,
  rw[preserves_def, foldl_propagates])

val imp_foldl_preserves = store_thm("imp_foldl_preserves",
  ``∀a. (∀r. preserves a (f r)) ∧ FOLDL (λs r. s >>= f r) (OK x) rs = OK y
      ⇒ a x = a y``,
  rw[] >> pop_assum (mp_tac o CONV_RULE (UNBETA_CONV ``x`` |> LHS_CONV)) >>
  match_mp_tac imp_preserves >> simp[foldl_preserves])

val set_register_def = Define`
  set_register ((reg, val) : num # value) (s : stack) : stack or_error =
  let f = HD s.frames in do
    assert (¬NULL s.frames) (InvalidState "stack underflow");
    assert (case f.state of DEAD _ => F | _ => T)
      (InvalidState "set_register on dead frame");
    regs <- mem_region_set_value "register" reg val f.regs;
    return (s with frames := (f with regs := regs)::TL s.frames)
  od
`

val set_register_follows = store_thm("set_register_follows",
  ``∀r s0 s1. set_register r s0 = OK s1 ⇒ stack_follows s0 s1``,
  Cases >> rw[set_register_def, stack_follows_def, stack_ok_def] >>
  fs[EVERY_EL] >> rw[] >>
  Cases_on `s0.frames` >> fs[LENGTH_CONS] >>
  Cases_on `n` >> res_tac >> fs[] >| [
    `frame_ok (EL 0 (h::t))` by simp[] >> fs[frame_ok_def] >>
      prove_tac[mem_region_set_value_ok],
    Cases_on `REVERSE t` >> fs[frame_follows_def, frame_ok_def] >>
      multi_case_tac >> prove_tac[mem_region_set_value_ok],
    ONCE_REWRITE_TAC[prove(``REVERSE t ++ [h] = REVERSE (h::t)``, simp[])] >>
      simp[EL_REVERSE] >> rw[] >> Cases_on `PRE (LENGTH t - n')` >>
      fs[frame_follows_def] >| [
        `frame_ok (EL 0 (h::t))` by simp[] >> fs[frame_ok_def] >>
          multi_case_tac >> prove_tac[mem_region_set_value_ok],
        `SUC n < SUC (LENGTH t)` by simp[] >> res_tac >> fs[]
      ]
  ])

val set_register_preserves = store_thm("set_register_preserves",
  ``∀r. preserves stack_next_frame (set_register r)
      ∧ preserves (TL o stack_frames) (set_register r)``,
  Cases >> rw[preserves_def, propagates_def, set_register_def] >> simp[])

val enqueue_store_def = Define`
  enqueue_store ((a, v) : addr # value) (th : thread) : thread =
    th with sb updated_by buffer_enqueue a v
`

val enqueue_invalidation_def = Define`
  enqueue_invalidation ((a, v) : addr # value) (th : thread) : thread =
    th with ib updated_by buffer_enqueue a v
`
(*
val enqueue_store_preserves = store_thm("enqueue_store_preserves",
  ``∀a. preserves thread_sid (enqueue_store a)
      ∧ preserves thread_ib (enqueue_store a)``,
  Cases >> rw[preserves_def, propagates_def, enqueue_store_def])

val enqueue_invalidation_preserves = store_thm("enqueue_invalidation_preserves",
  ``∀a. preserves thread_sid (enqueue_invalidation a)
      ∧ preserves thread_sb (enqueue_invalidation a)``,
  Cases >> rw[preserves_def, propagates_def, enqueue_invalidation_def])
*)
val jump_def = Define`
  jump (prg : program) (label : num) (args : value list) (st : stack)
       : stack or_error =
    let f = HD st.frames in do
      assert (¬NULL st.frames) (InvalidState "stack underflow");
      assert (case (HD st.frames).state of DEAD _ => F | _ => T)
        (InvalidState "jump on dead frame");
      blocks <- expect (FLOOKUP prg f.fn)
        (UndefinedBehavior "undefined function");
      block <- expect (lookup label blocks)
        (InvalidIR "undefined label");
      assert (LENGTH args = LENGTH block.params
            ∨ block.has_exc_param ∧ LENGTH args = SUC (LENGTH block.params))
        (InvalidIR "block arity mismatch");
      regs <- sptree$fromList <$> mapM (λ(arg, tys, offs). do
          assert (type_of_value arg = HD tys)
            (TypeMismatch "block argument" (type_of_value arg) (HD tys));
          return ((arg, tys, offs) : mem_cell)
        od) (ZIP (args, block.params));
      return (st with frames updated_by λfs.
        (HD fs with <|
          regs := if block.has_exc_param
                 then insert (LENGTH block.params)
                   ((if LENGTH args = LENGTH block.params
                     then RefV Void NONE
                     else EL (LENGTH block.params) args),
                    [Ref (Type Void)], []) regs
                 else regs;
          state := ACTIVE block.opns
        |>)::TL fs)
    od
`

val resume_stack_def = Define`
  resume_stack (prg : program) (rvs : value resume_values) (st : stack)
               : stack or_error =
    assert (¬NULL st.frames) (InvalidState "stack underflow") *>
    let f = HD st.frames in
    case f.state of
    | READY tys next => do
        (res_args, exc, label, params) <-
          case rvs of
          | NOR vs => return (vs, NONE, next.nor_jump)
          | EXC vs e => $, vs o $, (SOME e)
              <$> expect next.exc_jump (UndefinedBehavior "uncaught exception");
        args <- mapM (λparam.
            case param of
            | INR c => return c
            | INL n => if n < LENGTH res_args
                       then return (EL n res_args)
                       else Fail (InvalidState "missing resume argument"))
          params;
        jump prg label (option_CASE exc args (C SNOC args)) st
      od
    | _ => Fail (UndefinedBehavior "resuming non-READY frame")
`

val push_stack_def = Define`
  push_stack (prg : program)
             (fn : func_name)
             (sig : funcsig)
             (args : value list)
             (next : jumps option)
             (st : stack)
             : stack or_error =
    let new_frame = <|
      id := st.next_frame; fn := fn; regs := LN;
      state := READY sig.arg_types <|
        nor_jump := (0, GENLIST INL (LENGTH args));
        exc_jump := NONE
      |>
    |> in
    resume_stack prg (NOR args) (
      case next of
      (* SOME = normal call *)
      | SOME js => st with <|
          frames updated_by (λf.
            new_frame::(HD f with state := READY sig.return_types js)::TL f);
          next_frame updated_by frame_id_suc
        |>
      (* NONE = tail call *)
      | NONE => st with <|
          frames updated_by (λf. new_frame::TL f);
          next_frame updated_by frame_id_suc
        |>)
`

val pop_stack_def = Define`
  pop_stack (prg : program) (rvs : value resume_values) (st : stack)
            : stack or_error = do
    assert (¬NULL st.frames) (InvalidState "stack underflow");
    assert (case (HD st.frames).state of DEAD _ => F | _ => T)
      (InvalidState "pop_stack on dead frame");
    if NULL (TL st.frames)
    then return (st with frames :=
          [HD st.frames with state := DEAD (SOME rvs)])
    else resume_stack prg rvs (st with frames updated_by TL)
  od
`

val get_stack_def = Define`
  get_stack (id : stack_id) (stacks : stack list) : stack or_error =
    let n = stack_id_dest id in
    if n < LENGTH stacks
    then return (EL n stacks)
    else Fail (InvalidState "stack index out of bounds")
`

(* Creates a new thread with the given stack. *)
val new_thread_def = Define`
  new_thread (sid : stack_id) : thread =
    <| sid := sid; sb := new_address_space; ib := new_address_space |>
`

val new_thread_ok = store_thm("new_thread_ok",
  ``∀sid. thread_ok (new_thread sid)``,
  rw[thread_ok_def, new_thread_def, new_address_space_def,
     address_space_ok_def, wf_def, toList_def, toListA_def])

val _ = export_theory()