val app_value : adm: Zeta.App.app_data_model -> Prims.eqtype
let app_value (adm: app_data_model) = AppDataModel?.value adm
module Zeta.App

open FStar.Seq
open Zeta.Hash
open Zeta.Key
open Zeta.MultiSet
open Zeta.SeqAux

type u8 = FStar.UInt8.t
type u16 = FStar.UInt16.t
type u32 = FStar.UInt32.t
type u64 = FStar.UInt64.t

(*
 * We first define representation for the argument and result types of
 *   the functions that the verifier supports
 *
 * These are representations of the F* types,
 *   their interpretation is given by the interp_code function
 *
 * Note that we encode key and value also
 *   This allows us to pass around keys and values with other arguments,
 *   modeling multiple keys etc. using TPair
 *   For example, see below the representations for vget and vput (vget_sig and vput_sig)
 *
 *)

type code =
  | TUnit
  | TUInt8
  | TUInt16
  | TUInt32
  | TUInt64
  | TKey
  | TValue
  | TPair : code -> code -> code

(*
 * the application data model specifies the codes for key and data.
 * Currently, the keys are hard-coded to 256 bit vectors.
 *)
noeq type app_data_model =
  | AppDataModel: key: eqtype -> value: eqtype -> app_data_model

(* key type of the application *)
let app_key (adm: app_data_model) = AppDataModel?.key adm
/
Zeta.SeqAux.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Key.fsti.checked Zeta.Hash.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.Map.fsti.checked
Zeta.App.fsti
adm: Zeta.App.app_data_model -> Prims.eqtype
Zeta.App.app_data_model Zeta.App.__proj__AppDataModel__item__value Prims.eqtype
let app_value (adm: app_data_model) =
  
AppDataModel?.value adm