val comp_struct_def:struct_def comp_t
val comp_struct_def:struct_def comp_t
let comp_struct_def : struct_def comp_t =
  let fields = FStar.Set.add "limbs" (FStar.Set.singleton "precomp") in
  let fd_type (n: field_t fields) : Tot Type0 = match n with "limbs" -> base_array_t (scalar_t U64.t)  five 5sz | "precomp" -> base_array_t (scalar_t U64.t) twenty 20sz in
  let field_desc : field_description_gen_t (field_t fields) = {
    fd_nonempty = nonempty_set_nonempty_type "limbs" fields;
    fd_type = fd_type;
    fd_typedef = (fun (n: field_t fields) -> match n returns typedef (fd_type n) with "limbs" -> base_array0 five (scalar U64.t) 5sz | "precomp" -> base_array0 twenty (scalar U64.t) 20sz);
  }
  in {
    fields = fields;
    field_desc = field_desc;
    mk = (fun f -> Mkcomp_t (f "limbs") (f "precomp"));
    get = (fun x f -> match f with "limbs" -> x.limbs | "precomp" -> x.precomp);
    get_mk = (fun _ _ -> ());
    extensionality = (fun s1 s2 phi -> phi "limbs"; phi "precomp");
  }
module HaclExample
open Steel.ST.GenElim
open Steel.ST.C.Types
open Steel.C.Typenat
open Steel.C.Typestring
open Steel.ST.C.Types.Struct.Aux
open Steel.ST.C.Types.UserStruct // hides Struct

module SZ = FStar.SizeT
module U64 = FStar.UInt64

(** In this file we demonstrate how Steel could be used to manipulate the following data type used in Hacl*:
      https://github.com/project-everest/hacl-star/blob/master/code/poly1305/Hacl.Impl.Poly1305.fsti#L18
    This Low* definition amounts to the struct definition
      struct poly1305_ctx { uint64_t limbs[5]; uint64_t precomp[20]; };
    and, with our new model of structs and arrays and pointer-to-field, can be expresesd directly in Steel.

    See PointStruct.fst for more detailed explanations of the various definitions needed below.
*)

noextract inline_for_extraction let five = normalize (nat_t_of_nat 5)
noextract inline_for_extraction let twenty = normalize (nat_t_of_nat 20)
noextract inline_for_extraction let comp_name = normalize (mk_string_t "HaclExample2.comp")

noeq
type comp_t = {
  limbs: base_array_t (scalar_t U64.t)  five 5sz;
  precomp: base_array_t (scalar_t U64.t)  twenty 20sz;
}

noextract
inline_for_extraction
/
Steel.ST.GenElim.fsti.checked Steel.ST.C.Types.UserStruct.fsti.checked Steel.ST.C.Types.Struct.Aux.fsti.checked Steel.ST.C.Types.fst.checked Steel.C.Typestring.fsti.checked Steel.C.Typenat.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.SizeT.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
HaclExample.fst
Steel.ST.C.Types.UserStruct.struct_def HaclExample.comp_t
Steel.ST.C.Types.UserStruct.Mkstruct_def HaclExample.comp_t Steel.ST.C.Types.UserStruct.field_t Steel.ST.C.Types.Struct.Aux.__proj__Mkfield_description_gen_t__item__fd_type HaclExample.Mkcomp_t HaclExample.__proj__Mkcomp_t__item__limbs HaclExample.__proj__Mkcomp_t__item__precomp Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern Steel.ST.C.Types.Struct.Aux.field_description_gen_t Steel.ST.C.Types.Struct.Aux.Mkfield_description_gen_t Steel.ST.C.Types.UserStruct.nonempty_set_nonempty_type Steel.ST.C.Types.Base.typedef Steel.ST.C.Types.Array.base_array0 Steel.ST.C.Types.Scalar.scalar_t FStar.UInt64.t HaclExample.five Steel.ST.C.Types.Scalar.scalar FStar.SizeT.__uint_to_t HaclExample.twenty Steel.ST.C.Types.Array.base_array_t FStar.Set.set Prims.string FStar.Set.add FStar.Set.singleton
let comp_struct_def:struct_def comp_t =
  
let fields = FStar.Set.add "limbs" (FStar.Set.singleton "precomp") in
let fd_type (n: field_t fields) : Tot Type0 =
  match n with
  | "limbs" -> base_array_t (scalar_t U64.t) five 5sz
  | "precomp" -> base_array_t (scalar_t U64.t) twenty 20sz
in
let field_desc:field_description_gen_t (field_t fields) =
  {
    fd_nonempty = nonempty_set_nonempty_type "limbs" fields;
    fd_type = fd_type;
    fd_typedef
    =
    (fun (n: field_t fields) ->
        match n  returns typedef (fd_type n) with
        | "limbs" -> base_array0 five (scalar U64.t) 5sz
        | "precomp" -> base_array0 twenty (scalar U64.t) 20sz)
  }
in
{
  fields = fields;
  field_desc = field_desc;
  mk = (fun f -> Mkcomp_t (f "limbs") (f "precomp"));
  get
  =
  (fun x f ->
      match f with
      | "limbs" -> x.limbs
      | "precomp" -> x.precomp);
  get_mk = (fun _ _ -> ());
  extensionality
  =
  (fun s1 s2 phi ->
      phi "limbs";
      phi "precomp")
}