val interp_code (adm: app_data_model) (c: code) : eqtype
val interp_code (adm: app_data_model) (c: code) : eqtype
let rec interp_code (adm: app_data_model) (c:code) : eqtype =
  match c with
  | TUnit -> unit
  | TUInt8 -> u8
  | TUInt16 -> u16
  | TUInt32 -> u32
  | TUInt64 -> u64
  | TKey -> app_key adm
  | TValue -> app_value adm
  | TPair c1 c2 -> interp_code adm c1 & interp_code adm c2
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

(* value type of the application *)
let app_value (adm: app_data_model) = AppDataModel?.value 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 -> c: Zeta.App.code -> Prims.eqtype
Zeta.App.app_data_model Zeta.App.code Prims.unit Zeta.App.u8 Zeta.App.u16 Zeta.App.u32 Zeta.App.u64 Zeta.App.app_key Zeta.App.app_value FStar.Pervasives.Native.tuple2 Zeta.App.interp_code Prims.eqtype
let rec interp_code (adm: app_data_model) (c: code) : eqtype =
  
match c with
| TUnit -> unit
| TUInt8 -> u8
| TUInt16 -> u16
| TUInt32 -> u32
| TUInt64 -> u64
| TKey -> app_key adm
| TValue -> app_value adm
| TPair c1 c2 -> interp_code adm c1 & interp_code adm c2