val hash_value : Type0
let hash_value = KU.u256
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
/
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
Type0
Zeta.Steel.KeyUtils.u256
let hash_value =
  
KU.u256