val synth_record
  (x: Zeta.Formats.Aux.Record.record)
: Tot Zeta.Steel.LogEntry.Types.record
val synth_record
  (x: Zeta.Formats.Aux.Record.record)
: Tot Zeta.Steel.LogEntry.Types.record
let synth_record
  (x: Zeta.Formats.Aux.Record.record)
: Tot Zeta.Steel.LogEntry.Types.record
= match x with
  | Zeta.Formats.Aux.Record.Record_kv_key_internal r ->
    (Zeta.Steel.LogEntry.Types.InternalKey r.ir_key,
     Zeta.Steel.LogEntry.Types.MValue (synth_mval_value r.ir_value)
    )
  | Zeta.Formats.Aux.Record.Record_kv_key_application r ->
    (Zeta.Steel.LogEntry.Types.ApplicationKey r.Zeta.Formats.Aux.Application_record.ar_key,
     Zeta.Steel.LogEntry.Types.DValue
      begin match r.Zeta.Formats.Aux.Application_record.v_payload with
      | Zeta.Formats.Aux.Application_record_v_payload.V_payload_DValueNone _ ->
        None
      | Zeta.Formats.Aux.Application_record_v_payload.V_payload_DValueSome v ->
        Some v
      end
    )
module Zeta.Formats.Synth

friend Zeta.Formats.Aux.External.App
friend Zeta.Formats.Aux.External

let synth_hash_value
  (x: Zeta.Formats.Aux.Hash_value.hash_value)
: Tot Zeta.Steel.LogEntry.Types.hash_value
= synth_u256 x

let synth_hash_value_recip
  (x: Zeta.Steel.LogEntry.Types.hash_value)
: Tot Zeta.Formats.Aux.Hash_value.hash_value
= synth_u256_recip x

let synth_vbool
  (x: Zeta.Formats.Aux.Vbool.vbool)
: Tot Zeta.Steel.LogEntry.Types.vbool
= match x with
  | Zeta.Formats.Aux.Vbool.Vfalse -> Zeta.Steel.LogEntry.Types.Vfalse
  | Zeta.Formats.Aux.Vbool.Vtrue -> Zeta.Steel.LogEntry.Types.Vtrue

let synth_vbool_recip
  (x: Zeta.Steel.LogEntry.Types.vbool)
: Tot Zeta.Formats.Aux.Vbool.vbool
= match x with
  | Zeta.Steel.LogEntry.Types.Vfalse -> Zeta.Formats.Aux.Vbool.Vfalse
  | Zeta.Steel.LogEntry.Types.Vtrue -> Zeta.Formats.Aux.Vbool.Vtrue

let synth_descendent_hash_desc
  (x: Zeta.Formats.Aux.Descendent_hash_desc.descendent_hash_desc)
: Tot Zeta.Steel.LogEntry.Types.descendent_hash_desc
= {
    Zeta.Steel.LogEntry.Types.dhd_key = x.Zeta.Formats.Aux.Descendent_hash_desc.dhd_key;
    Zeta.Steel.LogEntry.Types.dhd_h = synth_hash_value x.Zeta.Formats.Aux.Descendent_hash_desc.dhd_h;
    Zeta.Steel.LogEntry.Types.evicted_to_blum = synth_vbool x.Zeta.Formats.Aux.Descendent_hash_desc.evicted_to_blum;
  }

let synth_descendent_hash_desc_recip
  (x: Zeta.Steel.LogEntry.Types.descendent_hash_desc)
: Tot Zeta.Formats.Aux.Descendent_hash_desc.descendent_hash_desc
= {
    Zeta.Formats.Aux.Descendent_hash_desc.dhd_key = x.Zeta.Steel.LogEntry.Types.dhd_key;
    Zeta.Formats.Aux.Descendent_hash_desc.dhd_h = synth_hash_value_recip
    x.Zeta.Steel.LogEntry.Types.dhd_h;
    Zeta.Formats.Aux.Descendent_hash_desc.evicted_to_blum = synth_vbool_recip x.Zeta.Steel.LogEntry.Types.evicted_to_blum;
  }

let synth_descendent_hash
  (x: Zeta.Formats.Aux.Descendent_hash.descendent_hash)
: Tot Zeta.Steel.LogEntry.Types.descendent_hash
= match x with
  | Zeta.Formats.Aux.Descendent_hash.Dh_vnone _ -> Zeta.Steel.LogEntry.Types.Dh_vnone ()
  | Zeta.Formats.Aux.Descendent_hash.Dh_vsome d ->
    Zeta.Steel.LogEntry.Types.Dh_vsome (synth_descendent_hash_desc d)

let synth_descendent_hash_recip
  (x: Zeta.Steel.LogEntry.Types.descendent_hash)
: Tot Zeta.Formats.Aux.Descendent_hash.descendent_hash
= match x with
  | Zeta.Steel.LogEntry.Types.Dh_vnone () ->
    Zeta.Formats.Aux.Descendent_hash.Dh_vnone ()
  | Zeta.Steel.LogEntry.Types.Dh_vsome d ->
    Zeta.Formats.Aux.Descendent_hash.Dh_vsome (synth_descendent_hash_desc_recip d)

let synth_mval_value
  (x: Zeta.Formats.Aux.Mval_value.mval_value)
: Tot Zeta.Steel.LogEntry.Types.mval_value
= Zeta.Steel.LogEntry.Types.Mkmval_value
    (synth_descendent_hash x.Zeta.Formats.Aux.Mval_value.l)
    (synth_descendent_hash x.Zeta.Formats.Aux.Mval_value.r)

let synth_mval_value_recip
  (x: Zeta.Steel.LogEntry.Types.mval_value)
: Tot Zeta.Formats.Aux.Mval_value.mval_value
= match x with
  | Zeta.Steel.LogEntry.Types.Mkmval_value l r ->
    Zeta.Formats.Aux.Mval_value.Mkmval_value
      (synth_descendent_hash_recip l)
      (synth_descendent_hash_recip r)
/
Zeta.Steel.LogEntry.Types.fst.checked Zeta.Formats.Aux.Vbool.fsti.checked Zeta.Formats.Aux.Value.fsti.checked Zeta.Formats.Aux.Record.fsti.checked Zeta.Formats.Aux.Mval_value.fsti.checked Zeta.Formats.Aux.Internal_record.fsti.checked Zeta.Formats.Aux.Hash_value.fsti.checked Zeta.Formats.Aux.External.App.fst.checked Zeta.Formats.Aux.External.fst.checked Zeta.Formats.Aux.Descendent_hash_desc.fsti.checked Zeta.Formats.Aux.Descendent_hash.fsti.checked Zeta.Formats.Aux.Application_record_v_payload.fsti.checked Zeta.Formats.Aux.Application_record.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Formats.Synth.fst
x: Zeta.Formats.Aux.Record.record -> Zeta.Steel.LogEntry.Types.record
Zeta.Formats.Aux.Record.record Zeta.Formats.Aux.Internal_record.internal_record FStar.Pervasives.Native.Mktuple2 Zeta.Steel.LogEntry.Types.key Zeta.Steel.LogEntry.Types.value Zeta.Steel.LogEntry.Types.InternalKey Zeta.Formats.Aux.Internal_record.__proj__Mkinternal_record__item__ir_key Zeta.Steel.LogEntry.Types.MValue Zeta.Formats.Synth.synth_mval_value Zeta.Formats.Aux.Internal_record.__proj__Mkinternal_record__item__ir_value Zeta.Formats.Aux.Application_record.application_record Zeta.Steel.LogEntry.Types.ApplicationKey Zeta.Formats.Aux.Application_record.__proj__Mkapplication_record__item__ar_key Zeta.Steel.LogEntry.Types.DValue Zeta.Formats.Aux.Application_record.__proj__Mkapplication_record__item__v_payload Prims.unit FStar.Pervasives.Native.None Zeta.Steel.ApplicationTypes.value_type Zeta.Formats.Aux.Application_value.application_value FStar.Pervasives.Native.Some FStar.Pervasives.Native.option Zeta.Steel.LogEntry.Types.record
let synth_record (x: Zeta.Formats.Aux.Record.record) : Tot Zeta.Steel.LogEntry.Types.record =
  
match x with
| Zeta.Formats.Aux.Record.Record_kv_key_internal r ->
  (Zeta.Steel.LogEntry.Types.InternalKey r.ir_key,
    Zeta.Steel.LogEntry.Types.MValue (synth_mval_value r.ir_value))
| Zeta.Formats.Aux.Record.Record_kv_key_application r ->
  (Zeta.Steel.LogEntry.Types.ApplicationKey r.Zeta.Formats.Aux.Application_record.ar_key,
    Zeta.Steel.LogEntry.Types.DValue
    (match r.Zeta.Formats.Aux.Application_record.v_payload with
      | Zeta.Formats.Aux.Application_record_v_payload.V_payload_DValueNone _ -> None
      | Zeta.Formats.Aux.Application_record_v_payload.V_payload_DValueSome v -> Some v))