val valid_logS_entry : vs: Zeta.Intermediate.Verifier.vtls_t vcfg {Mkvtls_t?.valid vs} ->
    e: Zeta.Intermediate.Verifier.logS_entry vcfg
  -> Prims.bool
let valid_logS_entry (#vcfg:_)
                     (vs: vtls_t vcfg{vs.valid})
                     (e: logS_entry _) =
  let st = vs.st in
  let s2k = Store.to_slot_state_map st in
  Logs.valid_logS_entry s2k e
module Zeta.Intermediate.StateRel

open Zeta.GenKey
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.Store
open Zeta.Intermediate.Verifier
open Zeta.Intermediate.Logs

module FE = FStar.FunctionalExtensionality
module HV = Zeta.High.Verifier
module GV = Zeta.GenericVerifier
module Merkle = Zeta.Merkle
module S = FStar.Seq

(* Relation between thread-local states
   * either both states have Failed
   * or both are Valid with equal contents
     (note that store_rel st st' enforces is_map st) *)
let vtls_rel #vcfg (vs:vtls_t vcfg) (vs':HV.vtls_t vcfg.app) : Type =
  vs.valid = vs'.valid /\
  (vs.valid ==> (vs.tid = vs'.tid /\
                 vs.clock = vs'.clock /\
                 vs.last_evict_key = vs'.last_evict_key /\
                 store_rel vs.st vs'.st))
/
Zeta.Merkle.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.Intermediate.Logs.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Zeta.Intermediate.StateRel.fsti

    vs: Zeta.Intermediate.Verifier.vtls_t vcfg {Mkvtls_t?.valid vs} ->
    e: Zeta.Intermediate.Verifier.logS_entry vcfg
  -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Verifier.vtls_t Prims.b2t Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__valid Zeta.Intermediate.Verifier.logS_entry Zeta.Intermediate.Logs.valid_logS_entry Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.Store.to_slot_state_map Zeta.Intermediate.Store.vstore Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Prims.bool
let valid_logS_entry (#vcfg: _) (vs: vtls_t vcfg {vs.valid}) (e: logS_entry _) =
  
let st = vs.st in
let s2k = Store.to_slot_state_map st in
Logs.valid_logS_entry s2k e