val verify_runapp_entry_post
      (tsm: M.thread_state_model)
      (t: V.thread_state_t)
      (pl: runApp_payload)
      (out_bytes: bytes)
      (out_offset: U32.t)
      (out: A.array U8.t)
      ([@@@ smt_fallback]res: verify_runapp_result)
    : vprop
val verify_runapp_entry_post
      (tsm: M.thread_state_model)
      (t: V.thread_state_t)
      (pl: runApp_payload)
      (out_bytes: bytes)
      (out_offset: U32.t)
      (out: A.array U8.t)
      ([@@@ smt_fallback]res: verify_runapp_result)
    : vprop
let verify_runapp_entry_post (tsm:M.thread_state_model)
                             (t:V.thread_state_t)
                             (pl: runApp_payload)
                             (out_bytes:bytes)
                             (out_offset:U32.t)
                             (out:A.array U8.t)
                             ([@@@smt_fallback] res:verify_runapp_result)
  : vprop
  = match res with
    | Run_app_parsing_failure
    | Run_app_verify_failure ->
      //failure, but leaves state unchanged
      V.thread_state_inv t tsm `star`
      array_pts_to out out_bytes

    | Run_app_success wrote ->
      exists_ (fun (out_bytes':Seq.seq U8.t) ->
        (let tsm' = M.verify_step_model tsm (RunApp pl) in
         V.thread_state_inv t tsm' `star` //tsm' is the new state of the thread
         array_pts_to out out_bytes' `star`
         pure (n_out_bytes tsm tsm' out_offset wrote out_bytes out_bytes')))
module Zeta.Steel.Application
(**
 * This interface will be instantiated by each Zeta application
 * It requires:
 *
 *    - A function to parse keys and values from raw bytes
 *
 *    - A function to run each application-specific state transition
 *      with specs relating it to the high-level model of a Zeta
 *      application
 **)
open Steel.ST.Util
open Zeta.Steel.ApplicationTypes
open Zeta.Steel.Util
module Parser = Zeta.Steel.Parser
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module A = Steel.ST.Array
module M = Zeta.Steel.ThreadStateModel
module V = Zeta.Steel.VerifierTypes
open Zeta.Steel.FormatsManual

noextract
let split3 (s:Seq.seq U8.t)
           (from:U32.t { U32.v from <= Seq.length s})
           (to:U32.t { U32.v to <= Seq.length s - U32.v from })
  = Seq.slice s 0 (U32.v from),
    Seq.slice s (U32.v from) (U32.v from + U32.v to),
    Seq.slice s (U32.v from + U32.v to) (Seq.length s)

let n_out_bytes (tsm tsm': M.thread_state_model)
                (out_offset:U32.t)
                (n_out:U32.t)
                (out_bytes_init:Seq.seq U8.t)
                (out_bytes_final:Seq.seq U8.t)
  : prop
  = Seq.length out_bytes_init == Seq.length out_bytes_final /\
    U32.v out_offset <= Seq.length out_bytes_init /\
    U32.v n_out <= Seq.length out_bytes_init - U32.v out_offset /\
    (let pfx, _, sfx = split3 out_bytes_init out_offset n_out in
     let pfx', s, sfx' = split3 out_bytes_final out_offset n_out in
     pfx `Seq.equal` pfx' /\
     sfx `Seq.equal` sfx' /\
     s `Seq.equal` M.delta_out_bytes tsm tsm')

type verify_runapp_result =
  | Run_app_parsing_failure: verify_runapp_result
  | Run_app_verify_failure: verify_runapp_result
  | Run_app_success: wrote:U32.t -> verify_runapp_result
/
Zeta.Steel.VerifierTypes.fsti.checked Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.Application.fsti

    tsm: Zeta.Steel.ThreadStateModel.thread_state_model ->
    t: Zeta.Steel.VerifierTypes.thread_state_t ->
    pl: Zeta.Steel.LogEntry.Types.runApp_payload ->
    out_bytes: Zeta.Steel.ApplicationTypes.bytes ->
    out_offset: FStar.UInt32.t ->
    out: Steel.ST.Array.array FStar.UInt8.t ->
    res: Zeta.Steel.Application.verify_runapp_result
  -> Steel.Effect.Common.vprop
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.VerifierTypes.thread_state_t Zeta.Steel.LogEntry.Types.runApp_payload Zeta.Steel.ApplicationTypes.bytes FStar.UInt32.t Steel.ST.Array.array FStar.UInt8.t Zeta.Steel.Application.verify_runapp_result Steel.Effect.Common.star Zeta.Steel.VerifierTypes.thread_state_inv Zeta.Steel.Util.array_pts_to Steel.ST.Util.exists_ FStar.Seq.Base.seq Steel.ST.Util.pure Zeta.Steel.Application.n_out_bytes Zeta.Steel.ThreadStateModel.verify_step_model Zeta.Steel.LogEntry.Types.RunApp Steel.Effect.Common.vprop
let verify_runapp_entry_post
      (tsm: M.thread_state_model)
      (t: V.thread_state_t)
      (pl: runApp_payload)
      (out_bytes: bytes)
      (out_offset: U32.t)
      (out: A.array U8.t)
      ([@@@ smt_fallback]res: verify_runapp_result)
    : vprop =
  
match res with
| Run_app_parsing_failure
| Run_app_verify_failure -> (V.thread_state_inv t tsm) `star` (array_pts_to out out_bytes)
| Run_app_success wrote ->
  exists_ (fun (out_bytes': Seq.seq U8.t) ->
        (let tsm' = M.verify_step_model tsm (RunApp pl) in
          ((V.thread_state_inv t tsm') `star` (array_pts_to out out_bytes'))
          `star`
          (pure (n_out_bytes tsm tsm' out_offset wrote out_bytes out_bytes'))))