val logK_entry : aprm: Zeta.App.app_params -> Prims.eqtype
let logK_entry = HV.vlog_entry
module Zeta.Intermediate.Logs

open FStar.Seq
open Zeta.SeqAux
open Zeta.Key
open Zeta.App
open Zeta.GenKey
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.SlotKeyRel
open Zeta.Intermediate.Verifier

module GV = Zeta.GenericVerifier
module HV = Zeta.High.Verifier


(* Definitions of different styles of verifier logs.
   - logK : contains only key references
   - logS: contains slot references
   - logL: contains slot references & low-level data structures (TODO) *)
/
Zeta.SeqAux.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.SlotKeyRel.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.Logs.fsti
aprm: Zeta.App.app_params -> Prims.eqtype
Zeta.High.Verifier.vlog_entry
let logK_entry =
  
HV.vlog_entry