evaluateScript.sml

(*
  Functional big-step semantics for evaluation of CakeML programs.
*)
open HolKernel Parse boolLib bossLib;
open libTheory fpValTreeTheory fpSemTheory astTheory namespaceTheory ffiTheory semanticPrimitivesTheory;

val _ = numLib.temp_prefer_num();

val _ = new_theory "evaluate"

(* The semantics is defined here using fix_clock so that HOL4 generates
 * provable termination conditions. However, after termination is proved, we
 * clean up the definition (in HOL4) to remove occurrences of fix_clock. *)

Definition fix_clock_def:
  fix_clock s (s',res) =
    (s' with clock := if s'.clock ≤ s.clock then s'.clock else s.clock, res)
End

Definition dec_clock_def:
  dec_clock s = (s with clock := s.clock − 1)
End

Definition do_eval_res_def:
  do_eval_res vs s =
    case do_eval vs s.eval_state of
    | NONE => (s,Rerr (Rabort Rtype_error))
    | SOME (env1,decs,es1) => (s with eval_state := es1,Rval (env1,decs))
End

(* list_result is equivalent to map_result (\v. [v]) I, where map_result is
 * defined in evalPropsTheory *)
Definition list_result_def[simp]:
  list_result (Rval v) = Rval [v] ∧
  list_result (Rerr e) = Rerr e
End

Triviality fix_clock_IMP:
  fix_clock s x = (s1,res) ==> s1.clock <= s.clock
Proof
  Cases_on ‘x’ \\ fs [fix_clock_def] \\ rw [] \\ fs []
QED

Triviality list_size_REVERSE:
  ∀xs. list_size f (REVERSE xs) = list_size f xs
Proof
  Induct \\ fs [listTheory.list_size_def,listTheory.list_size_append]
QED

Definition do_real_check_def:
  do_real_check b r=
  (if b then SOME r
   else (case r of
           Rval (Real r) => NONE
         | _ => SOME r))
End

Definition evaluate_def[nocompute]:
  evaluate st env [] = ((st:'ffi state),Rval [])
  ∧
  evaluate st env (e1::e2::es) =
    (case fix_clock st (evaluate st env [e1]) of
       (st',Rval v1) =>
         (case evaluate st' env (e2::es) of
            (st'',Rval vs) => (st'',Rval (HD v1::vs))
          | (st'',Rerr v8) => (st'',Rerr v8))
     | (st',Rerr v10) => (st',Rerr v10))
  ∧
  evaluate st env [Lit l] = (st,Rval [Litv l])
  ∧
  evaluate st env [Raise e] =
    (case evaluate st env [e] of
       (st',Rval v) => (st',Rerr (Rraise (HD v)))
     | (st',Rerr v8) => (st',Rerr v8))
  ∧
  evaluate st env [Handle e pes] =
    (case fix_clock st (evaluate st env [e]) of
       (st',Rval v7) => (st',Rval v7)
     | (st',Rerr (Rraise v)) =>
       if can_pmatch_all env.c st'.refs (MAP FST pes) v then
         evaluate_match st' env v pes v
       else (st',Rerr (Rabort Rtype_error))
     | (st',Rerr (Rabort v12)) => (st',Rerr (Rabort v12)))
  ∧
  evaluate st env [Con cn es] =
    (if do_con_check env.c cn (LENGTH es) then
       case evaluate st env (REVERSE es) of
         (st',Rval vs) =>
           (case build_conv env.c cn (REVERSE vs) of
              NONE => (st',Rerr (Rabort Rtype_error))
            | SOME v => (st',Rval [v]))
       | (st',Rerr v8) => (st',Rerr v8)
     else (st,Rerr (Rabort Rtype_error)))
  ∧
  evaluate st env [Var n] =
    (case nsLookup env.v n of
       NONE => (st,Rerr (Rabort Rtype_error))
     | SOME v => (st,Rval [v]))
  ∧
  evaluate st env [Fun x e] = (st,Rval [Closure env x e])
  ∧
  evaluate st env [App op es] =
   (case fix_clock st (evaluate st env (REVERSE es)) of
    (st', Rval vs) =>
    (case (getOpClass op) of
      FunApp =>
        (case do_opapp (REVERSE vs) of
          SOME (env',e) =>
            if st'.clock =( 0 : num) then
              (st', Rerr (Rabort Rtimeout_error))
            else
              evaluate (dec_clock st') env'  [e]
        | NONE => (st', Rerr (Rabort Rtype_error))
        )
     |EvalOp =>
        (case fix_clock st' (do_eval_res (REVERSE vs) st') of
          (st1, Rval (env1, decs)) =>
            if st1.clock = 0 then
              (st1, Rerr (Rabort Rtimeout_error))
            else
              (case fix_clock (dec_clock st1)
                      (evaluate_decs (dec_clock st1) env1 decs) of
                (st2, Rval env2) => (case declare_env st2.eval_state
                  (extend_dec_env env2 env1) of
                  SOME (x, es2) => (( st2 with<| eval_state :=
                    (reset_env_generation st'.eval_state es2) |>), Rval [x])
                | NONE => (st2, Rerr (Rabort Rtype_error)))
              | (st2, Rerr (Rabort a)) => (st2, Rerr (Rabort a))
              | (st2, Rerr e) => (( st2 with<| eval_state :=
                  (reset_env_generation st'.eval_state st2.eval_state) |>), Rerr e))
        | (st1, Rerr e) => (st1, Rerr e))
    | Simple =>
        (case do_app (st'.refs,st'.ffi) op (REVERSE vs) of
          NONE => (st', Rerr (Rabort Rtype_error))
        | SOME ((refs,ffi),r) =>
            (( st' with<| refs := refs; ffi := ffi |>), list_result r))
    | Icing =>
      (case do_app (st'.refs,st'.ffi) op (REVERSE vs) of
        NONE => (st', Rerr (Rabort Rtype_error))
      | SOME ((refs,ffi),r) =>
        let fp_opt =
          (if (st'.fp_state.canOpt = FPScope Opt)
          then
            ((case (do_fprw r (st'.fp_state.opts 0) st'.fp_state.rws) of
            (* if it fails, just use the old value tree *)
              NONE => r
            | SOME r_opt => r_opt
            ))
            (* If we cannot optimize, we should not allow matching on the structure in the oracle *)
          else r)
        in
        let stN = (if (st'.fp_state.canOpt = FPScope Opt) then shift_fp_opts st' else st') in
        let fp_res =
          (if (isFpBool op)
          then (case fp_opt of
              Rval (FP_BoolTree fv) => Rval (Boolv (compress_bool fv))
            | v => v
            )
          else fp_opt)
        in ((( stN with<| refs := refs; ffi := ffi |>)), list_result fp_res))
    | Reals =>
      if (st'.fp_state.real_sem) then
      (case do_app (st'.refs,st'.ffi) op (REVERSE vs) of
        NONE => (st', Rerr (Rabort Rtype_error))
      | SOME ((refs,ffi),r) =>
        (( st' with<| refs := refs; ffi := ffi |>), list_result r)
      )
      else (shift_fp_opts st', Rerr (Rabort Rtype_error)))
    | res => res)
  ∧
  evaluate st env [Log lop e1 e2] =
    (case fix_clock st (evaluate st env [e1]) of
       (st',Rval v1) =>
         (case do_log lop (HD v1) e2 of
            NONE => (st',Rerr (Rabort Rtype_error))
          | SOME (Exp e) => evaluate st' env [e]
          | SOME (Val v) => (st',Rval [v]))
     | (st',Rerr v9) => (st',Rerr v9))
  ∧
  evaluate st env [If e1 e2 e3] =
    (case fix_clock st (evaluate st env [e1]) of
       (st',Rval v) =>
         (case do_if (HD v) e2 e3 of
            NONE => (st',Rerr (Rabort Rtype_error))
          | SOME e => evaluate st' env [e])
     | (st',Rerr v8) => (st',Rerr v8))
  ∧
  evaluate st env [Mat e pes] =
    (case fix_clock st (evaluate st env [e]) of
       (st',Rval v) =>
         if can_pmatch_all env.c st'.refs (MAP FST pes) (HD v) then
           evaluate_match st' env (HD v) pes bind_exn_v
         else (st',Rerr (Rabort Rtype_error))
     | (st',Rerr v8) => (st',Rerr v8))
  ∧
  evaluate st env [Let xo e1 e2] =
    (case fix_clock st (evaluate st env [e1]) of
       (st',Rval v) =>
         evaluate st' (env with v := nsOptBind xo (HD v) env.v) [e2]
     | (st',Rerr v8) => (st',Rerr v8))
  ∧
  evaluate st env [Letrec funs e] =
    (if ALL_DISTINCT (MAP (λ(x,y,z). x) funs) then
       evaluate st (env with v := build_rec_env funs env env.v) [e]
     else (st,Rerr (Rabort Rtype_error)))
  ∧
  evaluate st env [Tannot e t] = evaluate st env [e]
  ∧
  evaluate st env [Lannot e l] = evaluate st env [e]
  ∧
  evaluate st env [FpOptimise annot e]=
   (let newFpState =
    (if (st.fp_state.canOpt = Strict)
    then st.fp_state
    else ( st.fp_state with<| canOpt := (FPScope annot)|>))
  in
    (case fix_clock st (evaluate (( st with<| fp_state := newFpState |>)) env [e]) of
      (st', Rval vs) =>
    (( st' with<| fp_state := (( st'.fp_state with<| canOpt := (st.fp_state.canOpt) |>)) |>),
        Rval (do_fpoptimise annot vs))
    | (st', Rerr e) =>
    (( st' with<| fp_state := (( st'.fp_state with<| canOpt := (st.fp_state.canOpt) |>)) |>), Rerr e)
    ))
  ∧
  evaluate_match st env v [] err_v = (st,Rerr (Rraise err_v))
  ∧
  evaluate_match st env v ((p,e)::pes) err_v =
    (if ALL_DISTINCT (pat_bindings p []) then
       case pmatch env.c st.refs p v [] of
         No_match => evaluate_match st env v pes err_v
       | Match_type_error => (st,Rerr (Rabort Rtype_error))
       | Match env_v' =>
         evaluate st (env with v := nsAppend (alist_to_ns env_v') env.v) [e]
     else (st,Rerr (Rabort Rtype_error)))
  ∧
  evaluate_decs st env [] = (st,Rval <|v := nsEmpty; c := nsEmpty|>)
  ∧
  evaluate_decs st env (d1::d2::ds) =
    (case fix_clock st (evaluate_decs st env [d1]) of
       (st1,Rval env1) =>
         (case evaluate_decs st1 (extend_dec_env env1 env) (d2::ds) of
            (st2,r) => (st2,combine_dec_result env1 r))
     | (st1,Rerr v7) => (st1,Rerr v7))
  ∧
  evaluate_decs st env [Dlet locs p e] =
    (if ALL_DISTINCT (pat_bindings p []) ∧
        every_exp (one_con_check env.c) e
     then
       case evaluate st env [e] of
         (st',Rval v) =>
           (st',
            case pmatch env.c st'.refs p (HD v) [] of
              No_match => Rerr (Rraise bind_exn_v)
            | Match_type_error => Rerr (Rabort Rtype_error)
            | Match new_vals =>
              Rval <|v := alist_to_ns new_vals; c := nsEmpty|>)
       | (st',Rerr err) => (st',Rerr err)
     else (st,Rerr (Rabort Rtype_error)))
  ∧
  evaluate_decs st env [Dletrec locs funs] =
    (st,
     if ALL_DISTINCT (MAP (λ(x,y,z). x) funs) ∧
        EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs
     then
       Rval <|v := build_rec_env funs env nsEmpty; c := nsEmpty|>
     else Rerr (Rabort Rtype_error))
  ∧
  evaluate_decs st env [Dtype locs tds] =
    (if EVERY check_dup_ctors tds then
       (st with next_type_stamp := st.next_type_stamp + LENGTH tds,
        Rval <|v := nsEmpty; c := build_tdefs st.next_type_stamp tds|>)
     else (st,Rerr (Rabort Rtype_error)))
  ∧
  evaluate_decs st env [Dtabbrev locs tvs tn t] =
    (st,Rval <|v := nsEmpty; c := nsEmpty|>)
  ∧
  evaluate_decs st env [Denv n] =
    (case declare_env st.eval_state env of
       NONE => (st,Rerr (Rabort Rtype_error))
     | SOME (x,es') =>
       (st with eval_state := es',Rval <|v := nsSing n x; c := nsEmpty|>))
  ∧
  evaluate_decs st env [Dexn locs cn ts] =
    (st with next_exn_stamp := st.next_exn_stamp + 1,
     Rval
       <|v := nsEmpty;
         c := nsSing cn (LENGTH ts,ExnStamp st.next_exn_stamp)|>)
  ∧
  evaluate_decs st env [Dmod mn ds] =
    (case evaluate_decs st env ds of
       (st',r) =>
         (st',
          case r of
            Rval env' =>
              Rval <|v := nsLift mn env'.v; c := nsLift mn env'.c|>
          | Rerr err => Rerr err))
  ∧
  evaluate_decs st env [Dlocal lds ds] =
    case fix_clock st (evaluate_decs st env lds) of
      (st1,Rval env1) => evaluate_decs st1 (extend_dec_env env1 env) ds
    | (st1,Rerr v7) => (st1,Rerr v7)
Termination
  WF_REL_TAC ‘inv_image ($< LEX $<)
    (λx. case x of
         | INL(s,_,es) => (s.clock,list_size exp_size es)
         | INR(INL (s,_,_,pes,_)) => (s.clock,list_size (pair_size pat_size exp_size) pes)
         | INR(INR (s,_,ds)) => (s.clock,list_size dec_size ds))’
  \\ rw [do_if_def,do_log_def,do_eval_res_def,dec_clock_def]
  \\ imp_res_tac fix_clock_IMP \\ fs []
  \\ fs [listTheory.list_size_def,dec_size_eq,exp_size_eq,list_size_REVERSE]
End

(* tidy up evalute_def and evaluate_ind *)

Theorem evaluate_clock:
  (∀(s1:'ffi state) env e r s2.
     evaluate s1 env e = (s2,r) ⇒ s2.clock ≤ s1.clock) ∧
  (∀(s1:'ffi state) env v p v' r s2.
     evaluate_match s1 env v p v' = (s2,r) ⇒ s2.clock ≤ s1.clock) ∧
  (∀(s1:'ffi state) env ds r s2.
     evaluate_decs s1 env ds = (s2,r) ⇒ s2.clock ≤ s1.clock)
Proof
  ho_match_mp_tac evaluate_ind >> rw[evaluate_def] >>
  gvs [AllCaseEqs()] >>
  fs[dec_clock_def,fix_clock_def] >> simp[] >>
  imp_res_tac fix_clock_IMP >> fs[shift_fp_opts_def] >>
  COND_CASES_TAC >> gs[]
QED

Theorem fix_clock_do_eval_res:
   fix_clock s (do_eval_res vs s) = do_eval_res vs s
Proof
  simp [do_eval_res_def]
  \\ rpt (CASE_TAC \\ fs [])
  \\ simp [fix_clock_def, state_component_equality]
QED

Theorem fix_clock_evaluate:
   fix_clock s1 (evaluate s1 env e) = evaluate s1 env e /\
   fix_clock s1 (evaluate_decs s1 env ds) = evaluate_decs s1 env ds
Proof
  Cases_on ‘evaluate s1 env e’ \\ fs [fix_clock_def]
  \\ Cases_on ‘evaluate_decs s1 env ds’ \\ fs [fix_clock_def]
  \\ imp_res_tac evaluate_clock
  \\ fs [arithmeticTheory.MIN_DEF,state_component_equality]
QED

Theorem fix_clock_fp_state:
  fix_clock st (evaluate (st with fp_state := newFpState) env [e]) =
    evaluate (st with fp_state := newFpState) env [e]
Proof
  qmatch_goalsub_abbrev_tac ‘evaluate newSt env [e]’
  \\ Cases_on ‘evaluate newSt env [e]’ \\ gs[fix_clock_def]
  \\ imp_res_tac evaluate_clock \\ unabbrev_all_tac
  \\ gs[arithmeticTheory.MIN_DEF,state_component_equality]
QED

Theorem full_evaluate_def[compute] =
  REWRITE_RULE [fix_clock_evaluate, fix_clock_do_eval_res, fix_clock_fp_state] evaluate_def;

Theorem full_evaluate_ind =
  REWRITE_RULE [fix_clock_evaluate, fix_clock_do_eval_res] evaluate_ind;

(* store evaluate_def and evaluate_ind in parts *)

val eval_pat = “evaluate$evaluate _ _ _”
val evaluate_conjs =
  CONJUNCTS full_evaluate_def
  |> filter (fn th => (th |> SPEC_ALL |> concl |> dest_eq |> fst
                          |> can (match_term eval_pat)));

val match_pat = “evaluate$evaluate_match _ _ _ _ _”
val evaluate_match_conjs =
  CONJUNCTS full_evaluate_def
  |> filter (fn th => (th |> SPEC_ALL |> concl |> dest_eq |> fst
                          |> can (match_term match_pat)));

val decs_pat = “evaluate$evaluate_decs _ _ _”
val evaluate_decs_conjs =
  CONJUNCTS full_evaluate_def
  |> filter (fn th => (th |> SPEC_ALL |> concl |> dest_eq |> fst
                          |> can (match_term decs_pat)));

Theorem evaluate_def[allow_rebind] = LIST_CONJ (evaluate_conjs @ evaluate_match_conjs);

Theorem evaluate_match_def = LIST_CONJ evaluate_match_conjs;

Theorem evaluate_decs_def = LIST_CONJ evaluate_decs_conjs;

Theorem evaluate_ind[allow_rebind] =
  full_evaluate_ind
  |> Q.SPECL [‘P1’,‘P2’,‘λv1 v2 v3. T’]
  |> SIMP_RULE std_ss []
  |> Q.GENL [‘P1’,‘P2’];

Theorem evaluate_match_ind =
  full_evaluate_ind
  |> Q.SPECL [‘λv1 v2 v3. T’,‘P2’,‘λv1 v2 v3. T’]
  |> SIMP_RULE std_ss []
  |> Q.GEN ‘P2’;

Theorem evaluate_decs_ind =
  full_evaluate_ind
  |> Q.SPECL [‘λv1 v2 v3. T’,‘λv1 v2 v3 v4 v5. T’,‘P’]
  |> SIMP_RULE std_ss []
  |> Q.GEN ‘P’;

val _ = export_theory()