val n_out_bytes
      (tsm tsm': M.thread_state_model)
      (out_offset n_out: U32.t)
      (out_bytes_init out_bytes_final: Seq.seq U8.t)
    : prop
val n_out_bytes
      (tsm tsm': M.thread_state_model)
      (out_offset n_out: U32.t)
      (out_bytes_init out_bytes_final: Seq.seq U8.t)
    : prop
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')
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)
/
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 ->
    tsm': Zeta.Steel.ThreadStateModel.thread_state_model ->
    out_offset: FStar.UInt32.t ->
    n_out: FStar.UInt32.t ->
    out_bytes_init: FStar.Seq.Base.seq FStar.UInt8.t ->
    out_bytes_final: FStar.Seq.Base.seq FStar.UInt8.t
  -> Prims.prop
Zeta.Steel.ThreadStateModel.thread_state_model FStar.UInt32.t FStar.Seq.Base.seq FStar.UInt8.t Prims.l_and Prims.eq2 Prims.nat FStar.Seq.Base.length Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_Subtraction FStar.Seq.Base.equal Zeta.Steel.ThreadStateModel.delta_out_bytes Prims.logical FStar.Pervasives.Native.tuple3 Zeta.Steel.Application.split3 Prims.prop
let n_out_bytes
      (tsm tsm': M.thread_state_model)
      (out_offset n_out: U32.t)
      (out_bytes_init 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'))