val distinct_keys : sk: FStar.Seq.Base.seq (Zeta.App.app_record adm) -> Prims.logical
let distinct_keys #adm (sk: seq (app_record adm)) =
  forall (i1 i2: seq_index sk). i1 <> i2 ==> (let k1,_ = index sk i1 in
                                         let k2,_ = index sk i2 in
                                         k1 <> k2)
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

(* TODO: uncomment out TKey after the previous todo is completed (key is generalized) *)
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

(*
 * The function table
 *
 * Type of function identifiers
 *)
type fn_id = u8

(* data value with the option of a null type *)
type app_value_nullable (adm: app_data_model) =
  | Null: app_value_nullable adm
  | DValue: v: app_value adm -> app_value_nullable adm

(* an application record is a key-value pair *)
type app_record (adm: app_data_model) = app_key adm & app_value_nullable adm

(*
 * fn_sig is the signature that each function id in the table is mapped to
 *
 * It is parametrized by a, the type of the application specific state
 *
 * It contains the argument and result type of the function (their codes)
 *
 * f is the actual function
 *   it takes as input an argument of type (interp_code farg_t),
 *   a store st
 *     it must be the case that the footprint of f is contained in the store,
 *   and an application specific state
 *
 *   f then returns a result value (of type (interp_code fres_t)), and a new store and app state
 *)
type fn_return_code =
  | Fn_success
  | Fn_failure
/
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
sk: FStar.Seq.Base.seq (Zeta.App.app_record adm) -> Prims.logical
Zeta.App.app_data_model FStar.Seq.Base.seq Zeta.App.app_record Prims.l_Forall Zeta.SeqAux.seq_index Prims.l_imp Prims.b2t Prims.op_disEquality Zeta.App.app_key Zeta.App.app_value_nullable Prims.logical FStar.Seq.Base.index
let distinct_keys #adm (sk: seq (app_record adm)) =
  
forall (i1: seq_index sk) (i2: seq_index sk).
  i1 <> i2 ==>
  (let k1, _ = index sk i1 in
    let k2, _ = index sk i2 in
    k1 <> k2)