val do_something_with_limbs (#v: Ghost.erased (Seq.seq (scalar_t U64.t))) (a: array (scalar U64.t))
    : ST (Ghost.erased (Seq.seq (scalar_t U64.t)))
      (array_pts_to a v)
      (fun v' -> array_pts_to a v')
      (requires
        array_length a == 5 /\ fractionable_seq (scalar U64.t) v /\ full_seq (scalar U64.t) v)
      (ensures (fun v' -> fractionable_seq (scalar U64.t) v' /\ full_seq (scalar U64.t) v'))
val do_something_with_limbs (#v: Ghost.erased (Seq.seq (scalar_t U64.t))) (a: array (scalar U64.t))
    : ST (Ghost.erased (Seq.seq (scalar_t U64.t)))
      (array_pts_to a v)
      (fun v' -> array_pts_to a v')
      (requires
        array_length a == 5 /\ fractionable_seq (scalar U64.t) v /\ full_seq (scalar U64.t) v)
      (ensures (fun v' -> fractionable_seq (scalar U64.t) v' /\ full_seq (scalar U64.t) v'))
let do_something_with_limbs
  (#v: Ghost.erased (Seq.seq (scalar_t U64.t)))
  (a: array (scalar U64.t))
: ST (Ghost.erased (Seq.seq (scalar_t U64.t)))
    (array_pts_to a v)
    (fun v' -> array_pts_to a v')
    (requires
      array_length a == 5 /\
      fractionable_seq (scalar U64.t) v /\
      full_seq (scalar U64.t) v
    )
    (ensures (fun v' ->
      fractionable_seq (scalar U64.t) v' /\
      full_seq (scalar U64.t) v'
    ))
= let p = array_cell a 2sz in
  write p 0uL;
  unarray_cell _ _ _;
  drop (has_array_cell _ _ _); 
  return _
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
[@@ norm_field_attr]
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");
  }

noextract inline_for_extraction
let comp = struct_typedef comp_struct_def

(** To demonstrate how our model could be used, we write a simple
    function that takes pointers to the limbs and precomp fields and
    passes them to helper functions (which in this case simply set on
    element of the corresponding array to zero) *)
/
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
a: Steel.ST.C.Types.Array.array (Steel.ST.C.Types.Scalar.scalar FStar.UInt64.t)
  -> Steel.ST.Effect.ST
    (FStar.Ghost.erased (FStar.Seq.Base.seq (Steel.ST.C.Types.Scalar.scalar_t FStar.UInt64.t)))
FStar.Ghost.erased FStar.Seq.Base.seq Steel.ST.C.Types.Scalar.scalar_t FStar.UInt64.t Steel.ST.C.Types.Array.array Steel.ST.C.Types.Scalar.scalar Steel.ST.Util.return FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.C.Types.Array.array_pts_to Steel.Effect.Common.vprop FStar.Seq.Base.upd FStar.Ghost.reveal Steel.ST.C.Types.Base.unknown Steel.ST.C.Types.Base.mk_fraction Steel.ST.C.Types.Scalar.mk_scalar FStar.UInt64.__uint_to_t Steel.FractionalPermission.full_perm Prims.unit Steel.ST.Util.drop Steel.ST.C.Types.Array.has_array_cell FStar.SizeT.__uint_to_t Steel.ST.C.Types.Array.unarray_cell Prims.squash Prims.l_and Prims.b2t Prims.op_LessThan FStar.SizeT.v FStar.Seq.Base.length Prims.eq2 Prims.nat FStar.SizeT.t FStar.Pervasives.dsnd Steel.ST.C.Types.Array.array_ptr Steel.ST.C.Types.Array.array_len_t Steel.ST.C.Types.Scalar.write FStar.Seq.Base.index Steel.ST.C.Types.Base.ref FStar.SizeT.uint_to_t Steel.ST.C.Types.Array.array_cell Prims.int Steel.ST.C.Types.Array.array_length Steel.ST.C.Types.Array.fractionable_seq Steel.ST.C.Types.Array.full_seq Prims.l_True
let do_something_with_limbs (#v: Ghost.erased (Seq.seq (scalar_t U64.t))) (a: array (scalar U64.t))
    : ST (Ghost.erased (Seq.seq (scalar_t U64.t)))
      (array_pts_to a v)
      (fun v' -> array_pts_to a v')
      (requires
        array_length a == 5 /\ fractionable_seq (scalar U64.t) v /\ full_seq (scalar U64.t) v)
      (ensures (fun v' -> fractionable_seq (scalar U64.t) v' /\ full_seq (scalar U64.t) v')) =
  
let p = array_cell a 2sz in
write p 0uL;
unarray_cell _ _ _;
drop (has_array_cell _ _ _);
return _