val slot_id : Prims.eqtype
let slot_id = U16.t
module Zeta.Steel.LogEntry.Types
open Zeta.Steel.ApplicationRecord
include Zeta.Steel.KeyUtils
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module KU = Zeta.Steel.KeyUtils


// let significant_digits_t = significant_digits: U16.t { U16.v significant_digits <= 256 }

noeq 
type uninterpreted = {
 //  offset:U32.t; We'll need to know the offset in the input buffer where these bytes occur
 //  but this is probably not the place to stash it
  len: (len: U32.t { U32.v len < 2147483648 }); // FIXME: arbitrary bound due to the use of FStar.Bytes
  ebytes: (ebytes: Ghost.erased (Seq.seq U8.t) { Seq.length ebytes == U32.v len });
}

type timestamp = {
  epoch:U32.t;
  counter: U32.t
}

type thread_id = U16.t

let hash_value = KU.u256

type vbool =
  | Vfalse
  | Vtrue

noeq
type descendent_hash_desc = {
  dhd_key : base_key;
  dhd_h : hash_value;
  evicted_to_blum : vbool;
}

noeq
type descendent_hash =
  | Dh_vnone of unit
  | Dh_vsome of descendent_hash_desc

type value_kind =
  | Mval
  | Dval

noeq
type mval_value = {
  l : descendent_hash;
  r : descendent_hash;
}
/
Zeta.Steel.Parser.fst.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.ApplicationRecord.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.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.LogEntry.Types.fst
Prims.eqtype
FStar.UInt16.t
let slot_id =
  
U16.t