val synth_descendent_hash_recip (x: Zeta.Steel.LogEntry.Types.descendent_hash)
    : Tot Zeta.Formats.Aux.Descendent_hash.descendent_hash
val synth_descendent_hash_recip (x: Zeta.Steel.LogEntry.Types.descendent_hash)
    : Tot Zeta.Formats.Aux.Descendent_hash.descendent_hash
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)
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)
/
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.Steel.LogEntry.Types.descendent_hash -> Zeta.Formats.Aux.Descendent_hash.descendent_hash
Zeta.Steel.LogEntry.Types.descendent_hash Zeta.Formats.Aux.Descendent_hash.Dh_vnone Zeta.Steel.LogEntry.Types.descendent_hash_desc Zeta.Formats.Aux.Descendent_hash.Dh_vsome Zeta.Formats.Synth.synth_descendent_hash_desc_recip Zeta.Formats.Aux.Descendent_hash.descendent_hash
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)