val split3 : s: FStar.Seq.Base.seq FStar.UInt8.t ->
    from: FStar.UInt32.t{FStar.UInt32.v from <= FStar.Seq.Base.length s} ->
    to: FStar.UInt32.t{FStar.UInt32.v to <= FStar.Seq.Base.length s - FStar.UInt32.v from}
  -> (FStar.Seq.Base.seq FStar.UInt8.t * FStar.Seq.Base.seq FStar.UInt8.t) *
    FStar.Seq.Base.seq FStar.UInt8.t
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)
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
/
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

    s: FStar.Seq.Base.seq FStar.UInt8.t ->
    from: FStar.UInt32.t{FStar.UInt32.v from <= FStar.Seq.Base.length s} ->
    to: FStar.UInt32.t{FStar.UInt32.v to <= FStar.Seq.Base.length s - FStar.UInt32.v from}
  -> (FStar.Seq.Base.seq FStar.UInt8.t * FStar.Seq.Base.seq FStar.UInt8.t) *
    FStar.Seq.Base.seq FStar.UInt8.t
FStar.Seq.Base.seq FStar.UInt8.t FStar.UInt32.t Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v FStar.Seq.Base.length Prims.op_Subtraction FStar.Pervasives.Native.Mktuple3 FStar.Seq.Base.slice Prims.op_Addition FStar.Pervasives.Native.tuple3
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)